Documentation

Init.Data.BitVec.Lemmas

theorem BitVec.ofFin_eq_ofNat {w : Nat} {x : Nat} {lt : x < 2 ^ w} :
{ toFin := x, lt } = BitVec.ofNat w x

This normalized a bitvec using ofFin to ofNat.

theorem BitVec.eq_of_toNat_eq {n : Nat} {i : BitVec n} {j : BitVec n} :
i.toNat = j.toNati = j

Prove equality of bitvectors in terms of nat operations.

@[simp]
theorem BitVec.val_toFin {w : Nat} (x : BitVec w) :
x.toFin = x.toNat
theorem BitVec.toNat_eq {n : Nat} (x : BitVec n) (y : BitVec n) :
x = y x.toNat = y.toNat
theorem BitVec.toNat_ne {n : Nat} (x : BitVec n) (y : BitVec n) :
x y x.toNat y.toNat
theorem BitVec.testBit_toNat {w : Nat} {i : Nat} (x : BitVec w) :
x.toNat.testBit i = x.getLsb i
@[simp]
theorem BitVec.getLsb_ofFin {n : Nat} (x : Fin (2 ^ n)) (i : Nat) :
{ toFin := x }.getLsb i = (x).testBit i
@[simp]
theorem BitVec.getLsb_ge {w : Nat} (x : BitVec w) (i : Nat) (ge : w i) :
x.getLsb i = false
@[simp]
theorem BitVec.getMsb_ge {w : Nat} (x : BitVec w) (i : Nat) (ge : w i) :
x.getMsb i = false
theorem BitVec.lt_of_getLsb {w : Nat} (x : BitVec w) (i : Nat) :
x.getLsb i = truei < w
theorem BitVec.lt_of_getMsb {w : Nat} (x : BitVec w) (i : Nat) :
x.getMsb i = truei < w
theorem BitVec.getMsb_eq_getLsb {w : Nat} (x : BitVec w) (i : Nat) :
x.getMsb i = (decide (i < w) && x.getLsb (w - 1 - i))
theorem BitVec.getLsb_eq_getMsb {w : Nat} (x : BitVec w) (i : Nat) :
x.getLsb i = (decide (i < w) && x.getMsb (w - 1 - i))
theorem BitVec.eq_of_getLsb_eq {w : Nat} {x : BitVec w} {y : BitVec w} (pred : ∀ (i : Fin w), x.getLsb i = y.getLsb i) :
x = y
theorem BitVec.eq_of_getMsb_eq {w : Nat} {x : BitVec w} {y : BitVec w} (pred : ∀ (i : Fin w), x.getMsb i = y.getMsb i) :
x = y
theorem BitVec.of_length_zero {x : BitVec 0} :
x = 0#0
@[simp]
theorem BitVec.toNat_zero_length (x : BitVec 0) :
x.toNat = 0
@[simp]
theorem BitVec.getLsb_zero_length {i : Nat} (x : BitVec 0) :
x.getLsb i = false
@[simp]
theorem BitVec.getMsb_zero_length {i : Nat} (x : BitVec 0) :
x.getMsb i = false
@[simp]
theorem BitVec.msb_zero_length (x : BitVec 0) :
x.msb = false
theorem BitVec.eq_of_toFin_eq {w : Nat} {x : BitVec w} {y : BitVec w} :
x.toFin = y.toFinx = y
@[simp]
theorem BitVec.toNat_ofBool (b : Bool) :
(BitVec.ofBool b).toNat = b.toNat
@[simp]
theorem BitVec.msb_ofBool (b : Bool) :
(BitVec.ofBool b).msb = b
@[simp]
theorem BitVec.toNat_ofFin {n : Nat} (x : Fin (2 ^ n)) :
{ toFin := x }.toNat = x
@[simp]
theorem BitVec.toNat_ofNatLt {w : Nat} (x : Nat) (p : x < 2 ^ w) :
(x#'p).toNat = x
@[simp]
theorem BitVec.getLsb_ofNatLt {n : Nat} (x : Nat) (lt : x < 2 ^ n) (i : Nat) :
(x#'lt).getLsb i = x.testBit i
@[simp]
theorem BitVec.toNat_ofNat (x : Nat) (w : Nat) :
(BitVec.ofNat w x).toNat = x % 2 ^ w
@[simp]
theorem BitVec.toFin_ofNat {w : Nat} (x : Nat) :
(BitVec.ofNat w x).toFin = Fin.ofNat' x
theorem BitVec.getLsb_ofNat (n : Nat) (x : Nat) (i : Nat) :
(BitVec.ofNat n x).getLsb i = (decide (i < n) && x.testBit i)
@[simp, deprecated BitVec.toNat_ofNat]
theorem BitVec.toNat_zero (n : Nat) :
(0#n).toNat = 0
@[simp]
theorem BitVec.getLsb_zero {w : Nat} {i : Nat} :
(0#w).getLsb i = false
@[simp]
theorem BitVec.getMsb_zero {w : Nat} {i : Nat} :
(0#w).getMsb i = false
@[simp]
theorem BitVec.toNat_mod_cancel {n : Nat} (x : BitVec n) :
x.toNat % 2 ^ n = x.toNat

msb #

@[simp]
theorem BitVec.msb_zero {w : Nat} :
(0#w).msb = false
theorem BitVec.msb_eq_getLsb_last {w : Nat} (x : BitVec w) :
x.msb = x.getLsb (w - 1)
theorem BitVec.getLsb_last {w : Nat} (x : BitVec w) :
x.getLsb (w - 1) = decide (2 ^ (w - 1) x.toNat)
theorem BitVec.getLsb_succ_last {w : Nat} (x : BitVec (w + 1)) :
x.getLsb w = decide (2 ^ w x.toNat)
theorem BitVec.msb_eq_decide {w : Nat} (x : BitVec w) :
x.msb = decide (2 ^ (w - 1) x.toNat)
theorem BitVec.toNat_ge_of_msb_true {n : Nat} {x : BitVec n} (p : x.msb = true) :
x.toNat 2 ^ (n - 1)

cast #

@[simp]
theorem BitVec.toNat_cast {w : Nat} {v : Nat} (h : w = v) (x : BitVec w) :
(BitVec.cast h x).toNat = x.toNat
@[simp]
theorem BitVec.toFin_cast {w : Nat} {v : Nat} (h : w = v) (x : BitVec w) :
(BitVec.cast h x).toFin = Fin.cast x.toFin
@[simp]
theorem BitVec.getLsb_cast {w : Nat} {v : Nat} {i : Nat} (h : w = v) (x : BitVec w) :
(BitVec.cast h x).getLsb i = x.getLsb i
@[simp]
theorem BitVec.getMsb_cast {w : Nat} {v : Nat} {i : Nat} (h : w = v) (x : BitVec w) :
(BitVec.cast h x).getMsb i = x.getMsb i
@[simp]
theorem BitVec.msb_cast {w : Nat} {v : Nat} (h : w = v) (x : BitVec w) :
(BitVec.cast h x).msb = x.msb

toInt/ofInt #

theorem BitVec.toInt_eq_toNat_cond {n : Nat} (i : BitVec n) :
i.toInt = if 2 * i.toNat < 2 ^ n then i.toNat else i.toNat - (2 ^ n)

Prove equality of bitvectors in terms of nat operations.

theorem BitVec.msb_eq_false_iff_two_mul_lt {w : Nat} (x : BitVec w) :
x.msb = false 2 * x.toNat < 2 ^ w
theorem BitVec.msb_eq_true_iff_two_mul_ge {w : Nat} (x : BitVec w) :
x.msb = true 2 * x.toNat 2 ^ w
theorem BitVec.toInt_eq_msb_cond {w : Nat} (x : BitVec w) :
x.toInt = if x.msb = true then x.toNat - (2 ^ w) else x.toNat

Characterize x.toInt in terms of x.msb.

theorem BitVec.toInt_eq_toNat_bmod {n : Nat} (x : BitVec n) :
x.toInt = (x.toNat).bmod (2 ^ n)
theorem BitVec.eq_of_toInt_eq {n : Nat} {i : BitVec n} {j : BitVec n} :
i.toInt = j.toInti = j

Prove equality of bitvectors in terms of nat operations.

theorem BitVec.toInt_inj {n : Nat} (x : BitVec n) (y : BitVec n) :
x.toInt = y.toInt x = y
theorem BitVec.toInt_ne {n : Nat} (x : BitVec n) (y : BitVec n) :
x.toInt y.toInt x y
@[simp]
theorem BitVec.toNat_ofInt {n : Nat} (i : Int) :
(BitVec.ofInt n i).toNat = (i % (2 ^ n)).toNat
theorem BitVec.toInt_ofNat {n : Nat} (x : Nat) :
(BitVec.ofNat n x).toInt = (x).bmod (2 ^ n)
@[simp]
theorem BitVec.toInt_ofInt {n : Nat} (i : Int) :
(BitVec.ofInt n i).toInt = i.bmod (2 ^ n)
@[simp]
theorem BitVec.ofInt_natCast (w : Nat) (n : Nat) :

zeroExtend and truncate #

@[simp]
theorem BitVec.toNat_zeroExtend' {m : Nat} {n : Nat} (p : m n) (x : BitVec m) :
(BitVec.zeroExtend' p x).toNat = x.toNat
theorem BitVec.toNat_zeroExtend {n : Nat} (i : Nat) (x : BitVec n) :
(BitVec.zeroExtend i x).toNat = x.toNat % 2 ^ i
theorem BitVec.zeroExtend'_eq {w : Nat} {v : Nat} {x : BitVec w} (h : w v) :
@[simp]
theorem BitVec.toNat_truncate {n : Nat} {i : Nat} (x : BitVec n) :
(BitVec.truncate i x).toNat = x.toNat % 2 ^ i
@[simp]
theorem BitVec.zeroExtend_eq {n : Nat} (x : BitVec n) :
@[simp]
theorem BitVec.zeroExtend_zero (m : Nat) (n : Nat) :
@[simp]
theorem BitVec.truncate_eq {n : Nat} (x : BitVec n) :
@[simp]
theorem BitVec.ofNat_toNat {n : Nat} (m : Nat) (x : BitVec n) :
theorem BitVec.toNat_eq_nat {w : Nat} (x : BitVec w) (y : Nat) :
x.toNat = y y < 2 ^ w x = BitVec.ofNat w y

Moves one-sided left toNat equality to BitVec equality.

theorem BitVec.nat_eq_toNat {w : Nat} (x : BitVec w) (y : Nat) :
y = x.toNat y < 2 ^ w x = BitVec.ofNat w y

Moves one-sided right toNat equality to BitVec equality.

@[simp]
theorem BitVec.getLsb_zeroExtend' {m : Nat} {n : Nat} (ge : m n) (x : BitVec n) (i : Nat) :
(BitVec.zeroExtend' ge x).getLsb i = x.getLsb i
@[simp]
theorem BitVec.getMsb_zeroExtend' {m : Nat} {n : Nat} (ge : m n) (x : BitVec n) (i : Nat) :
(BitVec.zeroExtend' ge x).getMsb i = (decide (i m - n) && x.getMsb (i - (m - n)))
@[simp]
theorem BitVec.getLsb_zeroExtend {n : Nat} (m : Nat) (x : BitVec n) (i : Nat) :
(BitVec.zeroExtend m x).getLsb i = (decide (i < m) && x.getLsb i)
@[simp]
theorem BitVec.getMsb_zeroExtend_add {w : Nat} {k : Nat} {i : Nat} {x : BitVec w} (h : k i) :
(BitVec.zeroExtend (w + k) x).getMsb i = x.getMsb (i - k)
@[simp]
theorem BitVec.getLsb_truncate {n : Nat} (m : Nat) (x : BitVec n) (i : Nat) :
(BitVec.truncate m x).getLsb i = (decide (i < m) && x.getLsb i)
theorem BitVec.msb_truncate {w : Nat} {k : Nat} (x : BitVec w) :
(BitVec.truncate (k + 1) x).msb = x.getLsb k
@[simp]
@[simp]
theorem BitVec.truncate_truncate_of_le {w : Nat} {k : Nat} {l : Nat} (x : BitVec w) (h : k l) :
@[simp]
theorem BitVec.truncate_cast {w : Nat} {v : Nat} {x : BitVec w} {k : Nat} {h : w = v} :
theorem BitVec.msb_zeroExtend {w : Nat} {v : Nat} (x : BitVec w) :
(BitVec.zeroExtend v x).msb = (decide (0 < v) && x.getLsb (v - 1))
theorem BitVec.msb_zeroExtend' {w : Nat} {v : Nat} (x : BitVec w) (h : w v) :
(BitVec.zeroExtend' h x).msb = (decide (0 < v) && x.getLsb (v - 1))

extractLsb #

@[simp]
theorem BitVec.extractLsb_ofFin {n : Nat} (x : Fin (2 ^ n)) (hi : Nat) (lo : Nat) :
BitVec.extractLsb hi lo { toFin := x } = BitVec.ofNat (hi - lo + 1) (x >>> lo)
@[simp]
theorem BitVec.extractLsb_ofNat (x : Nat) (n : Nat) (hi : Nat) (lo : Nat) :
BitVec.extractLsb hi lo (BitVec.ofNat n x) = BitVec.ofNat (hi - lo + 1) ((x % 2 ^ n) >>> lo)
@[simp]
theorem BitVec.extractLsb'_toNat {n : Nat} (s : Nat) (m : Nat) (x : BitVec n) :
(BitVec.extractLsb' s m x).toNat = x.toNat >>> s % 2 ^ m
@[simp]
theorem BitVec.extractLsb_toNat {n : Nat} (hi : Nat) (lo : Nat) (x : BitVec n) :
(BitVec.extractLsb hi lo x).toNat = x.toNat >>> lo % 2 ^ (hi - lo + 1)
@[simp]
theorem BitVec.getLsb_extract {n : Nat} (hi : Nat) (lo : Nat) (x : BitVec n) (i : Nat) :
(BitVec.extractLsb hi lo x).getLsb i = (decide (i hi - lo) && x.getLsb (lo + i))

allOnes #

@[simp]
theorem BitVec.toNat_allOnes {v : Nat} :
(BitVec.allOnes v).toNat = 2 ^ v - 1
@[simp]
theorem BitVec.getLsb_allOnes {v : Nat} {i : Nat} :
(BitVec.allOnes v).getLsb i = decide (i < v)

or #

@[simp]
theorem BitVec.toNat_or {v : Nat} (x : BitVec v) (y : BitVec v) :
(x ||| y).toNat = x.toNat ||| y.toNat
@[simp]
theorem BitVec.toFin_or {v : Nat} (x : BitVec v) (y : BitVec v) :
(x ||| y).toFin = x.toFin ||| y.toFin
@[simp]
theorem BitVec.getLsb_or {v : Nat} {i : Nat} {x : BitVec v} {y : BitVec v} :
(x ||| y).getLsb i = (x.getLsb i || y.getLsb i)
@[simp]
theorem BitVec.getMsb_or {w : Nat} {i : Nat} {x : BitVec w} {y : BitVec w} :
(x ||| y).getMsb i = (x.getMsb i || y.getMsb i)
@[simp]
theorem BitVec.msb_or {w : Nat} {x : BitVec w} {y : BitVec w} :
(x ||| y).msb = (x.msb || y.msb)
@[simp]
theorem BitVec.truncate_or {w : Nat} {k : Nat} {x : BitVec w} {y : BitVec w} :
theorem BitVec.or_assoc {w : Nat} (x : BitVec w) (y : BitVec w) (z : BitVec w) :
x ||| y ||| z = x ||| (y ||| z)

and #

@[simp]
theorem BitVec.toNat_and {v : Nat} (x : BitVec v) (y : BitVec v) :
(x &&& y).toNat = x.toNat &&& y.toNat
@[simp]
theorem BitVec.toFin_and {v : Nat} (x : BitVec v) (y : BitVec v) :
(x &&& y).toFin = x.toFin &&& y.toFin
@[simp]
theorem BitVec.getLsb_and {v : Nat} {i : Nat} {x : BitVec v} {y : BitVec v} :
(x &&& y).getLsb i = (x.getLsb i && y.getLsb i)
@[simp]
theorem BitVec.getMsb_and {w : Nat} {i : Nat} {x : BitVec w} {y : BitVec w} :
(x &&& y).getMsb i = (x.getMsb i && y.getMsb i)
@[simp]
theorem BitVec.msb_and {w : Nat} {x : BitVec w} {y : BitVec w} :
(x &&& y).msb = (x.msb && y.msb)
@[simp]
theorem BitVec.truncate_and {w : Nat} {k : Nat} {x : BitVec w} {y : BitVec w} :
theorem BitVec.and_assoc {w : Nat} (x : BitVec w) (y : BitVec w) (z : BitVec w) :
x &&& y &&& z = x &&& (y &&& z)

xor #

@[simp]
theorem BitVec.toNat_xor {v : Nat} (x : BitVec v) (y : BitVec v) :
(x ^^^ y).toNat = x.toNat ^^^ y.toNat
@[simp]
theorem BitVec.toFin_xor {v : Nat} (x : BitVec v) (y : BitVec v) :
(x ^^^ y).toFin = x.toFin ^^^ y.toFin
@[simp]
theorem BitVec.getLsb_xor {v : Nat} {i : Nat} {x : BitVec v} {y : BitVec v} :
(x ^^^ y).getLsb i = xor (x.getLsb i) (y.getLsb i)
@[simp]
theorem BitVec.truncate_xor {w : Nat} {k : Nat} {x : BitVec w} {y : BitVec w} :
theorem BitVec.xor_assoc {w : Nat} (x : BitVec w) (y : BitVec w) (z : BitVec w) :
x ^^^ y ^^^ z = x ^^^ (y ^^^ z)

not #

theorem BitVec.not_def {v : Nat} {x : BitVec v} :
@[simp]
theorem BitVec.toNat_not {v : Nat} {x : BitVec v} :
(~~~x).toNat = 2 ^ v - 1 - x.toNat
@[simp]
theorem BitVec.toFin_not {w : Nat} (x : BitVec w) :
(~~~x).toFin = x.toFin.rev
@[simp]
theorem BitVec.getLsb_not {v : Nat} {i : Nat} {x : BitVec v} :
(~~~x).getLsb i = (decide (i < v) && !x.getLsb i)
@[simp]
theorem BitVec.truncate_not {w : Nat} {k : Nat} {x : BitVec w} (h : k w) :

cast #

@[simp]
theorem BitVec.not_cast {w : Nat} {w' : Nat} {x : BitVec w} (h : w = w') :
@[simp]
theorem BitVec.and_cast {w : Nat} {w' : Nat} {x : BitVec w} {y : BitVec w} (h : w = w') :
@[simp]
theorem BitVec.or_cast {w : Nat} {w' : Nat} {x : BitVec w} {y : BitVec w} (h : w = w') :
@[simp]
theorem BitVec.xor_cast {w : Nat} {w' : Nat} {x : BitVec w} {y : BitVec w} (h : w = w') :

shiftLeft #

@[simp]
theorem BitVec.toNat_shiftLeft {v : Nat} {n : Nat} {x : BitVec v} :
(x <<< n).toNat = x.toNat <<< n % 2 ^ v
@[simp]
theorem BitVec.toFin_shiftLeft {w : Nat} {n : Nat} (x : BitVec w) :
(x <<< n).toFin = Fin.ofNat' (x.toNat <<< n)
@[simp]
theorem BitVec.getLsb_shiftLeft {m : Nat} {i : Nat} (x : BitVec m) (n : Nat) :
(x <<< n).getLsb i = (decide (i < m) && !decide (i < n) && x.getLsb (i - n))
@[simp]
theorem BitVec.getMsb_shiftLeft {w : Nat} {k : Nat} (x : BitVec w) (i : Nat) :
(x <<< i).getMsb k = x.getMsb (k + i)
theorem BitVec.shiftLeftZeroExtend_eq {w : Nat} {n : Nat} {x : BitVec w} :
x.shiftLeftZeroExtend n = BitVec.zeroExtend (w + n) x <<< n
@[simp]
theorem BitVec.getLsb_shiftLeftZeroExtend {m : Nat} {i : Nat} (x : BitVec m) (n : Nat) :
(x.shiftLeftZeroExtend n).getLsb i = (!decide (i < n) && x.getLsb (i - n))
@[simp]
theorem BitVec.getMsb_shiftLeftZeroExtend {m : Nat} {i : Nat} (x : BitVec m) (n : Nat) :
(x.shiftLeftZeroExtend n).getMsb i = x.getMsb i
@[simp]
theorem BitVec.msb_shiftLeftZeroExtend {w : Nat} (x : BitVec w) (i : Nat) :
(x.shiftLeftZeroExtend i).msb = x.msb
theorem BitVec.shiftLeft_add {w : Nat} (x : BitVec w) (n : Nat) (m : Nat) :
x <<< (n + m) = x <<< n <<< m
@[deprecated BitVec.shiftLeft_add]
theorem BitVec.shiftLeft_shiftLeft {w : Nat} (x : BitVec w) (n : Nat) (m : Nat) :
x <<< n <<< m = x <<< (n + m)

ushiftRight #

@[simp]
theorem BitVec.toNat_ushiftRight {n : Nat} (x : BitVec n) (i : Nat) :
(x >>> i).toNat = x.toNat >>> i
@[simp]
theorem BitVec.getLsb_ushiftRight {n : Nat} (x : BitVec n) (i : Nat) (j : Nat) :
(x >>> i).getLsb j = x.getLsb (i + j)

sshiftRight #

theorem BitVec.sshiftRight_eq {n : Nat} {x : BitVec n} {i : Nat} :
x.sshiftRight i = BitVec.ofInt n (x.toInt >>> i)
theorem BitVec.sshiftRight_eq_of_msb_false {w : Nat} {x : BitVec w} {s : Nat} (h : x.msb = false) :
x.sshiftRight s = x >>> s

if the msb is false, the arithmetic shift right equals logical shift right

theorem BitVec.sshiftRight_eq_of_msb_true {w : Nat} {x : BitVec w} {s : Nat} (h : x.msb = true) :
x.sshiftRight s = ~~~(~~~x >>> s)

If the msb is true, the arithmetic shift right equals negating, then logical shifting right, then negating again. The double negation preserves the lower bits that have been shifted, and the outer negation ensures that the high bits are '1'.

theorem BitVec.getLsb_sshiftRight {w : Nat} (x : BitVec w) (s : Nat) (i : Nat) :
(x.sshiftRight s).getLsb i = (!decide (w i) && if s + i < w then x.getLsb (s + i) else x.msb)

signExtend #

The sign extension is the same as zero extending when msb = false.

The sign extension is a bitwise not, followed by a zero extend, followed by another bitwise not when msb = true. The double bitwise not ensures that the high bits are '1', and the lower bits are preserved.

@[simp]
theorem BitVec.getLsb_signExtend {w : Nat} (x : BitVec w) {v : Nat} {i : Nat} :
(BitVec.signExtend v x).getLsb i = (decide (i < v) && if i < w then x.getLsb i else x.msb)

append #

theorem BitVec.append_def {v : Nat} {w : Nat} (x : BitVec v) (y : BitVec w) :
x ++ y = x.shiftLeftZeroExtend w ||| BitVec.zeroExtend' y
@[simp]
theorem BitVec.toNat_append {m : Nat} {n : Nat} (x : BitVec m) (y : BitVec n) :
(x ++ y).toNat = x.toNat <<< n ||| y.toNat
@[simp]
theorem BitVec.getLsb_append {n : Nat} {m : Nat} {i : Nat} {v : BitVec n} {w : BitVec m} :
(v ++ w).getLsb i = bif decide (i < m) then w.getLsb i else v.getLsb (i - m)
@[simp]
theorem BitVec.getMsb_append {n : Nat} {m : Nat} {i : Nat} {v : BitVec n} {w : BitVec m} :
(v ++ w).getMsb i = bif decide (n i) then w.getMsb (i - n) else v.getMsb i
theorem BitVec.msb_append {w : Nat} {v : Nat} {x : BitVec w} {y : BitVec v} :
(x ++ y).msb = bif w == 0 then y.msb else x.msb
@[simp]
theorem BitVec.truncate_append {w : Nat} {v : Nat} {k : Nat} {x : BitVec w} {y : BitVec v} :
BitVec.truncate k (x ++ y) = if h : k v then BitVec.truncate k y else BitVec.cast (BitVec.truncate (k - v) x ++ y)
@[simp]
theorem BitVec.truncate_cons {w : Nat} {a : Bool} {x : BitVec w} :
@[simp]
theorem BitVec.not_append {w : Nat} {v : Nat} {x : BitVec w} {y : BitVec v} :
~~~(x ++ y) = ~~~x ++ ~~~y
@[simp]
theorem BitVec.and_append {w : Nat} {v : Nat} {x₁ : BitVec w} {x₂ : BitVec w} {y₁ : BitVec v} {y₂ : BitVec v} :
x₁ ++ y₁ &&& x₂ ++ y₂ = (x₁ &&& x₂) ++ (y₁ &&& y₂)
@[simp]
theorem BitVec.or_append {w : Nat} {v : Nat} {x₁ : BitVec w} {x₂ : BitVec w} {y₁ : BitVec v} {y₂ : BitVec v} :
x₁ ++ y₁ ||| x₂ ++ y₂ = (x₁ ||| x₂) ++ (y₁ ||| y₂)
@[simp]
theorem BitVec.xor_append {w : Nat} {v : Nat} {x₁ : BitVec w} {x₂ : BitVec w} {y₁ : BitVec v} {y₂ : BitVec v} :
x₁ ++ y₁ ^^^ x₂ ++ y₂ = (x₁ ^^^ x₂) ++ (y₁ ^^^ y₂)
theorem BitVec.shiftRight_add {w : Nat} (x : BitVec w) (n : Nat) (m : Nat) :
x >>> (n + m) = x >>> n >>> m
@[deprecated BitVec.shiftRight_add]
theorem BitVec.shiftRight_shiftRight {w : Nat} (x : BitVec w) (n : Nat) (m : Nat) :
x >>> n >>> m = x >>> (n + m)

rev #

theorem BitVec.getLsb_rev {w : Nat} (x : BitVec w) (i : Fin w) :
x.getLsb i.rev = x.getMsb i
theorem BitVec.getMsb_rev {w : Nat} (x : BitVec w) (i : Fin w) :
x.getMsb i.rev = x.getLsb i

cons #

@[simp]
theorem BitVec.toNat_cons {w : Nat} (b : Bool) (x : BitVec w) :
(BitVec.cons b x).toNat = b.toNat <<< w ||| x.toNat
theorem BitVec.toNat_cons' {w : Nat} {a : Bool} {x : BitVec w} :
(BitVec.cons a x).toNat = a.toNat <<< w + x.toNat

Variant of toNat_cons using + instead of |||.

@[simp]
theorem BitVec.getLsb_cons (b : Bool) {n : Nat} (x : BitVec n) (i : Nat) :
(BitVec.cons b x).getLsb i = if i = n then b else x.getLsb i
@[simp]
theorem BitVec.msb_cons {a : Bool} :
∀ {w : Nat} {x : BitVec w}, (BitVec.cons a x).msb = a
@[simp]
theorem BitVec.getMsb_cons_zero {a : Bool} :
∀ {w : Nat} {x : BitVec w}, (BitVec.cons a x).getMsb 0 = a
@[simp]
theorem BitVec.getMsb_cons_succ {a : Bool} :
∀ {w : Nat} {x : BitVec w} {i : Nat}, (BitVec.cons a x).getMsb (i + 1) = x.getMsb i
theorem BitVec.truncate_succ {w : Nat} {i : Nat} (x : BitVec w) :
BitVec.truncate (i + 1) x = BitVec.cons (x.getLsb i) (BitVec.truncate i x)
theorem BitVec.eq_msb_cons_truncate {w : Nat} (x : BitVec (w + 1)) :
@[simp]
theorem BitVec.not_cons {w : Nat} (x : BitVec w) (b : Bool) :
@[simp]
theorem BitVec.cons_or_cons {w : Nat} (x : BitVec w) (y : BitVec w) (a : Bool) (b : Bool) :
@[simp]
theorem BitVec.cons_and_cons {w : Nat} (x : BitVec w) (y : BitVec w) (a : Bool) (b : Bool) :
@[simp]
theorem BitVec.cons_xor_cons {w : Nat} (x : BitVec w) (y : BitVec w) (a : Bool) (b : Bool) :

concat #

@[simp]
theorem BitVec.toNat_concat {w : Nat} (x : BitVec w) (b : Bool) :
(x.concat b).toNat = x.toNat * 2 + b.toNat
theorem BitVec.getLsb_concat {w : Nat} (x : BitVec w) (b : Bool) (i : Nat) :
(x.concat b).getLsb i = if i = 0 then b else x.getLsb (i - 1)
@[simp]
theorem BitVec.getLsb_concat_zero :
∀ {w : Nat} {x : BitVec w} {b : Bool}, (x.concat b).getLsb 0 = b
@[simp]
theorem BitVec.getLsb_concat_succ :
∀ {w : Nat} {x : BitVec w} {b : Bool} {i : Nat}, (x.concat b).getLsb (i + 1) = x.getLsb i
@[simp]
theorem BitVec.not_concat {w : Nat} (x : BitVec w) (b : Bool) :
~~~x.concat b = (~~~x).concat !b
@[simp]
theorem BitVec.concat_or_concat {w : Nat} (x : BitVec w) (y : BitVec w) (a : Bool) (b : Bool) :
x.concat a ||| y.concat b = (x ||| y).concat (a || b)
@[simp]
theorem BitVec.concat_and_concat {w : Nat} (x : BitVec w) (y : BitVec w) (a : Bool) (b : Bool) :
x.concat a &&& y.concat b = (x &&& y).concat (a && b)
@[simp]
theorem BitVec.concat_xor_concat {w : Nat} (x : BitVec w) (y : BitVec w) (a : Bool) (b : Bool) :
x.concat a ^^^ y.concat b = (x ^^^ y).concat (xor a b)

add #

theorem BitVec.add_def {n : Nat} (x : BitVec n) (y : BitVec n) :
x + y = BitVec.ofNat n (x.toNat + y.toNat)
@[simp]
theorem BitVec.toNat_add {w : Nat} (x : BitVec w) (y : BitVec w) :
(x + y).toNat = (x.toNat + y.toNat) % 2 ^ w

Definition of bitvector addition as a nat.

@[simp]
theorem BitVec.toFin_add {w : Nat} (x : BitVec w) (y : BitVec w) :
(x + y).toFin = x.toFin + y.toFin
@[simp]
theorem BitVec.ofFin_add {n : Nat} (x : Fin (2 ^ n)) (y : BitVec n) :
{ toFin := x } + y = { toFin := x + y.toFin }
@[simp]
theorem BitVec.add_ofFin {n : Nat} (x : BitVec n) (y : Fin (2 ^ n)) :
x + { toFin := y } = { toFin := x.toFin + y }
theorem BitVec.ofNat_add {n : Nat} (x : Nat) (y : Nat) :
theorem BitVec.ofNat_add_ofNat {n : Nat} (x : Nat) (y : Nat) :
theorem BitVec.add_assoc {n : Nat} (x : BitVec n) (y : BitVec n) (z : BitVec n) :
x + y + z = x + (y + z)
instance BitVec.instAssociativeHAdd {n : Nat} :
Std.Associative fun (x x_1 : BitVec n) => x + x_1
Equations
  • =
theorem BitVec.add_comm {n : Nat} (x : BitVec n) (y : BitVec n) :
x + y = y + x
instance BitVec.instCommutativeHAdd {n : Nat} :
Std.Commutative fun (x x_1 : BitVec n) => x + x_1
Equations
  • =
@[simp]
theorem BitVec.add_zero {n : Nat} (x : BitVec n) :
x + 0#n = x
@[simp]
theorem BitVec.zero_add {n : Nat} (x : BitVec n) :
0#n + x = x
instance BitVec.instLawfulIdentityHAddOfNatOfNatNat {n : Nat} :
Std.LawfulIdentity (fun (x x_1 : BitVec n) => x + x_1) 0#n
Equations
  • =
theorem BitVec.truncate_add {w : Nat} {i : Nat} (x : BitVec w) (y : BitVec w) (h : i w) :
@[simp]
theorem BitVec.toInt_add {w : Nat} (x : BitVec w) (y : BitVec w) :
(x + y).toInt = (x.toInt + y.toInt).bmod (2 ^ w)
theorem BitVec.ofInt_add {n : Nat} (x : Int) (y : Int) :

sub/neg #

theorem BitVec.sub_def {n : Nat} (x : BitVec n) (y : BitVec n) :
x - y = BitVec.ofNat n (2 ^ n - y.toNat + x.toNat)
@[simp]
theorem BitVec.toNat_sub {n : Nat} (x : BitVec n) (y : BitVec n) :
(x - y).toNat = (2 ^ n - y.toNat + x.toNat) % 2 ^ n
theorem BitVec.toNat_sub' {n : Nat} (x : BitVec n) (y : BitVec n) :
(x - y).toNat = (x.toNat + (2 ^ n - y.toNat)) % 2 ^ n
@[simp]
theorem BitVec.toFin_sub {n : Nat} (x : BitVec n) (y : BitVec n) :
(x - y).toFin = x.toFin - y.toFin
@[simp]
theorem BitVec.ofFin_sub {n : Nat} (x : Fin (2 ^ n)) (y : BitVec n) :
{ toFin := x } - y = { toFin := x - y.toFin }
@[simp]
theorem BitVec.sub_ofFin {n : Nat} (x : BitVec n) (y : Fin (2 ^ n)) :
x - { toFin := y } = { toFin := x.toFin - y }
theorem BitVec.ofNat_sub_ofNat {n : Nat} (x : Nat) (y : Nat) :
BitVec.ofNat n x - BitVec.ofNat n y = BitVec.ofNat n (2 ^ n - y % 2 ^ n + x)
@[simp]
theorem BitVec.sub_zero {n : Nat} (x : BitVec n) :
x - 0#n = x
@[simp]
theorem BitVec.sub_self {n : Nat} (x : BitVec n) :
x - x = 0#n
@[simp]
theorem BitVec.toNat_neg {n : Nat} (x : BitVec n) :
(-x).toNat = (2 ^ n - x.toNat) % 2 ^ n
@[simp]
theorem BitVec.toFin_neg {n : Nat} (x : BitVec n) :
(-x).toFin = Fin.ofNat' (2 ^ n - x.toNat)
theorem BitVec.sub_toAdd {n : Nat} (x : BitVec n) (y : BitVec n) :
x - y = x + -y
@[simp]
theorem BitVec.neg_zero (n : Nat) :
-0#n = 0#n
theorem BitVec.add_sub_cancel {w : Nat} (x : BitVec w) (y : BitVec w) :
x + y - y = x
theorem BitVec.sub_add_cancel {w : Nat} (x : BitVec w) (y : BitVec w) :
x - y + y = x
theorem BitVec.eq_sub_iff_add_eq {w : Nat} {x : BitVec w} {y : BitVec w} {z : BitVec w} :
x = z - y x + y = z
theorem BitVec.neg_eq_not_add {w : Nat} (x : BitVec w) :
-x = ~~~x + 1

mul #

theorem BitVec.mul_def {n : Nat} {x : BitVec n} {y : BitVec n} :
x * y = { toFin := x.toFin * y.toFin }
@[simp]
theorem BitVec.toNat_mul {n : Nat} (x : BitVec n) (y : BitVec n) :
(x * y).toNat = x.toNat * y.toNat % 2 ^ n
@[simp]
theorem BitVec.toFin_mul {n : Nat} (x : BitVec n) (y : BitVec n) :
(x * y).toFin = x.toFin * y.toFin
theorem BitVec.mul_comm {w : Nat} (x : BitVec w) (y : BitVec w) :
x * y = y * x
instance BitVec.instCommutativeHMul {w : Nat} :
Std.Commutative fun (x y : BitVec w) => x * y
Equations
  • =
theorem BitVec.mul_assoc {w : Nat} (x : BitVec w) (y : BitVec w) (z : BitVec w) :
x * y * z = x * (y * z)
instance BitVec.instAssociativeHMul {w : Nat} :
Std.Associative fun (x y : BitVec w) => x * y
Equations
  • =
@[simp]
theorem BitVec.mul_one {w : Nat} (x : BitVec w) :
x * 1#w = x
@[simp]
theorem BitVec.one_mul {w : Nat} (x : BitVec w) :
1#w * x = x
Equations
  • =
@[simp]
theorem BitVec.toInt_mul {w : Nat} (x : BitVec w) (y : BitVec w) :
(x * y).toInt = (x.toInt * y.toInt).bmod (2 ^ w)
theorem BitVec.ofInt_mul {n : Nat} (x : Int) (y : Int) :

le and lt #

theorem BitVec.le_def {n : Nat} (x : BitVec n) (y : BitVec n) :
x y x.toNat y.toNat
@[simp]
theorem BitVec.le_ofFin {n : Nat} (x : BitVec n) (y : Fin (2 ^ n)) :
x { toFin := y } x.toFin y
@[simp]
theorem BitVec.ofFin_le {n : Nat} (x : Fin (2 ^ n)) (y : BitVec n) :
{ toFin := x } y x y.toFin
@[simp]
theorem BitVec.ofNat_le_ofNat {n : Nat} (x : Nat) (y : Nat) :
BitVec.ofNat n x BitVec.ofNat n y x % 2 ^ n y % 2 ^ n
theorem BitVec.lt_def {n : Nat} (x : BitVec n) (y : BitVec n) :
x < y x.toNat < y.toNat
@[simp]
theorem BitVec.lt_ofFin {n : Nat} (x : BitVec n) (y : Fin (2 ^ n)) :
x < { toFin := y } x.toFin < y
@[simp]
theorem BitVec.ofFin_lt {n : Nat} (x : Fin (2 ^ n)) (y : BitVec n) :
{ toFin := x } < y x < y.toFin
@[simp]
theorem BitVec.ofNat_lt_ofNat {n : Nat} (x : Nat) (y : Nat) :
BitVec.ofNat n x < BitVec.ofNat n y x % 2 ^ n < y % 2 ^ n
theorem BitVec.lt_of_le_ne {n : Nat} (x : BitVec n) (y : BitVec n) (h1 : x y) (h2 : ¬x = y) :
x < y

intMax #

def BitVec.intMax (w : Nat) :

The bitvector of width w that has the largest value when interpreted as an integer.

Equations
Instances For
    theorem BitVec.getLsb_intMax_eq {i : Nat} (w : Nat) :
    (BitVec.intMax w).getLsb i = decide (i < w)
    theorem BitVec.toNat_intMax_eq {w : Nat} :
    (BitVec.intMax w).toNat = 2 ^ w - 1

    ofBoolList #

    @[simp]
    theorem BitVec.getMsb_ofBoolListBE {bs : List Bool} {i : Nat} :
    (BitVec.ofBoolListBE bs).getMsb i = bs.getD i false
    @[simp]
    theorem BitVec.getLsb_ofBoolListBE {bs : List Bool} {i : Nat} :
    (BitVec.ofBoolListBE bs).getLsb i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false)
    @[simp]
    theorem BitVec.getLsb_ofBoolListLE {bs : List Bool} {i : Nat} :
    (BitVec.ofBoolListLE bs).getLsb i = bs.getD i false
    @[simp]
    theorem BitVec.getMsb_ofBoolListLE {bs : List Bool} {i : Nat} :
    (BitVec.ofBoolListLE bs).getMsb i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false)

    Rotate Left #

    @[simp]
    theorem BitVec.rotateLeft_mod_eq_rotateLeft {w : Nat} {x : BitVec w} {r : Nat} :
    x.rotateLeft (r % w) = x.rotateLeft r

    rotateLeft is invariant under mod by the bitwidth.

    theorem BitVec.rotateLeft_eq_rotateLeftAux_of_lt {w : Nat} {x : BitVec w} {r : Nat} (hr : r < w) :
    x.rotateLeft r = x.rotateLeftAux r

    rotateLeft equals the bit fiddling definition of rotateLeftAux when the rotation amount is smaller than the bitwidth.

    theorem BitVec.getLsb_rotateLeftAux_of_le {w : Nat} {x : BitVec w} {r : Nat} {i : Nat} (hi : i < r) :
    (x.rotateLeftAux r).getLsb i = x.getLsb (w - r + i)

    Accessing bits in x.rotateLeft r the range [0, r) is equal to accessing bits x in the range [w - r, w).

    Proof by example: Let x := <6 5 4 3 2 1 0> : BitVec 7. x.rotateLeft 2 = (<6 5 | 4 3 2 1 0>).rotateLeft 2 = <3 2 1 0 | 6 5>

    (x.rotateLeft 2).getLsb ⟨i, i < 2⟩ = <3 2 1 0 | 6 5>.getLsb ⟨i, i < 2⟩ = <6 5>[i] = <6 5 | 4 3 2 1 0>[i + len(<4 3 2 1 0>)] = <6 5 | 4 3 2 1 0>[i + 7 - 2]

    theorem BitVec.getLsb_rotateLeftAux_of_geq {w : Nat} {x : BitVec w} {r : Nat} {i : Nat} (hi : i r) :
    (x.rotateLeftAux r).getLsb i = (decide (i < w) && x.getLsb (i - r))

    Accessing bits in x.rotateLeft r the range [r, w) is equal to accessing bits x in the range [0, w - r).

    Proof by example: Let x := <6 5 4 3 2 1 0> : BitVec 7. x.rotateLeft 2 = (<6 5 | 4 3 2 1 0>).rotateLeft 2 = <3 2 1 0 | 6 5>

    (x.rotateLeft 2).getLsb ⟨i, i ≥ 2⟩ = <3 2 1 0 | 6 5>.getLsb ⟨i, i ≥ 2⟩ = <3 2 1 0>[i - 2] = <6 5 | 3 2 1 0>[i - 2]

    Intuitively, grab the full width (7), then move the marker | by r to the right (-2) Then, access the bit at i from the right (+i).

    theorem BitVec.getLsb_rotateLeft_of_le {w : Nat} {x : BitVec w} {r : Nat} {i : Nat} (hr : r < w) :
    (x.rotateLeft r).getLsb i = bif decide (i < r) then x.getLsb (w - r + i) else decide (i < w) && x.getLsb (i - r)

    When r < w, we give a formula for (x.rotateRight r).getLsb i.

    @[simp]
    theorem BitVec.getLsb_rotateLeft {w : Nat} {x : BitVec w} {r : Nat} {i : Nat} :
    (x.rotateLeft r).getLsb i = bif decide (i < r % w) then x.getLsb (w - r % w + i) else decide (i < w) && x.getLsb (i - r % w)

    Rotate Right #

    theorem BitVec.getLsb_rotateRightAux_of_le {w : Nat} {x : BitVec w} {r : Nat} {i : Nat} (hi : i < w - r) :
    (x.rotateRightAux r).getLsb i = x.getLsb (r + i)

    Accessing bits in x.rotateRight r the range [0, w-r) is equal to accessing bits x in the range [r, w).

    Proof by example: Let x := <6 5 4 3 2 1 0> : BitVec 7. x.rotateRight 2 = (<6 5 4 3 2 | 1 0>).rotateRight 2 = <1 0 | 6 5 4 3 2>

    (x.rotateLeft 2).getLsb ⟨i, i ≤ 7 - 2⟩ = <1 0 | 6 5 4 3 2>.getLsb ⟨i, i ≤ 7 - 2⟩ = <6 5 4 3 2>.getLsb i = <6 5 4 3 2 | 1 0>[i + 2]

    theorem BitVec.getLsb_rotateRightAux_of_geq {w : Nat} {x : BitVec w} {r : Nat} {i : Nat} (hi : i w - r) :
    (x.rotateRightAux r).getLsb i = (decide (i < w) && x.getLsb (i - (w - r)))

    Accessing bits in x.rotateRight r the range [w-r, w) is equal to accessing bits x in the range [0, r).

    Proof by example: Let x := <6 5 4 3 2 1 0> : BitVec 7. x.rotateRight 2 = (<6 5 4 3 2 | 1 0>).rotateRight 2 = <1 0 | 6 5 4 3 2>

    (x.rotateLeft 2).getLsb ⟨i, i ≥ 7 - 2⟩ = <1 0 | 6 5 4 3 2>.getLsb ⟨i, i ≤ 7 - 2⟩ = <1 0>.getLsb (i - len(<6 5 4 3 2>) = <6 5 4 3 2 | 1 0> (i - len<6 4 4 3 2>)

    theorem BitVec.rotateRight_eq_rotateRightAux_of_lt {w : Nat} {x : BitVec w} {r : Nat} (hr : r < w) :
    x.rotateRight r = x.rotateRightAux r

    rotateRight equals the bit fiddling definition of rotateRightAux when the rotation amount is smaller than the bitwidth.

    @[simp]
    theorem BitVec.rotateRight_mod_eq_rotateRight {w : Nat} {x : BitVec w} {r : Nat} :
    x.rotateRight (r % w) = x.rotateRight r

    rotateRight is invariant under mod by the bitwidth.

    theorem BitVec.getLsb_rotateRight_of_le {w : Nat} {x : BitVec w} {r : Nat} {i : Nat} (hr : r < w) :
    (x.rotateRight r).getLsb i = bif decide (i < w - r) then x.getLsb (r + i) else decide (i < w) && x.getLsb (i - (w - r))

    When r < w, we give a formula for (x.rotateRight r).getLsb i.

    @[simp]
    theorem BitVec.getLsb_rotateRight {w : Nat} {x : BitVec w} {r : Nat} {i : Nat} :
    (x.rotateRight r).getLsb i = bif decide (i < w - r % w) then x.getLsb (r % w + i) else decide (i < w) && x.getLsb (i - (w - r % w))
    @[simp]
    theorem BitVec.toNat_twoPow (w : Nat) (i : Nat) :
    (BitVec.twoPow w i).toNat = 2 ^ i % 2 ^ w
    @[simp]
    theorem BitVec.getLsb_twoPow {w : Nat} (i : Nat) (j : Nat) :
    (BitVec.twoPow w i).getLsb j = (decide (i < w) && decide (i = j))
    theorem BitVec.and_twoPow_eq {w : Nat} (x : BitVec w) (i : Nat) :
    x &&& BitVec.twoPow w i = if x.getLsb i = true then BitVec.twoPow w i else 0#w
    @[simp]
    theorem BitVec.mul_twoPow_eq_shiftLeft {w : Nat} (x : BitVec w) (i : Nat) :
    x * BitVec.twoPow w i = x <<< i