Module safety 

The safety proof: at most one block is ever committed per chain and height.

The argument has one non-trivial step, LockPreservation, an induction over rounds showing that once a block is committed no later round can validate anything else. Everything before it is local implementation properties and per-round uniqueness; everything after it is bookkeeping.

Nothing in this module depends on synchrony, on message delivery, or on any validator being responsive. Safety holds in every execution permitted by MaxByzantineWeight, including ones where the protocol makes no progress at all.

Traits

Accountability

Remark (Agreement failure is attributable). The converse of CommitAgreement: when it fails, the failure is not silent. Two conflicting confirmed certificates are self-contained evidence convicting validators of at least validity_threshold weight, and no correct validator is ever convictable.

CommitAgreement

Theorem (Commit agreement). For a given chain and height, all valid ConfirmedBlockCertificates certify the same block. Equivalently: no two conflicting blocks (ConflictingBlocks) are ever both committed.

FastRetryPreservesBlock

Lemma (A fast retry cannot change the block). Let a block A be confirmed in Round::Fast, and let a correct validator later cast a validation vote for a block B on a proposal whose OriginalProposal::Fast retries A’s proposal. Then B = A.

LockPreservation

Theorem (Lock preservation). Suppose a valid ConfirmedBlockCertificate for a block A is certified in round r, at some height of some chain. Then for every round s ≥ r, every valid ValidatedBlockCertificate at that height and round s certifies A.

SafetyScope

Remark (What safety does not claim). Three exclusions are worth stating explicitly, because each is a property a reader may expect CommitAgreement to carry and it does not.

UniqueChain

Theorem (The committed chain is unique). For each chain there is at most one sequence of committed blocks: the committed blocks at heights 0, 1, 2, … form a single hash-linked list, and any two correct validators’ block_hashes agree wherever both are defined. In particular the committed prefixes observed by correct validators are always compatible — one is a prefix of the other.

UnlockingJustification

Lemma (Unlocking justification). Let a correct validator cast a validation vote for B in round s, and let (A, p) be its stored confirmation vote immediately before, with A ≠ B. Then a valid ValidatedBlockCertificate for B exists in some round t with p < t < s.