Trait UniqueChain 

pub trait UniqueChain:
    CommitAgreement
    + EpochAgreement
    + DeterministicExecution
    + TipAdvancesOnlyOnValidCertificate { }

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.

Proof. Induction on the height h.

At each height, CommitAgreement gives uniqueness of the committed block, provided EpochAgreement holds there. That proviso is what the induction supplies: the chain’s epoch and committee at height h are functions of the execution state after height h − 1, which by the induction hypothesis (uniqueness below h) and DeterministicExecution is unique. The base case h = 0 is the genesis configuration, which is agreed by construction. Applying CommitAgreement at h closes the step.

Linkage: by TipAdvancesOnlyOnValidCertificate a correct validator records a hash at h only for a certified block, and ChainTipState::verify_block_chaining requires a proposal’s previous_block_hash to equal the tip’s hash, so the unique committed block at h has the unique committed block at h − 1 as its parent. ∎

This is the point where the specification’s per-instance scoping (ConsensusInstance) is discharged: each consensus instance decides one height, and the heights compose into a chain.

Implementors