Bitblasting of bitvectors #
This module provides theorems for showing the equivalence between BitVec operations using
the Fin 2^n
representation and Boolean vectors. It is still under development, but
intended to provide a path for converting SAT and SMT solver proofs about BitVectors
as vectors of bits into proofs about Lean BitVec
values.
The module is named for the bit-blasting operation in an SMT solver that converts bitvector expressions into expressions about individual bits in each vector.
Main results #
x + y : BitVec w
is(adc x y false).2
.
Future work #
All other operations are to be PR'ed later and are already proved in https://github.com/mhk119/lean-smt/blob/bitvec/Smt/Data/Bitwise.lean.
Preliminaries #
Addition #
Carry function for bitwise addition.
Equations
- BitVec.adcb x y c = (x.atLeastTwo y c, x.xor (y.xor c))
Instances For
Bitwise addition implemented via a ripple carry adder.
Equations
- x.adc y = BitVec.iunfoldr fun (i : Fin w) (c : Bool) => BitVec.adcb (x.getLsb ↑i) (y.getLsb ↑i) c
Instances For
add #
Adding a bitvector to its own complement yields the all ones bitpattern
Subtracting x
from the all ones bitvector is equivalent to taking its complement