Grip.Graded: the graded byte-parser type

GParser g α is a run : ByteArray -> Nat -> ParseResult α (ok value pos | error e, one heap object per successful step, no reified tree) plus five erased Prop witnesses tying the static Grade (error x consumption Modality) to that runtime:

• cwit: a success advances the offset exactly as consumes claims,
• ewit: an always-error grade never succeeds (every input yields .error k),
• swit: a never-error grade always succeeds (every input yields .ok a q'),
• bwit: a success that starts in bounds ends in bounds,
• fwit: a failure that starts in bounds reports a position between the start and EOF.

The witnesses erase, so run stays the bare ParseResult fast path. The failure bound keeps ordered-choice diagnostics inside the interval being parsed; it does not prove that a client-provided position is the furthest point actually reached.

This module has the type, the grade-weakening coercion, and the total, fuel-bounded fix combinator. The point combinators live in Grip.Byte, the total scanners in Grip.Scan. No mathlib.

structure Grip.GParser (g : Grade) (α : Type) : Type

A byte-level parser with static grade g, producing α. Successful and failed endpoints from an in-bounds start are bounded by erased contracts. Built-in choice compares Err.pos, but the type proves only its interval, not that every client parser reports an honest furthest point.

The five Prop fields are the parser soundness witnesses; they are erased at runtime (proof-irrelevant, carrying no data), so run is the whole runtime cost.

• run : ByteArray → Nat → ParseResult α

  Run the parser at an offset, returning .ok value newOffset on success or .error e on failure.

• cwit {arr : ByteArray} {q : Nat} {a : α} {q' : Nat} : self.run arr q = ParseResult.ok a q' → consumptionWitness q q' g.consumes

  Consumption soundness: a successful parse advances the offset exactly as the grade's consumes component claims (always ⇒ q<q', possibly ⇒ q≤q', never ⇒ q=q').

• ewit : g.errors = always → ∀ (arr : ByteArray) (q : Nat), ∃ (e : Err), self.run arr q = ParseResult.error e

  Error soundness, must-fail direction: a grade claiming always-error never succeeds: for every input there exists a failure e.

• swit : g.errors = never → ∀ (arr : ByteArray) (q : Nat), ∃ (a : α), ∃ (q' : Nat), self.run arr q = ParseResult.ok a q'

  Error soundness, must-succeed direction: a grade claiming never-error always succeeds: for every input there exist a value a and next offset q'.

• bwit {arr : ByteArray} {q : Nat} {a : α} {q' : Nat} : q ≤ arr.size → self.run arr q = ParseResult.ok a q' → q' ≤ arr.size

  Bounds soundness: a success that starts in bounds ends in bounds (q ≤ arr.size ⇒ q' ≤ arr.size). Erased, proof-irrelevant. This is the invariant every real combinator satisfies; carrying it in the type makes the impossible grade ⟨never, always⟩ uninhabited outright, with no external hypothesis (see grip-props).

• fwit {arr : ByteArray} {q : Nat} {e : Err} : q ≤ arr.size → self.run arr q = ParseResult.error e → q ≤ e.pos ∧ e.pos ≤ arr.size

  Failure-position soundness: a failure from an in-bounds start reports a position no earlier than that start and no later than EOF. This bounds choice diagnostics and makes the absolute-position/remaining-size correspondence lawful without changing runtime data.

Grade-algebra witness helper lemmas

theorem Grip.cw_seq {c0 c1 : Modality} {q r s : Nat} (w0 : consumptionWitness q r c0) (w1 : consumptionWitness r s c1) : consumptionWitness q s (max c0 c1)

Chain two consumption witnesses across a shared midpoint. Used by the sequencing combinators in Grip.Byte.

theorem Grip.GParser.errors_ne_always {g : Grade} {α : Type} (p : GParser g α) {arr : ByteArray} {q : Nat} {a : α} {q' : Nat} (h : p.run arr q = ParseResult.ok a q') : g.errors ≠ always

A success rules out the always-error grade (via ewit).

theorem Grip.GParser.errors_ne_never {g : Grade} {α : Type} (p : GParser g α) {arr : ByteArray} {q : Nat} {e : Err} (h : p.run arr q = ParseResult.error e) : g.errors ≠ never

A failure rules out the never-error grade (via swit).

Running

@[inline]

def Grip.GParser.run? {g : Grade} {α : Type} (p : GParser g α) (arr : ByteArray) : Option α

Run a parser from offset 0, returning some value on success and none on failure. The error payload is discarded; use GParser.parse (in Grip.Parser) for a positioned ParseError.

Equations

• p.run? arr = match p.run arr 0 with | Grip.ParseResult.ok a newOffset => some a | Grip.ParseResult.error a => none

Grade weakening

@[inline]

def Grip.GParser.weaken {α : Type} {g g' : Grade} (p : GParser g α) (hc : ∀ {n m : Nat}, consumptionWitness n m g.consumes → consumptionWitness n m g'.consumes) (hew : g'.errors = always → g.errors = always) (hsw : g'.errors = never → g.errors = never) : GParser g' α

Weaken a GParser g α to a less-precise grade g'.

Proofs required:

• hc: a success that satisfies g.consumes also satisfies g'.consumes
• hew: g'.errors = always implies g.errors = always (preserves must-fail)
• hsw: g'.errors = never implies g.errors = never (preserves must-succeed)

Equations

• p.weaken hc hew hsw = { run := p.run, cwit := ⋯, ewit := ⋯, swit := ⋯, bwit := ⋯, fwit := ⋯ }

@[inline]

def Grip.GParser.weakenFallible {α : Type} {g : Grade} (p : GParser g α) : GParser fallible α

Weaken any parser to fallible (errors = possibly, consumes = possibly), losing all grade precision. Used by the ungraded Parser layer.

Equations

• p.weakenFallible = p.weaken ⋯ ⋯ ⋯

Recursion via a fixpoint

GParser.fix ties the knot on a parser transformer, giving the body a reference back to the whole parser so recursive grammars can be written from combinators. The self-reference is conditional (always-consuming), so a well-behaved grammar shrinks the input before each recursive call.

grip's byte core is not size-indexed: run is ByteArray → Nat → ParseResult, with no length in the type, so the kernel cannot see the offset measure arr.size - q decrease through the opaque transformer f. Rather than fall back to partial def, fix recurses on an explicit fuel (GParser.fixFuel), structurally decreasing, with the fuel set to the bytes remaining (arr.size - q + 1). A runtime clamp downgrades any non-advancing success to a failure, so every self-success advances the offset; the productive nesting depth is therefore bounded by the bytes remaining. A separate Guarded proof establishes that the chosen fuel does not truncate acceptance for a particular body. Direct left recursion exhausts the fuel and fails; arbitrary non-guarded bodies remain total but may be fuel-sensitive. This replaces the partial loop the implementation once had; see grip-props/GripProps/FixComplete.lean.

@[inline]

def Grip.clampAdvance {α : Type} (arr : ByteArray) (q : Nat) : ParseResult α → ParseResult α

Clamp a raw result so a success that did not advance past q becomes a failure at q. This is what makes the conditional (always-consume) witness hold for fix without unfolding the fuel recursion.

Equations

• Grip.clampAdvance arr q (Grip.ParseResult.ok a newOffset) = if q < newOffset ∧ newOffset ≤ arr.size then Grip.ParseResult.ok a newOffset else Grip.ParseResult.error { pos := q, expected := [] }
• Grip.clampAdvance arr q (Grip.ParseResult.error a) = Grip.ParseResult.error a

@[specialize #[]]

def Grip.GParser.fixFuel {α : Type} (f : GParser conditional α → GParser conditional α) : Nat → ByteArray → Nat → ParseResult α

The executable projection of fixFuelBounded. The bound proof is erased, so this remains the same Nat → ByteArray → Nat → ParseResult runtime interface.

Equations

• Grip.GParser.fixFuel f n arr q = (Grip.GParser.fixFuelBounded✝ f n arr q).val

@[specialize #[]]

def Grip.GParser.fix {α : Type} (f : GParser conditional α → GParser conditional α) : GParser conditional α

Build a recursive conditional parser as the fixpoint of f. See the module note above for the totality-not-productivity caveat.

Equations

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

def Grip.GParser.fixSelf {α : Type} (f : GParser conditional α → GParser conditional α) (n : Nat) : GParser conditional α

The clamped self-reference fix threads into the body at fuel level n: its recursive run is fixFuel f n behind the advance clamp. Exposed (with unfolding lemmas below) so the metatheory can reason about fixFuel without unfolding the anonymous inner structure; see grip-props/GripProps/FixComplete.lean.

Equations

• Grip.GParser.fixSelf f n = { run := fun (a : ByteArray) (p : Nat) => Grip.clampAdvance a p (Grip.GParser.fixFuel f n a p), cwit := ⋯, ewit := ⋯, swit := ⋯, bwit := ⋯, fwit := ⋯ }

@[simp]

theorem Grip.GParser.fixSelf_run {α : Type} (f : GParser conditional α → GParser conditional α) (n : Nat) (a : ByteArray) (p : Nat) : (fixSelf f n).run a p = clampAdvance a p (fixFuel f n a p)

fixSelf's run is the clamp of the lower-fuel fixFuel.

theorem Grip.GParser.fixFuel_succ {α : Type} (f : GParser conditional α → GParser conditional α) (n : Nat) (arr : ByteArray) (q : Nat) : fixFuel f (n + 1) arr q = (f (fixSelf f n)).run arr q

The one-step unfolding of fixFuel: at fuel n+1, run the body applied to the clamped fixSelf at fuel n.

@[simp]

theorem Grip.GParser.fixFuel_zero {α : Type} (f : GParser conditional α → GParser conditional α) (arr : ByteArray) (q : Nat) : fixFuel f 0 arr q = ParseResult.error { pos := q, expected := [] }

Fuel zero fails at the current offset.