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

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

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

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:

lo ≤ hi for the interval to be a well-formed closed interval.
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.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

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_of_le.toInt_signExtend_of_lt {w v : Nat} (h : w ≤ v) {x : BitVec w} (hv : w < v) :

(signExtend v x).toInt = x.toInt

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

@[simp]

theorem BitVec.toNat_append {m n : Nat} (x : BitVec m) (y : BitVec n) :

(x ++ y).toNat = x.toNat <<< n ||| y.toNat

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 = BitVec.cast ⋯ (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. Diagramatically:

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

source

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

extractLsb' start len (xhi ++ xlo) = extractLsb' start len xlo

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

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.

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

@[simp]

theorem BitVec.toNat_cons {w : Nat} (b : Bool) (x : BitVec w) :

(cons b x).toNat = b.toNat <<< w ||| x.toNat

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

theorem BitVec.getElem_cons {b : Bool} {n : Nat} {x : BitVec n} {i : Nat} (h : i < n + 1) :

(cons b x)[i] = if h : i = n then b else x[i]

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.cons_msb_setWidth {w : Nat} (x : BitVec (w + 1)) :

cons x.msb (setWidth w x) = x

source

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

theorem BitVec.eq_msb_cons_setWidth {w : Nat} (x : BitVec (w + 1)) :

x = cons x.msb (setWidth w x)

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.getLsbD_concat_zero {w✝ : Nat} {x : BitVec w✝} {b : Bool} :

(x.concat b).getLsbD 0 = b

source

@[simp]

theorem BitVec.getElem_concat_zero {w✝ : Nat} {x : BitVec w✝} {b : Bool} :

(x.concat b)[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

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

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

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

@[simp]

theorem BitVec.toNat_neg {n : Nat} (x : BitVec n) :

(-x).toNat = (2 ^ n - x.toNat) % 2 ^ 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

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

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

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

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.

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

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

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

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

Equation theorem for smod in terms of umod.

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

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 equalsk eeping 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.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.BitVec.setWidth_add_eq_mod {w i : Nat} {x y : BitVec w} :

setWidth i (x + y) = (setWidth i x + setWidth i y) % twoPow i w

intMin #

source

def BitVec.intMin (w : Nat) :

BitVec w

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

Equations

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

Instances For

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

def BitVec.intMax (w : Nat) :

BitVec w

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

Equations

BitVec.intMax w = BitVec.twoPow w (w - 1) - 1

Instances For

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

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)

Decidable quantifiers #

source

theorem BitVec.forall_zero_iff {P : BitVec 0 → Prop} :

(∀ (v : BitVec 0), P v) ↔ P 0#0

source

theorem BitVec.forall_cons_iff {n : Nat} {P : BitVec (n + 1) → Prop} :

(∀ (v : BitVec (n + 1)), P v) ↔ ∀ (x : Bool) (v : BitVec n), P (cons x v)

source

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

Decidable (∀ (v : BitVec 0), P v)

Equations

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

source

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

Decidable (∀ (v : BitVec (n + 1)), P v)

Equations

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

source

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

Decidable (∃ (v : BitVec 0), P v)

Equations

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

source

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

Decidable (∃ (v : BitVec (n + 1)), P v)

Equations

BitVec.instDecidableExistsBitVecSucc P = decidable_of_iff (¬∀ (v : BitVec (n + 1)), ¬P v) ⋯

source

instance BitVec.instDecidableForallBitVec (n : Nat) (P : BitVec n → Prop) [DecidablePred P] :

Decidable (∀ (v : BitVec n), P v)

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

Equations

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

source

instance BitVec.instDecidableExistsBitVec (n : Nat) (P : BitVec n → Prop) [DecidablePred P] :

Decidable (∃ (v : BitVec n), P v)

Equations

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

Deprecations #

source

@[reducible, inline, deprecated BitVec.toFin_uShiftRight (since := "2025-02-18")]

abbrev BitVec.toFin_uShiftRight {w : Nat} {x : BitVec w} {n : Nat} :

(x >>> n).toFin = x.toFin / Fin.ofNat' (2 ^ w) (2 ^ n)

Equations

@BitVec.toFin_uShiftRight = @BitVec.toFin_ushiftRight

Instances For

source

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

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

signExtend v x = setWidth v x

Equations

@BitVec.signExtend_eq_not_setWidth_not_of_msb_false = @BitVec.signExtend_eq_setWidth_of_msb_false

Instances For

source

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

abbrev BitVec.truncate_eq_zeroExtend {w v : Nat} {x : BitVec w} :

truncate v x = setWidth v x

Equations

@BitVec.truncate_eq_zeroExtend = @BitVec.truncate_eq_setWidth

Instances For

source

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

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

(setWidth' p x).toNat = x.toNat

Equations

@BitVec.toNat_zeroExtend' = @BitVec.toNat_setWidth'

Instances For

source

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

abbrev BitVec.toNat_zeroExtend {n : Nat} (i : Nat) (x : BitVec n) :

(setWidth i x).toNat = x.toNat % 2 ^ i

Equations

@BitVec.toNat_zeroExtend = @BitVec.toNat_setWidth

Instances For

source

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

abbrev BitVec.toNat_truncate {n : Nat} (i : Nat) (x : BitVec n) :

(setWidth i x).toNat = x.toNat % 2 ^ i

Equations

@BitVec.toNat_truncate = @BitVec.toNat_setWidth

Instances For

source

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

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

setWidth n x = x

Equations

@BitVec.zeroExtend_eq = @BitVec.setWidth_eq

Instances For

source

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

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

setWidth n x = x

Equations

@BitVec.truncate_eq = @BitVec.setWidth_eq

Instances For

source

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

abbrev BitVec.zeroExtend_zero (m n : Nat) :

setWidth m 0#n = 0#m

Equations

BitVec.zeroExtend_zero = BitVec.setWidth_zero

Instances For

source

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

abbrev BitVec.getElem_zeroExtend {n : Nat} (m : Nat) (x : BitVec n) (i : Nat) (h : i < m) :

(setWidth m x)[i] = x.getLsbD i

Equations

@BitVec.getElem_zeroExtend = @BitVec.getElem_setWidth

Instances For

source

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

abbrev BitVec.getElem_zeroExtend' {w v : Nat} (x : BitVec w) (i : Nat) (h : w ≤ v) (hi : i < v) :

(setWidth' h x)[i] = x.getLsbD i

Equations

@BitVec.getElem_zeroExtend' = @BitVec.getElem_setWidth'

Instances For

source

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

abbrev BitVec.getElem?_zeroExtend {n : Nat} (m : Nat) (x : BitVec n) (i : Nat) :

(setWidth m x)[i]? = if i < m then some (x.getLsbD i) else none

Equations

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

Instances For

source

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

abbrev BitVec.getElem?_zeroExtend' {w v : Nat} (x : BitVec w) (i : Nat) (h : w ≤ v) :

(setWidth' h x)[i]? = if i < v then some (x.getLsbD i) else none

Equations

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

Instances For

source

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

abbrev BitVec.getLsbD_zeroExtend {n : Nat} (m : Nat) (x : BitVec n) (i : Nat) :

(setWidth m x).getLsbD i = (decide (i < m) && x.getLsbD i)

Equations

@BitVec.getLsbD_zeroExtend = @BitVec.getLsbD_setWidth

Instances For

source

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

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

(setWidth' ge x).getLsbD i = x.getLsbD i

Equations

@BitVec.getLsbD_zeroExtend' = @BitVec.getLsbD_setWidth'

Instances For

source

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

abbrev BitVec.getMsbD_zeroExtend_add {w k i : Nat} {x : BitVec w} (h : k ≤ i) :

(setWidth (w + k) x).getMsbD i = x.getMsbD (i - k)

Equations

@BitVec.getMsbD_zeroExtend_add = @BitVec.getMsbD_setWidth_add

Instances For

source

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

abbrev BitVec.getMsbD_zeroExtend' {m n : Nat} (ge : m ≥ n) (x : BitVec n) (i : Nat) :

(setWidth' ge x).getMsbD i = (decide (m - n ≤ i) && x.getMsbD (i + n - m))

Equations

@BitVec.getMsbD_zeroExtend' = @BitVec.getMsbD_setWidth'

Instances For

source

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

abbrev BitVec.getElem_truncate {n : Nat} (m : Nat) (x : BitVec n) (i : Nat) (h : i < m) :

(setWidth m x)[i] = x.getLsbD i

Equations

@BitVec.getElem_truncate = @BitVec.getElem_setWidth

Instances For

source

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

abbrev BitVec.getElem?_truncate {n : Nat} (m : Nat) (x : BitVec n) (i : Nat) :

(setWidth m x)[i]? = if i < m then some (x.getLsbD i) else none

Equations

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

Instances For

source

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

abbrev BitVec.getLsbD_truncate {n : Nat} (m : Nat) (x : BitVec n) (i : Nat) :

(setWidth m x).getLsbD i = (decide (i < m) && x.getLsbD i)

Equations

@BitVec.getLsbD_truncate = @BitVec.getLsbD_setWidth

Instances For

source

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

abbrev BitVec.msb_truncate {w v : Nat} (x : BitVec w) :

(setWidth v x).msb = (decide (0 < v) && x.getLsbD (v - 1))

Equations

@BitVec.msb_truncate = @BitVec.msb_setWidth

Instances For

source

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

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

BitVec.cast h (setWidth v x) = setWidth v' x

Equations

@BitVec.cast_zeroExtend = @BitVec.cast_setWidth

Instances For

source

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

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

BitVec.cast h (setWidth v x) = setWidth v' x

Equations

@BitVec.cast_truncate = @BitVec.cast_setWidth

Instances For

source

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

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

setWidth k (setWidth l x) = setWidth k x

Equations

@BitVec.zeroExtend_zeroExtend_of_le = @BitVec.setWidth_setWidth_of_le

Instances For

source

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

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

setWidth n x = x

Equations

@BitVec.truncate_eq_self = @BitVec.setWidth_eq

Instances For

source

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

abbrev BitVec.truncate_cast {w v k : Nat} {x : BitVec w} {h : w = v} :

setWidth k (BitVec.cast h x) = setWidth k x

Equations

@BitVec.truncate_cast = @BitVec.setWidth_cast

Instances For

source

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

abbrev BitVec.mbs_zeroExtend {w v : Nat} (x : BitVec w) :

(setWidth v x).msb = (decide (0 < v) && x.getLsbD (v - 1))

Equations

@BitVec.mbs_zeroExtend = @BitVec.msb_setWidth

Instances For

source

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

abbrev BitVec.mbs_zeroExtend' {w v : Nat} (x : BitVec w) (h : w ≤ v) :

(setWidth' h x).msb = (decide (0 < v) && x.getLsbD (v - 1))

Equations

@BitVec.mbs_zeroExtend' = @BitVec.msb_setWidth'

Instances For

source

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

abbrev BitVec.zeroExtend_one_eq_ofBool_getLsb_zero {w : Nat} (x : BitVec w) :

setWidth 1 x = ofBool (x.getLsbD 0)

Equations

@BitVec.zeroExtend_one_eq_ofBool_getLsb_zero = @BitVec.setWidth_one_eq_ofBool_getLsb_zero

Instances For

source

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

abbrev BitVec.zeroExtend_ofNat_one_eq_ofNat_one_of_lt {v w : Nat} (hv : 0 < v) :

setWidth w 1#v = 1#w

Equations

@BitVec.zeroExtend_ofNat_one_eq_ofNat_one_of_lt = @BitVec.setWidth_ofNat_one_eq_ofNat_one_of_lt

Instances For

source

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

abbrev BitVec.truncate_one {w : Nat} {x : BitVec w} :

setWidth 1 x = ofBool (x.getLsbD 0)

Equations

@BitVec.truncate_one = @BitVec.setWidth_one

Instances For

source

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

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

setWidth v (BitVec.ofNat w x) = BitVec.ofNat v x

Equations

@BitVec.truncate_ofNat_of_le = @BitVec.setWidth_ofNat_of_le

Instances For

source

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

abbrev BitVec.truncate_or {w k : Nat} {x y : BitVec w} :

setWidth k (x ||| y) = setWidth k x ||| setWidth k y

Equations

@BitVec.truncate_or = @BitVec.setWidth_or

Instances For

source

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

abbrev BitVec.truncate_and {w k : Nat} {x y : BitVec w} :

setWidth k (x &&& y) = setWidth k x &&& setWidth k y

Equations

@BitVec.truncate_and = @BitVec.setWidth_and

Instances For

source

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

abbrev BitVec.truncate_xor {w k : Nat} {x y : BitVec w} :

setWidth k (x ^^^ y) = setWidth k x ^^^ setWidth k y

Equations

@BitVec.truncate_xor = @BitVec.setWidth_xor

Instances For

source

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

abbrev BitVec.truncate_not {w k : Nat} {x : BitVec w} :

k ≤ w → setWidth k (~~~x) = ~~~setWidth k x

Equations

@BitVec.truncate_not = @BitVec.setWidth_not

Instances For

source

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

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

signExtend v x = setWidth v x

Equations

@BitVec.signExtend_eq_not_zeroExtend_not_of_msb_false = @BitVec.signExtend_eq_setWidth_of_msb_false

Instances For

source

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

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

signExtend v x = ~~~setWidth v (~~~x)

Equations

@BitVec.signExtend_eq_not_zeroExtend_not_of_msb_true = @BitVec.signExtend_eq_not_setWidth_not_of_msb_true

Instances For

source

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

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

signExtend v x = setWidth v x

Equations

@BitVec.signExtend_eq_truncate_of_lt = @BitVec.signExtend_eq_setWidth_of_le

Instances For

source

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

abbrev BitVec.truncate_append {w v k : Nat} {x : BitVec w} {y : BitVec v} :

setWidth k (x ++ y) = if h : k ≤ v then setWidth k y else BitVec.cast ⋯ (setWidth (k - v) x ++ y)

Equations

@BitVec.truncate_append = @BitVec.setWidth_append

Instances For

source

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

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

setWidth (v' + w') (x ++ y) = setWidth v' x ++ setWidth w' y

Equations

@BitVec.truncate_append_of_eq = @BitVec.setWidth_append_of_eq

Instances For

source

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

abbrev BitVec.truncate_cons {w : Nat} {a : Bool} {x : BitVec w} :

setWidth w (cons a x) = x

Equations

@BitVec.truncate_cons = @BitVec.setWidth_cons

Instances For

source

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

abbrev BitVec.truncate_succ {w i : Nat} (x : BitVec w) :

setWidth (i + 1) x = cons (x.getLsbD i) (setWidth i x)

Equations

@BitVec.truncate_succ = @BitVec.setWidth_succ

Instances For

source

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

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

setWidth i (x + y) = setWidth i x + setWidth i y

Equations

@BitVec.truncate_add = @BitVec.setWidth_add

Instances For

source

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

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

setWidth w (setWidth (i + 1) x) = setWidth w (setWidth i x)

Equations

@BitVec.zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsbD_false = @BitVec.setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false

Instances For

source

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

abbrev BitVec.zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsbD_true {w : Nat} {x : BitVec w} {i : Nat} (hx : x.getLsbD i = true) :

setWidth w (setWidth (i + 1) x) = setWidth w (setWidth i x) ||| twoPow w i

Equations

@BitVec.zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsbD_true = @BitVec.setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true

Instances For

source

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

abbrev BitVec.and_one_eq_zeroExtend_ofBool_getLsbD {w : Nat} {x : BitVec w} :

x &&& 1#w = setWidth w (ofBool (x.getLsbD 0))

Equations

@BitVec.and_one_eq_zeroExtend_ofBool_getLsbD = @BitVec.and_one_eq_setWidth_ofBool_getLsbD

Instances For

source

@[reducible, inline, deprecated BitVec.msb_sshiftRight (since := "2024-10-03")]

abbrev BitVec.sshiftRight_msb_eq_msb {w n : Nat} {x : BitVec w} :

(x.sshiftRight n).msb = x.msb

Equations

@BitVec.sshiftRight_msb_eq_msb = @BitVec.msb_sshiftRight

Instances For

source

@[reducible, inline, deprecated BitVec.shiftLeft_zero (since := "2024-10-27")]

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

x <<< 0 = x

Equations

@BitVec.shiftLeft_zero_eq = @BitVec.shiftLeft_zero

Instances For

source

@[reducible, inline, deprecated BitVec.ushiftRight_zero (since := "2024-10-27")]

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

x >>> 0 = x

Equations

@BitVec.ushiftRight_zero_eq = @BitVec.ushiftRight_zero

Instances For

source

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

abbrev BitVec.replicate_zero_eq {w : Nat} {x : BitVec w} :

replicate 0 x = 0#0

Equations

@BitVec.replicate_zero_eq = @BitVec.replicate_zero

Instances For

source

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

abbrev BitVec.replicate_succ_eq {w n : Nat} {x : BitVec w} :

replicate (n + 1) x = BitVec.cast ⋯ (x ++ replicate n x)

Equations

@BitVec.replicate_succ_eq = @BitVec.replicate_succ

Instances For

msb #

cast #

toInt/ofInt #

sle/slt #

setWidth, zeroExtend and truncate #

extractLsb #

Condition 1: i < len #

Condition 2: start + len - i ≤ w #

allOnes #

or #

and #

xor #

not #

cast #

shiftLeft #

shiftLeft reductions from BitVec to Nat #

ushiftRight #

ushiftRight reductions from BitVec to Nat #

sshiftRight #

sshiftRight reductions from BitVec to Nat #

signExtend #

append #

rev #

cons #

concat #

shiftConcat #

add #

sub/neg #

add self #

fill #

mul #

pow #

le and lt #

udiv #

umod #

smtUDiv #

sdiv #

smtSDiv #

srem #

smod #

ofBoolList #

Rotate Left #

Rotate Right #

intMin #

intMax #

Non-overflow theorems #

neg #

abs #

Reverse #

Decidable quantifiers #

Deprecations #

Condition 1: `i < len` #

Condition 2: `start + len - i ≤ w` #