docs(silicon): withdraw the cannot-un-start claim from the wdg G474RE result

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

benches/gust/silicon/RESULTS-wdg-g474re.md

@@ -32,10 +32,25 @@ 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. (`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
+  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.

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 <extra -c args...>
+    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"

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.

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.