logicaffeine_verify/
equivalence.rs

1//! Semantic Equivalence Checking — The Core Contribution
2//!
3//! The question nobody else asks: does the LLM-generated SVA express
4//! the SAME property as the formally parsed FOL?
5//!
6//! ## Method
7//!
8//! Given two VerifyExpr formulas (one from FOL, one from SVA), both
9//! unrolled to bounded timesteps:
10//!
11//! 1. Declare all signal@timestep variables as Z3 booleans
12//! 2. Construct ¬(FOL ↔ SVA)
13//! 3. If UNSAT → equivalent (no assignment makes them differ)
14//! 4. If SAT → extract counterexample trace from Z3 model
15//! 5. If UNKNOWN → timeout/undecidable
16//!
17//! ## Why This Matters
18//!
19//! Current industry practice: SVAs are checked against RTL (the hardware
20//! implementation). Nobody checks SVAs against the specification, because
21//! nobody has a formal specification. LOGOS provides one.
22
23use crate::ir::{VerifyExpr, VerifyOp, VerifyType, BitVecOp};
24use std::collections::{HashMap, HashSet};
25use z3::{ast::Ast, ast::Bool, ast::Dynamic, ast::Int, SatResult};
26
27/// Result of checking semantic equivalence.
28#[derive(Debug)]
29pub enum EquivalenceResult {
30    /// The two expressions are semantically equivalent at the given bound.
31    Equivalent,
32    /// The expressions differ. Counterexample shows concrete signal values
33    /// where they diverge.
34    NotEquivalent { counterexample: Trace },
35    /// Z3 returned unknown (timeout or undecidable).
36    Unknown,
37}
38
39/// A counterexample trace showing signal values at each clock cycle.
40#[derive(Debug, Clone)]
41pub struct Trace {
42    pub cycles: Vec<CycleState>,
43}
44
45/// Multi-sorted signal value for counterexample traces.
46#[derive(Debug, Clone, PartialEq)]
47pub enum SignalValue {
48    Bool(bool),
49    Int(i64),
50    BitVec { width: u32, value: u64 },
51    Unknown,
52}
53
54impl SignalValue {
55    /// Get as bool if this is a boolean value.
56    pub fn as_bool(&self) -> Option<bool> {
57        match self {
58            SignalValue::Bool(b) => Some(*b),
59            _ => None,
60        }
61    }
62
63    /// Get as i64 if this is an integer value.
64    pub fn as_int(&self) -> Option<i64> {
65        match self {
66            SignalValue::Int(n) => Some(*n),
67            _ => None,
68        }
69    }
70}
71
72impl std::fmt::Display for SignalValue {
73    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
74        match self {
75            SignalValue::Bool(b) => write!(f, "{}", b),
76            SignalValue::Int(n) => write!(f, "{}", n),
77            SignalValue::BitVec { width, value } => {
78                let hex_digits = ((*width + 3) / 4) as usize;
79                write!(f, "0x{:0>width$X}", value, width = hex_digits)
80            }
81            SignalValue::Unknown => write!(f, "?"),
82        }
83    }
84}
85
86/// Signal assignments at a single clock cycle.
87#[derive(Debug, Clone)]
88pub struct CycleState {
89    pub cycle: usize,
90    pub signals: HashMap<String, SignalValue>,
91}
92
93/// Check whether two VerifyExpr formulas are semantically equivalent.
94///
95/// Both formulas should be bounded (timestep-unrolled) — i.e., all temporal
96/// operators have been expanded to conjunctions/disjunctions over timesteps,
97/// and signal references use the "name@timestep" naming convention.
98///
99/// The `signals` parameter lists signal names (without @timestep) to declare
100/// as boolean variables at each timestep.
101///
102/// # Example
103///
104/// ```
105/// use logicaffeine_verify::ir::{VerifyExpr, VerifyOp};
106/// use logicaffeine_verify::equivalence::{check_equivalence, EquivalenceResult};
107///
108/// let fol = VerifyExpr::binary(VerifyOp::Implies,
109///     VerifyExpr::Var("req@0".into()),
110///     VerifyExpr::Var("ack@0".into()),
111/// );
112/// let sva = VerifyExpr::binary(VerifyOp::Implies,
113///     VerifyExpr::Var("req@0".into()),
114///     VerifyExpr::Var("ack@0".into()),
115/// );
116/// let result = check_equivalence(&fol, &sva, &["req".into(), "ack".into()], 1);
117/// assert!(matches!(result, EquivalenceResult::Equivalent));
118/// ```
119pub fn check_equivalence(
120    fol_expr: &VerifyExpr,
121    sva_expr: &VerifyExpr,
122    signals: &[String],
123    bound: usize,
124) -> EquivalenceResult {
125    let solver = crate::solver::new_solver();
126
127    // 1. Collect all variable names referenced in both expressions
128    let mut all_vars: HashSet<String> = HashSet::new();
129    collect_vars(fol_expr, &mut all_vars);
130    collect_vars(sva_expr, &mut all_vars);
131
132    // Also declare signal@timestep variables from the signals list
133    for sig in signals {
134        for t in 0..=bound {
135            all_vars.insert(format!("{}@{}", sig, t));
136        }
137    }
138
139    // 2. Declare all signal@timestep variables as Z3 booleans,
140    //    and collect any integer variable names from the expressions.
141    let mut bool_vars: HashMap<String, Bool> = HashMap::new();
142    let mut int_vars: HashMap<String, Int> = HashMap::new();
143    let mut bv_vars: HashMap<String, z3::ast::BV> = HashMap::new();
144    let mut array_vars: HashMap<String, z3::ast::Array> = HashMap::new();
145    for var_name in &all_vars {
146        bool_vars.insert(
147            var_name.clone(),
148            Bool::new_const(var_name.as_str()),
149        );
150    }
151    // Pre-declare integer variables found in Int-typed positions
152    collect_int_vars(fol_expr, &mut int_vars);
153    collect_int_vars(sva_expr, &mut int_vars);
154    // Also collect variables used as array indices/values (they need Int sort)
155    collect_array_index_vars(fol_expr, &mut int_vars);
156    collect_array_index_vars(sva_expr, &mut int_vars);
157    // Collect quantifier-bound variables with their declared types
158    collect_quantifier_bound_vars(fol_expr, &mut int_vars, &mut bv_vars, &mut array_vars);
159    collect_quantifier_bound_vars(sva_expr, &mut int_vars, &mut bv_vars, &mut array_vars);
160    // Pre-declare bitvector variables found in BV-typed positions
161    collect_bv_vars(fol_expr, &mut bv_vars);
162    collect_bv_vars(sva_expr, &mut bv_vars);
163    // Pre-declare array variables found in array-typed positions
164    collect_array_vars(fol_expr, &mut array_vars);
165    collect_array_vars(sva_expr, &mut array_vars);
166
167    // 3. Encode both expressions into Z3 using the dynamic encoder
168    let encoder = EquivEncoder {
169        bool_vars: &bool_vars,
170        int_vars: &int_vars,
171        bv_vars: &bv_vars,
172        array_vars: &array_vars,
173    };
174    let fol_z3 = encoder.encode(fol_expr);
175    let sva_z3 = encoder.encode(sva_expr);
176
177    // 4. Construct ¬(FOL ↔ SVA) and check satisfiability
178    //    For Bool sorts, use iff; for other sorts, use _eq
179    //    If sorts differ (e.g. BV vs Bool), return NotEquivalent immediately
180    let fol_sort = fol_z3.get_sort();
181    let sva_sort = sva_z3.get_sort();
182    if fol_sort != sva_sort {
183        // Sort mismatch — expressions cannot be equivalent
184        return EquivalenceResult::NotEquivalent {
185            counterexample: Trace { cycles: vec![] },
186        };
187    }
188    let not_iff = if let (Some(fb), Some(sb)) = (fol_z3.as_bool(), sva_z3.as_bool()) {
189        fb.iff(&sb).not()
190    } else {
191        fol_z3.eq(&sva_z3).not()
192    };
193
194    solver.assert(&not_iff);
195
196    match solver.check() {
197        SatResult::Unsat => {
198            // No assignment makes them differ → equivalent
199            EquivalenceResult::Equivalent
200        }
201        SatResult::Sat => {
202            // Found an assignment where they differ → extract counterexample
203            let model = solver.get_model().unwrap();
204            let trace = extract_trace(&model, signals, bound, &bool_vars, &int_vars, &bv_vars);
205            EquivalenceResult::NotEquivalent { counterexample: trace }
206        }
207        SatResult::Unknown => EquivalenceResult::Unknown,
208    }
209}
210
211/// Extract unique signal names from a VerifyExpr by collecting Var references
212/// and stripping the @timestep suffix.
213pub fn extract_signals(expr: &VerifyExpr) -> Vec<String> {
214    let mut vars = HashSet::new();
215    collect_vars(expr, &mut vars);
216    let mut signals: HashSet<String> = HashSet::new();
217    for var in &vars {
218        if let Some(at_pos) = var.find('@') {
219            signals.insert(var[..at_pos].to_string());
220        }
221    }
222    signals.into_iter().collect()
223}
224
225/// Collect all variable names referenced in a VerifyExpr (public API).
226pub fn collect_vars_pub(expr: &VerifyExpr, vars: &mut HashSet<String>) {
227    collect_vars(expr, vars);
228}
229
230/// Collect integer-typed variable names from a VerifyExpr (public API).
231pub fn collect_int_vars_pub(expr: &VerifyExpr, int_vars: &mut HashMap<String, Int>) {
232    collect_int_vars(expr, int_vars);
233}
234
235/// Collect quantifier-bound variables from a VerifyExpr (public API).
236pub fn collect_quantifier_bound_vars_pub(
237    expr: &VerifyExpr,
238    int_vars: &mut HashMap<String, Int>,
239    bv_vars: &mut HashMap<String, z3::ast::BV>,
240    array_vars: &mut HashMap<String, z3::ast::Array>,
241) {
242    collect_quantifier_bound_vars(expr, int_vars, bv_vars, array_vars);
243}
244
245/// Collect all variable names referenced in a VerifyExpr.
246fn collect_vars(expr: &VerifyExpr, vars: &mut HashSet<String>) {
247    match expr {
248        VerifyExpr::Var(name) => { vars.insert(name.clone()); }
249        VerifyExpr::Binary { left, right, .. } => {
250            collect_vars(left, vars);
251            collect_vars(right, vars);
252        }
253        VerifyExpr::Not(inner) => collect_vars(inner, vars),
254        VerifyExpr::Iff(l, r) => {
255            collect_vars(l, vars);
256            collect_vars(r, vars);
257        }
258        VerifyExpr::ForAll { body, .. } => collect_vars(body, vars),
259        VerifyExpr::Exists { body, .. } => collect_vars(body, vars),
260        VerifyExpr::Apply { args, .. } | VerifyExpr::ApplyInt { args, .. } => {
261            for arg in args { collect_vars(arg, vars); }
262        }
263        // Bitvector and array variants
264        VerifyExpr::BitVecBinary { left, right, .. } => {
265            collect_vars(left, vars);
266            collect_vars(right, vars);
267        }
268        VerifyExpr::BitVecExtract { operand, .. } => collect_vars(operand, vars),
269        VerifyExpr::BitVecConcat(l, r) => {
270            collect_vars(l, vars);
271            collect_vars(r, vars);
272        }
273        VerifyExpr::Select { array, index } => {
274            collect_vars(array, vars);
275            collect_vars(index, vars);
276        }
277        VerifyExpr::Store { array, index, value } => {
278            collect_vars(array, vars);
279            collect_vars(index, vars);
280            collect_vars(value, vars);
281        }
282        VerifyExpr::AtState { state, expr } => {
283            collect_vars(state, vars);
284            collect_vars(expr, vars);
285        }
286        VerifyExpr::Transition { from, to } => {
287            collect_vars(from, vars);
288            collect_vars(to, vars);
289        }
290        // Literals have no variables
291        VerifyExpr::Int(_) | VerifyExpr::Bool(_) | VerifyExpr::BitVecConst { .. } => {}
292    }
293}
294
295/// Collect variable names that appear in integer-typed positions (inside arithmetic ops).
296fn collect_int_vars(expr: &VerifyExpr, int_vars: &mut HashMap<String, Int>) {
297    match expr {
298        VerifyExpr::Int(_) => {}
299        VerifyExpr::Bool(_) => {}
300        VerifyExpr::Var(_) => {} // Vars are bool by default; promoted to int when used in arith context
301        VerifyExpr::Binary { op, left, right } => {
302            match op {
303                // Arithmetic ops: children are integer-typed
304                VerifyOp::Add | VerifyOp::Sub | VerifyOp::Mul | VerifyOp::Div | VerifyOp::FloorDiv => {
305                    collect_int_var_leaves(left, int_vars);
306                    collect_int_var_leaves(right, int_vars);
307                }
308                // Comparison ops: children are integer-typed
309                VerifyOp::Gt | VerifyOp::Lt | VerifyOp::Gte | VerifyOp::Lte => {
310                    collect_int_var_leaves(left, int_vars);
311                    collect_int_var_leaves(right, int_vars);
312                }
313                // Eq/Neq: could be bool or int — check if children look integer
314                VerifyOp::Eq | VerifyOp::Neq => {
315                    if expr_is_integer(left) || expr_is_integer(right) {
316                        collect_int_var_leaves(left, int_vars);
317                        collect_int_var_leaves(right, int_vars);
318                    }
319                }
320                _ => {}
321            }
322            collect_int_vars(left, int_vars);
323            collect_int_vars(right, int_vars);
324        }
325        VerifyExpr::Not(inner) => collect_int_vars(inner, int_vars),
326        VerifyExpr::Iff(l, r) => {
327            collect_int_vars(l, int_vars);
328            collect_int_vars(r, int_vars);
329        }
330        VerifyExpr::ForAll { body, .. } | VerifyExpr::Exists { body, .. } => {
331            collect_int_vars(body, int_vars);
332        }
333        VerifyExpr::Apply { args, .. } | VerifyExpr::ApplyInt { args, .. } => {
334            for arg in args { collect_int_vars(arg, int_vars); }
335        }
336        _ => {}
337    }
338}
339
340/// Recursively collect Var leaves from integer-typed subexpressions.
341fn collect_int_var_leaves(expr: &VerifyExpr, int_vars: &mut HashMap<String, Int>) {
342    match expr {
343        VerifyExpr::Var(name) => {
344            if !int_vars.contains_key(name) {
345                int_vars.insert(name.clone(), Int::new_const(name.as_str()));
346            }
347        }
348        VerifyExpr::Binary { left, right, .. } => {
349            collect_int_var_leaves(left, int_vars);
350            collect_int_var_leaves(right, int_vars);
351        }
352        _ => {}
353    }
354}
355
356/// Collect variable names that appear in bitvector-typed positions.
357fn collect_bv_vars(expr: &VerifyExpr, bv_vars: &mut HashMap<String, z3::ast::BV>) {
358    match expr {
359        VerifyExpr::BitVecBinary { op: _, left, right } => {
360            collect_bv_var_leaves(left, bv_vars, None);
361            collect_bv_var_leaves(right, bv_vars, None);
362            collect_bv_vars(left, bv_vars);
363            collect_bv_vars(right, bv_vars);
364        }
365        VerifyExpr::BitVecExtract { operand, .. } => {
366            collect_bv_var_leaves(operand, bv_vars, None);
367            collect_bv_vars(operand, bv_vars);
368        }
369        VerifyExpr::BitVecConcat(l, r) => {
370            collect_bv_var_leaves(l, bv_vars, None);
371            collect_bv_var_leaves(r, bv_vars, None);
372            collect_bv_vars(l, bv_vars);
373            collect_bv_vars(r, bv_vars);
374        }
375        VerifyExpr::Binary { left, right, .. } => {
376            collect_bv_vars(left, bv_vars);
377            collect_bv_vars(right, bv_vars);
378        }
379        VerifyExpr::Not(inner) => collect_bv_vars(inner, bv_vars),
380        VerifyExpr::Iff(l, r) => {
381            collect_bv_vars(l, bv_vars);
382            collect_bv_vars(r, bv_vars);
383        }
384        VerifyExpr::ForAll { body, .. } | VerifyExpr::Exists { body, .. } => {
385            collect_bv_vars(body, bv_vars);
386        }
387        VerifyExpr::Apply { args, .. } | VerifyExpr::ApplyInt { args, .. } => {
388            for arg in args { collect_bv_vars(arg, bv_vars); }
389        }
390        VerifyExpr::Select { array, index } => {
391            collect_bv_vars(array, bv_vars);
392            collect_bv_vars(index, bv_vars);
393        }
394        VerifyExpr::Store { array, index, value } => {
395            collect_bv_vars(array, bv_vars);
396            collect_bv_vars(index, bv_vars);
397            collect_bv_vars(value, bv_vars);
398        }
399        VerifyExpr::AtState { state, expr } => {
400            collect_bv_vars(state, bv_vars);
401            collect_bv_vars(expr, bv_vars);
402        }
403        VerifyExpr::Transition { from, to } => {
404            collect_bv_vars(from, bv_vars);
405            collect_bv_vars(to, bv_vars);
406        }
407        _ => {}
408    }
409}
410
411/// Recursively collect Var leaves from bitvector-typed subexpressions.
412fn collect_bv_var_leaves(expr: &VerifyExpr, bv_vars: &mut HashMap<String, z3::ast::BV>, width_hint: Option<u32>) {
413    match expr {
414        VerifyExpr::Var(name) => {
415            if !bv_vars.contains_key(name) {
416                // Determine width from context or default to 8
417                let width = width_hint.unwrap_or_else(|| infer_bv_width_from_name(name));
418                bv_vars.insert(name.clone(), z3::ast::BV::new_const(name.as_str(), width));
419            }
420        }
421        VerifyExpr::BitVecConst { width: _, .. } => {
422            // A constant tells us the width of sibling vars
423            // (handled by the caller)
424        }
425        VerifyExpr::BitVecBinary { left, right, .. } => {
426            // Try to extract width from either side
427            let w = bv_expr_width(expr);
428            collect_bv_var_leaves(left, bv_vars, w);
429            collect_bv_var_leaves(right, bv_vars, w);
430        }
431        VerifyExpr::Binary { left, right, .. } => {
432            collect_bv_var_leaves(left, bv_vars, width_hint);
433            collect_bv_var_leaves(right, bv_vars, width_hint);
434        }
435        _ => {}
436    }
437}
438
439/// Infer bitvector width from variable name convention (e.g., "x_bv8" → 8, "data_bv16" → 16).
440fn infer_bv_width_from_name(name: &str) -> u32 {
441    if let Some(pos) = name.rfind("_bv") {
442        if let Ok(w) = name[pos + 3..].parse::<u32>() {
443            return w;
444        }
445    }
446    // Also try "bvN" at end without underscore
447    if let Some(pos) = name.rfind("bv") {
448        if let Ok(w) = name[pos + 2..].parse::<u32>() {
449            return w;
450        }
451    }
452    8 // default width
453}
454
455/// Try to determine the bitvector width of an expression.
456fn bv_expr_width(expr: &VerifyExpr) -> Option<u32> {
457    match expr {
458        VerifyExpr::BitVecConst { width, .. } => Some(*width),
459        VerifyExpr::BitVecBinary { left, right, .. } => {
460            bv_expr_width(left).or_else(|| bv_expr_width(right))
461        }
462        VerifyExpr::BitVecExtract { high, low, .. } => Some(high - low + 1),
463        VerifyExpr::BitVecConcat(l, r) => {
464            match (bv_expr_width(l), bv_expr_width(r)) {
465                (Some(wl), Some(wr)) => Some(wl + wr),
466                _ => None,
467            }
468        }
469        VerifyExpr::Var(name) => {
470            let w = infer_bv_width_from_name(name);
471            if w != 8 { Some(w) } else { None } // Only return if we found an explicit width
472        }
473        _ => None,
474    }
475}
476
477/// Collect variable names that appear in array-typed positions.
478/// Also collects index/value variables as int vars since arrays use Int → Int by default.
479fn collect_array_vars(expr: &VerifyExpr, array_vars: &mut HashMap<String, z3::ast::Array>) {
480    collect_array_vars_inner(expr, array_vars);
481}
482
483fn collect_array_vars_inner(expr: &VerifyExpr, array_vars: &mut HashMap<String, z3::ast::Array>) {
484    match expr {
485        VerifyExpr::Select { array, index } => {
486            if let VerifyExpr::Var(name) = array.as_ref() {
487                if !array_vars.contains_key(name) {
488                    let int_sort = z3::Sort::int();
489                    array_vars.insert(
490                        name.clone(),
491                        z3::ast::Array::new_const(name.as_str(), &int_sort, &int_sort),
492                    );
493                }
494            }
495            collect_array_vars_inner(array, array_vars);
496            collect_array_vars_inner(index, array_vars);
497        }
498        VerifyExpr::Store { array, index, value } => {
499            if let VerifyExpr::Var(name) = array.as_ref() {
500                if !array_vars.contains_key(name) {
501                    let int_sort = z3::Sort::int();
502                    array_vars.insert(
503                        name.clone(),
504                        z3::ast::Array::new_const(name.as_str(), &int_sort, &int_sort),
505                    );
506                }
507            }
508            collect_array_vars_inner(array, array_vars);
509            collect_array_vars_inner(index, array_vars);
510            collect_array_vars_inner(value, array_vars);
511        }
512        VerifyExpr::Binary { left, right, .. } => {
513            collect_array_vars_inner(left, array_vars);
514            collect_array_vars_inner(right, array_vars);
515        }
516        VerifyExpr::Not(inner) => collect_array_vars_inner(inner, array_vars),
517        VerifyExpr::Iff(l, r) => {
518            collect_array_vars_inner(l, array_vars);
519            collect_array_vars_inner(r, array_vars);
520        }
521        VerifyExpr::ForAll { body, .. } | VerifyExpr::Exists { body, .. } => {
522            collect_array_vars_inner(body, array_vars);
523        }
524        _ => {}
525    }
526}
527
528/// Collect variables used as array indices or values (they need Int sort, not Bool).
529fn collect_array_index_vars(expr: &VerifyExpr, int_vars: &mut HashMap<String, Int>) {
530    match expr {
531        VerifyExpr::Select { array, index } => {
532            collect_int_var_leaves(index, int_vars);
533            collect_array_index_vars(array, int_vars);
534            collect_array_index_vars(index, int_vars);
535        }
536        VerifyExpr::Store { array, index, value } => {
537            collect_int_var_leaves(index, int_vars);
538            collect_int_var_leaves(value, int_vars);
539            collect_array_index_vars(array, int_vars);
540            collect_array_index_vars(index, int_vars);
541            collect_array_index_vars(value, int_vars);
542        }
543        VerifyExpr::Binary { left, right, .. } => {
544            collect_array_index_vars(left, int_vars);
545            collect_array_index_vars(right, int_vars);
546        }
547        VerifyExpr::Not(inner) => collect_array_index_vars(inner, int_vars),
548        VerifyExpr::Iff(l, r) => {
549            collect_array_index_vars(l, int_vars);
550            collect_array_index_vars(r, int_vars);
551        }
552        VerifyExpr::ForAll { body, .. } | VerifyExpr::Exists { body, .. } => {
553            collect_array_index_vars(body, int_vars);
554        }
555        _ => {}
556    }
557}
558
559/// Collect quantifier-bound variables with their declared types.
560fn collect_quantifier_bound_vars(
561    expr: &VerifyExpr,
562    int_vars: &mut HashMap<String, Int>,
563    bv_vars: &mut HashMap<String, z3::ast::BV>,
564    array_vars: &mut HashMap<String, z3::ast::Array>,
565) {
566    match expr {
567        VerifyExpr::ForAll { vars, body } | VerifyExpr::Exists { vars, body } => {
568            for (name, ty) in vars {
569                match ty {
570                    VerifyType::Int | VerifyType::Object | VerifyType::Real => {
571                        if !int_vars.contains_key(name) {
572                            int_vars.insert(name.clone(), Int::new_const(name.as_str()));
573                        }
574                    }
575                    VerifyType::BitVector(w) => {
576                        if !bv_vars.contains_key(name) {
577                            bv_vars.insert(name.clone(), z3::ast::BV::new_const(name.as_str(), *w));
578                        }
579                    }
580                    VerifyType::Array(idx, elem) => {
581                        if !array_vars.contains_key(name) {
582                            let idx_sort = type_to_z3_sort(idx);
583                            let elem_sort = type_to_z3_sort(elem);
584                            array_vars.insert(
585                                name.clone(),
586                                z3::ast::Array::new_const(name.as_str(), &idx_sort, &elem_sort),
587                            );
588                        }
589                    }
590                    VerifyType::Bool => {
591                        // Bool vars are already declared in bool_vars by default
592                    }
593                }
594            }
595            collect_quantifier_bound_vars(body, int_vars, bv_vars, array_vars);
596        }
597        VerifyExpr::Binary { left, right, .. } => {
598            collect_quantifier_bound_vars(left, int_vars, bv_vars, array_vars);
599            collect_quantifier_bound_vars(right, int_vars, bv_vars, array_vars);
600        }
601        VerifyExpr::Not(inner) => {
602            collect_quantifier_bound_vars(inner, int_vars, bv_vars, array_vars);
603        }
604        VerifyExpr::Iff(l, r) => {
605            collect_quantifier_bound_vars(l, int_vars, bv_vars, array_vars);
606            collect_quantifier_bound_vars(r, int_vars, bv_vars, array_vars);
607        }
608        _ => {}
609    }
610}
611
612/// Convert a VerifyType to a Z3 Sort (standalone function).
613fn type_to_z3_sort(ty: &VerifyType) -> z3::Sort {
614    match ty {
615        VerifyType::Int => z3::Sort::int(),
616        VerifyType::Bool => z3::Sort::bool(),
617        VerifyType::Object => z3::Sort::int(),
618        VerifyType::Real => z3::Sort::real(),
619        VerifyType::BitVector(w) => z3::Sort::bitvector(*w),
620        VerifyType::Array(idx, elem) => {
621            let idx_sort = type_to_z3_sort(idx);
622            let elem_sort = type_to_z3_sort(elem);
623            z3::Sort::array(&idx_sort, &elem_sort)
624        }
625    }
626}
627
628/// Heuristic: does this expression look like it produces an integer?
629fn expr_is_integer(expr: &VerifyExpr) -> bool {
630    matches!(expr,
631        VerifyExpr::Int(_)
632        | VerifyExpr::Binary { op: VerifyOp::Add | VerifyOp::Sub | VerifyOp::Mul | VerifyOp::Div | VerifyOp::FloorDiv, .. }
633    )
634}
635
636/// Encoder that handles Bool, Int, BitVec, and Array Z3 expressions for equivalence checking.
637pub struct EquivEncoder<'a> {
638    bool_vars: &'a HashMap<String, Bool>,
639    int_vars: &'a HashMap<String, Int>,
640    bv_vars: &'a HashMap<String, z3::ast::BV>,
641    array_vars: &'a HashMap<String, z3::ast::Array>,
642}
643
644impl<'a> EquivEncoder<'a> {
645    /// Create a full encoder with all variable maps.
646    pub fn new(
647        bool_vars: &'a HashMap<String, Bool>,
648        int_vars: &'a HashMap<String, Int>,
649        bv_vars: &'a HashMap<String, z3::ast::BV>,
650        array_vars: &'a HashMap<String, z3::ast::Array>,
651    ) -> Self {
652        Self { bool_vars, int_vars, bv_vars, array_vars }
653    }
654
655    /// Encode as a Dynamic Z3 expression (may be Bool or Int).
656    fn encode(&self, expr: &VerifyExpr) -> Dynamic {
657        match expr {
658            VerifyExpr::Bool(b) => Dynamic::from_ast(&Bool::from_bool(*b)),
659
660            VerifyExpr::Int(n) => Dynamic::from_ast(&Int::from_i64(*n)),
661
662            VerifyExpr::Var(name) => {
663                // Check in order of specificity: BV > Array > Int > Bool
664                if let Some(bv) = self.bv_vars.get(name) {
665                    Dynamic::from_ast(bv)
666                } else if let Some(arr) = self.array_vars.get(name) {
667                    Dynamic::from_ast(arr)
668                } else if let Some(iv) = self.int_vars.get(name) {
669                    Dynamic::from_ast(iv)
670                } else if let Some(bv) = self.bool_vars.get(name) {
671                    Dynamic::from_ast(bv)
672                } else {
673                    Dynamic::from_ast(&Bool::new_const(name.as_str()))
674                }
675            }
676
677            VerifyExpr::Binary { op, left, right } => {
678                let l = self.encode(left);
679                let r = self.encode(right);
680                match op {
681                    // Boolean ops
682                    VerifyOp::And => {
683                        if let (Some(lb), Some(rb)) = (l.as_bool(), r.as_bool()) {
684                            Dynamic::from_ast(&Bool::and(&[&lb, &rb]))
685                        } else {
686                            l // fallback
687                        }
688                    }
689                    VerifyOp::Or => {
690                        if let (Some(lb), Some(rb)) = (l.as_bool(), r.as_bool()) {
691                            Dynamic::from_ast(&Bool::or(&[&lb, &rb]))
692                        } else {
693                            l
694                        }
695                    }
696                    VerifyOp::Implies => {
697                        if let (Some(lb), Some(rb)) = (l.as_bool(), r.as_bool()) {
698                            Dynamic::from_ast(&lb.implies(&rb))
699                        } else {
700                            l
701                        }
702                    }
703                    // Equality: works for both Bool and Int
704                    VerifyOp::Eq => {
705                        if let (Some(li), Some(ri)) = (l.as_int(), r.as_int()) {
706                            Dynamic::from_ast(&li.eq(&ri))
707                        } else if let (Some(lb), Some(rb)) = (l.as_bool(), r.as_bool()) {
708                            Dynamic::from_ast(&lb.iff(&rb))
709                        } else {
710                            Dynamic::from_ast(&l.eq(&r))
711                        }
712                    }
713                    VerifyOp::Neq => {
714                        if let (Some(li), Some(ri)) = (l.as_int(), r.as_int()) {
715                            Dynamic::from_ast(&li.eq(&ri).not())
716                        } else if let (Some(lb), Some(rb)) = (l.as_bool(), r.as_bool()) {
717                            Dynamic::from_ast(&lb.iff(&rb).not())
718                        } else {
719                            Dynamic::from_ast(&l.eq(&r).not())
720                        }
721                    }
722                    // Arithmetic ops → Int
723                    VerifyOp::Add => {
724                        if let (Some(li), Some(ri)) = (l.as_int(), r.as_int()) {
725                            Dynamic::from_ast(&Int::add(&[&li, &ri]))
726                        } else { l }
727                    }
728                    VerifyOp::Sub => {
729                        if let (Some(li), Some(ri)) = (l.as_int(), r.as_int()) {
730                            Dynamic::from_ast(&Int::sub(&[&li, &ri]))
731                        } else { l }
732                    }
733                    VerifyOp::Mul => {
734                        if let (Some(li), Some(ri)) = (l.as_int(), r.as_int()) {
735                            Dynamic::from_ast(&Int::mul(&[&li, &ri]))
736                        } else { l }
737                    }
738                    VerifyOp::Div => {
739                        if let (Some(li), Some(ri)) = (l.as_int(), r.as_int()) {
740                            Dynamic::from_ast(&li.div(&ri))
741                        } else { l }
742                    }
743                    // Floor division: real division then floor (`Real::to_int`), exact toward -inf.
744                    VerifyOp::FloorDiv => {
745                        if let (Some(li), Some(ri)) = (l.as_int(), r.as_int()) {
746                            Dynamic::from_ast(&(li.to_real() / ri.to_real()).to_int())
747                        } else { l }
748                    }
749                    // Comparison ops → Bool (from Int operands)
750                    VerifyOp::Gt => {
751                        if let (Some(li), Some(ri)) = (l.as_int(), r.as_int()) {
752                            Dynamic::from_ast(&li.gt(&ri))
753                        } else { Dynamic::from_ast(&Bool::from_bool(false)) }
754                    }
755                    VerifyOp::Lt => {
756                        if let (Some(li), Some(ri)) = (l.as_int(), r.as_int()) {
757                            Dynamic::from_ast(&li.lt(&ri))
758                        } else { Dynamic::from_ast(&Bool::from_bool(false)) }
759                    }
760                    VerifyOp::Gte => {
761                        if let (Some(li), Some(ri)) = (l.as_int(), r.as_int()) {
762                            Dynamic::from_ast(&li.ge(&ri))
763                        } else { Dynamic::from_ast(&Bool::from_bool(false)) }
764                    }
765                    VerifyOp::Lte => {
766                        if let (Some(li), Some(ri)) = (l.as_int(), r.as_int()) {
767                            Dynamic::from_ast(&li.le(&ri))
768                        } else { Dynamic::from_ast(&Bool::from_bool(false)) }
769                    }
770                }
771            }
772
773            VerifyExpr::Not(inner) => {
774                let i = self.encode(inner);
775                if let Some(b) = i.as_bool() {
776                    Dynamic::from_ast(&b.not())
777                } else {
778                    i
779                }
780            }
781
782            VerifyExpr::Iff(l, r) => {
783                let lb = self.encode(l);
784                let rb = self.encode(r);
785                if let (Some(lbool), Some(rbool)) = (lb.as_bool(), rb.as_bool()) {
786                    Dynamic::from_ast(&lbool.iff(&rbool))
787                } else {
788                    Dynamic::from_ast(&lb.eq(&rb))
789                }
790            }
791
792            VerifyExpr::ApplyInt { name, args } => {
793                let encoded_args: Vec<Dynamic> = args.iter().map(|a| self.encode(a)).collect();
794                let arg_sorts: Vec<z3::Sort> = encoded_args.iter().map(|a| a.get_sort()).collect();
795                let arg_sort_refs: Vec<&z3::Sort> = arg_sorts.iter().collect();
796                let int_sort = z3::Sort::int();
797                let func_decl = z3::FuncDecl::new(name.as_str(), &arg_sort_refs, &int_sort);
798                let arg_refs: Vec<&dyn z3::ast::Ast> = encoded_args.iter().map(|a| a as &dyn z3::ast::Ast).collect();
799                func_decl.apply(&arg_refs)
800            }
801
802            // Uninterpreted functions: create unique Z3 function symbol per name
803            VerifyExpr::Apply { name, args } => {
804                let encoded_args: Vec<Dynamic> = args.iter().map(|a| self.encode(a)).collect();
805                // Create a unique uninterpreted boolean function for each name
806                let arg_sorts: Vec<z3::Sort> = encoded_args.iter().map(|a| a.get_sort()).collect();
807                let arg_sort_refs: Vec<&z3::Sort> = arg_sorts.iter().collect();
808                let bool_sort = z3::Sort::bool();
809                let func_decl = z3::FuncDecl::new(name.as_str(), &arg_sort_refs, &bool_sort);
810                let arg_refs: Vec<&dyn z3::ast::Ast> = encoded_args.iter().map(|a| a as &dyn z3::ast::Ast).collect();
811                func_decl.apply(&arg_refs)
812            }
813
814            // Quantifiers: proper Z3 quantifier encoding
815            VerifyExpr::ForAll { vars, body } => {
816                if vars.is_empty() {
817                    return self.encode(body);
818                }
819                let body_encoded = self.encode_as_bool(body);
820                let bound_consts: Vec<Dynamic> = vars.iter().map(|(name, ty)| {
821                    self.make_quantifier_var(name, ty)
822                }).collect();
823                let bound_refs: Vec<&dyn Ast> = bound_consts.iter().map(|d| d as &dyn Ast).collect();
824                Dynamic::from_ast(&z3::ast::forall_const(&bound_refs, &[], &body_encoded))
825            }
826
827            VerifyExpr::Exists { vars, body } => {
828                if vars.is_empty() {
829                    return self.encode(body);
830                }
831                let body_encoded = self.encode_as_bool(body);
832                let bound_consts: Vec<Dynamic> = vars.iter().map(|(name, ty)| {
833                    self.make_quantifier_var(name, ty)
834                }).collect();
835                let bound_refs: Vec<&dyn Ast> = bound_consts.iter().map(|d| d as &dyn Ast).collect();
836                Dynamic::from_ast(&z3::ast::exists_const(&bound_refs, &[], &body_encoded))
837            }
838
839            // ---- Bitvector operations ----
840
841            VerifyExpr::BitVecConst { width, value } => {
842                Dynamic::from_ast(&z3::ast::BV::from_u64(*value, *width))
843            }
844
845            VerifyExpr::BitVecBinary { op, left, right } => {
846                let l = self.encode(left);
847                let r = self.encode(right);
848                self.encode_bv_binary(op, l, r)
849            }
850
851            VerifyExpr::BitVecExtract { high, low, operand } => {
852                let bv = self.encode(operand);
853                if let Some(bv) = bv.as_bv() {
854                    Dynamic::from_ast(&bv.extract(*high, *low))
855                } else {
856                    bv
857                }
858            }
859
860            VerifyExpr::BitVecConcat(left, right) => {
861                let l = self.encode(left);
862                let r = self.encode(right);
863                if let (Some(lb), Some(rb)) = (l.as_bv(), r.as_bv()) {
864                    Dynamic::from_ast(&lb.concat(&rb))
865                } else {
866                    l
867                }
868            }
869
870            // ---- Array theory ----
871
872            VerifyExpr::Select { array, index } => {
873                let a = self.encode(array);
874                let i = self.encode(index);
875                if let Some(arr) = a.as_array() {
876                    Dynamic::from_ast(&arr.select(&i))
877                } else {
878                    a
879                }
880            }
881
882            VerifyExpr::Store { array, index, value } => {
883                let a = self.encode(array);
884                let i = self.encode(index);
885                let v = self.encode(value);
886                if let Some(arr) = a.as_array() {
887                    Dynamic::from_ast(&arr.store(&i, &v))
888                } else {
889                    a
890                }
891            }
892
893            // ---- Temporal (BMC) ----
894
895            VerifyExpr::AtState { expr, .. } => {
896                self.encode(expr)
897            }
898
899            VerifyExpr::Transition { from, to } => {
900                let f = self.encode(from);
901                let t = self.encode(to);
902                if let (Some(fb), Some(tb)) = (f.as_bool(), t.as_bool()) {
903                    Dynamic::from_ast(&Bool::and(&[&fb, &tb]))
904                } else {
905                    f
906                }
907            }
908        }
909    }
910
911    /// Create a Z3 constant for a quantifier-bound variable with the correct sort.
912    fn make_quantifier_var(&self, name: &str, ty: &VerifyType) -> Dynamic {
913        match ty {
914            VerifyType::Int => Dynamic::from_ast(&Int::new_const(name)),
915            VerifyType::Bool => Dynamic::from_ast(&Bool::new_const(name)),
916            VerifyType::BitVector(w) => Dynamic::from_ast(&z3::ast::BV::new_const(name, *w)),
917            VerifyType::Object => Dynamic::from_ast(&Int::new_const(name)),
918            VerifyType::Real => Dynamic::from_ast(&z3::ast::Real::new_const(name)),
919            VerifyType::Array(idx, elem) => {
920                let idx_sort = self.type_to_sort(idx);
921                let elem_sort = self.type_to_sort(elem);
922                Dynamic::from_ast(&z3::ast::Array::new_const(name, &idx_sort, &elem_sort))
923            }
924        }
925    }
926
927    /// Convert a VerifyType to a Z3 Sort.
928    fn type_to_sort(&self, ty: &VerifyType) -> z3::Sort {
929        match ty {
930            VerifyType::Int => z3::Sort::int(),
931            VerifyType::Bool => z3::Sort::bool(),
932            VerifyType::Object => z3::Sort::int(),
933            VerifyType::Real => z3::Sort::real(),
934            VerifyType::BitVector(w) => z3::Sort::bitvector(*w),
935            VerifyType::Array(idx, elem) => {
936                let idx_sort = self.type_to_sort(idx);
937                let elem_sort = self.type_to_sort(elem);
938                z3::Sort::array(&idx_sort, &elem_sort)
939            }
940        }
941    }
942
943    /// Encode a bitvector binary operation.
944    fn encode_bv_binary(&self, op: &BitVecOp, l: Dynamic, r: Dynamic) -> Dynamic {
945        if let (Some(lb), Some(rb)) = (l.as_bv(), r.as_bv()) {
946            match op {
947                BitVecOp::And => Dynamic::from_ast(&lb.bvand(&rb)),
948                BitVecOp::Or => Dynamic::from_ast(&lb.bvor(&rb)),
949                BitVecOp::Xor => Dynamic::from_ast(&lb.bvxor(&rb)),
950                BitVecOp::Not => Dynamic::from_ast(&lb.bvnot()),
951                BitVecOp::Shl => Dynamic::from_ast(&lb.bvshl(&rb)),
952                BitVecOp::Shr => Dynamic::from_ast(&lb.bvlshr(&rb)),
953                BitVecOp::AShr => Dynamic::from_ast(&lb.bvashr(&rb)),
954                BitVecOp::Add => Dynamic::from_ast(&lb.bvadd(&rb)),
955                BitVecOp::Sub => Dynamic::from_ast(&lb.bvsub(&rb)),
956                BitVecOp::Mul => Dynamic::from_ast(&lb.bvmul(&rb)),
957                BitVecOp::SDiv => Dynamic::from_ast(&lb.bvsdiv(&rb)),
958                BitVecOp::SRem => Dynamic::from_ast(&lb.bvsrem(&rb)),
959                BitVecOp::ULt => Dynamic::from_ast(&lb.bvult(&rb)),
960                BitVecOp::SLt => Dynamic::from_ast(&lb.bvslt(&rb)),
961                BitVecOp::ULe => Dynamic::from_ast(&lb.bvule(&rb)),
962                BitVecOp::SLe => Dynamic::from_ast(&lb.bvsle(&rb)),
963                BitVecOp::Eq => Dynamic::from_ast(&lb.eq(&rb)),
964            }
965        } else {
966            l
967        }
968    }
969
970    /// Encode as a Z3 Bool, coercing if necessary.
971    pub fn encode_as_bool(&self, expr: &VerifyExpr) -> Bool {
972        let dyn_expr = self.encode(expr);
973        dyn_expr.as_bool().unwrap_or_else(|| {
974            // If we got an Int or other type, it can't be directly used as Bool.
975            // Fail closed: false, not true. Unsupported constructs must NOT
976            // silently become equivalent to anything (Sprint 0A consistency).
977            Bool::from_bool(false)
978        })
979    }
980}
981
982/// Extract a counterexample trace from a Z3 model.
983fn extract_trace(
984    model: &z3::Model,
985    signals: &[String],
986    bound: usize,
987    bool_vars: &HashMap<String, Bool>,
988    int_vars: &HashMap<String, Int>,
989    bv_vars: &HashMap<String, z3::ast::BV>,
990) -> Trace {
991    let mut cycles = Vec::new();
992    for t in 0..=bound {
993        let mut signal_values = HashMap::new();
994        for sig in signals {
995            let var_name = format!("{}@{}", sig, t);
996            // Try bitvector first, then int, then bool
997            if let Some(z3_var) = bv_vars.get(&var_name) {
998                if let Some(eval) = model.eval(z3_var, true) {
999                    let val = eval.as_u64().unwrap_or(0);
1000                    let width = z3_var.get_size();
1001                    signal_values.insert(sig.clone(), SignalValue::BitVec { width, value: val });
1002                }
1003                continue;
1004            }
1005            if let Some(z3_var) = int_vars.get(&var_name) {
1006                if let Some(eval) = model.eval(z3_var, true) {
1007                    if let Some(n) = eval.as_i64() {
1008                        signal_values.insert(sig.clone(), SignalValue::Int(n));
1009                    }
1010                }
1011                continue;
1012            }
1013            if let Some(z3_var) = bool_vars.get(&var_name) {
1014                let value = model.eval(z3_var, true)
1015                    .and_then(|v| v.as_bool())
1016                    .unwrap_or(false);
1017                signal_values.insert(sig.clone(), SignalValue::Bool(value));
1018            }
1019        }
1020        if !signal_values.is_empty() {
1021            cycles.push(CycleState {
1022                cycle: t,
1023                signals: signal_values,
1024            });
1025        }
1026    }
1027    Trace { cycles }
1028}
logicaffeine_verify/equivalence.rs

logicaffeine_verify/
equivalence.rs
