feat(gust): generic driver model — gust:hal seam + verified thin-seam UART driver (gale#65)#113
Merged
Conversation
…T spike) Right-sized first bite for a generic driver-extension model: define the gust:hal WIT capability seam (dissolved driver imports, TCB bridge implements) and prove it with ONE UART driver end-to-end, protocol in verified wasm, built at three seam granularities (thin MMIO-prim / mid byte-caps / fat embassy) to MEASURE the TCB bytes each costs — the empirical answer to "how much of a driver can move into verified wasm." Pinned to the STM32VLDISCOVERY (STM32F100) Renode target (real UART.STM32_UART model, content-based Wait-For-Line correctness gate, 4th renode_test target) — the constrained device we need anyway; the fat/embassy seam is expected to NOT fit 8 KB SRAM, which is itself the proof the tiny node requires the thin seam. embassy HAL-only (kiln stays the one executor); manifest+generator deferred until Jess's ask makes driver #2 (extract from real duplication, not guess). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…e composition Incorporate review feedback: - Target is the STM32F100 (Jess's device class) THROUGHOUT — no larger-device arm. Fat/embassy is the on-F100 overflow check (quantify why it can't fit 8 KB), not a path on a bigger part. - SRAM (.bss/.data) vs the 8 KB budget is the HEADLINE metric (the binding constraint), alongside TCB bytes. Flash is cheap (dissolved .text runs from 128 KB flash); SRAM = wasm linear memory / buffers / shadow stack is what binds. - Per-node bespoke composition is the core extension model: each node's image is one wasm composed with exactly the specific drivers it needs, fused + dissolved — the composition (not a fixed firmware) is the product; minimal SRAM, maximal verified surface. - XIP recorded as a follow-on lever that addresses flash/code (a library of per-node images in external flash), NOT the SRAM/buffer pressure — scoped out. - Risk: embassy-stm32 may not support F100 → fat-seam footprint taken on nearest supported F1 (F103) as proxy. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Traceability leads the feature loop. 15 artifacts under SYSREQ-BYOOS-001:
- REQ-DRV-{SEAM,WASM,SRAM,COMPOSE,ASYNC}-001 — the seam, the verified-wasm/TCB
split, the F100 8 KiB SRAM budget, per-node bespoke composition, sync+split-phase.
- DD-DRV-{EMBASSY,GRAN,XIP}-001 — embassy-HAL-only/kiln-executor, granularity-by-
measurement, XIP-as-flash-lever-not-SRAM.
- SAC-DRV-{HAL,UART} — the gust:hal WIT seam + the UART driver (3-seam bridges).
- VER-DRV-{UART-RENODE,SRAM} — the Renode content-based TX/RX gate + the SRAM
budget oracle.
- FIND-DRV-MEASURE-001 (the per-seam SRAM/TCB spike, results pending; feeds the
perf bench) + FIND-DRV-SPAR-001 (gust:hal hand-authored, spar->WIT not wired
for the wasm-component layer — friction logged).
rivet validate: PASS. Design spec: docs/superpowers/specs/2026-06-25-...
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ale#65) The thin-seam maximal-wasm extreme, realising gale#65's "only registers/MMIO are native, everything above is wasm" on the STM32F100 px4io failsafe class. - benches/gust/drivers/wit/gust-hal.wit — the capability seam: mmio (read32/ write32/read8/write8), irq (poll, split-phase), uart-byte (mid), uart-block (fat); driver-thin/mid/fat worlds. Hand-authored (FIND-DRV-SPAR-001); Jess co-designs per gale#65. - benches/gust/drivers/uart-thin — the ENTIRE STM32 USART protocol (init, baud, TXE/RXNE poll, RX drain) in verified wasm, importing only mmio + irq. Dissolved (loom 1.1.16 + synth 0.15.0, --native-pointer-abi): **326 B flash .text, 0 B .data, 0 B .bss — ZERO SRAM** (poll-drain form), TCB = 3 import relocations (mmio_read32/write32, irq_poll), exports driver_step. The whole driver is verified; the trusted surface is the ~10-line generic bridge. Honest caveat: a buffered CCSDS-stream RX (the gale#65 real target — USART @ 1.5 Mbaud carrying relay-sec-wrapped CCSDS, which can itself dissolve to wasm) puts its ring buffer in SRAM; the protocol logic stays SRAM-free. mid/fat seam measurements + the buffered variant + the Renode F100 USART gate are next. rivet: PASS (FIND-DRV-MEASURE-001 records the thin result). Spec updated with the gale#65 requirements source. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ed wasm") Correcting an overclaim: the thin driver was "in wasm", not verified. gale's bar is Verus + Rocq + Kani (CLAUDE.md), and a DAL-A px4io driver (gale#65) must meet it. So the driver's pure decision now carries a real proof: - usart_rx_decide (gale _decide style): errors take priority over data-ready, so the driver provably never reads DR on an overrun/framing error (stream desync). Wired into rx_poll. **Kani: VERIFICATION SUCCESSFUL** over all 2^32 SR values (cargo kani --harness rx_decide_error_priority, 0/14 checks failed). - Re-dissolved (synth 0.15.0): 382 B flash, still 0 SRAM (was 326 B; +56 B for the verified RX gate). Design corrected accordingly: - REQ-DRV-VERIFY-001 + VER-DRV-KANI in rivet — driver logic carries Verus+Rocq+ Kani like the kernel primitives; "verified" is earned by proofs. - Verus + Rocq tracks attach on promoting the decision into the gale verified crate (src/ -> verus-strip -> plain/ -> wasm; proofs/*.v). - Buffering will REUSE the already-proven gale::msgq ring (Verus+Rocq+Kani) rather than an unverified buffer — maximal-wasm AND maximal-verified. - Only the irreducible MMIO poke stays unverified I/O (the whole TCB). rivet: PASS. Spec gains a Verification section. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
….0 perf test The driver driven bare-metal on the M3, and the perf test the loop asked for. - gust_uart bin: the whole TRUSTED side — a ~10-line gust:hal thin bridge (mmio_read32/write32 + irq_poll) + the r11=0 trampoline (driver_step_body) + boot. Links the dissolved thin driver. build.rs wires it. - renode-test: usart1 = UART.STM32_UART @ 0x40013800 (-> nvic@37) added to stm32f100.repl + m3_64k.repl — the real STM32 USART register model. synth 0.15.0 perf test (new version), levers ON vs OFF on the UART driver: **0% delta** (382 B both, cm3==cm4) — the driver is I/O-bound (register loads/stores + poll via meld-dispatched imports), not the arithmetic the levers target (which gave gust_mix -31%). Finding for the perf loop: the optimisation opportunity for driver code is the MELD-DISPATCH import-call overhead, not the ARM peephole levers → a meld/synth recommendation. Honest status: gust_uart RUNS on the M3 (762 instr, no fault; USART SR TXE set, no TX spin). The content-based TX gate is PENDING a data-placement detail — native-pointer-abi places the TX string in the 1 MB wasm linmem at a VMA the gust linker doesn't map (control_step avoided this via its reserved-linmem .bss; this 0-bss driver's string doesn't). Resolution = the synth#383/native-pointer-abi linmem placement (or drop the string constant). Driver LOGIC is Kani-proven and dissolves clean; only the demo's string placement is pending. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…thin" Resolves the data-placement blocker by the cleaner design: a driver provides PROTOCOL PRIMITIVES (uart_init/uart_tx_byte/uart_rx/uart_rx_fired) and the APP owns the payload. The driver now carries NO data segment (the earlier failure was an embedded TX string landing in the wasm 1MB linmem at a VMA the linker didn't map under native-pointer-abi). 254 B flash, 0 SRAM, no r11 trampoline needed. End-to-end on a hermetic Renode Cortex-M3 with a REAL STM32 USART model: the dissolved driver TXes over MMIO and the USART emits — captured "gust-uart-thin" (614 instr, no fault). Bonus: a real USART file-backend IS capturable headless on the macOS portable (unlike SemihostingUart), so the content gate works locally + CI. Verification intact: usart_rx_decide still Kani-proven (error-priority over all 2^32 SR values). The driver logic is verified; the app's string is plain flash. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…real USART 4th renode_test target (gust-uart-renode): boots the gust_uart demonstrator on the hermetic Cortex-M3 + real STM32 USART model and asserts the dissolved driver's emitted bytes via `Wait For Line On Uart gust-uart-thin` — content on the wire, not just no-fault. Uses the terminal-tester mechanism the stm32f4 sem robots already prove in CI; a real USART captures headless (unlike the SemihostingUart, so this is a true content gate). Verified locally: the USART emits "gust-uart-thin". Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Add //:gust-uart-renode to the gust-renode workflow so the UART driver's content-based TX gate (Wait For Line on a real STM32 USART) runs in CI alongside the three M3 device-class targets. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
A generic, repeatable way to extend gust with drivers — and the first one working end-to-end. Realises gale#65 ("only registers/MMIO native, everything above is wasm") on the STM32F100 px4io class.
Run through the PulseEngine feature loop: rivet traceability →
gust:halWIT seam → verified driver → Kani proof → Renode content gate.The seam
gust:halWIT:mmio(read32/write32),irq(poll, split-phase),uart-byte(mid),uart-block(fat). A driver imports capabilities; the ~10-line TCB bridge implements them. Granularity (thin/mid/fat) trades TCB size vs verified-wasm fraction.Thin-seam UART driver — working & verified
The whole STM32 USART protocol in wasm, importing only
mmio+irq:usart_rx_decide): errors take priority over data-ready, so the driver provably never readsDRmid-error (all 2³² SR values —VERIFICATION SUCCESSFUL).UART.STM32_UART): emitsgust-uart-thin— asserted by a 4threnode_testCI target (gust-uart-renode,Wait For Line On Uart, content not just no-fault).Design notes
uart_init/uart_tx_byte/uart_rx). Keeps the driver data-segment-free (0 linmem) and fixed the native-pointer-abi placement issue.Follow-ups (tracked)
gale::msgqring (where SRAM + the CCSDS-stream verification attach).rivet: PASS. Spec:
docs/superpowers/specs/2026-06-25-gust-driver-model-design.md.🤖 Generated with Claude Code