pub trait EffectsSurviveRestart:
StorageAtomicity
+ SequentialChainState
+ CorrectValidator { }Expand description
Lemma (Effects are a function of persisted state). Everything a chain worker emits to other chains is derivable from that chain’s saved state, and re-emitting it is harmless. So a worker that crashes between persisting a transition and dispatching its effects loses nothing: on restart it re-derives them, and the recipients absorb the repeats.
Proof. Two halves, one per side of the delivery.
The sender re-derives. ChainWorkerState::create_network_actions does not read the
transition’s result. It calls reconcile_tracked_outboxes and then build_network_actions,
which builds the pending cross-chain requests from the reconciled outbox index — part of
the chain’s view, and therefore part of what save() wrote. By StorageAtomicity that view
is consistent after any crash, so the same set of actions is derivable again.
The recipient absorbs repeats. A redelivered bundle is filtered out before it reaches the
inbox: ChainWorkerState::select_message_bundles drops every bundle whose height is below the
inbox’s next_block_height_to_receive, logging them as repeated. Inbox::add_bundle would not
absorb one in any case — it requires the Cursor to be at least next_cursor_to_add and
rejects anything lower with InboxError::IncorrectOrder. Its two reconciliation branches cover
different situations: removed_bundles a bundle this chain consumed by anticipation before
delivery, and restored_cursor a bundle whose effects a checkpoint restore has already baked
into the state. Delivery is therefore at-least-once with idempotent effect. ∎
reset_and_reexecute_chain relies on exactly this from the other direction: having wiped and
replayed a chain, it returns a CrossChainRequest::RevertConfirm to every known sender,
asking them to re-derive and resend anything the replay dropped from the inbox.
The crash windows. CorrectValidator admits a crash at any point, and the four windows
have different mechanisms — only two are this lemma:
| crash window | what covers it |
|---|---|
before save() | the transition is rolled back and the client retries; needs re-execution to reproduce the outcome |
after save(), before dispatch | this lemma, sender half |
during save() | StorageAtomicity |
| after dispatch, recipient restarts | this lemma, recipient half |