Library HashgraphFacts

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

Require Import Bool.
Require Import Nat.
Require Import List.
Require Import Omega.
Require Import Decide.

Require Import Tact.
Require Import Relation.
Require Import Weight.
Require Import Calculate.
Require Import Majority.
Require Export Hashgraph.

Peers

Lemma eq_peer_decide : forall (a b : peer), decidable (a = b).

Lemma arbitrary_peer : inhabited peer.

Lemma distinct_peer :
  forall (P : peer -> Prop) a,
    majority stake P every
    -> exists b, P b /\ a <> b.

Lemma honest_decide :
  forall a, decidable (honest a).

Events

Lemma eq_event_decide : forall (x y : event), decidable (x = y).

Parents

Lemma initial_no_parent :
  forall x y, initial y -> parent x y -> False.

Lemma initial_no_self_parent :
  forall x y, initial y -> self_parent x y -> False.

Lemma parents_self_parent :
  forall x y z,
    parents x y z -> self_parent x z.

Lemma parent_decide :
  forall x y, decidable (parent x y).

Lemma parent_finite :
  forall x, finite (fun y => parent y x).

Lemma self_parent_impl_parent :
  forall x y, self_parent x y -> parent x y.

Lemma self_parent_fun :
  forall x x' y,
    self_parent x y
    -> self_parent x' y
    -> x = x'.

Lemma self_parent_creator :
  forall x y, self_parent x y -> creator x = creator y.

Lemma self_parent_decide :
  forall x y, decidable (self_parent x y).

Paths

Lemma self_ancestor_impl_ancestor :
  forall x y, x $= y -> x @= y.

Lemma strict_self_ancestor_impl_strict_ancestor :
  forall x y, x $ y -> x @ y.

Lemma self_parent_well_founded : well_founded self_parent.

Lemma strict_ancestor_well_founded : well_founded strict_ancestor.

Lemma strict_ancestor_parents :
  forall w x y z,
    parents x y z
    -> w @ z
    -> w @= x \/ w @= y.

Lemma strict_self_ancestor_parent :
  forall x y z,
    self_parent y z
    -> x $ z
    -> x $= y.

Lemma strict_ancestor_initial :
  forall x y, x @ y -> initial y -> False.

Lemma ancestor_initial :
  forall x y, x @= y -> initial y -> x = y.

Lemma self_ancestor_creator :
  forall x y, x $= y -> creator x = creator y.
step
Lemma strict_ancestor_irreflex :
  forall x, x @ x -> False.

Path decisions

Lemma strict_ancestor_finite : forall x, finite (fun y => y @ x).
Lemma ancestor_finite : forall x, finite (fun y => y @= x).
Lemma ancestor_decide :
  forall x y,
    decidable (x @= y).

Lemma strict_ancestor_decide :
  forall x y,
    decidable (x @ y).

Lemma self_ancestor_decide :
  forall x y,
    decidable (x $= y).

Lemma self_ancestor_total :
  forall W x y,
    member W x
    -> member W y
    -> honest (creator x)
    -> creator x = creator y
    -> x $= y \/ y $= x.

Lemma self_ancestor_total' :
  forall W x y,
    member W x
    -> member W y
    -> honest (creator x)
    -> creator x = creator y
    -> x $= y \/ y $ x.

Forks

Lemma fork_symm :
  forall x y, fork x y -> fork y x.

Lemma fork_creator :
  forall x y, fork x y -> creator x = creator y.

Lemma fork_decide :
  forall x y, decidable (fork x y).

Worlds

Definition realtime_before (s : sample) (x : event) : world.

Lemma event_world : forall x, exists W, member W x.

Textorder

Lemma textorder_decide :
  forall x y, decidable (Is_true (textorder x y)).