docs(silicon): withdraw the cannot-un-start claim from the wdg G474RE result - #230
Merged
Conversation
… result 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 <noreply@anthropic.com>
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
…IWDG on STM32F100 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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
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.
Found while a persona review panel audited the showcase video's claims against
docs/safety/verification-honesty.md. The panel's finding turned out to apply to the repo, not just the video.The defect
benches/gust/silicon/RESULTS-wdg-g474re.mdclaimed the silicon run:It does not.
gust_wdg_silicon.rsarms the watchdog and then simply stops refreshing it — it never attempts an un-start (grep -c 'wdg_(refresh|stop|disable)'on that firmware → 0). No rejection path was exercised on hardware.p2_cannot_un_startis a source-level Kani property over the pure FSM, and that is all it is.The correction
0x1c→0x3cand0x14→0x34) — we were under-claiming reproducibility while over-claiming the inference.Docs-only. No code, no artifacts, no rivet status changes.
🤖 Generated with Claude Code