car_ir/

precondition.rs

//! Shared precondition checking logic.
//!
//! Both static verification (car-verify) and runtime validation (car-validator)
//! need to check preconditions against state. This module provides a `StateView`
//! trait and a generic `check_precondition` function that both can reuse.

use crate::Precondition;
use serde_json::Value;

/// Abstraction over state access for precondition checking.
///
/// Implemented by both `car_verify::StaticState` (symbolic) and
/// `car_state::StateStore` (runtime).
pub trait StateView {
    /// Get a value by key. Returns `None` if the key doesn't exist.
    fn get_value(&self, key: &str) -> Option<Value>;

    /// Check if a key exists in state.
    fn key_exists(&self, key: &str) -> bool;

    /// Whether a key's value is unknown (symbolic analysis only).
    /// Returns `false` by default — runtime state is always known.
    fn is_unknown(&self, _key: &str) -> bool {
        false
    }
}

/// Check a single precondition against a state view.
///
/// Returns `Some(error_message)` if the precondition fails, `None` if it passes.
/// Supports operators: `exists`, `not_exists`, `eq`, `neq`, `gt`, `lt`, `gte`, `lte`, `contains`.
pub fn check_precondition(pre: &Precondition, state: &dyn StateView) -> Option<String> {
    let op = pre.operator.as_str();

    if op == "exists" {
        return if !state.key_exists(&pre.key) && !state.is_unknown(&pre.key) {
            Some(format!("key '{}' does not exist", pre.key))
        } else {
            None
        };
    }

    if op == "not_exists" {
        return if state.key_exists(&pre.key) || state.is_unknown(&pre.key) {
            Some(format!("key '{}' exists", pre.key))
        } else {
            None
        };
    }

    if op == "contains" {
        let current = state.get_value(&pre.key);
        return match current {
            None if state.is_unknown(&pre.key) => None,
            None => Some(format!("key '{}' has no value, cannot check contains", pre.key)),
            Some(val) => {
                let val_str = match &val {
                    Value::String(s) => s.clone(),
                    other => other.to_string(),
                };
                let needle = match &pre.value {
                    Value::String(s) => s.clone(),
                    other => other.to_string(),
                };
                if val_str.contains(&needle) {
                    None
                } else {
                    Some(format!("key '{}' does not contain {:?}", pre.key, pre.value))
                }
            }
        };
    }

    // For value-comparison operators, we need the current value
    if state.is_unknown(&pre.key) {
        return None; // can't disprove, assume ok
    }

    let current = state.get_value(&pre.key);
    if current.is_none() {
        return Some(format!("key '{}' has no value", pre.key));
    }
    let current = current.unwrap();

    match op {
        "eq" => {
            if current != pre.value {
                Some(format!("'{}' is {:?}, need {:?}", pre.key, current, pre.value))
            } else {
                None
            }
        }
        "neq" => {
            if current == pre.value {
                Some(format!("'{}' is {:?}, must not be", pre.key, current))
            } else {
                None
            }
        }
        "gt" | "lt" | "gte" | "lte" => {
            let c = current.as_f64();
            let e = pre.value.as_f64();
            match (c, e) {
                (Some(c), Some(e)) => {
                    let pass = match op {
                        "gt" => c > e,
                        "lt" => c < e,
                        "gte" => c >= e,
                        "lte" => c <= e,
                        _ => unreachable!(),
                    };
                    if !pass {
                        Some(format!("'{}' is {:?}, need {} {:?}", pre.key, current, op, pre.value))
                    } else {
                        None
                    }
                }
                _ => Some(format!("cannot compare '{}': {:?} {} {:?}", pre.key, current, op, pre.value)),
            }
        }
        _ => Some(format!("unknown operator '{}'", op)),
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use std::collections::HashMap;

    /// Simple in-memory state for testing.
    struct TestState {
        data: HashMap<String, Value>,
    }

    impl StateView for TestState {
        fn get_value(&self, key: &str) -> Option<Value> {
            self.data.get(key).cloned()
        }
        fn key_exists(&self, key: &str) -> bool {
            self.data.contains_key(key)
        }
    }

    fn pre(key: &str, op: &str, value: Value) -> Precondition {
        Precondition {
            key: key.to_string(),
            operator: op.to_string(),
            value,
            description: String::new(),
        }
    }

    #[test]
    fn exists_passes_when_present() {
        let state = TestState { data: [("x".into(), Value::from(1))].into() };
        assert!(check_precondition(&pre("x", "exists", Value::Null), &state).is_none());
    }

    #[test]
    fn exists_fails_when_absent() {
        let state = TestState { data: HashMap::new() };
        assert!(check_precondition(&pre("x", "exists", Value::Null), &state).is_some());
    }

    #[test]
    fn not_exists_passes_when_absent() {
        let state = TestState { data: HashMap::new() };
        assert!(check_precondition(&pre("x", "not_exists", Value::Null), &state).is_none());
    }

    #[test]
    fn eq_passes() {
        let state = TestState { data: [("x".into(), Value::from(42))].into() };
        assert!(check_precondition(&pre("x", "eq", Value::from(42)), &state).is_none());
    }

    #[test]
    fn eq_fails() {
        let state = TestState { data: [("x".into(), Value::from(1))].into() };
        assert!(check_precondition(&pre("x", "eq", Value::from(2)), &state).is_some());
    }

    #[test]
    fn neq_passes() {
        let state = TestState { data: [("x".into(), Value::from(1))].into() };
        assert!(check_precondition(&pre("x", "neq", Value::from(2)), &state).is_none());
    }

    #[test]
    fn gt_lt_gte_lte() {
        let state = TestState { data: [("n".into(), Value::from(10))].into() };
        assert!(check_precondition(&pre("n", "gt", Value::from(5)), &state).is_none());
        assert!(check_precondition(&pre("n", "gt", Value::from(20)), &state).is_some());
        assert!(check_precondition(&pre("n", "lt", Value::from(20)), &state).is_none());
        assert!(check_precondition(&pre("n", "gte", Value::from(10)), &state).is_none());
        assert!(check_precondition(&pre("n", "lte", Value::from(10)), &state).is_none());
    }

    #[test]
    fn contains_passes() {
        let state = TestState { data: [("msg".into(), Value::from("hello world"))].into() };
        assert!(check_precondition(&pre("msg", "contains", Value::from("world")), &state).is_none());
    }

    #[test]
    fn contains_fails() {
        let state = TestState { data: [("msg".into(), Value::from("hello"))].into() };
        assert!(check_precondition(&pre("msg", "contains", Value::from("world")), &state).is_some());
    }
}