Init.Data.BitVec.Lemmas

source

theorem BitVec.ofFin_eq_ofNat {w : Nat} {x : Nat} {lt : x < 2 ^ w} :

{ toFin := { val := x, isLt := lt } } = x#w

This normalized a bitvec using ofFin to ofNat.

source

theorem BitVec.eq_of_toNat_eq {n : Nat} {i : BitVec n} {j : BitVec n} :

BitVec.toNat i = BitVec.toNat j → i = j

Prove equality of bitvectors in terms of nat operations.

source

@[simp]

theorem BitVec.val_toFin {w : Nat} (x : BitVec w) :

↑x.toFin = BitVec.toNat x

source

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

x = y ↔ BitVec.toNat x = BitVec.toNat y

source

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

x ≠ y ↔ BitVec.toNat x ≠ BitVec.toNat y

source

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

BitVec.toNat x < 2 ^ n

source

theorem BitVec.testBit_toNat {w : Nat} {i : Nat} (x : BitVec w) :

Nat.testBit (BitVec.toNat x) i = BitVec.getLsb x i

source

@[simp]

theorem BitVec.getLsb_ofFin {n : Nat} (x : Fin (2 ^ n)) (i : Nat) :

BitVec.getLsb { toFin := x } i = Nat.testBit (↑x) i

source

@[simp]

theorem BitVec.getLsb_ge {w : Nat} (x : BitVec w) (i : Nat) (ge : i ≥ w) :

BitVec.getLsb x i = false

source

theorem BitVec.lt_of_getLsb {w : Nat} (x : BitVec w) (i : Nat) :

BitVec.getLsb x i = true → i < w

source

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

x = y

source

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

x = y

source

@[simp]

theorem BitVec.of_length_zero {x : BitVec 0} :

x = 0#0

source

theorem BitVec.eq_of_toFin_eq {w : Nat} {x : BitVec w} {y : BitVec w} :

x.toFin = y.toFin → x = y

source

@[simp]

theorem BitVec.toNat_ofBool (b : Bool) :

BitVec.toNat (BitVec.ofBool b) = Bool.toNat b

source

theorem BitVec.ofNat_one (n : Nat) :

n#1 = BitVec.ofBool (decide (n % 2 = 1))

source

theorem BitVec.ofBool_eq_iff_eq (b : Bool) (b' : Bool) :

BitVec.ofBool b = BitVec.ofBool b' ↔ b = b'

source

@[simp]

theorem BitVec.toNat_ofFin {n : Nat} (x : Fin (2 ^ n)) :

BitVec.toNat { toFin := x } = ↑x

source

@[simp]

theorem BitVec.toNat_ofNatLt {w : Nat} (x : Nat) (p : x < 2 ^ w) :

BitVec.toNat x#'p = x

source

@[simp]

theorem BitVec.getLsb_ofNatLt {n : Nat} (x : Nat) (lt : x < 2 ^ n) (i : Nat) :

BitVec.getLsb (x#'lt) i = Nat.testBit x i

source

@[simp]

theorem BitVec.toNat_ofNat (x : Nat) (w : Nat) :

BitVec.toNat x#w = x % 2 ^ w

source

theorem BitVec.getLsb_ofNat (n : Nat) (x : Nat) (i : Nat) :

BitVec.getLsb (x#n) i = (decide (i < n) && Nat.testBit x i)

source

@[simp, deprecated BitVec.toNat_ofNat]

theorem BitVec.toNat_zero (n : Nat) :

BitVec.toNat 0#n = 0

source

@[simp]

theorem BitVec.getLsb_zero {w : Nat} {i : Nat} :

BitVec.getLsb (0#w) i = false

source

@[simp]

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

BitVec.toNat x % 2 ^ n = BitVec.toNat x

msb #

source

@[simp]

theorem BitVec.msb_zero {w : Nat} :

BitVec.msb 0#w = false

source

theorem BitVec.msb_eq_getLsb_last {w : Nat} (x : BitVec w) :

BitVec.msb x = BitVec.getLsb x (w - 1)

source

theorem BitVec.getLsb_last {w : Nat} (x : BitVec w) :

BitVec.getLsb x (w - 1) = decide (2 ^ (w - 1) ≤ BitVec.toNat x)

source

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

BitVec.getLsb x w = decide (2 ^ w ≤ BitVec.toNat x)

source

theorem BitVec.msb_eq_decide {w : Nat} (x : BitVec w) :

BitVec.msb x = decide (2 ^ (w - 1) ≤ BitVec.toNat x)

source

theorem BitVec.toNat_ge_of_msb_true {n : Nat} {x : BitVec n} (p : BitVec.msb x = true) :

BitVec.toNat x ≥ 2 ^ (n - 1)

cast #

source

@[simp]

theorem BitVec.toNat_cast {w : Nat} {v : Nat} (h : w = v) (x : BitVec w) :

BitVec.toNat (BitVec.cast h x) = BitVec.toNat x

source

@[simp]

theorem BitVec.toFin_cast {w : Nat} {v : Nat} (h : w = v) (x : BitVec w) :

(BitVec.cast h x).toFin = Fin.cast ⋯ x.toFin

source

@[simp]

theorem BitVec.getLsb_cast {w : Nat} {v : Nat} {i : Nat} (h : w = v) (x : BitVec w) :

BitVec.getLsb (BitVec.cast h x) i = BitVec.getLsb x i

source

@[simp]

theorem BitVec.getMsb_cast {w : Nat} {v : Nat} {i : Nat} (h : w = v) (x : BitVec w) :

BitVec.getMsb (BitVec.cast h x) i = BitVec.getMsb x i

source

@[simp]

theorem BitVec.msb_cast {w : Nat} {v : Nat} (h : w = v) (x : BitVec w) :

BitVec.msb (BitVec.cast h x) = BitVec.msb x

toInt/ofInt #

source

theorem BitVec.toInt_eq_toNat_cond {n : Nat} (i : BitVec n) :

BitVec.toInt i = if 2 * BitVec.toNat i < 2 ^ n then ↑(BitVec.toNat i) else ↑(BitVec.toNat i) - ↑(2 ^ n)

Prove equality of bitvectors in terms of nat operations.

source

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

BitVec.toInt x = Int.bmod (↑(BitVec.toNat x)) (2 ^ n)

source

theorem BitVec.eq_of_toInt_eq {n : Nat} {i : BitVec n} {j : BitVec n} :

BitVec.toInt i = BitVec.toInt j → i = j

Prove equality of bitvectors in terms of nat operations.

source

@[simp]

theorem BitVec.toNat_ofInt {n : Nat} (i : Int) :

BitVec.toNat (BitVec.ofInt n i) = Int.toNat (i % ↑(2 ^ n))

source

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

BitVec.toInt x#n = Int.bmod (↑x) (2 ^ n)

source

@[simp]

theorem BitVec.toInt_ofInt {n : Nat} (i : Int) :

BitVec.toInt (BitVec.ofInt n i) = Int.bmod i (2 ^ n)

zeroExtend and truncate #

source

@[simp]

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

BitVec.toNat (BitVec.zeroExtend' p x) = BitVec.toNat x

source

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

BitVec.toNat (BitVec.zeroExtend i x) = BitVec.toNat x % 2 ^ i

source

@[simp]

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

BitVec.toNat (BitVec.truncate i x) = BitVec.toNat x % 2 ^ i

source

@[simp]

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

BitVec.zeroExtend n x = x

source

@[simp]

theorem BitVec.zeroExtend_zero (m : Nat) (n : Nat) :

BitVec.zeroExtend m 0#n = 0#m

source

@[simp]

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

BitVec.truncate n x = x

source

@[simp]

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

(BitVec.toNat x)#m = BitVec.truncate m x

source

theorem BitVec.toNat_eq_nat {w : Nat} (x : BitVec w) (y : Nat) :

BitVec.toNat x = y ↔ y < 2 ^ w ∧ x = y#w

Moves one-sided left toNat equality to BitVec equality.

source

theorem BitVec.nat_eq_toNat {w : Nat} (x : BitVec w) (y : Nat) :

y = BitVec.toNat x ↔ y < 2 ^ w ∧ x = y#w

Moves one-sided right toNat equality to BitVec equality.

source

@[simp]

theorem BitVec.getLsb_zeroExtend' {m : Nat} {n : Nat} (ge : m ≥ n) (x : BitVec n) (i : Nat) :

BitVec.getLsb (BitVec.zeroExtend' ge x) i = BitVec.getLsb x i

source

@[simp]

theorem BitVec.getLsb_zeroExtend {n : Nat} (m : Nat) (x : BitVec n) (i : Nat) :

BitVec.getLsb (BitVec.zeroExtend m x) i = (decide (i < m) && BitVec.getLsb x i)

source

@[simp]

theorem BitVec.getLsb_truncate {n : Nat} (m : Nat) (x : BitVec n) (i : Nat) :

BitVec.getLsb (BitVec.truncate m x) i = (decide (i < m) && BitVec.getLsb x i)

source

@[simp]

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

BitVec.zeroExtend k (BitVec.zeroExtend l x) = BitVec.zeroExtend k x

source

@[simp]

theorem BitVec.truncate_truncate_of_le {w : Nat} {k : Nat} {l : Nat} (x : BitVec w) (h : k ≤ l) :

BitVec.truncate k (BitVec.truncate l x) = BitVec.truncate k x

source

theorem BitVec.msb_zeroExtend {w : Nat} {v : Nat} (x : BitVec w) :

BitVec.msb (BitVec.zeroExtend v x) = (decide (0 < v) && BitVec.getLsb x (v - 1))

extractLsb #

source

@[simp]

theorem BitVec.extractLsb_ofFin {n : Nat} (x : Fin (2 ^ n)) (hi : Nat) (lo : Nat) :

BitVec.extractLsb hi lo { toFin := x } = (↑x >>> lo)#(hi - lo + 1)

source

@[simp]

theorem BitVec.extractLsb_ofNat (x : Nat) (n : Nat) (hi : Nat) (lo : Nat) :

BitVec.extractLsb hi lo x#n = ((x % 2 ^ n) >>> lo)#(hi - lo + 1)

source

@[simp]

theorem BitVec.extractLsb'_toNat {n : Nat} (s : Nat) (m : Nat) (x : BitVec n) :

BitVec.toNat (BitVec.extractLsb' s m x) = BitVec.toNat x >>> s % 2 ^ m

source

@[simp]

theorem BitVec.extractLsb_toNat {n : Nat} (hi : Nat) (lo : Nat) (x : BitVec n) :

BitVec.toNat (BitVec.extractLsb hi lo x) = BitVec.toNat x >>> lo % 2 ^ (hi - lo + 1)

source

@[simp]

theorem BitVec.getLsb_extract {n : Nat} (hi : Nat) (lo : Nat) (x : BitVec n) (i : Nat) :

BitVec.getLsb (BitVec.extractLsb hi lo x) i = (decide (i ≤ hi - lo) && BitVec.getLsb x (lo + i))

allOnes #

source

@[simp]

theorem BitVec.toNat_allOnes {v : Nat} :

BitVec.toNat (BitVec.allOnes v) = 2 ^ v - 1

source

@[simp]

theorem BitVec.getLsb_allOnes {v : Nat} {i : Nat} :

BitVec.getLsb (BitVec.allOnes v) i = decide (i < v)

or #

source

@[simp]

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

BitVec.toNat (x ||| y) = BitVec.toNat x ||| BitVec.toNat y

source

@[simp]

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

(x ||| y).toFin = x.toFin ||| y.toFin

source

@[simp]

theorem BitVec.getLsb_or {v : Nat} {i : Nat} {x : BitVec v} {y : BitVec v} :

BitVec.getLsb (x ||| y) i = (BitVec.getLsb x i || BitVec.getLsb y i)

and #

source

@[simp]

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

BitVec.toNat (x &&& y) = BitVec.toNat x &&& BitVec.toNat y

source

@[simp]

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

(x &&& y).toFin = x.toFin &&& y.toFin

source

@[simp]

theorem BitVec.getLsb_and {v : Nat} {i : Nat} {x : BitVec v} {y : BitVec v} :

BitVec.getLsb (x &&& y) i = (BitVec.getLsb x i && BitVec.getLsb y i)

xor #

source

@[simp]

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

BitVec.toNat (x ^^^ y) = BitVec.toNat x ^^^ BitVec.toNat y

source

@[simp]

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

(x ^^^ y).toFin = x.toFin ^^^ y.toFin

source

@[simp]

theorem BitVec.getLsb_xor {v : Nat} {i : Nat} {x : BitVec v} {y : BitVec v} :

BitVec.getLsb (x ^^^ y) i = xor (BitVec.getLsb x i) (BitVec.getLsb y i)

not #

source

theorem BitVec.not_def {v : Nat} {x : BitVec v} :

~~~x = BitVec.allOnes v ^^^ x

source

@[simp]

theorem BitVec.toNat_not {v : Nat} {x : BitVec v} :

BitVec.toNat (~~~x) = 2 ^ v - 1 - BitVec.toNat x

source

@[simp]

theorem BitVec.toFin_not {w : Nat} (x : BitVec w) :

(~~~x).toFin = Fin.rev x.toFin

source

@[simp]

theorem BitVec.getLsb_not {v : Nat} {i : Nat} {x : BitVec v} :

BitVec.getLsb (~~~x) i = (decide (i < v) && !BitVec.getLsb x i)

shiftLeft #

source

@[simp]

theorem BitVec.toNat_shiftLeft {v : Nat} {n : Nat} {x : BitVec v} :

BitVec.toNat (x <<< n) = BitVec.toNat x <<< n % 2 ^ v

source

@[simp]

theorem BitVec.toFin_shiftLeft {w : Nat} {n : Nat} (x : BitVec w) :

(x <<< n).toFin = Fin.ofNat' (BitVec.toNat x <<< n) ⋯

source

@[simp]

theorem BitVec.getLsb_shiftLeft {m : Nat} {i : Nat} (x : BitVec m) (n : Nat) :

BitVec.getLsb (x <<< n) i = (decide (i < m) && !decide (i < n) && BitVec.getLsb x (i - n))

source

theorem BitVec.shiftLeftZeroExtend_eq {w : Nat} {n : Nat} {x : BitVec w} :

BitVec.shiftLeftZeroExtend x n = BitVec.zeroExtend (w + n) x <<< n

source

@[simp]

theorem BitVec.getLsb_shiftLeftZeroExtend {m : Nat} {i : Nat} (x : BitVec m) (n : Nat) :

BitVec.getLsb (BitVec.shiftLeftZeroExtend x n) i = (!decide (i < n) && BitVec.getLsb x (i - n))

ushiftRight #

source

@[simp]

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

BitVec.toNat (x >>> i) = BitVec.toNat x >>> i

source

@[simp]

theorem BitVec.getLsb_ushiftRight {n : Nat} (x : BitVec n) (i : Nat) (j : Nat) :

BitVec.getLsb (x >>> i) j = BitVec.getLsb x (i + j)

append #

source

theorem BitVec.append_def {v : Nat} {w : Nat} (x : BitVec v) (y : BitVec w) :

x ++ y = BitVec.shiftLeftZeroExtend x w ||| BitVec.zeroExtend' ⋯ y

source

@[simp]

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

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

source

@[simp]

theorem BitVec.getLsb_append {n : Nat} {m : Nat} {i : Nat} {v : BitVec n} {w : BitVec m} :

BitVec.getLsb (v ++ w) i = bif decide (i < m) then BitVec.getLsb w i else BitVec.getLsb v (i - m)

rev #

source

theorem BitVec.getLsb_rev {w : Nat} (x : BitVec w) (i : Fin w) :

BitVec.getLsb x ↑(Fin.rev i) = BitVec.getMsb x ↑i

source

theorem BitVec.getMsb_rev {w : Nat} (x : BitVec w) (i : Fin w) :

BitVec.getMsb x ↑(Fin.rev i) = BitVec.getLsb x ↑i

cons #

source

@[simp]

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

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

source

@[simp]

theorem BitVec.getLsb_cons (b : Bool) {n : Nat} (x : BitVec n) (i : Nat) :

BitVec.getLsb (BitVec.cons b x) i = if i = n then b else BitVec.getLsb x i

source

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

BitVec.truncate (i + 1) x = BitVec.cons (BitVec.getLsb x i) (BitVec.truncate i x)

concat #

source

@[simp]

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

BitVec.toNat (BitVec.concat x b) = BitVec.toNat x * 2 + Bool.toNat b

source

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

BitVec.getLsb (BitVec.concat x b) i = if i = 0 then b else BitVec.getLsb x (i - 1)

source

@[simp]

theorem BitVec.getLsb_concat_zero :

∀ {w : Nat} {x : BitVec w} {b : Bool}, BitVec.getLsb (BitVec.concat x b) 0 = b

source

@[simp]

theorem BitVec.getLsb_concat_succ :

∀ {w : Nat} {x : BitVec w} {b : Bool} {i : Nat}, BitVec.getLsb (BitVec.concat x b) (i + 1) = BitVec.getLsb x i

add #

source

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

x + y = (BitVec.toNat x + BitVec.toNat y)#n

source

@[simp]

theorem BitVec.toNat_add {w : Nat} (x : BitVec w) (y : BitVec w) :

BitVec.toNat (x + y) = (BitVec.toNat x + BitVec.toNat y) % 2 ^ w

Definition of bitvector addition as a nat.

source

@[simp]

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

@[simp]

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

x#n + y#n = (x + y)#n

source

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

x + y + z = x + (y + z)

source

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

x + y = y + x

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

sub/neg #

source

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

x - y = (BitVec.toNat x + (2 ^ n - BitVec.toNat y))#n

source

@[simp]

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

BitVec.toNat (x - y) = (BitVec.toNat x + (2 ^ n - BitVec.toNat y)) % 2 ^ n

source

@[simp]

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

(x - y).toFin = x.toFin - y.toFin

source

@[simp]

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

{ toFin := x } - y = { toFin := x - y.toFin }

source

@[simp]

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 : Nat) (y : Nat) :

x#n - y#n = (x + (2 ^ n - y % 2 ^ n))#n

source

@[simp]

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

x - 0#n = 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) :

BitVec.toNat (-x) = (2 ^ n - BitVec.toNat x) % 2 ^ n

source

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

x - y = x + -y

source

@[simp]

theorem BitVec.neg_zero (n : Nat) :

-0#n = 0#n

source

theorem BitVec.add_sub_cancel {w : Nat} (x : BitVec w) (y : BitVec w) :

x + y - y = x

source

theorem BitVec.negOne_eq_allOnes {w : Nat} :

-1#w = BitVec.allOnes w

mul #

source

theorem BitVec.mul_def {n : Nat} {x : BitVec n} {y : BitVec n} :

x * y = { toFin := x.toFin * y.toFin }

source

@[simp]

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

BitVec.toNat (x * y) = BitVec.toNat x * BitVec.toNat y % 2 ^ n

source

@[simp]

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

(x * y).toFin = x.toFin * y.toFin

source

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

x * y = y * x

source

instance BitVec.instCommutativeBitVecHMulInstHMulInstMulBitVec {w : Nat} :

Std.Commutative fun (x y : BitVec w) => x * y

Equations

⋯ = ⋯

source

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

x * y * z = x * (y * z)

source

instance BitVec.instAssociativeBitVecHMulInstHMulInstMulBitVec {w : Nat} :

Std.Associative fun (x y : BitVec w) => x * y

Equations

⋯ = ⋯

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.instLawfulCommIdentityBitVecHMulInstHMulInstMulBitVecOfNatOfNatNatInstOfNatNatInstCommutativeBitVecHMulInstHMulInstMulBitVec {w : Nat} :

Std.LawfulCommIdentity (fun (x y : BitVec w) => x * y) 1#w

Equations

⋯ = ⋯

le and lt #

source

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

x ≤ y ↔ BitVec.toNat x ≤ BitVec.toNat y

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 : Nat} (x : Nat) (y : Nat) :

x#n ≤ y#n ↔ x % 2 ^ n ≤ y % 2 ^ n

source

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

x < y ↔ BitVec.toNat x < BitVec.toNat y

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 : Nat} (x : Nat) (y : Nat) :

x#n < y#n ↔ x % 2 ^ n < y % 2 ^ n

source

theorem BitVec.lt_of_le_ne {n : Nat} (x : BitVec n) (y : BitVec n) (h1 : x ≤ y) (h2 : ¬x = y) :

x < y

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 = (2 ^ w - 1)#w

Instances For

source

theorem BitVec.getLsb_intMax_eq {i : Nat} (w : Nat) :

BitVec.getLsb (BitVec.intMax w) i = decide (i < w)

source

theorem BitVec.toNat_intMax_eq {w : Nat} :

BitVec.toNat (BitVec.intMax w) = 2 ^ w - 1