Documentation

Init.Data.BitVec.Bitblast

Bitblasting of bitvectors #

This module provides theorems for showing the equivalence between BitVec operations using the Fin 2^n representation and Boolean vectors. It is still under development, but intended to provide a path for converting SAT and SMT solver proofs about BitVectors as vectors of bits into proofs about Lean BitVec values.

The module is named for the bit-blasting operation in an SMT solver that converts bitvector expressions into expressions about individual bits in each vector.

Main results #

x + y : BitVec w is (adc x y false).2.

Future work #

All other operations are to be PR'ed later and are already proved in https://github.com/mhk119/lean-smt/blob/bitvec/Smt/Data/Bitwise.lean.

@[reducible, inline]

abbrev Bool.atLeastTwo (a : Bool) (b : Bool) (c : Bool) :

At least two out of three booleans are true.

Equations

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

@[simp]

theorem Bool.atLeastTwo_false_left {b : Bool} {c : Bool} :

false.atLeastTwo b c = (b && c)

@[simp]

theorem Bool.atLeastTwo_false_mid {a : Bool} {c : Bool} :

a.atLeastTwo false c = (a && c)

@[simp]

theorem Bool.atLeastTwo_false_right {a : Bool} {b : Bool} :

a.atLeastTwo b false = (a && b)

@[simp]

theorem Bool.atLeastTwo_true_left {b : Bool} {c : Bool} :

true.atLeastTwo b c = (b || c)

@[simp]

theorem Bool.atLeastTwo_true_mid {a : Bool} {c : Bool} :

a.atLeastTwo true c = (a || c)

@[simp]

theorem Bool.atLeastTwo_true_right {a : Bool} {b : Bool} :

a.atLeastTwo b true = (a || b)

Preliminaries #

Addition #

def BitVec.carry {w : Nat} (i : Nat) (x : BitVec w) (y : BitVec w) (c : Bool) :

carry i x y c returns true if the i carry bit is true when computing x + y + c.

Equations

BitVec.carry i x y c = decide (x.toNat % 2 ^ i + y.toNat % 2 ^ i + c.toNat ≥ 2 ^ i)

@[simp]

theorem BitVec.carry_zero :

∀ {w : Nat} {x y : BitVec w} {c : Bool}, BitVec.carry 0 x y c = c

theorem BitVec.carry_succ {w : Nat} (i : Nat) (x : BitVec w) (y : BitVec w) (c : Bool) :

BitVec.carry (i + 1) x y c = (x.getLsbD i).atLeastTwo (y.getLsbD i) (BitVec.carry i x y c)

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

BitVec.carry i x y false = false

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

theorem BitVec.carry_width {w : Nat} {c : Bool} {x : BitVec w} {y : BitVec w} :

BitVec.carry w x y c = decide (x.toNat + y.toNat + c.toNat ≥ 2 ^ w)

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

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

(x + y).toNat = x.toNat + y.toNat

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

def BitVec.adcb (x : Bool) (y : Bool) (c : Bool) :

Carry function for bitwise addition.

Equations

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

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

Bool → Bool × BitVec w

Bitwise addition implemented via a ripple carry adder.

Equations

x.adc y = BitVec.iunfoldr fun (i : Fin w) (c : Bool) => BitVec.adcb (x.getLsbD ↑i) (y.getLsbD ↑i) c

theorem BitVec.getLsbD_add_add_bool {w : Nat} {i : Nat} (i_lt : i < w) (x : BitVec w) (y : BitVec w) (c : Bool) :

(x + y + BitVec.setWidth w (BitVec.ofBool c)).getLsbD i = (x.getLsbD i ^^ (y.getLsbD i ^^ BitVec.carry i x y c))

theorem BitVec.getLsbD_add {w : Nat} {i : Nat} (i_lt : i < w) (x : BitVec w) (y : BitVec w) :

(x + y).getLsbD i = (x.getLsbD i ^^ (y.getLsbD i ^^ BitVec.carry i x y false))

theorem BitVec.getElem_add_add_bool {w : Nat} {i : Nat} (i_lt : i < w) (x : BitVec w) (y : BitVec w) (c : Bool) :

(x + y + BitVec.setWidth w (BitVec.ofBool c))[i] = (x[i] ^^ (y[i] ^^ BitVec.carry i x y c))

theorem BitVec.getElem_add {w : Nat} {i : Nat} (i_lt : i < w) (x : BitVec w) (y : BitVec w) :

(x + y)[i] = (x[i] ^^ (y[i] ^^ BitVec.carry i x y false))

theorem BitVec.adc_spec {w : Nat} (x : BitVec w) (y : BitVec w) (c : Bool) :

x.adc y c = (BitVec.carry w x y c, x + y + BitVec.setWidth w (BitVec.ofBool c))

theorem BitVec.add_eq_adc (w : Nat) (x : BitVec w) (y : BitVec w) :

x + y = (x.adc y false).snd

add #

@[simp]

theorem BitVec.add_not_self {w : Nat} (x : BitVec w) :

x + ~~~x = BitVec.allOnes w

Adding a bitvector to its own complement yields the all ones bitpattern

theorem BitVec.allOnes_sub_eq_not {w : Nat} (x : BitVec w) :

BitVec.allOnes w - x = ~~~x

Subtracting x from the all ones bitvector is equivalent to taking its complement

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

x + y = x ||| y

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

Negation #

theorem BitVec.bit_not_testBit {w : Nat} (x : BitVec w) (i : Fin w) :

(BitVec.iunfoldr (fun (i : Fin w) (c : Unit) => (c, !x.getLsbD ↑i)) ()).snd.getLsbD ↑i = !x.getLsbD ↑i

theorem BitVec.bit_not_add_self {w : Nat} (x : BitVec w) :

(BitVec.iunfoldr (fun (i : Fin w) (c : Unit) => (c, !x.getLsbD ↑i)) ()).snd + x = -1

theorem BitVec.bit_not_eq_not {w : Nat} (x : BitVec w) :

(BitVec.iunfoldr (fun (i : Fin w) (c : Unit) => (c, !x.getLsbD ↑i)) ()).snd = ~~~x

theorem BitVec.bit_neg_eq_neg {w : Nat} (x : BitVec w) :

-x = ((BitVec.iunfoldr (fun (i : Fin w) (c : Unit) => (c, !x.getLsbD ↑i)) ()).snd.adc (1#w) false).snd

Inequalities (le / lt) #

theorem BitVec.ult_eq_not_carry {w : Nat} (x : BitVec w) (y : BitVec w) :

x.ult y = !BitVec.carry w x (~~~y) true

theorem BitVec.ule_eq_not_ult {w : Nat} (x : BitVec w) (y : BitVec w) :

x.ule y = !y.ult x

theorem BitVec.ule_eq_carry {w : Nat} (x : BitVec w) (y : BitVec w) :

x.ule y = BitVec.carry w y (~~~x) true

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

x.slt y = x.ult y

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

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

x.ult y = y.msb

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

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

x.slt y = !x.ult y

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

theorem BitVec.slt_eq_ult {w : Nat} (x : BitVec w) (y : BitVec w) :

x.slt y = (x.msb != y.msb ^^ x.ult y)

theorem BitVec.slt_eq_not_carry {w : Nat} (x : BitVec w) (y : BitVec w) :

x.slt y = (x.msb == y.msb ^^ BitVec.carry w x (~~~y) true)

theorem BitVec.sle_eq_not_slt {w : Nat} (x : BitVec w) (y : BitVec w) :

x.sle y = !y.slt x

theorem BitVec.sle_eq_carry {w : Nat} (x : BitVec w) (y : BitVec w) :

x.sle y = !(x.msb == y.msb ^^ BitVec.carry w y (~~~x) true)

mul recurrence for bitblasting #

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

A recurrence that describes multiplication as repeated addition. Is useful for bitblasting 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 : BitVec w) (y : BitVec w) :

x.mulRec y 0 = if y.getLsbD 0 = true then x else 0

theorem BitVec.mulRec_succ_eq {w : Nat} (x : BitVec w) (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) :

BitVec.setWidth w (BitVec.setWidth (i + 1) x) = BitVec.setWidth w (BitVec.setWidth i x) + (x &&& BitVec.twoPow w i)

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

@[reducible, inline, deprecated BitVec.setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow]

abbrev BitVec.zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow {w : Nat} (x : BitVec w) (i : Nat) :

BitVec.setWidth w (BitVec.setWidth (i + 1) x) = BitVec.setWidth w (BitVec.setWidth i x) + (x &&& BitVec.twoPow w i)

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

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 : BitVec w) (y : BitVec w) (s : Nat) :

x.mulRec y s = x * BitVec.setWidth w (BitVec.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]

abbrev BitVec.mulRec_eq_mul_signExtend_truncate {w : Nat} (x : BitVec w) (y : BitVec w) (s : Nat) :

x.mulRec y s = x * BitVec.setWidth w (BitVec.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 : BitVec w) (y : BitVec w) (i : Nat) :

(x * y).getLsbD i = (x.mulRec y w).getLsbD i

theorem BitVec.getElem_mul {w : Nat} {x : BitVec w} {y : BitVec w} {i : Nat} (h : i < w) :

(x * y)[i] = (x.mulRec y w)[i]

shiftLeft recurrence for bitblasting #

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

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

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

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

Equations

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

@[simp]

theorem BitVec.shiftLeftRec_zero {w₁ : Nat} {w₂ : Nat} {x : BitVec w₁} {y : BitVec w₂} :

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

@[simp]

theorem BitVec.shiftLeftRec_succ {w₁ : Nat} {w₂ : Nat} {n : Nat} {x : BitVec w₁} {y : BitVec w₂} :

x.shiftLeftRec y (n + 1) = x.shiftLeftRec y n <<< (y &&& BitVec.twoPow w₂ (n + 1))

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

x <<< (y ||| z) = x <<< y <<< z

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

theorem BitVec.shiftLeftRec_eq {w₁ : Nat} {w₂ : Nat} {x : BitVec w₁} {y : BitVec w₂} {n : Nat} :

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

x <<< y = x.shiftLeftRec y (w₂ - 1)

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

udiv/urem recurrence for bitblasting #

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 : BitVec w} {n : BitVec w} {q : BitVec w} {r : BitVec w} (hd : 0 < d) (hrd : r < d) (hdqnr : d.toNat * q.toNat + r.toNat = n.toNat) :

n.udiv 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 : BitVec w} {n : BitVec w} {q : BitVec w} {r : BitVec w} (hrd : r < d) (hdqnr : d.toNat * q.toNat + r.toNat = n.toNat) :

n.umod 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) :

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

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 : BitVec.DivModArgs w) (qr : BitVec.DivModState w) :

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.

theorem BitVec.DivModState.Lawful.hwrn {w : Nat} {args : BitVec.DivModArgs w} {qr : BitVec.DivModState w} (self : BitVec.DivModState.Lawful args qr) :

qr.wr + qr.wn = w

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

theorem BitVec.DivModState.Lawful.hdPos {w : Nat} {args : BitVec.DivModArgs w} {qr : BitVec.DivModState w} (self : BitVec.DivModState.Lawful args qr) :

0 < args.d

The denominator is positive.

theorem BitVec.DivModState.Lawful.hrLtDivisor {w : Nat} {args : BitVec.DivModArgs w} {qr : BitVec.DivModState w} (self : BitVec.DivModState.Lawful args qr) :

qr.r.toNat < args.d.toNat

The remainder is strictly less than the denominator.

theorem BitVec.DivModState.Lawful.hrWidth {w : Nat} {args : BitVec.DivModArgs w} {qr : BitVec.DivModState w} (self : BitVec.DivModState.Lawful args qr) :

qr.r.toNat < 2 ^ qr.wr

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

theorem BitVec.DivModState.Lawful.hqWidth {w : Nat} {args : BitVec.DivModArgs w} {qr : BitVec.DivModState w} (self : BitVec.DivModState.Lawful args qr) :

qr.q.toNat < 2 ^ qr.wr

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

theorem BitVec.DivModState.Lawful.hdiv {w : Nat} {args : BitVec.DivModArgs w} {qr : BitVec.DivModState w} (self : BitVec.DivModState.Lawful args qr) :

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 : BitVec.DivModArgs w} {qr : BitVec.DivModState w} {h : BitVec.DivModState.Lawful args qr} :

0 < w

A lawful DivModState implies w > 0.

Equations

⋯ = ⋯

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

BitVec.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 : BitVec.DivModArgs w) (hd : 0#w < args.d) :

BitVec.DivModState.Lawful args (BitVec.DivModState.init w)

The initial state is lawful.

Equations

⋯ = ⋯

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

n.udiv 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 : BitVec w} {d : BitVec w} {qr : BitVec.DivModState w} (h : BitVec.DivModState.Lawful { n := n, d := d } qr) (h_final : qr.wn = 0) :

n.umod 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 : BitVec.DivModArgs w) (qr : BitVec.DivModState w) extends BitVec.DivModState.Lawful :

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.

theorem BitVec.DivModState.Poised.hwn_lt {w : Nat} {args : BitVec.DivModArgs w} {qr : BitVec.DivModState w} (self : BitVec.DivModState.Poised args qr) :

0 < qr.wn

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

def BitVec.DivModState.wr_lt_w {w : Nat} {args : BitVec.DivModArgs w} {qr : BitVec.DivModState w} (h : BitVec.DivModState.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 : BitVec.DivModArgs w) (qr : BitVec.DivModState w) :

BitVec.DivModState w

One round of the division algorithm, that tries to perform a subtract shift. Note that this should only be called when r.msb = false, so we 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 : BitVec.DivModArgs w} {qr : BitVec.DivModState w} (h : BitVec.DivModState.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 : BitVec.DivModArgs w} (qr : BitVec.DivModState w) (h : BitVec.DivModState.Poised args qr) :

BitVec.DivModState.Lawful args (BitVec.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 : BitVec.DivModArgs w) (qr : BitVec.DivModState w) :

BitVec.DivModState w

A recursive definition of division for bitblasting, 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 : BitVec.DivModArgs w} (qr : BitVec.DivModState w) :

BitVec.divRec 0 args qr = qr

@[simp]

theorem BitVec.divRec_succ {w : Nat} (m : Nat) (args : BitVec.DivModArgs w) (qr : BitVec.DivModState w) :

BitVec.divRec (m + 1) args qr = BitVec.divRec m args (BitVec.divSubtractShift args qr)

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

BitVec.DivModState.Lawful args (BitVec.divRec qr.wn args qr)

The output of divRec is a lawful state

@[simp]

theorem BitVec.wn_divRec {w : Nat} (args : BitVec.DivModArgs w) (qr : BitVec.DivModState w) :

(BitVec.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 : BitVec w} {n : BitVec w} (hd : 0#w < d) :

let out := BitVec.divRec w { n := n, d := d } (BitVec.DivModState.init w); n.udiv d = out.q

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

theorem BitVec.umod_eq_divRec {w : Nat} {d : BitVec w} {n : BitVec w} (hd : 0#w < d) :

let out := BitVec.divRec w { n := n, d := d } (BitVec.DivModState.init w); n.umod d = out.r

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

theorem BitVec.divRec_succ' {w : Nat} (m : Nat) (args : BitVec.DivModArgs w) (qr : BitVec.DivModState w) :

BitVec.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 }; BitVec.divRec m args input

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

sshiftRightRec x y n shifts x arithmetically/signed to the right by the first n bits of y. The theorem sshiftRight_eq_sshiftRightRec proves the equivalence of (x.sshiftRight y) and sshiftRightRec. Together with equations sshiftRightRec_zero, sshiftRightRec_succ, this allows us to unfold sshiftRight into a circuit for bitblasting.

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₁ : Nat} {w₂ : Nat} (x : BitVec w₁) (y : BitVec w₂) :

x.sshiftRightRec y 0 = x.sshiftRight' (y &&& 1#w₂)

@[simp]

theorem BitVec.sshiftRightRec_succ_eq {w₁ : Nat} {w₂ : Nat} (x : BitVec w₁) (y : BitVec w₂) (n : Nat) :

x.sshiftRightRec y (n + 1) = (x.sshiftRightRec y n).sshiftRight' (y &&& BitVec.twoPow w₂ (n + 1))

theorem BitVec.sshiftRight'_or_of_and_eq_zero {w₁ : Nat} {w₂ : Nat} {x : BitVec w₁} {y : BitVec w₂} {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₁ : Nat} {w₂ : Nat} (x : BitVec w₁) (y : BitVec w₂) (n : Nat) :

x.sshiftRightRec y n = x.sshiftRight' (BitVec.setWidth w₂ (BitVec.setWidth (n + 1) y))

theorem BitVec.sshiftRight_eq_sshiftRightRec {w₁ : Nat} {w₂ : Nat} {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 bitblasting.

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

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

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

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

Equations

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

@[simp]

theorem BitVec.ushiftRightRec_zero {w₁ : Nat} {w₂ : Nat} (x : BitVec w₁) (y : BitVec w₂) :

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

@[simp]

theorem BitVec.ushiftRightRec_succ {w₁ : Nat} {w₂ : Nat} {n : Nat} (x : BitVec w₁) (y : BitVec w₂) :

x.ushiftRightRec y (n + 1) = x.ushiftRightRec y n >>> (y &&& BitVec.twoPow w₂ (n + 1))

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

x >>> (y ||| z) = x >>> y >>> z

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

theorem BitVec.ushiftRightRec_eq {w₁ : Nat} {w₂ : Nat} (x : BitVec w₁) (y : BitVec w₂) (n : Nat) :

x.ushiftRightRec y n = x >>> BitVec.setWidth w₂ (BitVec.setWidth (n + 1) y)

theorem BitVec.shiftRight_eq_ushiftRightRec {w₁ : Nat} {w₂ : Nat} (x : BitVec w₁) (y : BitVec w₂) :

x >>> y = x.ushiftRightRec y (w₂ - 1)

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