car-verify 0.7.0

//! Formal verification for Agent IR.
//!
//! Given a state S and proposal P, you can:
//! 1. **verify**: Prove P is satisfiable in S without executing
//! 2. **simulate**: Compute expected final state S' without tools
//! 3. **equivalent**: Show two proposals produce identical state
//! 4. **optimize**: Reorder actions provably safely

use car_ir::{build_dag, Action, ActionProposal, ActionType};
use car_ir::precondition::{self, StateView};
use serde_json::Value;
use std::collections::{HashMap, HashSet};

/// Symbolic state for static analysis.
#[derive(Debug, Clone)]
pub struct StaticState {
    pub known: HashMap<String, Value>,
    pub unknown_keys: HashSet<String>,
}

impl StaticState {
    pub fn new() -> Self {
        Self {
            known: HashMap::new(),
            unknown_keys: HashSet::new(),
        }
    }

    pub fn from_map(map: HashMap<String, Value>) -> Self {
        Self {
            known: map,
            unknown_keys: HashSet::new(),
        }
    }

    pub fn get(&self, key: &str) -> Option<&Value> {
        self.known.get(key)
    }

    pub fn exists(&self, key: &str) -> bool {
        self.known.contains_key(key)
    }

    pub fn is_unknown(&self, key: &str) -> bool {
        self.unknown_keys.contains(key)
    }

    pub fn set(&mut self, key: &str, value: Value) {
        self.known.insert(key.to_string(), value);
        self.unknown_keys.remove(key);
    }
}

impl Default for StaticState {
    fn default() -> Self {
        Self::new()
    }
}

impl StateView for StaticState {
    fn get_value(&self, key: &str) -> Option<Value> {
        self.known.get(key).cloned()
    }
    fn key_exists(&self, key: &str) -> bool {
        self.known.contains_key(key)
    }
    fn is_unknown(&self, key: &str) -> bool {
        self.unknown_keys.contains(key)
    }
}

/// A single verification finding.
#[derive(Debug, Clone)]
pub struct VerifyIssue {
    pub action_id: String,
    pub severity: String, // "error", "warning", "info"
    pub message: String,
}

/// Complete verification result.
#[derive(Debug)]
pub struct VerifyResult {
    pub valid: bool,
    pub issues: Vec<VerifyIssue>,
    pub simulated_state: HashMap<String, Value>,
    pub execution_levels: Vec<Vec<String>>,
    pub conflicts: Vec<(String, String, String)>, // (action1, action2, key)
}

impl VerifyResult {
    pub fn errors(&self) -> Vec<&VerifyIssue> {
        self.issues.iter().filter(|i| i.severity == "error").collect()
    }

    pub fn warnings(&self) -> Vec<&VerifyIssue> {
        self.issues.iter().filter(|i| i.severity == "warning").collect()
    }
}

// --- Action effects (symbolic) ---

fn apply_action_effects(action: &Action, state: &mut StaticState) {
    if action.action_type == ActionType::StateWrite {
        if let Some(key) = action.parameters.get("key").and_then(|v| v.as_str()) {
            let value = action.parameters.get("value").cloned().unwrap_or(Value::Null);
            state.set(key, value);
        }
    }
    for (key, value) in &action.expected_effects {
        state.set(key, value.clone());
    }
}

// --- Conflict detection ---

fn detect_conflicts(actions: &[Action]) -> Vec<(String, String, String)> {
    let mut writers: HashMap<String, Vec<String>> = HashMap::new();

    for action in actions {
        let mut keys_written = HashSet::new();
        if action.action_type == ActionType::StateWrite {
            if let Some(k) = action.parameters.get("key").and_then(|v| v.as_str()) {
                keys_written.insert(k.to_string());
            }
        }
        for key in action.expected_effects.keys() {
            keys_written.insert(key.clone());
        }
        for key in keys_written {
            writers.entry(key).or_default().push(action.id.clone());
        }
    }

    let dep_map: HashMap<String, HashSet<String>> = actions
        .iter()
        .map(|a| (a.id.clone(), a.state_dependencies.iter().cloned().collect()))
        .collect();

    let mut conflicts = Vec::new();
    for (key, action_ids) in &writers {
        if action_ids.len() < 2 {
            continue;
        }
        for i in 0..action_ids.len() {
            for j in (i + 1)..action_ids.len() {
                let a1 = &action_ids[i];
                let a2 = &action_ids[j];
                let deps_a2 = dep_map.get(a2).cloned().unwrap_or_default();
                let deps_a1 = dep_map.get(a1).cloned().unwrap_or_default();
                if !deps_a2.contains(key) && !deps_a1.contains(key) {
                    conflicts.push((a1.clone(), a2.clone(), key.clone()));
                }
            }
        }
    }
    conflicts
}

// --- Core verification ---

/// Statically verify a proposal against an initial state.
pub fn verify(
    proposal: &ActionProposal,
    initial_state: Option<&HashMap<String, Value>>,
    registered_tools: Option<&HashSet<String>>,
    max_actions: usize,
) -> VerifyResult {
    let mut state = match initial_state {
        Some(s) => StaticState::from_map(s.clone()),
        None => StaticState::new(),
    };
    let mut issues = Vec::new();

    // Resource bounds
    if proposal.actions.len() > max_actions {
        issues.push(VerifyIssue {
            action_id: proposal.actions.first().map(|a| a.id.clone()).unwrap_or_default(),
            severity: "warning".to_string(),
            message: format!("excessive actions: {} (limit {})", proposal.actions.len(), max_actions),
        });
    }

    // Loop detection
    let mut seen_calls: HashMap<String, u32> = HashMap::new();
    for action in &proposal.actions {
        if action.action_type == ActionType::ToolCall {
            if let Some(ref tool) = action.tool {
                let params = serde_json::to_string(&action.parameters).unwrap_or_default();
                let key = format!("{}:{}", tool, params);
                *seen_calls.entry(key).or_insert(0) += 1;
            }
        }
    }
    for (call_key, count) in &seen_calls {
        let tool_name = call_key.split(':').next().unwrap_or("?");
        if *count >= 3 {
            issues.push(VerifyIssue {
                action_id: "proposal".to_string(),
                severity: "error".to_string(),
                message: format!("repeated identical tool call: {} ({}x) — likely loop", tool_name, count),
            });
        } else if *count == 2 {
            issues.push(VerifyIssue {
                action_id: "proposal".to_string(),
                severity: "warning".to_string(),
                message: format!("duplicate tool call: {} ({}x)", tool_name, count),
            });
        }
    }

    // Build DAG
    let levels = build_dag(&proposal.actions);
    let execution_levels: Vec<Vec<String>> = levels
        .iter()
        .map(|level| level.iter().map(|&i| proposal.actions[i].id.clone()).collect())
        .collect();

    // Walk in topological order
    for level in &levels {
        for &idx in level {
            let action = &proposal.actions[idx];

            // Check preconditions
            for pre in &action.preconditions {
                if let Some(error) = precondition::check_precondition(pre, &state) {
                    issues.push(VerifyIssue {
                        action_id: action.id.clone(),
                        severity: "error".to_string(),
                        message: format!("precondition will fail: {}", error),
                    });
                }
            }

            // State dependencies
            for dep in &action.state_dependencies {
                if !state.exists(dep) && !state.is_unknown(dep) {
                    issues.push(VerifyIssue {
                        action_id: action.id.clone(),
                        severity: "error".to_string(),
                        message: format!("state dependency '{}' not available at this point", dep),
                    });
                }
            }

            // Tool existence
            if action.action_type == ActionType::ToolCall {
                if let Some(ref tool) = action.tool {
                    if let Some(tools) = registered_tools {
                        if !tools.contains(tool.as_str()) {
                            issues.push(VerifyIssue {
                                action_id: action.id.clone(),
                                severity: "error".to_string(),
                                message: format!("tool '{}' is not registered", tool),
                            });
                        }
                    }
                } else {
                    issues.push(VerifyIssue {
                        action_id: action.id.clone(),
                        severity: "error".to_string(),
                        message: "tool_call action has no tool specified".to_string(),
                    });
                }
            }

            apply_action_effects(action, &mut state);
        }
    }

    // Conflicts
    let conflicts = detect_conflicts(&proposal.actions);
    for (a1, a2, key) in &conflicts {
        issues.push(VerifyIssue {
            action_id: a1.clone(),
            severity: "warning".to_string(),
            message: format!("write conflict on '{}' with action {} (no dependency declared)", key, a2),
        });
    }

    let has_errors = issues.iter().any(|i| i.severity == "error");

    VerifyResult {
        valid: !has_errors,
        issues,
        simulated_state: state.known,
        execution_levels,
        conflicts,
    }
}

/// Simulate a proposal's state effects without executing tools.
pub fn simulate(
    proposal: &ActionProposal,
    initial_state: Option<&HashMap<String, Value>>,
) -> HashMap<String, Value> {
    verify(proposal, initial_state, None, usize::MAX).simulated_state
}

/// Test if two proposals produce identical state transitions.
pub fn equivalent(
    p1: &ActionProposal,
    p2: &ActionProposal,
    test_states: Option<&[HashMap<String, Value>]>,
) -> bool {
    let defaults = vec![
        HashMap::new(),
        [("x".to_string(), Value::from(1)), ("y".to_string(), Value::from(2))].into(),
    ];
    let states = test_states.unwrap_or(&defaults);

    for state in states {
        let s1 = simulate(p1, Some(state));
        let s2 = simulate(p2, Some(state));
        if s1 != s2 {
            return false;
        }
    }
    true
}

/// Optimize a proposal: remove phantom dependencies to enable more parallelism.
pub fn optimize(proposal: &ActionProposal) -> ActionProposal {
    // Find which keys are actually written
    let mut written_keys = HashSet::new();
    for action in &proposal.actions {
        if action.action_type == ActionType::StateWrite {
            if let Some(k) = action.parameters.get("key").and_then(|v| v.as_str()) {
                written_keys.insert(k.to_string());
            }
        }
        for key in action.expected_effects.keys() {
            written_keys.insert(key.clone());
        }
    }

    let optimized_actions: Vec<Action> = proposal
        .actions
        .iter()
        .map(|action| {
            let pruned: Vec<String> = action
                .state_dependencies
                .iter()
                .filter(|d| written_keys.contains(d.as_str()))
                .cloned()
                .collect();

            if pruned.len() != action.state_dependencies.len() {
                let mut new_action = action.clone();
                new_action.state_dependencies = pruned;
                new_action
            } else {
                action.clone()
            }
        })
        .collect();

    ActionProposal {
        id: proposal.id.clone(),
        source: proposal.source.clone(),
        actions: optimized_actions,
        timestamp: proposal.timestamp,
        context: proposal.context.clone(),
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use car_ir::{FailureBehavior, Precondition};

    fn tool_call(id: &str, tool: &str) -> Action {
        Action {
            id: id.to_string(),
            action_type: ActionType::ToolCall,
            tool: Some(tool.to_string()),
            parameters: HashMap::new(),
            preconditions: vec![],
            expected_effects: HashMap::new(),
            state_dependencies: vec![],
            idempotent: false,
            max_retries: 3,
            failure_behavior: FailureBehavior::Abort,
            timeout_ms: None,
            metadata: HashMap::new(),
        }
    }

    fn state_write(id: &str, key: &str, value: Value) -> Action {
        Action {
            id: id.to_string(),
            action_type: ActionType::StateWrite,
            tool: None,
            parameters: [
                ("key".to_string(), Value::from(key)),
                ("value".to_string(), value),
            ]
            .into(),
            preconditions: vec![],
            expected_effects: HashMap::new(),
            state_dependencies: vec![],
            idempotent: false,
            max_retries: 3,
            failure_behavior: FailureBehavior::Abort,
            timeout_ms: None,
            metadata: HashMap::new(),
        }
    }

    fn prop(actions: Vec<Action>) -> ActionProposal {
        ActionProposal {
            id: "test".to_string(),
            source: "test".to_string(),
            actions,
            timestamp: chrono::Utc::now(),
            context: HashMap::new(),
        }
    }

    #[test]
    fn verify_valid_proposal() {
        let p = prop(vec![
            state_write("a1", "x", Value::from(1)),
            {
                let mut a = tool_call("a2", "search");
                a.state_dependencies = vec!["x".to_string()];
                a
            },
        ]);
        let r = verify(&p, None, Some(&["search".to_string()].into()), 30);
        assert!(r.valid);
    }

    #[test]
    fn verify_catches_unsatisfied_precondition() {
        let mut a = tool_call("a1", "deploy");
        a.preconditions = vec![Precondition {
            key: "tests_passed".to_string(),
            operator: "eq".to_string(),
            value: Value::Bool(true),
            description: String::new(),
        }];
        let r = verify(&prop(vec![a]), None, None, 30);
        assert!(!r.valid);
    }

    #[test]
    fn verify_precondition_satisfied_by_earlier_action() {
        let mut a2 = tool_call("a2", "deploy");
        a2.preconditions = vec![Precondition {
            key: "ready".to_string(),
            operator: "eq".to_string(),
            value: Value::Bool(true),
            description: String::new(),
        }];
        a2.state_dependencies = vec!["ready".to_string()];

        let p = prop(vec![state_write("a1", "ready", Value::Bool(true)), a2]);
        let r = verify(&p, None, None, 30);
        assert!(r.valid);
    }

    #[test]
    fn verify_missing_state_dependency() {
        let mut a = tool_call("a1", "x");
        a.state_dependencies = vec!["nonexistent".to_string()];
        let r = verify(&prop(vec![a]), None, None, 30);
        assert!(!r.valid);
    }

    #[test]
    fn verify_tool_not_registered() {
        let a = tool_call("a1", "quantum");
        let r = verify(&prop(vec![a]), None, Some(&HashSet::new()), 30);
        assert!(!r.valid);
    }

    #[test]
    fn verify_no_tool_specified() {
        let mut a = tool_call("a1", "x");
        a.tool = None;
        let r = verify(&prop(vec![a]), None, None, 30);
        assert!(!r.valid);
    }

    #[test]
    fn detect_write_conflict() {
        let p = prop(vec![
            state_write("a1", "x", Value::from(1)),
            state_write("a2", "x", Value::from(2)),
        ]);
        let r = verify(&p, None, None, 30);
        assert!(!r.conflicts.is_empty());
    }

    #[test]
    fn simulate_state_writes() {
        let p = prop(vec![
            state_write("a1", "x", Value::from(10)),
            state_write("a2", "y", Value::from(20)),
        ]);
        let s = simulate(&p, None);
        assert_eq!(s.get("x"), Some(&Value::from(10)));
        assert_eq!(s.get("y"), Some(&Value::from(20)));
    }

    #[test]
    fn equivalent_proposals() {
        let p1 = prop(vec![
            state_write("a1", "x", Value::from(1)),
            state_write("a2", "y", Value::from(2)),
        ]);
        let p2 = prop(vec![
            state_write("b1", "y", Value::from(2)),
            state_write("b2", "x", Value::from(1)),
        ]);
        assert!(equivalent(&p1, &p2, None));
    }

    #[test]
    fn non_equivalent_proposals() {
        let p1 = prop(vec![state_write("a1", "x", Value::from(1))]);
        let p2 = prop(vec![state_write("b1", "x", Value::from(99))]);
        assert!(!equivalent(&p1, &p2, None));
    }

    #[test]
    fn optimize_removes_phantom_deps() {
        let mut a = tool_call("a1", "search");
        a.state_dependencies = vec!["phantom".to_string()];
        let p = prop(vec![a]);
        let optimized = optimize(&p);
        assert!(optimized.actions[0].state_dependencies.is_empty());
    }

    #[test]
    fn optimize_preserves_real_deps() {
        let mut a2 = tool_call("a2", "x");
        a2.state_dependencies = vec!["x".to_string()];
        let p = prop(vec![state_write("a1", "x", Value::from(1)), a2]);
        let optimized = optimize(&p);
        assert_eq!(optimized.actions[1].state_dependencies, vec!["x"]);
    }

    #[test]
    fn loop_detection_duplicates() {
        let p = prop(vec![
            tool_call("a1", "search"),
            tool_call("a2", "search"),
        ]);
        let r = verify(&p, None, None, 30);
        assert!(r.issues.iter().any(|i| i.message.contains("duplicate")));
    }

    #[test]
    fn loop_detection_triple() {
        let p = prop(vec![
            tool_call("a1", "search"),
            tool_call("a2", "search"),
            tool_call("a3", "search"),
        ]);
        let r = verify(&p, None, None, 30);
        assert!(!r.valid);
        assert!(r.issues.iter().any(|i| i.message.contains("likely loop")));
    }

    #[test]
    fn resource_bounds() {
        let actions: Vec<Action> = (0..35)
            .map(|i| tool_call(&format!("a{}", i), &format!("t{}", i)))
            .collect();
        let r = verify(&prop(actions), None, None, 30);
        assert!(r.issues.iter().any(|i| i.message.contains("excessive")));
    }
}