Trait TimeoutCertificateForms 

pub trait TimeoutCertificateForms:
    TimeoutVoteConditions
    + RoundsWithoutTimeout
    + CorrectValidatorsFormQuorum
    + CorrectValidatorAvailability
    + EventualSynchrony
    + ClockAccuracy { }

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.

Proof. ChainClient::request_leader_timeout issues CommunicateAction::RequestTimeout { chain_id, height, round } with round read from its local ChainManagerInfo::current_round and height from ChainInfo::next_block_height, through Client::communicate_chain_action. Each recipient runs ChainWorkerState::vote_for_leader_timeout, which checks the height against ChainTipState::next_block_height and calls ChainManager::create_timeout_vote. By TimeoutVoteConditions its four conditions hold under the hypotheses, so every correct validator signs; by CorrectValidatorAvailability and EventualSynchrony every such vote arrives within Δ of the request.

The votes aggregate: communicate_with_quorum groups by the full signed payload (value_hash, round, unlocking_round, first_round, justification_commitment), and every timeout vote for this height carries the same Timeout::new(chain_id, height, epoch) value — identical by ClockAccuracy-independent construction, since the epoch is the chain’s — with unlocking_round: None, first_round: false and no justification commitment. So all correct votes land in one group, which by CorrectValidatorsFormQuorum reaches quorum_threshold, and communicate_with_quorum returns it. ∎

The hypothesis “every correct validator is in round r” is not free — see RoundAdvancement, which is what establishes it for the next round.

Implementors