Trait RoundAdvancement 

pub trait RoundAdvancement:
    TimeoutCertificateForms
    + TimeoutCertificateAdvancesRound
    + CurrentRoundMonotone
    + RoundTimeoutGrowth
    + SingleLeaderRoundsNeedTimeout { }

Lemma (Round advancement). After GST, a correct driver can bring every correct validator into a common round strictly above r, within O(Δ), provided r has a configured timeout. Consequently the common round grows without bound as long as the driver keeps trying.

Proof. By TimeoutCertificateForms the driver obtains a TimeoutCertificate for r. ChainClient::request_leader_timeout then feeds it to its own node and calls Client::communicate_chain_updates, which delivers it to the validators; each correct recipient runs ChainWorkerState::process_timeout, which verifies it against the committee and calls ChainManager::handle_timeout_certificate. By TimeoutCertificateAdvancesRound each then has a current round of at least ChainOwnership::next_round(r) > r, and by CurrentRoundMonotone it stays there.

They are in a common round because RoundFloor makes the round a deterministic function of the evidence held, and after this step every correct validator holds the same highest timeout certificate — unless some hold additional evidence (a higher lock or proposal), which only moves them higher, and which the driver’s own synchronization (FullReachability) then propagates. Unboundedness follows by induction, using RoundTimeoutGrowth to know that each successive round again has a finite timeout. ∎

This is strictly weaker than liveness. It says rounds advance, not that a block is committed; an execution in which the driver forever advances rounds without ever committing satisfies this lemma. Turning it into progress is what RoundProgress does, and it needs EventuallyCorrectLeader and LockRecovery besides.

Implementors