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

ARB over DL + RB et version BFT

Browse Source
This commit is contained in:
Amaury JOLY
2025-12-09 16:17:51 +01:00
parent 3c90fdc774
commit 6fdcdadfd2
13 changed files with 1603 additions and 99 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
.devcontainer/devcontainer.json
View File

@@ -20,6 +20,7 @@
"james-yu.latex-workshop",
"eamodio.gitlens",
"jenselme.grammalecte",
"jebbs.plantuml"
],
"settings": {
"grammalecte.allowedExtension": ".md,.rst,.adoc,.asciidoc,.creole,.t2t,.tex",

8
.devcontainer/install-tools.sh
View File

@@ -12,4 +12,10 @@ apt install python3 unzip wget -y
mkdir /root/.grammalecte
cd /root/.grammalecte
wget https://grammalecte.net/zip/Grammalecte-fr-v2.1.1.zip
unzip Grammalecte-fr-v2.1.1.zip
unzip Grammalecte-fr-v2.1.1.zip
#Installation de plantuml
cd /tmp/
wget https://github.com/plantuml/plantuml/releases/download/v1.2025.10/plantuml-1.2025.10.jar
mkdir /usr/share/plantuml/
mv plantuml-1.2025.10.jar /usr/share/plantuml/plantuml.jar

BIN
Recherche/ALDLoverAB/main.pdf
View File

Binary file not shown.

264
Recherche/ALDLoverAB/main.tex
View File

@@ -40,6 +40,7 @@
\newtheorem{remark}{Remark}
\newcommand{\RB}{\textsf{RB}\xspace}
\newcommand{\res}{\mathsf{res}}
\newcommand{\ARB}{\textsf{ARB}\xspace}
\newcommand{\DL}{\textsf{DL}\xspace}
\newcommand{\APPEND}{\textsf{APPEND}}
@@ -58,6 +59,9 @@
\newcommand{\delivered}{\mathsf{delivered}}
\newcommand{\received}{\mathsf{received}}
\newcommand{\prop}{\mathsf{prop}}
\newcommand{\current}{\mathsf{current}}
\newcommand{\Seq}{\mathsf{Seq}}
\crefname{theorem}{Theorem}{Theorems}
\crefname{lemma}{Lemma}{Lemmas}
@@ -89,8 +93,6 @@ We consider a static set of $n$ processes with known identities, communicating b
\paragraph{Notation.} Let $\Pi$ be the finite set of process identifiers and let $n \triangleq |\Pi|$. Two authorization subsets are $\Pi_M \subseteq \Pi$ (processes allowed to issue \APPEND) and $\Pi_V \subseteq \Pi$ (processes allowed to issue \PROVE). Indices $i,j \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 round $r \in \mathcal{R}$, define $\Winners_r \triangleq \{\, j \in \Pi \mid (j,\PROVEtrace(r)) \prec \APPEND(r) \,\}$, i.e., the set of processes whose $\PROVE(r)$ appears before the first $\APPEND(r)$ in the \DL{} linearization.
We denoted by $\PROVE^{(j)}(r)$ or $\APPEND^{(j)}(r)$ the operation $\PROVE(r)$ or $\APPEND(r)$ invoked by process $j$.
% For any round r ∈ R, define Winnersr ≜ { j ∈ Π | (j, prove(r)) ≺ APPEND(r) }. Pas bien on compare des tuples et des operations
% ------------------------------------------------------------------------------
\section{Primitives}
\subsection{Reliable Broadcast (RB)}
@@ -103,21 +105,28 @@ We denoted by $\PROVE^{(j)}(r)$ or $\APPEND^{(j)}(r)$ the operation $\PROVE(r)$
\end{itemize}
\subsection{DenyList (DL)}
The \DL is a \emph{shared, append-only} object that records attestations about opaque application-level tokens. It exposes the following operations:
\begin{itemize}[leftmargin=*]
\item \APPEND$(x)$
\item \PROVE$(x)$: issue an attestation for token $x$; this operation is \emph{valid} (return true) only if no \APPEND$(x)$ occurs earlier in the \DL linearization. Otherwise, it is invalid (return false).
\item \READ$()$: return a (permutation of the) valid operations observed so far; subsequent reads are monotone (contain supersets of previously observed valid operations).
We assume a synchronous DenyList (\DL) object with the following properties.
The DenyList object type supports three operations: $\APPEND$, $\PROVE$, and $\READ$. These operations appear as if executed in a sequence $\Seq$ such that:
\begin{itemize}
\item \textbf{Termination.} A $\PROVE$, an $\APPEND$, or a $\READ$ operation invoked by a correct process always returns.
\item \textbf{APPEND Validity.} The invocation of $\APPEND(x)$ by a process $p$ is valid if:
\begin{itemize}
\item $p \in \Pi_M \subseteq \Pi$; \textbf{and}
\item $x \in S$, where $S$ is a predefined set.
\end{itemize}
Otherwise, the operation is invalid.
\item \textbf{PROVE Validity.} If the invocation of a $op = \PROVE(x)$ by a correct process $p$ is not valid, then:
\begin{itemize}
\item $p \not\in \Pi_V \subseteq \Pi$; \textbf{or}
\item A valid $\APPEND(x)$ appears before $op$ in $\Seq$.
\end{itemize}
Otherwise, the operation is valid.
\item \textbf{PROVE Anti-Flickering.} If the invocation of a operation $op = \PROVE(x)$ by a correct process $p \in \Pi_V$ is invalid, then any $\PROVE(x)$ operation that appears after $op$ in $\Seq$ is invalid.
\item \textbf{READ Validity.} The invocation of $op = \READ()$ by a process $p \in \pi_V$ returns the list of valid invocations of $\PROVE$ that appears before $op$ in $\Seq$ along with the names of the processes that invoked each operation.
\item \textbf{Anonymity.} Let us assume the process $p$ invokes a $\PROVE(v)$ operation. If the process $p'$ invokes a $\READ()$ operation, then $p'$ cannot learn the value $v$ unless $p$ leaks additional information.
\end{itemize}
\paragraph{Validity.} \APPEND$(x)$ is valid iff the issuer is authorized (in $\Pi_M$) and $x$ belongs to the application-defined domain $S$. \PROVE$(x)$ is valid iff the issuer is authorized (in $\Pi_V$) and there is no earlier \APPEND$(x)$ in the \DL linearization.
\paragraph{Progress.} If a correct process invokes \APPEND$(x)$, then eventually all correct processes will be unable to issue a valid \PROVE$(x)$, and \READ{} at all correct processes will (eventually) reflect that \APPEND$(x)$ has been recorded.
\paragraph{Termination.} Every operation invoked by a correct process eventually returns.
\paragraph{Interface and Semantics.} The \DL provides a single global linearization of operations consistent with each process's program order. \READ{} is prefix-monotone; concurrent updates become visible to all correct processes within bounded time (by synchrony). Duplicate requests may be idempotently coalesced by the implementation.
% ------------------------------------------------------------------------------
\section{Target Abstraction: Atomic Reliable Broadcast (ARB)}
Processes export \ABbroadcast$(m)$ and \ABdeliver$(m)$. \ARB requires total order:
@@ -144,6 +153,7 @@ Each process $p_i$ maintains:
\State $\received \gets \emptyset$ \Comment{Messages received via \RB but not yet delivered}
\State $\delivered \gets \emptyset$ \Comment{Messages already delivered}
\State $\prop[r][j] \gets \bot,\ \forall r,j$ \Comment{Proposal from process $j$ for round $r$}
\State $\current \gets 0$
\end{algorithmic}
\paragraph{DenyList.} The \DL is initialized empty. We assume $\Pi_M = \Pi_V = \Pi$ (all processes can invoke \APPEND and \PROVE).
@@ -164,7 +174,6 @@ Each process $p_i$ maintains:
% \paragraph{} An \ABbroadcast$(m)$ chooses the next open round from the \DL view, proposes all pending messages together with the new $m$, disseminates this proposal via \RB, then executes $\PROVE(r)$ followed by $\APPEND(r)$ to freeze the winners of the round. The loop polls \DL until (i) some winner’s proposal includes $m$ in a \emph{closed} round and (ii) all winners' proposals for closed rounds are known locally, ensuring eventual inclusion and delivery.
% Partie avec le max-1 pas ouf; essayer de faire incr la boucle autrement
\renewcommand{\algletter}{B}
\begin{algorithm}[H]
\caption{\ABbroadcast$(m)$ (at process $p_i$)}\label{alg:ab-bcast}
@@ -187,48 +196,34 @@ Each process $p_i$ maintains:
\end{algorithmic}
\end{algorithm}
% \paragraph{} TODO
\renewcommand{\algletter}{C}
\begin{algorithm}[H]
\caption{\ABdeliver() at process $p_i$}\label{alg:delivery}
\begin{algorithmic}[1]
%local variables
\State $next \gets 0$ \Comment{Next round to deliver}
\State $to\_deliver \gets \emptyset$ \Comment{Queue of messages ready to be delivered}
\vspace{1em}
\Function{ABdeliver}{}
% \State \textbf{on} \ABdeliver() \textbf{do} \Comment{Called when the process wants to receive the next message}
\If{$to\_deliver = \emptyset$} \Comment{If no message is ready to deliver, try to fetch the next round}
\State $P \leftarrow \READ()$ \Comment{Fetch latest \DL state to learn recent $\PROVE$ operations}
\If{$\forall j : (j, \PROVEtrace(next)) \not\in P$} \Comment{Check if some process proved round $next$}
\State \Return $\bot$ \Comment{Round $next$ is still open}
\EndIf
\State $\APPEND(next)$; $P \leftarrow \READ()$ \Comment{Close round $next$ if not already closed}
\State $W_{next} \leftarrow \{ j : (j, \PROVEtrace(next)) \in P \}$ \Comment{Compute winners of round $next$}
\If{$\exists j \in W_{next},\ \prop[next][j] = \bot$} \Comment{Check if we have all winners' proposals}
\State \Return $\bot$ \Comment{Some winner's proposal for round $next$ is still missing}
\EndIf
\State $M_{next} \leftarrow \bigcup_{j \in W_{next}} \prop[next][j]$ \Comment{Compute the agreed proposal for round $next$}
\For{\textbf{each}\ $m \in \ordered(M_{next})$} \Comment{Enqueue messages in deterministic order}
\If{$m \notin \delivered$}
\State $to\_deliver.push(m)$ \Comment{Append $m$ to the delivery queue}
\EndIf
\EndFor
\State $next \leftarrow next + 1$ \Comment{Advance to the next round}
\State $r \gets \current$
\State $P \gets \READ()$
\If{$\forall j : (j, \PROVEtrace(r)) \not\in P$}
\State \Return $\bot$
\EndIf
\State $m \leftarrow \text{to\_deliver.pop()}$
% \State $to\_deliver \leftarrow to\_deliver \setminus \{m\}$
\State $\APPEND(r)$; $P \gets \READ()$
\State $W_r \gets \{ j : (j, \PROVEtrace(r)) \in P \}$
\If{$\exists j \in W_r,\ \prop[r][j] = \bot$}
\State \Return $\bot$
\EndIf
\State $M_r \gets \bigcup_{j \in W_r} \prop[r][j]$
\State $m \gets \ordered(M_r \setminus \delivered)[0]$ \Comment{Set $m$ as the smaller message not already delivered}
\State $\delivered \leftarrow \delivered \cup \{m\}$
\If{$M_r \setminus \delivered = \emptyset$} \Comment{Check if all messages from round $r$ have been delivered}
\State $\current \leftarrow \current + 1$
\EndIf
\State \textbf{return} $m$
\EndFunction
\end{algorithmic}
\end{algorithm}
% ------------------------------------------------------------------------------
\section{Correctness}
%attention au usage de "unique"
%definition de APPEND* ssi r closed
\begin{lemma}[Stable round closure]\label{lem:closure-stable}
If a round $r$ is closed, then there exists a linearization point $t_0$ of $\APPEND(r)$ in the \DL, and from that point on, no $\PROVE(r)$ can be valid.
@@ -279,10 +274,10 @@ If there exists a $r$ such that $r$ is closed, $\forall r'$ such that $r' < r$,
If round $k$ wasn't closed when $p_1$ execute $\PROVE^{(1)}(k)$ at B6, then the condition at B8 should be true which implies that $p_1$ sould leave the loop at round $k$, contradicting the assumption that $p_1$ is now executing $\PROVE^{(1)}(r+1)$. In this case $k$ is closed.
\end{itemize}
\item \textbf{Case (C9) :}
Some process invokes $\APPEND(k+1)$ at C9.
Line C9 is guarded by the presence of $\PROVE(\textit{next})$ in $P$ with $\textit{next}=k+1$ (C6).
Moreover, the local pointer $\textit{next}$ grow by increment of 1 and only advances after finishing the current round (C20), so if a process can reach $\textit{next}=k+1$ it implies that he has completed round $k$, which includes closing $k$ at C9 when $\PROVE(k)$ is observed.
\item \textbf{Case (C8) :}
Some process invokes $\APPEND(k+1)$ at C8.
Line C8 is guarded by the presence of $\PROVE(\textit{next})$ in $P$ with $\textit{next}=k+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}=k+1$ it implies that he has completed round $k$, which includes closing $k$ at C8 when $\PROVE(k)$ is observed.
Hence $\APPEND^\star(k+1)$ implies a prior $\APPEND(k)$ in $H$, so $k$ is closed.
\end{itemize}
@@ -312,7 +307,7 @@ If there exists a $r$ such that $r$ is closed, $\forall r'$ such that $r' < r$,
\end{proof}
\begin{lemma}[Well-defined winners]\label{lem:winners}
For any correct process and round $r$, if the process computes $W_r$ at line C10, then :
For any correct process and round $r$, if the process computes $W_r$ at line C9, then :
\begin{itemize}
\item $\Winners_r$ is defined;
\item the computed $W_r$ is exactly $\Winners_r$.
@@ -320,9 +315,9 @@ If there exists a $r$ such that $r$ is closed, $\forall r'$ such that $r' < r$,
\end{lemma}
\begin{proof}
Let take a correct process $p_i$ that reach line C10 to compute $W_r$. \\
By program order, $p_i$ must have executed $\APPEND^{(i)}(r)$ at C9 before, which implies by \Cref{def:closed-round} that round $r$ is closed. 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 $(\_,\PROVEtrace(r))$ in their \DL view. Hence, when $p_i$ executes the $\READ()$ at C9 after the $\APPEND^{(i)}(r)$, it observes a set $P$ that includes all valid tuples $(\_,\PROVEtrace(r))$ such that
Let take a correct process $p_i$ that reach line C9 to compute $W_r$. \\
By program order, $p_i$ must have executed $\APPEND^{(i)}(r)$ at C8 before, which implies by \Cref{def:closed-round} that round $r$ is closed. 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 $(\_,\PROVEtrace(r))$ in their \DL view. Hence, when $p_i$ executes the $\READ()$ at C8 after the $\APPEND^{(i)}(r)$, it observes a set $P$ that includes all valid tuples $(\_,\PROVEtrace(r))$ such that
\[
W_r = \{ j : (j,\PROVEtrace(r)) \in P \} = \{j : \PROVE^{(j)}(r) \prec \APPEND^\star(r) \} = \Winners_r
\]
@@ -339,8 +334,8 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
\item \textbf{Case (B6) :}
There exists a process $p^\star$ who's the issuer of the earliest $\APPEND^{(\star)}(r)$ in the DL linearization $H$. By program order, $p^\star$ must have previously invoked $\PROVE^{(\star)}(r)$ before invoking $\APPEND^{(\star)}(r)$ at B6. 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 (C9) :}
There exist a process $p^\star$ invokes $\APPEND^{(\star)}(r)$ at C9. Line C9 is guarded by the condition at C6, which ensures that $p$ observed some $(\_,\PROVEtrace(r))$ in $P$. In this case, there is at least one $\PROVE(r)$ valid in $H$ issued by some process before $\APPEND^{(\star)}(r)$.
\item \textbf{Case (C8) :}
There exist a process $p^\star$ invokes $\APPEND^{(\star)}(r)$ at C8. Line C8 is guarded by the condition at C5, which ensures that $p$ observed some $(\_,\PROVEtrace(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)$.
@@ -382,13 +377,13 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
\end{proof}
\begin{lemma}[Eventual proposal closure]\label{lem:eventual-closure}
If a correct process $p_i$ define $M_r$ at line C14, then for every $j \in \Winners_r$, $\prop^{(i)}[r][j] \neq \bot$.
If a correct process $p_i$ define $M_r$ at line C13, 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 C14. By \Cref{lem:winners}, $p_i$ computes the unique winner set $\Winners_r$.
Let take a correct process $p_i$ that computes $M_r$ at line C13. By \Cref{lem:winners}, $p_i$ computes the unique winner set $\Winners_r$.
By \Cref{lem:nonempty}, $\Winners_r \neq \emptyset$. The instruction at line C14 where $p_i$ computes $M_r$ is guarded by the condition at C11, which ensures that $p_i$ has received all \RB messages from every winner $j \in \Winners_r$. Hence, when $p_i$ computes $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 C13 where $p_i$ computes $M_r$ is guarded by the condition at C10, which ensures that $p_i$ has received all \RB messages from every winner $j \in \Winners_r$. Hence, when $p_i$ computes $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$.
\end{proof}
\begin{lemma}[Unique proposal per sender per round]\label{lem:unique-proposal}
@@ -400,14 +395,14 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
\end{proof}
\begin{lemma}[Proposal convergence]\label{lem:convergence}
For any round $r$, for any correct processes $p_i$ that define $M_r$ at line C14, we have
For any round $r$, for any correct processes $p_i$ that define $M_r$ at line C13, we have
\[
M_r^{(i)} = \Messages_r
\]
\end{lemma}
\begin{proof}[Proof]
Let take a correct process $p_i$ that define $M_r$ at line C14. That implies that $p_i$ has defined $W_r$ at line C10. It implies that, by \Cref{lem:winners}, $r$ is closed and $W_r = \Winners_r$. \\
Let take a correct process $p_i$ that define $M_r$ at line C13. That implies that $p_i$ has defined $W_r$ at line C9. 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
\[
M_r^{(i)} = \bigcup_{j\in\Winners_r} \prop^{(i)}[r][j] = \bigcup_{j\in\Winners_r} S^{(j)} = \Messages_r.
@@ -437,20 +432,18 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
\end{proof}
\begin{lemma}[Broadcast Termination]\label{lem:bcast-termination}
If a correct process $p$ invokes $\ABbroadcast(m)$, then $p$ eventually quit the function and returns.
If a correct process invokes $\ABbroadcast(m)$, then he eventually exit the function and returns.
\end{lemma}
\begin{proof}[Proof]
Let a correct process $p_i$ that invokes $\ABbroadcast(m)$. The lemma is true if $(i, \PROVEtrace(r)) \in P$; or there exists $j: (j, \PROVEtrace(r')) \in P \wedge m \in \prop[r'][j]$ (like guarded at B8).
Let a correct process $p_i$ that invokes $\ABbroadcast(m)$. The lemma is true if $\exists r_1$ such that $r_1 \geq r_{max}$ and if $(i, \PROVEtrace(r_1)) \in P$; or if $\exists r_2$ such that $r_2 \geq r_{max}$ and if $\exists j: (j, \PROVEtrace(r_2)) \in P \wedge m \in \prop[r_2][j]$ (like guarded at B8).
\begin{itemize}
\item \textbf{Case 1:} there exists a round $r'$ such that $p_i$ invokes a valid $\PROVE(r')$. Hence by \DL \emph{Progress} and \emph{Semantics} the following $\READ()$ at line B7 will defined a P such as $(i, \PROVEtrace(r')) \in P$. Hence $p_i$ exits the loop at B8.
\item \textbf{Case 2:} there exists no round $r'$ such that $p_i$ invokes a valid $\PROVE(r')$. In this case $p_i$ invokes infinitely many $\RBcast(S, r', i)$ at B6 with $m \in S$ (line B4).\\
The assumption that no $\PROVE(r')$ invoked by $p$ is valid implies by \DL \emph{Validity} that for every round $r'$, 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 a correct 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$ execute \Cref{alg:rb-handler} and do $\received \leftarrow \received \cup \{S\}$ with $m \in S$ (line A2).
For the first invocation of $\ABbroadcast(\_)$ by $p_k$ after the execution of \Cref{alg:rb-handler}, $p_k$ must include $m$ in his proposal $S$ at line B4 (because $m$ is pending in $j$'s $\received \setminus \delivered$ set). There exists a minimum round $r_1$ such that $p_k \in \Winners_{r_1}$ after $t_0$. By \Cref{lem:winner-propose-nonbot}, eventually $\prop^{(i)}[r_1][k] \neq \bot$. By \Cref{lem:unique-proposal}, $\prop^{(i)}[r_1][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_1][k]$ and $k \in \Winners_{r_1}$.
\end{itemize}
The first case explicit the case where $p_i$ is a winner and also covers the condition $(i, \PROVEtrace(r')) \in P$. And in the second case, 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)$.
Let admit 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 B6 with $m \in S$ (line B4).\\
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 a correct 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$ execute \Cref{alg:rb-handler} and do $\received \leftarrow \received \cup \{S\}$ with $m \in S$ (line A2).
For the first invocation of $\ABbroadcast(\_)$ by $p_k$ after the execution of \Cref{alg:rb-handler}, $p_k$ must include $m$ in his proposal $S$ at line B4 (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:winner-propose-nonbot}, 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 cover the condition $(i, \PROVEtrace(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)$.
\end{proof}
\begin{lemma}[Validity]\label{lem:validity}
@@ -463,43 +456,21 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
\RBcast(S, r, j)\quad\text{with}\quad m\in S.
\]
By \Cref{lem:eventual-closure}, when $p_q$ computes $M_r$ at line C14, $\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_r$ at line C13, $\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
\[
M_r = \bigcup_{k\in\Winners_r} \prop[r][k],
\]
we have $m \in \prop[r][j] = S$, so $m \in M_r$. By line C16–C18, $m$ is enqueued into $to\_deliver$ unless it has already been delivered. Therefore, $p_q$ will eventually invokes $\ABdeliver()$, which will returns $m$.
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 any correct process that defines it includes $m$. At each invocation of $\ABdeliver()$ which deliver $m'$, $m'$ is add to $\delivered$ until $M_r \subseteq \delivered$. Once this append we're assured that there exist an invocation of $\ABdeliver()$ which return $m$. Hence $m$ is well delivered.
\end{proof}
\begin{lemma}[Across \ABdeliver]\label{lem:across-abdeliver}
A $\ABdeliver()$ invocation return $m$, a non-$\bot$ value, implie that there exist an invocation of $\ABdeliver()$ which is the earliest of the round $r$ where $m$ is proposed by a winner and which define $M_r$.
\end{lemma}
\begin{proof}
Let take any $\ABdeliver()$ invocation which return a non-$\bot$ value, $m$ which was proposed in round $r$. To return a non-$\bot$ value we can distinguish two cases:
\begin{itemize}
\item This actual invocation of $\ABdeliver$ have the queue $to\_deliver \neq \emptyset$ which implies that there exist an earliest invocation of $\ABdeliver$ which reach the line C17 to fill this queue for round $next = r$. We can call this invocation $\ABdeliver^{(\star r)}$. $\ABdeliver^{(\star r)}$ have to fill $to\_deliver$ at line C17, hence by program order define $M_r$ at C14.
\item This actual invocation of $\ABdeliver$ have the queue $to\_deliver = \emptyset$. To return a non-$\bot$ this execution have to pass the two conditions at lines C6 and C11 to compute $m_r$. Hence $\ABdeliver()$ is the $\ABdeliver^{(\star r)}()$ as described in the first case.
\end{itemize}
\end{proof}
\begin{definition}[First \ABdeliver]\label{def:first-abdeliver}
For any process which invoke an infinite times $\ABdeliver()$. There exist for any round $r$ an unique earliest invocation which defined $M_r$ and return a non-$\bot$ value. We denote by $\ABdeliver^{(\star r)}()$ this invocation.
\end{definition}
\begin{lemma}[No duplication]\label{lem:no-duplication}
No correct process delivers the same message more than once.
\end{lemma}
\begin{proof}
Let consider two invokations of $\ABdeliver()$ made by the same correct process which returns respectively $m_1$ and $m_2$. Let call these two invokations respectively $\ABdeliver^{(A)}()$ and $\ABdeliver^{(B)}()$.
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)}()$.
By \Cref{def:first-abdeliver} we denote $\ABdeliver^{(\star A)}()$ and $\ABdeliver^{(\star B)}()$ the two earliest invocations of each $\ABdeliver()$ respectively in theirs rounds with $A$ the round where $m_1$ is delivered and $B$ the round where $m_2$ is delivered.
Let consider the following cases :
\begin{itemize}
\item \textbf{$A < B$ :} Let consider $m_1 = m_2 = m$. In the execution of $\ABdeliver^{(\star A)}$ the process iterate on line C17 and push $m$ in $to\_deliver$ since $m$ is not in $\delivered$. When the process invoke later $\ABdeliver^{(\star B)}$ he empties the queue. The only way to empties the queue is at line C22 which implie by program order to add $m$ to the $\delivered$ set. Hence when $\ABdeliver^{(\star B)}$ iterate on line C17 he will never be able to push $m$ in the queue because the condition $m \not\in \delivered$ at line C16 is never satisfied. Hence in this case $\ABdeliver^{(B)}()$ can't happen if $m_1 = m_2$.
\item \text{$A = B$ :} Let consider $m_1 = m_2 = m$. $\ABdeliver^{(\star A)}$ and $\ABdeliver^{(\star B)}$ reference the same invocation of $\ABdeliver()$. In this unique execution, when the process define $M_r$ he's making a union operation on all the sets which can contains a multiple times the same message $m$. This operation must result in a unique set which contain a unique time $m$. Hence when the iteration on C17 is done, $m$ is pushed only once, and can be delivered only once too. So $\ABdeliver^{(B)}()$ can't happen if $m_1 = m_2$.
\end{itemize}
When $\ABdeliver^{(A)}()$ occur, by program order and because it reach line C19 to return $m$, the process must have add $m$ to $\delivered$. Hence when $\ABdeliver^{(B)}()$ reach line C14 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 deliver $m$ can't occur.
\end{proof}
\begin{lemma}[Total order]\label{lem:total-order}
@@ -517,9 +488,9 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
Let consider three cases :
\begin{itemize}
\item \textbf{Case 1:} $r_1 < r_2$. By program order, any correct process must have waited to empty the queue $to\_deliver$ (which contains $m_1$) to exit at round $r_1$ before invoking $\ABdeliver()$ that returns $m_2$. 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_{r_1}$ (which contains $m_1$) to increment $\current$ and eventually set $\current = r_2$ to compute $M_{r_2}$ and then invoke the $\ABdeliver()$ that returns $m_2$. 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 C14 computes the same set of messages $\Messages_{r_1}$. By line C16–C18, messages are enqueued into $to\_deliver$ 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_{r_1}$ at line C13 computes the same set of messages $\Messages_{r_1}$. By line C14 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.
@@ -547,9 +518,106 @@ If some process invokes $\APPEND(r)$, then at least a process must have previous
Under the assumed \DL synchrony and \RB reliability, the algorithm implements FIFO 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.
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$.
This gives the usual Validity property of \ARB.
Concerning Integrity and No-duplicates, the construction only ever delivers messages that have been obtained from the underlying \RB primitive.
By the Integrity property of \RB, every such message was previously \RBcast by some process, so no spurious messages are delivered.
In addition, \Cref{lem:no-duplication} states that no correct process delivers the same message more than once.
Together, these arguments yield the Integrity and No-duplicates properties required by \ARB.
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.
\end{proof}
\section{Reciprocity}
% ------------------------------------------------------------------------------
So far, we assumed the existence of a synchronous DenyList (\DL) object and
showed how to upgrade a Reliable Broadcast (\RB) primitive into FIFO Atomic
Reliable Broadcast (\ARB). We now briefly argue that, conversely, an \ARB{}
primitive is strong enough to implement a synchronous \DL object (ignoring the
anonymity property).
\paragraph{DenyList as a deterministic state machine.}
Without anonymity, the \DL specification defines a
deterministic abstract object: given a sequence $\Seq$ of operations
$\APPEND(x)$, $\PROVE(x)$, and $\READ()$, the resulting sequence of return
values and the evolution of the abstract state (set of appended elements,
history of operations) are uniquely determined.
\paragraph{State machine replication over \ARB.}
Assume a system that exports a FIFO-\ARB primitive with the guarantees that if a correct process invokes $\ABbroadcast(m)$, then every correct process eventually $\ABdeliver(m)$ and the invocation eventually returns.
Following the classical \emph{state machine replication} approach
such as described in Schneider~\cite{Schneider90}, we can implement a fault-tolerant service by ensuring the following properties:
\begin{quote}
\textbf{Agreement.} Every nonfaulty state machine replica receives every request. \\
\textbf{Order.} Every nonfaulty state machine replica processes the requests it receives in
the same relative order.
\end{quote}
Which are cover by our FIFO-\ARB specification.
\paragraph{Correctness.}
\begin{theorem}[From \ARB to synchronous \DL]\label{thm:arb-to-dl}
In an asynchronous message-passing system with crash failures, assume a
FIFO Atomic Reliable Broadcast primitive with Integrity, No-duplicates,
Validity, and the liveness of $\ABbroadcast$. Then, ignoring anonymity, there
exists an implementation of a synchronous DenyList object that satisfies the
Termination, Validity, and Anti-flickering properties.
\end{theorem}
\begin{proof}
Because the \DL object is deterministic, all correct processes see the same
sequence of operations and compute the same sequence of states and return
values. We obtain:
\begin{itemize}[leftmargin=*]
\item \textbf{Termination.} The liveness of \ARB ensures that each
$\ABbroadcast$ invocation by a correct process eventually returns, and
the corresponding operation is eventually delivered and applied at all
correct processes. Thus every $\APPEND$, $\PROVE$, and $\READ$ operation invoked by a correct process
eventually returns.
\item \textbf{APPEND/PROVE/READ Validity.} The local code that forms
\ABbroadcast requests can achieve the same preconditions as in the
abstract \DL specification (e.g., $p\in\Pi_M$, $x\in S$ for
$\APPEND(x)$). Once an operation is delivered, its effect and return
value are exactly those of the sequential \DL specification applied in
the common order.
\item \textbf{PROVE Anti-Flickering.} In the sequential \DL specification,
once an element $x$ has been appended, all subsequent $\PROVE(x)$ are
invalid forever. Since all replicas apply operations in the same order,
this property holds in every execution of the replicated implementation:
after the first linearization point of $\APPEND(x)$, no later
$\PROVE(x)$ can return ``valid'' at any correct process.
\end{itemize}
Formally, we can describe the \DL object with the state machine approach for
crash-fault, asynchronous message-passing systems with a total order broadcast
layer~\cite{Schneider90}.
\end{proof}
\bibliographystyle{plain}
\begin{thebibliography}{9}
% (left intentionally blank)
\bibitem{Schneider90}
Fred B.~Schneider.
\newblock Implementing fault-tolerant services using the state machine
approach: a tutorial.
\newblock {\em ACM Computing Surveys}, 22(4):299--319, 1990.
\end{thebibliography}
\end{document}

40
Recherche/BFT-ARBover/.latexmkrc Normal file
View File

@@ -0,0 +1,40 @@
$pdf_mode = 1; # latexmk -pdf par défaut
$pdflatex = 'pdflatex -interaction=nonstopmode -synctex=1 %O %S';
# --- Config PlantUML ----------------------------------------------------
# Si plantuml est dans le PATH :
# $plantuml = 'plantuml';
# Si tu utilises un JAR :
$plantuml = 'java -jar -Djava.awt.headless=true /usr/share/plantuml/plantuml.jar';
# Options PlantUML : sortie LaTeX/TikZ
$plantuml_opts = '-tlatex:nopreamble';
# --- Dépendance personnalisée .puml -> .tex -----------------------------
# Quand latexmk a besoin de "truc.tex" et que "truc.puml" existe,
# il appelle la fonction puml2tex pour le générer.
add_cus_dep( 'puml', 'tex', 0, 'puml2tex' );
sub puml2tex {
my ($base_name) = @_; # base du fichier cible, sans extension
# Exemple : $base_name = 'diagrams/login'
my $puml = "$base_name.puml";
my $tex = "$base_name.tex";
# Message dans le log latexmk
print "PlantUML: génération de $tex à partir de $puml\n";
# Commande PlantUML
my $cmd = "$plantuml $plantuml_opts $puml ";
my $ret = system($cmd);
# 0 = succès, 1 = erreur pour latexmk
return $ret ? 1 : 0;
}
# --- Confort ------------------------------------------------------------
# Compilation continue (latexmk -pvc)
$preview_continuous = 1;

54
Recherche/BFT-ARBover/diagrams/BFT_behaviour.puml Normal file
View File

@@ -0,0 +1,54 @@
@startuml
!pragma teoz true
database DL
actor P1
actor P2
P1 -> DL : <latex>READ()</latex>
DL --> P1 : <latex>P</latex>
P1 -> P1 : <latex>r_{max} = max\{r : (\_, prove(r)) \in P\}</latex>
loop <latex>\textbf{foreach } r \in \{r_{max} + 1, \dots\}</latex>
' P1 ->(05) P2 : <latex>RBcast(prop, S, r, 1)</latex>
P1 -> DL : <latex>PROVE(r)</latex>
P1 -> DL : <latex>APPEND(r)</latex>
P1 -> DL : <latex>READ()</latex>
DL --> P1 : <latex>P</latex>
alt <latex>(1, \text{prove(}r\text{)}) \in P</latex>
note over P1 : break
end
end
P2 -> P2 : <latex>ABdeliver()</latex>
P2 -> DL : <latex>READ()</latex>
DL --> P2 : <latex>P</latex>
note over P2
line(C4)
process P2 check locally if
<latex>\forall j : (j, prove(r)) \not\in P</latex>
which is false since P1 correctly
PROVE(r) and APPEND(r)
<latex>\text{P1 is next include in } W_r</latex>
end note
P2 -> DL : <latex>APPEND(r)</latex>
P2 -> DL : <latex>READ()</latex>
DL --> P2 : <latex>P</latex>
note over P2
line(C9)
process P2 check locally if
<latex>\forall j \in W_r : prop[r][j] = \bot</latex>
which can't be false since P1 didn't
execute <latex>RBcast(prop, S, r, 1)</latex>
P2 will never progress and
deliver any futur messages
end note
hide footbox
@enduml

113
Recherche/BFT-ARBover/diagrams/BFT_behaviour.tex Normal file
View File

@@ -0,0 +1,113 @@
% generated by Plantuml 1.2025.10
\definecolor{plantucolor0000}{RGB}{255,255,255}
\definecolor{plantucolor0001}{RGB}{24,24,24}
\definecolor{plantucolor0002}{RGB}{0,0,0}
\definecolor{plantucolor0003}{RGB}{226,226,240}
\definecolor{plantucolor0004}{RGB}{238,238,238}
\definecolor{plantucolor0005}{RGB}{254,255,221}
\begin{tikzpicture}[yscale=-1
,pstyle0/.style={color=plantucolor0000,line width=0.0pt}
,pstyle1/.style={color=plantucolor0001,line width=0.5pt,dash pattern=on 5.0pt off 5.0pt}
,pstyle2/.style={color=plantucolor0001,fill=plantucolor0003,line width=0.5pt}
,pstyle3/.style={color=plantucolor0001,line width=0.5pt}
,pstyle4/.style={color=plantucolor0001,fill=plantucolor0001,line width=1.0pt}
,pstyle5/.style={color=plantucolor0001,line width=1.0pt}
,pstyle6/.style={color=plantucolor0001,line width=1.0pt,dash pattern=on 2.0pt off 2.0pt}
,pstyle7/.style={color=black,fill=plantucolor0004,line width=1.5pt}
,pstyle8/.style={color=black,line width=1.5pt}
,pstyle9/.style={color=plantucolor0001,fill=plantucolor0005,line width=0.5pt}
]
\draw[pstyle0] (20.5pt,75pt) rectangle (28.5pt,722.6982pt);
\draw[pstyle1] (24pt,75pt) -- (24pt,722.6982pt);
\draw[pstyle0] (105.8255pt,75pt) rectangle (113.8255pt,722.6982pt);
\draw[pstyle1] (109.3255pt,75pt) -- (109.3255pt,722.6982pt);
\draw[pstyle0] (273.8933pt,75pt) rectangle (281.8933pt,722.6982pt);
\draw[pstyle1] (277.3933pt,75pt) -- (277.3933pt,722.6982pt);
\node at (14.055pt,65pt)[below right,color=black,inner sep=0]{DL};
\draw[pstyle2] (6pt,29pt) ..controls (6pt,19pt) and (24pt,19pt) .. (24pt,19pt) ..controls (24pt,19pt) and (42pt,19pt) .. (42pt,29pt) -- (42pt,55pt) ..controls (42pt,65pt) and (24pt,65pt) .. (24pt,65pt) ..controls (24pt,65pt) and (6pt,65pt) .. (6pt,55pt) -- (6pt,29pt);
\draw[pstyle3] (6pt,29pt) ..controls (6pt,39pt) and (24pt,39pt) .. (24pt,39pt) ..controls (24pt,39pt) and (42pt,39pt) .. (42pt,29pt);
\node at (100.4205pt,65pt)[below right,color=black,inner sep=0]{P1};
\draw[pstyle2] (109.3255pt,13.5pt) ellipse (8pt and 8pt);
\draw[pstyle3] (109.3255pt,21.5pt) -- (109.3255pt,48.5pt)(96.3255pt,29.5pt) -- (122.3255pt,29.5pt)(109.3255pt,48.5pt) -- (96.3255pt,63.5pt)(109.3255pt,48.5pt) -- (122.3255pt,63.5pt);
\node at (268.4883pt,65pt)[below right,color=black,inner sep=0]{P2};
\draw[pstyle2] (277.3933pt,13.5pt) ellipse (8pt and 8pt);
\draw[pstyle3] (277.3933pt,21.5pt) -- (277.3933pt,48.5pt)(264.3933pt,29.5pt) -- (290.3933pt,29.5pt)(277.3933pt,48.5pt) -- (264.3933pt,63.5pt)(277.3933pt,48.5pt) -- (290.3933pt,63.5pt);
\draw[pstyle4] (35pt,95pt) -- (25pt,99pt) -- (35pt,103pt) -- (31pt,99pt) -- cycle;
\draw[pstyle5] (29pt,99pt) -- (108.3255pt,99pt);
\node at (41pt,87pt)[below right,inner sep=0]{$READ()$};
\draw[pstyle4] (97.3255pt,115.8333pt) -- (107.3255pt,119.8333pt) -- (97.3255pt,123.8333pt) -- (101.3255pt,119.8333pt) -- cycle;
\draw[pstyle6] (24pt,119.8333pt) -- (103.3255pt,119.8333pt);
\node at (31pt,111pt)[below right,inner sep=0]{$P$};
\draw[pstyle5] (109.3255pt,143.8333pt) -- (151.3255pt,143.8333pt);
\draw[pstyle5] (151.3255pt,143.8333pt) -- (151.3255pt,156.8333pt);
\draw[pstyle5] (110.3255pt,156.8333pt) -- (151.3255pt,156.8333pt);
\draw[pstyle4] (120.3255pt,152.8333pt) -- (110.3255pt,156.8333pt) -- (120.3255pt,160.8333pt) -- (116.3255pt,156.8333pt) -- cycle;
\node at (116.3255pt,131.8333pt)[below right,inner sep=0]{$r_{max} = max\{r : (\_, prove(r)) \in P\}$};
\draw[pstyle7] (8pt,168.8333pt) -- (74.4pt,168.8333pt) -- (74.4pt,170.8333pt) -- (64.4pt,180.8333pt) -- (8pt,180.8333pt) -- (8pt,168.8333pt);
\draw[pstyle8] (8pt,168.8333pt) rectangle (259.8182pt,353.6666pt);
\node at (23pt,169.8333pt)[below right,color=black,inner sep=0]{\textbf{loop}};
\node at (89.4pt,172.0833pt)[below right,color=black,inner sep=0]{\textbf{[}};
\node at (92.59pt,170.8333pt)[below right,inner sep=0]{$\textbf{foreach } r \in \{r_{max} + 1, \dots\}$};
\node at (215.4514pt,172.0833pt)[below right,color=black,inner sep=0]{\textbf{]}};
\draw[pstyle4] (35pt,202.8333pt) -- (25pt,206.8333pt) -- (35pt,210.8333pt) -- (31pt,206.8333pt) -- cycle;
\draw[pstyle5] (29pt,206.8333pt) -- (108.3255pt,206.8333pt);
\node at (41pt,194.8333pt)[below right,inner sep=0]{$PROVE(r)$};
\draw[pstyle4] (35pt,226.8333pt) -- (25pt,230.8333pt) -- (35pt,234.8333pt) -- (31pt,230.8333pt) -- cycle;
\draw[pstyle5] (29pt,230.8333pt) -- (108.3255pt,230.8333pt);
\node at (41pt,218.8333pt)[below right,inner sep=0]{$APPEND(r)$};
\draw[pstyle4] (35pt,250.8333pt) -- (25pt,254.8333pt) -- (35pt,258.8333pt) -- (31pt,254.8333pt) -- cycle;
\draw[pstyle5] (29pt,254.8333pt) -- (108.3255pt,254.8333pt);
\node at (41pt,242.8333pt)[below right,inner sep=0]{$READ()$};
\draw[pstyle4] (97.3255pt,271.6666pt) -- (107.3255pt,275.6666pt) -- (97.3255pt,279.6666pt) -- (101.3255pt,275.6666pt) -- cycle;
\draw[pstyle6] (24pt,275.6666pt) -- (103.3255pt,275.6666pt);
\node at (31pt,266.8333pt)[below right,inner sep=0]{$P$};
\draw[pstyle7] (65.7255pt,287.6666pt) -- (123.9755pt,287.6666pt) -- (123.9755pt,289.6666pt) -- (113.9755pt,299.6666pt) -- (65.7255pt,299.6666pt) -- (65.7255pt,287.6666pt);
\draw[pstyle8] (65.7255pt,287.6666pt) rectangle (234.8182pt,339.6666pt);
\node at (80.7255pt,288.6666pt)[below right,color=black,inner sep=0]{\textbf{alt}};
\node at (138.9755pt,290.9166pt)[below right,color=black,inner sep=0]{\textbf{[}};
\node at (142.1655pt,289.6666pt)[below right,inner sep=0]{$(1, \text{prove(}r\text{)}) \in P$};
\node at (215.6282pt,290.9166pt)[below right,color=black,inner sep=0]{\textbf{]}};
\draw[pstyle9] (86.7255pt,314.6666pt) -- (86.7255pt,334.6666pt) -- (131.7255pt,334.6666pt) -- (131.7255pt,324.6666pt) -- (121.7255pt,314.6666pt) -- (86.7255pt,314.6666pt);
\draw[pstyle9] (121.7255pt,314.6666pt) -- (121.7255pt,324.6666pt) -- (131.7255pt,324.6666pt) -- (121.7255pt,314.6666pt);
\node at (92.7255pt,319.6666pt)[below right,color=black,inner sep=0]{break};
\draw[pstyle5] (277.3933pt,383.6666pt) -- (319.3933pt,383.6666pt);
\draw[pstyle5] (319.3933pt,383.6666pt) -- (319.3933pt,396.6666pt);
\draw[pstyle5] (278.3933pt,396.6666pt) -- (319.3933pt,396.6666pt);
\draw[pstyle4] (288.3933pt,392.6666pt) -- (278.3933pt,396.6666pt) -- (288.3933pt,400.6666pt) -- (284.3933pt,396.6666pt) -- cycle;
\node at (284.3933pt,371.6666pt)[below right,inner sep=0]{$ABdeliver()$};
\draw[pstyle4] (35pt,416.6666pt) -- (25pt,420.6666pt) -- (35pt,424.6666pt) -- (31pt,420.6666pt) -- cycle;
\draw[pstyle5] (29pt,420.6666pt) -- (276.3933pt,420.6666pt);
\node at (41pt,408.6666pt)[below right,inner sep=0]{$READ()$};
\draw[pstyle4] (265.3933pt,437.4999pt) -- (275.3933pt,441.4999pt) -- (265.3933pt,445.4999pt) -- (269.3933pt,441.4999pt) -- cycle;
\draw[pstyle6] (24pt,441.4999pt) -- (271.3933pt,441.4999pt);
\node at (31pt,432.6666pt)[below right,inner sep=0]{$P$};
\draw[pstyle9] (195.7533pt,454.4999pt) -- (195.7533pt,534.4999pt) -- (358.7533pt,534.4999pt) -- (358.7533pt,464.4999pt) -- (348.7533pt,454.4999pt) -- (195.7533pt,454.4999pt);
\draw[pstyle9] (348.7533pt,454.4999pt) -- (348.7533pt,464.4999pt) -- (358.7533pt,464.4999pt) -- (348.7533pt,454.4999pt);
\node at (201.7533pt,459.4999pt)[below right,color=black,inner sep=0]{line(C4)};
\node at (201.7533pt,470.4999pt)[below right,color=black,inner sep=0]{process P2 check locally if~};
\node at (201.7533pt,480.4999pt)[below right,inner sep=0]{$\forall j : (j, prove(r)) \not\in P$};
\node at (201.7533pt,491.4999pt)[below right,color=black,inner sep=0]{which is false since P1 correctly~};
\node at (201.7533pt,501.4999pt)[below right,color=black,inner sep=0]{PROVE(r) and APPEND(r)};
\node at (201.7533pt,511.4999pt)[below right,color=black,inner sep=0]{~};
\node at (201.7533pt,521.4999pt)[below right,inner sep=0]{$\text{P1 is next include in } W_r$};
\draw[pstyle4] (35pt,551.9399pt) -- (25pt,555.9399pt) -- (35pt,559.9399pt) -- (31pt,555.9399pt) -- cycle;
\draw[pstyle5] (29pt,555.9399pt) -- (276.3933pt,555.9399pt);
\node at (41pt,543.9399pt)[below right,inner sep=0]{$APPEND(r)$};
\draw[pstyle4] (35pt,575.9399pt) -- (25pt,579.9399pt) -- (35pt,583.9399pt) -- (31pt,579.9399pt) -- cycle;
\draw[pstyle5] (29pt,579.9399pt) -- (276.3933pt,579.9399pt);
\node at (41pt,567.9399pt)[below right,inner sep=0]{$READ()$};
\draw[pstyle4] (265.3933pt,596.7732pt) -- (275.3933pt,600.7732pt) -- (265.3933pt,604.7732pt) -- (269.3933pt,600.7732pt) -- cycle;
\draw[pstyle6] (24pt,600.7732pt) -- (271.3933pt,600.7732pt);
\node at (31pt,591.9399pt)[below right,inner sep=0]{$P$};
\draw[pstyle9] (189.1283pt,613.7732pt) -- (189.1283pt,706.7732pt) -- (365.1283pt,706.7732pt) -- (365.1283pt,623.7732pt) -- (355.1283pt,613.7732pt) -- (189.1283pt,613.7732pt);
\draw[pstyle9] (355.1283pt,613.7732pt) -- (355.1283pt,623.7732pt) -- (365.1283pt,623.7732pt) -- (355.1283pt,613.7732pt);
\node at (195.1283pt,618.7732pt)[below right,color=black,inner sep=0]{line(C9)};
\node at (195.1283pt,629.7732pt)[below right,color=black,inner sep=0]{process P2 check locally if};
\node at (195.1283pt,639.7732pt)[below right,inner sep=0]{$\forall j \in W_r : prop[r][j] = \bot$};
\node at (195.1283pt,650.7732pt)[below right,color=black,inner sep=0]{which can't be false since P1 didn't};
\node at (195.1283pt,662.6982pt)[below right,color=black,inner sep=0]{execute~};
\node at (230.9483pt,660.7732pt)[below right,inner sep=0]{$RBcast(prop, S, r, 1)$};
\node at (195.1283pt,672.6982pt)[below right,color=black,inner sep=0]{~};
\node at (195.1283pt,682.6982pt)[below right,color=black,inner sep=0]{P2 will never progress and};
\node at (195.1283pt,692.6982pt)[below right,color=black,inner sep=0]{deliver any futur messages};
\end{tikzpicture}

37
Recherche/BFT-ARBover/diagrams/classic_seq.puml Normal file
View File

@@ -0,0 +1,37 @@
@startuml
!pragma teoz true
database DL
actor P1
actor P2
actor Pt
actor Pn
P1 ->(05) P2: <latex>RBcast(prop, S, r, 1)</latex>
& P1 ->(25) Pt : <latex>RBcast(prop, S, r, 1)</latex>
& P1 ->(50) Pn : <latex>RBcast(prop, S, r, 1)</latex>
P2 -> P2 : <latex>S'(sk_2, r)</latex>
P2 -> P1 : <latex>send(\sigma_2)</latex>
... <latex>\text{Wait until P1 received }\sigma \text{ t times}</latex> ...
Pt -> Pt : <latex>S'(sk_t, r)</latex>
Pt -> P1 : <latex>send(\sigma_t)</latex>
P1 -> P1 : <latex>C'(pkc, r, J, \{\sigma_r^j\}_{j\in J})</latex>
P1 -> DL : <latex>PROVE(\sigma)</latex>
P1 -> DL : <latex>APPEND(\sigma)</latex>
P2 -> Pt
P1 ->(05) P2: <latex>RBcast(submit, S, r, 1, \sigma)</latex>
& P1 ->(25) Pt : <latex>RBcast(submit, S, r, 1, \sigma)</latex>
& P1 ->(50) Pn : <latex>RBcast(submit, S, r, 1, \sigma)</latex>
P2 -> DL : <latex>P \gets READ()</latex>
& Pt -> DL
& Pn -> DL
P2 -> P2 : <latex>V'(pk, r, \sigma)</latex>
& Pt -> Pt : <latex>V'(pk, r, \sigma)</latex>
& Pn -> Pn : <latex>V'(pk, r, \sigma)</latex>
hide footbox
@enduml

127
Recherche/BFT-ARBover/diagrams/classic_seq.tex Normal file
View File

@@ -0,0 +1,127 @@
% generated by Plantuml 1.2025.10
\definecolor{plantucolor0000}{RGB}{255,255,255}
\definecolor{plantucolor0001}{RGB}{24,24,24}
\definecolor{plantucolor0002}{RGB}{0,0,0}
\definecolor{plantucolor0003}{RGB}{226,226,240}
\begin{tikzpicture}[yscale=-1
,pstyle0/.style={color=plantucolor0000,line width=0.0pt}
,pstyle1/.style={color=plantucolor0001,line width=0.5pt,dash pattern=on 5.0pt off 5.0pt}
,pstyle2/.style={color=plantucolor0001,line width=0.5pt,dash pattern=on 1.0pt off 4.0pt}
,pstyle3/.style={color=plantucolor0001,fill=plantucolor0003,line width=0.5pt}
,pstyle4/.style={color=plantucolor0001,line width=0.5pt}
,pstyle5/.style={color=plantucolor0001,fill=plantucolor0001,line width=1.0pt}
,pstyle6/.style={color=plantucolor0001,line width=1.0pt}
]
\draw[pstyle0] (19.5pt,75pt) rectangle (27.5pt,218.0178pt);
\draw[pstyle1] (23pt,75pt) -- (23pt,218.0178pt);
\draw[pstyle2] (23pt,218.0178pt) -- (23pt,256.0178pt);
\draw[pstyle0] (19.5pt,256.0178pt) rectangle (27.5pt,562.1754pt);
\draw[pstyle1] (23pt,256.0178pt) -- (23pt,562.1754pt);
\draw[pstyle0] (106.109pt,75pt) rectangle (114.109pt,218.0178pt);
\draw[pstyle1] (109.609pt,75pt) -- (109.609pt,218.0178pt);
\draw[pstyle2] (109.609pt,218.0178pt) -- (109.609pt,256.0178pt);
\draw[pstyle0] (106.109pt,256.0178pt) rectangle (114.109pt,562.1754pt);
\draw[pstyle1] (109.609pt,256.0178pt) -- (109.609pt,562.1754pt);
\draw[pstyle0] (241.3331pt,75pt) rectangle (249.3331pt,218.0178pt);
\draw[pstyle1] (244.8331pt,75pt) -- (244.8331pt,218.0178pt);
\draw[pstyle2] (244.8331pt,218.0178pt) -- (244.8331pt,256.0178pt);
\draw[pstyle0] (241.3331pt,256.0178pt) rectangle (249.3331pt,562.1754pt);
\draw[pstyle1] (244.8331pt,256.0178pt) -- (244.8331pt,562.1754pt);
\draw[pstyle0] (303.7197pt,75pt) rectangle (311.7197pt,218.0178pt);
\draw[pstyle1] (307.2197pt,75pt) -- (307.2197pt,218.0178pt);
\draw[pstyle2] (307.2197pt,218.0178pt) -- (307.2197pt,256.0178pt);
\draw[pstyle0] (303.7197pt,256.0178pt) rectangle (311.7197pt,562.1754pt);
\draw[pstyle1] (307.2197pt,256.0178pt) -- (307.2197pt,562.1754pt);
\draw[pstyle0] (366.1062pt,75pt) rectangle (374.1062pt,218.0178pt);
\draw[pstyle1] (369.6062pt,75pt) -- (369.6062pt,218.0178pt);
\draw[pstyle2] (369.6062pt,218.0178pt) -- (369.6062pt,256.0178pt);
\draw[pstyle0] (366.1062pt,256.0178pt) rectangle (374.1062pt,562.1754pt);
\draw[pstyle1] (369.6062pt,256.0178pt) -- (369.6062pt,562.1754pt);
\node at (13.055pt,65pt)[below right,color=black,inner sep=0]{DL};
\draw[pstyle3] (5pt,29pt) ..controls (5pt,19pt) and (23pt,19pt) .. (23pt,19pt) ..controls (23pt,19pt) and (41pt,19pt) .. (41pt,29pt) -- (41pt,55pt) ..controls (41pt,65pt) and (23pt,65pt) .. (23pt,65pt) ..controls (23pt,65pt) and (5pt,65pt) .. (5pt,55pt) -- (5pt,29pt);
\draw[pstyle4] (5pt,29pt) ..controls (5pt,39pt) and (23pt,39pt) .. (23pt,39pt) ..controls (23pt,39pt) and (41pt,39pt) .. (41pt,29pt);
\node at (100.704pt,65pt)[below right,color=black,inner sep=0]{P1};
\draw[pstyle3] (109.609pt,13.5pt) ellipse (8pt and 8pt);
\draw[pstyle4] (109.609pt,21.5pt) -- (109.609pt,48.5pt)(96.609pt,29.5pt) -- (122.609pt,29.5pt)(109.609pt,48.5pt) -- (96.609pt,63.5pt)(109.609pt,48.5pt) -- (122.609pt,63.5pt);
\node at (235.9281pt,65pt)[below right,color=black,inner sep=0]{P2};
\draw[pstyle3] (244.8331pt,13.5pt) ellipse (8pt and 8pt);
\draw[pstyle4] (244.8331pt,21.5pt) -- (244.8331pt,48.5pt)(231.8331pt,29.5pt) -- (257.8331pt,29.5pt)(244.8331pt,48.5pt) -- (231.8331pt,63.5pt)(244.8331pt,48.5pt) -- (257.8331pt,63.5pt);
\node at (298.8697pt,65pt)[below right,color=black,inner sep=0]{Pt};
\draw[pstyle3] (307.2197pt,13.5pt) ellipse (8pt and 8pt);
\draw[pstyle4] (307.2197pt,21.5pt) -- (307.2197pt,48.5pt)(294.2197pt,29.5pt) -- (320.2197pt,29.5pt)(307.2197pt,48.5pt) -- (294.2197pt,63.5pt)(307.2197pt,48.5pt) -- (320.2197pt,63.5pt);
\node at (360.4212pt,65pt)[below right,color=black,inner sep=0]{Pn};
\draw[pstyle3] (369.6062pt,13.5pt) ellipse (8pt and 8pt);
\draw[pstyle4] (369.6062pt,21.5pt) -- (369.6062pt,48.5pt)(356.6062pt,29.5pt) -- (382.6062pt,29.5pt)(369.6062pt,48.5pt) -- (356.6062pt,63.5pt)(369.6062pt,48.5pt) -- (382.6062pt,63.5pt);
\draw[pstyle5] (232.9877pt,99.6332pt) -- (242.8331pt,104pt) -- (232.6921pt,107.6278pt) -- (236.8372pt,103.7783pt) -- cycle;
\draw[pstyle6] (109.609pt,99pt) -- (242.8331pt,104pt);
\node at (116.609pt,87pt)[below right,inner sep=0]{$RBcast(prop, S, r, 1)$};
\draw[pstyle5] (295.8008pt,118.7765pt) -- (305.2197pt,124pt) -- (294.7967pt,126.7133pt) -- (299.2671pt,123.2469pt) -- cycle;
\draw[pstyle6] (109.609pt,99pt) -- (305.2197pt,124pt);
\node at (116.609pt,87pt)[below right,inner sep=0]{$RBcast(prop, S, r, 1)$};
\draw[pstyle5] (358.5415pt,143.1835pt) -- (367.6062pt,149pt) -- (357.0307pt,151.0395pt) -- (361.7142pt,147.8669pt) -- cycle;
\draw[pstyle6] (109.609pt,99pt) -- (367.6062pt,149pt);
\node at (116.609pt,87pt)[below right,inner sep=0]{$RBcast(prop, S, r, 1)$};
\draw[pstyle6] (244.8331pt,173.0178pt) -- (286.8331pt,173.0178pt);
\draw[pstyle6] (286.8331pt,173.0178pt) -- (286.8331pt,186.0178pt);
\draw[pstyle6] (245.8331pt,186.0178pt) -- (286.8331pt,186.0178pt);
\draw[pstyle5] (255.8331pt,182.0178pt) -- (245.8331pt,186.0178pt) -- (255.8331pt,190.0178pt) -- (251.8331pt,186.0178pt) -- cycle;
\node at (251.8331pt,161pt)[below right,inner sep=0]{$S'(sk_2, r)$};
\draw[pstyle5] (120.609pt,206.0178pt) -- (110.609pt,210.0178pt) -- (120.609pt,214.0178pt) -- (116.609pt,210.0178pt) -- cycle;
\draw[pstyle6] (114.609pt,210.0178pt) -- (243.8331pt,210.0178pt);
\node at (126.609pt,198.0178pt)[below right,inner sep=0]{$send(\sigma_2)$};
\node at (122.1916pt,232.0178pt)[below right,color=black,inner sep=0]{~};
\node at (125.5216pt,234.8578pt)[below right,inner sep=0]{$\text{Wait until P1 received }\sigma \text{ t times}$};
\node at (267.0846pt,232.0178pt)[below right,color=black,inner sep=0]{~};
\draw[pstyle6] (307.2197pt,272.0356pt) -- (349.2197pt,272.0356pt);
\draw[pstyle6] (349.2197pt,272.0356pt) -- (349.2197pt,285.0356pt);
\draw[pstyle6] (308.2197pt,285.0356pt) -- (349.2197pt,285.0356pt);
\draw[pstyle5] (318.2197pt,281.0356pt) -- (308.2197pt,285.0356pt) -- (318.2197pt,289.0356pt) -- (314.2197pt,285.0356pt) -- cycle;
\node at (314.2197pt,260.0178pt)[below right,inner sep=0]{$S'(sk_t, r)$};
\draw[pstyle5] (120.609pt,305.0356pt) -- (110.609pt,309.0356pt) -- (120.609pt,313.0356pt) -- (116.609pt,309.0356pt) -- cycle;
\draw[pstyle6] (114.609pt,309.0356pt) -- (306.2197pt,309.0356pt);
\node at (126.609pt,297.0356pt)[below right,inner sep=0]{$send(\sigma_t)$};
\draw[pstyle6] (109.609pt,334.1576pt) -- (151.609pt,334.1576pt);
\draw[pstyle6] (151.609pt,334.1576pt) -- (151.609pt,347.1576pt);
\draw[pstyle6] (110.609pt,347.1576pt) -- (151.609pt,347.1576pt);
\draw[pstyle5] (120.609pt,343.1576pt) -- (110.609pt,347.1576pt) -- (120.609pt,351.1576pt) -- (116.609pt,347.1576pt) -- cycle;
\node at (116.609pt,321.0356pt)[below right,inner sep=0]{$C'(pkc, r, J, \{\sigma_r^j\}_{j\in J})$};
\draw[pstyle5] (34pt,367.1576pt) -- (24pt,371.1576pt) -- (34pt,375.1576pt) -- (30pt,371.1576pt) -- cycle;
\draw[pstyle6] (28pt,371.1576pt) -- (108.609pt,371.1576pt);
\node at (40pt,359.1576pt)[below right,inner sep=0]{$PROVE(\sigma)$};
\draw[pstyle5] (34pt,391.1576pt) -- (24pt,395.1576pt) -- (34pt,399.1576pt) -- (30pt,395.1576pt) -- cycle;
\draw[pstyle6] (28pt,395.1576pt) -- (108.609pt,395.1576pt);
\node at (40pt,383.1576pt)[below right,inner sep=0]{$APPEND(\sigma)$};
\draw[pstyle5] (295.2197pt,405.1576pt) -- (305.2197pt,409.1576pt) -- (295.2197pt,413.1576pt) -- (299.2197pt,409.1576pt) -- cycle;
\draw[pstyle6] (244.8331pt,409.1576pt) -- (301.2197pt,409.1576pt);
\draw[pstyle5] (232.9877pt,433.7908pt) -- (242.8331pt,438.1576pt) -- (232.6921pt,441.7853pt) -- (236.8372pt,437.9359pt) -- cycle;
\draw[pstyle6] (109.609pt,433.1576pt) -- (242.8331pt,438.1576pt);
\node at (116.609pt,421.1576pt)[below right,inner sep=0]{$RBcast(submit, S, r, 1, \sigma)$};
\draw[pstyle5] (295.8008pt,452.9341pt) -- (305.2197pt,458.1576pt) -- (294.7967pt,460.8708pt) -- (299.2671pt,457.4045pt) -- cycle;
\draw[pstyle6] (109.609pt,433.1576pt) -- (305.2197pt,458.1576pt);
\node at (116.609pt,421.1576pt)[below right,inner sep=0]{$RBcast(submit, S, r, 1, \sigma)$};
\draw[pstyle5] (358.5415pt,477.3411pt) -- (367.6062pt,483.1576pt) -- (357.0307pt,485.1971pt) -- (361.7142pt,482.0245pt) -- cycle;
\draw[pstyle6] (109.609pt,433.1576pt) -- (367.6062pt,483.1576pt);
\node at (116.609pt,421.1576pt)[below right,inner sep=0]{$RBcast(submit, S, r, 1, \sigma)$};
\draw[pstyle5] (34pt,503.1576pt) -- (24pt,507.1576pt) -- (34pt,511.1576pt) -- (30pt,507.1576pt) -- cycle;
\draw[pstyle6] (28pt,507.1576pt) -- (243.8331pt,507.1576pt);
\node at (40pt,495.1576pt)[below right,inner sep=0]{$P \gets READ()$};
\draw[pstyle5] (34pt,503.1576pt) -- (24pt,507.1576pt) -- (34pt,511.1576pt) -- (30pt,507.1576pt) -- cycle;
\draw[pstyle6] (28pt,507.1576pt) -- (306.2197pt,507.1576pt);
\draw[pstyle5] (34pt,503.1576pt) -- (24pt,507.1576pt) -- (34pt,511.1576pt) -- (30pt,507.1576pt) -- cycle;
\draw[pstyle6] (28pt,507.1576pt) -- (368.6062pt,507.1576pt);
\draw[pstyle6] (244.8331pt,531.1754pt) -- (286.8331pt,531.1754pt);
\draw[pstyle6] (286.8331pt,531.1754pt) -- (286.8331pt,544.1754pt);
\draw[pstyle6] (245.8331pt,544.1754pt) -- (286.8331pt,544.1754pt);
\draw[pstyle5] (255.8331pt,540.1754pt) -- (245.8331pt,544.1754pt) -- (255.8331pt,548.1754pt) -- (251.8331pt,544.1754pt) -- cycle;
\node at (251.8331pt,519.1576pt)[below right,inner sep=0]{$V'(pk, r, \sigma)$};
\draw[pstyle6] (307.2197pt,531.1754pt) -- (349.2197pt,531.1754pt);
\draw[pstyle6] (349.2197pt,531.1754pt) -- (349.2197pt,544.1754pt);
\draw[pstyle6] (308.2197pt,544.1754pt) -- (349.2197pt,544.1754pt);
\draw[pstyle5] (318.2197pt,540.1754pt) -- (308.2197pt,544.1754pt) -- (318.2197pt,548.1754pt) -- (314.2197pt,544.1754pt) -- cycle;
\node at (314.2197pt,519.1576pt)[below right,inner sep=0]{$V'(pk, r, \sigma)$};
\draw[pstyle6] (369.6062pt,531.1754pt) -- (411.6062pt,531.1754pt);
\draw[pstyle6] (411.6062pt,531.1754pt) -- (411.6062pt,544.1754pt);
\draw[pstyle6] (370.6062pt,544.1754pt) -- (411.6062pt,544.1754pt);
\draw[pstyle5] (380.6062pt,540.1754pt) -- (370.6062pt,544.1754pt) -- (380.6062pt,548.1754pt) -- (376.6062pt,544.1754pt) -- cycle;
\node at (376.6062pt,519.1576pt)[below right,inner sep=0]{$V'(pk, r, \sigma)$};
\end{tikzpicture}

32
Recherche/BFT-ARBover/diagrams/nonBFT_behaviour.puml Normal file
View File

@@ -0,0 +1,32 @@
@startuml
!pragma teoz true
database DL
actor P1
actor Pi
P1 -> P1 : <latex>ABcast(m)</latex>
P1 -> P1 : <latex>m \in S</latex>
P1 -> DL : <latex>READ()</latex>
DL --> P1 : <latex>P</latex>
P1 -> P1 : <latex>r_{max} = max\{r : (\_, prove(r)) \in P\}</latex>
loop <latex>\textbf{foreach } r \in \{r_{max} + 1, \dots\}</latex>
P1 ->(05) Pi : <latex>RBcast(prop, S, r, 1)</latex>
P1 -> DL : <latex>PROVE(r)</latex>
P1 -> DL : <latex>APPEND(r)</latex>
P1 -> DL : <latex>READ()</latex>
DL --> P1 : <latex>P</latex>
alt <latex>(1, \text{prove(}r\text{)}) \in P</latex>
note over P1 : break
else <latex>(\exists j, r' : (j, prove(r')) \in P \land m \in prop[r'][j])</latex>
note over P1 : break
end
end
hide footbox
@enduml

93
Recherche/BFT-ARBover/diagrams/nonBFT_behaviour.tex Normal file
View File

@@ -0,0 +1,93 @@
% generated by Plantuml 1.2025.10
\definecolor{plantucolor0000}{RGB}{255,255,255}
\definecolor{plantucolor0001}{RGB}{24,24,24}
\definecolor{plantucolor0002}{RGB}{0,0,0}
\definecolor{plantucolor0003}{RGB}{226,226,240}
\definecolor{plantucolor0004}{RGB}{238,238,238}
\definecolor{plantucolor0005}{RGB}{254,255,221}
\begin{tikzpicture}[yscale=-1
,pstyle0/.style={color=plantucolor0000,line width=0.0pt}
,pstyle1/.style={color=plantucolor0001,line width=0.5pt,dash pattern=on 5.0pt off 5.0pt}
,pstyle2/.style={color=plantucolor0001,fill=plantucolor0003,line width=0.5pt}
,pstyle3/.style={color=plantucolor0001,line width=0.5pt}
,pstyle4/.style={color=plantucolor0001,line width=1.0pt}
,pstyle5/.style={color=plantucolor0001,fill=plantucolor0001,line width=1.0pt}
,pstyle6/.style={color=plantucolor0001,line width=1.0pt,dash pattern=on 2.0pt off 2.0pt}
,pstyle7/.style={color=black,fill=plantucolor0004,line width=1.5pt}
,pstyle8/.style={color=black,line width=1.5pt}
,pstyle10/.style={color=plantucolor0001,fill=plantucolor0005,line width=0.5pt}
]
\draw[pstyle0] (20.5pt,75pt) rectangle (28.5pt,537.1498pt);
\draw[pstyle1] (24pt,75pt) -- (24pt,537.1498pt);
\draw[pstyle0] (105.8255pt,75pt) rectangle (113.8255pt,537.1498pt);
\draw[pstyle1] (109.3255pt,75pt) -- (109.3255pt,537.1498pt);
\draw[pstyle0] (273.8933pt,75pt) rectangle (281.8933pt,537.1498pt);
\draw[pstyle1] (277.3933pt,75pt) -- (277.3933pt,537.1498pt);
\node at (14.055pt,65pt)[below right,color=black,inner sep=0]{DL};
\draw[pstyle2] (6pt,29pt) ..controls (6pt,19pt) and (24pt,19pt) .. (24pt,19pt) ..controls (24pt,19pt) and (42pt,19pt) .. (42pt,29pt) -- (42pt,55pt) ..controls (42pt,65pt) and (24pt,65pt) .. (24pt,65pt) ..controls (24pt,65pt) and (6pt,65pt) .. (6pt,55pt) -- (6pt,29pt);
\draw[pstyle3] (6pt,29pt) ..controls (6pt,39pt) and (24pt,39pt) .. (24pt,39pt) ..controls (24pt,39pt) and (42pt,39pt) .. (42pt,29pt);
\node at (100.4205pt,65pt)[below right,color=black,inner sep=0]{P1};
\draw[pstyle2] (109.3255pt,13.5pt) ellipse (8pt and 8pt);
\draw[pstyle3] (109.3255pt,21.5pt) -- (109.3255pt,48.5pt)(96.3255pt,29.5pt) -- (122.3255pt,29.5pt)(109.3255pt,48.5pt) -- (96.3255pt,63.5pt)(109.3255pt,48.5pt) -- (122.3255pt,63.5pt);
\node at (269.5983pt,65pt)[below right,color=black,inner sep=0]{Pi};
\draw[pstyle2] (277.3933pt,13.5pt) ellipse (8pt and 8pt);
\draw[pstyle3] (277.3933pt,21.5pt) -- (277.3933pt,48.5pt)(264.3933pt,29.5pt) -- (290.3933pt,29.5pt)(277.3933pt,48.5pt) -- (264.3933pt,63.5pt)(277.3933pt,48.5pt) -- (290.3933pt,63.5pt);
\draw[pstyle4] (109.3255pt,99pt) -- (151.3255pt,99pt);
\draw[pstyle4] (151.3255pt,99pt) -- (151.3255pt,112pt);
\draw[pstyle4] (110.3255pt,112pt) -- (151.3255pt,112pt);
\draw[pstyle5] (120.3255pt,108pt) -- (110.3255pt,112pt) -- (120.3255pt,116pt) -- (116.3255pt,112pt) -- cycle;
\node at (116.3255pt,87pt)[below right,inner sep=0]{$ABcast(m)$};
\draw[pstyle4] (109.3255pt,133.2243pt) -- (151.3255pt,133.2243pt);
\draw[pstyle4] (151.3255pt,133.2243pt) -- (151.3255pt,146.2243pt);
\draw[pstyle4] (110.3255pt,146.2243pt) -- (151.3255pt,146.2243pt);
\draw[pstyle5] (120.3255pt,142.2243pt) -- (110.3255pt,146.2243pt) -- (120.3255pt,150.2243pt) -- (116.3255pt,146.2243pt) -- cycle;
\node at (116.3255pt,124pt)[below right,inner sep=0]{$m \in S$};
\draw[pstyle5] (35pt,166.2243pt) -- (25pt,170.2243pt) -- (35pt,174.2243pt) -- (31pt,170.2243pt) -- cycle;
\draw[pstyle4] (29pt,170.2243pt) -- (108.3255pt,170.2243pt);
\node at (41pt,158.2243pt)[below right,inner sep=0]{$READ()$};
\draw[pstyle5] (97.3255pt,187.0576pt) -- (107.3255pt,191.0576pt) -- (97.3255pt,195.0576pt) -- (101.3255pt,191.0576pt) -- cycle;
\draw[pstyle6] (24pt,191.0576pt) -- (103.3255pt,191.0576pt);
\node at (31pt,182.2243pt)[below right,inner sep=0]{$P$};
\draw[pstyle4] (109.3255pt,215.0576pt) -- (151.3255pt,215.0576pt);
\draw[pstyle4] (151.3255pt,215.0576pt) -- (151.3255pt,228.0576pt);
\draw[pstyle4] (110.3255pt,228.0576pt) -- (151.3255pt,228.0576pt);
\draw[pstyle5] (120.3255pt,224.0576pt) -- (110.3255pt,228.0576pt) -- (120.3255pt,232.0576pt) -- (116.3255pt,228.0576pt) -- cycle;
\node at (116.3255pt,203.0576pt)[below right,inner sep=0]{$r_{max} = max\{r : (\_, prove(r)) \in P\}$};
\draw[pstyle7] (8pt,240.0576pt) -- (74.4pt,240.0576pt) -- (74.4pt,242.0576pt) -- (64.4pt,252.0576pt) -- (8pt,252.0576pt) -- (8pt,240.0576pt);
\draw[pstyle8] (8pt,240.0576pt) rectangle (293.4464pt,513.1498pt);
\node at (23pt,241.0576pt)[below right,color=black,inner sep=0]{\textbf{loop}};
\node at (89.4pt,243.3076pt)[below right,color=black,inner sep=0]{\textbf{[}};
\node at (92.59pt,242.0576pt)[below right,inner sep=0]{$\textbf{foreach } r \in \{r_{max} + 1, \dots\}$};
\node at (215.4514pt,243.3076pt)[below right,color=black,inner sep=0]{\textbf{]}};
\draw[pstyle5] (265.5167pt,278.762pt) -- (275.3933pt,283.0576pt) -- (265.2788pt,286.7585pt) -- (269.396pt,282.8792pt) -- cycle;
\draw[pstyle4] (109.3255pt,278.0576pt) -- (275.3933pt,283.0576pt);
\node at (116.3255pt,266.0576pt)[below right,inner sep=0]{$RBcast(prop, S, r, 1)$};
\draw[pstyle5] (35pt,303.0576pt) -- (25pt,307.0576pt) -- (35pt,311.0576pt) -- (31pt,307.0576pt) -- cycle;
\draw[pstyle4] (29pt,307.0576pt) -- (108.3255pt,307.0576pt);
\node at (41pt,295.0576pt)[below right,inner sep=0]{$PROVE(r)$};
\draw[pstyle5] (35pt,327.0576pt) -- (25pt,331.0576pt) -- (35pt,335.0576pt) -- (31pt,331.0576pt) -- cycle;
\draw[pstyle4] (29pt,331.0576pt) -- (108.3255pt,331.0576pt);
\node at (41pt,319.0576pt)[below right,inner sep=0]{$APPEND(r)$};
\draw[pstyle5] (35pt,351.0576pt) -- (25pt,355.0576pt) -- (35pt,359.0576pt) -- (31pt,355.0576pt) -- cycle;
\draw[pstyle4] (29pt,355.0576pt) -- (108.3255pt,355.0576pt);
\node at (41pt,343.0576pt)[below right,inner sep=0]{$READ()$};
\draw[pstyle5] (97.3255pt,371.8909pt) -- (107.3255pt,375.8909pt) -- (97.3255pt,379.8909pt) -- (101.3255pt,375.8909pt) -- cycle;
\draw[pstyle6] (24pt,375.8909pt) -- (103.3255pt,375.8909pt);
\node at (31pt,367.0576pt)[below right,inner sep=0]{$P$};
\draw[pstyle7] (65.7255pt,387.8909pt) -- (123.9755pt,387.8909pt) -- (123.9755pt,389.8909pt) -- (113.9755pt,399.8909pt) -- (65.7255pt,399.8909pt) -- (65.7255pt,387.8909pt);
\draw[pstyle8] (65.7255pt,387.8909pt) rectangle (268.4464pt,499.1498pt);
\node at (80.7255pt,388.8909pt)[below right,color=black,inner sep=0]{\textbf{alt}};
\node at (138.9755pt,391.1409pt)[below right,color=black,inner sep=0]{\textbf{[}};
\node at (142.1655pt,389.8909pt)[below right,inner sep=0]{$(1, \text{prove(}r\text{)}) \in P$};
\node at (215.6282pt,391.1409pt)[below right,color=black,inner sep=0]{\textbf{]}};
\draw[color=black,line width=1.0pt,dash pattern=on 2.0pt off 2.0pt] (65.7255pt,450.8909pt) -- (268.4464pt,450.8909pt);
\node at (70.7255pt,454.1498pt)[below right,color=black,inner sep=0]{\textbf{[}};
\node at (73.9155pt,452.8909pt)[below right,inner sep=0]{$(\exists j, r' : (j, prove(r')) \in P \land m \in prop[r'][j])$};
\node at (263.2564pt,454.1498pt)[below right,color=black,inner sep=0]{\textbf{]}};
\draw[pstyle10] (86.7255pt,414.8909pt) -- (86.7255pt,434.8909pt) -- (131.7255pt,434.8909pt) -- (131.7255pt,424.8909pt) -- (121.7255pt,414.8909pt) -- (86.7255pt,414.8909pt);
\draw[pstyle10] (121.7255pt,414.8909pt) -- (121.7255pt,424.8909pt) -- (131.7255pt,424.8909pt) -- (121.7255pt,414.8909pt);
\node at (92.7255pt,419.8909pt)[below right,color=black,inner sep=0]{break};
\draw[pstyle10] (86.7255pt,474.1498pt) -- (86.7255pt,494.1498pt) -- (131.7255pt,494.1498pt) -- (131.7255pt,484.1498pt) -- (121.7255pt,474.1498pt) -- (86.7255pt,474.1498pt);
\draw[pstyle10] (121.7255pt,474.1498pt) -- (121.7255pt,484.1498pt) -- (131.7255pt,484.1498pt) -- (121.7255pt,474.1498pt);
\node at (92.7255pt,479.1498pt)[below right,color=black,inner sep=0]{break};
\end{tikzpicture}

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

Binary file not shown.

933
Recherche/BFT-ARBover/main.tex Normal file
View File

@@ -0,0 +1,933 @@
\documentclass[11pt]{article}
\usepackage[margin=1in]{geometry}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{lmodern}
\usepackage{microtype}
\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{thmtools}
\usepackage{enumitem}
\usepackage{csquotes}
\usepackage[hidelinks]{hyperref}
\usepackage[nameinlink,noabbrev]{cleveref}
\usepackage{algorithm}
\usepackage{algpseudocode}
\usepackage{graphicx}
% Line-number prefix configuration (A/B/C)
\renewcommand{\thealgorithm}{\Alph{algorithm}} % Float labels: Algorithm A, B, C
\newcommand{\algletter}{}
\algrenewcommand\alglinenumber[1]{\scriptsize\textbf{\algletter}#1}
\usepackage{tikz}
\graphicspath{{diagrams/out}}
\usepackage{xspace}
% \usepackage{plantuml}
\usepackage[fr-FR]{datetime2}
\usepackage{fancyhdr}
\pagestyle{fancy}
\fancyhf{}
\fancyfoot[L]{Compilé le \DTMnow}
\fancyfoot[C]{\thepage}
\renewcommand{\headrulewidth}{0pt}
\renewcommand{\footrulewidth}{0pt}
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\theoremstyle{definition}
\newtheorem{definition}{Definition}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newcommand{\RB}{\textsf{RB}\xspace}
\newcommand{\res}{\mathsf{res}}
\newcommand{\ARB}{\textsf{ARB}\xspace}
\newcommand{\DL}{\textsf{DL}\xspace}
\newcommand{\APPEND}{\textsf{APPEND}}
\newcommand{\PROVE}{\textsf{PROVE}}
\newcommand{\PROVEtrace}{\textsf{prove}}
\newcommand{\READ}{\textsf{READ}}
\newcommand{\ABbroadcast}{\textsf{AB-broadcast}}
\newcommand{\ABdeliver}{\textsf{AB-deliver}}
\newcommand{\RBcast}{\textsf{RB-cast}}
\newcommand{\RBreceived}{\textsf{RB-received}}
\newcommand{\ordered}{\textsf{ordered}}
\newcommand{\Winners}{\mathsf{Winners}}
\newcommand{\Messages}{\mathsf{Messages}}
\newcommand{\ABlisten}{\textsf{AB-listen}}
\newcommand{\SHARE}{\mathsf{SHARE}}
\newcommand{\COMBINE}{\mathsf{COMBINE}}
\newcommand{\VERIFY}{\mathsf{VERIFY}}
\newcommand{\delivered}{\mathsf{delivered}}
\newcommand{\received}{\mathsf{received}}
\newcommand{\prop}{\mathsf{prop}}
\newcommand{\resolved}{\mathsf{resolved}}
\newcommand{\current}{\mathsf{current}}
\newcommand{\Seq}{\mathsf{Seq}}
\crefname{theorem}{Theorem}{Theorems}
\crefname{lemma}{Lemma}{Lemmas}
\crefname{definition}{Definition}{Definitions}
\crefname{algorithm}{Algorithm}{Algorithms}
% Code exécuté par tout processus p_i
\begin{document}
\section{Model}
We consider a static set of $n$ processes with known identities, communicating by reliable point-to-point channels, in a complete graph. Messages are uniquely identifiable.
\paragraph{Synchrony.} The network is asynchronous. Processes may crash; at most $f$ crashes occur.
\paragraph{Communication.} Processes can exchange through a Reliable Broadcast (\RB) primitive (defined below) which's invoked with the functions \RBcast$(m)$ and \RBreceived$(m)$. There exists a shared object called DenyList (\DL) (defined below) that is interfaced with the functions \APPEND$(x)$, \PROVE$(x)$ and \READ$()$.
\paragraph{Notation.} Let $\Pi$ be the finite set of process identifiers and let $n \triangleq |\Pi|$. Two authorization subsets are $\Pi_M \subseteq \Pi$ (processes allowed to issue \APPEND) and $\Pi_V \subseteq \Pi$ (processes allowed to issue \PROVE). Indices $i,j \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 round $r \in \mathcal{R}$, define $\Winners_r \triangleq \{\, j \in \Pi \mid (j,\PROVEtrace(r)) \prec \APPEND(r) \,\}$, i.e., the set of processes whose $\PROVE(r)$ appears before the first $\APPEND(r)$ in the \DL{} linearization.
We denoted by $\PROVE^{(j)}(r)$ or $\APPEND^{(j)}(r)$ the operation $\PROVE(r)$ or $\APPEND(r)$ invoked by process $j$.
% ------------------------------------------------------------------------------
\section{Primitives}
\subsection{Reliable Broadcast (RB)}
\RB provides the following properties in the model.
\begin{itemize}[leftmargin=*]
\item \textbf{Integrity}: Every message received was previously sent. $\forall p_i:\ \RBreceived_i(m) \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}
\subsection{DenyList (DL)}
We assume a synchronous DenyList (\DL) object with the following properties.
The DenyList object type supports three operations: $\APPEND$, $\PROVE$, and $\READ$. These operations appear as if executed in a sequence $\Seq$ such that:
\begin{itemize}
\item \textbf{Termination.} A $\PROVE$, an $\APPEND$, or a $\READ$ operation invoked by a correct process always returns.
\item \textbf{APPEND Validity.} The invocation of $\APPEND(x)$ by a process $p$ is valid if:
\begin{itemize}
\item $p \in \Pi_M \subseteq \Pi$; \textbf{and}
\item $x \in S$, where $S$ is a predefined set.
\end{itemize}
Otherwise, the operation is invalid.
\item \textbf{PROVE Validity.} If the invocation of a $op = \PROVE(x)$ by a correct process $p$ is not valid, then:
\begin{itemize}
\item $p \not\in \Pi_V \subseteq \Pi$; \textbf{or}
\item A valid $\APPEND(x)$ appears before $op$ in $\Seq$.
\end{itemize}
Otherwise, the operation is valid.
\item \textbf{PROVE Anti-Flickering.} If the invocation of a operation $op = \PROVE(x)$ by a correct process $p \in \Pi_V$ is invalid, then any $\PROVE(x)$ operation that appears after $op$ in $\Seq$ is invalid.
\item \textbf{READ Validity.} The invocation of $op = \READ()$ by a process $p \in \pi_V$ returns the list of valid invocations of $\PROVE$ that appears before $op$ in $\Seq$ along with the names of the processes that invoked each operation.
\item \textbf{Anonymity.} Let us assume the process $p$ invokes a $\PROVE(v)$ operation. If the process $p'$ invokes a $\READ()$ operation, then $p'$ cannot learn the value $v$ unless $p$ leaks additional information.
\end{itemize}
% ------------------------------------------------------------------------------
\section{Target Abstraction: Atomic Reliable Broadcast (ARB)}
Processes export \ABbroadcast$(m)$ and \ABdeliver$(m)$. \ARB requires total order:
\begin{equation*}
\forall m_1,m_2,\ \forall p_i,p_j:\ \ \ABdeliver_i(m_1) < \ABdeliver_i(m_2) \Rightarrow \ABdeliver_j(m_1) < \ABdeliver_j(m_2),
\end{equation*}
plus Integrity/No-duplicates/Validity (inherited from \RB and the construction).
\section{ARB over RB and DL}
% ------------------------------------------------------------------------------
\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$ iff $H$ contains an operation $\APPEND(r)$.
Equivalently, there exists a time after which every $\PROVE(r)$ is invalid in $H$.
\end{definition}
\subsubsection{Variables}
Each process $p_i$ maintains:
%on met toutes les variables locales ici
\begin{algorithmic}
\State $\received \gets \emptyset$ \Comment{Messages received via \RB but not yet delivered}
\State $\delivered \gets \emptyset$ \Comment{Messages already delivered}
\State $\prop[r][j] \gets \bot,\ \forall r,j$ \Comment{Proposal from process $j$ for round $r$}
\State $\current \gets 0$
\end{algorithmic}
\paragraph{DenyList.} The \DL is initialized empty. We assume $\Pi_M = \Pi_V = \Pi$ (all processes can invoke \APPEND and \PROVE).
\subsubsection{Handlers and Procedures}
\renewcommand{\algletter}{A}
\begin{algorithm}[H]
\caption{\RB handler (at process $p_i$)}\label{alg:rb-handler}
\begin{algorithmic}[1]
\Function{RBreceived}{$S, r, j$}
% \State \textbf{on} $\RBreceived(S, r, j)$ \textbf{do}
\State $\received \leftarrow \received \cup \{S\}$
\State $\prop[r][j] \leftarrow S$ \Comment{Record sender $j$'s proposal $S$ for round $r$}
\EndFunction
\end{algorithmic}
\end{algorithm}
% \paragraph{} An \ABbroadcast$(m)$ chooses the next open round from the \DL view, proposes all pending messages together with the new $m$, disseminates this proposal via \RB, then executes $\PROVE(r)$ followed by $\APPEND(r)$ to freeze the winners of the round. The loop polls \DL until (i) some winner’s proposal includes $m$ in a \emph{closed} round and (ii) all winners' proposals for closed rounds are known locally, ensuring eventual inclusion and delivery.
\renewcommand{\algletter}{B}
\begin{algorithm}[H]
\caption{\ABbroadcast$(m)$ (at process $p_i$)}\label{alg:ab-bcast}
\begin{algorithmic}[1]
\Function{ABbroadcast}{$m$}
\State $P \leftarrow \READ()$ \Comment{Fetch latest \DL state to learn recent $\PROVE$ operations}
\State $r_{max} \leftarrow \max(\{ r' : \exists j,\ (j,\PROVE(r')) \in P \})$ \Comment{Pick current open round}
\State $S \leftarrow (\received \setminus \delivered) \cup \{m\}$ \Comment{Propose all pending messages plus the new $m$}
\vspace{1em}
\For{\textbf{each}\ $r \in \{r_{max}, r_{max}+1, \cdots \}$}
\State $\RBcast(S, r, i)$; $\PROVE(r)$; $\APPEND(r)$;
\State $P \leftarrow \READ()$ \Comment{Refresh local view of \DL}
\If{($\big((i, \PROVEtrace(r)) \in P\ \vee\ (\exists j, r': (j, \PROVEtrace(r')) \in P \wedge \ m \in \prop[r'][j]))$)}
\State \textbf{break} \Comment{Exit loop once $m$ is included in some closed round}
\EndIf
\EndFor
\EndFunction
\end{algorithmic}
\end{algorithm}
\renewcommand{\algletter}{C}
\begin{algorithm}[H]
\caption{\ABdeliver() at process $p_i$}\label{alg:delivery}
\begin{algorithmic}[1]
\Function{ABdeliver}{}
\State $r \gets \current$
\State $P \gets \READ()$
\If{$\forall j : (j, \PROVEtrace(r)) \not\in P$}
\State \Return $\bot$
\EndIf
\State $\APPEND(r)$; $P \gets \READ()$
\State $W_r \gets \{ j : (j, \PROVEtrace(r)) \in P \}$
\If{$\exists j \in W_r,\ \prop[r][j] = \bot$}
\State \Return $\bot$
\EndIf
\State $M_r \gets \bigcup_{j \in W_r} \prop[r][j]$
\State $m \gets \ordered(M_r \setminus \delivered)[0]$ \Comment{Set $m$ as the smaller message not already delivered}
\State $\delivered \leftarrow \delivered \cup \{m\}$
\If{$M_r \setminus \delivered = \emptyset$} \Comment{Check if all messages from round $r$ have been delivered}
\State $\current \leftarrow \current + 1$
\EndIf
\State \textbf{return} $m$
\EndFunction
\end{algorithmic}
\end{algorithm}
% ------------------------------------------------------------------------------
\subsection{Correctness}
\begin{lemma}[Stable round closure]\label{lem:closure-stable}
If a round $r$ is closed, then there exists a linearization point $t_0$ of $\APPEND(r)$ in the \DL, and from that point on, no $\PROVE(r)$ can be valid.
Once closed, a round never becomes open again.
\end{lemma}
\begin{proof}
By \Cref{def:closed-round}, some $\APPEND(r)$ occurs in the linearization $H$. \\
$H$ is a total order of operations, the set of $\APPEND(r)$ operations is totally ordered, and hence there exists a smallest $\APPEND(r)$ in $H$. We denote this operation $\APPEND^{(\star)}(r)$ and $t_0$ its linearization point. \\
By the validity property of \DL, a $\PROVE(r)$ is valid iff $\PROVE(r) \prec \APPEND^{(\star)}(r)$. Thus, after $t_0$, no $\PROVE(r)$ can be valid. \\
$H$ is a immutable grow-only history, and hence once closed, a round never becomes open again. \\
Hence there exists a linearization point $t_0$ of $\APPEND(r)$ in the \DL, and from that point on, no $\PROVE(r)$ can be valid and the closure is stable.
\end{proof}
\begin{definition}[First APPEND]\label{def:first-append}
Given a \DL{} linearization $H$, for any closed round $r\in\mathcal{R}$, we denote by $\APPEND^{(\star)}(r)$ the earliest $\APPEND(r)$ in $H$.
\end{definition}
\begin{lemma}[Across rounds]\label{lem:across}
If there exists a $r$ such that $r$ is closed, $\forall r'$ such that $r' < r$, r' is also closed.
\end{lemma}
\begin{proof}
\emph{Base.} For a closed round $k=0$, the set $\{k' \in \mathcal{R},\ k' < k\}$ is empty, hence the lemma is true.
\emph{Induction.} Assume the lemma is true for round $k\geq 0$, we prove it for round $k+1$.
\smallskip
Assume $k+1$ is closed and let $\APPEND^{(\star)}(k+1)$ be the earliest $\APPEND(k+1)$ in the DL linearization $H$.
By Lemma 1, after an $\APPEND(k)$ is in $H$, any later $\PROVE(k)$ is rejected also, a process’s program order is preserved in $H$.
There are two possibilities for where $\APPEND^{(\star)}(k+1)$ is invoked.
\begin{itemize}
\item \textbf{Case (B6) :}
Some process $p^\star$ executes the loop (lines B5–B11) and invokes $\APPEND^{(\star)}(k+1)$ at line B6.
Immediately before line B6, line B5 sets $r\leftarrow r+1$, so the previous loop iteration (if any) targeted $k$. We consider two sub-cases.
\begin{itemize}
\item \emph{(i) $p^\star$ is not in its first loop iteration.}
In the previous iteration, $p^\star$ executed $\PROVE^{(\star)}(k)$ at B6, followed (in program order) by $\APPEND^{(\star)}(k)$.
If round $k$ wasn't closed when $p^\star$ execute $\PROVE^{(\star)}(k)$ at B9, then the condition at B8 would be true hence the tuple $(p^\star, \PROVEtrace(k))$ should be visible in P which implies that $p^\star$ should leave the loop at round $k$, contradicting the assumption that $p^\star$ is now executing another iteration.
Since the tuple is not visible, the $\PROVE^{(\star)}(k)$ was rejected by the DL which implies by definition an $\APPEND(k)$ already exists in $H$. Thus in this case $k$ is closed.
\item \emph{(ii) $p^\star$ is in its first loop iteration.}
To compute the value $r_{max}$, $p^\star$ must have observed one or many $(\_ , \PROVEtrace(k+1))$ in $P$ at B2/B3, issued by some processes (possibly different from $p^\star$). Let's call $p_1$ the issuer of the first $\PROVE^{(1)}(k+1)$ in the linearization $H$. \\
When $p_1$ executed $P \gets \READ()$ at B2 and compute $r_{max}$ at B3, he observed no tuple $(\_,\PROVEtrace(k+1))$ in $P$ because he's the issuer of the first one. So when $p_1$ executed the loop (B5–B11), he run it for the round $k$, didn't seen any $(1,\PROVEtrace(k))$ in $P$ at B8, and then executed the first $\PROVE^{(1)}(k+1)$ at B6 in a second iteration. \\
If round $k$ wasn't closed when $p_1$ execute $\PROVE^{(1)}(k)$ at B6, then the condition at B8 should be true which implies that $p_1$ sould leave the loop at round $k$, contradicting the assumption that $p_1$ is now executing $\PROVE^{(1)}(r+1)$. In this case $k$ is closed.
\end{itemize}
\item \textbf{Case (C8) :}
Some process invokes $\APPEND(k+1)$ at C8.
Line C8 is guarded by the presence of $\PROVE(\textit{next})$ in $P$ with $\textit{next}=k+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}=k+1$ it implies that he has completed round $k$, which includes closing $k$ at C8 when $\PROVE(k)$ is observed.
Hence $\APPEND^\star(k+1)$ implies a prior $\APPEND(k)$ in $H$, so $k$ is closed.
\end{itemize}
\smallskip
In all cases, $k+1$ closed implie $k$ closed. By induction on $k$, if the lemme is true for a closed $k$ then it is true for a closed $k+1$.
Therefore, the lemma is true for all closed rounds $r$.
\end{proof}
\begin{definition}[Winner Invariant]\label{def:winner-invariant}
For any closed round $r$, define
\[
\Winners_r \triangleq \{ j : \PROVE^{(j)}(r) \prec \APPEND^\star(r) \}
\]
as the unique set of winners of round $r$.
\end{definition}
\begin{lemma}[Invariant view of closure]\label{lem:closure-view}
For any closed round $r$, all correct processes eventually observe the same set of valid tuples $(\_,\PROVEtrace(r))$ in their \DL view.
\end{lemma}
\begin{proof}
Let's take a closed round $r$. By \Cref{def:first-append}, there exists a unique earliest $\APPEND(r)$ in the DL linearization, denoted $\APPEND^\star(r)$.
Consider any correct process $p$ that invokes $\READ()$ after $\APPEND^\star(r)$ in the DL linearization. Since $\APPEND^\star(r)$ invalidates all subsequent $\PROVE(r)$, the set of valid tuples $(\_,\PROVEtrace(r))$ observed by any correct process after $\APPEND^\star(r)$ is fixed and identical across all correct processes.
Therefore, for any closed round $r$, all correct processes eventually observe the same set of valid tuples $(\_,\PROVEtrace(r))$ in their \DL view.
\end{proof}
\begin{lemma}[Well-defined winners]\label{lem:winners}
For any correct process and round $r$, if the process computes $W_r$ at line C9, then :
\begin{itemize}
\item $\Winners_r$ is defined;
\item the computed $W_r$ is exactly $\Winners_r$.
\end{itemize}
\end{lemma}
\begin{proof}
Let take a correct process $p_i$ that reach line C9 to compute $W_r$. \\
By program order, $p_i$ must have executed $\APPEND^{(i)}(r)$ at C8 before, which implies by \Cref{def:closed-round} that round $r$ is closed. 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 $(\_,\PROVEtrace(r))$ in their \DL view. Hence, when $p_i$ executes the $\READ()$ at C8 after the $\APPEND^{(i)}(r)$, it observes a set $P$ that includes all valid tuples $(\_,\PROVEtrace(r))$ such that
\[
W_r = \{ j : (j,\PROVEtrace(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)$.
\end{lemma}
\begin{proof}[Proof]
Consider the round $r$ such that some process invokes $\APPEND(r)$. There are two possible cases
\begin{itemize}
\item \textbf{Case (B6) :}
There exists a process $p^\star$ who's the issuer of the earliest $\APPEND^{(\star)}(r)$ in the DL linearization $H$. By program order, $p^\star$ must have previously invoked $\PROVE^{(\star)}(r)$ before invoking $\APPEND^{(\star)}(r)$ at B6. 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 (C8) :}
There exist a process $p^\star$ invokes $\APPEND^{(\star)}(r)$ at C8. Line C8 is guarded by the condition at C5, which ensures that $p$ observed some $(\_,\PROVEtrace(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 round, if $\Winners_r$ is defined, then $\Winners_r \neq \emptyset$.
\end{lemma}
\begin{proof}[Proof]
If $\Winners_r$ is defined, then by \Cref{def:winner-invariant}, round $r$ is closed. By \Cref{def:closed-round}, some $\APPEND(r)$ occurs in the DL linearization. \\
By \Cref{lem:append-prove}, at least a process must have invoked a valid $\PROVE(r)$ before $\APPEND^{(\star)}(r)$. Hence, there exists at least one $j$ such that $\{j: \PROVE^{(j)}(r) \prec \APPEND^\star(r)\}$, so $\Winners_r \neq \emptyset$.
\end{proof}
\begin{lemma}[Winners must propose]\label{lem:winners-propose}
For any closed round $r$, $\forall j \in \Winners_r$, process $j$ must have invoked a $\RBcast(S^{(j)}, r, j)$
\end{lemma}
\begin{proof}[Proof]
Fix a closed round $r$. By \Cref{def:winner-invariant}, for any $j \in \Winners_r$, there exist a valid $\PROVE^{(j)}(r)$ such that $\PROVE^{(j)}(r) \prec \APPEND^\star(r)$ in the DL linearization. By program order, if $j$ invoked a valid $\PROVE^{(j)}(r)$ at line B6 he must have invoked $\RBcast(S^{(j)}, r, j)$ directly before.
\end{proof}
\begin{definition}[Messages invariant]\label{def:messages-invariant}
For any closed round $r$ and any correct process $p_i$ such that $\nexists j \in \Winners_r : prop^{[i)}[r][j] = \bot$, define
\[
\Messages_r \triangleq \bigcup_{j\in\Winners_r} \prop^{(i)}[r][j]
\]
as the unique set of messages proposed by the winners of round $r$.
\end{definition}
\begin{lemma}[Non-empty winners proposal]\label{lem:winner-propose-nonbot}
For any closed round $r$, $\forall j \in \Winners_r$, for any correct process $p_i$, eventually $\prop^{(i)}[r][j] \neq \bot$.
\end{lemma}
\begin{proof}[Proof]
Fix a closed round $r$. By \Cref{def:winner-invariant}, for any $j \in \Winners_r$, there exist a valid $\PROVE^{(j)}(r)$ such that $\PROVE^{(j)}(r) \prec \APPEND^\star(r)$ in the DL linearization. By \Cref{lem:winners-propose}, $j$ must have invoked $\RBcast(S^{(j)}, r, j)$.
Let take a process $p_i$, by \RB \emph{Validity}, every correct process eventually receives $j$'s \RB message for round $r$, which sets $\prop[r][j]$ to a non-$\bot$ value at line A3.
\end{proof}
\begin{lemma}[Eventual proposal closure]\label{lem:eventual-closure}
If a correct process $p_i$ define $M_r$ at line C13, 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 C13. By \Cref{lem:winners}, $p_i$ computes the unique winner set $\Winners_r$.
By \Cref{lem:nonempty}, $\Winners_r \neq \emptyset$. The instruction at line C13 where $p_i$ computes $M_r$ is guarded by the condition at C10, which ensures that $p_i$ has received all \RB messages from every winner $j \in \Winners_r$. Hence, when $p_i$ computes $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$.
\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)$.
\end{lemma}
\begin{proof}[Proof]
By program order, any process $p_i$ invokes $\RBcast(S, r, i)$ at line B6 must be in the loop B5–B11. No matter the number of iterations of the loop, line B5 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$.
\end{proof}
\begin{lemma}[Proposal convergence]\label{lem:convergence}
For any round $r$, for any correct processes $p_i$ that define $M_r$ at line C13, we have
\[
M_r^{(i)} = \Messages_r
\]
\end{lemma}
\begin{proof}[Proof]
Let take a correct process $p_i$ that define $M_r$ at line C13. That implies that $p_i$ has defined $W_r$ at line C9. 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
\[
M_r^{(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{with}\quad m\in S.
\]
\end{lemma}
\begin{proof}
Fix a correct process $p_i$ that invokes $\ABbroadcast(m)$ and eventually exits the loop (B5–B11) at some round $r$. There are two possible cases.
\begin{itemize}
\item \textbf{Case 1:} $p_i$ exits the loop because $(i, \PROVEtrace(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 B6 before invoking $\PROVE^{(i)}(r)$ at B7. By line B4, $m \in S$. Hence there exist a closed round $r$ and a correct process $j=i\in\Winners_r$ such that $j$ invokes $\RBcast(S, r, j)$ with $m\in S$.
\item \textbf{Case 2:} $p_i$ exits the loop because $\exists j, r': (j, \PROVEtrace(r')) \in P \wedge m \in \prop[r'][j]$. In this case, by \Cref{lem:winners-propose} and \Cref{lem:unique-proposal} $j$ must have invoked a unique $\RBcast(S, r', j)$. Which set $\prop^{(i)}[r'][j] = S$ 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.
\]
\end{proof}
\begin{lemma}[Broadcast Termination]\label{lem:bcast-termination}
If a correct process invokes $\ABbroadcast(m)$, then he eventually exit the function and returns.
\end{lemma}
\begin{proof}[Proof]
Let a correct process $p_i$ that invokes $\ABbroadcast(m)$. The lemma is true if $\exists r_1$ such that $r_1 \geq r_{max}$ and if $(i, \PROVEtrace(r_1)) \in P$; or if $\exists r_2$ such that $r_2 \geq r_{max}$ and if $\exists j: (j, \PROVEtrace(r_2)) \in P \wedge m \in \prop[r_2][j]$ (like guarded at B8).
Let admit 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 B6 with $m \in S$ (line B4).\\
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 a correct 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$ execute \Cref{alg:rb-handler} and do $\received \leftarrow \received \cup \{S\}$ with $m \in S$ (line A2).
For the first invocation of $\ABbroadcast(\_)$ by $p_k$ after the execution of \Cref{alg:rb-handler}, $p_k$ must include $m$ in his proposal $S$ at line B4 (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:winner-propose-nonbot}, 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 cover the condition $(i, \PROVEtrace(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)$.
\end{proof}
\begin{lemma}[Validity]\label{lem:validity}
If a correct process $p$ invokes $\ABbroadcast(m)$, then every correct process that invokes a infinitely often times $\ABdeliver()$ eventually delivers $m$.
\end{lemma}
\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.
\]
By \Cref{lem:eventual-closure}, when $p_q$ computes $M_r$ at line C13, $\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
\[
M_r = \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 any correct process that defines it includes $m$. At each invocation of $\ABdeliver()$ which deliver $m'$, $m'$ is add to $\delivered$ until $M_r \subseteq \delivered$. Once this append we're assured that there exist an invocation of $\ABdeliver()$ which return $m$. Hence $m$ is well delivered.
\end{proof}
\begin{lemma}[No duplication]\label{lem:no-duplication}
No correct process delivers the same message more than once.
\end{lemma}
\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)}()$ occur, by program order and because it reach line C19 to return $m$, the process must have add $m$ to $\delivered$. Hence when $\ABdeliver^{(B)}()$ reach line C14 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 deliver $m$ can't occur.
\end{proof}
\begin{lemma}[Total order]\label{lem:total-order}
For any two messages $m_1$ and $m_2$ delivered by correct processes, if a correct process $p_i$ delivers $m_1$ before $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}
Consider any correct process that delivers both $m_1$ and $m_2$. By \Cref{lem:validity}, there exist 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(S_2, r'_2, k_2)\quad\text{with}\quad m_2\in S_2.
\]
Let consider three 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 $\ABdeliver()$ that returns $m_2$. 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 C13 computes the same set of messages $\Messages_{r_1}$. By line C14 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 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 two messages $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$ 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.
\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.
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$.
This gives the usual Validity property of \ARB.
Concerning Integrity and No-duplicates, the construction only ever delivers messages that have been obtained from the underlying \RB primitive.
By the Integrity property of \RB, every such message was previously \RBcast by some process, so no spurious messages are delivered.
In addition, \Cref{lem:no-duplication} states that no correct process delivers the same message more than once.
Together, these arguments yield the Integrity and No-duplicates properties required by \ARB.
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.
\end{proof}
\subsection{Reciprocity}
% ------------------------------------------------------------------------------
So far, we assumed the existence of a synchronous DenyList (\DL) object and
showed how to upgrade a Reliable Broadcast (\RB) primitive into FIFO Atomic
Reliable Broadcast (\ARB). We now briefly argue that, conversely, an \ARB{}
primitive is strong enough to implement a synchronous \DL object (ignoring the
anonymity property).
\paragraph{DenyList as a deterministic state machine.}
Without anonymity, the \DL specification defines a
deterministic abstract object: given a sequence $\Seq$ of operations
$\APPEND(x)$, $\PROVE(x)$, and $\READ()$, the resulting sequence of return
values and the evolution of the abstract state (set of appended elements,
history of operations) are uniquely determined.
\paragraph{State machine replication over \ARB.}
Assume a system that exports a FIFO-\ARB primitive with the guarantees that if a correct process invokes $\ABbroadcast(m)$, then every correct process eventually $\ABdeliver(m)$ and the invocation eventually returns.
Following the classical \emph{state machine replication} approach
such as described in Schneider~\cite{Schneider90}, we can implement a fault-tolerant service by ensuring the following properties:
\begin{quote}
\textbf{Agreement.} Every nonfaulty state machine replica receives every request. \\
\textbf{Order.} Every nonfaulty state machine replica processes the requests it receives in
the same relative order.
\end{quote}
Which are cover by our FIFO-\ARB specification.
\paragraph{Correctness.}
\begin{theorem}[From \ARB to synchronous \DL]\label{thm:arb-to-dl}
In an asynchronous message-passing system with crash failures, assume a
FIFO Atomic Reliable Broadcast primitive with Integrity, No-duplicates,
Validity, and the liveness of $\ABbroadcast$. Then, ignoring anonymity, there
exists an implementation of a synchronous DenyList object that satisfies the
Termination, Validity, and Anti-flickering properties.
\end{theorem}
\begin{proof}
Because the \DL object is deterministic, all correct processes see the same
sequence of operations and compute the same sequence of states and return
values. We obtain:
\begin{itemize}[leftmargin=*]
\item \textbf{Termination.} The liveness of \ARB ensures that each
$\ABbroadcast$ invocation by a correct process eventually returns, and
the corresponding operation is eventually delivered and applied at all
correct processes. Thus every $\APPEND$, $\PROVE$, and $\READ$ operation invoked by a correct process
eventually returns.
\item \textbf{APPEND/PROVE/READ Validity.} The local code that forms
\ABbroadcast requests can achieve the same preconditions as in the
abstract \DL specification (e.g., $p\in\Pi_M$, $x\in S$ for
$\APPEND(x)$). Once an operation is delivered, its effect and return
value are exactly those of the sequential \DL specification applied in
the common order.
\item \textbf{PROVE Anti-Flickering.} In the sequential \DL specification,
once an element $x$ has been appended, all subsequent $\PROVE(x)$ are
invalid forever. Since all replicas apply operations in the same order,
this property holds in every execution of the replicated implementation:
after the first linearization point of $\APPEND(x)$, no later
$\PROVE(x)$ can return ``valid'' at any correct process.
\end{itemize}
Formally, we can describe the \DL object with the state machine approach for
crash-fault, asynchronous message-passing systems with a total order broadcast
layer~\cite{Schneider90}.
\end{proof}
\subsubsection{Example executions}
\begin{figure}[H]
\centering
\resizebox{0.4\textwidth}{!}{
\input{diagrams/nonBFT_behaviour.tex}
}
\caption{Example execution of the ARB algorithm in a non-BFT setting}
\end{figure}
\begin{figure}
\centering
\resizebox{0.4\textwidth}{!}{
\input{diagrams/BFT_behaviour.tex}
}
\caption{Example execution of the ARB algorithm with a byzantine process}
\end{figure}
\section{BFT-ARB over RB and DL}
\subsection{Model extension}
We consider a static set of $n$ processes with known identities, communicating by reliable point-to-point channels, in a complete graph. Messages are uniquely identifiable.
\paragraph{Synchrony.} The network is asynchronous. Processes may crash or be byzantine; at most $f = \frac{n}{2} - 1$ processes can be faulty.
\paragraph{Communication.} Processes can exchange through a Reliable Broadcast (\RB) primitive (defined below) which's invoked with the functions \RBcast$(m)$ and \RBreceived$(m)$. There exists a shared object called DenyList (\DL) (defined below) that is interfaced with the functions \APPEND$(x)$, \PROVE$(x)$ and \READ$()$.
\paragraph{Byzantine behaviour}
A process exhibits Byzantine behavior if it deviates arbitrarily from the specified algorithm. This includes, but is not limited to, the following actions:
\begin{itemize}
\item Invoking primitives (\RBcast, \APPEND, \PROVE, etc.) with invalid or maliciously crafted inputs.
\item Colluding with other Byzantine processes to manipulate the system's state or violate its guarantees.
\item Delaying or accelerating message delivery to specific nodes to disrupt the expected timing of operations.
\item Withholding messages or responses to create inconsistencies in the system's state.
\end{itemize}
Byzantine processes are constrained by the following:
\begin{itemize}
\item They cannot forge valid cryptographic signatures or threshold shares without the corresponding private keys.
\item They cannot violate the termination, validity, or anti-flickering properties of the \DL{} object.
\item They cannot break the integrity, no-duplicates, or validity properties of the \RB{} primitive.
\end{itemize}
\paragraph{Notation.} Let $\Pi$ be the finite set of process identifiers and let $n \triangleq |\Pi|$. Two authorization subsets are $M \subseteq \Pi$ (processes allowed to issue \APPEND) and $V \subseteq \Pi$ (processes allowed to issue \PROVE). Indices $i,j \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 round $r \in \mathcal{R}$, define $\Winners_r \triangleq \{\, j \in \Pi \mid (j,\PROVEtrace(r)) \prec \APPEND(r) \,\}$, i.e., the set of processes whose $\PROVE(r)$ appears before the first $\APPEND(r)$ in the \DL{} linearization.
We denoted by $\PROVE^{(j)}(r)$ or $\APPEND^{(j)}(r)$ the operation $\PROVE(r)$ or $\APPEND(r)$ invoked by process $j$.
% ------------------------------------------------------------------------------
\subsection{Primitives}
\subsubsection{BFT DenyList}
We consider a \DL object that satisfies the following properties despite the presence of up to $f$ byzantine processes:
\begin{itemize}
\item \textbf{Termination.} Every operation $\APPEND(x)$, $\PROVE(x)$, and $\READ()$ invoked by a correct process eventually returns.
\item \textbf{APPEND/PROVE/READ Validity.} The preconditions for invoking $\APPEND(x)$, $\PROVE(x)$, and $\READ()$ are respected (cf. \#2.2). The return values of these operations conform to the sequential specification of the \DL object.
\item \textbf{APPEND Justification.} For any element $x$, if an operation $\APPEND(x)$ invoked by a correct process completes successfully, then there exists at least one valid $\PROVE(x)$ operation that that precedes this $\APPEND(x)$ in the \DL linearization.
\item \textbf{PROVE Anti-Flickering.} Once an element $x$ has been appended to the \DL by any process, all subsequent invocations of $\PROVE(x)$ by any process return ``invalid''.
\end{itemize}
\subsubsection{t-out-of-n Threshold Random Number Generator}
We consider a function that with t out of n shares any process can reconstruct a deterministic random number. The function is defined as follows:
\begin{itemize}
\item \textbf{$t$-reconstruction.} Given any subset $S$ of at least $t$ valid shares derived from the same value $r$, there exists a unique value $\sigma$ consistent with all shares in~$S$, and $\sigma$ can be efficiently reconstructed from~$S$.
\item \textbf{$(t-1)$-non-reconstructibility.} Given any subset $S$ of at most $t-1$ valid shares derived from the same value $r$, there exist two distinct values $\sigma$ and $\sigma'$ that are both consistent with all shares in~$S$. In particular, no algorithm that only sees the shares in $S$ can always distinguish whether the underlying value is $\sigma$ or $\sigma'$. \item \textbf{Per-process non-equivocation.} For any process $p$ and value $r$, there is at most one valid share that $p$ can derive from $r$. Formally, if $\sigma$ and $\sigma'$ are two valid shares output by process $p$ from the same value $r$, then $\sigma = \sigma'$. In particular, a single process cannot emit two different valid shares for the same underlying value~$r$.
\end{itemize}
\paragraph{Interface.}
For algorithmic purposes, we model the $t$-out-of-$n$ threshold random number generator
as providing the following interface to each process $p \in \Pi$.
\begin{itemize}
\item{$\mathsf{SHARE}_{p_i}(r)$:} On input a value $r$, run locally by process $p_i$, returns a valid share $\sigma_r^i$. By per-process share uniqueness, for any fixed $p_i$ and $r$ the value $\sigma_r^i$ is uniquely determined.
\item{$\mathsf{COMBINE}(S)$:} On a set $S$ of at least $t$ pairs $(p_i,\sigma_r^i)$, returns the reconstructed value $\sigma_r$. By $t$-reconstruction, this value is well defined and independent of the particular set $S$ of valid shares of size at least $t$.
\item{$\mathsf{VERIFY}(r,\sigma_{r'})$:} On input a value $r$ and a candidate value $\sigma_{r'}$, returns \textsf{true} if and only if there exists a set $S$ of at least $t$ valid shares for $r$ such that $\mathsf{Combine}(r,S) = \sigma_{r'}$, and \textsf{false} otherwise. We say that $\sigma_{r'}$ is \emph{valid for $r$} if $\mathsf{Verify}(r,\sigma_{r'})=\textsf{true}$.
\end{itemize}
\subsection{Algorithm}
\subsubsection{Variables}
Each process $p_i$ maintains the following local variables:
\begin{algorithmic}
\State $\current \gets 0$
\State $\received \gets \emptyset$
\State $\delivered \gets \emptyset$
\State $\prop[r][j] \gets \bot, \forall r, j$
\State $X_r \gets \bot, \forall r$
\State $\resolved[r] \gets \bot, \forall r$
\end{algorithmic}
\renewcommand{\algletter}{D}
\begin{algorithm}[H]
\caption{\ABbroadcast}\label{alg:ab-cast}
\begin{algorithmic}[1]
\Function{ABcast}{$m$}
\State $S \gets (\received \setminus \delivered) \cup \{m\}$
\State $\RBcast(prop, S, r, i)$
\State \textbf{wait until} $|X_r| \geq f+1$
\State $\sigma_r \gets \COMBINE(X_r)$
\State $\PROVE(\sigma_r); \APPEND(\sigma_r);$
\State $\RBcast(submit, S, \sigma_r, r, i)$
\EndFunction
\end{algorithmic}
\end{algorithm}
\renewcommand{\algletter}{E}
\begin{algorithm}[H]
\caption{\ABdeliver}\label{alg:ab-deliver}
\begin{algorithmic}[1]
\Function{$\ABdeliver$}{}
\State $r \gets \current; \sigma_r \gets \resolved[r];$
\If{$\sigma_r == \bot$}
\State \Return $\bot$
\EndIf
\State $P \gets \READ()$
\If{$\forall j : (j,prove(\sigma_r)) \not\in P$}
\State \Return $\bot$
\EndIf
\State $\APPEND(\sigma_r); P \gets \READ();$
\State $W_r \gets \{j : (j, \PROVEtrace(\sigma_r)) \in P\}$
\If{$\exists j \in W_r : \prop[r][j] == \bot$}
\State \Return $\bot$
\EndIf
\State $M_r \gets \bigcup_{j \in W_r} \prop[r][j];$
\State $m \gets \ordered(M_r)[0]$
\State $\delivered \gets \delivered \cup \{m\};$
\If{$M_r \setminus \delivered = \emptyset$}
\State $\current \gets \current + 1;$
\EndIf
\State \Return $m$
\EndFunction
\end{algorithmic}
\end{algorithm}
\renewcommand{\algletter}{F}
\begin{algorithm}[H]
\caption{RBreceived handler}\label{alg:rb-handler}
\begin{algorithmic}[1]
\Function{RBrcvd}{$prop, S_j, r_j, j$}
\If{$r_j \geq r$}
\State $\prop[r_j][j] = S_j$
\State $\sigma^i_{r_j} \gets \SHARE(r_j)$
\State $send_j(r, \sigma^i_{r_j})$
\EndIf
\EndFunction
\end{algorithmic}
\end{algorithm}
\renewcommand{\algletter}{G}
\begin{algorithm}[H]
\caption{RBreceived handler}\label{alg:rb-handler-2}
\begin{algorithmic}[1]
\Function{RBrcvd}{$submit, S_j, \sigma_{r_j}, r_j, j$}
\If{$\VERIFY(r_j, \sigma_{r_j})$}
\State $\resolved[r_j] \gets \sigma_{r_j}$
\EndIf
\EndFunction
\end{algorithmic}
\end{algorithm}
\renewcommand{\algletter}{H}
\begin{algorithm}[H]
\caption{Share received handler}\label{alg:share-handler}
\begin{algorithmic}[1]
\Function{received}{$r_j, \sigma^j_{r_j}, j$}
\If{$r_j == r$}
\State $X_r \gets X_r \cup \sigma^j_{r}$
\EndIf
\EndFunction
\end{algorithmic}
\end{algorithm}
\subsection{Example execution}
\begin{figure}[H]
\centering
\input{diagrams/classic_seq.tex}
\caption{Expected Executions of P1 willing to send a message at round r}
\end{figure}
\section{Implementation of BFT-DenyList and Threshold Cryptography}
\subsection{DenyList}
\paragraph{BFT-DenyList}
In our algorithm we use multiple DenyList as follows:
\begin{itemize}
\item Let $\mathcal{DL} = \{DL_1, \dots, DL_k\}$ be the set of DenyList used by the algorithm.
\item We set $k = \binom{n}{f}$.
\item For each $i \in \{1,\dots,k\}$, let $M_i$ be the set of moderators associated with $DL_i$ according to the DenyList definition, so that $|M_i| = n-f$.
\item Let $\mathcal{M} = \{M_1, \dots, M_k\}$. We require that the $M_i$ are pairwise distinct:
\[
\forall i,j \in \{1,\dots,k\},\ i \neq j \implies M_i \neq M_j.
\]
\end{itemize}
\begin{lemma}
$\exists M_i \in M : \forall p \in M_i$ $p$ is correct.
\end{lemma}
\begin{proof}
Let consider the set $F$ of faulty processes, with $|F| = f$. We can construct the set $M_i = \Pi \setminus F$ such that $|M_i| = n - |F| = n - f$. By construction, $\forall p \in M_i$ $p$ is correct.
\end{proof}
\begin{lemma}
$\forall M_i \in M, \exists p \in M_i$ such that $p$ is correct.
\end{lemma}
\begin{proof}
$\forall i \in \{1, \dots, k\}, |M_i| = n-f$ with $n \geq 2f+1$. We can say that $|M_i| \geq 2f+1-f = f+1 > f$
\end{proof}
Each process can invoke the following functions :
\begin{itemize}
\item $\READ' : () \rightarrow \mathcal{L}(\mathbb{R} \times \PROVEtrace(\mathbb{R}))$
\item $\APPEND' : \mathbb{R} \rightarrow ()$
\item $\PROVE' : \mathbb{R} \rightarrow \{0, 1\}$
\end{itemize}
Such that :
\begin{algorithm}[H]
\caption{$\READ'() \rightarrow \mathcal{L}(\mathbb{R} \times \PROVEtrace(\mathbb{R}))$}
\begin{algorithmic}
\Function{READ'}{}
\State $j \gets$ the process invoking $\READ'()$
\State $res \gets \emptyset$
\ForAll{$i \in \{1, \dots, k\}$}
\State $res \gets res \cup DL_i.\READ()$
\EndFor
\State \Return $res$
\EndFunction
\end{algorithmic}
\end{algorithm}
\begin{algorithm}[H]
\caption{$\APPEND'(\sigma) \rightarrow ()$}
\begin{algorithmic}
\Function{APPEND'}{$\sigma$}
\State $j \gets$ the process invoking $\APPEND'(\sigma)$
\ForAll{$M_i \in \{M_k \in M : j \in M_k\}$}
\State $DL_i.\APPEND(\sigma)$
\EndFor
\EndFunction
\end{algorithmic}
\end{algorithm}
\begin{algorithm}[H]
\caption{$\PROVE'(\sigma) \rightarrow \{0, 1\}$}
\begin{algorithmic}
\Function{PROVE'}{$\sigma$}
\State $j \gets$ the process invoking $\PROVE'(\sigma)$
\State $flag \gets false$
\ForAll{$i \in \{1, \dots, k\}$}
\State $flag \gets flag$ OR $DL_i.\PROVE(\sigma)$
\EndFor
\State \Return $flag$
\EndFunction
\end{algorithmic}
\end{algorithm}
\subsection{Threshold Cryptography}
We are using the Boneh-Lynn-Shacham scheme as cryptography primitive to our threshold signature scheme.
With :
\begin{itemize}
\item $G : \mathbb{R} \rightarrow \mathbb{R} \times \mathbb{R} $
\item $S : \mathbb{R} \times \mathcal{R} \rightarrow \mathbb{R} $
\item $V : \mathbb{R} \times \mathcal{R} \times \mathbb{R} \rightarrow \{0, 1\} $
\end{itemize}
Such that :
\begin{itemize}
\item $G(x) \rightarrow (pk, sk)$ : where $x$ is a random value such that $\nexists x_1, x_2: x_1 \neq x_2, G(x_1) = G(x_2)$
\item $S(sk, m) \rightarrow \sigma_m$
\item $V(pk, m_1, \sigma_{m_2}) \rightarrow k$ : with $k = 1$ iff $m_1 == m_2$ and $\exists x \in \mathbb{R}$ such that $G(x) \rightarrow (pk, sk)$; otherwise $k = 0$
\end{itemize}
\paragraph{threshold Scheme}
In our algorithm we are only using the following functions :
\begin{itemize}
\item $G' : \mathbb{R} \times \mathbb{N} \times \mathbb{N} \rightarrow \mathbb{R} \times (\mathbb{R} \times \mathbb{R})^n$ : with $n \triangleq |\Pi|$
\item $S' : \mathbb{R} \times \mathcal{R} \rightarrow \mathbb{R}$
\item $C' : \mathbb{R}^n \times \mathcal{R} \times \mathbb{R} \times \mathbb{R}^t \rightarrow \{\mathbb{R}, \bot\}$ : with $t \leq n$
\item $V' : \mathbb{R} \times \mathcal{R} \times \mathbb{R} \rightarrow \{0, 1\}$
\end{itemize}
Such that :
\begin{itemize}
\item $G'(x, n, t) \rightarrow (pk, pk_1, sk_1, \dots, pk_n, sk_n)$ : let define $pkc = {pk_1, \dots, pk_n}$
\item $S'(sk_i, m) \rightarrow \sigma_m^i$
\item $C'(pkc, m_1, J, \{\sigma_{m_2}^j\}_{j \in J}) \rightarrow \sigma$ : with $J \subseteq \Pi$; and $\sigma = \sigma_{m_1}$ iff $|J| \geq t, \forall j \in J: V(pk_j, m_1, \sigma_{m_2}^j) == 1$; otherwise $\sigma = \bot$.
\item $V'(pk, m_1, \sigma_{m_2}) \rightarrow V(pk, m_1, \sigma_{m_2})$
\end{itemize}
\bibliographystyle{plain}
\begin{thebibliography}{9}
% (left intentionally blank)
\bibitem{Schneider90}
Fred B.~Schneider.
\newblock Implementing fault-tolerant services using the state machine
approach: a tutorial.
\newblock {\em ACM Computing Surveys}, 22(4):299--319, 1990.
\end{thebibliography}
\end{document}