Module bitblast 

Bit-blasting: BoundedExpr datapath (bitvector) operations → boolean ProofExpr.

A bitvector is represented LSB-first as a Vec<Bit>, each Bit either a known constant or a boolean ProofExpr (a signal bit name#i, or a gate). Every combinator constant-folds, so a constant operand collapses gates instead of emitting them — the CNF stays small. Each operation is the textbook circuit: ripple-carry add/sub, array multiplier, barrel shifters, magnitude/signed comparators, slice and concat.

This is the data-path half of the certified-prover seam: combined with the Boolean lowering in super::sva_to_proof, multi-bit hardware obligations reduce to a propositional formula our CDCL→RUP tiers discharge — in the browser, no Z3.

Functions

lower_bool

Lower a boolean-VALUED datapath comparison to a ProofExpr, or None if unsupported. Comparisons over bitvectors are unsigned unless the op is explicitly signed (SLt).