diff --git a/CHANGELOG.md b/CHANGELOG.md index 2f4c238..fd03580 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -11,6 +11,13 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 - Added an opt-in differential schema-validity harness against libxml2 (`XSTSDifferentialTests`, production-readiness stopper #3: characterise correctness against an independent reference, not just the labelled suite). Over 9618 corpus schemas PureXML and libxml2 agree on 4912 (3161 valid, 1751 invalid); the 87 where PureXML is stricter were triaged as PureXML being more correct (libxml2 omits facet consistency, Element Declarations Consistent, whiteSpace restriction, au-props-correct, and notation rules), independently corroborating that PureXML does not over-reject. The 117 where libxml2 is stricter are a false-negative triage queue (stopper #2), written with the rest to /tmp/xsts-differential.txt. xmllint and the corpus are used only in the test harness, never the shipped package. +- Added the counted-content-automaton design for the interactive resource-bound + arc. The design separates the language-recognition, matched-particle + attribution, and UPA/determinism claims; replaces occurrence unrolling with + counter scopes; states the target `O(N * S * D)` runtime and `O(S * D)` live + memory bounds; and makes deleting `occursUnrollCap`, `totalStateCap`, and + `positionCap` the acceptance criterion. + - OpenAPIKit-style validation framework completion: `BuiltinValidation` registry (23 rules), exhaustive fail/succeed isolation tests, configuration pins, public-type and field coverage gates (`scripts/check-validation-coverage.sh`, `scripts/check-validation-fields.sh`), warnings channel with `strict:` promotion, two-tier `Validator` defaults, XSD schema compile rules as composable validations (`SchemaCompileValidation`), and `ValidationOutcome` non-throwing accessor. ### Changed diff --git a/docs/design/counted-content-automaton.md b/docs/design/counted-content-automaton.md new file mode 100644 index 0000000..c3176da --- /dev/null +++ b/docs/design/counted-content-automaton.md @@ -0,0 +1,342 @@ +# Counted content automaton + +This is the design for replacing the content-model NFA's occurrence unrolling with +a counted automaton. It is intentionally separate from XSTS conformance fixes: +this work closes the production-readiness resource-bound stopper, not one +schema-validity bucket. + +## Problem + +`ContentNFABuilder` currently compiles a particle by copying the repeated term +`minOccurs` times and then adding optional copies up to `maxOccurs`. That makes +automaton size proportional to the numeric occurrence value, not to the schema +text. A short schema containing `maxOccurs="1000000000"` can request a billion +states. + +The current safety valves are: + +- `occursUnrollCap = 16384` +- `totalStateCap = 2^20` +- "degrade to star" when a cap is hit + +Those caps prevent OOM, but they change the language. A finite `{m,n}` can become +`{m,unbounded}` or, after an exhausted required prefix, effectively `*`. That is +a silent false negative: invalid instances can pass because the matcher widened a +bounded content model. + +`ContentModelDeterminism` has a smaller version of the same issue: +`positionCap = 4096` skips the UPA check when the raw position automaton grows +too large. Skipping a check is bounded as an under-rejection, but it is still +silent debt. + +## Sources + +Research notes read for this design: + +- `/Volumes/Code/DeveloperExt/private/PureXML-research/notes/strange-cases-literature.md` +- `/Volumes/Code/DeveloperExt/private/PureXML-research/notes/xsd-content-model-implementations-survey.md` +- `/Volumes/Code/DeveloperExt/private/PureXML-research/research/scientific-literature.md` + +The relevant literature line is: + +- Brüggemann-Klein and Wood: UPA is one-unambiguity; the Glushkov position + automaton is the canonical decision tool. +- Kilpeläinen and Tuhkanen: numeric occurrence indicators make naive + one-unambiguity algorithms erroneous or exponential; a polynomial method exists. +- Gelade, Gyssens, and Martens: counting separates weak and strong determinism; + unrolling can be exponentially less succinct than the counted representation. +- Kilpeläinen 2011: the principled XML Schema determinism tool is a counting + automaton, not occurrence unrolling. + +These are witnesses for the algorithm family. PureXML's implementation still has +to be derived against its own `Particle` model and verified locally. + +## Correctness claims + +Every claim below is labeled per proof discipline. + +| Claim | Status | Meaning | +|---|---|---| +| Counted matcher accepts exactly the same child-name language as the XSD particle tree for `element`, `wildcard`, `sequence`, and `choice` with `minOccurs`/`maxOccurs`. | theorem target | Proved by structural induction over the particle tree once the implementation replaces `ContentNFA`. | +| Counted matcher keeps per-child matched-particle attribution. | theorem target under UPA | For UPA-valid content models, each consumed element is matched to exactly one particle; that particle's type/value metadata is the one used by child validation. | +| Counted matcher build size is independent of numeric occurrence magnitudes. | theorem target | Program states and counters are proportional to particle nodes, not to `minOccurs` or `maxOccurs` values. | +| Counted matcher runtime is bounded for interactive validation. | theorem target | For `N` child elements, `S` program states, and `D` counter scopes, validation is bounded by `O(N * S * D)` time and `O(S * D)` live matcher memory. The constants are schema-structural, not occurrence-magnitude structural. | +| `all` groups remain exact. | theorem already implemented, out of scope for NFA replacement | `all` is validated by direct member counts in `ComplexValidator.matchesAll` and `allStructureErrors`; the counted automaton does not need to encode it initially. | +| Counted UPA/determinism replaces `positionCap`. | blocked design frontier | The instance matcher can be replaced first. Deleting `positionCap` requires a separate counted determinism pass or a proof that the existing clamp is exact for XSD's admitted content models. | + +## Bound representation + +Do not store occurrence bounds as only `Int`. + +XSD occurrence values are lexical `nonNegativeInteger`; users can write values +larger than machine integer range. The parser needs an internal representation +that preserves the bound and compares it without overflow: + +```swift +enum OccurrenceUpper: Sendable, Equatable { + case finite(NonNegativeDecimal) + case unbounded +} + +struct OccurrenceRange: Sendable, Equatable { + var minimum: NonNegativeDecimal + var maximum: OccurrenceUpper +} +``` + +`NonNegativeDecimal` is a normalized ASCII decimal string, with leading zeroes +removed except for `0`. It supports: + +- equality by string equality; +- ordering by digit count, then lexicographic comparison; +- `isGreaterThan(_ limit: Int)` without constructing a large integer; +- `clamped(to limit: Int) -> Int`, used only when the input length gives a + semantic cap. + +For a concrete instance with `N` child elements: + +- any finite upper bound above `N` is equivalent to `N + 1` for rejection/acceptance; +- any minimum above `N` means the model cannot complete after this child list; +- counters never need to hold values above `N + 1`. + +That is the key bridge from arbitrary-size lexical numbers to machine-size +runtime counters without changing semantics. + +## Program model + +Compile the particle tree to a counted epsilon program: + +```swift +struct CountedContentProgram: Sendable { + var states: [State] + var counters: [CounterScope] + var start: StateID + var accept: StateID +} + +struct State: Sendable { + var epsilon: [EpsilonEdge] + var consuming: ConsumingEdge? +} + +struct EpsilonEdge: Sendable { + var target: StateID + var guards: [CounterGuard] + var actions: [CounterAction] +} + +struct ConsumingEdge: Sendable { + var label: TermLabel + var target: StateID + var particle: MatchedParticle +} +``` + +A `CounterScope` belongs to one particle occurrence range. The scope records: + +- its `minimum`; +- its `maximum` (`finite` or `unbounded`); +- which nested counters must be reset at the start of each iteration. + +The edge language is small: + +- `reset(counter)` when entering a repeated particle's scope; +- `increment(counter)` when one iteration of the repeated body completes; +- `counter >= minimum` guard to allow exit; +- `counter < maximum` guard to allow another iteration; +- unconditional epsilon edges for sequence/choice structure. + +No operation copies the body `minimum` or `maximum` times. + +## Compilation rules + +The compiler is structural. + +### Element and wildcard + +An element or wildcard compiles to one consuming edge. The consuming edge carries +the same `TermLabel` and `MatchedParticle` metadata that `ContentState` carries +today. + +### Sequence + +Compile each child. Link the previous child's accept state to the next child's +start state with an unconditional epsilon edge. Empty sequence is one epsilon edge +from start to accept. + +### Choice + +Compile each branch. Add unconditional epsilon edges from the choice start to each +branch start, and from each branch accept to the choice accept. + +### Occurrence wrapper + +Every particle gets an occurrence wrapper around its term program: + +1. On entry, reset the particle counter and every counter nested in its term. +2. If `minimum == 0`, add an exit edge guarded by `counter >= minimum`. +3. If `counter < maximum`, enter the body. +4. On body accept, increment the counter. +5. After increment, either exit when `counter >= minimum` or loop when + `counter < maximum`. + +For `maxOccurs="unbounded"`, the upper guard is always true. For finite maximum, +the guard uses decimal comparison against the current counter value. + +The exact one-iteration case `{1,1}` still creates a counter scope initially. A +later optimization may erase scopes whose range is statically `{1,1}`; the proof +does not depend on that optimization. + +### Nested occurrence + +Nested scopes are reset when their containing scope begins a new iteration. This +is required for models like `(a{2,3}){4,5}`: the inner count is per outer +iteration, not cumulative over the whole match. + +This reset relation is computed during compilation by giving each particle term a +set of descendant counter IDs. When an outer scope loops, its entry edge resets +all descendants before the body is entered. + +## Runtime algorithm + +A runtime configuration is: + +```swift +struct Configuration: Hashable { + var state: StateID + var counters: CounterStore +} +``` + +`CounterStore` holds only counters whose value differs from zero. Values are +machine `Int`s clamped to `N + 1`, where `N` is the child-count being validated. + +Validation: + +1. Compute epsilon closure from the start configuration. +2. For each child name: + - inspect consuming edges from the current closure; + - select matching edges by `TermLabel.matches`; + - emit the matched particle for the chosen edge when the model is UPA-valid; + - advance to each target configuration; + - compute epsilon closure again. +3. At the end, accept iff any closed configuration is at the accept state. + +Closure applies guards and actions atomically per edge. A guard that fails drops +that edge. An increment above `N + 1` stores `N + 1`; no later decision can +distinguish values above that threshold for a length-`N` input. + +## Determinism and attribution + +For valid XSD content models, UPA says no input element can be attributed to two +different particles at the same position without lookahead. The counted matcher +should preserve the current API: + +- `matchesWhole(_:)` +- `follow(after:)` +- `matchedParticles(_:)` +- incremental `startStates` / `step` + +Internally, those APIs become wrappers over counted configurations instead of +plain NFA state sets. + +When more than one consuming edge matches a child, that is either: + +- an invalid schema that UPA should have rejected; or +- a known UPA under-rejection frontier. + +The implementation may keep the current deterministic tie-breaker for recovery +diagnostics, but it must not call that tie-breaker a proof. The proof of +attribution applies only when the content model is UPA-valid. + +## Follow sets and completions + +`follow(after:)` returns labels available from the current closed configurations. +The counted closure means these labels respect counters exactly: + +- after consuming `a` once in `a{1,1}`, `` is not offered again; +- after consuming `a` once in `a{1,2}`, `` is offered once more; +- after consuming `a` twice in `a{1,2}`, `` is no longer offered; +- after consuming fewer than `minOccurs`, completion is false even if the current + state is structurally close to accept. + +This is the visible user-facing benefit for IDE completions: numeric occurrence +diagnostics become exact without unrolling large bounds. + +## Resource bound + +Let: + +- `P` be the number of particle nodes in the compiled content model; +- `S` be the number of counted program states; +- `D` be the number of occurrence scopes/counters; +- `N` be the number of child elements being matched. + +Compilation creates a constant number of states and edges per particle and a +constant number of counters per particle: + +- `S = O(P)` +- `D = O(P)` +- build memory `O(P)` + +During matching, each active configuration has one state and at most `D` live +counter values. For UPA-valid models the closure frontier is bounded by the +program size. Each child step evaluates each reachable consuming edge and closure +edge at most once per distinct reachable configuration after deduplication. + +Target bound: + +- time `O(N * S * D)`; +- live memory `O(S * D)`; +- counter values bounded by `N + 1`; +- no factor depends on the numeric magnitude of `minOccurs` or `maxOccurs`. + +This is the proof obligation the implementation must satisfy before deleting the +current caps. + +## Migration plan + +1. Add `NonNegativeDecimal`, `OccurrenceUpper`, and `OccurrenceRange` while + preserving the existing `Particle` API for call sites that only need small + integer comparisons. +2. Add `CountedContentProgram` and a builder beside `ContentNFABuilder`. +3. Add differential tests comparing old and counted matchers on ordinary models + below the current caps. +4. Add high-bound tests that are exact and currently impossible without language + widening: + - `a{2,2}` rejects one `a` and three `a`s; + - `a{2,100000000000000000000}` accepts two `a`s and rejects one; + - `a{0,2}` rejects three `a`s; + - `(a{2,3}){2,2}` accepts four to six `a`s and rejects three/seven; + - `sequence(a{1000000000000}, b)` never offers `b` before enough `a`s. +5. Switch `ComplexValidatorContentModel`, `XSDCompletions`, and + `matchedParticles` to the counted program. +6. Delete `occursUnrollCap` and `totalStateCap`. +7. Replace `ContentNFAStateBudgetTests` with exact high-bound tests. The old + state-ceiling assertion should disappear because there is no state ceiling. +8. Design and land the counted UPA pass; then delete `positionCap`. + +## Non-goals for the first implementation slice + +- Exact Particle Valid (Restriction) language inclusion. That remains the + `ParticleRestriction` arc; inclusion for counted regular expressions is a + different and harder problem. +- Regex counted quantifier replacement. `RegexAutomaton` has the same cap posture, + but XSD content models are the IDE resource-bound blocker. Regex can reuse the + counted-bound representation later. +- Changing `all` group semantics. `all` is already matched by counters over its + members and has XSD-specific occurrence limits. + +## Done criteria + +This arc is complete only when all are true: + +- `ContentMatcher.swift` contains no `occursUnrollCap`, `totalStateCap`, or + cap-triggered "degrade to star" path. +- `ContentModelDeterminism.swift` contains no `positionCap` skip. +- Tests include exact high-bound acceptance/rejection cases whose numeric bounds + exceed any practical unroll count. +- The proof labels in this document are upgraded from "theorem target" to + "theorem" with code references. +- `docs/release-hurdles.md` no longer lists content-model occurrence unrolling as + an interactive-safety blocker. diff --git a/docs/plans/2026-06-18-false-negative-tail.md b/docs/plans/2026-06-18-false-negative-tail.md index 5e0d0c9..2ad3b6e 100644 --- a/docs/plans/2026-06-18-false-negative-tail.md +++ b/docs/plans/2026-06-18-false-negative-tail.md @@ -291,6 +291,8 @@ acceptance criteria for this later arc are: delete `occursUnrollCap`, `totalStateCap`, and `positionCap`; remove silent "degrade to star" behavior; state a worst-case time and memory bound; prove high numeric occurrence bounds do not create proportional states. +The design artifact is `docs/design/counted-content-automaton.md`; implementation +must follow that proof plan rather than adding another cap. **Verifies:** diff --git a/docs/release-hurdles.md b/docs/release-hurdles.md index 13ceae2..525cef4 100644 --- a/docs/release-hurdles.md +++ b/docs/release-hurdles.md @@ -132,4 +132,5 @@ foundational rather than incremental. - **Part 2:** a counter-automaton design for `ContentMatcher` (and the determinism automaton), with acceptance criteria = the `occursUnrollCap` / `totalStateCap` / `positionCap` caps deleted and a stated worst-case bound, no silent star-degradation - (M4 "proven bounds"). Aligns with the performance epic (#139, #175–178). + (M4 "proven bounds"). Aligns with the performance epic (#139, #175–178). The + design is now pinned in `docs/design/counted-content-automaton.md`.