the same argument. Such recursion eventually stops due to the fact that only
finitely many valid views exist (by Theorem 48), which implies that only
finitely many valid views smaller than $v$ exist. Therefore, $r$ eventually
sets its $\mathit{current\\_view}.\mathit{view}$ variable to $v$, thus
concluding the proof. ∎

Recall that $v_{\mathit{final}}$ denotes the greatest forever-alive view. The
greatest forever-alive view is well-defined since (1) $\mathit{genesis}$ is a
forever-alive view (by Definition 2; hence, $v_{\mathit{final}}\neq\bot$), (2)
all forever-alive views are valid (by definitions 1 and 2), (3) all valid
views are comparable (by the view comparability property; Theorem 50), and (4)
there exist only finitely many valid views (by Theorem 48). We now show that
$\alpha_{\infty}(v_{\mathit{final}})=\top$.

###### Lemma 0.

$\alpha_{\infty}(v_{\mathit{final}})=\top$.

###### Proof.

Since $v_{\mathit{final}}$ is valid, $v_{\mathit{final}}\in V(\infty)$ (by
Lemma 41). By contradiction, let $\alpha_{\infty}(v_{\mathit{final}})=\bot$.
Hence, $\mathit{genesis}\neq v_{\mathit{final}}$ (since
$\alpha_{\infty}(\mathit{genesis})=\top$).

By Lemma 61, all correct members of $v_{\mathit{final}}$ eventually set their
$\mathit{current\\_view}.\mathit{view}$ variable to $v_{\mathit{final}}$
(since $v_{\mathit{final}}$ is the greatest forever-alive view). Since
$v_{\mathit{final}}\neq\mathit{genesis}$, this is done at line 29 of
LABEL:lst:reconfiguration_view_transition. Furthermore, every correct member
of $v_{\mathit{final}}$ starts $\mathit{vg}(v_{\mathit{final}})$ with a
proposal at line 83 of LABEL:lst:reconfiguration_view_transition (since
$v_{\mathit{final}}$ is not installable at time $\infty$; similarly to Lemma
9). Moreover, the proposal is valid (by Lemma 53).

Suppose that a correct member of $v_{\mathit{final}}$ enters the pseudocode at
line 3 of LABEL:lst:reconfiguration_view_transition after setting its
$\mathit{current\\_view}.\mathit{view}$ variable to $v_{\mathit{final}}$. By
Lemma 60, $v_{\mathit{final}}$ is not the greatest forever-alive view. Thus,
contradiction and no correct member of $v_{\mathit{final}}$ enters the
pseudocode at line 3 of LABEL:lst:reconfiguration_view_transition after
setting its $\mathit{current\\_view}.\mathit{view}$ variable to
$v_{\mathit{final}}$.

Therefore, no correct member of $v_{\mathit{final}}$ stops
$\mathit{vg}(v_{\mathit{final}})$ (since $\mathit{vg}(v_{\mathit{final}})$ can
only be stopped at line 26 of LABEL:lst:reconfiguration_view_transition).
Because of the liveness property of $\mathit{vg}(v_{\mathit{final}})$, a
correct member of $v_{\mathit{final}}$ decides $\mathit{set}_{\mathit{final}}$
from $\mathit{vg}(v_{\mathit{final}})$ (line 21 of
LABEL:lst:reconfiguration_view_generation). By the validity property of
$\mathit{vg}(v_{\mathit{final}})$,
$\mathit{set}_{\mathit{final}}\neq\emptyset$, $\mathit{set}_{\mathit{final}}$
is a sequence and
$\mathit{set}_{\mathit{final}}.\mathtt{follows}(v_{\mathit{final}})=\top$
(since $\mathit{preconditions}(v_{final},\infty)=\top$). Thus, a correct
member of $v_{\mathit{final}}$ enters the pseudocode at line 3 of
LABEL:lst:reconfiguration_view_transition (because of the $\mathtt{INSTALL}$
message “created” using $\mathit{set}_{\mathit{final}}$). Therefore, we reach
contradiction, which implies that $\alpha_{\infty}(v_{\mathit{final}})=\top$.
∎

Next, we show that, if a view $v$ is forever-alive, then all installable views
smaller than or equal to $v$ are forever-alive.

###### Lemma 0.

For every view $v^{*}$ such that $\alpha_{\infty}(v^{*})=\top$ and
$v^{*}\subseteq v_{\mathit{final}}$, $v^{*}$ is forever-alive.

###### Proof.

Follows directly from Lemma 55 and the definition of $v_{\mathit{final}}$. ∎

Finally, we are able to prove the finality property.

###### Theorem 65 (Finality).

Finality is satisfied.

###### Proof.

By Lemma 61, all correct members of $v_{\mathit{final}}$ eventually set their
$\mathit{current\\_view}.\mathit{view}$ variable to $v_{\mathit{final}}$
(since $v_{\mathit{final}}$ is the greatest forever-alive view). Hence, all
correct members of $v_{\mathit{final}}$ update their current view to
$v_{\mathit{final}}$.

Next, we prove that no correct member of $v_{\mathit{final}}$ enters the
pseudocode at line 3 of LABEL:lst:reconfiguration_view_transition after
setting its $\mathit{current\\_view}.\mathit{view}$ variable to
$v_{\mathit{final}}$ (which is already proven in the proof of Lemma 63). If a
correct member of $v_{\mathit{final}}$ does enter the pseudocode,
$v_{\mathit{final}}$ is not the greatest forever-alive view (by Lemma 60).
Therefore, no correct member of $v_{\mathit{final}}$ enters the pseudocode at
line 3 of LABEL:lst:reconfiguration_view_transition after setting its
$\mathit{current\\_view}.\mathit{view}$ variable to $v_{\mathit{final}}$.

Now, consider a correct server $r\in v_{\mathit{final}}.\mathtt{members()}$.
We aim to prove that $r$ installs $v_{\mathit{final}}$. If
$v_{\mathit{final}}=\mathit{genesis}$, $r$ installs $v_{\mathit{final}}$ at
line 44 of LABEL:lst:reconfiguration_initialization. Suppose that
$v_{\mathit{final}}\neq\mathit{genesis}$. By contradiction, assume that $r$
does not install $v_{\mathit{final}}$. Since $r$ does not install
$v_{\mathit{final}}$, $r$ starts $\mathit{vg}(v_{\mathit{final}})$ with a
proposal at line 83 of LABEL:lst:reconfiguration_view_transition. Moreover,
the proposal is valid (by Lemma 53). Since no correct member of
$v_{\mathit{final}}$ enters the pseudocode at line 3 of
LABEL:lst:reconfiguration_view_transition after setting its
$\mathit{current\\_view}.\mathit{view}$ variable to $v_{\mathit{final}}$, no
correct member of $v_{\mathit{final}}$ stops $\mathit{vg}(v_{\mathit{final}})$
(since $\mathit{vg}(v_{\mathit{final}})$ can only be stopped at line 26 of
LABEL:lst:reconfiguration_view_transition). Because of the liveness property
of $\mathit{vg}(v_{\mathit{final}})$, $r$ decides
$\mathit{set}_{\mathit{final}}$ from $\mathit{vg}(v_{\mathit{final}})$ (line
21 of LABEL:lst:reconfiguration_view_generation). By the validity property of
$\mathit{vg}(v_{\mathit{final}})$,
$\mathit{set}_{\mathit{final}}\neq\emptyset$, $\mathit{set}_{\mathit{final}}$
is a sequence and
$\mathit{set}_{\mathit{final}}.\mathtt{follows}(v_{\mathit{final}})=\top$
(since $\mathit{preconditions}(v_{final},\infty)=\top$). Thus, $r$ enters the
pseudocode at line 3 of LABEL:lst:reconfiguration_view_transition (because of
the $\mathtt{INSTALL}$ message “created” using
$\mathit{set}_{\mathit{final}}$). Therefore, we reach contradiction, which
implies that $r$ indeed installs $v_{\mathit{final}}$.

Since $r$ never enters the pseudocode at line 3 of
LABEL:lst:reconfiguration_view_transition after setting its
$\mathit{current\\_view}.\mathit{view}$ variable to $v_{\mathit{final}}$, $r$
does not update its current view after updating it to $v_{\mathit{final}}$.
Similarly, $r$ does not leave.

Finally, by contradiction, suppose that $r$ stops processing in
$v_{\mathit{final}}$ (i.e., $r$ executes line 10 of
LABEL:lst:reconfiguration_state_transfer for some view
$v_{\mathit{stop}}\supseteq v_{\mathit{final}}$). By the check at line 3 of
LABEL:lst:reconfiguration_state_transfer,
$v_{\mathit{stop}}\in\mathit{history}$ at server $r$. By Lemma 5,
$v_{\mathit{stop}}$ is a valid view. Moreover,
$\mathit{set}^{\prime}\neq\emptyset$151515$\mathit{set}^{\prime}$ is the set
of views specified at line 3 of LABEL:lst:reconfiguration_state_transfer. is a
sequence and $\mathit{set}^{\prime}.\mathtt{follows}(v_{\mathit{stop}})=\top$
(since $\mathit{set}^{\prime}\in\rho_{\infty}(v_{\mathit{stop}})$ and
Invariant 1). Since $v_{\mathit{final}}\subseteq v_{\mathit{stop}}$ and
$\mathit{set}^{\prime}.\mathtt{follows}(v_{\mathit{stop}})=\top$,
$v_{\mathit{final}}\subset\mathit{set}^{\prime}.\mathtt{first()}$.
Furthermore, $\mathit{set}^{\prime}.\mathtt{first()}\in\mathit{history}$ (see
LABEL:lst:install_messages and LABEL:lst:storage_processing). Hence, by Lemma
4, $r$ has obtained a view-path
$\mathit{path}\subseteq\mathit{install\\_messages}$ (at server $r$) to
$\mathit{set}^{\prime}.\mathtt{first()}$ (note that
$\mathit{set}^{\prime}.\mathtt{first()}\neq\mathit{genesis}$ since
$\mathit{set}^{\prime}.\mathtt{first()}\supset v_{\mathit{final}}$ and
$v_{\mathit{final}}\supseteq\mathit{genesis}$). Finally, since $r$ never
leaves and $r$ has gossiped all messages that belong to $\mathit{path}$ (at
line 12 of LABEL:lst:storage_processing), Definition 2 is satisfied for
$\mathit{set}^{\prime}.\mathtt{first()}$. Hence,
$\mathit{set}^{\prime}.\mathtt{first()}\supset v_{\mathit{final}}$ is forever-
alive. Thus, we reach contradiction with the fact that $v_{\mathit{final}}$ is
the greatest forever-alive view, which implies that $r$ does not stop
processing in $v_{\mathit{final}}$. Therefore, the theorem holds. ∎

The next important intermediate result we prove is that there exists a view
$v$ such that $r\in v.\mathtt{members()}$ (resp., $r\notin
v.\mathtt{members()}$) and $\alpha_{\infty}(v)=\top$ if a correct server $r$
requests to join (resp., leave). First, we introduce the next two lemmas that
help us prove the aforementioned result.

###### Lemma 0.

Let $r\in v_{\mathit{final}}.\mathtt{members()}$ be a correct server.
Moreover, let $(+,r^{\prime})\in\mathit{reconfiguration}.\mathit{requested}$
at server $r$. Then, $(+,r^{\prime})\in v_{\mathit{final}}$.

###### Proof.

By contradiction, suppose that $(+,r^{\prime})\notin v_{\mathit{final}}$. By
Lemma 47, $(-,r^{\prime})\notin v_{\mathit{final}}$.

Consider any correct server $r^{*}\in v_{\mathit{final}}.\mathtt{members()}$.
By the finality property:

  * •

$r^{*}$ eventually updates its current view to $v_{\mathit{final}}$,

  * •

$r^{*}$ never updates its current view afterwards,

  * •

$r^{*}$ installs $v_{\mathit{final}}$, and

  * •

$r^{*}$ does not leave.

Since $(+,r^{\prime})\notin v_{\mathit{final}}$, the rule at line 13 of
LABEL:lst:reconfiguration_view_generation is eventually active at server $r$.
Hence, $r$ proposes to $\mathit{vg}(v_{\mathit{final}})$ at line 18 of
LABEL:lst:reconfiguration_view_generation. By Lemma 53, the proposal is valid.
Every correct member of $v_{\mathit{final}}$ starts
$\mathit{vg}(v_{\mathit{final}})$ and no correct member of
$v_{\mathit{final}}$ stops $\mathit{vg}(v_{\mathit{final}})$ (due to the
finality property). Because of the liveness property of
$\mathit{vg}(v_{\mathit{final}})$, a correct member of $v_{\mathit{final}}$
decides $\mathit{set}_{\mathit{final}}$ from $\mathit{vg}(v_{\mathit{final}})$
(line 21 of LABEL:lst:reconfiguration_view_generation). By the validity
property of $\mathit{vg}(v_{\mathit{final}})$,
$\mathit{set}_{\mathit{final}}\neq\emptyset$, $\mathit{set}_{\mathit{final}}$
is a sequence and
$\mathit{set}_{\mathit{final}}.\mathtt{follows}(v_{\mathit{final}})=\top$
(since $\mathit{preconditions}(v_{final},\infty)=\top$). Thus, a correct
member of $v_{\mathit{final}}$ enters the pseudocode at line 3 of
LABEL:lst:reconfiguration_view_transition (because of the $\mathtt{INSTALL}$
message “created” using $\mathit{set}_{\mathit{final}}$). By Lemma 60,
$v_{\mathit{final}}$ is not the greatest forever-alive view. Thus, we reach
contradiction, which implies that $(+,r^{\prime})\in v_{\mathit{final}}$. ∎

###### Lemma 0.

Let $r\in v_{\mathit{final}}.\mathtt{members()}$ be a correct server.
Moreover, let $(-,r^{\prime})\in\mathit{reconfiguration}.\mathit{requested}$
at server $r$ and let $(+,r^{\prime})\in v_{\mathit{final}}$. Then,
$(-,r^{\prime})\in v_{\mathit{final}}$.

###### Proof.

By contradiction, suppose that $(-,r^{\prime})\notin v_{\mathit{final}}$.

Consider any correct server $r^{*}\in v_{\mathit{final}}.\mathtt{members()}$.
By the finality property:

  * •

$r^{*}$ eventually updates its current view to $v_{\mathit{final}}$,

  * •

$r^{*}$ never updates its current view afterwards,

  * •

$r^{*}$ installs $v_{\mathit{final}}$, and

  * •

$r^{*}$ does not leave.

Since $(-,r^{\prime})\notin v_{\mathit{final}}$ and $(+,r^{\prime})\in
v_{\mathit{final}}$, the rule at line 13 of
LABEL:lst:reconfiguration_view_generation is eventually active at server $r$.
Hence, $r$ proposes to $\mathit{vg}(v_{\mathit{final}})$ at line 18 of
LABEL:lst:reconfiguration_view_generation. By Lemma 53, the proposal is valid.
Every correct member of $v_{\mathit{final}}$ starts
$\mathit{vg}(v_{\mathit{final}})$ and no correct member of
$v_{\mathit{final}}$ stops $\mathit{vg}(v_{\mathit{final}})$. Because of the
liveness property of $\mathit{vg}(v_{\mathit{final}})$, a correct member of
$v_{\mathit{final}}$ decides $\mathit{set}_{\mathit{final}}$ from
$\mathit{vg}(v_{\mathit{final}})$ (line 21 of
LABEL:lst:reconfiguration_view_generation). By the validity property of
$\mathit{vg}(v_{\mathit{final}})$,
$\mathit{set}_{\mathit{final}}\neq\emptyset$, $\mathit{set}_{\mathit{final}}$
is a sequence and
$\mathit{set}_{\mathit{final}}.\mathtt{follows}(v_{\mathit{final}})=\top$
(since $\mathit{preconditions}(v_{final},\infty)=\top$). Thus, a correct
member of $v_{\mathit{final}}$ enters the pseudocode at line 3 of
LABEL:lst:reconfiguration_view_transition (because of the $\mathtt{INSTALL}$
message “created” using $\mathit{set}_{\mathit{final}}$). By Lemma 60,
$v_{\mathit{final}}$ is not the greatest forever-alive view. Thus, we reach
contradiction, which implies that $(-,r^{\prime})\in v_{\mathit{final}}$. ∎

The next lemma proves that there cannot exist an $\mathtt{INSTALL}$ message
$m$ such that $(-,r)\in m.\mathtt{destination()}$ and $(+,r)\notin
m.\mathtt{source()}$, where $m.\mathtt{source()}$ is a valid view and $m$ is a
server.

###### Lemma 0.

Let $m\in\mathcal{I}^{*}(\infty)$, where $m.\mathtt{source()}$ is a valid
view. Let $(+,r)\notin m.\mathtt{source()}$, for some server $r$. Then,
$(-,r)\notin m.\mathtt{destination()}$.

###### Proof.

Follows from the membership validity property of
$\mathit{vg}(m.\mathtt{source()})$ (since $m.\mathtt{source()}$ is a valid
view and
$\mathit{preconditions}(m.\mathtt{source()},\infty)=\top$). ∎

Finally, we prove that there exists an installable view $v_{r}\subseteq
v_{\mathit{final}}$ such that $r\in v_{r}.\mathtt{members()}$, where $r$ is a
correct server that requested to join.

###### Lemma 0.

Let a correct server $r$ request to join. Then, there exists a view
$v_{r}\subseteq v_{\mathit{final}}$ such that $\alpha_{\infty}(v_{r})=\top$
and $r\in v_{r}.\mathtt{members()}$.

###### Proof.

Since $r$ requests to join, $r\notin\mathit{genesis}.\mathtt{members()}$ (see
§ 3.3, paragraph “Server’s rules”). Therefore, $(+,r)\notin\mathit{genesis}$.
First, we prove that $(+,r)\in v_{\mathit{final}}$. By contradiction, assume
that $(+,r)\notin v_{\mathit{final}}$. Hence, $r$ does not join (by Lemma 59
and the fact that $v_{\mathit{final}}$ is the greatest forever-alive view),
which implies that $r$ does not leave. Hence, $r$ never halts (see § 3.3,
paragraph “Server’s rules”), which means that $r$ is forever-correct.

Since $r$ is forever-correct, the $\mathtt{JOIN}$ message gossiped by $r$ (at
line 4 of LABEL:lst:reconfiguration_joining) is received by a correct member
of $v_{\mathit{final}}$ (due to the validity property of the gossip
primitive). Hence, $(+,r)$ is included into the
$\mathit{reconfiguration}.\mathit{requested}$ variable of that server (due to
the fact that $r$ broadcasts the voting proof; see § 3.3, paragraph “Server’s
rules”). By Lemma 66, $(+,r)\in v_{\mathit{final}}$, which represents the
contradiction with $(+,r)\notin v_{\mathit{final}}$. Therefore, our starting
assumption was not correct, hence $(+,r)\in v_{\mathit{final}}$.

If $(-,r)\notin v_{\mathit{final}}$, the lemma holds since
$\alpha_{\infty}(v_{\mathit{final}})=\top$ (by Lemma 63).

Hence, let $(-,r)\in v_{\mathit{final}}$. In this case,
$v_{\mathit{final}}\neq\mathit{genesis}$ (since $\mathit{genesis}$ does not
contain “negative” changes; see § 2, paragraph “Constants”). Therefore, there
exists a view $v_{i}$ such that $v_{i}$ is the greatest view smaller than
$v_{\mathit{final}}$ that is installable at time $\infty$. By Lemma 43,
$v_{i}$ leads to $v_{\mathit{final}}$ at time $\infty$. Furthermore,
$\mathit{seq}_{i}\in\rho_{\infty}(v_{i})$, where $\mathit{seq}_{i}=...\to
v_{\mathit{final}}$ (by Definition 11). By the membership validity property of
$\mathit{vg}(v_{i})$ (since $\mathit{preconditions}(v_{i},\infty)=\top$),
$(+,r)\in v_{i}$. Therefore, we reach the point we reached with
$v_{\mathit{final}}$: (1) $\alpha_{\infty}(v_{i})=\top$, and (2) $(+,r)\in
v_{i}$. The recursion eventually stops due to (1) the fact that there are only
finitely many valid views (by Theorem 48), which implies existence of only
finitely many views installable at time $\infty$, (2) $\mathit{genesis}$ is
the smallest installable view (since $\mathit{genesis}$ is installable by
definition and $\mathit{genesis}$ is the smallest valid view, by Lemma 45),
and (3) $(+,r)\notin\mathit{genesis}$. Therefore, the lemma holds. ∎

Next, we prove that $(+,r),(-,r)\in v_{\mathit{final}}$, where $r$ is a
correct server that requested to leave.

###### Lemma 0.

Let a correct server $r$ request to leave. Then, $(+,r),(-,r)\in
v_{\mathit{final}}$.

###### Proof.

Since $r$ requests to leave, $r$ has previously joined (see § 3.3, paragraph
“Server’s rules”). Hence, $(+,r)\in v_{\mathit{final}}$ (by Lemma 59 and the
fact that $v_{\mathit{final}}$ is the greatest forever-alive view). By
contradiction, let $(-,r)\notin v_{\mathit{final}}$. Thus, $r$ never leaves
(by Lemma 60 and the fact that $v_{\mathit{final}}$ is the greatest forever-
alive view), which means that $r$ is forever-correct.

Since $r$ is forever-correct, the $\mathtt{LEAVE}$ message gossiped by $r$ (at
line 4 of LABEL:lst:reconfiguration_leaving) is received by a correct member
of $v_{\mathit{final}}$ (due to the validity property of the gossip primitive;
see § 2). Hence, $(-,r)$ is included into the
$\mathit{reconfiguration}.\mathit{requested}$ variable of that server. By
Lemma 67, $(-,r)\in v_{\mathit{final}}$, which represents the contradiction
with $(-,r)\notin v_{\mathit{final}}$. Therefore, our starting assumption was
not correct, hence $(-,r)\in v_{\mathit{final}}$. The lemma holds. ∎

Before we are able to prove the join and leave liveness defined in § 3.3, we
show that a correct server eventually “discharges” a view.

###### Lemma 0 (Eventual Dischargement).

Let a correct server $r$ enter the pseudocode at line 3 of
LABEL:lst:reconfiguration_view_transition. Eventually,
$\mathit{reconfiguration}.\mathit{discharged}=\top$ at server $r$.

###### Proof.

By contradiction, suppose that the
$\mathit{reconfiguration}.\mathit{discharged}$ variable is not set to $\top$
at server $r$. Hence, $r$ never halts (since it never leaves), which makes $r$
forever-correct. Then,
$[\mathtt{INSTALL},v^{\prime},\mathit{seq}=v\to...,\omega]\in\mathit{install\\_messages}$
at server $r$, where $r\notin v.\mathtt{members}()$. By Lemma 60, a view
$v^{*}\supseteq v$ is forever-alive. Since $v^{*}\subseteq
v_{\mathit{final}}$, $v\subseteq v_{\mathit{final}}$.

Since $r$ is forever-correct, the $\mathtt{DISCHARGEMENT-REQUEST}$ gossiped by
$r$ (at line 20 of LABEL:lst:reconfiguration_view_transition) is received by
every member of $v_{\mathit{final}}$ while their
$\mathit{current\\_view}.\mathit{view}$ variable is equal to
$v_{\mathit{final}}$ (holds because of the validity property of the gossip
primitive and the finality property). Moreover, $r$ eventually includes
$v_{\mathit{final}}$ into its $\mathit{history}$ variable (since $r$ is
forever-correct). Therefore, $r$ eventually receives $[\mathtt{DISCHARGEMENT-
CONFIRM},v_{\mathit{final}}]$ messages from all correct members of
$v_{\mathit{final}}$. Once that happens, the rule at line 11 of
LABEL:lst:reconfiguration_view_dischargement is active and $r$ sets its
$\mathit{reconfiguration}.\mathit{discharged}$ variable to $\top$. Thus, the
lemma holds. ∎

Finally, we are ready to prove the join liveness property defined in § 3.3.

###### Theorem 72 (Join Liveness).

Join liveness is satisfied.

###### Proof.

Let $r$ be a correct server that requests to join. By Lemma 69, there exists a
view $v_{r}\subseteq v_{\mathit{final}}$ such that (1)
$\alpha_{\infty}(v_{r})=\top$, and (2) $r\in v_{r}.\mathtt{members()}$. By
Lemma 64, $v_{r}$ is forever-alive. Then, $r$ joins due to Lemma 62. ∎

Next, we prove the leave liveness property defined in § 3.3.

###### Theorem 73 (Leave Liveness).

Leave liveness is satisfied.

###### Proof.

Let $r$ be a correct server that requests to leave. Therefore, $r$ has
previously joined (see § 3.3, paragraph “Server’s rules”). By Lemma 70,
$(+,r),(-,r)\in v_{\mathit{final}}$; hence, $r\notin
v_{\mathit{final}}.\mathtt{members()}$.

By contradiction, suppose that $r$ never leaves. Hence, $r$ never halts, which
means that $r$ is forever-correct. Since $r$ has joined, the
$\mathit{current\\_view}.\mathit{view}$ variable at $r$ is not equal to
$\bot$; let $\mathit{current\\_view}.\mathit{view}$ variable have its final
value $v_{r}$ (the final value is indeed defined since
$\mathit{current\\_view}.\mathit{view}$ variable of a correct server is set
only to valid views, it only “grows” and there exist finitely many valid
views, by Theorem 48). By Lemma 59, $v_{r}\subseteq v_{\mathit{final}}$. Since
$r\in v_{r}.\mathtt{members()}$ and $r\notin
v_{\mathit{final}}.\mathtt{members()}$, $v_{r}\subset v_{\mathit{final}}$.

Since $r$ is forever-correct, $r$ eventually enters the pseudocode at line 3
of LABEL:lst:reconfiguration_view_transition due to the fact that $r$
eventually obtains a view-path to $v_{\mathit{final}}$ and $v_{r}\subset
v_{\mathit{final}}$. Let the “destination” view be $v_{r}^{\prime}$. If
$r\notin v_{r}^{\prime}.\mathtt{members()}$, then $r$ eventually leaves (by
Lemma 71). This is impossible due to the fact that $r$ never leaves. Hence,
$r\in v_{r}^{\prime}.\mathtt{members()}$. Therefore, $r$ updates its
$\mathit{current\\_view}.\mathit{view}$ variable to $v_{r}^{\prime}\supset
v_{r}$ (by Lemma 58). Thus, we reach contradiction with the fact that $v_{r}$
is the final value of $\mathit{current\\_view}.\mathit{view}$ at server $r$,
which means that our starting assumption was not correct and $r$ leaves. ∎

Lastly, we prove the removal liveness property defined in § 3.3. In order to
prove the removal liveness property, we prove that a correct forever-validator
is a member of $v_{\mathit{final}}$.

###### Lemma 0.

Let $r$ be a correct forever-validator. Then, $r\in
v_{\mathit{final}}.\mathtt{members()}$.

###### Proof.

Since $r$ is correct forever-validator, $r$ has joined (see § 3.3, paragraph
“Validators”). By Lemma 59, $(+,r)\in v_{\mathit{final}}$. By contradiction,
suppose that $(-,r)\in v_{\mathit{final}}$.

Since $r$ has joined, the $\mathit{current\\_view}.\mathit{view}$ variable at
$r$ is not equal to $\bot$; let $\mathit{current\\_view}.\mathit{view}$
variable have its final value $v_{r}$. By Lemma 59, $v_{r}\subseteq
v_{\mathit{final}}$. Since $r\in v_{r}.\mathtt{members()}$ and $r\notin
v_{\mathit{final}}.\mathtt{members()}$, $v_{r}\subset v_{\mathit{final}}$.

Since $r$ is forever-correct (because it does not leave), $r$ eventually
enters the pseudocode at line 3 of LABEL:lst:reconfiguration_view_transition
due to the fact that $r$ eventually obtains a view-path to
$v_{\mathit{final}}$ and $v_{r}\subset v_{\mathit{final}}$. Let the
“destination” view be $v_{r}^{\prime}$. If $r\notin
v_{r}^{\prime}.\mathtt{members()}$, then $r$ eventually leaves (by Lemma 71).
This is impossible due to the fact that $r$ never leaves. Hence, $r\in
v_{r}^{\prime}.\mathtt{members()}$. Therefore, $r$ updates its
$\mathit{current\\_view}.\mathit{view}$ variable to $v_{r}^{\prime}\supset
v_{r}$ (by Lemma 58). Thus, we reach contradiction with the fact that $v_{r}$
is the final value of $\mathit{current\\_view}.\mathit{view}$ at server $r$,
which means that our starting assumption was not correct and $(-,r)\notin
v_{\mathit{final}}$. Hence, $r\in v_{\mathit{final}}.\mathtt{members()}$. ∎

The next theorem proves the removal liveness property.

###### Theorem 75 (Removal Liveness).

Removal liveness is satisfied.

###### Proof.

Let $r^{*}$ be a correct forever-validator that obtains a voting proof
$\sigma_{v}$ that a server $r$ is voted out. By Lemma 74, $r^{*}\in
v_{\mathit{final}}.\mathtt{members()}$. Since $r$ is a validator at time $t$,
that means that $r$ joined by time $t$. We aim to prove that $(+,r)\in
v_{\mathit{final}}$. Let us consider both possible cases:

  * •

Let $r$ be a correct server. Hence, $(+,r)\in v_{\mathit{final}}$ due to Lemma
59.

  * •

Let $r$ be a faulty server. Hence, a correct server triggered the special
$r\text{ }\mathtt{joined}$ event (at line 53 of
LABEL:lst:reconfiguration_initialization or at line 60 of
LABEL:lst:reconfiguration_view_transition). Hence, $(+,r)\in
v_{\mathit{final}}$ due to Lemma 59.

Therefore, $(+,r)\in v_{\mathit{final}}$. By Lemma 67, $(-,r)\in
v_{\mathit{final}}$, as well. Since $(-,r)\in v_{\mathit{final}}$,
$\mathit{genesis}\neq v_{\mathit{final}}$ (see § 2, paragraph “Constants”).

Again, we separate two possible cases:

  * •

Let $r$ be a correct server. By contradiction, suppose that $r$ does not
leave. Since $r$ has joined, the $\mathit{current\\_view}.\mathit{view}$
variable at $r$ is not equal to $\bot$; let
$\mathit{current\\_view}.\mathit{view}$ variable have its final value $v_{r}$
(the final value of the $\mathit{current\\_view}.\mathit{view}$ variable
exists since there are only finitely many valid views, by Theorem 48, and a
correct server updates the variable only with greater values, by the check at
line 3 of LABEL:lst:reconfiguration_view_transition). By Lemma 59,
$v_{r}\subseteq v_{\mathit{final}}$. Since $r\in v_{r}.\mathtt{members()}$ and
$r\notin v_{\mathit{final}}.\mathtt{members()}$, $v_{r}\subset
v_{\mathit{final}}$.

Since $r$ is forever-correct (because it does not leave), $r$ eventually
enters the pseudocode at line 3 of LABEL:lst:reconfiguration_view_transition
due to the fact that $r$ eventually obtains a view-path to
$v_{\mathit{final}}$ and $v_{r}\subset v_{\mathit{final}}$. Let the
“destination” view be $v_{r}^{\prime}$. If $r\notin
v_{r}^{\prime}.\mathtt{members()}$, then $r$ eventually leaves (by Lemma 71).
This is impossible due to the fact that $r$ never leaves. Hence, $r\in
v_{r}^{\prime}.\mathtt{members()}$. Therefore, $r$ updates its
$\mathit{current\\_view}.\mathit{view}$ variable to $v_{r}^{\prime}\supset
v_{r}$ (by Lemma 58). Thus, we reach contradiction with the fact that $v_{r}$
is the final value of $\mathit{current\\_view}.\mathit{view}$ at server $r$,
which means that our starting assumption was not correct and $r$ leaves.

  * •

Let $r$ be a faulty server. By the finality property, $r^{*}$ eventually sets
its $\mathit{current\\_view}.\mathit{view}$ variable to
$v_{\mathit{final}}\neq\mathit{genesis}$. Hence, $r^{*}$ enters the pseudocode
at line 3 of LABEL:lst:reconfiguration_view_transition with the “source” view
$v_{s}$ and with the “destination” view $v_{\mathit{final}}$. We know that
$(+,r),(-,r)\in v_{\mathit{final}}$. By the membership validity property of
$\mathit{vg}(v_{s})$ (since $v_{s}$ is a valid view and
$\mathit{preconditions}(v_{s},\infty)=\top$), $(+,r)\in v_{s}$. If
$(-,r)\notin v_{s}$, then $r$ leaves since $r^{*}$ triggers the special
$r\text{ }\mathtt{left}$ event (at line 64 of
LABEL:lst:reconfiguration_view_transition).

Otherwise, $(+,r),(-,r)\in v_{s}$ and $v_{s}\neq\mathit{genesis}$ (since
$\mathit{genesis}$ does not contain “negative” changes; see § 2, paragraph
“Constants”). Now, we consider a correct server $r_{s}\in
v_{s}.\mathtt{members()}$ that sets its
$\mathit{current\\_view}.\mathit{view}$ variable to $v_{s}$ at line 29 of
LABEL:lst:reconfiguration_view_transition; such server exists due to the fact
that the $\mathtt{INSTALL}$ message $m$ is obtained, where
$m.\mathtt{source()}=v_{s}$ and $m.\mathtt{destination()}=v_{\mathit{final}}$,
and due to the decision permission property of $\mathit{vg}(v_{s})$. Hence, we
apply the same reasoning as with $v_{\mathit{final}}$. Such recursion
eventually stops due to (1) the fact that there are only finitely many valid
views (by Theorem 48), (2) $\mathit{genesis}$ is the smallest valid view (by
Lemma 45), and (3) $(-,r)\notin\mathit{genesis}$. Therefore, $r$ leaves.

The theorem holds since $r$ leaves in all possible cases. ∎

##  7\. Client’s Implementation

This section is devoted to the implementation of the client. As we have
already mentioned in § 3, clients are the users of Carbon, i.e., clients are
the entities that are able to issue transactions. Before we give the
implementation of a client, we define the commitment proof of a transaction.
Specifically, we define when
$\mathtt{verify\\_commit}(\mathit{tx}\in\mathcal{T},\sigma_{c}\in\Sigma_{c})=\top$.

⬇

1function verify_commit(Transaction $\mathit{tx}$, Commitment_Proof
$\sigma_{c}$):

2 if $\sigma_{c}$ is not Set(Message):

3 return $\bot$

4 if does not exist View $v$ such that $m=[$COMMITTED, $\mathit{tx}$, $v$,
View_Path $\mathit{path}]$ and $v=\mathit{path}$.destination(), for every
Message $m\in\sigma_{c}$:

5 return $\bot$

7 Set(Server) $\mathit{senders}=\\{m\text{.sender}\,|\,m\in\sigma_{c}\\}$

8 if $\mathit{senders}\not\subseteq v$.members():

9 return $\bot$

10 return $|\mathit{senders}|\geq v$.plurality()

12function (Commitment_Proof $\sigma_{c}$).signers:

13 return $\\{m\text{.sender}\,|\,m\in\sigma_{c}\\}$

Listing 35: The $\mathtt{verify\\_commit}$ function

Intuitively, $\mathtt{verify\\_commit}(\mathit{tx},\sigma_{c})=\top$ if and
only if $\sigma_{c}$ contains $v.\mathtt{plurality()}$ $\mathtt{COMMITTED}$
messages, where $v$ is a valid view. Finally, we give the implementation of a
client. We assume that each transaction is signed by its issuer, i.e., a
transaction $\mathit{tx}$ is signed by $\mathit{tx}.\mathit{issuer}$. Hence,
only $\mathit{tx}.\mathit{issuer}$ can issue $\mathit{tx}$. For the sake of
brevity, we omit this logic in the pseudocode given below.

⬇

1Client:

2 Implementation:

3 upon start: // executed as soon as the $\mathtt{start}$ event is triggered

4 Set(Message) $\mathit{waiting\\_messages}=\emptyset$

6 // reconfiguration variables

7 View $\mathit{current\\_view}=\mathit{genesis}$

8 Sequence $\mathit{history}=\mathit{genesis}$

9 Set(Install_Message) $\mathit{install\\_messages}=\emptyset$

11 String $state=$ "idle"

13 // transaction variables

14 Transaction $\mathit{current\\_transaction}=\bot$

15 Map(View $\to$ Set(Server)) $\mathit{acks\\_from}=\\{v\to\emptyset\text{,
for every View }v\\}$

16 Map(View $\to$ Set(Message)) $\mathit{acks}=\\{v\to\emptyset\text{, for
every View }v\\}$

17 Set(Message) $\mathit{certificate}=\bot$

19 // query variables

20 Integer $\mathit{query\\_id}=0$

21 Map(View $\to$ Set(Server))
$\mathit{responses\\_from}=\\{v\to\emptyset\text{, for every View }v\\}$

22 Map(View $\to$ Set(Integer)) $\mathit{responses}=\\{v\to\emptyset\text{,
for every View }v\\}$

24 upon receipt of Message $m$:

25 $\mathit{waiting\\_messages}=\mathit{waiting\\_messages}\cup\\{m\\}$

27 upon exists Install_Message $m\in\mathit{waiting\\_messages}$ such that
$m=[$INSTALL, $v$, $\mathit{set}$, $\omega]$ and $v\in\mathit{history}$ and
$m\notin\mathit{install\\_messages}$:

28 $\mathit{waiting\\_messages}=\mathit{waiting\\_messages}\setminus{\\{m\\}}$

29 $\mathit{install\\_messages}=\mathit{install\\_messages}\cup\\{m\\}$

30 gossip $m$

31 View $v^{\prime}=m$.destination()

32 if $v^{\prime}\notin\mathit{history}$:

33 $\mathit{history}=\mathit{history}\cup\\{v^{\prime}\\}$

35 upon exists View $v\in\mathit{history}$ such that
$\mathit{current\\_view}\subset v$:

36 $\mathit{current\\_view}=v$

37 if $\mathit{state}=$ "query":

38 broadcast $[$QUERY, $\mathit{query\\_id}$,
$\mathit{current\\_view}.\mathit{view}]$ to
$\mathit{current\\_view}.\mathit{view}$.members()

39 if $\mathit{state}=$ "certificate collection":

40 broadcast $[$PREPARE, $\mathit{current\\_transaction}$,
$\mathit{current\\_view}]$ to $\mathit{current\\_view}$.members()

41 if $\mathit{state}=$ "commitment proof collection":

42 broadcast $[$COMMIT, $\mathit{current\\_transaction}$,
$\mathit{certificate}$, $\mathit{current\\_view}]$ to
$\mathit{current\\_view}$.members()

44 upon issue Transaction $\mathit{tx}$: // the client issues a transaction
$\mathit{tx}$

45 // reset transaction variables

46 $\mathit{acks\\_from}=\\{v\to\emptyset\text{, for every View }v\\}$

47 $\mathit{acks}=\\{v\to\emptyset\text{, for every View }v\\}$

48 $\mathit{certificate}=\bot$

50 $\mathit{state}=$ "certificate collection" // set state to "certificate
collection"

51 $\mathit{current\\_transaction}=\mathit{tx}$ // remember the transaction

52 // broadcast the prepare message to all members of
$\mathit{current\\_view}$

53 broadcast $[$PREPARE, $\mathit{tx}$, $\mathit{current\\_view}]$ to
$\mathit{current\\_view}.$members()

55 upon query market: // the client requests to learn the total amount of
money

56 // reset transaction variables

57 $\mathit{responses\\_from}=\\{v\to\emptyset\text{, for every View }v\\}$

58 $\mathit{responses}=\\{v\to\emptyset\text{, for every View }v\\}$

60 $\mathit{state}=$ "query" // set state to "query"

61 $\mathit{query\\_id}=\mathit{query\\_id}+1$

62 // broadcast the query message to all members of $\mathit{current\\_view}$

63 broadcast $[$QUERY, $\mathit{query\\_id}$, $\mathit{current\\_view}]$ to
$\mathit{current\\_view}.$members()

65 upon exists Message $m\in\mathit{waiting\\_messages}$ such that $m=[$ACK,
Transaction $\mathit{tx}$, View $v$, View_Path $\mathit{path}]$ and
$\mathit{tx}=\mathit{current\\_transaction}$ and $\mathit{path}$.destination()
$=v$ and $m$.sender $\in v$.members() and
$state=$ "certificate collection":

66 $\mathit{waiting\\_messages}=\mathit{waiting\\_messages}\setminus{\\{m\\}}$

67 Server $r=m$.sender

68 if $r\notin\mathit{acks\\_from}[v]$:

69 $\mathit{acks\\_from}[v]=\mathit{acks\\_from}[v]\cup\\{r\\}$

70 $\mathit{acks}[v]=\mathit{acks}[v]\cup\\{m\\}$

72 upon exists View $v$ such that $|\mathit{acks\\_from}[v]|\geq v$.quorum()
and $\mathit{state}=$ "certificate collection":

73 $\mathit{state}=$ "commitment proof collection" // set state to "commitment
proof collection"

74 $\mathit{certificate}=\mathit{acks}[v]$ // update the certificate

75 // broadcast the commit message to all members of $\mathit{current\\_view}$

76 broadcast $[$COMMIT, $\mathit{tx}$, $\mathit{certificate}$,
$\mathit{current\\_view}]$ to $\mathit{current\\_view}$.members()

78 upon obtaining Commitment_Proof $\sigma_{c}$ such that
verify_commit(Transaction $\mathit{tx}$, $\sigma_{c}$) $=\top$:

79 trigger committed $\mathit{tx}$ // the client learns that $\mathit{tx}$ is
committed

80 if $\mathit{tx}=\mathit{current\\_transaction}$:

81 $\mathit{state}=$ "idle"

82 $\mathit{current\\_transaction}=\bot$

84 upon exists Message $m\in\mathit{waiting\\_messages}$ such that $m=[$QUERY-
RESPONSE, Integer $\mathit{response}$, Integer $\mathit{qid}$, View $v$,
View_Path $\mathit{path}]$ and $\mathit{query\\_id}=\mathit{qid}$ and
$\mathit{state}=$ "query" and $\mathit{path}$.destination() $=v$ and
$m$.sender $\in v$.members():

85 $\mathit{waiting\\_messages}=\mathit{waiting\\_messages}\setminus{\\{m\\}}$

86 Server $r=m$.sender

87 if $r\notin\mathit{responses\\_from}[v]$:

88 $\mathit{responses\\_from}[v]=\mathit{responses\\_from}[v]\cup\\{r\\}$

89 $\mathit{responses}[v]=\mathit{responses}[v]\cup\\{\mathit{response}\\}$

91 upon exists View $v$ such that $|\mathit{responses\\_from}[v]|\geq
v$.quorum() and $\mathit{state}=$ "query":

92 $\mathit{state}=$ "idle"

93 trigger total money median($\mathit{responses}[v]$)

Listing 36: Client - implementation

Let us emphasize that the $\mathit{history}$ variable of a client is indeed a
sequence since all views that belong to $\mathit{history}$ are valid (follows
from line 27 of LABEL:lst:client).

##  8\. Server’s Modules: Transaction Module

This section is devoted to the _transaction module_ of a server. The
transaction module contains the logic for processing transactions issued by
clients.

We start by specifying what constitutes as a “valid” transaction certificate
(see LABEL:lst:transaction_certificate_verification). Then, we give the
implementation used for representing the _state_ of a server, i.e., all
transactions processed by the server (paragraph “State representation”).
Lastly, we present the implementation of the transaction module (paragraph
“Transaction module - implementation”).

⬇

1function verify_transaction_certificate(Transaction $\mathit{tx}$,
Set(Message) $\mathit{certificate}$):

2 if does not exist View $v$ such that $m=[$ACK, $\mathit{tx}$, $v$, View_Path
$\mathit{path}]$ and $v=\mathit{path}$.destination(), for every Message
$m\in\mathit{certificate}$:

3 return $\bot$

4 return $|\\{m.\mathtt{sender}\,|\,m\in\mathit{certificate}\text{ and
}m\text{.sender}\in v\text{.members()}\\}|\geq v$.quorum()

Listing 37: Transaction certificate - verification

A transaction certificate $\mathit{certificate}$ is “valid” for a transaction
$\mathit{tx}$ if and only if
$\mathtt{verify\\_transaction\\_certificate}(\mathit{tx},\mathit{certificate})=\top$.
Intuitively, this is the case if $\mathit{certificate}$ contains a quorum of
$\mathtt{ACK}$ messages for $\mathit{tx}$.

##### State representation.

We give below the implementation for representing the state of a server. This
part of the pseudocode is important since servers exchange their state
representations during the state transfer periods.

⬇

1State_Representation:

2 instance $\mathit{state}=$ {

3 Map(Transaction $\to$ Message) $\mathit{log}$

4 Map(Client, Integer $\to$ Set(Transaction)) $\mathit{allowed\\_acks}$

5 }

7 function verify_transaction_proof(Transaction $\mathit{tx}$, Message
$\mathit{proof}$):

8 return $\mathit{proof}=[$COMMIT, $\mathit{tx}$, Set(Message)
$\mathit{certificate}$, View $v]$ such that
verify_transaction_certificate($\mathit{tx}$, $\mathit{certificate}$) $=\top$
// see LABEL:lst:transaction_certificate_verification

10 function (State_Representation $\mathit{state}$).extract_log():

11 Log $\mathit{log}=\emptyset$

12 for each Transaction $\mathit{tx}$ such that
$\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot$:

13 if verify_transaction_proof($\mathit{tx}$,
$\mathit{state}.\mathit{log}[\mathit{tx}]$) $=\top$:

14 $\mathit{log}=\mathit{log}\cup\\{\mathit{tx}\\}$

15 else:

16 return $\bot$

17 return $\mathit{log}$

19 function (State_Representation $\mathit{state}$).verify_log():

20 Log $\mathit{log}=\mathit{state}$.extract_log()

21 if $\mathit{log}=\bot$:

22 return $\bot$

23 return admissible($\mathit{log}$) // see
LABEL:lst:admissible_transaction_set

25 function (State_Representation $\mathit{state}$).verify_allowed_acks():

26 for each Client $c$ and Integer $i$ such that
$\mathit{state}.\mathit{allowed\\_acks}[c][i]\neq\bot$:

27 for each Transaction
$\mathit{tx}\in\mathit{state}.\mathit{allowed\\_acks}[c][i]$:

28 if $\mathit{tx}.\mathit{issuer}\neq c$ or $\mathit{tx}.\mathit{sn}\neq i$:

29 return $\bot$

30 return $\top$

32 function (State_Representation $\mathit{state}$).verify():

33 return $\mathit{state}$.verify_log() and
$\mathit{state}$.verify_allowed_acks()

35 function merge_logs(State_Representation $\mathit{state}_{1}$,
State_Representation $\mathit{state}_{2}$):

36 if $\mathit{state}_{1}$.verify() $=\bot$ or $\mathit{state}_{2}$.verify()
$=\bot$:

37 return $\bot$

39 Map(Transaction $\to$ Message)
$\mathit{new\\_log}=\\{\mathit{tx}\to\bot,\text{ for every Transaction
}\mathit{tx}\\}$

40 $\mathit{new\\_log}=\mathit{state}_{1}.\mathit{log}$

41 for each Transaction $\mathit{tx}$ such that
$\mathit{state}_{2}.\mathit{log}[\mathit{tx}]\neq\bot$:

42
$\mathit{new\\_log}[\mathit{tx}]=\mathit{state}_{2}.\mathit{log}[\mathit{tx}]$

44 return $\mathit{new\\_log}$

Listing 38: State representation

##### Transaction module - implementation.

Finally, we give the implementation of the transaction module of a server.

⬇

1Transaction Module:

2 Implementation:

3 upon start: // executed as soon as the $\mathtt{start}$ event is triggered

4 Log $\mathit{log}=\emptyset$

5 Map(Transaction $\to$ Bool)
$\mathit{quasi\\_committed}=\\{\mathit{tx}\to\bot\text{, for every Transaction
}\mathit{tx}\\}$

6 Map(Transaction $\to$ Bool) $\mathit{confirmed}=\\{\mathit{tx}\to\bot\text{,
for every Transaction }\mathit{tx}\\}$

7 Map(Client $\to$ Integer) $\mathit{log\\_height}=\\{c\to 0\text{, for every
Client }c\\}$

8 Map(Client $\to$ Integer) $\mathit{log\\_quasi\\_committed\\_height}=\\{c\to
0\text{, for every Client }c\\}$

9 State_Representation $\mathit{state}=$ {

10 $\\{\mathit{tx}\to\bot$, for every Transaction $\mathit{tx}\\}$, //
$\mathit{log}$

11 $\\{c,i\to\emptyset$, for every Client $c$ and every Integer $i\\}$, //
$\mathit{allowed\\_acks}$

12 }

14 Set(Client) $\mathit{faulty\\_clients}=\emptyset$

16 Set(Transaction) $\mathit{quasi\\_committed\\_current\\_view}=\emptyset$

17 Map(Transaction, View $\to$ Set(Server))
$\mathit{commit\\_confirms\\_from}=\\{\mathit{tx},v\to\emptyset\text{, for
every Transaction }\mathit{tx}\text{ and every View }v\\}$

18 Map(Transaction, View $\to$ Set(Message))
$\mathit{commit\\_confirms}=\\{\mathit{tx},v\to\emptyset\text{, for every
Transaction }\mathit{tx}\text{ and every View }v\\}$

20 Map(Transaction, View $\to$ Set(Server))
$\mathit{committed\\_from}=\\{\mathit{tx},v\to\emptyset\text{, for every
Transaction }\mathit{tx}\text{ and every View }v\\}$

21 Map(Transaction, View $\to$ Set(Message))
$\mathit{committeds}=\\{\mathit{tx},v\to\emptyset\text{, for every Transaction
}\mathit{tx}\text{ and every View }v\\}$

23 function balance_after_height(Client $c$, Integer $\mathit{height}$):

24 Integer $\mathit{balance}=$ initial_balance($c$)

25 Integer $current\\_height=1$

26 while $\mathit{current\\_height}\leq\mathit{height}$:

27 let $\mathit{tx}$ be Transaction such that $\mathit{tx}\in\mathit{log}$ and
$\mathit{tx}.\mathit{issuer}=c$ and
$\mathit{tx}.\mathit{sn}=\mathit{current\\_height}$

28 if $\mathit{tx}$ is Withdrawal_Transaction:

29 $\mathit{balance}=\mathit{balance}-\mathit{tx}.\mathit{amount}$

30 else if $\mathit{tx}$ is Deposit_Transaction:

31
$\mathit{balance}=\mathit{balance}+\mathit{tx}.\mathit{withdrawal}.\mathit{amount}$

32 else if $\mathit{tx}$ is Minting_Transaction:

33 $\mathit{balance}=\mathit{balance}+\mathit{tx}.\mathit{amount}$

34 $\mathit{current\\_height}=\mathit{current\\_height}+1$

35 return $\mathit{balance}$

37 upon exists Message $m\in\mathit{waiting\\_messages}$ such that
$m=[$PREPARE, Transaction $\mathit{tx}$, View $v]$ and
$v=\mathit{current\\_view}.\mathit{view}$ and
$\mathit{current\\_view}.\mathit{installed}=\top$ and
$\mathit{tx}.\mathit{issuer}\notin\mathit{faulty\\_clients}$ and
$\mathit{current\\_view}.\mathit{processing}=\top$ and
$\mathit{tx}.\mathit{sn}=\mathit{log\\_height}[\mathit{tx}.\mathit{issuer}]+1$
and (if $\mathit{tx}$ is Deposit_Transaction then
$\mathit{tx}.\mathit{withdrawal}\in\mathit{log}$):

38 $\mathit{waiting\\_messages}=\mathit{waiting\\_messages}\setminus{\\{m\\}}$

40 // check whether the server is allowed to send ACK

41 if
$\mathit{state}.\mathit{allowed\\_acks}[\mathit{tx}.\mathit{issuer}][\mathit{tx}.\mathit{sn}]=\emptyset$
or
$\mathit{state}.\mathit{allowed\\_acks}[\mathit{tx}.\mathit{issuer}][\mathit{tx}.\mathit{sn}]=\\{\mathit{tx}\\}$:

42 if $\mathit{tx}$ is Withdrawal_Transaction:

43 if $\mathit{tx}.\mathit{amount}>$
balance_after_height($\mathit{tx}.\mathit{issuer}$,
$\mathit{tx}.\mathit{sn}-1$): // not enough money

44 return

45 else if $\mathit{tx}$ is Deposit_Transaction: // deposit transaction

46 if exists Transaction $\mathit{tx}^{\prime}\in\mathit{log}$ such that
$\mathit{tx}^{\prime}$ is Deposit_Transaction and
$\mathit{tx}^{\prime}.\mathit{issuer}=\mathit{tx}.\mathit{issuer}$ and
$\mathit{tx}^{\prime}.\mathit{withdrawal}=\mathit{tx}.\mathit{withdrawal}$: //
withdrawal already used

47 return

48 else if $\mathit{tx}$ is Vote_Transaction: // vote transaction

49 if exists Transaction $\mathit{tx}^{\prime}\in\mathit{log}$ such that
$\mathit{tx}^{\prime}$ is Vote_Transaction and
$\mathit{tx}^{\prime}.\mathit{issuer}=\mathit{tx}.\mathit{issuer}$ and
$\mathit{tx}^{\prime}.\mathit{motion}=\mathit{tx}.\mathit{motion}$: // the
motion is already being voted for

50 return

51
$\mathit{state}.\mathit{allowed\\_acks}[\mathit{tx}.\mathit{issuer}][\mathit{tx}.\mathit{sn}]=\\{\mathit{tx}\\}$

52 send $[$ACK, $\mathit{tx}$, $v$, $\mathit{view\\_path}[v]]$ to
$\mathit{tx}.\mathit{issuer}$

53 else:

54 // new proof of misbehavior discovered

55
$\mathit{state}.\mathit{allowed\\_acks}[\mathit{tx}.\mathit{issuer}][\mathit{tx}.\mathit{sn}]=\mathit{state}.\mathit{allowed\\_acks}[\mathit{tx}.\mathit{issuer}][\mathit{tx}.\mathit{sn}]\cup\\{\mathit{tx}\\}$

56
$\mathit{faulty\\_clients}=\mathit{faulty\\_clients}\cup\\{\mathit{tx}.\mathit{issuer}\\}$

58 function allowed_to_commit_confirm(Transaction $\mathit{tx}$):

59 if $\mathit{tx}\in\mathit{log}$:

60 return $\top$

62 if
$\mathit{tx}.\mathit{sn}\neq\mathit{log\\_height}[\mathit{tx}.\mathit{issuer}]+1$:

63 return $\bot$

65 if $\mathit{tx}$ is Withdrawal_Transaction or $\mathit{tx}$ is
Vote_Transaction or $\mathit{tx}$ is Minting_Transaction:

66 return $\top$

67 else:

68 return $\mathit{tx}.\mathit{withdrawal}\in\mathit{log}$

70 upon exists Message $m\in\mathit{waiting\\_messages}$ such that
$m=[$COMMIT, Transaction $\mathit{tx}$, Set(Message) $\mathit{certificate}$,
View $v]$ and verify_transaction_certificate($\mathit{tx}$,
$\mathit{certificate}$) $=\top$ and $v=\mathit{current\\_view}.\mathit{view}$
and $\mathit{current\\_view}.\mathit{installed}=\top$ and
$\mathit{current\\_view}.\mathit{processing}=\top$ and
allowed_to_commit_confirm($\mathit{tx}$) $=\top$:

71 $\mathit{waiting\\_messages}=\mathit{waiting\\_messages}\setminus{\\{m\\}}$

72 // first sight of the commit message

73 if $\mathit{tx}\notin\mathit{log}$:

74 // update the state representation

75 $\mathit{state}.\mathit{log}[\mathit{tx}]=m$

77 $\mathit{log}=\mathit{log}\cup\\{\mathit{tx}\\}$

78
$\mathit{log\\_height}[\mathit{tx}.\mathit{issuer}]=\mathit{tx}.\mathit{sn}$

80 broadcast $[$COMMIT, $\mathit{tx}$, $\mathit{certificate}$, $v]$ to
$v$.members()

82 send $[$COMMIT-CONFIRM, $\mathit{tx}$, $v$, $\mathit{view\\_path}[v]]$ to
$m$.sender // confirm to the sender, not to the $\mathit{tx}.\mathit{issuer}$

84 upon exists Message $m\in\mathit{waiting\\_messages}$ such that
$m=[$COMMIT-CONFIRM, Transaction $\mathit{tx}$, View $v$, View_Path
$\mathit{path}]$ and $\mathit{path}$.destination() $=v$ and $m$.sender $\in
v$.members() and $\mathit{tx}\in\mathit{log}$:

85 $\mathit{waiting\\_messages}=\mathit{waiting\\_messages}\setminus{\\{m\\}}$

86 if $m$.sender $\notin\mathit{commit\\_confirms\\_from}[\mathit{tx}][v]$:

87
$\mathit{commit\\_confirms\\_from}[\mathit{tx}][v]=\mathit{commit\\_confirms\\_from}[\mathit{tx}][v]\cup\\{m.$sender$\\}$

88
$\mathit{commit\\_confirms}[\mathit{tx}][v]=\mathit{commit\\_confirms}[\mathit{tx}][v]\cup\\{m\\}$

90 function allowed_to_quasi_commit(Transaction $\mathit{tx}$):

91 if $\mathit{tx}\notin\mathit{log}$ or
$\mathit{quasi\\_committed}[\mathit{tx}]=\top$:

92 return $\bot$

94 if
$\mathit{log\\_quasi\\_committed\\_height}[\mathit{tx}.\mathit{issuer}]+1\neq\mathit{tx}.\mathit{sn}$:

95 return $\bot$

97 if $\mathit{tx}$ is Deposit_Transaction and
($\mathit{tx}.\mathit{withdrawal}\notin\mathit{log}$ or
$\mathit{quasi\\_committed}[\mathit{tx}.\mathit{withdrawal}]=\bot$):

98 return $\bot$

100 if (exists View $v^{*}$ such that
$|\mathit{commit\\_confirms\\_from}[\mathit{tx}][v^{*}]|\geq v^{*}$.quorum())
$=\bot$:

101 return $\bot$

103 let $v$ be the smallest View such that
$|\mathit{commit\\_confirms\\_from}[\mathit{tx}][v]|\geq v$.quorum()

104 if $v\subset\mathit{current\\_view}.\mathit{view}$:

105 return $\top$

106 else: // $v=\mathit{current\\_view}.\mathit{view}$

107 if $\mathit{quasi\\_committed\\_current\\_view}=\emptyset$:

108 return $\top$

109 Set(Server)
$\mathit{intersection}=\bigcap\limits_{\mathit{tx}^{\prime}\in\mathit{quasi\\_committed\\_current\\_view}}\mathit{commit\\_confirms\\_from}[\mathit{tx}^{\prime}][v]$

110 return
$|\mathit{commit\\_confirms\\_from}[\mathit{tx}][v]\cap\mathit{intersection}|\geq
v$.quorum()

112 upon exists Transaction $\mathit{tx}$ such that
allowed_to_quasi_commit($\mathit{tx}$) $=\top$:

113 $\mathit{quasi\\_committed}[\mathit{tx}]=\top$

114
$\mathit{log\\_quasi\\_committed\\_height}[\mathit{tx}.\mathit{issuer}]=\mathit{tx}.\mathit{sn}$

116 let $v$ be the smallest View such that
$\mathit{commit\\_confirms\\_from}[\mathit{tx}][v]\geq v$.quorum()

117 if $v=\mathit{current\\_view}.\mathit{view}$:

118
$\mathit{quasi\\_committed\\_current\\_view}=\mathit{quasi\\_committed\\_current\\_view}\cup\\{\mathit{tx}\\}$

120 upon exists Message $m\in\mathit{waiting\\_messages}$ such that
$m=[$COMMITTED, Transaction $\mathit{tx}$, View $v$, View_Path
$\mathit{path}]$ and $\mathit{path}$.destination() $=v$ and $m$.sender $\in
v$.members():

121
$\mathit{waiting\\_messages}=\mathit{waiting\\_messages}\setminus{\\{m\\}}$

122 if $m$.sender $\notin\mathit{committed\\_from}[\mathit{tx}][v]$:

123
$\mathit{committed\\_from}[\mathit{tx}][v]=\mathit{committed\\_from}[\mathit{tx}][v]\cup\\{m.\mathtt{sender}\\}$

124
$\mathit{committeds}[\mathit{tx}][v]=\mathit{committeds}[\mathit{tx}][v]\cup\\{m\\}$

126 function allowed_to_broadcast_committed(Transaction $\mathit{tx}$):

127 if $\mathit{quasi\\_committed}[\mathit{tx}]=\bot$:

128 return $\bot$

130 if $\mathit{tx}.\mathit{sn}=1$ and $\mathit{tx}$ is not
Deposit_Transaction:

131 return $\top$

133 if $\mathit{tx}.\mathit{sn}=1$:

134 return $\mathit{confirmed}[\mathit{tx}.\mathit{withdrawal}]$

136 if $\mathit{tx}$ is not Deposit_Transaction:

137 return exists Transaction $\mathit{tx}^{\prime}$ such that
$\mathit{tx}^{\prime}.\mathit{issuer}=\mathit{tx}.\mathit{issuer}$ and
$\mathit{tx}^{\prime}.\mathit{sn}=\mathit{tx}.\mathit{sn}-1$ and
$\mathit{confirmed}[\mathit{tx}^{\prime}]=\top$

139 return (exists Transaction $\mathit{tx}^{\prime}$ such that
$\mathit{tx}^{\prime}.\mathit{issuer}=\mathit{tx}.\mathit{issuer}$ and
$\mathit{tx}^{\prime}.\mathit{sn}=\mathit{tx}.\mathit{sn}-1$ and
$\mathit{confirmed}[\mathit{tx}^{\prime}]=\top$) and
$\mathit{confirmed}[\mathit{tx}.\mathit{withdrawal}]=\top$

141 upon exists Transaction $\mathit{tx}$ such that
allowed_to_broadcast_committed($\mathit{tx}$) $=\top$ and
$\mathit{current\\_view}.\mathit{installed}=\top$:

142 broadcast $[$COMMITTED, $\mathit{tx}$,
$\mathit{current\\_view}.\mathit{view}$,
$\mathit{view\\_path}[\mathit{current\\_view}.\mathit{view}]]$ to
$\mathit{current\\_view}.\mathit{view}$.members()

144 upon exist Transaction $\mathit{tx}$ and View $v$ such that
$\mathit{committed\\_from}[\mathit{tx}][v]\geq v$.plurality():

145 $\mathit{confirmed}[\mathit{tx}]=\top$

146 send $\mathit{committeds}[\mathit{tx}][v]$ to
$\mathit{tx}.\mathit{issuer}$

147 if $\mathit{tx}$ is Withdrawal_Transaction:

148 send $\mathit{committeds}[\mathit{tx}][v]$ to
$\mathit{tx}.\mathit{receiver}$

150 upon exists Message $m\in\mathit{waiting\\_messages}$ such that
$m=[$QUERY, Integer $\mathit{qid}$, View $v]$ and
$v=\mathit{current\\_view}.\mathit{view}$ and
$\mathit{current\\_view}.\mathit{installed}=\top$ and
$\mathit{current\\_view}.\mathit{processing}=\top$:

151
$\mathit{waiting\\_messages}=\mathit{waiting\\_messages}\setminus{\\{m\\}}$

152 Log
$\mathit{quasi\\_committed\\_log}=\\{\mathit{tx}\,|\,\mathit{quasi\\_committed}[\mathit{tx}]=\top\\}$

153 send $[$QUERY-RESPONSE, $\mathit{quasi\\_committed\\_log}$.total_money(),
$\mathit{qid}$, $v$, $\mathit{view\\_path}[v]]$ to $m$.sender

155 function refine_state(Set(State_Representation) $\mathit{states}$): //
$\mathit{states}\neq\emptyset$

156 for each State_Representation $\mathit{rec\\_state}\in\mathit{states}$:

157 for each Client $c$ and Integer $i$ such that
$\mathit{rec\\_state}.\mathit{allowed\\_acks}[c][i]\neq\bot$:

158
$\mathit{state}.\mathit{allowed\\_acks}[c][i]=\mathit{state}.\mathit{allowed\\_acks}[c][i]\cup\mathit{rec\\_state}.\mathit{allowed\\_acks}[c][i]$

160 if $\mathit{state}$.verify() $=\top$:

161 for each State_Representation $\mathit{rec\\_state}\in\mathit{states}$:

162 $\mathit{state}.\mathit{log}=$ merge_logs($\mathit{state}$,
$\mathit{rec\\_state}$) // from LABEL:lst:state_representation

164 $\mathit{log}=\mathit{state}$.extract_log() //
$\mathit{committed}[\mathit{tx}]=\bot$, for every newly inserted transaction

165 for each Client $c$:

166 Log
$\mathit{client\\_log}=\\{\mathit{tx}\,|\,\mathit{tx}\in\mathit{log}\text{ and
}\mathit{tx}.\mathit{issuer}=c\\}$

167 $\mathit{log\\_height}[c]=|\mathit{client\\_log}|$

168 // $\mathit{log\\_quasi\\_committed\\_height}[c]$ does not change

169 $\mathit{faulty\\_clients}=\\{c\,|\,\text{exists Integer }i\text{ such
that }|\mathit{state}.\mathit{allowed\\_acks}[c][i]|\geq 2\\}$

171 function installed(View $v$):

172 $\mathit{quasi\\_committed\\_current\\_view}=\emptyset$

173 // try to quasi-commit non-quasi-committed transactions

174 for each Transaction $\mathit{tx}\in\mathit{log}$ such that
$\mathit{quasi\\_committed}[\mathit{tx}]=\bot$:

175 let $\mathit{state}.\mathit{log}[\mathit{tx}]=[$COMMIT, $\mathit{tx}$,
Set(Message) $\mathit{certificate}$, View $v^{\prime}]$

176 broadcast $[$COMMIT, $\mathit{tx}$, $\mathit{certificate}$, $v]$ to
$v$.members()

Listing 39: Transaction module - implementation

##### Proof of correctness.

We now prove the commitment validity, integrity, learning, admissibility and
signing property of Carbon (see § 3.3). The first property we prove is the
commitment integrity.

###### Theorem 1 (Commitment Integrity).

Commitment integrity is satisfied.

###### Proof.

Let a transaction $\mathit{tx}$ be committed and let
$\mathit{tx}.\mathit{issuer}$ be correct. Since $\mathit{tx}$ is committed, a
(correct or faulty) process has obtained a commitment proof $\sigma_{c}$ such
that $\mathtt{verify\\_commit}(\mathit{tx},\sigma_{c})=\top$ (see § 3.1,
paragraph “Commitment proofs”). Since $\sigma_{c}$ is a collection of
$\mathtt{COMMITTED}$ messages that contain $\mathit{tx}$ signed by
$\mathit{tx}.\mathit{issuer}$ (see LABEL:lst:commitment_proof_verification),
$\mathit{tx}.\mathit{issuer}$ has issued $\mathit{tx}$ (since
$\mathit{tx}.\mathit{issuer}$ signs $\mathit{tx}$ upon issuing it; line 44 of
LABEL:lst:client). Hence, the theorem holds. ∎

The next property we prove is the commitment admissibility property. In order
to prove the property, we first define _certified_ transactions.

###### Definition 0 (Certified Transaction).

A transaction $\mathit{tx}$ is _certified_ if and only if a (correct or
faulty) process obtains a set of messages $\mathit{certificate}$ such that
$\mathtt{verify\\_transaction\\_certificate}(\mathit{tx},\mathit{certificate})=\top$.
Moreover, if the view specified in the $\mathtt{ACK}$ messages of
$\mathit{certificate}$ (see LABEL:lst:transaction_certificate_verification) is
$v$, then $\mathit{tx}$ is certified in $v$.

Next lemma proves that a transaction can be certified only in a view that is
installable at time $\infty$.

###### Lemma 0.

Let a transaction $\mathit{tx}$ be certified in a view $v$. Then,
$\alpha_{\infty}(v)=\top$.

###### Proof.

Since $\mathit{tx}$ is certified in $v$, at least a single correct server
$r\in v.\mathtt{members()}$ sends the $\mathtt{ACK}$ message associated with
$v$ for $\mathit{tx}$ (see LABEL:lst:transaction_certificate_verification);
note that $v$ is a valid view since every $\mathtt{ACK}$ message is
accompanied by a view-path to $v$ (by line 2 of
LABEL:lst:transaction_certificate_verification). Since a correct member of $v$
sends the message at line 52 of LABEL:lst:transaction_module, $v$ is installed
at that correct server (by the check at line 37 of
LABEL:lst:transaction_module). If $v=\mathit{genesis}$,
$\alpha_{\infty}(\mathit{genesis})=\top$ (by definition) and the lemma holds.
Otherwise, $\alpha_{\infty}(v)=\top$ (similarly to Lemma 9) and the lemma is
concluded. ∎

The important result before proving the commitment admissibility property is
that conflicting transactions cannot be certified. In order to prove this
statement, we first show that no transaction stored in the
$\mathit{state}.\mathit{allowed\\_acks}$ variable of a correct server is ever
removed.

###### Lemma 0.

Consider any client $c$ and any integer $i$. Let $\mathit{allowed\\_acks}_{t}$
be the value of the $\mathit{state}.\mathit{allowed\\_acks}[c][i]$ variable at
a correct server $r$ at time $t$. Let $\mathit{allowed\\_acks}_{t^{\prime}}$
be the value of the $\mathit{state}.\mathit{allowed\\_acks}[c][i]$ variable at
$r$ at time $t^{\prime}>t$. Then,
$\mathit{allowed\\_acks}_{t}\subseteq\mathit{allowed\\_acks}_{t^{\prime}}$.

###### Proof.

The lemma follows from the fact that no transaction is ever removed from the
$\mathit{state}.\mathit{allowed\\_acks}$ variable at a correct server (see
LABEL:lst:transaction_module). ∎

The next lemma shows that two conflicting transactions cannot be certified in
the same view.

###### Lemma 0.

Let transactions $\mathit{tx}$ and $\mathit{tx}^{\prime}$ be certified in a
view $v$ such that (1)
$\mathit{tx}.\mathit{issuer}=\mathit{tx}^{\prime}.\mathit{issuer}$, and (2)
$\mathit{tx}.\mathit{sn}=\mathit{tx}^{\prime}.\mathit{sn}$. Then,
$\mathit{tx}=\mathit{tx}^{\prime}$.

###### Proof.

By contradiction, let $\mathit{tx}\neq\mathit{tx}^{\prime}$. By Lemma 3, $v$
is installable at time $\infty$ (i.e., $\alpha_{\infty}(v)=\top$). Moreover,
$v$ is a valid view. Hence, at least quorum of members of $v$ are correct (see
§ 2, paragraph “Failure model”).

Since $\mathit{tx}$ (resp., $\mathit{tx}^{\prime}$) is certified in $v$, a
quorum of members of $v$ have sent the $\mathtt{ACK}$ message associated with
$v$ for $\mathit{tx}$ (resp., $\mathit{tx}^{\prime}$), by
LABEL:lst:transaction_certificate_verification. Because of the quorum
intersection, there exists a correct server $r\in v.\mathtt{members()}$ that
has sent $\mathtt{ACK}$ messages for both transactions. Without loss of
generality, suppose that $r$ has sent the $\mathtt{ACK}$ message for
$\mathit{tx}$ before the $\mathtt{ACK}$ message for $\mathit{tx}^{\prime}$.

At the moment of sending the $\mathtt{ACK}$ message for $\mathit{tx}$,
$\mathit{state}.\mathit{allowed\\_acks}[\mathit{tx}.\mathit{issuer}][\mathit{tx}.\mathit{sn}]=\\{\mathit{tx}\\}$
at server $r$ (by line 51 of LABEL:lst:transaction_module). Similarly, at the
moment of sending the $\mathtt{ACK}$ message for $\mathit{tx}^{\prime}$,
$\mathit{state}.\mathit{allowed\\_acks}[\mathit{tx}^{\prime}.\mathit{issuer}=\mathit{tx}.\mathit{issuer}][\mathit{tx}^{\prime}.\mathit{sn}=\mathit{tx}.\mathit{sn}]=\\{\mathit{tx}^{\prime}\\}$
(by line 51 of LABEL:lst:transaction_module). This is impossible due to Lemma
4, hence $r$ does not send both $\mathtt{ACK}$ messages. Therefore,
$\mathit{tx}\neq\mathit{tx}^{\prime}$ and the lemma holds. ∎

Now, we prove that any correct member of a view $v^{\prime}\supset v$ is aware
of the fact that a transaction $\mathit{tx}$ is certified in a view $v$, if
that is indeed the case.

###### Lemma 0.

Let a transaction $\mathit{tx}$ be certified in a view $v$. Consider time $t$
and a correct server $r\in v^{\prime}.\mathtt{members()}$ with
$\mathit{current\\_view}.\mathit{view}=v^{\prime}$ at server $r$ at time $t$,
where $v^{\prime}\supset v$. Then,
$\mathit{tx}\in\mathit{state}.\mathit{allowed\\_acks}[\mathit{tx}.\mathit{issuer}][\mathit{tx}.\mathit{sn}]$
at server $r$ at time $t$.

###### Proof.

By Lemma 3, $v$ is installable at time $\infty$ (i.e.,
$\alpha_{\infty}(v)=\top$). Moreover, $v$ is a valid view.

Let $t^{*}$ be the first time at which a correct server sets its
$\mathit{current\\_view}.\mathit{view}$ variable to a view greater than $v$;
let us denote that server by $r^{*}$ and the view by $v^{*}$. We now prove
that the statement of the lemma holds at time $t^{*}$ at server $r^{*}$.

Since $v\subset v^{*}$, $v^{*}\neq\mathit{genesis}$ (by Lemma 45). Hence,
$r^{*}$ has executed line 29 of LABEL:lst:reconfiguration_view_transition.
This implies that
$\mathit{reconfiguration}.\mathit{destination}=v^{*}$ at that time at server
$r^{*}$. Furthermore, $\mathit{reconfiguration}.\mathit{source}=v$. Let us
prove this claim. If $\mathit{reconfiguration}.\mathit{source}\subset v$, this
fact conflicts with Lemma 56. If
$\mathit{reconfiguration}.\mathit{source}\supset v$, then $t^{*}$ would not be
the first time at which a correct server sets its
$\mathit{current\\_view}.\mathit{view}$ variable to a view greater than $v$
(since the $\mathtt{INSTALL}$ message $m$ is obtained, where
$m.\mathtt{source()}\supset v$). Finally,
$\mathit{reconfiguration}.\mathit{prepared}=\top$ at server $r^{*}$.

Since $r^{*}\in v^{*}.\mathtt{members}()$, $r^{*}$ has not executed line 10 of
LABEL:lst:reconfiguration_view_transition. Let us investigate both places at
which $r^{*}$ could have set its $\mathit{reconfiguration}.\mathit{prepared}$
variable to $\top$:

  * •

line 41 of LABEL:lst:reconfiguration_state_transfer: Server $r^{*}$ has
received $\mathtt{STATE-UPDATE}$ messages from a quorum of members of $v$
(recall that $\mathit{reconfiguration}.\mathit{source}=v$ at that time). By
the quorum intersection, there exists a correct server $R$ such that (1) $R$
has sent the $\mathtt{ACK}$ message for $\mathit{tx}$ in view $v$, and (2)
$r^{*}$ has received the $\mathtt{STATE-UPDATE}$ message from $R$.

First, we show that $R$ has sent the $\mathtt{ACK}$ message before the
$\mathtt{STATE-UPDATE}$ message. By contradiction, suppose that $R$ has sent
the $\mathtt{STATE-UPDATE}$ message to $r^{*}$ before the $\mathtt{ACK}$
message. At the moment of sending the $\mathtt{STATE-UPDATE}$ message (line 14
of LABEL:lst:reconfiguration_state_transfer),
$\mathit{current\\_view}.\mathit{view}$ at server $R$ is smaller than or equal
to $v$ or is equal to $\bot$ (otherwise, $t^{*}$ would not be the first time
at which a correct server sets its $\mathit{current\\_view}.\mathit{view}$
variable to a view greater than $v$). Hence, the
$\mathit{stop\\_processing\\_until}$ variable (set at line 12 of
LABEL:lst:reconfiguration_state_transfer) at server $R$ is at least equal to
$v$ at that time. Therefore, the check at line 37 of
LABEL:lst:transaction_module does not pass while
$\mathit{current\\_view}.\mathit{view}=v$ (since
$\mathit{current\\_view}.\mathit{processing}=\bot$; see
LABEL:lst:reconfiguration_view_transition), which means that $R$ does not send
the $\mathtt{ACK}$ message associated with view $v$. Hence, we reach
contradiction.

At the moment of sending the $\mathtt{ACK}$ message for $\mathit{tx}$
associated with view $v$,
$\mathit{state}.\mathit{allowed\\_acks}[\mathit{tx}.\mathit{issuer}][\mathit{tx}.\mathit{sn}]=\\{\mathit{tx}\\}$
at server $R$ (by line 51 of LABEL:lst:transaction_module). Therefore, by
Lemma 4, at the moment of sending the $\mathtt{STATE-UPDATE}$ message to
$r^{*}$,
$\mathit{tx}\in\mathit{state}.\mathit{allowed\\_acks}[\mathit{tx}.\mathit{issuer}][\mathit{tx}.\mathit{sn}]$
at server $R$. After executing the $\mathtt{refine\\_state}$ function (see
LABEL:lst:transaction_module),
$\mathit{tx}\in\mathit{state}.\mathit{allowed\\_acks}[\mathit{tx}.\mathit{issuer}][\mathit{tx}.\mathit{sn}]$
at server $r^{*}$. By Lemma 4, the statement of the lemma holds for $r^{*}$ at
time $t^{*}$.

  * •

line 47 of LABEL:lst:reconfiguration_state_transfer: This scenario is
impossible since it contradicts the fact that $t^{*}$ is the first time at
which a correct server sets its $\mathit{current\\_view}.\mathit{view}$
variable to a view greater than $v$.

Note that, because of Lemma 4, the statement of the lemma is satisfied at
server $r^{*}$ at all times after time $t^{*}$.

Next, we introduce the following invariant. Consider time $t^{**}$ and a
server $r^{**}$ such that $\mathit{current\\_view}.\mathit{view}=v^{**}$ at
server $r^{**}$ at time $t^{**}$, where $v\subset v^{**}$. Then, the statement
of the lemma holds at server $r^{**}$ at time $t^{**}$. Note that this
invariant is satisfied at time $t^{*}$, which is the first time at which these
conditions are satisfied.

Consider a server $r^{\prime}$ that sets its
$\mathit{current\\_view}.\mathit{view}$ variable to $v^{\prime}\supset v$.
Hence, $\mathit{reconfiguration}.\mathit{prepared}=\top$ at server
$r^{\prime}$. Moreover, $\mathit{reconfiguration}.\mathit{source}\supseteq v$
(otherwise, Lemma 56 is contradicted). Let us investigate both places at which
$r^{\prime}$ could have set its $\mathit{reconfiguration}.\mathit{prepared}$
variable to $\top$:

  * •

line 41 of LABEL:lst:reconfiguration_state_transfer: If
$\mathit{reconfiguration}.\mathit{source}\supset v$, we know that a correct
process from which $r^{\prime}$ has received the $\mathtt{STATE-UPDATE}$
message has its $\mathit{current\\_view}.\mathit{view}$ greater than $v$ at
the moment of sending the $\mathtt{STATE-UPDATE}$ message (because of the
obtained $\mathtt{INSTALL}$ message $m$, where $m.\mathtt{source()}\supset v$
and the quorum intersection). Thus, the invariant is preserved since the
invariant holds for a correct server from which $r^{\prime}$ receives the
$\mathtt{STATE-UPDATE}$ message (see the $\mathtt{refine\\_state}$ function in
LABEL:lst:state_representation).

If $\mathit{reconfiguration}.\mathit{source}=v$, then $r^{\prime}$ has
received the $\mathtt{STATE-UPDATE}$ messages from at least
$v.\mathtt{plurality}()$ of correct members of $v$. If at least a single such
member had $\mathit{current\\_view}.\mathit{view}$ variable equal to a view
greater than $v$ at the moment of sending the $\mathtt{STATE-UPDATE}$ message,
the invariant is preserved because of the invariant hypothesis (and the
$\mathtt{refine\\_state}$ function). Otherwise, the invariant is preserved
because of the argument given in the base step. The statement of the lemma is
preserved for server $r^{\prime}$ forever by Lemma 4.

  * •

line 47 of LABEL:lst:reconfiguration_state_transfer: Since
$\mathit{reconfiguration}.\mathit{source}\supseteq v$, the invariant is
preserved because of the invariant hypothesis (and the
$\mathtt{state\\_refine}$ function).

Since the invariant is preserved, the lemma holds. ∎

The next lemma proves that two conflicting transactions cannot be certified in
different views.

###### Lemma 0.

Let a transaction $\mathit{tx}$ be certified in a view $v$. Let a transaction
$\mathit{tx}^{\prime}$ be certified in a view $v^{\prime}\neq v$. Moreover,
let (1) $\mathit{tx}.\mathit{issuer}=\mathit{tx}^{\prime}.\mathit{issuer}$,
and (2) $\mathit{tx}.\mathit{sn}=\mathit{tx}^{\prime}.\mathit{sn}$. Then,
$\mathit{tx}=\mathit{tx}^{\prime}$.

###### Proof.

By contradiction, let $\mathit{tx}\neq\mathit{tx}^{\prime}$. By Lemma 3, $v$
and $v^{\prime}$ are installable views at time $\infty$. Therefore, both views
are valid. By the view comparability property, $v$ and $v^{\prime}$ are
comparable. Without loss of generality, let $v\subset v^{\prime}$.

Since $\mathit{tx}^{\prime}$ is certified in $v^{\prime}$, there exists a
correct server $r^{\prime}$ that sends the $\mathtt{ACK}$ message for
$\mathit{tx}^{\prime}$ associated with view $v^{\prime}$ (at line 52 of
LABEL:lst:transaction_module). By line 51 of LABEL:lst:transaction_module,
$\mathit{state}.\mathit{allowed\\_acks}[\mathit{tx}^{\prime}.\mathit{issuer}][\mathit{tx}^{\prime}.\mathit{sn}]=\\{\mathit{tx}^{\prime}\\}$
at server $r^{\prime}$ at that time.

Let $r^{\prime}$ set its $\mathit{current\\_view}.\mathit{view}$ variable to
$v^{\prime}$ at some time $t_{v^{\prime}}$; note that this indeed happens
since $r^{\prime}$ sends the $\mathtt{ACK}$ message associated with
$v^{\prime}$ (by the check at line 37 of LABEL:lst:transaction_module).
Because of Lemma 6,
$\mathit{tx}\in\mathit{state}.\mathit{allowed\\_acks}[\mathit{tx}.\mathit{issuer}=\mathit{tx}^{\prime}.\mathit{issuer}][\mathit{tx}.\mathit{sn}=\mathit{tx}^{\prime}.\mathit{sn}]$
at server $r^{\prime}$ at time $t_{v^{\prime}}$. Finally, $r^{\prime}$ sends
the $\mathtt{ACK}$ message for $\mathit{tx}^{\prime}$ after time
$t_{v^{\prime}}$ (by the check at line 37 of LABEL:lst:transaction_module,
$r^{\prime}$ has already updated its $\mathit{current\\_view}.\mathit{view}$
variable to $v^{\prime}$). Recall that
$\mathit{state}.\mathit{allowed\\_acks}[\mathit{tx}^{\prime}.\mathit{issuer}][\mathit{tx}^{\prime}.\mathit{sn}]=\\{\mathit{tx}^{\prime}\\}$
at server $r^{\prime}$ at that time. This is impossible due to Lemma 4, which
implies that $\mathit{tx}=\mathit{tx}^{\prime}$. ∎

Finally, we prove that conflicting transactions cannot be certified.

###### Lemma 0 (Conflicting Transactions Cannot Be Certified).

Let transactions $\mathit{tx}$ and $\mathit{tx}^{\prime}$ be certified such
that (1) $\mathit{tx}.\mathit{issuer}=\mathit{tx}^{\prime}.\mathit{issuer}$,
and (2) $\mathit{tx}.\mathit{sn}=\mathit{tx}^{\prime}.\mathit{sn}$. Then,
$\mathit{tx}=\mathit{tx}^{\prime}$.

###### Proof.

Let $v$ denote the smallest view in which $\mathit{tx}$ is certified and let
$v^{\prime}$ denote the smallest view in which $\mathit{tx}^{\prime}$ is
certified. Since $v$ and $v^{\prime}$ are valid views (follows from Lemma 3),
$v$ and $v^{\prime}$ are comparable (by the view comparability property
defined in LABEL:lst:reconfiguration_properties_new; see Theorem 50). If
$v=v^{\prime}$, the lemma follows from Lemma 5. Otherwise, the lemma follows
from Lemma 7. ∎

The next lemma proves that the $\mathit{state}.\mathit{log}$ variable at a
correct server only “grows”.

###### Lemma 0.

Consider a correct server $r$. Let
$\mathit{log}_{t}^{r}=\\{\mathit{tx}\,|\,\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot\text{
at server }r\text{ at some time }t\\}$. Let
$\mathit{log}_{t^{\prime}}^{r}=\\{\mathit{tx}\,|\,\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot\text{
at server }r\text{ at some time }t^{\prime}>t\\}$. Then,
$\mathit{log}_{t}^{r}\subseteq\mathit{log}_{t^{\prime}}^{r}$.

###### Proof.

In order to prove the lemma, we prove that
$\mathit{state}.\mathit{log}[\mathit{tx}]$, for any transaction $\mathit{tx}$,
is never reverted to $\bot$. Therefore, we consider all the place at which
$\mathit{state}.\mathit{log}$ variable at server $r$ changes:

  * •

line 75 of LABEL:lst:transaction_module: The invariant is trivially preserved
in this case.

  * •

line 162 of LABEL:lst:transaction_module: In this case, the invariant is
preserved because of the $\mathtt{merge\\_logs}$ function (see
LABEL:lst:state_representation).

Therefore, the lemma holds. ∎

The next important intermediate result we show is that
$\mathit{state}.\mathtt{verify()}=\top$ at a correct server at all times. In
order to do so, we prove that the $\mathtt{merge\\_logs}$ function (see
LABEL:lst:state_representation) invoked with two “valid” states (according to
the $\mathtt{verify()}$ function) returns an admissible log.

###### Lemma 0.

Let $\mathit{state}_{1}$ (resp., $\mathit{state}_{2}$) be a state
representation such that $\mathit{state}_{1}.\mathtt{verify()}=\top$ (resp.,
$\mathit{state}_{2}.\mathtt{verify()}=\top$). Let
$\mathit{log\\_map}=\mathtt{merge\\_logs}(\mathit{state}_{1},\mathit{state}_{2})$
and let
$\mathit{log}=\\{\mathit{tx}\,|\,\mathit{log\\_map}[\mathit{tx}]\neq\bot\\}$.
Then, $\mathit{log}$ is admissible.

###### Proof.

Let $\mathit{log}_{1}=\mathit{state}_{1}.\mathtt{extract\\_log()}$ and
$\mathit{log}_{2}=\mathit{state}_{2}.\mathtt{extract\\_log()}$. Every
transaction $\mathit{tx}\in\mathit{log}_{1}\cup\mathit{log}_{2}$ is certified
(follows from the $\mathtt{verify\\_transaction\\_proof}$ function and the
fact that
$\mathit{state}_{1}.\mathtt{verify()}=\mathit{state}_{2}.\mathtt{verify()}=\top$).
Furthermore, $\mathit{log}=\mathit{log}_{1}\cup\mathit{log}_{2}$.

We now consider the $\mathtt{admissible}(\mathit{log})$ function (see
LABEL:lst:admissible_transaction_set):

  1. (1)

The check at line 8 of LABEL:lst:admissible_transaction_set passes since
$\mathit{log}=\mathit{log}_{1}\cup\mathit{log}_{2}$ and
$\mathtt{admissible}(\mathit{log}_{1})=\mathtt{admissible}(\mathit{log}_{2})=\top$
(since
$\mathit{state}_{1}.\mathtt{verify()}=\mathit{state}_{2}.\mathtt{verify()}=\top$).

  2. (2)

Let $\mathit{log}_{c}=\\{\mathit{tx}\,|\,\mathit{tx}\in\mathit{log}\text{ and
}\mathit{tx}.\mathit{issuer}=c\\}$, for some client $c$. Let
$\mathit{log}_{c}^{1}=\\{\mathit{tx}\,|\,\mathit{tx}\in\mathit{log}_{1}\text{
and }\mathit{tx}.\mathit{issuer}=c\\}$ and
$\mathit{log}_{c}^{2}=\\{\mathit{tx}\,|\,\mathit{tx}\in\mathit{log}_{2}\text{
and }\mathit{tx}.\mathit{issuer}=c\\}$. Since
$\mathit{state}_{1}.\mathtt{verify()}=\mathit{state}_{2}.\mathtt{verify()}=\top$,
$\mathit{log}=\mathit{log}_{1}\cup\mathit{log}_{2}$ and Lemma 8,
$\mathit{log}_{c}=\mathit{log}_{c}^{1}$ or
$\mathit{log}_{c}=\mathit{log}_{c}^{2}$. Therefore,
$\mathtt{admissible\\_client\\_log}(c,\mathit{log}_{c})=\top$ (because
$\mathit{state}_{1}.\mathtt{verify()}=\mathit{state}_{2}.\mathtt{verify()}=\top$).

Therefore, $\mathit{log}$ is indeed admissible. ∎

The next lemma proves that, if
$\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot$ at a correct server, then
$\mathit{tx}$ is certified.

###### Lemma 0.

At all times, if $\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot$ at a
correct server, then $\mathit{tx}$ is certified.

###### Proof.

Initially, the statement of the lemma holds (since $\mathit{state}$ does not
“contain” any information). We introduce the invariant that the statement of
the lemma holds and we consider all the places at which
$\mathit{state}.\mathit{log}$ is modified:

  * •

line 77 of LABEL:lst:transaction_module: The invariant is preserved since the
newly inserted transaction is certified (by line 70 of
LABEL:lst:transaction_module).

  * •

line 162 of LABEL:lst:transaction_module: The invariant is preserved since
$\mathit{state}.\mathtt{verify()}=\top$ (by line 160 of
LABEL:lst:transaction_module) and
$\mathit{rec\\_state}.\mathtt{verify()}=\top$ (ensured by line 16 of
LABEL:lst:reconfiguration_state_transfer) and the $\mathtt{merge\\_logs}$
function (LABEL:lst:state_representation).

The lemma holds. ∎

The next lemma proves that $\mathit{state}.\mathtt{verify()}=\top$ at a
correct server.

###### Lemma 0.

At all times, $\mathit{state}.\mathtt{verify()}=\top$ at a correct server.

###### Proof.

Initially, $\mathit{state}.\mathtt{verify()}=\top$ (since $\mathit{state}$
does not “contain” any information). We introduce the invariant that
$\mathit{state}.\mathtt{verify()}=\top$ and check the next modification of the
variable. Let us consider all the places at which such modification can occur:

  * •

line 51 of LABEL:lst:transaction_module: The only change introduced is that
$\mathit{state}.\mathit{allowed\\_acks}[\mathit{tx}.\mathit{issuer}][\mathit{tx}.\mathit{sn}]=\\{\mathit{tx}\\}$,
for some transaction $\mathit{tx}$. The $\mathtt{verify\\_allowed\\_acks}$
function still returns $\top$, which means that the invariant is preserved.

  * •

line 55 of LABEL:lst:transaction_module: Similarly to the previous case, the
$\mathtt{verify\\_allowed\\_acks}$ function returns $\top$, which implies that
the invariant is preserved.

  * •

line 75 of LABEL:lst:transaction_module: Let $\mathit{state}_{\mathit{new}}$
be the the value of the $\mathit{state}$ variable _after_ the execution of
this line. First, note that
$\mathit{state}_{\mathit{new}}.\mathtt{extract\\_log()}=\mathit{log}\neq\bot$.
Moreover,
$\mathit{state}_{\mathit{new}}.\mathtt{verify\\_allowed\\_acks()}=\top$.
Therefore, it is left to show that $\mathit{log}$ is admissible.

Let
$\mathit{log}_{\mathit{before}}=\\{\mathit{tx}\,|\,\mathit{state}_{\mathit{before}}.\mathit{log}[\mathit{tx}]\neq\bot\\}$,
where $\mathit{state}_{\mathit{before}}$ is the value of the $\mathit{state}$
variable _before_ the execution of this line. Hence,
$\mathit{log}=\mathit{log}_{\mathit{before}}\cup\\{\mathit{tx}\\}$, where
$\mathit{tx}$ is the transaction inserted at this line. Let
$c=\mathit{tx}.\mathit{issuer}$. Let us consider the
$\mathtt{admissible}(\mathit{log})$ function (see
LABEL:lst:admissible_transaction_set):

    1. (1)

The check at line 3 of LABEL:lst:admissible_transaction_set passes due to the
construction of $\mathit{log}$.

    2. (2)

The check at line 8 of LABEL:lst:admissible_transaction_set passes since
$\mathit{log}_{\mathit{before}}$ is admissible and, if $\mathit{tx}$ is a
deposit transaction, then
$\mathit{tx}.\mathit{withdrawal}\in\mathit{log}_{\mathit{before}}$ (by the
check at line 68 of LABEL:lst:transaction_module).

    3. (3)

Consider any client $c^{\prime}\neq c$. Let
$\mathit{log}_{c^{\prime}}=\\{\mathit{tx}\,|\,\mathit{tx}\in\mathit{log}\text{
and }\mathit{tx}.\mathit{issuer}=c^{\prime}\\}$ and let
$\mathit{log}_{c^{\prime}}^{\mathit{before}}=\\{\mathit{tx}\,|\,\mathit{tx}\in\mathit{log}_{\mathit{before}}\text{
and }\mathit{tx}.\mathit{issuer}=c^{\prime}\\}$. Since the only inserted
transaction is $\mathit{tx}$ and $\mathit{tx}.\mathit{issuer}\neq c^{\prime}$,
$\mathit{log}_{c^{\prime}}=\mathit{log}_{c^{\prime}}^{\mathit{before}}$.
Hence,
$\mathtt{admissible\\_client\\_log}(c^{\prime},\mathit{log}_{c^{\prime}})=\top$
(because of the invariant). Therefore, we need to prove the same for $c$.

Let $\mathit{log}_{c}=\\{\mathit{tx}\,|\,\mathit{tx}\in\mathit{log}\text{ and
}\mathit{tx}.\mathit{issuer}=c\\}$ and
$\mathit{log}_{c}^{\mathit{before}}=\\{\mathit{tx}\,|\,\mathit{tx}\in\mathit{log}_{\mathit{before}}\text{
and }\mathit{tx}.\mathit{issuer}=c\\}$. Because of the check at line 62 of
LABEL:lst:transaction_module,
$\mathit{tx}.\mathit{sn}=|\mathit{log}_{c}^{\mathit{before}}|+1$. Consider the
$\mathtt{admissible\\_client\\_log}(c,\mathit{log}_{c})$ function:

      1. (a)

The check at line 23 of LABEL:lst:admissible_transaction_set passes since all
transactions from $\mathit{log}_{c}$ are certified (since
$\mathit{state}_{\mathit{new}}.\mathtt{extract\\_log()}\neq\bot$) and no two
conflicting transactions are certified (by Lemma 8).

      2. (b)

The check at line 27 of LABEL:lst:admissible_transaction_set passes since the
invariant holds for $\mathit{state}_{\mathit{before}}$ and
$\mathit{tx}.\mathit{sn}=|\mathit{log}_{c}^{\mathit{before}}|+1$.

      3. (c)

Since $\mathit{tx}$ (the only inserted transaction) is certified (by the check
at line 70 of LABEL:lst:transaction_module), there exists a correct server $R$
that has sent the $\mathtt{ACK}$ message for $\mathit{tx}$ (at line 52 of
LABEL:lst:transaction_module). Therefore, the check from line 40 to 45 of
LABEL:lst:admissible_transaction_set passes because of the fact that the
invariant holds for $\mathit{state}_{\mathit{before}}$, because $R$ has
executed the checks from line 42 to line 49 of LABEL:lst:transaction_module
and by lemmas 8 and 11.

Therefore, $\mathtt{admissible\\_client\\_log}(c,\mathit{log}_{c})=\top$,
which concludes the invariant preservation in this case.

  * •

line 158 of LABEL:lst:transaction_module: In this case, the invariant is
preserved since $\mathit{rec\\_state}.\mathtt{verify()}=\top$ (ensured by line
16 of LABEL:lst:reconfiguration_state_transfer).

  * •

line 162 of LABEL:lst:transaction_module: Let $\mathit{state}_{\mathit{new}}$
be the value of the $\mathit{state}$ variable _after_ executing this line.
First,
$\mathit{state}_{\mathit{new}}.\mathtt{extract\\_log()}=\mathit{log}\neq\bot$.
By Lemma 10, $\mathit{log}$ is admissible. Therefore, the invariant is
preserved.

The invariant is always preserved, thus the lemma holds. ∎

Note that Lemma 12 is crucial for the liveness of the reconfiguration module
since the proof (see § 6.2.3) assumes that correct servers always send the
“valid” (according to the $\mathtt{verify}$ function) state. Lemma 12 proves
that this is indeed the case. Finally, we are ready to prove the commitment
admissibility property.

###### Theorem 13 (Commitment Admissibility).

Commitment admissibility is satisfied.

###### Proof.

Consider $\mathit{log}_{t}$, the set of committed transactions at time $t$.
Consider a transaction $\mathit{tx}\in\mathit{log}_{t}$. Since
$\mathit{tx}\in\mathit{log}_{t}$ (i.e., $\mathit{tx}$ is committed), there
exists a correct server that sends the $\mathtt{COMMITTED}$ message for
$\mathit{tx}$ (see LABEL:lst:commitment_proof_verification); the
$\mathtt{COMMITTED}$ message is broadcast at line 142 of
LABEL:lst:transaction_module. We start by proving the following three claims:

  1. (1)

If $\mathit{tx}.\mathit{sn}>1$, then
$\mathit{tx}^{\prime}\in\mathit{log}_{t}$, where
$\mathit{tx}^{\prime}.\mathit{issuer}=\mathit{tx}.\mathit{issuer}$ and
$\mathit{tx}^{\prime}.\mathit{sn}=\mathit{tx}.\mathit{sn}-1$. Before the
$\mathtt{COMMITTED}$ message for $\mathit{tx}$ is sent, the server checks
whether $\mathit{confirmed}[\mathit{tx}^{\prime}]=\top$ (at lines 137 or 139
of LABEL:lst:transaction_module). Therefore, $\mathit{tx}^{\prime}$ is
committed (by line 145 of LABEL:lst:transaction_module and
LABEL:lst:commitment_proof_verification).

  2. (2)

If $\mathit{tx}$ is a deposit transaction, then
$\mathit{tx}.\mathit{withdrawal}\in\mathit{log}_{t}$ (similarly to the
previous case).

  3. (3)

$\mathit{tx}$ does not precede $\mathit{tx}$ in $\mathit{log}_{t}$. By
contradiction, suppose that it does. Therefore, the entire cycle was included
in the $\mathit{log}$ variable of the sender at the moment of sending the
$\mathtt{COMMITTED}$ message. Hence, the entire cycle is stored in
$\mathit{state}.\texttt{extract\\_log()}$. Since
$\mathit{state}.\mathtt{verify()}=\top$ (by Lemma 12), this is impossible (due
to the check at line 3 of LABEL:lst:admissible_transaction_set).

Because of the $\mathtt{allowed\\_to\\_broadcast\\_committed}$ function,
$\mathit{quasi\\_committed}[\mathit{tx}]=\top$ at the server (by line 127 of
LABEL:lst:transaction_module). Therefore,
$\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot$ at the server at that time
(because of the $\mathtt{allowed\\_to\\_quasi\\_commit}$ function; by the
check at line 91 of LABEL:lst:transaction_module). Since
$\mathit{state}.\mathtt{verify()}=\top$ (by Lemma 12), $\mathit{tx}$ is
certified.

Let us now consider the $\mathtt{admissible}(\mathit{log}_{t})$ function (see
LABEL:lst:admissible_transaction_set):

  1. (1)

The check at line 3 of LABEL:lst:admissible_transaction_set passes because of
the third statement.

  2. (2)

The check at line 8 of LABEL:lst:admissible_transaction_set passes because of
the second statement.

  3. (3)

Consider a client $c$. Let
$\mathit{log}_{c}=\\{\mathit{tx}\,|\,\mathit{tx}\in\mathit{log}_{t}\text{ and
}\mathit{tx}.\mathit{issuer}=c\\}$. Since all transactions that belong to
$\mathit{log}_{t}$ are certified, no conflicting transactions are in
$\mathit{log}_{c}$ (by Lemma 8). Moreover, if a transaction
$\mathit{tx}\in\mathit{log}_{c}$, where $\mathit{tx}.\mathit{sn}>1$, then
$\mathit{tx}^{\prime}\in\mathit{log}_{c}$ with
$\mathit{tx}^{\prime}.\mathit{sn}=\mathit{tx}.\mathit{sn}-1$ (by the first
statement from the proof). Finally,
$\mathtt{admissible\\_client\\_log}(c,\mathit{log}_{c})=\top$ since, for every
transaction $\mathit{tx}\in\mathit{log}_{c}$, there exists a correct server
such that $\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot$ at some time, and
lemmas 8 and 12 hold.

Therefore, the theorem holds. ∎

Next, we define when a transaction is _quasi-committed_. In order to do so, we
define the $\mathtt{verify\\_quasi\\_committed}$ function below.

⬇

1function verify_quasi_committed(Transaction $\mathit{tx}$, Set(Message)
$\mathit{quasi\\_committed\\_certificate}$):

2 if does not exist View $v$ such that $m=[$COMMIT-CONFIRM, $\mathit{tx}$,
$v$, View_Path $\mathit{path}]$ and
$v=\mathit{path}$.destination(), for every Message
$m\in\mathit{quasi\\_committed\\_certificate}$:

3 return $\bot$

4 return
$|m.\mathtt{sender}\,|\,m\in\mathit{quasi\\_committed\\_certificate}\text{ and
}m\text{.sender}\in v\text{.members()}|\geq v$.quorum()

Listing 40: Quasi-commitment - verification

###### Definition 0 (Quasi-Committed Transaction).

We say that a transaction $\mathit{tx}$ is _quasi-committed_ if and only if a
(correct or faulty) process obtains a set of messages
$\mathit{quasi\\_committed\\_certificate}$ such that
$\mathtt{verify\\_quasi\\_committed}(\mathit{tx},\mathit{quasi\\_committed\\_certificate})=\top$.
Moreover, if the view specified in the $\mathtt{COMMIT-CONFIRM}$ messages of
$\mathit{quasi\\_committed\\_certificate}$ (see
LABEL:lst:quasi_commitment_verification) is $v$, then $\mathit{tx}$ is quasi-
committed in $v$.

Next, we prove that a transaction can be quasi-committed only in a view that
is installable at time $\infty$ (similarly to Lemma 3).

###### Lemma 0.

Let a transaction $\mathit{tx}$ be quasi-committed in a view $v$. Then,
$\alpha_{\infty}(v)=\top$.

###### Proof.

Since $\mathit{tx}$ is quasi-committed in $v$, at least a single correct
server $r\in v.\mathtt{members()}$ sends the $\mathtt{COMMIT-CONFIRM}$ message
associated with $v$ for $\mathit{tx}$ (see
LABEL:lst:quasi_commitment_verification); note that $v$ is a valid view since
every $\mathtt{COMMIT-CONFIRM}$ message is accompanied by a view-path to $v$
(by line 2 of LABEL:lst:quasi_commitment_verification). Since a correct member
of $v$ sends the message at line 82 of LABEL:lst:transaction_module, $v$ is
installed at that correct server (by the check at line 70 of
LABEL:lst:transaction_module). If $v=\mathit{genesis}$,
$\alpha_{\infty}(\mathit{genesis})=\top$ (by definition) and the lemma holds.
Otherwise, $\alpha_{\infty}(v)=\top$ (similarly to Lemma 9) and the lemma is
concluded. ∎

The next lemma proves that a quasi-committed transaction is “carried” by
servers forever.

###### Lemma 0.

Let a transaction $\mathit{tx}$ be quasi-committed in a view $v$. Consider
time $t$ and a correct server $r\in v^{\prime}.\mathtt{members()}$ with
$\mathit{current\\_view}.\mathit{view}=v^{\prime}$ at time $t$, where
$v^{\prime}\supset v$. Then,
$\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot$ at server $r$ at time $t$.

###### Proof.

By Lemma 15, $v$ is installable at time $\infty$ (i.e.,
$\alpha_{\infty}(v)=\top)$. Moreover, $v$ is a valid view.

Let time $t^{*}$ be the first time at which a correct server sets its
$\mathit{current\\_view}.\mathit{view}$ variable to a view greater than $v$;
let us denote that server by $r^{*}$ and the view by $v^{*}$. We now prove
that the statement of the lemma holds at server $r^{*}$ at time $t^{*}$.

Since $v\subset v^{*}$, $v^{*}\neq\mathit{genesis}$ (by Lemma 45). Hence,
$r^{*}$ has executed line 29 of LABEL:lst:reconfiguration_view_transition.
This implies that
$\mathit{reconfiguration}.\mathit{destination}=v^{*}$ at that time at server
$r^{*}$. Furthermore, $\mathit{reconfiguration}.\mathit{source}=v$. Let us
prove this claim. If $\mathit{reconfiguration}.\mathit{source}\subset v$, then
this fact conflicts with Lemma 56. If
$\mathit{reconfiguration}.\mathit{source}\supset v$, then $t^{*}$ would not be
the first time at which a correct server sets its
$\mathit{current\\_view}.\mathit{view}$ variable to a view greater than $v$
(since the $\mathtt{INSTALL}$ message $m$ is obtained, where
$m.\mathtt{source()}\supset v$). Finally,
$\mathit{reconfiguration}.\mathit{prepared}=\top$.

Since $r^{*}\in v^{*}.\mathtt{members}()$, $r^{*}$ has not executed line 10 of
LABEL:lst:reconfiguration_view_transition. Let us investigate both places at
which $r^{*}$ could have set its $\mathit{reconfiguration}.\mathit{prepared}$
variable to $\top$:

  * •

line 41 of LABEL:lst:reconfiguration_state_transfer: Hence, $r^{*}$ has
received $\mathtt{STATE-UPDATE}$ messages from a quorum of members of $v$
(recall that $\mathit{reconfiguration}.\mathit{source}=v$ at that time). By
the quorum intersection, we know that there is a correct server $R$ such that
(1) $R$ has sent the $\mathtt{COMMIT-CONFIRM}$ message for $\mathit{tx}$ in
view $v$, and (2) $r^{*}$ has received the $\mathtt{STATE-UPDATE}$ message
from $R$.

First, we show that $R$ has sent the $\mathtt{COMMIT-CONFIRM}$ message before
the $\mathtt{STATE-UPDATE}$ message. By contradiction, suppose that $R$ has
sent the $\mathtt{STATE-UPDATE}$ message to $r^{*}$ before the
$\mathtt{COMMIT-CONFIRM}$ message. At the moment of sending the
$\mathtt{STATE-UPDATE}$ message (line 14 of
LABEL:lst:reconfiguration_state_transfer), we know that
$\mathit{current\\_view}.\mathit{view}$ at server $R$ is smaller than or equal
to $v$ or is equal to $\bot$ (otherwise, $t^{*}$ would not be the first time
at which a correct server sets its $\mathit{current\\_view}.\mathit{view}$
variable to a view greater than $v$). Hence, the
$\mathit{stop\\_processing\\_until}$ variable (set at line 12 of
LABEL:lst:reconfiguration_state_transfer) is at least equal to $v$ at that
time. Therefore, the check at line 70 of LABEL:lst:transaction_module does not
pass while $\mathit{current\\_view}.\mathit{view}=v$ (since
$\mathit{current\\_view}.\mathit{processing}=\bot$; see
LABEL:lst:reconfiguration_view_transition), which means that $R$ does not send
the $\mathtt{COMMIT-CONFIRM}$ message associated with view $v$. Thus, we reach
contradiction.

At the moment of sending the $\mathtt{COMMIT-CONFIRM}$ message,
$\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot$ at server $R$ (by lines 73
and 75 of LABEL:lst:transaction_module). By Lemma 9,
$\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot$ at server $R$ at the moment
of sending the $\mathtt{STATE-UPDATE}$ message. Since
$\mathit{state}.\mathtt{verify()}=\top$ at server $r^{*}$ (by Lemma 12), the
check at line 160 of LABEL:lst:transaction_module passes at server $r^{*}$.
Therefore, because of the $\mathtt{merge\\_logs}$ function,
$\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot$ at server $r^{*}$ at time
$t^{*}$.

  * •

line 47 of LABEL:lst:reconfiguration_state_transfer: This scenario is
impossible since it contradicts the fact that $t^{*}$ is the first time at
which a correct server sets its $\mathit{current\\_view}.\mathit{view}$
variable to a view greater than $v$.

By Lemma 9, the statement of the lemma is satisfied at all times after time
$t^{*}$ at server $r^{*}$.

Next, we introduce the following invariant. Consider time $t^{**}$ and a
server $r^{**}$ such that $\mathit{current\\_view}.\mathit{view}=v^{**}$ at
server $r^{**}$ at time $t^{**}$, where $v\subset v^{**}$. Then, the statement
of the lemma holds at server $r^{**}$ at time $t^{**}$. Note that this
invariant is satisfied at time $t^{*}$, which is the first time at which these
conditions are satisfied.

Consider a server $r^{\prime}$ that sets its
$\mathit{current\\_view}.\mathit{view}$ variable to $v^{\prime}\supset v$.
Hence, $\mathit{reconfiguration}.\mathit{prepared}=\top$ at server
$r^{\prime}$. Moreover, $\mathit{reconfiguration}.\mathit{source}\supseteq v$
(otherwise, Lemma 56 is contradicted). Let us investigate both places at which
$r^{\prime}$ could have set its $\mathit{reconfiguration}.\mathit{prepared}$
variable to $\top$:

  * •

line 41 of LABEL:lst:reconfiguration_state_transfer: If
$\mathit{reconfiguration}.\mathit{source}\supset v$, we know that a correct
process from which $r^{\prime}$ has received $\mathtt{STATE-UPDATE}$ message
has its $\mathit{current\\_view}.\mathit{view}$ greater than $v$ at the moment
of sending the $\mathtt{STATE-UPDATE}$ message (because of the obtained
$\mathtt{INSTALL}$ message $m$, where $m.\mathtt{source()}\supset v$ and the
quorum intersection). Hence, the invariant is preserved since
$\mathit{state}.\mathtt{verify()}=\top$ (by Lemma 12), which means that the
check at line 160 of LABEL:lst:transaction_module passes, and the invariant
holds for a server from which $r^{\prime}$ has received the $\mathtt{STATE-
UPDATE}$ message (see the $\mathtt{merge\\_logs}$ function).

If $\mathit{reconfiguration}.\mathit{source}=v$, then $r^{\prime}$ has
received the $\mathtt{STATE-UPDATE}$ messages from at least
$v.\mathtt{plurality}()$ of correct members of $v$. If at least a single such
member had $\mathit{current\\_view}.\mathit{view}$ variable equal to a view
greater than $v$ at the moment of sending the $\mathtt{STATE-UPDATE}$ message,
the invariant is preserved because the check at line 160 of
LABEL:lst:transaction_module passes at $r^{\prime}$ (by Lemma 12) and the
invariant hypothesis. Otherwise, the invariant is preserved because of the
argument given in the base step.

  * •

line 47 of LABEL:lst:reconfiguration_state_transfer: Since
$\mathit{reconfiguration}.\mathit{source}\supseteq v$, the invariant is
preserved because of the check at line 160 of LABEL:lst:transaction_module
passes at $r^{\prime}$ (by Lemma 12) and the invariant hypothesis.

Since the invariant is always preserved, the lemma holds. ∎

We say that a transaction $\mathit{tx}$ _depends on_ a transaction
$\mathit{tx}^{\prime}$ if and only if:

  * •

$\mathit{tx}.\mathit{issuer}=\mathit{tx}^{\prime}.\mathit{issuer}$ and
$\mathit{tx}.\mathit{sn}=\mathit{tx}^{\prime}.\mathit{sn}+1$; or

  * •

$\mathit{tx}$ is a deposit transaction, $\mathit{tx}^{\prime}$ is a withdrawal
transaction and $\mathit{tx}.\mathit{withdrawal}=\mathit{tx}^{\prime}$.

Now, given an admissible log, we specify the rank of every transaction that
belongs to the log; we denote by $\mathit{rank}_{L}(\mathit{tx})$ the rank of
a transaction $\mathit{tx}$ in an admissible log $L$. We define the rank in
the following manner:

  * •

If $\mathit{tx}$ does not depend on any transaction that belongs to $L$, then
$\mathit{rank}_{L}(\mathit{tx})=0$.

  * •

Otherwise,
$\mathit{rank}_{L}(\mathit{tx})=\mathit{max}(\mathit{rank}_{L}(\mathit{tx}_{1}),\mathit{rank}_{L}(\mathit{tx}_{2}))+1$,
where $\mathit{tx}$ depends on $\mathit{tx}_{1}\in L$ and $\mathit{tx}$
depends on $\mathit{tx}_{2}\in L$.

Recall that $v_{\mathit{final}}$ is the greatest forever-alive view (see
Definition 2). Moreover, we say that a transaction $\mathit{tx}$ is quasi-
committed at a correct server $r$ if and only if
$\mathit{quasi\\_committed}[\mathit{tx}]=\top$ at server $r$. The next lemma
shows that any transaction that belongs to the $\mathit{log}$ variable (recall
that $\mathit{log}=\mathit{state}.\mathtt{extract\\_log()}$) of a correct
member of $v_{\mathit{final}}$ eventually belongs to the $\mathit{log}$
variable of all other correct members of $v_{\mathit{final}}$.

###### Lemma 0.

Consider a correct server $r\in v_{\mathit{final}}.\mathtt{members}()$. Let
$\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot$ at server $r$. Eventually,
$\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot$ at every correct server
$r^{\prime}\in v_{\mathit{final}}.\mathtt{members()}$.

###### Proof.

Recall that, by the finality property (see
LABEL:lst:reconfiguration_properties_new), the following holds:

  1. (1)

all correct members of $v_{\mathit{final}}$ update their current view to
$v_{\mathit{final}}$ (i.e., set their $\mathit{current\\_view}.\mathit{view}$
variable to $v_{\mathit{final}}$),

  2. (2)

no correct member of $v_{\mathit{final}}$ updates its current view to any
other view afterwards,

  3. (3)

all correct members of $v_{\mathit{final}}$ install $v_{\mathit{final}}$,

  4. (4)

no correct member of $v_{\mathit{final}}$ leaves, and

  5. (5)

no correct member of $v_{\mathit{final}}$ stops processing in
$v_{\mathit{final}}$.

Let
$\mathit{log}_{r}=\\{\mathit{tx}\,|\,\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot\text{
at server }r\\}$. By Lemma 12, $\mathit{log}_{r}$ is admissible (see
LABEL:lst:state_representation). In the rest of the proof, we consider a
particular server $r^{*}\neq r$, where $r^{*}\in
v_{\mathit{final}}.\mathtt{members()}$. We prove the lemma by induction.

Base step: We consider all the transactions that belong to $\mathit{log}_{r}$
with rank $0$. Let us denote that set of transactions by $\mathit{TX}_{0}$.

If $r$ broadcasts the $\mathtt{COMMIT}$ message for
$\mathit{tx}\in\mathit{TX}_{0}$ to all members of $v_{\mathit{final}}$ at line
80 or line 176 of LABEL:lst:transaction_module, $r^{*}$ eventually receives
the message and sets $\mathit{state}.\mathit{log}[\mathit{tx}]$ to the
received $\mathtt{COMMIT}$ message (by the finality property and the fact that
$\mathit{tx}$ is certified, by Lemma 12).

Otherwise, $\mathit{tx}$ is quasi-committed at server $r$ (since
$\mathit{quasi\\_committed}[\mathit{tx}]=\top$; line 174 of
LABEL:lst:transaction_module) at the moment of installing $v_{\mathit{final}}$
(line 171 of LABEL:lst:transaction_module). Let $v_{\mathit{tx}}$ be the
smallest view in which $\mathit{tx}$ is quasi-committed; note that such view
is defined since all views in which $\mathit{tx}$ is quasi-committed are valid
(by Lemma 15) and all valid views are comparable (by the view comparability
property; see LABEL:lst:reconfiguration_properties_new). By
LABEL:lst:transaction_module, $v_{\mathit{tx}}\subset v_{\mathit{final}}$.
Hence, the base case is satisfied by Lemma 16 and the finality property.

Inductive step: We consider all transactions that belong to $\mathit{log}_{r}$
with rank $\mathit{rank}$. Let $\mathit{TX}_{\mathit{rank}}$ denote that set
of transactions. We assume, for all transactions $\mathit{tx}^{\prime}$ that
belong to $\mathit{log}_{r}$ with the smaller rank, that
$\mathit{state}.\mathit{log}[\mathit{tx}^{\prime}]\neq\bot$ at every correct
member of $v_{\mathit{final}}$. We prove that the invariant is preserved for
all transactions that belong to $\mathit{TX}_{\mathit{rank}}$.

If $r$ broadcasts the $\mathtt{COMMIT}$ message for
$\mathit{tx}\in\mathit{TX}_{\mathit{rank}}$ to all members of
$v_{\mathit{final}}$ at line 80 or line 176 of LABEL:lst:transaction_module,
$r^{*}$ eventually receives the message and sets
$\mathit{state}.\mathit{log}[\mathit{tx}]$ to the received $\mathtt{COMMIT}$
message (by the finality property, induction hypothesis and the fact that
$\mathit{tx}$ is certified, by Lemma 12).

Otherwise, $\mathit{tx}$ is quasi-committed at server $r$ (since
$\mathit{quasi\\_committed}[\mathit{tx}]=\top$; line 174 of
LABEL:lst:transaction_module) at the moment of installing $v_{\mathit{final}}$
(line 171 of LABEL:lst:transaction_module). Let $v_{\mathit{tx}}$ be the
smallest view in which $\mathit{tx}$ is quasi-committed; note that such view
is defined since all views in which $\mathit{tx}$ is quasi-committed are valid
(by Lemma 15) and all valid views are comparable (by the view comparability
property; see LABEL:lst:reconfiguration_properties_new). By
LABEL:lst:transaction_module, $v_{\mathit{tx}}\subset v_{\mathit{final}}$.
Hence, the inductive case is satisfied by Lemma 16 and the finality property.

∎

The next lemma proves that a correct member of $v_{\mathit{final}}$ eventually
receives the $\mathtt{COMMIT-CONFIRM}$ messages from all correct members of
$v_{\mathit{final}}$.

###### Lemma 0.

Let a correct server $r\in v_{\mathit{final}}.\mathtt{members}()$ broadcast
the $\mathtt{COMMIT}$ message for a transaction $\mathit{tx}$ to all members
of $v_{\mathit{final}}$. Eventually, $\mathit{r}$ receives $\mathtt{COMMIT-
CONFIRM}$ message for $\mathit{tx}$ associated with $v_{\mathit{final}}$ from
all correct members of $v_{\mathit{final}}$.

###### Proof.

We consider all possible places at which $r$ could broadcast the
$\mathtt{COMMIT}$ message:

  * •

line 80 of LABEL:lst:transaction_module: Therefore,
$\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot$ at server $r$ (by line 75
of LABEL:lst:transaction_module).

  * •

line 176 of LABEL:lst:transaction_module: Again,
$\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot$ at server $r$ (by the check
at line 174 of LABEL:lst:transaction_module).

Since in both possible cases,
$\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot$ at server $r$,
$\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot$ at every correct server
$r^{\prime}\in v_{\mathit{final}}.\mathtt{members()}$ (by Lemma 17).

Once this happens at a correct server $r^{\prime}$ and $r^{\prime}$ receives
the $\mathtt{COMMIT}$ message sent by $r$ (which happens because of the
finality property), $r^{\prime}$ sends the $\mathtt{COMMIT-CONFIRM}$ message
for $\mathit{tx}$ associated with $v_{\mathit{final}}$ at line 82 of
LABEL:lst:transaction_module (because of the
$\mathtt{allowed\\_to\\_commit\\_confirm}$ function; line 59 of
LABEL:lst:transaction_module). Furthermore, the finality property ensures that
$r$ eventually receives this $\mathtt{COMMIT-CONFIRM}$ message sent by
$r^{\prime}$, which concludes the proof. ∎

Next, we prove that a transaction $\mathit{tx}$ is quasi-committed at a
correct server $r\in v_{\mathit{final}}$, where
$\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot$ at $r$.

###### Lemma 0.

Consider a correct server $r\in v_{\mathit{final}}.\mathtt{members}()$. Let
$\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot$ at server $r$. Then, $r$
eventually quasi-commits $\mathit{tx}$.

###### Proof.

We prove the lemma by contradiction. Hence, suppose that $r$ does not quasi-
commit $\mathit{tx}$. By Lemma 17,
$\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot$ at every correct member of
$v_{\mathit{final}}$.

Let
$\mathit{log}_{r}=\\{\mathit{tx}\,|\,\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot\text{
at server }r\\}$. Because of Lemma 12, $\mathit{log}_{r}$ is admissible.
Recall that $\mathit{tx}\in\mathit{log}_{r}$.

Let $\mathcal{D}(\mathit{tx})$ be the reflexive transitive closure of the
“depends-on” relation for $\mathit{tx}$ given $\mathit{log}_{r}$. Let
$\mathit{quasi\\_committed}_{r}$ denote the set of transactions quasi-
committed by $r$; note that $\mathit{tx}\notin\mathit{quasi\\_committed}_{r}$
(by the assumption). Moreover, let $\mathit{quasi\\_committed}_{r}^{*}$ denote
the set of transactions quasi-committed at $r$ for which $r$ has sent the
$\mathtt{COMMIT}$ message associated with $v_{\mathit{final}}$; observe that
$\mathit{quasi\\_committed}_{r}^{*}\subseteq\mathit{quasi\\_committed}_{r}$.
By Lemma 18, $r$ eventually receives $\mathtt{COMMIT-CONFIRM}$ messages for
$\mathit{tx}^{\prime}$ associated with $v_{\mathit{final}}$ from all correct
members of $v_{\mathit{final}}$, for all transactions
$\mathit{tx}^{\prime}\in\mathit{quasi\\_committed}_{r}^{*}$.

Let $\mathit{tx}^{*}\in\mathcal{D}(\mathit{tx})$ such that (1)
$\mathit{tx}^{*}\notin\mathit{quasi\\_committed}_{r}$, and (2) all
dependencies of $\mathit{tx}^{*}$ are quasi-committed at $r$; note that
$\mathit{tx}^{*}$ indeed exists since
$\mathit{tx}\in\mathcal{D}(\mathit{tx})$,
$\mathit{tx}\notin\mathit{quasi\\_committed}_{r}$ and $\mathit{log}_{r}$ is a
DAG (since it is admissible).

Since $\mathit{tx}^{*}\notin\mathit{quasi\\_committed}_{r}$, $r$ broadcasts
the $\mathtt{COMMIT}$ message for $\mathit{tx}^{*}$ to all members of
$v_{\mathit{final}}$ (by the finality property; lines 80 or 176 of
LABEL:lst:transaction_module). Eventually, $r$ receives $\mathtt{COMMIT-
CONFIRM}$ messages for $\mathit{tx}^{*}$ associated with $v_{\mathit{final}}$
from all correct members of $v_{\mathit{final}}$ (by Lemma 18).

Recall that all dependencies of $\mathit{tx}^{*}$ are quasi-committed by $r$.
Therefore, once (1) all dependencies of $\mathit{tx}^{*}$ are quasi-committed
by $r$, (2) $\mathtt{COMMIT-CONFIRM}$ messages for $\mathit{tx}^{*}$ are
received from all correct members of $v_{\mathit{final}}$, and (3)
$\mathtt{COMMIT-CONFIRM}$ messages for $\mathit{tx}^{\prime}$ are received
from all correct members of $v_{\mathit{final}}$, for every
$\mathit{tx}^{\prime}\in\mathit{quasi\\_committed}_{r}^{*}$ (note that
$\mathit{quasi\\_committed\\_current\\_view}\subseteq\mathit{quasi\\_committed}_{r}^{*}$),
$r$ quasi-commits $\mathit{tx}^{*}$ (since the
$\mathtt{allowed\\_to\\_quasi\\_commit}$ function returns $\top$). Thus, we
reach contradiction and $\mathit{tx}$ is quasi-committed at $r$. ∎

The next lemma proves that a correct server $r\in
v_{\mathit{final}}.\mathtt{members()}$ eventually obtains a commitment proof
for $\mathit{tx}$ if $\mathit{tx}$ is quasi-committed at $r$.

###### Lemma 0.

Consider a correct server $r\in v_{\mathit{final}}.\mathtt{members()}$. Let
$\mathit{tx}$ be quasi-committed at $r$. Then, $r$ eventually obtains a
commitment proof $\sigma_{c}$ such that
$\mathtt{verify\\_commit}(\mathit{tx},\sigma_{c})=\top$.

###### Proof.

Since $\mathit{tx}$ is quasi-committed at $r$,
$\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot$ at $r$ (because of the
$\mathtt{allowed\\_to\\_quasi\\_commit}$ function and Lemma 9; line 91 of
LABEL:lst:transaction_module). Let
$\mathit{log}_{r}=\\{\mathit{tx}\,|\,\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot\text{
at server }r\\}$. Because of Lemma 12, $\mathit{log}_{r}$ is admissible.
Recall that $\mathit{tx}\in\mathit{log}_{r}$.

By Lemma 17, $\mathit{state}.\mathit{log}[\mathit{tx}^{\prime}]\neq\bot$ at
every correct member of $v_{\mathit{final}}$, for every
$\mathit{tx}^{\prime}\in\mathit{log}_{r}$. Finally, by Lemma 19,
$\mathit{tx}^{\prime}$ is quasi-committed at every correct member of
$v_{\mathit{final}}$, for every $\mathit{tx}^{\prime}\in\mathit{log}_{r}$.

Let $\mathcal{D}(\mathit{tx})$ be the reflexive transitive closure of the
“depends-on” relation for $\mathit{tx}$ given $\mathit{log}_{r}$; note that
$\mathcal{D}(\mathit{tx})\subseteq\mathit{log}_{r}$. We prove the lemma by
induction.

Base step: We consider all the transactions that belong to
$\mathcal{D}(\mathit{tx})$ with rank $0$. Let us denote that set of
transactions by $\mathit{TX}_{0}$.

Eventually, every correct member of $v_{\mathit{final}}$ broadcasts the
$\mathtt{COMMITTED}$ message for $\mathit{tx}\in\mathit{TX}_{0}$ to members of
$v_{\mathit{final}}$ (because of the
$\mathtt{allowed\\_to\\_broadcast\\_committed}$ function and the finality
property). The finality property ensures that every correct member of
$v_{\mathit{final}}$ receives the set of
$v_{\mathit{final}}.\mathtt{plurality()}$ messages (at line 144 of
LABEL:lst:transaction_module), which constitutes a commitment proof
$\sigma_{c}$ for $\mathit{tx}$ (see LABEL:lst:commitment_proof_verification).
Moreover, $\mathit{confirmed}[\mathit{tx}]=\top$ at every correct member of
$v_{\mathit{final}}$. Therefore, the base step holds.

Inductive step: We consider all transactions that belong to
$\mathcal{D}(\mathit{tx})$ with rank $\mathit{rank}$. Let
$\mathit{TX}_{\mathit{rank}}$ denote that set of transactions. We assume, for
all transactions $\mathit{tx}^{\prime}$ that belong to
$\mathcal{D}(\mathit{tx})$ with the smaller rank, that
$\mathit{confirmed}[\mathit{tx}]=\top$ at every correct member of
$v_{\mathit{final}}$. We prove that the invariant is preserved for all
transactions that belong to $\mathit{TX}_{\mathit{rank}}$.

Eventually, every correct member of $v_{\mathit{final}}$ broadcasts the
$\mathtt{COMMITTED}$ message for $\mathit{tx}\in\mathit{TX}_{\mathit{rank}}$
to members of $v_{\mathit{final}}$ (because of the
$\mathtt{allowed\\_to\\_broadcast\\_committed}$ function, the inductive
hypothesis and the finality property). The finality property ensures that
every correct member of $v_{\mathit{final}}$ receives the set of
$v_{\mathit{final}}.\mathtt{plurality()}$ messages (at line 144 of
LABEL:lst:transaction_module), which constitutes a commitment proof
$\sigma_{c}$ for $\mathit{tx}$ (see LABEL:lst:commitment_proof_verification).
Moreover, $\mathit{confirmed}[\mathit{tx}]=\top$ at every correct member of
$v_{\mathit{final}}$. Therefore, the inductive step holds, as well. Thus, the
proof is concluded. ∎

Finally, we are ready to prove the commitment validity property.

###### Theorem 21 (Commitment Validity).

Commitment validity is satisfied.

###### Proof.

Consider a transaction $\mathit{tx}$ issued by a forever-correct client which
is not committed. All transactions on which $\mathit{tx}$ depends are
committed (see § 3.1, paragraph “Rules”). Let $\mathit{tx}$ be dependent on
$\mathit{tx}^{\prime}$; as already mentioned, $\mathit{tx}^{\prime}$ is
committed. Therefore, $\mathit{tx}^{\prime}$ is quasi-committed (by the
$\mathtt{allowed\\_to\\_broadcast\\_committed}$ function; line 127 of
LABEL:lst:transaction_module). Let $v_{\mathit{tx}^{\prime}}$ be the smallest
view in which $\mathit{tx}^{\prime}$ is quasi-committed. We distinguish two
cases:

  * •

Let $v_{\mathit{tx}^{\prime}}\subset v_{\mathit{final}}$. Therefore,
$\mathit{state}.\mathit{log}[\mathit{tx}^{\prime}]\neq\bot$ at every correct
member of $v_{\mathit{final}}$ (by Lemma 16).

  * •

Let $v_{\mathit{tx}^{\prime}}=v_{\mathit{final}}$. Hence, there exists a
correct member of $v_{\mathit{final}}$ that sends the $\mathtt{COMMIT-
CONFIRM}$ message for $\mathit{tx}^{\prime}$ associated with
$v_{\mathit{final}}$. Thus,
$\mathit{state}.\mathit{log}[\mathit{tx}^{\prime}]\neq\bot$ at that server (by
line 75 of LABEL:lst:transaction_module). By Lemma 17,
$\mathit{state}.\mathit{log}[\mathit{tx}^{\prime}]\neq\bot$ at every correct
member of $v_{\mathit{final}}$.

In both cases, $\mathit{state}.\mathit{log}[\mathit{tx}^{\prime}]\neq\bot$ at
every correct member of $v_{\mathit{final}}$. By Lemma 19,
$\mathit{tx}^{\prime}$ is quasi-committed at every correct member of
$v_{\mathit{final}}$. Finally, by Lemma 20, every correct member of
$v_{\mathit{final}}$ obtains a commitment proof for $\mathit{tx}^{\prime}$
(and sets $\mathit{confirmed}[\mathit{tx}^{\prime}]=\top$).

Since $\mathit{tx}.\mathit{issuer}$ is forever-correct, the client eventually
learns about $v_{\mathit{final}}$ (i.e.,
$v_{\mathit{final}}\in\mathit{history}$ at the client). Once that happens, the
client sends the $\mathtt{PREPARE}$ message for $\mathit{tx}$ to all members
of $v_{\mathit{final}}$ (at lines 40 or 53 of LABEL:lst:client). Since
$\mathit{state}.\mathit{log}[\mathit{tx}^{\prime}]\neq\bot$ at every correct
member of $v_{\mathit{final}}$, for every dependency $\mathit{tx}^{\prime}$ of
$\mathit{tx}$, all correct members of $v_{\mathit{final}}$ send the
$\mathtt{ACK}$ message to the client (at line 52 of
LABEL:lst:transaction_module). Hence, the client eventually obtains a
transaction certificate for $\mathit{tx}$.

Similarly, the client sends the $\mathtt{COMMIT}$ message to all members of
$v_{\mathit{final}}$ (at lines 42 or 76 of LABEL:lst:client). Therefore, every
correct member of $v_{\mathit{final}}$ eventually receives the
$\mathtt{COMMIT}$ message (since
$\mathit{state}.\mathit{log}[\mathit{tx}^{\prime}]\neq\bot$ at every correct
member of $v_{\mathit{final}}$, for every dependency $\mathit{tx}^{\prime}$ of
$\mathit{tx}$). Finally, this means that
$\mathit{log}.\mathit{state}[\mathit{tx}]\neq\bot$ at every correct member of
$v_{\mathit{final}}$ (by line 75 of LABEL:lst:transaction_module). By Lemma
19, $\mathit{tx}$ is quasi-committed at every correct member of
$v_{\mathit{final}}$. Furthermore, every correct member of
$v_{\mathit{final}}$ eventually obtains a commitment proof for $\mathit{tx}$
(by Lemma 20), which implies that $\mathit{tx}$ is committed. Since we reach
contradiction, our starting assumption was not correct, which means that
$\mathit{tx}$ is committed. The theorem holds. ∎

Next, we prove the commitment learning property.

###### Theorem 22 (Commitment Learning).

Commitment learning is satisfied.

###### Proof.

Let a transaction $\mathit{tx}$ be committed. Therefore, $\mathit{tx}$ is
quasi-committed (by the $\mathtt{allowed\\_to\\_broadcast\\_committed}$
function; line 127 of LABEL:lst:transaction_module). Let $v_{\mathit{tx}}$ be
the smallest view in which $\mathit{tx}^{\prime}$ is quasi-committed. We
distinguish two cases:

  * •

Let $v_{\mathit{tx}}\subset v_{\mathit{final}}$. Therefore,
$\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot$ at every correct member of
$v_{\mathit{final}}$ (by Lemma 16).

  * •

Let $v_{\mathit{tx}}=v_{\mathit{final}}$. Hence, there exists a correct member
of $v_{\mathit{final}}$ that sends the $\mathtt{COMMIT-CONFIRM}$ message for
$\mathit{tx}$ associated with $v_{\mathit{final}}$. Thus,
$\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot$ at that server (by line 75
of LABEL:lst:transaction_module). By Lemma 17,
$\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot$ at every correct member of
$v_{\mathit{final}}$.

In both cases, $\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot$ at every
correct member of $v_{\mathit{final}}$. By Lemma 19, $\mathit{tx}$ is quasi-
committed at every correct member of $v_{\mathit{final}}$. Finally, by Lemma
20, every correct member of $v_{\mathit{final}}$ obtains a commitment proof
for $\mathit{tx}$ (and sets $\mathit{confirmed}[\mathit{tx}^{\prime}]=\top$).
Once that happens, a correct member of $v_{\mathit{final}}$ sends the
commitment proof to $\mathit{tx}.\mathit{issuer}$ (at line 146 of
LABEL:lst:transaction_module) and, if $\mathit{tx}$ is a withdrawal
transaction, to $\mathit{tx}.\mathit{receiver}$ (at line 148 of
LABEL:lst:transaction_module). Since no correct member of $v_{\mathit{final}}$
leaves (by the finality property), the appropriate clients eventually obtain
commitment proofs (at line 78 of LABEL:lst:client) and the theorem holds. ∎

The last property of Carbon we need to prove is the commitment signing
property (see § 3.3, paragraph “Properties of Carbon”). In order to show that
this property holds, we first prove that an issued transaction cannot be
quasi-committed in “stale” views.

###### Lemma 0.

Let a transaction $\mathit{tx}$ be issued at time $t$. Let
$\mathcal{V}(t)=\\{v\,|\,\mathit{current\\_view}.\mathit{view}=v\neq\bot\text{
at a correct server at time }t\\}$. If $\mathcal{V}(t)\neq\emptyset$ and
$v_{\mathit{max}}$ is the greatest view of $\mathcal{V}(t)$, then
$\mathit{tx}$ is not quasi-committed in a view $v$, for any view $v\subset
v_{\mathit{max}}$.

###### Proof.

Note that $\mathcal{V}(t)$ might contain values of the
$\mathit{current\\_view}.\mathit{view}$ variable of correct servers that
halted by time $t$ (note that $\mathit{current\\_view}.\mathit{view}$ is not
modified upon leaving; see LABEL:lst:reconfiguration_view_transition). We
prove the lemma by contradiction. Therefore, let $\mathit{tx}$ be quasi-
committed in a view $v\subset v_{\mathit{max}}$.

First, note that no correct server obtains $\mathit{tx}$ before time $t$ (due
to the definition of “issued at time $t$”; see § 3.3, paragraph “Properties of
Carbon”). Therefore, no correct server sends the $\mathtt{COMMIT-CONFIRM}$
message for $\mathit{tx}$ before $t$. Moreover, since $\mathit{tx}$ is quasi-
committed in $v$ and Lemma 15 holds, $v$ is a view installable at time
$\infty$.

Let $r_{\mathit{first}}$ be the first correct server to set its
$\mathit{current\\_view}.\mathit{view}$ variable to a view greater than $v$;
let that view be $v_{\mathit{first}}\supset v$. Observe that
$r_{\mathit{first}}$ sets its $\mathit{current\\_view}.\mathit{view}$ variable
to $v_{\mathit{first}}$ by time $t$. Since $v\subset v_{\mathit{first}}$,
$v_{\mathit{first}}\neq\mathit{genesis}$ (by Lemma 45). Therefore, before
updating its $\mathit{current\\_view}.\mathit{view}$ variable to
$v_{\mathit{first}}$, $r_{\mathit{first}}$ has received $\mathtt{STATE-
UPDATE}$ messages from the quorum of members of $v$ (the rule at line 40 of
LABEL:lst:reconfiguration_state_transfer becomes active and
$\mathit{reconfiguration}.\mathit{source}=v$ at that time at
$r_{\mathit{first}}$, by Lemma 56). Each such $\mathtt{STATE-UPDATE}$ message
is sent before time $t$ at line 14 of
LABEL:lst:reconfiguration_state_transfer. Therefore, before sending the
$\mathtt{STATE-UPDATE}$ message (i.e., before time $t$), the
$\mathit{stop\\_processing\\_until}$ variable is equal to (at least) $v$ at
each correct server that sends the $\mathtt{STATE-UPDATE}$ message received by
$r_{\mathit{first}}$.

Furthermore, since $\mathit{tx}$ is quasi-committed in $v$, at least
$v.\mathtt{plurality()}$ of correct members of $v$ have sent the
$\mathtt{COMMIT-CONFIRM}$ message for $\mathit{tx}$ associated with $v$ (at
line 82 of LABEL:lst:transaction_module); each such message is sent at some
time greater than or equal to $t$. Therefore, there exists a correct member of
$v$ that (1) sets its $\mathit{stop\\_processing\\_until}$ variable to (at
least) $v$ before time $t$, and (2) sends the $\mathtt{COMMIT-CONFIRM}$
message for $\mathit{tx}$ associated with $v$ at time $t$ (or later). Such
behavior is not a correct one (see LABEL:lst:reconfiguration_view_transition).
Hence, we reach contradiction and $\mathit{tx}$ is not quasi-committed in $v$.
The lemma holds. ∎

The direct consequence of Lemma 23 is that no correct server sends the
$\mathtt{COMMITTED}$ message associated with a view smaller than
$v_{\mathit{max}}$. Let us prove this claim.

###### Lemma 0.

Let a transaction $\mathit{tx}$ be issued at time $t$. Let
$\mathcal{V}(t)=\\{v\,|\,\mathit{current\\_view}.\mathit{view}=v\neq\bot\text{
at a correct server at time }t\\}$. If $\mathcal{V}(t)\neq\emptyset$ and
$v_{\mathit{max}}$ is the greatest view of $\mathcal{V}(t)$, then no correct
server sends the $\mathtt{COMMITTED}$ message for $\mathit{tx}$ associated
with a view $v$, for any view $v\subset v_{\mathit{max}}$.

###### Proof.

By contradiction, let a correct server $r$ send the $\mathtt{COMMITTED}$
message for $\mathit{tx}$ associated with a view $v\subset v_{\mathit{max}}$.
That means that $\mathit{tx}$ is quasi-committed at server $r$ (by the
$\mathtt{allowed\\_to\\_broadcast\\_committed}$ function; line 127 of
LABEL:lst:transaction_module). Since $\mathit{current\\_view}.\mathit{view}=v$
at the moment of sending the $\mathtt{COMMITTED}$ message (by line 142 of
LABEL:lst:transaction_module), $\mathit{tx}$ is quasi-committed in a view
smaller than or equal to $v$. Since $v\subset v_{\mathit{max}}$, this is not
possible due to Lemma 23. Therefore, $r$ does not send the
$\mathtt{COMMITTED}$ message for $\mathit{tx}$ associated with $v\subset
v_{\mathit{max}}$ and the lemma holds. ∎

The next theorem shows that the commitment signing property is satisfied.

###### Theorem 25 (Commitment Signing).

Commitment signing is satisfied.

###### Proof.

Let a transaction $\mathit{tx}$ be issued at time $t$ and let a commitment
proof $\sigma_{c}$ be obtained at time $t^{\prime}\geq t$, where
$\mathtt{verify\\_commit}(\mathit{tx},\sigma_{c})=\top$. Since $\mathit{tx}$
is issued at time $t$, no correct server sends the $\mathtt{COMMITTED}$
message for $\mathit{tx}$ before time $t$ (follows from the definition of
“issued at time $t$”; see § 3.3, paragraph “Properties of Carbon”).

Consider a correct server $r$. We distinguish two cases:

  1. (1)

Let $r$ leave before time $t$. Since $r$ does not send any
$\mathtt{COMMITTED}$ message for $\mathit{tx}$ before time $t$ and $r$ halts
immediately after leaving (which happens before time $t$),
$r\notin\sigma_{c}.\mathtt{signers}$.

  2. (2)

Let $r$ join after time $t^{\prime}$. All the $\mathtt{COMMITTED}$ messages
that belong to $\sigma_{c}$ are sent by time $t^{\prime}$. Since $r$ does not
send any $\mathtt{COMMITTED}$ messages before joining (see
LABEL:lst:transaction_module; $r$ joins after time $t^{\prime}$),
$r\notin\sigma_{c}.\mathtt{signers}$.

Finally, consider a faulty server $r$. Again, we distinguish two cases:

  1. (1)

Let $r$ leave before time $t$. Therefore, there exists a correct server
$r^{*}$ that triggers the special $r\text{ }\mathtt{left}$ event (at line 64
of LABEL:lst:reconfiguration_view_transition) before time $t$.

Let
$\mathcal{V}(t)=\\{v\,|\,\mathit{current\\_view}.\mathit{view}=v\neq\bot\text{
at a correct server at time }t\\}$. First, $\mathcal{V}(t)\neq\emptyset$
because of $r^{*}$ and $r\notin v_{\mathit{max}}.\mathtt{members()}$, where
$v_{\mathit{max}}$ is the greatest view of $\mathcal{V}(t)$. Moreover, for any
view $v$ such that $r\in v.\mathtt{members()}$, $v\subset v_{\mathit{max}}$.
By Lemma 24, no correct server sends the $\mathtt{COMMITTED}$ message for
$\mathit{tx}$ associated with any view smaller than $v_{\mathit{max}}$. Hence,
$r\notin\sigma_{c}.\mathtt{signers}$.

  2. (2)

Let $r$ join after time $t^{\prime}$. All the $\mathtt{COMMITTED}$ messages
that belong to $\sigma_{c}$ are sent by time $t^{\prime}$. Let $r^{*}$ be a
correct server that sends the $\mathtt{COMMITTED}$ message $m\in\sigma_{c}$;
such correct server indeed exists due to
LABEL:lst:commitment_proof_verification. Let that message be associated with
view $v$.

Assume that $r\in v.\mathtt{members()}$. If $v=\mathit{genesis}$, then $r$
would have joined by time $t^{\prime}$ because $r^{*}$ would have triggered
the special $r\text{ }\mathtt{joined}$ event at line 53 of
LABEL:lst:reconfiguration_initialization. Hence, $v\neq\mathit{genesis}$.
Therefore, $r^{*}$ have entered the pseudocode at line 3 of
LABEL:lst:reconfiguration_view_transition with the “source” view being
$v_{s}$. If $r\notin v_{s}.\mathtt{members()}$, $r$ would have joined by time
$t^{\prime}$ (by line 60 of LABEL:lst:reconfiguration_view_transition executed
by $r^{*}$). Hence, $r\in v_{s}.\mathtt{members()}$ and we reach the same
point as we reached with view $v$. Eventually, the recursion stops since
$\mathit{genesis}$ is the smallest valid view (by Lemma 45). Therefore,
$r\in\mathit{genesis}.\mathtt{members()}$, which means that $r$ joins before
time $t^{\prime}$. Thus, we reach contradiction and $r\notin
v.\mathtt{members()}$, which implies that
$r\notin\sigma_{c}.\mathtt{signers}$.

The theorem holds and commitment signing is satisfied. ∎

Next, we prove the query validity property.

###### Theorem 26 (Query Validity).

Query validity is satisfied.

###### Proof.

By contradiction, suppose that the query validity property is not satisfied.
Since the client is forever-correct, the client eventually learns about
$v_{\mathit{final}}$ (i.e., $v_{\mathit{final}}\in\mathit{history}$ at the
client) and it broadcasts the $\mathtt{QUERY}$ message to members of
$v_{\mathit{final}}$ (line 38 or 63 of LABEL:lst:client). By the finality
property (see LABEL:lst:reconfiguration_properties_new), every correct member
of $v_{\mathit{final}}$ eventually installs $v_{\mathit{final}}$, does not
update its current view afterwards and does not leave. Therefore, every
correct member of $v_{\mathit{final}}$ eventually receives the
$\mathtt{QUERY}$ message (at line 150 of LABEL:lst:transaction_module) and
responds with the $\mathtt{QUERY-RESPONSE}$ message (at line 153 of
LABEL:lst:transaction_module). Eventually, the client receives the
$\mathtt{QUERY-RESPONSE}$ messages from all correct members of
$v_{\mathit{final}}$ (i.e., the rule at line 91 of LABEL:lst:client becomes
active) and the client learns the total amount of money in Carbon. Thus, the
theorem holds. ∎

The next theorem proves the query safety property.

###### Theorem 27 (Query Safety).

Query safety is satisfied.

###### Proof.

Since a correct client learns the total amount of money, the client has
received the $\mathtt{QUERY-RESPONSE}$ messages from $v.\mathtt{quorum()}$ of
members of a valid view $v$ (by the rule at line 91 of LABEL:lst:client). Let
the client learn that the total amount of money is $X$. Therefore, there
exists a correct server that has sent the $\mathtt{QUERY-RESPONSE}$ message
for a value $X^{\prime}\geq X$. Let that server be $r\in
v.\mathtt{members()}$.

Since $r$ “calculates” the total amount of money by “looking into” all the
transactions it has quasi-committed (by lines 152 and 153 of
LABEL:lst:transaction_module), there exists a set $\mathit{mints}$ of quasi-
committed minting transactions such that
$X^{\prime}=\sum\limits_{\mathit{tx}\in\mathit{mints}}\mathit{tx}.\mathit{amount}$.
For each transaction $\mathit{tx}\in\mathit{mints}$, let $v_{\mathit{tx}}$ be
the smallest view in which $\mathit{tx}$ is quasi-committed. We distinguish
two cases:

  * •

Let $v_{\mathit{tx}}\subset v_{\mathit{final}}$. Therefore,
$\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot$ at every correct member of
$v_{\mathit{final}}$ (by Lemma 16).

  * •

Let $v_{\mathit{tx}}=v_{\mathit{final}}$. Hence, there exists a correct member
of $v_{\mathit{final}}$ that sends the $\mathtt{COMMIT-CONFIRM}$ message for
$\mathit{tx}$ associated with $v_{\mathit{final}}$. Thus,
$\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot$ at that server (by line 75
of LABEL:lst:transaction_module). By Lemma 17,
$\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot$ at every correct member of
$v_{\mathit{final}}$.

In both cases, $\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot$ at every
correct member of $v_{\mathit{final}}$, for every transaction
$\mathit{tx}\in\mathit{mints}$. By Lemma 19, $\mathit{tx}$ is quasi-committed
at every correct member of $v_{\mathit{final}}$, for every
$\mathit{tx}\in\mathit{mints}$. Finally, by Lemma 20, every correct member of
$v_{\mathit{final}}$ obtains a commitment proof for $\mathit{tx}$, which means
that $\mathit{tx}$ is committed, for every $\mathit{tx}\in\mathit{mints}$.
Hence, the theorem holds. ∎

Finally, we prove the query liveness property.

###### Theorem 28 (Query Liveness).

Query liveness is satisfied.

###### Proof.

Let $X=\sum\limits_{\mathit{tx}\in\mathit{mints}}\mathit{tx}.\mathit{amount}$.
Since $\mathit{tx}$ is committed, for every $\mathit{tx}\in\mathit{mints}$,
$\mathit{tx}$ is quasi-committed (by the
$\mathtt{allowed\\_to\\_broadcast\\_committed}$ function; line 127 of
LABEL:lst:transaction_module). For each transaction
$\mathit{tx}\in\mathit{mints}$, let $v_{\mathit{tx}}$ be the smallest view in
which $\mathit{tx}$ is quasi-committed. We distinguish two cases:

  * •

Let $v_{\mathit{tx}}\subset v_{\mathit{final}}$. Therefore,
$\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot$ at every correct member of
$v_{\mathit{final}}$ (by Lemma 16).

  * •

Let $v_{\mathit{tx}}=v_{\mathit{final}}$. Hence, there exists a correct member
of $v_{\mathit{final}}$ that sends the $\mathtt{COMMIT-CONFIRM}$ message for
$\mathit{tx}$ associated with $v_{\mathit{final}}$. Thus,
$\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot$ at that server (by line 75
of LABEL:lst:transaction_module). By Lemma 17,
$\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot$ at every correct member of
$v_{\mathit{final}}$.

In both cases, $\mathit{state}.\mathit{log}[\mathit{tx}]\neq\bot$ at every
correct member of $v_{\mathit{final}}$, for every transaction
$\mathit{tx}\in\mathit{mints}$. By Lemma 19, $\mathit{tx}$ is quasi-committed
at every correct member of $v_{\mathit{final}}$, for every
$\mathit{tx}\in\mathit{mints}$. Therefore, eventually all correct members of
$v_{\mathit{final}}$ would send the $\mathtt{QUERY-RESPONSE}$ message (at line
153 of LABEL:lst:transaction_module) for a value $X^{\prime}\geq X$.

Let the client request to learn the total amount of money after this happens
and after all correct members of $v_{\mathit{final}}$ have set their
$\mathit{current\\_view}.\mathit{view}$ variable to $v_{\mathit{final}}$
(which does happen due to the finality property). Therefore, the client
eventually receives (at most) $v_{\mathit{final}}.\mathtt{plurality}()-1$
values (through the $\mathtt{QUERY-RESPONSE}$ messages) smaller than $X$.
Hence, the $\mathtt{median}$ function (at line 93 of LABEL:lst:client) returns
a value greater than or equal to $X$. Thus, the query liveness property is
satisfied. ∎

Hence, all properties of Carbon specified in § 3.3 are satisfied.

###### Corollary 0.

All properties of Carbon specified in § 3.3 are satisfied.

###### Proof.

We list all the properties of Carbon and their corresponding proofs:

  * •

Commitment validity follows from Theorem 21.

  * •

Commitment integrity follows from Theorem 1.

  * •

Commitment learning follows from Theorem 22.

  * •