fix(drv): the cross-arch gate was green because it could not see the defect

.github/workflows/drv-cross-arch.yml

@@ -1,15 +1,21 @@
 # Cross-architecture seam gate for the thin-seam drivers (gale#307 follow-up).
 #
-# The property: a driver "crosses" only if its lowered object keeps gust:hal's
-# mmio calls as UNDEFINED symbols on BOTH ARM and RISC-V. An object with 0
-# undefined symbols has not crossed — it has been silently truncated (the
-# synth#871 shape, where imported calls were dropped rather than relocated).
+# The property: a driver "crosses" only if its lowered object's UNDEFINED symbol
+# set is EXACTLY the set of names its wasm imports. Not "> 0", which a leaked
+# symbol satisfies as well as a real seam symbol, and which fails a correct
+# driver that imports nothing (hm-thin). Not "== 0" either, which is the
+# synth#871 truncation shape. Equality.
 #
-# This was believed red on RISC-V for all 8 drivers. It was not: that reading
-# came from an ambient synth 0.49.0, nine versions behind gale's pin, which
-# skipped 14 of 18 functions. On the pinned toolchain every driver crosses and
-# the gate exits 0. The script now REFUSES to run unpinned rather than answer
-# from whatever is on PATH.
+# On that rule: ARM holds for all 13 drivers. RISC-V holds for NONE of them --
+# synth's RV32 selector declines a function it cannot select, emits the call
+# site anyway, and ships the unlinkable object with exit 0 (synth#1102). The
+# RISC-V leg is therefore carried as an explicit known-defect ledger inside
+# check-cross-arch.py, which FAILS if a driver's status changes in either
+# direction, so the ledger shrinks to empty rather than outliving the bug.
+#
+# An earlier version of this file claimed "on the pinned toolchain every driver
+# crosses and the gate exits 0". That was the `> 0` rule reading a dangling
+# `synth_func_N` as a seam symbol. The script still refuses to run unpinned.
 name: driver cross-arch seam
 
 on:
@@ -19,13 +25,15 @@ on:
       - "benches/gust/drivers/*-thin/**"
       - "benches/gust/drivers/wit/**"
       - "benches/gust/drivers/build-cross-arch.sh"
+      - "benches/gust/drivers/check-cross-arch.py"
       - ".github/workflows/drv-cross-arch.yml"
   pull_request:
     branches: [main]
     paths:
       - "benches/gust/drivers/*-thin/**"
       - "benches/gust/drivers/wit/**"
       - "benches/gust/drivers/build-cross-arch.sh"
+      - "benches/gust/drivers/check-cross-arch.py"
       - ".github/workflows/drv-cross-arch.yml"
 
 permissions:
@@ -48,7 +56,7 @@ jobs:
     # producing NO output at all. gustos-dissolve.yml — the other synth-using
     # workflow — is already on 24.04; this one copied 22.04 from a workflow that
     # does not use synth.
-    name: "seam survives lowering on ARM and RISC-V (8 drivers)"
+    name: "seam survives lowering on ARM and RISC-V (all thin drivers)"
     runs-on: ubuntu-24.04
     steps:
       - uses: actions/checkout@v7
@@ -77,6 +85,13 @@ jobs:
           fetch loom  "$LOOM_VERSION"  loom
           echo "$HOME/pe-toolchain/bin" >> "$GITHUB_PATH"
 
+      - name: Install wasm-tools
+        # check-cross-arch.py derives each driver's EXPECTED undefined set from
+        # the wasm's import section, so it needs wasm-tools -- the old shell gate
+        # only ran nm and did not. Pinned to the same version drv-components.yml
+        # uses, so the two gates read imports through identical tooling.
+        run: cargo install wasm-tools --version 1.245.1 --locked
+
       - name: Install binutils (nm)
         run: sudo apt-get update -qq && sudo apt-get install -y -qq binutils-arm-none-eabi
 
@@ -111,8 +126,13 @@ jobs:
             command -v "$t" >/dev/null && echo "  $t: $(command -v $t)" || echo "  $t: MISSING"
           done
 
+      - name: Negative control — the gate's own rule must reject a leaked symbol
+        run: |
+          cd benches/gust/drivers
+          python3 check-cross-arch.py --self-test
+
       - name: Cross-arch seam gate
         run: |
           cd benches/gust/drivers
-          SYNTH="$HOME/pe-toolchain/bin/synth" LOOM="$HOME/pe-toolchain/bin/loom" \
-            NM=arm-none-eabi-nm bash build-cross-arch.sh
+          SYNTH="$HOME/pe-toolchain/bin/synth" \
+            NM=arm-none-eabi-nm python3 check-cross-arch.py

benches/gust/drivers/CROSS-ARCH.md

@@ -1,40 +1,89 @@
-# Cross-architecture: one wasm, two instruction sets (2026-07-29, synth 0.52.0)
+# Cross-architecture: one wasm, two instruction sets (re-measured 2026-08-28, synth 0.58.0)
 
 The thin-seam drivers are written once, built once to wasm, and lowered to **both** ARM
 Cortex-M and RISC-V RV32 from that same input. This is the "change the tires, not the
 car" claim reduced to something checkable: the driver does not change, the native
 residual under it does.
 
-Reproduce: `bash benches/gust/drivers/build-cross-arch.sh` (needs synth >= 0.52.0).
+## Measured (re-measured 2026-08-28, synth 0.58.0)
 
-## Measured
+Reproduce: `python3 benches/gust/drivers/check-cross-arch.py`.
 
-| driver | ARM cortex-m3 | RISC-V rv32imc |
-|---|---|---|
-| wdg-thin | 6 T, 2 U, 638 B | 5 T, 2 U — 1 of 6 skipped |
-| gpio-thin | 5 T, 2 U, 502 B | 5 T, 2 U — complete |
-| i2c-thin | 7 T, 2 U, 954 B | 6 T, 2 U — 1 of 7 skipped |
-| timer-thin | 5 T, 2 U, 204 B | 5 T, 2 U — complete |
-| adc-thin | 8 T, 2 U, 736 B | 8 T, 2 U — complete |
-| dac-thin | 8 T, 2 U, 642 B | 8 T, 2 U — complete |
-| pwm-thin | 6 T, 1 U, 694 B | 6 T, 1 U — complete |
-| uart-thin | 4 T, 3 U, 254 B | 4 T, 3 U — complete |
+| driver | imports | ARM cortex-m3 | RISC-V rv32imc |
+|---|---|---|---|
+| adc-thin | `read32 write32` | 45 T, 2 U — complete | 26 T, 3 U — 1 of 27 skipped, **1 dangling** |
+| can-thin | `read32 write32` | 34 T, 2 U — complete | 19 T, 3 U — 1 of 20 skipped, **1 dangling** |
+| dac-thin | `read32 write32` | 43 T, 2 U — complete | 24 T, 3 U — 1 of 25 skipped, **1 dangling** |
+| gpio-thin | `read32 write32` | 30 T, 2 U — complete | 17 T, 3 U — 1 of 18 skipped, **1 dangling** |
+| hm-thin | `(none)` | 19 T, 0 U — complete | 12 T, 1 U — 1 of 13 skipped, **1 dangling** |
+| i2c-thin | `read32 write32` | 38 T, 2 U — complete | 21 T, 3 U — 1 of 22 skipped, **1 dangling** |
+| mpu-thin | `mpu-write` | 27 T, 1 U — complete | **no object** — synth exits non-zero (#952) |
+| pwm-thin | `write32` | 36 T, 1 U — complete | 21 T, 2 U — 1 of 22 skipped, **1 dangling** |
+| spi-thin | `read32 write32` | 34 T, 2 U — complete | 19 T, 3 U — 1 of 20 skipped, **1 dangling** |
+| switch-thin | `ctx-resume ctx-save region-swap` | 41 T, 3 U — complete | 17 T, 10 U — 13 of 30 skipped, **10 dangling** |
+| timer-thin | `read32 write32` | 30 T, 2 U — complete | 17 T, 3 U — 1 of 18 skipped, **1 dangling** |
+| uart-thin | `poll read32 write32` | 27 T, 3 U — complete | 16 T, 4 U — 1 of 17 skipped, **1 dangling** |
+| wdg-thin | `read32 write32` | 35 T, 2 U — complete | 20 T, 3 U — 1 of 21 skipped, **1 dangling** |
 
-Six of eight drivers lower **completely** on both targets, with the same number of
-defined functions and the same seam width on each. Deterministic: repeated runs are
-byte-identical.
+**ARM: 13 of 13 lower completely**, and each object's undefined set is *exactly* the
+set of names its wasm imports — no leak, no truncation. That half of the claim holds.
 
-## Why the undefined-symbol count is the gate, not the byte count
+**RISC-V: 0 of 13.** Twelve emit an object that cannot be linked, because synth's RV32
+selector skips a function it cannot select and emits the call site anyway, leaving a
+dangling `synth_func_N`. The thirteenth (`mpu-thin`) emits nothing at all. This is not
+new and is not a regression: synth 0.52.0 — the version the previous version of this
+table cited — produces byte-for-byte the same result on today's sources, as does
+0.60.0, the latest release. `ld.lld` refuses the objects outright:
 
-`build-cross-arch.sh` fails if either object has **zero** undefined symbols. That is not
-a stylistic preference — it is the failure mode this whole approach has to detect. Under
-synth 0.49 the RISC-V backend silently dropped every function containing an imported
-call, so `wdg-thin` emitted a 468 B object with 2 defined functions and *no* undefined
-symbols. It looked like a smaller, cleaner result. It was a truncated one. An object
-whose `gust:hal` calls have vanished has not been ported; it has been hollowed out.
+```
+ld.lld: error: undefined symbol: synth_func_18
+>>> referenced by out.o:(gust:hal/gpio@0.1.0#set)
+```
 
-So the invariant is: the mmio imports must still be there, unresolved, on every target.
-That is what makes the native layer swappable while the wasm stays put.
+Filed upstream as **synth#1102**.
+
+## What the previous table said, and why it was wrong
+
+It reported eight drivers, six of them "complete" on both targets, gpio-thin at
+"5 T, 2 U — complete". That was measured before these drivers were componentized
+(`wdg-thin` had 6 functions then; it has 21 now), so it describes sources that no
+longer exist. It was not re-measured when the sources changed.
+
+Two mechanisms kept it from being caught:
+
+1. **The gate enumerated its drivers by hand.** `build-cross-arch.sh` carried
+   `DRIVERS=(wdg-thin gpio-thin i2c-thin timer-thin adc-thin dac-thin pwm-thin
+   uart-thin)` — eight names, while thirteen `*-thin` directories exist. can, hm,
+   mpu, spi and switch were never gated.
+2. **The rule was `undefined_count > 0`.** See below.
+
+## Why `> 0` was the wrong rule
+
+The old gate failed an object with **zero** undefined symbols, on the reasoning that
+a vanished seam means a truncated object (the synth 0.49 shape, where the RISC-V
+backend dropped every function containing an imported call).
+
+That reasoning is right about the failure it names and blind to its neighbour. `> 0`
+is satisfied by *any* undefined symbol — including a leaked one. Every RISC-V object
+above carries a dangling `synth_func_N`, so every one of them counted as passing. The
+gate was green because the objects were broken in a way it could not distinguish from
+being correct.
+
+`hm-thin` shows the other edge: it imports nothing, so a correct object has **zero**
+undefined symbols. Under `> 0` a correct driver fails.
+
+The rule is therefore neither `> 0` nor `== 0` but **equality**:
+
+> the lowered object's undefined set must equal the set of names the wasm imports.
+
+That is what `check-cross-arch.py` gates, and it is the same rule
+`check-driver-components.py` already applies on its object axis. It is correct for a
+driver importing nothing, for a driver whose seam is not `gust:hal` (`mpu-thin`,
+`switch-thin`), and it rejects a leak, which `> 0` cannot.
+
+The RISC-V leg is carried as an explicit known-defect ledger in that script rather
+than skipped: if a driver starts crossing cleanly the gate **fails** until it is
+removed from the ledger, so the list shrinks to empty instead of outliving the bug.
 
 ## Honest boundary
 

benches/gust/drivers/build-cross-arch.sh

@@ -1,4 +1,11 @@
 #!/usr/bin/env bash
+# SUPERSEDED AS A GATE by `check-cross-arch.py`. This script remains as a loud
+# reporting tool (it prints byte sizes, which the gate does not) and as the
+# subject of the workflow's pin-guard negative control. Its VERDICT was wrong
+# twice over -- it enumerated 8 of 13 drivers by hand, and its rule was
+# `undefined_count > 0`, which a leaked `synth_func_N` satisfies just as well
+# as a real seam symbol. See CROSS-ARCH.md. Do not gate on this file.
+#
 # Cross-architecture matrix for the thin-seam drivers: one wasm per driver, lowered to
 # BOTH ARM Cortex-M and RISC-V RV32, reporting the symbol shape of each object.
 #
@@ -41,7 +48,11 @@ echo "gate toolchain: synth $synth_ver"
 NM="${NM:-nm}"
 ARM_SIZE="${ARM_SIZE:-arm-none-eabi-size}"
 
-DRIVERS=(wdg-thin gpio-thin i2c-thin timer-thin adc-thin dac-thin pwm-thin uart-thin)
+# Discovered, not enumerated. The hand-written list this replaced named 8 of the
+# 13 drivers that exist, and silently skipped every one added after it was written.
+DRIVERS=()
+for _d in "$HERE"/*-thin; do [ -d "$_d" ] && DRIVERS+=("$(basename "$_d")"); done
+[ "${#DRIVERS[@]}" -gt 0 ] || { echo "FATAL: no *-thin drivers found" >&2; exit 2; }
 
 printf '%-12s | %-22s | %-22s\n' "driver" "ARM cortex-m3" "RISC-V rv32imc"
 printf '%-12s-+-%-22s-+-%-22s\n' "------------" "----------------------" "----------------------"