cat / miau-is-true
clone

a browser grid puzzle game where you push words around to rewrite the rules of each level

main
miau-is-true / openspec / changes / archive / 2026-09-24-scale-solver-state-search / verification.md
verification.md 6.4K source

W3 verification ledger

The compact codec, parent-linked breadth-first core, public fallback adapter, and fast engine transition are committed independently. This ledger separates mechanical parity from solver rollout and world performance claims.

State and turn parity

  • Codec round trips preserve the next direct-engine event and settled state after noun chains, automaton waits, SINK removal, and word-rule edits.
  • Thirteen focused fast-turn tests compare stepFast() and waitFast() with public step() and wait() across stacked rules, PUSH/STOP, DEFEAT/WIN, transformations, SINK removal, Clockwork phases, word-motion provenance, blocked input, and parser-budget rollback. Fast transitions add no Undo entry.
  • A temporary differential script took up to 32 deterministic movement actions on each of 30 available core and draft-world levels, adding waits on automata levels. It found zero mismatches in acceptance or settled state.
  • Ten exact baseline routes across core, Word Lab, Crossword, Crate Works, Tidewater, and Clockwork contributed 150 actions with zero mismatches after every action. The comparison included objects, nouns, rules, sentence spans, automata phases, and win state.

At this checkpoint the full Node suite passed 260/260 and npm run build passed. The world author CLI has not yet switched to the compact solver, so the baseline routes and memory figures remain the pre-rollout comparison.

Compact solver comparison before CLI rollout

The committed solveLevel() adapter was run in separate processes with both public and fast engine transitions at the same proof caps used in the baseline. All ten proofs returned the exact baseline action strings, and both modes attempted and expanded the same number of states for each proof. Elapsed time for the larger searches was:

Proof Public transition Fast transition Attempts / expanded
Core break-the-rule 4.5 s 3.8 s 46,792 / 11,698
Crate Works night-shift 1.02 s 0.83 s 4,636 / 1,159
Clockwork mouse-hole 9.8 s 8.0 s 61,323 / 12,265
Crossword pass-it-on 31.2 s 26.1 s 290,092 / 72,523

The smaller core, Word Lab, and Tidewater proofs also matched their exact routes and counts; fast mode was no slower in this run. Timing is descriptive, not a CI threshold. A separate 20 ms in-process RSS sampler measured fast-mode peaks of 149.0 MiB for break-the-rule, 145.3 MiB for mouse-hole, and 190.6 MiB for pass-it-on. Those runs included the normal shortest-path search only. The pre-W3 whole-command baseline also includes a BYPASS re-search, so its peak RSS is not a direct one-to-one memory comparison.

For a direct memory comparison, the temporary legacy CLI copy was run again with only its normal shortest-path search; BYPASS re-search was disabled in that temporary copy. A 20 ms worker-thread RSS sampler measured each process under the same proof cap. Routes and search counts were identical to fast mode:

Proof Legacy / fast elapsed Legacy full-state RSS Compact fast RSS Reduction
Core break-the-rule 6.38 / 3.75 s 251.0 MiB 149.0 MiB 40.6%
Clockwork mouse-hole 8.57 / 7.99 s 206.8 MiB 145.3 MiB 29.7%
Crossword pass-it-on 26.63 / 25.92 s 359.8 MiB 190.6 MiB 47.0%

These are measurements on one host rather than CI thresholds. They cover representative solved proofs; the multi-million-transition challenge cases still need author budget decisions and their own bounded runs.

Author CLI rollout

tools/solve.mjs now calls compact solveLevel() in fast mode (c5ec50e). The CLI tests cover pack and level selection, shortest route, replay, already won boards, repeated --forbid, an initially forbidden rule, a rule formed and sunk in one turn, existential BYPASS/HANDS-OFF flags, and both transition and retained-state limits. Mod loading succeeds for the shipped Word Lab pack and the Crate Works, Tidewater, and Clockwork drafts. The full Node suite at this checkpoint passes 269/269 and the production build passes.

The old CLI incremented explored before checking --max, so a LIMIT at cap N printed after N+1 states. The new search attempts exactly N transitions and prints after N states. --max-visited gives a separate explicit cap on retained frontier states and marks that LIMIT as (visited cap).

The committed CLI also completed authored heavy smokes under their documented caps: Crossword pass-it-on exited 0 in 25.3 s with its exact 25-step route, and Clockwork mouse-hole exited 0 in 8.1 s with its exact 23-step route. Neither reported BYPASS or HANDS-OFF. Word Lab's three proofs, Crate Works night-shift, Tidewater low-tide, and Clockwork mouse-keeps-time also retained their known routes. The last of these reports BYPASS and not HANDS-OFF under the agreed motion definitions; the worlds team has accepted separate allowBypass and allowHandsOff declarations for CI gating.

Browser acceptance after the fast engine and restore-cache changes passed on local Vite: automata.mjs covered movement, WAIT, Undo, and reset on desktop and mobile; rule-reading.mjs covered stacked words, DEFEAT-before-WIN, and a shared mobile proof; undo-death.mjs covered immediate and delayed Undo plus restored visual state. All three reported no console or page errors. The full Node suite, production build, mod loading, and strict OpenSpec validation also passed at this checkpoint.

Shell-game constraint investigation

The corrected CLI honored an explicit 3,000,000-attempt cap for Tidewater shell-game --forbid 'JELLY IS SHELL'; the search returned LIMIT in 223.47 s. That is inconclusive about the rule's necessity. A bounded 100,000-attempt audit found 50,417 authored-ID states and zero duplicates after grouping ordinary same-noun object positions. Interchangeable-ID quotienting would not reduce this observed frontier, and the engine has ID-based movement and automaton ordering that would require an equivariance proof before quotienting.

A lexical rule-target precheck is also too weak to resolve this proof soundly: the available words overapproximate alternate rules such as MIAU IS SHELL, JELLY IS WIN, and JELLY IS MIAU. Rule geometry, transformation order, control survival, and contact precedence would have to be modeled before it could conclude UNSOLVED. The mustForm field stays unset for this proof; no search-cap result is reported as an impossibility proof.