Implement EOF as semantic symbol -1 with logical synthesis - #1516

Approving. I reviewed the eof-minus-one.md specification earlier, so this pass checked the implementation against what that design established rather than just re-reading the diff.

Gates

Codec

The implementation matches the spec's formulas (mask is the doc's terminalMask, terminalSize = mask + 1). I re-verified exhaustively against the code as written, not the doc:

• all 16,777,216 semantic values -1 .. 2^24 - 2 encode to 16,777,216 distinct codes, 0 round-trip failures;
• the reverse direction too: every one of the 2^24 stored codes decodes into the semantic domain and re-encodes to itself.

Negative-controlled by perturbing decodeTerminal to ((value + 2) & mask) - 1, which fails all 16,777,216 in both directions.

Ordering

This is the defect the design invites, so I checked every comparison the change touches, and all of them are on decoded values:

• removeOne decodes both operands before the a0 < a / b < b0 comparisons and before Math.min / Math.max;
• descent compares rangeContains(...rangeDecode(rule))(symbolAt(...));
• ll1 builds its dispatch rangeMap from rangeDecode(rule), so stored codes never reach the map — the emitted cut point for eof is [[null, -2], [·, -1]], which is what the new proof pins.

Behavioural spot-checks past the ASCII range where an encoded comparison would have shown up: not({e: eof}) → [[0, 16777214]] (EOF is not in any complement); remove([-1, 5], {eof}) → [[0, 5]]; remove([-1, 5], {2}) → [[-1, 1], [3, 5]]; a terminal spanning [-1, 'A'] matches empty input, A, and rejects B in both backends.

The beforeEOF || afterEOF correction

Taken in the corrected form, and existing whole-input grammars still accept. In ll1, the empty-input path only diverges from main's when dispatchOp.get(rangeMap)(eofSymbol) is non-null; otherwise it returns main's mrSuccess(emptyTag, [], emptyTag === undefined ? null : cp) verbatim, so a grammar that does not mention eof is untouched. descent likewise only reaches the new pos === cp.length case for a rule that can match EOF. Verified end-to-end: fjs/fsc/json.f.mjs still parses {"a":[1,2,null]} on both backends (descent idx 16 of 16), and the body eof idiom accepts ABC / rejects AB1 on both, with descent reporting failure.idx = 2, expected = [range('AZ'), eof].

Also checked the constants you flagged: offset = 24 and mask = 16777215 are unchanged; eof still packs to 0xFFFFFF_FFFFFF so old serialized eof reads correctly; fullRange moved 0x000000_FFFFFF → 0x000000_FFFFFE, and unicodeRange is unaffected because ordinary symbols encode to themselves. grep over the tree found no remaining literal carrying the old EOF code, so there is no stale in-repo range needing regeneration. token_symbol.capacity is arithmetically identical to main's (0xFFFFFE - 0x110000 + 1 = 0xFFFFFF - 0x110000), so that alphabet did not silently resize.

New proofs actually cover the new paths

Mutation-tested rather than assumed — 14 mutants against the bnf proof trees:

killed — decodeTerminal identity (14 fails), maxSymbol off-by-one (4), fullRange back to the old literal (6), isValid excluding EOF (module load throws), ll1 EOF made repeatable (1), ll1 EOF not marked consumed (1), ll1 EOF synthesis removed (4), descent pos <= cp.length → < (6), symbolAt returning -2 (6), physicalIdx not clamping (7), leafAt emitting an EOF leaf (5), descent failure recorded on the physical index instead of the complete cursor (1).

survived — two, neither a coverage gap I would act on:

• encodeTerminal → value & mask is an equivalent mutant: adding 2^24 cannot change the low 24 bits, so the two expressions agree on the whole domain.
• capacity = lastOrdinary - start + 1 → + 2 survives because the only test that exercises the bound, throw.tooManyNames, builds its array from capacity itself. Pre-existing — main's capacity = eofSymbol - start has the same self-referential pin — and the value is provably unchanged, so nothing regressed. If you want it pinned, assertEq(capacity, 0xFFFFFE - 0x110000 + 1) would do it.

Coverage

npm run cov gives real numbers here (Node v23.11.0), so the new branches are measured, not assumed:

(line / branch / function.) descent holds 100% branch across a considerably larger module, and ll1's branch number moved up; the residual gap there is pre-existing.

One optional nit

ll1/types.ts documents MatchRule as "Internal match function signature used by compiled dispatch rules", and it is used only inside ll1/module.f.mjs — yet it is exported unprefixed while the sibling this PR adds is _MatchResultEof. Since you are changing its signature anyway, this is a cheap moment to make it _MatchRule. Not a blocker, and not something this PR introduced.

Nothing else. The [eof, eof] LL(1) result (success: true, null remainder) reads oddly, but that is this backend's pre-existing "ran out of input" convention — main returns the same shape for [range('AA'), range('BB')] on "A" — and the proof comment says so explicitly. descent reports it as a proper failure.