@[simp]

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

@[simp]

theorem BitVec.getElem_ofFin {n : Nat} (x : Fin (2 ^ n)) (i : Nat) (h : i < n) : { toFin := x }[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_iff {w n : Nat} {a : Bool} {l : BitVec w} : l[n]? = some a ↔ ∃ (h : n < w), l[n] = a

@[reducible, inline, deprecated BitVec.getElem?_eq_some_iff (since := "2025-02-17")]

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

Equations

• @BitVec.getElem?_eq_some = @BitVec.getElem?_eq_some_iff

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

@[simp]

theorem BitVec.getElem_of_getLsbD_eq_true {w : Nat} {x : BitVec w} {i : Nat} (h : x.getLsbD i = true) : (x[i] = true) = True

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.toNat_lt_twoPow_of_le {m n : Nat} (h : m ≤ n) {x : BitVec m} : x.toNat < 2 ^ n

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_getElem_eq {n : Nat} {x y : BitVec n} : (∀ (i : Nat) (hi : i < n), x[i] = y[i]) → x = y

theorem BitVec.eq_of_getElem_eq_iff {n : Nat} {x y : BitVec n} : x = y ↔ ∀ (i : Nat) (hi : i < n), x[i] = y[i]

theorem BitVec.eq_of_getLsbD_eq_iff {w : Nat} {x y : BitVec w} : x = y ↔ ∀ (i : Nat), i < w → x.getLsbD i = y.getLsbD i

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.toInt_zero_length (x : BitVec 0) : x.toInt = 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.toInt_of_zero_length {w : Nat} (h : w = 0) (x : BitVec w) : x.toInt = 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.eq_of_zero_length {w : Nat} (h : w = 0) {x y : BitVec w} : x = y

theorem BitVec.length_pos_of_ne {w : Nat} {x y : BitVec w} (h : x ≠ y) : 0 < w

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

@[deprecated BitVec.toNat_ofNatLT (since := "2025-02-13")]

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

@[deprecated BitVec.getLsbD_ofNatLT (since := "2025-02-13")]

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

@[deprecated BitVec.getMsbD_ofNatLT (since := "2025-02-13")]

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

theorem BitVec.ofNatLT_eq_ofNat {w n : Nat} (hn : n < 2 ^ w) : n#'hn = BitVec.ofNat w n

@[simp]

theorem BitVec.toFin_ofNat {w : Nat} (x : Nat) : (BitVec.ofNat w x).toFin = Fin.ofNat' (2 ^ w) x

@[simp]

theorem BitVec.finMk_toNat {w : Nat} (x : BitVec w) : ⟨x.toNat, ⋯⟩ = x.toFin

@[simp]

theorem BitVec.toFin_ofNatLT {w n : Nat} (h : n < 2 ^ w) : (n#'h).toFin = ⟨n, h⟩

@[simp]

theorem BitVec.toFin_ofFin {w : Nat} (n : Fin (2 ^ w)) : { toFin := n }.toFin = n

@[simp]

theorem BitVec.ofFin_toFin {w : Nat} (x : BitVec w) : { toFin := x.toFin } = x

@[simp]

theorem BitVec.ofNatLT_finVal {w : Nat} (n : Fin (2 ^ w)) : (↑n)#'⋯ = { toFin := n }

@[simp]

theorem BitVec.ofNatLT_toNat {w : Nat} (x : BitVec w) : x.toNat#'⋯ = x

@[simp]

theorem BitVec.ofNat_finVal {w : Nat} (n : Fin (2 ^ w)) : BitVec.ofNat w ↑n = { toFin := n }

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_toNat_mod_cancel_of_toNat {w : Nat} {x : BitVec w} (h : x.toNat ≠ 0) : (2 ^ w - x.toNat) % 2 ^ w = 2 ^ w - x.toNat

@[simp]

theorem BitVec.toNat_mod_cancel_of_lt {n m : Nat} {x : BitVec n} (h : n < m) : x.toNat % 2 ^ m = 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)

@[simp]

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

@[simp]

theorem BitVec.getElem_ofBool {i : Nat} {b : Bool} {h : i < 1} : (ofBool b)[i] = 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.toNat_toInt_of_msb {w : Nat} (b : BitVec w) (hb : b.msb = false) : b.toInt.toNat = b.toNat

theorem BitVec.toInt_eq_toNat_bmod {n : Nat} (x : BitVec n) : x.toInt = (↑x.toNat).bmod (2 ^ n)

theorem BitVec.toInt_neg_of_msb_true {w : Nat} {x : BitVec w} (h : x.msb = true) : x.toInt < 0

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

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)

theorem BitVec.toInt_ofInt_eq_self {w : Nat} (hw : 0 < w) {n : Int} (h : -2 ^ (w - 1) ≤ n) (h' : n < 2 ^ (w - 1)) : (BitVec.ofInt w n).toInt = 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

@[simp]

theorem BitVec.toNat_one {w : Nat} (h : 0 < w) : (1#w).toNat = 1

@[simp]

theorem BitVec.toInt_one {w : Nat} (h : 1 < w) : (1#w).toInt = 1

@[simp]

theorem BitVec.sub_toNat_mod_cancel_of_msb_true {w : Nat} {x : BitVec w} (h : x.msb = true) : (2 ^ w - x.toNat) % 2 ^ w = 2 ^ w - x.toNat

theorem BitVec.toNat_lt_of_msb_false {w : Nat} {x : BitVec w} (h : x.msb = false) : x.toNat < 2 ^ (w - 1)

theorem BitVec.le_toNat_of_msb_true {w : Nat} {x : BitVec w} (h : x.msb = true) : 2 ^ (w - 1) ≤ x.toNat

theorem BitVec.two_mul_toInt_lt {w : Nat} {x : BitVec w} : 2 * x.toInt < 2 ^ w

x.toInt is less than 2^(w-1). We phrase the fact in terms of 2^w to prevent a case split on w=0 when the lemma is used.

theorem BitVec.two_mul_toInt_le {w : Nat} {x : BitVec w} : 2 * x.toInt ≤ 2 ^ w - 1

theorem BitVec.toInt_lt {w : Nat} {x : BitVec w} : x.toInt < 2 ^ (w - 1)

theorem BitVec.toInt_le {w : Nat} {x : BitVec w} : x.toInt ≤ 2 ^ (w - 1) - 1

theorem BitVec.le_two_mul_toInt {w : Nat} {x : BitVec w} : -2 ^ w ≤ 2 * x.toInt

x.toInt is greater than or equal to -2^(w-1). We phrase the fact in terms of 2^w to prevent a case split on w=0 when the lemma is used.

theorem BitVec.le_toInt {w : Nat} (x : BitVec w) : -2 ^ (w - 1) ≤ x.toInt

sle/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.

theorem BitVec.slt_zero_eq_msb {w : Nat} {x : BitVec w} : x.slt 0#w = x.msb

theorem BitVec.sle_eq_decide {w : Nat} {x y : BitVec w} : x.sle y = decide (x.toInt ≤ y.toInt)

theorem BitVec.slt_eq_decide {w : Nat} {x y : BitVec w} : x.slt y = decide (x.toInt < y.toInt)

theorem BitVec.ule_eq_decide {w : Nat} {x y : BitVec w} : x.ule y = decide (x.toNat ≤ y.toNat)

theorem BitVec.ult_eq_decide {w : Nat} {x y : BitVec w} : x.ult y = decide (x.toNat < y.toNat)

theorem BitVec.ule_eq_decide_le {w : Nat} {x y : BitVec w} : x.ule y = decide (x ≤ y)

theorem BitVec.ult_eq_decide_lt {w : Nat} {x y : BitVec w} : x.ult y = decide (x < y)

theorem BitVec.ule_iff_le {w : Nat} {x y : BitVec w} : x.ule y = true ↔ x ≤ y

theorem BitVec.ult_iff_lt {w : Nat} {x y : BitVec w} : x.ult y = true ↔ x < y

theorem BitVec.sle_iff_toInt_le {w : Nat} {x y : BitVec w} : x.sle y = true ↔ x.toInt ≤ y.toInt

theorem BitVec.slt_iff_toInt_lt {w : Nat} {x y : BitVec w} : x.slt y = true ↔ x.toInt < y.toInt

theorem BitVec.ule_iff_toNat_le {w : Nat} {x y : BitVec w} : x.ule y = true ↔ x.toNat ≤ y.toNat

theorem BitVec.ult_iff_toNat_lt {w : Nat} {x y : BitVec w} : x.ult y = true ↔ x.toNat < y.toNat

theorem BitVec.sle_eq_slt_or_eq {w : Nat} {x y : BitVec w} : x.sle y = (x.slt y || x == y)

theorem BitVec.slt_eq_sle_and_ne {w : Nat} {x y : BitVec w} : x.slt y = (x.sle y && x != y)

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.

@[simp]

theorem BitVec.msb_setWidth'_of_lt {m n : Nat} (p : m < n) {x : BitVec m} : (setWidth' ⋯ x).msb = false

@[simp]

theorem BitVec.toInt_setWidth'_of_lt {m n : Nat} (p : m < n) {x : BitVec m} : (setWidth' ⋯ x).toInt = ↑x.toNat

theorem BitVec.toInt_setWidth' {m n : Nat} (p : m ≤ n) {x : BitVec m} : (setWidth' p x).toInt = if m = n then x.toInt else ↑x.toNat

@[simp]

theorem BitVec.toFin_setWidth' {m n : Nat} (p : m ≤ n) (x : BitVec m) : (setWidth' p x).toFin = Fin.castLE ⋯ x.toFin

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.toInt_extractLsb' {n s m : Nat} {x : BitVec n} : (extractLsb' s m x).toInt = (↑(x.toNat >>> s)).bmod (2 ^ m)

@[simp]

theorem BitVec.toInt_extractLsb {n hi lo : Nat} {x : BitVec n} : (extractLsb hi lo x).toInt = (↑(x.toNat >>> lo)).bmod (2 ^ (hi - lo + 1))

@[simp]

theorem BitVec.toFin_extractLsb' {n s m : Nat} {x : BitVec n} : (extractLsb' s m x).toFin = Fin.ofNat' (2 ^ m) (x.toNat >>> s)

@[simp]

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

@[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.getMsbD_extractLsb' {w start len : Nat} {x : BitVec w} {i : Nat} : (extractLsb' start len x).getMsbD i = (decide (i < len) && (decide (start + len - i ≤ w) && x.getMsbD (w - (start + len - i))))

Get the most significant bit after extractLsb'. With extractLsb', we extract a BitVec len x' with length len from BitVec w x, starting from the element at position start. The function getMsb extracts a bit counting from the most significant bit. Assuming certain conditions, (@extractLsbD' w x start len).getMsbD i is equal to @getMsbD w x (w - (start + len - i)).

Example (w := 10, start := 3, len := 4):

                            |---| = w - (start + len) = 3
                                  |start + len|       = 7
                                        |start|       = 3
                                  | len |             = 4

let x = 9 8 7 6 5 4 3 2 1 0 let x' = x.extractLsb' 3 4 = 6 5 4 3 | | | x'.getMsbD 1 = x.getMsbD (i := w - (start + len - i) = 10 - (3 + 4 - 1) = 4) | x'.getMsbD 0 = x.getMsbD (i := w - (start + len - i) = 10 - (3 + 4 - 0) = 3)

Condition 1: i < len

The index i must be within the range of len.

Condition 2: start + len - i ≤ w

If start + len is larger than w, the high bits at i with w ≤ i are filled with 0, meaning that getMsbD[i] = false for these i. If i is large enough, getMsbD[i] is again within the bounds x. The precise condition is:

start + len - i ≤ w

Example (w := 10, start := 7, len := 5):

                                |= w - (start + len)    = 0
                            |      start + len    |     = 12
                                    |    start    |     = 7
                            |  len  |                   = 5

let x = 9 8 7 6 5 4 3 2 1 0 let x' = x.extractLsb' 7 5 = _ _ 9 8 7 | | | x'.getMsbD (i := 2) = | x.getMsbD (i := w - (start + len - i) = 10 - (7 + 5 - 2)) = | x.getMsbD 0 | ✅ start + len - i ≤ w | 7 + 5 - 2 = 10 ≤ 10 | x'.getMsbD (i := 0) = x.getMsbD (i := w - (start + len - i) = 10 - (7 + 5 - 0)) = x.getMsbD (i := w - (start + len - i) = x.getMsbD (i := -2) -- in Nat becomes 0 ❌ start + len - i ≤ w 7 + 5 - 0 ≤ w

@[simp]

theorem BitVec.msb_extractLsb' {w start len : Nat} {x : BitVec w} : (extractLsb' start len x).msb = (decide (0 < len) && (decide (start + len ≤ w) && x.getMsbD (w - (start + len))))

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

@[simp]

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

@[simp]

theorem BitVec.getMsbD_extractLsb {w hi lo : Nat} {x : BitVec w} {i : Nat} : (extractLsb hi lo x).getMsbD i = (decide (i < hi - lo + 1) && (decide (max hi lo - i < w) && x.getMsbD (w - 1 - (max hi lo - i))))

@[simp]

theorem BitVec.msb_extractLsb {w hi lo : Nat} {x : BitVec w} : (extractLsb hi lo x).msb = (decide (max hi lo < w) && x.getMsbD (w - 1 - max hi lo))

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)

@[simp]

theorem BitVec.extractLsb'_eq_self {w : Nat} {x : BitVec w} : extractLsb' 0 w x = x

Extracting all the bits of a bitvector is an identity operation.

theorem BitVec.getLsbD_eq_extractLsb' {w : Nat} (x : BitVec w) (i : Nat) : x.getLsbD i = (extractLsb' i 1 x == 1#1)

theorem BitVec.getElem_eq_extractLsb' {w : Nat} (x : BitVec w) (i : Nat) (h : i < w) : x[i] = (extractLsb' i 1 x == 1#1)

@[simp]

theorem BitVec.extractLsb'_zero {w start len : Nat} : extractLsb' start len 0#w = 0#len

@[simp]

theorem BitVec.extractLsb'_eq_zero {w : Nat} {x : BitVec w} {start : Nat} : extractLsb' start 0 x = 0#0

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

theorem BitVec.msb_allOnes {w : Nat} (hw : 0 < w) : (allOnes w).msb = true

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

@[simp]

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

@[simp]

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

@[simp]

theorem BitVec.ofNat_xor {w x y : Nat} : BitVec.ofNat w (x ^^^ y) = BitVec.ofNat w x ^^^ BitVec.ofNat w 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 {w : Nat} (x : BitVec w) : x &&& ~~~x = 0

@[simp]

theorem BitVec.not_and_self {w : Nat} (x : BitVec w) : ~~~x &&& x = 0

@[simp]

theorem BitVec.or_not_self {w : Nat} (x : BitVec w) : x ||| ~~~x = allOnes w

@[simp]

theorem BitVec.not_or_self {w : Nat} (x : BitVec w) : ~~~x ||| x = allOnes w

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.

@[simp]

theorem BitVec.ne_not_self {w : Nat} {a : BitVec w} (h : 0 < w) : a ≠ ~~~a

@[simp]

theorem BitVec.not_self_ne {w : Nat} {a : BitVec w} (h : 0 < w) : ~~~a ≠ a

theorem BitVec.not_and {w : Nat} {x y : BitVec w} : ~~~(x &&& y) = ~~~x ||| ~~~y

theorem BitVec.not_or {w : Nat} {x y : BitVec w} : ~~~(x ||| y) = ~~~x &&& ~~~y

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

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

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[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] = if h' : i < n then false else x[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

@[simp]

theorem BitVec.setWidth_shiftLeft_of_le {w i : Nat} {x : BitVec w} {y : Nat} (hi : i ≤ w) : setWidth i (x <<< y) = setWidth i x <<< y

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[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.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.setWidth_ushiftRight {w i : Nat} {x : BitVec w} {y : Nat} (hi : w ≤ i) : setWidth i (x >>> y) = setWidth i x >>> y

ushiftRight reductions from BitVec to Nat

@[simp]

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

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

@[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 h : s + i < w then x[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))

theorem BitVec.toInt_shiftRight_lt {w : Nat} {x : BitVec w} {n : Nat} : x.toInt >>> n < 2 ^ (w - 1)

theorem BitVec.le_toInt_shiftRight {w : Nat} {x : BitVec w} {n : Nat} : -2 ^ (w - 1) ≤ x.toInt >>> n

theorem BitVec.toNat_sshiftRight_of_msb_true {w : Nat} {x : BitVec w} {n : Nat} (h : x.msb = true) : (x.sshiftRight n).toNat = 2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> n

theorem BitVec.toNat_sshiftRight_of_msb_false {w : Nat} {x : BitVec w} {n : Nat} (h : x.msb = false) : (x.sshiftRight n).toNat = x.toNat >>> n

theorem BitVec.toNat_sshiftRight {w : Nat} {x : BitVec w} {n : Nat} : (x.sshiftRight n).toNat = if x.msb = true then 2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> n else x.toNat >>> n

theorem BitVec.toFin_sshiftRight_of_msb_true {w : Nat} {x : BitVec w} {n : Nat} (h : x.msb = true) : (x.sshiftRight n).toFin = Fin.ofNat' (2 ^ w) (2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> n)

theorem BitVec.toFin_sshiftRight_of_msb_false {w : Nat} {x : BitVec w} {n : Nat} (h : x.msb = false) : (x.sshiftRight n).toFin = Fin.ofNat' (2 ^ w) (x.toNat >>> n)

theorem BitVec.toFin_sshiftRight {w : Nat} {x : BitVec w} {n : Nat} : (x.sshiftRight n).toFin = if x.msb = true then Fin.ofNat' (2 ^ w) (2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> n) else Fin.ofNat' (2 ^ w) (x.toNat >>> n)

@[simp]

theorem BitVec.toInt_sshiftRight {w : Nat} {x : BitVec w} {n : Nat} : (x.sshiftRight n).toInt = x.toInt >>> 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.toNat_sshiftRight'_of_msb_true {w : Nat} {x y : BitVec w} (h : x.msb = true) : (x.sshiftRight' y).toNat = 2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> y.toNat

theorem BitVec.toNat_sshiftRight'_of_msb_false {w : Nat} {x y : BitVec w} (h : x.msb = false) : (x.sshiftRight' y).toNat = x.toNat >>> y.toNat

theorem BitVec.toNat_sshiftRight' {w : Nat} {x y : BitVec w} : (x.sshiftRight' y).toNat = if x.msb = true then 2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> y.toNat else x.toNat >>> y.toNat

theorem BitVec.toFin_sshiftRight'_of_msb_true {w : Nat} {x y : BitVec w} (h : x.msb = true) : (x.sshiftRight' y).toFin = Fin.ofNat' (2 ^ w) (2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> y.toNat)

theorem BitVec.toFin_sshiftRight'_of_msb_false {w : Nat} {x y : BitVec w} (h : x.msb = false) : (x.sshiftRight' y).toFin = Fin.ofNat' (2 ^ w) (x.toNat >>> y.toNat)

theorem BitVec.toFin_sshiftRight' {w : Nat} {x y : BitVec w} : (x.sshiftRight' y).toFin = if x.msb = true then Fin.ofNat' (2 ^ w) (2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> y.toNat) else Fin.ofNat' (2 ^ w) (x.toNat >>> y.toNat)

theorem BitVec.toInt_sshiftRight' {w : Nat} {x y : BitVec w} : (x.sshiftRight' y).toInt = x.toInt >>> 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] = if h : y.toNat + i < w then x[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 h : i < w then x[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_le {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.

@[deprecated BitVec.signExtend_eq_setWidth_of_le (since := "2025-03-07")]

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

@[simp]

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_le {w v : Nat} {x : BitVec w} (h : w ≤ v) : (signExtend v x).toInt = x.toInt

If the current width w is smaller than the extended width v, then the value when interpreted as an integer does not change.

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

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

If the current width w is larger than the extended width v, then the value when interpreted as an integer is truncated, and we compute a modulo by 2^v.

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

Interpreting the sign extension of (x : BitVec w) to width v computes x % 2^v (where % is the balanced mod). See toInt_signExtend for a version stated in terms of toInt instead of toNat.

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

theorem BitVec.toInt_signExtend_eq_toInt_bmod_of_le {w v : Nat} (x : BitVec w) (h : v ≤ w) : (signExtend v x).toInt = x.toInt.bmod (2 ^ v)

theorem BitVec.toFin_signExtend_of_le {w v : Nat} {x : BitVec w} (hv : v ≤ w) : (signExtend v x).toFin = Fin.ofNat' (2 ^ v) x.toNat

theorem BitVec.toFin_signExtend {w v : Nat} (x : BitVec w) : (signExtend v x).toFin = Fin.ofNat' (2 ^ v) (x.toNat + if x.msb = true then 2 ^ v - 2 ^ w else 0)

@[simp]

theorem BitVec.signExtend_and {w v : Nat} {x y : BitVec w} : signExtend v (x &&& y) = signExtend v x &&& signExtend v y

@[simp]

theorem BitVec.signExtend_or {w v : Nat} {x y : BitVec w} : signExtend v (x ||| y) = signExtend v x ||| signExtend v y

@[simp]

theorem BitVec.signExtend_xor {w v : Nat} {x y : BitVec w} : signExtend v (x ^^^ y) = signExtend v x ^^^ signExtend v y

@[simp]

theorem BitVec.signExtend_not {w v : Nat} {x : BitVec w} (h : 0 < w) : signExtend v (~~~x) = ~~~signExtend v x

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 h : i < m then y[i] else x[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.setWidth_eq_append_extractLsb' {v : Nat} {x : BitVec v} {w : Nat} : setWidth w x = BitVec.cast ⋯ (0#(w - v) ++ extractLsb' 0 (min v w) x)

A (x : BitVec v) set to width w equals (v - w) zeros, followed by the low (min v w) bits of x`

theorem BitVec.setWidth_eq_append {v : Nat} {x : BitVec v} {w : Nat} (h : v ≤ w) : setWidth w x = BitVec.cast ⋯ (0#(w - v) ++ x)

A (x : BitVec v) set to a width w ≥ v equals (w - v) zeros, followed by x.

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

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)

theorem BitVec.extractLsb'_append_extractLsb'_eq_extractLsb' {w start₂ start₁ len₁ len₂ : Nat} {x : BitVec w} (h : start₂ = start₁ + len₁) : extractLsb' start₂ len₂ x ++ extractLsb' start₁ len₁ x = BitVec.cast ⋯ (extractLsb' start₁ (len₁ + len₂) x)

Combine adjacent extractLsb' operations into a single extractLsb'.

theorem BitVec.not_extractLsb'_append_not_extractLsb'_eq_not_extractLsb' {w start₂ start₁ len₁ len₂ : Nat} {x : BitVec w} (h : start₂ = start₁ + len₁) : ~~~extractLsb' start₂ len₂ x ++ ~~~extractLsb' start₁ len₁ x = BitVec.cast ⋯ (~~~extractLsb' start₁ (len₁ + len₂) x)

Combine adjacent ~~~ (extractLsb _)' operations into a single ~~~ (extractLsb _)'.

theorem BitVec.signExtend_eq_append_extractLsb' {w v : Nat} {x : BitVec w} : signExtend v x = BitVec.cast ⋯ ((if x.msb = true then allOnes (v - w) else 0#(v - w)) ++ extractLsb' 0 (min w v) x)

A sign extension of x : BitVec w equals high bits of either 0 or 1 depending on x.msb, followed by the low bits of x.

theorem BitVec.signExtend_eq_append_of_le {w v : Nat} {x : BitVec w} (h : w ≤ v) : signExtend v x = BitVec.cast ⋯ ((if x.msb = true then allOnes (v - w) else 0#(v - w)) ++ x)

A sign extension of x : BitVec w to a larger bitwidth v ≥ w equals high bits of either 0 or 1 depending on x.msb, followed by x.

theorem BitVec.extractLsb'_append_eq_ite {v w : Nat} {xhi : BitVec v} {xlo : BitVec w} {start len : Nat} : extractLsb' start len (xhi ++ xlo) = if hstart : start < w then if hlen : start + len < w then extractLsb' start len xlo else BitVec.cast ⋯ (extractLsb' (start - w) (len - (w - start)) xhi ++ extractLsb' start (w - start) xlo) else extractLsb' (start - w) len xhi

The 'master theorem' for extracting bits from (xhi ++ xlo), which performs a case analysis on the start index, length, and the lengths of xlo, xhi. · If the start index is entirely out of the xlo bitvector, then grab the bits from xhi. · If the start index is entirely contained in the xlo bitvector, then grab the bits from xlo. · If the start index is split between the two bitvectors, then append (w - start) bits from xlo with (len - (w - start)) bits from xhi. Diagramatically:

               xhi                      xlo
        (<---------------------](<-------w--------]
start+len..start:  (<-----len---*------]
w - start:                      *------*
len - (w -start):  *------------*

theorem BitVec.extractLsb'_append_eq_of_lt {v w : Nat} {xhi : BitVec v} {xlo : BitVec w} {start len : Nat} (h : start + len < w) : extractLsb' start len (xhi ++ xlo) = extractLsb' start len xlo

Extracting bits [start..start+len) from (xhi ++ xlo) equals extracting the bits from xlo when start + len is within xlo.

theorem BitVec.extractLsb'_append_eq_of_le {v w : Nat} {xhi : BitVec v} {xlo : BitVec w} {start len : Nat} (h : w ≤ start) : extractLsb' start len (xhi ++ xlo) = extractLsb' (start - w) len xhi

Extracting bits [start..start+len) from (xhi ++ xlo) equals extracting the bits from xhi when start is outside xlo.

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 h : i = n then b else x[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 h : i = 0 then b else x[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.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]

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)

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.toInt_sub_toInt_lt_twoPow_iff {w : Nat} {x y : BitVec w} : x.toInt - y.toInt < -2 ^ (w - 1) ↔ x.toInt < 0 ∧ 0 ≤ y.toInt ∧ 0 ≤ (x.toInt - y.toInt).bmod (2 ^ w)

theorem BitVec.twoPow_le_toInt_sub_toInt_iff {w : Nat} {x y : BitVec w} : 2 ^ (w - 1) ≤ x.toInt - y.toInt ↔ 0 ≤ x.toInt ∧ y.toInt < 0 ∧ (x.toInt - y.toInt).bmod (2 ^ w) < 0

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)

theorem BitVec.ofInt_neg {w : Nat} {n : Int} : BitVec.ofInt w (-n) = -BitVec.ofInt w n

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

theorem BitVec.not_eq_neg_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_eq_iff_eq_neg {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

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

theorem BitVec.add_neg_eq_sub {w : Nat} {x y : BitVec w} : x + -y = x - y

@[simp]

theorem BitVec.sub_neg {w : Nat} {x y : BitVec w} : x - -y = x + y

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

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

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

theorem BitVec.neg_add_mul_eq_mul_not {w : Nat} {x y : BitVec w} : -(x + x * y) = x * ~~~y

theorem BitVec.neg_mul_not_eq_add_mul {w : Nat} {x y : BitVec w} : -(x * ~~~y) = x + x * y

theorem BitVec.neg_eq_neg_one_mul {w : Nat} (b : BitVec w) : -b = -1#w * b

theorem BitVec.setWidth_mul {w i : Nat} (x y : BitVec w) (h : i ≤ w) : setWidth i (x * y) = setWidth i x * setWidth i 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

theorem BitVec.le_of_lt {w : Nat} {x y : BitVec w} (h : x < y) : x ≤ y

theorem BitVec.le_of_eq {w : Nat} {x y : BitVec w} (h : x = y) : x ≤ y

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

@[simp]

theorem BitVec.lt_allOnes_iff {w : Nat} {x : BitVec w} : x < allOnes w ↔ x ≠ allOnes w

theorem BitVec.le_of_zero_length {w : Nat} (h : w = 0) {x y : BitVec w} : x ≤ y

theorem BitVec.pos_of_msb {w : Nat} {x : BitVec w} (hx : x.msb = true) : 0#w < x

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)

@[simp]

theorem BitVec.msb_udiv_eq_false_of {w : Nat} {x y : BitVec w} (h : x.msb = false) : (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)

@[simp]

theorem BitVec.srem_zero {w : Nat} {x : BitVec w} : x.srem 0#w = x

@[simp]

theorem BitVec.zero_srem {w : Nat} {x : BitVec w} : (0#w).srem x = 0#w

@[simp]

theorem BitVec.srem_one {w : Nat} {x : BitVec w} : x.srem 1#w = 0#w

@[simp]

theorem BitVec.srem_self {w : Nat} {x : BitVec w} : x.srem x = 0#w

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 {w : Nat} {x : BitVec w} : x.smod 0#w = x

@[simp]

theorem BitVec.zero_smod {w : Nat} {x : BitVec w} : (0#w).smod x = 0#w

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)

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

theorem BitVec.toFin_rotateLeft {w : Nat} {x : BitVec w} {r : Nat} : (x.rotateLeft r).toFin = Fin.ofNat' (2 ^ w) (x.toNat <<< (r % w)) ||| x.toFin / Fin.ofNat' (2 ^ w) (2 ^ (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.toInt_rotateRight {w : Nat} {x : BitVec w} {r : Nat} : (x.rotateRight r).toInt = (↑((x >>> (r % w)).toNat ||| (x <<< (w - r % w)).toNat)).bmod (2 ^ w)

theorem BitVec.toFin_rotateRight {w : Nat} {x : BitVec w} {r : Nat} : (x.rotateRight r).toFin = x.toFin / Fin.ofNat' (2 ^ w) (2 ^ (r % w)) ||| Fin.ofNat' (2 ^ w) (x.toNat <<< (w - r % 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

theorem BitVec.toNat_twoPow_of_le {i w : Nat} (h : w ≤ i) : (twoPow w i).toNat = 0

theorem BitVec.toNat_twoPow_of_lt {i w : Nat} (h : i < w) : (twoPow w i).toNat = 2 ^ i

theorem BitVec.toNat_twoPow_eq_ite {i w : Nat} : (twoPow w i).toNat = if i < w then 2 ^ i else 0

@[simp]

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

@[simp]

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

theorem BitVec.toInt_twoPow {w i : Nat} : (twoPow w i).toInt = if w ≤ i then 0 else if i + 1 = w then -↑(2 ^ i) else 2 ^ i

theorem BitVec.toFin_twoPow {w i : Nat} : (twoPow w i).toFin = Fin.ofNat' (2 ^ w) (2 ^ i)

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

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.

theorem BitVec.shiftLeft_neg {w : Nat} {x : BitVec w} {y : Nat} : (-x) <<< y = -x <<< y

@[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_one {w : Nat} {x : BitVec w} : replicate 1 x = BitVec.cast ⋯ x

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

theorem BitVec.BitVec.setWidth_add_eq_mod {w i : Nat} {x y : BitVec w} : setWidth i (x + y) = (setWidth i x + setWidth i y) % twoPow i w

intMin

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

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

Equations

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

theorem BitVec.getLsbD_intMin {i : Nat} (w : Nat) : (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.

theorem BitVec.toNat_intMin_of_pos {w : Nat} (hw : 0 < w) : (intMin w).toNat = 2 ^ (w - 1)

@[simp]

theorem BitVec.intMin_eq_zero_iff {w : Nat} : intMin w = 0#w ↔ w = 0

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_of_pos {v : Nat} (hv : 0 < v) : (intMin v).toInt = -2 ^ (v - 1)

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.neg_eq_intMin {w : Nat} {x : BitVec w} : -x = intMin w ↔ x = intMin w

theorem BitVec.neg_ne_intMin_inj {w : Nat} {x : BitVec w} : -x ≠ intMin w ↔ x ≠ 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)

theorem BitVec.ne_intMin_of_msb_eq_false {w : Nat} (h : 0 < w) {n : BitVec w} (hn : n.msb = false) : n ≠ intMin w

theorem BitVec.toInt_neg_eq_of_msb {w : Nat} {x : BitVec w} (h : x.msb = false) : (-x).toInt = -x.toInt

theorem BitVec.lt_intMin_iff_msb_eq_false {w : Nat} {x : BitVec w} (hw : 0 < w) : x < intMin w ↔ x.msb = false

theorem BitVec.intMin_le_iff_msb_eq_true {w : Nat} {x : BitVec w} (hw : 0 < w) : intMin w ≤ x ↔ x.msb = true

theorem BitVec.le_intMin_of_msb_eq_false {w : Nat} {x : BitVec w} (hx : x.msb = false) : x ≤ intMin w

theorem BitVec.neg_le_intMin_of_msb_eq_true {w : Nat} {x : BitVec w} (hx : x.msb = true) : -x ≤ intMin 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

@[simp]

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

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

theorem BitVec.toFin_abs {w : Nat} {x : BitVec w} : x.abs.toFin = if x.msb = true then Fin.ofNat' (2 ^ w) (2 ^ w - x.toNat) else x.toFin

Reverse

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

theorem BitVec.getElem_reverse {w i : Nat} (x : BitVec w) (h : i < w) : x.reverse[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

@[simp]

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

@[simp]

theorem BitVec.msb_replicate {n w : Nat} {x : BitVec w} : (replicate n x).msb = (decide (0 < n) && x.msb)

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.toFin_uShiftRight (since := "2025-02-18")]

abbrev BitVec.toFin_uShiftRight {w : Nat} {x : BitVec w} {n : Nat} : (x >>> n).toFin = x.toFin / Fin.ofNat' (2 ^ w) (2 ^ n)

Equations

• @BitVec.toFin_uShiftRight = @BitVec.toFin_ushiftRight

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

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