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

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.toNat → i = 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 = true → i < w

theorem BitVec.lt_of_getMsb {w : Nat} (x : BitVec w) (i : Nat) : x.getMsb i = true → i < 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.toFin → x = 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

theorem BitVec.ofNat_one (n : Nat) : n#1 = BitVec.ofBool (decide (n % 2 = 1))

theorem BitVec.ofBool_eq_iff_eq (b : Bool) (b' : Bool) : BitVec.ofBool b = BitVec.ofBool b' ↔ b = b'

@[simp]

theorem BitVec.not_ofBool {b : Bool} : ~~~BitVec.ofBool b = BitVec.ofBool !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) : (x#w).toNat = x % 2 ^ w

theorem BitVec.getLsb_ofNat (n : Nat) (x : Nat) (i : Nat) : (x#n).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.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.toInt → i = j

Prove equality of bitvectors in terms of nat operations.

@[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) : (x#n).toInt = (↑x).bmod (2 ^ n)

@[simp]

theorem BitVec.toInt_ofInt {n : Nat} (i : Int) : (BitVec.ofInt n i).toInt = i.bmod (2 ^ n)

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) : BitVec.zeroExtend' h x = BitVec.zeroExtend v x

@[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) : BitVec.zeroExtend n x = x

@[simp]

theorem BitVec.zeroExtend_zero (m : Nat) (n : Nat) : BitVec.zeroExtend m 0#n = 0#m

@[simp]

theorem BitVec.truncate_eq {n : Nat} (x : BitVec n) : BitVec.truncate n x = x

@[simp]

theorem BitVec.ofNat_toNat {n : Nat} (m : Nat) (x : BitVec n) : x.toNat#m = BitVec.truncate m x

theorem BitVec.toNat_eq_nat {w : Nat} (x : BitVec w) (y : Nat) : x.toNat = y ↔ y < 2 ^ w ∧ x = y#w

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 = y#w

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]

theorem BitVec.zeroExtend_zeroExtend_of_le {w : Nat} {k : Nat} {l : Nat} (x : BitVec w) (h : k ≤ l) : BitVec.zeroExtend k (BitVec.zeroExtend l x) = BitVec.zeroExtend k x

@[simp]

theorem BitVec.truncate_truncate_of_le {w : Nat} {k : Nat} {l : Nat} (x : BitVec w) (h : k ≤ l) : BitVec.truncate k (BitVec.truncate l x) = BitVec.truncate k x

@[simp]

theorem BitVec.truncate_cast {w : Nat} {v : Nat} {x : BitVec w} {k : Nat} {h : w = v} : BitVec.truncate k (BitVec.cast h x) = BitVec.truncate k x

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 } = (↑x >>> lo)#(hi - lo + 1)

@[simp]

theorem BitVec.extractLsb_ofNat (x : Nat) (n : Nat) (hi : Nat) (lo : Nat) : BitVec.extractLsb hi lo x#n = ((x % 2 ^ n) >>> lo)#(hi - lo + 1)

@[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} : BitVec.truncate k (x ||| y) = BitVec.truncate k x ||| BitVec.truncate k y

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} : BitVec.truncate k (x &&& y) = BitVec.truncate k x &&& BitVec.truncate k y

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} : BitVec.truncate k (x ^^^ y) = BitVec.truncate k x ^^^ BitVec.truncate k y

not

theorem BitVec.not_def {v : Nat} {x : BitVec v} : ~~~x = BitVec.allOnes v ^^^ x

@[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) : BitVec.truncate k (~~~x) = ~~~BitVec.truncate k x

cast

@[simp]

theorem BitVec.not_cast {w : Nat} {w' : Nat} {x : BitVec w} (h : w = w') : ~~~BitVec.cast h x = BitVec.cast h (~~~x)

@[simp]

theorem BitVec.and_cast {w : Nat} {w' : Nat} {x : BitVec w} {y : BitVec w} (h : w = w') : BitVec.cast h x &&& BitVec.cast h y = BitVec.cast h (x &&& y)

@[simp]

theorem BitVec.or_cast {w : Nat} {w' : Nat} {x : BitVec w} {y : BitVec w} (h : w = w') : BitVec.cast h x ||| BitVec.cast h y = BitVec.cast h (x ||| y)

@[simp]

theorem BitVec.xor_cast {w : Nat} {w' : Nat} {x : BitVec w} {y : BitVec w} (h : w = w') : BitVec.cast h x &&& BitVec.cast h y = BitVec.cast h (x &&& y)

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

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)

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} : BitVec.truncate w (BitVec.cons a x) = x

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

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)) : x = BitVec.cons x.msb (BitVec.truncate w x)

@[simp]

theorem BitVec.not_cons {w : Nat} (x : BitVec w) (b : Bool) : ~~~BitVec.cons b x = BitVec.cons (!b) (~~~x)

@[simp]

theorem BitVec.cons_or_cons {w : Nat} (x : BitVec w) (y : BitVec w) (a : Bool) (b : Bool) : BitVec.cons a x ||| BitVec.cons b y = BitVec.cons (a || b) (x ||| y)

@[simp]

theorem BitVec.cons_and_cons {w : Nat} (x : BitVec w) (y : BitVec w) (a : Bool) (b : Bool) : BitVec.cons a x &&& BitVec.cons b y = BitVec.cons (a && b) (x &&& y)

@[simp]

theorem BitVec.cons_xor_cons {w : Nat} (x : BitVec w) (y : BitVec w) (a : Bool) (b : Bool) : BitVec.cons a x ^^^ BitVec.cons b y = BitVec.cons (xor a b) (x ^^^ y)

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 = (x.toNat + y.toNat)#n

@[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) : (x + y)#n = x#n + y#n

theorem BitVec.ofNat_add_ofNat {n : Nat} (x : Nat) (y : Nat) : x#n + y#n = (x + y)#n

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) : BitVec.truncate i (x + y) = BitVec.truncate i x + BitVec.truncate i y

@[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) : BitVec.ofInt n (x + y) = BitVec.ofInt n x + BitVec.ofInt n y

sub/neg

theorem BitVec.sub_def {n : Nat} (x : BitVec n) (y : BitVec n) : x - y = (x.toNat + (2 ^ n - y.toNat))#n

@[simp]

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) : x#n - y#n = (x + (2 ^ n - y % 2 ^ n))#n

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

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.negOne_eq_allOnes {w : Nat} : -1#w = BitVec.allOnes w

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

instance BitVec.instLawfulCommIdentityHMulOfNatOfNatNat {w : Nat} : Std.LawfulCommIdentity (fun (x y : BitVec w) => x * y) 1#w

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) : BitVec.ofInt n (x * y) = BitVec.ofInt n x * BitVec.ofInt n y

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) : x#n ≤ y#n ↔ 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) : x#n < y#n ↔ 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) : BitVec w

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

Equations

• BitVec.intMax w = (2 ^ w - 1)#w

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)