inductive CordialMiners.TrecFact (Wave : Type u_1) (Hash : Type u_2) : Type (max u_1 u_2)

A coarse protocol fact (the language of T_rec). Evidence-free: a certThresh fact records that a threshold certificate exists, not the signers or signatures.

• propose {Wave : Type u_1} {Hash : Type u_2} (w : Wave) (h : Hash) : TrecFact Wave Hash
• qApprove {Wave : Type u_1} {Hash : Type u_2} (w : Wave) (h : Hash) : TrecFact Wave Hash
• certThresh {Wave : Type u_1} {Hash : Type u_2} (w : Wave) (h : Hash) : TrecFact Wave Hash
• final {Wave : Type u_1} {Hash : Type u_2} (w : Wave) (h : Hash) : TrecFact Wave Hash
• finalLeader {Wave : Type u_1} {Hash : Type u_2} (w : Wave) (h : Hash) : TrecFact Wave Hash
• orderedPrefix {Wave : Type u_1} {Hash : Type u_2} (hs : List Hash) : TrecFact Wave Hash

@[implicit_reducible]

instance CordialMiners.instDecidableEqTrecFact {Wave✝ : Type u_1} {Hash✝ : Type u_2} [DecidableEq Wave✝] [DecidableEq Hash✝] : DecidableEq (TrecFact Wave✝ Hash✝)

Equations

• CordialMiners.instDecidableEqTrecFact = CordialMiners.instDecidableEqTrecFact.decEq

def CordialMiners.instDecidableEqTrecFact.decEq {Wave✝ : Type u_1} {Hash✝ : Type u_2} [DecidableEq Wave✝] [DecidableEq Hash✝] (x✝ x✝¹ : TrecFact Wave✝ Hash✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• CordialMiners.instDecidableEqTrecFact.decEq (CordialMiners.TrecFact.propose w h) (CordialMiners.TrecFact.qApprove w_1 h_1) = isFalse ⋯
• CordialMiners.instDecidableEqTrecFact.decEq (CordialMiners.TrecFact.propose w h) (CordialMiners.TrecFact.certThresh w_1 h_1) = isFalse ⋯
• CordialMiners.instDecidableEqTrecFact.decEq (CordialMiners.TrecFact.propose w h) (CordialMiners.TrecFact.final w_1 h_1) = isFalse ⋯
• CordialMiners.instDecidableEqTrecFact.decEq (CordialMiners.TrecFact.propose w h) (CordialMiners.TrecFact.finalLeader w_1 h_1) = isFalse ⋯
• CordialMiners.instDecidableEqTrecFact.decEq (CordialMiners.TrecFact.propose w h) (CordialMiners.TrecFact.orderedPrefix hs) = isFalse ⋯
• CordialMiners.instDecidableEqTrecFact.decEq (CordialMiners.TrecFact.qApprove w h) (CordialMiners.TrecFact.propose w_1 h_1) = isFalse ⋯
• CordialMiners.instDecidableEqTrecFact.decEq (CordialMiners.TrecFact.qApprove w h) (CordialMiners.TrecFact.certThresh w_1 h_1) = isFalse ⋯
• CordialMiners.instDecidableEqTrecFact.decEq (CordialMiners.TrecFact.qApprove w h) (CordialMiners.TrecFact.final w_1 h_1) = isFalse ⋯
• CordialMiners.instDecidableEqTrecFact.decEq (CordialMiners.TrecFact.qApprove w h) (CordialMiners.TrecFact.finalLeader w_1 h_1) = isFalse ⋯
• CordialMiners.instDecidableEqTrecFact.decEq (CordialMiners.TrecFact.qApprove w h) (CordialMiners.TrecFact.orderedPrefix hs) = isFalse ⋯
• CordialMiners.instDecidableEqTrecFact.decEq (CordialMiners.TrecFact.certThresh w h) (CordialMiners.TrecFact.propose w_1 h_1) = isFalse ⋯
• CordialMiners.instDecidableEqTrecFact.decEq (CordialMiners.TrecFact.certThresh w h) (CordialMiners.TrecFact.qApprove w_1 h_1) = isFalse ⋯
• CordialMiners.instDecidableEqTrecFact.decEq (CordialMiners.TrecFact.certThresh w h) (CordialMiners.TrecFact.final w_1 h_1) = isFalse ⋯
• CordialMiners.instDecidableEqTrecFact.decEq (CordialMiners.TrecFact.certThresh w h) (CordialMiners.TrecFact.finalLeader w_1 h_1) = isFalse ⋯
• CordialMiners.instDecidableEqTrecFact.decEq (CordialMiners.TrecFact.certThresh w h) (CordialMiners.TrecFact.orderedPrefix hs) = isFalse ⋯
• CordialMiners.instDecidableEqTrecFact.decEq (CordialMiners.TrecFact.final w h) (CordialMiners.TrecFact.propose w_1 h_1) = isFalse ⋯
• CordialMiners.instDecidableEqTrecFact.decEq (CordialMiners.TrecFact.final w h) (CordialMiners.TrecFact.qApprove w_1 h_1) = isFalse ⋯
• CordialMiners.instDecidableEqTrecFact.decEq (CordialMiners.TrecFact.final w h) (CordialMiners.TrecFact.certThresh w_1 h_1) = isFalse ⋯
• CordialMiners.instDecidableEqTrecFact.decEq (CordialMiners.TrecFact.final w h) (CordialMiners.TrecFact.finalLeader w_1 h_1) = isFalse ⋯
• CordialMiners.instDecidableEqTrecFact.decEq (CordialMiners.TrecFact.final w h) (CordialMiners.TrecFact.orderedPrefix hs) = isFalse ⋯
• CordialMiners.instDecidableEqTrecFact.decEq (CordialMiners.TrecFact.finalLeader w h) (CordialMiners.TrecFact.propose w_1 h_1) = isFalse ⋯
• CordialMiners.instDecidableEqTrecFact.decEq (CordialMiners.TrecFact.finalLeader w h) (CordialMiners.TrecFact.qApprove w_1 h_1) = isFalse ⋯
• CordialMiners.instDecidableEqTrecFact.decEq (CordialMiners.TrecFact.finalLeader w h) (CordialMiners.TrecFact.certThresh w_1 h_1) = isFalse ⋯
• CordialMiners.instDecidableEqTrecFact.decEq (CordialMiners.TrecFact.finalLeader w h) (CordialMiners.TrecFact.final w_1 h_1) = isFalse ⋯
• CordialMiners.instDecidableEqTrecFact.decEq (CordialMiners.TrecFact.finalLeader w h) (CordialMiners.TrecFact.orderedPrefix hs) = isFalse ⋯
• CordialMiners.instDecidableEqTrecFact.decEq (CordialMiners.TrecFact.orderedPrefix hs) (CordialMiners.TrecFact.propose w h) = isFalse ⋯
• CordialMiners.instDecidableEqTrecFact.decEq (CordialMiners.TrecFact.orderedPrefix hs) (CordialMiners.TrecFact.qApprove w h) = isFalse ⋯
• CordialMiners.instDecidableEqTrecFact.decEq (CordialMiners.TrecFact.orderedPrefix hs) (CordialMiners.TrecFact.certThresh w h) = isFalse ⋯
• CordialMiners.instDecidableEqTrecFact.decEq (CordialMiners.TrecFact.orderedPrefix hs) (CordialMiners.TrecFact.final w h) = isFalse ⋯
• CordialMiners.instDecidableEqTrecFact.decEq (CordialMiners.TrecFact.orderedPrefix hs) (CordialMiners.TrecFact.finalLeader w h) = isFalse ⋯
• CordialMiners.instDecidableEqTrecFact.decEq (CordialMiners.TrecFact.orderedPrefix a) (CordialMiners.TrecFact.orderedPrefix b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[reducible, inline]

abbrev CordialMiners.TrecState (Wave : Type u_3) (Hash : Type u_4) : Type (max u_4 u_3)

A coarse state is the finite set of facts established so far.

Equations

• CordialMiners.TrecState Wave Hash = Finset (CordialMiners.TrecFact Wave Hash)

inductive CordialMiners.TrecState.Step {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] : TrecState Wave Hash → TrecState Wave Hash → Prop

The coarse step relation: each conceptual transition adds the fact justified by the facts already present. Proposal is always available; the others gate on their precondition fact. The state only grows, which is what makes the coarse theory monotone and proof-friendly.

• propose {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (s : TrecState Wave Hash) (w : Wave) (h : Hash) : s.Step (insert (TrecFact.propose w h) s)
• qapprove {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (s : TrecState Wave Hash) (w : Wave) (h : Hash) : TrecFact.propose w h ∈ s → s.Step (insert (TrecFact.qApprove w h) s)
• certify {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (s : TrecState Wave Hash) (w : Wave) (h : Hash) : TrecFact.qApprove w h ∈ s → s.Step (insert (TrecFact.certThresh w h) s)
• finalize {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (s : TrecState Wave Hash) (w : Wave) (h : Hash) : TrecFact.certThresh w h ∈ s → s.Step (insert (TrecFact.final w h) s)
• finalLead {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (s : TrecState Wave Hash) (w : Wave) (h : Hash) : TrecFact.final w h ∈ s → s.Step (insert (TrecFact.finalLeader w h) s)
• order {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] (s : TrecState Wave Hash) (hs : List Hash) : s.Step (insert (TrecFact.orderedPrefix hs) s)

theorem CordialMiners.trec_step_monotone {Wave : Type u_1} {Hash : Type u_2} [DecidableEq Wave] [DecidableEq Hash] {s s' : TrecState Wave Hash} (h : s.Step s') : s ⊆ s'

The coarse state only grows: every step adds facts and removes none.