Library Received

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

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

Require Import Tact.
Require Import Decide.
Require Import Relation.
Require Import HashgraphFacts.
Require Import Round.
Require Import Progress.
Require Import Decision.
Require Import Consensus.
Require Import Famous.
Require Import Fairness.

Definition ufwitness s W i x :=
  fwitness s W i x
  /\ forall y,
       fwitness s W i y
       -> creator x = creator y
       -> Is_true (textorder x y).

Lemma extends_fwitness :
  forall s W W' i x,
    extends W W'
    -> fwitness s W i x
    -> fwitness s W' i x.

In a few places we need to know that the set of uniue famous witnesses is Kuratowski finite (in order to decide received_by). This holds in all but pathological cases. For, example, it holds for any finite world (which includes all the hashgraphs that peers actually manipulate), and it holds for the global world.

Lemma fwitness_ufwitness_finite :
  forall s W i,
    finite (fwitness s W i) -> finite (ufwitness s W i).

Lemma fwitness_finite_finite :
  forall s W,
    finite (member W)
    -> forall i, finite (fwitness s W i).

Lemma ufwitness_finite_finite :
  forall s W,
    finite (member W)
    -> forall i, finite (ufwitness s W i).

Lemma fwitness_finite_global :
  forall s i, finite (fwitness s (global s) i).

Lemma ufwitness_finite_global :
  forall s i, finite (ufwitness s (global s) i).

Definition nonempty W := exists x, member W x.

Lemma nonterminating_nonempty :
  forall W, nonterminating W -> nonempty W.

Definition received_by (s : sample) (W : world) (i : nat) (x : event) :=
  (forall j w, j <= i -> member W w -> rwitness j w -> exists y b, member W y /\ decision s w y b)
  /\
  (forall w, ufwitness s W i w -> x @= w).

Definition received (s : sample) (W : world) (i : nat) (x : event) :=
  received_by s W i x
  /\ forall j, j < i -> ~ received_by s W j x.

Lemma received_by_inhabited :
  forall s W i x,
    nonempty W
    -> received_by s W i x
    -> exists y, member W y /\ round i y.
eq
Lemma received_fun :
  forall s W i i' x,
    received s W i x
    -> received s W i' x
    -> i = i'.

Lemma received_by_global :
  forall s i x,
    (forall w,
       ufwitness s (global s) i w -> x @= w)
    -> received_by s (global s) i x.

Lemma received_by_decide :
  forall s i x,
    decidable (received_by s (global s) i x).

Lemma received_by_exists :
  forall s x,
    member (global s) x
    -> honest (creator x)
    -> exists i,
         received_by s (global s) i x.

Lemma received_defined :
  forall s x,
    member (global s) x
    -> honest (creator x)
    -> exists i,
         received s (global s) i x.
0
Lemma received_by_consistent :
  forall s W W' i x,
    extends W W'
    -> (forall x, decidable (member W x))
    -> nonempty W
    -> received_by s W i x
    -> received_by s W' i x.

Lemma extends_ufwitness :
    forall s W W' i x,
    extends W W'
    -> (forall y, decidable (member W y))
    -> (forall w, member W w -> rwitness i w -> exists y b, member W y /\ decision s w y b)
    -> ufwitness s W i x
    -> ufwitness s W' i x.

Lemma received_consistent :
  forall s W W' i x,
    extends W W'
    -> (forall x, decidable (member W x))
    -> nonempty W
    -> received s W i x
    -> received s W' i x.

Lemma received_cumulative :
  forall s W W' x y i j,
    extends W W'
    -> (forall x, decidable (member W x))
    -> nonempty W
    -> received s W' i x
    -> received s W j y
    -> i <= j
    -> received s W i x.

Lemma decisions_support :
  forall s i,
    exists j,
      i <= j
      /\ forall x y,
           rwitness i x
           -> rwitness j y
           -> member (global s) y
           -> exists b, decision s x y b.
nil
cons

Lemma cumulative_decisions_support :
  forall s i,
    exists j,
      i <= j
      /\ forall i' x y,
           i' <= i
           -> rwitness i' x
           -> round j y
           -> member (global s) y
           -> exists z b, z @= y /\ decision s x z b.
0
Lemma received_by_support :
  forall s i x W,
    extends W (global s)
    -> (forall x, decidable (member W x))
    -> received_by s (global s) i x
    -> exists j,
         (exists y, member W y /\ round j y)
         -> received_by s W i x.

Lemma received_support :
  forall s i x W,
    extends W (global s)
    -> (forall x, decidable (member W x))
    -> nonempty W
    -> received s (global s) i x
    -> exists j,
         (exists y, member W y /\ round j y)
         -> received s W i x.