fix(drv): the cross-arch gate was green because it could not see the defect - #313
fix(drv): the cross-arch gate was green because it could not see the defect#313avrabe wants to merge 5 commits into
Conversation
|
Note on this PR's checks: it is currently based on Retargeting to |
801f749 to
73385e9
Compare
…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
9dd37c9 to
53c8afb
Compare
…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
|
Superseded by #316 — same branch, targeting Worth recording why this PR was never evidence of anything: it targeted a non- |
The gate merged in #310 was green for the wrong reason
It asserted
undefined_count > 0over a hand-written list of 8 drivers. Bothhalves were wrong, and they cancelled into a green light.
It gated 8 of 13.
DRIVERS=(wdg gpio i2c timer adc dac pwm uart)whilethirteen
*-thindirectories exist.can,hm,mpu,spi,switchwerenever checked. This is the third enumerated list this month to silently exclude
the newest thing — after
check-providers.shand the Lean target list. Nowdiscovered, like those.
> 0is not the property. It is satisfied by any undefined symbol,including a leaked one — and
hm-thinimports nothing, so a correct objecthas 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.pyalready applies on its objectaxis.
What the correct rule finds
Full table (re-measured, synth 0.58.0)
read32 write32read32 write32read32 write32read32 write32(none)read32 write32mpu-writewrite32read32 write32ctx-resume ctx-save region-swapread32 write32poll read32 write32read32 write32Twelve 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 namedfunc_N, so it never resolves). On ARMthe same internals are emitted as local
t func_N, all defined — the defect isspecific to the RISC-V backend.
For a skipped internal function synth exits 0, so the unlinkable object
ships with only a warning. That is exactly what let
> 0read 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 outlivingthe bug. A driver that newly breaks also fails.
CROSS-ARCH.md was stale, not wrong-at-the-time
It measured pre-componentization sources —
wdg-thinhad 6 functions then, 21now — and was never re-measured when they changed. Re-measured here. The
section that justified
> 0is replaced by one explaining why it was the wrongrule.
Also: a duplicate gate I created
check-driver-components.shalready existed — a red-first shell gate forREQ-DRV-COMPONENT-001 — when I wrote the
.pyfor the same requirement. Twogates for one requirement is itself a drift hazard, and the
.shwas wired tonothing. Removed; its red-first framing is preserved in the
.py.Kill-criterion
check-cross-arch.py --self-testmust reject a leaked-symbol superset and mustpass an empty expectation:
Both run in CI as a step before the gate.
🤖 Generated with Claude Code
https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo