Library Order

Copyright (c) 2018 by Swirlds, Inc. Implemented by Karl Crary.

Require Import Nat.
Require Import Bool.
Require Import Omega.
Require Import List.
Require Import Permutation.

Require Import Tact.
Require Import Decide.
Require Import Relation.
Require Import HashgraphFacts.
Require Import Sees.
Require Import Round.
Require Import Progress.
Require Import Decision.
Require Import Consensus.
Require Import Famous.
Require Import Received.
Require Import Median.

Definition earliest_observer (x y z : event) : Prop :=
  x @= y
  /\ (forall y', self_parent y' y -> x @= y' -> False)
  /\ y $= z.

Definition time_received (s : sample) (W : world) (x : event) (t : nat) : Prop :=
  exists i l,
    received s W i x
    /\ NoDup l
    /\ (forall y,
          (exists w,
             ufwitness s W i w
             /\ earliest_observer x y w)
          <-> In y l)
    /\ t = median l.

The consensus order.
Definition corder (s : sample) (W : world) (x y : event) : Prop :=
  exists i j t u,
    received s W i x
    /\ received s W j y
    /\ time_received s W x t
    /\ time_received s W y u
    /\ (i < j
        \/ (i = j /\ t < u)
        \/ (i = j /\ t = u /\ Is_true (textorder x y))).

Lemma earliest_observer_impl_self_ancestor :
  forall x y z,
    earliest_observer x y z
    -> y $= z.

Lemma time_received_fun :
  forall s W x t u,
    time_received s W x t
    -> time_received s W x u
    -> t = u.

Lemma received_impl_time_received :
  forall s W x i,
    received s W i x
    -> finite (ufwitness s W i)
    -> exists t,
         time_received s W x t.

Lemma time_received_defined :
  forall s x,
    member (global s) x
    -> honest (creator x)
    -> exists t,
         time_received s (global s) x t.

Theorem corder_antisym :
  forall s,
    antisymmetric event (corder s (global s)).

Theorem corder_trans :
  forall s,
    transitive event (corder s (global s)).

Theorem corder_total :
  forall s x y,
    member (global s) x
    -> member (global s) y
    -> honest (creator x)
    -> honest (creator y)
    -> corder s (global s) x y \/ corder s (global s) y x.

Theorem 5.19
Corollary corder_refl :
  forall s x,
    member (global s) x
    -> honest (creator x)
    -> corder s (global s) x x.

Lemma fwitness_stable :
  forall s W W' i y,
    extends W W'
    -> (forall x, decidable (member W x))
    -> nonempty W
    -> received_by s W i y
    -> forall x, fwitness s W i x <-> fwitness s W' i x.

Lemma ufwitness_stable :
  forall s W W' i y,
    extends W W'
    -> (forall x, decidable (member W x))
    -> nonempty W
    -> received_by s W i y
    -> forall x, ufwitness s W i x <-> ufwitness s W' i x.

Lemma time_received_consistent :
  forall s W W' x t,
    extends W W'
    -> (forall x, decidable (member W x))
    -> nonempty W
    -> time_received s W x t
    -> time_received s W' x t.

A hashgraph cannot later discover new predecessors in the consensus order.
Theorem corder_stable :
  forall s W W' x y,
    extends W W'
    -> (forall x, decidable (member W x))
    -> nonempty W
    -> corder s W y y
    -> corder s W' x y
    -> corder s W x y.

A hashgraph eventually places every (honest) event into the consensus order.
Theorem corder_support :
  forall s W x,
    extends W (global s)
    -> (forall x, decidable (member W x))
    -> nonempty W
    -> (forall i, finite (ufwitness s W i))
    -> member (global s) x
    -> honest (creator x)
    -> exists j,
         (exists y, member W y /\ round j y)
         -> corder s W x x.

Corollary corder_support_finite :
  forall s W x,
    extends W (global s)
    -> finite (member W)
    -> nonempty W
    -> member (global s) x
    -> honest (creator x)
    -> exists j,
         (exists y, member W y /\ round j y)
         -> corder s W x x.