diff --git a/docs/design/counted-content-automaton.md b/docs/design/counted-content-automaton.md index 2e026f7..b5e1709 100644 --- a/docs/design/counted-content-automaton.md +++ b/docs/design/counted-content-automaton.md @@ -572,3 +572,66 @@ that discharges the bound. Implementation is a separate, FP-critical effort gate 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. + +## Implementation blueprint (code-level, for the focused build) + +The algorithm and bound above are settled; this is the concrete plan so the build +is mechanical, not exploratory. It is the full scope of the reverted RTN attempt +(its *sharing* was correct) with the explicit stack replaced by the GSS. + +### Step 1: group-definition identity (no behaviour change) + +`Sources/Schema/ComplexType.swift`: `Term`/`Group` are value types, so a +multiply-referenced group has no exposed identity. Add `var definitionID: Int?` to +`Group`. `Sources/Schema/XSDParserParticles.swift` `groupReferenceParticle` +already keys the shared expansion by +`GroupParticleMemoKey(definition: ObjectIdentifier(definition), visiting:)` +(line ~105). Assign one stable `Int` per distinct key (a counter on `XSDContext`, +beside `groupMemo`) and stamp the cached group's `definitionID` when it is first +compiled, so every reference to the same expansion carries the same id and two +unrelated groups differ. Verify with a unit test on the parsed `Particle` tree +(same id for sibling refs, distinct for distinct definitions). Used by nothing +yet, so it ships green and FP-neutral on its own. + +### Step 2: call/return compilation (alongside, unused) + +A new `ContentRTNBuilder` (do NOT mutate `ContentNFABuilder`, the trusted oracle) +compiles each `definitionID` to ONE fragment, memoized in a +`[Int: (start, accept)]`. A `.group(group)` term whose `group.definitionID` is set +compiles to a `call` epsilon edge (target = the group fragment start, carrying the +return state) wrapped by the reference's own occurrence scope; the fragment's +accept is a `return`. Add two epsilon-edge kinds, `call(returnTo:)` and `pop`, to a +new `ContentState` variant or a parallel program type. Counters stay in the +configuration vector and are reset on entry exactly as today, so a shared fragment +entered from two live configurations does not alias (the reverted attempt proved +this part sound). A size test asserts the doubling chain compiles to `O(K)` states. + +### Step 3: GSS simulation (the new, FP-critical core) + +A `GSSNode` is `(returnState: Int, parents: Set)`, interned per +`(returnState, inputPosition)` so paths that return to the same site share one +node. The live configuration is `(state, counters, gssNode)`. The epsilon-closure: +on a `call(returnTo: B)` from gss node `P`, intern `Q = (B, {P})` (union `P` into an +existing `Q`'s parents) and continue at the callee start under `Q`; on a `pop` under +`Q`, fan out to `(returnState, parent)` for each parent. Deduplicate the worklist on +`(state, counters, gssNode)`. The consuming `step` and `isComplete`/`admissible`/ +`matchedParticles` carry the gss node through unchanged in shape. Accept iff a +configuration reaches the program accept under the EMPTY gss node. + +### Step 4: switch + gate (cardinal rule sacred) + +Differential (`ContentMatcher` is the oracle): over the whole XSTS corpus and the +`SchemaGenerator` fuzz (extended to emphasise multiply-referenced NULLABLE nested +groups, the exact shape that broke the pushdown), assert the RTN/GSS matcher's +accept/reject AND its per-child `MatchedParticle` equal the inlining matcher's. Only +when zero divergences: switch `ComplexValidatorContentModel` and `ComplexValidator` +to the RTN matcher, delete `ContentNFABuilder`. Add a perf ASSERTION (not a timeout, +per the reverted attempt's lesson) on a `K >= 24` doubling chain: poll the matcher's +own GSS-node and live-configuration counts and assert they stay `O(K)`, and that a +short instance validates in work proportional to its length. XSTS +`valid-schemas-rejected` stays 0; `invalid-schemas-accepted` does not rise (it may +fall: the instances that previously hung now get matched). + +Each step is its own PR; steps 1-2 are FP-neutral by construction (the oracle stays +authoritative), and step 4 is the only behaviour change, gated to verdict- and +attribution-equivalence on the corpus before it lands.