inductive CordialMiners.TfineFact (P : Type u_1) (Wave : Type u_2) (Hash : Type u_3) : Type (max (max u_1 u_2) u_3)

A fine protocol fact: the coarse facts plus the operational evidence. An approval, certificate, and final each carry the signer set S that the coarse theory abstracts away.

• propose {P : Type u_1} {Wave : Type u_2} {Hash : Type u_3} (w : Wave) (h : Hash) : TfineFact P Wave Hash
• qApprove {P : Type u_1} {Wave : Type u_2} {Hash : Type u_3} (w : Wave) (h : Hash) (signers : Finset P) : TfineFact P Wave Hash
• certThresh {P : Type u_1} {Wave : Type u_2} {Hash : Type u_3} (w : Wave) (h : Hash) (signers : Finset P) : TfineFact P Wave Hash
• final {P : Type u_1} {Wave : Type u_2} {Hash : Type u_3} (w : Wave) (h : Hash) (signers : Finset P) : TfineFact P Wave Hash
• finalLeader {P : Type u_1} {Wave : Type u_2} {Hash : Type u_3} (w : Wave) (h : Hash) : TfineFact P Wave Hash
• orderedPrefix {P : Type u_1} {Wave : Type u_2} {Hash : Type u_3} (hs : List Hash) : TfineFact P Wave Hash

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

Equations

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

@[implicit_reducible]

instance CordialMiners.instDecidableEqTfineFact {P✝ : Type u_1} {Wave✝ : Type u_2} {Hash✝ : Type u_3} [DecidableEq P✝] [DecidableEq Wave✝] [DecidableEq Hash✝] : DecidableEq (TfineFact P✝ Wave✝ Hash✝)

Equations

• CordialMiners.instDecidableEqTfineFact = CordialMiners.instDecidableEqTfineFact.decEq

def CordialMiners.alphaFact {P : Type u_1} {Wave : Type u_2} {Hash : Type u_3} : TfineFact P Wave Hash → TrecFact Wave Hash

The abstraction on facts: forget the signer-set evidence, keep the coarse shape.

Equations

• CordialMiners.alphaFact (CordialMiners.TfineFact.propose w h) = CordialMiners.TrecFact.propose w h
• CordialMiners.alphaFact (CordialMiners.TfineFact.qApprove w h signers) = CordialMiners.TrecFact.qApprove w h
• CordialMiners.alphaFact (CordialMiners.TfineFact.certThresh w h signers) = CordialMiners.TrecFact.certThresh w h
• CordialMiners.alphaFact (CordialMiners.TfineFact.final w h signers) = CordialMiners.TrecFact.final w h
• CordialMiners.alphaFact (CordialMiners.TfineFact.finalLeader w h) = CordialMiners.TrecFact.finalLeader w h
• CordialMiners.alphaFact (CordialMiners.TfineFact.orderedPrefix hs) = CordialMiners.TrecFact.orderedPrefix hs

@[reducible, inline]

abbrev CordialMiners.TfineState (P : Type u_1) (Wave : Type u_2) (Hash : Type u_3) : Type (max (max u_3 u_2) u_1)

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

Equations

• CordialMiners.TfineState P Wave Hash = Finset (CordialMiners.TfineFact P Wave Hash)

def CordialMiners.alpha {P : Type u_1} {Wave : Type u_2} {Hash : Type u_3} [DecidableEq Wave] [DecidableEq Hash] (s : TfineState P Wave Hash) : TrecState Wave Hash

The abstraction on states: take the image of every fine fact under alphaFact.

Equations

• CordialMiners.alpha s = Finset.image CordialMiners.alphaFact s

theorem CordialMiners.alpha_empty {P : Type u_1} {Wave : Type u_2} {Hash : Type u_3} [DecidableEq Wave] [DecidableEq Hash] : alpha ∅ = ∅

The abstraction of the empty fine state is the empty coarse state.

theorem CordialMiners.alpha_insert {P : Type u_1} {Wave : Type u_2} {Hash : Type u_3} [DecidableEq P] [DecidableEq Wave] [DecidableEq Hash] (f : TfineFact P Wave Hash) (s : TfineState P Wave Hash) : alpha (insert f s) = insert (alphaFact f) (alpha s)

The abstraction commutes with insertion: abstracting a state with one more fact is the abstract state with that fact's coarse shadow inserted.

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

The fine step relation mirrors the coarse one but threads the signer-set evidence: an approval, certificate, or final records the witnessing signers S.

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

theorem CordialMiners.tfine_refines_trec {P : Type u_1} {Wave : Type u_2} {Hash : Type u_3} [DecidableEq P] [DecidableEq Wave] [DecidableEq Hash] {s s' : TfineState P Wave Hash} (h : s.Step s') : (alpha s).Step (alpha s') ∨ alpha s = alpha s'

Forward simulation (the refinement): every fine step is matched by a coarse step on the abstracted states, or it leaves the abstraction unchanged (when the fact's coarse shadow was already present, e.g. a second certificate for the same value with different signers). The coarse precondition is always met because the fine precondition's coarse shadow lies in the abstracted state.

theorem CordialMiners.alpha_reachable {P : Type u_1} {Wave : Type u_2} {Hash : Type u_3} [DecidableEq P] [DecidableEq Wave] [DecidableEq Hash] {s : TfineState P Wave Hash} (h : Relation.ReflTransGen TfineState.Step ∅ s) : Relation.ReflTransGen TrecState.Step ∅ (alpha s)

Reachability transfers along the abstraction: the abstraction of any fine-reachable state is coarse-reachable. Steps that change the abstraction become coarse steps; steps that do not are absorbed (the abstract state stays put).

theorem CordialMiners.tfine_reachable_wf {P : Type u_1} {Wave : Type u_2} {Hash : Type u_3} [DecidableEq P] [DecidableEq Wave] [DecidableEq Hash] {s : TfineState P Wave Hash} (h : Relation.ReflTransGen TfineState.Step ∅ s) : TrecWF (alpha s)

The coarse causal well-formedness lifts to the fine theory: every fine-reachable state abstracts to a causally well-formed coarse state. The proof-friendly coarse safety therefore governs the evidence-carrying operational theory.