Casper CBC: Safety
This is just a list of lemmas & theorem in Casper CBC safety.
consensus" doesn't mean there are
validators which appeared at least once
is a function which generates a property of protocol states from a property of consensus values
> Again, the safety is "It is not possible for nodes to make inconsistent decisions".
The assumption "less than or equal t weight of validators are equivocating" is included in the definition of
and not "used" to prove the safety.
Tips in proof
$ \forall p \in A, \ Decided \land \forall q \in B, \ Decided \Leftrightarrow \forall p \in A \cup B, Decided
> Simply explained as follows.
1. Decided properties of states are consistent
States has common future as union set and decided properties of each state is True at the common future.