logicaffeine_verify/
compositional.rs

1//! Assume-Guarantee Compositional Reasoning
2//!
3//! Decompose verification into per-component proofs with interface contracts.
4//! Each component has assumptions (what it requires from environment) and
5//! guarantees (what it provides). Verify each component independently.
6
7use crate::ir::VerifyExpr;
8use crate::equivalence::Trace;
9use crate::kinduction;
10use std::collections::HashMap;
11
12/// A component specification for compositional verification.
13#[derive(Debug, Clone)]
14pub struct ComponentSpec {
15    pub name: String,
16    pub assumes: Vec<VerifyExpr>,
17    pub guarantees: Vec<VerifyExpr>,
18    pub init: VerifyExpr,
19    pub transition: VerifyExpr,
20}
21
22/// Result of compositional verification.
23#[derive(Debug)]
24pub enum CompositionalResult {
25    /// All components verified.
26    AllVerified,
27    /// A component failed verification.
28    ComponentFailed { name: String, trace: Trace },
29    /// Circular dependency detected.
30    CircularDependency { components: Vec<String> },
31    /// Could not determine.
32    Unknown,
33}
34
35/// Verify a set of components compositionally.
36///
37/// For each component:
38/// 1. Assume all assumptions hold
39/// 2. Verify all guarantees under those assumptions
40/// 3. Check that each component's guarantees discharge other components' assumptions
41pub fn verify_compositional(components: &[ComponentSpec]) -> CompositionalResult {
42    if components.is_empty() {
43        return CompositionalResult::AllVerified;
44    }
45
46
47    // Phase 1: Verify each component in isolation (assumptions → guarantees)
48    for comp in components {
49        for guarantee in &comp.guarantees {
50            // Check: init AND assumptions AND transition → guarantee
51            let assumptions = if comp.assumes.is_empty() {
52                VerifyExpr::bool(true)
53            } else {
54                comp.assumes.iter().cloned().reduce(|a, b| VerifyExpr::and(a, b)).unwrap()
55            };
56
57            // Use k-induction to verify: under assumptions, guarantee holds
58            let strengthened_init = VerifyExpr::and(comp.init.clone(), assumptions.clone());
59            let strengthened_transition = VerifyExpr::and(comp.transition.clone(), assumptions.clone());
60
61            let result = kinduction::k_induction(
62                &strengthened_init,
63                &strengthened_transition,
64                guarantee,
65                &[],
66                10,
67            );
68
69            match result {
70                kinduction::KInductionResult::Counterexample { trace, .. } => {
71                    return CompositionalResult::ComponentFailed {
72                        name: comp.name.clone(),
73                        trace,
74                    };
75                }
76                kinduction::KInductionResult::Proven { .. } => {
77                    // This guarantee verified
78                }
79                _ => {
80                    // Inconclusive — try IC3 as fallback
81                    let ic3_result = crate::ic3::ic3(
82                        &strengthened_init,
83                        &strengthened_transition,
84                        guarantee,
85                        10,
86                    );
87                    match ic3_result {
88                        crate::ic3::Ic3Result::Safe { .. } => {}
89                        crate::ic3::Ic3Result::Unsafe { trace } => {
90                            return CompositionalResult::ComponentFailed {
91                                name: comp.name.clone(),
92                                trace,
93                            };
94                        }
95                        _ => return CompositionalResult::Unknown,
96                    }
97                }
98            }
99        }
100    }
101
102    // Phase 2: Check that guarantees discharge assumptions
103    // For each component A's assumption, check that some component B's guarantee covers it
104    // (simplified: check that the conjunction of all guarantees implies each assumption)
105    let all_guarantees: Vec<VerifyExpr> = components.iter()
106        .flat_map(|c| c.guarantees.clone())
107        .collect();
108
109    if !all_guarantees.is_empty() {
110        let guarantees_conj = all_guarantees.iter().cloned()
111            .reduce(|a, b| VerifyExpr::and(a, b)).unwrap();
112
113        for comp in components {
114            for assumption in &comp.assumes {
115                // Check: guarantees_conj → assumption
116                let check = VerifyExpr::implies(guarantees_conj.clone(), assumption.clone());
117                let solver = crate::solver::new_solver();
118                let not_check = VerifyExpr::not(check);
119                let encoded = encode_bool(&not_check);
120                solver.assert(&encoded);
121                match solver.check() {
122                    z3::SatResult::Sat => {
123                        // Guarantee doesn't cover assumption — could be circular
124                        // For now, report as circular dependency
125                        return CompositionalResult::CircularDependency {
126                            components: vec![comp.name.clone()],
127                        };
128                    }
129                    z3::SatResult::Unsat => {} // Good: guarantees discharge assumption
130                    z3::SatResult::Unknown => return CompositionalResult::Unknown,
131                }
132            }
133        }
134    }
135
136    CompositionalResult::AllVerified
137}
138
139fn encode_bool(expr: &VerifyExpr) -> z3::ast::Bool {
140    let mut bool_vars = HashMap::new();
141    let mut int_vars = HashMap::new();
142    let mut all_vars = std::collections::HashSet::new();
143    crate::equivalence::collect_vars_pub(expr, &mut all_vars);
144    for name in &all_vars {
145        bool_vars.insert(name.clone(), z3::ast::Bool::new_const(name.as_str()));
146    }
147    crate::equivalence::collect_int_vars_pub(expr, &mut int_vars);
148    kinduction::encode_expr_bool(expr, &bool_vars, &int_vars)
149}
logicaffeine_verify/compositional.rs

logicaffeine_verify/
compositional.rs
