Emerging-Patterns · noah-emp · Sep 30, 2026 · Sep 30, 2026
diff --git a/AGENTS.md b/AGENTS.md
@@ -26,8 +26,8 @@ A `#|` equality for a proveable claim is a bug. A directory with
 
 - A `LAWS.bend` is human-owned: do not edit it to make a proof pass. Every
   law is quantified; `closed` reports one that is not.
-- Every `PROOF.bend` in the tree is gated (`bend PROOF.bend` prints "All
-  terms check."), so a fixture holding a proof meant to fail cannot live here.
+- Every `PROOF.bend` in the tree is gated (`bend PROOF.bend` prints `ALL
+  PROOFS CHECK`), so a fixture holding a proof meant to fail cannot live here.
 - Anything under a `tests/` directory is a test, and only the stay list may
   have one; `ez test` runs each on its own and caches none. Fixtures a test
   reads are not tests, so they live beside it -- `src/lsp/fixtures/`, not

diff --git a/SPEC.md b/SPEC.md
@@ -37,7 +37,7 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n
 | BOLT-RULE-U002 | `strict` reports exactly a self-call inside `Bool.and` or `Bool.or`, or in a comma-separated stretch holding `&&` or `\|\|` (matched by that exact text), where a `=>` ends the stretch on its left and a lambda body counts only by its own `&&` or `\|\|`. | Proved | proved | src/rules/LAWS.bend strict_walk_counts; src/rules/LAWS.bend strict_counts |
 | BOLT-RULE-U003 | `eager` reports exactly a looping def of the file called in a `Bool.pick` branch. | Proved | proved | src/rules/LAWS.bend eager_counts; src/rules/LAWS.bend eager_lambda; src/rules/LAWS.bend eager_comma; src/rules/LAWS.bend eager_plain |
 | BOLT-RULE-U004 | `concat` reports exactly a self-call argument that appends onto the parameter in its own position: the append written as the argument, inside any number of parentheses, or a lone name whose nearest `q = ..` or `+q = ..` let before the call, in its statement chain or an enclosing one, has such an append as its right side. | Proved | proved | src/rules/LAWS.bend concat_counts; src/rules/LAWS.bend concat_paren; src/rules/LAWS.bend concat_in_place; src/rules/LAWS.bend concat_via; src/rules/LAWS.bend concat_nearest; src/rules/LAWS.bend concat_other; src/rules/LAWS.bend concat_scope; src/rules/LAWS.bend concat_bound; src/rules/LAWS.bend concat_bound_plus |
-| BOLT-RULE-U006 | `fuel` reports exactly an argument that is one Nat literal token alone, in a call (not a self-call) to a def of the file, at a parameter named `fuel`, `gas`, `steps` or `budget` or starting with `fuel`. | Proved | proved | src/rules/LAWS.bend fuel_slots; src/rules/LAWS.bend fuel_walk_counts; src/rules/LAWS.bend fuel_counts |
+| BOLT-RULE-U006 | `fuel` reports exactly an argument that is one Nat literal token alone, or the dotted name `U32.to_nat` then a `(` group holding one U32 literal token (digits) alone, in a call (not a self-call) to a def of the file, at a parameter named `fuel`, `gas`, `steps` or `budget` or starting with `fuel`. | Proved | proved | src/rules/LAWS.bend fuel_slots; src/rules/LAWS.bend fuel_walk_counts; src/rules/LAWS.bend fuel_counts |
 | BOLT-RULE-U007 | `index` reports exactly a `List.get` or `String.get` at a non-literal index anywhere in a recursive def, except a `List.get` on a fixed table that `table` reports. | Proved | proved | src/rules/LAWS.bend index_counts |
 | BOLT-RULE-U008 | `table` reports exactly, in a def that calls itself, a `List.get` or `List.set` call whose index is not one number token and whose list is a fixed table: a list literal, a number-sized array, or `List.replicate` / `Array.new` / `List.range` with a number count, written inline, as a table def of the file, or held by the let of that name in scope. | Proved | proved | src/rules/LAWS.bend table_walk_counts; src/rules/LAWS.bend table_counts |
 | BOLT-RULE-U009 | `hoist` reports exactly, in a def that calls itself and is not a law or a proof, outside a lambda's body (the rest of a chain after `=>`), a case pattern, and a case arm that does not call the def: a `List.get`, `List.set`, `String.get`, `Array.get` or `Array.set` call whose collection is a table, and a let of one plain name to a table that a later get, set or `name[..]` in its block or the statements after it indexes; where a table is a list literal with eight or more top-level commas, an array literal of more than eight slots (`[v : T*n]` with n not a literal 0 to 8, `[v : T^d]` with d not a literal 0 to 3), a `List.replicate`, `Array.new` or `List.range` whose count is not a literal 0 to 8, a `List.map` or `Array.map`, or a call to a def of the file, other than an undotted self-call, whose body is a single statement that is a list literal, or an array literal, `List.replicate`, `Array.new` or `List.range` sized by a number literal, of more than eight cells by those measures; and every value name in the table (a callee or a `~` template aside) is a parameter that each self-call passes back unchanged in its own position. | Proved | proved | src/rules/LAWS.bend hoist_counts |
@@ -59,7 +59,7 @@ A tag may name a proved or a pending requirement, never a Trusted one or an ID n
 | :---- | :---- | :---- | :---- | :---- |
 | BOLT-LAW-1 | In every file under a law directory, except helpers, law files and tests, every def and type is named by a quantified law in a LAWS.bend or reached from one through calls. A quantified law names an item by a use in its statement that the binder (BOLT-SYN-5) resolves to that item, through an import alias or in the same file; a def calls an item by such a use on its own lines. A def is covered when such a law names it or a covered def calls it, in its own file or in another file of the run; a type is covered when such a law or a covered def names it or one of its constructors. | Proved | proved | src/rules/LAWS.bend coverage_reach; src/rules/LAWS.bend reach_from; src/rules/LAWS.bend reach_shut; src/rules/LAWS.bend reach_least; src/rules/LAWS.bend reach_digest; src/rules/LAWS.bend reach_binder |
 | BOLT-LAW-2 | `closed` reports any law in a LAWS.bend with no binder. | Proved | proved | src/rules/LAWS.bend closed_walk_counts; src/rules/LAWS.bend closed_counts |
-| BOLT-LAW-3 | An `@unsafe def` reachable by relative imports from a law file in the run is a finding. | Proved | proved | src/rules/LAWS.bend unsafe_reports; src/rules/LAWS.bend unsafe_from; src/rules/LAWS.bend unsafe_shut; src/rules/LAWS.bend unsafe_least |
+| BOLT-LAW-3 | An `@unsafe def` or a foreign def (a def whose body is only imports of `.c` or `.js` files) reachable by relative imports from a law file in the run is a finding, at the def, that names the first such law file and the import path from it to the def's file. | Proved | proved | src/rules/LAWS.bend unsafe_reports; src/rules/LAWS.bend unsafe_from; src/rules/LAWS.bend unsafe_shut; src/rules/LAWS.bend unsafe_least |
 | BOLT-LAW-5 | Run over the whole tree, the traceability rule reports exactly one finding for each defect of SPEC.md, in the format stated under "Tagging and traceability", against the laws read, and nothing else: a table row with the wrong number of cells; a row whose ID does not match the pattern; a requirement or trust row whose ID another row of its table kind also has; a requirement row that is neither Proved with status proved or pending nor Trusted with an empty status, a proved row that names no law, and a Trusted row that names one; a Trusted row with no trust row; for each Law entry of a Proved row, proved or pending, an entry that is not `<path> <law>`, a path no LAWS.bend read has, or a law it lacks, else one for no `for`/`exs` binder and one for no tag of the row; and a tag naming an ID no Proved row, proved or pending, lists. A pending row may name laws that prove part of it and a tag may name a pending row. With no SPEC.md it reports that once; over files named on the line, nothing. | Proved | proved | src/rules/LAWS.bend trace_pending_judged; src/rules/LAWS.bend trace_pending_shape; src/rules/LAWS.bend trace_proved_shape; src/rules/LAWS.bend trace_trusted_shape; src/rules/LAWS.bend trace_pending_claimed; src/rules/LAWS.bend trace_trusted_unclaimed; src/rules/LAWS.bend trace_unlisted_unclaimed; src/rules/LAWS.bend trace_counts; src/rules/LAWS.bend trace_unread; src/rules/LAWS.bend trace_named |
 
 ### Grading and config (BOLT-CFG)

diff --git a/docs/rfc/bolt-spec.md b/docs/rfc/bolt-spec.md
@@ -48,7 +48,7 @@ bolt has 271 laws, and 257 of them are closed: each pins one call on one input,
 | `#\|` test | A test written as a `#\|` trailer comment beside the code, which a test runner evaluates. bolt#10 moved most of bolt's into closed laws. |
 | Closed law | A law with no `for` or `exs` binder. It holds for one input, which makes it a unit test checked at compile time. |
 | Quantified law | A law with at least one binder. It holds for every input of that type. |
-| Proof gate | For every PROOF.bend, `bend PROOF.bend` prints exactly `All terms check.` as its first line. |
+| Proof gate | For every PROOF.bend, `bend PROOF.bend` prints exactly `ALL PROOFS CHECK` as its first line. |
 | Proved | A requirement backed by a quantified law tagged with its ID, passing the proof gate. |
 | Trusted | A requirement that is assumed, listed in the trust boundary, and checked by nothing in bolt. |
 | Pending | The status of a Proved requirement whose law has not landed. It is a status, not a level. |
@@ -109,7 +109,7 @@ The proposal has five parts, four of them carried over from ez. A **specificatio
 
 |  |
 |:---:|
-| <pre>┌──────────┐     ┌───────────────┐          ┌────────────────┐     ┌────────────────┐<br>│ SPEC.md  │────▶│ Requirement   │──Proved─▶│ LAWS.bend      │────▶│ PROOF.bend     │<br>│ (IDs +   │     │ ID + level    │          │ (quantified,   │     │ (gate: "All    │<br>│  levels) │     │               │          │  # BOLT-X-N)   │     │  terms check.")│<br>└──────────┘     └───────┬───────┘          └────────────────┘     └────────────────┘<br>                         │                          ▲<br>                      Trusted                       │ checked by<br>                         ▼                          │<br>                 ┌───────────────┐          ┌────────────────┐<br>                 │ Trust boundary│          │ bolt: closed + │<br>                 │ (in SPEC.md)  │          │ traceability   │<br>                 └───────────────┘          └────────────────┘</pre> |
+| <pre>┌──────────┐     ┌───────────────┐          ┌────────────────┐     ┌────────────────┐<br>│ SPEC.md  │────▶│ Requirement   │──Proved─▶│ LAWS.bend      │────▶│ PROOF.bend     │<br>│ (IDs +   │     │ ID + level    │          │ (quantified,   │     │ (gate: "ALL    │<br>│  levels) │     │               │          │  # BOLT-X-N)   │     │  PROOFS CHECK")│<br>└──────────┘     └───────┬───────┘          └────────────────┘     └────────────────┘<br>                         │                          ▲<br>                      Trusted                       │ checked by<br>                         ▼                          │<br>                 ┌───────────────┐          ┌────────────────┐<br>                 │ Trust boundary│          │ bolt: closed + │<br>                 │ (in SPEC.md)  │          │ traceability   │<br>                 └───────────────┘          └────────────────┘</pre> |
 | Caption: Every requirement ends in a tagged quantified law the proof gate checks, or in a named assumption. bolt's own rules check that the tags and binders are there. |
 
 ### Two levels, and the positions carried over from ez
@@ -118,7 +118,7 @@ We take ez's positions as settled rather than re-argue them, since the two speci
 
 The other positions follow from keeping only those two levels. Closed laws have no standing, because a law about one input is a test, and tests and fixtures are never evidence for a requirement for the same reason. Untagged quantified laws are allowed, but nothing protects them, so a change may edit or delete them freely. A guarantee proved in a pinned dependency is Trusted from bolt's side, because bolt's gate does not re-check the dependency's proofs.
 
-The proof gate is the one mechanical check the spec depends on: every PROOF.bend's first output line is exactly `All terms check.`, which rules out the `All terms check, but N defs rely on unsafe or foreign code:` form bend exits 0 with. bolt does not run that gate itself. `flake.nix` calls ez's `mkProofs`, which runs `ez test --unit-only` today and `ez prove` once ez ships it, and that runner's faithfulness is BOLT-TRUST-6.
+The proof gate is the one mechanical check the spec depends on: every PROOF.bend's first output line is exactly `ALL PROOFS CHECK`, which rules out `SOME PROOFS FAIL` (bend 2.0.34 prints it, then the reason, `Error: N defs rely on unsafe or foreign code:` or `Error: N TODOs found.` among them, and exits 1; before 2.0.32 a proof leaning on unsafe or foreign code printed `All terms check, but N defs rely on unsafe or foreign code:` and exited 0). bolt does not run that gate itself. `flake.nix` calls ez's `mkProofs`, which runs `ez test --unit-only` today and `ez prove` once ez ships it, and that runner's faithfulness is BOLT-TRUST-6.
 
 ### Closed laws and the `closed` rule
 
@@ -474,7 +474,7 @@ These assumptions sit outside the proofs. They are the complete list of Trusted
 | BOLT-TRUST-3 | The directory listing effect (`bolt/walk/dir.c`, `dir.js`) returns a directory's entries, marking directories with `/`, and the file read effect returns a file's text. | The walk and the reads are foreign code; the planner takes their answers as given. |
 | BOLT-TRUST-4 | The LSP transport (`bolt/lsp/transport/fd.c`, `fd.js`) delivers stdin bytes in order and writes stdout bytes whole. | Foreign code over descriptors 0 and 1. |
 | BOLT-TRUST-5 | `bend <file> --check-only` never runs `main`, and prints its report in the shape `bolt/lsp/report.bend` parses. | bend is a separate program, and the report format has already drifted once (`report_import`). |
-| BOLT-TRUST-6 | The proof gate runner runs bend on every PROOF.bend and accepts only an exact `All terms check.` first line. | It is ez code run by `mkProofs` (`ez test --unit-only` today, `ez prove` when ez ships it). CI builds from a clean tree. |
+| BOLT-TRUST-6 | The proof gate runner runs bend on every PROOF.bend and accepts only an exact `ALL PROOFS CHECK` first line. | It is ez code run by `mkProofs` (`ez test --unit-only` today, `ez prove` when ez ships it). CI builds from a clean tree. |
 | BOLT-TRUST-7 | Every commit on `main` passed `ci.yml`. | Holds only once the ruleset in REVIEW-8 exists. Today it does not hold. |
 | BOLT-TRUST-8 | shake v0.2.0 (`0x085b03c84ca37125e38dddede7b91e55`) parses argv as its proved rows say: SHAKE-TOK-1, SHAKE-TOK-3, SHAKE-TOK-4, SHAKE-PARSE-2, SHAKE-PARSE-3, SHAKE-PARSE-4, SHAKE-PARSE-8, SHAKE-GET-1, SHAKE-GET-2 and SHAKE-ERR-1; ezjson v1.1.0 (`0x81c67699424929b5c44cd8577e18117f`) parses and prints JSON correctly. | Pinned dependencies, by ez.toml hash, each proving its own rows in its own gate at the pinned tag. bolt reads shake through `main.bend` only and never unfolds its parser: the BOLT-CLI laws that name an argv take the answer those rows guarantee as premises, each citing its row, and prove what bolt does with it. |
 | BOLT-OUT-6 | A released code is never renumbered or reused. | A property across versions, enforced by review of the SPEC row that lists the table. |

diff --git a/src/README.md b/src/README.md
@@ -152,7 +152,8 @@ parameters and no `->`), which is how Bend fills the law named `f`.
   a law's `for` names, and every parameter of a foreign def, one whose body
   starts with `import` (its C and JS read them), however its header is
   wrapped.
-- `hole` — a TODO hole left in code, the one bend counts in "N TODO found":
+- `hole` — a TODO hole left in code, the one bend counts in "1 TODO found." /
+  "N TODOs found." (under `SOME PROOFS FAIL`, exit 1):
   `?` and then `TODO`, with spaces, newlines or comments allowed between
   (`?TODO`, `? TODO`). `?todo` and `?TODO_later` are other names, a type
   error to bend, and are not reported. LAWS.bend is exempt: its laws are open
@@ -307,14 +308,17 @@ parameters and no `->`), which is how Bend fills the law named `f`.
   reverse: the missing lane cannot run it. A file headed `# lanes: native`
   needs no `.js`: that exact line must be one of the comment lines before the
   file's first non-comment line.
-- `fuel` — a `Nat` literal (digits, then `n`) passed in a call, `name(..)`,
-  to a fuel parameter of a def of the same file. A fuel parameter is known by
-  its name alone, the one before its colon: `fuel`, `gas`, `steps` or
-  `budget`, or any name starting with `fuel`. Input past it is cut short
-  with no error: derive the fuel from the input. A literal of any size counts,
-  `3n` included. Only an argument that is one literal token alone counts, so
-  `U32.to_nat(1000)`, a let-bound literal and `(7n)` are not seen. A def's
-  own calls are exempt.
+- `fuel` — a `Nat` literal (digits, then `n`), or `U32.to_nat` of a U32
+  literal (`U32.to_nat(100000)`), passed in a call, `name(..)`, to a fuel
+  parameter of a def of the same file. A fuel parameter is known by its name
+  alone, the one before its colon: `fuel`, `gas`, `steps` or `budget`, or
+  any name starting with `fuel`. Input past it is cut short with no error:
+  derive the fuel from the input. In a law it is worse: a lemma proved over
+  every fuel, used at a big fixed one against a goal written another way,
+  overflows the checker's stack (bend 2.0.33/2.0.34). A literal of any size
+  counts, `3n` included. Only an argument that is the literal alone, or
+  `U32.to_nat(` it `)`, counts, so a let-bound literal and `(7n)` are not
+  seen. A def's own calls are exempt.
 - `tail` (pedantic) — a self-call that is not a tail call, in a def whose
   first live parameter is a `List` or a `String`. On a long one the JS lane
   overflows its stack (a 48 KB header crashed a server; ~4,900 entries and
@@ -338,11 +342,16 @@ parameters and no `->`), which is how Bend fills the law named `f`.
   (proved or pending) `<path> <law>` entry that is missing, has no binder or
   lacks the tag, a Trusted row with no trust row, and a tag SPEC.md does not
   list as a Proved row, proved or pending.
-- `unsafe` (project) — an `@unsafe def` that a LAWS.bend or PROOF.bend
-  reaches through its imports. There the checker prints "All terms check,
-  but N defs rely on unsafe or foreign code:" and a `- name` list (2.0.16
-  counted marks: "with N unsafe annotations.") and exits 0, so a gate that
-  reads the exit status goes green on an unproven claim.
+- `unsafe` (project) — an `@unsafe def` or a foreign def (a body of only
+  `import "./x.c"` / `import "./x.js"` lines) that a LAWS.bend or PROOF.bend
+  reaches through its relative imports, over the files bolt read. Since bend
+  2.0.32 such a proof fails: bend prints `SOME PROOFS FAIL`, then `Error: N
+  defs rely on unsafe or foreign code:` and a `- name` list, and exits 1
+  (2.0.34), every def of every imported module counted. That list names the
+  defs, not the import that brought the effect in; the finding names the
+  import path from the law file (`LAWS.bend -> mid.bend -> eff/io.bend`). Move
+  the effect into a sibling module no law file imports and pass it in as a
+  service. Hash imports (`import 0x.../path`) are not followed.
 - `coverage` (project) — in a project that states laws (a LAWS.bend among the
   files bolt read), a def or a type that no law reaches. It is `coverage`, not `law`,
   because `law` is a Bend keyword: `def law()` is no def, so a bolt.bend