def CordialMiners.ApprovesBlock {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} (L : Blocklace P Wave Slot Hash) (a b : Block P Wave Slot Hash) : Prop

Block approval: a observes b and does not observe any block conflicting with b. Observing a block is not enough to approve it if the observer also observes an equivocation against it.

Equations

• CordialMiners.ApprovesBlock L a b = (CordialMiners.Observes L a b ∧ ¬∃ c ∈ L, CordialMiners.Observes L a c ∧ CordialMiners.ConflictBlock b c)

theorem CordialMiners.bl_05_approval_observes {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} {L : Blocklace P Wave Slot Hash} {a b : Block P Wave Slot Hash} (h : ApprovesBlock L a b) : Observes L a b

BL-05: approval implies observation.

theorem CordialMiners.bl_05_approval_excludes_conflict {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} {L : Blocklace P Wave Slot Hash} {a b c : Block P Wave Slot Hash} (h : ApprovesBlock L a b) (hc : c ∈ L) (hconf : ConflictBlock b c) : ¬Observes L a c

BL-05: an approver of b does not observe any block conflicting with b.

structure CordialMiners.EquivEvidence (P : Type u_5) (Wave : Type u_6) (Slot : Type u_7) (Hash : Type u_8) : Type (max (max (max u_5 u_6) u_7) u_8)

Equivocation evidence: two conflicting blocks attributed to one participant.

• participant : P
• block1 : Block P Wave Slot Hash
• block2 : Block P Wave Slot Hash

def CordialMiners.ValidEquivEvidence {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} (L : Blocklace P Wave Slot Hash) (e : EquivEvidence P Wave Slot Hash) : Prop

Validity of equivocation evidence relative to a blocklace: both blocks present, both by the named participant, and conflicting.

Equations

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

def CordialMiners.mkEquivEvidence {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} (b c : Block P Wave Slot Hash) : EquivEvidence P Wave Slot Hash

Construct equivocation evidence from two conflicting blocks (canonical participant = creator).

Equations

• CordialMiners.mkEquivEvidence b c = { participant := b.creator, block1 := b, block2 := c }

theorem CordialMiners.bl_06_equiv_sound {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} {L : Blocklace P Wave Slot Hash} {b c : Block P Wave Slot Hash} (hb : b ∈ L) (hc : c ∈ L) (hconf : ConflictBlock b c) : ValidEquivEvidence L (mkEquivEvidence b c)

BL-06 (equivocation evidence soundness): evidence built from two in-blocklace conflicting blocks by the same creator is valid.