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

Negation

theorem BitVec.bit_not_testBit {w : Nat} (x : BitVec w) (i : Fin w) : (BitVec.iunfoldr (fun (i : Fin w) (c : Unit) => (c, !x.getLsb ↑i)) ()).snd.getLsb ↑i = !x.getLsb ↑i

theorem BitVec.bit_not_add_self {w : Nat} (x : BitVec w) : (BitVec.iunfoldr (fun (i : Fin w) (c : Unit) => (c, !x.getLsb ↑i)) ()).snd + x = -1

theorem BitVec.bit_not_eq_not {w : Nat} (x : BitVec w) : (BitVec.iunfoldr (fun (i : Fin w) (c : Unit) => (c, !x.getLsb ↑i)) ()).snd = ~~~x

theorem BitVec.bit_neg_eq_neg {w : Nat} (x : BitVec w) : -x = ((BitVec.iunfoldr (fun (i : Fin w) (c : Unit) => (c, !x.getLsb ↑i)) ()).snd.adc (1#w) false).snd

Inequalities (le / lt)

theorem BitVec.ult_eq_not_carry {w : Nat} (x : BitVec w) (y : BitVec w) : x.ult y = !BitVec.carry w x (~~~y) true

theorem BitVec.ule_eq_not_ult {w : Nat} (x : BitVec w) (y : BitVec w) : x.ule y = !y.ult x

theorem BitVec.ule_eq_carry {w : Nat} (x : BitVec w) (y : BitVec w) : x.ule y = BitVec.carry w y (~~~x) true

theorem BitVec.slt_eq_ult_of_msb_eq {w : Nat} {x : BitVec w} {y : BitVec w} (h : x.msb = y.msb) : x.slt y = x.ult y

If two bitvectors have the same msb, then signed and unsigned comparisons coincide

theorem BitVec.ult_eq_msb_of_msb_neq {w : Nat} {x : BitVec w} {y : BitVec w} (h : x.msb ≠ y.msb) : x.ult y = y.msb

If two bitvectors have different msbs, then unsigned comparison is determined by this bit

theorem BitVec.slt_eq_not_ult_of_msb_neq {w : Nat} {x : BitVec w} {y : BitVec w} (h : x.msb ≠ y.msb) : x.slt y = !x.ult y

If two bitvectors have different msbs, then signed and unsigned comparisons are opposites

theorem BitVec.slt_eq_ult {w : Nat} (x : BitVec w) (y : BitVec w) : x.slt y = (x.msb != y.msb).xor (x.ult y)

theorem BitVec.slt_eq_not_carry {w : Nat} (x : BitVec w) (y : BitVec w) : x.slt y = (x.msb == y.msb).xor (BitVec.carry w x (~~~y) true)

theorem BitVec.sle_eq_not_slt {w : Nat} (x : BitVec w) (y : BitVec w) : x.sle y = !y.slt x

theorem BitVec.sle_eq_carry {w : Nat} (x : BitVec w) (y : BitVec w) : x.sle y = !(x.msb == y.msb).xor (BitVec.carry w y (~~~x) true)