structure CordialMiners.WCertState (P : Type u_2) : Type u_2

The collector state: the accepted signer set, the accumulated weight, and whether a certificate has been emitted.

• signers : Finset P
• accWeight : Weight
• done : Bool

def CordialMiners.WCertState.init {P : Type u_1} : WCertState P

The initial collector state.

Equations

• CordialMiners.WCertState.init = { signers := ∅, accWeight := 0, done := false }

def CordialMiners.collectorStep {P : Type u_1} [DecidableEq P] (S : CommitteeSnapshot P) (ok : P → Bool) (st : WCertState P) (p : P) : WCertState P

One collector step on an incoming approval from p, whose validity is the abstract Boolean check ok p. Reject once done, off-committee, a duplicate signer, or invalid; otherwise accept p, add its weight, and emit once the threshold is crossed. One-shot and set-canonical.

Equations

• One or more equations did not get rendered due to their size.

def CordialMiners.WCertState.Inv {P : Type u_1} (S : CommitteeSnapshot P) (st : WCertState P) : Prop

The collector invariant (CERT-02): the accumulated weight equals the weight of the accepted signer set, the signers are within the committee, and done implies the threshold was crossed.

Equations

• One or more equations did not get rendered due to their size.

theorem CordialMiners.cert_02_init_inv {P : Type u_1} (S : CommitteeSnapshot P) : WCertState.Inv S WCertState.init

CERT-02 (base): the initial state satisfies the invariant.

theorem CordialMiners.cert_04_step_inv {P : Type u_1} [DecidableEq P] (S : CommitteeSnapshot P) (ok : P → Bool) {st : WCertState P} (h : WCertState.Inv S st) (p : P) : WCertState.Inv S (collectorStep S ok st p)

CERT-04: every collector step preserves the invariant.

theorem CordialMiners.cert_03_collector_sound {P : Type u_1} (S : CommitteeSnapshot P) {st : WCertState P} (h : WCertState.Inv S st) (hd : st.done = true) : S.Heavy st.signers

CERT-03 (collector soundness): a state that has emitted holds a threshold-heavy signer set, so the emitted certificate is valid in the snapshot.