Trait DoubleVoteSoundness 

pub trait DoubleVoteSoundness:
    UnforgeableSignatures
    + OneValidationVotePerRound
    + OneConfirmationVotePerRound
    + ConsensusInstance
    + SafetyStateRecovery { }

Lemma (Double votes are never honest). No correct validator is named by an accepted DoubleVote proof.

Proof. An accepted proof exhibits two signatures by v over VoteValues that agree on round and kind, whose headers share a chain and height, and whose hashes differ; by UnforgeableSignatures only v could have produced them, so a correct v cast both votes. Sharing a chain and height means both votes belong to the same ConsensusInstance — a reset changes the height, and SafetyStateRecovery shows the one path that recreates an instance at an unchanged height preserves the votes rather than forgetting them. Then:

• kind = Validated contradicts OneValidationVotePerRound;
• kind = Confirmed contradicts OneConfirmationVotePerRound;
• kind = Timeout is not realizable at all: the proof carries BlockHeaders and checks the signature over CryptoHash::new(header), whereas a timeout vote signs the hash of a Timeout value, so an accepted timeout-kind proof would require a block header colliding with a Timeout — excluded by UnforgeableSignatures. ∎

Implementors