logicaffeine_verify/
kinduction.rs

1//! k-Induction for Unbounded Safety Verification
2//!
3//! BMC proves a property holds for k cycles. k-Induction proves it holds forever.
4//!
5//! Algorithm:
6//! 1. For k = 1, 2, ..., max_k:
7//!    a. **Base case:** init AND T^k AND NOT(P) at each step. If UNSAT → base passes.
8//!    b. **Inductive step:** P holds for k consecutive steps AND T AND NOT(P) at step k+1.
9//!       If UNSAT → proven.
10//! 2. If base fails → Counterexample. If induction fails for all k → InductionFailed.
11
12use crate::ir::{VerifyExpr, VerifyOp};
13use crate::equivalence::Trace;
14use std::collections::HashMap;
15use z3::{ast::Ast, ast::Bool, ast::Dynamic, ast::Int, SatResult, Solver};
16
17/// Result of k-induction verification.
18#[derive(Debug)]
19pub enum KInductionResult {
20    /// Property holds for all time, proven at depth k.
21    Proven { k: u32 },
22    /// Base case violation at step k — property fails.
23    Counterexample { k: u32, trace: Trace },
24    /// Inductive step failed for all k up to max — may need larger k or strengthening.
25    InductionFailed { k: u32, trace: Trace },
26    /// Solver returned unknown (timeout or undecidable).
27    Unknown,
28}
29
30/// Signal declaration for k-induction.
31#[derive(Debug, Clone)]
32pub struct SignalDecl {
33    pub name: String,
34    pub width: Option<u32>,
35}
36
37/// Run k-induction on a safety property.
38///
39/// - `init`: Initial state predicate (using variables with @0 suffix)
40/// - `transition`: Transition relation (using @t and @(t+1) variables)
41/// - `property`: Safety property to verify (using @t variables)
42/// - `signals`: Signal declarations
43/// - `max_k`: Maximum induction depth
44pub fn k_induction(
45    init: &VerifyExpr,
46    transition: &VerifyExpr,
47    property: &VerifyExpr,
48    signals: &[SignalDecl],
49    max_k: u32,
50) -> KInductionResult {
51
52    for k in 1..=max_k {
53        // ---- Base case ----
54        // Check: init(0) AND T(0,1) AND T(1,2) AND ... AND T(k-2,k-1) AND NOT P(i) for some i
55        let base_result = check_base_case(init, transition, property, signals, k);
56        match base_result {
57            SatResult::Sat => {
58                // Base case failed — property violated within k steps
59                return KInductionResult::Counterexample {
60                    k,
61                    trace: Trace { cycles: vec![] },
62                };
63            }
64            SatResult::Unknown => return KInductionResult::Unknown,
65            SatResult::Unsat => {} // base passes, continue to inductive step
66        }
67
68        // ---- Inductive step ----
69        // Check: P(0) AND P(1) AND ... AND P(k-1) AND T(0,1) AND ... AND T(k-1,k) AND NOT P(k)
70        let step_result = check_inductive_step(transition, property, signals, k);
71        match step_result {
72            SatResult::Unsat => {
73                // Inductive step holds — property proven for all time!
74                return KInductionResult::Proven { k };
75            }
76            SatResult::Unknown => return KInductionResult::Unknown,
77            SatResult::Sat => {} // induction failed at this k, try larger k
78        }
79    }
80
81    // Exhausted max_k without proving or disproving
82    KInductionResult::InductionFailed {
83        k: max_k,
84        trace: Trace { cycles: vec![] },
85    }
86}
87
88/// Check the base case: init AND transitions AND NOT(property) at some step.
89fn check_base_case(
90    init: &VerifyExpr,
91    transition: &VerifyExpr,
92    property: &VerifyExpr,
93    _signals: &[SignalDecl],
94    k: u32,
95) -> SatResult {
96    let solver = Solver::new();
97
98    // Assert init at step 0
99    let init_0 = instantiate_at(init, 0);
100    let init_z3 = encode_to_bool(&init_0);
101    solver.assert(&init_z3);
102
103    // Assert transitions T(0,1), T(1,2), ..., T(k-2, k-1)
104    for t in 0..k.saturating_sub(1) {
105        let trans = instantiate_transition(transition, t);
106        let trans_z3 = encode_to_bool(&trans);
107        solver.assert(&trans_z3);
108    }
109
110    // Assert NOT P(i) for at least one step (disjunction)
111    // NOT(P(0)) OR NOT(P(1)) OR ... OR NOT(P(k-1))
112    let mut not_props: Vec<Bool> = Vec::new();
113    for t in 0..k {
114        let prop_t = instantiate_at(property, t);
115        let prop_z3 = encode_to_bool(&prop_t);
116        not_props.push(prop_z3.not());
117    }
118    let not_prop_refs: Vec<&Bool> = not_props.iter().collect();
119    let some_violation = Bool::or(&not_prop_refs);
120    solver.assert(&some_violation);
121
122    solver.check()
123}
124
125/// Check the inductive step: P holds for k steps, transition, NOT P at step k.
126fn check_inductive_step(
127    transition: &VerifyExpr,
128    property: &VerifyExpr,
129    _signals: &[SignalDecl],
130    k: u32,
131) -> SatResult {
132    let solver = Solver::new();
133
134    // Assert P(0), P(1), ..., P(k-1)
135    for t in 0..k {
136        let prop_t = instantiate_at(property, t);
137        let prop_z3 = encode_to_bool(&prop_t);
138        solver.assert(&prop_z3);
139    }
140
141    // Assert transitions T(0,1), T(1,2), ..., T(k-1, k)
142    for t in 0..k {
143        let trans = instantiate_transition(transition, t);
144        let trans_z3 = encode_to_bool(&trans);
145        solver.assert(&trans_z3);
146    }
147
148    // Assert NOT P(k)
149    let prop_k = instantiate_at(property, k);
150    let prop_k_z3 = encode_to_bool(&prop_k);
151    solver.assert(&prop_k_z3.not());
152
153    solver.check()
154}
155
156/// Instantiate an expression at a specific timestep by replacing @t with @{step}.
157pub fn instantiate_at(expr: &VerifyExpr, step: u32) -> VerifyExpr {
158    rename_timestep(expr, "t", step)
159}
160
161/// Instantiate a transition relation: replace @t with @{step} and @t' with @{step+1}.
162pub fn instantiate_transition(expr: &VerifyExpr, step: u32) -> VerifyExpr {
163    let e1 = rename_timestep(expr, "t", step);
164    rename_timestep(&e1, "t1", step + 1)
165}
166
167/// Replace @{old_suffix} with @{new_step} in all variable names.
168fn rename_timestep(expr: &VerifyExpr, suffix: &str, step: u32) -> VerifyExpr {
169    match expr {
170        VerifyExpr::Var(name) => {
171            let target = format!("@{}", suffix);
172            if name.ends_with(&target) {
173                let base = &name[..name.len() - target.len()];
174                VerifyExpr::Var(format!("{}@{}", base, step))
175            } else {
176                VerifyExpr::Var(name.clone())
177            }
178        }
179        VerifyExpr::Binary { op, left, right } => VerifyExpr::binary(
180            *op,
181            rename_timestep(left, suffix, step),
182            rename_timestep(right, suffix, step),
183        ),
184        VerifyExpr::Not(inner) => VerifyExpr::not(rename_timestep(inner, suffix, step)),
185        VerifyExpr::Bool(b) => VerifyExpr::Bool(*b),
186        VerifyExpr::Int(n) => VerifyExpr::Int(*n),
187        VerifyExpr::Iff(l, r) => VerifyExpr::iff(
188            rename_timestep(l, suffix, step),
189            rename_timestep(r, suffix, step),
190        ),
191        VerifyExpr::ForAll { vars, body } => VerifyExpr::forall(
192            vars.clone(),
193            rename_timestep(body, suffix, step),
194        ),
195        VerifyExpr::Exists { vars, body } => VerifyExpr::exists(
196            vars.clone(),
197            rename_timestep(body, suffix, step),
198        ),
199        VerifyExpr::ApplyInt { name, args } => VerifyExpr::apply_int(
200            name.clone(),
201            args.iter().map(|a| rename_timestep(a, suffix, step)).collect(),
202        ),
203        VerifyExpr::Apply { name, args } => VerifyExpr::apply(
204            name.clone(),
205            args.iter().map(|a| rename_timestep(a, suffix, step)).collect(),
206        ),
207        VerifyExpr::BitVecConst { width, value } => VerifyExpr::bv_const(*width, *value),
208        VerifyExpr::BitVecBinary { op, left, right } => VerifyExpr::bv_binary(
209            *op,
210            rename_timestep(left, suffix, step),
211            rename_timestep(right, suffix, step),
212        ),
213        VerifyExpr::BitVecExtract { high, low, operand } => VerifyExpr::BitVecExtract {
214            high: *high,
215            low: *low,
216            operand: Box::new(rename_timestep(operand, suffix, step)),
217        },
218        VerifyExpr::BitVecConcat(l, r) => VerifyExpr::BitVecConcat(
219            Box::new(rename_timestep(l, suffix, step)),
220            Box::new(rename_timestep(r, suffix, step)),
221        ),
222        VerifyExpr::Select { array, index } => VerifyExpr::Select {
223            array: Box::new(rename_timestep(array, suffix, step)),
224            index: Box::new(rename_timestep(index, suffix, step)),
225        },
226        VerifyExpr::Store { array, index, value } => VerifyExpr::Store {
227            array: Box::new(rename_timestep(array, suffix, step)),
228            index: Box::new(rename_timestep(index, suffix, step)),
229            value: Box::new(rename_timestep(value, suffix, step)),
230        },
231        VerifyExpr::AtState { state, expr } => VerifyExpr::AtState {
232            state: Box::new(rename_timestep(state, suffix, step)),
233            expr: Box::new(rename_timestep(expr, suffix, step)),
234        },
235        VerifyExpr::Transition { from, to } => VerifyExpr::Transition {
236            from: Box::new(rename_timestep(from, suffix, step)),
237            to: Box::new(rename_timestep(to, suffix, step)),
238        },
239    }
240}
241
242/// Encode a VerifyExpr to a Z3 Bool using check_equivalence infrastructure.
243/// We encode by creating: expr <-> true, then if equiv, the expr is always true.
244/// For direct encoding, we use the internal equivalence encoder.
245fn encode_to_bool(expr: &VerifyExpr) -> Bool {
246    // Build variable maps
247    let mut all_vars = std::collections::HashSet::new();
248    crate::equivalence::collect_vars_pub(expr, &mut all_vars);
249
250    let mut bool_vars: HashMap<String, Bool> = HashMap::new();
251    let mut int_vars: HashMap<String, Int> = HashMap::new();
252
253    for name in &all_vars {
254        bool_vars.insert(name.clone(), Bool::new_const(name.as_str()));
255    }
256    crate::equivalence::collect_int_vars_pub(expr, &mut int_vars);
257
258    // Use a simple recursive encoder
259    encode_expr_bool(expr, &bool_vars, &int_vars)
260}
261
262/// Simple recursive Bool encoder for k-induction formulas.
263pub fn encode_expr_bool(
264    expr: &VerifyExpr,
265    bool_vars: &HashMap<String, Bool>,
266    int_vars: &HashMap<String, Int>,
267) -> Bool {
268    match expr {
269        VerifyExpr::Bool(b) => Bool::from_bool(*b),
270        VerifyExpr::Var(name) => {
271            if let Some(bv) = bool_vars.get(name) {
272                bv.clone()
273            } else {
274                Bool::new_const(name.as_str())
275            }
276        }
277        VerifyExpr::Not(inner) => encode_expr_bool(inner, bool_vars, int_vars).not(),
278        VerifyExpr::Binary { op, left, right } => {
279            match op {
280                VerifyOp::And => {
281                    let l = encode_expr_bool(left, bool_vars, int_vars);
282                    let r = encode_expr_bool(right, bool_vars, int_vars);
283                    Bool::and(&[&l, &r])
284                }
285                VerifyOp::Or => {
286                    let l = encode_expr_bool(left, bool_vars, int_vars);
287                    let r = encode_expr_bool(right, bool_vars, int_vars);
288                    Bool::or(&[&l, &r])
289                }
290                VerifyOp::Implies => {
291                    let l = encode_expr_bool(left, bool_vars, int_vars);
292                    let r = encode_expr_bool(right, bool_vars, int_vars);
293                    l.implies(&r)
294                }
295                VerifyOp::Eq => {
296                    // Could be Bool or Int equality
297                    let li = encode_expr_int(left, int_vars);
298                    let ri = encode_expr_int(right, int_vars);
299                    if let (Some(l), Some(r)) = (li, ri) {
300                        l.eq(&r)
301                    } else {
302                        let l = encode_expr_bool(left, bool_vars, int_vars);
303                        let r = encode_expr_bool(right, bool_vars, int_vars);
304                        l.iff(&r)
305                    }
306                }
307                VerifyOp::Neq => {
308                    let li = encode_expr_int(left, int_vars);
309                    let ri = encode_expr_int(right, int_vars);
310                    if let (Some(l), Some(r)) = (li, ri) {
311                        l.eq(&r).not()
312                    } else {
313                        let l = encode_expr_bool(left, bool_vars, int_vars);
314                        let r = encode_expr_bool(right, bool_vars, int_vars);
315                        l.iff(&r).not()
316                    }
317                }
318                VerifyOp::Gt => {
319                    let l = encode_expr_int(left, int_vars).unwrap_or_else(|| Int::from_i64(0));
320                    let r = encode_expr_int(right, int_vars).unwrap_or_else(|| Int::from_i64(0));
321                    l.gt(&r)
322                }
323                VerifyOp::Lt => {
324                    let l = encode_expr_int(left, int_vars).unwrap_or_else(|| Int::from_i64(0));
325                    let r = encode_expr_int(right, int_vars).unwrap_or_else(|| Int::from_i64(0));
326                    l.lt(&r)
327                }
328                VerifyOp::Gte => {
329                    let l = encode_expr_int(left, int_vars).unwrap_or_else(|| Int::from_i64(0));
330                    let r = encode_expr_int(right, int_vars).unwrap_or_else(|| Int::from_i64(0));
331                    l.ge(&r)
332                }
333                VerifyOp::Lte => {
334                    let l = encode_expr_int(left, int_vars).unwrap_or_else(|| Int::from_i64(0));
335                    let r = encode_expr_int(right, int_vars).unwrap_or_else(|| Int::from_i64(0));
336                    l.le(&r)
337                }
338                VerifyOp::Add | VerifyOp::Sub | VerifyOp::Mul | VerifyOp::Div | VerifyOp::FloorDiv => {
339                    Bool::from_bool(false) // arithmetic ops aren't Bool
340                }
341            }
342        }
343        VerifyExpr::Iff(l, r) => {
344            let lb = encode_expr_bool(l, bool_vars, int_vars);
345            let rb = encode_expr_bool(r, bool_vars, int_vars);
346            lb.iff(&rb)
347        }
348        VerifyExpr::ForAll { vars, body } => {
349            if vars.is_empty() {
350                return encode_expr_bool(body, bool_vars, int_vars);
351            }
352            let body_bool = encode_expr_bool(body, bool_vars, int_vars);
353            let bound_consts: Vec<Dynamic> = vars.iter().map(|(name, ty)| {
354                match ty {
355                    crate::ir::VerifyType::Int | crate::ir::VerifyType::Object => {
356                        Dynamic::from_ast(&Int::new_const(name.as_str()))
357                    }
358                    crate::ir::VerifyType::Bool => {
359                        Dynamic::from_ast(&Bool::new_const(name.as_str()))
360                    }
361                    crate::ir::VerifyType::Real => {
362                        Dynamic::from_ast(&z3::ast::Real::new_const(name.as_str()))
363                    }
364                    crate::ir::VerifyType::BitVector(w) => {
365                        Dynamic::from_ast(&z3::ast::BV::new_const(name.as_str(), *w))
366                    }
367                    _ => Dynamic::from_ast(&Int::new_const(name.as_str())),
368                }
369            }).collect();
370            let refs: Vec<&dyn Ast> = bound_consts.iter().map(|d| d as &dyn Ast).collect();
371            z3::ast::forall_const(&refs, &[], &body_bool)
372        }
373        VerifyExpr::Exists { vars, body } => {
374            if vars.is_empty() {
375                return encode_expr_bool(body, bool_vars, int_vars);
376            }
377            let body_bool = encode_expr_bool(body, bool_vars, int_vars);
378            let bound_consts: Vec<Dynamic> = vars.iter().map(|(name, ty)| {
379                match ty {
380                    crate::ir::VerifyType::Int | crate::ir::VerifyType::Object => {
381                        Dynamic::from_ast(&Int::new_const(name.as_str()))
382                    }
383                    crate::ir::VerifyType::Bool => {
384                        Dynamic::from_ast(&Bool::new_const(name.as_str()))
385                    }
386                    crate::ir::VerifyType::Real => {
387                        Dynamic::from_ast(&z3::ast::Real::new_const(name.as_str()))
388                    }
389                    crate::ir::VerifyType::BitVector(w) => {
390                        Dynamic::from_ast(&z3::ast::BV::new_const(name.as_str(), *w))
391                    }
392                    _ => Dynamic::from_ast(&Int::new_const(name.as_str())),
393                }
394            }).collect();
395            let refs: Vec<&dyn Ast> = bound_consts.iter().map(|d| d as &dyn Ast).collect();
396            z3::ast::exists_const(&refs, &[], &body_bool)
397        }
398        _ => Bool::from_bool(true),
399    }
400}
401
402/// Try to encode an expression as a Z3 Int. Returns None if not integer-typed.
403pub fn encode_expr_int(
404    expr: &VerifyExpr,
405    int_vars: &HashMap<String, Int>,
406) -> Option<Int> {
407    match expr {
408        VerifyExpr::Int(n) => Some(Int::from_i64(*n)),
409        VerifyExpr::Var(name) => {
410            if let Some(iv) = int_vars.get(name) {
411                Some(iv.clone())
412            } else {
413                // If it looks like it should be an int, create one
414                Some(Int::new_const(name.as_str()))
415            }
416        }
417        VerifyExpr::Binary { op, left, right } => {
418            match op {
419                VerifyOp::Add => {
420                    let l = encode_expr_int(left, int_vars)?;
421                    let r = encode_expr_int(right, int_vars)?;
422                    Some(Int::add(&[&l, &r]))
423                }
424                VerifyOp::Sub => {
425                    let l = encode_expr_int(left, int_vars)?;
426                    let r = encode_expr_int(right, int_vars)?;
427                    Some(Int::sub(&[&l, &r]))
428                }
429                VerifyOp::Mul => {
430                    let l = encode_expr_int(left, int_vars)?;
431                    let r = encode_expr_int(right, int_vars)?;
432                    Some(Int::mul(&[&l, &r]))
433                }
434                VerifyOp::Div => {
435                    let l = encode_expr_int(left, int_vars)?;
436                    let r = encode_expr_int(right, int_vars)?;
437                    Some(l.div(&r))
438                }
439                // Floor division: real division then floor (`Real::to_int`), exact toward -inf.
440                VerifyOp::FloorDiv => {
441                    let l = encode_expr_int(left, int_vars)?;
442                    let r = encode_expr_int(right, int_vars)?;
443                    Some((l.to_real() / r.to_real()).to_int())
444                }
445                _ => None,
446            }
447        }
448        _ => None,
449    }
450}
logicaffeine_verify/kinduction.rs

logicaffeine_verify/
kinduction.rs
