This module defines the ByteSlice structure. It's a modified version of the SubArray code, with some functions specific to ByteSlice.

structure Std.Slice.Internal.ByteSliceData : Type

Internal representation of ByteSlice, which is an abbreviation for Slice ByteSliceData.

• byteArray : ByteArray

  The underlying byte array.

• start : Nat

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

• stop : Nat

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

• start_le_stop : self.start ≤ self.stop

  The starting index is no later than the ending index.

  The ending index is exclusive. If the starting and ending indices are equal, then the byte slice is empty.

• stop_le_size_byteArray : self.stop ≤ self.byteArray.size

  The stopping index is no later than the end of the byte array.

  The ending index is exclusive. If it is equal to the size of the byte array, then the last byte of the byte array is in the byte slice.

@[reducible, inline]

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

Equations

• ByteSlice = Std.Slice Std.Slice.Internal.ByteSliceData

instance instSelfSliceByteSliceDataByteSlice : Std.Slice.Self (Std.Slice Std.Slice.Internal.ByteSliceData) ByteSlice

@[inline]

def ByteSlice.byteArray (xs : ByteSlice) : ByteArray

The underlying byte array.

Equations

• xs.byteArray = xs.internalRepresentation.byteArray

@[inline]

def ByteSlice.start (xs : ByteSlice) : Nat

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

Equations

• xs.start = xs.internalRepresentation.start

@[inline]

def ByteSlice.stop (xs : ByteSlice) : Nat

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

Equations

• xs.stop = xs.internalRepresentation.stop

theorem ByteSlice.start_le_stop (xs : ByteSlice) : xs.start ≤ xs.stop

The starting index is no later than the ending index.

The ending index is exclusive. If the starting and ending indices are equal, then the byte slice is empty.

theorem ByteSlice.stop_le_size_byteArray (xs : ByteSlice) : xs.stop ≤ xs.byteArray.size

The stopping index is no later than the end of the byte array.

The ending index is exclusive. If it is equal to the size of the byte array, then the last byte of the byte array is in the byte slice.

def ByteSlice.size (s : ByteSlice) : Nat

Computes the size of the byte slice.

Equations

• s.size = s.stop - s.start

theorem ByteSlice.size_le_size_byteArray {s : ByteSlice} : s.size ≤ s.byteArray.size

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

Equations

• s.get i = s.byteArray[s.start + ↑i]

instance ByteSlice.instGetElemNatUInt8LtSize : GetElem ByteSlice Nat UInt8 fun (xs : ByteSlice) (i : Nat) => i < xs.size

Equations

• ByteSlice.instGetElemNatUInt8LtSize = { getElem := fun (xs : ByteSlice) (i : Nat) (h : i < xs.size) => xs.get ⟨i, h⟩ }

@[inline]

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

Equations

• s.getD i v₀ = if h : i < s.size then s[i] else v₀

@[reducible, inline]

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

Equations

• s.get! i = s.getD i 0

def ByteSlice.empty : ByteSlice

The empty byte slice.

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

Equations

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

def ByteSlice.ofByteArray (ba : ByteArray) : ByteSlice

Creates a new ByteSlice of a ByteArray

Equations

• ByteSlice.ofByteArray ba = { internalRepresentation := { byteArray := ba, start := 0, stop := ba.size, start_le_stop := ⋯, stop_le_size_byteArray := ⋯ } }

instance ByteSlice.instEmptyCollection : EmptyCollection ByteSlice

Equations

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

instance ByteSlice.instInhabited : Inhabited ByteSlice

Equations

• ByteSlice.instInhabited = { default := ∅ }

def ByteSlice.toByteArray (s : ByteSlice) : ByteArray

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

Equations

• s.toByteArray = s.byteArray.extract s.start (s.start + s.size)

@[extern lean_byteslice_beq]

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

Comparison function

Equations

• a.beq b = (a.toByteArray == b.toByteArray)

instance ByteSlice.instBEq : BEq ByteSlice

Equations

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

@[inline]

def ByteSlice.foldrM {β : 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

Equations

• ByteSlice.foldrM f init as = ByteSlice.foldrM.loop✝ f as 0 init

@[inline]

def ByteSlice.forM {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.

Equations

• ByteSlice.forM f as = ByteSlice.forM.loop✝ f as 0

@[inline]

def ByteSlice.foldr {β : 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

Equations

• ByteSlice.foldr f init as = (ByteSlice.foldrM (fun (x1 : UInt8) (x2 : β) => pure (f x1 x2)) init as).run

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

Equations

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

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

Equations

• s.contains byte = ByteSlice.contains.loop✝ s byte 0

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

Equations

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

instance instSliceableByteArrayNatByteSliceOfClosedOpenIntersection {shape : Std.PRange.RangeShape} [Std.PRange.ClosedOpenIntersection shape Nat] : Std.Slice.Sliceable shape ByteArray Nat ByteSlice

Equations

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

instance instSliceableByteSliceNatOfClosedOpenIntersection {shape : Std.PRange.RangeShape} [Std.PRange.ClosedOpenIntersection shape Nat] : Std.Slice.Sliceable shape ByteSlice Nat ByteSlice

Equations

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