Skip to content

fix(selector): RQ-65-DECLINE (#1208) — narrow i64 memory ops, i64 select and computed-condition value-if decline to the direct selector - #1228

Merged
avrabe merged 2 commits into
mainfrom
fix/decline-1208
Sep 9, 2026
Merged

fix(selector): RQ-65-DECLINE (#1208) — narrow i64 memory ops, i64 select and computed-condition value-if decline to the direct selector#1228
avrabe merged 2 commits into
mainfrom
fix/decline-1208

Conversation

@avrabe

@avrabe avrabe commented Sep 9, 2026

Copy link
Copy Markdown
Contributor

RQ-65-DECLINE (#1208) — silent wrong answers on the optimized path become loud declines

Refs #1208, #1213, #1205 (declined), #1204, #1206 (classified, stay pinned), #1209 #1210 #1211 #1214 #1215 (class c, stay pinned), #1207 (acceptance bug). Artifact: artifacts/release-v0.65/RQ-65-DECLINE.yaml (status: implemented; the file is also modified by #1219 — if that merges first, the rebase keeps both edits).

The anchor, reproduced before anything was changed

Eleven one-op modules (memory 1) (func (export "f") (param i32) ...), main binary (580d53f9), default vs --no-optimize, function bytes read from the ELF symtab:

op optimized (default) direct (--no-optimize)
i64.load8_s/u, load16_s/u, load32_s/u 7047 = bx lr, the whole body; [path-debug] optimized (ir_to_arm ok) ldrsb/ldrb/ldrsh/ldrh/ldr + extend into r0:r1
i64.store8/16/32 (const or extended value) value to r4:r5, mov r1,r5; mov r0,r4; pop — no store strb.w/strh.w/str.w r1,[fp,r0]
i64.load / i64.store direct (fallback: … issue #372), byte-equal to direct real code

All eleven exit 0, no warning. On this branch all nine narrow forms are direct (fallback: … issue #1208) and byte-equal to --no-optimize.

Classification — every optimized-path-only defect, each by ITS OWN bytes and executed result

The coordinator's mid-task correction is honoured: the direct selector is not globally trustworthy (#1222 is on it), so no decline below rests on a blanket claim.

issue class why landed
#1208 narrow i64 memory ops (a) decline sufficient direct bytes read for all nine ops (table above); address.wast m1's 90 assertions execute equal to wasmtime on the direct leg yes — the #372 guard extended to the nine forms
#1213 i64 select (a) direct sel64_lo moves the PAIR under it ne/eq (movne r5,r1; movne r6,r2; moveq r5,r3; moveq r6,r4); probe (sel64_wrap, sel64_lo x2) and spec as-convert-operand equal to wasmtime yes — Select arm declines when either value operand is in i64_halves, a set fed by the one push_i64 helper every pair producer now pushes through (no second type walk)
#1205 value-if, computed condition (a) direct vif_gt = cmp r0,r1; ite gt; movgt/movle r2; cmp r2,#0; beq … — a real compare on the operands; probe shapes gt_s/add/eqz/mixed-arm and spec check_jam x7, load.wast/local_tee.wast as-if-cond equal to wasmtime yes — the Pattern-1 rewrite (preprocess_wasm_ops, now Result) declines instead of moving a non-zero-input condition past the arm values. Pattern 2 is unaffected (it re-emits the popped condition in place)
#1204 unsaved R9–R11 write not decline-shaped (b, refused with the measurement) the only covering predicate ("emitted code writes R9–R11 unsaved") diverts 17/1831 optimized functions on the parity corpus (0.9 %) but 19/359 (5.3 %) on scripts/repro — and those 19 are base_cse_branch, redundant_base_materialization, spill_frame_499, stack_canary_687, volatile_segment_543, …: the memory-heavy shapes the optimized path exists for, several of them frozen goldens. Fix = the prologue save (ensure_callee_saved_prologue hard-codes R4–R8) no — stays pinned
#1206 loop-carried non-param local not decline-shaped countdown, countdown_set, countdown_nop_first hang; countdown_param and sum_to_n — same pre-loop-defined, in-loop-redefined local — are correct; none of the four lever opt-outs changes it. No statable predicate short of "every loop redefining a pre-loop local" no — stays pinned
#1209 #1210 #1211 #1214 #1215 (c) wrong on BOTH selectors nothing correct to fall back to no — stay pinned
#1207 acceptance bug (validator) not a lowering no

None of the three landed declines can relocate a function into #1222's class: has_wide_param routes every i64-param function to the direct selector BEFORE the bridge runs, so every re-routed function has no i64 param by construction.

The pins moved — red-first, inherited

Parity oracle, main binary: RESULT: PASS, 722 pinned assertions / 108 pins, 19145 assertions / 328 modules (main's table reproduced exactly; wasmtime-py 48.0.0, unicorn 2.1.4).

New binary, OLD pin table: exit 1 with exactly five PINNED DIVERGENCE VANISHED lines — anti_pinch.wast m0 check_jam (pinned 7, #1205), load.wast m0 as-if-cond (1, #1205), local_tee.wast m0 as-if-cond (1, #1205), address.wast m1 * (90, #1208), select.wast m0 as-convert-operand (1, #1213) — unpinned: 0, every non-vacuity floor met (optimized_funcs 1211 >= 1150, differing_funcs 1423 >= 1350), 19145/19145 assertions over 328 modules

New binary, edited table (the five pins removed): the discriminating subset on the rebased tree (--only address, select, anti_pinch, local_tee, load, plus the untouched controls control_*, r11_clobber, int_literals): unpinned: 0 in every run, no moved pin, the remaining #1209/#1210/#1204/#1206/#539 pins in those files hold at exactly their counts; the full run is the CI job on the pushed tree

Population: optimized routing 1267 → 1211, fallback 1527 → 1583, byte-differing functions 1479 → 1423, verdict ok 12447 → 12547, parity-divergence 158 → 58, contract-violation 14 → 14 (#1204, untouched).

Byte identity, proved not reasoned

Main binary vs branch over all 205 scripts/repro inputs, three ARM configurations:

configuration identical differing newly-declined newly-accepted both-declined
--relocatable (direct) 137 0 0 0 68
self-contained, default 173 1 0 0 31
self-contained, --no-optimize 174 0 0 0 31

The one difference is mem746_wide_static.wat: its three narrow-op functions (narrow8, narrow16s, narrow32) plus ONE Reset_Handler immediate — movw r0,#592movw r0,#744 (+0x98), which is exactly the .text growth 0x278 → 0x310 of those three bodies (the address of the #758 data-segment initializer blob that follows the code inside .text: blob start = text size - 0x28 on both binaries). Function counts are equal in every config.

Reach, measured

No module and no function newly declines in any configuration — the fallback is per-function and the direct selector accepts every re-routed function. Denominators: 205 repro inputs × 3 configs (above), the parity corpus (2245 modules; routing above), and the real modules on this host: 221 loom/kiln/relay inputs — default config 37 identical / 0 differing / 0 newly declined (184 decline on BOTH binaries: import-carrying modules need --relocatable), --relocatable 23 / 0 / 0 (198 both-declined); function and fallback counts equal on both binaries. The 805-module corpus (#1017) is gale's and is not on this machine — stated, not estimated.

The ledger pin that could not have failed

SYNTH-ARCH-LOUD-DECLINE bound "declines loudly" to fn is_intentionally_ignored in the DECODER — one layer above the lowering that emitted bx lr. Re-pointed at the lowering layer: exact count of optimized-path decline sites in optimizer_bridge.rs (14) and exact count of pinned optimized-path wrong answers in the parity oracle (4, the named residual). Sensitivity, run and restored:

[baseline] claim_check exit=0            ok   SYNTH-ARCH-LOUD-DECLINE
[mutation A: #1208 decline site removed from the count] exit=1
    FAIL SYNTH-ARCH-LOUD-DECLINE  count drifted: derived 13 != documented 14
[restored A] exit=0
[mutation B: #1208 re-pinned as a KNOWN opt-wrong] exit=1
    FAIL SYNTH-ARCH-LOUD-DECLINE  count drifted: derived 5 != documented 4
[restored B] exit=0     files restored byte-identical; 62/62 claims hold

The ARCHITECTURE.md sentence now says how the rule is enforced and names what remains pinned.

Gates run before push

cargo fmt --check, cargo clippy --workspace --all-targets -- -D warnings, unit tests 7/7 bridge + 4/4 backend, oracle_wiring_check.py --exact-emulation-floor 345122 (no script header changed; floor re-derives unchanged), claim_check.py 62/62, status_evidence_check.py, rivet validate (40 errors — the main baseline, none new).

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

avrabe added a commit that referenced this pull request Sep 9, 2026
…measured evidence, CHANGELOG entry

The RQ-65-DECLINE artifact moves proposed -> implemented with `landed:`
(what PR #1228 carries) and `verified-by:` (the per-defect classification,
each justified by the direct selector's bytes and executed result for its
own shape; the anchor, parity red-first, byte-identity, reach and ledger-
sensitivity runs as actually executed). The emulation floor is referred to
as re-derived by oracle_wiring_check, never restated (floor-prose 0).
CHANGELOG [Unreleased] gains the entry under main's existing header.

Refs #1208 #1213 #1205 #1204 #1206

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

codecov Bot commented Sep 9, 2026

Copy link
Copy Markdown

Codecov Report

❌ Patch coverage is 97.72727% with 6 lines in your changes missing coverage. Please review.

Files with missing lines Patch % Lines
crates/synth-backend/src/arm_backend.rs 95.45% 3 Missing ⚠️
crates/synth-synthesis/src/optimizer_bridge.rs 98.48% 3 Missing ⚠️

📢 Thoughts on this report? Let us know!

avrabe and others added 2 commits September 9, 2026 06:02
…ect and computed-condition value-if decline to the direct selector

Three optimized-path miscompile classes RQ-65-PARITY found by executing the
spec suite — every one exit 0, no warning — now decline with a machine reason
in the #120/#372/#374 pattern; the direct selector's bytes were read for each
shape and its executed results equal wasmtime, so each fallback is complete:

- #1208 the nine narrow i64 memory forms (i64.load8/16/32_{s,u},
  i64.store8/16/32): loads lowered to an EMPTY body (bx lr), stores dropped.
  The #372 guard is extended to the nine forms.
- #1213 an i64 `select` (register-pair operands): Opcode::Select moves one
  register. The Select arm declines when a value operand is in `i64_halves`,
  fed by the one `push_i64` helper every pair producer now pushes through.
- #1205 a value-`if` with simple arms and a COMPUTED condition: the select
  rewrite moved the condition past the arm values. `preprocess_wasm_ops` is
  now `Result` and declines instead.

Classified, not landed, with measurements: #1204 (an unsaved R9-R11 write —
the covering predicate diverts 0.9 % of optimized functions on the spec
corpus but 5.3 % on scripts/repro, the memory-heavy shapes the optimized path
exists for; the fix is the prologue save) and #1206 (loop-carried non-param
local; class boundary not statable — sum_to_n has the shape and is correct).
#1209/#1210/#1211/#1214/#1215 are wrong on both selectors and stay pinned.

Evidence: the parity oracle on the new binary with the OLD table reports
exactly the five pins as VANISHED (90+7+1+1+1 assertions -> ok, unpinned 0);
the pins are removed here. Byte identity over 205 scripts/repro inputs x 3
ARM configs: one differing module (mem746_wide_static.wat: its three
narrow-op functions + one Reset_Handler immediate tracking the grown .text);
0 newly declined in every config and on 221 local real modules.

SYNTH-ARCH-LOUD-DECLINE re-pointed from the decoder's
`fn is_intentionally_ignored` (green by construction while i64.load8_u
lowered to bx lr) to the lowering layer: exact count of optimized-path
decline sites (14) and of pinned optimized-path wrong answers in the parity
oracle (4). Sensitivity proved by mutation (13 != 14, 5 != 4), restored.
ARCHITECTURE.md's honesty sentence now states how it is enforced and what
remains pinned.

Refs #1208 #1213 #1205 #1204 #1206 #197

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…measured evidence, CHANGELOG entry

The RQ-65-DECLINE artifact moves proposed -> implemented with `landed:`
(what PR #1228 carries) and `verified-by:` (the per-defect classification,
each justified by the direct selector's bytes and executed result for its
own shape; the anchor, parity red-first, byte-identity, reach and ledger-
sensitivity runs as actually executed). The emulation floor is referred to
as re-derived by oracle_wiring_check, never restated (floor-prose 0).
CHANGELOG [Unreleased] gains the entry under main's existing header.

Refs #1208 #1213 #1205 #1204 #1206

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