Library Fairness

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 Majority.
Require Import Cardinality.
Require Import HashgraphFacts.
Require Import Sees.
Require Import Round.
Require Import Progress.
Require Import Vote.
Require Import Decision.
Require Import Consensus.
Require Import Famous.

Lemma stsees_impl_famous_pre :
  forall s i x y,
    member (global s) y
    -> rwitness i x
    -> (forall j z, parent z y -> round j z -> j <= i)
    -> stsees x y
    -> exists z,
         member (global s) z
         /\ decision s x z true
         /\ rwitness (S first_regular + i) z.
The heart of the proof starts here.

Lemma stsees_impl_famous :
  forall s i x y,
    member (global s) y
    -> rwitness i x
    -> (forall j z, parent z y -> round j z -> j <= i)
    -> stsees x y
    -> famous s (global s) x.

Lemma fwitness_finite_nonterm_if :
  forall s W,
    extends W (global s)
    -> nonterminating W
    -> (forall x, member (global s) x -> decidable (member W x))
    -> forall i x, fwitness s W i x -> finite (fwitness s W i).

Lemma fwitness_finite_global_if :
  forall s i x, fwitness s (global s) i x -> finite (fwitness s (global s) i).

Lemma minimal_witness :
  forall s i,
    exists x,
      member (global s) x
      /\ rwitness i x
      /\ forall j y, parent y x -> round j y -> j < i.

Lemma minimal_witness' :
  forall s i,
    exists x,
      member (global s) x
      /\ rwitness (S i) x
      /\ forall j y, parent y x -> round j y -> j <= i.

Theorem fairness :
  forall s i,
    supermajority
      stake
      (fun a => exists w, creator w = a /\ fwitness s (global s) i w)
      every.

Lemma famous_witness_exists :
  forall s i,
    exists x,
      fwitness s (global s) i x.