Redaction des deux derniers lemmes du BFT + explication des algos + transition partie crash partie byzantine plus fluide

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

@@ -1,12 +1,3 @@
-\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:\ m = \rbreceived_i() \Rightarrow \exists p_j:\ \RBcast_j(m)$.
-  \item \textbf{No-duplicates}: No message is received more than once at any process.
-  \item \textbf{Validity}: If a correct process broadcasts $m$, every correct process eventually receives $m$.
-\end{itemize}
-
 \subsection{DenyList Object}
 
  We assume a linearizable DenyList (\DL) object as in~\cite{frey:disc23} with the following properties.

Recherche/BFT-ARBover/3_ARB_Def/index.tex

@@ -1,6 +1,11 @@
 
-Processes export \ABbroadcast$(m)$ and $m = \ABdeliver()$. \ARB requires total order:
-\begin{equation*}
-  \forall m_1,m_2,\ \forall p_i,p_j:\ \ (m_1 = \ABdeliver_i()) \prec (m_2 = \ABdeliver_i()) \Rightarrow (m_1 = \ABdeliver_j()) \prec (m_2 = \ABdeliver_j())
-\end{equation*}
-plus Integrity/No-duplicates/Validity (inherited from \RB and the construction).
+Processes export \ABbroadcast$(m)$ and $m = \ABdeliver()$. \ARB requires the following properties:
+\begin{itemize}[leftmargin=*]
+  \item \textbf{Total Order}: 
+  \begin{equation*}
+    \forall m_1,m_2,\ \forall p_i,p_j:\ \ (m_1 = \ABdeliver_i()) \prec (m_2 = \ABdeliver_i()) \Rightarrow (m_1 = \ABdeliver_j()) \prec (m_2 = \ABdeliver_j())
+  \end{equation*}
+  \item \textbf{Integrity}: Every message delivered was previously broadcast. $\forall p_i:\ m = \ABdeliver_i() \Rightarrow \exists p_j:\ \ABbroadcast_j(m)$.
+  \item \textbf{No-duplicates}: No message is delivered more than once at any process.
+  \item \textbf{Validity}: If a correct process broadcasts $m$, every correct process eventually delivers $m$.
+\end{itemize}

Recherche/BFT-ARBover/4_ARB_with_RB_DL/index.tex

@@ -1,4 +1,4 @@
-We present below an example of implementation of Atomic Reliable Broadcast (\ARB) using a Reliable Broadcast (\RB) primitive and a DenyList (\DL) object according to the model and notations defined in Section 2.
+We present below an example of implementation of Atomic Reliable Broadcast (\ARB) using point-to-point reliable, error-free channels and a DenyList (\DL) object according to the model and notations defined in Section 2.
 
 \subsection{Algorithm}
 
@@ -28,14 +28,17 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
   \For{$r = 1, 2, \ldots$}{
     \textbf{wait until} $\unordered \setminus \ordered \neq \emptyset$\;
     $S \leftarrow (\unordered \setminus \ordered)$\;\nllabel{code:Sconstruction}
-    $\RBcast(\texttt{PROP}, S, \langle r, i \rangle)$; $\PROVE(r)$; $\APPEND(r)$\;\nllabel{code:submit-proposition}
+    \lForEach{$j \in \Pi$}{
+      $\send(\texttt{PROP}, S, \langle r, i \rangle) \textbf{ to } p_j$
+    }
+    $\PROVE(r)$; $\APPEND(r)$\;\nllabel{code:submit-proposition}
 
     $\winners[r] \gets \{ j : (j, r) \in \READ() \}$\;\nllabel{code:Wcompute}
     
     \textbf{wait until} $\forall j \in \winners[r],\ \prop[r][j] \neq \bot$\;\nllabel{code:check-winners-ack}
     
     $M \gets \bigcup_{j \in \winners[r]} \prop[r][j]$\;\nllabel{code:Mcompute-dl}
-    $\ordered \leftarrow \ordered \cdot \ordered(M)$\;\nllabel{code:next-msg-extraction}
+    $\ordered \leftarrow \ordered \cdot \order(M)$\;\nllabel{code:next-msg-extraction}
   }
 
   \vspace{0.3em}
@@ -46,7 +49,7 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
 
   \vspace{0.3em}
 
-  \Upon{$\rdeliver(\texttt{PROP}, S, \langle r, j \rangle)$ from process $p_j$}{
+  \Upon{$\receive(\texttt{PROP}, S, \langle r, j \rangle)$ from process $p_j$}{
     $\unordered \leftarrow \unordered \cup \{S\}$\;\nllabel{code:receivedConstruction}
     $\prop[r][j] \leftarrow S$\;\nllabel{code:prop-set}
   }
@@ -54,7 +57,7 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
   \vspace{0.3em}
 
   \Upon{$\ABdeliver()$}{
-    \If{$\ordered \setminus \delivered = \emptyset$}{
+    \lIf{$\ordered \setminus \delivered = \emptyset$}{
       \Return{$\bot$}
     }
     let $m$ be the first element in $(\ordered \setminus \delivered$)\;\nllabel{code:adeliver-extract}
@@ -63,6 +66,10 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
   }
 
 \end{algorithm}
+
+\paragraph{Algorithm intuition.}
+The crash-tolerant algorithm is organized around round closure and winner extraction. By \Cref{def:closed-round,def:first-append,lem:closure-view,lem:winners}, once a round is closed, every correct process eventually reads the same winner set $\Winners_r$. By \Cref{lem:nonempty}, this set is never empty, and by \Cref{lem:winners-propose} every winner has necessarily sent its proposal to all processes before becoming a winner, exactly because sending precedes $\PROVE(r)$ and $\APPEND(r)$ at line~\ref{code:submit-proposition}. Under reliable channels, these winner proposals are eventually received by every correct process, so the waiting condition at line~\ref{code:check-winners-ack} eventually becomes true, which is formalized by \Cref{lem:eventual-closure}. Then, by \Cref{lem:convergence}, all correct processes compute the same set $M$ at line~\ref{code:Mcompute-dl}, and because line~\ref{code:next-msg-extraction} applies the same deterministic ordering function, they append messages in the same order; this is exactly the core mechanism later used in \Cref{lem:validity,lem:no-duplication,lem:total-order}.
+
 \subsection{Correctness}
 
 \begin{definition}[First APPEND]\label{def:first-append}
@@ -109,7 +116,7 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
 \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.
+  For any closed round $r$, all correct processes eventually observe the same set of valid tuples $(\ \cdot,r)$ in their \DL view.
 \end{lemma}
   
 \begin{proof}
@@ -117,7 +124,7 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
 
   Consider any correct process $p_i$ 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 $(\_,r)$ retrieved by a $\READ()$ 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.
+  Therefore, for any closed round $r$, all correct processes eventually observe the same set of valid tuples $(\ \cdot,r )$ in their \DL view.
 \end{proof}
 
 \begin{lemma}[Well-defined winners]\label{lem:winners}
@@ -131,7 +138,7 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
 \begin{proof}
   Lets consider a correct process $p_i$ that reach line~\ref{code:Wcompute} to compute $\winners[r]$. \\
   By program order, $p_i$ must have executed $\APPEND_i(r)$ at line~\ref{code:submit-proposition} before, which implies by \Cref{def:closed-round} that round $r$ is closed at that point. So by \Cref{def:winner-invariant}, $\Winners_r$ is defined. \\
-  By \Cref{lem:closure-view}, all correct processes eventually observe the same set of valid tuples $(\_,r)$ in their \DL view. Hence, when $p_i$ executes the $\READ()$ at line~\ref{code:Wcompute} after the $\APPEND_i(r)$, it observes a set $P$ that includes all valid tuples $(\_,r)$ such that
+  By \Cref{lem:closure-view}, all correct processes eventually observe the same set of valid tuples $(\ \cdot,r)$ in their \DL view. Hence, when $p_i$ executes the $\READ()$ at line~\ref{code:Wcompute} after the $\APPEND_i(r)$, it observes a set $P$ that includes all valid tuples $(\ \cdot ,r)$ such that
   \[
     \winners[r] = \{ j : (j,r) \in P \} = \{j : \PROVE_j(r) \prec \APPEND^{(\star)}(r) \} = \Winners_r
   \]
@@ -150,13 +157,13 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
 \end{proof}
 
 \begin{lemma}[Winners must propose]\label{lem:winners-propose}
-  For any closed round $r$, $\forall i \in \Winners_r$, process $p_i$ must have invoked a $\RBcast(PROP, S^{(i)}, \langle r, i \rangle)$ and hence any correct will eventually set $\prop[r][i]$ to a non-$\bot$ value.
+  For any closed round $r$, $\forall i \in \Winners_r$, process $p_i$ must have sent messages to all processes $j \in \Pi$, and hence any correct process $p_j$ will eventually receive $p_i$'s message for round $r$ and set $\prop[r][i]$ to a non-$\bot$ value.
 \end{lemma}
 
 \begin{proof}[Proof]
-  Fix a closed round $r$. By \Cref{def:winner-invariant}, for any $i \in \Winners_r$, there exist a valid $\PROVE_i(r)$ such that $\PROVE_i(r) \prec \APPEND^\star(r)$ in the DL linearization. By program order, if $i$ invoked a valid $\PROVE_i(r)$ at line~\ref{code:submit-proposition} he must have invoked $\RBcast(PROP, S^{(i)}, \langle r, i \rangle)$ directly before.
-
-  Let take a correct process $p_j$, by \RB \emph{Validity}, every correct process eventually receives $i$'s \RB message for round $r$, which sets $\prop[r][i]$ to a non-$\bot$ value at line~\ref{code:prop-set}.
+  Fix a closed round $r$. By \Cref{def:winner-invariant}, for any $i \in \Winners_r$, there exists a valid $\PROVE_i(r)$ such that $\PROVE_i(r) \prec \APPEND^\star(r)$ in the DL linearization. By program order in Algorithm~\ref{alg:arb-crash}, $p_i$ must have sent messages to all $j \in \Pi$ at line~\ref{code:submit-proposition} before invoking $\PROVE(r)$.
+  
+  If $p_i$ is a correct process that completed sending to all processes, then by the reliable and error-free nature of the communication channels, every correct process $p_j$ will eventually receive $p_i$'s message, which sets $\prop[r][i] \leftarrow S$ at line~\ref{code:prop-set}. If $p_i$ crashes before sending to all processes, then $p_i$ cannot invoke a valid $\PROVE_i(r)$ afterwards, contradicting the assumption that $i \in \Winners_r$. Hence $p_i$ must have completed sending to all processes.
 \end{proof}
 
 \begin{definition}[Messages invariant]\label{def:messages-invariant}
@@ -174,17 +181,17 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
 \begin{proof}[Proof]
   Let take a correct process $p_i$ that computes $M$ at line~\ref{code:Mcompute-dl}. By \Cref{lem:winners}, $p_i$ computation is the winner set $\Winners_r$.
 
-  By \Cref{lem:nonempty}, $\Winners_r \neq \emptyset$. The instruction at line~\ref{code:Mcompute-dl} where $p_i$ computes $M$ is guarded by the condition at line~\ref{code:check-winners-ack}, which ensures that $p_i$ has received all \RB messages from every winner $j \in \Winners_r$. Hence, $M = \bigcup_{j\in\Winners_r} \prop^{(i)}[r][j]$, we have $\prop^{(i)}[r][j] \neq \bot$ for all $j \in \Winners_r$.
+  By \Cref{lem:nonempty}, $\Winners_r \neq \emptyset$. The instruction at line~\ref{code:Mcompute-dl} where $p_i$ computes $M$ is guarded by the condition at line~\ref{code:check-winners-ack}, which ensures that $p_i$ has received messages from every winner $j \in \Winners_r$. By \Cref{lem:winners-propose}, each winner $j$ has sent messages to all processes including $p_i$. Thus, by the reliable and error-free nature of the channels, if $p_i$ is correct, it will eventually receive $j$'s message, setting $\prop^{(i)}[r][j] \neq \bot$ at line~\ref{code:prop-set}. Hence, $\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(PROP, S, \langle r, i \rangle)$.
+  For any round $r$ and any process $p_i$, $p_i$ sends messages to all processes at most once for each round.
 \end{lemma}
 
 \begin{proof}[Proof]
-  In Algorithm~\ref{alg:arb-crash}, the only place where a process $p_i$ can invoke $\RBcast(PROP, S, \langle r, i \rangle)$ is at line~\ref{code:submit-proposition}, which appears inside the main loop indexed by rounds $r = 1, 2, \ldots$.
+  In Algorithm~\ref{alg:arb-crash}, the only place where a process $p_i$ can send messages to all processes is at line~\ref{code:submit-proposition}, which appears inside the main loop indexed by rounds $r = 1, 2, \ldots$.
   
-  Each iteration of this loop processes exactly one round value $r$, and within that iteration, line~\ref{code:submit-proposition} is executed at most once. Since the loop variable $r$ takes each value $1, 2, \ldots$ at most once during the execution, process $p_i$ invokes $\RBcast(PROP, S, \langle r, i \rangle)$ at most once for any given round $r$.
+  Each iteration of this loop processes exactly one round value $r$, and within that iteration, messages are sent at most once (before the $\PROVE(r)$ and $\APPEND(r)$ calls). Since the loop variable $r$ takes each value $1, 2, \ldots$ at most once during the execution, process $p_i$ sends messages at most once for any given round $r$.
 \end{proof}
 
 \begin{lemma}[Proposal convergence]\label{lem:convergence}
@@ -196,31 +203,28 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
 
 \begin{proof}[Proof]
   Let take a correct process $p_i$ that compute $M$ at line~\ref{code:Mcompute-dl}. That implies that $p_i$ has defined $\winners r$ at line~\ref{code:Wcompute}. It implies that, by \Cref{lem:winners}, $r$ is closed and $\winners_r = \Winners_r$. \\
-  By \Cref{lem:eventual-closure}, for every $j \in \Winners_r$, $\prop^{(i)}[r][j] \neq \bot$. By \Cref{lem:unique-proposal}, each winner $j$ invokes at most one $\RBcast(PROP, S^{(j)}, \langle r, j \rangle)$, so $\prop^{(i)}[r][j] = S^{(j)}$ is uniquely defined. Hence, when $p_i$ computes
+  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$ sends messages to all processes at most once per round. Thus, $\prop^{(i)}[r][j] = S^{(j)}$ is uniquely defined as the messages sent by $j$ in that round. Hence, when $p_i$ computes
   \[
     M^{(i)} = \bigcup_{j\in\Winners_r} \prop^{(i)}[r][j] = \bigcup_{j\in\Winners_r} S^{(j)} = \Messages_r.
   \]
 \end{proof}
 
 \begin{lemma}[Inclusion]\label{lem:inclusion}
-  If some correct process invokes $\ABbroadcast(m)$, then there exist a round $r$ and a process $j\in\Winners_r$ such that $p_j$ invokes
-  \[
-  \RBcast(PROP, S, \langle r, j \rangle)\quad\text{for some S with}\quad m\in S.
-  \]
+  If some correct process invokes $\ABbroadcast(m)$, then there exist a round $r$ and a process $j\in\Winners_r$ such that $p_j$ sends a proposal $S$ to all processes at line~\ref{code:submit-proposition} with $m\in S$.
 \end{lemma}
 
 \begin{proof}
   Let $p_i$ be a correct process that invokes $\ABbroadcast(m)$. By the handler at line~\ref{code:abbroadcast-add}, $m$ is added to $\unordered$. Since $p_i$ is correct, it continues executing the main loop. 
   
-  Consider any iteration of the loop where $p_i$ executes line~\ref{code:Sconstruction} while $m \in (\unordered \setminus \ordered)$. At that iteration, for some round $r$, process $p_i$ constructs $S$ containing $m$ and invokes $\RBcast(PROP, S, \langle r, i \rangle)$ at line~\ref{code:submit-proposition}.
+  Consider any iteration of the loop where $p_i$ executes line~\ref{code:Sconstruction} while $m \in (\unordered \setminus \ordered)$. At that iteration, for some round $r$, process $p_i$ constructs $S$ containing $m$ and sends $S$ to all processes at line~\ref{code:submit-proposition}.
   
   We distinguish two cases:
   \begin{itemize}
-    \item \textbf{Case 1: $p_i$ is a winner.} If $p_i \in \Winners_r$ for this round $r$, then by \Cref{def:winner-invariant} and program order, $p_i$ has invoked $\RBcast(PROP, S, \langle r, i \rangle)$ with $m \in S$, and the lemma holds with $j = i$.
+    \item \textbf{Case 1: $p_i$ is a winner.} If $p_i \in \Winners_r$ for this round $r$, then by \Cref{def:winner-invariant} and program order, $p_i$ has sent proposal $S$ to all processes with $m \in S$, and the lemma holds with $j = i$.
     
-    \item \textbf{Case 2: $p_i$ is not a winner.} If $p_i \notin \Winners_r$, then by the \RB \emph{Validity} property, all correct processes eventually \rdeliver $p_i$'s message. By line~\ref{code:receivedConstruction}, each correct process $p_k$ adds $m$ to its own $\unordered$ set. Hence every correct process will eventually attempt to broadcast $m$ in some subsequent round.
+    \item \textbf{Case 2: $p_i$ is not a winner.} If $p_i \notin \Winners_r$, then $p_i$ is still a correct process, so it has sent its proposal $S$ (containing $m$) to all processes in $\Pi$. By the reliable and error-free nature of the communication channels, all correct processes will eventually receive $p_i$'s message. By line~\ref{code:receivedConstruction}, each correct process $p_k$ adds $m$ to its own $\unordered$ set. Hence every correct process will eventually attempt to broadcast $m$ in some subsequent round.
     
-    Since there are infinitely many rounds and finitely many processes, and by \Cref{lem:nonempty} every closed round has at least one winner, there must exist a round $r'$ and a correct process $p_j \in \Winners_{r'}$ such that $m \in (\unordered \setminus \ordered)$ when $p_j$ constructs its proposal $S$ at line~\ref{code:Sconstruction} for round $r'$. Hence $p_j$ invokes $\RBcast(PROP, S, \langle r', j \rangle)$ with $m \in S$.
+    Since there are infinitely many rounds and finitely many processes, and by \Cref{lem:nonempty} every closed round has at least one winner, there must exist a round $r'$ and a correct process $p_j \in \Winners_{r'}$ such that $m \in (\unordered \setminus \ordered)$ when $p_j$ constructs its proposal $S$ at line~\ref{code:Sconstruction} for round $r'$. Hence $p_j$ sends messages $S$ with $m \in S$ at line~\ref{code:submit-proposition}.
   \end{itemize}
   
   In both cases, there exists a round and a winner whose proposal includes $m$.
@@ -239,12 +243,9 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
 \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(PROP, S, \langle r, j \rangle)\quad\text{with}\quad m\in S.
-  \]
+  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$ sends a proposal $S$ to all processes with $m\in S$.
 
-  By \Cref{lem:eventual-closure}, when $p_q$ computes $M$ at line~\ref{code:Mcompute-dl}, $\prop[r][j]$ is non-$\bot$ because $j \in \Winners_r$. By \Cref{lem:unique-proposal}, $p_j$ invokes at most one $\RBcast(PROP, S, \langle r, j \rangle)$, so $\prop[r][j]$ is uniquely defined. Hence, when $p_q$ computes
+  By \Cref{lem:eventual-closure}, when $p_q$ computes $M$ at line~\ref{code:Mcompute-dl}, $\prop[r][j]$ is non-$\bot$ because $j \in \Winners_r$. By \Cref{lem:unique-proposal}, $p_j$ sends messages at most once per round, so $\prop[r][j]$ is uniquely defined as the proposal sent by $j$. Hence, when $p_q$ computes
   \[
     M = \bigcup_{k\in\Winners_r} \prop[r][k],
   \]
@@ -266,13 +267,7 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
 \end{lemma}
 
 \begin{proof}
-  Consider a correct process that delivers both $m_1$ and $m_2$. By \Cref{lem:validity}, there exists a closed rounds $r_1$ and $r_2$ and correct processes $k_1 \in \Winners_{r_1}$ and $k_2 \in \Winners_{r_2}$ such that
-  \[
-    \RBcast(PROP, S_1, \langle r_1, k_1 \rangle)\quad\text{with}\quad m_1\in S_1,
-  \]
-  \[
-    \RBcast(PROP, S_2, \langle r_2, k_2 \rangle)\quad\text{with}\quad m_2\in S_2.
-  \]
+  Consider a correct process that delivers both $m_1$ and $m_2$. By \Cref{lem:validity}, there exists 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 $p_{k_1}$ and $p_{k_2}$ send proposals $S_1$ and $S_2$ respectively, with $m_1\in S_1$ and $m_2\in S_2$.
 
   Let consider two cases :
   \begin{itemize}
@@ -285,32 +280,32 @@ We present below an example of implementation of Atomic Reliable Broadcast (\ARB
 \end{proof}
 
 \begin{theorem}[\ARB]
-Under the assumed $\DL$ synchrony and $\RB$ reliability, the algorithm implements Atomic Reliable Broadcast.
+In a crash asynchronous message-passing system with reliable, error-free communication channels, assuming a synchronous DenyList ($\DL$) object, the algorithm implements Atomic Reliable Broadcast.
 \end{theorem}
 
 \begin{proof}
-  We show that the algorithm satisfies the properties of Atomic Reliable Broadcast under the assumed $\DL$ synchrony and $\RB$ reliability.
+  We show that the algorithm satisfies the properties of Atomic Reliable Broadcast under the assumed $\DL$ synchrony and reliable channel assumption.
 
   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.
+  Concerning Integrity and No-duplicates, the construction only ever delivers messages that have been obtained from processes that constructed and sent them in the algorithm.
+  Every delivered message was previously sent by some process at line~\ref{code:submit-proposition}, 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.
 
-  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.
+  All the above lemmas are proved under the assumptions that $\DL$ satisfies the required synchrony properties and that the communication channels are reliable and error-free (no message loss or corruption).
   Therefore, under these assumptions, the algorithm satisfies Validity, Integrity/No-duplicates, and total order, and hence implements Atomic Reliable Broadcast, as claimed.
 \end{proof}
 
 \subsection{Reciprocity}
 % ------------------------------------------------------------------------------
 
-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.
+So far, we assumed the existence of a synchronous DenyList ($\DL$) object and showed how to build an Atomic Reliable Broadcast ($\ARB$) primitive using reliable, error-free point-to-point channels. We now briefly argue that, conversely, an $\ARB$ primitive is strong enough to implement a synchronous $\DL$ object.
 
 \xspace
 
@@ -346,7 +341,7 @@ Which are cover by our FIFO-\ARB specification.
   \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.
+    \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

Recherche/BFT-ARBover/5_BFT_ARB/index.tex

@@ -1,15 +1,15 @@
 
 \subsection{Model extension}
-We consider a static set $\Pi$ of $n$ processes with known identities, communicating by reliable point-to-point channels, in a complete graph. Messages are uniquely identifiable. At most $f$ processes may be Byzantine, and we assume $n > 3f$.
+We extend the crash model of Section 1 (same process universe, asynchronous setting, uniquely identifiable messages, and reliable point-to-point channels) with Byzantine faults and Byzantine-resilient dissemination primitives.
 
-\paragraph{Synchrony.} The network is asynchronous.
+\paragraph{Failure threshold.} At most $t$ processes may be Byzantine, and we assume $n > 3t$.
 
-\paragraph{Communication.} Processes can exchange through a Reliable Broadcast ($\RB$) primitive (defined below) which is invoked with the functions $\RBcast(m)$ and $m = \rbreceived()$. The Reliable Broadcast is a Byzantine fault-tolerant primitive following Bracha's specification \cite{Bracha1987}: for any message $m$ broadcast by a process $p_j$, every correct process either receives the message $m$ or none at all; moreover, all correct processes that receive a broadcast from $p_j$ for a given sequence number or round receive exactly the same message. This ensures that Byzantine processes cannot send different messages to different correct processes for the same broadcast instance. There exists a shared object called DenyList ($\DL$) (defined below) that is interfaced with a set $O$ of operations. There exist three types of these operations: $\APPEND(x)$, $\PROVE(x)$ and $\READ()$.
+\paragraph{Additional communication primitive.} In addition to reliable point-to-point channels, processes use Reliable Broadcast ($\RB$) with operations $\RBcast(m)$ and $m=\rdeliver()$. We use Bracha's Byzantine RB specification (1987): for a fixed sender and broadcast instance, all correct processes that deliver, deliver the same payload, and Byzantine equivocation on that instance is prevented.
 
 \paragraph{Byzantine behaviour}
-A process is said to exhibit Byzantine behaviour if it deviates arbitrarily from the prescribed algorithm. Such deviations may, for instance, consist in invoking primitives ($\RBcast$, $\APPEND$, $\PROVE$, etc.) with invalid inputs or inputs crafted maliciously, colluding with other Byzantine processes in an attempt to manipulate the system state or violate its guarantees, deliberately delaying or accelerating the delivery of messages to selected nodes so as to disrupt the expected timing of operations, or withholding messages and responses in order to induce inconsistencies in the system state.
+A Byzantine process may deviate arbitrarily from the algorithm (malformed inputs, selective omission, collusion, inconsistent timing, etc.).
 
-Byzantine processes are constrained by the following. They cannot forge valid cryptographic signatures or threshold shares without access to the corresponding private keys. They cannot violate the termination, validity, or anti-flickering properties of the $\DL$ object. They also cannot break the integrity, no-duplicates, or validity properties of the $\RB$ primitive.
+Byzantine processes are still constrained by the assumed primitives: they cannot violate the safety/liveness guarantees of $\DL$ and cannot break the Integrity, No-duplicates, and Validity guarantees of $\RB$.
 
 
 \paragraph{Notation.} For any indice $k$ we defined by $\DL[k]$ as the $k$-th DenyList object. For a given $\DL[k]$ and any indice $x$ we defined by $\Pi_x^k$ a subset of $\Pi$. Still for a given $k$ we consider $\Pi_M^k \subseteq \Pi$ and $\Pi_V^k \subseteq \Pi$ two authorization subsets for $\DL[k]$. Indice $i \in \Pi$ refer to processes, and $p_i$ denotes the process with identifier $i$. Let $\mathcal{M}$ denote the universe of uniquely identifiable messages, with $m \in \mathcal{M}$. Let $\mathcal{R} \subseteq \mathbb{N}$ be the set of round identifiers; we write $r \in \mathcal{R}$ for a round. We use the precedence relation $\prec_k$ for the $\DL[k]$ linearization: $x \prec_k y$ means that operation $x$ appears strictly before $y$ in the linearized history of $\DL[k]$. 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).
@@ -18,6 +18,15 @@ For any operation $F \in O$,$F_i(...)$ denotes that the operation $F$ is invoked
 % ------------------------------------------------------------------------------
 \subsection{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:\ m = \rbreceived_i() \Rightarrow \exists p_j:\ \RBcast_j(m)$.
+  \item \textbf{No-duplicates}: No message is received more than once at any process.
+  \item \textbf{Validity}: If a correct process broadcasts $m$, every correct process eventually receives $m$.
+\end{itemize}
+
 \subsubsection{t-BFT-DL}
 
 We consider a t-Byzantine Fault Tolerant DenyList (t-$\BFTDL$) with the following properties.
@@ -29,7 +38,7 @@ There are 3 operations : $\BFTPROVE(x), \BFTAPPEND(x), \BFTREAD()$ such that :
 
 \paragraph{PROVE Anti-Flickering.} If the invocation of a operation $op = \BFTPROVE(x)$ by a correct process $p \in \Pi_V$ is invalid, then any $\BFTPROVE(x)$ operation that appears after $op$ in $\Seq$ is invalid.
 
-\paragraph{READ Liveness.} Let $op = \BFTREAD()$ invoke by a correct process such that $R$ is the result of $op$. For all $(i, \PROVEtrace(x)) \in R$ there exist a valid invocation of $\BFTPROVE(x)$ by $p_i$.
+\paragraph{READ Liveness.} Let $op = \BFTREAD()$ invoke by a correct process such that $R$ is the result of $op$. For all $(i, x) \in R$ there exist a valid invocation of $\BFTPROVE(x)$ by $p_i$.
 
 \paragraph{READ Anti-Flickering.} Let $op_1, op_2$ two $\BFTREAD()$ operations that returns respectively $R_1, R_2$. Iff $op_1 \prec op_2$ then $R_2 \subseteq R_1$. Otherwise $R_1 \subseteq R_2$.
 
@@ -83,6 +92,9 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au
     }
 \end{algorithm}
 
+\paragraph{Algorithm intuition.}
+In the Byzantine setting, a process identifier $j$ is selected in $\winners[r]$ only when it accumulates at least $t+1$ proofs for round $r$ in $\validated(r)$. A process emits such a proof for $j$ only after receiving $j$'s $\texttt{PROP}$ payload (handler $\rdeliver(\texttt{PROP},\cdot)$). Therefore, if $j$ is a winner, at least one correct process has received $j$'s proposal. By RB agreement/validity, once one correct process receives that proposal for the instance, all correct processes eventually receive the same payload, so winner proposals eventually become available everywhere and can be merged consistently.
+
 \begin{lemma}[BFT-PROVE Validity]\label{lem:bft-prove-validity}
     The invocation of $op = \BFTPROVE(x)$ by a correct process is invalid iff there exist at least $t+1$ distinct processes in $M$ that invoked a valid $\BFTAPPEND(x)$ before $op$ in $\Seq$.
 \end{lemma}
@@ -124,7 +136,7 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au
 \end{lemma}
 
 \begin{proof}
-    Let $R$ the result of a $READ()$ operation submit by any correct process. $(i, \PROVEtrace(x)) \in R$ implie that $\exists U^\star \in \mathcal{U}$ such that $(i, x) \in R^{U^\star}$ with $R^{U^\star}$ the result of $DL_{U^\star}.\READ()$. By \textbf{READ Validity} $(i, x) \in R^{U^\star}$ implie that there exist a valid  $DL_{U^\star}.\PROVE_i(x)$. The for loop in the $\BFTPROVE(x)$ implementation return true iff there at least one valid $DL_{U}.\PROVE_i(x)$ for any $U \in \mathcal{U}$.
+    Let $R$ the result of a $READ()$ operation submit by any correct process. $(i, x) \in R$ implie that $\exists U^\star \in \mathcal{U}$ such that $(i, x) \in R^{U^\star}$ with $R^{U^\star}$ the result of $DL_{U^\star}.\READ()$. By \textbf{READ Validity} $(i, x) \in R^{U^\star}$ implie that there exist a valid  $DL_{U^\star}.\PROVE_i(x)$. The for loop in the $\BFTPROVE(x)$ implementation return true iff there at least one valid $DL_{U}.\PROVE_i(x)$ for any $U \in \mathcal{U}$.
 
     Hence because there exist a $U^\star$ such that $DL_{U^\star}.\PROVE_i(x)$, there exist a valid $\BFTPROVE_i(x)$.
 
@@ -189,18 +201,18 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au
     \For{$r = 1, 2, \ldots$}{\nllabel{alg:main-loop}
         \textbf{wait until} $\unordered \setminus \ordered \neq \emptyset$\;
         $S \gets \unordered \setminus \ordered$;
-        $\RBcast(i, \texttt{PROP}, S, r)$\;
+        $\RBcast(\texttt{PROP}, S, \langle i, r \rangle)$\;
 
         \textbf{wait until} $|\validated(r)| \geq n - t$\;\nllabel{alg:check-validated}
 
         \BlankLine
 
         \lForEach{$j \in \Pi$}{
-            $\BFTAPPEND(\langle j, r\rangle)$\;\nllabel{alg:append}
+            $\BFTAPPEND(\langle j, r\rangle)$\nllabel{alg:append}
         }
 
         \lForEach{$j \in \Pi$}{
-            $\send(j, \texttt{DONE}, r)$\;
+            $\send(\texttt{DONE}, r)$ \textbf{ to } $p_j$
         }
 
         \BlankLine
@@ -211,7 +223,7 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au
         \BlankLine
 
         $M \gets \bigcup_{j \in \winners[r]} \prop[r][j]$\;\nllabel{code:Mcompute}
-        $\ordered \gets \ordered \cdot \ordered(M)$\;
+        $\ordered \gets \ordered \cdot \order(M)$\;
     }
 
     \vspace{0.3em}
@@ -253,6 +265,9 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au
     
 \end{algorithm}
 
+\paragraph{Algorithm intuition.}
+The Byzantine-tolerant construction combines threshold evidence and RB agreement to make winner selection robust. A sender $j$ appears in $\validated(r)$ only when at least $t+1$ proofs for $\langle j,r\rangle$ are observed through $\BFTREAD()$, and by \Cref{lem:bft-prove-validity} this threshold means that $j$ cannot be certified without broad enough support from the system. Once a round is closed, the winner set becomes stable by \Cref{lem:winners-stability}, so correct processes stop diverging on who contributes to the round outcome. For each stable winner, the associated proposal payload is unique at correct receivers by \Cref{lem:bft-unique-proposal}, which prevents equivocation from creating distinct local values for the same winner identity. Consequently, when correct processes wait for all winner proposals and compute the union at line~\ref{code:Mcompute}, they obtain the same message set by \Cref{lem:message-content-invariance}. Progress is then ensured by \Cref{lem:bft-eventual-closure}, which guarantees that if new messages remain unordered, a new round eventually closes with at least $n-t$ winners. Finally, once rounds are commonly closed, appending $\order(M)$ at each round yields a common delivery sequence, exactly formalized by \Cref{lem:bft-total-order}.
+
 % \textbf{Everything below has to be updated}
 
 % \begin{definition}[BFT Closed round for $k$]
@@ -422,11 +437,7 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au
     By strong induction, if round $r$ is closed, all rounds $r_1 < r$ are closed.
 \end{proof}
 
-\begin{lemma}[Eventual Closure]\label{lem:eventual-closure}
-    For any correct process $p_i$, if $\unordered \setminus \ordered \neq \emptyset$ and if $r$ is the highest closed round observed by $p_i$, then eventually round $r+1$ will be closed with $|\winners[r+1]| \geq n - t$.
-\end{lemma}
-
-\begin{lemma}[Uniqueness of Winners' Proposals]\label{lem:unique-proposal}
+\begin{lemma}[Uniqueness of Winners' Proposals]\label{lem:bft-unique-proposal}
     For any closed round $r$ and any process $p_j \in \winners[r]$, there exists a unique set $S_j \subseteq \mathcal{M}$ such that every correct process $p_i$ that has received a reliable delivery of a $\texttt{PROP}$ message from $p_j$ for round $r$ receives exactly this set $S_j$.
 \end{lemma}
 
@@ -437,7 +448,7 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au
     
     Since at least $t+1$ distinct processes have performed a valid $\BFTPROVE(\langle j, r \rangle)$, and since $t < n/3$, at least one of these processes is correct. Thus, at least one correct process must have received a reliable broadcast from $p_j$ for round $r$.
     
-    Now, by Bracha's Byzantine Reliable Broadcast specification \cite{Bracha1987}, for any message broadcast instance by process $p_j$ in round $r$, all correct processes that deliver this broadcast either receive the identical message or none at all. Formally, for all correct processes $p_i, p_i'$ that received a delivery from $p_j$ for round $r$, we have $S_j^{(i)} = S_j^{(i')}$. 
+    Now, by Bracha's Byzantine Reliable Broadcast specification, for any message broadcast instance by process $p_j$ in round $r$, all correct processes that deliver this broadcast either receive the identical message or none at all. Formally, for all correct processes $p_i, p_i'$ that received a delivery from $p_j$ for round $r$, we have $S_j^{(i)} = S_j^{(i')}$. 
     
     Therefore, there exists a unique set $S_j$ such that every correct process $p_i$ that receives a reliable delivery from $p_j$ for round $r$ receives exactly $S_j$.
 \end{proof}
@@ -477,7 +488,7 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au
     
     By \cref{lem:winners-stability}, the set $\winners[r]$ is stable once round $r$ is closed. Therefore, both $p_i$ and $p_{i'}$ compute the same set of winners $\winners[r]$.
     
-    Now, consider any winner $j \in \winners[r]$. By \cref{lem:unique-proposal}, there exists a unique set $S_j \subseteq \mathcal{M}$ such that every correct process that receives a reliable delivery of a $\texttt{PROP}$ message from $p_j$ for round $r$ receives exactly $S_j$. 
+    Now, consider any winner $j \in \winners[r]$. By \cref{lem:bft-unique-proposal}, there exists a unique set $S_j \subseteq \mathcal{M}$ such that every correct process that receives a reliable delivery of a $\texttt{PROP}$ message from $p_j$ for round $r$ receives exactly $S_j$. 
     
     By the algorithm, each correct process stores this received set in its local variable: $\prop^{(i)}[r][j] = S_j$ and $\prop^{(i')}[r][j] = S_j$.
     
@@ -489,10 +500,60 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au
     Therefore, all correct processes compute the same set $M$ for any closed round $r$.
 \end{proof}
 
-\begin{lemma}[Total Order]\label{lem:total-order}
+\begin{lemma}[Inclusion]\label{lem:bft-inclusion}
+    If a correct process $p_i$ invokes $\ABbroadcast(m)$, then there exist a closed round $r$ and a winner $j \in \winners[r]$ such that $p_j$ invoked $\RBcast(j, \texttt{PROP}, S, r)$ with $m \in S$.
+\end{lemma}
+
+\begin{proof}
+    Let $p_i$ be a correct process that invokes $\ABbroadcast(m)$. By the algorithm, $p_i$ adds $m$ to $\unordered$. Consequently, $\unordered \setminus \ordered \neq \emptyset$, and the process enters the main loop and eventually invokes $\RBcast(i, \texttt{PROP}, S_i^{(1)}, r_1)$ for some round $r_1$ where $m \in S_i^{(1)}$.
+
+    We distinguish two cases:
+    
+    \textbf{Case 1: $p_i$ becomes a winner in round $r_1$.}
+    If $p_i$ is elected as a winner for round $r_1$ (i.e., $i \in \winners[r_1]$), then the claim holds with $r = r_1$ and $j = i$.
+    
+    \textbf{Case 2: $p_i$ does not become a winner in round $r_1$.}
+    If $p_i$ is not elected as a winner, by the properties of Reliable Broadcast (Bracha's specification), at least one correct process $p_{i_1}$ will eventually receive the reliable delivery of the $\texttt{PROP}$ message from $p_i$ for round $r_1$. Process $p_{i_1}$ adds all messages from $S_i^{(1)}$ to its $\unordered$ set at line \ref{alg:append}. In particular, $m$ is now in $p_{i_1}$'s $\unordered$ set.
+    
+    In round $r_2 > r_1$ (and any subsequent round), process $p_{i_1}$ computes $S_{i_1}^{(2)} = \unordered \setminus \ordered$ and invokes $\RBcast(i_1, \texttt{PROP}, S_{i_1}^{(2)}, r_2)$ with $m \in S_{i_1}^{(2)}$.
+    
+    This process repeats: either $p_{i_1}$ becomes a winner and the claim holds, or another correct process receives $p_{i_1}$'s proposal and includes $m$ in its own proposal.
+    
+    Since $n > 3f$, we have $n - t > t + 1 > f$. By the pigeonhole principle, there eventually exists a round $r$ where at least $n - t$ distinct processes have proposed sets containing $m$. Since more than $2f$ processes have proposed $m$, at least one of them must be correct and be elected as a winner. Therefore, there exist a round $r$ and a winner $j \in \winners[r]$ such that $m \in S_j$ was broadcast by $p_j$.
+\end{proof}
+
+\begin{lemma}[Eventual Closure]\label{lem:bft-eventual-closure}
+    For any correct process $p_i$, if $\unordered \setminus \ordered \neq \emptyset$ and if $r$ is the highest closed round observed by $p_i$, then eventually round $r+1$ will be closed with $|\winners[r+1]| \geq n - t$.
+\end{lemma}
+
+\begin{proof}
+    Let $p_i$ be a correct process such that $\unordered \setminus \ordered \neq \emptyset$ after round $r$ is the highest closed round it observed. By the main loop of Algorithm~\ref{alg:bft-arb}, $p_i$ eventually enters round $r+1$, computes $S=\unordered\setminus\ordered$, and invokes $\RBcast(\texttt{PROP},S,\langle i,r+1\rangle)$.
+
+    By RB Validity, every correct process eventually $\rdeliver(\texttt{PROP},S,\langle i,r+1\rangle)$. Upon this delivery, each correct process executes $\BFTPROVE(\langle i,r+1\rangle)$. Hence at least $n-t$ correct processes issue a proof for candidate $i$ in round $r+1$, and in particular the threshold $t+1$ used in $\validated(r+1)$ is eventually met for that candidate.
+
+    The same argument applies to each correct process that broadcasts in round $r+1$: once its proposal is RB-delivered, at least $n-t$ correct processes issue the corresponding proofs, so that sender is eventually included in $\validated(r+1)$. Since there are at least $n-t$ correct processes, eventually $|\validated(r+1)| \geq n-t$, and the wait at line~\ref{alg:check-validated} is eventually released for every correct process in that round.
+
+    After this point, each correct process executes the $\BFTAPPEND$ loop (line~\ref{alg:append}) and sends $\texttt{DONE}$ to all processes. By reliability of point-to-point channels, every correct process eventually receives at least $n-t$ DONE messages, so the wait at line~\ref{alg:check-done} is also eventually released. At that moment, the process computes $\winners[r+1] \gets \validated(r+1)$, and by the previous bound we have $|\winners[r+1]| \geq n-t$.
+
+    Therefore round $r+1$ eventually becomes closed with at least $n-t$ winners.
+\end{proof}
+
+\begin{lemma}[Total Order]\label{lem:bft-total-order}
     For any two correct processes $p_i$ and $p_j$, the sequence $\ordered$ maintained locally by $p_i$ and the sequence maintained by $p_j$ contain the same messages in the same order, provided that both have reached the same set of closed rounds.
 \end{lemma}
 
+\begin{proof}
+    We prove the claim by induction on the number of closed rounds completed by both processes.
+
+    \textbf{Base case.} Before any closed round is completed, both local sequences are initialized to $\epsilon$, hence identical.
+
+    \textbf{Induction step.} Assume that after all closed rounds up to $r-1$, processes $p_i$ and $p_j$ have identical $\ordered$ prefixes. Consider round $r$.
+
+    By \Cref{lem:winners-stability}, once round $r$ is closed, both processes use the same stable winner set $\winners[r]$. By \Cref{lem:message-content-invariance}, the set $M$ computed at line~\ref{code:Mcompute} is identical at all correct processes for that round. Both processes then apply the same deterministic ordering function $\order(M)$ and append that same ordered block to their current sequence.
+
+    Since they started round $r$ from identical prefixes and append the same ordered suffix for round $r$, their resulting sequences after round $r$ are identical. The induction concludes that for any common set of closed rounds, both correct processes maintain the same messages in the same order.
+\end{proof}
+
 \begin{theorem}
     The algorithm implements a BFT Atomic Reliable Broadcast.
 \end{theorem}

Recherche/BFT-ARBover/main.tex

@@ -48,7 +48,7 @@
 \newcommand{\DL}{\textsf{DL}}
 \newcommand{\append}{\ensuremath{\mathsf{append}}}
 \newcommand{\prove}{\ensuremath{\mathsf{prove}}}
-\newcommand{\PROVEtrace}{\ensuremath{\mathsf{prove}}}
+% \newcommand{\PROVEtrace}{\ensuremath{\mathsf{prove}}}
 \newcommand{\readop}{\ensuremath{\mathsf{read}}}
 
 % Backward compatibility aliases
@@ -65,7 +65,7 @@
 \newcommand{\validated}{\ensuremath{\textsc{validated}}}
 \newcommand{\rbcast}{\ensuremath{\mathsf{rbcast}}}
 \newcommand{\rbreceived}{\ensuremath{\mathsf{rreceived}}}
-% \newcommand{\ordered}{\ensuremath{\mathsf{order}}}
+\newcommand{\order}{\ensuremath{\mathsf{order}}}
 
 % Backward compatibility aliases
 \newcommand{\RBcast}{\rbcast}
@@ -117,7 +117,7 @@ We consider a static set $\Pi$ of $n$ processes with known identities, communica
 
 \paragraph{Synchrony.} The network is asynchronous.
 
-\paragraph{Communication.} Processes can exchange through a Reliable Broadcast ($\RB$) primitive (defined below) which is invoked with the functions $\RBcast(m)$ and $m = \rbreceived()$. There exists a shared object called DenyList ($\DL$) (defined below) that is interfaced with a set $O$ of operations. There exist three types of these operations: $\APPEND(x)$, $\PROVE(x)$ and $\READ()$.   
+\paragraph{Communication.} Processes communicate through reliable, error-free point-to-point channels. Messages sent by a correct process to another correct process are eventually delivered without loss or corruption. There exists a shared object called DenyList ($\DL$) (defined below) that is interfaced with a set $O$ of operations. There exist three types of these operations: $\APPEND(x)$, $\PROVE(x)$ and $\READ()$.   
 
 \paragraph{Notation.} For any indice $x$ we defined by $\Pi_x$ a subset of $\Pi$. We consider two subsets $\Pi_M$ and $\Pi_V$ two authorization subsets. Indices $i \in \Pi$ refer to processes, and $p_i$ denotes the process with identifier $i$. Let $\mathcal{M}$ denote the universe of uniquely identifiable messages, with $m \in \mathcal{M}$. Let $\mathcal{R} \subseteq \mathbb{N}$ be the set of round identifiers; we write $r \in \mathcal{R}$ for a round. We use the precedence relation $\prec$ for the \DL{} linearization: $x \prec y$ means that operation $x$ appears strictly before $y$ in the linearized history of \DL. For any finite set $A \subseteq \mathcal{M}$, \ordered$(A)$ returns a deterministic total order over $A$ (e.g., lexicographic order on $(\textit{senderId},\textit{messageId})$ or on message hashes).
 For any operation $F \in O$,$F_i(...)$ denotes that the operation $F$ is invoked by process $p_i$.
@@ -132,7 +132,7 @@ For any operation $F \in O$,$F_i(...)$ denotes that the operation $F$ is invoked
 
 \input{3_ARB_Def/index.tex}
 
-\section{ARB over RB and DL}
+\section{ARB using DL}
 
 \input{4_ARB_with_RB_DL/index.tex}
 
@@ -143,156 +143,156 @@ For any operation $F \in O$,$F_i(...)$ denotes that the operation $F$ is invoked
 
 
 
-\section{Implementation of BFT-DenyList and Threshold Cryptography}
+% \section{Implementation of BFT-DenyList and Threshold Cryptography}
 
-\subsection{DenyList}
+% \subsection{DenyList}
 
-\paragraph{BFT-DenyList}
-In our algorithm we use multiple DenyList as follows:
+% \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{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{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{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{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}
+% \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 :
+% 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}
+% \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 :
+% 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}
 
 % \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}
+%     $j \gets$ the process invoking $\READ'()$\;
+%     $\res \gets \emptyset$\;
+%     \ForAll{$i \in \{1, \dots, k\}$}{
+%       $\res \gets \res \cup DL_i.\READ()$\;
+%     }
+%     \Return{$\res$}\;
+%  \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{$\APPEND'(\sigma) \rightarrow ()$}
+%       $j \gets$ the process invoking $\APPEND'(\sigma)$\;
+%       \ForAll{$M_i \in \{M_k \in  M : j \in M_k\}$}{
+%         $DL_i.\APPEND(\sigma)$\;
+%       }
+%   \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}
+%   \begin{algorithm}[H]
+%     \caption{$\PROVE'(\sigma) \rightarrow \{0, 1\}$}
+%       $j \gets$ the process invoking $\PROVE'(\sigma)$\;
+%       $\flag \gets false$\;
+%       \ForAll{$i \in \{1, \dots, k\}$}{
+%         $\flag \gets \flag$ OR $DL_i.\PROVE(\sigma)$\;
+%       }
+%       \Return{$\flag$}\;
+%   \end{algorithm}
 
-\begin{algorithm}[H]
-  \caption{$\READ'() \rightarrow \mathcal{L}(\mathbb{R} \times \PROVEtrace(\mathbb{R}))$}
-    $j \gets$ the process invoking $\READ'()$\;
-    $\res \gets \emptyset$\;
-    \ForAll{$i \in \{1, \dots, k\}$}{
-      $\res \gets \res \cup DL_i.\READ()$\;
-    }
-    \Return{$\res$}\;
- \end{algorithm}
+% \subsection{Threshold Cryptography}
 
-  \begin{algorithm}[H]
-    \caption{$\APPEND'(\sigma) \rightarrow ()$}
-      $j \gets$ the process invoking $\APPEND'(\sigma)$\;
-      \ForAll{$M_i \in \{M_k \in  M : j \in M_k\}$}{
-        $DL_i.\APPEND(\sigma)$\;
-      }
-  \end{algorithm}
+% We are using the Boneh-Lynn-Shacham scheme as cryptography primitive to our threshold signature scheme.
+% With :
 
-  \begin{algorithm}[H]
-    \caption{$\PROVE'(\sigma) \rightarrow \{0, 1\}$}
-      $j \gets$ the process invoking $\PROVE'(\sigma)$\;
-      $\flag \gets false$\;
-      \ForAll{$i \in \{1, \dots, k\}$}{
-        $\flag \gets \flag$ OR $DL_i.\PROVE(\sigma)$\;
-      }
-      \Return{$\flag$}\;
-  \end{algorithm}
+% \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}
 
-\subsection{Threshold Cryptography}
+% Such that :
 
-We are using the Boneh-Lynn-Shacham scheme as cryptography primitive to our threshold signature scheme.
-With :
+% \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}
 
-\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}
+% \paragraph{threshold Scheme}
 
-Such that :
+% In our algorithm we are only using the following functions :
 
-\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}
+% \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}
 
-\paragraph{threshold Scheme}
+% Such that :
 
-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}
+% \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}