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.

@[inline, reducible]

abbrev Bool.atLeastTwo (a : Bool) (b : Bool) (c : Bool) : Bool

At least two out of three booleans are true.

Equations

• Bool.atLeastTwo a b c = (a && b || a && c || b && c)

@[simp]

theorem Bool.atLeastTwo_false_left {b : Bool} {c : Bool} : Bool.atLeastTwo false b c = (b && c)

@[simp]

theorem Bool.atLeastTwo_false_mid {a : Bool} {c : Bool} : Bool.atLeastTwo a false c = (a && c)

@[simp]

theorem Bool.atLeastTwo_false_right {a : Bool} {b : Bool} : Bool.atLeastTwo a b false = (a && b)

@[simp]

theorem Bool.atLeastTwo_true_left {b : Bool} {c : Bool} : Bool.atLeastTwo true b c = (b || c)

@[simp]

theorem Bool.atLeastTwo_true_mid {a : Bool} {c : Bool} : Bool.atLeastTwo a true c = (a || c)

@[simp]

theorem Bool.atLeastTwo_true_right {a : Bool} {b : Bool} : Bool.atLeastTwo a b true = (a || b)

Preliminaries

Addition

def BitVec.carry {w : Nat} (i : Nat) (x : BitVec w) (y : BitVec w) (c : Bool) : Bool

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

Equations

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

@[simp]

theorem BitVec.carry_zero : ∀ {w : Nat} {x y : BitVec w} {c : Bool}, BitVec.carry 0 x y c = c

theorem BitVec.carry_succ {w : Nat} (i : Nat) (x : BitVec w) (y : BitVec w) (c : Bool) : BitVec.carry (i + 1) x y c = Bool.atLeastTwo (BitVec.getLsb x i) (BitVec.getLsb y i) (BitVec.carry i x y c)

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

Carry function for bitwise addition.

Equations

• BitVec.adcb x y c = (Bool.atLeastTwo x y c, Bool.xor x (Bool.xor y c))

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

Bitwise addition implemented via a ripple carry adder.

Equations

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

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

theorem BitVec.getLsb_add {w : Nat} {i : Nat} (i_lt : i < w) (x : BitVec w) (y : BitVec w) : BitVec.getLsb (x + y) i = Bool.xor (BitVec.getLsb x i) (Bool.xor (BitVec.getLsb y i) (BitVec.carry i x y false))

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

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

add

@[simp]

theorem BitVec.add_not_self {w : Nat} (x : BitVec w) : x + ~~~x = BitVec.allOnes w

Adding a bitvector to its own complement yields the all ones bitpattern

theorem BitVec.allOnes_sub_eq_not {w : Nat} (x : BitVec w) : BitVec.allOnes w - x = ~~~x

Subtracting x from the all ones bitvector is equivalent to taking its complement