source
@[simp]
theorem BitVec.mk_zero {w : Nat} {h : 0 < 2 ^ w} :
{ toFin := ⟨0, h⟩ } = 0#w
source
@[simp]
theorem BitVec.ofNatLT_zero {w : Nat} {h : 0 < 2 ^ w} :
0#'h = 0#w
source
@[simp]
theorem BitVec.getElem_ofFin {n : Nat} (x : Fin (2 ^ n)) (i : Nat) (h : i < n) :
{ toFin := x }[i] = (↑x).testBit i
source
@[simp]
theorem BitVec.getMsbD_of_ge {w : Nat} (x : BitVec w) (i : Nat) (ge : w ≤ i) :
x.getMsbD i = false
source
@[reducible, inline, deprecated BitVec.getLsbD_of_ge (since := "2025-04-04")]
abbrev BitVec.getLsbD_ge {w : Nat} (x : BitVec w) (i : Nat) (ge : w ≤ i) :
x.getLsbD i = false
Equations

- @BitVec.getLsbD_ge = @BitVec.getLsbD_of_ge

Instances For

source
@[reducible, inline, deprecated BitVec.getMsbD_of_ge (since := "2025-04-04")]
abbrev BitVec.getMsbD_ge {w : Nat} (x : BitVec w) (i : Nat) (ge : w ≤ i) :
x.getMsbD i = false
Equations

- @BitVec.getMsbD_ge = @BitVec.getMsbD_of_ge

Instances For

source
theorem BitVec.lt_of_getLsbD {w : Nat} {x : BitVec w} {i : Nat} :
x.getLsbD i = true → i < w
source
theorem BitVec.lt_of_getMsbD {w : Nat} {x : BitVec w} {i : Nat} :
x.getMsbD i = true → i < w
source
@[simp]
theorem BitVec.getElem?_eq_getElem {w : Nat} {l : BitVec w} {n : Nat} (h : n < w) :
l[n]? = some l[n]
source
theorem BitVec.getElem?_eq_some_iff {w n : Nat} {a : Bool} {l : BitVec w} :
l[n]? = some a ↔ ∃ (h : n < w), l[n] = a
source
theorem BitVec.some_eq_getElem?_iff {w : Nat} {a : Bool} {n : Nat} {l : BitVec w} :
some a = l[n]? ↔ ∃ (h : n < w), l[n] = a
source
theorem BitVec.getElem_of_getElem? {w n : Nat} {a : Bool} {l : BitVec w} :
l[n]? = some a → ∃ (h : n < w), l[n] = a
source
theorem BitVec.getElem?_eq_none_iff {w n : Nat} {l : BitVec w} :
l[n]? = none ↔ w ≤ n
source
theorem BitVec.none_eq_getElem?_iff {w n : Nat} {l : BitVec w} :
none = l[n]? ↔ w ≤ n
source
theorem BitVec.getElem?_eq_none {w n : Nat} {l : BitVec w} (h : w ≤ n) :
l[n]? = none
source
theorem BitVec.getElem?_eq {w : Nat} (l : BitVec w) (i : Nat) :
l[i]? = if h : i < w then some l[i] else none
source
theorem BitVec.some_getElem_eq_getElem? {w : Nat} (l : BitVec w) (i : Nat) (h : i < w) :
some l[i] = l[i]? ↔ True
source
theorem BitVec.getElem?_eq_some_getElem {w : Nat} (l : BitVec w) (i : Nat) (h : i < w) :
l[i]? = some l[i] ↔ True
source
theorem BitVec.getElem_eq_iff {w : Nat} {x : Bool} {l : BitVec w} {n : Nat} {h : n < w} :
l[n] = x ↔ l[n]? = some x
source
theorem BitVec.getElem_eq_getElem? {w : Nat} (l : BitVec w) (i : Nat) (h : i < w) :
l[i] = l[i]?.get ⋯
source
theorem BitVec.getLsbD_eq_getElem?_getD {w : Nat} {x : BitVec w} {i : Nat} :
x.getLsbD i = x[i]?.getD false
source
@[simp]
theorem BitVec.getElem_of_getLsbD_eq_true {w : Nat} {x : BitVec w} {i : Nat} (h : x.getLsbD i = true) :
(x[i] = true) = True
source
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`.

source
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.

source
@[simp]
theorem BitVec.val_toFin {w : Nat} (x : BitVec w) :
↑x.toFin = x.toNat
source
theorem BitVec.toNat_eq {n : Nat} {x y : BitVec n} :
x = y ↔ x.toNat = y.toNat
source
theorem BitVec.toNat_inj {n : Nat} {x y : BitVec n} :
x.toNat = y.toNat ↔ x = y
source
theorem BitVec.toNat_ne {n : Nat} {x y : BitVec n} :
x ≠ y ↔ x.toNat ≠ y.toNat
source
theorem BitVec.toNat_lt_twoPow_of_le {m n : Nat} (h : m ≤ n) {x : BitVec m} :
x.toNat < 2 ^ n
source
theorem BitVec.two_pow_le_toNat_of_getElem_eq_true {w i : Nat} {x : BitVec w} (hi : i < w) (hx : x[i] = true) :
2 ^ i ≤ x.toNat
source
theorem BitVec.msb_eq_getMsbD {w : Nat} (x : BitVec w) :
x.msb = x.getMsbD 0
source
theorem BitVec.getMsb_eq_getLsb {w : Nat} (x : BitVec w) (i : Fin w) :
x.getMsb i = x.getLsb ⟨w - 1 - ↑i, ⋯⟩
source
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
source
theorem BitVec.getMsbD_eq_getLsbD {w : Nat} (x : BitVec w) (i : Nat) :
x.getMsbD i = (decide (i < w) && x.getLsbD (w - 1 - i))
source
@[deprecated BitVec.getMsb_eq_getLsb (since := "2025-06-17")]
theorem BitVec.getMsb'_eq_getLsb' {w : Nat} (x : BitVec w) (i : Nat) :
x.getMsbD i = (decide (i < w) && x.getLsbD (w - 1 - i))
source
theorem BitVec.getLsbD_eq_getMsbD {w : Nat} (x : BitVec w) (i : Nat) :
x.getLsbD i = (decide (i < w) && x.getMsbD (w - 1 - i))
source
@[simp]
theorem BitVec.getElem?_of_ge {w : Nat} (x : BitVec w) (i : Nat) (ge : w ≤ i) :
x[i]? = none
source
@[simp]
theorem BitVec.getMsb?_of_ge {w : Nat} (x : BitVec w) (i : Nat) (ge : w ≤ i) :
x.getMsb? i = none
source
@[reducible, inline, deprecated BitVec.getElem?_of_ge (since := "2025-04-04")]
abbrev BitVec.getLsb?_ge {w : Nat} (x : BitVec w) (i : Nat) (ge : w ≤ i) :
x[i]? = none
Equations

- @BitVec.getLsb?_ge = @BitVec.getElem?_of_ge

Instances For

source
@[reducible, inline, deprecated BitVec.getMsb?_of_ge (since := "2025-04-04")]
abbrev BitVec.getMsb?_ge {w : Nat} (x : BitVec w) (i : Nat) (ge : w ≤ i) :
x.getMsb? i = none
Equations

- @BitVec.getMsb?_ge = @BitVec.getMsb?_of_ge

Instances For

source
theorem BitVec.lt_of_getElem?_eq_some {w : Nat} {b : Bool} (x : BitVec w) (i : Nat) :
x[i]? = some b → i < w
source
theorem BitVec.lt_of_getMsb?_eq_some {w : Nat} {b : Bool} (x : BitVec w) (i : Nat) :
x.getMsb? i = some b → i < w
source
theorem BitVec.lt_of_isSome_getElem? {w : Nat} (x : BitVec w) (i : Nat) :
x[i]?.isSome = true → i < w
source
theorem BitVec.lt_of_isSome_getMsb? {w : Nat} (x : BitVec w) (i : Nat) :
(x.getMsb? i).isSome = true → i < w
source
@[reducible, inline, deprecated BitVec.lt_of_getElem?_eq_some (since := "2025-04-04")]
abbrev BitVec.lt_of_getLsb?_eq_some {w : Nat} {b : Bool} (x : BitVec w) (i : Nat) :
x[i]? = some b → i < w
Equations

- @BitVec.lt_of_getLsb?_eq_some = @BitVec.lt_of_getElem?_eq_some

Instances For

source
@[reducible, inline, deprecated BitVec.lt_of_isSome_getElem? (since := "2025-04-04")]
abbrev BitVec.lt_of_getLsb?_isSome {w : Nat} (x : BitVec w) (i : Nat) :
x[i]?.isSome = true → i < w
Equations

- @BitVec.lt_of_getLsb?_isSome = @BitVec.lt_of_isSome_getElem?

Instances For

source
@[reducible, inline, deprecated BitVec.lt_of_isSome_getMsb? (since := "2025-04-04")]
abbrev BitVec.lt_of_getMsb?_isSome {w : Nat} (x : BitVec w) (i : Nat) :
(x.getMsb? i).isSome = true → i < w
Equations

- @BitVec.lt_of_getMsb?_isSome = @BitVec.lt_of_isSome_getMsb?

Instances For

source
theorem BitVec.getMsbD_eq_getMsb?_getD {w : Nat} (x : BitVec w) (i : Nat) :
x.getMsbD i = (x.getMsb? i).getD false
source
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
source
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
source
theorem BitVec.of_length_zero {x : BitVec 0} :
x = 0#0
source
theorem BitVec.toNat_zero_length (x : BitVec 0) :
x.toNat = 0
source
theorem BitVec.toInt_zero_length (x : BitVec 0) :
x.toInt = 0
source
theorem BitVec.toNat_zero {w : Nat} :
(0#w).toNat = 0
source
theorem BitVec.getLsbD_zero_length {i : Nat} (x : BitVec 0) :
x.getLsbD i = false
source
theorem BitVec.getMsbD_zero_length {i : Nat} (x : BitVec 0) :
x.getMsbD i = false
source
theorem BitVec.msb_zero_length (x : BitVec 0) :
x.msb = false
source
theorem BitVec.toNat_of_zero_length {w : Nat} (h : w = 0) (x : BitVec w) :
x.toNat = 0
source
theorem BitVec.toInt_of_zero_length {w : Nat} (h : w = 0) (x : BitVec w) :
x.toInt = 0
source
theorem BitVec.getLsbD_of_zero_length {w i : Nat} (h : w = 0) (x : BitVec w) :
x.getLsbD i = false
source
theorem BitVec.getMsbD_of_zero_length {w i : Nat} (h : w = 0) (x : BitVec w) :
x.getMsbD i = false
source
theorem BitVec.msb_of_zero_length {w : Nat} (h : w = 0) (x : BitVec w) :
x.msb = false
source
theorem BitVec.eq_of_zero_length {w : Nat} (h : w = 0) {x y : BitVec w} :
x = y
source
theorem BitVec.length_pos_of_ne {w : Nat} {x y : BitVec w} (h : x ≠ y) :
0 < w
source
theorem BitVec.ofFin_ofNat {w : Nat} (n : Nat) :
{ toFin := OfNat.ofNat n } = OfNat.ofNat n
source
@[simp]
theorem BitVec.ofFin_neg {w : Nat} {x : Fin (2 ^ w)} :
{ toFin := -x } = -{ toFin := x }
source
@[simp]
theorem BitVec.ofFin_natCast {w : Nat} (n : Nat) :
{ toFin := ↑n } = ↑n
source
theorem BitVec.eq_of_toFin_eq {w : Nat} {x y : BitVec w} :
x.toFin = y.toFin → x = y
source
theorem BitVec.toFin_inj {w : Nat} {x y : BitVec w} :
x.toFin = y.toFin ↔ x = y
source
theorem BitVec.toFin_zero {w : Nat} :
toFin 0 = 0
source
theorem BitVec.toFin_one {w : Nat} :
toFin 1 = 1
source
@[simp]
theorem BitVec.toFin_natCast {w : Nat} (n : Nat) :
(↑n).toFin = ↑n
source
@[simp]
theorem BitVec.toFin_ofBool (b : Bool) :
(ofBool b).toFin = Fin.ofNat 2 b.toNat
source
theorem BitVec.ofNat_one (n : Nat) :
BitVec.ofNat 1 n = ofBool (decide (n % 2 = 1))
source
theorem BitVec.ofBool_eq_iff_eq {b b' : Bool} :
ofBool b = ofBool b' ↔ b = b'
source
@[simp]
theorem BitVec.not_ofBool {b : Bool} :
~~~ofBool b = ofBool !b
source
@[simp]
theorem BitVec.ofBool_and_ofBool {b b' : Bool} :
ofBool b &&& ofBool b' = ofBool (b && b')
source
@[simp]
theorem BitVec.ofBool_or_ofBool {b b' : Bool} :
ofBool b ||| ofBool b' = ofBool (b || b')
source
@[simp]
theorem BitVec.ofBool_xor_ofBool {b b' : Bool} :
ofBool b ^^^ ofBool b' = ofBool (b ^^ b')
source
@[simp]
theorem BitVec.getLsbD_ofNatLT {n : Nat} (x : Nat) (lt : x < 2 ^ n) (i : Nat) :
(x#'lt).getLsbD i = x.testBit i
source
@[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))
source
theorem BitVec.ofNatLT_eq_ofNat {w n : Nat} (hn : n < 2 ^ w) :
n#'hn = BitVec.ofNat w n
source
@[simp]
theorem BitVec.toFin_ofNat {w : Nat} (x : Nat) :
(BitVec.ofNat w x).toFin = Fin.ofNat (2 ^ w) x
source
@[simp]
theorem BitVec.finMk_toNat {w : Nat} (x : BitVec w) :
⟨x.toNat, ⋯⟩ = x.toFin
source
@[simp]
theorem BitVec.toFin_ofNatLT {w n : Nat} (h : n < 2 ^ w) :
(n#'h).toFin = ⟨n, h⟩
source
@[simp]
theorem BitVec.toFin_ofFin {w : Nat} (n : Fin (2 ^ w)) :
{ toFin := n }.toFin = n
source
@[simp]
theorem BitVec.ofFin_toFin {w : Nat} (x : BitVec w) :
{ toFin := x.toFin } = x
source
@[simp]
theorem BitVec.ofNatLT_finVal {w : Nat} (n : Fin (2 ^ w)) :
(↑n)#'⋯ = { toFin := n }
source
@[simp]
theorem BitVec.ofNatLT_toNat {w : Nat} (x : BitVec w) :
x.toNat#'⋯ = x
source
@[simp]
theorem BitVec.ofNat_finVal {w : Nat} (n : Fin (2 ^ w)) :
BitVec.ofNat w ↑n = { toFin := n }
source
theorem BitVec.getLsbD_ofNat (n x i : Nat) :
(BitVec.ofNat n x).getLsbD i = (decide (i < n) && x.testBit i)
source
@[simp]
theorem BitVec.getLsbD_zero {w i : Nat} :
(0#w).getLsbD i = false
source
@[simp]
theorem BitVec.getElem_zero {i w : Nat} (h : i < w) :
(0#w)[i] = false
source
@[simp]
theorem BitVec.getMsbD_zero {w i : Nat} :
(0#w).getMsbD i = false
source
@[simp]
theorem BitVec.getLsbD_one {w i : Nat} :
(1#w).getLsbD i = (decide (0 < w) && decide (i = 0))
source
@[simp]
theorem BitVec.getElem_one {i w : Nat} (h : i < w) :
(1#w)[i] = decide (i = 0)
source
@[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.

source
@[simp]
theorem BitVec.toNat_mod_cancel {n : Nat} (x : BitVec n) :
x.toNat % 2 ^ n = x.toNat
source
@[simp]
theorem BitVec.toNat_mod_cancel' {n : Nat} {x : BitVec n} :
↑x.toNat % ↑(2 ^ n) = ↑x.toNat
source
@[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
source
@[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
source
@[simp]
theorem BitVec.toNat_mod_cancel_of_lt {n m : Nat} {x : BitVec n} (h : n < m) :
x.toNat % 2 ^ m = x.toNat
source
@[simp]
theorem BitVec.sub_sub_toNat_cancel {w : Nat} {x : BitVec w} :
2 ^ w - (2 ^ w - x.toNat) = x.toNat
source
@[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)
source
theorem BitVec.getElem_zero_ofNat_zero {w : Nat} (i : Nat) (h : i < w) :
(0#w)[i] = false
source
theorem BitVec.getElem_zero_ofNat_one {w : Nat} (h : 0 < w) :
(1#w)[0] = true
source
theorem BitVec.getElem?_zero_ofNat_zero {w : Nat} :
(0#(w + 1))[0]? = some false
source
theorem BitVec.getElem?_zero_ofNat_one {w : Nat} :
(1#(w + 1))[0]? = some true
source
theorem BitVec.getElem?_zero_ofBool (b : Bool) :
(ofBool b)[0]? = some b
source
@[simp]
theorem BitVec.getElem_zero_ofBool (b : Bool) :
(ofBool b)[0] = b
source
theorem BitVec.getElem?_succ_ofBool (b : Bool) (i : Nat) :
(ofBool b)[i + 1]? = none
source
@[simp]
theorem BitVec.getLsbD_ofBool (b : Bool) (i : Nat) :
(ofBool b).getLsbD i = (decide (i = 0) && b)
source
theorem BitVec.getElem_ofBool_zero {b : Bool} :
(ofBool b)[0] = b
source
@[simp]
theorem BitVec.getElem_ofBool {i : Nat} {b : Bool} {h : i < 1} :
(ofBool b)[i] = b
source
@[simp]
theorem BitVec.getMsbD_ofBool {i : Nat} (b : Bool) :
(ofBool b).getMsbD i = (decide (i = 0) && b)
source
@[simp]
theorem BitVec.msb_ofBool (b : Bool) :
(ofBool b).msb = b
source
@[simp]
theorem BitVec.one_eq_zero_iff {w : Nat} :
1#w = 0#w ↔ w = 0
source
@[simp]
theorem BitVec.zero_eq_one_iff (w : Nat) :
0#w = 1#w ↔ w = 0

`0#w = 1#w` iff the width is zero.

source
theorem BitVec.zero_iff_eq_false {w : Nat} {x : BitVec w} :
x = 0#w ↔ ∀ (i : Nat), x.getLsbD i = false

A bitvector is equal to 0#w if and only if all bits are `false`

### msb #

source
@[simp]
theorem BitVec.msb_zero {w : Nat} :
(0#w).msb = false
source
@[simp]
theorem BitVec.msb_one {w : Nat} :
(1#w).msb = decide (w = 1)
source
theorem BitVec.msb_eq_getLsbD_last {w : Nat} (x : BitVec w) :
x.msb = x.getLsbD (w - 1)
source
theorem BitVec.getLsbD_last {w : Nat} (x : BitVec w) :
x.getLsbD (w - 1) = decide (2 ^ (w - 1) ≤ x.toNat)
source
theorem BitVec.getLsbD_succ_last {w : Nat} (x : BitVec (w + 1)) :
x.getLsbD w = decide (2 ^ w ≤ x.toNat)
source
theorem BitVec.msb_eq_decide {w : Nat} (x : BitVec w) :
x.msb = decide (2 ^ (w - 1) ≤ x.toNat)
source
theorem BitVec.toNat_ge_of_msb_true {n : Nat} {x : BitVec n} (p : x.msb = true) :
x.toNat ≥ 2 ^ (n - 1)
source
theorem BitVec.msb_eq_getMsbD_zero {w : Nat} (x : BitVec w) :
x.msb = x.getMsbD 0

### cast #

source
@[simp]
theorem BitVec.toFin_cast {w v : Nat} (h : w = v) (x : BitVec w) :
(BitVec.cast h x).toFin = Fin.cast ⋯ x.toFin
source
@[simp]
theorem BitVec.getLsbD_cast {w v i : Nat} (h : w = v) (x : BitVec w) :
(BitVec.cast h x).getLsbD i = x.getLsbD i
source
@[simp]
theorem BitVec.getMsbD_cast {w v i : Nat} (h : w = v) (x : BitVec w) :
(BitVec.cast h x).getMsbD i = x.getMsbD i
source
@[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]
source
@[simp]
theorem BitVec.msb_cast {w v : Nat} (h : w = v) (x : BitVec w) :
(BitVec.cast h x).msb = x.msb

### toInt/ofInt #

source
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.

source
theorem BitVec.toInt_eq_toNat_of_lt {n : Nat} {x : BitVec n} (h : 2 * x.toNat < 2 ^ n) :
x.toInt = ↑x.toNat
source
theorem BitVec.msb_eq_false_iff_two_mul_lt {w : Nat} {x : BitVec w} :
x.msb = false ↔ 2 * x.toNat < 2 ^ w
source
theorem BitVec.msb_eq_true_iff_two_mul_ge {w : Nat} {x : BitVec w} :
x.msb = true ↔ 2 * x.toNat ≥ 2 ^ w
source
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`.

source
theorem BitVec.toInt_eq_toNat_of_msb {w : Nat} {x : BitVec w} (h : x.msb = false) :
x.toInt = ↑x.toNat
source
theorem BitVec.toNat_toInt_of_msb {w : Nat} (b : BitVec w) (hb : b.msb = false) :
b.toInt.toNat = b.toNat
source
theorem BitVec.toInt_eq_toNat_bmod {n : Nat} (x : BitVec n) :
x.toInt = (↑x.toNat).bmod (2 ^ n)
source
theorem BitVec.toInt_neg_of_msb_true {w : Nat} {x : BitVec w} (h : x.msb = true) :
x.toInt < 0
source
theorem BitVec.toInt_nonneg_of_msb_false {w : Nat} {x : BitVec w} (h : x.msb = false) :
0 ≤ x.toInt
source
@[simp]
theorem BitVec.toInt_one_of_lt {w : Nat} (h : 1 < w) :
(1#w).toInt = 1
source
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 integer operations.

source
theorem BitVec.toInt_inj {n : Nat} {x y : BitVec n} :
x.toInt = y.toInt ↔ x = y
source
theorem BitVec.toInt_ne {n : Nat} {x y : BitVec n} :
x.toInt ≠ y.toInt ↔ x ≠ y
source
@[simp]
theorem BitVec.toNat_ofInt {n : Nat} (i : Int) :
(BitVec.ofInt n i).toNat = (i % ↑(2 ^ n)).toNat
source
theorem BitVec.toInt_ofNat' {n : Nat} (x : Nat) :
(BitVec.ofNat n x).toInt = (↑x).bmod (2 ^ n)
source
theorem BitVec.toInt_ofNat {n : Nat} (x : Nat) :
(OfNat.ofNat x).toInt = (↑x).bmod (2 ^ n)
source
@[simp]
theorem BitVec.toInt_ofFin {w : Nat} (x : Fin (2 ^ w)) :
{ toFin := x }.toInt = (↑↑x).bmod (2 ^ w)
source
@[simp]
theorem BitVec.toInt_ofInt {n : Nat} (i : Int) :
(BitVec.ofInt n i).toInt = i.bmod (2 ^ n)
source
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
source
@[simp]
theorem BitVec.ofInt_natCast (w n : Nat) :
BitVec.ofInt w ↑n = BitVec.ofNat w n
source
@[simp]
theorem BitVec.ofInt_ofNat (w n : Nat) :
BitVec.ofInt w (OfNat.ofNat n) = BitVec.ofNat w (OfNat.ofNat n)
source
theorem BitVec.toInt_neg_iff {w : Nat} {x : BitVec w} :
x.toInt < 0 ↔ 2 ^ w ≤ 2 * x.toNat
source
theorem BitVec.toInt_pos_iff {w : Nat} {x : BitVec w} :
0 ≤ x.toInt ↔ 2 * x.toNat < 2 ^ w
source
theorem BitVec.eq_zero_or_eq_one (a : BitVec 1) :
a = 0#1 ∨ a = 1#1
source
@[simp]
theorem BitVec.toInt_zero {w : Nat} :
(0#w).toInt = 0
source
@[simp]
theorem BitVec.toInt_ofBool (b : Bool) :
(ofBool b).toInt = -b.toInt
source
@[simp]
theorem BitVec.toNat_one {w : Nat} (h : 0 < w) :
(1#w).toNat = 1
source
@[simp]
theorem BitVec.toInt_one {w : Nat} (h : 1 < w) :
(1#w).toInt = 1
source
@[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
source
theorem BitVec.toNat_lt_of_msb_false {w : Nat} {x : BitVec w} (h : x.msb = false) :
x.toNat < 2 ^ (w - 1)
source
theorem BitVec.le_toNat_of_msb_true {w : Nat} {x : BitVec w} (h : x.msb = true) :
2 ^ (w - 1) ≤ x.toNat
source
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.

source
theorem BitVec.two_mul_toInt_le {w : Nat} {x : BitVec w} :
2 * x.toInt ≤ 2 ^ w - 1
source
theorem BitVec.toInt_lt {w : Nat} {x : BitVec w} :
x.toInt < 2 ^ (w - 1)
source
theorem BitVec.toInt_le {w : Nat} {x : BitVec w} :
x.toInt ≤ 2 ^ (w - 1) - 1
source
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.

source
theorem BitVec.le_toInt {w : Nat} (x : BitVec w) :
-2 ^ (w - 1) ≤ x.toInt
source
@[simp]
theorem BitVec.ofInt_toInt {w : Nat} {x : BitVec w} :
BitVec.ofInt w x.toInt = x
source
@[simp]
theorem BitVec.toNat_intCast {w : Nat} (x : Int) :
(↑x).toNat = (x % 2 ^ w).toNat
source
@[simp]
theorem BitVec.toInt_intCast {w : Nat} (x : Int) :
(↑x).toInt = x.bmod (2 ^ w)

### sle/slt #

source
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.

source
theorem BitVec.slt_zero_eq_msb {w : Nat} {x : BitVec w} :
x.slt 0#w = x.msb
source
theorem BitVec.sle_eq_decide {w : Nat} {x y : BitVec w} :
x.sle y = decide (x.toInt ≤ y.toInt)
source
theorem BitVec.slt_eq_decide {w : Nat} {x y : BitVec w} :
x.slt y = decide (x.toInt < y.toInt)
source
theorem BitVec.ule_eq_decide {w : Nat} {x y : BitVec w} :
x.ule y = decide (x.toNat ≤ y.toNat)
source
theorem BitVec.ult_eq_decide {w : Nat} {x y : BitVec w} :
x.ult y = decide (x.toNat < y.toNat)
source
theorem BitVec.ule_eq_decide_le {w : Nat} {x y : BitVec w} :
x.ule y = decide (x ≤ y)
source
theorem BitVec.ult_eq_decide_lt {w : Nat} {x y : BitVec w} :
x.ult y = decide (x < y)
source
theorem BitVec.ule_iff_le {w : Nat} {x y : BitVec w} :
x.ule y = true ↔ x ≤ y
source
theorem BitVec.ult_iff_lt {w : Nat} {x y : BitVec w} :
x.ult y = true ↔ x < y
source
theorem BitVec.sle_iff_toInt_le {w : Nat} {x y : BitVec w} :
x.sle y = true ↔ x.toInt ≤ y.toInt
source
theorem BitVec.slt_iff_toInt_lt {w : Nat} {x y : BitVec w} :
x.slt y = true ↔ x.toInt < y.toInt
source
theorem BitVec.ule_iff_toNat_le {w : Nat} {x y : BitVec w} :
x.ule y = true ↔ x.toNat ≤ y.toNat
source
theorem BitVec.ult_iff_toNat_lt {w : Nat} {x y : BitVec w} :
x.ult y = true ↔ x.toNat < y.toNat
source
theorem BitVec.sle_eq_slt_or_eq {w : Nat} {x y : BitVec w} :
x.sle y = (x.slt y || x == y)
source
theorem BitVec.slt_eq_sle_and_ne {w : Nat} {x y : BitVec w} :
x.slt y = (x.sle y && x != y)
source
theorem BitVec.slt_trichotomy {w : Nat} (x y : BitVec w) :
x.slt y = true ∨ x = y ∨ y.slt x = true

For all bitvectors `x, y`, either `x` is signed less than `y`, or is equal to `y`, or is signed greater than `y`.

source
theorem BitVec.lt_trichotomy {w : Nat} (x y : BitVec w) :
x < y ∨ x = y ∨ y < x

For all bitvectors `x, y`, either `x` is unsigned less than `y`, or is equal to `y`, or is unsigned greater than `y`.

### setWidth, zeroExtend and truncate #

source
@[simp]
theorem BitVec.truncate_eq_setWidth {w v : Nat} {x : BitVec w} :
truncate v x = setWidth v x
source
@[simp]
theorem BitVec.zeroExtend_eq_setWidth {w v : Nat} {x : BitVec w} :
zeroExtend v x = setWidth v x
source
@[simp]
theorem BitVec.toInt_setWidth {w v : Nat} (x : BitVec w) :
(setWidth v x).toInt = (↑x.toNat).bmod (2 ^ v)
source
@[simp]
theorem BitVec.toFin_setWidth {w v : Nat} {x : BitVec w} :
(setWidth v x).toFin = Fin.ofNat (2 ^ v) x.toNat
source
@[simp]
theorem BitVec.setWidth_eq {n : Nat} (x : BitVec n) :
setWidth n x = x
source
@[simp]
theorem BitVec.setWidth_zero (m n : Nat) :
setWidth m 0#n = 0#m
source
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.

source
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.

source
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
source
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
source
@[simp]
theorem BitVec.getLsbD_setWidth' {m n : Nat} (ge : m ≥ n) (x : BitVec n) (i : Nat) :
(setWidth' ge x).getLsbD i = x.getLsbD i
source
@[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))
source
@[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)
source
@[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))
source
@[simp]
theorem BitVec.setWidth'_eq {w v : Nat} {x : BitVec w} (h : w ≤ v) :
setWidth' h x = setWidth v x
source
@[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)
source
@[simp]
theorem BitVec.cast_setWidth {v v' w : Nat} (h : v = v') (x : BitVec w) :
BitVec.cast h (setWidth v x) = setWidth v' x
source
@[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
source
@[simp]
theorem BitVec.setWidth_cast {w v k : Nat} {x : BitVec w} {h : w = v} :
setWidth k (BitVec.cast h x) = setWidth k x
source
theorem BitVec.msb_setWidth {w v : Nat} (x : BitVec w) :
(setWidth v x).msb = (decide (0 < v) && x.getLsbD (v - 1))
source
theorem BitVec.msb_setWidth' {w v : Nat} (x : BitVec w) (h : w ≤ v) :
(setWidth' h x).msb = (decide (0 < v) && x.getLsbD (v - 1))
source
theorem BitVec.msb_setWidth'' {w k : Nat} (x : BitVec w) :
(setWidth (k + 1) x).msb = x.getLsbD k
source
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.

source
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`.

source
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.

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

source
@[simp]
theorem BitVec.msb_setWidth'_of_lt {m n : Nat} (p : m < n) {x : BitVec m} :
(setWidth' ⋯ x).msb = false
source
@[simp]
theorem BitVec.toInt_setWidth'_of_lt {m n : Nat} (p : m < n) {x : BitVec m} :
(setWidth' ⋯ x).toInt = ↑x.toNat
source
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
source
@[simp]
theorem BitVec.toFin_setWidth' {m n : Nat} (p : m ≤ n) (x : BitVec m) :
(setWidth' p x).toFin = Fin.castLE ⋯ x.toFin
source
theorem BitVec.toNat_setWidth_of_le {w w' : Nat} {b : BitVec w} (h : w ≤ w') :
(setWidth w' b).toNat = b.toNat

## extractLsb #

source
@[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)
source
@[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)
source
@[simp]
theorem BitVec.extractLsb'_toNat {n : Nat} (s m : Nat) (x : BitVec n) :
(extractLsb' s m x).toNat = x.toNat >>> s % 2 ^ m
source
@[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)
source
@[simp]
theorem BitVec.toInt_extractLsb' {n s m : Nat} {x : BitVec n} :
(extractLsb' s m x).toInt = (↑(x.toNat >>> s)).bmod (2 ^ m)
source
@[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))
source
@[simp]
theorem BitVec.toFin_extractLsb' {n s m : Nat} {x : BitVec n} :
(extractLsb' s m x).toFin = Fin.ofNat (2 ^ m) (x.toNat >>> s)
source
@[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)
source
@[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)
source
@[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))
source
@[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

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

source
theorem BitVec.getLsbD_eq_extractLsb' {w : Nat} (x : BitVec w) (i : Nat) :
x.getLsbD i = (extractLsb' i 1 x == 1#1)
source
theorem BitVec.getElem_eq_extractLsb' {w : Nat} (x : BitVec w) (i : Nat) (h : i < w) :
x[i] = (extractLsb' i 1 x == 1#1)
source
@[simp]
theorem BitVec.extractLsb'_zero {w start len : Nat} :
extractLsb' start len 0#w = 0#len
source
@[simp]
theorem BitVec.extractLsb'_eq_zero {w : Nat} {x : BitVec w} {start : Nat} :
extractLsb' start 0 x = 0#0
source
theorem BitVec.extractLsb'_setWidth_of_le {w : Nat} {b : BitVec w} {start len w' : Nat} (h : start + len ≤ w') :
extractLsb' start len (setWidth w' b) = extractLsb' start len b
source
theorem BitVec.setWidth_extractLsb'_of_le {w len₁ len₂ start : Nat} {c : BitVec w} (h : len₁ ≤ len₂) :
setWidth len₁ (extractLsb' start len₂ c) = extractLsb' start len₁ c

### allOnes #

source
@[simp]
theorem BitVec.toNat_allOnes {v : Nat} :
(allOnes v).toNat = 2 ^ v - 1
source
@[simp]
theorem BitVec.toInt_allOnes {w : Nat} :
(allOnes w).toInt = if 0 < w then -1 else 0
source
@[simp]
theorem BitVec.toFin_allOnes {w : Nat} :
(allOnes w).toFin = Fin.ofNat (2 ^ w) (2 ^ w - 1)
source
@[simp]
theorem BitVec.getLsbD_allOnes {v i : Nat} :
(allOnes v).getLsbD i = decide (i < v)
source
@[simp]
theorem BitVec.getMsbD_allOnes {v i : Nat} :
(allOnes v).getMsbD i = decide (i < v)
source
@[simp]
theorem BitVec.getElem_allOnes {v : Nat} (i : Nat) (h : i < v) :
(allOnes v)[i] = true
source
@[simp]
theorem BitVec.ofFin_add_rev {n : Nat} (x : Fin (2 ^ n)) :
{ toFin := x + x.rev } = allOnes n
source
theorem BitVec.msb_allOnes {w : Nat} (hw : 0 < w) :
(allOnes w).msb = true

### or #

source
@[simp]
theorem BitVec.toNat_or {v : Nat} (x y : BitVec v) :
(x ||| y).toNat = x.toNat ||| y.toNat
source
@[simp]
theorem BitVec.toInt_or {w : Nat} (x y : BitVec w) :
(x ||| y).toInt = (↑(x.toNat ||| y.toNat)).bmod (2 ^ w)
source
@[simp]
theorem BitVec.toFin_or {v : Nat} (x y : BitVec v) :
(x ||| y).toFin = x.toFin ||| y.toFin
source
@[simp]
theorem BitVec.getLsbD_or {v i : Nat} {x y : BitVec v} :
(x ||| y).getLsbD i = (x.getLsbD i || y.getLsbD i)
source
@[simp]
theorem BitVec.getMsbD_or {w i : Nat} {x y : BitVec w} :
(x ||| y).getMsbD i = (x.getMsbD i || y.getMsbD i)
source
@[simp]
theorem BitVec.getElem_or {w : Nat} {x y : BitVec w} {i : Nat} (h : i < w) :
(x ||| y)[i] = (x[i] || y[i])
source
@[simp]
theorem BitVec.msb_or {w : Nat} {x y : BitVec w} :
(x ||| y).msb = (x.msb || y.msb)
source
@[simp]
theorem BitVec.setWidth_or {w k : Nat} {x y : BitVec w} :
setWidth k (x ||| y) = setWidth k x ||| setWidth k y
source
theorem BitVec.or_assoc {w : Nat} (x y z : BitVec w) :
x ||| y ||| z = x ||| (y ||| z)
source
instance BitVec.instAssociativeHOr {n : Nat} :
Std.Associative fun (x1 x2 : BitVec n) => x1 ||| x2
source
theorem BitVec.or_comm {w : Nat} (x y : BitVec w) :
x ||| y = y ||| x
source
instance BitVec.instCommutativeHOr {w : Nat} :
Std.Commutative fun (x y : BitVec w) => x ||| y
source
@[simp]
theorem BitVec.or_self {w : Nat} {x : BitVec w} :
x ||| x = x
source
instance BitVec.instIdempotentOpHOr {n : Nat} :
Std.IdempotentOp fun (x1 x2 : BitVec n) => x1 ||| x2
source
@[simp]
theorem BitVec.or_zero {w : Nat} {x : BitVec w} :
x ||| 0#w = x
source
instance BitVec.instLawfulCommIdentityHOrOfNatOfNatNat {n : Nat} :
Std.LawfulCommIdentity (fun (x1 x2 : BitVec n) => x1 ||| x2) 0#n
source
@[simp]
theorem BitVec.zero_or {w : Nat} {x : BitVec w} :
0#w ||| x = x
source
@[simp]
theorem BitVec.or_allOnes {w : Nat} {x : BitVec w} :
x ||| allOnes w = allOnes w
source
@[simp]
theorem BitVec.allOnes_or {w : Nat} {x : BitVec w} :
allOnes w ||| x = allOnes w
source
@[simp]
theorem BitVec.or_eq_zero_iff {w : Nat} {x y : BitVec w} :
x ||| y = 0#w ↔ x = 0#w ∧ y = 0#w
source
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
source
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
source
@[simp]
theorem BitVec.ofNat_or {w x y : Nat} :
BitVec.ofNat w (x ||| y) = BitVec.ofNat w x ||| BitVec.ofNat w y

### and #

source
@[simp]
theorem BitVec.toNat_and {v : Nat} (x y : BitVec v) :
(x &&& y).toNat = x.toNat &&& y.toNat
source
@[simp]
theorem BitVec.toInt_and {w : Nat} (x y : BitVec w) :
(x &&& y).toInt = (↑(x.toNat &&& y.toNat)).bmod (2 ^ w)
source
@[simp]
theorem BitVec.toFin_and {v : Nat} (x y : BitVec v) :
(x &&& y).toFin = x.toFin &&& y.toFin
source
@[simp]
theorem BitVec.getLsbD_and {v i : Nat} {x y : BitVec v} :
(x &&& y).getLsbD i = (x.getLsbD i && y.getLsbD i)
source
@[simp]
theorem BitVec.getMsbD_and {w i : Nat} {x y : BitVec w} :
(x &&& y).getMsbD i = (x.getMsbD i && y.getMsbD i)
source
@[simp]
theorem BitVec.getElem_and {w : Nat} {x y : BitVec w} {i : Nat} (h : i < w) :
(x &&& y)[i] = (x[i] && y[i])
source
@[simp]
theorem BitVec.msb_and {w : Nat} {x y : BitVec w} :
(x &&& y).msb = (x.msb && y.msb)
source
@[simp]
theorem BitVec.setWidth_and {w k : Nat} {x y : BitVec w} :
setWidth k (x &&& y) = setWidth k x &&& setWidth k y
source
theorem BitVec.and_assoc {w : Nat} (x y z : BitVec w) :
x &&& y &&& z = x &&& (y &&& z)
source
instance BitVec.instAssociativeHAnd {n : Nat} :
Std.Associative fun (x1 x2 : BitVec n) => x1 &&& x2
source
theorem BitVec.and_comm {w : Nat} (x y : BitVec w) :
x &&& y = y &&& x
source
instance BitVec.instCommutativeHAnd {w : Nat} :
Std.Commutative fun (x y : BitVec w) => x &&& y
source
@[simp]
theorem BitVec.and_self {w : Nat} {x : BitVec w} :
x &&& x = x
source
instance BitVec.instIdempotentOpHAnd {n : Nat} :
Std.IdempotentOp fun (x1 x2 : BitVec n) => x1 &&& x2
source
@[simp]
theorem BitVec.and_zero {w : Nat} {x : BitVec w} :
x &&& 0#w = 0#w
source
@[simp]
theorem BitVec.zero_and {w : Nat} {x : BitVec w} :
0#w &&& x = 0#w
source
@[simp]
theorem BitVec.and_allOnes {w : Nat} {x : BitVec w} :
x &&& allOnes w = x
source
instance BitVec.instLawfulCommIdentityHAndAllOnes {n : Nat} :
Std.LawfulCommIdentity (fun (x1 x2 : BitVec n) => x1 &&& x2) (allOnes n)
source
@[simp]
theorem BitVec.allOnes_and {w : Nat} {x : BitVec w} :
allOnes w &&& x = x
source
@[simp]
theorem BitVec.and_eq_allOnes_iff {w : Nat} {x y : BitVec w} :
x &&& y = allOnes w ↔ x = allOnes w ∧ y = allOnes w
source
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
source
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
source
@[simp]
theorem BitVec.ofNat_and {w x y : Nat} :
BitVec.ofNat w (x &&& y) = BitVec.ofNat w x &&& BitVec.ofNat w y
source
theorem BitVec.and_or_distrib_left {w : Nat} {x y z : BitVec w} :
x &&& (y ||| z) = x &&& y ||| x &&& z
source
theorem BitVec.and_or_distrib_right {w : Nat} {x y z : BitVec w} :
(x ||| y) &&& z = x &&& z ||| y &&& z

### xor #

source
@[simp]
theorem BitVec.toNat_xor {v : Nat} (x y : BitVec v) :
(x ^^^ y).toNat = x.toNat ^^^ y.toNat
source
@[simp]
theorem BitVec.toInt_xor {w : Nat} (x y : BitVec w) :
(x ^^^ y).toInt = (↑(x.toNat ^^^ y.toNat)).bmod (2 ^ w)
source
@[simp]
theorem BitVec.toFin_xor {v : Nat} (x y : BitVec v) :
(x ^^^ y).toFin = x.toFin ^^^ y.toFin
source
@[simp]
theorem BitVec.getLsbD_xor {v i : Nat} {x y : BitVec v} :
(x ^^^ y).getLsbD i = (x.getLsbD i ^^ y.getLsbD i)
source
@[simp]
theorem BitVec.getMsbD_xor {w i : Nat} {x y : BitVec w} :
(x ^^^ y).getMsbD i = (x.getMsbD i ^^ y.getMsbD i)
source
@[simp]
theorem BitVec.getElem_xor {w : Nat} {x y : BitVec w} {i : Nat} (h : i < w) :
(x ^^^ y)[i] = (x[i] ^^ y[i])
source
@[simp]
theorem BitVec.msb_xor {w : Nat} {x y : BitVec w} :
(x ^^^ y).msb = (x.msb ^^ y.msb)
source
@[simp]
theorem BitVec.setWidth_xor {w k : Nat} {x y : BitVec w} :
setWidth k (x ^^^ y) = setWidth k x ^^^ setWidth k y
source
theorem BitVec.xor_assoc {w : Nat} (x y z : BitVec w) :
x ^^^ y ^^^ z = x ^^^ (y ^^^ z)
source
instance BitVec.instAssociativeHXor {w : Nat} :
Std.Associative fun (x y : BitVec w) => x ^^^ y
source
theorem BitVec.xor_comm {w : Nat} (x y : BitVec w) :
x ^^^ y = y ^^^ x
source
instance BitVec.instCommutativeHXor {w : Nat} :
Std.Commutative fun (x y : BitVec w) => x ^^^ y
source
@[simp]
theorem BitVec.xor_self {w : Nat} {x : BitVec w} :
x ^^^ x = 0#w
source
@[simp]
theorem BitVec.xor_zero {w : Nat} {x : BitVec w} :
x ^^^ 0#w = x
source
instance BitVec.instLawfulCommIdentityHXorOfNatOfNatNat {n : Nat} :
Std.LawfulCommIdentity (fun (x1 x2 : BitVec n) => x1 ^^^ x2) 0#n
source
@[simp]
theorem BitVec.zero_xor {w : Nat} {x : BitVec w} :
0#w ^^^ x = x
source
@[simp]
theorem BitVec.xor_left_inj {w : Nat} {x y : BitVec w} (z : BitVec w) :
x ^^^ z = y ^^^ z ↔ x = y
source
@[simp]
theorem BitVec.xor_right_inj {w : Nat} {x y : BitVec w} (z : BitVec w) :
z ^^^ x = z ^^^ y ↔ x = y
source
@[simp]
theorem BitVec.xor_eq_zero_iff {w : Nat} {x y : BitVec w} :
x ^^^ y = 0#w ↔ x = y
source
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
source
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
source
@[simp]
theorem BitVec.ofNat_xor {w x y : Nat} :
BitVec.ofNat w (x ^^^ y) = BitVec.ofNat w x ^^^ BitVec.ofNat w y

### not #

source
theorem BitVec.not_def {v : Nat} {x : BitVec v} :
~~~x = allOnes v ^^^ x
source
@[simp]
theorem BitVec.toNat_not {v : Nat} {x : BitVec v} :
(~~~x).toNat = 2 ^ v - 1 - x.toNat
source
@[simp]
theorem BitVec.toInt_not {w : Nat} {x : BitVec w} :
(~~~x).toInt = (2 ^ w - 1 - ↑x.toNat).bmod (2 ^ w)
source
@[simp]
theorem BitVec.ofInt_negSucc_eq_not_ofNat {w n : Nat} :
BitVec.ofInt w (Int.negSucc n) = ~~~BitVec.ofNat w n
source
@[simp]
theorem BitVec.toFin_not {w : Nat} (x : BitVec w) :
(~~~x).toFin = x.toFin.rev
source
@[simp]
theorem BitVec.getLsbD_not {v i : Nat} {x : BitVec v} :
(~~~x).getLsbD i = (decide (i < v) && !x.getLsbD i)
source
@[simp]
theorem BitVec.getMsbD_not {v i : Nat} {x : BitVec v} :
(~~~x).getMsbD i = (decide (i < v) && !x.getMsbD i)
source
@[simp]
theorem BitVec.getElem_not {w : Nat} {x : BitVec w} {i : Nat} (h : i < w) :
(~~~x)[i] = !x[i]
source
@[simp]
theorem BitVec.setWidth_not {w k : Nat} {x : BitVec w} :
k ≤ w → setWidth k (~~~x) = ~~~setWidth k x
source
@[simp]
theorem BitVec.not_zero {n : Nat} :
~~~0#n = allOnes n
source
@[simp]
theorem BitVec.not_allOnes {w : Nat} :
~~~allOnes w = 0#w
source
@[simp]
theorem BitVec.xor_allOnes {w : Nat} {x : BitVec w} :
x ^^^ allOnes w = ~~~x
source
@[simp]
theorem BitVec.allOnes_xor {w : Nat} {x : BitVec w} :
allOnes w ^^^ x = ~~~x
source
@[simp]
theorem BitVec.not_not {w : Nat} {b : BitVec w} :
~~~~~~b = b
source
@[simp]
theorem BitVec.not_inj {w : Nat} {x y : BitVec w} :
~~~x = ~~~y ↔ x = y
source
@[simp]
theorem BitVec.and_not_self {w : Nat} (x : BitVec w) :
x &&& ~~~x = 0
source
@[simp]
theorem BitVec.not_and_self {w : Nat} (x : BitVec w) :
~~~x &&& x = 0
source
@[simp]
theorem BitVec.or_not_self {w : Nat} (x : BitVec w) :
x ||| ~~~x = allOnes w
source
@[simp]
theorem BitVec.not_or_self {w : Nat} (x : BitVec w) :
~~~x ||| x = allOnes w
source
theorem BitVec.not_eq_comm {w : Nat} {x y : BitVec w} :
~~~x = y ↔ x = ~~~y
source
@[reducible, inline, deprecated BitVec.getMsbD_not (since := "2025-04-04")]
abbrev BitVec.getMsb_not {v i : Nat} {x : BitVec v} :
(~~~x).getMsbD i = (decide (i < v) && !x.getMsbD i)
Equations

- @BitVec.getMsb_not = @BitVec.getMsbD_not

Instances For

source
@[simp]
theorem BitVec.msb_not {w : Nat} {x : BitVec w} :
(~~~x).msb = (decide (0 < w) && !x.msb)
source
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.

source
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.

source
@[simp]
theorem BitVec.ne_not_self {w : Nat} {a : BitVec w} (h : 0 < w) :
a ≠ ~~~a
source
@[simp]
theorem BitVec.not_self_ne {w : Nat} {a : BitVec w} (h : 0 < w) :
~~~a ≠ a
source
theorem BitVec.not_and {w : Nat} {x y : BitVec w} :
~~~(x &&& y) = ~~~x ||| ~~~y
source
theorem BitVec.not_or {w : Nat} {x y : BitVec w} :
~~~(x ||| y) = ~~~x &&& ~~~y
source
theorem BitVec.not_xor_left {w : Nat} {x y : BitVec w} :
~~~(x ^^^ y) = ~~~x ^^^ y
source
theorem BitVec.not_xor_right {w : Nat} {x y : BitVec w} :
~~~(x ^^^ y) = x ^^^ ~~~y

### cast #

source
@[simp]
theorem BitVec.not_cast {w w' : Nat} {x : BitVec w} (h : w = w') :
~~~BitVec.cast h x = BitVec.cast h (~~~x)
source
@[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)
source
@[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)
source
@[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 #

source
@[simp]
theorem BitVec.toNat_shiftLeft {v n : Nat} {x : BitVec v} :
(x <<< n).toNat = x.toNat <<< n % 2 ^ v
source
@[simp]
theorem BitVec.toInt_shiftLeft {w n : Nat} {x : BitVec w} :
(x <<< n).toInt = (↑(x.toNat <<< n)).bmod (2 ^ w)
source
@[simp]
theorem BitVec.toFin_shiftLeft {w n : Nat} (x : BitVec w) :
(x <<< n).toFin = Fin.ofNat (2 ^ w) (x.toNat <<< n)
source
@[simp]
theorem BitVec.shiftLeft_zero {w : Nat} (x : BitVec w) :
x <<< 0 = x
source
@[simp]
theorem BitVec.zero_shiftLeft {w : Nat} (n : Nat) :
0#w <<< n = 0#w
source
@[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))
source
@[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])
source
theorem BitVec.shiftLeft_xor_distrib {w : Nat} (x y : BitVec w) (n : Nat) :
(x ^^^ y) <<< n = x <<< n ^^^ y <<< n
source
theorem BitVec.shiftLeft_and_distrib {w : Nat} (x y : BitVec w) (n : Nat) :
(x &&& y) <<< n = x <<< n &&& y <<< n
source
theorem BitVec.shiftLeft_or_distrib {w : Nat} (x y : BitVec w) (n : Nat) :
(x ||| y) <<< n = x <<< n ||| y <<< n
source
@[simp]
theorem BitVec.getMsbD_shiftLeft {w k : Nat} (x : BitVec w) (i : Nat) :
(x <<< i).getMsbD k = x.getMsbD (k + i)
source
theorem BitVec.shiftLeftZeroExtend_eq {w n : Nat} {x : BitVec w} :
x.shiftLeftZeroExtend n = setWidth (w + n) x <<< n
source
@[simp]
theorem BitVec.toNat_shiftLeftZeroExtend {w n : Nat} {x : BitVec w} :
(x.shiftLeftZeroExtend n).toNat = x.toNat <<< n
source
@[simp]
theorem BitVec.toInt_shiftLeftZeroExtend {w n : Nat} {x : BitVec w} :
(x.shiftLeftZeroExtend n).toInt = x.toInt * 2 ^ n
source
theorem BitVec.toFin_shiftLeftZeroExtend {w n : Nat} {x : BitVec w} :
(x.shiftLeftZeroExtend n).toFin = Fin.ofNat (2 ^ (w + n)) (x.toNat * 2 ^ n)
source
@[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]
source
@[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))
source
@[simp]
theorem BitVec.getMsbD_shiftLeftZeroExtend {m i : Nat} (x : BitVec m) (n : Nat) :
(x.shiftLeftZeroExtend n).getMsbD i = x.getMsbD i
source
@[simp]
theorem BitVec.msb_shiftLeftZeroExtend {w : Nat} (x : BitVec w) (i : Nat) :
(x.shiftLeftZeroExtend i).msb = x.msb
source
theorem BitVec.shiftLeft_add {w : Nat} (x : BitVec w) (n m : Nat) :
x <<< (n + m) = x <<< n <<< m
source
@[simp]
theorem BitVec.allOnes_shiftLeft_and_shiftLeft {w : Nat} {x : BitVec w} {n : Nat} :
allOnes w <<< n &&& x <<< n = x <<< n
source
@[simp]
theorem BitVec.allOnes_shiftLeft_or_shiftLeft {w : Nat} {x : BitVec w} {n : Nat} :
allOnes w <<< n ||| x <<< n = allOnes w <<< n
source
@[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 #

source
@[simp]
theorem BitVec.shiftLeft_eq' {w₁ w₂ : Nat} {x : BitVec w₁} {y : BitVec w₂} :
x <<< y = x <<< y.toNat
source
theorem BitVec.shiftLeft_zero' {w₁ w₂ : Nat} {x : BitVec w₁} :
x <<< 0#w₂ = x
source
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)
source
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))
source
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])
source
@[simp]
theorem BitVec.shiftLeft_eq_zero {w : Nat} {x : BitVec w} {n : Nat} (hn : w ≤ n) :
x <<< n = 0#w
source
theorem BitVec.shiftLeft_ofNat_eq {w : Nat} {x : BitVec w} {k : Nat} :
x <<< BitVec.ofNat w k = x <<< (k % 2 ^ w)

### ushiftRight #

source
@[simp]
theorem BitVec.toNat_ushiftRight {n : Nat} (x : BitVec n) (i : Nat) :
(x >>> i).toNat = x.toNat >>> i
source
@[simp]
theorem BitVec.getLsbD_ushiftRight {n : Nat} (x : BitVec n) (i j : Nat) :
(x >>> i).getLsbD j = x.getLsbD (i + j)
source
@[simp]
theorem BitVec.getElem_ushiftRight {w : Nat} (x : BitVec w) (i n : Nat) (h : i < w) :
(x >>> n)[i] = x.getLsbD (n + i)
source
theorem BitVec.ushiftRight_xor_distrib {w : Nat} (x y : BitVec w) (n : Nat) :
(x ^^^ y) >>> n = x >>> n ^^^ y >>> n
source
theorem BitVec.ushiftRight_and_distrib {w : Nat} (x y : BitVec w) (n : Nat) :
(x &&& y) >>> n = x >>> n &&& y >>> n
source
theorem BitVec.ushiftRight_or_distrib {w : Nat} (x y : BitVec w) (n : Nat) :
(x ||| y) >>> n = x >>> n ||| y >>> n
source
@[simp]
theorem BitVec.ushiftRight_zero {w : Nat} (x : BitVec w) :
x >>> 0 = x
source
@[simp]
theorem BitVec.zero_ushiftRight {w n : Nat} :
0#w >>> n = 0#w
source
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)`.

source
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.

source
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)`.

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

source
@[simp]
theorem BitVec.toFin_ushiftRight {w : Nat} {x : BitVec w} {n : Nat} :
(x >>> n).toFin = x.toFin / Fin.ofNat (2 ^ w) (2 ^ n)
source
@[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)))
source
@[simp]
theorem BitVec.msb_ushiftRight {w : Nat} {x : BitVec w} {n : Nat} :
(x >>> n).msb = (!decide (0 < n) && x.msb)
source
@[simp]
theorem BitVec.setWidth_ushiftRight {w i : Nat} {x : BitVec w} {y : Nat} (hi : w ≤ i) :
setWidth i (x >>> y) = setWidth i x >>> y
source
theorem BitVec.setWidth_ushiftRight_eq_extractLsb {w w' w'' : Nat} {b : BitVec w} :
setWidth w'' (b >>> w') = extractLsb' w' w'' b

### ushiftRight reductions from BitVec to Nat #

source
@[simp]
theorem BitVec.ushiftRight_eq' {w₁ w₂ : Nat} (x : BitVec w₁) (y : BitVec w₂) :
x >>> y = x >>> y.toNat
source
theorem BitVec.ushiftRight_ofNat_eq {w : Nat} {x : BitVec w} {k : Nat} :
x >>> BitVec.ofNat w k = x >>> (k % 2 ^ w)
source
@[simp]
theorem BitVec.ushiftRight_self {w : Nat} (n : BitVec w) :
n >>> n.toNat = 0#w

### sshiftRight #

source
theorem BitVec.sshiftRight_eq {n : Nat} {x : BitVec n} {i : Nat} :
x.sshiftRight i = BitVec.ofInt n (x.toInt >>> i)
source
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

source
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'.

source
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)
source
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
source
theorem BitVec.sshiftRight_xor_distrib {w : Nat} (x y : BitVec w) (n : Nat) :
(x ^^^ y).sshiftRight n = x.sshiftRight n ^^^ y.sshiftRight n
source
theorem BitVec.sshiftRight_and_distrib {w : Nat} (x y : BitVec w) (n : Nat) :
(x &&& y).sshiftRight n = x.sshiftRight n &&& y.sshiftRight n
source
theorem BitVec.sshiftRight_or_distrib {w : Nat} (x y : BitVec w) (n : Nat) :
(x ||| y).sshiftRight n = x.sshiftRight n ||| y.sshiftRight n
source
theorem BitVec.sshiftRight'_ofNat_eq_sshiftRight {w : Nat} {x : BitVec w} {k : Nat} :
x.sshiftRight' (BitVec.ofNat w k) = x.sshiftRight (k % 2 ^ w)
source
@[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.

source
@[simp]
theorem BitVec.sshiftRight_zero {w : Nat} {x : BitVec w} :
x.sshiftRight 0 = x
source
@[simp]
theorem BitVec.zero_sshiftRight {w n : Nat} :
(0#w).sshiftRight n = 0#w
source
theorem BitVec.sshiftRight_add {w : Nat} {x : BitVec w} {m n : Nat} :
x.sshiftRight (m + n) = (x.sshiftRight m).sshiftRight n
source
theorem BitVec.not_sshiftRight {w n : Nat} {b : BitVec w} :
~~~b.sshiftRight n = (~~~b).sshiftRight n
source
@[simp]
theorem BitVec.not_sshiftRight_not {w : Nat} {x : BitVec w} {n : Nat} :
~~~(~~~x).sshiftRight n = x.sshiftRight n
source
@[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))
source
theorem BitVec.toInt_shiftRight_lt {w : Nat} {x : BitVec w} {n : Nat} :
x.toInt >>> n < 2 ^ (w - 1)
source
theorem BitVec.le_toInt_shiftRight {w : Nat} {x : BitVec w} {n : Nat} :
-2 ^ (w - 1) ≤ x.toInt >>> n
source
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
source
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
source
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
source
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)
source
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)
source
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)
source
@[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 #

source
@[simp]
theorem BitVec.sshiftRight_eq' {w w✝ : Nat} {y : BitVec w✝} (x : BitVec w) :
x.sshiftRight' y = x.sshiftRight y.toNat
source
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
source
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
source
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
source
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)
source
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)
source
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)
source
theorem BitVec.toInt_sshiftRight' {w : Nat} {x y : BitVec w} :
(x.sshiftRight' y).toInt = x.toInt >>> y.toNat
source
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)
source
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
source
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))
source
theorem BitVec.msb_sshiftRight' {w : Nat} {x y : BitVec w} :
(x.sshiftRight' y).msb = x.msb

### signExtend #

source
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`.

source
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.

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

source
@[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
source
@[simp]
theorem BitVec.signExtend_eq {w : Nat} (x : BitVec w) :
signExtend w x = x

Sign extending to the same bitwidth is a no op.

source
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.

source
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.

source
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`.

source
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`.

source
theorem BitVec.toInt_signExtend {w v : Nat} (x : BitVec w) :
(signExtend v x).toInt = x.toInt.bmod (2 ^ min v w)
source
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)
source
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
source
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)
source
@[simp]
theorem BitVec.signExtend_and {w v : Nat} {x y : BitVec w} :
signExtend v (x &&& y) = signExtend v x &&& signExtend v y
source
@[simp]
theorem BitVec.signExtend_or {w v : Nat} {x y : BitVec w} :
signExtend v (x ||| y) = signExtend v x ||| signExtend v y
source
@[simp]
theorem BitVec.signExtend_xor {w v : Nat} {x y : BitVec w} :
signExtend v (x ^^^ y) = signExtend v x ^^^ signExtend v y
source
@[simp]
theorem BitVec.signExtend_not {w v : Nat} {x : BitVec w} (h : 0 < w) :
signExtend v (~~~x) = ~~~signExtend v x

### append #

source
theorem BitVec.append_def {v w : Nat} (x : BitVec v) (y : BitVec w) :
x ++ y = x.shiftLeftZeroExtend w ||| setWidth' ⋯ y
source
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)
source
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]
source
@[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
source
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
source
@[simp]
theorem BitVec.append_zero_width {w : Nat} (x : BitVec w) (y : BitVec 0) :
x ++ y = x
source
theorem BitVec.toInt_append {n m : Nat} {x : BitVec n} {y : BitVec m} :
(x ++ y).toInt = if (n == 0) = true then y.toInt else 2 ^ m * x.toInt + ↑y.toNat
source
@[simp]
theorem BitVec.toInt_append_zero {n m : Nat} {x : BitVec n} :
(x ++ 0#m).toInt = 2 ^ m * x.toInt
source
@[simp]
theorem BitVec.toInt_zero_append {n m : Nat} {x : BitVec n} :
(0#m ++ x).toInt = if m = 0 then x.toInt else ↑x.toNat
source
theorem BitVec.toNat_shiftLeft_or_toNat_lt_two_pow_add {m n : Nat} (x : BitVec m) (y : BitVec n) :
x.toNat <<< n ||| y.toNat < 2 ^ (m + n)

Show that `(x.toNat <<< n) ||| y.toNat` is within bounds of `BitVec (m + n)`.

source
@[simp]
theorem BitVec.toFin_append {m n : Nat} {x : BitVec m} {y : BitVec n} :
(x ++ y).toFin = ⟨x.toNat <<< n ||| y.toNat, ⋯⟩
source
@[simp]
theorem BitVec.zero_width_append {v : Nat} (x : BitVec 0) (y : BitVec v) :
x ++ y = BitVec.cast ⋯ y
source
@[simp]
theorem BitVec.zero_append_zero {v w : Nat} :
0#v ++ 0#w = 0#(v + w)
source
@[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
source
@[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
source
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)
source
@[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
source
@[simp]
theorem BitVec.setWidth_cons {w : Nat} {a : Bool} {x : BitVec w} :
setWidth w (cons a x) = x
source
@[simp]
theorem BitVec.not_append {w v : Nat} {x : BitVec w} {y : BitVec v} :
~~~(x ++ y) = ~~~x ++ ~~~y
source
@[simp]
theorem BitVec.and_append {w v : Nat} {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} :
x₁ ++ y₁ &&& x₂ ++ y₂ = (x₁ &&& x₂) ++ (y₁ &&& y₂)
source
@[simp]
theorem BitVec.or_append {w v : Nat} {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} :
x₁ ++ y₁ ||| x₂ ++ y₂ = (x₁ ||| x₂) ++ (y₁ ||| y₂)
source
@[simp]
theorem BitVec.xor_append {w v : Nat} {x₁ x₂ : BitVec w} {y₁ y₂ : BitVec v} :
x₁ ++ y₁ ^^^ x₂ ++ y₂ = (x₁ ^^^ x₂) ++ (y₁ ^^^ y₂)
source
theorem BitVec.shiftRight_add {w : Nat} (x : BitVec w) (n m : Nat) :
x >>> (n + m) = x >>> n >>> m
source
theorem BitVec.shiftLeft_ushiftRight {w : Nat} {x : BitVec w} {n : Nat} :
x >>> n <<< n = x &&& allOnes w <<< n
source
@[simp]
theorem BitVec.msb_shiftLeft {w : Nat} {x : BitVec w} {n : Nat} :
(x <<< n).msb = x.getMsbD n
source
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`

source
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`.

source
theorem BitVec.setWidth_eq_extractLsb' {v : Nat} {x : BitVec v} {w : Nat} (h : w ≤ v) :
setWidth w x = extractLsb' 0 w x
source
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)
source
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)
source
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 = extractLsb' start₁ (len₂ + len₁) x

Combine adjacent `extractLsb'` operations into a single `extractLsb'`.

source
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 _)'`.

source
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`.

source
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`.

source
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. Diagrammatically:

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

source
theorem BitVec.extractLsb'_append_eq_of_add_le {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`.

source
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`.

source
theorem BitVec.extractLsb'_append_eq_left {w w' : Nat} {a : BitVec w} {b : BitVec w'} :
extractLsb' w' w (a ++ b) = a
source
theorem BitVec.extractLsb'_append_eq_right {w w' : Nat} {a : BitVec w} {b : BitVec w'} :
extractLsb' 0 w' (a ++ b) = b
source
theorem BitVec.setWidth_append_eq_right {w w' : Nat} {a : BitVec w} {b : BitVec w'} :
setWidth w' (a ++ b) = b
source
theorem BitVec.append_left_inj {w w' : Nat} {s₁ s₂ : BitVec w} (t : BitVec w') :
s₁ ++ t = s₂ ++ t ↔ s₁ = s₂
source
theorem BitVec.append_right_inj {w w' : Nat} (s : BitVec w) {t₁ t₂ : BitVec w'} :
s ++ t₁ = s ++ t₂ ↔ t₁ = t₂
source
theorem BitVec.setWidth_append_eq_shiftLeft_setWidth_or {w w' w'' : Nat} {b : BitVec w} {b' : BitVec w'} :
setWidth w'' (b ++ b') = setWidth w'' b <<< w' ||| setWidth w'' b'
source
theorem BitVec.setWidth_append_append_eq_shiftLeft_setWidth_or {w w' w'' w''' : Nat} {b : BitVec w} {b' : BitVec w'} {b'' : BitVec w''} :
setWidth w''' (b ++ b' ++ b'') = setWidth w''' b <<< (w' + w'') ||| setWidth w''' b' <<< w'' ||| setWidth w''' b''
source
theorem BitVec.setWidth_append_append_append_eq_shiftLeft_setWidth_or {w w' w'' w''' w'''' : Nat} {b : BitVec w} {b' : BitVec w'} {b'' : BitVec w''} {b''' : BitVec w'''} :
setWidth w'''' (b ++ b' ++ b'' ++ b''') = setWidth w'''' b <<< (w' + w'' + w''') ||| setWidth w'''' b' <<< (w'' + w''') ||| setWidth w'''' b'' <<< w''' ||| setWidth w'''' b'''
source
theorem BitVec.and_setWidth_allOnes (w' w : Nat) (b : BitVec (w' + w)) :
b &&& setWidth (w' + w) (allOnes w) = 0#w' ++ setWidth w b

### rev #

source
theorem BitVec.getLsbD_rev {w : Nat} (x : BitVec w) (i : Fin w) :
x.getLsbD ↑i.rev = x.getMsbD ↑i
source
theorem BitVec.getElem_rev {w : Nat} {x : BitVec w} {i : Fin w} :
x[i.rev] = x.getMsbD ↑i
source
theorem BitVec.getMsbD_rev {w : Nat} (x : BitVec w) (i : Fin w) :
x.getMsbD ↑i.rev = x.getLsbD ↑i

### cons #

source
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 `|||`.

source
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
source
@[simp]
theorem BitVec.msb_cons {a : Bool} {w✝ : Nat} {x : BitVec w✝} :
(cons a x).msb = a
source
@[simp]
theorem BitVec.getMsbD_cons_zero {a : Bool} {w✝ : Nat} {x : BitVec w✝} :
(cons a x).getMsbD 0 = a
source
@[simp]
theorem BitVec.getMsbD_cons_succ {a : Bool} {w✝ : Nat} {x : BitVec w✝} {i : Nat} :
(cons a x).getMsbD (i + 1) = x.getMsbD i
source
theorem BitVec.setWidth_succ {w i : Nat} (x : BitVec w) :
setWidth (i + 1) x = cons (x.getLsbD i) (setWidth i x)
source
@[simp]
theorem BitVec.not_cons {w : Nat} (x : BitVec w) (b : Bool) :
~~~cons b x = cons (!b) (~~~x)
source
@[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)
source
@[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)
source
@[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)
source
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))
source
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 #

source
@[simp]
theorem BitVec.toNat_concat {w : Nat} (x : BitVec w) (b : Bool) :
(x.concat b).toNat = x.toNat * 2 + b.toNat
source
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)
source
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]
source
@[simp]
theorem BitVec.getElem_concat_zero {w : Nat} {b : Bool} {x : BitVec w} :
(x.concat b)[0] = b
source
theorem BitVec.getLsbD_concat_zero {w✝ : Nat} {x : BitVec w✝} {b : Bool} :
(x.concat b).getLsbD 0 = b
source
@[simp]
theorem BitVec.getLsbD_concat_succ {w✝ : Nat} {x : BitVec w✝} {b : Bool} {i : Nat} :
(x.concat b).getLsbD (i + 1) = x.getLsbD i
source
@[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]
source
@[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
source
@[simp]
theorem BitVec.msb_concat {w : Nat} {b : Bool} {x : BitVec w} :
(x.concat b).msb = if 0 < w then x.msb else b
source
@[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
source
@[simp]
theorem BitVec.toFin_concat {w : Nat} (x : BitVec w) (b : Bool) :
(x.concat b).toFin = ⟨x.toNat * 2 + b.toNat, ⋯⟩
source
@[simp]
theorem BitVec.not_concat {w : Nat} (x : BitVec w) (b : Bool) :
~~~x.concat b = (~~~x).concat !b
source
@[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)
source
@[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)
source
@[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)
source
@[simp]
theorem BitVec.zero_concat_false {w : Nat} :
(0#w).concat false = 0#(w + 1)

### shiftConcat #

source
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))
source
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]
source
@[simp]
theorem BitVec.getElem_shiftConcat_zero {w : Nat} {x : BitVec w} (b : Bool) (h : 0 < w) :
(x.shiftConcat b)[0] = b
source
@[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]
source
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)))
source
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))
source
@[simp]
theorem BitVec.toNat_shiftConcat {w : Nat} {x : BitVec w} {b : Bool} :
(x.shiftConcat b).toNat = (x.toNat <<< 1 + b.toNat) % 2 ^ w
source
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`.

source
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 #

source
theorem BitVec.add_def {n : Nat} (x y : BitVec n) :
x + y = BitVec.ofNat n (x.toNat + y.toNat)
source
@[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.

source
@[simp]
theorem BitVec.toFin_add {w : Nat} (x y : BitVec w) :
(x + y).toFin = x.toFin + y.toFin
source
@[simp]
theorem BitVec.ofFin_add {n : Nat} (x : Fin (2 ^ n)) (y : BitVec n) :
{ toFin := x } + y = { toFin := x + y.toFin }
source
@[simp]
theorem BitVec.add_ofFin {n : Nat} (x : BitVec n) (y : Fin (2 ^ n)) :
x + { toFin := y } = { toFin := x.toFin + y }
source
theorem BitVec.ofNat_add {n : Nat} (x y : Nat) :
BitVec.ofNat n (x + y) = BitVec.ofNat n x + BitVec.ofNat n y
source
theorem BitVec.ofNat_add_ofNat {n : Nat} (x y : Nat) :
BitVec.ofNat n x + BitVec.ofNat n y = BitVec.ofNat n (x + y)
source
@[simp]
theorem BitVec.toNat_add_of_not_uaddOverflow {w : Nat} {x y : BitVec w} (h : ¬x.uaddOverflow y = true) :
(x + y).toNat = x.toNat + y.toNat
source
theorem BitVec.uaddOverflow_assoc {w : Nat} {x y z : BitVec w} (h : ¬x.uaddOverflow y = true) (h' : ¬y.uaddOverflow z = true) :
(x + y).uaddOverflow z = x.uaddOverflow (y + z)

Unsigned addition overflow reassociation. If `(x + y)` and `(y + z)` do not overflow, then `(x + y) + z` overflows iff `x + (y + z)` overflows.

source
theorem BitVec.add_assoc {n : Nat} (x y z : BitVec n) :
x + y + z = x + (y + z)
source
instance BitVec.instAssociativeHAdd {n : Nat} :
Std.Associative fun (x1 x2 : BitVec n) => x1 + x2
source
theorem BitVec.add_comm {n : Nat} (x y : BitVec n) :
x + y = y + x
source
instance BitVec.instCommutativeHAdd {n : Nat} :
Std.Commutative fun (x1 x2 : BitVec n) => x1 + x2
source
@[simp]
theorem BitVec.add_zero {n : Nat} (x : BitVec n) :
x + 0#n = x
source
@[simp]
theorem BitVec.zero_add {n : Nat} (x : BitVec n) :
0#n + x = x
source
instance BitVec.instLawfulIdentityHAddOfNatOfNatNat {n : Nat} :
Std.LawfulIdentity (fun (x1 x2 : BitVec n) => x1 + x2) 0#n
source
theorem BitVec.setWidth_add {w i : Nat} (x y : BitVec w) (h : i ≤ w) :
setWidth i (x + y) = setWidth i x + setWidth i y
source
@[simp]
theorem BitVec.toInt_add {w : Nat} (x y : BitVec w) :
(x + y).toInt = (x.toInt + y.toInt).bmod (2 ^ w)
source
theorem BitVec.ofInt_add {n : Nat} (x y : Int) :
BitVec.ofInt n (x + y) = BitVec.ofInt n x + BitVec.ofInt n y
source
@[simp]
theorem BitVec.toInt_add_of_not_saddOverflow {w : Nat} {x y : BitVec w} (h : ¬x.saddOverflow y = true) :
(x + y).toInt = x.toInt + y.toInt
source
theorem BitVec.saddOverflow_assoc {w : Nat} {x y z : BitVec w} (h : ¬x.saddOverflow y = true) (h' : ¬y.saddOverflow z = true) :
(x + y).saddOverflow z = x.saddOverflow (y + z)

Signed addition overflow reassociation. If `(x + y)` and `(y + z)` do not overflow, then `(x + y) + z` overflows iff `x + (y + z)` overflows.

source
@[simp]
theorem BitVec.shiftLeft_add_distrib {w : Nat} {x y : BitVec w} {n : Nat} :
(x + y) <<< n = x <<< n + y <<< n
source
theorem BitVec.add_eq_xor {a b : BitVec 1} :
a + b = a ^^^ b

### sub/neg #

source
theorem BitVec.sub_def {n : Nat} (x y : BitVec n) :
x - y = BitVec.ofNat n (2 ^ n - y.toNat + x.toNat)
source
@[simp]
theorem BitVec.toNat_sub {n : Nat} (x y : BitVec n) :
(x - y).toNat = (2 ^ n - y.toNat + x.toNat) % 2 ^ n
source
@[simp]
theorem BitVec.toInt_sub {w : Nat} {x y : BitVec w} :
(x - y).toInt = (x.toInt - y.toInt).bmod (2 ^ w)
source
@[simp]
theorem BitVec.toNat_sub_of_not_usubOverflow {w : Nat} {x y : BitVec w} (h : ¬x.usubOverflow y = true) :
(x - y).toNat = x.toNat - y.toNat
source
@[simp]
theorem BitVec.toInt_sub_of_not_ssubOverflow {w : Nat} {x y : BitVec w} (h : ¬x.ssubOverflow y = true) :
(x - y).toInt = x.toInt - y.toInt
source
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)
source
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
source
theorem BitVec.toNat_sub' {n : Nat} (x y : BitVec n) :
(x - y).toNat = (x.toNat + (2 ^ n - y.toNat)) % 2 ^ n
source
@[simp]
theorem BitVec.toFin_sub {n : Nat} (x y : BitVec n) :
(x - y).toFin = x.toFin - y.toFin
source
theorem BitVec.ofFin_sub {n : Nat} (x : Fin (2 ^ n)) (y : BitVec n) :
{ toFin := x } - y = { toFin := x - y.toFin }
source
theorem BitVec.sub_ofFin {n : Nat} (x : BitVec n) (y : Fin (2 ^ n)) :
x - { toFin := y } = { toFin := x.toFin - y }
source
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)
source
theorem BitVec.ofNat_sub_ofNat_of_le {w : Nat} (x y : Nat) (hy : y < 2 ^ w) (hlt : y ≤ x) :
BitVec.ofNat w x - BitVec.ofNat w y = BitVec.ofNat w (x - y)
source
@[simp]
theorem BitVec.sub_zero {n : Nat} (x : BitVec n) :
x - 0#n = x
source
@[simp]
theorem BitVec.zero_sub {n : Nat} (x : BitVec n) :
0#n - x = -x
source
@[simp]
theorem BitVec.sub_self {n : Nat} (x : BitVec n) :
x - x = 0#n
source
theorem BitVec.toNat_neg_of_pos {n : Nat} {x : BitVec n} (h : 0#n < x) :
(-x).toNat = 2 ^ n - x.toNat
source
theorem BitVec.toInt_neg {w : Nat} {x : BitVec w} :
(-x).toInt = (-x.toInt).bmod (2 ^ w)
source
@[simp]
theorem BitVec.toInt_neg_of_not_negOverflow {w : Nat} {x : BitVec w} (h : ¬x.negOverflow = true) :
(-x).toInt = -x.toInt
source
theorem BitVec.ofInt_neg {w : Nat} {n : Int} :
BitVec.ofInt w (-n) = -BitVec.ofInt w n
source
@[simp]
theorem BitVec.toFin_neg {n : Nat} (x : BitVec n) :
(-x).toFin = Fin.ofNat (2 ^ n) (2 ^ n - x.toNat)
source
theorem BitVec.sub_eq_add_neg {n : Nat} (x y : BitVec n) :
x - y = x + -y
source
@[reducible, inline, deprecated BitVec.sub_eq_add_neg (since := "2025-04-04")]
abbrev BitVec.sub_toAdd {n : Nat} (x y : BitVec n) :
x - y = x + -y
Equations

- @BitVec.sub_toAdd = @BitVec.sub_eq_add_neg

Instances For

source
theorem BitVec.add_left_neg {w : Nat} (x : BitVec w) :
-x + x = 0#w
source
theorem BitVec.add_right_neg {w : Nat} (x : BitVec w) :
x + -x = 0#w
source
@[simp]
theorem BitVec.neg_zero (n : Nat) :
-0#n = 0#n
source
theorem BitVec.add_sub_cancel {w : Nat} (x y : BitVec w) :
x + y - y = x
source
theorem BitVec.sub_add_cancel {w : Nat} (x y : BitVec w) :
x - y + y = x
source
theorem BitVec.eq_sub_iff_add_eq {w : Nat} {x y z : BitVec w} :
x = z - y ↔ x + y = z
source
theorem BitVec.sub_eq_iff_eq_add {w : Nat} {x y z : BitVec w} :
x - y = z ↔ x = z + y
source
theorem BitVec.neg_one_eq_allOnes {w : Nat} :
-1#w = allOnes w
source
@[reducible, inline, deprecated BitVec.neg_one_eq_allOnes (since := "2025-04-04")]
abbrev BitVec.negOne_eq_allOnes {w : Nat} :
-1#w = allOnes w
Equations

- @BitVec.negOne_eq_allOnes = @BitVec.neg_one_eq_allOnes

Instances For

source
theorem BitVec.neg_eq_not_add {w : Nat} (x : BitVec w) :
-x = ~~~x + 1#w
source
theorem BitVec.not_eq_neg_add {w : Nat} (x : BitVec w) :
~~~x = -x - 1#w
source
@[simp]
theorem BitVec.neg_neg {w : Nat} {x : BitVec w} :
- -x = x
source
@[simp]
theorem BitVec.neg_inj {w : Nat} {x y : BitVec w} :
-x = -y ↔ x = y
source
theorem BitVec.neg_eq_iff_eq_neg {w : Nat} {x y : BitVec w} :
-x = y ↔ x = -y
source
theorem BitVec.neg_ne_iff_ne_neg {w : Nat} {x y : BitVec w} :
-x ≠ y ↔ x ≠ -y
source
@[simp]
theorem BitVec.neg_eq_zero_iff {w : Nat} {x : BitVec w} :
-x = 0#w ↔ x = 0#w
source
theorem BitVec.sub_eq_xor {a b : BitVec 1} :
a - b = a ^^^ b
source
@[simp]
theorem BitVec.sub_eq_self {x : BitVec 1} :
-x = x
source
theorem BitVec.not_neg {w : Nat} (x : BitVec w) :
~~~(-x) = x - 1#w
source
theorem BitVec.neg_add {w : Nat} {x y : BitVec w} :
-(x + y) = -x - y
source
theorem BitVec.sub_sub {n : Nat} (a b c : BitVec n) :
a - b - c = a - (b + c)
source
theorem BitVec.add_neg_eq_sub {w : Nat} {x y : BitVec w} :
x + -y = x - y
source
@[simp]
theorem BitVec.sub_neg {w : Nat} {x y : BitVec w} :
x - -y = x + y
source
theorem BitVec.neg_sub {w : Nat} {x y : BitVec w} :
-(x - y) = -x + y
source
@[simp]
theorem BitVec.add_left_inj {w : Nat} {x y : BitVec w} (z : BitVec w) :
x + z = y + z ↔ x = y
source
@[simp]
theorem BitVec.add_right_inj {w : Nat} {x y : BitVec w} (z : BitVec w) :
z + x = z + y ↔ x = y
source
@[simp]
theorem BitVec.sub_left_inj {w : Nat} {x y : BitVec w} (z : BitVec w) :
x - z = y - z ↔ x = y
source
@[simp]
theorem BitVec.sub_right_inj {w : Nat} {x y : BitVec w} (z : BitVec w) :
z - x = z - y ↔ x = y

### add self #

source
@[simp]
theorem BitVec.add_left_eq_self {w : Nat} {x y : BitVec w} :
x + y = y ↔ x = 0#w
source
@[simp]
theorem BitVec.add_right_eq_self {w : Nat} {x y : BitVec w} :
x + y = x ↔ y = 0#w
source
@[simp]
theorem BitVec.self_eq_add_right {w : Nat} {x y : BitVec w} :
x = x + y ↔ y = 0#w
source
@[simp]
theorem BitVec.self_eq_add_left {w : Nat} {x y : BitVec w} :
x = y + x ↔ y = 0#w

### fill #

source
@[simp]
theorem BitVec.getLsbD_fill {w i : Nat} {v : Bool} :
(fill w v).getLsbD i = (v && decide (i < w))
source
@[simp]
theorem BitVec.getMsbD_fill {w i : Nat} {v : Bool} :
(fill w v).getMsbD i = (v && decide (i < w))
source
@[simp]
theorem BitVec.getElem_fill {w i : Nat} {v : Bool} (h : i < w) :
(fill w v)[i] = v
source
@[simp]
theorem BitVec.msb_fill {w : Nat} {v : Bool} :
(fill w v).msb = (v && decide (0 < w))
source
theorem BitVec.fill_eq {w : Nat} {v : Bool} :
fill w v = if v = true then allOnes w else 0#w
source
@[simp]
theorem BitVec.fill_true {w : Nat} :
fill w true = allOnes w
source
@[simp]
theorem BitVec.fill_false {w : Nat} :
fill w false = 0#w
source
@[simp]
theorem BitVec.fill_toNat {w : Nat} {v : Bool} :
(fill w v).toNat = if v = true then 2 ^ w - 1 else 0
source
@[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
source
@[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 #

source
theorem BitVec.mul_def {n : Nat} {x y : BitVec n} :
x * y = { toFin := x.toFin * y.toFin }
source
@[simp]
theorem BitVec.toNat_mul {n : Nat} (x y : BitVec n) :
(x * y).toNat = x.toNat * y.toNat % 2 ^ n
source
@[simp]
theorem BitVec.toFin_mul {n : Nat} (x y : BitVec n) :
(x * y).toFin = x.toFin * y.toFin
source
theorem BitVec.ofNat_mul {n : Nat} (x y : Nat) :
BitVec.ofNat n (x * y) = BitVec.ofNat n x * BitVec.ofNat n y
source
theorem BitVec.ofNat_mul_ofNat {n : Nat} (x y : Nat) :
BitVec.ofNat n x * BitVec.ofNat n y = BitVec.ofNat n (x * y)
source
theorem BitVec.mul_comm {w : Nat} (x y : BitVec w) :
x * y = y * x
source
instance BitVec.instCommutativeHMul {w : Nat} :
Std.Commutative fun (x y : BitVec w) => x * y
source
theorem BitVec.mul_assoc {w : Nat} (x y z : BitVec w) :
x * y * z = x * (y * z)
source
instance BitVec.instAssociativeHMul {w : Nat} :
Std.Associative fun (x y : BitVec w) => x * y
source
@[simp]
theorem BitVec.mul_one {w : Nat} (x : BitVec w) :
x * 1#w = x
source
@[simp]
theorem BitVec.one_mul {w : Nat} (x : BitVec w) :
1#w * x = x
source
instance BitVec.instLawfulCommIdentityHMulOfNatOfNatNat {w : Nat} :
Std.LawfulCommIdentity (fun (x y : BitVec w) => x * y) 1#w
source
@[simp]
theorem BitVec.mul_zero {w : Nat} {x : BitVec w} :
x * 0#w = 0#w
source
@[simp]
theorem BitVec.zero_mul {w : Nat} {x : BitVec w} :
0#w * x = 0#w
source
theorem BitVec.mul_add {w : Nat} {x y z : BitVec w} :
x * (y + z) = x * y + x * z
source
theorem BitVec.add_mul {w : Nat} {x y z : BitVec w} :
(x + y) * z = x * z + y * z
source
theorem BitVec.mul_succ {w : Nat} {x y : BitVec w} :
x * (y + 1#w) = x * y + x
source
theorem BitVec.succ_mul {w : Nat} {x y : BitVec w} :
(x + 1#w) * y = x * y + y
source
theorem BitVec.mul_two {w : Nat} {x : BitVec w} :
x * 2#w = x + x
source
theorem BitVec.two_mul {w : Nat} {x : BitVec w} :
2#w * x = x + x
source
@[simp]
theorem BitVec.toInt_mul {w : Nat} (x y : BitVec w) :
(x * y).toInt = (x.toInt * y.toInt).bmod (2 ^ w)
source
@[simp]
theorem BitVec.toNat_mul_of_not_umulOverflow {w : Nat} {x y : BitVec w} (h : ¬x.umulOverflow y = true) :
(x * y).toNat = x.toNat * y.toNat
source
theorem BitVec.umulOverflow_assoc {w : Nat} {x y z : BitVec w} (h : ¬x.umulOverflow y = true) (h' : ¬y.umulOverflow z = true) :
(x * y).umulOverflow z = x.umulOverflow (y * z)

Unsigned multiplication overflow reassociation. If `(x * y)` and `(y * z)` do not overflow, then `(x * y) * z` overflows iff `x * (y * z)` overflows.

source
@[simp]
theorem BitVec.toInt_mul_of_not_smulOverflow {w : Nat} {x y : BitVec w} (h : ¬x.smulOverflow y = true) :
(x * y).toInt = x.toInt * y.toInt
source
theorem BitVec.smulOverflow_assoc {w : Nat} {x y z : BitVec w} (h : ¬x.smulOverflow y = true) (h' : ¬y.smulOverflow z = true) :
(x * y).smulOverflow z = x.smulOverflow (y * z)

Signed multiplication overflow reassociation. If `(x * y)` and `(y * z)` do not overflow, then `(x * y) * z` overflows iff `x * (y * z)` overflows.

source
theorem BitVec.ofInt_mul {n : Nat} (x y : Int) :
BitVec.ofInt n (x * y) = BitVec.ofInt n x * BitVec.ofInt n y
source
theorem BitVec.mul_eq_and {a b : BitVec 1} :
a * b = a &&& b
source
@[simp]
theorem BitVec.neg_mul {w : Nat} (x y : BitVec w) :
-x * y = -(x * y)
source
@[simp]
theorem BitVec.mul_neg {w : Nat} (x y : BitVec w) :
x * -y = -(x * y)
source
theorem BitVec.neg_mul_neg {w : Nat} (x y : BitVec w) :
-x * -y = x * y
source
theorem BitVec.neg_mul_comm {w : Nat} (x y : BitVec w) :
-x * y = x * -y
source
theorem BitVec.mul_sub {w : Nat} {x y z : BitVec w} :
x * (y - z) = x * y - x * z
source
theorem BitVec.neg_add_mul_eq_mul_not {w : Nat} {x y : BitVec w} :
-(x + x * y) = x * ~~~y
source
theorem BitVec.neg_mul_not_eq_add_mul {w : Nat} {x y : BitVec w} :
-(x * ~~~y) = x + x * y
source
theorem BitVec.neg_eq_neg_one_mul {w : Nat} (b : BitVec w) :
-b = -1#w * b
source
theorem BitVec.setWidth_mul {w i : Nat} (x y : BitVec w) (h : i ≤ w) :
setWidth i (x * y) = setWidth i x * setWidth i y

### pow #

source
@[simp]
theorem BitVec.pow_zero {w : Nat} {x : BitVec w} :
x ^ 0 = 1#w
source
theorem BitVec.pow_succ {w n : Nat} {x : BitVec w} :
x ^ (n + 1) = x ^ n * x
source
@[simp]
theorem BitVec.pow_one {w : Nat} {x : BitVec w} :
x ^ 1 = x
source
theorem BitVec.pow_add {w : Nat} {x : BitVec w} {n m : Nat} :
x ^ (n + m) = x ^ n * x ^ m

### le and lt #

source
theorem BitVec.le_def {n : Nat} {x y : BitVec n} :
x ≤ y ↔ x.toNat ≤ y.toNat
source
@[simp]
theorem BitVec.le_ofFin {n : Nat} {x : BitVec n} {y : Fin (2 ^ n)} :
x ≤ { toFin := y } ↔ x.toFin ≤ y
source
@[simp]
theorem BitVec.ofFin_le {n : Nat} {x : Fin (2 ^ n)} {y : BitVec n} :
{ toFin := x } ≤ y ↔ x ≤ y.toFin
source
@[simp]
theorem BitVec.ofNat_le_ofNat {n x y : Nat} :
BitVec.ofNat n x ≤ BitVec.ofNat n y ↔ x % 2 ^ n ≤ y % 2 ^ n
source
theorem BitVec.lt_def {n : Nat} {x y : BitVec n} :
x < y ↔ x.toNat < y.toNat
source
@[simp]
theorem BitVec.lt_ofFin {n : Nat} {x : BitVec n} {y : Fin (2 ^ n)} :
x < { toFin := y } ↔ x.toFin < y
source
@[simp]
theorem BitVec.ofFin_lt {n : Nat} {x : Fin (2 ^ n)} {y : BitVec n} :
{ toFin := x } < y ↔ x < y.toFin
source
@[simp]
theorem BitVec.ofNat_lt_ofNat {n x y : Nat} :
BitVec.ofNat n x < BitVec.ofNat n y ↔ x % 2 ^ n < y % 2 ^ n
source
@[simp]
theorem BitVec.not_le {n : Nat} {x y : BitVec n} :
¬x ≤ y ↔ y < x
source
@[simp]
theorem BitVec.not_lt {n : Nat} {x y : BitVec n} :
¬x < y ↔ y ≤ x
source
@[simp]
theorem BitVec.le_refl {n : Nat} (x : BitVec n) :
x ≤ x
source
@[simp]
theorem BitVec.lt_irrefl {n : Nat} (x : BitVec n) :
¬x < x
source
theorem BitVec.le_trans {n : Nat} {x y z : BitVec n} :
x ≤ y → y ≤ z → x ≤ z
source
theorem BitVec.lt_trans {n : Nat} {x y z : BitVec n} :
x < y → y < z → x < z
source
theorem BitVec.le_total {n : Nat} (x y : BitVec n) :
x ≤ y ∨ y ≤ x
source
theorem BitVec.le_antisymm {n : Nat} {x y : BitVec n} :
x ≤ y → y ≤ x → x = y
source
theorem BitVec.lt_asymm {n : Nat} {x y : BitVec n} :
x < y → ¬y < x
source
theorem BitVec.lt_of_le_ne {n : Nat} {x y : BitVec n} :
x ≤ y → ¬x = y → x < y
source
theorem BitVec.ne_of_lt {n : Nat} {x y : BitVec n} :
x < y → x ≠ y
source
instance BitVec.instIsLinearOrder {n : Nat} :
Std.IsLinearOrder (BitVec n)
source
instance BitVec.instLawfulOrderLT {n : Nat} :
Std.LawfulOrderLT (BitVec n)
source
theorem BitVec.length_pos_of_lt {w : Nat} {b b' : BitVec w} (h : b < b') :
0 < w
source
theorem BitVec.umod_lt {n : Nat} (x : BitVec n) {y : BitVec n} :
0 < y → x % y < y
source
theorem BitVec.not_lt_iff_le {w : Nat} {x y : BitVec w} :
¬x < y ↔ y ≤ x
source
theorem BitVec.le_of_lt {w : Nat} {x y : BitVec w} (h : x < y) :
x ≤ y
source
theorem BitVec.le_of_eq {w : Nat} {x y : BitVec w} (h : x = y) :
x ≤ y
source
@[simp]
theorem BitVec.not_lt_zero {w : Nat} {x : BitVec w} :
¬x < 0#w
source
@[simp]
theorem BitVec.le_zero_iff {w : Nat} {x : BitVec w} :
x ≤ 0#w ↔ x = 0#w
source
@[simp]
theorem BitVec.lt_one_iff {w : Nat} {x : BitVec w} (h : 0 < w) :
x < 1#w ↔ x = 0#w
source
@[simp]
theorem BitVec.not_allOnes_lt {w : Nat} {x : BitVec w} :
¬allOnes w < x
source
@[simp]
theorem BitVec.allOnes_le_iff {w : Nat} {x : BitVec w} :
allOnes w ≤ x ↔ x = allOnes w
source
@[simp]
theorem BitVec.lt_allOnes_iff {w : Nat} {x : BitVec w} :
x < allOnes w ↔ x ≠ allOnes w
source
theorem BitVec.le_of_zero_length {w : Nat} (h : w = 0) {x y : BitVec w} :
x ≤ y
source
theorem BitVec.pos_of_msb {w : Nat} {x : BitVec w} (hx : x.msb = true) :
0#w < x
source
@[simp]
theorem BitVec.lt_of_msb_false_of_msb_true {w : Nat} {x y : BitVec w} (hx : x.msb = false) (hy : y.msb = true) :
x < y
source
theorem BitVec.lt_add_one {w : Nat} {b : BitVec w} (h : b ≠ allOnes w) :
b < b + 1

### udiv #

source
theorem BitVec.udiv_def {n : Nat} {x y : BitVec n} :
x / y = BitVec.ofNat n (x.toNat / y.toNat)
source
@[simp]
theorem BitVec.toFin_udiv {n : Nat} {x y : BitVec n} :
(x / y).toFin = x.toFin / y.toFin
source
@[simp]
theorem BitVec.toNat_udiv {n : Nat} {x y : BitVec n} :
(x / y).toNat = x.toNat / y.toNat
source
@[simp]
theorem BitVec.zero_udiv {w : Nat} {x : BitVec w} :
0#w / x = 0#w
source
@[simp]
theorem BitVec.udiv_zero {n : Nat} {x : BitVec n} :
x / 0#n = 0#n
source
@[simp]
theorem BitVec.udiv_one {w : Nat} {x : BitVec w} :
x / 1#w = x
source
@[simp]
theorem BitVec.udiv_eq_and {x y : BitVec 1} :
x / y = x &&& y
source
@[simp]
theorem BitVec.udiv_self {w : Nat} {x : BitVec w} :
x / x = if (x == 0#w) = true then 0#w else 1#w
source
theorem BitVec.msb_udiv {w : Nat} (x y : BitVec w) :
(x / y).msb = (x.msb && y == 1#w)
source
@[simp]
theorem BitVec.msb_udiv_eq_false_of {w : Nat} {x y : BitVec w} (h : x.msb = false) :
(x / y).msb = false
source
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.

source
theorem BitVec.udiv_eq_zero_iff_eq_zero_or_lt {w : Nat} {x y : BitVec w} :
x / y = 0#w ↔ y = 0#w ∨ x < y

Unsigned division is zero if and only if either the denominator is zero, or the numerator is unsigned less than the denominator

source
theorem BitVec.udiv_ne_zero_iff_ne_zero_and_le {w : Nat} {x y : BitVec w} :
¬x / y = 0#w ↔ y ≠ 0#w ∧ y ≤ x

### umod #

source
theorem BitVec.umod_def {n : Nat} {x y : BitVec n} :
x % y = BitVec.ofNat n (x.toNat % y.toNat)
source
@[simp]
theorem BitVec.toNat_umod {n : Nat} {x y : BitVec n} :
(x % y).toNat = x.toNat % y.toNat
source
@[simp]
theorem BitVec.toFin_umod {w : Nat} {x y : BitVec w} :
(x % y).toFin = x.toFin % y.toFin
source
@[simp]
theorem BitVec.umod_zero {n : Nat} {x : BitVec n} :
x % 0#n = x
source
@[simp]
theorem BitVec.zero_umod {w : Nat} {x : BitVec w} :
0#w % x = 0#w
source
@[simp]
theorem BitVec.umod_one {w : Nat} {x : BitVec w} :
x % 1#w = 0#w
source
@[simp]
theorem BitVec.umod_self {w : Nat} {x : BitVec w} :
x % x = 0#w
source
@[simp]
theorem BitVec.umod_eq_and {x y : BitVec 1} :
x % y = x &&& ~~~y
source
theorem BitVec.umod_eq_of_lt {w : Nat} {x y : BitVec w} (h : x < y) :
x % y = x
source
@[simp]
theorem BitVec.msb_umod {w : Nat} {x y : BitVec w} :
(x % y).msb = (x.msb && (decide (x < y) || y == 0#w))
source
theorem BitVec.toInt_umod {w : Nat} {x y : BitVec w} :
(x % y).toInt = (↑x.toNat % ↑y.toNat).bmod (2 ^ w)
source
theorem BitVec.toInt_umod_of_msb {w : Nat} {x y : BitVec w} (h : x.msb = false) :
(x % y).toInt = x.toInt % ↑y.toNat
source
@[simp]
theorem BitVec.msb_umod_of_msb_false_of_ne_zero {w : Nat} {x y : BitVec w} (hmsb : y.msb = false) (h_ne_zero : y ≠ 0#w) :
(x % y).msb = false

### smtUDiv #

source
theorem BitVec.smtUDiv_eq {w : Nat} (x y : BitVec w) :
x.smtUDiv y = if y = 0#w then allOnes w else x / y
source
@[simp]
theorem BitVec.smtUDiv_zero {n : Nat} {x : BitVec n} :
x.smtUDiv 0#n = allOnes n

### sdiv #

source
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`.

source
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
source
theorem BitVec.toFin_sdiv {w : Nat} {x y : BitVec w} :
(x.sdiv y).toFin = match x.msb, y.msb with | false, false => x.toFin / y.toFin | false, true => (-(x / -y)).toFin | true, false => (-(-x / y)).toFin | true, true => (-x).toFin / (-y).toFin
source
@[simp]
theorem BitVec.zero_sdiv {w : Nat} {x : BitVec w} :
(0#w).sdiv x = 0#w
source
@[simp]
theorem BitVec.sdiv_zero {n : Nat} {x : BitVec n} :
x.sdiv 0#n = 0#n
source
@[simp]
theorem BitVec.sdiv_one {w : Nat} {x : BitVec w} :
x.sdiv 1#w = x
source
theorem BitVec.sdiv_eq_and (x y : BitVec 1) :
x.sdiv y = x &&& y
source
@[simp]
theorem BitVec.sdiv_self {w : Nat} {x : BitVec w} :
x.sdiv x = if (x == 0#w) = true then 0#w else 1#w
source
theorem BitVec.toNat_div_toNat_lt {w : Nat} {x y : BitVec w} :
x.toNat / y.toNat < 2 ^ w

Unsigned division never overflows.

source
theorem BitVec.toInt_ediv_toInt_lt_of_nonneg_of_nonneg {w : Nat} {x y : BitVec w} (hx : 0 ≤ x.toInt) (hy : 0 ≤ y.toInt) :
x.toInt / y.toInt < 2 ^ (w - 1)

Non-overflowing signed division bounds when numerator is nonneg, denominator is nonneg.

source
theorem BitVec.toInt_ediv_toInt_nonpos_of_nonpos_of_nonneg {w : Nat} {x y : BitVec w} (hx : x.toInt ≤ 0) (hy : 0 ≤ y.toInt) :
x.toInt / y.toInt ≤ 0

Non-overflowing signed division bounds when numerator is nonpos, denominator is nonneg.

source
theorem BitVec.toInt_ediv_toInt_nonpos_of_nonneg_of_nonpos {w : Nat} {x y : BitVec w} (hx : 0 ≤ x.toInt) (hy : y.toInt ≤ 0) :
x.toInt / y.toInt ≤ 0

Non-overflowing signed division bounds when numerator is nonneg, denominator is nonpos.

source
theorem BitVec.neg_one_ediv_toInt_eq {w : Nat} {y : BitVec w} :
-1 / y.toInt = if y.toInt = 0 then 0 else if 0 < y.toInt then -1 else 1

Given the definition of ediv/emod for signed integer division (https://dl.acm.org/doi/pdf/10.1145/128861.128862) we have that for two integers `x` and `y`: `x/y = q ↔ x.ediv y = q ↔ r = x.emod y` and in particular: `-1/y = q ↔ -1.ediv y = q ↔ r = -1.emod y`. from which it follows that: (-1)/0 = 0 (-1)/y = -1 when 0 < y (-1)/(-5) = 1 when y < 0

source
theorem BitVec.toInt_ediv_toInt_lt_of_nonpos_of_lt_neg_one {w : Nat} {x y : BitVec w} (hx : x.toInt ≤ 0) (hy : y.toInt < -1) :
x.toInt / y.toInt < 2 ^ (w - 1)

Non-overflowing signed division bounds when numerator is nonpos, denominator is less than -1.

source
theorem BitVec.neg_two_pow_le_toInt_ediv {w : Nat} {x y : BitVec w} :
-2 ^ (w - 1) ≤ x.toInt / y.toInt

Signed division of (x y : BitVec w) is always -2 ^ w ≤ x.toInt / y.toInt.

### smtSDiv #

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

source
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)
source
@[simp]
theorem BitVec.srem_zero {w : Nat} {x : BitVec w} :
x.srem 0#w = x
source
@[simp]
theorem BitVec.zero_srem {w : Nat} {x : BitVec w} :
(0#w).srem x = 0#w
source
@[simp]
theorem BitVec.srem_one {w : Nat} {x : BitVec w} :
x.srem 1#w = 0#w
source
@[simp]
theorem BitVec.srem_self {w : Nat} {x : BitVec w} :
x.srem x = 0#w
source
theorem BitVec.toNat_srem {w : Nat} {x y : BitVec w} :
(x.srem y).toNat = match x.msb, y.msb with | false, false => x.toNat % y.toNat | false, true => x.toNat % (-y).toNat | true, false => (-(-x % y)).toNat | true, true => (-(-x % -y)).toNat
source
theorem BitVec.toFin_srem {w : Nat} {x y : BitVec w} :
(x.srem y).toFin = match x.msb, y.msb with | false, false => x.toFin % y.toFin | false, true => x.toFin % (-y).toFin | true, false => (-(-x % y)).toFin | true, true => (-(-x % -y)).toFin

### smod #

source
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 => have u := x.umod (-y); if u = 0#w then u else u + y | true, false => have 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`.

source
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 => have u := x.umod (-y); if u = 0#w then u.toNat else (u + y).toNat | true, false => have u := (-x).umod y; if u = 0#w then u.toNat else (y - u).toNat | true, true => (-(-x).umod (-y)).toNat
source
theorem BitVec.toFin_smod {w : Nat} {x y : BitVec w} :
(x.smod y).toFin = match x.msb, y.msb with | false, false => x.toFin % y.toFin | false, true => if x % -y = 0#w then 0 else (x % -y + y).toFin | true, false => if -x % y = 0#w then 0 else (y - -x % y).toFin | true, true => (-(-x % -y)).toFin
source
@[simp]
theorem BitVec.smod_zero {w : Nat} {x : BitVec w} :
x.smod 0#w = x
source
@[simp]
theorem BitVec.zero_smod {w : Nat} {x : BitVec w} :
(0#w).smod x = 0#w

### ofBoolList #

source
@[simp]
theorem BitVec.getMsbD_ofBoolListBE {bs : List Bool} {i : Nat} :
(ofBoolListBE bs).getMsbD i = bs.getD i false
source
@[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)
source
@[simp]
theorem BitVec.getElem_ofBoolListBE {i : Nat} {bs : List Bool} (h : i < bs.length) :
(ofBoolListBE bs)[i] = bs[bs.length - 1 - i]
source
@[simp]
theorem BitVec.getLsbD_ofBoolListLE {bs : List Bool} {i : Nat} :
(ofBoolListLE bs).getLsbD i = bs.getD i false
source
@[reducible, inline, deprecated BitVec.getLsbD_ofBoolListLE (since := "2025-04-04")]
abbrev BitVec.getLsb_ofBoolListLE {bs : List Bool} {i : Nat} :
(ofBoolListLE bs).getLsbD i = bs.getD i false
Equations

- @BitVec.getLsb_ofBoolListLE = @BitVec.getLsbD_ofBoolListLE

Instances For

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

source
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.

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

source
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.

source
theorem BitVec.getLsbD_rotateLeftAux_of_lt {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]

source
theorem BitVec.getLsbD_rotateLeftAux_of_ge {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)`.

source
@[reducible, inline, deprecated BitVec.getLsbD_rotateLeftAux_of_lt (since := "2025-04-04")]
abbrev 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)
Equations

- @BitVec.getLsbD_rotateLeftAux_of_le = @BitVec.getLsbD_rotateLeftAux_of_lt

Instances For

source
@[reducible, inline, deprecated BitVec.getLsbD_rotateLeftAux_of_ge (since := "2025-04-04")]
abbrev 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))
Equations

- @BitVec.getLsbD_rotateLeftAux_of_geq = @BitVec.getLsbD_rotateLeftAux_of_ge

Instances For

source
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`.

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

source
theorem BitVec.getMsbD_rotateLeft {r n w : Nat} {x : BitVec w} :
(x.rotateLeft r).getMsbD n = (decide (n < w) && x.getMsbD ((r + n) % w))
source
@[simp]
theorem BitVec.msb_rotateLeft {m w : Nat} {x : BitVec w} :
(x.rotateLeft m).msb = x.getMsbD (m % w)
source
@[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)
source
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)
source
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 #

source
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.

source
theorem BitVec.getLsbD_rotateRightAux_of_lt {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]

source
theorem BitVec.getLsbD_rotateRightAux_of_ge {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>)

source
@[reducible, inline, deprecated BitVec.getLsbD_rotateRightAux_of_lt (since := "2025-04-04")]
abbrev 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)
Equations

- @BitVec.getLsbD_rotateRightAux_of_le = @BitVec.getLsbD_rotateRightAux_of_lt

Instances For

source
@[reducible, inline, deprecated BitVec.getLsbD_rotateRightAux_of_ge (since := "2025-04-04")]
abbrev 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)))
Equations

- @BitVec.getLsbD_rotateRightAux_of_geq = @BitVec.getLsbD_rotateRightAux_of_ge

Instances For

source
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.

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

source
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`.

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

source
@[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))
source
@[simp]
theorem BitVec.msb_rotateRight {r w : Nat} {x : BitVec w} :
(x.rotateRight r).msb = x.getMsbD ((w - r % w) % w)
source
@[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
source
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)
source
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))
source
theorem BitVec.twoPow_eq (w i : Nat) :
twoPow w i = 1#w <<< i
source
@[simp]
theorem BitVec.toNat_twoPow (w i : Nat) :
(twoPow w i).toNat = 2 ^ i % 2 ^ w
source
theorem BitVec.toNat_twoPow_of_le {i w : Nat} (h : w ≤ i) :
(twoPow w i).toNat = 0
source
theorem BitVec.toNat_twoPow_of_lt {i w : Nat} (h : i < w) :
(twoPow w i).toNat = 2 ^ i
source
theorem BitVec.toNat_twoPow_eq_ite {i w : Nat} :
(twoPow w i).toNat = if i < w then 2 ^ i else 0
source
@[simp]
theorem BitVec.getLsbD_twoPow {w : Nat} (i j : Nat) :
(twoPow w i).getLsbD j = (decide (i < w) && decide (i = j))
source
@[simp]
theorem BitVec.msb_twoPow {i w : Nat} :
(twoPow w i).msb = (decide (i < w) && decide (i = w - 1))
source
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
source
theorem BitVec.toFin_twoPow {w i : Nat} :
(twoPow w i).toFin = Fin.ofNat (2 ^ w) (2 ^ i)
source
@[simp]
theorem BitVec.getElem_twoPow {w i j : Nat} (h : j < w) :
(twoPow w i)[j] = decide (j = i)
source
@[simp]
theorem BitVec.getMsbD_twoPow {i j w : Nat} :
(twoPow w i).getMsbD j = (decide (i < w) && decide (j = w - i - 1))
source
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
source
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
source
@[simp]
theorem BitVec.mul_twoPow_eq_shiftLeft {w : Nat} (x : BitVec w) (i : Nat) :
x * twoPow w i = x <<< i
source
theorem BitVec.twoPow_mul_eq_shiftLeft {w : Nat} (x : BitVec w) (i : Nat) :
twoPow w i * x = x <<< i
source
theorem BitVec.twoPow_zero {w : Nat} :
twoPow w 0 = 1#w
source
theorem BitVec.shiftLeft_eq_mul_twoPow {w : Nat} (x : BitVec w) (n : Nat) :
x <<< n = x * twoPow w n
source
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

source
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`.

source
theorem BitVec.toInt_mul_toInt_le {w : Nat} {x y : BitVec w} :
x.toInt * y.toInt ≤ 2 ^ (w * 2 - 2)
source
theorem BitVec.le_toInt_mul_toInt {w : Nat} {x y : BitVec w} :
-2 ^ (w * 2 - 2) ≤ x.toInt * y.toInt
source
theorem BitVec.shiftLeft_neg {w : Nat} {x : BitVec w} {y : Nat} :
(-x) <<< y = -x <<< y
source
@[simp]
theorem BitVec.true_cons_zero {w : Nat} :
cons true 0#w = twoPow (w + 1) w
source
@[simp]
theorem BitVec.false_cons_zero {w : Nat} :
cons false 0#w = 0#(w + 1)
source
@[simp]
theorem BitVec.zero_concat_true {w : Nat} :
(0#w).concat true = 1#(w + 1)
source
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.

source
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` equals keeping the lower `i` bits and then performing bitwise-or with `twoPow i = (1 << i)`,

source
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`.

source
@[simp]
theorem BitVec.replicate_zero {w : Nat} {x : BitVec w} :
replicate 0 x = 0#0
source
@[simp]
theorem BitVec.replicate_one {w : Nat} {x : BitVec w} :
replicate 1 x = BitVec.cast ⋯ x
source
@[simp]
theorem BitVec.replicate_succ {w n : Nat} {x : BitVec w} :
replicate (n + 1) x = BitVec.cast ⋯ (x ++ replicate n x)
source
@[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))
source
@[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]
source
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₃))
source
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₃)
source
theorem BitVec.replicate_append_self {w n : Nat} {x : BitVec w} :
x ++ replicate n x = BitVec.cast ⋯ (replicate n x ++ x)
source
theorem BitVec.replicate_succ' {w n : Nat} {x : BitVec w} :
replicate (n + 1) x = BitVec.cast ⋯ (replicate n x ++ x)
source
theorem 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
source
theorem BitVec.setWidth_setWidth_eq_self {w : Nat} {a : BitVec w} {w' : Nat} (h : a < twoPow w w') :
setWidth w (setWidth w' a) = a

### intMin #

source
theorem BitVec.getLsbD_intMin {i : Nat} (w : Nat) :
(intMin w).getLsbD i = decide (i + 1 = w)
source
theorem BitVec.getMsbD_intMin {w i : Nat} :
(intMin w).getMsbD i = (decide (0 < w) && decide (i = 0))
source
@[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`.

source
theorem BitVec.toNat_intMin_of_pos {w : Nat} (hw : 0 < w) :
(intMin w).toNat = 2 ^ (w - 1)
source
@[simp]
theorem BitVec.intMin_eq_zero_iff {w : Nat} :
intMin w = 0#w ↔ w = 0
source
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`.

source
theorem BitVec.toInt_intMin_of_pos {v : Nat} (hv : 0 < v) :
(intMin v).toInt = -2 ^ (v - 1)
source
theorem BitVec.toInt_intMin_le {w : Nat} (x : BitVec w) :
(intMin w).toInt ≤ x.toInt
source
theorem BitVec.intMin_sle {w : Nat} (x : BitVec w) :
(intMin w).sle x = true
source
@[simp]
theorem BitVec.neg_intMin {w : Nat} :
-intMin w = intMin w
source
@[simp]
theorem BitVec.neg_eq_intMin {w : Nat} {x : BitVec w} :
-x = intMin w ↔ x = intMin w
source
theorem BitVec.neg_ne_intMin_inj {w : Nat} {x : BitVec w} :
-x ≠ intMin w ↔ x ≠ intMin w
source
@[simp]
theorem BitVec.abs_intMin {w : Nat} :
(intMin w).abs = intMin w
source
theorem BitVec.toInt_neg_of_ne_intMin {w : Nat} {x : BitVec w} (rs : x ≠ intMin w) :
(-x).toInt = -x.toInt
source
theorem BitVec.toInt_neg_eq_ite {w : Nat} {x : BitVec w} :
(-x).toInt = if x = intMin w then x.toInt else -x.toInt
source
theorem BitVec.msb_intMin {w : Nat} :
(intMin w).msb = decide (0 < w)
source
theorem BitVec.ne_intMin_of_msb_eq_false {w : Nat} (h : 0 < w) {n : BitVec w} (hn : n.msb = false) :
n ≠ intMin w
source
theorem BitVec.toInt_neg_eq_of_msb {w : Nat} {x : BitVec w} (h : x.msb = false) :
(-x).toInt = -x.toInt
source
theorem BitVec.lt_intMin_iff_msb_eq_false {w : Nat} {x : BitVec w} (hw : 0 < w) :
x < intMin w ↔ x.msb = false
source
theorem BitVec.intMin_le_iff_msb_eq_true {w : Nat} {x : BitVec w} (hw : 0 < w) :
intMin w ≤ x ↔ x.msb = true
source
theorem BitVec.le_intMin_of_msb_eq_false {w : Nat} {x : BitVec w} (hx : x.msb = false) :
x ≤ intMin w
source
theorem BitVec.neg_le_intMin_of_msb_eq_true {w : Nat} {x : BitVec w} (hx : x.msb = true) :
-x ≤ intMin w

### intMax #

source
@[simp]
theorem BitVec.toNat_intMax {w : Nat} :
(intMax w).toNat = 2 ^ (w - 1) - 1
source
@[simp]
theorem BitVec.getLsbD_intMax {i : Nat} (w : Nat) :
(intMax w).getLsbD i = decide (i + 1 < w)
source
@[simp]
theorem BitVec.intMax_add_one {w : Nat} :
intMax w + 1#w = intMin w
source
@[simp]
theorem BitVec.toInt_intMax {w : Nat} :
(intMax w).toInt = 2 ^ (w - 1) - 1

### Non-overflow theorems #

source
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.

source
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`

source
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)`.

source
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`.

source
theorem BitVec.toNat_mul_toNat_lt {w : Nat} {x y : BitVec w} :
x.toNat * y.toNat < 2 ^ (w * 2)
source
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.

source
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.

source
theorem BitVec.sdiv_neg_one {w : Nat} {x : BitVec w} :
x.toInt / -1 = -x.toInt
source
theorem BitVec.sdivOverflow_eq_negOverflow_of_eq_allOnes {w : Nat} {x y : BitVec w} (hy : y = allOnes w) :
x.sdivOverflow y = x.negOverflow
source
theorem BitVec.two_pow_le_toInt_mul_toInt_iff {w : Nat} {x y : BitVec w} :
2 ^ (w - 1) ≤ x.toInt * y.toInt ↔ (signExtend (w * 2) (intMax w)).slt (signExtend (w * 2) x * signExtend (w * 2) y) = true
source
theorem BitVec.toInt_mul_toInt_lt_neg_two_pow_iff {w : Nat} {x y : BitVec w} :
x.toInt * y.toInt < -2 ^ (w - 1) ↔ (signExtend (w * 2) x * signExtend (w * 2) y).slt (signExtend (w * 2) (intMin w)) = true

### neg #

source
theorem BitVec.msb_eq_toInt {w : Nat} {x : BitVec w} :
x.msb = decide (x.toInt < 0)
source
theorem BitVec.msb_eq_toNat {w : Nat} {x : BitVec w} :
x.msb = decide (x.toNat ≥ 2 ^ (w - 1))
source
theorem BitVec.neg_ofNat_eq_ofInt_neg {w x : Nat} :
-BitVec.ofNat w x = BitVec.ofInt w (-↑x)

Negating a bitvector created from a natural number equals creating a bitvector from the the negative of that number.

source
@[simp]
theorem BitVec.neg_toInt_neg {w : Nat} {x : BitVec w} (h : x.msb = false) :
-(-x).toInt = ↑x.toNat
source
theorem BitVec.toNat_pos_of_ne_zero {w : Nat} {x : BitVec w} (hx : x ≠ 0#w) :
0 < x.toNat
source
theorem BitVec.toNat_neg_lt_of_msb {w : Nat} (x : BitVec w) (hmsb : x.msb = true) :
(-x).toNat ≤ 2 ^ (w - 1)

### abs #

source
theorem BitVec.abs_eq {w : Nat} (x : BitVec w) :
x.abs = if x.msb = true then -x else x
source
@[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
source
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
source
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]
source
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
source
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
source
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
source
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`.

source
theorem BitVec.toInt_abs_eq_natAbs_of_ne_intMin {w : Nat} {x : BitVec w} (hx : x ≠ intMin w) :
x.abs.toInt = ↑x.toInt.natAbs
source
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 #

source
theorem BitVec.getLsbD_reverse {w i : Nat} {x : BitVec w} :
x.reverse.getLsbD i = x.getMsbD i
source
theorem BitVec.getElem_reverse {w i : Nat} (x : BitVec w) (h : i < w) :
x.reverse[i] = x.getMsbD i
source
theorem BitVec.getMsbD_reverse {w i : Nat} {x : BitVec w} :
x.reverse.getMsbD i = x.getLsbD i
source
theorem BitVec.msb_reverse {w : Nat} {x : BitVec w} :
x.reverse.msb = x.getLsbD 0
source
theorem BitVec.reverse_append {w v : Nat} {x : BitVec w} {y : BitVec v} :
(x ++ y).reverse = BitVec.cast ⋯ (y.reverse ++ x.reverse)
source
@[simp]
theorem BitVec.reverse_cast {w v : Nat} (h : w = v) (x : BitVec w) :
(BitVec.cast h x).reverse = BitVec.cast h x.reverse
source
theorem BitVec.reverse_replicate {w n : Nat} {x : BitVec w} :
(replicate n x).reverse = replicate n x.reverse
source
@[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))
source
@[simp]
theorem BitVec.msb_replicate {n w : Nat} {x : BitVec w} :
(replicate n x).msb = (decide (0 < n) && x.msb)
source
@[simp]
theorem BitVec.reverse_eq_zero_iff {w : Nat} {x : BitVec w} :
x.reverse = 0#w ↔ x = 0#w
source
@[simp]
theorem BitVec.reverse_reverse_eq {w : Nat} {x : BitVec w} :
x.reverse.reverse = x

### Inequalities (le / lt) #

source
theorem BitVec.ule_eq_not_ult {w : Nat} (x y : BitVec w) :
x.ule y = !y.ult x
source
theorem BitVec.slt_eq_ult_of_msb_eq {w : Nat} {x y : BitVec w} (h : x.msb = y.msb) :
x.slt y = x.ult y

If two bitvectors have the same `msb`, then signed and unsigned comparisons coincide

source
theorem BitVec.ult_eq_msb_of_msb_neq {w : Nat} {x y : BitVec w} (h : x.msb ≠ y.msb) :
x.ult y = y.msb

If two bitvectors have different `msb`s, then unsigned comparison is determined by this bit

source
theorem BitVec.slt_eq_not_ult_of_msb_neq {w : Nat} {x y : BitVec w} (h : x.msb ≠ y.msb) :
x.slt y = !x.ult y

If two bitvectors have different `msb`s, then signed and unsigned comparisons are opposites

source
theorem BitVec.slt_eq_ult {w : Nat} {x y : BitVec w} :
x.slt y = (x.msb != y.msb ^^ x.ult y)
source
theorem BitVec.sle_eq_not_slt {w : Nat} {x y : BitVec w} :
x.sle y = !y.slt x
source
theorem BitVec.zero_sle_eq_not_msb {w : Nat} {x : BitVec w} :
(0#w).sle x = !x.msb
source
theorem BitVec.zero_sle_iff_msb_eq_false {w : Nat} {x : BitVec w} :
(0#w).sle x = true ↔ x.msb = false
source
theorem BitVec.toNat_toInt_of_sle {w : Nat} {x : BitVec w} (hx : (0#w).sle x = true) :
x.toInt.toNat = x.toNat
source
theorem BitVec.sle_eq_ule {w : Nat} {x y : BitVec w} :
x.sle y = (x.msb != y.msb ^^ x.ule y)
source
theorem BitVec.sle_eq_ule_of_msb_eq {w : Nat} {x y : BitVec w} (h : x.msb = y.msb) :
x.sle y = x.ule y
source
theorem BitVec.le_toNat_iff_getLsbD_eq_true {w i : Nat} {x : BitVec w} (hi : i < w) :
2 ^ i ≤ x.toNat ↔ ∃ (k : Nat), x.getLsbD (i + k) = true

A bitvector interpreted as a natural number is greater than or equal to `2 ^ i` if and only if there exists at least one bit with `true` value at position `i` or higher.

source
theorem BitVec.toNat_lt_iff_getLsbD_eq_false {w : Nat} {x : BitVec w} (i : Nat) (hi : i < w) :
x.toNat < 2 ^ i ↔ ∀ (k : Nat), x.getLsbD (i + k) = false

A bitvector interpreted as a natural number is strictly smaller than `2 ^ i` if and only if all bits at position `i` or higher are false.

source
theorem BitVec.getElem_eq_true_of_lt_of_le {w k : Nat} {x : BitVec w} (hk' : k < w) (hlt : x.toNat < 2 ^ (k + 1)) (hle : 2 ^ k ≤ x.toNat) :
x[k] = true

If a bitvector interpreted as a natural number is strictly smaller than `2 ^ (k + 1)` and greater than or equal to 2 ^ k, then the bit at position `k` must be `true`

source
theorem BitVec.not_lt_iff {w : Nat} {b : BitVec w} :
~~~b < b ↔ 0 < w ∧ b.msb = true

### Count leading zeros #

source
theorem BitVec.clzAuxRec_zero {w : Nat} (x : BitVec w) :
x.clzAuxRec 0 = if x.getLsbD 0 = true then BitVec.ofNat w (w - 1) else BitVec.ofNat w w
source
theorem BitVec.clzAuxRec_succ {w n : Nat} (x : BitVec w) :
x.clzAuxRec (n + 1) = if x.getLsbD (n + 1) = true then BitVec.ofNat w (w - 1 - (n + 1)) else x.clzAuxRec n
source
theorem BitVec.clzAuxRec_eq_clzAuxRec_of_le {w n : Nat} {x : BitVec w} (h : w - 1 ≤ n) :
x.clzAuxRec n = x.clzAuxRec (w - 1)
source
theorem BitVec.clzAuxRec_eq_clzAuxRec_of_getLsbD_false {w n k : Nat} {x : BitVec w} (h : ∀ (i : Nat), n < i → x.getLsbD i = false) :
x.clzAuxRec n = x.clzAuxRec (n + k)
source
theorem BitVec.clzAuxRec_le {w : Nat} {x : BitVec w} (n : Nat) :
x.clzAuxRec n ≤ ↑w
source
theorem BitVec.clzAuxRec_eq_iff_of_getLsbD_false {w n : Nat} {x : BitVec w} (h : ∀ (i : Nat), n < i → x.getLsbD i = false) :
x.clzAuxRec n = BitVec.ofNat w w ↔ ∀ (j : Nat), j ≤ n → x.getLsbD j = false
source
theorem BitVec.clz_le {w : Nat} {x : BitVec w} :
x.clz ≤ ↑w
source
@[simp]
theorem BitVec.clz_eq_iff_eq_zero {w : Nat} {x : BitVec w} :
x.clz = ↑w ↔ x = 0#w
source
theorem BitVec.clzAuxRec_eq_zero_iff {w n : Nat} {x : BitVec w} (h : ∀ (i : Nat), n < i → x.getLsbD i = false) (hw : 0 < w) :
(x.clzAuxRec n).toNat = 0 ↔ x[w - 1] = true
source
theorem BitVec.clz_eq_zero_iff {w : Nat} {x : BitVec w} (hw : 0 < w) :
x.clz.toNat = 0 ↔ 2 ^ (w - 1) ≤ x.toNat
source
theorem BitVec.clz_lt_iff_ne_zero {w : Nat} {x : BitVec w} :
x.clz < ↑w ↔ x ≠ 0#w

The number of leading zeroes is strictly less than the bitwidth iff the bitvector is nonzero.

source
theorem BitVec.getLsbD_false_of_clzAuxRec {w n : Nat} {x : BitVec w} (h : ∀ (i : Nat), n < i → x.getLsbD i = false) (j : Nat) :
x.getLsbD (w - (x.clzAuxRec n).toNat + j) = false
source
theorem BitVec.getLsbD_true_of_eq_clzAuxRec_of_ne_zero {w n : Nat} {x : BitVec w} (hx : ¬x = 0#w) (hn : ∀ (i : Nat), n < i → x.getLsbD i = false) :
x.getLsbD (w - 1 - (x.clzAuxRec n).toNat) = true
source
theorem BitVec.getLsbD_true_clz_of_ne_zero {w : Nat} {x : BitVec w} (hw : 0 < w) (hx : x ≠ 0#w) :
x.getLsbD (w - 1 - x.clz.toNat) = true
source
theorem BitVec.two_pow_sub_clz_le_toNat_of_ne_zero {w : Nat} {x : BitVec w} (hw : 0 < w) (hx : x ≠ 0#w) :
2 ^ (w - 1 - x.clz.toNat) ≤ x.toNat

A nonzero bitvector is lower-bounded by its leading zeroes.

source
theorem BitVec.toNat_lt_two_pow_sub_clz {w : Nat} {x : BitVec w} :
x.toNat < 2 ^ (w - x.clz.toNat)

A bitvector is upper bounded by the number of leading zeroes.

source
theorem BitVec.clz_eq_reverse_ctz {w : Nat} {x : BitVec w} :
x.clz = x.reverse.ctz

### Count trailing zeros #

source
theorem BitVec.ctz_eq_reverse_clz {w : Nat} {x : BitVec w} :
x.ctz = x.reverse.clz
source
@[simp]
theorem BitVec.ctz_lt_iff_ne_zero {w : Nat} {x : BitVec w} :
x.ctz < ↑w ↔ x ≠ 0#w

The number of trailing zeroes is strictly less than the bitwidth iff the bitvector is nonzero.

source
theorem BitVec.getLsbD_false_of_lt_ctz {w i : Nat} {x : BitVec w} (hi : i < x.ctz.toNat) :
x.getLsbD i = false

If a bitvec is different than zero the bits at indexes lower than `ctz x` are false.

source
theorem BitVec.getLsbD_true_ctz_of_ne_zero {w : Nat} {x : BitVec w} (hx : x ≠ 0#w) :
x.getLsbD x.ctz.toNat = true

If a bitvec is different than zero, the bit at index `ctz x`, i.e., the first bit after the trailing zeros, is true.

source
theorem BitVec.two_pow_ctz_le_toNat_of_ne_zero {w : Nat} {x : BitVec w} (hx : x ≠ 0#w) :
2 ^ x.ctz.toNat ≤ x.toNat

A nonzero bitvector is lower-bounded by its trailing zeroes.