def ByteArray.instBEq.beq : ByteArray → ByteArray → Bool

Equations

• ByteArray.instBEq.beq { data := a } { data := b } = (a == b)
• ByteArray.instBEq.beq x✝¹ x✝ = false

instance ByteArray.instBEq : BEq ByteArray

Equations

• ByteArray.instBEq = { beq := ByteArray.instBEq.beq }

theorem ByteArray.ext_iff {x y : ByteArray} : x = y ↔ x.data = y.data

instance ByteArray.instDecidableEq : DecidableEq ByteArray

Equations

• x✝¹.instDecidableEq x✝ = decidable_of_decidable_of_iff ⋯

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

abbrev ByteArray.mkEmpty (c : Nat) : ByteArray

Equations

• ByteArray.mkEmpty = ByteArray.emptyWithCapacity

instance ByteArray.instInhabited : Inhabited ByteArray

Equations

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

instance ByteArray.instEmptyCollection : EmptyCollection ByteArray

Equations

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

@[extern lean_sarray_size]

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

Equations

• a.usize = a.size.toUSize

@[extern lean_byte_array_uget]

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

Equations

• { data := bs }.uget x✝¹ x✝ = bs[x✝¹]

@[extern lean_byte_array_get]

def ByteArray.get! : ByteArray → Nat → UInt8

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

Equations

• { data := bs }.get! x✝ = bs[x✝]!

@[extern lean_byte_array_fget]

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

Equations

• { data := bs }.get x✝¹ x✝ = bs[x✝¹]

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.instGetElemUSizeUInt8LtNatValToFinSize : GetElem ByteArray USize UInt8 fun (xs : ByteArray) (i : USize) => ↑i.toFin < xs.size

Equations

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

@[extern lean_byte_array_set]

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

Equations

• { data := bs }.set! x✝¹ x✝ = { data := bs.set! x✝¹ x✝ }

@[extern lean_byte_array_fset]

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

Equations

• { data := bs }.set x✝² x✝¹ x✝ = { data := bs.set x✝² x✝¹ x✝ }

@[extern lean_byte_array_uset]

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

Equations

• { data := bs }.uset x✝² x✝¹ x✝ = { data := bs.uset x✝² x✝¹ x✝ }

@[extern lean_byte_array_hash]

opaque ByteArray.hash (a : ByteArray) : UInt64

Computes a hash for a ByteArray.

instance ByteArray.instHashable : Hashable ByteArray

Equations

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

def ByteArray.isEmpty (s : ByteArray) : Bool

Returns true when s contains zero bytes.

Equations

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

@[extern lean_byte_array_copy_slice]

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

Equations

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

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

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

Equations

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

@[inline]

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

Equations

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

@[simp]

theorem ByteArray.size_data {a : ByteArray} : a.data.size = a.size

@[csimp]

theorem ByteArray.append_eq_fastAppend : ByteArray.append = ByteArray.fastAppend

instance ByteArray.instAppend : Append ByteArray

Equations

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

@[simp]

theorem ByteArray.append_eq {a b : ByteArray} : a.append b = a ++ b

@[simp]

theorem ByteArray.fastAppend_eq {a b : ByteArray} : a.fastAppend b = a ++ b

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

Converts a packed array of bytes to a linked list.

Equations

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

@[irreducible]

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

Equations

• ByteArray.toList.loop bs i r = if i < bs.size then ByteArray.toList.loop bs (i + 1) (bs.get! i :: r) else r.reverse

@[inline]

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

Equations

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

@[irreducible, specialize #[]]

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

Equations

• ByteArray.findFinIdx?.loop a p i = if h : i < a.size then if p a[i] = true then some ⟨i, h⟩ else ByteArray.findFinIdx?.loop a p (i + 1) else none

@[inline]

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

Equations

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

@[irreducible, specialize #[]]

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

Equations

• ByteArray.findIdx?.loop a p i = if h : i < a.size then if p a[i] = true then some i else ByteArray.findIdx?.loop a p (i + 1) else none

@[inline]

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

An efficient implementation of ForIn.forIn for ByteArray that uses USize rather than Nat for indices.

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

Equations

• as.forInUnsafe b f = ByteArray.forInUnsafe.loop as f as.usize 0 b

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

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 β

The reference implementation of ForIn.forIn for ByteArray.

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

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.10} [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 : Nat := 0) (stop : Nat := as.size) : m β

An efficient implementation of a monadic left fold on for ByteArray that uses USize rather than Nat for indices.

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

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

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

Equations

• ByteArray.foldl f init as start stop = (ByteArray.foldlM (fun (x1 : β) (x2 : UInt8) => pure (f x1 x2)) init as start stop).run

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

def ByteArray.instInhabitedIterator.default : Iterator

Equations

• ByteArray.instInhabitedIterator.default = { array := default, idx := default }

instance ByteArray.instInhabitedIterator : Inhabited Iterator

Equations

• ByteArray.instInhabitedIterator = { default := ByteArray.instInhabitedIterator.default }

def ByteArray.mkIterator (arr : ByteArray) : Iterator

Creates an iterator at the beginning of an array.

Equations

• arr.mkIterator = { array := arr, idx := 0 }

@[reducible, inline]

abbrev ByteArray.iter (arr : ByteArray) : Iterator

Creates an iterator at the beginning of an array.

Equations

• ByteArray.iter = ByteArray.mkIterator

instance ByteArray.instSizeOfIterator : SizeOf Iterator

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

Equations

• ByteArray.instSizeOfIterator = { sizeOf := fun (i : ByteArray.Iterator) => i.array.size - i.idx }

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

def ByteArray.Iterator.remainingBytes : Iterator → Nat

The number of bytes remaining in the iterator.

Equations

• { array := arr, idx := i }.remainingBytes = arr.size - i

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

Equations

• ByteArray.Iterator.pos = ByteArray.Iterator.idx

@[inline]

def ByteArray.Iterator.atEnd : Iterator → Bool

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

Equations

• { array := arr, idx := i }.atEnd = decide (i ≥ arr.size)

@[inline]

def ByteArray.Iterator.curr : Iterator → UInt8

The byte at the current position.

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

Equations

• { array := arr, idx := i }.curr = if h : i < arr.size then arr[i] else default

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

Equations

• { array := arr, idx := i }.next = { array := arr, idx := i + 1 }

@[inline]

def ByteArray.Iterator.prev : Iterator → Iterator

Decreases the iterator's position.

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

Equations

• { array := arr, idx := i }.prev = { array := arr, idx := i - 1 }

@[inline]

def ByteArray.Iterator.hasNext : Iterator → Bool

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

Equations

• { array := arr, idx := i }.hasNext = decide (i < arr.size)

@[inline]

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

The byte at the current position. -

Equations

• { array := arr, idx := i }.curr' h_2 = arr[i]

@[inline]

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

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

Equations

• { array := arr, idx := i }.next' h_1 = { array := arr, idx := i + 1 }

@[inline]

def ByteArray.Iterator.hasPrev : Iterator → Bool

True if the position is not zero.

Equations

• { array := arr, idx := i }.hasPrev = decide (i > 0)

@[inline]

def ByteArray.Iterator.toEnd : Iterator → Iterator

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

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

Equations

• { array := arr, idx := i }.toEnd = { array := arr, idx := arr.size }

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

Equations

• { array := arr, idx := i }.forward x✝ = { array := arr, idx := i + x✝ }

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

Equations

• ByteArray.Iterator.nextn = ByteArray.Iterator.forward

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

Equations

• { array := arr, idx := i }.prevn x✝ = { array := arr, idx := i - x✝ }

instance instToStringByteArray : ToString ByteArray

Equations

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