Skip to content

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

Merged
avrabe merged 7 commits into
mainfrom
fix/aliasclass-1189
Sep 9, 2026

Conversation

@avrabe

@avrabe avrabe commented Sep 9, 2026

Copy link
Copy Markdown
Contributor

RQ-65-ALIASCLASS (#1189) — the home-register alias class, enumerated on all four legs; two new miscompiles fixed red-first (#1221, #1222), two adjacent defects filed and pinned open (#1223 IR fold, #1226 multi-module .wast widths)

local.get of a register-homed local pushes THE HOME REGISTER uncopied. #677, #989 and #1189 were three consumers that wrote it, each a silent wrong answer found one at a time and fixed at its own site. This artifact asks the question none of the fixes asked — how many others are there? — and answers it mechanically, over emitted instructions and by execution, rather than by re-reading selector arms.

The enumeration, per leg and per consumer, with each site's disposition (GUARD / PIN / FIXED) and the stated bound of the search: docs/analysis/HOME_REGISTER_ALIAS_CLASS_1189.md.

What was built

  1. Static audit, ARM direct selectorcrates/synth-synthesis/src/home_alias.rs: an exhaustive, wildcard-free register-writes table for all 222 ArmOp variants (gp_defs / vfp_defs, pinned by a doc-vs-source sweep: 30 mechanically-verified disagreements, 4 of them possible defects (not doc staleness) #946-style source scan) plus a loop-back-edge-extended liveness walk, independent of the selector's own param_last_read. Hooked at the tail of select_with_stack under SYNTH_HOME_ALIAS_AUDIT; a write to a live local's home that is not the local's own set/tee, and not proven straight-line into an inline epilogue ON THE STREAM, is a loud decline naming op, instruction, register and local. Byte-invisible otherwise (objects identical with and without the variable).
  2. Execution oracle, four legsscripts/repro/home_alias_class_1189_differential.py + three generated modules (scripts/gen_home_alias_class_1189.py): 117 consumer-family functions (i32, i64, promoted-local) that feed register-homed params to one op and RE-READ every home into the result, on ARM relocatable, ARM self-contained (the optimized selector aliases too — vreg_to_arm[dest] = param_reg), RV32 and AArch64; every expected value from wasmtime; declines pinned EXACTLY per (module, leg). Permanent red half: main's own objects for the five affected (module, leg) pairs, 10 pinned wrong vectors that must reproduce every run. CI job home-alias-class-1189-oracle, 1,629 emulations; emulation floor re-derived 325121 -> 326750.
  3. Structural pins for the clean legs, as tests: RV32 params COPY on local.get (the "accident of implementation" the artifact names — a future "alias params on the vstack" change must get past param_local_get_copies_and_no_consumer_writes_the_home_1189 and the oracle's rv32 leg) and a promoted s8 is written only by its own set and the epilogue; AArch64's temp pool is disjoint from x0..x7 and 21 families never write a param home; the optimized path's local vregs are never freed (18 families walked with the same gp_defs table).

What it found — red-first transcript on main (af81978)

live vectors: 990 matched, 9 diverged, RESULT: FAIL (9), every failure naming its value:

leg shape synth (main) wasmtime issue
aarch64 b_rotl(7,3) = rotl(a,b)+a+b 0x3c 0x42 #1221rotl negates the count IN PLACE (neg k, k, the #776 fix's "now-dead register" is a param home in a leaf function); 7 vectors, i32 and i64, all exactly rotl + a - b
arm-reloc / arm-self war64 = get, set, get, add on an i64 param 0x5_0000000e 0x7_0000000e #1222local.set/tee of a register-homed i64 param writes only the LO half, at index_to_reg(i) not the AAPCS pair, with the #989 snapshot reserving only val_lo
arm-self same_twice = (x - x) + x 0x0 0x7 #1223 — the optimized path's IR fold drops the surviving use of x. Not this class; filed, pinned KNOWN_OPEN in the oracle (the recorded wrong value must persist until the fix flips the pin)

#1226 (open, pinned in the sweep) — surfaced BY the #1222 fix: in a multi-module .wast the #1168 merge hands a later module's function the representative module's param-width table (arg counts are re-threaded per module, width masks are not), so an i64 param is homed as i32 and its pair overlaps the next param — (i64 i64 i32): $to at R1:R2. Reproduced with a two-module file; the standalone module is correct. 4 spec-suite functions x 4 legs (memory_{copy,fill,init}64 checkRange, memory_grow64 check-memory-zero) are pinned exactly (function, op, register, local, per leg) until the fix flips the pin. A CLI-merge defect, not the alias class, not fixed here.

None of the 10 open PARITY defects (#1204#1215) is this class; the closest, #1210, is a vstack temp across a call, not a home register.

The fixes, one site each

After the fixes: live vectors: 999 matched, 0 diverged, silent-wrong vectors: 10 (of 10 pinned) from main's captured bytes, known-open vectors: 1 (of 1), RESULT: PASS.

Byte-identity pre-fix vs post-fix over 1,419 compiles / 10,725 functions (spec suite + local corpus, per function from the ELF symtab, arm-reloc + arm-self + aarch64): 58 functions changed, every one an aarch64 function containing rotl or an ARM function that local.set/tees an i64 param; 0 newly declined, 0 newly accepted, 0 rc changes, no skip-set moved. The ARM ones were silently wrong on main and include spec-suite functions the census counted as compiled: fac.wast fac-opt, loop.wast while, local_set/local_tee.wast type-param-i64, the 64-bit bulk-memory checkRanges, memory_grow64 check-memory-zero.

Ledger

Not verified, stated

The 805-module real-world census is not on the lane machine. Hidden encoder-expansion scratch (#1021/#1048 class) is outside the ArmOp-level audit (the expansion-canary gates own it). VFP homes are audited on the m4f sweep legs but not executed under unicorn here. The other three legs have no per-op attribution and are pinned structurally plus by execution, not by an audit of every emitted word.

Refs #1189, #1221, #1222, #1223, #1226, #776, #989, #677

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

@avrabe
avrabe force-pushed the fix/aliasclass-1189 branch from da5b971 to 6505725 Compare September 9, 2026 00:16
@avrabe

avrabe commented Sep 9, 2026

Copy link
Copy Markdown
Contributor Author

Coordinator rebase onto dfbcb5bf — both cumulative counters RE-DERIVED, not carried

Three conflicts, none resolvable textually.

Emulation floor — this one mattered. The branch carried --exact-emulation-floor 326750,
correctly derived on its own base (pre-PARITY, 325121). main had since moved to 345122 via
RQ-65-PARITY's +20000 and RQ-65-FUNCN's +1. Taking either side wholesale would have been wrong, and
taking the branch's side would have silently dropped 18,372 emulations from the enforced floor
a gate weakening that no test would have caught, since the equality would still have held against
the number it was given.

Re-derived from oracle_wiring_check.py on the merged tree: 346751. Both the ci.yml and
claims.yaml pins moved to it, and the provenance comment was rewritten — the lane's 325121 -> 326750 line was stale the instant the rebase landed.

A duplicate key I nearly shipped. My first resolution of the claims.yaml conflict kept both sides
of the provenance block, which left two text: keys in one claim. An assertion caught it. Worth
recording because the obvious verification does not work: yaml.safe_load silently keeps the LAST
value on a duplicate key, so it reports a clean single claim either way. Confirmed clean with a
duplicate-key-strict loader, plus claim_check.py itself.

Ratchet. selector_lines_code re-derives to the pinned 19917 on the merged tree. The waiver
is proportionate and reads honestly — +177 lines, two named causes, and "Nothing could be deleted in
exchange: the class had NO handling."
That is the justification the ratchet asks for. Noted for the
release notes: this pin now carries 18 waivers and sits +2020 above its baseline on a metric whose
declared direction is FALL.

CHANGELOG. main gained the ## [Unreleased] header from #1220. Both bodies kept under the one
header, ALIASCLASS first. Never --ours/--theirs here — nothing in CI reads this file, so a
dropped entry would never redden.

Gates on the rebased tree: ci.yml parses, exact-floor PASS at 346751, status_evidence_check 0
failures, claim_check OK, no duplicate keys.

Refs #1189

@codecov

codecov Bot commented Sep 9, 2026

Copy link
Copy Markdown

Codecov Report

❌ Patch coverage is 92.32633% with 95 lines in your changes missing coverage. Please review.

Files with missing lines Patch % Lines
crates/synth-synthesis/src/home_alias.rs 89.82% 87 Missing ⚠️
...esis/src/instruction_selector/select_with_stack.rs 93.26% 7 Missing ⚠️
crates/synth-synthesis/src/instruction_selector.rs 99.09% 1 Missing ⚠️

📢 Thoughts on this report? Let us know!

avrabe added a commit that referenced this pull request Sep 9, 2026
…the DECLARED width; the fuzz harness was right and the fix over-applied

Salvaged and completed by the coordinator after the lane hit a session rate
limit mid-diagnosis. Three CI reds on #1227, all found only after the rebase.

RED 3 — the substantive one, and the fuzz target was CORRECT.

`i64_lowering_doesnt_clobber_params` asserted that nothing may write R1 while
`LocalGet(1)` still reads it, and caught:

  Mov { rd: R0, op2: Reg(R4) }, Mov { rd: R1, op2: Reg(R5) }

The convenient reading was that the harness encoded the pre-#1222 register
model and should move with the fix. It did not. `i64_locals` carries
body-INFERRED widths (`infer_i64_locals`), not only declared ones — so a param
the signature calls i32, or whose width nobody declared (a direct
`select_with_stack` caller, #1226's stale multi-module width table, invalid
wasm), is homed NARROW by `aapcs_param_layout` and its "hi half" IS the next
param's home. The #1222 pair-write fired there and genuinely clobbered local 1.

So the fix was over-applied, not the harness stale. `declared_wide_params`
now gates the pair arm on the declared width AND the layout having homed it
as a pair; anything else keeps the single-move arm — yesterday's bytes.

Regression test covers both configurations, which is the discrimination that
was missing: undeclared widths write R0 only with nothing touching R1 before
`local.get 1`; declared `(i64 i32)` writes the pair R0:R1 with local 1 in R2.

RED 1 — the audit oracle ran VACUOUSLY in CI. `ROOT` was
`Path(__file__).parent.parent`, which from `scripts/repro/` resolves to
`scripts/`, so it looked for the suite at `scripts/tests/spec-testsuite`,
found nothing and exited 1 having audited 0 functions. Now
`.parent.parent.parent`, matching the working sibling
`selector_parity_197_differential.py` in the same directory. Its FATAL message
also stops guessing ("submodule not checked out?" — it was) and prints the
path it actually looked at plus whether that path exists.

RED 2 — `arm_corpus_sweep_973.py` auto-sweeps every `scripts/repro/*.wat`, so
the new i64 fixture joined the corpus and legitimately declines its 10 `c_*`
exports (i64 compare feeding `i64.extend_i32_u`, #952). Registered in
EXPECTED_DECLINES with that reason; the other 38 exports compile and execute
equal to wasmtime.

Verified: fmt, clippy -D warnings clean, synth-synthesis 760 + suites 0
failed, exact-emulation-floor re-derived 346751 on the rebased tree,
status_evidence and claim_check green.

Refs #1189, #1221, #1222, #1226

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
@avrabe
avrabe force-pushed the fix/aliasclass-1189 branch from 8aabd93 to 2157484 Compare September 9, 2026 04:57
avrabe added a commit that referenced this pull request Sep 9, 2026
…the DECLARED width; the fuzz harness was right and the fix over-applied

Salvaged and completed by the coordinator after the lane hit a session rate
limit mid-diagnosis. Three CI reds on #1227, all found only after the rebase.

RED 3 — the substantive one, and the fuzz target was CORRECT.

`i64_lowering_doesnt_clobber_params` asserted that nothing may write R1 while
`LocalGet(1)` still reads it, and caught:

  Mov { rd: R0, op2: Reg(R4) }, Mov { rd: R1, op2: Reg(R5) }

The convenient reading was that the harness encoded the pre-#1222 register
model and should move with the fix. It did not. `i64_locals` carries
body-INFERRED widths (`infer_i64_locals`), not only declared ones — so a param
the signature calls i32, or whose width nobody declared (a direct
`select_with_stack` caller, #1226's stale multi-module width table, invalid
wasm), is homed NARROW by `aapcs_param_layout` and its "hi half" IS the next
param's home. The #1222 pair-write fired there and genuinely clobbered local 1.

So the fix was over-applied, not the harness stale. `declared_wide_params`
now gates the pair arm on the declared width AND the layout having homed it
as a pair; anything else keeps the single-move arm — yesterday's bytes.

Regression test covers both configurations, which is the discrimination that
was missing: undeclared widths write R0 only with nothing touching R1 before
`local.get 1`; declared `(i64 i32)` writes the pair R0:R1 with local 1 in R2.

RED 1 — the audit oracle ran VACUOUSLY in CI. `ROOT` was
`Path(__file__).parent.parent`, which from `scripts/repro/` resolves to
`scripts/`, so it looked for the suite at `scripts/tests/spec-testsuite`,
found nothing and exited 1 having audited 0 functions. Now
`.parent.parent.parent`, matching the working sibling
`selector_parity_197_differential.py` in the same directory. Its FATAL message
also stops guessing ("submodule not checked out?" — it was) and prints the
path it actually looked at plus whether that path exists.

RED 2 — `arm_corpus_sweep_973.py` auto-sweeps every `scripts/repro/*.wat`, so
the new i64 fixture joined the corpus and legitimately declines its 10 `c_*`
exports (i64 compare feeding `i64.extend_i32_u`, #952). Registered in
EXPECTED_DECLINES with that reason; the other 38 exports compile and execute
equal to wasmtime.

Verified: fmt, clippy -D warnings clean, synth-synthesis 760 + suites 0
failed, exact-emulation-floor re-derived 346751 on the rebased tree,
status_evidence and claim_check green.

Refs #1189, #1221, #1222, #1226

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe added a commit that referenced this pull request Sep 9, 2026
…t to the REAL corpus; the 12 first-full-corpus hits were the walk, fixed in the walk

The corpus sweep's first run WITH the suite submodule and the corrected
ROOT (previous lane: suite-only, 4628 functions) read 8317 functions /
8776 homes and `hits: 12 (unexplained: 12)` plus 16 pinned #1226 hits that
did not occur — RESULT: FAIL (3). Classified one by one, nothing silenced:

SHAPE A (8) — AUDIT FALSE POSITIVE, walk fixed. `Pop { regs: [R4..R8, PC] }`
at a mid-function `Return` (cabi_arena_{bind,realloc}.wat func_0, m4/m4f
self) and at a function-level `BrIf(0)` (home_alias_class_1189_promo.wat
p_brif, 4 legs), "writes R4 = home of local N, read again at op M". The
inline epilogue restores a promoted local's r4 and RETURNS in the same
instruction, so op M is unreachable from it. `write_is_terminal` scanned
only PAST the writer (next instruction = another op's, or the br_if's own
skip label) and never asked whether the writer IS the terminator. It does
now; `Pop` has no conditional form in `ArmOp` and both encoders emit it
unconditionally. The existing terminal test planted the home at R0, never
at the register the pop restores — that is why the unit test did not see
it; the new test plants R4.

SHAPE B (4) — LEGITIMATE-BUT-SAFE, proven on the stream instead of pinned.
`F32Load { sd: S0, addr: [SP, #24|#28] }` at op `Call(11)` (f32_ops_719.wat
xhome/xcall2, m4f-reloc/-self): `vstr s0, [sp, #0x18] … bl … vldr s0, [sp,
#0x18]` — the caller-save RESTORE of the f32 home from the slot the same op
saved it to. The audit had not stated the AAPCS VFP caller-saved clobber
(s0–s15) on calls, so the `bl` that makes the restore necessary was
INVISIBLE and its restore surfaced as the write; a MISSING restore was
invisible too. `vfp_defs` now lists s0–s15 on Bl/Blx/Call/CallIndirect
(re-swept with it stated: 0 new hits — every VFP home live across a call
on this corpus is saved and restored), and `write_is_bracketed_by_save_
restore` discharges the round trip only when save and restore name the
identical register and static slot, the save precedes every other write of
the home in the op, and nothing between them touches the slot, its base or
control flow. Unit-tested: the exempt shape (incl. an argument marshalled
INTO the home between save and restore) and 9 broken variants — no
restore, other slot, overlapping store, disjoint store (fine), SP move,
stale save, split op, label — as still-flagged. Executed: the CI-wired
f32_ops_719_differential.py runs xhome/xcall2 on m4f under unicorn,
238/238 bit-exact vs wasmtime.

Each exemption's negative-control build reproduces exactly its own shape
and nothing else: pop check off -> the 8 pop hits, 0 other; round trip off
(clobber stated) -> the 4 VFP functions, now reported at the `Bl`, 0 other.
The fixed walk sweeps the IDENTICAL population (1045 pairs / 8317 / 8776 /
261440 attributed) to 0 hits.

SHAPE C — the 16 #1226 pins stopped occurring because `declared_wide_params`
(c14f53a) reads the SAME stale width table #1226 describes, so on
`checkRange` the pair-write no longer fires and nothing lands on `$to`'s
R1. Verified on the bytes: the gate removed the HIT, not the MISCOMPILE —
`checkRange` still compares `$to` at R1:R2 (`cmp r0, r1; it eq; cmpeq r1,
r2`; AAPCS passes it in R2:R3), `local.set $from` is back to the
single-half `mov r0, r5` (the `adc r6` hi half dropped), and the `i64.const
-1` return sets R0 only. #1226 stays OPEN (bytes on the issue); the pins
are removed here because no sweep line can see the defect any more, and
the script says so.

Pins re-derived on the rebased tree with the submodule present (never
carried textually): in-script FLOORS 1045/8317/8776/261440, the `ci-checks:
stdout` header >= 8317, ci.yml greps `functions audited: 8317`, `homes
watched: 8776`, `hits: 0 (known-open: 0 [none], unexplained: 0)`; exact
emulation floor re-derived by oracle_wiring_check.py: 346751, unchanged;
selector ratchets unchanged (home_alias.rs is outside the ceiling;
claim_check --metric 63/63, status.json no drift). Artifact verified-by,
docs/analysis table (the VFP call-clobber row was WRONG: "no home exists
to alias" is true of core registers only), CHANGELOG and the waiver prose
now state what was measured.

Verified: cargo fmt --check, clippy --workspace --all-targets -D warnings,
synth-synthesis 766 + suites 0 failed, CI-form sweep via oracle_run with
the four exact greps ALL MATCH, home_alias_class_1189_differential.py 999
matched / 0 diverged / 1629 emulations PASS, f32_ops_719 238/238,
status_evidence_check green, duplicate-key-strict YAML parse of ci.yml,
the artifact and claims.yaml.

Refs #1189, #1222, #1226, #1227

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
@avrabe

avrabe commented Sep 9, 2026

Copy link
Copy Markdown
Contributor Author

Finishing lane — the third red, classified: all 12 hits were the WALK, fixed in the walk; #1226's 16 went silent, not fixed (21574841)

Rebased onto 761c6922 (main incl. RQ-65-DECLINE #1228). Submodule present
(257 .wast). Reproduced the coordinator's red first: hits: 12 (unexplained: 12), 16 pinned #1226 hits missing, RESULT: FAIL (3).

Classification of the 12

shape hits verdict evidence
A: Pop {R4..R8, PC} at Return (cabi_arena_{bind,realloc} func_0, m4/m4f self) and at function-level BrIf(0) (promo p_brif, 4 legs) 8 audit FALSE POSITIVE — walk fixed the pop restores a promoted local's r4 and RETURNS in the same instruction (mov r0,r4; add sp; pop {r4-r8,pc} then the next op / the br_if's skip:); write_is_terminal scanned only PAST the writer, never asked whether the writer IS the terminator. The previous lane's "pinned safe" exemption was applied — to the mov before the pop, whose scan sees the pop ahead — while the pop's own write fell through. Pop has no conditional form in ArmOp; both encoders emit it unconditionally. The old unit test planted the home at R0, never at the register the pop restores; the new one plants R4
B: F32Load S0 ← [SP,#24/#28] at Call(11) (f32_ops_719 xhome/xcall2, m4f-reloc/-self) 4 LEGITIMATE-BUT-SAFE — proven on the stream, not pinned vstr s0,[sp,#0x18] … bl … vldr s0,[sp,#0x18]: the caller-save restore of the home from the slot the same op saved it to. Root cause of the report: vfp_defs did not state the AAPCS VFP caller-saved clobber (s0–s15) on calls, so the bl was invisible, its restore looked like the write, and a MISSING restore would have been invisible too. Calls now carry s0–s15; write_is_bracketed_by_save_restore discharges the round trip only for identical register + static slot, save before any other write of the home in the op, nothing between touching the slot/base/control flow. 9 broken variants unit-tested as still-flagged. Re-swept with the clobber stated: 0 new hits — every VFP home live across a call on this corpus is saved and restored. Executed: the CI-wired f32_ops_719_differential.py runs exactly this shape on m4f under unicorn, 238/238 bit-exact (the doc's "VFP homes audited but not executed" was true of THIS artifact's oracle only)

Negative controls, each exemption off in turn on the four affected modules:
pop check off → 8 pop hits, 0 other; round trip off (clobber stated) →
the 4 VFP functions, now reported at the Bl, 0 other. Both on → 0. The
fixed walk sweeps the IDENTICAL population as the red run (1045 pairs / 8317 /
8776 / 261440 attributed) to 0 hits.

#1226 verdict: the gate removed the HIT, not the MISCOMPILE — stays open.
declared_wide_params reads self.params_i64, the same stale width table
#1226 describes, so on checkRange the pair-write no longer fires and
nothing writes R1. Bytes at the PR head (m4-reloc): cmp r0,r1; it eq; cmpeq r1,r2 ($to still at R1:R2, AAPCS says R2:R3); local.set $from is
back to adds r5,r0,r3; adc r6,r1,r4; mov r0,r5 (hi half dropped — the
#1222 single-half shape on this stale-width function); i64.const -1
return sets R0 only. Pins removed from the script (the rule: the PR that
moved the hit moves the pin), table left empty with the reason; the issue
carries the bytes and the note that no sweep line can see it any more.

Re-pinned to the real corpus (submodule present): in-script FLOORS
1045/8317/8776/261440, ci-checks: stdout … >= 8317, ci.yml greps
functions audited: 8317 / homes watched: 8776 / hits: 0 (known-open: 0 [none], unexplained: 0); CI-form run through oracle_run.py with the four
exact greps: ALL MATCH, RESULT: PASS. Exact emulation floor re-derived on
the rebased tree: 346751, unchanged (ci.yml + claims.yaml untouched).
Selector ratchets untouched (home_alias.rs is outside the ceiling;
claim_check --metric 63/63, --emit-status no drift). Artifact
verified-by, the docs table (its VFP call-clobber row was wrong — "no
home exists to alias" holds for core registers only), CHANGELOG and the
waiver prose now say what was measured.

Green on the tree: fmt, clippy -D warnings, synth-synthesis 766 + suites,
home_alias_class_1189_differential.py 999/0/1629 PASS,
status_evidence_check, duplicate-key-strict YAML. No new issue filed —
nothing in the 12 was a miscompile. Not merged (coordinator gates).

Refs #1189, #1222, #1226

@avrabe

avrabe commented Sep 9, 2026

Copy link
Copy Markdown
Contributor Author

Coordinator verification — hits: 0 is a meaningful claim, proven by mutation

I flagged a concern on this branch: the job asserts hits: 0 on a walk that had just been relaxed to
clear 12 false positives, and the job block itself (71 lines) contains no potency / self-test /
red-first mechanism. The functions audited >= 8317 stdout floor proves the sweep RAN; it does not
prove the DETECTOR FIRES. Those are different properties.

The concern is answered, and the answer is in the unit tests rather than the job. The exemptions
are paired positive/negative by construction — terminal_return_write_is_exempt_conditional_is_not,
call_save_restore_round_trip_of_a_vfp_home_is_exempt_every_break_is_not,
own_set_is_exempt_other_locals_set_is_not — with 26 assertions that a hit is produced. Those run
in cargo test on every CI run, so the potency is wired, not measured once at authoring.

Verified by mutation rather than by reading the names. Making each exemption unconditional:

mutation result
write_is_terminal always exempt FAILED — 8 of 14
write_is_bracketed_by_save_restore always exempt FAILED — 8 of 14
restored ok, 14/14; file byte-identical

A walk that stops discriminating reddens. That is what makes hits: 0 a claim rather than a silence.

On the two findings behind the 12, both worth recording because neither is "the audit was noisy":

  • Shape A: the previous lane's terminal-return pin WAS applied — to the mov before the pop — but
    write_is_terminal scanned only from k+1, so when the writer is the pop it fell through. The
    old unit test planted the home at R0, never at the register the pop restores, which is exactly why
    it never caught this. The new test plants R4.
  • Shape B is the more interesting one: vfp_defs stated no VFP clobber on calls, so a bl that
    really does clobber s0–s15 was invisible to the walk. The restore looked like the write — and a
    missing restore would have been invisible too. That is a blind spot in the detector, not noise,
    and closing it is worth more than the four hits it explained.

#1226 verdict, which is the honest one: declared_wide_params removed the HIT, not the
MISCOMPILE. It reads self.params_i64, the same stale width table #1226 describes, so on checkRange
the pair-write no longer fires and nothing lands on R1 — the wrong bytes are still emitted, just
differently wrong. #1226 stays open, the 16 pins are removed with that reason recorded, and no sweep
line can see it any more. That is a coverage loss stated as one rather than left as a parenthetical.

Refs #1189, #1226

avrabe added a commit that referenced this pull request Sep 9, 2026
…nt probe, 192 exact) and pin #1226 red-first on its REAL mechanism: the .wast path threads no width tables

Coordinator review of #1227: the sweep's `hits: 0` proved the sweep RAN
(work floors), not that the DETECTOR FIRES — and after the walk was
relaxed to clear 12 false positives that was the property under
suspicion. Two additions, and one correction the second one forced.

POTENCY, wired. `SYNTH_HOME_ALIAS_AUDIT=verbose,plant` makes
`home_alias::plant_probe` plant ONE synthetic write of a watched home at
op 0 of every function that has a home still read later (`mov <home>,
r12` / `F32Const` into the S-slot, on a COPY of the stream; shipped bytes
untouched). The corpus script's self-test phase runs first and requires,
per (fixture, leg), EXACTLY the pinned number of declines carrying the
needle at `op 0` — i32 params r0-r3 58/7/58/7, promoted locals r4-r8
11/9/11/9, VFP homes 0/0/11/11 (soft-float m4 has none) — and 0 declines
without the plant: 192 planted writes reported, through the same decline
/ needle / parse path the sweep relies on. ci.yml greps `POTENCY: PASS
(192 …)` exactly. (I first wrote 172 by hand; the script's derived total
is 192 — the pin is the derived number.) The selector's audit hook
collapsed to one call into `home_alias::selector_hook` (63 -> 12 lines;
`selector_lines_code` 19945 -> 19896, a FALL, waiver bound to the value
as the engine requires; `selector_lines_total` 30943 -> 30894).

#1226, STATED PLAINLY — and corrected. The walk is correct and #1226 was
never a home-register WRITE: it is a mis-HOMING, which this audit cannot
see because it trusts the selector's home table by construction; the 16
hits it carried were the #1222 pair-write (fired by body inference)
landing in the neighbour's wrongly assigned R1, removed by the
declared-width gate changing the EMISSION, not the walk — no coverage of
home writes was lost. Trying to pin it exposed that the issue's mechanism
is wrong: the two-module repro MERGED and the same functions STANDALONE
as `.wast` are equally wrong; the discriminator is the extension. The
synth-cli `.wast` driver path returns `Vec::new()` for EVERY declared-
width table (func/type ret_i64, params_i64/_f32/_f64, the f32/f64 return
masks — each annotated "WAST fixture suite is i32-only"), so on ANY
`.wast`, single-module too, an i64/f32/f64 param or result whose width
body inference cannot recover is homed as i32. Measured: the same module
text as `.wat` gives `second3` homes=4 and `mov r0, r2; mov r1, r3`; as a
`.wast` homes=2 and `mov r0, r1`; `fac-opt` is rescued by inference.
Static upper bound: 1393 exported spec-suite functions in 74 files carry
a wide param or result. Pinned RED-FIRST in the same self-test: one
fixture (`home_alias_width_1226.wast`), its last module derived at run
time as a single `.wast` and as the identical `.wat`; `homes=` must be
`wast < wat` on every leg — (7, 6, 8) relocatable, (4, 4, 8) self-
contained; ci.yml greps `WIDTH-1226: known-open (... on 4 legs)`; a fix
makes them equal and must flip the pin.

CONSEQUENCE for #1222, recorded in CHANGELOG / artifact / docs: the
pair-write is gated on the DECLARED width, so on `.wast` input it never
fires — the spec-suite functions the #1222 entry named as fixed (fac-opt,
loop `while`, type-param-i64, the 64-bit bulk-memory `checkRange`s) are
NOT fixed; they are wrong for #1226's reason until #1226 is fixed. #1222
holds for `.wat`/`.wasm` input (its own fixtures, executed).

Verified: fmt --check, clippy --workspace --all-targets -D warnings,
synth-synthesis 766 + suites 0 failed (16 home_alias unit tests incl.
the probe and S_REGS inverse), CI-form sweep via oracle_run with all SIX
exact greps matching (POTENCY 192, WIDTH-1226 known-open, 8317 / 8776 /
hits 0 / RESULT: PASS), exact emulation floor re-derived 346751
(unchanged: the self-test is stdout-declared), claim_check 63/63 with
status.json regenerated, status_evidence_check green, duplicate-key-
strict YAML on ci.yml / artifact / claims.

Refs #1189, #1222, #1226, #1227

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
@avrabe

avrabe commented Sep 9, 2026

Copy link
Copy Markdown
Contributor Author

Coordinator review addressed (6f25b977): potency wired and pinned exactly; #1226 stated plainly — and its mechanism corrected while pinning it

1. Potency, wired. SYNTH_HOME_ALIAS_AUDIT=verbose,plant makes
home_alias::plant_probe plant ONE synthetic write of a watched home at op 0
of every function that has a home still read later (mov <home>, r12 /
F32Const into the S-slot, on a COPY of the stream — shipped bytes untouched;
unit-tested for the exempt and the no-plant cases). The corpus script's
self-test phase runs BEFORE the sweep and requires, per (fixture, leg),
EXACTLY the pinned number of declines carrying the needle at op 0, through
the same decline / needle / parse path the sweep relies on — and 0 declines
without the plant:

fixture (home kind) m4-reloc m4-self m4f-reloc m4f-self
home_alias_class_1189_i32.wat (i32 params r0–r3) 58 7 58 7
home_alias_class_1189_promo.wat (promoted r4–r8) 11 9 11 9
f32_ops_719.wat (VFP homes; soft-float m4 has none) 0 0 11 11

192 planted writes reported, 0 without the plant. ci.yml greps
^POTENCY: PASS (192 planted writes reported, 0 without the plant, over 3 fixtures x 4 legs)$ exactly; fewer → the detector went quiet, more → the walk
over-reports again. (My first draft said 172 — hand-added; the pin is the
script's derived number.) The selector's audit hook collapsed to one call into
home_alias::selector_hook (63 → 12 lines): selector_lines_code 19945 →
19896, a FALL, waiver bound to the value as the engine requires;
selector_lines_total 30943 → 30894.

2. #1226 in one sentence: it was never a home-register write this audit
could see — it is a mis-homing the audit cannot see by construction (it trusts
the selector's home table), the 16 hits were a symptom the declared-width gate
removed by changing the emission, no coverage of home writes was lost, and it
is now pinned red-first on the audit's homes= count (same module text as
.wast vs .wat, 6 < 8 relocatable / 4 < 8 self-contained, WIDTH-1226: known-open grepped in ci.yml) until a fix makes them equal and flips the pin.

The correction that fell out of pinning it. The issue's mechanism is
wrong. Merged vs standalone .wast are EQUALLY wrong; the discriminator is
the extension: second3 ((param i64 i64 i32) (local.get 1)) as .wat
mov r0, r2; mov r1, r3, homes=4; as ANY .wast, single-module included →
mov r0, r1, homes=2. Cause, in synth-cli/src/main.rs: the .wast decode
arm returns Vec::new() for every declared-width table (params/returns
i64/f32/f64), each annotated "WAST fixture suite is i32-only"; the compile
loop's .get(index) && !p.is_empty() never fires, "assume i32". Body
inference rescues some (fac-opt sets its param → a pair), which is why it
looked module-position-dependent. Static upper bound: 1393 exported
spec-suite functions in 74 files. #1226 retitled + commented with the bytes.

Consequence for #1222, recorded in CHANGELOG / artifact / docs: the
pair-write is gated on the DECLARED width, so on .wast input it never fires
— the spec-suite functions the #1222 entry named as fixed (fac-opt, loop
while, type-param-i64, the 64-bit checkRanges) are NOT fixed; they are
wrong for #1226's reason until #1226 is. #1222 holds for .wat/.wasm input
(its own fixtures, executed).

Artifact verified-by now carries the real numbers (1045 / 8317 / 8776 /
0), the potency evidence and counts, the #1226 statement + pin, and the #1222
caveat. Emulation floor re-derived: 346751, unchanged (the self-test is
stdout-declared). Green: fmt, clippy -D warnings, synth-synthesis 766 +
suites, CI-form sweep with all SIX exact greps, claim_check 63/63 +
status.json regenerated, status_evidence_check, strict YAML. Not merged.

Refs #1189, #1222, #1226

@avrabe

avrabe commented Sep 9, 2026

Copy link
Copy Markdown
Contributor Author

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

avrabe commented Sep 9, 2026

Copy link
Copy Markdown
Contributor Author

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, r1mis-homed
#1232 e92d4010 e1a00002 e1a01003 e8bd8010 mov r0, r2; mov r1, r3correct 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:

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

avrabe and others added 6 commits September 9, 2026 08:58
…me-register consumer on four legs; fix aarch64 rotl (#1221) and i64-param local.set (#1222) red-first; pin #1223 open

THE QUESTION. `local.get` of a register-homed local pushes THE HOME
REGISTER uncopied onto the operand stack; #677, #989 and #1189 were three
consumers that wrote it, each found as a silent wrong answer and fixed at
its own site. How many others exist, across arm-reloc, arm-self, RV32 and
AArch64? Answered mechanically, not by re-reading arms.

STATIC AUDIT (ARM direct selector). `synth_synthesis::home_alias`: an
exhaustive, wildcard-free register-writes table for all 222 ArmOp variants
(`gp_defs`/`vfp_defs`, #946-style source-scan pin) + a loop-back-edge-
extended liveness walk independent of the selector's own `param_last_read`,
hooked at the tail of `select_with_stack` under SYNTH_HOME_ALIAS_AUDIT. A
write to a live local's home that is not the local's own set/tee, and not
proven straight-line into an inline epilogue ON THE STREAM, is a loud
decline naming op, instruction, register and local. Byte-invisible
otherwise. Swept over the pinned spec suite + local corpus on {reloc,
self} x {cortex-m4, cortex-m4f}: 4628 functions, 2372 homes, 227150
attributed instructions, 0 unexplained hits; 16 hits pinned KNOWN-OPEN
against #1226 (home_alias_audit_corpus_1189.py, CI job
home-alias-audit-1189). Potency against the real history: built at the
pre-#1190 commit it flags exactly the 10 functions #1190 recorded wrong
and none of its 7 clean ones.

EXECUTION ORACLE (four legs). home_alias_class_1189_differential.py + 3
generated modules: 117 consumer-family functions re-reading their homes
after every op, expected values from wasmtime, declines pinned EXACTLY per
(module, leg), main's own objects kept as a permanent red half (10 pinned
wrong vectors). Red-first on main af81978: 990 matched / 9 diverged:
  #1221 aarch64 i32/i64.rotl negates the count IN PLACE — the #776 fix's
        "now-dead register" is a param home in a leaf function; every
        result exactly rotl + a - b (7 vectors).
  #1222 direct selector local.set/tee of a register-homed i64 PARAM writes
        only the lo half, at index_to_reg(i) not the AAPCS pair, with the
        #989 snapshot reserving only val_lo; every leaf function assigning
        an i64 param (spec suite: fac-opt, loop `while`, type-param-i64,
        the 64-bit bulk-memory checkRanges) was silently wrong.
  #1223 optimized path folds (x - x) + x to 0 — an IR defect, NOT this
        class; filed, pinned KNOWN_OPEN (the recorded wrong value must
        persist until the fix flips the pin).
  #1226 surfaced BY the #1222 fix in the audit sweep: the multi-module
        .wast merge hands a later module's function the representative
        module's param-width table (#1168 re-threads arg counts, not
        width masks), so an i64 param is homed as i32 and its pair
        overlaps the next param. A CLI-merge defect, NOT this class;
        filed, 4 spec-suite functions x 4 legs pinned exactly until fixed.
Green on the fixes: 999 matched / 0 diverged, 10/10 pinned wrong vectors
still reproduce from main's bytes, 1629 emulations. CI job
home-alias-class-1189-oracle; emulation floor 325121 -> 326750 (re-derived
by oracle_wiring_check.py; ci.yml and claims.yaml in lockstep).

FIXES, one site each. aarch64 rotl: a param count is negated into a
scratch chosen with n, k and dst held live; a temp count keeps the #776
bytes. ARM direct: `write_i64_param_home` moves both halves at the
`local_to_reg` home, ordered for partial overlap, both halves of val
reserved for the alias snapshot. Byte-identity pre vs post over 1419
compiles / 10725 functions (arm-reloc, arm-self, aarch64): 58 functions
changed, every one an aarch64 rotl function or an ARM i64-param set/tee;
0 newly declined / accepted, no skip-set moved.

STRUCTURAL PINS for the clean legs, as tests: RV32 params COPY on
local.get (the accident of implementation the artifact names) and a
promoted s8 is written only by its own set + the epilogue; AArch64 TEMPS
disjoint from x0..x7, 21 families never write a param home; the optimized
path's local vregs are never freed (18 families walked with gp_defs).

LEDGER. selector_lines_code 19740 -> 19917 by waiver (the class had no
handling to delete); tracked totals 30565 -> 30857, 91 -> 93 (two
`_ => None` in the new test). RQ-65-ALIASCLASS implemented; enumeration in
docs/analysis/HOME_REGISTER_ALIAS_CLASS_1189.md; CHANGELOG [Unreleased].

Refs #1189, #1221, #1222, #1223, #1226

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…the DECLARED width; the fuzz harness was right and the fix over-applied

Salvaged and completed by the coordinator after the lane hit a session rate
limit mid-diagnosis. Three CI reds on #1227, all found only after the rebase.

RED 3 — the substantive one, and the fuzz target was CORRECT.

`i64_lowering_doesnt_clobber_params` asserted that nothing may write R1 while
`LocalGet(1)` still reads it, and caught:

  Mov { rd: R0, op2: Reg(R4) }, Mov { rd: R1, op2: Reg(R5) }

The convenient reading was that the harness encoded the pre-#1222 register
model and should move with the fix. It did not. `i64_locals` carries
body-INFERRED widths (`infer_i64_locals`), not only declared ones — so a param
the signature calls i32, or whose width nobody declared (a direct
`select_with_stack` caller, #1226's stale multi-module width table, invalid
wasm), is homed NARROW by `aapcs_param_layout` and its "hi half" IS the next
param's home. The #1222 pair-write fired there and genuinely clobbered local 1.

So the fix was over-applied, not the harness stale. `declared_wide_params`
now gates the pair arm on the declared width AND the layout having homed it
as a pair; anything else keeps the single-move arm — yesterday's bytes.

Regression test covers both configurations, which is the discrimination that
was missing: undeclared widths write R0 only with nothing touching R1 before
`local.get 1`; declared `(i64 i32)` writes the pair R0:R1 with local 1 in R2.

RED 1 — the audit oracle ran VACUOUSLY in CI. `ROOT` was
`Path(__file__).parent.parent`, which from `scripts/repro/` resolves to
`scripts/`, so it looked for the suite at `scripts/tests/spec-testsuite`,
found nothing and exited 1 having audited 0 functions. Now
`.parent.parent.parent`, matching the working sibling
`selector_parity_197_differential.py` in the same directory. Its FATAL message
also stops guessing ("submodule not checked out?" — it was) and prints the
path it actually looked at plus whether that path exists.

RED 2 — `arm_corpus_sweep_973.py` auto-sweeps every `scripts/repro/*.wat`, so
the new i64 fixture joined the corpus and legitimately declines its 10 `c_*`
exports (i64 compare feeding `i64.extend_i32_u`, #952). Registered in
EXPECTED_DECLINES with that reason; the other 38 exports compile and execute
equal to wasmtime.

Verified: fmt, clippy -D warnings clean, synth-synthesis 760 + suites 0
failed, exact-emulation-floor re-derived 346751 on the rebased tree,
status_evidence and claim_check green.

Refs #1189, #1221, #1222, #1226

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…egenerate status.json for the declared-width guard

The previous commit changed select_with_stack.rs without moving the pins, and
I pushed it because my `&&` chain guarded the `echo`, not the `git push` —
the exact "captured the exit code, didn't gate" trap the standing rules name.
The gate said FAIL and the push ran anyway as a separate statement. This
commit is chained through to the push so it cannot repeat.

Two real failures behind that FAIL, both re-derived, never hand-computed:

  selector_lines_code   19917 -> 19945  ceiling, must FALL -> waived
  selector_lines_total  30857 -> 30943  tracked, no direction -> value only
  artifacts/status.json                 stale -> regenerated with --emit-status

The waiver is bound to 19945, so a further regression needs its own waiver.
Its reason records that this +28 is a CORRECTION to the same artifact's own
+177, not new capability: the #1222 pair-write was gated on `i64_locals`,
which carries body-inferred widths, so it fired on params homed narrow and
clobbered the next param's home. Narrowing the arm cannot be done by
deleting — the correct behaviour needs the declared-width test the original
arm lacked.

Refs #1189, #1222

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…t to the REAL corpus; the 12 first-full-corpus hits were the walk, fixed in the walk

The corpus sweep's first run WITH the suite submodule and the corrected
ROOT (previous lane: suite-only, 4628 functions) read 8317 functions /
8776 homes and `hits: 12 (unexplained: 12)` plus 16 pinned #1226 hits that
did not occur — RESULT: FAIL (3). Classified one by one, nothing silenced:

SHAPE A (8) — AUDIT FALSE POSITIVE, walk fixed. `Pop { regs: [R4..R8, PC] }`
at a mid-function `Return` (cabi_arena_{bind,realloc}.wat func_0, m4/m4f
self) and at a function-level `BrIf(0)` (home_alias_class_1189_promo.wat
p_brif, 4 legs), "writes R4 = home of local N, read again at op M". The
inline epilogue restores a promoted local's r4 and RETURNS in the same
instruction, so op M is unreachable from it. `write_is_terminal` scanned
only PAST the writer (next instruction = another op's, or the br_if's own
skip label) and never asked whether the writer IS the terminator. It does
now; `Pop` has no conditional form in `ArmOp` and both encoders emit it
unconditionally. The existing terminal test planted the home at R0, never
at the register the pop restores — that is why the unit test did not see
it; the new test plants R4.

SHAPE B (4) — LEGITIMATE-BUT-SAFE, proven on the stream instead of pinned.
`F32Load { sd: S0, addr: [SP, #24|#28] }` at op `Call(11)` (f32_ops_719.wat
xhome/xcall2, m4f-reloc/-self): `vstr s0, [sp, #0x18] … bl … vldr s0, [sp,
#0x18]` — the caller-save RESTORE of the f32 home from the slot the same op
saved it to. The audit had not stated the AAPCS VFP caller-saved clobber
(s0–s15) on calls, so the `bl` that makes the restore necessary was
INVISIBLE and its restore surfaced as the write; a MISSING restore was
invisible too. `vfp_defs` now lists s0–s15 on Bl/Blx/Call/CallIndirect
(re-swept with it stated: 0 new hits — every VFP home live across a call
on this corpus is saved and restored), and `write_is_bracketed_by_save_
restore` discharges the round trip only when save and restore name the
identical register and static slot, the save precedes every other write of
the home in the op, and nothing between them touches the slot, its base or
control flow. Unit-tested: the exempt shape (incl. an argument marshalled
INTO the home between save and restore) and 9 broken variants — no
restore, other slot, overlapping store, disjoint store (fine), SP move,
stale save, split op, label — as still-flagged. Executed: the CI-wired
f32_ops_719_differential.py runs xhome/xcall2 on m4f under unicorn,
238/238 bit-exact vs wasmtime.

Each exemption's negative-control build reproduces exactly its own shape
and nothing else: pop check off -> the 8 pop hits, 0 other; round trip off
(clobber stated) -> the 4 VFP functions, now reported at the `Bl`, 0 other.
The fixed walk sweeps the IDENTICAL population (1045 pairs / 8317 / 8776 /
261440 attributed) to 0 hits.

SHAPE C — the 16 #1226 pins stopped occurring because `declared_wide_params`
(c14f53a) reads the SAME stale width table #1226 describes, so on
`checkRange` the pair-write no longer fires and nothing lands on `$to`'s
R1. Verified on the bytes: the gate removed the HIT, not the MISCOMPILE —
`checkRange` still compares `$to` at R1:R2 (`cmp r0, r1; it eq; cmpeq r1,
r2`; AAPCS passes it in R2:R3), `local.set $from` is back to the
single-half `mov r0, r5` (the `adc r6` hi half dropped), and the `i64.const
-1` return sets R0 only. #1226 stays OPEN (bytes on the issue); the pins
are removed here because no sweep line can see the defect any more, and
the script says so.

Pins re-derived on the rebased tree with the submodule present (never
carried textually): in-script FLOORS 1045/8317/8776/261440, the `ci-checks:
stdout` header >= 8317, ci.yml greps `functions audited: 8317`, `homes
watched: 8776`, `hits: 0 (known-open: 0 [none], unexplained: 0)`; exact
emulation floor re-derived by oracle_wiring_check.py: 346751, unchanged;
selector ratchets unchanged (home_alias.rs is outside the ceiling;
claim_check --metric 63/63, status.json no drift). Artifact verified-by,
docs/analysis table (the VFP call-clobber row was WRONG: "no home exists
to alias" is true of core registers only), CHANGELOG and the waiver prose
now state what was measured.

Verified: cargo fmt --check, clippy --workspace --all-targets -D warnings,
synth-synthesis 766 + suites 0 failed, CI-form sweep via oracle_run with
the four exact greps ALL MATCH, home_alias_class_1189_differential.py 999
matched / 0 diverged / 1629 emulations PASS, f32_ops_719 238/238,
status_evidence_check green, duplicate-key-strict YAML parse of ci.yml,
the artifact and claims.yaml.

Refs #1189, #1222, #1226, #1227

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…nt probe, 192 exact) and pin #1226 red-first on its REAL mechanism: the .wast path threads no width tables

Coordinator review of #1227: the sweep's `hits: 0` proved the sweep RAN
(work floors), not that the DETECTOR FIRES — and after the walk was
relaxed to clear 12 false positives that was the property under
suspicion. Two additions, and one correction the second one forced.

POTENCY, wired. `SYNTH_HOME_ALIAS_AUDIT=verbose,plant` makes
`home_alias::plant_probe` plant ONE synthetic write of a watched home at
op 0 of every function that has a home still read later (`mov <home>,
r12` / `F32Const` into the S-slot, on a COPY of the stream; shipped bytes
untouched). The corpus script's self-test phase runs first and requires,
per (fixture, leg), EXACTLY the pinned number of declines carrying the
needle at `op 0` — i32 params r0-r3 58/7/58/7, promoted locals r4-r8
11/9/11/9, VFP homes 0/0/11/11 (soft-float m4 has none) — and 0 declines
without the plant: 192 planted writes reported, through the same decline
/ needle / parse path the sweep relies on. ci.yml greps `POTENCY: PASS
(192 …)` exactly. (I first wrote 172 by hand; the script's derived total
is 192 — the pin is the derived number.) The selector's audit hook
collapsed to one call into `home_alias::selector_hook` (63 -> 12 lines;
`selector_lines_code` 19945 -> 19896, a FALL, waiver bound to the value
as the engine requires; `selector_lines_total` 30943 -> 30894).

#1226, STATED PLAINLY — and corrected. The walk is correct and #1226 was
never a home-register WRITE: it is a mis-HOMING, which this audit cannot
see because it trusts the selector's home table by construction; the 16
hits it carried were the #1222 pair-write (fired by body inference)
landing in the neighbour's wrongly assigned R1, removed by the
declared-width gate changing the EMISSION, not the walk — no coverage of
home writes was lost. Trying to pin it exposed that the issue's mechanism
is wrong: the two-module repro MERGED and the same functions STANDALONE
as `.wast` are equally wrong; the discriminator is the extension. The
synth-cli `.wast` driver path returns `Vec::new()` for EVERY declared-
width table (func/type ret_i64, params_i64/_f32/_f64, the f32/f64 return
masks — each annotated "WAST fixture suite is i32-only"), so on ANY
`.wast`, single-module too, an i64/f32/f64 param or result whose width
body inference cannot recover is homed as i32. Measured: the same module
text as `.wat` gives `second3` homes=4 and `mov r0, r2; mov r1, r3`; as a
`.wast` homes=2 and `mov r0, r1`; `fac-opt` is rescued by inference.
Static upper bound: 1393 exported spec-suite functions in 74 files carry
a wide param or result. Pinned RED-FIRST in the same self-test: one
fixture (`home_alias_width_1226.wast`), its last module derived at run
time as a single `.wast` and as the identical `.wat`; `homes=` must be
`wast < wat` on every leg — (7, 6, 8) relocatable, (4, 4, 8) self-
contained; ci.yml greps `WIDTH-1226: known-open (... on 4 legs)`; a fix
makes them equal and must flip the pin.

CONSEQUENCE for #1222, recorded in CHANGELOG / artifact / docs: the
pair-write is gated on the DECLARED width, so on `.wast` input it never
fires — the spec-suite functions the #1222 entry named as fixed (fac-opt,
loop `while`, type-param-i64, the 64-bit bulk-memory `checkRange`s) are
NOT fixed; they are wrong for #1226's reason until #1226 is fixed. #1222
holds for `.wat`/`.wasm` input (its own fixtures, executed).

Verified: fmt --check, clippy --workspace --all-targets -D warnings,
synth-synthesis 766 + suites 0 failed (16 home_alias unit tests incl.
the probe and S_REGS inverse), CI-form sweep via oracle_run with all SIX
exact greps matching (POTENCY 192, WIDTH-1226 known-open, 8317 / 8776 /
hits 0 / RESULT: PASS), exact emulation floor re-derived 346751
(unchanged: the self-test is stdout-declared), claim_check 63/63 with
status.json regenerated, status_evidence_check green, duplicate-key-
strict YAML on ci.yml / artifact / claims.

Refs #1189, #1222, #1226, #1227

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…1232 landed the fix this pin was waiting for

Rebased onto main after RQ-65-MVPCORE (#1232) merged, which is the fix this
pin's own rule anticipated: "a fix makes (b) == (c), this goes red, and the fix
flips the pin (known-open -> closed) in its own PR."

RE-DERIVED on the merged tree with `--print-self-test`, not asserted. Every leg
(merged-wast, single-wast, same-text-wat):

  before   m4-reloc (7, 6, 8)   m4-self (4, 4, 8)   wast < wat, open
  after    all four legs (0, 8, 8)                  wast == wat, merged refused

Two independent routes, both now clean: the single-module `.wast` path threads
declared widths so `wast == wat`, and the multi-module merge REFUSES an
i64-param module so `merged == 0`. The assertion becomes EQUALITY plus that
refusal, which is strictly stronger than the old inequality — a narrower `wast`
OR the merge silently accepting again now goes red.

POTENCY is untouched: 192 planted writes, 0 without the plant, across 3 fixtures
x 4 legs. Self-test RESULT: PASS on the rebased tree.

Artifact prose corrected where it had become FALSE rather than merely dated:
"#1226 stays OPEN" and "not fixed here" were true when written and are not now.
The spec-suite functions the artifact said were "NOT fixed by #1222 and stay so
until #1226 is fixed" ARE now correct, because #1226 is fixed. What remains of
#1226 is a REACH note, not a correctness one: the merge refuses i64-param
modules it previously accepted and mis-compiled — decline-honesty with the
acceptance cost stated.

Emulation floor re-derived on the rebased tree: 346751, unchanged.

Refs #1189, #1226, #1232

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
@avrabe
avrabe force-pushed the fix/aliasclass-1189 branch from 6f25b97 to 64ea7fe Compare September 9, 2026 07:02
…floors after #1232; the population fell because modules are now REFUSED

CI on the rebased tree reported the pin flip working — `WIDTH-1226: closed`,
`POTENCY: PASS (192 planted writes, 0 without the plant)`, `hits: 0` — and then
failed on the population floors, correctly:

  VACUOUS — declared floor stdout >= 8317, measured 7191

That is the floor doing its job. The cause is not scan rot: RQ-65-MVPCORE
(#1232) merged first and makes the multi-module `.wast` merge REFUSE modules it
would mis-handle (i64 params, data segments, accessed globals) instead of
silently mis-compiling them. A refused module audits no functions, so this
oracle's corpus shrank with them:

  modules compiled   1045 -> 940     (-105 refused)
  functions audited  8317 -> 7191    (-13.5 %)
  homes watched      8776 -> 8100
  attributed instrs  261440 -> 219807

Re-derived from CI's own run on the merged tree, not computed. The floors move
DOWN exactly once, here, with that reason written beside them in the script, the
artifact and ci.yml; a further fall without a reason is scan rot and stays red.

This is worth stating plainly rather than quietly re-pinning: it is the
ACCEPTANCE COST of decline-honesty, measured. #1232 traded reach for
correctness, and one place the bill lands is that a correctness oracle now
watches 13.5 % fewer functions.

Emulation floor unaffected (this oracle declares `stdout`, not `emulations`) and
re-derived at 346751 on the rebased tree.

Refs #1189, #1226, #1232

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
@avrabe
avrabe merged commit d2e26f4 into main Sep 9, 2026
70 checks passed
@avrabe
avrabe deleted the fix/aliasclass-1189 branch September 9, 2026 07:55
avrabe added a commit that referenced this pull request Sep 9, 2026
… introduced instead of carrying it

Rebased onto main after RQ-65-ALIASCLASS (#1227) and RQ-65-MVPCORE (#1232).
ci.yml conflicted because both PRs inserted a job at the same point; resolved by
taking main's file whole and re-inserting the mutation job after the
home-alias-audit job, then verifying BOTH parse and are present (64 jobs).
CHANGELOG kept one `[Unreleased]` header with both bodies.

MEASURED on the rebased tree, not assumed. #1232 grew
crates/synth-cli/src/main.rs 11143 -> 11405 and mutation sites are anchored by
file:line:col:

  sites enumerated                     1542
  ci_subset entries still resolving    7 of 7   (3 controls + 4 mutants)
  R5-startup mutants still resolving   0 of 7

THE LIVE GATE IS INTACT, and for a structural reason worth recording: the three
controls come from `control_sites()` rather than a line anchor, and the four
subset mutants live in optimizer_bridge.rs / liveness.rs / arm_backend.rs, which
#1232 did not touch. `mutation-survey-discrimination` still replays real
mutations and still fails if a recorded killer stops killing.

WHAT IS STALE, said in the report rather than fixed silently: all seven
R5-startup mutants point at moved code. They are 7 of the 21 byte-changing
mutants the rate is computed over (6 KILLED, 1 UNTESTED) — and that one UNTESTED
is one of the FOUR published survivors. So the 19 % stands as a measurement of
the tree it names, a third of its denominator is not replayable on main, and
re-anchoring R5 is follow-up work rather than a re-run: #1232 restructured that
region, so "the equivalent site" is a judgement, not a line-number shift.

A survey whose denominator quietly stops being checkable is the failure this
release exists to name. Recording it is the point.

Floor re-derived on the rebased tree: 346751, unchanged (this job declares no
emulations). Ratchets unmoved; mutants_untested 4 = pinned.

Refs #1189, #1232, #1227

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe added a commit that referenced this pull request Sep 9, 2026
…hat drifted; the baseline moved, not the site

CI failed the survey's own replay with `changed-set moved: 53 vs ledger 49`. That
is the gate working: all three controls still died to their recorded killers, both
the EQUIVALENT and DEAD entries reproduced, and exactly one entry disagreed.

CAUSE, measured rather than guessed. The site did not move. The BASELINE did:
13 of 609 corpus entries differ on the merged tree after #1232 and #1227, so the
mutation's blast radius moved with them. Byte triage re-derived on the merged tree
gives 53, and CI and a local run agree at 53 independently. Applied to both the
mutant record and the ci_subset entry.

`reanchor` separately relocated all 15 line-shifted sites by their stored `before`
TEXT (0 not found), so last commit's "R5 mutants are not replayable" is obsolete
and the report section is rewritten with the measured figures.

NOT RE-VERIFIED, AND THE REPORT SAYS SO: that mutant's CLASSIFICATION was measured
at `meta.commit` and is not re-established here. The CI replay checks byte triage
for UNTESTED entries, not the oracle suite (that needs --full). The published rate
stays relative to the commit the ledger names.

A LOCAL FULL RE-SURVEY WAS ATTEMPTED AND DISCARDED AS INVALID, recorded because
the near-miss matters: 147 of the 196 L1 steps invoke bare `python`, absent on
this machine, so they exit 127 in 0.1s and the harness scores that as a KILL; and
`fact_spec_div_494_differential.py` is red on the UNMUTATED tree here while green
in CI. That run reported 0 of 29 surviving — dead oracles, not a result. The
harness's own control check refused it: "1 control(s) not killed — the survey
measures nothing; do not publish the rate". A gate that stops its author
publishing a flattering number is the one worth having.

Refs #1189, #1232, #1227

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe added a commit that referenced this pull request Sep 9, 2026
…changing mutants survive a named suite (19 %, upper bound); 3 controls KILLED; survivors enumerated; ledger CI-pinned (#1233)

* feat(mutants): RQ-65-MUTANTS (#1189) — mutation survey: 4 of 21 byte-changing mutants survive a named 5-job suite + workspace tests (19 %, upper bound); 3 red-first controls KILLED; survivors enumerated; ledger CI-pinned

The v0.65 headline number, measured rather than asserted. scripts/mutation_survey.py
flips one codegen decision at a time (REG / COND / DROPMOV / IMM / GUARD / BOUND)
over five anchor-located regions supplied by RQ-65-PARITY, rebuilds, triages by
emitted bytes over 200 corpus modules x 3 ARM configurations, and runs a suite
DERIVED from ci.yml only on byte-changing mutants.

Measured at 580d53f, re-anchored at 761c692, seed 1189: 38 drawn, 6 uncompilable,
32 compiled, 21 byte-changing; 17 KILLED (6 execution, 8 structure, 2 freeze-only,
1 compiler hang), 4 UNTESTED = 19 % survival relative to the NAMED suite
(wast-conformance, repro-sweep-arm-corpus, join-alias-1189, cmp-select,
frame-slot-dce-242 + cargo test --workspace) — an upper bound under the full CI
board. 11 byte-identical: 5 EQUIVALENT, 4 DEAD, 2 UNRESOLVED (declared).
Controls: the #1189 copy disabled, the select operands swapped, the startup R10
seed into R9 — all KILLED (the third only by byte goldens: no execution oracle in
the suite boots the shipped Reset_Handler).

CI pin: the mutation-survey-discrimination job replays the ledger's ci_subset
(3 controls + 4 non-killed) and fails in either direction; claims.yaml gains the
eighth kind: ratchet (mutants_untested, a ceiling over docs/status/mutation_survey.json)
plus count-eq pins on 38 / 21 / 4, the controls and the subset floors. No new
emulation declaration; the exact floor is untouched.

Refs #1189

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

* docs(mutants): RQ-65-MUTANTS (#1189) — record PR #1233 in the artifact's landed field

Refs #1189

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

* docs(mutants): RQ-65-MUTANTS (#1189) — state the ledger staleness #1232 introduced instead of carrying it

Rebased onto main after RQ-65-ALIASCLASS (#1227) and RQ-65-MVPCORE (#1232).
ci.yml conflicted because both PRs inserted a job at the same point; resolved by
taking main's file whole and re-inserting the mutation job after the
home-alias-audit job, then verifying BOTH parse and are present (64 jobs).
CHANGELOG kept one `[Unreleased]` header with both bodies.

MEASURED on the rebased tree, not assumed. #1232 grew
crates/synth-cli/src/main.rs 11143 -> 11405 and mutation sites are anchored by
file:line:col:

  sites enumerated                     1542
  ci_subset entries still resolving    7 of 7   (3 controls + 4 mutants)
  R5-startup mutants still resolving   0 of 7

THE LIVE GATE IS INTACT, and for a structural reason worth recording: the three
controls come from `control_sites()` rather than a line anchor, and the four
subset mutants live in optimizer_bridge.rs / liveness.rs / arm_backend.rs, which
#1232 did not touch. `mutation-survey-discrimination` still replays real
mutations and still fails if a recorded killer stops killing.

WHAT IS STALE, said in the report rather than fixed silently: all seven
R5-startup mutants point at moved code. They are 7 of the 21 byte-changing
mutants the rate is computed over (6 KILLED, 1 UNTESTED) — and that one UNTESTED
is one of the FOUR published survivors. So the 19 % stands as a measurement of
the tree it names, a third of its denominator is not replayable on main, and
re-anchoring R5 is follow-up work rather than a re-run: #1232 restructured that
region, so "the equivalent site" is a judgement, not a line-number shift.

A survey whose denominator quietly stops being checkable is the failure this
release exists to name. Recording it is the point.

Floor re-derived on the rebased tree: 346751, unchanged (this job declares no
emulations). Ratchets unmoved; mutants_untested 4 = pinned.

Refs #1189, #1232, #1227

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

* fix(mutants): RQ-65-MUTANTS (#1189) — re-derive the one changed-set that drifted; the baseline moved, not the site

CI failed the survey's own replay with `changed-set moved: 53 vs ledger 49`. That
is the gate working: all three controls still died to their recorded killers, both
the EQUIVALENT and DEAD entries reproduced, and exactly one entry disagreed.

CAUSE, measured rather than guessed. The site did not move. The BASELINE did:
13 of 609 corpus entries differ on the merged tree after #1232 and #1227, so the
mutation's blast radius moved with them. Byte triage re-derived on the merged tree
gives 53, and CI and a local run agree at 53 independently. Applied to both the
mutant record and the ci_subset entry.

`reanchor` separately relocated all 15 line-shifted sites by their stored `before`
TEXT (0 not found), so last commit's "R5 mutants are not replayable" is obsolete
and the report section is rewritten with the measured figures.

NOT RE-VERIFIED, AND THE REPORT SAYS SO: that mutant's CLASSIFICATION was measured
at `meta.commit` and is not re-established here. The CI replay checks byte triage
for UNTESTED entries, not the oracle suite (that needs --full). The published rate
stays relative to the commit the ledger names.

A LOCAL FULL RE-SURVEY WAS ATTEMPTED AND DISCARDED AS INVALID, recorded because
the near-miss matters: 147 of the 196 L1 steps invoke bare `python`, absent on
this machine, so they exit 127 in 0.1s and the harness scores that as a KILL; and
`fact_spec_div_494_differential.py` is red on the UNMUTATED tree here while green
in CI. That run reported 0 of 29 surviving — dead oracles, not a result. The
harness's own control check refused it: "1 control(s) not killed — the survey
measures nothing; do not publish the rate". A gate that stops its author
publishing a flattering number is the one worth having.

Refs #1189, #1232, #1227

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

---------

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant