Trait DoubleValidationCompleteness 

pub trait DoubleValidationCompleteness:
    Intersection
    + CertificateEmbedsQuorum
    + CertificateSignaturesVerify
    + ThresholdArithmetic { }

Lemma (Two validated blocks in one round convict a validity threshold). If two valid ValidatedBlockCertificates for conflicting blocks are certified in the same round and are valid for the same committee, extract_double_validations returns accepted DoubleVote proofs naming validators of total weight at least Committee::validity_threshold.

Proof. By CertificateEmbedsQuorum both signature sets are quorums; by Intersection their intersection has weight at least f⁺; double_vote emits a proof for each member, with kind = Validated and the round both share. Each is accepted: the blocks differ, the chain and height agree, and by CertificateSignaturesVerify the extracted signatures verify individually. ∎

This is the accountability counterpart of UniqueValidatedBlockPerRound: that lemma says the situation cannot arise below the fault bound, this one says it is attributable if it does. Note the round equality is required — validating conflicting blocks in different rounds is legitimate, which is exactly what locks exist to regulate.

Implementors