Skip to content

feat(rules): scan (U013), argv (U014), thunk (U015) and setting (C011) - #226

Merged
ngngardner merged 7 commits into
mainfrom
claude/optimistic-hypatia-27r51a
Sep 30, 2026
Merged

ngngardner merged 7 commits into
mainfrom
claude/optimistic-hypatia-27r51a

Conversation

@ngngardner

Copy link
Copy Markdown
Contributor

Four new rules, chosen from the open rule candidates by three things:

Each rule went spec-first: a SPEC.md row, then a quantified law, a proof, and the row flipped to proved.

Closes #196, closes #217, closes #113, closes #224.

Requirements added or reworded

ID Level Status Laws
BOLT-RULE-U013 scan (new) Proved proved scan_counts (direct, a count against an independent counter), scan_quiet (frame), scan_slots
BOLT-RULE-U014 argv (new) Proved proved argv_counts (count: frame and completeness), inert_argv, argv_opt_in
BOLT-RULE-U015 thunk (new) Proved proved thunk_walk_counts, thunk_counts
BOLT-RULE-C011 setting (new) Proved proved unknown_exact, setting_reports
BOLT-CFG-7 Proved pending → proved unknown_exact, settings_graded
BOLT-RULE-EXEMPT, BOLT-RULE-INERT Proved proved lists grown by scan_exempt, thunk_exempt, inert_scan, inert_argv and inert_thunk
BOLT-OUT-3 Proved proved behavior change: setting's findings print after the per-file findings and before coverage, unsafe and trace
BOLT-SCOPE-2 Proved proved wording: setting sees the text of each bolt.bend that grading reads

No existing law was weakened, and the trust boundary did not grow. BOLT-OUT-1's per-row proof now covers the 34-row code table.

The rules

scan (U013), opt-in, suspicious.

  • What it reports: a def that calls itself and, on each step, hands a parameter it carries unchanged to a walk. A walk is a Base list search, or a def of the file that walks that argument. The cost is O(|A|·|B|).
  • Evidence: this shape took 135 s of a 208 s lint in unused, and Self hosted bend bendlang/bend#1207's P9 found the same quadratic rescan (33.66% of its profile samples).
  • On in bolt: turned on at error in bolt.bend. About 54 real but small bounded scans carry # noqa: U013 with a reason, across 23 comments.
  • Worth fixing later: rewalk's per-site walks, bind.refresh, digest.laws_of and unused's reportable.
  • Other repos: 14 findings in ez, 1 each in ezhttp and shake, none in ezjson, eztoml or snap.

argv (U014), opt-in, suspicious.

  • What it reports: every IO.args( call. Since bend 2.0.32 its head is the program as invoked, and that silently broke every direct reader in the org during the move to 2.0.34.
  • On in bolt: turned on in bolt.bend, and the one reader, src/args.bend, carries a noqa.
  • Other repos: all 7 reads in ez, ezjson and shake already drop the program name.

thunk (U015), opt-in, suspicious.

  • What it reports: a thunk whose body is exactly a self-call, such as Lazy.or_else(hit, _u => go(rest, k)). The closure is allocated on every miss, and the search leaves the loop each time round.
  • Evidence: on bend 2.0.34, 500 misses over 100k cells take 2.40 s against 0.28 s on JS, and 1.18 s against 0.76 s native, compared with carrying the test as a Bool. Self hosted bend bendlang/bend#1207 gained 5.8–6.7% per site.
  • Advice changed: AGENTS.md and the eager/Lazy headers now say to carry the Bool for a recursive search, and to keep Lazy.* for work that doesn't recurse.
  • Off in bolt for now: it reports 72 sites in bolt; migrating them is a follow-up.

setting (C011), on by default, correctness.

  • What it reports: a bolt.bend def <name>() whose name is no rule slug and no group in the code table, so it sets nothing. For example, def wrp() or a retired def quantify().
  • Where it shows: CLI only. An open bolt.bend still gets no lint in the editor (BOLT-LSP-4 is unchanged).
  • Other repos: no sibling bolt.bend has an unknown name.

Checks run

These ran on bend 2.0.34 with BEND_LIB set to the pinned shake, ezjson and snap. There is no nix or ez in the environment, so CI's nix flake check is the first full run.

  • All 7 PROOF.bend print ALL PROOFS CHECK.
  • bend main.bend -o bin/bolt.bin, then bin/bolt.bin --gpu off over the tree, gives 0 errors, 73 warnings. That is unchanged from main; all 73 are L001.
  • On a scratch project, U013, U014, U015 and C011 each fire on their shape.

Left pending

🤖 Generated with Claude Code

https://claude.ai/code/session_01X7i62UAece6mwMRV3Y1b9B


Generated by Claude Code

Since bend 2.0.32 IO.args() starts with the program as invoked, so a
program that parses it as it comes takes its own path for its first
argument (#217). `argv` reports each `IO.args` token with a `(` right
after it among the significant tokens, and nothing else; no path is
exempt. It is opt-in (BOLT-CFG-6): the one reader a program has, which
drops the head, carries `# noqa: U014`, as src/args.bend's now does.

BOLT-RULE-U014 is proved by argv_counts (a count against an independent
counter), inert_argv (also under BOLT-RULE-INERT) and argv_opt_in.
bolt.bend turns it on at error for this tree.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01X7i62UAece6mwMRV3Y1b9B
…r group

A setting in a bolt.bend whose name is neither a rule's slug nor a group of
the code table (a typo such as `def wrp()`, or a retired name such as
`quantify` or `shadow`) set nothing and failed open. `setting` (C011,
correctness, on by default) now reports it once for each bolt.bend that
grades a directory of the run, at that bolt.bend's path and the setting's
def line. CLI lint only; the LSP is unchanged.

- config.bend: settings keep their name, word and def line (Setting);
  parse is levels(settings(text)); `unknown` filters by Codes.table().
- lint/plan.bend: `settings` finds each grading bolt.bend and runs the rule.
- SPEC: BOLT-CFG-7 proved (unknown_exact, settings_graded); new
  BOLT-RULE-C011 proved (unknown_exact, setting_reports).

Behavior change: BOLT-OUT-3's output order gains a slot. `setting`'s
findings print after the per-file findings and before coverage, unsafe and
trace (lines_in_order reworded with it). BOLT-SCOPE-2 now also says what
`setting` sees (scope_findings' spec gains the slot).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01X7i62UAece6mwMRV3Y1b9B
… rule or group

Resolves the overlap with argv (U014): both laws and proofs kept, the code
table's per-row proof arms grown to 32 rows, the README group table naming
both rules, and the setting proofs' long lines wrapped for `space` (S002).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01X7i62UAece6mwMRV3Y1b9B
… on every step

A new opt-in suspicious rule: a lambda whose body is exactly a self-call of
its def, and whose parameter the call does not read (`Lazy.or_else(hit,
_u => go(rest, k))`). The closure is allocated on every step and the call in
it is not a tail call, so the search leaves the loop each time round (bend
2.0.34, 500 misses over 100k cells: JS 2.40 s against 0.28 s with the test
carried as a Bool, native 1.18 s against 0.76 s; bend PR #1207 measured
5.8 to 6.7% of the self-hosted compiler per site). The rule recommends
carrying the test into the next call, `go(rest, k, test(h))`, matched first.

BOLT-RULE-U015 is proved (thunk_walk_counts, thunk_counts against an
independent counter); thunk joins BOLT-RULE-EXEMPT (thunk_exempt),
BOLT-RULE-INERT (inert_thunk) and scope_law_file (BOLT-SCOPE-4). It is
opt-in (BOLT-CFG-6): off unless a bolt.bend names it, and bolt's own tree
does not turn it on yet (72 findings to migrate).

eager's header and README entry, lazy.bend's header and AGENTS.md's
Bool.pick/Lazy gotcha stop recommending a Lazy thunk around a recursive
step: carry the Bool for a recursive search, keep Lazy.* for work that does
not recurse. No rule message changes (eager's and pick's never named Lazy).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01X7i62UAece6mwMRV3Y1b9B
… loop

Resolves the overlap with argv (U014) and setting (C011): opt_in lists
trace, argv and thunk; BOLT-RULE-INERT's Law cell keeps inert_argv beside
inert_thunk; the code table's per-row proof arms cover 33 rows. Refs #224.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01X7i62UAece6mwMRV3Y1b9B
A def that calls itself and, on a hot step, passes a parameter every
self-call hands back unchanged to a walk: a Base list search
(List.contains, find, filter, length, any, all, foldl, foldr) or a def of
the file that walks that argument (the one it shrinks, unless a Nat or a
String, or one it passes on to a walk). Every step walks the list again,
O(|A| * |B|) (#196). Quiet on a literal or an expression in that argument,
lambda bodies, non-recursive case arms, laws and proofs.

Opt-in (BOLT-CFG-6): only `def scan()` turns it on. bolt.bend turns it on
at error; the 48 genuine per-item scans in bolt's own tree carry a
`# noqa: U013` with the list's bound.

BOLT-RULE-U013 is proved by scan_counts, scan_quiet and scan_slots;
scan_exempt joins BOLT-RULE-EXEMPT and inert_scan BOLT-RULE-INERT.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01X7i62UAece6mwMRV3Y1b9B
…hanged

Resolves the overlap with setting (C011), argv (U014) and thunk (U015):
scan_exempt and thunk_exempt, scan's and thunk's count sections kept whole
and apart; opt_in lists trace, argv, thunk and scan; BOLT-RULE-EXEMPT and
INERT name every new rule and law; the per-row proof arms cover 34 rows.
scan, now on in bolt.bend, reports setting's lookup of the fixed code table
per setting: marked with a noqa and its reason, like the other small-table
sites. Refs #196.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01X7i62UAece6mwMRV3Y1b9B
@ngngardner
ngngardner enabled auto-merge (squash) September 30, 2026 12:59
@ngngardner
ngngardner merged commit b60e9cd into main Sep 30, 2026
1 check passed
@ngngardner
ngngardner deleted the claude/optimistic-hypatia-27r51a branch September 30, 2026 13:02
ngngardner pushed a commit that referenced this pull request Sep 30, 2026
A false-positive audit of argv put its precision at 8%: every IO.args()
reader in the ecosystem already drops the program name, and the rule
cannot tell a correct reader from a wrong one, so nearly every finding
asked for a noqa. It merged in #226 and was never released, so it goes
now: the rule, its registration, its code-table row, its opt-in entry,
the laws argv_counts, inert_argv and argv_opt_in with their proofs, the
BOLT-RULE-U014 row, and bolt's own setting and noqa for it.

U014 stays reserved: codes are append-only, and src/codes.bend and
src/README.md list it as retired beside C001, U005 and L004.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01X7i62UAece6mwMRV3Y1b9B
ngngardner added a commit that referenced this pull request Sep 30, 2026
…re argv (#229)

* feat(rules): fromrev (U016), String.from_list of a List.reverse

`fromrev` reports each run of significant tokens whose texts are
`String.from_list`, `(`, `List.reverse` and `(`, one finding on the first,
and nothing else; a LAWS.bend or a PROOF.bend is exempt. Reversing a char
buffer and reading it into a String walks it twice and builds a list only
to throw it away, and String.from_list is not a tail call: fold the buffer
onto a String with SCon in one pass. On in `suspicious` by default.

Measured (bend 2.0.34, a 100k-char reversed buffer 200 times): native
--gpu off 0.35 s against 0.17 s folded; JS at 20k chars 4.6 s against
3.1 s, and at 50k the two-pass form overflows the JS stack.

BOLT-RULE-U016 is proved by fromrev_counts (a count against an independent
counter, zero on a law file), fromrev_exempt (also under BOLT-RULE-EXEMPT)
and inert_fromrev (also under BOLT-RULE-INERT). The code table's per-row
proof arms cover 35 rows.

bolt's own 9 sites now go through src/rchars.bend (Rchars.text, one pass):
the lexer's word, noqa's word, word.bend's text, frame's decode.end,
config's dir_of.go and home.segs, and trace's cells. The lexer and trace
proofs are carried over to the fold (rword.go, trace.text).

Refs #98

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01X7i62UAece6mwMRV3Y1b9B

* fix(rules): thunk (U015) reports only a lone thunk, not a dispatch

thunk now reports a self-call thunk only when it is the one lambda among
the arguments of the call it is passed to: the kids of a `(` group, split
at their comma leaves, hold exactly one argument with a `=>` leaf of its
own (not inside a bracket). A dispatch, a call given two or more lambdas
(`Lazy.either(T, c, _u => go(a), _v => go(b))`), is left alone: carrying
one Bool into the next call does not replace it. A lambda that is no
call's argument (`x = _u => go(t)`) is no longer reported either.

This narrows a guaranteed behavior: BOLT-RULE-U015 is reworded with the
rule's header, and thunk_walk_counts' independent counter (thunk.count,
now carrying whether the chain is such a call's kids, with thunk.args
and thunk.lone) is restated to match and re-proved; thunk_counts,
thunk_exempt and inert_thunk follow.

Over the corpus (bolt, ez, ezhttp, ezjson, eztoml, snap; law, proof and
test files removed): 200 -> 177 findings. bolt 77 -> 65, ez 69 -> 69,
ezhttp 19 -> 17, ezjson 6 -> 6, eztoml 27 -> 18, snap 2 -> 2. Every one
of the 23 dropped is a call with two or more lambdas.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01X7i62UAece6mwMRV3Y1b9B

* fix(rules): fuel (U006) skips effect loops, index (U007) skips the get's own self-call

Behavior change to two released rules, both with 0% sampled precision on
real code.

fuel (U006, BOLT-RULE-U006): a call to a def that returns an effect is no
longer reported. A def returns an effect when its header holds a top-level
`->` token with the capitalized name token `IO` right after it, or, when
the `->` is the header's last token, first on the line under it (`->` then
`IO(Unit):`). An effect loop's fuel bounds reads, frames or retries the
outside world sets, not the size of an input. The law fuel_slots is
restated (fuel.slots keeps only the defs that return no effect);
fuel_walk_counts and fuel_counts follow it. bolt's own two `# noqa: U006`
(src/lsp/files/disk.bend, src/lsp/transport/stdio.bend) silenced nothing
now and are removed.

index (U007, BOLT-RULE-U007): a List.get / String.get call whose name is
the def's own (the step of a def named List.get or String.get, as Base's
are) is no longer reported. index_counts is restated (index.count and
index.site take the def's name as self).

Counts on the sampled corpus (old -> new U006+U007): bend 6 -> 1 (the one
left is Wav.walk, a pure def, still reported), bolt tree 0 -> 0 with its
noqa comments gone, every other ecosystem repo 0 -> 0. bolt on this tree:
0 errors, 73 warnings, as before.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01X7i62UAece6mwMRV3Y1b9B

* fix(rules): unused (U001) and doc (S001) false positives

Behavior changes to two released rules, each with its SPEC row, rule
header and tagged law restated to match:

- unused (BOLT-RULE-U001): a foreign def, whose parameters are exempt, is
  one whose body's first statement is `import`, wherever its header's `->`
  and return type fall. A header that does not end in `:` runs on through
  the body's statements up to one that does, so `def f(..) ->` then
  `IO(T):` on the next line then `import "./x.c"` is foreign. Law
  unused_counts restated (Laws unused.imported now takes the header).
- unused: a name read in a dependent arrow at the start of a body
  (`@+x: U32 -> S`) is a use. The tree classified any `@`-led statement as
  a def (for `@unsafe def`), so the binder skipped the arrow; an `@`
  followed by a name, quantity-marked or not, and `:` now makes a term.
  New untagged laws in src/syntax: arrow_term, marked_arrow_term,
  attribute_def.
- doc (BOLT-RULE-S001): the comment block may sit right above a run of
  `@` lines (`@unsafe`) right above the item. Laws doc_walk_counts and
  doc_counts restated (Laws doc.lead replaces doc.hash); inert_doc
  (BOLT-RULE-INERT) now takes lines that start with `#` alike and with
  `@` alike.

Corpus (every group on at warn), old -> new:
- bend: U001 150 -> 98 (46 wrapped foreign params in bend2/base.bend,
  6 dependent-arrow params in bend3d.bend); S001 300 -> 298 (@unsafe)
- selfhost: U001 3815 -> 3815; S001 2592 -> 2508 (84, all @unsafe)
- bolt, ez, ezaudio, ezhttp, ezimg, ezjson, eztoml, shake, snap: 0 -> 0
No finding added anywhere, no other rule's findings changed. bolt on its
own tree: 0 errors, 73 warnings, as before.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01X7i62UAece6mwMRV3Y1b9B

* fix(rules): retire argv (U014) before its first release

A false-positive audit of argv put its precision at 8%: every IO.args()
reader in the ecosystem already drops the program name, and the rule
cannot tell a correct reader from a wrong one, so nearly every finding
asked for a noqa. It merged in #226 and was never released, so it goes
now: the rule, its registration, its code-table row, its opt-in entry,
the laws argv_counts, inert_argv and argv_opt_in with their proofs, the
BOLT-RULE-U014 row, and bolt's own setting and noqa for it.

U014 stays reserved: codes are append-only, and src/codes.bend and
src/README.md list it as retired beside C001, U005 and L004.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01X7i62UAece6mwMRV3Y1b9B

* chore: turn scan (U013) off in bolt's own bolt.bend

scan stays in bolt as an opt-in audit tool, its rule and laws unchanged;
bolt's own tree no longer turns it on. Its 55 noqa comments go with it,
since with scan off noqa (S005) would report each as naming a code that
no finding has. No logic changes.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01X7i62UAece6mwMRV3Y1b9B

---------

Co-authored-by: Claude <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment