pub trait ChainAuditability: SoundChain + CertificateEmbedsQuorum { }Expand description
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.
Proof. audit_confirmation walks the links upward and stops at the lowest one whose
reconstructed payload fails check_signatures. Every validator at the level immediately above
— the next link, or the confirmation quorum if the bad link is the top one — signed a payload
whose justification commitment is that link’s CommittedQuorum hash, so each receives an
InvalidJustification carrying that signature and that opening. Each is accepted:
EquivocationProof::check verifies the signature against the reconstructed payload and then
requires check_cited_quorum to fail, which it does, the opening’s signatures not forming a
quorum. ∎
Weaker than ConflictCompleteness, deliberately. The blamed set is a quorum only when
the bad link is the top one, where the accusers are the certificate’s own — verified —
confirmation quorum. Lower down, the accusers are the next link, whose own signatures the audit
has not yet reached, so they may be fewer than a quorum. Each individual proof is still
accepted, and an unsound level above is itself auditable one step further up; what is not
guaranteed is a f⁺-weight blame set from a single pass. Repairing that would mean verifying
links during certificate checking, which is the cost the attestation scheme exists to avoid.