logicaffeine_compile/codegen_sva/
bitblast.rs

1//! Bit-blasting: `BoundedExpr` datapath (bitvector) operations → boolean `ProofExpr`.
2//!
3//! A bitvector is represented LSB-first as a `Vec<Bit>`, each `Bit` either a known constant
4//! or a boolean `ProofExpr` (a signal bit `name#i`, or a gate). Every combinator
5//! constant-folds, so a constant operand collapses gates instead of emitting them — the CNF
6//! stays small. Each operation is the textbook circuit: ripple-carry add/sub, array
7//! multiplier, barrel shifters, magnitude/signed comparators, slice and concat.
8//!
9//! This is the data-path half of the certified-prover seam: combined with the Boolean
10//! lowering in [`super::sva_to_proof`], multi-bit hardware obligations reduce to a
11//! propositional formula our CDCL→RUP tiers discharge — in the browser, no Z3.
12
13use super::sva_to_verify::{BitVecBoundedOp, BoundedExpr, CmpBoundedOp};
14use logicaffeine_proof::ProofExpr;
15
16/// One blasted bit: a known constant, or a boolean `ProofExpr`.
17#[derive(Clone)]
18enum Bit {
19    Const(bool),
20    Dyn(ProofExpr),
21}
22
23fn b_not(x: Bit) -> Bit {
24    match x {
25        Bit::Const(c) => Bit::Const(!c),
26        Bit::Dyn(e) => Bit::Dyn(ProofExpr::Not(Box::new(e))),
27    }
28}
29
30fn b_and(a: Bit, b: Bit) -> Bit {
31    match (a, b) {
32        (Bit::Const(false), _) | (_, Bit::Const(false)) => Bit::Const(false),
33        (Bit::Const(true), y) | (y, Bit::Const(true)) => y,
34        (Bit::Dyn(x), Bit::Dyn(y)) => Bit::Dyn(ProofExpr::And(Box::new(x), Box::new(y))),
35    }
36}
37
38fn b_or(a: Bit, b: Bit) -> Bit {
39    match (a, b) {
40        (Bit::Const(true), _) | (_, Bit::Const(true)) => Bit::Const(true),
41        (Bit::Const(false), y) | (y, Bit::Const(false)) => y,
42        (Bit::Dyn(x), Bit::Dyn(y)) => Bit::Dyn(ProofExpr::Or(Box::new(x), Box::new(y))),
43    }
44}
45
46/// XNOR / equality of two bits.
47fn b_iff(a: Bit, b: Bit) -> Bit {
48    match (a, b) {
49        (Bit::Const(c), Bit::Const(d)) => Bit::Const(c == d),
50        (Bit::Const(true), y) | (y, Bit::Const(true)) => y,
51        (Bit::Const(false), y) | (y, Bit::Const(false)) => b_not(y),
52        (Bit::Dyn(x), Bit::Dyn(y)) => Bit::Dyn(ProofExpr::Iff(Box::new(x), Box::new(y))),
53    }
54}
55
56fn b_xor(a: Bit, b: Bit) -> Bit {
57    b_not(b_iff(a, b))
58}
59
60/// If-then-else (a 1-bit mux): `s ? t : e`.
61fn b_ite(s: Bit, t: Bit, e: Bit) -> Bit {
62    match s {
63        Bit::Const(true) => t,
64        Bit::Const(false) => e,
65        s => b_or(b_and(s.clone(), t), b_and(b_not(s), e)),
66    }
67}
68
69fn bit_to_proof(b: Bit) -> ProofExpr {
70    match b {
71        // `ProofExpr` has no Boolean literal; encode constants as a tautology / contradiction
72        // over a reserved atom (`Or(c,¬c)` is always true, `And(c,¬c)` always false).
73        Bit::Const(true) => {
74            let c = ProofExpr::Atom("__bit_const".to_string());
75            ProofExpr::Or(Box::new(c.clone()), Box::new(ProofExpr::Not(Box::new(c))))
76        }
77        Bit::Const(false) => {
78            let c = ProofExpr::Atom("__bit_const".to_string());
79            ProofExpr::And(Box::new(c.clone()), Box::new(ProofExpr::Not(Box::new(c))))
80        }
81        Bit::Dyn(e) => e,
82    }
83}
84
85// ── Bitvector circuits (operands LSB-first, equal width) ────────────────────────────────
86
87/// Ripple-carry add: returns `(sum bits, carry-out)`.
88fn ripple_add(a: &[Bit], b: &[Bit], carry_in: Bit) -> (Vec<Bit>, Bit) {
89    let mut carry = carry_in;
90    let mut out = Vec::with_capacity(a.len());
91    for i in 0..a.len() {
92        let axb = b_xor(a[i].clone(), b[i].clone());
93        let sum = b_xor(axb.clone(), carry.clone());
94        let carry_next = b_or(
95            b_and(a[i].clone(), b[i].clone()),
96            b_and(carry.clone(), axb),
97        );
98        out.push(sum);
99        carry = carry_next;
100    }
101    (out, carry)
102}
103
104fn bv_add(a: &[Bit], b: &[Bit]) -> Vec<Bit> {
105    ripple_add(a, b, Bit::Const(false)).0
106}
107
108/// Two's-complement subtract: `a - b = a + ¬b + 1`.
109fn bv_sub(a: &[Bit], b: &[Bit]) -> Vec<Bit> {
110    let nb: Vec<Bit> = b.iter().cloned().map(b_not).collect();
111    ripple_add(a, &nb, Bit::Const(true)).0
112}
113
114/// Shift-and-add array multiplier, truncated to the operand width.
115fn bv_mul(a: &[Bit], b: &[Bit]) -> Vec<Bit> {
116    let w = a.len();
117    let mut acc: Vec<Bit> = vec![Bit::Const(false); w];
118    for i in 0..w {
119        // Partial product: (a << i) gated by b[i], truncated to width w.
120        let mut pp: Vec<Bit> = vec![Bit::Const(false); w];
121        for j in i..w {
122            pp[j] = b_and(a[j - i].clone(), b[i].clone());
123        }
124        acc = bv_add(&acc, &pp);
125    }
126    acc
127}
128
129/// Shift left by a constant `k` (zero-fill), width-preserving.
130fn shl_const(a: &[Bit], k: usize) -> Vec<Bit> {
131    let w = a.len();
132    (0..w)
133        .map(|j| if j >= k { a[j - k].clone() } else { Bit::Const(false) })
134        .collect()
135}
136
137/// Shift right by a constant `k`, filling the vacated top bits with `fill`.
138fn shr_const(a: &[Bit], k: usize, fill: Bit) -> Vec<Bit> {
139    let w = a.len();
140    (0..w)
141        .map(|j| if j + k < w { a[j + k].clone() } else { fill.clone() })
142        .collect()
143}
144
145/// Barrel shifter for a variable amount: compose constant shifts of `1<<s` gated by the
146/// amount's bit `s`. `fill` is the vacated-bit value (0 for logical, sign for arithmetic);
147/// `left` selects direction.
148fn barrel_shift(a: &[Bit], amount: &[Bit], left: bool, fill: Bit) -> Vec<Bit> {
149    let w = a.len();
150    let mut cur = a.to_vec();
151    for (s, amt_bit) in amount.iter().enumerate() {
152        let dist = 1usize << s;
153        if dist >= w {
154            // Any set bit at or beyond this position shifts everything out.
155            let shifted = vec![fill.clone(); w];
156            cur = (0..w)
157                .map(|j| b_ite(amt_bit.clone(), shifted[j].clone(), cur[j].clone()))
158                .collect();
159            continue;
160        }
161        let shifted = if left {
162            shl_const(&cur, dist)
163        } else {
164            shr_const(&cur, dist, fill.clone())
165        };
166        cur = (0..w)
167            .map(|j| b_ite(amt_bit.clone(), shifted[j].clone(), cur[j].clone()))
168            .collect();
169    }
170    cur
171}
172
173/// `a == b` over equal-width bitvectors → a single bit.
174fn bv_eq(a: &[Bit], b: &[Bit]) -> Bit {
175    let mut acc = Bit::Const(true);
176    for i in 0..a.len() {
177        acc = b_and(acc, b_iff(a[i].clone(), b[i].clone()));
178    }
179    acc
180}
181
182/// Unsigned `a < b` → a single bit (LSB→MSB magnitude comparator).
183fn bv_ult(a: &[Bit], b: &[Bit]) -> Bit {
184    let mut lt = Bit::Const(false);
185    for i in 0..a.len() {
186        // a<b on bits 0..=i  ≡  (a[i]<b[i]) ∨ (a[i]=b[i] ∧ a<b on bits below i)
187        let bit_lt = b_and(b_not(a[i].clone()), b[i].clone());
188        let bit_eq = b_iff(a[i].clone(), b[i].clone());
189        lt = b_or(bit_lt, b_and(bit_eq, lt));
190    }
191    lt
192}
193
194/// Signed (two's-complement) `a < b` → a single bit.
195fn bv_slt(a: &[Bit], b: &[Bit]) -> Bit {
196    let w = a.len();
197    let sa = a[w - 1].clone();
198    let sb = b[w - 1].clone();
199    // Differing signs: the negative one (sign bit 1) is smaller, so result = a's sign.
200    // Same sign: the unsigned ordering coincides with the signed ordering.
201    b_ite(b_xor(sa.clone(), sb), sa, bv_ult(a, b))
202}
203
204// ── BoundedExpr → bits / bool ───────────────────────────────────────────────────────────
205
206/// Blast a bitvector-VALUED `BoundedExpr` into its bits (LSB-first), or `None` if it is not a
207/// supported bitvector expression (e.g. an Int, a comparison, or mismatched widths).
208fn blast_bits(e: &BoundedExpr) -> Option<Vec<Bit>> {
209    match e {
210        BoundedExpr::BitVecConst { width, value } => {
211            Some((0..*width).map(|i| Bit::Const((value >> i) & 1 == 1)).collect())
212        }
213        BoundedExpr::BitVecVar(name, width) => Some(
214            (0..*width)
215                .map(|i| Bit::Dyn(ProofExpr::Atom(format!("{name}#{i}"))))
216                .collect(),
217        ),
218        BoundedExpr::BitVecExtract { high, low, operand } => {
219            let bits = blast_bits(operand)?;
220            let (lo, hi) = (*low as usize, *high as usize);
221            if hi >= bits.len() || lo > hi {
222                return None;
223            }
224            Some(bits[lo..=hi].to_vec())
225        }
226        BoundedExpr::BitVecConcat(a, b) => {
227            // SVA `{a, b}`: `a` is the high half. LSB-first ⇒ b's bits then a's bits.
228            let mut bits = blast_bits(b)?;
229            bits.extend(blast_bits(a)?);
230            Some(bits)
231        }
232        BoundedExpr::BitVecBinary { op, left, right } => {
233            let a = blast_bits(left)?;
234            let b = blast_bits(right)?;
235            match op {
236                BitVecBoundedOp::Not => Some(a.into_iter().map(b_not).collect()),
237                // Width-preserving binary circuits require matching widths.
238                _ if a.len() != b.len() => None,
239                BitVecBoundedOp::And => Some(zip_map(a, b, b_and)),
240                BitVecBoundedOp::Or => Some(zip_map(a, b, b_or)),
241                BitVecBoundedOp::Xor => Some(zip_map(a, b, b_xor)),
242                BitVecBoundedOp::Add => Some(bv_add(&a, &b)),
243                BitVecBoundedOp::Sub => Some(bv_sub(&a, &b)),
244                BitVecBoundedOp::Mul => Some(bv_mul(&a, &b)),
245                BitVecBoundedOp::Shl => Some(barrel_shift(&a, &b, true, Bit::Const(false))),
246                BitVecBoundedOp::Shr => Some(barrel_shift(&a, &b, false, Bit::Const(false))),
247                BitVecBoundedOp::AShr => {
248                    let sign = a[a.len() - 1].clone();
249                    Some(barrel_shift(&a, &b, false, sign))
250                }
251                // Comparison ops are boolean-valued — not a bit vector.
252                BitVecBoundedOp::Eq | BitVecBoundedOp::ULt | BitVecBoundedOp::SLt => None,
253            }
254        }
255        _ => None,
256    }
257}
258
259fn zip_map(a: Vec<Bit>, b: Vec<Bit>, f: fn(Bit, Bit) -> Bit) -> Vec<Bit> {
260    a.into_iter().zip(b).map(|(x, y)| f(x, y)).collect()
261}
262
263/// Lower a boolean-VALUED datapath comparison to a `ProofExpr`, or `None` if unsupported.
264/// Comparisons over bitvectors are unsigned unless the op is explicitly signed (`SLt`).
265pub fn lower_bool(e: &BoundedExpr) -> Option<ProofExpr> {
266    let bit = match e {
267        BoundedExpr::BitVecBinary { op, left, right } => {
268            let a = blast_bits(left)?;
269            let b = blast_bits(right)?;
270            if a.len() != b.len() {
271                return None;
272            }
273            match op {
274                BitVecBoundedOp::Eq => bv_eq(&a, &b),
275                BitVecBoundedOp::ULt => bv_ult(&a, &b),
276                BitVecBoundedOp::SLt => bv_slt(&a, &b),
277                _ => return None,
278            }
279        }
280        BoundedExpr::Eq(l, r) => {
281            let a = blast_bits(l)?;
282            let b = blast_bits(r)?;
283            if a.len() != b.len() {
284                return None;
285            }
286            bv_eq(&a, &b)
287        }
288        BoundedExpr::Lt(l, r) | BoundedExpr::Gt(l, r) | BoundedExpr::Lte(l, r)
289        | BoundedExpr::Gte(l, r) => bv_compare(e, l, r)?,
290        BoundedExpr::Comparison { op, left, right } => {
291            let a = blast_bits(left)?;
292            let b = blast_bits(right)?;
293            if a.len() != b.len() {
294                return None;
295            }
296            match op {
297                CmpBoundedOp::Lt => bv_ult(&a, &b),
298                CmpBoundedOp::Gt => bv_ult(&b, &a),
299                CmpBoundedOp::Lte => b_not(bv_ult(&b, &a)),
300                CmpBoundedOp::Gte => b_not(bv_ult(&a, &b)),
301            }
302        }
303        _ => return None,
304    };
305    Some(bit_to_proof(bit))
306}
307
308/// Unsigned magnitude comparison for the top-level `Lt/Gt/Lte/Gte` BoundedExpr variants.
309fn bv_compare(e: &BoundedExpr, l: &BoundedExpr, r: &BoundedExpr) -> Option<Bit> {
310    let a = blast_bits(l)?;
311    let b = blast_bits(r)?;
312    if a.len() != b.len() {
313        return None;
314    }
315    Some(match e {
316        BoundedExpr::Lt(..) => bv_ult(&a, &b),
317        BoundedExpr::Gt(..) => bv_ult(&b, &a),
318        BoundedExpr::Lte(..) => b_not(bv_ult(&b, &a)),
319        BoundedExpr::Gte(..) => b_not(bv_ult(&a, &b)),
320        _ => return None,
321    })
322}
323
324#[cfg(test)]
325mod tests {
326    use super::*;
327    use logicaffeine_proof::sat::{prove_unsat, UnsatOutcome};
328
329    const W: u32 = 4;
330    const MASK: u64 = (1 << W) - 1;
331
332    fn konst(v: u64) -> BoundedExpr {
333        BoundedExpr::BitVecConst { width: W, value: v & MASK }
334    }
335    fn bv_bin(op: BitVecBoundedOp, a: u64, b: u64) -> BoundedExpr {
336        BoundedExpr::BitVecBinary { op, left: Box::new(konst(a)), right: Box::new(konst(b)) }
337    }
338    /// A constant boolean expression is a tautology — assert it via certified UNSAT of its
339    /// negation. `expect` says whether it should be a tautology or a contradiction.
340    fn assert_bool(e: &BoundedExpr, expect_true: bool) {
341        let p = lower_bool(e).expect("lowered to a boolean");
342        if expect_true {
343            assert_eq!(prove_unsat(&ProofExpr::Not(Box::new(p))), UnsatOutcome::Refuted);
344        } else {
345            assert_eq!(prove_unsat(&p), UnsatOutcome::Refuted);
346        }
347    }
348    /// Assert a bitvector op equals an integer-oracle result, exactly (and that off-by-one is
349    /// rejected), by lowering `op(a,b) == expected` and `== expected+1`.
350    fn assert_bv(op: BitVecBoundedOp, a: u64, b: u64, expected: u64) {
351        let eq = BoundedExpr::Eq(Box::new(bv_bin(op.clone(), a, b)), Box::new(konst(expected)));
352        assert_bool(&eq, true);
353        let neq =
354            BoundedExpr::Eq(Box::new(bv_bin(op, a, b)), Box::new(konst(expected.wrapping_add(1))));
355        assert_bool(&neq, false);
356    }
357
358    #[test]
359    fn add_sub_mul_match_integer_oracle_exhaustively() {
360        for a in 0..=MASK {
361            for b in 0..=MASK {
362                assert_bv(BitVecBoundedOp::Add, a, b, (a + b) & MASK);
363                assert_bv(BitVecBoundedOp::Sub, a, b, a.wrapping_sub(b) & MASK);
364                assert_bv(BitVecBoundedOp::Mul, a, b, (a * b) & MASK);
365            }
366        }
367    }
368
369    #[test]
370    fn bitwise_ops_match_oracle_exhaustively() {
371        for a in 0..=MASK {
372            for b in 0..=MASK {
373                assert_bv(BitVecBoundedOp::And, a, b, a & b);
374                assert_bv(BitVecBoundedOp::Or, a, b, a | b);
375                assert_bv(BitVecBoundedOp::Xor, a, b, a ^ b);
376            }
377        }
378        // NOT is unary: ¬a over the width.
379        for a in 0..=MASK {
380            let e = BoundedExpr::Eq(
381                Box::new(BoundedExpr::BitVecBinary {
382                    op: BitVecBoundedOp::Not,
383                    left: Box::new(konst(a)),
384                    right: Box::new(konst(0)),
385                }),
386                Box::new(konst(!a & MASK)),
387            );
388            assert_bool(&e, true);
389        }
390    }
391
392    #[test]
393    fn shifts_match_oracle_exhaustively() {
394        for a in 0..=MASK {
395            for s in 0..=MASK {
396                let sh = (s & MASK) as u32;
397                let shl = if sh < W { (a << sh) & MASK } else { 0 };
398                assert_bv(BitVecBoundedOp::Shl, a, s, shl);
399                let shr = if sh < W { (a & MASK) >> sh } else { 0 };
400                assert_bv(BitVecBoundedOp::Shr, a, s, shr);
401                // Arithmetic shift right: sign-extend the top bit.
402                let sign = (a >> (W - 1)) & 1 == 1;
403                let ashr = if sh >= W {
404                    if sign { MASK } else { 0 }
405                } else {
406                    let base = (a & MASK) >> sh;
407                    if sign {
408                        base | (MASK & !((1 << (W - sh)) - 1))
409                    } else {
410                        base
411                    }
412                };
413                assert_bv(BitVecBoundedOp::AShr, a, s, ashr & MASK);
414            }
415        }
416    }
417
418    #[test]
419    fn comparisons_match_oracle_exhaustively() {
420        for a in 0..=MASK {
421            for b in 0..=MASK {
422                assert_bool(&bv_bin(BitVecBoundedOp::Eq, a, b), a == b);
423                assert_bool(&bv_bin(BitVecBoundedOp::ULt, a, b), a < b);
424                // Signed interpretation over W bits (two's complement).
425                let sa = sign_extend(a);
426                let sb = sign_extend(b);
427                assert_bool(&bv_bin(BitVecBoundedOp::SLt, a, b), sa < sb);
428                // Top-level unsigned comparisons.
429                assert_bool(&BoundedExpr::Lt(Box::new(konst(a)), Box::new(konst(b))), a < b);
430                assert_bool(&BoundedExpr::Gte(Box::new(konst(a)), Box::new(konst(b))), a >= b);
431            }
432        }
433    }
434
435    fn sign_extend(v: u64) -> i64 {
436        let v = (v & MASK) as i64;
437        if (v >> (W - 1)) & 1 == 1 {
438            v - (1 << W)
439        } else {
440            v
441        }
442    }
443
444    #[test]
445    fn extract_and_concat_match_oracle() {
446        // extract [2:1] of a 4-bit constant.
447        for a in 0..=MASK {
448            let ex = BoundedExpr::BitVecExtract {
449                high: 2,
450                low: 1,
451                operand: Box::new(konst(a)),
452            };
453            let expected = (a >> 1) & 0b11;
454            let e = BoundedExpr::Eq(
455                Box::new(ex),
456                Box::new(BoundedExpr::BitVecConst { width: 2, value: expected }),
457            );
458            assert_bool(&e, true);
459        }
460        // concat {a(2b), b(2b)} == a<<2 | b, width 4.
461        for a in 0..4 {
462            for b in 0..4 {
463                let cc = BoundedExpr::BitVecConcat(
464                    Box::new(BoundedExpr::BitVecConst { width: 2, value: a }),
465                    Box::new(BoundedExpr::BitVecConst { width: 2, value: b }),
466                );
467                let e = BoundedExpr::Eq(Box::new(cc), Box::new(konst((a << 2) | b)));
468                assert_bool(&e, true);
469            }
470        }
471    }
472
473    #[test]
474    fn datapath_equivalence_over_variables() {
475        // x + y ≡ y + x (commutativity), proven over all 4-bit x,y by our certified prover.
476        let x = || Box::new(BoundedExpr::BitVecVar("x".to_string(), W));
477        let y = || Box::new(BoundedExpr::BitVecVar("y".to_string(), W));
478        let xy = BoundedExpr::BitVecBinary { op: BitVecBoundedOp::Add, left: x(), right: y() };
479        let yx = BoundedExpr::BitVecBinary { op: BitVecBoundedOp::Add, left: y(), right: x() };
480        let eq = BoundedExpr::Eq(Box::new(xy), Box::new(yx));
481        let p = lower_bool(&eq).unwrap();
482        assert_eq!(prove_unsat(&ProofExpr::Not(Box::new(p))), UnsatOutcome::Refuted);
483    }
484
485    #[test]
486    fn rotl_is_a_bit_permutation_at_full_32_bits() {
487        // The word-width proof wall closes: rotl over the FULL 32-bit width is proven a
488        // bit-permutation (injective) by our OWN certified CDCL — no Z3, and not a ≤16-bit
489        // exhaustive sample. rotl is pure wiring, so plain `prove_unsat` discharges it; the
490        // lex-leader symmetry-breaking layer (`logicaffeine_proof::symmetry`) is the lever
491        // reserved for the carry-heavy datapaths (wide add/mul) whose CNF would blow up.
492        const WW: u32 = 32;
493        // rotl(name, k) = (v << k) | (v >> (32 - k)) over a fresh 32-bit variable `name`.
494        fn rotl(name: &str, k: u32) -> BoundedExpr {
495            let v = || Box::new(BoundedExpr::BitVecVar(name.to_string(), WW));
496            let kc = |s: u32| Box::new(BoundedExpr::BitVecConst { width: WW, value: s as u64 });
497            let hi = Box::new(BoundedExpr::BitVecBinary { op: BitVecBoundedOp::Shl, left: v(), right: kc(k) });
498            let lo =
499                Box::new(BoundedExpr::BitVecBinary { op: BitVecBoundedOp::Shr, left: v(), right: kc(WW - k) });
500            BoundedExpr::BitVecBinary { op: BitVecBoundedOp::Or, left: hi, right: lo }
501        }
502        let var = |n: &str| Box::new(BoundedExpr::BitVecVar(n.to_string(), WW));
503
504        // The ChaCha20 rotation amounts — the ones the quarter-round actually uses.
505        for k in [7u32, 8, 12, 16] {
506            // Injectivity: rotl(x,k) == rotl(y,k)  ⟹  x == y. The counterexample (equal
507            // rotations, unequal inputs) must be REFUTED over all 32-bit inputs.
508            let eq_rot = lower_bool(&BoundedExpr::Eq(Box::new(rotl("x", k)), Box::new(rotl("y", k))))
509                .expect("rotation equality lowered");
510            let eq_in = lower_bool(&BoundedExpr::Eq(var("x"), var("y"))).expect("input equality lowered");
511            let counter = ProofExpr::And(Box::new(eq_rot), Box::new(ProofExpr::Not(Box::new(eq_in))));
512            assert_eq!(
513                prove_unsat(&counter),
514                UnsatOutcome::Refuted,
515                "rotl by {k} must be injective (a bit-permutation) over all 32-bit inputs"
516            );
517        }
518
519        // Non-vacuity: a NON-permutation (`x & 0`, which collapses every input to 0) must NOT
520        // be refuted — distinct inputs with equal images genuinely exist, so a sound prover
521        // finds the counterexample rather than vacuously "proving" injectivity.
522        let zero_and = |n: &str| BoundedExpr::BitVecBinary {
523            op: BitVecBoundedOp::And,
524            left: Box::new(BoundedExpr::BitVecVar(n.to_string(), WW)),
525            right: Box::new(BoundedExpr::BitVecConst { width: WW, value: 0 }),
526        };
527        let eq_img = lower_bool(&BoundedExpr::Eq(Box::new(zero_and("x")), Box::new(zero_and("y"))))
528            .expect("image equality lowered");
529        let eq_in = lower_bool(&BoundedExpr::Eq(var("x"), var("y"))).expect("input equality lowered");
530        let counter = ProofExpr::And(Box::new(eq_img), Box::new(ProofExpr::Not(Box::new(eq_in))));
531        assert_ne!(
532            prove_unsat(&counter),
533            UnsatOutcome::Refuted,
534            "x & 0 is NOT injective — the prover must not vacuously refute its counterexample"
535        );
536    }
537}
logicaffeine_compile/codegen_sva/bitblast.rs

logicaffeine_compile/codegen_sva/
bitblast.rs
