Library Vote
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 Majority.
Require Import HashgraphFacts.
Require Import Sees.
Require Import Round.
Definition elector (n : nat) (w y : event) :=
rwitness n w /\ stsees w y.
Definition creatorstake : event -> nat := fun w => stake (creator w).
This is phrased a bit oddly to ensure that V appears strictly positively.
Definition election (V : event -> bool -> Prop) (n : nat) (y : event)
:=
fun t f =>
exists T F,
weight creatorstake (fun w => elector n w y) (t + f)
/\ weight creatorstake T t
/\ weight creatorstake F f
/\ (forall w, T w -> elector n w y /\ V w true)
/\ (forall w, F w -> elector n w y /\ V w false).
Inductive vote : sample -> event -> event -> bool -> Prop :=
| vote_first {s x y m n v} :
rwitness m x
-> rwitness n y
-> m < n
-> m + first_regular >= n
-> (Is_true v <-> x @ y)
-> vote s x y v
| vote_regular {s x y m n t f v} :
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
-> ((t >= f /\ v = true) \/ (f > t /\ v = false))
-> vote s x y v
| vote_coin_super {s x y m n t f} {v : bool} :
rwitness m x
-> rwitness n y
-> m < 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
-> vote s x y v
| vote_coin {s x y m n t f} :
rwitness m x
-> rwitness n y
-> m < n
-> (n - m) mod coin_freq = 0
-> election (vote s x) (pred n) y t f
-> t <= two_thirds total_stake
-> f <= two_thirds total_stake
-> vote s x y (coin y s)
.
Lemma vote_witness :
forall s x y b,
vote s x y b
-> witness x /\ witness y.
Lemma vote_round :
forall s x y b,
vote s x y b
-> x << y.
Lemma maximum_votes :
forall V n y t f,
election V n y t f
-> t + f <= total_stake.
Lemma election_fun_gen :
forall (V : event -> bool -> Prop) n y t t' f f',
(forall w, w @ y -> forall v v', V w v -> V w v' -> v = v')
-> election V n y t f
-> election V n y t' f'
-> t = t' /\ f = f'.
:=
fun t f =>
exists T F,
weight creatorstake (fun w => elector n w y) (t + f)
/\ weight creatorstake T t
/\ weight creatorstake F f
/\ (forall w, T w -> elector n w y /\ V w true)
/\ (forall w, F w -> elector n w y /\ V w false).
Inductive vote : sample -> event -> event -> bool -> Prop :=
| vote_first {s x y m n v} :
rwitness m x
-> rwitness n y
-> m < n
-> m + first_regular >= n
-> (Is_true v <-> x @ y)
-> vote s x y v
| vote_regular {s x y m n t f v} :
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
-> ((t >= f /\ v = true) \/ (f > t /\ v = false))
-> vote s x y v
| vote_coin_super {s x y m n t f} {v : bool} :
rwitness m x
-> rwitness n y
-> m < 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
-> vote s x y v
| vote_coin {s x y m n t f} :
rwitness m x
-> rwitness n y
-> m < n
-> (n - m) mod coin_freq = 0
-> election (vote s x) (pred n) y t f
-> t <= two_thirds total_stake
-> f <= two_thirds total_stake
-> vote s x y (coin y s)
.
Lemma vote_witness :
forall s x y b,
vote s x y b
-> witness x /\ witness y.
Lemma vote_round :
forall s x y b,
vote s x y b
-> x << y.
Lemma maximum_votes :
forall V n y t f,
election V n y t f
-> t + f <= total_stake.
Lemma election_fun_gen :
forall (V : event -> bool -> Prop) n y t t' f f',
(forall w, w @ y -> forall v v', V w v -> V w v' -> v = v')
-> election V n y t f
-> election V n y t' f'
-> t = t' /\ f = f'.
Special case of Lemma 5.14
Blech, 16 cases!
first
first
regular
coin_super
coin
first
regular
coin_super
coin
first
regular
coin_super
coin
first
regular
coin_super
coin
Lemma 5.14
Lemma vote_consistent :
forall s w x y z n b b',
creator x = creator y
-> round n x
-> round n y
-> vote s w x b
-> vote s w y b'
-> stsees x z
-> stsees y z
-> b = b'.
Lemma elector_decide :
forall n y w,
decidable (elector n w y).
Lemma elector_weight :
forall n y,
exists i,
weight creatorstake (fun w => elector n w y) i.
Lemma election_defined :
forall (V : event -> bool -> Prop) r y,
(forall w v v', V w v -> V w v' -> v = v')
-> (forall w, w @ y -> rwitness r w -> exists v, V w v)
-> exists t f,
election V r y t f.
Lemma vote_defined :
forall s x y m n,
rwitness m x
-> rwitness n y
-> m < n
-> exists b, vote s x y b.
Lemma election_defined' :
forall s x m n y,
rwitness m x
-> m < n
-> exists t f,
election (vote s x) n y t f.
forall s w x y z n b b',
creator x = creator y
-> round n x
-> round n y
-> vote s w x b
-> vote s w y b'
-> stsees x z
-> stsees y z
-> b = b'.
Lemma elector_decide :
forall n y w,
decidable (elector n w y).
Lemma elector_weight :
forall n y,
exists i,
weight creatorstake (fun w => elector n w y) i.
Lemma election_defined :
forall (V : event -> bool -> Prop) r y,
(forall w v v', V w v -> V w v' -> v = v')
-> (forall w, w @ y -> rwitness r w -> exists v, V w v)
-> exists t f,
election V r y t f.
Lemma vote_defined :
forall s x y m n,
rwitness m x
-> rwitness n y
-> m < n
-> exists b, vote s x y b.
Lemma election_defined' :
forall s x m n y,
rwitness m x
-> m < n
-> exists t f,
election (vote s x) n y t f.