chore: coverage at error, the audit folded into the RFC

[ngngardner]

This finishes the RFC's phase four: the rollout is done.

coverage (L001) at error

bolt now reports clean, down from 30 warnings. Each warning was handled one of three ways.

Code no law applies to gets # noqa: L001 <why> on its def line (as the maintainer approved):

• the builders sub, flag, opt, many, pos, rest, in main.bend and src/cli.bend: a law could only restate the constructor, and the rollout deleted exactly those definitional laws;
• main.bend's type aliases Sub, Arg, SpecErr;
• proof machinery: the lemma proofs in src/eq.bend, and binds_of, Moved and Went in src/grow.bend;
• the example program's spec and text.

A real law for the report texts of check: spec_err_where says every report's text opens with where it is (spec: , or the command's path). It is proved by cases, and a report that drops its location fails the gate.

Deleted: show and its helpers. Nothing used them; they existed for the laws the rollout deleted.

bolt.bend's comment now says what a noqa must carry.

The inventory is folded into the RFC

docs/rfc/shake-spec.md now carries:

• State: Accepted and implemented.
• Rollout: every phase marked done, plus a short record of what each phase landed.
• An appendix with the audit: the method, the numbers, and a table of the findings F1–F13, each with what became of it.

docs/rfc/shake-law-inventory.md is deleted; its law-by-law tables stay in git at 72fd9a5. SPEC.md's link now points at the RFC.

Checks

• The gate prints All terms check.
• bolt reports clean.
• SPEC rows and tags agree.
• The demo builds and runs.

There is no behavior change.

🤖 Generated with Claude Code

https://claude.ai/code/session_01G7DgqW3jVEg2yWGQDayFaU

---

Generated by Claude Code