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.instInhabitedByteArray : Inhabited ByteArray

Equations

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

instance ByteArray.instEmptyCollectionByteArray : EmptyCollection ByteArray

Equations

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

@[extern lean_byte_array_push]

def ByteArray.push : ByteArray → UInt8 → ByteArray

Equations

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

@[extern lean_byte_array_size]

def ByteArray.size : ByteArray → Nat

Equations

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

@[extern lean_byte_array_uget]

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

Equations

• ByteArray.uget x 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

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

@[extern lean_byte_array_fget]

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

Equations

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

instance ByteArray.instGetElemByteArrayNatUInt8LtInstLTNatSize : GetElem ByteArray Nat UInt8 fun xs i => i < ByteArray.size xs

Equations

• ByteArray.instGetElemByteArrayNatUInt8LtInstLTNatSize = { getElem := fun xs i h => ByteArray.get xs { val := i, isLt := h } }

instance ByteArray.instGetElemByteArrayUSizeUInt8LtNatInstLTNatValSizeValSize : GetElem ByteArray USize UInt8 fun xs i => i.val.val < ByteArray.size xs

Equations

• ByteArray.instGetElemByteArrayUSizeUInt8LtNatInstLTNatValSizeValSize = { getElem := fun xs i h => ByteArray.uget xs i h }

@[extern lean_byte_array_set]

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

Equations

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

@[extern lean_byte_array_fset]

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

Equations

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

@[extern lean_byte_array_uset]

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

Equations

• ByteArray.uset x x x x = match x, x, x, x with | { data := bs }, i, v, h => { data := Array.uset bs i v h }

@[extern lean_byte_array_hash]

opaque ByteArray.hash (a : ByteArray) : UInt64

instance ByteArray.instHashableByteArray : Hashable ByteArray

Equations

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

def ByteArray.isEmpty (s : ByteArray) : Bool

Equations

• ByteArray.isEmpty s = (ByteArray.size s == 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

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

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

Equations

• ByteArray.append a b = ByteArray.copySlice b 0 a (ByteArray.size a) (ByteArray.size b) false

instance ByteArray.instAppendByteArray : Append ByteArray

Equations

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

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

Equations

• ByteArray.toList bs = 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

• ByteArray.findIdx? a 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} [inst : 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

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

@[specialize #[]]

unsafe def ByteArray.forInUnsafe.loop {β : Type v} {m : Type v → Type w} [inst : 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} [inst : Monad m] (as : ByteArray) (b : β) (f : UInt8 → β → m (ForInStep β)) : m β

Reference implementation for forIn

Equations

• ByteArray.forIn as b f = ByteArray.forIn.loop as f (ByteArray.size as) (_ : ByteArray.size as ≤ ByteArray.size as) b

def ByteArray.forIn.loop {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : ByteArray) (f : UInt8 → β → m (ForInStep β)) (i : Nat) (h : i ≤ ByteArray.size as) (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.instForInByteArrayUInt8 {m : Type u_1 → Type u_2} : ForIn m ByteArray UInt8

Equations

• ByteArray.instForInByteArrayUInt8 = { forIn := fun {β} [Monad m] => ByteArray.forIn }

@[inline]

unsafe def ByteArray.foldlMUnsafe {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : β → UInt8 → m β) (init : β) (as : ByteArray) (start : optParam Nat 0) (stop : optParam Nat (ByteArray.size as)) : 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} [inst : Monad m] (f : β → UInt8 → m β) (as : ByteArray) (i : USize) (stop : USize) (b : β) : m β

Equations

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

@[implemented_by ByteArray.foldlMUnsafe]

def ByteArray.foldlM {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : β → UInt8 → m β) (init : β) (as : ByteArray) (start : optParam Nat 0) (stop : optParam Nat (ByteArray.size as)) : 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} [inst : Monad m] (f : β → UInt8 → m β) (as : ByteArray) (stop : Nat) (h : stop ≤ ByteArray.size as) (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 (ByteArray.size as)) : β

Equations

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

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

Equations

• List.toByteArray bs = 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 (ByteArray.push x b)

instance instToStringByteArray : ToString ByteArray

Equations

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

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.