Trait ProofSoundness 

pub trait ProofSoundness:
    DoubleVoteSoundness
    + FirstRoundSoundness
    + LockViolationSoundness
    + InvalidJustificationSoundness { }

Theorem (Soundness — no correct validator is convictable). If EquivocationProof::check accepts a proof naming v against the committee of the epoch its votes were cast in, then v is faulty in the sense of CorrectValidator.

Proof. By cases on the four variants: DoubleVoteSoundness, FirstRoundSoundness, LockViolationSoundness and InvalidJustificationSoundness. ∎

Note what this does not assume: no MaxByzantineWeight, no synchrony, no bound on how many other validators misbehaved. Soundness is a statement about one validator’s own signatures, so it survives arbitrary corruption of everyone else — which is what makes a conviction meaningful in the regime where accountability is invoked. For three of the four variants it does not even depend on the committee (MisbehaviourProof); only the InvalidJustification case needs the right one.

Implementors