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

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

Prove nonequality 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 : Nat), i < w → x.getLsbD i = y.getLsbD i) : x = y

theorem BitVec.eq_of_getMsbD_eq {w : Nat} {x y : BitVec w} (pred : ∀ (i : Nat), i < 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} : toFin 0 = 0

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

@[simp]

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

@[simp]

theorem BitVec.toInt_ofBool (b : Bool) : (ofBool b).toInt = -b.toInt

@[simp]

theorem BitVec.toFin_ofBool (b : Bool) : (ofBool b).toFin = Fin.ofNat' 2 b.toNat

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

theorem BitVec.ofBool_eq_iff_eq {b b' : Bool} : ofBool b = ofBool b' ↔ b = b'

@[simp]

theorem BitVec.not_ofBool {b : Bool} : ~~~ofBool b = ofBool !b

@[simp]

theorem BitVec.ofBool_and_ofBool {b b' : Bool} : ofBool b &&& ofBool b' = ofBool (b && b')

@[simp]

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

@[simp]

theorem BitVec.ofBool_xor_ofBool {b b' : Bool} : ofBool b ^^^ ofBool b' = 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)

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

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) : (ofBool b)[0]? = some b

@[simp]

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

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

@[simp]

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

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

@[simp]

theorem BitVec.getMsbD_ofBool {i : Nat} (b : Bool) : (ofBool b).getMsbD i = (decide (i = 0) && b)

@[simp]

theorem BitVec.msb_ofBool (b : Bool) : (ofBool b).msb = b

@[simp]

theorem BitVec.one_eq_zero_iff {w : Nat} : 1#w = 0#w ↔ w = 0

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)

theorem BitVec.msb_eq_getMsbD_zero {w : Nat} (x : BitVec w) : x.msb = x.getMsbD 0

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.toInt_eq_toNat_of_lt {n : Nat} {x : BitVec n} (h : 2 * x.toNat < 2 ^ n) : x.toInt = ↑x.toNat

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_of_msb {w : Nat} {x : BitVec w} (h : x.msb = false) : x.toInt = ↑x.toNat

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)

@[simp]

theorem BitVec.ofInt_toInt {w : Nat} {x : BitVec w} : BitVec.ofInt w x.toInt = x

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} : truncate v x = setWidth v x

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem BitVec.toFin_setWidth {w v : Nat} {x : BitVec w} : (setWidth v x).toFin = Fin.ofNat' (2 ^ v) x.toNat

@[simp]

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

@[simp]

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

@[simp]

theorem BitVec.ofNat_toNat {n : Nat} (m : Nat) (x : BitVec n) : BitVec.ofNat m x.toNat = 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) : (setWidth' h x)[i] = x.getLsbD i

@[simp]

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

theorem BitVec.getElem?_setWidth' {w v : Nat} (x : BitVec w) (i : Nat) (h : w ≤ v) : (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) : (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) : (setWidth' ge x).getLsbD i = x.getLsbD i

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem BitVec.getMsbD_setWidth_add {w k i : Nat} {x : BitVec w} (h : k ≤ i) : (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 (setWidth v x) = setWidth v' x

@[simp]

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

@[simp]

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

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

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

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

theorem BitVec.setWidth_one_eq_ofBool_getLsb_zero {w : Nat} (x : BitVec w) : setWidth 1 x = 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) : 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} : setWidth 1 x = 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) : setWidth v (BitVec.ofNat w x) = BitVec.ofNat v x

@[simp]

theorem BitVec.setWidth_setWidth {u : Nat} {x : BitVec u} {w v : Nat} (h : ¬(v < u ∧ v < w)) : setWidth w (setWidth v x) = setWidth w x

Iterated setWidth agrees with the second setWidth except in the case the first setWidth is a non-trivial truncation, and the second setWidth is a non-trivial extension.

extractLsb

@[simp]

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

@[simp]

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

@[simp]

theorem BitVec.extractLsb_toNat {n : Nat} (hi lo : Nat) (x : BitVec n) : (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) : (extractLsb' start len x)[i] = x.getLsbD (start + i)

@[simp]

theorem BitVec.getLsbD_extractLsb' {n : Nat} (start len : Nat) (x : BitVec n) (i : Nat) : (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) : (extractLsb hi lo x)[i] = x.getLsbD (lo + i)

@[simp]

theorem BitVec.getLsbD_extract {n : Nat} (hi lo : Nat) (x : BitVec n) (i : Nat) : (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) : extractLsb' start len x = BitVec.cast ⋯ (extractLsb (len - 1 + start) start x)

allOnes

@[simp]

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

@[simp]

theorem BitVec.toInt_allOnes {w : Nat} : (allOnes w).toInt = if 0 < w then -1 else 0

@[simp]

theorem BitVec.toFin_allOnes {w : Nat} : (allOnes w).toFin = Fin.ofNat' (2 ^ w) (2 ^ w - 1)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem BitVec.ofFin_add_rev {n : Nat} (x : Fin (2 ^ n)) : { toFin := x + x.rev } = 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} : setWidth k (x ||| y) = setWidth k x ||| setWidth k y

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

instance 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

instance 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

instance 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

instance 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 ||| allOnes w = allOnes w

@[simp]

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

@[simp]

theorem BitVec.or_eq_zero_iff {w : Nat} {x y : BitVec w} : x ||| y = 0#w ↔ x = 0#w ∧ y = 0#w

theorem BitVec.extractLsb'_or {w : Nat} {x y : BitVec w} {start len : Nat} : extractLsb' start len (x ||| y) = extractLsb' start len x ||| extractLsb' start len y

theorem BitVec.extractLsb_or {w : Nat} {y x : BitVec w} {hi lo : Nat} : extractLsb lo hi (x ||| y) = extractLsb lo hi x ||| extractLsb lo hi y

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

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

instance 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

instance 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

instance 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 &&& allOnes w = x

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

@[simp]

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

@[simp]

theorem BitVec.and_eq_allOnes_iff {w : Nat} {x y : BitVec w} : x &&& y = allOnes w ↔ x = allOnes w ∧ y = allOnes w

theorem BitVec.extractLsb'_and {w : Nat} {x y : BitVec w} {start len : Nat} : extractLsb' start len (x &&& y) = extractLsb' start len x &&& extractLsb' start len y

theorem BitVec.extractLsb_and {w : Nat} {y x : BitVec w} {hi lo : Nat} : extractLsb lo hi (x &&& y) = extractLsb lo hi x &&& extractLsb lo hi y

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

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

instance 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

instance 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

instance 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

@[simp]

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

@[simp]

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

@[simp]

theorem BitVec.xor_eq_zero_iff {w : Nat} {x y : BitVec w} : x ^^^ y = 0#w ↔ x = y

theorem BitVec.extractLsb'_xor {w : Nat} {x y : BitVec w} {start len : Nat} : extractLsb' start len (x ^^^ y) = extractLsb' start len x ^^^ extractLsb' start len y

theorem BitVec.extractLsb_xor {w : Nat} {y x : BitVec w} {hi lo : Nat} : extractLsb lo hi (x ^^^ y) = extractLsb lo hi x ^^^ extractLsb lo hi y

not

theorem BitVec.not_def {v : Nat} {x : BitVec v} : ~~~x = 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} : k ≤ w → setWidth k (~~~x) = ~~~setWidth k x

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem BitVec.and_not_self {n : Nat} (x : BitVec n) : x &&& ~~~x = 0

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

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)

theorem BitVec.extractLsb'_not_of_lt {w : Nat} {x : BitVec w} {start len : Nat} (h : start + len < w) : extractLsb' start len (~~~x) = ~~~extractLsb' start len x

Negating x and then extracting [start..start+len) is the same as extracting and then negating, as long as the range [start..start+len) is in bounds. See that if the index is out-of-bounds, then extractLsb will return false, which makes the operation not commute.

theorem BitVec.extractLsb_not_of_lt {w : Nat} {x : BitVec w} {hi lo : Nat} (hlo : lo ≤ hi) (hhi : hi < w) : extractLsb hi lo (~~~x) = ~~~extractLsb hi lo x

Negating x and then extracting [lo:hi] is the same as extracting and then negating. For the extraction to be well-behaved, we need the range [lo:hi] to be a valid closed interval inside the bitvector:

1. lo ≤ hi for the interval to be a well-formed closed interval.
2. hi < w, for the interval to be contained inside the bitvector.

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

@[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 = 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} : allOnes w <<< n &&& x <<< n = x <<< n

@[simp]

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

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

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

@[simp]

theorem BitVec.shiftLeft_eq_zero {w : Nat} {x : BitVec w} {n : Nat} (hn : w ≤ n) : x <<< n = 0#w

theorem BitVec.shiftLeft_ofNat_eq {w : Nat} {x : BitVec w} {k : Nat} : x <<< BitVec.ofNat w k = x <<< (k % 2 ^ w)

ushiftRight

@[simp]

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

theorem BitVec.ushiftRight_ofNat_eq {w : Nat} {x : BitVec w} {k : Nat} : x >>> BitVec.ofNat w k = x >>> (k % 2 ^ w)

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

theorem BitVec.ushiftRight_eq_zero {w : Nat} {x : BitVec w} {n : Nat} (hn : w ≤ n) : x >>> n = 0#w

Shifting right by n, which is larger than the bitwidth w produces `0.

theorem BitVec.toInt_ushiftRight_of_lt {w : Nat} {x : BitVec w} {n : Nat} (hn : 0 < n) : (x >>> n).toInt = ↑(x.toNat >>> n)

Unsigned shift right by at least one bit makes the interpretations of the bitvector as an Int or Nat agree, because it makes the value of the bitvector less than or equal to 2^(w-1).

@[simp]

theorem BitVec.toInt_ushiftRight {w : Nat} {x : BitVec w} {n : Nat} : (x >>> n).toInt = if n = 0 then x.toInt else ↑(x.toNat >>> n)

Unsigned shift right by at least one bit makes the interpretations of the bitvector as an Int or Nat agree, because it makes the value of the bitvector less than or equal to 2^(w-1). In the case when n = 0, then the shift right value equals the integer interpretation.

@[simp]

theorem BitVec.toFin_uShiftRight {w : Nat} {x : BitVec w} {n : Nat} : (x >>> n).toFin = x.toFin / Fin.ofNat' (2 ^ w) (2 ^ 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)

@[simp]

theorem BitVec.ushiftRight_self {w : Nat} (n : BitVec w) : n >>> n.toNat = 0#w

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

theorem BitVec.sshiftRight'_ofNat_eq_sshiftRight {w : Nat} {x : BitVec w} {k : Nat} : x.sshiftRight' (BitVec.ofNat w k) = x.sshiftRight (k % 2 ^ w)

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

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)

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)

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

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

signExtend

theorem BitVec.signExtend_eq_setWidth_of_msb_false {w : Nat} {x : BitVec w} {v : Nat} (hmsb : x.msb = false) : signExtend v x = 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) : signExtend v x = ~~~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} : (signExtend v x).getLsbD i = (decide (i < v) && if i < w then x.getLsbD i else x.msb)

theorem BitVec.getMsbD_signExtend {w : Nat} {x : BitVec w} {v i : Nat} : (signExtend v x).getMsbD i = (decide (i < v) && if v - w ≤ i then x.getMsbD (i + w - v) else x.msb)

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

theorem BitVec.msb_signExtend {w v : Nat} {x : BitVec w} : (signExtend v x).msb = (decide (0 < v) && if w ≥ v then x.getMsbD (w - v) else x.msb)

theorem BitVec.signExtend_eq_setWidth_of_lt {w : Nat} (x : BitVec w) {v : Nat} (hv : v ≤ w) : signExtend v x = 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) : 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} : (signExtend v x).toNat = (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) : (signExtend v x).toInt = x.toInt

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

theorem BitVec.toInt_signExtend {w v : Nat} (x : BitVec w) : (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 ||| 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 = if 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] = if 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 = if 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 = if 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} : setWidth k (x ++ y) = if h : k ≤ v then setWidth k y else BitVec.cast ⋯ (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) : setWidth (v' + w') (x ++ y) = setWidth v' x ++ setWidth w' y

@[simp]

theorem BitVec.setWidth_cons {w : Nat} {a : Bool} {x : BitVec w} : setWidth w (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 &&& allOnes w <<< n

@[simp]

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

theorem BitVec.ushiftRight_eq_extractLsb'_of_lt {w : Nat} {x : BitVec w} {n : Nat} (hn : n < w) : x >>> n = BitVec.cast ⋯ (0#n ++ extractLsb' n (w - n) x)

theorem BitVec.shiftLeft_eq_concat_of_lt {w : Nat} {x : BitVec w} {n : Nat} (hn : n < w) : x <<< n = BitVec.cast ⋯ (extractLsb' 0 (w - n) x ++ 0#n)

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) : (cons b x).toNat = b.toNat <<< w ||| x.toNat

theorem BitVec.toNat_cons' {w : Nat} {a : Bool} {x : BitVec w} : (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) : (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) : (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✝} : (cons a x).msb = a

@[simp]

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

@[simp]

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

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

@[simp]

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

@[deprecated "Use the reverse direction of `cons_msb_setWidth`" (since := "2024-09-23")]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem BitVec.cons_append {w₁ w₂ : Nat} (x : BitVec w₁) (y : BitVec w₂) (a : Bool) : cons a x ++ y = BitVec.cast ⋯ (cons a (x ++ y))

theorem BitVec.cons_append_append {w₁ w₂ w₃ : Nat} (x : BitVec w₁) (y : BitVec w₂) (z : BitVec w₃) (a : Bool) : cons a x ++ y ++ z = BitVec.cast ⋯ (cons a (x ++ y ++ z))

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 + 1 < w + 1) : (x.concat b)[i + 1] = x[i]

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

@[simp]

theorem BitVec.toInt_concat {w : Nat} (x : BitVec w) (b : Bool) : (x.concat b).toInt = if w = 0 then -b.toInt else x.toInt * 2 + b.toInt

@[simp]

theorem BitVec.toFin_concat {w : Nat} (x : BitVec w) (b : Bool) : (x.concat b).toFin = ⟨x.toNat * 2 + b.toNat, ⋯⟩

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

@[simp]

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

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)

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

@[simp]

theorem BitVec.getElem_shiftConcat_zero {w : Nat} {x : BitVec w} (b : Bool) (h : 0 < w) : (x.shiftConcat b)[0] = b

@[simp]

theorem BitVec.getElem_shiftConcat_succ {w i : Nat} {x : BitVec w} {b : Bool} (h : i + 1 < w) : (x.shiftConcat b)[i + 1] = x[i]

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)

instance 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

instance 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

instance 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) : setWidth i (x + y) = setWidth i x + 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.toNat_neg_of_pos {n : Nat} {x : BitVec n} (h : 0#n < x) : (-x).toNat = 2 ^ n - x.toNat

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.sub_eq_iff_eq_add {w : Nat} {x y z : BitVec w} : x - y = z ↔ x = z + y

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

@[simp]

theorem BitVec.neg_inj {w : Nat} {x y : BitVec w} : -x = -y ↔ x = y

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

@[simp]

theorem BitVec.add_left_inj {w : Nat} {x y : BitVec w} (z : BitVec w) : x + z = y + z ↔ x = y

@[simp]

theorem BitVec.add_right_inj {w : Nat} {x y : BitVec w} (z : BitVec w) : z + x = z + y ↔ x = y

@[simp]

theorem BitVec.sub_left_inj {w : Nat} {x y : BitVec w} (z : BitVec w) : x - z = y - z ↔ x = y

@[simp]

theorem BitVec.sub_right_inj {w : Nat} {x y : BitVec w} (z : BitVec w) : z - x = z - y ↔ x = y

add self

@[simp]

theorem BitVec.add_left_eq_self {w : Nat} {x y : BitVec w} : x + y = y ↔ x = 0#w

@[simp]

theorem BitVec.add_right_eq_self {w : Nat} {x y : BitVec w} : x + y = x ↔ y = 0#w

@[simp]

theorem BitVec.self_eq_add_right {w : Nat} {x y : BitVec w} : x = x + y ↔ y = 0#w

@[simp]

theorem BitVec.self_eq_add_left {w : Nat} {x y : BitVec w} : x = y + x ↔ y = 0#w

fill

@[simp]

theorem BitVec.getLsbD_fill {w i : Nat} {v : Bool} : (fill w v).getLsbD i = (v && decide (i < w))

@[simp]

theorem BitVec.getMsbD_fill {w i : Nat} {v : Bool} : (fill w v).getMsbD i = (v && decide (i < w))

@[simp]

theorem BitVec.getElem_fill {w i : Nat} {v : Bool} (h : i < w) : (fill w v)[i] = v

@[simp]

theorem BitVec.msb_fill {w : Nat} {v : Bool} : (fill w v).msb = (v && decide (0 < w))

theorem BitVec.fill_eq {w : Nat} {v : Bool} : fill w v = if v = true then allOnes w else 0#w

@[simp]

theorem BitVec.fill_true {w : Nat} : fill w true = allOnes w

@[simp]

theorem BitVec.fill_false {w : Nat} : fill w false = 0#w

@[simp]

theorem BitVec.fill_toNat {w : Nat} {v : Bool} : (fill w v).toNat = if v = true then 2 ^ w - 1 else 0

@[simp]

theorem BitVec.fill_toInt {w : Nat} {v : Bool} : (fill w v).toInt = if (decide (v = true) && decide (0 < w)) = true then -1 else 0

@[simp]

theorem BitVec.fill_toFin {w : Nat} {v : Bool} : (fill w v).toFin = if v = true then (allOnes w).toFin else Fin.ofNat' (2 ^ w) 0

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

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

instance 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

instance 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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

theorem BitVec.not_lt_zero {w : Nat} {x : BitVec w} : ¬x < 0#w

@[simp]

theorem BitVec.le_zero_iff {w : Nat} {x : BitVec w} : x ≤ 0#w ↔ x = 0#w

@[simp]

theorem BitVec.lt_one_iff {w : Nat} {x : BitVec w} (h : 0 < w) : x < 1#w ↔ x = 0#w

@[simp]

theorem BitVec.not_allOnes_lt {w : Nat} {x : BitVec w} : ¬allOnes w < x

@[simp]

theorem BitVec.allOnes_le_iff {w : Nat} {x : BitVec w} : allOnes w ≤ x ↔ x = allOnes w

udiv

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

@[simp]

theorem BitVec.toFin_udiv {n : Nat} {x y : BitVec n} : (x / y).toFin = x.toFin / y.toFin

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

theorem BitVec.msb_udiv {w : Nat} (x y : BitVec w) : (x / y).msb = (x.msb && y == 1#w)

theorem BitVec.msb_udiv_eq_false_of {w : Nat} {x : BitVec w} (h : x.msb = false) (y : BitVec w) : (x / y).msb = false

theorem BitVec.toInt_udiv_of_msb {w : Nat} {x : BitVec w} (h : x.msb = false) (y : BitVec w) : (x / y).toInt = ↑x.toNat / ↑y.toNat

If x is nonnegative (i.e., does not have its msb set), then x / y is nonnegative, thus toInt and toNat coincide.

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.toFin_umod {w : Nat} {x y : BitVec w} : (x % y).toFin = x.toFin % y.toFin

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

theorem BitVec.umod_eq_of_lt {w : Nat} {x y : BitVec w} (h : x < y) : x % y = x

@[simp]

theorem BitVec.msb_umod {w : Nat} {x y : BitVec w} : (x % y).msb = (x.msb && (decide (x < y) || y == 0#w))

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

theorem BitVec.toInt_umod_of_msb {w : Nat} {x y : BitVec w} (h : x.msb = false) : (x % y).toInt = x.toInt % ↑y.toNat

smtUDiv

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

@[simp]

theorem BitVec.smtUDiv_zero {n : Nat} {x : BitVec n} : x.smtUDiv 0#n = 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 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} : (ofBoolListBE bs).getMsbD i = bs.getD i false

@[simp]

theorem BitVec.getLsbD_ofBoolListBE {bs : List Bool} {i : Nat} : (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) : (ofBoolListBE bs)[i] = bs[bs.length - 1 - i]

@[simp]

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

@[simp]

theorem BitVec.getMsbD_ofBoolListLE {bs : List Bool} {i : Nat} : (ofBoolListLE bs).getMsbD i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false)

Rotate Left

theorem BitVec.rotateLeft_def {w : Nat} {x : BitVec w} {r : Nat} : x.rotateLeft r = x <<< (r % w) ||| x >>> (w - r % w)

rotateLeft is defined in terms of left and right shifts.

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

@[simp]

theorem BitVec.toNat_rotateLeft {w : Nat} {x : BitVec w} {r : Nat} : (x.rotateLeft r).toNat = x.toNat <<< (r % w) % 2 ^ w ||| x.toNat >>> (w - r % w)

Rotate Right

theorem BitVec.rotateRight_def {w : Nat} {x : BitVec w} {r : Nat} : x.rotateRight r = x >>> (r % w) ||| x <<< (w - r % w)

rotateRight is defined in terms of left and right shifts.

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

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)

@[simp]

theorem BitVec.toNat_rotateRight {w : Nat} {x : BitVec w} {r : Nat} : (x.rotateRight r).toNat = x.toNat >>> (r % w) ||| x.toNat <<< (w - r % w) % 2 ^ w

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

theorem BitVec.mul_twoPow_eq_shiftLeft {w : Nat} (x : BitVec w) (i : Nat) : x * twoPow w i = x <<< i

theorem BitVec.twoPow_mul_eq_shiftLeft {w : Nat} (x : BitVec w) (i : Nat) : twoPow w i * x = x <<< i

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

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

theorem BitVec.twoPow_mul_twoPow_eq {w : Nat} (i j : Nat) : twoPow w i * twoPow w j = twoPow w (i + j)

2^i * 2^j = 2^(i + j) with bitvectors as well

theorem BitVec.udiv_twoPow_eq_of_lt {w : Nat} {x : BitVec w} {k : Nat} (hk : k < w) : x / 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} : cons true 0#w = twoPow (w + 1) w

@[simp]

theorem BitVec.false_cons_zero {w : Nat} : 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) : setWidth w (setWidth (i + 1) x) = setWidth w (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) : setWidth w (setWidth (i + 1) x) = setWidth w (setWidth i x) ||| 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 = setWidth w (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 {w : Nat} {x : BitVec w} : replicate 0 x = 0#0

@[simp]

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

@[simp]

theorem BitVec.getLsbD_replicate {i n w : Nat} (x : BitVec w) : (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) : (replicate n x)[i] = if h' : w = 0 then false else x[i % w]

theorem BitVec.append_assoc {w₁ w₂ w₃ : Nat} {x₁ : BitVec w₁} {x₂ : BitVec w₂} {x₃ : BitVec w₃} : x₁ ++ x₂ ++ x₃ = BitVec.cast ⋯ (x₁ ++ (x₂ ++ x₃))

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

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

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) : (intMin w).getLsbD i = decide (i + 1 = w)

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

@[simp]

theorem BitVec.toNat_intMin {w : Nat} : (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} : (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) : (intMin w).toInt ≤ x.toInt

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

@[simp]

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

@[simp]

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

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

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

theorem BitVec.msb_intMin {w : Nat} : (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} : (intMax w).toNat = 2 ^ (w - 1) - 1

@[simp]

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

@[simp]

theorem BitVec.intMax_add_one {w : Nat} : intMax w + 1#w = 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 addition (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 = intMin w then (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 ≠ 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 = intMin w then (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 ≠ intMin w) : x.abs.toInt = ↑x.toInt.natAbs

Reverse

theorem BitVec.getLsbD_reverse {w i : Nat} {x : BitVec w} : x.reverse.getLsbD i = x.getMsbD i

theorem BitVec.getMsbD_reverse {w i : Nat} {x : BitVec w} : x.reverse.getMsbD i = x.getLsbD i

theorem BitVec.msb_reverse {w : Nat} {x : BitVec w} : x.reverse.msb = x.getLsbD 0

theorem BitVec.reverse_append {w v : Nat} {x : BitVec w} {y : BitVec v} : (x ++ y).reverse = BitVec.cast ⋯ (y.reverse ++ x.reverse)

@[simp]

theorem BitVec.reverse_cast {w v : Nat} (h : w = v) (x : BitVec w) : (BitVec.cast h x).reverse = BitVec.cast h x.reverse

theorem BitVec.reverse_replicate {w n : Nat} {x : BitVec w} : (replicate n x).reverse = replicate n x.reverse

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 (cons x v)

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

Equations

• BitVec.instDecidableForallBitVecZero P = isTrue ⋯
• BitVec.instDecidableForallBitVecZero P = isFalse ⋯

instance BitVec.instDecidableForallBitVecSucc {n : Nat} (P : BitVec (n + 1) → Prop) [DecidablePred P] [Decidable (∀ (x : Bool) (v : BitVec n), P (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)

Equations

• BitVec.instDecidableExistsBitVecZero P = decidable_of_iff (¬∀ (v : BitVec 0), ¬P v) ⋯

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

Equations

• BitVec.instDecidableExistsBitVecSucc P = decidable_of_iff (¬∀ (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.

Equations

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

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.signExtend_eq_setWidth_of_msb_false (since := "2024-12-08")]

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

Equations

• @BitVec.signExtend_eq_not_setWidth_not_of_msb_false = @BitVec.signExtend_eq_setWidth_of_msb_false

@[reducible, inline, deprecated BitVec.truncate_eq_setWidth (since := "2024-09-18")]

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

Equations

• @BitVec.truncate_eq_zeroExtend = @BitVec.truncate_eq_setWidth

@[reducible, inline, deprecated BitVec.toNat_setWidth' (since := "2024-09-18")]

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

Equations

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

@[reducible, inline, deprecated BitVec.toNat_setWidth (since := "2024-09-18")]

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

Equations

• @BitVec.toNat_zeroExtend = @BitVec.toNat_setWidth

@[reducible, inline, deprecated BitVec.toNat_setWidth (since := "2024-09-18")]

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

Equations

• @BitVec.toNat_truncate = @BitVec.toNat_setWidth

@[reducible, inline, deprecated BitVec.setWidth_eq (since := "2024-09-18")]

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

Equations

• @BitVec.zeroExtend_eq = @BitVec.setWidth_eq

@[reducible, inline, deprecated BitVec.setWidth_eq (since := "2024-09-18")]

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

Equations

• @BitVec.truncate_eq = @BitVec.setWidth_eq

@[reducible, inline, deprecated BitVec.setWidth_zero (since := "2024-09-18")]

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

Equations

• BitVec.zeroExtend_zero = BitVec.setWidth_zero

@[reducible, inline, deprecated BitVec.getElem_setWidth (since := "2024-09-18")]

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

Equations

• @BitVec.getElem_zeroExtend = @BitVec.getElem_setWidth

@[reducible, inline, deprecated BitVec.getElem_setWidth' (since := "2024-09-18")]

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

Equations

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

@[reducible, inline, deprecated BitVec.getElem?_setWidth (since := "2024-09-18")]

abbrev BitVec.getElem?_zeroExtend {n : Nat} (m : Nat) (x : BitVec n) (i : Nat) : (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' (since := "2024-09-18")]

abbrev BitVec.getElem?_zeroExtend' {w v : Nat} (x : BitVec w) (i : Nat) (h : w ≤ v) : (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 (since := "2024-09-18")]

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

Equations

• @BitVec.getLsbD_zeroExtend = @BitVec.getLsbD_setWidth

@[reducible, inline, deprecated BitVec.getLsbD_setWidth' (since := "2024-09-18")]

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

Equations

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

@[reducible, inline, deprecated BitVec.getMsbD_setWidth_add (since := "2024-09-18")]

abbrev BitVec.getMsbD_zeroExtend_add {w k i : Nat} {x : BitVec w} (h : k ≤ i) : (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' (since := "2024-09-18")]

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

Equations

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

@[reducible, inline, deprecated BitVec.getElem_setWidth (since := "2024-09-18")]

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

Equations

• @BitVec.getElem_truncate = @BitVec.getElem_setWidth

@[reducible, inline, deprecated BitVec.getElem?_setWidth (since := "2024-09-18")]

abbrev BitVec.getElem?_truncate {n : Nat} (m : Nat) (x : BitVec n) (i : Nat) : (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 (since := "2024-09-18")]

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

Equations

• @BitVec.getLsbD_truncate = @BitVec.getLsbD_setWidth

@[reducible, inline, deprecated BitVec.msb_setWidth (since := "2024-09-18")]

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

Equations

• @BitVec.msb_truncate = @BitVec.msb_setWidth

@[reducible, inline, deprecated BitVec.cast_setWidth (since := "2024-09-18")]

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

Equations

• @BitVec.cast_zeroExtend = @BitVec.cast_setWidth

@[reducible, inline, deprecated BitVec.cast_setWidth (since := "2024-09-18")]

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

Equations

• @BitVec.cast_truncate = @BitVec.cast_setWidth

@[reducible, inline, deprecated BitVec.setWidth_setWidth_of_le (since := "2024-09-18")]

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

Equations

• @BitVec.zeroExtend_zeroExtend_of_le = @BitVec.setWidth_setWidth_of_le

@[reducible, inline, deprecated BitVec.setWidth_eq (since := "2024-09-18")]

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

Equations

• @BitVec.truncate_eq_self = @BitVec.setWidth_eq

@[reducible, inline, deprecated BitVec.setWidth_cast (since := "2024-09-18")]

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

Equations

• @BitVec.truncate_cast = @BitVec.setWidth_cast

@[reducible, inline, deprecated BitVec.msb_setWidth (since := "2024-09-18")]

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

Equations

• @BitVec.mbs_zeroExtend = @BitVec.msb_setWidth

@[reducible, inline, deprecated BitVec.msb_setWidth' (since := "2024-09-18")]

abbrev BitVec.mbs_zeroExtend' {w v : Nat} (x : BitVec w) (h : w ≤ v) : (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 (since := "2024-09-18")]

abbrev BitVec.zeroExtend_one_eq_ofBool_getLsb_zero {w : Nat} (x : BitVec w) : setWidth 1 x = 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 (since := "2024-09-18")]

abbrev BitVec.zeroExtend_ofNat_one_eq_ofNat_one_of_lt {v w : Nat} (hv : 0 < v) : 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 (since := "2024-09-18")]

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

Equations

• @BitVec.truncate_one = @BitVec.setWidth_one

@[reducible, inline, deprecated BitVec.setWidth_ofNat_of_le (since := "2024-09-18")]

abbrev BitVec.truncate_ofNat_of_le {v w : Nat} (h : v ≤ w) (x : Nat) : 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 (since := "2024-09-18")]

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

Equations

• @BitVec.truncate_or = @BitVec.setWidth_or

@[reducible, inline, deprecated BitVec.setWidth_and (since := "2024-09-18")]

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

Equations

• @BitVec.truncate_and = @BitVec.setWidth_and

@[reducible, inline, deprecated BitVec.setWidth_xor (since := "2024-09-18")]

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

Equations

• @BitVec.truncate_xor = @BitVec.setWidth_xor

@[reducible, inline, deprecated BitVec.setWidth_not (since := "2024-09-18")]

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

Equations

• @BitVec.truncate_not = @BitVec.setWidth_not

@[reducible, inline, deprecated BitVec.signExtend_eq_setWidth_of_msb_false (since := "2024-09-18")]

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

Equations

• @BitVec.signExtend_eq_not_zeroExtend_not_of_msb_false = @BitVec.signExtend_eq_setWidth_of_msb_false

@[reducible, inline, deprecated BitVec.signExtend_eq_not_setWidth_not_of_msb_true (since := "2024-09-18")]

abbrev BitVec.signExtend_eq_not_zeroExtend_not_of_msb_true {w : Nat} {x : BitVec w} {v : Nat} (hmsb : x.msb = true) : signExtend v x = ~~~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 (since := "2024-09-18")]

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

Equations

• @BitVec.signExtend_eq_truncate_of_lt = @BitVec.signExtend_eq_setWidth_of_lt

@[reducible, inline, deprecated BitVec.truncate_append (since := "2024-09-18")]

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

Equations

• @BitVec.truncate_append = @BitVec.setWidth_append

@[reducible, inline, deprecated BitVec.truncate_append_of_eq (since := "2024-09-18")]

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

Equations

• @BitVec.truncate_append_of_eq = @BitVec.setWidth_append_of_eq

@[reducible, inline, deprecated BitVec.truncate_cons (since := "2024-09-18")]

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

Equations

• @BitVec.truncate_cons = @BitVec.setWidth_cons

@[reducible, inline, deprecated BitVec.truncate_succ (since := "2024-09-18")]

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

Equations

• @BitVec.truncate_succ = @BitVec.setWidth_succ

@[reducible, inline, deprecated BitVec.truncate_add (since := "2024-09-18")]

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

Equations

• @BitVec.truncate_add = @BitVec.setWidth_add

@[reducible, inline, deprecated BitVec.setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false (since := "2024-09-18")]

abbrev BitVec.zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsbD_false {w : Nat} {x : BitVec w} {i : Nat} (hx : x.getLsbD i = false) : setWidth w (setWidth (i + 1) x) = setWidth w (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 (since := "2024-09-18")]

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) : setWidth w (setWidth (i + 1) x) = setWidth w (setWidth i x) ||| 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 (since := "2024-09-18")]

abbrev BitVec.and_one_eq_zeroExtend_ofBool_getLsbD {w : Nat} {x : BitVec w} : x &&& 1#w = setWidth w (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 (since := "2024-10-03")]

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 (since := "2024-10-27")]

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 (since := "2024-10-27")]

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

Equations

• @BitVec.ushiftRight_zero_eq = @BitVec.ushiftRight_zero

@[reducible, inline, deprecated BitVec.replicate_zero (since := "2025-01-08")]

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

Equations

• @BitVec.replicate_zero_eq = @BitVec.replicate_zero

@[reducible, inline, deprecated BitVec.replicate_succ (since := "2025-01-08")]

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

Equations

• @BitVec.replicate_succ_eq = @BitVec.replicate_succ