19.17. Byte Arrays🔗

Byte arrays are a specialized array type that can only contain elements of type UInt8. Due to this restriction, they can use a much more efficient representation, with no pointer indirections. Like other arrays, byte arrays are represented in compiled code as dynamic arrays, and the Lean runtime specially optimizes array operations. The operations that modify byte arrays first check the array's reference count, and if there are no other references to the array, it is modified in place.

There is no literal syntax for byte arrays. List.toByteArray can be used to construct an array from a list literal.

structure

ByteArray : Type
ByteArray : Type

ByteArray is like Array UInt8, but with an efficient run-time representation as a packed byte buffer.

Constructor

ByteArray.mk

Packs an array of bytes into a ByteArray.

Converting between Array and ByteArray takes linear time.

Fields

data : Array UInt8

The data contained in the byte array.

Converting between Array and ByteArray takes linear time.

19.17.1. API Reference

19.17.1.1. Constructing Byte Arrays

def

ByteArray.empty : ByteArray
ByteArray.empty : ByteArray

Constructs a new empty byte array with initial capacity 0.

Use ByteArray.emptyWithCapacity to create an array with a greater initial capacity.

def

ByteArray.emptyWithCapacity (c : Nat) : ByteArray
ByteArray.emptyWithCapacity (c : Nat) :
  ByteArray

Constructs a new empty byte array with initial capacity c.

def

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

Appends two byte arrays.

In compiled code, calls to ByteArray.append are replaced with the much more efficient ByteArray.fastAppend.

def

ByteArray.fastAppend (a b : ByteArray) : ByteArray
ByteArray.fastAppend (a b : ByteArray) :
  ByteArray

def

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

Copies 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.

19.17.1.2. Size

def

ByteArray.size : ByteArray → Nat
ByteArray.size : ByteArray → Nat

Returns the number of bytes in the byte array.

This is the number of bytes actually in the array, as distinct from its capacity, which is the amount of memory presently allocated for the array.

def

ByteArray.usize (a : ByteArray) : USize
ByteArray.usize (a : ByteArray) : USize

Retrieves the size of the array as a platform-specific fixed-width integer.

Because USize is big enough to address all memory on every platform that Lean supports, there are in practice no ByteArrays that have more elements that USize can count.

def

ByteArray.isEmpty (s : ByteArray) : Bool
ByteArray.isEmpty (s : ByteArray) : Bool

Returns true when s contains zero bytes.

19.17.1.3. Lookups

def

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

Retrieves the byte at the indicated index. Callers must prove that the index is in bounds.

Use uget for a more efficient alternative or get! for a variant that panics if the index is out of bounds.

def

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

Retrieves the byte at the indicated index. Callers must prove that the index is in bounds. The index is represented by a platform-specific fixed-width integer (either 32 or 64 bits).

Because USize is big enough to address all memory on every platform that Lean supports, there are in practice no ByteArrays for which uget cannot retrieve all elements.

def

ByteArray.get! : ByteArray → Nat → UInt8
ByteArray.get! : ByteArray → Nat → UInt8

Retrieves the byte at the indicated index. Panics if the index is out of bounds.

def

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

Copies the bytes with indices b (inclusive) to e (exclusive) to a new ByteArray.

19.17.1.4. Conversions

def

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

Converts a packed array of bytes to a linked list.

def

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

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

Panics if the array's size is not 8.

def

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

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

Panics if the array's size is not 8.

19.17.1.4.1. UTF-8

def

ByteArray.utf8Decode? (b : ByteArray) : Option (Array Char)
ByteArray.utf8Decode? (b : ByteArray) :
  Option (Array Char)

Decodes a sequence of characters from their UTF-8 representation. Returns none if the bytes are not a sequence of Unicode scalar values.

def

ByteArray.utf8DecodeChar? (bytes : ByteArray) (i : Nat) : Option Char
ByteArray.utf8DecodeChar?
  (bytes : ByteArray) (i : Nat) :
  Option Char

Decodes and returns the Char whose UTF-8 encoding begins at i in bytes.

Returns none if i is not the start of a valid UTF-8 encoding of a character.

def

ByteArray.utf8DecodeChar (bytes : ByteArray) (i : Nat)
  (h : (bytes.utf8DecodeChar? i).isSome = true) : Char
ByteArray.utf8DecodeChar
  (bytes : ByteArray) (i : Nat)
  (h :
    (bytes.utf8DecodeChar? i).isSome =
      true) :
  Char

Decodes and returns the Char whose UTF-8 encoding begins at i in bytes.

This function requires a proof that there is, in fact, a valid Char at i. utf8DecodeChar? is an alternative function that returns Option Char instead of requiring a proof ahead of time.

19.17.1.5. Modification

def

ByteArray.push : ByteArray → UInt8 → ByteArray
ByteArray.push :
  ByteArray → UInt8 → ByteArray

Adds an element to the end of an array. The resulting array's size is one greater than the input array. If there are no other references to the array, then it is modified in-place.

This takes amortized O(1) time because ByteArray is represented by a dynamic array.

def

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

Replaces the byte at the given index.

No bounds check is performed, but the function requires a proof that the index is in bounds. This proof can usually be omitted, and will be synthesized automatically.

The array is modified in-place if there are no other references to it.

def

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

Replaces the byte at the given index.

No bounds check is performed, but the function requires a proof that the index is in bounds. This proof can usually be omitted, and will be synthesized automatically.

The array is modified in-place if there are no other references to it.

def

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

Replaces the byte at the given index.

The array is modified in-place if there are no other references to it.

If the index is out of bounds, the array is returned unmodified.

19.17.1.6. Iteration

def

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

A left fold on ByteArray that iterates over an array from low to high indices, computing a running value.

Each element of the array is combined with the value from the prior elements using a function f. The initial value init is the starting value before any elements have been processed.

ByteArray.foldlM is a monadic variant of this function.

def

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

A monadic left fold on ByteArray that iterates over an array from low to high indices, computing a running value.

Each element of the array is combined with the value from the prior elements using a monadic function f. The initial value init is the starting value before any elements have been processed.

def

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

The reference implementation of ForIn.forIn for ByteArray.

In compiled code, this is replaced by the more efficient ByteArray.forInUnsafe.

19.17.1.7. Iterators

def

ByteArray.iter (arr : ByteArray) : ByteArray.Iterator
ByteArray.iter (arr : ByteArray) :
  ByteArray.Iterator

Creates an iterator at the beginning of an array.

structure

ByteArray.Iterator : Type
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.

Constructor

ByteArray.Iterator.mk

Fields

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).

def

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

The current position.

def

ByteArray.Iterator.atEnd : ByteArray.Iterator → Bool
ByteArray.Iterator.atEnd :
  ByteArray.Iterator → Bool

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

def

ByteArray.Iterator.hasNext : ByteArray.Iterator → Bool
ByteArray.Iterator.hasNext :
  ByteArray.Iterator → Bool

True if the iterator is valid; that is, it is not past the array's last byte.

def

ByteArray.Iterator.hasPrev : ByteArray.Iterator → Bool
ByteArray.Iterator.hasPrev :
  ByteArray.Iterator → Bool

True if the position is not zero.

def

ByteArray.Iterator.curr : ByteArray.Iterator → UInt8
ByteArray.Iterator.curr :
  ByteArray.Iterator → UInt8

The byte at the current position.

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

def

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

The byte at the current position. -

def

ByteArray.Iterator.next : ByteArray.Iterator → ByteArray.Iterator
ByteArray.Iterator.next :
  ByteArray.Iterator → ByteArray.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.

def

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

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

def

ByteArray.Iterator.forward :
  ByteArray.Iterator → Nat → ByteArray.Iterator
ByteArray.Iterator.forward :
  ByteArray.Iterator →
    Nat → ByteArray.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.

def

ByteArray.Iterator.nextn : ByteArray.Iterator → Nat → ByteArray.Iterator
ByteArray.Iterator.nextn :
  ByteArray.Iterator →
    Nat → ByteArray.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.

def

ByteArray.Iterator.prev : ByteArray.Iterator → ByteArray.Iterator
ByteArray.Iterator.prev :
  ByteArray.Iterator → ByteArray.Iterator

Decreases the iterator's position.

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

def

ByteArray.Iterator.prevn : ByteArray.Iterator → Nat → ByteArray.Iterator
ByteArray.Iterator.prevn :
  ByteArray.Iterator →
    Nat → ByteArray.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

ByteArray.Iterator.remainingBytes : ByteArray.Iterator → Nat
ByteArray.Iterator.remainingBytes :
  ByteArray.Iterator → Nat

The number of bytes remaining in the iterator.

def

ByteArray.Iterator.toEnd : ByteArray.Iterator → ByteArray.Iterator
ByteArray.Iterator.toEnd :
  ByteArray.Iterator → ByteArray.Iterator

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

Given i : ByteArray.Iterator, note that i.toEnd.atEnd is always true.

19.17.1.8. Slices

def

ByteArray.toByteSlice (as : ByteArray) (start : Nat := 0)
  (stop : Nat := as.size) : ByteSlice
ByteArray.toByteSlice (as : ByteArray)
  (start : Nat := 0)
  (stop : Nat := as.size) : ByteSlice

Returns a byte slice of a byte array, with the given bounds.

If start or stop are not valid bounds for a byte slice, then they are clamped to byte array's size. Additionally, the starting index is clamped to the ending index.

def

ByteSlice : Type
ByteSlice : Type

A region of some underlying byte array.

A byte slice contains a byte array together with the start and end indices of a region of interest. Byte slices can be used to avoid copying or allocating space, while being more convenient than tracking the bounds by hand. The region of interest consists of every index that is both greater than or equal to start and strictly less than stop.

def

ByteSlice.beq (a b : ByteSlice) : Bool
ByteSlice.beq (a b : ByteSlice) : Bool

Comparison function

def

ByteSlice.byteArray (xs : ByteSlice) : ByteArray
ByteSlice.byteArray (xs : ByteSlice) :
  ByteArray

The underlying byte array.

def

ByteSlice.contains (s : ByteSlice) (byte : UInt8) : Bool
ByteSlice.contains (s : ByteSlice)
  (byte : UInt8) : Bool

Checks if the byte slice contains a specific byte value.

Returns true if any byte in the slice equals the given value, false otherwise.

def

ByteSlice.empty : ByteSlice
ByteSlice.empty : ByteSlice

The empty byte slice.

This empty byte slice is backed by an empty byte array.

def

ByteSlice.foldr.{v} {β : Type v} (f : UInt8 → β → β) (init : β)
  (as : ByteSlice) : β
ByteSlice.foldr.{v} {β : Type v}
  (f : UInt8 → β → β) (init : β)
  (as : ByteSlice) : β

Folds an operation from right to left over the bytes in a byte slice.

An accumulator of type β is constructed by starting with init and combining each byte of the byte slice with the current accumulator value in turn, moving from the end to the start.

Examples:

(ByteArray.mk #[1, 2, 3]).toByteSlice.foldr (·.toNat + ·) 0 = 6
(ByteArray.mk #[1, 2, 3]).toByteSlice.popFront.foldr (·.toNat + ·) 0 = 5

def

ByteSlice.foldrM.{v, w} {β : Type v} {m : Type v → Type w} [Monad m]
  (f : UInt8 → β → m β) (init : β) (as : ByteSlice) : m β
ByteSlice.foldrM.{v, w} {β : Type v}
  {m : Type v → Type w} [Monad m]
  (f : UInt8 → β → m β) (init : β)
  (as : ByteSlice) : m β

Folds a monadic operation from right to left over the bytes in a byte slice.

An accumulator of type β is constructed by starting with init and monadically combining each byte of the byte slice with the current accumulator value in turn, moving from the end to the start. The monad in question may permit early termination or repetition.

Examples:

#eval (ByteArray.mk #[1, 2, 3]).toByteSlice.foldrM (init := 0) fun x acc =>
  some x.toNat + acc

some 6

def

ByteSlice.forM.{v, w} {m : Type v → Type w} [Monad m]
  (f : UInt8 → m PUnit) (as : ByteSlice) : m PUnit
ByteSlice.forM.{v, w}
  {m : Type v → Type w} [Monad m]
  (f : UInt8 → m PUnit) (as : ByteSlice) :
  m PUnit

Runs a monadic action on each byte of a byte slice.

The bytes are processed starting at the lowest index and moving up.

def

ByteSlice.get (s : ByteSlice) (i : Fin s.size) : UInt8
ByteSlice.get (s : ByteSlice)
  (i : Fin s.size) : UInt8

Extracts a byte from the byte slice.

The index is relative to the start of the byte slice, rather than the underlying byte array.

def

ByteSlice.get! (s : ByteSlice) (i : Nat) : UInt8
ByteSlice.get! (s : ByteSlice) (i : Nat) :
  UInt8

Extracts a byte from the byte slice, or returns a default value when the index is out of bounds.

The index is relative to the start and end of the byte slice, rather than the underlying byte array. The default value is 0.

def

ByteSlice.getD (s : ByteSlice) (i : Nat) (v₀ : UInt8) : UInt8
ByteSlice.getD (s : ByteSlice) (i : Nat)
  (v₀ : UInt8) : UInt8

Extracts a byte from the byte slice, or returns a default value v₀ when the index is out of bounds.

The index is relative to the start and end of the byte slice, rather than the underlying byte array.

def

ByteSlice.ofByteArray (ba : ByteArray) : ByteSlice
ByteSlice.ofByteArray (ba : ByteArray) :
  ByteSlice

Creates a new ByteSlice of a ByteArray

def

ByteSlice.size (s : ByteSlice) : Nat
ByteSlice.size (s : ByteSlice) : Nat

Computes the size of the byte slice.

def

ByteSlice.slice (s : ByteSlice) (start : Nat := 0)
  (stop : Nat := s.size) : ByteSlice
ByteSlice.slice (s : ByteSlice)
  (start : Nat := 0)
  (stop : Nat := s.size) : ByteSlice

Creates a sub-slice of the byte slice with the given bounds.

If start or stop are not valid bounds for a sub-slice, then they are clamped to the slice's size. Additionally, the starting index is clamped to the ending index.

The indices are relative to the current slice, not the underlying byte array.

def

ByteSlice.start (xs : ByteSlice) : Nat
ByteSlice.start (xs : ByteSlice) : Nat

The starting index of the region of interest (inclusive).

def

ByteSlice.stop (xs : ByteSlice) : Nat
ByteSlice.stop (xs : ByteSlice) : Nat

The ending index of the region of interest (exclusive).

def

ByteSlice.toByteArray (s : ByteSlice) : ByteArray
ByteSlice.toByteArray (s : ByteSlice) :
  ByteArray

Converts a byte slice back to a byte array by copying the relevant portion.

19.17.1.9. Element Predicates

def

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

Finds the index of the first byte in a for which p returns true. If no byte in a satisfies p, then the result is none.

The variant findFinIdx? additionally returns a proof that the found index is in bounds.

def

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

Finds the index of the first byte in a for which p returns true. If no byte in a satisfies p, then the result is none.

The index is returned along with a proof that it is a valid index in the array.