Module recovery 

The recovery lattice (PSP-9 system 11, Paper III Definition 8.1 and Theorem 6).

Rejection is the steady state of a stochastic proposer, so recovery must terminate by construction. Definition 8.1’s well-formedness conditions are adopted literally, because the b + k count is a consequence of them:

• One pool, every level. b is a single non-replenishing budget shared across the whole cascade. Every horizontal repetition consumes one unit — a second fallback route, a second refinement, and a second escalation each cost one unit exactly as a re-proposal does. A per-level budget (including a separate “refinement depth” counter) would give Σ_λ b_λ + k, not b + k; refinement depth is a cap on level-2 repetitions within the shared pool, never its own pool.
• Exhaustion forbids repetition. With zero remaining budget below the top level, the next non-terminal control MUST strictly escalate.
• The top level is unconditionally terminating.

Structs

GrantedControl

What the cascade granted for one requested control.

RecoveryCascade

The shared-pool cascade for one node (Definition 8.1).

Enums

CascadeClass

Theorem 6’s four terminal classes. Recorded alongside — not in place of — the node’s Paper II NodeTerminalOutcome.

CascadeLevel

The escalation chain. k is the number of strict escalations available from level 0, i.e. Contain as u8.

FailureKind

A failure observation’s deterministic classification. The classifier is total: unknown classes map to CascadeLevel::Contain.

Functions

classify_failure

Map every failure class to its entry control (PSP-9 system 11). Total by construction — the compiler enforces it.