feat(reach): RQ-65-MVPCORE (#1017) — MVP core re-derived on the executed path: single-module .wast routing (oracle first), merge refusals, start-function invocation; 14/114 -> 12/80

[avrabe]

RQ-65-MVPCORE (#1017) — the MVP-core row, re-derived on the path the oracles execute

Refs #1017, #1225, #1046, #1217. Filed on the way: #1225, #1229, #1230, #1231.

The measured delta, stated plainly (per backend, ok / partial)

set	backend	before (main 580d53f9)	after (this PR)	delta ok
corrected MVP core, 80 files	arm	13 / 31	12 / 21	-1
	riscv	10 / 31	9 / 23	-1
	aarch64	18 / 12	18 / 20	0
v0.63's MVP core, 114 files	arm	14 / 39	12 / 22	-2
	riscv	11 / 38	9 / 23	-2
	aarch64	21 / 17	18 / 20	-3

The reach increment (start-function invocation) moved ZERO files on every backend. Its four sole-blocker files are multi-module (start, annotations, binary) or a multi-memory twin (start0). The gain is module-level, in the parity oracle's own line: start-function modules: 4 seen, 2 both-accepted and booted ..., 10 assertion(s) ok — 0 both-accepted on the compiler before it. That is the file-vs-module gap v0.63's caution predicted, measured rather than assumed.

The row went down, and every mover was inspected: losses are refusals of objects that were wrong (int_exprs i64 signatures, const 402 f32/f64-result modules, stack accessed globals, binary-leb128/memory/address/float_memory data — aarch64 refuses data-carrying modules on the real path since v0.53); gains are first real compiles (nop/load → ok on arm once a real call_indirect table reached the backend; on aarch64 f32, f32_bitwise, f32_cmp, f64_bitwise, f64_cmp, float_misc, conversions → ok, and 12 core files from whole-file refusal to partial).

Why both numbers in "14 / 114" were properties of the instrument

1. Denominator. 31 multi-memory-proposal twins (address0, load0..2, memory_size0..3, data0/1, imports0..4, start0, ... — content-verified at 2..21 memories per module, suite commit 4b24564) and 3 relaxed-SIMD lane files sat in MVP core because spec_compile_census.py's family regexes predate the Wasm 3.0 merge (^multi.?memory|^memory_multi matched none; ^data\b cannot match data0). MVP core is 80 files; multi-memory is a family row and a FAMILY_OK_PINS entry. v0.63's top arm blocker (17 files sole) was a multi-memory decline mis-filed as scalar-core.
2. Numerator (The spec-suite census compiles .wast files on a path no oracle executes — it never sets R9, drops data segments and global initializers at exit 0 #1225, the "correct by accident" finding). synth compile file.wast — the census invocation — took the multi-module MERGE branch, written for synth's i32-only fixture suite and saying so beside every Vec::new() it passes. It handed the backends empty data segments, empty globals (the Cortex-M startup never wrote R9), i32-only signature tables and a default aarch64 substrate. One module compiled as .wast vs .wat: no data bytes and no R9 write on the .wast leg while get_g was ldr.w r4, [r9] on both; tests/wast/i64_arithmetic.wast's i64.add on two i64 params lowered as adds r3, r0, r1 (param 0's low half plus its own high half). Exit 0, counted ok. The parity oracle compiles per-module .wat — the other path — so the number the project planned from was measured on objects no oracle runs (the shape The spec-suite gap was declared closed by a COMPILE census — the behavioural half stayed open and nothing sampled it until #197 #1217 asks to sweep for).

Oracles landed FIRST, both red before

• scripts/repro/wast_single_module_path_identity_1225.py (new, wired into the Spec Suite workflow, # ci-checks: compiles >= 600): a single-module .wast must compile to exactly the bytes its module compiles to alone, three backends. Red on the pre-fix driver: arm 49 / riscv 33 / aarch64 56 of 140 mismatched. Then the driver routes a single-module .wast through the single-module path → 140 / 140 / 140 identical, RESULT PASS; the multi-module merge REFUSES a module carrying active data segments, accessed globals or a non-i32 signature over the functions it would retain (refuse_wast_merge_unrepresentable).
• selector_parity_197_differential.py stopped declining (start ...) modules and gained START_MODULES_FLOOR. Red on the pre-invocation compiler (--only start: 4 seen, 0 both-accepted, both legs module-decline). Then the self-contained Cortex-M Reset_Handler BLs the start function after the data copy and the R9 table, before the entry BLX r0 (a BL, never BLX r0 — the oracle's boot scanner stops at the first blx r0), patched post-layout via encode_thumb_bl; the closure is seeded with it. Green after: 2 both-accepted and booted, 10/10 assertions ok (get observes three incs from the start function on both selectors and in wasmtime), 0 divergences. Every other path — --relocatable, ET_REL degradation via imports (checked after compilation), an imported start, the single-function path, A32, RISC-V, AArch64 (neither of the last two emits a startup) — keeps the ALL backends SILENTLY DROP the (start ...) function — exit 0, never compiled, never run (same silent-drop class as #1041) #1046 refusal; start_section_refusal_1046.rs pins both halves (10/10, two new refusals).

Declined with measured reasons (docs/status/SPEC_FAMILY_CENSUS.md, ranked on the v0.65 path)

• the 22 multi-module MVP-core files the merge now refuses (9 signatures / 7 globals / 6 data) — the next lever is per-module compilation, a census-shape change;
• GI-FPU-002 f32/f64 is the census's no-FPU --cortex-m target: the same 80 files on --target cortex-m7dp measure 17 / 22 vs 12 / 21 — changing the invocation would move every pin to flatter one target;
• aarch64 br_table with value-carrying targets (2 sole, 13 files, 90 functions), visible now that the merge's "declares no globals" refusal no longer hides it;
• call_indirect self-contained dispatch stays silicon-gated (fix(#275): self-contained --cortex-m call_indirect — loud-decline the R11/linmem silent miscompile #717); multi-memory in a self-contained image is a multi-memory decline (Multi-memory phase 2: per-memory MPU isolation is unreachable — --safety-bounds mpu and multi-memory have disjoint paths #1145, no memory-k oracle);
• filed: arm direct selector: 'stack underflow: malformed WASM or compiler bug' on VALID spec modules — 74 functions / 6 MVP-core files, never a file's sole blocker #1229 (arm "stack underflow" on VALID modules, 74 functions, 0 sole — the exact v0.63 trap), VCR-RA-003 refuses its own emitted stream on spec modules: JoinValueNotAvailable { reg: R4 } on br/br_if/br_table/labels (+ an R5 instance) — a caught would-be miscompile #1230 (VCR-RA-003 JoinValueNotAvailable, a caught would-be miscompile), aarch64 selector: operand-class confusion — 'local.set: expected GP operand, got FP' / 'fcompare: expected FP operand, got GP' across the float MVP-core files #1231 (aarch64 GP/FP operand class).

Pins moved with the measurement, together

Census PINS / AT_LEAST_ONE_EXPORT / FAMILY_OK_PINS (whole-suite ok 22 / 12 / 27 → 16 / 9 / 21; at-least-one-export 84 / 74 / 57 → 47 / 43 / 47; other_error 0 / 0 / 0 — the VCR-MEM-002 multi-memory (#406) decline family reaches the census for the first time and is classified by its tag), README row, feature_matrix.md.tmpl (FEATURE_MATRIX.md regenerated by claim_check.py --emit-status), claims.yaml (SYNTH-SPEC-FAMILY-MVP-CORE, SYNTH-SPEC-SUITE-CENSUS-README/-MATRIX, a new count-min on the identity oracle's wiring). Emulation floor re-derived on the rebased tree by oracle_wiring_check.py: equal to the ci.yml/claims pin, so it does not move (the new oracle declares a compiles floor).

Note on generation: SPEC_FAMILY_CENSUS.md is TRANSCRIBED from the census's per-family stdout (the v0.63 cold review corrected "generated" to "transcribed"; FAMILY_OK_PINS in the script is the gate that reddens the census when a family count moves). FEATURE_MATRIX.md IS generated and was regenerated from the template.

Gates run on the rebased tree (761c6922 + this branch), release binary rebuilt there

• scripts/spec_compile_census.py: RESULT PASS on the new pins, all three backends (MVP core 80 files: arm 12 / 21, riscv 9 / 23, aarch64 18 / 20; other_error 0 / 0 / 0).
• scripts/repro/wast_single_module_path_identity_1225.py: RESULT PASS, 140 / 140 / 140 identical, 420 file-backend pairs compared.
• scripts/repro/selector_parity_197_differential.py, full corpus: RESULT PASS — 330 modules both-accepted, 19155/19155 assertions in parity, 622 pinned divergences across 103 pins (RQ-65-DECLINE's converted pins merged), 0 unpinned; start-function modules: 4 seen, 2 both-accepted and booted ..., 10 assertion(s) ok, 0 divergences. (Pre-rebase tree: also PASS, 722 pinned across 108 pins.)
• cargo test --workspace: 80 test binaries, 1293 passed, 0 failed.
• cargo clippy --workspace --all-targets -- -D warnings: clean. cargo fmt --check: clean.
• scripts/status_evidence_check.py: 0 failures (5 delivery-shaped commits in the window, 5 attributed; live floor restated 0 times). scripts/claim_check.py claims.yaml: 63/63 hold; --emit-status leaves every generated file unchanged.
• scripts/oracle_wiring_check.py: every script declared and wired; the derived emulation floor equals the ci.yml/claims pin, so it does not move.
• rivet validate: 40 errors — the pre-existing cross-repo baseline; this artifact adds no links.

Both pushes went through one && chain (fmt, clippy -D warnings, evidence check, claim check, push).

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[avrabe]

Coordinator verification of #1225 — reproduced independently, and it is a silent miscompile of the plainest possible shape

Not a re-read of the lane's report. Compiled synth's own tests/wast/i64_arithmetic.wast with the
main binary (761c6922) and with this branch's, and decoded .text directly rather than trusting a
disassembler rendering.

The function is (func (export "add") (param i64 i64) (result i64) local.get 0 local.get 1 i64.add).
Under AAPCS, param0 is r0:r1 and param1 is r2:r3.

main (the census's own compile path):

e92d4010  push {r4, lr}
e0903001  adds r3, r0, r1     <- adds param0's LO to param0's HI
e0a11002  adc  r1, r1, r2     <- param0.hi + param1.lo
e1a00003  mov  r0, r3
e1a01001  mov  r1, r1
e8bd8010  pop {r4, pc}

this branch:

e92d4010  push {r4, lr}
e0900002  adds r0, r0, r2     <- param0.lo + param1.lo
e0a11003  adc  r1, r1, r3     <- param0.hi + param1.hi
e1a00000  mov  r0, r0
e1a01001  mov  r1, r1
e8bd8010  pop {r4, pc}

Every parameter was being homed at r_i — the narrow, one-register-per-local model — so a two-i64
add summed the two halves of the same argument. exit 0, no decline, no warning, and the census
counted the file ok.

A second symptom worth recording: the object produced by that path has no .symtab at all
(sections are .text, .shstrtab, .ARM.attributes), while the CLI's own success message tells the
user to run objdump -t to see symbols. Any consumer reading symbols from that object gets nothing.

On the headline number. "MVP core is 14/114" was wrong in both halves and this artifact says so:
the denominator carried 31 multi-memory twins and 3 relaxed-SIMD files that are not MVP core, and the
numerator counted files compiled on this path. Re-deriving on the executed path moves arm 14/114 to
12/80. That the corrected number is lower is the right outcome to publish.

And the reach increment gained ZERO files, reported as such — which is exactly what the artifact
demanded ("report the MEASURED delta including if it is zero") and what the v0.63 precedent predicted.
The gain is real but module-level: 4 start modules seen, 2 both-accepted and booted, 0 before.

Refs #1225, #1017

[avrabe]

Coordinator: merge-order hazard between #1227 and #1232 — do not merge these in either order without re-deriving

Measured, not reasoned. Both PRs are green on their own base; together they break main.

#1227 pins #1226 red-first on an observable:

grep -Eq '^WIDTH-1226: known-open \(\.wast homes < \.wat homes for the same module text on 4 legs\)$'

Its fixture scripts/repro/home_alias_width_1226.wast is a two-module .wast — deliberately, because
the mis-homing lives in the multi-module merge path.

#1232 makes that merge path REFUSE any module it would mis-home (any(&module.func_params_i64) →
"signature tables are i32-only, so an i64 parameter pair is mis-homed"). Compiling #1227's fixture with
#1232's binary:

exit=1   Refused ... i32-only ... mis-homed

So once #1232 lands, the fixture no longer compiles, the audit cannot measure homes= on it, and
#1227's WIDTH-1226 grep fails. Green PR CI on a stale base, merges clean, reddens main.

A correction to my own first reading, recorded because it changes the conclusion. I initially tested a
single-module (param i64 i64) (result i64) local.get 1 and found #1232 emitting the correct pair
(mov r0,r2; mov r1,r3), and concluded #1232 had fixed the mis-homing. Then I ran the same input on
main's binary and got identical bytes — body inference recovers the width in that shape, so the test
discriminated nothing. The defect is specific to the merge path, which is exactly why the fixture is
two-module. #1232 converts a silent mis-homing into a loud refusal; it does not thread the widths.

Consequences to settle before either merge:

1. Merge order: feat(reach): RQ-65-MVPCORE (#1017) — MVP core re-derived on the executed path: single-module .wast routing (oracle first), merge refusals, start-function invocation; 14/114 -> 12/80 #1232 first, then fix(selector): RQ-65-ALIASCLASS (#1189) — enumerate every uncopied home-register consumer on four legs; fix aarch64 rotl (#1221) and i64-param local.set (#1222) red-first; pin #1223/#1226 open #1227 rebases and re-derives its #1226 observable against a tree
   where the multi-module fixture is refused. A refusal is not a homes= count, so the pin needs a
   different expression — or the fixture needs to reach the defect by a route feat(reach): RQ-65-MVPCORE (#1017) — MVP core re-derived on the executed path: single-module .wast routing (oracle first), merge refusals, start-function invocation; 14/114 -> 12/80 #1232 still compiles.
2. Is .wast driver path threads NO declared param/result width tables — every i64/f32/f64 param or result in ANY .wast module (single-module too) is homed as i32 unless body inference recovers it (was: multi-module merge / representative table) #1226 still open? After feat(reach): RQ-65-MVPCORE (#1017) — MVP core re-derived on the executed path: single-module .wast routing (oracle first), merge refusals, start-function invocation; 14/114 -> 12/80 #1232 the multi-module path emits no wrong bytes because it emits
   nothing. That is decline-honesty, which this project counts as the correct trade — but it is a reach
   loss, not a width fix. My reading is that .wast driver path threads NO declared param/result width tables — every i64/f32/f64 param or result in ANY .wast module (single-module too) is homed as i32 unless body inference recovers it (was: multi-module merge / representative table) #1226 stays open and changes character from "silent wrong
   answer" to "refused", and fix(selector): RQ-65-ALIASCLASS (#1189) — enumerate every uncopied home-register consumer on four legs; fix aarch64 rotl (#1221) and i64-param local.set (#1222) red-first; pin #1223/#1226 open #1227's note that the arm direct selector: local.set/local.tee of a register-homed i64 PARAM writes only the lo half (leaf functions), and the #989 snapshot can land on val's hi #1222 pair-write never fires on .wast still stands.
   The lane that owns it should confirm on the merged tree rather than take my word.

Refs #1226, #1225, #1222

[avrabe]

Correction: my earlier "correction" was wrong — #1232 DOES fix the single-module .wast mis-homing

I posted a hazard note saying I had first concluded #1232 fixes the mis-homing, then "corrected"
myself after finding main emitting identical bytes, and concluded the defect was specific to the
multi-module merge path. That correction was the error. The original reading was right.

Cause: both worktrees shared one CARGO_TARGET_DIR, so ./target/debug/synth belonged to whichever
tree built last. When I believed I was running main's binary I was running #1232's.

Re-measured with each branch built into its own target dir, same input
((module (func (export "f") (param i64 i64) (result i64) local.get 1)), a single-module .wast):

binary	.text	verdict
main	e92d4010 e1a00001 e8bd8010	mov r0, r1 — mis-homed
#1232	e92d4010 e1a00002 e1a01003 e8bd8010	mov r0, r2; mov r1, r3 — correct pair

So the ALIASCLASS lane's mechanism note was accurate as written: ANY .wast mis-homes on main,
single-module included, because the .wast decode arm threads no declared-width tables. #1232 fixes
the single-module case outright and refuses the multi-module case.

What this does and does not change:

• The merge-order hazard STANDS, for the reason I first gave. fix(selector): RQ-65-ALIASCLASS (#1189) — enumerate every uncopied home-register consumer on four legs; fix aarch64 rotl (#1221) and i64-param local.set (#1222) red-first; pin #1223/#1226 open #1227's WIDTH-1226 red-first pin
  needs its two-module fixture to COMPILE so it can compare homes= counts; feat(reach): RQ-65-MVPCORE (#1017) — MVP core re-derived on the executed path: single-module .wast routing (oracle first), merge refusals, start-function invocation; 14/114 -> 12/80 #1232 refuses it. Merge
  feat(reach): RQ-65-MVPCORE (#1017) — MVP core re-derived on the executed path: single-module .wast routing (oracle first), merge refusals, start-function invocation; 14/114 -> 12/80 #1232 first, then rebase fix(selector): RQ-65-ALIASCLASS (#1189) — enumerate every uncopied home-register consumer on four legs; fix aarch64 rotl (#1221) and i64-param local.set (#1222) red-first; pin #1223/#1226 open #1227 and re-derive that observable.
• .wast driver path threads NO declared param/result width tables — every i64/f32/f64 param or result in ANY .wast module (single-module too) is homed as i32 unless body inference recovers it (was: multi-module merge / representative table) #1226's disposition changes. After feat(reach): RQ-65-MVPCORE (#1017) — MVP core re-derived on the executed path: single-module .wast routing (oracle first), merge refusals, start-function invocation; 14/114 -> 12/80 #1232 the single-module path emits correct bytes and the
  multi-module path emits nothing, so the wrong-bytes symptom is closed on both routes — one by a fix,
  one by a refusal. fix(selector): RQ-65-ALIASCLASS (#1189) — enumerate every uncopied home-register consumer on four legs; fix aarch64 rotl (#1221) and i64-param local.set (#1222) red-first; pin #1223/#1226 open #1227 should re-state whether .wast driver path threads NO declared param/result width tables — every i64/f32/f64 param or result in ANY .wast module (single-module too) is homed as i32 unless body inference recovers it (was: multi-module merge / representative table) #1226 remains open as a reach issue (the merge
  path declining input it used to accept) rather than a correctness one.
• Note a single-module fixture would NOT reproduce the defect after feat(reach): RQ-65-MVPCORE (#1017) — MVP core re-derived on the executed path: single-module .wast routing (oracle first), merge refusals, start-function invocation; 14/114 -> 12/80 #1232 either, since feat(reach): RQ-65-MVPCORE (#1017) — MVP core re-derived on the executed path: single-module .wast routing (oracle first), merge refusals, start-function invocation; 14/114 -> 12/80 #1232 fixes
  that route. If the pin must survive, it needs a shape feat(reach): RQ-65-MVPCORE (#1017) — MVP core re-derived on the executed path: single-module .wast routing (oracle first), merge refusals, start-function invocation; 14/114 -> 12/80 #1232 still compiles AND still mis-homes — and
  it is a legitimate outcome to conclude no such shape exists and retire the pin with that reason.

Method note, since it cost two wrong claims: never compare two branches' binaries through a shared
CARGO_TARGET_DIR. Build each into its own, or you are comparing a tree against itself.

Refs #1226, #1225, #1017

[codecov]

Codecov Report

❌ Patch coverage is 87.13450% with 22 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-cli/src/main.rs	87.13%	22 Missing ⚠️

📢 Thoughts on this report? Let us know!