Module progress 

Progress lemmas: the individual steps a correct driver can force after GST.

Each result here says that one step of the protocol completes, given that the previous ones did. They are assembled into the liveness theorems in super::liveness.

The driver is ChainClient::process_pending_block, whose body (process_pending_block_inner) performs, in order: request a timeout if the round has expired (TimeoutCertificateForms, RoundAdvancement); finalize a locking block already in the current round; otherwise choose a block — the locking block if there is one (LockRecovery) — and a round (EventuallyCorrectLeader); submit the proposal (ProposalAccepted, ValidationQuorumForms); and finalize it (FinalizationQuorumForms).

Traits

EventuallyCorrectLeader

Lemma (Eventually a correct owner leads a round that starts after GST). Under ActiveCorrectDriver, LeaderFairness and RoundAdvancement, there are infinitely many SingleLeader rounds after GST whose leader is the correct driver’s owner.

FinalizationQuorumForms

Lemma (The finalization quorum forms). Given a valid ValidatedBlockCertificate for block B in round r, and every correct validator in round r after GST, the driver obtains a valid ConfirmedBlockCertificate for B within 2Δ plus local processing — so B becomes a CommittedBlock.

LockRecovery

Lemma (Lock recovery). Under FullReachability, after a correct driver completes ChainClient::synchronize_chain_state its local ChainManagerInfo::requested_locking has a round at least as high as the confirmed_vote round of every correct validator — and, if any correct validator holds a lock at all, is a ValidatedBlockCertificate for the same block that the highest such validator locked.

ProposalAccepted

Lemma (A recovered proposal is accepted). Let r be a SingleLeader or Validator round beginning after GST whose leader is the correct driver’s owner (EventuallyCorrectLeader), let every correct validator be in round r (RoundAdvancement), and let the driver have completed lock recovery (LockRecovery). Then the proposal the driver submits in round r passes ChainManager::check_proposed_block at every correct validator.

RoundAdvancement

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.

TimeoutCertificateForms

Lemma (A timeout certificate forms). Suppose that after GST every correct validator is in the same round r at the chain’s pending height, that r has a configured timeout (RoundsWithoutTimeout), and that the timeout has elapsed on every correct validator’s clock. Then a correct driver’s ChainClient::request_leader_timeout returns a valid TimeoutCertificate for round r within 2Δ plus local processing.

ValidationQuorumForms

Lemma (The validation quorum forms). Under the hypotheses of ProposalAccepted, the driver obtains a valid ValidatedBlockCertificate for its block in round r within 2Δ plus local processing.