structure ByteArray : Type

• data : Array UInt8

@[extern lean_mk_empty_byte_array]

def ByteArray.emptyWithCapacity (c : Nat) : ByteArray

Equations

• ByteArray.emptyWithCapacity c = { data := #[] }

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

abbrev ByteArray.mkEmpty (c : Nat) : ByteArray

Equations

• ByteArray.mkEmpty = ByteArray.emptyWithCapacity

def ByteArray.empty : ByteArray

Equations

• ByteArray.empty = ByteArray.emptyWithCapacity 0

instance ByteArray.instInhabited : Inhabited ByteArray

Equations

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

instance ByteArray.instEmptyCollection : EmptyCollection ByteArray

Equations

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

@[extern lean_byte_array_push]

def ByteArray.push : ByteArray → UInt8 → ByteArray

Equations

• { data := bs }.push x✝ = { data := bs.push x✝ }

@[extern lean_byte_array_size]

def ByteArray.size : ByteArray → Nat

Equations

• { data := bs }.size = bs.size

@[extern lean_sarray_size]

def ByteArray.usize (a : ByteArray) : USize

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

Equations

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

@[extern lean_byte_array_get]

def ByteArray.get! : ByteArray → Nat → UInt8

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

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

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

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

Equations

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

@[extern lean_byte_array_hash]

opaque ByteArray.hash (a : ByteArray) : UInt64

instance ByteArray.instHashable : Hashable ByteArray

Equations

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

def ByteArray.isEmpty (s : ByteArray) : Bool

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

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 e : Nat) : ByteArray

Equations

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

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

Equations

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

instance ByteArray.instAppend : Append ByteArray

Equations

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

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

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.findIdx? (a : ByteArray) (p : UInt8 → Bool) (start : Nat := 0) : Option Nat

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]

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

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]

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.

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 β

Reference implementation for forIn

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 β

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

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} [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) : β

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

instance ByteArray.instInhabitedIterator : Inhabited Iterator

Equations

• ByteArray.instInhabitedIterator = { default := { array := default, idx := 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

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.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.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.hasNext : Iterator → Bool

True if the iterator 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.

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✝ }

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

Converts a list of bytes into a ByteArray.

Equations

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

instance instToStringByteArray : ToString ByteArray

Equations

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

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.