Bounds

RS-Key is not formally verified. This page is generated from the registry and reports what evidence exists, not that a whole-system theorem does. The Definition of done keeps this sentence a requirement until one exists, and scripts/claims_gate.py holds every page naming three or more registered properties to it. What is out of scope and what is accepted: limitations and the threat model.

Every bound every closed slice was taken at, and what each one stops being proved. The rows are not written here: they are read out of assurance/bundle/*.toml, one per bound_* key, by scripts/bounds_gate.py, which regenerates this page on every gate run and refuses a stale copy of it.

It replaces a hand-typed table. Fourteen rows stood under The bounds in the slice design, no script read them, and six mutations — a docs bound moved while the bundle stood still, a bundle bound moved while the docs stood still, a row renamed after a constant that does not exist, a row deleted — were green on all eight gates. A number a reader trusts and no gate reads is the defect this page exists to end.

What is rendered

Every bundle the tree has — 11 of them. Not the first slice’s alone: the exit criterion says the slice’s bundle because there was one when it was written, and rendering one now would leave most of the tree’s bounds unshown, which is the same table written in parallel with a smaller denominator.

Every one of the 11 is a p0-launch row of assurance/configurations.toml, all in the SEC-FIDO family, so all the bundles and the P0-launch rows that have any raw evidence at all are one set. The rest of that tranche is the difference, derived here rather than typed: 6 of its 17 rows carry no bundle, so there is nothing to render for them — SEC-STORE-001, SEC-STORE-002, SEC-STORE-003, SEC-STORE-004, SEC-STORE-005, SEC-STORE-006.

Property	Invariant	Bundle	Method rows	Bounds	With a per-bound consequence
`SEC-FIDO-001`	`NoAuthorizationBypass`	`assurance/bundle/SEC-FIDO-001.toml`	8	33	33
`SEC-FIDO-002`	`NoCrossTransportTouchConsumption`	`assurance/bundle/SEC-FIDO-002.toml`	8	41	41
`SEC-FIDO-003`	`NoTokenAfterInvalidation`	`assurance/bundle/SEC-FIDO-003.toml`	9	46	46
`SEC-FIDO-004`	`NoAccessibleSecretWithoutGate`	`assurance/bundle/SEC-FIDO-004.toml`	7	32	32
`SEC-FIDO-005`	`NoUnmanageableCredential`	`assurance/bundle/SEC-FIDO-005.toml`	7	33	33
`SEC-FIDO-006`	`ResetNeverWeakensSurvivingState`	`assurance/bundle/SEC-FIDO-006.toml`	9	42	42
`SEC-FIDO-006A`	`ResetKeepsThePinGate`	`assurance/bundle/SEC-FIDO-006A.toml`	7	32	32
`SEC-FIDO-006B`	`ResetKeepsTheAlwaysUvGate`	`assurance/bundle/SEC-FIDO-006B.toml`	7	33	33
`SEC-FIDO-006C`	`ResetKeepsTheBackupSeal`	`assurance/bundle/SEC-FIDO-006C.toml`	8	37	37
`SEC-FIDO-007`	`RamNeverOutlivesFlashSeed`	`assurance/bundle/SEC-FIDO-007.toml`	5	26	26
`SEC-FIDO-008`	`NoLiveTokenWithoutPinRecord`	`assurance/bundle/SEC-FIDO-008.toml`	8	42	42

397 of 397 bounds carry a per-bound consequence. The column is stops_<name> beside bound_<name> in the bundle — the same way shipped_relation already travels with a method row, one field down — so the consequence moves with the number instead of being re-typed beside it. A cell reading — would be a bound the bundle carries no such field for; what such a bound costs is then only in its row’s shipped_relation, printed under each table as the row note.

The bounds, by property

`SEC-FIDO-001` — `NoAuthorizationBypass`

Method 1 — tier A: the requirement gate over the abstract relation

model-check over formal/RSKeyTokenGate.tla + TokenGate.cfg. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_states`	`44`	nothing by omission: the 44 are the WHOLE A domain and the number is a pin that they are reached, not a shrink of them. What no bound on this row can reach is the level above it — that the shipped machine holds no state this eight-boolean record cannot express
`bound_ops`	`11`	any protected operation the abstract alphabet does not name; and, inside the eleven, every requirement tier A has no vocabulary for — presence, the reset window, the retry counter, an rpId identity — because the oracle answers those TRUE and hands the obligation to tier B
`bound_outcomes`	`3`	the difference between a silent drop and a rejection. The alphabet is Silent, Authorized and Rejected and the invariant reads only the Authorized edges, so a defect that turns one refusal into the other is admitted here
`bound_relation_tuples`	`63888`	nothing by omission — the comprehension is enumerated whole. What its size costs is the FORM of the statement: read over the whole of it the predicate names no variable and TLC answers at startup with no counterexample, so the invariant is written as the slice at the current state and the 44 have to be pinned reachable instead

Row note (shipped_relation). 44 A states is the WHOLE domain, so this bound is not a shrink; the floor is a pin at 44 because the invariant is the relation’s slice at the current state

Method 2 — tier A: the oracle is not the relation

exhaustive sweep over TokenGateOracle.cfg + TokenGateDisagreement.cfg. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_states`	`22`	anything about the other half of the domain. The walk is exactly the set on which the requirement gate and the relation-read gate differ, so on every A state outside it the two definitions agree and this row cannot tell a second definition from the relation read back to itself
`bound_pairs`	`31`	nothing by sampling — the 31 are the whole disagreement set, computed by the model rather than chosen. What the count does not say is that any one of them is a defect: it is the measurement that the oracle is a SECOND definition, which the refuted per-FID projection is the reason for

Row note (shipped_relation). the disagreement set is exact, not sampled: every (state, op) pair of AStates × Ops is compared

Method 3 — tier B: every invariant Shipped.cfg names, over the shipped constants

model-check over Shipped.cfg. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_rps`	`2`	an rpId-binding defect needing a third relying party. The measured minimum is 1 and no mutant in the roster backs the module’s own `>= 2` comment
`bound_channels`	`2`	a three-channel interleaving, at B
`bound_max_retries`	`8`	nothing individually. The soft lock is unreachable unless MaxRetries exceeds MismatchLimit, so the real constraint is a relation between two constants and a per-constant minimum cannot express it — which is why formal/scopes.txt records `-` for both
`bound_mismatch_limit`	`3`	nothing individually — see stops_max_retries; the pair is what is bounded, not either constant
`bound_max_clock`	`1`	anything about elapsed time. At 0 the Tick action is measured dead, so 1 is the smallest non-degenerate value and not a claim about the clock
`bound_reset_window`	`0`	the INSIDE-the-window arm. RESET_WINDOW_MS (10000) is the shipped value; at 0 the model only ever sees a closed window, so the reset-window clause is exercised on re-opening and never on a legitimate in-window reset
`bound_symmetry_permutations`	permutations of RPs and Channels	soundness under liveness. Safety configurations only
`bound_credentials_per_rp`	`1`	anything about slot exhaustion or MAX_RESIDENT_CREDENTIALS (256)

Row note (shipped_relation). MaxRetries and MismatchLimit ARE the shipped MAX_PIN_RETRIES (8) and PIN_MISMATCH_LIMIT (3); RPs and Channels are 2 against an unbounded device; ResetWindow 0 exercises the window closed only, so a legitimate in-window reset is never seen; MaxClock 1 is the smallest value at which Tick is not dead

Method 4 — tier B: AS-AUTH-2’s other arm

model-check over AlwaysUv.cfg. cfg: none. features: always-uv (modelled as the compiled default, not built).

Bound	Value	What stops being proved
`bound_rps`	`2`	an rpId-binding defect needing a third relying party, on the alwaysUv arm
`bound_channels`	`2`	a three-channel interleaving, on the alwaysUv arm
`bound_max_retries`	`2`	the ladder as the image walks it. Two rungs against the shipped eight, so a defect that needs a third failed PIN attempt to be reached is outside this arm’s reachable set and Shipped.cfg is the row that runs the ladder
`bound_mismatch_limit`	`1`	the two rungs between one mismatch and the shipped three, and any approach to the soft lock that needs them

Row note (shipped_relation). the retry ladder is REDUCED on this arm and the shipped one is not: the arm buys the alwaysUv reachability question, and Shipped.cfg is the row that is about the ladder

Method 5 — tier C: the walk guard over a symbolic operation sequence

bounded proof over crates/rsk-fido/src/state_kani.rs::no_authorization_bypass_walk_owner. cfg: kani. features: kani-soft.

Bound	Value	What stops being proved
`bound_sequence`	`5`	any defect needing a sixth dispatch — Begin, Next, unrelated command, Begin, Next, Next is already six
`bound_channels`	`2`	a three-channel interleaving. Two is the measured model minimum for BugCmWalkIgnoresChannel; it has never been measured at the code level
`bound_clock_values`	`2`	a leg landing inside the idle window after a partial advance; the window is exercised as open or fully expired, never partially. The two values are T0 and T0 + PUAT_MAX_USAGE_PERIOD_MS (600000)
`bound_totals`	full symbolic u16 — not a shrink, and saying so is the point	nothing — this one is not a shrink, and saying so is the point of listing it

Row note (shipped_relation). 5 operations against a device that dispatches unboundedly; Begin/Next/other/Begin/Next/Next is already six

Method 6 — tier C: the Begin’s own decision, at its call site

bounded proof over crates/rsk-fido/src/credmgmt_kani.rs::no_authorization_bypass_rps_begin_at_call_site + …_creds_begin_at_call_site. cfg: kani. features: kani-soft.

Bound	Value	What stops being proved
`bound_sequence`	`1`	any defect needing a second dispatch after the Begin; this row proves one Begin out of one starting state and the walk harness (#5) is what covers a sequence
`bound_channels`	`2`	a three-channel interleaving at the call site
`bound_symbolic_bytes`	`1`	every pinUvAuthParam whose difference from the genuine MAC is not that one bit — a symbolic-length payload makes the compression function symbolic with it, and one harness over both Begins had not converged after 40 minutes and 8 GiB
`bound_totals`	full symbolic u16	nothing — not a shrink

Row note (shipped_relation). one Begin from one starting state; the pinUvAuthParam is a genuine 32-byte v2 MAC with ONE symbolic bit, because a symbolic-length payload makes the compression function symbolic with it — measured, one harness over both Begins had not converged after 40 minutes and 8 GiB

Method 7 — the cfg(kani) constant shrinks on this path

review over docs/assurance-bounds.md. cfg: kani. features: kani-soft.

Bound	Value	What stops being proved
`bound_ctap_max_message`	`3`	a pinUvAuthParam arriving across more than two continuation frames. Shipped is one INIT plus 128 continuations; rsk-device’s RESP_CAP IS this constant, so every harness in rsk-device — including the seven in presence_kani.rs — proves over a transport two frames wide
`bound_chain_buf_size`	`16`	any chained APDU over 16 bytes. Shipped is 2038, and rsk-device’s FidoCcidApplet is an rsk_sdk::Applet, so the FIDO applet’s CCID chaining is proved at 16
`bound_resp_chain_cap`	`16`	any chained response over 16 bytes; shipped is 2048
`bound_cfg_not_kani_assertions`	`2`	the equality of the two widths the getInfo response and the transport publish. crates/rsk-device/src/ctap.rs gates MAX_MSG_SIZE == RESP_CAP behind cfg(not(kani)), and rsk-usb does the same for the frame-multiple assertion; neither is a proof obligation and both are about the SHIPPED width, so under Kani the two constants are not held equal to each other

Row note (shipped_relation). CTAP_MAX_MESSAGE is 129 frames shipped and 3 under cfg(kani), and rsk-device’s RESP_CAP IS that constant, so all seven presence_kani.rs harnesses prove over a two-continuation transport; rsk-sdk’s CHAIN_BUF_SIZE/RESP_CHAIN_CAP are 2038/2048 shipped and 16 here. What stops being proved: a pinUvAuthParam arriving across more than two continuation frames, and any chained APDU over 16 bytes

Method 8 — the ghost’s completeness

exhaustive sweep over scripts/ghost_gate.py over formal/RSKeySecurityState.tla. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_actions`	`21`	nothing by omission — the 21 are every operator Next reaches, derived on each run rather than listed beside the module. What the equality cannot say is whether an action that records is recording the RIGHT thing; the Solo_ configurations and the code twins are what that is for
`bound_routes`	`24`	the value written. The rule compares which occurrences of the name exist inside a viol assignment and which policy each consults, never what the recorded name means once the guard is satisfied
`bound_guards`	`11`	any defect INSIDE a policy operator. The assignment is held to the guard it consults by NAME, so swapping one policy for another is a finding and weakening the body of one is not

Row note (shipped_relation). the whole module: every operator Next reaches, and every occurrence of the name inside a viol’ assignment

`SEC-FIDO-002` — `NoCrossTransportTouchConsumption`

Method 1 — tier B: the invariant over the whole reachable space of the shipped constants

model-check over formal/RSKeySecurityState.tla::NoCrossTransportTouchConsumption Shipped.cfg. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_rps`	`2`	nothing this invariant can express — it names pres.granted, pres.cancelBy, pres.scope and the ghost, and no constant. What two costs it is reach alone: a falsifying presence state that first arises over a third relying party is not in the set searched
`bound_channels`	`2`	nothing this invariant can express, and note which arity this is NOT: the transport count is `Owners`, a five-element set fixed in the module, so no .cfg can widen it. What two costs is reach — a cross-transport consumption that first arises over a third concurrent channel is not in the set searched
`bound_max_retries`	`8`	nothing at all. The ladder is off this property’s path, and at the shipped value it is not a shrink either; what it buys is that the PIN doors are reachable at the depth the image has
`bound_mismatch_limit`	`3`	nothing at all, for the same reason as the ladder it pairs with — no clause of this invariant names a mismatch counter, and three IS the shipped limit
`bound_max_clock`	`1`	nothing this invariant can express. What one Tick costs is reach: a falsifying state that needs a second unit of elapsed time is not in the set searched
`bound_reset_window`	`0`	nothing this invariant can express. What zero costs is reach: a reset STARTED inside the shipped window is a prefix no run here produces, so a presence decision crossing a transport during a legitimate in-window reset is not in the set searched

Row note (shipped_relation). MaxRetries and MismatchLimit ARE the shipped MAX_PIN_RETRIES (8) and PIN_MISMATCH_LIMIT (3); RPs and Channels are 2 against an unbounded device; MaxClock 1 is the smallest value at which Tick is not dead; ResetWindow 0 runs the window closed only. NONE OF THE SIX IS ON THIS PROPERTY’S PATH — the invariant names pres.granted, pres.cancelBy, pres.scope and the ghost, and no constant. What the six buy it is the reachable set a falsifying state would have to appear in; what they cost it is nothing it can express. The bound that IS on its path is not in this list and is not a configuration knob at all: Owners is a five-element SET fixed in the module at formal/RSKeySecurityState.tla:144, so the transport arity cannot be widened by a .cfg — AS-XT-2

Method 2 — tier B: the other arm of all three registered scope constants, against this invariant

model-check over AlwaysUv.cfg PermWide.cfg ForceChange.cfg. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_arms_run`	`3`	the fourth standing assumption. Three of the four `scripts/assumption_gate.py` tracks have both arms run against this invariant; PowerOnClearsScratch2 lives in RSKeyBootHardening and no configuration checking this property takes either of its arms, so nothing here says whether a power-on that fails to clear scratch2 can carry a presence decision across a transport
`bound_rps`	`2`	a falsifying state that first arises over a third relying party, on all three arms
`bound_channels`	`2`	a falsifying state that first arises over a third concurrent channel, on all three arms
`bound_max_retries`	`2`	nothing — the ladder is off this property’s path, so eight rungs down to two is free here in a way it is not for SEC-FIDO-001
`bound_mismatch_limit`	`1`	nothing, for the same reason: no clause names the mismatch counter, so one against the shipped three costs this invariant no term

Row note (shipped_relation). three configurations, one per constant: AlwaysUvShipped TRUE (formal/AlwaysUv.cfg), WidePerms TRUE (PermWide.cfg, one relying party) and ForceChangeModelled TRUE (ForceChange.cfg). The retry ladder is REDUCED on all three — 8:3 becomes 2:1 — and for THIS invariant that shrink is free in a way it is not for SEC-FIDO-001, because neither constant appears in the property. What the three rows buy is that of the four standing assumptions scripts/assumption_gate.py tracks, THREE have both arms run against this property; the fourth, PowerOnClearsScratch2, lives in RSKeyBootHardening and the overlap with the configurations checking this invariant is ZERO. That is a stronger position than SEC-FIDO-001 and SEC-FIDO-007, which each have one such constant

Method 3 — non-degeneracy: the invariant can go red, on a name that is its own, at five different (owner, canceller) pairs

model-check over Solo_BugUnscopedCancel.cfg Solo_BugPanelCancelable.cfg Solo_BugUnscopedOtpCancel.cfg Solo_BugNoDropStaleCancelAtEntry.cfg Solo_BugTouchNotSpent.cfg. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_invariants_checked`	`2`	anything about the other eight invariants. Each row checks TypeOK and this name alone, which is what makes a RED this property’s rather than a sibling’s — and the price is that a state falsifying two at once is seen here as falsifying one
`bound_armed_switches`	`1`	any defect that needs TWO of the model’s bug switches at once. One armed switch per row is what attributes the kill, and a cross-term between two injected defects is not a state any of the five reaches
`bound_isolated_rows`	`5`	a sixth way for this invariant to fail. Five arms are five defects somebody wrote a switch for, so non-degeneracy is shown for those five and for no failure mode nobody modelled
`bound_counterexample_depth_max`	`7`	nothing — the depths are MEASURED trace lengths and not a bound the configurations impose. What they say is that the five land on four different (scope, cancelBy) pairs rather than all tripping on the first; what they cannot say is that a longer trace would find nothing else

Row note (shipped_relation). each of the five arms ONE Bug* switch with every other FALSE and checks TypeOK and this invariant and nothing else, which is what tells a kill from a neighbouring invariant’s. Unlike SEC-FIDO-007 the Solo rows are not the only place this property is observed to fail: its invariant IS in formal/gen-configs.sh:105-107’s ALL_INV, so the five Mut_ twins that check the whole set report THIS name too — measured, all ten, and that is the b_mut_twins row. The four cancel counterexamples land at depths 4, 5, 5 and 5 and the confirm one at 7, on four DIFFERENT (scope, cancelBy) pairs, which is what says each reaches its own boundary rather than all five tripping on the first

Method 4 — tier C: the cancel clause at code level — the wait that ends Cancelled was cancelled by the transport that owns it

bounded proof over crates/rsk-device/src/presence_kani.rs::no_cross_transport_touch_consumption_cancel. cfg: kani. features: kani-soft.

Bound	Value	What stops being proved
`bound_budget_polls`	`3`	any defect that first appears on a fourth poll. The shipped wait polls for its whole ten-second budget at a 16 ms tick — hundreds of iterations — and every one past the third is outside this harness
`bound_unwind`	`6`	nothing beyond the poll budget it covers. At 6 against a budget of 3 the unwinding is slack, so it is not the binding bound on this row and BUDGET_POLLS is; too small would be loud rather than silent, because Kani fails the unwinding assertion
`bound_scopes`	`4`	an arbiter handed a scope byte that is none of the four. `scope` is drawn symbolically over the four SCOPE_* values and assumed to be one of them, so a fifth byte reaching the arbiter is outside the proof
`bound_cancel_producers`	`2`	a cancel from a producer that is neither host path. Both host cancels are raised or not in every slice, so the interleaving of THOSE two is symbolic and a third source of cancellation is not modelled
`bound_stale_cancel_arm`	`1`	the stale-cancel drop at the wait’s EXIT. Of the two drops only the one at entry is pinned here; observing the other needs a second wait, which is a unit test’s and not this harness’s

Row note (shipped_relation). BUDGET_POLLS is 3 and the unwind bound 6 (crates/rsk-device/src/presence_kani.rs:20-25), against a shipped wait whose budget is MIN_TIMEOUT_SECS 10 s at a 16 ms poll — about 625 iterations. scope is fully symbolic over the four SCOPE_* bytes and both host cancels are raised or not in every slice, so the interleaving is symbolic; what is NOT symbolic is the SCHEDULE, because Kani reads the arbiter’s atomics sequentially and says so — AS-XT-1. There is no cfg(kani) constant shrink on this path: git grep -n 'cfg(kani)' crates/rsk-device/src outside the harness files is one hit, the mod proofs hook at crates/rsk-device/src/presence.rs:260. SEC-FIDO-001’s method table says CTAP_MAX_MESSAGE’s shrink puts ‘all seven presence_kani.rs harnesses’ over a two-continuation transport; measured here, that constant is real for the crate build and INERT for these seven — RESP_CAP lives in ctap.rs and ccid.rs and none of the seven constructs either

Method 5 — tier C: the confirm clause, and the premise it reasons from proved rather than assumed

bounded proof over crates/rsk-device/src/presence_kani.rs::no_cross_transport_touch_consumption_confirm crates/rsk-device/src/presence_kani.rs::a_hold_that_satisfied_a_ceremony_is_spent_by_it. cfg: kani. features: kani-soft.

Bound	Value	What stops being proved
`bound_ceremonies`	`2`	a hold that spans three ceremonies. Two is what the harness runs, the second on a finger that never lifted, and the model’s TouchConfirm is what covers a longer hold
`bound_budget_polls`	`3`	any defect that first appears on a fourth poll of either ceremony, the same shrink as the cancel row
`bound_unwind`	`6`	nothing beyond the poll budget it covers; at 6 against 3 polls the unwinding is slack on this row too
`bound_scopes`	`4`	a ceremony whose scope byte is none of the four. The two scopes are independently symbolic over the four SCOPE_* values, which is the whole alphabet the type admits and nothing outside it

Row note (shipped_relation). two ceremonies under independently symbolic scopes, the second running on a finger that never lifted. Stated as one implication rather than an assume, so no premise can silently go unreachable, and the premise itself is the second harness rather than an assumption. The Rust proved is STRONGER than the model needs: spent carries no owner, so a still-held press confirms for nobody — including the same transport again — while the model’s usedBy only forbids the CROSS-transport case. Two ceremonies is the bound: a hold spanning three is not proved here and the model’s TouchConfirm is what covers it

Method 6 — the production side: which sites own the decision, whether the tagged owners are those sites, and what the derived columns see

review over crates/rsk-device/src/presence.rs::request_cancel crates/rsk-device/src/presence.rs::cancel_otp_wait crates/rsk-device/src/presence.rs::pending_for firmware/src/presence.rs::up_pending scripts/assurance_gate.py. cfg: none — every site above is unconditional production code on a button build; the two cfg(feature = "display") forwarders at firmware/src/presence.rs:263-269 are counted apart and are AS-XT-4’s. features: none.

Bound	Value	What stops being proved
`bound_tagged_owners`	`3`	any owner outside the three the tag set names. This is a count of SITES and not a shrink of a shipped constant, because a review has no other unit, so what it covers is exactly the sites that were read
`bound_cancel_writers`	`2`	nothing by omission on this axis — `cancel_requested.store(true` is exactly two sites and both carry a tag, so both halves of the cancel decision are covered. What a count of sites cannot say is that a future third writer would be noticed
`bound_scope_writers`	`4`	any scope write outside the four call sites in the worker. The sequencing around a dispatch is the worker’s, and reading four sites says which they are and not that the order between them is right
`bound_credited_files`	`2`	the difference between a file and a site. The derived column counts FILE names, so a second owner inside an already-counted file moves nothing — which is why one credited file carrying no tag never reddened a row
`bound_untagged_credited_files`	`1`	any warning from the derived column about exactly this. One of the two credited files carries no tag and the column still reads 2, so the column cannot distinguish a covered file from a counted one
`bound_harnesses_in_file`	`7`	the five harnesses the column does not count. Seven live in the proof file and two are credited, so whatever the other five prove is outside every derived number this row feeds
`bound_harnesses_counted`	`2`	any claim that the two counted harnesses are the strongest available. The count is what the column credits, not a judgement about which proofs are load-bearing

Row note (shipped_relation). git grep -n 'cancel_requested.store(true' is exactly TWO sites — crates/rsk-device/src/presence.rs:120 inside request_cancel’s SCOPE_FIDO test and :131 inside cancel_otp_wait’s SCOPE_OTP test — and both carry a tag, so both halves of the cancel decision are covered, which is the thing that had to be confirmed rather than assumed. The four set_wait_scope call sites are firmware/src/worker.rs:434, :528, :663 and :665. Two files are credited to the rust column and one of them carries no tag; seven harnesses live in the proof file and two are counted. These bounds are counts of SITES and not shrinks of a shipped constant, because a review has no other unit — the same weakness SEC-FIDO-007 recorded about its own review row

Method 7 — the code twin: the same defect in production Rust, driven to the name of every test that fell and the direction each fell in

mutation over formal/comutants.toml scripts/comutate.py crates/rsk-device/src/presence_tests.rs::w4c_no_cancel_crosses_a_transport_boundary. cfg: none. features: none — the slice formal/comutants.toml names is exactly cargo test -p rsk-device, on the default feature set.

Bound	Value	What stops being proved
`bound_patch_hunks`	`1`	any defect the one hunk cannot express. A co-refutation patch is a hunk count and not a shrink of a shipped constant, so what is driven is the defect somebody wrote and not the class it belongs to
`bound_patched_files`	`1`	a defect that has to span two files. All five of this property’s comutants patch the tagged owner, which is the healthy case; a cross-file ordering defect is not something this apparatus can inject
`bound_failing_tests`	`3`	which assertion is load-bearing. Three tests fall, and a count of them says the mutant died and not that any one of the three was written for this property
`bound_owner_canceller_pairs`	`6`	the two pairs the sweep excludes — an owner raising its own cancel — and any pair over a transport the four owners do not include
`bound_comutants_for_this_property`	`5`	any model switch with no code twin. Five comutants stand against this invariant and the register is what defines the set, so a modelled defect nobody wrote a patch for has no code-level verdict here

Row note (shipped_relation). all five of this property’s comutants patch ONE file, crates/rsk-device/src/presence.rs, which is the tagged owner — the healthy case, and not SEC-FIDO-007’s, where the patched file was neither an owner nor tagged. BugUnscopedCancel and BugPanelCancelable share an ANCHOR (formal/comutants.toml:159-163 and :450-454 quote the same three lines), which the file’s own note says in as many words: the model splits the scope test three ways and the code fuses it into one guard. One of the five was re-driven by hand here; the other four are the recorded expect = "killed", which .github/workflows/deep-checks.yml:476-479 re-drives WEEKLY as a gating row and the scripts/check.sh:"comutants lint" row lints on every run. The six pairs are w4c’s sweep: four owners × two host-reachable cancels, less the two an owner may raise for itself

Method 8 — the scope disposition: why four build columns are `out-of-scope` and not `gap`, and what that leaves open

review over assurance/configurations.toml firmware/src/presence.rs::poll_pressed docs/assurance-matrix.md. cfg: none. features: none — no-touch is the feature the four columns add, and no evidence in this bundle was built with it.

Bound	Value	What stops being proved
`bound_columns_total`	`31`	any build outside the thirty-one columns the ledger carries. The disposition is decided per column, so a configuration nobody listed has no cell to be `gap` or `out-of-scope` in
`bound_columns_out_of_scope`	`4`	nothing about the four, and that is the point: on a no-touch image no presence decision is produced at all, so a property about where a decision may be applied has no subject. What SURVIVES the disposition is that the arbiter and all three tagged functions ARE compiled into those images — what is absent is the wait, not the arbitration
`bound_columns_claimed`	`3`	twenty-seven of the thirty-one. Three columns carry a claim, so the invariant is asserted for three builds and for no other
`bound_columns_gap`	`24`	everything on those twenty-four columns. A gap is the honest remainder — nobody has judged — and three of them are board columns that move `presence.source` off BOOTSEL, where the decision’s producer is not the one this evidence was taken over
`bound_board_columns_moving_presence`	`3`	the three boards themselves. Naming which gap columns change the presence source says where the evidence would have to be retaken and never that it holds there

Row note (shipped_relation). this is the only row of the eleven-bundle programme with out-of-scope cells, and the disposition is DECIDED rather than open: on the four no-touch images ButtonWait::wait — the sole caller of set_up_pending(true) on a non-display build — is never called, because ButtonPresence::wait is cfg(not(feature = "no-touch")) and request/request_ceremony return Presence::Confirmed outright (firmware/src/presence.rs:202-258). So no presence DECISION is produced at all, and a property about where a decision may be applied has no subject. gap would say nobody has judged; out-of-scope says the claim is not made, which is the true state — and the tree already treats those builds that way, firmware/Cargo.toml saying ‘Never ship a no-touch build’ and release-build.yml refusing to release one. NOTE WHAT SURVIVES: Arbiter and all three tagged functions ARE compiled into those images; what is absent is the wait, not the arbitration. The 24 gap cells are the honest remainder and three of them are board columns that move presence.source off BOOTSEL

`SEC-FIDO-003` — `NoTokenAfterInvalidation`

Method 1 — tier B: the whole invariant over the shipped constants, on the arm the image actually builds

model-check over formal/RSKeySecurityState.tla::NoTokenAfterInvalidation + Shipped.cfg::NoTokenAfterInvalidation. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_rps`	`2`	an rpId-binding defect that needs a third relying party; two is what the ghost’s binding half is checked over
`bound_channels`	`2`	a three-channel interleaving of the invalidators — two channels is every concurrency this row searches
`bound_max_retries`	`8`	nothing by shrinking: eight IS the shipped MAX_PIN_RETRIES, so the two mutants that reach this invariant through the retry ladder walk the rungs the image has. The row that costs this property ladder depth is the reduced arm below, not this one
`bound_mismatch_limit`	`3`	nothing by shrinking, for the same reason as the ladder it pairs with — three IS PIN_MISMATCH_LIMIT, so the soft-lock approach is at shipped depth here
`bound_max_clock`	`1`	every question about elapsed time. One Tick is the whole clock, so the TIMER invalidator — `expire_stale_token` against a usage period this model has no wall clock for — is exercised as `some time has passed` and never at a duration
`bound_reset_window`	`0`	the reset invalidator as a legitimate in-window reset. At zero the window is only ever seen closed, so `reset` is reached through ResetStart and ResetConfirmed and never through the power-up window the shipped device opens

Row note (shipped_relation). MaxRetries and MismatchLimit ARE the shipped MAX_PIN_RETRIES (8) and PIN_MISMATCH_LIMIT (3) at crates/rsk-fido/src/consts.rs:368,372, and for THIS property that matters in a way it does not for SEC-FIDO-007: BugWrongPinKeepsToken and BugLocalPinKeepsToken are both reached through the retry ladder, so the ladder is on the path. RPs and Channels are 2 against an unbounded device; MaxClock 1 is the smallest value at which Tick is not dead, which bounds the TIMER arm — expire_stale_token is a tagged owner and PUAT_MAX_USAGE_PERIOD_MS (600 000 ms) is a wall clock this model does not have. ResetWindow 0 runs the window closed only, so the reset invalidator is exercised through ResetStart/ResetConfirmed and never through a legitimate in-window reset. This is the ONLY one of the four GREEN rows at AlwaysUvShipped = FALSE

Method 2 — tier B: the same invariant on the arm of AlwaysUvShipped the default image does not build

model-check over AlwaysUv.cfg::AlwaysUvShipped. cfg: none. features: always-uv (modelled as the compiled default, not built).

Bound	Value	What stops being proved
`bound_rps`	`2`	an rpId-binding defect needing a third relying party, on the alwaysUv arm
`bound_channels`	`2`	a three-channel interleaving, on the alwaysUv arm
`bound_max_retries`	`2`	the two rungs this arm does not have. Both mutants that reach this invariant walk the ladder, so at two rungs against the shipped eight this arm is not where a retry-shaped defect is caught
`bound_mismatch_limit`	`1`	the two mismatches between one and the shipped three, and any approach to the soft lock that needs them — the same shrink the ladder takes, on the counter it pairs with
`bound_max_clock`	`1`	every question about elapsed time, as on the shipped row: one Tick, so the timer invalidator is exercised as `some time has passed` only
`bound_reset_window`	`0`	the in-window reset arm, as on the shipped row — the window is seen closed on this arm too

Row note (shipped_relation). the retry ladder is REDUCED here and the shipped one is not — 8:3 becomes 2:1 (formal/AlwaysUv.cfg:6-7) — because the arm buys the alwaysUv reachability question and Shipped.cfg is the row that is about the ladder. What the row buys this property is that a registered standing assumption is run BOTH ways against it. What it costs is stated rather than implied: the two mutants that walk the ladder would have two fewer rungs to walk here, so this arm is not where a retry-shaped defect is caught

Method 3 — tier B: the permission alphabet’s other arm, which is the one this invariant’s own term reads

model-check over PermWide.cfg::WidePerms. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_perm_subsets`	`16`	nothing — sixteen is the whole four-bit domain and this axis is a WIDENING, not a shrink. It is worth more to this invariant than to its neighbours because `tok.perms # {}` is a term of the second conjunct, so the domain the permission set is drawn from is a domain the invariant quantifies over
`bound_rps`	`1`	the rpId-binding half of the ghost. One relying party is the price this row pays for the wide permission domain, so on this configuration a token has no second relying party to be wrongly bound to
`bound_channels`	`2`	a three-channel interleaving of the invalidators, on the wide-permission arm
`bound_max_retries`	`2`	the six rungs between two and the shipped eight, so the two ladder-walking mutants are shallower here than on the shipped row
`bound_mismatch_limit`	`1`	the two mismatches between one and the shipped three, on the wide-permission arm

Row note (shipped_relation). WidePerms = TRUE draws ps from SUBSET Perms — all sixteen subsets of {mc, ga, cm, acfg} instead of the five PermSets narrows to (RSKeySecurityState.tla:174-177). This row is worth MORE to this property than to SEC-FIDO-001, and the reason is textual: tok.perms # {} is a TERM of the second conjunct, so the domain the token’s permission set is drawn from is the domain the invariant quantifies over. The cost is on the other axis and is real — RPs drops to 1, so the rpId-binding half of the ghost has no second relying party to be bound to on this row, and AlwaysUvShipped is TRUE here as well

Method 4 — tier B: the forced-PIN-change gate’s other arm, a gate that refuses token ISSUANCE after a correct PIN

model-check over ForceChange.cfg::ForceChangeModelled. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_rps`	`1`	the rpId-binding half of the ghost, which this arm drops to one relying party the same way the wide-permission arm does
`bound_channels`	`2`	a three-channel interleaving, on the forced-change arm
`bound_max_retries`	`2`	the six rungs between two and the shipped eight; a retry-shaped defect is not what this arm is for
`bound_mismatch_limit`	`1`	the two mismatches between one and the shipped three, on the forced-change arm

Row note (shipped_relation). ForceChangeModelled = TRUE turns on gate.forceChange, EF_MINPINLEN byte 1, which clientpin.rs reads at the two get_pin_token doors and change_pin clears. It belongs to this property because it is a refusal AFTER the PIN has verified — a grant that must not be minted rather than one that must be retired — and assurance/platform.toml PLAT-MODEL-010 is discharged on it. What the arm does NOT reach is the built-in-UV door (clientpin.rs:493-495), which has no action in this module at all, and the panel’s own clear at clientpin.rs:1269

Method 5 — non-degeneracy: the invariant can go red, seven different ways, and each red names it rather than a sibling

model-check over Solo_BugTokenSurvivesPinChange.cfg Solo_BugStopUsingKeepsPerms.cfg Solo_BugWrongPinKeepsToken.cfg Solo_BugLocalPinKeepsToken.cfg Solo_BugChangePinKeepsPpuat.cfg Solo_BugPinWriteBeforeRevoke.cfg Solo_BugSetPinKeepsPpuat.cfg. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_invariants`	`2`	anything about the invariants a solo row does not check. TypeOK and this name alone is what tells a kill from a neighbouring invariant’s, and the price is that a state falsifying two at once is seen here as falsifying one
`bound_armed_switches`	`1`	any defect needing two switches at once. One armed switch is what attributes the kill to the defect that was injected
`bound_configurations`	`7`	an eighth way for this invariant to fail. Seven switches are seven defects somebody wrote, so non-degeneracy covers those seven and no failure mode nobody modelled
`bound_conjuncts_falsified`	`3`	nothing — all three conjuncts are separately falsified, which is the strongest single statement in this bundle, because a conjunction whose clauses are never falsified apart is a conjunction with a passenger. What it does not say is that each clause is falsified in every way it could be

Row note (shipped_relation). every one of the seven checks TypeOK and this invariant and NOTHING ELSE (formal/gen-configs.sh:181-184 emits the SOLO block — the WORKING-TREE numbers, re-taken by content after a sibling slice grew that file by 69 lines NET — 72 added and 3 removed, 923 lines to 992; the same four lines stood at :173-176 at this bundle’s build.commit, which stays where it is because scripts/evidence_gate.py:459-490 dates a bundle by a commit git can resolve and the one carrying this file does not exist yet), with exactly one Bug* TRUE and every other FALSE, which is what tells a kill from a neighbouring invariant’s. mut = 7 IS this set: assurance_gate.solo_target_counts counts single-target Solo_* configurations. All three conjuncts are separately falsified — the ghost by BugPinWriteBeforeRevoke, the session term by four, the persistent term by two — and that is the strongest single statement in this bundle, because a conjunction whose clauses are never falsified apart is a conjunction with a passenger

Method 6 — tier C: the session token’s own state machine, over a symbolic five-operation sequence

bounded proof over crates/rsk-fido/src/state_kani.rs::no_token_after_invalidation. cfg: kani. features: kani-soft.

Bound	Value	What stops being proved
`bound_sequence`	`5`	any defect needing a sixth operation. Five from one starting state against a device that dispatches unboundedly, so an invalidation sequence that has to set itself up over six steps is outside this harness
`bound_opcodes`	`8`	any invalidator the alphabet does not name. The four the registry statement names are all in the eight, so what is left out is any OTHER route by which a grant could be retired or kept alive
`bound_symbolic_permission_bytes`	`6`	nothing — the permission bytes are full symbolic u8, one per step plus the opening grant, so this axis is not a shrink and no permission valuation is excluded
`bound_clock_values`	`2`	a token that expires strictly BETWEEN the two clock values. The timer arm is exercised at T0 and at the end of the usage period and nowhere in between
`bound_clauses`	`4`	the persistent grant. Four clauses are the session token’s; `pcmr` lives in flash, no clause here names it, and AS-NTAI-3 is the row that owns that hole

Row note (shipped_relation). five operations from one starting state against a device that dispatches unboundedly, drawn from eight opcodes — Begin, MarkUsed, ConsumeAfterUp, Stop, ResetToken, AuthenticatorReset, PowerCycle, TimePasses — so the four invalidators the registry statement names are all in the alphabet. The permission sets are FULL symbolic u8, one per step plus the opening grant, which is not a shrink. The clock is two values, T0 and T0 + PUAT_MAX_USAGE_PERIOD_MS, so the timer arm is exercised at its edges and nowhere between. Every clause is an EQUALITY, not an implication, which is what stops an authenticator that retires everything on sight from satisfying it. What is NOT here: the persistent pcmr grant, which is in flash — the harness header says so, and AS-NTAI-3 is the row that owns it

Method 7 — tier C: the credentialManagement gate’s own decision, at its call site, with a replayed MAC

bounded proof over crates/rsk-fido/src/credmgmt_kani.rs::no_token_after_invalidation_at_call_site. cfg: kani. features: kani-soft.

Bound	Value	What stops being proved
`bound_sequence`	`4`	any replay that needs a fifth step to set up. Four operations is the whole run, so a longer approach to the same call site is outside it
`bound_opcodes`	`3`	any invalidator outside the three this run can issue; the walk harness above is the row that carries the eight-opcode alphabet
`bound_symbolic_permission_bytes`	`1`	every valuation the other steps could carry. One permission byte is symbolic and the rest are concrete, so a defect that needs two different permission sets inside one run is outside this harness
`bound_mac_payloads`	`1`	anything about `pinproto::verify` as a MAC. One concrete payload is driven, so what is shown is that THIS replayed MAC still verifies — never that a forged one would not, which is TCB-2’s
`bound_clauses`	`2`	the same pair of clauses at the other three token gates. They are inline in functions that need a `Ctx`, and a `Ctx` drags `p256` into the reachable set where Kani 0.67.0 aborts in codegen, so this pair is proved at one door of four

Row note (shipped_relation). the real verify_cm_token (credmgmt.rs:278-288) is driven, not a predicate standing in for it, and the pinUvAuthParam is a genuine v2 MAC minted while the grant was live and then REPLAYED. C2 is the load-bearing clause and it is the one that makes C1 mean something: the replayed MAC still verifies, so at this call site and at config.rs:243-245 zeroing permissions is not defence in depth — it is the only defence. One concrete payload, so this says nothing about pinproto::verify as a MAC (TCB-2). Only the cm permission and only this one of the four token gates: the other three are inline in functions that need a Ctx, and a Ctx drags p256 into the reachable set where Kani 0.67.0 aborts in codegen

Method 8 — the production side: which sites own each of the three conjuncts, and whether the tagged owners are those sites

review over crates/rsk-fido/src/state.rs::stop_using_token + crates/rsk-fido/src/seed.rs::clear_ppuat + crates/rsk-fido/src/clientpin.rs::write_pin_verifier. cfg: none — every site above is unconditional production code; the two Kani mirrors are not, and are named in the rows above rather than counted here. features: none.

Bound	Value	What stops being proved
`bound_tagged_owners`	`6`	any owner outside the six tagged sites. This is a count of SITES and not a shrink of a shipped constant, because a review has no other unit
`bound_tagged_files`	`3`	anything the derived column can see about a site. `assurance_gate.grep_word` returns FILE names, so a seventh tag inside a counted file moves nothing — which is why the tag missing from the third conjunct has never reddened a row
`bound_conjuncts`	`3`	the third conjunct’s ownership. Session maps onto three tagged sites and persistent onto three; the ORDER the ghost is written for maps onto none, because `write_pin_verifier` is untagged
`bound_untagged_owner_sites`	`4`	coverage of the sites the tag set does not reach. Two invalidators the statement names by word, `reset` and `power cycle`, are owned by sites carrying a sibling property’s tag or no tag at all
`bound_citations_read`	`23`	any citation the review never opened. Twenty-three OCCURRENCES were read, which is a count of readings and not of sources
`bound_citations_wrong`	`5`	how many SOURCES are wrong. The occurrences collapse onto fewer distinct references — one of them is written three times — so the defect count is smaller than the occurrence count and this bound cannot say by how much

Row note (shipped_relation). six tags over three files, and the rust column is 3 because assurance_gate.grep_word returns FILE names — a seventh tag in a counted file moves nothing, which is the reason the missing one has never reddened a row. The mapping is clean on two conjuncts and empty on the third: session gets state.rs:491/:551/:600, persistent gets clientpin.rs:175/:229 and seed.rs:337, and the ORDER — the conjunct SetPinWrite and ChangePinWrite write the ghost for — gets nothing, because write_pin_verifier is untagged. Two more invalidators the statement names by word, reset and power cycle, are owned by state.rs:426 and state.rs:371 and carry SEC-FIDO-006’s tag and no tag respectively. The citation bounds are OCCURRENCES, not distinct citations: 23 read and 5 wrong over 3 distinct references, and the distinction matters because one of the three is written three times. This bound is a count of sites and of citations, not a shrink of a shipped constant, because a review has no other unit

Method 9 — the code twins: the same defects injected into production Rust, and the one that could not be

mutation over formal/comutants.toml::BugStopUsingKeepsPerms + scripts/comutate.py + crates/rsk-display/src/gates.rs::local_pin_gate. cfg: none. features: none — the slices are cargo test -p rsk-fido and cargo test -p rsk-display on the default feature set.

Bound	Value	What stops being proved
`bound_patched_files`	`3`	a defect that has to span files the three do not include. A comutant is a hunk in a file, so a cross-file ordering defect is not something this apparatus can inject
`bound_patched_crates`	`2`	any invalidation door outside the two crates these patches reach
`bound_patch_hunks`	`9`	the CLASS each hunk belongs to. Nine hunks over six switches are the defects somebody wrote; a variant of the same defect that no hunk expresses has no code-level verdict here
`bound_killed`	`6`	anything about the seventh switch. Six carry a killed patch, so the co-refutation column covers six of the model’s seven defects
`bound_unreachable`	`1`	the setPIN arm at code level. No site’s removal reproduces `setPIN keeps the grant` alone, because the authoritative revoke is the chokepoint changePIN shares — so that switch has a model verdict and no code twin, which is why `mut` is 7 and `co` is 6

Row note (shipped_relation). six of the seven switches carry a patch with expect = "killed", which that file’s own status vocabulary (:20-22) defines as a RECORDED verdict and not a plan; the hunk count is the find/find2/find3 blocks summed over the six. Two crates, because BugLocalPinKeepsToken patches rsk-display — the only co-refutation entry for this property outside rsk-fido, and the door the model calls the fourth. The seventh, BugSetPinKeepsPpuat, is status = "unreachable" and its evidence field is a CODE-level measurement, not a model one: there is no site whose removal reproduces setPIN keeps the grant alone, because the authoritative revoke is the chokepoint changePIN shares. That asymmetry is why mut is 7 and co is 6

`SEC-FIDO-004` — `NoAccessibleSecretWithoutGate`

Method 1 — the invariant over the whole reachable space at the SHIPPED constants

model-check over formal/RSKeySecurityState.tla::NoAccessibleSecretWithoutGate + Shipped.cfg::NoAccessibleSecretWithoutGate. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_rps`	`2`	a falsifying state that first arises over a third relying party. The clause names two booleans and no relying party, so what two costs is reach and not a term
`bound_channels`	`2`	a falsifying state that first arises over a third concurrent channel — reach again, for the same reason
`bound_max_retries`	`8`	nothing by shrinking: eight IS the shipped ladder, and this is the ONE of the four green configurations that runs it. The ladder is off this property’s path and is what makes the PIN doors reachable at all
`bound_mismatch_limit`	`3`	nothing by shrinking, for the same reason as the ladder it pairs with — three IS the shipped mismatch limit
`bound_max_clock`	`1`	any falsifying state that needs a second unit of elapsed time. One Tick is the whole clock here
`bound_reset_window`	`0`	the in-window arm. At zero a reset may start only at clock 0, so a gate record dropped during a legitimate power-up-window reset is a prefix no run on this row produces

Row note (shipped_relation). MaxRetries and MismatchLimit ARE the shipped MAX_PIN_RETRIES (8) and PIN_MISMATCH_LIMIT (3) at crates/rsk-fido/src/consts.rs:368,372; RPs and Channels are 2 against an unbounded device; MaxClock 1 is the smallest value at which Tick is not dead; ResetWindow 0 runs the window closed only. THE RETRY LADDER IS NOT ON THIS PROPERTY’S PATH — gate.ppuat => pin.set names two booleans and no constant — but the ladder is what makes the PIN doors reachable, so what the six buy is the state set a falsifying state would have to appear in. And this is the ONE row of the four GREEN configurations that runs the shipped ladder at all: the other three set MaxRetries 2 and MismatchLimit 1, and two of those run one RP

Method 2 — the same invariant on the other arm of the three standing assumptions that have one

model-check over AlwaysUv.cfg::NoAccessibleSecretWithoutGate + PermWide.cfg + ForceChange.cfg. cfg: none. features: always-uv is modelled as the compiled default on the AlwaysUv arm, not built — no image was produced for any row here.

Bound	Value	What stops being proved
`bound_rps`	`2`	a falsifying state that first arises over a third relying party, on all three arms — and on two of the three the count is 1, so those rows have no second relying party at all
`bound_channels`	`2`	a falsifying state that first arises over a third concurrent channel, on all three arms
`bound_max_retries`	`2`	the six rungs between two and the shipped eight. All three arms run the reduced ladder, so the shipped constants are Shipped.cfg’s alone
`bound_mismatch_limit`	`1`	the two mismatches between one and the shipped three, on all three arms
`bound_configurations`	`3`	any arm of a standing assumption that no configuration takes. Three arms are three rows, and of the four configurations asserting this invariant three are the alwaysUv arm the default image does not build

Row note (shipped_relation). three arms and one caveat that is the honest half. AlwaysUvShipped is TRUE here and FALSE on Shipped.cfg, so BOTH arms of that assumption check this invariant; of the four configurations that ASSERT it, PermWide.cfg is the only one on WidePerms’ TRUE arm and ForceChange.cfg the only one on ForceChangeModelled’s — the roster’s other configurations taking either arm are mutants, which name this invariant in order to fall past it rather than to assert it. The caveat: all three run a REDUCED ladder (2:1 against the shipped 8:3, formal/AlwaysUv.cfg:6-7) and PermWide.cfg and ForceChange.cfg run ONE relying party. So of the four configurations that assert this invariant GREEN, three are the alwaysUv arm the default image does not build, and the shipped constants are Shipped.cfg alone

Method 3 — non-degeneracy: the invariant CAN go red, and the red names it rather than a sibling

model-check over Solo_NoAccessibleSecretWithoutGate.cfg::BugResetGatesFirst + Solo_BugPpuatIsAGate.cfg. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_invariants`	`2`	anything about the rest of the invariant set. Each configuration checks TypeOK and this name and nothing else — which is what tells this kill from a neighbour’s, and it is needed here because on a multi-invariant configuration TLC reports the first violated name and it need not be this one
`bound_armed_switches`	`1`	any defect needing two switches at once. One armed switch is what attributes the red to the defect that was injected
`bound_counterexample_states`	`11`	nothing — eleven is a MEASURED trace length and not a bound the configuration imposes. It is the shorter of the two rows; the same clause needs thirteen on the other
`bound_depth`	`11`	nothing, for the same reason: the depth is what the search found and not a cap it was given, so it cannot say that a longer trace would find nothing else

Row note (shipped_relation). the two bounds above are Solo_NoAccessibleSecretWithoutGate.cfg’s, the SHORTER of the two rows; Solo_BugPpuatIsAGate.cfg needs 13 states and depth 13 for the same clause. Each configuration checks TypeOK and this invariant and NOTHING ELSE — formal/Solo_NoAccessibleSecretWithoutGate.cfg:50-52 and formal/Solo_BugPpuatIsAGate.cfg:50-52 — and arms exactly one Bug* switch with every other FALSE, which is what tells this kill from a neighbouring invariant’s. It is needed in a way it is not on Shipped.cfg: formal/gen-configs.sh:106 puts this invariant in ALL_INV, so on a multi-invariant configuration TLC reports the first violated name and it need not be this one — measured, Solo_BugSetPinKeepsPpuat.cfg reports NoTokenAfterInvalidation under the same switch whose Mut_ twin reports this invariant

Method 4 — which of the three clauses the recorded verdicts are actually about

exhaustive sweep over formal/runs.toml + assurance/bundle/logs/SEC-FIDO-004/tlc-Historical_E77.log + assurance/bundle/logs/SEC-FIDO-004/tlc-Solo_NoAccessibleSecretWithoutGate.log. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_clauses`	`3`	two clauses of three. Only one is observed to fail anywhere in this tree, so for the other two there is no evidence that a red is even reachable
`bound_red_rows`	`5`	nothing by sampling — five is every row of `formal/runs.toml` whose verdict names this invariant, and every one of the five has its raw log in the backed-up tier. What exactness does not buy is discrimination: the apparatus reports all five the same way
`bound_distinct_counterexamples`	`2`	any failure mode outside the two traces. Both end at the same action with the same two fields set, so the five red rows are two observations and not five
`bound_clauses_observed`	`1`	non-degeneracy for the two clauses nothing falsifies. One of three is observed to fail; the other two are asserted by every configuration and refuted by none, which is the state a passenger conjunct would also be in

Row note (shipped_relation). the sweep is EXACT and not sampled: every row of formal/runs.toml whose verdict names this invariant is five, every one of the five has its raw log in the backed-up tier, and every one of the five final states was read. Two distinct counterexamples: a 13-state one shared by four rows (three of them byte-identical over the 404-line trace body, the fourth differing in the two lines that carry gate.ppuatStale) and an 11-state one. Both end at ResetAborts with gate.ppuat TRUE and pin.set FALSE. The bound that matters is the last: ONE of three clauses is observed to fail anywhere in this tree, and the apparatus reports all five as RED: NoAccessibleSecretWithoutGate without distinguishing them

Method 5 — the production side: which sites own each half of clause 3, and whether the tagged owners are among them

review over crates/rsk-fido/src/seed.rs::ensure_ppuat + crates/rsk-fido/src/credmgmt.rs::authorized_by_ppuat + crates/rsk-fido/src/reset.rs::is_fido_gate_fid. cfg: the two projection sites at rsk-device/src/ctap.rs are cfg-gated and reach no image; every other site above is unconditional production code. features: none.

Bound	Value	What stops being proved
`bound_tagged_owners`	`2`	any owner outside the two tagged sites. This is a count of SITES and not a shrink of a shipped constant, because a review has no other unit
`bound_producer_sites`	`1`	a second producer. One `put_sealed32` of the record is the whole write side that was read, so the argument is as complete as that grep is
`bound_consumer_sites`	`3`	a reader the three do not include, and any claim about ORDER: the count says which sites read the record, never that a reader runs after the producer it depends on
`bound_sweep_sites`	`2`	any phase of the wipe outside the two sweep predicates. One puts the record in the SECRETS phase and one keeps it out of the GATES phase, and a third classification site would be outside the review
`bound_files_in_argument`	`5`	anything in a sixth file. Five files carry the argument, two of them only through cfg-gated projections that reach no image
`bound_crates`	`2`	a site in a third crate. The argument spans two, so a consumer of this record outside them is not covered

Row note (shipped_relation). one producer (seed.rs:319, the sole put_sealed32 that MINTS the record; 0x09D9’s boot re-seal at seed.rs:508 writes it again and mints nothing); three consumers (seed.rs:302 load_ppuat, credmgmt.rs:266 through it, and clientpin.rs:418 which is also the producer’s call site); two sweep sites (reset.rs:275 is_fido_fid, which puts the record in the SECRETS phase, and reset.rs:248 is_fido_gate_record, which keeps it out of the GATES phase). Five files — seed.rs, credmgmt.rs, clientpin.rs, reset.rs and crates/rsk-device/src/ctap.rs:201,236, the two cfg-gated projections — across rsk-fido and rsk-device. This bound is a count of sites and not a shrink of a shipped constant, because a review has no other unit; the honest reading of that is in the counterpart bundle and it applies here too

Method 6 — the code twin: the same defect injected into production Rust, driven against the tree’s own suite

mutation over formal/comutants.toml::BugPpuatIsAGate + crates/rsk-fido/src/reset.rs::is_fido_gate_record + crates/rsk-fido/src/reset_tests.rs::a_torn_reset_never_leaves_a_grant_without_its_pin. cfg: none. features: none — the slice is cargo test -p rsk-fido on the default feature set.

Bound	Value	What stops being proved
`bound_patch_hunks`	`1`	any defect the single hunk cannot express. The patch reverts one commit in the shipped file, so what is driven is that defect and not the class it belongs to
`bound_patched_files`	`1`	a defect that has to span two files
`bound_tests_fallen`	`1`	which assertion is load-bearing. One test falls now and the count says the mutant died, not that the test was written for this property — it reads the gate set, which is what the patch edits. It was three before provisioning began minting the grant; see retired_owners_of_the_kill for why the two torn-wipe tests no longer reach the state
`bound_slice_crates`	`1`	any test outside the one crate the slice runs. A kill by a test in another crate would not be observed by this row

Row note (shipped_relation). the patch puts \|\| fid == EF_PAUTHTOKEN.get() back on is_fido_gate_record (formal/comutants.toml:395-414) — eab4b5c reverted, in the shipped file, not a model edit — and it is the ONE co-refutation in this tree whose patch site is a function this property’s own tag sits on. Driven here rather than transcribed: a throwaway worktree at 31c21a7, the anchor asserted to resolve exactly once, cargo test -p rsk-fido --target aarch64-apple-darwin against the main build cache. expect = "killed" in that file is a RECORDED verdict per its own status vocabulary (:19-21), and this run is the second observation of it

Method 7 — what the tag gate can and cannot see about which site owns this property

exhaustive sweep over scripts/assurance_gate.py over crates/rsk-fido/src/credmgmt.rs::authorized_by_ppuat and crates/rsk-fido/src/reset.rs::is_fido_gate_fid. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_variants`	`4`	nothing by omission — four is every subset of the two tags and the sweep is exhaustive over them. What exhaustiveness cannot reach is a THIRD tag: a site that starts owning this property arrives outside the sweep
`bound_tags`	`2`	which side of the implication a tag is on. The rule counts to one and the sweep measures that either tag alone clears it, so a tree whose only tag sits on a half that cannot falsify the invariant is still green
`bound_owner_configurations`	`9`	any configuration outside the nine the rule reads. A tag is owed only for the invariants those nine check, so an invariant checked nowhere among them owes none

Row note (shipped_relation). the sweep is over EVERY subset of the two tags — none, each alone, both — driven through check_tags, the gate’s own entry point, with production_rust pointed at copies rather than at the tree, so nothing was edited. The rule it exercises is scripts/assurance_gate.py:1053-1062: for each of the nine OWNER_CFGS, every invariant that configuration checks must carry a Refines tag SOMEWHERE in production Rust. It is a count-to-one rule and the sweep is what makes that a measurement instead of a reading: either tag alone clears it, and the rule knows nothing about which side of the implication a tag is on

`SEC-FIDO-005` — `NoUnmanageableCredential`

Method 1 — the invariant over the whole reachable space of the shipped constants

model-check over formal/RSKeySecurityState.tla::NoUnmanageableCredential + Shipped.cfg::NoUnmanageableCredential. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_rps`	`2`	every interleaving that needs a second credential for ONE relying party. `store.cred` and `store.rpent` are subsets of RPs, so the cardinality IS this invariant’s own domain — two relying parties with one credential each, against a device that holds hundreds over as many; AS-CRED-1 is the row that owns it
`bound_channels`	`2`	a falsifying state that first arises over a third concurrent channel
`bound_max_retries`	`8`	nothing by shrinking: eight IS the shipped ladder. It is off this property’s path and is what makes the doors above the store reachable
`bound_mismatch_limit`	`3`	nothing by shrinking, for the same reason as the ladder it pairs with
`bound_max_clock`	`1`	any falsifying state that needs a second unit of elapsed time
`bound_reset_window`	`0`	the in-window arm. At zero the wipe is reached only outside the power-up window, so an interleaving that begins inside a legitimate in-window reset is not searched

Row note (shipped_relation). MaxRetries and MismatchLimit ARE the shipped MAX_PIN_RETRIES (8) and PIN_MISMATCH_LIMIT (3) at crates/rsk-fido/src/consts.rs; MaxClock 1 is the smallest value at which Tick is not dead; ResetWindow 0 runs the window closed only. RPs = 2 IS on this property’s path, and that is the difference from SEC-FIDO-007’s identical-looking row: store.cred and store.rpent are SUBSETs of RPs, so the cardinality is the invariant’s own domain — two relying parties, one credential each, against a device that holds MAX_RESIDENT_CREDENTIALS (256) credentials over as many RPs. What two buys is that the counterexamples below are not artefacts of a single-RP degeneracy; what it costs is every interleaving that needs a second credential for ONE rp, which is AS-CRED-1

Method 2 — the same invariant on the three arms the default image does not build, so the assertion is not one configuration’s

model-check over AlwaysUv.cfg::NoUnmanageableCredential PermWide.cfg::NoUnmanageableCredential ForceChange.cfg::NoUnmanageableCredential. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_arms`	`3`	any arm of a standing assumption no configuration takes. What the three buy is that all four of the tree’s non-mutant configurations assert this invariant, which is the whole of its numerator; none of the three constants they vary is on this property’s path, so they buy no depth on it
`bound_rps`	`2`	every interleaving needing a second credential for one relying party, on the three arms as on the shipped row
`bound_channels`	`2`	a falsifying state that first arises over a third concurrent channel, on all three arms
`bound_max_retries`	`2`	the six rungs between two and the shipped eight, on the alwaysUv arm — free here, because no clause of this invariant names a retry count
`bound_mismatch_limit`	`1`	the two mismatches between one and the shipped three, and nothing this invariant can express

Row note (shipped_relation). the retry ladder is REDUCED on the AlwaysUv arm (formal/AlwaysUv.cfg:6-7, 2:1 against the shipped 8:3) and left alone on the other two. AND NONE OF THE THREE CONSTANTS THE ARMS VARY IS ON THIS PROPERTY’S PATH: AlwaysUvShipped is a gate default, WidePerms is the permission-set cardinality and ForceChangeModelled is a PIN-policy flag, while store.cred \subseteq store.rpent names two store fields and no gate. What the three rows buy is therefore not depth on the invariant but that all four of the tree’s non-mutant configurations assert it — which is the whole of the 4 of 40 numerator, and which most MODELLED-ONLY rows do not have

Method 3 — non-degeneracy: the invariant CAN go red, in each of the three places the tree models it failing, and the red names it rather than a sibling

model-check over Solo_BugCredBeforeRp.cfg::BugCredBeforeRp Solo_BugDeleteRpBeforeCred.cfg::BugDeleteRpBeforeCred Solo_BugSeedDoesNotLead.cfg::BugSeedDoesNotLead. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_invariants`	`2`	anything about the rest of the invariant set. TypeOK and this name alone is what tells these kills from a neighbour’s
`bound_armed_switches`	`1`	any defect needing two switches at once
`bound_solo_configurations`	`3`	a fourth ordering. The three switches are the three orderings the shipped tree chose — registration, credential-management delete and the wipe — so an ordering nobody wrote a switch for is not shown to be falsifiable
`bound_counterexample_depths`	`14`	nothing — the depth is the deepest MEASURED trace of the three and not a cap the configurations impose; the other two fall shallower

Row note (shipped_relation). each configuration checks TypeOK and this invariant and NOTHING else, and arms exactly one Bug* with every other FALSE — which is what tells these kills from a neighbouring invariant’s. The three switches are the three orderings the shipped tree chose: registration (EF_RP before EF_CRED, credential.rs:853 vs :888), credential-management delete (EF_CRED before the count, credmgmt.rs:672 vs :679) and the wipe (the seed before the batch — the FIDO_SEED_FIDS loop at reset.rs:113-117, under the comment at :105-107 that says why). The depth bound is the deepest of the three traces, 14 on Solo_BugDeleteRpBeforeCred; the other two fall at 7 and 13. Unlike SEC-FIDO-007, the Solo_ rows are not the ONLY place this property is observed to fail — formal/gen-configs.sh:185-187 puts a mutant’s target invariant FIRST in a Mut_ configuration’s INVARIANTS block, so all three Mut_ twins report this name too

Method 4 — the historical row: the wipe order this tree had before 0x08BF, run against the whole invariant set

model-check over Historical_E76.cfg::BugSeedDoesNotLead. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_invariants`	`7`	clause attribution. Seven invariants are checked at once, so TLC reports the first violated name and a red on this row need not be this property’s — which is what the solo rows above exist for
`bound_armed_switches`	`1`	any defect needing a PAIR of switches at once — and note what the one switch buys here now: this configuration and Mut_BugSeedDoesNotLead.cfg were the same file under two names when this row was written and differ at exactly line 48 today, so the roster’s denominator counts forty distinct configurations rather than one of them twice
`bound_states_searched`	`986872269`	anything about WHICH of the seven invariants earned the green. The search is complete now — 0 states left on queue, depth 58 — so the count is the whole reachable set rather than the point a violation stopped it at, and a completed search is equally silent about all seven names. The key was `bound_states_before_abort` while this configuration aborted; there is no abort to count to any more

Row note (shipped_relation). the configuration is the pre-0x08BF tree — BugSeedDoesNotLead = TRUE — at Shipped.cfg’s constants, and it is the row that says this invariant is what the E76 fix was FOR. It is also this bundle’s first finding about the apparatus rather than the property, AND THAT FINDING HAS SINCE BEEN REPAIRED AT THE GENERATOR. diff formal/Historical_E76.cfg formal/Mut_BugSeedDoesNotLead.cfg was EMPTY when this row was written, both emitted with the same four arguments, so the two files were one configuration under two names and the cfgs = 40 denominator counted 39 distinct ones. formal/gen-configs.sh:322 now passes TRUE for the repair — emit Historical_E76.cfg BugSeedDoesNotLead TRUE TRUE — where the Mut_ loop at :329 still passes FALSE, so diff is the single hunk 48c48 on FixSweepDropsCredsBeforeRpEntries and the forty are forty distinct. THE RUN OF THE NEW CONTENT NOW EXISTS and this row is derived from it: formal/runs.toml’s safety tier, recorded at 9cafee7, has Historical_E76.cfg GREEN states=986872269 distinct=77563872 depth=58 1927s. So the counterfactual repair HOLDS the invariant the E76 defect breaks — Mut_BugSeedDoesNotLead.cfg, the same switch with FixSweepDropsCredsBeforeRpEntries = FALSE, is still RED at 1 875 109 states — and the pair of constants costs the reachable set nothing: the distinct count is Shipped.cfg’s 77 563 872 exactly, at Shipped.cfg’s depth of 58, for 36 072 more states generated

Method 5 — the production side: which sites own each half, whether the tags reach them, and what `reachable by the management surface` means in Rust that `store.rpent` does not say

review over crates/rsk-fido/src/credential.rs::credential_store + crates/rsk-fido/src/credmgmt.rs::decrement_rp + …enumerate_rps + crates/rsk-fido/src/passkeys.rs::for_each_rp. cfg: none — every site above is unconditional production code; the invariant’s name appears in no cfg-gated mirror. features: none.

Bound	Value	What stops being proved
`bound_tagged_owners`	`3`	any owner outside the three the tag set names. This is a count of SITES and not a shrink of a shipped constant, because a review has no other unit
`bound_writer_sites`	`8`	a writer in a file the review did not open. Eight entries over four files is what was read, and one entry holds three best-effort rollbacks, so the site count is larger than the entry count
`bound_reader_sites`	`3`	anything about what a reader DOES with a slot it read. The count names the three browse surfaces and not their agreement — measured, two of them disagree on one skip condition
`bound_skip_conditions`	`3`	the invariant itself, and this is the finding: a record that exists and is SKIPPED satisfies `store.rpent` as plain set membership while being exactly what the clause forbids. Three skip conditions are three ways for that to happen, and no model bound reaches any of them
`bound_files_in_argument`	`4`	anything in a fifth file
`bound_crates`	`1`	a site outside rsk-fido. The whole argument is in one crate, so a management surface in another would be outside it

Row note (shipped_relation). eight writer entries over four files in ONE crate — ten sites, since one entry holds the three best-effort rollbacks — against the three functions the tag set names; the count is a count of sites and not a shrink of a shipped constant, because a review has no other unit. The three skip conditions are the finding: both browse surfaces drop an EF_RP slot when fs.read answers None (credmgmt.rs:364, passkeys.rs:113), when n < RP_PREFIX \|\| buf[0] == 0 (credmgmt.rs:368, passkeys.rs:117) and when unseal_rp_id fails (credmgmt.rs:402, passkeys.rs:122) — and store.rpent is plain set membership, so a record that exists and is skipped satisfies the invariant while being exactly what the clause forbids. The two surfaces do not even agree with each other on the third: enumerate_rps answers CtapError::Other for the WHOLE walk, so one unsealable record hides every other relying party from the host, while for_each_rp skips that one and lists the rest

Method 6 — the five sites the tree already records as open in this class, and whether the model’s abstraction hides them

review over CHANGELOG.md crates/rsk-fido/src/credential.rs::bump_rp crates/rsk-fido/src/credmgmt.rs::delete_credential crates/rsk-fido/src/largeblobext.rs::discard. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_open_sites`	`5`	any site in this class the CHANGELOG’s list does not name. The five were read from a list the tree already keeps, so the review is exactly as complete as that list is
`bound_sites_in_the_forbidden_direction`	`0`	nothing about whether the five are harmless. Measured, none can falsify this invariant — every one strands an EF_RP entry OVER a credential that is gone, which is the direction `cred subseteq rpent` does not constrain — so the zero says this property does not reach them and SEC-STORE-006 is where that direction is asserted
`bound_model_actions_that_can_fail`	`0`	every one of the five leaks. No action of the model can FAIL a flash write, so an `Err` returned by `Fs::put` and a best-effort rollback that itself fails are outside every configuration in this bundle
`bound_tear_producers`	`2`	a tear anywhere but between two writes that succeeded. Both producers act between successful writes, so the failure mode where the write itself returns an error is not a tear this model can produce

Row note (shipped_relation). CHANGELOG.md [0.4.11] Still open, same class, and named here names five sites as open, same class, so the next sweep starts from a list: the power-cut window between the RP bump and the credential write; delete_credential removing EF_CRED and then answering NotAllowed when the EF_RP write fails; decrement_rp’s own let _ = fs.delete(EF_RP + j); the trusted-display delete swallowing the same failure; and largeblobext::discard. MEASURED AGAINST THE INVARIANT, AND THIS IS THE ANSWER: none of the five can falsify it. Every one strands an EF_RP entry OVER a credential that is gone or never landed — rpent \supset cred, the direction cred \subseteq rpent does not constrain — which is precisely why the shipped order was chosen. What the model hides is therefore not a defect in this property’s direction but the five leaks themselves: no action of RSKeySecurityState can FAIL a flash write (the two tear producers are PowerCut, RSKeySecurityState.tla:1522, and ResetAborts, :1484, and both act between two writes that succeeded), so an Err returned by Fs::put and a best-effort rollback that itself fails are outside every configuration. AS-CRED-3 is the row that owns it, and SEC-STORE-006 NoSilentOrphan is where that direction is asserted instead

Method 7 — the code twins: the same three defects injected into production Rust, and whether the tree’s own suite catches them

mutation over formal/comutants.toml::BugCredBeforeRp + scripts/comutate.py + crates/rsk-fido/src/credential_tests.rs::a_failed_registration_never_leaves_a_credential_without_its_rp. cfg: none. features: none — the slice is cargo test -p rsk-fido --lib on the default feature set, with --target aarch64-apple-darwin because the workspace default target is the firmware’s.

Bound	Value	What stops being proved
`bound_registered_twins`	`3`	any model switch with no code twin. Three are registered, one per switch targeting this invariant, so the code-level verdict covers the defects somebody wrote patches for
`bound_patch_hunks`	`2`	any defect the two hunks cannot express. They defer one call past one write in the shipped file, which is that defect and not the class it belongs to
`bound_patched_files`	`1`	a defect that has to span two files
`bound_driven_here`	`1`	the other two verdicts as OBSERVATIONS. One of the three was re-driven for this bundle; the other two are transcribed from the register, so their kills are recorded rather than re-measured
`bound_credited_configurations`	`3`	what the killing tests are ABOUT. The credit is three because the index reads solo configurations by invariant name; the tests that fall are named for this property’s shape and not for the property, and no derived column counts them

Row note (shipped_relation). three twins are registered — one per model switch, at formal/comutants.toml:96, :125 and :343 — and all three carry expect = "killed", which is a RECORDED verdict per that file’s own status vocabulary (:19-21) and not a plan. ONE of the three was re-driven for this bundle, BugCredBeforeRp, whose two hunks defer bump_rp past the EF_CRED write in the shipped file; the other two are transcribed from the register and are marked as such in the mutation table. The credit is three because comutate.solo_index reads the Solo_ configuration BY INVARIANT NAME (scripts/comutate.py:337-365) and all three switches target this invariant. What the column does NOT say, and the source does: the killing tests are named for this property’s shape but not for the property, and no derived column counts them

`SEC-FIDO-006` — `ResetNeverWeakensSurvivingState`

Method 1 — the conjunction over the whole reachable space of the shipped constants

model-check over Shipped.cfg::ResetNeverWeakensSurvivingState formal/RSKeySecurityState.tla::ResetNeverWeakensSurvivingState. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_rps`	`2`	a torn prefix that first goes wrong over a third relying party; no clause names one, so what two costs is reach and not a term
`bound_channels`	`2`	a torn prefix that first goes wrong over a third concurrent channel
`bound_max_retries`	`8`	nothing by shrinking — eight IS the shipped ladder, and no clause of this conjunction names a retry count
`bound_mismatch_limit`	`3`	nothing by shrinking, for the same reason as the ladder it pairs with
`bound_max_clock`	`1`	any prefix that needs two units of elapsed time — and, with the window at zero, one Tick is also what closes the window, so the two bounds bite together on this row
`bound_reset_window`	`0`	the whole of the shipped power-up window but its first instant. `InResetWindowGuard` is `sys.clock <= ResetWindow`, so a reset may START only at clock 0 and one Tick refuses it: a reset begun late inside the shipped RESET_WINDOW_MS is a prefix no configuration here tears. What is NOT skipped is the touch — the ceremony runs unconditionally after the window check

Row note (shipped_relation). MaxRetries and MismatchLimit ARE the shipped MAX_PIN_RETRIES (8) and PIN_MISMATCH_LIMIT (3) at crates/rsk-fido/src/consts.rs:368,372; RPs and Channels are 2 against an unbounded device; MaxClock 1 is the smallest value at which Tick is not dead. ResetWindow 0 is the one that costs THIS property something. InResetWindowGuard is sys.clock <= ResetWindow (RSKeySecurityState.tla:1264-1267), so with ResetWindow 0 and MaxClock 1 a reset may START only at clock 0 and one Tick refuses it: the CTAP 2.1 §6.6 power-up window is exercised at its narrowest, and a reset begun late inside the shipped RESET_WINDOW_MS — 10 000 ms at crates/rsk-fido/src/consts.rs:404 — is a prefix no configuration here tears. The touch is not the thing being skipped: crates/rsk-fido/src/reset.rs:37-51 runs the ceremony unconditionally after the window check, and TouchGuard is an enabling conjunct of ResetConfirmed

Method 2 — the same conjunction on the other arms of the three registered scope constants

model-check over AlwaysUv.cfg PermWide.cfg ForceChange.cfg. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_rps`	2 on AlwaysUv.cfg, 1 on PermWide.cfg and ForceChange.cfg	a torn prefix that first goes wrong over a further relying party — and on two of the three arms there is no second one at all, so the ordering is checked over a single credential holder there
`bound_channels`	`2`	a torn prefix that first goes wrong over a third concurrent channel, on all three arms
`bound_max_retries`	`2`	nothing this conjunction can express: no clause names a retry count, so six rungs off the ladder is nearly free here
`bound_mismatch_limit`	`1`	nothing this conjunction can express, for the same reason
`bound_arms`	`3`	clause B on any arm where it can fail. All three arms take AlwaysUvShipped TRUE, and on that value clause B cannot fail — so what the three buy is the other value of three standing booleans and not a second chance at that clause

Row note (shipped_relation). all three REDUCE the retry ladder to 2:1 and two of them drop to one relying party, and for this property that shrink is nearly free: no clause names a retry count and snap.surv needs only one member to be non-empty. What the three arms buy is the other value of AlwaysUvShipped, WidePerms and ForceChangeModelled — and the first of those is not free at all in the other direction, because all three arms take AlwaysUvShipped = TRUE, on which clause B cannot fail. Measured: of the 40 configurations naming this invariant, exactly 3 take that arm and all 3 are among the 4 GREEN

Method 3 — clause isolation: which conjunct a mutant actually breaks, which the parent’s own verdict cannot say

model-check over SoloClause_ResetKeepsThePinGate.cfg SoloClause_ResetKeepsTheAlwaysUvGate.cfg SoloClause_ResetKeepsTheBackupSeal.cfg. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_invariants`	`2`	anything about the rest of the invariant set; TypeOK and one clause is the whole of what each row checks
`bound_clauses`	`3`	any conjunct outside the three. Clause isolation is what the parent’s verdict cannot give, and it is given here for exactly the three the conjunction has
`bound_armed_switches`	`2`	isolation of the DEFECT on one of the three rows. Two switches are on there, because arming one drags its companion in, so that row isolates the clause and not the bug
`bound_configurations`	`3`	a fourth clause-isolating row. Three configurations are three clauses, so a conjunct nobody wrote a row for would have no isolated verdict
`bound_depths`	16, 18 and 8	nothing — the depths are MEASURED trace lengths and not caps. What they say is why the parent’s verdict cannot name a clause: the shallowest is reported every time a search checks all three, so the other two are never the reported name

Row note (shipped_relation). each configuration checks TypeOK and ONE clause and nothing else (formal/gen-configs.sh:171-176 emits exactly that, and :261-262 is the loop that names the three), so a RED cannot be a sibling clause’s. Two of the three arm BugResetGatesFirst and the third arms BugBackupSealedNotAGate — which drags BugSeedDoesNotLead in with it through companion_bug (formal/gen-configs.sh:34-44), so that row is the only one here where TWO switches are on and the isolation is of the CLAUSE, not of the defect. The depths are the content: clause 3 falls at 8 where clauses 1 and 2 need 16 and 18, which is why a search that checks all three reports the third every time

Method 4 — tier C: the induction domain is preserved by every concrete reset step, including a power cut and the boot after it

bounded proof over crates/rsk-fido/src/reset_refinement_kani.rs::reset_never_weakens_surviving_state_across_reboot. cfg: kani. features: kani-soft.

Bound	Value	What stops being proved
`bound_steps`	`1`	every reachability question. Closure under one symbolic step out of a symbolic pre-state is an induction and carries to sequences; what it cannot say is that any particular interleaving is REACHED, so a step whose precondition no real run satisfies is proved about all the same
`bound_actions`	`13`	any reset step the thirteen do not name. The step is selected from those and applied once, so a transition the shipped reset can make and `apply_symbolic_step` has no arm for is outside the closure argument
`bound_symbolic_booleans`	`14`	every field of `FidoState` the projection does not carry. Fourteen booleans are the WHOLE projection, and there is one because a direct run through the real `FidoState::reset()` was stopped with the prover still expanding zeroize loops — so what is closed under a step is the projection and not the state
`bound_progress_values`	`5`	nothing by omission — five is the whole `ResetProgress` enum and the pre-state draws every variant, so this axis is not a shrink
`bound_covers`	`1`	every witness but the one. The single cover is a power-cut-with-a-snapshot, so nothing on this row says any OTHER interesting pre-state is reachable, and an assertion over a vacuous domain would pass the same way

Row note (shipped_relation). ONE symbolic step out of a symbolic pre-state, not a sequence: apply_symbolic_step selects one of 13 actions by raw % 13 and the harness applies it once, so what is proved is that the domain is closed under a step and never that a particular interleaving reaches anything. The 14 booleans (6 persistent, 6 snapshot, 2 volatile) are the WHOLE projection — ResetVolatileView observes two fields of a FidoState that has dozens, and docs/reset-refinement.md records why: a direct run through the real FidoState::reset() was stopped after 72.45 s with CBMC still expanding zeroize loops past 398 iterations. The projection is the reason there is a verdict at all

Method 5 — tier C: each conjunct after the same step, independently of the conjunction that names it

bounded proof over crates/rsk-fido/src/reset_refinement_kani.rs::reset_keeps_the_pin_gate crates/rsk-fido/src/reset_refinement_kani.rs::reset_keeps_the_always_uv_gate crates/rsk-fido/src/reset_refinement_kani.rs::reset_keeps_the_backup_seal. cfg: kani. features: kani-soft.

Bound	Value	What stops being proved
`bound_harnesses`	`3`	nothing these three assertions add on their own. On the tree as it stands the parent’s `well_formed(post)` already implies each clause after the same step, so what the three buy is their covers and a mutation signal, not new coverage
`bound_steps`	`1`	every reachability question, exactly as on the parent row: one step is an induction and not a walk
`bound_covers`	`3`	anything beyond the three antecedents they witness. One cover per clause says that clause’s antecedent is satisfiable and nothing about any other valuation
`bound_shared_precondition`	`1`	every pre-state `well_formed` refuses. All four harnesses assume the same one predicate, so if it were too strong all four would be proved over a smaller domain and none of them would notice

Row note (shipped_relation). AND ON THE TREE AS IT STANDS THESE THREE ASSERTIONS ARE IMPLIED BY THE ROW ABOVE. All four harnesses assume well_formed(pre), apply the same one symbolic step, and the parent asserts well_formed(post) — whose last conjunct IS the conjunction (crates/rsk-fido/src/reset_assurance.rs:267). So clause_i(post) follows from it. What the three DO add is a kani::cover! each, and those are not implied: the parent’s single cover is a power-cut-with-a-snapshot witness and says nothing about any clause’s antecedent being satisfiable. The other thing they add appears only under mutation — see §8’s the parent conjunction loses a conjunct row

Method 6 — the production side: which sites own the ordering, and what the five tags and the three columns actually count

review over crates/rsk-fido/src/reset.rs::reset crates/rsk-fido/src/reset.rs::sweep crates/rsk-fido/src/reset.rs::is_fido_gate_record crates/rsk-fido/src/state.rs::reset crates/rsk-fido/src/lib.rs::load_keydev crates/rsk-fido/src/reset_assurance.rs::well_formed. cfg: none — every site above is unconditional production code; reset_assurance.rs is the exception and is proved absent from every image by scripts/check.sh:576. features: none.

Bound	Value	What stops being proved
`bound_tagged_sites`	`5`	any owner outside the five tagged sites. This is a count of SITES and not a shrink of a shipped constant, because a review has no other unit
`bound_tagged_files`	`3`	anything the derived column can see about a site. `assurance_gate.grep_word` returns FILE names, so two of the five tags move nothing — and one of those is about a SECOND reset path, the trusted-display factory wipe, which the model does not have at all
`bound_clause_tagged_sites`	`3`	the ordering between the tagged sites. Three sites carry a clause’s tag, and a count of them says which sites own a clause, never that they run in the order the clause needs
`bound_gate_records`	`5`	the two gate records no clause names. The phase holds five and the clauses name three, so a record dropped from the gate phase that no clause mentions is outside this argument
`bound_wipe_steps`	`5`	the step boundary the model folds away. The wipe is five ordered steps and the model has four actions for them, `ResetConfirmed` folding the first two into one, so a tear BETWEEN those two is not a prefix any configuration produces
`bound_crates`	`1`	a site outside rsk-fido. Every site in the argument is in one crate, so an ordering owner elsewhere would be outside it

Row note (shipped_relation). five parent tags in three files, and the column is 3 because assurance_gate.grep_word returns FILE names — two tags move nothing, and one of them (survives_factory_reset) is about the trusted-display factory wipe, a SECOND reset path the model does not have at all. The gate phase holds five records and the clauses name three; the wipe is five ordered steps and the model has four actions for them, ResetConfirmed folding step 1 and step 2 into one. Every site is in one crate, which is what makes rust = 3 a count of three files of rsk-fido and not a spread

Method 7 — the code twins: each model switch as the real defect in production Rust, killed by the tree’s own suite

mutation over formal/comutants.toml::BugResetGatesFirst scripts/comutate.py crates/rsk-fido/src/reset.rs::reset. cfg: none. features: none — the slice each row names is cargo test -p rsk-fido on the default feature set.

Bound	Value	What stops being proved
`bound_twins`	`3`	any model switch with no code twin, and any defect of the same shape nobody registered
`bound_patch_hunks`	`4`	the CLASS each hunk belongs to. Four hunks over three switches are the defects somebody wrote; a variant no hunk expresses has no code-level verdict here
`bound_patched_files`	`1`	a defect that has to span two files
`bound_slice_crates`	`1`	any test outside the one crate the slice runs, and any schedule but the weekly one — no row of `check.sh` re-drives these

Row note (shipped_relation). three of the tree’s 31 co-refutation rows credit this invariant, and all three patch one file: BugResetGatesFirst swaps the two sweep calls (1 hunk), BugBackupSealedNotAGate drops EF_BACKUP_SEALED from the gate match arm (1 hunk), BugStateResetAfterWipe moves ctx.state.reset() behind ensure_seed (2 hunks). expect = "killed" is a RECORDED verdict per that file’s own status vocabulary (formal/comutants.toml:19-21), not a plan, and it is re-driven by the weekly comutate run rather than by any row of check.sh

Method 8 — the fuzz rung: what the byte-granular probe’s oracle actually asserts, read rather than run

review over fuzz/fuzz_targets/power_cut.rs::reset_property_holds fuzz/fuzz_targets/power_cut.rs::reset_probe. cfg: none. features: none — a nightly cargo fuzz build of the fuzz/ workspace, no feature flag.

Bound	Value	What stops being proved
`bound_oracle_asserts`	`1`	any verdict finer than the whole conjunction. One assertion means a passing run says only that the fold held, so a clause the fixture made vacuously true is indistinguishable from one that was tested
`bound_clauses_folded`	`3`	which clause fell. All three ARE in the expression, so nothing is omitted; what the folding costs is on the reporting side — a failure names the function while the module doc lists the three clauses by name
`bound_snapshot_valuations`	`1`	the seven other snapshot valuations. The fixture writes all four records before the reset, so three snapshot booleans are TRUE by construction and the eight combinations the Kani harnesses draw symbolically are never explored here
`bound_cut_budget_bytes`	`1048575`	a power cut later than the budget allows. The cut point is drawn from three bytes, so a tear further into the reset than that is not a prefix this target can produce

Row note (shipped_relation). the probe drives the REAL rsk_fido::reset::reset over the real SeqStorage on a mock NOR that can lose power inside a write, then mounts a fresh Fs, scans, runs ensure_seed and boots a second time. That is the strongest rung below the board. What it does NOT have is the split the two tiers above it do: reset_property_holds folds all three clauses into ONE boolean expression (fuzz/fuzz_targets/power_cut.rs:202-204), so a failure names the function and never the clause — while the module doc at :28-31 lists all three clauses by name. And the fixture pins one snapshot valuation: EF_CRED, EF_PIN, EF_ALWAYS_UV and EF_BACKUP_SEALED are all written before the reset, so snap.pin, snap.auv and snap.sealed are TRUE by construction and the 2^3 the Kani harnesses draw symbolically is never explored. The cut budget is data[1] & 0x0f over three bytes, so 0..1 048 575 bytes

Method 9 — the board rung, and what its column is worth: the HIL witness is OWNED and has never been recorded

accepted risk over tests/29_reset_power_cut.py::cut_during_reset docs/reset-refinement.md. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_recorded_runs`	`0`	everything the board rung would say. The column counts a FILE that names the invariant, and no run is recorded, so nothing here is evidence that a real power cut on real hardware preserves the property — PLAT-FLASH-001 owns the missing result and is pending
`bound_asserts`	`2`	any clause the two assertions do not separate. One folds clauses A and B and reports only that the operation was refused, without saying which gate refused it
`bound_clauses_localised`	`1`	clauses A and B. Only clause C has an assertion of its own, so a board run that went red on the folded one would not say which of the two gates it was

Row note (shipped_relation). this is the only one of the eleven registry rows whose test column is 1, and the column counts a FILE that names the invariant. formal/README.md’s own sentence is the one to read: a runtime column of one means the HIL harness is owned and discoverable, not that a board run passed. The script needs a throwaway board, the no-touch image and either an operator’s hand or a relay, and it can exit INCONCLUSIVE when the reset finishes before power goes. Its two assertions fold clauses A and B together (assert assertion_status != 0 — refused, without saying which gate refused) and give clause C its own (current != owner_seed). PLAT-FLASH-001 is the registry row that owns the missing result, and it is pending

`SEC-FIDO-006A` — `ResetKeepsThePinGate`

Method 1 — the clause by name over the whole reachable space of the shipped constants

model-check over Shipped.cfg::ResetKeepsThePinGate formal/RSKeySecurityState.tla::ResetKeepsThePinGate. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_rps`	`2`	a torn prefix that first goes wrong over a third relying party. `snap.surv` needs one member to be non-empty, so two is reach and not a term of the clause
`bound_channels`	`2`	a torn prefix that first goes wrong over a third concurrent channel
`bound_max_retries`	`8`	nothing by shrinking — eight IS the shipped ladder at crates/rsk-fido/src/consts.rs, and this clause names no retry count. `pin.retries` is 8 in the falsifying state and plays no part in it
`bound_mismatch_limit`	`3`	nothing this clause can express, for the same reason as the ladder it pairs with
`bound_max_clock`	`1`	any prefix that needs two units of elapsed time — and with the window at zero, one Tick is also what closes the window, so the two bounds bite together here
`bound_reset_window`	`0`	the whole of the shipped power-up window but its first instant. A reset may START only at clock 0, so a reset begun late inside the shipped RESET_WINDOW_MS — 10 000 ms — is a prefix no configuration here tears. The touch is NOT what is skipped: crates/rsk-fido/src/reset.rs:37-51 runs the ceremony unconditionally after the window check
`bound_invariants`	`12`	nothing about this clause — twelve is what this configuration checks, TypeOK and eleven invariants, and this clause is one of the twelve by name. What twelve costs is attribution rather than coverage: `NoAccessibleSecretWithoutGate` and `ResetNeverWeakensSurvivingState` are two of the other eleven, both are about `pin.set`, and a RED here would be reported under whichever of the three TLC reached first

Row note (shipped_relation). MaxRetries and MismatchLimit ARE the shipped MAX_PIN_RETRIES and PIN_MISMATCH_LIMIT; RPs and Channels are 2 against an unbounded device; MaxClock 1 is the smallest value at which Tick is not dead; ResetWindow 0 is the one that costs this clause something. The verdict is GREEN, and the name is in the INVARIANTS block — measured, twelve indented names between INVARIANTS and SYMMETRY, with ResetKeepsThePinGate among them. This is the only GREEN configuration in the tree that names this clause: grep -l over formal/*.cfg returns exactly two files and the other one must be RED

Method 2 — clause isolation: that this conjunct has an owner of its own, which the parent’s verdict cannot say

model-check over SoloClause_ResetKeepsThePinGate.cfg::ResetKeepsThePinGate. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_invariants`	`2`	anything about the rest of the invariant set. TypeOK and this one clause is the whole of what this row checks, which is exactly why its RED cannot be a neighbour’s — and equally why it says nothing about whether a neighbour would have caught the same defect
`bound_armed_switches`	`1`	any defect the one switch does not build. One armed switch is also what makes the runner compare the reported name: `formal/floors.txt:SoloClause_*.cfg` gives this family `RED -` with no invariant column, and `formal/run-tlc.sh:226-234` then DERIVES the expected name from the configuration’s own INVARIANTS block whenever `armed_count` is 1 — which it is here, measured
`bound_clauses`	`1`	the other two conjuncts of the parent. This row is about one third of `ResetNeverWeakensSurvivingState` and is silent on the rest
`bound_depth`	`16`	nothing — sixteen is a MEASURED trace length and not a cap. What it says is why the parent cannot report this clause: the third conjunct falls at depth 8, so a search that checks all three reports the third every time
`bound_distinct_states`	`918170`	nothing by omission; the search stopped on the counterexample with 333 663 states still on the queue, so this is the space explored before the first violation and not the space of the configuration

Row note (shipped_relation). this configuration checks TypeOK and ONE clause and arms exactly one switch, BugResetGatesFirst = TRUE, at Shipped.cfg’s own constants — measured by reading the file, forty-six CONSTANTS assignments of which thirty-five are the Bug family and exactly one of those is TRUE. So a RED cannot be a sibling clause’s, and the reported name is compared rather than taken on trust

Method 3 — whether the isolated RED is evidence of a catch the neighbouring property would have missed

model-check over Solo_NoAccessibleSecretWithoutGate.cfg::BugResetGatesFirst Solo_BugResetGatesFirst.cfg::ResetNeverWeakensSurvivingState. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_configurations`	`2`	any third reading of the same switch. `BugResetGatesFirst` is armed by FIVE configurations in this tree — measured, `grep -l 'BugResetGatesFirst = TRUE' formal/*.cfg` — and these two plus this clause’s own are the three whose INVARIANTS blocks make the comparison legible
`bound_switch`	`1`	every other defect. This row compares three verdicts of ONE switch and says nothing about a defect no switch in the tree builds
`bound_depths`	11 and 8	nothing — both are measured trace lengths. Read against this clause’s own 16 they are the content of the row: the same switch reddens the neighbouring invariant five levels shallower and the parent eight, so neither search ever reaches the state this clause is about

Row note (shipped_relation). Solo_NoAccessibleSecretWithoutGate.cfg arms BugResetGatesFirst alone and checks TypeOK plus NoAccessibleSecretWithoutGate; Solo_BugResetGatesFirst.cfg arms the same switch alone and checks TypeOK plus the parent. Both are RED. What the pair establishes is bounded and is stated as such: this clause’s own falsifying state ALSO falsifies NoAccessibleSecretWithoutGate, evaluated by hand on the printed state, so the isolated RED is a localisation and not a demonstration of unique reach. The converse IS witnessed — the neighbour’s falsifying state has snap.surv = {}, which makes this clause vacuous there — so the two are separated in one direction only

Method 4 — tier C: the clause holds after one concrete reset step out of any well-formed pre-state

bounded proof over crates/rsk-fido/src/reset_refinement_kani.rs::reset_keeps_the_pin_gate. cfg: kani. features: kani-soft.

Bound	Value	What stops being proved
`bound_steps`	`1`	every reachability question. Closure under one symbolic step out of a symbolic pre-state is an induction and carries to sequences; what it cannot say is that any particular interleaving is REACHED, so a step whose precondition no real run satisfies is proved about all the same
`bound_actions`	`13`	any reset step the thirteen do not name. One of the thirteen is a deliberate outsider — action eleven deletes an OpenPGP record outside the FIDO wipe — and a transition the shipped reset can make that `apply_symbolic_step` has no arm for is outside the closure argument
`bound_symbolic_booleans`	`14`	every field of `FidoState` the projection does not carry. Fourteen — six persistent, six snapshot, two volatile — is the WHOLE projection, so what is closed under a step is the projection and not the state
`bound_progress_values`	`5`	nothing by omission; five is the whole `ResetProgress` enum and the pre-state draws every variant
`bound_covers`	`1`	MORE than the parent bundle claims, and this is the row where that is measured. One cover per clause does NOT say this clause’s antecedent is satisfiable: the shipped condition names three of the antecedent’s four conjuncts and puts `persistent.pin`, the CONSEQUENT, where the fourth belongs. §8’s four `code` rows drive it
`bound_antecedent_conjuncts_covered`	`3`	the fourth conjunct, `snapshot.credential`. A witness satisfying the shipped cover may have it FALSE, and with it false the clause holds vacuously — so the cover cannot distinguish a domain in which this clause is non-trivially satisfied from one in which it cannot fail

Row note (shipped_relation). the harness assumes well_formed(pre) at crates/rsk-fido/src/reset_refinement_kani.rs:125, applies exactly one step, and asserts reset_keeps_the_pin_gate(&volatile) under the message ResetKeepsThePinGate at :130-133. Baseline on this tree: VERIFICATION SUCCESSFUL, 604 checks, 0 failed, 8 unreachable, one cover SATISFIED, 0.99 s. AND THE ASSERTION IS IMPLIED BY THE PARENT HARNESS: all four assume the same well_formed, take the same step, and the parent asserts well_formed(post) whose last conjunct at crates/rsk-fido/src/reset_assurance.rs:267 IS the conjunction. What this harness adds is its cover and a mutation signal — and the cover is the half this bundle found wanting

Method 5 — whether tier C’s non-vacuity guard can fail, driven rather than argued

mutation over crates/rsk-fido/src/reset_refinement_kani.rs::symbolic_snapshot crates/rsk-fido/src/reset_assurance.rs::reset_keeps_the_pin_gate. cfg: kani. features: kani-soft.

Bound	Value	What stops being proved
`bound_arms`	`4`	any question the four do not ask. Four arms answer: does the shipped cover accept a vacuous witness, does the repair still hold, does the shipped cover go UNSATISFIABLE on any vacuity route at all, and does one particular mutation model the defect it was written for
`bound_harness`	`1`	the two sibling clause harnesses. Their covers have the SAME shape — each names three of four antecedent conjuncts and substitutes the consequent — but only this one was driven, and a shape is not a verdict
`bound_conjuncts_named`	`3`	nothing this row proves; three of four is the count the arms are about, and the missing one is named
`bound_solver_seconds`	0.90 to 1.08	nothing — these are measured verification times off Kani’s own summary lines, not caps. What they say is that the repair is free: 0.98 s against a 0.99 s baseline

Row note (shipped_relation). every arm is one edit to the SCRATCH COPY described in build.scratch_workspace, never to this tree. The baseline arm reproduces this tree’s verdict, which is what makes the other three attributable to it. The two arms that matter are: the shipped cover conjoined with !snapshot.credential is SATISFIED, and the shipped cover under a real vacuity mutation is UNSATISFIABLE. Together they bound the finding — the guard is not inert, it simply does not guard the conjunct it omits

Method 6 — the production side: which line destroys EF_PIN, what holds the order, and what the tag counts

Bound	Value	What stops being proved
`bound_tagged_sites`	`1`	any owner outside the one tagged site. This is a count of SITES and a review has no other unit; the site that the clause is ABOUT — the five-line order at reset.rs:104-121 and reset.rs:72 — carries no tag at all
`bound_gate_records`	`5`	the four members this clause does not name. `EF_DEVICE_PIN` and `EF_MINPINLEN` are in the phase and in no clause of any property, which the source says out loud at reset.rs:237-243, so a torn reset that drops either early is unobserved by every rung here
`bound_clause_records`	`1`	everything but `EF_PIN` = 0x1080. One record is the whole of what this clause is about at the FID level
`bound_destroying_sites`	`2`	any third way the record can go. The gate sweep at reset.rs:121 is the reset’s own destroyer; the device-wide `Fs::factory_wipe` is the second, and is the reason `is_fido_gate_fid` is `pub`. Neither is reached by the model, which has an ordering over completed writes and no factory wipe at all

Row note (shipped_relation). the clause is a statement about five consecutive lines and their order is enforced by nothing but their sequence. sweep at reset.rs:134 is batched at 64 with a progress backstop and returns Err when the walk did not complete, so an un-yielded FID counts as absent only on a finished walk — which is the mechanism the clause’s consequent depends on and which no configuration models

Method 7 — what the two runtime columns of this row’s vector actually assert about THIS clause

review over fuzz/fuzz_targets/power_cut.rs::reset_property_holds tests/29_reset_power_cut.py::old_credential_without_gates. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_oracle_conjuncts`	`1`	any attribution at all. The fuzz oracle’s first conjunct is `!credential_usable \|\| (has_data(EF_PIN) && has_data(EF_ALWAYS_UV))` — clauses A and B `&&`-folded — so a failure names the function and never the clause, and a run that dropped EF_ALWAYS_UV reports identically to one that dropped EF_PIN
`bound_assertions`	`1`	the same attribution, one rung up. tests/29_reset_power_cut.py:526-530 asserts the old credential’s assertion was REFUSED; the refusal could be either gate’s and the assertion does not say. The failure MESSAGE prints both option flags, so a human reading a red run could tell — the assertion could not
`bound_recorded_board_runs`	`0`	everything the board column might have been. No run of that script is recorded anywhere in the tree; `hardware` is 0 on this row’s vector, `build` names no board revision because there is no board result to date one, and PLAT-FLASH-001 owns the missing result with `status = "pending"`

Row note (shipped_relation). both files NAME this clause in their doc comments — fuzz/fuzz_targets/power_cut.rs:29-31 and tests/29_reset_power_cut.py:12-14 list all three — and neither can report it. So of the four non-zero evidence columns on this row, two are counts of files whose oracles fold this clause into a sibling’s. The columns are not wrong; they count what they say they count, which is a file

`SEC-FIDO-006B` — `ResetKeepsTheAlwaysUvGate`

Method 1 — the clause over the whole reachable space of the shipped constants, on the one green configuration that names it

model-check over Shipped.cfg::ResetKeepsTheAlwaysUvGate formal/RSKeySecurityState.tla::ResetKeepsTheAlwaysUvGate. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_rps`	`2`	a torn prefix that first goes wrong over a third relying party. The clause needs only `snap.surv # {}`, so two is reach and not a term of the claim
`bound_channels`	`2`	a torn prefix that first goes wrong over a third concurrent channel
`bound_max_clock`	`1`	any prefix needing two units of elapsed time — and with `ResetWindow = 0` one Tick is also what closes the reset window, so the two bounds bite together on this row
`bound_reset_window`	`0`	the whole of the shipped power-up window but its first instant: a reset may START only at clock 0, so a reset begun late inside the shipped RESET_WINDOW_MS — 10 000 ms at crates/rsk-fido/src/consts.rs:404 — is a prefix this row never tears. The touch is NOT what is skipped; crates/rsk-fido/src/reset.rs:37-51 runs the ceremony unconditionally after the window check
`bound_invariants`	`12`	nothing about this clause by omission — twelve is what this configuration’s INVARIANTS block names, TypeOK and eleven invariants, and the last three are the clauses. It is worth the count because two other bundles describe this same block as nine, which was true at `b819ee5` and is false at the commit these runs were taken at
`bound_green_bases`	`1`	any second green configuration. Of the two hundred and ten configurations, forty name the parent invariant and exactly two name this clause; only one of those two is green, so this row is the whole of the clause’s positive model evidence and there is no independent arm to corroborate it

Row note (shipped_relation). MaxRetries 8 and MismatchLimit 3 ARE the shipped MAX_PIN_RETRIES and PIN_MISMATCH_LIMIT at crates/rsk-fido/src/consts.rs:368,372; RPs and Channels are 2 against an unbounded device. The constant that matters to THIS clause is AlwaysUvShipped = FALSE, and it is the shipped image’s own value: firmware/Cargo.toml’s default feature set does not name always-uv. On that value the record exists exactly when the flag is on, so the model’s consequent gate.alwaysUv and the firmware’s EF_ALWAYS_UV presence are the same fact — which is the correspondence the whole ladder below rests on and which the other arm breaks

Method 2 — non-degeneracy: that the clause has a falsifying state at all on the constants its green run uses, and that the state is this clause’s and not a sibling’s

model-check over SoloClause_ResetKeepsTheAlwaysUvGate.cfg SoloClause_ResetKeepsThePinGate.cfg. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_invariants`	`2`	anything about the rest of the invariant set; TypeOK and one clause is the whole of what each row checks, which is exactly what makes a RED attributable
`bound_armed_switches`	`1`	every defect but the one. `BugResetGatesFirst` is the sole model owner of this clause, so a defect the phase swap does not produce has no red row here
`bound_constant_deltas`	`1`	any doubt about whether the green base could go red. This configuration differs from Shipped.cfg in ONE constant (`BugResetGatesFirst = TRUE`) besides its invariant block — measured by `diff`, which reports that line and the INVARIANTS block and nothing else — so the red and the green are the same model with one switch between them
`bound_depth`	`18`	nothing — eighteen is a MEASURED trace length and not a cap. What it says is why the parent cannot name this clause: the sibling clause falls at sixteen and the third at eight, so a search checking all three reports the shallowest every time
`bound_distinct_states`	`2063890`	nothing by shrinking; it is what the search visited before the counterexample, and it is the figure to read against the parent’s own solo row, which reaches a violation in five thousand three hundred and thirty-one

Row note (shipped_relation). each configuration checks TypeOK and ONE clause (formal/gen-configs.sh:182-189 emits exactly that under SOLO, and :330-332 is the loop that names the three), so a RED here cannot be a sibling clause’s. Both rows arm the same switch, clause_mutant at formal/gen-configs.sh:321-328 mapping the first two clauses onto BugResetGatesFirst with the comment that the phase order is their only owner. The pair is what separates the two clauses by a WITNESS: in this clause’s counterexample pin.set is TRUE, so clause A holds there; in clause A’s, snap.auv is FALSE, so this clause is vacuous there

Method 3 — the other arm of the constant this clause depends on, and what the clause is worth on it

model-check over AlwaysUv.cfg PermWide.cfg ForceChange.cfg. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_arms`	`3`	this clause, on every one of them. All three take `AlwaysUvShipped = TRUE`, and on that value the clause has no falsifying state: what the three arms buy is the other value of three standing booleans for the OTHER invariants, and for this one they buy a vacuous conjunct
`bound_falsifying_states`	`0`	the whole of what a green run normally means. Zero is not a measurement of these runs — TLC reports no such count — it is the consequence of `gate.alwaysUv` having two writers, one that clears the antecedent’s `snap` and one that can only raise the flag on this arm
`bound_rps`	2 on AlwaysUv.cfg, 1 on PermWide.cfg and ForceChange.cfg	a torn prefix over a further relying party, and on two of the three arms there is no second one at all. For this clause that shrink costs nothing extra, since the arm has already cost it everything
`bound_max_retries`	`2`	nothing this clause can express: it names no retry count, so six rungs off the ladder is free here
`bound_configurations_arming_the_mutant`	`0`	the ability to EXHIBIT the vacuity rather than argue it. Measured: five configurations set `AlwaysUvShipped = TRUE` and five arm `BugResetGatesFirst`, and the two sets are disjoint — every configuration arming this clause’s mutant takes the FALSE arm. So no recorded run shows the switch failing to redden the clause on the TRUE arm; the claim rests on reading the two writers

Row note (shipped_relation). these three are the arms the scope registry buys — AlwaysUvShipped, WidePerms and ForceChangeModelled — and all three happen to take the first of them TRUE. On the shipped image the constant is FALSE, so these rows describe a build the tree publishes and does not ship. formal/gen-configs.sh:211-225 states the consequence in the generator itself and is the reason clauses=1 is on Shipped.cfg and on no other baseline: recording the clause as asserted on these three would be recording a row that cannot go red

Method 4 — tier C: the clause holds of the Rust projection after any one concrete reset step

bounded proof over crates/rsk-fido/src/reset_refinement_kani.rs::reset_keeps_the_always_uv_gate crates/rsk-fido/src/reset_assurance.rs::reset_keeps_the_always_uv_gate. cfg: kani. features: kani-soft.

Bound	Value	What stops being proved
`bound_steps`	`1`	every reachability question. Closure under one symbolic step out of a symbolic pre-state is an induction and carries to sequences; what it cannot say is that any particular interleaving is REACHED, so a step whose precondition no real run satisfies is proved about all the same
`bound_actions`	`13`	any reset step the thirteen do not name. One is selected by `action % 13` and applied once, so a transition the shipped reset can make and `apply_symbolic_step` has no arm for is outside the closure argument
`bound_symbolic_booleans`	`14`	every field of `FidoState` the projection does not carry. Fourteen booleans — six persistent, six snapshot, two volatile — are the WHOLE projection, and there is one because a direct run through the real reset was stopped with the prover still expanding zeroize loops
`bound_covers`	`1`	every witness but the one. This harness’s single `kani::cover!` says its own antecedent is satisfiable and nothing about any other valuation
`bound_feature_arms`	`1`	the arm this clause is about. `scripts/kani.sh` selects `-p rsk-fido --features kani-soft`, so the proof runs on the default build only; nothing bounded is proved about the build where the record’s presence inverts

Row note (shipped_relation). AND THE ASSERTION IS IMPLIED BY THE PARENT HARNESS on the tree as it stands, which this bundle says rather than presenting an independent proof: all four harnesses assume well_formed(pre), take the same one symbolic step, and well_formed ends in the conjunction (crates/rsk-fido/src/reset_assurance.rs:267), so well_formed(post) already gives this clause. What the harness adds is its own cover and a signal if the conjunction ever loses a conjunct. The α is ALSO not the model: its consequent is persistent.always_uv, the record’s presence, where the TLA+ consequent is the flag — the same fact only while the compiled default is off

Method 5 — the production side: which sites decide this clause, and which of them the tag counts

review over crates/rsk-fido/src/reset.rs::reset crates/rsk-fido/src/reset.rs::sweep crates/rsk-fido/src/reset.rs::is_fido_gate_record crates/rsk-fido/src/config.rs::toggle_always_uv crates/rsk-fido/src/config.rs::always_uv_state crates/rsk-fido/src/config.rs::DEFAULT_ALWAYS_UV. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_tagged_sites`	`1`	every site the tag is not on, which is where the property lives. The one tag is on the CLASSIFIER; the ordering that makes the clause true is two untagged lines at crates/rsk-fido/src/reset.rs:120-121, and the writer that decides what the record MEANS is in another file entirely
`bound_gate_records`	`5`	the two members no clause names. `is_fido_gate_record` matches EF_PIN, EF_DEVICE_PIN, EF_ALWAYS_UV, EF_MINPINLEN and EF_BACKUP_SEALED; three clauses cover three of them, and a torn reset that drops either of the other two early is unobserved by every artifact in this bundle
`bound_flag_writers`	`2`	any site outside the two. `toggle_always_uv` creates and removes the record; the gate sweep removes it. `crates/rsk-fido/src/config.rs:327-329`’s `always_uv_enabled` READS it and resolves a faulted read to ON rather than to the default, which is a strictness this clause does not model at all
`bound_feature_sites`	`2`	any dependence the two sites do not carry. `git grep 'feature = "always-uv"' crates/rsk-fido/src` returns exactly crates/rsk-fido/src/config.rs:315 and crates/rsk-fido/src/conformance/config.rs:77 — neither is in reset.rs or reset_assurance.rs, so no verification-side file in this bundle can tell the two builds apart

Row note (shipped_relation). the review is over the shipped source at b185fc3 with crates/rsk-fido/ clean in the working tree, and its result is a split: the model’s consequent is the FLAG and the Rust α’s is the RECORD, and toggle_always_uv is what makes the two coincide — it deletes the record when the new value equals DEFAULT_ALWAYS_UV and writes it otherwise, so record-present means flag-on exactly while that default is off

Method 6 — the runtime rungs, and whether either of them could report THIS clause rather than its sibling

review over fuzz/fuzz_targets/power_cut.rs::reset_property_holds fuzz/fuzz_targets/power_cut.rs::reset_probe tests/29_reset_power_cut.py::cut_during_reset. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_oracles`	`2`	any rung either oracle does not reach. One is a boolean over a mounted store, the other a sequence of CTAP commands after an operator’s cut, and neither has an assertion this clause owns
`bound_separable_clauses`	`1`	this clause and its PIN sibling, on both rungs. `reset_property_holds` folds them into one conjunct — `!credential_usable \|\| (fs.has_data(EF_PIN) && fs.has_data(EF_ALWAYS_UV))` — so a failure names the function; tests/29_reset_power_cut.py:526-529 folds them into `assert assertion_status != 0`, which says the assertion was refused without saying which gate refused it. Only the backup seal is separable, and it is the sibling this bundle is not about
`bound_recorded_runs`	`0`	everything the board rung would say. The `test` column counts a FILE that names the invariant; no board run is recorded anywhere, `hardware` is 0 on the evidence vector, and PLAT-FLASH-001 owns the missing result at `status = "pending"`
`bound_asserts`	`2`	any clause the two device assertions do not separate, and one of the two is the folded one. The script prints `alwaysUv` from getInfo in its failure message, so an operator reading a red run can see the flag — but the assertion does not test it

Row note (shipped_relation). both rungs drive the REAL reset: the fuzz target cuts inside the store writes and remounts, the device script asks an operator to pull the cable. Their oracles read what the device answers, which for alwaysUv is the FLAG on the device side (getInfo options.alwaysUv) and the RECORD on the fuzz side (fs.has_data(EF_ALWAYS_UV)) — a third spelling of the same split, and on the shipped default build the two agree

Method 7 — mutation: what has to break before something goes red about this clause, at the code tier

mutation over formal/comutants.toml crates/rsk-fido/src/reset_assurance_tests.rs::reset_property_controls_go_red_on_each_early_gate_mutant assurance/bundle/logs/SEC-FIDO-006B/cargo-test-reset-assurance-flavours.log. cfg: none. features: the default set and always-uv, driven separately.

Bound	Value	What stops being proved
`bound_patched_lines`	`2`	every defect the swap does not produce. The twin is the two `sweep` calls exchanged and nothing else, so a wipe that keeps the order and drops the record for another reason has no twin here
`bound_slices`	`1`	any suite the slice does not run. `cargo test -p rsk-fido` is the whole of what the kill is measured over, so a defect only the emulator or a device suite would catch reads as survived
`bound_negative_controls`	`1`	any control over the WIPE. The one per-clause control sets `persistent.always_uv = false` by hand after `begin()` and asserts the clause method returns false — it proves the method can fail, not that the phase order is what keeps it true
`bound_feature_flavours`	`2`	nothing, and that is the finding rather than a gap in the row: both flavours were driven and both are green, so the pair bounds no defect and instead measures that the α cannot tell them apart

Row note (shipped_relation). the twin patches the shipped file at the shipped lines: formal/comutants.toml:331-338’s find is crates/rsk-fido/src/reset.rs:120-121 verbatim, and its replace is the same two lines exchanged. The flavour probe drives the shipped test module unmodified under two feature sets, which is why its verdict is about the abstraction and not about a patch

`SEC-FIDO-006C` — `ResetKeepsTheBackupSeal`

Method 1 — the clause over the whole reachable space of the shipped constants, as one of the twelve names that configuration checks

model-check over Shipped.cfg::ResetKeepsTheBackupSeal formal/RSKeySecurityState.tla::ResetKeepsTheBackupSeal. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_rps`	`2`	a torn prefix that first goes wrong over a third relying party — and for THIS clause that costs less than for its siblings, because its antecedent names no credential at all: `snap.seed /\ snap.sealed` is true with `store.cred` empty, which the recorded counterexample confirms
`bound_channels`	`2`	a torn prefix that first goes wrong over a third concurrent channel
`bound_max_retries`	`8`	nothing by shrinking, and eight IS the shipped ladder at crates/rsk-fido/src/consts.rs:368. This clause names no retry count
`bound_mismatch_limit`	`3`	nothing by shrinking, for the same reason as the ladder it pairs with
`bound_max_clock`	`1`	any prefix that needs two units of elapsed time; with the window at zero one Tick is also what closes the window, so the two bounds bite together here
`bound_reset_window`	`0`	the whole of the shipped power-up window but its first instant. A reset may START only at clock 0, so a reset begun late inside the shipped RESET_WINDOW_MS — 10 000 ms at crates/rsk-fido/src/consts.rs:404 — is a prefix this configuration never tears. The touch is not what is skipped: crates/rsk-fido/src/reset.rs:43-51 runs the ceremony unconditionally after the window check
`bound_invariant_names`	`12`	any obligation outside the twelve. TypeOK and eleven invariants is what this configuration checks, and this clause is one of the three added to that block after the existing bundles’ runs were recorded — a sibling bundle describing the block as nine names is describing a different file

Row note (shipped_relation). MaxRetries and MismatchLimit ARE the shipped MAX_PIN_RETRIES and PIN_MISMATCH_LIMIT at crates/rsk-fido/src/consts.rs:368 and :368; RPs and Channels are two against an unbounded device. The clause held at every reachable state of this run, and that is a stronger reading than it looks: TLC evaluates an invariant at every state, so GREEN here is a verdict about (Idle /\ snap.seen) => ((snap.seed /\ snap.sealed) => gate.backupSealed) over the whole set and not about a sampled prefix. Measured against sed -n '/^INVARIANTS/,/^SYMMETRY/p' formal/Shipped.cfg, which lists TypeOK and eleven names

Method 2 — non-degeneracy: the clause alone, with its own defect armed, so a RED cannot belong to a sibling conjunct

model-check over SoloClause_ResetKeepsTheBackupSeal.cfg. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_invariants`	`2`	anything about the rest of the invariant set; TypeOK and this one clause is the whole of what the row checks
`bound_armed_switches`	`2`	isolation of the DEFECT. Two switches are armed — `BugBackupSealedNotAGate` and its companion `BugSeedDoesNotLead` — so what this configuration isolates is the CLAUSE, and the falsifying behaviour needs both. The mechanism is derived in `x_companion_mechanism` rather than asserted
`bound_depth`	`8`	nothing by capping — eight is a MEASURED trace length and not a bound. What it says is why the parent’s verdict cannot name a conjunct: this clause falls two states shallower than either sibling, so a search checking all three reports this one every time
`bound_distinct_states`	`5359`	any behaviour outside the reachable set this configuration explored. It is three orders of magnitude smaller than either sibling clause’s run, which is the same fact as the depth: the shallow clause is the cheap one to falsify and the one that masks the others

Row note (shipped_relation). the configuration checks TypeOK and this clause and nothing else — formal/gen-configs.sh:358 emits exactly that inside the loop over CLAUSE_INV at formal/gen-configs.sh:121, and clause_mutant at formal/gen-configs.sh:348 is what pairs this clause with BugBackupSealedNotAGate. Its constants are Shipped.cfg’s, verbatim, except the two armed switches. formal/floors.txt:SoloClause_*.cfg gives the family a wildcard RED row with no invariant column, so the runner does not compare the reported name for these; the name in formal/runs.toml:138 is the one TLC printed

Method 3 — the localisation claim: that every parent-level reset verdict in this tree reports THROUGH this clause, which is the reason the clause split exists at all

model-check over Solo_BugBackupSealedNotAGate.cfg Solo_BugResetGatesFirst.cfg Solo_BugSeedDoesNotLead.cfg. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_configurations`	`3`	a fourth reset-family switch. `BugStateResetAfterWipe` is the one not run here, and it is the parent bundle’s row — its falsifying state carries the same three fields, so including it would add a fourth instance and not a fourth kind
`bound_clause_reported`	`1`	which conjunct a reader would have to open the trace to learn. The parent invariant is what the verdict column prints; that the trace is this clause is recovered by reading the final state, and no column in this tree carries it
`bound_depths`	8, 8 and 13	nothing — the three are MEASURED trace lengths. Read against the two sibling clauses’ 16 and 18, they are the whole localisation argument
`bound_switches`	`2`	the pair as a unit. Two DISTINCT defects reach this clause at the parent level — the marker’s own and the phase-order one — and the third configuration is the companion, present to show it does NOT reach this clause

Row note (shipped_relation). formal/RSKeySecurityState.tla:1826-1830 claims all four reset-family mutants report the umbrella invariant on its third clause. Verified here by opening the final state of each artifact rather than by citing the comment: Solo_BugBackupSealedNotAGate.cfg and Solo_BugResetGatesFirst.cfg both end at ResetAborts with snap.surv empty, snap.pin FALSE, snap.seed TRUE, snap.sealed TRUE and gate.backupSealed FALSE — so the two sibling clauses are VACUOUS there and only this one is falsified, on a switch whose only model owner the sibling clauses are. The third artifact is the control in the other direction: Solo_BugSeedDoesNotLead.cfg falls on NoUnmanageableCredential at a state with snap.sealed FALSE, so the companion does not reach this clause and is not what its verdict is about

Method 4 — tier C: the clause holds of the projected reset state after one concrete step out of a symbolic pre-state

bounded proof over crates/rsk-fido/src/reset_refinement_kani.rs::reset_keeps_the_backup_seal crates/rsk-fido/src/reset_assurance.rs::reset_keeps_the_backup_seal. cfg: kani. features: kani-soft.

Bound	Value	What stops being proved
`bound_steps`	`1`	every reachability question. Closure under one symbolic step out of a symbolic pre-state is an induction and carries to sequences; what it cannot say is that any particular interleaving is REACHED, so a step whose precondition no real run satisfies is proved about all the same
`bound_actions`	`13`	any reset step the thirteen do not name. `apply_symbolic_step` at crates/rsk-fido/src/reset_refinement_kani.rs:56-94 selects one by `action % 13` and applies it once; a transition the shipped reset can make with no arm here is outside the closure argument. The arm that matters for this clause is `reset.delete(EF_BACKUP_SEALED)` at crates/rsk-fido/src/reset_refinement_kani.rs:77
`bound_symbolic_booleans`	`14`	every field of `FidoState` the projection does not carry. Fourteen booleans — six persistent, six snapshot, two volatile — are the WHOLE projection, so what is closed under a step is the projection and not the state
`bound_progress_values`	`5`	nothing by omission: five is the whole `ResetProgress` enum at crates/rsk-fido/src/reset_assurance.rs:62-68 and the pre-state draws every variant, so this axis is not a shrink
`bound_covers`	`1`	every witness but the one. The single `kani::cover!` at crates/rsk-fido/src/reset_refinement_kani.rs:173-178 witnesses `snapshot.seen /\ snapshot.owner_seed /\ owner_seed_reachable /\ persistent.backup_sealed`, and says nothing about any other valuation being reachable

Row note (shipped_relation). AND THIS ASSERTION IS IMPLIED BY THE PARENT HARNESS ON THE TREE AS IT STANDS, which this bundle says rather than presenting an independent proof: reset_never_weakens_surviving_state_across_reboot assumes the same well_formed(pre), applies the same one step, and asserts well_formed(post) — whose last conjunct at crates/rsk-fido/src/reset_assurance.rs:267 IS the conjunction. What this harness adds is its cover, which is not implied, and a mutation signal if the conjunction ever loses this conjunct. It is also the reason the property reads BOUNDED at all: status is rebuilt from the derivation and kani > 0 is what selects it. The α is WIDER than the TLA+ clause in one place and that widening belongs to this clause alone — see c_alpha_is_not_the_model

Method 5 — the production side: which site decides the marker’s phase, which sites read it, and what the derived column can see of any of that

review over crates/rsk-fido/src/reset.rs::is_fido_gate_record crates/rsk-fido/src/reset.rs::reset crates/rsk-fido/src/reset.rs::sweep crates/rsk-fido/src/vendor.rs::try_backup_sealed crates/rsk-fido/src/vendor.rs::backup_export. cfg: none — every site above is unconditional production code except crates/rsk-display/src/backup.rs, which is named in prose and not resolved here because it is behind the display feature. features: none.

Bound	Value	What stops being proved
`bound_tagged_sites`	`1`	every owner outside the one tagged site. The clause’s whole `rust` column is one `Refines` line on `is_fido_gate_record`, so the ordering block that the property actually lives in — crates/rsk-fido/src/reset.rs:104-121 — carries no tag of its own and is invisible to the derivation
`bound_gate_records`	`5`	the four gate records this clause does not name. The phase holds five and this clause is about one, so a torn prefix that drops `EF_DEVICE_PIN` or `EF_MINPINLEN` early is outside this argument entirely
`bound_consumers`	`2`	a third reader of the marker. Two exist — the host export at crates/rsk-fido/src/vendor.rs:847 and the on-device reveal at crates/rsk-display/src/backup.rs:47 — and the second is compiled in only on a display build, so on the default image this clause guards one surface and on a display image it guards two. The model has one boolean and no consumer at all
`bound_writers`	`2`	any path that could set the marker other than the two finalize surfaces. Both write the same one byte, so no reader can tell which wrote it, and neither can the model
`bound_crates`	`1`	the display crate, which is where the second consumer lives. Everything else in this argument is in `rsk-fido`, which is what makes `rust = 1` a count of one file rather than a spread

Row note (shipped_relation). the marker’s phase is decided at exactly one site — the matches! arm at crates/rsk-fido/src/reset.rs:251 — and consumed at two, in two different crates, one of them behind a feature. The runtime consumer is FAIL-CLOSED where this clause is fail-open: backup_sealed at crates/rsk-fido/src/vendor.rs:1035 answers true for a probe the medium could not complete, precisely because the absent arm hands out the master seed. So the only way the window re-opens on a live seed is a reset that removed the record, which is the behaviour this clause constrains and the reason it has no runtime backstop

Method 6 — the code twin: the model switch as the real defect in production Rust, and what the tree’s own suite is actually detecting when it kills it

mutation over formal/comutants.toml::BugBackupSealedNotAGate scripts/comutate.py::armed_subject crates/rsk-fido/src/reset_assurance_tests.rs::a_backup_seal_swept_with_the_secrets_is_a_reopened_export_window. cfg: none. features: none — the slice the row names is cargo test -p rsk-fido on the default feature set.

Bound	Value	What stops being proved
`bound_twins`	`1`	any defect of this shape nobody registered. One comutant credits this clause, against the parent’s three, so a variant that re-opens the window some other way has no code-level verdict here
`bound_patch_hunks`	`1`	the CLASS the hunk belongs to. One hunk drops one alternative from one match arm; a defect that needed two edits, or an edit anywhere but that arm, is not expressed
`bound_patched_files`	`1`	a defect that has to span two files — which the two-consumer shape above makes plausible and no comutant covers
`bound_slice_crates`	`1`	any test outside `cargo test -p rsk-fido`, and any schedule but the weekly one — no row of `scripts/check.sh` re-drives this
`bound_deterministic_killers`	`1`	the two transcribers and the coin flip, which is the whole point of the count. Three tests in the slice go red on this patch and only one of them is about the defect; the other three killers are recorded in the mutation register rather than counted here

Row note (shipped_relation). formal/comutants.toml:188 carries status = "patch" and expect = "killed", which that file’s own vocabulary at formal/comutants.toml:19-21 defines as a RECORDED verdict and not a plan. It is re-driven by the weekly comutate run and by no row of scripts/check.sh. THE ROW ALSO CARRIES ITS OWN CORRECTION, and it is the longest note in that file: it was status = "unreachable" on a verdict MEASURED IN THE MODEL AND WRITTEN ABOUT THE CODE. What the code answers is recorded in the register below, with which part of it this bundle re-measured and which it inherited

Method 7 — the fuzz rung: what the byte-granular probe’s oracle asserts about this clause, read rather than run

Bound	Value	What stops being proved
`bound_oracle_conjuncts`	`2`	any verdict finer than the two. The oracle at fuzz/fuzz_targets/power_cut.rs:194-204 is one boolean expression whose first conjunct folds the two sibling clauses and whose second is this one, so a failure names the function and the reader has to know which conjunct is which
`bound_separable_asserts`	`1`	the separation the two tiers above have. One assertion covers all three clauses, so a passing run cannot distinguish a clause that was exercised from one the fixture made vacuously true
`bound_snapshot_valuations`	`1`	the other snapshot valuations. `reset_probe` writes `EF_CRED`, `EF_PIN`, `EF_ALWAYS_UV` and `EF_BACKUP_SEALED` before the reset at fuzz/fuzz_targets/power_cut.rs:229-232, so `snap.sealed` is TRUE by construction and the symbolic draw the Kani harness makes over it never happens here
`bound_cut_budget_bytes`	`1048575`	a power cut later in the write stream than the budget allows. The cut point is `u32::from_be_bytes([0, data[1] & 0x0f, data[2], data[3]])` at fuzz/fuzz_targets/power_cut.rs:236-241, so a tear further in than that is not a prefix this target can produce

Row note (shipped_relation). the probe drives the REAL rsk_fido::reset::reset over a cuttable mock NOR, then mounts a fresh store, runs boot-time seed provisioning and boots a second time. It is the strongest rung below the board, and it is the ONLY rung of this clause’s ladder where the RAM copy of the seed is drawn: data[4] & 1 loads state.keydev_dec at fuzz/fuzz_targets/power_cut.rs:244-246, which is what makes owner_reachable in the oracle mean more than the flash record. No log of any run is in the tree and none is in this bundle

Method 8 — the board rung, and what its column is worth: this clause OWNS an assertion on hardware, and no run of it has ever been recorded

accepted risk over tests/29_reset_power_cut.py::cut_during_reset. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_recorded_runs`	`0`	everything the board rung would say. The `test` column counts a FILE that names the invariant; no run is recorded anywhere, so nothing here is evidence that a real supply cut on real silicon preserves this clause. `PLAT-FLASH-001` owns the missing result and is `pending`, and its own board record reads `outcome = "planned"`
`bound_clause_asserts`	`1`	nothing this clause needs — and it is the one place in the whole ladder where THIS clause is better off than its siblings. `tests/29_reset_power_cut.py:537` asserts `current != owner_seed` under its own name; the sibling clauses share one folded assertion at `tests/29_reset_power_cut.py:526-527` that says only that the operation was refused, without saying which gate refused it
`bound_flavours`	`1`	the display flavour’s second surface. The script drives the host `BACKUP_STATE` and `read_seed` path only, so the on-device recovery-phrase reveal — the marker’s other consumer — has no board assertion at any rung

Row note (shipped_relation). the script needs a throwaway board, the no-touch image, and either an operator’s hand or a relay, and it can exit inconclusive when the reset finishes before power goes. Its clause-C arm is conditional: it reads BACKUP_STATE, and only when the device reports NOT sealed does it try to read the seed back and assert it changed. So a board run in which the marker survived the cut passes this arm without exercising it, which is the correct shape for the property and worth saying out loud beside a column that reads one

`SEC-FIDO-007` — `RamNeverOutlivesFlashSeed`

Method 1 — the invariant over the whole reachable space of the shipped constants

model-check over formal/RSKeySecurityState.tla::RamNeverOutlivesFlashSeed + Shipped.cfg::RamNeverOutlivesFlashSeed. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_rps`	`2`	nothing this invariant can express — `ram => store.seed` names two booleans and no constant. What two costs is reach alone: a falsifying state that first arises over a third relying party is not in the set searched
`bound_channels`	`2`	nothing this invariant can express; what two costs is reach — a falsifying state first arising over a third concurrent channel is not in the set searched
`bound_max_retries`	`8`	nothing at all. The ladder is off this property’s path and eight IS the shipped value, so this axis is neither a shrink nor a term
`bound_mismatch_limit`	`3`	nothing at all, for the same reason as the ladder it pairs with
`bound_max_clock`	`1`	nothing this invariant can express. What one Tick costs is reach: a falsifying state needing a second unit of elapsed time is not in the set searched
`bound_reset_window`	`0`	nothing this invariant can express. What zero costs is reach: a reset started inside the shipped window is a prefix no run here produces

Row note (shipped_relation). MaxRetries and MismatchLimit ARE the shipped MAX_PIN_RETRIES (8) and PIN_MISMATCH_LIMIT (3) at crates/rsk-fido/src/consts.rs:368,372; RPs and Channels are 2 against an unbounded device; MaxClock 1 is the smallest value at which Tick is not dead; ResetWindow 0 runs the window closed only. AND NONE OF THE SIX IS ON THIS PROPERTY’S PATH: ram => store.seed names two booleans and no constant, so what the six buy is the reachable set a falsifying state would have to appear in, and what they cost this invariant is nothing it can express. That is the honest difference from SEC-FIDO-001, where MaxRetries IS the retry ladder the invariant is about

Method 2 — the same invariant on the arm of AlwaysUvShipped the default image does not build

model-check over AlwaysUv.cfg::RamNeverOutlivesFlashSeed. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_rps`	`2`	a falsifying state that first arises over a third relying party, on the alwaysUv arm — reach again, since the invariant names no relying party
`bound_channels`	`2`	a falsifying state that first arises over a third concurrent channel, on the alwaysUv arm
`bound_max_retries`	`2`	nothing this invariant can express: neither constant appears in `ram => store.seed`, so six rungs off the ladder is free here in a way it is not for SEC-FIDO-001
`bound_mismatch_limit`	`1`	nothing this invariant can express, for the same reason
`bound_max_clock`	`1`	any falsifying state needing a second unit of elapsed time, on this arm as on the shipped one
`bound_reset_window`	`0`	the in-window arm, on this arm as on the shipped one

Row note (shipped_relation). the retry ladder is REDUCED here and the shipped one is not — 8:3 becomes 2:1 (formal/AlwaysUv.cfg:6-7) — because the arm buys the alwaysUv reachability question and Shipped.cfg is the row that is about the ladder. For THIS invariant the shrink is free in a way it is not for SEC-FIDO-001: neither constant appears in ram => store.seed. What the row does buy is that both arms of a registered standing assumption run against this property, which SEC-FIDO-001 also has and the other MODELLED-ONLY rows mostly do not

Method 3 — non-degeneracy: the invariant CAN go red, and the red names it rather than a sibling

model-check over Solo_RamNeverOutlivesFlashSeed.cfg::BugStateResetAfterWipe. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_invariants`	`2`	anything about the rest of the invariant set — and the isolation is not optional here: the two structural facts are kept OUT of the model’s all-invariants block, and the Mut_ twin under this same switch is recorded going RED on a SIBLING’s name
`bound_armed_switches`	`1`	any defect needing two switches at once. One armed switch is what makes this the only place in the tree where this property is observed to fail
`bound_rps`	`2`	a falsifying state that first arises over a third relying party, on the one row where this invariant is seen to fail
`bound_channels`	`2`	a falsifying state that first arises over a third concurrent channel, on that same row

Row note (shipped_relation). the configuration checks TypeOK and this invariant and NOTHING ELSE (formal/Solo_RamNeverOutlivesFlashSeed.cfg:50-52), and arms BugStateResetAfterWipe alone with every other Bug* FALSE — which is what tells this kill from a neighbouring invariant’s. It is needed here in a way it is not on Shipped.cfg: formal/gen-configs.sh:109-114 keeps the two structural facts OUT of ALL_INV precisely so a mutant reports the first invariant it violates, and formal/runs.toml:93 records Mut_BugStateResetAfterWipe.cfg going RED: ResetNeverWeakensSurvivingState — a SIBLING’s name — under the same switch. So the Solo row is the only place in the tree where this property is observed to fail

Method 4 — the production side: which sites own the antecedent, and whether the tagged owner is one of them

review over crates/rsk-fido/src/seed.rs::ensure_seed + crates/rsk-fido/src/state.rs::clear_keydev_dec + crates/rsk-fido/src/lib.rs::load_keydev. cfg: none — every writer and reader above is unconditional production code; the two projection sites are not, and the bound counts them apart for that reason. features: none.

Bound	Value	What stops being proved
`bound_tagged_owners`	`1`	any owner outside the one tagged site. This is a count of SITES and not a shrink of a shipped constant, because a review has no other unit
`bound_ram_writer_sites`	`4`	a writer the grep did not reach. Four are one producer and three destroyers, and a count of them says which sites write the RAM copy, never that they run in an order the implication needs
`bound_ram_reader_sites`	`4`	anything about what a reader DOES with the copy it read. Four sites read it and the count is of sites, not of uses
`bound_projection_sites`	`2`	nothing about a shipped image — both projection sites are cfg-gated and neither is in one. They are counted apart for that reason, so no bound here credits them as production coverage
`bound_files_in_argument`	`6`	anything in a seventh file — and the measurement is the point: the slice page estimated three files, named the tag’s file, and missed both writers and the ordering site
`bound_crates`	`2`	a site outside the two crates. A holder of the RAM copy in a third would be outside the argument

Row note (shipped_relation). the four writers are one producer (vendor.rs:592) and three destroyers (vendor.rs:591, config.rs:428, and reset.rs:104 through FidoState::reset -> Drop); the four readers are crates/rsk-fido/src/lib.rs:106, config.rs:415, config.rs:421 and vendor.rs:967; the two projection sites are crates/rsk-device/src/ctap.rs:221 and crates/rsk-fido/src/reset_assurance.rs:49 and BOTH are cfg-gated, so neither is in a shipped image. Six files and two crates against the THREE files docs/authorization-slice.md:484-487 estimated (seed.rs, state.rs, lib.rs) — the estimate named the tag’s file and missed both writers and the ordering site, and seed.rs is the one of the three that contains no keydev_dec at all. This bound is a count of sites, not a shrink of a shipped constant, because a review has no other unit

Method 5 — the code twin: the same defect injected into production Rust is caught by the tree’s own suite

mutation over formal/comutants.toml::BugStateResetAfterWipe + scripts/comutate.py + crates/rsk-fido/src/reset_tests.rs::a_torn_reset_never_leaves_the_session_running_on_a_wiped_seed. cfg: none. features: none — the slice is cargo test -p rsk-fido on the default feature set.

Bound	Value	What stops being proved
`bound_patch_hunks`	`2`	any defect the two hunks cannot express. They move one call behind another in the shipped file, which is the historical regression and not the class it belongs to
`bound_patched_files`	`1`	a defect that has to span two files
`bound_slice_crates`	`1`	any test outside the one crate the slice runs
`bound_credited_configurations`	`1`	what the killing TEST is about. The one credit exists only because the index reads solo configurations by invariant name; the test that falls is not a test of this property, and the source says so

Row note (shipped_relation). the patch moves ctx.state.reset() from ahead of the flash work to behind ensure_seed (formal/comutants.toml:353-366) — the E76 regression, in the shipped file, not a model edit — and expect = "killed" is a RECORDED verdict per that file’s own status vocabulary (:19-21), not a plan. The one credited configuration is Solo_RamNeverOutlivesFlashSeed.cfg, which comutate.solo_index reads BY INVARIANT NAME (scripts/comutate.py:337-365); without that reading the kill is credited to SEC-FIDO-006 and this row’s column is the co = 0 docs/authorization-slice.md:455-469 describes correcting. What the column does NOT say, and the source says so in as many words, is that the killing TEST is a test of this property

`SEC-FIDO-008` — `NoLiveTokenWithoutPinRecord`

Method 1 — the invariant over the whole reachable space of the shipped constants

model-check over formal/RSKeySecurityState.tla::NoLiveTokenWithoutPinRecord + Shipped.cfg::NoLiveTokenWithoutPinRecord. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_rps`	`2`	nothing this invariant can express — `tok.live => pin.set` names two booleans and no relying party. What two costs is reach alone
`bound_channels`	`2`	nothing this invariant can express; what two costs is reach — a falsifying state first arising over a third concurrent channel is not in the set searched
`bound_max_retries`	`8`	nothing by shrinking: eight IS the shipped ladder, and this constant is ON this property’s path, because the only producer of the antecedent is reachable only through a successful PIN attempt. So the approach runs at full shipped depth here and is reduced on all three arms below
`bound_mismatch_limit`	`3`	nothing by shrinking, for the same reason as the ladder it pairs with — three IS the shipped mismatch limit and the antecedent’s approach passes through it
`bound_max_clock`	`1`	any falsifying state that needs a second unit of elapsed time
`bound_reset_window`	`0`	the in-window arm. At zero the reset that clears the PIN record is reached only outside the power-up window

Row note (shipped_relation). MaxRetries and MismatchLimit ARE the shipped MAX_PIN_RETRIES (8) and PIN_MISMATCH_LIMIT (3) at crates/rsk-fido/src/consts.rs; RPs and Channels are 2 against an unbounded device; MaxClock 1 is the smallest value at which Tick is not dead; ResetWindow 0 runs the window closed only. FOUR of the six are off this property’s path — tok.live => pin.set names two booleans and no constant — but two are NOT, and that is the difference from the counterpart: MaxRetries and MismatchLimit bound the PIN-attempt ladder, and GetPinToken (the only producer of the antecedent) is reachable only THROUGH a successful PinAttempt. A ladder of 8 is the shipped one, so the antecedent’s own approach is at full shipped depth here and reduced on the three arms below

Method 2 — the same invariant on the arm of AlwaysUvShipped the default image does not build

model-check over AlwaysUv.cfg::NoLiveTokenWithoutPinRecord. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_rps`	`2`	a falsifying state that first arises over a third relying party, on the alwaysUv arm
`bound_channels`	`2`	a falsifying state that first arises over a third concurrent channel, on the alwaysUv arm
`bound_max_retries`	`2`	the six rungs between two and the shipped eight, and it costs more here than for the counterpart property: the ladder is on the antecedent’s approach path, so this arm reaches a live token over a shallower PIN-attempt sequence than the image has
`bound_mismatch_limit`	`1`	the two mismatches between one and the shipped three, on the same approach path
`bound_max_clock`	`1`	any falsifying state needing a second unit of elapsed time, on this arm
`bound_reset_window`	`0`	the in-window arm, on this arm as on the shipped one

Row note (shipped_relation). the retry ladder is REDUCED here and the shipped one is not — 8:3 becomes 2:1 (formal/AlwaysUv.cfg:6-7) — because the arm buys the alwaysUv reachability question and Shipped.cfg is the row that is about the ladder. It matters MORE for this property than for the counterpart: the ladder is on the antecedent’s approach path, so this arm reaches tok.live over a shallower PIN-attempt sequence than the shipped image has. What it buys is that the guard whose inertness this invariant licenses — ~(gate.alwaysUv /\ ~pin.set) at RegisterStart:935 and AssertStart:1056 — is checked on the arm where gate.alwaysUv is the compiled default, which is the only arm where that conjunct can be reached with a live guard

Method 3 — the same invariant with the permission domain widened to all sixteen subsets

model-check over PermWide.cfg::NoLiveTokenWithoutPinRecord. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_rps`	`1`	the second relying party. One is the price this row pays for the wide permission domain, and it is harmless to this implication, which names no relying party at all
`bound_channels`	`2`	a falsifying state that first arises over a third concurrent channel, on the wide-permission arm
`bound_max_retries`	`2`	the six rungs between two and the shipped eight, on the approach to the antecedent
`bound_mismatch_limit`	`1`	the two mismatches between one and the shipped three, on that same approach
`bound_perm_subsets`	`16`	nothing — sixteen is the whole four-bit domain and this axis is a WIDENING. What it does not buy is reach on this property: `tok.live` is a flag and not a set, so the permission domain is off the implication and this row is a second arm of a standing boolean rather than new depth

Row note (shipped_relation). WidePerms draws ps from SUBSET Perms rather than from PermSets’ five, so the sixteen are the whole four-bit domain and this bound is not a shrink — it is the widening PLAT-MODEL-001 exists for. RPs falls to 1 to pay for it (formal/PermWide.cfg:4), which is a REAL narrowing on this row and a harmless one: the implication names no rp, and GetPinToken’s r \in RPs \cup {NoRp} only decides which credential a token is bound to. The permission set is likewise off the implication — tok.live is a flag, not a set — so what this row buys is a second arm of a standing boolean rather than new reach on the property

Method 4 — the same invariant with EF_MINPINLEN’s forced-PIN-change gate modelled

model-check over ForceChange.cfg::NoLiveTokenWithoutPinRecord. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_rps`	`1`	the second relying party, dropped on this arm as on the wide-permission one and harmless for the same reason
`bound_channels`	`2`	a falsifying state that first arises over a third concurrent channel, on the forced-change arm
`bound_max_retries`	`2`	the six rungs between two and the shipped eight, on the approach to the antecedent
`bound_mismatch_limit`	`1`	the two mismatches between one and the shipped three, on that same approach
`bound_gate_bits`	`5`	any gate state the record’s five fields cannot hold. Five is a count of the MODEL’s own structure and not a compressed shipped constant — the reset’s gate-record list is five as well, and the two fives are not the same five

Row note (shipped_relation). ForceChangeModelled TRUE puts gate.forceChange in play, and it is the one standing boolean of the three that lands directly on this property’s antecedent: PLAT-MODEL-010 records that the flag REFUSES token issuance after a correct PIN, so this arm is the only one where a successful PinAttempt does not reach tok' = [live \|-> TRUE, …]. The five gate bits are the record fields gate carries (ppuat, ppuatStale, alwaysUv, backupSealed, forceChange), which is a count of the model’s own structure and not a compressed shipped constant — the reset’s own gate-record list is five too (reset.rs:251) and the two fives are not the same five

Method 5 — non-degeneracy: the invariant CAN go red, the red names it rather than a sibling, and the counterexample lands on the untagged half

model-check over Solo_NoLiveTokenWithoutPinRecord.cfg::BugStateResetAfterWipe. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_invariants`	`2`	anything about the rest of the invariant set — and the isolation is not optional here: the two structural facts are kept out of the all-invariants block, and the Mut_ twin under this same switch is recorded going RED on a sibling’s name
`bound_armed_switches`	`1`	any defect needing two switches at once. One armed switch is what makes this the only place in the tree where this property is observed to fail
`bound_counterexample_states`	`12`	nothing — twelve is the counterexample’s MEASURED length and not a bound the configuration imposes. What it carries is the evidence: the falsifying state is reached only after the gate sweep, which is the untagged half
`bound_rps`	`2`	a falsifying state that first arises over a third relying party, on the one row where this invariant is seen to fail
`bound_channels`	`2`	a falsifying state that first arises over a third concurrent channel, on that same row

Row note (shipped_relation). the configuration checks TypeOK and this invariant and NOTHING else (formal/Solo_NoLiveTokenWithoutPinRecord.cfg:50-52) and arms BugStateResetAfterWipe alone with every other Bug* FALSE — measured, armed_count over that file is 1. It is needed here for the reason formal/gen-configs.sh:109-114 gives in as many words: the two structural facts are kept OUT of ALL_INV so a mutant reports the first invariant it violates, and formal/runs.toml:93 records Mut_BugStateResetAfterWipe.cfg going RED on a SIBLING’s name under the same switch. So this is the only place in the tree where this property is observed to fail. The twelve states are the counterexample’s length and not a bound the configuration imposes — a review-shaped bound in a model-check row, and it is here because the depth is the evidence: the falsifying state is reached only after ResetSweepGates, which is the untagged half

Method 6 — the production side: which sites own each half of the implication, and whether the one tag is on a half that can falsify it

review over crates/rsk-fido/src/clientpin.rs::issue_token + crates/rsk-fido/src/state.rs::begin_using_token + crates/rsk-fido/src/reset.rs::reset. cfg: none — every site above is unconditional production code except crates/rsk-fido/src/conformance/mod.rs:165, which is cfg(test) and is counted apart in owners_antecedent rather than in these bounds. features: none.

Bound	Value	What stops being proved
`bound_tagged_owners`	`1`	any owner outside the one tagged site — and which HALF it is on: the tag sits on the antecedent, and the half with the recorded history is the consequent. This is a count of SITES and not a shrink of a shipped constant, because a review has no other unit
`bound_antecedent_sites`	`4`	an antecedent site the review did not open. Four were read, one of them the record gate the door runs first, and a count of sites says which they are and never that the order between them holds
`bound_consequent_sites`	`5`	anything about what a consequent site DOES. Five sites clear or overwrite the record, and the count names them without saying that each leaves the implication standing
`bound_production_token_callers`	`1`	coverage of the caller outside a shipped image. One in-image caller is counted; the `cfg(test)` site is counted apart, so no bound here credits it
`bound_files_in_argument`	`5`	anything in a sixth file — and the measurement is the point: the slice page estimated ONE file, the tag’s, which is the antecedent half only
`bound_crates`	`2`	a site outside the two crates, including any other holder of the record the consequent names

Row note (shipped_relation). the four antecedent sites are the definition (state.rs:506), its one in-image caller (clientpin.rs:425), the door above it (clientpin.rs:345) and the record gate that door runs first (clientpin.rs:685-693); the five consequent sites are reset.rs:104, the phase-2 sweep at :121, the membership predicate at :228-252, Fs::factory_wipe at crates/rsk-fs/src/fs.rs:477 and the overwriting writer at clientpin.rs:845-846. Five files over two crates, against the ONE file docs/authorization-slice.md:462-467 estimated (crates/rsk-fido/src/clientpin.rs) — the estimate named the tag’s file, which is the antecedent half only, and the half with the recorded history is in a file it did not name. THIS BOUND IS A COUNT OF SITES, not a shrink of a shipped constant, because a review has no other unit; the same weakness the counterpart recorded, at the same group

Method 7 — the code twin: what the `co = 1` column credits, which configuration attributes it, and what the killing assertion is actually about

mutation over formal/comutants.toml::BugStateResetAfterWipe + scripts/comutate.py::solo_invariants + crates/rsk-fido/src/reset_tests.rs::a_torn_reset_never_leaves_the_session_running_on_a_wiped_seed. cfg: none. features: none — the slice formal/comutants.toml names is cargo test -p rsk-fido on the default feature set.

Bound	Value	What stops being proved
`bound_patch_hunks`	`2`	any defect the two hunks cannot express. They move one call behind another in the shipped file, which is the historical regression and not the class it belongs to
`bound_patched_files`	`1`	a defect that has to span two files
`bound_credited_configurations`	`1`	the credit under the older attribution path. The single-answer resolver names a sibling’s configuration for this bug, so without the by-invariant reading this kill is credited to SEC-FIDO-006 alone
`bound_tests_asserting_the_token_half`	`0`	everything the co-refutation column implies about THIS property. Zero tests assert the token half: the twin’s one falling test asserts a seed field, and the only test that asserts both `EF_PIN` gone and the permissions cleared tears nothing, so the mutant leaves it green — the kill is credited here and is not a kill of this invariant
`bound_slice_crates`	`1`	any test outside the one crate the slice runs — and this row was not re-driven here, so the verdict it records is the tree’s own recorded status

Row note (shipped_relation). the patch moves ctx.state.reset() from ahead of the flash work to behind ensure_seed (formal/comutants.toml:364-377) — the E76 regression, in the shipped file — and expect = "killed" is a RECORDED verdict in that file’s own status vocabulary. The one credited configuration is Solo_NoLiveTokenWithoutPinRecord.cfg, reached only because comutate.solo_index reads solo-style configurations BY INVARIANT NAME; comutate.solo_invariant, the older single-answer path, resolves this bug to Solo_BugStateResetAfterWipe.cfg and answers ResetNeverWeakensSurvivingState, so the kill is credited to SEC-FIDO-006 alone. AND THE FOURTH BOUND IS THE FINDING: ZERO tests in this tree assert the token half. The twin’s one falling test asserts state.keydev_dec.is_none(); the only test that asserts both !fs.has_data(EF_PIN) and paut.permissions == 0 tears nothing, so the mutant leaves it green. This row was NOT re-run here — comutate.py run patches a shared working tree and other agents are in it — so the verdict this bundle records for it is the tree’s own recorded status, and the mutation group says so

Method 8 — the two arguments that rest on this invariant, and the measurement that says the guard it makes redundant is inert while the invariant is not

review over formal/RSKeySecurityState.tla::ConfigGuard + formal/README.md::NoLiveTokenWithoutPinRecord + formal/gen-configs.sh::EXTRA_INV. cfg: none. features: none.

Bound	Value	What stops being proved
`bound_dependent_model_sites`	`3`	any site outside the module that rests on this sentence. Three model sites were read; the Rust that carries the same conjunct is not in the count
`bound_measured_inert_conjuncts`	`1`	the inertness of any other guard. One conjunct was measured, by removing it from both call sites at once, and no other guard in the module has been checked the same way
`bound_states_changed_by_removal`	`0`	anything about the INVARIANT. The zero says the GUARD disables nothing; the invariant itself has a reachable falsifying state the moment one switch is armed, and reading the zero as a claim about the property is the confusion this row exists to refuse
`bound_transitions_changed_by_removal`	`0`	the currency of the measurement. Both zeros are the review’s, recorded in `formal/README.md` and not re-taken here — no TLC run was performed for this bundle

Row note (shipped_relation). three sites in the module rest on this sentence: ConfigGuard at :1091 carries no pin.set conjunct because config.rs:243-245 tests the MAC and PERM_ACFG and nothing else, and the two ~(gate.alwaysUv /\ ~pin.set) conjuncts at :935 and :1056 are kept only because the Rust has them. formal/README.md:929-935 records the measurement: removed from BOTH call sites the reachable space is bit-identical AND the transition count is unchanged, so the conjunct disables nothing. THE DISTINCTION THIS ROW EXISTS FOR: it is the GUARD that is inert, not the invariant. The invariant has a reachable falsifying state — 98 069 distinct, depth 12 — the moment one switch is armed. The two zeros are that measurement’s, taken by the review formal/README.md records and NOT re-taken here; no TLC run was performed for this bundle

Keyboard shortcuts

RS-Key