Skip to main content

ConfirmationOnlyInCurrentRound

Trait ConfirmationOnlyInCurrentRound 

Source
pub trait ConfirmationOnlyInCurrentRound: VoteConstructionSites + RoundFloor { }
Expand description

Lemma (A non-fast confirmation happens only in the current round). When ChainManager::create_final_vote casts a confirmation vote in round r, ChainManager::current_round equals r at that moment — and it had already been raised to at least r earlier in the same call.

Proof. ChainManager::create_final_vote executes, in order: update_locking(LockingBlock::Regular(validated), blobs), which by RoundFloor leaves the lock at a round ≥ r; then update_current_round(local_time), which by the same result leaves ChainManager::current_round at least the lock’s round, hence ≥ r; then

if self.current_round() != round { return Ok(()); }

so the vote is cast only when the two are equal. ∎

This ordering is what makes the guard safe against a stale current_round: the lock is folded back into the round before the comparison, so a manager whose round register was reset below its lock cannot be induced to confirm in the lower round. SafetyStateRecovery uses this.

Implementors§