fix(#946): expand writes_sp's 175-of-222 wildcard into audited arms + no-wildcard tripwire

[avrabe]

Closes #946 (Tier-1 D). Artifact RQ-57-SPWILD.

The measurement, re-taken on origin/main

The issue's numbers are accurate, not stale:

ArmOp variants	222 (matches a32_no_silent_nop_615.rs's pin)
named by writes_sp	47
absorbed by a single _ => false	175 (79 %)

writes_sp documented itself as "exhaustive over every rd-carrying op the priced
instruction set can contain" — the #615 shape exactly: a function that claims to
enumerate a space while a wildcard silently answers for most of it.

Reachability: 30 of the 175 actually reach the predicate

analyze_loops has exactly one caller, wcet::function_wcet_intermediate, and
scan_for_decline runs before it. That scan declines everything op_cost calls
Unmodeled (141) or LoopedExpansion (4). So the stream reaching writes_sp
contains only OpCost::Cycles ops and direct calls:

• 30 of the 175 are priced → genuinely reachable
• 145 are pre-declined → unreachable

All three legs of that argument are now pinned by tests, not asserted in a comment
(op_cost_still_has_no_catch_all_arm, scan_for_decline_runs_before_analyze_loops,
analyze_loops_has_exactly_one_call_site).

One correction to the chain: Call bypasses the op_cost check entirely —
classify_call returns Direct and continues. It is unreachable for a different
reason (encode_thumb refuses it with a typed Err, #615). The comment now says so.

Was anything actually misclassified? Yes — live, and measured

I64Popcnt / I64Rotl / I64Rotr are priced and their expansions really do emit
PUSH/POP (0xB438/0xBC38; 0xB40F = PUSH {R0-R3} via
emit_i64_fixed_abi_entry). Two ordinary WASM modules, -t cortex-m4 --emit-wcet,
only wcet_loops.rs differing:

i64.rotl   in a trip-8 counted loop   main: bounded 3120 cyc
i64.popcnt in a trip-8 counted loop   main: bounded 4702 cyc

So the wildcard was reached and answered on real compilations — not latent.

But the numbers were not wrong. The push/pop is net-zero across the expansion and
writes strictly below the incoming SP, so neither the trip count nor the cycle sum is
corrupted. The bounds were right for a reason nothing checked: they needed the premise
that no tracked counter slot lives at a negative SP offset, and the walk took
addr.offset raw and signed.

I first took the conservative true (declining both loops). That was the wrong trade —
the answer was determinable, just unenforced, and Track D's whole arc is
decline→bound. The premise is now a WalkState invariant instead:

• read_slot(off < 0) → Top
• write_slot_word(off < 0) → taint rather than record
• shift_slots drops any entry a re-base pushed below SP (an epilogue pop {r4-r7}
  shifts by −16, so this case is real)

All three are conservative in one direction only. With the premise enforced, false is
derived, and the bounds come back byte-for-byte identical to main (3120 / 4702).

Net effect of this PR on emitted bounds: none. frozen_codegen_bytes green —
.text cannot move, this is analysis-only.

The _ => false → explicit arms

Grouped by reason, not by answer:

• Precise rd == SP for the priced i64 ops that have a destination
  (I64SetCond, I64Clz, I64Const, I64Ldr, I64Mul, I64Shl, …) — the same test
  their i32 counterparts already got. I64Const/I64Ldr are the wcet: two opcodes (I64Const, I64Str) account for all 9 unmodeled-op declines on a whole OS — and 11 cascades behind them #936 ops that became
  reachable here and silently inherited the wildcard.
• Earned false for the net-zero PUSH/POP group, with both facts spelled out.
• false for the reachable counted-loop vocabulary (Str, Cmp, BOffset,
  BCondOffset, Bx, Bl, Label, Nop, Udf, I64Str). true on any of these
  would decline every proven loop. Two traps recorded in-place: Str's rd is the
  stored value (a source) and MemAddr has no writeback; and Bx must stay
  false because resolve_toplevel_inits matches the guard arm before its Bx arm,
  so a true would shadow the return handling with no compiler warning.
• true for the 142 unreachable variants (VFP, MVE, i64 pseudo family, off-path
  pseudo-ops). Deliberate: true is the give-up direction, and when wcet: two opcodes (I64Const, I64Str) account for all 9 unmodeled-op declines on a whole OS — and 11 cascades behind them #936 priced three
  ops they instantly became reachable and inherited an unaudited false with nobody
  revisiting. Now pricing an op yields a loud decline until its SP effect is audited.

Renamed writes_sp → may_move_sp: both call sites use it as a give-up predicate,
and the old name could not honestly cover the unaudited answers.

Tripwire (#615 style), proven potent rather than assumed

Structural (tests/wcet_sp_no_wildcard_946.rs) — fails if may_move_sp grows a
catch-all, or if any of the 222 variants stops being named. The scanner rejects
bare-identifier bindings (op =>, op if pred(op) =>) as well as _ =>, because
wcet_loops.rs uses both shapes legitimately elsewhere and a _-only scan would be
bypassable. It asserts the extracted body really contains match op { before scanning
it — a scan over nothing passes silently.

Behavioural (unit tests) — pins the answers in both directions, plus an explicit
non-vacuity list.

Measured potency (not claimed):

mutation	result
replace the 142-line arm with _ => false,	3 tests RED (structural ×2 naming all 142, behavioural ×1); restore → green
delete read_slot's off < 0 guard	walk_state_never_tracks_a_slot_below_sp RED; restore → green

The behavioural half only bites because the unreachable bucket answers true — had it
answered false to match the old wildcard, the wildcard would be behaviourally
identical and that half would be vacuous. Three synthetic negative controls prove
the scanner itself can go red.

Bonus finding: a stale audit in a claims-pinned area

Auditing every SP-touching emission turned up STRAIGHTLINE_CEIL_PER_HALFWORD's
rationale claiming "the audited expansions push at most 3 registers, so this holds with
margin". Enumerating every 16-bit PUSH/POP and its owner:

owner	encoding	regs	status
I64Popcnt	0xB438/0xBC38	3	priced
I64DivU	0xB4F0/0xBCF0	4	LoopedExpansion (declined)
emit_i64_fixed_abi_entry	0xB40F	4	priced, via I64Rotl/I64Rotr

The margin does not exist: 1+4 = 5 in one halfword, exactly the ceiling. The bound is
unchanged and still sound, and the finding strengthens the model — it is precisely
why the constant had to go 4→5. The claims.yaml pin is on the constant, which does
not move; only the rationale comment beside it was stale.

Verification

• cargo test --workspace — no failures
• cargo clippy --workspace --all-targets -- -D warnings — clean
• cargo fmt --check — clean
• python3 scripts/claim_check.py claims.yaml — 43/43
• wcet_bound_gate — 44 → 47 executed tests, all green
• frozen_codegen_bytes — green (byte-invisible)

No [Unreleased] edit, no version bump, no artifacts/status.json regen.

Named follow-up

scan_for_decline reports only the first decline per function, so the 30-reachable
figure is a static-set argument rather than an observed one. A whole-object
--emit-wcet run would confirm which of the 30 occur in practice.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[codecov]

Codecov Report

❌ Patch coverage is 97.66082% with 4 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-backend/src/wcet_loops.rs	97.66%	4 Missing ⚠️

📢 Thoughts on this report? Let us know!