Trait ProposalAccepted 

pub trait ProposalAccepted:
    EventuallyCorrectLeader
    + RoundAdvancement
    + LockRecovery
    + ProposalGate
    + UnlockingRequiresHigherCertificate
    + LeaderEligibility { }

Lemma (A recovered proposal is accepted). Let r be a SingleLeader or Validator round beginning after GST whose leader is the correct driver’s owner (EventuallyCorrectLeader), let every correct validator be in round r (RoundAdvancement), and let the driver have completed lock recovery (LockRecovery). Then the proposal the driver submits in round r passes ChainManager::check_proposed_block at every correct validator.

Proof. By ProposalGate acceptance is exactly check_proposed_block returning Accept, so we take its guards in order, for a correct validator v in round r.

• Proposer eligibility. try_handle_block_proposal requires chain.manager.can_propose(&owner, r), which holds by LeaderEligibility since the driver is r’s leader; the driver selects r through ChainClient::round_for_new_proposal, which consults the same ChainManagerInfo::should_propose.
• Round. The SingleLeader(_) | Validator(_) arm requires r == v.current_round(), which is the hypothesis.
• Validation vote. Requires r > v.validated_vote.round. By VoteRoundBelowCurrentRound any earlier validation vote of v is in a round ≤ v.current_round() = r, and = r is excluded: a vote in round r needs a proposal in round r accepted by v, and by LeaderEligibility the only proposer v accepts in r is the driver, which has made no other proposal in r.
• Lock. Requires r > v.locking_block.round(). A lock round above r would by RoundFloor put v.current_round() above r, contradicting the hypothesis; and a lock round equal to r would require a ValidatedBlockCertificate in round r, which by CertificateCarriesCorrectVote would require a correct validator’s validation vote in round r — excluded by the previous point.
• Confirmed vote. This is the one that needs LockRecovery. If v has a confirmed vote in round p, then by LockRecovery the driver’s recovered lock has round t ≥ p and certifies the same block B that v confirmed if t = p. The driver proposes B as a Regular retry carrying that certificate (process_pending_block_inner takes the if let Some(locking) = info.manager.requested_locking branch and builds BlockProposal::new_retry_regular). By UnlockingRequiresHigherCertificate the guard then requires p ≤ t when the blocks match, which holds. (When t > p and the blocks differ, the guard requires p < t, which also holds.)

A LockingBlock::Fast lock is retried as BlockProposal::new_retry_fast, and the same guard requires v.confirmed_vote.round.is_fast() and a matching block, which holds because a fast confirmation is the only confirmation possible below the fast round’s successor. ∎

Implementors