structure ByteArray : Type

• data : Array UInt8

@[extern lean_mk_empty_byte_array]

def ByteArray.emptyWithCapacity (c : Nat) : ByteArray

@[reducible, inline, deprecated ByteArray.emptyWithCapacity (since := "2025-03-12")]

abbrev ByteArray.mkEmpty (c : Nat) : ByteArray

def ByteArray.empty : ByteArray

instance ByteArray.instInhabited : Inhabited ByteArray

instance ByteArray.instEmptyCollection : EmptyCollection ByteArray

@[extern lean_byte_array_push]

def ByteArray.push : ByteArray → UInt8 → ByteArray

@[extern lean_byte_array_size]

def ByteArray.size : ByteArray → Nat

@[extern lean_sarray_size]

def ByteArray.usize (a : ByteArray) : USize

@[extern lean_byte_array_uget]

def ByteArray.uget (a : ByteArray) (i : USize) (h : i.toNat < a.size := by get_elem_tactic) : UInt8

@[extern lean_byte_array_get]

def ByteArray.get! : ByteArray → Nat → UInt8

@[extern lean_byte_array_fget]

def ByteArray.get (a : ByteArray) (i : Nat) (h : i < a.size := by get_elem_tactic) : UInt8

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

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

@[extern lean_byte_array_set]

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

@[extern lean_byte_array_fset]

def ByteArray.set (a : ByteArray) (i : Nat) : UInt8 → (h : autoParam (i < a.size) _auto✝) → ByteArray

@[extern lean_byte_array_uset]

def ByteArray.uset (a : ByteArray) (i : USize) : UInt8 → (h : autoParam (i.toNat < a.size) _auto✝) → ByteArray

@[extern lean_byte_array_hash]

opaque ByteArray.hash (a : ByteArray) : UInt64

instance ByteArray.instHashable : Hashable ByteArray

def ByteArray.isEmpty (s : ByteArray) : Bool

@[extern lean_byte_array_copy_slice]

def ByteArray.copySlice (src : ByteArray) (srcOff : Nat) (dest : ByteArray) (destOff len : Nat) (exact : 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.

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

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

instance ByteArray.instAppend : Append ByteArray

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

@[irreducible]

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

@[inline]

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

@[irreducible, specialize #[]]

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

@[inline]

def ByteArray.findFinIdx? (a : ByteArray) (p : UInt8 → Bool) (start : Nat := 0) : Option (Fin a.size)

@[irreducible, specialize #[]]

def ByteArray.findFinIdx?.loop (a : ByteArray) (p : UInt8 → Bool) (i : Nat) : Option (Fin a.size)

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

@[specialize #[]]

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

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

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 β

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

@[inline]

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

See comment at forInUnsafe

@[specialize #[]]

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

@[implemented_by ByteArray.foldlMUnsafe]

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

Reference implementation for foldlM

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 j : Nat) (b : β) : m β

@[inline]

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

structure ByteArray.Iterator : Type

Iterator over the bytes (UInt8) of a ByteArray.

Typically created by arr.iter, where arr is a ByteArray.

An iterator is valid if the position i is valid for the array arr, meaning 0 ≤ i ≤ arr.size

Most operations on iterators return arbitrary values if the iterator is not valid. The functions in the ByteArray.Iterator API should rule out the creation of invalid iterators, with two exceptions:

• Iterator.next iter is invalid if iter is already at the end of the array (iter.atEnd is true)
• Iterator.forward iter n/Iterator.nextn iter n is invalid if n is strictly greater than the number of remaining bytes.

• array : ByteArray

  The array the iterator is for.

• idx : Nat

  The current position.

  This position is not necessarily valid for the array, for instance if one keeps calling Iterator.next when Iterator.atEnd is true. If the position is not valid, then the current byte is (default : UInt8).

instance ByteArray.instInhabitedIterator : Inhabited Iterator

def ByteArray.mkIterator (arr : ByteArray) : Iterator

Creates an iterator at the beginning of an array.

@[reducible, inline]

abbrev ByteArray.iter (arr : ByteArray) : Iterator

Creates an iterator at the beginning of an array.

instance ByteArray.instSizeOfIterator : SizeOf Iterator

The size of an array iterator is the number of bytes remaining.

theorem ByteArray.Iterator.sizeOf_eq (i : Iterator) : sizeOf i = i.array.size - i.idx

def ByteArray.Iterator.remainingBytes : Iterator → Nat

Number of bytes remaining in the iterator.

def ByteArray.Iterator.pos (self : Iterator) : Nat

The current position.

This position is not necessarily valid for the array, for instance if one keeps calling Iterator.next when Iterator.atEnd is true. If the position is not valid, then the current byte is (default : UInt8).

@[inline]

def ByteArray.Iterator.curr : Iterator → UInt8

The byte at the current position.

On an invalid position, returns (default : UInt8).

@[inline]

def ByteArray.Iterator.next : Iterator → Iterator

Moves the iterator's position forward by one byte, unconditionally.

It is only valid to call this function if the iterator is not at the end of the array, i.e. Iterator.atEnd is false; otherwise, the resulting iterator will be invalid.

@[inline]

def ByteArray.Iterator.prev : Iterator → Iterator

Decreases the iterator's position.

If the position is zero, this function is the identity.

@[inline]

def ByteArray.Iterator.atEnd : Iterator → Bool

True if the iterator is past the array's last byte.

@[inline]

def ByteArray.Iterator.hasNext : Iterator → Bool

True if the iterator is not past the array's last byte.

@[inline]

def ByteArray.Iterator.curr' (it : Iterator) (h : it.hasNext = true) : UInt8

The byte at the current position. -

@[inline]

def ByteArray.Iterator.next' (it : Iterator) (_h : it.hasNext = true) : Iterator

Moves the iterator's position forward by one byte. -

@[inline]

def ByteArray.Iterator.hasPrev : Iterator → Bool

True if the position is not zero.

@[inline]

def ByteArray.Iterator.toEnd : Iterator → Iterator

Moves the iterator's position to the end of the array.

Note that i.toEnd.atEnd is always true.

@[inline]

def ByteArray.Iterator.forward : Iterator → Nat → Iterator

Moves the iterator's position several bytes forward.

The resulting iterator is only valid if the number of bytes to skip is less than or equal to the number of bytes left in the iterator.

@[inline]

def ByteArray.Iterator.nextn : Iterator → Nat → Iterator

Moves the iterator's position several bytes forward.

The resulting iterator is only valid if the number of bytes to skip is less than or equal to the number of bytes left in the iterator.

@[inline]

def ByteArray.Iterator.prevn : Iterator → Nat → Iterator

Moves the iterator's position several bytes back.

If asked to go back more bytes than available, stops at the beginning of the array.

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

Converts a list of bytes into a ByteArray.

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

instance instToStringByteArray : ToString ByteArray

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

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

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

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