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.

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_carry {w : Nat} (x y : BitVec w) : x.ule y = carry w y (~~~x) true

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_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)

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.

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 multiplication.

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) : have 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) : have 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 = have wn := qr.wn - 1; have wr := qr.wr + 1; have r' := qr.r.shiftConcat (args.n.getLsbD wn); have 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.sdivOverflow_eq {w : Nat} (x y : BitVec w) : x.sdivOverflow y = (decide (0 < w) && decide (x = intMin w) && decide (y = allOnes w))

Prove that signed division x.toInt / y.toInt only overflows when x = intMin w and y = allOnes w (for 0 < w).

theorem BitVec.umulOverflow_eq {w : Nat} (x y : BitVec w) : x.umulOverflow y = (decide (0 < w) && decide (twoPow (w * 2) w ≤ zeroExtend (w * 2) x * zeroExtend (w * 2) y))

theorem BitVec.smulOverflow_eq {w : Nat} (x y : BitVec w) : x.smulOverflow y = (decide (0 < w) && ((signExtend (w * 2) (intMax w)).slt (signExtend (w * 2) x * signExtend (w * 2) y) || (signExtend (w * 2) x * signExtend (w * 2) y).slt (signExtend (w * 2) (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.getElem_sdiv {w i : Nat} {x y : BitVec w} (h : i < w) : (x.sdiv y)[i] = match x.msb, y.msb with | false, false => (x / y)[i] | false, true => (-(x / -y))[i] | true, false => (-(-x / y))[i] | true, true => (-x / -y)[i]

theorem BitVec.getLsbD_sdiv {w i : Nat} {x y : BitVec w} : (x.sdiv y).getLsbD i = match x.msb, y.msb with | false, false => (x / y).getLsbD i | false, true => (-(x / -y)).getLsbD i | true, false => (-(-x / y)).getLsbD i | true, true => (-x / -y).getLsbD i

theorem BitVec.getMsbD_sdiv {w i : Nat} {x y : BitVec w} : (x.sdiv y).getMsbD i = match x.msb, y.msb with | false, false => (x / y).getMsbD i | false, true => (-(x / -y)).getMsbD i | true, false => (-(-x / y)).getMsbD i | true, true => (-x / -y).getMsbD i

theorem BitVec.msb_sdiv_eq_decide {w : Nat} {x y : BitVec w} : (x.sdiv y).msb = (decide (0 < w) && (!x.msb && y.msb && decide (-y ≤ x)) || x.msb && !y.msb && decide (y ≤ -x) && !decide (y = 0#w) || x.msb && y.msb && decide (x = intMin w) && decide (y = -1#w))

the most significant bit of the signed division x.sdiv y can be computed by the following cases: (1) x nonneg, y nonneg: never neg. (2) x nonneg, y neg: neg when result nonzero. We know that y is nonzero since it is negative, so we only check |x| ≥ |y|. (3) x neg, y nonneg: neg when result nonzero. We check that y ≠ 0 and |x| ≥ |y|. (4) x neg, y neg: neg when x = intMin, y = -1, since intMin / -1 = intMin`.

The proof strategy is to perform a case analysis on the sign of x and y, followed by unfolding the sdiv into udiv.

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

theorem BitVec.getElem_srem {w i : Nat} {x y : BitVec w} (h : i < w) : (x.srem y)[i] = match x.msb, y.msb with | false, false => (x % y)[i] | false, true => (x % -y)[i] | true, false => (-(-x % y))[i] | true, true => (-(-x % -y))[i]

theorem BitVec.getLsbD_srem {w i : Nat} {x y : BitVec w} : (x.srem y).getLsbD i = match x.msb, y.msb with | false, false => (x % y).getLsbD i | false, true => (x % -y).getLsbD i | true, false => (-(-x % y)).getLsbD i | true, true => (-(-x % -y)).getLsbD i

theorem BitVec.getMsbD_srem {w i : Nat} {x y : BitVec w} : (x.srem y).getMsbD i = match x.msb, y.msb with | false, false => (x % y).getMsbD i | false, true => (x % -y).getMsbD i | true, false => (-(-x % y)).getMsbD i | true, true => (-(-x % -y)).getMsbD i

@[simp]

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

@[simp]

theorem BitVec.msb_intMin_umod_neg_of_msb_true {w : Nat} {y : BitVec w} (hy : y.msb = true) : (intMin w % -y).msb = false

@[simp]

theorem BitVec.msb_neg_umod_neg_of_msb_true_of_msb_true {w : Nat} {x y : BitVec w} (hx : x.msb = true) (hy : y.msb = true) : (-x % -y).msb = false

theorem BitVec.toInt_dvd_toInt_iff {w : Nat} {x y : BitVec w} : y.toInt ∣ x.toInt ↔ ((if x.msb = true then -x else x) % if y.msb = true then -y else y) = 0#w

theorem BitVec.toInt_dvd_toInt_iff_of_msb_true_msb_false {w : Nat} {x y : BitVec w} (hx : x.msb = true) (hy : y.msb = false) : y.toInt ∣ x.toInt ↔ -x % y = 0#w

theorem BitVec.toInt_dvd_toInt_iff_of_msb_false_msb_true {w : Nat} {x y : BitVec w} (hx : x.msb = false) (hy : y.msb = true) : y.toInt ∣ x.toInt ↔ x % -y = 0#w

@[simp]

theorem BitVec.neg_toInt_neg_umod_eq_of_msb_true_msb_true {w : Nat} {x y : BitVec w} (hx : x.msb = true) (hy : y.msb = true) : -(-(-x % -y)).toInt = ↑(-x % -y).toNat

@[simp]

theorem BitVec.toInt_umod_neg_add {w : Nat} {x y : BitVec w} (hymsb : y.msb = true) (hxmsb : x.msb = false) (hdvd : ¬y.toInt ∣ x.toInt) : (x % -y + y).toInt = x.toInt % y.toInt + y.toInt

@[simp]

theorem BitVec.toInt_sub_neg_umod {w : Nat} {x y : BitVec w} (hxmsb : x.msb = true) (hymsb : y.msb = false) (hdvd : ¬y.toInt ∣ x.toInt) : (y - -x % y).toInt = x.toInt % y.toInt

theorem BitVec.srem_zero_of_dvd {w : Nat} {x y : BitVec w} (h : y.toInt ∣ x.toInt) : x.srem y = 0#w

theorem BitVec.msb_srem {w : Nat} {x y : BitVec w} : (x.srem y).msb = (x.msb && decide (x.srem y ≠ 0))

The remainder for srem, i.e. division with rounding to zero is negative iff x is negative and y does not divide x.

We can eventually build fast circuits for the divisibility test x.srem y = 0.

theorem BitVec.toInt_smod {w : Nat} {x y : BitVec w} : (x.smod y).toInt = x.toInt.fmod y.toInt

theorem BitVec.getElem_smod {w i : Nat} {x y : BitVec w} (h : i < w) : (x.smod y)[i] = match x.msb, y.msb with | false, false => (x % y)[i] | false, true => (if x % -y = 0#w then x % -y else x % -y + y)[i] | true, false => (if -x % y = 0#w then -x % y else y - -x % y)[i] | true, true => (-(-x % -y))[i]

theorem BitVec.getLsbD_smod {w i : Nat} {x y : BitVec w} : (x.smod y).getLsbD i = match x.msb, y.msb with | false, false => (x % y).getLsbD i | false, true => if x % -y = 0#w then false else (x % -y + y).getLsbD i | true, false => if -x % y = 0#w then false else (y - -x % y).getLsbD i | true, true => (-(-x % -y)).getLsbD i

theorem BitVec.getMsbD_smod {w i : Nat} {x y : BitVec w} : (x.smod y).getMsbD i = match x.msb, y.msb with | false, false => (x % y).getMsbD i | false, true => (if x % -y = 0#w then x % -y else x % -y + y).getMsbD i | true, false => (if -x % y = 0#w then -x % y else y - -x % y).getMsbD i | true, true => (-(-x % -y)).getMsbD i

theorem BitVec.msb_smod {w : Nat} {x y : BitVec w} : (decide ((x.smod y).msb = (x.msb && decide (y = 0))) || y.msb && decide (x.smod y ≠ 0)) = true

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_zero_add_zero_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. We add a no_index annotation to HAppend.hAppend such that the width v + w does not act as a key in the discrimination tree. This is important to allow matching, when the type of the result of append x : BitVec 3 and y : BitVec 4 has been reduced to x ++ y : BitVec 7.

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

Adding bitvectors that are zero in complementary positions equals concatenation.

theorem BitVec.add_shiftLeft_eq_or_shiftLeft {w : Nat} {x y : BitVec w} : x + y <<< x = x ||| y <<< x

Heuristically, y <<< x is much larger than x, and hence low bits of y <<< x. Thus, x + (y <<< x) = x ||| (y <<< x).

theorem BitVec.shiftLeft_add_eq_shiftLeft_or {w : Nat} {x y : BitVec w} : y <<< x + x = y <<< x ||| x

Heuristically, y <<< x is much larger than x, and hence low bits of y <<< x. Thus, (y <<< x) + x = (y <<< x) ||| x.

Note [Fast Unsigned Multiplication Overflow Detection]

The fast unsigned multiplication overflow detection circuit is described in Efficient integer multiplication overflow detection circuits (https://ieeexplore.ieee.org/abstract/document/987767). With this circuit, the computation of the overflow flag for the unsigned multiplication of two bitvectors x and y with bitwidth w requires: · extending the operands by 1 bit and performing the multiplication with the extended operands, · computing the preliminary overflow flag, which describes whether x and y together have at most w - 2 leading zeros. If the most significant bit of the extended operands' multiplication is true or if the preliminary overflow flag is true, overflow happens. In particular, the conditions check two different cases: · if the most significant bit of the extended operands' multiplication is true, the result of the multiplication 2 ^ w ≤ x.toNat * y.toNat < 2 ^ (w + 1), · if the preliminary flag is true, then 2 ^ (w + 1) ≤ x.toNat * y.toNat.

The computation of the preliminary overflow flag resRec relies on two quantities: · uppcRec: the unsigned parallel prefix circuit for the bits until a certain i, · aandRec: the conjunction between the parallel prefix circuit at of the first operand until a certain i and the i-th bit in the second operand.

def BitVec.uppcRec {w : Nat} (x : BitVec w) (s : Nat) (hs : s < w) : Bool

uppcRec is the unsigned parallel prefix, x.uppcRec s = true iff x.toNat is greater or equal than 2 ^ (w - 1 - (s - 1)).

Equations

• x.uppcRec 0 hs_2 = x.msb
• x.uppcRec i.succ hs_2 = (x[w - 1 - i] || x.uppcRec i ⋯)

@[simp]

theorem BitVec.uppcRec_true_iff {w : Nat} (x : BitVec w) (s : Nat) (h : s < w) : x.uppcRec s h = true ↔ 2 ^ (w - 1 - (s - 1)) ≤ x.toNat

The unsigned parallel prefix of x at s is true if and only if x interpreted as a natural number is greater or equal than 2 ^ (w - 1 - (s - 1)).

def BitVec.aandRec {w : Nat} (x y : BitVec w) (s : Nat) (hs : s < w) : Bool

Conjunction for fast umulOverflow circuit

Equations

• x.aandRec y s hs = (y[s] && x.uppcRec s hs)

def BitVec.resRec {w : Nat} (x y : BitVec w) (s : Nat) (hs : s < w) (hslt : 0 < s) : Bool

Preliminary overflow flag for fast umulOverflow circuit as introduced in Efficient integer multiplication overflow detection circuits (https://ieeexplore.ieee.org/abstract/document/987767).

Equations

• x.resRec y 0 hs_2 hslt_2 = ⋯.elim
• x.resRec y (Nat.succ 0) hs_3 hslt_3 = x.aandRec y 1 hs_3
• x.resRec y s''.succ.succ hs_3 hslt_3 = (x.resRec y s''.succ ⋯ ⋯ || x.aandRec y s''.succ.succ ⋯)

theorem BitVec.resRec_true_iff {w : Nat} (x y : BitVec w) (s : Nat) (hs : s < w) (hs' : 0 < s) : x.resRec y s hs hs' = true ↔ ∃ (k : Nat), ∃ (h : k ≤ s), ∃ (x_1 : 0 < k), x.aandRec y k ⋯ = true

The preliminary overflow flag is true for a certain s if and only if the conjunction returns true at any k smaller than or equal to s.

theorem BitVec.resRec_of_clz_le {w : Nat} {x y : BitVec w} (hw : 1 < w) (hx : x ≠ 0#w) (hy : y ≠ 0#w) : x.clz.toNat + y.clz.toNat ≤ w - 2 → x.resRec y (w - 1) ⋯ ⋯ = true

If the sum of the leading zeroes of two bitvecs with bitwidth w is less than or equal to (w - 2), then the preliminary overflow flag is true and their unsigned multiplication overflows. The explanation is in Efficient integer multiplication overflow detection circuits https://ieeexplore.ieee.org/abstract/document/987767

theorem BitVec.fastUmulOverflow {w : Nat} (x y : BitVec w) : x.umulOverflow y = if hw : w ≤ 1 then false else (setWidth (w + 1) x * setWidth (w + 1) y)[w] || x.resRec y (w - 1) ⋯ ⋯

Complete fast overflow detection circuit for unsigned multiplication.