[lee-eojin]

Fixes #2066.

SPEC.bend holds what LAWS.bend measures: steps (n ticks, each one Slash.Game.step), fade (n ticks of a countdown, with a dec of its own) and cat (a frame's events joined). It has the header the other demos' spec files use. LAWS.bend and PROOF.bend import it and name Spec.steps, Spec.fade and Spec.cat; the laws and the proofs are otherwise unchanged. main.bend loses its # Spec section, which only those two files used, as #1932 did for pure_par_sort and pure_par_sum.

SPEC.bend imports main.bend only for Game.step and the game's types, as the SPEC.bend of pure_par_sort and the BOARD.bend of app_win_is_bug_2d do. fade counts with its own dec, the body of Sim.dec (as pure_par_sum's SPEC.bend keeps its own pow2 since 1570e07), so an edit to Sim.dec can't move the measure. The checker unfolds both countdowns to the same R.word, so the proofs didn't change beyond the names. cat is its own append.

What it leaves, as the issue says: the laws pin Game.step, not the loop that runs it.

Before and after

The same edits on main and on this branch, with bend PROOF.bend and bend PROOF.bend --verdict (Lean 4.34.0) giving the same answer in each cell:

	main at ae7341d	this branch
the issue's edit (a paused clock runs, the measure and PROOF.bend edited to match)	ALL PROOFS CHECK	SOME PROOFS FAIL at Laws.pause_freezes
Sim.dec gives 6 for 7 and 0 for anything else, which dec_floor still accepts	ALL PROOFS CHECK	SOME PROOFS FAIL at Laws.pause_freezes
nothing edited	ALL PROOFS CHECK	ALL PROOFS CHECK

On this branch the measure lives in SPEC.bend, so the first row applies only the bug and the PROOF.bend edit. The bug is in the game on both sides, so the issue's CHECK.bend prints after 3 ticks: time 3 on both; unedited, it prints time 0 on both.

What I checked

On ae7341d, macOS arm64:

• bend main.bend --check-only, bend main.bend --verdict and bend SPEC.bend --check-only print ALL PROOFS CHECK. bend LAWS.bend alone reports 7 TODOs, as on main.
• Moving only the loop to another stepper still checks, which is the limit above.
• bend main.bend -o builds, and SLASH_PROBE=120 runs headless and exits 0. The loop is unchanged, so I didn't open the window.
• Every other demo's PROOF.bend prints what it prints on main: ALL PROOFS CHECK, except pure_hvm5_mini, kept @unsafe in bend PROOF.bend fails on four unedited demos: their main.bend holds @unsafe defs that no law uses #1989.

repo-gate passes in CI. Not run: the cluster gates, Linux.

[Lorenzobattistela]

Thanks, this does what it says: on d2f4705 bend PROOF.bend and --verdict print ALL PROOFS CHECK, SPEC.bend --check-only checks, and safe on tests shows no false rejects. A few small things that fit in this PR:

1. dec_floor (LAWS.bend:70) still checks Slash.Sim.dec, not Spec.dec, so the floor law and the measure are about two different countdowns. Your second row (Sim.dec gives 6 for 7 and 0 otherwise) is caught only because Game.step happens to fade the flash with Sim.dec. If the flash fades some other way, a broken Sim.dec passes every law. Could you either point dec_floor at Spec.dec, or add a law {Slash.Sim.dec(x) == Spec.dec(x) : U32} so the two copies can't drift apart?

2. README.md (the Laws paragraph, line 17) names only LAWS.bend and PROOF.bend. Please mention SPEC.bend there too, and that it stays unchanged along with LAWS.bend, as the other demos with spec files do.

3. The deleted # Spec section in main.bend had the only note that the measured n ticks are the ones the loop's Live.steps runs. Could steps in SPEC.bend keep that line ("n ticks of the game, as the loop's Live.steps runs them")? Then the limit you describe stays visible to someone editing the loop.

Not for this PR, but worth an issue: the laws still pin Game.step rather than Live.steps, as you note, and esc_quits, pause_twice, back_to_title, pause_toggles and arrows_are_wasd are stated only through functions in main.bend. For example, a Game.events that always returns None{} makes esc_quits hold with a {==} proof.