Skip to content

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

Closed
avrabe wants to merge 5 commits into
fix/varve-pin-digestfrom
fix/cross-arch-gate-strict
Closed

fix(drv): the cross-arch gate was green because it could not see the defect#313
avrabe wants to merge 5 commits into
fix/varve-pin-digestfrom
fix/cross-arch-gate-strict

Conversation

@avrabe

@avrabe avrabe commented Aug 28, 2026

Copy link
Copy Markdown
Contributor

Stacked on #312 (the varve pin fix) — without it no varve-shimmed tool resolves in this repo.

The gate merged in #310 was green for the wrong reason

It 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, switch were
never checked. This is the third enumerated list this month to silently exclude
the newest thing — after check-providers.sh and the Lean target list. Now
discovered, like those.

> 0 is not the property. It is satisfied by any undefined symbol,
including a leaked one — and hm-thin imports nothing, so a correct object
has zero undefined symbols and would fail.

The rule is equality: the object's undefined set must equal the names the wasm
imports. Same rule check-driver-components.py already applies on its object
axis.

What the correct rule finds

result
ARM 13/13 clean — undefined set == imports, exactly. No leak, no truncation.
RISC-V 0/13.
Full table (re-measured, synth 0.58.0)
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 — 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

Twelve RISC-V objects cannot be linked: synth's RV32 selector skips a function
it cannot select and emits the call site anyway, leaving a dangling
synth_func_N (definitions are named func_N, so it never resolves). On ARM
the same internals are emitted as local t func_N, all defined — the defect is
specific to the RISC-V backend.

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)

For a skipped internal function synth exits 0, so the unlinkable object
ships with only a warning. That is exactly what let > 0 read green.

Not a regression. Bisected 0.52.0 / 0.53.0 / 0.54.0 / 0.55.0 / 0.57.0 /
0.58.0 — all produce identical results on today's sources. Filing upstream
separately.

The RISC-V leg is a ledger, not a skip

If a driver starts crossing cleanly the gate fails (exit 5) until it is
removed from RISCV_KNOWN_BAD. The list shrinks to empty instead of outliving
the bug. A driver that newly breaks also fails.

CROSS-ARCH.md 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. The
section that justified > 0 is replaced by one explaining why it was the wrong
rule.

Also: a duplicate gate I created

check-driver-components.sh already existed — a red-first shell gate for
REQ-DRV-COMPONENT-001 — when I wrote the .py for the same requirement. Two
gates for one requirement is itself a drift hazard, and the .sh was wired to
nothing. Removed; its red-first framing is preserved in the .py.

Kill-criterion

check-cross-arch.py --self-test must reject a leaked-symbol superset and must
pass an empty expectation:

  self-test ok: leaked symbol (superset) is rejected
  self-test ok: a driver importing nothing passes with 0 undefined

Both run in CI as a step before the gate.

🤖 Generated with Claude Code

https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo

@avrabe

avrabe commented Aug 28, 2026

Copy link
Copy Markdown
Contributor Author

Note on this PR's checks: it is currently based on fix/varve-pin-digest, and every gale workflow filters pull_request: branches: [main]. So no workflow fires on it at all — the zero-checks state here is an empty gate, not a pass, and it must not be read as green.

Retargeting to main once #312 merges, at which point the real gates run.

@avrabe
avrabe force-pushed the fix/varve-pin-digest branch from 801f749 to 73385e9 Compare August 28, 2026 02:30
avrabe and others added 4 commits August 28, 2026 04:30
…defect

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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
…m this PR disproves

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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
…at does not link

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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
@avrabe
avrabe force-pushed the fix/cross-arch-gate-strict branch from 9dd37c9 to 53c8afb Compare August 28, 2026 02:30
…er installed

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 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
@avrabe

avrabe commented Aug 28, 2026

Copy link
Copy Markdown
Contributor Author

Superseded by #316 — same branch, targeting main. GitHub auto-closed this one when fix/varve-pin-digest was deleted on #312's merge.

Worth recording why this PR was never evidence of anything: it targeted a non-main base, and every gale workflow filters pull_request: branches: [main], so no workflow ever ran on it. It sat at CLEAN with zero checks for its whole life. A stacked PR here does not get a reduced gate — it gets none.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant