Module proof 

Accountability: convicting the validators responsible when agreement fails.

CommitAgreement holds only while MaxByzantineWeight does. This module proves what happens when it does not: a violation leaves self-contained evidence naming validators of at least Committee::validity_threshold weight — more than the fault bound permits, so the conviction set is itself a proof that the assumption was broken.

Two properties, deliberately independent:

• Soundness (ProofSoundness) — a proof that EquivocationProof::check accepts names a genuinely faulty validator. No correct validator is ever convictable.
• Completeness (ConflictCompleteness) — two conflicting confirmed certificates yield enough accepted proofs, from the certificates alone.

Neither depends on MaxByzantineWeight, which is the point: both must hold precisely in the regime where the fault bound has failed. Soundness is per-validator and rests only on UnforgeableSignatures; completeness needs only Intersection, which in turn needs only ThresholdArithmetic. Accountability therefore sits on a strictly weaker assumption base than the safety theorem it backstops.

Traits

AccountabilityScope

Remark (What accountability does not cover). Four exclusions, the third being the substantive one.

AccountableSafety

Theorem (Accountable safety). For every chain and height, one of the following holds:

ChainAuditability

Lemma (An unsound chain convicts its attesters). If a confirmed certificate’s chain is not sound (SoundChain), audit_confirmation returns a non-empty list of proofs that EquivocationProof::check accepts.

ChainTilesRounds

Lemma (A sound chain tiles every round below the confirmation). Let a valid ConfirmedBlockCertificate in round s carry a non-empty chain with link rounds ρ₀ < ρ₁ < … < ρₖ. Then ρₖ = s, link i was cast under unlocking round ρᵢ₋₁ (and link 0 under None), and the half-open windows

ConflictCompleteness

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.

DoubleValidationCompleteness

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.

DoubleVoteSoundness

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

FirstRoundSoundness

Lemma (First-round attestations are never honestly contradicted). No correct validator is named by an accepted FirstRoundViolation proof.

InvalidJustificationSoundness

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).

LockViolationSoundness

Lemma (Lock violations are never honest). No correct validator is named by an accepted LockViolation proof — subject to the residual obligation below.

MisbehaviourProof

Definition (Proof of misbehaviour). A proof of misbehaviour against validator v is an EquivocationProof naming v for which EquivocationProof::check returns Ok against a committee. There are four shapes, and each exhibits a pair of v’s own signatures — or, for InvalidJustification, a single signature plus the opening it commits to.

ProofSoundness

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.

SoundChain

Definition (Sound justification chain). A JustificationChain carried by a confirmed certificate for block B is sound when every link’s signatures form a quorum over the Validated payload reconstructed for that link — the payload with B’s hash, the link’s round, the previous link’s round as unlocking round, and the previous link’s commitment.