Trait FirstRoundSoundness 

pub trait FirstRoundSoundness:
    UnforgeableSignatures
    + VoteConstructionSites
    + ConfirmationOnlyInCurrentRound
    + RoundFloor
    + LeaderEligibility
    + ConsensusInstance { }

Lemma (First-round attestations are never honestly contradicted). No correct validator is named by an accepted FirstRoundViolation proof.

Proof. An accepted proof exhibits v’s confirmation vote at round a carrying the attestation, and v’s confirmation vote at a round b < a on the same chain and height; by UnforgeableSignatures a correct v cast both, in the same instance.

Both sites that set the attestation — the fast branch of ChainManager::create_vote and ChainManager::create_final_vote (VoteConstructionSites) — compute it as round == self.ownership.get().first_round(). The ownership register has exactly one writer, ChainManager::reset, which by ConsensusInstance begins the instance, so first_round() is a constant φ throughout. The attestation at a therefore gives a = φ.

Now consider the vote at b < a = φ. By VoteConstructionSites it is either:

• ChainManager::create_final_vote, which by ConfirmationOnlyInCurrentRound requires current_round == b. But RoundFloor makes current_round ≥ φ = a > b at all times. Contradiction.
• the fast branch, so b = Round::Fast. Since φ > b, φ is not Round::Fast, which by ChainOwnership::first_round means super_owners is empty. But a fast-round proposal is rejected with WorkerError::InvalidOwner unless its proposer is a super owner (LeaderEligibility: can_propose returns false for Round::Fast for everyone else), so v never reaches the fast branch. Contradiction. ∎

Implementors