Trait UnlockingRequiresHigherCertificate 

pub trait UnlockingRequiresHigherCertificate: ProposalGate { }

Lemma (A validation vote past a lock needs a higher certificate). Suppose a correct validator casts a validation vote for block B in round r, and let (A, p) be the value of its confirmed_vote immediately before. Then p is defined only if the proposal carried an OriginalProposal, and:

• if the proposal is a regular retry carrying a certificate c (necessarily a valid ValidatedBlockCertificate for B, in a round c.round < r), then p ≤ c.round when A matches B’s proposal, and p < c.round otherwise;
• if the proposal is a fast retry, then p is Round::Fast and A matches B’s proposal;
• a fresh proposal is rejected outright.

This is the hinge of the safety argument: it says a correct validator abandons a block it has confirmed only when shown a quorum that validated the new block in a round strictly above its own confirmation.

Code correspondence.

transition	ChainManager::check_proposed_block, final ensure!
reads	confirmed_vote, proposal.original_proposal
writes	nothing
precondition	the proposal passed check_invariants, check_signature and — for a regular retry — certificate.check(committee), all in try_handle_block_proposal

Proof. By ProposalGate, Accept was returned, so the final ensure! of ChainManager::check_proposed_block held. With vote = (A, p) it evaluates

match proposal.original_proposal.as_ref() {
    None => false,
    Some(OriginalProposal::Regular { certificate }) =>
        if vote.value().matches_proposed_block(new_block) {
            vote.round <= certificate.round
        } else {
            vote.round < certificate.round
        },
    Some(OriginalProposal::Fast(_)) =>
        vote.round.is_fast() && vote.value().matches_proposed_block(new_block),
}

which is the case distinction claimed. That the retried certificate is valid and certifies exactly B comes from the caller: try_handle_block_proposal calls certificate.check(&committee)? on the Regular arm, and BlockProposal::check_invariants — also called there — requires certificate.check_value(&ValidatedBlock::new(outcome.with(block))), i.e. the certificate certifies the very block being proposed, and content.round > certificate.round. ∎

Note matches_proposed_block compares the ProposedBlock only, not the execution outcome; FastRetryPreservesBlock is where that gap is closed.

Implementors