From 7d3a21048e1b901bef2a6136802c343be811d8a9 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 23 Jul 2026 13:35:24 +0200 Subject: [PATCH 1/2] =?UTF-8?q?docs(release):=20record=20workstream=20D=20?= =?UTF-8?q?split=20=E2=80=94=20target-model=20ADC=20done=20(#215),=20silic?= =?UTF-8?q?on=20Vrefint=20blocked=20on=20#216?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 4.8 --- docs/releases/v0.5.0-unblock.md | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/docs/releases/v0.5.0-unblock.md b/docs/releases/v0.5.0-unblock.md index dcdfdc71..d7e3fdab 100644 --- a/docs/releases/v0.5.0-unblock.md +++ b/docs/releases/v0.5.0-unblock.md @@ -57,6 +57,20 @@ Vrefint** (channel 17). Add each peripheral's base to `stm32f100.aadl`, build th per-driver F100 firmware on generated constants, flash via the Pi (openocd `stlink-hla.cfg`), capture. Extend from wdg to the driver suite. +**Status (2026-07-23):** +- **D.1 target-model ADC support — DONE (#215, merged).** `stm32f100.aadl` gained a + `device Adc` (base `0x40012400`, `Vrefint_Ch => 17`); the generator emits + `ADC_BASE`/`VREFINT_CH` (kept optional via `device_opt`, so the G4 target is + byte-unchanged); WIT + goldens regenerated; all local oracles green. +- **D.2 silicon Vrefint anchor — BLOCKED on gale#216.** The dissolved adc-thin + driver writes `ADC_CR2` absolutely (`ADON` / `ADON|SWSTART`), so it drops + `CR2.TSVREFE` at the SWSTART instant — and TSVREFE must be set *during* the + conversion to read an F1 internal channel (Vrefint/temp). The verified driver + therefore cannot drive Vrefint. Unblocking needs a driver enhancement + (caller-supplied CR2-extra mask) + Kani re-verify + regenerated `.o` — see + gale#216. Deferred; **not** claimed as silicon-validated until that lands and the + physical read (~1489) is captured. + ### E. Docs accuracy + reader-friendliness (release hygiene) A release ships honest, readable docs. Fold in the claim-verification pass: - **Reconcile version claims** — remove/repair any "v0.5–v0.10 released/shipped" From ae2b0d96ad2b31a950ba89f2e7a5caec9062fe18 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 23 Jul 2026 13:45:08 +0200 Subject: [PATCH 2/2] docs(readme): replace drift-prone hand-typed counts with badges/qualitative; reconcile contradictions (v0.5.0 E) Co-Authored-By: Claude Opus 4.8 --- README.md | 10 +++++----- benches/gust/drivers/adc-thin/RESULTS.md | 6 ++++++ benches/gust/drivers/can-thin/RESULTS.md | 6 ++++++ benches/gust/drivers/dac-thin/RESULTS.md | 6 ++++++ benches/gust/drivers/gpio-thin/RESULTS.md | 7 +++++++ benches/gust/drivers/i2c-thin/RESULTS.md | 6 ++++++ benches/gust/drivers/pwm-thin/RESULTS.md | 6 ++++++ benches/gust/drivers/spi-thin/RESULTS.md | 6 ++++++ benches/gust/drivers/timer-thin/RESULTS.md | 6 ++++++ benches/gust/drivers/uart-thin/RESULTS.md | 7 +++++++ benches/gust/drivers/wdg-thin/RESULTS.md | 6 ++++++ benches/gust/esp32c3/RESULTS.md | 7 +++++++ benches/gust/silicon/RESULTS-f100.md | 6 ++++++ benches/gust/silicon/RESULTS-g474re.md | 6 ++++++ 14 files changed, 86 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index 319fddb8..5374667b 100644 --- a/README.md +++ b/README.md @@ -190,8 +190,8 @@ track alone can no longer silently invalidate the property. ### Functional testing (CI-enforced on every commit): -- **cargo test:** ~1015 runtime tests on stripped (non-Verus) code -- **Zephyr integration:** 36 upstream test suites on QEMU (M3 + MPS2/AN385 with MPU) +- **cargo test:** runtime tests on stripped (non-Verus) code — current pass/fail via the Rust CI badge above (`cargo test --workspace`) +- **Zephyr integration:** the upstream kernel test suites on QEMU (M3 + MPS2/AN385 with MPU) — current pass/fail via the Zephyr Tests badge above - **Renode emulation:** 3 boards (Cortex-M4F, M33, R5) - **Coverage:** Rust + Zephyr C line coverage → Codecov @@ -210,8 +210,8 @@ track alone can no longer silently invalidate the property. | Workflow | Scope | Status | |----------|-------|--------| -| Rust CI | cargo test, clippy, verus-strip gate | 995 tests | -| Zephyr Kernel Tests | 20 upstream test suites on qemu_cortex_m3 | 20/20 pass | +| Rust CI | cargo test, clippy, verus-strip gate | see Rust CI badge above | +| Zephyr Kernel Tests | upstream kernel test suites on qemu_cortex_m3 | see Zephyr Tests badge above | | Renode Emulation Tests | Cortex-M4F (STM32F4) + Cortex-M33 (STM32L552) + Cortex-R5 (ZynqMP) | 3 boards | ## Traceability @@ -247,7 +247,7 @@ The 277 lifecycle gaps break down as: ## Build ```bash -# Rust tests (995 tests) +# Rust tests cargo test # Verus verification diff --git a/benches/gust/drivers/adc-thin/RESULTS.md b/benches/gust/drivers/adc-thin/RESULTS.md index dee58093..76939821 100644 --- a/benches/gust/drivers/adc-thin/RESULTS.md +++ b/benches/gust/drivers/adc-thin/RESULTS.md @@ -41,3 +41,9 @@ capability externs are emitted as wasm imports via `.cargo/config.toml` A `gust_adc` demonstrator + Renode content-gate (assert the CR2 ADON/SWSTART writes and the DR-read-after-EOC ordering over a RAM-mapped ADC window, like `gust_spi`) and a rivet `VER-DRV-ADC-001` artifact — the same closure the SPI driver got. + +--- + +_Toolchain note: current pins are synth 0.49.0 / loom 1.2.0 (#208). The 0.49 regen +measured this driver's dissolved `.text` at **740 B** (was 754 B on synth 0.40.0, +above); register effects unchanged, 0-SRAM preserved._ diff --git a/benches/gust/drivers/can-thin/RESULTS.md b/benches/gust/drivers/can-thin/RESULTS.md index 54e25006..ebf78791 100644 --- a/benches/gust/drivers/can-thin/RESULTS.md +++ b/benches/gust/drivers/can-thin/RESULTS.md @@ -46,3 +46,9 @@ A `gust_can` demonstrator + Renode content-gate (assert BTR is written only insi INRQ/INAK window, and that TXRQ/RFOM0 are only ever set live-gated on TME0/FMP0) — the same closure the other thin-seam drivers got. Discharges rivet `VER-DRV-CAN-001` (artifacts/gust_can_driver.yaml). + +--- + +_Toolchain note: current pins are synth 0.49.0 / loom 1.2.0 (#208). The 0.49 regen +measured this driver's dissolved `.text` at **796 B** (was 804 B on synth 0.43.0, +above); register effects unchanged, 0-SRAM preserved._ diff --git a/benches/gust/drivers/dac-thin/RESULTS.md b/benches/gust/drivers/dac-thin/RESULTS.md index 37f699da..db573307 100644 --- a/benches/gust/drivers/dac-thin/RESULTS.md +++ b/benches/gust/drivers/dac-thin/RESULTS.md @@ -49,3 +49,9 @@ capability externs are emitted as wasm imports via `.cargo/config.toml` A `gust_dac` demonstrator + Renode content-gate (assert DHR write does NOT change DOR until the SWTRIGR write, then DOR == the loaded 12-bit code — the glitch-free property on real registers) and a rivet `VER-DRV-DAC-001` artifact. + +--- + +_Toolchain note: current pins are synth 0.49.0 / loom 1.2.0 (#208). The 0.49 regen +measured this driver's dissolved `.text` at **678 B** (was 686 B on synth 0.40.0, +above); register effects unchanged, 0-SRAM preserved._ diff --git a/benches/gust/drivers/gpio-thin/RESULTS.md b/benches/gust/drivers/gpio-thin/RESULTS.md index 52fc0365..a4a9e4a1 100644 --- a/benches/gust/drivers/gpio-thin/RESULTS.md +++ b/benches/gust/drivers/gpio-thin/RESULTS.md @@ -51,3 +51,10 @@ arm-zephyr-eabi-nm -u gpio-thin-cm3.o # only mmio_read32/write3 STM32VLDISCOVERY model (the mechanical oracle, mirroring `gust_uart`'s USART gate). This is the last gate; when it's green, `VER-DRV-GPIO-001` is added to rivet and `rivet release status v0.3.0` drops from `NOT cuttable (4)` → `(3)`. + +--- + +_Toolchain note: current pins are synth 0.49.0 / loom 1.2.0 (#208). The 0.49 regen +measured this driver's dissolved `.text` at **534 B** (was 490 B on synth 0.31.0, +above) — a +9% regression, the one outlier in the 10-driver byte-check; filed as a +synth note. Register effects unchanged, 0-SRAM preserved._ diff --git a/benches/gust/drivers/i2c-thin/RESULTS.md b/benches/gust/drivers/i2c-thin/RESULTS.md index ae76e2a9..b87f3986 100644 --- a/benches/gust/drivers/i2c-thin/RESULTS.md +++ b/benches/gust/drivers/i2c-thin/RESULTS.md @@ -60,3 +60,9 @@ are demonstrated via `i2c_start` (dup-START busy) and `i2c_addr_ack` (off-phase) instead. This is a wasm→native divergence in a reject path, consistent with the differentially-trusted (not proven-equivalent) dissolve; the safe polled path (Active reads/writes with the peripheral advancing SR1) is unaffected. + +--- + +_Toolchain note: current pins are synth 0.49.0 / loom 1.2.0 (#208). The 0.49 regen +measured this driver's dissolved `.text` at **974 B** (was 992 B on synth 0.40.0, +above); register effects unchanged, 0-SRAM preserved._ diff --git a/benches/gust/drivers/pwm-thin/RESULTS.md b/benches/gust/drivers/pwm-thin/RESULTS.md index 2f480dfe..c30a8e9d 100644 --- a/benches/gust/drivers/pwm-thin/RESULTS.md +++ b/benches/gust/drivers/pwm-thin/RESULTS.md @@ -41,3 +41,9 @@ A `gust_pwm` demonstrator + Renode content-gate (assert CCR ≤ ARR always, and `pwm_failsafe` clears MOE and no subsequent write re-enables output without a reconfigure) + rivet `VER-DRV-PWM-001`. Wires into the gale#63 Health Monitor as the actuator failsafe output stage. + +--- + +_Toolchain note: current pins are synth 0.49.0 / loom 1.2.0 (#208). The 0.49 regen +measured this driver's dissolved `.text` at **706 B** (was 728 B on synth 0.40.0, +above); register effects unchanged, 0-SRAM preserved._ diff --git a/benches/gust/drivers/spi-thin/RESULTS.md b/benches/gust/drivers/spi-thin/RESULTS.md index 1d1fd012..7c7da273 100644 --- a/benches/gust/drivers/spi-thin/RESULTS.md +++ b/benches/gust/drivers/spi-thin/RESULTS.md @@ -50,3 +50,9 @@ no-op. Source-level proof + native register-effect check; the wasm→native dissolve is differentially trusted, not proven equivalent (docs/safety/verification-honesty.md). + +--- + +_Toolchain note: current pins are synth 0.49.0 / loom 1.2.0 (#208). The 0.49 regen +measured this driver's dissolved `.text` at **454 B** (was 494 B on synth 0.33.1, +above); register effects unchanged, 0-SRAM preserved._ diff --git a/benches/gust/drivers/timer-thin/RESULTS.md b/benches/gust/drivers/timer-thin/RESULTS.md index a6fe31e0..e54e7fe0 100644 --- a/benches/gust/drivers/timer-thin/RESULTS.md +++ b/benches/gust/drivers/timer-thin/RESULTS.md @@ -44,3 +44,9 @@ wasm-tools print target/.../gust_timer_thin.wasm | grep -c 'i32.load offset=' loom optimize --passes inline --attestation false -o t.wasm synth compile t.wasm --target cortex-m3 --all-exports --relocatable -o timer-thin-cm3.o # 212 B, 0 SRAM ``` + +--- + +_Toolchain note: current pins are synth 0.49.0 / loom 1.2.0 (#208). The 0.49 regen +confirmed this driver's dissolved size is unchanged from the synth 0.33.0 measurement +above; register effects unchanged, 0-SRAM preserved._ diff --git a/benches/gust/drivers/uart-thin/RESULTS.md b/benches/gust/drivers/uart-thin/RESULTS.md index c713c7db..964b8eed 100644 --- a/benches/gust/drivers/uart-thin/RESULTS.md +++ b/benches/gust/drivers/uart-thin/RESULTS.md @@ -95,3 +95,10 @@ correctness gate works locally *and* in CI. | exports | uart_init, uart_tx_byte, uart_rx, uart_rx_fired | | TCB (import relocations) | mmio_read32, mmio_write32, irq_poll | | verified | usart_rx_decide — Kani SUCCESSFUL (error-priority, all 2³² SR) | + +--- + +_Toolchain note: current pins are synth 0.49.0 / loom 1.2.0 (#208), not the synth +0.15.0 used for the measurements above. The 0.49 regen (10-driver byte-check) +confirmed this driver's dissolved size is unchanged; register effects unchanged, +0-SRAM preserved._ diff --git a/benches/gust/drivers/wdg-thin/RESULTS.md b/benches/gust/drivers/wdg-thin/RESULTS.md index 5ed11bae..b7241c4b 100644 --- a/benches/gust/drivers/wdg-thin/RESULTS.md +++ b/benches/gust/drivers/wdg-thin/RESULTS.md @@ -42,3 +42,9 @@ once Running (`p3`). A `gust_wdg` demonstrator + Renode content-gate (assert the KR key sequence + that no software write clears the running state) and a rivet `VER-DRV-WDG-001` artifact. Ties into the partition-scheduler Health Monitor (gale#63) as the HW fail-to-safe backstop. + +--- + +_Toolchain note: current pins are synth 0.49.0 / loom 1.2.0 (#208). The 0.49 regen +measured this driver's dissolved `.text` at **648 B** (was 660 B on synth 0.40.0, +above); register effects unchanged, 0-SRAM preserved._ diff --git a/benches/gust/esp32c3/RESULTS.md b/benches/gust/esp32c3/RESULTS.md index ffd24a80..fd7cf89e 100644 --- a/benches/gust/esp32c3/RESULTS.md +++ b/benches/gust/esp32c3/RESULTS.md @@ -80,3 +80,10 @@ cat /dev/cu.usbmodem # the app re-prints the ratio in a loop Regenerate the dissolved object: `synth compile .wasm -b riscv --target esp32c3 --all-exports --relocatable -o gust_mix-esp32c3.o` + +--- + +_Toolchain note: current pins are synth 0.49.0 / loom 1.2.0 (#208), not the synth +0.40.0 dissolve measured above. `gust_mix` has not been re-measured on real +ESP32-C3 silicon under 0.49; the ratios above are historical until that re-run +happens._ diff --git a/benches/gust/silicon/RESULTS-f100.md b/benches/gust/silicon/RESULTS-f100.md index 9db0cc82..4c5ea3aa 100644 --- a/benches/gust/silicon/RESULTS-f100.md +++ b/benches/gust/silicon/RESULTS-f100.md @@ -38,3 +38,9 @@ baked in), not the `.bin`+offset (openocd 0.12 `program` arg quirk). For a more ergonomic setup, drive the F100 via the G474's **ST-LINK/V3 as an external SWD probe** (remove the VLDISCOVERY CN3 jumpers, wire SWD) — then probe-rs / run.sh work unchanged. + +--- + +_Toolchain note: current pins are synth 0.49.0 / loom 1.2.0 (#208), not the synth +0.15.0 dissolve measured above. `gust_mix` has not been re-measured on real F100 +silicon under 0.49; the ratio above is historical until that re-run happens._ diff --git a/benches/gust/silicon/RESULTS-g474re.md b/benches/gust/silicon/RESULTS-g474re.md index 0e5fb215..50c4f5d3 100644 --- a/benches/gust/silicon/RESULTS-g474re.md +++ b/benches/gust/silicon/RESULTS-g474re.md @@ -59,3 +59,9 @@ baseline-subtracted. Same harness as the 0.12.0 row above; only the dissolved - **Fixed** a latent `run.sh` arg-parse bug (`${1:?... {g474re|f100}}` appended a literal `}` to `$BOARD`). Two probes present (board ST-LINK + an ESP-JTAG); pass `--probe ` explicitly. + +--- + +_Toolchain note: current pins are synth 0.49.0 / loom 1.2.0 (#208), not the synth +0.40.0 "current pin" above. `gust_mix` has not been re-measured on real M4 silicon +under 0.49; the ratios above are historical until that re-run happens._