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.
Definition nonterminating (G : world) :=
  forall m, exists n x,
     m <= n
     /\ round n x
     /\ member G x.

Lemma 5.13
Lemma round_fun :
  forall x m n,
    round m x
    -> round n x
    -> m = n.
initial
initial
nwitness
witness
initial
nwitness
witness
initial
nwitness
witness
Lemma round_mono :
  forall x y m n,
    x @= y
    -> round m x
    -> round n y
    -> m <= n.
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).
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.
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.
nwitness
Lemma ancestor_witness :
  forall m n x,
    m <= n
    -> round n x
    -> exists y, y @= x /\ rwitness m y.
succ
initial
nadvance
advance
Lemma all_rounds_inhabited :
  forall W n,
    nonterminating W
    -> exists x, rwitness n x /\ member W x.

Lemma honest_witness_unique :
  forall W n x y,
    member W x
    -> member W y
    -> honest (creator x)
    -> creator x = creator y
    -> rwitness n x
    -> rwitness n y
    -> x = y.