Trait LockPreservation 

pub trait LockPreservation:
    UnlockingJustification
    + CommitRestsOnValidation
    + UniqueValidatedBlockPerRound
    + NoValidatedBlockInFastRound
    + OneConfirmationVotePerRound
    + ConfirmedVoteRoundMonotone
    + CastValidationRoundFloor
    + FastConfirmationNeedsEmptyLock
    + ConfirmationNeedsValidatedCertificate
    + ConfirmationOnlyInCurrentRound
    + UnlockingRequiresHigherCertificate
    + VoteRoundBelowCurrentRound
    + CurrentRoundMonotone
    + CorrectValidatorInIntersection
    + CertificateEmbedsQuorum
    + CorrectSignerCastItsVote
    + EpochAgreement { }

Theorem (Lock preservation). Suppose a valid ConfirmedBlockCertificate for a block A is certified in round r, at some height of some chain. Then for every round s ≥ r, every valid ValidatedBlockCertificate at that height and round s certifies A.

Proof. Strong induction on s ≥ r. Assume the claim for all t with r ≤ t < s, and let C' be a valid ValidatedBlockCertificate for B in round s. By EpochAgreement the confirmed certificate and C' are judged against the same committee; by CertificateEmbedsQuorum both signer sets are quorums of it, so by CorrectValidatorInIntersection they share a correct validator v, and by CorrectSignerCastItsVote v itself cast both votes: a confirmation vote for A in round r (call it (a)) and a validation vote for B in round s (call it (b)).

Case s = r. By NoValidatedBlockInFastRound, s is not the fast round, so r is not either; by CommitRestsOnValidation a valid ValidatedBlockCertificate for A in round r exists. By UniqueValidatedBlockPerRound applied to it and C', B = A.

Case s > r. Consider the order of (a) and (b) in v’s execution.

Suppose (b) preceded (a). By VoteRoundBelowCurrentRound and CurrentRoundMonotone, from (b) onwards v’s current round is ≥ s > r. If r is not the fast round, (a) comes from ChainManager::create_final_vote, which by ConfirmationNeedsValidatedCertificate and ConfirmationOnlyInCurrentRound casts a vote only when the current round equals r — impossible. If r is the fast round, (a) comes from the fast branch of ChainManager::create_vote, which by FastConfirmationNeedsEmptyLock requires an empty lock and an absent validation vote — but CastValidationRoundFloor, established by (b), forces max(validated_vote.round, lock round) ≥ s > Round::Fast. Also impossible. So (a) preceded (b).

So (a) preceded (b). Let (A', p) be v’s stored confirmation vote immediately before (b). It is present, since (a) stored one; and by ConfirmedVoteRoundMonotone, p ≥ r.

• If A' ≠ B, then UnlockingJustification yields a valid ValidatedBlockCertificate for B in a round t with p < t < s. Then r ≤ p < t < s, so the induction hypothesis applies at t and gives B = A.
• If A' = B, then v confirmed B in round p ≥ r.
  • If p = r: v also confirmed A in round r by (a), so OneConfirmationVotePerRound gives A = B.
  • If p > r: then p is not the fast round (it exceeds r ≥ Round::Fast), so by ConfirmationNeedsValidatedCertificate a valid ValidatedBlockCertificate for B in round p existed. Moreover UnlockingRequiresHigherCertificate applied to (b) — in the branch where the stored vote’s value matches the proposed block — gives p ≤ c.round < s for the certificate c the proposal carries, hence p < s. So r < p < s, the induction hypothesis applies at p, and B = A. ∎

The induction is well founded because rounds are totally ordered and every appeal to the hypothesis is at a round strictly between r and s.

Implementors