big refactoring in the ARB <=> RB+DL in crash model

.devcontainer/devcontainer.json

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

.devcontainer/install-tools.sh

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

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$
-    
-    \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} $\texttt{R-Broadcast}(\texttt{PROP}, S, r_1, j)$
 
     \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}$
+    \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} \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}

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}

Recherche/ALDLoverAB/main.tex

@@ -40,10 +40,12 @@
 \newtheorem{remark}{Remark}
 
 \newcommand{\RB}{\textsf{RB}\xspace}
+\newcommand{\res}{\mathsf{res}}
 \newcommand{\ARB}{\textsf{ARB}\xspace}
 \newcommand{\DL}{\textsf{DL}\xspace}
 \newcommand{\APPEND}{\textsf{APPEND}}
 \newcommand{\PROVE}{\textsf{PROVE}}
+\newcommand{\PROVEtrace}{\textsf{prove}}
 \newcommand{\READ}{\textsf{READ}}
 \newcommand{\ABbroadcast}{\textsf{AB-broadcast}}
 \newcommand{\ABdeliver}{\textsf{AB-deliver}}
@@ -51,11 +53,15 @@
 \newcommand{\RBreceived}{\textsf{RB-received}}
 \newcommand{\ordered}{\textsf{ordered}}
 \newcommand{\Winners}{\mathsf{Winners}}
+\newcommand{\Messages}{\mathsf{Messages}}
 \newcommand{\ABlisten}{\textsf{AB-listen}}
 
 \newcommand{\delivered}{\mathsf{delivered}}
 \newcommand{\received}{\mathsf{received}}
 \newcommand{\prop}{\mathsf{prop}}
+\newcommand{\current}{\mathsf{current}}
+
+\newcommand{\Seq}{\mathsf{Seq}}
 
 \crefname{theorem}{Theorem}{Theorems}
 \crefname{lemma}{Lemma}{Lemmas}
@@ -84,7 +90,8 @@ 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.
+We denoted by $\PROVE^{(j)}(r)$ or $\APPEND^{(j)}(r)$ the operation $\PROVE(r)$ or $\APPEND(r)$ invoked by process $j$.
 
 % ------------------------------------------------------------------------------
 \section{Primitives}
@@ -98,21 +105,28 @@ We consider a static set of $n$ processes with known identities, communicating b
 \end{itemize}
 
 \subsection{DenyList (DL)}
-The \DL is a \emph{shared, append-only} object that records attestations about opaque application-level tokens. It exposes the following operations:
-\begin{itemize}[leftmargin=*]
-  \item \APPEND$(x)$
-  \item \PROVE$(x)$: issue an attestation for token $x$; this operation is \emph{valid} (return true) only if no \APPEND$(x)$ occurs earlier in the \DL linearization. Otherwise, it is invalid (return false).
-  \item \READ$()$: return a (permutation of the) valid operations observed so far; subsequent reads are monotone (contain supersets of previously observed valid operations).
+We assume a synchronous DenyList (\DL) object with the following properties.
+
+The DenyList object type supports three operations: $\APPEND$, $\PROVE$, and $\READ$. These operations appear as if executed in a sequence $\Seq$ such that:
+\begin{itemize}
+  \item \textbf{Termination.} A $\PROVE$, an $\APPEND$, or a $\READ$ operation invoked by a correct process always returns.
+  \item \textbf{APPEND Validity.} The invocation of $\APPEND(x)$ by a process $p$ is valid if:
+  \begin{itemize}
+    \item $p \in \Pi_M \subseteq \Pi$; \textbf{and}
+    \item $x \in S$, where $S$ is a predefined set. 
+  \end{itemize} 
+  Otherwise, the operation is invalid.
+  \item \textbf{PROVE Validity.} If the invocation of a $op = \PROVE(x)$ by a correct process $p$ is not valid, then:  
+  \begin{itemize}
+    \item $p \not\in \Pi_V \subseteq \Pi$; \textbf{or}
+    \item A valid $\APPEND(x)$ appears before $op$ in $\Seq$. 
+  \end{itemize}
+  Otherwise, the operation is valid.
+  \item \textbf{PROVE Anti-Flickering.} If the invocation of a operation $op = \PROVE(x)$ by a correct process $p \in \Pi_V$ is invalid, then any $\PROVE(x)$ operation that appears after $op$ in $\Seq$ is invalid.
+  \item \textbf{READ Validity.} The invocation of $op = \READ()$ by a process $p \in \pi_V$ returns the list of valid invocations of $\PROVE$ that appears before $op$ in $\Seq$ along with the names of the processes that invoked each operation. 
+  \item \textbf{Anonymity.} Let us assume the process $p$ invokes a $\PROVE(v)$ operation. If the process $p'$ invokes a $\READ()$ operation, then $p'$ cannot learn the value $v$ unless $p$ leaks additional information.
 \end{itemize}
 
-\paragraph{Validity.} \APPEND$(x)$ is valid iff the issuer is authorized (in $\Pi_M$) and $x$ belongs to the application-defined domain $S$. \PROVE$(x)$ is valid iff the issuer is authorized (in $\Pi_V$) and there is no earlier \APPEND$(x)$ in the \DL linearization.
-
-\paragraph{Progress.} If a correct process invokes \APPEND$(x)$, then eventually all correct processes will be unable to issue a valid \PROVE$(x)$, and \READ{} at all correct processes will (eventually) reflect that \APPEND$(x)$ has been recorded.
-
-\paragraph{Termination.} Every operation invoked by a correct process eventually returns.
-
-\paragraph{Interface and Semantics.} The \DL provides a single global linearization of operations consistent with each process's program order. \READ{} is prefix-monotone; concurrent updates become visible to all correct processes within bounded time (by synchrony). Duplicate requests may be idempotently coalesced by the implementation.
-
 % ------------------------------------------------------------------------------
 \section{Target Abstraction: Atomic Reliable Broadcast (ARB)}
 Processes export \ABbroadcast$(m)$ and \ABdeliver$(m)$. \ARB requires total order:
@@ -124,196 +138,486 @@ 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}
+
+\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$}
+  \State $\current \gets 0$
+\end{algorithmic}
+
+\paragraph{DenyList.} The \DL is initialized empty. We assume $\Pi_M = \Pi_V = \Pi$ (all processes can invoke \APPEND and \PROVE).
 
 \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\}$
-    \State $\prop[r][j] \leftarrow S$ \Comment{Record sender $j$'s proposal $S$ for round $r$}
+    \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.
 
 \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}
-    \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 $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}
-      \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 
+    \Function{ABbroadcast}{$m$} 
+      \State $P \leftarrow \READ()$ \Comment{Fetch latest \DL state to learn recent $\PROVE$ operations}
+      \State $r_{max} \leftarrow \max(\{ r' : \exists j,\ (j,\PROVE(r')) \in P \})$ \Comment{Pick current open round}
+      \State $S \leftarrow (\received \setminus \delivered) \cup \{m\}$ \Comment{Propose all pending messages plus the new $m$}
+
+      \vspace{1em}
+
+      \For{\textbf{each}\ $r \in \{r_{max}, r_{max}+1, \cdots \}$} 
+        \State $\RBcast(S, r, i)$; $\PROVE(r)$; $\APPEND(r)$;
+        \State $P \leftarrow \READ()$ \Comment{Refresh local view of \DL}
+        \If{($\big((i, \PROVEtrace(r)) \in P\ \vee\ (\exists j, r': (j, \PROVEtrace(r')) \in P \wedge \ m \in \prop[r'][j]))$)} 
+          \State \textbf{break} \Comment{Exit loop once $m$ is included in some closed round}
+        \EndIf
+      \EndFor
+    \EndFunction
   \end{algorithmic}
 \end{algorithm}
 
-% \paragraph{} TODO
 \renewcommand{\algletter}{C}
 \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}
-      \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}
+    \Function{ABdeliver}{}
+      \State $r \gets \current$
+      \State $P \gets \READ()$ 
+      \If{$\forall j : (j, \PROVEtrace(r)) \not\in P$} 
+        \State \Return $\bot$
       \EndIf
-      \State $\APPEND(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}
-            \If{$m \notin \delivered$}
-              \State $\delivered \leftarrow \delivered \cup \{m\}$
-              \State \Return $m$ \Comment{Deliver exactly one message per call}
-            \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}
-        \EndIf
+      \State $\APPEND(r)$; $P \gets \READ()$
+      \State $W_r \gets \{ j : (j, \PROVEtrace(r)) \in P \}$
+      \If{$\exists j \in W_r,\ \prop[r][j] = \bot$} 
+        \State \Return $\bot$
       \EndIf
-      \State \Return $\bot$ \Comment{No closed round ready for delivery}
+      \State $M_r \gets \bigcup_{j \in W_r} \prop[r][j]$
+      \State $m \gets \ordered(M_r \setminus \delivered)[0]$ \Comment{Set $m$ as the smaller message not already delivered}
+      \State $\delivered \leftarrow \delivered \cup \{m\}$
+      \If{$M_r \setminus \delivered = \emptyset$} \Comment{Check if all messages from round $r$ have been delivered}
+        \State $\current \leftarrow \current + 1$
+      \EndIf
+      \State \textbf{return} $m$
+    \EndFunction
   \end{algorithmic}
 \end{algorithm}
+
 % ------------------------------------------------------------------------------
 \section{Correctness}
 
-\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{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 \Cref{def:closed-round}, some $\APPEND(r)$ occurs in the linearization $H$. \\
+  $H$ is a total order of operations, the set of $\APPEND(r)$ operations is totally ordered, and hence there exists a smallest $\APPEND(r)$ in $H$. We denote this operation $\APPEND^{(\star)}(r)$ and $t_0$ its linearization point. \\
+  By the validity property of \DL, a $\PROVE(r)$ is valid iff $\PROVE(r) \prec \APPEND^{(\star)}(r)$. Thus, after $t_0$, no $\PROVE(r)$ can be valid. \\
+  $H$ is a immutable grow-only history, and hence once closed, a round never becomes open again. \\
+  Hence there exists a linearization point $t_0$ of $\APPEND(r)$ in the \DL, and from that point on, no $\PROVE(r)$ can be valid and the closure is stable. 
+\end{proof}
+
+\begin{definition}[First APPEND]\label{def:first-append}
+  Given a \DL{} linearization $H$, for any closed round $r\in\mathcal{R}$, we denote by $\APPEND^{(\star)}(r)$ the earliest $\APPEND(r)$ in $H$.  
+\end{definition}
+
 \begin{lemma}[Across rounds]\label{lem:across}
-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{proof}
+  \emph{Base.} For a closed round $k=0$, the set $\{k' \in \mathcal{R},\ k' < k\}$ is empty, hence the lemma is true.
+
+  \emph{Induction.} Assume the lemma is true for round $k\geq 0$, we prove it for round $k+1$.
+  
+  \smallskip
+  Assume $k+1$ is closed and let $\APPEND^{(\star)}(k+1)$ be the earliest $\APPEND(k+1)$ in the DL linearization $H$.
+  By Lemma 1, after an $\APPEND(k)$ is in $H$, any later $\PROVE(k)$ is rejected also, a process’s program order is preserved in $H$.
+  
+  There are two possibilities for where $\APPEND^{(\star)}(k+1)$ is invoked.
+
+  \begin{itemize}
+    \item \textbf{Case (B6) :}
+    Some process $p^\star$ executes the loop (lines B5–B11) and invokes $\APPEND^{(\star)}(k+1)$ at line B6.
+    Immediately before line B6, line B5 sets $r\leftarrow r+1$, so the previous loop iteration (if any) targeted $k$. We consider two sub-cases.
+    
+    \begin{itemize}
+      \item \emph{(i) $p^\star$ is not in its first loop iteration.}
+      In the previous iteration, $p^\star$ executed $\PROVE^{(\star)}(k)$ at B6, followed (in program order) by $\APPEND^{(\star)}(k)$. 
+      If round $k$ wasn't closed when $p^\star$ execute $\PROVE^{(\star)}(k)$ at B9, then the condition at B8 would be true hence the tuple $(p^\star, \PROVEtrace(k))$ should be visible in P which implies that $p^\star$ should leave the loop at round $k$, contradicting the assumption that $p^\star$ is now executing another iteration.
+      Since the tuple is not visible, the $\PROVE^{(\star)}(k)$ was rejected by the DL which implies by definition an $\APPEND(k)$ already exists in $H$. Thus in this case $k$ is closed.
+    
+      \item \emph{(ii) $p^\star$ is in its first loop iteration.}
+      To compute the value $r_{max}$, $p^\star$ must have observed one or many $(\_ , \PROVEtrace(k+1))$ in $P$ at B2/B3, issued by some processes (possibly different from $p^\star$). Let's call $p_1$ the issuer of the first $\PROVE^{(1)}(k+1)$ in the linearization $H$. \\
+      When $p_1$ executed $P \gets \READ()$ at B2 and compute $r_{max}$ at B3, he observed no tuple $(\_,\PROVEtrace(k+1))$ in $P$ because he's the issuer of the first one. So when $p_1$ executed the loop (B5–B11), he run it for the round $k$, didn't seen any $(1,\PROVEtrace(k))$ in $P$ at B8, and then executed the first $\PROVE^{(1)}(k+1)$ at B6 in a second iteration. \\
+      If round $k$ wasn't closed when $p_1$ execute $\PROVE^{(1)}(k)$ at B6, then the condition at B8 should be true which implies that $p_1$ sould leave the loop at round $k$, contradicting the assumption that $p_1$ is now executing $\PROVE^{(1)}(r+1)$. In this case $k$ is closed.
+    \end{itemize}
+    
+    \item \textbf{Case (C8) :} 
+    Some process invokes $\APPEND(k+1)$ at C8. 
+    Line C8 is guarded by the presence of $\PROVE(\textit{next})$ in $P$ with $\textit{next}=k+1$ (C5). 
+    Moreover, the local pointer $\textit{next}$ grow by increment of 1 and only advances after finishing the current round (C17), so if a process can reach $\textit{next}=k+1$ it implies that he has completed round $k$, which includes closing $k$ at C8 when $\PROVE(k)$ is observed. 
+    Hence $\APPEND^\star(k+1)$ implies a prior $\APPEND(k)$ in $H$, so $k$ is closed.
+  \end{itemize}
+  
+  \smallskip
+  In all cases, $k+1$ closed implie $k$ closed. By induction on $k$, if the lemme is true for a closed $k$ then it is true for a closed $k+1$.
+  Therefore, the lemma is true for all closed rounds $r$.
+\end{proof}
+
+\begin{definition}[Winner Invariant]\label{def:winner-invariant}
+  For any closed round $r$, define
+  \[
+    \Winners_r \triangleq \{ j : \PROVE^{(j)}(r) \prec \APPEND^\star(r) \}
+  \] 
+  as the unique set of winners of round $r$.
+\end{definition}
+
+\begin{lemma}[Invariant view of closure]\label{lem:closure-view}
+  For any closed round $r$, all correct processes eventually observe the same set of valid tuples $(\_,\PROVEtrace(r))$ in their \DL view.
+\end{lemma}
+  
+\begin{proof}
+  Let's take a closed round $r$. By \Cref{def:first-append}, there exists a unique earliest $\APPEND(r)$ in the DL linearization, denoted $\APPEND^\star(r)$.
+
+  Consider any correct process $p$ that invokes $\READ()$ after $\APPEND^\star(r)$ in the DL linearization. Since $\APPEND^\star(r)$ invalidates all subsequent $\PROVE(r)$, the set of valid tuples $(\_,\PROVEtrace(r))$ observed by any correct process after $\APPEND^\star(r)$ is fixed and identical across all correct processes.
+
+  Therefore, for any closed round $r$, all correct processes eventually observe the same set of valid tuples $(\_,\PROVEtrace(r))$ in their \DL view.
+\end{proof}
+
 \begin{lemma}[Well-defined winners]\label{lem:winners}
-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.
+  For any correct process and round $r$, if the process computes $W_r$ at line C9, then :
+  \begin{itemize}
+    \item $\Winners_r$ is defined;
+    \item the computed $W_r$ is exactly $\Winners_r$.
+  \end{itemize}
 \end{lemma}
 
-\begin{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) \}
-\]
-with $\APPEND^\star(r)$ being the earliest \APPEND$(r)$ in the \DL linearization.
+\begin{proof}
+  Let take a correct process $p_i$ that reach line C9 to compute $W_r$. \\
+  By program order, $p_i$ must have executed $\APPEND^{(i)}(r)$ at C8 before, which implies by \Cref{def:closed-round} that round $r$ is closed. So by \Cref{def:winner-invariant}, $\Winners_r$ is defined. \\
+  By \Cref{lem:closure-view}, all correct processes eventually observe the same set of valid tuples $(\_,\PROVEtrace(r))$ in their \DL view. Hence, when $p_i$ executes the $\READ()$ at C8 after the $\APPEND^{(i)}(r)$, it observes a set $P$ that includes all valid tuples $(\_,\PROVEtrace(r))$ such that
+  \[
+    W_r = \{ j : (j,\PROVEtrace(r)) \in P \} = \{j : \PROVE^{(j)}(r) \prec \APPEND^\star(r) \} = \Winners_r
+  \]
+\end{proof}
+
+\begin{lemma}[No APPEND without PROVE]\label{lem:append-prove}
+If some process invokes $\APPEND(r)$, then at least a process must have previously invoked $\PROVE(r)$.
 \end{lemma}
 
 \begin{proof}[Proof]
-    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.
-
-    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) \}\]
-
-    Let's consider two correct processes $p_i$ and $p_j$ and two \READ{} responses $P_i$ and $P_j$ such that 
-    \[
-    \APPEND^\star(r) \prec (i,\PROVE(r)) \prec P_i
-    \APPEND^\star(r) \prec (j,\PROVE(r)) \prec P_j
-    \]
-    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.\]
+  Consider the round $r$ such that some process invokes $\APPEND(r)$. There are two possible cases
+  
+  \begin{itemize}
+    \item \textbf{Case (B6) :}
+    There exists a process $p^\star$ who's the issuer of the earliest $\APPEND^{(\star)}(r)$ in the DL linearization $H$. By program order, $p^\star$ must have previously invoked $\PROVE^{(\star)}(r)$ before invoking $\APPEND^{(\star)}(r)$ at B6. In this case, there is at least one $\PROVE(r)$ valid in $H$ issued by a correct process before $\APPEND^{(\star)}(r)$.
+    
+    \item \textbf{Case (C8) :}
+    There exist a process $p^\star$ invokes $\APPEND^{(\star)}(r)$ at C8. Line C8 is guarded by the condition at C5, which ensures that $p$ observed some $(\_,\PROVEtrace(r))$ in $P$. In this case, there is at least one $\PROVE(r)$ valid in $H$ issued by some process before $\APPEND^{(\star)}(r)$.
+  \end{itemize}
+    
+  In both cases, if some process invokes $\APPEND(r)$, then some process must have previously invoked $\PROVE(r)$.
 \end{proof}
 
 \begin{lemma}[No empty winners]\label{lem:nonempty}
-For any round $r$ closed, $\Winners_r \neq \emptyset$.
+  Let $r$ be a round, if $\Winners_r$ is defined, then $\Winners_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.
-  
-    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
-    \[
-       (k,\PROVE(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$,
-    \[
-       k \in \Winners_r.
-    \]
-    Therefore $\Winners_r \neq \emptyset$, i.e., $|\Winners_r|>0$.
+  If $\Winners_r$ is defined, then by \Cref{def:winner-invariant}, round $r$ is closed. By \Cref{def:closed-round}, some $\APPEND(r)$ occurs in the DL linearization. \\
+  By \Cref{lem:append-prove}, at least a process must have invoked a valid $\PROVE(r)$ before $\APPEND^{(\star)}(r)$. Hence, there exists at least one $j$ such that $\{j: \PROVE^{(j)}(r) \prec \APPEND^\star(r)\}$, so $\Winners_r \neq \emptyset$.
+\end{proof}
+
+\begin{lemma}[Winners must propose]\label{lem:winners-propose}
+  For any closed round $r$, $\forall j \in \Winners_r$, process $j$ must have invoked a $\RBcast(S^{(j)}, r, j)$
+\end{lemma}
+
+\begin{proof}[Proof]
+  Fix a closed round $r$. By \Cref{def:winner-invariant}, for any $j \in \Winners_r$, there exist a valid $\PROVE^{(j)}(r)$ such that $\PROVE^{(j)}(r) \prec \APPEND^\star(r)$ in the DL linearization. By program order, if $j$ invoked a valid $\PROVE^{(j)}(r)$ at line B6 he must have invoked $\RBcast(S^{(j)}, r, j)$ directly before.
+\end{proof}
+
+\begin{definition}[Messages invariant]\label{def:messages-invariant}
+  For any closed round $r$ and any correct process $p_i$ such that $\nexists j \in \Winners_r : prop^{[i)}[r][j] = \bot$, define
+  \[
+    \Messages_r \triangleq \bigcup_{j\in\Winners_r} \prop^{(i)}[r][j]
+  \]
+  as the unique set of messages proposed by the winners of round $r$.
+\end{definition}
+
+\begin{lemma}[Non-empty winners proposal]\label{lem:winner-propose-nonbot}
+  For any closed round $r$, $\forall j \in \Winners_r$, for any correct process $p_i$, eventually $\prop^{(i)}[r][j] \neq \bot$.  
+\end{lemma}
+
+\begin{proof}[Proof]
+  Fix a closed round $r$. By \Cref{def:winner-invariant}, for any $j \in \Winners_r$, there exist a valid $\PROVE^{(j)}(r)$ such that $\PROVE^{(j)}(r) \prec \APPEND^\star(r)$ in the DL linearization. By \Cref{lem:winners-propose}, $j$ must have invoked $\RBcast(S^{(j)}, r, j)$.
+
+  Let take a process $p_i$, by \RB \emph{Validity}, every correct process eventually receives $j$'s \RB message for round $r$, which sets $\prop[r][j]$ to a non-$\bot$ value at line A3.
+\end{proof}
+
+\begin{lemma}[Eventual proposal closure]\label{lem:eventual-closure}
+  If a correct process $p_i$ define $M_r$ at line C13, then for every $j \in \Winners_r$, $\prop^{(i)}[r][j] \neq \bot$. 
+\end{lemma}
+
+\begin{proof}[Proof]
+  Let take a correct process $p_i$ that computes $M_r$ at line C13. By \Cref{lem:winners}, $p_i$ computes the unique winner set $\Winners_r$.
+
+  By \Cref{lem:nonempty}, $\Winners_r \neq \emptyset$. The instruction at line C13 where $p_i$ computes $M_r$ is guarded by the condition at C10, which ensures that $p_i$ has received all \RB messages from every winner $j \in \Winners_r$. Hence, when $p_i$ computes $M_r = \bigcup_{j\in\Winners_r} \prop^{(i)}[r][j]$, we have $\prop^{(i)}[r][j] \neq \bot$ for all $j \in \Winners_r$.
+\end{proof}
+
+\begin{lemma}[Unique proposal per sender per round]\label{lem:unique-proposal}
+  For any round $r$ and any process $p_i$, $p_i$ invokes at most one $\RBcast(S, r, i)$.
+\end{lemma}
+
+\begin{proof}[Proof]
+  By program order, any process $p_i$ invokes $\RBcast(S, r, i)$ at line B6 must be in the loop B5–B11. No matter the number of iterations of the loop, line B5 always uses the current value of $r$ which is incremented by 1 at each turn. Hence, in any execution, any process $p_i$ invokes $\RBcast(S, r, j)$ at most once for any round $r$.
 \end{proof}
 
 \begin{lemma}[Proposal convergence]\label{lem:convergence}
-For any closed round $r$, after all \RB messages from $\Winners_r$ are received, every correct process computes the same $M_r = \bigcup_{j\in \Winners_r} \prop[r][j]$.
+  For any round $r$, for any correct processes $p_i$ that define $M_r$ at line C13, we have
+  \[
+    M_r^{(i)} = \Messages_r
+  \]
 \end{lemma}
 
 \begin{proof}[Proof]
-    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$:
-    \[
-      \RBcast(\_, S_j, r, j) \ \text{(B4)} \quad\text{before}\quad \PROVE(r) \ \text{(B5)} \quad\text{before}\quad \APPEND(r) \ \text{(B6)}.
-    \]
-    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$. 
+  Let take a correct process $p_i$ that define $M_r$ at line C13. That implies that $p_i$ has defined $W_r$ at line C9. It implies that, by \Cref{lem:winners}, $r$ is closed and $W_r = \Winners_r$. \\
+  By \Cref{lem:eventual-closure}, for every $j \in \Winners_r$, $\prop^{(i)}[r][j] \neq \bot$. By \Cref{lem:unique-proposal}, each winner $j$ invokes at most one $\RBcast(S^{(j)}, r, j)$, so $\prop^{(i)}[r][j] = S^{(j)}$ is uniquely defined. Hence, when $p_i$ computes
+  \[
+    M_r^{(i)} = \bigcup_{j\in\Winners_r} \prop^{(i)}[r][j] = \bigcup_{j\in\Winners_r} S^{(j)} = \Messages_r.
+  \]
 \end{proof}
 
-\begin{lemma}[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.
-\end{lemma}
-
-
-\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
-\[
-\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.
+  If some correct process invokes $\ABbroadcast(m)$, then there exist a round $r$ and a process $j\in\Winners_r$ such that $p_j$ invokes
+  \[
+  \RBcast(S, r, j)\quad\text{with}\quad m\in S.
+  \]
 \end{lemma}
 
-\begin{theorem}[\ARB]
-Under the assumed \DL synchrony and \RB reliability, the algorithm implements Atomic Reliable Broadcast.
+\begin{proof}
+  Fix a correct process $p_i$ that invokes $\ABbroadcast(m)$ and eventually exits the loop (B5–B11) at some round $r$. There are two possible cases.
+
+  \begin{itemize}
+    \item \textbf{Case 1:} $p_i$ exits the loop because $(i, \PROVEtrace(r)) \in P$. In this case, by \Cref{def:winner-invariant}, $p_i$ is a winner in round $r$. By program order, $p_i$ must have invoked $\RBcast(S, r, i)$ at B6 before invoking $\PROVE^{(i)}(r)$ at B7. By line B4, $m \in S$. Hence there exist a closed round $r$ and a correct process $j=i\in\Winners_r$ such that $j$ invokes $\RBcast(S, r, j)$ with $m\in S$.
+    
+    \item \textbf{Case 2:} $p_i$ exits the loop because $\exists j, r': (j, \PROVEtrace(r')) \in P \wedge m \in \prop[r'][j]$. In this case, by \Cref{lem:winners-propose} and \Cref{lem:unique-proposal} $j$ must have invoked a unique $\RBcast(S, r', j)$. Which set $\prop^{(i)}[r'][j] = S$ with $m \in S$.   
+  \end{itemize}
+    
+  In both cases, if some correct process invokes $\ABbroadcast(m)$, then there exist a round $r$ and a correct process $j\in\Winners_r$ such that $j$ invokes
+  \[
+    \RBcast(S, r, j)\quad\text{with}\quad m\in S.
+  \]
+\end{proof}
+
+\begin{lemma}[Broadcast Termination]\label{lem:bcast-termination}
+  If a correct process invokes $\ABbroadcast(m)$, then he eventually exit the function and returns.
+\end{lemma}
+
+\begin{proof}[Proof]
+  Let a correct process $p_i$ that invokes $\ABbroadcast(m)$. The lemma is true if $\exists r_1$ such that $r_1 \geq r_{max}$ and if $(i, \PROVEtrace(r_1)) \in P$; or if $\exists r_2$ such that $r_2 \geq r_{max}$ and if $\exists j: (j, \PROVEtrace(r_2)) \in P \wedge m \in \prop[r_2][j]$ (like guarded at B8).
+
+  Let admit that there exists no round $r_1$ such that $p_i$ invokes a valid $\PROVE(r_1)$. In this case $p_i$ invokes infinitely many $\RBcast(S, \_, i)$ at B6 with $m \in S$ (line B4).\\
+  The assumption that no $\PROVE(r_1)$ invoked by $p$ is valid implies by \DL \emph{Validity} that for every round $r' \geq r_{max}$, there exists at least one $\APPEND(r')$ in the DL linearization, hence by \Cref{lem:nonempty} for every possible round $r'$ there at least a winner. Because there is an infinite number of rounds, and a finite number of processes, there exists at least a correct process $p_k$ that invokes infinitely many valid $\PROVE(r')$ and by extension infinitely many $\ABbroadcast(\_)$. By \RB \emph{Validity}, $p_k$ eventually receives $p_i$ 's \RB messages. Let call $t_0$ the time when $p_k$ receives $p_i$ 's \RB message. \\
+  At $t_0$, $p_k$ execute \Cref{alg:rb-handler} and do $\received \leftarrow \received \cup \{S\}$ with $m \in S$ (line A2). 
+  For the first invocation of $\ABbroadcast(\_)$ by $p_k$ after the execution of \Cref{alg:rb-handler}, $p_k$ must include $m$ in his proposal $S$ at line B4 (because $m$ is pending in $j$'s $\received \setminus \delivered$ set). There exists a minimum round $r_2$ such that $p_k \in \Winners_{r_2}$ after $t_0$. By \Cref{lem:winner-propose-nonbot}, eventually $\prop^{(i)}[r_2][k] \neq \bot$. By \Cref{lem:unique-proposal}, $\prop^{(i)}[r_2][k]$ is uniquely defined as the set $S$ proposed by $p_k$ at B6, which by \Cref{lem:inclusion} includes $m$. Hence eventually $m \in \prop^{(i)}[r_2][k]$ and $k \in \Winners_{r_2}$. 
+
+  So if $p_i$ is a winner he cover the condition $(i, \PROVEtrace(r_1)) \in P$. And we show that if the first condition is never satisfied, the second one will eventually be satisfied. Hence either the first or the second condition will eventually be satisfied, and $p_i$ eventually exits the loop and returns from $\ABbroadcast(m)$.
+\end{proof}
+
+\begin{lemma}[Validity]\label{lem:validity}
+  If a correct process $p$ invokes $\ABbroadcast(m)$, then every correct process that invokes a infinitely often times $\ABdeliver()$ eventually delivers $m$.
+\end{lemma}
+
+\begin{proof}[Proof]
+  Let $p_i$ a correct process that invokes $\ABbroadcast(m)$ and $p_q$ a correct process that infinitely invokes $\ABdeliver()$. By \Cref{lem:inclusion}, there exist a closed round $r$ and a correct process $j\in\Winners_r$ such that $p_j$ invokes
+  \[
+    \RBcast(S, r, j)\quad\text{with}\quad m\in S.
+  \]
+
+  By \Cref{lem:eventual-closure}, when $p_q$ computes $M_r$ at line C13, $\prop[r][j]$ is non-$\bot$ because $j \in \Winners_r$. By \Cref{lem:unique-proposal}, $p_j$ invokes at most one $\RBcast(S, r, j)$, so $\prop[r][j]$ is uniquely defined. Hence, when $p_q$ computes
+  \[
+    M_r = \bigcup_{k\in\Winners_r} \prop[r][k],
+  \]
+  we have $m \in \prop[r][j] = S$, so $m \in M_r$. By \Cref{lem:convergence}, $M_r$ is invariant so each computation of $M_r$ by any correct process that defines it includes $m$. At each invocation of $\ABdeliver()$ which deliver $m'$, $m'$ is add to $\delivered$ until $M_r \subseteq \delivered$. Once this append we're assured that there exist an invocation of $\ABdeliver()$ which return $m$. Hence $m$ is well delivered.
+\end{proof}
+
+\begin{lemma}[No duplication]\label{lem:no-duplication}
+  No correct process delivers the same message more than once.
+\end{lemma}
+
+\begin{proof}
+  Let consider two invokations of $\ABdeliver()$ made by the same correct process which returns $m$. Let call these two invocations respectively $\ABdeliver^{(A)}()$ and $\ABdeliver^{(B)}()$.
+
+  When $\ABdeliver^{(A)}()$ occur, by program order and because it reach line C19 to return $m$, the process must have add $m$ to $\delivered$. Hence when $\ABdeliver^{(B)}()$ reach line C14 to extract the next message to deliver, it can't be $m$ because $m \not\in (M_r \setminus \{..., m, ...\})$. So a $\ABdeliver^{(B)}()$ which deliver $m$ can't occur.
+\end{proof}
+
+\begin{lemma}[Total order]\label{lem:total-order}
+  For any two messages $m_1$ and $m_2$ delivered by correct processes, if a correct process $p_i$ delivers $m_1$ before $m_2$, then any correct process $p_j$ that delivers both $m_1$ and $m_2$ delivers $m_1$ before $m_2$.  
+\end{lemma}
+
+\begin{proof}
+  Consider any correct process that delivers both $m_1$ and $m_2$. By \Cref{lem:validity}, there exist closed rounds $r'_1$ and $r'_2$ and correct processes $k_1 \in \Winners_{r'_1}$ and $k_2 \in \Winners_{r'_2}$ such that
+  \[
+    \RBcast(S_1, r'_1, k_1)\quad\text{with}\quad m_1\in S_1,
+  \]
+  \[
+    \RBcast(S_2, r'_2, k_2)\quad\text{with}\quad m_2\in S_2.
+  \]
+
+  Let consider three cases :
+  \begin{itemize}
+    \item \textbf{Case 1:} $r_1 < r_2$. By program order, any correct process must have waited to append in $\delivered$ every messages in $M_{r_1}$ (which contains $m_1$) to increment $\current$ and eventually set $\current = r_2$ to compute $M_{r_2}$ and then invoke the $\ABdeliver()$ that returns $m_2$. Hence, for any correct process that delivers both $m_1$ and $m_2$, it delivers $m_1$ before $m_2$.
+    
+    \item \textbf{Case 2:} $r_1 = r_2$. By \Cref{lem:convergence}, any correct process that computes $M_{r_1}$ at line C13 computes the same set of messages $\Messages_{r_1}$. By line C14 the messages are pull in a deterministic order defined by $\ordered(\_)$. Hence, for any correct process that delivers both $m_1$ and $m_2$, it delivers $m_1$ and $m_2$ in the deterministic order defined by $\ordered(\_)$.
+  \end{itemize}
+
+  In all possible cases, any correct process that delivers both $m_1$ and $m_2$ delivers $m_1$ and $m_2$ in the same order.
+\end{proof}
+
+\begin{lemma}[Fifo Order]\label{lem:fifo-order}
+  For any two messages $m_1$ and $m_2$ broadcast by the same correct process $p_i$, if $p_i$ invokes $\ABbroadcast(m_1)$ before $\ABbroadcast(m_2)$, then any correct process $p_j$ that delivers both $m_1$ and $m_2$ delivers $m_1$ before $m_2$.
+\end{lemma}
+
+\begin{proof}
+  Let take two messages $m_1$ and $m_2$ broadcast by the same correct process $p_i$, with $p_i$ invoking $\ABbroadcast(m_1)$ before $\ABbroadcast(m_2)$. By \Cref{lem:validity}, there exist closed rounds $r_1$ and $r_2$ and correct processes $k_1 \in \Winners_{r_1}$ and $k_2 \in \Winners_{r_2}$ such that
+  \[
+    \RBcast(S_1, r_1, k_1)\quad\text{with}\quad m_1\in S_1,
+  \]
+  \[
+    \RBcast(S_2, r_2, k_2)\quad\text{with}\quad m_2\in S_2.
+  \]
+
+  By program order, $p_i$ must have invoked $\RBcast(S_1, r_1, i)$ before $\RBcast(S_2, r_2, i)$. By \Cref{lem:unique-proposal}, any process invokes at most one $\RBcast(S, r, i)$ per round, hence $r_1 < r_2$. By \Cref{lem:total-order}, any correct process that delivers both $m_1$ and $m_2$ delivers them in a deterministic order.
+  
+  In all possible cases, any correct process that delivers both $m_1$ and $m_2$ delivers $m_1$ before $m_2$.
+\end{proof}
+
+\begin{theorem}[FIFO-\ARB]
+Under the assumed \DL synchrony and \RB reliability, the algorithm implements FIFO Atomic Reliable Broadcast.
 \end{theorem}
 
+\begin{proof}
+  We show that the algorithm satisfies the properties of FIFO Atomic Reliable Broadcast under the assumed \DL synchrony and \RB reliability.
+
+  First, by \Cref{lem:bcast-termination}, if a correct process invokes \ABbroadcast$(m)$, then it eventually returns from this invocation.
+  Moreover, \Cref{lem:validity} states that if a correct process invokes \ABbroadcast$(m)$, then every correct process that invokes \ABdeliver() infinitely often eventually delivers $m$.
+  This gives the usual Validity property of \ARB.
+
+  Concerning Integrity and No-duplicates, the construction only ever delivers messages that have been obtained from the underlying \RB primitive.
+  By the Integrity property of \RB, every such message was previously \RBcast by some process, so no spurious messages are delivered.
+  In addition, \Cref{lem:no-duplication} states that no correct process delivers the same message more than once.
+  Together, these arguments yield the Integrity and No-duplicates properties required by \ARB.
+
+  For the ordering guarantees, \Cref{lem:total-order} shows that for any two messages $m_1$ and $m_2$ delivered by correct processes, every correct process that delivers both $m_1$ and $m_2$ delivers them in the same order.
+  Hence all correct processes share a common total order on delivered messages.
+  Furthermore, \Cref{lem:fifo-order} states that for any two messages $m_1$ and $m_2$ broadcast by the same correct process, any correct process that delivers both messages delivers $m_1$ before $m_2$ whenever $m_1$ was broadcast before $m_2$.
+  Thus the global total order extends the per-sender FIFO order of \ABbroadcast.
+
+  All the above lemmas are proved under the assumptions that \DL satisfies the required synchrony properties and that the underlying primitive is a Reliable Broadcast (\RB) with Integrity, No-duplicates and Validity.
+  Therefore, under these assumptions, the algorithm satisfies Validity, Integrity/No-duplicates, total order and per-sender FIFO order, and hence implements FIFO Atomic Reliable Broadcast, as claimed.
+\end{proof}
+
+\section{Reciprocity}
+% ------------------------------------------------------------------------------
+
+So far, we assumed the existence of a synchronous DenyList (\DL) object and
+showed how to upgrade a Reliable Broadcast (\RB) primitive into FIFO Atomic
+Reliable Broadcast (\ARB). We now briefly argue that, conversely, an \ARB{}
+primitive is strong enough to implement a synchronous \DL object (ignoring the
+anonymity property).
+
+\paragraph{DenyList as a deterministic state machine.}
+Without anonymity, the \DL specification defines a
+deterministic abstract object: given a sequence $\Seq$ of operations
+$\APPEND(x)$, $\PROVE(x)$, and $\READ()$, the resulting sequence of return
+values and the evolution of the abstract state (set of appended elements,
+history of operations) are uniquely determined.
+
+\paragraph{State machine replication over \ARB.}
+Assume a system that exports a FIFO-\ARB primitive with the guarantees that if a correct process invokes $\ABbroadcast(m)$, then every correct process eventually $\ABdeliver(m)$ and the invocation eventually returns.
+Following the classical \emph{state machine replication} approach
+such as described in Schneider~\cite{Schneider90}, we can implement a fault-tolerant service by ensuring the following properties:
+\begin{quote}
+  \textbf{Agreement.} Every nonfaulty state machine replica receives every request. \\
+  \textbf{Order.} Every nonfaulty state machine replica processes the requests it receives in
+  the same relative order.
+\end{quote}
+
+Which are cover by our FIFO-\ARB specification.
+
+\paragraph{Correctness.}
+
+
+\begin{theorem}[From \ARB to synchronous \DL]\label{thm:arb-to-dl}
+  In an asynchronous message-passing system with crash failures, assume a
+  FIFO Atomic Reliable Broadcast primitive with Integrity, No-duplicates,
+  Validity, and the liveness of $\ABbroadcast$. Then, ignoring anonymity, there
+  exists an implementation of a synchronous DenyList object that satisfies the
+  Termination, Validity, and Anti-flickering properties.
+\end{theorem}
+
+\begin{proof}
+  Because the \DL object is deterministic, all correct processes see the same
+  sequence of operations and compute the same sequence of states and return
+  values. We obtain:
+
+  \begin{itemize}[leftmargin=*]
+    \item \textbf{Termination.} The liveness of \ARB ensures that each
+          $\ABbroadcast$ invocation by a correct process eventually returns, and
+          the corresponding operation is eventually delivered and applied at all
+          correct processes. Thus every $\APPEND$, $\PROVE$, and $\READ$ operation invoked by a correct process
+          eventually returns.
+    \item \textbf{APPEND/PROVE/READ Validity.} The local code that forms
+          \ABbroadcast requests can achieve the same preconditions as in the
+          abstract \DL specification (e.g., $p\in\Pi_M$, $x\in S$ for
+          $\APPEND(x)$). Once an operation is delivered, its effect and return
+          value are exactly those of the sequential \DL specification applied in
+          the common order.
+    \item \textbf{PROVE Anti-Flickering.} In the sequential \DL specification,
+          once an element $x$ has been appended, all subsequent $\PROVE(x)$ are
+          invalid forever. Since all replicas apply operations in the same order,
+          this property holds in every execution of the replicated implementation:
+          after the first linearization point of $\APPEND(x)$, no later
+          $\PROVE(x)$ can return ``valid'' at any correct process.
+  \end{itemize}
+
+  Formally, we can describe the \DL object with the state machine approach for
+  crash-fault, asynchronous message-passing systems with a total order broadcast
+  layer~\cite{Schneider90}.
+\end{proof}
+
+
+
 \bibliographystyle{plain}
 \begin{thebibliography}{9}
 % (left intentionally blank)
+\bibitem{Schneider90}
+Fred B.~Schneider.
+\newblock Implementing fault-tolerant services using the state machine
+  approach: a tutorial.
+\newblock {\em ACM Computing Surveys}, 22(4):299--319, 1990.
 \end{thebibliography}
 
 \end{document}

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}

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}
+}

Recherche/BFT-ARBover/.latexmkrc

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

Recherche/BFT-ARBover/diagrams/BFT_behaviour.puml

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

Recherche/BFT-ARBover/diagrams/BFT_behaviour.tex

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

Recherche/BFT-ARBover/diagrams/classic_seq.puml

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

Recherche/BFT-ARBover/diagrams/classic_seq.tex

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

Recherche/BFT-ARBover/diagrams/nonBFT_behaviour.puml

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

Recherche/BFT-ARBover/diagrams/nonBFT_behaviour.tex

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

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}

docs/presentations/LIS/CSI2025/main.tex

@@ -0,0 +1,252 @@
+\documentclass[aspectratio=169]{beamer}
+
+\usetheme{Madrid}
+\usefonttheme{professionalfonts}
+
+\usepackage[utf8]{inputenc}
+\usepackage[T1]{fontenc}
+\usepackage[french]{babel}
+\usepackage{mathtools,amssymb}
+\usepackage{microtype}
+\usepackage{pgfgantt}
+\usepackage{adjustbox}
+% Réduire la densité verticale par défaut
+% \ganttset{y unit chart=0.45cm, y unit title=0.6cm, bar height=0.35}
+
+% Acronymes utiles
+\newcommand{\EC}{\textsc{EC}}
+\newcommand{\CRDT}{\textsc{CRDT}}
+\newcommand{\PCDO}{\textsc{PCDO}}
+\newcommand{\RB}{\textsc{RB}}
+\newcommand{\ARB}{\textsc{ARB}}
+\newcommand{\BFT}{\textsc{BFT}}
+\newcommand{\DL}{\textsc{DL}}
+\newcommand{\AL}{\textsc{AL}}
+\newcommand{\ZT}{\textsc{ZT}}
+
+
+% =====================
+% Paramétrage générique et macros d'usage
+% ---------------------
+% Définir la fenêtre temporelle du diagramme (ISO 8601)
+\newcommand{\GanttSetup}[2]{% #1 = YYYY-MM-DD (début), #2 = YYYY-MM-DD (fin)
+  \def\GanttStart{#1}%
+  \def\GanttEnd{#2}%
+}
+% Evénement sur période
+% Usage : \Period[<opts pgfgantt>]{<label>}{<YYYY-MM-DD>}{<YYYY-MM-DD>}
+\newcommand{\Period}[4][]{\ganttbar[#1]{#2}{#3}{#4}}
+% Evénement ponctuel (jalon)
+% Usage : \Event[<opts pgfgantt>]{<label>}{<YYYY-MM-DD>}
+\newcommand{\Event}[3][]{\ganttmilestone[#1]{#2}{#3}}
+% Groupe (optionnel)
+% Usage : \Block[<opts>]{<label>}{<YYYY-MM-DD>}{<YYYY-MM-DD>}
+\newcommand{\Block}[4][]{\ganttgroup[#1]{#2}{#3}{#4}}
+
+% Style par défaut (sobre, lisible en salle)
+\ganttset{
+  calendar week text={},
+  time slot format=isodate,
+  vgrid, hgrid,
+  x unit=0.42cm,    % densité horizontale
+  y unit chart=0.45cm, y unit title=0.6cm, bar height=0.35,
+  bar/.append style={fill=blue!35},
+  group/.append style={fill=black!10},
+  milestone/.append style={fill=red!60},
+  bar label font=\scriptsize, group label font=\scriptsize, milestone label font=\scriptsize,
+  title label font=\footnotesize, title/.style={fill=black!5}
+}
+
+\title{2ème Comité de Suivi Individuel 2024-2025}
+\subtitle{Thèse CIFRE - Cohérence Faible pour le cloud zero-trust}
+\institute[AMU - LIS - Scille]{Université Aix-Marseille - LIS \and Scille} 
+% \logo{\includegraphics[height=0.5cm]{logo-lis.png} \hspace{2em} \includegraphics[height=0.5cm]{parsec.png}}
+\author[Amaury JOLY]{Amaury JOLY \\ \vspace{1em} \textbf{Encadrement :} Emmanuel GODARD, Corentin TRAVERS \\ \vspace{1em} \textbf{Comité de suivi :} Arnaud LABOUREL, Achour MOSTEFAOUI}
+\date{\today}
+
+\begin{document}
+
+\begin{frame}
+  \titlepage
+\end{frame}
+
+% Rajouter nombre d'heure recherche industrielle formation OK
+% Dire que le model CRDT et PCDO implique du RB OK
+% Usage de RB+DL=>ARB dans le cloud zero-trust
+% Etre plus claire sur les missions en cours avec Scille OK
+
+% Se renseigner sur l'état de l'art sur RB+DL=>ARB et PCDO
+
+% Voir avce Scille pour la poursuite de these
+
+% =======================
+\begin{frame}{Contexte de thèse (CIFRE)}
+  \begin{itemize}
+    \item Démarrage administratif : \textbf{janvier 2024}.
+    \item Sujet : \emph{Cohérence Faible pour le cloud zero-trust}.
+    \item Cadre : thèse \textbf{CIFRE} avec l’entreprise \textbf{Scille} (logiciel \texttt{parsec.cloud}).
+    \item Répartition d’activités : \textbf{70\% recherche} / \textbf{30\% entreprise}.
+  \end{itemize}
+  \end{frame}
+  
+  % =======================
+  \begin{frame}{Contexte industriel — partage de fichiers \ZT{}}
+  \begin{itemize}
+    \item Produit : logiciel de partage de fichiers \textbf{zero-trust}.
+    \item Modèle \ZT{} : le \textbf{serveur ne voit que des données chiffrées} et ne connaît pas l’identité des utilisateurs.
+    \item Model de communication : \textbf{serveur centralisé unique} pour tous les clients.
+    \item Hypothèses : confiance pour la \textbf{redistribution des messages} et la \textbf{disponibilité} ; serveur \textbf{honnête mais curieux}.
+  \end{itemize}
+  \end{frame}
+  
+  % =======================
+  \begin{frame}{Bilan des formations et divers (oct. 2024 — oct. 2025)}
+  \begin{itemize}
+    \item \textbf{REDOCS 2024} : 14 au 19 octobre 2024
+    \item \textbf{PEPR Trust in Cloud 2024} (Grenoble) : novembre 2024.
+    \item \textbf{PEPR Trust in Cloud 2025} (Massy) : octobre 2025.
+    \item \textbf{Séminaires entreprise} : 3 séances en présentiel.
+    \item \textbf{Reunion avancement produit et R\&D} : toutes les 2 semaines.
+    \item \textbf{Enseignement} : 30 h en M1 (24h TP + 6h TD) + Soutenances de stage M2 FSI
+  \end{itemize}
+  \end{frame}
+  
+  % =======================
+  \begin{frame}{Missions en entreprise (résumé)}
+  \begin{itemize}
+    \item \textbf{Document BPI} : état de l’art et \textbf{valeur ajoutée} des fonctionnalités d’\emph{édition collaborative} de l’équipe R\&D Parsec.
+    \item \textbf{État de l’art} sur \textbf{\ZT{}} et \textbf{Data-Centric Security} pour une réponse à appel d’offres \textbf{OTAN}.
+    \item \textbf{Conseil} : stratégie de \textbf{sauvegarde} dans un contexte \textbf{pair-à-pair distribué} pour l’édition collaborative.
+    \item \textbf{CIR} : rédaction en cours d’un \textbf{document consolidé} couvrant les projets R\&D (état de l’art, besoins spécifiques, caractère innovant, avancées annuelles).
+    \vspace{1em}
+    \item Développement de \textbf{fonctionnalités} experimentales dans \texttt{parsec}
+  \end{itemize}
+  \end{frame}
+  
+  % =======================
+  \begin{frame}{CRDT (Shapiro et al., 2011) - Rappel}
+  \begin{itemize}
+    \item Un \CRDT{} est une \textbf{spécification de type de donnée répliqué} qui permet d’\textbf{atteindre la cohérence éventuelle} (\EC) \textbf{sans imposer d’ordre total} entre les opérations (sous hypothèse de \textbf{Reliable Broadcast} (RB)).
+    \item L’idée clé est de \textbf{converger par construction} : les opérations (ou les jointures d’états) sont \textbf{commutatives} (souvent aussi associatives et idempotentes), garantissant que tout ordre de livraison mène au même état.
+    \pause
+    \item \textbf{Contrepartie} : la \textbf{structure commutative} restreint les usages aux applications dont les mises à jour sont naturellement commutatives; elle est moins adaptée lorsque des \textbf{invariants globaux non commutatifs} ou des \textbf{contraintes d’ordre} sont requis.
+  \end{itemize}
+  \end{frame}
+  
+  % =======================
+  \begin{frame}{PCDO (Frey et al., 2023)}
+  \begin{itemize}
+    \item Les \PCDO{} étendent les \CRDT{} mais \textbf{ajoute une notion de légalité d’état} : un prédicat caractérise quels états sont \emph{légaux}.
+    \item Alors que, dans les \CRDT, \textbf{toutes les opérations sont éventuellement traitées par tous les nœuds} (sans ordre global), un \PCDO{} autorise d’\textbf{exiger un ordre pour certaines opérations}.
+    \pause
+    \item Pour \textbf{atteindre} cela sans sacrifier l’asynchronisme, la \textbf{contrainte d’ordre est restreinte \emph{par processus}} : seules les opérations \textbf{émises par le même processus} doivent être \textbf{émises et exécutées dans un certain ordre}.
+    \item Les opérations inter-processus restent commutatives (au sens requis par le prédicat de légalité), préservant la \EC{}.
+  \end{itemize}
+  \end{frame}
+  
+  % =======================
+  \begin{frame}{\PCDO{} ?= \RB{} \BFT{}}
+  \begin{itemize}
+    \item \textbf{Question de recherche} : une implémentation \BFT{} d’un \PCDO{} est-elle \textbf{équivalente} à l’implémentation \BFT{} d’un \textbf{Reliable Broadcast} (\RB)?
+    \item Intuition : si un \PCDO{} impose un \textbf{ordre par émetteur}, et que \RB{}-BFT assure \textbf{livraison fiable/consistante}, peut-on \textbf{réduire} l’un à l’autre~?
+    \item \textbf{Travail en cours} : exploration d’algorithmes visant à \textbf{montrer l’équivalence} (ou une réduction bidirectionnelle). \textbf{À ce stade}, pas de résultat concluant.
+    \item Points de blocage actuels : \textbf{interaction entre la légalité d’état locale au processus} et les \textbf{garanties globales} de \RB{}-\BFT{} (accord, intégrité, terminaison).
+  \end{itemize}
+  \end{frame}
+  
+  % =======================
+  \begin{frame}{AllowList et DenyList (Frey et al., 2023)}
+  \begin{itemize}
+    \item Présentation de travaux de \textbf{Mathieu Gestin} : spécification d’\AL{} et de \DL{} comme \textbf{registre partagé} dans un système \textbf{asynchrone} sujet aux \textbf{crashs}.
+    \item Interface fondée sur \textbf{trois primitives} :
+    \begin{itemize}
+      \item \texttt{APPEND(x)} : ajout d’un élément à l'\AL{}/\DL{}.
+      \item \texttt{PROVE(x)} : fournir une \textbf{preuve vérifiable} de présence/absence.
+      \item \texttt{READ()} : obtenir une \textbf{vue cohérente} du registre.
+    \end{itemize}
+    \item L’objectif est d’\textbf{atteindre les garanties attendues} d’une \AL{}/\DL{} distribuée (sécurité, auditabilité, progression sous asynchronisme avec crashs).
+  \end{itemize}
+  \end{frame}
+  
+  % =======================
+  \begin{frame}{\RB{} + \DL{} $\Rightarrow$ \ARB{} (intuition)}
+  \begin{itemize}
+    \item Idée : utiliser la \textbf{\DL{} comme mécanisme de verrou/élection} pour \textbf{ordonner} des messages livrés via \RB{}, et ainsi passer à l’\textbf{Atomic Reliable Broadcast} (\ARB{}).
+    \item \textbf{Par rounds} :
+    \begin{enumerate}
+      \item À chaque round, un \textbf{ensemble non vide de vainqueurs} est sélectionné (via \DL{}) et \textbf{détient le droit d’émettre}.
+      \item Quand le round est \textbf{fermé}, les autres processus tentent d’être élus au \textbf{round suivant}.
+    \end{enumerate}
+    \item \textbf{Processus lents} : un mécanisme de \textbf{dissémination des messages en attente} force les nœuds corrects à \textbf{relayer/émettre} pour leur compte afin d’éviter les blocages.
+    \item L’ordonnancement par rounds permet d’\textbf{établir un ordre total} entre les messages.
+  \end{itemize}
+  \end{frame}
+  
+  % =======================
+  \begin{frame}{\RB{} + \DL{} $\Rightarrow$ \ARB{} (contexte industriel \& ZT)}
+  \begin{itemize}
+    \item \textbf{Contraintes industrielles (CIFRE)} : les \CRDT{}\ \PCDO{} ne couvrent pas tous les cas d’usage — certaines applications requièrent un \textbf{ordre total} global malgré l’asynchronisme.
+    \item \textbf{Hypothèse architecturale} : un \textbf{serveur « proxy » ZT} ne voyant que des \textbf{chiffrés}, chargé de \textbf{dispatcher} et de \textbf{synchroniser} les messages; aucune logique métier ni accès au clair.
+    \item \textbf{Levier} : combiner \RB{} avec \DL{} pour sérialiser les tours d’émission; le proxy n’est qu’un \textbf{médiateur d’ordonnancement}, pas une source de confiance.
+    \item \textbf{Pertinence} : solution adaptée aux environnements contraints où la \textbf{centralisation de l’ordonnancement} est acceptable mais où la \textbf{confiance} reste minimisée.
+  \end{itemize}
+  \end{frame}
+  
+  % =======================
+  \begin{frame}{\RB{} + \DL{} $\Rightarrow$ \ARB{} (état d’avancement)}
+  \begin{itemize}
+    \item \textbf{Algorithme} : spécifié et en cours de \textbf{finalisation de la preuve} dans un \textbf{modèle crash}.
+    \item \textbf{Propriété visée} : \ARB{} (accord, validité, intégrité, \textbf{ordre total}).
+    \item \textbf{Perspectives} : extension au \textbf{modèle byzantin} (\BFT{}). Implémentation d'une \DL{} \ZT{} (e.g. calcul homomorphe).
+    \item \textbf{Implémentation} : prototype intégré à \texttt{parsec} pour la fonctionnalités de chat collaboratif (en cours).
+  \end{itemize}
+  \end{frame}
+
+% =====================
+
+  \begin{frame}[t]{Gantt 2024-2025}
+    \scriptsize
+    % Fenêtre temporelle
+    \GanttSetup{2024-10-01}{2025-10-15}
+    
+    % Limiter à la largeur et à 80% de la hauteur de la slide
+    \begin{adjustbox}{max totalsize={\textwidth}{0.8\textheight},center}
+      \begin{ganttchart}[
+          expand chart=\textwidth,
+          y unit chart=0.45cm,
+          y unit title=0.6cm,
+          bar height=0.35,
+      ]{\GanttStart}{\GanttEnd}
+        \gantttitlecalendar{year, month}\\
+    
+        \Period{REDOCS}{2024-10-14}{2024-10-18}\\
+        % Plusieurs jalons sur une même ligne pour gagner de la place
+        \Event{Séminaire Parsec}{2024-11-19}\ \Event{}{2025-03-20}\ \Event{}{2025-07-12}\\
+        \Event{PEPR TrustInCloud}{2024-12-05}\ \Event{}{2025-10-07}\\
+    
+        \Period[bar/.append style={fill=green!40}]{Livrable BPI}{2025-01-01}{2025-02-01}\\
+        \Period[bar/.append style={fill=green!40}]{État de l'art OTAN}{2025-04-01}{2025-04-30}\\
+        \Period[bar/.append style={fill=green!40}]{Conseil sauvegarde P2P}{2025-08-01}{2025-08-15}\\
+        \Period[bar/.append style={fill=green!40}]{Rédaction CIR}{2025-09-01}{2025-10-15}\\
+    
+        \Period[bar/.append style={fill=orange!70}]{Cours M1}{2024-10-01}{2024-12-31}\\
+    
+        \Period[bar/.append style={fill=blue!35}]{PCDO BFT vs RB BFT}{2024-10-01}{2025-01-01}\\
+        \Period[bar/.append style={fill=blue!35}]{Spécification RB+DL=>ARB (crash)}{2025-02-01}{2025-10-15}\\
+      \end{ganttchart}
+    \end{adjustbox}
+    \end{frame}
+
+  % =======================
+  \begin{frame}{Perspectives Académiques 2025-2026}
+    \begin{itemize}
+      \item \textbf{Publication} : soumission d’un article sur \RB{} + \DL{} $\Rightarrow$ \ARB{} en modèle \BFT{} (\textbf{printemps 2026}).
+      \item \textbf{Soumission de la thèse} : rédaction \textbf{fin 2026}, soutenance \textbf{1er semestre 2027}.
+      \begin{itemize}
+        \item Implique une 4ème année de thèse (financement à confirmer avec Scille).
+      \end{itemize}
+    \end{itemize} 
+  \end{frame}
+
+  \end{document}
+  

docs/presentations/LIS/CSI2025/rapport/main.tex

@@ -0,0 +1,222 @@
+
+\documentclass[11pt,a4paper]{article}
+\usepackage[utf8]{inputenc}
+\usepackage[T1]{fontenc}
+\usepackage[french]{babel}
+\usepackage{geometry}
+\geometry{margin=2.2cm}
+\usepackage{graphicx}
+\usepackage{array}
+\usepackage{tabularx}
+\usepackage{longtable}
+\usepackage{booktabs}
+\usepackage{multirow}
+\usepackage{enumitem}
+\usepackage{amssymb}
+\usepackage{fancyhdr}
+\usepackage{pgfgantt}
+\usepackage{hyperref}
+\usepackage{xcolor}
+
+% ---------- Header / Footer with logo top-left on every page ----------
+\pagestyle{fancy}
+\fancyhf{} % clear
+% Replace 'logo_header.pdf' with your actual logo file (AMU/LIS or Scille). Height can be adjusted.
+\fancyhead[L]{\includegraphics[height=12mm]{logo_header.pdf}}
+\fancyfoot[C]{\thepage}
+
+% Avoid underlines for empty fields — we will leave space or boxes instead.
+
+% Table helpers
+\setlength{\extrarowheight}{1pt}
+\renewcommand{\arraystretch}{1.18}
+\newcolumntype{L}[1]{>{\raggedright\arraybackslash}p{#1}}
+\newcolumntype{C}[1]{>{\centering\arraybackslash}p{#1}}
+\newcolumntype{R}[1]{>{\raggedleft\arraybackslash}p{#1}}
+\setlist[itemize]{topsep=2pt,partopsep=0pt,itemsep=2pt,parsep=0pt}
+\setlist[enumerate]{topsep=2pt,partopsep=0pt,itemsep=2pt,parsep=0pt}
+
+% Checkboxes
+\newcommand{\cb}{\(\square\)}
+\newcommand{\cbdone}{\(\blacksquare\)} % when needed
+
+% Title info
+\title{\vspace{-1.5cm}\textbf{Rapport d'activité — 2\`eme Comité de Suivi Individuel (CSI) 2024--2025}\\[2mm]
+\large Thèse CIFRE --- Édition collaborative appliquée au cloud zero-trust}
+\author{Doctorant : Amaury JOLY \\
+Encadrement : Emmanuel GODARD, Corentin TRAVERS \\
+Comité de suivi : Arnaud LABOUREL, Achour MOSTEFAOUI \\
+Affiliations : Université Aix-Marseille (LIS), Scille}
+\date{14 octobre 2025}
+
+\begin{document}
+% ---------- Title page with logo top-left ----------
+\thispagestyle{fancy}
+\maketitle
+\vspace{-8mm}
+\begin{center}
+\includegraphics[height=18mm]{logo_header.pdf}
+\end{center}
+\vspace{4mm}
+\hrule
+\vspace{2mm}
+
+\section*{Résumé}
+Ce rapport présente les activités menées entre octobre 2024 et octobre 2025 dans le cadre de la thèse CIFRE d'Amaury JOLY, portant sur l'édition collaborative appliquée au cloud \emph{zero-trust}. Il reprend la structure et le style du rapport précédent tout en intégrant les éléments académiques, industriels et de recherche de l'année écoulée.\\[2mm]
+
+\section{Informations générales}
+\begin{tabularx}{\textwidth}{L{4.5cm}X}
+\toprule
+\textbf{Doctorant} & Amaury JOLY \\
+\textbf{Encadrants universitaires} & Emmanuel GODARD, Corentin TRAVERS \\
+\textbf{Entreprise (CIFRE)} & Scille (produit: \texttt{parsec.cloud}) \\
+\textbf{Comité de suivi (CSI)} & Arnaud LABOUREL, Achour MOSTEFAOUI \\
+\textbf{Démarrage administratif} & Janvier 2023 \\
+\textbf{Répartition d'activités} & 70\% recherche / 30\% entreprise \\
+\bottomrule
+\end{tabularx}
+
+\section{Contexte de thèse et industriel}
+\subsection{Sujet et cadre}
+Thèse CIFRE sur l'édition collaborative appliquée au cloud \emph{zero-trust} (ZT).
+
+\subsection{Contexte industriel --- partage de fichiers ZT}
+Produit visé : logiciel de partage de fichiers ZT. Hypothèses~: le serveur ne voit que des données chiffrées, ne connaît pas l'identité des utilisateurs ; modèle de communication centralisé (un serveur pour tous les clients) ; hypothèses de confiance limitées pour la redistribution et la disponibilité, serveur honnête mais curieux.
+
+\section{Bilan des formations, enseignement et diverses activités (oct. 2024 --- oct. 2025)}
+\subsection{Formations / événements}
+\begin{itemize}
+  \item \textbf{REDOCS 2024} : 14--19 octobre 2024.
+  \item \textbf{PEPR Trust in Cloud 2024 (Grenoble)} : novembre 2024.
+  \item \textbf{PEPR Trust in Cloud 2025 (Massy)} : octobre 2025.
+  \item \textbf{Séminaires entreprise} : 3 séances en présentiel.
+  \item \textbf{Réunions produit \& R\&D} : toutes les deux semaines.
+\end{itemize}
+
+\subsection{Enseignement}
+\begin{itemize}
+  \item \textbf{M1} : 30 h (24 h TP + 6 h TD).
+\end{itemize}
+
+\section{Missions en entreprise (synthèse)}
+\begin{itemize}
+  \item Document \textbf{BPI} : état de l’art et valeur ajoutée des fonctionnalités d’édition collaborative (équipe R\&D Parsec).
+  \item \textbf{ZT \& Data-Centric Security} : état de l’art pour une réponse à appel d’offres OTAN.
+  \item \textbf{Conseil} : stratégie de sauvegarde dans un contexte pair-à-pair distribué pour l’édition collaborative.
+  \item \textbf{CIR} : rédaction d’un document consolidé couvrant les projets R\&D (état de l’art, besoins spécifiques, caractère innovant, avancées annuelles).
+  \item \textbf{Développement} : fonctionnalités expérimentales dans \texttt{parsec}.
+\end{itemize}
+
+\section{Avancement scientifique}
+\subsection{Rappels : CRDT}
+Les CRDT (Shapiro \emph{et al.}, 2011) spécifient des types de données répliqués atteignant la \emph{cohérence éventuelle} (EC) sans ordre total global, sous hypothèse de \emph{Reliable Broadcast} (RB). L’idée clé est la convergence par construction grâce à la commutativité (souvent associativité et idempotence) des opérations ou jointures d’états. Limites : moins adapté quand des invariants globaux non commutatifs ou des contraintes d’ordre sont requis.
+
+\subsection{PCDO (Frey \emph{et al.}, 2023)}
+Les PCDO étendent les CRDT avec un prédicat de \emph{légalité} d’état. Ils autorisent d’exiger un ordre \emph{par processus} pour certaines opérations, tout en préservant l’asynchronisme et la EC pour les opérations inter-processus (commutatives au sens du prédicat de légalité).
+
+\subsection{Question en cours : \textit{PCDO ?= RB BFT}}
+Question : une implémentation BFT d’un PCDO est-elle équivalente à une implémentation BFT d’un RB ? Travail en cours (pas de résultat concluant à ce jour) : exploration d’algorithmes et des interactions entre légalité locale (par processus) et garanties globales de RB-BFT (accord, intégrité, terminaison).
+
+\subsection{AllowList / DenyList (travaux récents)}
+Spécification d’AllowList (AL) et DenyList (DL) comme registre partagé en système asynchrone avec crashs ; interface fondée sur \texttt{APPEND(x)}, \texttt{PROVE(x)} et \texttt{READ()} ; objectifs : sécurité, auditabilité, progression.
+
+\subsection{Vers ARB avec \textbf{RB + DL} : intuition et contexte ZT}
+\paragraph{Intuition.} Utiliser DL comme mécanisme de verrou/élection pour ordonner les messages livrés via RB et obtenir un \emph{Atomic Reliable Broadcast} (ARB). Fonctionnement par \emph{rounds} :\\[-5pt]
+\begin{enumerate}
+  \item À chaque round, un ensemble non vide de vainqueurs est élu (via DL) et détient le droit d’émettre.
+  \item À la fermeture du round, les autres processus tentent d’être élus au round suivant.
+\end{enumerate}
+Pour les processus lents, un mécanisme de dissémination force le relais/émission afin d’éviter les blocages, et l’ordonnancement par rounds induit un ordre total.
+
+\paragraph{Contexte industriel ZT.} Dans certains usages, les CRDT/PCDO ne suffisent pas : un ordre total global est nécessaire malgré l’asynchronisme. Hypothèse architecturale : un serveur \emph{proxy} ZT (médiateur d’ordonnancement, sans logique métier ni accès en clair) qui \emph{dispatch} et synchronise des messages chiffrés. L’objectif est de rester \emph{zero-trust} tout en centralisant l’ordonnancement au strict nécessaire.
+
+\subsection{État d’avancement (RB + DL $\Rightarrow$ ARB)}
+\begin{itemize}
+  \item \textbf{Algorithme} : spécifié ; preuve en cours de finalisation dans un modèle crash.
+  \item \textbf{Propriété visée} : ARB (accord, validité, intégrité, ordre total).
+  \item \textbf{Perspectives} : extension au modèle byzantin (BFT) ; implémentation d’une DL ZT (p.~ex. calcul homomorphe).
+  \item \textbf{Implémentation} : prototype intégré à \texttt{parsec} pour la fonctionnalité de \emph{chat} collaboratif (en cours).
+\end{itemize}
+
+\section{Planification --- Gantt 2024--2025}
+\begin{center}
+\resizebox{\textwidth}{!}{%
+\begin{ganttchart}[
+  time slot format=isodate,
+  y unit chart=0.7cm,
+  vgrid,
+  hgrid
+]{2024-10-01}{2025-10-01}
+\gantttitlecalendar{year, month=name} \\
+\ganttbar{REDOCS}{2024-10-14}{2024-10-19} \\
+\ganttbar{Séminaires Parsec}{2024-10-01}{2025-10-01} \\
+\ganttbar{PEPR TrustInCloud (Grenoble)}{2024-11-01}{2024-11-30} \\
+\ganttbar{Livrable BPI}{2024-12-01}{2025-01-31} \\
+\ganttbar{État de l'art OTAN}{2025-01-01}{2025-02-28} \\
+\ganttbar{Conseil sauvegarde P2P}{2025-02-01}{2025-03-31} \\
+\ganttbar{Rédaction CIR}{2025-03-01}{2025-05-31} \\
+\ganttbar{Cours M1}{2025-09-01}{2025-10-01} \\
+\ganttbar{PCDO BFT vs RB BFT}{2024-10-01}{2025-06-30} \\
+\ganttbar{Spécif. RB+DL $\Rightarrow$ ARB (crash)}{2025-04-01}{2025-10-01}
+\end{ganttchart}
+}
+\end{center}
+
+\section{Production scientifique, valorisation, expérience internationale}
+% Two-column checkboxes layout + single cell for Avis / Points / Reco
+\begin{longtable}{L{0.35\textwidth}L{0.3\textwidth}L{0.3\textwidth}}
+\toprule
+\textbf{Catégorie} & \textbf{Activités (cases à cocher)} & \textbf{Détails (si applicable)}\\
+\midrule
+\endfirsthead
+\toprule
+\textbf{Catégorie} & \textbf{Activités (cases à cocher)} & \textbf{Détails (si applicable)}\\
+\midrule
+\endhead
+\textbf{Production scientifique} & \cb~Article journal \quad \cb~Conf. int. \quad \cb~Conf. nat. \quad \cb~Préprint & \\[2mm]
+\textbf{Valorisation / Transfert} & \cb~Livrable \quad \cb~Logiciel (OSS) \quad \cb~Démonstrateur & \\[2mm]
+\textbf{Expérience internationale} & \cb~Séjour (dates:\hspace{1.5cm}) \quad \cb~Collab. int. & \\
+\bottomrule
+\end{longtable}
+
+\vspace{1mm}
+\noindent\textbf{Avis, Points de vigilance, Recommandations}\\[1mm]
+\begin{tabularx}{\textwidth}{|X|}
+\hline
+\vspace{0pt}\textbf{Avis} : \vspace{20mm}\\
+\textbf{Points de vigilance} : \vspace{20mm}\\
+\textbf{Recommandations} : \vspace{25mm}\\ \\
+\hline
+\end{tabularx}
+
+\section{Conditions de la formation doctorale (alignement amélioré)}
+\begin{tabularx}{\textwidth}{L{0.45\textwidth}X}
+\toprule
+\textbf{Sujet de thèse} & Édition collaborative appliquée au cloud zero-trust \\
+\textbf{École doctorale} & (à compléter) \\
+\textbf{Laboratoire} & LIS (AMU) \\
+\textbf{Financement} & CIFRE (Scille) \\
+\textbf{Formations suivies} & REDOCS 2024 ; PEPR Trust in Cloud 2024/2025 \\
+\textbf{Enseignement} & M1 : 30 h (24 h TP + 6 h TD) \\
+\textbf{Autres} & Séminaires entreprise (3) ; réunions produit/R\&D bi-hebdo \\
+\bottomrule
+\end{tabularx}
+
+\section{Perspectives académiques 2025--2026}
+\begin{itemize}
+  \item \textbf{Publication} : soumission d’un article \emph{RB + DL $\Rightarrow$ ARB} en modèle BFT (printemps 2026).
+  \item \textbf{Thèse} : début de rédaction fin 2026 ; soutenance visée au 1\textsuperscript{er} semestre 2027 (implique une 4\`eme année --- financement à confirmer avec Scille).
+\end{itemize}
+
+\section*{Espace réservé au compte rendu du CSI (à remplir le jour J)}
+\begin{tabularx}{\textwidth}{|L{0.22\textwidth}|X|}
+\hline
+\textbf{Participants} & \\[10mm]\hline
+\textbf{Synthèse des échanges} & \\[30mm]\hline
+\textbf{Décisions / Actions} & \\[20mm]\hline
+\end{tabularx}
+
+\vfill
+\noindent\footnotesize{Remarques de mise en page : (i) logo en haut à gauche sur toutes les pages ; (ii) pas de soulignement des champs vides ; (iii) listes en tableaux alignées en haut des cellules ; (iv) structure fidèle au rapport précédent ; (v) sections \og Avis, Points de vigilance, Recommandations\fg{} regroupées en une même cellule.}
+
+\end{document}

docs/presentations/autre/capitoledulibre/main.tex

@@ -0,0 +1,647 @@
+\documentclass[aspectratio=43]{beamer}
+
+\usetheme{Berlin}
+%\usefonttheme{professionalfonts}
+
+\usepackage[utf8]{inputenc}
+\usepackage[T1]{fontenc}
+\usepackage[french]{babel}
+\usepackage{mathtools,amssymb}
+\usepackage{microtype}
+\usepackage{pgfgantt}
+\usepackage{adjustbox}
+\usetikzlibrary{positioning}
+% \usepackage{qrcode}
+
+\title[]{Systèmes centralisés, fédérés et pair à pair : vu par la théorie des graphs}
+\author{Amaury JOLY}
+\institute[AMU - Skeptikon - Parsec]{Aix-Marseille université, Skeptikon, Parsec.cloud}
+
+\begin{document}
+
+\begin{frame}{}
+    \titlepage
+\end{frame}
+
+\note{test}
+\begin{frame}{Qui suis-je}
+    \begin{itemize}
+        \item \textbf{Doctorant} en informatique distribué
+        \begin{itemize}
+            \item \textit{Étude de la cohérence des données dans les systèmes distribués}
+        \end{itemize}
+        \item Ingénieur R\&D chez \textbf{Parsec.cloud}
+        \item Membre de l'association \textbf{Skeptikon}
+    \end{itemize}
+\end{frame}
+
+\section{Introduction a l'algorithmie distribué}
+
+\begin{frame}{Un système distribué c'est quoi}
+    \begin{quote}
+        On définit un système comme un ensemble de processus. On considère qu'un système est dit distribué lorsque plusieurs processus distincts travail à la réalisation d'une tâche commune.
+    \end{quote}
+
+    \vspace{1em}
+    Par exemple la rédaction de documents collaboratifs (ex: cryptpad, grist, colabora), le chat (ex: matrix, signal, XMPP, IRC, IMAP), le partage d'annuaire de vidéo (ex: PeerTube), la résolution des noms de domaines (DNS).
+\end{frame}
+
+\begin{frame}{Définir un système distribué: le modèle de communication}
+    La recherche traite globalement deux modèles de communication 
+    \begin{itemize}
+        \item Shared-Register
+
+        \pause
+        
+        \resizebox{0.5\linewidth}{!}{%
+          \begin{tikzpicture}[
+            node distance=1.8cm and 2.4cm,
+            process/.style={draw, circle, thick, minimum size=1cm, font=\small},
+            mem/.style={draw, thick, rounded corners, minimum width=5cm, minimum height=1.8cm, fill=gray!10},
+            reg/.style={draw, thin, minimum width=1.1cm, minimum height=0.7cm, font=\scriptsize},
+            arrow/.style={-Latex, thick}
+          ]
+        
+          % --- Mémoire partagée (abstraction) ---
+          \node[mem] (mem) {};
+        
+          % Quelques registres logiques dans la mémoire
+          \node[reg] (r1) at ($(mem.west)!0.2!(mem.east)$) {$R_1$};
+          \node[reg] (r2) at ($(mem.west)!0.5!(mem.east)$) {$R_\dots$};
+          \node[reg] (r3) at ($(mem.west)!0.8!(mem.east)$) {$R_n$};
+        
+          \node[font=\scriptsize, below=0.15cm of mem]{Tous les processus voient la même mémoire logique};
+        
+          % --- Processus concurrents ---
+          \node[process] (p1) [left=of p2] {$P_1$};
+          \node[process] (p2) [above=1.8cm of mem] {$P_\dots$};
+          \node[process] (p3) [right=of p2] {$P_n$};
+        
+          % --- Accès mémoire : opérations read/write ---
+          \draw[arrow] (p1.south) -- (r1.north);
+          \draw[arrow] (p1.south) -- (r2.north);
+          \draw[arrow] (p1.south) -- (r3.north);
+          \draw[arrow] (p2.south) -- (r2.north);
+          \draw[arrow] (p2.south) -- (r1.north);
+          \draw[arrow] (p2.south) -- (r3.north);
+          \draw[arrow] (p3.south) -- (r1.north);
+          \draw[arrow] (p3.south) -- (r2.north);
+          \draw[arrow] (p3.south) -- (r3.north);
+        
+          \end{tikzpicture}
+        }
+    \end{itemize}
+\end{frame}
+
+\begin{frame}{Définir un système distribué: le modèle de communication}
+    \begin{itemize}
+        \item Shared-Register
+        \item \textbf{Message-passing}
+
+        \centering
+        \resizebox{0.2\linewidth}{!}{%
+          \begin{tikzpicture}[
+            node distance=2.2cm and 1.4cm,
+            process/.style={draw, circle, thick, minimum size=1cm, font=\small},
+            state/.style={draw, thin, rounded corners, minimum width=1.6cm, 
+                          minimum height=0.7cm, font=\scriptsize, fill=gray!10},
+            msg/.style={-Latex, thick},
+            netbox/.style={draw, dashed, rounded corners, thick, inner sep=0.4cm}
+          ]
+        
+          % --- Processus avec état local ---
+          \node[process] (p1) {$P_1$};
+          \node[process] (p2) [above=of p1] {$P_2$};
+          \node[process] (p3) [right=of p1] {$P_3$};
+        
+          \node[state] (s1) [below=0.7cm of p1] {état local $S_1$};
+          \node[state] (s2) [above=0.7cm of p2] {état local $S_2$};
+          \node[state] (s3) [below=0.7cm of p3] {état local $S_3$};
+        
+          % --- Messages entre processus ---
+          \draw[msg] (p1) to[bend left=15] node[above, font=\scriptsize]{message $m_1$} (p2);
+          \draw[msg] (p2) to[bend left=15] node[above, font=\scriptsize]{message $m_2$} (p3);
+          \draw[msg] (p3) to[bend left=15] node[above, font=\scriptsize]{message $m_3$} (p1);
+                
+          \end{tikzpicture}
+        }%
+        
+    \end{itemize}
+\end{frame}
+
+\begin{frame}{Définir un système distribué: le modèle de synchronisme}
+    La recherche distingue deux grandes hypothèses de synchronisme :
+    \begin{itemize}
+        \item \textbf{Synchrone} (temps découpé en tours / rounds)
+
+        \pause
+        
+        \centering
+        \resizebox{0.7\linewidth}{!}{%
+          \begin{tikzpicture}[
+            x=1.4cm, y=0.9cm,
+            msg/.style={-Latex, thick},
+            proc/.style={font=\small},
+            roundline/.style={thick},
+            sep/.style={dashed, gray}
+          ]
+          
+          % --- Processus ---
+          \node[proc, anchor=east] at (0,0)   {$P_1$};
+          \node[proc, anchor=east] at (0,-1)  {$P_2$};
+          \node[proc, anchor=east] at (0,-2)  {$P_3$};
+
+          % --- Lignes de temps pour chaque processus ---
+          \foreach \y in {0,-1,-2}{
+            \draw[roundline] (0.2,\y) -- (3.0,\y);
+          }
+
+          % --- Séparation en tours synchrones ---
+          \foreach \x/\t in {0.8/1,1.6/2,2.4/3}{
+            \draw[sep] (\x,0.3) -- (\x,-2.3);
+            \node[font=\scriptsize] at (\x+0.35,0.35) {tour \t};
+          }
+
+          % --- Messages livrés dans le tour suivant ---
+          \draw[msg] (0.35,0)   .. controls (0.55,-0.2) .. (0.75,-1);   % P1 -> P2 dans le tour 1
+          \draw[msg] (1.0,-1)   .. controls (1.2,-1.8) .. (1.4,-2);     % P2 -> P3 dans le tour 2
+          \draw[msg] (1.7,-2)   .. controls (1.9,-1.2) .. (2.1,0);      % P3 -> P1 dans le tour 3
+
+          % --- Légende ---
+          \node[font=\scriptsize, align=center] at (1.6,-2.6){Bornes connues sur les durées de calcul et de communication,\\
+             tous les processus avancent par tours synchrones};
+          
+          \end{tikzpicture}
+        }
+    \end{itemize}
+\end{frame}
+
+\begin{frame}{Définir un système distribué: les modèles de synchronisme}
+    \begin{itemize}
+        \item Synchrone
+        \item \textbf{Asynchrone}
+    \end{itemize}
+
+    \pause
+
+    \centering
+    \resizebox{0.7\linewidth}{!}{%
+      \begin{tikzpicture}[
+        x=1.4cm, y=0.9cm,
+        msg/.style={-Latex, thick},
+        proc/.style={font=\small},
+        opbox/.style={draw, rounded corners, thick}
+      ]
+      
+        % --- Processus ---
+        \node[proc, anchor=east] at (0,0)   {$P_1$};
+        \node[proc, anchor=east] at (0,-1)  {$P_2$};
+        \node[proc, anchor=east] at (0,-2)  {$P_3$};
+
+        \pause
+
+        % --- Lignes de temps pour chaque processus ---
+        \foreach \y in {0,-1,-2}{
+          \draw[thick] (0.2,\y) -- (3.0,\y);
+        }
+
+        \pause
+
+        % --- "Ticks" locaux non alignés (horloges indépendantes) ---
+        \foreach \x in {0.5,1.2,2.3}{
+          \draw (\x,0.1) -- (\x,-0.1);       % P1
+        }
+        \foreach \x in {0.4,1.5,2.6}{
+          \draw (\x,-0.9) -- (\x,-1.1);      % P2
+        }
+        \foreach \x in {0.7,1.8,2.1}{
+          \draw (\x,-1.9) -- (\x,-2.1);      % P3
+        }
+
+        \pause
+
+        % --- Messages ---
+        \draw[msg] (0.35,0) -- (0.8,-1);
+        \draw[msg] (0.35,0) -- (2.5,-2);
+
+        \pause
+
+        \draw[msg] (1.0,-1) -- (1.8,0);
+        \draw[msg] (1.0,-1) -- (2.2,-2);
+
+        \pause
+
+        \draw[msg] (1.4,-2) -- (2.1,0);
+        \draw[msg] (1.4,-2) -- (2.5,-1);
+
+        \pause
+        % op_1 : diffusion de P1
+        % commence à x = 0.35 (émission) et finit à x = 2.5 (dernier reçu : P3)
+        \draw[opbox,densely dotted] (0.35,0.25) rectangle (2.5,-0.25);
+        % ligne de vie de P1 en pointillé dans l'intervalle de op_1
+        \draw[thick,densely dotted] (0.35,0) -- (2.5,0);
+        \node[font=\scriptsize, anchor=west] at (2.55,-0.2) {$op_1$};
+
+        \pause
+        % op_2 : diffusion de P2
+        % commence à x = 1.0 (émission) et finit à x = 2.2 (dernier reçu : P3)
+        \draw[opbox,densely dotted] (1.0,-0.75) rectangle (2.2,-1.25);
+        % ligne de vie de P2 en pointillé dans l'intervalle de op_2
+        \draw[thick,densely dotted] (1.0,-1) -- (2.2,-1);
+        \node[font=\scriptsize, anchor=west] at (2.25,-1.2) {$op_2$};
+        
+        \pause
+        % op_3 : diffusion de P3
+        % commence à x = 1.4 (émission) et finit à x = 2.5 (dernier reçu : P2)
+        \draw[opbox,densely dotted] (1.4,-1.75) rectangle (2.5,-2.25);
+        % ligne de vie de P3 en pointillé dans l'intervalle de op_3
+        \draw[thick,densely dotted] (1.4,-2) -- (2.5,-2);
+        \node[font=\scriptsize, anchor=west] at (2.55,-2.2) {$op_3$};
+
+      \end{tikzpicture}
+    }
+\end{frame}
+
+\begin{frame}{Définir un système distribué: les modèles de synchronisme}
+    \begin{itemize}
+        \item Synchrone
+        \item \textbf{Asynchrone}
+    \end{itemize}
+
+    \centering
+    \resizebox{0.7\linewidth}{!}{%
+      \begin{tikzpicture}[
+        x=1.4cm, y=0.9cm,
+        msg/.style={-Latex, thick},
+        proc/.style={font=\small},
+        opbox/.style={draw, rounded corners, thick}
+      ]
+      
+        % --- Processus ---
+        \node[proc, anchor=east] at (0,0)   {$P_1$};
+        \node[proc, anchor=east] at (0,-1)  {$P_2$};
+        \node[proc, anchor=east] at (0,-2)  {$P_3$};
+
+        % --- Lignes de temps pour chaque processus ---
+        \foreach \y in {0,-1,-2}{
+          \draw[thick] (0.2,\y) -- (3.0,\y);
+        }
+
+        % op_1 : diffusion de P1
+        % commence à x = 0.35 (émission) et finit à x = 2.5 (dernier reçu : P3)
+        \draw[opbox,densely dotted] (0.35,0.25) rectangle (2.5,-0.25);
+        % ligne de vie de P1 en pointillé dans l'intervalle de op_1
+        \draw[thick,densely dotted] (0.35,0) -- (2.5,0);
+        \node[font=\scriptsize, anchor=west] at (2.55,-0.2) {$op_1$};
+
+        % op_2 : diffusion de P2
+        % commence à x = 1.0 (émission) et finit à x = 2.2 (dernier reçu : P3)
+        \draw[opbox,densely dotted] (1.0,-0.75) rectangle (2.2,-1.25);
+        % ligne de vie de P2 en pointillé dans l'intervalle de op_2
+        \draw[thick,densely dotted] (1.0,-1) -- (2.2,-1);
+        \node[font=\scriptsize, anchor=west] at (2.25,-1.2) {$op_2$};
+        
+        % op_3 : diffusion de P3
+        % commence à x = 1.4 (émission) et finit à x = 2.5 (dernier reçu : P2)
+        \draw[opbox,densely dotted] (1.4,-1.75) rectangle (2.5,-2.25);
+        % ligne de vie de P3 en pointillé dans l'intervalle de op_3
+        \draw[thick,densely dotted] (1.4,-2) -- (2.5,-2);
+        \node[font=\scriptsize, anchor=west] at (2.55,-2.2) {$op_3$};
+
+      \end{tikzpicture}
+    }
+\end{frame}
+
+\section{Les différentes architectures de systèmes}
+
+\subsection{Les systèmes centralisés}
+
+\begin{frame}{Système centralisé}
+    \begin{itemize}
+        \item Architecture client--serveur
+        \item Un seul serveur central maintient l'état
+    \end{itemize}
+
+    \vspace{0.3cm}
+    \centering
+    \resizebox{0.6\linewidth}{!}{%
+      \begin{tikzpicture}[
+        node distance=1.8cm and 2.5cm,
+        client/.style={draw, circle, thick, minimum size=1cm, font=\small},
+        server/.style={draw, thick, rounded corners, minimum width=2.8cm, 
+                       minimum height=1.2cm, font=\small, fill=gray!10},
+        msg/.style={-Latex, thick},
+        resp/.style={Latex-, thick, dashed}
+      ]
+
+        % --- Serveur central ---
+        \node[server] (srv) at (0,0) {Serveur central};
+
+        % --- Clients ---
+        \node[client] (c1) at (-3,0) {$P_1$};
+        \node[client] (c2) at (0,-2) {$P_2$};
+        \node[client] (c3) at (3,-0) {$P_3$};
+
+        % --- Messages requête / réponse ---
+        \draw[msg]  (c1.east) -- (srv.west);
+        \draw[msg]  (c2.north) -- (srv.south);
+        \draw[msg]  (c3.west) -- (srv.east);
+
+      \end{tikzpicture}
+    }
+\end{frame}
+
+
+\begin{frame}{Système centralisé : exécution parallèle des clients}
+    \begin{itemize}
+        \item Requêtes concurrentes côté clients
+        \item Traitement séquentiel côté serveur (ordre total)
+    \end{itemize}
+
+    \vspace{0.3cm}
+    \centering
+    \resizebox{0.6\linewidth}{!}{%
+      \begin{tikzpicture}[
+        x=1.4cm, y=0.9cm,
+        msg/.style={-Latex, thick},
+        proc/.style={font=\small},
+        opbox/.style={draw, rounded corners, thick, fill=gray!10}
+      ]
+
+        % --- Processus : serveur + clients (lignes de vie) ---
+        \node[proc, anchor=east] at (0,0)    {$Serveur$};
+        \node[proc, anchor=east] at (0,-1)   {$P_1$};
+        \node[proc, anchor=east] at (0,-2)   {$P_2$};
+        \node[proc, anchor=east] at (0,-3)   {$P_3$};
+
+        \pause
+
+        % --- Lignes de temps ---
+        \foreach \y in {0,-1,-2,-3}{
+          \draw[thick] (0.2,\y) -- (4.0,\y);
+        }
+
+        \pause
+        % --- Requêtes des clients vers le serveur (légèrement décalées) ---
+        \draw[msg] (0.8,-1) -- (1.2,0)
+           node[midway, left, font=\scriptsize] {$op_1$};
+        \draw[msg] (0.9,-2) -- (1.3,0)
+           node[midway, left, font=\scriptsize] {$op_2$};
+        \draw[msg] (1.0,-3) -- (1.4,0)
+           node[midway, left, font=\scriptsize] {$op_3$};
+
+        % (On suggère qu'elles sont émises "en parallèle" côté clients.)
+
+        \pause
+        % --- Traitement séquentiel au serveur : op_1, op_2, op_3 ---
+        % op_1
+        \node[opbox, minimum width=0.2cm, minimum height=0.5cm] (o1) at (1.8,0) {$op_1$};
+        % op_2
+        \node[opbox, minimum width=0.2cm, minimum height=0.5cm, right=0.2cm of o1] (o2) {$op_2$};
+        % op_3
+        \node[opbox, minimum width=0.2cm, minimum height=0.5cm, right=0.2cm of o2] (o3) {$op_3$};
+
+        % Relier dans l'ordre pour bien montrer la séquentialisation
+        \draw[->, thick] (o1.east) -- (o2.west);
+        \draw[->, thick] (o2.east) -- (o3.west);
+
+        % --- Réponses (optionnelles, pour fermer la boucle) ---
+        \pause
+        \draw[msg] (o1.south) -- (2,-1);
+        \draw[msg] (o1.south) -- (2,-2);
+        \draw[msg] (o1.south) -- (2,-3);
+        \draw[msg] (o2.south) -- (2.8,-1);
+        \draw[msg] (o2.south) -- (2.8,-2);
+        \draw[msg] (o2.south) -- (2.8,-3);
+        \draw[msg] (o3.south) -- (3.8,-1);
+        \draw[msg] (o3.south) -- (3.8,-2);
+        \draw[msg] (o3.south) -- (3.8,-3);
+
+        % --- Évolution de l'état (optionnel mais parlant) ---
+        \node[font=\scriptsize, align=left] at (2.7,0.9)
+           {$S_0 \xrightarrow{op_1} S_1 \xrightarrow{op_2} S_2 \xrightarrow{op_3} S_3$};
+      \end{tikzpicture}
+    }
+\end{frame}
+
+\subsection{Les systèmes pair à pair}
+
+\begin{frame}{Système pair à pair}
+    \begin{itemize}
+        \item Pas de serveur central
+        \item Chaque processus entretient son état local en fonction des messages recu.
+    \end{itemize}
+
+    \vspace{0.3cm}
+    \centering
+    \resizebox{0.6\linewidth}{!}{%
+      \begin{tikzpicture}[
+        node distance=1.8cm and 2.5cm,
+        peer/.style={draw, circle, thick, minimum size=1cm, font=\small},
+        link/.style={<->, thick}
+      ]
+
+        % --- Pairs ---
+        \node[peer] (p1) at (-2,0) {$P_1$};
+        \node[peer] (p2) at ( 2,0) {$P_2$};
+        \node[peer] (p3) at ( 0,-2) {$P_3$};
+
+        % --- Connexions pair à pair ---
+        \draw[link] (p1) -- (p2);
+        \draw[link] (p1) -- (p3);
+        \draw[link] (p2) -- (p3);
+
+      \end{tikzpicture}
+    }
+\end{frame}
+
+\begin{frame}{Système pair à pair : exécution parallèle}
+    \begin{itemize}
+        \item Chaque pair exécute des opérations concurrentes
+        \item Pas de serveur central pour imposer un ordre total
+    \end{itemize}
+
+    \centering
+    \resizebox{0.7\linewidth}{!}{%
+      \begin{tikzpicture}[
+        x=1.4cm, y=0.9cm,
+        proc/.style={font=\small},
+        opbox/.style={draw, rounded corners, thick}
+      ]
+      
+        % --- Processus ---
+        \node[proc, anchor=east] at (0,0)   {$P_1$};
+        \node[proc, anchor=east] at (0,-1)  {$P_2$};
+        \node[proc, anchor=east] at (0,-2)  {$P_3$};
+
+        % --- Lignes de temps pour chaque processus ---
+        \foreach \y in {0,-1,-2}{
+          \draw[thick] (0.2,\y) -- (3.0,\y);
+        }
+
+        % op_1 : opération de P1
+        % commence à x = 0.35 et finit à x = 2.5
+        \draw[opbox,densely dotted] (0.35,0.25) rectangle (2.5,-0.25);
+        % ligne de vie de P_1 en pointillé dans l'intervalle de op_1
+        \draw[thick,densely dotted] (0.35,0) -- (2.5,0);
+        \node[font=\scriptsize, anchor=west] at (2.55,-0.2) {$op_1$};
+
+        % op_2 : opération de P2
+        % commence à x = 1.0 et finit à x = 2.2
+        \draw[opbox,densely dotted] (0.45,-0.75) rectangle (1.2,-1.25);
+        % ligne de vie de P_2 en pointillé dans l'intervalle de op_2
+        \draw[thick,densely dotted] (1.0,-1) -- (2.2,-1);
+        \node[font=\scriptsize, anchor=west] at (2.25,-1.2) {$op_2$};
+        
+        % op_3 : opération de P3
+        % commence à x = 1.4 et finit à x = 2.5
+        \draw[opbox,densely dotted] (1.4,-1.75) rectangle (2.5,-2.25);
+        % ligne de vie de P_3 en pointillé dans l'intervalle de op_3
+        \draw[thick,densely dotted] (1.4,-2) -- (2.5,-2);
+        \node[font=\scriptsize, anchor=west] at (2.55,-2.2) {$op_3$};
+
+      \end{tikzpicture}
+    }
+\end{frame}
+
+\subsection{Les systèmes fédérés}
+
+\begin{frame}{Système fédéré}
+    \begin{itemize}
+        \item Plusieurs serveurs, chacun gère un sous-ensemble de processus
+        \item Les serveurs se synchronisent entre eux (fédération)
+    \end{itemize}
+
+    \vspace{0.3cm}
+    \centering
+    \resizebox{0.4\linewidth}{!}{%
+      \begin{tikzpicture}[
+        node distance=1.8cm and 2.5cm,
+        server/.style={draw, thick, rounded corners, minimum width=2.8cm,
+                       minimum height=1.2cm, font=\small, fill=gray!10},
+        client/.style={draw, circle, thick, minimum size=0.9cm, font=\scriptsize},
+        srvlink/.style={<->, thick}
+      ]
+
+        % --- Serveurs fédérés ---
+        \node[server] (s1) at (0,1.5)  {Serveur $S_1$};
+        \node[server] (s2) at (-3,-0.5){Serveur $S_2$};
+        \node[server] (s3) at ( 3,-0.5){Serveur $S_3$};
+
+        % --- Processus locaux à chaque serveur ---
+        \node[client] (p1) at (0,3)  {$P_1$};
+        \node[client] (p2) at (-3,-2.5) {$P_2$};
+        \node[client] (p3) at ( 3,-2.5) {$P_3$};
+
+        % --- Liens client -- serveur local ---
+        \draw[-Latex, thick] (p1.south) -- (s1.north);
+        \draw[-Latex, thick] (p2.north) -- (s2.south);
+        \draw[-Latex, thick] (p3.north) -- (s3.south);
+
+        % --- Fédération entre serveurs ---
+        \draw[srvlink] (s1) -- (s2);
+        \draw[srvlink] (s1) -- (s3);
+        \draw[srvlink] (s2) -- (s3);
+
+      \end{tikzpicture}
+    }
+\end{frame}
+
+\begin{frame}{Système fédéré : exécution parallèle des serveurs}
+    \begin{itemize}
+        \item Chaque serveur impose un ordre total local sur ses opérations
+        \item Globalement, les opérations sur différents serveurs sont concurrentes
+    \end{itemize}
+
+    \centering
+    \resizebox{0.7\linewidth}{!}{%
+      \begin{tikzpicture}[
+        x=1.4cm, y=0.9cm,
+        proc/.style={font=\small},
+        opbox/.style={draw, rounded corners, thick}
+      ]
+      
+        % --- Processus (serveurs fédérés) ---
+        \node[proc, anchor=east] at (0,0)   {$S_1$};
+        \node[proc, anchor=east] at (0,-1)  {$S_2$};
+        \node[proc, anchor=east] at (0,-2)  {$S_3$};
+
+        % --- Lignes de temps pour chaque serveur ---
+        \foreach \y in {0,-1,-2}{
+          \draw[thick] (0.2,\y) -- (3.2,\y);
+        }
+
+        % op_1 : opération sur S_1 (longue)
+        \draw[opbox,densely dotted] (0.35,0.25) rectangle (2.3,-0.25);
+        \draw[thick,densely dotted] (0.35,0) -- (2.3,0);
+        \node[font=\scriptsize, anchor=west] at (2.35,-0.2) {$op_1$};
+
+        % op_2 : opération sur S_2 (décalée, plus courte)
+        \draw[opbox,densely dotted] (0.8,-0.75) rectangle (2.0,-1.25);
+        \draw[thick,densely dotted] (0.8,-1) -- (2.0,-1);
+        \node[font=\scriptsize, anchor=west] at (2.05,-1.2) {$op_2$};
+        
+        % op_3 : opération sur S_3 (commence plus tard, finit après op_2)
+        \draw[opbox,densely dotted] (1.3,-1.75) rectangle (2.8,-2.25);
+        \draw[thick,densely dotted] (1.3,-2) -- (2.8,-2);
+        \node[font=\scriptsize, anchor=west] at (2.85,-2.2) {$op_3$};
+
+      \end{tikzpicture}
+    }
+\end{frame}
+
+
+
+\begin{frame}{Jeu : placer les applications dans les architectures}
+    \begin{itemize}
+        \item À quel type d'architecture appartient chaque application ?
+    \end{itemize}
+
+    \vspace{0.3cm}
+    \centering
+    \resizebox{0.95\linewidth}{!}{%
+      \begin{tikzpicture}[
+        archibox/.style={draw, rounded corners, thick,
+                         minimum width=3.5cm, minimum height=1.6cm,
+                         font=\small, align=center, fill=gray!10},
+        app/.style={draw, rounded corners, thick,
+                    minimum width=2.0cm, minimum height=0.8cm,
+                    font=\scriptsize, align=center}
+      ]
+
+        % --- Zones d'architecture ---
+        \node[archibox] (central)   at (-4, 1.5) {Centralisé};
+        \node[archibox] (p2p)       at ( 0, 1.5) {Pair à pair};
+        \node[archibox] (federated) at ( 4, 1.5) {Fédéré};
+
+        % --- Jetons d'applications à placer ---
+        \node[app] at (-5, -0.2) {cryptpad};
+        \node[app] at (-2.5,-0.2) {grist};
+        \node[app] at ( 0, -0.2) {colabora};
+        \node[app] at ( 2.5,-0.2) {matrix};
+        \node[app] at ( 5, -0.2) {signal};
+
+        \node[app] at (-5, -1.8) {XMPP};
+        \node[app] at (-2.5,-1.8) {IRC};
+        \node[app] at ( 0, -1.8) {IMAP};
+        \node[app] at ( 2.5,-1.8) {PeerTube};
+        \node[app] at ( 5, -1.8) {DNS};
+
+      \end{tikzpicture}
+    }
+\end{frame}
+
+
+\begin{frame}{Un petit Quizz}
+    % \qrcode{partici.fi/38956702}
+\end{frame}
+
+\begin{frame}
+    \frametitle{MERCI !}
+
+    
+
+\end{frame}
+    
+
+\end{document}

misc/synthese2024/programme/main.tex

@@ -0,0 +1,138 @@
+\documentclass[a4paper,12pt]{article}
+
+\usepackage[utf8]{inputenc}
+\usepackage[T1]{fontenc}
+\usepackage[french]{babel}
+\usepackage{geometry}
+\usepackage{xcolor}
+\usepackage{graphicx}
+\usepackage{tabularx}
+\usepackage{array}
+\usepackage{setspace}
+
+\geometry{margin=1.5cm}
+\pagestyle{empty}
+
+% Quelques couleurs douces pour l'affiche
+\definecolor{maincolor}{RGB}{40,70,140}
+\definecolor{lightbg}{RGB}{230,236,250}
+
+\renewcommand{\familydefault}{\sfdefault} % Police sans serif
+\setlength{\parindent}{0pt}
+\renewcommand{\arraystretch}{1.5}
+
+\begin{document}
+\thispagestyle{empty}
+
+% --- Bandeau haut : logo + titre ---
+\begin{minipage}[t]{0.25\textwidth}
+    % Remplacer "logo.pdf" par le fichier de votre logo, ou commenter la ligne
+    %\includegraphics[width=\textwidth]{logo.pdf}
+\end{minipage}
+\hfill
+\begin{minipage}[t]{0.7\textwidth}
+    \raggedleft
+    {\Huge\bfseries Après-midi Synthèse}\\[0.4em]
+    {\Large Rencontre des Doctorants et Post-Doctorants du LIS}\\[0.4em]
+    {\large Date 03/12/2025\quad--\quad Lieu Saint-Charles FRUMAN}
+\end{minipage}
+
+\vspace{1cm}
+
+% --- Bloc "Programme" ---
+\begingroup
+\color{maincolor}
+{\LARGE\bfseries Programme de l'après-midi (14h--18h)}
+\endgroup
+
+\vspace{0.5cm}
+
+\setlength{\fboxsep}{8pt}
+\colorbox{lightbg}{%
+  \begin{minipage}{0.98\textwidth}
+    \vspace{0.3cm}
+    \small % on réduit un peu la taille dans le tableau pour que tout tienne
+    \begin{tabularx}{\textwidth}{>{\bfseries}p{2.8cm} X}
+      14h00 -- 15h00 & \textit{Brise Glace} \\
+                     & \textit{Intervenant·e : Marius} \\[0.3em]
+      15h00 -- 15h15 & \textit{Présentation du LIS} \\
+                     & \textit{Intervenant·e : Amaury} \\[0.3em]
+      15h15 -- 15h30 & \textit{Présentation du Comité JCC} \\[0.3em]
+                     & \textit{Intervenant·e : Amaury} \\[0.3em]
+      15h30 -- 15h45 & \textit{Présentation du Comité Parité} \\
+                     & \textit{Intervenant·e·s : Elie, Aliénor} \\[0.3em]
+      15h45 -- 16h30& & \textit{Wooclap des Doctorants} \\
+                     & \textit{Intervenant·e : Marius} \\[0.3em]
+      16h00 -- 16h15 & \textit{Pause café} \\[0.3em]
+      16h30 -- 18h00 & \textit{Speed-Dating} \\
+                     & \textit{Intervenant·e : Ioana} \\[0.3em]
+      18h00 -- 19h00 & \textit{Nom Nom Nom} \\[0.3em]
+      19h00 -- \dots & \textit{Soirée Jeu à la Barakajeu} \\
+    \end{tabularx}
+    \vspace{0.4cm}
+  \end{minipage}
+}
+
+\vspace{1cm}
+
+
+\vfill
+
+\newpage
+\thispagestyle{empty}
+
+% ===================== PAGE 2 : VERSION ANGLAISE =====================
+\selectlanguage{english}
+
+% --- Top banner: logo + title ---
+\begin{minipage}[t]{0.25\textwidth}
+    % Replace "logo.pdf" with your logo file, or comment the line
+    %\includegraphics[width=\textwidth]{logo.pdf}
+\end{minipage}
+\hfill
+\begin{minipage}[t]{0.7\textwidth}
+    \raggedleft
+    {\Huge\bfseries SynThèse Afternoon}\\[0.4em]
+    {\Large Meeting of LIS PhD Students and Postdocs}\\[0.4em]
+    {\large Date 03/12/2025\quad--\quad Venue Saint-Charles FRUMAN}
+\end{minipage}
+
+\vspace{1cm}
+
+% --- "Programme" block ---
+\begingroup
+\color{maincolor}
+{\LARGE\bfseries Afternoon schedule (14:00--19:00)}
+\endgroup
+
+\vspace{0.5cm}
+
+\setlength{\fboxsep}{8pt}
+\colorbox{lightbg}{%
+  \begin{minipage}{0.98\textwidth}
+    \vspace{0.3cm}
+    \small
+    \begin{tabularx}{\textwidth}{>{\bfseries}p{2.8cm} X}
+      14h00 -- 15h00 & \textit{Icebreaker} \\
+                     & \textit{Facilitator: Marius} \\[0.3em]
+      15h00 -- 15h15 & \textit{Presentation of LIS} \\
+                     & \textit{Speaker: Amaury} \\[0.3em]
+      15h15 -- 15h45 & \textit{PhD students Wooclap quiz} \\
+                     & \textit{Facilitator: Marius} \\[0.3em]
+      15h45 -- 16h00 & \textit{Presentation of the JCC Committee} \\
+                     & \textit{Speaker: Amaury} \\[0.3em]
+      16h15 -- 16h30 & \textit{Presentation of the Parity Committee} \\
+                     & \textit{Speakers: Elie, Aliénor} \\[0.3em]
+      16h00 -- 16h15 & \textit{Coffee break} \\[0.3em]
+      16h30 -- 18h00 & \textit{Speed-dating} \\
+                     & \textit{Facilitator: Ioana} \\[0.3em]
+      18h00 -- 19h00 & \textit{Nom Nom Nom (food \& drinks)} \\[0.3em]
+      19h00 -- \dots & \textit{Board games night at Barakajeu} \\
+    \end{tabularx}
+    \vspace{0.4cm}
+  \end{minipage}
+}
+
+\vfill
+
+\end{document}