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.