Module checkpoints 

Event streams across a checkpoint boundary.

Traits

AcknowledgedMessagesMayBeForgotten

Lemma (A sender may forget messages its recipient has checkpointed). A chain’s checkpoint dump names only those of its blocks that still carry outgoing bundles no recipient has acknowledged consuming. Acknowledged bundles are dropped, and no future incarnation of any recipient can ask for them again.

CheckpointPreservesBlobAvailability

Lemma (A checkpoint leaves blob availability unchanged). Checkpointing neither strands a blob the chain can still reach nor silently requires one a bootstrapping node cannot obtain.

CheckpointPreservesConsumptionBoundary

Lemma (A checkpoint moves the consumption boundary and nothing else about messages). Restoring a chain from a checkpoint changes which incoming bundles are still retained, never which have been consumed. Bundles below the restored cursor are already reflected in the restored execution state and are ignored on arrival and on consumption; bundles at or above it are queued, delivered and consumed exactly as they would have been with no checkpoint at all.

CheckpointRecertifiesReferencedBlocks

Lemma (A checkpoint re-certifies the blocks its outboxes still reference). The older blocks a chain still owes delivery from remain acceptable to a node that has never seen them, even after the committee that signed them has been removed.

CheckpointRestoresExecutionState

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.

CheckpointSummarizesUserStreams

Lemma (A checkpoint summarizes every user stream that published since the previous one). At a checkpoint, each application holding an event stream that has published since the previous checkpoint is given the chance to replace that stream’s history with a summary, and no system stream is ever in that position.

EventFloorTracksCheckpoints

Invariant (A stream’s readable floor is its first index since the last checkpoint). For every event stream of a chain, StreamCounts::first_index is the index of the first event published to that stream since the most recent checkpoint, and the indices from there up to StreamCounts::next_index are contiguous. Events below the floor may have been pruned and are unavailable to a node that bootstrapped from that checkpoint; events at or above it are untouched by checkpointing.