Library Progress

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

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

Require Import Tact.
Require Import Decide.
Require Import Cardinality.
Require Import Calculate.
Require Import Majority.
Require Import Relation.
Require Import HashgraphFacts.
Require Import Sees.
Require Import Round.

Lemma honest_event_exists :
  forall s, exists x, member (global s) x /\ honest (creator x).

Lemma realtime_impl_self_ancestor :
  forall s x y,
    honest (creator x)
    -> creator x = creator y
    -> realtime s x y
    -> x $= y.

Lemma event_transmit :
  forall s x a,
    member (global s) x
    -> honest (creator x)
    -> honest a
    -> exists y,
         member (global s) y
         /\ creator y = a
         /\ x @= y.

Lemma event_broadcast :
  forall s x,
    member (global s) x
    -> honest (creator x)
    -> exists y,
         member (global s) y
         /\ honest (creator y)
         /\ forall a,
              honest a
              -> exists w,
                   creator w = a
                   /\ x @= w
                   /\ w @= y.
nil
Lemma round_advanced :
  forall x y i j,
    round i x
    -> round j y
    -> supermajority
         stake
         (fun a =>
            exists w,
              creator w = a
              /\ x @= w
              /\ stsees w y)
         every
    -> i < j.

Lemma global_nonterminating :
  forall s, nonterminating (global s).
0
Lemma events_are_received :
  forall s x,
    member (global s) x
    -> honest (creator x)
    -> exists i,
         forall y,
           member (global s) y
           -> rwitness i y
           -> x @= y.

Lemma events_reach_every_world :
  forall s W x,
    extends W (global s)
    -> nonterminating W
    -> member (global s) x
    -> honest (creator x)
    -> member W x.