Trait OneConfirmationVotePerRound 

pub trait OneConfirmationVotePerRound:
    ProposalGate
    + FastConfirmationNeedsEmptyLock
    + ConfirmationNeedsValidatedCertificate
    + LockRoundMonotone
    + RoundFloor
    + DurablePersistence
    + SequentialChainState { }

Lemma (One confirmation vote per round). A correct validator casts at most one confirmation vote per round of an instance.

Proof. Two cases on the round r.

r is Round::Fast. By FastConfirmationNeedsEmptyLock, such a vote requires the lock to be None beforehand and installs a LockingBlock::Fast — of round Round::Fast — afterwards. A second fast confirmation would again require the lock to be None, contradicting LockRoundMonotone. (Directly: the lock guard ensure!(locking_block.round() < Round::Fast) in ChainManager::check_proposed_block is unsatisfiable.)

r is not Round::Fast. By ConfirmationNeedsValidatedCertificate the vote comes from create_final_vote, which is guarded by ChainManager::check_validated_block (ProposalGate). That guard contains

if let Some(locking) = self.locking_block.get() {
    ensure!(new_round > locking.round(), ChainError::InsufficientRoundStrict(locking.round()));
}

The first confirmation at round r ran update_locking(LockingBlock::Regular(validated), …) with validated.round == r, so afterwards the lock round is ≥ r by RoundFloor and LockRoundMonotone. A second certificate in round r therefore fails new_round > locking.round() and no second vote is cast. (If the second certificate is for the same block and round, ChainManager::check_validated_block returns Outcome::Skip on its first branch instead.)

As in OneValidationVotePerRound, the argument consumes DurablePersistence and SequentialChainState. ∎

Where this is fragile. In the non-fast case the guard lives in ChainManager::check_validated_block, i.e. at the call site, not inside create_final_vote — which re-checks only ChainManager::current_round and would sign again for a different block certified in the same round. See ProposalGate.

Implementors