update

2025-10-22 12:17:11 +00:00
parent 2194f699d6
commit e6865efc53
9 changed files with 492 additions and 2567 deletions
--- a/Recherche/ALDLoverAB/algo/index.tex
+++ b/Recherche/ALDLoverAB/algo/index.tex
@@ -5,9 +5,8 @@ We consider a set of processes communicating asynchronously over reliable point-
  \item \textbf{\textit{delivered}}: the set of messages that have been ordered.
  \item \textbf{\textit{prop}[$r$][$j$]}: the proposal set announced by process $j$ at round $r$. It contains a set of messages that process $j$ claims to have received but not yet delivered.
  \item \textbf{\textit{winner}$^r$}: the set of processes that have issued a valid \texttt{PROVE} for round $r$, as observed through the registry.
-  \item \textbf{\textit{window}}: the list of the ids from the $f+1$ last rounds. \textit{window.pop()} remove the first value of the array. \textit{window.push(x)} append x as the last value of the array.
-  \item \textbf{\texttt{RB-cast}$(\texttt{PROP}, S, r, j)$}: a reliable broadcast invocation that disseminates the proposal $S$ from process $j$ for round $r$.
-  \item \textbf{\texttt{RB-delivered}$(\texttt{PROP}, S, r, j)$}: the handler invoked upon reception of a \texttt{RB-cast}, which stores the received proposal $S$ into $\textit{prop}[r][j]$.
+  \item \textbf{\texttt{R-Broadcast}$(\texttt{PROP}, S, r, j)$}: a reliable broadcast invocation that disseminates the proposal $S$ from process $j$ for round $r$.
+  \item \textbf{\texttt{R-Delivered}$(\texttt{PROP}, S, r, j)$}: the handler invoked upon reception of a \texttt{RB-cast}, which stores the received proposal $S$ into $\textit{prop}[r][j]$.
  \item \textbf{\texttt{READ}()} : returns the current view of all valid operations stored in the DenyList registry.
  \item \textbf{\texttt{ordered}$(S)$}: returns a deterministic total order over a set $S$ of messages.
  \item \textbf{\texttt{hash}$(T, r)$}: returns the identifier of the next round as a deterministic function of the delivered set $T$ and current round $r$.
@@ -17,57 +16,53 @@ We consider a set of processes communicating asynchronously over reliable point-
 \begin{algorithm}
  \caption{Atomic Broadcast with DenyList}
  \begin{algorithmic}[1]    
-    \State $\textit{proves} \gets \emptyset$
    \State $\textit{received} \gets \emptyset$
    \State $\textit{delivered} \gets \emptyset$
-    \State $\textit{window} \gets [\bot]^{f+1}$
    \State $r_1 \gets 0$

    \vspace{1em}
-    % --- AB-Broadcast ---
-    \State \nextalgline \textbf{AB-Broadcast}$_j(m)$
-    \State \nextalgline \hspace{1em} $\texttt{RB-Broadcast}_j(m)$
+    % --- A-Broadcast ---
+    \State \nextalgline \textbf{A-Broadcast}$_j(m)$
+    \State \nextalgline \hspace{1em} $\texttt{R-Broadcast}_j(m)$

    \vspace{1em}
-    % --- RB-delivered ---
-    \State \nextalgline \textbf{RB-delivered}$_j(m)$
+    % --- R-delivered ---
+    \State \nextalgline \textbf{R-Delivered}$_j(m)$
    \State \nextalgline \hspace{1em} $\textit{received} \gets \textit{received} \cup \{m\}$
    \State \nextalgline \hspace{1em} \textbf{repeat while} $\textit{received} \setminus \textit{delivered} \neq \emptyset$
    \State \nextalgline \hspace{2em} $S \gets \textit{received} \setminus \textit{delivered}$
-    \State \nextalgline \hspace{2em} $\texttt{RB-broadcast}(\texttt{PROP}, S, r_1, j)$
-    \State \nextalgline \hspace{2em} $\textit{proves} \gets \texttt{READ}()$
-    \State \nextalgline \hspace{2em} $\texttt{PROVE}[j](r_1)$
-    % \State \nextalgline \hspace{2em} $r_1 \gets \max\{r : j,\ (j, \texttt{PROVE}(r)) \in \textit{proves}\} + 1$
+    \State \nextalgline \hspace{2em} $\texttt{R-Broadcast}(\texttt{PROP}, S, r_1, j)$

    \vspace{0.5em}
-    \State \nextalgline \hspace{2em} $\texttt{APPEND}[j](r_1)$
-    \State \nextalgline \hspace{2em} $S \gets \{1, ..., n\}$
-    \State \nextalgline \hspace{2em} \textbf{repeat while} $|S| \leq n - f$
-    \State \nextalgline \hspace{3em} \textbf{forall} $i \in S$
-    \State \nextalgline \hspace{4em} \textbf{if} $\neg \texttt{PROVE}[i](r_1)$
-    \State \nextalgline \hspace{5em} $S \gets S \setminus i$
+    \State \nextalgline \hspace{2em} \textbf{wait until } $|\{j_1 : |\{i_1 : (i_1, \textit{PROVE}(<r_1, j_1>)) \in \texttt{READ}[i_1]()\}| \geq n - f\}| \geq n -f$
+    \State \nextalgline \hspace{2em} $\texttt{APPEND\_LINE}[j](r_1)$
+    \State \nextalgline \hspace{2em} $B[r_1] \gets {1, ..., n}$ 
+    \State \nextalgline \hspace{2em} \textbf{do}
+    \State \nextalgline \hspace{3em} \textbf{for each } $j_1 \in B[r_1]$
+    \State \nextalgline \hspace{4em} \textbf{if } $\nexists i_1 \text{ s.t. } \texttt{PROVE}[j_1](<r_1, i_1>) == \text{TRUE}$
+    \State \nextalgline \hspace{5em} $B[r_1] \gets B[r_1] \setminus \{j_1\}$
+    \State \nextalgline \hspace{2em} \textbf{while } $|B[r_1]| \geq f+1$
+    \State \nextalgline \hspace{2em} $\textit{winner}[r_1] \gets \{j_1 : |\{i_1 : (i_1, \textit{PROVE}(<r_1, j_1>)) \in \texttt{READ}[i_1]()\}| \geq n - f\}$

    \vspace{0.5em}
-    \State \nextalgline \hspace{2em} $\textit{winner}[r_1] \gets \texttt{READ\_ALL}()$
-    \State \nextalgline \hspace{2em} \textbf{wait } $\forall j \in \textit{winner}[r_1],\ |\textit{prop}[r_1][j] \neq \bot| \geq f+1$
-    \State \nextalgline \hspace{2em} $T \gets \bigcup_{j \in \textit{winner}[r_1]} \textit{prop}[r_1][j] \setminus \textit{delivered}$
-
-    \vspace{0.5em}
-    \State \nextalgline \hspace{2em} \textbf{for each } $m \in \texttt{ordered}(T)$
+    \State \nextalgline \hspace{2em} \textbf{wait } $\forall j \in \textit{winner}[r_1],\ \textit{prop}[r_1][j] \neq \bot$
+    \State \nextalgline \hspace{2em} $M \gets \bigcup_{j \in \textit{winner}[r_1]} \textit{prop}[r_1][j] \setminus \textit{delivered}$
+    \State \nextalgline \hspace{2em} \textbf{for each } $m \in \texttt{ordered}(M)$
    \State \nextalgline \hspace{3em} $\textit{delivered} \gets \textit{delivered} \cup \{m\}$
-    \State \nextalgline \hspace{3em} $\texttt{AB-deliver}_j(m)$
-    \State \nextalgline \hspace{2em} $r_1 \gets \textit{hash}(T, r_1)$
+    \State \nextalgline \hspace{3em} $\texttt{A-Delivered}_j(m)$
+    \State \nextalgline \hspace{2em} $r_1 \gets \textit{hash}(M, r_1)$

    \vspace{1em}
-    % --- READ_ALL() ---
-    \State \nextalgline \textbf{READ\_ALL}$(r)$
-    \State \nextalgline \hspace{1em} \textbf{for each } $j \in (1, ... , n)$
-    \State \nextalgline \hspace{2em} $win[j] \gets \{j_1: \texttt{READ}_{j_1}() \ni (j, \texttt{PROVE}(r))\}$
-    \State \nextalgline \hspace{1em} \textbf{for} $i \in (1, ... , n)$
-    \State \nextalgline \hspace{2em} \textbf{for} $j \in (1, ... , n)$
-    \State \nextalgline \hspace{3em} \textbf{if} $i \in win[j]$
-    \State \nextalgline \hspace{4em} $count[i] ++$
-    \State \nextalgline \hspace{1em} \textbf{return} $\{i: count[i] \geq n-f\}$
+    % --- R-Delivered ---
+    \State \nextalgline \textbf{R-Delivered}$_j(PROP, S, r, j_j)$
+    \State \nextalgline \hspace{1em} $\textit{prop}[r][j_j] \gets S$
+    \State \nextalgline \hspace{1em} \texttt{PROVE}$[j](<r, j_1>)$ 
+
+    \vspace{1em}
+    % --- APPEND_LINE() ---
+    \State \nextalgline \textbf{APPEND\_LINE}$_j(r)$
+    \State \nextalgline \hspace{1em} \textbf{for each } $i_1 \in (1, ... , n)$
+    \State \nextalgline \hspace{2em} \texttt{APPEND}$[j](<r, i_1>)$

  \end{algorithmic}  
 \end{algorithm}
--- a/Recherche/ALDLoverAB/intro/index.tex
+++ b/Recherche/ALDLoverAB/intro/index.tex
@@ -26,6 +26,8 @@ Messages are uniquely identifiable: two messages sent by distinct processes or a

 \subsubsection{Reliable Broadcast Properties}

+Here are the properties of the reliable broadcast primitive:\cite{attiyaDistributedComputingFundamentals2004}
+
 \begin{property}{Integrity}
  Every message received was previously sent. \\
  Formally : \\
@@ -38,12 +40,18 @@ Messages are uniquely identifiable: two messages sent by distinct processes or a
  $\forall m, \forall p_i: \text{bc-recv}_i(m) \text{ occurs at most once}$ \\
 \end{property}

-\begin{property}{Validity}
-  All messages broadcast by a correct process are eventually received by all non faulty processors. \\
+\begin{property}{Nonfaulty Liveness}
+  All messages broadcast by a nonfaulty processor is either received by all nonfaulty procssors. \\
  Formally : \\
  $\forall m, \forall p_i: \text{correct}(p_i) \wedge \text{bc-send}_i(m) => \forall p_j : \text{correct}(p_j) \Rightarrow \text{bc-recv}_j(m)$
 \end{property}

+\begin{property}{Faulty Liveness}
+  Every message sent by a faulty processor is either received by all nonfaulty processors or by none of them. \\
+  Formally : \\
+  $\forall m, \forall p_i: \neg\text{correct}(p_i) \wedge \text{bc-send}_i(m) \Rightarrow \forall p_j : \text{correct}(p_j) \Rightarrow \text{bc-recv}_j(m)$
+\end{property}
+
 \subsubsection{AtomicBroadcast Properties}

 \begin{property}{AB Totally ordered}
--- a/Recherche/ALDLoverAB/main.bcf
+++ b/Recherche/ALDLoverAB/main.bcf
--- a/Recherche/ALDLoverAB/main.pdf
+++ b/Recherche/ALDLoverAB/main.pdf
--- a/Recherche/ALDLoverAB/main.tex
+++ b/Recherche/ALDLoverAB/main.tex
@@ -44,6 +44,7 @@
 \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}}
@@ -84,7 +85,9 @@ We consider a static set of $n$ processes with known identities, communicating b

 \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,\PROVE(r)) \prec \APPEND(r) \,\}$, i.e., the set of processes whose $\PROVE(r)$ appears before the first $\APPEND(r)$ in the \DL{} linearization.
+\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.
+
+% For any round r ∈ R, define Winnersr ≜ { j ∈ Π | (j, prove(r)) ≺ APPEND(r) }. Pas bien on compare des tuples et des operations

 % ------------------------------------------------------------------------------
 \section{Primitives}
@@ -124,45 +127,65 @@ plus Integrity/No-duplicates/Validity (inherited from \RB and the construction).
 % ------------------------------------------------------------------------------

 \section{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}
+
+\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}
+
+\subsection{Variables}
 Each process $p_i$ maintains:
-\begin{itemize}[leftmargin=*]
-  \item $\received$ --- set of \RB-received messages not yet delivered;
-  \item $\delivered$ --- set of messages already delivered;
-  \item $\prop[r][j]$ --- proposal set announced by process $p_j$ for round $r$ (possibly $\bot$ locally);
-  \item Local view of \DL via \READ().
-  \item $next$ --- lowest round index not yet delivered.
-\end{itemize}
+
+%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$}
+\end{algorithmic}
+
+\paragraph{DenyList.} The \DL is initialized empty. We assume $\Pi_M = \Pi_V = \Pi$ (all processes can invoke \APPEND and \PROVE).

 \subsection{Handlers and Procedures}
+
 \renewcommand{\algletter}{A}
 \begin{algorithm}[H]
  \caption{\RB handler (at process $p_i$)}\label{alg:rb-handler}
  \begin{algorithmic}[1]
-    \State \textbf{on} $\RBreceived(m, S, r, j)$ \textbf{do}
-    \State $\received \leftarrow \received \cup \{m\}$
+    \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.
+% \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}
  \begin{algorithmic}[1]
-    \State \textbf{on} $\ABbroadcast(m, S, r, j)$ \textbf{do}
+    \Function{ABbroadcast}{$m$} 
      \State $P \leftarrow \READ()$ \Comment{Fetch latest \DL state to learn recent $\PROVE$ operations}
-    \State $r \leftarrow \max\{ r' : \exists j,\ (j,\PROVE(r')) \in P \}$ \Comment{Pick next open round: one past the most recent proved round}
+      \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$}
-    \State $\RBcast\big(m, S, r, \textit{self}\big)$ \Comment{Asynchronously disseminate proposal via \RB}
-    \State $\PROVE(r)$ \Comment{Attest participation in round $r$ while it is still open}
-    \State $\APPEND(r)$ \Comment{Close round $r$; freezes $\Winners_r$ in the \DL linearization}
-    \While{$\big(\nexists j : \exists r, (j, \PROVE(r)) \in P \wedge \ m \in \prop[r][j])$} \Comment{Wait until $m$ is included in some closed round and all needed proposals are known}
+
+      \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}
-      \State $\RBcast\big(m, S, r, \textit{self}\big)$
-      \State $\PROVE(r)$
-      \State $\APPEND(r)$
-    \EndWhile 
+        \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}

@@ -171,93 +194,208 @@ Each process $p_i$ maintains:
 \begin{algorithm}[H]
  \caption{\ABdeliver() at process $p_i$}\label{alg:delivery}
  \begin{algorithmic}[1]
-    \State \textbf{on} \ABdeliver() \textbf{do} \Comment{Called when the process wants to receive the next message}
+    %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{$\nexists j : (j,\PROVE(next)) \in P$} \Comment{No process has proved round $\textit{next}$}
-        \State \Return $\bot$ \Comment{No closed round ready for delivery}
+        \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)$ \Comment{Close round $\textit{next}$ if not already closed}
-      \If{$\PROVE(next) == FALSE$} \Comment{Process closed rounds strictly in order}
-        \State $P \leftarrow \READ()$ \Comment{Refresh local view of \DL}
-        \State $\Winners_{\textit{next}} \leftarrow \{ j : (j,\PROVE(\textit{next})) \in P \}$ \Comment{Frozen winners of round $\textit{next}$}
-        \If{$\forall j \in \Winners_{\textit{next}}:\ \prop[\textit{next}][j] \neq \bot$}
-          \State $M_{\textit{next}} \leftarrow \bigcup_{j \in \Winners_{\textit{next}}} \prop[\textit{next}][j]$ \Comment{Round-$\textit{next}$ message set}
-          \ForAll{$m \in \ordered(M_{\textit{next}})$} \Comment{Deterministic per-round order}
+        \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 $\delivered \leftarrow \delivered \cup \{m\}$
-              \State \Return $m$ \Comment{Deliver exactly one message per call}
+            \State $to\_deliver.push(m)$ \Comment{Append $m$ to the delivery queue}
          \EndIf
        \EndFor
-          \State $\textit{next} \leftarrow \textit{next} + 1$ \Comment{This round fully processed; advance}
-          \State \textbf{continue} \Comment{Try the next closed round (if any)}
-        \Else
-          \State \Return $\bot$ \Comment{Some winners' proposals not yet known via \RB}
+        \State $next \leftarrow next + 1$ \Comment{Advance to the next round}
      \EndIf
-      \EndIf
-      \State \Return $\bot$ \Comment{No closed round ready for delivery}
+      \State $m \leftarrow \text{to\_deliver.pop()}$
+      % \State $to\_deliver \leftarrow to\_deliver \setminus \{m\}$
+      \State $\delivered \leftarrow \delivered \cup \{m\}$
+      \State \textbf{return} $m$
+    \EndFunction
  \end{algorithmic}
 \end{algorithm}
 % ------------------------------------------------------------------------------
 \section{Correctness}
-
-\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}
+%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 unique linearization point $t_0$ of $\APPEND(r)$ in the \DL, and from that point on, no $\PROVE(r)$ can be valid.
+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 definition of 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{lemma}[Across rounds]\label{lem:across}
-Rounds are delivered in strictly increasing $r$. Concatenating the per-round sequences yields a single global total order.
-Equivalently, $\forall r_1,r_2$ such that $r_1, r_2$ are closed and $r_1 < r_2$, all round $r$ such that $r_1 < r < r_2$ are also closed.
+If there exists a $r$ such that $r$ is closed, $\forall r'$ such that $r' < r$, r' is also closed.
 \end{lemma}

-\begin{lemma}[Well-defined winners]\label{lem:winners}
-In any execution, whenever some process computes $\Winners_r$, its current \DL-view contains $\APPEND(r)$; hence $\Winners_r$ is computed only for closed round.
+\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.
+  
+  \paragraph{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.
+  
+  \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.
+  
+  \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(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 $(j,\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(k+1)$ at B6 in a second iteration. \\
+  If round $k$ wasn't closed when $p_1$ execute $\PROVE(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(r+1)$. In this case $k$ is closed.
+  
+  \paragraph{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. 
+  Hence $\APPEND^\star(k+1)$ implies a prior $\APPEND(k)$ in $H$, so $k$ is closed.
+  
+  \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}
+  Let take a closed round $r$ (which implies by \Cref{def:closed-round} that some $\APPEND(r)$ occurs in the DL linearization $H$), there exist a unique and defined set of winners such as 
+  \[
+    \Winners_r = \{ j : (j,\PROVEtrace(r)) \prec \APPEND^\star(r) \}
+  \] 
+  with $\APPEND^\star(r)$ being the earliest \APPEND$(r)$ in the \DL linearization.
+\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}
+  Fix a round $r$ such that some $\APPEND(r)$ occurs; hence $r$ is \emph{closed}. By \Cref{lem:closure-stable}, 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}
+In any execution, when a process computes $W_{r}$, $r$ is closed. 
+\end{lemma}
+
+\begin{proof}
+  Fix a process $p$ that reaches line C10 (computing $W_{\textit{next}}$). Immediately before C10, line C9 executes
+  \[
+  \APPEND(\textit{next});\; P \gets \READ()
+  \]
+  
+  Line C9 is guarded by the condition at line C6, which 
+\end{proof}
+
 \begin{lemma}[View-Invariant Winners]\label{lem:view-invariant}
 For any closed round $r$, there exists a unique set
 \[
-    \Winners_r = \{ j : (j,\PROVE(r)) \prec \APPEND^\star(r) \}
+    \Winners_r = \{ j : (j,\PROVEtrace(r)) \prec \APPEND^\star(r) \}
 \]
-with $\APPEND^\star(r)$ being the earliest \APPEND$(r)$ in the \DL linearization.
+with $\APPEND^\star(r)$ being the earliest \APPEND$(r)$ in the \DL linearization.\\
+Such that for any correct process $p$ that computes $W_r$, $W_r = \Winners_r$.
 \end{lemma}

 \begin{proof}[Proof]
-    We admit that some $\APPEND(r)$ occurs; if $\APPEND(r)$ occurs then it exists an operation $\APPEND^\star(r)$ that is the earliest in the linearization.
+  Fix a round $r$ such that some $\APPEND(r)$ occurs; hence $r$ is \emph{closed}. By \Cref{lem:closure-stable}, there exists a unique earliest $\APPEND(r)$ in the DL linearization, denoted $\APPEND^\star(r)$.

-    Due to the validity property of DL, a $\PROVE(r)$ is valid iff $\PROVE(r) \prec \APPEND^\star(r)$. Thus, 
-    \[\Winners_r \triangleq \{ j : (j,\PROVE(r)) \prec \APPEND^\star(r) \}\]
+  Consider any correct process $p$ that computes $W_r$ at line C10. By \Cref{lem:winners}, $r$ is closed when $p$ computes $W_r$. By \Cref{lem:closure-stable}, the linearization point of $\APPEND^\star(r)$ precedes that of the subsequent $\READ()$ at C9, therefore the $P$ returned by this $\READ()$ is posterior to $\APPEND^\star(r)$ in the DL linearization.

-    Let's consider two correct processes $p_i$ and $p_j$ and two \READ{} responses $P_i$ and $P_j$ such that 
+  Hence, at the moment C10 computes
  \[
-    \APPEND^\star(r) \prec (i,\PROVE(r)) \prec P_i
-    \APPEND^\star(r) \prec (j,\PROVE(r)) \prec P_j
+    W_r \;\leftarrow\; \{\, j : (j,\PROVEtrace(r)) \in P \,\},
  \]
-    By the \DL interface, \READ{} returns a permutation of the valid operations observed so far, and hence every $\PROVE(r)$ that precedes $\APPEND^\star(r)$ is valid while any $\PROVE(r)$ that follows $\APPEND^\star(r)$ is invalid. We ensures that
-    \[\{ j : (j,\PROVE(r)) \in P_i \} = \{ j : (j,\PROVE(r)) \in P_j \} = \Winners_r.\]
+  the view $P$ is posterior to $\APPEND^\star(r)$, so
+  \[
+    W_r = \{\, j : (j,\PROVEtrace(r)) \prec \APPEND^\star(r) \,\} = \Winners_r.
+  \]
+  
+  Since this argument holds for any correct process computing $W_r$, all correct processes compute the same winner set $\Winners_r$ for closed round $r$.
+\end{proof}
+
+\begin{lemma}[No APPEND without PROVE]\label{lem:append-prove}
+If some correct process invokes $\APPEND(r)$, then some correct process must have previously invoked $\PROVE(r)$.
+\end{lemma}
+
+\begin{proof}[Proof]
+  Consider the round $r$ such that some correct process invokes $\APPEND(r)$. There are two possible cases
+  
+  \paragraph{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(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)$.
+
+  \paragraph{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)$.
+
+  In both cases, if some correct process invokes $\APPEND(r)$, then some correct process must have previously invoked $\PROVE(r)$.
 \end{proof}

 \begin{lemma}[No empty winners]\label{lem:nonempty}
-For any round $r$ closed, $\Winners_r \neq \emptyset$.
+For any correct process that computes $W_r$, $W_r \neq \emptyset$.
 \end{lemma}

 \begin{proof}[Proof]
-    Assume some correct process invokes \APPEND$(r)$. Hence an \APPEND$(r)$ occurs, and there exists an operation $\APPEND^\star(r)$ that is earliest in the \DL linearization.
+  By \Cref{lem:winners}, any correct process that computes $W_r$ implies that round $r$ is closed. By \Cref{lem:closure-stable}, there exists a unique earliest $\APPEND(r)$ in the DL linearization, denoted $\APPEND^\star(r)$.

-    Let $p_k$ be the issuer of $\APPEND^\star(r)$. By the algorithm (\ABbroadcast), any process that issues \APPEND$(r)$ (B6) must have previously invoked \PROVE$(r)$ (B5) in its program order. Because the \DL is linearizable and preserves per-process program order in the linearization, we obtain
+  By \Cref{lem:view-invariant}, any correct process computing $W_r$ obtains
  \[
-       (k,\PROVE(r)) \prec \APPEND^\star(r).
+    W_r = \Winners_r = \{\, j : (j,\PROVEtrace(r)) \prec \APPEND^\star(r) \,\}.
  \]
-    Consequently, $(k,\PROVE(r))$ is a \emph{valid} attestation for round $r$ (no prior \APPEND$(r)$ exists before $\APPEND^\star(r)$ by definition of $\APPEND^\star(r)$). By the definition of $\Winners_r$,
+
+  So
  \[
-       k \in \Winners_r.
+    W_r \neq \emptyset \implies \exists j : (j,\PROVEtrace(r)) \prec \APPEND^\star(r).
  \]
-    Therefore $\Winners_r \neq \emptyset$, i.e., $|\Winners_r|>0$.
+
+  Consider any correct process $p$ that computes $W_k$ at line C10. We show that $k$ is closed when $p$ executed the $\READ$ operation at C9 by \Cref{lem:winners}. This implies that some process must have invoked $\APPEND(k)$, which by \Cref{lem:append-prove} implies that some correct process must have previously invoked $\PROVE(k)$. Hence there exists at least one $j$ such that $(j,\PROVEtrace(k)) \prec \APPEND^\star(k)$, so $W_k \neq \emptyset$.
+\end{proof}
+
+\begin{lemma}[Eventual proposal closure]\label{lem:eventual-closure}
+  For any correct process $p_i$ that computes $M_r$ for round $r$, there exist no $j$ such that $j \in \Winners_r$ and $\prop^{(i)}[r][j] = \bot$.
+\end{lemma}
+
+\begin{proof}[Proof]
+  Fix a correct process $p_i$ that computes $M_r$ at line C14. By \Cref{lem:winners}, $r$ is closed when $p_i$ executed the $\READ$ operation at C9. By \Cref{lem:view-invariant}, $p_i$ computes the unique winner set $\Winners_r$.
+
+  By \Cref{lem:nonempty}, $\Winners_r \neq \emptyset$. Consider any $j \in \Winners_r$. Since $j$ is a winner, by definition of $\Winners_r$, $j$ must have invoked a valid $\PROVE(r)$ before the earliest $\APPEND(r)$ in the DL linearization. Since $j$ is correct and by program order, if he invoked a valid $\PROVE(r)$ he must have invoked $\RBcast(S^{(j)}, r, j)$ directly before. 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 (A3). The instruction 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[r][j]$, we have $\prop[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 $j$, $j$ invokes at most one $\RBcast(S, r, j)$.
+\end{lemma}
+
+\begin{proof}[Proof]
+  By program order, any process $j$ invokes $\RBcast(S, r, j)$ 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 line B5. Hence, in any execution, any process $j$ invokes $\RBcast(S, r, j)$ at most once for any round $r$.
 \end{proof}

 \begin{lemma}[Proposal convergence]\label{lem:convergence}
@@ -265,48 +403,94 @@ For any closed round $r$, after all \RB messages from $\Winners_r$ are received,
 \end{lemma}

 \begin{proof}[Proof]
-    Fix a round $r$ such that some $\APPEND(r)$ occurs; hence $r$ is \emph{closed}. By \Cref{lem:winners}, all correct processes that observe $\READ()$ after $\APPEND^\star(r)$ compute the same winner set $\Winners_r$.
-    
-    For any $j \in \Winners_r$, in process $p_j$'s program order we have, for round $r$:
+  Fix a closed round $r$. By \Cref{lem:view-invariant}, any correct process computing $W_r$ obtains the same winner set $\Winners_r$. By \Cref{lem:eventual-closure}, every correct process that computes $M_r$ has received all \RB messages from every winner $j \in \Winners_r$, so $\prop[r][j]$ is non-$\bot$ for all $j \in \Winners_r$. By \Cref{lem:unique-proposal}, each winner $j$ invokes at most one $\RBcast(S^{(j)}, r, j)$, so $\prop[r][j] = S^{(j)}$ is uniquely defined. Hence, every correct process computes the same
  \[
-      \RBcast(\_, S_j, r, j) \ \text{(B4)} \quad\text{before}\quad \PROVE(r) \ \text{(B5)} \quad\text{before}\quad \APPEND(r) \ \text{(B6)}.
+    M_r = \bigcup_{j\in\Winners_r} \prop[r][j] = \bigcup_{j\in\Winners_r} S^{(j)}.
  \]
-    Since $\Winners_r = \{\, j : (j,\PROVE(r)) \prec \APPEND^\star(r) \,\}$, each winner $j$ executed (B4) before $\APPEND^\star(r)$, thereby broadcasting a \RB message for $(r,j)$ with some (uniquely determined) payload $S_j$.
-    
-    The round chosen at (B2) is the next open round. After (B6) closes $r$, any later invocation of \ABbroadcast\ by $p_j$ picks a strictly larger round. Thus $p_j$ executes at most one $\RBcast(\_,\cdot,r,j)$, so the set $S_j$ attached to $(r,j)$ is unique.
-    
-    Now consider any two correct processes $p_a$ and $p_b$ that have (via \RB) received all winners' messages for round $r$. By the \RB \emph{Integrity} and \emph{No-duplicates} properties, every delivery of $p_j$'s \RB message for $(r,j)$ carries the same $S_j$, and the handler sets
-    \[
-      \prop[r][j] \leftarrow S_j \text{ (A3)}
-    \]
-    at both $p_a$ and $p_b$. Therefore,
-    \[
-      M_r^{(a)} \triangleq \bigcup_{j\in\Winners_r} \prop^{(a)}[r][j]
-      \;=\; \bigcup_{j\in\Winners_r} S_j
-      \;=\; \bigcup_{j\in\Winners_r} \prop^{(b)}[r][j]
-      \triangleq M_r^{(b)}.
-    \]
-    Hence, after all \RB messages from $\Winners_r$ have been received, every correct process computes the same $M_r$. 
 \end{proof}

-\begin{lemma}[Per-round determinism]\label{lem:per-round}
-Given \Cref{lem:convergence}, all correct processes iterate $\ordered(M_r)$ in the same order; hence the delivery order inside round $r$ is identical at all correct processes.
+\begin{lemma}[Broadcast Termination]\label{lem:bcast-termination}
+  If a correct process $p$ invokes $\ABbroadcast(m)$, then $p$ eventually quit the function and returns.
 \end{lemma}

+\begin{proof}[Proof]
+  Fix a correct process $p$ that invokes $\ABbroadcast(m)$. The lemma is true iff $(i, \PROVEtrace(r)) \in P$ or $\exists j, r': (j, \PROVEtrace(r')) \in P \wedge m \in \prop[r'][j]$ (like guarded at B8).
+
+  \begin{itemize}
+    \item \textbf{Case 1:} there exists a round $r$ such that $p$ invokes $\PROVE(r)$ and this $\PROVE(r)$ is valid. Hence eventually $(i, \PROVEtrace(r)) \in P$ and $p$ exits the loop at B8.
+    \item \textbf{Case 2:} there exists no round $r$ such that $p$ invokes $\PROVE(r)$ and this $\PROVE(r)$ is valid. In this case $p$ 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 \Cref{lem:nonempty} that for every possible round $r$ there at least one winner. Because there is an infinite number of rounds, and a finite number of processes, there exists at least one correct process $j$ that invokes infinitely many valid $\PROVE(r)$ and by extension infinitely many $\ABbroadcast(\_)$. By \RB \emph{Validity}, $j$ eventually receives $p$ 's \RB messages. Let call $t$ the time when $j$ receives $p$ 's \RB message \\
+    For the first invocation of $\ABbroadcast(m)$ by $j$ after $t$, $j$ must include $m$ in his proposal $S$ at B4 for round $r'$ (because $m$ is pending in $j$ 's $\received \setminus \delivered$). Because $j \in \Winners_{r'}$ and by \RB \emph{Validity}, every correct process eventually receives $j$ 's \RB message for round $r'$, including $p$. When $p$ receives $j$ 's \RB message, $\prop[r'][j]$ is set to a non-$\bot$ value (A3) which includes $m$. Hence eventually $\exists j, r': (j, \PROVEtrace(r')) \in P \wedge m \in \prop[r'][j]$ and $p$ exits the loop at B8.
+  \end{itemize}
+  The first case explicit the case where $p$ 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$ eventually exits the loop and returns from $\ABbroadcast(m)$.
+\end{proof}
  
-\begin{corollary}[No duplicates]
-Each message is delivered at most once since membership in $\delivered$ is tested before delivery.
-\end{corollary}

 \begin{lemma}[Inclusion]\label{lem:inclusion}
-If some process invokes $\ABbroadcast(m)$, then there exist a (closed) round $r$ and a process
-$j\in\Winners_r$ such that $j$ invokes
+If some correct process invokes $\ABbroadcast(m)$, then there exist a (closed) round $r$ and a corrcet process $j\in\Winners_r$ such that $j$ invokes
 \[
-\RBcast(\_, S, r, j)\quad\text{with}\quad m\in S.
+\RBcast(S, r, j)\quad\text{with}\quad m\in S.
 \]
-Equivalently, every $\ABbroadcast(m)$ is included in the proposal of some winner of some closed round.
 \end{lemma}

+\begin{proof}
+  Fix a correct process $p$ that invokes $\ABbroadcast(m)$. By \Cref{lem:bcast-termination}, $p$ eventually exits the loop (B5–B11) at some round $r$. There are two possible cases.
+
+  \paragraph{Case 1:} $p$ exits the loop because $(i, \PROVEtrace(r)) \in P$. In this case, $p$ is a winner in round $r$ by definition of $\Winners_r$. By program order, $p$ must have invoked $\RBcast(S, r, i)$ at B6 before invoking $\PROVE(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$.
+
+  \paragraph{Case 2:} $p$ exits the loop because $\exists j, r': (j, \PROVEtrace(r')) \in P \wedge m \in \prop[r'][j]$. In this case, by \Cref{lem:view-invariant}, any correct process computing $W_{r'}$ obtains the unique winner set $\Winners_{r'}$, so $j\in\Winners_{r'}$. By program order, $j$ must have invoked $\RBcast(S, r', j)$ at B6 before invoking $\PROVE(r')$ at B7. By line B4, $m \in S$. Hence there exist a closed round $r'=r$ and a correct process $j\in\Winners_{r'}$ such that $j$ invokes $\RBcast(S, r', j)$ with $m\in S$.
+
+  In both cases, if some correct process invokes $\ABbroadcast(m)$, then there exist a (closed) 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{proof}[Proof]
+  % 2 cas, p_i est winner et cest gagné.
+  % Si p_i n'est pas winner on fait par l'absurde comme quoi personne ne propose m. Et on montre que c'est impossible.
+
+  % S est modif a chaque iteration de la boucle. On montre que y a un plus petit S bloqué
+
+  % Pour sortir de la boucle on doit avoir A ou B vrai, et il faut montrer que non A implique B
+% \end{proof}
+
+\begin{lemma}[Validity]\label{lem:validity}
+  If a correct process $p$ invokes $\ABbroadcast(m)$, then every correct process who eventually invokes $\ABdeliver()$ delivers $m$.
+\end{lemma}
+
+\begin{proof}[Proof]
+  Fix a correct process $p$ that invokes $\ABbroadcast(m)$. By \Cref{lem:inclusion}, there exist a closed 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.
+  \]
+
+  Consider any correct process $q$ that eventually invokes $\ABdeliver()$. By \Cref{lem:eventual-closure}, when $q$ computes $M_r$ at line C14, $\prop[r][j]$ is non-$\bot$ because $j \in \Winners_r$. By \Cref{lem:unique-proposal}, $j$ invokes at most one $\RBcast(S, r, j)$, so $\prop[r][j] = S$ is uniquely defined. Hence, when $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, when $q$ eventually invokes $\ABdeliver()$, it eventually delivers $m$.
+\end{proof}
+
+\begin{lemma}[Total Order]\label{lem:total-order}
+  For any two messages $m_1$ and $m_2$ broadcast by correct processes such that $m_1$ is broadcast before $m_2$, any correct process $p_j$ that delivers both $m_1$ and $m_2$ delivers $m_1$ before $m_2$.
+\end{lemma}
+
+\begin{proof}[Proof]
+  Fix two messages $m_1$ and $m_2$ broadcast by correct processes. Consider any correct process $p_i$ that delivers $m_1$ before $m_2$. By program order, $p_i$ must have invoked $\ABbroadcast(m_1)$ before $\ABbroadcast(m_2)$. Let $r_1$ and $r_2$ be the rounds at which $p_i$ exits the loop (B5–B11) when invoking $\ABbroadcast(m_1)$ and $\ABbroadcast(m_2)$ respectively. By program order, $r_1 < r_2$.
+
+  Consider any correct process $p_j$ 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.
+  \]
+
+  By program order, $p_i$ must have waited for the loop (B5–B11) to exit at round $r_1$ before invoking $\ABbroadcast(m_2)$. Hence, $r_1 \leq r'_1 < r_2 \leq r'_2$, so $r'_1 < r'_2$. Because $p_j$ delivers messages in round order (C5–C20), $p_j$ delivers all messages from round $r'_1$ (including $m_1$) before delivering any message from round $r'_2$ (including $m_2$). Therefore, $p_j$ delivers $m_1$ before $m_2$.
+\end{proof}
+
 \begin{theorem}[\ARB]
 Under the assumed \DL synchrony and \RB reliability, the algorithm implements Atomic Reliable Broadcast.
 \end{theorem}
--- a/Recherche/ALDLoverAB/proof/index.tex
+++ b/Recherche/ALDLoverAB/proof/index.tex
@@ -1,3 +1,38 @@
+We define $W^t$ as the set of processes that are winners in round $r$ at time $t$.
+
+\begin{theorem}
+    $\forall j_1, j_2 \text{ corrects}, W_{j_1} = W_{j_2}$, where $W_j$ is the set of processes that are winners in round $r$.
+\end{theorem}
+
+\begin{proof}
+    \begin{align*}
+        J = \{j_1, ..., j_n\} & \text{(set of all processes)} \\
+        B \subseteq J, B = \{b_1, ..., b_f\} & \text{(set of faulty processes)} \\
+        C \subseteq J, C = \{c_1, ..., c_{n-f}\} & \text{(set of correct processes)} \\
+        \textbf{Let's assume } \exists b_1 \in B, \exists t_0 & \text{ such that } \texttt{R-Broadcast}_{b_1}(PROP, S, r, b_1) \text{ occurs} \\
+        \Rightarrow\; & \exists K^{t_0} \subseteq C \text{ such that } \forall k \in K^{t_0}, \texttt{R-Delivered}_k(PROP, S, r, b_1) \text{ occurs} \\
+        & \wedge |K^{t_0}| = n - 2f \\
+        \Rightarrow\; & \texttt{PROVE}_k[k](<r, b_1>) \text{ is valid for all } k \in K^{t_0} \\
+        \Rightarrow\; & b_1 \not\in W^{t_0} \text{ since } \texttt{PROVE}_k[k](<r, b_1>) \text{ is valid less than } n - f \text{ times} \\
+        \text{in the same way,} & \\
+        \textbf{Let's assume } \exists L^{t_0} \subseteq C \text{ such that } & \forall l \in L^{t_0}, \texttt{R-Broadcast}_{l}(PROP, \_, r, l) \text{ occurs} \\
+        \textbf{And } \exists M^{t_0} \subseteq C \text{ such that } & \forall m \in M^{t_0}, \texttt{R-Delivered}_m(PROP, \_, r, m) \text{ occurs} \\
+        & \text{with } |L^{t_0}| = n - f \text{ and } |M^{t_0}| = n - f \\
+        \Rightarrow\; & \forall m, l : \exists (m, PROVE(<r, l>)) \in \texttt{READ}[m]() \\
+        & \textbf{And because } |M^{t_0}| \geq n - f \\
+        \Rightarrow\; & \exists O^{t_0} \subseteq M^{t_0} \text{ such that } \forall o \in O^{t_0}, W^{t_0}_o \not\ni b_1 \\
+        & \exists t_1 \geq t_0 : \forall b \in B, \texttt{PROVE}_b[b](<r, b_1>) \text{ occurs} \\
+        \Rightarrow\; & \textbf{at time } t_1, \forall k \in K : \exists (k, \texttt{PROVE}(<r, b_1>)) \in \texttt{READ}[k]() \\
+        & \textbf{And } \forall b \in B, \exists (b, \texttt{PROVE}(<r, b_1>)) \in \texttt{READ}[b]() \\
+        \Rightarrow\; & \textbf{Because } |K| + |B| = n - 2f + f = n - f \text{ the condition is satisfied} \\
+        \Rightarrow\; & W^{t_1} \ni b_1 \\
+    \end{align*}
+\end{proof}
+
+\begin{theorem}
+    % $\exist j \text{ correct } W^{t_0}$
+\end{theorem}
+
 \begin{theorem}[Integrity]
    If a message $m$ is delivered by any process, then it was previously broadcast by some process via the \texttt{AB-broadcast} primitive.
 \end{theorem}
--- a/Recherche/ALDLoverAB/sources.bib
+++ b/Recherche/ALDLoverAB/sources.bib
@@ -0,0 +1,14 @@
+@book{attiyaDistributedComputingFundamentals2004,
+  title = {Distributed {{Computing}}: {{Fundamentals}}, {{Simulations}}, and {{Advanced Topics}}},
+  shorttitle = {Distributed {{Computing}}},
+  author = {Attiya, Hagit and Welch, Jennifer},
+  date = {2004-03-25},
+  eprint = {3xfhhRjLUJEC},
+  eprinttype = {googlebooks},
+  publisher = {John Wiley \& Sons},
+  abstract = {* Comprehensive introduction to the fundamental results in the mathematical foundations of distributed computing * Accompanied by supporting material, such as lecture notes and solutions for selected exercises * Each chapter ends with bibliographical notes and a set of exercises * Covers the fundamental models, issues and techniques, and features some of the more advanced topics},
+  isbn = {978-0-471-45324-6},
+  langid = {english},
+  pagetotal = {440},
+  keywords = {Computers / Computer Engineering,Computers / Computer Science,Computers / Networking / General}
+}
--- a/Recherche/yaoLatticeAgreement/main.pdf
+++ b/Recherche/yaoLatticeAgreement/main.pdf
--- a/Recherche/yaoLatticeAgreement/main.tex
+++ b/Recherche/yaoLatticeAgreement/main.tex
@@ -0,0 +1,105 @@
+\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}
+% 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}
+\usepackage{xspace}
+
+\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{\send}{\textsf{send}}
+\newcommand{\recv}{\textsf{recv}}
+\newcommand{\hash}{\textsf{hash}}
+\newcommand{\procQueue}{\textsf{processQueue}}
+\newcommand{\RBcast}{\textsf{RB-cast}}
+\newcommand{\RBreceived}{\textsf{RB-received}}
+
+\newcommand{\queue}{\mathsf{queue}}
+
+\crefname{theorem}{Theorem}{Theorems}
+\crefname{lemma}{Lemma}{Lemmas}
+\crefname{definition}{Definition}{Definitions}
+\crefname{algorithm}{Algorithm}{Algorithms}
+
+% \title{Upgrading Reliable Broadcast to Atomic Reliable Broadcast with a DenyList Primitive}
+\date{\vspace{-1ex}}
+
+\begin{document}
+% \maketitle
+
+\section*{Algorithm}
+
+\renewcommand{\algletter}{A}
+\begin{algorithm}
+  \begin{algorithmic}[1]    
+    \Function{send}{m} 
+      \State \RBcast$(self, m, \hash(H))$
+    \EndFunction
+    \vspace{1em}
+
+    \Function{\RBreceived}{$j, m, h$} 
+    \State $\queue[j] \gets \queue[j].push(\{(m, h)\})$
+      \If{$|\queue[j]| = 1$} \Comment{If this is the first message in the queue, process it}
+        \State \procQueue()
+      \EndIf
+    \EndFunction
+    \vspace{1em}
+
+    \Function{processQueue}{}
+      \For{$j$ such that $\queue[j] \neq \emptyset$}
+        \State $\{(m, h)\} \gets \queue[j].pop()$
+          % \If{$m$ is a singleton}
+          %   \State $H \gets H \cup \{m\}$; \recv$(m)$; $\queue[j] \gets \queue[j] \setminus \{(m, h)\}$
+          % \ElsIf{$\exists A : A \subseteq H\ \wedge\ \hash(A) = h$}
+          %   \State $H \gets H \cup \{m\}$; \recv$(m)$; $\queue[j] \gets \queue[j] \setminus \{(m, h)\}$
+          % \Else
+          %   \State \textbf{break}
+          % \EndIf
+        \If{$\exists A : A \subseteq H\ \wedge\ \hash(A) = h$}
+          \State $H \gets H \cup \{m\}$; \recv$(m)$; $\queue[j] \gets \queue[j] \setminus \{(m, h)\}$
+          \State \procQueue();
+          \Return;
+        \EndIf
+      \EndFor
+    \EndFunction
+  \end{algorithmic}
+\end{algorithm}
+
+% \bibliographystyle{plain}
+% \begin{thebibliography}{9}
+% % (left intentionally blank)
+% \end{thebibliography}
+
+\end{document}