Init.Data.ByteArray.Basic

ByteArray structure

Full source

structure ByteArray where
  data : Array UInt8

Byte Array

Informal description

The structure `ByteArray` represents an array of bytes, which is a sequence of 8-bit unsigned integers. It can be used to store binary data efficiently.

ByteArray.emptyWithCapacity definition

(c : @& Nat) : ByteArray

Full source

@[extern "lean_mk_empty_byte_array"]
def emptyWithCapacity (c : @& Nat) : ByteArray :=
  { data := #[] }

Empty byte array with specified capacity

Informal description

The function creates an empty byte array with a specified capacity `c`, where `c` is a natural number representing the number of bytes the array can hold. The actual byte array is initialized as empty (containing no bytes), but with the underlying storage allocated to accommodate up to `c` bytes.

ByteArray.mkEmpty abbrev

Full source

@[deprecated emptyWithCapacity (since := "2025-03-12")]
abbrev mkEmpty := emptyWithCapacity

Empty Byte Array

Informal description

The empty byte array, which is a byte array with zero capacity and no elements.

ByteArray.empty definition

: ByteArray

Full source

def empty : ByteArray := emptyWithCapacity 0

Empty byte array

Informal description

The empty byte array, which is a byte array with zero capacity and no elements.

ByteArray.instInhabited instance

: Inhabited ByteArray

Full source

instance : Inhabited ByteArray where
  default := empty

Byte Arrays are Inhabited

Informal description

The type of byte arrays is inhabited, with the empty byte array as its default element.

ByteArray.instEmptyCollection instance

: EmptyCollection ByteArray

Full source

instance : EmptyCollection ByteArray where
  emptyCollection := ByteArray.empty

Empty Byte Array Instance

Informal description

The type `ByteArray` has an empty collection instance, which is the empty byte array with zero capacity and no elements.

ByteArray.push definition

: ByteArray → UInt8 → ByteArray

Full source

@[extern "lean_byte_array_push"]
def push : ByteArray → UInt8 → ByteArray
  | ⟨bs⟩, b => ⟨bs.push b⟩

Append byte to byte array

Informal description

The function appends an unsigned 8-bit integer $b$ to the end of a byte array, resulting in a new byte array where $b$ is the last element.

ByteArray.size definition

: (@& ByteArray) → Nat

Full source

@[extern "lean_byte_array_size"]
def size : (@& ByteArray) → Nat
  | ⟨bs⟩ => bs.size

Size of a byte array

Informal description

The function returns the number of bytes in a byte array `bs`, which is equal to the length of its underlying array of unsigned 8-bit integers.

ByteArray.usize definition

(a : @& ByteArray) : USize

Full source

@[extern "lean_sarray_size", simp]
def usize (a : @& ByteArray) : USize :=
  a.size.toUSize

Byte array size as unsigned word-size integer

Informal description

The function converts the size of a byte array (as a natural number) to an unsigned word-size integer.

ByteArray.uget definition

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

Full source

@[extern "lean_byte_array_uget"]
def uget : (a : @& ByteArray) → (i : USize) → (h : i.toNat < a.size := by get_elem_tactic) → UInt8
  | ⟨bs⟩, i, h => bs[i]

Byte array indexing with unsigned word-size index

Informal description

The function retrieves the byte at index `i` in a byte array `a`, where `i` is a platform-dependent unsigned word-size integer. The index must satisfy the condition that its natural number representation is less than the size of the array. The byte is returned as an unsigned 8-bit integer.

ByteArray.get! definition

: (@& ByteArray) → (@& Nat) → UInt8

Full source

@[extern "lean_byte_array_get"]
def get! : (@& ByteArray) → (@& Nat) → UInt8
  | ⟨bs⟩, i => bs[i]!

Unsafe byte array indexing (with panic on out-of-bounds)

Informal description

The function retrieves the byte at index `i` in a byte array `a` as an unsigned 8-bit integer. If the index `i` is out of bounds (i.e., `i ≥ a.size`), it will panic.

ByteArray.get definition

: (a : @& ByteArray) → (i : @& Nat) → (h : i < a.size := by get_elem_tactic) → UInt8

Full source

@[extern "lean_byte_array_fget"]
def get : (a : @& ByteArray) → (i : @& Nat) → (h : i < a.size := by get_elem_tactic) → UInt8
  | ⟨bs⟩, i, _ => bs[i]

Byte array indexing

Informal description

The function retrieves the byte at index `i` in a byte array `a`, provided that `i` is less than the size of `a`. The byte is returned as an unsigned 8-bit integer.

ByteArray.instGetElemNatUInt8LtSize instance

: GetElem ByteArray Nat UInt8 fun xs i => i < xs.size

Full source

instance : GetElem ByteArray Nat UInt8 fun xs i => i < xs.size where
  getElem xs i h := xs.get i

Indexing Operation for Byte Arrays with Natural Number Indices

Informal description

The byte array type `ByteArray` supports indexing notation `xs[i]` where `xs` is a byte array, `i` is a natural number index, and the result is an unsigned 8-bit integer. The index `i` must satisfy `i < xs.size` to be valid.

ByteArray.instGetElemUSizeUInt8LtNatValToFinSize instance

: GetElem ByteArray USize UInt8 fun xs i => i.toFin < xs.size

Full source

instance : GetElem ByteArray USize UInt8 fun xs i => i.toFin < xs.size where
  getElem xs i h := xs.uget i h

Indexing Operation for Byte Arrays with Word-Size Indices

Informal description

The byte array type `ByteArray` supports indexing notation `xs[i]` where `xs` is a byte array, `i` is a platform-dependent unsigned word-size integer index, and the result is an unsigned 8-bit integer. The index `i` must satisfy that its natural number representation is less than the size of the byte array to be valid.

ByteArray.set! definition

: ByteArray → (@& Nat) → UInt8 → ByteArray

Full source

@[extern "lean_byte_array_set"]
def set! : ByteArray → (@& Nat) → UInt8 → ByteArray
  | ⟨bs⟩, i, b => ⟨bs.set! i b⟩

Destructive byte array update at index

Informal description

The function destructively updates a byte array by setting the element at index `i` (a natural number) to the unsigned 8-bit integer `b`. The operation modifies the original byte array in place. The index `i` must be within bounds (i.e., `i < bs.size`), otherwise the function will panic.

ByteArray.set definition

: (a : ByteArray) → (i : @& Nat) → UInt8 → (h : i < a.size := by get_elem_tactic) → ByteArray

Full source

@[extern "lean_byte_array_fset"]
def set : (a : ByteArray) → (i : @& Nat) → UInt8 → (h : i < a.size := by get_elem_tactic) → ByteArray
  | ⟨bs⟩, i, b, h => ⟨bs.set i b h⟩

Setting an element in a byte array

Informal description

The function takes a byte array `a`, a natural number index `i`, and an unsigned 8-bit integer `b`, and returns a new byte array where the element at index `i` is set to `b`. The index `i` must be less than the size of the byte array (ensured by the implicit proof `h`).

ByteArray.uset definition

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

Full source

@[extern "lean_byte_array_uset"]
def uset : (a : ByteArray) → (i : USize) → UInt8 → (h : i.toNat < a.size := by get_elem_tactic) → ByteArray
  | ⟨bs⟩, i, v, h => ⟨bs.uset i v h⟩

In-place modification of byte array at unsigned index

Informal description

The function modifies a byte array `a` by setting the element at index `i` (given as a platform-dependent unsigned word-size integer) to the value `v`, under the condition that the index is within bounds (i.e., `i.toNat < a.size`). The operation is performed in-place when the array reference is unique, making it as efficient as a C array write.

ByteArray.hash opaque

(a : @& ByteArray) : UInt64

Full source

@[extern "lean_byte_array_hash"]
protected opaque hash (a : @& ByteArray) : UInt64

Hash function for byte arrays

Informal description

The function `ByteArray.hash` takes a byte array `a` and returns a 64-bit unsigned integer hash value.

ByteArray.instHashable instance

: Hashable ByteArray

Full source

instance : Hashable ByteArray where
  hash := ByteArray.hash

Hashable Byte Arrays

Informal description

Every byte array can be hashed into a 64-bit unsigned integer.

ByteArray.isEmpty definition

(s : ByteArray) : Bool

Full source

def isEmpty (s : ByteArray) : Bool :=
  s.size == 0

Empty byte array check

Informal description

The function checks whether a byte array `s` is empty by verifying if its size is zero.

ByteArray.extract definition

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

Full source

def extract (a : ByteArray) (b e : Nat) : ByteArray :=
  a.copySlice b empty 0 (e - b)

Byte array extraction

Informal description

Given a byte array `a` and natural numbers `b` and `e`, the function extracts a subarray from index `b` (inclusive) to index `e` (exclusive) of `a`. The result is a new byte array containing the extracted bytes.

ByteArray.append definition

(a : ByteArray) (b : ByteArray) : ByteArray

Full source

protected def append (a : ByteArray) (b : ByteArray) : ByteArray :=
  -- we assume that `append`s may be repeated, so use asymptotic growing; use `copySlice` directly to customize
  b.copySlice 0 a a.size b.size false

Concatenation of byte arrays

Informal description

The function concatenates two byte arrays `a` and `b`, returning a new byte array consisting of the bytes from `a` followed by the bytes from `b`.

ByteArray.instAppend instance

: Append ByteArray

Full source

instance : Append ByteArray := ⟨ByteArray.append⟩

Append Operation for Byte Arrays

Informal description

The byte array type `ByteArray` is equipped with an append operation `++` that concatenates two byte arrays into a new byte array.

ByteArray.toList definition

(bs : ByteArray) : List UInt8

Full source

def toList (bs : ByteArray) : List UInt8 :=
  let rec loop (i : Nat) (r : List UInt8) :=
    if i < bs.size then
      loop (i+1) (bs.get! i :: r)
    else
      r.reverse
    termination_by bs.size - i
    decreasing_by decreasing_trivial_pre_omega
  loop 0 []

Conversion from byte array to list of bytes

Informal description

The function converts a byte array `bs` into a list of unsigned 8-bit integers by iterating through each byte in the array and collecting them into a list in the same order.

ByteArray.forIn definition

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

Full source

/-- Reference implementation for `forIn` -/
@[implemented_by ByteArray.forInUnsafe]
protected def forIn {β : Type v} {m : Type v → Type w} [Monad m] (as : ByteArray) (b : β) (f : UInt8 → β → m (ForInStep β)) : m β :=
  let rec loop (i : Nat) (h : i ≤ as.size) (b : β) : m β := do
    match i, h with
    | 0,   _ => pure b
    | i+1, h =>
      have h' : i < as.size            := Nat.lt_of_lt_of_le (Nat.lt_succ_self i) h
      have : as.size - 1 < as.size     := Nat.sub_lt (Nat.zero_lt_of_lt h') (by decide)
      have : as.size - 1 - i < as.size := Nat.lt_of_le_of_lt (Nat.sub_le (as.size - 1) i) this
      match (← f as[as.size - 1 - i] b) with
      | ForInStep.done b  => pure b
      | ForInStep.yield b => loop i (Nat.le_of_lt h') b
  loop as.size (Nat.le_refl _) b

Reverse iteration over byte arrays

Informal description

The function `ByteArray.forIn` implements iteration over a byte array `as` in reverse order, applying a monadic function `f` to each byte (of type `UInt8`) and an accumulator `b` (of type `β`). The iteration starts from the last byte of the array and proceeds to the first. The function `f` returns a `ForInStep β` value, which determines whether to continue iteration (`yield`) or terminate early (`done`). The final result is the accumulator after processing all bytes (or until early termination). More precisely, given: - A monad `m` - A byte array `as : ByteArray` - An initial accumulator value `b : β` - A function `f : UInt8 → β → m (ForInStep β)` The function processes bytes in reverse order (from index `as.size - 1` down to 0), applying `f` to each byte and the current accumulator. If `f` returns `ForInStep.done b'`, iteration stops immediately with result `b'`. If `f` returns `ForInStep.yield b'`, iteration continues with the next byte (moving left) and the new accumulator `b'`.

ByteArray.instForInUInt8 instance

: ForIn m ByteArray UInt8

Full source

instance : ForIn m ByteArray UInt8 where
  forIn := ByteArray.forIn

Reverse Monadic Iteration over Byte Arrays

Informal description

For any monad `m`, the byte array type `ByteArray` supports monadic iteration over its elements (of type `UInt8`) in reverse order. This means we can use the `for x in xs` notation in `do`-blocks to iterate through a byte array from the last byte to the first.

ByteArray.Iterator structure

Full source

/-- 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.
-/
structure Iterator where
  /-- The array the iterator is for. -/
  array : ByteArray
  /-- 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)`. -/
  idx : Nat
  deriving Inhabited

Byte Array Iterator

Informal description

An iterator over the bytes (represented as `UInt8`) of a `ByteArray`. An iterator is valid if its position `i` satisfies `0 ≤ i ≤ arr.size` for the underlying byte array `arr`. Most operations on iterators return arbitrary values if the iterator is invalid, except for `Iterator.next` (invalid if already at the end) and `Iterator.forward`/`Iterator.nextn` (invalid if the step size exceeds remaining bytes).

ByteArray.instInhabitedIterator instance

: Inhabited✝ (@ByteArray.Iterator)

Full source

Inhabited

Byte Array Iterators are Inhabited

Informal description

The type of byte array iterators is inhabited, with a default iterator.

ByteArray.mkIterator definition

(arr : ByteArray) : Iterator

Full source

/-- Creates an iterator at the beginning of an array. -/
def mkIterator (arr : ByteArray) : Iterator :=
  ⟨arr, 0⟩

Byte array iterator initialization

Informal description

The function creates an iterator for a given byte array, initialized to the start of the array (position 0).

ByteArray.iter abbrev

Full source

@[inherit_doc mkIterator]
abbrev iter := mkIterator

Byte Array Iterator Initialization

Informal description

The abbreviation `ByteArray.iter` provides a concise way to create an iterator for a given byte array, initialized to the start of the array (position 0). It is equivalent to calling `ByteArray.mkIterator`.

ByteArray.instSizeOfIterator instance

: SizeOf Iterator

Full source

/-- The size of an array iterator is the number of bytes remaining. -/
instance : SizeOf Iterator where
  sizeOf i := i.array.size - i.idx

Size of Byte Array Iterator as Remaining Bytes

Informal description

For any byte array iterator, its size is defined as the number of bytes remaining in the iterator, which is equal to the size of the underlying byte array minus the current position of the iterator.

ByteArray.Iterator.sizeOf_eq theorem

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

Full source

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

Size of Byte Array Iterator Equals Remaining Bytes

Informal description

For any byte array iterator $i$, the size of $i$ is equal to the size of the underlying byte array minus the current position index of the iterator, i.e., $\text{sizeOf}(i) = \text{array.size}(i) - \text{idx}(i)$.

ByteArray.Iterator.remainingBytes definition

: Iterator → Nat

Full source

/-- Number of bytes remaining in the iterator. -/
def remainingBytes : Iterator → Nat
  | ⟨arr, i⟩ => arr.size - i

Remaining bytes in byte array iterator

Informal description

Given an iterator `i` over a byte array, the function returns the number of bytes remaining to be iterated, computed as the difference between the size of the underlying byte array and the current position of the iterator.

ByteArray.Iterator.pos definition

Full source

@[inherit_doc Iterator.idx]
def pos := Iterator.idx

Current position of byte array iterator

Informal description

The function returns the current position (index) of the iterator within the byte array. The position is represented as a natural number indicating the current byte being pointed to by the iterator.

ByteArray.Iterator.curr definition

: Iterator → UInt8

Full source

/-- The byte at the current position.

On an invalid position, returns `(default : UInt8)`. -/
@[inline]
def curr : Iterator → UInt8
  | ⟨arr, i⟩ =>
    if h : i < arr.size then
      arr[i]'h
    else
      default

Current byte in byte array iterator

Informal description

The function returns the byte at the current position of the iterator. If the iterator's position is valid (i.e., less than the size of the underlying byte array), it returns the corresponding byte; otherwise, it returns the default value for `UInt8` (which is 0).

ByteArray.Iterator.next definition

: Iterator → Iterator

Full source

/-- 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 next : Iterator → Iterator
  | ⟨arr, i⟩ => ⟨arr, i + 1⟩

Advance byte array iterator by one byte

Informal description

Given a byte array iterator, this function advances the iterator's position by one byte, returning a new iterator. The function is only valid to call when the iterator is not at the end of the array (i.e., `Iterator.atEnd` is `false`); otherwise, the resulting iterator will be invalid.

ByteArray.Iterator.prev definition

: Iterator → Iterator

Full source

/-- Decreases the iterator's position.

If the position is zero, this function is the identity. -/
@[inline]
def prev : Iterator → Iterator
  | ⟨arr, i⟩ => ⟨arr, i - 1⟩

Decrement byte array iterator position

Informal description

Given a byte array iterator, this function returns a new iterator with its position decremented by 1. If the current position is already at the beginning (position 0), the function returns the iterator unchanged.

ByteArray.Iterator.atEnd definition

: Iterator → Bool

Full source

/-- True if the iterator is past the array's last byte. -/
@[inline]
def atEnd : Iterator → Bool
  | ⟨arr, i⟩ => i ≥ arr.size

Check if byte array iterator is at end

Informal description

Given a byte array iterator `it`, the function returns `true` if the iterator's current position is past the last byte of the array (i.e., if the position index `i` is greater than or equal to the size of the byte array), and `false` otherwise.

ByteArray.Iterator.hasNext definition

: Iterator → Bool

Full source

/-- True if the iterator is not past the array's last byte. -/
@[inline]
def hasNext : Iterator → Bool
  | ⟨arr, i⟩ => i < arr.size

Check if byte array iterator has more bytes

Informal description

Given a byte array iterator `it`, the function returns `true` if the iterator's current position `i` is strictly less than the size of the byte array (i.e., there are more bytes to iterate over), and `false` otherwise.

ByteArray.Iterator.curr' definition

(it : Iterator) (h : it.hasNext) : UInt8

Full source

/-- The byte at the current position. --/
@[inline]
def curr' (it : Iterator) (h : it.hasNext) : UInt8 :=
  match it with
  | ⟨arr, i⟩ =>
    have : i < arr.size := by
      simp only [hasNext, decide_eq_true_eq] at h
      assumption
    arr[i]

Current byte of a byte array iterator

Informal description

Given a byte array iterator `it` and a proof `h` that the iterator has more bytes to process (i.e., `it.hasNext` is true), the function returns the byte at the current position of the iterator as an unsigned 8-bit integer.

ByteArray.Iterator.next' definition

(it : Iterator) (_h : it.hasNext) : Iterator

Full source

/-- Moves the iterator's position forward by one byte. --/
@[inline]
def next' (it : Iterator) (_h : it.hasNext) : Iterator :=
  match it with
  | ⟨arr, i⟩ => ⟨arr, i + 1⟩

Advance byte array iterator by one byte

Informal description

Given a byte array iterator `it` that has more bytes to iterate over (i.e., `it.hasNext` is `true`), the function returns a new iterator with its position advanced by one byte.

ByteArray.Iterator.hasPrev definition

: Iterator → Bool

Full source

/-- True if the position is not zero. -/
@[inline]
def hasPrev : Iterator → Bool
  | ⟨_, i⟩ => i > 0

Check if byte array iterator has a previous position

Informal description

Given a byte array iterator, the function returns `true` if the iterator's current position is not at the beginning (i.e., the position is greater than 0), and `false` otherwise.

ByteArray.Iterator.toEnd definition

: Iterator → Iterator

Full source

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

Note that `i.toEnd.atEnd` is always `true`. -/
@[inline]
def toEnd : Iterator → Iterator
  | ⟨arr, _⟩ => ⟨arr, arr.size⟩

Move iterator to end of byte array

Informal description

Given a byte array iterator, the function returns a new iterator with its position set to the end of the array. The resulting iterator satisfies `i.atEnd = true`.

ByteArray.Iterator.forward definition

: Iterator → Nat → Iterator

Full source

/-- 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 forward : Iterator → Nat → Iterator
  | ⟨arr, i⟩, f => ⟨arr, i + f⟩

Advance byte array iterator by `n` bytes

Informal description

Given a byte array iterator and a natural number `n`, the function returns a new iterator with its position advanced by `n` bytes. The resulting iterator is only valid if `n` does not exceed the number of remaining bytes in the iterator.

ByteArray.Iterator.nextn definition

: Iterator → Nat → Iterator

Full source

@[inherit_doc forward, inline]
def nextn : Iterator → Nat → Iterator := forward

Advance byte array iterator by `n` bytes

Informal description

The function takes a byte array iterator and a natural number `n`, and returns a new iterator with its position advanced by `n` bytes. The resulting iterator is only valid if `n` does not exceed the number of remaining bytes in the iterator.

ByteArray.Iterator.prevn definition

: Iterator → Nat → Iterator

Full source

/-- Moves the iterator's position several bytes back.

If asked to go back more bytes than available, stops at the beginning of the array. -/
@[inline]
def prevn : Iterator → Nat → Iterator
  | ⟨arr, i⟩, f => ⟨arr, i - f⟩

Move byte array iterator back by `n` bytes

Informal description

Given a byte array iterator and a natural number `n`, the function returns a new iterator with its position moved back by `n` bytes. If `n` exceeds the current position, the iterator is set to the beginning of the array (position 0).

List.toByteArray definition

(bs : List UInt8) : ByteArray

Full source

/--
Converts a list of bytes into a `ByteArray`.
-/
def List.toByteArray (bs : List UInt8) : ByteArray :=
  let rec loop
    | [],    r => r
    | b::bs, r => loop bs (r.push b)
  loop bs ByteArray.empty

Conversion from list of bytes to byte array

Informal description

The function converts a list of unsigned 8-bit integers (bytes) into a `ByteArray` by iteratively appending each byte to an initially empty byte array.

instToStringByteArray instance

: ToString ByteArray

Full source

instance : ToString ByteArray := ⟨fun bs => bs.toList.toString⟩

String Representation of Byte Arrays

Informal description

The structure `ByteArray` has a canonical string representation.

ByteArray.toUInt64LE! definition

(bs : ByteArray) : UInt64

Full source

/-- Interpret a `ByteArray` of size 8 as a little-endian `UInt64`. -/
def ByteArray.toUInt64LE! (bs : ByteArray) : UInt64 :=
  assert! bs.size == 8
  (bs.get! 7).toUInt64 <<< 0x38 |||
  (bs.get! 6).toUInt64 <<< 0x30 |||
  (bs.get! 5).toUInt64 <<< 0x28 |||
  (bs.get! 4).toUInt64 <<< 0x20 |||
  (bs.get! 3).toUInt64 <<< 0x18 |||
  (bs.get! 2).toUInt64 <<< 0x10 |||
  (bs.get! 1).toUInt64 <<< 0x8  |||
  (bs.get! 0).toUInt64

Little-endian byte array to 64-bit unsigned integer conversion

Informal description

Given a byte array `bs` of size 8, the function interprets the bytes as a little-endian 64-bit unsigned integer. Specifically, it constructs the integer by combining the bytes in reverse order (from index 7 to 0), shifting each byte to its appropriate position and performing bitwise OR operations to merge them. Mathematically, the result is computed as: \[ \sum_{i=0}^{7} (\text{bs.get! } i) \times 2^{8i} \] where `bs.get! i` retrieves the byte at index `i` (0-based) in the byte array `bs`.

ByteArray.toUInt64BE! definition

(bs : ByteArray) : UInt64

Full source

/-- Interpret a `ByteArray` of size 8 as a big-endian `UInt64`. -/
def ByteArray.toUInt64BE! (bs : ByteArray) : UInt64 :=
  assert! bs.size == 8
  (bs.get! 0).toUInt64 <<< 0x38 |||
  (bs.get! 1).toUInt64 <<< 0x30 |||
  (bs.get! 2).toUInt64 <<< 0x28 |||
  (bs.get! 3).toUInt64 <<< 0x20 |||
  (bs.get! 4).toUInt64 <<< 0x18 |||
  (bs.get! 5).toUInt64 <<< 0x10 |||
  (bs.get! 6).toUInt64 <<< 0x8  |||
  (bs.get! 7).toUInt64

Big-endian unsigned 64-bit integer from byte array

Informal description

Given a byte array `bs` of size 8, the function interprets `bs` as a big-endian unsigned 64-bit integer by combining the bytes as follows: \[ (\text{bs}[0] \ll 56) \lor (\text{bs}[1] \ll 48) \lor (\text{bs}[2] \ll 40) \lor (\text{bs}[3] \ll 32) \lor (\text{bs}[4] \ll 24) \lor (\text{bs}[5] \ll 16) \lor (\text{bs}[6] \ll 8) \lor \text{bs}[7] \] where `$\ll$` denotes left shift and `$\lor$` denotes bitwise OR. The function panics if the byte array does not have exactly 8 elements.