Add proof test for JSON tokenizer minus state EOF handling - #1549

Reviewed at fe928fa2, baseline origin/main = 6d26e264. Proof-only, one file. Approving — the case has real, two-sided-verified kill power, and it avoids the two weaknesses that made earlier cases in this family vacuous.

Two-sided mutation test

Three independent mutations of the target branch (parseMinusState's input === null arm), each applied with node -e and grep-confirmed to have landed:

In every case the single failure is parseMinusStateEof and nothing else, so the case is the sole cause and nothing on main covers this branch. npm test at the head is 2653 pass / 0 fail against 2652 on main — exactly the one new case.

Against the known weaknesses in this family

• #1518 (pinned the error message, so a branch change preserving the message survived): not repeated. This case pins kind, not message, so it keys on the branch's semantic output rather than its prose.
• #1525 / #1528 (pinned one field, so a mutant with the right tag and a clobbered state survived): not repeated. It pins both halves of the returned pair — state.kind and the token list's length and kind. The def → - mutation above is exactly the #1525 mutant, and it dies here.
• #1535 was correctly not a defect because proof.throw asserts only that something throws; that reasoning does not apply here — these are assertEq on concrete values, so the distinction is moot.

Coverage delta (real numbers, npm run cov)

npm run cov produced a usable report in this environment on this run (it has reported a vacuous 100.00 over 0 tests before; it did not here — 2653 cases ran).

fjs/media/json/tokenizer/module.f.mjs   branch  93.75 -> 97.06
all files                               branch  98.60 -> 98.62

Line and function coverage were already 100.00 in that file and are unchanged; the gain is entirely the branch this case targets.

The unreachability claim in the comment

The comment asserts the branch cannot be reached through the public tokenize. I checked rather than took it: I replaced the branch body with a throw and ran tokenize over -, - , - , --, -x, -1, -\n, -, [-, [1,-], {"a":-, and "". None hit it — the JS tokenizer's own eof token takes the default arm and resets the state to def before the appended null sentinel arrives. The comment is accurate.

That does mean the branch is currently dead through the public API, and one could argue for deleting it instead of covering it. I do not think that is the right call here: parseMinusState is a StateScan handler whose input type includes null, so the arm is part of a total function over its declared domain, and covering it is cheaper and safer than narrowing the type. Noting it only so the choice is explicit.

Conventions

• export const proof in module.f.mjs (rather than proof.f.mjs) is required here because parseMinusState is module-private, and it is established practice — 10 module.f.mjs files already do it, including the sibling fjs/media/json/parser/module.f.mjs and fjs/js/tokenizer/module.f.mjs.
• No CHANGELOG entry, correctly: §8.3 exempts proof-only changes, and the diff touches nothing else.
• npx tsc --noEmit exit 0.