structure CordialMiners.Block (P : Type u_1) (Wave : Type u_2) (Slot : Type u_3) (Hash : Type u_4) : Type (max (max (max u_1 u_2) u_3) u_4)

A signed block: its creator, wave, round, slot, parent hashes, and its own hash. A creator may produce at most one non-equivocating block per slot.

• creator : P
• wave : Wave
• round : ℕ
• slot : Slot
• parents : Finset Hash
• blockHash : Hash

def CordialMiners.instDecidableEqBlock.decEq {P✝ : Type u_1} {Wave✝ : Type u_2} {Slot✝ : Type u_3} {Hash✝ : Type u_4} [DecidableEq P✝] [DecidableEq Wave✝] [DecidableEq Slot✝] [DecidableEq Hash✝] (x✝ x✝¹ : Block P✝ Wave✝ Slot✝ Hash✝) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance CordialMiners.instDecidableEqBlock {P✝ : Type u_1} {Wave✝ : Type u_2} {Slot✝ : Type u_3} {Hash✝ : Type u_4} [DecidableEq P✝] [DecidableEq Wave✝] [DecidableEq Slot✝] [DecidableEq Hash✝] : DecidableEq (Block P✝ Wave✝ Slot✝ Hash✝)

Equations

• CordialMiners.instDecidableEqBlock = CordialMiners.instDecidableEqBlock.decEq

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

Two blocks conflict when the same creator produced them in the same slot with different hashes.

Equations

• CordialMiners.ConflictBlock b c = (b.creator = c.creator ∧ b.slot = c.slot ∧ b.blockHash ≠ c.blockHash)

theorem CordialMiners.bl_conflict_symm {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} {b c : Block P Wave Slot Hash} (h : ConflictBlock b c) : ConflictBlock c b

Conflict is symmetric.

theorem CordialMiners.bl_conflict_irrefl {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} (b : Block P Wave Slot Hash) : ¬ConflictBlock b b

Conflict is irreflexive: a block never conflicts with itself.

@[reducible, inline]

abbrev CordialMiners.Blocklace (P : Type u_5) (Wave : Type u_6) (Slot : Type u_7) (Hash : Type u_8) : Type (max (max (max u_8 u_7) u_6) u_5)

A local blocklace is a finite set of blocks.

Equations

• CordialMiners.Blocklace P Wave Slot Hash = Finset (CordialMiners.Block P Wave Slot Hash)

def CordialMiners.hashesOf {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} [DecidableEq Hash] (L : Blocklace P Wave Slot Hash) : Finset Hash

The hashes present in a blocklace.

Equations

• CordialMiners.hashesOf L = Finset.image CordialMiners.Block.blockHash L

def CordialMiners.ParentClosed {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} [DecidableEq Hash] (L : Blocklace P Wave Slot Hash) : Prop

A blocklace is parent-closed when every block's parent hashes are present in the blocklace.

Equations

• CordialMiners.ParentClosed L = ∀ b ∈ L, ∀ h ∈ b.parents, h ∈ CordialMiners.hashesOf L

theorem CordialMiners.bl_02_insert_parentClosed {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} [DecidableEq P] [DecidableEq Wave] [DecidableEq Slot] [DecidableEq Hash] {L : Blocklace P Wave Slot Hash} {b : Block P Wave Slot Hash} (hL : ParentClosed L) (hb : b.parents ⊆ hashesOf L) : ParentClosed (insert b L)

BL-02: inserting a block whose parents are already present preserves parent closure.

def CordialMiners.ParentEdge {P : Type u_1} {Wave : Type u_2} {Slot : Type u_3} {Hash : Type u_4} (L : Blocklace P Wave Slot Hash) (child parent : Block P Wave Slot Hash) : Prop

A direct parent edge: child points to parent by hash, both in the blocklace.

Equations

• CordialMiners.ParentEdge L child parent = (child ∈ L ∧ parent ∈ L ∧ parent.blockHash ∈ child.parents)

def CordialMiners.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) : Prop

Observation: a observes b by following parent pointers zero or more times.

Equations

• CordialMiners.Observes L a b = Relation.ReflTransGen (CordialMiners.ParentEdge L) a b

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

BL-03 (reflexivity): every block observes itself.

theorem CordialMiners.bl_03_observes_trans {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₁ : Observes L a b) (h₂ : Observes L b c) : Observes L a c

BL-03 (transitivity): observation composes.