test(vcr-sel-005): universe-complete cross-backend op-parity gate — surface 16 silent ARM/RV32 op-gaps (#242, #223, #232)

.github/workflows/ci.yml

@@ -1671,3 +1671,39 @@ jobs:
         run: cargo test -p synth-synthesis --lib ra003_
       - name: Silent-on-real-codegen (frozen suite through the unconditional gate)
         run: cargo test -p synth-cli --test frozen_codegen_bytes
+
+  vcr-sel-005-cross-backend-op-parity-gate:
+    name: "VCR-SEL-005 cross-backend op-parity (universe-complete + red-first)"
+    # VCR-SEL-005 (#242, #223, #232): the "selector missed an op" class was never
+    # a silent miscompile — it was a silent cross-backend DIVERGENCE: ARM lowered
+    # an op RV32 loud-declined, so a function compiled on Cortex-M but was skipped
+    # on RISC-V and nothing caught it until gale ran it on qemu. This gate makes
+    # the divergence visible: for every WasmOp variant (a no-wildcard match — a
+    # new op fails to compile until classified, so the universe is
+    # compiler-enforced complete), the integer core is probed on BOTH the ARM
+    # (select_with_stack) and RV32 selectors and must be at parity — both lower,
+    # both decline, OR a ledgered one-sided divergence with a written reason. A
+    # NEW un-ledgered one-sided gap FAILS the gate; a ledgered gap that has CLOSED
+    # FAILS as stale. Float/f64/SIMD are StructurallyExcluded (their ARM lowering
+    # is target-parameterized), tracked as separate parity gaps.
+    #   RED-FIRST non-vacuity: red_first_unledgered_one_sided_gap_is_caught drops
+    #   the real i32.rotl ledger entry and asserts the gate reports it as an
+    #   unexpected divergence on the REAL backends — proving it detects a genuine
+    #   one-sided op-gap, not a synthetic one, with no shipping-code change.
+    # Test-only: emits nothing (.text byte-identical; frozen 10/10 unaffected).
+    runs-on: ubuntu-latest
+    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: Universe-complete parity + red-first + ledger-liveness
+        run: cargo test -p synth-backend-riscv --test cross_backend_op_parity

artifacts/verified-codegen-roadmap.yaml

@@ -559,6 +559,39 @@ artifacts:
       deferral is closable by routing i32 rotate through the same shift+or sequence
       the i64 path already uses (sharpens the FOLLOW-UP's first target; byte-changing
       codegen, gated — NOT in this test-only increment).
+
+      UNIVERSE-COMPLETENESS UPGRADE (2026-07-17, #49, frozen-safe test-only): the
+      oracle was hardened from a CURATED integer probe list (whose vacuity trap is
+      that a new WasmOp variant is silently never probed) to a COMPILER-ENFORCED
+      universe-complete gate. Every WasmOp variant is now assigned a ParityClass by
+      a NO-WILDCARD match (classify()); a new op fails to COMPILE until classified
+      (the #615 no-wildcard tripwire). Integer-core ops carry a probe and are
+      asserted; float/f64/SIMD are StructurallyExcluded with a written reason —
+      their ARM lowering is TARGET-PARAMETERIZED (measured: f32.add DECLINES with
+      fpu=None, LOWERS with FPUPrecision::Single/Double; f64.add needs Double), so
+      asserting "ARM lowers float" at a fixed no-FPU probe would be FALSE; float/SIMD
+      parity stays a separately-tracked gap. Enumerating the FULL universe surfaced
+      SIXTEEN previously-unprobed ARM-lowers / RV32-loud-declines one-sided gaps
+      (each confirmed END-TO-END via `synth compile -b riscv`, "unsupported wasm op
+      for RV32 skeleton: …"): global.get, global.set, memory.size, memory.grow,
+      memory.copy, memory.fill, br_table, and the nine sub-word i64 loads/stores
+      (i64.load8_s/u, i64.load16_s/u, i64.load32_s/u, i64.store8/16/32 — the
+      full-word i64.load/i64.store DO lower on both; only the sub-word extend/
+      truncate variants are the gap). All sixteen are now ledgered VCR-SEL-005
+      RV32-selector DEFERRALS (a gated, owned fact instead of a silicon surprise) —
+      the KNOWN_DIVERGENCES ledger is now 5 Zbb + 16 new = 21 entries. RED-FIRST
+      non-vacuity is now a first-class companion test
+      (red_first_unledgered_one_sided_gap_is_caught): it drops the real i32.rotl
+      ledger entry and asserts the gate reports it as an unexpected divergence on
+      the REAL backends (no synthetic op, no shipping-code change). A
+      ledger-liveness test guards drift. The gate is now WIRED as a named CI job
+      (vcr-sel-005-cross-backend-op-parity-gate) so a regression is visible on its
+      own failing check.
+
+      FOLLOW-UP EXPANDED: the RV32 sequence-lowering backlog this oracle drives now
+      also covers globals, the memory intrinsics (size/grow/copy/fill), br_table,
+      and the sub-word i64 memory variants — each landing retires its ledger line
+      via the stale-entry check.
     status: implemented
     tags: [codegen, selector, riscv, parity, oracle, track-a, release-v0.11.51]
     links:
@@ -570,10 +603,15 @@ artifacts:
       req-type: functional
       priority: should
       verification-criteria: >
-        cross_backend_integer_op_parity_242 is green: every integer-core probe is
-        at ARM/RV32 parity OR carries a reasoned KNOWN_DIVERGENCES entry, with the
-        at-parity floor (>=30 common-core ops) guarding against a construction
-        regression that would let "everything errors" masquerade as parity.
+        cross_backend_integer_op_parity_242 is green: every WasmOp variant is
+        classified by a no-wildcard match (universe-complete by construction), and
+        every integer-core probe is at ARM/RV32 parity OR carries a reasoned
+        KNOWN_DIVERGENCES entry, with the at-parity floor (>=65 common-core ops)
+        guarding against a construction regression that would let "everything
+        errors" masquerade as parity. The red-first companion
+        (red_first_unledgered_one_sided_gap_is_caught) proves non-vacuity by
+        surfacing the real i32.rotl gap once its ledger entry is removed, and the
+        gate is CI-wired as vcr-sel-005-cross-backend-op-parity-gate.
 
   # ---------------------------------------------------------------------------
   # Track B — authoritative semantics (independent; parallel with Track A)