- commit
- 3b357e14a85b18ad7273048691fb7142965cc80f
- parent
- e45f38ca3ecbc30f54225f5a17861332d6d1bd8c
- author
- Dami <dami.etoile@gmail.com>
| M | docs/ | 33 | +++++++++++++++++++++ |
| M | tests/ | 44 | ++++++++++++++++++++++++++++ |
| M | tools/ | 48 | +++++++++++++++++++++++++++--- |
@@ -175,6 +175,39 @@ Together with the core pack, these provide nine verified level proofs. The
175175 tests load each CommonJS file, create an engine game from every level, and176176 replay a concrete winning intent sequence.177177 178+## Checking proofs with the author solver179+180+The author CLI runs the same movement, rule, automaton, and contact phases as181+play while keeping compact states in its search frontier:182+183+```sh184+node tools/solve.mjs core185+node tools/solve.mjs mods/word-lab.cjs --level rules-are-cargo --max 5000186+node tools/solve.mjs mods/word-lab.cjs --level rules-are-cargo --replay RRRRRRR187+node tools/solve.mjs mods/worlds/crossword.cjs --level pass-it-on --forbid "ROCK IS WIN"188+```189+190+`--max` limits attempted actions; `--max-visited` separately limits retained191+frontier states. A `LIMIT` result means the cap was reached, not that the proof192+is unsolvable. Without `--max`, a proof's optional `solverBudget` sets its cap;193+otherwise the default is 2,000,000 attempts. An explicit `--max` overrides194+both. `--forbid` can be repeated and excludes a rule if it was active195+initially or at any rule-reading phase within a turn, even if it disappears196+before settlement. Replay prints each board using the public engine path.197+198+The CLI runs separate constrained searches for its current flags. `BYPASS`199+means a win exists without the player pushing a word; `HANDS-OFF` means a win200+exists with no word motion from either player or automata. A route's own201+classification does not establish whether another route has either property.202+World authors can declare optional `solverBudget`, `allowBypass`,203+`allowHandsOff`, and `mustForm` fields on a proof. `solverBudget` is a positive204+integer. The two `allow` booleans silence the corresponding warning when an205+unusual route is intentional. `mustForm: ['ROCK IS WIN']` asks the CLI to find206+any winning route that never uses that rule. A found route prints207+`SKIPPABLE(ROCK IS WIN)` and fails; a capped search prints `LIMIT(ROCK IS WIN)`208+and also fails because necessity remains unproven. The bundled-world CI gate209+is being integrated with the worlds team's authored budgets.210+178211 ## Pack service and sharing179212 180213 `src/pack-service.js` provides the presentation-independent pack operations:@@ -62,6 +62,11 @@ const transientPack = `module.exports = {
6262 ] }],6363 };`;6464 65+const metadataPack = simplePack.replace(66+ "id: 'walk', width",67+ "id: 'walk', allowBypass: true, allowHandsOff: true, mustForm: ['MIAU IS WIN'], solverBudget: 100, width",68+);69+6570 test('CLI preserves pack and level selection, route output, and replay', () => {6671 const pack = fixture(simplePack);6772 try {@@ -127,3 +132,42 @@ test('CLI forbid checks a transient formed then sunk rule', () => {
127132 pack.cleanup();128133 }129134 });135+136+test('CLI applies solverBudget and mustForm metadata while suppressing allowed warnings', () => {137+ const pack = fixture(metadataPack);138+ try {139+ const result = run([pack.file, '--level', 'walk']);140+ assert.equal(result.status, 1);141+ assert.match(result.stdout, /BYPASS\(3: RRR\)/);142+ assert.match(result.stdout, /HANDS-OFF\(3: RRR\)/);143+ assert.match(result.stdout, /SKIPPABLE\(MIAU IS WIN\)/);144+ assert.doesNotMatch(result.stdout, /WARNING:/);145+ } finally {146+ pack.cleanup();147+ }148+});149+150+test('CLI fails and labels a mustForm search that reaches its budget', () => {151+ const pack = fixture(metadataPack.replace('solverBudget: 100', 'solverBudget: 1'));152+ try {153+ const result = run([pack.file, '--level', 'walk']);154+ assert.equal(result.status, 1);155+ assert.match(result.stdout, /LIMIT\s+after 1 states/);156+ assert.match(result.stdout, /LIMIT\(MIAU IS WIN\)/);157+ } finally {158+ pack.cleanup();159+ }160+});161+162+test('explicit --max overrides a lower solverBudget', () => {163+ const pack = fixture(metadataPack.replace('solverBudget: 100', 'solverBudget: 1'));164+ try {165+ const result = run([pack.file, '--level', 'walk', '--max', '100']);166+ assert.equal(result.status, 1);167+ assert.match(result.stdout, /SOLVED\s+3 steps\s+RRR/);168+ assert.match(result.stdout, /SKIPPABLE\(MIAU IS WIN\)/);169+ assert.doesNotMatch(result.stdout, /LIMIT\(MIAU IS WIN\)/);170+ } finally {171+ pack.cleanup();172+ }173+});@@ -30,7 +30,11 @@ for (let index = 0; index < args.length; index += 1) {
3030 }3131 const opt = name => options.get(name)?.[0];3232 const file = positionals[0];33-const MAX = Number(opt('max') ?? 300000);33+// An explicit --max is the author/CI invocation override. Without it, a level34+// solverBudget overrides the default budget for that proof.35+const DEFAULT_BUDGET = 2_000_000;36+const maxOption = opt('max');37+const MAX = Number(maxOption ?? DEFAULT_BUDGET);3438 if (!Number.isInteger(MAX) || MAX < 1 || MAX > 50000000) { console.error('--max must be an integer from 1 to 50000000'); process.exit(2); }3539 const maxVisited = opt('max-visited') === undefined ? Infinity : Number(opt('max-visited'));3640 if (maxVisited !== Infinity && (!Number.isInteger(maxVisited) || maxVisited < 1 || maxVisited > 50000000)) { console.error('--max-visited must be an integer from 1 to 50000000'); process.exit(2); }@@ -78,14 +82,30 @@ let bad = 0;
7882 console.log(`${mod.manifest.name} (${mod.manifest.id}), ${mod.levels.length} levels`);7983 for (const level of mod.levels) {8084 if (only && level.id !== only) continue;81- const result = solveLevel(level, { cap: MAX, maxVisited, forbid, transitionMode: 'fast' });85+ const metadataErrors = [];86+ if (level.solverBudget !== undefined && (!Number.isSafeInteger(level.solverBudget) || level.solverBudget < 1)) {87+ metadataErrors.push('solverBudget must be a positive integer');88+ }89+ if (level.allowBypass !== undefined && typeof level.allowBypass !== 'boolean') metadataErrors.push('allowBypass must be boolean');90+ if (level.allowHandsOff !== undefined && typeof level.allowHandsOff !== 'boolean') metadataErrors.push('allowHandsOff must be boolean');91+ if (level.mustForm !== undefined && (!Array.isArray(level.mustForm) || level.mustForm.some(rule => typeof rule !== 'string' || !rule.trim()))) {92+ metadataErrors.push('mustForm must be an array of non-empty rule texts');93+ }94+ if (metadataErrors.length) {95+ bad++;96+ console.error(` ${(level.id || '?').padEnd(28)} INVALID ${metadataErrors.join('; ')}`);97+ continue;98+ }99+ const cap = maxOption === undefined ? (level.solverBudget ?? DEFAULT_BUDGET) : MAX;100+ const result = solveLevel(level, { cap, maxVisited, forbid, transitionMode: 'fast' });82101 const flags = [];102+ const warnings = [];83103 if (result.status === 'SOLVED') {84104 if (result.path.length === 0) flags.push('WON-AT-START');85105 else if (result.path.length < 6) flags.push('TRIVIAL');86106 const bypass = result.routeBypass87107 ? result88- : solveLevel(level, { cap: MAX, maxVisited, forbid, transitionMode: 'fast', wordMotion: 'player' });108+ : solveLevel(level, { cap, maxVisited, forbid, transitionMode: 'fast', wordMotion: 'player' });89109 if (bypass.status === 'SOLVED') flags.push(`BYPASS(${bypass.path.length}: ${bypass.path})`);90110 const handsOff = result.routeHandsOff91111 ? result@@ -93,10 +113,28 @@ for (const level of mod.levels) {
93113 ? bypass94114 : bypass.status === 'UNSOLVED'95115 ? bypass96- : solveLevel(level, { cap: MAX, maxVisited, forbid, transitionMode: 'fast', wordMotion: 'all' });116+ : solveLevel(level, { cap, maxVisited, forbid, transitionMode: 'fast', wordMotion: 'all' });97117 if (handsOff.status === 'SOLVED') flags.push(`HANDS-OFF(${handsOff.path.length}: ${handsOff.path})`);118+ if (bypass.status === 'LIMIT') {119+ warnings.push(`BYPASS search LIMIT after ${bypass.explored} states (unproven)`);120+ bad++;121+ } else if (bypass.status === 'SOLVED' && !level.allowBypass) warnings.push('BYPASS not allowed (set allowBypass: true if intended)');122+ if (handsOff.status === 'LIMIT') {123+ warnings.push(`HANDS-OFF search LIMIT after ${handsOff.explored} states (unproven)`);124+ bad++;125+ } else if (handsOff.status === 'SOLVED' && !level.allowHandsOff) warnings.push('HANDS-OFF not allowed (set allowHandsOff: true if intended)');98126 } else bad++;127+ for (const rule of level.mustForm || []) {128+ const required = solveLevel(level, { cap, maxVisited, forbid: rule, transitionMode: 'fast' });129+ if (required.status === 'SOLVED') {130+ flags.push(`SKIPPABLE(${rule})`);131+ bad++;132+ } else if (required.status === 'LIMIT') {133+ flags.push(`LIMIT(${rule})`);134+ bad++;135+ }136+ }99137 const detail = result.status === 'SOLVED' ? `${result.path.length} steps ${result.path}` : `after ${result.explored} states${result.limitReason === 'visited' ? ' (visited cap)' : ''}`;100- console.log(` ${(level.id || '?').padEnd(28)} ${result.status.padEnd(8)} ${detail}${flags.length ? ` ${flags.join(' ')}` : ''}`);138+ console.log(` ${(level.id || '?').padEnd(28)} ${result.status.padEnd(8)} ${detail}${flags.length ? ` ${flags.join(' ')}` : ''}${warnings.length ? ` WARNING: ${warnings.join('; ')}` : ''}`);101139 }102140 process.exit(bad ? 1 : 0);