logicaffeine_verify/
parameterized.rs

1//! Parameterized Verification
2//!
3//! Verify properties for any bus width N, any FIFO depth D, etc.
4//! Uses Z3 quantifiers: forall N:Int. N > 0 -> property(N).
5
6use crate::ir::{VerifyExpr, VerifyType};
7use crate::equivalence::Trace;
8use std::collections::HashMap;
9
10#[derive(Debug)]
11pub enum ParameterizedResult {
12    UniversallyValid,
13    ValidUpTo(u64),
14    Counterexample { param_value: u64, trace: Trace },
15    Unknown,
16}
17
18/// Verify a parameterized property.
19///
20/// Uses Z3 quantifiers to check: forall param. constraint(param) -> property(param).
21/// Falls back to bounded enumeration if quantifier reasoning times out.
22pub fn verify_parameterized(
23    property: &VerifyExpr,
24    parameter: &str,
25    param_type: VerifyType,
26    constraint: Option<&VerifyExpr>,
27) -> ParameterizedResult {
28
29    // Build: forall param. constraint(param) -> property(param)
30    let body = if let Some(c) = constraint {
31        VerifyExpr::implies(c.clone(), property.clone())
32    } else {
33        property.clone()
34    };
35
36    let quantified = VerifyExpr::forall(
37        vec![(parameter.to_string(), param_type.clone())],
38        body,
39    );
40
41    // Check: NOT(quantified) is UNSAT means universally valid
42    let negated = VerifyExpr::not(quantified);
43    let solver = crate::solver::new_solver();
44    let encoded = encode_bool(&negated);
45    solver.assert(&encoded);
46
47    match solver.check() {
48        z3::SatResult::Unsat => ParameterizedResult::UniversallyValid,
49        z3::SatResult::Sat => {
50            // Try bounded enumeration to find specific counterexample
51            for val in 0..=100u64 {
52                let specialized = substitute_param(property, parameter, val as i64);
53                let neg_spec = VerifyExpr::not(specialized);
54                let solver2 = crate::solver::new_solver();
55                solver2.assert(&encode_bool(&neg_spec));
56                if matches!(solver2.check(), z3::SatResult::Sat) {
57                    return ParameterizedResult::Counterexample {
58                        param_value: val,
59                        trace: Trace { cycles: vec![] },
60                    };
61                }
62            }
63            ParameterizedResult::ValidUpTo(100)
64        }
65        z3::SatResult::Unknown => {
66            // Fall back to bounded enumeration
67            for val in 0..=20u64 {
68                let specialized = substitute_param(property, parameter, val as i64);
69                let neg_spec = VerifyExpr::not(specialized);
70                let solver2 = crate::solver::new_solver();
71                solver2.assert(&encode_bool(&neg_spec));
72                if matches!(solver2.check(), z3::SatResult::Sat) {
73                    return ParameterizedResult::Counterexample {
74                        param_value: val,
75                        trace: Trace { cycles: vec![] },
76                    };
77                }
78            }
79            ParameterizedResult::ValidUpTo(20)
80        }
81    }
82}
83
84fn substitute_param(expr: &VerifyExpr, param: &str, value: i64) -> VerifyExpr {
85    match expr {
86        VerifyExpr::Var(name) if name == param => VerifyExpr::Int(value),
87        VerifyExpr::Var(_) => expr.clone(),
88        VerifyExpr::Binary { op, left, right } => VerifyExpr::binary(
89            *op,
90            substitute_param(left, param, value),
91            substitute_param(right, param, value),
92        ),
93        VerifyExpr::Not(inner) => VerifyExpr::not(substitute_param(inner, param, value)),
94        VerifyExpr::Bool(_) | VerifyExpr::Int(_) => expr.clone(),
95        VerifyExpr::Iff(l, r) => VerifyExpr::iff(
96            substitute_param(l, param, value),
97            substitute_param(r, param, value),
98        ),
99        VerifyExpr::ForAll { vars, body } => VerifyExpr::forall(
100            vars.clone(),
101            substitute_param(body, param, value),
102        ),
103        VerifyExpr::Exists { vars, body } => VerifyExpr::exists(
104            vars.clone(),
105            substitute_param(body, param, value),
106        ),
107        _ => expr.clone(),
108    }
109}
110
111fn encode_bool(expr: &VerifyExpr) -> z3::ast::Bool {
112    let mut bool_vars = HashMap::new();
113    let mut int_vars = HashMap::new();
114    let mut all_vars = std::collections::HashSet::new();
115    crate::equivalence::collect_vars_pub(expr, &mut all_vars);
116    for name in &all_vars {
117        bool_vars.insert(name.clone(), z3::ast::Bool::new_const(name.as_str()));
118    }
119    crate::equivalence::collect_int_vars_pub(expr, &mut int_vars);
120    let mut bv_vars = HashMap::new();
121    let mut array_vars = HashMap::new();
122    crate::equivalence::collect_quantifier_bound_vars_pub(expr, &mut int_vars, &mut bv_vars, &mut array_vars);
123    crate::kinduction::encode_expr_bool(expr, &bool_vars, &int_vars)
124}
logicaffeine_verify/parameterized.rs

logicaffeine_verify/
parameterized.rs
