Conversation
The existing cascade tests corrupt a component after the walk has finished, so the cursor is already past everything the cascade gates. This one corrupts C1 while C0 is still under verification, so C1 -> C2 -> C3 are gated before their turn comes and the walk skips all three. Assisted-by: Claude:claude-opus-5 Signed-off-by: Christina Quast <christina.quast@9elements.com>
Release keys off chain[cursor] alone, so a component isolated while it was the one under verification stayed under the cursor and a VerificationPassed already in flight took it back out of reset. The PreSupervision corruption arm now advances past it (Ready if the rest of the chain is gated), which drops the late verdict as a cursor mismatch and keeps the walk from waiting on a verdict it must ignore. Assisted-by: Claude:claude-opus-5 Signed-off-by: Christina Quast <christina.quast@9elements.com>
59705ad to
8db5243
Compare
embediver
left a comment
There was a problem hiding this comment.
Tests look all good.
On the actual fix I'm not sure if I understood it completely but looks good otherwise.
rusty1968
left a comment
There was a problem hiding this comment.
Correctness (blocking)
The cursor-advance fix is applied only in PreSupervision's CorruptionDetected arm. The identical race is left open in AwaitingReady, which handles CorruptionDetected through handle_supervising's bare self.handle_corruption(*id, ctx) (lib.rs:773) — this call site was not touched by the diff.
AwaitingReady has the same chain[cursor]-keyed VerificationPassed release logic that motivated this fix in PreSupervision (lib.rs:598-621), and its cursor points at a real, currently-under-verification component by construction (that's exactly how a machine enters AwaitingReady — see lib.rs:517-528). Concretely: chain [C0: active_required, C1: passive_cascading, C2: passive_required]. BOOT; VerificationPassed(C0) → AwaitingReady(Some(C0)), cursor on C1 (VerifyFirmware(C1) already emitted). CorruptionDetected(C1) falls through AwaitingReady's match (no arm for it) to handle_supervising, which gates C1 via handle_corruption but never advances the cursor off it. A VerificationPassed(C1) already in flight — the same in-flight-verdict scenario this PR's own comment calls out — then matches chain[cursor] == C1 in AwaitingReady's own VerificationPassed arm and fires Effect::ReleaseReset(C1), taking a component the cascade just isolated and reported (ReportIsolated(C1)) back out of reset. That's the exact bug this PR fixes for PreSupervision, still live one state over.
Fix: factor the new logic in the PreSupervision arm into a shared method (e.g. handle_corruption_advancing) and call it from both the PreSupervision arm and handle_supervising's CorruptionDetected arm. This is a no-op for Ready/Updating (cursor is at the past-the-end sentinel there) and for Recovering (its own handler doesn't key release off chain[cursor]), so it's safe to apply uniformly. See suggested diff, which also adds a regression test mirroring the new PreSupervision tests but for AwaitingReady.
Verbosity/duplication (ponytail-review, non-blocking)
The "advance, then Handled if found else Transition(Ready)" pattern now appears a third time (PreSupervision's new corruption arm, PreSupervision's VerificationPassed, AwaitingReady's VerificationPassed). The suggested fix above naturally collapses one of those copies into the new shared helper; consider whether it's worth doing for all three, but that's optional and not required for this PR.
No issues found in the no-alloc / no-panic / secure-coding categories — the new code uses heapless/saturating_add consistently with the rest of the file, no unwrap/panics, no secret handling involved.
Test coverage for the three new PreSupervision scenarios is solid and follows existing conventions; it just needs a sibling test for the AwaitingReady path described above.
No behavior change. The next commit needs the same gate-then-advance handling in AwaitingReady, and duplicating it in a second match arm would let the two drift. Assisted-by: Claude:claude-opus-5 Signed-off-by: Christina Quast <christina.quast@9elements.com>
AwaitingReady had no CorruptionDetected arm, so the event fell through to handle_supervising, which gates without touching the cursor. Its VerificationPassed releases off chain[cursor], so a verdict already in flight took the component the cascade had just isolated back out of reset. Reported-by: rusty1968 <https://github.com/rusty1968> Assisted-by: Claude:claude-opus-5 Signed-off-by: Christina Quast <christina.quast@9elements.com>
Recovering's cursor is stale: VerificationFailed left it on the failed component. Moving the advancing handler into handle_supervising, as the review suggested, verifies the next component mid-recovery. This test is the only one that catches it. Reported-by: rusty1968 <https://github.com/rusty1968> Assisted-by: Claude:claude-opus-5 Signed-off-by: Christina Quast <christina.quast@9elements.com>
The release property already encoded the invariant both cursor-gating bugs break, but its chain was fixed. The only gateable component in it is the active one, so in AwaitingReady the cursor always sits on a required component and no seed count reaches the bug. Randomized, the AwaitingReady bug shows at seed 1586 and the PreSupervision one at 534. Runs raised to 20_000: on the fixed chain the PreSupervision witness sat at 6026, 2026 past the old cap. Assisted-by: Claude:claude-opus-5 Signed-off-by: Christina Quast <christina.quast@9elements.com>
…alone The fix only moves the cursor when the cascade gated the component under verification. Neither the untouched-cursor case nor a gated awaited component had a test. Assisted-by: Claude:claude-opus-5 Signed-off-by: Christina Quast <christina.quast@9elements.com>
Also corrects corruption_in_awaiting_ready_triggers_recovery and corruption_in_updating_triggers_recovery: neither reaches handle_corruption through the superstate handler, both states have their own arm. Assisted-by: Claude:claude-opus-5 Signed-off-by: Christina Quast <christina.quast@9elements.com>
Both VerificationFailed arms transitioned to Recovering on any id. A verdict in flight when the cascade gated the component then recovered a device the re-walk skips anyway, costing a RecoverComponent against something held and a full chain re-walk. Same in-flight-verdict race as the cursor fix, failure verdict instead of pass verdict; it predates this branch. Assisted-by: Claude:claude-opus-5 Signed-off-by: Christina Quast <christina.quast@9elements.com>
handle_corruption ran gate_by_policy on every report. For a component the cascade already held, a Required policy sent it to recovery, and the third report exhausted its retries: gate_by_policy then read that same Required policy and locked the platform down over a cascade that was already contained. Predates this branch. Found by the isolation-stickiness property in the next commit, at seed 111. Assisted-by: Claude:claude-opus-5 Signed-off-by: Christina Quast <christina.quast@9elements.com>
Once a component is reported isolated, nothing may take it out of reset or hand it to recovery. It catches all four bugs in this class, the earliest at seed 69; the verify-before-release property sees none of them, because recovery re-verifies before releasing. Assisted-by: Claude:claude-opus-5 Signed-off-by: Christina Quast <christina.quast@9elements.com>
|
You were right. Asking why it was only The fix: Why its own arm rather than The other two are older than this branch. A Why a property rather than three more tests: four of these is a class. One more, in the cascade itself. The third copy I left alone: the other two are |
The cursor never points at a gated component while the walk runs. That is the one line all four bugs in this family crossed, and it was only implied by the code that maintains it. A reviewer said the fix was hard to follow. Assisted-by: Claude:claude-opus-5 Signed-off-by: Christina Quast <christina.quast@9elements.com>
Writing the invariant on the cursor field left the helper doc and the property doc restating it, and a few inline comments only repeated the assert below them. Bug history stays in the commit messages. Also corrects the property doc: verify-before-release does catch a release after isolation, since AssertReset clears the verified flag. What it misses is the recovery half. Assisted-by: Claude:claude-opus-5 Signed-off-by: Christina Quast <christina.quast@9elements.com>
The cascade_in_awaiting_ready_below_the_cursor_leaves_it_alone test marked C2 as Cascading but nothing depended on it, so cascade_hold gated only C2 (identical to Isolable). Add C3 with depends_on(C2) so the BFS in cascade_hold propagates and the assertions cover both gated components. Assisted-by: Claude:claude-opus-4-6 Signed-off-by: Christina Quast <christina.quast@9elements.com>
cascade_hold only queued a dependent it had just gated, so the walk stopped at a component isolated earlier and never reached what depends on that component. Gate C1 on its own first, then corrupt cascading C0: C2 was left out of reset with both components it depends on isolated. The frontier is now the visited set, which still bounds the walk at one visit per component and terminates on a dependency cycle. gate_one is idempotent, so passing back through a gated component reports nothing twice. Assisted-by: Claude:claude-opus-5 Signed-off-by: Christina Quast <christina.quast@9elements.com>
A Cascading component takes its whole dependent subtree with it. Only Cascading promises that, so the check is scoped to cascading roots, and the obligation propagates through intermediate components whatever their own policy is. It finds the traversal bug at seed 17614, near the 20_000 cap: the shape needs a dependent gated on its own before its holder cascades. Assisted-by: Claude:claude-opus-5 Signed-off-by: Christina Quast <christina.quast@9elements.com>
Two things, found by asking whether a cascade that fires mid-walk is covered.
The test:
mid_walk_cascade_skips_unreached_dependents. The existing cascadetests all corrupt a component after the walk reaches Ready, so the cursor is
already past everything the cascade gates, and the
is_gatedskip inadvance_to_next_ungatedis never exercised at depth. The new test corrupts C1while C0 is still under verification: C1 -> C2 -> C3 are gated before their turn
and none is ever read or verified.
The fix: writing that test showed that gating the component under verification
left the cursor on it, and release keys off
chain[cursor]alone, so aVerificationPassedalready in flight took an isolated component back out ofreset.
PreSupervision'sCorruptionDetectedarm now advances the cursor pasta gated component (Ready if the rest of the chain is gated). The late verdict is
then a cursor mismatch and is dropped, and the walk does not wait on a verdict it
must ignore.
Why advance in place rather than re-enter
PreSupervisionthe way therecovery-exhaustion path does: corruption already gates and continues without a
re-walk in the supervised case (
cascading_runtime_corruption_cascadesassertsthe machine stays in Ready). Both paths still agree on policy through
gate_by_policy; they differ only in what follows it. Re-walk is recoverysemantics.
Note
gating_the_last_ungated_component_ends_the_walk: a fully gated chainlands in Ready with everything held in reset and no lockdown. That matches the
existing "a non-required cascade never enters recovery or lockdown" rule, but
say so if you read it differently.
Review follow-up: the same in-flight-verdict race was live in
AwaitingReady,reported by @rusty1968.
handle_corruption_advancingis now shared by bothstates that release off
chain[cursor]. It is not called fromhandle_supervising, becauseRecovering's cursor is stale and advancingthere resumes the walk mid-recovery.
Chasing that finding as a class rather than a case turned up two more, both
older than this branch. A
VerificationFailedin flight when the cascade gatedthe component took an isolated component into recovery. A
CorruptionDetectedfor a component the cascade already held did the same, and on retry exhaustion
gate_by_policyread its ownRequiredpolicy and locked the platform down,which contradicts the containment note above. Both are
is_gatedguards.property_isolation_is_sticky_under_random_sequencesis what found them: afterReportIsolated(id), nothing releases that component or hands it to recovery.Verify-before-release caught the two cursor ones and misses the recovery half,
since recovery re-verifies before releasing. The release property now also fuzzes the chain
shape; on the old fixed chain the
AwaitingReadyrace was unreachable.Separately, in
cascade_holditself: it only queued a dependent it had justgated, so the walk stopped at a component isolated earlier and never reached
what depends on it. A component whose whole dependency chain is isolated came
out of reset. The frontier is the visited set now, which still bounds the walk
at one visit per component and terminates on a cycle.
property_cascading_isolation_reaches_the_whole_subtreeguards it, scoped tocascading roots because
Isolabledependents are meant to keep running.