Library Round
Copyright (c) 2018 by Swirlds, Inc.
Implemented by Karl Crary.
Require Import Nat.
Require Import Omega.
Require Import Tact.
Require Import Decide.
Require Import Majority.
Require Import Relation.
Require Import HashgraphFacts.
Require Import Sees.
We differ from the technical report by making the first round 0, instead of 1.
Also, we advance to round n+1 when an event strongly-sees an event in round n
on 2/3 of the peers. This differs from the technical report, which requires
that the strongly-seen event be a witness. The two formulations are equivalent
because you can strongly-see a round-n witness on peer a iff you can strongly-see
any round-n event on peer a. Formulating it this way allows us to untangle the
circularity between the definitions of round and witness.
Inductive round : nat -> event -> Prop :=
| round_initial {x} :
initial x
-> round 0 x
| round_nadvance {x y z m n A} :
parents y z x
-> round m y
-> round n z
-> superminority stake A every
-> (forall a w,
A a
-> creator w = a
-> stsees w x
-> exists i, i < max m n /\ round i w)
-> round (max m n) x
| round_advance {x y z m n A} :
parents y z x
-> round m y
-> round n z
-> supermajority stake A every
-> (forall a,
A a
-> exists w,
creator w = a
/\ stsees w x
/\ round (max m n) w)
-> round (S (max m n)) x
.
The definition of nonterminating only says that a hashgraph
receives events from a round >= n (for all n), but it is a consequence
(all_rounds_inhabited) that it receives events from every round.
Lemma 5.13
initial
initial
nwitness
witness
initial
nwitness
witness
initial
nwitness
witness
initial
Lemma round_defined :
forall x, exists n, round n x.
Lemma round_decide :
forall r x,
decidable (round r x).
Definition earlier (x y : event) : Prop :=
exists m n,
round m x
/\ round n y
/\ m < n.
Notation "x << y" := (earlier x y)
(at level 70, right associativity) : event_scope.
Lemma rounds_earlier :
forall x y m n,
round m x
-> round n y
-> m < n
-> x << y.
Lemma earlier_rounds :
forall x y m n,
x << y
-> round m x
-> round n y
-> m < n.
Lemma earlier_trans :
forall x y z,
x << y
-> y << z
-> x << z.
Definition witness (x : event) : Prop :=
initial x
\/ exists y, self_parent y x /\ y << x.
Lemma strict_self_ancestor_witness :
forall x y m n,
witness y
-> x $ y
-> round m x
-> round n y
-> m < n.
Lemma witness_decide :
forall x, decidable (witness x).
Definition rwitness (n : nat) (x : event) : Prop :=
round n x /\ witness x.
Lemma rwitness_witness :
forall n x,
rwitness n x
-> witness x.
Lemma rwitness_fun :
forall x m n,
rwitness m x
-> rwitness n x
-> m = n.
Lemma rwitness_earlier :
forall x y m n,
rwitness m x
-> rwitness n y
-> m < n
-> x << y.
Lemma rwitness_decide :
forall r x,
decidable (rwitness r x).
forall x, exists n, round n x.
Lemma round_decide :
forall r x,
decidable (round r x).
Definition earlier (x y : event) : Prop :=
exists m n,
round m x
/\ round n y
/\ m < n.
Notation "x << y" := (earlier x y)
(at level 70, right associativity) : event_scope.
Lemma rounds_earlier :
forall x y m n,
round m x
-> round n y
-> m < n
-> x << y.
Lemma earlier_rounds :
forall x y m n,
x << y
-> round m x
-> round n y
-> m < n.
Lemma earlier_trans :
forall x y z,
x << y
-> y << z
-> x << z.
Definition witness (x : event) : Prop :=
initial x
\/ exists y, self_parent y x /\ y << x.
Lemma strict_self_ancestor_witness :
forall x y m n,
witness y
-> x $ y
-> round m x
-> round n y
-> m < n.
Lemma witness_decide :
forall x, decidable (witness x).
Definition rwitness (n : nat) (x : event) : Prop :=
round n x /\ witness x.
Lemma rwitness_witness :
forall n x,
rwitness n x
-> witness x.
Lemma rwitness_fun :
forall x m n,
rwitness m x
-> rwitness n x
-> m = n.
Lemma rwitness_earlier :
forall x y m n,
rwitness m x
-> rwitness n y
-> m < n
-> x << y.
Lemma rwitness_decide :
forall r x,
decidable (rwitness r x).
Key corollary of the strongly-seeing lemma.
Lemma stseen_witness_unique :
forall W n x y z z',
member W z
-> member W z'
-> creator x = creator y
-> rwitness n x
-> rwitness n y
-> stsees x z
-> stsees y z'
-> x = y.
Lemma self_ancestor_witness :
forall n x,
round n x
-> exists y,
y $= x
/\ rwitness n y.
forall W n x y z z',
member W z
-> member W z'
-> creator x = creator y
-> rwitness n x
-> rwitness n y
-> stsees x z
-> stsees y z'
-> x = y.
Lemma self_ancestor_witness :
forall n x,
round n x
-> exists y,
y $= x
/\ rwitness n y.
initial
Lemma stsees_many_witnesses :
forall n x,
round (S n) x
-> supermajority
stake
(fun a =>
exists w,
creator w = a
/\ stsees w x
/\ rwitness n w)
every.
forall n x,
round (S n) x
-> supermajority
stake
(fun a =>
exists w,
creator w = a
/\ stsees w x
/\ rwitness n w)
every.
nwitness
succ
initial
nadvance
advance