Grip.Scan: total scanners and repetition

The looping combinators, all total (structural on arr.size - q) rather than partial. The raw scan loops scanFwd/foldFwd/natFwd with their forward-progress lemmas, and the parsers built on them: takeWhile/takeWhile1, foldMany/many, and nat. Also the JSON string scanners: the lenient scanStrFwd/takeStringBody (escape-aware, never fails) and the strict scanStrBody/scanStrLit/stringLit (validates escapes and control bytes). The @[specialize] on each loop lets a statically-known predicate monomorphize into it. The point combinators are in Grip.Byte; the graded type and fix in Grip.Graded.

@[irreducible, specialize #[]]

def Grip.scanFwd (arr : ByteArray) (f : UInt8 → Bool) (q : Nat) : Nat

Scan forward while f holds. Total: structural on the measure arr.size - q (each step advances one byte, bounded by arr.size). @[specialize] so a known predicate (e.g. Ascii.isWs) is monomorphized into the loop rather than called indirectly per byte.

Equations

• Grip.scanFwd arr f q = if h : q < arr.size then if f arr[q] = true then Grip.scanFwd arr f (q + 1) else q else q

theorem Grip.scanFwd_ge (arr : ByteArray) (f : UInt8 → Bool) (q : Nat) : q ≤ scanFwd arr f q

scanFwd never rewinds.

theorem Grip.scanFwd_gt (arr : ByteArray) (f : UInt8 → Bool) (q : Nat) (h : q < arr.size) (hf : f arr[q] = true) : q < scanFwd arr f q

With a leading matching byte, scanFwd strictly advances.

theorem Grip.scanFwd_le (arr : ByteArray) (f : UInt8 → Bool) (q : Nat) (hq : q ≤ arr.size) : scanFwd arr f q ≤ arr.size

scanFwd stays within bounds when it starts within bounds.

@[inline]

def Grip.GParser.takeWhile (f : UInt8 → Bool) : GParser flexible Nat

Scan while f holds, returning the number of bytes consumed. Always succeeds (result is .ok).

Equations

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

@[irreducible, specialize #[]]

def Grip.scanStrFwd (arr : ByteArray) (q : Nat) : Nat

Scan a JSON-style string body: advance until an unescaped " (0x22), treating a backslash (0x5c) as an escape that consumes the next byte too. Total: structural on arr.size - q.

Equations

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

theorem Grip.scanStrFwd_ge (arr : ByteArray) (q : Nat) : q ≤ scanStrFwd arr q

scanStrFwd never rewinds.

theorem Grip.scanStrFwd_le (arr : ByteArray) (q : Nat) (hq : q ≤ arr.size) : scanStrFwd arr q ≤ arr.size

scanStrFwd stays within bounds when it starts within bounds.

@[inline]

def Grip.GParser.takeStringBody : GParser flexible Nat

Scan a JSON string body (escape-aware), returning the number of bytes consumed. Always succeeds (result is .ok). Pair with a " on each side for a full string literal.

Equations

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

@[irreducible, specialize #[]]

def Grip.scanStrBody (arr : ByteArray) (q : Nat) : Option Nat

Scan a strict RFC-8259 string body: from just after the opening " at q, advance to and past the closing ", validating escapes. Returns some end (just past the closing quote) on a well-formed body, or none on a malformed one: an unescaped control byte (< 0x20), an unknown \-escape, a \u not followed by four hex digits, or end of input before the closing quote. Total (structural on arr.size - q). Unlike scanStrFwd, this validates and can reject, so the parser built on it is conditional, not flexible.

Equations

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

theorem Grip.scanStrBody_ge (arr : ByteArray) (q q' : Nat) (h : scanStrBody arr q = some q') : q ≤ q'

A successful scanStrBody never rewinds.

theorem Grip.scanStrBody_le (arr : ByteArray) (q q' : Nat) (h : scanStrBody arr q = some q') : q' ≤ arr.size

A successful scanStrBody stays within bounds.

@[inline]

def Grip.scanStrLit (arr : ByteArray) (q : Nat) : Option Nat

Scan a strict JSON string literal starting at the opening ": some end (past the closing ") or none.

Equations

• Grip.scanStrLit arr q = if h : q < arr.size then if (arr[q] == 34) = true then Grip.scanStrBody arr (q + 1) else none else none

theorem Grip.scanStrLit_gt (arr : ByteArray) (q q' : Nat) (h : scanStrLit arr q = some q') : q < q'

A successful scanStrLit strictly advances (it consumes the opening quote).

theorem Grip.scanStrLit_le (arr : ByteArray) (q q' : Nat) (h : scanStrLit arr q = some q') : q' ≤ arr.size

A successful scanStrLit stays within bounds.

@[inline]

def Grip.GParser.stringLit : GParser conditional Nat

A validated JSON string literal "..." in one scan, returning the number of bytes consumed (both quotes included). Fails on a malformed literal (see scanStrBody). This is the strict, single-pass counterpart to ch '"' *> takeStringBody *> ch '"': it validates escapes and rejects control bytes without per-byte combinator dispatch. On failure the furthest offset is the current position.

Equations

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

@[inline]

def Grip.GParser.takeWhile1 (f : UInt8 → Bool) : GParser conditional Nat

One-or-more bytes satisfying f. On failure the furthest offset is the current position.

Equations

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

@[irreducible, specialize #[]]

def Grip.foldFwd {ge : Modality} {α β : Type} (step : β → α → β) (p : GParser { errors := ge, consumes := always } α) (arr : ByteArray) (a : β) (q : Nat) : β × Nat

Total repetition core: fold p's results into a, advancing while p succeeds and strictly consumes (in bounds). Total: structural on arr.size - q; the guard q < q' ≤ arr.size guarantees the measure drops. @[specialize] so the step and the element parser fuse into the loop when they are statically known.

Equations

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

theorem Grip.foldFwd_ge {ge : Modality} {α β : Type} (step : β → α → β) (p : GParser { errors := ge, consumes := always } α) (arr : ByteArray) (a : β) (q : Nat) : q ≤ (foldFwd step p arr a q).snd

foldFwd never rewinds.

theorem Grip.foldFwd_le {ge : Modality} {α β : Type} (step : β → α → β) (p : GParser { errors := ge, consumes := always } α) (arr : ByteArray) (a : β) (q : Nat) (hq : q ≤ arr.size) : (foldFwd step p arr a q).snd ≤ arr.size

foldFwd stays within bounds when it starts within bounds (using the element's bwit).

@[inline]

def Grip.GParser.foldMany {ge : Modality} {α β : Type} (h : β → α → β) (acc : β) (p : GParser { errors := ge, consumes := always } α) : GParser flexible β

Fold p zero-or-more times into acc (no list). Total (see foldFwd). Always succeeds (result is .ok).

Equations

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

@[irreducible, specialize #[]]

def Grip.natFwd (arr : ByteArray) (acc q : Nat) : Nat × Nat

Fold decimal digits into acc. Total: structural on arr.size - q.

Equations

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

theorem Grip.natFwd_eq (arr : ByteArray) (acc q : Nat) : natFwd arr acc q = if h : q < arr.size then if (decide (48 ≤ arr[q]) && decide (arr[q] ≤ 57)) = true then natFwd arr (acc * 10 + (arr[q].toNat - 48)) (q + 1) else (acc, q) else (acc, q)

natFwd unfolded one step with the let inlined (so split sees the branch).

theorem Grip.natFwd_ge (arr : ByteArray) (acc q : Nat) : q ≤ (natFwd arr acc q).snd

natFwd never rewinds.

theorem Grip.natFwd_gt (arr : ByteArray) (acc q : Nat) (h : q < arr.size) (hd : (decide (48 ≤ arr[q]) && decide (arr[q] ≤ 57)) = true) : q < (natFwd arr acc q).snd

With a leading digit, natFwd strictly advances.

theorem Grip.natFwd_le (arr : ByteArray) (acc q : Nat) (hq : q ≤ arr.size) : (natFwd arr acc q).snd ≤ arr.size

natFwd stays within bounds when it starts within bounds.

@[inline]

def Grip.GParser.nat : GParser conditional Nat

Parse a decimal natural number (one or more digits). Always consumes on success. On failure the furthest offset is the current position.

Equations

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

@[inline]

def Grip.GParser.many {ge : Modality} {α : Type} (p : GParser { errors := ge, consumes := always } α) : GParser flexible (List α)

Zero-or-more p (always-consuming) into a list. Total (via foldFwd). Always succeeds (result is .ok).

Equations

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