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.

@[reducible, inline]

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

At least two out of three booleans are true.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Bool.atLeastTwo_true_right {a : Bool} {b : Bool} : a.atLeastTwo 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 (x.toNat % 2 ^ i + y.toNat % 2 ^ i + c.toNat ≥ 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 = (x.getLsb i).atLeastTwo (y.getLsb 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 = (x.atLeastTwo y c, x.xor (y.xor 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

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

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

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

theorem BitVec.adc_spec {w : Nat} (x : BitVec w) (y : BitVec w) (c : Bool) : x.adc 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 = (x.adc 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