Constructs a new empty byte array with initial capacity 0.

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

Constructs a new empty byte array with initial capacity c.

Appends two byte arrays.

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

Appends two byte arrays using fast array primitives instead of converting them into lists and back.

In compiled code, this function replaces calls to ByteArray.append.

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.

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.

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.

Returns true when s contains zero bytes.

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.

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.

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

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

Converts a packed array of bytes to a linked list.

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

Panics if the array's size is not 8.

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

Panics if the array's size is not 8.

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.

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.

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.

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.

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.

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.

The reference implementation of ForIn.forIn for ByteArray.

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

Creates an iterator at the beginning of an array.

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

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

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

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

True if the position is not zero.

The byte at the current position.

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

The byte at the current position. -

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.

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

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.

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.

Decreases the iterator's position.

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

Moves the iterator's position several bytes back.

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

The number of bytes remaining in the iterator.

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

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

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.

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.

Comparison function

The underlying byte array.

Checks if the byte slice contains a specific byte value.

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

The empty byte slice.

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

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

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

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

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

Extracts a byte from the byte slice.

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

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.

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.

Creates a new ByteSlice of a ByteArray

Computes the size of the byte slice.

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.

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

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

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

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.

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.