RQ-61-MVPANIC (#1093): parameter-taking block types decline loudly on ARM and RV32 — the aarch64 VCR-A64-CF-001 refusal ported

[avrabe]

Closes #1093.

What this is

Valid multi-value wasm — (if (param i32 i32) (result i32) ...) — panicked the ARM direct selector (select_with_stack.rs:3674) and the RV32 selector (selector.rs:3164): `at` split index (is 2) should be <= len (is 1), exit 101 on 7 of 8 invocation paths. Only aarch64 declined cleanly (the issue's table said rv32 declined too — it did not; reproduced before touching anything). Both selectors checkpoint the operand stack at frame entry and a parameter-taking block type consumes operands below the checkpoint.

Port, not a third variant: the predicate and message live once in synth-core (find_param_block_type / param_block_decline_msg — the aarch64 open_slot params != 0 refusal ported; the shared needle PARAMETER-taking block type matches aarch64's message so one parity probe covers all three backends). Call sites: compile_wasm_to_arm (the choke point BOTH ARM codegen paths cross), select_with_stack pre-flight (direct library callers), rv32 compile_function_with_opts (+ the module path now threads func.block_arity into the per-function config). aarch64 keeps its in-selector check: it is entangled with reconciliation-slot reservation and also covers the results > 1 case, and its message is pinned by cross_backend_op_parity.rs.

DO-NOT honored: this is a loud decline, NOT multi-value support.

The class sweep found the silent direction was worse (all measured, unicorn vs wasmtime)

shape	before	after
if (param ..) .. else	PANIC exit 101, ARM both paths + RV32	named decline
if (param ..) no else	exit 0, SILENTLY WRONG — ipe(0) → 0, want 7, all 4 ARM/RV32 legs	named decline
block (param ..) + br_if	RV32 exit 0, wrong join value (bpb(1) → 10, want 15); ARM correct	named decline
loop (param ..) + back-edge	RV32 exit 0, wrong (lpb(3) → 2, want 3); ARM declined (#509)	named decline
block/loop (param ..) fall-through only	exit 0, correct (measured 20/20 vectors)	named decline

The last row is the one deliberate behavior change for previously-correct input: the branch-free fall-through shape is correct only by accident of the vstack flowing through, telling it apart from the broken shapes would be a NEW predicate with its own proof burden, and aarch64 already refuses it — so the whole class declines, exactly like aarch64 (#1013 policy: match the existing refusal).

Gates

• Red-first: exit 101 shown on all 7 paths pre-fix (6 shapes x 8 invocations = 48 runs post-fix: 0 panics, all named declines, matrix in the lane transcript).
• Vendored spec suite, all 257 files: pre-fix exactly one panicking file per backend (if.wast); post-fix 0 compile panics on both --cortex-m and rv32 legs. if/block/loop.wast produce 8/7/9 named param-declines.
• Byte-identity: origin/main binary vs this branch over scripts/repro/*.wat x 5 legs (cortex-m image, ARM plain, ARM relocatable, rv32 plain, rv32 relocatable): 835 (fixture, leg) pairs, 0 differ (exit codes and output bytes).
• Differential corpora: arm_corpus_sweep_973.py PASS — compiled 154/167 (floor 144), 2502/2502 vectors, 0 mismatches; EXPECTED_DECLINES unchanged (no repo fixture contains a parameter-taking block type — grepped).
• In-tree tests: 9 new tests across synth-synthesis / synth-backend / synth-backend-riscv incl. negative controls ((0,1) if/else and empty side-table still compile); issue_509_br_value_carry updated — the loop-param shape now declines at frame OPEN (subsumes the Direct selector miscompiles value-returning br_table — carried value dropped (affects --relocatable/shipped path) #509 branch-site decline; the loud-Err property is unchanged, the Direct selector miscompiles value-returning br_table — carried value dropped (affects --relocatable/shipped path) #509 arm stays as defense-in-depth).
• Docs: run_supported.sh no longer claims panics are "optimizer regalloc — all pass with --no-optimize" (FALSE for this class: the panic is in instruction selection, before the optimizer, --no-optimize changed nothing).
• cargo fmt / clippy -D warnings / cargo test --workspace green; claim_check 52/52 (selector_lines_code 19199 → 19213, +14 waivered in the same commit; selector_lines_total 29845 → 29859; status.json regenerated).

Honest residuals

• status_evidence_check.py R4 fires on this branch only (the lane commit is first-parent here). On PR CI the checkout is the synthetic merge commit — lane subjects are not first-parent — and on main the coordinator flips the v0.61 artifact status at merge (release files untouched per the lane contract).
• The RV32 selector's own library API (select_with_signatures) still has no arity channel; every real driver (CLI per-function loop and the module-level compile) passes through the guarded backend entry.
• aarch64's check remains its own (shared-helper consumption there would duplicate, not deduplicate: it needs the results > 1 arm and slot rollback).

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[avrabe]

Coordinator verification — widened the reach-regression check beyond fixtures.

The lane's byte-identity evidence covers scripts/repro/*.wat. I extended it to the 108 real .wasm modules in the tree (loom/toolchain output rather than hand-written fixtures), old binary vs branch binary, three legs each:

108 real .wasm x 3 legs   byte-identical 93 · bytes-moved 0 · REACH REGRESSIONS 0
                          (231 pairs were already declined before this change)
scripts/repro/*.wat x 3   byte-identical 339 · bytes-moved 0 · newly-declined 0
                          ------------------------------------------------------
                          432 (module, leg) pairs, zero drift, zero reach lost

That is the property that actually matters for this change: a new decline is only safe if it declines nothing that previously compiled correctly. Confirmed on real input, not just the fixtures the guard was written against.

Separately verified the class conversion myself, from the emitted bytes rather than the lane's report. The else-less if (param i32) compiled cleanly before this PR and emitted:

movw r1, #7        <- the block PARAMETER
cmp  r0, #0
beq  +8            <- false path skips the then-branch
add  r3, r1, #42   <- r3 written ONLY on the true path
mov  r0, r3        <- result = r3

r3 is never written on the false path — the function returns an uninitialized register and the block parameter in r1 is dropped. wasmtime gives 7. All 12 (shape × path) combinations that panicked, plus the three silent shapes, now exit 1 with a named decline.

Holding the merge for all nine required contexts green by name — currently 3/9 with six queued on ubuntu-latest (#1062).

[avrabe]

Rebased onto 59dbe55b — the 8/9 was accumulating against a stale base.

baseRefOid was 88abab32, i.e. before #1098 merged five new v0.61 artifacts and moved ARTIFACT_FLOOR to 484. GitHub re-runs PR checks when the branch moves, not when the base does, so a PR can sit at a confident green describing a tree that no longer exists.

Verified the real post-merge tree locally before pushing:

status-evidence: 71 artifacts across 16 release files, 39 delivery commits matched,
                 19 done-when predicates evaluated, 0 failures
claim_check 52/52 · rivet 484 artifacts (floor 484)

Commit content is unchanged — only the base moved. Same treatment as #1099.

[codecov]

Codecov Report

❌ Patch coverage is 97.05882% with 3 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-backend-riscv/src/backend.rs	75.00%	2 Missing ⚠️
crates/synth-core/src/wasm_op.rs	98.38%	1 Missing ⚠️

📢 Thoughts on this report? Let us know!

[avrabe]

Rebased again onto b2abf951 — #1099 merged underneath this PR and put R7/R8/R9 live, three rules this branch's green had never been evaluated against.

Verified the combined tree locally before pushing:

status-evidence: 71 artifacts across 16 release files, 40 delivery commits matched,
                 19 done-when predicates evaluated,
                 5 release-scope archaeology checks (0 skipped), 0 failures
claim_check 52/52 · test_status_evidence_check 42 OK

RQ-61-MVPANIC passes all three: its done-when is manual: with a written verified-by (so R2 is satisfied and R9's crate-source trigger does not apply), and its release: v0.61 matches its file's directory (R8).

Second rebase for this PR. That is the real cost of the queue latency in #1062 — while a PR waits, siblings merge and invalidate the green it already earned. Commit content is unchanged both times.

[avrabe]

Holding the merge. All nine required contexts are green and the base is current — but MC/DC structural coverage (RQ-57-MCDC, #912) is RED, and it is not on the advisory list.

Only codecov and codecov/patch are advisory here. MC/DC is a real gate with declared floors and zero headroom on its dead ceiling by design.

Baseline first, before attributing it to this PR

main b2abf951   MC/DC success
main 59dbe55b   MC/DC success
main 88abab32   MC/DC success
main 4e7a179c   MC/DC success
PR #1098 head   MC/DC success
PR #1099 head   MC/DC success
PR #1096 head   MC/DC FAILURE          <- only here

Not environmental drift. This PR causes it.

Diagnosis, from the gate's own design

scripts/mcdc_gate.py carries BRANCH_POPULATION, an exact per-function branch-count pin over 20 scored functions. One of them:

"synth_backend_riscv::backend::compile_function_with_opts": 9,

That is precisely the function this PR modifies — the rv32 arity guard was added there (and the module path now threads func.block_arity). A new guard adds decision points, so the measured branch count no longer equals the pinned 9, and the gate's own test_grown_branch_reds_naming_the_function case fires.

The gate is working exactly as intended. The pin is what makes the MC/DC number non-vacuous: if a function's branch population changes and nobody re-pins it, the coverage figure describes a function that no longer exists. scripts/mcdc_gate.py emits a re-pin block with guard text for this case (test_mismatch_emits_repin_block_with_guard_text).

What is needed

Re-pin compile_function_with_opts to its new measured count, in this PR, with the increase explained — the same visible-diff discipline as the claims.yaml ratchet waivers. The new number must come from the gate's own emitted re-pin block, not from hand-counting the source: the count is over demangled LLVM decisions, not over if statements a human can see.

I verified the two host pre-steps pass locally (cargo test -p synth-mcdc-harness ok; scripts/test_mcdc_gate.py 6 tests OK), so the failure is at the scoring step, which needs the pinned witness binary and a wasm32-wasip1 build. The workflow run is still in progress, so the emitted re-pin block is not yet readable; I will take the number from the log when it lands.

Recording the near-miss plainly: my merge rule is "all nine required contexts green by name, plus baseRefOid current". Both were satisfied. A non-required job being red is outside both checks — and this one is a genuine coverage-integrity gate, not noise.

[avrabe]

MC/DC red addressed (commit a3b0173) — diagnosed from the run-33120589927 evidence, reproduced locally with mcdc_gate.py before changing anything.

1. Branch population 9 → 10 — repinned to 10. True source change: the #1093 guard added one br_if (manifest id 2571, instr=7, at the top of compile_function_with_opts). Value taken from the gate's own REPIN block, with a comment on the pin naming the cause and the covering rows.

2. dead 51 → fixed with rows, ceiling untouched. One mechanism note from the manifest/report diff: the new branch is not itself the dead condition — it is not in any scored decision. witness#208's layout-sensitive reconstruction regrouped the function's scored set (main: {2098 gap, 2099 gap} → branch: {old-2099 gap, old-2104 dead}), pulling a never-executed existing branch into scoring. The prescribed fix is still the right one: new harness export rv_param_block_gate drives the #1093 decline both ways through Backend::compile_function (params=0 void block compiles; params=1/2 decline — 2 is the repro's (param i32 i32) arity), rows added to mcdc_run.sh, driver asserted non-vacuous in the host sanity test.

Local A/B under CI's pinned witness 0.42.0 (macOS reconstruction differs from ubuntu, so deltas not absolutes): baseline 19 dec / 129 cond / 55 proved / 51 dead → with rows 20 / 131 / 56 / 49 dead. Dead falls 2 below the ceiling; every floor-relevant count rises. test_mcdc_gate.py 6/6, harness sanity test green, claim_check 52/52. CI on a3b0173 is the final oracle — watching it now.

[avrabe]

Diagnosis: (a), proven by the manifest diff — and the disposition is (c). No number touched: FLOOR_PROVED stands, CEILING_DEAD stands, the row stays.

The manifest diff (instrument side — the stable surface)

Reproduced both columns from the evidence artifacts (33120546295 main, 33126354714 branch). Per-function branch population: identical for all 20 scored functions except the intended compile_function_with_opts 9 → 10; per-branch (kind, instr_index) signatures byte-identical; totals 175 → 176. Nothing was deleted and nothing real was lost — by the gate's own discriminator this is witness#208 reconstruction, not coverage.

Where proved 60 → 56 actually went

All of it lands on functions this PR does not touch, whose populations did not move:

function	main	branch	note
sp_slot_store	2 proved (full_mcdc)	0 — its decision vanished from the report	same source, same branches, same rows
validate_final_allocation_rv32	27 proved	23	13 decisions regrouped into 12, different branch membership
build_options	4	3
validate_reloc_resolutions	4	3
validate_served_image	0 scored	+2 proved (4 scored)	scored zero conditions on main
runtime_image / spanned		+1 / +1

Net −4. Decisions vanish and appear over unchanged code in both directions — that is layout, not rows.

Your compound-predicate question — checked, and it is not the story

compile_function_with_opts's scored dec 1 / cond 4 / prov 1 / dead 3 is the RaFinalVerdict br_table (1 target proved, 2 targets + default dead) — identical on main (dec 871) and branch (dec 873). Not the guard, and unchanged by this PR. The guard itself (br_if@7) records hits: 7 in run.json and the driver provably reaches both outcomes (return flips 0/1, asserted in the harness host test) — yet the report holds it in no decision at all. A condition witness never scores cannot be proved by any row, so (b) is closed by run evidence, not inference.

Why not chase a driver shape

The FIRST red on this PR — before any harness change, the 14-line backend guard alone — already moved dec 32 → 29 / dead 48 → 51, in different functions than this red. The perturbation is a property of adding code anywhere, not of no_mangle/clamp/this driver. Iterating the driver's shape until reconstruction happens to reproduce main's grouping would be layout dice-rolling — the thing the gate's warning exists to prevent.

Filed, per (c)

• MC/DC gate: the report-side absolute floors are layout-coupled — a 14-line guard anywhere moves unrelated functions' proved counts both directions (witness#208) #1100 — the gate-fragility finding: report-side absolute floors are layout-coupled; BRANCH_POPULATION is the alarm that means something; a floor miss WITHOUT a population mismatch should follow the gate's own ARM: a local written on only ONE arm of a br_if is never zero-initialised — reads uninitialised stack (info disclosure); #970 closed the param half, not this one #990 protocol (re-statement WITH manifest evidence).
• friction: mcdc-json decision reconstruction is layout-sensitive — unrelated linked code regroups scored decisions (26->21, full 6->3) while the manifest branch population is byte-for-byte identical witness#208 — commented with this instance's two new data points (an executed-both-ways branch scored in no decision; a full_mcdc decision vanishing over unchanged code).

The decision that is yours

The gate's #990 block documents the remedy for exactly this state: "a re-statement WITH evidence and not a floor lowered to go green" — its own floors were re-derived 26→21 that way. The evidence above is that re-statement's justification, ready to cite. If you want it applied in this PR, the branch-measured baseline is dec 27 / cond 132 / prov 56 / full 9 / dead 50; the diff is one block in scripts/mcdc_gate.py citing #1100 and the manifest proof. I have not pushed it, per your instruction — say the word and it lands as its own signed commit, or leave the job red-with-stated-cause and gate the merge on the required nine.