Module timeouts 

Leaders, round timeouts, and how a height leaves a round it cannot finish in.

Nothing here is needed for safety — CommitAgreement holds however rounds advance, and indeed whether or not they advance at all. These results exist to be consumed by the progress lemmas in linera_core::proof::progress, and to record precisely which rounds can be left by which means. The last statement, RoundsWithoutTimeout, is a caveat rather than a guarantee, and is the main reason the liveness theorem is conditional in the way it is.

Round advancement is not autonomous. A validator never advances a round on its own initiative: it signs a timeout vote only when a client asks it to, through ChainInfoQuery::request_leader_timeout, and it never proposes a block at all. Round advancement is therefore driven entirely from linera_core::client, which is why the corresponding assumption (ActiveCorrectDriver) lives in that crate.

Traits

FallbackVote

Lemma (Fallback). ChainManager::vote_fallback signs a timeout vote in the fixed round Round::SingleLeader(u32::MAX), at most once per instance, and only while ChainManager::current_round is below Round::Validator(0). A quorum of such votes forms a TimeoutCertificate whose next_round is Round::Validator(0), moving the height into validator-led rounds.

LeaderEligibility

Lemma (Leader eligibility). In a SingleLeader or Validator round, exactly one owner may propose, namely ChainManager::round_leader(round); in a MultiLeader round any chain owner may (or anyone, when open_multi_leader_rounds); in Round::Fast only a super owner may. A super owner may additionally propose in any non-Validator round.

MultiLeaderRoundsAreLocal

Remark (In a multi-leader round, the round a validator is in is its own). Above the fast round, the protocol has two ways to leave a round, and they differ in kind rather than only in trigger. A TimeoutCertificate is quorum-signed, compact, and convinces anyone who receives it. A skipped multi-leader round leaves no artifact at all: by SingleLeaderRoundsNeedTimeout it ends when some owner proposes higher, which is a unilateral act, and by RoundsWithoutTimeout no timeout certificate for it can ever exist.

RoundsWithoutTimeout

Caveat (Rounds that never time out). ChainOwnership::round_timeout returns None — so that ChainManager::create_timeout_vote fails with ChainError::RoundDoesNotTimeOut and no timeout certificate can ever form — in three cases:

SingleLeaderRoundsNeedTimeout

Lemma (Which rounds can be skipped without a timeout). For a correct validator:

TimeoutCertificateAdvancesRound

Lemma (A timeout certificate advances the round). After a correct validator processes a valid TimeoutCertificate for round r at its pending height, its ChainManager::current_round is at least ChainOwnership::next_round(r), or Round::Validator(u32::MAX) if that is None.

TimeoutCertificateProvesRoundReached

Lemma (A timeout certificate proves a correct validator’s round expired). If a valid TimeoutCertificate is certified in round r for a chain and height, then some correct validator was in round r at that height, with a configured round timeout that had elapsed.

TimeoutVoteConditions

Lemma (Timeout vote conditions). A correct validator signs a Timeout vote in round r only if, at that moment: