Documentation

Projects.Util.BitVec

def BitVec.ofBit (w : ℕ) (b : Bit) :

Equations

BitVec.ofBit w Bit.B₀ = 0
BitVec.ofBit w Bit.B₁ = 1

Instances For

def BitVec.lowestBit {w : ℕ} (x : BitVec w) :

Equations

x.lowestBit = Bit.ofBool (decide (Odd x.toNat))

Instances For

def BitVec.ofBits (w : ℕ) (bs : List Bit) :

Equations

BitVec.ofBits w bs = List.foldr (fun (bit : Bit) (x : BitVec w) => x <<< 1 ||| BitVec.ofBit w bit) 0 bs

Instances For

def BitVec.toBits {w : ℕ} (x : BitVec w) :

Equations

x.toBits = List.map (fun (n : ℕ) => (x >>> n).lowestBit) (List.range w)

Instances For

@[simp]

theorem BitVec.ofNatLT_eq_ofNatLT_iff {w n m : ℕ} {hn : n < 2 ^ w} {hm : m < 2 ^ w} :

n#'hn = m#'hm ↔ n = m

@[simp]

theorem BitVec.lowestBit_ofNat {w n : ℕ} :

(BitVec.ofNat w n).lowestBit = Bit.ofBool (decide (Odd (n % 2 ^ w)))

@[simp]

theorem BitVec.toBits_zero {w : ℕ} :

(0#w).toBits = List.replicate w 0

@[simp]

theorem BitVec.toBits_nil {n : ℕ} :

(BitVec.ofNat 0 n).toBits = []

@[simp]

theorem BitVec.ofBits_nil {w : ℕ} :

ofBits w [] = 0#w

@[simp]

theorem BitVec.ofBit_zero {w : ℕ} :

ofBit w 0 = 0

@[simp]

theorem BitVec.ofBit_one {w : ℕ} :

ofBit w 1 = 1

@[simp]

theorem BitVec.toBits_cons {w : ℕ} {x : BitVec w} {b : Bool} :

(cons b x).toBits = x.toBits ++ [Bit.ofBool b]

theorem BitVec.shiftLeft_one_eq_mul_two {w : ℕ} {x : BitVec w} :

x <<< 1 = x * 2

theorem BitVec.mul_two_or_one_eq {w : ℕ} {x : BitVec w} :

x * 2 ||| 1 = x * 2 + 1

theorem BitVec.foldr_eq_add_ofBits {w : ℕ} {bs : List Bit} {z : BitVec w} :

List.foldr (fun (bit : Bit) (x : BitVec w) => x <<< 1 ||| ofBit w bit) z bs = z <<< bs.length + ofBits w bs

theorem BitVec.ofBits_snoc_eq_add_ofBits {w : ℕ} {bs : List Bit} {b : Bit} :

ofBits w (bs ++ [b]) = ofBit w b <<< bs.length + ofBits w bs

@[simp]

theorem BitVec.getElem_zero_ofBit {w : ℕ} {b : Bit} {h : 0 < w} :

(ofBit w b)[0] = b.toBool

@[simp]

theorem BitVec.getElem_succ_ofBit {w i : ℕ} {b : Bit} {h : i + 1 < w} :

(ofBit w b)[i + 1] = false

@[simp]

theorem BitVec.getElem_ofBits {w : ℕ} {bs : List Bit} {i : ℕ} {h : i < w} :

(ofBits w bs)[i] = bs[i]!.toBool

theorem BitVec.foldr_eq_or_ofBits {w : ℕ} {bs : List Bit} {z : BitVec w} :

List.foldr (fun (bit : Bit) (x : BitVec w) => x <<< 1 ||| ofBit w bit) z bs = z <<< bs.length ||| ofBits w bs

theorem BitVec.ofBits_snoc_eq_or_ofBits {w : ℕ} {bs : List Bit} {b : Bit} :

ofBits w (bs ++ [b]) = ofBit w b <<< bs.length ||| ofBits w bs

@[simp]

theorem BitVec.length_toBits {w : ℕ} {x : BitVec w} :

x.toBits.length = w

theorem BitVec.odd_shiftRight_toNat_iff {w : ℕ} {x : BitVec w} {i : ℕ} :

Odd (x.toNat >>> i) ↔ ∃ (h : i < w), x[i] = true

theorem BitVec.lowestBit_shiftRight {w : ℕ} {x : BitVec w} {i : ℕ} :

(x >>> i).lowestBit = if h : i < w then Bit.ofBool x[i] else 0

theorem BitVec.toBits_eq_map_getElem {w : ℕ} {x : BitVec w} :

x.toBits = List.map (fun (x_1 : { x : ℕ // x ∈ List.range w }) => match x_1 with | ⟨i, h⟩ => Bit.ofBool x[i]) (List.range w).attach

@[simp]

theorem BitVec.getElem_cons_last {w : ℕ} {x : BitVec w} {b : Bool} {h : w < w + 1} :

(cons b x)[w] = b

@[simp]

theorem BitVec.ofBits_toBits {w : ℕ} {x : BitVec w} :

ofBits w x.toBits = x

@[simp]

theorem BitVec.toBits_eq_iff {w : ℕ} {x y : BitVec w} :

x.toBits = y.toBits ↔ x = y

@[simp]

theorem BitVec.list_subset_zero_one {bs : List Bit} :

bs ⊆ [0, 1]

theorem BitVec.w_zero_eq {x : BitVec 0} :

x = 0#0

theorem BitVec.toBits_ofBits {w : ℕ} {bs : List Bit} :

(ofBits w bs).toBits = List.take w bs ++ List.replicate (w - bs.length) 0

theorem BitVec.toBits_ofBits_of_length_eq {w : ℕ} {bs : List Bit} (h : bs.length = w) :

(ofBits w bs).toBits = bs

theorem BitVec.toBits_ofBits_of_length_le {w : ℕ} {bs : List Bit} (h : bs.length ≤ w) :

(ofBits w bs).toBits = bs ++ List.replicate (w - bs.length) 0

theorem BitVec.toBits_ofBits_of_le_length {w : ℕ} {bs : List Bit} (h : w ≤ bs.length) :

(ofBits w bs).toBits = List.take w bs

@[simp]

theorem BitVec.toBits_eq_nil_iff {w : ℕ} {x : BitVec w} :

x.toBits = [] ↔ w = 0

@[simp]

theorem BitVec.ofBits_singleton {w : ℕ} {b : Bit} :

ofBits w [b] = ofBit w b

@[instance_reducible]

instance BitVec.instLinearOrder_projects {w : ℕ} :

LinearOrder (BitVec w)

Equations

BitVec.instLinearOrder_projects = { toLE := instLEBitVec, toLT := instLTBitVec, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯, toMin := minOfOrd', toMax := maxOfOrd', toOrd := instOrdBitVec, le_total := ⋯, toDecidableLE := fun {x y : BitVec w} => inferInstance, toDecidableEq := decidableEqOfDecidableLE, toDecidableLT := decidableLTOfDecidableLE, min_def := ⋯, max_def := ⋯, compare_eq_compareOfLessAndEq := ⋯ }

@[simp]

theorem BitVec.ofBits_snoc {w : ℕ} {bs : List Bit} {b : Bit} :

ofBits w (bs ++ [b]) = ofBits w bs ||| ofBit w b <<< bs.length

@[simp]

theorem BitVec.ofNat_eq_ofNat_iff {w n k : ℕ} :

BitVec.ofNat w n = BitVec.ofNat w k ↔ w = 0 ∨ n % 2 ^ w = k % 2 ^ w

@[simp]

theorem BitVec.ofNat_eq_one_iff {w n : ℕ} :

BitVec.ofNat w n = 1#w ↔ w = 0 ∨ n % 2 ^ w = 1

theorem BitVec.ext_iff {w : ℕ} {x y : BitVec w} :

x = y ↔ x.toNat = y.toNat

@[simp]

theorem BitVec.one_shiftLeft_eq_zero_iff {w n : ℕ} :

1#w <<< n = 0#w ↔ w = 0 ∨ w ≤ n

@[simp]

theorem BitVec.one_shiftLeft_eq_one_iff {w n : ℕ} :

1#w <<< n = 1#w ↔ w = 0 ∨ n = 0

@[simp]

theorem BitVec.le_size_pow {w : ℕ} {x : BitVec w} :

x ≤ BitVec.ofNat w (2 ^ w - 1)

@[simp]

theorem BitVec.toNat_lt_size_pow {w : ℕ} {x : BitVec w} :

x.toNat < 2 ^ w

@[simp]

theorem BitVec.toNat_ofBits_lt_pow {w : ℕ} {bs : List Bit} :

(ofBits w bs).toNat < 2 ^ bs.length

theorem BitVec.or_shiftLeft_eq_add {w : ℕ} {x y : BitVec w} {n : ℕ} (h : x.toNat < 2 ^ n) :

x ||| y <<< n = x + y <<< n

@[simp]

theorem BitVec.ofBits_append_eq_or {w : ℕ} {bs₁ bs₂ : List Bit} :

ofBits w (bs₁ ++ bs₂) = ofBits w bs₁ ||| ofBits w bs₂ <<< bs₁.length

theorem BitVec.ofBits_append_eq_add {w : ℕ} {bs₁ bs₂ : List Bit} :

ofBits w (bs₁ ++ bs₂) = ofBits w bs₁ + ofBits w bs₂ <<< bs₁.length

@[simp]

theorem BitVec.toNat_le_size_pow {w : ℕ} {x : BitVec w} :

x.toNat ≤ 2 ^ w

theorem BitVec.toNat_ofBit {w : ℕ} {b : Bit} :

(ofBit w b).toNat = if w ≠ 0 ∧ b = 1 then 1 else 0