Trait RoundProgress 

pub trait RoundProgress:
    EventuallyCorrectLeader
    + LockRecovery
    + ProposalAccepted
    + ValidationQuorumForms
    + FinalizationQuorumForms
    + TimeoutCertificateForms
    + CommittedBlock { }

Theorem (Round progress). Consider a chain with at least one regular owner, at a height whose consensus instance has not yet committed. Under ActiveCorrectDriver and the other assumptions of super::assumptions, there is a round r beginning after GST such that the height commits during r.

Proof. By RoundAdvancement the correct validators’ common round grows without bound after GST, and by RoundTimeoutGrowth the timeout of round number n is base_timeout + timeout_increment · n, unbounded in n. Let T be the wall-clock time a correct leader needs to complete one round after GST: by ProposalAccepted, ValidationQuorumForms and FinalizationQuorumForms this is O(Δ) plus bounded local processing, hence finite. Choose n with base_timeout + timeout_increment · n > T.

By EventuallyCorrectLeader there is a SingleLeader round r with number at least n, beginning after GST, whose leader is the correct driver’s owner. By RoundAdvancement every correct validator is in r when it begins, and by LockRecovery the driver enters r holding a lock at least as high as every correct validator’s confirmation. Then:

1. by ProposalAccepted, every correct validator accepts the driver’s proposal in r;
2. by ValidationQuorumForms, a ValidatedBlockCertificate for the proposed block forms in round r;
3. by FinalizationQuorumForms, a ConfirmedBlockCertificate for it forms in round r.

All three complete within T < the round’s timeout, so no correct validator signs a timeout vote for r in the meantime (TimeoutVoteConditions) and the round is not cut short. The block is therefore a CommittedBlock. ∎

Step 3’s precondition that no correct validator has left r is what the timeout comparison buys: without RoundTimeoutGrowth the round could expire mid-flight, every attempt could fail the same way, and rounds would advance forever without committing.

Implementors