Trait ConflictCompleteness 

pub trait ConflictCompleteness:
    ChainTilesRounds
    + SoundChain
    + Intersection
    + CertificateEmbedsQuorum
    + CertificateSignaturesVerify
    + ThresholdArithmetic { }

Theorem (Completeness — a conflict convicts a validity threshold). Let two valid ConfirmedBlockCertificates for conflicting blocks at the same chain and height, valid for the same committee and carrying sound chains (SoundChain), be certified in rounds r ≤ s. Then extract_equivocations applied to their JustifiedConfirmations returns proofs that EquivocationProof::check accepts, naming validators of total weight at least Committee::validity_threshold.

Proof. By CertificateEmbedsQuorum each certificate’s confirmation signatures form a quorum, and by ChainTilesRounds so does each link of a sound chain. Three cases, which are exactly the three the implementation tries.

• r = s. double_confirm walks the intersection of the two confirmation quorums, which by Intersection has weight at least f⁺, emitting a DoubleVote for each member. Each is accepted: the blocks differ, the chain and height agree, and by CertificateSignaturesVerify both extracted signatures verify individually — which is what EquivocationProof::check re-checks.
• r < s and the higher certificate carries a chain. By ChainTilesRounds some link’s window contains r, i.e. link.round > r and its unlocking round is ≤ r — precisely walk_chain’s guard. That link is a quorum, so its intersection with the lower confirmation quorum has weight at least f⁺ by Intersection, and each member gets a LockViolation. Each is accepted: check re-derives the same window condition confirmed_round < validated_round and validated_unlocking_round ≤ confirmed_round.
• r < s and the higher certificate carries no chain. Then LiteCertificate::check accepted it only because its first_round attestation is set. first_round_violation walks the intersection of the two confirmation quorums — weight at least f⁺ — emitting a FirstRoundViolation for each, accepted since earlier_round = r < s = attested_round.

In every case the blamed set is a full quorum intersection — which is where the weight claim comes from: its members are signers of a verified certificate, hence committee members of nonzero weight by CertificateEmbedsQuorum. EquivocationProof::check itself establishes no membership or weight (MisbehaviourProof), so a consumer tallying the threshold must read the weights from the committee. ∎

Depends on the shared-committee hypothesis. Intersection compares quorums of one committee; extract_equivocations checks only the chain and height, not the epoch, so two certificates declaring different epochs could yield no intersection at all. An auditor must establish that both certificates are valid for the same committee before drawing the conclusion.

Implementors