[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 54 law files, no shared definition files and 4 lemma files (ArrayItemsRoundTrip, BoolCharStringFacts, CompareSelfEqual, InitializeResultShape), replacing the 2.4k-line LAWS.bend and 1.8k-line PROOF.bend.
  • All 54 are SPEC.md's guarantees, one per row.
  • Six laws that two guarantees cite sit in the guarantee that states them, and the other guarantee says so with an also rests on: line: line_blank and line_message in BlankLinesGetNothing, line_decoded in LinesDecodedAsUtf8, ran_id in RepliesCarryRequestId, took_status_200 in ClientReadsReplies, and web_post in RevisionFromVersionHeader.
• No requirement IDs.
  • SPEC.md's source notes (the three revisions, how sections are cited, what differs between revisions, the pure modules, the departure from schema.json) now head LAWS.bend, which also names the first file of each family.
  • Each section's intro heads that family's first file. The OpenAPI citation notes are in laws/OperationsFromPaths.bend.
  • The "left to prove" note for UTF-8 decoding is in laws/LinesDecodedAsUtf8.bend, which says it is pending.
  • IDs cited in src/, main.bend and the README are now law paths or (trusted in src/io.bend).
  • The table itself is kept as docs/SPEC.md, along with its Not implemented list. LAWS.bend and the README point to it.
• Trust boundary, now # Trusted, not proved: comments on the code, or cites of the dependency's law files:
  • MCP-TRUST-1 (IO sequencing) goes on the src/io.bend header.
  • MCP-TRUST-2 (ezhttp) goes on the src/io.bend header too. It cites ezhttp's laws/BadRequestAnswers400.bend, laws/WithServesGetOctetsAndContext.bend, laws/FieldLookupIgnoresCase.bend, laws/DeadlineIsTimeout.bend and laws/OctetsDecodeAsUtf8.bend. Forking and max are cited as trusted in ezhttp's src/server.bend.
  • MCP-TRUST-3 (ezjson) is cited in laws/MessagesWrittenAsLines.bend (ezjson's laws/QuoteEscapesExactly.bend and laws/PrintIsCompactAndStable.bend) and in laws/UnparsedTextIsParseError.bend (ezjson's laws/ParsesExactlyJsonTexts.bend). The old row claimed ezjson proves a compact print of every well-formed value. ezjson proves that only for the print of a parsed value, so for values ezmcp builds, "no newline" is now stated as trusted.
  • MCP-TRUST-4 (the runner validates its inputs) goes on main.bend's "what a runner answers" section.
  • MCP-TRUST-5 (the stdin effect, and Base's write and print_err) goes on ezmcp.stdin in src/io.bend.
• Helpers: one proof helper no proof reached (eq.or_true) is dropped.
• bolt.bend drops def trace().

Depends on

• feat!: one guarantee per file under laws/ and proofs/; drop trace and SPEC.md 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.
• The cited law files of ezjson and ezhttp exist once refactor: one file per guarantee under laws/ and proofs/ ezjson#87 and refactor: one file per guarantee under laws/ and proofs/ ezhttp#64 land. The pins in ez.lock.toml are unchanged.

Test plan

• bend PROOF.bend → ALL PROOFS CHECK
• Lint with bolt from #257: 40 errors, 0 warnings. All 40 are S005 stale # noqa: L001 (all in examples/), which main also shows under that bolt. Main has 41 errors there; the extra one is the C011 for def trace().
• Bump the bolt pin after the release, then nix flake check

🤖 Generated with Claude Code