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.

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

@[inline]

def ByteSlice.byteArray (xs : ByteSlice) : ByteArray

The underlying byte array.

@[inline]

def ByteSlice.start (xs : ByteSlice) : Nat

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

@[inline]

def ByteSlice.stop (xs : ByteSlice) : Nat

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

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.

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.

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

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

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

def ByteSlice.empty : ByteSlice

The empty byte slice.

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

def ByteSlice.ofByteArray (ba : ByteArray) : ByteSlice

Creates a new ByteSlice of a ByteArray

instance ByteSlice.instEmptyCollection : EmptyCollection ByteSlice

instance ByteSlice.instInhabited : Inhabited ByteSlice

def ByteSlice.toByteArray (s : ByteSlice) : ByteArray

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

@[extern lean_byteslice_beq]

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

Comparison function

instance ByteSlice.instBEq : BEq ByteSlice

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

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

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

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.

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.

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.

instance instSliceableByteArrayNatByteSlice : Std.Rcc.Sliceable ByteArray Nat ByteSlice

instance instSliceableByteArrayNatByteSlice_1 : Std.Rco.Sliceable ByteArray Nat ByteSlice

instance instSliceableByteArrayNatByteSlice_2 : Std.Rci.Sliceable ByteArray Nat ByteSlice

instance instSliceableByteArrayNatByteSlice_3 : Std.Roc.Sliceable ByteArray Nat ByteSlice

instance instSliceableByteArrayNatByteSlice_4 : Std.Roo.Sliceable ByteArray Nat ByteSlice

instance instSliceableByteArrayNatByteSlice_5 : Std.Roi.Sliceable ByteArray Nat ByteSlice

instance instSliceableByteArrayNatByteSlice_6 : Std.Ric.Sliceable ByteArray Nat ByteSlice

instance instSliceableByteArrayNatByteSlice_7 : Std.Rio.Sliceable ByteArray Nat ByteSlice

instance instSliceableByteArrayNatByteSlice_8 : Std.Rii.Sliceable ByteArray Nat ByteSlice

instance instSliceableByteSliceNat : Std.Rcc.Sliceable ByteSlice Nat ByteSlice

instance instSliceableByteSliceNat_1 : Std.Rco.Sliceable ByteSlice Nat ByteSlice

instance instSliceableByteSliceNat_2 : Std.Rci.Sliceable ByteSlice Nat ByteSlice

instance instSliceableByteSliceNat_3 : Std.Roc.Sliceable ByteSlice Nat ByteSlice

instance instSliceableByteSliceNat_4 : Std.Roo.Sliceable ByteSlice Nat ByteSlice

instance instSliceableByteSliceNat_5 : Std.Roi.Sliceable ByteSlice Nat ByteSlice

instance instSliceableByteSliceNat_6 : Std.Ric.Sliceable ByteSlice Nat ByteSlice

instance instSliceableByteSliceNat_7 : Std.Rio.Sliceable ByteSlice Nat ByteSlice

instance instSliceableByteSliceNat_8 : Std.Rii.Sliceable ByteSlice Nat ByteSlice