logicaffeine_compile/codegen_sva/
sva_to_proof.rs

1//! Bounded SVA/FOL obligation → `ProofExpr` (the certified-prover seam).
2//!
3//! `BoundedExpr` is an SVA assertion (or Kripke-lowered FOL spec) already unrolled to
4//! discrete timesteps, with each signal-at-time a `signal@t` variable. This module lowers
5//! that bounded obligation into the `logicaffeine_proof::ProofExpr` vocabulary, where the
6//! pure-Rust CDCL → RUP → kernel trust tiers discharge it with a certificate — the very seam
7//! the grid solver uses, and the reason hardware proving runs in the browser with no Z3.
8//!
9//! Boolean (1-bit signal) obligations lower directly. Data-path operands — integers,
10//! bitvectors, arrays, comparisons, quantifiers, uninterpreted applications — return `None`,
11//! signalling that the caller must bit-blast them to the Boolean fragment first (the next
12//! layer). Returning `None` rather than guessing keeps the lowering fail-closed.
13
14use super::sva_to_verify::BoundedExpr;
15use logicaffeine_proof::ProofExpr;
16
17#[inline]
18fn boxed(e: ProofExpr) -> Box<ProofExpr> {
19    Box::new(e)
20}
21
22/// `ProofExpr` has no Boolean-literal node, so the constants are encoded as a tautology /
23/// contradiction over a reserved atom. `Or(c, ¬c)` is true and `And(c, ¬c)` is false
24/// regardless of `c`, so the encoding stays correct even if a signal happened to share the
25/// reserved name.
26fn truth() -> ProofExpr {
27    let c = ProofExpr::Atom("__bool_const".to_string());
28    ProofExpr::Or(boxed(c.clone()), boxed(ProofExpr::Not(boxed(c))))
29}
30fn falsity() -> ProofExpr {
31    let c = ProofExpr::Atom("__bool_const".to_string());
32    ProofExpr::And(boxed(c.clone()), boxed(ProofExpr::Not(boxed(c))))
33}
34
35/// Lower a Boolean-fragment `BoundedExpr` to `ProofExpr`, or `None` for any node outside the
36/// propositional fragment (integers, bitvectors, arrays, ordered comparisons, quantifiers,
37/// uninterpreted applications) — those require bit-blasting, not direct lowering.
38pub fn bounded_to_proof(e: &BoundedExpr) -> Option<ProofExpr> {
39    match e {
40        BoundedExpr::Var(name) => Some(ProofExpr::Atom(name.clone())),
41        BoundedExpr::Bool(true) => Some(truth()),
42        BoundedExpr::Bool(false) => Some(falsity()),
43        BoundedExpr::Not(p) => Some(ProofExpr::Not(boxed(bounded_to_proof(p)?))),
44        BoundedExpr::And(p, q) => {
45            Some(ProofExpr::And(boxed(bounded_to_proof(p)?), boxed(bounded_to_proof(q)?)))
46        }
47        BoundedExpr::Or(p, q) => {
48            Some(ProofExpr::Or(boxed(bounded_to_proof(p)?), boxed(bounded_to_proof(q)?)))
49        }
50        BoundedExpr::Implies(p, q) => {
51            Some(ProofExpr::Implies(boxed(bounded_to_proof(p)?), boxed(bounded_to_proof(q)?)))
52        }
53        // Equality of two Booleans is the biconditional; if either side is not Boolean, fall
54        // back to bit-blasted bitvector equality.
55        BoundedExpr::Eq(p, q) => match (bounded_to_proof(p), bounded_to_proof(q)) {
56            (Some(a), Some(b)) => Some(ProofExpr::Iff(boxed(a), boxed(b))),
57            _ => super::bitblast::lower_bool(e),
58        },
59        // Everything else: try the bit-blaster (datapath comparisons over bitvectors). It
60        // returns `None` for genuinely unsupported nodes (Int arithmetic, quantifiers, …).
61        _ => super::bitblast::lower_bool(e),
62    }
63}
64
65#[cfg(test)]
66mod tests {
67    use super::*;
68    use logicaffeine_proof::sat::{prove_equivalence, EquivOutcome};
69
70    fn v(s: &str) -> BoundedExpr {
71        BoundedExpr::Var(s.to_string())
72    }
73    fn b(e: BoundedExpr) -> Box<BoundedExpr> {
74        Box::new(e)
75    }
76
77    #[test]
78    fn overlapping_implication_proves_equivalent() {
79        // `req |-> ack` at t0, against the same FOL lowering.
80        let sva = BoundedExpr::Implies(b(v("req@0")), b(v("ack@0")));
81        let fol = BoundedExpr::Implies(b(v("req@0")), b(v("ack@0")));
82        let p = bounded_to_proof(&sva).unwrap();
83        let q = bounded_to_proof(&fol).unwrap();
84        assert_eq!(prove_equivalence(&p, &q), EquivOutcome::Equivalent);
85    }
86
87    #[test]
88    fn implication_vs_consequent_differ() {
89        let sva = BoundedExpr::Implies(b(v("req@0")), b(v("ack@0")));
90        let other = v("ack@0");
91        let p = bounded_to_proof(&sva).unwrap();
92        let q = bounded_to_proof(&other).unwrap();
93        match prove_equivalence(&p, &q) {
94            EquivOutcome::Differ(_) => {}
95            o => panic!("expected Differ, got {:?}", o),
96        }
97    }
98
99    #[test]
100    fn safety_demorgan_equivalent() {
101        // `!(a && b)` ≡ `!a || !b` — a real safety-property rewrite.
102        let lhs = BoundedExpr::Not(b(BoundedExpr::And(b(v("a@0")), b(v("b@0")))));
103        let rhs = BoundedExpr::Or(
104            b(BoundedExpr::Not(b(v("a@0")))),
105            b(BoundedExpr::Not(b(v("b@0")))),
106        );
107        let p = bounded_to_proof(&lhs).unwrap();
108        let q = bounded_to_proof(&rhs).unwrap();
109        assert_eq!(prove_equivalence(&p, &q), EquivOutcome::Equivalent);
110    }
111
112    #[test]
113    fn boolean_constants_lower_and_differ() {
114        let t = bounded_to_proof(&BoundedExpr::Bool(true)).unwrap();
115        let f = bounded_to_proof(&BoundedExpr::Bool(false)).unwrap();
116        match prove_equivalence(&t, &f) {
117            EquivOutcome::Differ(_) => {}
118            o => panic!("True vs False must Differ, got {:?}", o),
119        }
120    }
121
122    #[test]
123    fn datapath_returns_none() {
124        // Integers and bitvectors are outside the Boolean fragment → escalate.
125        assert!(bounded_to_proof(&BoundedExpr::Int(5)).is_none());
126        assert!(bounded_to_proof(&BoundedExpr::BitVecVar("data@0".to_string(), 8)).is_none());
127        // …and an ordered comparison built over them.
128        let cmp = BoundedExpr::Lt(b(BoundedExpr::Int(1)), b(BoundedExpr::Int(2)));
129        assert!(bounded_to_proof(&cmp).is_none());
130    }
131}
logicaffeine_compile/codegen_sva/sva_to_proof.rs

logicaffeine_compile/codegen_sva/
sva_to_proof.rs
