Conversation
…at all The model, its 44 mutants, floors.txt and the vacuity check were ratchets whose only puller was whoever remembered ./run-tlc.sh, on the one machine holding a jar at a hardcoded /nix/store path. The repo's own class: a check nobody watched go red. - nix/devshells.nix: tlaplus + jre8 join the pinned shell, which exports TLA2TOOLS_JAR. A gating tool belongs beside cargo-audit/deny/gitleaks; the 208 MB is the closure (the tool is 2.2 MB, the rest is the JDK it wraps) and the JDK is the point — java came from the host PATH before, so the prover's runtime differed per contributor. - formal/run-tlc.sh: the hardcoded jar path is gone; refuses with a clear message outside the shell. Tiers safety/liveness/all, drawn by heap: everything in safety runs at the 4g default, Liveness.cfg needs the 12g floors.txt gives it — and 11.1 GB is where the kani heavy runner already died twice. Tier membership lives in this file and nowhere else; 96 of 97 .cfg are covered, the one exception (Liveness_Full) documented. - deep-checks.yml: a weekly `formal` job running the safety tier, also fired by any push touching formal/ so a model edit is checked at once. set -o pipefail is load-bearing on the tee'd run line. Verified: the full safety tier on the pinned jar — 92 rows, 0 mismatches, exit 0, 24 min; Shipped/Fairness/Seams distinct-state counts byte-match the recorded baseline (the jar is sha256-identical to the hand-realized one, so floors.txt still describes the TLC that measured it). Four row breakages made and caught: unreadable jar, unset TLA2TOOLS_JAR, a floor raised above the measured count, a mutant switch flipped back to FALSE. actionlint clean; gate green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…oster assurance/properties.toml names every property TLC checks — 22 entries, 20 invariants and temporal properties across both modules plus the two maintainer-ruled accepted risks, so a ruled-away risk reads as a decision rather than a hole. Hand-written fields are only id, statement, source, status; scripts/assurance_gate.py derives the rest per run — defining module, checking cfgs, targeting mutants, Kani harnesses, fuzz targets, Rust files, device tests — and prints it. The worked example is why: a hand-written evidence record for the tree's best-documented property was wrong in three of six fields before any code existed. Both directions are closed: nothing TLC checks may be unregistered, nothing registered may be unchecked (which also catches a Solo_* mutant aimed at a ghost target), a status must equal the evidence ceiling — a Kani harness carrying the name forces BOUNDED, and PROVEN/OBSERVED are refused until the tree grows those evidence classes. Every formal/*.cfg must sit in a run-tlc.sh tier or carry a named exemption; run-tlc.sh gains --tiers (the kani.sh pattern) so the membership has one owner. assurance/crates.toml classifies all 26 workspace members — the ledger exists because two roadmap drafts enumerated crates from memory and missed four, including the second-largest in the tree. The derivation cross-checks against the recorded facts: SEC-FIDO-003 counts 7 targeting mutants, matching formal/README.md's table; the kani column matches the five property-named harnesses; and rust=1 on the touch invariant is a real signal — the name already lives in a presence.rs comment. New check.sh row `assurance registry`. Mutation table: scripts/test_assurance_gate.py, 19 cases — the first run of which caught the gate's own stale-exemption arm firing on a fixture without Liveness_Full.cfg, which is the arm working. pytest scripts: 294 passed; gate green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The traceability table's one all-zero column: no invariant name appeared in non-test Rust, so the model→code direction lived in formal/README.md prose alone. The 24 owner functions that page documents now carry a doc line — Refines `RSKeySecurityState!<Invariant>` — SEC-FIDO-NNN. — across rsk-fido and rsk-device/presence.rs, so one property greps both ways. Doc comments only: bcd_gate is line-aware and comments cannot reach the image, so no bcdDevice bump. assurance_gate.py validates every tag three ways (the module exists, the id is registered, the id↔invariant pairing matches — a copy-pasted tag naming one property by id and another by name is a finding, not two half-truths), refuses unregistered SEC-ids anywhere in production Rust, and ratchets the reverse direction: every invariant Shipped.cfg checks must be named in production Rust somewhere. That set is derived from the cfg, not kept by hand. Mutation table grows to 24 cases; the new ratchet proved falsifiable by breaking the old fixture on first contact. The tags shifted line numbers under ~175 of the model's file.rs:line citations; citation_gate caught 11 landing on blank lines, and the honest sweep was wider — every citation below an insertion point had silently slid one line. All 170 affected citations re-pointed by exact git-diff arithmetic rather than by the 11 findings; spot-checked that the re-pointed lines carry the code the model names. citation-gate: 351 citations resolve; pytest scripts 299 passed; gate green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
formal/ held 85 KB of analysis that did not exist from the outside: no SUMMARY.md entry pointed anywhere near it. docs/formal.md (Security section) is the map — the two modules, the checks-of-the-checks the matrix runs (mutants, floors, vacuity, the source lint), the property registry and the tags in code, how to run each tier and where CI runs them. The deep prose stays in formal/README.md next to the model; the page opens with what is NOT claimed and points at the measured formal-claims paragraph in Testing rather than restating it. docs.sh check: build OK, 0 broken links; gate green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…ects The TLC matrix proves the MODEL catches all 28 Bug* defects; nothing measured whether the code level catches the same ones. Three green checkers over three slightly different systems is the failure mode the whole formal apparatus exists for, and the difference between the two answers is an abstraction gap with a file and line attached. formal/comutants.toml: one entry per mutant — an exact-snippet patch (the defect, re-made in today's code; anchors fail loudly when the code moves), unreachable with the evidence a shipped fix made it so, or pending under a floor that only goes down. The target invariant is NOT recorded: comutate.py derives it from the mutant's own Solo_*.cfg, so this file cannot disagree with the matrix. scripts/comutate.py --lint is a check.sh row (closed world vs the Mut_*.cfg roster, anchors, floor); `run` applies each patch in a throwaway worktree — carrying the working-tree diff, so a gap closed by an uncommitted test reads killed before a commit — and demands the recorded verdict. Batch 1 measured, ten mutants: SEVEN KILLED (both write orders' guards, both unscoped cancels, wrong-PIN, setPIN-overwrite, stopUsing perms), TWO UNREACHABLE (0x08BF / eab4b5c, as the matrix already measured), ONE GAP CLOSED and ONE GAP RECORDED: - BugTokenSurvivesPinChange was a gap: changePIN leaving the in-RAM session token alive is caught by the model and was caught by NOTHING at the code level — the existing test covers the persistent pcmr grant through clear_ppuat, a different door. Closed with change_pin_revokes_the_session_token; re-measured killed. - BugDeleteRpBeforeCred stays a measured gap, recorded in the spec with the mechanism a killing harness needs (a mutating-op-budget tear over a sole-credential RP; Fs::delete interleaves a swallowed EF_META write with the backend remove). The harness is the next commit, not a rush. Mutation table: scripts/test_comutate.py, 13 cases, including the two traps the instrument caught in its own first runs — a HEAD worktree blind to uncommitted work, and the slice tail argument. comutate.py joins NAMED in test_gate_scripts.py. pytest scripts green; gate green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…tests Co-refutation's one remaining measured gap: the model's BugDeleteRpBeforeCred (NoUnmanageableCredential, RED at 111 503 states) swaps deleteCredential's order — decrement_rp ahead of the EF_CRED delete — and every host test stayed green. The registration twin is killed by a write-tearing harness; nothing tore a DELETE, and a write-only budget can never land between the two removes because Fs::delete interleaves a swallowed EF_META write with each backend remove. a_torn_delete_never_leaves_a_credential_without_its_rp closes it: TearMutatingAfter spends one budget on EVERY mutating op — write and remove both — and never recovers, a power cut rather than a blip. One credential on one RP, so decrement_rp takes its delete path; every budget in 0..8 tears the 0x06 flow at a different point, the medium is rebooted (fresh Fs, fresh caches, budget lifted), and the invariant is asserted exactly as the model states it: a live credential implies a live EF_RP record. Vacuity-guarded — some budget must produce a torn run, or the sweep proved nothing. Measured: green on the shipped order; the mutant order fails it at the tear between the two deletes. comutate run: 8 killed, 2 unreachable, 0 gaps, 0 verdicts differing from the record. Batch 1 closes with both of its measured gaps not recorded but killed. The test-side run() driver is generic over Storage now; existing callers infer RamStorage as before. Gate green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The 18 pending comutants are patches now and the floor is 0: every one of the model's 28 mutants either has its defect re-made in today's Rust, or carries the evidence a shipped fix made it unreachable. Full-roster verdicts, every one matching the record: 22 KILLED, 4 MEASURED GAPS, 2 UNREACHABLE — the first complete fidelity figure the model→code direction has carried. A kill must carry real test output now. The first BugPpuatIsAGate patch did not compile (EF_PAUTHTOKEN is a KeyFid, not a u16 match arm) and the old verdict logic scored the nonzero exit as killed — a broken patch masquerading as "the tests caught it". run_one tells a test failure from a compiler error: `build-broke` is its own verdict, never equal to any expect, so a patch that stops compiling fails the row loudly. Two fixture cases pin the distinction, including a stray "error:" line losing to a real "test result: FAILED". Re-measured with the patch fixed: a real kill, 3 tests down. The four gaps are recorded cargo-mutants-style — MISSED means "no unit test kills it", not "nothing does" — each with its mechanism and a filed harness: the two PIN-flow orders (clear_ppuat dropped, or reordered around store_new_pin) are observable only under a torn changePIN and no harness tears that flow; the warm-boot PinLock carry has no boot-path test; the torn-reset harness does not assert the live session drops before the flash work. Closing them is follow-on harness work with the mechanism already named, the same loop that closed batch 1's two. pytest scripts: 314 passed; gate green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The four measured gaps each get the harness their comutants.toml note filed, and every one re-measures killed: - change_pin_deletes_the_persistent_grant_record — §6.5.5.6 step 15's implementation IS the record's deletion (its presence is the grant), so the test asserts the deletion itself, not that the next mint differs (the sibling's property, which a re-seal satisfies through a different door). Kills BugChangePinKeepsPpuat, 5 tests down. - a_torn_change_pin_never_leaves_the_grant_under_the_new_pin — a mutating-op-budget tear over the changePIN flow: no tear point may leave a changed verifier with a live grant. The comparison reads the verifier region only — byte 0 is the retry budget, and the old-PIN verify spends and restores it before either record this property is about. Kills BugPinWriteBeforeRevoke with EXACTLY one failing test: the completed end state is identical either way, so the tear harness is the one instrument that can see the order. - a_torn_reset_never_leaves_the_session_running_on_a_wiped_seed — plants the RAM seed copy the way Ctx::load_keydev caches it and asserts it is gone at EVERY tear budget including 0, which is the E76 regression's exact shape. Kills BugStateResetAfterWipe. - a_warm_boot_carries_the_soft_lock_in — the first test to drive boot_state() with a live lock. Kills BugSoftLockLostOnWarmReset. Re-aiming the two PIN-flow mutants surfaced a finding of its own: the revoke is enforced TWICE — authoritatively inside write_pin_verifier (the run-37 fix moved it into the storage core) and redundantly in each caller — so the first single-layer patches measured the depth of that defence rather than a gap. The faithful mutants remove both layers; comutate grows a third anchor (find3) to move the revoke behind the write. Both notes record the redundancy. Test drivers run()/key_agreement() are generic over Storage now; the per-file tear-double convention holds (TearPinFlowAfter joins TearAfter, FailWriteAfter, TearMutatingAfter). Full roster: 26 killed with real test output on every one, 2 unreachable with evidence, zero verdicts differing from the record. pytest scripts 314 passed; gate green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The security model's PowerCut abstracts the store to per-record flags, so two questions one layer down were unaskable: can a torn delete leave metadata naming a file whose value is gone, and can the present-cache read a committed key as absent. Both are Fs contracts, both have shipped as defects (0x077C, audit run-36), and both are what the refinement pilot inducts its persistent envelope over (R0p) — so the store gets its own module, lifted from the Rust power-cut oracle beside the code. Three invariants, five mutants, each a shipped defect, each RED on the invariant that names it in both the full-set and Solo configurations; Store.cfg is GREEN exhaustive over 272 states with no dead action. The apparatus grew with it: run-tlc routes Store* to the module and tiers it, floors.txt carries its floor, the citation gate reads the new page (18 citations; a per-page floor so a tight model is not padded to clear the default), the registry gains SEC-STORE-001..003, the ledger flips rsk-fs and rsk-store to state-partial with the abstraction line named, four property tags land in fs.rs/powercut.rs, and the assurance gate learns StoreSolo_ so the mutant column cannot read 0 over five live mutants. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…closed comutate.py's closed world grows a second prefix: StoreMut_/StoreSolo_ join the roster (SeamMut_ stays out DELIBERATELY — the seam fixes carry their own YubiKey-measured regression tests, and their co-refutation is M4's; the exclusion is a stated plan in the docstring, not a glob accident). The lint went red on contact, demanding the five entries, which is its job. Each store-model defect re-injected into fs.rs reddens cargo test -p rsk-fs: the delete reorder and the present-bit meta gate fall to the power-cut oracle and the 0x077C regression tests, the fault-cache and truncated-scan mutants to the run-36 pair. The measurement surfaced ONE gap — the unknown-cache twin never drove a meta_add over an EF_META read that FAULTS, so the rebuilt-from- empty defect stayed green — closed in-session by a_faulted_ef_meta_read_never_rebuilds_the_blob_from_empty, re-measured killed with real test output. Roster now 31 patch + 2 unreachable, 0 gaps. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…he fourth module (M4) The seam module has the applets' status lifetime; it does not have the arithmetic behind establishing one. This module is that layer for the two applets that carry it — PIV's PIN/PUK and OpenPGP's PW1/PW3/RC: the finite counter behind each reference, the recovery reference that refills it, and the spend-refuse-refill rule that is identical at every one. It is the one applet surface with NO safe oracle — exhausting a real PUK ladder blocks the card and the only way back takes the keys — so the exhaustive check of every verify/block/recover interleaving runs here or nowhere. Three ghost invariants (the counter arithmetic erases its own history, so each is a fact about a step): NoAuthWhenBlocked, WrongAttemptIsCharged, BudgetRisesOnlyWithItsSecret. Three mutants, one per defended code site (the blocked floor, the pre-compare decrement, the recovery-secret check), each RED on its own target in full-set and Solo alike. Lattice.cfg is GREEN exhaustive over 243 states at depth 11 with no dead action — after TLC's deadlock check caught the first draft disabling a blocked card's VERIFY instead of answering it, which a locked-out card does. Scope stated, not implied: OATH/OTP codes are counter-less challenge- responses (the seam's exempt-refusal territory), PW3's admin path gates on a session (the seam's status), and LatMut_ stays out of co-refutation until the two-layer underflow analysis is done — all recorded in the ledger, the README and comutate.py's docstring. The apparatus grew by the M3 checklist: run-tlc routes Lat*, floors carry Lattice at 80, the citation gate reads the page (12 citations, floor 6), the registry gains SEC-LAT-001..003, and the assurance gate's solo-prefix tuple learns LatSolo_. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…EAM-006) The abstractions list carried this for two revisions: an unauthenticated OATH access-code removal is DEFINITIONALLY invisible to NoStatusOutsideItsSelection, because its oathCode exemption fires exactly when ~oathCodeSet — the very state the removal produces. Recorded rather than repaired, "because closing it needs a decision about what the exemption should say, not a switch". The decision turned out to be: change nothing about the exemption. The rule lives at the STEP — OathRemoveCode carries cmd_set_code's gate (crates/rsk-oath/src/lib.rs:356-358) as a Guard/Policy pair, and AccessCodeRemovalNeedsTheCode is its own recorder. Measured exactly as the two-revision-old diagnosis predicted: the action lands bit-identical at 662 distinct states (+48 transitions, every one into an already-reachable state), and BugRemoveCodeUnvalidated still falls RED in 77 — a violation no state predicate could ever have seen. All 26 seam configurations re-run RED on their own targets; the registry gains SEC-SEAM-006 and the rsk-oath ledger row discharges the promise that named this invariant. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…cue gate (M5) The surface above every applet: which applications EXIST (the USB_ENABLED mask), the always-on carve-out that keeps a disable reversible, and the operator-presence gate on the privileged rescue commands. A fifth module because it shares no variable with the other four, and because its central claim is a sequence property — no series of config writes can strand the device unable to re-enable an applet — which is about the mask's reachable space, not one write. Four invariants, four mutants, and TWO of the four rebuild defects that actually shipped: the pre-0x084A mask that was a DeviceInfo report while SELECT and dispatch never consulted it, and audit run-35's lock-code write whose empty stored record read back as SUPPORTED_CAPS and silently re-enabled everything the owner had disabled. The other two remove standing defences: the APPLET_CAPS cap-0 carve-out and rescue's require_presence. Admin.cfg is GREEN exhaustive over the mask's power set; every AdminSolo_ run is RED on its own target. All four are co-refuted — the first batch to measure 4/4 killed with no gap: the enforcement falls to the 0x084A regression pair, the carve-out to the_recovery_applets_can_never_be_disabled, the presence gate to the rescue suite's denied cases, and the run-35 merge to its own regression pair. The non-goals are stated where they are decided: the config write is modelled ungated because the default build ships it ungated (maintainer ruling, a documented reversible DoS), and the run-30 lock-code disclosure is one write's data handling, carried by its own unit test. Ledger: rsk-rescue and rsk-mgmt flip to state-partial; rsk-vendor and rsk-device name what M5 took and what remains. state-unmodelled is down to rsk-ui (M6) and rsk-usb (M8). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…sixth module (M6) WhatIsConfirmedIsWhatIsShown — the display build's whole reason to exist — had no model; the ledger carried it as rsk-display's named gap. This is the discharge, decomposed into the three rules TLC can hold, because the umbrella is a conjunction and a registered property nothing checks is what the registry refuses: an RP-naming operation completes only through the card that names it (the PIN pad's title is 'static, never RP data); a press that predates the card approves nothing (the controller reports level, not edges — the release edge is the whole defence, in two layers); and no exit but a deliberate Allow reads as Confirmed (Deny, sleep, timeout, cancel are all Cancelled). All three invariants are ghosts and the module says why: a completed ceremony leaves nothing on the glass, so no reachable state distinguishes a phished Confirmed from an honest one — the property lives at the step. Two of the three mutants are shipped display-build defects: run-28 F1 (built-in UV deleted the RP card) and run-33's pre-screen-touch class. Display.cfg is GREEN exhaustive over 5 states — the ceremony is modal, the space genuinely is that small, and the floor sits one under it because at this size the third-rule stops serving. All three co-refuted — the second consecutive zero-gap batch: run-28 F1 falls to its own three regressions, the ambient chokepoint to a_finger_already_down_is_not_a_tap_on_what_just_appeared (the ceremony's second edge recorded beside it), the zone collapse to a_deny_tap_is_a_real_decline and siblings. Ledger: rsk-display's promise discharged, rsk-ui flips to state-partial (hit_confirm is the modelled seam); state-unmodelled is down to rsk-usb alone (M8). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
… module (M7) firmware/ is the one workspace member with no host tests by construction — its checks run at build time and on hardware, nowhere in between — and the two machines at the reset line are the purest case of this tree's "model where you cannot measure" rule. The one-shot at-rest lap: EF_HARDENED says the scrub has run, the boot writes it only after compact() returns Ok (marker AFTER scrub, the same write-order family as the store's delete and the PIN flows' revoke), and every lazy re-key re-arms it — audit run-35 found four of five sites skipping exactly that. The scratch-word carry: a warm reset moves the WHOLE soft lock, because carrying the engaged flag without the mismatch batch lets a host stop one short and reboot — the budget laundered two attempts at a time. The security module owns the total drop; this module owns the partial one, which that mutant cannot express. Both invariants are structural — no viol ghost: a liar marker and a half- carried lock are states, not erased steps. Boot.cfg is GREEN exhaustive over 24 states; three mutants (one shipped at four sites, two removed defences), each RED on its target in full and Solo alike. Co-refutation is deliberately out and the exclusion is load-bearing: cargo test cannot reach firmware/, which is M7's point. The host-testable family got direct closure instead — the fido and PIV migration tests now pin EF_HARDENED cleared after a lazy re-key, each proved able to fail by removing its own site's re-arm in a worktree (the first probe removed the panel site by mistake and the fido test rightly stayed green — the asserts' specificity check, free). The panel and OATH/OpenPGP twins are recorded open in the README rather than implied. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…loses (M8) rsk-usb was the last workspace member no module covered. The frame reassembler is a genuine sequence machine — in_tx carries across the frames of a multi-frame message — and it is already unit-tested and fuzzed, which is exactly why it is worth modelling too: each of those exercises a single feed, or a fuzzer's random stream checked for no-panic. The security properties are not about one frame but about what an INTERLEAVING of channels can assemble: one host application's continuation never lands in another's message, an out-of-order frame aborts rather than fills the gap, and a declared length never overruns the buffer. Those are invariants over a transaction's reachable space that a per-frame test does not assert. Three mutants, each removing a real check (channel/seq/length), each RED on its target in full and Solo alike. Transport.cfg is GREEN exhaustive over 13 states; CTAPHID_INIT always resyncs so the graph never dead-ends. All three co-refuted — the third consecutive zero-gap batch: cont_wrong_cid_busy, wrong_seq_aborts and bcnt_too_large each catch their mutant in cargo test -p rsk-usb. With this the crate ledger has NO state-unmodelled member left: all 26 are modelled, modelled-in-part, pure, out-of-scope or embedded-binary. Phase 3 (M3 store, M4 retry lattice, M5 admin, M6 display, M7 boot, M8 transport) is complete — eight TLA+ modules, 41 registry properties, co-refutation at 41 patch + 2 unreachable / 0 gaps. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…against the model (phase 4) Everything before this kept model↔code fidelity by hand: citations name the code, mutants prove the model can catch defects, co-refutation proves the code level catches the same ones. None of it measured whether the code AS IT RUNS stays inside a model's behaviors. This is that empirical half, MongoDB-style, over the applet seams. The pipeline, each stage falsifiable. RECORD: formal/record-seam-trace.py drives a scripted CCID session against a live tools/emu and writes the wire-level events — the committed trace really was recorded, its 63C2 is the emulator's own retry counter answering a wrong PIN. MAP: scripts/trace_map.py turns events into model actions, deliberately STRICT (an unknown event, a strange status word, a verify off the selected applet are hard errors, never silent stutters — a mapper that skips what it does not understand is a checker that stopped checking); the one state it keeps is the selection, deciding Reselect vs SelectOther exactly as the Dispatcher's reselect flag does; a check.sh row holds the committed data module against the committed trace, and the mapper carries a 12-case mutation table. REPLAY: TraceSeams.tla forces the seam model through the recorded actions one position at a time, so a step the model refuses leaves no successor — a divergence is a TLC deadlock at the exact step; the committed session replays GREEN, 13 actions, invariants checked along the way. REFUSE: TraceSeamsBad.tla replays a hand-written session the model must reject (a key operation with no VERIFY behind it) and floors.txt requires that row RED — it deadlocks at step 2, the harness proven able to refuse. Both rows join the weekly safety tier. A green replay is evidence about the recorded sessions, not a proof about all runs — coverage grows by recording richer sessions, and regenerating is three documented commands. The spdx gate learns .jsonl as data (strict JSON has no comment to hold a header). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…asured
The roster put 31 of its first 43 patches in rsk-fido, rsk-device and rsk-fs.
rsk-piv, rsk-openpgp, rsk-oath and rsk-otp — 33 773 lines, and the subject of
four of the nine modules — held none, so "the applet models are green" was
fidelity nobody had measured. Each of the three exclusions was an argument:
that the seam fixes carry their own YubiKey-measured regressions, that a naive
lattice injection measures a u8 underflow, that the policy sites were a later
batch. The first turned out to be true of the fixes and silent about the rules.
19 of 24 were co-refuted on the first run. The five gaps:
BugSigPinNotSpent inc_sig_count clearing PW1 under the one-shot PW
status — no test ever wrote C4 = 00
BugPwStatusIgnoresAdmin put_pw_status own PW3 gate: the only session the
tests gave it was virgin, which the dispatch
refuses anyway, so the inner gate could be deleted
with everything still green
BugRemoveCodeUnvalidated the Rust half of SEC-SEAM-006. The model half was
closed two revisions ago; nothing held this one
BugRefusedValidateGrants a refused OATH VALIDATE that unlocks
BugRefusedValidateDropsUnlock and the same refusal dropping a standing unlock
Three regressions close all five, each re-measured killed with its mutant
applied and each failing on one assertion rather than taking a suite down. The
lattice patch is the both-layers shape the docstring asked for: rebinding left
to left.max(1) drops the floor and keeps the arithmetic under it in range, so
the slice fails on a blocked reference authenticating rather than on a panic.
The lint also gains a name-collision guard. Eight families share one roster key
space and roster() strips the prefix, so a reused bug name would have
overwritten an entry instead of colliding — both closed-world directions green
over a roster one mutant short. LiveMut_ and FairMut_ are now stated as excluded
rather than left to the glob that already excluded them.
Live roster: 67 entries, 65 executable patches killed, two unreachable, zero
gaps. Tests and tooling only; no firmware behaviour change, no bcdDevice bump.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Adversarial review of 44d9244 read the panic message behind every one of the 24 verdicts, and two of the patches turn out to model a different defect from the switch they are named after. A red run is not evidence until you know WHY it went red — the same failure as a green that proves nothing, wearing the opposite colour. BugPinFreshOutlivesPin deleted `self.pin_fresh = verified` from Session::set_pin, which is the INVERSE defect: that writer is the only one that ever sets freshness true, so the patch makes an ALWAYS slot permanently unusable. Fail-closed, where the switch is fail-open. All 11 failures read expected-9000-got-6982; not one was an operation that should have been refused succeeding. The faithful mutant is green, and the reason is the finding: pin_fresh has exactly one reader (auth.rs:64) and it is CONJOINED with the status it refines, so a freshness that outlives has_pin authorises nothing. Recorded unreachable with that evidence. BugCardResetKeepsStatus neutered the whole reset_card call, which also stops the SELECTION being dropped — and the only test that fell asserts the selection and never verifies a PIN. The faithful mutant (an empty applet slice, selection still taken) is green, because every route back to an applet after a card reset is a fresh select(reselect = false) and all three status-carrying applets re-lock there. Also unreachable, with the selection half named as what keeps that true. BugPwStatusIgnoresAdmin kept its verdict but not its meaning: it widened put_pw_status's inner PW3 gate, which the dispatch's write_authorized shadows, so the wire command still answered 6982. It now widens both layers, and put_data_c4_refuses_a_user_status drives the command so the outer gate is asserted too. BugAdminOpensKeyOps patched only PSO:CDS while its switch quantifies over pw1 and pw2; PSO:DECIPHER is now a second anchor, and the two sites this schema has no room for are named rather than left silent. Four line citations that had drifted are corrected, and two twin claims that carried no address now carry one. The guard shipped in that commit had a hole of its own, and it is the family the tree keeps meeting: prefix_collisions passed its own falsification while the three lines wiring it into lint() were covered by nothing. Delete them and the suite stays green over a roster one mutant short — and the weekly co-refutation job runs `run`, never pytest, so there the wiring is the only protection. Both guards are now driven through lint() by a test. The Solo half of the closed world gets its own: a <Family>Solo_<Bug>.cfg with no mutant of that family steals the invariant that mutant is judged by, and roster() cannot see it because the stem matches no Mut_ prefix. Full roster re-measured end to end: 67 entries, 63 executable patches killed, four unreachable with recorded evidence, zero gaps. Phase 2 unchanged at 26/28. Tests, tooling and docs only; no firmware behaviour change, no bcdDevice bump. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Both are one layer out from rules the file already states, and both are where those rules actually failed this week. "Never report unverified success" covered a green that proves nothing and said nothing about a RED that proves nothing. Two of 24 co-refutation patches modelled the inverse of their defect and scored a kill for it; the verdict column looked perfect, and the tell was only in the panic messages — every failure said "should have succeeded" and none said "should have been refused". "A guard's mutation table goes in the diff" was satisfied by a guard whose three lines of wiring into the gate were covered by nothing: delete them and the suite stays green, and the weekly rows that call a script rather than pytest lose their only protection. Falsify the ROW, not just the helper. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
BugAdminOpensKeyOps is quantified over PW1 and PW2 and its comment names PSO:CDS, PSO:DECIPHER and INTERNAL AUTHENTICATE; the AES PSO arm follows them by the tree's own decision. The entry patched PSO:CDS, then two, and named the rest in prose — honest, and still a quarter of the switch measured by an entry that read as covering it. The limit was never the three-anchor cap: the four gates sit in two files, and an entry held one `file`. So entries gain a `[[comutant.X.site]]` array — file, find, replace per site — with the flat form untouched for the 62 entries that are one file. `run_one` groups by file, counting every anchor before applying any. Numbered anchors lose their ceiling with it. Lifting a cap creates the holes the cap made impossible, so the guard ships in the same diff and is falsified through `lint()`, not through its own function: a `find3` written without a `find2` (the walk stops at the first gap), a `replace2` whose `find2` was renamed away (edits nothing), an entry carrying both forms (the flat half never applies), and a site with no file. The `[[site]]` feature gets its own falsification too — a slice green only when BOTH files are patched, plus the one-site variant that must come back killed, so the test can tell two patched files from one. Measured after: each of the four gates is killed ALONE (2/1/1/1 failing tests), so no site rides on a sibling's coverage. The combined run shows two failures rather than five because the same matrix tests span several gates — worth recording, since the first read of that number looked like two unasserted sites. Roster unchanged at 67 entries, 63 patches, four unreachable. Tests and tooling only; no firmware behaviour change, no bcdDevice bump. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`floors.txt` asks whether a run got smaller. Nothing asked the question one level out: is the scope it ran over big enough to express the defect its own mutants rebuild? A configuration can sit far above its floor, fire every action and still be blind, because the blindness is in the CONSTANTS. Measured, and it is not hypothetical. `BugCmWalkIgnoresChannel` explores 43 M+ distinct states at one CTAPHID channel without a counterexample and falls at two; `BugContIgnoresChannel` is the same shape at the reassembler. Both would have stayed green over a live defect if their domain were narrowed to a singleton, and nothing stopped that — the transport's `Channels` and the admin `Caps` were literals inside their modules, so no configuration could state the scope it ran at. Both are CONSTANTS now, emitted by `gen-configs.sh`, and every recorded count is unchanged. `formal/scopes.txt` records two hand-written columns per constant: the measured minimum, and THE INVARIANT IT WAS MEASURED AGAINST. The second is load-bearing — a minimum only binds configurations that check that invariant. `Fairness.cfg` sits in the safety tier, runs one channel deliberately and checks `OpAdvancesIsOneActivity`; holding it to a number measured on `NoAuthorizationBypass` would be a red for the wrong reason, and a gate that cries there gets deleted. Everything else is derived by `scripts/scope_gate.py` — which constants exist, which module owns a configuration, what each assigns — because a hand-kept copy of a derivable fact is the rot this tree has paid for twice. The same profile says something unflattering: every one of the thirty security configurations fires with a SINGLE relying party, including both registration-order mutants, against a module comment asking for two. The record says 1 rather than repeating the claim. Above two nothing probes at all, so a minimum equal to the shipped value means "nothing here looks higher", never "higher is safe". And the same pass answers the largest standing caveat on this model. The FIDO security state ran `MaxRetries` 3 : `MismatchLimit` 2 against a shipped 8 : 3, recorded as "an argument, not a proof". `SYMMETRY` closes it: relying parties and channels are interchangeable — no action, invariant or initial state names one — so TLC may quotient by `Permutations`, which takes the reduced-constant run from 61 215 504 distinct states to 25 829 584. The firmware's own constants then cost 48 679 968, FEWER than the reduced scope explored before, GREEN and exhaustive at depth 55 in 539 s, with all 28 mutants and both historical configurations still RED on their own invariant. Safety configurations only: TLC's liveness check is not sound under symmetry, so `Liveness*` and `Fairness*` keep their smaller constants. `Shipped.cfg`'s floor does not move — 20 000 000 is still under the measurement and stricter than the near-a-third rule. Falsified through the row, not the function: narrowing `Fids` in a throwaway worktree makes `./scripts/check.sh` exit 1 at `== formal scopes ==`. The guard carries a 21-case mutation table, and the cases that must NOT fire are the half that matters — a scope gate that reddened the liveness tier for running one relying party on purpose would be gone within a week. Two traps worth carrying. A temporary configuration must keep its family prefix: `run-tlc.sh`'s `spec_for` falls through to `RSKeySecurityState` for anything else, and a wrong-module run reports RED for an unassigned constant — the first pass of this probe read RED on every row for that reason. And the printed DEPTH is nondeterministic: `Transport.cfg` gave 4, 5, 4 on three identical runs with states and distinct stable, so a scope record must ratchet `distinct` and never `depth`. Model and tooling only, no firmware behaviour change. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Found by running co-refutation BACKWARDS for the first time. The existing direction asks whether the code level catches what the model catches — 63 patches, all killed. It had never asked the reverse, which is the question the pair's fidelity actually turns on: does the model catch what the code level misses? The instrument is mechanical — `cargo-mutants`' MISSED set, intersected with the lines the model ITSELF cites, is a list of code the model claims to describe and nothing tests. First batch, over the reassembler and the store: 394 mutants, 88 MISSED, 12 on a cited line. Twelve split three ways, and the split is the point — one equivalent (`|` and `^` agree on disjoint bits), two fail-safe (a stricter length bound; cleared `decided` bits send more reads to the reliable backend), and nine model-blind. The sharpest was worth the exercise on its own. `Fs::meta_add_reserve` refuses a FAILED EF_META read and the model carries that as `BugMetaAddDropsOnFault`; its sibling `Fs::meta_delete` has the identical guard, and NOTHING HELD IT AT EITHER LEVEL. No test killed it, and `MetaDelete` was modelled as an unconditional single write with no read to fail. Worse than a lost delete: the defect caches EF_META as *absent*, and the next `meta_add` legitimately trusts `known_absent` and rebuilds the blob from empty, so the records go on the write AFTER the defect. That is why `NoFalseMetaAbsent` (SEC-STORE-004) is a step recorder — once the cache has lied, the losing write is correct code and no state predicate over `meta` can tell the two apart. Closed at both levels in one pass. The model gains `metaAbsent`, the fault disjunct and the invariant: `Store.cfg` 272 → 364 distinct, still GREEN and exhaustive, `StoreMut_BugMetaDeleteDropsOnFault` RED in 57, and the co-refutation patch measures `killed`. `a_faulted_ef_meta_read_never_caches_the_blob_as_absent` closes the Rust half, proved by driving the real mutation — exactly one test fails, and on the assertion that names the defect rather than its inverse. The other five model-blind rows are closed as TEST gaps, not model gaps, and the distinction is deliberate: the dynamic-file registry is the capacity budget's bookkeeping and `factory_wipe`'s 64-key batching is a loop bound, neither of which `RSKeyStore` carries or should. Four tests own them, each proved by driving its real mutation with the whole suite watched — six for six, exactly one failure each, always the intended test. One of those six came back SURVIVED on the first attempt, and the test was mine. `retain(|f| f != fid)` inverted keeps exactly one entry too — just the WRONG one — so an assertion on `free_dynamic()`'s count held while the registry listed a deleted key and had dropped a live one. Re-writing the survivor is what separates them. A count is not an identity: when a mutation permutes rather than resizes, only driving it says the test cannot fail. The tree as shipped is correct throughout; this closes the holes that would have let a regression through unseen. No firmware behaviour change. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Four textual conflicts, resolved by hand; everything under `crates/rsk-ui/render` merged clean because `develop` never touched it -- its seven display commits went to the seam and presence plumbing, and the PR owns render/font/aa. - `bcdDevice`: ours 0x097D plus an incoming firmware-behaviour change is 0x097E, and the CHANGELOG stamp moves with it. The incoming entry claimed 0x095B, which was 0x095A+1 off `main` -- the same number our own OpenPGP entry already carries. - `check.sh`: both rows survive. `crate graph` was ours, `IBM Plex font data` is the PR's, and neither replaces the other. - `CHANGELOG.md`: `### Changed` is ordered newest-first, so the display entry goes to the top of the section rather than where the diff happened to land it. - `third_party/README.md`: not cosmetic. The old text closed with "these suites are never compiled or linked into the firmware, so the GPL/AGPL split does not interact with RS-Key's own build" -- and `ibm-plex/font_data.rs` IS linked in. "Two unrelated kinds" is three now, and the third bullet says what the other two do not: this one reaches the image, under OFL-1.1. Verified by content, not by "it built": `rsk_sdk::Rng` / `RsaKey` from the seam refactor are still there, the SEC-DISP-003 refinement comment survived, and all 23 formal citations into rsk-ui/rsk-display point above the PR's first hunk (its earliest change to display/lib.rs is line 208; the citations are 190 and 248), so none of them shifted. `crate_graph.py --check` still reads 28 crates / 100 edges -- `u8g2-fonts` was an external crate, not a workspace member. `nix develop -c ./scripts/check.sh`: ALL CHECKS PASSED. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…have The trusted display composites text per pixel: for every pixel of a run's bounding box it walks the string and asks each glyph what it covers there. A pixel both glyphs cover kept whichever it read LAST, so a following glyph's faint fringe overwrote a preceding glyph's solid stroke -- the wrong direction, and visible as a near-background speck punched into a light stroke. Glyph boxes really do overlap: of the 97 in the atlas, 8 have a negative left bearing and 28 carry ink past their advance. Sweeping all 97x97 pairs in all seven roles over the committed coverage tables, 53 pairs composite differently under "later" than under "greater". The worst are `\j` and `(j` in Heading at a delta of 13 of the 15 coverage steps -- an all-but-solid pixel replaced by an all-but- background one. Heading and Strong render the service name on the approve prompt, so the pair is attacker-choosable; the artefact is cosmetic, but nothing about it should be reachable from the other side of the USB cable. The regression is a property, not a golden pixel, so it outlives the atlas: render the prefix, render the pair, and assert no pixel got LIGHTER. White on black, so the green channel is the coverage. Driven red before the fix, and it fell on the right assertion in the right direction -- `Heading "\j"`, pixel (27, 49), 63 alone and 8 with the `j` added. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…an error type The PIN title scrolls by compositing into an off-screen four-bit band, and `BandCoverage::encode` recovered each pixel's coverage by inverting the blend -- searching the TEXT/PANEL_BG ramp for the value that produces the colour drawn. A colour off that ramp had no answer, so `encode` returned `Err`, the `?` in `draw_iter` propagated it out of `render_pin_title`, and `render_marquee_frame` answered by filling the buffer with zeros: one unexpected pixel and the entire title is gone from the band. Nothing triggers it today -- the title renderer emits exactly those two colours -- which is the whole problem with leaving it there. It is a fail-CLOSED path on a screen whose job is to say which PIN the host is asking for, guarded by nothing but the current palette of a renderer one crate away. The 1-bit mask this replaced did not have the failure mode, because it took the tolerant rule: a pixel that is not the background is a glyph. That rule is back -- off the ramp means full coverage -- and with no way left to fail, the target's error type is `Infallible` again. That deletes the blanking branch instead of repairing it, and a `const _` assertion on the associated type keeps a future edit from reintroducing an error path. Both drove red first: the runtime test could not even `unwrap` the write, and the type assertion failed to compile. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…tion table `check.sh` gained `run "IBM Plex font data" python scripts/generate_ui_fonts.py --check` with PR #88, and nothing in `scripts/` knew about it. `test_gate_scripts.py` collects tables by the `*_gate.py` glob plus a `NAMED` map, and `NAMED` already carries `crate_graph.py` under the comment "a generator whose `--check` mode is the gate row" -- the exact shape this is. So the whole check could have been deleted with the suite green, which is the hole five previous guards shipped with, one file over each time. Twelve cases, every one driven as a subprocess against the real script with `--check`, the way `check.sh` spells it -- not against `generated_text()` behind it. Falsifying a guard through its own function is what leaves the wiring untested, and the wiring is what breaks. The generator runs in 0.23 s, so nothing is bought by faking it. The table covers both halves of the tie, which matters more here than the count: a hand-edited coverage byte, glyph record, deleted role, edited font digest and deleted file are the committed side; a changed `CHARS` in the generator is the other side, and without that case the row would only prove the file cannot be edited, not that it still describes what the generator would emit today. Plus the two environment refusals (`IBM_PLEX_SANS_DIR` unset, a font dir with no files), which must fail loudly rather than pass quietly, and the clean-copy control so a fixture that is already red cannot pass the rest by accident. Proved to have teeth, not just to be green: with `--check`'s comparison replaced by `if False`, 6 of the 12 fail, each on the returncode and message it names. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…at render them `generate_ui_fonts.py` recorded a sha256 of each IBM Plex file, which is half the input. FreeType rasterises the outlines and Raqm lays them out, and either one moving rewrites every table in the file with nothing in the diff to say so -- the row simply goes red one day, after a nixpkgs bump nobody connects to it. Both versions are in the generated header now, so the red row carries its own diagnosis. The engine is pinned, not defaulted, and that half is not bookkeeping. Pillow selects Raqm when libraqm is present and FreeType's own layout when it is not, and the two do not agree: measured on this pin, forcing BASIC moves two advances in the 30 px face -- `f` and the middle dot, 10 px against 11. So a Pillow built without libraqm would have quietly produced a different atlas and a red row on an unrelated machine. The generator now names `Layout.RAQM` and refuses the run outright when libraqm is absent, rather than laying the glyphs out with something else. The tables are byte-identical -- one added comment line is the whole diff -- which is what says Raqm was already the effective engine, so this pins the status quo rather than changing it. No bump: a comment cannot reach the image, and `bcd_gate.py` agrees. The mutation table gains the case that makes the record worth keeping: editing the version line has to make the row stale, or recording it is decoration. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The antialiasing change replaced the rename keypad's `␣` with the word "SPACE", and it had to: the generated coverage tables cover ASCII plus the em dash and the middle dot, so U+2423 OPEN BOX would have drawn as `?`. A word on a key sized for one glyph is the wrong end to fix -- the atlas is the thing that was short. So the atlas carries the character now (98 entries), the key is a symbol again, and the cost is measured rather than guessed: 493 bytes, 409 of coverage and seven glyph records, against the 42 KB the tables already occupy in the display flavor. The assertion that came with the substitution -- "T9 key labels must use glyphs from the ASCII font atlas" -- was the right question with the wrong rule, and it would have refused this fix. The atlas is not ASCII; it is ASCII plus three. It moves to `font_tests.rs`, where the index is reachable, and asks the atlas directly: every character of every label must resolve to its own glyph rather than to the `?` fallback. Driven red by pointing the key at U+2192, which is not in the atlas. Not done here, deliberately: U+2026 for the truncation marker. It would cost one more glyph and read better in prose, but the marker's job on the approve screen is to be NOTICED -- it is what tells the owner the domain shown is not the whole domain -- and a single narrow ellipsis is less visible at 13 px than three full-width periods. The head-ellipsis case is the anti-phishing one; the marker stays `...`. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…'s build `rsk-emu --screenshots docs/images` re-renders all sixteen. Two of them move, and both for the same reason: the Firmware page and the Settings row that leads to it print `bcdDevice`, and the committed copies said 0x095b. The emulator derives that number from `firmware/src/main.rs` at compile time, so a screenshot is stale the moment the counter is, and this one had been stale for a while -- the copies on `develop` before the merge said 0x0875 against a firmware at 0x097D, which is 264 bumps of drift on a page whose entire job is to tell the owner which build is on the key. The other fourteen are byte-identical, which is worth recording: the four commits since the merge changed the atlas, the compositing rule and the marquee's error type, and none of them altered a pixel of the documented screens. The 53 glyph pairs the overlap fix repairs are combinations these demo strings do not contain -- the fix is held by its property test, not by these images. Not gated, unlike `crate-graph.svg` and the font tables: a screenshot row would have to compare pixels rather than PNG bytes, or a libpng bump reds it. Left as a note rather than done here. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…id so
`1881e93` asserted the band target's error type with a `const _: () = { fn
infallible<..>() {} fn assert() { .. } }`. The bound was genuinely checked -- a
function body type-checks whether or not anything calls it, and it did fail to compile
before that commit -- but neither function is ever *used*, and `clippy --all-targets
-- -D warnings` is a `check.sh` row: `error: function `assert` is never used`.
So `1881e93` does not pass the gate on its own. Recorded rather than amended: it is
the same mistake as taking an exit code through a pipe, one layer over -- I proved the
assertion could go red and did not prove the row stayed green, and running only
`cargo test -p rsk-display` is what let it through.
It is a `#[test]` now, which is what a test file wanted anyway: nothing is dead, the
bound is still resolved at compile time, and the check reads where the other three
band tests read.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`e5b0cab` added a bare `import PIL` next to the existing `from PIL import ...`
solely to read `PIL.__version__` for the generated header. `features.version("pil")`
returns the same string through the module the script already imports, so the second
import goes and every version in that header -- Pillow, FreeType, Raqm -- now comes
from one API. The generated file is unchanged, header included.
Worth recording because the line did go red once, and NOT for this reason. A gate run
failed the row with `ModuleNotFoundError: No module named 'PIL'` at that import while
every other python row in the same run passed. The cause is environmental, not the
import form: in this devshell `python` is the bare interpreter and packages arrive on
`PYTHONPATH`, where all the individually-listed ones (cryptography, fido2, pyscard,
click, ...) have their own store paths and **Pillow exists only inside the
`python3-…-env` entry**. The font row is the first row in `check.sh` that needs that
entry, so it is the first to notice when it is not there. `from PIL import ...` would
have failed identically -- this commit does not fix that, and nothing here should be
read as if it did. Not reproducible since; the store path is present again.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…er anything runs it
`test_every_gate_is_run_by_check_sh` iterates `GATES` -- the `*_gate.py` glob. The
`NAMED` half got two properties, "a table exists" and "the guard still exists", and
not the one that matters most: that something invokes it. So a `NAMED` entry could
arrive with a table, a file, and nothing running it, and this file would stay green.
Three tables paper over it today with their own `test_check_sh_runs_the_row`
(`crate_graph`, `security_trace`, `generate_ui_fonts`), which is the property asserted
by convention, one guard at a time -- and one guard at a time is exactly how the
fourth arrives without one. They stay: a name match cannot pin a row's flags, and
losing `--check` off the font row is a real way for it to go quiet.
The reason this is not a one-line loop over `NAMED`: **these guards are not wired in
the same place.** `impact.py` is a pre-commit hook, `kani.sh` is a `ci.yml` step,
`run-tlc.sh` is a weekly `deep-checks.yml` row, and `gen-configs.sh` is run by another
guard (`config_gen_gate.py` re-runs it -- that guard IS its runner). Five are
`check.sh` rows. So `NAMED`'s value is a pair now, (table, runner), and each guard is
asserted to appear in the runner it claims.
And it has to read code, not prose. `check.sh` names `run-tlc.sh` and `kani.sh` in
comments while running neither, so a substring rule over the whole file would have
been satisfied by the very sentences explaining that check.sh does not run them --
the same shape as `kani_gate.py` counting a commented-out invocation as live, and its
prefix-only repair still passing `true # cargo …`. Lines are cut at the first `#`,
which refuses both, and a unit case pins that: an invocation counts, a comment does
not, a trailing-comment invocation does not.
Mutation table, each driven and each killing exactly its own assertion:
M1 the font row deleted from check.sh -> ...is_run_by_its_stated_runner
M2 the same row COMMENTED OUT -> ...is_run_by_its_stated_runner
M3 a runner path that does not exist -> ...named_runners_still_exist
M4 kani.sh claimed as a check.sh row -> ...is_run_by_its_stated_runner
M5 both kani.sh steps cut from ci.yml -> ...is_run_by_its_stated_runner
M2 is the one worth keeping: a naive substring rule passes it. M4 is the proof the
runner column is not bookkeeping -- claiming the wrong runner for a guard that IS
wired in elsewhere still goes red. M3 first killed two tests with one cause, the
wiring test dying on a traceback rather than a sentence; it skips a runner that is
absent now, so that cause has one owner and one message.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Issue #89 asked for PIN complexity enforcement. Most of it already ships behind `strong-pin` / `fips-profile` -- a six-code-point floor, `pinComplexityPolicy` advertised in getInfo, enforced on both the host setPIN path and the trusted-display pad. What it actually checked was narrower than the docs made it sound: one repeated code point, and a +/-1 run. `121212`, `123123` and `112211` were accepted. Four rules now, and the first subsumes the old one: periodic some prefix of length p <= n/2 repeated fills the PIN. p == 1 IS the old repeated-code-point rule; p > 1 is what it missed, and it does not need p to divide n, so `12121` goes too. +/-1 run unchanged, both directions. <= 2 distinct NOT a length argument. Two symbols leave two smudges on the glass, and what an onlooker or a fingerprint leaves is then the orderings of two marks, however long the PIN. Directly the threat #90 is about, one layer up. denylist ten shapes the three rules cannot express: 3x3 keypad lines and diagonals, where the smudge pattern IS the PIN, and the mirror/stutter/Fibonacci runs people reach for when told "not 123456". Six code points each -- the floor here is six, so a four-digit entry could never be reached to be refused. The scoring scheme the issue proposed is deliberately NOT what landed. `score = length(pin)` minus per-pattern penalties makes length buy off a pattern, and the arithmetic inverts at eight: `12345678` scores 8-4=4 and is ACCEPTED, `123456789` scores 5 and is ACCEPTED, while `1234` and `123456` are correctly refused. Adopting it would have been a REGRESSION against what already shipped, which refuses a +/-1 run at any length. A pattern has to be disqualifying regardless of length, because its search space does not grow with it; length may only buy off the absence of a pattern. Every rule reads code points, not bytes. The floor next door counts code points (getInfo 0x0D) and the old check counted bytes, so a repeated multi-byte character (`АААААА`) passed a rule written to refuse exactly that. Not-UTF-8 is refused rather than measured, the same call the host path makes one step earlier. Verified in both directions: seven families driven through the real setPIN request (a rule the request path never reaches refuses nothing), and a boundary test for what must still be ACCEPTED -- three distinct code points is enough, `135790` and the display suite's own `481629` still pass -- without which the rule could simply be `true`.⚠️ `cargo test -p rsk-fido --features strong-pin` fails 61 tests ON HEAD, before this change, and 61 after: the suite sets `1234` throughout and was written for the default four-code-point floor. CI builds the flavor and tests it nowhere. Left alone here -- it is a separate change with its own diff -- but it means this policy's own regression tests are the only ones that ever run under the feature that enables it. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Issue #90. Settings -> Security -> "Scramble PIN pad", OFF by default. On, the ten digit keys are ordered at random for each PIN entry -- and again between the "New PIN" and "Confirm PIN" steps, since each is its own entry -- so a fingerprint trail, a worn patch of glass, or an onlooker who sees the hand but not the panel learns nothing from WHERE the taps landed. What it does not do is in the guide, because the issue got it wrong: it buys **nothing against a screen recording**. Anyone who can see the panel reads the digits off it. The threat it answers is the one the issue's own first sentence names -- smudges and touch traces -- and the panel already offers a bigger exposure to a camera than the layout ever was (the reveal eye prints the typed digits). Off by default, and that is not timidity. Scrambling costs muscle memory: entry is slower and mistyping likelier, against `PIN_MISMATCH_LIMIT` = three wrong PINs per power cycle before the key demands a physical replug. Spending someone's retry budget is not a default a firmware gets to pick for them. One `PinLayout` value paints the labels AND answers the hit-test. Making it a value rather than two tables is the whole design: a pad drawn in one order and tapped in another types digits nobody pressed, and nothing on the screen would look wrong. The regression asserts exactly that over both the identity and shuffled layouts, and was driven red by pointing `hit_pin` at a second layout -- "cell (1,0) paints one key and taps another". The order is Fisher-Yates with **rejection sampling**, not `% 10`. A bare modulo over a byte favours the low digits by up to 6/256, and a pad whose `1` sits top-left more often than it should leaks a little of what it exists to hide. Nine swaps draw from 32 bytes; exhausting that needs 23 consecutive rejections (p < 1e-38) and leaves the rest unswapped rather than reusing a byte. The setting rides a spare bit of `EF_DISPLAY`'s EXISTING flags byte, so the record does not grow: a device provisioned before this -- including one carrying the original flags-less three-byte block -- loads with scrambling off, which is right, because a firmware upgrade is not the owner asking for it. Tests pin both directions of that. Seven Security rows did not fit at the old 36px pitch (the last row's bottom lands at 352 on a 320px panel) and the compile-time layout assert is what refused it, not a runtime clip. Rows are 32px with a 4px gap now; the page was rendered and read before and after. Also: `tools/emu` is a detached workspace, and `cargo check` on it without `--all-targets` misses its test targets -- two `hit_pin` call sites there failed the gate after a "clean" local check. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`cargo test -p rsk-fido --features strong-pin` failed 61 of its cases, and had for as
long as the feature existed. `--features fips-profile` failed 63. Nothing was broken in
the firmware: the suite typed `1234` almost everywhere, which is fine under CTAP's
four-code-point floor and refused twice over under those profiles -- too short, and a
+/-1 run -- so every case that set a PIN died on `PinPolicyViolation`.
Nothing had ever run them. `ci.yml`'s `flavors (strong-pin, ...)` rows only BUILD the
flavour, and `scripts/check.sh` tests the default feature set, so the shipped
`firmware-strong-pin` / `firmware-fips` images had no behavioural coverage beyond the
handful of `#[cfg(feature = ...)]` cases written for them by hand. The recorded family
is "a check nobody has watched go red"; this is its mirror.
default 610 passed / 0 failed (unchanged)
strong-pin 551 / 61 -> 614 / 0
fips-profile 544 / 63 -> 605 / 2
The two left under fips (`vendor::tests::an_unsupported_protocol_is_judged_before_the_
missing_token`, `a_gated_subcommand_spends_the_mse_channel`) fail on HEAD as well,
touch no PIN, and are a separate finding.
`test_pins.rs` holds four values that clear the strictest profile's every rule -- six
code points, no period, no run, six distinct digits, off the denylist -- and they are
the values `rsk-display`'s tests already use, so one vocabulary spans both crates. A
test whose SUBJECT is a refused PIN keeps its literal, with a comment saying so.
Three places where the sweep would have made a test pass for the wrong reason, which is
worse than the red it replaced:
* `store_local_pin_enforces_min_length` and `fips_min_pin_floor_is_six` ARE the short
PIN. Neither sits under `cfg(strong-pin)` -- the second is gated on `fips-profile` --
so filtering by that one attribute did not protect them.
* `UvPad::typing(b"0000")` is refused for its LENGTH under these profiles, not for
being wrong, so the retry it exists to burn was never spent. `WRONG_PIN` is the same
length as `PIN` and differs in one digit.
* a `change_pin_req` swept without its paired `get_token_req` changes the PIN and then
asks for a token with the old one.
And the length lives next to the literal in two shapes, not one: `padded[..4]
.copy_from_slice(...)` AND the `PinEntry::Entered(4)` a mock pad reports. Fixing only
the first made the pad type six bytes while claiming four, and took three cases in the
DEFAULT profile with it -- the profile that was green before I touched anything.
Not done here, deliberately: no row runs these. Measured from a warm build, a
`strong-pin` test row costs 6.5 s and a `fips` one 1.4 s against a ~20 minute gate, so
the case for `check.sh` over the weekly matrix is strong -- but the gate is the
maintainer's, and a row of mine would arrive without their say-so and without the
mutation table this repo asks of one.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…tright
`vendor::tests::a_gated_subcommand_spends_the_mse_channel` and
`an_unsupported_protocol_is_judged_before_the_missing_token` failed under
`--features fips-profile`, and had since the profile existed. Neither is about seed
export -- one pins that ANY subcommand in `consumes_mse` spends the channel even when
the ceremony is declined, the other that an unsupported pinUvAuthProtocol is judged
ahead of a missing token, inside the shared `gate()`. They just carried those
properties on `VENDOR_BACKUP_EXPORT`, and `backup_export`'s FIRST line is
`if cfg!(feature = "fips-profile") { return Err(NotAllowed) }`. Under that profile the
call never reached the ceremony or the gate, so both cases asserted an error the
build cannot produce.
The firmware is fine, and I checked rather than assumed: the channel is spent by
`vendor()`'s wrapper on the way out, `if consumes_mse(req.subcommand)`, whatever the
handler returned -- so a fips refusal still spends it and the one-shot promise holds.
Both now carry on `VENDOR_ATT_CLEAR`: also gated, also in `consumes_mse`, also routed
through `gate()`, and not refused by any profile. Same property, same assertions, one
meaning on all three builds. Teeth re-proved after the swap, each on its own mutation:
drop `ATT_CLEAR` from `consumes_mse` and the first falls on "the consumer must spend the
channel"; swap the protocol and token checks in `pin_gate` and the second falls with
`PuatRequired` where `InvalidParameter` belongs.
A `fips-profile` case takes over what the swap gave up: export is refused with
`NotAllowed` and the channel is spent anyway. It is worth its own test because the
refusal returns before any handler code runs, so it is the wrapper -- not the handler --
that keeps the promise there; moving the spend into the handlers would quietly except
this profile from it. Driven red by spending the channel only on `res.is_ok()`.
default 610 / 0
strong-pin 614 / 0
fips-profile 605 / 2 -> 608 / 0 (544 / 63 before the PIN sweep)
⚠️ The gate run for this went red on `pytest (tools/rsk)` with "No module named pytest",
which is NOT this change and not a broken shell. `nix develop -c <cmd>` registers no GC
root for the devshell, and `nix-store --query --roots` on
`/nix/store/…-python3-3.13.13-env` returns none -- it is held only by `PYTHONPATH`, and
an environment variable is not a root. So a concurrent nix operation can collect it
mid-run, and exactly the packages that live only in that env (pytest, Pillow) vanish
while the individually-pathed ones (cryptography, fido2, click) keep working. Same
symptom hit the IBM Plex row earlier today. In this run `pytest (gate scripts)` and the
IBM Plex row both PASSED before `pytest (tools/rsk)` failed, which is what makes it
mid-run collection rather than a missing package. Rows 1-98 passed on this tree; 99-101
were run individually afterwards and are green.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…rite made the guess free `check_pin` compared the password first and called `pin_wrong_retry` afterwards, with no read-back. That counter is the applet's only rate limit -- unlike clientPIN there is no per-boot soft lock -- so a decrement that never reached flash left the attempt free: `63Cx` to a wrong password with the counter frozen, which is guesses at one power cycle apiece. `rsk-piv`'s `check_ref`, `rsk-fido`'s `spend_and_verify_pin_hash` and `rsk-oath`'s `spend_and_match_otp_pin` have charged first and read back since audit run-6; OpenPGP is the applet that sweep never reached (E31). `spend_pin_retry` charges the attempt before `ct_eq` -- after the record reads, so a card-state fault still costs nothing -- then reads the counter back, and the success path gives the charge back. `pin_reset_retries` is called with `force` now, because a correct password on the last try legitimately takes the counter to zero. A storage failure answers `6581` instead of the `6983` the old code conflated it with. Ordering is what closes it and not the read-back, and the mutation table is where that stopped being a quotation: with the charge moved back after the comparison and the read-back KEPT, the wrong-password case still passes and only the right-password one falls. Both cases drive a store whose write to EF_PW_PRIV reports success and keeps the old bytes -- one fid and the `write` verb only, so the interleaving they are about stays reachable. Two costs, both deliberate: an interrupted VERIFY now spends a try the holder did not use, which is the direction to fail in and which the guide now says, and a successful VERIFY writes EF_PW_PRIV twice, as PIV's already does. bcdDevice 0x0983 -> 0x0984. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…them was prose `McTokenlessRefused`'s `pin.set` conjunct was true at every gate boundary the recording held, which is not the same as being right. `09_tokenless_gate_no_pin` records the two cells that were missing -- a PIN-less discoverable registration REPEATED, which reuses the slot and therefore writes nothing, and a PIN-less non-discoverable one -- so the grid is six cells with all six filled. The suite holds itself to getInfo `0x14 remainingDiscoverableCredentials` rather than to the status word: `0x00` says only that the gate served the request, and the free-slot count standing still (256 -> 255 -> 255 -> 255, measured) is what makes those boundaries gate rows at all. The proof that they carry weight is a co-mutant, not the count: `TraceSecurityBadPinSet.cfg` -- a rule that forgets `makeCredUvNotRqd` -- is RED on `R4cGateAnswers` at `tracePc = 11` against this recording and GREEN against the recording without them, replaying all 61 states. Measured by regenerating the data from `git show HEAD` of the trace with the ratchets lowered to match. Schema 6 carries the clientPIN SUBCOMMAND, read by the command's own parser (`clientpin::assurance`, cfg-gated out of the image like its makeCredential sibling). A token re-issued with the permissions it already holds moves no raw field, so it arrived as the `getKeyAgreement` it shares a footprint with and B shrugged; the recording has exactly one such boundary and B answers `Authorized` there now. Outcome-committed boundaries are 13 with the rule and 12 with `TOKEN_SUBCOMMANDS` emptied -- both measured, and `@TraceSecurityOutcomesMin` is what makes a retreat to NO-OPINION cost something. The third arm is one line of Rust: `security_trace_builtin_uv` is what §6.1.2 step 6.3's arm rests on, `builtin_uv` is `false` in every recorded byte, and the accessor had no test -- a hard-wired `false` would have read identically. It has a two-arm one now, in the ordinary test row rather than behind the feature, and it is driven red by hard-wiring the accessor either way. What stays unwritten is the SESSION with a pad, not the plumbing. Coverage: commands 32 -> 40, steps 60 -> 74, gate boundaries 5 -> 7, AMBIGUOUS still 0. The mapper's own tests stopped reading the recording positionally while doing this -- six selectors by shape, the way `resets()` already did it, because eight new events broke eleven cases that indexed by number. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…th the heaviest slice
`--shard` takes a CONTIGUOUS slice and not every n-th mutant -- measured, by
reproducing the tool's own list at the commit CI ran -- so where the boundaries
fall decides a shard's crate mix, and with it how much build output piles up on
the runner's ~14 GB. At 8 the 6th slice was 1802 mutants over six crates ending
in `rsk-rsa-asm`, and it killed the hosted runner twice: SIGTERM at 85 % of the
shard, the same 358 survivors both times, the tool healthy to its last line
(`Auto-set test timeout to 44s`, 14 timeouts reported and survived).
Both of that shard's suspect crates were then re-run locally at that commit and
completed clean -- 255 `rsk-rsa-asm` mutants with the same 12 timeouts CI saw,
264 in `rsk-sha512` + `rsk-slip39` in three minutes -- so nothing in the shard is
poisoned and what died was the host.
At 12 the slices are ~1201 over five crates. This is a REDUCTION IN PRESSURE, not
a proven fix: the runner's own resource state was never in the log and this
commit does not claim to have found the cause. The twelve slices were checked to
tile the list exactly -- 14413 entries, same order, no duplicates, nothing lost.
The denominator is `${{ strategy.job-total }}` rather than a second hand-kept 12.
Two numbers that must agree is how a shard space silently loses a slice, and this
one already had that failure mode once: `--shard` counts from zero, so passing
the 1-based number straight through ran 1..7 and never index 0.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`3511112` changed `crates/rsk-device/src/ctap.rs` after `3ca8daf` last bumped `bcdDevice`, so `check.sh`'s `bcd bump + CHANGELOG` row has been RED on a clean HEAD ever since -- found only because the next change's own gate run stopped there, at row 85 of 101. No image differs. The edit is inside `#[cfg(feature = "security-trace")]`, and that feature is declared by `crates/rsk-device` and forwarded by `tools/emu` alone: `firmware/Cargo.toml` has no trace feature at all, so nothing that gets flashed can carry the line. The row does not ask that question, though. It asks whether a line can REACH the image, the counter counts builds rather than behaviour, and an exemption taught for a feature nothing enables is the edit that makes the guard stop firing on the ones that do. 0x0984 -> 0x0985. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`check.sh`'s `test (fips: rsk-fido)`, `test (fips: rsk-piv)` and
`test (strong-pin)` each passed a bare name to `cargo test`, so the only
behavioural coverage the shipped `firmware-fips` and `firmware-strong-pin` images
get was 4, 1 and 4 cases -- with 605, 134 and 611 reported as "filtered out" on
the same line, which is the number nobody read. They run the whole suite now:
134, 608 and 614 cases for 2.52 s + 1.34 s + 1.37 s against a ~20 min gate, the
build for each permutation having happened either way. `test (fido-conformance)`
was widened for exactly this reason in `d4eb40e`, two rows above.
`34fa766` swept rsk-fido's fixtures and stopped there; rsk-piv was still red, six
cases, the same shape one applet over. They provision an RSA-1024 key or a 3DES
management key, both of which `fips-profile` refuses (SP 800-131A), so each
asserted an error the build cannot produce -- in its SETUP, which is why every
failure read "should have succeeded" and none read "should have been refused".
Split the way the profile itself splits them. Where the size is the case's
FIXTURE -- the freshness ladder and the two family-relaxation cases -- the pair
of RSA ids swaps under the profile (`ALGO_RSA_FIXTURE` / `ALGO_RSA_OTHER` and
their two lengths), so the same properties run at 2048 there and at 1024
everywhere else. A 2048 keygen costs 93-414 ms here over three seeds, which is
why the fixture generates rather than imports; 4096 would put a minute into every
run, as the relaxation case's own comment already said. Where the refused
algorithm IS the subject -- the 3DES round trip, the 1024 keygen round trip, the
1024 import vector -- the case is cfg'd out and
`fips_refuses_3des_mgm_and_rsa1024` carries the profile's half. That test gained
the import arm: `keygen.rs` holds two guards on the same rule and only the keygen
one had ever been asserted.
Mutation table, each driven through the row rather than the function:
fixture back to ALGO_RSA1024 NEW red, 6A80 for 9000 in setup OLD green, 1 test ran
test_pins::PIN back to "1234" NEW red, 60 cases OLD green, 4 tests ran
the same under strong-pin NEW red, 60 cases OLD green, 4 tests ran
drop the fips import guard NEW red, 9000 where 6A80 belongs named fips_, so filtered too
The last row is what says the new assertion is load-bearing rather than
decorative; the first three are what the old rows could not have gone red on.
Default profile unmoved at 136 rsk-piv cases, and `rsk-display` -- which declares
both features and compiles a trivial-PIN reject under them -- is deliberately not
given a row: its suite costs 39 s per flavour and nothing drives that arm yet.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`Fs::delete` swallowed `meta_delete`'s error and removed the value anyway, so
over a medium whose EF_META read faults once the caller was told `Ok(())` about a
file whose value is gone and whose record still stands -- the 0x077C databug's
end state, reached with no power cut in it. Reachable on hardware: `rsk-store`'s
`read`/`size` set `last_err` straight from `sequential-storage`'s `fetch_item`.
The repair `docs/store-refinement.md` proposed -- propagate before the value goes
-- is the wrong one and is not what this does. EF_META is ONE blob shared by
every applet, a failed read of it means "cannot tell" rather than "no record",
and 24 of the 33 call sites spell this `let _ = fs.delete(...)`. So `?` would
have stopped every delete on the device for the lifetime of one flash fault,
wipes included, while the callers that discard the result went on reporting
success: an orphaned record traded for a secret outliving its erase, which is the
direction that matters.
The removal stays unconditional and the error is RETURNED. `Err` names a state --
the value is gone and a record may stand over it -- instead of hiding it, and the
nine callers that read a delete's answer report failure where they claimed
success.
Swept by class rather than by site: `meta_add*` is called from `rsk-piv` and
nowhere else, so the one caller that deletes a fid carrying a head is PIV's MOVE
with `to = 0xFF`, the slot delete. It reads the answer now -- the head gets a
retry, because one EF_META read can fault where the next lands, and the key is
read back, because a `remove` that failed leaves the source holding a live key.
Both directions answer 6581 where they used to answer 9000.
Mutation table, each driven through the test and not the function:
delete back to `let _ =` red: "answered Ok(())" on a faulted drop
PIV back to the swallow red: 9000 where 6581 belongs
drop the retry red: 6581 at one faulted read, head standing
drop the key read-back red: 9000 with the key still there
Both injectors are armed for the step and disarmed for the observations, and
rsk-piv's faults EF_META alone: a blanket read fault takes the source key's own
read with it and answers FILE_NOT_FOUND, which is a pass for the wrong reason.
Two couplings paid on the way, neither of them a test. 28 model citations drifted
(+10 in fs.rs, +9 in rsk-piv), and the gate's own suggestion for `fs.rs:441`
pointed into `force_delete`, which carries the same line verbatim -- a citation
that resolves to something DIFFERENT is the invisible kind, so the repair was
made by content and read back off the lock diff. One span straddled the insert
and had to GROW (425-434 -> 425-444) rather than shift. And both `Delete`
co-mutants anchored on the rewritten line: re-derived, re-run, still killed
(51/3 and 47/7).
The model half is not here. `RSKeyStore!Delete` still carries no faulted
disjunct, so the sweep cannot yet judge this shape and `NoOrphanedMetadata` reads
as unconditional where the code now permits a reported orphan; that is the
direction that at least fails loudly, and it is recorded in
docs/store-refinement.md.
bcdDevice 0x0985 -> 0x0986.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`RSKeyStore!Delete` carried one disjunct, the power cut, so a faulted metadata
drop was a transition nothing stated -- and the host sweep said so in a comment,
arming its injector for `MetaAdd` and `MetaDelete` and leaving `Delete` alone.
The previous commit made that gap the model's alone: `Fs::delete` reports the
failed drop now, so the state it leaves is one the caller is told about, and
there is something to hold it to.
Two arms, two clauses. An orphaned record IS a state the shipped tree can reach
-- the value goes even when EF_META cannot be read, because refusing there would
stop every delete on the device -- so `NoOrphanedMetadata` keeps every arm whose
drop landed and the new `NoSilentOrphan` (SEC-STORE-006) forbids one thing only:
answering `Ok` from the arm that could not. A single invariant could not say
that, which is why the second exists rather than the first being weakened.
Store.cfg GREEN 4185 states 364 distinct
StoreSolo_BugDeleteHidesFaultedDrop.cfg RED: NoSilentOrphan 61 distinct
safety tier 186 rows, no mismatches
The distinct count does not move, and that is not the arm being inert: the state
it lands in -- value gone, record standing -- is one a meta-only file already
occupies, so what the disjunct adds is a STEP, not a state. The mutant reddening
at depth 4 is what says it is reachable.
The code co-mutant is the previous commit inverted, `let meta = ... meta` back to
`let _ = ... Ok(())`, and it is killed by TWO tests now: the unit case, and the
sweep, which arms the fault for `Step::Delete` and carries a fifth liveness
counter for the times it actually met a record standing over a value it had
removed. Without that counter the new clause could have been a loop over a state
the walk never reaches. The clean arm stays the RAM sweeps' -- `RamStorage` never
fails a read -- because an injector armed for every delete would leave the arm
the order's own clause is about untested, which is the blindfold the G4 review
paid for once already.
`assert_every_recorder_was_live` takes the indices it must find live now: the
fifth recorder is not every sweep's to reach, and naming that is what keeps it a
decision rather than a counter nobody noticed sitting at zero.
Two gate mechanics worth recording. The `Refines` tag is parsed, not read: a
second invariant named in prose ("the faulted one is `RSKeyStore!NoSilentOrphan`")
is invisible to `assurance_gate.py`, whose regex wants the word before the
backtick -- reworded in place, same line count, so no citation moved twice. And
`README.md`'s store paragraph said 272 distinct where the module has measured 364
since `BugMetaDeleteDropsOnFault` landed; corrected while editing the sentence
above it, not by this change.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`tests/*.py` reach the device over CTAPHID and nothing else, so no suite can answer a prompt the trusted display puts up. That is why the recording the formal replay is held to carries `builtin_uv` FALSE in every event, and why §6.1.2 step 6.3's built-in-UV upgrade is a boundary `scripts/security_trace.py` refuses rather than checks: not because the model cannot state it, but because nothing could produce the session that exercises it. `--taps` cannot close that. A script is queued whole and consumed whenever the flow next polls, so its contacts race the host commands they are meant to answer -- the pad reads level, not edges, at 16 ms in a modal and 100 ms in the ambient loop, and a gesture counted in samples is a different gesture on a different screen. The crate's own display tests do not have that problem because they hold BOTH sides in one thread. `--taps-port` gives a suite the same footing. The channel is the whole mechanism: a bound of one, exactly as `display_tests.rs` uses, so `send` returns when the panel has room -- which after the first contact means it has TAKEN the one before -- and the `ok` answering a line is written only then. A suite that reads `ok` knows where the finger is. Measured against the shipped binary, not just the test: the first `settle` is answered in 0.00 s and the second in 0.53 s, which is the panel's own poll cadence showing through. Lines carry the `--taps` grammar, `settle` for the two lifted samples a nested release wait needs, or a control's NAME -- `key 7`, `onboard skip`, `allow,800` -- resolved through the panel's own hit test. That is the point of the vocabulary: a control that moves takes its name with it, where a coordinate in a Python file would sit there pointing at the wrong pixel. The pad resolves against the IDENTITY layout, and the doc says why: with `Scramble PIN pad` on the digits are laid out afresh per entry and nothing outside the panel can know where they went, which is the setting working rather than a gap here. `--taps` and `--taps-port` are refused together. One is a queue and the other a rendezvous; sharing a pad they would race, which is the defect this exists to remove. The test drives the socket rather than the parser: two lines against a one-deep channel, the second unanswered until the pad takes the first, then the names checked against `hit_pin`/`hit_onboard` themselves. Its teeth: moving the `send` into a background thread so `ok` is written first turns it red on "the second was answered with the first still on the pad". A key the pad does not have (`key 11`) is answered `err`, not silently resolved. The consumer -- a suite that types a PIN on the pad, and the padded recording it produces for R4c's ceremony arm -- is the next change. This one is the mechanism, its vocabulary and their test. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`[Unreleased]` becomes `[0.4.11]` with a lead and a TL;DR in the shape 0.4.10 uses, because `release-build.yml` builds the release notes from that section alone -- what is not in it does not reach the release page. Two repairs while cutting. The section carried `### Changed` TWICE, the second holding one entry (the 12-shard mutants sweep); folded into the first, since a reader looking for what changed has no way to know there is a second list further down. And the 16 MB upgrade warning is carried into the version's own section: the banner at the top of the file says to do that for as long as pre-0.4.8 16 MB keys are out there, and 0.4.10 did not -- so a 16 MB owner reading that release's notes was never told. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
|
You are seeing this message because GitHub Code Scanning has recently been set up for this repository, or this pull request contains the workflow file for the Code Scanning tool. What Enabling Code Scanning Means:
For more information about GitHub Code Scanning, check out the documentation. |
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
… row
`proofs` did not fail a proof — it failed to COMPILE `rsk-device`, and took every
harness in the crate with it:
error[E0080]: assertion failed: rsk_fido::consts::MAX_MSG_SIZE as usize == RESP_CAP
`RESP_CAP` is `rsk_usb::ctaphid::CTAP_MAX_MESSAGE`, which shrinks to two
continuation frames under `cfg(kani)` on purpose (175 against the shipped 7609)
because CBMC runs out of memory at the real width. `MAX_MSG_SIZE` is a literal
and does not shrink, so the compile-time tie between the advertised size and the
transport that carries it is false in exactly that build. Its sibling in
`rsk-usb` (ctaphid.rs:224) carries `#[cfg(not(kani))]` for this reason; this one
did not. Guarded, and the comment says which of the two facts the shrink moves.
Not verifiable locally — the devshell has no kani crate, so `--cfg kani` dies
earlier on `E0433` — the arithmetic and the sibling are the argument, and the PR
run is the check.
`usb` is the row working: 5 usb suites passed, and pico-fido reported
`XPASS(strict)` on `test_enc_cred_store_state_changes_with_resident_credentials`.
The divergence list said `encCredStoreState` (0x1E) was "not implemented" and it
has been since F6, so the test passed and the strict marker turned that into a
failure -- which is what third_party/README.md promises: a divergence that gets
FIXED fails the run instead of quietly staying listed.
Swept the list rather than deleting the one line that fired. Two neighbours were
stale in the same way and are corrected rather than dropped, because both cases
do still fail -- for reasons the entries had wrong:
* `test_get_info_ctap_23_fields_are_well_formed` reads getInfo without minting a
PERSISTENT token, and 0x1E is served only to a holder of one (seed.rs:386).
* `test_pin_complexity_policy_extension` asks to SET 0x1B through
setMinPINLength. The member is advertised; the policy is the build's, not a
host-writable flag.
Nothing else in the table names a member this cycle added (0x18, 0x19, 0x1A,
0x1B, 0x1E, FIDO over CCID), and the OpenPGP half is 256/0 with no xpass.
The six lines of comment moved every citation below them: shifted by content and
relocked, and the traceability table regenerated -- its rows carry the same
citations, and one of them lives in `assurance/crates.toml` where the generator
reads it from, not in the README the gate had named.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
9 tasks
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
2 participants
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.
Opened to run CI, not to merge.
ciandemulatorfire onpull_requestand apush to
developfires neither, so this PR is the test run — the point of itis the CI surface we have been rebuilding, not the merge button.
136 commits on top of
main.bcdDeviceis0x0986; the CHANGELOG section iscut as
[0.4.11]andrelease-build.ymlreads its notes from there.What is in it
encIdentifier,transportsForReset,longTouchForReset,pinComplexityPolicy,attestationFormatsPreference,encCredStoreStatewith conditional mediation,and an enterprise-attestation RP-ID list that can actually be aimed. Two members
are deliberately absent and say why at the skip.
ykmanandpython-fido2reach the same authenticator the browser does.
-50), byte-exact against the ACVP vectors, stillunadvertised by default for the measured Firefox reason.
default).
rsacrate is out of the trust base, RUSTSEC-2023-0071 with it.replays against a real device's recorded state now, and the gates that hold the
apparatus honest found several earlier instruments proving nothing — 20 Kani
proofs nothing ran, fuzz targets that never reached their applet, gate rows
nobody had watched go red. Each is written up in
Internalwith what it missed.What this run is meant to prove
The gate is green locally (
scripts/check.sh, 101 rows) and the TLC safety tieris green at 186 rows, but neither is what this PR is for. Watch instead:
ci—check, theknobsaggregate, and theflavorsmatrix, includingthe profile rows whose test filters were dropped this cycle (they ran 1, 4 and 4
cases before; they run 134, 608 and 614 now).
emulator— the socket-transport suites and the USB half in the QEMU guest.deep-checksif it fires — the weeklycargo-mutantssweep is 12 shardsnow, after the 6th slice took the hosted runner down twice at 8.
Hardware, for the record
firmware-no-touchat0x0986was flashed to a 4 MB board and swept: 35 of oursuites pass, 16 need a physical replug the CTAP 6.6 window makes unavoidable, and
the rest are environment or wrong-flavour rather than firmware. The vendored
OpenPGP card suite is 256/0. CTAP 2.3 conformance is 215/6/73 on the emulator
— the six being the known, already-decided non-findings — and 212/9/73 on the
board, the three extra explained by the no-touch build and the metadata flavour.
🤖 Generated with Claude Code