Trait CheckpointRestoresExecutionState 

pub trait CheckpointRestoresExecutionState: SequentialChainState { }

Lemma (A checkpoint restores exactly the execution state it captured). Applying a checkpoint’s blobs reproduces the chain’s execution state as it stood immediately before the checkpoint block, in full.

Proof. Four parts.

The dump is total. ExecutionStateView has exactly one field: an inner view holding the system state, the user applications’ key-value stores, and the two previous-block maps. Everything the outer view exposes is reached by dereferencing into it, and dump_content serializes that inner view’s persisted content whole. No part of the execution state can be left out of a checkpoint by oversight — totality here is structural, not an inventory someone has to keep current as fields are added.

The dump is quiescent. dump_content reads from storage and refuses to run while the view holds pending in-memory changes, failing with ViewError::HasPendingChanges. prepare_checkpoint is therefore a pre-block operation, run before block-level setup mutates the chain. The captured bytes are the committed pre-block state — exactly what a bootstrapping node restores before re-applying the certified checkpoint block.

The bytes are pinned by the certificate. The dump is chunked at the epoch’s maximum_blob_size and published as created blobs of the checkpoint block, their ids listed in that block’s OracleResponse::Checkpoint as execution_state_blobs. Blobs are content addressed, so a node fetching them cannot be handed different bytes; and the id list is part of the certified outcome, so it cannot be pointed at a different dump. Integrity here is free, in the way integrity of any blob is free — availability is the separate question, and is linera_core::proof::availability::CertifiedBlockIsAvailable’s.

The hash agrees. ExecutionStateView::crypto_hash_mut derives the state hash from the inner view’s historical hash, and restore_from_content records the hash of the restored bytes as the new stored hash. A node that restores and then re-applies the certified checkpoint block computes the state_hash that block certifies, so a restore that went wrong does not go unnoticed. ∎

This is the execution state, not the chain. The two totality arguments point opposite ways and it is worth being exact about which applies. ExecutionStateView has one field, so the dump covers all of it. ChainStateView has sixteen, of which the blob covers exactly one — execution_state. Inboxes, outboxes, the tip, the chain manager, the block-hash index and the event trackers are all outside it.

Two of those are restored by named mechanisms rather than by the blob, and a checkpoint would be unusable without them:

• Inboxes. Each inbox’s restored_cursor is seeded from PreparedCheckpoint::inbox_cursors, carried in the certified oracle response rather than the dump (CheckpointPreservesConsumptionBoundary).
• Outboxes. outboxes, outbox_counters and nonempty_outboxes are rebuilt by ChainStateView’s restore_outboxes_from_unfinalized, run once after restore_from_content, from the on-chain unfinalized_message_blocks (AcknowledgedMessagesMayBeForgotten). Off-chain outbox state is not certified, so without this a bootstrapped node would go quiet on cross-chain delivery while looking healthy.

So a checkpoint is not a snapshot of a chain. It is a certified snapshot of the chain’s execution state, plus enough certified bookkeeping to reconstruct the message-passing state around it. What the remaining chain-state fields hold after a bootstrap is outside this lemma.

Residual obligation. restore_from_content leaves the in-memory view stale: its documentation requires the caller to reload afterwards, and nothing in the type enforces it. A caller that skipped the reload would continue against a view that no longer describes storage. This is the same shape as SafetyStateRecovery — a correctness condition discharged by convention at the call site rather than by construction.

Implementors