A window of a ByteArray.

structure Parser.BytesWindow (w : Nat) : Type

A w bytes window of buf[start .. start + w - 1]

• buf : ByteArray
• start : Nat
• valid : self.start + w ≤ self.buf.size

@[instance_reducible]

instance Parser.instGetElemBytesWindowNatUInt8Lt {w : Nat} : GetElem (BytesWindow w) Nat UInt8 fun (x : BytesWindow w) (i : Nat) => i < w

Equations

• Parser.instGetElemBytesWindowNatUInt8Lt = { getElem := fun (b : Parser.BytesWindow w) (i : Nat) (h : i < w) => b.buf[b.start + i] }

@[simp]

theorem Parser.BytesWindow.getElem_def {w : Nat} (b : BytesWindow w) (i : Nat) (h : i < w) : b[i] = b.buf[b.start + i]

@[reducible, inline]

abbrev Parser.BytesWindow.narrow {w : Nat} (b : BytesWindow w) (offset w' : Nat) (h : offset + w' ≤ w := by omega) : BytesWindow w'

Equations

• b.narrow offset w' h = { buf := b.buf, start := b.start + offset, valid := ⋯ }

def Parser.BytesWindow.toByteArray {w : Nat} (b : BytesWindow w) : ByteArray

Equations

• b.toByteArray = b.buf.extract b.start (b.start + w)

theorem Parser.BytesWindow.toByteArray_succ {w : Nat} (b : BytesWindow (w + 1)) : b.toByteArray = [b[0]].toByteArray ++ (b.narrow 1 w ⋯).toByteArray