Grip.Char: a UTF-8 / Char layer above the byte core

Consumers that think in Char rather than UInt8 use these combinators. Each decodes one UTF-8 scalar from the ByteArray and advances by its byte width, so the fast path stays byte-level: there is no String allocation and no intermediate decode of the whole input.

satisfyChar/anyChar/char are conditional (they consume at least one byte on success). The if q < q' clamp in each run makes the always-consume witness hold without reasoning about the decoder's width, mirroring GParser.fix. The decoder decodeUtf8 and the byte-level literal matcher matchBytes are exposed for grammars that mix levels; GParser.string matches a whole UTF-8 literal.

@[inline]

def Grip.decodeUtf8 (arr : ByteArray) (q : Nat) : Option (Char × Nat)

Decode one UTF-8 scalar starting at byte offset q, returning the Char and the new offset q + width (width 1 to 4), or none on truncated or invalid input.

Equations

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

theorem Grip.decodeUtf8_le {arr : ByteArray} {q : Nat} {c : Char} {q' : Nat} (h : decodeUtf8 arr q = some (c, q')) : q' ≤ arr.size

A successful decodeUtf8 ends within bounds: each branch that returns some (c, q + k) first checks the byte at q + (k-1), so q + k ≤ arr.size.

@[inline]

def Grip.GParser.satisfyChar (p : Char → Bool) : GParser conditional Char

Consume one Char satisfying p, or fail without consuming. Grade conditional.

Equations

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

@[inline]

def Grip.GParser.anyChar : GParser conditional Char

Consume any one Char. Grade conditional.

Equations

• Grip.GParser.anyChar = Grip.GParser.satisfyChar fun (x : Char) => true

@[inline]

def Grip.GParser.char (c : Char) : GParser conditional Char

Consume the specific Char c. Grade conditional.

Equations

• Grip.GParser.char c = Grip.GParser.satisfyChar fun (x : Char) => x == c

@[irreducible]

def Grip.matchBytes (arr bs : ByteArray) (i q : Nat) : Bool

Do the bytes of bs from index i match arr from offset q?

Equations

• Grip.matchBytes arr bs i q = if i < bs.size then if q < arr.size then arr[q]! == bs[i]! && Grip.matchBytes arr bs (i + 1) (q + 1) else false else true

theorem Grip.matchBytes_le (arr bs : ByteArray) (i q : Nat) (hi : i < bs.size) (h : matchBytes arr bs i q = true) : q + (bs.size - i) ≤ arr.size

A successful matchBytes starting at a real index (i < bs.size) ends within bounds: each matched byte requires q < arr.size, so q + (bs.size - i) ≤ arr.size.

@[inline]

def Grip.GParser.string (s : String) : GParser conditional Unit

Match the UTF-8 bytes of the literal s, consuming them. Intended for a nonempty literal (grade conditional); the if q < q' clamp fails an empty match.

Equations

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

Sanity guards.