# Carbon: An Asynchronous Voting-Based Payment System for a Client-Server
Architecture

Martina Camaioni  École Polytechnique Fédérale de Lausanne (EPFL)Switzerland ,
Rachid Guerraoui  École Polytechnique Fédérale de Lausanne (EPFL)Switzerland ,
Jovan Komatovic  École Polytechnique Fédérale de Lausanne (EPFL)Switzerland ,
Matteo Monti  École Polytechnique Fédérale de Lausanne (EPFL)Switzerland and
Manuel Vidigueira  École Polytechnique Fédérale de Lausanne (EPFL)Switzerland

###### Abstract.

We present Carbon, an asynchronous payment system. To the best of our
knowledge, Carbon is the first asynchronous payment system designed
specifically for a client-server architecture. Namely, besides being able to
make payments, clients of Carbon are capable of changing the set of running
servers using a novel voting mechanism – asynchronous, balance-based voting.

††copyright: none††conference:  ; ; ††journalyear: 2021

##  1\. Introduction & Overview

This document represents the definition of the problem Carbon solves, its
implementation and formal proof of correctness.

##### Problem overview.

In its core, Carbon solves the asset-transfer problem (auvolat2020money, ;
collins2020online, ; guerraoui2019consensus, ; kuznetsov2021permissionless, ;
nakamoto2008bitcoin, ; wood2014ethereum, ) among its users. A user of Carbon
is able to issue a payment transaction transferring its money to another user,
thus decreasing its balance and increasing the balance of the receiving user.
In a nutshell, Carbon guarantees the following two properties:

  * •

_Liveness:_ A payment issued by a user is eventually processed, thus
decreasing the balance of the issuer and increasing the balance of the
receiver.

  * •

_Safety:_ No user can successfully issue multiple payments using the “same”
money.

The violation of the safety property is traditionally known as _double-
spending_ (nakamoto2008bitcoin, ) and represents the core problem in
implementing a cryptocurrency.

Since the goal of Carbon is to serve millions of users in an efficient way,
users themselves cannot be responsible for processing payments. To this end,
we introduce _servers_ : members of the system that are actually responsible
for processing payments issued by Carbon’s users. Since Carbon is designed to
be a long-lived BFT system, set of servers that actually process transactions
must change over time (e.g., failed servers should be replaced with new ones).
Thus, Carbon supports _reconfiguration_ : the feature of changing the set of
servers running the system while still processing payments.

Importantly, the set of servers running the system is _chosen_ by users of
Carbon. Specifically, users select which servers run Carbon through a _voting_
mechanism: a user can support “candidacy” of a server for a spot in the
“running set” by issuing a special vote transaction. A server eventually joins
the set of running servers if money owned by users that have supported its
candidacy accounts for more than half of the total amount of money in Carbon.

##### Inspiration.

Carbon is influenced by a variety of previously developed ideas. This
paragraph briefly presents the work which has inspired the development of
Carbon.

The problem of a cryptocurrency rose to prominence with Bitcoin
(nakamoto2008bitcoin, ). Bitcoin solves the problem by ensuring that its users
agree on a sequence of processed transactions (i.e., payments), i.e., all
transactions are totally-ordered. Since then, many protocols have followed the
same approach in solving the problem (buchman2018latest, ; wood2014ethereum, ;
bitcoin-ng_nsdi16, ; algorand_sosp17, ; stellar_sosp19, ; omniledger_sp18, ).

Only recently has it been shown that total order of transactions is not
necessary to solve the problem of asset-transfer (guerraoui2019consensus, ),
which lies at the core of any cryptocurrency. Consequently, the reliable
broadcast primitive (cachin2011introduction, ), which can be implemented in a
completely asynchronous distributed system, suffices for asset-transfer
(collins2020online, ; auvolat2020money, ). Carbon builds upon this approach by
adopting the reliable broadcast primitive for processing transactions.

On the other hand, reconfiguration of distributed systems have been studied in
both crash-stop (aguilera2011dynamic, ; alchieri2018efficient, ;
jehl2015smartmerge, ; gafni2015elastic, ) and Byzantine
(kuznetsov2020asynchronous, ; guerraoui2020dynamic, ) failure model. Since
Carbon solves the cryptocurrency problem, which implies that Carbon assumes
the Byzantine failure model, the reconfiguration logic of Carbon relies on
(kuznetsov2020asynchronous, ; guerraoui2020dynamic, ). More concretely,
Carbon’s reconfiguration mechanism is identical to the one of dbrb
(guerraoui2020dynamic, ).

##### Roadmap.

We start by introducing the system model and preliminaries in § 2. § 3
provides the formal definition of the problem Carbon solves. Then, we give the
implementation of Carbon. First, we present the view generator primitive,
which is the crucial building block of the reconfiguration mechanism of Carbon
(§ 4). § 5 is devoted to the storage module of a server: the module used for
storing information. In § 6, we introduce the reconfiguration module of a
server: the module that contains the reconfiguration logic of a server. Next,
we introduce the implementation of a Carbon user in § 7. § 8 presents the
transaction module of a server: the module used for processing payments issued
by users of Carbon. Finally, § 9 is devoted to the voting module of a server:
the module responsible for ensuring the validity of Carbon’s voting mechanism.

##  2\. System Model & Preliminaries

##### Clients & servers.

We consider a system of _asynchronous_ processes: a process proceeds at its
own arbitrary (and non-deterministic) speed. Each process is either a _client_
or a _server_. We denote by $\mathcal{C}$ the (possibly infinite) set of
clients and by $\mathcal{R}$ the (possibly infinite) set of servers. Each
process in the system is assigned its _protocol_ to follow.

A process is in one of the four states at all times:

  * •

_inactive:_ The process has not yet performed a computational step.

  * •

_obedient:_ The process has performed a computational step and followed its
protocol.

  * •

_disobedient:_ The process has performed a computational step and (at some
point) deviated from its protocol.

  * •

_halted:_ The process has stopped executing computational steps.

Every process starts its execution in the inactive state. Once the special
$\mathtt{start}$ event triggers at the process (e.g., the process turns on),
the process transits to the obedient state. The process remains in the
obedient state as long as it respects the assigned protocol and does not
execute the special $\mathtt{stop}$ command. Once the process deviates from
the assigned protocol, the process transits to the disobedient state and stays
there permanently. Finally, once the special $\mathtt{stop}$ command is
executed by the process (e.g., the process shuts down) which is in the
obedient state, the process halts and stays in the halted state. If the
process performs a computational step afterwards, it transits to the faulty
state (and remains in that state forever). The state diagram of a process is
given in Figure 1.

Figure 1. State diagram of a process.

Once the $\mathtt{start}$ event triggers at a process, we say that the process
_starts_. We assume that only finitely many servers start in any execution. On
the other hand, infinitely many clients are allowed to start. Any process that
starts and does not transit to the disobedient state is said to be _correct_.
Any correct process that never halts is _forever-correct_. If, at any point, a
process transits to the disobedient state, the process is _faulty_.

##### Cryptographic primitives.

We make use of standard cryptographic primitives. Specifically, we assume an
idealized _public-key infrastructure_ (PKI): each process is associated with
its own public/private key pair that is used to sign messages and verify
signatures of other processes. Each message has its sender; we denote by
$m.\mathtt{sender}$ the sender of message $m$. All messages are signed by
their senders. We assume that faulty processes cannot forge signatures of
correct processes. Moreover, a message that is not properly signed is
immediately discarded by a correct process. We assume that processes can
forward messages to other processes and include messages in other messages;
forwarded and included messages can also be authenticated, i.e., their
signatures can be verified111If an included or forwarded message is not
properly signed, the entire message is discarded by a correct process..

##### Execution paradigm.

We assume that each process is single-threaded, i.e., the execution of the
protocol assigned to each process is single-threaded. The protocol of a
process consists of a set of $\mathtt{upon}$ rules; if a rule guarding a part
of the protocol is permanently active at a correct process, we assume that the
part of the protocol guarded by that rule is eventually executed.

A discrete global clock is assumed and the range of clock’s ticks is the set
$\\{0\\}\cup\mathbb{N}$. No process has access to the discrete global clock.
Computation proceeds in atomic steps. Each step happens at a clock’s tick and
a process may: (1) send a message, (2) receive a message, (3) get an external
input (e.g., trigger of the special $\mathtt{start}$ event), or (4) perform an
internal computation.

##### Communication.

The processes are connected pair-wise by _asynchronous_ authenticated channels
(cachin2011introduction, ): there does not exist an upper bound on message
delays. The only requirement is that message delays are finite.

We assume the existence of the following communication primitives:

  1. (1)

_Perfect links:_ A process can directly send a message $m$ to a process $q$;
we write “$\mathtt{send}$ $m\text{ }\mathtt{to}\text{ }q$”. Perfect links
provide the following properties:

     * •

_Validity:_ If a forever-correct process sends a message to a forever-correct
process, then the message is eventually received.

     * •

_Integrity:_ A message is received at most once by a correct process and, if
the sender is correct, only if the message was sent by the sender.

Note that perfect links present a generalization of the perfect links
primitive (cachin2011introduction, ) to a dynamic environment in which correct
processes can halt.

  2. (2)

_Best-effort broadcast:_ This primitive allows a process to send the same
message $m$ to a fixed set of processes; we write “$\mathtt{broadcast}$
$m\text{ }\mathtt{to}\text{ }S$”, where $S$ is a set of processes. The best-
effort broadcast ensures:

     * •

_Validity:_ If a forever-correct process broadcasts a message to a set $S$ of
processes and a process $q\in S$ is forever-correct, then $q$ eventually
receives the message.

     * •

_Integrity:_ A message is received at most once by a correct process and, if
the sender is correct, only if the message was broadcast by the sender.

The best-effort primitive represents the generalization of the primitive
(cachin2011introduction, ) to dynamic environments. It consists of sending the
broadcast message to all processes from the set of receivers using the perfect
links.

  3. (3)

_Gossip:_ This primitive (kermarrec2007gossiping, ) allows a process to
disseminate a message $m$ to all processes without specifying the particular
set of receivers; we write “$\mathtt{gossip}$ $m$”. The gossip primitive
ensures the following properties:

     * •

_Validity:_ If a forever-correct process gossips a message, then every
forever-correct process receives the message infinitely many times.

     * •

_Integrity:_ If a message is received by a correct process and the sender of
the message is correct, then the message was previously gossiped by the
sender.

##### Preliminaries.

We now introduce the concepts of changes, views and sequences. A _change_
$c\in\\{+,-\\}\times\mathcal{R}$ is a tuple that expresses an intent of a
server either to _join_ the set of servers running Carbon or to _leave_ it
(see § 1). For instance, $c=(+,r)$ denotes the intent of server
$r\in\mathcal{R}$ to join, whereas $c^{\prime}=(-,r^{\prime})$ denotes the
intent of server $r^{\prime}\in\mathcal{R}$ to leave.

⬇

1Change:

2 instance $c=(s,r)$, with $s\in\\{+,-\\}$ and $r$ is Server

Listing 1: Change

A _view_ is a set of changes. We associate three functions with any view $v$:

  * •

$\mathtt{members}$: returns _members_ of the view $v$, i.e., returns all the
servers $r\in\mathcal{R}$ such that $(+,r)\in v$ and $(-,r)\notin v$.

  * •

$\mathtt{quorum}$: returns the _quorum size_ of the view $v$, i.e., it returns
$n-\lfloor\frac{n-1}{3}\rfloor$, where $n=|v.\mathtt{members}()|$.

  * •

$\mathtt{plurality}$: returns the _plurality_ of the view $v$, i.e., it
returns $\lfloor\frac{n-1}{3}\rfloor+1$, where $n=|v.\mathtt{members}()|$.

We say that views $v_{1}$ and $v_{2}$ are _comparable_ if and only if
$v_{1}\subseteq v_{2}$ or $v_{1}\supset v_{2}$. If $v_{1}\subset v_{2}$, we
say that $v_{1}$ is _smaller than_ $v_{2}$ and $v_{2}$ is _greater than_
$v_{1}$. Finally, we render some views as _valid_ (we give the formal
definition in Definition 1).

⬇

1View:

2 instance $v$, with $v$ is Set(Change)

4 function (View $v$).members():

5 return $\\{r$ $|$ $(+,r)\in v$ and $(-,r)\notin v\\}$

7 function (View $v$).quorum():

8 $n=|v$.members()$|$

9 return $n-\lfloor\frac{n-1}{3}\rfloor$

11 function (View $v$).plurality():

12 $n=|v$.members()$|$

13 return $\lfloor\frac{n-1}{3}\rfloor+1$

15 function comparable(View $v$, View $w$):

16 return $v\subseteq w$ or $v\supset w$

18 function valid(View $v$) $\to\\{\top,\bot\\}$

Listing 2: View

Lastly, a _sequence_ is a set of views with any two views of the sequence
being comparable. We say that a sequence $\mathit{seq}$ _follows_ a view $v$
if all views contained in $\mathit{seq}$ are greater than $v$. Moreover, we
define the _first_ (resp., _last_) view of a sequence as the smallest (resp.,
greatest) view that belongs to the sequence.

⬇

1Sequence:

2 instance $\mathit{seq}$, with $\mathit{seq}$ is Set(View) such that
comparable($v,w$) $=\top$, for all $v,w\in\mathit{seq}$

4 function (Sequence $\mathit{seq}$).follows(View $v$):

5 return for every $w\in\mathit{seq}$: $w\supset v$

7 function (Sequence $\mathit{seq}$).first():

8 return $w\in\mathit{seq}$ such that $w\subseteq v$, for every
$v\in\mathit{seq}$

10 function (Sequence $\mathit{seq}$).last():

11 return $w\in\mathit{seq}$ such that $w\supseteq v$, for every
$v\in\mathit{seq}$

Listing 3: Sequence

If $\mathit{seq}=\\{v_{1},...,v_{x}\\}$ is a sequence, we write
$\mathit{seq}=v_{1}\to...\to v_{x}$, where $v_{i}\subset v_{i+1}$, for every
$1\leq i<x$.

In summary, a change is a tuple $c=(\mathit{sym}\in\\{+,-\\},r\in\mathcal{R})$
and it symbolizes the intent of server $r$ to either join (if
$\mathit{sym}=+$) or leave (if $\mathit{sym}=-$). A view is a set of changes,
whereas a sequence is a set of comparable views.

##### Failure model.

We assume that at most $\lfloor\frac{n-1}{3}\rfloor$ members of $v$ are
faulty, where $n=|v.\mathtt{members()}|$, for every valid view $v$.222Recall
that a view $v$ is valid if and only if $\mathtt{valid}(v)=\top$ (see
LABEL:lst:view).

##### Certificates.

Throughout the implementation of Carbon, we often use _certificates_. A
certificate is a construct used to prove that a value is indeed “produced” by
a specific instance of a distributed primitive. Therefore, certificates
prevent faulty processes to “lie” about obtained values. If
$\mathtt{verify\\_output}(\mathit{value},\mathit{instance},\omega)=\top$, then
we say that $\mathit{value}$ is _produced_ by $\mathit{instance}$, where
$\mathit{instance}$ is an instance of a distributed primitive.

⬇

1function verify_output(Value $\mathit{value}$, Distributed_Primitive_Instance
$\mathit{instance}$, Certificate $\omega$) $\to\\{\top,\bot\\}$

Listing 4: The $\mathtt{verify\\_output}$ function

##### Constants.

We assume the existence of a specific view known by all processes; we denote
this view by $\mathit{genesis}$. The $\mathit{genesis}$ view does not contain
$(-,r)$ changes, i.e., $(-,r)\notin\mathit{genesis}$, for any server $r$.
Moreover, $\mathit{genesis}$ has only finitely many members. Finally, we
assume that the $\mathtt{start}$ event eventually triggers at all members of
the $\mathit{genesis}$ view.

⬇

1Constants:

2 View $\mathit{genesis}$

Listing 5: Constants

##  3\. Problem Definition

As briefly mentioned in § 1, the core problem solved by Carbon is the asset-
transfer problem (auvolat2020money, ; collins2020online, ;
guerraoui2019consensus, ; kuznetsov2021permissionless, ; nakamoto2008bitcoin,
; wood2014ethereum, ) among clients (i.e., users of Carbon). We present the
formal definition of the asset-transfer problem in § 3.1.

Since our goal is to allow Carbon to efficiently serve millions of clients,
the burden of transaction processing must be taken away from clients. We put
this burden on a set of servers - _validators_. In order to allow clients to
select validators that actually process payments in Carbon, we develop
_asynchronous balance-based voting_ : the mechanism that allows clients to
vote a server in or out of the set of validators. We formally define the
asynchronous balance-based voting problem in § 3.2.

Finally, the definitive formulation of the problem consists of the asset-
transfer problem (§ 3.1) enriched by the problem of changing the set of
validators based on our voting mechanism (§ 3.2). We merge these in § 3.3,
thus painting the full picture of the problem Carbon solves.

###  3.1. Core Problem: Asset-Transfer

The asset-transfer problem allows clients to issue transactions in order to
(1) transfer some of their money to another clients, thus decreasing their
balance, and (2) claim money transferred to them by another clients, thus
increasing their balance. We proceed to formally define the asset-transfer
problem.

##### Transactions.

Clients can issue transactions of the following three types:

  * •

_withdrawal:_ A client issues a withdrawal transaction once it aims to
transfer some of its money to another client.

  * •

_deposit:_ A client issues a deposit transaction in order to claim money
transferred to it by another client.

  * •

_minting:_ A client issues a minting transaction to increase the amount of
money owned by it.

⬇

1Withdrawal_Transaction:

2 Client $\mathit{issuer}$

3 Client $\mathit{receiver}$

4 Integer $\mathit{amount}$

5 Integer $\mathit{sn}$

⬇

1Deposit_Transaction:

2 Client $\mathit{issuer}$

3 Withdrawal_Transaction
$\mathit{withdrawal}$

4 Integer $\mathit{sn}$

⬇

1Minting_Transaction:

2 Client $\mathit{issuer}$

3 Integer $\mathit{amount}$

4 Integer $\mathit{sn}$

Each transaction is parameterized with its issuer (i.e., the client issuing
the transaction) and its sequence number. Withdrawal transactions specify the
client that receives the transferred money and the amount of the money being
transferred. Each deposit transaction specifies a corresponding withdrawal
transaction, i.e., the transaction that allows the issuer to claim the money.
A minting transaction specifies the amount of money the issuer obtains. For
the sake of simplicity, we assume that sequence numbers of all transactions
are greater than $0$ and, if $\mathit{tx}$ is a deposit transaction, then
$\mathit{tx}.\mathit{widthdrawal}.\mathit{receiver}=\mathit{tx}.\mathit{issuer}$.
We denote by $\mathcal{T}$ the set of all possible transactions.

##### Client’s balance.

Each client has its _balance_ , i.e., the amount of money owned by the client
at a given time. The balance of a client is the sum of claimed (by deposit or
minting transactions) money subtracted by the sum of transferred money. The
initial balance of a client $c$ is denoted by $\mathtt{initial\\_balance}(c)$.

##### Commitment proofs.

We denote by $\Sigma_{c}$ the set of _commitment proofs_. Intuitively, a
commitment proof shows that a specific transaction is succesfully processed in
Carbon. Formally, we define the $\mathtt{verify\\_commit}\text{:
}\mathcal{T}\times\Sigma_{c}\to\\{\top,\bot\\}$ function that maps a
transaction and a commitment proof into a boolean value. A transaction
$\mathit{tx}\in\mathcal{T}$ is _commited_ if and only if a (correct or faulty)
process obtains (i.e., stores in its local memory) a commitment proof
$\sigma_{c}\in\Sigma_{c}$ such that
$\mathtt{verify\\_commit}(\mathit{tx},\sigma_{c})=\top$; if the first
attainment of such commitment proof occurs at time $t$, we say that
$\mathit{tx}$ is committed at time $t^{\prime}\geq t$.

##### Logs.

A _log_ is a set of transactions. We say that a log $\mathit{log}$ is
_admissible_ if and only if:

  * •

for every deposit transaction $\mathit{tx}\in\mathit{log}$,
$\mathit{tx}.\mathit{withdrawal}\in\mathit{log}$, i.e., a deposit transaction
is “accompanied” by the corresponding withdrawal transaction, and

  * •

for each client $c$, let
$\mathit{log}_{c}=\\{\mathit{tx}\,|\,\mathit{tx}\in\mathit{log}\text{ and
}\mathit{tx}.\mathit{issuer}=c\\}$. Then, the following holds:

    * –

$\mathit{log}_{c}$ does not contain conflicting transactions, i.e., different
transactions with the same sequence number, and

    * –

all transactions in $\mathit{log}_{c}$ must have adjacent sequence numbers,
i.e., no “gaps” can exist, and

    * –

a single withdrawal transaction is referenced by at most one deposit
transaction, i.e., the client cannot claim the “same” money multiple times,
and

    * –

the client has enough money for every issued withdrawal transaction.

More formally, a log $\mathit{log}$ is admissible if and only if
$\mathtt{admissible}(\mathit{log})=\top$, where the $\mathtt{admissible}$
function is defined in LABEL:lst:admissible_transaction_set.

Before introducing the $\mathtt{admissible}$ function, we define the notion of
_precedence_ in a set of transactions. Let $X$ be a set of transactions. We
say that $\mathit{tx}_{1}\in X$ precedes $\mathit{tx}_{2}\in X$ in $X$ if :

  * •

$\mathit{tx}_{1}.\mathit{issuer}=\mathit{tx}_{2}.\mathit{issuer}$ and
$\mathit{tx}_{1}.\mathit{sn}<\mathit{tx}_{2}.\mathit{sn}$, or

  * •

$\mathit{tx}_{1}$ is a withdrawal transaction, $\mathit{tx}_{2}$ is a deposit
transaction and $\mathit{tx}_{2}.\mathit{withdrawal}=\mathit{tx}_{1}$, or

  * •

there exists a transaction $\mathit{tx}$ such that $\mathit{tx}_{1}$ precedes
$\mathit{tx}$ in $X$ and $\mathit{tx}$ precedes $\mathit{tx}_{2}$ in $X$.

Finally, we give the definition of the $\mathtt{admissible}$ function.

⬇

1function admissible(Log $\mathit{log}$):

2 // check whether there are cycles

3 if exists Transaction $\mathit{tx}\in\mathit{log}$ such that $\mathit{tx}$
precedes $\mathit{tx}$ in $\mathit{log}$

4 return $\bot$

6 // check whether the withdrawals of all deposit transactions are in
$\mathit{log}$

7 for each Deposit_Transaction $\mathit{tx}\in\mathit{log}$:

8 if $\mathit{tx}.\mathit{withdrawal}\notin\mathit{log}$:

9 return $\bot$

11 for each Client $c$:

12 Log $\mathit{log}_{c}=\\{\mathit{tx}\,|\,\mathit{tx}\in\mathit{log}\text{
and }\mathit{tx}.\mathit{issuer}=c\\}$

13 if admissible_client_log($c$, $\mathit{log}_{c}$) $=\bot$: // the client
log is not admissible

14 return $\bot$

15 return $\top$

17function admissible_client_log(Client $c$, Log $\mathit{log}_{c}$):

18 // if $\mathit{log}_{c}$ is empty, then return $\top$

19 if $\mathit{log}_{c}=\emptyset$:

20 return $\top$

22 // if there exist conflicting transactions, return $\bot$

23 if exist Transaction $\mathit{tx}_{1},\mathit{tx}_{2}\in\mathit{log}_{c}$
such that $\mathit{tx}_{1}\neq\mathit{tx}_{2}$ and
$\mathit{tx}_{1}.\mathit{sn}=\mathit{tx}_{2}.\mathit{sn}$:

24 return $\bot$

26 // sequence numbers of transactions must be adjacent

27 if exists Transaction $\mathit{tx}\in\mathit{log}_{c}$ and exists Integer
$\mathit{num}$, where $1\leq\mathit{num}<\mathit{tx}.\mathit{sn}$, such that
does not exist Transaction $\mathit{tx}^{\prime}\in\mathit{log}_{c}$ with
$\mathit{tx}^{\prime}.\mathit{sn}=\mathit{num}$:

28 return $\bot$

30 // the client log contains non-conflicting transactions and transactions
have adjacent sequence numbers

31 // sort the log by the sequence numbers of the transactions in the
ascending order

32 Array $\mathit{array\\_log}_{c}=\mathit{log}_{c}$.sort_by($\mathit{sn}$)

34 // introduce the balance of the client before executing any transaction
from its log

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

36 Set(Withdrawal_Transaction) $\mathit{withdrawals}=\emptyset$ // observed
withdrawal transactions

38 // iterate through all transactions in the increasing order of their
sequence numbers

39 for each Transaction $\mathit{tx}\in\mathit{array\\_log}_{c}$:

40 if $\mathit{tx}$ is Withdrawal_Transaction: // withdrawal transaction

41 if $\mathit{tx}.\mathit{amount}>\mathit{balance}$: // not enough money

42 return $\bot$

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

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

45 if $\mathit{tx}.\mathit{withdrawal}\in\mathit{withdrawals}$: // withdrawal
already used

46 return $\bot$

47 else:

48
$\mathit{withdrawals}=\mathit{withdrawals}\cup\\{\mathit{tx}.\mathit{withdrawal}\\}$

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

50 else: // minting transaction

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

53 return $\top$

Listing 6: Log admissibility

##### Interface.

Interface of a client consists of:

  * •

invocation $\mathtt{issue}\text{ }\mathit{tx}$: the client issues a
transaction $\mathit{tx}$,

  * •

invocation $\mathtt{query}\text{ }\mathtt{market}$: the client requests to
learn the total amount of money in Carbon,

  * •

indication $\mathtt{committed}\text{ }\mathit{tx}$: the client learns that a
transaction $\mathit{tx}$ is committed, and

  * •

indication $\mathtt{total}\text{ }\mathtt{money}\text{ }\mathit{money}$: the
client learns that the total amount of money in Carbon is $\mathit{money}$.

##### Rules.

The following is assumed about a correct client $c$:

  * •

The client does not invoke an operation (i.e., does not issue a transaction or
does not query about the total amount of money) before the previous invocation
is completed.

  * •

If a transaction $\mathit{tx}$ is issued by $c$, then
$\mathit{tx}.\mathit{issuer}=c$.

  * •

Client $c$ does not issue a transaction before it learns that all previously
issued transactions by $c$ are committed.

  * •

Let $\mathit{tx}$ be the $i$-th transaction issued by $c$. Then,
$\mathit{tx}.\mathit{sn}=i$.

  * •

Client $c$ does not issue a withdrawal transaction $\mathit{tx}$ unless the
balance of $c$ at the moment of issuing $\mathit{tx}$ is at least
$\mathit{tx}.\mathit{amount}$.

  * •

Client $c$ does not issue a deposit transaction $\mathit{tx}$ before it learns
that $\mathit{tx}.\mathit{withdrawal}$ is committed.

  * •

Client $c$ does not issue conflicting transactions, i.e., different
transactions with the same sequence number.

  * •

Client $c$ does not issue multiple deposit transactions that reference the
same withdrawal transaction.

##### Properties.

Finally, we introduce the properties of the asset-transfer problem:

  * •

_Commitment Validity:_ If a forever-correct client issues a transaction
$\mathit{tx}$, then $\mathit{tx}$ is eventually committed.

  * •

_Commitment Integrity:_ If a transaction $\mathit{tx}$ is committed and
$\mathit{tx}.\mathit{issuer}$ is correct, then $\mathit{tx}$ was issued by
$\mathit{tx}.\mathit{issuer}$.

  * •

_Commitment Learning:_ Let a transaction $\mathit{tx}$ be committed. If
$\mathit{tx}.\mathit{issuer}$ is forever-correct, then $\mathit{tx}$
eventually learns that $\mathit{tx}$ is committed. If $\mathit{tx}$ is a
withdrawal transaction and $\mathit{tx}.\mathit{receiver}$ is forever-correct,
then $\mathit{tx}.\mathit{receiver}$ eventually learns that $\mathit{tx}$ is
committed.

  * •

_Commitment Admissibility:_ Let $\mathit{log}_{t}$ denote the set of all
committed transactions at time $t$. For all times $t$, $\mathit{log}_{t}$ is
admissible.

  * •

_Query Validity:_ If a forever-correct client requests to learn the total
amount of money in Carbon, the client eventually learns.

  * •

_Query Safety:_ Let $\mathit{mints}_{\infty}$ denote the set of all committed
minting transactions. If a correct client learns that the total amount of
money is $\mathit{money}$, then
$\mathit{money}\leq\sum\limits_{\mathit{tx}\in\mathit{mints}_{\infty}}\mathit{tx}.\mathit{amount}$.

  * •

_Query Liveness:_ Let $\mathit{mints}$ denote a finite set of committed
minting transactions. If a forever-correct client requests infinitely many
times to learn the total amount of money in Carbon, the client eventually
learns
$\mathit{money}\geq\sum\limits_{\mathit{tx}\in\mathit{mints}}\mathit{tx}.\mathit{amount}$.

###  3.2. Asynchronous Balance-Based Voting

The asynchronous balance-based voting mechanism revolves around the clients
being able to express their support for a specific _motion_ by issuing _vote_
transactions. Intuitively, a motion _passes_ if “enough” clients (i.e.,
clients that own “enough” money) have expressed their support for the motion.
We formally define the problem below.

##### Vote transactions.

As withdrawal and deposit transactions, each vote transaction is parametrized
with its issuer and its sequence number. Moreover, each vote transaction
specifies the motion for which the issuer votes by issuing the transaction.

⬇

1Vote_Transaction:

2 Client $\mathit{issuer}$

3 Motion $\mathit{motion}$

4 Integer $\mathit{sn}$

##### Motions.

A motion is any statement that can be voted for by clients. We say that a
motion $\mathit{mot}$ is _proposed_ at time $t$ if and only if a correct
process (either client or a server) obtains a vote transaction for
$\mathit{mot}$ at time $t$ and no correct process has obtained a vote
transaction for $\mathit{mot}$ before $t$. Intuitively, a motion is proposed
at time $t$ if and only if the first correct process to observe a client
voting for the motion observes such voting action at time $t$.

A log _supports_ a motion if a “majority” of the money votes for the motion.
In order to formally define when a log supports a motion, we first define how
the balance of each client is calculated in a log. Moreover, we define the
total amount of money in a log. Finally, we define the amount of money in a
log “voting” for a motion.

⬇

1Log:

2 instance $\mathit{log}$, with $\mathit{log}$ is Set(Transaction)

4 function (Log $\mathit{log}$).balance(Client $c$):

5 Log $\mathit{log}_{c}=\\{\mathit{tx}\,|\,\mathit{tx}\in\mathit{log}\text{
and }\mathit{tx}.\mathit{issuer}=c\\}$

6 $\mathit{balance}=$ initial_balance($c$)

7 Array $\mathit{array\\_log}_{c}=\mathit{log}_{c}$.sort_by($\mathit{sn}$) //
sort the log by the sequence numbers

8 for each Transaction $\mathit{tx}\in\mathit{array\\_log}_{c}$:

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

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

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

12
$\mathit{balance}=\mathit{balance}+\mathit{tx}.\mathit{witdrawal}.\mathit{amount}$

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

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

15 return $\mathit{balance}$

17 function (Log $\mathit{log}$).total_money():

18 Set(Transaction)
$\mathit{mints}=\\{\mathit{tx}\,|\,\mathit{tx}\in\mathit{log}\text{ and
}\mathit{tx}\text{ is Minting\\_Transaction}\\}$

19 return
$\sum\limits_{\mathit{tx}\in\mathit{mints}}\mathit{tx}.\mathit{amount}$ // the
sum of all minting transactions

21 function (Log $\mathit{log}$).voted_for(Motion $\mathit{mot}$):

22 Set(Client) $\mathit{voted\\_for}=\\{c\,|\,\mathit{tx}\in\mathit{log}\text{
and }\mathit{tx}\text{ is Vote\\_Transaction and
}\mathit{tx}.\mathit{motion}=\mathit{mot}\text{ and
}\mathit{tx}.\mathit{issuer}=c\\}$

23 return
$\sum\limits_{c\in\mathit{voted\\_for}}\mathit{log}\text{.balance(}c\text{)}$

Listing 7: Log

Finally, we are ready to formally define when a log supports a motion. A log
$\mathit{log}$ supports a motion $\mathit{mot}$ if and only if
$\mathtt{support}(\mathit{log},\mathit{mot})=\top$, where the
$\mathtt{support}$ function is defined in the following manner:

⬇

1function support(Log $\mathit{log}$, Motion $\mathit{mot}$):

2 return $\mathit{log}$.voted_for($\mathit{mot}$)$>0$ and
$\mathit{log}\text{.voted\\_for(}\mathit{mot}\text{)}\geq\frac{\mathit{log}\text{.total\\_money()}}{2}$

Listing 8: Motion support

##### Voting proofs.

We denote by $\Sigma_{v}$ the set of _voting proofs_. Intuitively, a voting
proof shows that a specific motion passes. Formally, a motion $\mathit{mot}$
_passes_ if and only if a (correct or faulty) process obtains a voting proof
$\sigma_{v}\in\Sigma_{v}$ such that
$\mathtt{verify\\_voting}(\mathit{mot},\sigma_{v})=\top$. We use voting proofs
in § 3.3 in order to abstract away the asynchronous balance-based voting
problem (for the sake of simplicity).

##### Rules.

We assume that a correct client does not vote for the same motion more than
once.

##### Properties.

Finally, we define the properties of the asynchronous balance-based voting
primitive:

  * •

_Voting Safety:_ Let a motion $\mathit{mot}$ be proposed at time $t$ and let
$\mathit{mot}$ pass. Let a correct client learn at time $t$ that the total
amount of money in Carbon is $\mathit{money}$ and let $\mathit{log}_{\infty}$
denote the set of all committed transactions. There exists an admissible log
$\mathit{log}_{\mathit{pass}}\subseteq\mathit{log}_{\infty}$ such that
$\mathit{log}_{\mathit{pass}}.\mathtt{voted\\_for}(\mathit{mot})\geq\frac{money}{2}$.

  * •

_Voting Liveness:_ Let a motion $\mathit{mot}$ be proposed and let
$\mathit{log}_{\infty}$ denote the set of all committed transactions. If there
exists an admissible log
$\mathit{log}_{\mathit{pass}}\subseteq\mathit{log}_{\infty}$ such that
$\mathit{log}_{\mathit{greater}}$ supports $\mathit{mot}$, for every
admissible log $\mathit{log}_{\mathit{greater}}$, where
$\mathit{log}_{\mathit{pass}}\subseteq\mathit{log}_{\mathit{greater}}\subseteq\mathit{log}_{\infty}$,
then $\mathit{mot}$ passes.

Intuitively, the voting safety property guarantees that, if a motion passes,
more than half of the money held in the system “at the moment” of proposing
the motion has “voted” for the motion to pass. Voting liveness guarantees that
a motion passes if, after some time, the motion is “forever-supported”.

###  3.3. Carbon = Asset-Transfer + Voting-Driven Reconfiguration

Finally, we formally define the “complete” problem solved by Carbon.

##### Validators.

A correct server _joins_ once the server triggers the special
$\mathtt{joined}$ event; if the special $\mathtt{joined}$ event is triggered
at time $t$, the server joins at time $t$. A faulty server $r$ joins if a
correct server triggers the special $r\text{ }\mathtt{joined}$ event and no
correct server has previously triggered the special $r\text{ }\mathtt{left}$
event; if the first $r\text{ }\mathtt{joined}$ event that satisfies the
aforementioned condition is triggered at time $t$, the server joins at time
$t$.

A correct server _leaves_ once the server triggers the special $\mathtt{left}$
event; if the special $\mathtt{left}$ event is triggered at time $t$, the
server leaves at time $t$. A faulty server $r$ leaves if a correct server
triggers the special $r\text{ }\mathtt{left}$ event; if the first $r\text{
}\mathtt{left}$ event triggered by correct servers is triggered at time $t$,
the server leaves at time $t$. In summary, a correct server joins (resp.,
leaves) once the server itself claims to have joined (resp., left); a faulty
server joins (resp., leaves) once a correct server claims that $r$ has joined
(resp., left).

A server $r$ is a _validator_ at time $t$ if and only if the server joins by
time $t$ and does not leave by time $t$. Moreover, a server is a _forever-
validator_ if and only if it joins and never leaves.

##### Commitment proofs - revisited.

Since the notion of a validator is introduced, we aim to ensure that
transactions are “processed” only by validators of Carbon. Intuitively, if a
transaction $\mathit{tx}$ is issued at time $t$ and a server $r$ left before
time $t$, our goal is to guarantee that $r$ cannot be a server that helps
$\mathit{tx}$ to be processed. In order to formally define such property of
Carbon, we introduce a set of _signers_ of a commitment proof: the set of
servers that have “created” a commitment proof. We denote by
$\sigma_{c}.\mathtt{signers}$ the set of signers of a commitment proof
$\sigma_{c}$.

##### Server’s interface.

Interface of a server consists of two invocations:

  * •

Invocation “$\mathtt{join}\text{ }\mathtt{with}\text{ }\mathtt{voting}\text{
}\mathtt{proof}\text{ }\sigma_{v}$”: The server requests to join (i.e., to
become a validator) and provides the voting proof $\sigma_{v}$ such that
$\mathtt{verify\\_voting}(\text{``add server }r\text{''},\sigma_{v})=\top$.

  * •

Invocation “$\mathtt{leave}$”: The server requests to leave (i.e., to stop
being a validator).

##### Server’s rules.

The following is assumed about a correct server $r$:

  1. (1)

If $r\in\mathit{genesis}.\mathtt{members()}$, then $r$ does not request to
join.

  2. (2)

Server $r$ requests to join at most once.

  3. (3)

If $r$ requests to join and provides the voting proof $\sigma_{v}$, then
$\mathtt{verify\\_voting}(\text{``add server }r\text{''},\sigma_{v})=\top$.

  4. (4)

If $r$ requests to join, then $r$ does not halt before it leaves.

  5. (5)

If $r$ requests to leave, $r$ has previously joined.

  6. (6)

If $r$ leaves, then $r$ immediately halts.

##### Properties of Carbon.

Finally, we introduce the complete list of properties satisfied by Carbon. We
say that a transaction $\mathit{tx}$ is _issued_ at time $t$ if and only if:

  * •

if $\mathit{tx}.\mathit{issuer}$ is correct, then $\mathtt{issue}\text{
}\mathit{tx}$ was invoked at time $t$ (see § 3.1),

  * •

if $\mathit{tx}.\mathit{issuer}$ is not correct, then the first correct
process that obtains $\mathit{tx}$ obtains $\mathit{tx}$ at time $t$.

If the motion “add server $r$” passes, we say that $r$ is _voted in_.
Similarly, if the motion “remove server $r$” passes, we say that $r$ is _voted
out_. We are ready to define the properties of Carbon:

  * •

_Commitment Validity:_ If a forever-correct client issues a transaction
$\mathit{tx}$, then $\mathit{tx}$ is eventually committed.

  * •

_Commitment Integrity:_ If a transaction $\mathit{tx}$ is committed and
$\mathit{tx}.\mathit{issuer}$ is correct, then $\mathit{tx}$ was issued by
$\mathit{tx}.\mathit{issuer}$.

  * •

_Commitment Learning:_ Let a transaction $\mathit{tx}$ be committed. If
$\mathit{tx}.\mathit{issuer}$ is forever-correct, then $\mathit{tx}$
eventually learns that $\mathit{tx}$ is committed. If $\mathit{tx}$ is a
withdrawal transaction and $\mathit{tx}.\mathit{receiver}$ is forever-correct,
then $\mathit{tx}.\mathit{receiver}$ eventually learns that $\mathit{tx}$ is
committed.

  * •

_Commitment Admissibility:_ Let $\mathit{log}_{t}$ denote the set of all
committed transactions at time $t$. At all times $t$, $\mathit{log}_{t}$ is
admissible.

  * •

_Commitment Signing:_ Let a transaction $\mathit{tx}$ be issued at time $t$.
Let a commitment proof $\sigma_{c}$ be obtained at time $t^{\prime}$, where
$\mathtt{verify\\_commit}(\mathit{tx},\sigma_{c})=\top$. If
$a\in\sigma_{c}.\mathtt{signers}$, then $a$ is a validator at time
$t_{\mathit{val}}$, where $t\leq t_{\mathit{val}}\leq t^{\prime}$.

  * •

_Query Validity:_ If a forever-correct client requests to learn the total
amount of money in Carbon, the client eventually learns.

  * •

_Query Safety:_ Let $\mathit{mints}_{\infty}$ denote the set of all committed
minting transactions. If a correct client learns that the total amount of
money is $\mathit{money}$, then
$\mathit{money}\leq\sum\limits_{\mathit{tx}\in\mathit{mints}_{\infty}}\mathit{tx}.\mathit{amount}$.

  * •

_Query Liveness:_ Let $\mathit{mints}$ denote a finite set of committed
minting transactions. If a forever-correct client requests infinitely many
times to learn the total amount of money in Carbon, the client eventually
learns
$\mathit{money}\geq\sum\limits_{\mathit{tx}\in\mathit{mints}}\mathit{tx}.\mathit{amount}$.

  * •

_Join Safety:_ If a server $r$ joins, then
$r\in\mathit{genesis}.\mathtt{members()}$ or $r$ is voted in.

  * •

_Leave Safety:_ If a correct server leaves, then the server requested to leave
or is voted out.

  * •

_Join Liveness:_ If a correct server requests to join, the server eventually
joins (i.e., becomes a validator).

  * •

_Leave Liveness:_ If a correct server requests to leave, the server eventually
leaves (i.e., stops being a validator).

  * •

_Removal Liveness:_ If a correct forever-validator obtains a voting proof
$\sigma_{v}$ such that $\mathtt{verify\\_voting}(\text{``remove server
}r\text{''},\sigma_{v})=\top$ and $r$ is a validator at some time (i.e., $r$
has joined), then $r$ eventually leaves (i.e., stops being a validator).

##  4\. View Generator

The first primitive we present, which is used in the implementation of Carbon,
is the _view generator_ primitive (alchieri2018efficient, ). The view
generator primitive is used by the servers exclusively.

Each instance of the view generator is parameterized with a view. We denote by
$\mathit{vg}(v)$ the instance of the view generator primitive parameterized
with view $v$. Servers can (1) start $\mathit{vg}(v)$ with or without a
proposal, (2) stop $\mathit{vg}(v)$, (3) propose a set of views (along with
some additional information) to $\mathit{vg}(v)$, and (4) decide a set of
views from $\mathit{vg}(v)$. Finally, we assume that (at least) a quorum of
members of view $v$ are correct.

We assume an existence of _evidences_ , which are (for now) abstract
constructs. The input of a view generator instance is a tuple
$(v,\mathit{set},\epsilon)$, where $v$ is a view, $\mathit{set}$ is a set of
views and and $\epsilon$ is a proof. For every tuple
$\mathit{input}=(v,\mathit{set},\epsilon)$ and every view $v^{\prime}$, we
define $\mathtt{valid}(\mathit{input},v^{\prime})$ function that returns
either $\top$ or $\bot$. Again, the concrete implementation of the
$\mathtt{valid}$ function is not given for now.

⬇

1View, Set, Evidence:

2 instance $(v,\mathit{set},\epsilon)$, with $v$ is View, $\mathit{set}$ is
Set(View) and $\epsilon$ is Evidence

4 function valid(View, Set, Evidence $(v,\mathit{set},\epsilon)$, View
$v^{\prime}$) $\to\\{\top,\bot\\}$

Listing 9: (View, Set, Evidence) tuple

We are now ready to introduce the interface of an instance of the view
generator primitive.

⬇

1View Generator:

2 instance $\mathit{vg}(v)$, with $v$ is View

4 Interface:

5 Requests:

6 $\bullet$ <$\mathit{vg}(v)$.Start | View, Set, Evidence $(v^{\prime},\mathit{set}^{\prime},\epsilon^{\prime})$>: starts $\mathit{vg}(v)$; if $(v^{\prime},\mathit{set}^{\prime},\epsilon^{\prime})=\bot$, then $\mathit{vg}(v)$ is started without a proposal. If $(v^{\prime},\mathit{set}^{\prime},\epsilon^{\prime})\neq\bot$, then the server has proposed to $\mathit{vg}(v)$.

8 $\bullet$ <$\mathit{vg}(v)$.Stop>: stops $\mathit{vg}(v)$.

10 $\bullet$ <$\mathit{vg}(v)$.Propose | View, Set, Evidence $(v^{\prime},\mathit{set}^{\prime},\epsilon^{\prime})$>: proposes $(v^{\prime},\mathit{set}^{\prime},\epsilon^{\prime})$ to $\mathit{vg}(v)$.

12 Indications:

13 $\bullet$ <$\mathit{vg}(v)$.Decide | Set(View) $\mathit{set}^{\prime}$, Certificate $\omega^{\prime}$>: indicates that $\mathit{set}^{\prime}$ is decided with the certificate $\omega^{\prime}$.

15 Rules:

16 1) No correct server $r\notin v$.members() invokes any request to
$\mathit{vg}(v)$.

17 2) Every correct server invokes each request at most once.

18 3) If a correct server invokes <$\mathit{vg}(v)$.Start | $(v^{\prime},\mathit{set}^{\prime},\epsilon^{\prime})\neq\bot$>, then the server does not invoke <$\mathit{vg}(v)$.Propose>.

19 4) No correct server invokes <$\mathit{vg}(v)$.Stop> or
<$\mathit{vg}(v)$.Propose> unless it has already invoked
<$\mathit{vg}(v)$.Start>.

20 5) A correct server invokes <$\mathit{vg}(v)$.Stop> before halting.

21 6) If a correct server invokes <$\mathit{vg}(v)$.Start | $(v^{\prime},\mathit{set}^{\prime},\epsilon^{\prime})\neq\bot$> or <$\mathit{vg}(v)$.Propose | $(v^{\prime},\mathit{set}^{\prime},\epsilon^{\prime})$>, then valid($(v^{\prime},\mathit{set}^{\prime},\epsilon^{\prime})$, $v$) $=\top$.

Listing 10: View generator - interface

We denote by $E_{t}^{v}$ the set of evidences such that, for every
$\epsilon\in E_{t}^{v}$, the following holds: (1) $\epsilon$ is obtained
(i.e., stored in the local memory) by time $t$ by a (correct or faulty)
process333Once an evidence is obtained by a (correct or faulty) process, the
evidence is obtained by any time in the future. In other words, an attainment
of an evidence is _irrevocable_., and (2) there exists a view $v^{\prime}$ and
a set of views $\mathit{set}^{\prime}$ that satisfy
$\mathtt{valid}((v^{\prime},\mathit{set}^{\prime},\epsilon),v)=\top$. By
definition, $E_{t}^{v}\subseteq E_{t^{\prime}}^{v}$, for any times
$t,t^{\prime}$ with $t^{\prime}>t$.

Now, let
$\Lambda_{t}^{v}=\\{(v^{\prime},\mathit{set}^{\prime},\epsilon^{\prime})\,|\,\mathtt{valid}((v^{\prime},\mathit{set}^{\prime},\epsilon^{\prime}),v)=\top\text{
and }\epsilon^{\prime}\in E_{t}^{v}\\}$. Due to the fact that
$E_{t}^{v}\subseteq E_{t^{\prime}}^{v}$, for any times $t,t^{\prime}$ with
$t^{\prime}>t$, we have that
$\Lambda_{t}^{v}\subseteq\Lambda_{t^{\prime}}^{v}$.

Moreover, we define the $\mathit{preconditions}(v,t)$ function such that
$\mathit{preconditions}(v,t)=\top$ if and only if:

  * •

for every
$(v^{\prime},\mathit{set}^{\prime},\epsilon^{\prime})\in\Lambda_{t}^{v}$,
$\mathit{set}^{\prime}$ is a sequence, and

  * •

for every
$(v^{\prime},\mathit{set}^{\prime}=\emptyset,\epsilon^{\prime})\in\Lambda_{t}^{v}$,
$v\subset v^{\prime}$, and

  * •

for every
$(v^{\prime},\mathit{set}^{\prime}\neq\emptyset,\epsilon^{\prime})\in\Lambda_{t}^{v}$,
$\mathit{set}^{\prime}.\mathtt{follows}(v)=\top$ and
$v^{\prime}\in\mathit{set}^{\prime}$, and

  * •

if $(+,r)\notin v$, for some server $r$, then, for every
$(v^{\prime},\mathit{set}^{\prime},\epsilon^{\prime})\in\Lambda_{t}^{v}$,
$(-,r)\notin v^{\prime}$ and, if $\mathit{set}^{\prime}\neq\emptyset$,
$(-,r)\notin\mathit{set}^{\prime}.\mathtt{last}()$, and

  * •

for any pair
$(v^{\prime},\mathit{set}^{\prime},\epsilon^{\prime}),(v^{\prime\prime},\mathit{set}^{\prime\prime},\epsilon^{\prime\prime})\in\Lambda_{t}^{v}$,
either $\mathit{set}^{\prime}\subseteq\mathit{set}^{\prime\prime}$ or
$\mathit{set}^{\prime}\supset\mathit{set}^{\prime\prime}$.

Since $\Lambda_{t}^{v}\subseteq\Lambda_{t^{\prime}}^{v}$, for any times
$t,t^{\prime}$ with $t^{\prime}>t$, we have that
$\mathit{preconditions}(v,t^{\prime})=\top\implies\mathit{preconditions}(v,t)=\top$.

Finally, if a (correct or faulty) process obtains (i.e., stores in its local
memory) a certificate $\omega$, where
$\mathtt{verify\\_output}(\mathit{set},\mathit{vg}(v),\omega)=\top$, for some
set $\mathit{set}$ of views, then we say that $\mathit{set}$ is _committed_ by
$\mathit{vg}(v)$. Moreover, $\mathit{set}$ is committed at time $t$ if and
only if the certificate attainment happens at time $t^{\prime}\leq t$. Note
that we assume that an attainment of a certificate is irrevocable; hence, if
$\mathit{set}$ is committed at time $t$, then $\mathit{set}$ is committed at
any time $t^{\prime}>t$.

We are now ready to define properties of $\mathit{vg}(v)$.

⬇

1View Generator:

2 instance $\mathit{vg}(v)$, with $v$ is View

4 Properties:

5 \- Integrity: No correct server $r\notin v$.members() receives any
indication from $\mathit{vg}(v)$.

6 \- Comparability: If $\mathit{set}_{1}$ and $\mathit{set}_{2}$ are committed
by $\mathit{vg}(v)$, then either $\mathit{set}_{1}\subseteq\mathit{set}_{2}$
or $\mathit{set}_{1}\supset\mathit{set}_{2}$.

7 \- Validity: If $\mathit{set}$ is committed by $\mathit{vg}(v)$ at time $t$
and $\mathit{preconditions}(v,t-1)=\top$, then (1)
$\mathit{set}\neq\emptyset$, (2) $\mathit{set}$ is a sequence, and (3)
$\mathit{set}$.follows($v$) = $\top$.

8 \- Membership Validity: If $\mathit{set}$ is committed by $\mathit{vg}(v)$
at time $t$, $(+,r)\notin v$, for some server $r$, and
$\mathit{preconditions}(v,t-1)=\top$, then $(-,r)\notin\mathit{set}$.last().

9 \- Safety: Let $\mathit{set}$ be committed by $\mathit{vg}(v)$ at time $t$
and let $\mathit{preconditions}(v,t-1)=\top$. Then,
$(v^{*},\emptyset,\epsilon^{*})\in\Lambda_{t-1}^{v}$ or
$(v^{*},\mathit{set},\epsilon^{*})\in\Lambda_{t-1}^{v}$, for some view $v^{*}$
and some evidence $\epsilon^{*}$.

10 \- Decision Certification: If a correct server decides $\mathit{set}$ with
a certificate $\omega$ from $\mathit{vg}(v)$, then
verify_output($\mathit{set}$, $\mathit{vg}(v)$, $\omega$) $=\top$.

11 \- Decision Permission: If a set of views is committed by $\mathit{vg}(v)$,
then at least $v$.plurality() of correct members of $v$ have previously
started $\mathit{vg}(v)$.

12 \- Bounded Decisions: Let
$\mathit{SET}=\\{\mathit{set}\,|\,\mathit{set}\text{ is committed by
}\mathit{vg}(v)\\}$. Then, $|\mathit{SET}|<\infty$.

13 \- Liveness: If all correct servers $r\in v$.members() start
$\mathit{vg}(v)$, at least one correct server proposes to $\mathit{vg}(v)$ and
no correct server stops $\mathit{vg}(v)$, then all correct servers $r\in
v$.members() eventually decide from $\mathit{vg}(v)$.

Listing 11: View generator - properties

In order to present the view generator primitive, we start by introducing
_reconfiguration lattice agreement_ (RLA).

###  4.1. Reconfiguration Lattice Agreement (RLA)

The RLA primitive is extremely similar to the Byzantine lattice agreement
(di2020byzantine, ; di2020synchronous, ; zheng2019byzantine, ) primitive. In
the Byzantine lattice agreement (BLA) primitive, each process $p$ starts with
its proposal $\mathit{pro}_{p}\in\mathcal{V}$ and eventually decides
$\mathit{dec}_{p}\in\mathcal{V}$. Values from the $\mathcal{V}$ set form a
join semi-lattice $L=(\mathcal{V},\oplus)$ for a commutative join operation
$\oplus$. That is, for any two $v_{1},v_{2}\in\mathcal{V}$, $v_{1}\leq v_{2}$
if and only if $v_{1}\oplus v_{2}=v_{2}$. If
$V=\\{v_{1},v_{2},...,v_{n}\\}\subseteq\mathcal{V}$, $\bigoplus(V)=v_{1}\oplus
v_{2}\oplus...\oplus v_{n}$. BLA that tolerates up to $f$ Byzantine failures
ensures:

  * •

_Liveness:_ Each correct process eventually outputs its decision value
$\mathit{dec}\in\mathcal{V}$.

  * •

_Stability:_ Each correct process outputs a unique decision value.

  * •

_Comparability:_ Given any two correct processes $p,q$, either
$\mathit{dec}_{p}\leq\mathit{dec}_{q}$ or
$\mathit{dec}_{q}\leq\mathit{dec}_{p}$.

  * •

_Inclusivity:_ Given any correct process $p$, we have that
$\mathit{pro}_{p}\leq\mathit{dec}_{p}$.

  * •

_Non-Triviality:_ Given any correct process $p$, we have that
$\mathit{dec}_{p}\leq\bigoplus(X\cup B)$, where $X$ is the set of proposed
values of all correct processes ($X=\\{\mathit{pro}_{q}\,|\,q\text{ is
correct}\\}$) and $B\subseteq\mathcal{V}$ satisfies $|B|\leq f$.

RLA considers a specific semi-lattice over sets, i.e., $\mathcal{V}$ is a set
of sets in RLA and $\oplus$ is the union operation. More specifically,
$\mathcal{V}$ is a set of sets of objects of abstract type $\mathtt{X}$, where
the function $\mathtt{valid}$ is defined for each object of type $X$ and each
view. Finally, in contrast to BLA, not all correct processes are required to
propose in RLA.

Each instance of the RLA primitive is associated with a single view. However,
an RLA instance is not completely defined by its view (in contrast to
instances of the view generator primitive), i.e., there can exist multiple
instances of the RLA primitive associated with the same view. Therefore, each
instance of the RLA primitive is also associated with a unique identifier. In
summary, one instance of the RLA primitive is completely defined by its view
and its identifier; the instance associated with view $v$ and identifier
$\mathit{id}$ is denoted by $\mathit{rla}(v,\mathit{id})$. As for the failure
model assumed by RLA, (at least) a quorum of members of view $v$ are assumed
to be correct.

We now introduce the interface of an RLA instance.

⬇

1Reconfiguration Lattice Agreement:

2 instance $\mathit{rla}(v,\mathit{id})$, with $v$ is View and $\mathit{id}$
is Integer

4 Interface:

5 Requests:

6 $\bullet$ <$\mathit{rla}(v,\mathit{id})$.Start | Set(X) $\mathit{pro}$>: starts $\mathit{rla}(v,\mathit{id})$ with proposal $\mathit{pro}$; if $\mathit{pro}=\bot$, then $\mathit{rla}(v,\mathit{id})$ is started without a proposal. If $\mathit{pro}\neq\bot$, then the server has proposed to $\mathit{rla}(v,\mathit{id})$.

8 $\bullet$ <$\mathit{rla}(v,\mathit{id})$.Stop>: stops
$\mathit{rla}(v,\mathit{id})$.

10 $\bullet$ <$\mathit{rla}(v,\mathit{id})$.Propose | Set(X) $\mathit{pro}$>: proposes $\mathit{pro}$ to $\mathit{rla}(v,\mathit{id})$.

12 Indications:

13 $\bullet$ <$\mathit{rla}(v,\mathit{id})$.Decide | Set(X) $\mathit{dec}$, Certificate $\omega$>: indicates that $\mathit{dec}$ is decided with the certificate $\omega$.

15 Rules:

16 1) No correct server $r\notin v$.members() invokes any request to
$\mathit{rla}(v,\mathit{id})$.

17 2) Every correct server invokes each request at most once.

18 3) If a correct server invokes <$\mathit{rla}(v,\mathit{id})$.Start | $\mathit{pro}\neq\bot$>, then the server does not invoke
<$\mathit{rla}(v,\mathit{id})$.Propose>.

19 4) No correct server invokes <$\mathit{rla}(v,\mathit{id})$.Stop> or
<$\mathit{rla}(v,\mathit{id})$.Propose> unless it has already invoked
<$\mathit{rla}(v,\mathit{id})$.Start>.

20 5) A correct server invokes <$\mathit{rla}(v,\mathit{id})$.Stop> before
halting.

21 6) If a correct server invokes <$\mathit{rla}(v,\mathit{id})$.Start | $\mathit{pro}\neq\bot$> or <$\mathit{rla}(v,\mathit{id})$.Propose | $\mathit{pro}$>, then (1) $\mathit{pro}=\\{x\\}$444The proposal contains a single element., and (2) valid($x,v$) = $\top$.

Listing 12: RLA - interface

If a (correct or faulty) process obtains (i.e., stores in its local memory) a
certificate $\omega$, where
$\mathtt{verify\\_output}(\mathit{dec},\mathit{rla}(v,\mathit{id}),\omega)=\top$,
for some set $\mathit{dec}$ of objects of type $\mathtt{X}$, then we say that
$\mathit{dec}$ is _committed_ by $\mathit{rla}(v,\mathit{id})$. Moreover,
$\mathit{dec}$ is committed at time $t$ if and only if the certificate
attainment happens at time $t^{\prime}\leq t$. Note that we assume that an
attainment of a certificate is irrevocable; hence, if $\mathit{dec}$ is
committed at time $t$, then $\mathit{dec}$ is committed at any time
$t^{\prime}\geq t$. Finally, we present the properties of an RLA instance.

⬇

1Reconfiguration Lattice Agreement:

2 instance $\mathit{rla}(v,\mathit{id})$, with $v$ is View and $\mathit{id}$
is Integer

4 Properties:

5 \- Integrity: No correct server $r\notin v$.members() receives any
indication from $\mathit{rla}(v,\mathit{id})$.

6 \- Decision Certification: If a correct server decides $\mathit{dec}$ with a
certificate $\omega$ from $\mathit{rla}(v,\mathit{id})$, then
verify_output($\mathit{dec}$, $\mathit{rla}(v,\mathit{id})$, $\omega$)
$=\top$.

7 \- Comparability: If $\mathit{dec}$ and $\mathit{dec}^{\prime}$ are
committed by $\mathit{rla}(v,\mathit{id})$, then either
$\mathit{dec}\subseteq\mathit{dec}^{\prime}$ or
$\mathit{dec}\supset\mathit{dec}^{\prime}$.

8 - Validity: If $\mathit{dec}$ is committed by $\mathit{rla}(v,\mathit{id})$,
$\mathit{dec}\neq\emptyset$, and, for every $x\in\mathit{dec}$, valid($x,v$) =
$\top$.

9 \- Decision Permission: If a set is committed by
$\mathit{rla}(v,\mathit{id})$, then at least $v$.plurality() of correct
members of $v$ have previously started $\mathit{rla}(v,\mathit{id})$.

10 \- Bounded Decisions: Let
$\mathit{DEC}=\\{\mathit{dec}\,|\,\mathit{dec}\text{ is committed by
}\mathit{rla}(v,\mathit{id})\\}$. Then, $|\mathit{DEC}|<\infty$.

11 \- Liveness: If all correct servers $r\in v$.members() start
$\mathit{rla}(v,\mathit{id})$, at least one correct server proposes to
$\mathit{rla}(v,\mathit{id})$ and no correct server stops
$\mathit{rla}(v,\mathit{id})$, then all correct servers $r\in v$.members()
eventually decide from $\mathit{rla}(v,\mathit{id})$.

Listing 13: RLA - properties

##### Implementation.

We now give an implementation of the $\mathit{rla}(v,\mathit{id})$ instance of
the RLA primitive. Recall that the failure model of
$\mathit{rla}(v,\mathit{id})$ assumes (at least) a quorum of correct members
of view $v$. Since $\mathit{rla}(v,\mathit{id})$ is associated with view $v$,
a correct server $r\in v.\mathtt{members()}$ discards all messages sent by
processes that are not members of $v$; for brevity, this check is omitted from
LABEL:lst:rla_proposer and LABEL:lst:rla_acceptor.

Moreover, we assume that there exists the reliable broadcast primitive that
allows processes to “reliably” broadcast a message $m$ to a fixed set of
processes; we write “$\mathtt{reliably}\text{ }\mathtt{broadcast}$ $m\text{
}\mathtt{to}\text{ }S$”, where $S$ is a set of processes. The reliable
broadcast primitive can be implemented in static systems
(cachin2011introduction, ), i.e., in systems in which correct processes never
halt. However, any implementation of the primitive in a static environment
implements the primitive in a dynamic system (in which correct processes might
halt) if we assume that the properties of the primitive need to be ensured
only if no correct process halts.

The presented implementation is highly inspired by the protocol given in
(di2020byzantine, ); the changes we introduce account for subtle differences
between RLA and BLA. For the presentational purposes, we distinguish two roles
of servers implementing $\mathit{rla}(v,\mathit{id})$: _proposer_ and
_acceptor_. However, the following implementation assumes that each server
takes _both_ roles.

⬇

1Reconfiguration Lattice Agreement:

2 instance $\mathit{rla}(v,\mathit{id})$, with $v$ is View and $\mathit{id}$
is Integer

4 Proposer Implementation:

5 upon <$\mathit{rla}(v,\mathit{id})$.Init>: // initialization of
$\mathit{rla}(v,\mathit{id})$ for the proposer

6 Set(X) $\mathit{proposed\\_value}=\bot$

7 Integer $\mathit{init\\_counter}=0$

8 Set(X) $\mathit{Proposed\\_Set}=\emptyset$

9 Set(Server) $\mathit{Ack\\_Set}=\emptyset$

10 Set(Message) $\omega=\emptyset$

11 Set(X) $\mathit{Safe\\_Set}=\emptyset$

12 Set(Message) $\mathit{Waiting\\_Msgs}=\emptyset$

13 String $\mathit{state}=$ "disclosing"

15 // Disclosure Phase

16 upon <$\mathit{rla}(v,\mathit{id})$.Start | Set(X) $\mathit{proposal}$>:

17 if $\mathit{proposal}\neq\bot$:

18 $\mathit{proposed\\_value}=\mathit{proposal}$

19 $\mathit{Safe\\_Set}=\mathit{Safe\\_Set}\cup\mathit{proposed\\_value}$

20
$\mathit{Proposed\\_Set}=\mathit{Proposed\\_Set}\cup\mathit{proposed\\_value}$

21 reliably broadcast $[$DISCLOSURE($v$, $\mathit{id}$),
$\mathit{proposed\\_value}]$ to $v$.members()

22 start processing protocol messages of $\mathit{rla}(v,\mathit{id})$

24 upon <$\mathit{rla}(v,\mathit{id})$.Propose | Set(X) $\mathit{proposal}$>:

25 if $\mathit{proposed\\_value}=\bot$:

26 $\mathit{proposed\\_value}=\mathit{proposal}$

27 $\mathit{Safe\\_Set}=\mathit{Safe\\_Set}\cup\mathit{proposed\\_value}$

28
$\mathit{Proposed\\_Set}=\mathit{Proposed\\_Set}\cup\mathit{proposed\\_value}$

29 reliably broadcast $[$DISCLOSURE($v$, $\mathit{id}$),
$\mathit{proposed\\_value}]$ to $v$.members()

31 upon <$\mathit{rla}(v,\mathit{id})$.Stop>:

32 stop processing protocol messages of $\mathit{rla}(v,\mathit{id})$

34 upon reliably deliver Message $m=[$DISCLOSURE($v$, $\mathit{id}$), Set(X)
$\mathit{proposal}]$:

35 if $|\mathit{proposal}|=1$ and for all
$x\in\mathit{proposal}:\mathtt{valid}(x,v)=\top$:

36 $\mathit{Safe\\_Set}=\mathit{Safe\\_Set}\cup\mathit{proposal}$

37 $\mathit{init\\_counter}=\mathit{init\\_counter}+1$

38 if $\mathit{state}=$ "disclosing":

39 if $\mathit{proposed\\_value}=\bot$:

40 $\mathit{proposed\\_value}=\mathit{proposal}$

41 reliably broadcast $[$DISCLOSURE($v$, $\mathit{id}$),
$\mathit{proposed\\_value}]$ to $v$.members()

42 $\mathit{Proposed\\_Set}=\mathit{Proposed\\_Set}\cup\mathit{proposal}$

44 // Deciding Phase

45 upon $\mathit{init\\_counter}\geq v$.quorum() and $\mathit{state}=$
"disclosing":

46 $\mathit{state}=$ "proposing"

47 broadcast $[$ACK_REQ($v$, $\mathit{id}$), $\mathit{Proposed\\_Set}]$ to
$v$.members()

49 upon receipt of Message $m$ such that $m=[$ACK_CON($v$, $\mathit{id}$),
Set(X) $\mathit{proposed}]$ or $m=[$NACK($v$, $\mathit{id}$), Set(X)
$\mathit{update}$, Set(X) $\mathit{proposed}]$:

50 $\mathit{Waiting\\_Msgs}=\mathit{Waiting\\_Msgs}\cup\\{m\\}$

52 upon exists Message $m\in\mathit{Waiting\\_Msgs}$ such that Safe($m$)
$=\top$ and $\mathit{state}=$ "proposing" and $m=[$ACK_CON($v$,
$\mathit{id}$), Set(X) $\mathit{proposed}]$ and
$\mathit{proposed}=\mathit{Proposed\\_Set}$:

53 $\mathit{Waiting\\_Msgs}=\mathit{Waiting\\_Msgs}\setminus\\{m\\}$

54 if $m$.sender $\notin\mathit{Ack\\_Set}$:

55 $\mathit{Ack\\_Set}=\mathit{Ack\\_Set}\cup\\{m$.sender$\\}$

56 $\omega=\omega\cup\\{m\\}$

58 upon exists Message $m\in\mathit{Waiting\\_Msgs}$ such that Safe($m$)
$=\top$ and $\mathit{state}=$ "proposing" and $m=[$NACK($v$, $\mathit{id}$),
Set(X) $\mathit{update}$, Set(X) $\mathit{proposed}]$ and
$\mathit{proposed}=\mathit{Proposed\\_Set}$:

59 $\mathit{Waiting\\_Msgs}=\mathit{Waiting\\_Msgs}\setminus\\{m\\}$

60 if $\mathit{update}\cup\mathit{Proposed\\_Set}\neq\mathit{Proposed\\_Set}$:

61 $\mathit{Proposed\\_Set}=\mathit{Proposed\\_Set}\cup\mathit{update}$

62 $\mathit{Ack\\_Set}=\emptyset$; $\omega=\emptyset$

63 broadcast $[$ACK_REQ($v$, $\mathit{id}$), $\mathit{Proposed\\_Set}]$ to
$v$.members()

65 upon $|\mathit{Ack\\_Set}|\geq v$.quorum() and $\mathit{state}=$
"proposing":

66 $\mathit{state}=$ "decided"

67 trigger <$\mathit{rla}(v,\mathit{id})$.Decide | $\mathit{Proposed\\_Set}$, $\omega$>

69 function Safe(Message $m$):

70 if $m=[$ACK_CON($v$, $\mathit{id}$), Set(X) $\mathit{proposed}]$:

71 return $\mathit{proposed}\subseteq\mathit{Safe\\_Set}$

72 if $m=[$NACK($v$, $\mathit{id}$), Set(X) $\mathit{update}$, Set(X)
$\mathit{proposed}]$:

73 return $\mathit{update}\subseteq\mathit{Safe\\_Set}$

74 return $\bot$

Listing 14: RLA - proposer implementation

Next, we provide the acceptor implementation.

⬇

1Reconfiguration Lattice Agreement:

2 instance $\mathit{rla}(v,\mathit{id})$, with $v$ is View and $\mathit{id}$
is Integer

4 Acceptor Implementation:

5 upon <$\mathit{rla}(v,\mathit{id})$.Init>: // initialization of
$\mathit{rla}(v,\mathit{id})$ for the acceptor

6 Set(X) $\mathit{Accepted\\_Set}=\emptyset$

7 Set(Message) $\mathit{Waiting\\_Msgs}=\emptyset$

8 Set(X) $\mathit{Safe\\_Set}$ // reference to $\mathit{Safe\\_Set}$ in the
corresponding proposer

10 upon receipt of Message $m$ such that $m=[$ACK_REQ($v$, $\mathit{id}$),
Set(X) $\mathit{proposal}]$:

11 $\mathit{Waiting\\_Msgs}=\mathit{Waiting\\_Msgs}\cup\\{m\\}$

13 upon exists Message $m\in\mathit{Waiting\\_Msgs}$ such that Safe($m$)
$=\top$ and $m=[$ACK_REQ($v$, $\mathit{id}$), Set(X) $\mathit{proposal}]$ and
$\mathit{proposal}\neq\emptyset$:

14 $\mathit{Waiting\\_Msgs}=\mathit{Waiting\\_Msgs}\setminus\\{m\\}$

15 if $\mathit{Accepted\\_Set}\subseteq\mathit{proposal}$:

16 $\mathit{Accepted\\_Set}=\mathit{proposal}$

17 send $[$ACK_CON($v$, $\mathit{id}$), $\mathit{Accepted\\_Set}]$ to
$m$.sender

18 else:

19 send $[$NACK($v$, $\mathit{id}$), $\mathit{Accepted\\_Set}$,
$\mathit{proposal}]$ to $m$.sender

20 $\mathit{Accepted\\_Set}=\mathit{Accepted\\_Set}\cup\mathit{proposal}$

22 function Safe(Message $m$):

23 if $m=[$ACK_REQ($v$, $\mathit{id}$), Set(X) $\mathit{proposal}]$:

24 return $\mathit{proposal}\subseteq\mathit{Safe\\_Set}$

25 return $\bot$

Listing 15: RLA - acceptor implementation

In order to conclude the implementation of $\mathit{rla}(v,\mathit{id})$, we
need to define when
$\mathtt{verify\\_output}(\mathit{dec},\mathit{rla}(v,\mathit{id}),\omega)=\top$.

⬇

1function verify_output(Set(X) $\mathit{dec}$, Distributed_Primitive_Instance
$\mathit{rla}(v,\mathit{id})$, Certificate $\omega$):

2 if $\omega$ is not Set(Message): return $\bot$

4 Integer $\mathit{senders\\_num}=|\\{r\,|\,m\in\omega$ and $m$.sender
$=r\text{ and }r\in v\text{.members()}\\}|$

5 if $\mathit{senders\\_num}<$ $v$.quorum(): return $\bot$

7 return for every Message $m\in\omega$, $m=[$ACK_CON($v$, $\mathit{id}$),
$\mathit{dec}]$

Listing 16: The $\mathtt{verify\\_output}$ function for
$\mathit{rla}(v,\mathit{id})$

Proof of correctness. We are now ready to prove the correctness of the
implementation given in LABEL:lst:rla_proposer and LABEL:lst:rla_acceptor. We
start by proving the safety properties of $\mathit{rla}(v,\mathit{id})$.

First, we prove the integrity property.

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

Algorithm given in LABEL:lst:rla_proposer and LABEL:lst:rla_acceptor satisfies
integrity.

###### Proof.

Since a server $r\notin v.\mathtt{members()}$ never starts
$\mathit{rla}(v,\mathit{id})$, it never starts processing protocol messages of
$\mathit{rla}(v,\mathit{id})$ (i.e., $r$ never executes line 22 of
LABEL:lst:rla_proposer). Hence, the rule at line 65 of LABEL:lst:rla_proposer
is never active at server $r$. Thus, $r$ never decides from
$\mathit{rla}(v,\mathit{id})$ and the theorem holds. ∎

Next, we prove decision certification.

###### Theorem 2 (Decision Certification).

Algorithm given in LABEL:lst:rla_proposer and LABEL:lst:rla_acceptor satisfies
decision certification.

###### Proof.

Let a correct server $r$ decide $\mathit{dec}$ with a certificate $\omega$. We
know that $\omega$ is a set of messages (by line 10 of LABEL:lst:rla_proposer)
and that the number of distinct senders “contained” in $\omega$ is greater
than or equal to $v.\mathtt{quorum()}$ (by line 65 of LABEL:lst:rla_proposer).
Moreover, all messages that belong to $\omega$ are for
$\mathit{Proposed\\_Set}=\mathit{dec}$ due to the check at line 52 of
LABEL:lst:rla_proposer and due to the “flush” of the $\mathit{Ack\\_Set}$
variable (at line 62 of LABEL:lst:rla_proposer) once the value of
$\mathit{Proposed\\_Set}$ is updated. ∎

We now prove comparability.

###### Theorem 3 (Comparability).

Algorithm given in LABEL:lst:rla_proposer and LABEL:lst:rla_acceptor satisfies
comparability.

###### Proof.

Let $\mathit{dec}_{1}$ and let $\mathit{dec}_{2}$ be committed by
$\mathit{rla}(v,\mathit{id})$. Hence, at least $v.\mathtt{quorum()}$ acceptors
have sent the $\mathtt{ACK\\_CON}(v,\mathit{id})$ message for
$\mathit{dec}_{1}$. Similarly, $v.\mathtt{quorum()}$ acceptors have sent the
$\mathtt{ACK\\_CON}(v,\mathit{id})$ message for $\mathit{dec}_{2}$. Hence,
there exists at least a single correct acceptor that has sent both messages
(due to the quorum intersection and the fact that at least
$v.\mathtt{quorum()}$ members of $v$ are correct); let that acceptor be $k$.

Without loss of generality, we assume that $k$ has first sent the
$\mathtt{ACK\\_CON}(v,\mathit{id})$ message for $\mathit{dec}_{1}$. At the
moment $t$ of sending the $\mathtt{ACK\\_CON}(v,\mathit{id})$ message for
$\mathit{dec}_{1}$, we have that $\mathit{Accepted\\_Set}=\mathit{dec}_{1}$ at
server $k$ (line 16 of LABEL:lst:rla_acceptor). On the other hand, at the
moment $t^{\prime}\geq t$ of sending the $\mathtt{ACK\\_CON}(v,\mathit{id})$
message for $\mathit{dec}_{2}$, we have that
$\mathit{Accepted\\_Set}=\mathit{dec}_{2}$ at $k$ (line 16 of
LABEL:lst:rla_acceptor). Hence, we investigate how $\mathit{Accepted\\_Set}$
changes after time $t$ at acceptor $k$.

Initially, at time $t$, $\mathit{Accepted\\_Set}=\mathit{dec}_{1}$. Hence, we
set the induction hypothesis
$\mathit{dec}_{1}\subseteq\mathit{Accepted\\_Set}$. We investigate all
possibilities for $k$ to modify its $\mathit{Accepted\\_Set}$ variable:

  * •

line 16 of LABEL:lst:rla_acceptor: The hypothesis is preserved because of the
check at line 15 of LABEL:lst:rla_acceptor.

  * •

line 20 of LABEL:lst:rla_acceptor: The hypothesis is preserved because of the
fact that the new value of $\mathit{Accepted\\_Set}$ contains the old value of
$\mathit{Accepted\\_Set}$ and $\mathit{dec}_{1}$ is included in the old value
of $\mathit{Accepted\\_Set}$.

Therefore, all values of the $\mathit{Accepted\\_Set}$ variable at acceptor
$k$ after time $t$ contain $\mathit{dec}_{1}$. Thus, we have that
$\mathit{dec}_{1}\subseteq\mathit{dec}_{2}$, which concludes the theorem. ∎

The following lemma proves that, if $x\in\mathit{Safe\\_Set}$ at a correct
server, then $\mathtt{valid}(x,v)=\top$.

###### Lemma 0.

Let $r$ be a correct server. If $x\in\mathit{Safe\\_Set}$ at $r$, then
$\mathtt{valid}(x,v)=\top$.

###### Proof.

We examine all possible ways for a correct server to modify its
$\mathit{Safe\\_Set}$ variable:

  * •

line 19 of LABEL:lst:rla_proposer: By rule 6 of $\mathit{rla}(v,\mathit{id})$
(line 21 of LABEL:lst:rla_interface), a single element $x$ is added to
$\mathit{Safe\\_Set}$ and $\mathtt{valid}(x,v)=\top$.

  * •

line 27 of LABEL:lst:rla_proposer: As in the previous case, a single element
$x$ is added to $\mathit{Safe\\_Set}$ and $\mathtt{valid}(x,v)=\top$ (by rule
6 of $\mathit{rla}(v,\mathit{id})$).

  * •

line 36 of LABEL:lst:rla_proposer: A single element $x$ is added to
$\mathit{Safe\\_Set}$ and $\mathtt{valid}(x,v)=\top$ (by the check at line 35
of LABEL:lst:rla_proposer).

The fact that, at all times, for every $x\in\mathit{Safe\\_Set}$,
$\mathtt{valid}(x,v)=\top$ concludes the theorem. ∎

The following theorem proves validity.

###### Theorem 5 (Validity).

Algorithm given in LABEL:lst:rla_proposer and LABEL:lst:rla_acceptor satisfies
validity.

###### Proof.

Let $\mathit{dec}$ be committed by $\mathit{rla}(v,\mathit{id})$. Since no
correct acceptor ever sends the
$[\mathtt{ACK\\_CON}(v,\mathit{id}),\emptyset]$ message (due to the check at
line 13 of LABEL:lst:rla_acceptor), $\mathit{dec}\neq\emptyset$.

Since $\mathit{dec}$ is committed by $\mathit{rla}(v,\mathit{id})$, there
exists a correct acceptor $k\in v.\mathtt{members}()$ that has sent the
$\mathtt{ACK\\_CON}(v,\mathit{id})$ message for $\mathit{dec}$. At that time,
we know that $\mathit{dec}\subseteq\mathit{Safe\\_Set}$ at server $k$ (by line
13 of LABEL:lst:rla_acceptor). Therefore, the theorem conclusion follows from
Lemma 4. ∎

The next safety property we have to prove is the bounded decisions property.
In order to do so, we first prove that
$\mathit{Accepted\\_Set}\subseteq\mathit{Safe\\_Set}$ at a correct server at
all times.

###### Lemma 0.

At all times, $\mathit{Accepted\\_Set}\subseteq\mathit{Safe\\_Set}$ at a
correct acceptor.

###### Proof.

Initially, $\mathit{Accepted\\_Set}=\mathit{Safe\\_Set}=\emptyset$. Thus,
initially the invariant holds.

We now introduce the induction hypothesis
$\mathit{Accepted\\_Set}\subseteq\mathit{Safe\\_Set}$. Let us investigate all
places at which the $\mathit{Accepted\\_Set}$ variable or the
$\mathit{Safe\\_Set}$ variable is changed:

  * •

line 19 of LABEL:lst:rla_proposer: Holds because of the induction hypothesis.

  * •

line 27 of LABEL:lst:rla_proposer: Holds because of the induction hypothesis.

  * •

line 36 of LABEL:lst:rla_proposer: Holds because of the induction hypothesis.

  * •

line 16 of LABEL:lst:rla_acceptor: Holds because
$\mathit{proposal}\subseteq\mathit{Safe\\_Set}$ (because of the
$\mathtt{Safe}()$ function; line 24 of LABEL:lst:rla_acceptor).

  * •

line 20 of LABEL:lst:rla_acceptor: Holds because of the induction hypothesis
and the fact that $\mathit{proposal}\subseteq\mathit{Safe\\_Set}$ (because of
the $\mathtt{Safe}()$ function).

Since the induction hypothesis is always preserved, the lemma holds. ∎

We are now ready to prove the bounded decisions property.

###### Theorem 7 (Bounded Decisions).

Algorithm given in LABEL:lst:rla_proposer and LABEL:lst:rla_acceptor satisfies
bounded decisions.

###### Proof.

Let $\mathit{dec}$ be committed by $\mathit{rla}(v,\mathit{id})$. We have that
$\mathit{Accepted\\_Set}=\mathit{dec}$ at some correct server $r$ (line 16 of
LABEL:lst:rla_acceptor). By Lemma 6, we know that
$\mathit{dec}\subseteq\mathit{Safe\\_Set}$ at server $r$ at that time.

Let
$\mathit{proposals}=\\{\mathit{proposal}\,|\,\mathit{proposal}\subseteq\mathit{Safe\\_Set}\text{
at a correct server at some time and }|\mathit{proposal}|=1\\}$. We know that
$|\mathit{proposals}|\leq|v.\mathtt{members}()|$ due to the fact that each
$\mathit{proposal}\in\mathit{proposals}$ is broadcast using the reliable
broadcast primitive. Now, let
$\mathit{SAFE\\_SET}=\bigcup\limits_{\mathit{proposal}\in\mathit{proposals}}\mathit{proposal}$.
Hence, at any point in time, we have that
$\mathit{Safe\\_Set}\subseteq\mathit{SAFE\\_SET}$ at a correct server. That
means that $\mathit{dec}\subseteq\mathit{SAFE\\_SET}$, for any committed
$\mathit{dec}$. Since $\mathit{SAFE\\_SET}$ is finite, it has finitely many
subsets. Therefore, the theorem holds. ∎

The last safety property we need to prove is decision permission.

###### Theorem 8 (Decision Permission).

Algorithm given in LABEL:lst:rla_proposer and LABEL:lst:rla_acceptor satisfies
decision permission.

###### Proof.

Assume that $\mathit{dec}$ is committed by $\mathit{rla}(v,\mathit{id})$.
Hence, at least $v.\mathtt{plurality()}$ of correct members of $v$ have sent
the $[\mathtt{ACK\\_CON}(v,\mathit{id}),\mathit{dec}]$ message (by
LABEL:lst:verify_output_rla). Since a correct server does not send any
$\mathtt{ACK\\_CON}(v,\mathit{id})$ message before starting
$\mathit{rla}(v,\mathit{id})$ (ensured by the fact that a correct server
starts processing protocol messages of $\mathit{rla}(v,\mathit{id})$ only once
it starts $\mathit{rla}(v,\mathit{id})$; line 22 of LABEL:lst:rla_proposer),
the decision permission property is ensured. ∎

Lastly, we prove liveness. Recall that liveness is guaranteed only if all
correct servers start $\mathit{rla}(v,\mathit{id})$, a correct server proposes
to $\mathit{rla}(v,\mathit{id})$ and no correct server stops
$\mathit{rla}(v,\mathit{id})$. We implicitly assume that these hold in the
following lemmas.

First, we show that $\mathit{Safe\\_Set}$ variables of correct servers are
eventually identical. This is ensured because of the properties of the
reliable broadcast primitive.

###### Lemma 0.

Eventually, $\mathit{Safe\\_Set}_{r}=\mathit{Safe\\_Set}_{r^{\prime}}$, where
$r$ and $r^{\prime}$ are correct servers, $\mathit{Safe\\_Set}_{r}$ denotes
the value of $\mathit{Safe\\_Set}$ at server $r$ and
$\mathit{Safe\\_Set}_{r^{\prime}}$ denotes the value of $\mathit{Safe\\_Set}$
at server $r^{\prime}$.

###### Proof.

A correct server updates its $\mathit{Safe\\_Set}$ variable at following
places in LABEL:lst:rla_proposer:

  * •

line 19: The update is reliably broadcast at line 21 of
LABEL:lst:rla_proposer. By rule 6 of $\mathit{rla}(v,\mathit{id})$, we know
that $\mathit{proposed\\_value}=\\{x\\}$ and $\mathtt{valid}(x,v)=\top$.
Hence, whenever another correct server receives the
$\mathtt{DISCLOSURE}(v,\mathit{id})$ message for $\mathit{proposed\\_value}$,
the check at line 35 of LABEL:lst:rla_proposer passes and
$\mathit{proposed\\_value}$ is included in $\mathit{Safe\\_Set}$.

  * •

line 27: The update is reliably broadcast at line 29 of
LABEL:lst:rla_proposer. By rule 6 of $\mathit{rla}(v,\mathit{id})$, we know
that $\mathit{proposed\\_value}=\\{x\\}$ and $\mathtt{valid}(x,v)=\top$.
Hence, whenever another correct server receives the
$\mathtt{DISCLOSURE}(v,\mathit{id})$ message for $\mathit{proposed\\_value}$,
the check at line 35 of LABEL:lst:rla_proposer passes and
$\mathit{proposed\\_value}$ is included in $\mathit{Safe\\_Set}$.

  * •

line 36: The update is reliably delivered (at line 34 of
LABEL:lst:rla_proposer). Due to the check at line 35 of
LABEL:lst:rla_proposer, we know that $\mathit{proposal}=\\{x\\}$ and
$\mathtt{valid}(x,v)=\top$. Hence, whenever another correct server receives
the $\mathtt{DISCLOSURE}(v,\mathit{id})$ message for $\mathit{proposal}$
(which happens because of the totality and agreement properties of the
reliable broadcast primitive), the check at line 35 of LABEL:lst:rla_proposer
passes and $\mathit{proposal}$ is included in $\mathit{Safe\\_Set}$.

Thus, every update to $\mathit{Safe\\_Set}$ of a correct server eventually
reaches every other correct server due to the properties of the reliable
broadcast primitive. The lemma holds. ∎

Next, we prove that $\mathit{Proposed\\_Set}\subseteq\mathit{Safe\\_Set}$ at a
correct server.

###### Lemma 0.

At all times, $\mathit{Proposed\\_Set}\subseteq\mathit{Safe\\_Set}$ at a
correct proposer.

###### Proof.

Initially, $\mathit{Proposed\\_Set}=\mathit{Safe\\_Set}=\emptyset$. Thus,
initially the invariant holds.

We now introduce the induction hypothesis
$\mathit{Proposed\\_Set}\subseteq\mathit{Safe\\_Set}$. Let us investigate all
places at which either $\mathit{Proposed\\_Set}$ or $\mathit{Safe\\_Set}$
variables are changed in LABEL:lst:rla_proposer:

  * •

line 19: Holds because of the induction hypothesis.

  * •

line 20: Holds because of the induction hypothesis and the fact that
$\mathit{proposed\\_value}\subseteq\mathit{Safe\\_Set}$.

  * •

line 27: Holds because of the induction hypothesis.

  * •

line 28: Holds because of the induction hypothesis and the fact that
$\mathit{proposed\\_value}\subseteq\mathit{Safe\\_Set}$.

  * •

line 36: Holds because of the induction hypothesis.

  * •

line 42: Holds because of the induction hypothesis and the fact that
$\mathit{proposal}\subseteq\mathit{Safe\\_Set}$.

  * •

line 61: Holds because of the induction hypothesis and the fact that
$\mathit{update}\subseteq\mathit{Safe\\_Set}$ (because of the
$\mathtt{Safe}()$ function; line 73 of LABEL:lst:rla_proposer).

Since the induction hypothesis is always preserved, the lemma holds. ∎

Now, we show that every message sent by a correct server is eventually “safe”
at all other correct servers.

###### Lemma 0.

Any $\mathtt{ACK\\_CON}(v,\mathit{id})$, $\mathtt{NACK}(v,\mathit{id})$ or
$\mathtt{ACK\\_REQ}(v,\mathit{id})$ message sent by a correct server is
eventually safe (i.e., the $\mathtt{Safe}()$ function returns $\top$) for any
other correct server.

###### Proof.

Let us first consider a message
$m=[\mathtt{ACK\\_CON}(v,\mathit{id}),\mathit{set}]$ sent by a correct server
$r$ to a correct server $r^{\prime}$. Since $r$ has previously received the
$\mathtt{ACK\\_REQ}$ message for $\mathit{set}$ from $r^{\prime}$, we know
that $\mathit{Proposed\\_Set}=\mathit{set}$ at server $r^{\prime}$ at the
moment of broadcasting this message (line 47 or line 63 of
LABEL:lst:rla_proposer). Hence, $\mathit{set}\subseteq\mathit{Safe\\_Set}$ at
server $r^{\prime}$ (by Lemma 10), which ensures that the lemma holds in this
case.

Now, let $m=[\mathtt{NACK}(v,\mathit{id}),\mathit{set},\mathit{proposed}]$ be
sent by a correct server $r$. At the moment of sending $m$, we know that
$\mathit{Accepted\\_Set}=\mathit{set}$ at server $r$ (by line 19 of
LABEL:lst:rla_acceptor). By Lemma 6, we know that
$\mathit{set}\subseteq\mathit{Safe\\_Set}$ at server $r$. Eventually, by Lemma
9, we know that $\mathit{set}\subseteq\mathit{Safe\\_Set}$ at any other
correct server. Hence, $m$ eventually becomes safe.

Finally, let
$m=[\mathtt{ACK\\_REQ}(v,\mathit{id}),\mathit{set},\mathit{number}]$ be
broadcast by a correct server $r$. We know that
$\mathit{Proposed\\_Set}=\mathit{set}$ (by lines 47 and 63 of
LABEL:lst:rla_proposer). By Lemma 10, we know that
$\mathit{set}\subseteq\mathit{Safe\\_Set}$ at server $r$. Eventually, by Lemma
9, we know that $\mathit{set}\subseteq\mathit{Safe\\_Set}$ at any other
correct server. Hence, $m$ eventually becomes safe, which concludes the lemma.
∎

Now, we show that a correct server modifies its proposal at most
$\lfloor\frac{n-1}{3}\rfloor$ times, where $n=|v.\mathtt{members}()|$.

###### Lemma 0.

A correct server $r$ refines its proposal (i.e., executes line 63 of
LABEL:lst:rla_proposer) at most $\lfloor\frac{n-1}{3}\rfloor$ times, where
$n=|v.\mathtt{members}()|$.

###### Proof.

The first proposal of server $r$ includes proposals from (at least)
$v.\mathtt{quorum()}$ servers (lines 45 and 47 of LABEL:lst:rla_proposer).
Since $|\mathit{Safe\\_Set}|$ at $r$ is at most $n$ (due to rule 6 and the
check at line 35 of LABEL:lst:rla_proposer) and
$n-v.\mathtt{quorum}()=\lfloor\frac{n-1}{3}\rfloor$, $r$ can execute line 63
of LABEL:lst:rla_proposer at most $\lfloor\frac{n-1}{3}\rfloor$ times. ∎

The next lemma shows that a correct proposer never sends an
$\mathtt{ACK\\_REQ}$ message for $\emptyset$.

###### Lemma 0.

Let a correct server $r$ send the
$[\mathtt{ACK\\_REQ}(v,\mathit{id}),\mathit{proposal}]$ message. Then,
$\mathit{proposal}\neq\emptyset$.

###### Proof.

The first $\mathtt{ACK\\_REQ}$ message is sent for $\mathit{proposal}$ at line
47 of LABEL:lst:rla_proposer, where
$\mathit{proposal}=\mathit{Proposed\\_Set}$. By the check at line 35 of
LABEL:lst:rla_proposer, we know that $\mathit{Proposed\\_Set}\neq\emptyset$.

After the first sent $\mathtt{ACK\\_REQ}$, other $\mathtt{ACK\\_REQ}$ messages
are sent at line 63 of LABEL:lst:rla_proposer for $\mathit{Proposed\\_Set}$.
Since $\mathit{Proposed\\_Set}$ is never updated to $\emptyset$ and elements
of $\mathit{Proposed\\_Set}$ are never removed, we conclude the lemma. ∎

The next lemma shows that, if a correct proposer stops refining its proposal,
then the proposer eventually decides.

###### Lemma 0.

If there exists a time $t$ after which a correct server $r$, which is in the
$\mathtt{proposing}$ state, does not execute line 63 of
LABEL:lst:rla_proposer, then $r$ eventually decides.

###### Proof.

Let $\mathit{proposal}$ be the last proposal for which $r$ sends an
$\mathtt{ACK\\_REQ}(v,\mathit{id})$ message in an execution. Since $r$ does
not execute line 63 of LABEL:lst:rla_proposer after this message has been
sent, either $r$ does not receive any $\mathtt{NACK}(v,\mathit{id})$ message
or no received $\mathtt{NACK}(v,\mathit{id})$ message allows $r$ to pass the
check at line 60 of LABEL:lst:rla_proposer. Since $r$ is correct, its
$[\mathtt{ACK\\_REQ}(v,\mathit{id}),\mathit{proposal}]$ message eventually
reaches every correct acceptor (by lemmas 11 and 13). Then, each correct
acceptor sends the $[\mathtt{ACK\\_CON}(v,\mathit{id}),\mathit{proposal}]$
message to $r$. By contradiction, suppose that a correct acceptor sends
$[\mathtt{NACK}(v,\mathit{id}),\mathit{update},\mathit{proposed}]$ to $r$,
then:

  * •

$\mathit{update}\not\subseteq\mathit{proposal}$ (by line 15 of
LABEL:lst:rla_acceptor), and

  * •

$m$ would eventually be “safe” at $r$ (due to Lemma 11) and, since $r$ does
not update its $\mathit{Proposed\\_Set}$ variable, line 58 of
LABEL:lst:rla_proposer eventually passes at $r$, and

  * •

the check at line 60 of LABEL:lst:rla_proposer passes at $r$ since
$\mathit{update}\not\subseteq\mathit{proposal}$.

Therefore, $r$ would refine its proposal, which contradicts the fact that $r$
never refines $\mathit{proposal}$.

Hence, once $r$ receives $\mathtt{ACK\\_CON}(v,\mathit{id})$ messages from all
correct servers, these messages are safe for $r$ (by Lemma 11) and, since
$\mathit{Proposed\\_Set}$ at server $r$ does not change, the rule at line 65
of LABEL:lst:rla_proposer is active, which implies that $r$ decides. ∎

Finally, we prove the liveness property of $\mathit{rla}(v,\mathit{id})$.

###### Theorem 15 (Liveness).

Algorithm given in LABEL:lst:rla_proposer and LABEL:lst:rla_acceptor satisfies
liveness.

###### Proof.

Let a correct server $\mathit{proposer}$ propose to
$\mathit{rla}(v,\mathit{id})$. This means that every correct server $r$
eventually obtains proposals of $v.\mathtt{quorum()}$ servers (line 45 of
LABEL:lst:rla_proposer) and sends an $\mathtt{ACK\\_REQ}$ message (line 47 of
LABEL:lst:rla_proposer). By Lemma 12, $r$ refines its proposal only finitely
many times. Once $r$ stops refining its proposal, $r$ decides (by Lemma 14). ∎

###  4.2. View Generator - Implementation

Now that we have introduced RLA, we are ready to present our implementation of
$\mathit{vg}(v)$. Recall that the failure model of $\mathit{vg}(v)$ assumes
(at least) a quorum of correct members of view $v$.

Our implementation of $\mathit{vg}(v)$ consists of two RLA instances:
$\mathit{rla}(v,1)$ and $\mathit{rla}(v,2)$. We provide the descriptions of
both instances below:

  1. (1)

$\mathit{rla}(v,1)$ description: Sets of tuples
$(v^{\prime},\mathit{set}^{\prime},\epsilon^{\prime})$, where $v^{\prime}$ is
a view, $\mathit{set}^{\prime}$ is a set of views and $\epsilon^{\prime}$ is
an evidence, are processed by $\mathit{rla}(v,1)$. Recall that such tuples are
given as inputs to $\mathit{vg}(v)$.

  2. (2)

$\mathit{rla}(v,2)$ description: Sets of tuples
$(\mathit{set}^{\prime},\epsilon^{\prime})$ are processed by
$\mathit{rla}(v,2)$, where $\mathit{set}^{\prime}$ is a set of views and
$\epsilon^{\prime}$ is an evidence (see LABEL:lst:set_proof).

⬇

1Set, Evidence:

2 instance $(\mathit{set}^{\prime},\epsilon^{\prime})$, with
$\mathit{set}^{\prime}$ is Set(View) and $\epsilon^{\prime}$ is Evidence

4 function construct(Set(View, Set, Evidence) $\mathit{set}$):

5 Set(Set(View))
$\mathit{SET}=\\{\mathit{set}^{*}\,|\,(v^{*},\mathit{set}^{*},\epsilon^{*})\in\mathit{set}\text{
and }\mathit{set}^{*}\neq\emptyset\\}$

6 Set(View)
$\mathit{VIEW}=\\{v^{*}\,|\,(v^{*},\mathit{set}^{*},\epsilon^{*})\in\mathit{set}\text{
and }\mathit{set}^{*}=\emptyset\\}$

7 Set(View) $\mathit{result\\_set}=\bot$

9 if $|\mathit{VIEW}|=0$: // no ‘‘stand-alone’’ views

10 $\mathit{result\\_set}=$ max_cardinality555We assume that the
$\mathtt{max\\_cardinality(\mathit{set})}$ deterministic function, where
$\mathit{set}$ is a set of sets, returns the set with the greatest cardinality
that belongs to $\mathit{set}$; if there are multiple sets that satisfy the
condition, then any such set is returned.($\mathit{SET}$) // get the set with
the greatest cardinality

11 else:

12 Set(View) $\mathit{greatest\\_set}=$ max_cardinality($\mathit{SET}$) // get
the set with the greatest cardinality

13 View $\mathit{greatest\\_view}=\emptyset$

14 if $\mathit{greatest\\_set}\neq\bot$:

15 $\mathit{greatest\\_view}=$ max_cardinality($\mathit{greatest\\_set}$) //
get the view with the greatest cardinality666Recall that a view is a set of
changes.

16 View $\mathit{union\\_view}=\bigcup\limits_{v^{*}\in\mathit{VIEW}}v^{*}$

17
$\mathit{result\\_set}=\\{\mathit{greatest\\_view}\cup\mathit{union\\_view}\\}$

18 return $\mathit{result\\_set}$

20 // we need to define the $\mathtt{valid}$ function

21 function valid(Set, Evidence $(\mathit{set}^{\prime},\epsilon^{\prime})$,
View $v$):

22 if does not exist Set(View, Set, Evidence) $\mathit{set}$ such that
verify_output($\mathit{set}$, $\mathit{rla}(v,1)$, $\epsilon^{\prime}$)
$=\top$:

23 return $\bot$

24 return construct($\mathit{set}$) $=\mathit{set}^{\prime}$

Listing 17: (Set, Evidence) tuple

Finally, we give our implementation of $\mathit{vg}(v)$.

⬇

1View Generator:

2 instance $\mathit{vg}(v)$, with $v$ is View

4 Implementation:

5 upon <$\mathit{vg}(v)$.Init>: // initialization of $\mathit{vg}(v)$

6 Bool $\mathit{started1}=\bot$

7 Bool $\mathit{started2}=\bot$

9 upon <$\mathit{vg}(v)$.Start | View, Set, Evidence $(v^{\prime},\mathit{set}^{\prime},\epsilon^{\prime})$>:

10 $\mathit{started1}=\top$

11 if $(v^{\prime},\mathit{set}^{\prime},\epsilon^{\prime})\neq\bot$:

12 trigger <$\mathit{rla}(v,1)$.Start | $\\{(v^{\prime},\mathit{set}^{\prime},\epsilon^{\prime})\\}$>

13 else:

14 trigger <$\mathit{rla}(v,1)$.Start | $\bot$>

16 upon <$\mathit{vg}(v)$.Propose | View, Set, Evidence $(v^{\prime},\mathit{set}^{\prime},\epsilon^{\prime})$>:

17 trigger <$\mathit{rla}(v,1)$.Propose | $\\{(v^{\prime},\mathit{set}^{\prime},\epsilon^{\prime})\\}$>

19 upon <$\mathit{rla}(v,1)$.Decide | Set(View, Set, Evidence) $\mathit{dec}$, Certificate $\omega$>:

20 Set(View) $\mathit{proposal}=$ construct($\mathit{dec}$) // the function
from LABEL:lst:set_proof

21 $\mathit{started2}=\top$

22 trigger <$\mathit{rla}(v,2)$.Start | $\\{(\mathit{proposal},\omega)\\}$>

24 upon <$\mathit{rla}(v,2)$.Decide | Set(Set, Evidence) $\mathit{dec}$, Certificate $\omega$>:

25 Set(Set(View))
$\mathit{SET}=\\{\mathit{set}^{*}\,|\,(\mathit{set}^{*},\epsilon^{*})\in\mathit{dec}\\}$

26 trigger <$\mathit{vg}(v)$.Decide | $\bigcup\limits_{\mathit{set}^{*}\in\mathit{SET}}\mathit{set}^{*}$, $\omega$>

28 upon <$\mathit{vg}(v)$.Stop>:

29 if $\mathit{started1}=\top$:

30 trigger <$\mathit{rla}(v,1)$.Stop>

31 if $\mathit{started2}=\top$:

32 trigger <$\mathit{rla}(v,2)$.Stop>

Listing 18: View generator - implementation

In order to conclude the implementation of $\mathit{vg}(v)$, we need to define
when
$\mathtt{verify\\_output}(\mathit{set}_{\mathit{res}},\mathit{vg}(v),\omega)=\top$.

⬇

1function verify_output(Set(View) $\mathit{set}_{\mathit{res}}$,
Distributed_Primitive_Instance $\mathit{vg}(v)$, Certificate $\omega$):

2 if $\omega$ is not Set(Message): return $\bot$

4 if does not exist Set(Set, Evidence) $\mathit{set}$ such that
verify_output($\mathit{set}$, $\mathit{rla}(v,2)$, $\omega$) $=\top$:

5 return $\bot$

7 Set(Set(View))
$\mathit{SET}=\\{\mathit{set}^{*}\,|\,(\mathit{set}^{*},\epsilon^{*})\in\mathit{set}\\}$

8 return
$\mathit{set}_{\mathit{res}}=\bigcup\limits_{\mathit{set}^{*}\in\mathit{SET}}\mathit{set}^{*}$

Listing 19: The $\mathtt{verify\\_output}$ function for $\mathit{vg}(v)$

Proof of correctness. Finally, we prove the correctness of $\mathit{vg}(v)$.
We start by proving the integrity property.

###### Theorem 16 (Integrity).

Algorithm given in LABEL:lst:view_generator_implementation satisfies
integrity.

###### Proof.

By integrity of $\mathit{rla}(v,2)$, a correct server $r\notin
v.\mathtt{members}()$ never decides from $\mathit{rla}(v,2)$. Hence, the rule
at line 24 of LABEL:lst:view_generator_implementation is never active at
server $r$, which means that $r$ never decides from $\mathit{vg}(v)$.
Therefore, integrity is satisfied. ∎

Next, we prove the comparability property.

###### Theorem 17 (Comparability).

Algorithm given in LABEL:lst:view_generator_implementation satisfies
comparability.

###### Proof.

Let $\mathit{set}_{1}$ and $\mathit{set}_{2}$ be committed by
$\mathit{vg}(v)$. Hence, a set $\mathit{set}_{1}^{*}$, where (1)
$\mathit{set}_{1}^{*}$ is a set of tuples of the $\mathtt{Set,Evidence}$ type,
and (2)
$\mathit{set}_{1}=\bigcup\limits_{(\mathit{set}^{*},\epsilon^{*})\in\mathit{set}_{1}^{*}}\mathit{set}^{*}$,
is committed by $\mathit{rla}(v,2)$ (by LABEL:lst:verify_output_vg).
Similarly, a set $\mathit{set}_{2}^{*}$, where (1) $\mathit{set}_{2}^{*}$ is a
set of tuples of the $\mathtt{Set,Evidence}$ type, and (2)
$\mathit{set}_{2}=\bigcup\limits_{(\mathit{set}^{*},\epsilon^{*})\in\mathit{set}_{2}^{*}}\mathit{set}^{*}$,
is committed by $\mathit{rla}(v,2)$ (by LABEL:lst:verify_output_vg). By
comparability of $\mathit{rla}(v,2)$, either
$\mathit{set}_{1}^{*}\subseteq\mathit{set}_{2}^{*}$ or
$\mathit{set}_{1}^{*}\supset\mathit{set}_{2}^{*}$. We investigate all cases:

  * •

$\mathit{set}_{1}^{*}=\mathit{set}_{2}^{*}$: In this case,
$\mathit{set}_{1}=\mathit{set}_{2}$ and the theorem holds.

  * •

$\mathit{set}_{1}^{*}\subset\mathit{set}_{2}^{*}$: Therefore, every view
$v_{1}\in\mathit{set}_{1}$ belongs to $\mathit{set}_{2}$. Hence, the theorem
holds.

  * •

$\mathit{set}_{1}^{*}\supset\mathit{set}_{2}^{*}$: The case is symmetrical to
the previous one.

The theorem is satisfied in all possible cases, which concludes the proof. ∎

Next, we prove validity. In order to do so, we prove that all sets committed
by $\mathit{rla}(v,1)$ at time $t$ are subsets of $\Lambda_{t-1}^{v}$.

###### Lemma 0.

Let $\mathit{dec}$ be committed at $\mathit{rla}(v,1)$ at time $t$. Then,
$\mathit{dec}\subseteq\Lambda_{t-1}^{v}$.

###### Proof.

Suppose that there exists a tuple
$(v^{\prime},\mathit{set}^{\prime},\epsilon^{\prime})\in\mathit{dec}$ such
that
$\mathtt{valid}((v^{\prime},\mathit{set}^{\prime},\epsilon^{\prime}),v)=\bot$.
In this case, the validity property of $\mathit{rla}(v,1)$ is violated. Hence,
$\mathtt{valid}((v^{\prime},\mathit{set}^{\prime},\epsilon^{\prime}),v)=\top$,
for every
$(v^{\prime},\mathit{set}^{\prime},\epsilon^{\prime})\in\mathit{dec}$. Let
$E_{\mathit{dec}}=\\{\epsilon^{\prime}\,|\,(v^{\prime},\mathit{set}^{\prime},\epsilon^{\prime})\in\mathit{dec}\\}$.

Since $\mathit{dec}$ is committed at time $t$, there exists a (correct or
faulty) process that obtains $\omega_{\mathit{dec}}$ at time $t^{\prime}\leq
t$ such that
$\mathtt{verify\\_output}(\mathit{dec},\mathit{rla}(v,1),\omega_{\mathit{dec}})=\top$.
We know that $\omega_{\mathit{dec}}$ is a set of
$[\mathtt{ACK\\_CON}(v,1),\mathit{dec}]$ messages with
$|\omega_{\mathit{dec}}|\geq v.\mathtt{quorum()}$ (by
LABEL:lst:verify_output_rla). Hence, a correct server $r_{\mathit{dec}}\in
v.\mathtt{members()}$ sends its $\mathtt{ACK\\_CON}$ message by time $t$
(since $\omega_{\mathit{dec}}$ is obtained by time $t$) at line 17 of
LABEL:lst:rla_acceptor. Therefore, $\mathit{dec}$ is obtained before time $t$
(at line 16 of LABEL:lst:rla_acceptor), which implies that every
$\epsilon^{\prime}\in E_{\mathit{dec}}$ is obtained before time $t$. Thus, the
lemma holds. ∎

Since $\Lambda_{t-1}^{v}\subseteq\Lambda_{t^{\prime}}^{v}$, for any time
$t^{\prime}>t-1$, we conclude that
$\mathit{dec}\subseteq\Lambda_{t^{\prime}}^{v}$, if $\mathit{dec}$ is
committed by $\mathit{rla}(v,1)$ at time $t$. Next, we prove that all valid
inputs of $\mathit{rla}(v,2)$ “contain” sequences if the
$\mathit{preconditions}$ predicate is satisfied.

###### Lemma 0.

Let a (correct or faulty) process obtain $\epsilon$ at time $t$, such that
$o=(\mathit{set},\epsilon)$ is a tuple of the $\mathtt{Set,Evidence}$ type and
$\mathtt{valid}(o,v)=\top$. Let $\mathit{preconditions}(v,t-1)=\top$. Then,
$\mathit{set}$ is a sequence.

###### Proof.

Since $\mathtt{valid}(o,v)=\top$, we conclude that a set $\mathit{set}^{*}$,
where $\mathit{set}^{*}$ is a set of tuples of the
$\mathtt{View,Set,Evidence}$ type and
$\mathit{set}=\mathtt{construct}(\mathit{set}^{*})$, is committed by
$\mathit{rla}(v,1)$ at time $t$ (by LABEL:lst:set_proof). Hence,
$\mathit{set}^{*}\subseteq\Lambda_{t-1}^{v}$ (by Lemma 18). Let us take a
closer look at the $\mathtt{construct}(\mathit{set}^{*})$ function:

  * •

Let $|\mathit{VIEW}|=0$. Since $\mathit{preconditions}(v,t-1)=\top$ and
$\mathit{set}^{*}\subseteq\Lambda_{t-1}^{v}$, we know that all sets from
$\mathit{SET}$ are sequences. Hence, $\mathit{set}$ is a sequence.

  * •

Let $|\mathit{VIEW}|\neq 0$. In this case, we have that $|\mathit{set}|=1$.
Hence, $\mathit{set}$ is trivially a sequence.

The lemma holds. ∎

The next lemma builds upon Lemma 19 by showing that all views that belong to
two valid inputs of $\mathit{rla}(v,2)$ are comparable.

###### Lemma 0.

Let a (correct or faulty) process obtain $\epsilon_{1}$ at time $t_{1}$, such
that $o_{1}=(\mathit{set}_{1},\epsilon_{1})$ is a tuple of the
$\mathtt{Set,Evidence}$ type and $\mathtt{valid}(o_{1},v)=\top$. Moreover, let
a (correct or faulty) process obtain $\epsilon_{2}$ at time $t_{2}\geq t_{1}$,
such that $o_{2}=(\mathit{set}_{2},\epsilon_{2})$ is a tuple of the
$\mathtt{Set,Evidence}$ type and $\mathtt{valid}(o_{2},v)=\top$. Let
$v_{1}\in\mathit{set}_{1}$, $v_{2}\in\mathit{set}_{2}$ and
$\mathit{preconditions}(v,t_{2}-1)=\top$. Then, either $v_{1}\subseteq v_{2}$
or $v_{1}\supset v_{2}$.

###### Proof.

Since $\mathtt{valid}(o_{1},v)=\top$, we conclude that a set
$\mathit{set}_{1}^{*}$, where $\mathit{set}_{1}^{*}$ is a set of tuples of the
$\mathtt{View,Set,Evidence}$ type and
$\mathit{set}_{1}=\mathtt{construct}(\mathit{set}_{1}^{*})$, is committed by
$\mathit{rla}(v,1)$ at time $t_{1}$ (by LABEL:lst:set_proof). Similarly, a set
$\mathit{set}_{2}^{*}$, where $\mathit{set}_{2}^{*}$ is a set of tuples of the
$\mathtt{View,Set,Evidence}$ type and
$\mathit{set}_{2}=\mathtt{construct}(\mathit{set}_{2}^{*})$, is committed by
$\mathit{rla}(v,1)$ at time $t_{2}$ (by LABEL:lst:set_proof). By comparability
of $\mathit{rla}(v,1)$, we know that either
$\mathit{set}_{1}^{*}\subseteq\mathit{set}_{2}^{*}$ or
$\mathit{set}_{1}^{*}\supset\mathit{set}_{2}^{*}$. Furthermore, we know that
$\mathit{set}_{1}^{*}\subseteq\Lambda_{t_{2}-1}^{v}$ and
$\mathit{set}_{2}^{*}\subseteq\Lambda_{t_{2}-1}^{v}$ (by Lemma 18). We
investigate all three possibilities:

  * •

$\mathit{set}_{1}^{*}=\mathit{set}_{2}^{*}$: In this case,
$\mathit{set}_{1}=\mathit{set}_{2}$. Now, if
$|\mathit{set}_{1}|=|\mathit{set}_{2}|=1$, the lemma is satisfied. However, if
$|\mathit{set}_{1}|=|\mathit{set}_{2}|\neq 1$, we need to show that
$\mathit{set}_{1}=\mathit{set}_{2}$ is a sequence.

If $|\mathit{set}_{1}|=|\mathit{set}_{2}|\neq 1$, we know that
$\mathit{set}_{1}=\mathit{set}_{2}=\mathtt{max\\_cardinality}(\mathit{SET})$
in the $\mathtt{construct}$ function (line 10 of LABEL:lst:set_proof). Since
$\mathit{preconditions}(v,t_{2}-1)=\top$, we know that all sets from
$\mathit{SET}$ are sequences. Therefore, $\mathit{set}_{1}=\mathit{set}_{2}$
is a sequence. Thus, the lemma holds in this case.

  * •

$\mathit{set}_{1}^{*}\subset\mathit{set}_{2}^{*}$: We further distinguish
three cases:

    * –

$|\mathit{VIEW}_{1}|=|\mathit{VIEW}_{2}|=0$, where $|\mathit{VIEW}_{1}|$ is
the number of “stand-alone” views in $\mathit{set}_{1}^{*}$ (line 6 of
LABEL:lst:set_proof) and $|\mathit{VIEW}_{2}|$ is the number of “stand-alone”
views in $\mathit{set}_{2}^{*}$ (line 6 of LABEL:lst:set_proof): We know that
$\mathit{set}_{1}^{*},\mathit{set}_{2}^{*}\subseteq\Lambda_{t_{2}-1}^{v}$.
Since $\mathit{preconditions}(v,t_{2}-1)=\top$, we know that
$\mathit{set}_{1}$ is the greatest set of $\mathit{SET}_{1}$ with respect to
the containment relation (line 5 of LABEL:lst:set_proof), i.e.,
$\mathit{set}\subseteq\mathit{set}_{1}$, for every
$\mathit{set}\in\mathit{SET}_{1}$. Similarly, we know that $\mathit{set}_{2}$
is the greatest set of $\mathit{SET}_{2}$ with respect to the containment
relation (line 5 of LABEL:lst:set_proof), i.e.,
$\mathit{set}\subseteq\mathit{set}_{2}$, for every
$\mathit{set}\in\mathit{SET}_{2}$. Since
$\mathit{preconditions}(v,t_{2}-1)=\top$ and
$\mathit{set}_{1}^{*}\subset\mathit{set}_{2}^{*}$, we know that (1)
$\mathit{set}_{2}$ is a sequence, and (2)
$\mathit{set}_{1}\subseteq\mathit{set}_{2}$. Finally, the fact that
$v_{1}\in\mathit{set}_{2}$ ensures that
$\mathtt{comparable}(v_{1},v_{2})=\top$, which concludes the lemma in this
case.

    * –

$|\mathit{VIEW}_{1}|=0$ and $|\mathit{VIEW}_{2}|\neq 0$: In this case,
$\mathit{set}_{2}=\\{v_{2}\\}$. Since
$\mathit{set}_{1}^{*}\subseteq\Lambda_{t_{2}-1}^{v}$ and
$\mathit{preconditions}(v,t_{2}-1)=\top$, we know that $\mathit{set}_{1}$ is
the greatest set of $\mathit{SET}_{1}$ with respect to the containment
relation (line 5 of LABEL:lst:set_proof), i.e.,
$\mathit{set}\subseteq\mathit{set}_{1}$, for every
$\mathit{set}\in\mathit{SET}_{1}$. Moreover, we know that $\mathit{set}_{1}$
is a sequence.

Since $\mathit{set}_{1}^{*}\subset\mathit{set}_{2}^{*}$, we know that
$\mathit{set}_{1}\in\mathit{SET}_{2}$. Let $\mathit{set}_{2}^{\mathit{max}}$
be the greatest set of $\mathit{SET}_{2}$ with respect to the containment
relation (line 5 of LABEL:lst:set_proof), i.e.,
$\mathit{set}\subseteq\mathit{set}_{2}^{\mathit{max}}$, for every
$\mathit{set}\in\mathit{SET}_{2}$; because
$\mathit{set}_{2}^{*}\subseteq\Lambda_{t_{2}-1}^{v}$ and
$\mathit{preconditions}(v,t_{2}-1)=\top$, the greatest set
$\mathit{set}_{2}^{\mathit{max}}$ among $\mathit{SET}_{2}$ is indeed well
defined. Moreover, $\mathit{set}_{2}^{\mathit{max}}$ is a sequence. We
conclude that $\mathit{set}_{1}\subseteq\mathit{set}_{2}^{\mathit{max}}$.
Therefore,
$\mathit{set}_{1}.\mathtt{last}()\subseteq\mathit{greatest\\_view}$, where
$\mathit{greatest\\_view}=\mathtt{max\\_cardinality}(\mathit{set}_{2}^{\mathit{max}})=\mathit{set}_{2}^{\mathit{max}}.\mathtt{last()}$
(line 15 of LABEL:lst:set_proof). This implies, since $\mathit{set}_{1}$ is a
sequence, that $v_{1}\subseteq v_{2}$, which concludes the lemma in this case.

    * –

$|\mathit{VIEW}_{1}|\neq 0$ and $|\mathit{VIEW}_{2}|\neq 0$: Let
$\mathit{max}_{1}$ be the greatest set of $\mathit{SET}_{1}$ with respect to
the containment relation, i.e., $\mathit{set}\subseteq\mathit{max}_{1}$, for
every $\mathit{set}\in\mathit{SET}_{1}$; since
$\mathit{set}_{1}^{*}\subseteq\Lambda_{t_{2}-1}^{v}$ and
$\mathit{preconditions}(v,t_{2}-1)=\top$, the greatest set $\mathit{max}_{1}$
among $\mathit{SET}_{1}$ is well defined. Similarly, let $\mathit{max}_{2}$ be
the greatest set of $\mathit{SET}_{2}$ with respect to the containment
relation, i.e., $\mathit{set}\subseteq\mathit{max}_{2}$, for every
$\mathit{set}\in\mathit{SET}_{2}$; since
$\mathit{set}_{2}^{*}\subseteq\Lambda_{t_{2}-1}^{v}$ and
$\mathit{preconditions}(v,t_{2}-1)=\top$, the greatest set $\mathit{max}_{2}$
among $\mathit{SET}_{2}$ is well defined.

If $\mathit{max}_{1}\neq\bot$ and $\mathit{max}_{2}\neq\bot$, we know that
$\mathit{max}_{1}\subseteq\mathit{max}_{2}$ (since
$\mathit{set}_{1}^{*}\subset\mathit{set}_{2}^{*}$). Note that it is impossible
that $\mathit{max}_{1}\neq\bot$ and $\mathit{max}_{2}=\bot$ due to the fact
that $\mathit{set}_{1}^{*}\subset\mathit{set}_{2}^{*}$. Hence,
$\mathit{greatest\\_view}_{1}\subseteq\mathit{greatest\\_view}_{2}$, where
$\mathit{greatest\\_view}_{1}$ (resp., $\mathit{greatest\\_view}_{2}$) is the
value of the $\mathit{greatest\\_view}$ variable at line 17 of
LABEL:lst:set_proof of the $\mathtt{construct}(\mathit{set}_{1}^{*})$ (resp.,
$\mathtt{construct}(\mathit{set}_{2}^{*})$) function.

Similarly, we know that
$\bigcup\limits_{v^{*}\in\mathit{VIEW}_{1}}v^{*}\subseteq\bigcup\limits_{v^{**}\in\mathit{VIEW}_{2}}v^{**}$
(by comparability of $\mathit{rla}(v,1)$). Finally,
$v_{1}=\mathit{greatest\\_view}_{1}\cup\bigcup\limits_{v^{*}\in\mathit{VIEW}_{1}}v^{*}$
and
$v_{2}=\mathit{greatest\\_view}_{2}\cup\bigcup\limits_{v^{**}\in\mathit{VIEW}_{2}}v^{**}$,
which proves that $v_{1}\subseteq v_{2}$.

  * •

$\mathit{set}_{1}^{*}\supset\mathit{set}_{2}^{*}$: This case is symmetrical to
the previous one.

The lemma holds. ∎

The last lemma we prove prior to proving the validity property shows that a
set $\mathit{set}$ given as an input to $\mathit{rla}(v,2)$ must satisfy
$\mathit{set}.\mathtt{follows}(v)=\top$.

###### Lemma 0.

Let a (correct or faulty) process obtain $\epsilon$ at time $t$, such that
$o=(\mathit{set},\epsilon)$ is a tuple of the $\mathtt{Set,Evidence}$ type and
$\mathtt{valid}(o,v)=\top$. Let $\mathit{preconditions}(v,t-1)=\top$. Then,
$\mathit{set}.\mathtt{follows}(v)=\top$.

###### Proof.

Since $\mathtt{valid}(o,v)=\top$, we conclude that a set $\mathit{set}^{*}$,
where $\mathit{set}^{*}$ is a set of tuples of the
$\mathtt{View,Set,Evidence}$ type and
$\mathit{set}=\mathtt{construct}(\mathit{set}^{*})$, is committed by
$\mathit{rla}(v,1)$ at time $t$ (by LABEL:lst:set_proof).

By validity of $\mathit{rla}(v,1)$, we know that
$\mathit{set}^{*}\neq\emptyset$. Moreover,
$\mathit{set}^{*}\subseteq\Lambda_{t-1}^{v}$ (by Lemma 18). Let us take a
closer look at every tuple
$(v^{\prime},\mathit{set}^{\prime},\epsilon^{\prime})\in\mathit{set}^{*}$:

  * •

If $\mathit{set}^{\prime}=\emptyset$, we know that $v\subset v^{\prime}$ (due
to the fact that $\mathit{preconditions}(v,t-1)=\top$).

  * •

Otherwise, $\mathit{set}^{\prime}.\mathtt{follows}(v)=\top$ and
$v^{\prime}\in\mathit{set}^{\prime}$ (due to the fact that
$\mathit{preconditions}(v,t-1)=\top$).

Finally, we consider the $\mathtt{construct}(\mathit{set}^{*})$ function:

  * •

Let $|\mathit{VIEW}|=0$. Since $\mathit{preconditions}(v,t-1)=\top$ and
$\mathit{set}^{*}\subseteq\Lambda_{t-1}^{v}$, we know that
$\mathit{set}.\mathtt{follows}(v)=\top$, which concludes the lemma.

  * •

Let $|\mathit{VIEW}|\neq 0$. In this case, $\mathit{set}$ contains a single
view. Moreover, we have that $v\subset v^{\prime}$, for every “stand-alone”
view $v^{\prime}\in\mathit{VIEW}$. Therefore,
$\mathit{set}.\mathtt{follows}(v)=\top$.

Hence, the lemma holds. ∎

Finally, we are able to prove the validity property of $\mathit{vg}(v)$.

###### Theorem 22 (Validity).

Algorithm given in LABEL:lst:view_generator_implementation satisfies validity.

###### Proof.

Let $\mathit{set}$ be committed by $\mathit{vg}(v)$ at time $t$ and let
$\mathit{preconditions}(v,t-1)=\top$. Since $\mathit{set}$ is committed at
time $t$ by $\mathit{vg}(v)$, a set $\mathit{set}_{\mathit{rla}(v,2)}$ is
committed by $\mathit{rla}(v,2)$ at time $t$, where (1)
$\mathit{set}_{\mathit{rla}(v,2)}$ is a set of tuples of the
$\mathtt{Set,Evidence}$ type, and (2)
$\mathit{set}=\bigcup\limits_{(\mathit{set}^{*},\epsilon^{*})\in\mathit{set}_{\mathit{rla}(v,2)}}\mathit{set}^{*}$
(by LABEL:lst:verify_output_vg). By validity of $\mathit{rla}(v,2)$, we know
that $\mathit{set}_{\mathit{rla}(v,2)}\neq\emptyset$. Moreover, because of the
$\mathtt{construct}$ function, we know that $\mathit{set}\neq\emptyset$.

Next, we show that $\mathit{set}$ is a sequence. Suppose, by contradiction,
that $v_{1},v_{2}\in\mathit{set}$ such that
$\mathtt{comparable}(v_{1},v_{2})=\bot$. Since $v_{1}\in\mathit{set}$, we know
that $v_{1}\in\mathit{set}^{*}$, where
$(\mathit{set}^{*},\epsilon^{*})\in\mathit{set}_{\mathit{rla}(v,2)}$.
Similarly, we know that $v_{2}\in\mathit{set}^{**}$, where
$(\mathit{set}^{**},\epsilon^{**})\in\mathit{set}_{\mathit{rla}(v,2)}$. We
distinguish two scenarios:

  * •

Let $\mathit{set}^{*}=\mathit{set}^{**}$. We know that
$\mathtt{valid}((\mathit{set}^{*},\epsilon^{*}),v)=\top$ (by validity of
$\mathit{rla}(v,2)$). Moreover, a process obtains $\epsilon^{*}$ at time
$t^{\prime}\leq t$. Since $\mathit{preconditions}(v,t-1)=\top$, we conclude
that $\mathit{set}^{*}=\mathit{set}^{**}$ is a sequence (by Lemma 19). Thus,
$\mathtt{comparable}(v_{1},v_{2})$ cannot return $\bot$.

  * •

Let $\mathit{set}^{*}\neq\mathit{set}^{**}$. By validity of
$\mathit{rla}(v,2)$, we know that
$\mathtt{valid}((\mathit{set}^{*},\epsilon^{*}),v)=\mathtt{valid}((\mathit{set}^{**},\epsilon^{**}),v)=\top$.
Since $\mathit{set}$ is committed at time $t$, we conclude that a (correct or
faulty) process obtains $\epsilon^{*}$ (resp., $\epsilon^{**}$) at time
$t^{*}\leq t$ (resp., $t^{**}\leq t$). Finally, the fact that
$\mathit{preconditions}(v,t-1)=\top$ implies that it is impossible that
$\mathtt{comparable}(v_{1},v_{2})=\bot$ (by Lemma 20).

Therefore, $\mathit{set}$ is indeed a sequence.

Finally, we show that $\mathit{set}.\mathtt{follows}(v)=\top$. Suppose, by
contradiction, that there exists a view $v^{*}\in\mathit{set}$ such that
$v\not\subset v^{*}$. Hence, there exists
$(\mathit{set}^{*},\epsilon^{*})\in\mathit{set}_{\mathit{rla}(v,2)}$ such that
(1) $v^{*}\in\mathit{set}^{*}$, and (2)
$\mathtt{valid}((\mathit{set}^{*},\epsilon^{*}),v)=\top$ (by validity of
$\mathit{rla}(v,2)$). Moreover, $\epsilon^{*}$ is obtained at time $t^{*}\leq
t$ by a server. Since $\mathit{preconditions}(v,t-1)=\top$, we know that
$\mathit{set}^{*}.\mathtt{follows}(v)=\top$ (by Lemma 21). Hence,
$v^{*}\notin\mathit{set}^{*}$, which concludes the theorem. ∎

The next theorem proves membership validity of $\mathit{vg}(v)$.

###### Theorem 23 (Membership Validity).

Algorithm given in LABEL:lst:view_generator_implementation satisfies
membership validity.

###### Proof.

Let $\mathit{preconditions}(v,t-1)=\top$ and let $(+,r)\notin v$, for some
server $r$. Let $\mathit{set}$ be committed by $\mathit{vg}(v)$ at time $t$.
By contradiction, suppose that $(-,r)\in\mathit{set}.\mathtt{last()}$; recall
that $\mathit{set}$ is a sequence because of the validity property of
$\mathit{vg}(v)$. Let $\mathit{set}.\mathtt{last()}=v^{*}$.

Since $\mathit{set}$ is committed at time $t$ by $\mathit{vg}(v)$, a set
$\mathit{set}_{\mathit{rla}(v,2)}$ is committed by $\mathit{rla}(v,2)$ at time
$t$, where (1) $\mathit{set}_{\mathit{rla}(v,2)}$ is a set of tuples of the
$\mathtt{Set,Evidence}$ type, and (2)
$\mathit{set}=\bigcup\limits_{(\mathit{set}^{*},\epsilon^{*})\in\mathit{set}_{\mathit{rla}(v,2)}}\mathit{set}^{*}$
(by LABEL:lst:verify_output_vg). We conclude that there exists a tuple
$(\mathit{set}^{*},\epsilon^{*})\in\mathit{set}_{\mathit{rla}_{v,2}}$ such
that $v^{*}\in\mathit{set}^{*}$. Moreover, we know that
$\mathtt{valid}((\mathit{set}^{*},\epsilon^{*}),v)=\top$ (by the validity
property of $\mathit{rla}(v,2)$).

Since $\epsilon^{*}$ is obtained by time $t$, a set
$\mathit{set}_{\mathit{rla}(v,1)}$ is committed by $\mathit{rla}(v,1)$ at time
$t$, where (1) $\mathit{set}_{\mathit{rla}(v,1)}$ is a set of tuples of the
$\mathtt{View,Set,Evidence}$ type, and (2)
$\mathit{set^{*}}=\mathtt{construct}(\mathit{set}_{\mathit{rla}(v,1)})$ (by
LABEL:lst:set_proof). Hence,
$\mathit{set}_{\mathit{rla}(v,1)}\subseteq\Lambda_{t-1}^{v}$ (by Lemma 18).
Finally, we consider the
$\mathtt{construct}(\mathit{set}_{\mathit{rla}(v,1)})$ function:

  * •

Let $|\mathit{VIEW}|=0$. Since $\mathit{preconditions}(v,t-1)=\top$ and
$\mathit{set}_{\mathit{rla}(v,1)}\subseteq\Lambda_{t-1}^{v}$, we know that
$(-,r)\notin\mathit{set}^{*}.\mathtt{last()}$. Since $\mathit{set}^{*}$ is a
sequence, that means that $v^{*}\notin\mathit{set}^{*}$.

  * •

Let $|\mathit{VIEW}|\neq 0$. In this case, $\mathit{set}$ contains a single
view. We know that $(-,r)\notin\mathit{greatest\\_view}$ at line 17 of
LABEL:lst:set_proof since $\mathit{preconditions}(v,t-1)=\top$. Moreover, we
have that $(-,r)\notin v^{\prime}$, for every “stand-alone” view
$v^{\prime}\in\mathit{VIEW}$ (since $\mathit{preconditions}(v,t-1)=\top$).
Therefore, it is impossible that $v^{*}\in\mathit{set}^{*}$.

The theorem holds. ∎

Next, we prove the safety property of $\mathit{vg}(v)$.

###### Theorem 24 (Safety).

Algorithm given in LABEL:lst:view_generator_implementation satisfies safety.

###### Proof.

Let $\mathit{set}$ be committed by $\mathit{vg}(v)$ at time $t$. In the rest
of the proof, let
$(v^{\prime},\emptyset,\epsilon^{\prime})\notin\Lambda_{t-1}^{v}$. In order to
prove the theorem, we prove that
$(v_{\mathit{set}},\mathit{set},\epsilon_{\mathit{set}})\in\Lambda_{t-1}^{v}$
in this case, for some view $v_{\mathit{set}}$ and some proof
$\epsilon_{\mathit{set}}$.

Since $\mathit{set}$ is committed by $\mathit{vg}(v)$ at time $t$, we know
that $\mathit{set}_{\mathit{rla}(v,2)}$ is committed by $\mathit{rla}(v,2)$ at
time $t$, where
$\mathit{set}=\bigcup\limits_{(\mathit{set}^{*},\epsilon^{*})\in\mathit{set}_{\mathit{rla}(v,2)}}\mathit{set}^{*}$
(by LABEL:lst:verify_output_vg).

Let $(\mathit{set}^{*},\epsilon^{*})\in\mathit{set}_{\mathit{rla}(v,2)}$. We
know that $\mathtt{valid}((\mathit{set}^{*},\epsilon^{*}),v)=\top$ (by
validity of $\mathit{rla}(v,2)$). Hence, a set
$\mathit{set}_{\mathit{rla}(v,1)}$ of tuples of the
$\mathtt{View,Set,Evidence}$ type is committed by $\mathit{rla}(v,1)$ at time
$t$, where
$\mathit{set}^{*}=\mathtt{construct}(\mathit{set}_{\mathit{rla}(v,1)})$ (by
LABEL:lst:set_proof). By Lemma 18, we know that
$\mathit{set}_{\mathit{rla}(v,1)}\subseteq\Lambda_{t-1}^{v}$.

Let us now take a closer look at the
$\mathtt{construct}(\mathit{set}_{\mathit{rla}(v,1)})$ function. Since
$(v^{\prime},\emptyset,\epsilon^{\prime})\notin\Lambda_{t-1}^{v}$ and
$\mathit{preconditions}(v,t-1)=\top$, we conclude that
$\mathit{set}^{*}\in\mathit{SET}$ (because $|\mathit{VIEW}|=0$). Hence,
$(v^{*},\mathit{set}^{*},\epsilon^{*})\in\Lambda_{t-1}^{v}$.

Because $\mathit{preconditions}(v,t-1)=\top$, either
$\mathit{set}_{1}^{*}\subseteq\mathit{set}_{2}^{*}$ or
$\mathit{set}_{1}^{*}\supset\mathit{set}_{2}^{*}$, where
$(\mathit{set}_{1}^{*},\epsilon_{1}^{*}),(\mathit{set}_{2}^{*},\epsilon_{2}^{*})\in\mathit{set}_{\mathit{rla}(v,2)}$.
Hence, $\mathit{set}=\mathit{set}^{**}$, where
$(\mathit{set}^{**},\epsilon^{**})\in\mathit{set}_{\mathit{rla}(v,2)}$.
Therefore,
$(v_{\mathit{set}},\mathit{set},\epsilon_{\mathit{set}})\in\Lambda_{t-1}^{v}$,
for some view $v_{\mathit{set}}$ and some evidence $\epsilon_{\mathit{set}}$,
which concludes the proof of the theorem. ∎

The next theorem proves the decision certification property.

###### Theorem 25 (Decision Certification).

Algorithm given in LABEL:lst:view_generator_implementation satisfies decision
certification.

###### Proof.

The theorem follows from the decision certification property of
$\mathit{rla}(v,2)$ and the fact that a correct server decides the union of
all sets (at line 26 of LABEL:lst:view_generator_implementation). ∎

Next, we prove the decision permission property.

###### Theorem 26 (Decision Permission).

Algorithm given in LABEL:lst:view_generator_implementation satisfies decision
permission.

###### Proof.

Let $\mathit{set}$ be committed by $\mathit{vg}(v)$. Hence,
$\mathit{set}_{\mathit{rla}(v,2)}$ is committed by $\mathit{rla}(v,2)$ (by
line 4 of LABEL:lst:verify_output_vg). Hence, at least
$v.\mathtt{plurality()}$ of correct members of $v$ have previously started
$\mathit{rla}(v,2)$ (by decision permission of $\mathit{rla}(v,2)$). All those
servers have started $\mathit{rla}(v,2)$ at line 22 of
LABEL:lst:view_generator_implementation.

Therefore, $\mathit{set}_{\mathit{rla}(v,1)}$ is committed by
$\mathit{rla}(v,1)$ (by the decision certification of $\mathit{rla}(v,1)$).
Again, at least $v.\mathtt{plurality()}$ of correct members of $v$ have
previously started $\mathit{rla}(v,1)$ (by decision permission of
$\mathit{rla}(v,1)$). All those servers have started $\mathit{rla}(v,1)$ at
line 12 or at line 14 of LABEL:lst:view_generator_implementation. Thus, all
those servers have started $\mathit{vg}(v)$, which concludes the theorem. ∎

Next, we prove the bounded decisions property of $\mathit{vg}(v)$.

###### Theorem 27 (Bounded Decisions).

Algorithm given in LABEL:lst:view_generator_implementation satisfies bounded
decisions.

###### Proof.

Follows directly from the bounded decisions property of $\mathit{rla}(v,2)$
(by LABEL:lst:verify_output_vg). ∎

Finally, we prove the liveness property of $\mathit{vg}(v)$.

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

Algorithm given in LABEL:lst:view_generator_implementation satisfies liveness.

###### Proof.

If every correct server $r\in v.\mathtt{members}()$ starts $\mathit{vg}(v)$, a
correct server proposes to $\mathit{vg}(v)$ and no correct server
$r^{\prime}\in v.\mathtt{members}()$ stops $\mathit{vg}(v)$, every correct
server eventually decides from $\mathit{rla}(v,1)$ (by liveness of
$\mathit{rla}(v,1)$). Then, every correct server starts $\mathit{rla}(v,2)$
with a proposal. By liveness of $\mathit{rla}(v,2)$, all correct servers
eventually decide from $\mathit{rla}(v,2)$. Thus, all correct servers
eventually decide from $\mathit{vg}(v)$ at line 26 of
LABEL:lst:view_generator_implementation. ∎

##  5\. Server’s Modules: Storage Module

As servers carry the most of the logic of Carbon, we separate the protocol
executed by servers into a multiple _modules_. Each module of a server
contains its own logic.

The first module of a server we present is the _storage module_. The storage
module, as the name suggests, has the responsibility of storing fundamental
information used by other modules. For example, the storage module keeps track
of received messages.

##### “Install” messages.

Servers exchange different types of messages in Carbon. The information about
the evolution of the system membership is carried by $\mathtt{INSTALL}$
messages. We define these messages below.

⬇

1Install_Message:

2 instance $[$INSTALL, $\mathit{source}$, $\mathit{set}$, $\omega]$, with
$\mathit{source}$ is View, $\mathit{set}$ is Set(View) and $\omega$ is
Certificate such that verify_output($\mathit{set}$,
$\mathit{vg}(\mathit{source})$, $\omega$) $=\top$

4 function (Install_Message $m$).source():

5 let $m=[$INSTALL, $\mathit{source}$, $\mathit{set}$, $\omega]$

6 return $\mathit{source}$

8 function (Install_Message $m$).destination():

9 let $m=[$INSTALL, $\mathit{source}$, $\mathit{set}$, $\omega]$

10 return min_cardinality777We assume that the
$\mathtt{min\\_cardinality(\mathit{set})}$ deterministic function, where
$\mathit{set}$ is a set of sets, returns the set with the smallest cardinality
that belongs to $\mathit{set}$; if there are multiple sets that satisfy the
condition, then any such set is returned.($\mathit{set}$) // get the view with
the smallest cardinality888Recall that a view is a set of changes.

12 function (Install_Message $m$).tail():

13 let $m=[$INSTALL, $\mathit{source}$, $\mathit{set}$, $\omega]$

14 return $\mathit{set}\setminus\\{m$.destination()$\\}$

Listing 20: $\mathtt{INSTALL}$ message

As it can be seen from LABEL:lst:install_messages, $\mathit{set}$ is a set of
views. However, we prove in the rest of the paper that $\mathit{set}$ is,
actually, a sequence. Until we prove this claim, we treat $\mathit{set}$ as a
set of views (as written in LABEL:lst:install_messages).

##### View-paths.

Next, we introduce _view-paths_ : ordered sets of “adjacent”
$\mathtt{INSTALL}$ messages.

⬇

1View_Path:

2 instance $[m_{1},m_{2},...,m_{k}]$ with $k\geq 1$ is Integer, $m_{i}$ is
Install_Message, for every $i\in[1,k]$,
$m_{1}$.source() $=\mathit{genesis}$ and $m_{j}$.source()
$=m_{j-1}$.destination(), for every $j\in[2,k]$

4 function (View_Path $\mathit{path}$).views():

5 let $\mathit{path}=[m_{1},...,m_{k}]$

6 return $\\{v\,|\,v=\mathit{genesis}\text{ or }v=m_{i}$.destination(), where
$m_{i}\in\mathit{path}\\}$

8 function (View_Path $\mathit{path}$).destination():

9 let $\mathit{path}=[m_{1},...,m_{k}]$

10 return $m_{k}$.destination()

12 function (View_Path $\mathit{path}$).tail():

13 let $\mathit{path}=[m_{1},...,m_{k}]$

14 return $m_{k}$.tail()

Listing 21: View-path

By slightly abusing the notion, sometimes we write
“$\mathit{path}\subseteq\mathit{set}$”, where $\mathit{path}$ is a view-path
and $\mathit{set}$ is a set of $\mathtt{INSTALL}$ messages, to mean that every
message that belongs to $\mathit{path}$ belongs to $\mathit{set}$, as well.

##### Storage module - implementation.

We now give the implementation of the storage module.

⬇

1Storage Module:

2 Implementation:

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

4 Set(Message) $\mathit{waiting\\_messages}=\emptyset$ // all received
messages that have not been processed

6 Set(View) $\mathit{history}=\\{\mathit{genesis}\\}$ // we prove that
$\mathit{history}$ is actually a sequence; see § 6.2.2

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

9 Map(View $\to$ View) $\mathit{source}=\\{\mathit{genesis}\to\bot\\}$

10 // as we show in the rest of the paper, these are actually sequences (not
‘‘just’’ sets of views); see § 6.2.2

11 Map(View $\to$ Set(View)) $\mathit{sequence}=\\{\mathit{genesis}\to\bot\\}$

12 Map(View $\to$ View_Path)
$\mathit{view\\_path}=\\{\mathit{genesis}\to\emptyset\\}$

Listing 22: Storage module - initialization

⬇

1Storage Module:

2 Implementation:

3 upon receipt of Message $m$:

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

6 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}$:

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

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

9 extract_requests_and_voting_proofs($m$) // see
LABEL:lst:reconfiguration_extract_requests_passing_proofs

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

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

12 gossip $m$ // gossip the message

13 if $\mathit{source}[v^{\prime}]=\bot$ or
$\mathit{source}[v^{\prime}]\supset v$:

14 $\mathit{source}[v^{\prime}]=v$

15 $\mathit{sequence}[v^{\prime}]=\mathit{set}$

16 $\mathit{view\\_path}[v^{\prime}]=\mathit{view\\_path}[v]||m$ // $||$
denotes the concatenation

Listing 23: Storage module - message processing

##  6\. Server’s Modules: Reconfiguration Module

This section is devoted to the _reconfiguration module_ of a server. The
reconfiguration module carries the reconfiguration logic of Carbon.

##### Valid views.

Next, we give the formal definition of _valid views_ (see LABEL:lst:view).

###### Definition 0 (Valid View).

Let $\mathcal{I}^{*}(\infty)$ denote the set of $\mathtt{INSTALL}$ messages
ever obtained by (correct or faulty) processes. A view $v$ is _valid_ if and
only if:

  * •

$v=\mathit{genesis}$, or

  * •

there exists a view-path $\mathit{path}$ such that
$\mathit{path}\subseteq\mathcal{I}^{*}(\infty)$ and
$\mathit{path}.\mathtt{destination()}=v$.

Recall that we assume that at least a quorum of members of a valid view is
correct (see § 2, paragraph “Failure model”).

##### Forever-alive views.

Next important concept we introduce is a concept of _forever-alive views_.
Intuitively, a view $v$ is forever-alive if there exists a forever-correct
process that “knows” a view-path to $v$ and “shares” that information by
gossiping it. We give the formal definition below.

###### Definition 0 (Forever-Alive View).

We say that a valid view $v$ is _forever-alive_ if and only if:

  * •

$v=\mathit{genesis}$, or

  * •

there exists a forever-correct process $p$ such that (1) $p$ obtains a view-
path $\mathit{path}$ with $\mathit{path}.\mathtt{destination()}=v$, and (2)
$p$ gossips all messages that belong to $\mathit{path}$.

Observe that every forever-alive view is valid.

##### Properties.

We now introduce a few properties that are satisfied by the reconfiguration
(and storage) module. A correct process _updates_ its current view to a view
$v$ if and only if it triggers the special $\mathtt{update}\text{
}\mathtt{current}\text{ }\mathtt{view}\text{ }\mathtt{to}\text{
}\mathtt{view}\text{ }v$ event. Similarly, a correct process _installs_ a view
$v$ if and only if it triggers the special $\mathtt{install}\text{
}\mathtt{view}\text{ }v$ event. Finally, a correct process _stops processing_
in a view $v$ if and only if it triggers the special $\mathtt{stop}\text{
}\mathtt{processing}\text{ }\mathtt{in}\text{ }\mathtt{view}\text{
}v^{\prime}$ event, where $v^{\prime}\supseteq v$.

⬇

1Reconfiguration and Storage Module:

2 Properties:

3 \- View Comparability: All valid views are comparable.

4 \- Finitely Many Valid Views: There exist only finitely many valid views.

5 \- Finality: Let $v_{\mathit{final}}$ be the greatest forever-alive
view999Note that $v_{\mathit{final}}$ is well-defined due to the fact that
$\mathit{genesis}$ is a forever-alive view, all forever-alive views are valid,
there are finitely many valid views and all valid views are comparable (by the
view comparability property).. Then, (1) all correct members of
$v_{\mathit{final}}$ update their current view to $v_{\mathit{final}}$, (2) no
correct member of $v_{\mathit{final}}$ updates its current view to any view
after updating it to $v_{\mathit{final}}$, (3) all correct members of
$v_{\mathit{final}}$ install $v_{\mathit{final}}$, (4) no correct member of
$v_{\mathit{final}}$ leaves, and (5) no correct member of $v_{\mathit{final}}$
stops processing in $v_{\mathit{final}}$.

Listing 24: Reconfiguration and storage modules - properties

###  6.1. Reconfiguration Module - Implementation

We now give the implementation of the reconfiguration module. We start by
introducing the evidence used as the input to the view generator primitive
(see § 4).

⬇

1View_Generator_Evidence:

2 instance $\epsilon_{\mathit{vg}}=$ {

3 View_Path $\mathit{path}$

4 Map(Change $\to$ Message) $\mathit{requests}$

5 Map(Change $\to$ Voting_Proof) $\mathit{voting\\_proofs}$

6 }

Listing 25: Evidence used as the input for the view generator primitive

Next, we define when are inputs of the view generator primitive deemed valid.

⬇

1function valid(View, Set, Evidence
$(v^{\prime},\mathit{set}^{\prime},\epsilon^{\prime})$, View $v$):

2 if $v=\mathit{genesis}$:

3 if $v\not\subset v^{\prime}$ or $\mathit{set}^{\prime}\neq\emptyset$ or
$\epsilon^{\prime}$ is not View_Generator_Evidence:

4 return $\bot$

6 if $\epsilon^{\prime}.\mathit{path}\neq\bot$:

7 return $\bot$

9 if $(+,r)\notin v$ and $(-,r)\in v^{\prime}$, for some Server $r$:

10 return $\bot$

12 for each Change $c\in v^{\prime}$:

13 if $c\notin\mathit{genesis}$:

14 if $c=(+,r)$, for some Server $r$:

15 Message $m=\mathit{requests}[c]$

16 if $m\neq[$JOIN, Voting_Proof $\sigma_{v}]$ or $m.$sender $\neq r$ or
verify_voting(“add server $r$”, $\sigma_{v}$) $\neq\top$:

17 return $\bot$

18 else:

19 let $c=(-,r)$, for some Server $r$

20 Message $m=\mathit{requests}[c]$

21 Voting_Proof $\sigma_{v}=\mathit{voting\\_proofs}[c]$

22 if ($m\neq[$LEAVE$]$ or $m.$sender $\neq r$) and verify_voting(“remove
server $r$”, $\sigma_{v}$) $\neq\top$:

23 return $\bot$

24 return $\top$

26 // $v\neq\mathit{genesis}$

27 if $\mathit{set}^{\prime}\neq\emptyset$ and
$v^{\prime}\notin\mathit{set}^{\prime}$:

28 return $\bot$

30 if $\mathit{set}^{\prime}=\emptyset$ and $v\not\subset v^{\prime}$:

31 return $\bot$

33 if exists View $v^{*}\in\mathit{set}^{\prime}$ such that $v\not\subset
v^{*}$:

34 return $\bot$

36 if $(+,r)\notin v$ and exists View $v^{*}\in\mathit{set}^{\prime}$ such
that $(-,r)\in v^{*}$, for some Server $r$:

37 return $\bot$

39 if $(+,r)\notin v$ and $(-,r)\in v^{\prime}$, for some Server $r$:

40 return $\bot$

42 if $\epsilon^{\prime}$ is not View_Generator_Evidence:

43 return $\bot$

45 if $\epsilon^{\prime}.\mathit{path}$.destination() $\neq v$ or
$\epsilon^{\prime}.\mathit{path}$.tail() $\neq\mathit{set}^{\prime}$:

46 return $\bot$

48 for each Change $c\in
v^{\prime}\cup\bigcup\limits_{v^{*}\in\mathit{set}^{\prime}}v^{*}$:

49 if $c\notin\mathit{genesis}$:

50 if $c=(+,r)$, for some Server $r$:

51 Message $m=\mathit{requests}[c]$

52 if $m\neq[$JOIN, Voting_Proof $\sigma_{v}]$ or $m.$sender $\neq r$ or
verify_voting(“add server $r$”, $\sigma_{v}$) $\neq\top$:

53 return $\bot$

54 else:

55 let $c=(-,r)$, for some Server $r$

56 Message $m=\mathit{requests}[c]$

57 Voting_Proof $\sigma_{v}=\mathit{voting\\_proofs}[c]$

58 if ($m\neq[$LEAVE$]$ or $m.$sender $\neq r$) and verify_voting(“remove
server $r$”, $\sigma_{v}$) $\neq\top$:

59 return $\bot$

60 return $\top$

Listing 26: (View, Set, Evidence) tuple - the $\mathtt{valid}$ function

Finally, we give the implementation of the reconfiguration module.

⬇

1Reconfiguration Module:

2 Implementation:

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

4 $\mathit{current\\_view}=$ {

5 View $\mathit{view}=\bot$

6 Bool $\mathit{installed}=\bot$

7 Bool $\mathit{processing}=\bot$

8 View_Path $\mathit{proof}=\bot$

9 }

11 Bool $\mathit{joined}=\bot$

12 View $\mathit{stop\\_processing\\_until}=\emptyset$

13 Bool $\mathit{proposed}=\bot$

15 $\mathit{reconfiguration}=$ {

16 Set(Change) $\mathit{requested}=\emptyset$

17 Map(Change $\to$ Message) $\mathit{requests}=\\{c\to\bot\text{, for every
Change }c\\}$

18 Map(Change $\to$ Voting_Proof) $\mathit{voting\\_proofs}=\\{c\to\bot\text{,
for every Change }c\\}$

20 View $\mathit{source}=\bot$

21 View $\mathit{destination}=\bot$