Skip to content

orchestrator: Move the cursor off a component gated mid-walk - #454

Open
chrysh wants to merge 16 commits into
OpenPRoT:mainfrom
9elements:fix-midwalk-gated-cursor
Open

chrysh wants to merge 16 commits into
OpenPRoT:mainfrom
9elements:fix-midwalk-gated-cursor

Conversation

@chrysh

@chrysh chrysh commented Aug 31, 2026

Copy link
Copy Markdown
Contributor

Two things, found by asking whether a cascade that fires mid-walk is covered.

The test: mid_walk_cascade_skips_unreached_dependents. The existing cascade
tests all corrupt a component after the walk reaches Ready, so the cursor is
already past everything the cascade gates, and the is_gated skip in
advance_to_next_ungated is never exercised at depth. The new test corrupts C1
while 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 a
VerificationPassed already in flight took an isolated component back out of
reset. PreSupervision's CorruptionDetected arm now advances the cursor past
a 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 PreSupervision the way the
recovery-exhaustion path does: corruption already gates and continues without a
re-walk in the supervised case (cascading_runtime_corruption_cascades asserts
the machine stays in Ready). Both paths still agree on policy through
gate_by_policy; they differ only in what follows it. Re-walk is recovery
semantics.

Note gating_the_last_ungated_component_ends_the_walk: a fully gated chain
lands 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_advancing is now shared by both
states that release off chain[cursor]. It is not called from
handle_supervising, because Recovering's cursor is stale and advancing
there 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 VerificationFailed in flight when the cascade gated
the component took an isolated component into recovery. A CorruptionDetected
for a component the cascade already held did the same, and on retry exhaustion
gate_by_policy read its own Required policy and locked the platform down,
which contradicts the containment note above. Both are is_gated guards.

property_isolation_is_sticky_under_random_sequences is what found them: after
ReportIsolated(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 AwaitingReady race was unreachable.

Separately, in cascade_hold itself: it only queued a dependent it had just
gated, 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_subtree guards it, scoped to
cascading roots because Isolable dependents are meant to keep running.

chrysh added 2 commits August 31, 2026 21:56
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>
@chrysh
chrysh force-pushed the fix-midwalk-gated-cursor branch from 59705ad to 8db5243 Compare August 31, 2026 20:09
@chrysh
chrysh marked this pull request as ready for review August 31, 2026 20:09

@embediver embediver left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Tests look all good.
On the actual fix I'm not sure if I understood it completely but looks good otherwise.

@rusty1968 rusty1968 left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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>
@chrysh

chrysh commented Sep 8, 2026

Copy link
Copy Markdown
Contributor Author

You were right. Asking why it was only PreSupervision turned up two more like
it.

The fix: AwaitingReady has its own CorruptionDetected arm now, calling a
shared handle_corruption_advancing.
mid_walk_cascade_in_awaiting_ready_drops_late_verdict is your scenario. The
invariant is on the cursor field now: while the walk runs, the cursor never
points at a gated component.

Why its own arm rather than handle_supervising: Recovering reaches that
handler too, and its cursor is stale, so the uniform version resumes the walk
mid-recovery. I tried it, and
corruption_during_recovery_does_not_advance_the_walk is the only one of the 93
tests that fails. Ready and Updating are no-ops as you say, so only
Recovering forces the placement.

The other two are older than this branch. A VerificationFailed in flight when
the cascade gated the component sent an isolated component into recovery. And
handle_corruption ran gate_by_policy on every report, including one for a
component already held, so a cascade-held Required component went 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. Both fixes are one-line is_gated guards.

Why a property rather than three more tests: four of these is a class.
property_isolation_is_sticky_under_random_sequences says that after
ReportIsolated(id) nothing releases that component or hands it to recovery. It
finds all four; the release property only ever caught the two cursor ones, and
misses the recovery half because recovery re-verifies before releasing. It also
fuzzes the chain shape now, which is what made your case reachable at all.

One more, in the cascade itself. 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 it: gate C1 on its own, then corrupt cascading C0, and
C2 comes out of reset with both components it depends on isolated. The frontier
is the visited set now, and
property_cascading_isolation_reaches_the_whole_subtree guards it, scoped to
cascading roots since Isolable dependents are meant to keep running. Neither
existing property saw that one: C2 was verified before release, and never
isolated.

The third copy I left alone: the other two are VerificationPassed arms where
the advance is interleaved with release bookkeeping, and PreSupervision's also
branches on ComponentKind::Active. Say so if you want it collapsed anyway.

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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants