RQ-59-WARALIAS (#989): ARM local.set/tee WAR aliasing — snapshot home-register aliases; optimized-path WAR + dropped-param-store declines (red-first)

.github/workflows/ci.yml

@@ -3624,6 +3624,8 @@ jobs:
         run: pip install wasmtime unicorn pyelftools capstone
       - name: "#973 i64-cmp select execution differential (both ARM legs)"
         run: python scripts/oracle_run.py scripts/repro/select_i64cmp_973_arm_differential.py
+      - name: "#989 local.set/tee WAR-aliasing execution differential (both ARM legs)"
+        run: python scripts/oracle_run.py scripts/repro/war_aliasing_989_arm_differential.py
       - name: "ARM corpus sweep — compile census + execution differential (#973)"
         run: python scripts/oracle_run.py scripts/repro/arm_corpus_sweep_973.py
       # #910: close the job with what it EXECUTED. Asserts every oracle
@@ -3636,7 +3638,7 @@ jobs:
         if: always()
         run: |
           set -euo pipefail
-          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 2
+          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 3
 
   repro-sweep-wcet-oracle:
     name: repro sweep — WCET bound soundness cross-checks (phases 2-6)

CHANGELOG.md

@@ -7,6 +7,30 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+### Fixed
+
+- **#989 (RQ-59-WARALIAS): ARM `local.set`/`local.tee` clobbered an earlier
+  `local.get` of the same local still on the operand stack (WAR aliasing).**
+  `local.get` of a register-homed local (param in r0-r3, promoted local in
+  r4-r8) pushed the HOME register by reference; a later write to the same
+  local destroyed the pushed value — `war_set` returned 200 for every input.
+  Fixed on BOTH ARM lowering paths, gated by a new executed unicorn-vs-wasmtime
+  differential (`war_aliasing_989_arm_differential.py`, 110 wrong vectors → 0,
+  wired in CI) landed RED-FIRST before the fix:
+  - direct selector (`select_with_stack`, the `--relocatable`/production
+    path): new `snapshot_home_reg_aliases` guard — the ARM analogue of RV32's
+    #472 `snapshot_aliases` — copies still-live aliases to a fresh temp before
+    the home register is overwritten (i64 pairs snapshotted as consecutive
+    pairs, defence in depth);
+  - optimized IR path (self-contained straight-line functions): the same WAR
+    shape now LOUD-DECLINES to the direct selector (#500/#188-style honest
+    degradation), and a `local.set` of a PARAMETER — whose write the IR
+    lowering silently DROPPED (`swap_two_params` returned p0−p1 instead of
+    p1−p0) — declines likewise instead of miscompiling.
+  The four #989 entries left `KNOWN_ARM_MISMATCHES` (the sweep's
+  both-direction ratchet records the fix); all 10 frozen anchors are
+  byte-identical — no frozen fixture carries the WAR shape.
+
 ## [0.58.0] - 2026-08-20
 
 **Delete the thing you replaced.**

artifacts/status.json

@@ -28,8 +28,8 @@
   "sel_dsl_rule_qed": 74,
   "sel_dsl_rules": 74,
   "sel_rules_simplified_basis": 74,
-  "selector_lines_code": 17961,
-  "selector_lines_total": 28582,
+  "selector_lines_code": 18134,
+  "selector_lines_total": 28755,
   "selector_wildcard_arms_code": 55,
   "selector_wildcard_arms_total": 90,
   "version": "0.58.0",

claims.yaml

@@ -1255,7 +1255,7 @@ claims:
       - kind: ratchet
         name: selector_lines_code
         direction: down
-        value: 17961
+        value: 18134
         baseline: 17897
         waivers:
           - to: 17961
@@ -1299,6 +1299,20 @@ claims:
               the hand-written imm-fold/conversion/select emissions, each
               byte-identity-gated — the residual 15 above baseline is the
               #946 enumeration, still justified as stated above.
+          - to: 18134
+            reason: >-
+              RQ-59-WARALIAS (#989): the executed local.set/local.tee WAR
+              miscompile — `local.get` of a register-homed local pushed the
+              HOME register by reference, and a later write to the SAME
+              local destroyed it (war_set returned 200 for every input, 44
+              wrong vectors across 4 exports). +173 lines are the
+              `snapshot_home_reg_aliases` guard (the ARM analogue of RV32's
+              #472 `snapshot_aliases`) plus its four call sites in the
+              LocalSet/LocalTee register-homed arms — new SOUNDNESS
+              decisions, zero wildcards, gated by the executed
+              war_aliasing_989_arm_differential (110 wrong vectors -> 0,
+              both ARM legs) and the corpus sweep's both-direction ratchet
+              (the four #989 KNOWN_ARM_MISMATCHES entries deleted).
       # The whole-file figures the release plan and the sibling lanes quote. An
       # unpinned quoted number is the drift class this release is about — but
       # they are `track`, not `down`, and the distinction is deliberate. Both
@@ -1327,7 +1341,10 @@ claims:
         # the 2,503 moved lines themselves are ±0 under the family glob.
         # 28559 -> 28582 (RQ-58-SPLIT unit 2): +23 module plumbing for the
         # select_with_stack.rs relocation; the 7,754 moved lines are ±0.
-        value: 28582
+        # 28582 -> 28755 (RQ-59-WARALIAS #989): +173 code, all in the
+        # snapshot_home_reg_aliases WAR guard + its four call sites (see the
+        # lines_code waiver); zero test-module movement.
+        value: 28755
       # RQ-58-WILDCARD's real denominator, and THE directed wildcard pin. 62
       # absorbing arms are in the lowering code; the other 43 of the plan's 105
       # are assertion helpers in the test module, where a `_ =>` is not a

crates/synth-synthesis/src/instruction_selector.rs

@@ -1037,6 +1037,116 @@ fn spill_deepest_reg(
     Ok(true)
 }
 
+/// #989 — the ARM analogue of the RV32 selector's `snapshot_aliases` (#472):
+/// before a `local.set`/`local.tee` overwrites a register-homed local's HOME
+/// register `target` (a param in r0-r3 or a #390-promoted local in r4-r8),
+/// copy any operand-stack entry that still ALIASES `target` — pushed by an
+/// EARLIER `local.get` of the same local, which aliases the home register
+/// by reference rather than copying — into a fresh temp, and rewrite those
+/// entries to the temp. Without this, the `mov target, val` destroys the
+/// earlier value (the get→set→use WAR hazard): `war_set` returned 200 for
+/// EVERY input (44 wrong vectors across 4 exports, executed in #989).
+///
+/// `skip` is the operand-stack index NOT to rewrite — `local.tee`'s own kept
+/// top IS the value being written and stays aliased to its producer. Fires
+/// only when an alias is present, so code without the WAR shape emits nothing
+/// and stays byte-identical.
+///
+/// The aliased entries are still ON the stack during allocation, so the
+/// allocators cannot return `target` itself; `reserved` must carry the
+/// just-popped/peeked `val` (plus the live params) so the temp cannot land on
+/// the value about to be written either. The spill fallback inside the
+/// allocators is sound here: spilling an ALIASED entry stores `target`'s
+/// current (pre-write) value — exactly the value the entry needs — and the
+/// entry stops aliasing.
+///
+/// i64 defence in depth (RV32 checks pair halves too): an i64 entry whose
+/// pair overlaps `target` (lo == target or hi == target) is snapshotted as a
+/// whole pair into a fresh CONSECUTIVE pair — ARM i64 stack entries derive
+/// hi = lo+1 (`i64_pair_hi`), so rewriting one half alone is unrepresentable.
+fn snapshot_home_reg_aliases(
+    target: Reg,
+    skip: Option<usize>,
+    stack: &mut [StackVal],
+    next_temp: &mut u8,
+    instructions: &mut Vec<ArmInstruction>,
+    spill: &mut SpillState,
+    reserved: &[Reg],
+    line: usize,
+) -> Result<()> {
+    let overlaps = |v: &StackVal| -> bool {
+        if let StackVal::Reg { reg, is_i64 } = v {
+            *reg == target || (*is_i64 && i64_pair_hi(*reg).is_ok_and(|hi| hi == target))
+        } else {
+            false // spilled/VFP entries hold no core register
+        }
+    };
+    let aliased = |stack: &[StackVal], wide: bool| -> bool {
+        stack
+            .iter()
+            .enumerate()
+            .any(|(i, v)| Some(i) != skip && v.is_i64() == wide && overlaps(v))
+    };
+    if aliased(stack, false) {
+        let tmp = alloc_temp_or_spill(next_temp, stack, instructions, spill, reserved, line)?;
+        instructions.push(ArmInstruction {
+            op: ArmOp::Mov {
+                rd: tmp,
+                op2: Operand2::Reg(target),
+            },
+            source_line: Some(line),
+        });
+        for (i, v) in stack.iter_mut().enumerate() {
+            if Some(i) != skip
+                && let StackVal::Reg { reg, is_i64: false } = v
+                && *reg == target
+            {
+                *reg = tmp;
+            }
+        }
+    }
+    // The allocator's spill fallback may itself de-alias entries (see above),
+    // so re-check after every pair allocation rather than trusting the first
+    // scan — a dead snapshot MOV for an entry that just got spilled would be
+    // harmless but is refused on principle (emit only what is still needed).
+    while aliased(stack, true) {
+        let (new_lo, new_hi) =
+            alloc_consecutive_pair(next_temp, stack, instructions, spill, &[], reserved, line)?;
+        let mut found = None;
+        for (i, v) in stack.iter().enumerate() {
+            if Some(i) != skip
+                && let StackVal::Reg { reg, is_i64: true } = v
+                && overlaps(v)
+            {
+                found = Some(*reg);
+                break;
+            }
+        }
+        let Some(old_lo) = found else {
+            break; // the pair allocation's spill fallback de-aliased everything
+        };
+        let old_hi = i64_pair_hi(old_lo)?;
+        for (rd, rs) in [(new_lo, old_lo), (new_hi, old_hi)] {
+            instructions.push(ArmInstruction {
+                op: ArmOp::Mov {
+                    rd,
+                    op2: Operand2::Reg(rs),
+                },
+                source_line: Some(line),
+            });
+        }
+        for (i, v) in stack.iter_mut().enumerate() {
+            if Some(i) != skip
+                && let StackVal::Reg { reg, is_i64: true } = v
+                && *reg == old_lo
+            {
+                *reg = new_lo;
+            }
+        }
+    }
+    Ok(())
+}
+
 /// Reconcile one if-result position between the two arms (#313): make the
 /// else-arm's result register(s) hold the SAME value the then-arm's do, by
 /// emitting `MOV R_then, R_else` (i64: lo and hi) on the ELSE path when the two

crates/synth-synthesis/src/instruction_selector/select_with_stack.rs

@@ -5174,6 +5174,22 @@ impl InstructionSelector {
                     } else if *local_idx < num_params.min(4) {
                         let target = index_to_reg(*local_idx as u8);
                         if val != target {
+                            // #989: an EARLIER `local.get` of this same param
+                            // pushed `target` by reference — copy any such
+                            // still-live stack entry out before the overwrite
+                            // destroys it (the get→set→use WAR hazard).
+                            let mut rsv = live_params.clone();
+                            rsv.push(val);
+                            snapshot_home_reg_aliases(
+                                target,
+                                None,
+                                &mut stack,
+                                &mut next_temp,
+                                &mut instructions,
+                                &mut spill,
+                                &rsv,
+                                idx,
+                            )?;
                             instructions.push(ArmInstruction {
                                 op: ArmOp::Mov {
                                     rd: target,
@@ -5193,6 +5209,21 @@ impl InstructionSelector {
                         // only elides a redundant self-move. Checked before
                         // `layout.locals` so the dead frame slot is never written.
                         if val != target {
+                            // #989: same WAR snapshot as the param arm —
+                            // `local.get` of a promoted local aliases r4..r8
+                            // by reference.
+                            let mut rsv = live_params.clone();
+                            rsv.push(val);
+                            snapshot_home_reg_aliases(
+                                target,
+                                None,
+                                &mut stack,
+                                &mut next_temp,
+                                &mut instructions,
+                                &mut spill,
+                                &rsv,
+                                idx,
+                            )?;
                             instructions.push(ArmInstruction {
                                 op: ArmOp::Mov {
                                     rd: target,
@@ -5293,6 +5324,23 @@ impl InstructionSelector {
                     } else if *local_idx < num_params.min(4) {
                         let target = index_to_reg(*local_idx as u8);
                         if val != target {
+                            // #989: snapshot earlier `local.get` aliases of this
+                            // param's home register before overwriting it. The
+                            // tee's own kept top is SKIPPED — it is the value
+                            // being written and stays aliased to its producer.
+                            let mut rsv = live_params.clone();
+                            rsv.push(val);
+                            let top_idx = stack.len() - 1;
+                            snapshot_home_reg_aliases(
+                                target,
+                                Some(top_idx),
+                                &mut stack,
+                                &mut next_temp,
+                                &mut instructions,
+                                &mut spill,
+                                &rsv,
+                                idx,
+                            )?;
                             instructions.push(ArmInstruction {
                                 op: ArmOp::Mov {
                                     rd: target,
@@ -5310,6 +5358,21 @@ impl InstructionSelector {
                         // later `local.get` both see the same value from independent
                         // homes. Reserved like LocalSet, so `val != target`.
                         if val != target {
+                            // #989: same WAR snapshot as the param arm, top
+                            // skipped (tee semantics).
+                            let mut rsv = live_params.clone();
+                            rsv.push(val);
+                            let top_idx = stack.len() - 1;
+                            snapshot_home_reg_aliases(
+                                target,
+                                Some(top_idx),
+                                &mut stack,
+                                &mut next_temp,
+                                &mut instructions,
+                                &mut spill,
+                                &rsv,
+                                idx,
+                            )?;
                             instructions.push(ArmInstruction {
                                 op: ArmOp::Mov {
                                     rd: target,