Trait FastConfirmationNeedsEmptyLock 

pub trait FastConfirmationNeedsEmptyLock:
    VoteConstructionSites
    + ProposalGate
    + UnlockingRequiresHigherCertificate { }

Lemma (A fast confirmation requires an empty lock and no prior vote). If a correct validator casts a confirmation vote in Round::Fast, then immediately before that vote its locking_block, validated_vote and confirmed_vote were all None; and immediately after, locking_block holds a LockingBlock::Fast for the very block confirmed.

Proof. By VoteConstructionSites such a vote comes from the if round.is_fast() branch of ChainManager::create_vote, so the proposal’s round is Round::Fast. By ProposalGate, ChainManager::check_proposed_block returned Accept for it. Since Round::Fast is the minimum of the round order (RoundOrder):

• the locking_block guard ensure!(locking_block.round() < new_round) is unsatisfiable for new_round == Round::Fast, so locking_block was None;
• the validated_vote guard ensure!(new_round > vote.round) is likewise unsatisfiable, so validated_vote was None;
• for confirmed_vote, BlockProposal::check_invariants forces a fast-round proposal to have original_proposal == None — a Fast original requires content.round > Round::Fast and a Regular original requires content.round > certificate.round ≥ Round::Fast — so the ensure! of UnlockingRequiresHigherCertificate takes the None => false arm and would reject. Hence confirmed_vote was None.

For the post-state: with original_proposal == None and round.is_fast(), the third arm of the match in ChainManager::create_vote runs update_locking(LockingBlock::Fast( proposal.clone()), …) under self.locking_block.get().is_none(), which we just established, so the lock is installed on the proposal being confirmed. ∎

Implementors