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

Prove equality of bitvectors in terms of nat operations.

theorem Std.BitVec.toNat_eq {n : Nat} (x : Std.BitVec n) (y : Std.BitVec n) : x = y ↔ Std.BitVec.toNat x = Std.BitVec.toNat y

theorem Std.BitVec.testBit_toNat {w : Nat} {i : Nat} (x : Std.BitVec w) : Nat.testBit (Std.BitVec.toNat x) i = Std.BitVec.getLsb x i

@[simp]

theorem Std.BitVec.getLsb_ge {w : Nat} (x : Std.BitVec w) (i : Nat) (ge : i ≥ w) : Std.BitVec.getLsb x i = false

theorem Std.BitVec.eq_of_getLsb_eq {w : Nat} {x : Std.BitVec w} {y : Std.BitVec w} (pred : ∀ (i : Fin w), Std.BitVec.getLsb x i.val = Std.BitVec.getLsb y i.val) : x = y

theorem Std.BitVec.eq_of_getMsb_eq {w : Nat} {x : Std.BitVec w} {y : Std.BitVec w} (pred : ∀ (i : Fin w), Std.BitVec.getMsb x i.val = Std.BitVec.getMsb y i.val) : x = y

@[simp]

theorem Std.BitVec.toNat_ofBool (b : Bool) : Std.BitVec.toNat (Std.BitVec.ofBool b) = Bool.toNat b

@[simp]

theorem Std.BitVec.toNat_ofFin {n : Nat} (x : Fin (2 ^ n)) : Std.BitVec.toNat { toFin := x } = x.val

theorem Std.BitVec.toNat_ofNat (x : Nat) (w : Nat) : Std.BitVec.toNat x#w = x % 2 ^ w

@[simp]

theorem Std.BitVec.toNat_zero (n : Nat) : Std.BitVec.toNat 0#n = 0

@[simp]

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

theorem Std.BitVec.toNat_append {m : Nat} {n : Nat} (x : Std.BitVec m) (y : Std.BitVec n) : Std.BitVec.toNat (x ++ y) = Std.BitVec.toNat x <<< n ||| Std.BitVec.toNat y

@[simp]

theorem Std.BitVec.toNat_cast {m : Nat} {n : Nat} (e : m = n) (x : Std.BitVec m) : Std.BitVec.toNat (Std.BitVec.cast e x) = Std.BitVec.toNat x

theorem Std.BitVec.toNat_cons {w : Nat} (b : Bool) (x : Std.BitVec w) : Std.BitVec.toNat (Std.BitVec.cons b x) = Bool.toNat b <<< w ||| Std.BitVec.toNat x

cons

theorem Std.BitVec.getLsb_cons (b : Bool) {n : Nat} (x : Std.BitVec n) (i : Nat) : Std.BitVec.getLsb (Std.BitVec.cons b x) i = if i = n then b else Std.BitVec.getLsb x i

zeroExtend and truncate

@[simp]

theorem Std.BitVec.toNat_zeroExtend' {m : Nat} {n : Nat} (p : m ≤ n) (x : Std.BitVec m) : Std.BitVec.toNat (Std.BitVec.zeroExtend' p x) = Std.BitVec.toNat x

theorem Std.BitVec.toNat_zeroExtend {n : Nat} (i : Nat) (x : Std.BitVec n) : Std.BitVec.toNat (Std.BitVec.zeroExtend i x) = Std.BitVec.toNat x % 2 ^ i

@[simp]

theorem Std.BitVec.zeroExtend_eq {n : Nat} (x : Std.BitVec n) : Std.BitVec.zeroExtend n x = x

@[simp]

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

@[simp]

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

@[simp]

theorem Std.BitVec.toNat_truncate {n : Nat} {i : Nat} (x : Std.BitVec n) : Std.BitVec.toNat (Std.BitVec.truncate i x) = Std.BitVec.toNat x % 2 ^ i

theorem Std.BitVec.getLsb_zeroExtend' {m : Nat} {n : Nat} (ge : m ≥ n) (x : Std.BitVec n) (i : Nat) : Std.BitVec.getLsb (Std.BitVec.zeroExtend' ge x) i = Std.BitVec.getLsb x i

theorem Std.BitVec.getLsb_zeroExtend {n : Nat} (m : Nat) (x : Std.BitVec n) (i : Nat) : Std.BitVec.getLsb (Std.BitVec.zeroExtend m x) i = (decide (i < m) && Std.BitVec.getLsb x i)

theorem Std.BitVec.getLsb_truncate {n : Nat} (m : Nat) (x : Std.BitVec n) (i : Nat) : Std.BitVec.getLsb (Std.BitVec.truncate m x) i = (decide (i < m) && Std.BitVec.getLsb x i)

theorem Std.BitVec.truncate_succ {w : Nat} {i : Nat} (x : Std.BitVec w) : Std.BitVec.truncate (i + 1) x = Std.BitVec.cons (Std.BitVec.getLsb x i) (Std.BitVec.truncate i x)

add

theorem Std.BitVec.toNat_add {w : Nat} (x : Std.BitVec w) (y : Std.BitVec w) : Std.BitVec.toNat (x + y) = (Std.BitVec.toNat x + Std.BitVec.toNat y) % 2 ^ w

Definition of bitvector addition as a nat.

@[simp]

theorem Std.BitVec.add_zero {n : Nat} (x : Std.BitVec n) : x + 0#n = x