docs(v0.5.0 E): claim accuracy — badges over drift-prone counts, RESULTS synth-0.49 provenance, D-split status

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

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._

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._

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._

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._

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._

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._

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._

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 <wasm> --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._

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._

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._

benches/gust/esp32c3/RESULTS.md

@@ -80,3 +80,10 @@ cat /dev/cu.usbmodem<N>          # the app re-prints the ratio in a loop
 
 Regenerate the dissolved object:
 `synth compile <stripped gust_mix>.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._

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._

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 <STLink VID:PID:serial>` 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._

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"