Causal well-formedness: each derived fact has its immediate precondition fact present. This is the invariant the coarse step relation maintains, stated as a property of a single state.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CordialMiners.trec_reachable_wf
{Wave : Type u_1}
{Hash : Type u_2}
[DecidableEq Wave]
[DecidableEq Hash]
{s : TrecState Wave Hash}
(hreach : Relation.ReflTransGen TrecState.Step ∅ s)
:
TrecWF s
Every state reachable from the empty state by coarse steps is causally well-formed. The empty state is vacuously well-formed; each step adds one fact whose precondition it required, and monotonicity keeps every earlier precondition in place.
theorem
CordialMiners.trec_final_needs_propose
{Wave : Type u_1}
{Hash : Type u_2}
[DecidableEq Wave]
[DecidableEq Hash]
{s : TrecState Wave Hash}
(hreach : Relation.ReflTransGen TrecState.Step ∅ s)
{w : Wave}
{h : Hash}
(hfin : TrecFact.final w h ∈ s)
:
The full causal chain: in any reachable coarse state, a final fact is backed by the proposal it
descends from. Two correct miners that both see final w h therefore agree it began as the same
proposal, which is the coarse mirror of threshold-finality safety.