amaury_joly/bwconsistency
1
0
Fork 0
Code Issues 5 Pull Requests Packages Projects 3 Releases Wiki Activity

Compare commits

base: amaury_joly:55fa76a2720b108a4e8efaff49c63fac43bbab40
Branches Tags
amaury_joly:main amaury_joly:main_old amaury_joly:master
...
compare: amaury_joly:9a9d7af09836cc160b7365ef6336bbb0bd8b4fcf
Branches Tags
amaury_joly:main amaury_joly:main_old amaury_joly:master

3 Commits
55fa76a272 ... 9a9d7af098

Author SHA1 Message Date
Amaury JOLY
9a9d7af098 redaction des lemmes + preuve 2026-03-05 10:52:29 +00:00
Amaury JOLY
61282a0737 refactoring 2026-03-04 18:38:08 +00:00
Amaury JOLY
e4e3abad91 refacto preuve crash 2026-03-03 12:36:34 +00:00
5 changed files with 330 additions and 294 deletions
Expand all files Collapse all files

2
Recherche/BFT-ARBover/2_Primitives/index.tex
View File

@@ -2,7 +2,7 @@
\RB provides the following properties in the model.
\begin{itemize}[leftmargin=*]
\item \textbf{Integrity}: Every message received was previously sent. $\forall p_i:\ m = \RBreceived_i() \Rightarrow \exists p_j:\ \RBcast_j(m)$.
\item \textbf{Integrity}: Every message received was previously sent. $\forall p_i:\ m = \rbreceived_i() \Rightarrow \exists p_j:\ \RBcast_j(m)$.
\item \textbf{No-duplicates}: No message is received more than once at any process.
\item \textbf{Validity}: If a correct process broadcasts $m$, every correct process eventually receives $m$.
\end{itemize}

237
Recherche/BFT-ARBover/4_ARB_with_RB_DL/index.tex
View File

@@ -1,7 +1,6 @@
We present below an example of implementation of Atomic Reliable Broadcast (\ARB) using a Reliable Broadcast (\RB) primitive and a DenyList (\DL) object according to the model and notations defined in Section 2.
\subsection{Algorithm}
% granularité diff commentaire de code et paragraphe pre algo
\begin{definition}[Closed round]\label{def:closed-round}
Given a \DL{} linearization $H$, a round $r\in\mathcal{R}$ is \emph{closed} in $H$ if $H$ contains an operation $\APPEND(r)$.
@@ -18,52 +17,48 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
\SetKwBlock{LocalVars}{Local Variables:}{}
\LocalVars{
$\mathit{unordered} \gets \emptyset$,
$\mathit{ordered} \gets \epsilon$,
$\mathit{delivered} \gets \epsilon$\;
$\mathit{prop}[r][j] \gets \bot,\ \forall r,j$\;
$\unordered \gets \emptyset$,
$\ordered \gets \epsilon$,
$\delivered \gets \epsilon$\;
$\prop[r][j] \gets \bot,\ \forall r,j$\;
}
\vspace{0.3em}
\For{$r = 1, 2, \ldots$}{
\textbf{wait until} $\mathit{unordered} \setminus \mathit{ordered} \neq \emptyset$\;
$S \leftarrow (\mathit{unordered} \setminus \mathit{ordered})$\;\nllabel{code:Sconstruction}
$\RBcast(S, r, i)$; $\PROVE(r)$; $\APPEND(r)$\;\nllabel{code:submit-proposition}
\textbf{wait until} $\unordered \setminus \ordered \neq \emptyset$\;
$S \leftarrow (\unordered \setminus \ordered)$\;\nllabel{code:Sconstruction}
$\RBcast(\texttt{PROP}, S, \langle r, i \rangle)$; $\PROVE(r)$; $\APPEND(r)$\;\nllabel{code:submit-proposition}
$\mathit{winners}_r \gets \{(j,r): (j,r) \in \READ()\}$\;
\textbf{wait until} $\mathit{winners}_r \neq \emptyset$\;\nllabel{code:check-if-winners}
$\winners[r] \gets \{ j : (j, r) \in \READ() \}$\;\nllabel{code:Wcompute}
$\APPEND(r)$\;\nllabel{code:append-read}
$W_r \gets \{ j : (j, r) \in \READ() \}$\;\nllabel{code:Wcompute}
\textbf{wait until} $\forall j \in \winners[r],\ \prop[r][j] \neq \bot$\;\nllabel{code:check-winners-ack}
\textbf{wait until} $\forall j \in W_r,\ \mathit{prop}[r][j] \neq \bot$\;\nllabel{code:check-winners-ack}
$M_r \gets \bigcup_{j \in W_r} \mathit{prop}[r][j]$\;\nllabel{code:Mcompute}
$\mathit{ordered} \leftarrow \mathit{ordered} \cdot \ordered(M_r)$\;\nllabel{code:next-msg-extraction}
$M \gets \bigcup_{j \in \winners[r]} \prop[r][j]$\;\nllabel{code:Mcompute-dl}
$\ordered \leftarrow \ordered \cdot \ordered(M)$\;\nllabel{code:next-msg-extraction}
}
\vspace{0.3em}
\Upon{$\ABbroadcast(m)$}{
$\mathit{unordered} \gets \mathit{unordered} \cup \{m\}$\;
$\unordered \gets \unordered \cup \{m\}$\;\nllabel{code:abbroadcast-add}
}
\vspace{0.3em}
\Upon{$\textsf{rdeliver}(S, r, j)$ from process $p_j$}{
$\mathit{unordered} \leftarrow \mathit{unordered} \cup \{S\}$\;\nllabel{code:receivedConstruction}
$\mathit{prop}[r][j] \leftarrow S$\;\nllabel{code:prop-set}
\Upon{$\rdeliver(\texttt{PROP}, S, \langle r, j \rangle)$ from process $p_j$}{
$\unordered \leftarrow \unordered \cup \{S\}$\;\nllabel{code:receivedConstruction}
$\prop[r][j] \leftarrow S$\;\nllabel{code:prop-set}
}
\vspace{0.3em}
\Upon{$\ABdeliver()$}{
\If{$\mathit{ordered} \setminus \mathit{delivered} = \emptyset$}{
\If{$\ordered \setminus \delivered = \emptyset$}{
\Return{$\bot$}
}
$m \gets (\mathit{ordered} \setminus \mathit{delivered})[0]$\;\nllabel{code:adeliver-extract}
$\mathit{delivered} \gets \mathit{delivered} \cdot m$\;
let $m$ be the first element in $(\ordered \setminus \delivered$)\;\nllabel{code:adeliver-extract}
$\delivered \gets \delivered \cdot m$\;\nllabel{code:adeliver-mark}
\Return{$m$}
}
@@ -92,45 +87,17 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
\end{lemma}
\begin{proof}
\emph{Base.} For a closed round $r=0$, the set $\{r' \in \mathcal{R},\ r' < r\}$ is empty, hence the lemma is true.
\emph{Base.} For a closed round $r=0$, the set $\{r' \in \mathcal{R} : r' < r\}$ is empty, so the claim holds.
\emph{Induction.} Assume the lemma is true for round $r\geq 0$, we prove it for round $r+1$.
\smallskip
Assume $r+1$ is closed and by \cref{def:first-append} $\APPEND^{(\star)}(r+1)$ be the earliest $\APPEND(r+1)$ in the DL linearization $H$.
By Lemma 1, after an $\APPEND(r)$ were in $H$, any later $\PROVE(r)$ will be invalid also, a process’s program order is preserved in $H$.
There are two possibilities for where $\APPEND^{(\star)}(r+1)$ is invoked.
\emph{Induction step.} Assume $r+1$ is closed. By \cref{def:first-append}, there exists an earliest operation $\APPEND^{(\star)}(r+1)$ in the \DL linearization $H$. Let $p_j$ be the process that invokes this operation.
\begin{itemize}
\item \textbf{Case Algorithm \ref{alg:arb-crash} :}
Some process executes the loop at \ref{code:sumbited-check-loop} and invokes $\PROVE(r+1);\APPEND^{(\star)}(r+1)$ at line~\ref{code:submit-proposition}. Let $p_i$ be this process.
Immediately before line~\ref{code:submit-proposition}, line~\ref{code:round-increment} sets $r\leftarrow r+1$, so the previous loop iteration targeted $r$. We consider two sub-cases.
\begin{itemize}
\item \emph{(i) $p_i$ is not in its first loop iteration.}
In the previous iteration, $p_i$ executed $\PROVE_i(r)$ at \ref{code:submit-proposition}, followed (in program order) by $\APPEND_i(r)$.
If round $r$ wasn't closed when $p_i$ execute $\PROVE_i(r)$ at \ref{code:submit-proposition}, then the condition at \ref{code:sumbited-check-loop} would be true hence the tuple $(i, r)$ should be visible in P which implies that $p_i$ should leave the loop at round $r$, contradicting the assumption that $p_i$ is now executing another iteration.
Since the tuple is not visible, the $\PROVE_i(r)$ was invalid which implies by definition that an $\APPEND(r)$ already exists in $H$. Thus in this case $r$ is closed.
\item \emph{(ii) $p_i$ is in its first loop iteration.}
To compute the value $r_{max}$, $p_i$ must have observed one or many $(\_ , r+1)$ in $P$ at \ref{code:rmax-compute}, issued by some processes (possibly different from $p_i$). Let's call $p_j$ the issuer of the first $\PROVE_j(r+1)$ in the linearization $H$. \\
When $p_j$ executed $P \gets \READ()$ at \ref{code:set-up-read} and compute $r_{max}$ at \ref{code:rmax-compute}, he observed no tuple $(\_,r+1)$ in $P$ because he's the issuer of the first one. So when $p_j$ executed the loop (\ref{code:sumbited-check-loop}), he run it for the round $r$, didn't seen any $(j,r)$ in $P$ at B6, and then executed the first $\PROVE_j(r+1)$ at \ref{code:submit-proposition} in a second iteration. \\
If round $r$ wasn't closed when $p_j$ execute $\PROVE_j(r)$ at \ref{code:submit-proposition}, then the $(j, r)$ will be in $P$ and the condition at \ref{code:sumbited-check-loop} should be true which implies that $p_j$ sould leave the loop at round $r$, contradicting the assumption that $p_j$ is now executing $\PROVE_j(r+1)$. In this case $r$ is closed.
\end{itemize}
\item \textbf{Case Algorithm \ref{alg:arb-crash} :}
Some process invokes $\APPEND(r+1)$ at \ref{code:append-read}. Let $p_i$ be this process.
Line~\ref{code:append-read} is guarded by the condition at \ref{code:check-if-winners}, which ensures that $p_i$ observed some $(\_,r+1)$ in $P$. Let $p_j$ be the issuer of the first $\PROVE_j(r+1)$ in the linearization $H$.
When $p_j$ executed $\PROVE_j(r+1)$ at \ref{code:submit-proposition}, he observed no tuple $(\_,r+1)$ in $P$ at \ref{code:check-if-winners} because he's the issuer of the first one. By the same reasoning as in the Case Algorithm \ref{alg:arb-crash} (ii), $p_j$ must have observed that the round $r$ was closed.
% Line C7 is guarded by the presence of $\PROVE(r)$ in $P$ with $r=r+1$ (C5).
% Moreover, the local pointer $\textit{next}$ grow by increment of 1 and only advances after finishing the current round (C17), so if a process can reach $\textit{next}=r+1$ it implies that he has completed round $r$, which includes closing $r$ at C8 when $\PROVE(r)$ is observed.
% Hence $\APPEND^\star(r+1)$ implies a prior $\APPEND(r)$ in $H$, so $r$ is closed.
\end{itemize}
\smallskip
In all cases, $r+1$ closed implies $r$ closed. By induction on $r$, if the lemma is true for a closed $r$ then it is true for a closed $r+1$.
Therefore, the lemma is true for all closed rounds $r$.
In Algorithm~\ref{alg:arb-crash}, the call to $\APPEND(\cdot)$ appears at line~\ref{code:submit-proposition}, inside the loop indexed by rounds $1,2,\ldots$. Therefore, if $p_j$ reaches line~\ref{code:submit-proposition} for round $r+1$, then in the previous loop iteration (round $r$) process order implies that $p_j$ has already invoked $\APPEND(r)$ at the same line.
Hence an $\APPEND(r)$ exists in $H$, so round $r$ is closed by \cref{def:closed-round}. We proved:
\[
(r+1\ \text{closed}) \Rightarrow (r\ \text{closed}).
\]
By repeated application, if some round $r$ is closed, then every round $r' < r$ is also closed.
\end{proof}
\begin{definition}[Winner Invariant]\label{def:winner-invariant}
@@ -154,61 +121,46 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
\end{proof}
\begin{lemma}[Well-defined winners]\label{lem:winners}
For any correct process $p_i$ and round $r$, if $p_i$ computes $W_r$ at line~\ref{code:Wcompute}, then :
For any correct process $p_i$ and round $r$, if $p_i$ computes $\winners[r]$ at line~\ref{code:Wcompute}, then :
\begin{itemize}
\item $\Winners_r$ is defined;
\item the computed $W_r$ is exactly $\Winners_r$.
\item the computed $\winners[r]$ is exactly $\Winners_r$.
\end{itemize}
\end{lemma}
\begin{proof}
Lets consider a correct process $p_i$ that reach line~\ref{code:Wcompute} to compute $W_r$. \\
By program order, $p_i$ must have executed $\APPEND_i(r)$ at line~\ref{code:append-read} before, which implies by \Cref{def:closed-round} that round $r$ is closed at that point. So by \Cref{def:winner-invariant}, $\Winners_r$ is defined. \\
By \Cref{lem:closure-view}, all correct processes eventually observe the same set of valid tuples $(\_,r)$ in their \DL view. Hence, when $p_i$ executes the $\READ()$ at line~\ref{code:append-read} after the $\APPEND_i(r)$, it observes a set $P$ that includes all valid tuples $(\_,r)$ such that
Lets consider a correct process $p_i$ that reach line~\ref{code:Wcompute} to compute $\winners[r]$. \\
By program order, $p_i$ must have executed $\APPEND_i(r)$ at line~\ref{code:submit-proposition} before, which implies by \Cref{def:closed-round} that round $r$ is closed at that point. So by \Cref{def:winner-invariant}, $\Winners_r$ is defined. \\
By \Cref{lem:closure-view}, all correct processes eventually observe the same set of valid tuples $(\_,r)$ in their \DL view. Hence, when $p_i$ executes the $\READ()$ at line~\ref{code:Wcompute} after the $\APPEND_i(r)$, it observes a set $P$ that includes all valid tuples $(\_,r)$ such that
\[
W_r = \{ j : (j,r) \in P \} = \{j : \PROVE_j(r) \prec \APPEND^{(\star)}(r) \} = \Winners_r
\winners[r] = \{ j : (j,r) \in P \} = \{j : \PROVE_j(r) \prec \APPEND^{(\star)}(r) \} = \Winners_r
\]
\end{proof}
\begin{lemma}[No APPEND without PROVE]\label{lem:append-prove}
If some process invokes $\APPEND(r)$, then at least a process must have previously invoked $\PROVE(r)$.
\begin{lemma}[Winners are non-empty]\label{lem:nonempty}
For any closed round $r$, there exists at least one process $p_j$ that invoked $\PROVE_j(r) \prec \APPEND^\star(r)$, so $\Winners_r \neq \emptyset$.
\end{lemma}
\begin{proof}[Proof]
Consider the round $r$ such that some process invokes $\APPEND(r)$. There are two possible cases
Let $r$ be a closed round. By \Cref{def:closed-round}, some $\APPEND(r)$ occurs in the \DL linearization $H$. Let $p_i$ be the process invoking the earliest such operation, $\APPEND^{(\star)}(r)$.
\begin{itemize}
\item \textbf{Case (\ref{code:submit-proposition}) :}
There exists a process $p_i$ who's the issuer of the earliest $\APPEND^{(\star)}(r)$ in the DL linearization $H$. By program order, $p_i$ must have previously invoked $\PROVE_i(r)$ before invoking $\APPEND^{(\star)}(r)$ at line~\ref{code:submit-proposition}. In this case, there is at least one $\PROVE(r)$ valid in $H$ issued by a correct process before $\APPEND^{(\star)}(r)$.
\item \textbf{Case (\ref{code:append-read}) :}
There exists a process $p_i$ that invoked $\APPEND^{(\star)}(r)$ at . Line~\ref{code:append-read} is guarded by the condition at \ref{code:check-if-winners}, which ensures that $p$ observed some $(\_,r)$ in $P$. In this case, there is at least one $\PROVE(r)$ valid in $H$ issued by some process before $\APPEND^{(\star)}(r)$.
\end{itemize}
In both cases, if some process invokes $\APPEND(r)$, then some process must have previously invoked $\PROVE(r)$.
\end{proof}
\begin{lemma}[No empty winners]\label{lem:nonempty}
Let $r$ be a closed round, then $\Winners_r \neq \emptyset$.
\end{lemma}
\begin{proof}[Proof]
By \Cref{def:closed-round}, some $\APPEND(r)$ occurs in the DL linearization. \\
By \Cref{lem:append-prove}, at least one process must have invoked a valid $\PROVE(r)$ before $\APPEND^{(\star)}(r)$. Hence, there exists at least one $p_j$ such that $p_j$ invoked $\PROVE_j(r) \prec \APPEND^\star(r)$, so $\Winners_r \neq \emptyset$.
By program order in Algorithm~\ref{alg:arb-crash}, the call to $\APPEND(\cdot)$ at line~\ref{code:submit-proposition} is immediately preceded by $\PROVE(r)$. Thus $p_i$ must have invoked $\PROVE_i(r)$ before $\APPEND^{(\star)}(r)$, and by the sequence of code at line~\ref{code:submit-proposition}, this $\PROVE_i(r)$ executes before $\APPEND^{(\star)}(r)$ in the linearization.
By \Cref{def:winner-invariant}, $p_i \in \Winners_r$. Hence $\Winners_r \neq \emptyset$.
\end{proof}
\begin{lemma}[Winners must propose]\label{lem:winners-propose}
For any closed round $r$, $\forall i \in \Winners_r$, process $p_i$ must have invoked a $\RBcast(S^{(i)}, r, i)$ and hence any correct will eventually set $\prop[r][i]$ to a non-$\bot$ value.
For any closed round $r$, $\forall i \in \Winners_r$, process $p_i$ must have invoked a $\RBcast(PROP, S^{(i)}, \langle r, i \rangle)$ and hence any correct will eventually set $\prop[r][i]$ to a non-$\bot$ value.
\end{lemma}
\begin{proof}[Proof]
Fix a closed round $r$. By \Cref{def:winner-invariant}, for any $i \in \Winners_r$, there exist a valid $\PROVE_i(r)$ such that $\PROVE_i(r) \prec \APPEND^\star(r)$ in the DL linearization. By program order, if $i$ invoked a valid $\PROVE_i(r)$ at line~\ref{code:submit-proposition} he must have invoked $\RBcast(S^{(i)}, r, i)$ directly before.
Fix a closed round $r$. By \Cref{def:winner-invariant}, for any $i \in \Winners_r$, there exist a valid $\PROVE_i(r)$ such that $\PROVE_i(r) \prec \APPEND^\star(r)$ in the DL linearization. By program order, if $i$ invoked a valid $\PROVE_i(r)$ at line~\ref{code:submit-proposition} he must have invoked $\RBcast(PROP, S^{(i)}, \langle r, i \rangle)$ directly before.
Let take a correct process $p_j$, by \RB \emph{Validity}, every correct process eventually receives $i$'s \RB message for round $r$, which sets $\prop[r][i]$ to a non-$\bot$ value at line~\ref{code:prop-set}.
\end{proof}
\begin{definition}[Messages invariant]\label{def:messages-invariant}
For any closed round $r$ and any correct process $p_i$ such that $\forall j \in \Winners_r : prop^{[i)}[r][j] \neq \bot$, define
For any closed round $r$ and any correct process $p_i$ such that $\forall j \in \Winners_r : prop^{(i)}[r][j] \neq \bot$, define
\[
\Messages_r \triangleq \bigcup_{j\in\Winners_r} \prop^{(i)}[r][j]
\]
@@ -216,73 +168,70 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
\end{definition}
\begin{lemma}[Eventual proposal closure]\label{lem:eventual-closure}
If a correct process $p_i$ define $M_r$ at line~\ref{code:Mcompute}, then for every $j \in \Winners_r$, $\prop^{(i)}[r][j] \neq \bot$.
If a correct process $p_i$ define $M$ at line~\ref{code:Mcompute-dl}, then for every $j \in \Winners_r$, $\prop^{(i)}[r][j] \neq \bot$.
\end{lemma}
\begin{proof}[Proof]
Let take a correct process $p_i$ that computes $M_r$ at line~\ref{code:Mcompute}. By \Cref{lem:winners}, $p_i$ computation is the winner set $\Winners_r$.
Let take a correct process $p_i$ that computes $M$ at line~\ref{code:Mcompute-dl}. By \Cref{lem:winners}, $p_i$ computation is the winner set $\Winners_r$.
By \Cref{lem:nonempty}, $\Winners_r \neq \emptyset$. The instruction at line~\ref{code:Mcompute} where $p_i$ computes $M_r$ is guarded by the condition at line~\ref{code:check-winners-ack}, which ensures that $p_i$ has received all \RB messages from every winner $j \in \Winners_r$. Hence, $M_r = \bigcup_{j\in\Winners_r} \prop^{(i)}[r][j]$, we have $\prop^{(i)}[r][j] \neq \bot$ for all $j \in \Winners_r$.
By \Cref{lem:nonempty}, $\Winners_r \neq \emptyset$. The instruction at line~\ref{code:Mcompute-dl} where $p_i$ computes $M$ is guarded by the condition at line~\ref{code:check-winners-ack}, which ensures that $p_i$ has received all \RB messages from every winner $j \in \Winners_r$. Hence, $M = \bigcup_{j\in\Winners_r} \prop^{(i)}[r][j]$, we have $\prop^{(i)}[r][j] \neq \bot$ for all $j \in \Winners_r$.
\end{proof}
\begin{lemma}[Unique proposal per sender per round]\label{lem:unique-proposal}
For any round $r$ and any process $p_i$, $p_i$ invokes at most one $\RBcast(S, r, i)$.
For any round $r$ and any process $p_i$, $p_i$ invokes at most one $\RBcast(PROP, S, \langle r, i \rangle)$.
\end{lemma}
\begin{proof}[Proof]
By program order, any process $p_i$ invokes $\RBcast(S, r, i)$ at line~\ref{code:submit-proposition} must be in the loop \ref{code:sumbited-check-loop}. No matter the number of iterations of the loop, line~\ref{code:sumbited-check-loop} always uses the current value of $r$ which is incremented by 1 at each turn. Hence, in any execution, any process $p_i$ invokes $\RBcast(S, r, j)$ at most once for any round $r$.
In Algorithm~\ref{alg:arb-crash}, the only place where a process $p_i$ can invoke $\RBcast(PROP, S, \langle r, i \rangle)$ is at line~\ref{code:submit-proposition}, which appears inside the main loop indexed by rounds $r = 1, 2, \ldots$.
Each iteration of this loop processes exactly one round value $r$, and within that iteration, line~\ref{code:submit-proposition} is executed at most once. Since the loop variable $r$ takes each value $1, 2, \ldots$ at most once during the execution, process $p_i$ invokes $\RBcast(PROP, S, \langle r, i \rangle)$ at most once for any given round $r$.
\end{proof}
\begin{lemma}[Proposal convergence]\label{lem:convergence}
For any round $r$, for any correct processes $p_i$ that execute line~\ref{code:Mcompute}, we have
For any round $r$, for any correct processes $p_i$ that execute line~\ref{code:Mcompute-dl}, we have
\[
M_r^{(i)} = \Messages_r
M^{(i)} = \Messages_r
\]
\end{lemma}
\begin{proof}[Proof]
Let take a correct process $p_i$ that compute $M_r$ at line~\ref{code:Mcompute}. That implies that $p_i$ has defined $W_r$ at line~\ref{code:Wcompute}. It implies that, by \Cref{lem:winners}, $r$ is closed and $W_r = \Winners_r$. \\
By \Cref{lem:eventual-closure}, for every $j \in \Winners_r$, $\prop^{(i)}[r][j] \neq \bot$. By \Cref{lem:unique-proposal}, each winner $j$ invokes at most one $\RBcast(S^{(j)}, r, j)$, so $\prop^{(i)}[r][j] = S^{(j)}$ is uniquely defined. Hence, when $p_i$ computes
Let take a correct process $p_i$ that compute $M$ at line~\ref{code:Mcompute-dl}. That implies that $p_i$ has defined $\winners r$ at line~\ref{code:Wcompute}. It implies that, by \Cref{lem:winners}, $r$ is closed and $\winners_r = \Winners_r$. \\
By \Cref{lem:eventual-closure}, for every $j \in \Winners_r$, $\prop^{(i)}[r][j] \neq \bot$. By \Cref{lem:unique-proposal}, each winner $j$ invokes at most one $\RBcast(PROP, S^{(j)}, \langle r, j \rangle)$, so $\prop^{(i)}[r][j] = S^{(j)}$ is uniquely defined. Hence, when $p_i$ computes
\[
M_r^{(i)} = \bigcup_{j\in\Winners_r} \prop^{(i)}[r][j] = \bigcup_{j\in\Winners_r} S^{(j)} = \Messages_r.
M^{(i)} = \bigcup_{j\in\Winners_r} \prop^{(i)}[r][j] = \bigcup_{j\in\Winners_r} S^{(j)} = \Messages_r.
\]
\end{proof}
\begin{lemma}[Inclusion]\label{lem:inclusion}
If some correct process invokes $\ABbroadcast(m)$, then there exist a round $r$ and a process $j\in\Winners_r$ such that $p_j$ invokes
\[
\RBcast(S, r, j)\quad\text{for same S with}\quad m\in S.
\RBcast(PROP, S, \langle r, j \rangle)\quad\text{for some S with}\quad m\in S.
\]
\end{lemma}
\begin{proof}
Fix a correct process $p_i$ that invokes $\ABbroadcast(m)$ and eventually exits the loop (\ref{code:sumbited-check-loop}) at some round $r$. There are two possible cases.
Let $p_i$ be a correct process that invokes $\ABbroadcast(m)$. By the handler at line~\ref{code:abbroadcast-add}, $m$ is added to $\unordered$. Since $p_i$ is correct, it continues executing the main loop.
Consider any iteration of the loop where $p_i$ executes line~\ref{code:Sconstruction} while $m \in (\unordered \setminus \ordered)$. At that iteration, for some round $r$, process $p_i$ constructs $S$ containing $m$ and invokes $\RBcast(PROP, S, \langle r, i \rangle)$ at line~\ref{code:submit-proposition}.
We distinguish two cases:
\begin{itemize}
\item \textbf{Case 1:} $p_i$ exits the loop because $(i, r) \in P$. In this case, by \Cref{def:winner-invariant}, $p_i$ is a winner in round $r$. By program order, $p_i$ must have invoked $\RBcast(S, r, i)$ at \ref{code:submit-proposition} before invoking $\PROVE_i(r)$. By line~\ref{code:Sconstruction}, $m \in S$. Hence there exist a closed round $r$ and $p_i$ is a correct process such that $i\in\Winners_r$. Hence, $i$ invokes $\RBcast(S, r, i)$ with $m\in S$.
\item \textbf{Case 1: $p_i$ is a winner.} If $p_i \in \Winners_r$ for this round $r$, then by \Cref{def:winner-invariant} and program order, $p_i$ has invoked $\RBcast(PROP, S, \langle r, i \rangle)$ with $m \in S$, and the lemma holds with $j = i$.
\item \textbf{Case 2:} $p_i$ exits the loop because $\exists j, r': (j, r') \in P \wedge m \in \prop[r'][j]$. In this case, by \Cref{lem:winners-propose} and \Cref{lem:unique-proposal} $p_j$ must have invoked a unique $\RBcast(S, r', j)$. Which set $\prop^{(i)}[r'][j] = S$ with $m \in S$.
\item \textbf{Case 2: $p_i$ is not a winner.} If $p_i \notin \Winners_r$, then by the \RB \emph{Validity} property, all correct processes eventually \rdeliver $p_i$'s message. By line~\ref{code:receivedConstruction}, each correct process $p_k$ adds $m$ to its own $\unordered$ set. Hence every correct process will eventually attempt to broadcast $m$ in some subsequent round.
Since there are infinitely many rounds and finitely many processes, and by \Cref{lem:nonempty} every closed round has at least one winner, there must exist a round $r'$ and a correct process $p_j \in \Winners_{r'}$ such that $m \in (\unordered \setminus \ordered)$ when $p_j$ constructs its proposal $S$ at line~\ref{code:Sconstruction} for round $r'$. Hence $p_j$ invokes $\RBcast(PROP, S, \langle r', j \rangle)$ with $m \in S$.
\end{itemize}
In both cases, if some correct process invokes $\ABbroadcast(m)$, then there exist a round $r$ and a correct process $j\in\Winners_r$ such that $j$ invokes
\[
\RBcast(S, r, j)\quad\text{with}\quad m\in S.
\]
In both cases, there exists a round and a winner whose proposal includes $m$.
\end{proof}
\begin{lemma}[Broadcast Termination]\label{lem:bcast-termination}
A correct process which invokes $\ABbroadcast(m)$, eventually exits the function and returns.
A correct process which invokes $\ABbroadcast(m)$ eventually exits the function and returns.
\end{lemma}
\begin{proof}[Proof]
Consider a correct process $p_i$ that invokes $\ABbroadcast(m)$. The statement is true if $\exists r_1$ such that $r_1 \geq r_{max}$ and if $(i, r_1) \in P$; or if $\exists r_2$ such that $r_2 \geq r_{max}$ and if $\exists j: (j, r_2) \in P \wedge m \in \prop[r_2][j]$ (like guarded at B8).
Consider that there exists no round $r_1$ such that $p_i$ invokes a valid $\PROVE(r_1)$. In this case $p_i$ invokes infinitely many $\RBcast(S, \_, i)$ at line~\ref{code:submit-proposition} with $m \in S$ (line~\ref{code:Sconstruction}).\\
The assumption that no $\PROVE(r_1)$ invoked by $p$ is valid implies by \DL \emph{Validity} that for every round $r' \geq r_{max}$, there exists at least one $\APPEND(r')$ in the DL linearization, hence by \Cref{lem:nonempty} for every possible round $r'$ there at least a winner. Because there is an infinite number of rounds, and a finite number of processes, there exists at least one process $p_k$ that invokes infinitely many valid $\PROVE(r')$ and by extension infinitely many $\ABbroadcast(\_)$. By \RB \emph{Validity}, $p_k$ eventually receives $p_i$ 's \RB messages. Let call $t_0$ the time when $p_k$ receives $p_i$ 's \RB message. \\
At $t_0$, $p_k$ executes Algorithm \ref{alg:arb-crash} and sets $\mathit{received} \leftarrow \mathit{received} \cup \{S\}$ with $m \in S$ (line~\ref{code:receivedConstruction}).
For the first invocation of $\ABbroadcast(\_)$ by $p_k$ after the execution of \texttt{RReceived()}, $p_k$ must include $m$ in his proposal $S$ at line~\ref{code:Sconstruction} (because $m$ is pending in $j$'s $\received \setminus \delivered$ set). There exists a minimum round $r_2$ such that $p_k \in \Winners_{r_2}$ after $t_0$. By \Cref{lem:winners-propose}, eventually $\prop^{(i)}[r_2][k] \neq \bot$. By \Cref{lem:unique-proposal}, $\prop^{(i)}[r_2][k]$ is uniquely defined as the set $S$ proposed by $p_k$ at B6, which by \Cref{lem:inclusion} includes $m$. Hence eventually $m \in \prop^{(i)}[r_2][k]$ and $k \in \Winners_{r_2}$.
So if $p_i$ is a winner he satisfies the condition $(i, r_1) \in P$. And we show that if the first condition is never satisfied, the second one will eventually be satisfied. Hence either the first or the second condition will eventually be satisfied, and $p_i$ eventually exits the loop and returns from $\ABbroadcast(m)$.
By Algorithm~\ref{alg:arb-crash}, the handler for $\ABbroadcast(m)$ at line~\ref{code:abbroadcast-add} performs a single local operation: adding $m$ to the local set $\unordered$. This operation terminates immediately and the function returns.
\end{proof}
\begin{lemma}[Validity]\label{lem:validity}
@@ -292,14 +241,14 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
\begin{proof}[Proof]
Let $p_i$ a correct process that invokes $\ABbroadcast(m)$ and $p_q$ a correct process that infinitely invokes $\ABdeliver()$. By \Cref{lem:inclusion}, there exist a closed round $r$ and a correct process $j\in\Winners_r$ such that $p_j$ invokes
\[
\RBcast(S, r, j)\quad\text{with}\quad m\in S.
\RBcast(PROP, S, \langle r, j \rangle)\quad\text{with}\quad m\in S.
\]
By \Cref{lem:eventual-closure}, when $p_q$ computes $M_r$ at line~\ref{code:Mcompute}, $\prop[r][j]$ is non-$\bot$ because $j \in \Winners_r$. By \Cref{lem:unique-proposal}, $p_j$ invokes at most one $\RBcast(S, r, j)$, so $\prop[r][j]$ is uniquely defined. Hence, when $p_q$ computes
By \Cref{lem:eventual-closure}, when $p_q$ computes $M$ at line~\ref{code:Mcompute-dl}, $\prop[r][j]$ is non-$\bot$ because $j \in \Winners_r$. By \Cref{lem:unique-proposal}, $p_j$ invokes at most one $\RBcast(PROP, S, \langle r, j \rangle)$, so $\prop[r][j]$ is uniquely defined. Hence, when $p_q$ computes
\[
M_r = \bigcup_{k\in\Winners_r} \prop[r][k],
M = \bigcup_{k\in\Winners_r} \prop[r][k],
\]
we have $m \in \prop[r][j] = S$, so $m \in M_r$. By \Cref{lem:convergence}, $M_r$ is invariant so each computation of $M_r$ by a correct process includes $m$. At each invocation of $m' = \ABdeliver()$, $m'$ is added to $\delivered$ until $M_r \subseteq \delivered$. Once this happens we're assured that there exists an invocation of $\ABdeliver()$ which return $m$. Hence $m$ is well delivered.
we have $m \in \prop[r][j] = S$, so $m \in M$. By \Cref{lem:convergence}, $M$ is invariant so each computation of $M$ by a correct process includes $m$. At each invocation of $m' = \ABdeliver()$, $m'$ is added to $\delivered$ until $M \subseteq \delivered$. Once this happens we're assured that there exists an invocation of $\ABdeliver()$ which return $m$. Hence $m$ is well delivered.
\end{proof}
\begin{lemma}[No duplication]\label{lem:no-duplication}
@@ -309,7 +258,7 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
\begin{proof}
Let consider two invokations of $\ABdeliver()$ made by the same correct process which returns $m$. Let call these two invocations respectively $\ABdeliver^{(A)}()$ and $\ABdeliver^{(B)}()$.
When $\ABdeliver^{(A)}()$ occurs, by program order and because it reached line C18 to return $m$, the process must have add $m$ to $\delivered$. Hence when $\ABdeliver^{(B)}()$ reached line~\ref{code:next-msg-extraction} to extract the next message to deliver, it can't be $m$ because $m \not\in (M_r \setminus \{..., m, ...\})$. So a $\ABdeliver^{(B)}()$ which delivers $m$ can't occur.
When $\ABdeliver^{(A)}()$ occurs, by program order and because it reached line~\ref{code:adeliver-mark} to return $m$, the process must have add $m$ to $\delivered$. Hence when $\ABdeliver^{(B)}()$ reached line~\ref{code:adeliver-extract} to extract the next message to deliver, it can't be $m$ because $m \not\in (\ordered \setminus \delivered)$. So a $\ABdeliver^{(B)}()$ which delivers $m$ can't occur.
\end{proof}
\begin{lemma}[Total order]\label{lem:total-order}
@@ -317,48 +266,30 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
\end{lemma}
\begin{proof}
Consider a correct process that delivers both $m_1$ and $m_2$. By \Cref{lem:validity}, there exists a closed rounds $r'_1$ and $r'_2$ and correct processes $k_1 \in \Winners_{r'_1}$ and $k_2 \in \Winners_{r'_2}$ such that
Consider a correct process that delivers both $m_1$ and $m_2$. By \Cref{lem:validity}, there exists a closed rounds $r_1$ and $r_2$ and correct processes $k_1 \in \Winners_{r_1}$ and $k_2 \in \Winners_{r_2}$ such that
\[
\RBcast(S_1, r'_1, k_1)\quad\text{with}\quad m_1\in S_1,
\RBcast(PROP, S_1, \langle r_1, k_1 \rangle)\quad\text{with}\quad m_1\in S_1,
\]
\[
\RBcast(S_2, r'_2, k_2)\quad\text{with}\quad m_2\in S_2.
\RBcast(PROP, S_2, \langle r_2, k_2 \rangle)\quad\text{with}\quad m_2\in S_2.
\]
Let consider three cases :
Let consider two cases :
\begin{itemize}
\item \textbf{Case 1:} $r_1 < r_2$. By program order, any correct process must have waited to append in $\delivered$ every messages in $M_{r_1}$ (which contains $m_1$) to increment $\current$ and eventually set $\current = r_2$ to compute $M_{r_2}$ and then invoke the $ m_2 = \ABdeliver()$. Hence, for any correct process that delivers both $m_1$ and $m_2$, it delivers $m_1$ before $m_2$.
\item \textbf{Case 1:} $r_1 < r_2$. By program order, any correct process must have waited to append in $\delivered$ every messages in $M$ (which contains $m_1$) to increment $\current$ and eventually set $\current = r_2$ to compute $M$ and then invoke the $ m_2 = \ABdeliver()$. Hence, for any correct process that delivers both $m_1$ and $m_2$, it delivers $m_1$ before $m_2$.
\item \textbf{Case 2:} $r_1 = r_2$. By \Cref{lem:convergence}, any correct process that computes $M_{r_1}$ at line~\ref{code:Mcompute} computes the same set of messages $\Messages_{r_1}$. By line~\ref{code:next-msg-extraction} the messages are pull in a deterministic order defined by $\ordered(\_)$. Hence, for any correct process that delivers both $m_1$ and $m_2$, it delivers $m_1$ and $m_2$ in the deterministic order defined by $\ordered(\_)$.
\item \textbf{Case 2:} $r_1 = r_2$. By \Cref{lem:convergence}, any correct process that computes $M$ at line~\ref{code:Mcompute-dl} computes the same set of messages $\Messages_{r_1}$. By line~\ref{code:next-msg-extraction} the messages are pull in a deterministic order defined by $\ordered(\_)$. Hence, for any correct process that delivers both $m_1$ and $m_2$, it delivers $m_1$ and $m_2$ in the deterministic order defined by $\ordered(\_)$.
\end{itemize}
In all possible cases, any correct process that delivers both $m_1$ and $m_2$ delivers $m_1$ and $m_2$ in the same order.
\end{proof}
\begin{lemma}[Fifo Order]\label{lem:fifo-order}
For any two distints messages $m_1$ and $m_2$ broadcast by the same correct process $p_i$, if $p_i$ invokes $\ABbroadcast(m_1)$ before $\ABbroadcast(m_2)$, then any correct process $p_j$ that delivers both $m_1$ and $m_2$ delivers $m_1$ before $m_2$.
\end{lemma}
\begin{proof}
Let take $m_1$ and $m_2$ broadcast by the same correct process $p_i$, with $p_i$ invoking $\ABbroadcast(m_1)$ before $\ABbroadcast(m_2)$. By \Cref{lem:validity}, there exist closed rounds $r_1$ and $r_2$ such that $r_1 \leq r_2$ and correct processes $k_1 \in \Winners_{r_1}$ and $k_2 \in \Winners_{r_2}$ such that
\[
\RBcast(S_1, r_1, k_1)\quad\text{with}\quad m_1\in S_1,
\]
\[
\RBcast(S_2, r_2, k_2)\quad\text{with}\quad m_2\in S_2.
\]
By program order, $p_i$ must have invoked $\RBcast(S_1, r_1, i)$ before $\RBcast(S_2, r_2, i)$. By \Cref{lem:unique-proposal}, any process invokes at most one $\RBcast(S, r, i)$ per round, hence $r_1 < r_2$. By \Cref{lem:total-order}, any correct process that delivers both $m_1$ and $m_2$ delivers them in a deterministic order.
In all possible cases, any correct process that delivers both $m_1$ and $m_2$ delivers $m_1$ before $m_2$.
\end{proof}
\begin{theorem}[FIFO-\ARB]
Under the assumed $\DL$ synchrony and $\RB$ reliability, the algorithm implements FIFO Atomic Reliable Broadcast.
\begin{theorem}[\ARB]
Under the assumed $\DL$ synchrony and $\RB$ reliability, the algorithm implements Atomic Reliable Broadcast.
\end{theorem}
\begin{proof}
We show that the algorithm satisfies the properties of FIFO Atomic Reliable Broadcast under the assumed $\DL$ synchrony and $\RB$ reliability.
We show that the algorithm satisfies the properties of Atomic Reliable Broadcast under the assumed $\DL$ synchrony and $\RB$ reliability.
First, by \Cref{lem:bcast-termination}, if a correct process invokes $\ABbroadcast(m)$, then it eventually returns from this invocation.
Moreover, \Cref{lem:validity} states that if a correct process invokes $\ABbroadcast(m)$, then every correct process that invokes $\ABdeliver()$ infinitely often eventually delivers $m$.
@@ -371,11 +302,9 @@ Under the assumed $\DL$ synchrony and $\RB$ reliability, the algorithm implement
For the ordering guarantees, \Cref{lem:total-order} shows that for any two messages $m_1$ and $m_2$ delivered by correct processes, every correct process that delivers both $m_1$ and $m_2$ delivers them in the same order.
Hence all correct processes share a common total order on delivered messages.
Furthermore, \Cref{lem:fifo-order} states that for any two messages $m_1$ and $m_2$ broadcast by the same correct process, any correct process that delivers both messages delivers $m_1$ before $m_2$ whenever $m_1$ was broadcast before $m_2$.
Thus the global total order extends the per-sender FIFO order of $\ABbroadcast$.
All the above lemmas are proved under the assumptions that $\DL$ satisfies the required synchrony properties and that the underlying primitive is a Reliable Broadcast ($\RB$) with Integrity, No-duplicates and Validity.
Therefore, under these assumptions, the algorithm satisfies Validity, Integrity/No-duplicates, total order and per-sender FIFO order, and hence implements FIFO Atomic Reliable Broadcast, as claimed.
Therefore, under these assumptions, the algorithm satisfies Validity, Integrity/No-duplicates, and total order, and hence implements Atomic Reliable Broadcast, as claimed.
\end{proof}
\subsection{Reciprocity}

292
Recherche/BFT-ARBover/5_BFT_ARB/index.tex
View File

@@ -4,7 +4,7 @@ We consider a static set $\Pi$ of $n$ processes with known identities, communica
\paragraph{Synchrony.} The network is asynchronous.
\paragraph{Communication.} Processes can exchange through a Reliable Broadcast ($\RB$) primitive (defined below) which is invoked with the functions $\RBcast(m)$ and $m = \RBreceived()$. There exists a shared object called DenyList ($\DL$) (defined below) that is interfaced with a set $O$ of operations. There exist three types of these operations: $\APPEND(x)$, $\PROVE(x)$ and $\READ()$.
\paragraph{Communication.} Processes can exchange through a Reliable Broadcast ($\RB$) primitive (defined below) which is invoked with the functions $\RBcast(m)$ and $m = \rbreceived()$. The Reliable Broadcast is a Byzantine fault-tolerant primitive following Bracha's specification \cite{Bracha1987}: for any message $m$ broadcast by a process $p_j$, every correct process either receives the message $m$ or none at all; moreover, all correct processes that receive a broadcast from $p_j$ for a given sequence number or round receive exactly the same message. This ensures that Byzantine processes cannot send different messages to different correct processes for the same broadcast instance. There exists a shared object called DenyList ($\DL$) (defined below) that is interfaced with a set $O$ of operations. There exist three types of these operations: $\APPEND(x)$, $\PROVE(x)$ and $\READ()$.
\paragraph{Byzantine behaviour}
A process is said to exhibit Byzantine behaviour if it deviates arbitrarily from the prescribed algorithm. Such deviations may, for instance, consist in invoking primitives ($\RBcast$, $\APPEND$, $\PROVE$, etc.) with invalid inputs or inputs crafted maliciously, colluding with other Byzantine processes in an attempt to manipulate the system state or violate its guarantees, deliberately delaying or accelerating the delivery of messages to selected nodes so as to disrupt the expected timing of operations, or withholding messages and responses in order to induce inconsistencies in the system state.
@@ -65,21 +65,21 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au
\vspace{1em}
\Fn{$\BFTPROVE(x)$}{
$state \gets false$\;
$\state \gets false$\;
\For{\textbf{each } $U \in \mathcal{U}$}{
$state \gets state \textbf{ OR } DL_U.\PROVE(x)$\;\nllabel{code:prove-or}
$\state \gets \state \textbf{ OR } DL_U.\PROVE(x)$\;\nllabel{code:prove-or}
}
\Return{$state$}\;
\Return{$\state$}\;
}
\vspace{1em}
\Fn{$\BFTREAD()$}{
$results \gets \emptyset$\;
$\results \gets \emptyset$\;
\For{\textbf{each } $U \in \mathcal{U}$}{
$results \gets results \cup DL_U.\READ()$\;
$\results \gets \results \cup DL_U.\READ()$\;
}
\Return{$results$}\;
\Return{$\results$}\;
}
\end{algorithm}
@@ -92,7 +92,7 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au
\begin{itemize}
\item \textbf{Case (i): $|A|\ge t+1$.}
Fix any $U\in\mathcal{U}$. $A\cap U\neq\emptyset$. Pick $j\in A\cap U$. Since $j\in U$, the call $\BFTAPPEND_j(x)$ triggers $DL_U.\APPEND(x)$, and because $\BFTAPPEND_j(x)\prec op$ in $\Seq$, this induces a valid $DL_U.\APPEND(x)$ that appears before the induced $DL_U.\PROVE(x)$ by $p_i$. By \textbf{PROVE Validity} of $\DL$, the induced $DL_U.\PROVE(x)$ is invalid. As this holds for every $U\in\mathcal{U}$, there is \emph{no} component $DL_U$ where $\PROVE(x)$ is valid, so the field $state$ at line~\ref{code:prove-or} is never becoming true, and $op$ return false.
Fix any $U\in\mathcal{U}$. $A\cap U\neq\emptyset$. Pick $j\in A\cap U$. Since $j\in U$, the call $\BFTAPPEND_j(x)$ triggers $DL_U.\APPEND(x)$, and because $\BFTAPPEND_j(x)\prec op$ in $\Seq$, this induces a valid $DL_U.\APPEND(x)$ that appears before the induced $DL_U.\PROVE(x)$ by $p_i$. By \textbf{PROVE Validity} of $\DL$, the induced $DL_U.\PROVE(x)$ is invalid. As this holds for every $U\in\mathcal{U}$, there is \emph{no} component $DL_U$ where $\PROVE(x)$ is valid, so the field $\state$ at line~\ref{code:prove-or} is never becoming true, and $op$ return false.
\item \textbf{Case (ii): $|A|\le t$.}
There exists $U^\star\in\mathcal{U}$ such that $A\cap U^\star=\emptyset$. For any $j\in A$, we have $j\notin U^\star$, so $\BFTAPPEND_j(x)$ does \emph{not} call $DL_{U^\star}.\APPEND(x)$. Hence no valid $DL_{U^\star}.\APPEND(x)$ appears before the induced $DL_{U^\star}.\PROVE(x)$. Since also $i\in \Pi_V(DL_{U^\star})$, by \textbf{PROVE Validity} of $\DL$ the induced $DL_{U^\star}.\PROVE(x)$ is valid. Therefore, there exists a component with a valid $\PROVE(x)$, so $op$ is valid.
@@ -102,7 +102,7 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au
Combining the cases yields the claimed characterization of invalidity.
\end{proof}
\begin{lemma}[BFT-PROVE Anti-Flickering]
\begin{lemma}[BFT-PROVE Anti-Flickering]\label{lem:bft-prove-anti-flickering}
If the invocation of a operation $op = \BFTPROVE(x)$ by a correct process $p \in \Pi_V$ is invalid, then any $\BFTPROVE(x)$ operation that appears after $op$ in $\Seq$ is invalid.
\end{lemma}
@@ -131,7 +131,7 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au
$(i, x) \in R \implies \exists \BFTPROVE_i(x)$
\end{proof}
\begin{lemma}[BFT-READ Anti-Flickering]
\begin{lemma}[BFT-READ Anti-Flickering]\label{lem:bft-read-anti-flickering}
Let $op_1, op_2$ two $\BFTREAD()$ operations that returns respectively $R_1, R_2$. Iff $op_1 \prec op_2$ then $R_2 \subseteq R_1$. Otherwise $R_1 \subseteq R_2$.
\end{lemma}
@@ -177,150 +177,155 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au
\SetKwBlock{LocalVars}{Local Variables:}{}
\LocalVars{
$\mathit{unordered} \gets \emptyset$,
$\mathit{ordered} \gets \epsilon$,
$\mathit{delivered} \gets \epsilon$\;
$\mathit{prop}[r][j] \gets \bot, \forall j, r \in \Pi \times \mathbb{N}$\;
$\mathit{done}[r] \gets \emptyset, \forall r \in \mathbb{N}$\;
$\unordered \gets \emptyset$,
$\ordered \gets \epsilon$,
$\delivered \gets \epsilon$\;
$\prop[r][j] \gets \bot, \forall j, r \in \Pi \times \mathbb{N}$\;
$\done[r] \gets \emptyset, \forall r \in \mathbb{N}$\;
}
\vspace{0.3em}
\For{$r = 1, 2, \ldots$}{
\textbf{wait until} $\mathit{unordered} \setminus \mathit{ordered} \neq \emptyset$\;
$S \gets \mathit{unordered} \setminus \mathit{ordered}$;
\For{$r = 1, 2, \ldots$}{\nllabel{alg:main-loop}
\textbf{wait until} $\unordered \setminus \ordered \neq \emptyset$\;
$S \gets \unordered \setminus \ordered$;
$\RBcast(i, \texttt{PROP}, S, r)$\;
\textbf{wait until} $|\textsf{validated}(r)| \geq n - t$\;
\textbf{wait until} $|\validated(r)| \geq n - t$\;\nllabel{alg:check-validated}
\ForEach{$j \in \Pi$}{
$\BFTAPPEND(\langle j, r\rangle)$\;
\BlankLine
\lForEach{$j \in \Pi$}{
$\BFTAPPEND(\langle j, r\rangle)$\;\nllabel{alg:append}
}
\ForEach{$j \in \Pi$}{
$\textsf{send}(j, \texttt{DONE}, r)$\;
\lForEach{$j \in \Pi$}{
$\send(j, \texttt{DONE}, r)$\;
}
\textbf{wait until} $|\mathit{done}[r]| \geq n - t$\;
$\mathit{winners}[r] \gets \textsf{validated}(r)$\;
\BlankLine
\textbf{wait until} $\forall j \in \mathit{winners}[r],\ \mathit{prop}[r][j] \neq \bot$\;
$M \gets \bigcup_{j \in \mathit{winners}[r]} \mathit{prop}[r][j]$\;\nllabel{code:Mcompute}
$\mathit{ordered} \gets \mathit{ordered} \cdot \ordered(M)$\;
\textbf{wait until} $|\done[r]| \geq n - t$\;\nllabel{alg:check-done}
\textbf{wait until} $\forall j \in \winners[r],\ \prop[r][j] \neq \bot$ \textbf{ with } $\winners[r] \gets \validated(r)$\;
\BlankLine
$M \gets \bigcup_{j \in \winners[r]} \prop[r][j]$\;\nllabel{code:Mcompute}
$\ordered \gets \ordered \cdot \ordered(M)$\;
}
\vspace{0.3em}
\Fn{\textsf{validated}($r$)}{
\Fn{\validated($r$)}{
\Return{$\{j: |\{k: (k, r) \in \BFTREAD()\}| \geq t+1\}$}\;
}
\vspace{0.3em}
\Upon{$\ABbroadcast(m)$}{
$\mathit{unordered} \gets \mathit{unordered} \cup \{m\}$\;
$\unordered \gets \unordered \cup \{m\}$\;
}
\vspace{0.3em}
\Upon{$\textsf{rdeliver}(\texttt{PROP}, S, \langle j, r \rangle)$ from process $p_j$}{
$\mathit{unordered} \gets \mathit{unordered} \cup S$;
$\mathit{prop}[r][j] \gets S$\;
\Upon{$\rdeliver(\texttt{PROP}, S, \langle j, r \rangle)$ from process $p_j$}{
$\unordered \gets \unordered \cup S$;
$\prop[r][j] \gets S$\;
$\BFTPROVE(\langle j, r\rangle)$\;
}
\vspace{0.3em}
\Upon{$\textsf{receive}(\texttt{DONE}, r)$ from process $p_j$}{
$\mathit{done}[r] \gets \mathit{done}[r] \cup \{j\}$\;
\Upon{$\receive(\texttt{DONE}, r)$ from process $p_j$}{
$\done[r] \gets \done[r] \cup \{j\}$\;
}
\vspace{0.3em}
\Upon{$\ABdeliver()$}{
\If{$\mathit{ordered} \setminus \mathit{delivered} = \emptyset$}{
\lIf{$\ordered \setminus \delivered = \emptyset$}{
\Return{$\bot$}
}
let $m$ be the first message in $\mathit{ordered} \setminus \mathit{delivered}$\;
$\mathit{delivered} \gets \mathit{delivered} \cdot \{m\}$\;
let $m$ be the first message in $(\ordered \setminus \delivered)$\;
$\delivered \gets \delivered \cdot \{m\}$\;
\Return{$m$}
}
\end{algorithm}
\textbf{Everything below has to be updated}
% \textbf{Everything below has to be updated}
\begin{definition}[BFT Closed round for $k$]
Given $Seq^{k}$ the linearization of the $\BFTDL$ $Y[k]$, a round $r \in \mathcal{R}$ is \emph{closed} in $\Seq$ iff there exist at least $n - f$ distinct processes $j \in \Pi$ such that $\BFTAPPEND_j(r)$ appears in $\Seq^k$. Let call $\BFTAPPEND(r)^\star$ the $(n-f)^{th}$ $\BFTAPPEND(r)$.
\end{definition}
% \begin{definition}[BFT Closed round for $k$]
% Given $Seq^{k}$ the linearization of the $\BFTDL$ $Y[k]$, a round $r \in \mathcal{R}$ is \emph{closed} in $\Seq$ iff there exist at least $n - f$ distinct processes $j \in \Pi$ such that $\BFTAPPEND_j(r)$ appears in $\Seq^k$. Let call $\BFTAPPEND(r)^\star$ the $(n-f)^{th}$ $\BFTAPPEND(r)$.
% \end{definition}
\begin{definition}[BFT Closed round]\label{def:bft-closed-round}
A round $r \in \mathcal{R}$ is \emph{closed} iff for all $\DL[k]$, $r$ is closed in $\Seq^k$.
\end{definition}
% \begin{definition}[BFT Closed round]\label{def:bft-closed-round}
% A round $r \in \mathcal{R}$ is \emph{closed} iff for all $\DL[k]$, $r$ is closed in $\Seq^k$.
% \end{definition}
\subsection{Proof of correctness}
% \subsection{Proof of correctness}
\begin{remark}[BFT Stable round closure]\label{rem:bft-stable-round-closure}
If a round $r$ is closed, no more $\BFTPROVE(r)$ can be valid and thus linearized. In other words, once $\BFTAPPEND(r)^\star$ is linearized, no more process can make a proof on round $r$, and the set of valid proofs for round $r$ is fixed. Therefore $\Winners_r$ is fixed.
\end{remark}
% \begin{remark}[BFT Stable round closure]\label{rem:bft-stable-round-closure}
% If a round $r$ is closed, no more $\BFTPROVE(r)$ can be valid and thus linearized. In other words, once $\BFTAPPEND(r)^\star$ is linearized, no more process can make a proof on round $r$, and the set of valid proofs for round $r$ is fixed. Therefore $\Winners_r$ is fixed.
% \end{remark}
\begin{proof}
By definition $r$ closed means that for all process $p_i$, there exist at least $n - f$ distinct processes $j \in \Pi$ such that $\BFTAPPEND_j(r)$ appears in $\Seq^k$. By BFT-PROVE Validity, any subsequent $\BFTPROVE(r)$ is invalid because at least $n - f$ processes already invoked a valid $\BFTAPPEND(r)$ before it. Thus no new valid $\BFTPROVE(r)$ can be linearized after $\BFTAPPEND(r)^\star$. Hence the set of valid proofs for round $r$ is fixed, and so is $\Winners_r$.
\end{proof}
% \begin{proof}
% By definition $r$ closed means that for all process $p_i$, there exist at least $n - f$ distinct processes $j \in \Pi$ such that $\BFTAPPEND_j(r)$ appears in $\Seq^k$. By BFT-PROVE Validity, any subsequent $\BFTPROVE(r)$ is invalid because at least $n - f$ processes already invoked a valid $\BFTAPPEND(r)$ before it. Thus no new valid $\BFTPROVE(r)$ can be linearized after $\BFTAPPEND(r)^\star$. Hence the set of valid proofs for round $r$ is fixed, and so is $\Winners_r$.
% \end{proof}
\begin{lemma}[BFT Across rounds]\label{lem:bft-across-rounds}
For any $r, r'$ such that $r < r'$, if $r'$ is closed, $r$ is also closed.
\end{lemma}
% \begin{lemma}[BFT Across rounds]\label{lem:bft-across-rounds}
% For any $r, r'$ such that $r < r'$, if $r'$ is closed, $r$ is also closed.
% \end{lemma}
\begin{proof}
Let $r \in \mathcal{R}$. By \cref{def:bft-closed-round}, if $r + 1$ is closed, then for all $\DL[k]$, $r + 1$ is closed in $\Seq^k$. By the implementation, a process can only invoke $\BFTAPPEND(r + 1)$ after observing at least $n - f$ valid $\BFTPROVE(r)$, which means that for all $\DL[k]$, $r$ is closed in $\Seq^k$. Hence by \cref{def:bft-closed-round}, $r$ is closed.
% \begin{proof}
% Let $r \in \mathcal{R}$. By \cref{def:bft-closed-round}, if $r + 1$ is closed, then for all $\DL[k]$, $r + 1$ is closed in $\Seq^k$. By the implementation, a process can only invoke $\BFTAPPEND(r + 1)$ after observing at least $n - f$ valid $\BFTPROVE(r)$, which means that for all $\DL[k]$, $r$ is closed in $\Seq^k$. Hence by \cref{def:bft-closed-round}, $r$ is closed.
Because $r$ is monotonically increasing, we can reccursively apply the same argument to conclude that for any $r, r'$ such that $r < r'$, if $r'$ is closed, $r$ is also closed.
\end{proof}
% Because $r$ is monotonically increasing, we can reccursively apply the same argument to conclude that for any $r, r'$ such that $r < r'$, if $r'$ is closed, $r$ is also closed.
% \end{proof}
\begin{lemma}[BFT Progress]\label{lem:bft_progress}
For any correct process $p_i$ such that
\[
\received \setminus (\delivered \cup (\cup_{r' < r} \cup_{j \in W[r'] \prop[r'][j]})) \neq \emptyset
\]
with $r$ the highest closed round in the $\DL$ linearization. Eventually $r+1$ will be closed.
\end{lemma}
% \begin{lemma}[BFT Progress]\label{lem:bft_progress}
% For any correct process $p_i$ such that
% \[
% \received \setminus (\delivered \cup (\cup_{r' < r} \cup_{j \in W[r'] \prop[r'][j]})) \neq \emptyset
% \]
% with $r$ the highest closed round in the $\DL$ linearization. Eventually $r+1$ will be closed.
% \end{lemma}
\begin{lemma}[BFT Winners invariant]\label{lem:bft-winners-invariant}
For any closed round $r$, define
\[
\Winners_r = \{j: \BFTPROVE_j(r) \prec \BFTAPPEND^\star(r)\}
\]
called the unique set of winners of round $r$.
\end{lemma}
% \begin{lemma}[BFT Winners invariant]\label{lem:bft-winners-invariant}
% For any closed round $r$, define
% \[
% \Winners_r = \{j: \BFTPROVE_j(r) \prec \BFTAPPEND^\star(r)\}
% \]
% called the unique set of winners of round $r$.
% \end{lemma}
\begin{lemma}[BFT n-f lower-bounded Winners]
Let $r$ a closed round, $|W[r]| \geq n-f$.
\end{lemma}
% \begin{lemma}[BFT n-f lower-bounded Winners]
% Let $r$ a closed round, $|W[r]| \geq n-f$.
% \end{lemma}
\begin{remark}\label{rem:correct-in-winners}
Because we assume $n \geq 2f+ 1$, if $|W[r]| \geq n-f$ at least 1 correct have to be in $W[r]$ to progress.
\end{remark}
% \begin{remark}\label{rem:correct-in-winners}
% Because we assume $n \geq 2f+ 1$, if $|W[r]| \geq n-f$ at least 1 correct have to be in $W[r]$ to progress.
% \end{remark}
\begin{lemma}[BFT Winners must purpose]\label{lem:bft-winners-purpose}
Let $r$ a closed round, for all process $p_j$ such that $j \in W[r]$, $p_j$ must have executed $\RBcast(j, PROP, \_, r)$ and hence any correct will eventually set $\prop[r][j]$ to a non-$\bot$ value.
\end{lemma}
% \begin{lemma}[BFT Winners must purpose]\label{lem:bft-winners-purpose}
% Let $r$ a closed round, for all process $p_j$ such that $j \in W[r]$, $p_j$ must have executed $\RBcast(j, PROP, \_, r)$ and hence any correct will eventually set $\prop[r][j]$ to a non-$\bot$ value.
% \end{lemma}
\begin{lemma}[BFT Messages Incariant]\label{lem:bft-messages-invariant}
For any closed round $r$ and any correct process $p_i$ such that $\forall j \in \Winners_r$: $\prop^{(i)}[r][j] \neq \bot$ define
\[
\Messages_r = \cup_{j \in \Winners_r} prop^{(i)}[r][j]
\]
as the set of messages proposed by the winners of round $r$
\end{lemma}
% \begin{lemma}[BFT Messages Incariant]\label{lem:bft-messages-invariant}
% For any closed round $r$ and any correct process $p_i$ such that $\forall j \in \Winners_r$: $\prop^{(i)}[r][j] \neq \bot$ define
% \[
% \Messages_r = \cup_{j \in \Winners_r} prop^{(i)}[r][j]
% \]
% as the set of messages proposed by the winners of round $r$
% \end{lemma}
\begin{lemma}[BFT EVentual proposal closure]\label{lem:bft-eventual-proposal-closure}
If a correct process $p_i$ define $M$ at line~\ref{code:Mcompute}, then for every $j \in \Winners_r$, $\prop^{(i)}[r][j] \neq \bot$.
\end{lemma}
% \begin{lemma}[BFT EVentual proposal closure]\label{lem:bft-eventual-proposal-closure}
% If a correct process $p_i$ define $M$ at line~\ref{code:Mcompute}, then for every $j \in \Winners_r$, $\prop^{(i)}[r][j] \neq \bot$.
% \end{lemma}
\begin{lemma}[BFT Unique proposal per sender per round]\label{lem:bft-unique-proposal}
For any round $r$ and any process $p_i$, if $p_i$ invokes two $\RBcast$ call for the same round, such that $\RBcast(i, PROP, S, r) \prec \RBcast(i, PROP, S', r)$. Then for any correct process $p_j$, $\prop^{(j)}[r][i] \in \{\bot, S\}$
\end{lemma}
% \begin{lemma}[BFT Unique proposal per sender per round]\label{lem:bft-unique-proposal}
% For any round $r$ and any process $p_i$, if $p_i$ invokes two $\RBcast$ call for the same round, such that $\RBcast(i, PROP, S, r) \prec \RBcast(i, PROP, S', r)$. Then for any correct process $p_j$, $\prop^{(j)}[r][i] \in \{\bot, S\}$
% \end{lemma}
@@ -391,6 +396,103 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au
% Since $p_i$ is correct, seeing that $m \in \prop[r'][j]$ for some $j \in W_{r'}$ implies that $p_i$ received a $Rdeliver(j, \texttt{PROP}, S, r')$ message from $p_j$ such that $m \in S$. And because $p_j$ is in $W_{r'}$, at least $n - f$ correct processes invoked a valid $Y[j].\BFTPROVE(r')$ before the round $r'$ were closed. By the reliable broadcast properties, the $Rdeliver(j, \texttt{PROP}, S, r')$ message will eventually be delivered to every correct process, hence eventually for any correct process $m \in \prop[r'][j]$ with $j \in W_{r'}$. Hence $m$ will eventually be included in the set $\Messages_{r'}$ defined in \Cref{def:bft-message-invariant} and thus eventually be ADelivered by any correct process.
% \end{proof}
\subsection{Correctness Lemmas}
\begin{definition}[Closed Round]
A round $r \in \mathcal{R}$ is said to be \emph{closed} for a correct process $p_i$ if at the moment $p_i$ computes $\winners[r]$, it satisfies $|\{k : (k, r) \in \BFTREAD()\}| \geq n - t$.
\end{definition}
\begin{lemma}[Round Monotonicity]\label{lem:round-monotonicity}
If a round $r$ is closed, then every round $r_1 < r$ is also closed.
\end{lemma}
\begin{proof}
\textbf{Base:} $r = 0$. Suppose round $1$ is closed, the set $\{r' \in \mathcal{R}: r' < r\}$ is empty, so the claim holds.
\textbf{Inductive step:} Let $r \geq 1$. Assume that the property holds for all rounds $r' < r$: whenever round $r'$ is closed, all rounds $r_2 < r'$ are also closed. We show that if round $r$ is closed, then all rounds $r_1 < r$ are closed.
Suppose round $r$ is closed. This means at least one correct process $p_i$ has reached line \ref{alg:check-validated} and satisfied the condition $|\validated(r)| \geq n - t$. Consequently, $p_i$ has invoked $\BFTAPPEND(\langle j, r \rangle)$ for each $j \in \Pi$ at line \ref{alg:append}. Since these operations are invoked by a correct process, and they depend on valid proofs in the byzantine fault tolerant deny list, at least one of these operations must have succeeded in the DL object.
Moreover, by the algorithm structure, a correct process can only reach the beginning of round $r$ after completing round $r-1$. In particular, process $p_i$ reaches line \ref{alg:main-loop} for round $r$ only after having completed round $r-1$, which requires the process to have observed at least $|\done[r-1]| \geq n - t$ (line \ref{alg:check-done} for round $r-1$). This condition can only be satisfied if round $r-1$ is closed: at least $n - t$ processes must have issued DONE messages, and since $n > 3f$, at least one of these is correct.
Since $n - t > 2f + 1$, among the $n - t$ processes satisfying the condition for round $r-1$, at least one is correct. A correct process that issued a DONE message for round $r-1$ must have previously completed its execution of lines \ref{alg:append} for round $r-1$, which in turn required observing $|\validated(r-1)| \geq n - t$ from line \ref{alg:check-validated}. Thus, round $r-1$ is closed.
Now, considering any round $r_1 < r-1$: by the inductive hypothesis applied to round $r-1$, since round $r-1$ is closed and $r_1 < r-1$, we have that $r_1$ is also closed.
By strong induction, if round $r$ is closed, all rounds $r_1 < r$ are closed.
\end{proof}
\begin{lemma}[Eventual Closure]\label{lem:eventual-closure}
For any correct process $p_i$, if $\unordered \setminus \ordered \neq \emptyset$ and if $r$ is the highest closed round observed by $p_i$, then eventually round $r+1$ will be closed with $|\winners[r+1]| \geq n - t$.
\end{lemma}
\begin{lemma}[Uniqueness of Winners' Proposals]\label{lem:unique-proposal}
For any closed round $r$ and any process $p_j \in \winners[r]$, there exists a unique set $S_j \subseteq \mathcal{M}$ such that every correct process $p_i$ that has received a reliable delivery of a $\texttt{PROP}$ message from $p_j$ for round $r$ receives exactly this set $S_j$.
\end{lemma}
\begin{proof}
Let $r$ be a closed round and $p_j \in \winners[r]$. Since $j \in \winners[r]$, it means that $(j, r) \in \BFTREAD()$, i.e., at least $t+1$ distinct processes have invoked a valid $\BFTPROVE(\langle j, r \rangle)$ before the round $r$ closed.
By the algorithm, a correct process $p_i$ invokes $\BFTPROVE(\langle j, r \rangle)$ only upon receiving a reliable delivery of a $\texttt{PROP}$ message from $p_j$ for round $r$ at line \ref{alg:append}. Let $S_j^{(i)}$ denote the set received by $p_i$.
Since at least $t+1$ distinct processes have performed a valid $\BFTPROVE(\langle j, r \rangle)$, and since $t < n/3$, at least one of these processes is correct. Thus, at least one correct process must have received a reliable broadcast from $p_j$ for round $r$.
Now, by Bracha's Byzantine Reliable Broadcast specification \cite{Bracha1987}, for any message broadcast instance by process $p_j$ in round $r$, all correct processes that deliver this broadcast either receive the identical message or none at all. Formally, for all correct processes $p_i, p_i'$ that received a delivery from $p_j$ for round $r$, we have $S_j^{(i)} = S_j^{(i')}$.
Therefore, there exists a unique set $S_j$ such that every correct process $p_i$ that receives a reliable delivery from $p_j$ for round $r$ receives exactly $S_j$.
\end{proof}
\begin{lemma}[Winners Stability]\label{lem:winners-stability}
For any closed round $r$, the set $\winners[r]$ is stable.
\end{lemma}
\begin{proof}
Let $r$ be a closed round. By definition, a closed round $r$ means that at least one correct process $p_i$ has observed $|\{k : (k, r) \in \BFTREAD()\}| \geq n - t$ and computed $\winners[r]$ at line \ref{alg:check-done}.
When round $r$ becomes closed, this implies that at least $n - t$ distinct processes have invoked $\BFTAPPEND(\langle j, r \rangle)$ for $j \in \Pi$ (by the algorithm structure, since $\done[r]$ contains DONE messages from processes that completed line \ref{alg:append}). Since $n > 3f$, we have $n - t > 2f + 1 > t + 1$.
Consider a fixed $j \in \Pi$. Since at least $n - t > t + 1$ processes have invoked a valid $\BFTAPPEND(\langle j, r \rangle)$, by \cref{lem:bft-prove-validity}, any subsequent invocation of $\BFTPROVE(\langle j, r \rangle)$ will be invalid.
By \cref{lem:bft-prove-anti-flickering}, once a $\BFTPROVE(\langle j, r \rangle)$ operation becomes invalid, all subsequent $\BFTPROVE(\langle j, r \rangle)$ operations are also invalid.
This holds for all $j \in \Pi$. Therefore, after the round $r$ is closed, the set of valid $\BFTPROVE(\langle j, r \rangle)$ operations for each $j$ cannot grow. By \cref{lem:bft-read-anti-flickering}, any subsequent $\BFTREAD()$ invocation will not return any new $(k, r)$ pairs beyond those already returned. Thus, $\winners[r] = \{j : (j, r) \in \BFTREAD()\}$ becomes stable and cannot change.
Since this reasoning applies to all correct processes that compute $\winners[r]$ after round $r$ is closed, all correct processes will compute the same stable set $\winners[r]$.
\end{proof}
\begin{lemma}[Message Content Invariance]\label{lem:message-content-invariance}
For any closed round $r$ and any correct process $p_i$, the set $M$ computed at line \ref{code:Mcompute} by $p_i$ is identical to the set computed by any other correct process $p_j$ for the same round $r$.
\end{lemma}
\begin{proof}
Let $r$ be a closed round and let $p_i, p_{i'}$ be two correct processes. By the algorithm, both processes compute $M$ as:
\[
M^{(i)} = \bigcup_{j \in \winners[r]} \prop^{(i)}[r][j]
\]
and
\[
M^{(i')} = \bigcup_{j \in \winners[r]} \prop^{(i')}[r][j]
\]
at line \ref{code:Mcompute}.
By \cref{lem:winners-stability}, the set $\winners[r]$ is stable once round $r$ is closed. Therefore, both $p_i$ and $p_{i'}$ compute the same set of winners $\winners[r]$.
Now, consider any winner $j \in \winners[r]$. By \cref{lem:unique-proposal}, there exists a unique set $S_j \subseteq \mathcal{M}$ such that every correct process that receives a reliable delivery of a $\texttt{PROP}$ message from $p_j$ for round $r$ receives exactly $S_j$.
By the algorithm, each correct process stores this received set in its local variable: $\prop^{(i)}[r][j] = S_j$ and $\prop^{(i')}[r][j] = S_j$.
Since both processes compute the union over the same set of winners, and each winner's proposal is identical for all correct processes:
\[
M^{(i)} = \bigcup_{j \in \winners[r]} \prop^{(i)}[r][j] = \bigcup_{j \in \winners[r]} S_j = \bigcup_{j \in \winners[r]} \prop^{(i')}[r][j] = M^{(i')}
\]
Therefore, all correct processes compute the same set $M$ for any closed round $r$.
\end{proof}
\begin{lemma}[Total Order]\label{lem:total-order}
For any two correct processes $p_i$ and $p_j$, the sequence $\ordered$ maintained locally by $p_i$ and the sequence maintained by $p_j$ contain the same messages in the same order, provided that both have reached the same set of closed rounds.
\end{lemma}
\begin{theorem}
The algorithm implements a BFT Atomic Reliable Broadcast.
\end{theorem}

BIN
Recherche/BFT-ARBover/main.pdf
View File

Binary file not shown.

93
Recherche/BFT-ARBover/main.tex
View File

@@ -44,54 +44,59 @@
\newtheorem{remark}{Remark}
\newcommand{\RB}{\textsf{RB}\xspace}
\newcommand{\res}{\mathsf{res}}
\newcommand{\ARB}{\textsf{ARB}\xspace}
\newcommand{\DL}{\textsf{DL}}
\newcommand{\APPEND}{\textsf{APPEND}}
\newcommand{\PROVE}{\textsf{PROVE}}
\newcommand{\PROVEtrace}{\textsf{prove}}
\newcommand{\READ}{\textsf{READ}}
\newcommand{\append}{\ensuremath{\mathsf{append}}}
\newcommand{\prove}{\ensuremath{\mathsf{prove}}}
\newcommand{\PROVEtrace}{\ensuremath{\mathsf{prove}}}
\newcommand{\readop}{\ensuremath{\mathsf{read}}}
\newcommand{\BFTAPPEND}{\textsf{BFT\text{-}APPEND}}
\newcommand{\BFTPROVE}{\textsf{BFT\text{-}PROVE}}
\newcommand{\BFTREAD}{\textsf{BFT\text{-}READ}}
% Backward compatibility aliases
\newcommand{\APPEND}{\append}
\newcommand{\PROVE}{\prove}
\newcommand{\READ}{\readop}
\newcommand{\BFTAPPEND}{\textsc{bft-append}}
\newcommand{\BFTPROVE}{\textsc{bft-prove}}
\newcommand{\BFTREAD}{\textsc{bft-read}}
\newcommand{\ABbroadcast}{\textsf{ABroadcast}}
\newcommand{\ABdeliver}{\textsf{ADeliver}}
\newcommand{\RBcast}{\textsf{RBroadcast}}
\newcommand{\RBreceived}{\textsf{RReceived}}
\newcommand{\ordered}{\textsf{order}}
\newcommand{\ABbroadcast}{\textsc{abroadcast}}
\newcommand{\ABdeliver}{\textsc{adeliver}}
\newcommand{\validated}{\ensuremath{\textsc{validated}}}
\newcommand{\rbcast}{\ensuremath{\mathsf{rbcast}}}
\newcommand{\rbreceived}{\ensuremath{\mathsf{rreceived}}}
% \newcommand{\ordered}{\ensuremath{\mathsf{order}}}
% Backward compatibility aliases
\newcommand{\RBcast}{\rbcast}
\newcommand{\rdeliver}{\ensuremath{\mathsf{rdeliver}}}
\newcommand{\send}{\ensuremath{\mathsf{send}}}
\newcommand{\receive}{\ensuremath{\mathsf{receive}}}
% Local variables
\newcommand{\unordered}{\ensuremath{\mathit{unordered}}}
\newcommand{\ordered}{\ensuremath{\mathit{ordered}}}
\newcommand{\delivered}{\ensuremath{\mathit{delivered}}}
\newcommand{\prop}{\ensuremath{\mathit{prop}}}
\newcommand{\winners}{\ensuremath{\mathit{winners}}}
\newcommand{\done}{\ensuremath{\mathit{done}}}
\newcommand{\res}{\ensuremath{\mathit{res}}}
\newcommand{\flag}{\ensuremath{\mathit{flag}}}
%% Used in BFT-DL implementation
\newcommand{\state}{\ensuremath{\mathit{state}}}
\newcommand{\results}{\ensuremath{\mathit{results}}}
% Invariant/concept names (used in proofs)
\newcommand{\Winners}{\mathsf{Winners}}
\newcommand{\Messages}{\mathsf{Messages}}
\newcommand{\ABlisten}{\textsf{AB-listen}}
\newcommand{\CANDIDATE}{\textsf{VOTE}}
\newcommand{\CLOSE}{\textsf{COMMIT}}
\newcommand{\READGE}{\textsf{RESULT}}
\newcommand{\SHARE}{\mathsf{SHARE}}
\newcommand{\COMBINE}{\mathsf{COMBINE}}
\newcommand{\VERIFY}{\mathsf{VERIFY}}
\newcommand{\RETRIEVE}{\mathsf{RETRIEVE}}
\newcommand{\SUBMIT}{\mathsf{SUBMIT}}
\newcommand{\delivered}{\mathsf{delivered}}
\newcommand{\received}{\mathsf{received}}
\newcommand{\prop}{\mathsf{prop}}
\newcommand{\resolved}{\mathsf{resolved}}
\newcommand{\current}{\mathsf{current}}
\newcommand{\received}{\ensuremath{\mathsf{received}}}
\newcommand{\current}{\ensuremath{\mathsf{current}}}
\newcommand{\Seq}{\mathsf{Seq}}
\newcommand{\GE}{\mathsf{GE}}
\newcommand{\BFTDL}{\textsf{BFT\text{-}DL}}
\newcommand{\BFTGE}{\textsf{BFT\text{-}GE}}
\newcommand{\BFTVOTE}{\textsf{BFT\text{-}VOTE}}
\newcommand{\BFTCOMMIT}{\textsf{BFT\text{-}COMMIT}}
\newcommand{\BFTRESULT}{\textsf{BFT\text{-}RESULT}}
\crefname{theorem}{Theorem}{Theorems}
\crefname{lemma}{Lemma}{Lemmas}
@@ -112,7 +117,7 @@ We consider a static set $\Pi$ of $n$ processes with known identities, communica
\paragraph{Synchrony.} The network is asynchronous.
\paragraph{Communication.} Processes can exchange through a Reliable Broadcast ($\RB$) primitive (defined below) which is invoked with the functions $\RBcast(m)$ and $m = \RBreceived()$. There exists a shared object called DenyList ($\DL$) (defined below) that is interfaced with a set $O$ of operations. There exist three types of these operations: $\APPEND(x)$, $\PROVE(x)$ and $\READ()$.
\paragraph{Communication.} Processes can exchange through a Reliable Broadcast ($\RB$) primitive (defined below) which is invoked with the functions $\RBcast(m)$ and $m = \rbreceived()$. There exists a shared object called DenyList ($\DL$) (defined below) that is interfaced with a set $O$ of operations. There exist three types of these operations: $\APPEND(x)$, $\PROVE(x)$ and $\READ()$.
\paragraph{Notation.} For any indice $x$ we defined by $\Pi_x$ a subset of $\Pi$. We consider two subsets $\Pi_M$ and $\Pi_V$ two authorization subsets. Indices $i \in \Pi$ refer to processes, and $p_i$ denotes the process with identifier $i$. Let $\mathcal{M}$ denote the universe of uniquely identifiable messages, with $m \in \mathcal{M}$. Let $\mathcal{R} \subseteq \mathbb{N}$ be the set of round identifiers; we write $r \in \mathcal{R}$ for a round. We use the precedence relation $\prec$ for the \DL{} linearization: $x \prec y$ means that operation $x$ appears strictly before $y$ in the linearized history of \DL. For any finite set $A \subseteq \mathcal{M}$, \ordered$(A)$ returns a deterministic total order over $A$ (e.g., lexicographic order on $(\textit{senderId},\textit{messageId})$ or on message hashes).
For any operation $F \in O$,$F_i(...)$ denotes that the operation $F$ is invoked by process $p_i$.
@@ -225,11 +230,11 @@ Such that :
\begin{algorithm}[H]
\caption{$\READ'() \rightarrow \mathcal{L}(\mathbb{R} \times \PROVEtrace(\mathbb{R}))$}
$j \gets$ the process invoking $\READ'()$\;
$res \gets \emptyset$\;
$\res \gets \emptyset$\;
\ForAll{$i \in \{1, \dots, k\}$}{
$res \gets res \cup DL_i.\READ()$\;
$\res \gets \res \cup DL_i.\READ()$\;
}
\Return{$res$}\;
\Return{$\res$}\;
\end{algorithm}
\begin{algorithm}[H]
@@ -243,11 +248,11 @@ Such that :
\begin{algorithm}[H]
\caption{$\PROVE'(\sigma) \rightarrow \{0, 1\}$}
$j \gets$ the process invoking $\PROVE'(\sigma)$\;
$flag \gets false$\;
$\flag \gets false$\;
\ForAll{$i \in \{1, \dots, k\}$}{
$flag \gets flag$ OR $DL_i.\PROVE(\sigma)$\;
$\flag \gets \flag$ OR $DL_i.\PROVE(\sigma)$\;
}
\Return{$flag$}\;
\Return{$\flag$}\;
\end{algorithm}
\subsection{Threshold Cryptography}