Trait InvalidJustificationSoundness 

pub trait InvalidJustificationSoundness:
    UnforgeableSignatures
    + VoteConstructionSites
    + MisbehaviourProof { }

Lemma (Attested justifications are never honestly invalid). No correct validator is named by an accepted InvalidJustification proof, when the proof is adjudicated against the committee of the vote’s own epoch (MisbehaviourProof).

Proof. An accepted proof exhibits v’s signature over a VoteValue whose justification commitment is opening.commitment(), together with an opening on which check_cited_quorum fails. By UnforgeableSignatures a correct v produced that signature, so it is one of the five sites of VoteConstructionSites. Take them in turn.

• ChainManager::create_timeout_vote, ChainManager::vote_fallback, and the fast branch of ChainManager::create_vote all sign a commitment of None. A proof requires Some(opening.commitment()), so its signature check fails and it is not accepted.
• The non-fast branch of ChainManager::create_vote, on a regular retry. It signs unlocking_round = Some(c.round) and Some(c.full_justification_commitment()), whose opening is c‘s own quorum. check_cited_quorum then asks exactly the four things that verifying c already established: that the opening’s value_hash is the voted block’s hash (given by BlockProposal::check_invariants, which binds c to the proposed block); that unlocking_round == Some(opening.round) and opening.round < round (the first by construction, the second by check_invariants’ content.round > certificate.round); that the opening’s own unlocking round and previous commitment are both present or both absent (from LiteCertificate::check, where a Validated certificate’s unlocking_round equals its chain’s top and its commitment is None exactly when the chain is empty); and that the opening’s signatures form a quorum over the reconstructed Validated payload — which is verbatim the check LiteCertificate::check performed on c, the first_round component being false for every ValidatedBlockCertificate. A fresh or fast-retry proposal signs None and is covered by the first case.
• ChainManager::create_final_vote. It signs unlocking_round = None, Some(validated.full_justification_commitment()) — or None in the chain’s first round, again covered above — in the round validated.round. For kind = Confirmed check_cited_quorum requires opening.round == round, which holds since the vote’s round is validated.round; the remaining conditions are as in the previous case, validated having been verified by the caller (ConfirmationNeedsValidatedCertificate). ∎

Implementors