22 Set(View) $\mathit{sequence}=\bot$ // we prove that this is actually a
sequence; see § 6.2.2

24 Bool $\mathit{prepared}=\bot$

25 Bool $\mathit{discharged}=\bot$

26 }

28 $\mathit{state\\_transfer}=$ {

29 Bool $\mathit{in\\_progress}=\bot$

30 Map(View $\to$ Set(State)) $\mathit{states}=\\{v\to\emptyset\text{, for
every View }v\\}$

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

32 }

34 $dischargement=$ {

35 View $\mathit{dischargement\\_view}=\bot$

36 Map(View $\to$ Set(Server))
$\mathit{dischargements}=\\{v\to\emptyset\text{, for every View }v\\}$

37 }

39 if $r\in\mathit{genesis}$.members():

40 $\mathit{current\\_view}.\mathit{view}=\mathit{genesis}$

41 trigger update current view to $\mathit{genesis}$ // the server updates its
current view to $\mathit{genesis}$

43 $\mathit{current\\_view}.\mathit{installed}=\top$

44 trigger install view $\mathit{genesis}$ // the server installs
$\mathit{genesis}$

45 installed($\mathit{genesis}$) // see LABEL:lst:transaction_module

46 $\mathit{current\\_view}.\mathit{processing}=\top$

48 $\mathit{joined}=\top$

49 trigger joined // the server joins

51 // triggering events for joined servers

52 for each Server $r\in\mathit{genesis}$.members():

53 trigger $r$ joined // server $r$ joins

55 trigger <$\mathit{vg}(\mathit{genesis})$.Start | $\bot$>

Listing 27: Reconfiguration module - initialization

⬇

1Reconfiguration Module:

2 Implementation:

3 function extract_requests_and_voting_proofs(Install_Message $m$):

4 update $\mathit{reconfiguration}.\mathit{requests}$ with requests from $m$

5 update $\mathit{reconfiguration}.\mathit{voting\\_proofs}$ with voting
proofs from $m$

Listing 28: Reconfiguration module - the
$\mathtt{extract\\_requests\\_and\\_voting\\_proofs}$ function

⬇

1Reconfiguration Module:

2 Implementation:

3 upon join with voting proof $\sigma_{v}$: // the server requests to join

4 gossip [JOIN, $\sigma_{v}$]

6 upon exists Message $m\in\mathit{waiting\\_messages}$ such that $m=[$JOIN,
Voting_Proof $\sigma_{v}]$ and
verify_voting(“add server $m$.sender”, $\sigma_{v}$) $=\top$ and
$(+,m$.sender$)\notin\mathit{reconfiguration}.\mathit{requested}$:

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

8
$\mathit{reconfiguration}$.$\mathit{requested}=\mathit{reconfiguration}$.$\mathit{requested}\cup\\{(+,m.$sender$)\\}$

9 $\mathit{reconfiguration}.\mathit{requests}[(+,m.\text{sender})]=m$

Listing 29: Reconfiguration module - joining

⬇

1Reconfiguration Module:

2 Implementation:

3 upon leave: // the server requests to leave

4 gossip [LEAVE]

6 upon exists Message $m\in\mathit{waiting\\_messages}$ such that
$m=[$LEAVE$]$ and
$(-,m$.sender$)\notin\mathit{reconfiguration}.\mathit{requested}$:

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

8
$\mathit{reconfiguration}.\mathit{requested}=\mathit{reconfiguration}.\mathit{requested}\cup\\{(-,m$.sender$)\\}$

9 $\mathit{reconfiguration}.\mathit{requests}[(-,m.\text{sender})]=m$

11 upon obtaining Voting_Proof $\sigma_{v}$ such that
verify_voting(“remove server $r$”, $\sigma_{v}$) $=\top$ and
$(-,r)\notin\mathit{reconfiguration}.\mathit{requested}$:

12
$\mathit{reconfiguration}.\mathit{requested}=\mathit{reconfiguration}.\mathit{requested}\cup\\{(-,r)\\}$

13 $\mathit{reconfiguration}.\mathit{voting\\_proofs}[(-,r)]=\sigma_{v}$

Listing 30: Reconfiguration module - leaving

⬇

1Reconfiguration Module:

2 Implementation:

3 function to_propose():

4 Set(Change) $\mathit{proposal}=\emptyset$

5 for each Change
$\mathit{change}\in\mathit{reconfiguration}.\mathit{requested}$ such that
$\mathit{change}\notin\mathit{current\\_view}.\mathit{view}$:

6 if $\mathit{change}=(+,r)$, for some Server $r$:

7 $\mathit{proposal}=\mathit{proposal}\cup\\{\mathit{change}\\}$

8 else if $\mathit{change}=(-,r)$, for some Server $r$:

9 if $(+,r)\in\mathit{current\\_view}.\mathit{view}$:

10 $\mathit{proposal}=\mathit{proposal}\cup\\{\mathit{change}\\}$

11 return $\mathit{proposal}$

13 upon to_propose() $=\mathit{proposal}\neq\emptyset$ and
$\mathit{current\\_view}.\mathit{installed}=\top$ and
$\mathit{proposed}=\bot$:

14 View_Generator_Evidence $\epsilon_{\mathit{vg}}$

15
$\epsilon_{\mathit{vg}}.\mathit{path}=\mathit{current\\_view}.\mathit{proof}$

16
$\epsilon_{\mathit{vg}}.\mathit{requests}=\mathit{reconfiguration}.\mathit{requests}$

17
$\epsilon_{\mathit{vg}}.\mathit{voting\\_proofs}=\mathit{reconfiguration}.\mathit{voting\\_proofs}$

18 trigger <$\mathit{vg}(\mathit{current\\_view}.\mathit{view})$.Propose | $(\mathit{current\\_view}.\mathit{view}\cup\mathit{proposal},\emptyset,\epsilon_{\mathit{vg}})$>

19 $\mathit{proposed}=\top$

21 upon <$\mathit{vg}(\mathit{current\\_view}.\mathit{view})$.Decide | Set(View) $\mathit{set}$, Certificate $\omega$>:

22 Install_Message $m=[$INSTALL, $\mathit{current\\_view}.\mathit{view}$,
$\mathit{set}$, $\omega]$ // create the INSTALL message

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

Listing 31: Reconfiguration module - view generation

⬇

1Reconfiguration Module:

2 Implementation:

3 upon $\\{$($\mathit{joined}=\bot$ and exists View $v\in\mathit{history}$
such that $r\in v$.members() and $r\notin\mathit{source}[v]$.members()) or
($\mathit{joined}=\top$ and exists View $v\in\mathit{history}$ such that
$\mathit{current\\_view}.\mathit{view}\subset v$ and
$\mathit{source}[v]\subseteq\mathit{current\\_view}.\mathit{view}$)$\\}$ and
$\mathit{reconfiguration}.\mathit{destination}=\bot$:

4 $\mathit{reconfiguration}.\mathit{destination}=v$

5 $\mathit{reconfiguration}.\mathit{source}=\mathit{source}[v]$

6 $\mathit{reconfiguration}.\mathit{sequence}=\mathit{sequence}[v]$

7 View_Path $\mathit{path}=\mathit{view\\_path}[v]$

9 if $r\notin\mathit{reconfiguration}.\mathit{destination}$.members():

10 $\mathit{reconfiguration}.\mathit{prepared}=\top$

11 else:

12 $\mathit{state\\_transfer}.\mathit{in\\_progress}=\top$

13 gossip $[$STATE-REQUEST, $\mathit{reconfiguration}.\mathit{source}$,
$\mathit{reconfiguration}.\mathit{sequence}]$ // ask for state

16 if $r\in\mathit{reconfiguration}.\mathit{destination}$.members():

17 $\mathit{reconfiguration}.\mathit{discharged}=\top$

18 else:

19
$\mathit{dischargement}.\mathit{dischargement\\_view}=\mathit{reconfiguration}.\mathit{destination}$

20 gossip $[$DISCHARGEMENT-REQUEST,
$\mathit{reconfiguration}.\mathit{destination}]$

22 wait until $\mathit{reconfiguration}.\mathit{prepared}=\top$ and
$\mathit{reconfiguration}.\mathit{discharged}=\top$

24 // stop the view generator of the previous view

25 if $\mathit{joined}=\top$:

26 trigger <$\mathit{vg}(\mathit{current\\_view}.\mathit{view})$.Stop>

28 if $r\in\mathit{reconfiguration}.\mathit{destination}$.members():

29
$\mathit{current\\_view}.\mathit{view}=\mathit{reconfiguration}.\mathit{destination}$

30 trigger update current view to
$\mathit{reconfiguration}.\mathit{destination}$

31 $\mathit{current\\_view}.\mathit{proof}=\mathit{path}$

32 if $\mathit{joined}=\bot$:

33 $\mathit{joined}=\top$

34 trigger joined // the server joins

36 $\mathit{reconfiguration}.\mathit{source}=\bot$

37 $\mathit{reconfiguration}.\mathit{destination}=\bot$

39 // reset state transfer

40 $\mathit{state\\_transfer}.\mathit{states}[v]=\emptyset$, for every View
$v$

41 $\mathit{state\\_transfer}.\mathit{states\\_from}[v]=\emptyset$, for every
View $v$

43 // reset dischargement

44 $\mathit{dischargement}.\mathit{dischargement\\_view}=\bot$

45 $\mathit{dischargement}.\mathit{dischargements}[v]=\emptyset$, for every
View $v$

47 // reset prepared and discharged

48 $\mathit{reconfiguration}.\mathit{prepared}=\bot$

49 $\mathit{reconfiguration}.\mathit{discharged}=\bot$

51 // reset proposed

52 $\mathit{proposed}=\bot$

54 if $r\notin\mathit{reconfiguration}.\mathit{destination}$.members():

55 trigger left // the server leaves

56 return // we assume that the server executes the special $\mathtt{stop}$
command as soon as it leaves

58 // triggering events for joined servers

59 for each Server
$r\in\mathit{reconfiguration}.\mathit{destination}$.members()$\setminus{\mathit{reconfiguration}.\mathit{source}}$.members():

60 trigger $r$ joined // server $r$ joins

62 // triggering events for left servers

63 for each Server
$r\in\mathit{reconfiguration}.\mathit{source}$.members()$\setminus{\mathit{reconfiguration}.\mathit{destination}}$.members():

64 trigger $r$ left // server $r$ leaves

66 // $\mathit{reconfiguration}.\mathit{sequence}$ has a single element

67 if
$\mathit{reconfiguration}.\mathit{sequence}=\\{\mathit{current\\_view}.\mathit{view}\\}$:

68 $\mathit{current\\_view}.\mathit{installed}=\top$

69 trigger install view $\mathit{current\\_view}.\mathit{view}$ // the server
installs $\mathit{current\\_view}.\mathit{view}$

70 installed($\mathit{genesis}$) // see LABEL:lst:transaction_module

72 if
$\mathit{current\\_view}.\mathit{view}\supset\mathit{stop\\_processing\\_until}$:

73 $\mathit{stop\\_processing\\_until}=\emptyset$

74 $\mathit{current\\_view}.\mathit{processing}=\top$

75 else:

76 $\mathit{current\\_view}.\mathit{processing}=\bot$

77 trigger <$\mathit{vg}(\mathit{current\\_view}.\mathit{view})$.Start | $\bot$>

78 else:

79 View_Generator_Evidence $\epsilon_{\mathit{vg}}$

80
$\epsilon_{\mathit{vg}}.\mathit{path}=\mathit{current\\_view}.\mathit{proof}$

81
$\epsilon_{\mathit{vg}}.\mathit{requests}=\mathit{reconfiguration}.\mathit{requests}$

82
$\epsilon_{\mathit{vg}}.\mathit{voting\\_proofs}=\mathit{reconfiguration}.\mathit{voting\\_proofs}$

83 trigger <$\mathit{vg}(\mathit{current\\_view}.\mathit{view})$.Start | $($min_cardinality($\mathit{current\\_view}.\mathit{proof}$.tail()), $\mathit{current\\_view}.\mathit{proof}$.tail(), $\epsilon_{\mathit{vg}})$>

84 $\mathit{reconfiguration}.\mathit{sequence}=\bot$

Listing 32: Reconfiguration module - view transition

⬇

1Reconfiguration Module:

2 Implementation:

3 upon exists Message $m\in\mathit{waiting\\_messages}$ such that $m=[$STATE-
REQUEST, View $\mathit{source}^{\prime}$, Set(View) $\mathit{set}^{\prime}]$
such that $\mathit{source}^{\prime}\in\mathit{history}$ and $[$INSTALL,
$\mathit{source}^{\prime}$, $\mathit{set}^{\prime}$, Certificate
$\omega^{\prime}]\in\mathit{install\\_messages}$:

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

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

6 if $m$.sender $\in m^{\prime}$.destination().members(): // otherwise, the
message can safely be discarded

7 // the server does not need to have joined

8 if $\mathit{self}\in\mathit{source}^{\prime}$.members() and
($\mathit{current\\_view}.\mathit{view}\subseteq\mathit{source}^{\prime}$ or
$\mathit{current\\_view}.\mathit{view}=\bot$):

9 $\mathit{current\\_view}.\mathit{processing}=\bot$

10 trigger stop processing in view $\mathit{source}^{\prime}$ // the server
stops processing in $\mathit{source}^{\prime}$

11 if $\mathit{source}^{\prime}\supset\mathit{stop\\_processing\\_until}$:

12 $\mathit{stop\\_processing\\_until}=\mathit{source}^{\prime}$

13 // $\mathit{state}$ is a variable defined in LABEL:lst:transaction_module

14 send $[$STATE-UPDATE, $\mathit{source}^{\prime}$, $\mathit{set}^{\prime}$,
$\mathit{state}$, $\mathit{current\\_view.\mathit{view}}]$ to $m$.sender

16 upon exists Message $m\in\mathit{waiting\\_messages}$ such that $m=[$STATE-
UPDATE, View $\mathit{source}^{\prime}$, Set(View) $\mathit{set}^{\prime}$,
State_Representation $\mathit{state}$, View $\mathit{view}]$ such that
$\mathit{source}^{\prime}=\mathit{reconfiguration}.\mathit{source}$ and
$\mathit{set}^{\prime}=\mathit{reconfiguration}.\mathit{sequence}$ and
$\mathit{state}$.verify() $=\top$ and
$\mathit{state\\_transfer}.\mathit{in\\_progress}=\top$:

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

18 Server $r^{\prime}=m$.sender

19 if
$r^{\prime}\notin\mathit{state\\_transfer}.\mathit{states\\_from}[\mathit{view}]$
and $r^{\prime}\in\mathit{view}$.members():

20
$\mathit{state\\_transfer}.\mathit{states}[\mathit{view}]=\mathit{state\\_transfer}.\mathit{states}[\mathit{view}]\cup\\{\mathit{state}\\}$
// store the state

21
$\mathit{state\\_transfer}.\mathit{states\\_messages}[\mathit{view}]=\mathit{state\\_transfer}.\mathit{states\\_messages}[\mathit{view}]\cup\\{m\\}$
// store the sender

22
$\mathit{state\\_transfer}.\mathit{states\\_from}[\mathit{view}]=\mathit{state\\_transfer}.\mathit{states\\_from}[\mathit{view}]\cup\\{r^{\prime}\\}$
// store the sender

24 if
$r^{\prime}\notin\mathit{state\\_transfer}.\mathit{states\\_from}[\mathit{source}^{\prime}]$
and $r^{\prime}\in\mathit{source}^{\prime}$.members():

25
$\mathit{state\\_transfer}.\mathit{states}[.\mathit{source}^{\prime}]=\mathit{state\\_transfer}.\mathit{states}[\mathit{source}^{\prime}]\cup\\{\mathit{state}\\}$
// store the state

26
$\mathit{state\\_transfer}.\mathit{states\\_messages}[\mathit{source}^{\prime}]=\mathit{state\\_transfer}.\mathit{states\\_messages}[\mathit{source}^{\prime}]\cup\\{m\\}$
// store the sender

27
$\mathit{state\\_transfer}.\mathit{states\\_from}[\mathit{source}^{\prime}]=\mathit{state\\_transfer}.\mathit{states\\_from}[\mathit{source}^{\prime}]\cup\\{r^{\prime}\\}$
// store the sender

29 function enough_states_received(View $v$):

30 Set(State_Representation) $\mathit{states}=\emptyset$

31 for each Server $\mathit{rep}\in v$.members():

32 if exists View $\mathit{view}$ such that $\mathit{view}\supseteq v$ and
$\mathit{rep}\in\mathit{state\\_transfer}.\mathit{states\\_from}[\mathit{view}]$:

33 $\mathit{states}=\mathit{states}\cup\\{\mathit{state}\\}$, where
$m=[$STATE-UPDATE, $\mathit{reconfiguration}.\mathit{source}$,
$\mathit{reconfiguration}.\mathit{sequence}$, $\mathit{state}$,
$v]\in\mathit{state\\_transfer}.\mathit{states}[v]$ and $m$.sender
$=\mathit{rep}$

34 if $|\mathit{states}|<v$.plurality():

35 return $\bot$

36 else:

37 return $\mathit{states}$

39 // state received from a quorum of members of
$\mathit{reconfiguration}.\mathit{source}$

40 upon
$|\mathit{state\\_transfer}.\mathit{states\\_from}[\mathit{reconfiguration}.\mathit{source}]|\geq\mathit{reconfiguration}.\mathit{source}$.quorum()
and $\mathit{state\\_transfer}.\mathit{in\\_progress}=\top$:

41 $\mathit{reconfiguration}.\mathit{prepared}=\top$

42 $\mathit{state\\_transfer}.\mathit{in\\_progress}=\bot$

43
refine_state($\mathit{state\\_transfer}.\mathit{states}[\mathit{reconfiguration}.\mathit{source}]$)

45 // state received from at least one correct member of a view ‘‘greater’’
than $\mathit{reconfiguration}.\mathit{source}$

46 upon exists View $v\in\mathit{history}$ such that
$\mathit{reconfiguration}.\mathit{source}\subset v$ and $\mathit{states}=$
enough_states_received($v$) and $\mathit{states}\neq\bot$ and
$\mathit{state\\_transfer}.\mathit{in\\_progress}=\top$:

47 $\mathit{reconfiguration}.\mathit{prepared}=\top$

48 $\mathit{state\\_transfer}.\mathit{in\\_progress}=\bot$

49 refine_state($\mathit{states}$)

Listing 33: Reconfiguration module - state transfer

⬇

1Reconfiguration Module:

2 Implementation:

3 upon exists Message $m\in\mathit{waiting\\_messages}$ such that
$m=[$DISCHARGEMENT-REQUEST, View $v]$ and $\mathit{joined}=\top$ and
$\mathit{current\\_view}.\mathit{view}\supseteq v$:

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

5 send $[$DISCHARGEMENT-CONFIRM, $\mathit{current\\_view}.\mathit{view}]$

7 upon exists Message $m\in\mathit{waiting\\_messages}$ such that
$m=[$DISCHARGEMENT-CONFIRM, View $v]$ and $v\in\mathit{history}$ and
$m$.sender $\in v$.members():

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

9
$\mathit{dischargement}.\mathit{dischargements}[v]=\mathit{dischargement}.\mathit{dischargements}[v]\cup\\{m$.sender$\\}$

11 upon exists View $v$ such that
$\mathit{dischargement}.\mathit{dischargement\\_view}\neq\bot$ and
$v\supseteq\mathit{dischargement}.\mathit{dischargement\\_view}$ and
$|\mathit{dischargement}.\mathit{dischargements}[v]|\geq v$.quorum():

12 $\mathit{reconfiguration}.\mathit{discharged}=\top$

Listing 34: Reconfiguration module - view dischargement

###  6.2. Proof of Correctness

We now prove the properties presented in
LABEL:lst:reconfiguration_properties_new. We start by proving some
intermediate results that play the crucial role in the proof (§ 6.2.1).

####  6.2.1. Intermediate Results

First, we show that a correct server that updates its
$\mathit{current\\_view}.\mathit{view}$ variable to $v$ has $v$ in its
$\mathit{history}$ variable.

###### Lemma 0.

Let $\mathit{current\\_view}.\mathit{view}=v$ at a correct server $r$ at time
$t$. Then, $v\in\mathit{history}$ at server $r$ at time $t$.

###### Proof.

If $v=\mathit{genesis}$, the lemma follows from line 6 of
LABEL:lst:storage_initialization and the fact that no view is ever removed
from the $\mathit{history}$ variable of a correct server.

Let $v\neq\mathit{genesis}$. Since $\mathit{current\\_view}.\mathit{view}=v$
at server $r$ at time $t$ and $v\neq\mathit{genesis}$, we know that line 29 of
LABEL:lst:reconfiguration_view_transition is executed by $r$ at time
$t_{v}\leq t$. Hence, $\mathit{reconfiguration}.\mathit{destination}=v$ at
time $t_{v}$. Moreover, $v\in\mathit{history}$ at time $t_{v}$ at server $r$
(by line 3 of LABEL:lst:reconfiguration_view_transition and the fact that no
view is ever removed from the $\mathit{history}$ variable of a correct
server). Therefore, the lemma holds in this case, as well. ∎

Next, we show that, if $v\in\mathit{history}$ at a correct server, then the
server has previously obtained a view-path to $v$.

###### Lemma 0.

Let $v\in\mathit{history}$ at a correct server $r$ at time $t$, where
$v\neq\mathit{genesis}$. Then, there exists a view-path
$\mathit{path}=[m_{1},...,m_{k}]$ such that (1)
$\mathit{path}.\mathtt{destination}()=v$, and (2)
$m_{i}\in\mathit{install\\_messages}$ at server $r$ at time $t$, for every
$i\in[1,k]$.

###### Proof.

In order to prove the lemma, we show that, if, at any point in time,
$v^{*}\in\mathit{history}$ at a correct server $r$, then $r$ has previously
obtained a view-path to $v^{*}$ (and the view-path consists of messages from
the $\mathit{install\\_messages}$ variable). Note that no message is ever
removed from the $\mathit{install\\_messages}$ variable of a correct server.
We set the following invariant to hold at time $t^{*}\geq 0$: If
$v^{*}\in\mathit{history}$ at time $t^{*}$, then $r$ has previously included a
view-path to $v^{*}$ in $\mathit{install\\_messages}$. Observe that the
invariant holds initially (i.e., at the time the server starts) since
$\mathit{history}=\\{\mathit{genesis}\\}$ (line 6 of
LABEL:lst:storage_initialization) and $\mathit{install\\_messages}=\emptyset$
(line 7 of LABEL:lst:storage_initialization).

We now prove that the invariant is preserved once the $\mathit{history}$
variable at server $r$ is updated with a view $v^{**}$. The only place in
which the $\mathit{history}$ variable can be modified is line 11 of
LABEL:lst:storage_processing. Since $v\in\mathit{history}$ (by line 6 of
LABEL:lst:storage_processing), we know that there exists a view-path to $v$,
which is previously obtained and included in $\mathit{install\\_messages}$
(because of the invariant hypothesis). Hence, there is a view-path to $v^{**}$
since the received $\mathtt{INSTALL}$ message is included in
$\mathit{install\\_messages}$ (line 8 of LABEL:lst:storage_processing). Thus,
the lemma holds. ∎

Lemma 5 proves that any view $v$ that belongs to the $\mathit{history}$
variable of a correct server is valid.

###### Lemma 0.

Let $v\in\mathit{history}$ at a correct server. Then, $v$ is a valid view.

###### Proof.

If $v=\mathit{genesis}$, Definition 1 is satisfied for $v$. Otherwise,
Definition 1 holds for $v$ because of Lemma 4. ∎

Finally, we show that correct servers “transit” only to valid views, i.e., if
$\mathit{current\\_view}.\mathit{view}=v$ at a correct server, then $v$ is a
valid view.

###### Lemma 0.

Let $\mathit{current\\_view}.\mathit{view}=v$ at a correct server $r$ at some
time $t\geq 0$. Then, $v$ is a valid view.

###### Proof.

We know that $v\in\mathit{history}$ at server $r$ (by Lemma 3). Hence, $v$ is
valid by Lemma 5. ∎

We now give a brief explanation of the upcoming steps in proving the
properties from LABEL:lst:reconfiguration_properties_new.

##### Explanation.

We fix some time $t$ in an execution of Carbon. At time $t$, we observe all
$\mathtt{INSTALL}$ messages obtained by (correct or faulty) processes. Then,
we introduce a set of invariants concerned with all obtained
$\mathtt{INSTALL}$ messages (this set of invariants is satisfied at time $0$).
The introduced invariants allow us to identify all possible “new”
$\mathtt{INSTALL}$ messages that can be obtained after time $t$. Finally, we
prove that the invariants are preserved after such $\mathtt{INSTALL}$ messages
are indeed obtained by processes after time $t$.

Fix a time $t\geq 0$ in an execution. Let $\mathcal{I}_{p}(t)$ denote all
$\mathtt{INSTALL}$ messages obtained by a (correct or faulty) process $p$ by
time $t$; note that obtaining of an $\mathtt{INSTALL}$ message is irrevocable,
i.e., $\mathcal{I}_{p}(t^{\prime})\subseteq\mathcal{I}_{p}(t)$, for any time
$t^{\prime}\leq t$. Moreover, $\mathcal{I}_{p}(0)=\emptyset$, for every
process $p$. Let
$\mathcal{I}^{*}(t)=\bigcup\limits_{p\in\mathcal{C}\cup\mathcal{R}}\mathcal{I}_{p}(t)$.
Observe that $\mathcal{I}^{*}(t^{\prime})\subseteq\mathcal{I}^{*}(t)$, for any
time $t^{\prime}<t$.

We say that a view $v$ is _well-founded_ at time $t$ if and only if:

  * •

$v=\mathit{genesis}$, or

  * •

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

Now, we prove that, if a process has obtained an $\mathtt{INSTALL}$ message
(see LABEL:lst:install_messages) associated with a view $\mathit{source}$ by
time $t$ and $\mathit{source}$ is not well-founded at time $t$, then
$\mathit{source}$ is not a valid view.

###### Lemma 0.

Let a (correct or faulty) process obtain
$m=[\mathtt{INSTALL},\mathit{source},\mathit{set},\omega]$ at some time $t>0$.
Moreover, let $\mathit{source}$ not be well-founded at time $t-1$. Then,
$\mathit{source}$ is not a valid view.

###### Proof.

Note that $\mathit{source}\neq\mathit{genesis}$, since $\mathit{genesis}$ is
well-founded at any time. We prove the lemma by contradiction. Hence, let
$\mathit{source}$ be a valid view.

Since $\mathit{source}$ is a valid view, that means that (at least) a quorum
of members of $\mathit{source}$ are correct (by the failure model). Moreover,
we know that $\mathit{set}$ is committed by $\mathit{vg}(\mathit{source})$ (by
LABEL:lst:install_messages). Because of the fact that $\omega$ contains
messages from at least $\mathit{source}.\mathtt{quorum()}$ distinct members of
$\mathit{source}$ (see LABEL:lst:verify_output_vg), there exists a correct
server $r$ that sets its $\mathit{current\\_view}.\mathit{view}$ variable to
$\mathit{source}$ before time $t$ at line 29 of
LABEL:lst:reconfiguration_view_transition (since
$\mathit{source}\neq\mathit{genesis}$ and $\mathit{vg}(\mathit{source})$ is
started by $r$, which follows from the decision permission property of
$\mathit{vg}(\mathit{source})$). By Lemma 3,
$\mathit{source}\in\mathit{history}$ before time $t$. Furthermore, Lemma 4
shows that $r$ has obtained a view-path to $\mathit{source}$ before time $t$.
Therefore, $\mathit{source}$ is well-founded at time $t-1$, which implies
contradiction. ∎

Finally, we introduce a few concepts that describe the state of the system at
some fixed time $t$. First, we denote by $V(t)$ the set of well-founded views
at time $t$, i.e., $V(t)=\\{v\,|\,v\text{ is well-founded at time }t\\}$.

For every view $v\in V(t)$, we define a logical predicate $\alpha_{t}(v)$ such
that $\alpha_{t}(v)=\top$ if and only of:

  * •

$v=\mathit{genesis}$, or

  * •

$[\mathtt{INSTALL},v^{\prime},\\{v\\},\omega]\in\mathcal{I}^{*}(t)$, where
$v^{\prime}\in V(t)$; in other words, $m\in\mathcal{I}^{*}(t)$, where
$m.\mathtt{source()}\in V(t)$, $m.\mathtt{destination()}=v$ and
$m.\mathtt{tail()}=\emptyset$.

Otherwise, $\alpha_{t}(v)=\bot$. If $\alpha_{t}(v)=\top$, we say that $v$ is
_installable_ at time $t$.

Moreover, for every view $v\in V(t)$, we define $\beta_{t}(v)$ such that
$\mathit{set}\in\beta_{t}(v)$ if and only if
$m=[\mathtt{INSTALL},v^{\prime},\mathit{set}^{\prime}=\\{v\\}\cup\mathit{set},\omega]\in\mathcal{I}^{*}(t)$,
where $v^{\prime}\in V(t)$, $m.\mathtt{destination()}=v$, and
$\mathit{set}\neq\emptyset$; in other words, $m\in\mathcal{I}^{*}(t)$, where
$m.\mathtt{source()}\in V(t)$, $m.\mathtt{destination()}=v$ and
$m.\mathtt{tail()}=\mathit{set}\neq\emptyset$. Otherwise,
$\beta_{t}(v)=\emptyset$.

Finally, for every view $v\in V(t)$, we define $\rho_{t}(v)$ such that
$\mathit{set}\in\rho_{t}(v)$ if and only if
$[\mathtt{INSTALL},v,\mathit{set},\omega]\in\mathcal{I}^{*}(t)$.

First, we prove that every view $v\in V(t)$ is valid.

###### Lemma 0.

Let $v\in V(t)$. Then, $v$ is a valid view.

###### Proof.

Follows from the definition of well-founded views and Definition 1. ∎

We now introduce the first invariant.

###### Invariant 1.

Let $v\in V(t)$. If $\mathit{set}\in\rho_{t}(v)$, then (1)
$\mathit{set}\neq\emptyset$, (2) $\mathit{set}$ is a sequence, and (3)
$\mathit{set}.\mathtt{follows}(v)=\top$.

Since $\mathcal{I}^{*}(0)=\emptyset$, we conclude that
$V(0)=\\{\mathit{genesis}\\}$ and Invariant 1 holds at time $0$. Now, we show
that any information obtained by a process by time $t$ is captured in $V(t)$,
$\rho_{t}$ and $\beta_{t}$.

###### Lemma 0.

Let a (correct or faulty) process $p$ obtain a view-path
$\mathit{path}=[m_{1},m_{2},...,m_{k}]$ by time $t$, where $k\geq 1$. Then,
the following holds:

  * •

$\mathit{path}.\mathtt{views}()\subseteq V(t)$;

  * •

Let $\mathit{destination}=\mathit{path}.\mathtt{destination}()$. If
$\mathit{path}.\mathtt{tail}()\neq\emptyset$, then
$\mathit{path}.\mathtt{tail}()\in\beta_{t}(\mathit{destination})$.

###### Proof.

Since $p$ obtains $\mathit{path}$ by time $t$, we conclude that
$m_{i}\in\mathcal{I}^{*}(t)$, for every $i\in[1,k]$. We know that
$\mathit{genesis}\in V(t)$, by the definition of well-founded views. All other
views that belong to $\mathit{path}.\mathtt{views}()$, therefore, are included
in $V(t)$ (including $\mathit{destination}$ and $m_{k}.\mathtt{source}()$).
Hence, if $\mathit{path}.\mathtt{tail}()\neq\emptyset$, then
$\mathit{path}.\mathtt{tail}()\in\beta_{t}(\mathit{destination})$. ∎

Next, we show that any two sets that belong to $\rho_{t}(v)$, where $v\in
V(t)$, are “comparable”.

###### Lemma 0.

Let $v\in V(t)$ and let $\mathit{set}_{1},\mathit{set}_{2}\in\rho_{t}(v)$.
Then, either $\mathit{set}_{1}\subseteq\mathit{set}_{2}$ or
$\mathit{set}_{1}\supset\mathit{set}_{2}$.

###### Proof.

Since $v\in V(t)$, we know that $v$ is a valid view (by Lemma 8). Moreover, we
know that $\mathit{set}_{1}$ and $\mathit{set}_{2}$ are committed by
$\mathit{vg}(v)$ (by LABEL:lst:install_messages). Hence, the lemma follows
from the comparability property of $\mathit{vg}(v)$. ∎

We now define an invariant that explains how installable views are
“instantiated”.

###### Invariant 2 (Creation of Installable Views).

For every $v\in V(t)$ such that (1) $\alpha_{t}(v)=\top$, and (2)
$v\neq\mathit{genesis}$, there exists a view $v^{\prime}\in V(t)$ such that:

  * •

$\alpha_{t}(v^{\prime})=\top$, and

  * •

$\mathit{seq}\in\rho_{t}(v^{\prime})$, where $\mathit{seq}=v_{1}\to...\to
v_{x}\to v,(x\geq 0)$101010Recall that all sets that belong to $\rho_{t}(v)$,
for any view $v\in V(t)$, are sequences (by Invariant 1)., and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$, $v_{i}\in V(t)$ and
$\alpha_{t}(v_{i})=\bot$, and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$,
$\mathit{seq}_{i}\in\rho_{t}(v_{i})$, where $\mathit{seq}_{i}=v_{i+1}\to...\to
v_{x}\to v$.

Note that Invariant 2 is satisfied at time $0$ since
$V(0)=\\{\mathit{genesis}\\}$. Next, we define what it means for a view to
_lead_ to another view.

###### Definition 0 (Leading to a View).

Consider views $v,v^{\prime}\in V(t)$ such that:

  * •

$\alpha_{t}(v)=\alpha_{t}(v^{\prime})=\top$, and

  * •

$\mathit{seq}\in\rho_{t}(v^{\prime})$, where $\mathit{seq}=v_{1}\to...\to
v_{x}\to v,(x\geq 0)$, and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$, $v_{i}\in V(t)$ and
$\alpha_{t}(v_{i})=\bot$, and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$,
$\mathit{seq}_{i}\in\rho_{t}(v_{i})$, where $\mathit{seq}_{i}=v_{i+1}\to...\to
v_{x}\to v$.

We say that $v^{\prime}$ _leads to_ $v$ at time $t$.

We now show that $v^{\prime}\subset v$ if $v^{\prime}$ leads to $v$.

###### Lemma 0.

Let $v^{\prime}\in V(t)$ lead to $v\in V(t)$ at time $t$. Then,
$v^{\prime}\subset v$.

###### Proof.

By Definition 11, $\mathit{seq}\in\rho_{t}(v^{\prime})$, where
$\mathit{seq}=...\to v$. Since
$\mathit{seq}.\mathtt{follows}(v^{\prime})=\top$ (by Invariant 1), the lemma
holds. ∎

Now, we introduce another invariant that we assume holds at time $t$:
$\mathit{genesis}$ is a subset of every other installable view.

###### Invariant 3.

For every view $v\in V(t)$ such that (1) $\alpha_{t}(v)=\top$, and (2)
$v\neq\mathit{genesis}$, $\mathit{genesis}\subset v$.

Invariant 3 holds at time $0$ since $V(0)=\\{\mathit{genesis}\\}$. Now, we
show that, for every installable view different from $\mathit{genesis}$, there
exists a view that leads to it at time $t$ (follows directly from Invariant
2).

###### Lemma 0.

Let $v^{\prime}\in V(t)$ such that (1) $\alpha_{t}(v^{\prime})=\top$, and (2)
$v^{\prime}\neq\mathit{genesis}$. Then, there exists a view $v\in V(t)$ such
that $v$ leads to $v^{\prime}$ at time $t$.

###### Proof.

According to Invariant 2, there exists a view $v\in V(t)$ such that:

  * •

$\alpha_{t}(v)=\top$, and

  * •

$\mathit{seq}\in\rho_{t}(v)$, where $\mathit{seq}=v_{1}\to...\to v_{x}\to
v^{\prime},(x\geq 0)$, and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$, $v_{i}\in V(t)$ and
$\alpha_{t}(v_{i})=\bot$, and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$,
$\mathit{seq}_{i}\in\rho_{t}(v_{i})$, where $\mathit{seq}_{i}=v_{i+1}\to...\to
v_{x}\to v^{\prime}$.

By Definition 11, $v$ leads to $v^{\prime}$ at time $t$, which concludes the
proof. ∎

We now prove that no view leads to $\mathit{genesis}$ at time $t$.

###### Lemma 0.

No view $v\in V(t)$ leads to $\mathit{genesis}$ at time $t$.

###### Proof.

We prove the lemma by contradiction. Let there exist a view $v\in V(t)$ such
that $v$ leads to $\mathit{genesis}$ at time $t$. By Lemma 12,
$v\subset\mathit{genesis}$. However, this contradicts Invariant 3, which
concludes the proof. ∎

A view can lead to (at most) one other view. The following lemma proves this
statement.

###### Lemma 0.

Let $v\in V(t)$ such that $\alpha_{t}(v)=\top$. If $v$ leads to $v^{\prime}\in
V(t)$ at time $t$ and $v$ leads to $v^{\prime\prime}\in V(t)$ at time $t$,
then $v^{\prime}=v^{\prime\prime}$.

###### Proof.

According to Definition 11, $\mathit{seq}^{\prime}\in\rho_{t}(v)$, where
$\mathit{seq}^{\prime}$ is a sequence (by Invariant 1) and
$\mathit{seq}^{\prime}=...\to v^{\prime}$. Similarly,
$\mathit{seq}^{\prime\prime}\in\rho_{t}(v)$, where
$\mathit{seq}^{\prime\prime}$ is a sequence (by Invariant 1) and
$\mathit{seq}^{\prime\prime}=...\to v^{\prime\prime}$. According to Lemma 10,
either $\mathit{seq}^{\prime}\subseteq\mathit{seq}^{\prime\prime}$ or
$\mathit{seq}^{\prime}\supset\mathit{seq}^{\prime\prime}$. Let us analyze two
possible cases:

  * •

$\mathit{seq}^{\prime}=\mathit{seq}^{\prime\prime}$: In this case, we have
that $v^{\prime}=v^{\prime\prime}$ and the lemma holds.

  * •

$\mathit{seq}^{\prime}\neq\mathit{seq}^{\prime\prime}$: Without loss of
generality, let $\mathit{seq}^{\prime}\subset\mathit{seq}^{\prime\prime}$.
Therefore, $v^{\prime}\in\mathit{seq}^{\prime\prime}$ and $v^{\prime}\subseteq
v^{\prime\prime}$. If $v^{\prime}\subset v^{\prime\prime}$, Definition 11 is
not satisfied for $v^{\prime\prime}$ (since $\alpha_{t}(v^{\prime})=\top$).
Hence, $v^{\prime}=v^{\prime\prime}$.

The lemma holds. ∎

Now, we prove that there exists exactly one view that does not lead to any
view. Recall that we assume that only finitely many valid views exist (see §
6, paragraph “Failure model & assumptions”). Since all views that belong to
$V(t)$ are valid (by Lemma 8), we conclude that $|V(t)|<\infty$.

###### Lemma 0.

There exists _exactly_ one view $v\in V(t)$ such that (1)
$\alpha_{t}(v)=\top$, and (2) $v$ does not lead to any view at time $t$.

###### Proof.

Let there be $x$ installable views at time $t$. Because of lemmas 13 and 14,
we conclude that _exactly_ $x-1$ installable views (all installable views
except $\mathit{genesis}$; $\mathit{genesis}$ is installable at any time) have
views that lead to them at time $t$. According to Lemma 15, each installable
view leads to at most one view at time $t$. Hence, at least $x-1$ views lead
to a view at time $t$.

In order to prove the lemma, it is sufficient to show that it is impossible
for all $x$ installable views to lead to some view at time $t$. We prove this
statement by contradiction.

Let $\mathcal{I}\mathcal{N}\mathcal{S}$ denote the set of all installable
views at time $t$; note that $|\mathcal{I}\mathcal{N}\mathcal{S}|<\infty$
(since $|V(t)|<\infty$ and $\mathcal{I}\mathcal{N}\mathcal{S}\subseteq V(t)$).
Consider the following construction:

  1. (1)

Start with $V\leftarrow\\{\mathit{genesis}\\}$,
$\mathit{last}\leftarrow\mathit{genesis}$ and
$R\leftarrow\mathcal{I}\mathcal{N}\mathcal{S}\setminus\\{\mathit{genesis}\\}$.

  2. (2)

Repeat until $V\neq\mathcal{I}\mathcal{N}\mathcal{S}$:

    1. (a)

Select a view $v\in\mathcal{I}\mathcal{N}\mathcal{S}$ such that
$\mathit{last}$ leads to $v$ at time $t$.

    2. (b)

Update $V\leftarrow V\cup\\{v\\}$, $\mathit{last}\leftarrow v$ and
$R\leftarrow R\setminus\\{v\\}$.

    3. (c)

If $V\neq\mathcal{I}\mathcal{N}\mathcal{S}$, go to step 2.

    4. (d)

Otherwise, select a view $v\in\mathcal{I}\mathcal{N}\mathcal{S}$ such that
$\mathit{last}$ leads to $v$ at time $t$.

Note that $V$ represents a sequence (because of the construction and Lemma
12). Hence, $\mathit{last}$ represents the greatest (with respect to the
containment relation) element of $V$. Therefore, a view $v$, where
$\mathit{last}$ leads to $v$ at time $t$, must belong to $R$ (otherwise, we
would contradict Lemma 12). Thus, the $V$ set is constantly “growing” and the
$R$ set is constantly “shrinking”.

Once $V=\mathcal{I}\mathcal{N}\mathcal{S}$ in step 2(c), we conclude that
$R=\emptyset$. Hence, $\mathit{last}$ cannot lead to any view. Thus, we reach
contradiction with the fact that $\mathit{last}$ leads to a view, which
concludes the proof. ∎

The next lemma shows that at most one view can lead to a view $v$ at time $t$.

###### Lemma 0.

Let $v\in V(t)$ such that $\alpha_{t}(v)=\top$. If $v^{\prime}\in V(t)$ leads
to $v$ at time $t$ and $v^{\prime\prime}\in V(t)$ leads to $v$ at time $t$,
then $v^{\prime}=v^{\prime\prime}$.

###### Proof.

Let there be $x$ installable views at time $t$. Because of lemmas 13 and 14,
we conclude that exactly $x-1$ installable views (all installable views except
$\mathit{genesis}$) have views that lead to them. According to Lemma 15, each
view leads to at most one view. Lemma 16 shows that there exists an
installable view that does not lead to any view at time $t$. Hence, there are
exactly $x-1$ installable views and exactly $x-1$ “lead-to” relations. Thus,
only one view leads to $v$ at time $t$ and the lemma holds. ∎

Finally, we show that all installable views are comparable.

###### Lemma 0.

Let $v,v^{\prime}\in V(t)$ such that
$\alpha_{t}(v)=\alpha_{t}(v^{\prime})=\top$. Then, either $v\subseteq
v^{\prime}$ or $v\supset v^{\prime}$.

###### Proof.

Let $\mathcal{I}\mathcal{N}\mathcal{S}$ denote the set of all installable
views at time $t$. In order to prove the lemma, we prove that
$\mathcal{I}\mathcal{N}\mathcal{S}$ is a sequence. Let
$x=|\mathcal{I}\mathcal{N}\mathcal{S}|<\infty$. According to Lemma 16, exactly
$x-1$ installable views lead to some view at time $t$.

Consider the construction similar to the one from the proof of Lemma 16:

  1. (1)

Start with $V\leftarrow\\{\mathit{genesis}\\}$ and
$\mathit{last}\leftarrow\mathit{genesis}$.

  2. (2)

Repeat until $\mathit{last}$ does not lead to any view at time $t$:

    1. (a)

Select a view $v\in\mathcal{I}\mathcal{N}\mathcal{S}$ such that
$\mathit{last}$ leads to $v$ at time $t$.

    2. (b)

Update $V\leftarrow V\cup\\{v\\}$ and $\mathit{last}\leftarrow v$.

Because of the construction and Lemma 12, $V$ is a sequence. In order to
conclude the lemma, it suffices to prove that
$V=\mathcal{I}\mathcal{N}\mathcal{S}$. We prove this statement by
contradiction.

Suppose that $V\neq\mathcal{I}\mathcal{N}\mathcal{S}$. Because of the
construction, we know that $V\subset\mathcal{I}\mathcal{N}\mathcal{S}$. Let
$|V|=p<x$. This means that there exist $x-p$ views in
$R=\mathcal{I}\mathcal{N}\mathcal{S}\setminus{V}$. The following holds for
each view $v\in R$:

  * •

$v$ leads to a view $v^{\prime}\in\mathcal{I}\mathcal{N}\mathcal{S}$ at time
$t$: This statement holds because $x-1$ installable views lead to some view at
time $t$ (by Lemma 16). By construction, we have that $p-1$ views of $V$ lead
to some view at time $t$. Given that $|R|=x-p$ and $x-1-(p-1)=x-p$, the
statement is true.

  * •

$v$ leads to a view $v^{\prime}\in R$ at time $t$: Suppose that $v$ leads to a
view $v^{\prime}\in V$ at time $t$. If $v^{\prime}=\mathit{genesis}$, Lemma 14
is contradicted. If $v^{\prime}\neq\mathit{genesis}$, Lemma 17 is contradicted
(since $v^{\prime}$ has more than one view leading to it). Thus, the statement
is correct.

Finally, we model the set $R$ with a graph $G$ with $x-p$ vertices ($x-p$
installable views) and $x-p$ edges ($x-p$ “lead-to” relations). Thus, $G$ has
a cycle. However, that is not possible given Lemma 12. Hence,
$V=\mathcal{I}\mathcal{N}\mathcal{S}$ and the lemma holds. ∎

The next lemma proves that only the greatest installable view at time $t$ does
not lead to any view at time $t$. Recall that all installable views are
comparable (by Lemma 18).

###### Lemma 0.

A view $v\in V(t)$, where $\alpha_{t}(v)=\top$, does not lead to any view at
time $t$ if and only if $v$ is the greatest installable view at time $t$.

###### Proof.

We prove the lemma by proving both directions of the statement.

Let $v$ be the view that does not lead to any view at time $t$; such view
exists due to Lemma 16. By contradiction, suppose that $v$ is not the greatest
installable view at time $t$. Let $v_{\mathit{max}}$ be the greatest
installable view at time $t$. According to Lemma 16, $v_{\mathit{max}}$ leads
to some view $v^{\prime}$ at time $t$. By Lemma 12, we have that
$v_{\mathit{max}}\subset v^{\prime}$, which contradicts the fact that
$v_{\mathit{max}}$ is the greatest installable view at time $t$. Thus, the
lemma holds in this direction.

Suppose that $v$ is the greatest installable view at time $t$ and that, by
contradiction, it leads to a view $v^{\prime}\in V(t)$ at time $t$. According
to Lemma 12, $v\subset v^{\prime}$. This is contradiction with the fact that
$v$ is the greatest installable view at time $t$. The lemma holds in this
direction, as well. ∎

Now, we introduce an invariant that explains how non-installable views are
“instantiated”.

###### Invariant 4 (Creation of Non-Installable Views).

For every $v\in V(t)$ such that $\alpha_{t}(v)=\bot$, there exists a view
$v^{\prime}\in V(t)$ such that:

  * •

$\alpha_{t}(v^{\prime})=\top$, and

  * •

$\mathit{seq}\in\rho_{t}(v^{\prime})$, where $\mathit{seq}=v_{1}\to...\to
v_{x}\to v\to v_{1}^{\prime}\to...\to v_{y}^{\prime},(x\geq 0,y\geq 1)$, and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$, $v_{i}\in V(t)$ and
$\alpha_{t}(v_{i})=\bot$, and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$,
$\mathit{seq}_{i}\in\rho_{t}(v_{i})$, where $\mathit{seq}_{i}=v_{i+1}\to...\to
v_{x}\to v\to v_{1}^{\prime}\to...\to v_{y}^{\prime}$.

Invariant 4 holds at time $0$ since $V(0)=\\{\mathit{genesis}\\}$ and
$\alpha_{0}(\mathit{genesis})=\top$. Next, we define _auxiliary views_.

###### Definition 0 (Auxiliary View).

Consider views $v,v^{\prime}\in V(t)$ such that:

  * •

$\alpha_{t}(v^{\prime})=\top$, and

  * •

$\alpha_{t}(v)=\bot$, and

  * •

$\mathit{seq}\in\rho_{t}(v^{\prime})$, where $\mathit{seq}=v_{1}\to...\to
v_{x}\to v\to v_{1}^{\prime}\to...\to v_{y}^{\prime},(x\geq 0,y\geq 1)$, and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$, $v_{i}\in V(t)$ and
$\alpha_{t}(v_{i})=\bot$, and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$,
$\mathit{seq}_{i}\in\rho_{t}(v_{i})$, where $\mathit{seq}_{i}=v_{i+1}\to...\to
v_{x}\to v\to v_{1}^{\prime}\to...\to v_{y}^{\prime}$.

We say that $v$ is an _auxiliary view_ for $v^{\prime}$ at time $t$.

The following lemma shows that any non-installable view is an auxiliary view
for some installable view.

###### Lemma 0.

Let $v\in V(t)$ such that $\alpha_{t}(v)=\bot$. Then, $v$ is an auxiliary view
for a view $v^{\prime}\in V(t)$ at time $t$.

###### Proof.

The lemma follows from Invariant 4 and Definition 20. ∎

If $v$ is an auxiliary view for $v^{\prime}$ at time $t$, then
$v^{\prime}\subset v$. The following lemma proves this claim.

###### Lemma 0.

Let $v\in V(t)$ be an auxiliary view for a view $v^{\prime}\in V(t)$ at time
$t$. Then, $v^{\prime}\subset v$.

###### Proof.

According to Definition 20, $\mathit{seq}\in\rho_{t}(v^{\prime})$, where
$\mathit{seq}=...\to v\to v_{1}^{\prime}\to...\to v_{y}^{\prime},(y\geq 1)$.
By Invariant 1, we know that $\mathit{seq}.\mathtt{follows}(v^{\prime})=\top$,
which implies that $v^{\prime}\subset v$. ∎

If $v$ is an auxiliary view for a view $v^{\prime}$ and $v^{\prime}$ leads to
a view $v^{\prime\prime}$, then $v\subset v^{\prime\prime}$.

###### Lemma 0.

Let $v\in V(t)$ be an auxiliary view for a view $v^{\prime}\in V(t)$ at time
$t$. Let $v^{\prime}$ lead to $v^{\prime\prime}\in V(t)$ at time $t$. Then,
$v\subset v^{\prime\prime}$.

###### Proof.

According to Definition 20, $\mathit{seq}\in\rho_{t}(v^{\prime})$, where
$\mathit{seq}=...\to v\to v_{1}^{\prime}\to...\to v_{y}^{\prime},(y\geq 1)$.
By Definition 11, $\mathit{seq}^{\prime\prime}\in\rho_{t}(v^{\prime})$, where
$\mathit{seq}^{\prime\prime}=...\to v^{\prime\prime}$. Invariant 1 ensures
that (1) $\mathit{seq}$ and $\mathit{seq}^{\prime\prime}$ are sequences, and
(2)
$\mathit{seq}.\mathtt{follows}(v^{\prime})=\mathit{seq}^{\prime\prime}.\mathtt{follows}(v^{\prime})=\top$.
By Lemma 10, there are three possible scenarios:

  * •

$\mathit{seq}=\mathit{seq}^{\prime\prime}$: In this case, we have that
$v\subset v^{\prime\prime}$. The lemma holds.

  * •

$\mathit{seq}\subset\mathit{seq}^{\prime\prime}$: In this case, we know that
$v\in\mathit{seq}^{\prime\prime}$. Thus, $v\subset v^{\prime\prime}$ and the
lemma holds.

  * •

$\mathit{seq}\supset\mathit{seq}^{\prime\prime}$: Hence,
$v^{\prime\prime}\in\mathit{seq}$. We conclude that $v\subset
v^{\prime\prime}$ because, otherwise, either (1) $\alpha_{t}(v)=\top$ (if
$v=v^{\prime\prime}$), or (2) $v$ is not an auxiliary view for $v^{\prime}$ at
time $t$ since $\alpha_{t}(v^{\prime\prime})=\top$ (if
$v^{\prime\prime}\subset v$).

The lemma holds since the claim is correct in all possible cases. ∎

The following lemma shows that if $v$ leads to $v^{\prime}$, then there does
not exist an installable view $v^{\prime\prime}$ such that $v\subset
v^{\prime\prime}\subset v^{\prime}$.

###### Lemma 0.

Let $v\in V(t)$ lead to $v^{\prime}\in V(t)$ at time $t$. There does not exist
a view $v^{\prime\prime}\in V(t)$ such that (1)
$\alpha_{t}(v^{\prime\prime})=\top$, and (2) $v\subset v^{\prime\prime}\subset
v^{\prime}$.

###### Proof.

Let $\mathcal{I}\mathcal{N}\mathcal{S}=\\{v\,|\,v\in
V(t)\land\alpha_{t}(v)=\top\\}$. According to Lemma 18,
$\mathcal{I}\mathcal{N}\mathcal{S}$ is a sequence. Moreover,
$|\mathcal{I}\mathcal{N}\mathcal{S}|<\infty$.

We prove the lemma by contradiction. Hence, suppose that there exists a view
$v^{\prime\prime}$ such that (1)
$v^{\prime\prime}\in\mathcal{I}\mathcal{N}\mathcal{S}$, and (2) $v\subset
v^{\prime\prime}\subset v^{\prime}$.

Since $v$ leads to $v^{\prime}$ at time $t$, we know that $v\subset
v^{\prime}$ (by Lemma 12). We consider the following construction:

  1. (1)

Start with $V\leftarrow\\{v,v^{\prime}\\}$ and $\mathit{first}\leftarrow v$.

  2. (2)

Repeat until $\mathit{first}=\mathit{genesis}$:

    1. (a)

Select a view $v_{i}\in\mathcal{I}\mathcal{N}\mathcal{S}$ such that $v_{i}$
leads to $\mathit{first}$.

    2. (b)

Update $V\leftarrow V\cup\\{v_{i}\\}$ and $\mathit{first}\leftarrow v_{i}$.

According to the construction and Lemma 12, $V$ is a sequence. Moreover,
$\mathit{first}$ represents the first (i.e., smallest) view of $V$. Therefore,
a view $v_{i}$, where $v_{i}$ leads to $\mathit{first}$, must belong to
$\mathcal{I}\mathcal{N}\mathcal{S}\setminus{V}$ (otherwise, we would
contradict Lemma 12). Thus, $V$ is “growing” with each iteration. Finally, an
execution of the construction eventually terminates since (1)
$|\mathcal{I}\mathcal{N}\mathcal{S}|<\infty$, (2) Lemma 13 holds, (3) Lemma 14
stands, and (4) $\mathit{genesis}\in\mathcal{I}\mathcal{N}\mathcal{S}$.

Since $v\subset v^{\prime\prime}$, we conclude that $v^{\prime\prime}\notin V$
and $v^{\prime\prime}\neq\mathit{genesis}$. Therefore, there exists a view
that leads to $v^{\prime\prime}$ (by Lemma 13). Let
$R=\mathcal{I}\mathcal{N}\mathcal{S}\setminus{V}$. Hence, $v^{\prime\prime}\in
R$. Now, we consider the following construction:

  1. (1)

Start with $V^{\prime}\leftarrow\\{v^{\prime\prime}\\}$ and
$\mathit{first}\leftarrow v^{\prime\prime}$.

  2. (2)

Select a view $v_{i}\in\mathcal{I}\mathcal{N}\mathcal{S}$ such that $v_{i}$
leads to $\mathit{first}$.

  3. (3)

If $v_{i}\in V$, then terminate.

  4. (4)

Update $V^{\prime}\leftarrow V^{\prime}\cup\\{v_{i}\\}$ and
$\mathit{first}\leftarrow v_{i}$.

  5. (5)

Go to step 2.

By construction and Lemma 12, $V^{\prime}$ is a sequence. Hence, for every
view $\mathit{view}\in V^{\prime}$, $\mathit{view}\subseteq v^{\prime\prime}$.
Importantly, an execution of this construction eventually terminates because
(1) $|\mathcal{I}\mathcal{N}\mathcal{S}|<\infty$, (2) Lemma 13, (3) Lemma 14,
and (4) $\mathit{genesis}\in V$. Thus, once the execution terminates, we
either contradict Lemma 12 (if $v_{i}=v^{\prime}$; since
$\mathit{view}\subseteq v^{\prime\prime}$, for every $\mathit{view}\in
V^{\prime}$) or Lemma 15 (if $v_{i}\neq v^{\prime}$). Therefore, the lemma
holds. ∎

Now, we prove that a view can be an auxiliary view for a single installable
view.

###### Lemma 0.

Let $v\in V(t)$ be an auxiliary view for a view $v^{\prime}\in V(t)$ at time
$t$. Moreover, let $v$ be an auxiliary view for a view $v^{\prime\prime}\in
V(t)$ at time $t$. Then, $v^{\prime}=v^{\prime\prime}$.

###### Proof.

By contradiction, suppose that $v^{\prime}\neq v^{\prime\prime}$. Lemma 18
shows that either $v^{\prime}\subset v^{\prime\prime}$ or $v^{\prime}\supset
v^{\prime\prime}$. Without loss of generality, let $v^{\prime}\subset
v^{\prime\prime}$. Given Lemma 22, we conclude that $v^{\prime}\subset v$ and
$v^{\prime\prime}\subset v$.

Let $v^{\prime}$ lead to a view $v_{i}\in V(t)$ at time $t$ (such view $v_{i}$
exists since $v^{\prime}\subset v^{\prime\prime}$ and lemmas 16 and 19). We
know, by Lemma 18, that either $v_{i}\subseteq v^{\prime\prime}$ or
$v_{i}\supset v^{\prime\prime}$. We conclude that $v_{i}\subseteq
v^{\prime\prime}$ (otherwise, the statement of Lemma 24 would be violated).

Lemma 23 shows that $v\subset v_{i}$. Given that $v_{i}\subseteq
v^{\prime\prime}$, we conclude that $v\subset v^{\prime\prime}$. This
represents contradiction with $v^{\prime\prime}\subset v$, which concludes the
proof. ∎

The next lemma proves that, if a process obtains an evidence $\epsilon$ for
$\mathit{set}\neq\emptyset$ and view $v^{\prime}$ by time $t$, then
$\mathit{set}\in\beta_{t}(v)$.

###### Lemma 0.

Let a (correct or faulty) process obtain an evidence $\epsilon^{\prime}$ by
time $t$ such that
$\mathtt{valid}((v^{\prime},\mathit{set}^{\prime},\epsilon^{\prime}),v)=\top$,
where $\mathit{set}^{\prime}\neq\emptyset$. Then, $v\in V(t)$ and
$\mathit{set}^{\prime}\in\beta_{t}(v)$.

###### Proof.

First, we conclude that $v\neq\mathit{genesis}$ since
$\mathtt{valid}((v^{\prime},\mathit{set}^{\prime}\neq\emptyset,\epsilon^{\prime}),\mathit{genesis})$
must return $\bot$ (because of the check at line 3 of
LABEL:lst:view_set_evidence_valid). Moreover, we know that
$\epsilon^{\prime}.\mathit{path}.\mathtt{destination()}=v$ and
$\epsilon^{\prime}.\mathit{path}.\mathtt{tail()}=\mathit{set}^{\prime}$ (by
the check at line 45 of LABEL:lst:view_set_evidence_valid). By Lemma 9, we
know that $v\in V(t)$ and $\mathit{set}^{\prime}\in\beta_{t}(v)$, which
concludes the proof. ∎

Similarly, if a process obtains an evidence $\epsilon$ for
$\mathit{set}=\emptyset$ by time $t$, then $\alpha_{t}(v)=\top$.

###### Lemma 0.

Let a (correct or faulty) process obtain an evidence $\epsilon^{\prime}$ by
time $t$ such that
$\mathtt{valid}((v^{\prime},\emptyset,\epsilon^{\prime}),v)=\top$, Then, $v\in
V(t)$ and $\alpha_{t}(v)=\top$.

###### Proof.

If $v=\mathit{genesis}$, the lemma trivially holds. Otherwise, we know that
$\epsilon^{\prime}.\mathit{path}.\mathtt{destination()}=v$ and
$\epsilon^{\prime}.\mathit{path}.\mathtt{tail()}=\emptyset$ (by the check at
line 45 of LABEL:lst:view_set_evidence_valid). By Lemma 9, $v\in V(t)$. Let
$m$ be the last message in the ordered set of
$\epsilon^{\prime}.\mathit{path}$. We know that $m.\mathtt{tail()}=\emptyset$
and $m.\mathtt{destination()}=v$ (by LABEL:lst:view_path). Moreover,
$m\in\mathcal{I}^{*}(t)$ and $m.\mathtt{source()}\in V(t)$ (by Lemma 9).
Hence, $\alpha_{t}(v)=\top$. ∎

We now introduce the last invariant we assume holds at time $t$.

###### Invariant 5.

Let $v\in V(t)$. If $\mathit{set}\in\beta_{t}(v)$, where
$\mathit{set}=\\{v_{1}^{\prime},...,v_{y}^{\prime}\\}$ and $y\geq 1$, then:

  * •

$\mathit{seq}^{\prime}\in\rho_{t}(v^{\prime})$, where $v^{\prime}\in V(t)$,
$\alpha_{t}(v^{\prime})=\top$ and $\mathit{seq}^{\prime}=v_{1}\to...\to
v_{x}\to v\to v_{1}^{\prime}\to...\to v_{y}^{\prime},(x\geq 0)$, and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$, $v_{i}\in V(t)$ and
$\alpha_{t}(v_{i})=\bot$, and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$,
$\mathit{seq}_{i}\in\rho_{t}(v_{i})$, where $\mathit{seq}_{i}=v_{i+1}\to...\to
v_{x}\to v\to v_{1}^{\prime}\to...\to v_{y}^{\prime}$.

Since $\mathcal{I}^{*}(0)=\emptyset$ at time $0$, we know that
$V(0)=\\{\mathit{genesis}\\}$ and $\beta_{0}(\mathit{genesis})=\emptyset$.
Hence, Invariant 5 is satisfied at time $0$.

###### Lemma 0.

$\beta_{t}(\mathit{genesis})=\emptyset$.

###### Proof.

By contradiction, let $\beta_{t}(\mathit{genesis})\neq\emptyset$. Let
$\mathit{set}\in\beta_{t}(\mathit{genesis})$, where
$\mathit{set}=\\{v_{1}^{\prime},...,v_{y}^{\prime}\\}$ and $y\geq 1$.
According to Invariant 5, there exists an installable view $v\in V(t)$ such
that $\mathit{seq}^{\prime}\in\rho_{t}(v)$, where
$\mathit{seq}^{\prime}=v_{1}\to...\to v_{x}\to\mathit{genesis}\to
v_{1}^{\prime}\to...\to v_{y}^{\prime}$ and $x\geq 0$. By Invariant 1, we know
that $\mathit{seq}^{\prime}.\mathtt{follows}(v)=\top$, which implies that
$v\subset\mathit{genesis}$. However, this statement contradicts Invariant 3,
which concludes the proof. ∎

We prove that, if $\mathit{set}\in\beta_{t}(v)$, then $\mathit{set}$ is a
sequence and $\mathit{set}.\mathtt{follows}(v)=\top$.

###### Lemma 0.

Let $v\in V(t)$. If $\mathit{set}\in\beta_{t}(v)$, then (1) $\mathit{set}$ is
a sequence, and (2) $\mathit{set}.\mathtt{follows}(v)=\top$.

###### Proof.

Let $\mathit{set}=\\{v_{1}^{\prime},...,v_{y}^{\prime}\\}$, where $y\geq 1$.
By Invariant 5, there exists a view $v^{\prime}\in V(t)$ such that (1)
$\alpha_{t}(v^{\prime})=\top$, and (2)
$\mathit{seq}^{\prime}\in\rho_{t}(v^{\prime})$, where
$\mathit{seq}^{\prime}=v_{1}\to...\to v_{x}\to v\to v_{1}^{\prime}\to...\to
v_{y}^{\prime}$, where $x\geq 0$. Therefore, $\mathit{set}$ is a sequence and
$\mathit{set}.\mathtt{follows}(v)=\top$. ∎

The next lemma shows that, if $\mathit{seq}\in\beta_{t}(v)$, where $v$ is an
installable view, and $\mathit{seq}$ “comes from” an installable view
$v^{\prime}$, then $v^{\prime}$ leads to $v$. Recall that all sets in
$\beta_{t}(v)$ are sequences according to Lemma 29.

###### Lemma 0.

Let $\mathit{seq}\in\beta_{t}(v)$, where $\mathit{seq}=v_{1}^{\prime}\to...\to
v_{y}^{\prime},(y\geq 1)$ and $\alpha_{t}(v)=\top$. Then,
$\mathit{seq}^{\prime}\in\rho_{t}(v^{\prime})$, where
$\mathit{seq}^{\prime}=v_{1}\to...\to v_{x}\to v\to v_{1}^{\prime}\to...\to
v_{y}^{\prime},(x\geq 0)$ and $v^{\prime}$ leads to $v$ at time $t$.

###### Proof.

By Invariant 5, we know that:

  * •

$\mathit{seq}^{\prime}\in\rho_{t}(v^{\prime})$, where
$\alpha_{t}(v^{\prime})=\top$ and $\mathit{seq}^{\prime}=v_{1}\to...\to
v_{x}\to v\to v_{1}^{\prime}\to...\to v_{y}^{\prime},(x\geq 0)$, and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$, $v_{i}\in V(t)$ and
$\alpha_{t}(v_{i})=\bot$, and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$,
$\mathit{seq}_{i}\in\rho_{t}(v_{i})$, where $\mathit{seq}_{i}=v_{i+1}\to...\to
v_{x}\to v\to v_{1}^{\prime}\to...\to v_{y}^{\prime}$.

In order to conclude the proof, we need to prove that $v^{\prime}$ indeed
leads to $v$ at time $t$.

By Invariant 1, we have that $v^{\prime}\subset v$. By contradiction, suppose
that $v^{\prime}$ leads to $v^{\prime\prime}\neq v$ at time $t$ (such view
$v^{\prime\prime}$ exists since $v^{\prime}\subset v$ and lemmas 16 and 19).
Therefore, by Definition 11,
$\mathit{seq}^{\prime\prime}\in\rho_{t}(v^{\prime})$, where
$\mathit{seq}^{\prime\prime}=...\to v^{\prime\prime}$. Let us analyze all
three possible cases according to Lemma 10:

  * •

$\mathit{seq}^{\prime}=\mathit{seq}^{\prime\prime}$: Hence, $v\subset
v^{\prime\prime}$ and Definition 11 is not satisfied for $v^{\prime\prime}$
(since $\alpha_{t}(v)=\top$).

  * •

$\mathit{seq}^{\prime}\subset\mathit{seq}^{\prime\prime}$: Hence,
$v\in\mathit{seq}^{\prime\prime}$. Thus, $v\subset v^{\prime\prime}$ and
Definition 11 is not satisfied for $v^{\prime\prime}$ (since
$\alpha_{t}(v)=\top$).

  * •

$\mathit{seq}^{\prime}\supset\mathit{seq}^{\prime\prime}$: Hence,
$v^{\prime\prime}\in\mathit{seq}^{\prime}$. If $v^{\prime\prime}\subset v$,
Invariant 5 is violated since $\alpha_{t}(v^{\prime\prime})=\top$. If
$v\subset v^{\prime\prime}$, then we have the following: (1) $v^{\prime}$
leads to $v^{\prime\prime}$, and (2) $v^{\prime}\subset v\subset
v^{\prime\prime}$, where $\alpha_{t}(v)=\top$. Hence, Lemma 24 is
contradicted.

The lemma holds. ∎

The next lemma shows that, if $\mathit{seq}\in\beta_{t}(v)$, where $v$ is non-
installable, and $\mathit{seq}$ “comes from” an installable view $v^{\prime}$,
then $v$ is an auxiliary view for $v^{\prime}$.

###### Lemma 0.

Let $\mathit{seq}\in\beta_{t}(v)$, where $\mathit{seq}=v_{1}^{\prime}\to...\to
v_{y}^{\prime},(y\geq 1)$ and $\alpha_{t}(v)=\bot$. Then,
$\mathit{seq}^{\prime}\in\rho_{t}(v^{\prime})$, where
$\mathit{seq}^{\prime}=v_{1}\to...\to v_{x}\to v\to v_{1}^{\prime}\to...\to
v_{y}^{\prime},(x\geq 0)$, views from the $\\{v_{1},...,v_{x}\\}$ set are not
installable at time $t$ and $v$ is an auxiliary view for $v^{\prime}$ at time
$t$.

###### Proof.

By Invariant 5, we know that:

  * •

$\mathit{seq}^{\prime}\in\rho_{t}(v^{\prime})$, where
$\alpha_{t}(v^{\prime})=\top$ and $\mathit{seq}^{\prime}=v_{1}\to...\to
v_{x}\to v\to v_{1}^{\prime}\to...\to v_{y}^{\prime},(x\geq 0)$, and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$, $v_{i}\in V(t)$ and
$\alpha_{t}(v_{i})=\bot$, and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$,
$\mathit{seq}_{i}\in\rho_{t}(v_{i})$, where $\mathit{seq}_{i}=v_{i+1}\to...\to
v_{x}\to v\to v_{1}^{\prime}\to...\to v_{y}^{\prime}$.

Hence, Definition 20 is satisfied and $v$ is an auxiliary view for
$v^{\prime}$ at time $t$. Moreover, views from the $\\{v_{1},...,v_{x}\\}$ set
are not installable at time $t$, which concludes the proof. ∎

The next lemma shows that, if
$\mathit{seq}_{1},\mathit{seq}_{2}\in\beta_{t}(v)$, then $\mathit{seq}_{1}$
and $\mathit{seq}_{2}$ are comparable.

###### Lemma 0.

Let $v\in V(t)$. If $\mathit{seq}_{1},\mathit{seq}_{2}\in\beta_{t}(v)$, then
either $\mathit{seq}_{1}\subseteq\mathit{seq}_{2}$ or
$\mathit{seq}_{1}\supset\mathit{seq}_{2}$.

###### Proof.

Let $\alpha_{t}(v)=\top$. For every $\mathit{seq}\in\beta_{t}(v)$, where
$\mathit{seq}=v_{1}^{\prime}\to...\to v_{y}^{\prime},(y\geq 1)$,
$\mathit{seq}^{\prime}\in\rho_{t}(v^{\prime})$, where
$\mathit{seq}^{\prime}=...\to v\to v_{1}^{\prime}\to...\to v_{y}^{\prime}$ and
$v^{\prime}$ leads to $v$ at time $t$ (according to Lemma 30). By Lemma 17,
only view $v^{\prime}$ leads to $v$ at time $t$. Thus, the lemma follows from
Lemma 10.

Let $\alpha_{t}(v)=\bot$. For every $\mathit{seq}\in\beta_{t}(v)$, where
$\mathit{seq}=v_{1}^{\prime}\to...\to v_{y}^{\prime},(y\geq 1)$,
$\mathit{seq}^{\prime}\in\rho_{t}(v^{\prime})$, where
$\mathit{seq}^{\prime}=...\to v\to v_{1}^{\prime}\to...\to v_{y}^{\prime}$ and
$v$ is an auxiliary view for $v^{\prime}$ at time $t$ (according to Lemma 31).
According to Lemma 25, $v$ is an auxiliary view only for view $v^{\prime}$ at
time $t$. Thus, the lemma follows from Lemma 10. ∎

Let $[\mathtt{INSTALL},v,\mathit{set},\omega]$ be the first $\mathtt{INSTALL}$
message obtained by a (correct or faulty) process after time $t$ such that
$v\in V(t)$. We prove that either $\mathit{set}\in\beta_{t}(v)$ or
$\alpha_{t}(v)=\top$. Note that we do not consider $\mathtt{INSTALL}$ messages
with $v\notin V(t)$ since, in that case, $v$ is not a valid view (by Lemma 7).

Importantly, if multiple new $\mathtt{INSTALL}$ messages are obtained at the
same time $t^{\prime}>t$, the notion of the “first” $\mathtt{INSTALL}$ message
is not defined. However, in that case, we order the messages in any arbitrary
way. In other words, we “artificially” select the “first” $\mathtt{INSTALL}$
message and observe its properties, as well as the properties after this
message has been processed (i.e., added to the set of all obtained
$\mathtt{INSTALL}$ messages). Importantly, we process all messages from time
$t^{\prime}$ before moving on to processing messages from some time
$t^{\prime\prime}>t^{\prime}$. We are allowed to “separately” process the
$\mathtt{INSTALL}$ messages from time $t^{\prime}$ because, after all these
$\mathtt{INSTALL}$ messages are processed, we obtain the exact same system
state as we would obtain if all the messages were processed “together”.

###### Lemma 0.

Let $[\mathtt{INSTALL},v,\mathit{set},\omega]\notin\mathcal{I}^{*}(t)$ be the
first $\mathtt{INSTALL}$ message obtained by a (correct or faulty) process
after time $t$ such that $v\in V(t)$; let that time be $t^{\prime}>t$. Then,
$\mathit{set}\in\beta_{t}(v)$ or $\alpha_{t}(v)=\top$.

###### Proof.

By Lemma 8, $v$ is a valid view. Moreover,
$\mathit{preconditions}(v,t^{\prime}-1)=\top$ (since $t^{\prime}$ is the first
time after time $t$ at which an $\mathtt{INSTALL}$ message is obtained and by
lemmas 26, 29 and 32). By safety of $\mathit{vg}(v)$, we have that
$(v^{*},\emptyset,\epsilon^{*})\in\Lambda_{t^{\prime}-1}^{v}$ or
$(v^{*},\mathit{set},\epsilon^{*})\in\Lambda_{t^{\prime}-1}^{v}$. If
$(v^{*},\emptyset,\epsilon^{*})\in\Lambda_{t^{\prime}-1}^{v}$, then
$\alpha_{t}(v)=\top$ (by Lemma 27). If
$(v^{*},\mathit{set},\epsilon^{*})\in\Lambda_{t^{\prime}-1}^{v}$, then
$\mathit{set}\in\beta_{t}(v)$ (by Lemma 26). Therefore, the lemma holds. ∎

Next, we prove some properties of $\mathit{set}$.

###### Lemma 0.

Let $[\mathtt{INSTALL},v,\mathit{set},\omega]\notin\mathcal{I}^{*}(t)$ be the
first $\mathtt{INSTALL}$ message obtained by a (correct or faulty) process
after time $t$ such that $v\in V(t)$; let that time be $t^{\prime}>t$. Then,
(1) $\mathit{set}\neq\emptyset$, (2) $\mathit{set}$ is a sequence, and (3)
$\mathit{set}.\mathtt{follows}(v)=\top$.

###### Proof.

By Lemma 8, $v$ is a valid view. Moreover,
$\mathit{preconditions}(v,t^{\prime}-1)=\top$ (since $t^{\prime}$ is the first
time after time $t$ at which an $\mathtt{INSTALL}$ message is obtained and by
lemmas 26, 29 and 32). Hence, the lemma follows from validity of
$\mathit{vg}(v)$. ∎

Finally, we prove that all well-founded views at time $t$ are comparable. This
lemma is the crucial ingredient for proving the view comparability property
(see LABEL:lst:reconfiguration_properties_new).

###### Lemma 0.

Let $v,v^{\prime}\in V(t)$. Then, either $v\subseteq v^{\prime}$ or $v\supset
v^{\prime}$.

###### Proof.

If $v=v^{\prime}$, the lemma holds. Otherwise, we consider four possible
cases:

  1. (1)

$\alpha_{t}(v)=\alpha_{t}(v^{\prime})=\top$: In this case, the lemma follows
from Lemma 18.

  2. (2)

$\alpha_{t}(v)=\top$ and $\alpha_{t}(v^{\prime})=\bot$: Let $v^{\prime}$ be
the auxiliary view for a view $v_{i}$ at time $t$ (such view $v_{i}$ exists
due to Lemma 21). According to Lemma 18, $v\subseteq v_{i}$ or $v\supset
v_{i}$. We analyze all three possibilities:

     * •

$v=v_{i}$: In this case, the lemma holds since $v\subset v^{\prime}$ (by Lemma
22).

     * •

$v\subset v_{i}$: We have that $v_{i}\subset v^{\prime}$ (by Lemma 22). Hence,
$v\subset v^{\prime}$ and the lemma holds.

     * •

$v\supset v_{i}$: Let $v_{i}$ lead to a view $v^{\prime\prime}$ at time $t$
(such view $v^{\prime\prime}$ exists due to lemmas 16 and 19). Because of
Lemma 18 and Lemma 24, we have that $v^{\prime\prime}\subseteq v$. We conclude
that $v^{\prime}\subset v$ since $v^{\prime}\subset v^{\prime\prime}$ (by
Lemma 23).

  3. (3)

$\alpha_{t}(v)=\bot$ and $\alpha_{t}(v^{\prime})=\top$: Analogous to the
previous case.

  4. (4)

$\alpha_{t}(v)=\alpha_{t}(v^{\prime})=\bot$: Let $v$ be an auxiliary view for
$v_{i}$ and let $v^{\prime}$ be an auxiliary view for $v_{i}^{\prime}$ (by
Lemma 21). According to Lemma 18, we have three possibilities to examine:

     * •

$v_{i}=v_{i}^{\prime}$: By Definition 20, we have that
$\mathit{seq},\mathit{seq}^{\prime}\in\rho_{t}(v_{i})$, where
$\mathit{seq}=...\to v\to...$ and $\mathit{seq}^{\prime}=...\to
v^{\prime}\to...$. The lemma follows from Lemma 10, Invariant 1 and the
definition of a sequence.

     * •

$v_{i}\subset v_{i}^{\prime}$: Let $v_{i}$ lead to a view $v^{\prime\prime}$
at time $t$ (such view $v^{\prime\prime}$ exists by lemmas 16 and 19). Because
of Lemma 18 and Lemma 24, we have that $v^{\prime\prime}\subseteq
v_{i}^{\prime}$. We conclude that $v\subset v^{\prime}$ since $v\subset
v^{\prime\prime}$ (by Lemma 23).

     * •

$v_{i}\supset v_{i}^{\prime}$: Analogous to the case $v_{i}\subset
v_{i}^{\prime}$.

The lemma holds since it holds in all four possibilities. ∎

Let $[\mathtt{INSTALL},v,\mathit{set},\omega]$ be the first $\mathtt{INSTALL}$
message obtained by a (correct or faulty) process after time $t$ such that
$v\in V(t)$. Let that happen at time $t^{\prime}$. The following lemma proves
that $\mathit{set}$ comes from a view that is installable at time
$t^{\prime}$.

###### Lemma 0.

Let $[\mathtt{INSTALL},v,\mathit{seq}=v_{1}^{\prime}\to...\to
v_{y}^{\prime},\omega]\notin\mathcal{I}^{*}(t)$, where $y\geq 1$, be the first
$\mathtt{INSTALL}$ message obtained by a (correct or faulty) process after
time $t$ such that $v\in V(t)$; let that be at time $t^{\prime}>t$. Then:

  * •

$\mathit{seq}^{\prime}\in\rho_{t^{\prime}}(v^{\prime})$, where $v^{\prime}\in
V(t^{\prime})$, $\alpha_{t^{\prime}}(v^{\prime})=\top$ and
$\mathit{seq}^{\prime}=v_{1}\to...\to v_{x}\to v_{1}^{\prime}\to...\to
v_{y}^{\prime},(x\geq 0)$, and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$, $v_{i}\in V(t^{\prime})$ and
$\alpha_{t^{\prime}}(v_{i})=\bot$, and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$,
$\mathit{seq}_{i}\in\rho_{t^{\prime}}(v_{i})$, where
$\mathit{seq}_{i}=v_{i+1}\to...\to v_{x}\to v_{1}^{\prime}\to...\to
v_{y}^{\prime}$.

###### Proof.

If $\alpha_{t}(v)=\top$, then $\alpha_{t^{\prime}}(v)=\top$ (since
$\mathcal{I}^{*}(t)\subseteq\mathcal{I}^{*}(t^{\prime})$). Moreover, we have
that $\mathit{seq}\in\rho_{t^{\prime}}(v)$, which concludes the lemma.

Let $\alpha_{t}(v)=\bot$. According to Lemma 33,
$\mathit{seq}\in\beta_{t}(v)$. Since Invariant 5 holds at time $t$, we
conclude that:

  * •

$\mathit{seq}^{\prime}\in\rho_{t}(v^{\prime})$, where $v^{\prime}\in V(t)$,
$\alpha_{t}(v^{\prime})=\top$ and $\mathit{seq}^{\prime}=v_{1}\to...\to
v_{x}\to v\to v_{1}^{\prime}\to...\to v_{y}^{\prime},(x\geq 0)$, and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$, $v_{i}\in V(t)$ and
$\alpha_{t}(v_{i})=\bot$, and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$,
$\mathit{seq}_{i}\in\rho_{t}(v_{i})$, where $\mathit{seq}_{i}=v_{i+1}\to...\to
v_{x}\to v\to v_{1}^{\prime}\to...\to v_{y}^{\prime}$.

At time $t^{\prime}$, the previous statements still hold (since
$\mathcal{I}^{*}(t)\subseteq\mathcal{I}^{*}(t^{\prime})$). Moreover,
$\mathit{seq}\in\rho_{t^{\prime}}(v)$, which concludes the lemma. ∎

Finally, we show that all invariants are preserved after a new
$\mathtt{INSTALL}$ message is obtained.

###### Theorem 37.

Let
$[\mathtt{INSTALL},v,\mathit{seq}=v^{\prime},\omega]\notin\mathcal{I}^{*}(t)$
be the first $\mathtt{INSTALL}$ message obtained by a (correct or faulty)
process after time $t$ such that $v\in V(t)$; let that be at time
$t^{\prime}>t$. Let $v^{\prime}\notin V(t)$. Then, all invariants hold at time
$t^{\prime}$.

###### Proof.

We prove the preservation of invariants one by one.

Invariant 1: Invariant 1 holds for $v^{\prime}$ at time $t^{\prime}$ since
$\rho_{t^{\prime}}(v^{\prime})=\emptyset$. Let us prove this statement. By
contradiction, suppose that a process has obtained an $\mathtt{INSTALL}$
message associated with view $v^{\prime}$ before time $t^{\prime}$. Since
$v^{\prime}\notin V(t)$, we know that $v^{\prime}$ is not a valid view (by
Lemma 7). However, since $v^{\prime}\in V(t^{\prime})$, $v^{\prime}$ is a
valid view according to Lemma 8. Thus, contradiction.

The invariant holds for all views $v_{t}\in V(t)$, where $v_{t}\neq v$,
because $\rho_{t^{\prime}}(v_{t})=\rho_{t}(v_{t})$ and the invariant holds at
time $t$. Finally, the invariant holds for $v$ at time $t^{\prime}$ because of
Lemma 34 and the fact that the invariant holds at time $t$.

Invariant 2: We conclude that $\alpha_{t^{\prime}}(v^{\prime})=\top$. By Lemma
36, there exists a view $v^{*}\in V(t^{\prime})$ such that:

  * •

$\alpha_{t^{\prime}}(v^{*})=\top$, and

  * •

$\mathit{seq}^{\prime}\in\rho_{t^{\prime}}(v^{*})$, where
$\mathit{seq}^{\prime}=v_{1}\to...\to v_{x}\to v^{\prime},(x\geq 0)$, and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$, $v_{i}\in V(t^{\prime})$ and
$\alpha_{t^{\prime}}(v_{i})=\bot$, and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$,
$\mathit{seq}_{i}\in\rho_{t^{\prime}}(v_{i})$, where
$\mathit{seq}_{i}=v_{i+1}\to...\to v_{x}\to v^{\prime}$.

Hence, Invariant 2 holds for $v^{\prime}$ at time $t^{\prime}$.

Since $v^{\prime}\notin V(t)$ and Invariant 2 holds at time $t$, we conclude
that Invariant 2 holds for all views $v_{t}\in V(t)$. Thus, Invariant 2 holds
at time $t^{\prime}$.

Invariant 3: Since $v^{*}\in V(t)$ and Invariant 3 holds at time $t$, we know
that $\mathit{genesis}\subseteq v^{*}$. We know that
$\mathit{seq}^{\prime}\in\rho_{t^{\prime}}(v^{*})$. Since Invariant 1 holds at
time $t^{\prime}$, we know that $v^{*}\subset v^{\prime}$. Hence,
$\mathit{genesis}\subset v^{\prime}$, which proves the invariant preservation
at time $t^{\prime}$.

Invariant 4: Since $v^{\prime}\notin V(t)$,
$\alpha_{t^{\prime}}(v^{\prime})=\top$ and Invariant 4 holds at time $t$,
Invariant 4 holds at time $t^{\prime}$.

Invariant 5: Since $v^{\prime}\notin V(t)$,
$\beta_{t^{\prime}}(v^{\prime})=\emptyset$ and Invariant 5 holds at time $t$,
Invariant 5 holds at time $t^{\prime}$. ∎

Now, we analyze the second possibility.

###### Theorem 38.

Let
$[\mathtt{INSTALL},v,\mathit{seq}=v^{\prime},\omega]\notin\mathcal{I}^{*}(t)$
be the first $\mathtt{INSTALL}$ message obtained by a (correct or faulty)
process after time $t$ such that $v\in V(t)$; let that be at time
$t^{\prime}>t$. Let $v^{\prime}\in V(t)$. Then, all invariants hold at time
$t^{\prime}$.

###### Proof.

We separate the proof into two cases.

(1) Let $\alpha_{t}(v^{\prime})=\top$.

Invariant 1: Invariant 1 holds for all views $v_{t}\in V(t)\setminus\\{v\\}$
at time $t^{\prime}$ since it holds at time $t$. The invariant holds for $v$
at time $t^{\prime}$ because of Lemma 34 and the fact that the invariant holds
at time $t$.

Invariant 2: Since $\alpha_{t}(v^{\prime})=\top$, all views installable at
time $t$ are installable at time $t^{\prime}$. The fact that Invariant 2 holds
at time $t$ implies that the invariant holds at time $t^{\prime}$.

Invariant 3: Since $\alpha_{t}(v^{\prime})=\top$, all views installable at
time $t$ are installable at time $t^{\prime}$. Hence, Invariant 3 holds at
time $t^{\prime}$ since it holds at time $t$.

Invariant 4: Since $\alpha_{t}(v^{\prime})=\top$, all views installable at
time $t$ are installable at time $t^{\prime}$. Hence, the invariant holds at
time $t^{\prime}$ since it holds at time $t$.

Invariant 5: Since $\alpha_{t}(v^{\prime})=\top$, all views installable at
time $t$ are installable at time $t^{\prime}$. Moreover,
$\beta_{t^{\prime}}(v_{t})=\beta_{t}(v_{t})$, for every view $v_{t}\in V(t)$
(note that $V(t^{\prime})=V(t)$). Hence, the invariant holds at time
$t^{\prime}$ since it holds at time $t$.

(2) Let $\alpha_{t}(v^{\prime})=\bot$.

Invariant 1: Invariant 1 holds for all views $v_{t}\in V(t)\setminus\\{v\\}$
at time $t^{\prime}$ since it holds at time $t$. The invariant holds for $v$
at time $t^{\prime}$ because of Lemma 34 and the fact that the invariant holds
at time $t$.

Invariant 2: By Lemma 36, there exists a view $v^{*}\in V(t^{\prime})$ such
that:

  * •

$\alpha_{t^{\prime}}(v^{*})=\top$, and

  * •

$\mathit{seq}^{\prime}\in\rho_{t^{\prime}}(v^{*})$, where
$\mathit{seq}^{\prime}=v_{1}\to...\to v_{x}\to v^{\prime},(x\geq 0)$, and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$, $v_{i}\in V(t^{\prime})$ and
$\alpha_{t^{\prime}}(v_{i})=\bot$, and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$,
$\mathit{seq}_{i}\in\rho_{t^{\prime}}(v_{i})$, where
$\mathit{seq}_{i}=v_{i+1}\to...\to v_{x}\to v^{\prime}$.

Hence, Invariant 2 holds for $v^{\prime}$ at time $t^{\prime}$.

Consider now a view $v_{\mathit{ins}}\in V(t)$ such that (1)
$v_{\mathit{ins}}\neq\mathit{genesis}$, and (2)
$\alpha_{t}(v_{\mathit{ins}})=\top$. Since Invariant 2 holds at time $t$ and
$v_{\mathit{ins}}\neq\mathit{genesis}$, there is a view $v_{\mathit{lead}}$
that leads to $v_{\mathit{ins}}$ at time $t$ (by Lemma 13). By Definition 11,
we have:

  * •

$\alpha_{t}(v_{\mathit{lead}})=\top$, and

  * •

$\mathit{seq}_{\mathit{ins}}\in\rho_{t}(v_{\mathit{lead}})$, where
$\mathit{seq}_{\mathit{ins}}=v_{1}^{\prime}\to...\to v_{y}^{\prime}\to
v_{\mathit{ins}}$ and $y\geq 0$, and

  * •

for every $v_{i}\in\\{v_{1}^{\prime},...,v_{y}^{\prime}\\}$, $v_{i}\in V(t)$
and $\alpha_{t}(v_{i})=\bot$, and

  * •

for every $v_{i}\in\\{v_{1}^{\prime},...,v_{y}^{\prime}\\}$,
$\mathit{seq}_{i}\in\rho_{t}(v_{i})$, where
$\mathit{seq}_{i}=v_{i+1}^{\prime}\to...\to v_{y}^{\prime}\to
v_{\mathit{ins}}$.

If $v^{\prime}\notin\mathit{seq}_{\mathit{ins}}$, Invariant 2 is satisfied for
$v_{\mathit{ins}}$ at time $t^{\prime}$.

Otherwise, let $\mathit{seq}_{\mathit{ins}}=v_{1}^{\prime\prime}\to...\to
v_{z}^{\prime\prime}\to v^{\prime}\to v_{1}^{\prime\prime\prime}\to...\to
v_{q}^{\prime\prime\prime}\to v_{\mathit{ins}}$, where $z\geq 0$ and $q\geq
0$. The following holds at time $t^{\prime}$:

  * •

$\alpha_{t^{\prime}}(v^{\prime})=\top$, and

  * •

$\mathit{seq}_{v}\in\rho_{t^{\prime}}(v^{\prime})$, where
$\mathit{seq}_{v}=v_{1}^{\prime\prime\prime}\to...\to
v_{q}^{\prime\prime\prime}\to v_{\mathit{ins}}$ (recall that
$\mathit{seq}_{v}\in\rho_{t}(v^{\prime})$), and

  * •

for every
$v_{i}\in\\{v_{1}^{\prime\prime\prime},...,v_{q}^{\prime\prime\prime}\\}$,
$v_{i}\in V(t^{\prime})$ and $\alpha_{t^{\prime}}(v_{i})=\bot$, and

  * •

for every
$v_{i}\in\\{v_{1}^{\prime\prime\prime},...,v_{q}^{\prime\prime\prime}\\}$,
$\mathit{seq}^{\prime}_{i}\in\rho_{t^{\prime}}(v_{i}^{\prime})$, where
$\mathit{seq}^{\prime}_{i}=v_{i+1}^{\prime\prime\prime}\to...\to
v_{q}^{\prime\prime\prime}\to v_{\mathit{ins}}$.

Therefore, Invariant 2 is, even in this case, satisfied for
$\mathit{v}_{\mathit{ins}}$ at time $t^{\prime}$.

Invariant 3: Since $v^{*}\in V(t)$ and Invariant 3 holds at time $t$,
$\mathit{genesis}\subseteq v^{*}$. Moreover,
$\mathit{seq}^{\prime}\in\rho_{t^{\prime}}(v^{*})$. Since Invariant 1 holds at
time $t^{\prime}$, $v^{*}\subset v^{\prime}$. Hence, $\mathit{genesis}\subset
v^{\prime}$, which proves the invariant preservation at time $t^{\prime}$.

Invariant 4: Consider a view $v_{\mathit{aux}}\in V(t)$ such that (1)
$\alpha_{t}(v_{\mathit{aux}})=\bot$, and (2) $v_{\mathit{aux}}\neq
v^{\prime}$. Since all invariants hold at time $t$, we have (by Definition
20):

  * •

$\alpha_{t}(v_{\mathit{ins}})=\top$, for some view $v_{\mathit{ins}}\in V(t)$,
and

  * •

$\mathit{seq}_{\mathit{aux}}\in\rho_{t}(v_{\mathit{ins}})$, where
$\mathit{seq}_{\mathit{aux}}=v_{1}\to...\to v_{x}\to v_{\mathit{aux}}\to
v_{1}^{\prime}\to...\to v_{y}^{\prime}$, $x\geq 0$ and $y\geq 1$, and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$, $v_{i}\in V(t)$ and
$\alpha_{t}(v_{i})=\bot$, and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$,
$\mathit{seq}_{i}\in\rho_{t}(v_{i})$, where $\mathit{seq}_{i}=v_{i+1}\to...\to
v_{x}\to v_{\mathit{aux}}\to v_{1}^{\prime}\to...\to v_{y}^{\prime}$.

If $v^{\prime}\notin\\{v_{1},...,v_{x}\\}$, Invariant 4 is satisfied for
$v_{\mathit{aux}}$ at time $t^{\prime}$.

Otherwise, let $\mathit{seq}_{\mathit{aux}}=v_{1}\to...\to v_{z-1}\to
v^{\prime}\to v_{z+1}\to...\to v_{x}\to v_{\mathit{aux}}\to
v_{1}^{\prime}\to...\to v_{y}^{\prime}$, where $z\geq 0$. The following holds
at time $t^{\prime}$:

  * •

$\alpha_{t^{\prime}}(v^{\prime})=\top$, and

  * •

$\mathit{seq}_{v^{\prime}}\in\rho_{t^{\prime}}(v^{\prime})$, where
$\mathit{seq}_{v^{\prime}}=v_{z+1}\to...\to v_{x}\to v_{\mathit{aux}}\to
v_{1}^{\prime}\to...\to v_{y}^{\prime}$ (recall that
$\mathit{seq}_{v^{\prime}}\in\rho_{t}(v^{\prime})$), and

  * •

for every $v_{i}\in\\{v_{z+1},...,v_{x}\\}$, $v_{i}\in V(t^{\prime})$ and
$\alpha_{t^{\prime}}(v_{i})=\bot$, and

  * •

for every $v_{i}\in\\{v_{z+1},...,v_{x}\\}$,
$\mathit{seq}_{i}\in\rho_{t^{\prime}}(v_{i})$, where
$\mathit{seq}^{\prime}_{i}=v_{i+1}\to...\to v_{x}\to v_{\mathit{aux}}\to
v_{1}^{\prime}\to...\to v_{y}^{\prime}$.

Therefore, Invariant 4 is, even in this case, satisfied for
$\mathit{v}_{\mathit{aux}}$ at time $t^{\prime}$.

Invariant 5: We have that $\beta_{t^{\prime}}(v_{t})=\beta_{t}(v_{t})$, for
every view $v_{t}\in V(t^{\prime})$ (recall that $V(t^{\prime})=V(t)$).
Consider a view $v^{**}\in V(t^{\prime})$ such that
$\mathit{set}\in\beta_{t}(v^{**})$ and
$\mathit{set}=\\{v_{1}^{\prime},...,v_{y}^{\prime}\\}$, where $y\geq 1$. We
know that $\mathit{set}\in\beta_{t^{\prime}}(v^{**})$. Since Invariant 5 holds
at time $t$, we have the following:

  * •

$\mathit{seq}^{**}\in\rho_{t}(v_{\mathit{ins}})$, where
$\alpha_{t}(v_{\mathit{ins}})=\top$ and $\mathit{seq}^{**}=v_{1}\to...\to
v_{x}\to v^{**}\to v_{1}^{\prime}\to...\to v_{y}^{\prime},(x\geq 0)$, and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$, $v_{i}\in V(t)$ and
$\alpha_{t}(v_{i})=\bot$, and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$,
$\mathit{seq}_{i}\in\rho_{t}(v_{i})$, where $\mathit{seq}_{i}=v_{i+1}\to...\to
v_{x}\to v^{**}\to v_{1}^{\prime}\to...\to v_{y}^{\prime}$.

Now, if $v^{\prime}\notin\\{v_{1},...,v_{x}\\}$, Invariant 5 is satisfied for
$v^{**}$ at time $t^{\prime}$.

Otherwise, let $\mathit{seq}^{**}=v_{1}\to...\to v_{z-1}\to v^{\prime}\to
v_{z+1}\to...\to v_{x}\to v^{**}\to v_{1}^{\prime}\to...\to v_{y}^{\prime}$,
where $z\geq 0$. The following holds at time $t^{\prime}$:

  * •

$\alpha_{t^{\prime}}(v^{\prime})=\top$, and

  * •

$\mathit{seq}_{v^{\prime}}\in\rho_{t^{\prime}}(v^{\prime})$, where
$\mathit{seq}_{v^{\prime}}=v_{z+1}\to...\to v_{x}\to v^{**}\to
v_{1}^{\prime}\to...\to v_{y}^{\prime}$ (recall that
$\mathit{seq}_{v^{\prime}}\in\rho_{t}(v^{\prime})$), and

  * •

for every $v_{i}\in\\{v_{z+1},...,v_{x}\\}$, $v_{i}\in V(t^{\prime})$ and
$\alpha_{t^{\prime}}(v_{i})=\bot$, and

  * •

for every $v_{i}\in\\{v_{z+1},...,v_{x}\\}$,
$\mathit{seq}_{i}\in\rho_{t^{\prime}}(v_{i})$, where
$\mathit{seq}^{\prime}_{i}=v_{i+1}\to...\to v_{x}\to v^{**}\to
v_{1}^{\prime}\to...\to v_{y}^{\prime}$.

Therefore, Invariant 5 is, even in this case, satisfied for $\mathit{v}^{**}$
at time $t^{\prime}$. ∎

Next, we analyze the third possible case.

###### Theorem 39.

Let $[\mathtt{INSTALL},v,\mathit{seq}=v^{\prime}\to v_{1}^{\prime}\to...\to
v_{y}^{\prime},\omega]\notin\mathcal{I}^{*}(t)$ be the first
$\mathtt{INSTALL}$ message obtained by a (correct or faulty) process after
time $t$ such that $v\in V(t)$; let that be at time $t^{\prime}>t$. Let
$v^{\prime}\notin V(t)$111111Observe that $v^{\prime}$ is the destination of
the message since $\mathit{seq}$ is a sequence (by Lemma 34) and $v^{\prime}$
is the smallest view of the sequence. and $y\geq 1$. Then, all invariants hold
at time $t^{\prime}$.

###### Proof.

We prove the preservation of the invariants one by one.

Invariant 1: Invariant 1 holds for $v^{\prime}$ at time $t^{\prime}$ since
$\rho_{t^{\prime}}(v^{\prime})=\emptyset$. Let us prove this statement. By
contradiction, suppose that a process has obtained an $\mathtt{INSTALL}$
message associated with view $v^{\prime}$ before time $t^{\prime}$. Since
$v^{\prime}\notin V(t)$, we know that $v^{\prime}$ is not a valid view (by
Lemma 7). However, since $v^{\prime}\in V(t^{\prime})$, $v^{\prime}$ is a
valid view according to Lemma 8. Thus, contradiction.

The invariant holds for all views $v_{t}\in V(t)$, where $v_{t}\neq v$,
because $\rho_{t^{\prime}}(v_{t})=\rho_{t}(v_{t})$ and the invariant holds at
time $t$. Finally, the invariant holds for $v$ at time $t^{\prime}$ because of
Lemma 34 and the fact that the invariant holds at time $t$.

Invariant 2: The set of installable views at time $t^{\prime}$ is identical to
the set of installable views at time $t$. Thus, the invariant is preserved
since it is satisfied at time $t$.

Invariant 3: The set of installable views at time $t^{\prime}$ is identical to
the set of installable views at time $t$. Thus, the invariant is preserved
since it is satisfied at time $t$.

Invariant 4: By Lemma 36, there exists a view $v^{*}\in V(t^{\prime})$ such
that:

  * •

$\alpha_{t^{\prime}}(v^{*})=\top$, and

  * •

$\mathit{seq}^{\prime}\in\rho_{t^{\prime}}(v^{*})$, where
$\mathit{seq}^{\prime}=v_{1}\to...\to v_{x}\to v^{\prime}\to
v_{1}^{\prime}\to...\to v_{y}^{\prime},(x\geq 0)$, and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$, $v_{i}\in V(t^{\prime})$ and
$\alpha_{t^{\prime}}(v_{i})=\bot$, and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$,
$\mathit{seq}_{i}\in\rho_{t^{\prime}}(v_{i})$, where
$\mathit{seq}_{i}=v_{i+1}\to...\to v_{x}\to v^{\prime}\to
v_{1}^{\prime}\to...\to v_{y}^{\prime}$.

Hence, Invariant 4 is satisfied at time $t^{\prime}$ for $v^{\prime}$.
Moreover, since the set of installable views at time $t^{\prime}$ is identical
to the set of installable views at time $t$ and Invariant 4 holds at time $t$,
the invariant is preserved at time $t^{\prime}$.

Invariant 5: We have that
$\beta_{t^{\prime}}(v^{\prime})=\\{v_{1}^{\prime}\to...\to v_{y}^{\prime}\\}$.
By Lemma 36, there exists a view $v^{*}\in V(t)$ such that:

  * •

$\alpha_{t^{\prime}}(v^{*})=\top$, and

  * •

$\mathit{seq}^{\prime}\in\rho_{t^{\prime}}(v^{*})$, where
$\mathit{seq}^{\prime}=v_{1}\to...\to v_{x}\to v^{\prime}\to
v_{1}^{\prime}\to...\to v_{y}^{\prime},(x\geq 0)$, and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$, $v_{i}\in V(t^{\prime})$ and
$\alpha_{t^{\prime}}(v_{i})=\bot$, and

  * •

for every $v_{i}\in\\{v_{1},...,v_{x}\\}$,
$\mathit{seq}_{i}\in\rho_{t^{\prime}}(v_{i})$, where
$\mathit{seq}_{i}=v_{i+1}\to...\to v_{x}\to v^{\prime}\to
v_{1}^{\prime}\to...\to v_{y}^{\prime}$.

Hence, Invariant 5 is satisfied for $v^{\prime}$ at time $t^{\prime}$.

For every view $v_{t}\in V(t)$, $\beta_{t^{\prime}}(v_{t})=\beta_{t}(v_{t})$.
Therefore, Invariant 5 is satisfied for $v_{t}$ at time $t^{\prime}$ since it
holds at time $t$ and the set of installable views at time $t^{\prime}$ is
identical to the set of installable views at time $t$. ∎

Lastly, we analyze the fourth possible case.

###### Theorem 40.

Let $[\mathtt{INSTALL},v,\mathit{seq}=v^{\prime}\to v_{1}^{\prime}\to...\to
v_{y}^{\prime},\omega]\notin\mathcal{I}^{*}(t)$ be the first
$\mathtt{INSTALL}$ message obtained by a (correct or faulty) process after
time $t$ such that $v\in V(t)$; let that be at time $t^{\prime}>t$. Let
$v^{\prime}\in V(t)$121212Note that $v^{\prime}$ is the destination of the
message since $\mathit{seq}$ is a sequence (by Lemma 34) and $v^{\prime}$ is
the smallest view of the sequence. and $y\geq 1$. Then, all invariants hold at
time $t^{\prime}$.

###### Proof.

We distinguish two cases:

(1) Let $\alpha_{t}(v^{\prime})=\top$.

Invariant 1: Invariant 1 holds for all views $v_{t}\in V(t)\setminus\\{v\\}$
at time $t^{\prime}$ since it holds at time $t$. The invariant holds for $v$
at time $t^{\prime}$ because of Lemma 34 and the fact that the invariant holds
at time $t$.

Invariant 2: Since $\alpha_{t}(v^{\prime})=\top$, all views installable at
time $t$ are installable at time $t^{\prime}$. The fact that Invariant 2 holds
at time $t$ implies that the invariant holds at time $t^{\prime}$.

Invariant 3: Since $\alpha_{t}(v^{\prime})=\top$, all views installable at
time $t$ are installable at time $t^{\prime}$. Hence, Invariant 3 holds at
time $t^{\prime}$ since it holds at time $t$.

Invariant 4: Since $\alpha_{t}(v^{\prime})=\top$, all views installable at
time $t$ are installable at time $t^{\prime}$. Hence, the invariant holds at
time $t^{\prime}$ since it holds at time $t$.

Invariant 5: Since $\alpha_{t}(v^{\prime})=\top$, all views installable at
time $t$ are installable at time $t^{\prime}$. Moreover,
$\beta_{t^{\prime}}(v_{t})=\beta_{t}(v_{t})$, for every view $v_{t}\in
V(t)\setminus{\\{v^{\prime}\\}}$ (note that $V(t^{\prime})=V(t)$). Hence, the
invariant holds at time $t^{\prime}$ for $v_{t}$ since it holds at time $t$.
Furthermore, Invariant 5 holds for $v^{\prime}$ at time $t^{\prime}$ because
of Lemma 36 and the fact that the invariant holds at time $t$. Thus, the
invariant is preserved at time $t^{\prime}$.

(2) Let $\alpha_{t}(v^{\prime})=\bot$.

Invariant 1: Invariant 1 holds for all views $v_{t}\in V(t)\setminus\\{v\\}$
at time $t^{\prime}$ since it holds at time $t$. The invariant holds for $v$
at time $t^{\prime}$ because of Lemma 34 and the fact that the invariant holds
at time $t$.

Invariant 2: The set of views installable at time $t$ is identical to the set
of views installable at time $t^{\prime}$. Given that the invariant holds at
time $t$, the invariant is preserved at time $t^{\prime}$.

Invariant 3: The set of views installable at time $t$ is identical to the set
of views installable at time $t^{\prime}$. Given that the invariant holds at
time $t$, the invariant is preserved at time $t^{\prime}$.

Invariant 4: The set of views installable at time $t$ is identical to the set
of views installable at time $t^{\prime}$. Given that the invariant holds at
time $t$, the invariant is preserved at time $t^{\prime}$.

Invariant 5: We have that $\beta_{t^{\prime}}(v_{t})=\beta_{t}(v_{t})$, for
every view $v_{t}\in V(t^{\prime})\setminus{\\{v^{\prime}\\}}$ (note that
$V(t^{\prime})=V(t)$). Therefore, the invariant is ensured at time
$t^{\prime}$ for $v_{t}$ since it holds at time $t$. Moreover, Invariant 5 is
ensured for $v^{\prime}$ at time $t^{\prime}$ because of Lemma 36 and the fact
that the invariant holds at time $t$. Thus, the invariant is preserved at time
$t^{\prime}$. ∎

##### Epilogue.

We have shown that, at all times, all the invariants we have introduced hold.
Now, we give some results that represent consequences of the introduced
invariants.

We start by proving that all valid views belong to $V(\infty)$.

###### Lemma 0 (Valid Views are in $V(\infty)$).

Let a view $v$ be valid. Then, $v\in V(\infty)$.

###### Proof.

Follows from Definition 1 and the definition of $V(\infty)$. ∎

Since all invariants hold at all times, we have the following for each valid
view $v\in V(\infty)$:

  * •

If $\mathit{set}\in\rho_{\infty}(v)$, then (1) $\mathit{set}\neq\emptyset$,
(2) $\mathit{set}$ is a sequence, and (3)
$\mathit{set}.\mathtt{follows}(v)=\top$ (due to the fact that Invariant 1
holds at time $\infty$).

  * •

If $\alpha_{\infty}(v)=\bot$ and $\mathit{seq}\in\rho_{\infty}(v)$, where
$\mathit{set}=v_{1}\to...\to v_{x}$ ($x\geq 1$), then
$\mathit{seq}^{\prime}\in\rho_{\infty}(v^{\prime})$, where
$\mathit{seq}^{\prime}=...\to v\to v_{1}\to...\to v_{x}$ and $v$ is an
auxiliary view for $v^{\prime}$ at time $\infty$ (due to lemmas 31 and 33).

  * •

$\mathit{preconditions}(v,t)=\top$, for any time $t$ (this follows from the
fact that $\mathit{preconditions}(v,\infty)=\top$, which is a result of lemmas
26, 29 and 32).

Next, any obtained $\mathtt{INSTALL}$ message associated with a valid view
“carries” a sequence that follows the associated view.

###### Lemma 0.

Let a (correct or faulty) process obtain the
$m=[\mathtt{INSTALL},\mathit{source},\mathit{set},\omega]$ message, where
$\mathit{source}=m.\mathtt{source()}$ is a valid view. Then, (1)
$\mathit{set}\neq\emptyset$, (2) $\mathit{set}$ is a sequence, and (3)
$\mathit{set}.\mathtt{follows}(\mathit{source})=\top$.

###### Proof.

Since $\mathit{source}$ is a valid view, $\mathit{source}\in V(\infty)$ (by
Lemma 41). Moreover, $m\in\mathcal{I}^{*}(\infty)$. Hence,
$\mathit{set}\in\rho_{\infty}(\mathit{source})$. Therefore, the lemma holds
since Invariant 1 holds at time $\infty$. ∎

Let $m=[\mathtt{INSTALL},v,\mathit{seq},\omega]$, where $v$ is a valid view.
According to Lemma 42, $\mathit{seq}\neq\emptyset$, $\mathit{seq}$ is a
sequence and $\mathit{seq}.\mathtt{follows}(v)=\top$. Moreover,
$m.\mathtt{destination()}=\mathit{seq}.\mathtt{first()}$ and
$m.\mathtt{tail()}=\mathit{seq}\setminus\\{\mathit{seq}.\mathtt{first()}\\}$.

The next lemma proves that a view $v$ leads to a view $v^{\prime}$ at time
$\infty$ if and only if $v^{\prime}$ is the smallest installable view greater
than $v$.

###### Lemma 0.

Let $v,v^{\prime}\in V(\infty)$ such that
$\alpha_{\infty}(v)=\alpha_{\infty}(v^{\prime})=\top$ and $v\subset
v^{\prime}$. Then, $v$ leads to $v^{\prime}$ at time $\infty$ if and only if
there does not exist a view $v^{\prime\prime}\in V(\infty)$ such that
$\alpha_{\infty}(v^{\prime\prime})=\top$ and $v\subset v^{\prime\prime}\subset
v^{\prime}$.

###### Proof.

In order to prove the lemma, we prove the both directions of the statement.

First, if $v$ leads to $v^{\prime}$, then there does not exist a view
$v^{\prime\prime}$ such that $\alpha_{\infty}(v^{\prime\prime})=\top$ and
$v\subset v^{\prime\prime}\subset v^{\prime}$. This statement is true due to
Lemma 24.

Now, suppose that such view $v^{\prime\prime}$ does not exist. We need to
prove that $v$ leads to $v^{\prime}$ at time $\infty$. By contradiction,
suppose that $v$ does not lead to $v^{\prime}$ at time $\infty$. Since
$v\subset v^{\prime}$, $v$ leads to a view $v_{i}\neq v^{\prime}$ at time
$\infty$ (by lemmas 16 and 19). By Lemma 12, $v\subset v_{i}$. By lemmas 18
and 24, $v_{i}\subseteq v^{\prime}$. Since $v_{i}\neq v^{\prime}$,
$v_{i}\subset v^{\prime}$. However, this contradicts the fact that an
installable view greater than $v$ and smaller than $v^{\prime}$ does not
exist. Thus, the lemma holds. ∎

Similarly to Lemma 43, a view $v^{\prime}$ is an auxiliary view for a view $v$
at time $\infty$ if and only if $v$ is the greatest installable view smaller
than $v^{\prime}$.

###### Lemma 0.

Let $v,v^{\prime}\in V(\infty)$ such that $\alpha_{\infty}(v)=\top$,
$\alpha_{\infty}(v^{\prime})=\bot$ and $v\subset v^{\prime}$. Then,
$v^{\prime}$ is an auxiliary view for $v$ at time $\infty$ if and only if
there does not exist a view $v^{\prime\prime}\in V(\infty)$ such that
$\alpha_{\infty}(v^{\prime\prime})=\top$ and $v\subset v^{\prime\prime}\subset
v^{\prime}$.

###### Proof.

In order to prove the lemma, we prove the both directions of the statement.

First, if $v^{\prime}$ is an auxiliary view for $v$ at time $\infty$, then
there does not exist a view $v^{\prime\prime}$ such that
$\alpha_{\infty}(v^{\prime\prime})=\top$ and $v\subset v^{\prime\prime}\subset
v^{\prime}$. By contradiction, let there exist such view $v^{\prime\prime}$.
By lemmas 16 and 19, $v$ leads to a view $v_{i}$ at time $\infty$. Moreover,
$v_{i}\subseteq v^{\prime\prime}$ (by lemmas 18 and 24). Since $v^{\prime}$ is
an auxiliary view for $v$ at time $\infty$, $v^{\prime}\subset v_{i}$ (by
Lemma 23). Hence, $v^{\prime}\subset v^{\prime\prime}$, which contradicts that
$v^{\prime\prime}\subset v^{\prime}$. This direction of the statement is
satisfied.

Now, suppose that such view $v^{\prime\prime}$ does not exist. We need to
prove that $v^{\prime}$ is an auxiliary view for $v$ at time $\infty$. By
contradiction, suppose that $v^{\prime}$ is not an auxiliary view for $v$ at
time $\infty$. Let $v^{\prime}$ be an auxiliary view for a view $v^{*}\neq v$
(such view $v^{*}$ exists due to Lemma 21). By Lemma 22, $v^{*}\subset
v^{\prime}$. By Lemma 18, either $v\subseteq v^{*}$ or $v\supset v^{*}$. Since
$v\neq v^{*}$ and no installable view “between” $v$ and $v^{\prime}$ exists,
$v^{*}\subset v$. Let $v^{*}$ lead to a view $v_{i}$ (by lemmas 16 and 19). By
lemmas 18 and 24, $v_{i}\subseteq v$. By Lemma 23, $v^{\prime}\subset v_{i}$.
Hence, $v^{\prime}\subset v$, which represents contradiction with $v\subset
v^{\prime}$. Thus, the lemma holds. ∎

The next lemma shows that all valid views are greater than or equal to
$\mathit{genesis}$.

###### Lemma 0.

Let a view $v$ be valid. Then, $\mathit{genesis}\subseteq v$.

###### Proof.

By Lemma 41, we know that $v,\mathit{genesis}\in V(\infty)$. By Lemma 35, we
know that either $\mathit{genesis}\subseteq v$ or $\mathit{genesis}\supset v$.
For the sake of contradiction, let $v\subset\mathit{genesis}$.

Since Invariant 3 holds at time $\infty$, $\alpha_{\infty}(v)=\bot$.
Therefore, $v$ is an auxiliary view for some view $v^{*}$ at time $\infty$ (by
Lemma 21). By Lemma 22, $v^{*}\subset v$, which implies that
$v^{*}\subset\mathit{genesis}$. However, this is impossible due to Invariant
3. The lemma holds. ∎

The next lemma shows that views that “belong” to a view-path are ordered.

###### Lemma 0.

Let $\mathit{path}=[m_{1},...,m_{k}]$, where $k\geq 1$, be a view-path. Then:

  1. (1)

$m_{i-1}.\mathtt{source()}\subset m_{i}.\mathtt{source()}$, for every
$i\in[2,k]$, and

  2. (2)

$m_{k}.\mathtt{source()}\subset m_{k}.\mathtt{destination()}$.

###### Proof.

Note that $\mathit{path}.\mathtt{views()}\subseteq V(\infty)$ (by Lemma 41).
Since $m_{i}.\mathtt{source()}=m_{i-1}.\mathtt{destination()}$, for every
$i\in[2,k]$ (see LABEL:lst:view_path), the first claim of the lemma follows
from Invariant 1. Moreover, Invariant 1 ensures that the second claim of the
lemma is true, as well. ∎

Next, we show that it is impossible that $(+,r)\notin v$ and $(-,r)\in v$,
where $v$ is a valid view and $r$ is a server.

###### Lemma 0.

Let $v$ be a valid view such that $(-,r)\in v$, where $r$ is a server. Then,
$(+,r)\in v$.

###### Proof.

By contradiction, let $(-,r)\in v$ and $(+,r)\notin v$. First,
$v\neq\mathit{genesis}$ due to the fact that $\mathit{genesis}$ does not
contain “negative” changes (see § 2, paragraph “Constants”). Thus, there
exists a view-path $\mathit{path}\subseteq\mathcal{I}^{*}(\infty)$ such that
$\mathit{path}.\mathtt{destination()}=v$ (by Definition 1).

By Lemma 46, $v^{\prime}\subset v$, where $v^{\prime}=m.\mathtt{source()}$,
$v=m.\mathtt{destination()}$ and $m$ is the last message of $\mathit{path}$.
Thus, $(+,r)\notin v^{\prime}$, which means that the membership validity
property of $\mathit{vg}(v^{\prime})$ is violated (recall that $v^{\prime}$ is
a valid view, by Lemma 9, and
$\mathit{preconditions}(v^{\prime},\infty)=\top$). Hence, the lemma holds. ∎

We now show that there are finitely many valid views (see
LABEL:lst:reconfiguration_properties_new).

###### Theorem 48 (Finitely Many Valid Views).

There exist only finitely many valid views.

###### Proof.

Consider any valid view $v$. We prove that $|C_{v}^{+}=\\{(+,r)\,|\,(+,r)\in
v\\}|<\infty$. We distinguish two possible cases:

  * •

Let $v=\mathit{genesis}$. In this case, $|C_{v}^{+}|<\infty$ due to the
definition of $\mathit{genesis}$ (see § 2, paragraph “Constants”).

  * •

Let $v\neq\mathit{genesis}$. By Definition 1, there exists a view-path
$\mathit{path}\subseteq\mathcal{I}^{*}(\infty)$ such that
$\mathit{path}.\mathtt{destination()}=v$. Let $m\in\mathit{path}$ be the
$\mathtt{INSTALL}$ message such that $m.\mathtt{destination()}=v$; note that
$m.\mathtt{source()}$ is a valid view. Now, for every $(+,r)\in C_{v}^{+}$,
the $\mathtt{JOIN}$ message is sent by $r$ (see
LABEL:lst:view_set_evidence_valid); hence, $r$ has previously started. Due to
the assumption that only finitely many servers start, $|C_{v}^{+}|<\infty$.

Now, let $C_{v}^{-}=\\{(-,r)\,|\,(-,r)\in v\\}$. Because of Lemma 47 and
$|C_{v}^{+}|<\infty$, we conclude that $|C_{v}^{-}|<\infty$. Therefore,
$|v|<\infty$. Recall that every valid view belongs to $V(\infty)$ (by Lemma
41). Since all valid views have finitely many changes, all valid views belong
to $V(\infty)$ and all views from $V(\infty)$ are comparable (by Lemma 35),
the theorem holds. ∎

Moreover, we prove that there are finitely many sequences in
$\rho_{\infty}(v)$, where $v$ is a valid view.

###### Lemma 0 (Finitely Many Sequences).

Let view $v$ be valid. Then, $|\rho_{\infty}(v)|<\infty$.

###### Proof.

Follows directly from the bounded decisions property of $\mathit{vg}(v)$. ∎

For the sake of brevity, we might use the result of Lemma 49 without
explicitly stating it in the rest of the paper.

####  6.2.2. Safety Properties

We start by proving the view comparability property specified in
LABEL:lst:reconfiguration_properties_new.

###### Theorem 50 (View Comparability).

View comparability is satisfied.

###### Proof.

All valid views belong to $V(\infty)$ (by Lemma 41). Hence, the theorem
follows from Lemma 35. ∎

The direct consequence of the view comparability property is that the
$\mathit{history}$ variable (initialized at line 6 of
LABEL:lst:storage_initialization) of a correct server is a sequence. The
indirect consequences of the property are:

  1. (1)

The $\mathit{sequence}$ variable (initialized at line 11 of
LABEL:lst:storage_initialization) of a correct server contains sequences.

  2. (2)

The $\mathit{reconfiguration}.\mathit{sequence}$ variable (initialized at line
22 of LABEL:lst:reconfiguration_initialization) of a correct server is a
sequence (or $\bot$).

We are ready to prove the join safety property (see § 3.3, paragraph
“Properties of Carbon”).

###### Theorem 51 (Join Safety).

Join safety is satisfied.

###### Proof.

Let a server $r$ join and let $r\notin\mathit{genesis}.\mathtt{members()}$. We
prove that $r$ is voted in, i.e., that a process obtains a voting proof
$\sigma_{v}$ such that $\mathtt{verify\\_voting}(\text{``add server
}r\text{''},\sigma_{v})=\top$.

Since $r$ joins and $r\notin\mathit{genesis}.\mathtt{members()}$, there exists
a correct server that executes line 34 of
LABEL:lst:reconfiguration_view_transition (if $r$ is correct, then $r$ itself
executes this line; see § 3.3, paragraph “Validators”) or line 60 of
LABEL:lst:reconfiguration_view_transition (if $r$ is faulty, a correct server
executes this line). Hence, there exists a valid view $v\neq\mathit{genesis}$
such that $r\in v.\mathtt{members()}$.

Since $v\neq\mathit{genesis}$ is valid, there exists a view-path
$\mathit{path}\subseteq\mathcal{I}^{*}(\infty)$ such that
$\mathit{path}.\mathtt{destination()}=v$ (by Definition 1). All views that
belong to $\mathit{path}.\mathtt{views()}$ are valid (by Lemma 9). Hence,
there exists an $\mathtt{INSTALL}$ message $m$ such that $m.\mathtt{source()}$
is a valid view and $r\in m.\mathtt{destination()}.\mathtt{members()}$.
Finally, the theorem holds because the evidence handed to the view generator
primitive contains $\mathtt{JOIN}$ messages with the voting proofs for every
$(+,r^{\prime})$ “proposed” change (by line 16 or line 52 of
LABEL:lst:view_set_evidence_valid), where $r^{\prime}$ is a server. ∎

The next theorem proves the leave safety property of Carbon (see § 3.3,
paragraph “Properties of Carbon”).

###### Theorem 52 (Leave Safety).

Leave safety is satisfied.

###### Proof.

Let a correct server $r$ leave. Hence, $r$ executes line 55 of
LABEL:lst:reconfiguration_view_transition. Therefore, there exist valid views
$v_{1}$ and $v_{2}$ such that (1) $r\in v_{1}.\mathtt{members()}$, and (2)
$r\notin v_{2}.\mathtt{members()}$ (by line 3 of
LABEL:lst:reconfiguration_view_transition).

Since $r\in v_{1}.\mathtt{members()}$, $(+,r)\in v_{1}$ (see LABEL:lst:view).
Moreover, since $v_{1}\subset v_{2}$ and $r\notin v_{2}.\mathtt{members()}$,
$(+,r),(-,r)\in v_{2}$. Hence, $v_{2}\neq\mathit{genesis}$ (since
$\mathit{genesis}$ does not contain “negative” changes; see § 2, paragraph
“Constants”). By Definition 1, there exists a view-path
$\mathit{path}\subseteq\mathcal{I}^{*}(\infty)$ such that
$\mathit{path}.\mathtt{destination()}=v_{2}$. Similarly to the proof of join
safety (Theorem 51), there exists an $\mathtt{INSTALL}$ message $m$ such that
$m.\mathtt{source()}$ is a valid view and $(-,r)\in m.\mathtt{destination()}$.
Furthermore, the evidence handed to the view generator primitive contains
either voting proofs or $\mathtt{LEAVE}$ messages for every $(-,r^{\prime})$
“proposed” change (by line 22 or line 58 of
LABEL:lst:view_set_evidence_valid), where $r^{\prime}$ is a server. Therefore,
$r$ either sent the $\mathtt{LEAVE}$ message or is voted out. Finally, if $r$
sent the $\mathtt{LEAVE}$ message, then $r$ has previously requested to leave
(because the $\mathtt{LEAVE}$ message is sent at line 4 of
LABEL:lst:reconfiguration_leaving). The theorem holds. ∎

####  6.2.3. Liveness Properties

We now prove the finality property specified in
LABEL:lst:reconfiguration_properties_new. Then, we show the join liveness,
leave liveness and removal liveness properties of Carbon.

We start by showing that a correct server always hand “valid” proposals to a
view generator instance.

###### Lemma 0.

Let a correct server $r$ propose
$(v^{\prime},\mathit{set}^{\prime},\epsilon^{\prime})$ to $\mathit{vg}(v)$.
Then,
$\mathtt{valid}((v^{\prime},\mathit{set}^{\prime},\epsilon^{\prime}),v)=\top$.

###### Proof.

There are two places for $r$ to propose to $\mathit{vg}(v)$. We take a look at
both places:

  * •

line 18 of LABEL:lst:reconfiguration_view_generation: We separate two
possibilities:

    * –

Let $v=\mathit{genesis}$. First, $v\subset v^{\prime}$ (ensured by the
$\mathtt{to\\_propose}$ function; line 3 of
LABEL:lst:reconfiguration_view_generation). Moreover,
$\epsilon^{\prime}.\mathit{path}=\bot$ (by line 8 of
LABEL:lst:reconfiguration_initialization). The check at line 9 of
LABEL:lst:view_set_evidence_valid passes due to the $\mathtt{to\\_propose}$
function. Finally, for each change that belongs to the
$\mathit{reconfiguration}.\mathit{requested}$ variable, server $r$ stores the
$\mathtt{JOIN}$ (at line 9 of LABEL:lst:reconfiguration_joining) or the
$\mathtt{LEAVE}$ message (at line 9 of LABEL:lst:reconfiguration_leaving) or
the corresponding voting proof (at line 13 of
LABEL:lst:reconfiguration_leaving) in the
$\mathit{reconfiguration}.\mathit{requests}$ or
$\mathit{reconfiguration}.\mathit{voting\\_proofs}$ variable. Thus, the lemma
holds in this scenario.

    * –

Let $v\neq\mathit{genesis}$. First, $v\subset v^{\prime}$ (ensured by the
$\mathtt{to\\_propose}$ function; line 3 of
LABEL:lst:reconfiguration_view_generation). Then, the check at line 39 of
LABEL:lst:view_set_evidence_valid passes due to the $\mathtt{to\\_propose}$
function. The check at line 45 of LABEL:lst:view_set_evidence_valid passes
since
$\epsilon^{\prime}.\mathit{path}=\mathit{current\\_view}.\mathit{proof}$.
Finally, for each change that belongs to the
$\mathit{reconfiguration}.\mathit{requested}$ variable, server $r$ stores the
$\mathtt{JOIN}$ (at line 9 of LABEL:lst:reconfiguration_joining) or the
$\mathtt{LEAVE}$ message (at line 9 of LABEL:lst:reconfiguration_leaving) or
the corresponding voting proof (at line 13 of
LABEL:lst:reconfiguration_leaving) in the
$\mathit{reconfiguration}.\mathit{requests}$ or
$\mathit{reconfiguration}.\mathit{voting\\_proofs}$ variable. Therefore, the
lemma holds in this scenario.

  * •

line 83 of LABEL:lst:reconfiguration_view_transition: We know that
$\epsilon^{\prime}.\mathit{path}.\mathtt{tail()}=\mathit{set}^{\prime}$.
Furthermore, $\mathit{set}^{\prime}\in\beta_{\infty}(v)$. By Lemma 28,
$v\neq\mathit{genesis}$.

The check at line 27 of LABEL:lst:view_set_evidence_valid passes since
$v^{\prime}\in\mathit{set}^{\prime}$. Next, the check at line 33 of
LABEL:lst:view_set_evidence_valid passes because of Lemma 29.

Now, if $(+,r)\notin v$, then no view $v^{*}\in\mathit{set}^{\prime}$ exists
such that $(-,r)\in v^{*}$. Let us prove this claim. Since
$\mathit{set}^{\prime}\in\beta_{\infty}(v)$,
$\mathit{seq}^{\prime\prime}\in\rho_{\infty}(v^{\prime\prime})$, where
$\alpha_{\infty}(v^{\prime\prime})=\top$, $\mathit{seq}^{\prime\prime}=...\to
v\to v_{1}\to...\to v_{x},(x\geq 1)$ and $\mathit{set}^{\prime}=v_{1}\to...\to
v_{x}$ (by Invariant 5). Since
$\mathit{seq}^{\prime\prime}.\mathtt{follows}(v^{\prime\prime})=\top$ (by
Invariant 1), $v^{\prime\prime}\subset v$. Hence, $(+,r)\notin
v^{\prime\prime}$. Therefore, no view that belongs to $\mathit{set}^{\prime}$
contains $(-,r)$ due to membership validity of $\mathit{vg}(v^{\prime\prime})$
(since $v^{\prime\prime}$ is a valid view and
$\mathit{preconditions}(v^{\prime\prime},\infty)=\top$). Thus, the checks at
lines 36 and 39 of LABEL:lst:view_set_evidence_valid pass.

The check at line 45 of LABEL:lst:view_set_evidence_valid passes since
$\epsilon^{\prime}.\mathit{path}=\mathit{current\\_view}.\mathit{proof}$.
Finally, for each change that belongs to a view of $\mathit{set}^{\prime}$,
server $r$ stores the $\mathtt{JOIN}$ or the $\mathtt{LEAVE}$ message or the
corresponding voting proof in the $\mathit{reconfiguration}.\mathit{requests}$
or $\mathit{reconfiguration}.\mathit{voting\\_proofs}$ variable because of the
$\mathtt{extract\\_requests\\_and\\_voting\\_proofs}$ function invoked after
an $\mathtt{INSTALL}$ message is processed (line 9 of
LABEL:lst:storage_processing).

The lemma is satisfied since it holds in both possible scenarios. ∎

The next lemma shows that installable views cannot be “skipped”. Specifically,
we show that any view-path to a view $v^{\prime}$ “contains” a view $v$, where
$v$ is the greatest installable view smaller than $v^{\prime}$; observe that
such installable view always exists since any view-path contains at least a
single message and the source of the first message is $\mathit{genesis}$,
which is the smallest valid view (by Lemma 45).

###### Lemma 0.

Let $\mathit{path}\subseteq\mathcal{I}^{*}(\infty)$ such that
$\mathit{path}.\mathtt{destination()}=v^{\prime}$131313Note that
$v^{\prime}\supset\mathit{genesis}$ since view-paths have at least a single
message (see LABEL:lst:view_path) and Invariant 1 holds.. Let $v$ be the
greatest view smaller than $v^{\prime}$ with $\alpha_{\infty}(v)=\top$. Then,
$v\in\mathit{path}.\mathtt{views()}$.

###### Proof.

Let $m^{*}$ be the last message of $\mathit{path}$; note that
$m^{*}.\mathtt{destination()}=v^{\prime}$. Let
$v^{*}=m^{*}.\mathtt{source()}$. If $v^{*}=v$, the lemma holds. Otherwise, we
prove that $v\subset v^{*}$.

By contradiction, suppose that $v^{*}\subset v$. We distinguish two
possibilities:

  * •

Let $\alpha_{\infty}(v^{*})=\top$. Since $v^{*}\subset v$, $v^{*}$ leads to a
view $v_{i}$ at time $\infty$ (by lemmas 16 and 19). By lemmas 18 and 24,
$v_{i}\subseteq v$.

Since $m^{*}\in\mathit{path}$, $\mathit{seq}\in\rho_{\infty}(v^{*})$, where
$\mathit{seq}=v^{\prime}\to...$. By Definition 11,
$\mathit{seq}_{i}\in\rho_{\infty}(v^{*})$, where $\mathit{seq}_{i}=...\to
v_{i}$. By Lemma 10, either $\mathit{seq}\subseteq\mathit{seq}_{i}$ or
$\mathit{seq}\supset\mathit{seq}_{i}$. Therefore, $v^{\prime}\subseteq v_{i}$,
which implies that $v^{\prime}\subseteq v$. However, this contradicts the fact
that $v^{\prime}\supset v$. In this case, $v\subset v^{*}$.

  * •

Let $\alpha_{\infty}(v^{*})=\bot$. By Lemma 21, $v^{*}$ is an auxiliary view
for a view $v_{i}$. By Lemma 22, $v_{i}\subset v^{*}$. Since $v^{*}\subset v$,
$v_{i}\subset v$. Therefore, $v_{i}$ leads to a view $v_{i}^{\prime}$ at time
$\infty$ (by lemmas 16 and 19). Lemmas 18 and 24 show that
$v_{i}^{\prime}\subseteq v$.

Since $m^{*}\in\mathit{path}$, $\mathit{seq}\in\rho_{\infty}(v^{*})$, where
$\mathit{seq}=v^{\prime}\to...$. Moreover,
$\mathit{seq}^{\prime}\in\rho_{\infty}(v_{i})$, where
$\mathit{seq}^{\prime}=...\to v^{*}\to v^{\prime}\to...$ (by lemmas 33 and 31
and the fact that $v^{*}$ is an auxiliary view for $v_{i}$). On the other
hand, $\mathit{seq}_{i}^{\prime}\in\rho_{\infty}(v_{i})$, where
$\mathit{seq}_{i}^{\prime}=...\to v_{i}^{\prime}$ (since $v_{i}$ leads to
$v_{i}^{\prime}$ at time $\infty$ and Definition 1). By Lemma 10, either
$\mathit{seq}^{\prime}\subseteq\mathit{seq}_{i}^{\prime}$ or
$\mathit{seq}^{\prime}\supset\mathit{seq}_{i}^{\prime}$. Therefore,
$v^{\prime}\subseteq v_{i}^{\prime}$, which implies that $v^{\prime}\subseteq
v$. This statement contradicts the fact that $v^{\prime}\supset v$. Thus,
$v\subset v^{*}$ in this case, as well.

Since $v\subset v^{*}$, we reach the starting point of the lemma. The
recursion eventually stops since $\mathit{path}$ “contains” finitely many
views (by Theorem 48 and the fact that all views from $\mathit{path}$ are
valid), the smallest view that belongs to $\mathit{path}.\mathtt{views()}$ is
$\mathit{genesis}$ (see LABEL:lst:view_path and Lemma 46) and
$v\supseteq\mathit{genesis}$ (by Lemma 45). ∎

A direct consequence of Lemma 54 is that all installable views smaller than
the destination of a view-path are “contained” in the view-path.

###### Lemma 0.

Let $\mathit{path}\subseteq\mathcal{I}^{*}(\infty)$ such that
$\mathit{path}.\mathtt{destination()}=v^{\prime}$. Consider a view $v\subset
v^{\prime}$ such that $\alpha_{\infty}(v)=\top$. Then,
$v\in\mathit{path}.\mathtt{views()}$.

###### Proof.

Follows directly from Lemma 54. ∎

A direct consequence of Lemma 55 is that there does not exist an
$\mathtt{INSTALL}$ message $m$ such that (1) $m.\mathtt{source()}$ is a valid
view, and (2) $m.\mathtt{source()}\subset v\subset m.\mathtt{destination()}$,
where $v$ is a view installable at time $\infty$. We prove this result below.

###### Lemma 0.

Let a view $v$ be installable at time $\infty$ (i.e.,
$\alpha_{\infty}(v)=\top$). Then,
$[\mathtt{INSTALL},v^{\prime},\mathit{seq}^{\prime}=v^{\prime\prime}\to...,\omega]\notin\mathcal{I}^{*}(\infty)$,
where (1) $v^{\prime}$ is a valid view, and (2) $v^{\prime}\subset v\subset
v^{\prime\prime}$.

###### Proof.

Let
$m=[\mathtt{INSTALL},v^{\prime},\mathit{seq}^{\prime}=v^{\prime\prime}\to...,\omega]$.
By contradiction, let $m\in\mathcal{I}^{*}(\infty)$. Since $v^{\prime}$ is a
valid view, $v^{\prime}=\mathit{genesis}$ or there exists a view-path
$\mathit{path}\subseteq\mathcal{I}^{*}(\infty)$ such that
$\mathit{path}.\mathtt{destination()}=v^{\prime}$ (by Definition 1). Let us
consider both cases:

  * •

Let $v^{\prime}=\mathit{genesis}$. Let $\mathit{path}^{\prime}=[m]$. Hence,
$\mathit{path}^{\prime}$ is a view-path (see LABEL:lst:view_path) and
$\mathit{path}^{\prime}.\mathtt{destination()}=v^{\prime\prime}$. Moreover,
$\mathit{path}^{\prime}\subseteq\mathcal{I}^{*}(\infty)$.

  * •

Let $v^{\prime}\neq\mathit{genesis}$. Let
$\mathit{path}^{\prime}=\mathit{path}||m$. Hence, $\mathit{path}^{\prime}$ is
a view-path (see LABEL:lst:view_path) and
$\mathit{path}^{\prime}.\mathtt{destination()}=v^{\prime\prime}$. Moreover,
$\mathit{path}^{\prime}\subseteq\mathcal{I}^{*}(\infty)$.

Hence, $\mathit{path}^{\prime}\subseteq\mathcal{I}^{*}(\infty)$ exists such
that $\mathit{path}^{\prime}.\mathtt{destination()}=v^{\prime\prime}\supset v$
and $v\notin\mathit{path}^{\prime}.\mathtt{views()}$. This contradicts Lemma
55, which concludes the proof. ∎

Next, we prove that $\mathit{install\\_messages}$ variables of two forever-
correct servers are eventually identical.

###### Lemma 0.

Let servers $r$ and $r^{\prime}$ be forever-correct. Then,
$\mathit{install\\_messages}_{r}=\mathit{install\\_messages}_{r^{\prime}}$,
where $\mathit{install\\_messages}_{r}$ (resp.,
$\mathit{install\\_messages}_{r^{\prime}}$) denotes the value of the
$\mathit{install\\_messages}$ variable at server $r$ (resp., $r^{\prime}$) at
time $\infty$.

###### Proof.

First, $|\mathit{install\\_messages}_{r}|<\infty$ and
$|\mathit{install\\_messages}_{r^{\prime}}|<\infty$, which follows from the
fact that only finitely many valid views exist (by Theorem 48) and from the
fact that $|\rho_{\infty}(v)|<\infty$, for every valid view $v$ (by Lemma 49).
Then, the lemma follows from the fact that all messages inserted into the
$\mathit{install\\_messages}$ variable at a correct server are gossiped (at
line 12) of LABEL:lst:storage_processing). ∎

Now, we prove that a correct server eventually gets “prepared” for a view,
i.e., a correct server eventually sets its
$\mathit{reconfiguration}.\mathit{prepared}$ variable to $\top$. The next
lemma assumes that all correct servers send the “valid” state according to the
$\mathtt{verify}$ function (see line 16 of
LABEL:lst:reconfiguration_state_transfer). We prove that this is indeed the
case in Lemma 12.

###### Lemma 0 (Eventual Preparedness).

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

###### Proof.

By contradiction, suppose that $\mathit{reconfiguration}.\mathit{prepared}$ is
never set to $\top$ at server $r$. Hence, $r$ gossips the
$\mathtt{STATE-REQUEST}$ message at line 13 of
LABEL:lst:reconfiguration_view_transition. Moreover, since $r$ has entered the
pseudocode at line 3 of LABEL:lst:reconfiguration_view_transition, there
exists a valid view $v_{r}$ such that $r\in v_{r}.\mathtt{members()}$. Hence,
the $\mathtt{JOIN}$ message was sent by $r$ (by checks at lines 16 and 52 of
LABEL:lst:view_set_evidence_valid), which implies that $r$ has requested to
join. Since $r$ is correct, $r$ does not halt before leaving (see § 3.3,
paragraph “Server’s rules”). Because
$\mathit{reconfiguration}.\mathit{prepared}$ is never set to $\top$ by server
$r$ (by the assumption), $r$ never leaves. Therefore, $r$ never halts, which
means that $r$ is forever-correct. Now, suppose that
$\mathit{reconfiguration}.\mathit{source}=v$ and
$\mathit{reconfiguration}.\mathit{sequence}=\mathit{seq}$ at server $r$.

Eventually, the rule at line 3 of LABEL:lst:reconfiguration_state_transfer is
active at every forever-correct server (follows from Lemma 57). We now
separate two possibilities:

  * •

If $v.\mathtt{quorum()}$ correct members of $v$ are forever-correct, then
these servers send the $\mathtt{STATE-UPDATE}$ message to $r$ at line 14 of
LABEL:lst:reconfiguration_state_transfer and these messages are received by
$r$. Therefore, the rule at line 40 of
LABEL:lst:reconfiguration_state_transfer is eventually active at server $r$
and $r$ sets its $\mathit{reconfiguration}.\mathit{prepared}$ variable to
$\top$ in this case.

  * •

Otherwise, a correct member of $v$ halts; let $r^{\prime}\in
v.\mathtt{members()}$ be a correct server that halts. Since $r^{\prime}\in
v.\mathtt{members()}$, $r^{\prime}$ has requested to join (by checks at lines
16 and 52 of LABEL:lst:view_set_evidence_valid). Therefore, $r^{\prime}$
leaves (see § 3.3, paragraph “Server’s rules”), which implies that
$r^{\prime}$ executes line 55 of LABEL:lst:reconfiguration_view_transition.
Prior to leaving, $\mathit{reconfiguration}.\mathit{discharged}=\top$ (line 22
of LABEL:lst:reconfiguration_view_transition) and
$\mathit{dischargement}.\mathit{dischargement\\_view}=v^{\prime}$, for some
valid view $v^{\prime}\supset v$, at server $r^{\prime}$. This means that
$r^{\prime}$ has, before leaving, received $\mathtt{DISCHARGEMENT-CONFIRM}$
messages associated with a view $v^{*}$, where $v^{*}\supseteq v^{\prime}$ and
$v^{*}$ is a valid view, from a quorum of members of $v^{*}$ (line 11 of
LABEL:lst:reconfiguration_view_dischargement). Let $C$ denote the subset of
servers from which $r^{\prime}$ has received the $[\mathtt{DISCHARGEMENT-
CONFIRM},v^{*}]$ messages such that, for every server $c\in C$, $c$ is
correct; note that $|C|\geq v^{*}.\mathtt{plurality()}$. We separate two
cases:

    * –

At least $v^{*}.\mathtt{plurality}()$ of servers that belong to $C$ are
forever-correct. In this case, these servers eventually send the
$\mathtt{STATE-UPDATE}$ message while their
$\mathit{current\\_view}.\mathit{view}$ variable is greater than or equal to
$v^{*}$ (this holds due to the fact that these servers eventually set their
$\mathit{current\\_view}.\mathit{view}$ variable to $v^{*}$ and the
$\mathit{current\\_view}.\mathit{view}$ variable of a correct server is only
updated with greater values). Moreover, $v^{*}\in\mathit{history}$ at server
$r$ eventually (due to Lemma 57). Hence, the rule at line 46 of
LABEL:lst:reconfiguration_state_transfer is eventually active at server $r$,
which ensures that $r$ sets its $\mathit{reconfiguration}.\mathit{prepared}$
variable to $\top$.

    * –

Otherwise, there exists a server $c\in C$ that leaves (i.e., executes line 11
of LABEL:lst:reconfiguration_view_dischargement). Prior to leaving,
$\mathit{reconfiguration}.\mathit{discharged}=\top$ (line 22 of
LABEL:lst:reconfiguration_view_transition) and
$\mathit{dischargement}.\mathit{dischargement\\_view}=v^{\prime\prime}$, for
some valid view $v^{\prime\prime}\supset v^{*}$. Since $v^{*}\supset v$,
$v^{\prime\prime}\supset v$. Hence, we apply the same reasoning as done
towards $v^{\prime}$. Such recursion eventually stops due to the fact that
there exist only finitely many valid views (by Theorem 48), which means that
$r$ eventually sets its $\mathit{reconfiguration}.\mathit{prepared}$ variable
to $\top$.

Since we reach contradiction,
$\mathit{reconfiguration}.\mathit{prepared}=\top$ at server $r$ eventually and
the lemma holds. ∎

The next two results show that some specific views are forever-alive
(Definition 2). Recall that, given definitions 1 and 2, all forever-alive
views are valid.

###### Lemma 0.

Let a correct server $r\in v.\mathtt{members}()$ set its
$\mathit{current\\_view}.\mathit{view}$ variable to $v$. Then, a view
$v^{\prime}\supseteq v$ is forever-alive.

###### Proof.

If $v=\mathit{genesis}$, $v$ is forever-alive by Definition 2. Hence, the
lemma trivially holds in this case.

Let $v\neq\mathit{genesis}$. Since $r$ sets its
$\mathit{current\\_view}.\mathit{view}$ variable to $v$,
$v\in\mathit{history}$ at server $r$ (by Lemma 3). By Lemma 4, there exists a
view-path $\mathit{path}\subseteq\mathit{install\\_messages}$ (at server $r$)
such that $\mathit{path}.\mathtt{destination()}=v$. Moreover, all messages
that belong to $\mathit{path}$ are gossiped at line 12 of
LABEL:lst:storage_processing. If $r$ is forever-correct, Definition 2 is
satisfied for $v$. Thus, the lemma holds in this case.

Otherwise, server $r$ halts. Since $r\in v.\mathtt{members()}$ and $v$ is a
valid view (since $v\in\mathit{history}$ at server $r$, $v$ is valid according
to Lemma 5), server $r$ leaves (see § 3.3, paragraph “Server’s rules”) at line
55 of LABEL:lst:reconfiguration_view_transition. Moreover,
$v\supset\mathit{genesis}$ (by Lemma 45). This means that $r$ learns from a
correct server $r^{\prime}$ that $r^{\prime}$’s
$\mathit{current\\_view}.\mathit{view}$ variable is set to some valid view
$v^{\prime}\supset v$ (see LABEL:lst:reconfiguration_view_transition and
LABEL:lst:reconfiguration_view_dischargement), where $r\notin
v^{\prime}.\mathtt{members()}$ and $r^{\prime}\in
v^{\prime}.\mathtt{members()}$.

By Lemma 3, $v^{\prime}\in\mathit{history}$ at server $r^{\prime}$. By Lemma
4, there exists a view-path
$\mathit{path}^{\prime}\subseteq\mathit{install\\_messages}$ (at server
$r^{\prime}$) such that
$\mathit{path}^{\prime}.\mathtt{destination()}=v^{\prime}$. Moreover, all
messages that belong to $\mathit{path}^{\prime}$ are gossiped at line 12 of
LABEL:lst:storage_processing by server $r^{\prime}$. If $r^{\prime}$ is
forever-correct, Definition 2 is satisfied for $v^{\prime}\supset v$ and the
lemma holds. Otherwise, server $r^{\prime}$ halts and we apply the same
reasoning as done towards server $r$. The recursion eventually stops due to
the fact that only finitely many valid views exist (by Theorem 48), which
implies that a view greater than $v$ is forever-alive if server $r$ halts (and
leaves). Thus, the lemma holds. ∎

###### Lemma 0.

Let a correct server $r$ enter the pseudocode at line 3 of
LABEL:lst:reconfiguration_view_transition with $\mathit{joined}=\top$. Then, a
view $v^{\prime}\supseteq v$ is forever-alive141414View $v$ is the view
specified at line 3 of LABEL:lst:reconfiguration_view_transition..

###### Proof.

We start by observing that $v\neq\mathit{genesis}$. This statement follows
from the fact that $\mathit{genesis}$ is the smallest valid view (by Lemma
45). If $r\in v.\mathtt{members}()$, then eventually
$\mathit{current\\_view}.\mathit{view}=v$ at server $r$ (by Lemma 58).
Therefore, the lemma follows from Lemma 59.

Otherwise, we distinguish two possibilities:

  * •

If $r$ never leaves, then $r$ is forever-correct (see § 3.3, paragraph
“Server’s rules”). Since $v\in\mathit{history}$ at server $r$ (due to the
check at line 3 of LABEL:lst:reconfiguration_view_transition), Lemma 4 shows
(since $v\neq\mathit{genesis}$) that there exists a view-path
$\mathit{path}\subseteq\mathit{install\\_messages}$ (at server $r$) such that
$\mathit{path}.\mathtt{destination()}=v$. Since all messages that belong to
$\mathit{path}$ are gossiped (at line 12 of LABEL:lst:storage_processing) by
server $r$, $v$ is forever-alive (by Definition 2). Therefore, the lemma holds
in this case.

  * •

If $r$ leaves, there exists a correct server $r^{\prime}\in
v^{\prime}.\mathtt{members()}$, where $v^{\prime}\supseteq v$, that sets its
$\mathit{current\\_view}.\mathit{view}$ variable to $v^{\prime}$ (see
LABEL:lst:reconfiguration_view_transition and
LABEL:lst:reconfiguration_view_dischargement). Hence, the lemma follows from
Lemma 59.

The proof is concluded since the lemma holds in all possible cases. ∎

The next lemma proves that a correct member of a forever-alive view sets its
$\mathit{current\\_view}.\mathit{view}$ variable to that view or there exists
a greater view which is forever-alive.

###### Lemma 0.

Let $v$ be a forever-alive view. Then, a correct server $r\in
v.\mathtt{members()}$ eventually sets its
$\mathit{current\\_view}.\mathit{view}$ variable to $v$ or a view
$v^{\prime}\supset v$ is forever-alive.

###### Proof.

If $v=\mathit{genesis}$, the lemma trivially holds since all correct members
of $v=\mathit{genesis}$ set their $\mathit{current\\_view}.\mathit{view}$
variable to $\mathit{genesis}$ (at line 40 of
LABEL:lst:reconfiguration_initialization).

Let $v\neq\mathit{genesis}$. Since $v$ is a forever-alive view, $v$ is a valid
view (by definitions 1 and 2). Because $r\in v.\mathtt{members()}$, $r$ has
requested to join (by checks at lines 16 and 52 of
LABEL:lst:view_set_evidence_valid). Therefore, $r$ does not halt unless it has
previously left (see § 3.3, paragraph “Server’s rules”). Finally, since $v$ is
a forever-alive view, every forever-correct process eventually obtains a view-
path to $v$ (due to the validity property of the gossip primitive).

The lemma is satisfied if one of the following statements is true:

  1. (1)

Server $r$ sets its $\mathit{current\\_view}.\mathit{view}$ variable to $v$.

  2. (2)

Server $r$ sets its $\mathit{current\\_view}.\mathit{view}$ variable to
$v^{\prime}\supset v$. In this case, we know that a view $v^{*}\supseteq
v^{\prime}$ is forever-alive (by Lemma 59). Since $v^{*}\supset v$, the lemma
is indeed satisfied.

  3. (3)

Server $r$ enters the pseudocode at line 3 of
LABEL:lst:reconfiguration_view_transition with $\mathit{joined}=\top$, where
the “destination” view $v^{*}$ (i.e., view $v$ from the line 3 of
LABEL:lst:reconfiguration_view_transition; note that $v^{*}\neq v$) is greater
than $v$, i.e., $v\subset v^{*}$. By Lemma 60, a view greater than or equal to
$v^{*}$ is forever-alive. Since $v\subset v^{*}$, the lemma is satisfied.

By contradiction, suppose that none of the three statements is true. Hence,
$r$ never halts (since it never leaves due to the fact that the third
statement is not true). Hence, $r$ is forever-correct and $r$ eventually
obtains a view-path to $v$.

First, we prove that $r$ eventually joins. If
$r\in\mathit{genesis}.\mathtt{members}()$, $r$ joins at line 49 of
LABEL:lst:reconfiguration_initialization. Otherwise, since $r$ eventually
receives a view-path to $v$ and $r\notin\mathit{genesis}.\mathtt{members()}$,
the rule at line 3 of LABEL:lst:reconfiguration_view_transition becomes
eventually active and $r$ joins (because of Lemma 58). Once $r$ joins, $r$
sets its $\mathit{current\\_view}.\mathit{view}$ variable to $v_{r}$, where
$r\in v_{r}.\mathtt{members()}$. Moreover, $v_{r}\subset v$ (since the
aforementioned statements are assumed to not be true).

Next, server $r$ eventually enters the pseudocode at line 3 of
LABEL:lst:reconfiguration_view_transition since $r$ eventually obtains a view-
path to $v$ and $v_{r}\subset v$. Let $v_{r}^{\prime}$ be the “destination”
view (i.e., $\mathit{reconfiguration}.\mathit{destination}=v_{r}^{\prime}$
upon entering the pseudocode; set at line 4 of
LABEL:lst:reconfiguration_view_transition). Since the third statement is not
true, $v_{r}^{\prime}\subseteq v$. Suppose that $v_{r}^{\prime}=v$. By Lemma
58, $r$ eventually sets its $\mathit{current\\_view}.\mathit{view}$ variable
to $v$. This is impossible due to the fact that the first statement is not
true. Hence, $v_{r}^{\prime}\subset v$.

We know that $v_{r}\subset v_{r}^{\prime}$ (ensured by the check at line 3 of
LABEL:lst:reconfiguration_view_transition). Since $r\in
v_{r}.\mathtt{members()}$, $r\in v.\mathtt{members()}$ and $v_{r}\subset
v_{r}^{\prime}\subset v$, $r\in v_{r}^{\prime}.\mathtt{members()}$. Hence, $r$
eventually sets its $\mathit{current\\_view}.\mathit{view}$ variable to
$v_{r}^{\prime}\subset v$ (by Lemma 58).

We reach the same point as we have reached after $r$ has joined (and set its
$\mathit{current\\_view}.\mathit{view}$ variable to $v_{r}$). Thus, we apply
the same argument. Such recursion eventually stops due to the fact that only
finitely many valid views exist (by Theorem 48), which implies that only
finitely many valid views smaller than $v$ exist. Therefore, $r$ eventually
enters the pseudocode at line 3 of LABEL:lst:reconfiguration_view_transition
with the “destination” view greater than or equal to $v$. Once this happens,
either the first of the third statement is proven to be true, thus concluding
the proof of the lemma. ∎

The next lemma shows that all correct members of a forever-alive and
installable view eventually “transit” to that view.

###### Lemma 0.

Let $v$ be a forever-alive view such that $\alpha_{\infty}(v)=\top$. Then, a
correct server $r\in v.\mathtt{members()}$ eventually sets its
$\mathit{current\\_view}.\mathit{view}$ variable to $v$.

###### Proof.

If $v=\mathit{genesis}$, the lemma trivially holds since all correct members
of $v=\mathit{genesis}$ set their $\mathit{current\\_view}.\mathit{view}$
variable to $\mathit{genesis}$ (at line 40 of
LABEL:lst:reconfiguration_initialization).

Let $v\neq\mathit{genesis}$. Since $v$ is forever-alive, $v$ is a valid view
(by definitions 1 and 2). Because $r\in v.\mathtt{members()}$, $r$ has
requested to join (by checks at lines 16 and 52 of
LABEL:lst:view_set_evidence_valid). Hence, $r$ does not halt unless it has
previously left (see § 3.3, paragraph “Server’s rules”). Finally, since $v$ is
forever-alive, every forever-correct process eventually obtains a view-path to
$v$ (due to the validity property of the gossip primitive).

First, we prove that $r$ eventually joins. If
$r\in\mathit{genesis}.\mathtt{members()}$, $r$ joins at line 49 of
LABEL:lst:reconfiguration_initialization in this case. Let
$r\notin\mathit{genesis}.\mathtt{members()}$. By contradiction, suppose that
$r$ does not join. Hence, $r$ does not leave, which implies that $r$ does not
halt. Therefore, $r$ is forever-correct, which means that $r$ eventually
obtains a view-path to $v$. Furthermore, the rule at line 3 of
LABEL:lst:reconfiguration_view_transition becomes eventually active (since
$r\notin\mathit{genesis}.\mathtt{members()}$) and $r$ joins (by Lemma 58).
Once $r$ joins, $r$ sets its $\mathit{current\\_view}.\mathit{view}$ variable
to $v_{r}$, where $r\in v_{r}.\mathtt{members()}$.

Next, we prove that $v_{r}\subseteq v$. By contradiction, suppose that
$v_{r}\supset v$ (note that both $v_{r}$ and $v$ are valid and, thus,
comparable; Theorem 50). Let $\mathit{vr}^{\prime}=\mathit{source}[v_{r}]$ at
the moment of entering the pseudocode at line 3 of
LABEL:lst:reconfiguration_view_transition. Since $v_{r}^{\prime}\subset
v_{r}$, $r\in v_{r}.\mathtt{members()}$ and $r\notin
v_{r}^{\prime}.\mathtt{members()}$, $v_{r}^{\prime}\subset v$. Hence, Lemma 56
is contradicted. Therefore, $v_{r}\subseteq v$.

If $v_{r}=v$, the lemma holds. Otherwise, $v_{r}\subset v$. We prove that $r$
eventually enters the pseudocode at line 3 of
LABEL:lst:reconfiguration_view_transition. By contradiction, suppose that this
does not happen. Hence, $r$ does not leave, which implies that $r$ does not
halt (i.e., $r$ is forever-correct). Therefore, $r$ eventually obtains a view-
path to $v$, which means that $r$ eventually enters the pseudocode at line 3
of LABEL:lst:reconfiguration_view_transition, which represents contradiction.

Let $v_{r}^{\prime}$ be the “destination” view once $r$ enters the pseudocode
at line 3 of LABEL:lst:reconfiguration_view_transition. By Lemma 56,
$v_{r}^{\prime}\subseteq v$. Since $r\in v_{r}.\mathtt{members()}$, $r\in
v.\mathtt{members()}$ and $v_{r}\subset v_{r}^{\prime}\subseteq v$, $r\in
v_{r}^{\prime}.\mathtt{members()}$. By Lemma 58, $r$ eventually sets its
$\mathit{current\\_view}.\mathit{view}$ variable to $v_{r}^{\prime}$.

If $v_{r}^{\prime}=v$, the lemma holds. Otherwise, we reach the same point as
we have reached after $r$ has joined (and set its
$\mathit{current\\_view}.\mathit{view}$ variable to $v_{r}$). Thus, we apply