plan(v0.59): add RQ-59-POPCNT (#1021) and RQ-59-TIERCENSUS — a proof sitting above a defective expansion

[avrabe]

RQ-59-CRSWEEP verified all 11 critical/high code-review findings against the current binary. Ten were stale records. One was real, and it executes.

RQ-59-POPCNT (#1021) — folded into v0.59

The Thumb-2 i32.popcnt expansion takes R11 as a second scratch — its own comment says "We need a second scratch register. Use R11." — and R11 is the WASM linear memory base. The A32 transcription (#615) deliberately mirrors that register contract and inherits the defect.

Executed differential (unicorn vs wasmtime, --cortex-m):

expected	1242
observed	0x20020008

That's popcnt(0xFF)=8 plus the word at address 0 — the vector table's initial SP — because R11 ended as r5>>16 = 0.

R11 is not in the pushed set, so it leaks to the caller and every later [R11] access in the whole call chain reads through the garbage base. Reachable from both selector paths. i64.popcnt is unaffected (R3/R4/R5/R12, all pushed) — a useful control, and a fix should explain why i64 got it right.

Folded into v0.59 rather than cut as v0.58.1; the precedent for the other choice was v0.56.2, cut mid-v0.57 for the #959 identity-mask OOB.

RQ-59-TIERCENSUS — the finding behind the finding

rule_i32_popcnt is Rocq-proved. It emits the ArmOp::Popcnt pseudo-op, and the defect lives in that pseudo-op's encoder expansion. The proof is stated at pseudo-op tier, above the expansion — so it certifies "the selector emits Popcnt correctly" while the thing Popcnt becomes destroys the memory base.

Same shape as v0.57's ArmSemantics::encode_op silently no-oping 87 of 222 ops, one layer lower: there the model didn't reach the instructions; here the proof doesn't reach the expansion.

This artifact is a census, not a fix: of the 80 proved rules, how many emit pseudo-ops; which of those expansions are unguarded by proof, frozen anchor, or execution differential; and which use registers outside the pushed set as scratch (#1021's mechanism). Report and stop — the tier-boundary fix is a v0.60 program.

A census finding the unguarded set is small is as valuable as one finding it large: it would mean #1021 is near a one-off rather than systemic, and that changes how v0.60 gets scoped.

claim_check 49/49. Rivet artifact only.

Refs #1021, #242.

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!