aarch64: br_table + value-carrying block/loop/if (#851, VCR-A64-CF-001)

.github/workflows/ci.yml

@@ -217,7 +217,7 @@ jobs:
         run: |
           set -euo pipefail
           python3 scripts/oracle_wiring_check.py --json /tmp/oracle-wiring.json --list \
-            --min-emulation-floor 295333 \
+            --min-emulation-floor 295421 \
             | tee /tmp/oracle-wiring.log
           python3 - <<'PY'
           import json, sys
@@ -576,9 +576,15 @@ jobs:
     # CNT/ADDV), and f64<->i64 reinterpret. v0.54 L2 completes the SCALAR float
     # surface — rounding (FRINT), f32/f64 load/store (bounds-checked), i64->
     # float converts, and the DOMAIN-GUARDED trapping i64-target truncations —
-    # so the decline-matrix probe now asserts the STRUCTURAL declines
-    # (call_indirect, br_table, param writes, globals, bulk memory,
-    # value-carrying blocks, SIMD) still LOUD-decline.
+    # so the decline-matrix probe moved on to the STRUCTURAL declines. v0.54 L3
+    # then landed call_indirect + globals and v0.55 L6 (VCR-A64-CF-001)
+    # `br_table` + value-carrying block/loop/if, so what the probe asserts today
+    # is the NARROWER residue: param writes in a LEAF function, bulk memory,
+    # SIMD, a `br_table` past 16 targets or with value-carrying targets, a block
+    # type with params / multi-value results, and a non-leaf FLOAT param. Each
+    # entry LEAVES this list the day its lowering lands — asserting a decline
+    # for a capability that now ships is the same doc-honesty defect as claiming
+    # one that does not.
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v7
@@ -689,6 +695,41 @@ jobs:
           echo "float-completion oracle ran $n checks, $t of them trap cases"
           [ "$n" -ge 300 ]
           [ "$t" -ge 40 ]
+      - name: Run v0.55 L6 br_table + VALUE-CARRYING block/loop/if oracle (VCR-A64-CF-001)
+        # The two largest entries in the mechanically-derived aarch64 decline
+        # complement, now lowered. `br_table` is a compare-and-branch CHAIN, so
+        # a wrong destination is a wrong RESULT: the harness walks the index
+        # lattice per table (every arm, the index AT the bound, one OVER it, and
+        # 0xFFFFFFFF — which a SIGNED compare would mis-dispatch, since WASM
+        # reads the index UNSIGNED), and puts a LOOP HEADER in the same table as
+        # a forward block end so a wrong branch DIRECTION shows up as a wrong
+        # trip count. The value-carrying frames are driven down BOTH edges of
+        # every join, including a frame containing a `bl` — the one soundness
+        # claim (a call cannot clobber a live reconciliation slot) that nothing
+        # else executes.
+        #
+        # ANTI-VACUITY (#890). `set -euo pipefail`, NOT bare `pipefail`: with
+        # pipefail ALONE the step's exit status is the LAST command's, so an
+        # oracle that printed FAIL and exited 1 still went GREEN. The verdict is
+        # then taken from the script's OWN summary line, and the counts are
+        # asserted NON-ZERO in both outcome classes — an oracle that stopped
+        # trapping (or stopped returning values) must go RED. The relocation
+        # count is asserted too: the harness APPLIES the `R_AARCH64_CALL26`
+        # relocations itself, and if they vanished the calls would become
+        # self-branches and the clobber claim would go untested while the gate
+        # stayed green.
+        run: |
+          set -euo pipefail
+          SYNTH=./target/debug/synth \
+            python scripts/oracle_run.py \
+              scripts/repro/aarch64_brtable_blockvals_851_differential.py \
+            | tee /tmp/a64_brtable.log
+          grep -q '^RESULT: PASS' /tmp/a64_brtable.log
+          grep -Eq '^[1-9][0-9]* checks \([1-9][0-9]* trap, [1-9][0-9]* value\) across [1-9][0-9]* exported' /tmp/a64_brtable.log
+          grep -Eq '\[[1-9][0-9]* direct-call relocations applied\]' /tmp/a64_brtable.log
+          n=$(sed -n 's/^\([0-9]*\) checks .*/\1/p' /tmp/a64_brtable.log)
+          echo "br_table/value-carrying oracle ran $n checks"
+          [ "$n" -ge 60 ]
       - name: Run decline-matrix honesty oracle
         run: SYNTH=./target/debug/synth python scripts/oracle_run.py scripts/repro/aarch64_m2_decline_538.py
       # #910: close the job with what it EXECUTED. Asserts every oracle

CHANGELOG.md

@@ -55,12 +55,12 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   not "checks", because naming a measurement after something it does not measure
   is the defect this lane exists to remove.
 
-- **The differential population is reported, and ratcheted.** **135 oracles
-  assert 295,333 emulator entries per CI run**; 7 assert a printed count, 9
+- **The differential population is reported, and ratcheted.** **136 oracles
+  assert 295,421 emulator entries per CI run**; 7 assert a printed count, 9
   assert compilations, 1 can bind to nothing. Reported **per mode and never
   summed across modes** — three different units, and one impressive combined
   figure is exactly the instrument defect being fixed.
-  `oracle_wiring_check.py --min-emulation-floor 295333` enforces the total in
+  `oracle_wiring_check.py --min-emulation-floor 295421` enforces the total in
   the already-required `Claim Check` job (a brand-new job is not a required
   context on `main` and could sit red for weeks — the #890 failure), sharing the
   driver's header parser by import rather than re-implementing the grammar.
@@ -157,6 +157,29 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Added
 
+- **aarch64 `br_table` + value-carrying `block`/`loop`/`if` (VCR-A64-CF-001,
+  #851).** The two largest entries left in the VCR-SEL-005 third-backend
+  complement were structural, not arithmetic — and both made whole functions
+  skip on `-b aarch64`. `br_table` now lowers as a compare-and-branch chain
+  (`cbz` for entry 0, `cmp`+`b.eq` per further entry, then the default `b`),
+  deliberately the same construction #882 chose for RV32 so the two backends
+  stay reviewable against each other; the index is compared in the W view, so
+  the UNSIGNED index rule holds exactly and every out-of-range index —
+  including the "negative" i32s that denote huge unsigned values — reaches the
+  DEFAULT. One table may MIX a backward loop header with forward block ends.
+  A value-carrying frame reserves a reconciliation register that every incoming
+  edge deposits into (`br`/`br_if` at the branch, the then-arm at `else`, the
+  fall-through at `end`), so the frame's result sits in ONE register on every
+  path — i32/i64 through `mov x`, f32/f64 through `fmov d`. The aarch64
+  selector goes **184 → 185 ops**.
+- **The soundness-critical asymmetry is by construction, not by test.** A `br`
+  to a LOOP label targets the header and carries the loop's PARAMETERS, not its
+  results, so a `loop (result T)` back-edge must reconcile NOTHING — the frame
+  carries `label_arity` separately from `result_arity` and branch
+  reconciliation is driven off the former. The natural wrong implementation
+  (reconcile whenever the frame has a result) stamps a garbage value into the
+  result register on every iteration.
+
 - **VCR-DEC-001 increment 4 (VCR-REACH-001, #242) — the graph-colouring
   allocator models the i64 register-PAIR ops.** Increments 2 (joins) and 3
   (calls) both returned *do not flip*, and both for the same reason: the
@@ -295,6 +318,22 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Changed
 
+- **Three named residuals replace two blanket declines.** `br_table` past 16
+  targets (`BR_TABLE_MAX_TARGETS`, the same threshold RV32 uses — the chain is
+  O(n) and PC-relative jump-table dispatch is a follow-up), a `br_table` whose
+  targets are value-carrying (the flat chain has no per-path edge to deposit a
+  result on), and a block type with PARAMETERS or MULTI-VALUE results (the slot
+  is one register). Each loud-declines with a machine reason and is pinned BY
+  NAME in `br_table_subshape_asymmetry_882`, which fails in both directions —
+  partial coverage with named gaps rather than a claim that cannot be backed.
+  The `br_table` whole-op entry is deleted from `aarch64_known_divergences()`;
+  the parity gate's stale-entry check is what forced the deletion.
+- **The #554 float-honesty fixture moves again.** It targeted a value-carrying
+  f32-result `block`; that shape now lowers, so the fixture re-points at a
+  float construct that genuinely still declines — a NON-LEAF function reading
+  an f32 parameter (float params live in `v0..v7`, which a `bl` clobbers, and
+  the encoder has no FP store to home them with).
+
 - **VCR-RA-003's join-availability half now covers the i64-pair family — on the
   DEFAULT build.** It built its CFG from `reg_effect` alone, so every
   i64-containing function returned `NotAttempted`: the interesting half of the
@@ -305,6 +344,30 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
   and self-contained paths, and all 633 pre-existing relocatable functions plus
   all 1059 self-contained ones byte-identical to v0.54.
 
+### Verified
+
+- `scripts/repro/aarch64_brtable_blockvals_851_differential.py` (CI-wired): 88
+  checks over 19 exported functions against wasmtime, under unicorn AND
+  natively on an arm64 host. Per table it walks the index lattice — every arm,
+  the index exactly AT the bound, one OVER it, and `0xFFFFFFFF` (the case a
+  SIGNED compare would mis-dispatch) — plus a table at exactly 16 targets, a
+  `br_table` arm falling into a trap, and both join edges of every
+  value-carrying frame including a value-carrying loop's back-edge. Two cases
+  put a `bl` INSIDE a value-carrying frame — the one soundness claim (a call
+  cannot clobber a live reconciliation slot) that nothing else executes; the
+  harness applies the `R_AARCH64_CALL26` relocations itself, so the emitted
+  relocation is part of what is checked rather than a hang.
+  NON-VACUITY was demonstrated by MUTATION, not asserted: taking the join
+  position before the fall-through's reconciliation move reddens 16 checks, an
+  off-by-one in the chain constants reddens 22, and using `result_arity` where
+  `label_arity` belongs (the loop back-edge bug) makes two functions fail to
+  compile at all.
+- Void control flow is **byte-identical**: 13 of the 14 aarch64 repro fixtures
+  compile to the same object as v0.54.0, and the one that differs
+  (`aarch64_f32_unsupported_554`) differs exactly because its declined function
+  now lowers. A void frame reserves no register and emits no reconciliation
+  move, so the property holds by construction.
+
 ### Notes
 
 - `SYNTH_GRAPH_ALLOC` remains **off by default**; flag-off output is

artifacts/status.json

@@ -1,5 +1,5 @@
 {
-  "aarch64_selector_ops": 184,
+  "aarch64_selector_ops": 185,
   "arm_refinement_assumed_connection": 5,
   "arm_semantics_axioms": 72,
   "backends": [

artifacts/sw-verification.yaml

@@ -669,3 +669,49 @@ artifacts:
             DEFAULT build with 0 hard errors across the corpus (thumb2 AND the
             cortex-r5 A32 path, whose expansions differ)
 
+  - id: SWVER-024
+    type: sw-verification
+    title: AArch64 br_table + value-carrying block/loop/if (#851 — VCR-A64-CF-001)
+    description: >
+      Verifies VCR-A64-CF-001 in both directions. CAPABILITY: an execution
+      differential compiles a WAT carrying the new shapes with `-b aarch64`,
+      reads the emitted `.text` out of the object's symtab, and runs every
+      exported function under unicorn (UC_ARCH_ARM64) — and NATIVELY in a forked
+      child on an arm64 host — against wasmtime as the reference. The cases are
+      chosen so a wrong branch destination changes the RESULT rather than
+      merely the schedule: br_table default arm, index exactly AT the table
+      bound, index OVER the bound, index 0xFFFFFFFF (the unsigned-index rule), a
+      table whose targets mix a backward loop header with forward block ends,
+      and a value-carrying `loop` back-edge (the case where reconciling on the
+      back-edge — the natural wrong implementation — silently returns a garbage
+      result). A guarded `unreachable` gives a TRAP case so the harness cannot
+      collapse to "every case returns a value", and non-vacuity is asserted on
+      both the trap and the value counts.
+      DECLINE-HONESTY: the residuals (>16 targets, value-carrying br_table
+      targets, block/loop params, multi-value results) are asserted by name at
+      selector level in `br_table_subshape_asymmetry_882`, which fails in BOTH
+      directions — a residual that closes must delete its assertion, and a
+      capability that regresses reddens the same test. The whole-op ledger entry
+      for `br_table` is deleted from `aarch64_known_divergences()`; the parity
+      gate's stale-entry check is what forces that deletion.
+      FROZEN-SAFETY: a void frame reserves no register and emits no
+      reconciliation move, so the pre-existing aarch64 control-flow oracles must
+      stay green with unchanged output, and the ARM/RV32 frozen goldens (10/10)
+      are untouched.
+    status: implemented
+    tags: [aarch64, control-flow, br-table, differential, vcr-sel, issue-851]
+    links:
+      - type: verifies
+        target: VCR-A64-CF-001
+    fields:
+      method: automated-test
+      steps:
+        run: "cargo test -p synth-backend-aarch64 && cargo test -p synth-backend-riscv --test cross_backend_op_parity"
+        coverage: >
+          scripts/repro/aarch64_brtable_blockvals_851_differential.py (wasmtime
+          vs unicorn/native execution over the br_table index lattice + the
+          value-carrying block/loop/if shapes, CI-wired) +
+          crates/synth-backend-riscv/tests/cross_backend_op_parity.rs
+          (br_table_subshape_asymmetry_882 — the three aarch64 residuals pinned
+          by name) + crates/synth-backend-aarch64/src/selector.rs unit tests +
+          scripts/repro/aarch64_m2_decline_538.py (decline-matrix honesty)