car-verify 0.52.1

//! Static workflow-graph verification — structural checks + witnesses
//! (arXiv 2603.20356, *Agentproof: Static Verification of Agent Workflow
//! Graphs*).
//!
//! See `docs/proposals/workflow-graph-verification.md`. Agent workflows are
//! graphs; a schema-valid workflow can still have topology defects — a dead-end
//! stage, an unreachable exit, a trap loop — that only surface at runtime when
//! the bad path is exercised. This module catches them statically and hands back
//! a **witness** (the entry→subject path) for each, so a repair loop gets an
//! actionable counter-example, not just a boolean.
//!
//! It's the workflow-topology member of CAR's verify family — pure and
//! deterministic, alongside [`crate::transaction`], [`crate::infoflow`], and
//! [`crate::concurrency`]. The model is an abstract graph (the paper's "unified
//! abstract graph"), so it's framework-agnostic; `car-workflow` can feed its real
//! stage graph into this model in a later slice.

use serde::{Deserialize, Serialize};
use std::collections::{HashMap, HashSet, VecDeque};

/// A directed edge between two stages, optionally guarded by a condition label.
#[derive(Debug, Clone, Default, Serialize, Deserialize)]
pub struct WorkflowEdge {
    pub from: String,
    pub to: String,
    #[serde(default)]
    pub condition: Option<String>,
}

/// An abstract workflow graph: an entry stage, the terminal (exit) stages, all
/// stage ids, and the directed edges between them.
#[derive(Debug, Clone, Default, Serialize, Deserialize)]
pub struct WorkflowGraph {
    pub entry: String,
    #[serde(default)]
    pub terminals: Vec<String>,
    #[serde(default)]
    pub stages: Vec<String>,
    #[serde(default)]
    pub edges: Vec<WorkflowEdge>,
}

/// The class of a structural defect.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
#[serde(rename_all = "snake_case")]
pub enum WorkflowDefectKind {
    /// The entry is empty or not a declared stage.
    MissingEntry,
    /// An edge references a stage id absent from `stages`.
    DanglingEdge,
    /// A stage is not reachable from the entry.
    UnreachableStage,
    /// A non-terminal stage has no outgoing edge — execution stalls there.
    DeadEnd,
    /// A reachable stage from which no terminal is reachable — a trap or a loop
    /// with no exit.
    NoExitReachable,
    /// A declared terminal is not reachable from the entry.
    UnreachableTerminal,
}

/// A single detected defect, with a witness path and an explanation.
#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
pub struct WorkflowDefect {
    pub kind: WorkflowDefectKind,
    /// The stage id (or `"from->to"` for a dangling edge) the defect is about.
    pub subject: String,
    /// A demonstrating path from the entry to the subject, when one exists.
    pub witness: Vec<String>,
    pub explanation: String,
}

/// The verification report. `sound` is true when none of the checks below
/// found a defect — it reports the absence of detected defects, not a
/// soundness proof. See the crate README for what these checks do and don't
/// cover.
#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
pub struct WorkflowVerifyReport {
    pub sound: bool,
    pub defects: Vec<WorkflowDefect>,
}

impl WorkflowVerifyReport {
    /// What kind of check produced these defects — see
    /// [`crate::EvidenceTier`].
    ///
    /// The topology checks are reachability over a finite graph, computed by
    /// BFS: entry-reaches-stage, stage-reaches-terminal, edge-endpoint-exists.
    /// Each is decided for the graph it was handed, and every defect ships a
    /// witness path you can walk yourself.
    ///
    /// Note what the tier does *not* upgrade: `sound` still means "no defect
    /// of the six kinds this module looks for was found", exactly as the field
    /// docs say. A decision procedure for one property is not a verdict on
    /// every property.
    pub const fn evidence_tier(&self) -> crate::EvidenceTier {
        crate::EvidenceTier::DecisionProcedure
    }
}

/// BFS from `start` over `adj`, returning the set of reachable nodes and a
/// parent map for witness-path reconstruction.
fn bfs(start: &str, adj: &HashMap<&str, Vec<&str>>) -> (HashSet<String>, HashMap<String, String>) {
    let mut seen = HashSet::new();
    let mut parent: HashMap<String, String> = HashMap::new();
    let mut q = VecDeque::new();
    seen.insert(start.to_string());
    q.push_back(start.to_string());
    while let Some(n) = q.pop_front() {
        if let Some(succs) = adj.get(n.as_str()) {
            for &s in succs {
                if seen.insert(s.to_string()) {
                    parent.insert(s.to_string(), n.clone());
                    q.push_back(s.to_string());
                }
            }
        }
    }
    (seen, parent)
}

/// Reconstruct the entry→`target` path from a BFS parent map.
fn witness_path(entry: &str, target: &str, parent: &HashMap<String, String>) -> Vec<String> {
    let mut path = vec![target.to_string()];
    let mut cur = target.to_string();
    while cur != entry {
        match parent.get(&cur) {
            Some(p) => {
                path.push(p.clone());
                cur = p.clone();
            }
            None => break,
        }
    }
    path.reverse();
    path
}

/// Statically verify a workflow graph for the six structural defect classes,
/// each with a witness path. Deterministic and pure.
pub fn verify_workflow_graph(g: &WorkflowGraph) -> WorkflowVerifyReport {
    let mut defects = Vec::new();
    let stage_set: HashSet<&str> = g.stages.iter().map(|s| s.as_str()).collect();

    // --- MissingEntry ---
    if g.entry.is_empty() || !stage_set.contains(g.entry.as_str()) {
        defects.push(WorkflowDefect {
            kind: WorkflowDefectKind::MissingEntry,
            subject: g.entry.clone(),
            witness: vec![],
            explanation: if g.entry.is_empty() {
                "workflow has no entry stage".to_string()
            } else {
                format!("entry stage '{}' is not a declared stage", g.entry)
            },
        });
        // Without a valid entry, reachability checks are meaningless.
        return WorkflowVerifyReport {
            sound: false,
            defects,
        };
    }

    // --- DanglingEdge --- (and build adjacency over valid edges only)
    let mut adj: HashMap<&str, Vec<&str>> = HashMap::new();
    for e in &g.edges {
        let from_ok = stage_set.contains(e.from.as_str());
        let to_ok = stage_set.contains(e.to.as_str());
        if !from_ok || !to_ok {
            defects.push(WorkflowDefect {
                kind: WorkflowDefectKind::DanglingEdge,
                subject: format!("{}->{}", e.from, e.to),
                witness: vec![],
                explanation: format!(
                    "edge '{}'->'{}' references {} stage",
                    e.from,
                    e.to,
                    if !from_ok && !to_ok {
                        "two undeclared"
                    } else {
                        "an undeclared"
                    }
                ),
            });
            continue;
        }
        adj.entry(e.from.as_str()).or_default().push(e.to.as_str());
    }

    // Forward reachability from entry.
    let (reachable, parent) = bfs(&g.entry, &adj);
    let terminal_set: HashSet<&str> = g.terminals.iter().map(|s| s.as_str()).collect();

    // --- UnreachableStage ---
    for s in &g.stages {
        if !reachable.contains(s) {
            defects.push(WorkflowDefect {
                kind: WorkflowDefectKind::UnreachableStage,
                subject: s.clone(),
                witness: vec![],
                explanation: format!("stage '{s}' is not reachable from entry '{}'", g.entry),
            });
        }
    }

    // --- UnreachableTerminal ---
    for t in &g.terminals {
        if stage_set.contains(t.as_str()) && !reachable.contains(t) {
            defects.push(WorkflowDefect {
                kind: WorkflowDefectKind::UnreachableTerminal,
                subject: t.clone(),
                witness: vec![],
                explanation: format!("terminal '{t}' is not reachable from entry '{}'", g.entry),
            });
        }
    }

    // Reverse adjacency for "can reach a terminal?" analysis.
    let mut radj: HashMap<&str, Vec<&str>> = HashMap::new();
    for e in &g.edges {
        if stage_set.contains(e.from.as_str()) && stage_set.contains(e.to.as_str()) {
            radj.entry(e.to.as_str()).or_default().push(e.from.as_str());
        }
    }
    // Multi-source reverse BFS from all terminals → set of stages that can reach
    // some terminal.
    let mut can_exit: HashSet<String> = HashSet::new();
    let mut q = VecDeque::new();
    for t in &g.terminals {
        if stage_set.contains(t.as_str()) && can_exit.insert(t.clone()) {
            q.push_back(t.clone());
        }
    }
    while let Some(n) = q.pop_front() {
        if let Some(preds) = radj.get(n.as_str()) {
            for &p in preds {
                if can_exit.insert(p.to_string()) {
                    q.push_back(p.to_string());
                }
            }
        }
    }

    // --- DeadEnd and NoExitReachable --- over reachable, non-terminal stages.
    for s in &g.stages {
        if !reachable.contains(s) || terminal_set.contains(s.as_str()) {
            continue;
        }
        let has_out = adj.get(s.as_str()).map(|v| !v.is_empty()).unwrap_or(false);
        if !has_out {
            defects.push(WorkflowDefect {
                kind: WorkflowDefectKind::DeadEnd,
                subject: s.clone(),
                witness: witness_path(&g.entry, s, &parent),
                explanation: format!(
                    "stage '{s}' is non-terminal but has no outgoing edge — execution stalls"
                ),
            });
        } else if !can_exit.contains(s) {
            // Has successors, but none of them can reach a terminal — a trap/loop.
            defects.push(WorkflowDefect {
                kind: WorkflowDefectKind::NoExitReachable,
                subject: s.clone(),
                witness: witness_path(&g.entry, s, &parent),
                explanation: format!(
                    "no terminal is reachable from stage '{s}' — it is a trap or an exitless loop"
                ),
            });
        }
    }

    // A graph with no terminals at all can never exit.
    if g.terminals.is_empty() {
        defects.push(WorkflowDefect {
            kind: WorkflowDefectKind::NoExitReachable,
            subject: g.entry.clone(),
            witness: vec![g.entry.clone()],
            explanation: "workflow declares no terminal stages — it can never exit".to_string(),
        });
    }

    WorkflowVerifyReport {
        sound: defects.is_empty(),
        defects,
    }
}

// === Slice 2: temporal safety policies ===
//
// The paper's policy layer: evaluate temporal safety policies over the graph.
// Agentproof compiles a DSL to a DFA and checks it by a graph × DFA product;
// the headline policy (and its 55%-violation finding) is the **human-gate**:
// a guard stage must occur before a sensitive stage on *every* path. This slice
// implements that precedence policy soundly — specialized to the precedence
// automaton, the product reduces to a reachability query — with a witness path
// that demonstrates the violation.

/// A temporal safety policy over stages.
#[derive(Debug, Clone, Serialize, Deserialize)]
#[serde(tag = "kind", rename_all = "snake_case")]
pub enum TemporalPolicy {
    /// `earlier` must be visited before `later` on every path that reaches
    /// `later` (e.g. a `human_gate` stage must precede an `irreversible` stage).
    Precedes {
        earlier: String,
        later: String,
        #[serde(default)]
        name: Option<String>,
    },
}

/// A policy violation, with a witness path that reaches the guarded stage
/// without first visiting the required stage.
#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
pub struct PolicyViolation {
    /// Policy name (or a derived label).
    pub policy: String,
    /// The guarded stage reached without the required predecessor.
    pub stage: String,
    /// An entry→stage path that skips the required stage.
    pub witness: Vec<String>,
    pub explanation: String,
}

/// The result of checking temporal policies.
#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
pub struct PolicyReport {
    pub compliant: bool,
    pub violations: Vec<PolicyViolation>,
}

impl PolicyReport {
    /// What kind of check produced these violations — see
    /// [`crate::EvidenceTier`].
    ///
    /// `Precedes` is checked by deleting the required stage and asking whether
    /// the guarded stage is still reachable from the entry. That is an
    /// if-and-only-if over the given graph — a path exists or it does not —
    /// and the witness is the path itself.
    ///
    /// Scope, unchanged by this: the check is over the *declared stage graph*,
    /// so it says nothing about whether a run took an edge the graph doesn't
    /// model. Ordering constraints over an actual execution trace are
    /// [`crate::trace_policy`]'s job.
    pub const fn evidence_tier(&self) -> crate::EvidenceTier {
        crate::EvidenceTier::DecisionProcedure
    }
}

/// Check temporal safety policies over a workflow graph. For each `Precedes`
/// policy, a violation exists iff some path from the entry reaches `later`
/// without visiting `earlier` — found by BFS over the graph with `earlier`
/// deleted (the precedence automaton's reject state). Deterministic and pure.
pub fn check_temporal_policies(g: &WorkflowGraph, policies: &[TemporalPolicy]) -> PolicyReport {
    let stage_set: HashSet<&str> = g.stages.iter().map(|s| s.as_str()).collect();
    let mut violations = Vec::new();

    for p in policies {
        match p {
            TemporalPolicy::Precedes {
                earlier,
                later,
                name,
            } => {
                let label = name
                    .clone()
                    .unwrap_or_else(|| format!("{earlier} precedes {later}"));

                // Reaching `later` without ever passing `earlier`: build
                // adjacency that excludes `earlier` (so any path through it is
                // pruned), then BFS from entry. If entry *is* `earlier`, the
                // policy is trivially satisfied (every path starts past it).
                if &g.entry == earlier {
                    continue;
                }
                let mut adj: HashMap<&str, Vec<&str>> = HashMap::new();
                for e in &g.edges {
                    if e.from == *earlier || e.to == *earlier {
                        continue; // delete the gate node from the graph
                    }
                    if stage_set.contains(e.from.as_str()) && stage_set.contains(e.to.as_str()) {
                        adj.entry(e.from.as_str()).or_default().push(e.to.as_str());
                    }
                }
                // If entry was deleted as the gate we'd have `continue`d above.
                let (reached, parent) = bfs(&g.entry, &adj);
                if reached.contains(later) {
                    violations.push(PolicyViolation {
                        policy: label,
                        stage: later.clone(),
                        witness: witness_path(&g.entry, later, &parent),
                        explanation: format!(
                            "stage '{later}' is reachable without first visiting required stage \
                             '{earlier}' — the precedence policy can be violated"
                        ),
                    });
                }
            }
        }
    }

    PolicyReport {
        compliant: violations.is_empty(),
        violations,
    }
}

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

    fn edge(from: &str, to: &str) -> WorkflowEdge {
        WorkflowEdge {
            from: from.into(),
            to: to.into(),
            condition: None,
        }
    }

    fn graph(
        entry: &str,
        terminals: &[&str],
        stages: &[&str],
        edges: &[(&str, &str)],
    ) -> WorkflowGraph {
        WorkflowGraph {
            entry: entry.into(),
            terminals: terminals.iter().map(|s| s.to_string()).collect(),
            stages: stages.iter().map(|s| s.to_string()).collect(),
            edges: edges.iter().map(|(f, t)| edge(f, t)).collect(),
        }
    }

    #[test]
    fn linear_workflow_is_sound() {
        let g = graph(
            "start",
            &["done"],
            &["start", "work", "done"],
            &[("start", "work"), ("work", "done")],
        );
        let r = verify_workflow_graph(&g);
        assert!(r.sound, "{:?}", r.defects);
    }

    #[test]
    fn missing_entry_is_flagged_and_short_circuits() {
        let g = graph("ghost", &["done"], &["start", "done"], &[("start", "done")]);
        let r = verify_workflow_graph(&g);
        assert!(!r.sound);
        assert_eq!(r.defects.len(), 1);
        assert_eq!(r.defects[0].kind, WorkflowDefectKind::MissingEntry);
    }

    #[test]
    fn dangling_edge_is_flagged() {
        let g = graph(
            "start",
            &["done"],
            &["start", "done"],
            &[("start", "nowhere"), ("start", "done")],
        );
        let r = verify_workflow_graph(&g);
        assert!(r
            .defects
            .iter()
            .any(|d| d.kind == WorkflowDefectKind::DanglingEdge && d.subject == "start->nowhere"));
    }

    #[test]
    fn unreachable_stage_is_flagged() {
        let g = graph(
            "start",
            &["done"],
            &["start", "orphan", "done"],
            &[("start", "done"), ("orphan", "done")],
        );
        let r = verify_workflow_graph(&g);
        assert!(r
            .defects
            .iter()
            .any(|d| d.kind == WorkflowDefectKind::UnreachableStage && d.subject == "orphan"));
    }

    #[test]
    fn dead_end_has_witness_path() {
        // start -> trap (non-terminal, no outgoing); start -> done.
        let g = graph(
            "start",
            &["done"],
            &["start", "trap", "done"],
            &[("start", "trap"), ("start", "done")],
        );
        let r = verify_workflow_graph(&g);
        let d = r
            .defects
            .iter()
            .find(|d| d.kind == WorkflowDefectKind::DeadEnd)
            .expect("dead end");
        assert_eq!(d.subject, "trap");
        assert_eq!(d.witness, vec!["start".to_string(), "trap".to_string()]);
    }

    #[test]
    fn exitless_loop_is_no_exit_reachable() {
        // start -> a -> b -> a (loop), never reaches done.
        let g = graph(
            "start",
            &["done"],
            &["start", "a", "b", "done"],
            &[("start", "a"), ("a", "b"), ("b", "a")],
        );
        let r = verify_workflow_graph(&g);
        assert!(r
            .defects
            .iter()
            .any(|d| d.kind == WorkflowDefectKind::NoExitReachable));
        // 'done' is also unreachable here.
        assert!(r
            .defects
            .iter()
            .any(|d| d.kind == WorkflowDefectKind::UnreachableTerminal && d.subject == "done"));
    }

    #[test]
    fn no_terminals_can_never_exit() {
        let g = graph(
            "start",
            &[],
            &["start", "work"],
            &[("start", "work"), ("work", "start")],
        );
        let r = verify_workflow_graph(&g);
        assert!(r
            .defects
            .iter()
            .any(|d| d.kind == WorkflowDefectKind::NoExitReachable));
    }

    #[test]
    fn conditional_branches_both_reaching_exit_are_sound() {
        let g = graph(
            "start",
            &["done"],
            &["start", "yes", "no", "done"],
            &[
                ("start", "yes"),
                ("start", "no"),
                ("yes", "done"),
                ("no", "done"),
            ],
        );
        let r = verify_workflow_graph(&g);
        assert!(r.sound, "{:?}", r.defects);
    }

    // --- Slice 2: temporal policies ---

    fn precedes(earlier: &str, later: &str) -> TemporalPolicy {
        TemporalPolicy::Precedes {
            earlier: earlier.into(),
            later: later.into(),
            name: None,
        }
    }

    #[test]
    fn gate_on_every_path_is_compliant() {
        // start -> gate -> act -> done. The gate is unavoidable before `act`.
        let g = graph(
            "start",
            &["done"],
            &["start", "gate", "act", "done"],
            &[("start", "gate"), ("gate", "act"), ("act", "done")],
        );
        let r = check_temporal_policies(&g, &[precedes("gate", "act")]);
        assert!(r.compliant, "{:?}", r.violations);
    }

    #[test]
    fn bypass_path_violates_with_witness() {
        // start -> act bypasses the gate; start -> gate -> act is the safe path.
        let g = graph(
            "start",
            &["done"],
            &["start", "gate", "act", "done"],
            &[
                ("start", "gate"),
                ("gate", "act"),
                ("start", "act"), // the bypass
                ("act", "done"),
            ],
        );
        let r = check_temporal_policies(&g, &[precedes("gate", "act")]);
        assert!(!r.compliant);
        let v = &r.violations[0];
        assert_eq!(v.stage, "act");
        // witness reaches `act` without `gate`.
        assert!(!v.witness.contains(&"gate".to_string()));
        assert_eq!(v.witness, vec!["start".to_string(), "act".to_string()]);
    }

    #[test]
    fn entry_as_gate_is_trivially_satisfied() {
        let g = graph(
            "gate",
            &["done"],
            &["gate", "act", "done"],
            &[("gate", "act"), ("act", "done")],
        );
        let r = check_temporal_policies(&g, &[precedes("gate", "act")]);
        assert!(r.compliant);
    }
}