owned this note
owned this note
Published
Linked with GitHub
# [Minimal CBC Casper](https://github.com/cbc-casper/cbc-casper-paper/blob/master/cbc-casper-paper-draft.pdf) Symbol / Terminology
## Prerequisite Notation
![](https://i.imgur.com/QG4EKdv.png)
- (anonymous function)[https://en.wikipedia.org/wiki/Lambda_calculus]
### 2.1 validator name
![](https://i.imgur.com/zO7ofO8.png)
### 2.2 validator weights
![](https://i.imgur.com/pPCgANk.png)
### 2.3 byzantein fault tolerance threshold
![](https://i.imgur.com/W8S9pbS.png)
### 2.4 consensus value
![](https://i.imgur.com/aFSwALM.png)
### 2.5 estimator
![](https://i.imgur.com/V09RGZ0.png)
### ?? protocol state, protocol message
![](https://i.imgur.com/seWP5Un.png)
### 2.6 estimate, sender, justification
![](https://i.imgur.com/6tNhjFm.png)
### 2.7 preliminary protocol state, protocol message
![](https://i.imgur.com/CW1HNdG.png)
### 2.8 protocol state transition
![](https://i.imgur.com/OQy6BW8.png)
### 2.9 equivocating messages
![](https://i.imgur.com/WxIJjBV.png)
### 2.10 equivocating validators
![](https://i.imgur.com/QqFrNpK.png)
### 2.11 equivocation fault weight
![](https://i.imgur.com/KhgQwKP.png)
### 2.12 protocol state with equivocation fault tolerance t
![](https://i.imgur.com/DddLo85.png)
### def 3.1 future cone
![](https://i.imgur.com/FvJUwti.png)
### lemma 1: monotonic futures
![](https://i.imgur.com/RsC25t1.png)
### theorem 1: 2-party common futures
![](https://i.imgur.com/uzxlfnr.png)
### theorem 2: n-party common futures
![](https://i.imgur.com/355l3ob.png)
### def 3.2: properties of protocol states
![](https://i.imgur.com/sPBUGuC.png)
잠깐 중간 요약
- estimator: state -> consensus value
- estimate: consensus value
- property: state -> boolean
### def 3.2: decided properties of protocol states
![](https://i.imgur.com/NlYtpx3.png)
### lemma 2: forward consistency
![](https://i.imgur.com/gap4qnf.png)
### lemma 3: backward consistency
![](https://i.imgur.com/5pjMJUY.png)
### theorem 3: two-party consensus safety
![](https://i.imgur.com/QZsP0Tm.png)
### def 3.4: inconsistency of properties of protocol states
![](https://i.imgur.com/xWL55YT.png)
### def 3.5: consistency of properties of protocol states
![](https://i.imgur.com/CXwNQeA.png)
### def 3.6: decisions on properties of protocol states
![](https://i.imgur.com/7EGBiLY.png)
### theorem 4: n-party consensus safety for properties of protocol states
![](https://i.imgur.com/AJZNIZe.png)
### def 3.7: properties of consensus
![](https://i.imgur.com/hvD3KwR.png)
- 주의: properties of protocol state와 다름
### def 3.8: mutually corresponding property of protocol states
![](https://i.imgur.com/1CDs5Ve.png)
- For example, if we have an estimator for a binary consensus protocol, which has function signature E : Σ → P({0,1}) \ ∅, and the property of consensus values p ∈ P{0,1} with p(0) = True and p(1) = False, then H(p) is defined to be satisifed by a protocol state σ if E(σ) = {0}, but not if E(σ) = {1} or E(σ) = {0,1}.
### def 3.9: consistency of properties of the consensus
![](https://i.imgur.com/R9Mbxqv.png)
### lemma 4: if properties of protocol states that correspond to properties of consensus values are consistent, then these properties of consensus values are also consistent
![](https://i.imgur.com/gyiIBu6.png)
### def 3.10: Decided on properties of consensus values
![](https://i.imgur.com/JGB4vc7.png)
### def 3.11: Decisions on properties of consensus values
![](https://i.imgur.com/ghP9afw.png)
### theorem 5: n-partyh consensus sasfety for properties of the consensus (values)
![](https://i.imgur.com/mEBAf4l.png)
## 4 Example Protocols
## 4.1 Preliminary Definitions
### Definition 4.1 (Observed validators).
![](https://i.imgur.com/e7LyDBI.png)
### Definition 4.2. Later messages
![](https://i.imgur.com/wZTFOvT.png)
### Definition 4.3 (Message From a Sender).
![](https://i.imgur.com/UQzFxDe.png)
### Definition 4.4 (Messages From a Group).
![](https://i.imgur.com/D1rUTZL.png)
### Definition 4.5. Later messages from a sender
![](https://i.imgur.com/5ZAvBC4.png)
### Definition 4.6 (Latest Message).
![](https://i.imgur.com/ql9slMw.png)
### Definition 4.7 (Latest message driven estimator).
![](https://i.imgur.com/XlxT7Gi.png)
### Definition 4.8 (Latest Estimates).
![](https://i.imgur.com/BOJvtG3.png)
### Definition 4.9 (Latest message driven estimator).
![](https://i.imgur.com/2nRlfqr.png)
### Definition 4.10 (≼).
![](https://i.imgur.com/jdMRfCs.png)
### Lemma 5 (Non-equivocating validators have at most one latest message). ∀v ∈ V,
![](https://i.imgur.com/0IWfwh2.png)
![](https://i.imgur.com/AYEWyIk.png)
### lemma 6
![](https://i.imgur.com/MIchKxn.png)
### Lemma 7 (Monotonicity of Justifications).
![](https://i.imgur.com/sQhWlD4.png)
### Lemma 8
![](https://i.imgur.com/ubKUXCR.png)
### Lemma 9
![](https://i.imgur.com/0X27Gft.png)
### Lemma 10 (Observed non-equivocating validators have one latest messages). ∀σ ∈ Σ, ∀v ∈ V
![](https://i.imgur.com/vocHxrL.png)
### Definition 4.11 (Latest messages from non-Equivocating validators).
![](https://i.imgur.com/XeL4FjL.png)
### Definition 4.12 (Latest honest message driven estimator).
![](https://i.imgur.com/Ld7ugqd.png)
### Definition 4.13 (Latest Estimates from non-Equivocating validators).
![](https://i.imgur.com/AFWJObi.png)
### Definition 4.14 (Latest honest estimate driven estimator).
![](https://i.imgur.com/U1M0Wtq.png)
### Definition 4.15 (Argmax).
![](https://i.imgur.com/SF4ckes.png)
### Definition 4.16 (Score).
![](https://i.imgur.com/QAxJBsp.png)
### Definition 4.17 (Casper the Friendly Binary Consensus).
![](https://i.imgur.com/JIBFfwG.png)
### Definition 4.18 (Example non-trivial properties of this binary consensus protocol).
![](https://i.imgur.com/NuL1If7.png)
## 4.3 Casper the Friendly Integer Consensus
![](https://i.imgur.com/4xKaUyZ.png)
## 4.4 Casper the Friendly GHOST
### Definition 4.23 (Blocks).
![](https://i.imgur.com/OGPCDe1.png)
- g: genesis block
- D: block data
### Definition 4.24 (Previous block resolver).
![](https://i.imgur.com/z2QEzVd.png)
- Proj_1 ?
### Definition 4.25 (n-cestor: n’th generation ancestor block).
![](https://i.imgur.com/e4DXrGM.png)
### Definition 4.26 (Blockchain membership, m1 m2).
![](https://i.imgur.com/LxGeo1x.png)
### Definition 4.27 (Score of a block).
![](https://i.imgur.com/IQZt2Cj.png)
### Definition 4.28. (Children of a block)
![](https://i.imgur.com/5x09loJ.png)
### Definition 4.29. (Best children of a block)
![](https://i.imgur.com/duyVJQJ.png)
### Definition 4.30. GHOST
![](https://i.imgur.com/9KezItJ.png)
### Definition 4.31 (Casper the Friendly Ghost).
![](https://i.imgur.com/pcVKIac.png)
### Definition 4.32 (Example non-trivial properties of consensus values).
![](https://i.imgur.com/dyVzCsX.png)
## 4.5 Casper the Friendly CBC Finality Gadget
### Definition 4.33 (The underlying blockchain). We assume the blockchain has blocks:
![](https://i.imgur.com/k2ntDYC.png)
### Definition 4.34 (Blocks).
![](https://i.imgur.com/MpDdaHj.png)
- Blocks/blockchains will be the consensus value for blockchain consensus.
- Every block in a blockchain has a single previous block.
### Definition 4.35 (Previous block resolver).
![](https://i.imgur.com/E1UTZbt.png)
### Definition 4.36 (n-cestor: n’th generation ancestor block).
![](https://i.imgur.com/Y1Vr4PV.png)
### Definition 4.37 (Blockchain membership, m1 m2).
![](https://i.imgur.com/Si1qbz7.png)
![](https://i.imgur.com/MXfDFre.png)
### Definition 4.38 (Consensus values in the CBC Finality Gadget).
![](https://i.imgur.com/lpmyPEW.png)
### Definition 4.39 (Epoch Score).
![](https://i.imgur.com/omlWPEu.png)
### Definition 4.40 (Children Epochs).
![](https://i.imgur.com/5s9Gzrj.png)
### Definition 4.41. Best Children Epochs
![](https://i.imgur.com/tnHnxfL.png)
### Definition 4.42. GHOST on the epochs:
![](https://i.imgur.com/cZijuuK.png)
### Definition 4.43 (Estimator for the CBC Finality gadget).
![](https://i.imgur.com/yAbkgKe.png)
### Definition 4.44 (Fork Choice Rule for the CBC Finality gadget).
![](https://i.imgur.com/VVTHYlN.png)
## 4.6 Casper the Friendly CBC Sharded Blockchain
### Definition 4.45 (Shard IDs S).
### Definition 4.46 (Message Payloads P).
### Definition 4.47 (Block Data D).
![](https://i.imgur.com/lkAU32s.png)
### Definition 4.48 (Lists of Things).
### Definition 4.49 (List Prefix ≼).
![](https://i.imgur.com/MNODWU3.png)
![](https://i.imgur.com/RGSmvPV.png)
### Definition 4.50 (Blocks B).
<!-- ![](https://i.imgur.com/8gU8XgM.png) -->
![](https://i.imgur.com/eXWIYeW.png)
### Definition 4.51 (Cross-shard Messages Q).
![](https://i.imgur.com/QqaEHuq.png)
### Definition 4.52 (Genesis Logs).
![](https://i.imgur.com/NZhKr7o.png)
### Definition 4.53 (Genesis Sources).
![](https://i.imgur.com/k79FUEc.png)
### Definition 4.54 (Shard ID Consistency).
![](https://i.imgur.com/iLdfupP.png)
### Definition 4.55 (Monotonicity Conditions).
![](https://i.imgur.com/ILknQIW.png)
### Definition 4.56 (Messsage Arrival Conditions).
![](https://i.imgur.com/3xJyLXP.png)
### Definition 4.57 (Set of Blocks B).
![](https://i.imgur.com/6WXaRl6.png)
### Definition 4.58 (Consensus values).
![](https://i.imgur.com/hkPs8IE.png)
### Definition 4.60 (Filter Conditions).
![](https://i.imgur.com/N4R8L7D.png)
![](https://i.imgur.com/Md5ukPS.png)
### Definition 4.61 (Filtered Children).
![](https://i.imgur.com/1cpQ6aD.png)
### Definition 4.62 (Best Child).
![](https://i.imgur.com/H2CshNz.png)
### Definition 4.63 (Block score).
![](https://i.imgur.com/7ensEmd.png)
### Definition 4.64. Filtered_GHOST
![](https://i.imgur.com/2wYMhXc.png)
### Definition 4.65 (Fork Choice $\mathcal{E}_C$ (for child shard C)).
![](https://i.imgur.com/E6pOkM9.png)
## + Safety Oracle + [naterush/cbc-casper-paper](https://github.com/naterush/cbc-casper-paper/blob/188c4b0/safety-oracle.tex)
### Definition 7.7 (Latest justifications from non-Equivocating validators).
$$
L^H_J:\Sigma \to (\mathcal{V} \to \mathcal{P}(\Sigma)) \\
L^H_J(\sigma)(v) = \{Justification(m) : m \in L^H_M(\sigma)(v)\}
$$
### Definition 7.8 (Validators agreeing with p in σ).
$$
Agreeing: P_{\mathcal{C}} \times \Sigma \to \mathcal{P}(\mathcal{V}) \\
Agreeing(p, \sigma) :\Leftrightarrow \{v \in \mathcal{V} : \forall c \in L^H_E(\sigma)(v), p(c)\}
$$
### Definition 7.9 (Validators disagreeing with p in σ).
$$
Disagreeing: P_{\mathcal{C}} \times \Sigma \to \mathcal{P}(\mathcal{V})\\
Disagreeing(p, \sigma) :\Leftrightarrow \{v \in \mathcal{V} : \exists c \in L^H_E(\sigma)(v), \neg p(c)\}
$$
### Definition 7.10 (Weight measure).
$$
Weight: \mathcal{P}(\mathcal{V}) \to \mathbb{R}_+ \\
Weight(V) :\Leftrightarrow \sum_{v \in V} \mathcal{W}(v)
$$
### Definition 7.11 (Non-equivocating majority). ??
$$
Majority^H: \mathcal{P}(\mathcal{V}) \times \Sigma \to \{True, False\}\\
Majority^H(V, \sigma) :\Leftrightarrow Weight(V) > Weight(\mathcal{V} \setminus E(\sigma))/2
$$
### Definition 7.12 (Non-equivocating majority driven property). ??
$$
Majority\_Driven^H: P_{\mathcal{C}} \to \{True, False\}\\
Majority\_Driven^H(p) :\Leftrightarrow \forall \sigma \in \Sigma, Majority^H(Agreeing(p, \sigma), \sigma) \implies \forall c \in \mathcal{E}(\sigma), p(c)
$$
### Definition 7.13 (Max weight driven property).
$$
Max\_Driven: P_{\mathcal{C}} \to \{True, False\}\\
Max\_Driven(p) :\Leftrightarrow \forall \sigma \in \Sigma, Weight(Agreeing(p, \sigma)) > Weight(Disagreeing(p, \sigma)) \implies \forall c \in \mathcal{E}(\sigma), p(c)
$$
### Definition 7.14 (Later disagreeing messages).
$$
Later\_Disagreeing: P_{\mathcal{C}} \times M \times \mathcal{V} \times \Sigma \to \mathcal{P}(M)\\
Later\_Disagreeing(p,m,v,\sigma) = \{m' \in Later\_From(m, v, \sigma) : \neg p(Estimate(m')) \}
$$
### Definition 7.15. Helper function ( !({a}) = a )
$$
!: \mathcal{P}(X) \to X\\
!(A) = a \in A : \forall b \in A, b = a
$$
### Definition 7.16 (Clique with n layers).
\begin{align}
Clique&: \mathbb{N}^+ \times \mathcal{P}(\mathcal{V}) \times P_{\mathcal{C}} \times \Sigma \to \{True, False\} \\
Clique(1, V, p, \sigma) &:\Leftrightarrow \forall v \in V, V \subseteq Agreeing(p, L^H_J(\sigma)(v)) \\
&~~~~\land \forall v' \in V, Later\_Disagreeing(p, L^H_M(L^H_J(\sigma)(v))(v'), v', \sigma) = \emptyset \\
Clique(n, V, p, \sigma) &:\Leftrightarrow \forall v \in V, V \subseteq Agreeing(p, L^H_J(\sigma)(v)) \\
&~~~~\land \forall v \in V, Clique\_Cond(n - 1, V, p, L^H_J(\sigma)(v))
\end{align}
### Definition 7.17 (Minimal transitions).
$$
Minimal_t = \{ (\sigma, \sigma') \in \Sigma_t^2: \sigma \to \sigma' \land \nexists \sigma'' . \sigma \to \sigma'' \to \sigma' \land \sigma'' \neq \sigma \land \sigma'' \neq \sigma' \}
$$
### Lemma 11 (Minimal transitions do not change Later From for any non-sender)
$\forall (\sigma, \sigma') \in Minimal_t, \forall m \in M$, letting $\overline{m} =~!\sigma'\setminus\sigma$ and $\overline{v} = Sender(\overline{m})$,
$$
\forall v \in \mathcal{V} \setminus \{\overline{v}\}, Later\_From(m,v,\sigma) = Later\_From(m,v,\sigma')
$$
### Lemma 12 (Minimal transitions do not change equivocation status for any non-sender).
$\forall (\sigma, \sigma') \in Minimal_t$, letting $\overline{m} =~!\sigma'\setminus\sigma$, and $\overline{v} = Sender(\overline{m})$,
$$
\forall v \in \mathcal{V} \setminus \{\overline{v}\}, (v \in E(\sigma) \iff v \in E(\sigma'))
$$
### Lemma 13 (Minimal transitions do not change latest messages for any non-sender)
$\forall (\sigma, \sigma') \in Minimal_t$, letting $\overline{m} =~!\sigma'\setminus\sigma$, and $\overline{v} = Sender(\overline{m})$
$$
\forall v \in \mathcal{V} \setminus \{\overline{v}\}, L^H_M(\sigma)(v) = L^H_M(\sigma')(v)
$$
### Lemma 14 (Minimal transitions do not change latest justification for any non-sender)
$\forall (\sigma, \sigma') \in Minimal_t$, letting $\overline{m} =~!\sigma'\setminus\sigma$, and $\overline{v} = Sender(\overline{m})$
$$
\forall v \in \mathcal{V} \setminus \{\overline{v}\}, L^H_J(\sigma)(v) = L^H_J(\sigma')(v)
$$
### Lemma 15 (Minimal transitions do not change Later Disagreeing for any non-sender).
$\forall p \in P_{\mathcal{C}}, \forall (\sigma, \sigma') \in Minimal_t, \forall m \in M$, letting $\overline{m} =~!\sigma'\setminus\sigma$ and $\overline{v} = Sender(\overline{m})$
$$
\forall v \in \mathcal{V} \setminus \{\overline{v}\}, Later\_Disagreeing(p, m, v, \sigma) = Later\_Disagreeing(p, m, v, \sigma')
$$
### Lemma 16 (Minimal transition from outside clique maintains clique).
$\forall p \in P_{\mathcal{C}}, \forall (\sigma, \sigma') \in Minimal_t, \forall V \subseteq \mathcal{V}$, letting $\overline{m} =~!\sigma'\setminus\sigma$ and $\overline{v} = Sender(\overline{m})$
$$
\overline{v} \notin V \land Clique(1, V, p, \sigma) \implies Clique(1, V, p, \sigma')
$$
---
> New messages at least leaves a smaller clique behind
### Lemma 17 (Free sub-clique).
$\forall p \in P_{\mathcal{C}}, \forall V \subseteq \mathcal{V}, \forall (\sigma, \sigma') \in Minimal_t$, letting $\overline{m} =~!\sigma'\setminus\sigma$ and $\overline{v} = Sender(\overline{m})$,
$$
Clique(1, V, p, \sigma) \implies Clique(1, V \setminus \{\overline{v}\}, p, \sigma')
$$
---
> Non-equivocating messages from clique members see clique agree.
### Lemma 18 (Later messages from a non-equivocating validator include all earlier messages).
$\forall \sigma \in \Sigma$,
\begin{align}
&v \notin E(\sigma) \land \sigma_1 \in \Sigma ~\land \sigma_1 \subseteq \sigma \land \sigma_2 \subseteq \sigma \land \sigma_1 \cap \sigma_2 = \emptyset \\
\implies& \forall m_1 \in \sigma_1 : Sender(m_1) = v, \forall m_2 \in \sigma_2 : Sender(m_2) = v, m_1 \in Justification(m_2)
\end{align}
Note that $\sigma_2$ is not a protocol state, but just a collection of messages. The notation should probably be changed!
- 본인이 보낸 메시지들은 항상 later 관계를 유지 -- honest 하기 때문에 당연..
### Lemma 19 ($\overline{m}$ is $\overline{v}$'s latest message in $\sigma$').
$\forall (\sigma, \sigma') \in Minimal_t$, letting $\overline{m} =~!\sigma'\setminus\sigma$ and $\overline{v} = Sender(\overline{m})$,
$$
\overline{v} \notin E(\sigma') \implies \forall m \in \sigma: Sender(m) = \overline{v}, m \in Justification(\overline{m})
$$
### Lemma 20 (Latest honest messages from non-equivocating messages are either the same as in their previous latest message, or later)
$\forall (\sigma, \sigma') \in Minimal_t, \forall v \in \mathcal{V}$, letting $\overline{m} =~!\sigma'\setminus\sigma$ and $\overline{v} = Sender(\overline{m})$
\begin{align}
\overline{v} \notin E(\sigma') \land v \notin E(\sigma) \implies&~!L^H_M(Justification(\overline{m}))(v) =~!L^H_M(!L^H_J(\sigma)(\overline{v}))(v) \\
&\lor Later(!L^H_M(Justification(\overline{m}))(v),~!L^H_M(!L^H_J(\sigma)(\overline{v}))(v))
\end{align}
-
### Lemma 21 (Later message inclusion?).
$\forall \sigma^* \in \Sigma, \forall m_1 \in \sigma^*, \forall m_2 \in \sigma^*$,
$$
Later(m_1, m_2) \implies m_1 \in Later\_From(m_2, Sender(m_1), \sigma^*)
$$
### Lemma 22 (Helper function).
$\forall \sigma \in \Sigma, \forall v \in \mathcal{V}$ such that ! is defined,
$$
p(Estimate(!L^H_M(\sigma)(v))) \implies v \in Agreeing(p, \sigma)
$$
### Lemma 23 (Non-equivocating messages from clique members see clique agree)
$\forall p \in P_{\mathcal{C}} : Majority\_Driven^H(p), \forall (\sigma, \sigma') \in Minimal_t, \forall V \subseteq \mathcal{V}$, letting $\overline{m} =~!\sigma'\setminus\sigma$ and $\overline{v} = Sender(\overline{m})$
$$
Clique(1, V, p, \sigma) \land \overline{v} \in V \land \overline{v} \notin E(\sigma') \implies V \subseteq Agreeing(p, Justification(\overline{m}))
$$
---
> Non-equivocating messages from majority clique members agree
### Lemma 24 (New messages from majority clique members agree)
$\forall p \in P_{\mathcal{C}} : Majority\_Driven^H(p), \forall (\sigma, \sigma') \in Minimal_t, \forall V \subseteq \mathcal{V}$, letting $\overline{m} =~!\sigma'\setminus\sigma$ and $\overline{v} = Sender(\overline{m})$.
\begin{align}
Clique(1, V, p, \sigma) \land \overline{v} \in V \land \overline{v} \notin E(\sigma')& \\
\land \forall v \in V, Majority^H(V, !L^H_J(\sigma)(v)) & \implies \overline{v} \in Agreeing(p, \sigma')
\end{align}
---
> Honest messages from majority clique members do not break the clique
### Lemma 25.
$$
\overline{v} \notin E(\sigma') \implies !L^H_M(Justification(\overline{m}))(\overline{v}) = !L^H_M(\sigma)(\overline{v})
$$
### Lemma 26.
$$
\overline{v} \notin E(\sigma') \implies Later(\overline{m}, !L^H_M(\sigma)(\overline{v}))
$$
### Lemma 27 (Nothing later than latest honest message).
$\forall v \in \mathcal{V}, \forall \sigma \in \Sigma, \forall m \in M$
$$
v \notin E(\sigma) \implies Later\_From(!L^H_M(\sigma)(v), v, \sigma) = \emptyset
$$
### Lemma 28 (Later messages for sender is just the new message).
$\forall v \in \mathcal{V}, \forall \sigma \in \Sigma, \forall m \in M$
$$
v \notin E(\sigma) \implies Later\_From(!L^H_M(\sigma)(v), v, \sigma) = \emptyset
$$
### Lemma 29 (Later disagreeing is monotonic).
$\forall v \in V, \forall \sigma \in \Sigma, \forall m_1 \in M$,
$$
m_1 \in Justification(m_2) \implies Later\_Disagreeing(p,m_2,v,\sigma) \subseteq Later\_Disagreeing(p,m_1,v,\sigma)
$$
### Lemma 30.
\begin{align}
&\overline{v} \notin E(\sigma') \land v' \notin E(\sigma) \\
&Later\_Disagreeing(p, L^H_M(L^H_J(\sigma)(\overline{v}))(v'), v', \sigma) = \emptyset \\
\implies&Later\_Disagreeing(p,~!L^H_M(Justification(\overline{m}))(v'), v', \sigma') = \emptyset \\
\end{align}
### Lemma 31 (New non-equivocating latest messages from members of majority clique don’t break the clique).
$\forall p \in P_{\mathcal{C}} : Majority\_Driven^H(p), \forall \sigma \in \Sigma_t, \forall (\sigma, \sigma') \in Minimal_t,\forall V \subseteq \mathcal{V}$, letting $\overline{m} =~!\sigma'\setminus\sigma$, and $\overline{v} = Sender(\overline{m})$,
\begin{align}
Clique(1, V, p, \sigma) \land \overline{v} \in V \land \overline{v} \notin E(\sigma') &\\
\land ~\forall v \in V, Majority^H(V, !L^H_J(\sigma)(v)) & \implies Clique(1, V, p, \sigma')
\end{align}
---
> Equivocations from Validators in Clique do not break cliques
### Definition 7.18 (One layer clique oracle threshold size).
\begin{align}
Threshold_t&: \mathcal{P}(\mathcal{V}) \times \Sigma_t \to \{True, False\} \\
Threshold_t(V, \sigma) &:\Leftrightarrow Weight(V) > Weight(\mathcal{V})/2 + t - Weight(E(\sigma))
\end{align}
### Lemma 32.
$$
Threshold_t(V, \sigma) \implies \forall v \in V, Majority^H(V, !L^H_J(\sigma)(v))
$$
### Definition 7.19 (Clique oracle with n layers).
\begin{align}
Clique\_Oracle_t&: \mathcal{P}(\mathcal{V}) \times \Sigma_t \to \{True, False\} \\
Clique\_Oracle_t(n, V, \sigma, p) &:\Leftrightarrow Clique(n, V \setminus E(\sigma), \sigma, p) \land Threshold_t(V \setminus E(\sigma), \sigma) \\
\end{align}
### Lemma 33 (Clique oracles preserved over minimal transitions from validators not in clique).
$\forall p \in P_{\mathcal{C}} : Majority\_Driven^H(p),$ $\forall (\sigma, \sigma') \in Minimal_t, \forall V \subseteq \mathcal{V}$, letting $\overline{m} = ~ !\sigma'\setminus\sigma$, and $\overline{v} = Sender(\overline{m})$,
$$
\overline{v} \notin V \setminus E(\sigma) \land Clique\_Oracle_t(1, V, \sigma, p) \implies Clique\_Oracle_t(1, V, \sigma', p)
$$
### Lemma 34 (Clique oracles preserved over minimal transitions from non-equivocating validators)
$\forall p \in P_{\mathcal{C}} : Majority\_Driven^H(p),$ $\forall (\sigma, \sigma') \in Minimal_t, \forall V \subseteq \mathcal{V}$, letting $\overline{m} = ~ !\sigma'\setminus\sigma$, and $\overline{v} = Sender(\overline{m})$,
$$
\overline{v} \in V \setminus E(\sigma) \land \overline{v} \notin E(\sigma') \land Clique\_Oracle_t(1, V, \sigma, p) \implies Clique\_Oracle_t(1, V, \sigma', p)
$$
### Lemma 35 (Clique oracles preserved over minimal transitions from equivocating validators).
$\forall p \in P_{\mathcal{C}} : Majority\_Driven^H(p),$ $\forall (\sigma, \sigma') \in Minimal_t, \forall V \subseteq \mathcal{V}$, letting $\overline{m} = ~ !\sigma'\setminus\sigma$, and $\overline{v} = Sender(\overline{m})$,
$$
\overline{v} \in V \setminus E(\sigma) \land \overline{v} \in E(\sigma') \land Clique\_Oracle_t(1, V, \sigma, p) \implies Clique\_Oracle_t(1, V, \sigma', p)
$$
### Lemma 36 (Clique oracles preserved over minimal transitions)
$\forall p \in P_{\mathcal{C}} : Majority\_Driven^H(p),$ $\forall (\sigma, \sigma') \in Minimal_t, \forall V \subseteq \mathcal{V}$, letting $\overline{m} = ~ !\sigma'\setminus\sigma$, and $\overline{v} = Sender(\overline{m})$,
$$
Clique\_Oracle_t(1, V, \sigma, p) \implies Clique\_Oracle_t(1, V, \sigma', p)
$$
### Lemma 37. if there is a clique, then everyone in the clique is agreeing in the current protocol state.
$\forall p \in P_{\mathcal{C}} : Majority\_Driven^H(p),$ $\forall (\sigma, \sigma') \in Minimal_t, \forall V \subseteq \mathcal{V}$
\begin{align}
Clique(1, V, p, \sigma) &\implies V \subseteq Agreeing(p, \sigma)
\end{align}
### Lemma 38.
$\forall p \in P_{\mathcal{C}} : Majority\_Driven^H(p),$ $\forall (\sigma, \sigma') \in Minimal_t, \forall V \subseteq \mathcal{V}$
\begin{align}
Clique(1, V \setminus E(\sigma), p, \sigma) \land Threshold_t(V \setminus E(\sigma), \sigma) &\implies \forall c \in \mathcal{E}(\sigma), p(c)
\end{align}
### Lemma 39 (Cliques exist in all futures).
$\forall p \in P_{\mathcal{C}} : Majority\_Driven^H(p), \forall \sigma \in \Sigma_t, \forall V \subseteq \mathcal{V}$,
$$
Clique\_Oracle_t(1, V, p, \sigma) \implies \forall \sigma' \in Futures_t(\sigma), Clique\_Oracle_t(1, V, p, \sigma')
$$
### Lemma 40 (Clique oracle is a safety oracle).
$\forall p \in P_{\mathcal{C}} : Majority\_Driven^H(p), \forall \sigma \in \Sigma_t, \forall V \subseteq \mathcal{V}$,
$$
Clique\_Oracle_t(1, V, p, \sigma) \implies Decided_{\mathcal{C},t}(p, \sigma)
$$
###### tags: `cbc` `casper` `cbc capser` `symbols`
0.3
5
8
?15?
2
4
1
2.5
2