From 03d73949242b6032272c8563ec4c51057bb10037 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 29 Jul 2026 06:09:43 +0200 Subject: [PATCH 1/2] docs(silicon): withdraw the cannot-un-start claim from the wdg G474RE result MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A persona review panel auditing the showcase material against docs/safety/verification-honesty.md found this file claiming the silicon run 'validates the wdg driver's IWDG programming + the cannot-un-start effect on real silicon'. It does not. gust_wdg_silicon.rs arms the watchdog and stops refreshing it; it never ATTEMPTS an un-start (grep for wdg_refresh/stop/disable in that firmware returns 0 hits), so no rejection path was exercised on hardware. p2_cannot_un_start is a source-level Kani property over the pure FSM and stays exactly that. Restates what the run does evidence — one happy path, once, on one die: the dissolved object emitted an unlock/configure/lock/start key sequence the real IWDG accepted, and the hardware fired — and notes the effect has reproduced across two sessions (0x1c->0x3c and 0x14->0x34). Also flags that the ~1.2 s is the CONFIGURED timeout (PR=5, RLR=0x123, nominal LSI), not a measured interval; the probe-rs log's wall-clock gap is host detection latency and carries no timing claim. Co-Authored-By: Claude Opus 4.8 --- benches/gust/silicon/RESULTS-wdg-g474re.md | 21 +++++++++++++++++---- 1 file changed, 17 insertions(+), 4 deletions(-) diff --git a/benches/gust/silicon/RESULTS-wdg-g474re.md b/benches/gust/silicon/RESULTS-wdg-g474re.md index 5d2e7d56..41585a37 100644 --- a/benches/gust/silicon/RESULTS-wdg-g474re.md +++ b/benches/gust/silicon/RESULTS-wdg-g474re.md @@ -32,10 +32,23 @@ reset source. A silently-no-op'd start (KR=0xCCCC) would never reset, so the tes cannot false-pass. ## Scope / honesty -- This validates the wdg driver's IWDG programming + the cannot-un-start effect - **on real silicon** — the strongest evidence tier (above the qemu probe + Renode - content-gate). The Kani proofs (7/7) remain the source-level guarantee; this shows - the *dissolved object* drives real hardware to the real effect. +- This validates the wdg driver's IWDG **unlock → configure → lock → start** key + sequence **on real silicon** — the strongest evidence tier (above the qemu probe + + Renode content-gate). The Kani proofs (7/7) remain the source-level guarantee; this + shows the *dissolved object* drives real hardware to the real effect. +- **NOT evidenced here: cannot-un-start.** An earlier revision of this file claimed + this run validated "the cannot-un-start effect on real silicon". It does not, and the + claim has been withdrawn. `gust_wdg_silicon.rs` arms the watchdog and then simply + stops refreshing it; it never *attempts* an un-start, so nothing on silicon exercised + a rejection path. `p2_cannot_un_start` is a source-level Kani property over the pure + FSM and stays exactly that. What this run evidences is one happy path, once, on one + die: the dissolved object emitted a key sequence the real IWDG accepted, and the + hardware fired. (n=1; `RESULTS` also records a second session at + `RCC_CSR=0x14000000 → 0x34000000`, so the effect has reproduced across runs.) +- The stated **~1.2 s** is the *configured* timeout computed from PR=5 / RLR=0x123 + against a nominal ~32 kHz LSI — it is not a measured interval, and the LSI is spec'd + loose. The captured probe-rs log shows a much longer wall-clock gap before the + session drops (host detection latency), so no timing claim should be read off it. - Only the **IWDG** is register-portable F1→G4. adc/dac/i2c/can/pwm use F1-specific register maps → faithful silicon needs an STM32F1 board (VLDISCOVERY) or a G4 re-target; those remain qemu/Renode-validated for now. From 5811dc7b28a91937fba58a00f4c2ec7f585e75eb Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 29 Jul 2026 06:35:33 +0200 Subject: [PATCH 2/2] =?UTF-8?q?docs(silicon):=20second=20die=20=E2=80=94?= =?UTF-8?q?=20the=20same=20dissolved=20wdg-thin=20.o=20fires=20the=20IWDG?= =?UTF-8?q?=20on=20STM32F100?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The G474RE result carried an n=1 caveat. This reproduces it on a different family and a different die: the identical wdg-thin-cm3.o (same wasm, same dissolve, unrebuilt) arms the real IWDG on an STM32F100/Cortex-M3 and the hardware fires the reset — RCC_CSR 0x14000000 -> 0x34000000, IWDGRSTF set. Twice, back to back. It is also cleaner evidence than the G4 run. probe-rs loses its session when the watchdog resets the G4, so boot 1 and boot 2 there are two invocations. openocd holds SWD across the reset, so this is one unspliced capture, and the harness clears RMVF and starts the CPU with SYSRESETREQ (which sets SFTRSTF, not IWDGRSTF) — a set IWDGRSTF at boot 2 cannot be stale. Scope is unchanged: a second die for the same happy path, not a new property. It does not evidence cannot-un-start, ~1.2 s is still the configured timeout and not a measurement, and the cross-architecture claim stays narrow — no thin-seam driver dissolves to RISC-V today (synth 0.49.0 emits no relocations for imported calls; filed as synth#871), so what is shown is one wasm -> one Cortex-M object -> two dies. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo --- benches/gust/silicon/RESULTS-wdg-f100.md | 61 ++++++++++++++++++++++ benches/gust/silicon/RESULTS-wdg-g474re.md | 6 ++- benches/gust/silicon/run-wdg-f100.sh | 54 +++++++++++++++++++ benches/gust/silicon/wdg-f100-run1.log | 3 ++ benches/gust/silicon/wdg-f100-run2.log | 3 ++ 5 files changed, 125 insertions(+), 2 deletions(-) create mode 100644 benches/gust/silicon/RESULTS-wdg-f100.md create mode 100755 benches/gust/silicon/run-wdg-f100.sh create mode 100644 benches/gust/silicon/wdg-f100-run1.log create mode 100644 benches/gust/silicon/wdg-f100-run2.log diff --git a/benches/gust/silicon/RESULTS-wdg-f100.md b/benches/gust/silicon/RESULTS-wdg-f100.md new file mode 100644 index 00000000..17fd34c0 --- /dev/null +++ b/benches/gust/silicon/RESULTS-wdg-f100.md @@ -0,0 +1,61 @@ +# wdg-thin — SECOND DIE: STM32F100 (VLDISCOVERY), Cortex-M3 (2026-07-29) + +The **same** dissolved `wdg-thin-cm3.o` that fired the watchdog on the NUCLEO-G474RE +(Cortex-M4) also fires it on an **STM32F100 / Cortex-M3** — a different family, a +different die, and the architecture the object was actually compiled for +(`synth --target cortex-m3`). On the G4 it runs as thumbv7m ⊂ thumbv7em; here it runs +natively. + +Nothing about the driver was rebuilt for this: the wasm, the dissolve, and the `.o` +are identical. Only `memory.x` (flash/RAM geometry) and the firmware's target feature +differ, and neither touches the driver. + +## Captured evidence + +Two consecutive runs, `wdg-f100-run{1,2}.log`, identical in outcome: + + gust-wdg-silicon: boot 1 on STM32F100 (RCC_CSR=0x14000000, no prior WDG reset). + Arming the REAL IWDG @0x40003000 via the dissolved wdg-thin driver + (PR=5, RLR=0x123 ≈ 1.2 s)... + gust-wdg-silicon: armed (last KR write=0x0000, is_running=1). NOT refreshing — + expect a HARDWARE reset in ~1.2 s, after which boot 2 reads IWDGRSTF=1. + gust-wdg-silicon OK: IWDG watchdog reset CONFIRMED on real STM32F100 silicon + (RCC_CSR=0x34000000, IWDGRSTF=1) — the dissolved wdg-thin driver armed the + hardware watchdog and it fired the reset. + +`RCC_CSR` 0x14000000 → 0x34000000: bit 29 (`IWDGRSTF`) set by the hardware. + +## Why this run is better evidence than the G474RE one + +- **One continuous session, not two.** The G474RE capture is two `probe-rs` + invocations, because the watchdog reset kills the probe-rs session — boot 1 and + boot 2 had to be reported as separate takes. Here openocd holds the SWD session + across the reset, so boot 1 → hardware reset → boot 2 is a **single unspliced + capture**. The reset is observed in-line, not inferred from a reconnect. +- **The reset flags are cleared by the harness immediately before the run** + (`mww 0x40021024 0x01000000`, RMVF), and the CPU is started with a software reset + (`SYSRESETREQ`), which sets `SFTRSTF` — *not* `IWDGRSTF`. So a set `IWDGRSTF` at + boot 2 cannot be stale. +- **Reproduced twice**, back to back, byte-identical outcome. + +## Scope / honesty + +- This is a **second die** for the same happy path, not a new property. It evidences + portability of the dissolved object and reproduces the arm→fire effect. It does + **not** evidence `p2_cannot_un_start` — the firmware still never attempts an + un-start (see `RESULTS-wdg-g474re.md`). +- **~1.2 s remains the configured timeout**, computed from PR=5 / RLR=0x123 against a + nominal ~32 kHz LSI. It is not measured here either; the LSI is spec'd loose and the + F1 and G4 LSIs are different parts. +- Portability holds here because the **IWDG is register-identical** across the STM32 + line. It does not generalise: adc/dac/i2c/can/pwm use family-specific register maps. +- The cross-*architecture* claim is narrower still. The same wasm dissolves to + RISC-V only for import-free modules; `synth` 0.49.0 cannot yet emit a relocatable + RISC-V object for a module with imports (`external call without relocation table`), + so no thin-seam driver dissolves to RISC-V today. Filed upstream as synth#871. + What is demonstrated here is **one wasm → one Cortex-M object → two different STM32 + dies**. + +## Reproduce + + benches/gust/silicon/run-wdg-f100.sh # needs an ST-LINK + openocd diff --git a/benches/gust/silicon/RESULTS-wdg-g474re.md b/benches/gust/silicon/RESULTS-wdg-g474re.md index 41585a37..f32d09ed 100644 --- a/benches/gust/silicon/RESULTS-wdg-g474re.md +++ b/benches/gust/silicon/RESULTS-wdg-g474re.md @@ -43,8 +43,10 @@ cannot false-pass. a rejection path. `p2_cannot_un_start` is a source-level Kani property over the pure FSM and stays exactly that. What this run evidences is one happy path, once, on one die: the dissolved object emitted a key sequence the real IWDG accepted, and the - hardware fired. (n=1; `RESULTS` also records a second session at - `RCC_CSR=0x14000000 → 0x34000000`, so the effect has reproduced across runs.) + hardware fired. (`RESULTS` also records a second session at + `RCC_CSR=0x14000000 → 0x34000000`, so the effect has reproduced across runs. It has + since also reproduced on a **second die of a different family** — the same `.o` on an + STM32F100/Cortex-M3, twice, in one unspliced session: see `RESULTS-wdg-f100.md`.) - The stated **~1.2 s** is the *configured* timeout computed from PR=5 / RLR=0x123 against a nominal ~32 kHz LSI — it is not a measured interval, and the LSI is spec'd loose. The captured probe-rs log shows a much longer wall-clock gap before the diff --git a/benches/gust/silicon/run-wdg-f100.sh b/benches/gust/silicon/run-wdg-f100.sh new file mode 100755 index 00000000..34d34de6 --- /dev/null +++ b/benches/gust/silicon/run-wdg-f100.sh @@ -0,0 +1,54 @@ +#!/usr/bin/env bash +# wdg-thin on real STM32F100 silicon (VLDISCOVERY, ST-LINK/V1) — see RESULTS-wdg-f100.md +# +# Boot 1 arms the real IWDG through the dissolved wdg-thin object and stops refreshing +# it; the hardware resets the chip; boot 2 reads IWDGRSTF=1. openocd holds the SWD +# session across the reset, so the whole thing is one capture. +# +# The firmware prints via semihosting, so openocd must stay attached — this is not a +# flash-and-walk-away run. +# +# Env: +# OCD_HOST run openocd over ssh on this host (e.g. pi@192.168.178.88); local if unset +set -euo pipefail +cd "$(dirname "$0")/.." + +ELF=target/thumbv7m-none-eabi/release/gust_wdg_silicon +RCC_CSR=0x40021024 # STM32F1 reset/clock control — status +RMVF=0x01000000 # clear the reset flags +AIRCR=0xE000ED0C +SYSRESETREQ=0x05FA0004 + +echo "==> building for F100 (only memory.x and the target feature differ; the driver .o does not)" +cp memory.x /tmp/memory.x.bak +cp targets/generated/memory-stm32f100.x memory.x +trap 'cp /tmp/memory.x.bak memory.x' EXIT +rm -f "$ELF" # force a relink at 0x08000000 +touch src/bin/gust_wdg_silicon.rs +cargo build --release --bin gust_wdg_silicon \ + --no-default-features --features target-f100 --target thumbv7m-none-eabi + +OCD=(openocd -f interface/stlink-hla.cfg -c "transport select swd" + -f target/stm32f1x.cfg -c "reset_config none separate") + +run_ocd() { # run_ocd + if [ -n "${OCD_HOST:-}" ]; then + # shellcheck disable=SC2029 + ssh "$OCD_HOST" "sudo timeout 25 $(printf '%q ' "${OCD[@]}" "$@")" + else + sudo timeout 25 "${OCD[@]}" "$@" + fi +} + +if [ -n "${OCD_HOST:-}" ]; then scp "$ELF" "$OCD_HOST:/tmp/wdg_f100.elf"; FW=/tmp/wdg_f100.elf +else FW="$ELF"; fi + +echo "==> flashing" +run_ocd -c init -c "program $FW verify" -c exit + +echo "==> arming (flags cleared first, so IWDGRSTF at boot 2 cannot be stale)" +run_ocd -c init -c "arm semihosting enable" -c halt \ + -c "mww $RCC_CSR $RMVF" -c "mww $AIRCR $SYSRESETREQ" -c halt -c resume \ + 2>&1 | grep --line-buffered "gust-wdg-silicon" || true + +echo "==> expected: RCC_CSR 0x14000000 -> 0x34000000, IWDGRSTF=1" diff --git a/benches/gust/silicon/wdg-f100-run1.log b/benches/gust/silicon/wdg-f100-run1.log new file mode 100644 index 00000000..457de946 --- /dev/null +++ b/benches/gust/silicon/wdg-f100-run1.log @@ -0,0 +1,3 @@ +gust-wdg-silicon: boot 1 on STM32F100 (RCC_CSR=0x14000000, no prior WDG reset). Arming the REAL IWDG @0x40003000 via the dissolved wdg-thin driver (PR=5, RLR=0x123 ≈ 1.2 s)... +gust-wdg-silicon: armed (last KR write=0x0000, is_running=1). NOT refreshing — expect a HARDWARE reset in ~1.2 s, after which boot 2 reads IWDGRSTF=1. +gust-wdg-silicon OK: IWDG watchdog reset CONFIRMED on real STM32F100 silicon (RCC_CSR=0x34000000, IWDGRSTF=1) — the dissolved wdg-thin driver armed the hardware watchdog and it fired the reset. diff --git a/benches/gust/silicon/wdg-f100-run2.log b/benches/gust/silicon/wdg-f100-run2.log new file mode 100644 index 00000000..457de946 --- /dev/null +++ b/benches/gust/silicon/wdg-f100-run2.log @@ -0,0 +1,3 @@ +gust-wdg-silicon: boot 1 on STM32F100 (RCC_CSR=0x14000000, no prior WDG reset). Arming the REAL IWDG @0x40003000 via the dissolved wdg-thin driver (PR=5, RLR=0x123 ≈ 1.2 s)... +gust-wdg-silicon: armed (last KR write=0x0000, is_running=1). NOT refreshing — expect a HARDWARE reset in ~1.2 s, after which boot 2 reads IWDGRSTF=1. +gust-wdg-silicon OK: IWDG watchdog reset CONFIRMED on real STM32F100 silicon (RCC_CSR=0x34000000, IWDGRSTF=1) — the dissolved wdg-thin driver armed the hardware watchdog and it fired the reset.