car-verify 0.18.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::precondition::{self, StateView};
use car_ir::{build_dag, Action, ActionProposal, ActionType, ToolSchema};
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
}

// --- Tool-parameter schema validation ---

/// Friendly JSON type name for error messages.
fn json_type_name(v: &Value) -> &'static str {
    match v {
        Value::Null => "null",
        Value::Bool(_) => "boolean",
        Value::Number(_) => "number",
        Value::String(_) => "string",
        Value::Array(_) => "array",
        Value::Object(_) => "object",
    }
}

/// Does `v` satisfy a single JSON Schema `type` keyword?
fn value_matches_type(v: &Value, expected: &str) -> bool {
    match expected {
        "string" => v.is_string(),
        "number" => v.is_number(),
        // JSON Schema "integer": an integral number. Accept i64/u64,
        // plus a float with no fractional part (e.g. `5.0`).
        "integer" => {
            v.is_i64() || v.is_u64() || v.as_f64().map(|f| f.fract() == 0.0).unwrap_or(false)
        }
        "boolean" => v.is_boolean(),
        "array" => v.is_array(),
        "object" => v.is_object(),
        "null" => v.is_null(),
        // Unknown/unsupported type keyword: don't flag — we only
        // enforce the keywords we understand.
        _ => true,
    }
}

/// Validate a tool_call's `parameters` against the tool's JSON-Schema
/// `parameters` object. Intentionally a focused subset of JSON Schema
/// — the two checks that catch the overwhelming majority of malformed
/// model output: declared property `type`s and `required` presence.
/// Returns human-readable violation messages; empty when the schema
/// imposes no constraints (e.g. the default empty object `{}`).
fn validate_tool_params(params: &HashMap<String, Value>, schema: &Value) -> Vec<String> {
    let mut out = Vec::new();
    let Some(schema_obj) = schema.as_object() else {
        // Non-object schema: nothing we can enforce.
        return out;
    };

    // required: every named key must be present in params.
    if let Some(Value::Array(required)) = schema_obj.get("required") {
        for req in required {
            if let Some(name) = req.as_str() {
                if !params.contains_key(name) {
                    out.push(format!("missing required parameter '{name}'"));
                }
            }
        }
    }

    // property types: each supplied param whose key has a declared
    // `type` must match it. `type` may be a string or an array of
    // strings (JSON Schema union).
    if let Some(Value::Object(properties)) = schema_obj.get("properties") {
        for (key, val) in params {
            let Some(prop_schema) = properties.get(key).and_then(|s| s.as_object()) else {
                continue;
            };
            let ok = match prop_schema.get("type") {
                Some(Value::String(t)) => value_matches_type(val, t),
                Some(Value::Array(types)) => types
                    .iter()
                    .filter_map(|t| t.as_str())
                    .any(|t| value_matches_type(val, t)),
                // No declared type (or non-string/array): accept.
                _ => true,
            };
            if !ok {
                let expected = match prop_schema.get("type") {
                    Some(Value::String(t)) => t.clone(),
                    Some(Value::Array(types)) => types
                        .iter()
                        .filter_map(|t| t.as_str())
                        .collect::<Vec<_>>()
                        .join("|"),
                    _ => String::new(),
                };
                out.push(format!(
                    "parameter '{key}' has wrong type: expected {expected}, got {}",
                    json_type_name(val)
                ));
            }
        }
    }

    out
}

// --- Core verification ---

/// Statically verify a proposal against an initial state.
///
/// `registered_tools` carries tool *names* only, so tool-existence is
/// checked but `parameters` are not. To additionally validate each
/// `tool_call`'s parameters against the tool's registered JSON Schema
/// (type mismatches, missing required fields), use
/// [`verify_with_schemas`].
pub fn verify(
    proposal: &ActionProposal,
    initial_state: Option<&HashMap<String, Value>>,
    registered_tools: Option<&HashSet<String>>,
    max_actions: usize,
) -> VerifyResult {
    verify_inner(proposal, initial_state, registered_tools, None, max_actions)
}

/// Like [`verify`], but validates each `tool_call`'s `parameters`
/// against the registered [`ToolSchema`]'s `parameters` JSON Schema —
/// catching type mismatches (`{"path": 42}` for a `string` param) and
/// missing `required` fields before dispatch. Tool existence is
/// checked against the schema map's keys. This is the path the runtime
/// (`verify_proposal`) and daemon (`verify` JSON-RPC) use, where the
/// full schemas registered via `register_tool_schema` are available.
pub fn verify_with_schemas(
    proposal: &ActionProposal,
    initial_state: Option<&HashMap<String, Value>>,
    tool_schemas: Option<&HashMap<String, ToolSchema>>,
    max_actions: usize,
) -> VerifyResult {
    verify_inner(proposal, initial_state, None, tool_schemas, max_actions)
}

fn verify_inner(
    proposal: &ActionProposal,
    initial_state: Option<&HashMap<String, Value>>,
    registered_tools: Option<&HashSet<String>>,
    tool_schemas: Option<&HashMap<String, ToolSchema>>,
    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 + parameter-schema validation
            if action.action_type == ActionType::ToolCall {
                if let Some(ref tool) = action.tool {
                    // Existence: prefer the schema map's keys, fall
                    // back to the name set. When neither is provided
                    // (both None) existence isn't checked.
                    let registered = match (tool_schemas, registered_tools) {
                        (Some(schemas), _) => Some(schemas.contains_key(tool.as_str())),
                        (None, Some(names)) => Some(names.contains(tool.as_str())),
                        (None, None) => None,
                    };
                    if registered == Some(false) {
                        issues.push(VerifyIssue {
                            action_id: action.id.clone(),
                            severity: "error".to_string(),
                            message: format!("tool '{}' is not registered", tool),
                        });
                    }
                    // Parameters: validate against the registered
                    // schema when we have one. This is the check the
                    // `register_tool_schema` contract promises —
                    // type mismatches and missing required fields.
                    if let Some(schema) = tool_schemas.and_then(|s| s.get(tool.as_str())) {
                        for msg in validate_tool_params(&action.parameters, &schema.parameters) {
                            issues.push(VerifyIssue {
                                action_id: action.id.clone(),
                                severity: "error".to_string(),
                                message: format!("tool '{tool}': {msg}"),
                            });
                        }
                    }
                } 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);
    }

    // --- tool-parameter schema validation (car-releases#56) ---

    fn echo_schema_parameters() -> Value {
        serde_json::json!({
            "type": "object",
            "properties": { "msg": { "type": "string" } },
            "required": ["msg"],
        })
    }

    fn schema_map(parameters: Value) -> HashMap<String, ToolSchema> {
        [(
            "echo".to_string(),
            ToolSchema {
                name: "echo".to_string(),
                description: String::new(),
                parameters,
                returns: None,
                idempotent: true,
                cache_ttl_secs: None,
                rate_limit: None,
            },
        )]
        .into()
    }

    fn echo_call(params: HashMap<String, Value>) -> ActionProposal {
        let mut a = tool_call("a1", "echo");
        a.parameters = params;
        prop(vec![a])
    }

    #[test]
    fn schema_verify_accepts_well_typed_params() {
        let p = echo_call([("msg".to_string(), Value::from("hi"))].into());
        let r = verify_with_schemas(&p, None, Some(&schema_map(echo_schema_parameters())), 30);
        assert!(r.valid, "{:?}", r.issues);
    }

    #[test]
    fn schema_verify_rejects_type_mismatch() {
        let p = echo_call([("msg".to_string(), Value::from(42))].into());
        let r = verify_with_schemas(&p, None, Some(&schema_map(echo_schema_parameters())), 30);
        assert!(!r.valid);
        assert!(r
            .issues
            .iter()
            .any(|i| i.message.contains("wrong type") && i.message.contains("msg")));
    }

    #[test]
    fn schema_verify_rejects_missing_required() {
        let p = echo_call(HashMap::new());
        let r = verify_with_schemas(&p, None, Some(&schema_map(echo_schema_parameters())), 30);
        assert!(!r.valid);
        assert!(r
            .issues
            .iter()
            .any(|i| i.message.contains("missing required parameter") && i.message.contains("msg")));
    }

    #[test]
    fn schema_verify_rejects_unknown_tool() {
        let mut a = tool_call("a1", "nope");
        a.parameters = [("msg".to_string(), Value::from("hi"))].into();
        let r = verify_with_schemas(&prop(vec![a]), None, Some(&schema_map(echo_schema_parameters())), 30);
        assert!(!r.valid);
        assert!(r.issues.iter().any(|i| i.message.contains("not registered")));
    }

    #[test]
    fn name_only_verify_still_skips_param_validation() {
        // Back-compat: verify() with names checks existence only. A
        // bad parameter type must NOT be flagged when no schema is
        // supplied — that path has no schema to validate against.
        let p = echo_call([("msg".to_string(), Value::from(42))].into());
        let r = verify(&p, None, Some(&["echo".to_string()].into()), 30);
        assert!(r.valid, "name-only verify must not validate params: {:?}", r.issues);
    }

    #[test]
    fn schema_verify_accepts_integer_and_union_types() {
        let parameters = serde_json::json!({
            "type": "object",
            "properties": {
                "n": { "type": "integer" },
                "maybe": { "type": ["string", "null"] },
            },
            "required": ["n"],
        });
        let p = echo_call(
            [
                ("n".to_string(), Value::from(7)),
                ("maybe".to_string(), Value::Null),
            ]
            .into(),
        );
        let r = verify_with_schemas(&p, None, Some(&schema_map(parameters)), 30);
        assert!(r.valid, "{:?}", r.issues);
    }

    #[test]
    fn schema_verify_empty_schema_imposes_no_constraints() {
        // Default `{}` parameters schema -> existence only, no param
        // checks (preserves behavior for tools registered without a
        // detailed schema).
        let p = echo_call([("anything".to_string(), Value::from(42))].into());
        let r = verify_with_schemas(&p, None, Some(&schema_map(serde_json::json!({}))), 30);
        assert!(r.valid, "{:?}", r.issues);
    }

    #[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")));
    }
}