Trait CommitAgreement 

pub trait CommitAgreement:
    LockPreservation
    + CommitRestsOnValidation
    + OneConfirmationVotePerRound
    + CorrectValidatorInIntersection
    + CertificateEmbedsQuorum
    + CorrectSignerCastItsVote
    + ConflictingBlocks
    + EpochAgreement
    + TipAdvancesOnlyOnValidCertificate { }

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.

Proof. Let valid confirmed certificates for A in round r and for B in round s exist, with r ≤ s after renaming.

• If r = s: by EpochAgreement both are judged against the same committee, and by CertificateEmbedsQuorum their signer sets are quorums of it, so by CorrectValidatorInIntersection a correct validator v signed both. By CorrectSignerCastItsVote, v cast confirmation votes for A and for B in round r. By OneConfirmationVotePerRound, A = B.
• If r < s: then s is not Round::Fast, so CommitRestsOnValidation gives a valid ValidatedBlockCertificate for B in round s. By LockPreservation, applied to the commit of A in round r and to s > r, that certificate certifies A. Hence B = A. ∎

In observable terms. Combining with TipAdvancesOnlyOnValidCertificate: if any correct validator’s ChainTipState records a block hash at height h, then no correct validator ever records a different hash at h — whatever the network does, and whatever the faulty validators sign.

Implementors