Trait UniqueValidatedBlockPerRound 

pub trait UniqueValidatedBlockPerRound:
    OneValidationVotePerRound
    + CorrectValidatorInIntersection
    + CertificateEmbedsQuorum
    + CorrectSignerCastItsVote
    + EpochAgreement { }

Lemma (At most one validated block per round). For a given chain and height, all valid ValidatedBlockCertificates certified in the same round certify the same block.

Proof. Let two such certificates certify B₁ and B₂ in round s. By EpochAgreement they are judged against the same committee, so by CertificateEmbedsQuorum their signer sets are two quorums of it, and by CorrectValidatorInIntersection some correct validator v signed both. By CorrectSignerCastItsVote, v cast validation votes for B₁ and for B₂, both in round s. By OneValidationVotePerRound, B₁ = B₂. ∎

Implementors