[ngngardner]

Summary

• One file per guarantee. Each guarantee is laws/<Name>.bend (its prose, then its quantified laws), proved by proofs/<Name>.bend. LAWS.bend and PROOF.bend only import them. That's 22 law files, 6 shared definition files and 16 lemma files, replacing the 3.4k-line LAWS.bend, the 6.4k-line PROOF.bend and the fifteen proof/wp*.bend lemma modules.
• proof/ folded in. Its lemmas are placed by the files that use them, like any other proof helper. 14 identical copies of a lemma across modules are kept once; where two modules gave different lemmas the same name (42 names), the later one takes its module's topic as a prefix (ras.add_zero, huf.fl).
• No requirement IDs.
  • SPEC.md's definitions (well formed, sample) and the section scopes now head LAWS.bend.
  • png_walk_anc, which two rows cited, is its own guarantee: laws/PngAncillaryChunksIgnored.bend.
  • The table itself is kept as docs/SPEC.md, since the RFCs cite its IDs.
• Trust boundary.
  • Dropped: the checker's soundness and the gate runner, which hold for every Bend project.
  • Other encoders' DEFLATE streams are now trusted in a comment on src/inflate.bend's header, other encoders' JPEGs on src/jpeg.bend's header, the T.871 conversion on Jpeg.rgb, and the JPEG round trip's within-8 bound on encode_jpeg in main.bend.
• Helpers: 8 proof helpers that no proof reached are gone.
• bolt.bend drops def trace().

Depends on

Emerging-Patterns/bolt#257. The pinned bolt reads law files by name only and still runs trace. This PR stays a draft until that release lands and the pin is bumped here.

Test plan

• bend PROOF.bend → ALL PROOFS CHECK (about 50 s, same as main)
• Lint with bolt from #257: 0 errors, 3 warnings (the L001 coverage warnings on main.bend, which main also shows). Main has 1 error under that bolt, the C011 for def trace().
• Bump the bolt pin after the release, then nix flake check

🤖 Generated with Claude Code