# [Minimal CBC Casper](https://github.com/cbc-casper/cbc-casper-paper/blob/master/cbc-casper-paper-draft.pdf) Symbol / Terminology

## Prerequisite Notation

- (anonymous function)[https://en.wikipedia.org/wiki/Lambda_calculus]

### 2.1 validator name

### 2.2 validator weights

### 2.3 byzantein fault tolerance threshold

### 2.4 consensus value

### 2.5 estimator

### ?? protocol state, protocol message

### 2.6 estimate, sender, justification

### 2.7 preliminary protocol state, protocol message

### 2.8 protocol state transition

### 2.9 equivocating messages

### 2.10 equivocating validators

### 2.11 equivocation fault weight

### 2.12 protocol state with equivocation fault tolerance t

### def 3.1 future cone

### lemma 1: monotonic futures

### theorem 1: 2-party common futures

### theorem 2: n-party common futures

### def 3.2: properties of protocol states

잠깐 중간 요약
- estimator: state -> consensus value
- estimate: consensus value
- property: state -> boolean

### def 3.2: decided properties of protocol states

### lemma 2: forward consistency

### lemma 3: backward consistency

### theorem 3: two-party consensus safety

### def 3.4: inconsistency of properties of protocol states

### def 3.5: consistency of properties of protocol states

### def 3.6: decisions on properties of protocol states

### theorem 4: n-party consensus safety for properties of protocol states

### def 3.7: properties of consensus

- 주의: properties of protocol state와 다름

### def 3.8: mutually corresponding property of protocol states
- 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

### 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

### def 3.10: Decided on properties of consensus values

### def 3.11: Decisions on properties of consensus values

### theorem 5: n-partyh consensus sasfety for properties of the consensus (values)

## 4 Example Protocols

## 4.1 Preliminary Definitions

### Definition 4.1 (Observed validators).

### Definition 4.2. Later messages

### Definition 4.3 (Message From a Sender).

### Definition 4.4 (Messages From a Group).

### Definition 4.5. Later messages from a sender

### Definition 4.6 (Latest Message).

### Definition 4.7 (Latest message driven estimator).

### Definition 4.8 (Latest Estimates).

### Definition 4.9 (Latest message driven estimator).

### Definition 4.10 (≼).

### Lemma 5 (Non-equivocating validators have at most one latest message). ∀v ∈ V,


### lemma 6

### Lemma 7 (Monotonicity of Justifications).

### Lemma 8

### Lemma 9

### Lemma 10 (Observed non-equivocating validators have one latest messages). ∀σ ∈ Σ, ∀v ∈ V

### Definition 4.11 (Latest messages from non-Equivocating validators).

### Definition 4.12 (Latest honest message driven estimator).

### Definition 4.13 (Latest Estimates from non-Equivocating validators).

### Definition 4.14 (Latest honest estimate driven estimator).

### Definition 4.15 (Argmax).

### Definition 4.16 (Score).

### Definition 4.17 (Casper the Friendly Binary Consensus).

### Definition 4.18 (Example non-trivial properties of this binary consensus protocol).

## 4.3 Casper the Friendly Integer Consensus


## 4.4 Casper the Friendly GHOST

### Definition 4.23 (Blocks).
- g: genesis block
- D: block data

### Definition 4.24 (Previous block resolver).
- Proj_1 ?

### Definition 4.25 (n-cestor: n’th generation ancestor block).

### Definition 4.26 (Blockchain membership, m1 􏰃 m2).

### Definition 4.27 (Score of a block).

### Definition 4.28. (Children of a block)

### Definition 4.29. (Best children of a block)

### Definition 4.30. GHOST

### Definition 4.31 (Casper the Friendly Ghost).

### Definition 4.32 (Example non-trivial properties of consensus values).

## 4.5 Casper the Friendly CBC Finality Gadget

### Definition 4.33 (The underlying blockchain). We assume the blockchain has blocks:


### Definition 4.34 (Blocks).

- 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).

### Definition 4.36 (n-cestor: n’th generation ancestor block).

### Definition 4.37 (Blockchain membership, m1 􏰃 m2).


### Definition 4.38 (Consensus values in the CBC Finality Gadget).

### Definition 4.39 (Epoch Score).

### Definition 4.40 (Children Epochs).

### Definition 4.41. Best Children Epochs

### Definition 4.42. GHOST on the epochs:

### Definition 4.43 (Estimator for the CBC Finality gadget).

### Definition 4.44 (Fork Choice Rule for the CBC Finality gadget).

## 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).


### Definition 4.48 (Lists of Things).
### Definition 4.49 (List Prefix ≼).



### Definition 4.50 (Blocks B).
<!--  -->

### Definition 4.51 (Cross-shard Messages Q).

### Definition 4.52 (Genesis Logs).

### Definition 4.53 (Genesis Sources).

### Definition 4.54 (Shard ID Consistency).

### Definition 4.55 (Monotonicity Conditions).

### Definition 4.56 (Messsage Arrival Conditions).

### Definition 4.57 (Set of Blocks B).

### Definition 4.58 (Consensus values).

### Definition 4.60 (Filter Conditions).

### Definition 4.61 (Filtered Children).

### Definition 4.62 (Best Child).

### Definition 4.63 (Block score).

### Definition 4.64. Filtered_GHOST

### Definition 4.65 (Fork Choice $\mathcal{E}_C$ (for child shard C)).

## + 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