[lee-eojin]

Fixes #1931.

As in #1915, each demo gets a SPEC.bend beside LAWS.bend, with BOARD.bend's header. It holds every definition the laws' meaning needs, and LAWS.bend and PROOF.bend read them from there.

I named all three SPEC.bend since they play the same part in each demo, so the name says what the file is for. BOARD.bend keeps its name here.

demo	moved to SPEC.bend	main.bend
proof_insertion_sort	LE, Sorted.from, Sorted, bump, count	le_case and dec use Spec.LE
pure_par_sum	pow2, seq	sum uses Spec.pow2
pure_par_sort	sum	loses sum, nothing else

LE and pow2 move too: moving only Sorted, count and seq leaves the laws standing on definitions in main.bend, and an edit there still passes (the issue has both). The programs import them, so le_case now returns evidence of SPEC.bend's order, and sum splits its range with SPEC.bend's pow2. Those two SPEC.bend files say so in their header.

One choice is yours: pow2 is both part of what the law means (2^d numbers) and how sum splits its range. The other way is a copy of pow2 in SPEC.bend and a lemma Par.pow2(d) == Spec.pow2(d) in PROOF.bend, so the split stays the program's and only SPEC.bend reads the program, as in #1915, for one more induction. I'm happy to switch to that.

pure_par_sort's SPEC.bend reads Sort.Tree, the type the program sorts. Spec.sum checks only if a leaf is a Nat and a node a pair of trees, so a different Tree fails in SPEC.bend rather than changing what the sum means.

The proofs change only in names (Sort.LE to Spec.LE, Par.seq to Spec.seq, and so on). No checker, kernel, gate or other demo changes.

What I checked

On 4f99f4c, macOS arm64:

• bend PROOF.bend and bend PROOF.bend --verdict (Lean 4.34.0) print ALL PROOFS CHECK in each demo, and bend SPEC.bend checks.
• The programs print what they printed before: [1n, 2n, 3n] (interpreted and C), 2147450880 (C, on Metal and with +RTS --gpu off), sorted (C, on Metal and with +RTS --gpu off).
• The issue's edits now fail, each at its law. I ran them in throwaway copies, as Keep the flag law outside the editable game #1915 did, rather than adding attack demos to the tree:
  • pure_par_sort, mix returning x: expected Nat.add(Spec.sum(d, x), Spec.sum(d, y)), observed Nat.add(Spec.sum(d, x), Spec.sum(d, x)).
  • pure_par_sum, sum returning 0n, with or without its own pow2 returning 0n: expected 0n, observed Spec.seq(Spec.pow2(d), i).
  • proof_insertion_sort, sort returning xs, with or without its own LE as Unit: expected Spec.LE(lo, h), observed Unit.
• A def Spec.seq in main.bend or PROOF.bend is refused ("Spec is an import's alias"). A def SPEC.seq there is accepted, but the law still reads SPEC.bend's: with sum returning 0n it fails as above, and it checks only when SPEC.bend's own seq returns 0n.
• The changed and new files are in gates/repo.ts's allow list, and demos have no token cap. I couldn't run the gate itself here (no ttok).

Not run: the cluster gates, Linux.