Trait LockRecovery 

pub trait LockRecovery:
    FullReachability
    + ConfirmationNeedsValidatedCertificate
    + ConfirmationOnlyInCurrentRound
    + LockRoundMonotone
    + UniqueValidatedBlockPerRound { }

Lemma (Lock recovery). Under FullReachability, after a correct driver completes ChainClient::synchronize_chain_state its local ChainManagerInfo::requested_locking has a round at least as high as the confirmed_vote round of every correct validator — and, if any correct validator holds a lock at all, is a ValidatedBlockCertificate for the same block that the highest such validator locked.

Proof. Two steps.

Every correct validator’s lock dominates its own confirmation. If a correct validator’s confirmed_vote is in round p, then either p is Round::Fast — and by FastConfirmationNeedsEmptyLock it then holds a LockingBlock::Fast at that same round — or by ConfirmationNeedsValidatedCertificate it confirmed via ChainManager::create_final_vote, which installs the certificate as the lock before signing (ConfirmationOnlyInCurrentRound). Either way its lock round is ≥ p, and stays so by LockRoundMonotone.

The driver collects the maximum. Client::synchronize_chain_state_from reads each validator’s ChainManagerInfo with manager values, and for a LockingBlock::Regular(cert) calls try_process_locking_block_from, which feeds the certificate to the local node’s process_validated_block; that calls ChainManager::create_final_vote, whose update_locking keeps the higher of the two by LockRoundMonotone. A LockingBlock::Fast is instead replayed as a proposal. Iterating over the validators reached — all of the correct ones, by FullReachability — leaves the local lock at the maximum. That it is a certificate for the locked block is immediate, since a lock is the certificate; and by UniqueValidatedBlockPerRound two correct validators locked at the same round hold certificates for the same block. ∎

This is what makes ProposalAccepted possible: the driver re-proposes the block it just recovered, so no correct validator’s UnlockingRequiresHigherCertificate guard can reject it.

Implementors