CBC-style FFG Safety
Roughly speaking, the safety property of CBC Casper is "safety of decisions" i.e. for any set of validators, there is always a common future state where all the decisions of each validator are true. To detect the safety, validators need the safety oracle. Here I try to prove the safety of Casper FFG with this way. I modify the CBC framework a bit without breaking the "safety of decisions" and then give a safety oracle of FFG. Functions and symbols which are neither defined nor overridden here are the same with definitions in section 1, 2, 3 and 4.5 of the CBC Casper paper.
TODO:
Modify the definition of consensus values so that they include "source" and "target" blocks and add the definition of "supermajority link", "justified".
Modify the slashing condition.
Add proof of safety oracle.
Limitation of parameters
estimator
$ \epsilon_{FFG} = \lambda \sigma. \{b \in C : Latest\_Finalized\_Block(\sigma) \downharpoonright b\}
$ Latest\_Finalized\_Block(\sigma) = argmax \ Height(b), b \in C: Finalized(b, \sigma)
$ Supermajority\_Agreeing(b, \sigma) :\Leftrightarrow sum \ W(v) ≧ 2/3 W\_{total}
$ s.t.\exists v \in V ,\ \exists m \in M, \ sender(m) = v \land estimate(m) = b
$ Finalized(b, \sigma) = Supermajority\_Agreeing(b, \sigma)
Checkpoints
$ C_{FFG} = \{b ∈ B : Height(b) ≡ 0 \ (mod \ Epoch\_Length)\}
Block membership properties
$ Block\_Membership(p) :\Leftrightarrow \exists ! b \in C, \forall b' \in C, (b \downharpoonright b' \Rightarrow p(b') = True) \land (\neg b \downharpoonright b' \Rightarrow p(b') = False)
Modification of CBC framework
To construct FFG, we need to replace the definition of "equivocating messages" with this.
byzantine messages
$ m_1 ⊥ m_2 \Leftrightarrow Sender(m_1) \neq Sender(m_2) \land Estimate(m_1) \downharpoonright Estimate(m_2) \land Estimate(m_2) \downharpoonright Estimate(m_1)
nrryuya.icon > If we adopt the valid message set$ Mwith the above estimator, we need to modify like this. However, can we modify the $ M of FFG with a more complicated estimator so that we can reuse the notion of "equivocating"?
Note that the semantices of$ E(\sigma),$ F(\sigma)and$ \Sigma_tare chenged because of this replacement.
Safety oracle of FFG
BFT oracle for block membership property
$ BFT\_Oracle(p(b), \sigma) = Finalized(b, \sigma)
Lemma: $ BFT\_Oracle is safety oracle if the estimater and consensus values are FFG-style
$ \epsilon = \epsilon_{FFG}, C = C_{FFG},\forall p \in P_C: Block\_Membership(p), \ BFT\_Oracle(p(b), \sigma) \Rightarrow Safe_{c,t}(p, \sigma)