pub trait FallbackVote: TimeoutCertificateAdvancesRound + ConsensusInstance { }Expand description
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.
Proof. The method returns false if fallback_vote is already set or
current_round >= Round::Validator(0), and otherwise signs Timeout::new(chain_id, height, epoch) at Round::SingleLeader(u32::MAX). By ChainOwnership::next_round, the successor
of SingleLeader(r) is SingleLeader(r + 1) unless that overflows, and it does at
u32::MAX, so the successor is Round::Validator(0); combine with
TimeoutCertificateAdvancesRound. ∎
Note what is not checked here, unlike TimeoutVoteConditions: there is no
round_timeout comparison. The precondition is external — ChainWorkerState:: vote_for_fallback only calls it after reading the admin chain’s epoch event and confirming
that fallback_duration has elapsed since the next epoch was created. The method’s own
documentation states this obligation.