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)

theorem BitVec.carry_of_and_eq_zero {w : Nat} {i : Nat} {x : BitVec w} {y : BitVec w} (h : x &&& y = 0#w) : BitVec.carry i x y false = false

If x &&& y = 0, then the carry bit (x + y + 0) is always false for any index i. Intuitively, this is because a carry is only produced when at least two of x, y, and the previous carry are true. However, since x &&& y = 0, at most one of x, y can be true, and thus we never have a previous carry, which means that the sum cannot produce a carry.

theorem BitVec.carry_width {w : Nat} {c : Bool} {x : BitVec w} {y : BitVec w} : BitVec.carry w x y c = decide (x.toNat + y.toNat + c.toNat ≥ 2 ^ w)

The final carry bit when computing x + y + c is true iff x.toNat + y.toNat + c.toNat ≥ 2^w.

theorem BitVec.toNat_add_of_and_eq_zero {w : Nat} {x : BitVec w} {y : BitVec w} (h : x &&& y = 0#w) : (x + y).toNat = x.toNat + y.toNat

If x &&& y = 0, then addition does not overflow, and thus (x + y).toNat = x.toNat + y.toNat.

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

theorem BitVec.add_eq_or_of_and_eq_zero {w : Nat} (x : BitVec w) (y : BitVec w) (h : x &&& y = 0#w) : x + y = x ||| y

Addition of bitvectors is the same as bitwise or, if bitwise and is zero.

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)

mul recurrence for bitblasting

def BitVec.mulRec {w : Nat} (l : BitVec w) (r : BitVec w) (s : Nat) : BitVec w

A recurrence that describes multiplication as repeated addition. Is useful for bitblasting multiplication.

Equations

• l.mulRec r 0 = if r.getLsb 0 = true then l <<< 0 else 0
• l.mulRec r s_2.succ = l.mulRec r s_2 + if r.getLsb s_2.succ = true then l <<< s_2.succ else 0

theorem BitVec.mulRec_zero_eq {w : Nat} (l : BitVec w) (r : BitVec w) : l.mulRec r 0 = if r.getLsb 0 = true then l else 0

theorem BitVec.mulRec_succ_eq {w : Nat} (l : BitVec w) (r : BitVec w) (s : Nat) : l.mulRec r (s + 1) = l.mulRec r s + if r.getLsb (s + 1) = true then l <<< (s + 1) else 0

theorem BitVec.zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow {w : Nat} (x : BitVec w) (i : Nat) : BitVec.zeroExtend w (BitVec.truncate (i + 1) x) = BitVec.zeroExtend w (BitVec.truncate i x) + (x &&& BitVec.twoPow w i)

Recurrence lemma: truncating to i+1 bits and then zero extending to w equals truncating upto i bits [0..i-1], and then adding the ith bit of x.

theorem BitVec.mulRec_eq_mul_signExtend_truncate {w : Nat} (l : BitVec w) (r : BitVec w) (s : Nat) : l.mulRec r s = l * BitVec.zeroExtend w (BitVec.truncate (s + 1) r)

Recurrence lemma: multiplying l with the first s bits of r is the same as truncating r to s bits, then zero extending to the original length, and performing the multplication.

theorem BitVec.getLsb_mul {w : Nat} (x : BitVec w) (y : BitVec w) (i : Nat) : (x * y).getLsb i = (x.mulRec y w).getLsb i

shiftLeft recurrence for bitblasting

def BitVec.shiftLeftRec {w₁ : Nat} {w₂ : Nat} (x : BitVec w₁) (y : BitVec w₂) (n : Nat) : BitVec w₁

shiftLeftRec x y n shifts x to the left by the first n bits of y.

The theorem shiftLeft_eq_shiftLeftRec proves the equivalence of (x <<< y) and shiftLeftRec.

Together with equations shiftLeftRec_zero, shiftLeftRec_succ, this allows us to unfold shiftLeft into a circuit for bitblasting.

Equations

• x.shiftLeftRec y 0 = x <<< (y &&& BitVec.twoPow w₂ 0)
• x.shiftLeftRec y s_1.succ = x.shiftLeftRec y s_1 <<< (y &&& BitVec.twoPow w₂ s_1.succ)

@[simp]

theorem BitVec.shiftLeftRec_zero {w₁ : Nat} {w₂ : Nat} {x : BitVec w₁} {y : BitVec w₂} : x.shiftLeftRec y 0 = x <<< (y &&& BitVec.twoPow w₂ 0)

@[simp]

theorem BitVec.shiftLeftRec_succ {w₁ : Nat} {w₂ : Nat} {n : Nat} {x : BitVec w₁} {y : BitVec w₂} : x.shiftLeftRec y (n + 1) = x.shiftLeftRec y n <<< (y &&& BitVec.twoPow w₂ (n + 1))

theorem BitVec.shiftLeft_or_of_and_eq_zero {w₁ : Nat} {w₂ : Nat} {x : BitVec w₁} {y : BitVec w₂} {z : BitVec w₂} (h : y &&& z = 0#w₂) : x <<< (y ||| z) = x <<< y <<< z

If y &&& z = 0, x <<< (y ||| z) = x <<< y <<< z. This follows as y &&& z = 0 implies y ||| z = y + z, and thus x <<< (y ||| z) = x <<< (y + z) = x <<< y <<< z.

theorem BitVec.shiftLeftRec_eq {w₁ : Nat} {w₂ : Nat} {x : BitVec w₁} {y : BitVec w₂} {n : Nat} : x.shiftLeftRec y n = x <<< BitVec.zeroExtend w₂ (BitVec.truncate (n + 1) y)

shiftLeftRec x y n shifts x to the left by the first n bits of y.

theorem BitVec.shiftLeft_eq_shiftLeftRec {w₁ : Nat} {w₂ : Nat} (x : BitVec w₁) (y : BitVec w₂) : x <<< y = x.shiftLeftRec y (w₂ - 1)

Show that x <<< y can be written in terms of shiftLeftRec. This can be unfolded in terms of shiftLeftRec_zero, shiftLeftRec_succ for bitblasting.

def BitVec.ushiftRightRec {w₁ : Nat} {w₂ : Nat} (x : BitVec w₁) (y : BitVec w₂) (n : Nat) : BitVec w₁

ushiftRightRec x y n shifts x logically to the right by the first n bits of y.

The theorem shiftRight_eq_ushiftRightRec proves the equivalence of (x >>> y) and ushiftRightRec.

Together with equations ushiftRightRec_zero, ushiftRightRec_succ, this allows us to unfold ushiftRight into a circuit for bitblasting.

Equations

• x.ushiftRightRec y 0 = x >>> (y &&& BitVec.twoPow w₂ 0)
• x.ushiftRightRec y s_1.succ = x.ushiftRightRec y s_1 >>> (y &&& BitVec.twoPow w₂ s_1.succ)

@[simp]

theorem BitVec.ushiftRightRec_zero {w₁ : Nat} {w₂ : Nat} (x : BitVec w₁) (y : BitVec w₂) : x.ushiftRightRec y 0 = x >>> (y &&& BitVec.twoPow w₂ 0)

@[simp]

theorem BitVec.ushiftRightRec_succ {w₁ : Nat} {w₂ : Nat} {n : Nat} (x : BitVec w₁) (y : BitVec w₂) : x.ushiftRightRec y (n + 1) = x.ushiftRightRec y n >>> (y &&& BitVec.twoPow w₂ (n + 1))

theorem BitVec.ushiftRight'_or_of_and_eq_zero {w₁ : Nat} {w₂ : Nat} {x : BitVec w₁} {y : BitVec w₂} {z : BitVec w₂} (h : y &&& z = 0#w₂) : x >>> (y ||| z) = x >>> y >>> z

If y &&& z = 0, x >>> (y ||| z) = x >>> y >>> z. This follows as y &&& z = 0 implies y ||| z = y + z, and thus x >>> (y ||| z) = x >>> (y + z) = x >>> y >>> z.

theorem BitVec.ushiftRightRec_eq {w₁ : Nat} {w₂ : Nat} (x : BitVec w₁) (y : BitVec w₂) (n : Nat) : x.ushiftRightRec y n = x >>> BitVec.zeroExtend w₂ (BitVec.truncate (n + 1) y)

theorem BitVec.shiftRight_eq_ushiftRightRec {w₁ : Nat} {w₂ : Nat} (x : BitVec w₁) (y : BitVec w₂) : x >>> y = x.ushiftRightRec y (w₂ - 1)

Show that x >>> y can be written in terms of ushiftRightRec. This can be unfolded in terms of ushiftRightRec_zero, ushiftRightRec_succ for bitblasting.