def ByteArray.getD (bs : ByteArray) (z : UInt8) (i : ℕ) : UInt8

Equations

• bs.getD z i = if h : i < bs.size then bs[i] else z

@[irreducible]

def ByteArray.ofBits' (acc : List UInt8) (bs : List Bit) : List UInt8

Equations

• ByteArray.ofBits' acc bs = if bs = [] then acc else match _h : List.splitAt 8 bs with | (xs, bs') => ByteArray.ofBits' (UInt8.ofBits xs :: acc) bs'

def ByteArray.ofBits (bs : List Bit) : ByteArray

Equations

• ByteArray.ofBits bs = { data := { toList := (ByteArray.ofBits' [] bs).reverse } }

def ByteArray.toBits (bs : ByteArray) : List Bit

Equations

• bs.toBits = List.flatMap UInt8.toBits bs.data.toList

theorem ByteArray.empty_def : ∅ = { data := { toList := [] } }

@[simp]

theorem ByteArray.ofBits_nil : ofBits [] = ∅

@[simp]

theorem ByteArray.ofBits'_nil {acc : List UInt8} : ofBits' acc [] = acc

@[simp]

theorem ByteArray.ofBits_toBits {bs : ByteArray} : ofBits bs.toBits = bs

@[simp]

theorem ByteArray.toBits_empty : empty.toBits = []

theorem ByteArray.ofBits'_of_length_le {bs₁ : List UInt8} {bs₂ : List Bit} (h₁ : bs₂ ≠ []) (h₂ : bs₂.length ≤ 8) : ofBits' bs₁ bs₂ = UInt8.ofBits bs₂ :: bs₁

theorem ByteArray.ofBits'_eq_append {bs₁ : List UInt8} {bs₂ : List Bit} : ofBits' bs₁ bs₂ = ofBits' [] bs₂ ++ bs₁

@[simp]

theorem ByteArray.toBits_ofBits {bs : List Bit} : (ofBits bs).toBits = bs ++ List.replicate ((8 - bs.length % 8) % 8) 0

theorem ByteArray.ofBits_of_length_le {bs : List Bit} (h₁ : bs ≠ []) (h₂ : bs.length ≤ 8) : ofBits bs = { data := { toList := [UInt8.ofBits bs] } }

@[simp]

theorem ByteArray.size_mk {bs : Array UInt8} : { data := bs }.size = bs.size

@[simp]

theorem ByteArray.get!_mk {bs : Array UInt8} {i : ℕ} : { data := bs }.get! i = bs[i]!

@[simp]

theorem ByteArray.toList_mk {bs : Array UInt8} : { data := bs }.toList = bs.toList

theorem ByteArray.toList_eq_toList_data {bs : ByteArray} : bs.toList = bs.data.toList

theorem ByteArray.ofBits_of_le_length {bs : List Bit} (h : 8 ≤ bs.length) : ofBits bs = { data := { toList := UInt8.ofBits (List.take 8 bs) :: (ofBits (List.drop 8 bs)).toList } }

@[simp]

theorem ByteArray.getElem_mk {xs : Array UInt8} {i : ℕ} {h : i < { data := xs }.size} : { data := xs }[i] = xs[i]

@[simp]

theorem ByteArray.singleton_eq_iff {xs : ByteArray} {x : UInt8} : empty.push x = xs ↔ xs.size = 1 ∧ xs[0]! = x

@[simp]

theorem ByteArray.eq_singleton_iff {xs : ByteArray} {x : UInt8} : xs = empty.push x ↔ xs.size = 1 ∧ xs[0]! = x