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 equivalent to adc x y false.

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/BitVec.lean.

Preliminaries

Addition

def Std.BitVec.carry (w : Nat) (x : Nat) (y : Nat) (c : Bool) : Bool

carry w x y c returns true if the w carry bit is true when computing x + y + c.

Equations

• Std.BitVec.carry w x y c = decide (x % 2 ^ w + y % 2 ^ w + Bool.toNat c ≥ 2 ^ w)

@[simp]

theorem Std.BitVec.carry_zero {x : Nat} {y : Nat} {c : Bool} : Std.BitVec.carry 0 x y c = c

def Std.BitVec.adcb (x : Bool) (y : Bool) (c : Bool) : Bool × Bool

Carry function for bitwise addition.

Equations

• Std.BitVec.adcb x y c = (x && y || x && c || y && c, Bool.xor x (Bool.xor y c))

def Std.BitVec.adc {w : Nat} (x : Std.BitVec w) (y : Std.BitVec w) : Bool → Bool × Std.BitVec w

Bitwise addition implemented via a ripple carry adder.

Equations

• Std.BitVec.adc x y = Std.BitVec.iunfoldr fun (i : Fin w) (c : Bool) => Std.BitVec.adcb (Std.BitVec.getLsb x i.val) (Std.BitVec.getLsb y i.val) c

theorem Std.BitVec.adc_overflow_limit (x : Nat) (y : Nat) (i : Nat) (c : Bool) : x % 2 ^ i + (y % 2 ^ i + Bool.toNat c) < 2 ^ (i + 1)

theorem Std.BitVec.carry_succ (w : Nat) (x : Nat) (y : Nat) (c : Bool) : Std.BitVec.carry (Nat.succ w) x y c = decide (Bool.toNat (Nat.testBit x w) + Bool.toNat (Nat.testBit y w) + Bool.toNat (Std.BitVec.carry w x y c) ≥ 2)

theorem Std.BitVec.adc_value_step {w : Nat} {i : Nat} (i_lt : i < w) (x : Std.BitVec w) (y : Std.BitVec w) (c : Bool) : Std.BitVec.getLsb (x + y + Std.BitVec.zeroExtend w (Std.BitVec.ofBool c)) i = Bool.xor (Std.BitVec.getLsb x i) (Bool.xor (Std.BitVec.getLsb y i) (Std.BitVec.carry i (Std.BitVec.toNat x) (Std.BitVec.toNat y) c))

theorem Std.BitVec.adc_correct {w : Nat} (x : Std.BitVec w) (y : Std.BitVec w) (c : Bool) : Std.BitVec.adc x y c = (Std.BitVec.carry w (Std.BitVec.toNat x) (Std.BitVec.toNat y) c, x + y + Std.BitVec.zeroExtend w (Std.BitVec.ofBool c))

theorem Std.BitVec.add_as_adc (w : Nat) (x : Std.BitVec w) (y : Std.BitVec w) : x + y = (Std.BitVec.adc x y false).snd