1 Introduction↩︎

We are concerned with generating SQL (and, more generally, sentences of any LALR(1)-parsable language) from a large language model under the operating conditions of an enterprise CRUD/RBAC deployment. In that setting, “the model usually writes valid SQL” is not an acceptable contract. Six problems, each of which shapes the design, must be solved simultaneously:

1. Validity and policy, jointly. Output must parse under the SQL dialect and comply with per-role policy (allowed verbs, banned clauses) and per-schema vocabulary (only real tables and columns). Policy is not a post-hoc filter: a role that may only select must be unable to emit delete at all, and identifiers must be schema-valid by construction.

2. Provable guarantees. Soundness (never emit a token that leaves the language’s prefix set), completeness (never block a token that could still lead to a valid sentence), and termination (every stop is a complete sentence) must be theorems with explicit preconditions, each paired with the test that verifies it—not emergent properties of a test suite.

3. Flat per-token cost (requirement R). Guard-rail cost per token must be amortized \(O(1)\) in the current output length \(n\) (worst case bounded by grammar/nesting constants, never by \(n\)), so total guard cost is \(O(n)\) over a generation. A guard whose per-token cost grows with context is unusable for long generations; §8.2 shows a 2023-era system for which per-token overhead grows by \(\sim\)​1.19 ms per position.

4. A replayable audit trail. In a compliance setting, “what was the model allowed to say at step \(t\), and why?” must be answerable after the fact: a hash-chained, per-token record of permit/block decisions, replayable bit-identically against versioned grammar artifacts.

5. Serving reality. Production decoding is batched, grammars are heterogeneous across co-batched requests, and new schemas arrive while a hot batch is running. The guard must overlap mask computation with the GPU forward pass, never stall co-batched requests on one request’s cold miss (the cold-schema-into-hot-batch problem), and never substitute an approximate mask under deadline pressure.

6. An honest boundary for the unenforceable residue. Some policy is provably not enforceable by any left-to-right context-free mask—column-level RBAC being the canonical case (Proposition 11). The system must name that boundary rather than blur it, enforce it post-parse, and—where a capable model is available—convert the named violations into a checker-guided repair loop.

GRID answers these with one architectural idea and its consequences: key everything on parser configurations. 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. Masks are computed from configurations, cached under configuration-derived keys whose soundness is a stated obligation (a Myhill–Nerode-style refinement, §4.3), and audited under a rolling configuration hash. The mask cost therefore tracks the grammar configuration, not the output position, which is requirement R by construction; the benchmarks in §8 measure that this holds on real vocabularies at \(n = 16{,}384\).

1.0.0.1 Contributions.

(1) A formal framework for configuration-keyed constrained decoding: the incremental LALR(1) parser as a viable-prefix oracle with exact EOS gating under table compression (§3); a byte-level token\(\leftrightarrow\)terminal bridge with a context-independent/context-dependent split that makes cache-key soundness hold by construction (§4); the cache-key soundness obligation OBL-KEY1 and the identifier composition rule, with the scanner normal form that maximizes sound cross-request sharing (§4.3). (2) Four guarantees stated as propositions with explicit preconditions, including the honest negative result that column-level RBAC is mask-unenforceable (§5). (3) A system realizing the framework—grammar pipeline, Rust kernels (v4\(\to\)v7, warm serving step \(7.39\to1.33\) μs/request, then a v7 fused cold-miss path), two-tier write-back mask cache, a serving contract for batched heterogeneous decoding, and a hash-chained audit log (§6)—with worked examples (§7). (4) A committed benchmark record: per-token mask latency against XGrammar, llguidance, and Outlines on two tokenizers; requirement-R slope measurements; MaskBench; Spider execution accuracy with checker-guided repair; and an end-to-end vLLM serving record including a cold-miss stress arm (§8).

1.0.0.2 Design lineage.

The initial patent filing captured an early, partial snapshot of this design (v0.0.5, designed August 2023): a precomputed validity table over token sequences against a pushdown automaton, with decode-time logit masking. Planned iteration carried the design forward: v0.0.6 (September 2023) already outperformed the July-2023 release of guidance on the scaling benchmarks of that era, and v0.0.7 (November 2023)—the system described in this paper, and the line the final patent application followed—replaced sequence keys with configuration keys and acceptance semantics with prefix viability, added the byte-level token\(\leftrightarrow\)terminal bridge, the write-back cache, RBAC/schema projections, the audit chain, and checker-guided repair; the work has continued to improve since. Sections 3–4 present the design analysis behind the two load-bearing revisions. The design drew inspiration from published work—notably Willard and Louf’s Outlines paper [1], whose finite-state-machine formalization of guided generation this paper deliberately parallels in register—while GRID’s design and implementation are our own throughout.

2 Preliminaries↩︎

2.0.0.1 Masked decoding.

Let \(V\) be a tokenizer vocabulary with \(|V| = N\) and let \(\Sigma\) be the byte alphabet. An autoregressive LM defines logits \(\boldsymbol{\alpha} = \mathrm{LM}(s_{1..t},\boldsymbol{\theta}) \in \mathbb{R}^N\); guided generation applies a mask \(m \in \{0,1\}^N\) before sampling, \(\tilde{\boldsymbol{\alpha}} = m \odot \boldsymbol{\alpha}\) (implemented as an in-place masked_fill_(\(-\infty\))), and samples \(s_{t+1} \sim \mathrm{Categorical}(\tilde{\boldsymbol{\alpha}})\). Constructing \(m\) at each step is the entire problem: done naively it costs a parse of the whole prefix per candidate token per step.

2.0.0.2 Tokens are byte strings.

Each token has a canonical spelling \(\mathrm{bytes}\colon V \to \Sigma^\ast\) (token_bytes): byte-level-BPE unicode remaps inverted, SentencePiece/BPE space markers normalized to 0x20, byte-fallback literals <0xNN> mapped to their byte. One definition serves the trie build, the fast path, and the reference oracle. Distinct token ids may share a spelling (alias classes); masks are over ids, not spellings.

2.0.0.3 Three grammar layers, one language.

• L1 (dialect core). A CFG \(G = (\mathcal{N}, T, P, S)\) whose terminals \(\tau \in T\) carry regular lexeme languages \(R_\tau \subseteq \Sigma^\ast\), with an ignored subset \(I \subseteq T\) (whitespace, comments) that is first-class. Production SQL grammars (PostgreSQL, MySQL, SQLite) are LALR(1), so deterministic-PDA coverage suffices. Lexing is maximal munch over the union automaton with contextual resolution: a forced emission event carries the full candidate terminal set at the longest match and the consumer picks the highest-priority parser-viable candidate (this is what lets TABLE_NAME and COLUMN_NAME share one regex, and what resolves JSON’s property-key-vs-string overlap with no new mechanism).

• L2 (role projection). A production subset \(P_{\mathrm{role}} \subseteq P\) (verb subsets, clause bans) followed by mandatory useless-symbol elimination and a verified \(L(G_{\mathrm{role}}) \neq \emptyset\). Reducedness is load-bearing: without it, “non-empty action set \(\Rightarrow\) viable prefix” fails and dead ends return.

• L3 (schema lexicon). For identifier categories \(C \subseteq T\), finite allow-lists \(W_c \subseteq \Sigma^\ast\) realized as lexer tries; the lists are generated from the database catalog (information_schema). Precondition, validated at guide build rather than assumed: \(W_c \subseteq R_{c}\) for every category (each allowed word must be scannable to an accepting state of its terminal).

The constrained language \(L = L(G_{\mathrm{role}},\mathrm{schema})\) is the set of byte strings that lex and parse under the projected grammar with every category-\(c\) lexeme in \(W_c\). Both the policy bundle and the schema snapshot are fingerprinted, immutable inputs; grammars, tries, and reserve tables are content-addressed artifacts.

3 The viable-prefix oracle↩︎

3.1 Design analysis: why sequence keys and acceptance semantics fail↩︎

The v0.0.5 design snapshot precomputed an in-memory table tagging LLM token sequences as accepted or rejected by a pushdown automaton, and masked per step from table lookups. Two observations, made during the planned design review of that snapshot, force the shape of everything that follows.

A “representative subset” of that table is defined by outcome, not by a construction, so it offers no build recipe. The information the table was trying to enumerate is, however, finitely presentable: by the viable-prefix property of LR automata [2], the set of viable prefixes of an LR grammar is characterized by the parser’s configurations, a grammar-sized key space (\(10^4\)–\(10^6\) for SQL-class grammars).

Both conclusions are constructive, not merely destructive: they identify the correct key space (configurations) and the correct semantics (prefix viability), which the rest of this section formalizes.

3.2 Configurations and the correct-prefix property↩︎

Two refinements make this exact in practice rather than merely in principle.

3.2.0.1 Allowed terminals under table compression.

LALR tables with default reductions over-approximate raw action rows (spurious reduces). The allowed-terminal set is therefore computed by simulation: \(A(\sigma) = \{\tau : \mathrm{simulate}(\sigma,\tau) \text{ reaches a SHIFT}\}\), where simulate runs the reduce chain on a virtual overlay stack (pop \(|\mathrm{rhs}|\), GOTO, repeat) until shift or error. Cost is \(O(|\mathrm{row}| \times \mathrm{depth})\) worst case, amortized far less, and memoized per stack node.

3.2.0.2 EOS gating by reduce-chain simulation, mid-lexeme aware.

EOS may enter the mask only when the current output is a complete sentence. A raw row read is wrong twice: compressed tables have spurious reduces, and after ...FROM t the pending lexeme t is a complete identifier still awaiting maximal-munch finalization—the stack alone would wrongly report EOS illegal. The rule: EOS is legal iff (the remainder is empty or the pending lexeme finalizes as exactly one winning hypothesis) and, after virtually shifting that finalized terminal on a scratch stack, ACCEPT is reachable via the reduce chain of $end.

4 The token–terminal bridge↩︎

LLM tokens do not align with grammar lexemes: sel+ect spells SELECT, and schema identifiers are never single tokens. Masking out “fragment” tokens destroys completeness; admitting them requires scoring every token’s bytes against the live configuration. The early design snapshot illustrated this misalignment and left the mechanism as later work; this section is that mechanism.

4.1 The trie walk and the exact mask↩︎

\(M(\kappa)\) is computed by a DFS over the trie that carries an \(O(1)\)-updatable scan state per frame (DFA state, current segment, last-accept, pending forced-emission cascade): a byte that kills the DFA triggers maximal-munch emission of the last accept and requeues the unconsumed tail. Rejection is monotone under extension, so rejected subtrees are skipped wholesale via the packed subtree size. At identifier positions the DFA runs against the L3 trie intersection. Masks are complete over ids via alias expansion.

4.2 The context-independent/context-dependent split↩︎

The walk therefore classifies every admitted token as CI (context-independent: resolvable within the current lexeme, or ending exactly at one terminal boundary with that terminal in \(A\))—cacheable—or CD (context-dependent: boundary-crossing continuation)—returned as a residue list and checked against the live stack every step, never cached. Without this split, the cache-key soundness obligation of §4.3 is violated by construction, not merely unverified. The CD residue is the main hot-path cost and gets its own machinery:

4.2.0.1 Verdict-equivalence grouping.

The per-step verdict of a CD entry depends on the entry only through its per-event candidate terminal sets, its segments and trailing remainder only via the lexicon predicates, and the live set of its remainder’s scan state. Entries are therefore partitioned once, at publish time, into verdict-equivalence classes; each step evaluates one stack-dependent verdict per class and extends the mask with the class’s alias-expanded ids. On the SQL bench this turned \(\sim\)​25k per-step entry checks into \(\sim\)​150 class verdicts (measured mean 143–150 classes/step at \(n{=}16{,}000\); §8.2), and a later kernel round that keyed classes by verdict equivalence instead of raw bytes collapsed \(\sim\)​55k singleton groups to \(\sim\)​1.4k classes, a \(9.3\times\) cold-build reduction (§6.2).

4.3 Configuration-keyed caching: OBL-KEY1 and the identifier rule↩︎

The write-back mask cache carries the v0.0.5 table’s spirit—precomputed where cached, computed on miss—to its workable form: entries are keyed on configurations, published idempotently (content-hashed \(\mathrm{entry\_id} = \mathrm{BLAKE2b\text{-}128}(\text{key} \,\|\, \text{encoding tag} \,\|\, \text{payload})\), so racing writers produce the same id), immutable, and versioned under namespaces that roll over when grammars are superseded.

OBL-KEY1 is verified, not assumed: differential tests check cache-on \(\equiv\) cache-off over randomized replays including cross-role hits, and publish is content-addressed so a racing writer of the same key with a different mask trips a runtime assertion.

The rule is enforced structurally: identifier-position keys are a distinct key type that cannot collide with generic keys, and consulting a generic entry at an identifier position raises an error in all builds (a test injects the condition and asserts it fires).

4.3.0.1 The cross-family tier (T2) and the scanner normal form.

A second tier shares entries across the grammar family—the enterprise shape is many roles \(\times\) schemas over one dialect. Role projections share the L1 terminal numbering (assigned at freeze; projections subset productions, never renumber), so two roles reaching the same normalized configuration share entries. To maximize sharing soundly, non-identifier keys normalize the remainder to the genN scanner normal form: scanning \(r\) with last-accept tracking yields \((q, \ell, p)\)—the live DFA state \(q\), the last-accept length \(\ell\), and the last-accept state \(p\)—and the key becomes \[\big(\text{genN},\; p,\; q,\; v,\; \mathrm{sorted}(A),\; \mathrm{schema\_fp}\big), \qquad v = r[\ell{:}] \;\text{(the post-accept suffix bytes)},\] sound only under the lexicon-visibility guard \((\mathrm{live}[q] \cup \mathrm{accepts}[p]) \cap \mathrm{LEX} = \emptyset\): every terminal whose lexicon predicates the walk could consult on remainder-derived bytes lies in that set, so under the guard those checks are lexicon-inert and the walk’s future is a function of \((p,q,v,A)\) and the lexicons alone—remainders the walk provably cannot distinguish share one entry. The suffix \(v\) is load-bearing (e.g.b"1e" and b"1E" share \((q,\ell,p)\) but requeue different bytes on emission). Guard failure falls back to the raw key.

5 Guarantees↩︎

Each guarantee is stated with its exact preconditions; each clause is paired with the test or benchmark that verifies it (§8). \(L\) is the role/schema-projected language of §2.

Precondition (d) earned its “validated, not assumed” status empirically: the first real-world schema violation (a Spider database column named Official_ratings_(millions), whose parentheses lie outside the column-name regex) produced an empty mask at a viable state within 100 generations—every prefix of the word passes the lexicon-prefix check, yet no token can ever complete the lexeme. The precondition is now checked at guide build.

Proposition 11 is not an apology but a load-bearing design input: it defines the residue that the SemanticChecker names precisely, which in turn is what makes checker-guided repair work at scale (§8.4).

6 System↩︎

6.1 Architecture↩︎

Figure 1 shows the three time scales. Everything expensive is offline and content-addressed; everything per-request is a registry lookup with single-flight construction; the per-token hot path touches only configuration-sized state.

6.1.0.1 The per-token hot path

(normative order; every step audited):

1. \(A \leftarrow\) allowed terminals by reduce-chain simulation on the virtual stack (memoized per node).

2. \(\mathrm{eos\_ok} \leftarrow\) mid-lexeme-aware ACCEPT-reachability (§3).

3. Reserve trigger (session budget, not grammar state): if \(\mathrm{budget} \le |\mathrm{completion}| + \mathrm{safety}\), return \(\mathrm{Write}(\text{shortest completion} + \mathrm{EOS})\).

4. Key \(\leftarrow\) Definition 5 / the genN normal form; T1 then T2 lookup; miss \(\Rightarrow\) trie walk (CI mask \(+\) CD residue), publish idempotently.

5. Mask \(\leftarrow\) CI \(\cup\) CD-pass (live-stack class verdicts) \(\cup\) \(\{\mathrm{EOS}\;\text{iff eos\_ok}\}\); empty mask raises—a bug by Proposition 8, asserted throughout the test suite.

6. Singleton masks extend to a maximal forced span (jump-forward Write, bounded chain length); otherwise return the full exact mask, applied as a hard in-place fill.

7. On the sampled token: bytes \(\to\) lexer advance (maximal munch, candidate sets, parser-viable pick) \(\to\) shift/reduce on the persistent stack \(\to\) append the audit record.

Two implementations of this semantics coexist: a \(\sim\)​140-line pure-Python executable specification (brute-force trial-parse over the vocabulary) and the fast path, bound bit-identically by differential and parity tests. This discipline caught—before any debugging session—alias ids silently dropped from masks, lexicon-blind reserve completions, and a real Rust/Python divergence in a CD group key.

6.2 The kernel line: v4 \(\to\) v5 \(\to\) v5.1 \(\to\) v6 \(\to\) v7↩︎

Four hot symbols (trie walk, CD verdicts, LALR advance, bitmask fill) are bound to Rust kernels; the Python spec path remains and a flag forces it. The performance history is a lesson in where the cost actually was:

• v4 — a persistent, structurally interned stack arena with cross-token memos and a one-call assembled hit pass: warm-hit p50 \(12.9 \to 3.5\) μs (dev host). The interning insight: once a hot path is in Rust, the next win is usually not calling it—parser configurations recur massively across positions. v4 also releases the GIL on the cold walk; measured main-thread liveness during a cold replay rose from \(9\%\) (walk holding the GIL: “overlap” was a lie) to \(88\%\).

• v5 — scheduler-side fill_bits: the whole per-request bitmask row (pre-packed CI bit words \(+\) live CD bits \(+\) EOS) written into vLLM’s buffer in one FFI call. Motivated by the first real batched run: batch-1 overhead \(+1.26\%\) but batch-8 \(+3984\%\) and batch-32 \(+5151\%\)—three stacked serving-only defects (a fill path that skipped the warm kernel; a prefetcher that scheduled every successor onto one worker; per-request copies re-registering every entry). Fixes in dependency order took the batch-32 step from 708 ms to 16 ms.

• v5.1 — verdict-equivalence CD grouping (Remark in §4.2): cold CD-heavy mask builds \(124 \to 13.3\) ms (\(9.3\times\)); warm fill p90 \(38 \to 3.8\) μs. Both prior theories of this cost (“151k-vocab walks are superlinear,” “the warm gap is Python dispatch”) failed under component-level measurement; the real causes were CD keys embedding raw bytes and re-packing \(\sim\)​47k CD ids per fill.

• v6 — the whole per-request serving step in-kernel (session_accept/session_fill, one FFI call each): warm serving step \(7.39 \to 1.33\) μs/request (accept \(6.16 \to 0.56\), fill \(1.22 \to 0.77\); local M-series measurement), restricted to audit-off serving paths; audit-enabled and processor-mode guides keep v5. A 200-seed lockstep fuzz of v6 against v5 showed zero divergence and the pre-implementation review surfaced a real v5 bug (post-COMPLETE state resurrection under speculative decoding), now pinned by the differential suite.

• v7 — the entire cold mask miss moved into Rust (RustWalker.walk_payload \(+\) RustVerdicts.register_blob): walk, group-blob, CI pack, adaptive encode, BLAKE2b entry_id, and registration in one GIL-released call; Python receives a handle plus a thin MaskEntryV7 shell. The red-team’s original premise—that the per-cold-entry Python cost was make_entry/encode/hash—was wrong on inspection (those are microseconds); the real source of the measured 6.8–8.7 ms per boundary entry was the WalkResult glue building CDEntry reps plus \(\sim\)​30–60k gc-tracked objects per miss, whose allocation triggered gen-2 GC pauses inside the walk. Keeping the miss in Rust removes both: the per-boundary-entry cost falls \(6.8\)–\(8.7 \to 0.003\) ms. entry_id is byte-identical (so the audit trail replays unchanged); GRID_V7 defaults on and =0 is byte-identical to v6. The win is localized to the serving cold-entry path—the warm hit path, the R-microharness, and the engine-comparison latencies are v7-unchanged.

6.3 The serving contract↩︎

Under vLLM, GRID implements the structured-output backend contract (scheduler-side bitmask fill, rollback natural on persistent states) and a logits-processor mode. The contract that keeps a batch healthy:

• Overlap, cold-only. Mask computation runs on CPU overlapped with the GPU forward pass. The prefetcher schedules a successor’s mask onto the worker pool only when it is not already warm: the warm steady state never touches the pool (unconditionally scheduling every successor serialized the steady state behind one worker’s queue—one of the three batched-run defects).

• Skip-a-round defer. If a request’s mask is not ready at sampling time (worst case: a cold identifier-position walk), that request is deferred from the current scheduling round and rejoins the next step; co-batched requests are never stalled, and an approximate mask is never substituted—by design there is no over-approximating deadline fallback, because one over-admitted token exits \(\mathrm{Prefix}(L)\) and voids Proposition 7. In vLLM this is realized as a scheduler mask-readiness guard (one small patch site; upstream PR drafted).

• Single-flight everything. One build per artifact fingerprint; \(N\) concurrent waiters share the result or the same exception; failures are negatively cached with a TTL.

• An honest negative result: warmup-at-admission fails on the GIL. The tempting alternative to the defer—warm the fresh request’s masks while it sits in the WAITING queue—was implemented and measured harmful: the tier work is GIL-bound, so admission warmup starved the live engine (fresh-request TTFT \(10\times\) worse and multi-second batch stalls). It defaults off. The defer, plus genN key normalization and rayon-parallel cold walks (bit-identical; \(2.05\times\) at 8 threads locally), is the shipped cold-schema stack.

6.4 The audit chain↩︎

Every step appends a record \((\mathrm{step}, \mathrm{config\_hash}, \mathrm{mask\_entry\_id}, \mathrm{token}, \mathrm{blocked\_count}, \mathrm{kind}, \mathrm{prev\_hash})\)—including each interior token of a forced span and the EOS tail record—chained by BLAKE2b from a genesis constant and sealed with the stop reason, artifact fingerprints, and mode flags (e.g.processor-only downgrades). The configuration hash is rolling and \(O(1)\) per push, \[H(\mathrm{node}) = \mathrm{low}_{64}\,\mathrm{BLAKE2b\text{-}128}\big(H(\mathrm{parent}) \,\|\, \mathrm{u32}(\mathrm{state}) \,\|\, \mathrm{u32}(\mathrm{goto})\big), \qquad H(\mathrm{root}) = 0,\] since hashing the stack from scratch would be a hidden \(\Theta(\mathrm{depth})\)-per-token dependence. Because mask entries are immutable and content-addressed and the hash pins the parser trajectory, a log replays against archived artifacts to bit-identical masks; §8.7 reports the full-scale replay measurement.

7 Worked examples↩︎

7.1 Masking mid-identifier under a schema lexicon↩︎

Take the CRUD-subset grammar (lowercase keywords; TABLE_NAME and COLUMN_NAME share the regex [a-z_][a-z0-9_]* and are L3 categories), the role analyst whose L2 projection keeps only select_stmt among the query productions, and the schema lexicon \[W_{\mathrm{TABLE}} = \{\texttt{employees},\;\texttt{employees\_public},\; \texttt{orders}\},\] with a table salaries existing in the database but absent from the role’s lexicon. The model has emitted

so the configuration \(\kappa\) has: stack \(\sigma\) with select, *, from shifted (allowed next terminal set \(A = \{\mathrm{TABLE\_NAME}\}\)), and remainder \(r = \texttt{emplo}\) scanning inside an identifier lexeme with the L3 category context set. Because \(A\) contains an identifier category, the cache key is the ident type and carries the schema fingerprint (Proposition 6); the walk intersects the token trie with the lexicon trie from the state reached by emplo (Figure 2). Representative verdicts:

• token yees (bytes yees): completes exactly employees, a lexeme boundary with \(\mathrm{TABLE\_NAME} \in A\) \(\Rightarrow\) CI, admitted (and cached in the entry’s CI payload).

• token y: extends to employ, a live lexicon prefix \(\Rightarrow\) CI, admitted (mid-lexeme continuation).

• token yees where: crosses the boundary (emits TABLE_NAME = employees, skips ignored whitespace, begins where) and continues \(\Rightarrow\) CD: its verdict depends on whether where can shift after table_ref, i.e.on the live stack—checked this step, never cached (Proposition 4). Here it passes.

• token yer: employer is not a prefix of any allowed word \(\Rightarrow\) blocked, monotonically with its whole trie subtree.

• At the earlier position select * from (empty remainder): token sal matches the generic identifier regex but is a prefix only of the absent salaries \(\Rightarrow\) blocked. A generic-IDENT cache entry would have admitted it and the parser would never have objected—the silent RBAC violation the identifier composition rule exists to prevent.

• At the statement head, tokens spelling insert, update, delete are blocked for this role because L2 removed those productions and reduction pruned their terminals: the verbs are not merely improbable, they are outside the language. No prompt can path to them (the model-independent RBAC test probes every reachable identifier position with an exhaustive multi-token speller; §8.6).

• EOS is not in the mask: simulating $end after virtually finalizing emplo as TABLE_NAME does not reach ACCEPT (the grammar requires the closing ;), even though emplo’s finalization itself is legal. After a later ... ; the reduce chain reaches ACCEPT and EOS enters the mask through the explicit gate only.

7.2 A cold schema entering a hot batch↩︎

Thirty-two requests are decoding at steady state (warm caches, kernel fills of a few microseconds) when a request arrives for a schema the deployment has never seen. The fresh request pays, in order: a single-flight grammar+lexicon specialization (27.3 ms cold, measured; every concurrent duplicate waits on the same build), then—at its first identifier-heavy positions—cold trie walks that are milliseconds-scale by nature (vocabulary-sized DFS). The contract of §6.3 makes these costs private to the fresh request: the walk runs GIL-released on the pool, overlapped with the forward pass; if it is still unfinished at sampling time, the scheduler’s mask-readiness guard defers only that request for the round (Figure 3). Measured on the declared H100 SXM5 runner (§8.5): at kernel v7 the serving record holds the 31 warm co-tenants to a 15.3 ms worst engine step while the fresh request’s \(\sim\)​0.66 s cold window induces a transient \(+33.8\%\) co-batched TPOT slowdown—no longer a GIL-bound software cost (the v7 fused cold-miss path removed that) but host CPU/memory-bandwidth contention between the cold walk and the forward loop, which shrinks as walk threads grow. The defer remains the load-bearing protection: with it disabled the same leg reads \(+373\%\) and 65.7 ms. The fresh request itself sees TTFT \(0.7\) ms and then runs at \(1.00\times\) warm speed: a never-seen schema trades its own first-token latency for exact masks throughout—no approximation is ever substituted.

8 Evaluation↩︎

All numbers below are from committed benchmark reports in the repository (bench/RESULTS*.md) or the measured-results log; each table carries its host label verbatim. Declared runner = a named cloud instance type and image recorded in the report (Lambda 1\(\times\)H100 PCIe or SXM5 80GB, or 1\(\times\)A10 24GB; Ubuntu 24.04; virtualized); local dev = an unpinned Apple-Silicon workstation. Cross-engine ratios proved host-invariant; absolute constants carry the host label.

8.1 Per-token mask latency vs.XGrammar, llguidance, Outlines↩︎

The engine-comparison harness measures the wall time to produce the full next-token mask at each replay step, for all engines on the same SQL-subset grammar (expressed in each engine’s native format) and tokenizer, 11 replays. Table ¿tbl:tab:engines? reports both tokenizers on the declared H100 SXM5 runner at kernel v7 (re-recorded; within noise of v6, as expected—v7’s win is localized to the serving cold-entry path, not this per-token latency path).

4pt

Reading the table honestly: at kernel v7 GRID leads llguidance—the strongest prior engine in our measurements—at both p50 and p90 on both tokenizers (\(3.6\) vs.\(6.6\) μs p50 and \(80\) vs.\(224\) μs p90 on gpt2; \(6.7\) vs.\(14.9\) μs and \(109\) vs.\(384\) μs on Qwen), beats XGrammar at every reported percentile, and is the only engine with zero rejected replays. Its cache split is p50 \(3.5\) μs hit / \(4.8\) ms miss at \(92\%\) hit rate (gpt2; \(6.7\) μs / \(13.9\) ms / \(92\%\) on Qwen), so the p99 remains cold-miss trie walk on this recursive SQL grammar: llguidance’s Earley/derivative core keeps the flattest p99 (\(352\) μs vs.GRID’s \(5.3\) ms on gpt2), and we say so plainly. Outlines \(\ge\)​1.x has no CFG engine of its own: outlines.types.CFG routes to a backend, default llguidance, so its row is the same matcher plus Outlines’ logits-processor wrapper—identical rejects by construction. The steep negative table slopes are an artifact of cold misses clustering early in replays; the warm-replay check (slope \(+0.002\) μs/pos on gpt2, first-half p50 3 μs vs.second-half 4 μs; \(-0.004\) μs/pos and 5 μs vs. μs on Qwen) is the R-relevant statistic.

8.2 Requirement R: flat per-token cost↩︎

8.2.0.1 The R microharness

(declared H100 SXM5 runner, kernel v7; gpt2; \(n = 16{,}000\) tokens per stream, 20 seeded runs per nesting depth, warm-pass OLS; \(\varepsilon = 10^{-4}\) μs/pos) isolates guard cost from the model (Table 1). Slope confidence intervals sit well over an order of magnitude under \(\varepsilon\) at every depth; hit p50 is \(4.8\)–\(6.8\) μs; the steady-state hit rate is \(100\%\); cumulative-cost fits are linear with \(R^2 \ge 0.9998\).

4pt

8.2.0.2 Head-to-head scaling vs.guidance, three eras

(local dev Mac, unpinned; slopes and shape are the claim, absolutes indicative). The project’s founding claim—guard cost flat as generated context grows—was measured against guidance in three vintages on the same growing WHERE-chain statements, \(n \in \{512, \ldots, 16{,}384\}\). At \(n = 16{,}384\): GRID runs at \(3.2\) μs/step with slope \(-3.3\times10^{-5}\) μs/pos (kernels active); guidance 0.3.1 (today’s llguidance core) is also flat but at a \(\sim\)​30\(\times\) higher constant (\(97.7\) μs); guidance 0.1.5 (November 2023, Python Earley) holds a flat median (\(\sim\)​114 μs) while its worst-case single step grows \(67.5 \to 106.2\) ms across one generation’s quarters (gen-2 GC scanning the growing Earley chart, verified via gc.callbacks); and guidance 0.0.64 (July 2023, the release the v0.0.5 design was conceived against) breaks requirement R outright: measured overhead-vs-position slopes \(+1{,}105\) to \(+1{,}189\) μs/pos (mechanism confirmed in its code: full-string regex rebuilds per candidate per token, whole-prompt re-encoding per operation), i.e.quadratic total cost—it spent 898 s reaching position 873 and could not complete \(n = 2{,}048\); the linear fit extrapolates (labeled as such, not measured) to \(\approx\)​19.5 s/token at position 16,384. Total constraint cost over one 16k replay: GRID 0.05 s vs. s (0.3.1) vs. s (0.1.5) vs.\(\approx\)​44 h (0.0.64, extrapolated).

8.3 MaskBench (JSON Schema)↩︎

GRID claims extensibility to any LALR(1)-parsable language; MaskBench (guidance-ai/jsonschemabench [7]) is the cheapest public test of where that is true. GRID enters via a JSON-Schema\(\to\)grammar compiler and a protocol-exact runner (TTFM/TBM semantics verbatim; llama-3.1 tokenizer; 315-schema stratified sample; host: local dev, unpinned). Table 2 shows the three-way comparison.

GRID’s p25–p75 (14/28/34 μs) is the kernel hit path, with kernels active on \(100\%\) of compiled schemas, and GRID is the only engine with zero validation errors—every valid instance of every schema it compiled was accepted; its 68 invalidation errors are all traceable to deliberately ignored value constraints (the XGrammar-default convention, itemized in the report). Its honesty boundary is llguidance-style: 79/315 schemas are declared compile errors (allOf, patternProperties, if/then/else, …, including 5 genuine LALR conflicts). The TBM p90 traces a clean kernel lineage across the identical 315-schema sample: v3-era \(27.8\) ms \(\to\) v5.1 verdict-equivalence grouping \(208\) μs \(\to\) v7 fused walk\(\to\)blob\(\to\)register \(75\) μs. This is the kernel-v7 re-record: the correctness columns are byte-identical to the earlier records, while the last step—v5.1 to v7—cut TBM p90 a further \(\sim\) \(2.8\times\) (\(208 \to 75\) μs) and the TBM average from \(683\) to \(562\) μs by moving the per-cold-entry Python materialization/glue (and its gen-2 GC pauses) into Rust; the llguidance and XGrammar latency arms moved under \(10\%\) between records, a host-noise control placing the delta on GRID’s side. Two structural facts explain the remaining tails: the TBM p95\(+\) tail is the cold trie walk, which MaskBench’s one-shot-per-schema protocol never lets the write-back cache amortize (the serving benchmark is where that design choice pays), and TTFM is a pure-Python table build (\(19\times\) llguidance’s at p50, but 26–43\(\times\) ahead of XGrammar’s p75\(+\) compile blowups).

8.4 Spider: execution accuracy and checker-guided repair↩︎

Executability is measured where it matters: the full 1,034-question Spider dev set [8], greedy decoding, grammar with \(100\%\) dev-gold coverage plus per-database L3 lexicons—every constrained output parses with schema-valid identifiers by construction (Table 3).

The scale finding, measured at both ends: the mask alone is worth \(+13\) EX points at 0.5B—it erases the syntax-error class a weak model commits constantly (\(+26\) points of syntactic validity)—but only \(\sim\) \(+1\) at 7B, because a capable model rarely errs syntactically. The repair half closes the loop at scale: GRID’s residual 7B failures are alias\(\leftrightarrow\)column binding—exactly the class Proposition 11 proves out of mask scope, and exactly what the alias-aware SemanticChecker names precisely. One constrained retry with the violations quoted back converts a third of that floor (\(91.3 \to 94.5\%\) executes; \(21\%\) of kept retries newly correct) at \(+5\) tokens/query (\(+14\%\)) on the \(\sim\)​7% of queries that engage. The capability symmetry is measured in both directions, not asserted: at 0.5B the same feedback is worthless (an interim run of 55 questions: repair metrics identical to plain GRID—the model repairs its binding mistakes into different-but-equally-wrong queries), while at 7B the mask matters less but the feedback converts—constraint quality determines feedback quality, because the checker can only name violations precisely when the mask has already guaranteed everything else. Ablations on the same harness (EX-invariant by construction): disabling the write-back cache costs \(32\%\) of generation throughput (\(2.5 \to 1.7\) tok/s, \(n{=}20\)); audit-off and jump-forward-off move throughput within noise.

8.5 Batched serving under vLLM↩︎

The end-to-end serving benchmark runs vLLM 0.24 (V1 engine) with Qwen2.5-7B on the declared H100 SXM5 runner: heterogeneous grammars (4 distinct) across batches 1/8/32, unconstrained control arm, warm-through protocol, kernel v7 (Table ¿tbl:tab:serving?).

Warm serving overhead is low at every batch size—\(+1.51\%\) time-per-output-token at batch 32—warm and cold TTFT are \(1.51\) and \(27.3\) ms, and both single-flight behaviors hold. In the cold-miss stress arm the warm co-tenants’ worst engine step is 15.3 ms (thread-invariant at 15–18 ms across walk threads \(0/2/8\)). The one residual cost is a transient co-batched TPOT slowdown of \(+33.8\%\), confined to the fresh schema’s cold window; we characterize it below.

What v7 changed. On the v6 stack the cold window cost more—a \(+114.7\%\) co-batched slowdown and a 36.0 ms worst step—and both were attributed to GIL-bound mask-entry materialization in the fresh request’s cold window. That attribution was half right. Moving the entire cold miss into Rust (§6.2: fused walk\(\to\)blob\(\to\)register, one GIL-released call) collapsed the per-boundary-entry cost \(6.8\)–\(8.7 \to 0.003\) ms and, with it, the worst engine step on real hardware (\(36.0 \to 15.3\) ms). The residual glue theory (“make_entry/encode/hash is the cost”) was disproved by the fix: the real culprit was the WalkResult glue allocating \(\sim\)​30–60k gc-tracked objects per miss, whose gen-2 pauses landed inside the walk—which is exactly why keeping the walk in Rust removed them.

The estimators. The cold-window metrics are computed with artifact-robust estimators (median-over-legs degradation; min-over-legs max step, with the raw per-leg maxima always printed) because vLLM 0.24’s multiprocess engine exhibits a once-per-leg 0.7–2 s frozen engine step that we exonerated five ways before believing it: it fires in all-warm baselines with zero GRID work in flight, is invariant to the defer, warmup, walk-thread, and JIT-warming levers and to both child- and driver-side GC control, and vanishes entirely with the engine in-process—an engine-topology artifact, filed upstream as vllm-project/vllm issue #48229 (the repository’s LESSONS.md §6.8–6.9 holds the exoneration record). The raw per-leg step maxima \([15, 15, 16, 16, 16]\) ms show the v7 max step is now clean and tight, with no exogenous 1–2 s outliers polluting the min-over-legs estimator.

The cold-window slowdown, characterized. At v6 the co-batched degradation was called a Python/GIL/software cost with a kernel fix pending. That fix has shipped, and the degradation did not go to zero—because it was never primarily a software cost. It is genuine host CPU/memory-bandwidth contention between the cold walk and the engine forward loop during the fresh schema’s \(\sim\)​0.66 s specialization window. The diagnostic evidence is direct: the slowdown decreases as walk threads increase, because more threads shrink the window in which the contention occurs—a software-serialization cost would not behave this way. Walk/pool thread niceness mitigates the residual. Full closure is therefore a compute-isolation trade-off (throttle the walk and lengthen the fresh request’s TTFT, or accept the number), noted as future work rather than a defect to fix. Throughout, the fresh request itself pays only its own cost: TTFT \(0.7\) ms, and \(1.00\times\) warm effective TPOT once specialized—there is zero steady-state co-tenant interference. As a pre-v7 observation (superseded by this record, retained only for lineage): an artifact-free JIT-warmed lockstep leg on the v6 stack read \(-1.75\%\) co-batched slowdown and a 23.9 ms max step; the same leg with the defer disabled read \(+373\%\) and 65.7 ms, the attribution that makes the defer the load-bearing protection. Finally, the tempting admission-time warmup alternative was measured harmful on the GIL and ships disabled (§6.3); negative results are recorded next to the positive ones.

8.6 Policy enforcement and end-to-end correctness at scale↩︎

The guarantees of §5 are checked directly, each against the test that exercises the corresponding property.

8.6.0.1 Soundness, completeness, termination end-to-end.

Two arms exercise the whole decode loop. The walk arm generates 10,000/10,000 outputs that parse, with 0 dead ends and 0 budget overruns (local dev). The model arm, driving Qwen2.5-0.5B on the declared H100 runner, generates 1,000/1,000 parseable and audit-verified outputs, again with 0 dead ends, and 706 reserve-completed stops (the termination machinery of Proposition 9 firing as designed).

8.6.0.2 Policy/RBAC enforcement.

A model-free exhaustive speller probes every reachable identifier position: across 58 role\(\times\)position\(\times\)target probes it records 0 bypasses, with 9/9 positive controls reachable so the test is non-vacuous. A 12-prompt injection suite (the adversarial-prompt arm) emits 0 forbidden lexemes on the declared H100 runner, and column-violation fixtures are 100% flagged by the post-parse checker (the residue Proposition 11 places out of mask scope).

8.6.0.3 Differential correctness, cache soundness, and kernel parity.

The fast path is checked bit-exact against the trial-parse oracle over quota-counted corpora including multi-terminal tokens, across a four-tokenizer matrix; the viable-prefix oracle is checked by corpus, mutation, and mid-lexeme EOS differentials against lark. Cache-key soundness (OBL-KEY1) is verified by cache-on \(\equiv\) cache-off runs including cross-role hits, namespace rollover, and racing publishes. Grammar-pipeline reducedness and deterministic fingerprints have property tests. All of these run in CI.

8.7 Audit replay and tamper detection↩︎

Over 1,000 generations spanning 29,242 audited steps and one cache-namespace rollover, every log replays bit-identically (1,000/1,000) against its archived artifacts, and tamper detection catches every injected mutation (1,000/1,000), on local dev.

8.8 Cross-engine comparison, summarized↩︎

Taken together with §8.1: on per-token mask latency GRID leads llguidance and XGrammar at p50 on both tokenizers (Table ¿tbl:tab:engines?), by more than \(2\times\) over XGrammar; llguidance retains the flattest p99. The SynCode and GBNF arms were dropped by decision (2026-07-10) as the engine comparison had already settled on this front.

9 Limitations and honest boundaries↩︎

• Distribution faithfulness. Masking changes the sampling distribution (Remark 2); GRID measures the downstream effect (EX deltas) rather than claiming neutrality. GAD/ASAp-style faithful sampling and CRANE-style two-phase decoding are compatible, deferred arms.

• Column-level RBAC is post-parse by proof (Proposition 11). The mask guarantee is verb- and table-level; the checker covers the residue and feeds repair.

• LALR(1) languages only (v1). MaskBench draws the boundary concretely: 79/315 schemas are declared compile errors, 5 of them genuine LALR conflicts. An Earley fallback is a recorded option, unexercised because no target dialect construct has forced it.

• Cold-walk tails. The cold trie walk over a 100k+ vocabulary is milliseconds by nature; the write-back cache amortizes it across requests (86–98% hit rates in replay- and serving-shaped workloads) and the serving contract keeps it off co-tenants’ critical path, but one-shot workloads see it (MaskBench p95\(+\)). Walk-level pruning is the named next kernel target.

• The cold-window serving contention. A fresh, never-before-seen schema induces a transient co-batched slowdown (\(\sim\)​34% during its \(\sim\)​0.66 s first-request specialization window). The kernel-v7 fused cold-miss path removed the GIL-bound entry-materialization cost that dominated at v6, so the residual is genuine host CPU/memory-bandwidth contention between the cold walk and the engine forward loop; it shrinks as walk parallelism rises and is mitigated by scheduling niceness. The fresh request itself runs at warm speed and steady-state co-tenant requests are unaffected. Fully eliminating it is a compute-isolation trade-off, noted as future work (§8.5).

• One characterized exogenous artifact. The serving record’s per-step tail on vLLM 0.24’s multiprocess topology contains a once-per-leg frozen step that is provably not GRID’s (five-way exoneration, §8.5); the serving metrics use artifact-robust estimators and the issue is filed upstream (vllm-project/vllm #48229) rather than papered over.

• Termination is mode-dependent. The full termination guarantee (reserve-completed stops) holds in the GRID-owned loop; processor-only serving weakens to EOS-only-at-ACCEPT with truncation recorded (Proposition 9).

• Host honesty. Headline performance numbers run on declared cloud runners; local-dev numbers are labeled and used for shape, not records.

10 Related work↩︎

Outlines [1] reformulated guided generation as FSM state transitions with a vocabulary index, extending to CFGs via lexer-aware scanning over parser states—the paper whose problem statement and formal register this work parallels, and an explicit inspiration for GRID’s design. GRID differs in what it keys and what it promises: masks keyed on live LALR configurations with a write-back cross-request cache rather than a per-automaton precomputed index; policy (roles, schemas) compiled into the language; guarantees stated with preconditions and empirically verified; an audit trail. Notably, current Outlines releases delegate CFG constraining to llguidance [9], so the engine-level comparison collapses into the llguidance one (§8.1). guidance/llguidance [9], [10] pair an Earley/derivative core with a token trie; llguidance keeps the flattest p99 tails and the fastest compiles in our measurements and is the bar GRID names—at kernel v7 GRID leads it at p50 and p90 on both tokenizers (§8.1) while llguidance retains the p99 edge. GRID’s answer is also architectural rather than raw-constant: configuration-keyed write-back caching across grammar families, mask-level RBAC/schema projection, requirement R as a committed contract, and the audit chain. XGrammar [11] introduced the context-independent/context-dependent vocabulary split with compile-time precomputation and scheduler overlap; GRID adopts the CI/CD idea but makes the split a cache-key soundness requirement (never cache CD), computes on miss with write-back (rewarding the per-role/per-tenant family shape), and adds the identifier composition rule that per-schema policy needs. SynCode [12] formalizes grammar masks over lexer-state \(\times\) remainder tables with soundness/completeness theorems; its shipped \(d\)-lookahead masks are sound but incomplete, which is incompatible with dead-end freedom—GRID chooses exact byte-level masks for exactly that reason. PICARD [13] pioneered constrained SQL decoding by incremental parsing over beam candidates (reject-and-filter rather than exact masks). Grammar-aligned decoding [4] and CRANE [6] address the distribution and reasoning costs of strict masking; both are complementary layers above an exact-mask engine like GRID. Automata-theoretic treatments of the token–terminal misalignment [14] give the detokenization correctness framing our byte-trie bridge instantiates. JSONSchemaBench [7] supplies the cross-engine schema corpus used in §8.3. Serving integration follows the vLLM structured-output interface [15]. Classical foundations: viable prefixes and LR parsing [2], [3]; linear Earley parsing on LR-regular grammars [16] (the recorded fallback engine).

11 Conclusion↩︎

GRID shows that the properties an enterprise actually needs from constrained decoding—policy compiled into the language, guarantees with preconditions, position-flat guard cost, a replayable audit trail, and batch-safe serving with honest cold-start behavior—all follow from one commitment: key every mask, cache entry, and audit record on the parser configuration, and prove (then verify) that the keys refine the equivalence the semantics requires. The residue the mask provably cannot enforce is not hidden but named, checked post-parse, and—at model scales that can use feedback—repaired. The committed record spans engine microbenchmarks, a public schema corpus, full-dataset execution accuracy, and an end-to-end serving benchmark, each number carried with its host label; the remaining open costs (cold-walk tails, the once-per-schema cold-window serving contention, one upstream engine artifact) are stated as precisely as the wins.

References↩︎