Documentation

Init.Data.BitVec.Lemmas

@[simp]
theorem BitVec.getLsbD_ofFin {n : Nat} (x : Fin (2 ^ n)) (i : Nat) :
{ toFin := x }.getLsbD i = (↑x).testBit i
@[simp]
theorem BitVec.getLsbD_ge {w : Nat} (x : BitVec w) (i : Nat) (ge : w i) :
x.getLsbD i = false
@[simp]
theorem BitVec.getMsbD_ge {w : Nat} (x : BitVec w) (i : Nat) (ge : w i) :
x.getMsbD i = false
theorem BitVec.lt_of_getLsbD {w : Nat} {x : BitVec w} {i : Nat} :
x.getLsbD i = truei < w
theorem BitVec.lt_of_getMsbD {w : Nat} {x : BitVec w} {i : Nat} :
x.getMsbD i = truei < w
@[simp]
theorem BitVec.getElem?_eq_getElem {w : Nat} {l : BitVec w} {n : Nat} (h : n < w) :
l[n]? = some l[n]
theorem BitVec.getElem?_eq_some {w : Nat} {n : Nat} {a : Bool} {l : BitVec w} :
l[n]? = some a ∃ (h : n < w), l[n] = a
@[simp]
theorem BitVec.getElem?_eq_none_iff {w : Nat} {n : Nat} {l : BitVec w} :
l[n]? = none w n
theorem BitVec.getElem?_eq_none {w : Nat} {n : Nat} {l : BitVec w} (h : w n) :
l[n]? = none
theorem BitVec.getElem?_eq {w : Nat} (l : BitVec w) (i : Nat) :
l[i]? = if h : i < w then some l[i] else none
@[simp]
theorem BitVec.some_getElem_eq_getElem? {w : Nat} (l : BitVec w) (i : Nat) (h : i < w) :
some l[i] = l[i]? True
@[simp]
theorem BitVec.getElem?_eq_some_getElem {w : Nat} (l : BitVec w) (i : Nat) (h : i < w) :
l[i]? = some l[i] True
theorem BitVec.getElem_eq_iff {w : Nat} {x : Bool} {l : BitVec w} {n : Nat} {h : n < w} :
l[n] = x l[n]? = some x
theorem BitVec.getElem_eq_getElem? {w : Nat} (l : BitVec w) (i : Nat) (h : i < w) :
l[i] = l[i]?.get
theorem BitVec.getLsbD_eq_getElem?_getD {w : Nat} {x : BitVec w} {i : Nat} :
x.getLsbD i = x[i]?.getD false
theorem BitVec.ofFin_eq_ofNat {w : Nat} {x : Nat} {lt : x < 2 ^ w} :
{ toFin := x, lt } = BitVec.ofNat w x

This normalized a bitvec using ofFin to ofNat.

theorem BitVec.eq_of_toNat_eq {n : Nat} {x : BitVec n} {y : BitVec n} :
x.toNat = y.toNatx = y

Prove equality of bitvectors in terms of nat operations.

@[simp]
theorem BitVec.val_toFin {w : Nat} (x : BitVec w) :
x.toFin = x.toNat
theorem BitVec.toNat_eq {n : Nat} {x : BitVec n} {y : BitVec n} :
x = y x.toNat = y.toNat
theorem BitVec.toNat_ne {n : Nat} {x : BitVec n} {y : BitVec n} :
x y x.toNat y.toNat
theorem BitVec.testBit_toNat {w : Nat} {i : Nat} (x : BitVec w) :
x.toNat.testBit i = x.getLsbD i
theorem BitVec.getMsb'_eq_getLsb' {w : Nat} (x : BitVec w) (i : Fin w) :
x.getMsb' i = x.getLsb' w - 1 - i,
theorem BitVec.getMsb?_eq_getLsb? {w : Nat} (x : BitVec w) (i : Nat) :
x.getMsb? i = if i < w then x.getLsb? (w - 1 - i) else none
theorem BitVec.getMsbD_eq_getLsbD {w : Nat} (x : BitVec w) (i : Nat) :
x.getMsbD i = (decide (i < w) && x.getLsbD (w - 1 - i))
theorem BitVec.getLsbD_eq_getMsbD {w : Nat} (x : BitVec w) (i : Nat) :
x.getLsbD i = (decide (i < w) && x.getMsbD (w - 1 - i))
@[simp]
theorem BitVec.getLsb?_ge {w : Nat} (x : BitVec w) (i : Nat) (ge : w i) :
x[i]? = none
@[simp]
theorem BitVec.getMsb?_ge {w : Nat} (x : BitVec w) (i : Nat) (ge : w i) :
x.getMsb? i = none
theorem BitVec.lt_of_getLsb?_eq_some {w : Nat} {b : Bool} (x : BitVec w) (i : Nat) :
x[i]? = some bi < w
theorem BitVec.lt_of_getMsb?_eq_some {w : Nat} {b : Bool} (x : BitVec w) (i : Nat) :
x.getMsb? i = some bi < w
theorem BitVec.lt_of_getLsb?_isSome {w : Nat} (x : BitVec w) (i : Nat) :
x[i]?.isSome = truei < w
theorem BitVec.lt_of_getMsb?_isSome {w : Nat} (x : BitVec w) (i : Nat) :
(x.getMsb? i).isSome = truei < w
theorem BitVec.getMsbD_eq_getMsb?_getD {w : Nat} (x : BitVec w) (i : Nat) :
x.getMsbD i = (x.getMsb? i).getD false
theorem BitVec.eq_of_getLsbD_eq_iff {w : Nat} {x : BitVec w} {y : BitVec w} :
x = y ∀ (i : Fin w), x.getLsbD i = y.getLsbD i
theorem BitVec.eq_of_getLsbD_eq {w : Nat} {x : BitVec w} {y : BitVec w} (pred : ∀ (i : Fin w), x.getLsbD i = y.getLsbD i) :
x = y
theorem BitVec.eq_of_getMsbD_eq {w : Nat} {x : BitVec w} {y : BitVec w} (pred : ∀ (i : Fin w), x.getMsbD i = y.getMsbD i) :
x = y
theorem BitVec.of_length_zero {x : BitVec 0} :
x = 0#0
theorem BitVec.toNat_zero_length (x : BitVec 0) :
x.toNat = 0
theorem BitVec.getLsbD_zero_length {i : Nat} (x : BitVec 0) :
x.getLsbD i = false
theorem BitVec.getMsbD_zero_length {i : Nat} (x : BitVec 0) :
x.getMsbD i = false
theorem BitVec.toNat_of_zero_length {w : Nat} (h : w = 0) (x : BitVec w) :
x.toNat = 0
theorem BitVec.getLsbD_of_zero_length {w : Nat} {i : Nat} (h : w = 0) (x : BitVec w) :
x.getLsbD i = false
theorem BitVec.getMsbD_of_zero_length {w : Nat} {i : Nat} (h : w = 0) (x : BitVec w) :
x.getMsbD i = false
theorem BitVec.msb_of_zero_length {w : Nat} (h : w = 0) (x : BitVec w) :
x.msb = false
theorem BitVec.eq_of_toFin_eq {w : Nat} {x : BitVec w} {y : BitVec w} :
x.toFin = y.toFinx = y
@[simp]
theorem BitVec.toNat_ofBool (b : Bool) :
(BitVec.ofBool b).toNat = b.toNat
@[simp]
theorem BitVec.msb_ofBool (b : Bool) :
(BitVec.ofBool b).msb = b
@[simp]
theorem BitVec.toNat_ofFin {n : Nat} (x : Fin (2 ^ n)) :
{ toFin := x }.toNat = x
@[simp]
theorem BitVec.toNat_ofNatLt {w : Nat} (x : Nat) (p : x < 2 ^ w) :
(x#'p).toNat = x
@[simp]
theorem BitVec.getLsbD_ofNatLt {n : Nat} (x : Nat) (lt : x < 2 ^ n) (i : Nat) :
(x#'lt).getLsbD i = x.testBit i
@[simp]
theorem BitVec.toNat_ofNat (x : Nat) (w : Nat) :
(BitVec.ofNat w x).toNat = x % 2 ^ w
@[simp]
theorem BitVec.toFin_ofNat {w : Nat} (x : Nat) :
(BitVec.ofNat w x).toFin = Fin.ofNat' (2 ^ w) x
theorem BitVec.getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) :
(BitVec.ofNat n x).getLsbD i = (decide (i < n) && x.testBit i)
@[simp]
theorem BitVec.getLsbD_zero {w : Nat} {i : Nat} :
(0#w).getLsbD i = false
@[simp]
theorem BitVec.getElem_zero {i : Nat} {w : Nat} (h : i < w) :
(0#w)[i] = false
@[simp]
theorem BitVec.getMsbD_zero {w : Nat} {i : Nat} :
(0#w).getMsbD i = false
@[simp]
theorem BitVec.toNat_mod_cancel {n : Nat} (x : BitVec n) :
x.toNat % 2 ^ n = x.toNat
@[simp]
theorem BitVec.toNat_mod_cancel' {n : Nat} {x : BitVec n} :
x.toNat % (2 ^ n) = x.toNat
@[simp]
theorem BitVec.sub_toNat_mod_cancel {w : Nat} {x : BitVec w} (h : ¬x = 0#w) :
(2 ^ w - x.toNat) % 2 ^ w = 2 ^ w - x.toNat
@[simp]
theorem BitVec.sub_sub_toNat_cancel {w : Nat} {x : BitVec w} :
2 ^ w - (2 ^ w - x.toNat) = x.toNat
@[simp]
theorem BitVec.getElem_zero_ofNat_zero {w : Nat} (i : Nat) (h : i < w) :
(0#w)[i] = false
@[simp]
theorem BitVec.getElem_zero_ofNat_one {w : Nat} (h : 0 < w) :
(1#w)[0] = true
theorem BitVec.getElem?_zero_ofNat_zero {w : Nat} :
(0#(w + 1))[0]? = some false
theorem BitVec.getElem?_zero_ofNat_one {w : Nat} :
(1#(w + 1))[0]? = some true
@[simp]
theorem BitVec.getElem?_succ_ofBool (b : Bool) (i : Nat) :
(BitVec.ofBool b)[i + 1]? = none
@[simp]
theorem BitVec.getLsbD_ofBool (b : Bool) (i : Nat) :
(BitVec.ofBool b).getLsbD i = (decide (i = 0) && b)
@[simp]
theorem BitVec.getElem_ofBool {b : Bool} {i : Nat} :
(BitVec.ofBool b)[0] = b

msb #

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

cast #

@[simp]
theorem BitVec.toNat_cast {w : Nat} {v : Nat} (h : w = v) (x : BitVec w) :
(BitVec.cast h x).toNat = x.toNat
@[simp]
theorem BitVec.toFin_cast {w : Nat} {v : Nat} (h : w = v) (x : BitVec w) :
(BitVec.cast h x).toFin = Fin.cast x.toFin
@[simp]
theorem BitVec.getLsbD_cast {w : Nat} {v : Nat} {i : Nat} (h : w = v) (x : BitVec w) :
(BitVec.cast h x).getLsbD i = x.getLsbD i
@[simp]
theorem BitVec.getMsbD_cast {w : Nat} {v : Nat} {i : Nat} (h : w = v) (x : BitVec w) :
(BitVec.cast h x).getMsbD i = x.getMsbD i
@[simp]
theorem BitVec.getElem_cast {w : Nat} {v : Nat} {i : Nat} (h : w = v) (x : BitVec w) (p : i < v) :
(BitVec.cast h x)[i] = x[i]
@[simp]
theorem BitVec.msb_cast {w : Nat} {v : Nat} (h : w = v) (x : BitVec w) :
(BitVec.cast h x).msb = x.msb

toInt/ofInt #

theorem BitVec.toInt_eq_toNat_cond {n : Nat} (x : BitVec n) :
x.toInt = if 2 * x.toNat < 2 ^ n then x.toNat else x.toNat - (2 ^ n)

Prove equality of bitvectors in terms of nat operations.

theorem BitVec.msb_eq_false_iff_two_mul_lt {w : Nat} {x : BitVec w} :
x.msb = false 2 * x.toNat < 2 ^ w
theorem BitVec.msb_eq_true_iff_two_mul_ge {w : Nat} {x : BitVec w} :
x.msb = true 2 * x.toNat 2 ^ w
theorem BitVec.toInt_eq_msb_cond {w : Nat} (x : BitVec w) :
x.toInt = if x.msb = true then x.toNat - (2 ^ w) else x.toNat

Characterize x.toInt in terms of x.msb.

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

Prove equality of bitvectors in terms of nat operations.

theorem BitVec.toInt_inj {n : Nat} {x : BitVec n} {y : BitVec n} :
x.toInt = y.toInt x = y
theorem BitVec.toInt_ne {n : Nat} {x : BitVec n} {y : BitVec n} :
x.toInt y.toInt x y
@[simp]
theorem BitVec.toNat_ofInt {n : Nat} (i : Int) :
(BitVec.ofInt n i).toNat = (i % (2 ^ n)).toNat
theorem BitVec.toInt_ofNat {n : Nat} (x : Nat) :
(BitVec.ofNat n x).toInt = (↑x).bmod (2 ^ n)
@[simp]
theorem BitVec.toInt_ofInt {n : Nat} (i : Int) :
(BitVec.ofInt n i).toInt = i.bmod (2 ^ n)
@[simp]
theorem BitVec.ofInt_natCast (w : Nat) (n : Nat) :
theorem BitVec.toInt_neg_iff {w : Nat} {x : BitVec w} :
x.toInt < 0 2 ^ w 2 * x.toNat
theorem BitVec.toInt_pos_iff {w : Nat} {x : BitVec w} :
0 x.toInt 2 * x.toNat < 2 ^ w
theorem BitVec.eq_zero_or_eq_one (a : BitVec 1) :
a = 0#1 a = 1#1

setWidth, zeroExtend and truncate #

@[simp]
@[simp]
theorem BitVec.toNat_setWidth' {m : Nat} {n : Nat} (p : m n) (x : BitVec m) :
(BitVec.setWidth' p x).toNat = x.toNat
@[simp]
theorem BitVec.toNat_setWidth {n : Nat} (i : Nat) (x : BitVec n) :
(BitVec.setWidth i x).toNat = x.toNat % 2 ^ i
theorem BitVec.setWidth'_eq {w : Nat} {v : Nat} {x : BitVec w} (h : w v) :
@[simp]
theorem BitVec.setWidth_eq {n : Nat} (x : BitVec n) :
@[simp]
theorem BitVec.setWidth_zero (m : Nat) (n : Nat) :
BitVec.setWidth m 0#n = 0#m
@[simp]
theorem BitVec.ofNat_toNat {n : Nat} (m : Nat) (x : BitVec n) :
theorem BitVec.toNat_eq_nat {w : Nat} {x : BitVec w} {y : Nat} :
x.toNat = y y < 2 ^ w x = BitVec.ofNat w y

Moves one-sided left toNat equality to BitVec equality.

theorem BitVec.nat_eq_toNat {w : Nat} {x : BitVec w} {y : Nat} :
y = x.toNat y < 2 ^ w x = BitVec.ofNat w y

Moves one-sided right toNat equality to BitVec equality.

theorem BitVec.getElem_setWidth' {w : Nat} {v : Nat} (x : BitVec w) (i : Nat) (h : w v) (hi : i < v) :
(BitVec.setWidth' h x)[i] = x.getLsbD i
@[simp]
theorem BitVec.getElem_setWidth {n : Nat} (m : Nat) (x : BitVec n) (i : Nat) (h : i < m) :
(BitVec.setWidth m x)[i] = x.getLsbD i
theorem BitVec.getElem?_setWidth' {w : Nat} {v : Nat} (x : BitVec w) (i : Nat) (h : w v) :
(BitVec.setWidth' h x)[i]? = if i < v then some (x.getLsbD i) else none
theorem BitVec.getElem?_setWidth {n : Nat} (m : Nat) (x : BitVec n) (i : Nat) :
(BitVec.setWidth m x)[i]? = if i < m then some (x.getLsbD i) else none
@[simp]
theorem BitVec.getLsbD_setWidth' {m : Nat} {n : Nat} (ge : m n) (x : BitVec n) (i : Nat) :
(BitVec.setWidth' ge x).getLsbD i = x.getLsbD i
@[simp]
theorem BitVec.getMsbD_setWidth' {m : Nat} {n : Nat} (ge : m n) (x : BitVec n) (i : Nat) :
(BitVec.setWidth' ge x).getMsbD i = (decide (i m - n) && x.getMsbD (i - (m - n)))
@[simp]
theorem BitVec.getLsbD_setWidth {n : Nat} (m : Nat) (x : BitVec n) (i : Nat) :
(BitVec.setWidth m x).getLsbD i = (decide (i < m) && x.getLsbD i)
@[simp]
theorem BitVec.getMsbD_setWidth_add {w : Nat} {k : Nat} {i : Nat} {x : BitVec w} (h : k i) :
(BitVec.setWidth (w + k) x).getMsbD i = x.getMsbD (i - k)
@[simp]
theorem BitVec.cast_setWidth {v : Nat} {v' : Nat} {w : Nat} (h : v = v') (x : BitVec w) :
@[simp]
theorem BitVec.setWidth_setWidth_of_le {w : Nat} {k : Nat} {l : Nat} (x : BitVec w) (h : k l) :
@[simp]
theorem BitVec.setWidth_cast {w : Nat} {v : Nat} {x : BitVec w} {k : Nat} {h : w = v} :
theorem BitVec.msb_setWidth {w : Nat} {v : Nat} (x : BitVec w) :
(BitVec.setWidth v x).msb = (decide (0 < v) && x.getLsbD (v - 1))
theorem BitVec.msb_setWidth' {w : Nat} {v : Nat} (x : BitVec w) (h : w v) :
(BitVec.setWidth' h x).msb = (decide (0 < v) && x.getLsbD (v - 1))
theorem BitVec.msb_setWidth'' {w : Nat} {k : Nat} (x : BitVec w) :
(BitVec.setWidth (k + 1) x).msb = x.getLsbD k

zero extending a bitvector to width 1 equals the boolean of the lsb.

theorem BitVec.setWidth_ofNat_one_eq_ofNat_one_of_lt {v : Nat} {w : Nat} (hv : 0 < v) :
BitVec.setWidth w 1#v = 1#w

Zero extending 1#v to 1#w equals 1#w when v > 0.

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

Truncating to width 1 produces a bitvector equal to the least significant bit.

@[simp]
theorem BitVec.setWidth_ofNat_of_le {v : Nat} {w : Nat} (h : v w) (x : Nat) :

extractLsb #

@[simp]
theorem BitVec.extractLsb_ofFin {n : Nat} (x : Fin (2 ^ n)) (hi : Nat) (lo : Nat) :
BitVec.extractLsb hi lo { toFin := x } = BitVec.ofNat (hi - lo + 1) (x >>> lo)
@[simp]
theorem BitVec.extractLsb_ofNat (x : Nat) (n : Nat) (hi : Nat) (lo : Nat) :
BitVec.extractLsb hi lo (BitVec.ofNat n x) = BitVec.ofNat (hi - lo + 1) ((x % 2 ^ n) >>> lo)
@[simp]
theorem BitVec.extractLsb'_toNat {n : Nat} (s : Nat) (m : Nat) (x : BitVec n) :
(BitVec.extractLsb' s m x).toNat = x.toNat >>> s % 2 ^ m
@[simp]
theorem BitVec.extractLsb_toNat {n : Nat} (hi : Nat) (lo : Nat) (x : BitVec n) :
(BitVec.extractLsb hi lo x).toNat = x.toNat >>> lo % 2 ^ (hi - lo + 1)
@[simp]
theorem BitVec.getElem_extractLsb' {n : Nat} {start : Nat} {len : Nat} {x : BitVec n} {i : Nat} (h : i < len) :
(BitVec.extractLsb' start len x)[i] = x.getLsbD (start + i)
@[simp]
theorem BitVec.getLsbD_extractLsb' {n : Nat} (start : Nat) (len : Nat) (x : BitVec n) (i : Nat) :
(BitVec.extractLsb' start len x).getLsbD i = (decide (i < len) && x.getLsbD (start + i))
@[simp]
theorem BitVec.getElem_extract {n : Nat} {hi : Nat} {lo : Nat} {x : BitVec n} {i : Nat} (h : i < hi - lo + 1) :
(BitVec.extractLsb hi lo x)[i] = x.getLsbD (lo + i)
@[simp]
theorem BitVec.getLsbD_extract {n : Nat} (hi : Nat) (lo : Nat) (x : BitVec n) (i : Nat) :
(BitVec.extractLsb hi lo x).getLsbD i = (decide (i hi - lo) && x.getLsbD (lo + i))
theorem BitVec.extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start : Nat) (len : Nat) (h : len > 0) :
BitVec.extractLsb' start len x = BitVec.cast (BitVec.extractLsb (len - 1 + start) start x)

allOnes #

@[simp]
theorem BitVec.toNat_allOnes {v : Nat} :
(BitVec.allOnes v).toNat = 2 ^ v - 1
@[simp]
theorem BitVec.getLsbD_allOnes {v : Nat} {i : Nat} :
(BitVec.allOnes v).getLsbD i = decide (i < v)
@[simp]
theorem BitVec.getElem_allOnes {v : Nat} (i : Nat) (h : i < v) :
@[simp]
theorem BitVec.ofFin_add_rev {n : Nat} (x : Fin (2 ^ n)) :
{ toFin := x + x.rev } = BitVec.allOnes n

or #

@[simp]
theorem BitVec.toNat_or {v : Nat} (x : BitVec v) (y : BitVec v) :
(x ||| y).toNat = x.toNat ||| y.toNat
@[simp]
theorem BitVec.toFin_or {v : Nat} (x : BitVec v) (y : BitVec v) :
(x ||| y).toFin = x.toFin ||| y.toFin
@[simp]
theorem BitVec.getLsbD_or {v : Nat} {i : Nat} {x : BitVec v} {y : BitVec v} :
(x ||| y).getLsbD i = (x.getLsbD i || y.getLsbD i)
@[simp]
theorem BitVec.getMsbD_or {w : Nat} {i : Nat} {x : BitVec w} {y : BitVec w} :
(x ||| y).getMsbD i = (x.getMsbD i || y.getMsbD i)
@[simp]
theorem BitVec.getElem_or {w : Nat} {x : BitVec w} {y : BitVec w} {i : Nat} (h : i < w) :
(x ||| y)[i] = (x[i] || y[i])
@[simp]
theorem BitVec.msb_or {w : Nat} {x : BitVec w} {y : BitVec w} :
(x ||| y).msb = (x.msb || y.msb)
@[simp]
theorem BitVec.setWidth_or {w : Nat} {k : Nat} {x : BitVec w} {y : BitVec w} :
theorem BitVec.or_assoc {w : Nat} (x : BitVec w) (y : BitVec w) (z : BitVec w) :
x ||| y ||| z = x ||| (y ||| z)
instance BitVec.instAssociativeHOr {n : Nat} :
Std.Associative fun (x1 x2 : BitVec n) => x1 ||| x2
Equations
  • =
theorem BitVec.or_comm {w : Nat} (x : BitVec w) (y : BitVec w) :
x ||| y = y ||| x
instance BitVec.instCommutativeHOr {w : Nat} :
Std.Commutative fun (x y : BitVec w) => x ||| y
Equations
  • =
@[simp]
theorem BitVec.or_self {w : Nat} {x : BitVec w} :
x ||| x = x
instance BitVec.instIdempotentOpHOr {n : Nat} :
Std.IdempotentOp fun (x1 x2 : BitVec n) => x1 ||| x2
Equations
  • =
@[simp]
theorem BitVec.or_zero {w : Nat} {x : BitVec w} :
x ||| 0#w = x
Equations
  • =
@[simp]
theorem BitVec.zero_or {w : Nat} {x : BitVec w} :
0#w ||| x = x
@[simp]
@[simp]

and #

@[simp]
theorem BitVec.toNat_and {v : Nat} (x : BitVec v) (y : BitVec v) :
(x &&& y).toNat = x.toNat &&& y.toNat
@[simp]
theorem BitVec.toFin_and {v : Nat} (x : BitVec v) (y : BitVec v) :
(x &&& y).toFin = x.toFin &&& y.toFin
@[simp]
theorem BitVec.getLsbD_and {v : Nat} {i : Nat} {x : BitVec v} {y : BitVec v} :
(x &&& y).getLsbD i = (x.getLsbD i && y.getLsbD i)
@[simp]
theorem BitVec.getMsbD_and {w : Nat} {i : Nat} {x : BitVec w} {y : BitVec w} :
(x &&& y).getMsbD i = (x.getMsbD i && y.getMsbD i)
@[simp]
theorem BitVec.getElem_and {w : Nat} {x : BitVec w} {y : BitVec w} {i : Nat} (h : i < w) :
(x &&& y)[i] = (x[i] && y[i])
@[simp]
theorem BitVec.msb_and {w : Nat} {x : BitVec w} {y : BitVec w} :
(x &&& y).msb = (x.msb && y.msb)
@[simp]
theorem BitVec.setWidth_and {w : Nat} {k : Nat} {x : BitVec w} {y : BitVec w} :
theorem BitVec.and_assoc {w : Nat} (x : BitVec w) (y : BitVec w) (z : BitVec w) :
x &&& y &&& z = x &&& (y &&& z)
instance BitVec.instAssociativeHAnd {n : Nat} :
Std.Associative fun (x1 x2 : BitVec n) => x1 &&& x2
Equations
  • =
theorem BitVec.and_comm {w : Nat} (x : BitVec w) (y : BitVec w) :
x &&& y = y &&& x
instance BitVec.instCommutativeHAnd {w : Nat} :
Std.Commutative fun (x y : BitVec w) => x &&& y
Equations
  • =
@[simp]
theorem BitVec.and_self {w : Nat} {x : BitVec w} :
x &&& x = x
instance BitVec.instIdempotentOpHAnd {n : Nat} :
Std.IdempotentOp fun (x1 x2 : BitVec n) => x1 &&& x2
Equations
  • =
@[simp]
theorem BitVec.and_zero {w : Nat} {x : BitVec w} :
x &&& 0#w = 0#w
@[simp]
theorem BitVec.zero_and {w : Nat} {x : BitVec w} :
0#w &&& x = 0#w
@[simp]
theorem BitVec.and_allOnes {w : Nat} {x : BitVec w} :
Equations
  • =
@[simp]
theorem BitVec.allOnes_and {w : Nat} {x : BitVec w} :

xor #

@[simp]
theorem BitVec.toNat_xor {v : Nat} (x : BitVec v) (y : BitVec v) :
(x ^^^ y).toNat = x.toNat ^^^ y.toNat
@[simp]
theorem BitVec.toFin_xor {v : Nat} (x : BitVec v) (y : BitVec v) :
(x ^^^ y).toFin = x.toFin ^^^ y.toFin
@[simp]
theorem BitVec.getLsbD_xor {v : Nat} {i : Nat} {x : BitVec v} {y : BitVec v} :
(x ^^^ y).getLsbD i = (x.getLsbD i ^^ y.getLsbD i)
@[simp]
theorem BitVec.getMsbD_xor {w : Nat} {i : Nat} {x : BitVec w} {y : BitVec w} :
(x ^^^ y).getMsbD i = (x.getMsbD i ^^ y.getMsbD i)
@[simp]
theorem BitVec.getElem_xor {w : Nat} {x : BitVec w} {y : BitVec w} {i : Nat} (h : i < w) :
(x ^^^ y)[i] = (x[i] ^^ y[i])
@[simp]
theorem BitVec.msb_xor {w : Nat} {x : BitVec w} {y : BitVec w} :
(x ^^^ y).msb = (x.msb ^^ y.msb)
@[simp]
theorem BitVec.setWidth_xor {w : Nat} {k : Nat} {x : BitVec w} {y : BitVec w} :
theorem BitVec.xor_assoc {w : Nat} (x : BitVec w) (y : BitVec w) (z : BitVec w) :
x ^^^ y ^^^ z = x ^^^ (y ^^^ z)
instance BitVec.instAssociativeHXor {w : Nat} :
Std.Associative fun (x y : BitVec w) => x ^^^ y
Equations
  • =
theorem BitVec.xor_comm {w : Nat} (x : BitVec w) (y : BitVec w) :
x ^^^ y = y ^^^ x
instance BitVec.instCommutativeHXor {w : Nat} :
Std.Commutative fun (x y : BitVec w) => x ^^^ y
Equations
  • =
@[simp]
theorem BitVec.xor_self {w : Nat} {x : BitVec w} :
x ^^^ x = 0#w
@[simp]
theorem BitVec.xor_zero {w : Nat} {x : BitVec w} :
x ^^^ 0#w = x
Equations
  • =
@[simp]
theorem BitVec.zero_xor {w : Nat} {x : BitVec w} :
0#w ^^^ x = x

not #

theorem BitVec.not_def {v : Nat} {x : BitVec v} :
@[simp]
theorem BitVec.toNat_not {v : Nat} {x : BitVec v} :
(~~~x).toNat = 2 ^ v - 1 - x.toNat
@[simp]
theorem BitVec.toFin_not {w : Nat} (x : BitVec w) :
(~~~x).toFin = x.toFin.rev
@[simp]
theorem BitVec.getLsbD_not {v : Nat} {i : Nat} {x : BitVec v} :
(~~~x).getLsbD i = (decide (i < v) && !x.getLsbD i)
@[simp]
theorem BitVec.getElem_not {w : Nat} {x : BitVec w} {i : Nat} (h : i < w) :
(~~~x)[i] = !x[i]
@[simp]
theorem BitVec.setWidth_not {w : Nat} {k : Nat} {x : BitVec w} (h : k w) :
@[simp]
theorem BitVec.not_zero {n : Nat} :
@[simp]
@[simp]
theorem BitVec.xor_allOnes {w : Nat} {x : BitVec w} :
@[simp]
theorem BitVec.allOnes_xor {w : Nat} {x : BitVec w} :
@[simp]
theorem BitVec.not_not {w : Nat} {b : BitVec w} :
@[simp]
theorem BitVec.getMsb_not {w : Nat} {i : Nat} {x : BitVec w} :
(~~~x).getMsbD i = (decide (i < w) && !x.getMsbD i)
@[simp]
theorem BitVec.msb_not {w : Nat} {x : BitVec w} :
(~~~x).msb = (decide (0 < w) && !x.msb)

cast #

@[simp]
theorem BitVec.not_cast {w : Nat} {w' : Nat} {x : BitVec w} (h : w = w') :
@[simp]
theorem BitVec.and_cast {w : Nat} {w' : Nat} {x : BitVec w} {y : BitVec w} (h : w = w') :
@[simp]
theorem BitVec.or_cast {w : Nat} {w' : Nat} {x : BitVec w} {y : BitVec w} (h : w = w') :
@[simp]
theorem BitVec.xor_cast {w : Nat} {w' : Nat} {x : BitVec w} {y : BitVec w} (h : w = w') :

shiftLeft #

@[simp]
theorem BitVec.toNat_shiftLeft {v : Nat} {n : Nat} {x : BitVec v} :
(x <<< n).toNat = x.toNat <<< n % 2 ^ v
@[simp]
theorem BitVec.toFin_shiftLeft {w : Nat} {n : Nat} (x : BitVec w) :
(x <<< n).toFin = Fin.ofNat' (2 ^ w) (x.toNat <<< n)
@[simp]
theorem BitVec.shiftLeft_zero_eq {w : Nat} (x : BitVec w) :
x <<< 0 = x
@[simp]
theorem BitVec.zero_shiftLeft {w : Nat} (n : Nat) :
0#w <<< n = 0#w
@[simp]
theorem BitVec.getLsbD_shiftLeft {m : Nat} {i : Nat} (x : BitVec m) (n : Nat) :
(x <<< n).getLsbD i = (decide (i < m) && !decide (i < n) && x.getLsbD (i - n))
@[simp]
theorem BitVec.getElem_shiftLeft {m : Nat} {i : Nat} {x : BitVec m} {n : Nat} (h : i < m) :
(x <<< n)[i] = (!decide (i < n) && x.getLsbD (i - n))
theorem BitVec.shiftLeft_xor_distrib {w : Nat} (x : BitVec w) (y : BitVec w) (n : Nat) :
(x ^^^ y) <<< n = x <<< n ^^^ y <<< n
theorem BitVec.shiftLeft_and_distrib {w : Nat} (x : BitVec w) (y : BitVec w) (n : Nat) :
(x &&& y) <<< n = x <<< n &&& y <<< n
theorem BitVec.shiftLeft_or_distrib {w : Nat} (x : BitVec w) (y : BitVec w) (n : Nat) :
(x ||| y) <<< n = x <<< n ||| y <<< n
@[simp]
theorem BitVec.getMsbD_shiftLeft {w : Nat} {k : Nat} (x : BitVec w) (i : Nat) :
(x <<< i).getMsbD k = x.getMsbD (k + i)
theorem BitVec.shiftLeftZeroExtend_eq {w : Nat} {n : Nat} {x : BitVec w} :
x.shiftLeftZeroExtend n = BitVec.setWidth (w + n) x <<< n
@[simp]
theorem BitVec.getElem_shiftLeftZeroExtend {m : Nat} {i : Nat} {x : BitVec m} {n : Nat} (h : i < m + n) :
(x.shiftLeftZeroExtend n)[i] = (!decide (i < n) && x.getLsbD (i - n))
@[simp]
theorem BitVec.getLsbD_shiftLeftZeroExtend {m : Nat} {i : Nat} (x : BitVec m) (n : Nat) :
(x.shiftLeftZeroExtend n).getLsbD i = (!decide (i < n) && x.getLsbD (i - n))
@[simp]
theorem BitVec.getMsbD_shiftLeftZeroExtend {m : Nat} {i : Nat} (x : BitVec m) (n : Nat) :
(x.shiftLeftZeroExtend n).getMsbD i = x.getMsbD i
@[simp]
theorem BitVec.msb_shiftLeftZeroExtend {w : Nat} (x : BitVec w) (i : Nat) :
(x.shiftLeftZeroExtend i).msb = x.msb
theorem BitVec.shiftLeft_add {w : Nat} (x : BitVec w) (n : Nat) (m : Nat) :
x <<< (n + m) = x <<< n <<< m
@[simp]
@[deprecated BitVec.shiftLeft_add]
theorem BitVec.shiftLeft_shiftLeft {w : Nat} (x : BitVec w) (n : Nat) (m : Nat) :
x <<< n <<< m = x <<< (n + m)

shiftLeft reductions from BitVec to Nat #

@[simp]
theorem BitVec.shiftLeft_eq' {w₁ : Nat} {w₂ : Nat} {x : BitVec w₁} {y : BitVec w₂} :
x <<< y = x <<< y.toNat
theorem BitVec.shiftLeft_zero' {w₁ : Nat} {w₂ : Nat} {x : BitVec w₁} :
x <<< 0#w₂ = x
theorem BitVec.shiftLeft_shiftLeft' {w₁ : Nat} {w₂ : Nat} {w₃ : Nat} {x : BitVec w₁} {y : BitVec w₂} {z : BitVec w₃} :
x <<< y <<< z = x <<< (y.toNat + z.toNat)
theorem BitVec.getLsbD_shiftLeft' {w₁ : Nat} {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))
@[simp]
theorem BitVec.getElem_shiftLeft' {w₁ : Nat} {w₂ : Nat} {x : BitVec w₁} {y : BitVec w₂} {i : Nat} (h : i < w₁) :
(x <<< y)[i] = (!decide (i < y.toNat) && x.getLsbD (i - y.toNat))

ushiftRight #

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

ushiftRight reductions from BitVec to Nat #

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

sshiftRight #

theorem BitVec.sshiftRight_eq {n : Nat} {x : BitVec n} {i : Nat} :
x.sshiftRight i = BitVec.ofInt n (x.toInt >>> i)
theorem BitVec.sshiftRight_eq_of_msb_false {w : Nat} {x : BitVec w} {s : Nat} (h : x.msb = false) :
x.sshiftRight s = x >>> s

if the msb is false, the arithmetic shift right equals logical shift right

theorem BitVec.sshiftRight_eq_of_msb_true {w : Nat} {x : BitVec w} {s : Nat} (h : x.msb = true) :
x.sshiftRight s = ~~~(~~~x >>> s)

If the msb is true, the arithmetic shift right equals negating, then logical shifting right, then negating again. The double negation preserves the lower bits that have been shifted, and the outer negation ensures that the high bits are '1'.

theorem BitVec.getLsbD_sshiftRight {w : Nat} (x : BitVec w) (s : Nat) (i : Nat) :
(x.sshiftRight s).getLsbD i = (!decide (w i) && if s + i < w then x.getLsbD (s + i) else x.msb)
theorem BitVec.getElem_sshiftRight {w : Nat} {x : BitVec w} {s : Nat} {i : Nat} (h : i < w) :
(x.sshiftRight s)[i] = if s + i < w then x.getLsbD (s + i) else x.msb
theorem BitVec.sshiftRight_xor_distrib {w : Nat} (x : BitVec w) (y : BitVec w) (n : Nat) :
(x ^^^ y).sshiftRight n = x.sshiftRight n ^^^ y.sshiftRight n
theorem BitVec.sshiftRight_and_distrib {w : Nat} (x : BitVec w) (y : BitVec w) (n : Nat) :
(x &&& y).sshiftRight n = x.sshiftRight n &&& y.sshiftRight n
theorem BitVec.sshiftRight_or_distrib {w : Nat} (x : BitVec w) (y : BitVec w) (n : Nat) :
(x ||| y).sshiftRight n = x.sshiftRight n ||| y.sshiftRight n
theorem BitVec.sshiftRight_msb_eq_msb {w : Nat} {n : Nat} {x : BitVec w} :
(x.sshiftRight n).msb = x.msb

The msb after arithmetic shifting right equals the original msb.

@[simp]
theorem BitVec.sshiftRight_zero {w : Nat} {x : BitVec w} :
x.sshiftRight 0 = x
theorem BitVec.sshiftRight_add {w : Nat} {x : BitVec w} {m : Nat} {n : Nat} :
x.sshiftRight (m + n) = (x.sshiftRight m).sshiftRight n
theorem BitVec.not_sshiftRight {w : Nat} {n : Nat} {b : BitVec w} :
~~~b.sshiftRight n = (~~~b).sshiftRight n
@[simp]
theorem BitVec.not_sshiftRight_not {w : Nat} {x : BitVec w} {n : Nat} :
~~~(~~~x).sshiftRight n = x.sshiftRight n

sshiftRight reductions from BitVec to Nat #

@[simp]
theorem BitVec.sshiftRight_eq' {w : Nat} :
∀ {w_1 : Nat} {y : BitVec w_1} (x : BitVec w), x.sshiftRight' y = x.sshiftRight y.toNat

udiv #

theorem BitVec.udiv_eq {n : Nat} {x : BitVec n} {y : BitVec n} :
x.udiv y = BitVec.ofNat n (x.toNat / y.toNat)
@[simp]
theorem BitVec.toNat_udiv {n : Nat} {x : BitVec n} {y : BitVec n} :
(x.udiv y).toNat = x.toNat / y.toNat

umod #

theorem BitVec.umod_eq {n : Nat} {x : BitVec n} {y : BitVec n} :
x.umod y = BitVec.ofNat n (x.toNat % y.toNat)
@[simp]
theorem BitVec.toNat_umod {n : Nat} {x : BitVec n} {y : BitVec n} :
(x.umod y).toNat = x.toNat % y.toNat

sdiv #

theorem BitVec.sdiv_eq {w : Nat} (x : BitVec w) (y : BitVec w) :
x.sdiv y = match x.msb, y.msb with | false, false => x.udiv y | false, true => -x.udiv (-y) | true, false => -(-x).udiv y | true, true => (-x).udiv (-y)

Equation theorem for sdiv in terms of udiv.

theorem BitVec.toNat_sdiv {w : Nat} {x : BitVec w} {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
theorem BitVec.sdiv_eq_and (x : BitVec 1) (y : BitVec 1) :
x.sdiv y = x &&& y

smod #

theorem BitVec.smod_eq {w : Nat} (x : BitVec w) (y : BitVec w) :
x.smod y = match x.msb, y.msb with | false, false => x.umod y | false, true => let u := x.umod (-y); if u = 0#w then u else u + y | true, false => let u := (-x).umod y; if u = 0#w then u else y - u | true, true => -(-x).umod (-y)

Equation theorem for smod in terms of umod.

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

signExtend #

The sign extension is the same as zero extending when msb = false.

The sign extension is a bitwise not, followed by a zero extend, followed by another bitwise not when msb = true. The double bitwise not ensures that the high bits are '1', and the lower bits are preserved.

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

Sign extending to a width smaller than the starting width is a truncation.

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

Sign extending to the same bitwidth is a no op.

append #

theorem BitVec.append_def {v : Nat} {w : Nat} (x : BitVec v) (y : BitVec w) :
x ++ y = x.shiftLeftZeroExtend w ||| BitVec.setWidth' y
@[simp]
theorem BitVec.toNat_append {m : Nat} {n : Nat} (x : BitVec m) (y : BitVec n) :
(x ++ y).toNat = x.toNat <<< n ||| y.toNat
theorem BitVec.getLsbD_append {n : Nat} {m : Nat} {i : Nat} {x : BitVec n} {y : BitVec m} :
(x ++ y).getLsbD i = bif decide (i < m) then y.getLsbD i else x.getLsbD (i - m)
theorem BitVec.getElem_append {n : Nat} {m : Nat} {i : Nat} {x : BitVec n} {y : BitVec m} (h : i < n + m) :
(x ++ y)[i] = bif decide (i < m) then y.getLsbD i else x.getLsbD (i - m)
@[simp]
theorem BitVec.getMsbD_append {n : Nat} {m : Nat} {i : Nat} {x : BitVec n} {y : BitVec m} :
(x ++ y).getMsbD i = bif decide (n i) then y.getMsbD (i - n) else x.getMsbD i
theorem BitVec.msb_append {w : Nat} {v : Nat} {x : BitVec w} {y : BitVec v} :
(x ++ y).msb = bif w == 0 then y.msb else x.msb
@[simp]
theorem BitVec.append_zero_width {w : Nat} (x : BitVec w) (y : BitVec 0) :
x ++ y = x
@[simp]
theorem BitVec.zero_width_append {v : Nat} (x : BitVec 0) (y : BitVec v) :
x ++ y = BitVec.cast y
@[simp]
theorem BitVec.zero_append_zero {v : Nat} {w : Nat} :
0#v ++ 0#w = 0#(v + w)
@[simp]
theorem BitVec.cast_append_right {w : Nat} {v : Nat} {v' : Nat} (h : w + v = w + v') (x : BitVec w) (y : BitVec v) :
BitVec.cast h (x ++ y) = x ++ BitVec.cast y
@[simp]
theorem BitVec.cast_append_left {w : Nat} {v : Nat} {w' : Nat} (h : w + v = w' + v) (x : BitVec w) (y : BitVec v) :
BitVec.cast h (x ++ y) = BitVec.cast x ++ y
theorem BitVec.setWidth_append {w : Nat} {v : Nat} {k : Nat} {x : BitVec w} {y : BitVec v} :
BitVec.setWidth k (x ++ y) = if h : k v then BitVec.setWidth k y else BitVec.cast (BitVec.setWidth (k - v) x ++ y)
@[simp]
theorem BitVec.setWidth_append_of_eq {v : Nat} {w : Nat} {w' : Nat} {v' : Nat} {x : BitVec v} {y : BitVec w} (h : w' = w) :
@[simp]
theorem BitVec.setWidth_cons {w : Nat} {a : Bool} {x : BitVec w} :
@[simp]
theorem BitVec.not_append {w : Nat} {v : Nat} {x : BitVec w} {y : BitVec v} :
~~~(x ++ y) = ~~~x ++ ~~~y
@[simp]
theorem BitVec.and_append {w : Nat} {v : Nat} {x₁ : BitVec w} {x₂ : BitVec w} {y₁ : BitVec v} {y₂ : BitVec v} :
x₁ ++ y₁ &&& x₂ ++ y₂ = (x₁ &&& x₂) ++ (y₁ &&& y₂)
@[simp]
theorem BitVec.or_append {w : Nat} {v : Nat} {x₁ : BitVec w} {x₂ : BitVec w} {y₁ : BitVec v} {y₂ : BitVec v} :
x₁ ++ y₁ ||| x₂ ++ y₂ = (x₁ ||| x₂) ++ (y₁ ||| y₂)
@[simp]
theorem BitVec.xor_append {w : Nat} {v : Nat} {x₁ : BitVec w} {x₂ : BitVec w} {y₁ : BitVec v} {y₂ : BitVec v} :
x₁ ++ y₁ ^^^ x₂ ++ y₂ = (x₁ ^^^ x₂) ++ (y₁ ^^^ y₂)
theorem BitVec.shiftRight_add {w : Nat} (x : BitVec w) (n : Nat) (m : Nat) :
x >>> (n + m) = x >>> n >>> m
theorem BitVec.shiftLeft_ushiftRight {w : Nat} {x : BitVec w} {n : Nat} :
@[deprecated BitVec.shiftRight_add]
theorem BitVec.shiftRight_shiftRight {w : Nat} (x : BitVec w) (n : Nat) (m : Nat) :
x >>> n >>> m = x >>> (n + m)

rev #

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

cons #

@[simp]
theorem BitVec.toNat_cons {w : Nat} (b : Bool) (x : BitVec w) :
(BitVec.cons b x).toNat = b.toNat <<< w ||| x.toNat
theorem BitVec.toNat_cons' {w : Nat} {a : Bool} {x : BitVec w} :
(BitVec.cons a x).toNat = a.toNat <<< w + x.toNat

Variant of toNat_cons using + instead of |||.

theorem BitVec.getLsbD_cons (b : Bool) {n : Nat} (x : BitVec n) (i : Nat) :
(BitVec.cons b x).getLsbD i = if i = n then b else x.getLsbD i
theorem BitVec.getElem_cons {b : Bool} {n : Nat} {x : BitVec n} {i : Nat} (h : i < n + 1) :
(BitVec.cons b x)[i] = if i = n then b else x.getLsbD i
@[simp]
theorem BitVec.msb_cons {a : Bool} :
∀ {w : Nat} {x : BitVec w}, (BitVec.cons a x).msb = a
@[simp]
theorem BitVec.getMsbD_cons_zero {a : Bool} :
∀ {w : Nat} {x : BitVec w}, (BitVec.cons a x).getMsbD 0 = a
@[simp]
theorem BitVec.getMsbD_cons_succ {a : Bool} :
∀ {w : Nat} {x : BitVec w} {i : Nat}, (BitVec.cons a x).getMsbD (i + 1) = x.getMsbD i
theorem BitVec.setWidth_succ {w : Nat} {i : Nat} (x : BitVec w) :
BitVec.setWidth (i + 1) x = BitVec.cons (x.getLsbD i) (BitVec.setWidth i x)
@[simp]
theorem BitVec.cons_msb_setWidth {w : Nat} (x : BitVec (w + 1)) :
@[deprecated]
theorem BitVec.eq_msb_cons_setWidth {w : Nat} (x : BitVec (w + 1)) :
@[simp]
theorem BitVec.not_cons {w : Nat} (x : BitVec w) (b : Bool) :
@[simp]
theorem BitVec.cons_or_cons {w : Nat} (x : BitVec w) (y : BitVec w) (a : Bool) (b : Bool) :
@[simp]
theorem BitVec.cons_and_cons {w : Nat} (x : BitVec w) (y : BitVec w) (a : Bool) (b : Bool) :
@[simp]
theorem BitVec.cons_xor_cons {w : Nat} (x : BitVec w) (y : BitVec w) (a : Bool) (b : Bool) :

concat #

@[simp]
theorem BitVec.toNat_concat {w : Nat} (x : BitVec w) (b : Bool) :
(x.concat b).toNat = x.toNat * 2 + b.toNat
theorem BitVec.getLsbD_concat {w : Nat} (x : BitVec w) (b : Bool) (i : Nat) :
(x.concat b).getLsbD i = if i = 0 then b else x.getLsbD (i - 1)
theorem BitVec.getElem_concat {w : Nat} (x : BitVec w) (b : Bool) (i : Nat) (h : i < w + 1) :
(x.concat b)[i] = if i = 0 then b else x.getLsbD (i - 1)
@[simp]
theorem BitVec.getLsbD_concat_zero :
∀ {w : Nat} {x : BitVec w} {b : Bool}, (x.concat b).getLsbD 0 = b
@[simp]
theorem BitVec.getElem_concat_zero :
∀ {w : Nat} {x : BitVec w} {b : Bool}, (x.concat b)[0] = b
@[simp]
theorem BitVec.getLsbD_concat_succ :
∀ {w : Nat} {x : BitVec w} {b : Bool} {i : Nat}, (x.concat b).getLsbD (i + 1) = x.getLsbD i
@[simp]
theorem BitVec.getElem_concat_succ {w : Nat} {b : Bool} {x : BitVec w} {i : Nat} (h : i < w) :
(x.concat b)[i + 1] = x[i]
@[simp]
theorem BitVec.not_concat {w : Nat} (x : BitVec w) (b : Bool) :
~~~x.concat b = (~~~x).concat !b
@[simp]
theorem BitVec.concat_or_concat {w : Nat} (x : BitVec w) (y : BitVec w) (a : Bool) (b : Bool) :
x.concat a ||| y.concat b = (x ||| y).concat (a || b)
@[simp]
theorem BitVec.concat_and_concat {w : Nat} (x : BitVec w) (y : BitVec w) (a : Bool) (b : Bool) :
x.concat a &&& y.concat b = (x &&& y).concat (a && b)
@[simp]
theorem BitVec.concat_xor_concat {w : Nat} (x : BitVec w) (y : BitVec w) (a : Bool) (b : Bool) :
x.concat a ^^^ y.concat b = (x ^^^ y).concat (a ^^ b)

shiftConcat #

theorem BitVec.getLsbD_shiftConcat {w : Nat} (x : BitVec w) (b : Bool) (i : Nat) :
(x.shiftConcat b).getLsbD i = (decide (i < w) && if i = 0 then b else x.getLsbD (i - 1))
theorem BitVec.getLsbD_shiftConcat_eq_decide {w : Nat} (x : BitVec w) (b : Bool) (i : Nat) :
(x.shiftConcat b).getLsbD i = (decide (i < w) && (decide (i = 0) && b || decide (0 < i) && x.getLsbD (i - 1)))
theorem BitVec.shiftRight_sub_one_eq_shiftConcat {w : Nat} {wn : Nat} (n : BitVec w) (hwn : 0 < wn) :
n >>> (wn - 1) = (n >>> wn).shiftConcat (n.getLsbD (wn - 1))
@[simp]
theorem BitVec.toNat_shiftConcat {w : Nat} {x : BitVec w} {b : Bool} :
(x.shiftConcat b).toNat = (x.toNat <<< 1 + b.toNat) % 2 ^ w
theorem BitVec.toNat_shiftConcat_eq_of_lt {w : Nat} {x : BitVec w} {b : Bool} {k : Nat} (hk : k < w) (hx : x.toNat < 2 ^ k) :
(x.shiftConcat b).toNat = x.toNat * 2 + b.toNat

x.shiftConcat b does not overflow if x < 2^k for k < w, and so x.shiftConcat b |>.toNat = x.toNat * 2 + b.toNat.

theorem BitVec.toNat_shiftConcat_lt_of_lt {w : Nat} {x : BitVec w} {b : Bool} {k : Nat} (hk : k < w) (hx : x.toNat < 2 ^ k) :
(x.shiftConcat b).toNat < 2 ^ (k + 1)
@[simp]
theorem BitVec.zero_concat_false {w : Nat} :
(0#w).concat false = 0#(w + 1)

add #

theorem BitVec.add_def {n : Nat} (x : BitVec n) (y : BitVec n) :
x + y = BitVec.ofNat n (x.toNat + y.toNat)
@[simp]
theorem BitVec.toNat_add {w : Nat} (x : BitVec w) (y : BitVec w) :
(x + y).toNat = (x.toNat + y.toNat) % 2 ^ w

Definition of bitvector addition as a nat.

@[simp]
theorem BitVec.toFin_add {w : Nat} (x : BitVec w) (y : BitVec w) :
(x + y).toFin = x.toFin + y.toFin
@[simp]
theorem BitVec.ofFin_add {n : Nat} (x : Fin (2 ^ n)) (y : BitVec n) :
{ toFin := x } + y = { toFin := x + y.toFin }
@[simp]
theorem BitVec.add_ofFin {n : Nat} (x : BitVec n) (y : Fin (2 ^ n)) :
x + { toFin := y } = { toFin := x.toFin + y }
theorem BitVec.ofNat_add {n : Nat} (x : Nat) (y : Nat) :
theorem BitVec.ofNat_add_ofNat {n : Nat} (x : Nat) (y : Nat) :
theorem BitVec.add_assoc {n : Nat} (x : BitVec n) (y : BitVec n) (z : BitVec n) :
x + y + z = x + (y + z)
instance BitVec.instAssociativeHAdd {n : Nat} :
Std.Associative fun (x1 x2 : BitVec n) => x1 + x2
Equations
  • =
theorem BitVec.add_comm {n : Nat} (x : BitVec n) (y : BitVec n) :
x + y = y + x
instance BitVec.instCommutativeHAdd {n : Nat} :
Std.Commutative fun (x1 x2 : BitVec n) => x1 + x2
Equations
  • =
@[simp]
theorem BitVec.add_zero {n : Nat} (x : BitVec n) :
x + 0#n = x
@[simp]
theorem BitVec.zero_add {n : Nat} (x : BitVec n) :
0#n + x = x
instance BitVec.instLawfulIdentityHAddOfNatOfNatNat {n : Nat} :
Std.LawfulIdentity (fun (x1 x2 : BitVec n) => x1 + x2) 0#n
Equations
  • =
theorem BitVec.setWidth_add {w : Nat} {i : Nat} (x : BitVec w) (y : BitVec w) (h : i w) :
@[simp]
theorem BitVec.toInt_add {w : Nat} (x : BitVec w) (y : BitVec w) :
(x + y).toInt = (x.toInt + y.toInt).bmod (2 ^ w)
theorem BitVec.ofInt_add {n : Nat} (x : Int) (y : Int) :
@[simp]
theorem BitVec.shiftLeft_add_distrib {w : Nat} {x : BitVec w} {y : BitVec w} {n : Nat} :
(x + y) <<< n = x <<< n + y <<< n
theorem BitVec.add_eq_xor {a : BitVec 1} {b : BitVec 1} :
a + b = a ^^^ b

sub/neg #

theorem BitVec.sub_def {n : Nat} (x : BitVec n) (y : BitVec n) :
x - y = BitVec.ofNat n (2 ^ n - y.toNat + x.toNat)
@[simp]
theorem BitVec.toNat_sub {n : Nat} (x : BitVec n) (y : BitVec n) :
(x - y).toNat = (2 ^ n - y.toNat + x.toNat) % 2 ^ n
theorem BitVec.toNat_sub' {n : Nat} (x : BitVec n) (y : BitVec n) :
(x - y).toNat = (x.toNat + (2 ^ n - y.toNat)) % 2 ^ n
@[simp]
theorem BitVec.toFin_sub {n : Nat} (x : BitVec n) (y : BitVec n) :
(x - y).toFin = x.toFin - y.toFin
@[simp]
theorem BitVec.ofFin_sub {n : Nat} (x : Fin (2 ^ n)) (y : BitVec n) :
{ toFin := x } - y = { toFin := x - y.toFin }
@[simp]
theorem BitVec.sub_ofFin {n : Nat} (x : BitVec n) (y : Fin (2 ^ n)) :
x - { toFin := y } = { toFin := x.toFin - y }
theorem BitVec.ofNat_sub_ofNat {n : Nat} (x : Nat) (y : Nat) :
BitVec.ofNat n x - BitVec.ofNat n y = BitVec.ofNat n (2 ^ n - y % 2 ^ n + x)
@[simp]
theorem BitVec.sub_zero {n : Nat} (x : BitVec n) :
x - 0#n = x
@[simp]
theorem BitVec.sub_self {n : Nat} (x : BitVec n) :
x - x = 0#n
@[simp]
theorem BitVec.toNat_neg {n : Nat} (x : BitVec n) :
(-x).toNat = (2 ^ n - x.toNat) % 2 ^ n
theorem BitVec.toInt_neg {w : Nat} {x : BitVec w} :
(-x).toInt = (-x.toInt).bmod (2 ^ w)
@[simp]
theorem BitVec.toFin_neg {n : Nat} (x : BitVec n) :
(-x).toFin = Fin.ofNat' (2 ^ n) (2 ^ n - x.toNat)
theorem BitVec.sub_toAdd {n : Nat} (x : BitVec n) (y : BitVec n) :
x - y = x + -y
@[simp]
theorem BitVec.neg_zero (n : Nat) :
-0#n = 0#n
theorem BitVec.add_sub_cancel {w : Nat} (x : BitVec w) (y : BitVec w) :
x + y - y = x
theorem BitVec.sub_add_cancel {w : Nat} (x : BitVec w) (y : BitVec w) :
x - y + y = x
theorem BitVec.eq_sub_iff_add_eq {w : Nat} {x : BitVec w} {y : BitVec w} {z : BitVec w} :
x = z - y x + y = z
theorem BitVec.neg_eq_not_add {w : Nat} (x : BitVec w) :
-x = ~~~x + 1
@[simp]
theorem BitVec.neg_neg {w : Nat} {x : BitVec w} :
- -x = x
theorem BitVec.neg_ne_iff_ne_neg {w : Nat} {x : BitVec w} {y : BitVec w} :
-x y x -y
theorem BitVec.sub_eq_xor {a : BitVec 1} {b : BitVec 1} :
a - b = a ^^^ b

abs #

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

mul #

theorem BitVec.mul_def {n : Nat} {x : BitVec n} {y : BitVec n} :
x * y = { toFin := x.toFin * y.toFin }
@[simp]
theorem BitVec.toNat_mul {n : Nat} (x : BitVec n) (y : BitVec n) :
(x * y).toNat = x.toNat * y.toNat % 2 ^ n
@[simp]
theorem BitVec.toFin_mul {n : Nat} (x : BitVec n) (y : BitVec n) :
(x * y).toFin = x.toFin * y.toFin
theorem BitVec.mul_comm {w : Nat} (x : BitVec w) (y : BitVec w) :
x * y = y * x
instance BitVec.instCommutativeHMul {w : Nat} :
Std.Commutative fun (x y : BitVec w) => x * y
Equations
  • =
theorem BitVec.mul_assoc {w : Nat} (x : BitVec w) (y : BitVec w) (z : BitVec w) :
x * y * z = x * (y * z)
instance BitVec.instAssociativeHMul {w : Nat} :
Std.Associative fun (x y : BitVec w) => x * y
Equations
  • =
@[simp]
theorem BitVec.mul_one {w : Nat} (x : BitVec w) :
x * 1#w = x
@[simp]
theorem BitVec.one_mul {w : Nat} (x : BitVec w) :
1#w * x = x
Equations
  • =
@[simp]
theorem BitVec.BitVec.mul_zero {w : Nat} {x : BitVec w} :
x * 0#w = 0#w
theorem BitVec.BitVec.mul_add {w : Nat} {x : BitVec w} {y : BitVec w} {z : BitVec w} :
x * (y + z) = x * y + x * z
theorem BitVec.mul_succ {w : Nat} {x : BitVec w} {y : BitVec w} :
x * (y + 1#w) = x * y + x
theorem BitVec.succ_mul {w : Nat} {x : BitVec w} {y : BitVec w} :
(x + 1#w) * y = x * y + y
theorem BitVec.mul_two {w : Nat} {x : BitVec w} :
x * 2#w = x + x
theorem BitVec.two_mul {w : Nat} {x : BitVec w} :
2#w * x = x + x
@[simp]
theorem BitVec.toInt_mul {w : Nat} (x : BitVec w) (y : BitVec w) :
(x * y).toInt = (x.toInt * y.toInt).bmod (2 ^ w)
theorem BitVec.ofInt_mul {n : Nat} (x : Int) (y : Int) :
theorem BitVec.mul_eq_and {a : BitVec 1} {b : BitVec 1} :
a * b = a &&& b

le and lt #

theorem BitVec.le_def {n : Nat} {x : BitVec n} {y : BitVec n} :
x y x.toNat y.toNat
@[simp]
theorem BitVec.le_ofFin {n : Nat} {x : BitVec n} {y : Fin (2 ^ n)} :
x { toFin := y } x.toFin y
@[simp]
theorem BitVec.ofFin_le {n : Nat} {x : Fin (2 ^ n)} {y : BitVec n} :
{ toFin := x } y x y.toFin
@[simp]
theorem BitVec.ofNat_le_ofNat {n : Nat} {x : Nat} {y : Nat} :
BitVec.ofNat n x BitVec.ofNat n y x % 2 ^ n y % 2 ^ n
theorem BitVec.lt_def {n : Nat} {x : BitVec n} {y : BitVec n} :
x < y x.toNat < y.toNat
@[simp]
theorem BitVec.lt_ofFin {n : Nat} {x : BitVec n} {y : Fin (2 ^ n)} :
x < { toFin := y } x.toFin < y
@[simp]
theorem BitVec.ofFin_lt {n : Nat} {x : Fin (2 ^ n)} {y : BitVec n} :
{ toFin := x } < y x < y.toFin
@[simp]
theorem BitVec.ofNat_lt_ofNat {n : Nat} {x : Nat} {y : Nat} :
BitVec.ofNat n x < BitVec.ofNat n y x % 2 ^ n < y % 2 ^ n
@[simp]
theorem BitVec.not_le {n : Nat} {x : BitVec n} {y : BitVec n} :
¬x y y < x
@[simp]
theorem BitVec.not_lt {n : Nat} {x : BitVec n} {y : BitVec n} :
¬x < y y x
@[simp]
theorem BitVec.le_refl {n : Nat} (x : BitVec n) :
x x
@[simp]
theorem BitVec.lt_irrefl {n : Nat} (x : BitVec n) :
¬x < x
theorem BitVec.le_trans {n : Nat} {x : BitVec n} {y : BitVec n} {z : BitVec n} :
x yy zx z
theorem BitVec.lt_trans {n : Nat} {x : BitVec n} {y : BitVec n} {z : BitVec n} :
x < yy < zx < z
theorem BitVec.le_total {n : Nat} (x : BitVec n) (y : BitVec n) :
x y y x
theorem BitVec.le_antisymm {n : Nat} {x : BitVec n} {y : BitVec n} :
x yy xx = y
theorem BitVec.lt_asymm {n : Nat} {x : BitVec n} {y : BitVec n} :
x < y¬y < x
theorem BitVec.lt_of_le_ne {n : Nat} {x : BitVec n} {y : BitVec n} :
x y¬x = yx < y
theorem BitVec.ne_of_lt {n : Nat} {x : BitVec n} {y : BitVec n} :
x < yx y
theorem BitVec.umod_lt {n : Nat} (x : BitVec n) {y : BitVec n} :
0 < yx.umod y < y
theorem BitVec.not_lt_iff_le {w : Nat} {x : BitVec w} {y : BitVec w} :
¬x < y y x

ofBoolList #

@[simp]
theorem BitVec.getMsbD_ofBoolListBE {bs : List Bool} {i : Nat} :
(BitVec.ofBoolListBE bs).getMsbD i = bs.getD i false
@[simp]
theorem BitVec.getLsbD_ofBoolListBE {bs : List Bool} {i : Nat} :
(BitVec.ofBoolListBE bs).getLsbD i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false)
@[simp]
theorem BitVec.getElem_ofBoolListBE {i : Nat} {bs : List Bool} (h : i < bs.length) :
(BitVec.ofBoolListBE bs)[i] = bs[bs.length - 1 - i]
@[simp]
theorem BitVec.getLsb_ofBoolListLE {bs : List Bool} {i : Nat} :
(BitVec.ofBoolListLE bs).getLsbD i = bs.getD i false
@[simp]
theorem BitVec.getMsbD_ofBoolListLE {bs : List Bool} {i : Nat} :
(BitVec.ofBoolListLE bs).getMsbD i = (decide (i < bs.length) && bs.getD (bs.length - 1 - i) false)

Rotate Left #

@[simp]
theorem BitVec.rotateLeft_mod_eq_rotateLeft {w : Nat} {x : BitVec w} {r : Nat} :
x.rotateLeft (r % w) = x.rotateLeft r

rotateLeft is invariant under mod by the bitwidth.

theorem BitVec.rotateLeft_eq_rotateLeftAux_of_lt {w : Nat} {x : BitVec w} {r : Nat} (hr : r < w) :
x.rotateLeft r = x.rotateLeftAux r

rotateLeft equals the bit fiddling definition of rotateLeftAux when the rotation amount is smaller than the bitwidth.

theorem BitVec.getLsbD_rotateLeftAux_of_le {w : Nat} {x : BitVec w} {r : Nat} {i : Nat} (hi : i < r) :
(x.rotateLeftAux r).getLsbD i = x.getLsbD (w - r + i)

Accessing bits in x.rotateLeft r the range [0, r) is equal to accessing bits x in the range [w - r, w).

Proof by example: Let x := <6 5 4 3 2 1 0> : BitVec 7. x.rotateLeft 2 = (<6 5 | 4 3 2 1 0>).rotateLeft 2 = <3 2 1 0 | 6 5>

(x.rotateLeft 2).getLsbD ⟨i, i < 2⟩ = <3 2 1 0 | 6 5>.getLsbD ⟨i, i < 2⟩ = <6 5>[i] = <6 5 | 4 3 2 1 0>[i + len(<4 3 2 1 0>)] = <6 5 | 4 3 2 1 0>[i + 7 - 2]

theorem BitVec.getLsbD_rotateLeftAux_of_geq {w : Nat} {x : BitVec w} {r : Nat} {i : Nat} (hi : i r) :
(x.rotateLeftAux r).getLsbD i = (decide (i < w) && x.getLsbD (i - r))

Accessing bits in x.rotateLeft r the range [r, w) is equal to accessing bits x in the range [0, w - r).

Proof by example: Let x := <6 5 4 3 2 1 0> : BitVec 7. x.rotateLeft 2 = (<6 5 | 4 3 2 1 0>).rotateLeft 2 = <3 2 1 0 | 6 5>

(x.rotateLeft 2).getLsbD ⟨i, i ≥ 2⟩ = <3 2 1 0 | 6 5>.getLsbD ⟨i, i ≥ 2⟩ = <3 2 1 0>[i - 2] = <6 5 | 3 2 1 0>[i - 2]

Intuitively, grab the full width (7), then move the marker | by r to the right (-2) Then, access the bit at i from the right (+i).

theorem BitVec.getLsbD_rotateLeft_of_le {w : Nat} {x : BitVec w} {r : Nat} {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.rotateRight r).getLsbD i.

@[simp]
theorem BitVec.getLsbD_rotateLeft {w : Nat} {x : BitVec w} {r : Nat} {i : Nat} :
(x.rotateLeft r).getLsbD i = bif decide (i < r % w) then x.getLsbD (w - r % w + i) else decide (i < w) && x.getLsbD (i - r % w)
@[simp]
theorem BitVec.getElem_rotateLeft {w : Nat} {x : BitVec w} {r : Nat} {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]

Rotate Right #

theorem BitVec.getLsbD_rotateRightAux_of_le {w : Nat} {x : BitVec w} {r : Nat} {i : Nat} (hi : i < w - r) :
(x.rotateRightAux r).getLsbD i = x.getLsbD (r + i)

Accessing bits in x.rotateRight r the range [0, w-r) is equal to accessing bits x in the range [r, w).

Proof by example: Let x := <6 5 4 3 2 1 0> : BitVec 7. x.rotateRight 2 = (<6 5 4 3 2 | 1 0>).rotateRight 2 = <1 0 | 6 5 4 3 2>

(x.rotateLeft 2).getLsbD ⟨i, i ≤ 7 - 2⟩ = <1 0 | 6 5 4 3 2>.getLsbD ⟨i, i ≤ 7 - 2⟩ = <6 5 4 3 2>.getLsbD i = <6 5 4 3 2 | 1 0>[i + 2]

theorem BitVec.getLsbD_rotateRightAux_of_geq {w : Nat} {x : BitVec w} {r : Nat} {i : Nat} (hi : i w - r) :
(x.rotateRightAux r).getLsbD i = (decide (i < w) && x.getLsbD (i - (w - r)))

Accessing bits in x.rotateRight r the range [w-r, w) is equal to accessing bits x in the range [0, r).

Proof by example: Let x := <6 5 4 3 2 1 0> : BitVec 7. x.rotateRight 2 = (<6 5 4 3 2 | 1 0>).rotateRight 2 = <1 0 | 6 5 4 3 2>

(x.rotateLeft 2).getLsbD ⟨i, i ≥ 7 - 2⟩ = <1 0 | 6 5 4 3 2>.getLsbD ⟨i, i ≤ 7 - 2⟩ = <1 0>.getLsbD (i - len(<6 5 4 3 2>) = <6 5 4 3 2 | 1 0> (i - len<6 4 4 3 2>)

theorem BitVec.rotateRight_eq_rotateRightAux_of_lt {w : Nat} {x : BitVec w} {r : Nat} (hr : r < w) :
x.rotateRight r = x.rotateRightAux r

rotateRight equals the bit fiddling definition of rotateRightAux when the rotation amount is smaller than the bitwidth.

@[simp]
theorem BitVec.rotateRight_mod_eq_rotateRight {w : Nat} {x : BitVec w} {r : Nat} :
x.rotateRight (r % w) = x.rotateRight r

rotateRight is invariant under mod by the bitwidth.

theorem BitVec.getLsbD_rotateRight_of_le {w : Nat} {x : BitVec w} {r : Nat} {i : Nat} (hr : r < w) :
(x.rotateRight r).getLsbD i = bif decide (i < w - r) then x.getLsbD (r + i) else decide (i < w) && x.getLsbD (i - (w - r))

When r < w, we give a formula for (x.rotateRight r).getLsb i.

@[simp]
theorem BitVec.getLsbD_rotateRight {w : Nat} {x : BitVec w} {r : Nat} {i : Nat} :
(x.rotateRight r).getLsbD i = bif decide (i < w - r % w) then x.getLsbD (r % w + i) else decide (i < w) && x.getLsbD (i - (w - r % w))
@[simp]
theorem BitVec.getElem_rotateRight {w : Nat} {x : BitVec w} {r : Nat} {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)]
@[simp]
theorem BitVec.toNat_twoPow (w : Nat) (i : Nat) :
(BitVec.twoPow w i).toNat = 2 ^ i % 2 ^ w
@[simp]
theorem BitVec.getLsbD_twoPow {w : Nat} (i : Nat) (j : Nat) :
(BitVec.twoPow w i).getLsbD j = (decide (i < w) && decide (i = j))
@[simp]
theorem BitVec.getElem_twoPow {w : Nat} {i : Nat} {j : Nat} (h : j < w) :
(BitVec.twoPow w i)[j] = decide (j = i)
theorem BitVec.and_twoPow {w : Nat} (x : BitVec w) (i : Nat) :
x &&& BitVec.twoPow w i = if x.getLsbD i = true then BitVec.twoPow w i else 0#w
theorem BitVec.twoPow_and {w : Nat} (x : BitVec w) (i : Nat) :
BitVec.twoPow w i &&& x = if x.getLsbD i = true then BitVec.twoPow w i else 0#w
@[simp]
theorem BitVec.mul_twoPow_eq_shiftLeft {w : Nat} (x : BitVec w) (i : Nat) :
x * BitVec.twoPow w i = x <<< i
@[simp]
theorem BitVec.getLsbD_one {w : Nat} {i : Nat} :
(1#w).getLsbD i = (decide (0 < w) && decide (0 = i))
@[simp]
theorem BitVec.getElem_one {w : Nat} {i : Nat} (h : i < w) :
(1#w)[i] = decide (i = 0)
theorem BitVec.shiftLeft_eq_mul_twoPow {w : Nat} (x : BitVec w) (n : Nat) :
x <<< n = x * BitVec.twoPow w n
@[simp]
@[simp]
theorem BitVec.false_cons_zero {w : Nat} :
BitVec.cons false 0#w = 0#(w + 1)
@[simp]
theorem BitVec.zero_concat_true {w : Nat} :
(0#w).concat true = 1#(w + 1)

When the (i+1)th bit of x is false, keeping the lower (i + 1) bits of x equals keeping the lower i bits.

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

Bitwise and of (x : BitVec w) with 1#w equals zero extending x.lsb to w.

@[simp]
theorem BitVec.replicate_zero_eq {w : Nat} {x : BitVec w} :
@[simp]
theorem BitVec.replicate_succ_eq {w : Nat} {n : Nat} {x : BitVec w} :
@[simp]
theorem BitVec.getLsbD_replicate {i : Nat} {n : Nat} {w : Nat} (x : BitVec w) :
(BitVec.replicate n x).getLsbD i = (decide (i < w * n) && x.getLsbD (i % w))
@[simp]
theorem BitVec.getElem_replicate {i : Nat} {n : Nat} {w : Nat} (x : BitVec w) (h : i < w * n) :
(BitVec.replicate n x)[i] = if h' : w = 0 then false else x[i % w]

intMin #

def BitVec.intMin (w : Nat) :

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

Equations
Instances For
    theorem BitVec.getLsbD_intMin {i : Nat} (w : Nat) :
    (BitVec.intMin w).getLsbD i = decide (i + 1 = w)
    @[simp]
    theorem BitVec.toNat_intMin {w : Nat} :
    (BitVec.intMin w).toNat = 2 ^ (w - 1) % 2 ^ w

    The RHS is zero in case w = 0 which is modeled by wrapping the expression in ... % 2 ^ w.

    @[simp]
    theorem BitVec.toInt_intMin {w : Nat} :
    (BitVec.intMin w).toInt = -(2 ^ (w - 1) % 2 ^ w)

    The RHS is zero in case w = 0 which is modeled by wrapping the expression in ... % 2 ^ w.

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

    intMax #

    def BitVec.intMax (w : Nat) :

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

    Equations
    Instances For
      @[simp]
      theorem BitVec.toNat_intMax {w : Nat} :
      (BitVec.intMax w).toNat = 2 ^ (w - 1) - 1
      @[simp]
      theorem BitVec.getLsbD_intMax {i : Nat} (w : Nat) :
      (BitVec.intMax w).getLsbD i = decide (i + 1 < w)

      Non-overflow theorems #

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

      theorem BitVec.toNat_sub_of_le {n : Nat} {x : BitVec n} {y : BitVec n} (h : y x) :
      (x - y).toNat = x.toNat - y.toNat

      If y ≤ x, then the subtraction (x - y) does not overflow. Thus, (x - y).toNat = x.toNat - y.toNat

      theorem BitVec.toNat_sub_of_lt {w : Nat} {x : BitVec w} {y : BitVec w} (h : x < y) :
      (x - y).toNat = 2 ^ w - (y.toNat - x.toNat)

      If y > x, then the subtraction (x - y) does overflow, and the result is the wraparound. Thus, (x - y).toNat = 2^w - (y.toNat - x.toNat).

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

      Decidable quantifiers #

      theorem BitVec.forall_zero_iff {P : BitVec 0Prop} :
      (∀ (v : BitVec 0), P v) P 0#0
      theorem BitVec.forall_cons_iff {n : Nat} {P : BitVec (n + 1)Prop} :
      (∀ (v : BitVec (n + 1)), P v) ∀ (x : Bool) (v : BitVec n), P (BitVec.cons x v)
      instance BitVec.instDecidableForallBitVecSucc {n : Nat} (P : BitVec (n + 1)Prop) [DecidablePred P] [Decidable (∀ (x : Bool) (v : BitVec n), P (BitVec.cons x v))] :
      Decidable (∀ (v : BitVec (n + 1)), P v)
      Equations
      instance BitVec.instDecidableExistsBitVecZero (P : BitVec 0Prop) [Decidable (P 0#0)] :
      Decidable (∃ (v : BitVec 0), P v)
      Equations
      instance BitVec.instDecidableExistsBitVecSucc {n : Nat} (P : BitVec (n + 1)Prop) [DecidablePred P] [Decidable (∀ (x : Bool) (v : BitVec n), ¬P (BitVec.cons x v))] :
      Decidable (∃ (v : BitVec (n + 1)), P v)
      Equations
      instance BitVec.instDecidableForallBitVec (n : Nat) (P : BitVec nProp) [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
      instance BitVec.instDecidableExistsBitVec (n : Nat) (P : BitVec nProp) [DecidablePred P] :
      Decidable (∃ (v : BitVec n), P v)

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

      Equations

      Deprecations #

      @[reducible, inline, deprecated BitVec.truncate_eq_setWidth]
      Equations
      Instances For
        @[reducible, inline, deprecated BitVec.toNat_setWidth']
        abbrev BitVec.toNat_zeroExtend' {m : Nat} {n : Nat} (p : m n) (x : BitVec m) :
        (BitVec.setWidth' p x).toNat = x.toNat
        Equations
        Instances For
          @[reducible, inline, deprecated BitVec.toNat_setWidth]
          abbrev BitVec.toNat_zeroExtend {n : Nat} (i : Nat) (x : BitVec n) :
          (BitVec.setWidth i x).toNat = x.toNat % 2 ^ i
          Equations
          Instances For
            @[reducible, inline, deprecated BitVec.toNat_setWidth]
            abbrev BitVec.toNat_truncate {n : Nat} (i : Nat) (x : BitVec n) :
            (BitVec.setWidth i x).toNat = x.toNat % 2 ^ i
            Equations
            Instances For
              @[reducible, inline, deprecated BitVec.setWidth_eq]
              abbrev BitVec.zeroExtend_eq {n : Nat} (x : BitVec n) :
              Equations
              Instances For
                @[reducible, inline, deprecated BitVec.setWidth_eq]
                abbrev BitVec.truncate_eq {n : Nat} (x : BitVec n) :
                Equations
                Instances For
                  @[reducible, inline, deprecated BitVec.setWidth_zero]
                  abbrev BitVec.zeroExtend_zero (m : Nat) (n : Nat) :
                  BitVec.setWidth m 0#n = 0#m
                  Equations
                  Instances For
                    @[reducible, inline, deprecated BitVec.getElem_setWidth]
                    abbrev BitVec.getElem_zeroExtend {n : Nat} (m : Nat) (x : BitVec n) (i : Nat) (h : i < m) :
                    (BitVec.setWidth m x)[i] = x.getLsbD i
                    Equations
                    Instances For
                      @[reducible, inline, deprecated BitVec.getElem_setWidth']
                      abbrev BitVec.getElem_zeroExtend' {w : Nat} {v : Nat} (x : BitVec w) (i : Nat) (h : w v) (hi : i < v) :
                      (BitVec.setWidth' h x)[i] = x.getLsbD i
                      Equations
                      Instances For
                        @[reducible, inline, deprecated BitVec.getElem?_setWidth]
                        abbrev BitVec.getElem?_zeroExtend {n : Nat} (m : Nat) (x : BitVec n) (i : Nat) :
                        (BitVec.setWidth m x)[i]? = if i < m then some (x.getLsbD i) else none
                        Equations
                        Instances For
                          @[reducible, inline, deprecated BitVec.getElem?_setWidth']
                          abbrev BitVec.getElem?_zeroExtend' {w : Nat} {v : Nat} (x : BitVec w) (i : Nat) (h : w v) :
                          (BitVec.setWidth' h x)[i]? = if i < v then some (x.getLsbD i) else none
                          Equations
                          Instances For
                            @[reducible, inline, deprecated BitVec.getLsbD_setWidth]
                            abbrev BitVec.getLsbD_zeroExtend {n : Nat} (m : Nat) (x : BitVec n) (i : Nat) :
                            (BitVec.setWidth m x).getLsbD i = (decide (i < m) && x.getLsbD i)
                            Equations
                            Instances For
                              @[reducible, inline, deprecated BitVec.getLsbD_setWidth']
                              abbrev BitVec.getLsbD_zeroExtend' {m : Nat} {n : Nat} (ge : m n) (x : BitVec n) (i : Nat) :
                              (BitVec.setWidth' ge x).getLsbD i = x.getLsbD i
                              Equations
                              Instances For
                                @[reducible, inline, deprecated BitVec.getMsbD_setWidth_add]
                                abbrev BitVec.getMsbD_zeroExtend_add {w : Nat} {k : Nat} {i : Nat} {x : BitVec w} (h : k i) :
                                (BitVec.setWidth (w + k) x).getMsbD i = x.getMsbD (i - k)
                                Equations
                                Instances For
                                  @[reducible, inline, deprecated BitVec.getMsbD_setWidth']
                                  abbrev BitVec.getMsbD_zeroExtend' {m : Nat} {n : Nat} (ge : m n) (x : BitVec n) (i : Nat) :
                                  (BitVec.setWidth' ge x).getMsbD i = (decide (i m - n) && x.getMsbD (i - (m - n)))
                                  Equations
                                  Instances For
                                    @[reducible, inline, deprecated BitVec.getElem_setWidth]
                                    abbrev BitVec.getElem_truncate {n : Nat} (m : Nat) (x : BitVec n) (i : Nat) (h : i < m) :
                                    (BitVec.setWidth m x)[i] = x.getLsbD i
                                    Equations
                                    Instances For
                                      @[reducible, inline, deprecated BitVec.getElem?_setWidth]
                                      abbrev BitVec.getElem?_truncate {n : Nat} (m : Nat) (x : BitVec n) (i : Nat) :
                                      (BitVec.setWidth m x)[i]? = if i < m then some (x.getLsbD i) else none
                                      Equations
                                      Instances For
                                        @[reducible, inline, deprecated BitVec.getLsbD_setWidth]
                                        abbrev BitVec.getLsbD_truncate {n : Nat} (m : Nat) (x : BitVec n) (i : Nat) :
                                        (BitVec.setWidth m x).getLsbD i = (decide (i < m) && x.getLsbD i)
                                        Equations
                                        Instances For
                                          @[reducible, inline, deprecated BitVec.msb_setWidth]
                                          abbrev BitVec.msb_truncate {w : Nat} {v : Nat} (x : BitVec w) :
                                          (BitVec.setWidth v x).msb = (decide (0 < v) && x.getLsbD (v - 1))
                                          Equations
                                          Instances For
                                            @[reducible, inline, deprecated BitVec.cast_setWidth]
                                            abbrev BitVec.cast_zeroExtend {v : Nat} {v' : Nat} {w : Nat} (h : v = v') (x : BitVec w) :
                                            Equations
                                            Instances For
                                              @[reducible, inline, deprecated BitVec.cast_setWidth]
                                              abbrev BitVec.cast_truncate {v : Nat} {v' : Nat} {w : Nat} (h : v = v') (x : BitVec w) :
                                              Equations
                                              Instances For
                                                @[reducible, inline, deprecated BitVec.setWidth_setWidth_of_le]
                                                Equations
                                                Instances For
                                                  @[reducible, inline, deprecated BitVec.setWidth_eq]
                                                  abbrev BitVec.truncate_eq_self {n : Nat} (x : BitVec n) :
                                                  Equations
                                                  Instances For
                                                    @[reducible, inline, deprecated BitVec.setWidth_cast]
                                                    abbrev BitVec.truncate_cast {w : Nat} {v : Nat} {x : BitVec w} {k : Nat} {h : w = v} :
                                                    Equations
                                                    Instances For
                                                      @[reducible, inline, deprecated BitVec.msb_setWidth]
                                                      abbrev BitVec.mbs_zeroExtend {w : Nat} {v : Nat} (x : BitVec w) :
                                                      (BitVec.setWidth v x).msb = (decide (0 < v) && x.getLsbD (v - 1))
                                                      Equations
                                                      Instances For
                                                        @[reducible, inline, deprecated BitVec.msb_setWidth']
                                                        abbrev BitVec.mbs_zeroExtend' {w : Nat} {v : Nat} (x : BitVec w) (h : w v) :
                                                        (BitVec.setWidth' h x).msb = (decide (0 < v) && x.getLsbD (v - 1))
                                                        Equations
                                                        Instances For
                                                          @[reducible, inline, deprecated BitVec.setWidth_one_eq_ofBool_getLsb_zero]
                                                          Equations
                                                          Instances For
                                                            @[reducible, inline, deprecated BitVec.setWidth_ofNat_one_eq_ofNat_one_of_lt]
                                                            abbrev BitVec.zeroExtend_ofNat_one_eq_ofNat_one_of_lt {v : Nat} {w : Nat} (hv : 0 < v) :
                                                            BitVec.setWidth w 1#v = 1#w
                                                            Equations
                                                            Instances For
                                                              @[reducible, inline, deprecated BitVec.setWidth_one]
                                                              abbrev BitVec.truncate_one {w : Nat} {x : BitVec w} :
                                                              BitVec.setWidth 1 x = BitVec.ofBool (x.getLsbD 0)
                                                              Equations
                                                              Instances For
                                                                @[reducible, inline, deprecated BitVec.setWidth_ofNat_of_le]
                                                                abbrev BitVec.truncate_ofNat_of_le {v : Nat} {w : Nat} (h : v w) (x : Nat) :
                                                                Equations
                                                                Instances For
                                                                  @[reducible, inline, deprecated BitVec.setWidth_or]
                                                                  abbrev BitVec.truncate_or {w : Nat} {k : Nat} {x : BitVec w} {y : BitVec w} :
                                                                  Equations
                                                                  Instances For
                                                                    @[reducible, inline, deprecated BitVec.setWidth_and]
                                                                    abbrev BitVec.truncate_and {w : Nat} {k : Nat} {x : BitVec w} {y : BitVec w} :
                                                                    Equations
                                                                    Instances For
                                                                      @[reducible, inline, deprecated BitVec.setWidth_xor]
                                                                      abbrev BitVec.truncate_xor {w : Nat} {k : Nat} {x : BitVec w} {y : BitVec w} :
                                                                      Equations
                                                                      Instances For
                                                                        @[reducible, inline, deprecated BitVec.setWidth_not]
                                                                        abbrev BitVec.truncate_not {w : Nat} {k : Nat} {x : BitVec w} (h : k w) :
                                                                        Equations
                                                                        Instances For
                                                                          @[reducible, inline, deprecated BitVec.signExtend_eq_not_setWidth_not_of_msb_false]
                                                                          Equations
                                                                          Instances For
                                                                            @[reducible, inline, deprecated BitVec.signExtend_eq_not_setWidth_not_of_msb_true]
                                                                            Equations
                                                                            Instances For
                                                                              @[reducible, inline, deprecated BitVec.signExtend_eq_setWidth_of_lt]
                                                                              Equations
                                                                              Instances For
                                                                                @[reducible, inline, deprecated BitVec.truncate_append]
                                                                                abbrev BitVec.truncate_append {w : Nat} {v : Nat} {k : Nat} {x : BitVec w} {y : BitVec v} :
                                                                                BitVec.setWidth k (x ++ y) = if h : k v then BitVec.setWidth k y else BitVec.cast (BitVec.setWidth (k - v) x ++ y)
                                                                                Equations
                                                                                Instances For
                                                                                  @[reducible, inline, deprecated BitVec.truncate_append_of_eq]
                                                                                  abbrev BitVec.truncate_append_of_eq {v : Nat} {w : Nat} {w' : Nat} {v' : Nat} {x : BitVec v} {y : BitVec w} (h : w' = w) :
                                                                                  Equations
                                                                                  Instances For
                                                                                    @[reducible, inline, deprecated BitVec.truncate_cons]
                                                                                    abbrev BitVec.truncate_cons {w : Nat} {a : Bool} {x : BitVec w} :
                                                                                    Equations
                                                                                    Instances For
                                                                                      @[reducible, inline, deprecated BitVec.truncate_succ]
                                                                                      abbrev BitVec.truncate_succ {w : Nat} {i : Nat} (x : BitVec w) :
                                                                                      BitVec.setWidth (i + 1) x = BitVec.cons (x.getLsbD i) (BitVec.setWidth i x)
                                                                                      Equations
                                                                                      Instances For
                                                                                        @[reducible, inline, deprecated BitVec.truncate_add]
                                                                                        abbrev BitVec.truncate_add {w : Nat} {i : Nat} (x : BitVec w) (y : BitVec w) (h : i w) :
                                                                                        Equations
                                                                                        Instances For
                                                                                          @[reducible, inline, deprecated BitVec.setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false]
                                                                                          Equations
                                                                                          Instances For
                                                                                            @[reducible, inline, deprecated BitVec.and_one_eq_setWidth_ofBool_getLsbD]
                                                                                            Equations
                                                                                            Instances For