diff --git a/docs/src/SUMMARY.md b/docs/src/SUMMARY.md
index bf6ff0e0..b7c13b51 100644
--- a/docs/src/SUMMARY.md
+++ b/docs/src/SUMMARY.md
@@ -32,3 +32,6 @@
 * [Design](./design/README.md)
   * [Pigweed Integration Overview](./design/pigweed-overview.md)
   * [pw_kernel IPC](./design/pw-kernel-ipc.md)
+  * [Orchestrator](./design/orchestrator/orchestrator-overview.md)
+    * [Verification Model](./design/orchestrator/orchestrator-model.md)
+    * [State Machine](./design/orchestrator/orchestrator-machine.md)
diff --git a/docs/src/design/README.md b/docs/src/design/README.md
index f7c767f9..5326ea94 100644
--- a/docs/src/design/README.md
+++ b/docs/src/design/README.md
@@ -13,3 +13,7 @@ of the project.
 -   [**pw_kernel IPC**](./pw-kernel-ipc.md): How to declare and use channel
     objects to communicate between two `pw_kernel` userspace processes.
     Worked example lives at `target/veer/ipc/`.
+-   [**Orchestrator**](./orchestrator/orchestrator-overview.md): The eRoT boot-sequence state
+    machine (`services/orchestrator/sm`). Covers the two-tier firmware
+    verification model (`ComponentAttrs`, eRoT gate, iRoT gate), the
+    verification boundary, and the full state/transition table.
diff --git a/docs/src/design/orchestrator/orchestrator-machine.md b/docs/src/design/orchestrator/orchestrator-machine.md
new file mode 100644
index 00000000..b7227f8a
--- /dev/null
+++ b/docs/src/design/orchestrator/orchestrator-machine.md
@@ -0,0 +1,379 @@
+# State Machine
+
+This document describes the state machine that lives in
+`services/orchestrator/sm/src/lib.rs`: its states, shared storage, entry
+actions, transition table, and the `SupervisingPlatform` superstate.
+
+```mermaid
+stateDiagram-v2
+    [*] --> PowerOnReset
+
+    PowerOnReset --> PreSupervision : PowerGood(Provisioned)
+    PowerOnReset --> Locked             : PowerGood(Unprovisioned)
+    PowerOnReset --> Locked             : PowerGood(SelfVerificationFailed)
+
+    PreSupervision --> PreSupervision : VerificationPassed [more, Passive]<br/>/ ReleaseReset · ReadFirmware · VerifyFirmware
+    PreSupervision --> AwaitingReady     : VerificationPassed [more, Active]<br/>/ ReleaseReset · ReadFirmware · VerifyFirmware
+    PreSupervision --> Ready             : VerificationPassed [chain done]<br/>/ ReleaseReset
+    PreSupervision --> Recovering        : VerificationFailed (any policy)<br/>/ RestoreGoldenImage
+
+    AwaitingReady --> AwaitingReady : VerificationPassed [more]<br/>/ ReleaseReset · ReadFirmware · VerifyFirmware
+    AwaitingReady --> Ready         : ComponentReady [chain done or cursor past end]
+    AwaitingReady --> AwaitingReady : ComponentReady [more]
+    AwaitingReady --> Recovering    : VerificationFailed (any policy)<br/>/ RestoreGoldenImage
+    AwaitingReady --> Recovering    : Timeout(id) [id == awaiting]<br/>/ RestoreGoldenImage
+
+    state SupervisingPlatform {
+        Ready         --> Updating      : UpdateRequest<br/>/ AuthenticateUpdate · StageUpdate
+        Updating      --> Ready         : UpdateVerified / ActivateUpdate
+        Updating      --> Ready         : UpdateRejected / DiscardStaged
+        Ready         --> Recovering    : CorruptionDetected<br/>/ RestoreGoldenImage
+        Updating      --> Recovering    : CorruptionDetected<br/>/ RestoreGoldenImage
+        AwaitingReady --> Recovering    : CorruptionDetected<br/>/ RestoreGoldenImage
+    }
+
+    Recovering --> PreSupervision : Restored [retry < max_retry]<br/>(re-verify)
+    Recovering --> PreSupervision : Restored [retry ≥ max_retry, Isolable/Cascading]<br/>/ AssertReset (skip — held)
+    Recovering --> Locked    : Restored [retry ≥ max_retry, Required]<br/>(self-emits RecoveryFailed) / LatchLockdown
+    Locked     --> Locked    : (terminal — all events ignored)
+```
+
+---
+
+## Shared storage — `Rot<N, E>`
+
+Every handler receives a `&mut Rot<N, E>` alongside the event and the `Sink`.
+This struct is the machine's *shared storage*: a single allocation that persists
+across events and is visible to every handler. States are a plain `State` enum
+(some variants carry a payload); all other mutable data lives here.
+
+| Field | Type | Purpose |
+|---|---|---|
+| `chain` | `Vec<(ComponentId, ComponentAttrs), N>` | Ordered trust chain, supplied by the platform driver at construction time. Never mutated after build. |
+| `cursor` | `u8` | Index of the component currently under verification. Reset to 0 on every `PreSupervision` entry. Advances on each `VerificationPassed`, and past any component marked `Isolated` in `statuses` (skipped without verification), via `Outcome::Handled`. |
+| `statuses` | `Vec<ComponentStatus, N>` | One record per chain component, parallel by index. Each `ComponentStatus` is `{ lifecycle: ComponentLifecycle, retry: u8 }`. `lifecycle` (`Nominal` / `Isolated`) marks whether the component has been gated out of service — an `Isolated` component is held in reset and skipped on every walk. `retry` is its consecutive failed-restore count, kept per component so interleaved recoveries never share a budget. Durable across a return to `Ready` (only `retry` is cleared there; `Isolated` persists); reset only by a fresh `Rot` on `PowerOnReset`. |
+| `max_retry` | `u8` | Ceiling for a component's `retry`, chosen by the platform driver. When `statuses[i].retry >= max_retry` recovery is **exhausted** and the failed component's recovery-failure policy (`Isolable`/`Cascading`/`Required`) is applied. |
+| `_effect_cap` | `PhantomData<[u8; E]>` | Zero-sized; ties the effect-buffer size `E` to the type so the `E >= 2 * N + 2` bound is enforced at construction. |
+
+Two pieces of per-episode data are **not** stored on `Rot`: the component whose
+recovery is in progress and the `Active` component whose readiness is
+outstanding. These live in the `State` payloads `Recovering(ComponentId)` and
+`AwaitingReady(Option<ComponentId>)`, so they exist only while the machine is in
+those states — the type system guarantees they cannot be read in any other.
+
+The effect buffer is deliberately **absent** from `Rot`. Effects flow through the
+`Sink` (the handler's context), which the orchestrator creates fresh for every
+event and drains afterward.
+
+---
+
+## Context — `Sink`
+
+The only thing a handler can do to the outside world is call `ctx.emit(effect)`.
+`Sink` is an append-only `heapless::Vec<Effect, E>`. It can push; it
+cannot pull, read, or do I/O. The orchestrator owns a fresh `Sink` per dispatch
+and reads the effects out after the handler returns.
+
+---
+
+## States
+
+### `PowerOnReset`
+
+The machine's initial state. The first event is always `PowerGood(PowerOnResult)`.
+
+**Entry action**: none.
+
+| Event | Guard | Effects | Next state |
+|---|---|---|---|
+| `PowerGood(Provisioned)` | — | — | `PreSupervision` |
+| `PowerGood(Unprovisioned)` | — | — | `Locked` |
+| `PowerGood(SelfVerificationFailed)` | — | — | `Locked` |
+| anything else | — | — | `Outcome::Super` (top level — discarded) |
+
+---
+
+### `PreSupervision`
+
+Walks the trust chain component-by-component. The cursor advances on each
+`VerificationPassed` (or optional `VerificationFailed`) using `Outcome::Handled`
+rather than a self-transition — a self-transition would re-run the entry action
+and reset the cursor.
+
+**Entry action**: reset `cursor` to 0 and emit `ReadFirmware` + `VerifyFirmware`
+for the first component **not** marked `Isolated` in `statuses` (`Isolated`
+components stay in reset and are skipped). The `Isolated` marks are *not* cleared
+here — they persist across re-walks so exhausted components are not re-verified.
+
+| Event | Guard | Effects | Next state |
+|---|---|---|---|
+| `VerificationPassed(id)` | more, current `Passive` | `ReleaseReset` · `ReadFirmware(next)` · `VerifyFirmware(next)` | `Handled` (cursor ++) |
+| `VerificationPassed(id)` | more, current `Active` | `ReleaseReset` · `ReadFirmware(next)` · `VerifyFirmware(next)` | `AwaitingReady(Some(id))` |
+| `VerificationPassed(id)` | chain done | `ReleaseReset(id)` | `Ready` |
+| `VerificationFailed(id)` | — | — | `Recovering(id)` — recovery is attempted first, regardless of the component's recovery-failure policy |
+| `CorruptionDetected(id)` | `Required`/unknown | `RestoreGoldenImage` | `Recovering(id)` |
+| `CorruptionDetected(id)` | `Isolable`/`Cascading` | `AssertReset` · `ReportIsolated` | `Handled` (component gated; walk continues) |
+| anything else | — | — | `Outcome::Super` (top level — discarded) |
+
+When advancing the cursor, any component marked `Isolated` is skipped without
+verification — it stays in reset and no `ReadFirmware`/`VerifyFirmware` is emitted
+for it. The recovery-failure policy (`Isolable`/`Cascading`/`Required`) is
+**not** consulted for a *passing* walk; it is applied on failure — either here on
+`CorruptionDetected`, or later in `Recovering` once restore attempts are
+exhausted.
+
+> **Corruption is handled here; attestation is not.** `PreSupervision` has no
+> superstate link, so it handles `CorruptionDetected` *directly* (the two rows
+> above) rather than inheriting the `SupervisingPlatform` behavior — a
+> corruption report during the walk still triggers recovery (`Required`) or
+> gating (`Isolable`/`Cascading`), even on an all-`Passive` chain that would
+> otherwise self-loop here for the entire walk. `AttestationChallenge`, by
+> contrast, falls through to the `anything else` row and is discarded: CSA
+> defines no requirement to answer challenges before the chain walk completes.
+> See `corruption_during_presupervision_selfloop_triggers_recovery` in
+> `tests.rs`.
+
+---
+
+### `AwaitingReady`
+
+Reached when an `Active` component passes eRoT authentication. The machine waits
+here until the component's iRoT signals readiness via `ComponentReady`. The
+speculative eRoT check for the next component (`ReadFirmware` + `VerifyFirmware`)
+was already emitted by the `PreSupervision` handler that triggered this
+transition.
+
+**Entry action**: none.
+
+| Event | Guard | Effects | Next state |
+|---|---|---|---|
+| `ComponentReady(id)` | `id != awaited` | — | `Handled` (stale/spurious — ignore, INV9) |
+| `ComponentReady(id)` | `id == awaited`, cursor in bounds | — | `AwaitingReady(None)` (readiness satisfied; walk not yet done) |
+| `ComponentReady(id)` | `id == awaited`, cursor past end | — | `Ready` |
+| `VerificationPassed(id)` | more | `ReleaseReset` · `ReadFirmware(next)` · `VerifyFirmware(next)` | `Handled` (cursor ++) |
+| `VerificationPassed(id)` | chain done | `ReleaseReset(id)` | `Ready` |
+| `Timeout(id)` | `id == awaited` | — | `Recovering(id)` |
+| `Timeout(id)` | `id != awaited` | — | `Handled` (stale — ignore) |
+| `VerificationFailed(id)` | — | — | `Recovering(id)` — recovery attempted first |
+| anything else | — | — | `Outcome::Super` → `SupervisingPlatform` |
+
+`ComponentReady` and `VerificationPassed` are independent and may arrive in
+either order. Both must be seen before the walk advances. The `AwaitingReady`
+payload (`Some(id)`) tracks whether `ComponentReady` is still outstanding — it
+becomes `None` once readiness arrives; the `cursor` tracks whether
+`VerificationPassed` is still outstanding.
+
+---
+
+### `Ready`
+
+Normal operational state: the full chain has been verified, all required
+components are released, and the machine handles attestation, update requests,
+and corruption events.
+
+**Entry action**: reset every component's `retry` to 0 (makes the cap count
+*consecutive* failures — INV7). The `Isolated` marks are **not** cleared — a
+component isolated by exhausted recovery stays held across a return to `Ready`;
+only a fresh `Rot` on `PowerOnReset` releases it.
+
+| Event | Guard | Effects | Next state |
+|---|---|---|---|
+| `UpdateRequest` | — | — | `Updating` |
+| anything else | — | — | `Outcome::Super` → `SupervisingPlatform` |
+
+---
+
+### `Updating`
+
+An update is in progress.
+
+**Entry action**: emit `AuthenticateUpdate` + `StageUpdate`.
+
+> **Rejected** here has a specific meaning from the CSA authenticated-update
+> sequence: the staged candidate failed verification — its signature did not
+> validate under the platform's provisioned DSA public key (or it failed the
+> anti-rollback/SVN check). A failed verification is answered with a reject, the
+> candidate is discarded (`DiscardStaged`), and the device keeps running its
+> current image. Rejection is therefore an *update* outcome, not a corruption of
+> the running image — hence INV4 keeps it off the recovery path.
+
+| Event | Guard | Effects | Next state |
+|---|---|---|---|
+| `UpdateVerified` | — | `ActivateUpdate` | `Ready` |
+| `UpdateRejected` | — | `DiscardStaged` | `Ready` (INV4) |
+| `CorruptionDetected(id)` | `Required`/unknown | `DiscardStaged` (then `RestoreGoldenImage` on entry) | `Recovering(id)` (update preempted; staged image discarded) |
+| `CorruptionDetected(id)` | `Isolable`/`Cascading` | `AssertReset(id)` · `ReportIsolated(id)` | `Handled` (component gated; update continues, staged image kept) |
+| anything else | — | — | `Outcome::Super` → `SupervisingPlatform` |
+
+`Updating` handles `CorruptionDetected` in its own arm rather than inheriting the
+superstate behavior, so that a *preemption* (transition out to `Recovering`) can
+emit `DiscardStaged` first — the in-flight staged image would otherwise be
+orphaned. An `Isolable`/`Cascading` corruption is gated and the update continues,
+so its staged image is kept.
+
+---
+
+### `Recovering`
+
+The machine is attempting to restore a corrupted or rejected component.
+
+**Entry action**: emit `RestoreGoldenImage(failed)`, where `failed` is the
+`Recovering(ComponentId)` payload — targets the failed component's *recovery
+region*: all components sharing the same `RegionId` are restored together. The
+core supplies the failed component ID; the platform driver resolves region
+membership from the chain at startup. Only the named component triggers the
+restore, but the
+entire region is affected (not the whole chain — INV5).
+
+| Event | Guard | Effects | Next state |
+|---|---|---|---|
+| `Restored(id)` | `id != failed` | — | `Handled` (stale — belongs to a displaced episode; the re-walk re-verifies it) |
+| `Restored(id)` | `id == failed`, `retry + 1 < max_retry` | — | `PreSupervision` (re-verify — the restored image may pass) |
+| `Restored(id)` | `id == failed`, cap reached, `Isolable` | `AssertReset(failed)` · `ReportIsolated(failed)` | `PreSupervision` (recovery exhausted: mark `failed` `Isolated`, reset its `retry`; the re-walk skips it) |
+| `Restored(id)` | `id == failed`, cap reached, `Cascading` | `AssertReset` · `ReportIsolated` (per component) | `PreSupervision` (recovery exhausted: mark `failed` + `depends_on` dependents `Isolated`) |
+| `Restored(id)` | `id == failed`, cap reached, `Required` | `ReportRecoveryFailed(failed)` · `Effect::Emit(RecoveryFailed)` | `Handled` (orchestrator queues `RecoveryFailed` next — INV7) |
+| `RecoveryFailed` | — | — | `Locked` |
+| anything else | — | — | `Outcome::Super` → `SupervisingPlatform` |
+
+("cap reached" = `retry + 1 >= max_retry`.)
+
+**Two-stage recovery (CSA-aligned).** A verification failure never skips a
+component outright. Every failure — during initial boot or a re-walk — first
+brings the machine here, to `Recovering`, which restores the failed component's
+recovery region and re-verifies. Only when the restore attempts are *exhausted*
+(`retry` reaches `max_retry` and the restored image still fails) does the
+component's **recovery-failure policy** decide what happens next:
+
+- `Isolable` — skip just this component; mark it `Isolated` (held in reset) and
+  continue booting the rest of the platform.
+- `Cascading` — skip this component *and* its `depends_on` dependents; continue
+  booting the remainder.
+- `Required` — stop entirely: self-emit `RecoveryFailed`, which drives the
+  machine to `Locked`. (CSA's narrative docs call this outcome "platform
+  halt" — same behavior, `Required` is the type-level name.)
+
+This mirrors the CSA Boot Sequence **Recovery Policy**: recovery (region restore)
+is attempted for *every* failed device first, and the `Isolable`/`Cascading`/
+`Required` classification applies only *after* a recovery attempt itself
+fails.
+
+`Effect::Emit(RecoveryFailed)` is the *feedback-as-data* mechanism. It is easiest
+to understand by asking why the machine doesn't just jump straight to `Locked`
+when a `Required` component's retry cap is hit.
+
+When a `Required` component's last restore attempt fails, the machine has a
+decision to make: give up and lock down. It could act on that decision silently,
+transitioning directly from `Recovering` to `Locked` inside the handler. Instead
+it does something that
+looks indirect at first: it emits `RecoveryFailed` as an *effect* — a piece of
+data saying "a follow-up event named `RecoveryFailed` should happen next" — and
+returns. The orchestrator sees that effect, puts `RecoveryFailed` at the front of
+the queue, and dispatches it right away. That second event is what actually moves
+the machine to `Locked`.
+
+The payoff is that the give-up decision becomes a visible event rather than a
+hidden jump. Anyone reading the effect trace sees `RecoveryFailed` appear at the
+exact moment the cap was reached, and `Locked` is only ever entered one way — by
+handling that event — no matter where the lockdown was triggered from. The core
+never reaches out and changes its own state behind the scenes; every transition,
+including its own internally-generated ones, travels through the same event path
+and shows up in the same trace.
+
+**Why re-walk from `cursor = 0`?** After restoring a component the machine
+re-enters `PreSupervision` and re-verifies the entire chain from scratch
+rather than resuming at the failed component. This is a deliberate conservative
+policy: a corruption event may indicate a broader integrity problem, and the
+CSA architecture's core principle — "no component executes unverified firmware"
+(NIST SP 800-193) — requires that trust be re-established end-to-end before the
+platform is considered healthy again. The CSA document does not prescribe the
+exact recovery sequencing, but the re-walk implements the spirit of that
+principle. Components already marked `Isolated` — those whose recovery was
+exhausted under an `Isolable` or `Cascading` policy — are skipped during the
+re-walk: they stay in reset and are not re-verified. Every other component is re-verified from
+scratch, and a fresh failure restarts the two-stage recovery for that component.
+
+---
+
+### `Locked`
+
+Terminal state. All events are discarded.
+
+**Entry action**: emit `LatchLockdown` — instruct the platform driver to hold
+all components in reset permanently.
+
+---
+
+## Superstate — `SupervisingPlatform`
+
+`Ready`, `Updating`, `Recovering`, and `AwaitingReady` share this superstate.
+When a leaf state returns `Outcome::Super`, the engine calls the superstate
+handler (`handle_supervising`).
+
+| Event | Guard | Effects | Next state |
+|---|---|---|---|
+| `AttestationChallenge` | — | `SignAttestation` | `Handled` (no transition — INV6) |
+| `CorruptionDetected(id)` | `attrs.failure_policy == Required` | — | `Recovering(id)` (INV5) |
+| `CorruptionDetected(id)` | `attrs.failure_policy != Required` | `AssertReset(id)` · `ReportIsolated(id)` | `Handled` (component gated; machine stays in current state) |
+| anything else | — | — | `Outcome::Super` (discarded) |
+
+---
+
+## Centralizing the Supervision Contract
+
+Four states run once the platform is up: `Ready`, `Updating`, `Recovering`, and
+`AwaitingReady`. Two rules must hold in all four — an attestation challenge is
+always answered, and a corruption report always starts recovery. Rather than
+copy those rules into each state (where they can silently drift), the four states
+sit under one superstate, `SupervisingPlatform`, that holds the **supervision
+contract** exactly once. When a leaf state does not handle an event, it falls
+through to the superstate handler, so each state handles what is unique to it and
+the parent handles what they all share. This matters most for the in-between
+states — `AwaitingReady` (still booting) and `Recovering` (still restoring) —
+which are the easy ones to forget: putting them under the same parent means the
+corruption rule applies to them automatically.
+
+---
+
+## Invariant Catalogue
+
+The numbered invariants originate as docstrings on the tests that pin them in
+`services/orchestrator/sm/src/tests.rs`; the transition tables above cite them by
+number. This catalogue is the consolidated list — each invariant is enforced by
+the named test(s).
+
+| # | Invariant | Verified by |
+|---|---|---|
+| INV1–INV3 | Provisioned power-on walks the chain **in order**; no component is released before its eRoT-side verification passes. | `cold_boot_walks_chain_in_order` |
+| INV4 | A rejected update rolls back via `DiscardStaged` and **never** enters `Recovering` — update failure is not corruption. | `update_rollback_is_not_recovery` |
+| INV5 | Runtime corruption targets the **named** component and re-walks the chain from the top after restore. | `runtime_corruption_targets_component_and_rewalks` |
+| INV6 | `AttestationChallenge` is answerable from **every** `SupervisingPlatform` state, with no transition. | `attestation_shared_across_supervising_platform_states` |
+| INV7 | Recovery retries count **consecutive** failures only; after `MAX_RETRY` restores the core self-emits `RecoveryFailed` and latches `Locked`; a successful recovery resets the count. | `retry_cap_self_latches_via_emit`, `retry_count_resets_after_successful_recovery` |
+| INV8 | Verify-before-release (whole-input-space): across arbitrary event sequences, a component is released only if it was verified since its most recent hold — never on a verification from before it was last taken down. This is the fuzz-checked form of "recovery is a re-boot". | `property_verify_before_release_holds_under_random_sequences` |
+| INV9 | A `ComponentReady` for a component other than the awaited one is silently ignored. | `spurious_component_ready_is_ignored` |
+| INV10 | An `Active` component **gates** the chain walk — the cursor does not advance past it until its `ComponentReady` arrives. | `active_component_gates_on_component_ready` |
+| INV11 | `SelfVerificationFailed` at power-on latches `Locked` immediately, without entering `PreSupervision`. | `self_verification_failure_latches_immediately` |
+| INV12 | `AttestationChallenge` is also handled in `AwaitingReady`. | `attestation_in_awaiting_ready` |
+
+---
+
+## Invariant Verification
+
+The invariants for the `SupervisingPlatform` superstate describe the whole
+superstate, not one state at a time. Because the hierarchy stores each rule at
+that same superstate level, verifying an invariant is checking one authoritative
+copy of the rule plus the four links into it — not reconciling four independent
+copies spread across per-state tables.
+
+| Invariant | Where it lives | To verify |
+|---|---|---|
+| INV6 — attestation answered in any `SupervisingPlatform` state, no transition | `AttestationChallenge → SignAttestation`, `Handled` (one row in `SupervisingPlatform`) | Read one row + confirm four states link to `SupervisingPlatform` |
+| INV5 — corruption triggers recovery from any `SupervisingPlatform` state | `CorruptionDetected → Recovering` (one row in `SupervisingPlatform`) | Read one row + confirm four states link to `SupervisingPlatform` |
+
+A state that forgets to link, or handles the event itself, silently drops out of
+the rule — so the four links do matter. The win is that the safe thing is the
+easy thing: a state that does nothing falls through to the shared rule.
+
+
+`initial()` is a `fn() -> State` with no `self`, so the machine always starts
+in `PowerOnReset`. The `PowerGood(PowerOnResult)` event supplied by the platform
+driver is the first real branching point.
diff --git a/docs/src/design/orchestrator/orchestrator-model.md b/docs/src/design/orchestrator/orchestrator-model.md
new file mode 100644
index 00000000..3d39187d
--- /dev/null
+++ b/docs/src/design/orchestrator/orchestrator-model.md
@@ -0,0 +1,430 @@
+# Verification Model
+
+This document describes how platform firmware verification is modelled in the
+orchestrator state machine (`services/orchestrator/sm`): the problem it solves,
+the types that carry the domain, the states that sequence the work, and the
+boundary between the pure core and the platform that executes it.
+
+---
+
+## 1. The Problem
+
+The eRoT (external Root of Trust — the discrete RoT device, e.g. on a DC-SCM)
+must verify every platform component's firmware before releasing it from reset.
+Two independent mechanisms do this:
+
+1. **eRoT-side**: the eRoT reads the component's firmware image from the SPI
+   flash it controls, verifies the signature and SVN against a Reference
+   Integrity Manifest (RIM/PFM), and only then releases the component from reset.
+
+2. **iRoT-side**: components with an integrated Root of Trust (e.g. a BMC SoC
+   or CPU with Caliptra) perform their own independent local self-verification
+   after reset. The eRoT must wait for this local check to complete before
+   treating the component as trusted and advancing to the next one in the chain.
+
+Components that have no integrated iRoT (e.g. a NIC) rely solely on the
+eRoT-side check. The eRoT can advance immediately after releasing them.
+
+This two-tier model — eRoT gate + optional iRoT gate — is the core problem the
+verification states solve. It is grounded directly in the CSA architecture boot
+sequence: "The eRoT and the iRoT provide complementary guarantees: the eRoT
+controls whether a component is released from reset; the iRoT controls whether
+the component's own firmware executes."
+
+The **verification boundary** is the interface between the platform and the
+pure state-machine core. Only verdicts cross it: the platform performs all
+cryptographic work (reading flash, checking signatures and SVN) and then signals
+the outcome via an event. The core never sees raw firmware data or hash values —
+it only acts on the resulting `VerificationPassed` or `VerificationFailed`. This
+keeps the core free of I/O and testable without hardware.
+
+---
+
+## 2. Domain Types
+
+### `ComponentKind`
+
+Classifies the iRoT gate for a component. Supplied by the platform at chain-build
+time; the core never derives it.
+
+```
+Active  — has an integrated iRoT (e.g. Caliptra); both eRoT and iRoT checks apply
+Passive — no integrated iRoT; only the eRoT check applies
+```
+
+In CSA terminology: `Active` corresponds to a *SoC with an integrated iRoT*
+(e.g. a BMC or CPU with Caliptra). `Passive` corresponds to a *symbiont device*
+— per NIST SP 800-193 §3.4, a device that lacks the capability to perform its
+own firmware verification and relies on an external RoT (the eRoT, or an
+intermediate RoT in a tiered model) to do so on its behalf.
+
+### `FailurePolicy`
+
+Determines what the orchestrator does when a component's firmware fails
+verification.
+
+```
+Required   — attempt recovery; re-walk the chain after `Restored`; latch
+             `Locked` if the retry cap is reached
+Isolable   — hold the component in reset; advance past it; continue the walk
+Cascading  — same as Isolable, and additionally hold in reset any component
+             whose `depends_on` names this one
+```
+
+### `RegionId`
+
+An opaque `u8` that groups components into a *recovery region*. Components
+assigned the same `RegionId` must be restored together; when any region member
+triggers `Recovering`, the platform issues a joint restore operation for the
+entire region. The core treats the id as an equality key only and never
+inspects the membership.
+
+### `ComponentAttrs`
+
+Per-component attributes:
+
+```rust
+pub struct ComponentAttrs {
+    pub kind: ComponentKind,              // iRoT gate: Active | Passive
+    pub failure_policy: FailurePolicy,    // verification-failure handling
+    pub recovery_region: RegionId,        // which components are recovered together
+    pub depends_on: Option<ComponentId>,  // cascade trigger: held if named component was skipped
+}
+```
+
+| `failure_policy` | `VerificationFailed` behaviour |
+|---|---|
+| `Required` | → `Recovering`; component held in reset; chain walk halts until restored |
+| `Isolable` | component held in reset; cursor advances; chain walk continues; no cascade to dependents |
+| `Cascading` | component marked `Isolated` (held in reset); any component whose `depends_on` matches this id is also marked `Isolated` and skipped; cursor advances; chain walk continues |
+
+A component that fails verification is **never** released from reset regardless
+of its failure policy — releasing a component whose firmware failed verification
+would mean running untrusted code, which breaks the trust invariant.
+
+`depends_on` is only meaningful when the named component has `FailurePolicy::Cascading`.
+Only `Cascading`-failed components (and their transitively cascade-skipped dependents)
+are marked `Isolated`. Before emitting `ReadFirmware` for any component, the core
+checks whether its `depends_on` names a component already marked `Isolated`; if so, the
+depending component is also held in reset and marked `Isolated` without emitting
+`ReadFirmware` or `VerifyFirmware`. This check repeats for each newly-isolated
+component's successors until no further cascade is triggered. An `Isolable` failure
+skips only the failed component; it marks nothing else `Isolated` and causes no
+downstream cascade.
+
+Convenience constructors: `ComponentAttrs::active_required()`,
+`passive_required()`, `active_isolable()`, `passive_isolable()`,
+`active_cascading()`, `passive_cascading()`.
+
+### `ComponentId`
+
+An opaque `u8` the core carries and equality-compares but never inspects. The
+platform decides which id maps to which physical device.
+
+### Events that cross the verification boundary
+
+| Event | Direction | Meaning |
+|---|---|---|
+| `VerificationPassed(ComponentId)` | platform → core | The eRoT-side check passed: signature and SVN valid. |
+| `VerificationFailed(ComponentId)` | platform → core | The eRoT-side check failed: image rejected. |
+| `ComponentReady(ComponentId)` | platform → core | An `Active` component's integrated iRoT has finished its local verification and the component is operational (e.g. MCTP channel established). |
+| `Timeout(ComponentId)` | platform → core | The platform's watchdog fired: the named `Active` component did not deliver `ComponentReady` within the platform-policy window. The platform arms the watchdog after emitting `ReleaseReset` and cancels it on `ComponentReady`. Treated as a verification failure for recovery purposes. |
+
+### Effects the core emits for verification work
+
+| Effect | Meaning |
+|---|---|
+| `ReadFirmware(ComponentId)` | Ask the platform to read the component's firmware image from eRoT-controlled flash. |
+| `VerifyFirmware(ComponentId)` | Ask the platform to verify the image against the RIM/PFM. The platform responds with `VerificationPassed` or `VerificationFailed`. |
+| `ReleaseReset(ComponentId)` | Release the named component from reset. Emitted only after `VerificationPassed`. |
+
+These are descriptions, not actions. The platform's `Platform::execute` carries
+them out; the core never touches hardware.
+
+---
+
+## 3. Sequencing by `ComponentAttrs`
+
+### Active → Passive (happy path)
+
+```
+chain: [(C0, {Active, Required}), (C1, {Passive, Required})]
+
+PreSupervision (entry):
+  emit ReadFirmware(C0)
+  emit VerifyFirmware(C0)
+
+VerificationPassed(C0):           ← eRoT check done
+  emit ReleaseReset(C0)
+  emit ReadFirmware(C1)           ← speculative eRoT check of next
+  emit VerifyFirmware(C1)
+  cursor = 1, awaiting = Some(C0)
+  → AwaitingReady
+
+ComponentReady(C0):               ← C0's iRoT done
+  awaiting = None
+  Handled (stay in AwaitingReady, wait for VerificationPassed(C1))
+
+VerificationPassed(C1):           ← speculative eRoT check resolved
+  emit ReleaseReset(C1)
+  chain done → Ready
+```
+
+### Isolable component failure (skip, continue)
+
+```
+chain: [(BMC, {Active, Required}), (NIC, {Passive, Isolable})]
+
+VerificationPassed(BMC):
+  emit ReleaseReset(BMC)
+  emit ReadFirmware(NIC)
+  emit VerifyFirmware(NIC)
+  awaiting = Some(BMC) → AwaitingReady
+
+VerificationFailed(NIC):          ← NIC firmware rejected; Isolable → skip
+  NIC stays held in reset
+  cursor advances past end
+  awaiting is still Some(BMC) → stay in AwaitingReady
+
+ComponentReady(BMC):              ← BMC iRoT done; cursor past end → Ready
+  awaiting = None → Ready
+```
+
+### Concrete example: BMC (Active, required) → HOST (Active, required) → NIC (Passive, optional)
+
+This matches the CSA single-node boot sequence.
+
+```
+chain: [(BMC, {Active, Required}), (HOST, {Active, Required}), (NIC, {Passive, Isolable})]
+
+PreSupervision (entry):
+  emit ReadFirmware(BMC)
+  emit VerifyFirmware(BMC)          ← eRoT reads and checks BMC firmware from SPI flash
+
+VerificationPassed(BMC):            ← eRoT: BMC firmware signature + SVN valid
+  emit ReleaseReset(BMC)            ← eRoT releases BMC from reset; Caliptra iRoT runs
+  emit ReadFirmware(HOST)           ← speculative: eRoT starts HOST firmware check
+  emit VerifyFirmware(HOST)           while BMC's Caliptra iRoT is still booting
+  cursor = 1, awaiting = Some(BMC)
+  → AwaitingReady
+
+ComponentReady(BMC):                ← BMC Caliptra iRoT done; MCTP channel up
+  awaiting = None
+  Handled (still in AwaitingReady, waiting for VerificationPassed(HOST))
+
+VerificationPassed(HOST):           ← eRoT: HOST firmware signature + SVN valid
+  emit ReleaseReset(HOST)           ← eRoT releases HOST from reset; Caliptra iRoT runs
+  emit ReadFirmware(NIC)            ← speculative: eRoT starts NIC firmware check
+  emit VerifyFirmware(NIC)            while HOST's Caliptra iRoT is still booting
+  cursor = 2
+  Handled (stay in AwaitingReady — still waiting on ComponentReady(HOST) and/or NIC result)
+
+ComponentReady(HOST):               ← HOST Caliptra iRoT done; BIOS/UEFI executing
+  awaiting = None
+  Handled
+
+VerificationPassed(NIC):            ← eRoT: NIC firmware valid (Passive — no iRoT gate)
+  emit ReleaseReset(NIC)
+  chain done → Ready
+```
+
+If NIC fails verification instead:
+```
+VerificationFailed(NIC):            ← NIC Isolable → skip; NIC stays held in reset
+  cursor = 3 (past end)
+  awaiting = None (already cleared by ComponentReady(HOST))
+  → Ready
+```
+
+---
+
+## 4. The Speculative Read Pattern
+
+When an `Active` component passes eRoT verification the core does three things
+in the same handler, before transitioning to `AwaitingReady`:
+
+```
+emit ReleaseReset(current)
+emit ReadFirmware(next)        ← speculative: next eRoT check starts immediately
+emit VerifyFirmware(next)      ← while current's iRoT is still booting
+cursor += 1
+awaiting = Some(current)
+→ Transition(AwaitingReady)
+```
+
+This overlaps the integrated iRoT boot time of the current component with the
+eRoT firmware read of the next. The two checks are independent (different
+hardware paths), so the overlap is safe.
+
+**Deliberate divergence from the CSA boot sequence diagram.** The CSA diagram
+shows strictly sequential ordering — for example, the BMC MCTP channel is
+established before the eRoT begins reading the CPU firmware. The
+speculative-read pattern departs from this: the eRoT starts the next
+component's firmware read as soon as the current one is released from reset,
+without waiting for `ComponentReady`. The trust guarantee is fully preserved:
+`ReleaseReset` for the next component is never emitted until that component's
+own `VerificationPassed` arrives. The overlap reduces boot time on real
+hardware where iRoT initialization can take several seconds.
+
+---
+
+## 5. Recovery Is a Re-boot
+
+A firmware check is only meaningful while its component is held in reset. This
+is a CSA/NIST principle, not an orchestrator invention: corruption detection is
+defined *at boot* and *at rest*, both operating on the firmware image in NVM
+rather than on running code, and *"the eRoT holds each downstream component in
+reset until verification is complete and then releases it"* — *"no component
+executes unverified firmware"* (CSA boot sequence; NIST SP 800-193 Protection
+and Recovery). The reason is concrete: if a component is already executing, the
+verdict says nothing about the code actually running — a live component can be
+running something other than what is in flash, and can rewrite its own flash the
+instant after the check passes. `VerifyFirmware` is therefore an *at-rest*
+operation, and the initial power-on walk is sound only because the platform
+holds every component in reset at power-on and the core releases each one
+(`ReleaseReset`) solely after its own `VerificationPassed`.
+
+Recovery re-runs that walk, so it must re-establish the same precondition. CSA
+grounds this too: recovery *activates through a reset* — its Recovery Sequence
+ends by marking the recovered slot as the boot target and *initiating a reset or
+slot-switch*, so a recovered component always re-enters service from a held,
+freshly-verified state rather than being patched live.
+
+**Design decision (orchestrator-specific):** CSA describes recovery *per
+device* — write the recovery image to the failed slot, reset that device. This
+orchestrator goes further: on re-entering `PreSupervision` the core first
+asserts reset on **every** non-isolated component, then walks the whole chain
+from a fully-held state and re-releases each part in order. Quiescing the entire
+chain (not just the failed device) is our choice, not a verbatim CSA
+requirement; it *follows from* the at-rest principle and buys two things — a
+single verification path shared with power-on, and the removal of any foothold a
+compromised neighbor may have gained after it was released. The result is one
+invariant:
+
+> Every running component was verified while held in reset, immediately before
+> it was released, since the most recent full walk. No live component is ever
+> re-verified.
+
+Re-verifying a still-live sibling from a previous walk would be meaningless: its
+earlier pass belongs to a walk that is over, and nothing has held it at rest
+since. Recovery returns the platform to a known-held state and rebuilds trust
+from there, exactly as power-on does.
+
+The strength of this rests on a platform-side precondition on `AssertReset`; see
+§6.
+
+---
+
+## 6. The Platform Boundary
+
+The orchestrator is split into a **pure core** and the **platform** that hosts
+it. The core is a deterministic state machine: it receives an `Event`, updates its
+own in-memory state, and appends `Effect` descriptions to a write-only `Sink`.
+It performs no I/O, reads no hardware, and cannot observe the result of any
+effect except as a future `Event`. Everything that touches the world — flash,
+reset lines, transports, timers, measurement results — lives in the platform.
+
+```mermaid
+graph LR
+    subgraph WORLD ["World  (board / platform)  —  examples/board.rs"]
+        W1["reads OTP/UFM<br/>hardware IRQs<br/>measurement results"]
+        W2["Platform::execute<br/>drives flash / reset<br/>SPI / I3C / MCTP"]
+    end
+
+    subgraph CORE ["Pure Core  —  src/lib.rs"]
+        ORCH["Orchestrator<br/>dispatch loop"]
+        SM["StateMachine<br/>Rot shared storage<br/>State handlers<br/>Operational superstate"]
+        SINK["Sink<br/>append-only effect buffer<br/>cannot read or do IO"]
+        ORCH --> SM
+        SM -->|"ctx.emit"| SINK
+    end
+
+    W1 -->|"Event"| ORCH
+    SINK -->|"Effect<br/>drained after each dispatch"| W2
+```
+
+Only two value types cross the boundary, and they cross in opposite directions:
+
+- **`Event` (world → core)** — the platform's report of something that already
+  happened: a verdict (`VerificationPassed`/`Failed`), a readiness signal
+  (`ComponentReady`), a timer expiry (`Timeout`), or a power-on result. Events
+  are the *only* way the core learns anything about the world.
+- **`Effect` (core → world)** — a description of work the platform should
+  perform: `ReadFirmware`, `VerifyFirmware`, `ReleaseReset`, `RecoverComponent`,
+  and so on. Effects are inert data; the core never waits on them and never
+  sees them succeed or fail directly.
+
+This inversion is what keeps the core testable without hardware: a test drives
+`Event`s in and asserts on the `Effect`s that come out, with no flash, no
+transports, and no clocks. It also fixes *where mechanism lives*. The core
+names **what** must happen to **which** component; the platform decides **how**.
+For example, `Effect::RecoverComponent(id)` says only "recover this component" —
+whether that resolves to a golden-image restore, an A/B slot swap, a streamed
+image, or a vendor-specific scheme is a platform/configuration decision, never
+encoded in the core.
+
+The core never reads flash, never checks signatures, never observes reset lines.
+It only emits descriptions. The complete split:
+
+| Responsibility | Core (`sm/src/lib.rs`) | Platform (`Platform` impl) |
+|---|---|---|
+| Chain order and `ComponentAttrs` | reads from `Rot.chain`, set by platform at startup | decides and provides |
+| Read firmware image | emits `ReadFirmware(id)` | executes: eRoT reads via SPI interposition, I3C, or other transport |
+| Verify signature / SVN | emits `VerifyFirmware(id)` | executes: eRoT checks against RIM/PFM; responds with `VerificationPassed` or `VerificationFailed` |
+| Release from reset | emits `ReleaseReset(id)` | executes: eRoT drives reset GPIO or equivalent |
+| Detect iRoT readiness | waits for `ComponentReady(id)` event | observes: integrated iRoT signals readiness (MCTP channel-up, GPIO, etc.); calls `dispatch` |
+| Per-component failure policy | checks `attrs.failure_policy` in handler | none — policy is encoded in the chain at startup |
+| Cascade-skip evaluation | checks `attrs.depends_on` against the `Isolated` components in `statuses` before emitting `ReadFirmware` | encodes the dependency graph at chain-build time |
+| Recovery region membership | reads `attrs.recovery_region` when entering `Recovering` | assigns each component to a region at chain-build time |
+
+**Reset must hold until release.** The core only emits the *ordering* of
+`AssertReset` and `ReleaseReset`; it relies on the platform to make
+`AssertReset` durable — a held quiesce, not a pulse — and to guarantee that no
+component executes between its reset assertion and its post-verification
+`ReleaseReset`. This is what makes an at-rest check meaningful, and it is the
+precondition the recovery re-boot (§5) depends on.
+
+**The core is policy-free.** It carries no tunable policy and no mechanism of
+its own — every policy input is either board-supplied config data or arrives as
+an event:
+
+- **Failure handling is data-driven.** The handlers *read* each component's
+  `FailurePolicy` from the chain and branch on it; nothing is hardcoded.
+  Fail-open vs fail-close is therefore a *per-component* configuration choice
+  (`Required` = fail-close; `Isolable`/`Cascading` = fail-open), set at
+  chain-build time.
+- **The retry cap is supplied, not baked in.** `max_retry` is a constructor
+  argument, not a constant.
+- **Timing lives outside.** The core sets no durations; `Timeout` and
+  `CommitTimeout` arrive as events from the platform's watchdogs. The core only
+  decides whether a given timeout is actionable.
+- **Mechanism is deferred.** Effects name *what* to do to *which* component;
+  the platform decides *how* (see `RecoverComponent` above).
+
+The core supervises only the components in the configured chain. If an event
+ever names a component id the chain does not contain, the core drops it: the
+id describes something the core has no model of and never released, so there is
+nothing to hold, recover, or protect. This is uniform across every event —
+verdicts, corruption reports, and liveness signals alike — so a malformed
+report from the platform can neither drive a spurious recovery nor latch the
+platform to `Locked`. It is a guard against bad input from the world, not a
+policy deployments configure.
+
+---
+
+## 7. What This Model Does Not Cover
+
+- **Self-verification of the eRoT firmware itself**: happens one boot layer down
+  (eRoT ROM + measuring bootloader) before this machine runs. The result is
+  delivered as `PowerOnResult` in `Event::PowerGood`.
+- **Attestation** (`AttestationChallenge` / `SignAttestation`): handled in the
+  `SupervisingPlatform` superstate, not part of the boot-time verification chain.
+- **Firmware update verification** (`AuthenticateUpdate`): handled in the
+  `Updating` state, distinct from boot-time chain verification.
+- **Multiple intermediate boot-progress checkpoints per component**: the CSA
+  architecture allows platform policy to require multiple intermediate
+  readiness signals before a component is considered fully booted. This model
+  simplifies that to a single `ComponentReady` event per `Active` component.
+  The platform is responsible for aggregating any intermediate signals and
+  delivering `ComponentReady` only once all platform-policy checkpoints have
+  been satisfied.
diff --git a/docs/src/design/orchestrator/orchestrator-overview.md b/docs/src/design/orchestrator/orchestrator-overview.md
new file mode 100644
index 00000000..100117ba
--- /dev/null
+++ b/docs/src/design/orchestrator/orchestrator-overview.md
@@ -0,0 +1,99 @@
+# Orchestrator State Machine
+
+The orchestrator is the eRoT's boot-sequence controller. It walks the platform
+trust chain — verifying each component's firmware and releasing it from reset in
+order — and then governs the operational lifecycle (attestation, firmware update,
+corruption recovery).
+
+It lives in `services/orchestrator/sm` as a pure state machine: it never touches
+hardware directly. Every action is described as an [`Effect`] value that the
+surrounding platform carries out; every piece of outside information arrives as an
+[`Event`]. This keeps the core testable without hardware and free of I/O.
+
+## State Topology
+
+The reachable states, the events (with guards) that drive transitions between
+them, and the effects each transition emits are all shown in the full state
+diagram in [State Machine](./orchestrator-machine.md#state-machine). That diagram
+is the single source of truth for the topology; it is not duplicated here to
+avoid the two drifting apart.
+
+## Documents
+
+- [**Verification Model**](./orchestrator-model.md): The two-tier firmware
+  verification model (eRoT gate + optional iRoT gate), the verification
+  boundary, `ComponentAttrs`, and concrete sequencing examples.
+- [**State Machine**](./orchestrator-machine.md): All states, shared storage, entry
+  actions, transition table, and the `SupervisingPlatform` superstate.
+
+## Design Principles
+
+**Effects, not actions; reads as events.** Handlers only call
+`ctx.emit(Effect::…)` to describe what should happen, and receive every piece of
+outside information in event payloads — the core never reads flash, drives a
+GPIO, opens a channel, or touches a provisioning store. The full core/platform
+split is the [Platform Boundary](./orchestrator-model.md#5-the-platform-boundary)
+in the Verification Model.
+
+**Feedback as data.** Internal follow-up signals (e.g. the retry-cap lockdown
+`RecoveryFailed`) are emitted as `Effect::Emit(event)`. The orchestrator queues
+and handles them immediately, making them visible in the effect trace rather than
+hiding them as implicit state changes. See the
+[`Recovering` state](./orchestrator-machine.md#recovering) for a worked example.
+
+**Board-supplied policy.** The core hard-codes no deployment-specific values.
+The platform supplies the trust chain (component ids, kinds, and required/optional
+policy) and the recovery-retry cap at startup.
+
+## Relationship to CSA Architecture
+
+The state machine is a direct implementation of the boot sequence described in
+the CSA architecture document:
+
+| CSA concept | State machine encoding |
+|---|---|
+| eRoT holds component in reset until firmware verified | `PreSupervision` emits `ReleaseReset` only on `VerificationPassed` |
+| Component with Caliptra iRoT requires two independent checks | `ComponentKind::Active` → `AwaitingReady` until `ComponentReady` |
+| Passive component (no iRoT): eRoT check only | `ComponentKind::Passive` → advance immediately after `ReleaseReset` |
+| Isolable component: failure skips, not blocks | `FailurePolicy::Isolable` → skip (held in reset); advance without `Recovering`; no cascade |
+| Cascading skip: failure also holds dependents | `FailurePolicy::Cascading` + `ComponentAttrs::depends_on` → cascade-skip via `statuses` (`Isolated`) |
+| Boot-progress watchdog: component must signal readiness in time | `Timeout(ComponentId)` event → `AwaitingReady` → `Recovering` |
+| Recovery scope groups components that restore together | `ComponentAttrs::recovery_region` (`RegionId`) → platform restores full region on `RestoreGoldenImage` |
+
+## Applicability Across Admissible Architectures
+
+The orchestrator is **eRoT-scoped**: one instance runs per discrete eRoT chip
+running OpenPRoT firmware. The same crate and binary are used at every such
+tier — the only difference between deployments is the chain configuration
+supplied at startup. eRoT chips not running OpenPRoT (e.g. a third-party AMC
+or a legacy DC-SCM implementation) appear as opaque `ComponentId` entries in
+the chain of the nearest OpenPRoT eRoT above them.
+
+**Model 1 — Module** (single PCIe add-in card): a discrete eRoT is optional.
+When present, it runs one orchestrator instance with a short chain containing
+the card's SoC. When absent, the module relies on the parent node's eRoT
+instance to verify and release it as a `ComponentId` in the node's chain.
+
+**Model 2 — Single Node Compute**: the DC-SCM discrete eRoT runs one
+orchestrator instance whose chain covers all critical node devices (CPU, BMC,
+NIC, storage). This is the canonical single-instance deployment.
+
+**Model 3 — Complex Heterogeneous Compute**: the three-tier hierarchy maps to
+independent orchestrator instances at each tier:
+
+- Each **AMC / EAM** (subsystem eRoT) runs one instance whose chain covers the
+  GPU or AI accelerator devices it manages.
+- The **DC-SCM node eRoT** runs one instance whose chain covers CPUs, BMC,
+  SmartNICs, storage, and the AMC/EAM chips themselves.
+
+The node eRoT treats each AMC/EAM as just another `ComponentId` — `Active` if
+the AMC has its own integrated iRoT, `Passive` if not. It has no visibility
+into the AMC's internal chain walk; it only observes the AMC's
+`VerificationPassed` / `ComponentReady` signals, like any other component.
+
+| Admissible Architecture | Orchestrator instances | Chain scope per instance |
+|---|---|---|
+| Module (eRoT present) | 1 | Card SoC |
+| Module (no eRoT) | 0 | — (verified by parent node eRoT) |
+| Single Node Compute | 1 | All node critical devices |
+| Complex Heterogeneous Compute | 1 per subsystem eRoT + 1 node eRoT | Subsystem devices / all node devices including subsystem eRoTs |
diff --git a/services/orchestrator/sm/BUILD.bazel b/services/orchestrator/sm/BUILD.bazel
new file mode 100644
index 00000000..6707f9fa
--- /dev/null
+++ b/services/orchestrator/sm/BUILD.bazel
@@ -0,0 +1,25 @@
+# Licensed under the Apache-2.0 license
+# SPDX-License-Identifier: Apache-2.0
+
+load("@rules_rust//rust:defs.bzl", "rust_library", "rust_test")
+
+rust_library(
+    name = "orchestrator_sm",
+    srcs = [
+        "src/lib.rs",
+        "src/model.rs",
+        "src/tests.rs",
+    ],
+    crate_name = "openprot_orchestrator_sm",
+    edition = "2024",
+    visibility = ["//visibility:public"],
+    deps = [
+        "@rust_crates//:heapless",
+    ],
+)
+
+rust_test(
+    name = "orchestrator_sm_test",
+    crate = ":orchestrator_sm",
+    edition = "2024",
+)
diff --git a/services/orchestrator/sm/README.md b/services/orchestrator/sm/README.md
new file mode 100644
index 00000000..c8016430
--- /dev/null
+++ b/services/orchestrator/sm/README.md
@@ -0,0 +1,55 @@
+<!-- Licensed under the Apache-2.0 license -->
+<!-- SPDX-License-Identifier: Apache-2.0 -->
+
+# orchestrator state machine (`openprot_orchestrator_sm`)
+
+Pure-reducer eRoT boot-sequence state machine. Walks the platform trust chain
+— verifying each component's firmware and releasing it from reset in order —
+then governs the operational lifecycle (attestation, firmware update, corruption
+recovery).
+
+**No I/O, no hardware.** Every action is an [`Effect`] the surrounding shell
+carries out. Every piece of outside information arrives as an [`Event`].
+
+## Key types
+
+| Type | Role |
+|---|---|
+| `ComponentId` | Opaque `u8` — the shell maps it to hardware; the core never inspects it. |
+| `ComponentKind` | `Active` (eRoT + iRoT gates) or `Passive` (eRoT gate only). |
+| `ComponentAttrs` | `kind` + `required`: if `false`, a failed component is skipped (held in reset) rather than triggering recovery. |
+| `Orchestrator<N>` | Public handle for the caller's event loop. Call `dispatch` or `dispatch_with` once per event. |
+| `Platform` | Implement this to carry out effects (drives reset GPIOs, reads flash, etc.). |
+
+## Usage
+
+```rust
+use openprot_orchestrator_sm::{
+    ComponentAttrs, ComponentId, Orchestrator, Event, PowerOnResult, State,
+};
+
+const CAPACITY: usize = 3;
+const BMC:  ComponentId = ComponentId::new(0);
+const HOST: ComponentId = ComponentId::new(1);
+const NIC:  ComponentId = ComponentId::new(2);
+
+let mut chain = heapless::Vec::<_, CAPACITY>::new();
+let _ = chain.push((BMC,  ComponentAttrs::active_required()));
+let _ = chain.push((HOST, ComponentAttrs::active_required()));
+let _ = chain.push((NIC,  ComponentAttrs::passive_optional()));
+
+let mut orch = Orchestrator::new(chain, /*max_retry=*/ 3);
+let mut board = MyBoard;
+
+orch.dispatch(&mut board, Event::PowerGood(PowerOnResult::Provisioned));
+// ...deliver VerificationPassed / ComponentReady events as they arrive...
+assert_eq!(orch.state(), State::Ready);
+```
+
+## Design docs
+
+Full domain model, verification boundary, and state transition tables are in the
+OpenPRoT book:
+
+- `docs/src/design/orchestrator/verification-model.md`
+- `docs/src/design/orchestrator/state-machine.md`
diff --git a/services/orchestrator/sm/src/lib.rs b/services/orchestrator/sm/src/lib.rs
new file mode 100644
index 00000000..5fe7e252
--- /dev/null
+++ b/services/orchestrator/sm/src/lib.rs
@@ -0,0 +1,1052 @@
+// Licensed under the Apache-2.0 license
+// SPDX-License-Identifier: Apache-2.0
+
+//! `openprot_orchestrator_sm` — the eRoT boot-sequence state machine.
+//!
+//! This is the pure-reducer core ported from `rot_reducer`. It describes side
+//! effects as [`Effect`] values rather than performing them; the surrounding
+//! OpenPRoT shell carries them out via a [`Platform`] impl. No concrete hardware
+//! appears here — the machine is generic over an opaque [`ComponentId`].
+//!
+//! See `docs/verification-model.md` and `docs/state-machine.md` in the
+//! `rot_reducer` workspace for the full domain context and design rationale.
+//!
+//! Three invariants define the boundary:
+//!   1. **Effects flow through [`Sink`]** — fresh per event, drained afterward.
+//!   2. **Feedback as data ([`Effect::Emit`])** — follow-up events are effects,
+//!      visible in the trace; used for the retry cap (INV7).
+//!   3. **Reads as events** — outside information arrives in [`Event`] payloads;
+//!      the core never reads anything directly.
+
+#![no_std]
+#![forbid(unsafe_code)]
+
+use core::marker::PhantomData;
+
+mod model;
+pub use model::*;
+
+// Internal capacities — these follow from how the machine works, not from the
+// deployment. The board owns `N` (chain length), `E` (effect-buffer size) and
+// max_retry.
+
+/// Upper bound on how many events one settle can queue: the triggering outside
+/// event, at most one `Emit` follow-up (`RecoveryFailed`, emitted at most once
+/// before latching), and at most one injected `EffectFailed` (de-duplicated in
+/// `dispatch_with` — it is idempotent and terminal, so a second is never
+/// queued). Three total; `PENDING_CAP` keeps headroom above that so the pushes
+/// in `dispatch_with` can never overflow.
+const PENDING_CAP: usize = 8;
+
+/// Compile-time floor tying the queue capacity to that worst case, mirroring
+/// `Rot::EFFECT_CAP_OK` for the effect buffer. Evaluated at build time (an
+/// anonymous `const`), so an under-sized `PENDING_CAP` fails to compile rather
+/// than risking a runtime overflow.
+const _: () = assert!(
+    PENDING_CAP >= 3,
+    "PENDING_CAP must hold one outside event + one Emit follow-up + one EffectFailed",
+);
+
+/// Result of dispatching one event to a state (or its superstate).
+enum Outcome {
+    /// Event consumed; state unchanged; no entry action runs.
+    Handled,
+    /// Change to this state and run its entry action.
+    Transition(State),
+    /// Not handled here; defer to the superstate (or discard if none).
+    Super,
+}
+
+/// The effect buffer handed to every handler, sized to `E`.
+///
+/// The only thing a handler can do to the outside world is call `emit`. The
+/// orchestrator gives each event a fresh `Sink` and drains it afterward.
+///
+/// `E` is bounded from below by the chain length: the worst single event is a
+/// full cascade (up to `N` `AssertReset`s, each paired with a `ReportIsolated`)
+/// plus the destination `PreSupervision` entry's `ReadFirmware`/`VerifyFirmware`
+/// (2), all landing in one `Sink`. The re-walk quiesce (an `AssertReset` per
+/// live component) never pushes past this bound, because gating and quiescing
+/// are mutually exclusive per component: a component the cascade isolates is not
+/// also live, so the two counts never sum above the full-cascade worst case.
+/// `Rot::new` refuses to compile unless `E >= 2 * N + 2`, so a machine that
+/// builds can never overflow this buffer.
+pub struct Sink<const E: usize> {
+    effects: heapless::Vec<Effect, E>,
+}
+
+impl<const E: usize> Sink<E> {
+    fn new() -> Self {
+        Self {
+            effects: heapless::Vec::new(),
+        }
+    }
+
+    /// Append one effect. `E` is sized so overflow is impossible for a machine
+    /// that compiles: `Rot::EFFECT_CAP_OK` proves `E >= 2 * N + 2` and no
+    /// handler emits more than `2 * N + 2` effects into one `Sink`, so the push
+    /// below can never fail. The `Err` arm is therefore dead — dropped rather
+    /// than panicked, since a runtime panic here would be unreachable code
+    /// shipped in the binary.
+    ///
+    /// The driver runs the effects from one handler in the order they were
+    /// emitted, and it does not run them as a single all-or-nothing group: if
+    /// one effect fails, the ones before it have already happened. When an
+    /// effect fails, the driver stops there — it skips the rest and injects
+    /// `EffectFailed` so the machine locks down. Stopping partway is still safe
+    /// no matter what order the effects were in: a component is only ever
+    /// released after it has passed verification, and every other effect either
+    /// tightens things (holds a component in reset, or latches lockdown) or just
+    /// reports what happened. So a batch that stops early can only leave the
+    /// platform more locked down, never less. A skipped report costs information,
+    /// not containment — and the batch was cut short by a failure that latches
+    /// lockdown anyway, which is the louder signal.
+    pub fn emit(&mut self, effect: Effect) {
+        // Dead Err arm: overflow is proved impossible by `Rot::EFFECT_CAP_OK`
+        // (`E >= 2 * N + 2`) plus the reducer never emitting more than
+        // `2 * N + 2` effects into one Sink.
+        let _ = self.effects.push(effect);
+    }
+
+    pub fn effects(&self) -> &[Effect] {
+        &self.effects
+    }
+}
+
+/// Outcome of [`Rot::gate_by_policy`]: whether a component was gated out of
+/// service. Collapses the three [`FailurePolicy`] values into the two
+/// control-flow outcomes the caller actually branches on — so the
+/// runtime-corruption path and the recovery-exhaustion path decide on the same
+/// result.
+#[derive(Clone, Copy, PartialEq, Eq, Debug)]
+enum Gating {
+    /// The component was gated (`Isolable` → itself; `Cascading` → itself and
+    /// its transitive dependents). Its reset is asserted and the walk skips it.
+    Gated,
+    /// Not a gating policy (`Required`, or an unknown/missing id). Nothing was
+    /// gated; the caller handles this in its own context — recover (at runtime)
+    /// or lock down (once recovery is exhausted).
+    NotGated,
+}
+
+/// Per-component service lifecycle. Each chain component carries one of these
+/// inside its [`ComponentStatus`], recording whether it is in normal service or
+/// gated out. The walk-phase payloads (`AwaitingReady`/`Recovering`) stay on the
+/// global [`State`] rather than here — those phases are properties of the whole
+/// machine, not of one component. Named for the *component service* axis to keep
+/// it distinct from fwmanager's trial-boot/commit (update-slot) lifecycle, which
+/// is a separate concern.
+#[derive(Clone, Copy, PartialEq, Eq, Debug)]
+enum ComponentLifecycle {
+    /// In the normal flow: held, under verification, or released. The global
+    /// `State` carries which of those the walk is in.
+    Nominal,
+    /// Durably gated out of service: has a live `AssertReset` and is skipped on
+    /// every chain walk.
+    Isolated,
+}
+
+/// One per-component record (see [`Rot::statuses`]).
+#[derive(Clone, Copy, PartialEq, Eq, Debug)]
+struct ComponentStatus {
+    lifecycle: ComponentLifecycle,
+    /// Consecutive failed-restore count (INV7: consecutive only).
+    retry: u8,
+    /// Set while this component has been released from reset but has not yet
+    /// reported its boot-progress signal ([`Event::ComponentReady`] for an
+    /// `Active` component, [`Event::Booted`] for a `Passive` one). The shell
+    /// arms a per-component watchdog on release; this bit is what a later
+    /// [`Event::Timeout`] consults to tell a real boot failure from a stale or
+    /// spurious timeout. Orthogonal to `lifecycle`: a gated component owes no
+    /// boot-progress signal, so gating clears it.
+    awaiting_boot: bool,
+    /// Set while this component has been released from reset and not since held
+    /// again — i.e. it is *live*, executing code. Set at every `ReleaseReset`,
+    /// cleared at every `AssertReset` (gating, recovery, or the pre-walk
+    /// quiesce). This is what makes recovery a genuine platform re-boot: on
+    /// re-entering [`State::PreSupervision`] the machine asserts reset on every
+    /// live component before re-verifying, so `VerifyFirmware` never runs
+    /// against code that is still executing (a live check says nothing about
+    /// what is running and is open to a post-check flash rewrite). Distinct from
+    /// `awaiting_boot`, which is cleared once the component reports in but stays
+    /// live: a booted component is `released` yet no longer `awaiting_boot`.
+    released: bool,
+}
+
+impl Default for ComponentStatus {
+    fn default() -> Self {
+        Self {
+            lifecycle: ComponentLifecycle::Nominal,
+            retry: 0,
+            awaiting_boot: false,
+            released: false,
+        }
+    }
+}
+
+/// Shared storage: data that persists across events. `N` is the chain capacity
+/// and `E` the effect-buffer size — both board choices; the core sets no
+/// default. `E` must be at least `2 * N + 2` (enforced in [`Rot::new`]).
+pub struct Rot<const N: usize, const E: usize> {
+    chain: heapless::Vec<(ComponentId, ComponentAttrs), N>,
+    cursor: u8,
+    /// One record per chain component (parallel to `chain` by index). Each
+    /// [`ComponentStatus`] holds the component's service `lifecycle` (`Isolated`
+    /// means gated out of the walk) and its consecutive failed-restore `retry`
+    /// count, kept per component so interleaved recoveries never share a budget.
+    /// Durable across a return to `Ready`; only a fresh `Rot` on `PowerOnReset`
+    /// resets it.
+    statuses: heapless::Vec<ComponentStatus, N>,
+    max_retry: u8,
+    /// Set when an update has been activated ([`Effect::ActivateUpdate`]) but
+    /// its anti-rollback floor has not yet been committed, i.e. the machine is
+    /// in the *activated-but-not-committed* window inside [`State::Ready`]. A
+    /// [`Event::BootConfirmed`] commits the floor and clears this; a
+    /// [`Event::CommitTimeout`] fired while this is set latches
+    /// [`State::Locked`] (commit-or-lock: the floor is never advanced for an
+    /// image that has not proven healthy, and the downgrade window is never left
+    /// open indefinitely). Cleared on [`Event::BootConfirmed`] (the window
+    /// closes normally) and on entry to the two states that end the window by
+    /// leaving `Ready` while still running — [`State::Updating`] (a superseding
+    /// update) and [`State::Recovering`] (corruption/timeout) — so any path that
+    /// leaves and later re-enters `Ready` resets the window without per-branch
+    /// bookkeeping. (It is *not* cleared on `Ready` entry, because activation
+    /// sets it while transitioning *into* `Ready`.)
+    pending_commit: bool,
+    /// Ties the effect-buffer size `E` to this type (zero-sized).
+    _effect_cap: PhantomData<[u8; E]>,
+}
+
+impl<const N: usize, const E: usize> Rot<N, E> {
+    /// Compile-time floor: the effect buffer must hold a full cascade (`N`
+    /// `AssertReset`s paired with `N` `ReportIsolated`s) plus the destination
+    /// `PreSupervision` entry's two effects. Forced by `new` below, so an
+    /// under-sized `E` fails to build.
+    const EFFECT_CAP_OK: () = assert!(
+        E >= 2 * N + 2,
+        "effect buffer E must be >= 2 * chain length N + 2",
+    );
+
+    pub fn new(chain: Chain<N>, max_retry: u8) -> Self {
+        let () = Self::EFFECT_CAP_OK;
+        let chain = chain.into_entries();
+        // One status record per chain component, parallel by index.
+        let mut statuses = heapless::Vec::new();
+        for _ in 0..chain.len() {
+            let _ = statuses.push(ComponentStatus::default());
+        }
+        Self {
+            chain,
+            cursor: 0,
+            statuses,
+            max_retry,
+            pending_commit: false,
+            _effect_cap: PhantomData,
+        }
+    }
+
+    /// Look up a component's attributes by id. `None` if the id is not in the
+    /// chain (should never happen for ids the core itself produced).
+    fn attrs_of(&self, id: ComponentId) -> Option<ComponentAttrs> {
+        self.chain
+            .iter()
+            .find(|(cid, _)| *cid == id)
+            .map(|(_, a)| *a)
+    }
+
+    /// Index of `id` in the parallel `chain`/`statuses` arrays. `None` if the
+    /// id is not in the chain (should never happen for core-produced ids).
+    fn status_index(&self, id: ComponentId) -> Option<usize> {
+        self.chain.iter().position(|(cid, _)| *cid == id)
+    }
+
+    /// Whether `id` names a component in the configured chain. The core only
+    /// supervises chain components, so an event that names an id outside the
+    /// chain is dropped rather than acted on — it describes something the core
+    /// has no model of and never released.
+    fn in_chain(&self, id: ComponentId) -> bool {
+        self.status_index(id).is_some()
+    }
+
+    fn is_gated(&self, id: ComponentId) -> bool {
+        self.status_index(id)
+            .is_some_and(|i| self.statuses[i].lifecycle == ComponentLifecycle::Isolated)
+    }
+
+    /// Gate one component out of service, returning `true` if this newly gated
+    /// it (`false` if already `Isolated`). Emits the paired `AssertReset` +
+    /// `ReportIsolated` only on the newly-gated transition, so reporting is
+    /// idempotent per component.
+    fn gate_one(&mut self, ctx: &mut Sink<E>, id: ComponentId) -> bool {
+        if self.is_gated(id) {
+            return false;
+        }
+        ctx.emit(Effect::AssertReset(id));
+        ctx.emit(Effect::ReportIsolated(id));
+        if let Some(i) = self.status_index(id) {
+            self.statuses[i].lifecycle = ComponentLifecycle::Isolated;
+            // A gated component is held in reset and no longer owes a
+            // boot-progress signal; drop any pending watchdog so a late
+            // `Timeout` can't drag an already-isolated component into recovery.
+            // It is also no longer live — the `AssertReset` above holds it.
+            self.statuses[i].awaiting_boot = false;
+            self.statuses[i].released = false;
+        }
+        true
+    }
+
+    /// Increment `id`'s consecutive failed-restore count and return the new
+    /// value. Counts are kept per component so that interleaved recovery
+    /// episodes for different components never share a budget.
+    fn bump_retry(&mut self, id: ComponentId) -> u8 {
+        match self.status_index(id) {
+            Some(i) => {
+                self.statuses[i].retry = self.statuses[i].retry.saturating_add(1);
+                self.statuses[i].retry
+            }
+            None => 0,
+        }
+    }
+
+    /// Drop `id`'s retry count. Called when the component recovers (passes
+    /// verification) or is gated — either way its consecutive-failure streak
+    /// ends, so a future failure starts counting fresh (INV7: consecutive only).
+    fn clear_retry(&mut self, id: ComponentId) {
+        if let Some(i) = self.status_index(id) {
+            self.statuses[i].retry = 0;
+        }
+    }
+
+    /// Record that `id` has been released and now owes a boot-progress signal.
+    /// Paired with the `ReleaseReset` emitted at each release site: the shell
+    /// arms its per-component boot watchdog there, and this arms ours. Also
+    /// marks the component *live* (`released`), which a later re-entry to
+    /// [`State::PreSupervision`] uses to quiesce it before re-verifying.
+    fn mark_released(&mut self, id: ComponentId) {
+        if let Some(i) = self.status_index(id) {
+            self.statuses[i].awaiting_boot = true;
+            self.statuses[i].released = true;
+        }
+    }
+
+    /// Clear `id`'s boot-progress watchdog because it reported in
+    /// ([`Event::ComponentReady`] or [`Event::Booted`]). Idempotent: a report
+    /// for a component not awaiting boot simply changes nothing.
+    fn clear_awaiting_boot(&mut self, id: ComponentId) {
+        if let Some(i) = self.status_index(id) {
+            self.statuses[i].awaiting_boot = false;
+        }
+    }
+
+    /// Whether `id` has been released and still owes a boot-progress signal.
+    /// A [`Event::Timeout`] is a real boot failure only for such a component;
+    /// otherwise it is stale/spurious.
+    fn is_awaiting_boot(&self, id: ComponentId) -> bool {
+        self.status_index(id)
+            .is_some_and(|i| self.statuses[i].awaiting_boot)
+    }
+
+    /// Advance `cursor` from `start_idx` to the first component not in
+    /// `gated`, emitting its `ReadFirmware`/`VerifyFirmware`. Returns `true` if
+    /// found. If the rest of the chain is exhausted or entirely gated, sets
+    /// `cursor` to a past-the-end sentinel (`chain.len()`) and returns
+    /// `false` — the caller should treat that as "chain done".
+    fn advance_to_next_ungated(&mut self, ctx: &mut Sink<E>, start_idx: usize) -> bool {
+        let mut idx = start_idx;
+        while let Some(&(id, _)) = self.chain.get(idx) {
+            if !self.is_gated(id) {
+                // `idx < chain.len() <= N`; chain capacity is board-chosen and
+                // assumed to fit `u8`, matching the existing `cursor: u8` contract.
+                self.cursor = idx as u8;
+                ctx.emit(Effect::ReadFirmware(id));
+                ctx.emit(Effect::VerifyFirmware(id));
+                return true;
+            }
+            idx += 1;
+        }
+        self.cursor = self.chain.len() as u8;
+        false
+    }
+
+    /// Hold the whole platform for an at-rest re-verification: assert reset on
+    /// every component that is currently *live* (`released`) and drop its
+    /// boot-progress watchdog, so the walk that follows verifies code that is
+    /// quiesced rather than executing. This is what makes recovery a genuine
+    /// platform re-boot — no released component is ever re-verified while it is
+    /// still running (a live check says nothing about what is executing and is
+    /// open to a post-check flash rewrite).
+    ///
+    /// Lifecycle is untouched: these components are held for re-check, not gated
+    /// (`Nominal` stays `Nominal`), and each is released again by its
+    /// `ReleaseReset` once it re-passes verification. Isolated components are
+    /// already held (`released == false`) and are skipped, as is anything under
+    /// active recovery. At the initial power-on walk nothing is live yet, so
+    /// this emits nothing and cold boot is unchanged.
+    fn quiesce_all(&mut self, ctx: &mut Sink<E>) {
+        for i in 0..self.chain.len() {
+            if !self.statuses[i].released {
+                continue;
+            }
+            let (id, _) = self.chain[i];
+            ctx.emit(Effect::AssertReset(id));
+            self.statuses[i].released = false;
+            self.statuses[i].awaiting_boot = false;
+        }
+    }
+    /// shared by both paths that take a component out of service — the
+    /// runtime-corruption path ([`handle_corruption`](Self::handle_corruption))
+    /// and the recovery-exhaustion path — so the two can never disagree about
+    /// what a policy means (in particular, `Cascading` cascades in both).
+    ///
+    /// - `Isolable` → gate this component alone → [`Gating::Gated`].
+    /// - `Cascading` → gate this component and every transitive dependent →
+    ///   [`Gating::Gated`].
+    /// - `Required`, or an unknown/missing id → gate nothing →
+    ///   [`Gating::NotGated`], leaving the caller to handle the non-gating
+    ///   outcome in its own context (recover, at runtime; lock down, once
+    ///   recovery is exhausted).
+    ///
+    /// Every component this gates also gets an [`Effect::ReportIsolated`], so
+    /// management software learns the platform is degraded no matter which path
+    /// took the component out of service.
+    ///
+    /// Idempotent per component (guarded by `is_gated`) — so is the reporting:
+    /// a component already gated is neither re-reset nor re-reported.
+    fn gate_by_policy(&mut self, ctx: &mut Sink<E>, id: ComponentId) -> Gating {
+        match self.attrs_of(id).map(|attrs| attrs.failure_policy) {
+            Some(FailurePolicy::Cascading) => {
+                self.cascade_hold(ctx, id);
+                Gating::Gated
+            }
+            Some(FailurePolicy::Isolable) => {
+                self.gate_one(ctx, id);
+                Gating::Gated
+            }
+            // `Required`, or an unknown/missing id: not a gating policy.
+            _ => Gating::NotGated,
+        }
+    }
+
+    /// Shared `CorruptionDetected` handling, called from both `PreSupervision`
+    /// (directly) and `SupervisingPlatform` (via its superstate handler).
+    /// Delegates the policy interpretation to [`gate_by_policy`](Self::gate_by_policy)
+    /// so this path and the recovery-exhaustion path can never diverge:
+    /// `Isolable`/`Cascading` → gate the component (single or cascade) and stay
+    /// put, so a later re-walk skips it instead of silently re-releasing one we
+    /// already found corrupt; `Required` → recover first (the halt-on-exhaustion
+    /// decision happens later in `Recovering`).
+    fn handle_corruption(&mut self, id: ComponentId, ctx: &mut Sink<E>) -> Outcome {
+        match self.gate_by_policy(ctx, id) {
+            Gating::Gated => Outcome::Handled,
+            Gating::NotGated => Outcome::Transition(State::Recovering(id)),
+        }
+    }
+
+    /// Hold `root` and cascade-hold every component whose `depends_on`
+    /// (transitively) names it. Emits `AssertReset` and `ReportIsolated` for
+    /// each newly gated component, including `root` itself — every isolated
+    /// device is reported, not just the one that failed.
+    fn cascade_hold(&mut self, ctx: &mut Sink<E>, root: ComponentId) {
+        // BFS over the growing isolation front. `frontier` holds the components
+        // gated so far whose dependents still need visiting; `statuses` records
+        // the durable `Isolated` mark for each.
+        let mut frontier: heapless::Vec<ComponentId, N> = heapless::Vec::new();
+        if self.gate_one(ctx, root) {
+            let _ = frontier.push(root);
+        }
+        let mut i = 0;
+        while let Some(&holder) = frontier.get(i) {
+            i += 1;
+            let mut newly_gated: heapless::Vec<ComponentId, N> = heapless::Vec::new();
+            for &(id, attrs) in self.chain.iter() {
+                if attrs.depends_on == Some(holder) && !self.is_gated(id) {
+                    let _ = newly_gated.push(id);
+                }
+            }
+            for id in newly_gated {
+                if self.gate_one(ctx, id) {
+                    let _ = frontier.push(id);
+                }
+            }
+        }
+    }
+}
+
+/// The reducer proper: the per-state handlers, the superstate handler, and the
+/// entry actions. These are pure functions of `(stored data, state, event)` —
+/// they mutate [`Rot`]'s storage and push [`Effect`]s into the [`Sink`], and
+/// return an [`Outcome`] describing what should happen to the current state.
+/// Applying that outcome is the engine's job ([`Orchestrator::step`]).
+impl<const N: usize, const E: usize> Rot<N, E> {
+    /// Dispatch `event` to the handler for `state` (the leaf state). An
+    /// [`Outcome::Super`] here means "not handled at this level" — the engine
+    /// forwards to [`handle_supervising`](Self::handle_supervising) if `state`
+    /// is supervised, and otherwise discards the event.
+    fn handle(&mut self, state: State, event: &Event, ctx: &mut Sink<E>) -> Outcome {
+        match state {
+            State::PowerOnReset => match event {
+                Event::PowerGood(PowerOnResult::Provisioned) => {
+                    Outcome::Transition(State::PreSupervision)
+                }
+                Event::PowerGood(PowerOnResult::Unprovisioned) => {
+                    Outcome::Transition(State::Locked)
+                }
+                Event::PowerGood(PowerOnResult::SelfVerificationFailed) => {
+                    Outcome::Transition(State::Locked)
+                }
+                Event::EffectFailed => Outcome::Transition(State::Locked),
+                _ => Outcome::Super,
+            },
+
+            // Cursor walk via Outcome::Handled — a self-transition would reset cursor.
+            State::PreSupervision => match event {
+                Event::VerificationPassed(id) => {
+                    // Only the component currently under verification
+                    // (`chain[cursor]`, whose `VerifyFirmware` was just emitted)
+                    // may be released. A verdict for any other id is stale or
+                    // out-of-turn and is dropped, so a misordered or hostile
+                    // report cannot release an unverified component (cf. INV9
+                    // for `ComponentReady`).
+                    if self.chain.get(self.cursor as usize).map(|(c, _)| c) != Some(id) {
+                        return Outcome::Handled;
+                    }
+                    // The component passed its check — it has recovered, so its
+                    // consecutive-failure streak ends (INV7: consecutive only).
+                    self.clear_retry(*id);
+                    ctx.emit(Effect::ReleaseReset(*id));
+                    // Released: it is now live, and owes a boot-progress signal
+                    // (both tiers).
+                    self.mark_released(*id);
+                    let current_kind = self.chain.get(self.cursor as usize).map(|(_, a)| a.kind);
+                    let next_idx = (self.cursor as usize).saturating_add(1);
+                    if self.advance_to_next_ungated(ctx, next_idx) {
+                        match current_kind {
+                            Some(ComponentKind::Active) => {
+                                Outcome::Transition(State::AwaitingReady(Some(*id)))
+                            }
+                            _ => Outcome::Handled,
+                        }
+                    } else {
+                        Outcome::Transition(State::Ready)
+                    }
+                }
+                Event::VerificationFailed(id) => {
+                    // Recovery is attempted first for every failure, regardless
+                    // of the component's recovery-failure policy (CSA: recover
+                    // first, classify only once retries are exhausted).
+                    Outcome::Transition(State::Recovering(*id))
+                }
+                // Minimal fix: react to a corruption report if one arrives,
+                // even though `PreSupervision` isn't linked to
+                // `SupervisingPlatform`. Not acting on data we already have
+                // would be strictly worse than acting on it, regardless of
+                // whether CSA defines a mechanism that guarantees this event
+                // exists in the first place. `AttestationChallenge` is left
+                // unhandled here (falls through to `Outcome::Super` and is
+                // discarded) — that's a separate question.
+                Event::CorruptionDetected(id) => self.handle_corruption(*id, ctx),
+                // Boot-progress liveness for a passive component released
+                // speculatively earlier in this same walk. Clear its watchdog
+                // even though `PreSupervision` is unsupervised — acting on a
+                // report we already have is never worse than dropping it (same
+                // rationale as `CorruptionDetected` above). An `Active`
+                // component's `ComponentReady` cannot arrive here: releasing an
+                // active moves the machine straight to `AwaitingReady`.
+                Event::Booted(id) => {
+                    self.clear_awaiting_boot(*id);
+                    Outcome::Handled
+                }
+                // Device-agnostic boot-progress watchdog. A passive component
+                // released speculatively can miss its window while the walk is
+                // still in `PreSupervision`; treat that as a boot failure and
+                // recover it, exactly as the supervised states do. A timeout for
+                // a component not awaiting boot (e.g. still under verification)
+                // is spurious and dropped.
+                Event::Timeout(id) => {
+                    if self.is_awaiting_boot(*id) {
+                        Outcome::Transition(State::Recovering(*id))
+                    } else {
+                        Outcome::Handled
+                    }
+                }
+                Event::EffectFailed => Outcome::Transition(State::Locked),
+                _ => Outcome::Super,
+            },
+
+            // `awaiting` is the state's own payload, so changing it means
+            // re-entering the variant: `Outcome::Handled` leaves the payload
+            // untouched. That is correct only because `AwaitingReady` has no
+            // entry action — do not add one.
+            State::AwaitingReady(awaiting) => match event {
+                Event::ComponentReady(id) => {
+                    // Clear this component's boot-progress watchdog whether or
+                    // not it is the one this state's slot is tracking: a later
+                    // `Active` released speculatively reports its readiness here
+                    // too, and its watchdog must be cleared just the same.
+                    self.clear_awaiting_boot(*id);
+                    if awaiting != Some(*id) {
+                        return Outcome::Handled; // not the tracked slot (INV9)
+                    }
+                    // If cursor is past the end, the eRoT side of the walk has
+                    // already finished (chain done, or the remainder is held) —
+                    // nothing left to verify, we're done.
+                    if (self.cursor as usize) >= self.chain.len() {
+                        Outcome::Transition(State::Ready)
+                    } else {
+                        // Readiness satisfied, chain not done: stay supervised,
+                        // now awaiting nothing.
+                        Outcome::Transition(State::AwaitingReady(None))
+                    }
+                }
+                Event::VerificationPassed(id) => {
+                    // Only the component currently under verification
+                    // (`chain[cursor]`) may be released; a verdict for any other
+                    // id is stale or out-of-turn and is dropped (cf. INV9 for
+                    // `ComponentReady`).
+                    if self.chain.get(self.cursor as usize).map(|(c, _)| c) != Some(id) {
+                        return Outcome::Handled;
+                    }
+                    // The component passed its check — it has recovered, so its
+                    // consecutive-failure streak ends (INV7: consecutive only).
+                    self.clear_retry(*id);
+                    ctx.emit(Effect::ReleaseReset(*id));
+                    // Released: it is now live, and owes a boot-progress signal
+                    // (both tiers).
+                    self.mark_released(*id);
+                    let next_idx = (self.cursor as usize).saturating_add(1);
+                    if self.advance_to_next_ungated(ctx, next_idx) {
+                        // `Handled` preserves the current payload: `awaiting` is
+                        // cleared only by `ComponentReady` or `VerificationFailed`.
+                        Outcome::Handled
+                    } else {
+                        Outcome::Transition(State::Ready)
+                    }
+                }
+                Event::VerificationFailed(id) => {
+                    // Recovery is attempted first for every failure, regardless
+                    // of the component's recovery-failure policy.
+                    Outcome::Transition(State::Recovering(*id))
+                }
+                // `Timeout` is intentionally not handled here: it falls through
+                // to `handle_supervising`, which runs the device-agnostic
+                // boot-progress watchdog uniformly across every supervised state
+                // (an `AwaitingReady` timeout is no longer special-cased).
+                _ => Outcome::Super,
+            },
+
+            State::Ready => match event {
+                Event::UpdateRequest => Outcome::Transition(State::Updating),
+                // Proven-boot checkpoint: the image authenticated at
+                // `ActivateUpdate`, but the SVN floor only advances now, once
+                // the driver reports it healthy. Handled in place — confirming a
+                // running image is not a state change. Closing the window clears
+                // `pending_commit` so a later `CommitTimeout` cannot lock a
+                // device that has already committed.
+                Event::BootConfirmed(id) => {
+                    ctx.emit(Effect::CommitSvnFloor(*id));
+                    self.pending_commit = false;
+                    Outcome::Handled
+                }
+                // Commit watchdog. If the activated-but-not-committed window is
+                // still open, fail closed: never commit an unproven image, and
+                // never leave the downgrade window open indefinitely. Outside
+                // the window this is a stale watchdog fire and is dropped.
+                Event::CommitTimeout => {
+                    if self.pending_commit {
+                        Outcome::Transition(State::Locked)
+                    } else {
+                        Outcome::Handled
+                    }
+                }
+                _ => Outcome::Super,
+            },
+
+            State::Updating => match event {
+                Event::UpdateVerified => {
+                    ctx.emit(Effect::ActivateUpdate);
+                    // Open the activated-but-not-committed window: the floor is
+                    // NOT advanced here; it waits for `BootConfirmed`. The
+                    // driver arms its commit watchdog on `ActivateUpdate`, and
+                    // `CommitTimeout` bounds this window (commit-or-lock).
+                    self.pending_commit = true;
+                    Outcome::Transition(State::Ready)
+                }
+                Event::UpdateRejected => {
+                    ctx.emit(Effect::DiscardStaged);
+                    Outcome::Transition(State::Ready)
+                }
+                Event::CorruptionDetected(id) => {
+                    let outcome = self.handle_corruption(*id, ctx);
+                    // Only a *preemption* (transition out to recovery) orphans
+                    // the staged image. An `Isolable`/`Cascading` corruption
+                    // returns `Handled` and the update continues untouched, so
+                    // its staged image must survive — do not discard then.
+                    if matches!(outcome, Outcome::Transition(State::Recovering(_))) {
+                        // Dispose of the orphaned image *and* answer the update
+                        // requester: the update it was awaiting a verdict on has
+                        // been superseded by recovery, not merely delayed.
+                        ctx.emit(Effect::DiscardStaged);
+                        ctx.emit(Effect::ReportUpdateAborted);
+                    }
+                    outcome
+                }
+                _ => Outcome::Super,
+            },
+
+            State::Recovering(failed) => match event {
+                Event::Restored(id) => {
+                    // A `Restored` for a component other than the current
+                    // recovery target (e.g. an episode displaced by a later
+                    // corruption) must not be credited to this recovery. Drop
+                    // it; the eventual re-walk re-verifies every component.
+                    if *id != failed {
+                        return Outcome::Handled;
+                    }
+                    // Count this attempt against the specific component in
+                    // recovery, not a global budget (CSA: exhaustion is
+                    // per-device). The recovery target is the state's payload,
+                    // so it is always present — no defensive fallback needed.
+                    let attempts = self.bump_retry(failed);
+                    if attempts < self.max_retry {
+                        Outcome::Transition(State::PreSupervision)
+                    } else {
+                        // Retries exhausted: gate via the same `gate_by_policy`
+                        // the runtime-corruption path uses, so the two can never
+                        // disagree. Gated → continue the walk; NotGated
+                        // (Required/unknown) → lock down.
+                        match self.gate_by_policy(ctx, failed) {
+                            Gating::Gated => {
+                                self.clear_retry(failed);
+                                Outcome::Transition(State::PreSupervision)
+                            }
+                            // `Required`, or an unknown/missing id: report the
+                            // component that forced the halt, then lock down.
+                            // The report precedes the internal `Emit`, so it is
+                            // actuated before the machine moves toward `Locked`.
+                            Gating::NotGated => {
+                                ctx.emit(Effect::ReportRecoveryFailed(failed));
+                                ctx.emit(Effect::Emit(Event::RecoveryFailed));
+                                Outcome::Handled
+                            }
+                        }
+                    }
+                }
+                Event::RecoveryFailed => Outcome::Transition(State::Locked),
+                _ => Outcome::Super,
+            },
+
+            State::Locked => Outcome::Super,
+        }
+    }
+
+    /// The supervising handler, reached only when [`handle`](Self::handle)
+    /// returns [`Outcome::Super`] from one of the four supervised states
+    /// ([`State::AwaitingReady`], [`State::Ready`], [`State::Updating`],
+    /// [`State::Recovering`] — see [`Orchestrator::is_supervised`]). It provides
+    /// two platform-wide guarantees that must hold across all four:
+    ///
+    /// - Attestation challenges are always answered.
+    /// - Corruption of a required component always triggers recovery.
+    ///
+    /// Note: [`State::PreSupervision`] is deliberately *not* supervised, so the
+    /// attestation guarantee does not hold while a component is still being
+    /// walked there — CSA defines no requirement to answer challenges before the
+    /// chain walk completes, so `AttestationChallenge` is left unhandled in
+    /// `PreSupervision` (falls through to [`Outcome::Super`] and, with no
+    /// supervisor, is discarded).
+    ///
+    /// The corruption guarantee, however, *does* hold in `PreSupervision`: that
+    /// state handles [`Event::CorruptionDetected`] directly (via
+    /// [`handle_corruption`](Self::handle_corruption)) rather than through this
+    /// handler, since routing it here would also pull in the attestation
+    /// behavior above. CSA defines no mechanism guaranteeing a corruption report
+    /// arrives for an already-released component's *live, executing* state (its
+    /// only at-rest mechanism — background NVM integrity polling — is explicitly
+    /// scoped to "at rest"/"between boots", not an in-progress boot's chain
+    /// walk), but that only means such a report isn't guaranteed to exist — it's
+    /// not a reason to discard one if it does arrive. See
+    /// `corruption_during_presupervision_selfloop_triggers_recovery` in
+    /// `tests.rs`.
+    fn handle_supervising(&mut self, event: &Event, ctx: &mut Sink<E>) -> Outcome {
+        match event {
+            Event::AttestationChallenge => {
+                ctx.emit(Effect::SignAttestation);
+                Outcome::Handled
+            }
+            Event::CorruptionDetected(id) => self.handle_corruption(*id, ctx),
+            // Boot-progress signals arriving after the walk left `PreSupervision`
+            // / `AwaitingReady` (e.g. once the machine is already `Ready`): clear
+            // the component's watchdog. `ComponentReady` is the active tier,
+            // `Booted` the passive tier; both just retire the outstanding wait.
+            Event::ComponentReady(id) | Event::Booted(id) => {
+                self.clear_awaiting_boot(*id);
+                Outcome::Handled
+            }
+            // Device-agnostic boot-progress watchdog across every supervised
+            // state: a released component that never reported in before its
+            // window closed is recovered like any other boot failure. A timeout
+            // for a component not awaiting boot (already reported, gated, or
+            // never released) is stale/spurious and dropped.
+            Event::Timeout(id) => {
+                if self.is_awaiting_boot(*id) {
+                    Outcome::Transition(State::Recovering(*id))
+                } else {
+                    Outcome::Handled
+                }
+            }
+            // A new update cannot start from any supervised state except
+            // `Ready` (the machine is mid-walk, mid-update, or mid-recovery).
+            // `Ready` accepts `UpdateRequest` upstream in `handle` (→ `Updating`)
+            // and so never reaches here; this arm therefore fires only for
+            // `AwaitingReady`, `Updating`, and `Recovering`. Report the refusal
+            // rather than dropping it silently, and leave the in-flight
+            // walk/update/recovery untouched (`Handled`, no transition).
+            Event::UpdateRequest => {
+                ctx.emit(Effect::ReportUpdateDeferred);
+                Outcome::Handled
+            }
+            Event::EffectFailed => Outcome::Transition(State::Locked),
+            _ => Outcome::Super,
+        }
+    }
+
+    /// Run `state`'s entry action. Called by the engine only when a handler
+    /// returned [`Outcome::Transition`] — never on [`Outcome::Handled`]. That
+    /// distinction is load-bearing: `PreSupervision`'s cursor walk returns
+    /// `Handled` precisely so this does not re-run and reset the cursor.
+    fn entry_action(&mut self, state: State, ctx: &mut Sink<E>) {
+        match state {
+            State::PreSupervision => {
+                // Recovery is a full platform re-boot: quiesce every live
+                // component before the walk, so verification always covers code
+                // at rest, never a component whose earlier pass says nothing
+                // about what it is currently running. Empty at the initial
+                // power-on walk (nothing live yet), so cold boot is unchanged.
+                self.quiesce_all(ctx);
+                let _ = self.advance_to_next_ungated(ctx, 0);
+            }
+            State::Updating => {
+                // A new update supersedes any activated-but-not-committed image;
+                // the prior commit window is void.
+                self.pending_commit = false;
+                ctx.emit(Effect::AuthenticateUpdate);
+                ctx.emit(Effect::StageUpdate);
+            }
+            State::Recovering(failed) => {
+                // Recovery voids any activated-but-not-committed image: the
+                // running image is now under suspicion, so its commit window
+                // ends here.
+                self.pending_commit = false;
+                // The component under recovery is being restored, not booting;
+                // drop any pending boot-progress watchdog so a late `Timeout`
+                // can't re-enter recovery for it. It is also held (not live)
+                // while the platform restores it, so it is not quiesced again on
+                // the re-walk.
+                self.clear_awaiting_boot(failed);
+                if let Some(i) = self.status_index(failed) {
+                    self.statuses[i].released = false;
+                }
+                ctx.emit(Effect::RecoverComponent(failed));
+            }
+            State::Locked => {
+                ctx.emit(Effect::LatchLockdown);
+            }
+            State::Ready => {
+                // NB: `gated` is intentionally NOT cleared here. It is a durable
+                // trust-boundary gate (each id has a live `AssertReset`);
+                // clearing it would let a later chain walk re-release a
+                // component that policy deliberately isolated. Only a fresh
+                // `Rot` on `PowerOnReset` clears it.
+                //
+                // Retry counts, by contrast, ARE cleared: a clean boot means no
+                // recovery episode is in flight, so every per-component streak
+                // resets to zero. (The `Isolated` lifecycle is preserved.)
+                for s in self.statuses.iter_mut() {
+                    s.retry = 0;
+                }
+            }
+            _ => {}
+        }
+    }
+}
+
+/// Signals that the shell could not carry out an [`Effect`]. The machine does
+/// not need the shell's error detail — **every** actuation failure is treated
+/// the same, fail-closed: the driver injects [`Event::EffectFailed`] and the
+/// machine latches to [`State::Locked`]. This blanket policy is deliberate and
+/// is what lets the failure signal stay a payload-less marker; a future design
+/// that needs per-effect recovery must add a *new*, descriptive event rather
+/// than widen this type. The shell logs the specifics on its side.
+#[derive(Clone, Copy, PartialEq, Eq, Debug)]
+pub struct EffectError;
+
+/// Outward connection to the platform. Carry out one effect, reporting
+/// [`EffectError`] if it could not be performed. Never called with
+/// [`Effect::Emit`] — the orchestrator consumes those internally.
+///
+/// Contract the reducer relies on:
+/// - **Honest, complete feedback.** The reducer's correctness rests entirely on
+///   the event stream the shell feeds back; dropping, reordering, or
+///   synthesizing events silently breaks the state machine's invariants.
+/// - **`AssertReset` holds, it does not pulse.** A reset must keep the component
+///   quiesced and non-executing until its matching `ReleaseReset`. The reducer's
+///   at-rest verification guarantee depends on this: it re-asserts reset on
+///   every live component before a recovery re-walk (`quiesce_all`) so that
+///   `VerifyFirmware` covers code that cannot run or rewrite its own flash
+///   between the check and the release. A reset that merely pulses would let a
+///   component resume before verification and void that guarantee.
+/// - **A failed [`Effect::LatchLockdown`] is a hard fault.** Lockdown is the top
+///   of the escalation ladder — the reducer has nothing stronger to emit and
+///   will *believe* it is `Locked`. The shell must treat that failure as
+///   terminal (halt/reset), not a recoverable error.
+pub trait Platform {
+    fn execute(&mut self, effect: Effect) -> Result<(), EffectError>;
+}
+
+/// A handle for a caller's own event loop. Owns the machine's storage
+/// ([`Rot`]) and its current [`State`], and drives them through [`step`].
+///
+/// [`step`]: Self::step
+pub struct Orchestrator<const N: usize, const E: usize> {
+    rot: Rot<N, E>,
+    state: State,
+}
+
+impl<const N: usize, const E: usize> Orchestrator<N, E> {
+    pub fn new(chain: Chain<N>, max_retry: u8) -> Self {
+        Self {
+            rot: Rot::new(chain, max_retry),
+            // The initial state. `PowerOnReset` has no entry action, so there is
+            // nothing to run here before the first event.
+            state: State::PowerOnReset,
+        }
+    }
+
+    pub fn state(&self) -> State {
+        self.state
+    }
+
+    /// Whether `state` is nested under the supervising handler
+    /// ([`Rot::handle_supervising`]) — i.e. whether an [`Outcome::Super`] from
+    /// its leaf handler has anywhere to go. The four supervised states are the
+    /// ones the eRoT can be in after it has exited [`State::PreSupervision`],
+    /// and before it locks down.
+    const fn is_supervised(state: State) -> bool {
+        matches!(
+            state,
+            State::AwaitingReady(_) | State::Ready | State::Updating | State::Recovering(_)
+        )
+    }
+
+    /// Reduce one event: dispatch, fall through to the supervisor if needed, and
+    /// apply the resulting outcome.
+    ///
+    /// The machine defines no exit actions and no supervisor entry/exit actions,
+    /// so a transition's only side effect is the target state's entry action —
+    /// and it lands in the *same* `ctx` as the handler that caused it, which the
+    /// `E >= 2 * N + 2` bound relies on (a full gate cascade, with its paired
+    /// isolation reports, plus the destination `PreSupervision` entry's two
+    /// effects share one `Sink`).
+    fn step(&mut self, event: &Event, ctx: &mut Sink<E>) {
+        // 0. Single point of id-membership enforcement. The core supervises
+        //    only the components in the configured chain, so an event that names
+        //    an id the chain does not contain is dropped here, before any
+        //    handler runs — no handler needs its own membership check, and none
+        //    can act on a component the core never modeled. Events that name no
+        //    component (`component_id() == None`) always pass through.
+        if let Some(id) = event.component_id()
+            && !self.rot.in_chain(id)
+        {
+            return;
+        }
+
+        // 1. Dispatch to the current (leaf) state.
+        let mut outcome = self.rot.handle(self.state, event, ctx);
+
+        // 2. On `Super`, defer to the supervising handler if this state has one;
+        //    otherwise the event is discarded. Discarding is what keeps `Locked`
+        //    terminal: it is unsupervised, so its blanket `Super` drops every
+        //    event — including the `EffectFailed` from a failed `LatchLockdown`,
+        //    which would otherwise loop.
+        if let Outcome::Super = outcome
+            && Self::is_supervised(self.state)
+        {
+            outcome = self.rot.handle_supervising(event, ctx);
+        }
+
+        // 3. Apply a transition. `Handled` and an unhandled `Super` both leave
+        //    the state alone and run no entry action.
+        if let Outcome::Transition(target) = outcome {
+            self.state = target;
+            self.rot.entry_action(target, ctx);
+        }
+    }
+
+    /// Handle one event all the way through — including any [`Effect::Emit`]
+    /// follow-ups — calling `on_effect` for each external effect in order.
+    ///
+    /// If `on_effect` reports an [`EffectError`], the driver injects an
+    /// [`Event::EffectFailed`] into the same run, so a failed actuation is
+    /// handled fail-closed (the machine latches to [`State::Locked`]) rather
+    /// than silently ignored.
+    pub fn dispatch_with(
+        &mut self,
+        event: Event,
+        mut on_effect: impl FnMut(Effect) -> Result<(), EffectError>,
+    ) {
+        let mut pending: heapless::Vec<Event, PENDING_CAP> = heapless::Vec::new();
+        // Dead Err arm: `pending` is empty and `PENDING_CAP >= 3` (asserted at
+        // build time), so the first push always fits.
+        let _ = pending.push(event);
+
+        let mut i = 0;
+        while i < pending.len() {
+            let ev = pending[i];
+            i += 1;
+
+            let mut buf = Sink::<E>::new();
+            self.step(&ev, &mut buf);
+
+            for &effect in buf.effects() {
+                match effect {
+                    Effect::Emit(internal) => {
+                        // Dead Err arm: the reducer emits at most one `Emit`
+                        // (`RecoveryFailed`) per settle, well within PENDING_CAP.
+                        let _ = pending.push(internal);
+                    }
+                    external => {
+                        if on_effect(external).is_err() {
+                            // Fail-closed AND fail-fast: abandon the rest of this
+                            // batch so no effect ordered after the failed one hits
+                            // hardware. `step` has already advanced the state as if
+                            // the whole batch applied, so actuating `k+1..` would
+                            // carry out effects for a transition we are about to
+                            // override by latching to `Locked`.
+                            //
+                            // Inject `EffectFailed` once: it is idempotent and
+                            // terminal (drives to `Locked`, which discards
+                            // everything after), so a second injection would be a
+                            // no-op. De-duping against this append-only queue —
+                            // which still holds the first `EffectFailed` as its own
+                            // marker — caps the queue at the worst case
+                            // `PENDING_CAP` is sized for. Dead Err arm: that bound
+                            // is below PENDING_CAP.
+                            if !pending.contains(&Event::EffectFailed) {
+                                let _ = pending.push(Event::EffectFailed);
+                            }
+                            break;
+                        }
+                    }
+                }
+            }
+        }
+    }
+
+    /// Same as [`dispatch_with`] but routes effects to a [`Platform`].
+    pub fn dispatch(&mut self, platform: &mut impl Platform, event: Event) {
+        self.dispatch_with(event, |effect| platform.execute(effect));
+    }
+}
+
+#[cfg(test)]
+mod tests;
diff --git a/services/orchestrator/sm/src/model.rs b/services/orchestrator/sm/src/model.rs
new file mode 100644
index 00000000..ae9cfd8f
--- /dev/null
+++ b/services/orchestrator/sm/src/model.rs
@@ -0,0 +1,472 @@
+// Licensed under the Apache-2.0 license
+// SPDX-License-Identifier: Apache-2.0
+
+//! Domain vocabulary for the orchestrator state machine: the component model,
+//! events, effects, states, and the validated [`Chain`] of trust. These types
+//! carry no reducer behavior; the state machine itself lives in the crate root.
+
+/// An opaque identifier for one platform component. The core never inspects it;
+/// the board layer decides which real hardware each id refers to.
+#[derive(Clone, Copy, PartialEq, Eq, Debug)]
+pub struct ComponentId(u8);
+
+impl ComponentId {
+    pub const fn new(id: u8) -> Self {
+        Self(id)
+    }
+
+    pub const fn get(self) -> u8 {
+        self.0
+    }
+}
+
+/// How a component in the trust chain is classified. The board supplies one
+/// [`ComponentKind`] per [`ComponentId`] when building the chain.
+///
+/// Corresponds directly to the two-tier model in the CSA architecture document:
+/// `Active` = eRoT gate + iRoT gate; `Passive` = eRoT gate only.
+#[derive(Clone, Copy, PartialEq, Eq, Debug)]
+pub enum ComponentKind {
+    /// Has an integrated iRoT (e.g. Caliptra). Both eRoT-side (signature + SVN)
+    /// and iRoT-side (local self-verification) checks apply. The machine waits in
+    /// [`State::AwaitingReady`] for [`Event::ComponentReady`] before advancing.
+    Active,
+    /// No integrated iRoT. The eRoT's signature + SVN check is the only *trust*
+    /// gate, so the chain walk advances speculatively after `ReleaseReset`
+    /// without blocking in [`State::AwaitingReady`]. The released component is
+    /// still watched for boot-progress liveness ([`Event::Booted`]) under the
+    /// same per-component watchdog as an `Active` component's
+    /// [`Event::ComponentReady`]: a passive device that never reports in before
+    /// its [`Event::Timeout`] is recovered like any other boot failure. CSA
+    /// boot-progress checkpointing is device-agnostic — every released device
+    /// owes a boot-progress signal, iRoT or not.
+    Passive,
+}
+
+/// Recovery-failure classification: what the machine does once a required
+/// component's restore attempts are **exhausted** (its per-component retry
+/// count reaches `max_retry`). Every verification or corruption failure enters
+/// [`State::Recovering`] and is retried first, regardless of this
+/// classification — CSA's "recover first" principle. This value is consulted
+/// only after retries are exhausted.
+///
+/// (The narrative design docs sometimes call the `Required` outcome "platform
+/// halt" — same behavior, this is the type-level name.)
+#[derive(Clone, Copy, PartialEq, Eq, Debug)]
+pub enum FailurePolicy {
+    /// Stop the boot sequence entirely: self-emits [`Event::RecoveryFailed`],
+    /// which drives the machine to [`State::Locked`].
+    Required,
+    /// Hold this component in reset (added to `Rot.gated`) and continue
+    /// booting the rest of the platform.
+    Isolable,
+    /// Hold this component **and** any component whose `depends_on` names it
+    /// (transitively), then continue booting the rest of the platform.
+    Cascading,
+}
+
+/// Opaque recovery-region key supplied by the board at chain-build time.
+/// Components sharing a `RegionId` are restored together: when any region
+/// member enters [`State::Recovering`], the shell resolves and restores the
+/// whole region. The core treats this as an equality key only and never
+/// inspects membership itself.
+#[derive(Clone, Copy, PartialEq, Eq, Debug)]
+pub struct RegionId(u8);
+
+impl RegionId {
+    pub const fn new(id: u8) -> Self {
+        Self(id)
+    }
+    pub const fn get(self) -> u8 {
+        self.0
+    }
+}
+
+/// Per-component attributes supplied by the board at chain-build time.
+///
+/// Three orthogonal axes:
+/// - [`kind`](ComponentAttrs::kind): controls the iRoT gate (Active vs Passive).
+/// - [`failure_policy`](ComponentAttrs::failure_policy): controls what happens
+///   once this component's recovery is exhausted.
+/// - [`recovery_region`](ComponentAttrs::recovery_region) /
+///   [`depends_on`](ComponentAttrs::depends_on): control restore grouping and
+///   cascade-skip on exhaustion.
+///
+/// A component that fails verification is never released from reset —
+/// running untrusted firmware would break the trust invariant regardless of
+/// `failure_policy`.
+#[derive(Clone, Copy, PartialEq, Eq, Debug)]
+pub struct ComponentAttrs {
+    pub kind: ComponentKind,
+    pub failure_policy: FailurePolicy,
+    pub recovery_region: RegionId,
+    pub depends_on: Option<ComponentId>,
+}
+
+impl ComponentAttrs {
+    pub const fn active_required() -> Self {
+        Self {
+            kind: ComponentKind::Active,
+            failure_policy: FailurePolicy::Required,
+            recovery_region: RegionId::new(0),
+            depends_on: None,
+        }
+    }
+    pub const fn passive_required() -> Self {
+        Self {
+            kind: ComponentKind::Passive,
+            failure_policy: FailurePolicy::Required,
+            recovery_region: RegionId::new(0),
+            depends_on: None,
+        }
+    }
+    pub const fn active_isolable() -> Self {
+        Self {
+            kind: ComponentKind::Active,
+            failure_policy: FailurePolicy::Isolable,
+            recovery_region: RegionId::new(0),
+            depends_on: None,
+        }
+    }
+    pub const fn passive_isolable() -> Self {
+        Self {
+            kind: ComponentKind::Passive,
+            failure_policy: FailurePolicy::Isolable,
+            recovery_region: RegionId::new(0),
+            depends_on: None,
+        }
+    }
+    pub const fn active_cascading() -> Self {
+        Self {
+            kind: ComponentKind::Active,
+            failure_policy: FailurePolicy::Cascading,
+            recovery_region: RegionId::new(0),
+            depends_on: None,
+        }
+    }
+    pub const fn passive_cascading() -> Self {
+        Self {
+            kind: ComponentKind::Passive,
+            failure_policy: FailurePolicy::Cascading,
+            recovery_region: RegionId::new(0),
+            depends_on: None,
+        }
+    }
+
+    /// Builder: assign a non-default recovery region (default is region `0`).
+    pub const fn with_region(mut self, region: RegionId) -> Self {
+        self.recovery_region = region;
+        self
+    }
+
+    /// Builder: mark this component as cascade-held whenever `dependency` is
+    /// held. Only meaningful in combination with `FailurePolicy::Cascading`
+    /// on the *dependency*, not on this component.
+    pub const fn with_depends_on(mut self, dependency: ComponentId) -> Self {
+        self.depends_on = Some(dependency);
+        self
+    }
+}
+
+/// The result of the board's power-on checks, delivered inside [`Event::PowerGood`].
+#[derive(Clone, Copy, PartialEq, Eq, Debug)]
+pub enum PowerOnResult {
+    /// Self-verified and provisioned.
+    Provisioned,
+    /// Self-verified but not provisioned — cannot act as a RoT.
+    Unprovisioned,
+    /// Self-verification failed — latches immediately to [`State::Locked`].
+    SelfVerificationFailed,
+}
+
+/// Everything the outside world can tell the state machine.
+#[derive(Clone, Copy, PartialEq, Eq, Debug)]
+pub enum Event {
+    /// Power-on, carrying the shell's self-verification and provisioning result.
+    PowerGood(PowerOnResult),
+    /// The eRoT's signature + SVN check on this component passed.
+    VerificationPassed(ComponentId),
+    /// The eRoT's signature + SVN check on this component failed.
+    VerificationFailed(ComponentId),
+    /// An `Active` component's iRoT has finished local verification and is ready.
+    ComponentReady(ComponentId),
+    /// A `Passive` component reported boot-progress liveness — its firmware came
+    /// up. The passive-tier counterpart to [`Event::ComponentReady`]: a passive
+    /// component has no iRoT to self-verify, so "it booted" is the only
+    /// post-release signal it can produce. Clears that component's boot-progress
+    /// watchdog. Mirrors fwmanager's `BootProgress::Booted`.
+    Booted(ComponentId),
+    /// A challenger has requested a signed attestation.
+    AttestationChallenge,
+    /// A firmware update has been requested.
+    UpdateRequest,
+    /// The staged update authenticated successfully.
+    UpdateVerified,
+    /// The staged update failed authentication.
+    UpdateRejected,
+    /// The activated image proved itself healthy at runtime (supervised
+    /// health / attestation pass — not mere boot). Gates the anti-rollback
+    /// commit: only now is it safe to advance the SVN floor past this image,
+    /// because it has demonstrated it runs, not merely that it authenticated.
+    BootConfirmed(ComponentId),
+    /// This component was found corrupt at runtime.
+    CorruptionDetected(ComponentId),
+    /// This component has been restored from its configured recovery source.
+    Restored(ComponentId),
+    /// A required component's recovery was exhausted.
+    RecoveryFailed,
+    /// The shell's boot-progress watchdog fired: `id` did not report its
+    /// boot-progress signal ([`Event::ComponentReady`] for an `Active`
+    /// component, [`Event::Booted`] for a `Passive` one) within its configured
+    /// boot timeout. Treated as a verification failure — a component still
+    /// awaiting boot-progress enters recovery. A timeout for a component that is
+    /// not awaiting boot (never released, already reported in, or already gated)
+    /// is stale/spurious and dropped. The watchdog is per component and
+    /// device-agnostic, matching CSA boot-progress checkpointing.
+    Timeout(ComponentId),
+    /// The driver's *commit* watchdog fired: an update was activated
+    /// ([`Effect::ActivateUpdate`]) but did not report [`Event::BootConfirmed`]
+    /// within the policy window. Distinct from [`Event::Timeout`], which is the
+    /// per-component boot-progress watchdog; this one bounds the single
+    /// activated-but-not-committed window in [`State::Ready`]. Handled only while
+    /// that window is open: it latches [`State::Locked`] (commit-or-lock — the
+    /// anti-rollback floor is never advanced for an unproven image, and the
+    /// downgrade window may not stay open indefinitely). Outside the window
+    /// (nothing pending) it is stale and dropped. The driver arms this watchdog
+    /// when it executes [`Effect::ActivateUpdate`] and cancels it on
+    /// [`Effect::CommitSvnFloor`].
+    CommitTimeout,
+    /// The shell could not carry out an emitted [`Effect`]; fail-closed, it
+    /// latches to [`State::Locked`] from any state. Injected by the driver when
+    /// a [`Platform::execute`](crate::Platform::execute) call fails; never
+    /// produced by a handler.
+    EffectFailed,
+}
+
+impl Event {
+    /// The component this event is about, or `None` for events that name no
+    /// component (`PowerGood`, `UpdateRequest`, `CommitTimeout`, …).
+    ///
+    /// This is the single enumeration of the id-carrying events, consulted once
+    /// at the dispatch boundary ([`Orchestrator::step`](crate::Orchestrator::step))
+    /// to drop any event that names a component outside the configured chain
+    /// before a handler ever sees it. A new id-carrying variant must be listed
+    /// here, or it will bypass that membership check.
+    pub(crate) fn component_id(&self) -> Option<ComponentId> {
+        match self {
+            Event::VerificationPassed(id)
+            | Event::VerificationFailed(id)
+            | Event::ComponentReady(id)
+            | Event::Booted(id)
+            | Event::BootConfirmed(id)
+            | Event::CorruptionDetected(id)
+            | Event::Restored(id)
+            | Event::Timeout(id) => Some(*id),
+            Event::PowerGood(_)
+            | Event::AttestationChallenge
+            | Event::UpdateRequest
+            | Event::UpdateVerified
+            | Event::UpdateRejected
+            | Event::RecoveryFailed
+            | Event::CommitTimeout
+            | Event::EffectFailed => None,
+        }
+    }
+}
+
+/// Everything the state machine can ask the outside world to do.
+///
+/// [`Effect::Emit`] is the sole internal effect: the orchestrator catches it and
+/// queues the carried event for immediate handling, making follow-up events
+/// visible in the effect trace instead of hidden state changes.
+#[derive(Clone, Copy, PartialEq, Eq, Debug)]
+pub enum Effect {
+    ReadFirmware(ComponentId),
+    VerifyFirmware(ComponentId),
+    ReleaseReset(ComponentId),
+    /// Assert reset on a component that is already running — the inverse of
+    /// [`ReleaseReset`]. Emitted when an `Isolable`/`Cascading` component is
+    /// found corrupt at runtime, or is held after recovery is exhausted: the
+    /// component is gated without triggering (or continuing) a recovery cycle.
+    AssertReset(ComponentId),
+    SignAttestation,
+    AuthenticateUpdate,
+    StageUpdate,
+    ActivateUpdate,
+    DiscardStaged,
+    /// Advance the anti-rollback (SVN) floor past `id`'s now-confirmed image.
+    /// Deliberately decoupled from [`ActivateUpdate`]: activation happens on
+    /// authentication (`UpdateVerified`), but the floor may only move once the
+    /// image has proven healthy ([`Event::BootConfirmed`]). Committing the
+    /// floor earlier would burn anti-rollback on an image that authenticated
+    /// but has not yet demonstrated it can boot and run.
+    CommitSvnFloor(ComponentId),
+    /// Recover `id` from its configured recovery source. The mechanism —
+    /// golden image, A/B slot, streamed image, or vendor-specific scheme — is
+    /// deferred to the [`Platform`](crate::Platform) driver, which resolves it
+    /// per configuration policy. The reducer only names the component to
+    /// recover; it does not encode how recovery is performed.
+    RecoverComponent(ComponentId),
+    /// Report that a component has been isolated (held in reset and removed
+    /// from the trust chain) so management software is aware the platform is
+    /// running degraded. Emitted once per component, at the moment it is
+    /// gated — CSA's degraded-mode clause requires the failure to be reported
+    /// through the platform management interface, not just contained.
+    ReportIsolated(ComponentId),
+    /// Report that a `Required` component exhausted its recovery attempts,
+    /// immediately before the machine latches to [`Locked`](crate::State::Locked).
+    /// Names the component that forced the halt.
+    ReportRecoveryFailed(ComponentId),
+    /// Report that an [`Event::UpdateRequest`] was declined because the machine
+    /// is busy in a supervised state other than [`Ready`](crate::State::Ready)
+    /// — a chain walk is finishing ([`AwaitingReady`](crate::State::AwaitingReady)),
+    /// an update is already staged ([`Updating`](crate::State::Updating)), or a
+    /// recovery is in flight ([`Recovering`](crate::State::Recovering)). Emitted
+    /// instead of silently dropping the request, so the refusal is visible in
+    /// the effect trace and the driver can answer the requester (e.g. a PLDM
+    /// "retry later" completion code). Advisory only: it changes no state and
+    /// does not perturb the in-flight update or recovery. `Ready` never produces
+    /// this — it accepts the request and transitions to `Updating`.
+    ReportUpdateDeferred,
+    /// Report that an update *already in flight* ([`Updating`](crate::State::Updating))
+    /// was aborted because a `Required` component was found corrupt and recovery
+    /// preempted it (the machine left `Updating` for
+    /// [`Recovering`](crate::State::Recovering)). Its counterpart on the intake
+    /// side is [`ReportUpdateDeferred`]: `Deferred` refuses an update that never
+    /// started, `Aborted` announces the loss of one that had. Paired with the
+    /// [`DiscardStaged`] that cleans up the orphaned image — `DiscardStaged`
+    /// disposes of the *image*, this answers the *request*, so the requester
+    /// (which was awaiting `UpdateVerified`/`UpdateRejected`) learns the update
+    /// was superseded by recovery and can retry once the platform is whole.
+    ReportUpdateAborted,
+    LatchLockdown,
+    /// Internal only — tells the orchestrator to handle this event next.
+    /// Never forwarded to a [`Platform`](crate::Platform).
+    Emit(Event),
+}
+
+/// The states the machine can be in. A variant carries exactly the data that is
+/// meaningful only while in that state; everything that spans states (the
+/// cursor, the gate set, retry counts) lives in [`Rot`](crate::Rot) shared
+/// storage.
+#[derive(Clone, Copy, PartialEq, Eq, Debug)]
+pub enum State {
+    PowerOnReset,
+    PreSupervision,
+    /// eRoT has released an `Active` component; the payload is the component
+    /// whose iRoT readiness is outstanding (INV9). Only the active-tier readiness
+    /// checkpoint lives on this payload; per-component boot-progress liveness
+    /// (for both tiers) is tracked in each component's status, not here.
+    ///
+    /// - `AwaitingReady(Some(id))` — waiting for `id`'s
+    ///   [`Event::ComponentReady`].
+    /// - `AwaitingReady(None)` — that readiness has been satisfied but the chain
+    ///   walk is not finished; the machine stays supervised while draining the
+    ///   remaining speculative verifications, and any further `ComponentReady`
+    ///   is spurious.
+    AwaitingReady(Option<ComponentId>),
+    Ready,
+    Updating,
+    /// A component failed verification (or was found corrupt under a
+    /// non-gating policy) and is being restored from its configured recovery
+    /// source. The payload is
+    /// that component — always present, since the machine only enters this state
+    /// with a recovery target in hand.
+    Recovering(ComponentId),
+    Locked,
+}
+
+/// A validated **chain of trust**: the ordered list of components the eRoT
+/// walks, verifies, and supervises, in walk order.
+///
+/// Build one with [`TryFrom`]/[`TryInto`] from a `heapless::Vec` of
+/// `(ComponentId, ComponentAttrs)` pairs. The conversion is the single place
+/// the reducer's structural invariants are enforced, so a malformed chain
+/// fails closed at the boundary instead of misbehaving later:
+///
+/// - the chain is non-empty,
+/// - every [`ComponentId`] is unique,
+/// - every `depends_on` names a component that exists and appears *strictly
+///   earlier* in the chain (no dangling, forward, or self dependencies — a
+///   dependency is always walked before its dependents),
+/// - the length fits `u8`, the `cursor` index type.
+///
+/// ```ignore
+/// let mut v = heapless::Vec::<_, 4>::new();
+/// v.push((ComponentId::new(0), ComponentAttrs::passive_required())).unwrap();
+/// let chain: Chain<4> = v.try_into()?;
+/// ```
+#[derive(Clone, Debug)]
+pub struct Chain<const N: usize> {
+    entries: heapless::Vec<(ComponentId, ComponentAttrs), N>,
+}
+
+/// Why a `heapless::Vec` of components is not a valid [`Chain`].
+#[derive(Clone, Copy, PartialEq, Eq, Debug)]
+pub enum ChainError {
+    /// The chain has no components.
+    Empty,
+    /// The chain is longer than `u8::MAX`, so `cursor` could not index it.
+    TooLong,
+    /// The same [`ComponentId`] appears more than once.
+    DuplicateId(ComponentId),
+    /// A `depends_on` names an id that is not in the chain.
+    UnknownDependency {
+        component: ComponentId,
+        depends_on: ComponentId,
+    },
+    /// A `depends_on` names a component that does not appear strictly earlier
+    /// in the chain (a forward reference or a self-reference). A dependency
+    /// must be walked before its dependents.
+    ForwardDependency {
+        component: ComponentId,
+        depends_on: ComponentId,
+    },
+}
+
+impl<const N: usize> Chain<N> {
+    /// Consume the validated chain, yielding its components in walk order.
+    pub(crate) fn into_entries(self) -> heapless::Vec<(ComponentId, ComponentAttrs), N> {
+        self.entries
+    }
+}
+
+impl<const N: usize> TryFrom<heapless::Vec<(ComponentId, ComponentAttrs), N>> for Chain<N> {
+    type Error = ChainError;
+
+    fn try_from(
+        entries: heapless::Vec<(ComponentId, ComponentAttrs), N>,
+    ) -> Result<Self, ChainError> {
+        if entries.is_empty() {
+            return Err(ChainError::Empty);
+        }
+        if entries.len() > u8::MAX as usize {
+            return Err(ChainError::TooLong);
+        }
+        for (i, (id, _)) in entries.iter().enumerate() {
+            if entries[..i].iter().any(|(prev, _)| prev == id) {
+                return Err(ChainError::DuplicateId(*id));
+            }
+        }
+        for (i, (id, attrs)) in entries.iter().enumerate() {
+            if let Some(dep) = attrs.depends_on {
+                match entries.iter().position(|(cid, _)| *cid == dep) {
+                    None => {
+                        return Err(ChainError::UnknownDependency {
+                            component: *id,
+                            depends_on: dep,
+                        });
+                    }
+                    Some(j) if j >= i => {
+                        return Err(ChainError::ForwardDependency {
+                            component: *id,
+                            depends_on: dep,
+                        });
+                    }
+                    Some(_) => {}
+                }
+            }
+        }
+        Ok(Self { entries })
+    }
+}
diff --git a/services/orchestrator/sm/src/tests.rs b/services/orchestrator/sm/src/tests.rs
new file mode 100644
index 00000000..60bf6efe
--- /dev/null
+++ b/services/orchestrator/sm/src/tests.rs
@@ -0,0 +1,1968 @@
+// Licensed under the Apache-2.0 license
+// SPDX-License-Identifier: Apache-2.0
+
+extern crate std;
+
+use super::*;
+use std::vec::Vec;
+
+const C0: ComponentId = ComponentId::new(0);
+const C1: ComponentId = ComponentId::new(1);
+const C2: ComponentId = ComponentId::new(2);
+const C3: ComponentId = ComponentId::new(3);
+
+const BOOT: Event = Event::PowerGood(PowerOnResult::Provisioned);
+
+const CAPACITY: usize = 8;
+const ECAP: usize = 2 * CAPACITY + 2;
+const MAX_RETRY: u8 = 3;
+
+fn chain(
+    ids: &[(ComponentId, ComponentAttrs)],
+) -> heapless::Vec<(ComponentId, ComponentAttrs), CAPACITY> {
+    let mut c = heapless::Vec::new();
+    for &entry in ids {
+        c.push(entry).expect("chain within CAPACITY");
+    }
+    c
+}
+
+fn passive_required(ids: &[ComponentId]) -> heapless::Vec<(ComponentId, ComponentAttrs), CAPACITY> {
+    chain(
+        &ids.iter()
+            .map(|&id| (id, ComponentAttrs::passive_required()))
+            .collect::<std::vec::Vec<_>>(),
+    )
+}
+
+struct Recorder {
+    recorded: Vec<Effect>,
+}
+
+impl Recorder {
+    fn new() -> Self {
+        Self {
+            recorded: Vec::new(),
+        }
+    }
+}
+
+impl Platform for Recorder {
+    fn execute(&mut self, effect: Effect) -> Result<(), EffectError> {
+        self.recorded.push(effect);
+        Ok(())
+    }
+}
+
+fn drive(
+    chain: heapless::Vec<(ComponentId, ComponentAttrs), CAPACITY>,
+    script: &[Event],
+) -> (Vec<Effect>, State) {
+    let mut orch =
+        Orchestrator::<CAPACITY, ECAP>::new(chain.try_into().expect("valid chain"), MAX_RETRY);
+    let mut platform = Recorder::new();
+    for &event in script {
+        orch.dispatch(&mut platform, event);
+    }
+    (platform.recorded, orch.state())
+}
+
+/// INV1/INV2/INV3: provisioned power-on walks the chain in order; no
+/// component is released before its eRoT-side verification passes.
+#[test]
+fn cold_boot_walks_chain_in_order() {
+    let (effects, state) = drive(
+        passive_required(&[C0, C1]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::VerificationPassed(C1),
+        ],
+    );
+    assert_eq!(
+        effects,
+        std::vec![
+            Effect::ReadFirmware(C0),
+            Effect::VerifyFirmware(C0),
+            Effect::ReleaseReset(C0),
+            Effect::ReadFirmware(C1),
+            Effect::VerifyFirmware(C1),
+            Effect::ReleaseReset(C1),
+        ],
+    );
+    assert_eq!(state, State::Ready);
+}
+
+/// Unprovisioned power-on latches immediately.
+#[test]
+fn unprovisioned_boot_locks_down() {
+    let (effects, state) = drive(
+        passive_required(&[C0]),
+        &[Event::PowerGood(PowerOnResult::Unprovisioned)],
+    );
+    assert_eq!(effects, std::vec![Effect::LatchLockdown]);
+    assert_eq!(state, State::Locked);
+}
+
+/// INV11: SelfVerificationFailed latches immediately without entering
+/// PreSupervision.
+#[test]
+fn self_verification_failure_latches_immediately() {
+    let (effects, state) = drive(
+        passive_required(&[C0]),
+        &[Event::PowerGood(PowerOnResult::SelfVerificationFailed)],
+    );
+    assert_eq!(effects, std::vec![Effect::LatchLockdown]);
+    assert_eq!(state, State::Locked);
+}
+
+/// INV6: AttestationChallenge is answerable from every SupervisingPlatform state.
+#[test]
+fn attestation_shared_across_supervising_platform_states() {
+    let (effects, state) = drive(
+        passive_required(&[C0]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::AttestationChallenge,
+        ],
+    );
+    assert_eq!(effects.last(), Some(&Effect::SignAttestation));
+    assert_eq!(state, State::Ready);
+
+    let (effects, state) = drive(
+        passive_required(&[C0]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::UpdateRequest,
+            Event::AttestationChallenge,
+        ],
+    );
+    assert_eq!(effects.last(), Some(&Effect::SignAttestation));
+    assert_eq!(state, State::Updating);
+}
+
+/// INV4: a rejected update rolls back via DiscardStaged and never enters
+/// Recovering.
+#[test]
+fn update_rollback_is_not_recovery() {
+    let (effects, state) = drive(
+        passive_required(&[C0]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::UpdateRequest,
+            Event::UpdateRejected,
+        ],
+    );
+    let tail = &effects[effects.len() - 3..];
+    assert_eq!(
+        tail,
+        &[
+            Effect::AuthenticateUpdate,
+            Effect::StageUpdate,
+            Effect::DiscardStaged
+        ],
+    );
+    assert_eq!(state, State::Ready);
+    assert!(!effects.contains(&Effect::LatchLockdown));
+}
+
+/// INV5: runtime corruption targets the named component and re-walks from
+/// the top after restore.
+#[test]
+fn runtime_corruption_targets_component_and_rewalks() {
+    let (effects, state) = drive(
+        passive_required(&[C0, C1]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::VerificationPassed(C1),
+            Event::CorruptionDetected(C1),
+            Event::Restored(C1),
+        ],
+    );
+    let tail = &effects[effects.len() - 2..];
+    assert_eq!(
+        tail,
+        &[Effect::ReadFirmware(C0), Effect::VerifyFirmware(C0)]
+    );
+    assert_eq!(state, State::PreSupervision);
+}
+
+/// Recovery is a full platform re-boot: a live sibling is held in reset before
+/// the re-walk re-verifies, so `VerifyFirmware` never runs against executing
+/// code. Here C0 and C1 both boot and go live; C0 is then corrupted and
+/// restored. The re-walk must `AssertReset(C1)` (quiesce the live sibling)
+/// before it re-reads and re-verifies C0 from a fully-held state.
+#[test]
+fn recovery_rewalk_quiesces_live_siblings_first() {
+    let (effects, state) = drive(
+        passive_required(&[C0, C1]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::VerificationPassed(C1), // both live → Ready
+            Event::CorruptionDetected(C0), // required → Recovering(C0)
+            Event::Restored(C0),           // re-walk: quiesce C1, then re-verify C0
+        ],
+    );
+    // The re-walk holds the live sibling before any re-verification.
+    let tail = &effects[effects.len() - 3..];
+    assert_eq!(
+        tail,
+        &[
+            Effect::AssertReset(C1),
+            Effect::ReadFirmware(C0),
+            Effect::VerifyFirmware(C0),
+        ],
+    );
+    assert_eq!(state, State::PreSupervision);
+}
+
+/// `quiesce_all` holds *every* live component, not just the immediate
+/// neighbor: with three live parts, recovering one asserts reset on both
+/// siblings before the re-walk re-verifies anything.
+#[test]
+fn recovery_rewalk_quiesces_all_live_siblings() {
+    let (effects, state) = drive(
+        passive_required(&[C0, C1, C2]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::VerificationPassed(C1),
+            Event::VerificationPassed(C2), // all live → Ready
+            Event::CorruptionDetected(C0), // required → Recovering(C0)
+            Event::Restored(C0),           // re-walk: quiesce C1 and C2 first
+        ],
+    );
+    // Both live siblings are held before the re-walk re-reads the chain.
+    let rewalk_read = effects
+        .iter()
+        .rposition(|e| *e == Effect::ReadFirmware(C0))
+        .unwrap();
+    let hold_c1 = effects
+        .iter()
+        .position(|e| *e == Effect::AssertReset(C1))
+        .unwrap();
+    let hold_c2 = effects
+        .iter()
+        .position(|e| *e == Effect::AssertReset(C2))
+        .unwrap();
+    assert!(hold_c1 < rewalk_read);
+    assert!(hold_c2 < rewalk_read);
+    assert_eq!(state, State::PreSupervision);
+}
+
+/// The TOCTOU closure: a live sibling is not trusted across a recovery on
+/// its old pass. The re-walk holds it (`AssertReset`), re-verifies it from
+/// that held state (`ReadFirmware`/`VerifyFirmware`), and only then releases
+/// it again — so the sibling is verified twice and released twice, with the
+/// hold in between.
+#[test]
+fn recovery_rewalk_reverifies_live_sibling_at_rest() {
+    let (effects, state) = drive(
+        passive_required(&[C0, C1]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::VerificationPassed(C1), // both live → Ready
+            Event::CorruptionDetected(C0), // required → Recovering(C0)
+            Event::Restored(C0),           // re-walk: quiesce C1
+            Event::VerificationPassed(C0), // re-release C0, re-read C1
+            Event::VerificationPassed(C1), // re-verify C1 at rest → Ready
+        ],
+    );
+    assert_eq!(state, State::Ready);
+    let count = |target: Effect| effects.iter().filter(|e| **e == target).count();
+    // C1 is held once (quiesce), and verified + released a second time.
+    assert_eq!(count(Effect::AssertReset(C1)), 1);
+    assert_eq!(count(Effect::VerifyFirmware(C1)), 2);
+    assert_eq!(count(Effect::ReleaseReset(C1)), 2);
+    // The re-verification and re-release both come after the hold.
+    let hold = effects
+        .iter()
+        .position(|e| *e == Effect::AssertReset(C1))
+        .unwrap();
+    let reverify = effects
+        .iter()
+        .rposition(|e| *e == Effect::VerifyFirmware(C1))
+        .unwrap();
+    let rerelease = effects
+        .iter()
+        .rposition(|e| *e == Effect::ReleaseReset(C1))
+        .unwrap();
+    assert!(hold < reverify);
+    assert!(reverify < rerelease);
+}
+
+/// `PreSupervision` reacts to `CorruptionDetected` directly (via
+/// [`Rot::handle_corruption`]), even though it isn't linked to
+/// `SupervisingPlatform` (so `AttestationChallenge` is still discarded
+/// there — a separate question). CSA defines no mechanism guaranteeing a
+/// corruption report exists for an already-released component's *live,
+/// executing* state (at-rest/NVM-polling is scoped to "at
+/// rest"/"between boots", not an in-progress boot's chain walk) — but
+/// that only means such a report isn't guaranteed to arrive, not that one
+/// should be ignored if it does.
+#[test]
+fn corruption_during_presupervision_selfloop_triggers_recovery() {
+    let (effects, state) = drive(
+        passive_required(&[C0, C1, C2]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0), // released; walk continues (still PreSupervision)
+            Event::CorruptionDetected(C0), // C0 already released, but caught anyway
+        ],
+    );
+    assert_eq!(state, State::Recovering(C0));
+    assert!(effects.contains(&Effect::RecoverComponent(C0)));
+}
+
+/// INV7 (feedback-as-data): after MAX_RETRY restores the core self-emits
+/// RecoveryFailed and latches to Locked without any external RecoveryFailed
+/// in the script.
+#[test]
+fn retry_cap_self_latches_via_emit() {
+    let mut script = std::vec![BOOT, Event::VerificationPassed(C0)];
+    script.push(Event::CorruptionDetected(C0));
+    for _ in 0..(MAX_RETRY - 1) {
+        script.push(Event::Restored(C0));
+        script.push(Event::VerificationFailed(C0));
+    }
+    script.push(Event::Restored(C0));
+
+    let (effects, state) = drive(passive_required(&[C0]), &script);
+
+    assert!(!script.contains(&Event::RecoveryFailed));
+    assert_eq!(state, State::Locked);
+    assert_eq!(effects.last(), Some(&Effect::LatchLockdown));
+}
+
+/// INV7: retry count resets after a successful recovery so a later episode
+/// starts from zero.
+#[test]
+fn retry_count_resets_after_successful_recovery() {
+    let mut c = heapless::Vec::<(ComponentId, ComponentAttrs), CAPACITY>::new();
+    c.push((C0, ComponentAttrs::passive_required()))
+        .expect("fits");
+    let mut orch = Orchestrator::<CAPACITY, ECAP>::new(c.try_into().expect("valid chain"), 2);
+    let mut effects = Vec::new();
+
+    for ev in [
+        BOOT,
+        Event::VerificationPassed(C0),
+        Event::CorruptionDetected(C0),
+        Event::Restored(C0),
+        Event::VerificationPassed(C0),
+    ] {
+        orch.dispatch_with(ev, |e| {
+            effects.push(e);
+            Ok(())
+        });
+    }
+    assert_eq!(orch.state(), State::Ready);
+
+    let start = effects.len();
+    for ev in [
+        Event::CorruptionDetected(C0),
+        Event::Restored(C0),
+        Event::VerificationPassed(C0),
+    ] {
+        orch.dispatch_with(ev, |e| {
+            effects.push(e);
+            Ok(())
+        });
+    }
+    assert_eq!(orch.state(), State::Ready);
+    assert!(!effects[start..].contains(&Effect::LatchLockdown));
+}
+
+/// Retry budgets are **per component**, not a single global counter. Two
+/// required components each fail exactly once (well under `max_retry = 2`)
+/// in an interleaved recovery sequence before the chain finally settles.
+/// Under a shared global counter the second failure would push the count to
+/// the cap and latch the platform to `Locked`; per-component counting lets
+/// each device use its own budget, so the walk reaches `Ready`.
+#[test]
+fn retry_budget_is_per_component() {
+    let mut c = heapless::Vec::<(ComponentId, ComponentAttrs), CAPACITY>::new();
+    c.push((C0, ComponentAttrs::passive_required()))
+        .expect("fits");
+    c.push((C1, ComponentAttrs::passive_required()))
+        .expect("fits");
+    let mut orch = Orchestrator::<CAPACITY, ECAP>::new(c.try_into().expect("valid chain"), 2);
+    let mut effects = Vec::new();
+
+    for ev in [
+        BOOT,
+        Event::VerificationFailed(C0), // C0 fails once → Recovering
+        Event::Restored(C0),           // C0 count = 1 (< 2) → re-walk
+        Event::VerificationPassed(C0), // C0 recovered → its streak clears
+        Event::VerificationFailed(C1), // C1 fails once → Recovering
+        Event::Restored(C1),           // C1 count = 1 (< 2); global would be 2 → latch
+        Event::VerificationPassed(C0), // re-walk restarts at the top
+        Event::VerificationPassed(C1), // chain done → Ready
+    ] {
+        orch.dispatch_with(ev, |e| {
+            effects.push(e);
+            Ok(())
+        });
+    }
+
+    assert_eq!(orch.state(), State::Ready);
+    assert!(!effects.contains(&Effect::LatchLockdown));
+}
+
+/// Board-supplied retry cap: max_retry = 1 latches on the first failed
+/// restore.
+#[test]
+fn custom_retry_cap_latches_sooner() {
+    let mut c = heapless::Vec::<(ComponentId, ComponentAttrs), CAPACITY>::new();
+    c.push((C0, ComponentAttrs::passive_required()))
+        .expect("fits");
+    let mut orch = Orchestrator::<CAPACITY, ECAP>::new(c.try_into().expect("valid chain"), 1);
+    let mut effects = Vec::new();
+    for ev in [
+        BOOT,
+        Event::VerificationPassed(C0),
+        Event::CorruptionDetected(C0),
+        Event::Restored(C0),
+    ] {
+        orch.dispatch_with(ev, |e| {
+            effects.push(e);
+            Ok(())
+        });
+    }
+    assert_eq!(orch.state(), State::Locked);
+    assert_eq!(effects.last(), Some(&Effect::LatchLockdown));
+}
+
+/// Three-component chain uses N=3; walks all three to Ready.
+#[test]
+fn custom_capacity_walks_full_chain() {
+    let mut c = heapless::Vec::<(ComponentId, ComponentAttrs), 3>::new();
+    for &id in &[C0, C1, C2] {
+        c.push((id, ComponentAttrs::passive_required()))
+            .expect("3 fits");
+    }
+    let mut orch = Orchestrator::<3, 8>::new(c.try_into().expect("valid chain"), MAX_RETRY);
+    let mut effects = Vec::new();
+    for ev in [
+        BOOT,
+        Event::VerificationPassed(C0),
+        Event::VerificationPassed(C1),
+        Event::VerificationPassed(C2),
+    ] {
+        orch.dispatch_with(ev, |e| {
+            effects.push(e);
+            Ok(())
+        });
+    }
+    assert_eq!(orch.state(), State::Ready);
+    assert_eq!(effects.last(), Some(&Effect::ReleaseReset(C2)));
+}
+
+/// INV10: Active component gates the chain walk — cursor does not advance
+/// until ComponentReady arrives.
+#[test]
+fn active_component_gates_on_component_ready() {
+    let (effects, state) = drive(
+        chain(&[
+            (C0, ComponentAttrs::active_required()),
+            (C1, ComponentAttrs::passive_required()),
+        ]),
+        &[BOOT, Event::VerificationPassed(C0)],
+    );
+    assert_eq!(state, State::AwaitingReady(Some(C0)));
+    assert!(effects.contains(&Effect::ReleaseReset(C0)));
+    assert!(effects.contains(&Effect::ReadFirmware(C1)));
+
+    let (effects2, state2) = drive(
+        chain(&[
+            (C0, ComponentAttrs::active_required()),
+            (C1, ComponentAttrs::passive_required()),
+        ]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::ComponentReady(C0),
+            Event::VerificationPassed(C1),
+        ],
+    );
+    assert_eq!(state2, State::Ready);
+    assert!(effects2.contains(&Effect::ReleaseReset(C1)));
+}
+
+/// INV9: a ComponentReady for the wrong id is silently ignored.
+#[test]
+fn spurious_component_ready_is_ignored() {
+    let (effects, state) = drive(
+        chain(&[
+            (C0, ComponentAttrs::active_required()),
+            (C1, ComponentAttrs::passive_required()),
+        ]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::ComponentReady(C1), // wrong id
+        ],
+    );
+    assert_eq!(state, State::AwaitingReady(Some(C0)));
+    assert!(!effects.contains(&Effect::ReleaseReset(C1)));
+}
+
+/// INV12: AttestationChallenge is handled in AwaitingReady.
+#[test]
+fn attestation_in_awaiting_ready() {
+    let (effects, state) = drive(
+        chain(&[
+            (C0, ComponentAttrs::active_required()),
+            (C1, ComponentAttrs::passive_required()),
+        ]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::AttestationChallenge,
+        ],
+    );
+    assert_eq!(state, State::AwaitingReady(Some(C0)));
+    assert_eq!(effects.last(), Some(&Effect::SignAttestation));
+}
+
+/// D2: a boot-progress timeout for the awaited component is treated as a
+/// verification failure and enters recovery.
+#[test]
+fn timeout_awaited_enters_recovering() {
+    let (effects, state) = drive(
+        chain(&[
+            (C0, ComponentAttrs::active_required()),
+            (C1, ComponentAttrs::passive_required()),
+        ]),
+        &[BOOT, Event::VerificationPassed(C0), Event::Timeout(C0)],
+    );
+    assert_eq!(state, State::Recovering(C0));
+    assert!(effects.contains(&Effect::RecoverComponent(C0)));
+}
+
+/// D2: a timeout for a component that is not awaiting boot-progress is
+/// stale/spurious and is dropped. Here `C1` has only been *verified*
+/// speculatively, not released, so no boot watchdog is armed for it; the
+/// machine keeps waiting on the component it actually released (`C0`).
+#[test]
+fn timeout_stale_id_ignored() {
+    let (effects, state) = drive(
+        chain(&[
+            (C0, ComponentAttrs::active_required()),
+            (C1, ComponentAttrs::passive_required()),
+        ]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::Timeout(C1), // verified but never released → not awaiting boot
+        ],
+    );
+    assert_eq!(state, State::AwaitingReady(Some(C0)));
+    assert!(!effects.contains(&Effect::RecoverComponent(C1)));
+}
+
+/// An out-of-chain id in a `VerificationFailed` report is dropped: the core
+/// supervises only chain components, so a verdict for an id the chain does not
+/// contain neither enters `Recovering` nor emits `RecoverComponent`.
+#[test]
+fn verification_failed_out_of_chain_id_is_dropped() {
+    let (effects, state) = drive(
+        passive_required(&[C0, C1]),
+        &[BOOT, Event::VerificationFailed(C3)],
+    );
+    assert!(!effects.contains(&Effect::RecoverComponent(C3)));
+    // Untouched: still walking the chain from the top with C0 under verification.
+    assert_eq!(state, State::PreSupervision);
+}
+
+/// An out-of-chain id in a `CorruptionDetected` report is likewise dropped: a
+/// malformed report from the platform cannot drive a spurious recovery or move
+/// the machine out of `Ready`.
+#[test]
+fn corruption_out_of_chain_id_is_dropped() {
+    let (effects, state) = drive(
+        passive_required(&[C0, C1]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::VerificationPassed(C1),
+            Event::CorruptionDetected(C3),
+        ],
+    );
+    assert!(!effects.contains(&Effect::RecoverComponent(C3)));
+    assert_eq!(state, State::Ready);
+}
+
+/// Device-agnostic boot-progress: a *passive* component that is released but
+/// never reports [`Event::Booted`] before its watchdog fires is recovered like
+/// any other boot failure — even while the walk is still in `PreSupervision`.
+/// This closes the release-and-forget gap (CSA boot-progress checkpointing is
+/// device-agnostic; fwmanager arms a `boot_timeout` for every device).
+#[test]
+fn passive_boot_timeout_enters_recovering() {
+    let (effects, state) = drive(
+        passive_required(&[C0, C1]),
+        // C0 released (watchdog armed), walk speculatively verifies C1, then
+        // C0's boot window closes with no `Booted`.
+        &[BOOT, Event::VerificationPassed(C0), Event::Timeout(C0)],
+    );
+    assert_eq!(state, State::Recovering(C0));
+    assert!(effects.contains(&Effect::ReleaseReset(C0)));
+    assert!(effects.contains(&Effect::RecoverComponent(C0)));
+}
+
+/// A passive boot timeout is caught even after the chain walk has completed and
+/// the machine has reached `Ready`: speculative release means a component can
+/// still owe a boot-progress signal in `Ready`, and the supervisor runs the
+/// same device-agnostic watchdog there.
+#[test]
+fn passive_boot_timeout_in_ready_enters_recovering() {
+    let (effects, state) = drive(
+        passive_required(&[C0]),
+        // Single passive: reaches `Ready` on VerificationPassed while still
+        // awaiting C0's boot-progress; the timeout then fires in `Ready`.
+        &[BOOT, Event::VerificationPassed(C0), Event::Timeout(C0)],
+    );
+    assert_eq!(state, State::Recovering(C0));
+    assert!(effects.contains(&Effect::RecoverComponent(C0)));
+}
+
+/// A passive component that reports [`Event::Booted`] retires its watchdog, so a
+/// later timeout for it is stale and dropped — the machine stays `Ready`.
+#[test]
+fn passive_booted_clears_watchdog_then_timeout_is_stale() {
+    let (effects, state) = drive(
+        passive_required(&[C0, C1]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::Booted(C0), // C0 reports in → watchdog cleared
+            Event::VerificationPassed(C1),
+            Event::Booted(C1),
+            Event::Timeout(C0), // stale: C0 already booted
+        ],
+    );
+    assert_eq!(state, State::Ready);
+    assert!(!effects.contains(&Effect::RecoverComponent(C0)));
+}
+
+/// D2: full path — timeout drives recovery, restore rewalks from the top, and
+/// the chain then completes normally.
+#[test]
+fn timeout_recovers_then_rewalks_to_ready() {
+    let (effects, state) = drive(
+        chain(&[
+            (C0, ComponentAttrs::active_required()),
+            (C1, ComponentAttrs::passive_required()),
+        ]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::Timeout(C0),  // → Recovering(C0)
+            Event::Restored(C0), // → PreSupervision, rewalk from top
+            Event::VerificationPassed(C0),
+            Event::ComponentReady(C0),
+            Event::VerificationPassed(C1),
+        ],
+    );
+    assert_eq!(state, State::Ready);
+    assert!(effects.contains(&Effect::RecoverComponent(C0)));
+    assert!(effects.contains(&Effect::ReleaseReset(C1)));
+}
+
+/// Isolable component: every `VerificationFailed` is retried through a full
+/// recovery episode first; only once retries are exhausted does the
+/// component get held in reset and the walk continue to `Ready`.
+#[test]
+fn isolable_component_exhausts_recovery_then_skips() {
+    let mut script = std::vec![BOOT, Event::VerificationPassed(C0)];
+    for _ in 0..MAX_RETRY {
+        script.push(Event::VerificationFailed(C1));
+        script.push(Event::Restored(C1));
+        script.push(Event::VerificationPassed(C0));
+    }
+    let (effects, state) = drive(
+        chain(&[
+            (C0, ComponentAttrs::passive_required()),
+            (C1, ComponentAttrs::passive_isolable()),
+        ]),
+        &script,
+    );
+    assert_eq!(state, State::Ready);
+    // C1 must never be released.
+    assert!(!effects.contains(&Effect::ReleaseReset(C1)));
+    // Recovery IS attempted before C1 is classified and held.
+    assert!(effects.contains(&Effect::RecoverComponent(C1)));
+    assert!(effects.contains(&Effect::AssertReset(C1)));
+    assert!(!effects.contains(&Effect::LatchLockdown));
+}
+
+/// Isolable Active component failure in AwaitingReady: retried through a
+/// full recovery episode, then held once exhausted; the walk still
+/// reaches Ready once the remaining chain (past the held component) drains.
+#[test]
+fn isolable_active_component_exhausted_in_awaiting_ready_skips() {
+    // C0 Active required, C1 Active isolable.
+    let mut script = std::vec![BOOT, Event::VerificationPassed(C0)]; // → AwaitingReady; spec ReadFirmware(C1)
+    for _ in 0..MAX_RETRY {
+        script.push(Event::VerificationFailed(C1));
+        script.push(Event::Restored(C1));
+        script.push(Event::VerificationPassed(C0)); // re-walk restarts at C0 each episode
+    }
+    let (effects, state) = drive(
+        chain(&[
+            (C0, ComponentAttrs::active_required()),
+            (C1, ComponentAttrs::active_isolable()),
+        ]),
+        &script,
+    );
+    assert_eq!(state, State::Ready);
+    assert!(!effects.contains(&Effect::ReleaseReset(C1)));
+    assert!(effects.contains(&Effect::RecoverComponent(C1)));
+    assert!(effects.contains(&Effect::AssertReset(C1)));
+}
+
+/// Runtime corruption of an `Isolable` component gates the component
+/// (AssertReset) but does not trigger recovery — the machine stays in Ready.
+#[test]
+fn isolable_runtime_corruption_is_ignored() {
+    let (effects, state) = drive(
+        chain(&[
+            (C0, ComponentAttrs::passive_required()),
+            (C1, ComponentAttrs::passive_isolable()),
+        ]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::VerificationPassed(C1),
+            Event::CorruptionDetected(C1), // Isolable → gate, no recovery
+        ],
+    );
+    assert_eq!(state, State::Ready);
+    assert!(effects.contains(&Effect::AssertReset(C1)));
+    assert!(!effects.contains(&Effect::RecoverComponent(C1)));
+    assert!(!effects.contains(&Effect::LatchLockdown));
+}
+
+/// Runtime corruption of an `Isolable` component holds it in reset: it is
+/// added to `held`, so a later re-walk triggered by a *required*
+/// component's recovery skips it instead of re-releasing a component we
+/// already found corrupt.
+#[test]
+fn isolable_runtime_corruption_holds_across_rewalk() {
+    let (effects, state) = drive(
+        chain(&[
+            (C0, ComponentAttrs::passive_required()),
+            (C1, ComponentAttrs::passive_isolable()),
+        ]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::VerificationPassed(C1),
+            Event::CorruptionDetected(C1), // isolable → gate + hold
+            Event::CorruptionDetected(C0), // required → Recovering
+            Event::Restored(C0),           // re-walk from top
+            Event::VerificationPassed(C0), // C1 stays held → chain done
+        ],
+    );
+    assert_eq!(state, State::Ready);
+    // C1 is released exactly once (the initial walk); the post-corruption
+    // re-walk must not release it again.
+    assert_eq!(
+        effects
+            .iter()
+            .filter(|e| **e == Effect::ReleaseReset(C1))
+            .count(),
+        1,
+    );
+    // C1 is held exactly once (the gate). `quiesce_all` skips it on the
+    // recovery re-walk because it is already held — no duplicate reset.
+    assert_eq!(
+        effects
+            .iter()
+            .filter(|e| **e == Effect::AssertReset(C1))
+            .count(),
+        1,
+    );
+}
+
+/// A durable gate must survive a return to `Ready`. The gate set is *not*
+/// cleared on `Ready` entry, so a component isolated by policy stays gated
+/// across an intervening return to `Ready` and a later chain walk never
+/// re-reads or re-releases it. Extends the single-walk
+/// `..._holds_across_rewalk` case with a *second* return to `Ready` — the
+/// exact point where the old `held.clear()` dropped the gate.
+#[test]
+fn gate_survives_return_to_ready() {
+    let (effects, state) = drive(
+        chain(&[
+            (C0, ComponentAttrs::passive_required()),
+            (C1, ComponentAttrs::passive_isolable()),
+        ]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::VerificationPassed(C1), // walk 1 done → Ready
+            Event::CorruptionDetected(C1), // isolable → gate + hold C1
+            Event::CorruptionDetected(C0), // required → Recovering
+            Event::Restored(C0),           // walk 2 from top
+            Event::VerificationPassed(C0), // C1 gated skip → Ready (gate must persist)
+            Event::CorruptionDetected(C0), // required → Recovering again
+            Event::Restored(C0),           // walk 3 from top
+            Event::VerificationPassed(C0), // C1 still gated → chain done → Ready
+        ],
+    );
+    assert_eq!(state, State::Ready);
+    // C1 was read/verified and released exactly once, on walk 1. If the
+    // gate were dropped at `Ready`, walk 3 would re-read and re-release it.
+    assert_eq!(
+        effects
+            .iter()
+            .filter(|e| **e == Effect::ReadFirmware(C1))
+            .count(),
+        1,
+    );
+    assert_eq!(
+        effects
+            .iter()
+            .filter(|e| **e == Effect::ReleaseReset(C1))
+            .count(),
+        1,
+    );
+}
+
+/// Runtime corruption of a `Required` component still triggers
+/// recovery as before.
+#[test]
+fn required_runtime_corruption_triggers_recovery() {
+    let (effects, state) = drive(
+        chain(&[
+            (C0, ComponentAttrs::passive_required()),
+            (C1, ComponentAttrs::passive_isolable()),
+        ]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::VerificationPassed(C1),
+            Event::CorruptionDetected(C0), // required → Recovering
+        ],
+    );
+    assert_eq!(state, State::Recovering(C0));
+    assert!(effects.contains(&Effect::RecoverComponent(C0)));
+}
+
+/// Runtime corruption of a `Cascading` component must gate the whole
+/// cascade, not just the reported component. The runtime-corruption path
+/// and the recovery-exhaustion path share one `gate_by_policy` source of
+/// truth, so `Cascading` cascades in both. C2 `depends_on` C1; corrupting
+/// C1 must assert reset on C1 **and** C2.
+#[test]
+fn cascading_runtime_corruption_cascades() {
+    let (effects, state) = drive(
+        chain(&[
+            (C0, ComponentAttrs::passive_required()),
+            (C1, ComponentAttrs::passive_cascading()),
+            (C2, ComponentAttrs::passive_required().with_depends_on(C1)),
+        ]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::VerificationPassed(C1),
+            Event::VerificationPassed(C2), // walk done → Ready
+            Event::CorruptionDetected(C1), // Cascading → gate C1 and its dependents
+        ],
+    );
+    assert_eq!(state, State::Ready);
+    // The whole cascade is gated: C1 (the root) and C2 (its dependent).
+    assert!(effects.contains(&Effect::AssertReset(C1)));
+    assert!(effects.contains(&Effect::AssertReset(C2)));
+    // No recovery is started for a non-required corruption.
+    assert!(!effects.contains(&Effect::RecoverComponent(C1)));
+    assert!(!effects.contains(&Effect::LatchLockdown));
+}
+
+/// Degraded mode (CSA): isolating a component is only half the requirement —
+/// the failure must also be *reported* through the platform management
+/// interface. An `Isolable` component that exhausts recovery emits
+/// `ReportIsolated` alongside its `AssertReset`, and the platform keeps running.
+#[test]
+fn isolable_exhaustion_reports_isolation() {
+    let mut script = std::vec![BOOT, Event::VerificationPassed(C0)];
+    for _ in 0..MAX_RETRY {
+        script.push(Event::VerificationFailed(C1));
+        script.push(Event::Restored(C1));
+        script.push(Event::VerificationPassed(C0));
+    }
+    let (effects, state) = drive(
+        chain(&[
+            (C0, ComponentAttrs::passive_required()),
+            (C1, ComponentAttrs::passive_isolable()),
+        ]),
+        &script,
+    );
+    assert_eq!(state, State::Ready);
+    assert!(effects.contains(&Effect::AssertReset(C1)));
+    assert!(effects.contains(&Effect::ReportIsolated(C1)));
+    // Degraded, not halted: this is an isolation report, not a halt report.
+    assert!(!effects.contains(&Effect::ReportRecoveryFailed(C1)));
+    assert!(!effects.contains(&Effect::LatchLockdown));
+}
+
+/// Every component taken out of service by a cascade is reported, not just the
+/// one that failed: operators need to know that C2 is down too, even though
+/// nothing was wrong with C2 itself.
+#[test]
+fn cascading_exhaustion_reports_each_isolated() {
+    let mut script = std::vec![BOOT, Event::VerificationPassed(C0)];
+    for _ in 0..MAX_RETRY {
+        script.push(Event::VerificationFailed(C1));
+        script.push(Event::Restored(C1));
+        script.push(Event::VerificationPassed(C0));
+    }
+    let (effects, state) = drive(
+        chain(&[
+            (C0, ComponentAttrs::passive_required()),
+            (C1, ComponentAttrs::passive_cascading()),
+            (C2, ComponentAttrs::passive_required().with_depends_on(C1)),
+        ]),
+        &script,
+    );
+    assert_eq!(state, State::Ready);
+    // The root and its transitive dependent are both isolated and both reported.
+    assert!(effects.contains(&Effect::AssertReset(C1)));
+    assert!(effects.contains(&Effect::AssertReset(C2)));
+    assert!(effects.contains(&Effect::ReportIsolated(C1)));
+    assert!(effects.contains(&Effect::ReportIsolated(C2)));
+    assert!(!effects.contains(&Effect::LatchLockdown));
+}
+
+/// Cascades propagate transitively, not just one hop: a `Cascading` failure at
+/// the root pulls down its direct dependent AND that dependent's dependent.
+/// This exercises the BFS re-enqueue in `cascade_hold` past a single iteration
+/// — propagation follows `depends_on` regardless of the dependent's own policy
+/// (C2/C3 are `Required` yet are still isolated because they hang off C1).
+#[test]
+fn cascading_runtime_corruption_cascades_transitively() {
+    let (effects, state) = drive(
+        chain(&[
+            (C0, ComponentAttrs::passive_required()),
+            (C1, ComponentAttrs::passive_cascading()),
+            (C2, ComponentAttrs::passive_required().with_depends_on(C1)),
+            (C3, ComponentAttrs::passive_required().with_depends_on(C2)),
+        ]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::VerificationPassed(C1),
+            Event::VerificationPassed(C2),
+            Event::VerificationPassed(C3), // walk done → Ready
+            Event::CorruptionDetected(C1), // Cascading root
+        ],
+    );
+    assert_eq!(state, State::Ready);
+    // Root, its dependent, and the transitive dependent are all isolated and
+    // all reported — the two-hop chain C1 → C2 → C3 is fully gated.
+    assert!(effects.contains(&Effect::AssertReset(C1)));
+    assert!(effects.contains(&Effect::AssertReset(C2)));
+    assert!(effects.contains(&Effect::AssertReset(C3)));
+    assert!(effects.contains(&Effect::ReportIsolated(C1)));
+    assert!(effects.contains(&Effect::ReportIsolated(C2)));
+    assert!(effects.contains(&Effect::ReportIsolated(C3)));
+    // A non-required cascade never enters recovery or lockdown.
+    assert!(!effects.contains(&Effect::RecoverComponent(C1)));
+    assert!(!effects.contains(&Effect::LatchLockdown));
+}
+
+/// Runtime corruption under a non-`Required` policy reports too. This path
+/// never enters recovery at all, so without its own report the isolation would
+/// be silent.
+#[test]
+fn runtime_corruption_isolable_reports() {
+    let (effects, state) = drive(
+        chain(&[
+            (C0, ComponentAttrs::passive_required()),
+            (C1, ComponentAttrs::passive_isolable()),
+        ]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::VerificationPassed(C1),
+            Event::CorruptionDetected(C1),
+        ],
+    );
+    assert_eq!(state, State::Ready);
+    assert!(effects.contains(&Effect::ReportIsolated(C1)));
+    assert!(!effects.contains(&Effect::RecoverComponent(C1)));
+}
+
+/// A `Required` component whose recovery is exhausted is named in a
+/// `ReportRecoveryFailed` *before* the platform latches, so management software
+/// learns which component forced the halt rather than just that one did.
+#[test]
+fn required_exhaustion_reports_before_lockdown() {
+    let mut script = std::vec![BOOT, Event::VerificationPassed(C0)];
+    script.push(Event::CorruptionDetected(C0));
+    for _ in 0..(MAX_RETRY - 1) {
+        script.push(Event::Restored(C0));
+        script.push(Event::VerificationFailed(C0));
+    }
+    script.push(Event::Restored(C0));
+
+    let (effects, state) = drive(passive_required(&[C0]), &script);
+
+    assert_eq!(state, State::Locked);
+    let report = effects
+        .iter()
+        .position(|e| *e == Effect::ReportRecoveryFailed(C0))
+        .expect("the component that forced the halt is reported");
+    let latch = effects
+        .iter()
+        .position(|e| *e == Effect::LatchLockdown)
+        .expect("the platform latches");
+    assert!(
+        report < latch,
+        "the report must be actuated before the latch",
+    );
+}
+
+/// A component that recovers within its retry budget is not degraded, so
+/// nothing is reported — reports mark components taken *out of service*, not
+/// every transient failure.
+#[test]
+fn successful_recovery_emits_no_isolation_report() {
+    let (effects, state) = drive(
+        passive_required(&[C0]),
+        &[
+            BOOT,
+            Event::VerificationFailed(C0),
+            Event::Restored(C0),
+            Event::VerificationPassed(C0),
+        ],
+    );
+    assert_eq!(state, State::Ready);
+    assert!(effects.contains(&Effect::RecoverComponent(C0)));
+    assert!(
+        !effects.iter().any(|e| matches!(
+            e,
+            Effect::ReportIsolated(_) | Effect::ReportRecoveryFailed(_)
+        )),
+        "a recovered component is not degraded",
+    );
+}
+
+/// Reporting is guarded by `is_gated` exactly like the reset it accompanies, so
+/// a repeated corruption report on an already-isolated component does not
+/// re-report it. Management software sees one isolation event per component.
+#[test]
+fn report_isolated_emitted_once_per_component() {
+    let (effects, state) = drive(
+        chain(&[
+            (C0, ComponentAttrs::passive_required()),
+            (C1, ComponentAttrs::passive_isolable()),
+        ]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::VerificationPassed(C1),
+            Event::CorruptionDetected(C1), // isolable → gate + report
+            Event::CorruptionDetected(C1), // already gated → nothing
+        ],
+    );
+    assert_eq!(state, State::Ready);
+    assert_eq!(
+        effects
+            .iter()
+            .filter(|e| **e == Effect::ReportIsolated(C1))
+            .count(),
+        1,
+    );
+    assert_eq!(
+        effects
+            .iter()
+            .filter(|e| **e == Effect::AssertReset(C1))
+            .count(),
+        1,
+    );
+}
+
+/// Boot-time VerificationFailed on a required component → Recovering.
+/// (Distinct from CorruptionDetected: this is a failed eRoT-side check
+/// before the component is ever released from reset.)
+#[test]
+fn boot_failure_required_enters_recovering() {
+    let (effects, state) = drive(
+        passive_required(&[C0, C1]),
+        &[BOOT, Event::VerificationFailed(C0)],
+    );
+    assert_eq!(state, State::Recovering(C0));
+    assert!(effects.contains(&Effect::RecoverComponent(C0)));
+    // Component must never be released when its eRoT check failed.
+    assert!(!effects.contains(&Effect::ReleaseReset(C0)));
+}
+
+/// Full boot-failure recovery cycle: VerificationFailed → Recovering →
+/// Restored → re-walk from top → VerificationPassed → Ready.
+#[test]
+fn boot_failure_recovery_cycle_completes() {
+    let (effects, state) = drive(
+        passive_required(&[C0]),
+        &[
+            BOOT,
+            Event::VerificationFailed(C0),
+            Event::Restored(C0),
+            Event::VerificationPassed(C0),
+        ],
+    );
+    assert_eq!(state, State::Ready);
+    assert!(effects.contains(&Effect::RecoverComponent(C0)));
+    // ReleaseReset only after the recovery re-walk passes.
+    assert!(effects.contains(&Effect::ReleaseReset(C0)));
+}
+
+/// VerificationFailed (required) on a speculative check while the machine
+/// is in AwaitingReady → enters Recovering without releasing the component.
+#[test]
+fn required_failure_in_awaiting_ready_enters_recovering() {
+    let (effects, state) = drive(
+        chain(&[
+            (C0, ComponentAttrs::active_required()),
+            (C1, ComponentAttrs::passive_required()),
+        ]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0), // → AwaitingReady; spec check of C1 starts
+            Event::VerificationFailed(C1), // required → Recovering
+        ],
+    );
+    assert_eq!(state, State::Recovering(C1));
+    assert!(effects.contains(&Effect::RecoverComponent(C1)));
+    assert!(!effects.contains(&Effect::ReleaseReset(C1)));
+}
+
+/// CorruptionDetected while in AwaitingReady (required component) →
+/// Recovering via the SupervisingPlatform superstate handler.
+#[test]
+fn corruption_in_awaiting_ready_triggers_recovery() {
+    let (effects, state) = drive(
+        chain(&[
+            (C0, ComponentAttrs::active_required()),
+            (C1, ComponentAttrs::passive_required()),
+        ]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0), // → AwaitingReady
+            Event::CorruptionDetected(C0),
+        ],
+    );
+    assert_eq!(state, State::Recovering(C0));
+    assert!(effects.contains(&Effect::RecoverComponent(C0)));
+}
+
+/// CorruptionDetected while in Updating (required component) → Recovering
+/// via the SupervisingPlatform superstate handler.
+#[test]
+fn corruption_in_updating_triggers_recovery() {
+    let (effects, state) = drive(
+        passive_required(&[C0]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::UpdateRequest,
+            Event::CorruptionDetected(C0),
+        ],
+    );
+    assert_eq!(state, State::Recovering(C0));
+    assert!(effects.contains(&Effect::RecoverComponent(C0)));
+}
+
+/// Concurrent faults: corruption of a *different* component arriving while the
+/// machine is already in `Recovering` re-targets recovery at the new component.
+/// `Recovering` is a supervised state, so `CorruptionDetected` falls through to
+/// the `SupervisingPlatform` handler even mid-recovery — the one supervising
+/// state with no other corruption-during-flight test. The second (Required)
+/// fault displaces the first: the machine ends in `Recovering(C2)`.
+#[test]
+fn corruption_while_recovering_retargets_to_new_component() {
+    let (effects, state) = drive(
+        passive_required(&[C0, C1, C2]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::VerificationPassed(C1),
+            Event::VerificationPassed(C2), // walk done → Ready
+            Event::CorruptionDetected(C1), // → Recovering(C1)
+            Event::CorruptionDetected(C2), // arrives mid-recovery → Recovering(C2)
+        ],
+    );
+    assert_eq!(state, State::Recovering(C2));
+    // Both recovery episodes kicked off a recovery.
+    assert!(effects.contains(&Effect::RecoverComponent(C1)));
+    assert!(effects.contains(&Effect::RecoverComponent(C2)));
+    assert!(!effects.contains(&Effect::LatchLockdown));
+}
+
+/// An `UpdateRequest` arriving mid-recovery is declined, not silently dropped:
+/// the machine emits `ReportUpdateDeferred` and stays in `Recovering`, leaving
+/// the in-flight recovery untouched (single-flight, recovery-priority).
+#[test]
+fn update_request_while_recovering_is_deferred() {
+    let (effects, state) = drive(
+        passive_required(&[C0, C1]),
+        &[
+            BOOT,
+            Event::VerificationFailed(C0), // → Recovering(C0)
+            Event::UpdateRequest,          // declined while recovering
+        ],
+    );
+    assert_eq!(state, State::Recovering(C0));
+    assert_eq!(effects.last(), Some(&Effect::ReportUpdateDeferred));
+}
+
+/// A second `UpdateRequest` while an update is already staged (`Updating`) is
+/// declined the same way — reported, not dropped, and the staged update is
+/// left in place.
+#[test]
+fn update_request_while_updating_is_deferred() {
+    let (effects, state) = drive(
+        passive_required(&[C0]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::UpdateRequest, // → Updating
+            Event::UpdateRequest, // declined while updating
+        ],
+    );
+    assert_eq!(state, State::Updating);
+    assert_eq!(effects.last(), Some(&Effect::ReportUpdateDeferred));
+}
+
+/// An `UpdateRequest` while the chain walk is still finishing (`AwaitingReady`)
+/// is declined too: the machine is not yet `Ready`, so it reports the refusal
+/// and keeps waiting on the outstanding component.
+#[test]
+fn update_request_while_awaiting_ready_is_deferred() {
+    let (effects, state) = drive(
+        chain(&[
+            (C0, ComponentAttrs::active_required()),
+            (C1, ComponentAttrs::passive_required()),
+        ]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0), // active released → AwaitingReady(Some(C0))
+            Event::UpdateRequest,          // declined while awaiting readiness
+        ],
+    );
+    assert_eq!(state, State::AwaitingReady(Some(C0)));
+    assert_eq!(effects.last(), Some(&Effect::ReportUpdateDeferred));
+}
+
+/// Negative control: from `Ready` an `UpdateRequest` is *accepted* — it starts
+/// an update (→ `Updating`) and never emits `ReportUpdateDeferred`. `Ready`
+/// intercepts the request upstream, so it can never reach the deferral arm.
+#[test]
+fn update_request_in_ready_starts_update_not_deferred() {
+    let (effects, state) = drive(
+        passive_required(&[C0]),
+        &[BOOT, Event::VerificationPassed(C0), Event::UpdateRequest],
+    );
+    assert_eq!(state, State::Updating);
+    assert!(!effects.contains(&Effect::ReportUpdateDeferred));
+}
+
+/// UpdateVerified activates the staged image and returns to Ready.
+/// (Complements update_rollback_is_not_recovery which tests UpdateRejected.)
+#[test]
+fn update_verified_activates_update() {
+    let (effects, state) = drive(
+        passive_required(&[C0]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::UpdateRequest,
+            Event::UpdateVerified,
+        ],
+    );
+    assert_eq!(state, State::Ready);
+    assert!(effects.contains(&Effect::ActivateUpdate));
+    assert!(!effects.contains(&Effect::DiscardStaged));
+    assert!(!effects.contains(&Effect::RecoverComponent(C0)));
+}
+
+/// The anti-rollback floor is committed only on a proven-healthy boot, never
+/// at activation. `UpdateVerified` activates the image (authentication) but
+/// must NOT emit `CommitSvnFloor`; a later `BootConfirmed` (the runtime health
+/// proof) is what advances the floor. This pins the decoupling so activation
+/// can never silently commit the floor early.
+#[test]
+fn svn_floor_commits_on_boot_confirmed_not_on_activation() {
+    // Activation alone: no floor commit yet.
+    let (activated, activated_state) = drive(
+        passive_required(&[C0]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::UpdateRequest,
+            Event::UpdateVerified,
+        ],
+    );
+    assert_eq!(activated_state, State::Ready);
+    assert!(activated.contains(&Effect::ActivateUpdate));
+    assert!(!activated.contains(&Effect::CommitSvnFloor(C0)));
+
+    // Proven-healthy boot: the floor advances now, without leaving Ready.
+    let (confirmed, confirmed_state) = drive(
+        passive_required(&[C0]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::UpdateRequest,
+            Event::UpdateVerified,
+            Event::BootConfirmed(C0),
+        ],
+    );
+    assert_eq!(confirmed_state, State::Ready);
+    assert!(confirmed.contains(&Effect::CommitSvnFloor(C0)));
+}
+
+/// Commit-or-lock watchdog: while the activated-but-not-committed window is
+/// open (update activated, `BootConfirmed` not yet seen), a `CommitTimeout`
+/// fails closed — the machine latches `Locked` rather than leaving the
+/// downgrade window open indefinitely, and never commits the unproven image.
+#[test]
+fn commit_timeout_while_pending_latches_locked() {
+    let (effects, state) = drive(
+        passive_required(&[C0]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::UpdateRequest,
+            Event::UpdateVerified,
+            // Window open: activated, awaiting BootConfirmed. Watchdog fires.
+            Event::CommitTimeout,
+        ],
+    );
+    assert_eq!(state, State::Locked);
+    assert!(effects.contains(&Effect::ActivateUpdate));
+    assert!(effects.contains(&Effect::LatchLockdown));
+    // The floor was never advanced for the unproven image.
+    assert!(!effects.contains(&Effect::CommitSvnFloor(C0)));
+}
+
+/// Once `BootConfirmed` has committed the floor the window is closed, so a
+/// later (stale) `CommitTimeout` is a no-op: the machine stays `Ready` and does
+/// not lock.
+#[test]
+fn commit_timeout_after_confirm_is_stale_noop() {
+    let (effects, state) = drive(
+        passive_required(&[C0]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::UpdateRequest,
+            Event::UpdateVerified,
+            Event::BootConfirmed(C0),
+            // Window already closed by the commit above.
+            Event::CommitTimeout,
+        ],
+    );
+    assert_eq!(state, State::Ready);
+    assert!(effects.contains(&Effect::CommitSvnFloor(C0)));
+    assert!(!effects.contains(&Effect::LatchLockdown));
+}
+
+/// A `CommitTimeout` in steady-state `Ready` with no update in flight (no
+/// window open) is stale and ignored — a spurious watchdog fire must not lock a
+/// healthy device.
+#[test]
+fn commit_timeout_without_pending_is_ignored() {
+    let (effects, state) = drive(
+        passive_required(&[C0]),
+        &[BOOT, Event::VerificationPassed(C0), Event::CommitTimeout],
+    );
+    assert_eq!(state, State::Ready);
+    assert!(!effects.contains(&Effect::LatchLockdown));
+}
+
+/// A recovery that intervenes during the commit window voids it: after the
+/// machine recovers and walks back to `Ready`, the window is closed, so a
+/// `CommitTimeout` no longer locks. This pins that entering `Recovering` clears
+/// `pending_commit`, so the flag cannot go stale across a recovery round-trip.
+#[test]
+fn recovery_clears_commit_window() {
+    let (effects, state) = drive(
+        passive_required(&[C0]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::UpdateRequest,
+            Event::UpdateVerified,
+            // Window open, then a Required corruption preempts to recovery.
+            Event::CorruptionDetected(C0),
+            // Restore succeeds (retry < MAX_RETRY) and re-walk re-verifies.
+            Event::Restored(C0),
+            Event::VerificationPassed(C0),
+            // Back in Ready with the window voided; the watchdog is now stale.
+            Event::CommitTimeout,
+        ],
+    );
+    assert_eq!(state, State::Ready);
+    assert!(!effects.contains(&Effect::LatchLockdown));
+}
+
+/// Locked is a terminal state: no effects are produced in response to any
+/// event after the machine latches.
+#[test]
+fn locked_is_terminal() {
+    let mut c: heapless::Vec<(ComponentId, ComponentAttrs), CAPACITY> = heapless::Vec::new();
+    c.push((C0, ComponentAttrs::passive_required())).unwrap();
+    // max_retry = 1 so the first failed restore latches immediately.
+    let mut orch = Orchestrator::<CAPACITY, ECAP>::new(c.try_into().expect("valid chain"), 1);
+    let mut effects: Vec<Effect> = Vec::new();
+
+    for ev in [BOOT, Event::VerificationFailed(C0), Event::Restored(C0)] {
+        orch.dispatch_with(ev, |e| {
+            effects.push(e);
+            Ok(())
+        });
+    }
+    assert_eq!(orch.state(), State::Locked);
+
+    let count_before = effects.len();
+    for ev in [
+        BOOT,
+        Event::VerificationPassed(C0),
+        Event::AttestationChallenge,
+        Event::UpdateRequest,
+        Event::CorruptionDetected(C0),
+    ] {
+        orch.dispatch_with(ev, |e| {
+            effects.push(e);
+            Ok(())
+        });
+    }
+    assert_eq!(
+        effects.len(),
+        count_before,
+        "Locked state must produce no effects"
+    );
+}
+
+/// An Isolable component at the head of the chain exhausts its recovery
+/// retries, gets held, and the walk continues to the remaining required
+/// components.
+#[test]
+fn isolable_first_component_exhausts_then_walk_continues() {
+    let mut script = std::vec![BOOT];
+    for _ in 0..MAX_RETRY {
+        script.push(Event::VerificationFailed(C0));
+        script.push(Event::Restored(C0));
+    }
+    script.push(Event::VerificationPassed(C1));
+    let (effects, state) = drive(
+        chain(&[
+            (C0, ComponentAttrs::passive_isolable()),
+            (C1, ComponentAttrs::passive_required()),
+        ]),
+        &script,
+    );
+    assert_eq!(state, State::Ready);
+    assert!(!effects.contains(&Effect::ReleaseReset(C0)));
+    assert!(effects.contains(&Effect::ReleaseReset(C1)));
+    // Recovery IS attempted before C0 is classified and held.
+    assert!(effects.contains(&Effect::RecoverComponent(C0)));
+    assert!(effects.contains(&Effect::AssertReset(C0)));
+}
+
+/// The speculative read emits ReleaseReset · ReadFirmware · VerifyFirmware
+/// all in the same handler as VerificationPassed for an Active component,
+/// before ComponentReady has arrived. Verifies both presence and order.
+#[test]
+fn speculative_read_effects_are_emitted_together() {
+    let mut orch = Orchestrator::<CAPACITY, ECAP>::new(
+        chain(&[
+            (C0, ComponentAttrs::active_required()),
+            (C1, ComponentAttrs::passive_required()),
+        ])
+        .try_into()
+        .expect("valid chain"),
+        MAX_RETRY,
+    );
+    let mut effects: Vec<Effect> = Vec::new();
+
+    orch.dispatch_with(BOOT, |e| {
+        effects.push(e);
+        Ok(())
+    });
+    assert_eq!(
+        effects,
+        std::vec![Effect::ReadFirmware(C0), Effect::VerifyFirmware(C0)],
+    );
+
+    effects.clear();
+    orch.dispatch_with(Event::VerificationPassed(C0), |e| {
+        effects.push(e);
+        Ok(())
+    });
+    // All three effects emitted in the same handler, before ComponentReady.
+    assert_eq!(
+        effects,
+        std::vec![
+            Effect::ReleaseReset(C0),
+            Effect::ReadFirmware(C1),
+            Effect::VerifyFirmware(C1),
+        ],
+    );
+    assert_eq!(orch.state(), State::AwaitingReady(Some(C0)));
+}
+
+/// A chain with a single Active component goes directly to Ready on
+/// VerificationPassed — no AwaitingReady, no ComponentReady required.
+/// This exercises the `chain done` branch of PreSupervision for an
+/// Active component (distinct from the multi-component Active path which
+/// transitions to AwaitingReady).
+#[test]
+fn single_active_chain_goes_directly_to_ready() {
+    let mut c: heapless::Vec<(ComponentId, ComponentAttrs), CAPACITY> = heapless::Vec::new();
+    c.push((C0, ComponentAttrs::active_required())).unwrap();
+    let (effects, state) = drive(c, &[BOOT, Event::VerificationPassed(C0)]);
+    assert_eq!(state, State::Ready);
+    assert_eq!(
+        effects,
+        std::vec![
+            Effect::ReadFirmware(C0),
+            Effect::VerifyFirmware(C0),
+            Effect::ReleaseReset(C0),
+        ],
+    );
+}
+
+/// An empty component list is not a valid chain of trust.
+#[test]
+fn chain_rejects_empty() {
+    let empty = heapless::Vec::<(ComponentId, ComponentAttrs), CAPACITY>::new();
+    assert_eq!(Chain::try_from(empty).unwrap_err(), ChainError::Empty);
+}
+
+/// A repeated `ComponentId` is rejected: the reducer's linear id lookups would
+/// otherwise be ambiguous.
+#[test]
+fn chain_rejects_duplicate_id() {
+    let v = chain(&[
+        (C0, ComponentAttrs::passive_required()),
+        (C0, ComponentAttrs::passive_required()),
+    ]);
+    assert_eq!(Chain::try_from(v).unwrap_err(), ChainError::DuplicateId(C0),);
+}
+
+/// A `depends_on` that names a component not in the chain is rejected.
+#[test]
+fn chain_rejects_unknown_dependency() {
+    let v = chain(&[(C1, ComponentAttrs::passive_required().with_depends_on(C0))]);
+    assert_eq!(
+        Chain::try_from(v).unwrap_err(),
+        ChainError::UnknownDependency {
+            component: C1,
+            depends_on: C0,
+        },
+    );
+}
+
+/// A dependency must appear strictly earlier in the walk than its dependent;
+/// a forward reference is rejected.
+#[test]
+fn chain_rejects_forward_dependency() {
+    let v = chain(&[
+        (C0, ComponentAttrs::passive_required().with_depends_on(C1)),
+        (C1, ComponentAttrs::passive_cascading()),
+    ]);
+    assert_eq!(
+        Chain::try_from(v).unwrap_err(),
+        ChainError::ForwardDependency {
+            component: C0,
+            depends_on: C1,
+        },
+    );
+}
+
+/// A component may not depend on itself.
+#[test]
+fn chain_rejects_self_dependency() {
+    let v = chain(&[(C0, ComponentAttrs::passive_required().with_depends_on(C0))]);
+    assert_eq!(
+        Chain::try_from(v).unwrap_err(),
+        ChainError::ForwardDependency {
+            component: C0,
+            depends_on: C0,
+        },
+    );
+}
+
+/// A well-formed chain with a backward dependency validates successfully.
+#[test]
+fn chain_accepts_valid_dependency() {
+    let v = chain(&[
+        (C0, ComponentAttrs::passive_cascading()),
+        (C1, ComponentAttrs::passive_required().with_depends_on(C0)),
+    ]);
+    assert!(Chain::try_from(v).is_ok());
+}
+
+/// A [`Platform`] that records every effect and fails a chosen one, to exercise
+/// the effect failure channel.
+struct FailOn {
+    trigger: Effect,
+    recorded: Vec<Effect>,
+    failed: bool,
+}
+
+impl FailOn {
+    fn new(trigger: Effect) -> Self {
+        Self {
+            trigger,
+            recorded: Vec::new(),
+            failed: false,
+        }
+    }
+}
+
+impl Platform for FailOn {
+    fn execute(&mut self, effect: Effect) -> Result<(), EffectError> {
+        self.recorded.push(effect);
+        if effect == self.trigger {
+            self.failed = true;
+            Err(EffectError)
+        } else {
+            Ok(())
+        }
+    }
+}
+
+/// A failed reset actuation is fail-closed: the driver injects `EffectFailed`
+/// and the machine latches to `Locked`, emitting `LatchLockdown`.
+#[test]
+fn effect_failure_latches_lockdown() {
+    let mut c = heapless::Vec::<(ComponentId, ComponentAttrs), CAPACITY>::new();
+    c.push((C0, ComponentAttrs::passive_required())).unwrap();
+    let mut orch =
+        Orchestrator::<CAPACITY, ECAP>::new(c.try_into().expect("valid chain"), MAX_RETRY);
+    let mut plat = FailOn::new(Effect::ReleaseReset(C0));
+
+    orch.dispatch(&mut plat, BOOT); // ReadFirmware/VerifyFirmware C0 — both succeed
+    orch.dispatch(&mut plat, Event::VerificationPassed(C0)); // ReleaseReset(C0) fails
+
+    assert!(plat.failed, "the trigger effect should have been attempted");
+    assert_eq!(orch.state(), State::Locked);
+    assert!(plat.recorded.contains(&Effect::LatchLockdown));
+}
+
+/// A failed isolation actuation (`AssertReset`) is equally fail-closed: even a
+/// non-required component's containment failing latches the platform.
+#[test]
+fn failed_isolation_actuation_latches_lockdown() {
+    let mut c = heapless::Vec::<(ComponentId, ComponentAttrs), CAPACITY>::new();
+    c.push((C0, ComponentAttrs::passive_required())).unwrap();
+    c.push((C1, ComponentAttrs::passive_isolable())).unwrap();
+    let mut orch =
+        Orchestrator::<CAPACITY, ECAP>::new(c.try_into().expect("valid chain"), MAX_RETRY);
+    let mut plat = FailOn::new(Effect::AssertReset(C1));
+
+    orch.dispatch(&mut plat, BOOT);
+    orch.dispatch(&mut plat, Event::VerificationPassed(C0));
+    orch.dispatch(&mut plat, Event::VerificationPassed(C1)); // C1 released → Ready
+    orch.dispatch(&mut plat, Event::CorruptionDetected(C1)); // isolable → AssertReset(C1) fails
+
+    assert!(plat.failed);
+    assert_eq!(orch.state(), State::Locked);
+    assert!(plat.recorded.contains(&Effect::LatchLockdown));
+}
+
+/// A failed recovery actuation is fail-closed too: if the shell cannot even
+/// recover a required component, the platform latches rather
+/// than continuing with an unrecovered component.
+#[test]
+fn failed_restore_actuation_latches_lockdown() {
+    let mut c = heapless::Vec::<(ComponentId, ComponentAttrs), CAPACITY>::new();
+    c.push((C0, ComponentAttrs::passive_required())).unwrap();
+    let mut orch =
+        Orchestrator::<CAPACITY, ECAP>::new(c.try_into().expect("valid chain"), MAX_RETRY);
+    let mut plat = FailOn::new(Effect::RecoverComponent(C0));
+
+    orch.dispatch(&mut plat, BOOT);
+    orch.dispatch(&mut plat, Event::VerificationFailed(C0)); // → Recovering → RecoverComponent(C0) fails
+
+    assert!(plat.failed);
+    assert_eq!(orch.state(), State::Locked);
+    assert!(plat.recorded.contains(&Effect::LatchLockdown));
+}
+
+/// The lockdown latch is the last line of defense: even if *it* fails to
+/// actuate, the machine must not spin. The re-injected `EffectFailed` is
+/// ignored while `Locked`, so dispatch terminates and the latch is attempted
+/// exactly once.
+#[test]
+fn failed_lockdown_actuation_does_not_loop() {
+    let mut c = heapless::Vec::<(ComponentId, ComponentAttrs), CAPACITY>::new();
+    c.push((C0, ComponentAttrs::passive_required())).unwrap();
+    let mut orch =
+        Orchestrator::<CAPACITY, ECAP>::new(c.try_into().expect("valid chain"), MAX_RETRY);
+    let mut plat = FailOn::new(Effect::LatchLockdown);
+
+    // An unprovisioned power-on latches immediately; the latch actuation fails.
+    orch.dispatch(&mut plat, Event::PowerGood(PowerOnResult::Unprovisioned));
+
+    assert!(plat.failed, "the lockdown latch should have been attempted");
+    assert_eq!(orch.state(), State::Locked);
+    assert_eq!(
+        plat.recorded
+            .iter()
+            .filter(|&&e| e == Effect::LatchLockdown)
+            .count(),
+        1,
+        "a failing latch must not re-latch forever",
+    );
+}
+
+/// Actuation is fail-fast: once an effect in a batch fails, no effect ordered
+/// *after* it is attempted. Here `VerificationPassed(C0)` emits the batch
+/// `[ReleaseReset(C0), ReadFirmware(C1), VerifyFirmware(C1)]`; failing the first
+/// effect must abandon the two speculative reads of `C1` and latch, rather than
+/// actuate them for a transition that is immediately overridden by `Locked`.
+#[test]
+fn batch_actuation_is_fail_fast() {
+    let mut orch = Orchestrator::<CAPACITY, ECAP>::new(
+        passive_required(&[C0, C1]).try_into().expect("valid chain"),
+        MAX_RETRY,
+    );
+    let mut plat = FailOn::new(Effect::ReleaseReset(C0));
+
+    orch.dispatch(&mut plat, BOOT); // ReadFirmware/VerifyFirmware C0 — both succeed
+    orch.dispatch(&mut plat, Event::VerificationPassed(C0)); // ReleaseReset(C0) fails first
+
+    assert!(plat.failed, "the failing effect should have been attempted");
+    assert!(
+        plat.recorded.contains(&Effect::ReleaseReset(C0)),
+        "the failing effect itself is attempted",
+    );
+    assert!(
+        !plat.recorded.contains(&Effect::ReadFirmware(C1)),
+        "an effect ordered after the failure must not be actuated",
+    );
+    assert!(
+        !plat.recorded.contains(&Effect::VerifyFirmware(C1)),
+        "an effect ordered after the failure must not be actuated",
+    );
+    assert_eq!(orch.state(), State::Locked);
+    assert!(plat.recorded.contains(&Effect::LatchLockdown));
+}
+
+/// GAP 1 (red): a `Required` corruption of another device while an update is in
+/// flight preempts the update but leaves the staged image dangling. Correct
+/// behavior emits `DiscardStaged` when leaving `Updating` for recovery.
+#[test]
+fn corruption_during_update_discards_staged() {
+    let (effects, state) = drive(
+        passive_required(&[C0, C1]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::VerificationPassed(C1), // → Ready
+            Event::UpdateRequest,          // → Updating (AuthenticateUpdate, StageUpdate)
+            Event::CorruptionDetected(C1), // Required corruption preempts the update
+        ],
+    );
+    assert_eq!(state, State::Recovering(C1));
+    assert!(
+        effects.contains(&Effect::DiscardStaged),
+        "leaving Updating for recovery must discard the staged image",
+    );
+    assert!(
+        effects.contains(&Effect::ReportUpdateAborted),
+        "preempting an in-flight update must report it aborted, not drop it silently",
+    );
+}
+
+/// The abort report is *only* for a genuine preemption. An `Isolable`
+/// corruption of another device while `Updating` is contained (`Handled`) and
+/// the update continues untouched — so neither `DiscardStaged` nor
+/// `ReportUpdateAborted` is emitted, and the machine stays in `Updating`.
+#[test]
+fn contained_corruption_during_update_does_not_abort() {
+    let (effects, state) = drive(
+        chain(&[
+            (C0, ComponentAttrs::passive_required()),
+            (C1, ComponentAttrs::passive_isolable()),
+        ]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::VerificationPassed(C1), // → Ready
+            Event::UpdateRequest,          // → Updating
+            Event::CorruptionDetected(C1), // isolable: contained, update survives
+        ],
+    );
+    assert_eq!(state, State::Updating);
+    assert!(!effects.contains(&Effect::ReportUpdateAborted));
+    assert!(!effects.contains(&Effect::DiscardStaged));
+}
+
+/// GAP 2 (red): a second `Required` corruption while already recovering clobbers
+/// the single `Recovering` slot, and because `Restored` is id-blind a restore
+/// for the *displaced* target is mis-credited to the new one. Correct behavior:
+/// a `Restored` whose id is not the recovery target does not advance recovery.
+#[test]
+fn restored_for_wrong_component_does_not_advance_recovery() {
+    let (_effects, state) = drive(
+        passive_required(&[C0, C1]),
+        &[
+            BOOT,
+            Event::VerificationPassed(C0),
+            Event::VerificationPassed(C1), // → Ready
+            Event::CorruptionDetected(C0), // → Recovering(C0)
+            Event::CorruptionDetected(C1), // clobbers → Recovering(C1)
+            Event::Restored(C0),           // restore of the *displaced* target
+        ],
+    );
+    assert_eq!(
+        state,
+        State::Recovering(C1),
+        "a Restored for a non-target component must not be credited to the current recovery",
+    );
+}
+
+// ---------------------------------------------------------------------------
+// Property / model test
+//
+// Instead of enumerating hand-picked traces, drive the machine with thousands
+// of *arbitrary* event sequences — including nonsensical and adversarial
+// orderings a hostile platform could inject — and assert the one safety
+// invariant that no example-based test generalizes across the whole input
+// space. It complements the example suite: those pin *behavior*, this pins
+// *safety* over every ordering.
+//
+// The lockdown-absorbing and membership properties are intentionally *not*
+// re-checked here — they are already covered by dedicated example tests
+// (`self_verification_failure_latches_immediately`, the boundary-guard
+// `*_out_of_chain_id_is_dropped` cases), so repeating them under the fuzzer
+// would add cost without signal.
+//
+// Invariant checked:
+//   INV8  Verify-before-release. A component is released (`ReleaseReset`)
+//         only if it was verified (`VerifyFirmware`) since its most recent
+//         hold. A component starts held; `AssertReset` and `RecoverComponent`
+//         re-hold it. So a component is never released on a stale verification
+//         from before it was last taken down — the whole-input-space form of
+//         "recovery is a re-boot" / "no live component trusted without an
+//         at-rest recheck". This is the property the quiesce change introduced
+//         and the one no single example trace captures.
+// ---------------------------------------------------------------------------
+
+/// SplitMix64 — a tiny, dependency-free deterministic PRNG. `no_std`/bazel
+/// friendly: no external proptest/quickcheck crate required.
+struct SplitMix64(u64);
+
+impl SplitMix64 {
+    fn next_u64(&mut self) -> u64 {
+        self.0 = self.0.wrapping_add(0x9E37_79B9_7F4A_7C15);
+        let mut z = self.0;
+        z = (z ^ (z >> 30)).wrapping_mul(0xBF58_476D_1CE4_E5B9);
+        z = (z ^ (z >> 27)).wrapping_mul(0x94D0_49BB_1331_11EB);
+        z ^ (z >> 31)
+    }
+
+    /// Uniform-ish value in `0..n`.
+    fn below(&mut self, n: u32) -> u32 {
+        (self.next_u64() % n as u64) as u32
+    }
+}
+
+/// Build one random event over the given id palette. Id-less events ignore it.
+fn random_event(rng: &mut SplitMix64, ids: &[ComponentId]) -> Event {
+    let id = ids[rng.below(ids.len() as u32) as usize];
+    match rng.below(15) {
+        0 => Event::VerificationPassed(id),
+        1 => Event::VerificationFailed(id),
+        2 => Event::ComponentReady(id),
+        3 => Event::Booted(id),
+        4 => Event::BootConfirmed(id),
+        5 => Event::CorruptionDetected(id),
+        6 => Event::Restored(id),
+        7 => Event::Timeout(id),
+        8 => Event::AttestationChallenge,
+        9 => Event::UpdateRequest,
+        10 => Event::UpdateVerified,
+        11 => Event::UpdateRejected,
+        12 => Event::RecoveryFailed,
+        13 => Event::CommitTimeout,
+        _ => Event::EffectFailed,
+    }
+}
+
+#[test]
+fn property_verify_before_release_holds_under_random_sequences() {
+    const RUNS: u64 = 4000;
+    const MAX_LEN: u32 = 24;
+
+    // C0..C2 are in-chain; C3 is intentionally out-of-chain — fed as noise so
+    // the fuzzer also exercises the dispatch-boundary guard, but membership is
+    // asserted by the dedicated boundary-guard example tests, not here.
+    let palette = [C0, C1, C2, C3];
+
+    for seed in 0..RUNS {
+        let mut rng = SplitMix64(seed.wrapping_mul(0xD1B5_4A32_D192_ED03).wrapping_add(1));
+
+        let ch = chain(&[
+            (C0, ComponentAttrs::passive_required()),
+            (C1, ComponentAttrs::active_isolable()),
+            (C2, ComponentAttrs::passive_required()),
+        ]);
+        let mut orch =
+            Orchestrator::<CAPACITY, ECAP>::new(ch.try_into().expect("valid chain"), MAX_RETRY);
+        let mut platform = Recorder::new();
+
+        // Power on first — usually a clean provisioned boot, occasionally a
+        // degraded power-on result so lockdown paths get exercised too.
+        let boot = match rng.below(12) {
+            0 => Event::PowerGood(PowerOnResult::Unprovisioned),
+            1 => Event::PowerGood(PowerOnResult::SelfVerificationFailed),
+            _ => BOOT,
+        };
+        orch.dispatch(&mut platform, boot);
+
+        let len = 1 + rng.below(MAX_LEN);
+        for _ in 0..len {
+            let event = random_event(&mut rng, &palette);
+            orch.dispatch(&mut platform, event);
+        }
+
+        // Post-hoc structural scan over the full effect trace.
+        let trace = &platform.recorded;
+
+        // INV8: verify-before-release. A component starts held; AssertReset
+        // and RecoverComponent re-hold it; VerifyFirmware clears it for release.
+        let mut verified = [false; CAPACITY];
+
+        for effect in trace {
+            match effect {
+                Effect::AssertReset(id) | Effect::RecoverComponent(id) => {
+                    verified[id.get() as usize] = false;
+                }
+                Effect::VerifyFirmware(id) => {
+                    verified[id.get() as usize] = true;
+                }
+                Effect::ReleaseReset(id) => {
+                    assert!(
+                        verified[id.get() as usize],
+                        "seed {seed}: released {id:?} without a verify since its last hold",
+                    );
+                }
+                _ => {}
+            }
+        }
+    }
+}