Trait AccountableSafety 

pub trait AccountableSafety:
    ProofSoundness
    + ConflictCompleteness
    + ChainAuditability
    + CommitAgreement { }

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

1. at most one block is committed there (CommitAgreement); or
2. two conflicting confirmed certificates exist, and then — from those certificates alone, with no further observation of the network — validators of total weight at least Committee::validity_threshold are convictable by proofs that EquivocationProof::check accepts, every one of them genuinely faulty (ProofSoundness); or
3. a certificate’s justification chain is unsound, and then its attesters are convictable (ChainAuditability) with no conflict required at all.

Proof. Case 1 is CommitAgreement, which holds whenever MaxByzantineWeight does. If it fails, there are conflicting confirmed certificates; if both carry sound chains, case 2 is ConflictCompleteness together with ProofSoundness, and otherwise case 3 is ChainAuditability. ∎

Case 2 convicts strictly more weight than the fault bound permits — f⁺ against a permitted f⁺ − 1 — so a conviction set is itself evidence that the assumption underpinning CommitAgreement was violated, rather than merely that some validator misbehaved.

Implementors