Bit blasting 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.

Example: How bit blasting works for multiplication

We explain how the lemmas here are used for bit blasting, by using multiplication as a prototypical example. Other bit blasters for other operations follow the same pattern. To bit blast a multiplication of the form x * y, we must unfold the above into a form that the SAT solver understands.

We assume that the solver already knows how to bit blast addition. This is known to bv_decide, by exploiting the lemma add_eq_adc, which says that x + y : BitVec w equals (adc x y false).2, where adc builds an add-carry circuit in terms of the primitive operations (bitwise and, bitwise or, bitwise xor) that bv_decide already understands. In this way, we layer bit blasters on top of each other, by reducing the multiplication bit blaster to an addition operation.

The core lemma is given by getLsbD_mul:

 x y : BitVec w ⊢ (x * y).getLsbD i = (mulRec x y w).getLsbD i

Which says that the ith bit of x * y can be obtained by evaluating the ith bit of (mulRec x y w). Once again, we assume that bv_decide knows how to implement getLsbD, given that mulRec can be understood by bv_decide.

We write two lemmas to enable bv_decide to unfold (mulRec x y w) into a complete circuit, when w is a known constant. This is given by two recurrence lemmas, mulRec_zero_eqandmulRec_succ_eq, which are applied repeatedly when the width is 0and when the width isw' + 1`:

mulRec_zero_eq :
    mulRec x y 0 =
      if y.getLsbD 0 then x else 0

mulRec_succ_eq
    mulRec x y (s + 1) =
      mulRec x y s +
      if y.getLsbD (s + 1) then (x <<< (s + 1)) else 0 := rfl

By repeatedly applying the lemmas mulRec_zero_eq and mulRec_succ_eq, one obtains a circuit for multiplication. Note that this circuit uses BitVec.add, BitVec.getLsbD, BitVec.shiftLeft. Here, BitVec.add and BitVec.shiftLeft are (recursively) bit blasted by bv_decide, using the lemmas add_eq_adc and shiftLeft_eq_shiftLeftRec, and BitVec.getLsbD is a primitive that bv_decide knows how to reduce to SAT.

The two lemmas, mulRec_zero_eq, and mulRec_succ_eq, are used in Std.Tactic.BVDecide.BVExpr.bitblast.blastMul to prove the correctness of the circuit that is built by bv_decide.

def blastMul (aig : AIG BVBit) (input : AIG.BinaryRefVec aig w) : AIG.RefVecEntry BVBit w
theorem denote_blastMul (aig : AIG BVBit) (lhs rhs : BitVec w) (assign : Assignment) :
   ...
   ⟦(blastMul aig input).aig, (blastMul aig input).vec[idx], assign.toAIGAssignment⟧
     =
   (lhs * rhs).getLsbD idx

The definition and theorem above are internal to bv_decide, and use mulRec_{zero,succ}_eq to prove that the circuit built by bv_decide computes the correct value for multiplication.

To zoom out, therefore, we follow two steps: First, we prove bitvector lemmas to unfold a high-level operation (such as multiplication) into already bit blastable operations (such as addition and left shift). We then use these lemmas to prove the correctness of the circuit that bv_decide builds.

We use this workflow to implement bit blasting for all SMT-LIB v2 operations.

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 b c : Bool) : Bool

At least two out of three Booleans are true.

This function is typically used to model addition of binary numbers, to combine a carry bit with two addend bits.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

Preliminaries

Addition

def BitVec.carry {w : Nat} (i : Nat) (x 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} : carry 0 x y c = c

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

theorem BitVec.carry_succ_one {w : Nat} (i : Nat) (x : BitVec w) (h : 0 < w) : carry (i + 1) x (1#w) false = decide (∀ (j : Nat), j ≤ i → x.getLsbD j = true)

theorem BitVec.carry_of_and_eq_zero {w i : Nat} {x y : BitVec w} (h : x &&& y = 0#w) : 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 y : BitVec w} : 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 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 y c : Bool) : Bool × Bool

Carry function for bitwise addition.

Equations

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

def BitVec.adc {w : Nat} (x 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.getLsbD ↑i) (y.getLsbD ↑i) c

theorem BitVec.getLsbD_add_add_bool {w i : Nat} (i_lt : i < w) (x y : BitVec w) (c : Bool) : (x + y + setWidth w (ofBool c)).getLsbD i = (x.getLsbD i ^^ (y.getLsbD i ^^ carry i x y c))

theorem BitVec.getLsbD_add {w i : Nat} (i_lt : i < w) (x y : BitVec w) : (x + y).getLsbD i = (x.getLsbD i ^^ (y.getLsbD i ^^ carry i x y false))

theorem BitVec.getElem_add_add_bool {w i : Nat} (i_lt : i < w) (x y : BitVec w) (c : Bool) : (x + y + setWidth w (ofBool c))[i] = (x[i] ^^ (y[i] ^^ carry i x y c))

theorem BitVec.getElem_add {w i : Nat} (i_lt : i < w) (x y : BitVec w) : (x + y)[i] = (x[i] ^^ (y[i] ^^ carry i x y false))

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

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

add

theorem BitVec.getMsbD_add {w i : Nat} {i_lt : i < w} {x y : BitVec w} : (x + y).getMsbD i = (x.getMsbD i ^^ (y.getMsbD i ^^ carry (w - 1 - i) x y false))

theorem BitVec.msb_add {w : Nat} {x y : BitVec w} : (x + y).msb = (x.msb ^^ (y.msb ^^ carry (w - 1) x y false))

@[simp]

theorem BitVec.add_not_self {w : Nat} (x : BitVec w) : x + ~~~x = 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) : 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 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.

Sub

theorem BitVec.getLsbD_sub {w i : Nat} {i_lt : i < w} {x y : BitVec w} : (x - y).getLsbD i = (x.getLsbD i ^^ ((~~~y + 1#w).getLsbD i ^^ carry i x (~~~y + 1#w) false))

theorem BitVec.getMsbD_sub {w i : Nat} {i_lt : i < w} {x y : BitVec w} : (x - y).getMsbD i = (x.getMsbD i ^^ ((~~~y + 1).getMsbD i ^^ carry (w - 1 - i) x (~~~y + 1) false))

theorem BitVec.getElem_sub {w i : Nat} {x y : BitVec w} (h : i < w) : (x - y)[i] = (x[i] ^^ ((~~~y + 1#w)[i] ^^ carry i x (~~~y + 1#w) false))

theorem BitVec.msb_sub {w : Nat} {x y : BitVec w} : (x - y).msb = (x.msb ^^ ((~~~y + 1#w).msb ^^ carry (w - 1 - 0) x (~~~y + 1#w) false))

Negation

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

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

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

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

theorem BitVec.getLsbD_neg {w i : Nat} {x : BitVec w} : (-x).getLsbD i = (x.getLsbD i ^^ decide (i < w) && decide (∃ (j : Nat), j < i ∧ x.getLsbD j = true))

Remember that negating a bitvector is equal to incrementing the complement by one, i.e., -x = ~~~x + 1. See also neg_eq_not_add.

This computation has two crucial properties:

• The least significant bit of -x is the same as the least significant bit of x, and
• The i+1-th least significant bit of -x is the complement of the i+1-th bit of x, unless all of the preceding bits are false, in which case the bit is equal to the i+1-th bit of x

theorem BitVec.getElem_neg {w i : Nat} {x : BitVec w} (h : i < w) : (-x)[i] = (x[i] ^^ decide (∃ (j : Nat), j < i ∧ x.getLsbD j = true))

theorem BitVec.getMsbD_neg {w i : Nat} {x : BitVec w} : (-x).getMsbD i = (x.getMsbD i ^^ decide (∃ (j : Nat), j < w ∧ i < j ∧ x.getMsbD j = true))

theorem BitVec.msb_neg {w : Nat} {x : BitVec w} : (-x).msb = (x != 0#w && x != intMin w ^^ x.msb)

@[simp]

theorem BitVec.signExtend_neg_of_le {v w : Nat} (h : w ≤ v) (b : BitVec v) : signExtend w (-b) = -signExtend w b

This is false if v < w and b = intMin. See also signExtend_neg_of_ne_intMin.

@[simp]

theorem BitVec.signExtend_neg_of_ne_intMin {v w : Nat} (b : BitVec v) (hb : b ≠ intMin v) : signExtend w (-b) = -signExtend w b

This is false if v < w and b = intMin. See also signExtend_neg_of_le.

@[simp]

theorem BitVec.BitVec.setWidth_neg_of_le {v w : Nat} {x : BitVec v} (h : w ≤ v) : setWidth w (-x) = -setWidth w x

abs

theorem BitVec.msb_abs {w : Nat} {x : BitVec w} : x.abs.msb = (decide (x = intMin w) && decide (0 < w))

Inequalities (le / lt)

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

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

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

theorem BitVec.slt_eq_ult_of_msb_eq {w : Nat} {x 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 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 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 y : BitVec w} : x.slt y = (x.msb != y.msb ^^ x.ult y)

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

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

theorem BitVec.zero_sle_eq_not_msb {w : Nat} {x : BitVec w} : (0#w).sle x = !x.msb

theorem BitVec.zero_sle_iff_msb_eq_false {w : Nat} {x : BitVec w} : (0#w).sle x = true ↔ x.msb = false

theorem BitVec.toNat_toInt_of_sle {w : Nat} {x : BitVec w} (hx : (0#w).sle x = true) : x.toInt.toNat = x.toNat

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

theorem BitVec.neg_slt_zero {w : Nat} (h : 0 < w) {x : BitVec w} : (-x).slt 0#w = (x == intMin w || (0#w).slt x)

theorem BitVec.neg_sle_zero {w : Nat} (h : 0 < w) {x : BitVec w} : (-x).sle 0#w = (x == intMin w || (0#w).sle x)

theorem BitVec.sle_eq_ule {w : Nat} {x y : BitVec w} : x.sle y = (x.msb != y.msb ^^ x.ule y)

theorem BitVec.sle_eq_ule_of_msb_eq {w : Nat} {x y : BitVec w} (h : x.msb = y.msb) : x.sle y = x.ule y

mul recurrence for bit blasting

def BitVec.mulRec {w : Nat} (x y : BitVec w) (s : Nat) : BitVec w

A recurrence that describes multiplication as repeated addition.

This function is useful for bit blasting multiplication.

Equations

• x.mulRec y 0 = if y.getLsbD 0 = true then x <<< 0 else 0
• x.mulRec y s_2.succ = x.mulRec y s_2 + if y.getLsbD s_2.succ = true then x <<< s_2.succ else 0

theorem BitVec.mulRec_zero_eq {w : Nat} (x y : BitVec w) : x.mulRec y 0 = if y.getLsbD 0 = true then x else 0

theorem BitVec.mulRec_succ_eq {w : Nat} (x y : BitVec w) (s : Nat) : x.mulRec y (s + 1) = x.mulRec y s + if y.getLsbD (s + 1) = true then x <<< (s + 1) else 0

theorem BitVec.setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow {w : Nat} (x : BitVec w) (i : Nat) : setWidth w (setWidth (i + 1) x) = setWidth w (setWidth i x) + (x &&& 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.

@[reducible, inline, deprecated BitVec.setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow (since := "2024-09-18")]

abbrev BitVec.zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow {w : Nat} (x : BitVec w) (i : Nat) : setWidth w (setWidth (i + 1) x) = setWidth w (setWidth i x) + (x &&& 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.

Equations

• @BitVec.zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow = @BitVec.setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow

theorem BitVec.mulRec_eq_mul_signExtend_setWidth {w : Nat} (x y : BitVec w) (s : Nat) : x.mulRec y s = x * setWidth w (setWidth (s + 1) y)

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

@[reducible, inline, deprecated BitVec.mulRec_eq_mul_signExtend_setWidth (since := "2024-09-18")]

abbrev BitVec.mulRec_eq_mul_signExtend_truncate {w : Nat} (x y : BitVec w) (s : Nat) : x.mulRec y s = x * setWidth w (setWidth (s + 1) y)

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

Equations

• @BitVec.mulRec_eq_mul_signExtend_truncate = @BitVec.mulRec_eq_mul_signExtend_setWidth

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

theorem BitVec.mul_eq_mulRec {w : Nat} {x y : BitVec w} : x * y = x.mulRec y w

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

theorem BitVec.getElem_mul {w : Nat} {x y : BitVec w} {i : Nat} (h : i < w) : (x * y)[i] = (x.mulRec y w)[i]

shiftLeft recurrence for bit blasting

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

Shifts x to the left by the first n bits of y.

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

Together with equations BitVec.shiftLeftRec_zero and BitVec.shiftLeftRec_succ, this allows BitVec.shiftLeft to be unfolded into a circuit for bit blasting.

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₁ w₂ : Nat} {x : BitVec w₁} {y : BitVec w₂} : x.shiftLeftRec y 0 = x <<< (y &&& twoPow w₂ 0)

@[simp]

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

theorem BitVec.shiftLeft_or_of_and_eq_zero {w₁ w₂ : Nat} {x : BitVec w₁} {y 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₁ w₂ : Nat} {x : BitVec w₁} {y : BitVec w₂} {n : Nat} : x.shiftLeftRec y n = x <<< setWidth w₂ (setWidth (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₁ 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 bit blasting.

udiv/urem recurrence for bit blasting

In order to prove the correctness of the division algorithm on the integers, one shows that n.div d = q and n.mod d = r iff n = d * q + r and 0 ≤ r < d. Mnemonic: n is the numerator, d is the denominator, q is the quotient, and r the remainder.

This uniqueness of decomposition is not true for bitvectors. For n = 0, d = 3, w = 3, we can write:

• 0 = 0 * 3 + 0 (q = 0, r = 0 < 3.)
• 0 = 2 * 3 + 2 = 6 + 2 ≃ 0 (mod 8) (q = 2, r = 2 < 3).

Such examples can be created by choosing different (q, r) for a fixed (d, n) such that (d * q + r) overflows and wraps around to equal n.

This tells us that the division algorithm must have more restrictions than just the ones we have for integers. These restrictions are captured in DivModState.Lawful. The key idea is to state the relationship in terms of the toNat values of {n, d, q, r}. If the division equation d.toNat * q.toNat + r.toNat = n.toNat holds, then n.udiv d = q and n.umod d = r.

Following this, we implement the division algorithm by repeated shift-subtract.

References:

• Fast 32-bit Division on the DSP56800E: Minimized nonrestoring division algorithm by David Baca
• Bitwuzla sources for bitblasting.h

theorem BitVec.udiv_eq_of_mul_add_toNat {w : Nat} {d n q r : BitVec w} (hd : 0 < d) (hrd : r < d) (hdqnr : d.toNat * q.toNat + r.toNat = n.toNat) : n / d = q

If the division equation d.toNat * q.toNat + r.toNat = n.toNat holds, then n.udiv d = q.

theorem BitVec.umod_eq_of_mul_add_toNat {w : Nat} {d n q r : BitVec w} (hrd : r < d) (hdqnr : d.toNat * q.toNat + r.toNat = n.toNat) : n % d = r

If the division equation d.toNat * q.toNat + r.toNat = n.toNat holds, then n.umod d = r.

DivModState

structure BitVec.DivModState (w : Nat) : Type

DivModState is a structure that maintains the state of recursive divrem calls.

• wn : Nat

  The number of bits in the numerator that are not yet processed

• wr : Nat

  The number of bits in the remainder (and quotient)

• q : BitVec w

  The current quotient.

• r : BitVec w

  The current remainder.

structure BitVec.DivModArgs (w : Nat) : Type

DivModArgs contains the arguments to a divrem call which remain constant throughout execution.

• n : BitVec w

  the numerator (aka, dividend)

• d : BitVec w

  the denumerator (aka, divisor)

structure BitVec.DivModState.Lawful {w : Nat} (args : DivModArgs w) (qr : DivModState w) : Prop

A DivModState is lawful if the remainder width wr plus the numerator width wn equals w, and the bitvectors r and n have values in the bounds given by bitwidths wr, resp. wn.

This is a proof engineering choice: an alternative world could have been r : BitVec wr and n : BitVec wn, but this required much more dependent typing coercions.

Instead, we choose to declare all involved bitvectors as length w, and then prove that the values are within their respective bounds.

We start with wn = w and wr = 0, and then in each step, we decrement wn and increment wr. In this way, we grow a legal remainder in each loop iteration.

• hwrn : qr.wr + qr.wn = w

  The sum of widths of the dividend and remainder is w.

• hdPos : 0 < args.d

  The denominator is positive.

• hrLtDivisor : qr.r.toNat < args.d.toNat

  The remainder is strictly less than the denominator.

• hrWidth : qr.r.toNat < 2 ^ qr.wr

  The remainder is morally a Bitvec wr, and so has value less than 2^wr.

• hqWidth : qr.q.toNat < 2 ^ qr.wr

  The quotient is morally a Bitvec wr, and so has value less than 2^wr.

• hdiv : args.n.toNat >>> qr.wn = args.d.toNat * qr.q.toNat + qr.r.toNat

  The low (w - wn) bits of n obey the invariant for division.

def BitVec.DivModState.Lawful.hw {w : Nat} {args : DivModArgs w} {qr : DivModState w} {h : Lawful args qr} : 0 < w

A lawful DivModState implies w > 0.

Equations

• ⋯ = ⋯

def BitVec.DivModState.init (w : Nat) : DivModState w

An initial value with both q, r = 0.

Equations

• BitVec.DivModState.init w = { wn := w, wr := 0, q := 0#w, r := 0#w }

def BitVec.DivModState.lawful_init {w : Nat} (args : DivModArgs w) (hd : 0#w < args.d) : Lawful args (init w)

The initial state is lawful.

Equations

• ⋯ = ⋯

theorem BitVec.DivModState.udiv_eq_of_lawful {w : Nat} {n d : BitVec w} {qr : DivModState w} (h_lawful : Lawful { n := n, d := d } qr) (h_final : qr.wn = 0) : n / d = qr.q

A lawful DivModState with a fully consumed dividend (wn = 0) witnesses that the quotient has been correctly computed.

theorem BitVec.DivModState.umod_eq_of_lawful {w : Nat} {n d : BitVec w} {qr : DivModState w} (h : Lawful { n := n, d := d } qr) (h_final : qr.wn = 0) : n % d = qr.r

A lawful DivModState with a fully consumed dividend (wn = 0) witnesses that the remainder has been correctly computed.

DivModState.Poised

structure BitVec.DivModState.Poised {w : Nat} (args : DivModArgs w) (qr : DivModState w) extends BitVec.DivModState.Lawful args qr : Prop

A Poised DivModState is a state which is Lawful and furthermore, has at least one numerator bit left to process (0 < wn)

The input to the shift subtractor is a legal input to divrem, and we also need to have an input bit to perform shift subtraction on, and thus we need 0 < wn.

• hwrn : qr.wr + qr.wn = w
• hdPos : 0 < args.d
• hrLtDivisor : qr.r.toNat < args.d.toNat
• hrWidth : qr.r.toNat < 2 ^ qr.wr
• hqWidth : qr.q.toNat < 2 ^ qr.wr
• hdiv : args.n.toNat >>> qr.wn = args.d.toNat * qr.q.toNat + qr.r.toNat
• hwn_lt : 0 < qr.wn

  Only perform a round of shift-subtract if we have dividend bits.

def BitVec.DivModState.wr_lt_w {w : Nat} {args : DivModArgs w} {qr : DivModState w} (h : Poised args qr) : qr.wr < w

In the shift subtract input, the dividend is at least one bit long (wn > 0), so the remainder has bits to be computed (wr < w).

Equations

• ⋯ = ⋯

Division shift subtractor

def BitVec.divSubtractShift {w : Nat} (args : DivModArgs w) (qr : DivModState w) : DivModState w

One round of the division algorithm. It tries to perform a subtract shift.

This should only be called when r.msb = false, so it will not overflow.

Equations

• One or more equations did not get rendered due to their size.

theorem BitVec.DivModState.toNat_shiftRight_sub_one_eq {w : Nat} {args : DivModArgs w} {qr : DivModState w} (h : Poised args qr) : args.n.toNat >>> (qr.wn - 1) = args.n.toNat >>> qr.wn * 2 + (args.n.getLsbD (qr.wn - 1)).toNat

The value of shifting right by wn - 1 equals shifting by wn and grabbing the lsb at (wn - 1).

theorem BitVec.lawful_divSubtractShift {w : Nat} {args : DivModArgs w} (qr : DivModState w) (h : DivModState.Poised args qr) : DivModState.Lawful args (divSubtractShift args qr)

We show that the output of divSubtractShift is lawful, which tells us that it obeys the division equation.

Core division algorithm circuit

def BitVec.divRec {w : Nat} (m : Nat) (args : DivModArgs w) (qr : DivModState w) : DivModState w

A recursive definition of division for bit blasting, in terms of a shift-subtraction circuit.

Equations

• BitVec.divRec 0 args qr = qr
• BitVec.divRec s_1.succ args qr = BitVec.divRec s_1 args (BitVec.divSubtractShift args qr)

@[simp]

theorem BitVec.divRec_zero {w : Nat} {args : DivModArgs w} (qr : DivModState w) : divRec 0 args qr = qr

@[simp]

theorem BitVec.divRec_succ {w : Nat} (m : Nat) (args : DivModArgs w) (qr : DivModState w) : divRec (m + 1) args qr = divRec m args (divSubtractShift args qr)

theorem BitVec.lawful_divRec {w : Nat} {args : DivModArgs w} {qr : DivModState w} (h : DivModState.Lawful args qr) : DivModState.Lawful args (divRec qr.wn args qr)

The output of divRec is a lawful state

@[simp]

theorem BitVec.wn_divRec {w : Nat} (args : DivModArgs w) (qr : DivModState w) : (divRec qr.wn args qr).wn = 0

The output of divRec has no more bits left to process (i.e., wn = 0)

theorem BitVec.udiv_eq_divRec {w : Nat} {d n : BitVec w} (hd : 0#w < d) : let out := divRec w { n := n, d := d } (DivModState.init w); n / d = out.q

The result of udiv agrees with the result of the division recurrence.

theorem BitVec.umod_eq_divRec {w : Nat} {d n : BitVec w} (hd : 0#w < d) : let out := divRec w { n := n, d := d } (DivModState.init w); n % d = out.r

The result of umod agrees with the result of the division recurrence.

theorem BitVec.divRec_succ' {w : Nat} (m : Nat) (args : DivModArgs w) (qr : DivModState w) : divRec (m + 1) args qr = let wn := qr.wn - 1; let wr := qr.wr + 1; let r' := qr.r.shiftConcat (args.n.getLsbD wn); let input := if r' < args.d then { wn := wn, wr := wr, q := qr.q.shiftConcat false, r := r' } else { wn := wn, wr := wr, q := qr.q.shiftConcat true, r := r' - args.d }; divRec m args input

theorem BitVec.getElem_udiv {w : Nat} (n d : BitVec w) (hy : 0#w < d) (i : Nat) (hi : i < w) : (n / d)[i] = (divRec w { n := n, d := d } (DivModState.init w)).q[i]

theorem BitVec.getLsbD_udiv {w : Nat} (n d : BitVec w) (hy : 0#w < d) (i : Nat) : (n / d).getLsbD i = (decide (i < w) && (divRec w { n := n, d := d } (DivModState.init w)).q.getLsbD i)

theorem BitVec.getMsbD_udiv {w : Nat} (n d : BitVec w) (hd : 0#w < d) (i : Nat) : (n / d).getMsbD i = (decide (i < w) && (divRec w { n := n, d := d } (DivModState.init w)).q.getMsbD i)

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

Shifts x arithmetically (signed) to the right by the first n bits of y.

The theorem BitVec.sshiftRight_eq_sshiftRightRec proves the equivalence of (x.sshiftRight y) and BitVec.sshiftRightRec x y. Together with equations BitVec.sshiftRightRec_zero, and BitVec.sshiftRightRec_succ, this allows BitVec.sshiftRight to be unfolded into a circuit for bit blasting.

Equations

• x.sshiftRightRec y 0 = x.sshiftRight' (y &&& BitVec.twoPow w₂ 0)
• x.sshiftRightRec y s_1.succ = (x.sshiftRightRec y s_1).sshiftRight' (y &&& BitVec.twoPow w₂ s_1.succ)

@[simp]

theorem BitVec.sshiftRightRec_zero_eq {w₁ w₂ : Nat} (x : BitVec w₁) (y : BitVec w₂) : x.sshiftRightRec y 0 = x.sshiftRight' (y &&& twoPow w₂ 0)

@[simp]

theorem BitVec.sshiftRightRec_succ_eq {w₁ w₂ : Nat} (x : BitVec w₁) (y : BitVec w₂) (n : Nat) : x.sshiftRightRec y (n + 1) = (x.sshiftRightRec y n).sshiftRight' (y &&& twoPow w₂ (n + 1))

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

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

theorem BitVec.sshiftRightRec_eq {w₁ w₂ : Nat} (x : BitVec w₁) (y : BitVec w₂) (n : Nat) : x.sshiftRightRec y n = x.sshiftRight' (setWidth w₂ (setWidth (n + 1) y))

theorem BitVec.sshiftRight_eq_sshiftRightRec {w₁ w₂ i : Nat} (x : BitVec w₁) (y : BitVec w₂) : (x.sshiftRight' y).getLsbD i = (x.sshiftRightRec y (w₂ - 1)).getLsbD i

Show that x.sshiftRight y can be written in terms of sshiftRightRec. This can be unfolded in terms of sshiftRightRec_zero_eq, sshiftRightRec_succ_eq for bit blasting.

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

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

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

Together with equations BitVec.ushiftRightRec_zero and BitVec.ushiftRightRec_succ, this allows BitVec.ushiftRight to be unfolded into a circuit for bit blasting.

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₁ w₂ : Nat} (x : BitVec w₁) (y : BitVec w₂) : x.ushiftRightRec y 0 = x >>> (y &&& twoPow w₂ 0)

@[simp]

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

theorem BitVec.ushiftRight'_or_of_and_eq_zero {w₁ w₂ : Nat} {x : BitVec w₁} {y 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₁ w₂ : Nat} (x : BitVec w₁) (y : BitVec w₂) (n : Nat) : x.ushiftRightRec y n = x >>> setWidth w₂ (setWidth (n + 1) y)

theorem BitVec.shiftRight_eq_ushiftRightRec {w₁ 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 bit blasting.

Overflow definitions

theorem BitVec.uaddOverflow_eq {w : Nat} (x y : BitVec w) : x.uaddOverflow y = (setWidth (w + 1) x + setWidth (w + 1) y).msb

Unsigned addition overflows iff the final carry bit of the addition circuit is true.

theorem BitVec.saddOverflow_eq {w : Nat} (x y : BitVec w) : x.saddOverflow y = (x.msb == y.msb && !(x + y).msb == x.msb)

theorem BitVec.usubOverflow_eq {w : Nat} (x y : BitVec w) : x.usubOverflow y = decide (x < y)

theorem BitVec.ssubOverflow_eq {w : Nat} (x y : BitVec w) : x.ssubOverflow y = (!x.msb && y.msb && (x - y).msb || x.msb && !y.msb && !(x - y).msb)

theorem BitVec.negOverflow_eq {w : Nat} (x : BitVec w) : x.negOverflow = (decide (0 < w) && x == intMin w)

theorem BitVec.getElem_umod {w i : Nat} {n d : BitVec w} (hi : i < w) : (n % d)[i] = if d = 0#w then n[i] else (divRec w { n := n, d := d } (DivModState.init w)).r[i]

theorem BitVec.getLsbD_umod {w i : Nat} {n d : BitVec w} : (n % d).getLsbD i = if d = 0#w then n.getLsbD i else (divRec w { n := n, d := d } (DivModState.init w)).r.getLsbD i

theorem BitVec.getMsbD_umod {w i : Nat} {n d : BitVec w} : (n % d).getMsbD i = if d = 0#w then n.getMsbD i else (divRec w { n := n, d := d } (DivModState.init w)).r.getMsbD i

Mappings to and from BitVec

theorem BitVec.eq_iff_eq_of_inv {α : Sort u_1} {w : Nat} (f : α → BitVec w) (g : BitVec w → α) (h : ∀ (x : α), g (f x) = x) (x y : α) : x = y ↔ f x = f y

@[simp]

theorem BitVec.ne_intMin_of_lt_of_msb_false {w : Nat} {x : BitVec w} (hw : 0 < w) (hx : x.msb = false) : x ≠ intMin w

@[simp]

theorem BitVec.ne_zero_of_msb_true {w : Nat} {x : BitVec w} (hx : x.msb = true) : x ≠ 0#w

@[simp]

theorem BitVec.msb_neg_of_ne_intMin_of_ne_zero {w : Nat} {x : BitVec w} (h : x ≠ intMin w) (h' : x ≠ 0#w) : (-x).msb = !x.msb

@[simp]

theorem BitVec.udiv_intMin_of_msb_false {w : Nat} {x : BitVec w} (h : x.msb = false) : x / intMin w = 0#w

theorem BitVec.sdiv_intMin {w : Nat} {x : BitVec w} : x.sdiv (intMin w) = if x = intMin w then 1#w else 0#w

theorem BitVec.sdiv_neg {w : Nat} {x y : BitVec w} (h : y ≠ intMin w) : x.sdiv (-y) = -x.sdiv y

theorem BitVec.neg_sdiv {w : Nat} {x y : BitVec w} (h : x ≠ intMin w) : (-x).sdiv y = -x.sdiv y

theorem BitVec.neg_sdiv_neg {w : Nat} {x y : BitVec w} (h : x ≠ intMin w) : (-x).sdiv (-y) = x.sdiv y

theorem BitVec.intMin_eq_neg_two_pow {w : Nat} : intMin w = BitVec.ofInt w (-2 ^ (w - 1))

theorem BitVec.toInt_intMin_eq_bmod {w : Nat} : (intMin w).toInt = (-2 ^ (w - 1)).bmod (2 ^ w)

@[simp]

theorem BitVec.toInt_bmod_cancel {w : Nat} (b : BitVec w) : b.toInt.bmod (2 ^ w) = b.toInt

theorem BitVec.sdiv_ne_intMin_of_ne_intMin {w : Nat} {x y : BitVec w} (h : x ≠ intMin w) : x.sdiv y ≠ intMin w

theorem BitVec.toInt_eq_neg_toNat_neg_of_msb_true {w : Nat} {x : BitVec w} (h : x.msb = true) : x.toInt = -↑(-x).toNat

theorem BitVec.toInt_eq_neg_toNat_neg_of_nonpos {w : Nat} {x : BitVec w} (h : x = 0#w ∨ x.msb = true) : x.toInt = -↑(-x).toNat

theorem BitVec.intMin_udiv_eq_intMin_iff {w : Nat} (x : BitVec w) : intMin w / x = intMin w ↔ x = 1#w

theorem BitVec.intMin_udiv_ne_zero_of_ne_zero {w : Nat} {b : BitVec w} (hb : b.msb = false) (hb0 : b ≠ 0#w) : intMin w / b ≠ 0#w

theorem BitVec.toInt_sdiv_of_ne_or_ne {w : Nat} (a b : BitVec w) (h : a ≠ intMin w ∨ b ≠ -1#w) : (a.sdiv b).toInt = a.toInt.tdiv b.toInt

theorem BitVec.intMin_sdiv_neg_one {w : Nat} : (intMin w).sdiv (-1#w) = intMin w

theorem BitVec.toInt_sdiv {w : Nat} (a b : BitVec w) : (a.sdiv b).toInt = (a.toInt.tdiv b.toInt).bmod (2 ^ w)

theorem BitVec.msb_umod_eq_false_of_left {w : Nat} {x : BitVec w} (hx : x.msb = false) (y : BitVec w) : (x % y).msb = false

theorem BitVec.msb_umod_of_le_of_ne_zero_of_le {w : Nat} {x y : BitVec w} (hx : x ≤ intMin w) (hy : y ≠ 0#w) (hy' : y ≤ intMin w) : (x % y).msb = false

@[simp]

theorem BitVec.toInt_srem {w : Nat} (x y : BitVec w) : (x.srem y).toInt = x.toInt.tmod y.toInt

Lemmas that use bit blasting circuits

theorem BitVec.add_sub_comm {w : Nat} {z x y : BitVec w} : x + y - z = x - z + y

theorem BitVec.sub_add_comm {w : Nat} {z x y : BitVec w} : x - y + z = x + z - y

theorem BitVec.not_add_one {w : Nat} {x : BitVec w} : ~~~(x + 1#w) = ~~~x - 1#w

theorem BitVec.not_add_eq_not_neg {w : Nat} {x y : BitVec w} : ~~~(x + y) = ~~~x - y

theorem BitVec.not_sub_one_eq_not_add_one {w : Nat} {x : BitVec w} : ~~~(x - 1#w) = ~~~x + 1#w

theorem BitVec.not_sub_eq_not_add {w : Nat} {x y : BitVec w} : ~~~(x - y) = ~~~x + y

theorem BitVec.carry_extractLsb'_eq_carry {w i len : Nat} (hi : i < len) {x y : BitVec w} {b : Bool} : carry i (extractLsb' 0 len x) (extractLsb' 0 len y) b = carry i x y b

The value of (carry i x y false) can be computed by truncating x and y to len bits where len ≥ i.

theorem BitVec.extractLsb'_add {w len : Nat} {x y : BitVec w} (hlen : len ≤ w) : extractLsb' 0 len (x + y) = extractLsb' 0 len x + extractLsb' 0 len y

The [0..len) low bits of x + y can be computed by truncating x and y to len bits and then adding.

theorem BitVec.extractLsb'_mul {w len : Nat} {x y : BitVec w} (hlen : len ≤ w) : extractLsb' 0 len (x * y) = extractLsb' 0 len x * extractLsb' 0 len y

extractLsb' commutes with multiplication.

theorem BitVec.append_add_append_eq_append {v w : Nat} {x : BitVec v} {y : BitVec w} : x ++ 0#w + (0#v ++ y) = x ++ y

Adding bitvectors that are zero in complementary positions equals concatenation.