Module commit 

The commit rule: what it takes for a block to become final, and what a node does about it.

The protocol has a two-step commit rule outside the fast round — validate, then confirm — and a one-step rule inside it. This module pins down both, and connects “a confirmed block certificate exists” to the observable state a node reaches.

Traits

CertifiedBlockWasExecuted

Lemma (Every certified block was executed by a correct validator). If a valid ValidatedBlockCertificate for a block B exists, then some correct validator executed B’s ProposedBlock itself and obtained B’s BlockExecutionOutcome. The same follows for a ConfirmedBlockCertificate outside the fast round, by CommitRestsOnValidation; inside the fast round it holds directly, a fast proposal carrying no outcome.

CommitRestsOnValidation

Lemma (A commit outside the fast round rests on a validated block certificate). If a ConfirmedBlockCertificate for B is certified in a round r other than Round::Fast, then a valid ValidatedBlockCertificate for B in the same round r exists.

CommittedBlock

Definition (Committed block). A block B at height h of a chain is committed when a ConfirmedBlockCertificate for B, valid for the committee of its epoch, exists — that is, when a quorum has cast confirmation votes for B.

EventReadsResolveLocally

Lemma (Event reads resolve against the validator’s own storage). When a correct validator votes on a proposal that reads an event, the value it votes for is the one in its own storage under the EventId the block cites — resolved locally, exactly as an oracle call is, and never taken from the proposer.

IncomingBundlesMatchTheLocalInbox

Lemma (Incoming bundles are matched against the validator’s own inbox). A correct validator casts a validation or fast-confirmation vote for a block only if every IncomingBundle the block consumes is already present in its own inbox for that origin, and is equal to the bundle it holds there.

TipAdvancesOnlyOnValidCertificate

Lemma (The tip advances only on a verified certificate). A correct validator’s ChainTipState::next_block_height passes from h to h + 1, and its block_hashes records a hash at h, only for a block carried by a ConfirmedBlockCertificate that has passed check against the committee of the block’s epoch.