Module availability 

What a certified block guarantees to everyone else, and what a crash costs.

Agreement (CommitAgreement) says at most one block is certified per height. It says nothing about anyone being able to act on that block. The results here supply the other half: once a quorum has certified a block, any node — a validator that was down, a validator that did not exist yet, a client — can obtain it and everything needed to execute it.

Traits

BlobAdmissionIsBounded

Lemma (Unpaid blob storage is bounded). A validator’s storage of blobs that no certified block references is bounded, so pushing data at a validator buys neither storage nor availability.

BlockOutputsArePersisted

Lemma (A block’s outputs are persisted before it counts as processed). When a correct validator’s ChainTipState::next_block_height passes a height, the outputs of the block at that height are already in storage: the blobs it publishes, the events it emits, and the certificate itself. A crash before that point costs nothing but repeated work — the tip is what marks a block processed, so the block is handled again on restart and the writes are redone.

BoundedCatchUp

Caveat (Catch-up is not time-bounded). The work a node must do to reach a chain’s tip is proportional to the number of blocks it must replay, which is the height above the chain’s latest checkpoint — and nothing in the protocol bounds that distance.

BundleConsumedAtMostOnce

Lemma (A bundle is consumed at most once). No two blocks of a chain consume the same MessageBundle from the same origin, even though delivery is at-least-once.

CertifiedBlockIsAvailable

Lemma (A certified block and its dependencies are retrievable). Once a block is a CommittedBlock, any node that can reach a quorum can obtain the certificate, the ancestors it needs, and every blob and event the block requires, and can then execute it.

DeliveryAndConsumptionAreOrdered

Lemma (Bundles are delivered and consumed in order). For a given (sender, recipient) pair, bundles enter an inbox in strictly increasing Cursor order and are consumed in strictly increasing cursor order. A bundle may be passed over only if every message in it is skippable.

DeliveryIsRepairedOnDemand

Lemma (Delivery is repaired on demand, not guaranteed by the sender). A validator makes a bounded effort to deliver a bundle to its own worker for the recipient chain, and no more. What makes delivery dependable is that a client needing the bundle can always cause it: the recipient side of MissingDependenciesAreRecoverable is a repair path, not merely a diagnosis.

EffectsSurviveRestart

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.

InboxHoldsOnlySentBundles

Lemma (An inbox holds only bundles its origin really sent). Every MessageBundle in a correct validator’s inbox for an origin was produced by a block of that origin which the same validator has processed.

LockingBlobsTravelWithTheLock

Lemma (A locked block’s blobs travel with the lock). Whenever a correct validator holds a locking block, it also holds the blobs that block requires, and any node that can reach it can obtain them.

MissingDependenciesAreRecoverable

Lemma (A client can obtain everything a submission depends on). A client can always find, on the network, the data it needs in order to submit