feat(selector): RQ-64-MVLOWER (#1093) — parameter-taking block types LOWER on the ARM direct selector (--relocatable), proven per shape by the #1097 oracle; every other leg stays declined with its measured reason

[avrabe]

RQ-64-MVLOWER (#1093): parameter-taking block types LOWER on the ARM direct selector (--relocatable), proven per shape by the #1097 oracle — and every other leg stays declined with its measured reason

Artifact: artifacts/release-v0.64/RQ-64-MVLOWER.yaml → implemented. Refs #1093, #1097.

The constraint, and how it was met

No shape's decline was relaxed without scripts/repro/param_block_silent_1097_differential.py passing for it. The oracle asserted refusals == 6 unconditionally, so it structurally could not pass for a lowered leg; it was strengthened first (commit 1, behaviour-identical, negative control captured), never paralleled or weakened:

• a per-leg LOWERED mode: a listed (shape, backend) must compile and every vector must equal live wasmtime on the NEW object — the fixture's pinned silent-wrong vectors, its match vectors, extra probes (both signs + the i32 wrap boundary), and a per-construct _lowered.wat sub-shape module; a lowered leg with nothing to execute FAILS;
• refusals: and lowered legs: pinned exactly in ci.yml (the fix(oracle): #1104 shadowed the aarch64 builder guard and left its oracle pinned to the superseded wording #1112 pattern) — a leg moves between the counts only in the PR that relaxes its guard;
• the RED half (pre-RQ-61-MVPANIC (#1093): parameter-taking block types decline loudly on ARM and RV32 — the aarch64 VCR-A64-CF-001 refusal ported #1096 bytes pinned wrong) is untouched.

Every relaxation went red-first: the leg was listed LOWERED on the previous binary (compile declines → exit 1, captured), then the lowering landed, then green.

Verdict per shape (ARM direct selector, --relocatable — the one configuration the oracle executes)

shape	verdict	evidence
block (param ..)	LOWERED	14/14 vectors. Params are plain operand-stack entries; #509's designated-result-register landing already reconciles every forward edge (the pre-#1096 fixture matched for that reason). Zero selector lines.
if (param ..)	LOWERED	16/16 vectors. The artifact's vector: pre-#1096 ipe(0) returned 0xC0DE0003 (uninitialized R3); it now returns wasmtime's 7. Checkpoint below the params; params snapshotted at If, re-pushed at Else; else-less if joined like a two-arm if (B end; else: MOV R_then, R_param), moves PLANNED first, parallel-move hazards decline loudly with nothing emitted. Includes the #1093 panicking two-param if/else repro.
loop (param ..)	LOWERED	17/17 vectors. Private header register per parameter, reserved for the loop's extent like #509's result_reg, written by every back-edge (same hazard check). Retires the #509 "br to a loop header with N loop parameter(s)" refusal on this path. The RV32-pinned lpb(3) (2, want 10) is 10 on ARM.
all three, ARM self-contained image path	still declined	no #1097 oracle leg executes those images (the harness loads ET_REL leaf objects); the same selector code is not the same evidence. The decline names the path.
all three, RV32	still declined	the RV32 selector has NO blocktype-arity plumbing; reconcile_br_edge records entry ABOVE the params so a param frame's br_if "carries nothing" (the pinned uninit-T2 vector); the loop back-edge mis-reconciles (lpb(3) 2 want 10); compile_function_with_opts is MC/DC-pinned at 10 branches. None attempted.
AArch64	still declined	VCR-A64-CF-001's single-slot design; no oracle leg.
if/loop whose inputs are not on the operand stack (multi-value CALL result, spec if.wast add64_u_saturated)	still declined, loudly	the direct selector models a multi-value call result as one entry; multi-value call results themselves already fail the check_no_underflow pre-flight (both backends).

The guard is now a policy, not a predicate: synth_core::ParamBlockLowering + arm_param_block_lowering(relocatable) + find_unlowered_param_block_type, defined once and read by both ARM guard sites, keyed on --relocatable.

Found while proving it — a register-alias clobber, and it is on main

local.get of an R0–R3 parameter pushes the HOME register by alias, so a then-arm ending in local.get 0 makes the join's else-path mov write local 0. Adding such vectors to the oracle went RED on this lane's first if-lowering (ipa(0) 14 want 7; ipq(0) 16 want 8); canonicalize_then_results copies an aliased then-result into a private temp on the then path and both are green.

The parameter-free #313 join has the identical exposure on main — measured on the base binary (16721807), relocatable ARM:

(func (export "al") (param i32) (result i32)
  (if (result i32) (local.get 0) (then (local.get 0)) (else (i32.const 9)))
  (local.get 0) (i32.add))

al(0) → 18, wasmtime 9; exit 0, silent. Deliberately NOT fixed here — it moves bytes outside this lane's acceptance oracle and needs its own red-first oracle and byte accounting. Filed by the coordinator as #1189, owned by a separate lane; this PR leaves it alone.

Measured, not argued

• Byte-identity, base (16721807) vs this tree, scripts/repro/*.wat × 3 legs (arm-reloc, arm-self, rv32-reloc), whole-object compare: 356 identical / 0 differing / 0 newly-declined / 6 newly-ACCEPTED (the six param-taking modules, arm-reloc only). Every parameter-free construct is byte-identical (lowerings keyed on params > 0).
• Reach, spec suite if.wast on --relocatable: base skipped 16 functions (8 param-taking declines); now 13 skipped, 0 param-taking declines — 5 of the 8 lower, 2 fall through to the pre-existing Direct selector miscompiles value-returning br_table — carried value dropped (affects --relocatable/shipped path) #509 "br to a result-typed if/else join" decline, 1 to the multi-value-call decline.
• Oracle counts: refusals 6 → 3; lowered legs 0 → 3 (51 vectors); emulation header 19 → 70; the exact emulation floor RE-DERIVED by oracle_wiring_check.py on the lane tree and moved in ci.yml + claims.yaml together.
• Ratchets: selector_lines_code grew in three waived steps (each reason names what the lines are and that nothing could be deleted in exchange — the class had no lowering to retire); wildcard arms unchanged (55/90 — let .. else / matches!, no _ =>).
• Tests: fmt/clippy clean; synth-core + synth-synthesis + synth-backend suites green, 11 new unit tests (policy predicate, path-keyed policy, relocatable-only acceptance per construct, reconcile/canonicalize negative controls: swap, i64 overlap, arity/width mismatch, aliased then-result copied to a private temp).

#973 ARM corpus sweep — the retired guard says so

The sweep compiles every scripts/repro/*.wat at cortex-m4f --relocatable --all-exports — the path this PR relaxed — so its ratchet arm fired on the three param_block_silent_1097_{block,if,loop}.wat EXPECTED_DECLINES entries. Their guard comment forbade removal "by lowering the shapes without passing that oracle first"; that precondition was discharged (the oracle now asserts lowered legs: 3 where it asserted refusals: 6), and the comment is rewritten to record the discharge — by whom, with what evidence, which assertion replaces the entries, and which legs stay declined on paths the sweep does not compile. Its new-decline arm did NOT fire: the three _lowered.wat fixtures compile there and Phase B executes them (block 4 exports, if 8, loop 4, ×12 vectors) — a second, independent execution oracle over the same lowerings. Measured: PHASE A fixtures=180 compiled=164 declined=16 hard-error=0; PHASE B 53 modules, 2744 vectors, 0 mismatches, 0 faults; PASS.

Earlier: rebased onto f4780608 (#1184 MACHO, #1187 CFOBLIG) — re-derived, not carried

Clean replay of all five commits. On the merged tree: oracle_wiring_check.py derives the emulation floor to exactly the pinned value (MACHO's oracle is compiles-mode and does not move it); claim_check.py 62/62 with the selector ratchets unchanged (main did not touch the selector); status_evidence_check.py 0 failures, floor-prose 0 restatements; the #1097 oracle and the #973 sweep re-run PASS on a binary built from the merged tree; three-crate tests + fmt + clippy green.

Merged with main at e96d23ff (#1190, the #1189 fix) — one mechanism, not two

Both lanes independently built the then-result alias copy at the if join. The merge keeps #1190's liveness-gated copy as the single mechanism and deletes this PR's canonicalize_then_results (and its unit test): main's inline Else block is lifted verbatim into copy_live_home_then_results (returns the emitted count so cf accounting is identical) and called at both joins — Else (every if, #1190) and the RQ-64 implicit-else join at End with end_idx = idx. What this PR still adds on top of it for parameter-taking ifs: the checkpoint landing below the params, the param snapshot/re-push, and the else-less join as an empty explicit else with the planned-move hazard check. git checkout --ours would have dropped #1190's general fix; it was resolved hunk by hunk instead.

#1189 not regressed, measured on the merged binary: join_alias_1189_differential.py → refusals: 1; silent-wrong vectors: 14 (of 14 pinned); fixture match vectors: 60; live vectors: 149 matched, 0 diverged (of 149); PASS. The oracle was not touched.

Counters derived on the merged tree, never carried: exact emulation floor oracle_wiring_check.py → 325121 (ci.yml + claims.yaml in lockstep; neither side's number); selector_lines_code → 19740 with BOTH lanes' waivers kept and a third waiver at the merged value explaining it is the sum of two landed growths minus the deleted duplicate (19663 mine, 19355 main's: the merged value is below their deltas summed); selector_lines_total → 30565; wildcard code arms unchanged (55); claim_check 62/62; status_evidence_check 0 failures, floor-prose 0; status.json regenerated, not hand-merged. #1097 oracle on the merged binary: refusals 3, lowered 3 (51 vectors), PASS. #973 sweep on the merged corpus (now 183 fixtures incl. #1189's): 167 compiled, 16 declined, 2936 vectors, 0 mismatches, PASS. Three-crate tests + fmt + clippy green on the merged tree. Byte-identity, main e96d23ff (with #1190) vs the merged tree, scripts/repro/*.wat × 3 legs, whole-object: 364 identical / 0 differing / 0 newly-declined / 6 newly-accepted (the six param-taking modules, arm-reloc only) — every parameter-free module, #1190's own fixture modules included, carries main's bytes unchanged.

Also noticed, left as found (logged, not fixed here; neither is this PR's)

• claims.yaml's RQ-61-MVPANIC (#1093): parameter-taking block types decline loudly on ARM and RV32 — the aarch64 VCR-A64-CF-001 refusal ported #1096 waiver names a test select_with_stack_declines_param_block_types that does not exist in the tree (the pins live in issue_1093_param_block_decline.rs).
• The tree's tests/spec-testsuite is a submodule not initialized in worktrees; the reach probe read the root checkout's copy.

Commits (all signed): oracle mode (behaviour-identical, negative control) → block → if (+ alias finding, oracle strengthened red-first) → loop → #973 sweep guard retired with its discharge recorded.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[codecov]

Codecov Report

❌ Patch coverage is 79.52286% with 103 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
...esis/src/instruction_selector/select_with_stack.rs	67.30%	51 Missing ⚠️
crates/synth-synthesis/src/instruction_selector.rs	78.07%	50 Missing ⚠️
crates/synth-backend/src/arm_backend.rs	90.00%	1 Missing ⚠️
crates/synth-core/src/wasm_op.rs	99.08%	1 Missing ⚠️

📢 Thoughts on this report? Let us know!