Library Sees
Copyright (c) 2018 by Swirlds, Inc.
Implemented by Karl Crary.
Require Import Decide.
Require Import Tact.
Require Import Relation.
Require Import Majority.
Require Import HashgraphFacts.
y sees x
Definition sees (x y : event) : Prop :=
x @= y
/\ ~ exists z z', z @= y /\ z' @= y /\ fork z z' /\ creator z = creator x.
x @= y
/\ ~ exists z z', z @= y /\ z' @= y /\ fork z z' /\ creator z = creator x.
y strongly sees x
Definition stsees (x y : event) : Prop :=
exists w,
w @= y
/\ supermajority
stake
(fun a => exists z, creator z = a /\ sees x z /\ sees z w)
every.
Lemma sees_impl_ancestor :
forall x y, sees x y -> x @= y.
exists w,
w @= y
/\ supermajority
stake
(fun a => exists z, creator z = a /\ sees x z /\ sees z w)
every.
Lemma sees_impl_ancestor :
forall x y, sees x y -> x @= y.
Lemma 5.12
Lemma strongly_seeing :
forall W x y v w,
member W v
-> member W w
-> fork x y
-> stsees x v
-> stsees y w
-> False.
Lemma stsees_impl_strict_ancestor :
forall x y, stsees x y -> x @ y.
Lemma stsees_impl_ancestor :
forall x y, stsees x y -> x @= y.
Lemma sees_decide :
forall x y,
decidable (sees x y).
Lemma stsees_decide :
forall x y,
decidable (stsees x y).
Lemma self_ancestor_sees_trans :
forall x y z,
x $= y
-> sees y z
-> sees x z.
Lemma self_ancestor_stsees_trans :
forall x y z,
x $= y
-> stsees y z
-> stsees x z.
Lemma stsees_ancestor_trans :
forall x y z,
stsees x y
-> y @= z
-> stsees x z.
Lemma ancestor_sees :
forall x y,
honest (creator x)
-> x @= y
-> sees x y.
forall W x y v w,
member W v
-> member W w
-> fork x y
-> stsees x v
-> stsees y w
-> False.
Lemma stsees_impl_strict_ancestor :
forall x y, stsees x y -> x @ y.
Lemma stsees_impl_ancestor :
forall x y, stsees x y -> x @= y.
Lemma sees_decide :
forall x y,
decidable (sees x y).
Lemma stsees_decide :
forall x y,
decidable (stsees x y).
Lemma self_ancestor_sees_trans :
forall x y z,
x $= y
-> sees y z
-> sees x z.
Lemma self_ancestor_stsees_trans :
forall x y z,
x $= y
-> stsees y z
-> stsees x z.
Lemma stsees_ancestor_trans :
forall x y z,
stsees x y
-> y @= z
-> stsees x z.
Lemma ancestor_sees :
forall x y,
honest (creator x)
-> x @= y
-> sees x y.