[ngngardner]

empty reports Nat.is_eq(List.length(.., x), 0n) and Nat.is_eq(String.length(x), 0n) when the test is an argument (right after (, [, { or ,) and x, a plain name, is read again after it in the same group. Base's lengths count every cell and are not tail calls. List.is_empty(.., x) / String.is_empty(x) take the same arguments, look at one cell and give the same Bool. On in suspicious by default, beside prefix and fromrev.

Why only a kept x

On the native lane, freeing a list the program never walked costs more than walking it: callgrind puts about 155 instructions a cell in the runtime's term_drop against about 28 for a compiled walk. When the test is x's last use, the original length walk frees x cheaply and the fix is slower on native. Measured on bend 2.0.38 (a 0–1000 char String, old/new):

shape	JS	native
kept and read after	1.31×	1.57×
dropped after the test	1.65×	0.27×

So the rule leaves alone:

• a test with no read of x after it in its group,
• a test that reads x only before it,
• a test outside any group (v = Nat.is_eq(..)).

It also skips a law and a def that is a proof (no type, or one returning -> {..}) in any file, plus LAWS.bend and PROOF.bend. A first version reported 4 law statements and proof defs in bendlib's mathlib, which is why the proof skip is there.

Evidence

• Corpus: over the public Bend 2 repos awesome-bend lists, it reports exactly 8 sites in 2 repos (BendKV 6, birc 2). All 8 were read by hand and are true positives, and no other file is reported.
• No fix commit: no public commit rewrites this shape.

Laws (each proved)

• Reports: empty_reports_{list,string}_kept, empty_reports_in_typed_def.
• Skips:
  • empty_skips_{list,string}_{dropped,before,bare}
  • empty_skips_in_{law,untyped_def,proof_def}
• Exemptions: empty_exempt, role_empty, role_empty_exempt.
• Inert: inert_empty. Comment and string contents never change the findings. The rule reads token text only through code(k, t), so this needs no "as the lexer makes them" hypotheses.

The code table gains a row, U018. Its proof's arms already reach past the 30 rows, so it is unchanged.

Also

• bolt's own dir_of (src/rules/imports.bend) tested a kept list's length; it uses List.is_empty now.
• Merge with main: merged with feat(rules)!: regroup, demote and retire rules after the audit #267's regroup; empty stays in suspicious.
• Gate: nix flake check passes locally and in CI.
• Out of scope: the same native drop cost also makes pick, strict and eager's suggested fix slower when the searched list is fresh and dropped right after the search (0.62–0.94× on native in my runs; faster when the list is kept). This PR leaves those rules unchanged.

🤖 Generated with Claude Code

https://claude.ai/code/session_0186KEnst9PZ9GVQD8BtKhu4

BEGIN_COMMIT_OVERRIDE
feat(rules): empty (U018), a kept length compared to zero is is_empty
END_COMMIT_OVERRIDE