Paper deep dive
Breaking the Space Barrier and its Application to Language Model Inference
Arip Asadulaev
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 92%
Last extracted: 10/8/2026, 6:57:34 AM
Summary
This paper introduces a novel inference engine for language models that enforces structured output (e.g., JSON, tool calls) by leveraging the theoretical properties of 'few-path' graphs. The authors prove that reachability in these graphs can be decided with O(log^2 n / log log n) space, significantly below Savitch's theorem. This theoretical result is applied to create an engine that recomputes masks on the GPU without storing large tables, handles forced text efficiently, supports recursive formats with a small stack, and enables parallel decoding of independent fields. Experiments on Apple M2 Pro hardware show the engine is 1.2-1.3x faster and uses significantly less memory (3 MB vs 1.5 GB) compared to the baseline MLX with llguidance.
Entities (14)
Relation Signals (8)
stcon → outperforms → MLX with llguidance
confidence 95% · schema-constrained extraction finishes 1.2- 1.3x sooner with the same answers
stcon → reducesmemoryusage → 3 MB
confidence 95% · a grammar costs 3 MB instead of up to 1.5 GB
stcon → runson → Apple M2 Pro
confidence 95% · On one 16 GB Apple M2 Pro with Qwen3.5-2B and 4B
stcon → usestheoryof → few-path graphs
confidence 95% · The constructions behind the proofs become an inference engine
stcon → achievesspacecomplexity → O(log^2 n / log log n)
confidence 90% · needs only O(log2 n/ log log n) space, below the classical O(log2 n) of Savitch's theorem
stcon → enables → parallel decoding
confidence 90% · independent fields are decoded in parallel and verified
Apers and Edenhofer → posedquestionabout → few-path graphs
confidence 90% · Apers and Edenhofer [3] recently asked a precise question about such graphs
stcon → supports → recursive formats
confidence 90% · recursive formats use a small stack
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Language models are more and more often asked for structured output: JSON that follows a schema, or a tool call with typed arguments. A small machine, an automaton, enforces the format by forbidding the tokens that would break it. We observe that this machine has a rare property: from any of its states, each token leads along exactly one path. Graphs in which only a few paths join any two points are a classical object of complexity theory, and our theoretical result settles an open question about them: one can decide whether such a graph connects two points while verifying that it really has few paths, with very little memory. Precisely, the problem lies in the classes ReachUL, LOGDCFL, C=L and SC2, and needs only O(log2 n/ log log n) space, below the classical O(log2 n) of Savitch's theorem. The constructions behind the proofs become an inference engine: text the format forces is written without running the model, the mask is recomputed on the GPU without any table, recursive formats use a small stack, every output stays valid under a token limit, and independent fields are decoded in parallel and verified. On one 16 GB Apple M2 Pro with Qwen3.5-2B and 4B, against MLX with llguidance, the standard setup for this hardware, schema-constrained extraction finishes 1.2- 1.3x sooner with the same answers, a grammar costs 3 MB instead of up to 1.5 GB, one server holds sixteen grammars where tables run out of memory, and sixteen tool-calling agents finish 2.5x sooner.
Tags
Links
- Source: https://arxiv.org/abs/2610.09139v1
- Canonical: https://arxiv.org/abs/2610.09139v1
Trouble viewing inline? Open PDF directly →
Full Text
183,701 characters extracted from source content.
Expand or collapse full text
Breaking the Space Barrier and its Application to Language Model Inference Arip Asadulaev Affiliation: MBZUAI Abstract Language models are more and more often asked for structured output: JSON that follows a schema, or a tool call with typed arguments. A small machine, an automaton, enforces the format by forbidding the tokens that would break it. We observe that this machine has a rare property: from any of its states, each token leads along exactly one path. Graphs in which only a few paths join any two points are a classical object of complexity theory, and our theoretical result settles an open question about them: one can decide whether such a graph connects two points while verifying that it really has few paths, with very little memory. Precisely, the problem lies in the classes ReachUL, LOGDCFL, C=L and SC2, and needs only O(log2n/loglogn)O( ^2n/ n) space, below the classical O(log2n)O( ^2n) of Savitch’s theorem. The constructions behind the proofs become an inference engine: text the format forces is written without running the model, the mask is recomputed on the GPU without any table, recursive formats use a small stack, every output stays valid under a token limit, and independent fields are decoded in parallel and verified. On one 16 GB Apple M2 Pro with Qwen3.5-2B and 4B, against MLX with llguidance, the standard setup for this hardware, schema-constrained extraction finishes 1.21.2–1.3×1.3× sooner with the same answers, a grammar costs 3 MB instead of up to 1.5 GB, one server holds sixteen grammars where tables run out of memory, and sixteen tool-calling agents finish 2.5×2.5× sooner. 1 Introduction A language model writes text one token at a time. When an application needs the output in a fixed format, for example a JSON object with given keys or a call to a tool with typed arguments, the format is compiled into a small machine called an automaton. At every step the automaton says which tokens are allowed; all others are forbidden (masked). This is constrained decoding, and libraries such as llguidance [23], Outlines [35] and XGrammar [11] provide it. On a laptop it is usually a cost: the model runs as before, and the mask is extra work at every step. Our starting observation is simple. Fix a state of the automaton and a token. The token is a fixed string of bytes and the automaton is deterministic, so reading the token leads to exactly one next state. If we draw all the ways of reading tokens from a state, we get a tree: there is exactly one path to every point. Graphs with this property, and more generally graphs in which at most k paths join any two points (k-strongly few graphs), are a classical topic of complexity theory, the field that studies how much time and memory problems need. The theory. Apers and Edenhofer [3] recently asked a precise question about such graphs. Suppose you are handed a graph and two points, and you must answer whether the graph has at most k paths between every pair of points and the second point can be reached from the first. How much memory does a classical computer need? The difficulty is that nothing is promised: the graph may contain cycles or astronomically many paths, and the algorithm must notice. We answer the question. The problem can be solved with memory logarithmic in the input size by a machine that never has two ways to reach the same state (the class ReachUL), by a deterministic machine with a stack (LOGDCFL), and by a single algorithm that is fast and uses O(log2n)O( ^2n) memory at the same time (SC2); it also lies in C=L, and it needs only O(log2n/loglogn)O( ^2n/ n) memory, less than Savitch’s classical O(log2n)O( ^2n) for reachability. Section 3 explains these results without assuming any background; the proofs are in Appendix B. The practice. The proofs are built from a few constructive ideas: stop every search at a budget, certify a structure before counting on it, recompute along unique paths instead of storing, keep a small capped stack, and split a problem at points every path must cross. Applied to the graph of one decoding step, these ideas become an engine (Section 4). Text the format forces is written without running the model, so a constrained output needs fewer model runs than a free one; the mask is recomputed on the GPU in microseconds, so no table is stored; forced text is split into tokens exactly as the model’s tokenizer would split it; recursive formats run on a small GPU stack; outputs stay valid under any feasible token limit; and independent fields of a JSON object are decoded in parallel and then verified. Table 1 summarizes the gains against MLX [17] with llguidance, the standard way to run constrained decoding on Apple hardware. Table 1: Headline results on one Apple M2 Pro (16 GB), Qwen3.5-2B / 4B in 4-bit precision, greedy decoding. The baseline is llguidance with MLX: in our decode loop with the same kernels for the first two rows, stock mlx-lm with llguidance for the last three. Setting MLX + llguidance stcon (ours) six JSON extractions, decode time (2B / 4B) 2.41 / 4.59 s 1.89 / 3.89 s memory of a 1,106-state tool-call grammar does not compile (token table: 824 MB) 3.4 MB sixteen tool-calling agents, wall time (2B) 74.6 s 29.3 s eight concurrent tool-call requests (2B) 134 tok/s 410 tok/s eighteen JSON jobs, 8 parallel slots, keys-only prompt (2B) 6.12 s 3.83 s Contributions. (1) We settle the classical complexity of total few-path reachability, the question of Apers and Edenhofer, with three new constructions, and extend them to arbitrary walk budgets, a compiler for programs with few computation paths, completeness results, a sharp threshold phenomenon and a structure theory (Section 3, Appendix B). (2) We turn these constructions into six exact mechanisms for constrained decoding, each with a theorem (Section 4, Appendix C). (3) We build them into an engine on MLX and measure speed, answer quality and memory (Section 5, Appendices E–H). 2 Background Why a laptop counts model runs. To produce one token, the model runs once over its whole network, and on a laptop that run is dominated by reading all the weights from memory (1.1 GB for Qwen3.5-2B, 2.26 GB for the 4B). The arithmetic is nearly free next to it. Two consequences guide everything below: a token that can be written without running the model saves a whole run, and a run that processes several tokens at once costs barely more than a run for one (Fig. 1). 1144881212161600224466tokens processed in one runcost (one token =1=1)if cost were linearmeasured Figure 1: What one model run costs (Qwen3.5-2B on an M2 Pro). A run over 8 tokens costs 1.6×1.6× a run over one, not 8×8×, because the run is dominated by reading the weights. So skipping runs saves time, and tokens added to a run that happens anyway are almost free. Constraints. A JSON schema or a regular expression is compiled into a deterministic automaton over bytes: a few hundred states, and in each state a set of allowed bytes. The vocabulary of Qwen3.5 has 248k tokens, each a string of bytes. At every step the decoder needs the mask (which tokens keep the output valid) and, after sampling, the next state. Existing libraries compute the mask on the CPU at every step; on a laptop this forces the GPU to wait for the CPU once per token. Graphs, walks and few paths. A directed graph has vertices and arrows. A walk follows arrows and may revisit vertices; standing still counts as one walk. A graph is k-strongly few if at most k walks join any two vertices, and a mangrove if at most one does (Fig. 2). Such a graph cannot contain a cycle, because going around a cycle again and again gives infinitely many walks. A forced chain is a run of vertices with one way in and one way out: whoever enters it must walk to its end. sstttwo walks: N(s,t)=2N(s,t)=2sstta forced chain (blue), then a choice Figure 2: Left: the smallest graph with two walks between a pair; it is 2-strongly few. Right: a vertex with one way in and one way out is forced: whoever enters a forced chain walks it to its end. Theorem 11 says that once forced chains are contracted, at most 2k2k vertices remain between any two vertices; in decoding, a forced chain is output the model is not asked about. Complexity classes in plain words. Complexity theory measures problems by the resources a machine needs. Here the resource is memory, measured in bits as a function of the input size n; “logarithmic space” means a few counters of logn n bits, enough to remember a handful of vertex names but not the graph. Table 2 lists the classes that appear in our results. The classical benchmark is directed reachability: it is in NL, and the best known deterministic algorithm, Savitch’s, uses O(log2n)O( ^2n) space. Table 2: The complexity classes in our results, in plain words. All machines use logarithmic memory unless stated otherwise. Class What the machine may do L compute deterministically NL guess, and accept if some sequence of guesses succeeds (directed reachability is the typical problem) ReachUL guess, but every state of the machine is reachable by at most one sequence of guesses: no ambiguity anywhere LOGDCFL compute deterministically with an extra stack of unlimited size, in polynomial time SC2 one deterministic algorithm that is fast (polynomial time) and uses O(log2n)O( ^2n) memory simultaneously C=L decide whether a signed count of computation paths is exactly zero PL decide whether such a count is positive (much more powerful) 3 The theory in plain words The problem. The input is a graph G, two vertices s,ts,t and a number k. Answer yes exactly when G is k-strongly few and t can be reached from s. We call this problem STCONsf STCON_sf. The word and is the whole difficulty: the algorithm is not promised a good graph. It must also say no on graphs with cycles or with exponentially many walks, and it must do so with the same tiny memory. Think of a ticket inspector who must not only check that a ticket is valid but also detect forgeries, without ever taking notes longer than a few lines. Theorem 1 (Main theorem, informal). STCONsf STCON_sf can be solved by an unambiguous machine with logarithmic memory (ReachUL), by a deterministic machine with a stack (LOGDCFL), by a single fast algorithm with O(log2n)O( ^2n) memory (SC2), and by a zero test of a signed count (C=L). It needs only O(log2n/loglogn)O( ^2n/ n) memory, less than Savitch’s O(log2n)O( ^2n). Theorem 2 in Appendix B is the formal version. Apers and Edenhofer had shown that a quantum computer with logarithmic memory solves the problem and asked whether these classical bounds hold; Theorem 1 answers yes. Three ideas prove it, and each reappears in the engine. Idea 1: stop every search at a budget. If every vertex may be the end of at most k walks from a start, the total budget is B=nkB=nk. A walk of length B has B+1B+1 prefixes, all different walks, which is more than the budget allows. So it suffices to explore walks of length at most B: either everything has been seen, or a violation has already been found. With this cap, a depth-first search that keeps only a stack of “where to continue” always stops, even on a cyclic graph, and this gives the stack machine (Theorem 8). Idea 2: certify, then count. Give every walk a short fingerprint, a polynomial hash of its edges, and build the graph of (endpoint, length, fingerprint). If no two walks collide, counting the reachable fingerprints counts the walks. The machine first certifies that no collision happened, by a check that itself never becomes ambiguous, and only then counts (Theorem 9). If the graph is good, some choice of hash has no collision; if the graph is bad, either no hash certifies or the count exposes the violation. Idea 3: one equation for everything. For each pair of vertices, the product (N−0)(N−1)⋯(N−k)(N-0)(N-1)·s(N-k) is zero exactly when the walk count N is at most k. Summing the squares of all these products gives a single number that is zero exactly on good inputs (Theorem 10). What else follows. The same ideas validate any system of walk budgets, not just a uniform k; they turn any program whose number of computation paths is expected to be small into one that checks this on every input (Theorem 4); fixing k gives problems that are as hard as anything in ReachUL (Theorem 5); and writing k in binary instead of unary makes the problem jump to PL-complete (Theorem 6). Few-path graphs also have a clean shape (Appendix B): between two vertices almost everything is a forced chain, at most 2k2k branching vertices remain (Theorem 11), and the paths split into independent pieces at vertices that every path crosses (Theorem 12). The engine uses exactly these two facts. 4 From the theory to the decoding engine The step graph is a mangrove. Store the vocabulary as a trie: a tree of byte strings in which tokens share their prefixes (0.59 million nodes for Qwen3.5). Fix an automaton state q and pair every trie node with the state the automaton reaches after reading that node’s bytes from q (Fig. 3). Each node has one parent, because the trie fixes the bytes and the automaton is deterministic, so this step graph is a tree, a mangrove. Every token sits at exactly one node, which carries its next state (Proposition 1). Six mechanisms follow (Table 3); Appendix C states each as a theorem and Appendix C proves it. q0q_0q1q_1q2q_2"a-z"automatonε ""avocabulary trie(ε,q1)( ,q_1)(a,q1q_1)(ab,q1q_1)(",q2q_2)("a: dead)step graph Pq1P_q_1: a tree Figure 3: The step graph. Left: an automaton for a quoted word. Middle: part of the vocabulary trie. Right: their product from q1q_1. Every trie node appears with the one state the automaton is in when it gets there, so there is exactly one route to every vertex. The token "a is dead from q1q_1 because no letter may follow the closing quote. 1. The mask without a table (from “recompute, do not store”). A naive engine stores, for every state and token, the next state: 3|Q|×248k3|Q|× 248k bytes, 77 MB for a 104-state schema and 1.5 GB for 1,970 states. Because every token has a single path, the needed row can be recomputed at every step: a GPU kernel runs one thread per token, walks the token’s bytes through the automaton and writes the state it reaches. This takes 7–18 μ per step against a 7–15 ms model run, and a grammar costs only its automaton (512 bytes per state) plus 2.9 MB of vocabulary shared by all grammars (Theorem 18). Since the mask lives on the GPU, the GPU never waits for the CPU. 2. Forced text is free (from forced chains). Much of a JSON output is not chosen by the model: after "name":"Maria" the schema allows only ,"age":. A state with one allowed byte is a forced chain. After each sampled token the engine feeds the whole forced continuation in the same model run, so it costs nothing extra (Fig. 4). The output is exactly what token-by-token decoding would give, and no decoder that does not speculate can use fewer runs (Theorem 19). A key costs no run at all, however long it is, and a field with r possible values costs at most r−1r-1 runs (Corollary 1). "name":"Maria␣Gonzalez","age":34,"email":"maria.g@example.com","status":"approved","tags":["hiking","photography","machine␣learning"] Figure 4: One constrained output, token by token (Qwen3.5-2B, the person schema). White: sampled by the model (27 tokens, 27 passes). Blue: forced by the constraint (7 tokens, fed in the passes of the preceding sampled tokens). The key splits (name then ":") are the tokenizer’s own (Section C.4). 3. Forced text in the tokenizer’s own split (from the block product). The forced bytes ":" can be split into tokens in several ways, but the model was trained on the tokenizer’s split only. Tokenizers first cut text into words, numbers and punctuation runs; these cuts are points every tokenization crosses, so the split factors into independent blocks and only the last block can change when more text arrives. The engine commits every block except possibly the last, and a one-byte test certifies when the last one is safe too (Theorem 20). 4. Never cut a value in half (from budgets). If an output reaches the token limit in the middle of a value, it does not parse. The engine precomputes, for every state, the fewest tokens needed to finish validly (a shortest-path table), and allows a token only if a valid ending still fits. Every output is then valid under every limit that admits a valid output at all, and no less restrictive rule has this guarantee (Theorem 21). 5. Recursive formats with a small stack (from the stack machine). A schema for a tree of nodes refers to itself, so no finite automaton describes it. As in Idea 1, the engine uses an automaton plus a capped stack of return points, kept on the GPU (64 entries). We prove that a token depends only on the stack entries it pops, so a table indexed by the top two entries suffices (Theorem 22). qaq_aqbq_brrqcq_c":[]call: push r"name":⋯·sreturn: pop, continue at rrstate on the GPU:[q,stack pointer,stack[0..63]][\,q,\ stack pointer,\ stack[0..63]\,] Figure 5: A recursive schema as an automaton with a stack. A child node is a “call”: the engine pushes the place to return to (r) and starts a new node; the node’s closing bracket pops it. The whole state, stack included, is a small integer vector on the GPU. 6. Independent fields in parallel, then verified (from “certify, then count”). The language of a JSON object splits at each key, a point every valid output crosses, so the values can be drafted in parallel as rows of one batch. The model then checks the whole draft in one run, position by position; the first wrong token is corrected and its field continues. The result is token-identical to sequential greedy decoding (Theorem 23). prompt(read once)name: "Maria Gonzalez"age: 34email: "maria.g@..."tags: ["hiking",...]assemblethe draftcheck in one run:would the modelpick every token?yes: output(= sequential)no: fix the firstwrong token, redothat field only Figure 6: Certified parallel decoding. The fields of a JSON object are drafted at the same time, as rows of one batch, then the model checks the whole draft in one run. The result is identical to decoding token by token. Table 3: From the theory to the engine. Each mechanism reuses an idea of Section 3; the guarantee is proved in Appendix C. Mechanism Idea from the theory Guarantee mask without a table recompute along the unique path same mask as a full table; memory = automaton forced text in the same run forced chains same output; fewest model runs possible without speculation tokenizer’s split paths split at crossing points committed tokens are the tokenizer’s own split budget rule stop at a budget; shortest paths valid under every feasible limit; least restrictive GPU stack for recursion capped stack machine exact up to nesting depth 64 certified parallel fields split at crossing points; certify, then use identical to sequential greedy decoding 5 Experiments Setup. All measurements run on one Apple M2 Pro laptop (19-core GPU, 16 GB of unified memory) with two current open models, Qwen3.5-2B and Qwen3.5-4B, in 4-bit precision and with greedy decoding. The baseline is MLX with llguidance [17, 23], the standard way to run structured generation on Apple hardware. We use it in two forms. For single requests, llguidance runs inside our MLX decode loop with exactly the same matrix kernels, in its mask-only mode and in its fast-forward mode, so that every difference comes from how the constraint is handled. For serving, batches and agents, we compare the whole engine with stock mlx-lm plus llguidance. The workloads are six JSON extractions with schemas (a person record, a tool call, a product, an event with attendees, a review classification and a contact card), four recursive schemas (trees of nodes), and coding agents that call tools. We report the time to finish a task, the number of model runs, and answer quality; every timing is a median of interleaved rounds in one process. Our practical results at a glance. (1) Faster: structured extraction finishes 1.28×1.28× (2B) and 1.18×1.18× (4B) sooner than MLX + llguidance, and 1.8×1.8× sooner than its mask-only mode, with 31% of all tokens written without running the model. (2) Same answers: every output valid, 45/45 fact fields correct, character-identical outputs on the 2B. (3) Small: a grammar costs 3 MB instead of up to 1.5 GB; one server keeps 16 grammars where token tables crash at the 15th. (4) Guaranteed: 90/90 outputs valid under tight token limits (3/90 without our rule); parallel decoding reproduces greedy outputs with 1.8×1.8× fewer model runs. (5) In real use: 2.55×2.55× faster for sixteen coding agents and 3.1×3.1× the throughput for concurrent tool calls against stock mlx-lm + llguidance. 5.1 Structured output is faster Table 4: Speed, six JSON extractions, one request at a time; llguidance runs in the same MLX loop. Decode time for all six outputs and time per model run. decode time (s) ms per run engine 2B 4B 2B / 4B llguidance, mask only 3.34 6.08 9.7 / 18.3 llguidance, fast-forward 2.41 4.59 9.8 / 18.8 stcon (ours) 1.89 3.89 8.3 / 17.1 speedup vs fast-forward 1.28×1.28× 1.18×1.18× speedup vs mask only 1.77×1.77× 1.56×1.56× Table 5: Model runs for the same six outputs (2B): runs per output token and tokens written without a run. engine runs / token forced free text, no constraint 1.01 0% llguidance, mask only 1.00 0% llguidance, fast-forward 0.72 28% stcon (ours) 0.69 31% Table 5 is the main speed result: on the same prompts, with the same model and the same kernels, stcon finishes the six extractions in 1.89 s on the 2B where MLX with llguidance needs 2.41 s in its best mode and 3.34 s with masks only; on the 4B, 3.89 s against 4.59 s and 6.08 s. The gain decomposes exactly into the two mechanisms of Section 4. First, fewer model runs: forced text rides along with sampled tokens, so the six outputs need 226 runs instead of 343 (Table 5); a constrained stream needs fewer runs per token (0.69) than unconstrained text (1.01). Second, cheaper runs: because the mask is computed on the GPU, the GPU never waits for the CPU, and a run costs 8.3 ms instead of 9.7 ms. Multiplying the two, 343×9.7ms=3.3343× 9.7\,ms=3.3 s becomes 226×8.3ms=1.9226× 8.3\,ms=1.9 s. llguidance’s fast-forward mode also skips forced tokens, but it keeps the CPU-side mask, so each of its runs costs 9.8 ms and it ends up 1.28×1.28× slower. 5.2 The answers stay the same Table 6: Answer quality, six JSON extractions (2B / 4B). Gold: 45 fact fields read off the source texts. llguidance stcon valid outputs 6/6, 6/6 6/6, 6/6 fact fields correct 45/45, 45/45 45/45, 45/45 values as in free answer 49/52, 47/55 49/52, 47/55 Table 7: How forced text is split into tokens (2B, same constraint): agreement with the model’s free answer, and model runs. how forced text is fed agreement runs llguidance, mask only 0.95 341 llguidance, fast-forward 0.95 245 model chooses the split 0.93 343 whole chain, any split 0.93 246 stcon: tokenizer’s own split 0.95 224 Speed would be worthless if the answers changed. Table 7 checks three things: whether outputs parse and follow the schema, whether the 45 facts that the source texts state (names, ages, prices, dates, cities, phone numbers, enum values and list items) are extracted correctly, and how many values coincide with what the model writes without any constraint. Both engines are perfect on validity and on the facts, and on the 2B the outputs of stcon and llguidance are character for character identical. Table 7 shows why the tokenizer rule of Section 4 matters. If forced text is fed in any split, or the model is left to choose the split, agreement drops: in one case the model writes “Just-Luc Moreau” where it otherwise writes “Jean-Luc”. Feeding forced text exactly as the tokenizer would split it restores the agreement and also needs the fewest runs of all, 224. 5.3 Recursive formats keep their speed Table 8: Recursive schemas (trees), one request: time per model run (2B / 4B), throughput and valid outputs (2B). engine ms / run tok/s valid llguidance, mask only 9.8 / 18.0 94 4/4 llguidance, fast-forward 10.0 / 18.8 143 4/4 stcon (GPU stack) 8.7 / 17.0 170 4/4 A schema that refers to itself, such as a tree of nodes with children, cannot be written as a regular expression; the regex library we build on unrolls three levels and then silently drops the recursive field. Our GPU stack handles any depth up to 64, at 170 tokens/s against 143 and 94 for llguidance on the 2B (Table 8). Recursion costs almost nothing extra because the stack lives on the GPU together with the automaton state, so the decode loop never waits for the CPU, and because forced text crosses the stack’s returns: after the last value of a node, the closing brackets and the next opening key, ],"name":", are fed as one forced span. Every engine produces valid trees on these tasks; when the model nests without end, our engine stops cleanly at the depth limit. 5.4 A grammar costs megabytes, not gigabytes Table 9: Constraint memory per grammar (248k-token vocabulary). Ours: automaton only, plus 2.9 MB shared by all grammars. grammar (states) token table llguidance stcon person schema (104) 77 MB <<0.5 MB 0.05 MB typed tool calls (1,106) 824 MB fails 0.57 MB 96 fields (1,970) 1.5 GB <<0.5 MB 1.0 MB sixteen grammars 7.2 GB 4.7 MB 4.9 MB shared, paid once — 153 MB 2.9 MB Table 10: One server, sixteen grammars in turn: grammars served, GPU memory above the model, longest wait for a first answer. mask served memory wait 2B tables 15, crash 8.2 GB 26 s ours 16 0.6 GB 2.8 s 4B tables 14, crash 6.9 GB 26 s ours 16 1.1 GB 6.6 s A precomputed mask table grows with the grammar and stays in memory for the life of the server: 77 MB for a five-field schema, 824 MB for a tool-call grammar, 1.5 GB for a 96-field form. Because our mask is recomputed on the GPU at every step in 7–18 μ , a grammar costs only its automaton, a few hundred kilobytes, and decoding runs at the table’s speed with identical outputs (Table 10). This changes what a laptop server can do. The typed tool-call grammar, which fixes the name and the type of every argument of every tool, has 1,106 states; llguidance cannot compile it and its table does not fit in the server, while with our kernel it costs 3.4 MB and 46 of 46 tool calls from eight concurrent agents arrive with every argument present and correctly typed, against 43 of 52 with an untyped grammar at the same speed. When a server sees many different grammars, as an agent platform does, tables accumulate until the process crashes; ours serves all sixteen within about 1 GB (Table 10, Fig. 7). 005510101515002,0002,0004,0004,0006,0006,000crash at 15different grammars servedmemory above model (MB)token tablesstcon0055101015150010102020different grammars servedwait for first answer (s)token tablesstcon Figure 7: A server that receives sixteen different grammars (Qwen3.5-4B). With token tables, memory grows by hundreds of megabytes per grammar, the fourteenth grammar waits 26 s for its first answer, and the fifteenth crashes the server. With stcon, all sixteen fit in about 1 GB and first answers stay fast. 5.5 Guarantees: valid under any limit, and exact in parallel Table 11: Guarantees (2B unless stated). Top: valid outputs under token limits. Bottom: model runs for 18 outputs; certified blocks give the same tokens. valid under a token limit no rule our rule JSON, every feasible limit 3/90 90/90 recursive, 61 limits 2/61 54/61 runs for 18 outputs sequential ours Qwen3.5-2B 672 374 (exact) Qwen3.5-4B 686 484 (exact) Table 12: One output under shrinking limits (event schema, 2B): with our rule the output stays valid and shortens gracefully. limit output (abridged) 320 "title":"The Applied AI Summit", …, "attendees":[3 people] 48 …, "attendees":["name":"Dr.", "role":"speaker"] 32 …, "venue":"", "city":"", …, "attendees":[] 40, no rule …, "attendees":["name":" (broken) Every application sets a token limit, and an output cut in the middle of a value does not parse. With the budget rule of Section 4, every JSON output is valid under every limit that admits a valid output at all, 90 of 90, against 3 of 90 without it, and for recursive schemas 54 of 61 against 2 of 61 (Table 12). Table 12 shows how: as the limit tightens, the engine closes the attendee list early, then shortens strings, then empties them, instead of stopping mid-value. Certified parallel decoding, which drafts the fields of an object at the same time and then verifies them, reproduces the sequential greedy outputs token for token on all 36 tests with 1.80×1.80× (2B) and 1.42×1.42× (4B) fewer model runs. On this laptop GPU extra rows in a batch are not free, so the wall time does not drop yet; the saving in runs is the hardware-independent number and turns into time on accelerators where extra rows are nearly free. 5.6 The whole engine in real use Table 13: The whole engine against stock mlx-lm with llguidance (2B unless stated). These numbers also include our matrix kernels and batching, which are engineering rather than theory. workload mlx-lm + llguidance stcon gain 16 coding agents with tool calls, wall time 74.6 s 29.3 s 2.55×2.55× 8 concurrent tool-call requests through the server 134 tok/s 410 tok/s 3.1×3.1× 18 JSON jobs, 8 slots, schema in the prompt 6.12 s 4.66 s 1.31×1.31× 18 JSON jobs, 8 slots, keys-only prompt for stcon 6.12 s 3.83 s 1.60×1.60× 8 streams, no constraint, 2B / 4B (stock mlx-lm) 188 / 87 tok/s 576 / 271 tok/s 3.1×3.1× 40 LiveCodeBench problems, 8 streams, 4B (stock mlx-lm) 1,181 s 476 s 2.5×2.5× In practice the constraint mechanisms run together with our batched matrix kernels, which read the weights once per step for all requests. Table 13 measures the complete systems. Sixteen coding agents, each calling tools such as write_file and run_python in the model’s native format with every reply constrained to a well-formed call, finish their suite in 29.3 s instead of 74.6 s, and more of them finish within the time limit (12 against 9 of 16). Through our OpenAI-compatible server, eight concurrent tool-using requests are served at three times the throughput, and every reply parses. A batch of eighteen JSON jobs finishes 1.31×1.31× sooner with the same prompts, and 1.6×1.6× sooner when the prompt lists only the keys and options, because forced text supplies the schema’s syntax without the model reading it. Without any constraint, eight parallel streams run three times faster than stock mlx-lm, and forty recent LiveCodeBench programming problems finish in 476 s instead of 1,181 s, with a similar pass rate (12 against 13 of 40). The engine thus brings structured, tool-using workloads that are usually reserved for servers within reach of a 16 GB laptop. 6 Related work Few-path complexity. Unambiguous and few-path logspace computation was introduced by Buntrock, Jenner, Lange and Rossmanith [5]; Allender and Lange [1] introduced mangroves and the O(log2n/loglogn)O( ^2n/ n) simulation of ReachUL; Lange [21], Reinhardt and Allender [28], Garvin et al. [13] and Pavan et al. [26] developed unambiguous logspace further. Apers and Edenhofer [3] solved few-path reachability in quantum logspace and asked for its classical complexity, which we settle. Constrained decoding. Outlines [35] precomputes allowed tokens per state; llguidance [23] computes masks on the CPU with fast-forward tokens; XGrammar [11], SynCode [33] and grammar-constrained decoding [15] handle context-free grammars; SGLang [37] decodes runs of forced transitions in one step; Koo et al. [20] compose the tokenizer with the automaton. Non-canonical tokenizations hurt accuracy [4, 14, 34]. Fewer model runs. Speculative decoding [22, 7] and lookahead decoding [12] verify drafts; our forced spans are drafts accepted with certainty, and certified blocks verify drafts that the grammar makes independent. 7 Discussion Where the gains come from, and where they transfer. The speedups of Section 5 have two sources that are independent of the particular hardware. Skipping model runs for forced text helps whenever a model run is expensive compared with the work of the constraint, which is the case on every device where decoding is limited by memory bandwidth: laptops, phones and edge accelerators, and servers that decode few requests at a time. Keeping the mask on the GPU helps whenever the CPU and the GPU would otherwise take turns, which is the case in any decode loop that waits for a CPU-side mask before the next step. When a server batches many requests so that each step is limited by arithmetic rather than memory, extra tokens in a run stop being free, and the first gain shrinks (in our batch at 16 slots it disappears), while the memory gains remain. What a practitioner gets. The engine is a drop-in OpenAI-compatible server: any JSON schema, regular expression or tool-call format can be sent with a request and is enforced exactly, without compiling a table, with outputs that always parse, even when the token limit is reached. Prompts can be shorter, since the format’s syntax is supplied by forced text. Many grammars and many agents can share one 16 GB laptop, because a grammar costs megabytes. All of this keeps the model’s own answers: on our extraction tasks the facts extracted are the same as with llguidance, and on the 2B the outputs are identical character for character. Why the theory was useful. Each mechanism could have been tried as a heuristic; the theory is what turns it into a guarantee. Forced spans are not just “skip easy tokens”: the pass-optimality theorem says the output is unchanged and no exact decoder without speculation can use fewer runs. The table-free mask is not an approximation: one path per token means the recomputed row equals the table exactly. The budget rule is not a timeout: it is a shortest-path invariant that keeps every output valid and is provably the least restrictive such rule. Parallel decoding is not a guess that fields are independent: the grammar’s split points license the draft, and the verification makes the result identical to sequential decoding. In each case the proof also told us what to measure. Outlook. Three directions follow directly. The table-free GPU walk can be extended to the recursive path, so that recursive grammars also cost only megabytes and can be batched. The same mechanisms apply unchanged to other accelerators and larger models, where the memory savings matter even more. And forced spans and certified blocks combine naturally with sampling-based decoding, since both are defined for any sampling rule. On the theoretical side, the remaining question is whether STCONsf STCON_sf belongs to StrongFewL, which would make it a natural complete problem for that class. Limitations. Our measurements use one machine and one model family, six JSON schemas, four recursive schemas and greedy decoding. The recursive path serves one request at a time, and it accepts grammars whose recursive alternatives can be told apart by their first byte, which covers JSON schemas but not every grammar. Certified parallel decoding saves model runs but not yet wall time on this GPU. 8 Conclusion Total few-path reachability, the question of Apers and Edenhofer, is solved with logarithmic memory by an unambiguous machine, by a deterministic stack machine and by a single zero test, and in less memory than Savitch’s bound. The same constructions organize structured decoding: what the format forces costs no model run, the mask is recomputed instead of stored, forced text keeps the tokenizer’s split, recursion is a small stack, outputs stay valid under any feasible limit, and independent fields run in parallel and are verified. Few paths, in short, mean fast decoding: the structure that makes the theory work is the structure that makes structured output cheap. 0011223344stconfast-forwardmask only3.343.342.412.411.891.89seconds, six JSON extractions (2B)002020404060608080stconbaseline74.674.629.329.3seconds, sixteen coding agents (2B) Figure 8: Practical results in two numbers. Left: one request at a time, same model and kernels, 1.28×1.28× faster than llguidance’s fast-forward mode and 1.77×1.77× faster than its mask-only mode, with the same answers. Right: the whole engine on an agent workload, 2.55×2.55× faster than the baseline, stock mlx-lm with llguidance. Statement of novelty The theoretical results of this paper, the classical placement of total few-path reachability in ReachUL, LOGDCFL, C=L and SC2 with its sub-Savitch space bound, the budget, compiler, completeness and threshold results, and the structure theory of few-path graphs, were obtained independently by the author in August 2026. The remaining time was spent on the practical application: identifying the few-path structure of constrained decoding, deriving the decoding mechanisms and their guarantees from the constructions of the proofs, building the engine on MLX. References [1] E. Allender and K.-J. Lange. RUSPACE(logn)⊆DSPACE(log2n/loglogn) RUSPACE( n) DSPACE( ^2n/ n). Theory of Computing Systems, 31:539–550, 1998. [2] E. Allender, K. Reinhardt, and S. Zhou. Isolation, matching, and counting: uniform and nonuniform upper bounds. Journal of Computer and System Sciences, 59(2):164–181, 1999. [3] S. Apers and R. Edenhofer. Directed st-connectivity with few paths is in quantum logspace. In Computational Complexity Conference (C), LIPIcs 339, Article 18, 2025. [4] L. Beurer-Kellner, M. Fischer, and M. Vechev. Guiding LLMs the right way: fast, non-invasive constrained generation. In ICML, 2024. [5] G. Buntrock, B. Jenner, K.-J. Lange, and P. Rossmanith. Unambiguity and fewness for logarithmic space. In Fundamentals of Computation Theory (FCT), LNCS 529, pages 168–179, 1991. [6] R. Beigel and B. Fu. Circuits over P and PL. In IEEE Conference on Computational Complexity, pages 24–35, 1997. [7] C. Chen, S. Borgeaud, G. Irving, J.-B. Lespiau, L. Sifre, and J. Jumper. Accelerating large language model decoding with speculative sampling. arXiv:2302.01318, 2023. [8] S. A. Cook. Deterministic CFL’s are accepted simultaneously in polynomial time and log squared space. In STOC, 1979. [9] T. Dao, D. Y. Fu, S. Ermon, A. Rudra, and C. Ré. FlashAttention: fast and memory-efficient exact attention with IO-awareness. In NeurIPS, 2022. [10] K. Dinesh and C. Sasidharan. Space complexity of reachability in simple path graphs. In MFCS, LIPIcs 386, 2026. [11] Y. Dong, C. F. Ruan, Y. Cai, R. Lai, Z. Xu, Y. Zhao, and T. Chen. XGrammar: flexible and efficient structured generation engine for large language models. In MLSys, 2025. arXiv:2411.15100. [12] Y. Fu, P. Bailis, I. Stoica, and H. Zhang. Break the sequential dependency of LLM inference using lookahead decoding. In ICML, 2024. [13] B. Garvin, D. Stolee, R. Tewari, and N. V. Vinodchandran. ReachFewL = ReachUL. Computational Complexity, 23(1):85–98, 2014. [14] R. L. Geh, H. Zhang, K. Ahmed, B. Wang, and G. Van den Broeck. Where is the signal in tokenization space? In EMNLP, 2024. [15] S. Geng, M. Josifoski, M. Peyrard, and R. West. Grammar-constrained decoding for structured NLP tasks without finetuning. In EMNLP, 2023. [16] Guidance contributors. Guidance: a guidance language for controlling large language models. https://github.com/guidance-ai/guidance, 2023. [17] A. Hannun, J. Digani, A. Katharopoulos, and R. Collobert. MLX: efficient and flexible machine learning on Apple silicon. https://github.com/ml-explore/mlx, 2023. [18] N. Immerman. Nondeterministic space is closed under complementation. SIAM Journal on Computing, 17(5):935–938, 1988. [19] N. Jain, K. Han, A. Gu, W.-D. Li, F. Yan, T. Zhang, S. Wang, A. Solar-Lezama, K. Sen, and I. Stoica. LiveCodeBench: holistic and contamination free evaluation of large language models for code. arXiv:2403.07974, 2024. [20] T. Koo, F. Liu, and L. He. Automata-based constraints for language model decoding. In COLM, 2024. [21] K.-J. Lange. An unambiguous class possessing a complete set. In STACS, LNCS 1200, pages 339–350, 1997. [22] Y. Leviathan, M. Kalman, and Y. Matias. Fast inference from transformers via speculative decoding. In ICML, 2023. [23] M. Moskal et al. llguidance: super-fast structured outputs. https://github.com/guidance-ai/llguidance, 2024. [24] X. Ning, Z. Lin, Z. Zhou, Z. Wang, H. Yang, and Y. Wang. Skeleton-of-Thought: prompting LLMs for efficient parallel generation. In ICLR, 2024. [25] K. Park, J. Wang, T. Berg-Kirkpatrick, N. Polikarpova, and L. D’Antoni. Grammar-aligned decoding. In NeurIPS, 2024. [26] A. Pavan, R. Tewari, and N. V. Vinodchandran. On the power of unambiguity in log-space. arXiv:1001.2034, 2010. [27] O. Reingold. Undirected connectivity in log-space. Journal of the ACM, 55(4), 2008. [28] K. Reinhardt and E. Allender. Making nondeterminism unambiguous. SIAM Journal on Computing, 29(4):1118–1131, 2000. [29] A. Santilli, S. Severino, E. Postolache, V. Maiorca, M. Mancusi, R. Marin, and E. Rodolà. Accelerating transformer inference for translation via parallel decoding. In ACL, 2023. [30] A. Saxena. Prompt lookup decoding. https://github.com/apoorvumang/prompt-lookup-decoding, 2023. [31] I. H. Sudborough. On the tape complexity of deterministic context-free languages. Journal of the ACM, 25(3):405–414, 1978. [32] R. Szelepcsényi. The method of forced enumeration for nondeterministic automata. Acta Informatica, 26:279–284, 1988. [33] S. Ugare, T. Suresh, H. Kang, S. Misailovic, and G. Singh. SynCode: LLM generation with grammar augmentation. arXiv:2403.01632, 2024. [34] T. Vieira, B. LeBrun, M. Giulianelli, J. L. Gastaldi, B. DuSell, J. Terilla, T. J. O’Donnell, and R. Cotterell. From language models over tokens to language models over characters. arXiv:2412.03719, 2024. [35] B. T. Willard and R. Louf. Efficient guided generation for large language models. arXiv:2307.09702, 2023. [36] S. Yang, J. Kautz, and A. Hatamizadeh. Gated Delta Networks: improving Mamba2 with delta rule. In ICLR, 2025. [37] L. Zheng, L. Yin, Z. Xie, C. Sun, J. Huang, C. H. Yu, S. Cao, C. Kozyrakis, I. Stoica, J. E. Gonzalez, C. Barrett, and Y. Sheng. SGLang: efficient execution of structured language model programs. In NeurIPS, 2024. Appendix The appendix is self-contained. Appendix A explains the inference terms. Appendix B proves every statement of Section 3, Appendix C every statement of Section 4. Appendix D describes the mechanisms and the engine as implemented. Appendices E–H hold every measurement, Appendix I the negative results, and Appendix J the tests and the scripts. Appendix A Background in plain words, and what goes wrong on a laptop Decoding. A language model is given a prompt, a list of tokens, and produces a score (a logit) for every token of its vocabulary (248,320 tokens for the Qwen3.5 models) as the next one. The engine picks one, appends it and asks again. Taking the highest-scoring token is greedy decoding; drawing at random from the scores is sampling. Processing the prompt is the prefill; producing the answer token by token is the decode. One decode step is one forward pass, which on a laptop reads all of the model’s weights from memory: a weight stream. A pass that appends several tokens at once costs little more than a pass that appends one, because the weights are read once either way. Caches. A transformer keeps, for every token it has seen, a small vector per layer (the KV cache), so that it need not re-read the prompt. The Qwen3.5 models are hybrid: three of every four layers are recurrent (Gated DeltaNet [36]) and keep a fixed-size state instead of a per-token cache. On the 4B the KV cache costs 32 KB per token per stream and the recurrent state 50 MB per stream. Constraints. A constraint says which outputs are acceptable: a JSON schema, a regular expression, the grammar of tool calls. It is compiled into an automaton that reads one byte at a time; at each state some bytes are allowed. To enforce it, the engine forbids at every step the tokens whose bytes the automaton would reject (the mask) and moves the automaton along the bytes of the chosen token. Three designs exist. Outlines [35] keeps a table of states × vocabulary per grammar. XGrammar [11] precomputes, per grammar position, a compressed cache of the tokens whose validity does not depend on the stack and checks the others against a stack on the CPU. llguidance [23] computes masks lazily on the CPU. Streams and batches. An answer being decoded, with its prompt, caches and automaton state, is a stream. Several streams decoded together form a batch; one step serves all of them per weight stream. In an agent system the streams are agents waiting for answers; the engine’s slots are the largest batch it will run. Where GPU memory goes. The weights; the prompt cache (recent prefills kept for reuse); the streams’ caches, which grow with every token; a transient used while a prompt is prefilled; and the constraints’ tables. On a 16 GB M2 Pro the GPU may wire 10.7 GB. What goes wrong as grammars and agents multiply (all measured in Appendices E–F): • Every grammar costs a table if masks are tabulated: 77 MB (104 states) to 1.5 GB (1,970 states); a typed tool grammar 824 MB and 1–2 minutes to build, kept for the life of the process. • A server dies as grammars accumulate: with tables, the fifteenth distinct grammar exhausts the wired limit on the 4B. • Host-side masks cost a step’s worth of time in an MLX decode loop: with masks only, llguidance decodes at 103 tokens/s against 137 free on the 2B, because each step must synchronize with the host (Section 5). • Throughput stalls with more agents in the stock library (87 tokens/s at 4 and at 8 streams on the 4B), and long answers do not fit (stock mlx-lm runs out of memory at six 16k-token streams). The first three are about the control side and are addressed by Sections 3–4; the last two are about the engine’s kernels and memory management (Appendices E–F). Appendix B The theory: formal statements and proofs This appendix first states every theoretical result formally, then proves it. Formal statements B.1 Walks, few paths, and the total language Definition 1 (Walks). Let G=(V,E)G=(V,E) be a finite directed graph with n vertices. A walk of length i from u to v is a sequence of edges whose endpoints concatenate, from u to v; vertices may repeat, and the empty walk (i=0i=0) is one walk from every vertex to itself. NG(u,v)∈ℕ∪∞N_G(u,v) ∪\∞\ is the number of walks from u to v, and NG≤L(u,v)N^≤ L_G(u,v) the number of those of length at most L. NG(u,v)N_G(u,v) is infinite exactly when a directed cycle is reachable from u and reaches v. Definition 2 (Few paths). For k≥1k≥ 1, G is k-strongly few if NG(u,v)≤kN_G(u,v)≤ k for every ordered pair of vertices, and k-reach-few from s if NG(s,v)≤kN_G(s,v)≤ k for every v. A 1-strongly-few graph is a mangrove [1]. Since the empty walk is counted, a k-strongly-few graph is acyclic. The language studied is STCONsf=⟨G,s,t,1k⟩:NG(u,v)≤kfor all u,v∈V,andNG(s,t)≥1, STCON_sf= \ G,s,t,1^k :N_G(u,v)≤ k\ for all u,v∈ V,\ and\ N_G(s,t)≥ 1 \, with G given by its adjacency matrix and k in unary; M is the input length, so n≤Mn≤ M and nk≤M2nk≤ M^2. More generally, with numerical budgets κ of polynomial total size, RootBudget asks for NH(r,q)≤κ(q)N_H(r,q)≤κ(q) for all q and NH(r,f)≥1N_H(r,f)≥ 1 for some f∈Ff∈ F, and PairBudget for NG(u,v)≤κ(u,v)N_G(u,v)≤κ(u,v) for all pairs and NG(s,t)≥1N_G(s,t)≥ 1. The totality obstacle. The bound on the number of walks is part of what must be decided, not a promise handed to the algorithm. A promise algorithm may enumerate paths because fewness guarantees there are few of them. A total algorithm receives an arbitrary graph, possibly with cycles or exponentially many walks, and must reject it within the same space, time and ambiguity bounds it uses on good inputs. Each classical tool fails on bad inputs in its own way: a depth-first traversal of a cyclic graph never ends, a fingerprint hash of exponentially many walks collides and miscounts, and an unambiguous machine that guesses a path through an ambiguous graph ceases to be unambiguous. Fig. 2 shows the two shapes that recur below: two walks between a pair, and a forced chain. B.2 Main results Theorem 2 (Main theorem). For unary k, STCONsf∈ReachUL=ReachFewL,STCONsf∈LOGDCFL∩C=L∩SC2, STCON_sf =ReachFewL, STCON_sf _=L ^2, STCONsf∈DSPACE(O(log2M/loglogM)). STCON_sf (O( ^2M/ M) ). STCONsf STCON_sf is StrongFewL-hard under deterministic logspace many-one reductions. What the theorem settles. Apers and Edenhofer [3] placed this language in quantum logspace and asked whether the classical bounds known for few-path computation, SC2 and the space bound O(log2M/loglogM)O( ^2M/ M), hold for the total language. Theorem 2 answers yes, and proves more: the total language is in ReachUL itself. A machine with at most one computation path to every configuration decides, on every input, whether the graph has few walks; it rejects cycles and exponentially many walks without ever becoming ambiguous. The result is a deterministic algorithm in space O(log2M/loglogM)O( ^2M/ M), below Savitch’s O(log2M)O( ^2M), for a reachability problem that certifies its own few-path condition, and a single deterministic algorithm with polynomial time and O(log2M)O( ^2M) space. Three constructions prove it (Table 14). Table 14: The classical placement of total few-path reachability. Every membership is proved on arbitrary inputs; the proofs are in Appendix B. Target Result Construction ReachUL == ReachFewL membership certified finite-field lift (Theorem 9) LOGDCFL membership capped deterministic auxiliary pushdown (Theorem 8) SC2 membership Cook’s simulation of the same pushdown DSPACE(log2MloglogM)( ^2M M) membership the ReachUL machine, simulated as in [1] C=L membership one GapL zero test of squared vanishing products (Theorem 10) NL membership collision-averaged fingerprints (Theorem 6) StrongFewL hardness; membership open configuration graphs (Theorem 7) The constructions are not specific to the uniform bound k. They validate any polynomially bounded system of walk budgets, and they compile any logspace computation whose ambiguity is bounded only semantically. Theorem 3 (Total budget validation). If the total numerical budget is polynomially bounded in the input length, then RootBudget,PairBudget∈ReachUL∩LOGDCFL∩C=L∩SC2. RootBudget,\ PairBudget\ ∈\ ReachUL _=L ^2. Theorem 2 is the special case κ(u,v)=kκ(u,v)=k. Theorem 4 (Fail-closed compiler). Let M0M_0 be a polynomial-time nondeterministic logspace machine, πx(c) _x(c) the number of its computation paths on input x from the initial configuration to configuration c, and κx(c)≥0 _x(c)≥ 0 logspace computable with a fixed polynomial bound on ∑cκx(c) _c _x(c). Then LM0,κ=x:πx(c)≤κx(c)for every c,and M0 accepts xL_M_0,κ=\x:\ _x(c)≤ _x(c)\ for every c,\ and M_0 accepts x\ is in ReachUL∩LOGDCFL∩C=L∩SC2ReachUL _=L ^2. In words: a nondeterministic logspace computation that is expected to have few computation paths, with no promise and no restriction on the machine, can be replaced by a reach-unambiguous one that checks the expectation on every input and rejects where it fails. Theorem 5 (Completeness). For every fixed k≥1k≥ 1, the rooted language RootFewk=⟨G,s,t⟩:NG(s,v)≤k∀v,NG(s,t)≥1 RootFew_k=\ G,s,t :N_G(s,v)≤ k\ ∀ v,\ N_G(s,t)≥ 1\ is ReachUL-complete under logspace reductions, and remains so on DAGs; rooted k-few recognition is ReachUL-complete; and the two-cone language FBFewk,1 FBFew_k,1, which bounds walks out of s by k and into t by 11, is ReachUL-complete. Theorem 6 (A phase transition in the threshold encoding). (i) With polynomially bounded thresholds, RootBudget,PairBudget∈NL RootBudget, PairBudget , and an FLNLFL^NL transducer outputs the capped counts minN≤B(r,v),K+1 \N^≤ B(r,v),K+1\. More generally, for every #L function f and polynomially bounded logspace threshold τ, x:f(x)≥τ(x)∈NL\x:f(x)≥τ(x)\ ; hence the class of such polynomial-threshold #L languages equals NL. (i) With the threshold K in binary, Bin-STCONsf Bin- STCON_sf is PL-complete, even on DAGs on which s reaches t by construction. (i) For a single pair and a fixed cap k, ⟨G,s,t⟩:G a DAG,NG(s,t)≤k\ G,s,t :G a DAG,\ N_G(s,t)≤ k\ is NL-complete. The complexity of validating few paths thus moves from inside ReachUL∩LOGDCFLReachUL to PL-complete exactly when the numerical threshold may become exponential, not when its notation changes (Table 15). Table 15: Validation tasks and their classification. Validation task Classification one pair, fixed cap NL-complete one rooted row, fixed k ReachUL-complete (also on DAGs) one rooted row or all pairs, polynomial total budget in ReachUL∩LOGDCFL∩C=L∩SC2ReachUL _=L ^2 all pairs, unary k (STCONsf STCON_sf) in ReachUL∩LOGDCFL∩C=L∩SC2ReachUL _=L ^2; StrongFewL-hard all pairs, binary threshold PL-complete Theorem 7 (The StrongFewL boundary). STCONsf STCON_sf is StrongFewL-hard. A proof that STCONsf∈StrongFewL STCON_sf would make it a natural complete problem for StrongFewL. The reach-unambiguous machine of Theorem 2 controls the paths from its initial configuration; StrongFewL asks for polynomially many paths between every pair of configurations, including pairs unreachable from the start. That extra invariant is exactly what membership in StrongFewL requires, and it is the precise open question left by this work (Appendix B.10). B.3 How the proofs go All three constructions bound a search by a budget, and one elementary lemma says why that is allowed. Lemma 1 (Budget truncation). Let H be a finite directed graph with a root r, give every vertex a budget κ(v)∈ℕκ(v) , and let B=∑vκ(v)B= _vκ(v). Then NH(r,v)≤κ(v)N_H(r,v)≤κ(v) for all v if and only if NH≤B(r,v)≤κ(v)N^≤ B_H(r,v)≤κ(v) for all v. Proof. Left to right is immediate. Conversely, suppose the bounded counts respect the budgets and some walk from r has length at least B. Its prefixes of lengths 0,…,B0,…,B are B+1B+1 distinct walks from r of length at most B; since the budgets sum to B, some vertex v ends more than κ(v)κ(v) of them, a contradiction. So every walk from r is shorter than B, and NH=NH≤BN_H=N^≤ B_H. ∎ Explore walks only up to the total budget: either you have seen every walk, or you have already found a violation. The depth B is tight (a directed cycle on B vertices with unit budgets). All-pairs budgets reduce to one root by a universal source with per-source copies: the graph U(G)U(G) has a root ρ, a vertex (a,v)(a,v) for every pair, an edge ρ→(a,a)ρ→(a,a) for every a, and an edge (a,u)→(a,v)(a,u)→(a,v) for every edge u→vu→ v and every tag a. Every walk from ρ to (a,v)(a,v) enters copy a and stays there, so NU(G)(ρ,(a,v))=NG(a,v)N_U(G)(ρ,(a,v))=N_G(a,v) for every pair, and the budget of (a,v)(a,v) can be set to κ(a,v)κ(a,v) (Lemma 2). Construction 1: a capped deterministic pushdown (LOGDCFL, SC2). Buntrock et al. [5] observed that a depth-first search of a reach-few machine, keeping a stack of return points, runs in LOGDCFL; on an arbitrary graph that search may never stop. Capping it by the total budget makes it total. Theorem 8 (Capped stack traversal). Run, from every source a, a depth-first traversal of the tree of walks from a that keeps a stack of return points (a vertex and the index of its next successor) and aborts as soon as more than nknk nodes have been entered; reject on any abort; then recount, for every pair (a,b)(a,b), the walks from a to b, rejecting when a count exceeds k; accept iff the (s,t)(s,t) count is positive. This decider accepts exactly STCONsf STCON_sf, and it is a deterministic auxiliary pushdown automaton with an O(logM)O( M) work tape running in polynomial time; hence STCONsf∈LOGDCFL⊆SC2 STCON_sf ^2 [31, 8]. Proof idea. In a k-strongly-few graph every source has at most nknk walks, so every traversal completes and, the graph being acyclic, its counts are exact. A source on a directed cycle has a walk of every length, so its traversal enters nk+1nk+1 nodes and aborts. The order of passes matters: recounts start only after every source has bounded its whole tree, so a bad input cannot force an exponentially long recount (Appendix B.11). ∎ Construction 2: a certified lift (ReachUL). The idea is to certify before counting. Hash every walk from the root by a polynomial fingerprint of its edge indices, evaluated at a point α of a prime field, into a layered graph HαH_α whose states record the endpoint, the length and the hash; walks correspond one-to-one to root paths of HαH_α. If HαH_α is reach-unambiguous, every walk reaches its own state and the number of reachable states in the fiber of v is exactly N≤B(r,v)N^≤ B(r,v), whether or not the input is valid. Reach-unambiguity of a rooted graph is decided by a total ReachUL recognizer [21], and ReachUL is closed under logspace oracle computations [13]. Theorem 9 (Certified lift). The controller that, for α=0,1,…α=0,1,…, certifies HαH_α and, for the first certified α, compares every fiber count with its budget, decides RootBudget by a reach-unambiguous logspace computation. With the universal source, PairBudget and STCONsf STCON_sf are in ReachUL. On a valid input a separating α exists, because at most (B−1)∑v(κ(v)2)<p(B-1) _v κ(v)2<p evaluation points cause a collision. On an invalid input either no lift is certified, or a certified lift exposes an over-budget fiber, by Lemma 1. Certification is followed by a budget comparison, not replaced by it: in a diamond, a separating lift exists whatever the budget at the merge vertex, and only the exact fiber count of two can reject a budget of one. Appendix B.7 gives the proof, and Appendix B.8 a second, self-contained certification that uses no oracle. Construction 3: one zero test (C=L). The bounded counts fuv=N≤nk(u,v)f_uv=N^≤ nk(u,v) are #L functions. The products ∏j=0k(fuv−j) _j=0^k(f_uv-j) vanish exactly when a count is within budget, and the designated pair uses ∏j=1k(fst−j) _j=1^k(f_st-j). The sum of their squares is a GapL function that is zero exactly on STCONsf STCON_sf. Theorem 10 (Signed counting). STCONsf∈C=L STCON_sf _=L, and PairBudget, RootBudget ∈C=L _=L for budgets of polynomial total size. C=L also contains ReachUL (ReachUL ⊆ UL ⊆ SPL ⊆ C=L), so the separate value of Theorem 10 is its certificate: one nonnegative integer whose vanishing enforces every budget at once, although C=L is not known to be closed under complement. B.4 The shape of few-path graphs Restrict a graph to the vertices and edges on some s–t path: the result is a trimmed two-terminal DAG H=(V,E,s,t)H=(V,E;s,t) with r=NH(s,t)r=N_H(s,t) paths and cyclomatic number c(H)=|E|−|V|+1c(H)=|E|-|V|+1. A branch vertex has out-degree at least two. The theorems below say what a few-path graph looks like; the decoding mechanisms of Section 4 read several of them off the graph of a decoding step. Theorem 11 (Branch kernel). c(H)+1≤r≤2c(H)c(H)+1≤ r≤ 2^c(H), and H has at most c(H)≤r−1c(H)≤ r-1 branch vertices. Suppressing every internal vertex with in- and out-degree one leaves a multigraph with the same r terminal paths, at most 2c(H)+2≤2r2c(H)+2≤ 2r vertices and at most 3c(H)+13c(H)+1 edges. Hence between any two vertices of a k-strongly-few graph, the vertices on paths between them form a subdivision of a multigraph with at most 2k2k vertices and 3k−23k-2 edges. Theorem 12 (Block product). Let B1,…,BqB_1,…,B_q be the biconnected blocks on the route from s to t in the block–cut tree of the underlying undirected graph of H, with entry and exit vertices ai,bia_i,b_i. Then r=∏iNBi(ai,bi)r= _iN_B_i(a_i,b_i) and c(H)=∑ic(Bi)c(H)= _ic(B_i); every ai,bia_i,b_i lies on every s–t path, and a path is an independent choice of one aia_i–bib_i path per block. If r≤kr≤ k, at most ⌊log2k⌋ _2k blocks have more than one path. Theorem 13 (Finite forbidden-subdivision basis). For every fixed k≥1k≥ 1 there is a finite family ℱkF_k of acyclic two-terminal multigraphs such that a finite directed graph is k-strongly few if and only if it has no directed cycle and contains no directed subdivision of a member of ℱkF_k. Every member has between k+1k+1 and 2k2k terminal paths, at most 2k2k vertices and at most 3k−13k-1 edges, and |ℱk|≤2O(klogk)|F_k|≤ 2^O(k k). Theorem 14 (Bounded fixed point and mangrove normal form). (i) G is k-strongly few iff the equation C=I+AC=I+AC has a solution C∈0,…,kn×nC∈\0,…,k\^n× n (A the adjacency matrix); the solution is then unique and equals the path-count matrix (I−A)−1(I-A)^-1. (i) The path-count matrix of every k-strongly-few graph, k≥2k≥ 2, factors over the nonnegative integers as C=M1M2⋯MrC=M_1M_2·s M_r with fewer than 4log2k4 _2k factors, each the path-count matrix of a mangrove, by a recursion of depth at most 1+⌊log2log2k⌋1+ _2 _2k . For path-convex mangrove decompositions this is optimal: a chain of r diamonds needs at least r+1r+1 blocks and depth at least ⌈log2(r+1)⌉ _2(r+1) . Theorem 15 (Density and width). A simple k-strongly-few graph on n vertices has at most min(n2),n2/4+3(k−1)n/4 \ n2,\ n^2/4+3(k-1)n/4\ edges, and for every fixed k≥2k≥ 2 the maximum is n2/4+Θk(n)n^2/4+ _k(n). Every reachability interval I(u,v)=x:u↝x↝vI(u,v)=\x:u x v\ has width at most NG(u,v)≤kN_G(u,v)≤ k and is the union of at most k directed u–v paths. Theorem 16 (Tractable regimes). Let λ(G)λ(G) be the smaller of the numbers of sources and of sinks, and b(G)b(G) the largest cyclomatic number of a biconnected block of the underlying undirected graph. Total strongly-few reachability is decidable in polynomial time and O((kλ(G)+1)logM)O((kλ(G)+1) M) space, and in 2O(b(G))MO(1)2^O(b(G))M^O(1) time and O(b(G)+logM)O(b(G)+ M) space. In particular it is in L for fixed k and a fixed number of sources or sinks, in SCdSC^d when kλ(G)=O(logd−1M)kλ(G)=O( ^d-1M), and in L when b(G)=O(logM)b(G)=O( M), as for chains of diamonds and oriented cacti. All proofs are in Appendix B.15. Read together, these results say that between two vertices of a few-path graph almost everything is forced, the rest factors into independent blocks, every violation contains one of finitely many small witnesses, and the whole path structure is a short product of mangroves. Proofs B.5 Machines, classes and the published interfaces A nondeterministic logspace machine M has a read-only input tape and a work tape of O(log|x|)O( |x|) cells. A configuration consists of the state, the input head position and the work tape with its head; GM(x)G_M(x) is the configuration graph on input x, with start configuration C0C_0. As usual we assume a clock, so that M halts on every path in polynomial time and GM(x)G_M(x) is acyclic, and a unique accepting configuration. A computation path halts by entering a configuration without successors; halted paths are not merged into a common rejecting configuration, so a failed guess ends where it is. • M is reach-unambiguous if on every input every configuration has at most one path from C0C_0. ReachUL is the class of languages accepted by such machines; ReachFewL allows polynomially many paths to every configuration, and ReachFewL == ReachUL [13]. • UL: at most one accepting path on every input. StrongFewL: for every input and every ordered pair of configurations, including pairs unreachable from C0C_0, at most polynomially many paths between them [5]. • LOGDCFL: the languages logspace-reducible to deterministic context-free languages; equivalently, those accepted by deterministic auxiliary pushdown automata with a logarithmic work tape in polynomial time [31]. SC2: one deterministic machine within polynomial time and O(log2|x|)O( ^2|x|) space simultaneously; LOGDCFL ⊆ SC2 [8]. • GapL: differences of two #L functions; closed under logspace-uniform polynomial sums and products. C=L: x:g(x)=0\x:g(x)=0\ for some g∈g∈ GapL. PL: x:g(x)>0\x:g(x)>0\. SPL: languages whose characteristic function is in GapL [2]. Two published facts about ReachUL are used. (a) The total language STCONru=⟨J,r,t⟩:NJ(r,x)≤1∀x,NJ(r,t)=1 STCON_ru=\ J,r,t :N_J(r,x)≤ 1\ ∀ x,\ N_J(r,t)=1\ is in ReachUL (and complete for it) [21]. (b) ReachUL is closed under complement and under deterministic logspace oracle computations with logspace-generated queries, LReachUL=ReachULL^ReachUL=ReachUL [13]. The composition behind (b) guesses each oracle answer and runs a reach-unambiguous recognizer for the oracle language or its complement; only the branch with the correct answer returns, every call carries its own tags (the answer, the saved controller configuration and a call index), and rejected branches keep their data rather than merge, so the composed machine reaches every configuration by at most one path. Appendix B.8 gives a second proof of the ReachUL membership that uses neither fact. B.6 The universal source and total root budgets Lemma 2 (Universal source with per-source copies). Let U(G)U(G) have vertices ρ∪(a,v):a,v∈V\ρ\∪\(a,v):a,v∈ V\, an edge ρ→(a,a)ρ→(a,a) for every a, and an edge (a,u)→(a,v)(a,u)→(a,v) for every edge u→vu→ v of G and every a. Then NU(G)(ρ,(a,v))=NG(a,v)N_U(G)(ρ,(a,v))=N_G(a,v) for all a,va,v. Proof. A walk from ρ to (a,v)(a,v) begins with the unique edge ρ→(a,a)ρ→(a,a) and then stays in copy a, whose first coordinate never changes. Deleting the first edge is a bijection onto the walks from a to v in G; the edge ρ→(a,a)ρ→(a,a) alone represents the empty walk at a. ∎ So PairBudget with budgets κ(u,v)κ(u,v) is RootBudget on U(G)U(G) with root ρ, budget 11 at ρ, budget κ(a,v)κ(a,v) at (a,v)(a,v) and target (s,t)(s,t); the total budget is 1+∑u,vκ(u,v)1+ _u,vκ(u,v), which is 1+n2k1+n^2k for STCONsf STCON_sf. (A universal source without copies would bound only the sums ∑aN(a,v) _aN(a,v); the copies are what preserve every pair.) Theorem 17 (Root budgets in LOGDCFL). If the states, transitions and budgets are logspace enumerable and the total budget B is polynomially bounded, RootBudget ∈ LOGDCFL. Proof. Reject if B=0B=0. Otherwise traverse the complete, untruncated walk-unfolding from r depth first, with the suspended frames (a state and the index of its next transition) on the pushdown, and reject on entering node B+1B+1. If the unfolding has more than B nodes, node B+1B+1 is reached after polynomially many entries, even along an infinite branch generated by a cycle. If the traversal completes, the whole unfolding is finite and has at most B nodes. Then rerun the traversal once per state q, counting nodes ending at q and rejecting at κ(q)+1κ(q)+1; these recounts are exact because the first pass exhausted the unfolding. Accept iff some accepting state is reached. Every traversal enters at most B+1B+1 nodes, the work tape holds a constant number of O(logM)O( M)-bit fields, and the procedure is a polynomial-time deterministic auxiliary pushdown automaton. Its invariant is: either the complete unfolding has at most B nodes, or node B+1B+1 is reached and the input is rejected. ∎ With Lemma 2, PairBudget ∈ LOGDCFL ⊆ SC2. Theorem 8 is the uniform special case, written per source. B.7 Proof of Theorem 9 (the certified lift) Fix a RootBudget instance (H,r,κ,F)(H,r,κ,F) with edge occurrences e1,…,eme_1,…,e_m and total budget B≥1B≥ 1 (reject B=0B=0 or κ(r)=0κ(r)=0 directly). Let S=∑v(κ(v)2)S= _v κ(v)2 and let p be the least prime with p>maxm,BS,2p> \m,BS,2\, found by trial division; p is polynomial and depends only on the supplied budgets, not on their validity. For α∈pα _p and a walk P=ei1⋯eidP=e_i_1·s e_i_d put hα(P)=i1αd−1+⋯+idmodph_α(P)=i_1α^d-1+·s+i_d p, computed by z↦αz+iz α z+i. Definition 3 (The lift). HαH_α has states (v,d,z)(v,d,z) with 0≤d≤B0≤ d≤ B and z∈pz _p, an edge (u,d,z)→(v,d+1,αz+imodp)(u,d,z)→(v,d+1,α z+i p) for every edge occurrence ei=(u,v)e_i=(u,v) and d<Bd<B, and root (r,0,0)(r,0,0). Lemma 3 (Separation). If all budgets hold, some α∈pα _p separates every two distinct walks of the same length and endpoint. Proof. For two distinct walks of the same length d≤Bd≤ B, the difference of their formal fingerprints is a polynomial of degree at most B−1B-1; it is nonzero because some edge-index coefficient differs and indices are below p. So each pair collides at most at B−1B-1 points. With the budgets holding, at most κ(v)κ(v) walks end at v, so there are at most S relevant pairs and at most (B−1)S<p(B-1)S<p bad points. ∎ Lemma 4 (Correspondence and exact fibers). Walks of length d≤Bd≤ B from r to v correspond bijectively to paths from (r,0,0)(r,0,0) to (v,d,hα(P))(v,d,h_α(P)). Whenever HαH_α is reach-unambiguous from its root, whether or not the budgets hold, NH≤B(r,v)=|(d,z):(r,0,0)↝(v,d,z) in Hα|.N^≤ B_H(r,v)= |\(d,z):(r,0,0) (v,d,z) in H_α\ |. Proof. Along a lifted path the residue is forced by the recurrence, so every walk lifts to exactly one path, and projection inverts lifting. Two distinct walks reaching the same lifted state would give two root paths to it, contradicting reach-unambiguity. ∎ Proof of Theorem 9. The controller enumerates α∈pα _p. For each α it queries STCONru(Hα,(r,0,0),(r,0,0)) STCON_ru(H_α,(r,0,0),(r,0,0)), which holds exactly when HαH_α is reach-unambiguous from its root (the only path from the root to itself is the empty one). For the first certified α, it scans every endpoint fiber, querying reachability of each lifted state (an ordinary reachability query once the lift is certified) and keeping a counter saturated at κ(v)+1κ(v)+1; it rejects if a count exceeds its budget, and otherwise accepts iff some fiber of a vertex in F is nonempty. If no α is certified, it rejects. Correctness. On a valid input, Lemma 3 gives a certified α, every fiber count equals N≤B(r,v)≤κ(v)N^≤ B(r,v)≤κ(v) (Lemma 4), and the reachability condition is read off correctly. On an invalid input, either no lift is certified and the controller rejects, or a certified lift gives exact bounded counts (Lemma 4), and by Lemma 1 some bounded count exceeds its budget, or the reachability condition fails. (The diamond r→a→vr→ a→ v, r→b→vr→ b→ v shows why the budget comparison is needed: separating lifts exist whatever the budget at v, and only the exact fiber count two rejects a budget of one.) Resources. Each lift has |Q|(B+1)p|Q|(B+1)p states and a logspace adjacency predicate; the controller stores α, an endpoint, a layer, a residue and a saturated counter, and makes polynomially many queries. It is a deterministic logspace oracle machine with oracle STCONru∈ STCON_ru∈ ReachUL, so by fact (b) the language is in ReachUL. With Lemma 2, PairBudget and STCONsf STCON_sf are in ReachUL. ∎ B.8 A second, oracle-free proof of the ReachUL membership The certification of the lift can also be done directly, by a reach-unambiguous machine that never guesses through a layer it has not certified. We give this proof for STCONsf STCON_sf, hashing vertex sequences rather than edge indices. Let the input be ⟨G,s,t,1k⟩ G,s,t,1^k with V=0,…,n−1V=\0,…,n-1\. Set L=nkL=nk and let p be the least prime with p>max(n,L(nk)2)p> (n,\,L(nk)^2); by Bertrand’s postulate p<2max(n,L(nk)2)p<2 (n,L(nk)^2), and p is found in logspace by trial division. All numbers below have O(logM)O( M) bits. For a walk ω=(v0,…,vi)ω=(v_0,…,v_i) write Hα(ω)=∑j=0ivjαi−jmodpH_α(ω)= _j=0^iv_jα^i-j p for α∈pα _p, computed by Horner’s rule h0=v0h_0=v_0, hj=αhj−1+vjh_j=α h_j-1+v_j. Write Ni(a,v)N_i(a,v) for the number of walks of length exactly i from a to v. Definition 4 (Hashed unfolding). For a∈Va∈ V and α∈pα _p, Γa,α _a,α is the graph on states (v,i,h)∈V×0,…,L×p(v,i,h)∈ V×\0,…,L\×F_p with an edge (u,i,h)→(v,i+1,αh+v)(u,i,h)→(v,i+1,α h+v) for every (u,v)∈E(u,v)∈ E and i<Li<L, and root ra=(a,0,a)r_a=(a,0,a). Layer i is the set of states with second coordinate i. Γa,α _a,α is certified through layer d if every state of layers 0,…,d0,…,d has at most one path from rar_a. The adjacency of Γa,α _a,α is computable in logspace from the input, a and α. Lemma 5 (Walks are root paths). The map ω↦((v0,0,h0),…,(vi,i,hi))ω ((v_0,0,h_0),…,(v_i,i,h_i) ) is a bijection from the walks of length i≤Li≤ L starting at a onto the paths of length i starting at rar_a; the image of ω ends at (vi,i,Hα(ω))(v_i,i,H_α(ω)). Hence the number of paths from rar_a to (v,i,h)(v,i,h) equals the number of walks of length i from a to v with Hα(ω)=hH_α(ω)=h. Proof. Edges of Γa,α _a,α project to edges of G, and along a path from rar_a the third coordinate is determined by the first coordinates through Horner’s rule; conversely every walk lifts to exactly one path. ∎ Lemma 6. Γa,α _a,α is certified through layer d if and only if HαH_α is injective on the walks of length i from a to v, for all i≤di≤ d and v∈Vv∈ V. In that case Ni(a,v)=|h:(v,i,h) is reachable from ra|N_i(a,v)=|\h:(v,i,h) is reachable from r_a\| for every i≤di≤ d and v. Proof. Immediate from Lemma 5. ∎ Lemma 7 (A good evaluation point exists). If ∑vN≤L(a,v)≤nk _vN^≤ L(a,v)≤ nk, then fewer than p values of α fail to certify Γa,α _a,α through layer L; in particular some α∈pα _p certifies it. Proof. Let ω≠ω′ω≠ω be walks of the same length i≤Li≤ L from a to the same v. Their coefficient sequences are their vertex sequences, which differ and have entries below n<pn<p, so Pω(X)−Pω′(X)P_ω(X)-P_ω (X), with Pω(X)=∑jvjXi−jP_ω(X)= _jv_jX^i-j, is a nonzero polynomial over pF_p of degree at most L and vanishes at most at L points. There are at most (∑i,vNi(a,v))2≤(nk)2( _i,vN_i(a,v))^2≤(nk)^2 such pairs, so at most L(nk)2<pL(nk)^2<p values of α make some pair collide. By Lemma 6 every other value certifies Γa,α _a,α through layer L. ∎ Algorithm 1 Tour(a,α,d) Tour(a,α,d): Euler tour of the reachable states of layers ≤d≤ d of Γa,α _a,α, assumed certified through layer d, calling Visit once per state. 1: x←rax← r_a; Visit(x)(x); ←mode← down 2: loop 3: if =mode= down then 4: if layer(x)<dlayer(x)<d and x has an out-neighbour then 5: x←x← the first out-neighbour of x; Visit(x)(x); continue 6: else ←mode← up 7: end if 8: end if 9: if x=rax=r_a then return 10: end if 11: u←Parent(x)u← Parent(x) ⊳ nondeterministic, below 12: if u has an out-neighbour after x then 13: x←x← that out-neighbour; Visit(x)(x); ←mode← down 14: else x←ux← u ⊳ mode stays up 15: end if 16: end loop 17: 18: Parent(x)(x), for x at layer j≥1j≥ 1: guess a state u of layer j−1j-1 with an edge u→xu→ x; guess z0=ra,z1,…,zj−1z_0=r_a,z_1,…,z_j-1, each zm+1z_m+1 an out-neighbour of zmz_m, storing only zmz_m and m; if zj−1=uz_j-1=u return u, otherwise halt (this computation path dies). Lemma 8 (Traversal of a certified prefix). Suppose Γ=Γa,α = _a,α is certified through layer d, and let T be the set of states of layers ≤d≤ d reachable from rar_a. Then (i) T with the edges of Γ inside it is an out-tree rooted at rar_a, in which the children of every x∈Tx∈ T of layer <d<d are exactly its out-neighbours in Γ ; (i) Algorithm 1, started in a configuration reached by a unique path, visits every state of T exactly once, has exactly one computation path that returns, reaches every configuration on its way by exactly one path from its start, and uses O(logM)O( M) work space in addition to that of Visit. Proof. (i) Every x∈Tx∈ T has exactly one path from rar_a; its predecessor on that path is its only in-neighbour in T, because an in-neighbour u∈Tu∈ T would give the path ra↝u→xr_a u→ x. Every out-neighbour y of x∈Tx∈ T with layer(x)<dlayer(x)<d is reachable, hence in T, and its unique path passes through x. (i) By (i) the tour is the deterministic Euler tour of a tree, so it visits every state of T once, provided Parent returns the parent. In Parent(x)(x) the guessed states zmz_m follow edges from rar_a, so each zmz_m lies in T at layer m≤d−1m≤ d-1 and its guessed prefix z0,…,zmz_0,…,z_m is the unique path to it. The guess succeeds iff u is reachable at layer j−1j-1 and the guessed path is its path; by (i) the only reachable in-neighbour of x is its parent. So exactly one computation path of Parent succeeds, and it returns the parent. The configurations of the procedure are tour configurations (x,,pending child)(x,mode,pending child) and recovery configurations (x,,u,zm,m)(x,mode,u,z_m,m). The tour configurations occur in a fixed order without repetition, since in an Euler tour each state is entered once and left upward once, and each is reached through the unique successful paths of the preceding recoveries. A recovery configuration arises only from the one tour configuration that invokes Parent(x)(x), by one choice of u and by the guesses z1,…,zmz_1,…,z_m, which zmz_m determines; hence it too has exactly one path. The work tape holds x, u, zmz_m, m and the mode, O(log(nLp))=O(logM)O( (nLp))=O( M) bits. ∎ Lemma 9 (Certifying layer by layer). The procedure Certify(a,α) Certify(a,α), which for d=0,1,…,L−1d=0,1,…,L-1 and every state y of layer d+1d+1 runs Tour(a,α,d) Tour(a,α,d) counting (up to 2) the visited states x of layer d with x→yx→ y, and fails as soon as a count reaches 2, returns ok iff Γa,α _a,α is certified through layer L. It runs Tour only with a d through which Γa,α _a,α is certified, has exactly one returning computation path, and reaches every configuration by exactly one path from its start. Proof. Layer 00 is ra\r_a\, so Γa,α _a,α is certified through layer 00. If it is certified through layer d, every reachable state of layer d has exactly one path, so the number of paths to a state y of layer d+1d+1 equals the number of its reachable in-neighbours, which the tour counts. All counts are at most one iff the graph is certified through layer d+1d+1. Tour is therefore only invoked under its hypothesis. The loop variables d, y and the count are part of every configuration of an invocation, so by Lemma 8 invocations neither share configurations nor create a second path to any. ∎ Algorithm 2 The ReachUL decider for STCONsf STCON_sf. 1: compute n, L=nkL=nk and the prime p; R←R← false 2: for a=0,…,n−1a=0,…,n-1 do 3: ←ok← false 4: for α=0,…,p−1α=0,…,p-1 do 5: if Certify(a,α)=ok Certify(a,α)= ok then 6: for v=0,…,n−1v=0,…,n-1 do 7: C←C← number of states visited by Tour(a,α,L) Tour(a,α,L) whose vertex is v, counted up to k+1k+1 8: if C>kC>k then reject 9: end if 10: if a=sa=s, v=tv=t and C≥1C≥ 1 then R←R← true 11: end if 12: end for 13: ←ok← true; break 14: end if 15: end for 16: if not ok then reject 17: end if 18: end for 19: if R then accept else reject Oracle-free proof that STCONsf∈ReachUL STCON_sf . Consider Algorithm 2. Correctness. When an α certifies Γa,α _a,α through layer L, the count computed for v is ∑i≤LNi(a,v)=N≤L(a,v) _i≤ LN_i(a,v)=N^≤ L(a,v) (capped at k+1k+1), by Lemma 6. Suppose the input is in STCONsf STCON_sf. For every a, N(a,v)≤kN(a,v)≤ k for all v, so ∑vN≤L(a,v)≤nk _vN^≤ L(a,v)≤ nk and Lemma 7 provides a certifying α; the counts are at most k, no rejection occurs, and R becomes true because N≤L(s,t)≥1N^≤ L(s,t)≥ 1. Conversely, suppose the algorithm accepts. Then for every a some α certified, and N≤L(a,v)≤kN^≤ L(a,v)≤ k for all v; by Lemma 1 with κ≡kκ≡ k and B=nk=LB=nk=L, N(a,v)≤kN(a,v)≤ k for all v. So G is k-strongly few, and N(s,t)≥N≤L(s,t)≥1N(s,t)≥ N^≤ L(s,t)≥ 1. (A rejection because no α certifies is correct by the contrapositive of Lemma 7; a rejection because a count exceeds k is correct because N≥N≤LN≥ N^≤ L.) Reach-unambiguity. The outer control is deterministic, and every nondeterministic step happens inside Parent, within invocations of Tour on certified prefixes (Lemma 9 for Certify; for the counting tours, Certify has just returned ok). Each invocation has exactly one returning computation path and reaches every configuration by exactly one path (Lemma 8); the outer variables (a,α,v,C,R,)(a,α,v,C,R,ok) advance strictly between invocations and are part of every configuration. Hence on every input every configuration is reached by at most one path, and exactly one computation path reaches the end. Resources. The work tape holds a constant number of O(logM)O( M)-bit numbers. The number of tours is polynomial, each visits at most n(L+1)pn(L+1)p states, and each parent recovery takes O(L)O(L) steps, so the surviving path runs in polynomial time. ∎ The procedure Certify is itself a reach-unambiguous decider for the reach-unambiguity of a layered graph through a given layer, which is what makes this proof self-contained. B.9 Proof of Theorem 10 (signed counting) For x=⟨G,s,t,1k⟩x= G,s,t,1^k let fuv(x)=NG≤nk(u,v)f_uv(x)=N^≤ nk_G(u,v). A nondeterministic logspace machine that chooses a length at most nknk and then exactly that many edge-occurrence codes, accepting iff the resulting walk goes from u to v, has one accepting computation per walk, so fuv∈#Lf_uv∈\#L. For (u,v)≠(s,t)(u,v)≠(s,t) put Puv=∏j=0k(fuv−j)P_uv= _j=0^k(f_uv-j), and Pst=∏j=1k(fst−j)P_st= _j=1^k(f_st-j); thus Puv=0P_uv=0 iff 0≤fuv≤k0≤ f_uv≤ k and Pst=0P_st=0 iff 1≤fst≤k1≤ f_st≤ k. Let g=Pst2+∑(u,v)≠(s,t)Puv2g=P_st^2+ _(u,v)≠(s,t)P_uv^2. Logspace-uniform polynomial products and sums preserve GapL, so g∈g∈ GapL. Every term is an integer square, so g(x)=0g(x)=0 exactly when all truncated counts satisfy the bound and the designated count is positive, and by Lemma 1 (with the per-source budgets of Lemma 2) exactly when x∈STCONsfx∈ STCON_sf. Malformed inputs and k=0k=0 get a constant nonzero gap. For pair budgets, use fuv=N≤L(u,v)f_uv=N^≤ L(u,v) with L=max∑vuκ(u,v)L= _u _vκ(u,v) and products up to κ(u,v)κ(u,v); for root budgets, Pv=∏j=0κ(v)(fv−j)P_v= _j=0^κ(v)(f_v-j) and PF=∏j=1B(fF−j)P_F= _j=1^B(f_F-j) with fF=∑v∈Ffvf_F= _v∈ Ff_v. The sum of squares is what makes one zero test enforce every equality at once, although C=L is not known to be closed under complement. B.10 Proof of Theorem 2, Theorem 3 and the StrongFewL boundary Memberships. ReachUL: Theorem 9. LOGDCFL: Theorem 8 (and Theorem 17 for budgets). SC2: Cook’s simultaneous simulation of the same polynomial-time deterministic auxiliary pushdown automaton [8], a single algorithm with both bounds. C=L: Theorem 10. DSPACE(O(log2M/loglogM))(O( ^2M/ M)): ReachUL =RUSPACE(logn)⊆DSPACE(log2n/loglogn)=RUSPACE( n) ( ^2n/ n) [1]; this is a pure space bound with no time claim. NL: Theorem 6(i). Also STCONsf∈ STCON_sf∈ UL ∩ coUL, since ReachUL is closed under complement. Hardness. Let A be accepted by a StrongFewL machine with at most q(|x|)q(|x|) paths between any two configurations, with a unique accepting configuration. Its configuration graph GxG_x is logspace computable, acyclic (a cycle would give infinitely many paths) and q(|x|)q(|x|)-strongly few, possibly after adding a clock or an accepting collector, which multiplies the bound by a fixed polynomial factor; parallel transitions are replaced by private two-edge paths. Hence x∈Ax∈ A iff ⟨Gx,C0,Cacc,1q′(|x|)⟩∈STCONsf G_x,C_0,C_acc,1^q (|x|) ∈ STCON_sf. Why membership in StrongFewL is open. The reach-unambiguous machines above control the paths from their initial configuration; configurations unreachable from it may still be joined by many paths, and the unique-return oracle composition gives no all-pairs bound inside the composed machine. A proof of STCONsf∈ STCON_sf∈ StrongFewL needs a total validator whose entire configuration graph has polynomially many paths between arbitrary configurations; with the hardness above it would make STCONsf STCON_sf StrongFewL-complete. B.11 Proof of Theorem 8 (the capped stack traversal) Algorithm 3 Capped traversal from a source a with a budget of nknk nodes. In target mode for b it also counts the entered nodes that end at b and aborts at k+1k+1. 1: current←acurrent← a; next←1next← 1; depth←0depth← 0; total←1total← 1; countb←[a=b]count_b←[a=b] 2: loop 3: if depth=nkdepth=nk or next>nnext>n then 4: if stack empty then return (ok, totaltotal, countbcount_b) 5: end if 6: pop (v,j)(v,j); current←vcurrent← v; next←jnext← j; depth←depth−1depth -1; continue 7: end if 8: w←nextw ; next←next+1next +1 9: if (current,w)∉E(current,w)∉ E then continue 10: end if 11: push (current,next)(current,next); current←wcurrent← w; next←1next← 1; depth←depth+1depth +1; total←total+1total +1 12: if total=nk+1total=nk+1 then return overflow 13: end if 14: if target mode and current=bcurrent=b then 15: countb←countb+1count_b _b+1; if countb=k+1count_b=k+1 return overflow 16: end if 17: end loop For a source a and length ℓ , the walk-unfolding tree TaℓT _a has one node per walk of length at most ℓ from a; distinct walks are distinct nodes even when they end at the same vertex, so |Taℓ|=∑bN≤ℓ(a,b)|T _a|= _bN^≤ (a,b). Algorithm 3 is a depth-first traversal of TankT^nk_a whose stack holds, for each node on the current branch, its vertex and the index of its next successor. Lemma 10. (i) If |Tank|>nk|T^nk_a|>nk then G is not k-strongly few. (i) If G is k-strongly few then |Tank|≤nk|T^nk_a|≤ nk for every a. (i) If G has a directed cycle, a source on it has |Tank|≥nk+1|T^nk_a|≥ nk+1. (iv) If G is acyclic, N≤nk(a,b)=N(a,b)N^≤ nk(a,b)=N(a,b). Proof. (i) More than nknk nodes among n endpoints put at least k+1k+1 distinct walks on some endpoint. (i) is (i) contrapositive, summed over endpoints. (i) Following the cycle gives a walk of every length 0,…,nk0,…,nk. (iv) In an acyclic graph every walk is a simple path of length at most n−1≤nkn-1≤ nk. ∎ Proof of Theorem 8. If the input is in STCONsf STCON_sf, every global traversal completes by Lemma 10(i), every recount is exact by (iv) and at most k, and the (s,t)(s,t) count is positive. Conversely, if the decider accepts, no source overflowed, so G is acyclic by (i); all recounts are then exact and at most k, so G is k-strongly few, and N(s,t)≥1N(s,t)≥ 1. The recounts start only after every global traversal has bounded its tree by nknk nodes, so an invalid input cannot force an exponentially long recount. Resources: the work tape holds a constant number of O(logM)O( M)-bit counters; a stack frame (v,j)(v,j) has 2⌈log2(n+2)⌉2 _2(n+2) bits; a traversal enters at most nk+1nk+1 nodes and tests at most n successors per node, so with an O(M)O(M) input scan per adjacency test it takes O(n2kM+nklogM)O(n^2kM+nk M) steps, and there are n+n2n+n^2 traversals. The decider is therefore a deterministic auxiliary pushdown automaton with logarithmic work tape running in polynomial time, and such machines accept exactly LOGDCFL [31]. ∎ Without the budget, this depth-first search is the one Buntrock et al. [5] use for reach-few machines, whose configuration graphs are promised to have few paths; the budget and the order of the passes are what make it total. B.12 Proof of Theorem 5 (completeness) Membership of all three languages follows from Theorem 3 (for FBFew, apply the root-budget theorem to s in G and to t in the reversed graph, since NGrev(t,v)=NG(v,t)N_G^rev(t,v)=N_G(v,t)). RootFewk RootFew_k. For k=1k=1 the language is STCONru STCON_ru, which is ReachUL-complete [21]. For k>1k>1, add a new root r and k internally disjoint two-edge paths r→ai→sr→ a_i→ s; then NH(r,v)=kNG(s,v)N_H(r,v)=k\,N_G(s,v) for every old vertex, so a bound of one becomes a bound of k and reachability is preserved. DAGs. Given a rooted threshold-one instance on n vertices, build layers 0,…,2n−10,…,2n-1 reproducing every edge between consecutive layers, and add for every vertex v a fresh sink cvc_v with an edge from every layered copy of v; use (s,0)(s,0) as root and ctc_t as target. On a reach-unambiguous input every layered state and every sink has at most one rooted path. If the reachable part is acyclic but ambiguous, two simple rooted paths of length at most n−1n-1 reach one sink; if a cycle is reachable, a simple prefix to a cycle vertex and the same prefix followed by one tour give two walks of length at most 2n−12n-1 to one sink. The k-fold prefix gadget then gives DAG hardness for every fixed k. Recognition and two cones. Rooted reach-unambiguity recognition is ReachUL-complete [10], and the k-fold prefix reduces it to rooted k-few recognition. For FBFewk,1 FBFew_k,1, given ⟨G,s⟩ G,s add fresh vertices r,zr,z and the edges r→sr→ s, r→zr→ z, and use r as source and z as target: NH(r,v)=NG(s,v)N_H(r,v)=N_G(s,v) for old vertices, every backward count into z is at most one, and r↝zr z holds, so ⟨G,s⟩ G,s is rooted k-few iff ⟨H,r,z⟩∈FBFewk,1 H,r,z ∈ FBFew_k,1. B.13 Proof of Theorem 4 (the fail-closed compiler) Generate the clocked configuration graph of M0M_0 on x in logspace, take the initial configuration as root and the accepting configurations as F, and attach the budgets κx _x. The graph has polynomial size, a computation path is exactly a rooted path, and the clock makes the graph finite even on rejected inputs. Theorems 17, 9 and 10 apply. The compiler validates a bound on computation prefixes from the initial configuration; it does not produce a machine with few paths between arbitrary configurations, which is the StrongFewL question above. B.14 Proof of Theorem 6 (the threshold phase transition) (i) Polynomial thresholds: collision-averaged fingerprints. Fix a root, budgets of total mass B and maximum K≥1K≥ 1, edge occurrences e1,…,eme_1,…,e_m, q0=(B−1)(K+12)+1q_0=(B-1) K+12+1, a prime p>maxm,q0p> \m,q_0\ and a set A⊆pA _p of q0q_0 points. For a walk P of length d≤Bd≤ B let ϕα(P)=(d,hα(P)) _α(P)=(d,h_α(P)). For an endpoint v let WvW_v be the rooted walks of length at most B ending at v, cv=|Wv|c_v=|W_v|, and Dv=∑α∈A|ϕα(Wv)|D_v= _α∈ A| _α(W_v)|, the total number of distinct images. Lemma 11 (Collision-averaged decoding). For every v and t≤Kt≤ K: cv≤tc_v≤ t iff Dv≤q0tD_v≤ q_0t. Hence mincv,K+1=min⌈Dv/q0⌉,K+1 \c_v,K+1\= \ D_v/q_0 ,K+1\. Proof. If cv≤tc_v≤ t, each point yields at most cvc_v images, so Dv≤q0tD_v≤ q_0t. Conversely let cv≥t+1c_v≥ t+1 and pick t+1t+1 distinct walks. Walks of different lengths never collide; two of the same length collide at at most B−1B-1 points. At a fixed α with collision classes of sizes sjs_j, the number of lost images is ∑j(sj−1)≤∑j(sj2) _j(s_j-1)≤ _j s_j2, the number of colliding pairs. Summing over A, the selected walks have at least q0(t+1)−(B−1)(t+12)>q0tq_0(t+1)-(B-1) t+12>q_0t images, and the full family has at least as many. ∎ Taking the disjoint union of the lifts HαH_α, α∈Aα∈ A, under a super-root, DvD_v is the number of reachable states in the fiber of v. A logspace machine with an NL oracle counts them, and LNL=NLL^NL=NL because NL == coNL [18, 32]. So RootBudget ∈ NL, the capped counts are in FLNLFL^NL, and with Lemma 2 PairBudget ∈ NL. Applied to the accepting computations of an NL machine (with their length stored), the same decoding shows x:f(x)≥τ(x)∈\x:f(x)≥τ(x)\∈ NL for f∈#f∈\#L and a polynomially bounded logspace threshold τ; conversely every L∈L∈ NL is x:f(x)≥1\x:f(x)≥ 1\ for its accepting-path count. (i) Binary thresholds are PL-complete. Membership: reject cyclic graphs (NL ⊆ PL); on a DAG each NG(u,v)N_G(u,v) is a #L function, and a logspace machine has exactly K+1K+1 accepting branches by guessing a number in [0,K][0,K] bit by bit against K, so (K+1)−NG(u,v)∈(K+1)-N_G(u,v)∈ GapL and NG(u,v)≤KN_G(u,v)≤ K is a PL predicate. PL is closed under complement, union, intersection and NC1 reductions [6], so the conjunction over all pairs and the reachability test stays in PL. Hardness: take a probabilistic logspace machine with exactly p binary choices that accepts on A(x)A(x) of its 2p2^p paths, x∈L⇔A(x)>2p−1x∈ L A(x)>2^p-1. Between common endpoints a,ba,b put a chain of p+1p+1 diamonds (C=2p+1C=2^p+1 paths) in parallel with the layered configuration graph (A(x)A(x) paths) and set K=C+2p−1K=C+2^p-1. Every pair other than (a,b)(a,b) has at most C paths, N(a,b)=C+A(x)N(a,b)=C+A(x), and a reaches b on every input, so the instance is accepted iff A(x)≤2p−1A(x)≤ 2^p-1; this reduces the complement of L, and PL is closed under complement. (i) One pair, fixed cap. Reject non-DAGs with the NL cycle test and NL == coNL. On a DAG the complement guesses k+1k+1 paths in parallel, storing their current vertices and pairwise-difference flags, O(logn)O( n) space for fixed k, so the language is in coNL == NL. Hardness: reduce DAG non-reachability by adding a new source with k+1k+1 internally disjoint prefixes into the old source; the new count is 00 if the target was unreachable and at least k+1k+1 otherwise. B.15 Proofs of the structure theorems Proof of Theorem 11. Lower bound. The unit s–t flows of H form a polytope; flow conservation at the |V|−2|V|-2 internal vertices together with the unit-value constraint has rank |V|−1|V|-1, so the polytope has dimension |E|−|V|+1=c(H)|E|-|V|+1=c(H). Its vertices are the indicator vectors of the s–t paths (the constraint matrix is totally unimodular), and a c-dimensional polytope has at least c+1c+1 vertices. Upper bound. Fix a path P0P_0. The map P↦χP⊕χP0P _P _P_0 sends paths to even subgraphs, elements of the cycle space over GF(2), which has dimension c(H)c(H); the map is injective. Kernel. In a trimmed H every vertex x≠tx≠ t has out-degree at least one, and summing over all x≠tx≠ t, the source included, gives ∑x≠t(d+(x)−1)=|E|−(|V|−1)=c(H) _x≠ t(d^+(x)-1)=|E|-(|V|-1)=c(H). So at most c(H)c(H) vertices have out-degree at least two, and likewise for in-degree. Every vertex that survives the contraction is a terminal or one of these, and contracting a vertex of in- and out-degree one merges two edges and preserves the paths and c. This gives at most 2c+2≤2r2c+2≤ 2r vertices and, since c is preserved, at most c+(2c+2)−1=3c+1c+(2c+2)-1=3c+1 edges. ∎ Proof of Theorem 12. A simple s–t path follows the unique route of blocks in the block–cut tree. It cannot enter an off-route block and return, since it would repeat the cut vertex through which it entered. Inside route block BiB_i it traverses one aia_i–bib_i path, and arbitrary choices concatenate into distinct s–t paths. The cyclomatic numbers add because the blocks share only cut vertices. If r≤kr≤ k, each block with more than one path contributes a factor of at least two. ∎ Proof of Theorem 13. Minimal obstructions. Let H=(V,E,s,t)H=(V,E;s,t) be acyclic, trimmed, edge-minimal subject to NH(s,t)>kN_H(s,t)>k, with its mandatory initial and final chains contracted, so d+(s)≥2d^+(s)≥ 2 and d−(t)≥2d^-(t)≥ 2; write r=NH(s,t)r=N_H(s,t) and c=c(H)c=c(H). For an out-edge e of s, let rer_e be the number of terminal paths through e. Deleting e leaves at most k paths, so re≥r−kr_e≥ r-k; the classes of the at least two out-edges partition the paths, so r≥2(r−k)r≥ 2(r-k), i.e. r≤2kr≤ 2k. For c: in the unit-flow polytope (dimension c), the face xe=0\x_e=0\ of an irredundant inequality is a facet of dimension c−1c-1 whose vertices are the paths avoiding e, at most k by minimality; a (c−1)(c-1)-dimensional polytope has at least c vertices, so c≤kc≤ k. The source has out-degree at least two and the sink in-degree at least two, and the excess-degree identities of Theorem 11 give at most c vertices of each kind, so after suppressing unary vertices the core has at most 2c≤2k2c≤ 2k vertices and (2c−1)+c≤3k−1(2c-1)+c≤ 3k-1 edges. The basis. If G is acyclic and violates the bound at some pair, restrict to the vertices and edges on paths of that pair, take an edge-minimal violating subgraph, contract its mandatory terminal chains and suppress unary vertices: the result is a core as above, and the subgraph of G is a directed subdivision of it. Conversely, subdividing edges preserves the number of terminal paths, so a subdivision of a core with more than k paths is a violation. Directed cycles are excluded separately. Only finitely many multigraphs have at most 2k2k vertices and 3k−13k-1 edges, which gives the counting bound. ∎ Proof of Theorem 14. (i) If G is k-strongly few it is acyclic, An=0A^n=0, and C=I+A+⋯+An−1=(I−A)−1C=I+A+…+A^n-1=(I-A)^-1 solves C=I+AC=I+AC with entries the path counts. Conversely let C≥0C≥ 0 solve it and put =Cr=C1; then =+Ar=1+Ar, so ru=1+∑u→wrw>rvr_u=1+ _u→ wr_w>r_v for every edge u→vu→ v, and a directed cycle would give a strict chain returning to its start. So G is acyclic, I−AI-A is invertible, and C=(I−A)−1C=(I-A)^-1 is the path-count matrix with entries at most k. (i) For 1≤τ<k1≤τ<k let μ(v)=maxaN(a,v)μ(v)= _aN(a,v), Lτ=v:μ(v)≤τL_τ=\v:μ(v)≤τ\ and HτH_τ the rest. Since μ(v)≥μ(u)N(u,v)μ(v)≥μ(u)N(u,v) along reachability, no path goes from HτH_τ to LτL_τ, both parts are path-convex, G[Lτ]G[L_τ] is τ-strongly few and G[Hτ]G[H_τ] is ⌊k/(τ+1)⌋ k/(τ+1) -strongly few. With τ=⌊k⌋τ= k both parts are ⌊k⌋ k -strongly few. Ordering L before H, the path-count matrix factors as C=(CL00I)(IB0I)(I00CH)C= pmatrixC_L&0\\ 0&I pmatrix pmatrixI&B\\ 0&I pmatrix pmatrixI&0\\ 0&C_H pmatrix, where the middle factor counts the identity paths and single bridge edges, a mangrove. Recursing on both blocks, the number of mangrove leaves ℓ(k) (k) satisfies ℓ(1)=1 (1)=1 and ℓ(k)≤2ℓ(⌊k⌋) (k)≤ 2 ( k ), so ℓ(k)≤2log2k (k)≤ 2 _2k, and with one bridge factor per internal node the number of factors is 2ℓ−1<4log2k2 -1<4 _2k; repeated square roots reach one in at most 1+⌊log2log2k⌋1+ _2 _2k levels. Optimality. In a chain of r diamonds with merge vertices z0,…,zrz_0,…,z_r, two consecutive merge vertices cannot share a path-convex mangrove block (it would contain both branches of a diamond), and two non-consecutive ones would force all intermediate merge vertices into the block; so the ziz_i lie in r+1r+1 distinct blocks, and a binary recursive decomposition has depth at least ⌈log2(r+1)⌉ _2(r+1) . With k=2rk=2^r the bounds O(logk)O( k) and O(loglogk)O( k) are therefore tight. ∎ Proof of Theorem 15. Density. Since G is acyclic every triangle of the underlying graph is transitively oriented x→y→zx→ y→ z, x→zx→ z; assign it to its long edge. An edge with rer_e triangles has 1+re1+r_e paths between its endpoints, so re≤k−1r_e≤ k-1 and the number of triangles is T≤(k−1)mT≤(k-1)m. Summing |N(x)∩N(y)|≥dx+dy−n|N(x)∩ N(y)|≥ d_x+d_y-n over edges gives 3T≥∑xdx2−mn≥4m2/n−mn3T≥ _xd_x^2-mn≥ 4m^2/n-mn by Cauchy–Schwarz, so 3(k−1)m≥4m2/n−mn3(k-1)m≥ 4m^2/n-mn, which rearranges to the bound. For the lower bound, take |B|=k−1|B|=k-1, split the remaining n−k+1n-k+1 vertices evenly into A and C, and add all edges A→BA→ B, B→CB→ C, A→CA→ C: each pair (a,c)(a,c) has exactly k paths and every other pair at most one, giving ⌊(n−k+1)2/4⌋+(k−1)(n−k+1) (n-k+1)^2/4 +(k-1)(n-k+1) edges. Width. Let X be an antichain in I(u,v)I(u,v). For each x∈Xx∈ X concatenate a path u↝xu x and a path x↝vx v; two elements of X on the same u–v path would be comparable, so |X|≤N(u,v)|X|≤ N(u,v). Every vertex and edge of the interval extends to a u–v path, so the at most k such paths cover it. ∎ B.16 Proof of Theorem 16 (tractable regimes) Terminal width. For a root a of a DAG, the walk-unfolding tree TaT_a has La=1+∑v:d+(v)>0N(a,v)(d+(v)−1)L_a=1+ _v:d^+(v)>0N(a,v)(d^+(v)-1) leaves (a rooted tree has one more leaf than the sum of its excess out-degrees), and every leaf ends at a sink, so La≤kτ+(G)L_a≤ kτ^+(G) on a valid input, τ+τ^+ being the number of sinks. A depth-first traversal that stores a frame only at nodes with at least two children keeps at most La−1L_a-1 frames, since a tree with L leaves has at most L−1L-1 branching nodes. The decider counts sources and sinks (rejecting a nonempty graph with neither), chooses the orientation with fewer sinks (reversing edges transposes the path-count matrix and swaps sources and sinks), and runs the source-global and recount passes of Theorem 8 with choice frames only, keeping the node cap nk+1nk+1, a length cap n (a walk of length n certifies a cycle) and a stack cap kλ(G)−1kλ(G)-1. On a valid input no cap triggers and the recounts are exact; on an invalid input any cap may reject, and if none does, the absence of a length-n walk proves acyclicity and acceptance is sound. Each frame has O(logM)O( M) bits, giving O((kλ(G)+1)logM)O((kλ(G)+1) M) space in polynomial time, hence L for fixed k and λ, and SCd when kλ(G)=O(logd−1M)kλ(G)=O( ^d-1M). Block-cyclomatic width. In a connected component with cyclomatic number c, enumerate the 2c2^c vectors of the cycle space relative to a spanning tree, generating each selected edge set on demand; requiring in/out-degrees (0,1)(0,1) at s, (1,0)(1,0) at t, (0,0)(0,0) or (1,1)(1,1) elsewhere and undirected connectivity of the selection characterizes the directed simple s–t paths, one vector each, and directed cycles are detected the same way, in 2O(c)MO(1)2^O(c)M^O(1) time and O(c+logM)O(c+ M) space. Every simple cycle lies in one biconnected block, so cycles are detected blockwise. On a DAG, for each pair follow the unique route of blocks in the block–cut tree (navigated by undirected connectivity tests after deleting a candidate articulation vertex, using Reingold’s algorithm [27]), count the paths between the entry and exit vertices of each route block by cycle-space enumeration with at most b bits, and multiply with a counter saturated at k+1k+1 (Theorem 12). This gives 2O(b)MO(1)2^O(b)M^O(1) time and O(b+logM)O(b+ M) space; a chain of diamonds has unbounded global cycle rank but block-cyclomatic width one. Appendix C The decoding mechanisms: formal statements and proofs This appendix first states the decoding results formally, then proves them. Formal statements C.1 Cost model, constraints and the step graph Cost. Let τ(S)τ(S) be the latency of one forward pass that appends S tokens to a cached prefix and returns logits at every new position. On a laptop, single-stream decoding is bound by memory bandwidth: a pass reads all weights (1.1 GB for Qwen3.5-2B, 2.26 GB for the 4B at 4 bits), and the arithmetic for a few tokens is nearly free. On an M2 Pro, τ(4)=1.36τ(1)τ(4)=1.36\,τ(1), τ(8)=1.58τ(1)τ(8)=1.58\,τ(1) and τ(16)=2.04τ(1)τ(16)=2.04\,τ(1) on the 2B (Fig. 10 in Appendix E). Hence the cost of decoding is its number of passes. A model maps a token prefix u to logits ℓ(u) (u); by causality, one pass over v1⋯vSv_1·s v_S after u yields the same cache and logits as S single-token passes, up to floating-point reassociation. Constraints. Let Σ be the byte alphabet. Definition 5 (Control machine). A control machine is =(C,δ,c0,F)A=(C,δ,c_0,F) with configurations C, a partial step δ:C×Σ⇀Cδ:C× C, start c0c_0 and accepting set F. δ∗δ^* extends δ to strings, L()=x:δ∗(c0,x)∈FL(A)=\x:δ^*(c_0,x)∈ F\, and live(c)=b:δ(c,b) definedlive(c)=\b:δ(c,b) defined\. A is trim if an accepting configuration is reachable from every configuration reachable from c0c_0. A DFA is the case of a finite C=QC=Q; a deterministic pushdown is the case C=Q×R∗C=Q× R^* (Section C.6). The vocabulary is a set ⊂Σ+V⊂ ^+ of byte strings plus a token eos. Constrained decoding at configuration c samples from the model’s logits restricted to A(c)=t∈:δ∗(c,t) defined∪eos:c∈FA(c)=\t :δ^*(c,t) defined\∪\ eos:c∈ F\ (the mask), then moves to δ∗(c,t)δ^*(c,t); if A is trim, every emitted prefix extends to a string of L()L(A). The vocabulary trie T_V is the tree of all token prefixes (0.59M nodes for the 248k-token Qwen3.5 vocabulary). Definition 6 (Step graph). For c∈Cc∈ C, PcP_c has vertices (w,δ∗(c,w))(w,δ^*(c,w)) for the trie nodes w at which δ∗(c,w)δ^*(c,w) is defined, edges (w,c′)→(wb,δ(c′,b))(w,c )→(wb,δ(c ,b)), and root (ε,c)( ,c). Proposition 1. For every deterministic control machine and every c, PcP_c is an out-tree; hence a mangrove. The disjoint union of PcP_c over any set of configurations is a forest, and each token t∈A(c)∖eost∈ A(c) \ eos\ corresponds to exactly one vertex of PcP_c, which carries δ∗(c,t)δ^*(c,t). Proof. Every edge lengthens w; a vertex (wb,c′)(wb,c ) has the single parent (w,δ∗(c,w))(w,δ^*(c,w)), because the trie fixes w and determinism fixes the configuration. ∎ The proposition is elementary. Its use is that every fact about a decoding step can be computed along a tree, once per vertex, without merging information from two parents. Neither a nondeterministic automaton nor the lattice of all tokenizations of a string has this property (Fig. 3). C.2 The token table, with and without storing it Theorem 18 (Two ways to evaluate the step graph). Let A be a DFA with states Q, and T[t,q]=δ∗(q,t)∈Q∪⊥T[t,q]=δ^*(q,t)∈ Q∪\ \. (i) One pass. Walking the trie level by level with all |Q||Q| states as the columns of one array computes T in depth(T)depth(T_V) gathers with total work at most |T|⋅|Q||T_V|·|Q|, within a factor |T|/|||T_V|/|V| (2.4 for Qwen3.5) of the ||⋅|Q||V|·|Q| entries any algorithm must write, and never more than evaluating every token from every state separately. (i) No table. For any state q, the row T[⋅,q]T[·,q] is computed by |||V| independent walks from q, one per token, with ∑t|t| _t|t| lookups in total and depth maxt|t| _t|t|, using only the automaton (256|Q|256|Q| entries) and the packed token bytes. Proof idea. (i) Row w at depth d holds the vertices of Pqq\P_q\_q above trie node w; by Proposition 1 each has one parent, in the row of w’s parent, so one gather computes a level. (i) The walk of token t from q is the root-to-t path of PqP_q, which depends on nothing else (Appendix C.8). ∎ What the engine does. Either way, the mask is a row and the transition is an entry, so both stay on the GPU: the mask at q is [T[⋅,q]≠⊥][T[·,q]≠ ] and the next state is T[y,q]T[y,q], indexed by device values. The host never enters the decode step, so a constrained step pipelines like a free one. With (i) the table costs 3|Q|||3|Q||V| bytes, 77 MB for a 104-state schema and 1.5 GB for 1,970 states, and is built in 0.2–0.6 s for the schemas we use. With (i) a Metal kernel runs one thread per token each step (7–18 μ against a 7–15 ms step) and the grammar costs its automaton, 512 bytes per state, plus 2.9 MB of packed vocabulary shared by all grammars. We call (i) the walk kernel. It trades a stored table for recomputation along the single path of each token, the same trade the certified lift makes when it counts reachable states instead of storing walks. C.3 Forced output costs no pass Definition 7 (Forced configurations and chains). A configuration c is forced if c∉Fc∉ F and |live(c)|=1|live(c)|=1, and a decision point otherwise. chain(c)chain(c) is the byte string read by following the unique live byte from c while the configuration is forced. Forcing is a property of the automaton, not of the step graph: it says that only one byte may follow, whatever tokens exist. If A is trim, chain(c)chain(c) is finite and ends at a decision point; otherwise every run from c would follow it forever and never accept. Definition 8 (Segmentation policy; reference and forced-span decoders). A segmentation policy φ assigns to each configuration c a token string φ(c)∈∗ (c) ^* whose bytes are a prefix of chain(c)chain(c), and to each sampling configuration a nonempty set Aφ(c)⊆A(c)A_ (c) A(c) of admissible tokens; both depend on A and the tokenizer only, never on the model. Both decoders below feed φ(c0) (c_0) with the prompt and sample first at c1=δ∗(c0,φ(c0))c_1=δ^*(c_0, (c_0)). At a sampling configuration c, the reference decoder RφR_ samples t from the logits restricted to Aφ(c)A_ (c), sets c′=δ∗(c,t)c =δ^*(c,t), feeds the tokens of φ(c′) (c ) one pass each, and continues at δ∗(c′,φ(c′))δ^*(c , (c )). The forced-span decoder FφF_ is identical except that t and φ(c′) (c ) are fed in one pass. Theorem 19 (Pass optimality). Let A be trim and φ a segmentation policy. (i) Exactness. For every causal model, sampling rule and seed, FφF_ and RφR_ emit the same tokens and, in exact arithmetic, see the same logits at every sampling point. (i) Cost. On an output with N sampled tokens, FφF_ makes N passes and RφR_ one pass per emitted token. (i) Lower bound. If |Aφ(c)|≥2|A_ (c)|≥ 2 at every sampling configuration, every non-speculative decoder (one that feeds the model only tokens it has already emitted) whose output distribution equals RφR_ ’s for every model under greedy or softmax sampling makes at least N passes on every output with N sampled tokens. Corollary 1 (Length independence). Let φ commit the whole chain. Let c,c†c,c be configurations such that every accepting run from c passes through c†c , the runs from c to c†c form a trimmed two-terminal DAG H with r paths, and no configuration of H other than c†c accepts. Then FφF_ samples at most c(H)≤r−1c(H)≤ r-1 tokens that start in H before c†c . A key or any other string the constraint determines costs no pass, and a field with r admissible values costs at most r−1r-1 passes, however long they are. Proof. Every sampled token starts at a decision point; a decision point of H other than c†c has two live bytes, each on an accepting run through c†c since A is trim, so it is a branch vertex of H. Distinct sampled tokens start at distinct vertices, and Theorem 11 bounds the branch vertices by c(H)≤r−1c(H)≤ r-1. ∎ The DAG hypothesis matters: an automaton with free-text fields has cycles and is not few-path, and Theorem 11 applies only to its acyclic parts between two cut configurations (keys, enum values, booleans, closing brackets). What the engine does. After each sampled token, the engine looks up the chain of the new configuration, splits it into tokens (Section C.4) and feeds the sampled token and the forced tokens in one pass of m+1m+1 positions. Once the model has written the closing quote of "name":"Maria", the schema allows only ,"age":, seven bytes and two tokens, fed with the quote. On our six JSON schemas about 30% of output tokens are forced (Fig. 4). Speculative decoding [22, 7] goes below N passes only by verification; forced spans are drafts accepted with probability one. C.4 Splitting forced text the way the tokenizer would A byte-level BPE tokenizer is a pre-tokenizer π, which cuts a string into blocks (words, numbers, punctuation runs), followed by a per-block encoder: tok(s)=bpe(s1)⋯bpe(sm)tok(s)=bpe(s_1)·sbpe(s_m) for π(s)=(s1,…,sm)π(s)=(s_1,…,s_m). Models are trained on tok(s)tok(s). Two things can go wrong with forced bytes. A non-canonical split puts the model in a context it has not seen. And committing the canonical split of forced bytes w too early can contradict the canonical split of wxwx once the next bytes x arrive, because x may merge into the last block of w. Among the segmentations the tokenizer can produce, block boundaries are cut vertices, so only the last block is at risk (Theorem 12); in the lattice of all tokenizations they are not, since a token such as "M may cross a boundary. The question is exactly when the last block is safe. Assumption 1 (Locality of the pre-tokenizer). For a string s let m(s)m(s) be the start of the last block of π(s)π(s) or of the maximal trailing whitespace run of s, whichever is smaller. For every s and character a, every block of π(s)π(s) that ends at or before m(s)m(s) is a block of π(sa)π(sa). Regex pre-tokenizers look ahead one character at whitespace ( +(?! )), which is why the whitespace clause is needed. We tested Assumption 1 on the Qwen3.5 pre-tokenizer with 720,000 random (string, character) pairs and 400,000 multi-character extensions over JSON punctuation, letters, digits, whitespace, contractions and non-ASCII characters, and found no violation. Theorem 20 (Canonical commitment). Let π satisfy Assumption 1 and let o be the output so far, in configuration c. (i) For every string x, every block of π(o)π(o) that ends at or before m(o)m(o) is a block of π(ox)π(ox); their canonical tokens can be committed now. (i) If o does not end in whitespace and π(o)π(o) is a prefix of π(ob)π(ob) for every b∈live(c)b (c), then π(o)π(o) is a prefix of π(ox)π(ox) for every x with δ∗(c,x)δ^*(c,x) defined, so tok(o)tok(o) is a prefix of tok(ox)tok(ox). Part (i) says what may always be committed; part (i) is a test on single bytes that certifies the last block, and it quantifies only over the bytes the constraint allows. What the engine does (the canonical policy): after a sampled token and its chain, commit the blocks licensed by Theorem 20 and hold back the rest; if the held-back block is one vocabulary token of length ℓ , the next sampled token must span at least ℓ bytes (boundary cover), so the model chooses how the block continues in one token, as the tokenizer would. The policy only chooses which tokens ride in the next pass, so by Theorem 19 it costs nothing. C.5 Valid outputs under a token budget Every deployed decoder has a token limit, and a constrained output that reaches it is cut mid-value. Fix a policy φ (without healing) and count every emitted token, sampled or forced, against a budget R; an output that exhausts the budget ends there and is valid iff it ends in F. For a sampling configuration c define need(c)=0c∈F,mint∈Aφ(c)∖eoscost(c,t)otherwise,cost(c,t)=1+|φ(c′)|+need(c′),need(c)= cases0&c∈ F,\\ _t∈ A_ (c) \ eos\cost(c,t)&otherwise, cases (c,t)=1+| (c )|+need(c ), with c′=δ∗(c,t)c =δ^*(c,t) and c′=δ∗(c′,φ(c′))c =δ^*(c , (c )). With r tokens left, the budget mask is Mr(c)=t∈Aφ(c):cost(c,t)≤r∪eos:c∈FM_r(c)=\t∈ A_ (c):cost(c,t)≤ r\∪\ eos:c∈ F\. Theorem 21 (Least restrictive valid mask). Let A be a trim DFA. (i) needneed is a shortest-path distance, computed by Bellman–Ford in at most |Q||Q| vectorized rounds. (i) If need(c1)≤Rneed(c_1)≤ R, where R is the budget left at the first sampling configuration c1c_1, every output decoded under MrM_r, by any model and sampling rule, is in L()L(A), whether it ends by eos or by the budget. (i) t∈Mr(c)t∈ M_r(c) iff some continuation after t reaches F within the remaining budget; any mask that admits a token outside Mr(c)M_r(c) admits a model whose output is invalid. The mask is inactive until the last maxc,tcost(c,t) _c,tcost(c,t) tokens (17–38 on our schemas), so outputs with room are unchanged; if need(c1)>Rneed(c_1)>R, no valid output fits, which the decoder can report before it starts. C.6 Recursion: a deterministic pushdown with a capped stack A schema that refers to itself, such as a tree of nodes with children, has no regular expression. Definitions on a cycle of the schema’s reference graph become nonterminals; each is a DFA over bytes and call symbols; a call edge q→calljrq call_jr pushes the return state r and continues at the callee’s start, and a callee that accepts with no successor pops and continues at r; a callee that accepts with successors pops lazily, when the next byte is not its own. Two L(1) conditions, checked at compile time, make at most one move applicable, so the machine is deterministic; grammars that violate them are refused. Call a pop real if it removes a symbol that was on the stack before the token began, and exposed if another move of the token’s run follows it. Theorem 22 (Stack locality). For a token t and a state q, the run of t from (q,σ)(q,σ) depends on σ only through the symbols revealed by its exposed real pops: there is a decision tree of depth e≤|t|e≤|t|, branching only on those symbols, whose leaves give the final state (or “continue at the popped state”), the number of real pops and the pushed string. If e=0e=0, one table entry serves every stack. What the engine does. The token table splits into a context-free table ×QV× Q and a small context table indexed by the top e stack symbols, both computed by the level pass of Theorem 18(i) with rows that carry a symbolic stack. On Qwen3.5’s vocabulary and our recursive schemas only 7–12 tokens at 4–11 states are context-dependent, and e≤2e≤ 2 suffices except for the token , which is masked; tokens that would push more than three symbols are masked as well. Masking such tokens removes no byte string from the language, because every single byte is a token. The stack is a 64-entry array on the GPU, and masking and advancing are gathers on (state, top two stack symbols). The depth cap changes the language: the engine enforces L()∩nesting depth≤64L(A)∩\nesting depth≤ 64\, and a configuration left with no admissible token stops with an explicit error rather than emit an invalid one. Forced chains cross calls and returns: after a node’s last value, ],"name":" is one span. The proof of Theorem 22 and the sound byte-level budget for pushdowns are in Appendix C.12. C.7 Independent parts in parallel, certified Lemma 12 (Concatenation at cut states). Let A be a trim DFA and c1,…,cmc_1,…,c_m states such that every accepting run from c0c_0 visits c1,…,cmc_1,…,c_m in this order, each exactly once. Then every w∈L()w∈ L(A) factors uniquely as w=x0x1⋯xmw=x_0x_1·s x_m with δ∗(ci,xi)=ci+1δ^*(c_i,x_i)=c_i+1 (and cm+1∈Fc_m+1∈ F), and every such concatenation is in L()L(A). For an object schema whose keys are all required, every key is a forced chain, so the state after each key is a cut state, and the language is a product of one value language per field: the automaton analogue of Theorem 12. The model’s distribution over the values is not a product. The decoder therefore uses the factorization only to draft, and certifies the draft. Theorem 23 (Certified block decoding). Fix a policy φ and greedy decoding. Draft each field independently, from the configuration at which the sequential decoder would begin it; assemble the draft D and replay it through A with φ , obtaining the configuration qiq_i before every sampled position i; compute the logits at every position of D in one pass; and accept position i iff DiD_i is the masked argmax at qiq_i. Then, in exact arithmetic, the longest accepted prefix of D, extended by the argmax at the first rejected position, is a prefix of the sequential greedy output. Repeating from that prefix produces exactly the sequential output, and each round adds at least one sampled token. The theorem is an instance of speculative verification [22, 7], with drafts that the grammar’s factorization makes independent. Two caveats are stated with it. In floating point, the certification pass computes logits over many positions at once, in fp16 and with chunked recurrent kernels, so a near-tie could flip; all 36 measured outputs were token-identical. And a round costs the longest draft plus one certification pass, so in the worst case, one new token per round, it is slower than sequential decoding. A cap on rounds followed by sequential decoding bounds this; our implementation stops at 24 rounds, a cap never approached (at most 3 rounds on the 2B and 4 on the 4B). Algorithms and the related finite-region decision are in Appendix D. Table 16: What each mechanism rests on. Every mechanism is a construction of Section 3 applied to the step graph of a decoding step. Mechanism Result Guarantee one-pass token table Thm. 18(i), Lemma 2 exact table in depth(T)depth(T_V) gathers, work within 2.4×2.4× of the output size walk kernel Thm. 18(i), Thm. 9 the table’s row recomputed each step; memory = automaton + shared vocabulary forced spans Thm. 19, Cor. 1 same outputs, minimum passes among non-speculative decoders canonical policy Thm. 20 + Assumption 1 committed tokens are the tokenizer’s split under every continuation budget mask Thm. 21 valid under every feasible limit; least restrictive such mask pushdown constraint Thm. 22; the machine of Thm. 8 exact up to nesting depth 64; table indexed by top two stack symbols certified blocks Lemma 12, Thm. 23 greedy output in exact arithmetic (36/36 identical in fp16) Proofs C.8 Theorem 18: the one-pass table and the walk Algorithm 4 All-state token table: all |Q||Q| states side by side, one trie level per step. For each trie node at depth d, parentdparent_d gives its parent and bytedbyte_d its last byte; tokdtok_d lists the tokens ending at depth d. 1: S0←[ 0,1,…,|Q|−1]S_0←[\,0,1,…,|Q|-1\,] ⊳ one row, the root; every state is a root 2: for d=1,2,…,depth(T)d=1,2,…,depth(T_V) do 3: rows ← nodes w at depth d whose parent row survived at depth d−1d-1 4: Sd[w,⋅]←δ[Sd−1[parentd(w),⋅],byted(w)]S_d[w,·]←δ [S_d-1[parent_d(w),·],\ byte_d(w) ] for all rows ⊳ one gather; ⊥ stays ⊥ 5: T[t,⋅]←Sd[node(t),⋅]T[t,·]← S_d[node(t),·] for every t∈tokdt _d 6: drop the rows with Sd[w,⋅]≡⊥S_d[w,·]≡ 7: end for Proof of Theorem 18. (i) By induction on d, row w of SdS_d holds (δ∗(q,w))q∈Q(δ^*(q,w))_q∈ Q: for d=0d=0 it is the identity, and for d>0d>0, δ∗(q,w)=δ(δ∗(q,parent(w)),byte(w))δ^*(q,w)=δ(δ^*(q,parent(w)),byte(w)) with ⊥ absorbing. A row that is ⊥ for every state has only ⊥ descendants, so dropping it loses no token. Each level processes at most |Td||T_V^d| rows of |Q||Q| entries, so the work is at most |T|⋅|Q||T_V|·|Q|. The output has ||⋅|Q||V|·|Q| entries; mapping every non-root trie node w to a pair (t,|w|)(t,|w|) with w a prefix of t is injective, so |T|−1≤∑t|t||T_V|-1≤ _t|t|, the cost of walking every token separately. (i) The walk of t from q reads the bytes of t through δ; it is the root-to-t path of PqP_q (Proposition 1) and uses no other token’s walk. ∎ On Qwen3.5’s vocabulary and the 104-state person schema, the pass performs 61M lookups in 0.3 s and touches the trie essentially once, because a schema with free-text fields keeps almost every trie node alive for some state (Fig. 9). 1122446688101012121414161618182020025k50k75k100ktrie depth (bytes)rows at this leveltrie nodes at this depthrows still alive in the pass Figure 9: The all-state pass, level by level (person schema, 104 states). Gray: trie nodes of the 248k-token vocabulary by byte depth. Blue: rows Algorithm 4 keeps alive at that level (a row dies only when it is dead for all states). Depths beyond 20 hold under 1% of the nodes. C.9 Theorem 19: pass optimality Proof. (i) Both decoders begin at the same sampling configuration with identical caches. Suppose this holds at the k-th sampling point. Both evaluate the same logits and, with the same randomness, draw the same t. RφR_ then feeds t and φ(c′) (c ) in 1+|φ(c′)|1+| (c )| passes and FφF_ in one; by causality the resulting caches and last-position logits coincide, and the next sampling configuration δ∗(c′,φ(c′))δ^*(c , (c )) is the same because φ does not depend on the model. (i) is counting. (i) Fix a model p and an output y of positive probability, and let i1<⋯<iNi_1<…<i_N be the positions at which RφR_ samples on y. Step 1: D evaluates ℓ(y<ik) (y_<i_k) before it emits yiky_i_k. Otherwise, with positive probability, D emits yiky_i_k after y<iky_<i_k without that evaluation. Let p′p agree with p on every prefix except y<iky_<i_k, where it changes the probability of yiky_i_k among the at least two admissible tokens (under softmax sampling any change of the relative logits does this; under greedy decoding, make another admissible token the argmax). On that event D behaves identically under p and p′p , while RφR_ ’s conditional distribution differs, contradicting exactness for both models. Step 2: the evaluations happen in distinct passes. Let Πk _k be the pass that yields ℓ(y<ik) (y_<i_k). D emits yiky_i_k only after Πk _k completes and, being non-speculative, feeds it only in a later pass; Πk+1 _k+1 computes logits at a prefix that contains yiky_i_k, so it is or follows a pass that feeds yiky_i_k. Hence Πk+1 _k+1 starts after Πk _k completes, and Π1,…,ΠN _1,…, _N are distinct. ∎ C.10 Theorem 20: canonical commitment Proof. For a string s let e(s)e(s) be the largest block boundary of π(s)π(s) that is at most m(s)m(s); the blocks of π(s)π(s) ending at or before m(s)m(s) are exactly those that tile [0,e(s))[0,e(s)). Claim: these blocks are blocks of π(sa)π(sa), and e(sa)≥e(s)e(sa)≥ e(s). The first part is Assumption 1. For the second, e(s)e(s) is a boundary of π(sa)π(sa); the last block of π(sa)π(sa) contains position |s||s|, so it is not one of the preserved blocks and starts at or after e(s)e(s); the trailing whitespace run of sasa starts at |s|+1|s|+1 if a is not whitespace, and otherwise at |s||s| or at the start of the trailing run of s, which is at least m(s)≥e(s)m(s)≥ e(s). Hence m(sa)≥e(s)m(sa)≥ e(s) and e(s)e(s) is a boundary at most m(sa)m(sa). (i) follows by induction on |x||x|, since e never decreases and the blocks tiling [0,e(o))[0,e(o)) are preserved at every step; as toktok encodes blocks independently, their canonical tokens are a prefix of tok(ox)tok(ox). (i) Let x=bx′x=bx with b∈live(c)b (c) (every x with δ∗(c,x)δ^*(c,x) defined and x≠εx≠ starts with such a byte). By hypothesis π(o)π(o) is a prefix of π(ob)π(ob), so the last block of π(ob)π(ob) is [|o|,|o|+1)[|o|,|o|+1); since o does not end in whitespace, m(ob)=|o|m(ob)=|o|, every block of π(o)π(o) ends at or before m(ob)m(ob), and (i) applied to obob and x′x concludes. ∎ We identify a byte with the characters it can begin; the implementation tests every ASCII byte and one representative per class of non-ASCII lead bytes. For o not ending in whitespace, “π(ob)π(ob) has a boundary at |o||o|” was equivalent to “π(o)π(o) is a prefix of π(ob)π(ob)” in all 1.44M tested pairs, and the implementation tests the former. The whitespace clause of Assumption 1 is necessary: appending to a string ending in ␣ merges its last two blocks. C.11 Theorem 21: the least restrictive valid mask Proof. (i) The definition of needneed is the Bellman equation of a shortest-path problem with positive integer weights 1+|φ(c′)|1+| (c )| on the token-step graph of the |Q||Q| sampling configurations; its least solution is the distance to F, reached within |Q||Q| rounds, each a gather over the transition table and a row-wise minimum. (i) Invariant: need(c)≤rneed(c)≤ r at every sampling point. It holds at c1c_1. If c∈Fc∈ F and r=0r=0, the output ends validly. If c∉Fc∉ F, some t has cost(c,t)=need(c)≤rcost(c,t)=need(c)≤ r, so Mr(c)≠∅M_r(c)≠ ; for any admitted t the forced span fits, because 1+|φ(c′)|≤cost(c,t)≤r1+| (c )| (c,t)≤ r, and at the next sampling point c′c , r′=r−1−|φ(c′)|≥cost(c,t)−1−|φ(c′)|=need(c′)r =r-1-| (c )| (c,t)-1-| (c )|=need(c ). If r reaches 00 at a sampling point, the invariant gives need(c)=0need(c)=0, i.e. c∈Fc∈ F; an output that ends by eos ends in F by definition of A(c)A(c). (i) If cost(c,t)≤rcost(c,t)≤ r, following minimizing tokens realizes a continuation of weight cost(c,t)cost(c,t) that reaches F; conversely every continuation after t that reaches F has weight at least cost(c,t)cost(c,t). If a mask admits t with cost(c,t)>rcost(c,t)>r, a model that greedily prefers t at c leaves no continuation reaching F within the budget, and the output is cut outside F. ∎ C.12 Theorem 22 and budgets for pushdowns The machine. Definitions on a cycle of the schema’s reference graph (strongly connected components) become nonterminals N1,…,NCN_1,…,N_C; every other reference is inlined. Each NjN_j is a DFA over Σ∪call1,…,callC ∪\call_1,…,call_C\; a call edge q→calljrq call_jr records its return state r, and R is the set of return states. A configuration is (q,σ)(q,σ) with σ∈R∗σ∈ R^*. On byte b the machine (1) moves if δ(q,b)δ(q,b) is defined; else (2) if q has a call edge to NjN_j with b∈first(Nj)b (N_j), pushes r and moves to δ(startj,b)δ(start_j,b); else (3) if q accepts and σ=σ′rσ=σ r, pops and retries b at r (a lazy return); and (4) after a move, while the state accepts and has no successor, pops and continues at the popped state (an eager return; with an empty stack this is the end of the output). The compiler checks first(Nj)∩live(q)=∅first(N_j) (q)= at every call site and live(q)∩follow(Nj)=∅live(q) (N_j)= at every accepting state of a called NjN_j that has successors (an L(1) condition), refuses grammars that violate them, and requires return states not to accept, so that the end of output depends only on the state and an empty stack. Proof of Theorem 22. Simulate the run of t from q with the initial stack unknown, tracking the symbols that t itself pushes. Every move reads the state and, for a return, the top symbol. While the top symbol was pushed by t, it is known. A pop that reaches below these symbols is real. If no further move follows it, its symbol enters the result only as “continue at the popped state”. If another move follows, the run branches on the popped symbol’s value, through the return state reached and its moves. Each exposed real pop consumes one symbol of the original stack and is followed by at least one byte or pop of t, so the branching depth is at most |t||t|. The leaves record the final state, the number of real pops and the pushed string. ∎ Proposition 2 (Sound budgets for pushdowns). Let bn(q)bn(q) be the length of the shortest byte string that completes the current nonterminal from q: the least fixpoint of bn(q)=0bn(q)=0 for accepting q and otherwise min1+bn(δ(q,b)),bn(startj)+bn(r) \1+bn(δ(q,b)),\ bn(start_j)+bn(r)\ over bytes and call edges q→calljrq call_jr. Then need+(q,σ)=bn(q)+∑r∈σbn(r)need^+(q,σ)=bn(q)+ _r∈σbn(r) is the length of the shortest byte completion of (q,σ)(q,σ). If every single byte is a token, admitting a token only if 1+need+(c′)≤r1+need^+(c )≤ r for the configuration c′c after it guarantees validity in the sense of Theorem 21(i). Proof. Every completion of (q,σ)(q,σ) decomposes into a string taking q to an accepting state of its nonterminal, the return to the top of σ, a completion of that return state’s nonterminal, and so on; the L(1) conditions make the pops occur exactly at these points. Each part has length at least bnbn of its state, and concatenating shortest parts is a valid completion, so need+need^+ is the exact shortest byte completion. Every token and every forced span covers at least one byte, and forced bytes lie on every completion. A token admitted by 1+need+(c′)≤r1+need^+(c )≤ r therefore leaves r−1−f≥need+(c′)−f′=need+(c′)r-1-f ^+(c )-f =need^+(c ), where f forced tokens cover f′≥f ≥ f bytes; the single-byte token that begins a shortest completion is always admitted; the invariant need+≤rneed^+≤ r follows as in Theorem 21(i). ∎ The bound is sound but not least restrictive, because a token may cover several bytes. The device state vector carries the running sum ∑r∈σbn(r) _r∈σbn(r), so the mask reads one extra column. C.13 Lemma 12 and Theorem 23: certified blocks Proof of Lemma 12. The run of w∈L()w∈ L(A) is unique and visits c1,…,cmc_1,…,c_m in order, once each; cutting it at those visits gives the factorization, which is unique because the run is. Conversely, the runs on x0,…,xmx_0,…,x_m concatenate to an accepting run. ∎ Proof of Theorem 23. Let Y be the sequential greedy output under φ . Between sampled positions both Y and the replayed draft D consist of the forced tokens φ prescribes, which depend only on the configuration. Let i∗i^* be the first sampled position of D that is not accepted. By induction over the sampled positions before i∗i^*: at each, the replay’s configuration equals the sequential decoder’s, the prefixes agree, so the logits computed by the certification pass at that position equal the sequential decoder’s logits in exact arithmetic (Theorem 19(i)), and acceptance means D’s token is the sequential choice. Hence D<i∗=Y<i∗D_<i^*=Y_<i^*, and the masked argmax at i∗i^* is Yi∗Y_i^*. Each round therefore extends the certified prefix by at least one sampled token, and repeating, or finishing sequentially after a cap on rounds, yields Y. ∎ Appendix D Mechanisms and engine as implemented D.1 Constraint compilation A JSON schema is turned into a regular expression by outlines-core; a regex constraint is used as given. Our parser builds a Thompson NFA over bytes (a character class over code points is expanded into UTF-8 byte sequences), determinizes it by subset construction with a state budget (200,000 by default; beyond it compilation stops with an error), trims states from which no accepting state is reachable, and minimizes by Moore refinement. Lookaround and backreferences are rejected. The vocabulary’s byte strings are recovered from the tokenizer; special tokens have no bytes and are never allowed by a constraint; added tokens that are not special (Qwen’s <tool_call>, </think>) receive their surface bytes, so a constraint that expects that text can allow the single token. The trie is stored level by level (arrays parentdparent_d, bytedbyte_d and the tokens ending at each node). D.2 The walk kernel The automaton is kept on the device as 256⋅|Q|256·|Q| int16 entries (⊥=−1 =-1), with the accepting vector and an end-of-sequence vector over the vocabulary; the vocabulary is packed once (every token’s bytes concatenated, with offsets: 1.5 MB plus 1 MB of offsets for the 248k tokens, the shared 2.9 MB with the rest). One Metal kernel (mx.fast.metal_kernel, grid ||×B|V|× B, threadgroup 256) runs per step: thread t of row b reads state qbq_b, walks its token’s bytes (s = table[s*256 + byte] until the end or ⊥ ) and writes the state reached. The mask is row≠⊥row≠ or (q accepting and the token is eos), combined with the boundary cover (len(t)≥cover[q]len(t) [q]); the next state is row[y]row[y]. The host side (accept, forced, finished) runs the automaton over the token’s bytes and uses the same planner as the table controller. States with at most 4,096 allowed tokens keep a sparse output head: their allowed ids are computed once on the CPU (about 4 ms) and stored (at most 16 KB per state). The batch engine builds one combined automaton table (block i is constraint i’s table with next states offset to global ids; global state 0 is the free state) and launches one kernel over all rows. Healing is off with the walk kernel, as it is in practice with the table (its threshold exceeds 200 tokens on our schemas). D.3 The forced planner (the canonical policy) Given the previous sampled token y and the configuration q after it, the planner follows the unique live byte while the configuration is forced (the forced string w), and then: (1) cuts s=bytes(y)ws=bytes(y)\,w to its longest valid UTF-8 prefix; (2) computes the pre-token block starts of s and holds back the last block, unless all of w survived, s does not end in whitespace, and for every byte allowed after w (every ASCII byte and one representative per non-ASCII class) the pre-tokenizer puts a boundary at |s||s| (the stable-tail test of Theorem 20(i)); (3) if the end of y is not a block boundary of s, re-encodes y together with w and replaces y before it is fed (healing; no cache rollback is needed in the synchronous loop); (4) tokenizes the committed segment with the model’s tokenizer and checks that the tokens spell it; (5) returns the tokens, whether y is replaced, the end configuration and the cover of the end configuration: if the remaining forced bytes form one pre-token block that is a single vocabulary token of length ℓ , the next token must have at least ℓ bytes. The cover is a per-state table on the device. D.4 The pushdown constraint Each nonterminal’s DFA has 256+C256+C columns (a call of NiN_i is the private code point U+200000+iU+200000+i, mapped to column 256+i256+i); states are numbered globally. The token tables are the level pass of Algorithm 4 for all states at once, with rows that carry a symbolic stack: pushes inside a token are recorded (at most three) and matched by pops inside it; a real pop splits the row into one row per candidate return state of the popped nonterminal (plus end of output for the root); at most two real pops are resolved and deeper ones masked. A token whose walk makes no real pop, or ends exactly at its single real pop, gets a context-free entry (next state, pushes, pops) in the ||×|Q||V|×|Q| table; a token that continues past a real pop, or pops twice, lives in a context table of shape nctx×nqc×(|R|+1)2n_ctx× n_qc×(|R|+1)^2 indexed by the top two stack symbols. The device state vector is [q,ptr,stack[0..63],S][q,ptr,stack[0..63],S], with S=∑r∈σbn(r)S= _r∈σbn(r) for budgets; masking and advancing are gathers on (q,top1,top2)(q,top_1,top_2). For the schema of a tree of named nodes the root rule is "name":S,"children":[(call0(,call0)∗)?(call_0( ,call_0)^*)^?] with S the JSON-string regex: 37 states, one call site and 6 context-dependent tokens at 4 states on Qwen’s vocabulary. D.5 Certified block-parallel decoding Plan. The planner accepts an object schema whose properties are all required, flattening nested objects of the same shape into their leaves; arrays and free strings stay single blocks. Two dummy documents with different placeholder values are rendered, recording for every leaf the byte offsets after its key and at the next key; running the automaton over each prefix gives the state after the key name and the exit state, which must agree between the renderings (the automaton is minimal, so the language after a value does not depend on the value). A block starts where the sequential decoder starts sampling, i.e. after the committed part of the key’s chain; its context is the bare key path ("parent":"key). Wave. Every block is a row of the batch engine, started from the prompt’s cache (array handles shared, recurrent state copied), with a controller that stops when the state leaves the block. Rows run in ragged mode (a sampled token and its forced span in one step). First-wave budget per block: 24 steps, or 1.5×1.5× the block’s mean length +2+2 once the schema has been seen. Certificate. The samples are replayed block by block through a fresh controller; the replay yields the token sequence D, the state before every sampled token and the block of each position, and detects three inconsistencies (a block reached at a state other than its branch’s start, a block cut by its budget, a previous token that carried past the block’s start). One pass over D from a copy of the prompt’s cache gives the logits at every position; the masked argmax (allowed row and cover at the recorded state) is compared with DiD_i. Every failing block continues in one wave from its first failing position with the correct token, its prefix re-prefilled from the prompt’s cache; the loop repeats (at most 24 rounds). What was tried and rejected. Earlier values as placeholders in the branch context (the model copied them), an ellipsis placeholder (copied), type names (copied); no initial plan at the block start (nothing certified); no first-wave cap (a runaway number such as 60.0000… cost the whole wave); certifying one mismatch per pass (one wave per failing block). Finite regions. An enum, a boolean or a tool name is a finite region: a depth-first search over the automaton lists every completion up to a budget (raising an error on a cycle), and all completions are scored after the same prefix in one right-padded batched pass; the decision is the completion with the largest summed log-probability. It is exact for what it computes; Appendix I reports why it is not a better classifier. D.6 Rows on demand (host-side variant) LazyConstraint keeps the automaton, the forced chains and the accepting information (O(256|Q|)O(256|Q|)) and a bounded dictionary of rows, each computed on first use by the level pass restricted to one root (about 4 ms per state on the CPU, since a free-text state keeps nearly every trie node alive). Memory is proportional to the visited states: 17 rows (13 MB) instead of the 824 MB table for the typed tool grammar. It runs on the synchronous engine only, because the pipelined engine builds the next mask before the host knows the sampled token; the walk kernel supersedes it. D.7 The engine Kernels. 4-bit matrix-vector kernels for 1–16 rows dequantize weights straight into 8×88× 8 simdgroup-matrix fragments (a fixed permutation inside each 128-wide chunk lets a lane find its 32 weights in one 128-bit load); a half-precision variant converts two nibbles with one shift, one mask and one fused multiply–add; a two-level autotuner picks, per shape and then per whole model step timed pipelined, among these families and MLX’s kernels (first load on the 4B: about 19 minutes; later loads 3 s). One fused Metal kernel per layer performs the whole Gated DeltaNet decode step (convolution, norms, gates, the delta-rule recurrence on the 128×128128× 128 state, the gated output norm) for up to 16 tokens. M1/M2 GPUs have no native bf16 arithmetic, so bf16 checkpoints run in fp16, which is also closer to float32 (Table 25). From 128 rows the prompt pass uses MLX’s dense matrix multiplication. Pipelining. A step is built lazily (logits, mask, sampled token y, next state q′=T[y,q]q =T[y,q]), and step n+1n+1 is enqueued with y and q′q as unevaluated device values while the GPU runs step n; the host’s graph construction (about 1.2 ms) and command encoding (1.8 ms) overlap the GPU’s 7 ms. When a forced span may follow q′q , the next step is built on a functional cache and discarded if the host, on reading y, finds a span, which is then fed with y in one pass. Outputs are identical to the synchronous loop. Batching. Streams join and leave a running batch at any step; every row feeds exactly one token per step, its next forced token or the token it sampled (drip mode), so each step is a uniform batch whose inputs are known without the host; new prompts are prefilled in one right-padded batch; a radix-trie prompt cache serves exact prefix hits (the recurrent state exists only at the end of a stored stream). Sampling. Greedy, or temperature with top-p and top-k under the same rule as mlx-lm’s sampler, so that sampled runs of the two engines follow the same distribution. D.8 The local tool: server, reply grammar and agents The engine is packaged as an OpenAI-compatible server (/v1/chat/completions with tools and json_schema response formats), serving our engine and stock mlx-lm with llguidance from one process, and as a command that configures the OpenCode coding agent (a team of orchestrator, coder, researcher, tester and reviewer agents driven through one opencode serve). Every request is a row of the running batch. The server re-renders an assistant turn that carried tool calls verbatim, so the whole previous turn is served from the prompt cache (647 of 675 prompt tokens on a tool round trip). A reply to a request that offers tools decodes under a regular language: free text that cannot start a call, then zero or more calls: REPLY =FREE(CALL(↩CALL)∗)?, =FREE\, (CALL\,( )^* )^?, CALL =<tool_call>↩<function=NAME>↩PARAM∗ = <tool\_call> <function=NAME > \,PARAM^* </function>↩</tool_call>, </function> </tool\_call>, PARAM =<parameter=P>↩VAL↩</parameter>↩, = <parameter=P > </parameter> , with NAMENAME an alternation of the offered tool names, VALVAL any text not containing </parameter> and FREEFREE any text containing neither <tool_call> nor <function=. In the typed grammar every tool’s parameter names and value types are fixed (1,106 states on Qwen’s vocabulary), which only the walk kernel can afford. Proposition 3 (Exact “not containing” expression). Let ℓ1,…,ℓm _1,…, _m be strings that start with < and contain no other <, and ρi _i be ℓi _i without its first character. A string contains no ℓi _i iff no segment that follows a < (segments being the maximal <-free substrings) starts with some ρi _i. In the trie of the ρi _i, such a segment either ends at a node p that is not a complete ρi _i or leaves the trie at p with a character that is not a child of p. Hence NotContaining(ℓ1,…,ℓm)=[^<]*(<(⋃p[^<c1⋯cj][^<]*∪⋃p))∗NotContaining( _1,…, _m)= [ <]* ( <( _pp\, [ <c_1·s c_j ][ <]*∪ _pp) )^*, where p ranges over trie nodes that are not complete ρi _i and have no complete ρi _i as a prefix, and c1⋯cjc_1·s c_j are the children of p. The construction is tested against brute force on all strings up to length 6 and on 2,000 random strings per literal set. Every tag of a call is a forced span (20–30% of a call’s tokens are fed, not sampled), and a reply cut by the token budget still closes its call. For small models the server cancels a reply that exceeds a number of complete calls, repeats a call, or repeats its last n tokens three times (n∈8,…,128n∈\8,…,128\), and steers a turn that repeats the previous turn’s call. Appendix E Speed: all measurements Setup. As in Section 5. Qwen3.5-2B is 1.1 GB resident and Qwen3.5-4B 2.26 GB. Stock means mlx-lm as shipped, in its own process, with its own kernels and bf16 arithmetic. Every number names the script that produced it; the result files ship with the paper. 1144881212161600224466tokens in the pass, Sτ(S)/τ(1)τ(S)/τ(1)if tokens cost linearlymeasured (2B, one stream) Figure 10: What a wider pass costs (Qwen3.5-2B, one stream). A pass over S tokens costs far less than S passes, because it is bound by reading the weights. On the 4B a pass costs 13 ms at S=1S=1, 21 ms at S=4S=4 and 39 ms at S=16S=16. E.1 One stream under a constraint Table 17: Constrained decoding, one stream: tokens per second (counting forced tokens), passes per output token, share of output tokens fed as forced spans, and the derived time per sampled token. f: llguidance’s fast-forward. Six JSON schemas and five recursive schemas. Qwen3.5-2B Qwen3.5-4B mode tok/s passes/tok forced ms/sampled tok/s passes/tok forced ms/sampled free decoding 138 1.01 0% 7.2 63.2 1.01 0% 15.7 JSON schema, stcon 180 0.69 31% 8.0 82.3 0.69 31% 17.6 JSON schema, llguidance f 136 0.72 28% 10.2 68.6 0.73 27% 20.0 recursive, stcon 170 0.72 28% 8.2 78.6 0.70 30% 18.2 recursive, llguidance f 143 0.71 29% 9.9 67.4 0.72 28% 20.6 recursive, llguidance 94 1.00 0% 10.6 Table 18: stcon and llguidance in one loop, full (max 256 tokens, medians of three interleaved rounds; 2B / 4B). For llguidance’s fast-forward the better of the plain and the overlapped integration (CPU mask computed while the GPU runs) is shown; the overlap gained at most 2%. Decode time is the sum over the tasks’ outputs. path engine tok/s passes/tok forced output tokens decode time ms/sampled regular free decoding 137 / 66 1.01 / 1.01 0 / 0% 570 / 597 4.15 / 9.02 s 7.2 / 15.0 (6 schemas) stcon 173 / 85 0.69 / 0.69 31 / 31% 327 / 329 1.89 / 3.89 s 8.3 / 17.1 llguidance, mask only 103 / 55 1.00 / 1.00 0 / 0% 343 / 333 3.34 / 6.08 s 9.7 / 18.3 llguidance, fast-forward 143 / 73 0.72 / 0.73 28 / 27% 343 / 333 2.41 / 4.59 s 9.8 / 18.8 recursive free decoding 135 / 67 1.01 / 1.00 0 / 0% 592 / 845 4.39 / 12.57 s 7.4 / 14.8 (4 schemas) stcon (pushdown) 161 / 84 0.72 / 0.70 28 / 30% 469 / 382 2.92 / 4.54 s 8.7 / 17.0 llguidance, mask only 103 / 56 1.00 / 1.00 0 / 0% 310 / 418 3.03 / 7.52 s 9.8 / 18.0 llguidance, fast-forward 141 / 73 0.71 / 0.73 29 / 28% 310 / 418 2.19 / 5.69 s 10.0 / 18.8 End to end. On 18 extraction jobs on the 2B (prefill plus decode), stcon takes 8.0 s against 12.3 s for llguidance, and 6.8 s when the prompt carries only the keys and enum options instead of the schema’s syntax, which the forced chains supply (Fig. 11 gives the batched version); agreement with the unconstrained answer is 0.93 in every mode and all outputs are valid. E.2 Recursive schemas in detail Table 19: Recursive schemas: five tasks (a Solar-System tree, an expression tree, a threaded discussion, a directory tree, a taxonomy) × three phrasings, Qwen3.5-2B, greedy, 400-token limit. ms per token is over valid outputs only. mode valid passes forced tokens ms / token stcon pushdown, canonical policy 11/15 1,452 921 5.9 stcon pushdown, commit-all 12/15 1,304 875 5.8 llguidance 12/15 2,204 0 9.4 llguidance fast-forward 12/15 1,309 895 7.0 On the expression task every engine fails: the model nests without end; ours stops at the depth cap, llguidance at the token limit. Under the canonical policy one phrasing of the discussion task duplicates replies until the limit; the same policy yields the complete Solar-System tree (all five planets, 92 tokens) where llguidance stops after Earth (46 tokens). Single greedy samples of a 2B model are path-sensitive in both directions. Forced spans cross returns: after a node’s last value the whole ],"name":" continuation is one span. E.3 Typed tool calls through the server On eight concurrent agent requests, two rounds: on the 2B, the typed grammar with the walk kernel produces 46 of 46 calls with every argument present and of its declared type at 366–403 tokens/s (30% of tokens forced, since parameter names are chains), against 43 of 52 typed calls with the untyped grammar and token tables at 372–410 tokens/s (20% forced). On the 4B, 8 of 8 calls are typed either way (131 against 139 tokens/s): the typed grammar turns a habit into a guarantee at a cost of 6%. E.4 Certified blocks Table 20: Forward passes per output: six schemas, three prompt variants each, greedy; sequential decoding against certified block-parallel decoding, which produces the same tokens in every case. On the 4B, block passes split into wave steps and certification passes. Qwen3.5-2B Qwen3.5-4B schema sequential blocks exact sequential blocks (waves + cert.) exact person 84 33 3/3 84 33 (30 + 3) 3/3 tool_call 35 17 3/3 35 20 (14 + 6) 3/3 product 112 53 3/3 112 46 (40 + 6) 3/3 event 169 96 3/3 167 109 (94 + 10) 3/3 classification 126 112 3/3 142 159 (148 + 7) 3/3 contact_card 146 63 3/3 146 117 (108 + 6) 3/3 all 18 outputs 672 374 18/18 686 484 18/18 rounds (max / median) 3 / 2 4 / 2 decode wall time 5.9 s 7.4 s 12.2 s 18.6 s First-round certification accepts 438 of 654 sampled tokens on the 2B and 365 of 668 on the 4B (the larger model commits to earlier values more). On the M2 Pro a wave step over 5–9 rows costs 14–20 ms against 7 ms for one row, and a certification pass over 34–50 tokens costs 33–55 ms. Per job on the 2B (first prompt variant): person 11 against 27 passes (210 against 230 ms), tool_call 6 against 12 (125 against 124 ms), product 19 against 38, event 32 against 56, classification 37 against 43, contact_card 21 against 49. E.5 Throughput by number of streams (engine) Table 21: Free decoding, total tokens/s by number of streams (256 tokens per stream, no constraint). mlx-lm on ours: mlx-lm’s batch generator running on our patched model in the same process. Qwen3.5-2B Qwen3.5-4B streams stock mlx-lm on ours stcon vs stock stock stcon vs stock 1 127 140 142 1.12×1.12× 61 64 1.04×1.04× 2 172 251 259 1.51×1.51× 82 116 1.41×1.41× 4 186 341 339 1.82×1.82× 87 160 1.83×1.83× 8 188 575 576 3.06×3.06× 87 271 3.13×3.13× 16 342 751 758 2.22×2.22× 157 341 2.17×2.17× 32 624 844 873 1.40×1.40× 64 615 837 952 1.55×1.55× 96 613 962 1.57×1.57× 128 613 830 892 1.45×1.45× Stock mlx-lm’s batch generator stalls between 4 and 8 streams; mlx-lm’s own loop on our patched model reaches our numbers, so the gain is in the kernels and fp16, not the loop. With the same prompt on all eight streams the numbers do not move (273 against 273 tokens/s for ours on the 4B), so nothing is shared between streams. At 128 streams the recurrent states hold 2.3 GB and the wider matrix multiplications cost more than the extra rows return. Single-stream decode on the 2B falls only from 138 to 118 tokens/s as the context grows from 128 to 8,192 tokens (Fig. 11), because only 6 of the 24 layers attend over the context; prefill runs at about 1,700 tokens/s. 1285121k2k4k8k005050100100150150context length (tokens)tokens/s, one streammlx-lm on our modelstcon4 slots8 slots16 slots0022446688wall time, 18 jobs (s)mlx-lm + llguidancestconstcon (compact hint) Figure 11: Left: decode speed against context length (2B, one stream, 128 output tokens). Right: batched constrained serving (2B, 18 JSON extraction jobs, best of two runs, all outputs valid). With the schema in the prompt our drip engine is 1.33×1.33× and 1.31×1.31× faster than mlx-lm’s batch generator with llguidance at 4 and 8 slots and level at 16, where a step is bound by arithmetic and forced spans buy nothing on a uniform batch. The compact hint puts only keys and enum options in the prompt (118 instead of 212 tokens) and lets forced spans supply the syntax: 1.51.5–1.6×1.6× at every slot count. E.6 Agents (engine, plus the typed grammar) Table 22: Parallel agents (built-in suite of small coding tasks, Qwen3.5-2B, greedy, every reply constrained to one well-formed tool call). Stock: mlx-lm’s batch generator with llguidance for the tool-call grammar. Both use continuous batching and the same prompt cache (94–96% hits). 16 agents 8 agents stock stcon stock stcon wall time 74.6 s 29.3 s (2.55×2.55×) 19.4 s 22.1 s (0.87×0.87×) throughput 125.5 tok/s 271.1 tok/s (2.16×2.16×) 108.6 tok/s 170.6 tok/s (1.57×1.57×) agents finished 9/16 12/16 5/8 6/8 checks passed 11/16 10/16 5/8 4/8 At eight agents our wall time is longer although the throughput is 1.57×1.57× higher, because our agents generated 80% more tokens (3,778 against 2,104): the engines do not make the same decisions, and this small model finishes about half the tasks under either. Throughput is the like-for-like number. Through the OpenAI-compatible server (stcon bench --n 8 --rounds 3, 2B), ours serves 1,928–1,954 output tokens per round in 4.6–4.8 s (median 410 tokens/s, 366–454 of the tokens forced) against 597–792 tokens in 4.5–7.3 s for stock (134 tokens/s); the stock replies are shorter, so the fair reading is about three times the tokens in the same wall time, every reply parsing. Four OpenCode coder agents through one opencode serve: 19 s wall, prompt cache 61%, three of four tasks correct. E.7 LiveCodeBench (engine) The 4B on LiveCodeBench [19] (code_generation_lite, release v6, 1,055 problems with hidden tests): the 40 most recent easy and medium problems (March–April 2025; 20 functional, 20 stdin), the official prompt, the last code block extracted, a problem passed only when every public and hidden test passes. Every engine runs in its own process on the same prompts. Table 23: LiveCodeBench on Qwen3.5-4B: pass@1, decode tokens, tokens/s (one stream) or in total (batch), wall time, answers cut at the cap. †Thinking on, 20 problems, 6 slots, temperature 0.6 / top-p 0.95 / top-k 20 (greedy loops in thinking mode); 5 of 20 finish within the cap on our engine and all 5 pass. cap engine pass@1 tokens tokens/s wall cut 1,024, greedy stcon, one stream 8/40 28.2k 63.4 481 s 23 mlx-lm, one stream 11/40 27.6k 62.3 499 s 22 stcon, batch 8 9/40 27.4k 160.4 171 s 22 mlx-lm, batch 8 10/40 28.3k 74.5 379 s 23 4,096, greedy stcon, one stream 9/40 96.0k 59.1 1,667 s 22 mlx-lm, one stream 14/40 87.2k 61.1 1,482 s 17 stcon, batch 8 12/40 93.3k 196.1 476 s 20 mlx-lm, batch 8 13/40 93.0k 78.7 1,181 s 19 16,384, thinking† stcon, batch 6 6/20 275k 119.8 2,296 s 15 mlx-lm, batch 6 1/20 4.4k — out of memory — Table 24: Which token does float32 prefer at a divergence?. For every problem where an engine’s output parts from mlx-lm’s single stream, the prompt plus the common prefix is run in float32 and the logit gap between the two competing tokens read. cap engine divergent median gap max gap float32: mlx-lm float32: other 4,096 stcon, one stream, fp16 35 0.056 0.52 3 32 stcon, batch 8, fp16 34 0.062 0.52 2 32 mlx-lm, batch 8 36 0.145 1.83 22 14 1,024 stcon, one stream, bf16 38 0.097 0.33 23 15 With thinking off, the 4B reasons in prose at length before its code; half the answers hit the 4,096-token cap, and the outputs of any two engines are identical on only 2–6 of 40 problems (mlx-lm’s own single-stream and batched paths agree on 4 of 40). Pass rates therefore differ by a few problems in either direction between engines that compute the same model, and every divergence is a near-tie; at those ties float32 prefers our fp16 engine’s token on 32 of 35. With thinking on and greedy decoding the 4B loops (16 of 20 problems run to a 16k cap, 11 repeating one sentence); with the model card’s sampling settings 5 of 20 finish and all pass, and mlx-lm’s batch generator runs out of memory at six 16k-token streams after one finished answer, where our engine completes the run inside the wired limit (Table 30). E.8 Arithmetic fidelity (engine) Table 25: Compute dtype against float32 (six prompts, 96 teacher-forced positions each). model dtype top-1 agreement mean KL p99 KL max KL max |Δlogit|| | 4B bfloat16 (mlx-lm) 0.9965 1.67×10−41.67× 10^-4 2.0×10−32.0× 10^-3 3.0×10−33.0× 10^-3 5.60 4B float16 (stcon) 1.0000 3.1×−3.1× 10^-6 4.6×10−54.6× 10^-5 9.1×10−59.1× 10^-5 0.31 2B bfloat16 0.9965 2.6×10−42.6× 10^-4 2.8×10−32.8× 10^-3 5.1×10−35.1× 10^-3 0.71 2B float16 1.0000 3.6×−3.6× 10^-6 3.6×10−53.6× 10^-5 5.3×10−55.3× 10^-5 0.09 On the 2B, greedy generations of the two engines diverge only at near-ties (competing tokens within 0.08 logits in float32); on twelve generic 4B prompts, 5 of 12 200-token generations are identical in either dtype, all gaps within ±0.27± 0.27, float32 siding with ours on 6 of 7 in fp16. Appendix F Memory: all measurements Memory is read from MLX’s own counters (active and peak bytes on the GPU) inside each engine’s process; the resident set size is meaningless for unified memory. Table 26: Constraint memory against grammar size: token table against walk kernel, pipelined engine, greedy, no healing on either side; tokens/s median of three interleaved rounds. The table’s memory is 3|Q|||3|Q||V| bytes; the walk’s is the automaton plus the 2.9 MB packed vocabulary. Outputs are identical wherever the table exists. 4B rows for the typed grammar and 96 fields are from a fresh process. tok/s, 2B tok/s, 4B grammar states table table build walk kernel table walk table walk person 104 77 MB 0.7 s 2.9 MB 12–14 μ 156 153 75 75 tool_call 164 122 MB 1.0 s 2.9 MB 7–9 μ 263 256 124 121 product 192 143 MB 1.3 s 2.9 MB 8–9 μ 191 189 90 89 event 178 133 MB 1.3 s 2.9 MB 7–9 μ 168 161 80 78 classification 158 118 MB 1.0 s 2.9 MB 7–9 μ 159 169 82 83 contact_card 246 183 MB 1.7 s 3.0 MB 7–8 μ 183 180 88 87 48 fields 986 735 MB 9 s 3.3 MB 9–14 μ 274 267 131 132 typed tool calls 1,106 824 MB 62–127 s 3.4 MB 11–18 μ 206 189 89 87 96 fields 1,970 1.5 GB not built 3.85 MB 8–14 μ — 260 — 121 What remains of the compile with the walk kernel is the automaton: 0.02–0.5 s for the schemas, 25–28 s for the tool grammar, whose subset construction, not its table, is the cost. On the 4B, a process that had already built the tables of the earlier grammars next to the model no longer had room for the typed grammar’s 824 MB table: it took 332 s to build and decoded at 6 tokens/s under swap pressure, while the walk in the same process ran at 25 tokens/s; the rows in Table 26 are from a fresh process. Table 27: Rows on demand (host-side variant, Qwen3.5-2B, synchronous engine, no healing): rows computed by one decode and their memory against the full table; tokens/s with the full table, with warm rows and with cold rows. grammar states full table rows row memory tok/s full / warm / cold person 104 77 MB 11 8 MB 129 / 124 / 95 tool_call 164 122 MB 9 7 MB 224 / 210 / 159 product 192 143 MB 21 16 MB 154 / 158 / 133 event 178 133 MB 17 13 MB 138 / 136 / 106 classification 158 118 MB 13 10 MB 135 / 139 / 123 contact_card 246 183 MB 16 12 MB 147 / 150 / 114 48 fields 986 735 MB 85 63 MB 215 / 222 / 160 typed tool calls 1,106 824 MB 17 13 MB 148 / 164 / 94 96 fields 1,970 1.5 GB (not built) 85 63 MB — / 222 / 159 Table 28: Constraint memory and compile time, token table, walk kernel and llguidance: Qwen3.5 vocabulary, CPU-side, each library in its own process, every grammar driven through a valid document computing the mask at every step. stcon token table stcon walk kernel llguidance person schema (104 states) 77 MB 0.05 MB <<0.5 MB 96 fields (1,970 states) 1.5 GB 1.0 MB <<0.5 MB typed tool calls (1,106 states) 824 MB 0.57 MB does not compile recursive schema (solar) 38 MB (pushdown tables) — <<0.5 MB 16-grammar server, grammars 7.2 GB (dies at the 15th) 4.9 MB 4.7 MB shared, once per process — 2.9 MB 153 MB compile, typed tool grammar 25 s DFA + 62–127 s table 25 s DFA — compile, one schema 0.7–1.7 s 0.02–0.4 s 1–2 ms mask, per step GPU gather 7–18 μ (GPU) 60–270 μ (CPU) Table 29: The server in the wild, both models: grammars served before failure, GPU memory above the model after the last grammar served, longest first-request wait. model, prompt cache constraints served above the model longest first request 2B, 50 MB token tables 15/16, then out of memory 8.2 GB 26 s 2B, 50 MB walk kernel 16/16 0.6 GB 2.8 s 2B, 1.5 GB token tables 14/16, then out of memory 7.6 GB 20 s 2B, 1.5 GB walk kernel 16/16 2.2 GB 3.1 s 4B, 50 MB token tables 14/16, then out of memory 6.9 GB 26 s 4B, 50 MB walk kernel 16/16 1.1 GB 6.6 s The sixteen grammars are the six schemas, then schemas of 8, 12, 16, 24, 32, 40, 48, 64, 80 and 96 fields; four requests per grammar, three concurrent. With the walk kernel the automata and the packed vocabulary are about 50 MB of the 0.6 GB above the model on the 2B; the rest is MLX’s buffer cache. Throughput with the walk kernel stays within the run-to-run spread (114–209 against 107–218 tokens/s on the 2B). F.1 Decoding regimes, the prefill transient and a memory budget (engine) Table 30: Peak GPU memory above the model by decoding regime (Qwen3.5-4B, B streams × N tokens on LiveCodeBench prompts, no constraint). stcon stock mlx-lm streams × tokens above the model tok/s above the model tok/s 1×40961× 4096 1.0 GB 65 0.8 GB 60 8×648× 64 (prefill only) 6.4 GB 3.8 GB 8×10248× 1024 6.4 GB 175 3.7 GB 82 8×40968× 4096 6.4 GB 212 5.2 GB 84 6×81926× 8192 4.9 GB 93 5.9 GB 64 6×163846× 16384 4.9 GB 128 out of memory — Table 31: The prefill transient (Qwen3.5-4B, our engine, nothing decoded): peak memory above the model while prefilling the longest prompt (1,360 tokens) alone, and B prompts in one right-padded batch, by prefill chunk. 2048 1024 512 256 128 one stream, 1,360 tokens 1.41 GB 1.46 GB 1.23 GB 1.09 GB 1.19 GB batch of 2 2.12 GB 1.36 GB batch of 4 3.50 GB 1.59 GB batch of 8 6.48 GB 2.43 GB At short contexts the peak is the prompt pass, not the caches: our batch engine prefills every admitted prompt in one right-padded batch with 1,024-token chunks, about 0.8 MB per token of (rows × chunk), while stock prefills four prompts at a time in 512-token steps but computes logits at every prompt position (about 1 MB per token). Capping a prefill pass at about 2,000 tokens brings our 8-slot peak to about 2.4 GB; skipping the output head in the single-stream prompt pass saves about 1.2 GB. At long contexts our caches never exceed the prefill transient (the peak at 6×81926× 8192 equals the peak at 6×163846× 16384, although the caches hold 3.3 GB at 16k tokens), while stock grows its KV cache by copying, so its growth costs about twice the raw cache and exceeds the wired limit at six 16k-token streams. A budget for n agents. With W the weights, C the prompt-cache budget, P the prefill transient, n streams of T tokens and G the constraints, the peak is about M≈W+C+P+n(s+τT)+GM≈ W+C+P+n(s+τ T)+G; on the 4B, W=2.26W=2.26 GB, s=50s=50 MB, τ=32τ=32 KB per token, P≈0.8MB×(rows×chunk)P≈ 0.8\,MB×(rows×chunk) for our batch prefill, and G is 3 MB per grammar with the walk kernel against 3|Q|||3|Q||V| bytes, never freed, with tables. Eight coding agents with 1,000-token prompts, 4,000-token answers and four schemas need 2.26+1.5+6.4+8×(0.05+0.13)+0.01≈11.62.26+1.5+6.4+8×(0.05+0.13)+0.01≈ 11.6 GB on our engine today, about 7.67.6 GB with the 2,000-token prefill cap; on stock mlx-lm with tables for the four schemas, about 10.810.8 GB, at the edge of the 10.7 GB limit. Appendix G Budget masking: measurements Table 32: Validity under a token budget, regular path (Qwen3.5-2B): budgets B=2,4,…B=2,4,… up to the full greedy answer; need0need_0 is the budget table’s value at the start (the shortest valid output under the forced-span policy). Feasible budgets are those with B≥need0B _0. schema full answer need0need_0 first valid feasible valid, mask valid, no mask person 34 16 16 10 10 1 tool_call 29 25 26 2 2 0 product 57 37 38 10 10 0 event 75 18 18 29 29 0 classification 58 22 22 19 19 1 contact_card 74 35 36 20 20 1 all 90 90 3 None of the 72 infeasible budgets (B<need0B<need_0) yields a valid output with or without the mask, as Theorem 21 predicts; the first valid budget is need0need_0 or the next even number. On the pushdown path (four completable recursive tasks, steps of six from eight tokens), the sound byte-level bound of Proposition 2 gives 54 of 61 valid outputs against 2 of 61, every budget valid from the first one that yields a valid output (12–20 tokens) upward. 0.30.30.50.50.70.70.90.911025%50%75%100%token budget, as a fraction of the full answershare of valid outputsregular, with maskpushdown, with maskregular, no maskpushdown, no mask Figure 12: Validity against the token budget (Qwen3.5-2B; budget as a fraction of each task’s full answer; six regular and four recursive tasks). Without the mask every cut output is invalid. With it, outputs shorten gracefully; where the masked regular curve is below 100%, the budget is below the shortest valid answer for some schemas. budget output (Qwen3.5-2B, the event schema) 320 (75 used) "title":"The Applied AI Summit","date":"2026-11-12","location":"venue":"Congress Center","city":"Berlin","country":"Germany","attendees":["name":"Dr. Aiko Tanaka","role":"speaker","name":"Lars Petersen","role":"speaker","name":"Nina Weber","role":"organizer"] 48 "title":"The Applied AI Summit","date":"2026-11-12","location":"venue":"Congress Center","city":"Berlin","country":"Germany","attendees":["name":"Dr.","role":"speaker"] 32 "title":"The Applied AI Summit","date":"2026-11-","location":"venue":"","city":"","country":"","attendees":[] 24 "title":"The Applied AI Summit","date":"","location":"venue":"","city":"","country":"","attendees":[] 40, no mask "title":"The Applied AI Summit","date":"2026-11-12","location":"venue":"Congress Center","city":"Berlin","country":"Germany","attendees":["name":" (cut mid-value, invalid) Figure 13: The budget mask on one output. As the budget tightens the decoder closes the array early, then shortens strings, then empties them, because it admits only tokens after which a valid ending still fits. Appendix H Quality: details Metrics. Agreement is the share of leaf values of the model’s unconstrained greedy answer (its parsed JSON) that the constrained output reproduces exactly, pooled over the six schemas (the per-workload mean is 0.94 / 0.87 for stcon). It measures fidelity to what the model would have said, not correctness, and it penalizes harmless variants. Gold correctness compares 45 objective fields of five schemas with values read off the source texts: person (name, age, email, status, three tags and their number: 8 fields), tool_call (function, location, unit, include_forecast, days: 5), product (name, with or without “The”; price, currency, in_stock, three categories and their number, three dimensions: 11), event (title, with or without “The”; date, venue, city, country, three attendees with names and roles and their number: 12), contact_card (all nine fields). The classification task has no single correct answer and is excluded. Strings are compared after trimming and lowercasing, numbers numerically. Intervals are 95% Wilson intervals with fields treated as independent, which they are not entirely. Table 33: Gold fields reproduced, per schema (outputs of Table 7). engine (2B / 4B) person tool_call product event contact_card all free, stcon, llguidance (all modes) 8 / 8 5 / 5 11 / 11 12 / 12 9 / 9 45 / 45 Segmentation policies. A separate run on the 2B (six schemas, 320-token limit, per-workload mean agreement) compares our three policies on the same regex: plain token-level masking (the model chooses how forced bytes are split) 0.93 at 343 passes, commit-all 0.93 at 246, and the canonical policy 0.95 at 224; llguidance in the same run reaches 0.95 with 341 passes (mask only) and 245 (fast-forward). The policy visibly matters on one task: under plain token-level masking the model writes “Just-Luc Moreau” on the contact card where its unconstrained answer and both forcing policies write “Jean-Luc”. Since only the segmentation policy differs between these runs, the divergence is due to the policy. Appendix I What did not help Table 34: Measured ceilings and negative results (Qwen3.5-2B). Every candidate was first bounded by replacing the component with a free stand-in and timing the real step. idea measurement defer the recurrent-state writes (a log of updates) removing the state store saves 2.3% of a step at batch 1, 6.7% at 16–32; not built a certified low-rank vocabulary head the head’s spectrum is flat: rank 1,024 of 2,048 rules out under 2% of rows; not built fuse the norms, residual adds and SwiGLU 2–10% of a pipelined step; each costs 1–2 μ score few-choice regions as a tree in one pass forced spans already absorb them: 0–4% fewer passes, no wall-time change finite regions (sequence-level decision of a label among 16) 2.0 passes against 2.9, but the intended label on 7 of 24 tickets against 15 for token-level greedy: the most probable complete string is the short generic label decode sibling subtrees of a recursive array in parallel slower on every task (Table 35); branches invent what their siblings decide speculative drafts in the batch engine a 2-token step at 8 rows costs 1.48×1.48× a 1-token step: batched steps are compute-bound prompt-lookup drafts verified against the constraint exact; 1.02×1.02× overall, 1.11.1–1.27×1.27× where the model copies, up to 11% slower where drafts are rejected; off by default block-parallel fields without a certificate 1.76×1.76× end to end on 18 requests at agreement 0.94, but approximate: a value does not see earlier values Table 35: Sibling-parallel decoding of recursive arrays (siblings.py, Qwen3.5-2B, wall time = prefill + decode). task sequential pushdown sibling-parallel solar 0.84 s, 109 tok/s, 11 nodes 2.02 s, 66 tok/s, 13 nodes (Venus given Earth’s subtree) thread 2.67 s, 143 tok/s 2.67 s, 71 tok/s (a reply duplicated) fs 0.85 s, 122 tok/s 4.03 s, 82 tok/s cats 0.55 s, 76 tok/s 2.00 s, 55 tok/s org 0.32 s, 79 tok/s 2.09 s, 89 tok/s menu 0.39 s, 104 tok/s 35 s, 1,168 invented nodes The block product holds for the language of sibling subtrees; it does not make the model’s decisions independent. That is why the certified block decoder verifies its drafts, and why the parallel decoding of siblings without verification fails. Appendix J Exactness and tests Exactness. In exact arithmetic none of the mechanisms changes what greedy decoding produces, except the canonical policy, which changes the segmentation of forced text on purpose (Theorem 19 compares decoders under the same policy; Appendix H). Measured: certified block decoding is token-identical to sequential decoding on all 36 outputs of both models; the walk kernel’s rows equal the table’s columns for every state, and its outputs are identical on every grammar, single-stream and batched; pipelined and synchronous loops give identical outputs; the pushdown tables equal byte-by-byte stepping on every reachable configuration of a small vocabulary with stacks to depth 4 (69k, 35k and 13k configuration–token pairs for three grammars) and brute force over all 248k tokens at sampled prefixes with the real vocabulary; budgets survive a simulated stopping rule with adversarial token choices. Comparisons with other engines are subject to floating-point near-ties (Table 24). Tests. 234 automated tests, 44 of which also run against the 4B: the capped traversal and path counts against brute force on random graphs; the regex parser, UTF-8 expansion, subset construction, trimming and minimization against Python’s re; forced chains, the canonical split, stable-tail commit, boundary cover and healing against the tokenizer; pipelined against synchronous decoding; every kernel family and the fused recurrent step against stock mlx-lm in both dtypes; the budget stopping rule; the pushdown (exhaustive reachable configurations, real-vocabulary traces, determinism and depth limit); the walk kernel against the table, single and batched; certified blocks against sequential decoding; the not-containing expression against brute force; the server (tool calls, prompt-cache round trip, JSON response formats); sampling with top-k and top-p. Protocol. One machine, one GPU job at a time, configurations interleaved inside one process with medians reported, baselines run as controllers in our loop with our kernels when the comparison is about the control side, and in their own process when it is about the engine.