@[simp]

theorem BitVec.getLsbD_ofFin {n : Nat} (x : Fin (2 ^ n)) (i : Nat) : { toFin := x }.getLsbD i = (↑x).testBit i

@[simp]

theorem BitVec.getLsbD_ge {w : Nat} (x : BitVec w) (i : Nat) (ge : w ≤ i) : x.getLsbD i = false

@[simp]

theorem BitVec.getMsbD_ge {w : Nat} (x : BitVec w) (i : Nat) (ge : w ≤ i) : x.getMsbD i = false

theorem BitVec.lt_of_getLsbD {w : Nat} {x : BitVec w} {i : Nat} : x.getLsbD i = true → i < w

theorem BitVec.lt_of_getMsbD {w : Nat} {x : BitVec w} {i : Nat} : x.getMsbD i = true → i < w

@[simp]

theorem BitVec.getElem?_eq_getElem {w : Nat} {l : BitVec w} {n : Nat} (h : n < w) : l[n]? = some l[n]

theorem BitVec.getElem?_eq_some {w n : Nat} {a : Bool} {l : BitVec w} : l[n]? = some a ↔ ∃ (h : n < w), l[n] = a

@[simp]

theorem BitVec.getElem?_eq_none_iff {w n : Nat} {l : BitVec w} : l[n]? = none ↔ w ≤ n

theorem BitVec.getElem?_eq_none {w n : Nat} {l : BitVec w} (h : w ≤ n) : l[n]? = none

theorem BitVec.getElem?_eq {w : Nat} (l : BitVec w) (i : Nat) : l[i]? = if h : i < w then some l[i] else none

@[simp]

theorem BitVec.some_getElem_eq_getElem? {w : Nat} (l : BitVec w) (i : Nat) (h : i < w) : some l[i] = l[i]? ↔ True

@[simp]

theorem BitVec.getElem?_eq_some_getElem {w : Nat} (l : BitVec w) (i : Nat) (h : i < w) : l[i]? = some l[i] ↔ True

theorem BitVec.getElem_eq_iff {w : Nat} {x : Bool} {l : BitVec w} {n : Nat} {h : n < w} : l[n] = x ↔ l[n]? = some x

theorem BitVec.getElem_eq_getElem? {w : Nat} (l : BitVec w) (i : Nat) (h : i < w) : l[i] = l[i]?.get ⋯

theorem BitVec.getLsbD_eq_getElem?_getD {w : Nat} {x : BitVec w} {i : Nat} : x.getLsbD i = x[i]?.getD false

theorem BitVec.ofFin_eq_ofNat {w 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} {x y : BitVec n} : x.toNat = y.toNat → x = y

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 y : BitVec n} : x = y ↔ x.toNat = y.toNat

theorem BitVec.toNat_ne {n : Nat} {x y : BitVec n} : x ≠ y ↔ x.toNat ≠ y.toNat

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

theorem BitVec.getMsb'_eq_getLsb' {w : Nat} (x : BitVec w) (i : Fin w) : x.getMsb' i = x.getLsb' ⟨w - 1 - ↑i, ⋯⟩

theorem BitVec.getMsb?_eq_getLsb? {w : Nat} (x : BitVec w) (i : Nat) : x.getMsb? i = if i < w then x.getLsb? (w - 1 - i) else none

theorem BitVec.getMsbD_eq_getLsbD {w : Nat} (x : BitVec w) (i : Nat) : x.getMsbD i = (decide (i < w) && x.getLsbD (w - 1 - i))

theorem BitVec.getLsbD_eq_getMsbD {w : Nat} (x : BitVec w) (i : Nat) : x.getLsbD i = (decide (i < w) && x.getMsbD (w - 1 - i))

@[simp]

theorem BitVec.getLsb?_ge {w : Nat} (x : BitVec w) (i : Nat) (ge : w ≤ i) : x[i]? = none

@[simp]

theorem BitVec.getMsb?_ge {w : Nat} (x : BitVec w) (i : Nat) (ge : w ≤ i) : x.getMsb? i = none

theorem BitVec.lt_of_getLsb?_eq_some {w : Nat} {b : Bool} (x : BitVec w) (i : Nat) : x[i]? = some b → i < w

theorem BitVec.lt_of_getMsb?_eq_some {w : Nat} {b : Bool} (x : BitVec w) (i : Nat) : x.getMsb? i = some b → i < w

theorem BitVec.lt_of_getLsb?_isSome {w : Nat} (x : BitVec w) (i : Nat) : x[i]?.isSome = true → i < w

theorem BitVec.lt_of_getMsb?_isSome {w : Nat} (x : BitVec w) (i : Nat) : (x.getMsb? i).isSome = true → i < w

theorem BitVec.getMsbD_eq_getMsb?_getD {w : Nat} (x : BitVec w) (i : Nat) : x.getMsbD i = (x.getMsb? i).getD false

theorem BitVec.eq_of_getLsbD_eq {w : Nat} {x y : BitVec w} (pred : ∀ (i : Fin w), x.getLsbD ↑i = y.getLsbD ↑i) : x = y

theorem BitVec.eq_of_getMsbD_eq {w : Nat} {x y : BitVec w} (pred : ∀ (i : Fin w), x.getMsbD ↑i = y.getMsbD ↑i) : x = y

theorem BitVec.of_length_zero {x : BitVec 0} : x = 0#0

theorem BitVec.toNat_zero_length (x : BitVec 0) : x.toNat = 0

theorem BitVec.getLsbD_zero_length {i : Nat} (x : BitVec 0) : x.getLsbD i = false

theorem BitVec.getMsbD_zero_length {i : Nat} (x : BitVec 0) : x.getMsbD i = false

theorem BitVec.msb_zero_length (x : BitVec 0) : x.msb = false

theorem BitVec.toNat_of_zero_length {w : Nat} (h : w = 0) (x : BitVec w) : x.toNat = 0

theorem BitVec.getLsbD_of_zero_length {w i : Nat} (h : w = 0) (x : BitVec w) : x.getLsbD i = false

theorem BitVec.getMsbD_of_zero_length {w i : Nat} (h : w = 0) (x : BitVec w) : x.getMsbD i = false

theorem BitVec.msb_of_zero_length {w : Nat} (h : w = 0) (x : BitVec w) : x.msb = false

theorem BitVec.ofFin_ofNat {w : Nat} (n : Nat) : { toFin := OfNat.ofNat n } = OfNat.ofNat n

theorem BitVec.eq_of_toFin_eq {w : Nat} {x y : BitVec w} : x.toFin = y.toFin → x = y

theorem BitVec.toFin_inj {w : Nat} {x y : BitVec w} : x.toFin = y.toFin ↔ x = y

theorem BitVec.toFin_zero {w : Nat} : BitVec.toFin 0 = 0

theorem BitVec.toFin_one {w : Nat} : BitVec.toFin 1 = 1

@[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) : BitVec.ofNat 1 n = BitVec.ofBool (decide (n % 2 = 1))

theorem BitVec.ofBool_eq_iff_eq {b 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.ofBool_and_ofBool {b b' : Bool} : BitVec.ofBool b &&& BitVec.ofBool b' = BitVec.ofBool (b && b')

@[simp]

theorem BitVec.ofBool_or_ofBool {b b' : Bool} : BitVec.ofBool b ||| BitVec.ofBool b' = BitVec.ofBool (b || b')

@[simp]

theorem BitVec.ofBool_xor_ofBool {b b' : Bool} : BitVec.ofBool b ^^^ BitVec.ofBool b' = BitVec.ofBool (b ^^ 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.getLsbD_ofNatLt {n : Nat} (x : Nat) (lt : x < 2 ^ n) (i : Nat) : (x#'lt).getLsbD i = x.testBit i

@[simp]

theorem BitVec.getMsbD_ofNatLt {n x i : Nat} (h : x < 2 ^ n) : (x#'h).getMsbD i = (decide (i < n) && x.testBit (n - 1 - i))

@[simp]

theorem BitVec.toNat_ofNat (x 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' (2 ^ w) x

theorem BitVec.getLsbD_ofNat (n x i : Nat) : (BitVec.ofNat n x).getLsbD i = (decide (i < n) && x.testBit i)

@[simp]

theorem BitVec.getLsbD_zero {w i : Nat} : (0#w).getLsbD i = false

@[simp]

theorem BitVec.getElem_zero {i w : Nat} (h : i < w) : (0#w)[i] = false

@[simp]

theorem BitVec.getMsbD_zero {w i : Nat} : (0#w).getMsbD i = false

@[simp]

theorem BitVec.getLsbD_one {w i : Nat} : (1#w).getLsbD i = (decide (0 < w) && decide (i = 0))

@[simp]

theorem BitVec.getElem_one {i w : Nat} (h : i < w) : (1#w)[i] = decide (i = 0)

@[simp]

theorem BitVec.getMsbD_one {w i : Nat} : (1#w).getMsbD i = (decide (i = w - 1) && decide (0 < w))

The msb at index w-1 is the least significant bit, and is true when the width is nonzero.

@[simp]

theorem BitVec.toNat_mod_cancel {n : Nat} (x : BitVec n) : x.toNat % 2 ^ n = x.toNat

@[simp]

theorem BitVec.toNat_mod_cancel' {n : Nat} {x : BitVec n} : ↑x.toNat % ↑(2 ^ n) = ↑x.toNat

@[simp]

theorem BitVec.sub_toNat_mod_cancel {w : Nat} {x : BitVec w} (h : ¬x = 0#w) : (2 ^ w - x.toNat) % 2 ^ w = 2 ^ w - x.toNat

@[simp]

theorem BitVec.sub_sub_toNat_cancel {w : Nat} {x : BitVec w} : 2 ^ w - (2 ^ w - x.toNat) = x.toNat

@[simp]

theorem BitVec.sub_add_bmod_cancel {w : Nat} {x y : BitVec w} : (↑(2 ^ w) - ↑y.toNat + ↑x.toNat).bmod (2 ^ w) = (↑x.toNat - ↑y.toNat).bmod (2 ^ w)

@[simp]

theorem BitVec.getElem_zero_ofNat_zero {w : Nat} (i : Nat) (h : i < w) : (0#w)[i] = false

@[simp]

theorem BitVec.getElem_zero_ofNat_one {w : Nat} (h : 0 < w) : (1#w)[0] = true

theorem BitVec.getElem?_zero_ofNat_zero {w : Nat} : (0#(w + 1))[0]? = some false

theorem BitVec.getElem?_zero_ofNat_one {w : Nat} : (1#(w + 1))[0]? = some true

theorem BitVec.getElem?_zero_ofBool (b : Bool) : (BitVec.ofBool b)[0]? = some b

@[simp]

theorem BitVec.getElem_zero_ofBool (b : Bool) : (BitVec.ofBool b)[0] = b

theorem BitVec.getElem?_succ_ofBool (b : Bool) (i : Nat) : (BitVec.ofBool b)[i + 1]? = none

@[simp]

theorem BitVec.getLsbD_ofBool (b : Bool) (i : Nat) : (BitVec.ofBool b).getLsbD i = (decide (i = 0) && b)

@[simp]

theorem BitVec.getElem_ofBool {b : Bool} {i : Nat} : (BitVec.ofBool b)[0] = b

msb

@[simp]

theorem BitVec.msb_zero {w : Nat} : (0#w).msb = false

@[simp]

theorem BitVec.msb_one {w : Nat} : (1#w).msb = decide (w = 1)

theorem BitVec.msb_eq_getLsbD_last {w : Nat} (x : BitVec w) : x.msb = x.getLsbD (w - 1)

theorem BitVec.getLsbD_last {w : Nat} (x : BitVec w) : x.getLsbD (w - 1) = decide (2 ^ (w - 1) ≤ x.toNat)

theorem BitVec.getLsbD_succ_last {w : Nat} (x : BitVec (w + 1)) : x.getLsbD 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 v : Nat} (h : w = v) (x : BitVec w) : (BitVec.cast h x).toNat = x.toNat

@[simp]

theorem BitVec.toFin_cast {w v : Nat} (h : w = v) (x : BitVec w) : (BitVec.cast h x).toFin = Fin.cast ⋯ x.toFin

@[simp]

theorem BitVec.getLsbD_cast {w v i : Nat} (h : w = v) (x : BitVec w) : (BitVec.cast h x).getLsbD i = x.getLsbD i

@[simp]

theorem BitVec.getMsbD_cast {w v i : Nat} (h : w = v) (x : BitVec w) : (BitVec.cast h x).getMsbD i = x.getMsbD i

@[simp]

theorem BitVec.getElem_cast {w v i : Nat} (h : w = v) (x : BitVec w) (p : i < v) : (BitVec.cast h x)[i] = x[i]

@[simp]

theorem BitVec.msb_cast {w 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} (x : BitVec n) : x.toInt = if 2 * x.toNat < 2 ^ n then ↑x.toNat else ↑x.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} {x y : BitVec n} : x.toInt = y.toInt → x = y

Prove equality of bitvectors in terms of nat operations.

theorem BitVec.toInt_inj {n : Nat} {x y : BitVec n} : x.toInt = y.toInt ↔ x = y

theorem BitVec.toInt_ne {n : Nat} {x 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 n : Nat) : BitVec.ofInt w ↑n = BitVec.ofNat w n

@[simp]

theorem BitVec.ofInt_ofNat (w n : Nat) : BitVec.ofInt w (OfNat.ofNat n) = BitVec.ofNat w (OfNat.ofNat n)

theorem BitVec.toInt_neg_iff {w : Nat} {x : BitVec w} : x.toInt < 0 ↔ 2 ^ w ≤ 2 * x.toNat

theorem BitVec.toInt_pos_iff {w : Nat} {x : BitVec w} : 0 ≤ x.toInt ↔ 2 * x.toNat < 2 ^ w

theorem BitVec.eq_zero_or_eq_one (a : BitVec 1) : a = 0#1 ∨ a = 1#1

@[simp]

theorem BitVec.toInt_zero {w : Nat} : (0#w).toInt = 0

slt

theorem BitVec.slt_zero_iff_msb_cond {w : Nat} (x : BitVec w) : x.slt 0#w = true ↔ x.msb = true

A bitvector, when interpreted as an integer, is less than zero iff its most significant bit is true.

setWidth, zeroExtend and truncate

@[simp]

theorem BitVec.truncate_eq_setWidth {w v : Nat} {x : BitVec w} : BitVec.truncate v x = BitVec.setWidth v x

@[simp]

theorem BitVec.zeroExtend_eq_setWidth {w v : Nat} {x : BitVec w} : BitVec.zeroExtend v x = BitVec.setWidth v x

@[simp]

theorem BitVec.toNat_setWidth' {m n : Nat} (p : m ≤ n) (x : BitVec m) : (BitVec.setWidth' p x).toNat = x.toNat

@[simp]

theorem BitVec.toNat_setWidth {n : Nat} (i : Nat) (x : BitVec n) : (BitVec.setWidth i x).toNat = x.toNat % 2 ^ i

@[simp]

theorem BitVec.toInt_setWidth {w v : Nat} (x : BitVec w) : (BitVec.setWidth v x).toInt = (↑x.toNat).bmod (2 ^ v)

theorem BitVec.setWidth'_eq {w v : Nat} {x : BitVec w} (h : w ≤ v) : BitVec.setWidth' h x = BitVec.setWidth v x

@[simp]

theorem BitVec.setWidth_eq {n : Nat} (x : BitVec n) : BitVec.setWidth n x = x

@[simp]

theorem BitVec.setWidth_zero (m n : Nat) : BitVec.setWidth m 0#n = 0#m

@[simp]

theorem BitVec.ofNat_toNat {n : Nat} (m : Nat) (x : BitVec n) : BitVec.ofNat m x.toNat = BitVec.setWidth m x

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.

theorem BitVec.getElem_setWidth' {w v : Nat} (x : BitVec w) (i : Nat) (h : w ≤ v) (hi : i < v) : (BitVec.setWidth' h x)[i] = x.getLsbD i

@[simp]

theorem BitVec.getElem_setWidth {n : Nat} (m : Nat) (x : BitVec n) (i : Nat) (h : i < m) : (BitVec.setWidth m x)[i] = x.getLsbD i

theorem BitVec.getElem?_setWidth' {w v : Nat} (x : BitVec w) (i : Nat) (h : w ≤ v) : (BitVec.setWidth' h x)[i]? = if i < v then some (x.getLsbD i) else none

theorem BitVec.getElem?_setWidth {n : Nat} (m : Nat) (x : BitVec n) (i : Nat) : (BitVec.setWidth m x)[i]? = if i < m then some (x.getLsbD i) else none

@[simp]

theorem BitVec.getLsbD_setWidth' {m n : Nat} (ge : m ≥ n) (x : BitVec n) (i : Nat) : (BitVec.setWidth' ge x).getLsbD i = x.getLsbD i

@[simp]

theorem BitVec.getMsbD_setWidth' {m n : Nat} (ge : m ≥ n) (x : BitVec n) (i : Nat) : (BitVec.setWidth' ge x).getMsbD i = (decide (i ≥ m - n) && x.getMsbD (i - (m - n)))

@[simp]

theorem BitVec.getLsbD_setWidth {n : Nat} (m : Nat) (x : BitVec n) (i : Nat) : (BitVec.setWidth m x).getLsbD i = (decide (i < m) && x.getLsbD i)

@[simp]

theorem BitVec.getMsbD_setWidth_add {w k i : Nat} {x : BitVec w} (h : k ≤ i) : (BitVec.setWidth (w + k) x).getMsbD i = x.getMsbD (i - k)

@[simp]

theorem BitVec.cast_setWidth {v v' w : Nat} (h : v = v') (x : BitVec w) : BitVec.cast h (BitVec.setWidth v x) = BitVec.setWidth v' x

@[simp]

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

@[simp]

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

theorem BitVec.msb_setWidth {w v : Nat} (x : BitVec w) : (BitVec.setWidth v x).msb = (decide (0 < v) && x.getLsbD (v - 1))

theorem BitVec.msb_setWidth' {w v : Nat} (x : BitVec w) (h : w ≤ v) : (BitVec.setWidth' h x).msb = (decide (0 < v) && x.getLsbD (v - 1))

theorem BitVec.msb_setWidth'' {w k : Nat} (x : BitVec w) : (BitVec.setWidth (k + 1) x).msb = x.getLsbD k

theorem BitVec.setWidth_one_eq_ofBool_getLsb_zero {w : Nat} (x : BitVec w) : BitVec.setWidth 1 x = BitVec.ofBool (x.getLsbD 0)

zero extending a bitvector to width 1 equals the boolean of the lsb.

theorem BitVec.setWidth_ofNat_one_eq_ofNat_one_of_lt {v w : Nat} (hv : 0 < v) : BitVec.setWidth w 1#v = 1#w

Zero extending 1#v to 1#w equals 1#w when v > 0.

theorem BitVec.setWidth_one {w : Nat} {x : BitVec w} : BitVec.setWidth 1 x = BitVec.ofBool (x.getLsbD 0)

Truncating to width 1 produces a bitvector equal to the least significant bit.

@[simp]

theorem BitVec.setWidth_ofNat_of_le {v w : Nat} (h : v ≤ w) (x : Nat) : BitVec.setWidth v (BitVec.ofNat w x) = BitVec.ofNat v x

extractLsb

@[simp]

theorem BitVec.extractLsb_ofFin {n : Nat} (x : Fin (2 ^ n)) (hi lo : Nat) : BitVec.extractLsb hi lo { toFin := x } = BitVec.ofNat (hi - lo + 1) (↑x >>> lo)

@[simp]

theorem BitVec.extractLsb_ofNat (x n hi 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 m : Nat) (x : BitVec n) : (BitVec.extractLsb' s m x).toNat = x.toNat >>> s % 2 ^ m

@[simp]

theorem BitVec.extractLsb_toNat {n : Nat} (hi lo : Nat) (x : BitVec n) : (BitVec.extractLsb hi lo x).toNat = x.toNat >>> lo % 2 ^ (hi - lo + 1)

@[simp]

theorem BitVec.getElem_extractLsb' {n start len : Nat} {x : BitVec n} {i : Nat} (h : i < len) : (BitVec.extractLsb' start len x)[i] = x.getLsbD (start + i)

@[simp]

theorem BitVec.getLsbD_extractLsb' {n : Nat} (start len : Nat) (x : BitVec n) (i : Nat) : (BitVec.extractLsb' start len x).getLsbD i = (decide (i < len) && x.getLsbD (start + i))

@[simp]

theorem BitVec.getElem_extract {n hi lo : Nat} {x : BitVec n} {i : Nat} (h : i < hi - lo + 1) : (BitVec.extractLsb hi lo x)[i] = x.getLsbD (lo + i)

@[simp]

theorem BitVec.getLsbD_extract {n : Nat} (hi lo : Nat) (x : BitVec n) (i : Nat) : (BitVec.extractLsb hi lo x).getLsbD i = (decide (i ≤ hi - lo) && x.getLsbD (lo + i))

theorem BitVec.extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h : len > 0) : BitVec.extractLsb' start len x = BitVec.cast ⋯ (BitVec.extractLsb (len - 1 + start) start x)

allOnes

@[simp]

theorem BitVec.toNat_allOnes {v : Nat} : (BitVec.allOnes v).toNat = 2 ^ v - 1

@[simp]

theorem BitVec.getLsbD_allOnes {v i : Nat} : (BitVec.allOnes v).getLsbD i = decide (i < v)

@[simp]

theorem BitVec.getMsbD_allOnes {v i : Nat} : (BitVec.allOnes v).getMsbD i = decide (i < v)

@[simp]

theorem BitVec.getElem_allOnes {v : Nat} (i : Nat) (h : i < v) : (BitVec.allOnes v)[i] = true

@[simp]

theorem BitVec.ofFin_add_rev {n : Nat} (x : Fin (2 ^ n)) : { toFin := x + x.rev } = BitVec.allOnes n

or

@[simp]

theorem BitVec.toNat_or {v : Nat} (x y : BitVec v) : (x ||| y).toNat = x.toNat ||| y.toNat

@[simp]

theorem BitVec.toInt_or {w : Nat} (x y : BitVec w) : (x ||| y).toInt = (↑(x.toNat ||| y.toNat)).bmod (2 ^ w)

@[simp]

theorem BitVec.toFin_or {v : Nat} (x y : BitVec v) : (x ||| y).toFin = x.toFin ||| y.toFin

@[simp]

theorem BitVec.getLsbD_or {v i : Nat} {x y : BitVec v} : (x ||| y).getLsbD i = (x.getLsbD i || y.getLsbD i)

@[simp]

theorem BitVec.getMsbD_or {w i : Nat} {x y : BitVec w} : (x ||| y).getMsbD i = (x.getMsbD i || y.getMsbD i)

@[simp]

theorem BitVec.getElem_or {w : Nat} {x y : BitVec w} {i : Nat} (h : i < w) : (x ||| y)[i] = (x[i] || y[i])

@[simp]

theorem BitVec.msb_or {w : Nat} {x y : BitVec w} : (x ||| y).msb = (x.msb || y.msb)

@[simp]

theorem BitVec.setWidth_or {w k : Nat} {x y : BitVec w} : BitVec.setWidth k (x ||| y) = BitVec.setWidth k x ||| BitVec.setWidth k y

theorem BitVec.or_assoc {w : Nat} (x y z : BitVec w) : x ||| y ||| z = x ||| (y ||| z)

theorem BitVec.instAssociativeHOr {n : Nat} : Std.Associative fun (x1 x2 : BitVec n) => x1 ||| x2

theorem BitVec.or_comm {w : Nat} (x y : BitVec w) : x ||| y = y ||| x

theorem BitVec.instCommutativeHOr {w : Nat} : Std.Commutative fun (x y : BitVec w) => x ||| y

@[simp]

theorem BitVec.or_self {w : Nat} {x : BitVec w} : x ||| x = x

theorem BitVec.instIdempotentOpHOr {n : Nat} : Std.IdempotentOp fun (x1 x2 : BitVec n) => x1 ||| x2

@[simp]

theorem BitVec.or_zero {w : Nat} {x : BitVec w} : x ||| 0#w = x

theorem BitVec.instLawfulCommIdentityHOrOfNatOfNatNat {n : Nat} : Std.LawfulCommIdentity (fun (x1 x2 : BitVec n) => x1 ||| x2) 0#n

@[simp]

theorem BitVec.zero_or {w : Nat} {x : BitVec w} : 0#w ||| x = x

@[simp]

theorem BitVec.or_allOnes {w : Nat} {x : BitVec w} : x ||| BitVec.allOnes w = BitVec.allOnes w

@[simp]

theorem BitVec.allOnes_or {w : Nat} {x : BitVec w} : BitVec.allOnes w ||| x = BitVec.allOnes w

and

@[simp]

theorem BitVec.toNat_and {v : Nat} (x y : BitVec v) : (x &&& y).toNat = x.toNat &&& y.toNat

@[simp]

theorem BitVec.toInt_and {w : Nat} (x y : BitVec w) : (x &&& y).toInt = (↑(x.toNat &&& y.toNat)).bmod (2 ^ w)

@[simp]

theorem BitVec.toFin_and {v : Nat} (x y : BitVec v) : (x &&& y).toFin = x.toFin &&& y.toFin

@[simp]

theorem BitVec.getLsbD_and {v i : Nat} {x y : BitVec v} : (x &&& y).getLsbD i = (x.getLsbD i && y.getLsbD i)

@[simp]

theorem BitVec.getMsbD_and {w i : Nat} {x y : BitVec w} : (x &&& y).getMsbD i = (x.getMsbD i && y.getMsbD i)

@[simp]

theorem BitVec.getElem_and {w : Nat} {x y : BitVec w} {i : Nat} (h : i < w) : (x &&& y)[i] = (x[i] && y[i])

@[simp]

theorem BitVec.msb_and {w : Nat} {x y : BitVec w} : (x &&& y).msb = (x.msb && y.msb)

@[simp]

theorem BitVec.setWidth_and {w k : Nat} {x y : BitVec w} : BitVec.setWidth k (x &&& y) = BitVec.setWidth k x &&& BitVec.setWidth k y

theorem BitVec.and_assoc {w : Nat} (x y z : BitVec w) : x &&& y &&& z = x &&& (y &&& z)

theorem BitVec.instAssociativeHAnd {n : Nat} : Std.Associative fun (x1 x2 : BitVec n) => x1 &&& x2

theorem BitVec.and_comm {w : Nat} (x y : BitVec w) : x &&& y = y &&& x

theorem BitVec.instCommutativeHAnd {w : Nat} : Std.Commutative fun (x y : BitVec w) => x &&& y

@[simp]

theorem BitVec.and_self {w : Nat} {x : BitVec w} : x &&& x = x

theorem BitVec.instIdempotentOpHAnd {n : Nat} : Std.IdempotentOp fun (x1 x2 : BitVec n) => x1 &&& x2

@[simp]

theorem BitVec.and_zero {w : Nat} {x : BitVec w} : x &&& 0#w = 0#w

@[simp]

theorem BitVec.zero_and {w : Nat} {x : BitVec w} : 0#w &&& x = 0#w

@[simp]

theorem BitVec.and_allOnes {w : Nat} {x : BitVec w} : x &&& BitVec.allOnes w = x

theorem BitVec.instLawfulCommIdentityHAndAllOnes {n : Nat} : Std.LawfulCommIdentity (fun (x1 x2 : BitVec n) => x1 &&& x2) (BitVec.allOnes n)

@[simp]

theorem BitVec.allOnes_and {w : Nat} {x : BitVec w} : BitVec.allOnes w &&& x = x

xor

@[simp]

theorem BitVec.toNat_xor {v : Nat} (x y : BitVec v) : (x ^^^ y).toNat = x.toNat ^^^ y.toNat

@[simp]

theorem BitVec.toInt_xor {w : Nat} (x y : BitVec w) : (x ^^^ y).toInt = (↑(x.toNat ^^^ y.toNat)).bmod (2 ^ w)

@[simp]

theorem BitVec.toFin_xor {v : Nat} (x y : BitVec v) : (x ^^^ y).toFin = x.toFin ^^^ y.toFin

@[simp]

theorem BitVec.getLsbD_xor {v i : Nat} {x y : BitVec v} : (x ^^^ y).getLsbD i = (x.getLsbD i ^^ y.getLsbD i)

@[simp]

theorem BitVec.getMsbD_xor {w i : Nat} {x y : BitVec w} : (x ^^^ y).getMsbD i = (x.getMsbD i ^^ y.getMsbD i)

@[simp]

theorem BitVec.getElem_xor {w : Nat} {x y : BitVec w} {i : Nat} (h : i < w) : (x ^^^ y)[i] = (x[i] ^^ y[i])

@[simp]

theorem BitVec.msb_xor {w : Nat} {x y : BitVec w} : (x ^^^ y).msb = (x.msb ^^ y.msb)

@[simp]

theorem BitVec.setWidth_xor {w k : Nat} {x y : BitVec w} : BitVec.setWidth k (x ^^^ y) = BitVec.setWidth k x ^^^ BitVec.setWidth k y

theorem BitVec.xor_assoc {w : Nat} (x y z : BitVec w) : x ^^^ y ^^^ z = x ^^^ (y ^^^ z)

theorem BitVec.instAssociativeHXor {w : Nat} : Std.Associative fun (x y : BitVec w) => x ^^^ y

theorem BitVec.xor_comm {w : Nat} (x y : BitVec w) : x ^^^ y = y ^^^ x

theorem BitVec.instCommutativeHXor {w : Nat} : Std.Commutative fun (x y : BitVec w) => x ^^^ y

@[simp]

theorem BitVec.xor_self {w : Nat} {x : BitVec w} : x ^^^ x = 0#w

@[simp]

theorem BitVec.xor_zero {w : Nat} {x : BitVec w} : x ^^^ 0#w = x

theorem BitVec.instLawfulCommIdentityHXorOfNatOfNatNat {n : Nat} : Std.LawfulCommIdentity (fun (x1 x2 : BitVec n) => x1 ^^^ x2) 0#n

@[simp]

theorem BitVec.zero_xor {w : Nat} {x : BitVec w} : 0#w ^^^ x = x

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.toInt_not {w : Nat} {x : BitVec w} : (~~~x).toInt = (2 ^ w - 1 - ↑x.toNat).bmod (2 ^ w)

@[simp]

theorem BitVec.ofInt_negSucc_eq_not_ofNat {w n : Nat} : BitVec.ofInt w (Int.negSucc n) = ~~~BitVec.ofNat w n

@[simp]

theorem BitVec.toFin_not {w : Nat} (x : BitVec w) : (~~~x).toFin = x.toFin.rev

@[simp]

theorem BitVec.getLsbD_not {v i : Nat} {x : BitVec v} : (~~~x).getLsbD i = (decide (i < v) && !x.getLsbD i)

@[simp]

theorem BitVec.getMsbD_not {v i : Nat} {x : BitVec v} : (~~~x).getMsbD i = (decide (i < v) && !x.getMsbD i)

@[simp]

theorem BitVec.getElem_not {w : Nat} {x : BitVec w} {i : Nat} (h : i < w) : (~~~x)[i] = !x[i]

@[simp]

theorem BitVec.setWidth_not {w k : Nat} {x : BitVec w} (h : k ≤ w) : BitVec.setWidth k (~~~x) = ~~~BitVec.setWidth k x

@[simp]

theorem BitVec.not_zero {n : Nat} : ~~~0#n = BitVec.allOnes n

@[simp]

theorem BitVec.not_allOnes {w : Nat} : ~~~BitVec.allOnes w = 0#w

@[simp]

theorem BitVec.xor_allOnes {w : Nat} {x : BitVec w} : x ^^^ BitVec.allOnes w = ~~~x

@[simp]

theorem BitVec.allOnes_xor {w : Nat} {x : BitVec w} : BitVec.allOnes w ^^^ x = ~~~x

@[simp]

theorem BitVec.not_not {w : Nat} {b : BitVec w} : ~~~~~~b = b

theorem BitVec.not_eq_comm {w : Nat} {x y : BitVec w} : ~~~x = y ↔ x = ~~~y

@[simp]

theorem BitVec.getMsb_not {w i : Nat} {x : BitVec w} : (~~~x).getMsbD i = (decide (i < w) && !x.getMsbD i)

@[simp]

theorem BitVec.msb_not {w : Nat} {x : BitVec w} : (~~~x).msb = (decide (0 < w) && !x.msb)

cast

@[simp]

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

@[simp]

theorem BitVec.and_cast {w w' : Nat} {x 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 w' : Nat} {x 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 w' : Nat} {x 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 n : Nat} {x : BitVec v} : (x <<< n).toNat = x.toNat <<< n % 2 ^ v

@[simp]

theorem BitVec.toFin_shiftLeft {w n : Nat} (x : BitVec w) : (x <<< n).toFin = Fin.ofNat' (2 ^ w) (x.toNat <<< n)

@[simp]

theorem BitVec.shiftLeft_zero {w : Nat} (x : BitVec w) : x <<< 0 = x

@[simp]

theorem BitVec.zero_shiftLeft {w : Nat} (n : Nat) : 0#w <<< n = 0#w

@[simp]

theorem BitVec.getLsbD_shiftLeft {m i : Nat} (x : BitVec m) (n : Nat) : (x <<< n).getLsbD i = (decide (i < m) && !decide (i < n) && x.getLsbD (i - n))

@[simp]

theorem BitVec.getElem_shiftLeft {m i : Nat} {x : BitVec m} {n : Nat} (h : i < m) : (x <<< n)[i] = (!decide (i < n) && x.getLsbD (i - n))

theorem BitVec.shiftLeft_xor_distrib {w : Nat} (x y : BitVec w) (n : Nat) : (x ^^^ y) <<< n = x <<< n ^^^ y <<< n

theorem BitVec.shiftLeft_and_distrib {w : Nat} (x y : BitVec w) (n : Nat) : (x &&& y) <<< n = x <<< n &&& y <<< n

theorem BitVec.shiftLeft_or_distrib {w : Nat} (x y : BitVec w) (n : Nat) : (x ||| y) <<< n = x <<< n ||| y <<< n

@[simp]

theorem BitVec.getMsbD_shiftLeft {w k : Nat} (x : BitVec w) (i : Nat) : (x <<< i).getMsbD k = x.getMsbD (k + i)

theorem BitVec.shiftLeftZeroExtend_eq {w n : Nat} {x : BitVec w} : x.shiftLeftZeroExtend n = BitVec.setWidth (w + n) x <<< n

@[simp]

theorem BitVec.getElem_shiftLeftZeroExtend {m i : Nat} {x : BitVec m} {n : Nat} (h : i < m + n) : (x.shiftLeftZeroExtend n)[i] = (!decide (i < n) && x.getLsbD (i - n))

@[simp]

theorem BitVec.getLsbD_shiftLeftZeroExtend {m i : Nat} (x : BitVec m) (n : Nat) : (x.shiftLeftZeroExtend n).getLsbD i = (!decide (i < n) && x.getLsbD (i - n))

@[simp]

theorem BitVec.getMsbD_shiftLeftZeroExtend {m i : Nat} (x : BitVec m) (n : Nat) : (x.shiftLeftZeroExtend n).getMsbD i = x.getMsbD 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 m : Nat) : x <<< (n + m) = x <<< n <<< m

@[simp]

theorem BitVec.allOnes_shiftLeft_and_shiftLeft {w : Nat} {x : BitVec w} {n : Nat} : BitVec.allOnes w <<< n &&& x <<< n = x <<< n

@[simp]

theorem BitVec.allOnes_shiftLeft_or_shiftLeft {w : Nat} {x : BitVec w} {n : Nat} : BitVec.allOnes w <<< n ||| x <<< n = BitVec.allOnes w <<< n

@[deprecated BitVec.shiftLeft_add]

theorem BitVec.shiftLeft_shiftLeft {w : Nat} (x : BitVec w) (n m : Nat) : x <<< n <<< m = x <<< (n + m)

shiftLeft reductions from BitVec to Nat

@[simp]

theorem BitVec.shiftLeft_eq' {w₁ w₂ : Nat} {x : BitVec w₁} {y : BitVec w₂} : x <<< y = x <<< y.toNat

theorem BitVec.shiftLeft_zero' {w₁ w₂ : Nat} {x : BitVec w₁} : x <<< 0#w₂ = x

theorem BitVec.shiftLeft_shiftLeft' {w₁ w₂ w₃ : Nat} {x : BitVec w₁} {y : BitVec w₂} {z : BitVec w₃} : x <<< y <<< z = x <<< (y.toNat + z.toNat)

theorem BitVec.getLsbD_shiftLeft' {w₁ w₂ : Nat} {x : BitVec w₁} {y : BitVec w₂} {i : Nat} : (x <<< y).getLsbD i = (decide (i < w₁) && !decide (i < y.toNat) && x.getLsbD (i - y.toNat))

@[simp]

theorem BitVec.getElem_shiftLeft' {w₁ w₂ : Nat} {x : BitVec w₁} {y : BitVec w₂} {i : Nat} (h : i < w₁) : (x <<< y)[i] = (!decide (i < y.toNat) && x.getLsbD (i - y.toNat))

ushiftRight

@[simp]

theorem BitVec.toNat_ushiftRight {n : Nat} (x : BitVec n) (i : Nat) : (x >>> i).toNat = x.toNat >>> i

@[simp]

theorem BitVec.getLsbD_ushiftRight {n : Nat} (x : BitVec n) (i j : Nat) : (x >>> i).getLsbD j = x.getLsbD (i + j)

@[simp]

theorem BitVec.getElem_ushiftRight {w : Nat} (x : BitVec w) (i n : Nat) (h : i < w) : (x >>> n)[i] = x.getLsbD (n + i)

theorem BitVec.ushiftRight_xor_distrib {w : Nat} (x y : BitVec w) (n : Nat) : (x ^^^ y) >>> n = x >>> n ^^^ y >>> n

theorem BitVec.ushiftRight_and_distrib {w : Nat} (x y : BitVec w) (n : Nat) : (x &&& y) >>> n = x >>> n &&& y >>> n

theorem BitVec.ushiftRight_or_distrib {w : Nat} (x y : BitVec w) (n : Nat) : (x ||| y) >>> n = x >>> n ||| y >>> n

@[simp]

theorem BitVec.ushiftRight_zero {w : Nat} (x : BitVec w) : x >>> 0 = x

@[simp]

theorem BitVec.zero_ushiftRight {w n : Nat} : 0#w >>> n = 0#w

theorem BitVec.toNat_ushiftRight_lt {w : Nat} (x : BitVec w) (n : Nat) (hn : n ≤ w) : (x >>> n).toNat < 2 ^ (w - n)

Shifting right by n < w yields a bitvector whose value is less than 2 ^ (w - n).

@[simp]

theorem BitVec.getMsbD_ushiftRight {w : Nat} {x : BitVec w} {i n : Nat} : (x >>> n).getMsbD i = (decide (i < w) && (!decide (i < n) && x.getMsbD (i - n)))

@[simp]

theorem BitVec.msb_ushiftRight {w : Nat} {x : BitVec w} {n : Nat} : (x >>> n).msb = (!decide (0 < n) && x.msb)

ushiftRight reductions from BitVec to Nat

@[simp]

theorem BitVec.ushiftRight_eq' {w₁ w₂ : Nat} (x : BitVec w₁) (y : BitVec w₂) : x >>> y = x >>> y.toNat

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.getLsbD_sshiftRight {w : Nat} (x : BitVec w) (s i : Nat) : (x.sshiftRight s).getLsbD i = (!decide (w ≤ i) && if s + i < w then x.getLsbD (s + i) else x.msb)

theorem BitVec.getElem_sshiftRight {w : Nat} {x : BitVec w} {s i : Nat} (h : i < w) : (x.sshiftRight s)[i] = if s + i < w then x.getLsbD (s + i) else x.msb

theorem BitVec.sshiftRight_xor_distrib {w : Nat} (x y : BitVec w) (n : Nat) : (x ^^^ y).sshiftRight n = x.sshiftRight n ^^^ y.sshiftRight n

theorem BitVec.sshiftRight_and_distrib {w : Nat} (x y : BitVec w) (n : Nat) : (x &&& y).sshiftRight n = x.sshiftRight n &&& y.sshiftRight n

theorem BitVec.sshiftRight_or_distrib {w : Nat} (x y : BitVec w) (n : Nat) : (x ||| y).sshiftRight n = x.sshiftRight n ||| y.sshiftRight n

@[simp]

theorem BitVec.msb_sshiftRight {w n : Nat} {x : BitVec w} : (x.sshiftRight n).msb = x.msb

The msb after arithmetic shifting right equals the original msb.

@[simp]

theorem BitVec.sshiftRight_zero {w : Nat} {x : BitVec w} : x.sshiftRight 0 = x

@[simp]

theorem BitVec.zero_sshiftRight {w n : Nat} : (0#w).sshiftRight n = 0#w

theorem BitVec.sshiftRight_add {w : Nat} {x : BitVec w} {m n : Nat} : x.sshiftRight (m + n) = (x.sshiftRight m).sshiftRight n

theorem BitVec.not_sshiftRight {w n : Nat} {b : BitVec w} : ~~~b.sshiftRight n = (~~~b).sshiftRight n

@[simp]

theorem BitVec.not_sshiftRight_not {w : Nat} {x : BitVec w} {n : Nat} : ~~~(~~~x).sshiftRight n = x.sshiftRight n

@[simp]

theorem BitVec.getMsbD_sshiftRight {w : Nat} {x : BitVec w} {i n : Nat} : (x.sshiftRight n).getMsbD i = (decide (i < w) && if i < n then x.msb else x.getMsbD (i - n))

sshiftRight reductions from BitVec to Nat

@[simp]

theorem BitVec.sshiftRight_eq' {w w✝ : Nat} {y : BitVec w✝} (x : BitVec w) : x.sshiftRight' y = x.sshiftRight y.toNat

@[simp]

theorem BitVec.getLsbD_sshiftRight' {w : Nat} {x y : BitVec w} {i : Nat} : (x.sshiftRight' y).getLsbD i = (!decide (w ≤ i) && if y.toNat + i < w then x.getLsbD (y.toNat + i) else x.msb)

@[simp]

theorem BitVec.getElem_sshiftRight' {w : Nat} {x y : BitVec w} {i : Nat} (h : i < w) : (x.sshiftRight' y)[i] = (!decide (w ≤ i) && if y.toNat + i < w then x.getLsbD (y.toNat + i) else x.msb)

@[simp]

theorem BitVec.getMsbD_sshiftRight' {w : Nat} {x y : BitVec w} {i : Nat} : (x.sshiftRight y.toNat).getMsbD i = (decide (i < w) && if i < y.toNat then x.msb else x.getMsbD (i - y.toNat))

@[simp]

theorem BitVec.msb_sshiftRight' {w : Nat} {x y : BitVec w} : (x.sshiftRight' y).msb = x.msb

signExtend

theorem BitVec.signExtend_eq_not_setWidth_not_of_msb_false {w : Nat} {x : BitVec w} {v : Nat} (hmsb : x.msb = false) : BitVec.signExtend v x = BitVec.setWidth v x

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

theorem BitVec.signExtend_eq_not_setWidth_not_of_msb_true {w : Nat} {x : BitVec w} {v : Nat} (hmsb : x.msb = true) : BitVec.signExtend v x = ~~~BitVec.setWidth v (~~~x)

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.

theorem BitVec.getLsbD_signExtend {w : Nat} (x : BitVec w) {v i : Nat} : (BitVec.signExtend v x).getLsbD i = (decide (i < v) && if i < w then x.getLsbD i else x.msb)

theorem BitVec.getElem_signExtend {w : Nat} {x : BitVec w} {v i : Nat} (h : i < v) : (BitVec.signExtend v x)[i] = if i < w then x.getLsbD i else x.msb

theorem BitVec.signExtend_eq_setWidth_of_lt {w : Nat} (x : BitVec w) {v : Nat} (hv : v ≤ w) : BitVec.signExtend v x = BitVec.setWidth v x

Sign extending to a width smaller than the starting width is a truncation.

theorem BitVec.signExtend_eq {w : Nat} (x : BitVec w) : BitVec.signExtend w x = x

Sign extending to the same bitwidth is a no op.

theorem BitVec.toNat_signExtend {w : Nat} (x : BitVec w) {v : Nat} : (BitVec.signExtend v x).toNat = (BitVec.setWidth v x).toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0

Sign extending to a larger bitwidth depends on the msb. If the msb is false, then the result equals the original value. If the msb is true, then we add a value of (2^v - 2^w), which arises from the sign extension.

theorem BitVec.toInt_signExtend_of_lt {w v : Nat} {x : BitVec w} (hv : w < v) : (BitVec.signExtend v x).toInt = x.toInt

theorem BitVec.toInt_signExtend_of_le {w v : Nat} {x : BitVec w} (hv : v ≤ w) : (BitVec.signExtend v x).toInt = (↑x.toNat).bmod (2 ^ v)

theorem BitVec.toInt_signExtend {w v : Nat} (x : BitVec w) : (BitVec.signExtend v x).toInt = (↑x.toNat).bmod (2 ^ min v w)

append

theorem BitVec.append_def {v w : Nat} (x : BitVec v) (y : BitVec w) : x ++ y = x.shiftLeftZeroExtend w ||| BitVec.setWidth' ⋯ y

@[simp]

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

theorem BitVec.getLsbD_append {n m i : Nat} {x : BitVec n} {y : BitVec m} : (x ++ y).getLsbD i = bif decide (i < m) then y.getLsbD i else x.getLsbD (i - m)

theorem BitVec.getElem_append {n m i : Nat} {x : BitVec n} {y : BitVec m} (h : i < n + m) : (x ++ y)[i] = bif decide (i < m) then y.getLsbD i else x.getLsbD (i - m)

@[simp]

theorem BitVec.getMsbD_append {n m i : Nat} {x : BitVec n} {y : BitVec m} : (x ++ y).getMsbD i = bif decide (n ≤ i) then y.getMsbD (i - n) else x.getMsbD i

theorem BitVec.msb_append {w v : Nat} {x : BitVec w} {y : BitVec v} : (x ++ y).msb = bif w == 0 then y.msb else x.msb

@[simp]

theorem BitVec.append_zero_width {w : Nat} (x : BitVec w) (y : BitVec 0) : x ++ y = x

@[simp]

theorem BitVec.zero_width_append {v : Nat} (x : BitVec 0) (y : BitVec v) : x ++ y = BitVec.cast ⋯ y

@[simp]

theorem BitVec.zero_append_zero {v w : Nat} : 0#v ++ 0#w = 0#(v + w)

@[simp]

theorem BitVec.cast_append_right {w v v' : Nat} (h : w + v = w + v') (x : BitVec w) (y : BitVec v) : BitVec.cast h (x ++ y) = x ++ BitVec.cast ⋯ y

@[simp]

theorem BitVec.cast_append_left {w v w' : Nat} (h : w + v = w' + v) (x : BitVec w) (y : BitVec v) : BitVec.cast h (x ++ y) = BitVec.cast ⋯ x ++ y

theorem BitVec.setWidth_append {w v k : Nat} {x : BitVec w} {y : BitVec v} : BitVec.setWidth k (x ++ y) = if h : k ≤ v then BitVec.setWidth k y else BitVec.cast ⋯ (BitVec.setWidth (k - v) x ++ y)

@[simp]

theorem BitVec.setWidth_append_of_eq {v w w' v' : Nat} {x : BitVec v} {y : BitVec w} (h : w' = w) : BitVec.setWidth (v' + w') (x ++ y) = BitVec.setWidth v' x ++ BitVec.setWidth w' y

@[simp]

theorem BitVec.setWidth_cons {w : Nat} {a : Bool} {x : BitVec w} : BitVec.setWidth w (BitVec.cons a x) = x

@[simp]

theorem BitVec.not_append {w v : Nat} {x : BitVec w} {y : BitVec v} : ~~~(x ++ y) = ~~~x ++ ~~~y

@[simp]

theorem BitVec.and_append {w v : Nat} {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} : x₁ ++ y₁ &&& x₂ ++ y₂ = (x₁ &&& x₂) ++ (y₁ &&& y₂)

@[simp]

theorem BitVec.or_append {w v : Nat} {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} : x₁ ++ y₁ ||| x₂ ++ y₂ = (x₁ ||| x₂) ++ (y₁ ||| y₂)

@[simp]

theorem BitVec.xor_append {w v : Nat} {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} : x₁ ++ y₁ ^^^ x₂ ++ y₂ = (x₁ ^^^ x₂) ++ (y₁ ^^^ y₂)

theorem BitVec.shiftRight_add {w : Nat} (x : BitVec w) (n m : Nat) : x >>> (n + m) = x >>> n >>> m

theorem BitVec.shiftLeft_ushiftRight {w : Nat} {x : BitVec w} {n : Nat} : x >>> n <<< n = x &&& BitVec.allOnes w <<< n

@[simp]

theorem BitVec.msb_shiftLeft {w : Nat} {x : BitVec w} {n : Nat} : (x <<< n).msb = x.getMsbD n

@[deprecated BitVec.shiftRight_add]

theorem BitVec.shiftRight_shiftRight {w : Nat} (x : BitVec w) (n m : Nat) : x >>> n >>> m = x >>> (n + m)

rev

theorem BitVec.getLsbD_rev {w : Nat} (x : BitVec w) (i : Fin w) : x.getLsbD ↑i.rev = x.getMsbD ↑i

theorem BitVec.getElem_rev {w : Nat} {x : BitVec w} {i : Fin w} : x[i.rev] = x.getMsbD ↑i

theorem BitVec.getMsbD_rev {w : Nat} (x : BitVec w) (i : Fin w) : x.getMsbD ↑i.rev = x.getLsbD ↑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 |||.

theorem BitVec.getLsbD_cons (b : Bool) {n : Nat} (x : BitVec n) (i : Nat) : (BitVec.cons b x).getLsbD i = if i = n then b else x.getLsbD i

theorem BitVec.getElem_cons {b : Bool} {n : Nat} {x : BitVec n} {i : Nat} (h : i < n + 1) : (BitVec.cons b x)[i] = if i = n then b else x.getLsbD i

@[simp]

theorem BitVec.msb_cons {a : Bool} {w✝ : Nat} {x : BitVec w✝} : (BitVec.cons a x).msb = a

@[simp]

theorem BitVec.getMsbD_cons_zero {a : Bool} {w✝ : Nat} {x : BitVec w✝} : (BitVec.cons a x).getMsbD 0 = a

@[simp]

theorem BitVec.getMsbD_cons_succ {a : Bool} {w✝ : Nat} {x : BitVec w✝} {i : Nat} : (BitVec.cons a x).getMsbD (i + 1) = x.getMsbD i

theorem BitVec.setWidth_succ {w i : Nat} (x : BitVec w) : BitVec.setWidth (i + 1) x = BitVec.cons (x.getLsbD i) (BitVec.setWidth i x)

@[simp]

theorem BitVec.cons_msb_setWidth {w : Nat} (x : BitVec (w + 1)) : BitVec.cons x.msb (BitVec.setWidth w x) = x

@[deprecated]

theorem BitVec.eq_msb_cons_setWidth {w : Nat} (x : BitVec (w + 1)) : x = BitVec.cons x.msb (BitVec.setWidth 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 y : BitVec w) (a 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 y : BitVec w) (a 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 y : BitVec w) (a b : Bool) : BitVec.cons a x ^^^ BitVec.cons b y = BitVec.cons (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.getLsbD_concat {w : Nat} (x : BitVec w) (b : Bool) (i : Nat) : (x.concat b).getLsbD i = if i = 0 then b else x.getLsbD (i - 1)

theorem BitVec.getElem_concat {w : Nat} (x : BitVec w) (b : Bool) (i : Nat) (h : i < w + 1) : (x.concat b)[i] = if i = 0 then b else x.getLsbD (i - 1)

@[simp]

theorem BitVec.getLsbD_concat_zero {w✝ : Nat} {x : BitVec w✝} {b : Bool} : (x.concat b).getLsbD 0 = b

@[simp]

theorem BitVec.getElem_concat_zero {w✝ : Nat} {x : BitVec w✝} {b : Bool} : (x.concat b)[0] = b

@[simp]

theorem BitVec.getLsbD_concat_succ {w✝ : Nat} {x : BitVec w✝} {b : Bool} {i : Nat} : (x.concat b).getLsbD (i + 1) = x.getLsbD i

@[simp]

theorem BitVec.getElem_concat_succ {w : Nat} {b : Bool} {x : BitVec w} {i : Nat} (h : i < w) : (x.concat b)[i + 1] = x[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 y : BitVec w) (a b : Bool) : x.concat a ||| y.concat b = (x ||| y).concat (a || b)

@[simp]

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

@[simp]

theorem BitVec.concat_xor_concat {w : Nat} (x y : BitVec w) (a b : Bool) : x.concat a ^^^ y.concat b = (x ^^^ y).concat (a ^^ b)

shiftConcat

theorem BitVec.getLsbD_shiftConcat {w : Nat} (x : BitVec w) (b : Bool) (i : Nat) : (x.shiftConcat b).getLsbD i = (decide (i < w) && if i = 0 then b else x.getLsbD (i - 1))

theorem BitVec.getLsbD_shiftConcat_eq_decide {w : Nat} (x : BitVec w) (b : Bool) (i : Nat) : (x.shiftConcat b).getLsbD i = (decide (i < w) && (decide (i = 0) && b || decide (0 < i) && x.getLsbD (i - 1)))

theorem BitVec.shiftRight_sub_one_eq_shiftConcat {w wn : Nat} (n : BitVec w) (hwn : 0 < wn) : n >>> (wn - 1) = (n >>> wn).shiftConcat (n.getLsbD (wn - 1))

@[simp]

theorem BitVec.toNat_shiftConcat {w : Nat} {x : BitVec w} {b : Bool} : (x.shiftConcat b).toNat = (x.toNat <<< 1 + b.toNat) % 2 ^ w

theorem BitVec.toNat_shiftConcat_eq_of_lt {w : Nat} {x : BitVec w} {b : Bool} {k : Nat} (hk : k < w) (hx : x.toNat < 2 ^ k) : (x.shiftConcat b).toNat = x.toNat * 2 + b.toNat

x.shiftConcat b does not overflow if x < 2^k for k < w, and so x.shiftConcat b |>.toNat = x.toNat * 2 + b.toNat.

theorem BitVec.toNat_shiftConcat_lt_of_lt {w : Nat} {x : BitVec w} {b : Bool} {k : Nat} (hk : k < w) (hx : x.toNat < 2 ^ k) : (x.shiftConcat b).toNat < 2 ^ (k + 1)

@[simp]

theorem BitVec.zero_concat_false {w : Nat} : (0#w).concat false = 0#(w + 1)

@[simp]

theorem BitVec.getMsbD_concat {i w : Nat} {b : Bool} {x : BitVec w} : (x.concat b).getMsbD i = if i < w then x.getMsbD i else decide (i = w) && b

@[simp]

theorem BitVec.msb_concat {w : Nat} {b : Bool} {x : BitVec w} : (x.concat b).msb = if 0 < w then x.msb else b

add

theorem BitVec.add_def {n : Nat} (x y : BitVec n) : x + y = BitVec.ofNat n (x.toNat + y.toNat)

@[simp]

theorem BitVec.toNat_add {w : Nat} (x 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 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 y : Nat) : BitVec.ofNat n (x + y) = BitVec.ofNat n x + BitVec.ofNat n y

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

theorem BitVec.add_assoc {n : Nat} (x y z : BitVec n) : x + y + z = x + (y + z)

theorem BitVec.instAssociativeHAdd {n : Nat} : Std.Associative fun (x1 x2 : BitVec n) => x1 + x2

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

theorem BitVec.instCommutativeHAdd {n : Nat} : Std.Commutative fun (x1 x2 : BitVec n) => x1 + x2

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

theorem BitVec.instLawfulIdentityHAddOfNatOfNatNat {n : Nat} : Std.LawfulIdentity (fun (x1 x2 : BitVec n) => x1 + x2) 0#n

theorem BitVec.setWidth_add {w i : Nat} (x y : BitVec w) (h : i ≤ w) : BitVec.setWidth i (x + y) = BitVec.setWidth i x + BitVec.setWidth i y

@[simp]

theorem BitVec.toInt_add {w : Nat} (x y : BitVec w) : (x + y).toInt = (x.toInt + y.toInt).bmod (2 ^ w)

theorem BitVec.ofInt_add {n : Nat} (x y : Int) : BitVec.ofInt n (x + y) = BitVec.ofInt n x + BitVec.ofInt n y

@[simp]

theorem BitVec.shiftLeft_add_distrib {w : Nat} {x y : BitVec w} {n : Nat} : (x + y) <<< n = x <<< n + y <<< n

theorem BitVec.add_eq_xor {a b : BitVec 1} : a + b = a ^^^ b

sub/neg

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

@[simp]

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

@[simp]

theorem BitVec.toInt_sub {w : Nat} {x y : BitVec w} : (x - y).toInt = (x.toInt - y.toInt).bmod (2 ^ w)

theorem BitVec.toNat_sub' {n : Nat} (x y : BitVec n) : (x - y).toNat = (x.toNat + (2 ^ n - y.toNat)) % 2 ^ n

@[simp]

theorem BitVec.toFin_sub {n : Nat} (x y : BitVec n) : (x - y).toFin = x.toFin - y.toFin

theorem BitVec.ofFin_sub {n : Nat} (x : Fin (2 ^ n)) (y : BitVec n) : { toFin := x } - y = { toFin := x - y.toFin }

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 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.zero_sub {n : Nat} (x : BitVec n) : 0#n - x = -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.toInt_neg {w : Nat} {x : BitVec w} : (-x).toInt = (-x.toInt).bmod (2 ^ w)

@[simp]

theorem BitVec.toFin_neg {n : Nat} (x : BitVec n) : (-x).toFin = Fin.ofNat' (2 ^ n) (2 ^ n - x.toNat)

theorem BitVec.sub_toAdd {n : Nat} (x 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 y : BitVec w) : x + y - y = x

theorem BitVec.sub_add_cancel {w : Nat} (x y : BitVec w) : x - y + y = x

theorem BitVec.eq_sub_iff_add_eq {w : Nat} {x y z : BitVec w} : x = z - y ↔ x + y = z

theorem BitVec.negOne_eq_allOnes {w : Nat} : -1#w = BitVec.allOnes w

theorem BitVec.neg_eq_not_add {w : Nat} (x : BitVec w) : -x = ~~~x + 1#w

@[simp]

theorem BitVec.neg_neg {w : Nat} {x : BitVec w} : - -x = x

theorem BitVec.neg_ne_iff_ne_neg {w : Nat} {x y : BitVec w} : -x ≠ y ↔ x ≠ -y

@[simp]

theorem BitVec.neg_eq_zero_iff {w : Nat} {x : BitVec w} : -x = 0#w ↔ x = 0#w

theorem BitVec.sub_eq_xor {a b : BitVec 1} : a - b = a ^^^ b

@[simp]

theorem BitVec.sub_eq_self {x : BitVec 1} : -x = x

theorem BitVec.not_neg {w : Nat} (x : BitVec w) : ~~~(-x) = x + -1#w

mul

theorem BitVec.mul_def {n : Nat} {x y : BitVec n} : x * y = { toFin := x.toFin * y.toFin }

@[simp]

theorem BitVec.toNat_mul {n : Nat} (x y : BitVec n) : (x * y).toNat = x.toNat * y.toNat % 2 ^ n

@[simp]

theorem BitVec.toFin_mul {n : Nat} (x y : BitVec n) : (x * y).toFin = x.toFin * y.toFin

theorem BitVec.mul_comm {w : Nat} (x y : BitVec w) : x * y = y * x

theorem BitVec.instCommutativeHMul {w : Nat} : Std.Commutative fun (x y : BitVec w) => x * y

theorem BitVec.mul_assoc {w : Nat} (x y z : BitVec w) : x * y * z = x * (y * z)

theorem BitVec.instAssociativeHMul {w : Nat} : Std.Associative fun (x y : BitVec w) => x * y

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

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

@[simp]

theorem BitVec.mul_zero {w : Nat} {x : BitVec w} : x * 0#w = 0#w

@[simp]

theorem BitVec.zero_mul {w : Nat} {x : BitVec w} : 0#w * x = 0#w

theorem BitVec.mul_add {w : Nat} {x y z : BitVec w} : x * (y + z) = x * y + x * z

theorem BitVec.mul_succ {w : Nat} {x y : BitVec w} : x * (y + 1#w) = x * y + x

theorem BitVec.succ_mul {w : Nat} {x y : BitVec w} : (x + 1#w) * y = x * y + y

theorem BitVec.mul_two {w : Nat} {x : BitVec w} : x * 2#w = x + x

theorem BitVec.two_mul {w : Nat} {x : BitVec w} : 2#w * x = x + x

@[simp]

theorem BitVec.toInt_mul {w : Nat} (x y : BitVec w) : (x * y).toInt = (x.toInt * y.toInt).bmod (2 ^ w)

theorem BitVec.ofInt_mul {n : Nat} (x y : Int) : BitVec.ofInt n (x * y) = BitVec.ofInt n x * BitVec.ofInt n y

theorem BitVec.mul_eq_and {a b : BitVec 1} : a * b = a &&& b

le and lt

theorem BitVec.le_def {n : Nat} {x 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 x y : Nat} : BitVec.ofNat n x ≤ BitVec.ofNat n y ↔ x % 2 ^ n ≤ y % 2 ^ n

theorem BitVec.lt_def {n : Nat} {x 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 x y : Nat} : BitVec.ofNat n x < BitVec.ofNat n y ↔ x % 2 ^ n < y % 2 ^ n

@[simp]

theorem BitVec.not_le {n : Nat} {x y : BitVec n} : ¬x ≤ y ↔ y < x

@[simp]

theorem BitVec.not_lt {n : Nat} {x y : BitVec n} : ¬x < y ↔ y ≤ x

@[simp]

theorem BitVec.le_refl {n : Nat} (x : BitVec n) : x ≤ x

@[simp]

theorem BitVec.lt_irrefl {n : Nat} (x : BitVec n) : ¬x < x

theorem BitVec.le_trans {n : Nat} {x y z : BitVec n} : x ≤ y → y ≤ z → x ≤ z

theorem BitVec.lt_trans {n : Nat} {x y z : BitVec n} : x < y → y < z → x < z

theorem BitVec.le_total {n : Nat} (x y : BitVec n) : x ≤ y ∨ y ≤ x

theorem BitVec.le_antisymm {n : Nat} {x y : BitVec n} : x ≤ y → y ≤ x → x = y

theorem BitVec.lt_asymm {n : Nat} {x y : BitVec n} : x < y → ¬y < x

theorem BitVec.lt_of_le_ne {n : Nat} {x y : BitVec n} : x ≤ y → ¬x = y → x < y

theorem BitVec.ne_of_lt {n : Nat} {x y : BitVec n} : x < y → x ≠ y

theorem BitVec.umod_lt {n : Nat} (x : BitVec n) {y : BitVec n} : 0 < y → x % y < y

theorem BitVec.not_lt_iff_le {w : Nat} {x y : BitVec w} : ¬x < y ↔ y ≤ x

udiv

theorem BitVec.udiv_def {n : Nat} {x y : BitVec n} : x / y = BitVec.ofNat n (x.toNat / y.toNat)

@[simp]

theorem BitVec.toNat_udiv {n : Nat} {x y : BitVec n} : (x / y).toNat = x.toNat / y.toNat

@[simp]

theorem BitVec.zero_udiv {w : Nat} {x : BitVec w} : 0#w / x = 0#w

@[simp]

theorem BitVec.udiv_zero {n : Nat} {x : BitVec n} : x / 0#n = 0#n

@[simp]

theorem BitVec.udiv_one {w : Nat} {x : BitVec w} : x / 1#w = x

@[simp]

theorem BitVec.udiv_eq_and {x y : BitVec 1} : x / y = x &&& y

@[simp]

theorem BitVec.udiv_self {w : Nat} {x : BitVec w} : x / x = if (x == 0#w) = true then 0#w else 1#w

umod

theorem BitVec.umod_def {n : Nat} {x y : BitVec n} : x % y = BitVec.ofNat n (x.toNat % y.toNat)

@[simp]

theorem BitVec.toNat_umod {n : Nat} {x y : BitVec n} : (x % y).toNat = x.toNat % y.toNat

@[simp]

theorem BitVec.umod_zero {n : Nat} {x : BitVec n} : x % 0#n = x

@[simp]

theorem BitVec.zero_umod {w : Nat} {x : BitVec w} : 0#w % x = 0#w

@[simp]

theorem BitVec.umod_one {w : Nat} {x : BitVec w} : x % 1#w = 0#w

@[simp]

theorem BitVec.umod_self {w : Nat} {x : BitVec w} : x % x = 0#w

@[simp]

theorem BitVec.umod_eq_and {x y : BitVec 1} : x % y = x &&& ~~~y

smtUDiv

theorem BitVec.smtUDiv_eq {w : Nat} (x y : BitVec w) : x.smtUDiv y = if y = 0#w then BitVec.allOnes w else x / y

@[simp]

theorem BitVec.smtUDiv_zero {n : Nat} {x : BitVec n} : x.smtUDiv 0#n = BitVec.allOnes n

sdiv

theorem BitVec.sdiv_eq {w : Nat} (x y : BitVec w) : x.sdiv y = match x.msb, y.msb with | false, false => x.udiv y | false, true => -x.udiv (-y) | true, false => -(-x).udiv y | true, true => (-x).udiv (-y)

Equation theorem for sdiv in terms of udiv.

theorem BitVec.toNat_sdiv {w : Nat} {x y : BitVec w} : (x.sdiv y).toNat = match x.msb, y.msb with | false, false => (x.udiv y).toNat | false, true => (-x.udiv (-y)).toNat | true, false => (-(-x).udiv y).toNat | true, true => ((-x).udiv (-y)).toNat

@[simp]

theorem BitVec.zero_sdiv {w : Nat} {x : BitVec w} : (0#w).sdiv x = 0#w

@[simp]

theorem BitVec.sdiv_zero {n : Nat} {x : BitVec n} : x.sdiv 0#n = 0#n

@[simp]

theorem BitVec.sdiv_one {w : Nat} {x : BitVec w} : x.sdiv 1#w = x

theorem BitVec.sdiv_eq_and (x y : BitVec 1) : x.sdiv y = x &&& y

@[simp]

theorem BitVec.sdiv_self {w : Nat} {x : BitVec w} : x.sdiv x = if (x == 0#w) = true then 0#w else 1#w

smtSDiv

theorem BitVec.smtSDiv_eq {w : Nat} (x y : BitVec w) : x.smtSDiv y = match x.msb, y.msb with | false, false => x.smtUDiv y | false, true => -x.smtUDiv (-y) | true, false => -(-x).smtUDiv y | true, true => (-x).smtUDiv (-y)

@[simp]

theorem BitVec.smtSDiv_zero {n : Nat} {x : BitVec n} : x.smtSDiv 0#n = if x.slt 0#n = true then 1#n else BitVec.allOnes n

srem

theorem BitVec.srem_eq {w : Nat} (x y : BitVec w) : x.srem y = match x.msb, y.msb with | false, false => x % y | false, true => x % -y | true, false => -(-x % y) | true, true => -(-x % -y)

smod

theorem BitVec.smod_eq {w : Nat} (x y : BitVec w) : x.smod y = match x.msb, y.msb with | false, false => x.umod y | false, true => let u := x.umod (-y); if u = 0#w then u else u + y | true, false => let u := (-x).umod y; if u = 0#w then u else y - u | true, true => -(-x).umod (-y)

Equation theorem for smod in terms of umod.

theorem BitVec.toNat_smod {w : Nat} {x y : BitVec w} : (x.smod y).toNat = match x.msb, y.msb with | false, false => (x.umod y).toNat | false, true => let u := x.umod (-y); if u = 0#w then u.toNat else (u + y).toNat | true, false => let u := (-x).umod y; if u = 0#w then u.toNat else (y - u).toNat | true, true => (-(-x).umod (-y)).toNat

@[simp]

theorem BitVec.smod_zero {n : Nat} {x : BitVec n} : x.smod 0#n = x

ofBoolList

@[simp]

theorem BitVec.getMsbD_ofBoolListBE {bs : List Bool} {i : Nat} : (BitVec.ofBoolListBE bs).getMsbD i = bs.getD i false

@[simp]

theorem BitVec.getLsbD_ofBoolListBE {bs : List Bool} {i : Nat} : (BitVec.ofBoolListBE bs).getLsbD i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false)

@[simp]

theorem BitVec.getElem_ofBoolListBE {i : Nat} {bs : List Bool} (h : i < bs.length) : (BitVec.ofBoolListBE bs)[i] = bs[bs.length - 1 - i]

@[simp]

theorem BitVec.getLsb_ofBoolListLE {bs : List Bool} {i : Nat} : (BitVec.ofBoolListLE bs).getLsbD i = bs.getD i false

@[simp]

theorem BitVec.getMsbD_ofBoolListLE {bs : List Bool} {i : Nat} : (BitVec.ofBoolListLE bs).getMsbD 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.getLsbD_rotateLeftAux_of_le {w : Nat} {x : BitVec w} {r i : Nat} (hi : i < r) : (x.rotateLeftAux r).getLsbD i = x.getLsbD (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).getLsbD ⟨i, i < 2⟩ = <3 2 1 0 | 6 5>.getLsbD ⟨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.getLsbD_rotateLeftAux_of_geq {w : Nat} {x : BitVec w} {r i : Nat} (hi : i ≥ r) : (x.rotateLeftAux r).getLsbD i = (decide (i < w) && x.getLsbD (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).getLsbD ⟨i, i ≥ 2⟩ = <3 2 1 0 | 6 5>.getLsbD ⟨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.getLsbD_rotateLeft_of_le {w : Nat} {x : BitVec w} {r i : Nat} (hr : r < w) : (x.rotateLeft r).getLsbD i = bif decide (i < r) then x.getLsbD (w - r + i) else decide (i < w) && x.getLsbD (i - r)

When r < w, we give a formula for (x.rotateLeft r).getLsbD i.

@[simp]

theorem BitVec.getLsbD_rotateLeft {w : Nat} {x : BitVec w} {r i : Nat} : (x.rotateLeft r).getLsbD i = bif decide (i < r % w) then x.getLsbD (w - r % w + i) else decide (i < w) && x.getLsbD (i - r % w)

@[simp]

theorem BitVec.getElem_rotateLeft {w : Nat} {x : BitVec w} {r i : Nat} (h : i < w) : (x.rotateLeft r)[i] = if h' : i < r % w then x[w - r % w + i] else x[i - r % w]

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

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

theorem BitVec.getMsbD_rotateLeft_of_lt {r n w : Nat} {x : BitVec w} (hi : r < w) : (x.rotateLeft r).getMsbD n = (decide (n < w) && x.getMsbD ((r + n) % w))

When r < w, we give a formula for (x.rotateLeft r).getMsbD i.

theorem BitVec.getMsbD_rotateLeft {r n w : Nat} {x : BitVec w} : (x.rotateLeft r).getMsbD n = (decide (n < w) && x.getMsbD ((r + n) % w))

@[simp]

theorem BitVec.msb_rotateLeft {m w : Nat} {x : BitVec w} : (x.rotateLeft m).msb = x.getMsbD (m % w)

Rotate Right

theorem BitVec.getLsbD_rotateRightAux_of_le {w : Nat} {x : BitVec w} {r i : Nat} (hi : i < w - r) : (x.rotateRightAux r).getLsbD i = x.getLsbD (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).getLsbD ⟨i, i ≤ 7 - 2⟩ = <1 0 | 6 5 4 3 2>.getLsbD ⟨i, i ≤ 7 - 2⟩ = <6 5 4 3 2>.getLsbD i = <6 5 4 3 2 | 1 0>[i + 2]

theorem BitVec.getLsbD_rotateRightAux_of_geq {w : Nat} {x : BitVec w} {r i : Nat} (hi : i ≥ w - r) : (x.rotateRightAux r).getLsbD i = (decide (i < w) && x.getLsbD (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).getLsbD ⟨i, i ≥ 7 - 2⟩ = <1 0 | 6 5 4 3 2>.getLsbD ⟨i, i ≤ 7 - 2⟩ = <1 0>.getLsbD (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.getLsbD_rotateRight_of_lt {w : Nat} {x : BitVec w} {r i : Nat} (hr : r < w) : (x.rotateRight r).getLsbD i = bif decide (i < w - r) then x.getLsbD (r + i) else decide (i < w) && x.getLsbD (i - (w - r))

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

@[simp]

theorem BitVec.getLsbD_rotateRight {w : Nat} {x : BitVec w} {r i : Nat} : (x.rotateRight r).getLsbD i = bif decide (i < w - r % w) then x.getLsbD (r % w + i) else decide (i < w) && x.getLsbD (i - (w - r % w))

@[simp]

theorem BitVec.getElem_rotateRight {w : Nat} {x : BitVec w} {r i : Nat} (h : i < w) : (x.rotateRight r)[i] = if h' : i < w - r % w then x[r % w + i] else x[i - (w - r % w)]

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

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

@[simp]

theorem BitVec.getMsbD_rotateRight_of_lt {w n m : Nat} {x : BitVec w} (hr : m < w) : (x.rotateRight m).getMsbD n = (decide (n < w) && if n < m % w then x.getMsbD ((w + n - m % w) % w) else x.getMsbD (n - m % w))

When m < w, we give a formula for (x.rotateLeft m).getMsbD i.

@[simp]

theorem BitVec.getMsbD_rotateRight {w n m : Nat} {x : BitVec w} : (x.rotateRight m).getMsbD n = (decide (n < w) && if n < m % w then x.getMsbD ((w + n - m % w) % w) else x.getMsbD (n - m % w))

@[simp]

theorem BitVec.msb_rotateRight {r w : Nat} {x : BitVec w} : (x.rotateRight r).msb = x.getMsbD ((w - r % w) % w)

theorem BitVec.twoPow_eq (w i : Nat) : BitVec.twoPow w i = 1#w <<< i

@[simp]

theorem BitVec.toNat_twoPow (w i : Nat) : (BitVec.twoPow w i).toNat = 2 ^ i % 2 ^ w

@[simp]

theorem BitVec.getLsbD_twoPow {w : Nat} (i j : Nat) : (BitVec.twoPow w i).getLsbD j = (decide (i < w) && decide (i = j))

@[simp]

theorem BitVec.getElem_twoPow {w i j : Nat} (h : j < w) : (BitVec.twoPow w i)[j] = decide (j = i)

@[simp]

theorem BitVec.getMsbD_twoPow {i j w : Nat} : (BitVec.twoPow w i).getMsbD j = (decide (i < w) && decide (j = w - i - 1))

@[simp]

theorem BitVec.msb_twoPow {i w : Nat} : (BitVec.twoPow w i).msb = (decide (i < w) && decide (i = w - 1))

theorem BitVec.and_twoPow {w : Nat} (x : BitVec w) (i : Nat) : x &&& BitVec.twoPow w i = if x.getLsbD i = true then BitVec.twoPow w i else 0#w

theorem BitVec.twoPow_and {w : Nat} (x : BitVec w) (i : Nat) : BitVec.twoPow w i &&& x = if x.getLsbD 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

theorem BitVec.twoPow_zero {w : Nat} : BitVec.twoPow w 0 = 1#w

theorem BitVec.shiftLeft_eq_mul_twoPow {w : Nat} (x : BitVec w) (n : Nat) : x <<< n = x * BitVec.twoPow w n

theorem BitVec.udiv_twoPow_eq_of_lt {w : Nat} {x : BitVec w} {k : Nat} (hk : k < w) : x / BitVec.twoPow w k = x >>> k

The unsigned division of x by 2^k equals shifting x right by k, when k is less than the bitwidth w.

@[simp]

theorem BitVec.true_cons_zero {w : Nat} : BitVec.cons true 0#w = BitVec.twoPow (w + 1) w

@[simp]

theorem BitVec.false_cons_zero {w : Nat} : BitVec.cons false 0#w = 0#(w + 1)

@[simp]

theorem BitVec.zero_concat_true {w : Nat} : (0#w).concat true = 1#(w + 1)

theorem BitVec.setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false {w : Nat} {x : BitVec w} {i : Nat} (hx : x.getLsbD i = false) : BitVec.setWidth w (BitVec.setWidth (i + 1) x) = BitVec.setWidth w (BitVec.setWidth i x)

When the (i+1)th bit of x is false, keeping the lower (i + 1) bits of x equals keeping the lower i bits.

theorem BitVec.setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true {w : Nat} {x : BitVec w} {i : Nat} (hx : x.getLsbD i = true) : BitVec.setWidth w (BitVec.setWidth (i + 1) x) = BitVec.setWidth w (BitVec.setWidth i x) ||| BitVec.twoPow w i

When the (i+1)th bit of x is true, keeping the lower (i + 1) bits of x equalsk eeping the lower i bits and then performing bitwise-or with twoPow i = (1 << i),

theorem BitVec.and_one_eq_setWidth_ofBool_getLsbD {w : Nat} {x : BitVec w} : x &&& 1#w = BitVec.setWidth w (BitVec.ofBool (x.getLsbD 0))

Bitwise and of (x : BitVec w) with 1#w equals zero extending x.lsb to w.

@[simp]

theorem BitVec.replicate_zero_eq {w : Nat} {x : BitVec w} : BitVec.replicate 0 x = 0#0

@[simp]

theorem BitVec.replicate_succ_eq {w n : Nat} {x : BitVec w} : BitVec.replicate (n + 1) x = BitVec.cast ⋯ (x ++ BitVec.replicate n x)

@[simp]

theorem BitVec.getLsbD_replicate {i n w : Nat} (x : BitVec w) : (BitVec.replicate n x).getLsbD i = (decide (i < w * n) && x.getLsbD (i % w))

@[simp]

theorem BitVec.getElem_replicate {i n w : Nat} (x : BitVec w) (h : i < w * n) : (BitVec.replicate n x)[i] = if h' : w = 0 then false else x[i % w]

intMin

def BitVec.intMin (w : Nat) : BitVec w

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

Equations

• BitVec.intMin w = BitVec.twoPow w (w - 1)

theorem BitVec.getLsbD_intMin {i : Nat} (w : Nat) : (BitVec.intMin w).getLsbD i = decide (i + 1 = w)

theorem BitVec.getMsbD_intMin {w i : Nat} : (BitVec.intMin w).getMsbD i = (decide (0 < w) && decide (i = 0))

@[simp]

theorem BitVec.toNat_intMin {w : Nat} : (BitVec.intMin w).toNat = 2 ^ (w - 1) % 2 ^ w

The RHS is zero in case w = 0 which is modeled by wrapping the expression in ... % 2 ^ w.

@[simp]

theorem BitVec.toInt_intMin {w : Nat} : (BitVec.intMin w).toInt = -↑(2 ^ (w - 1) % 2 ^ w)

The RHS is zero in case w = 0 which is modeled by wrapping the expression in ... % 2 ^ w.

theorem BitVec.toInt_intMin_le {w : Nat} (x : BitVec w) : (BitVec.intMin w).toInt ≤ x.toInt

theorem BitVec.intMin_sle {w : Nat} (x : BitVec w) : (BitVec.intMin w).sle x = true

@[simp]

theorem BitVec.neg_intMin {w : Nat} : -BitVec.intMin w = BitVec.intMin w

@[simp]

theorem BitVec.abs_intMin {w : Nat} : (BitVec.intMin w).abs = BitVec.intMin w

theorem BitVec.toInt_neg_of_ne_intMin {w : Nat} {x : BitVec w} (rs : x ≠ BitVec.intMin w) : (-x).toInt = -x.toInt

theorem BitVec.toInt_neg_eq_ite {w : Nat} {x : BitVec w} : (-x).toInt = if x = BitVec.intMin w then x.toInt else -x.toInt

theorem BitVec.msb_intMin {w : Nat} : (BitVec.intMin w).msb = decide (0 < w)

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 = BitVec.twoPow w (w - 1) - 1

@[simp]

theorem BitVec.toNat_intMax {w : Nat} : (BitVec.intMax w).toNat = 2 ^ (w - 1) - 1

@[simp]

theorem BitVec.getLsbD_intMax {i : Nat} (w : Nat) : (BitVec.intMax w).getLsbD i = decide (i + 1 < w)

@[simp]

theorem BitVec.intMax_add_one {w : Nat} : BitVec.intMax w + 1#w = BitVec.intMin w

Non-overflow theorems

theorem BitVec.toNat_add_of_lt {w : Nat} {x y : BitVec w} (h : x.toNat + y.toNat < 2 ^ w) : (x + y).toNat = x.toNat + y.toNat

If x.toNat * y.toNat < 2^w, then the multiplication (x * y) does not overflow.

theorem BitVec.toNat_sub_of_le {n : Nat} {x y : BitVec n} (h : y ≤ x) : (x - y).toNat = x.toNat - y.toNat

If y ≤ x, then the subtraction (x - y) does not overflow. Thus, (x - y).toNat = x.toNat - y.toNat

theorem BitVec.toNat_sub_of_lt {w : Nat} {x y : BitVec w} (h : x < y) : (x - y).toNat = 2 ^ w - (y.toNat - x.toNat)

If y > x, then the subtraction (x - y) does overflow, and the result is the wraparound. Thus, (x - y).toNat = 2^w - (y.toNat - x.toNat).

theorem BitVec.toNat_mul_of_lt {w : Nat} {x y : BitVec w} (h : x.toNat * y.toNat < 2 ^ w) : (x * y).toNat = x.toNat * y.toNat

If x.toNat * y.toNat < 2^w, then the multiplication (x * y) does not overflow. Thus, (x * y).toNat = x.toNat * y.toNat.

theorem BitVec.le_add_iff_sub_le {w : Nat} {x y z : BitVec w} (hxz : z ≤ x) (hbz : y.toNat + z.toNat < 2 ^ w) : x ≤ y + z ↔ x - z ≤ y

x ≤ y + z if and only if x - z ≤ y when x - z and y + z do not overflow.

theorem BitVec.sub_le_sub_iff_le {w : Nat} {x y z : BitVec w} (hxz : z ≤ x) (hyz : z ≤ y) : x - z ≤ y - z ↔ x ≤ y

x - z ≤ y - z if and only if x ≤ y when x - z and y - z do not overflow.

neg

theorem BitVec.msb_eq_toInt {w : Nat} {x : BitVec w} : x.msb = decide (x.toInt < 0)

theorem BitVec.msb_eq_toNat {w : Nat} {x : BitVec w} : x.msb = decide (x.toNat ≥ 2 ^ (w - 1))

abs

theorem BitVec.abs_eq {w : Nat} (x : BitVec w) : x.abs = if x.msb = true then -x else x

@[simp]

theorem BitVec.toNat_abs {w : Nat} {x : BitVec w} : x.abs.toNat = if x.msb = true then 2 ^ w - x.toNat else x.toNat

theorem BitVec.getLsbD_abs {w i : Nat} {x : BitVec w} : x.abs.getLsbD i = if x.msb = true then (-x).getLsbD i else x.getLsbD i

theorem BitVec.getElem_abs {w i : Nat} {x : BitVec w} (h : i < w) : x.abs[i] = if x.msb = true then (-x)[i] else x[i]

theorem BitVec.getMsbD_abs {w i : Nat} {x : BitVec w} : x.abs.getMsbD i = if x.msb = true then (-x).getMsbD i else x.getMsbD i

theorem BitVec.toInt_abs_eq_ite {w : Nat} {x : BitVec w} : x.abs.toInt = if x = BitVec.intMin w then (BitVec.intMin w).toInt else if x.msb = true then -x.toInt else x.toInt

theorem BitVec.toInt_abs_eq_ite_of_ne_intMin {w : Nat} {x : BitVec w} (hx : x ≠ BitVec.intMin w) : x.abs.toInt = if x.msb = true then -x.toInt else x.toInt

theorem BitVec.toInt_abs_eq_natAbs {w : Nat} {x : BitVec w} : x.abs.toInt = if x = BitVec.intMin w then (BitVec.intMin w).toInt else ↑x.toInt.natAbs

The absolute value of x : BitVec w, interpreted as an integer, is a case split:

• When x = intMin w, then x.abs = intMin w
• Otherwise, x.abs.toInt equals the absolute value (x.toInt.natAbs).

This is a simpler version of BitVec.toInt_abs_eq_ite, which hides a case split on x.msb.

theorem BitVec.toInt_abs_eq_natAbs_of_ne_intMin {w : Nat} {x : BitVec w} (hx : x ≠ BitVec.intMin w) : x.abs.toInt = ↑x.toInt.natAbs

Decidable quantifiers

theorem BitVec.forall_zero_iff {P : BitVec 0 → Prop} : (∀ (v : BitVec 0), P v) ↔ P 0#0

theorem BitVec.forall_cons_iff {n : Nat} {P : BitVec (n + 1) → Prop} : (∀ (v : BitVec (n + 1)), P v) ↔ ∀ (x : Bool) (v : BitVec n), P (BitVec.cons x v)

instance BitVec.instDecidableForallBitVecZero (P : BitVec 0 → Prop) [Decidable (P 0#0)] : Decidable (∀ (v : BitVec 0), P v)

instance BitVec.instDecidableForallBitVecSucc {n : Nat} (P : BitVec (n + 1) → Prop) [DecidablePred P] [Decidable (∀ (x : Bool) (v : BitVec n), P (BitVec.cons x v))] : Decidable (∀ (v : BitVec (n + 1)), P v)

Equations

• BitVec.instDecidableForallBitVecSucc P = decidable_of_iff' (∀ (x : Bool) (v : BitVec n), P (BitVec.cons x v)) ⋯

instance BitVec.instDecidableExistsBitVecZero (P : BitVec 0 → Prop) [Decidable (P 0#0)] : Decidable (∃ (v : BitVec 0), P v)

instance BitVec.instDecidableExistsBitVecSucc {n : Nat} (P : BitVec (n + 1) → Prop) [DecidablePred P] [Decidable (∀ (x : Bool) (v : BitVec n), ¬P (BitVec.cons x v))] : Decidable (∃ (v : BitVec (n + 1)), P v)

instance BitVec.instDecidableForallBitVec (n : Nat) (P : BitVec n → Prop) [DecidablePred P] : Decidable (∀ (v : BitVec n), P v)

For small numerals this isn't necessary (as typeclass search can use the above two instances), but for large numerals this provides a shortcut. Note, however, that for large numerals the decision procedure may be very slow, and you should use bv_decide if possible.

instance BitVec.instDecidableExistsBitVec (n : Nat) (P : BitVec n → Prop) [DecidablePred P] : Decidable (∃ (v : BitVec n), P v)

For small numerals this isn't necessary (as typeclass search can use the above two instances), but for large numerals this provides a shortcut. Note, however, that for large numerals the decision procedure may be very slow.

Equations

• BitVec.instDecidableExistsBitVec 0 x_3 = inferInstance
• BitVec.instDecidableExistsBitVec n.succ x_3 = inferInstance

Deprecations

@[reducible, inline, deprecated BitVec.truncate_eq_setWidth]

abbrev BitVec.truncate_eq_zeroExtend {w v : Nat} {x : BitVec w} : BitVec.truncate v x = BitVec.setWidth v x

Equations

• @BitVec.truncate_eq_zeroExtend = @BitVec.truncate_eq_setWidth

@[reducible, inline, deprecated BitVec.toNat_setWidth']

abbrev BitVec.toNat_zeroExtend' {m n : Nat} (p : m ≤ n) (x : BitVec m) : (BitVec.setWidth' p x).toNat = x.toNat

Equations

• @BitVec.toNat_zeroExtend' = @BitVec.toNat_setWidth'

@[reducible, inline, deprecated BitVec.toNat_setWidth]

abbrev BitVec.toNat_zeroExtend {n : Nat} (i : Nat) (x : BitVec n) : (BitVec.setWidth i x).toNat = x.toNat % 2 ^ i

Equations

• @BitVec.toNat_zeroExtend = @BitVec.toNat_setWidth

@[reducible, inline, deprecated BitVec.toNat_setWidth]

abbrev BitVec.toNat_truncate {n : Nat} (i : Nat) (x : BitVec n) : (BitVec.setWidth i x).toNat = x.toNat % 2 ^ i

Equations

• @BitVec.toNat_truncate = @BitVec.toNat_setWidth

@[reducible, inline, deprecated BitVec.setWidth_eq]

abbrev BitVec.zeroExtend_eq {n : Nat} (x : BitVec n) : BitVec.setWidth n x = x

Equations

• @BitVec.zeroExtend_eq = @BitVec.setWidth_eq

@[reducible, inline, deprecated BitVec.setWidth_eq]

abbrev BitVec.truncate_eq {n : Nat} (x : BitVec n) : BitVec.setWidth n x = x

Equations

• @BitVec.truncate_eq = @BitVec.setWidth_eq

@[reducible, inline, deprecated BitVec.setWidth_zero]

abbrev BitVec.zeroExtend_zero (m n : Nat) : BitVec.setWidth m 0#n = 0#m

Equations

• BitVec.zeroExtend_zero = BitVec.setWidth_zero

@[reducible, inline, deprecated BitVec.getElem_setWidth]

abbrev BitVec.getElem_zeroExtend {n : Nat} (m : Nat) (x : BitVec n) (i : Nat) (h : i < m) : (BitVec.setWidth m x)[i] = x.getLsbD i

Equations

• @BitVec.getElem_zeroExtend = @BitVec.getElem_setWidth

@[reducible, inline, deprecated BitVec.getElem_setWidth']

abbrev BitVec.getElem_zeroExtend' {w v : Nat} (x : BitVec w) (i : Nat) (h : w ≤ v) (hi : i < v) : (BitVec.setWidth' h x)[i] = x.getLsbD i

Equations

• @BitVec.getElem_zeroExtend' = @BitVec.getElem_setWidth'

@[reducible, inline, deprecated BitVec.getElem?_setWidth]

abbrev BitVec.getElem?_zeroExtend {n : Nat} (m : Nat) (x : BitVec n) (i : Nat) : (BitVec.setWidth m x)[i]? = if i < m then some (x.getLsbD i) else none

Equations

• @BitVec.getElem?_zeroExtend = @BitVec.getElem?_setWidth

@[reducible, inline, deprecated BitVec.getElem?_setWidth']

abbrev BitVec.getElem?_zeroExtend' {w v : Nat} (x : BitVec w) (i : Nat) (h : w ≤ v) : (BitVec.setWidth' h x)[i]? = if i < v then some (x.getLsbD i) else none

Equations

• @BitVec.getElem?_zeroExtend' = @BitVec.getElem?_setWidth'

@[reducible, inline, deprecated BitVec.getLsbD_setWidth]

abbrev BitVec.getLsbD_zeroExtend {n : Nat} (m : Nat) (x : BitVec n) (i : Nat) : (BitVec.setWidth m x).getLsbD i = (decide (i < m) && x.getLsbD i)

Equations

• @BitVec.getLsbD_zeroExtend = @BitVec.getLsbD_setWidth

@[reducible, inline, deprecated BitVec.getLsbD_setWidth']

abbrev BitVec.getLsbD_zeroExtend' {m n : Nat} (ge : m ≥ n) (x : BitVec n) (i : Nat) : (BitVec.setWidth' ge x).getLsbD i = x.getLsbD i

Equations

• @BitVec.getLsbD_zeroExtend' = @BitVec.getLsbD_setWidth'

@[reducible, inline, deprecated BitVec.getMsbD_setWidth_add]

abbrev BitVec.getMsbD_zeroExtend_add {w k i : Nat} {x : BitVec w} (h : k ≤ i) : (BitVec.setWidth (w + k) x).getMsbD i = x.getMsbD (i - k)

Equations

• @BitVec.getMsbD_zeroExtend_add = @BitVec.getMsbD_setWidth_add

@[reducible, inline, deprecated BitVec.getMsbD_setWidth']

abbrev BitVec.getMsbD_zeroExtend' {m n : Nat} (ge : m ≥ n) (x : BitVec n) (i : Nat) : (BitVec.setWidth' ge x).getMsbD i = (decide (i ≥ m - n) && x.getMsbD (i - (m - n)))

Equations

• @BitVec.getMsbD_zeroExtend' = @BitVec.getMsbD_setWidth'

@[reducible, inline, deprecated BitVec.getElem_setWidth]

abbrev BitVec.getElem_truncate {n : Nat} (m : Nat) (x : BitVec n) (i : Nat) (h : i < m) : (BitVec.setWidth m x)[i] = x.getLsbD i

Equations

• @BitVec.getElem_truncate = @BitVec.getElem_setWidth

@[reducible, inline, deprecated BitVec.getElem?_setWidth]

abbrev BitVec.getElem?_truncate {n : Nat} (m : Nat) (x : BitVec n) (i : Nat) : (BitVec.setWidth m x)[i]? = if i < m then some (x.getLsbD i) else none

Equations

• @BitVec.getElem?_truncate = @BitVec.getElem?_setWidth

@[reducible, inline, deprecated BitVec.getLsbD_setWidth]

abbrev BitVec.getLsbD_truncate {n : Nat} (m : Nat) (x : BitVec n) (i : Nat) : (BitVec.setWidth m x).getLsbD i = (decide (i < m) && x.getLsbD i)

Equations

• @BitVec.getLsbD_truncate = @BitVec.getLsbD_setWidth

@[reducible, inline, deprecated BitVec.msb_setWidth]

abbrev BitVec.msb_truncate {w v : Nat} (x : BitVec w) : (BitVec.setWidth v x).msb = (decide (0 < v) && x.getLsbD (v - 1))

Equations

• @BitVec.msb_truncate = @BitVec.msb_setWidth

@[reducible, inline, deprecated BitVec.cast_setWidth]

abbrev BitVec.cast_zeroExtend {v v' w : Nat} (h : v = v') (x : BitVec w) : BitVec.cast h (BitVec.setWidth v x) = BitVec.setWidth v' x

Equations

• @BitVec.cast_zeroExtend = @BitVec.cast_setWidth

@[reducible, inline, deprecated BitVec.cast_setWidth]

abbrev BitVec.cast_truncate {v v' w : Nat} (h : v = v') (x : BitVec w) : BitVec.cast h (BitVec.setWidth v x) = BitVec.setWidth v' x

Equations

• @BitVec.cast_truncate = @BitVec.cast_setWidth

@[reducible, inline, deprecated BitVec.setWidth_setWidth_of_le]

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

Equations

• @BitVec.zeroExtend_zeroExtend_of_le = @BitVec.setWidth_setWidth_of_le

@[reducible, inline, deprecated BitVec.setWidth_eq]

abbrev BitVec.truncate_eq_self {n : Nat} (x : BitVec n) : BitVec.setWidth n x = x

Equations

• @BitVec.truncate_eq_self = @BitVec.setWidth_eq

@[reducible, inline, deprecated BitVec.setWidth_cast]

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

Equations

• @BitVec.truncate_cast = @BitVec.setWidth_cast

@[reducible, inline, deprecated BitVec.msb_setWidth]

abbrev BitVec.mbs_zeroExtend {w v : Nat} (x : BitVec w) : (BitVec.setWidth v x).msb = (decide (0 < v) && x.getLsbD (v - 1))

Equations

• @BitVec.mbs_zeroExtend = @BitVec.msb_setWidth

@[reducible, inline, deprecated BitVec.msb_setWidth']

abbrev BitVec.mbs_zeroExtend' {w v : Nat} (x : BitVec w) (h : w ≤ v) : (BitVec.setWidth' h x).msb = (decide (0 < v) && x.getLsbD (v - 1))

Equations

• @BitVec.mbs_zeroExtend' = @BitVec.msb_setWidth'

@[reducible, inline, deprecated BitVec.setWidth_one_eq_ofBool_getLsb_zero]

abbrev BitVec.zeroExtend_one_eq_ofBool_getLsb_zero {w : Nat} (x : BitVec w) : BitVec.setWidth 1 x = BitVec.ofBool (x.getLsbD 0)

Equations

• @BitVec.zeroExtend_one_eq_ofBool_getLsb_zero = @BitVec.setWidth_one_eq_ofBool_getLsb_zero

@[reducible, inline, deprecated BitVec.setWidth_ofNat_one_eq_ofNat_one_of_lt]

abbrev BitVec.zeroExtend_ofNat_one_eq_ofNat_one_of_lt {v w : Nat} (hv : 0 < v) : BitVec.setWidth w 1#v = 1#w

Equations

• @BitVec.zeroExtend_ofNat_one_eq_ofNat_one_of_lt = @BitVec.setWidth_ofNat_one_eq_ofNat_one_of_lt

@[reducible, inline, deprecated BitVec.setWidth_one]

abbrev BitVec.truncate_one {w : Nat} {x : BitVec w} : BitVec.setWidth 1 x = BitVec.ofBool (x.getLsbD 0)

Equations

• @BitVec.truncate_one = @BitVec.setWidth_one

@[reducible, inline, deprecated BitVec.setWidth_ofNat_of_le]

abbrev BitVec.truncate_ofNat_of_le {v w : Nat} (h : v ≤ w) (x : Nat) : BitVec.setWidth v (BitVec.ofNat w x) = BitVec.ofNat v x

Equations

• @BitVec.truncate_ofNat_of_le = @BitVec.setWidth_ofNat_of_le

@[reducible, inline, deprecated BitVec.setWidth_or]

abbrev BitVec.truncate_or {w k : Nat} {x y : BitVec w} : BitVec.setWidth k (x ||| y) = BitVec.setWidth k x ||| BitVec.setWidth k y

Equations

• @BitVec.truncate_or = @BitVec.setWidth_or

@[reducible, inline, deprecated BitVec.setWidth_and]

abbrev BitVec.truncate_and {w k : Nat} {x y : BitVec w} : BitVec.setWidth k (x &&& y) = BitVec.setWidth k x &&& BitVec.setWidth k y

Equations

• @BitVec.truncate_and = @BitVec.setWidth_and

@[reducible, inline, deprecated BitVec.setWidth_xor]

abbrev BitVec.truncate_xor {w k : Nat} {x y : BitVec w} : BitVec.setWidth k (x ^^^ y) = BitVec.setWidth k x ^^^ BitVec.setWidth k y

Equations

• @BitVec.truncate_xor = @BitVec.setWidth_xor

@[reducible, inline, deprecated BitVec.setWidth_not]

abbrev BitVec.truncate_not {w k : Nat} {x : BitVec w} (h : k ≤ w) : BitVec.setWidth k (~~~x) = ~~~BitVec.setWidth k x

Equations

• @BitVec.truncate_not = @BitVec.setWidth_not

@[reducible, inline, deprecated BitVec.signExtend_eq_not_setWidth_not_of_msb_false]

abbrev BitVec.signExtend_eq_not_zeroExtend_not_of_msb_false {w : Nat} {x : BitVec w} {v : Nat} (hmsb : x.msb = false) : BitVec.signExtend v x = BitVec.setWidth v x

Equations

• @BitVec.signExtend_eq_not_zeroExtend_not_of_msb_false = @BitVec.signExtend_eq_not_setWidth_not_of_msb_false

@[reducible, inline, deprecated BitVec.signExtend_eq_not_setWidth_not_of_msb_true]

abbrev BitVec.signExtend_eq_not_zeroExtend_not_of_msb_true {w : Nat} {x : BitVec w} {v : Nat} (hmsb : x.msb = true) : BitVec.signExtend v x = ~~~BitVec.setWidth v (~~~x)

Equations

• @BitVec.signExtend_eq_not_zeroExtend_not_of_msb_true = @BitVec.signExtend_eq_not_setWidth_not_of_msb_true

@[reducible, inline, deprecated BitVec.signExtend_eq_setWidth_of_lt]

abbrev BitVec.signExtend_eq_truncate_of_lt {w : Nat} (x : BitVec w) {v : Nat} (hv : v ≤ w) : BitVec.signExtend v x = BitVec.setWidth v x

Equations

• @BitVec.signExtend_eq_truncate_of_lt = @BitVec.signExtend_eq_setWidth_of_lt

@[reducible, inline, deprecated BitVec.truncate_append]

abbrev BitVec.truncate_append {w v k : Nat} {x : BitVec w} {y : BitVec v} : BitVec.setWidth k (x ++ y) = if h : k ≤ v then BitVec.setWidth k y else BitVec.cast ⋯ (BitVec.setWidth (k - v) x ++ y)

Equations

• @BitVec.truncate_append = @BitVec.setWidth_append

@[reducible, inline, deprecated BitVec.truncate_append_of_eq]

abbrev BitVec.truncate_append_of_eq {v w w' v' : Nat} {x : BitVec v} {y : BitVec w} (h : w' = w) : BitVec.setWidth (v' + w') (x ++ y) = BitVec.setWidth v' x ++ BitVec.setWidth w' y

Equations

• @BitVec.truncate_append_of_eq = @BitVec.setWidth_append_of_eq

@[reducible, inline, deprecated BitVec.truncate_cons]

abbrev BitVec.truncate_cons {w : Nat} {a : Bool} {x : BitVec w} : BitVec.setWidth w (BitVec.cons a x) = x

Equations

• @BitVec.truncate_cons = @BitVec.setWidth_cons

@[reducible, inline, deprecated BitVec.truncate_succ]

abbrev BitVec.truncate_succ {w i : Nat} (x : BitVec w) : BitVec.setWidth (i + 1) x = BitVec.cons (x.getLsbD i) (BitVec.setWidth i x)

Equations

• @BitVec.truncate_succ = @BitVec.setWidth_succ

@[reducible, inline, deprecated BitVec.truncate_add]

abbrev BitVec.truncate_add {w i : Nat} (x y : BitVec w) (h : i ≤ w) : BitVec.setWidth i (x + y) = BitVec.setWidth i x + BitVec.setWidth i y

Equations

• @BitVec.truncate_add = @BitVec.setWidth_add

@[reducible, inline, deprecated BitVec.setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false]

abbrev BitVec.zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsbD_false {w : Nat} {x : BitVec w} {i : Nat} (hx : x.getLsbD i = false) : BitVec.setWidth w (BitVec.setWidth (i + 1) x) = BitVec.setWidth w (BitVec.setWidth i x)

Equations

• @BitVec.zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsbD_false = @BitVec.setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false

@[reducible, inline, deprecated BitVec.setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true]

abbrev BitVec.zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsbD_true {w : Nat} {x : BitVec w} {i : Nat} (hx : x.getLsbD i = true) : BitVec.setWidth w (BitVec.setWidth (i + 1) x) = BitVec.setWidth w (BitVec.setWidth i x) ||| BitVec.twoPow w i

Equations

• @BitVec.zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsbD_true = @BitVec.setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true

@[reducible, inline, deprecated BitVec.and_one_eq_setWidth_ofBool_getLsbD]

abbrev BitVec.and_one_eq_zeroExtend_ofBool_getLsbD {w : Nat} {x : BitVec w} : x &&& 1#w = BitVec.setWidth w (BitVec.ofBool (x.getLsbD 0))

Equations

• @BitVec.and_one_eq_zeroExtend_ofBool_getLsbD = @BitVec.and_one_eq_setWidth_ofBool_getLsbD

@[reducible, inline, deprecated BitVec.msb_sshiftRight]

abbrev BitVec.sshiftRight_msb_eq_msb {w n : Nat} {x : BitVec w} : (x.sshiftRight n).msb = x.msb

Equations

• @BitVec.sshiftRight_msb_eq_msb = @BitVec.msb_sshiftRight

@[reducible, inline, deprecated BitVec.shiftLeft_zero]

abbrev BitVec.shiftLeft_zero_eq {w : Nat} (x : BitVec w) : x <<< 0 = x

Equations

• @BitVec.shiftLeft_zero_eq = @BitVec.shiftLeft_zero

@[reducible, inline, deprecated BitVec.ushiftRight_zero]

abbrev BitVec.ushiftRight_zero_eq {w : Nat} (x : BitVec w) : x >>> 0 = x

Equations

• @BitVec.ushiftRight_zero_eq = @BitVec.ushiftRight_zero