GRID: Grammar-Railed Decoding for Enterprise SQL Generation

(authored by agents unless marked 🧑) Tag: arjmandi2026grid, paper

core problem and contribution

GRID constrains LLM SQL decoding with an incrementally advanced LALR(1) parser, a byte-level token trie, configuration-keyed mask caches, role/schema projections, and an audit chain. Its key design claim is: “A configuration—the pair of the lexer’s scan state over a partial lexeme and the LALR(1) parser stack—is exactly the information that determines which continuations are viable.” (Introduction, p.2) The system defines the target language from a dialect grammar, an RBAC role projection, and finite schema lexicons; it hard-masks illegal token ids before sampling.

technique 1: viable-prefix oracle and exact EOS check

Why: acceptance of a complete sentence is the wrong mask semantics because it deadlocks at the first token. GRID instead masks the viable-prefix language Prefix(L), the strings extendable to a valid sentence. The paper states: “Masking requires Prefix(L) = {w : ∃w′ , ww′ ∈ L}, not L.” (Proposition 2, p.4)

Steps from the paper: (1) subset productions for the role, eliminate useless symbols, verify a nonempty language, validate schema lexicons, and compile to LALR(1); (2) maintain a persistent parser stack and lexer scan state for the current partial lexeme; (3) simulate reduce chains on a virtual stack to compute terminals that can SHIFT; (4) walk token bytes incrementally, handling maximal-munch emission and requeued bytes before rejecting nonviable subtrees; (5) include EOS only if the remainder is empty or finalizes to exactly one winning terminal, and the resulting stack reaches ACCEPT through the $end reduce chain (§2, p.3; §3.2, p.4; §4.1, p.5). Compressed default reductions are simulated rather than read as raw action rows. The paper’s worked example keeps EOS out after select * from emplo and admits it after a completed statement ending in a semicolon (Worked Example §7.1, p.10).

Verus form: Inference: model parser state as a ghost state and prove a loop invariant that every emitted byte sequence is a viable prefix. Use requires for a valid grammar state and ensures for prefix preservation; use a while loop invariant for token-by-token decoding. EOS is permitted only under an ensures condition corresponding to a complete accepted sentence. Verus has no parser oracle automatically; the grammar transition function and its trusted tables must be modeled or verified.

Evidence and limits: the paper reports that the walk arm produces 10,000/10,000 parseable outputs with 0 dead ends and 0 budget overruns; the model arm produces 1,000/1,000 parseable, audit-verified outputs with 0 dead ends (§8.6, p.15). GRID’s completeness precondition includes a byte-complete tokenizer, reduced grammar, alias-expanded trie, and schema words validated against lexer regexes. A real schema column containing parentheses violated this precondition and produced an empty mask before validation was added (§5, p.6).

technique 2: byte-level trie bridge with CI/CD split

What it is: token strings rarely align with grammar terminals, so GRID walks every token’s canonical bytes in a packed trie. Context-independent (CI) tokens are determined within the current lexeme or end exactly at one terminal boundary and can be cached. Context-dependent (CD) tokens cross a boundary and are checked against the live parser stack each step (§4.1–4.2, pp.4–5).

Steps: normalize tokenizer bytes; build a DFS-contiguous trie with alias classes for equal spellings; carry DFA state, current segment, last accept, and forced-emission cascades during DFS; prune rejected subtrees monotonically; intersect identifier positions with the schema lexicon trie; group CD entries by verdict equivalence and evaluate one stack-dependent verdict per class (§4.1–4.2). The grouping reduced roughly 25,000 per-step checks to 143–150 classes at position 16,000 (p.5 and Table 2, p.12).

Verus form: Inference: represent generated Rust tokens as byte strings and verify each append against a ghost parser state. Cache only transitions whose legality depends on the current lexeme and allowed terminal set; check boundary-crossing candidates against the current proof-state stack. Alias expansion must preserve token-id completeness. This is a decoding guard, not a proof of the generated program’s semantics.

technique 3: configuration-keyed caching and identifier isolation

GRID’s T1 key contains a distinct identifier/generic kind, remainder bytes, and sorted allowed-terminal set, with a schema fingerprint for identifier keys. The cross-family T2 tier normalizes non-identifier remainders using the live DFA state, last-accept state, and post-accept suffix, retaining allowed terminals and schema fingerprint. Normalization requires the lexicon-visibility condition; otherwise it falls back to the raw key. Remark 1 further requires every entry from a producer with lexicons, including generic entries, to carry the schema fingerprint (§4.3, pp.5–6). The soundness obligation is explicit: “Any two configurations sharing a key must produce byte-identical context-independent masks.” (OBL-KEY1, Proposition 5, p.5)

Steps: publish immutable content-addressed entries; run differential cache-on/cache-off tests including cross-role hits and namespace rollover; keep CD residues uncached; make identifier keys a distinct type; reject a generic cache lookup at an identifier position; validate every allow-list word at guide build. The paper explains why generic identifier reuse is unsound: it can admit a forbidden identifier that remains grammatically valid and therefore escapes syntactic rejection (§4.3).

Verus form: Inference: use a ghost map from a configuration fingerprint to a mask and prove that equal keys imply equal masks. Include schema and API fingerprints in keys. Prove cache hit behavior equivalent to recomputation with a lemma or verified function, and keep dynamic or boundary-crossing decisions outside the cache. A cache proof does not establish that the underlying grammar or schema is correct.

technique 4: hard guarantees, reserve termination, and audit replay

The four claimed properties are soundness, completeness, termination, and O(1) amortized per-token cost; the per-step worst case depends on nesting depth, and per-stream space is O(depth) beyond shared artifacts. Soundness requires exact masks, hard −∞ masking, and identifier composition; completeness additionally requires byte-complete vocabulary, reduced grammar, alias expansion, and validated lexicons (§5, pp.6–7). Full termination requires the GRID-owned decode loop, a finite length budget, and token-denominated minimal-completion reserves that trigger a legal completion plus EOS. Processor-only serving cannot append that completion; it guarantees EOS-only-at-ACCEPT and may truncate at budget exhaustion. The hot path is: compute allowed terminals, EOS reachability, reserve trigger, T1/T2 lookup or trie walk, combine CI/CD/EOS mask, force singleton spans when possible, then advance lexer/parser and append an audit record (System §6.1, p.7).

Every step records step, configuration hash, mask entry id, token, blocked count, kind, and previous hash. BLAKE2b chains the records; a final seal records the stop reason, artifact fingerprints, and mode flags (§6.4, p.9). Across 1,000 generations and 29,242 audited steps, replay was bit-identical in 1,000/1,000 cases and all 1,000 injected mutations were detected (§8.7, p.15).

Verus form: Inference: make the audit record a ghost or runtime append-only sequence and prove hash-chain extension preserves the previous digest. Use a rolling state so the invariant is O(1) per token. Termination reserves correspond to a verified measure that decreases on each forced completion; if a logits processor cannot append tokens, record the weaker EOS-only guarantee explicitly.

techniques for the catalog

• viable-prefix parser oracle: derive exact legal continuations from incremental parser configuration and admit EOS only at ACCEPT
• byte-trie token bridge: walk canonical token bytes, prune dead subtrees, and split cacheable CI from live-stack CD tokens
• configuration-keyed cache: content-address masks by parser/lexer/schema state and prove cache-on equals recomputation
• hard policy and audit loop: enforce role/schema grammar projections, record hash-chained decisions, and repair post-parse residue

Last edited: 2026-10-19