[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 270 law files, 2 shared definition files and 7 lemma files, replacing the 5.5k-line LAWS.bend and 6.5k-line PROOF.bend.
  • 61 files are SPEC.md's guarantees.
  • 6 hold a law two guarantees rest on, named for what it says (PhraseTableLookup, InterimStatusIs1xx, LocationResolvedBySort, LocationSplitsAtQuery, SplitAtCharacter, CutAtFirstEquals). The guarantees that rest on them say so with an also rests on: line.
  • 203 are the laws SPEC.md never inventoried (URL parsing, framing, credentials, the cookie jar, caching, CORS). Each has a file of its own, named for what its law states (Base64EncodesF, NoStoreNeverFresh, UrlPathIsAbsolute, ...), with no prose. LAWS.bend's header says they promise nothing beyond their equality.
• No requirement IDs.
  • SPEC.md's definitions (proved, pending, the gate) now head LAWS.bend, which also names the first file of each family.
  • Each section's intro heads that family's first file (e.g. laws/BadRequestAnswers400.bend for the server).
  • The "left to prove" note for the percent-encoding frame is in laws/QuoteOutputIsFramed.bend.
  • IDs cited in src/, main.bend, bench/ and the README are now law paths.
  • The table itself is kept as docs/SPEC.md.
• Trust boundary, now # Trusted, not proved: comments on the code:
  • HTTP-TRUST-1 (Base TCP and recv) and HTTP-TRUST-2 (server sequencing) go on the src/server.bend header.
  • HTTP-TRUST-3 (bend-kit wire, dns and bytes) goes on the src/wire.bend header.
  • HTTP-TRUST-4 goes on client.follow, and HTTP-TRUST-5 (client sequencing) on the src/client.bend header.
  • HTTP-TRUST-6 (errno reporting) goes on wire.fail in src/wirespec.bend.
  • HTTP-TRUST-7 (entities table) goes on the src/entities.bend header, which tools/entities.py now writes. It says the table is generated from WHATWG's entities.json. It drops SPEC.md's claim of a differential test against html.unescape, since no such test exists in the tree, CI or history.
  • HTTP-TRUST-8 goes on form.body, and HTTP-TRUST-9 on the src/packed.bend header.
• Helpers: no proof helper or law def was unreachable, so none were dropped.
• 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
• Lint with bolt from #257: 3 errors, 1007 warnings. The errors are the S005 stale # noqa in bench/main.bend, which main also shows under that bolt (4 errors, 1007 warnings there: main also has a C011 for def trace()).
• Bump the bolt pin after the release, then nix flake check

🤖 Generated with Claude Code