Library Consensus

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

Spawn order

Lemma ancestor_impl_spawn_le :
  forall s i x y,
    y = spawn s i
    -> x @= y
    -> exists j, x = spawn s j /\ j <= i.
refl
Lemma strict_ancestor_impl_spawn_lt :
  forall s i x y,
    y = spawn s i
    -> x @ y
    -> exists j, x = spawn s j /\ j < i.

Lemma realtime_refl_spawn :
  forall s i,
    realtime s (spawn s i) (spawn s i).

Lemma realtime_spawn_impl_leq :
  forall s i j,
    realtime s (spawn s i) (spawn s j)
    -> i <= j.

Similarity

Lemma similar_weaken :
  forall s s' i j,
    j <= i
    -> similar s s' i
    -> similar s s' j.

Lemma similar_symm :
  forall s s' i,
    similar s s' i
    -> similar s' s i.

Lemma similar_election :
  forall (V V' : event -> bool -> Prop) n y t f,
    (forall z v, z @ y -> V z v -> V' z v)
    -> election V n y t f
    -> election V' n y t f.

Lemma similar_vote :
  forall s s' x y v,
    (forall z, z @= y -> coin z s = coin z s')
    -> vote s x y v
    -> vote s' x y v.
first
First witnesses
Definition first_witness (s : sample) (n : nat) (x : event) :=
  member (global s) x
  /\ rwitness n x
  /\ forall y,
       member (global s) y
       -> rwitness n y
       -> realtime s x y.

Lemma first_witness_fun :
  forall s n x y,
    first_witness s n x
    -> first_witness s n y
    -> x = y.
Lemma first_witness_realtime :
  forall s n x y,
    first_witness s n x
    -> member (global s) y
    -> rwitness n y
    -> realtime s x y.

Lemma similar_first_witness :
  forall s s' i n,
    similar s s' i
    -> first_witness s n (spawn s i)
    -> first_witness s' n (spawn s i).

Lemma first_witness_exists :
  forall s n x,
    member (global s) x
    -> rwitness n x
    -> exists y, first_witness s n y.
0
S

The coin assumption
Proving this constructively and without any form of the axiom of choice is surprisingly tricky.

Lemma good_coins :
  forall s m x,
    rwitness m x
    -> exists n y t f v,
         m < n
         /\ (n - m) mod coin_freq = 0
         /\ member (global s) y
         /\ rwitness n y
         /\ election (vote s x) (pred n) y t f
         /\ ((t >= f /\ v = true) \/ (f > t /\ v = false))
         /\ forall w,
              member (global s) w
              -> rwitness n w
              -> honest (creator w)
              -> coin w s = v.
We can't name the specific y we want (without using choice) so we have to describe it.
Qs are disjoint
Qs are honest
Number of Qs is bounded
P(i) is limited to before Q(i)

Lemma eligible_voter_maximum :
  forall s n,
    weight_lt
      creatorstake
      (fun x =>
         exists y,
           member (global s) y
           /\ rwitness n x
           /\ stsees x y) (S total_stake).
Lemma neq_negb :
  forall b b', b <> b' -> negb b = b'.

Lemma too_many_voters :
  forall s m n x y i j v,
    member (global s) y
    -> rwitness m x
    -> rwitness (S n) y
    -> m < n
    -> weight creatorstake (fun w => elector n w y /\ vote s x w v) i
    -> weight creatorstake (fun w => elector n w y /\ vote s x w (negb v)) j
    -> weight_lt creatorstake (fun w => exists z, member (global s) z /\ rwitness n w /\ vote s x w v /\ stsees w z) (one_third total_stake)
    -> i >= j
    -> False.

Lemma too_many_voters_elector :
  forall s n x y z i j k v,
    member (global s) y
    -> member (global s) z
    -> rwitness (S n) y
    -> rwitness (S n) z
    -> weight creatorstake (fun w => elector n w y /\ vote s x w v) i
    -> weight creatorstake (fun w => elector n w y /\ vote s x w (negb v)) j
    -> weight creatorstake (fun w => elector n w z /\ vote s x w (negb v)) k
    -> i >= j
    -> k > two_thirds total_stake
    -> False.

Lemma too_many_voters_honest :
  forall s m n x y i j v,
    member (global s) y
    -> rwitness m x
    -> rwitness (S n) y
    -> m < n
    -> weight creatorstake (fun w => elector n w y /\ vote s x w v) i
    -> weight creatorstake (fun w => elector n w y /\ vote s x w (negb v)) j
    -> (forall w, member (global s) w -> rwitness n w -> honest (creator w) -> vote s x w (negb v))
    -> i >= j
    -> False.

Lemma plus_two_no_coin :
  forall n,
    n mod coin_freq = 0
    -> (2 + n) mod coin_freq <> 0.

Theorem 5.16
Theorem fame_consensus :
  forall s x,
    member (global s) x
    -> witness x
    -> exists y v,
         member (global s) y
         /\ decision s x y v.
first
regular
coin_super
first
regular
coin_super
coin