From 1057fc19d0673cb4d48e4114c97ac0d607a66786 Mon Sep 17 00:00:00 2001 From: Mihaela Mihaljevic Date: Sun, 28 Jun 2026 01:15:51 +0200 Subject: [PATCH] docs(design): derive the graph-structured-stack bound for the content matcher (#361) Closes the proof gap that sank the reverted RTN matcher. The counted automaton removed the occurrence-magnitude blow-up and the compositional determinism check removed the determinism group-sharing blow-up, but the per-instance matcher build (ContentNFABuilder.group) still expands a multiply-referenced group once per reference, so a doubling chain g0=(g1,g1)... builds 2^K states and hangs on the first validate. That is the last place stopper 4 is a hang, not a proven bound. The reverted pushdown rewrite compiled the group DAG to call/return edges (O(groups) program) but kept EXPLICIT return stacks, so a nullable doubling chain made the start epsilon-closure reach ~3^depth distinct stacks: the exponential moved from the build to the per-keystroke closure. It was verdict-correct yet bounded nothing, and was reverted. This section derives the fix: a graph-structured stack (the GLL/Earley device). A GSS node (returnState, parents-set) shares stack suffixes, so configurations are keyed on (state, counters, gssNode) and the live set is bounded by O(states), not by the number of distinct stacks. The nullable doubling chain that produced 3^depth explicit stacks produces O(K) GSS nodes. The section states the size and termination bounds (counters clamped to N+1, non-recursive group DAG), the deterministic-model O(N*S*D) match, and the same alongside-then-differential-gated rollout that made the compositional-determinism change FP-safe, with a perf ASSERTION on configuration/GSS counts rather than a wall-clock limit (the reverted attempt's lesson). Design only; no code change. Status: DESIGNED, not implemented. --- docs/design/counted-content-automaton.md | 125 +++++++++++++++++++++++ 1 file changed, 125 insertions(+) diff --git a/docs/design/counted-content-automaton.md b/docs/design/counted-content-automaton.md index 033e9b4..2e026f7 100644 --- a/docs/design/counted-content-automaton.md +++ b/docs/design/counted-content-automaton.md @@ -447,3 +447,128 @@ skip; verdict-equivalent on the XSTS corpus (zero divergences); `SchemaDeterminismGroupBlowupTests` compiles a 2^20-position model without hanging and rejects an ambiguous one; XSTS `valid-schemas-rejected` 0 and `invalid-schemas-accepted` unchanged at 15. + +## The matcher's group-sharing residual (the open resource bound) + +The counted automaton above removed the *occurrence-magnitude* blow-up (a +`maxOccurs="1000000000"` no longer allocates a billion states). It did NOT remove +the *group-sharing* blow-up. `ContentNFABuilder.build` is called per instance +(`ComplexValidator` and `ComplexValidatorContentModel`), and its `group(_:)` +recurses into a group's body once per *reference*. The compiled `Particle` tree is +a DAG (a multiply-referenced group is one shared, copy-on-write `Particle`), but +the NFA build flattens that DAG by tree traversal, so a doubling chain + +``` +g0 = (g1, g1) g1 = (g2, g2) ... g_{K-1} = (gK, gK) gK = +``` + +builds `2^K` states. There is no cap on this path; validating any instance against +such a model hangs on the first `validate`. This is the last place the +production-readiness resource bound (stopper 4) is a hang, not a proven bound. The +determinism check escaped the same `2^K` by summarizing each group once +(`CompositionalDeterminism`, DONE above); the matcher must escape it too. + +### Why the reverted pushdown did not close it + +The natural fix is to compile the group DAG to a Recursive Transition Network: a +group reference becomes a `call(returnTo:)` epsilon edge into the group's single +shared sub-program, and the group's accept becomes a `pop`. Then the program is +`O(groups)`, not `2^K`. That rewrite was built and reverted (2026-06-23): it was +verdict-correct (full suite + XSTS + the streaming differential all passed) but +did not bound anything. It keyed each live configuration on +`(state, counters, stack)` and enumerated configurations explicitly. Over a +*nullable* doubling chain the start-state epsilon-closure alone reaches +exponentially many distinct return stacks (measured `~3^depth`: +`startStates().count` was 1.72M at depth 10), because a nullable group can be +entered and exited by epsilon, and each distinct path leaves a distinct explicit +stack. The exponential moved from the build to the closure; arguably worse, +because it now fires on every keystroke, not just on compile. + +The lesson (recorded against this design): an RTN with **explicit** stacks is not +a bound. The configuration count must be made independent of the number of +distinct stacks. + +### The fix: a graph-structured stack (the stack DAG) + +Represent the return stack as a **graph-structured stack** (GSS), the device GLL +and Earley parsing use for exactly this. A GSS node is a pair `(returnState, +sourceSet)` where `sourceSet` is a set of *parent GSS nodes* rather than a single +parent. Two computations that reach the same `returnState` by different paths +*share* that one GSS node, recording both parents in its `sourceSet`; they do not +fork two stacks. A `pop` from a GSS node fans out to all its parents. + +The live configuration set is then keyed on `(state, counters, gssNode)`, and the +number of distinct GSS nodes at a given input position is bounded by the number of +distinct `returnState`s, which is `O(states)`, NOT by the number of distinct +explicit stacks (`2^K`). The nullable doubling chain that produced `3^depth` +distinct explicit stacks produces `O(K)` distinct GSS nodes: every entry into the +shared `g_i` sub-program that wants to return to the same site reuses the one GSS +node for that site. + +This is the precise meaning of "collapse matching-equivalent stack-distinct +configurations": configurations that agree on `(state, counters)` and on the +*return continuation* (the GSS node, which is the shared tail of every stack that +returns there) are one configuration. Different *prefixes* of the stack are +already shared as the GSS's parent edges. + +### Bound (theorem target, to discharge before implementing) + +Let `S` be the number of program states (`O(schema text)`, since groups compile +once), `D` the number of counter scopes (`O(S)`), and `N` the instance child +count. Counters are clamped to `N+1` (the bridge above), so a counter vector has +`O(D)` entries each in `0...N+1`. + +- **GSS size.** A GSS node is created per `(returnState, inputPosition)`, so there + are `O(S·N)` GSS nodes over a full match, each with at most `O(S)` parents: + `O(S²·N)` GSS edges. Claim: independent of group-nesting depth, hence no `2^K`. +- **Epsilon-closure termination.** Group definitions are non-recursive (a + transitive self-reference is already a schema error), so the call graph is a + DAG; combined with the counter guards (a counter cannot be incremented past its + clamp, and a nullable body's empty iteration is taken at most once per GSS node), + the closure at one input position visits each `(state, counters, gssNode)` once. +- **Per-position work.** `O(S·D·(N+1)^{?})` configurations bounded by deduplication + on `(state, counters, gssNode)`; for a **UPA-valid** model (the only models the + matcher ever runs on, since a non-deterministic model is a rejected schema) the + live set at each position has size `O(S)` because determinism leaves at most one + matching consuming edge per element. So for the conformant case the match is + `O(N·S·D)`; the general (defensive) bound is polynomial via the GSS, never + `2^K`. + +The acceptance discipline mirrors the determinism rollout, which the cardinal rule +makes non-negotiable: + +### FP-safe rollout (cardinal rule sacred) + +1. Build the GSS matcher ALONGSIDE the inlining `ContentNFABuilder`; the inlining + matcher stays authoritative. +2. Differential: for every fuzzed schema whose inlining build stays under a size + the oracle can afford (so the inlining matcher is exact) AND over the whole + XSTS corpus, assert the GSS matcher's accept/reject AND its per-child matched + particle equal the inlining matcher's. Extend `SchemaGenerator` to emphasize + multiply-referenced *nullable* nested groups (the exact shape that broke the + pushdown). Reuse the #246 deep-group differential. +3. Iterate toward agreement; the inlining matcher is the trusted oracle, any + divergence is a GSS bug fixed toward it. Nothing ships until equivalent. +4. Switch the matcher and delete the inlining build. Add a perf ASSERTION (not a + wall-clock limit, per the reverted attempt's lesson): on the `2^K` doubling + chain at `K ≥ 24`, assert the live configuration set and GSS node count stay + `O(K)` (poll the matcher's own counts), and that a short instance validates in + work proportional to its length, not `2^K`. + +### Acceptance criteria + +- `ContentNFABuilder`'s per-reference group expansion is gone; a group compiles + once. +- The GSS/inlining differential passes on XSTS + a deep nullable-group fuzz. +- A perf test on a `K ≥ 24` doubling chain asserts `O(K)` configuration/GSS counts + (the bound is observed, not timed). +- XSTS `valid-schemas-rejected` stays 0 and `invalid-schemas-accepted` does not + rise (it may fall: instances that previously hung now get matched). + +### Status: DESIGNED (2026-06-28), not yet implemented + +The reverted pushdown failed for lack of this proof; the GSS is the representation +that discharges the bound. Implementation is a separate, FP-critical effort gated +exactly as the compositional-determinism change was. Until it lands, the residual +stays disclosed: a deeply-nested, multiply-referenced group model is the one +content shape whose per-instance match is not yet polynomial.