car-verify 0.32.1

//! Symbolic plan precondition verification (arXiv 2603.14730, *GNNVerifier:
//! Graph-based Verifier for LLM Task Planning*; pre-execution premise shared
//! with *VerifyLLM*, arXiv 2507.05118).
//!
//! See `docs/proposals/plan-precondition-verification.md`. A plan can be fluent
//! and well-formed yet infeasible — a step whose preconditions the earlier steps
//! never establish. GNNVerifier learns to score a plan's precondition/effect
//! structure with a GNN; CAR computes the same diagnosis **deterministically and
//! training-free** by forward-simulating the plan over a symbolic fact set (the
//! classic STRIPS applicability check) — the verify-before-execute primitive the
//! runtime is built on, alongside [`crate::transaction`], [`crate::concurrency`],
//! and [`crate::workflow_graph`].

use serde::{Deserialize, Serialize};
use std::collections::BTreeSet;

/// One plan step in the STRIPS sense: facts it needs (`preconditions`), facts it
/// makes true (`add_effects`), and facts it makes false (`del_effects`).
#[derive(Debug, Clone, Default, Serialize, Deserialize)]
pub struct PlanStep {
    pub id: String,
    #[serde(default)]
    pub preconditions: Vec<String>,
    #[serde(default)]
    pub add_effects: Vec<String>,
    #[serde(default)]
    pub del_effects: Vec<String>,
}

/// A plan to verify: the facts true at the start, the ordered steps, and the
/// goal facts that must hold at the end.
#[derive(Debug, Clone, Default, Serialize, Deserialize)]
pub struct PlanCheckRequest {
    #[serde(default)]
    pub initial: Vec<String>,
    #[serde(default)]
    pub steps: Vec<PlanStep>,
    #[serde(default)]
    pub goal: Vec<String>,
}

/// The class of a plan defect.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
#[serde(rename_all = "snake_case")]
pub enum PlanDefectKind {
    /// A step required a fact that wasn't true when it ran.
    UnmetPrecondition,
    /// A goal fact was not true after the plan finished.
    GoalNotAchieved,
}

/// A single detected defect.
#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
pub struct PlanDefect {
    pub kind: PlanDefectKind,
    /// The step that failed its precondition (None for a goal defect).
    #[serde(default, skip_serializing_if = "Option::is_none")]
    pub step: Option<String>,
    /// The missing fact.
    pub fact: String,
    pub explanation: String,
}

/// The verification report.
#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
pub struct PlanCheckReport {
    pub valid: bool,
    pub defects: Vec<PlanDefect>,
    /// The simulated end state (sorted), for debugging / repair feedback.
    pub final_state: Vec<String>,
}

/// Verify a plan by forward-simulating its preconditions and effects over a
/// symbolic fact set. Deterministic and pure. Effects are applied even when a
/// step's precondition failed, so a single pass surfaces every defect.
pub fn check_plan(req: &PlanCheckRequest) -> PlanCheckReport {
    let mut state: BTreeSet<String> = req.initial.iter().cloned().collect();
    let mut defects = Vec::new();

    for step in &req.steps {
        for pre in &step.preconditions {
            if !state.contains(pre) {
                defects.push(PlanDefect {
                    kind: PlanDefectKind::UnmetPrecondition,
                    step: Some(step.id.clone()),
                    fact: pre.clone(),
                    explanation: format!(
                        "step '{}' requires '{}', which is not established by the preceding steps",
                        step.id, pre
                    ),
                });
            }
        }
        // Apply effects (deletes first, then adds, so a fact in both nets to true).
        for d in &step.del_effects {
            state.remove(d);
        }
        for a in &step.add_effects {
            state.insert(a.clone());
        }
    }

    for g in &req.goal {
        if !state.contains(g) {
            defects.push(PlanDefect {
                kind: PlanDefectKind::GoalNotAchieved,
                step: None,
                fact: g.clone(),
                explanation: format!("goal fact '{g}' does not hold after the plan finishes"),
            });
        }
    }

    PlanCheckReport {
        valid: defects.is_empty(),
        defects,
        final_state: state.into_iter().collect(),
    }
}

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

    fn step(id: &str, pre: &[&str], add: &[&str], del: &[&str]) -> PlanStep {
        PlanStep {
            id: id.into(),
            preconditions: pre.iter().map(|s| s.to_string()).collect(),
            add_effects: add.iter().map(|s| s.to_string()).collect(),
            del_effects: del.iter().map(|s| s.to_string()).collect(),
        }
    }

    fn req(initial: &[&str], steps: Vec<PlanStep>, goal: &[&str]) -> PlanCheckRequest {
        PlanCheckRequest {
            initial: initial.iter().map(|s| s.to_string()).collect(),
            steps,
            goal: goal.iter().map(|s| s.to_string()).collect(),
        }
    }

    #[test]
    fn feasible_plan_is_valid() {
        // have_ingredients -> cook (needs ingredients) -> serve (needs cooked).
        let r = check_plan(&req(
            &["ingredients"],
            vec![
                step("cook", &["ingredients"], &["cooked"], &["ingredients"]),
                step("serve", &["cooked"], &["served"], &[]),
            ],
            &["served"],
        ));
        assert!(r.valid, "{:?}", r.defects);
        assert!(r.final_state.contains(&"served".to_string()));
    }

    #[test]
    fn unmet_precondition_is_flagged_with_step_and_fact() {
        // 'serve' needs 'cooked' but nothing cooks.
        let r = check_plan(&req(
            &["ingredients"],
            vec![step("serve", &["cooked"], &["served"], &[])],
            &["served"],
        ));
        assert!(!r.valid);
        let d = &r.defects[0];
        assert_eq!(d.kind, PlanDefectKind::UnmetPrecondition);
        assert_eq!(d.step.as_deref(), Some("serve"));
        assert_eq!(d.fact, "cooked");
    }

    #[test]
    fn deleted_fact_breaks_a_later_step() {
        // step1 consumes 'key' (deletes it); step2 still needs 'key'.
        let r = check_plan(&req(
            &["key"],
            vec![
                step("open", &["key"], &["opened"], &["key"]),
                step("relock", &["key"], &["locked"], &[]),
            ],
            &[],
        ));
        assert!(!r.valid);
        assert!(r
            .defects
            .iter()
            .any(|d| d.step.as_deref() == Some("relock") && d.fact == "key"));
    }

    #[test]
    fn goal_not_achieved_is_flagged() {
        let r = check_plan(&req(&["a"], vec![step("noop", &["a"], &[], &[])], &["b"]));
        assert!(!r.valid);
        assert_eq!(r.defects[0].kind, PlanDefectKind::GoalNotAchieved);
        assert_eq!(r.defects[0].fact, "b");
    }

    #[test]
    fn add_and_delete_same_fact_nets_to_true() {
        // A step that both deletes and adds 'x' leaves 'x' true (add after del).
        let r = check_plan(&req(&[], vec![step("refresh", &[], &["x"], &["x"])], &["x"]));
        assert!(r.valid, "{:?}", r.defects);
    }

    #[test]
    fn all_defects_surfaced_in_one_pass() {
        // Two unmet preconditions + an unreached goal — all reported.
        let r = check_plan(&req(
            &[],
            vec![step("s1", &["p1"], &[], &[]), step("s2", &["p2"], &[], &[])],
            &["g"],
        ));
        assert_eq!(r.defects.len(), 3);
    }

    #[test]
    fn empty_plan_with_satisfied_goal_is_valid() {
        let r = check_plan(&req(&["done"], vec![], &["done"]));
        assert!(r.valid);
    }
}