Trait UnlockingJustification 

pub trait UnlockingJustification: UnlockingRequiresHigherCertificate + FastRetryPreservesBlock { }

Lemma (Unlocking justification). Let a correct validator cast a validation vote for B in round s, and let (A, p) be its stored confirmation vote immediately before, with A ≠ B. Then a valid ValidatedBlockCertificate for B exists in some round t with p < t < s.

Proof. By UnlockingRequiresHigherCertificate, with a stored confirmation vote present the proposal must carry an OriginalProposal, and:

• a fresh proposal (None) is rejected;
• a fast retry requires A to match B’s proposal, which by FastRetryPreservesBlock forces A = B, contradicting the hypothesis;
• a regular retry carries a certificate c which — by the caller’s certificate.check(& committee) and BlockProposal::check_invariants — is a valid ValidatedBlockCertificate for exactly B, with c.round < s; and since A does not match B, the accepted branch is vote.round < certificate.round, i.e. p < c.round.

Take t = c.round. ∎

This is the hinge of LockPreservation: a correct validator abandons a block it confirmed only in exchange for a quorum that validated the replacement strictly above its own confirmation — which lets the induction step down into a strictly smaller round.

Implementors