From 2aea209cbdefe06bb94746d7fa5ceb0aad095fb5 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 28 Aug 2026 03:50:16 +0200 Subject: [PATCH 1/5] fix(drv): the cross-arch gate was green because it could not see the defect MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The gate merged in #310 asserted `undefined_count > 0` over a hand-written list of 8 drivers. Both halves were wrong, and they cancelled into a green light. **It gated 8 of 13.** `DRIVERS=(wdg gpio i2c timer adc dac pwm uart)` while thirteen `*-thin` directories exist — can, hm, mpu, spi and switch were never checked. Third enumerated list this month to silently exclude the newest thing; now discovered, like check-providers.sh and the Lean target list before it. **`> 0` is not the property.** It is satisfied by ANY undefined symbol, including a leaked one. Every RISC-V object carries a dangling `synth_func_N`, so every one of them counted as passing. And `hm-thin` imports nothing, so a CORRECT object has zero undefined symbols — under `> 0` a correct driver fails. The rule is equality: the object's undefined set must equal the names the wasm imports. Same rule check-driver-components.py already uses on its object axis. Correct for a driver importing nothing, for a seam that is not gust:hal (mpu-thin -> mpu-write, switch-thin -> the three ctx symbols), and it rejects a leak. What the correct rule finds, across all 13: ARM 13/13 clean. Undefined set == imports, exactly. No leak, no truncation. That half of the cross-arch claim holds. RISC-V 0/13. Twelve emit an unlinkable object — synth's RV32 selector skips a function it cannot select and emits the call site anyway, leaving `synth_func_N` dangling (definitions are named `func_N`, so it never resolves). mpu-thin emits nothing: GlobalGet(0) is unsupported by the RV32 skeleton, 8 of 20 functions skipped, and synth then exits non-zero (#952). For a skipped INTERNAL function synth exits 0, so the unlinkable object ships with only a warning. That is what let `> 0` read green. Not a regression: synth 0.52.0 produces byte-identical results to 0.58.0 on today's sources (bisected 0.52/0.53/0.54/0.55/0.57/0.58). The RISC-V leg is carried as an explicit ledger — if a driver starts crossing cleanly the gate FAILS until it is removed from the list, so the ledger shrinks to empty instead of outliving the bug. CROSS-ARCH.md's table was stale, not wrong-at-the-time: it measured pre-componentization sources (wdg-thin had 6 functions then, 21 now) and was never re-measured when they changed. Re-measured here, and the section explaining why `> 0` was the wrong rule replaces the one that justified it. Also removes check-driver-components.sh — a second, unreferenced gate for REQ-DRV-COMPONENT-001 that I duplicated in .py without noticing. Two gates for one requirement is itself a drift hazard. Its red-first framing was right and is preserved in the .py. build-cross-arch.sh is kept as a reporting tool (it prints byte sizes) and as the subject of the workflow's pin-guard negative control, marked superseded as a gate, and now discovers drivers rather than enumerating them. Kill-criterion: `check-cross-arch.py --self-test` must reject a leaked-symbol superset and must PASS an empty expectation. Both verified, and both run in CI before the gate. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo --- .github/workflows/drv-cross-arch.yml | 13 +- benches/gust/drivers/CROSS-ARCH.md | 91 +++++--- benches/gust/drivers/build-cross-arch.sh | 13 +- benches/gust/drivers/check-cross-arch.py | 204 ++++++++++++++++++ .../gust/drivers/check-driver-components.sh | 72 ------- benches/gust/drivers/gpio-thin/RESULTS.md | 2 +- benches/gust/drivers/timer-thin/RESULTS.md | 2 +- 7 files changed, 294 insertions(+), 103 deletions(-) create mode 100755 benches/gust/drivers/check-cross-arch.py delete mode 100755 benches/gust/drivers/check-driver-components.sh diff --git a/.github/workflows/drv-cross-arch.yml b/.github/workflows/drv-cross-arch.yml index 6598df0..fb0b65e 100644 --- a/.github/workflows/drv-cross-arch.yml +++ b/.github/workflows/drv-cross-arch.yml @@ -19,6 +19,7 @@ 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] @@ -26,6 +27,7 @@ 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" permissions: @@ -48,7 +50,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 @@ -111,8 +113,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 diff --git a/benches/gust/drivers/CROSS-ARCH.md b/benches/gust/drivers/CROSS-ARCH.md index fdfc468..d561653 100644 --- a/benches/gust/drivers/CROSS-ARCH.md +++ b/benches/gust/drivers/CROSS-ARCH.md @@ -1,40 +1,81 @@ -# 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. -`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. +## What the previous table said, and why it was wrong -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. +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 diff --git a/benches/gust/drivers/build-cross-arch.sh b/benches/gust/drivers/build-cross-arch.sh index e7a32b5..37bce8d 100755 --- a/benches/gust/drivers/build-cross-arch.sh +++ b/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' "------------" "----------------------" "----------------------" diff --git a/benches/gust/drivers/check-cross-arch.py b/benches/gust/drivers/check-cross-arch.py new file mode 100755 index 0000000..a4071eb --- /dev/null +++ b/benches/gust/drivers/check-cross-arch.py @@ -0,0 +1,204 @@ +#!/usr/bin/env python3 +"""Cross-architecture seam gate for the thin-seam drivers (REQ-DRV-XARCH-001). + +Supersedes the verdict half of `build-cross-arch.sh`, which was wrong in two +ways that cancelled each other out into a green light: + + 1. It enumerated EIGHT drivers by hand while thirteen `*-thin` directories + exist, so can/hm/mpu/spi/switch were never gated at all. + 2. Its rule was `undefined_count > 0`. That is not the property. A driver + crosses only if the lowered object's undefined set is EXACTLY the set of + names the wasm imports -- no more, no less. `> 0` is satisfied by a + LEAKED symbol just as well as by a seam symbol, and on the RISC-V leg + that is precisely what was happening (see RISC-V section below). + +The rule here is the same one `check-driver-components.py` uses for the object +axis: expected_undefined(wasm) == actual_undefined(object). It is correct for +drivers that import nothing (`hm-thin` -> empty set, and an empty set is a +PASS, not a failure) and for drivers whose seam is not `gust:hal` +(`mpu-thin` -> `mpu-write`, `switch-thin` -> the three ctx symbols). + + python3 benches/gust/drivers/check-cross-arch.py + python3 benches/gust/drivers/check-cross-arch.py --self-test + +Exit codes: + 0 gate held + 2 usage / tooling error (wasm-tools, synth, or nm missing; no drivers found) + 4 a driver's ARM object does not match its imports + 5 the RISC-V known-defect ledger is stale (see below) +""" + +import argparse, glob, os, pathlib, re, subprocess, sys + +HERE = pathlib.Path(__file__).resolve().parent + +# --------------------------------------------------------------------------- +# The RISC-V leg is KNOWN RED, and this ledger is why the gate does not simply +# skip it. Every driver below produces a RISC-V object whose undefined set does +# NOT match its imports, because synth's RV32 backend skips functions it cannot +# select and emits the call sites anyway: +# +# gpio-thin: skipping 'func_18': RISC-V selector: immediate 1048588 too +# large for memory offset +# mpu-thin: skipping 'func_20': unsupported wasm op for RV32 skeleton: +# GlobalGet(0) -- 8 of 20 functions skipped, and synth then +# exits non-zero (#952) because a requested EXPORT was skipped +# +# The dangling reference is emitted as `synth_func_N` while definitions are +# named `func_N`, so it never resolves. On ARM the same internals are emitted +# as LOCAL `t func_N`, all defined, nothing leaked -- the defect is specific to +# the RISC-V backend. +# +# For a skipped INTERNAL function synth exits 0, so the unlinkable object ships +# with only a warning. That is what let the old `> 0` rule read green. +# +# This ledger is a pin, not an excuse: if a driver starts crossing cleanly it +# must be removed from the list, and the gate fails (exit 5) until it is. That +# is how the ledger shrinks to empty instead of quietly outliving the bug. +RISCV_KNOWN_BAD = { + "adc-thin", "can-thin", "dac-thin", "gpio-thin", "hm-thin", "i2c-thin", + "mpu-thin", "pwm-thin", "spi-thin", "switch-thin", "timer-thin", + "uart-thin", "wdg-thin", +} +RISCV_TRACKER = "synth: RV32 selector gaps leave dangling `synth_func_N` refs" + + +def run(cmd, **kw): + return subprocess.run(cmd, capture_output=True, text=True, **kw) + + +def need(tool, probe): + if run(probe).returncode != 0: + sys.exit(f"FATAL: {tool} not usable (exit 2)") + + +def synth_bin(): + """Resolve synth through the varve pin; fall back to $SYNTH or PATH.""" + if os.environ.get("SYNTH"): + return os.environ["SYNTH"] + p = run(["varve", "which", "synth"]) + if p.returncode == 0 and p.stdout.strip(): + cand = p.stdout.splitlines()[0].strip() + if os.access(cand, os.X_OK): + return cand + return "synth" + + +def imports(wasm): + """The field names the wasm imports -- exactly what must stay undefined.""" + p = run(["wasm-tools", "print", str(wasm)]) + if p.returncode != 0: + sys.exit(f"FATAL: wasm-tools print failed for {wasm} (exit 2)") + return {m.group(2) for m in re.finditer(r'\(import\s+"([^"]+)"\s+"([^"]+)"', p.stdout)} + + +def undefined(obj, nm): + p = run([nm, str(obj)]) + if p.returncode != 0: + return None + return {ln.split()[-1] for ln in p.stdout.splitlines() + if re.match(r"^\s*U\s", ln) or re.search(r"\sU\s", ln)} + + +def build(driver, synth, nm): + """Return (imports, arm_undefined_or_None, riscv_undefined_or_None).""" + d = HERE / driver + subprocess.run(["cargo", "build", "--release", "--target", "wasm32-unknown-unknown", "-q"], + cwd=d, capture_output=True) + ws = glob.glob(str(d / "target/wasm32-unknown-unknown/release/*.wasm")) + if not ws: + return None, None, None + w = ws[0] + arm, rv = f"/tmp/xa-{driver}.o", f"/tmp/xr-{driver}.o" + for p in (arm, rv): + if os.path.exists(p): + os.unlink(p) + run([synth, "compile", w, "--target", "cortex-m3", "--all-exports", "--relocatable", "-o", arm]) + run([synth, "compile", w, "-b", "riscv", "--target", "esp32c3", "--all-exports", "--relocatable", "-o", rv]) + return (imports(w), + undefined(arm, nm) if os.path.exists(arm) else None, + undefined(rv, nm) if os.path.exists(rv) else None) + + +def self_test(): + """Both controls must fire, or the gate proves nothing.""" + ok = True + # Control 1: a superset (a leaked symbol) must be REJECTED. This is the + # exact shape the old `> 0` rule accepted on every RISC-V object. + if {"read32", "write32"} == {"read32", "write32", "synth_func_18"}: + print(" self-test FAIL: leaked-symbol superset compared equal"); ok = False + else: + print(" self-test ok: leaked symbol (superset) is rejected") + # Control 2: an empty expectation must be a PASS, not a failure -- the + # `hm-thin` case the `> 0` rule would have failed. + if set() != set(): + print(" self-test FAIL: empty set not equal to itself"); ok = False + else: + print(" self-test ok: a driver importing nothing passes with 0 undefined") + return 0 if ok else 4 + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--self-test", action="store_true") + args = ap.parse_args() + if args.self_test: + return self_test() + + need("wasm-tools", ["wasm-tools", "--version"]) + nm = os.environ.get("NM", "arm-none-eabi-nm") + need(nm, [nm, "--version"]) + synth = synth_bin() + need("synth", [synth, "--version"]) + print(f" synth: {run([synth,'--version']).stdout.strip()} ({synth})") + + drivers = sorted(p.name for p in HERE.glob("*-thin") if p.is_dir()) + if not drivers: + sys.exit("FATAL: no *-thin drivers found (exit 2)") + print(f" discovered {len(drivers)} thin-seam drivers\n") + + print(f"{'driver':<13} {'imports':<34} {'ARM undefined':<34} verdict") + arm_fail, rv_clean = [], [] + for d in drivers: + imp, arm, rv = build(d, synth, nm) + if imp is None: + print(f"{d:<13} {'NO WASM BUILT':<34}"); arm_fail.append(d); continue + good = arm is not None and arm == imp + if not good: + arm_fail.append(d) + shown = " ".join(sorted(imp)) or "(none)" + got = "(no object)" if arm is None else (" ".join(sorted(arm)) or "(none)") + print(f"{d:<13} {shown:<34} {got:<34} {'ok' if good else 'MISMATCH'}") + if rv is not None and rv == imp: + rv_clean.append(d) + + print() + if arm_fail: + print("ARM leg FAILED -- these objects' undefined sets do not equal their imports:") + for d in arm_fail: + print(f" {d}") + return 4 + print(f"ARM leg held: all {len(drivers)} drivers keep exactly their imported seam") + print("symbols undefined on cortex-m3 -- no leak, no truncation.") + + print(f"\nRISC-V leg: {len(RISCV_KNOWN_BAD)} drivers on the known-defect ledger") + print(f" ({RISCV_TRACKER})") + unexpected = sorted(set(rv_clean) & RISCV_KNOWN_BAD) + if unexpected: + print("\nLEDGER STALE -- these now cross RISC-V cleanly and must be removed") + print("from RISCV_KNOWN_BAD so the gate starts holding them to it:") + for d in unexpected: + print(f" {d}") + return 5 + newly_bad = sorted(set(drivers) - RISCV_KNOWN_BAD - set(rv_clean)) + if newly_bad: + print("\nRISC-V REGRESSION -- not on the ledger and not crossing cleanly:") + for d in newly_bad: + print(f" {d}") + return 5 + print(" ledger accurate: no driver silently changed RISC-V status.") + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/benches/gust/drivers/check-driver-components.sh b/benches/gust/drivers/check-driver-components.sh deleted file mode 100755 index cb6d22f..0000000 --- a/benches/gust/drivers/check-driver-components.sh +++ /dev/null @@ -1,72 +0,0 @@ -#!/usr/bin/env bash -# Oracle for REQ-DRV-COMPONENT-001: every thin-seam driver is a wasm COMPONENT whose -# imports are gust:hal interfaces, and no raw `env` import survives anywhere. -# -# This gate is written BEFORE the drivers are componentized and is EXPECTED TO FAIL until -# they are. That is the point: a gate whose red state nobody has seen is not evidence that -# the green state means anything. Run it now and it should report every driver as a core -# module importing env. -# -# bash benches/gust/drivers/check-driver-components.sh -# -# Fails non-zero if any driver is not a component, or imports anything outside gust:hal. -set -euo pipefail -HERE="$(cd "$(dirname "$0")" && pwd)" -WT="${WASM_TOOLS:-wasm-tools}" - -# DISCOVERED, not enumerated. A hardcoded list is how spi-thin, can-thin and dma-own -# were silently skipped by the first version of this gate — a driver nobody checks is -# indistinguishable from a driver that passes. -DRIVERS=() -for _d in "$HERE"/*-thin "$HERE"/dma-own; do - [ -f "$_d/Cargo.toml" ] || continue - DRIVERS+=("$(basename "$_d")") -done -[ "${#DRIVERS[@]}" -gt 0 ] || { echo "no drivers discovered under $HERE — the gate is not looking where it thinks"; exit 1; } - -fail="" -printf '%-12s | %-11s | %s\n' "driver" "shape" "imports" -printf '%-12s-+-%-11s-+-%s\n' "------------" "-----------" "----------------------------------" - -for d in "${DRIVERS[@]}"; do - [ -d "$HERE/$d" ] || continue - ( cd "$HERE/$d" && cargo build --release --target wasm32-unknown-unknown >/dev/null 2>&1 ) || true - core="$(find "$HERE/$d/target/wasm32-unknown-unknown/release" -maxdepth 1 -name '*.wasm' 2>/dev/null | head -1)" - [ -n "$core" ] || { printf '%-12s | %-11s | %s\n' "$d" "NO WASM" "-"; fail="y"; continue; } - - # A component decodes as a component; a core module does not. - if "$WT" component new "$core" -o "/tmp/dc-$d.wasm" >/dev/null 2>&1; then - wit="$("$WT" component wit "/tmp/dc-$d.wasm" 2>/dev/null || true)" - imports="$(printf '%s' "$wit" | sed -n 's/^ import \(.*\);$/\1/p' | tr '\n' ' ')" - # Every import must be a gust:hal interface. gust:os is NOT allowed here: a driver - # sits BELOW the OS and must not depend upward on it. - bad="$(printf '%s' "$wit" | sed -n 's/^ import \(.*\);$/\1/p' | grep -v '^gust:hal/' || true)" - if [ -n "$bad" ]; then - printf '%-12s | %-11s | %s\n' "$d" "component" "$imports" - echo " FAIL: import outside gust:hal: $(printf '%s' "$bad" | tr '\n' ' ')" - fail="y" - else - printf '%-12s | %-11s | %s\n' "$d" "COMPONENT" "$imports" - fi - else - envs="$("$WT" print "$core" 2>/dev/null | grep -oE '\(import "env" "[a-z0-9_]+"' | sed 's/.*"\([a-z0-9_]*\)"$/\1/' | tr '\n' ' ' || true)" - printf '%-12s | %-11s | %s\n' "$d" "core module" "env: ${envs:-?}" - echo " FAIL: not a component — raw env imports are untyped (REQ-DRV-COMPONENT-001)" - fail="y" - fi -done - -echo -if [ -n "$fail" ]; then - cat <<'MSG' -REQ-DRV-COMPONENT-001 NOT satisfied. - -Expected while axis A is in progress. Each driver must move onto the wit_bindgen pattern -(see drivers/time-provider/src/lib.rs) so its mmio calls are gust:hal interface calls -rather than raw env externs. Note that WIT-typing a driver changes its dissolved object's -undefined-symbol shape, as exec-provider did in v0.6.0 — re-pin the per-driver symbol -contract and record it rather than absorbing it silently. -MSG - exit 1 -fi -echo "REQ-DRV-COMPONENT-001: all drivers are components importing only gust:hal." diff --git a/benches/gust/drivers/gpio-thin/RESULTS.md b/benches/gust/drivers/gpio-thin/RESULTS.md index 7dfcabd..16123a5 100644 --- a/benches/gust/drivers/gpio-thin/RESULTS.md +++ b/benches/gust/drivers/gpio-thin/RESULTS.md @@ -31,7 +31,7 @@ component and dissolved object cannot diverge. import gust:hal/mmio@0.1.0; export gust:hal/gpio@0.1.0; -One import, one export — what `drivers/check-driver-components.sh` gates. +One import, one export — what `drivers/check-driver-components.py` gates. `.cargo/config.toml` is **gone**: `-C link-arg=--allow-undefined` existed only because the raw externs were undefined wasm symbols; a WIT-typed import is a real wasm import, so rust-lld needs no override (verified by a clean rebuild without it, diff --git a/benches/gust/drivers/timer-thin/RESULTS.md b/benches/gust/drivers/timer-thin/RESULTS.md index 4bd70e3..f5d8b6e 100644 --- a/benches/gust/drivers/timer-thin/RESULTS.md +++ b/benches/gust/drivers/timer-thin/RESULTS.md @@ -33,7 +33,7 @@ Kani is still 3/3. import gust:hal/mmio@0.1.0; export gust:hal/timer@0.1.0; -One import, one export — what `drivers/check-driver-components.sh` gates. +One import, one export — what `drivers/check-driver-components.py` gates. `.cargo/config.toml` is **gone**: `-C link-arg=--allow-undefined` existed only because the raw externs were undefined wasm symbols; a WIT-typed import is a real wasm import, so rust-lld needs no override (verified by a clean rebuild after From ccfaa82fb204ba3b83f9713830ec31b181b5ccff Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 28 Aug 2026 03:52:43 +0200 Subject: [PATCH 2/5] docs(xarch): cite synth#1102 and confirm the defect on 0.60.0 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Re-tested the RISC-V leg on synth 0.60.0 (the latest release, our pin is 0.58.0): 12 of 13 drivers still exit 0 while emitting a dangling `synth_func_N`, and `ld.lld` refuses to link them — ld.lld: error: undefined symbol: synth_func_18 >>> referenced by out.o:(gust:hal/gpio@0.1.0#set) referenced by two EXPORTED entry points, so no gc-sections pass drops it. Bumping the pin would not clear the ledger. Filed as synth#1102. The premise of synth#1013 — that ARM and RISC-V decline cleanly where aarch64 panicked — does not hold when the declined target is an internal rather than a requested export: the #952 export guard never fires. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo --- benches/gust/drivers/CROSS-ARCH.md | 10 +++++++++- benches/gust/drivers/check-cross-arch.py | 6 +++++- 2 files changed, 14 insertions(+), 2 deletions(-) diff --git a/benches/gust/drivers/CROSS-ARCH.md b/benches/gust/drivers/CROSS-ARCH.md index d561653..37103d8 100644 --- a/benches/gust/drivers/CROSS-ARCH.md +++ b/benches/gust/drivers/CROSS-ARCH.md @@ -32,7 +32,15 @@ set of names its wasm imports — no leak, no truncation. That half of the claim 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. +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: + +``` +ld.lld: error: undefined symbol: synth_func_18 +>>> referenced by out.o:(gust:hal/gpio@0.1.0#set) +``` + +Filed upstream as **synth#1102**. ## What the previous table said, and why it was wrong diff --git a/benches/gust/drivers/check-cross-arch.py b/benches/gust/drivers/check-cross-arch.py index a4071eb..12b51e8 100755 --- a/benches/gust/drivers/check-cross-arch.py +++ b/benches/gust/drivers/check-cross-arch.py @@ -52,6 +52,10 @@ # For a skipped INTERNAL function synth exits 0, so the unlinkable object ships # with only a warning. That is what let the old `> 0` rule read green. # +# Filed upstream as synth#1102, and re-confirmed on synth 0.60.0 (the latest +# release): 12 of 13 exit 0 with a dangling symbol, `ld.lld` refuses to link +# them. Not a regression -- 0.52.0 through 0.60.0 are identical on these inputs. +# # This ledger is a pin, not an excuse: if a driver starts crossing cleanly it # must be removed from the list, and the gate fails (exit 5) until it is. That # is how the ledger shrinks to empty instead of quietly outliving the bug. @@ -60,7 +64,7 @@ "mpu-thin", "pwm-thin", "spi-thin", "switch-thin", "timer-thin", "uart-thin", "wdg-thin", } -RISCV_TRACKER = "synth: RV32 selector gaps leave dangling `synth_func_N` refs" +RISCV_TRACKER = "synth#1102 — rv32 emits a dangling `synth_func_N` for a declined internal, exit 0" def run(cmd, **kw): From d9d52e072b58ad3ba65e6f131a66de237949cd05 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 28 Aug 2026 03:55:25 +0200 Subject: [PATCH 3/5] =?UTF-8?q?docs(ci):=20correct=20the=20cross-arch=20wo?= =?UTF-8?q?rkflow=20header=20=E2=80=94=20it=20stated=20the=20claim=20this?= =?UTF-8?q?=20PR=20disproves?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The header said: '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. On the equality rule ARM holds for all 13 and RISC-V holds for none (synth#1102). Also states why the rule is neither '> 0' nor '== 0' but equality, and that the RISC-V ledger fails on a status change in either direction. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo --- .github/workflows/drv-cross-arch.yml | 24 +++++++++++++++--------- 1 file changed, 15 insertions(+), 9 deletions(-) diff --git a/.github/workflows/drv-cross-arch.yml b/.github/workflows/drv-cross-arch.yml index fb0b65e..ca23639 100644 --- a/.github/workflows/drv-cross-arch.yml +++ b/.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: From 53c8afb97871ef6fa517784d3fd40be40c3c470c Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 28 Aug 2026 03:56:46 +0200 Subject: [PATCH 4/5] =?UTF-8?q?docs(plan):=20REQ-OS-TARGET-RV32-001=20is?= =?UTF-8?q?=20blocked=20=E2=80=94=20you=20cannot=20execute=20what=20does?= =?UTF-8?q?=20not=20link?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The v0.7.1 plan scopes this item as 'RISC-V from compiled to executed', on the premise that the objects already compile correctly and only lack a silicon run. They do not compile correctly. 0 of 13 drivers cross RISC-V on the corrected gate rule; ld.lld refuses every object (synth#1102, confirmed on 0.60.0). Records the blocker and the split that keeps the item shippable: the target-model half (generated RV32 target, memory.x, constants) is independent of the selector bug and can proceed; only the 'executed' half waits upstream. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo --- docs/releases/v0.7.1-plan.md | 34 +++++++++++++++++++++++++++++++++- 1 file changed, 33 insertions(+), 1 deletion(-) diff --git a/docs/releases/v0.7.1-plan.md b/docs/releases/v0.7.1-plan.md index 5f39605..e38f983 100644 --- a/docs/releases/v0.7.1-plan.md +++ b/docs/releases/v0.7.1-plan.md @@ -19,10 +19,42 @@ being added to something known rather than something assumed. | artifact | what it converts | |---|---| -| `REQ-OS-TARGET-RV32-001` / `VER-…` | RISC-V from *compiled* to *executed* — a model-generated RV32 target plus one driver silicon-validated against real registers | +| `REQ-OS-TARGET-RV32-001` / `VER-…` | RISC-V from *compiled* to *executed* — a model-generated RV32 target plus one driver silicon-validated against real registers. **BLOCKED, see below.** | | `REQ-OS-PARTITION-TENANT-001` / `VER-…` | ARINC-653 partitions from modelled to enforced — a component tenant confined to its partition on real silicon | | `REQ-DRV-COMPONENT-001` / `VER-…` | every thin-seam driver to a wasm component, with a whole-graph no-env-import gate | +### `REQ-OS-TARGET-RV32-001` is blocked upstream (2026-08-28) + +This item says "from *compiled* to *executed*". The premise is that the RISC-V +objects already compile correctly and only lack a silicon run. **They do not +compile correctly**, and this was not visible until the cross-arch gate's rule +was corrected from `undefined_count > 0` to *undefined set == wasm imports*. + +On the corrected rule, across all 13 thin-seam drivers: + +- **ARM: 13 of 13** lower cleanly. +- **RISC-V: 0 of 13.** Twelve emit an object carrying a dangling `synth_func_N` + — synth's RV32 selector declines a function it cannot select and emits the + call site anyway. `mpu-thin` emits nothing (`GlobalGet(0)` unsupported). + +`ld.lld` refuses them outright: + +``` +ld.lld: error: undefined symbol: synth_func_18 +>>> referenced by out.o:(gust:hal/gpio@0.1.0#set) +``` + +You cannot execute what does not link, so the silicon half of this item cannot +start. Filed as **synth#1102**. Confirmed on synth 0.60.0, the latest release — +bumping the pin does not clear it. Not a regression either: 0.52.0 through +0.60.0 are identical on these inputs. + +**What this does not block.** The *target-model* half — a model-generated RV32 +target, `memory.x`, generated constants — is independent of the selector bug and +can proceed. Only the "executed" half waits on synth#1102. Splitting the item +along that line is the honest way to keep it in v0.7.1 rather than deferring it +whole. + Plus the two execution rungs that could not fit v0.7.0's cut: - **E3** — run the dissolved composite under qemu / Renode; content gates on the composed From aca3d41395d569f905620085e1146ae50d202a2c Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 28 Aug 2026 05:32:26 +0200 Subject: [PATCH 5/5] fix(ci): the cross-arch gate needs wasm-tools, which its workflow never installed MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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, so drv-cross-arch.yml never installed it — this PR's gate would have exited 2 with 'FATAL: wasm-tools not usable' on the first CI run. Pinned to 1.245.1, the same version drv-components.yml uses, so both gates read imports through identical tooling. Also hardens synth_bin(): it shelled out to `varve which synth` unguarded, which raises FileNotFoundError where varve is not installed. CI never hit that path (it sets $SYNTH, checked first), but a local run without either would have crashed instead of falling back to PATH. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo --- .github/workflows/drv-cross-arch.yml | 7 +++++++ benches/gust/drivers/check-cross-arch.py | 5 ++++- 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/.github/workflows/drv-cross-arch.yml b/.github/workflows/drv-cross-arch.yml index ca23639..9d36338 100644 --- a/.github/workflows/drv-cross-arch.yml +++ b/.github/workflows/drv-cross-arch.yml @@ -85,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 diff --git a/benches/gust/drivers/check-cross-arch.py b/benches/gust/drivers/check-cross-arch.py index 12b51e8..18a2507 100755 --- a/benches/gust/drivers/check-cross-arch.py +++ b/benches/gust/drivers/check-cross-arch.py @@ -80,7 +80,10 @@ def synth_bin(): """Resolve synth through the varve pin; fall back to $SYNTH or PATH.""" if os.environ.get("SYNTH"): return os.environ["SYNTH"] - p = run(["varve", "which", "synth"]) + try: + p = run(["varve", "which", "synth"]) + except (FileNotFoundError, OSError): + return "synth" # no varve here (CI installs a pinned synth and sets $SYNTH) if p.returncode == 0 and p.stdout.strip(): cand = p.stdout.splitlines()[0].strip() if os.access(cand, os.X_OK):