feat(rules): unsafe reaches foreign defs, fuel sees U32.to_nat, bend 2.0.34 text

[noah-emp]

Brings three rules up to bend 2.0.32–2.0.34.

unsafe (L003, BOLT-LAW-3)

Since 2.0.32 a proof fails (SOME PROOFS FAIL, then Error: N defs rely on unsafe or foreign code:, exit 1) when any def it loads is @unsafe or foreign, whether or not a law names that def. The rule used to catch only @unsafe. Now it also reports a foreign def (a body of only import "./x.c" / import "./x.js" lines, the shape rule foreign already reads) that a LAWS.bend or PROOF.bend reaches through relative imports. The message names the shortest import path from the law file (LAWS.bend -> mid.bend -> eff/io.bend, from the new Imports.trail BFS) and says to move the effect into a sibling module no law file imports. The header rationale is rewritten for 2.0.34.

• Digest.Unsafe gets a foreign: Bool field, and Digest.of appends the file's top-level foreign defs.
• Hash imports (import 0x…/path through BEND_LIB) are not followed. bolt reads only the files in the run. Following them would mean new planner asks for .ez/lib/<hash>/… files and reading BEND_LIB, plus changes to the planner's laws. That is left for a follow-up.

fuel (U006, BOLT-RULE-U006)

U32.to_nat(<U32 literal>) passed as a fuel argument is now reported the same way a Nat literal is. Let-bound and parenthesized literals are still out of scope. The rationale is updated: 2.0.29 made recursion on a Nat literal linear (#983), so the checker no longer hangs. On 2.0.33/2.0.34, though, a lemma proved over every fuel and then used at a big fixed fuel overflows the checker's stack. bolt's own two IO read loops (src/lsp/files/disk.bend, src/lsp/transport/stdio.bend) now carry a noqa: U006 with the reason.

hole

The header now quotes bend's 1 TODO found. / N TODOs found., printed under SOME PROOFS FAIL with exit 1. The stale All terms check. quotes in AGENTS.md and docs/rfc/bolt-spec.md now say ALL PROOFS CHECK.

Verification

• Every PROOF.bend prints ALL PROOFS CHECK on bend 2.0.34.
• nix flake check -L passes (0 errors, 73 warnings, the same L001 warnings as main).
• A binary built from this branch finds no L003 in ezaudio, ezhttp, snap or ez.
• The wider fuel rule adds new U006 findings: 1 in snap and 15 in ez. Every one is a U32.to_nat(N) bound on an IO/walk loop, and those repos grade U006 as an error.

🤖 Generated with Claude Code