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.
Mihaela Mihaljevic
1057fc19d0