owned this note
owned this note
Published
Linked with GitHub
# CBC Casper Explained (2/2)
<!--
> list: https://hackmd.io/4PFKtf-RR6GKk183mZvMLw
> 1/2: AbstracbCBC + CasperTFG
> 2/2: Introducing the “Minimal CBC Casper” Family of Consensus Protocols + Refinement and Verification of CBC Casper
> [Minimal CBC Casper Symbol / Terminology](https://hackmd.io/sDXKV1QRQcG-hJeV6kKpsQ)
-->
## 1. [Minimal CBC Casper](https://github.com/cbc-casper/cbc-casper-paper)
이전 포스트에서 proposition을 기반으로 두 검증자간의 consensus safety를 다뤘습니다. Minimal CBC Casper에서 다룰 내용은 다음과 같습니다.
1. 이전 포스트에서 다뤘던 "일관성"의 증명과 함께 노드의 protocol state를 기반으로 consensus value에 safety를 보장받을 수 있는 방법
2. 두 검증자간의 consensus safety를 다자간의 consensus safety로 확장
3. Latest Message Driven GHOST의 정의
정리의 증명들만 다루며, 보조정리의 증명은 해당 페이퍼를 참고하시기 바랍니다.
### 1.1 Consensus Safety
### 1.1.1 Common Notations (Terminology? Definitions?)
Minimal CBC Casper 페이퍼에서 사용하는 정의 / 보조정리 / 정리의 목록은 [여기](https://hackmd.io/sDXKV1QRQcG-hJeV6kKpsQ)서 확인하실 수 있습니다. 적어도 [Prerequisite Notation](https://hackmd.io/sDXKV1QRQcG-hJeV6kKpsQ?both#Prerequisite-Notation)은 사전에 한번 읽어보는 것을 강력히 권장드립니다.
1. 두 protocol state $\sigma_1, \sigma_2$간의 **transition**은 포함관계(improper subset)에 있습니다.
($\sigma_1 \to \sigma_2 :\Leftrightarrow \hspace{1mm} \sigma_1 \subseteq \sigma_2$)
2. Protocol message $m$의 estimate, sender, justification을 반환하는 함수는 각각 $Estimate(m), Sender(m), Justification(m)$ 입니다.
3. **Equivocating message**($Eq(m_1, m_2)$)는 $m_1 \perp m_2$로 표기합니다.
4. 이전 글의 Byzantine nodes($B(M)$)는 **equivocating validators**($E(\sigma)$)와 동일합니다.
($\sigma$는 protocol messages의 집합이기 때문에 $M$과 동일한 의미를 가집니다.)
5. 이전 글의 weight of byzantine faults($F(M)$)는 **equivocation fault weight**($F(\sigma)$)와 동일합니다.
$\sigma_1 \subseteq \sigma_2$이기 때문에 $F(\sigma_1) \leq F(\sigma_2)$ 입니다. (단조 함수)
6. $\sigma \in \Sigma_t$의 **모든 future states**를 반환하는 함수는 $Future_t(\sigma)$입니다.
7. 이전 글의 Propositions의 집합($Props(L_C): \mathcal{C} \to \{True, False\}$)은 **Properties of consensus values**($P_\mathcal{C}=\{True, False\}^\mathcal{C}$)와 동일합니다. $p \in P_\mathcal{C}$는 $p(0) = True$와 같이 특정 consensus value에 대하여 boolean을 반환하는 map(function)입니다.
8. **Properties of protocol states**($P_\Sigma=\{True, False\}^\Sigma$)는 Properties of consensus values에 대응하는 다른 집합입니다.
엄밀히 말하면 검증자의 protocol message를 이용하여 의사결정하는 노드는 검증자의 protocol state와 common future state가 존재할 경우 일관성이 보장된 의사결정을 내릴 수 있습니다. Minimal CBC Casper의 주된 주제 중 하나는 Properties of protocol states에 대하여 일관성을 증명한 후 이를 Properties of consensus value에서도 동일하게 일관성이 유지됨을 보이는 것입니다.
9. 앞서 논의한 property of consensus values와 property of protocol states는 대응관계에 있습니다. 즉, $p_\mathcal{C} \in P_\mathcal{C}, p_\Sigma \in P_\Sigma$에 대해 $p_\Sigma = H(p_\mathcal{C})$인 함수($H: P_\mathcal{C} \to P_\Sigma$)가 존재합니다. $H$를 **naturally corresponding property of protocol states**라고 부릅니다.
$H(p) :\Leftrightarrow \lambda \sigma . \forall c \in \mathcal{E}(\sigma), p(c)$이며 의사코드로는 다음과 같습니다.
```
function H(p):
return function (𝜎): // p_Sigma
for all c in estimator(𝜎):
if !p(c): return false
return true
```
binary consensus를 예로들면, property of consensus values $p \in P_{\{0, 1\}}$가 $p(0) = True, p(1) = False$일 때, $H(p)$는 임의의 $\sigma$에 대하여 아래 식을 만족하는 property of protocol state입니다.
\begin{align*}
H(p)(\sigma) &=
\begin{cases}
True & \text{if } \mathcal{E}(\sigma)=\{0\} \\
False & \text{otherwise}
\end{cases}
\end{align*}
<!-- TODO: estimate safety ~ property of protocol state -->
10. 이전 글의 Estimate safety($S(p, \sigma): p \in Props(L_C)$)는 *property of consensus value*에 대해하여 **결정된(decided)** 것과 동일합니다. ($Decided_{\mathcal{C}, t}: P_\mathcal{C} \times \Sigma_t \to Boolean$). 마찬가지로 *property of protocol state*에 대하여 **결정된** 것은 $Decided_{\Sigma, t}: P_\Sigma \times \Sigma \to Boolean$ 으로 표기합니다.
$Decided_{\mathcal{C}, t}, Decided_{\Sigma, t}$은 이전 글의 estimate safety의 정의와 마찬가지로 모든 future states에 대해서도 해당 property가 $True$일 경우에 성립합니다. 이들은 각각 이전 글의 보조정리 1, 3에 대응하는 forward cosnistency, backward consistency(Minimal CBC Casper의 보조정리 2, 3)를 가집니다.
$$
Decided_{\Sigma, t}(p, \sigma) :\Leftrightarrow \forall \sigma' \in Futures_t(\sigma), p(\sigma') \\
Decided_{\mathcal{C},t}(p, \sigma)= Decided_{\Sigma,t}(H(p), \sigma)
$$
11. 모든 future state에게 일관성을 가지는 *결정된* properties (of consensus values or of protocol states)들에 대해서 노드는 **의사결정(decision)** 을 할 수 있습니다. properties of protocol states에대해 *가능한 모든* 의사 결정($Decisions_{\Sigma,t}$)과 properties of consensus values에대해 *가능한 모든* 의사 결정($Decisions_{\mathcal{C},t}$)은 다음과 같습니다.
$$
Decisions_{\Sigma,t} : \Sigma \to \mathcal{P}(P_\Sigma) \\
Decisions_{\mathcal{C},t} : \Sigma_t \to \mathcal{P}(P_{\mathcal{C}}) \\
\\
Decisions_{\Sigma,t}(\sigma)= \{ p \in P_\Sigma: Decided_{\Sigma, t}(p,\sigma) \} \\
Decisions_{\mathcal{C},t}(\sigma) = \{q \in P_{\mathcal{C}}: H(q) \in Decisions_{\Sigma,t}(\sigma)\}
$$
다자간의 Consensus safety를 가진다는 것은 "consensus values에 대한 다자간의 의사결정이 일관성을 보이는 것"과 동일합니다. 하지만 그 전에 byzantine fault $t$ 이하일 때 common future state를 지는 것을 증명하는 것이 먼저입니다. 그 다음에 Common future state를 기반으로 다자간의 consensus safety까지 증명하도록 하겠습니다.
### 1.1.2 Common Futures
$\sigma \in \Sigma_t$의 **모든 future states**를 반환하는 함수는 $Future_t(\sigma)$입니다.
#### 보조정리 1: Monotonic futures
$$
\forall \sigma \in \Sigma_t, \forall \sigma' \in \Sigma_t, \\
\sigma' \in Futures_t(\sigma) \iff Futures_t(\sigma') \subseteq Futures_t(\sigma)
$$
이 보조정리는 future states가 존재할 수 있는 공간는 protocol execution을 거치면서 점점 줄어든다는 것(shrinking)을 의미합니다.
#### 정리 1: 2-party common futures
$$
\forall \sigma_1 \in \Sigma_t, \forall \sigma_2 \in \Sigma_t, \\
F(\sigma_1 \cup \sigma_2) \leq t \implies Futures_t(\sigma_1) \cap Futures_t(\sigma_2) \neq \emptyset
$$
![](https://i.imgur.com/Uklzsx1.png)
38번 라인의 "두 state의 합집합이 두 state의 future에 동일하게 포함된다"가 정리1 증명의 핵심입니다. 다르게 말하면, byzantine fault $t$ 이하일 경우 $\sigma_1, \sigma_2$는 적어도 $\sigma_1 \cup \sigma_2$를 future state로 가집니다.
#### 정리 2: $n$-party common futures
$$
\forall \sigma_i \in \Sigma_t, \\
F(\bigcup_{i=1}^n \sigma_i) \leq t \implies \bigcap_{i=1}^n Futures_t(\sigma_i) \neq \emptyset
$$
정리2의 증명은 위와 유사하기에 생략합니다.
위 정리들을 통해 다자간의 common future states는 byzantine fault $t$ 이하일 경우 언제나 존재하고, 적어도 $\bigcup_{i=1}^n \sigma_i$가 common future state 중 하나일 것입니다. 따라서 정직한 노드들은 common future state가 존재함을 가정하고 아래에서 다룰 일관성을 보장받을 수 있습니다.
### 1.1.3 Consistent Decisions (Consensus Safety)
Consensus Safety란 각 노드들이 내린 의사 결정이 일관성을 가진다는 것과 동일한 의미입니다.
우선 properties of protocol states의 일관성을 다룬 이후 이를 이용하여 properties of consensus values의 일관성을 논의하겠습니다.
#### 보조정리 2: Forward consistency
$$
\forall \sigma \in \Sigma_t, \forall \sigma' \in \Sigma_t, \forall p \in P_\Sigma, \\
\sigma' \in Futures_t(\sigma) \implies (Decided_{\Sigma, t}(p,\sigma) \implies Decided_{\Sigma, t}(p,\sigma'))
$$
#### 보조정리 3: Backward consistency
$$
\forall \sigma \in \Sigma_t, \forall \sigma' \in \Sigma_t, \forall p \in P_\Sigma, \\
\sigma' \in Futures_t(\sigma) \implies (Decided_{\Sigma, t}(p,\sigma') \implies \neg Decided_{\Sigma, t}(\neg p,\sigma))
$$
보조정리 1, 2는 이전 글의 보조정리 1, 3과 동일합니다.
#### 정리 3: 2-party consensus safety
$$
\forall \sigma_1 \in \Sigma_t, \forall \sigma_2 \in \Sigma_t, \forall p \in P_\Sigma, \\
F(\sigma_1 \cup \sigma_2) \leq t \implies \neg (Decided_{\Sigma, t}(p,\sigma_1) \land Decided_{\Sigma, t}(\neg p, \sigma_2))
$$
![](https://i.imgur.com/8ZruLtv.png)
정리3의 증명은 정리1의 "common future state의 존재성"으로 시작합니다. 그리고 $Decided_{\Sigma, t}$ (estimate safety)와 forward, backward consistency(보조정리 2, 3)를 이용합니다. 정리3은 이전 글의 consensus safety와 동일한 의미를 가집니다.
2-party consensus safety를 곧바로 n-party consensus safety로 확장할 수 없는 예를 생각해봅시다. 세 properties of protocol states $p, q, r$가 $p \land q \implies \neg r$일 때, 세 노드는 각각 $p, q, r$에 대해 결정할 수 있습니다. 그리고 세 pair $(p, q), (q, r), (r, q)$는 각각이 2-party consensus safety를 달성할 수 있을 것입니다. 하지만 triple $(p, q, r)$은 $p \land q \implies \neg r$이기 때문에 consensus safety를 가질 수 없습니다.
#### 정의 3.4: Inconsistency of properties of protocol states
$$ Inconsistent_\Sigma : \mathcal{P}(P_\Sigma) \to \{True, False\}\\
Inconsistent_\Sigma(Q): \Leftrightarrow \forall \sigma \in \Sigma, \bigwedge_{q \in Q} q(\sigma) = False
$$
#### 정의 3.5: Consistency of properties of protocol states
$$
Consistent_\Sigma : \mathcal{P}(P_\Sigma) \to \{True, False\}, \\
Consistent_\Sigma(Q): \Leftrightarrow \exists \sigma \in \Sigma, \forall q \in Q, ~ q(\sigma)
$$
위 두 정의는 properties($Q$)를 만족하는 $\sigma$가 존재하면 일관성을 가지고, 그렇지 않으면 일관성을 가지지 않음을 의미합니다.
따라서 각 노드들의 상태($\sigma_i$)에서 가능한 **모든 의사 결정**($Decisions_{\Sigma,t}(\sigma)= \{ p \in P_\Sigma: Decided_{\Sigma, t}(p,\sigma_) \}$)이 *일관성을 가질 때* 다자간의 consensus safety가 보장됩니다.
#### 정리 4: $n$-party consensus safety for properties of protocol states
$$
\forall \sigma_i \in \Sigma_t, \\
F(\bigcup_{i=1}^n \sigma_i) \leq t \implies Consistent_\Sigma(\bigcup_{i=1}^n Decisions_{\Sigma,t}(\sigma_i))
$$
![](https://i.imgur.com/09o3Q7v.png)
정리 4의 대우는 일관성이 없으면 byzantine fault가 $t$이상임을 의미합니다.
지금까지 논의한 것은 properties of protocol states에 대한 safety(consistency)입니다. 이를 이용하여 **properties of consensus (values)** 대한 safety까지 확장합니다.
#### 정의 3.9: Consistency of properties of the consensus
$$
Consistent_{\mathcal{C}} : \mathcal{P}(P_{\mathcal{C}}) \to \{True, False\}, \\
Consistent_{\mathcal{C}}(Q): \Leftrightarrow \exists c \in \mathcal{C}, \forall q \in Q, ~ q(c)
$$
$Consistent_{\mathcal{C}}$는 $Consistent_\Sigma$와 마찬가지로 모든 properties($Q$)를 만족시킬 수 있는 $c$의 존재성에 따라 결정됩니다.
#### 보조정리 4:
$$\forall p_i \in P_{\mathcal{C}}, \\
Consistent_\Sigma(\{H(p_1), H(p_2),\dots,H(p_n)\}) \implies Consistent_{\mathcal{C}}(\{p_1,p_2,\dots,p_n\})
$$
보조정리 4는 정리 4에서 다룬 properties of protocol states($p_i$)의 일관성을 그에 대응하는 properties of consensus values($H(p_i)$)으로 확장할 수 있음을 의미합니다.
#### 정리 5: $n$-party consensus safety for properties of the consensus
$$
\forall \sigma_i \in \Sigma_t, \\
F(\bigcup_{i=1}^n \sigma_i) \leq t \implies Consistent_{\mathcal{C}}(\bigcup_{i=1}^n Decisions_{\mathcal{C},t}(\sigma_i))
$$
![](https://i.imgur.com/emLwdui.png)
정리 5는 정리 4에 보조정리 4를 이용하여 $\Sigma$에 대한 $Consistent$, $Decisions$을 $\mathcal{C}$로 확장한 것입니다.
정리 5가 의미하는 것은 protocol states(a set of messages)의 conesnsus safety(정리 4)를 consensus value에 대한 의사결정에도
지금까지 다룬 내용을 다시한번 간략히 요약하자면, byzantine fault $t$ 이하일 경우 common futures가 언제나 존재하고, protocol states에 기반한 의사결정은 safety를 가지며, 이는 consensus values에 기반한 의사결정 또한 마찬가지로 safety를 가진다는 것입니다. 정리 4와 정리 5는 "byzantine fault $t$ 이하일 경우"를 전제하고 있기 때문에 이에 대한 대우를 생각해보면, "일관성이 보장되는 $Decisions$가 없을 경우 byzantine fault $t$ 초과"를 의미합니다.
Consensus safety는 safety를 가지는 estimate가 존재함을 보장합니다. 하지만 개별 노드가 $Decided_{\mathcal{C}, t}$, $Decided_{\Sigma, t}$를 계산하기 위해선 safety를 판별할 수 있는 oracle이 필요합니다. 이와 관련된 내용은 [여기](#2-Refinement-and-Verification-of-CBC-Casper)를 참조하십시오.
### 1.2 Example Protocols
Consensus safety를 가질 수 있는 프로토콜을 이더리움의 fork choice rule(GHOST)에 적용해 봅시다. 그 전에 estimate와 estimator를 정의하기 위한 몇가지 용어가 필요합니다.
- protocol state $\sigma$에서 **관찰된 검증자들(observed validartors)** 는 $Observed(\sigma) = \{ Sender(m) : m \in \sigma \}$ 입니다.
- protocol message $m$ **이후에 보내진 메시지들(later messages)** 는 $Later(m, \sigma) = \{m' \in \sigma : m \in Justification(m') \}$ 입니다.
- protocol message $m$을 **보낸 검증자(message from a sender)** 는 $From\_Sender(v, \sigma) = \{m \in \sigma : Sender(m) = v \}$ 입니다.
- protocol message $m$을 **보낸 검증자 집단(messages from a group)** 은 $From\_Group(V, \sigma) = \{m \in \sigma : Sender(m) \in V \}$ 입니다.
- **검증자 $v$가 $m$이후에 보낸 메시지들** 은 $Later\_From(m, v, \sigma) = Later(m, \sigma) \cap From\_Sender(v, \sigma)$ 입니다.
- 검증자 $v$가 $\sigma$에서 보낸 **최근 메시지(latest message)** 는 $L_M(\sigma)(v) = \{m \in From\_Sender(v, \sigma): Later\_From(m, v, \sigma) = \emptyset \}$ 입니다. 검증자 $v$가 보낸 최근 메시지는 $v$가 정직하다면 오직 1개만 존재합니다. (보조정리 5)
- **정직한 검증자 $v$가 $\sigma$에서 보낸 최근 메시지들(latest messages from non-equivocating validators)** 는
$$
L^H_M(\sigma)(v) = \left\{ \begin{array}{ll} \emptyset \text{ for } v \in E(\sigma) \\ L_M(\sigma)(v) \text{ otherwise } \end{array} \right.
$$
입니다.
- 검증자 $v$가 $\sigma$에서 보낸 **최근 estimate(latest estimate)** 는 $L_E(\sigma)(v) = \{Estimate(m): m \in L_M(\sigma)(v)\}$ 입니다. 즉, latest messages의 estimate입니다.
- **정직한 검증자 $v$가 $\sigma$에서 보낸 최근 estimate(latest estimates from non-equivocating validators)** 는 $L^H_E(\sigma)(v) = \{Estimate(m) : m \in L^H_M(\sigma)(v)\}$ 입니다.
- 두 protocol messages $m_1, m_2$의 justification의 사이즈를 비교한 것을 $m_1 \preceq m_2 :\Leftrightarrow |Justification(m_1)| \geq |Justification(m_2)|$라고 합니다. $\preceq$는 두 메시지를 비교하기 위한 연산으로, $(S, \preceq)$가 [total order](https://en.wikipedia.org/wiki/Total_order)임을 보조정리 6에서 보입니다. (Total order는 간략히 설명하면 $(\mathbb{N}, \geq)$와 같이 임의의 두 자연수는 $\geq$ 연산을 통해 대소비교가 가능한 집합입니다.)
- 집합 $X$에 함수 $f$를 적용한 가장 큰 원소들을 반환하는 함수 $Argmax$는 $Argmax(X, f) = \{x \in X : \nexists x' \in X, f(x') > f(x)\}$ 입니다. 편의를 위해 $\underset{x\in X}{\operatorname{argmax} f(x)}$로 표기합니다.
- genesis 블록 $g$와 블록 데이터 $D$에 대하여, **n 번째 블록 $B_n$과 모든 블록 $B$** 은 다음과 같습니다.
\begin{align*}
B_0 &= \{g\} \\
B_n &= B_{n-1} \times D \\
B &= \bigcup_{i = 0}^{\infty} B_i
\end{align*}
- **이전 블록(부모 블록)을 반환하는 함수** $Prev$는 다음과 같습니다.
$$
Prev(b) = \begin{cases}
g &\text{ if $b = g$ }\\
b' &\text{ otherwise, if $b = (b', d)$ }\\
\end{cases}
$$
유사하게 블록 $b$의 **n번째 부모 블록을 반환하는 함수** $n\text{-}cestor$는 다음과 같습니다.
\begin{align*}
n\text{-}cestor(b, n) = \left\{
\begin{array}{ll}
b& \text{ if $n = 0$ } \\
n\text{-}cestor(Prev(b), n - 1)& \text{ otherwise }
\end{array}
\right.
\end{align*}
- 블록 $b_2$가 블록 $b_1$을 포함했을 때 $b_1 \downharpoonright b_2$로 표기하며, 정의는 다음과 같습니다.
\begin{align*}
b_1 \downharpoonright b_2 &:\Leftrightarrow \exists n \in \mathbb{N}, b_1 = n\text{-}cestor(b_2, n)
\end{align*}
### 1.2.1 Casper the Friendly GHOST (Latest Message Driven)
이 예시는 CBC Casper 방식을 Greedy Heaviest Observed Sub-Tree fork choice rule(GHOST)에 latest message를 기반으로 적용한 것입니다. 이전 포스트와 마찬가지로 추상적인 CBC 방식을 적용하는 것은 결국 올바른 estimator를 정의하는 것과 다르지 않습니다.
#### 정의 4.27: Score of a block
$$
Score(b, \sigma) = \sum_{v \in \mathcal{V} : \exists b' \in L^H_E(\sigma)(v), b \downharpoonright b'} \mathcal{W}(v)
$$
$\sigma$에서 $b$의 점수는 "$b$를 포함하는 latest estimate($b'$)를 보낸 정직한 검증자 $v$의 weight의 합" 이라고 할 수 있습니다. 여기서 주목할 점은 블록의 점수를 계산하기 위해서 **latest estimate**(latest message)을 사용했다는 점입니다.
#### 정의 4.28: Children of a block
$\sigma$에서 $b$의 자식 블록들을 반환하는 함수 $Children$은 다음과 같습니다.
$$
Children(b,\sigma) = \{b' \in \bigcup_{m \in \sigma} \{Estimate(m)\} : Prev(b') = b\}
$$
#### 정의 4.28: Best Children of a block
Best children은 가장 높은 점수를 가진 자식 블록들입니다.
$$
Best\_Children(b,\sigma) = \underset{b' \in Children(b, \sigma)}{\operatorname{argmax} Score(b', \sigma)}
$$
#### 정의 4.30: GHOST
따라서 $\sigma$에서 블록체인 $\underline{b}$의 fork choice rule을 수행한 결과인 "점수가 가장 높은 head 블록들"은 다음과 같습니다. 여기서 $\underline{b}$는 블록체인이기 때문에 "블록들의 집합"을 의미합니다.
$$
GHOST(\underline{b},\sigma) = \bigcup\limits_{\substack{b \in \underline{b} ~:\\ Children(b, \sigma) \neq \emptyset}} GHOST(Best\_Children(b,\sigma), \sigma) \\
~~~\cup \bigcup\limits_{\substack{b \in \underline{b} ~:\\ Children(b, \sigma) = \emptyset}} \{b\}
$$
위 수식을 풀어 설명하면 다음과 같습니다. "블록체인 $\underline{b}$에 포함된 각 블록 $b$은 1) $b$가 자식 블록이 있을 경우 재귀적으로 $Best\_Children(b, \sigma)$에 대하여 $GHOST$를 다시 적용하고, 2) 그렇지 않을 경우 $b$ 자기 자신을 반환한다." 입니다. 따라서 $GHOST(\underline{b},\sigma)$는 $\underline{b}$에서 점수가 가장 높은 head 블록들입니다.
#### 정의 4.31: Casper the Friendly GHOST
Casper the Friendly GHOST의 estimator는 genesis block $g$에 대하여 $GHOST$를 적용한 것과 동일합니다.
$$
\mathcal{E}(\sigma) = GHOST(\{g\}, \sigma)
$$
### 1.2.2 Casper the Friendly CBC Finality Gadget
Finality gadget은 PoW와 같은 underlying blockchain 위에서 동작하는 합의 프로토콜입니다. Finality gadget을 적용함으로써 genesis block이 아니라 finality gadget이 제공하는 finalized block에서 underlying blockchain의 fork choice rule을 적용하게 됩니다. 이번 예시에서는 CBC Casper 방식을 통해 finality gadget을 구성하겠습니다.
Underlying blockchain의 블록 $B$, 이전 블록 $Prev$, n 번째 조상 $n\text{-}cestor$, 블록체인 포함관계 $b_1 \downarrow b_2$는 이전 정의와 동일합니다.
- $Height$은 블록 $b$의 높이를 반환하는 함수입니다.
\begin{align*}
Height(b) &= \begin{cases}
\text{$0$} &\text{if $b = g$} \\
\text{$1 + Height(Prev(b))$} &\text{otherwise}
\end{cases}
\end{align*}
- Fork choice rule $\mathcal{F}$는 "시작 블록"과 "블록체인(블록들)"을 인자로 받고 "head 블록"을 반환하는 함수입니다. ($\mathcal{F}: B \times \mathcal{P}(B) \to B$).
#### 정의 4.38: Consensus values in the CBC Finality Gadget
CBC Finality Gadget에서는 Casper FFG와 마찬가지로 epoch의 checkpoint 블록을 기준으로 의사결정을 내립니다. 따라서 자연수 $Epoch\_Length \in \mathbb{N}_+$에 대하여, consensus values $\mathcal{C}$는 다음과 같습니다.
$$
\mathcal{C} = \{b \in B : Height(b) \equiv 0 \pmod{Epoch\_Length}\}
$$
[1.2.1 Casper the Friendly GHOST](#121-Casper-the-Friendly-GHOST-Latest-Message-Driven0)에서 사용한 Score, Children, Best_Children, GHOST들을 블록이 아닌 에퍽에 대하여 재정의 해야 합니다. $Score\_Epoch$, $Children\_Epochs$, $Best\_Children\_Epochs$은 단순히 consensus values만 모든 블록 $B$에서 checkpoint 블록으로 달라진 것이므로 자세한 설명은 생략합니다.
#### 정의 4.42: GHOST on epochs
$$
GHOST(\underline{b},\sigma) = \bigcup\limits_{\substack{b \in \underline{b} ~:\\ Children\_Epochs(b, \sigma) \neq \emptyset}} GHOST(Best\_Children\_Epochs(b,\sigma), \sigma) \\
~~~\cup \bigcup\limits_{\substack{b \in \underline{b} ~:\\ Children\_Epochs(b, \sigma) = \emptyset}} \{b\}
$$
#### 정의 4.43: Estimator for the CBC Finality gadget
$$
\mathcal{E}(\sigma) = \{ b \in \mathcal{C}: \exists b' \in GHOST(\{g\}, \sigma), b' \downharpoonright b \}
$$
GHOST 또한 모든 블록 $B$가 아닌 checkpoint 블록을 대상으로 수행하기에 동일한 로직을 가집니다.
#### 정의 4.43: Fork Choice Rule for the CBC Finality gadget
$$
\mathcal{F}(\mathcal{E}(\sigma), \underline{b}))
$$
기존의 fork choice rule은 $\mathcal{F}(\{g\}, \underline{b})$ 이었습니다. Fork choice를 시작하는 블록을 CBC Casper의 estimator를 적용한 것으로, CBC 검증자들이 합의한 블록은 finalized된 것을 의미합니다.
<!-- 따라서 fork choice rule에 의해 선택된 블록체인 $\underline{B}$에 포함된 블록 $b$은 $\forall b \in B, \forall \underline{B} \in \mathcal{P}(B), b \downharpoonright \mathcal{F}(b, \underline{B})$ 을 만족합니다. -->
## 2. [Refinement and Verification of CBC Casper](https://eprint.iacr.org/2019/415.pdf)
Refinement and Verification of CBC Casper는 Minimal CBC Casper를 개선하고 Safety와 Liveness를 보다 엄밀히 증명하였습니다. 특히 Isabelle/HOL을 이용하여 formal verification을 구현한 결과를 [LayerXcom/cbc-casper-proof](https://github.com/LayerXcom/cbc-casper-proof)에서 확인할 수 있습니다.
### 2.1 Safety Oracle
이전 포스트에서 언급했던 simple clique oracle의 정의 및 clique 내부의 검증자들이 정말 safety를 올바르게 판별할 수 있는지는 엄밀히 증명하지 않았습니다. Minimal CBC Casper 또한 증명을 생략한 상태이고 얻을 수 있는 자료는 오랜기간 병합되지 않은 [cbc-casper/cbc-casper-paper#13](https://github.com/cbc-casper/cbc-casper-paper/pull/13)뿐입니다. 논리상 문제가 있는 부분은 아직 발견되지 않았으며 사소한 오탈자와 용어정리 측면에서는 변경의 여지가 있음을 감안하고 살펴보도록 하겠습니다.
(보조정리가 많이 사용되는 관계로 결론을 내기위해 필요한 보조정리를 위주로 살펴봅니다. 모든 정의 및 보조정리 목록은 [여기](/sDXKV1QRQcG-hJeV6kKpsQ#-Safety-Oracle)서 확인할 수 있습니다.)
#### 2.1.1 Definitions
- **Latest justifications from non-Equivocating validators**:
$$
L^H_J(\sigma)(v) = \{Justification(m) : m \in L^H_M(\sigma)(v)\}
$$
정직한 검증자 $v$의 $\sigma$에서의 최신 메시지 $m$의 justification입니다.
- **Validators agreeing with p in σ**:
$$
Agreeing(p, \sigma): \Leftrightarrow \{v \in \mathcal{V} : \forall c \in L^H_E(\sigma)(v), p(c)\}
$$
이전 포스트에서 논의했던 "$p$에 동의하는 검증자"들의 집합입니다. 검증자 $v$는 $\sigma$에서의 모든 latest estimates가 $p$에 대해 참일 경우 "$p$에 동의"합니다.
- **Validators disagreeing with p in σ**:
$$
Disagreeing(p, \sigma) :\Leftrightarrow \{v \in \mathcal{V} : \exists c \in L^H_E(\sigma)(v), \neg p(c)\}
$$
이전 포스트에서 논의했던 "$p$에 반대하는 검증자"들의 집합입니다. 동의하는 검증자들($Agreeing(p, \sigma)$), 반대하는 검증자들($Disagreeing(p, \sigma)$), equivocating하는 검증자들($E(\sigma)$)는 서로 겹치지 않습니다. (mutually disjoint)
- **Weight measure**:
$$
Weight(V) :\Leftrightarrow \sum_{v \in V} \mathcal{W}(v)
$$
검증자 집단의 총 weight의 합을 반환하는 함수입니다.
- **Non-equivocating majority**:
$$
Majority^H(V, \sigma) :\Leftrightarrow Weight(V) > Weight(\mathcal{V} \setminus E(\sigma))/2
$$
이전 포스트에서 "**clique에 속한 검증자들의 총 weight이 모든 검증자의 weight의 1/2보다 클 때** clique 내부 혹은 외부의 새로운 메시지가 estiamte의 score를 변경시키지 않는다"고 했습니다. 위 문장의 선행 조건을 $Majority^H(V, \sigma)$로 표기합니다.
- **Non-equivocating majority driven property**:
$$
Majority\_Driven^H(p) :\Leftrightarrow \forall \sigma \in \Sigma, Majority^H(Agreeing(p, \sigma), \sigma) \implies \forall c \in \mathcal{E}(\sigma), p(c)
$$
$\forall p \in P_C: Majority\_Driven^H(p)$는 모든 $\sigma \in \Sigma$에 대하여 $\neg Majority^H(Agreeing(p, \sigma)) \lor Majority^H(Agreeing(p, \sigma)) \land \forall c \in \mathcal{E}(\sigma), p(c)$일 것입니다. 따라서 $Majority\_Driven^H$는 $Majority^H$가 참이라면 "다수가 동의하는 $Decided_{C, t}$될 수 있는 $p$의 집합"는 의미로 해석할 수 있습니다.
- **Max weight driven property**:
$$
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)
$$
$Majority\_Driven^H$과 유사합니다. 특히 $\mathcal{V} \setminus Agreeing(p, \sigma) \setminus Disagreeing(p, \sigma) \setminus E(\sigma) = \emptyset$ 인 $\sigma$ (메시지를 보내지 않은 검증자가 없을 경우) 에서는 $Majority\_Driven^H$와 동일한 의미를 가집니다.
- **Later disagreeing messages**:
$$
Later\_Disagreeing(p,m,v,\sigma) = \{m' \in Later\_From(m, v, \sigma) : \neg p(Estimate(m')) \}
$$
$\sigma$에서 메시지 $m$이후로 검증자 $v$가 보낸 $p$에 반대하는 메시지들의 집합입니다.
- **helper function(!) := "!({a}) = a"**:
$$
!: \mathcal{P}(X) \to X\\
!(A) = a \in A : \forall b \in A, b = a
$$
$!$ 함수는 크기가 1인 집합에서 유일하게 존재하는 해당 원소를 반환하는 함수입니다. 크기가 1보다 크거나 0일때는 정의되지 않습니다. $!$는 $L^H_M, L^H_E$와 같은 정직한 노드의 최신 메시지(혹은 estimate)는 1개만 있기 때문에 해당 메시지(혹은 estimate)를 선택하기 위해 사용됩니다.
- **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(n - 1, V, p, L^H_J(\sigma)(v))
\end{align}
$n = 1$일 때를 1-layer clique라고 합니다. 1-layer clique의 정의는 이전 포스트와 동일하게 "상호 동의" 하였고, 이후에 "반대하지 않는" 검증자들 입니다.
$n > 1$일 경우 재귀적으로 $\sigma$에서 $L_J^H(\sigma)(v)$로 protocol state를 대상으로 clique를 확인하며, $n$-layer clique라고 합니다.
![](https://i.imgur.com/BMknvLb.png)
위 그림에서 실선은 부모 블록 참조를, 점선은 메시지 justification을 의미합니다. 이 때, 검증자 A, C, D가 2번째로 보낸 파란색 블록들의 justification은 빨간 블록들을 포함하고 있다는 사실에 주목하십시오. 그리고 빨간 블록들은 (암시적으로) 검증자 A가 처음으로 보낸, 가장 왼쪽의 빨간 블록을 justification으로 포함하고 있습니다. 1-layer clique는 가장 왼쪽 블록에 대한 clique를 형성하기 위하여 파란 블록들(latest estimates)과 그의 justificatoin (latest justification)에 대한 "$Agreeing$과 $Later\_Disagreeing$".을 이용하고 있습니다.
검증자 A, B, C, D가 각각 $\sigma_A, \sigma_B, \sigma_C, \sigma_D$에 있을 때, $V = \{A, C, D\}$는 $\sigma = \sigma_A \cup \sigma_B \cup \sigma_C \cup \sigma_D$에서 "검증자 A가 보낸 첫번째 블록이 fork choice rule의 올바른 결과이다" 라는 $p$에 대하여 clique를 형성하는 과정은 다음과 같습니다.
$v \in V$에 대하여 $L_J^H(\sigma)(v)$는 모든 빨간 블록들입니다. 빨간 블록들은 A의 n번째 자식블록이기에, $p$를 만족합니다. 따라서 $V \subseteq Agreeing(p, L_J^H(\sigma)(v))$를 만족합니다.
또한 $L_M^H(L_J^H(\sigma)(v))(v')$는 검증자가 보낸 각각의 빨간 블록들입니다. 파란 블록은 빨간 블록 이후의 메시지이며 $p$를 반대하지 않습니다. 따라서 $Later\_Disagreeing(p, L_M^H(L_J^H(\sigma)(v))(v'), v', \sigma) = \emptyset$을 만족합니다.
- **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' \}
$$
Minimal transitions는 future state $\sigma'$로 곧바로 전이할 수 있는 transition입니다. 앞으로 다룰 "letting $\overline{m} =~!\sigma'\setminus\sigma$ and $\overline{v} = Sender(\overline{m})$" 이란 표현은 minimal transition $(\sigma, \sigma')$을 일으킨 새로운 매시지 $\overline{m}$와 그를 보낸 검증자 $\overline{v}$를 가리킵니다.
- **One layer clique oracle threshold size**:
\begin{align}
Threshold_t(V, \sigma) &:\Leftrightarrow Weight(V) > Weight(\mathcal{V})/2 + t - Weight(E(\sigma))
\end{align}
이전 포스트에서 다뤘던 "$e$-clique in $M$이 안전하기 위한 검증자들의 weight의 합의 최소값"입니다. 이는 byzantine fault $t$와 다른 값입니다. $Threshold_t(V, \sigma)$는 $Majority^H(V, \sigma)$ 보다 더 큰 값에 대하여 비교하고 있습니다. ($Weight(\mathcal{V})/2 + t - Weight(E(\sigma)) > Weight(\mathcal{V} \setminus E(\sigma))/2$) 따라서 $Threshold_t(V, \sigma)$ 이면 $Majority^H(V, \sigma)$ 입니다. ([보조정리 32](/sDXKV1QRQcG-hJeV6kKpsQ#Lemma-32))
- **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}
마지막으로 clique와 $Threshold_t$를 동시에 충족하는 할 경우 $Clique\_Oracle$이 safe하다고 정의합니다. 2.1은 $Clique\_Oracle$가 $\overline{v}$의 새로운 메시지 $\overline{m}$에 대하여 safe한지 아닌지 증명하는 것이 목적입니다.
이제 clique의 **내부 혹은 외부** 검증자가 보낸 새로운 메시지 $\overline{m}$가 clique를 새로운 $\sigma'$와 기존 검증자 집단 $V$에 대하여 그대로 유지할 수 있음을 살펴봅시다.
#### 2.1.2 Cliques Survive Messages from Validators Outside Clique
#### 보조정리 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')
$$
<!-- ![](https://i.imgur.com/Y260Y2V.png) -->
[보조정리 11](https://hackmd.io/sDXKV1QRQcG-hJeV6kKpsQ#Lemma-11-Minimal-transitions-do-not-change-Later-From-for-any-non-sender)부터 [보조정리 15](https://hackmd.io/sDXKV1QRQcG-hJeV6kKpsQ#Lemma-15-Minimal-transitions-do-not-change-Later-Disagreeing-for-any-non-sender)는 minimal transition을 일으킨 검증자를 제외한 *다른 검증자들*의 다양한 특성들(later, equivocation status, latest message, latest justification, later disagreeing)을 변경시키지 않음을 보입니다. 이를 이용하여 [보조정리 16](#%EB%B3%B4%EC%A1%B0%EC%A0%95%EB%A6%AC-16-Minimal-transition-from-outside-clique-maintains-clique)을 증명할 수 있습니다.
이 보조정리는 clique *외부의* 검증자들이 보낸 새로운 매시지들은 clique를 바꾸지 못한다는 의미입니다. **따라서 외부 검증자들의 equivocating 여부와 관계 없이 clique는 항상 유효할 것입니다.**
다음으로는 clique *내부의* 검증자들이 보낸 새로운 메시지들에 대하여 clique가 보존될 수 있는지 살펴봅시다. 경우를 나누자면 서로가 동의함을 확인한 clique 내부 검증자들은 새로운 메시지를 보낸 검증자가 1) non-equivocating 하거나 2) equivocating 하거나 둘 중 하나일 것입니다.
#### 2.1.3 Cliques Survice Messages from Validators Inside Clique
이 항목에서 논의할 내용은 다음 순서로 구성됩니다.
1. ([보조정리 17](/sDXKV1QRQcG-hJeV6kKpsQ#Lemma-17-Free-sub-clique)): 우선 새로운 메시지와 clique에 속한 검증자 집합간의 관계에 대해서 다룹니다.
2. ([보조정리 18](/sDXKV1QRQcG-hJeV6kKpsQ#Lemma-18-Later-messages-from-a-non-equivocating-validator-include-all-earlier-messages) ~ [보조정리 23](/sDXKV1QRQcG-hJeV6kKpsQ#Lemma-23-Non-equivocating-messages-from-clique-members-see-clique-agree)): clique 내부의 정직한(non-equivocating) 검증자 $\overline{v}$가 보낸 새로운 메시지 $\overline{m}$는 검증자 집단 $V$이 $Justification(\overline{m})$에 대한 동의를 암시합니다.
($V \subseteq Agreeing(p, Justification(\overline{m}))$)
3. ([보조정리 24](/sDXKV1QRQcG-hJeV6kKpsQ#Lemma-24-New-messages-from-majority-clique-members-agree)): **Majority** clique 내부의 정직한(non-equivocating) 검증자 $\overline{v}$가 보낸 새로운 메시지 $\overline{m}$는 $\overline{v}$가 $\sigma'$에서 $p$에 대해 동의합니다.
($\overline{v} \in Agreeing(p, \sigma')$)
4. ([보조정리 25](https://hackmd.io/sDXKV1QRQcG-hJeV6kKpsQ?view#Lemma-25) ~ [보조정리 31](/sDXKV1QRQcG-hJeV6kKpsQ#Lemma-31-New-non-equivocating-latest-messages-from-members-of-majority-clique-don%E2%80%99t-break-the-clique)): 2, 3번을 확장하여 **Majority** clique 내부의 *정직한(non-equivocating)* 검증자 $\overline{v}$가 보낸 새로운 메시지 $\overline{m}$는 clique를 $\sigma'$에서 여전히 유효합니다.
5. ([보조정리 32](/sDXKV1QRQcG-hJeV6kKpsQ#Lemma-32) ~ [보조정리 36](https://hackmd.io/sDXKV1QRQcG-hJeV6kKpsQ?view#Lemma-36-Clique-oracles-preserved-over-minimal-transitions)): clique 에 속한 검증자가 보낸 새로운 메시지 $\overline{m}$이 *equivocating 하더라도* clique는 보존됩니다.
<!--
17 New messages at least leaves a smaller clique behind
-
18-23 Non-equivocating messages from clique members see clique agree
- clique 멤버의 메시지 -> clique의 동의
- 새로운 메시지 -> clique 멤버들도 여전히 동의
24 Non-equivocating messages from majority clique members agree
- majority clique 멤버의 메시지 -> member의 동의
- 새로운 메시지 + majority member -> overline{v}도 여전히 동의
25-31 Honest messages from majority clique members do not break the clique
-
32-36 Equivocations from Validators in Clique do not break cliques
-
-->
#### 2.1.3.1 [보조정리 17](/sDXKV1QRQcG-hJeV6kKpsQ#Lemma-17-Free-sub-clique)
<!-- 17 New messages at least leaves a smaller clique behind -->
#### 보조정리 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')
$$
이 보조정리는 $\overline{v}$의 새로운 메시지 $\overline{m}$는 적어도 $V \setminus \{\overline{v}\}$로 이루어진 새로운 clique를 생성한다는 의미입니다. 물론 $\overline{m}$가 $Agreeing(p, L^H_J(\sigma')(\overline{v}))$를 동일하게 유지한다면, 검증자 집합은 새로운 clique에서도 동일합니다.
<!-- 18-23 Non-equivocating messages from clique members see clique agree -->
#### 2.1.3.2 [보조정리 18](/sDXKV1QRQcG-hJeV6kKpsQ#Lemma-18-Later-messages-from-a-non-equivocating-validator-include-all-earlier-messages) ~ [보조정리 23](/sDXKV1QRQcG-hJeV6kKpsQ#Lemma-23-Non-equivocating-messages-from-clique-members-see-clique-agree)
#### 보조정리 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}
보조정리 20은 크게 두가지 경우로 나누어져 있습니다. $\overline{v}$가 $v$의 새로운 메시지를 발견했을 때, 이를 $New$ 라고 한다면, $New = \emptyset$ 혹은 $New \neq \emptyset$ 인 두 가지 경우로 나뉩니다. 이 두 경우들이 $\lor$로 해당 보조정리에서 연결되어 있습니다.
#### 보조정리 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}))
$$
보조정리 20에 따르면, $Justification(\overline{m})$을 통해 $\overline{v}$가 $v$의 새로운 메시지를 확인했는지 아닌지에 따라 경우가 나뉘었습니다. 이 두 경우를 clique의 정의 각각과 연결지어 증명합니다. 첫 번째 경우($New = \emptyset$)엔 clique의 정의 "clique에 속한 검증자들은 서로가 동의함을 확인함"를 이용합니다. 두 번째 경우($New \neq \emptyset$)엔 clique의 정의 "이후에 disagreeing 하지 않음"을 이용합니다.
<!-- ![](https://i.imgur.com/GcRhQLj.png) -->
<!-- -->
<!-- ![](https://i.imgur.com/l7DnRuC.png) -->
보조정리 23은 $Justification(\overline{m})$에 대해서 clique가 동의함을 보이고 있습니다. 그러나 $Justification(\overline{m})$은 어디까지나 과거 메시지입니다. 새로운 프로토콜 상태인 $\sigma'$로 확장하는 것은 보조정리 24에서 다룹니다.
<!-- 24 Non-equivocating messages from majority clique members agree -->
#### 2.1.3.3 [보조정리 24](/sDXKV1QRQcG-hJeV6kKpsQ#Lemma-24-New-messages-from-majority-clique-members-agree)
#### 보조정리 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}
이전 포스트에서 "(t=0임을 가정하면) clique에 속한 검증자의 weight의 합이 전체 검증자의 weight의 1/2보다 클 때" clique oracle이 secure하다고 했습니다. 따라서 이 보조정리는 $Majority^H(V, !L_J^H(\sigma)(v))$를 함께 가정하고 있습니다 (majority clique). 이는 곧, $\forall p \in P_C: Majority\_Driven^H(p)$가 $!L_J^H(\sigma)(v)$에서 항상 성립한다는 것을 의미합니다.
이 보조정리의 증명은 보조정리 23에서 시작하여, 1) $Justification(\overline{m}) \supseteq !L_J^H(\sigma)(v)$과 $E$의 단조성(monotonicity), 2) $Majority\_Driven^H(p)$의 정의, 3) 보조정리 22를 이용합니다.
<!-- ![](https://i.imgur.com/bNMI4NX.png) -->
<!-- ![](https://i.imgur.com/UyjLH3g.png) -->
<!-- 보조정리 24를 통해 majority cliques의 $\overline{v}$이 새로운 프로토콜 상태 $\sigma'$에서 $p$에 대해 동의함을 확인 했습니다. 이제 다음으로 $\sigma'$에서 $V \setminus \{\overline{v}\}$
-->
<!-- 25-31 Honest messages from majority clique members do not break the clique -->
#### 2.1.3.4 [보조정리 25](https://hackmd.io/sDXKV1QRQcG-hJeV6kKpsQ?view#Lemma-25) ~ [보조정리 31](/sDXKV1QRQcG-hJeV6kKpsQ#Lemma-31-New-non-equivocating-latest-messages-from-members-of-majority-clique-don%E2%80%99t-break-the-clique)
#### 보조정리 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}
이 보조정리는 보조정리 17를 $\overline{v}$까지 확장했습니다. 증명을 위해 clique의 정의(상호 동의, 이후 반대 없음)를 $\overline{v}$와 $V \setminus \{\overline{v}\}$ 간의 포함관계에 따라 5가지 경우로 나누어 증명하였습니다.
\begin{align}
\textbf{1:} & \forall v \in \{\overline{v}\}, &V \subseteq Agreeing(p, !L^H_J(\sigma')(v)) \\
\textbf{2:} & \forall v \in V \setminus \{\overline{v}\}, &\{\overline{v}\} \subseteq Agreeing(p, !L^H_J(\sigma')(v)) \\
\textbf{3:} & \forall v \in \{\overline{v}\}, \forall v' \in \{\overline{v}\}, & Later\_Disagreeing(p,~!L^H_M(!L^H_J(\sigma')(v))(v'), v', \sigma') = \emptyset \\
\textbf{4:} & \forall v \in \{\overline{v}\}, \forall v' \in V \setminus \{\overline{v}\}, & Later\_Disagreeing(p,~!L^H_M(!L^H_J(\sigma')(v))(v'), v', \sigma') = \emptyset \\
\textbf{5:} & \forall v \in V \setminus \{\overline{v}\}, \forall v' \in \{\overline{v}\}, & Later\_Disagreeing(p,~!L^H_M(!L^H_J(\sigma')(v))(v'), v', \sigma') = \emptyset
\end{align}
이제 clique의 내부 혹은 외부에서 발생한 정직한 메시지에 한해서 clique는 보존될 수 있습니다. 앞으로는 clique 내부에서 발생한 equivocations을 확인 해 봅시다.
<!-- 32-36 Equivocations from Validators in Clique do not break cliques -->
#### 2.1.3.5 [보조정리 32](/sDXKV1QRQcG-hJeV6kKpsQ#Lemma-32) ~ [보조정리 36](https://hackmd.io/sDXKV1QRQcG-hJeV6kKpsQ?view#Lemma-36-Clique-oracles-preserved-over-minimal-transitions)
Equovication 한 검증자는 clique의 정의(상호 동의)에 따라 clique에 *속할 수 없습니다*. 따라서 clique의 검증자 집단은 해당 minimal transition으로 인해 $V \setminus \{\overline{v}\}$으로 변경될 수 밖에 없습니다. 따라서 우리는 clique 검증자 집단의 weight의 총 합은 $Weight(\{\overline{v}\})$만큼 줄어듬에도 불구하고, **clique oracle이 유효할 수 있는지**를 주목해야 합니다.
보조정리 33부터 35는 clique oracle이 minimal transition에 대하여 33) 검증자가 clique 외부에 있을 때 34) 검증자가 내부에서 non-equivocating 할 때 35) 검증자가 내부에서 equivocating 할 때로 나누어 증명 합니다. 그리고 이 세개의 보조정리를 취합하여 보조정리 36을 증명합니다. 보조정리 33, 34는 기존의 보조정리 16, 31에 대응합니다. 따라서 이번엔 equivocation을 다루는 보조정리 35에 집중합니다.
#### 보조정리 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)
$$
clique oracle의 정의는 $Clique(n, V \setminus E(\sigma), \sigma, p) \land Threshold_t(V \setminus E(\sigma), \sigma)$ 입니다. $\sigma'$에서의 두 조건($Clique, Threshold_t$)의 유효성을 다음의 방식으로 증명합니다.
1. $V \setminus E(\sigma)$는 $\sigma'$에서 $V \setminus E(\sigma')$가 됩니다. $\overline{v}$가 기존의 clique 검증자 집단에서 제외됩니다. $E(\sigma) = E(\sigma') \cup \{\overline{v}\}$ 이기 때문에 기존의 정직한 검증자들로 유효한 clique를 형성할 수 있습니다.
2. 마찬가지로 $V \setminus E(\sigma') = V \setminus E(\sigma) \setminus \{\overline{v}\}$ 입니다. $Weight(V \setminus E(\sigma)) - Weight(V \setminus E(\sigma'))$와 $E(\sigma) - E(\sigma')$는 같기 때문에 동일하게 $\sigma'$에서 $Threshold_t$를 만족합니다. (동일하게 $W(\overline{v})$만큼 감소합니다.)
#### 보조정리 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)
$$
보조정리 33, 34, 35을 이용하여 증명합니다.
### 2.2 Clique Oracle Is A Safety Oracle
지금까지 clique oracle의 검증자 집단 내부 혹은 외부에서의 새로운 메시지의 equivocation 여부와 관계 없이 항상 clique oracle이 보존된다는 것을 살펴봤습니다. 이렇게 항상 유지되는 clique oracle을 이용하여 consensus safety를 적용할 수 있는 $Decided_t$를 판별할 수 있는지, 다르게 표현하면, **clique oracle이 safe oracle인지** 살펴보겠습니다.
#### 보조정리 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}
clique의 검증자 $v \in V$는 clique의 정의에 따라 $v'$이 $Later\_Disagreeing(p, L^H_M(L^H_J(\sigma)(v))(v'), v', \sigma) = \emptyset$인지 서로 확인했습니다. 증명에는 이것이 사용됩니다.
#### 보조정리 38: if there is a threshold sized clique where no validators are equivocating, then the estimator will agree.
$\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}
$Majority\_Driven^H(p)$의 정의에 따르면 다수가 $p$에 동의하면 ($Majority^H(Agreeing(p, \sigma), \sigma)$) estimator 또한 동의합니다. 보조정리 37에 의하여 이 검증자들은 $Agreeing(p, \sigma)$에 포함됩니다.
1. $Threshold_t(V \setminus E(\sigma), \sigma)$ 이면 $Weight(V \setminus E(\sigma)) > Weight(\mathcal{V} \setminus E(\sigma)) \ / \ 2$ 입니다.
2. 동의하는 검증자들의 weight은 모든 정직한 검증자들의 weight의 절반보다 큽니다. ($Weight(Agreeing(p, \sigma)) \geq Weight(V \setminus E(\sigma))$)
따라서 $Weight(Agreeing(p, \sigma)) > Weight(\mathcal{V} \setminus E(\sigma)) \ / \ 2$입니다. 이는 곧 $Majority\_Driven^H(p)$ 정의에 따라 estimator 또한 동의함을 의미합니다.
이 보조정리의 선행 조건은 곧 clique oracle을 의미한다는 점에 주목하십시오.
#### 보조정리 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')
$$
이전 논의에 따르면 clique oracle은 state transition에 대하여 언제나 존재합니다. 따라서 $\forall \sigma' \in Future_t(\sigma)$에서도 항상 존재합니다.
#### 보조정리 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)
$$
보조정리 39에 따르면 모든 future state $\sigma'$에 대하여 clique oracle이 존재합니다. 보조정리 38에 따르면 clique oracle이 존재하면 estimator 또한 $Majority\_Driven^H(p)$에 대하여 동의합니다. 따라서 모든 $\sigma'$에 대하여 estimator가 동의합니다. 이는 곧 $Decided_{\mathcal{C},t}(p, \sigma)$를 의미합니다.
## Conclusion
이번 포스트에서는 n-party consensus safety 정리와 이를 적용한 Casper the Friendly GHOST (Latest Message Driven GHOST)와 Casper the Friendly CBC Finality Gadget를 살펴봤습니다. 또한 이전 포스트에서 미흡했던 safety에 대한 내용을 clique oracle이 safety oracle인지 살펴보았습니다.
## References
- https://hackmd.io/4PFKtf-RR6GKk183mZvMLw
- https://hackmd.io/sDXKV1QRQcG-hJeV6kKpsQ
- https://github.com/cbc-casper/cbc-casper-paper
- https://github.com/cbc-casper/cbc-casper-paper/pull/13
- https://hackmd.io/sDXKV1QRQcG-hJeV6kKpsQ?both#Prerequisite-Notation
- https://en.wikipedia.org/wiki/Total_order
- https://eprint.iacr.org/2019/415.pdf
- https://github.com/LayerXcom/cbc-casper-proof
###### tags: `cbc` `casper` `cbc capser` `explained`