feat(mir): implement clean_counter via faint-variable analysis

[gertybotbot]

Closes #2178.

Implements the clean_counter MIR lint via faint-variable analysis: a counter that is
updated but never observed is reported as removable.

Scope correction (important)

The lint ships scoped to float accumulators, not integers. This is narrower than
#2178 implies, and the narrowing is a soundness result rather than a shortcut:

• Integer counters under checked arithmetic are genuinely strongly live. The
  overflow flag feeds Branch → Trap, so the counter is observable through the trap
  edge and removing it would change program behaviour. These correctly never fire.
• Float accumulation has no trap edge, so an unobserved float counter is soundly
  removable.

IntArithChecked is therefore deliberately kept off the purity allowlist.

Discrimination, not presence

Tests are built as controls rather than assertions that the lint exists:

• two identical accumulators in one function — only the unobserved one fires
• integer counters: silent (per the trap-edge result above)
• for-range counters: silent
• returned counters: silent
• printed counters: silent

clean_counter is registered as a real lint, so -D / -W / -A all work.

Verification (run bare, exit codes read directly)

• cargo test -p hew-mir → RC=0
• cargo test -p hew-cli --test lint_pass_e2e → 40/40, RC=0
• cargo clippy --workspace --all-targets → RC=0
• cargo fmt --all --check → RC=0

Relationship to #2873

#2873 wires MIR lint findings into the LSP and wasm/playground surfaces keyed off
IrPipeline::lint_warnings. That plumbing is already written such that clean_counter
surfaces on both surfaces for free once this lands — the two are independent but
complementary, and this one is the substrate.

[gertybotbot]

Reviewed against post-rc1 main (4ce27c7).

Blocking: this does not compile against current main. Green CI here is misleading — the branch predates rc1's change to instr_reads_writes, and because the two never touch the same lines GitHub still reports MERGEABLE/CLEAN.

hew-mir/src/dataflow.rs:670 now returns a 3-tuple:

pub(crate) fn instr_reads_writes(instr: &Instr) -> (Vec<Place>, Vec<Place>, Vec<Place>)

hew-mir/src/faint.rs destructures it as a pair at both call sites (the collect_seeds_and_edges loop and the defining-instruction scan). Rebasing onto 4ce27c7 needs let (reads, writes, _) = instr_reads_writes(...) at both, and the surrounding Place::Local match arms adjusted for the resulting binding modes. The third element is interior_writes; it deserves a deliberate decision rather than a discard, since an interior write is a way a counter can be observed and dropping it on the floor is exactly the shape of a false positive this lint cannot afford.

Soundness of the float-only scoping: holds. IntArithChecked is correctly absent from is_pure_value_instr, and the argument is stronger than the PR body claims — in collect_seeds_and_edges every instruction outside the small pure allowlist seeds its operands as observable, so a checked integer add makes its counter strongly live directly, without needing to trace the overflow flag to the Branch → Trap edge. Two further independent guards (counter_target_name accepting only F32|F64, and the update-shape match accepting only float arithmetic) mean the integer case is closed three times over.

I tried to construct a false positive in the classes that would matter for a lint telling users to delete code — FFI and runtime exposure, globals, actor state, aliasing, side-effecting drop — and could not. Each routes through a non-pure instruction or a terminator operand, which seeds the source local observable. Floats have no drop behaviour. The unknown-instruction path yields silence rather than a finding, so the error direction is false negatives (e.g. FloatDiv/FloatRem are absent from the pure shape allowlist), which is the right way round.

Ordering with #2873. Land #2873 first. Its body carries a time-qualified scope correction asserting clean_counter does not exist and that run_mir_lints calls detect_dead_stores and nothing else; merging this PR first makes those statements false at merge time. With #2873 in first, its correction stays true as written and this PR then needs its own stale wording updated — the CLI-only claims at docs/design/lint-pass.md:23-24, :150-160, :322-328 and hew-mir/src/liveness.rs:431-433, which currently say LSP/WASM stop at HIR and that #2176 is deferred.

[gertybotbot]

Rebased onto rc1 (4ce27c7) and pushed. This branch did not compile against main — rc1 changed instr_reads_writes to return a 3-tuple (reads, writes, interior_writes) and faint.rs destructured it as a pair at both call sites:

error[E0308]: mismatched types
  --> hew-mir/src/faint.rs:190:17
  expected a tuple with 3 elements, found one with 2 elements
error: could not compile `hew-mir` (lib) due to 5 previous errors

GitHub reported MERGEABLE/CLEAN and CI was green because the branch and rc1 never touch the same lines; the break only exists once they are combined.

I handled the third element rather than discarding it, because an interior write is precisely a way a counter gets observed without the analysis seeing it — it mutates through a place whose MIR slot bytes do not change (BytesAppend rewriting its receiver's buffer, Drop on a variant place) and never appears in writes. Two guards: seed interior targets as observable, and refuse to classify an accumulate step whose counter or temp is interior-written.

Both guards are redundant today and the comment says so. Every interior-writing instruction is impure, so pure_single_dest is None and its reads are already seeded. They are kept explicit because that is a property of the current is_pure_value_instr allowlist (Move plus float arithmetic), not an invariant of the IR — adding an interior-writing instruction to that allowlist would silently open the false-positive path.

On the soundness argument: it holds, and it is stronger than the description claims. The trap-edge reasoning is not what closes the integer case. In collect_seeds_and_edges every instruction outside the pure allowlist seeds its operands observable, so a checked integer add makes its counter strongly live directly. counter_target_name accepting only F32|F64 and the update-shape match close it twice more. I tried to construct false positives through FFI, globals, actor state, aliasing, and side-effecting drop and could not — each routes through a non-pure instruction or a terminator operand. The error direction is false negatives (FloatDiv/FloatRem are absent from the pure shape allowlist), which is the right way round for this lint.

Verification after rebase: cargo test -p hew-mir --test diagnostics faint 14 passed (including the discrimination controls); cargo test -p hew-cli --test lint_pass_e2e 40 passed; cargo clippy -p hew-mir --all-targets clean.

Merge after #2873. The two PRs were written against each other's absence. #2873's scope-correction section asserts clean_counter does not exist and that run_mir_lints calls only detect_dead_stores; merging this first makes those statements false at merge time. I left the run_mir_lints doc comment pointing at #2176/#2873 as pending rather than asserting either state, so it is accurate in the current tree and needs a one-line update once #2873 lands.

[slepp]

Thanks — this is a nice piece of work. What I appreciated most is that the checked-arithmetic problem became the scope of the lint rather than something to work around: integer counters are genuinely observable through the trap edge, and keeping IntArithChecked off the purity allowlist says so plainly.

I mutation-tested the soundness argument rather than taking it on trust. Deleting the faintness gate turns four tests red, and widening both the type guard and the shape allowlist to admit integers leaves the lint silent — so faintness really is the guard doing the work, and the other two are belt-and-braces. Ran the compiled Hew suite and scanned all 1863 .hew files: green, no spurious firings.

Two small followups, neither worth holding this up. In recover_counter_shape, the backward scan returns as soon as it finds the temp's defining instruction, so if the first Move into a local isn't an accumulate, later writebacks to that local in the same block never get examined — a continue would widen it. And an accumulator updated in both arms of an if inside a loop emits one warning per arm; defensible, since each line is dead work, but worth a deliberate call.