Trait TimeoutVoteConditions 

pub trait TimeoutVoteConditions { }

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

1. r equals its ChainManager::current_round;
2. its round_timeout is Some(t) with local_time ≥ t;
3. it has not already signed a timeout vote in round r;

and the value it signs is Timeout::new(chain_id, height, epoch) for the chain’s pending height and current epoch.

Code correspondence.

transition	ChainManager::create_timeout_vote
reads	current_round, round_timeout, timeout_vote
writes	timeout_vote
precondition	height equals ChainTipState::next_block_height, checked by the caller ChainWorkerState::vote_for_leader_timeout

Proof. Direct reading of ChainManager::create_timeout_vote: it returns Ok(false) without a key pair, then ensure!(round == self.current_round()), then let Some(round_timeout) = *self.round_timeout.get() else { return Err(RoundDoesNotTimeOut) }, then ensure!(local_time >= round_timeout), then returns Ok(false) if timeout_vote.round == round. Only after all four does it construct the vote. ∎

Implementors