Skip to content

feat(rules): fromrev (U016), fewer false positives in six rules, retire argv - #229

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

feat(rules): fromrev (U016), fewer false positives in six rules, retire argv#229
ngngardner merged 6 commits into
mainfrom
claude/optimistic-hypatia-27r51a

Conversation

@ngngardner

@ngngardner ngngardner commented Sep 30, 2026

Copy link
Copy Markdown
Contributor

This follows #226. It adds one rule, and it narrows or fixes the rules that a false-positive audit on real code found noisy.

  • Corpus: the tracked non-law .bend files of 9 Emerging-Patterns repos, bendlang/bend's demos and base, and the self-hosted compiler from Self hosted bend bendlang/bend#1207.
  • Method: each copy got a bolt.bend turning every rule on, and up to 15 hits per rule were read at the source.

Closes #98.

Changes

Commit Rule Kind Spec row
feat(rules): fromrev (U016) new new rule, on in suspicious BOLT-RULE-U016 added, proved
fix(rules): thunk (U015) … U015 (unreleased) narrowed U015 reworded, still proved
fix(rules): fuel (U006) … index (U007) … U006, U007 behavior change: fewer findings U006 and U007 reworded, still proved
fix(rules): unused (U001) and doc (S001) … U001, S001 behavior change: fewer findings U001 and S001 reworded, still proved
fix(rules): retire argv (U014) … U014 (unreleased) removed; U014 stays reserved U014 row removed
chore: turn scan (U013) off … U013 bolt's own config only none

Each narrowing only removes findings; no repo gained one. No law was weakened to pass a proof, and the trust boundary did not grow.

New: fromrev (U016)

  • What it reports: String.from_list(List.reverse(..)), where folding the buffer onto a String with SCon does it in one pass.
  • Cost: on bend 2.0.34 it is about 2× slower natively. On the JS lane, the reverse-then-from_list form overflows the stack at 50k characters, because String.from_list is not a tail call.
  • Precision: every hit on real code was the exact shape.
  • bolt's own 9 sites: rewritten with a new pure helper, src/rchars.bend.
  • Downstream: it will report 4 sites in eztoml, 1 in ez and 1 in shake when they bump their bolt pin.

Narrowed or fixed

Rule Audit finding Change Corpus hits
thunk U015 23 of 200 were dispatch (Lazy.either(.., _u => go(a), _v => go(b))), where carrying a Bool is the wrong advice reports only a thunk that is the one lambda of its call 200 → 177; all 23 dropped were dispatch
fuel U006 6 of 6 sampled were a fixed budget on an IO loop (App.loop, Client.drain, bolt's own reads) skips a call to a def returning IO(..); bolt's 2 stale noqa: U006 removed bend 4 → 1
index U007 2 of 2 were Base's own List.get/String.get recursion skips the def's own self-call 2 → 0
unused U001 a foreign def whose return type wraps to the next line; names used inside a @+x: T -> .. arrow foreign exemption holds however the header wraps; arrow uses count (the fix is in src/syntax/tree.bend) bend 150 → 98
doc S001 a comment above an @unsafe line was rejected a comment above a run of @ lines counts 86 fewer (bend and selfhost)

inert_doc now also assumes the two sources' lines start with @ alike; BOLT-RULE-INERT's row is unchanged. The new untagged laws arrow_term, marked_arrow_term and attribute_def pin the tree change.

Opt-in rules from #226

  • argv (U014) is retired before its first release.
    • It was worth fixing in only 8% of hits: every reader in the org already drops the program name, and the rule cannot tell a correct reader from a wrong one.
    • U014 is never reused.
    • The IO.args documentation in AGENTS.md stays.
  • scan (U013) stays opt-in but is off in bolt's own bolt.bend.

Checks

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 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, unchanged from main (all L001).
  • Each fix was first confirmed on a minimal file with the old binary, and each restated law was seen to fail before it was re-proved.

Left open

🤖 Generated with Claude Code

https://claude.ai/code/session_01X7i62UAece6mwMRV3Y1b9B

Generated by Claude Code

@claude
feat(rules): fromrev (U016), String.from_list of a List.reverse
030da91 
`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
@claude
fix(rules): thunk (U015) reports only a lone thunk, not a dispatch
5da74a2 
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
@claude
fix(rules): fuel (U006) skips effect loops, index (U007) skips the ge…
6c6379d 
…t'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
@claude
fix(rules): unused (U001) and doc (S001) false positives
3c39e82 
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
@claude
fix(rules): retire argv (U014) before its first release
ae55302 
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
@claude
chore: turn scan (U013) off in bolt's own bolt.bend
ef75d66 
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
@ngngardner
ngngardner merged commit 35271b9 into main Sep 30, 2026
1 check passed
@ngngardner
ngngardner deleted the claude/optimistic-hypatia-27r51a branch September 30, 2026 15:01
@github-actions github-actions Bot mentioned this pull request Sep 30, 2026
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

rule candidate: fromrev — String.from_list(List.reverse(buf))

2 participants

@ngngardner @claude