Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 18 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,24 @@ tag: the USB `bcdDevice` build counter (bumped on every behavior change), and

## [Unreleased]

### Added

- **A status-only panel build (`--features panel`) for a screen board with no
touch.** It paints the device's own status — the build `bcdDevice`, the chip
serial, whether USB is attached, and uptime — on a plain 4-wire SPI LCD, and it
shows a **PRESS THE KEY** banner for as long as a user-presence wait is pending,
so the press the LED would blink for is named on the screen too. It adds no
presence source of its own: the BOOTSEL button still decides, the banner never
renders an operation or a relying party, and `shows_confirm()` stays false — this
is *not* the trusted display and every host ceremony is unchanged. The reference
board is ALIENTEK's RP2350A small-system board (1.14" ST7789V2, 240×135, on
SPI1). Panel wiring and SPI clock come from a board file's `[panel]` section,
defaulting to that board's pins (`cs`=9, `dc`=8, backlight=25 — active-low,
through the board's PNP high-side switch); SCK/MOSI on
GPIO10/11 are hard-wired. The feature is `dep:`-gated and mutually exclusive with
`display` (one geometry and one presence source per image), so a standard key is
unaffected. Build it `LED_KIND=none ... --features panel`. **`bcdDevice` → `0x09DB`.**

## [0.4.11] - 2026-09-08

The catch-up release, and the one where the instruments were audited harder than
Expand Down
6 changes: 3 additions & 3 deletions assurance/board/PLAT-TIMER-002.toml

Large diffs are not rendered by default.

4 changes: 2 additions & 2 deletions assurance/board/PLAT-TIMER-003.toml
Original file line number Diff line number Diff line change
Expand Up @@ -22,8 +22,8 @@
# INCONCLUSIVE, because a comparator whose counter has stopped can be observed
# neither to miss a match nor to make one.
assumption = "PLAT-TIMER-003"
method = """Take PLAT-TIMER-002's run -- a DEFAULT-image board powered and LEFT ALONE for at least 8589.934592 s with its LED recorded end to end -- and read the SAME series for a second question: did the render ever stop and stay stopped. TWO CONDITIONS THIS QUESTION ADDS TO THAT RUN, and neither is hygiene. NO DEBUGGER ATTACHED: TIMER0 carries a DBGPAUSE register whose own words are `Set bits high to enable pause when the corresponding debug ports are active`, so a probe that halts a core is a DOCUMENTED way to stop this very counter, and a run taken with one attached observes the probe instead of the silicon. AND A SUPPLY THAT DOES NOT DROP for the whole window: a brown-out reboots the board, and a reboot restarts the counter and repaints the render, which on the recording reads as a run that never froze. THE READING IS ARITHMETIC over the recording's own clock, the same clock that record locates its crossings by -- find the longest interval in which the sampled LED holds one value, and ask whether anything changed after it. Sample as that record says, ten frames a second or better and not the one frame a second the run's length makes tempting, for the same reason there and a sharper one here: a sampler near the ambient cadence aliases into a constant, and here that manufactures the FAIL out of an instrument that was too slow. THE DEVICE'S OWN CLOCK IS THE SECOND WITNESS, and for this row it is worth more than a date stamp. firmware/src/main.rs:800 stamps the origin at boot, immediately before the USB pull-up; firmware/src/usb_attach.rs:34-36 is the milliseconds since it, the clock the FIDO layer measures every window against; tools/rsk/audit.py:170 prints it as the `uptime` column. So a counter that stopped for an interval reports an uptime SHORTER than the wall-clock length of the recording, whether or not it restarted, and a board that rebooted reports one shorter still. Reading it costs a command, and a command inside the window is the traffic PLAT-TIMER-002 refuses, so it BRACKETS the run exactly as it does there, and THE CLOSING STEP IS A COMMAND THAT WRITES: enumerate, `rsk audit enable` (PIN and one touch) before the window opens, go quiet, then `rsk audit disable` -- or `rsk audit verify`, which additionally needs a provisioned OTP DEVK -- and only THEN `rsk audit log`. A READ-ONLY CLOSE CANNOT PRODUCE THIS ROW'S PASS AT ALL, and that is the defect this sentence carried until 2026-09-05. AUDIT_READ appends nothing (crates/rsk-fido/src/vendor.rs:481), so after a quiet window the newest entry is the PRE-WINDOW enable, its `uptime` is materially shorter than the recording ON A PERFECTLY HEALTHY BOARD, and the PASS below was unreachable by construction. The confound the witness exists to exclude was invisible in the same breath: `EV_BOOT` is appended lazily on the first journalled event of a power cycle (crates/rsk-fido/src/journal.rs:215-217), so a reboot inside a read-only window writes nothing and the exported window is byte-identical with and without one. MEASURED against this tree's journal code, on the host rather than on a board, with enable at 1000 ms and 8589935 ms of silence: read-only, newest `uptime` 1000 ms and the rebooted run byte-identical; closing with the write, 8590935 ms on the quiet run and, on the rebooted one, a SECOND `EV_BOOT` and 4294967 ms. On the charger arm there is no host to ask and no journal to read, and what stands in for the second witness is a supply that can be shown not to have dropped."""
boot_config = """PLAT-TIMER-002's, unchanged, because it is the same run on the same image: the DEFAULT build, firmware/src/main.rs:524's `embassy_rp::config::Config::default()`, and a stored `EF_LED_CONF` still at the factory look. The same three images are refused for the same reason and it is sharper here -- `LED_KIND=none` compiles no render task, brightness zero paints nothing, steady mode stops the frame changing while the alarms underneath it keep running -- and each of those is an image in which the LED holds one value for the whole run with the counter in perfect health, which is this row's FAIL signature exactly. A run on any of them observes an absent instrument and answers INCONCLUSIVE, never FAIL."""
method = """Take PLAT-TIMER-002's run -- a DEFAULT-image board powered and LEFT ALONE for at least 8589.934592 s with its LED recorded end to end -- and read the SAME series for a second question: did the render ever stop and stay stopped. TWO CONDITIONS THIS QUESTION ADDS TO THAT RUN, and neither is hygiene. NO DEBUGGER ATTACHED: TIMER0 carries a DBGPAUSE register whose own words are `Set bits high to enable pause when the corresponding debug ports are active`, so a probe that halts a core is a DOCUMENTED way to stop this very counter, and a run taken with one attached observes the probe instead of the silicon. AND A SUPPLY THAT DOES NOT DROP for the whole window: a brown-out reboots the board, and a reboot restarts the counter and repaints the render, which on the recording reads as a run that never froze. THE READING IS ARITHMETIC over the recording's own clock, the same clock that record locates its crossings by -- find the longest interval in which the sampled LED holds one value, and ask whether anything changed after it. Sample as that record says, ten frames a second or better and not the one frame a second the run's length makes tempting, for the same reason there and a sharper one here: a sampler near the ambient cadence aliases into a constant, and here that manufactures the FAIL out of an instrument that was too slow. THE DEVICE'S OWN CLOCK IS THE SECOND WITNESS, and for this row it is worth more than a date stamp. firmware/src/main.rs:849 stamps the origin at boot, immediately before the USB pull-up; firmware/src/usb_attach.rs:34-36 is the milliseconds since it, the clock the FIDO layer measures every window against; tools/rsk/audit.py:170 prints it as the `uptime` column. So a counter that stopped for an interval reports an uptime SHORTER than the wall-clock length of the recording, whether or not it restarted, and a board that rebooted reports one shorter still. Reading it costs a command, and a command inside the window is the traffic PLAT-TIMER-002 refuses, so it BRACKETS the run exactly as it does there, and THE CLOSING STEP IS A COMMAND THAT WRITES: enumerate, `rsk audit enable` (PIN and one touch) before the window opens, go quiet, then `rsk audit disable` -- or `rsk audit verify`, which additionally needs a provisioned OTP DEVK -- and only THEN `rsk audit log`. A READ-ONLY CLOSE CANNOT PRODUCE THIS ROW'S PASS AT ALL, and that is the defect this sentence carried until 2026-09-05. AUDIT_READ appends nothing (crates/rsk-fido/src/vendor.rs:481), so after a quiet window the newest entry is the PRE-WINDOW enable, its `uptime` is materially shorter than the recording ON A PERFECTLY HEALTHY BOARD, and the PASS below was unreachable by construction. The confound the witness exists to exclude was invisible in the same breath: `EV_BOOT` is appended lazily on the first journalled event of a power cycle (crates/rsk-fido/src/journal.rs:215-217), so a reboot inside a read-only window writes nothing and the exported window is byte-identical with and without one. MEASURED against this tree's journal code, on the host rather than on a board, with enable at 1000 ms and 8589935 ms of silence: read-only, newest `uptime` 1000 ms and the rebooted run byte-identical; closing with the write, 8590935 ms on the quiet run and, on the rebooted one, a SECOND `EV_BOOT` and 4294967 ms. On the charger arm there is no host to ask and no journal to read, and what stands in for the second witness is a supply that can be shown not to have dropped."""
boot_config = """PLAT-TIMER-002's, unchanged, because it is the same run on the same image: the DEFAULT build, firmware/src/main.rs:573's `embassy_rp::config::Config::default()`, and a stored `EF_LED_CONF` still at the factory look. The same three images are refused for the same reason and it is sharper here -- `LED_KIND=none` compiles no render task, brightness zero paints nothing, steady mode stops the frame changing while the alarms underneath it keep running -- and each of those is an image in which the LED holds one value for the whole run with the counter in perfect health, which is this row's FAIL signature exactly. A run on any of them observes an absent instrument and answers INCONCLUSIVE, never FAIL."""
expected = """The counter advances for the whole of a bounded window, and the render is what says so. PASS = the recorded series has NO interval in which the sampled LED takes one value and never changes again -- every quiet stretch is followed by more change, right up to the last sample -- AND, on the bracketed arm, the `uptime` of the entry THE CLOSING COMMAND APPENDED is not materially shorter than the wall-clock length of the recording and no second `EV_BOOT` stands in the window, which together rule out a reboot that repainted the render; on the charger arm a supply shown not to have dropped stands in for both. FAIL = the series stops changing and stays stopped to the end of the recording, with at least one full period, 4294.967296 s, recorded after it stops. That is a counter that quit: every task in the queue is waiting on an alarm that can no longer match, and the three properties this row supports -- `EveryOpQuiesces`, `EveryWaitReleases`, `EveryWalkCloses` -- are false of every operation in flight and of every one begun afterwards, each being an EVENTUALLY claim on a device where nothing is ever again. THE SECOND WITNESS IS OWED HERE TOO, and was not until 2026-09-05: this arm sat under a PASS carrying an uptime condition and carried none itself, while a FAIL REFUTES the statement (scripts/platform_gate.py:1337 maps `fail` to `refuted`). So a FAIL needs, beside the frozen series: on the bracketed arm a closing `uptime` materially shorter than the recording and no second `EV_BOOT` saying the board rebooted, and on the charger arm a supply shown not to have dropped. WITHOUT IT THE ARM IS SATISFIED BY A HALTED PROGRAM RATHER THAN A STOPPED COUNTER, which is the nearest thing this tree has to this row's own failure and is reachable in it: firmware/Cargo.toml:75 is `panic-halt = \"1\"` and nothing arms a watchdog reset anywhere -- `WATCHDOG` appears only as the scratch register firmware/src/pin_lock.rs:54 writes -- so a panicking render task freezes the frame for ever with the counter in perfect health. AND IF THE CLOSING COMMAND DOES NOT COME BACK, that is a reading rather than a gap: a stopped counter wedges everything that awaits a `Timer`, so a device that still ENUMERATES and will not answer the close answers this arm the same way a short `uptime` does. A device that does not enumerate at all is the INCONCLUSIVE arm below instead, because a halted core produces that too and nothing outside the device tells the two apart. INCONCLUSIVE, and every arm of it but the last is about the RUN. That matters because the last one IS about the configuration and could otherwise be read as this row forbidding its own PASS: it does not, because the image `boot_config` names takes none of these arms -- the shipped default compiles a render task, animates it out of the factory `EF_LED_CONF`, needs no debugger and no host, and so produces the PASS above on any supply that holds. The arms: a recording with a gap, since a stretch nobody watched cannot be shown to have been a stretch of change; the device does not enumerate after the window, which is the halted program's other half and an arm of its own rather than a note on the one above -- a panic takes USB down with the render, so the second witness is unreadable at exactly the moment the reading calls for it, and a frozen frame with no journal behind it does not tell a stopped counter from a stopped program; a freeze beginning inside the last period, which is PLAT-TIMER-002's stall and this row's failure with nothing yet to tell them apart; a debugger attached, since DBGPAUSE makes a halted core a documented way to stop this counter and the run would then be about the probe; a supply that dropped, or a SECOND `EV_BOOT` in the post-window journal, since a reboot repaints the render and reads as continued progress -- and it is that entry and not a short `uptime` that names a reboot, because a stopped counter shortens the `uptime` as well and THAT case is this row's FAIL above, not this arm; a recording sampled at or near the ambient cadence, which aliases into a held value; and an image or an LED configuration with no animation in it, which observes an absent instrument. WHAT THE SHARED RECORDING DOES NOT SETTLE HERE, said because a reader who has just read the other record will carry its verdict across. PLAT-TIMER-002's PASS is not this row's: it is satisfied by a counter that stops one second after the recording ends. PLAT-TIMER-002's FAIL is this row's PASS, since a stall that resumes is a counter that went on counting. Only the never-resuming stall is this row's FAIL, and it leaves that row INCONCLUSIVE rather than joining it."""
outcome = "planned"
board = ""
Expand Down
Loading
Loading