Library Decision

Copyright (c) 2018 by Swirlds, Inc. Implemented by Karl Crary.
Require Import Nat.
Require Import Bool.
Require Import List.
Require Import Omega.
Require Import Tact.
Require Import Relation.
Require Import Decide.
Require Import Weight.
Require Import Calculate.
Require Import Weight.
Require Import Majority.
Require Import HashgraphFacts.
Require Import Sees.
Require Import Round.
Require Import Vote.
Definition decision (s : sample) (x y : event) (v : bool) :=
  exists m n t f,
    rwitness m x
    /\ rwitness n y
    /\ m + first_regular < n
    /\ (n - m) mod coin_freq <> 0
    /\ election (vote s x) (pred n) y t f
    /\ (if v then t else f) > two_thirds total_stake.

Lemma elector_rwitness :
  forall n x y, elector n x y -> rwitness n x.

Lemma elector_unique :
  forall W n x y z z',
    member W z
    -> member W z'
    -> creator x = creator y
    -> elector n x z
    -> elector n y z'
    -> x = y.

Lemma elector_minimum :
  forall n x e,
    round (S n) x
    -> weight creatorstake (fun w => elector n w x) e
    -> e > two_thirds total_stake.

Lemma election_fun :
  forall s n x y t t' f f',
    election (vote s x) n y t f
    -> election (vote s x) n y t' f'
    -> t = t' /\ f = f'.

Lemma decision_fun :
  forall s x y v v',
    decision s x y v
    -> decision s x y v'
    -> v = v'.

Lemma decision_decide :
  forall s x y b,
    decidable (decision s x y b).

Lemma destruct_election :
  forall s n x y t f,
    election (vote s x) n y t f
    -> weight creatorstake (fun w => elector n w y) (t + f)
       /\ weight creatorstake (fun w => elector n w y /\ vote s x w true) t
       /\ weight creatorstake (fun w => elector n w y /\ vote s x w false) f.

Lemma destruct_election' :
  forall s n x y t f,
    election (vote s x) n y t f
    -> weight creatorstake (fun w => elector n w y) (t + f)
       /\ forall v, weight creatorstake (fun w => elector n w y /\ vote s x w v) (if v then t else f).

Definition peer_vote (s : sample) (W : world) (w : event) (n : nat) (a : peer) (v : bool) :=
  exists x y, creator x = a /\ round n x /\ vote s w x v /\ stsees x y /\ member W y.

Definition offer (n : nat) (a : peer) (y : event) :=
  exists x, creator x = a /\ elector n x y.

Lemma elector_vote_peer :
  forall s W n x y z v,
    member W z
    -> elector n y z
    -> vote s x y v
    -> peer_vote s W x n (creator y) v.

Lemma peer_vote_elector :
  forall s W x n a v y z,
    member W z
    -> peer_vote s W x n a v
    -> creator y = a
    -> elector n y z
    -> vote s x y v.

Lemma peer_vote_offer :
  forall s W x n a v y,
    member W y
    -> peer_vote s W x n a v
    -> offer n a y
    -> exists z, creator z = a /\ elector n z y /\ vote s x z v.

Lemma decision_vote_consistent :
  forall s W w x y n v v',
    member W x
    -> member W y
    -> round n x
    -> round n y
    -> decision s w x v
    -> vote s w y v'
    -> v = v'.

Lemma unanimous_election :
  forall s W n x y v e,
    member W y
    -> rwitness (S n) y
    -> (forall w, member W w -> rwitness n w -> vote s x w v)
    -> weight creatorstake (fun w => elector n w y) e
    -> election (vote s x) n y (if v then e else 0) (if v then 0 else e).

Lemma unanimity_persists :
  forall s W m n x v,
    round m x
    -> m + first_regular < n
    -> (forall y, member W y -> rwitness n y -> vote s x y v)
    -> (forall y, member W y -> rwitness (S n) y -> vote s x y v).

Lemma unanimity :
  forall s W m n x y v,
    member W y
    -> round m y
    -> m <= n
    -> decision s x y v
    -> forall z, member W z -> rwitness n z -> vote s x z v.
eq
Lemma decision_consistent :
  forall s W x y y' v v',
    member W y
    -> member W y'
    -> decision s x y v
    -> decision s x y' v'
    -> v = v'.

Lemma unanimity_impl_decision :
  forall s W x y m n v,
    member W y
    -> round m x
    -> (forall z, member W z -> rwitness n z -> vote s x z v)
    -> rwitness (S n) y
    -> m + first_regular < S n
    -> (S n - m) mod coin_freq <> 0
    -> decision s x y v.

Lemma decisions_propagate :
  forall s W x y l m v,
    member W y
    -> round l x
    -> round m y
    -> decision s x y v
    -> forall n z,
         member W z
         -> m < n
         -> (n - l) mod coin_freq <> 0
         -> rwitness n z
         -> decision s x z v.

Lemma succ_no_coin :
  forall n,
    n mod coin_freq = 0
    -> (S n) mod coin_freq <> 0.

Lemma 5.15
Corollary decisions_propagate_round :
  forall s W x y m v,
    member W y
    -> nonterminating W
    -> round m y
    -> decision s x y v
    -> exists n,
         n <= m + 2
         /\ forall z,
              member W z
              -> rwitness n z
              -> decision s x z v.