car-verify 0.37.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};

pub mod concurrency;
pub mod cwm;
pub mod dag;
pub mod goal;
pub mod infoflow;
pub mod intent;
pub mod plan_check;
pub mod transaction;
pub use goal::{
    anchor_directive, evaluate_goal, governor_check, run_goal_loop, GoalCondition, GoalGovernor,
    GoalHalt, GoalInputs, GoalRun, GoalRunState, GoalSpec, GoalStatus, GoalVerdict,
    IterationOutcome,
};
pub use intent::{
    check_intent, gate_intent, intent_actions_from, IntentAction, IntentDisposition,
    IntentGateDecision, IntentGatePolicy, IntentReport, IntentSpec, IntentViolation,
    IntentViolationKind,
};
pub use plan_check::{
    check_plan, PlanCheckReport, PlanCheckRequest, PlanDefect, PlanDefectKind, PlanStep,
};
pub mod workflow_graph;
pub use concurrency::{
    analyze as analyze_concurrency, gate_concurrency, AgentOp, AnomalyFinding, ConcurrencyAnomaly,
    ConcurrencyGate, ConcurrencyGatePolicy, ConcurrencyReport, ConsistencyLevel, Disposition,
    GatedRemediation, Remediation,
};
pub use cwm::{
    score, score_predictions, simulate_with_model, synthesize_cwm, CwmRequest, CwmResult,
    EffectModel, Failure, GatedEffectModel, GatedPrediction, ScoreReport, Transition,
};
pub use infoflow::{
    check_information_flow, gate_flow, Confidentiality, FlowAction, FlowGateDecision,
    FlowGatePolicy, FlowPolicy, FlowReport, FlowViolation, FlowViolationKind, ToolLabels,
    TrustLevel,
};
pub use transaction::{
    check_transaction, check_transaction_with_predictions, ConflictKind, TransactionConflict,
    TransactionReport,
};
pub use workflow_graph::{
    check_temporal_policies, verify_workflow_graph, PolicyReport, PolicyViolation, TemporalPolicy,
    WorkflowDefect, WorkflowDefectKind, WorkflowEdge, WorkflowGraph, WorkflowVerifyReport,
};

/// 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, serde::Serialize)]
pub struct VerifyIssue {
    pub action_id: String,
    pub severity: String, // "error", "warning", "info"
    pub message: String,
}

/// Scope record for one verification check.
///
/// Survey "Code as Agent Harness" §5.2.2 argues a green check creates a
/// false sense of correctness unless the verifier declares *what it
/// verifies, what it cannot verify, and what confidence it provides*. A
/// `CheckRecord` makes that scope explicit per check so downstream
/// consumers (self-repair, harness evolution, human review) can reason
/// about *why* a proposal is `valid`, not merely that it is.
#[derive(Debug, Clone, serde::Serialize)]
pub struct CheckRecord {
    /// Stable identifier, e.g. `"preconditions"`, `"tool_existence"`.
    pub name: String,
    /// Whether this check actually ran. Some checks are conditional —
    /// parameter-schema validation only runs when tool schemas are
    /// supplied; when skipped, `ran=false` and `cannot_verify` names the
    /// resulting blind spot.
    pub ran: bool,
    /// What a pass of this check establishes.
    pub verifies: String,
    /// The scope boundary: what a pass does *not* establish. The core
    /// anti-overconfidence signal.
    pub cannot_verify: String,
    /// Number of issues this check contributed to `issues`.
    pub findings: usize,
}

/// Evidence bundle accompanying a verification result.
///
/// Makes the verifier's scope inspectable so a `valid` verdict is not
/// mistaken for a full-specification guarantee (survey §5.2.2: "every
/// accepted action [should] carry an evidence bundle containing the
/// checks run, the assumptions preserved, the untested regions, and the
/// remaining risks"). Static verification is sound only within its
/// declared scope; this bundle is that declaration.
#[derive(Debug, Clone, serde::Serialize)]
pub struct VerificationEvidence {
    /// Per-check scope records.
    pub checks: Vec<CheckRecord>,
    /// Assumptions the verdict relies on (e.g. registered tools behave
    /// per their schema; supplied state values are accurate).
    pub assumptions: Vec<String>,
    /// State keys / aspects static verification could not evaluate —
    /// unknown or dynamic keys, and runtime-only tool outputs.
    pub untested_regions: Vec<String>,
    /// Risks that persist even when `valid` is true — downgraded
    /// warnings, undeclared write conflicts, dynamically-resolved
    /// preconditions.
    pub residual_risks: Vec<String>,
    /// Heuristic 0.0–1.0 coverage confidence: how completely the
    /// applicable checks covered this proposal. 1.0 means every
    /// applicable check ran against fully-known state with no warnings;
    /// reduced by skipped checks, unknown/dynamic state, and warnings.
    /// This is a coverage signal, not a probability of success.
    pub confidence: f64,
}

/// Complete verification result.
#[derive(Debug, serde::Serialize)]
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)
    /// Inspectable scope of this verdict (survey §5.2.2). See
    /// [`VerificationEvidence`].
    pub evidence: VerificationEvidence,
}

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) ---

pub(crate) 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();

    // Per-check finding counters for the evidence bundle (§5.2.2). The
    // topo-walk checks below are interleaved per action, so they are
    // tallied inline rather than by issue-vector deltas.
    let mut precondition_findings = 0usize;
    let mut state_dependency_findings = 0usize;
    let mut tool_existence_findings = 0usize;
    let mut param_schema_findings = 0usize;
    let mut has_tool_calls = false;
    // A malformed `tool_call` with no tool named is a structural finding
    // the existence pass produces even without a registry — track it so
    // the check's `ran` flag and `findings` count can't contradict
    // (neo review m1).
    let mut saw_missing_tool = false;
    // Which conditional checks actually ran, given the inputs we were
    // handed. Existence needs *some* tool registry; parameter-schema
    // validation needs the full schemas.
    let has_tool_registry = tool_schemas.is_some() || registered_tools.is_some();
    let param_schema_ran = tool_schemas.is_some();

    // Resource bounds
    let issues_before_bounds = issues.len();
    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
            ),
        });
    }

    let resource_bound_findings = issues.len() - issues_before_bounds;

    // Loop detection
    let issues_before_loop = issues.len();
    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),
            });
        }
    }

    let loop_detection_findings = issues.len() - issues_before_loop;

    // 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) {
                    precondition_findings += 1;
                    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) {
                    state_dependency_findings += 1;
                    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 {
                has_tool_calls = true;
                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) {
                        tool_existence_findings += 1;
                        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) {
                            param_schema_findings += 1;
                            issues.push(VerifyIssue {
                                action_id: action.id.clone(),
                                severity: "error".to_string(),
                                message: format!("tool '{tool}': {msg}"),
                            });
                        }
                    }
                } else {
                    saw_missing_tool = true;
                    tool_existence_findings += 1;
                    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 conflict_findings = conflicts.len();

    let has_errors = issues.iter().any(|i| i.severity == "error");
    let warning_count = issues.iter().filter(|i| i.severity == "warning").count();

    // --- Assemble the evidence bundle (§5.2.2) ---
    let checks = vec![
        CheckRecord {
            name: "resource_bounds".into(),
            ran: true,
            verifies: format!("action count is within the limit ({max_actions})"),
            cannot_verify: "per-action cost, wall-clock time, or memory at runtime".into(),
            findings: resource_bound_findings,
        },
        CheckRecord {
            name: "loop_detection".into(),
            ran: true,
            verifies: "no identical tool call is repeated enough to look like a loop".into(),
            cannot_verify: "semantically redundant calls with differing arguments".into(),
            findings: loop_detection_findings,
        },
        CheckRecord {
            name: "preconditions".into(),
            ran: true,
            verifies: "declared preconditions hold against the statically-known state".into(),
            cannot_verify: "preconditions over keys whose values are only known at runtime".into(),
            findings: precondition_findings,
        },
        CheckRecord {
            name: "state_dependencies".into(),
            ran: true,
            verifies: "each declared state dependency is produced before it is read".into(),
            cannot_verify: "undeclared reads — state a tool consumes without listing it".into(),
            findings: state_dependency_findings,
        },
        CheckRecord {
            // The existence pass "ran" if a registry let us check names,
            // or if it caught a structurally malformed tool_call (no tool
            // named) even without one — so `ran` and `findings` agree.
            name: "tool_existence".into(),
            ran: has_tool_registry || saw_missing_tool,
            verifies: if has_tool_registry {
                "every tool_call names a registered tool".into()
            } else if saw_missing_tool {
                "tool_call structural well-formedness (a tool is named); registry not supplied so existence unchecked".into()
            } else {
                "(skipped — no tool registry supplied)".into()
            },
            cannot_verify: "whether the registered tool behaves as its name/description implies"
                .into(),
            findings: tool_existence_findings,
        },
        CheckRecord {
            name: "param_schema".into(),
            ran: param_schema_ran,
            verifies: if param_schema_ran {
                "tool_call parameters match the registered JSON Schema (types + required)".into()
            } else {
                "(skipped — no tool schemas supplied; existence only)".into()
            },
            cannot_verify:
                "value-level constraints beyond type/required (ranges, formats, cross-field)".into(),
            findings: param_schema_findings,
        },
        CheckRecord {
            name: "write_conflicts".into(),
            ran: true,
            verifies: "concurrent writers to the same key declare an ordering dependency".into(),
            cannot_verify:
                "semantic conflicts — two actions whose effects are logically incompatible".into(),
            findings: conflict_findings,
        },
    ];

    // Untested regions: values the static pass cannot pin down because
    // they are only determined at runtime. A tool_call's return value is
    // opaque to static analysis, and any state key the tool is declared
    // to write holds a runtime-determined value (the declared effect is a
    // placeholder, not the real value). We source these from the IR
    // directly rather than from `StaticState`, which only tracks
    // statically-known values (neo review M1).
    let mut untested_regions: Vec<String> = Vec::new();
    for action in &proposal.actions {
        if action.action_type == ActionType::ToolCall {
            if let Some(ref tool) = action.tool {
                untested_regions.push(format!(
                    "runtime output of tool '{tool}' (action {})",
                    action.id
                ));
            }
            for key in action.expected_effects.keys() {
                untested_regions.push(format!(
                    "state key '{key}' (value set at runtime by action {})",
                    action.id
                ));
            }
        }
    }
    untested_regions.sort();
    untested_regions.dedup();

    let mut assumptions = vec![
        "supplied initial-state values are accurate".to_string(),
        "tool implementations honor their declared effects and side effects".to_string(),
    ];
    if !param_schema_ran && has_tool_calls {
        assumptions.push(
            "tool_call parameters are well-formed (no schemas supplied to check them)".to_string(),
        );
    }

    let mut residual_risks = Vec::new();
    if !conflicts.is_empty() {
        residual_risks.push(format!(
            "{} undeclared write conflict(s) — last-writer-wins at runtime",
            conflicts.len()
        ));
    }
    if warning_count > 0 {
        residual_risks.push(format!(
            "{warning_count} warning(s) not blocking the verdict"
        ));
    }
    if !untested_regions.is_empty() {
        residual_risks.push(
            "outcomes depending on runtime tool output or runtime-set state are unverified"
                .to_string(),
        );
    }

    // Coverage confidence: start full, dock for skipped applicable
    // checks, unknown/dynamic state, and warnings. A coverage signal,
    // not a probability — documented on the field.
    let mut confidence: f64 = 1.0;
    if has_tool_calls && !has_tool_registry {
        confidence -= 0.15;
    }
    if has_tool_calls && !param_schema_ran {
        confidence -= 0.20;
    }
    confidence -= (untested_regions.len() as f64 * 0.02).min(0.25);
    confidence -= (warning_count as f64 * 0.05).min(0.20);
    let confidence = confidence.clamp(0.0, 1.0);

    let evidence = VerificationEvidence {
        checks,
        assumptions,
        untested_regions,
        residual_risks,
        confidence,
    };

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

/// 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![],
            read_set: vec![],
            write_set: vec![],
            assumptions: vec![],
            invocation_mode: Default::default(),
            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![],
            read_set: vec![],
            write_set: vec![],
            assumptions: vec![],
            invocation_mode: Default::default(),
            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")));
    }

    // --- evidence bundle (§5.2.2) ---

    #[test]
    fn evidence_declares_all_check_scopes() {
        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);
        // Every check category is present with a non-empty scope.
        for want in [
            "resource_bounds",
            "loop_detection",
            "preconditions",
            "state_dependencies",
            "tool_existence",
            "param_schema",
            "write_conflicts",
        ] {
            let rec = r
                .evidence
                .checks
                .iter()
                .find(|c| c.name == want)
                .unwrap_or_else(|| panic!("missing check record {want}"));
            assert!(!rec.verifies.is_empty());
            assert!(!rec.cannot_verify.is_empty());
        }
        // With schemas supplied, both conditional checks ran.
        let by = |n: &str| r.evidence.checks.iter().find(|c| c.name == n).unwrap();
        assert!(by("param_schema").ran);
        assert!(by("tool_existence").ran);
    }

    #[test]
    fn evidence_marks_param_schema_skipped_without_schemas() {
        // Tool call but no schemas: param_schema can't run; confidence
        // is docked and the blind spot is recorded as an assumption.
        let p = prop(vec![tool_call("a1", "search")]);
        let r = verify(&p, None, None, 30);
        let param = r
            .evidence
            .checks
            .iter()
            .find(|c| c.name == "param_schema")
            .unwrap();
        assert!(!param.ran);
        assert!(
            r.evidence.confidence < 1.0,
            "skipped check should dock coverage"
        );
        assert!(r
            .evidence
            .assumptions
            .iter()
            .any(|a| a.contains("well-formed")));
    }

    #[test]
    fn evidence_full_confidence_for_pure_state_writes() {
        // No tool calls, fully-known state, no warnings: coverage is 1.0.
        let p = prop(vec![state_write("a1", "x", Value::from(1))]);
        let r = verify(&p, None, None, 30);
        assert!(r.valid);
        assert_eq!(r.evidence.confidence, 1.0);
        assert!(r.evidence.untested_regions.is_empty());
    }

    #[test]
    fn evidence_conflicts_become_residual_risk() {
        // Two undeclared writers to the same key: warning, not error, so
        // it must surface as a residual risk rather than vanish.
        let p = prop(vec![
            state_write("a1", "k", Value::from(1)),
            state_write("a2", "k", Value::from(2)),
        ]);
        let r = verify(&p, None, None, 30);
        assert!(r.valid, "conflicts are warnings, not errors");
        assert!(!r.conflicts.is_empty());
        assert!(r
            .evidence
            .residual_risks
            .iter()
            .any(|s| s.contains("write conflict")));
        let wc = r
            .evidence
            .checks
            .iter()
            .find(|c| c.name == "write_conflicts")
            .unwrap();
        assert_eq!(wc.findings, r.conflicts.len());
    }

    #[test]
    fn evidence_untested_includes_runtime_set_effect_keys() {
        // A tool whose declared effect writes `out`: the *key* exists
        // statically but its *value* is runtime-determined, so it is an
        // untested region — not just the tool's opaque return (neo M1).
        let mut a = tool_call("a1", "fetch");
        a.expected_effects = [("out".to_string(), Value::from("placeholder"))].into();
        let r = verify(
            &prop(vec![a]),
            None,
            Some(&["fetch".to_string()].into()),
            30,
        );
        assert!(r
            .evidence
            .untested_regions
            .iter()
            .any(|s| s.contains("state key 'out'")));
        assert!(r
            .evidence
            .untested_regions
            .iter()
            .any(|s| s.contains("runtime output of tool 'fetch'")));
    }

    #[test]
    fn evidence_tool_existence_ran_consistent_with_findings() {
        // Malformed tool_call (no tool named) with no registry supplied:
        // the existence record must not claim ran:false while reporting a
        // finding (neo m1).
        let mut a = tool_call("a1", "x");
        a.tool = None;
        let r = verify(&prop(vec![a]), None, None, 30);
        assert!(!r.valid);
        let te = r
            .evidence
            .checks
            .iter()
            .find(|c| c.name == "tool_existence")
            .unwrap();
        assert!(te.findings >= 1);
        assert!(
            te.ran,
            "ran must be true whenever the check produced a finding"
        );
    }
}