fix(#973): ARM select on an i64-comparison returns the then-arm — and an ARM leg for the corpus CI never compiled

.github/workflows/ci.yml

@@ -260,7 +260,7 @@ jobs:
         run: |
           set -euo pipefail
           python3 scripts/oracle_wiring_check.py --json /tmp/oracle-wiring.json --list \
-            --min-emulation-floor 295726 \
+            --min-emulation-floor 298754 \
             | tee /tmp/oracle-wiring.log
           python3 - <<'PY'
           import json, sys
@@ -3508,6 +3508,76 @@ jobs:
           set -euo pipefail
           python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 11
 
+  repro-sweep-arm-corpus-oracle:
+    name: "repro sweep — ARM corpus (#973: CI never compiled these for ARM)"
+    # RQ-58-SELECT973, the second half and the larger one. #973 — `select` on an
+    # i64-comparison condition returning the then-arm on every vector where the
+    # else-arm was due — was found only because a lane compiled
+    # `scripts/repro/*.wat` for ARM BY HAND. Nothing in CI did that. The
+    # `repro-sweep-*` jobs above run hand-listed oracles, each pinned to the one
+    # fixture its issue was about, so a fixture written for RV32 or aarch64 never
+    # reached the ARM backend even when its shape is backend-independent.
+    # `rv32_cmp_select_472.wat` carried the #973 shape as `sel_cmp_i64` since
+    # v0.11 and no ARM build ever saw it — MEASURED: run against the PRE-fix
+    # binary this sweep reports 7 wrong vectors for exactly that export, so the
+    # leg is red-first against the defect it was built for, using a fixture that
+    # was already in the tree.
+    #
+    # Two phases, because compiling alone would NOT have caught #973 (it compiled
+    # perfectly and returned the wrong number): a no-wildcard COMPILE census over
+    # every fixture, then an EXECUTION differential against wasmtime over every
+    # all-i32 export of every module pure enough to emulate faithfully.
+    #
+    # Turning this on surfaced 48 pre-existing wrong vectors unrelated to #973 —
+    # #989 (a local.set/tee clobbers a live local.get of the same local) and #990
+    # (a local written on one arm of a br_if is never zero-inited, so the merge
+    # reads uninitialised stack). They are LISTED by name against their issue
+    # inside the harness and ratcheted in both directions, not narrowed away.
+    runs-on: ubuntu-latest
+    env:
+      SYNTH: ./target/debug/synth
+    steps:
+      - uses: actions/checkout@v7
+      - uses: dtolnay/rust-toolchain@stable
+      - name: Cache Cargo dependencies
+        uses: actions/cache@v6
+        with:
+          path: |
+            ~/.cargo/registry
+            ~/.cargo/git
+            target/
+          key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }}
+          restore-keys: |
+            ${{ runner.os }}-cargo-
+      - name: Build synth
+        run: cargo build -p synth-cli
+      - uses: actions/setup-python@v7
+        with:
+          python-version: "3.x"
+      # Deliberately NO wabt. Both oracles here assemble `.wat` with wasmtime's
+      # OWN assembler (`wasmtime.wat2wasm` / `Module.from_file`), so the
+      # reference side is ONE toolchain: what parses and what runs cannot
+      # disagree, and the executed population does not depend on the runner's
+      # wabt build. That host-dependency class (#850/#881) is the one thing a
+      # never-before-run job discovers the hard way.
+      - name: Install emulation deps
+        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: "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
+      # met its declared floor AND that the expected number of them
+      # reported at all — a step deleted, commented out, or skipped by an
+      # early exit leaves the ledger short, which is a red job rather than
+      # a quietly smaller number. Also writes the measured totals to the
+      # step summary, per unit, never summed.
+      - name: Differential evidence ledger (#910)
+        if: always()
+        run: |
+          set -euo pipefail
+          python3 scripts/oracle_evidence.py "$ORACLE_EVIDENCE_JSONL" --min-oracles 2
+
   repro-sweep-wcet-oracle:
     name: repro sweep — WCET bound soundness cross-checks (phases 2-6)
     # #890: the SOUNDNESS evidence for --emit-wcet. The cargo gate

claims.yaml

@@ -1143,7 +1143,7 @@ claims:
   # ---------------------------------------------------------------------------
   - id: SYNTH-ORACLE-CHECK-FLOORS-910
     doc: scripts/repro/ORACLE_WIRING.md
-    text: "**296,059 emulator entries**"
+    text: "**298,754 emulator entries**"
     evidence:
       - kind: file-exists
         path: scripts/oracle_run.py
@@ -1156,13 +1156,13 @@ claims:
       - kind: count-min                      # the EXECUTION population, per script
         pattern: '^# ci-checks: emulations >= '
         glob: ['scripts/repro/*.py', 'scripts/repro/*.sh']
-        min: 144
+        min: 146
       - kind: count-max                      # the "nothing can be bound" hatch
         pattern: '^# ci-checks: none'
         glob: ['scripts/repro/*.py', 'scripts/repro/*.sh']
         max: 1
       - kind: verbatim                       # the doc carries the per-mode split
-        text: "**144 oracles**"
+        text: "**146 oracles**"
       - kind: verbatim
         text: "Reported per mode and never summed across modes."
       - kind: verbatim                       # the itemized weak-floor list stays
@@ -1183,14 +1183,14 @@ claims:
   # ---------------------------------------------------------------------------
   - id: SYNTH-ORACLE-CHECK-FLOORS-910-MATRIX
     doc: scripts/templates/feature_matrix.md.tmpl
-    text: "**144 oracles assert 296,059 emulator"
+    text: "**146 oracles assert 298,754 emulator"
     evidence:
       - kind: file-exists
         path: scripts/oracle_run.py
       - kind: count-min                      # same population the other two pin
         pattern: '^# ci-checks: emulations >= '
         glob: ['scripts/repro/*.py', 'scripts/repro/*.sh']
-        min: 144
+        min: 146
 
   # ---------------------------------------------------------------------------
   # #910 — the CI side of the same claim, pinned so the doc's number and the
@@ -1200,7 +1200,7 @@ claims:
   # ---------------------------------------------------------------------------
   - id: SYNTH-ORACLE-CHECK-FLOORS-910-CI
     doc: .github/workflows/ci.yml
-    text: "--min-emulation-floor 295726"
+    text: "--min-emulation-floor 298754"
     evidence:
       - kind: count-min                      # oracle steps routed through the driver
         pattern: 'oracle_run\.py scripts/repro/'