1# W3 verification ledger23The compact codec, parent-linked breadth-first core, public fallback adapter,4and fast engine transition are committed independently. This ledger separates5mechanical parity from solver rollout and world performance claims.67## State and turn parity89- Codec round trips preserve the next direct-engine event and settled state10 after noun chains, automaton waits, SINK removal, and word-rule edits.11- Thirteen focused fast-turn tests compare `stepFast()` and `waitFast()` with12 public `step()` and `wait()` across stacked rules, PUSH/STOP, DEFEAT/WIN,13 transformations, SINK removal, Clockwork phases, word-motion provenance,14 blocked input, and parser-budget rollback. Fast transitions add no Undo15 entry.16- A temporary differential script took up to 32 deterministic movement actions17 on each of 30 available core and draft-world levels, adding waits on18 automata levels. It found zero mismatches in acceptance or settled state.19- Ten exact baseline routes across core, Word Lab, Crossword, Crate Works,20 Tidewater, and Clockwork contributed 150 actions with zero mismatches after21 every action. The comparison included objects, nouns, rules, sentence spans,22 automata phases, and win state.2324At this checkpoint the full Node suite passed 260/260 and `npm run build`25passed. The world author CLI has not yet switched to the compact solver, so26the baseline routes and memory figures remain the pre-rollout comparison.2728## Compact solver comparison before CLI rollout2930The committed `solveLevel()` adapter was run in separate processes with both31public and fast engine transitions at the same proof caps used in the baseline.32All ten proofs returned the **exact baseline action strings**, and both modes33attempted and expanded the same number of states for each proof. Elapsed time34for the larger searches was:3536| Proof | Public transition | Fast transition | Attempts / expanded |37| --- | ---: | ---: | ---: |38| Core `break-the-rule` | 4.5 s | 3.8 s | 46,792 / 11,698 |39| Crate Works `night-shift` | 1.02 s | 0.83 s | 4,636 / 1,159 |40| Clockwork `mouse-hole` | 9.8 s | 8.0 s | 61,323 / 12,265 |41| Crossword `pass-it-on` | 31.2 s | 26.1 s | 290,092 / 72,523 |4243The smaller core, Word Lab, and Tidewater proofs also matched their exact44routes and counts; fast mode was no slower in this run. Timing is descriptive,45not a CI threshold. A separate 20 ms in-process RSS sampler measured fast-mode46peaks of **149.0 MiB** for `break-the-rule`, **145.3 MiB** for `mouse-hole`, and47**190.6 MiB** for `pass-it-on`. Those runs included the normal shortest-path48search only. The pre-W3 whole-command baseline also includes a BYPASS49re-search, so its peak RSS is not a direct one-to-one memory comparison.5051For a direct memory comparison, the temporary legacy CLI copy was run again52with only its normal shortest-path search; BYPASS re-search was disabled in53that temporary copy. A 20 ms worker-thread RSS sampler measured each process54under the same proof cap. Routes and search counts were identical to fast55mode:5657| Proof | Legacy / fast elapsed | Legacy full-state RSS | Compact fast RSS | Reduction |58| --- | ---: | ---: | ---: | ---: |59| Core `break-the-rule` | 6.38 / 3.75 s | 251.0 MiB | 149.0 MiB | 40.6% |60| Clockwork `mouse-hole` | 8.57 / 7.99 s | 206.8 MiB | 145.3 MiB | 29.7% |61| Crossword `pass-it-on` | 26.63 / 25.92 s | 359.8 MiB | 190.6 MiB | 47.0% |6263These are measurements on one host rather than CI thresholds. They cover64representative solved proofs; the multi-million-transition challenge cases65still need author budget decisions and their own bounded runs.6667## Author CLI rollout6869`tools/solve.mjs` now calls compact `solveLevel()` in fast mode (`c5ec50e`).70The CLI tests cover pack and level selection, shortest route, replay, already71won boards, repeated `--forbid`, an initially forbidden rule, a rule formed72and sunk in one turn, existential BYPASS/HANDS-OFF flags, and both transition73and retained-state limits. Mod loading succeeds for the shipped Word Lab pack74and the Crate Works, Tidewater, and Clockwork drafts. The full Node suite at75this checkpoint passes 269/269 and the production build passes.7677The old CLI incremented `explored` before checking `--max`, so a LIMIT at cap78`N` printed `after N+1 states`. The new search attempts exactly `N` transitions79and prints `after N states`. `--max-visited` gives a separate explicit cap on80retained frontier states and marks that LIMIT as `(visited cap)`.8182The committed CLI also completed authored heavy smokes under their documented83caps: Crossword `pass-it-on` exited 0 in 25.3 s with its exact 25-step route,84and Clockwork `mouse-hole` exited 0 in 8.1 s with its exact 23-step route.85Neither reported BYPASS or HANDS-OFF. Word Lab's three proofs, Crate Works86`night-shift`, Tidewater `low-tide`, and Clockwork `mouse-keeps-time` also87retained their known routes. The last of these reports BYPASS and not88HANDS-OFF under the agreed motion definitions; the worlds team has accepted89separate `allowBypass` and `allowHandsOff` declarations for CI gating.9091Browser acceptance after the fast engine and restore-cache changes passed on92local Vite: `automata.mjs` covered movement, WAIT, Undo, and reset on desktop93and mobile; `rule-reading.mjs` covered stacked words, DEFEAT-before-WIN, and a94shared mobile proof; `undo-death.mjs` covered immediate and delayed Undo plus95restored visual state. All three reported no console or page errors. The full96Node suite, production build, mod loading, and strict OpenSpec validation also97passed at this checkpoint.9899## Shell-game constraint investigation100101The corrected CLI honored an explicit 3,000,000-attempt cap for Tidewater102`shell-game --forbid 'JELLY IS SHELL'`; the search returned `LIMIT` in 223.47 s.103That is inconclusive about the rule's necessity. A bounded 100,000-attempt104audit found 50,417 authored-ID states and **zero** duplicates after grouping105ordinary same-noun object positions. Interchangeable-ID quotienting would not106reduce this observed frontier, and the engine has ID-based movement and107automaton ordering that would require an equivariance proof before quotienting.108109A lexical rule-target precheck is also too weak to resolve this proof soundly:110the available words overapproximate alternate rules such as `MIAU IS SHELL`,111`JELLY IS WIN`, and `JELLY IS MIAU`. Rule geometry, transformation order,112control survival, and contact precedence would have to be modeled before it113could conclude UNSOLVED. The `mustForm` field stays unset for this proof; no114search-cap result is reported as an impossibility proof.