RV32 br_table lowering + hard-error on target/backend ISA mismatch (#882)

.github/workflows/ci.yml

@@ -1020,6 +1020,44 @@ jobs:
           SYNTH: ./target/debug/synth
         run: python scripts/repro/const_addr_fold_riscv_differential.py
 
+  rv32-br-table-oracle:
+    name: rv32 br_table execution oracle (#882)
+    # #882: RV32 lowers `br_table` as a compare-and-branch chain (entry 0 vs
+    # x0, li+beq per further entry, jal to default) — the last op standing
+    # between gale's wdg-thin driver and a complete RV32 lowering. The
+    # differential EXECUTES gale's exact shape (targets [0,1,0] default 1) plus
+    # 3-distinct-target and default-distinct dispatches under unicorn
+    # (UC_ARCH_RISCV) vs wasmtime, with indices covering EVERY table entry AND
+    # out-of-range/unsigned-edge (0x80000000, 0xFFFFFFFF must land on default —
+    # a wrong default or a signed chain compare is loud). A missing export
+    # (the pre-fix decline) fails the vacuity guard, so this can never pass
+    # vacuously. Isolated job: emulation deps pip-installed here ONLY.
+    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: Build synth
+        run: cargo build -p synth-cli
+      - uses: actions/setup-python@v7
+        with:
+          python-version: "3.x"
+      - name: Install emulation deps
+        run: pip install wasmtime unicorn pyelftools
+      - name: Run RV32 br_table execution oracle
+        env:
+          SYNTH: ./target/debug/synth
+        run: python scripts/repro/rv32_br_table_882_differential.py
+
   rv32-extern-call-reloc-oracle:
     name: rv32 external-call relocation oracle (#871)
     # #871: the gale thin-seam driver shape — exported functions calling an

CHANGELOG.md

@@ -7,8 +7,36 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+### Added
+
+- **RV32 `br_table` lowering (#882)** — the RISC-V selector now lowers
+  `br_table` as a compare-and-branch chain (entry 0 against `x0`, `li`+`beq`
+  per further entry, `jal` to the default), closing the last op gap on gale's
+  `wdg-thin` driver (`wdg_unlock`, `targets: [0, 1, 0], default: 1`). Any index
+  `>= targets.len()` — including "negative" i32s under the unsigned
+  interpretation — lands on the default label, per WASM core semantics. Tables
+  past 16 targets LOUD-DECLINE by name (`BrTableTooLarge`; the jump-table
+  upgrade is a named follow-up), and value-carrying `br_table` (the #509
+  block-arity-threading class) LOUD-DECLINES (`BrTableValueCarrying`) instead
+  of silently miscompiling path-dependent result registers. Execution-verified
+  under unicorn RV32 vs wasmtime across every table entry AND out-of-range /
+  unsigned-edge indices (`scripts/repro/rv32_br_table_882_differential.py`,
+  CI job `rv32-br-table-oracle`, vacuity-guarded against skipped exports).
+
 ### Fixed
 
+- **`--target`/backend ISA mismatch is now a hard error (#882).** `synth
+  compile --target riscv32` without `-b riscv` silently printed
+  `Using backend: arm` and built Thumb code into a RISC-V ELF container,
+  failing only deep in the emitter ("non-CALL_PLT relocation ThmCall reached
+  the RISC-V ELF emitter") — a plausible-looking wrong-ISA object. A
+  recognised `--target` whose ISA family does not match the selected
+  single-ISA backend (arm / riscv / aarch64) now exits non-zero naming the
+  right `-b`; an explicit mismatched `-b` lists the targets it accepts; and an
+  unknown `--target` names the full valid set (now including cortex-m55,
+  cortex-r5, cortex-a53 and riscv32). No behavior change for good input —
+  every valid target/backend pairing resolves exactly as before (gated by
+  `crates/synth-cli/tests/unknown_target_882.rs`).
 - **The gpio-thin gate is now a gate (#879).** `gpio_thin_846_differential.py`
   — the check behind the v0.50.1 (534→506 B) and v0.52.0 (506→502 B) headline
   size claims, and the only harness that executes gale's real driver across a