structure ByteArray : Type

• data : Array UInt8

@[extern lean_mk_empty_byte_array]

def ByteArray.mkEmpty (c : Nat) : ByteArray

Equations

• ByteArray.mkEmpty c = { data := #[] }

def ByteArray.empty : ByteArray

Equations

• ByteArray.empty = ByteArray.mkEmpty 0

instance ByteArray.instInhabited : Inhabited ByteArray

Equations

• ByteArray.instInhabited = { default := ByteArray.empty }

instance ByteArray.instEmptyCollection : EmptyCollection ByteArray

Equations

• ByteArray.instEmptyCollection = { emptyCollection := ByteArray.empty }

@[extern lean_byte_array_push]

def ByteArray.push : ByteArray → UInt8 → ByteArray

Equations

• x✝.push x = match x✝, x with | { data := bs }, b => { data := bs.push b }

@[extern lean_byte_array_size]

def ByteArray.size : ByteArray → Nat

Equations

• x.size = match x with | { data := bs } => bs.size

@[extern lean_byte_array_uget]

def ByteArray.uget (a : ByteArray) (i : USize) : i.toNat < a.size → UInt8

Equations

• x✝¹.uget x✝ x = match x✝¹, x✝, x with | { data := bs }, i, h => bs[i]

@[extern lean_byte_array_get]

def ByteArray.get! : ByteArray → Nat → UInt8

Equations

• x✝.get! x = match x✝, x with | { data := bs }, i => bs.get! i

@[extern lean_byte_array_fget]

def ByteArray.get (a : ByteArray) : Fin a.size → UInt8

Equations

• x✝.get x = match x✝, x with | { data := bs }, i => bs.get i

instance ByteArray.instGetElemNatUInt8LtSize : GetElem ByteArray Nat UInt8 fun (xs : ByteArray) (i : Nat) => i < xs.size

Equations

• ByteArray.instGetElemNatUInt8LtSize = { getElem := fun (xs : ByteArray) (i : Nat) (h : i < xs.size) => xs.get ⟨i, h⟩ }

instance ByteArray.instGetElemUSizeUInt8LtNatValValSize : GetElem ByteArray USize UInt8 fun (xs : ByteArray) (i : USize) => ↑i.val < xs.size

Equations

• ByteArray.instGetElemUSizeUInt8LtNatValValSize = { getElem := fun (xs : ByteArray) (i : USize) (h : ↑i.val < xs.size) => xs.uget i h }

@[extern lean_byte_array_set]

def ByteArray.set! : ByteArray → Nat → UInt8 → ByteArray

Equations

• x✝¹.set! x✝ x = match x✝¹, x✝, x with | { data := bs }, i, b => { data := bs.set! i b }

@[extern lean_byte_array_fset]

def ByteArray.set (a : ByteArray) : Fin a.size → UInt8 → ByteArray

Equations

• x✝¹.set x✝ x = match x✝¹, x✝, x with | { data := bs }, i, b => { data := bs.set i b }

@[extern lean_byte_array_uset]

def ByteArray.uset (a : ByteArray) (i : USize) : UInt8 → i.toNat < a.size → ByteArray

Equations

• x✝².uset x✝¹ x✝ x = match x✝², x✝¹, x✝, x with | { data := bs }, i, v, h => { data := bs.uset i v h }

@[extern lean_byte_array_hash]

opaque ByteArray.hash (a : ByteArray) : UInt64

instance ByteArray.instHashable : Hashable ByteArray

Equations

• ByteArray.instHashable = { hash := ByteArray.hash }

def ByteArray.isEmpty (s : ByteArray) : Bool

Equations

• s.isEmpty = (s.size == 0)

@[extern lean_byte_array_copy_slice]

def ByteArray.copySlice (src : ByteArray) (srcOff : Nat) (dest : ByteArray) (destOff : Nat) (len : Nat) (exact : optParam Bool true) : ByteArray

Copy the slice at [srcOff, srcOff + len) in src to [destOff, destOff + len) in dest, growing dest if necessary. If exact is false, the capacity will be doubled when grown.

Equations

• One or more equations did not get rendered due to their size.

def ByteArray.extract (a : ByteArray) (b : Nat) (e : Nat) : ByteArray

Equations

• a.extract b e = a.copySlice b ByteArray.empty 0 (e - b)

def ByteArray.append (a : ByteArray) (b : ByteArray) : ByteArray

Equations

• a.append b = b.copySlice 0 a a.size b.size false

instance ByteArray.instAppend : Append ByteArray

Equations

• ByteArray.instAppend = { append := ByteArray.append }

def ByteArray.toList (bs : ByteArray) : List UInt8

Equations

• bs.toList = ByteArray.toList.loop bs 0 []

partial def ByteArray.toList.loop (bs : ByteArray) (i : Nat) (r : List UInt8) : List UInt8

@[inline]

def ByteArray.findIdx? (a : ByteArray) (p : UInt8 → Bool) (start : optParam Nat 0) : Option Nat

Equations

• a.findIdx? p start = ByteArray.findIdx?.loop a p start

@[specialize #[]]

partial def ByteArray.findIdx?.loop (a : ByteArray) (p : UInt8 → Bool) (i : Nat) : Option Nat

@[inline]

unsafe def ByteArray.forInUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteArray) (b : β) (f : UInt8 → β → m (ForInStep β)) : m β

We claim this unsafe implementation is correct because an array cannot have more than usizeSz elements in our runtime. This is similar to the Array version.

TODO: avoid code duplication in the future after we improve the compiler.

Equations

• as.forInUnsafe b f = let sz := USize.ofNat as.size; ByteArray.forInUnsafe.loop as f sz 0 b

@[specialize #[]]

unsafe def ByteArray.forInUnsafe.loop {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteArray) (f : UInt8 → β → m (ForInStep β)) (sz : USize) (i : USize) (b : β) : m β

Equations

• One or more equations did not get rendered due to their size.

@[implemented_by ByteArray.forInUnsafe]

def ByteArray.forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteArray) (b : β) (f : UInt8 → β → m (ForInStep β)) : m β

Reference implementation for forIn

Equations

• as.forIn b f = ByteArray.forIn.loop as f as.size ⋯ b

def ByteArray.forIn.loop {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteArray) (f : UInt8 → β → m (ForInStep β)) (i : Nat) (h : i ≤ as.size) (b : β) : m β

Equations

• One or more equations did not get rendered due to their size.
• ByteArray.forIn.loop as f 0 x b = pure b

instance ByteArray.instForInUInt8 {m : Type u_1 → Type u_2} : ForIn m ByteArray UInt8

Equations

• ByteArray.instForInUInt8 = { forIn := fun {β : Type u_1} [Monad m] => ByteArray.forIn }

@[inline]

unsafe def ByteArray.foldlMUnsafe {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt8 → m β) (init : β) (as : ByteArray) (start : optParam Nat 0) (stop : optParam Nat as.size) : m β

See comment at forInUnsafe

Equations

• One or more equations did not get rendered due to their size.

@[specialize #[]]

unsafe def ByteArray.foldlMUnsafe.fold {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt8 → m β) (as : ByteArray) (i : USize) (stop : USize) (b : β) : m β

Equations

• ByteArray.foldlMUnsafe.fold f as i stop b = if (i == stop) = true then pure b else do let __do_lift ← f b (as.uget i ⋯) ByteArray.foldlMUnsafe.fold f as (i + 1) stop __do_lift

@[implemented_by ByteArray.foldlMUnsafe]

def ByteArray.foldlM {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt8 → m β) (init : β) (as : ByteArray) (start : optParam Nat 0) (stop : optParam Nat as.size) : m β

Reference implementation for foldlM

Equations

• One or more equations did not get rendered due to their size.

def ByteArray.foldlM.loop {β : Type v} {m : Type v → Type w} [Monad m] (f : β → UInt8 → m β) (as : ByteArray) (stop : Nat) (h : stop ≤ as.size) (i : Nat) (j : Nat) (b : β) : m β

Equations

• One or more equations did not get rendered due to their size.

@[inline]

def ByteArray.foldl {β : Type v} (f : β → UInt8 → β) (init : β) (as : ByteArray) (start : optParam Nat 0) (stop : optParam Nat as.size) : β

Equations

• ByteArray.foldl f init as start stop = (ByteArray.foldlM f init as start stop).run

def List.toByteArray (bs : List UInt8) : ByteArray

Equations

• bs.toByteArray = List.toByteArray.loop bs ByteArray.empty

def List.toByteArray.loop : List UInt8 → ByteArray → ByteArray

Equations

• List.toByteArray.loop [] x = x
• List.toByteArray.loop (b :: bs) x = List.toByteArray.loop bs (x.push b)

instance instToStringByteArray : ToString ByteArray

Equations

• instToStringByteArray = { toString := fun (bs : ByteArray) => bs.toList.toString }

def ByteArray.toUInt64LE! (bs : ByteArray) : UInt64

Interpret a ByteArray of size 8 as a little-endian UInt64.

Equations

• One or more equations did not get rendered due to their size.

def ByteArray.toUInt64BE! (bs : ByteArray) : UInt64

Interpret a ByteArray of size 8 as a big-endian UInt64.

Equations

• One or more equations did not get rendered due to their size.