# 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 `i`th bit of `x * y` can be obtained by evaluating the `i`th 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_eq`and`mulRec_succ_eq`, which are applied repeatedly when the width is` 0`and when the width is`w' + 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.

source
@[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)

Instances For

source
@[simp]
theorem Bool.atLeastTwo_false_left {b c : Bool} :
false.atLeastTwo b c = (b && c)
source
@[simp]
theorem Bool.atLeastTwo_false_mid {a c : Bool} :
a.atLeastTwo false c = (a && c)
source
@[simp]
theorem Bool.atLeastTwo_false_right {a b : Bool} :
a.atLeastTwo b false = (a && b)
source
@[simp]
theorem Bool.atLeastTwo_true_left {b c : Bool} :
true.atLeastTwo b c = (b || c)
source
@[simp]
theorem Bool.atLeastTwo_true_mid {a c : Bool} :
a.atLeastTwo true c = (a || c)
source
@[simp]
theorem Bool.atLeastTwo_true_right {a b : Bool} :
a.atLeastTwo b true = (a || b)

### Preliminaries #

### Addition #

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

Instances For

source
@[simp]
theorem BitVec.carry_zero {w✝ : Nat} {x y : BitVec w✝} {c : Bool} :
carry 0 x y c = c
source
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)
source
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)
source
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.

source
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`.

source
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`.

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

Instances For

source
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

Instances For

source
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))
source
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))
source
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))
source
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))
source
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))
source
theorem BitVec.add_eq_adc (w : Nat) (x y : BitVec w) :
x + y = (x.adc y false).snd

### add #

source
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))
source
theorem BitVec.msb_add {w : Nat} {x y : BitVec w} :
(x + y).msb = (x.msb ^^ (y.msb ^^ carry (w - 1) x y false))
source
@[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

source
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

source
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 #

source
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))
source
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))
source
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))
source
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 #

source
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
source
theorem BitVec.bit_not_add_self {w : Nat} (x : BitVec w) :
(iunfoldr (fun (i : Fin w) (c : Unit) => (c, !x[↑i])) ()).snd + x = -1
source
theorem BitVec.bit_not_eq_not {w : Nat} (x : BitVec w) :
(iunfoldr (fun (i : Fin w) (c : Unit) => (c, !x[i])) ()).snd = ~~~x
source
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
source
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`

source
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))
source
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))
source
theorem BitVec.msb_neg {w : Nat} {x : BitVec w} :
(-x).msb = (x != 0#w && x != intMin w ^^ x.msb)
source
@[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`.

source
@[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 #

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

### Inequalities (le / lt) #

source
theorem BitVec.ult_eq_not_carry {w : Nat} (x y : BitVec w) :
x.ult y = !carry w x (~~~y) true
source
theorem BitVec.ule_eq_carry {w : Nat} (x y : BitVec w) :
x.ule y = carry w y (~~~x) true
source
theorem BitVec.slt_eq_not_carry {w : Nat} {x y : BitVec w} :
x.slt y = (x.msb == y.msb ^^ carry w x (~~~y) true)
source
theorem BitVec.sle_eq_carry {w : Nat} {x y : BitVec w} :
x.sle y = !(x.msb == y.msb ^^ carry w y (~~~x) true)
source
theorem BitVec.neg_slt_zero {w : Nat} (h : 0 < w) {x : BitVec w} :
(-x).slt 0#w = (x == intMin w || (0#w).slt x)
source
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 #

source
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

Instances For

source
theorem BitVec.mulRec_zero_eq {w : Nat} (x y : BitVec w) :
x.mulRec y 0 = if y.getLsbD 0 = true then x else 0
source
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
source
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 `i`th bit of `x`.

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

source
theorem BitVec.getLsbD_mul {w : Nat} (x y : BitVec w) (i : Nat) :
(x * y).getLsbD i = (x.mulRec y w).getLsbD i
source
theorem BitVec.mul_eq_mulRec {w : Nat} {x y : BitVec w} :
x * y = x.mulRec y w
source
theorem BitVec.getMsbD_mul {w : Nat} (x y : BitVec w) (i : Nat) :
(x * y).getMsbD i = (x.mulRec y w).getMsbD i
source
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 #

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

Instances For

source
@[simp]
theorem BitVec.shiftLeftRec_zero {w₁ w₂ : Nat} {x : BitVec w₁} {y : BitVec w₂} :
x.shiftLeftRec y 0 = x <<< (y &&& twoPow w₂ 0)
source
@[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))
source
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`.

source
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`.

source
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

source
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`.

source
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 #

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

Instances For

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

Instances For

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

Instances For

source
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

- ⋯ = ⋯

Instances For

source
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 }

Instances For

source
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

- ⋯ = ⋯

Instances For

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

source
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 #

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

Instances For

source
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

- ⋯ = ⋯

Instances For

### Division shift subtractor #

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

Instances For

source
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)`.

source
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 #

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

Instances For

source
@[simp]
theorem BitVec.divRec_zero {w : Nat} {args : DivModArgs w} (qr : DivModState w) :
divRec 0 args qr = qr
source
@[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)
source
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

source
@[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`)

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

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

source
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
source
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]
source
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)
source
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)
source
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)

Instances For

source
@[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)
source
@[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))
source
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`.

source
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))
source
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.

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

Instances For

source
@[simp]
theorem BitVec.ushiftRightRec_zero {w₁ w₂ : Nat} (x : BitVec w₁) (y : BitVec w₂) :
x.ushiftRightRec y 0 = x >>> (y &&& twoPow w₂ 0)
source
@[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))
source
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`.

source
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)
source
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 #

source
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`.

source
theorem BitVec.saddOverflow_eq {w : Nat} (x y : BitVec w) :
x.saddOverflow y = (x.msb == y.msb && !(x + y).msb == x.msb)
source
theorem BitVec.usubOverflow_eq {w : Nat} (x y : BitVec w) :
x.usubOverflow y = decide (x < y)
source
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)
source
theorem BitVec.negOverflow_eq {w : Nat} (x : BitVec w) :
x.negOverflow = (decide (0 < w) && x == intMin w)
source
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`).

source
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))
source
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))))
source
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]
source
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
source
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 #

source
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
source
@[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
source
@[simp]
theorem BitVec.ne_zero_of_msb_true {w : Nat} {x : BitVec w} (hx : x.msb = true) :
x ≠ 0#w
source
@[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
source
@[simp]
theorem BitVec.udiv_intMin_of_msb_false {w : Nat} {x : BitVec w} (h : x.msb = false) :
x / intMin w = 0#w
source
theorem BitVec.sdiv_intMin {w : Nat} {x : BitVec w} :
x.sdiv (intMin w) = if x = intMin w then 1#w else 0#w
source
theorem BitVec.sdiv_neg {w : Nat} {x y : BitVec w} (h : y ≠ intMin w) :
x.sdiv (-y) = -x.sdiv y
source
theorem BitVec.neg_sdiv {w : Nat} {x y : BitVec w} (h : x ≠ intMin w) :
(-x).sdiv y = -x.sdiv y
source
theorem BitVec.neg_sdiv_neg {w : Nat} {x y : BitVec w} (h : x ≠ intMin w) :
(-x).sdiv (-y) = x.sdiv y
source
theorem BitVec.intMin_eq_neg_two_pow {w : Nat} :
intMin w = BitVec.ofInt w (-2 ^ (w - 1))
source
theorem BitVec.toInt_intMin_eq_bmod {w : Nat} :
(intMin w).toInt = (-2 ^ (w - 1)).bmod (2 ^ w)
source
@[simp]
theorem BitVec.toInt_bmod_cancel {w : Nat} (b : BitVec w) :
b.toInt.bmod (2 ^ w) = b.toInt
source
theorem BitVec.sdiv_ne_intMin_of_ne_intMin {w : Nat} {x y : BitVec w} (h : x ≠ intMin w) :
x.sdiv y ≠ intMin w
source
theorem BitVec.toInt_eq_neg_toNat_neg_of_msb_true {w : Nat} {x : BitVec w} (h : x.msb = true) :
x.toInt = -↑(-x).toNat
source
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
source
theorem BitVec.intMin_udiv_eq_intMin_iff {w : Nat} (x : BitVec w) :
intMin w / x = intMin w ↔ x = 1#w
source
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
source
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
source
theorem BitVec.intMin_sdiv_neg_one {w : Nat} :
(intMin w).sdiv (-1#w) = intMin w
source
theorem BitVec.toInt_sdiv {w : Nat} (a b : BitVec w) :
(a.sdiv b).toInt = (a.toInt.tdiv b.toInt).bmod (2 ^ w)
source
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]
source
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
source
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
source
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`.

source
theorem BitVec.msb_umod_eq_false_of_left {w : Nat} {x : BitVec w} (hx : x.msb = false) (y : BitVec w) :
(x % y).msb = false
source
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
source
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]
source
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
source
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
source
@[simp]
theorem BitVec.toInt_srem {w : Nat} (x y : BitVec w) :
(x.srem y).toInt = x.toInt.tmod y.toInt
source
@[simp]
theorem BitVec.msb_intMin_umod_neg_of_msb_true {w : Nat} {y : BitVec w} (hy : y.msb = true) :
(intMin w % -y).msb = false
source
@[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
source
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
source
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
source
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
source
@[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
source
@[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
source
@[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
source
theorem BitVec.srem_zero_of_dvd {w : Nat} {x y : BitVec w} (h : y.toInt ∣ x.toInt) :
x.srem y = 0#w
source
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`.

source
theorem BitVec.toInt_smod {w : Nat} {x y : BitVec w} :
(x.smod y).toInt = x.toInt.fmod y.toInt
source
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]
source
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
source
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
source
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 #

source
theorem BitVec.add_sub_comm {w : Nat} {z x y : BitVec w} :
x + y - z = x - z + y
source
theorem BitVec.sub_add_comm {w : Nat} {z x y : BitVec w} :
x - y + z = x + z - y
source
theorem BitVec.not_add_one {w : Nat} {x : BitVec w} :
~~~(x + 1#w) = ~~~x - 1#w
source
theorem BitVec.not_add_eq_not_neg {w : Nat} {x y : BitVec w} :
~~~(x + y) = ~~~x - y
source
theorem BitVec.not_sub_one_eq_not_add_one {w : Nat} {x : BitVec w} :
~~~(x - 1#w) = ~~~x + 1#w
source
theorem BitVec.not_sub_eq_not_add {w : Nat} {x y : BitVec w} :
~~~(x - y) = ~~~x + y
source
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`.

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

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

source
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`.

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

source
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).`

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

source
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 ⋯)

Instances For

source
@[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))`.

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

Instances For

source
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 ⋯)

Instances For

source
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`.

source
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

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