Main result

Introduce main properties of Up (well-ordered relation for "upwards" induction on ℕ) and of ByteArray

def Nat.Up (ub : Nat) (a : Nat) (i : Nat) : Prop

A well-ordered relation for "upwards" induction on the natural numbers up to some bound ub.

Equations

• ub.Up a i = (i < a ∧ i < ub)

theorem Nat.Up.next {ub : Nat} {i : Nat} (h : i < ub) : ub.Up (i + 1) i

theorem Nat.Up.WF (ub : Nat) : WellFounded ub.Up

def Nat.upRel (ub : Nat) : WellFoundedRelation Nat

A well-ordered relation for "upwards" induction on the natural numbers up to some bound ub.

Equations

• ub.upRel = { rel := ub.Up, wf := ⋯ }

structure ByteSliceT : Type

A terminal byte slice, a suffix of a byte array.

• arr : ByteArray
• off : Nat

@[inline]

def ByteSliceT.size (self : ByteSliceT) : Nat

The number of elements in the byte slice.

Equations

• self.size = self.arr.size - self.off

@[inline]

def ByteSliceT.getOp (self : ByteSliceT) (idx : Nat) : UInt8

Index into a byte slice. The getOp function allows the use of the buf[i] notation.

Equations

• self.getOp idx = self.arr.get! (self.off + idx)

def ByteArray.toSliceT (arr : ByteArray) : ByteSliceT

Convert a byte array into a terminal slice.

Equations

• arr.toSliceT = { arr := arr, off := 0 }

structure ByteSlice : Type

A byte slice, given by a backing byte array, and an offset and length.

• arr : ByteArray
• off : Nat
• len : Nat

def ByteSlice.toArray : ByteSlice → ByteArray

Convert a byte slice into an array, by copying the data if necessary.

Equations

• x.toArray = match x with | { arr := arr, off := off, len := len } => arr.extract off len

@[inline]

def ByteSlice.getOp (self : ByteSlice) (idx : Nat) : UInt8

Index into a byte slice. The getOp function allows the use of the buf[i] notation.

Equations

• self.getOp idx = self.arr.get! (self.off + idx)

@[irreducible]

def ByteSlice.forIn.loop {m : Type u → Type v} {β : Type u} [Monad m] (f : UInt8 → β → m (ForInStep β)) (arr : ByteArray) (off : Nat) (_end : Nat) (i : Nat) (b : β) : m β

The inner loop of the forIn implementation for byte slices.

Equations

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

instance ByteSlice.instForInUInt8 {m : Type u → Type v} : ForIn m ByteSlice UInt8

Equations

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

def ByteSliceT.toSlice : ByteSliceT → ByteSlice

Convert a terminal byte slice into a regular byte slice.

Equations

• x.toSlice = match x with | { arr := arr, off := off } => { arr := arr, off := off, len := arr.size - off }

def ByteArray.toSlice (arr : ByteArray) : ByteSlice

Convert a byte array into a byte slice.

Equations

• arr.toSlice = { arr := arr, off := 0, len := arr.size }

def String.toAsciiByteArray (s : String) : ByteArray

Convert a string of assumed-ASCII characters into a byte array. (If any characters are non-ASCII they will be reduced modulo 256.)

Equations

• s.toAsciiByteArray = String.toAsciiByteArray.loop s 0 ByteArray.empty

@[irreducible]

def String.toAsciiByteArray.loop (s : String) (p : String.Pos) (out : ByteArray) : ByteArray

Equations

• String.toAsciiByteArray.loop s p out = if h : s.atEnd p = true then out else let c := s.get p; let_fun this := ⋯; String.toAsciiByteArray.loop s (s.next p) (out.push c.toUInt8)

def ByteSlice.toString (bs : ByteSlice) : String

Convert a byte slice into a string. This does not handle non-ASCII characters correctly: every byte will become a unicode character with codepoint < 256.

Equations

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

instance instToStringByteSlice : ToString ByteSlice

Equations

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