nouvel algo

encore pas bon
nouvel algo + proofs
2025-09-29 16:06:43 +02:00 · 2025-06-27 07:53:09 +00:00 · 2025-05-19 16:50:06 +02:00 · 2025-05-16 14:38:08 +02:00 · 2025-05-16 14:29:23 +02:00 · 2025-05-16 14:27:20 +02:00
21 changed files with 2874 additions and 1306 deletions
--- a/.devcontainer/devcontainer.json
+++ b/.devcontainer/devcontainer.json
@@ -6,7 +6,7 @@
    "containerEnv": { //Add your build arguments here
        "DEBIAN_FRONTEND": "noninteractive"
    },
-    "runArgs": [], //Add you docker run arguments here
+    "runArgs": ["--net=host"], //Add you docker run arguments here
    "updateContentCommand": ".devcontainer/install-tools.sh", //Path to the installation script run inside the DevContainer
    // "customizations": {
    //     //Add your customizations here
--- a/.gitignore
+++ b/.gitignore
@@ -36,8 +36,7 @@ auto/

 # === Nextcloud ===
 .sync-exclude.lst
-.sync_*.db
-.sync_*.db-wal
+.sync_*.db*
 *.nextcloud.log
 *.owncloud.log
 *.owncloudsync.log
--- a/README.md
+++ b/README.md
@@ -1,7 +1,7 @@
 # Consistence Faible Byzantine Pour le Cloud

-Ce projet est hébergé ici: [https://amauryjoly.fr/gitea/amaury_joly/bwconsistency](https://amauryjoly.fr/gitea/amaury_joly/bwconsistency).  
-Un miror est disponible sur le gitlab du laboratoire du LIS: [https://gitlab.lis-lab.fr/amaury.joly/bwconsistency](https://gitlab.lis-lab.fr/amaury.joly/bwconsistency)
+Ce projet est hébergé ici: <https://amauryjoly.fr/gitea/amaury_joly/bwconsistency>.  
+Un miror est disponible sur le gitlab du laboratoire du LIS: <https://gitlab.lis-lab.fr/amaury.joly/bwconsistency>

 ## Introduction

--- a/Recherche/ALDLoverAB/algo/index.tex
+++ b/Recherche/ALDLoverAB/algo/index.tex
@@ -1,60 +1,78 @@
-We consider a set of processes communicating asynchronously over reliable point-to-point channels. Each process maintains the following shared variables:
+We consider a set of processes communicating asynchronously over reliable point-to-point channels. Each process maintains the following local or shared variables:

 \begin{itemize}
-  \item \textbf{received}: the set of messages received (but not yet delivered).
-  \item \textbf{delivered}: the set of messages that have been received, ordered, and delivered.
-  \item \textbf{prop[$r$][$j$]}: the proposal set of process $j$ at round $r$. It contains the set of messages that process $j$ claims to have received but not yet delivered at round $r$, concatenated with its newly broadcast message.
-  \item \textbf{proves}: the current content of the \texttt{DenyList} registry, accessible via the operation \texttt{READ()}. It returns a list of tuples $(j, \texttt{PROVE}(r))$, each indicating that process $j$ has issued a valid \texttt{PROVE} for round $r$.
-  \item \textbf{winner$^r$}: the set of processes that have issued a valid \texttt{PROVE} operation for round $r$.
-  \item \textbf{RB-cast}: a reliable broadcast primitive that satisfies the properties defined in Section~1.1.2.
-  \item \textbf{APPEND$(r)$}, \textbf{PROVE$(r)$}: operations that respectively insert (APPEND) and attest (PROVE) the participation of a process in round $r$ in the DenyList registry.
-  \item \textbf{READ()}: retrieves the current local view of valid operations (APPENDs and PROVEs) from the DenyList.
-  \item \textbf{ordered$(S)$}: returns a deterministic total order over a set $S$ of messages (e.g., via hash or lexicographic order).
+  \item \textbf{\textit{received}}: the set of messages that have been received via the reliable broadcast primitive but not yet ordered.
+  \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{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$.
 \end{itemize}

 \resetalgline
 \begin{algorithm}
-  
-  \vspace{1em}
-  \textbf{RB-received$(m, S, r_0, j_0)$}
-  \begin{algorithmic}[1]
-    \State \nextalgline $\textit{received} \gets \textit{received} \cup \{m\}$
-    \State \nextalgline $\textit{prop}[r_0][j_0] \gets S$
-  \end{algorithmic}
+  \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}
-  \textbf{AB-broadcast$(m, j_0)$}
-  \begin{algorithmic}[1]
-    \State \nextalgline $\textit{proves} \gets \texttt{READ}()$
-    \State \nextalgline $r_0 \gets \max\{r : \exists j,\ (j, \texttt{PROVE}(r)) \in \textit{proves}\} + 1$
-    \State \nextalgline $\texttt{RB-cast}(m, (\textit{received} \setminus \textit{delivered}) \cup \{m\}, r_0, j_0)$
-    \State \nextalgline \texttt{PROVE}$(r_0)$
-    \State \nextalgline \texttt{APPEND}$(r_0)$
-    \Repeat
-      \State \nextalgline $\textit{proves} \gets \texttt{READ}()$
-      \State \nextalgline $r_1 \gets \max\{r : \exists j,\ (j, \texttt{PROVE}(r)) \in \textit{proves}\} - 1$
-      \State \nextalgline $\textit{winner}^{r_1} \gets \{j : (j, \texttt{PROVE}(r_1)) \in \textit{proves}\}$
-      \State \nextalgline \textbf{wait} $\forall j \in \textit{winner}^{r_1},\ \textit{prop}[r_1][j] \neq \bot$
-    \Until{\nextalgline $\forall r_2,\ \exists j_2 \in \textit{winner}^{r_2},\ m \in \textit{prop}[r_2][j_2]$} \nextalgline
-  \end{algorithmic}
+    \vspace{1em}
+    % --- AB-Broadcast ---
+    \State \nextalgline \textbf{AB-Broadcast}$_j(m)$
+    \State \nextalgline \hspace{1em} $\texttt{RB-Broadcast}_j(m)$

-  \vspace{1em}
-  \textbf{AB-listen}
-  \begin{algorithmic}[1]
-    \While{true}
-      \State \nextalgline $\textit{proves} \gets \texttt{READ}()$
-      \State \nextalgline $r_1 \gets \max\{r : \exists j,\ (j, \texttt{PROVE}(r)) \in \textit{proves}\} - 1$
-      \For{$r_2 \in [r_0, \dots, r_1]$} \nextalgline
-        \State \nextalgline \texttt{APPEND}$(r_2)$
-        \State \nextalgline $\textit{proves} \gets \texttt{READ}()$
-        \State \nextalgline $\textit{winner}^{r_2} \gets \{j : (i, \texttt{PROVE}(r_2)) \in \textit{proves}\}$
-        \State \nextalgline \textbf{wait} $\forall j \in \textit{winner}^{r_2},\ \textit{prop}[r_2][j] \neq \bot$
-        \State \nextalgline $M^{r_2} \gets \bigcup_{j \in \textit{winner}^{r_2}} \textit{prop}[r_2][j]$
-        \ForAll{$m \in \texttt{ordered}(M^{r_2})$} \nextalgline
-          \State \nextalgline $\textit{delivered} \gets \textit{delivered} \cup \{m\}$
-          \State \nextalgline \texttt{AB-deliver}$(m)$
-        \EndFor
-      \EndFor
-    \EndWhile
-  \end{algorithmic}
-\end{algorithm}
+    \vspace{1em}
+    % --- RB-delivered ---
+    \State \nextalgline \textbf{RB-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$
+
+    \vspace{0.5em}
+    \State \nextalgline \hspace{2em} $\textit{winner}[r_1] \gets \texttt{READ\_ALL}()$
+    \State \nextalgline \hspace{2em} \textbf{wait } $\forall j \in \textit{winner}[r_1],\ |\textit{prop}[r_1][j] \neq \bot| \geq f+1$
+    \State \nextalgline \hspace{2em} $T \gets \bigcup_{j \in \textit{winner}[r_1]} \textit{prop}[r_1][j] \setminus \textit{delivered}$
+
+    \vspace{0.5em}
+    \State \nextalgline \hspace{2em} \textbf{for each } $m \in \texttt{ordered}(T)$
+    \State \nextalgline \hspace{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)$
+
+    \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\}$
+
+  \end{algorithmic}  
+\end{algorithm}
+
+\subsection{Round mecansism}
+
+We assume that the hash function is deterministic and without collisions. Because we're sure that the round contains at least f + 1 processes as winners, the next round ID is unpredictable by a process who would not follow the protocol and would drop messages legally sent by non-byzantine process.
+Also, it ensures that if a byzantine process try to go faster than the others, he will at least wait the faster non-byzantine process to progress.
--- a/Recherche/ALDLoverAB/main.bcf
+++ b/Recherche/ALDLoverAB/main.bcf
--- a/Recherche/ALDLoverAB/main.pdf
+++ b/Recherche/ALDLoverAB/main.pdf
--- a/Recherche/ALDLoverAB/main.tex
+++ b/Recherche/ALDLoverAB/main.tex
@@ -1,63 +1,319 @@
-\documentclass{article}
+\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[french]{babel}
-\usepackage[affil-it]{authblk}
-\usepackage{fullpage}
-
-\usepackage{amsmath}
-\usepackage{amssymb}
-
-\usepackage{biblatex}
-
-% \usepackage[linesnumbered,ruled,vlined]{algorithm2e}
+\usepackage[hidelinks]{hyperref}
+\usepackage[nameinlink,noabbrev]{cleveref}
 \usepackage{algorithm}
-\usepackage{algorithmicx}
-\usepackage[noend]{algpseudocode}
-\algrenewcommand\alglinenumber[1]{\tiny #1}
+\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{etoolbox}
+\usepackage[fr-FR]{datetime2}

-% --- Partage du compteur de lignes entre plusieurs algorithmes
-\makeatletter
-\newcounter{algoLine}
-\renewcommand{\alglinenumber}[1]{\arabic{algoLine}}
-\newcommand{\nextalgline}{\stepcounter{algoLine}}
-\newcommand{\resetalgline}{\setcounter{algoLine}{1}}
-\makeatother
+\usepackage{fancyhdr}
+\pagestyle{fancy}
+\fancyhf{}
+\fancyfoot[L]{Compilé le \DTMnow}
+\fancyfoot[C]{\thepage}
+\renewcommand{\headrulewidth}{0pt}
+\renewcommand{\footrulewidth}{0pt}

-\newtheorem{property}{Property}
+\theoremstyle{plain}
 \newtheorem{theorem}{Theorem}
-\newtheorem{proof}{Proof}
+\newtheorem{lemma}[theorem]{Lemma}
+\newtheorem{corollary}[theorem]{Corollary}
+\theoremstyle{definition}
+\newtheorem{definition}{Definition}
+\theoremstyle{remark}
+\newtheorem{remark}{Remark}

-\addbibresource{sources.bib}
+\newcommand{\RB}{\textsf{RB}\xspace}
+\newcommand{\ARB}{\textsf{ARB}\xspace}
+\newcommand{\DL}{\textsf{DL}\xspace}
+\newcommand{\APPEND}{\textsf{APPEND}}
+\newcommand{\PROVE}{\textsf{PROVE}}
+\newcommand{\READ}{\textsf{READ}}
+\newcommand{\ABbroadcast}{\textsf{AB-broadcast}}
+\newcommand{\ABdeliver}{\textsf{AB-deliver}}
+\newcommand{\RBcast}{\textsf{RB-cast}}
+\newcommand{\RBreceived}{\textsf{RB-received}}
+\newcommand{\ordered}{\textsf{ordered}}
+\newcommand{\Winners}{\mathsf{Winners}}
+\newcommand{\ABlisten}{\textsf{AB-listen}}
+
+\newcommand{\delivered}{\mathsf{delivered}}
+\newcommand{\received}{\mathsf{received}}
+\newcommand{\prop}{\mathsf{prop}}
+
+\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

-\title{???}
-\author{JOLY Amaury  \\ \textbf{Encadrants :} GODARD Emmanuel, TRAVERS Corentin}
-\affil{Aix-Marseille Université, Scille}
-\date{\today}
-
-\begin{titlepage}
-  \maketitle
-\end{titlepage}
+\begin{abstract}
+We show how to upgrade a Reliable Broadcast (\RB) primitive to Atomic Reliable Broadcast (\ARB) by leveraging a synchronous DenyList (\DL) object. In a purely asynchronous message-passing model with crashes, \ARB is impossible without additional power. The \DL supplies this power by enabling round closing and agreement on a set of "+winners" for each round. We present the algorithm, its safety arguments, and discuss liveness and complexity under the assumed synchrony of \DL.
+\end{abstract}

+\paragraph{Keywords} Atomic broadcast, total order broadcast, reliable broadcast, consensus, synchrony, shared object, linearizability.

 \section{Introduction}
+Atomic Reliable Broadcast (\ARB)---a.k.a. total order broadcast---ensures that all processes deliver the same sequence of messages. In asynchronous message-passing systems with crashes, implementing \ARB is impossible without additional assumptions, as it enables consensus. We assume a synchronous DenyList (\DL) object and demonstrate how to combine \DL with an asynchronous \RB to realize \ARB.

-\subsection{Model}
-\input{intro/index.tex}
+\section{Model}
+We consider a static set of $n$ processes with known identities, communicating by reliable point-to-point channels, in a complete graph. Messages are uniquely identifiable. 

-\subsection{Algorithms}
-\input{algo/index.tex}
+\paragraph{Synchrony.} The network is asynchronous. Processes may crash; at most $f$ crashes occur.

-\subsection{proof}
-\input{proof/index.tex}
+\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$()$. 

-\printbibliography
+\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.
+
+% ------------------------------------------------------------------------------
+\section{Primitives}
+\subsection{Reliable Broadcast (RB)}
+
+\RB provides the following properties in the model.
+\begin{itemize}[leftmargin=*]
+  \item \textbf{Integrity}: Every message received was previously sent. $\forall p_i:\ \RBreceived_i(m) \Rightarrow \exists p_j:\ \RBcast_j(m)$.
+  \item \textbf{No-duplicates}: No message is received more than once at any process.
+  \item \textbf{Validity}: If a correct process broadcasts $m$, every correct process eventually receives $m$.
+\end{itemize}
+
+\subsection{DenyList (DL)}
+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).
+\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:
+\begin{equation*}
+  \forall m_1,m_2,\ \forall p_i,p_j:\ \ \ABdeliver_i(m_1) < \ABdeliver_i(m_2) \Rightarrow \ABdeliver_j(m_1) < \ABdeliver_j(m_2),
+\end{equation*}
+plus Integrity/No-duplicates/Validity (inherited from \RB and the construction).
+
+% ------------------------------------------------------------------------------
+
+\section{Algorithm}
+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}
+
+\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$}
+  \end{algorithmic}
+\end{algorithm}
+
+\paragraph{} An \ABbroadcast$(m)$ chooses the next open round from the \DL view, proposes all pending messages together with the new $m$, disseminates this proposal via \RB, then executes $\PROVE(r)$ followed by $\APPEND(r)$ to freeze the winners of the round. The loop polls \DL until (i) some winner’s proposal includes $m$ in a \emph{closed} round and (ii) all winners' proposals for closed rounds are known locally, ensuring eventual inclusion and delivery.
+
+\renewcommand{\algletter}{B}
+\begin{algorithm}[H]
+  \caption{\ABbroadcast$(m)$ (at process $p_i$)}\label{alg:ab-bcast}
+  \begin{algorithmic}[1]
+    \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 
+  \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}
+      \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
+      \EndIf
+      \State \Return $\bot$ \Comment{No closed round ready for delivery}
+  \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.
+Once closed, a round never becomes open again.
+\end{lemma}
+
+\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.
+\end{lemma}
+
+\begin{lemma}[Well-defined winners]\label{lem:winners}
+In any execution, whenever some process computes $\Winners_r$, its current \DL-view contains $\APPEND(r)$; hence $\Winners_r$ is computed only for closed round.
+\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.
+\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.\]
+\end{proof}
+
+\begin{lemma}[No empty winners]\label{lem:nonempty}
+For any round $r$ closed, $\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$.
+\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]$.
+\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$. 
+\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}


-\end{document}
+\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.
+\end{lemma}
+
+\begin{theorem}[\ARB]
+Under the assumed \DL synchrony and \RB reliability, the algorithm implements Atomic Reliable Broadcast.
+\end{theorem}
+
+\bibliographystyle{plain}
+\begin{thebibliography}{9}
+% (left intentionally blank)
+\end{thebibliography}
+
+\end{document}
--- a/Recherche/ALDLoverAB/proof/index.tex
+++ b/Recherche/ALDLoverAB/proof/index.tex
@@ -2,24 +2,30 @@
    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}

+
 \begin{proof}
-    Let $j$ be a process such that $\text{AB-deliver}_j(m)$ occurs.
+    % Let $j$ be a process such that $\texttt{AB-deliver}_j(m)$ occurs.

-    \begin{align*}
-        &\text{AB-deliver}_j(m) & \text{(line 24)} \\
-        \Rightarrow\; &\exists r_0 : m \in \texttt{ordered}(M^{r_0}) & \text{(line 22)} \\
-        \Rightarrow\; &\exists j_0 : j_0 \in \textit{winner}^{r_0} \land m \in \textit{prop}[r_0][j_0] & \text{(line 21)} \\
-        \Rightarrow\; &\exists m_0, S_0 : \text{RB-received}_{j_0}(m_0, S_0, r_0, j_0) \land m \in S_0 & \text{(line 2)} \\
-        \Rightarrow\; &S_0 = (\textit{received}_{j_0} \setminus \textit{delivered}_{j_0}) \cup \{m_1\} & \text{(line 5)} \\
-        \Rightarrow\; &\textbf{if } m_1 = m: \exists\, \text{AB-broadcast}_{j_0}(m) \hspace{1em} \square \\
-        &\textbf{else if } m_1 \neq m: \\
-        &\quad m \in \textit{received}_{j_0} \setminus \textit{delivered}_{j_0} \Rightarrow m \in \textit{received}_{j_0} \land m \notin \textit{delivered}_{j_0} \\
-        &\quad \exists j_1, S_1, r_1 : \text{RB-received}_{j_1}(m, S_1, r_1, j_1) & \text{(line 1)} \\
-        &\quad \Rightarrow \exists\, \text{AB-broadcast}_{j_1}(m) \hspace{1em} \square & \text{(line 5)}
-    \end{align*}
+    % \begin{align*}
+    %     &\texttt{AB-deliver}_j(m) & \text{(line 18)} \\
+    %     \Rightarrow\; & m \in \texttt{ordered}(T),\ \text{with } T = \bigcup_{j' \in \textit{winner}^r} \textit{prop}[r][j'] \setminus \textit{delivered} & \text{(lines 16-17)} \\
+    %     \Rightarrow\; & \exists j_0,\ r_0 : m \in \textit{prop}[r_0][j_0] & \text{(line 16)} \\
+    %     \Rightarrow\; & \textit{prop}[r_0][j_0] = S,\ \text{with } \texttt{RB-delivered}_{j}(PROP, S, r_0, j_0) & \text{(line 22)} \\
+    %     \Rightarrow\; & S \text{ was sent in } \texttt{RB-cast}(PROP, S, r_0, j_0) & \text{(line 9)} \\
+    %     \Rightarrow\; & S = \textit{received}_{j_0} \setminus \textit{delivered}_{j_0} & \text{(line 6)} \\
+    %     \Rightarrow\; & m' \in \textit{received}_{j_0}\ \text{where } m' \text{ broadcast by } j_0 & \text{(line 4)} \\
+    %     \Rightarrow\; & \textbf{if } m = m' \\
+    %     & \quad \Rightarrow \texttt{RB-Broadcast}_{j_0}(m) \text{ occurred} & \text{(line 3)} \\
+    %     & \quad \Rightarrow \texttt{AB-Broadcast}_{j_0}(m) \text{ occurred} & \text{(line 1)} & \hspace{1em} \square \\
+    %     & \textbf{else: } m \in \textit{received}_{j_0} \setminus \textit{delivered}_{j_0} \\
+    %     & \quad \Rightarrow m \in \textit{received}_{j_0} & \text{(line 4)} \\
+    %     & \quad \Rightarrow \texttt{RB-delivered}_{j_0}(m) \text{ occurred} & \text{(line 3)} \\
+    %     & \quad \Rightarrow \exists j_1 : \texttt{RB-Broadcast}_{j_1}(m) \text{ occurred} & \text{(line 2)} \\
+    %     & \quad \Rightarrow \texttt{AB-Broadcast}_{j_1}(m) \text{ occurred} & \text{(line 1)} & \hspace{1em} \square
+    % \end{align*}
+
+    % Therefore, every delivered message $m$ must originate from some call to \texttt{AB-Broadcast}.
 \end{proof}
-    
-


 \begin{theorem}[No Duplication]
@@ -27,95 +33,76 @@
 \end{theorem}

 \begin{proof}
-    Let $j$ be a process such that both $\text{AB-deliver}_j(m_0)$ and $\text{AB-deliver}_j(m_1)$ occur, with $m_0 = m_1$.
-
-    \begin{align*}
-        &\text{AB-deliver}_j(m_0) \wedge \text{AB-deliver}_j(m_1) & \text{(line 24)} \\
-        \Rightarrow\; & m_0, m_1 \in \textit{delivered}_j & \text{(line 23)} \\
-        \Rightarrow\; &\exists r_0, r_1 : m_0 \in M^{r_0} \wedge m_1 \in M^{r_1} & \text{(line 22)} \\
-        \Rightarrow\; &\exists j_0, j_1 : m_0 \in \textit{prop}[r_0][j_0] \wedge m_1 \in \textit{prop}[r_1][j_1] \\
-        &\hspace{2.5em} \wedge\ j_0 \in \textit{winner}^{r_0},\ j_1 \in \textit{winner}^{r_1} & \text{(line 21)}
-    \end{align*}
+    % Assume by contradiction that a process $j$ delivers the same message $m$ more than once, i.e.,
+    % \[
+    % \texttt{AB-deliver}_j(m) \text{ occurs at least twice.}
+    % \]
    
-    We now distinguish two cases:
+    % \begin{align*}
+    %     &\texttt{AB-deliver}_j(m) \text{ occurs} & \text{(line 19)} \\
+    %     \Rightarrow\; & m \in \texttt{ordered}(T),\ \text{where } T = \bigcup_{j' \in \textit{winner}^r} \textit{prop}[r][j'] \setminus \textit{delivered} & \text{(lines 16-17)} \\
+    %     \Rightarrow\; & m \notin \textit{delivered} \text{ at that time} \\
+    %     \\
+    %     \text{However:} \\
+    %     & \texttt{delivered} \gets \texttt{delivered} \cup \{m\} & \text{(line 18)} \\
+    %     \Rightarrow\; & m \in \textit{delivered} \text{ permanently} \\
+    %     \Rightarrow\; & \text{In any future round, } m \notin T' \text{ since } T' = \bigcup_{j' \in \textit{winner}^r} \textit{prop}[r'][j'] \setminus \textit{delivered} \\
+    %     \Rightarrow\; & m \text{ will not be delivered again} \\
+    %     \Rightarrow\; & \text{Contradiction.}
+    % \end{align*}
    
-    \vspace{0.5em}
-    \noindent\textbf{Case 1:} $r_0 = r_1$:
-    \begin{itemize}
-        \item If $j_0 \neq j_1$: this contradicts message uniqueness, since two different processes would include the same message in round $r_0$.
-        \item If $j_0 = j_1$:
-        \begin{align*}
-            \Rightarrow & |{(j_0, \texttt{PROVE}(r_0)) \in proves}| \geq 2 & \text{(line 19)}\\
-            \Rightarrow &\texttt{PROVE}_{j_0}(r_0) \text{ occurs 2 times} & \text{(line 6)}\\
-            \Rightarrow &\texttt{AB-Broadcast}_{j_0}(m_0) \text{ were invoked two times} \\
-            \Rightarrow &(max\{r: \exists j, (j, \texttt{PROVE}(r)) \in proves\} + 1) & \text{(line 4)}\\
-            &\text{ returned the same value in two differents invokations of \texttt{AB-Broadcast}} \\
-            &\textbf{But } \texttt{PROVE}(r_0) \Rightarrow \texttt{max}\{r: \exists j, (j, \texttt{PROVE}(r)) \in proves\} + 1 > r_0 \\
-            &\text{It's impossible for a single process to submit two messages in the same round} \hspace{1em} \\
-        \end{align*}
-    \end{itemize}
-    
-    % \vspace{0.5em}
-    \noindent\textbf{Case 2:} $r_0 \ne r_1$:
-    \begin{itemize}
-        \item If $j_0 \neq j_1$: again, message uniqueness prohibits two different processes from broadcasting the same message in different rounds.
-        \item If $j_0 = j_1$: message uniqueness also prohibits the same process from broadcasting the same message in two different rounds.
-    \end{itemize}
-    
-    In all cases, we reach a contradiction. Therefore, it is impossible for a process to deliver the same message more than once. $\square$
+    % Therefore, no message can be delivered more than once by the same process. $\square$
 \end{proof}

-% \subsubsection{No Duplication}
+\begin{theorem}[Validity]
+    If a correct process invokes $\texttt{AB-Broadcast}_j(m)$, then all correct processes eventually deliver $m$.
+\end{theorem}
+    
+\begin{proof}
+    % Let $j$ be a correct process such that $\texttt{AB-Broadcast}_j(m)$ occurs (line 5).
+    
+    % \begin{align*}
+    %     &\texttt{AB-Broadcast}_j(m) & \text{(line 1)}\\
+    %     \Rightarrow\; & \texttt{RB-Broadcast}_j(m) \text{ occurs} & \text{(line 2)} \\
+    %     \Rightarrow\; & \forall j_0 : \texttt{RB-delivered}_{j_0}(m) & \text{(line 3)} \\
+    %     \Rightarrow\; & m \in \textit{received}_{j_0} & \text{(line 4)} \\
+    %     \Rightarrow\; & \textbf{if } m \in \texttt{delivered}_{j_0} \\
+    %     & \quad \Rightarrow \textit{delivered}_{j_0} \gets textit{delivered}_{j_0} \cup \{m\} & \text{(line 18)} \\
+    %     & \quad \Rightarrow \texttt{AB-delivered}_{j_0}(m) & \text{(line 19)}  & \hspace{1em} \square \\
+    %     & \textbf{else } m \notin \textit{delivered}_{j_0} : \\
+    %     & \quad \Rightarrow m \in S_{j_0}\ \text{since } S_{j_0} = \textit{receieved}_{j_0} \setminus \textit{delivered}_{j_0} & \text{(line 6)} \\
+    %     & \quad \Rightarrow \exists r : \texttt{RB-cast}_{j_0}(texttt{PROP}, S_{j_0}, r, j_0) & \text{(line 9)} \\
+    %     & \quad \quad \Rightarrow \forall j_1 : \texttt{RB-Deliver}_{j_1}(\texttt{PROP}, S_{j_0}, r, j_0)\ \text{occurs} & \text{(line 21)} \\
+    %     & \quad \quad \Rightarrow \textit{prop}[r][j_0] = S_{j_0} & \text{(line 22)} \\
+    %     & \quad \Rightarrow \exists j_2 \in j_0 : \texttt{PROVE}_{j_2}(r)\ \text{is valid} & \text{(line 10)} \\
+    %     & \quad \Rightarrow j_2 \in textit{winner}^r & \text{(line 14)} \\
+    %     & \quad \Rightarrow T_{j_0} \ni \textit{prop}[r][j_2] \setminus \textit{delivered}_{j_0} & \text{(line 16)} \\
+    %     & \quad \Rightarrow T_{j_0} \ni S_{j_2} \setminus \textit{delivered}_{j_0} \ni m & \text{(line 16)} \\
+    %     & \quad \Rightarrow \texttt{AB-deliver}_{j_0}(m) & \text{(line 19)} & \hspace{1em} \square \\
+    % \end{align*}

-% $M = (\bigcup_{i \rightarrow |P|} AB\_receieved_{i}(m)), \not\exists m_0 m_1 \in M \text{s.t. } m_1 = m_2$
-% \\
-% Proof \\
-% \begin{align*}
-%     &\text{Soit } i, m_0, m_1 \text{ tels que } m_0 = m_1 \\
-%     &\exists r_0,\ m_0 \in M^{r_0} \\
-%     &\exists r_1,\ m_1 \in M^{r_1} \\
-%     &\text{if } r_0 = r_1 \\
-%     &\quad \exists j_0, j_1,\ \text{prop tq } \text{prop}[r_0][j_0] = m_0,\ \text{prop}[r_0][j_1] = m_1 \quad j_0, j_1 \in \text{winnner}^{r_0} \\
-%     &\quad \text{if} j_0 \neq j_1 \\
-%     &\quad\quad \text{On admet qu'il est impossible pour un processus de soumettre le même msg qu'un autre} \\
-%     &\quad \text{if } j_0 = j_1 \\
-%     &\quad\quad j_0 \text{ a émis son } \text{PROVE}(r_0) \text{ valide 2 fois}\\
-%     &\quad\quad \text{Impossible si } j_0 \text{ correct} \\
-%     &\text{else} \\
-%     &\quad \exists j_0, j_1,\ \text{prop tq } \text{prop}[r_0][j_0] = m_0,\ \text{prop}[r_0][j_1] = m_1 \quad j_0, j_1 \in \text{winnner}^{r_0} \\
-%     &\quad \text{if } j_0 \neq j_1 \\    
-%     &\quad\quad \text{On admet qu'il est impossible pour un processus de soumettre le même msg qu'un autre} \\
-%     &\quad \text{if } j_0 = j_1 \\
-%     &j_0 \text{ à emis et validé 2 fois le même messages a des rounds différents.}\\
-%     &\text{On admet que deux message identiques soumis a des rounds différents ne peuvent être identiques}
-% \end{align*}
+\end{proof}

-\subsubsection{Broadcast Validity}
-$\exists j_0, m_0 \quad AB\_broadcast_{j_0}(m_0) \Rightarrow \forall j_1 \quad AB\_received_{j_1}(m_0)$ \\
+\begin{theorem}[Total Order]
+    If two correct processes deliver two messages $m_1$ and $m_2$, then they deliver them in the same order.
+\end{theorem}
+    
+\begin{proof}
+    
+    % \begin{align*}  
+    %     & \forall j_0 : \texttt{AB-Deliver}_{j_0}(m_0) \wedge \texttt{AB-Deliver}_{j_0}(m_1) & \text{(line 19)} \\
+    %     \Rightarrow\; & \exists r_0, r_1 : m_0 \in \texttt{ordered}(T^{r_0}) \wedge m_1 \in \texttt{ordered}(T^{r_1}) & \text{(line 17)} \\
+    %     \Rightarrow\; & T^{r_0} = \bigcup_{j' \in \textit{winner}^{r_0}} \textit{prop}[r_0][j'] \setminus \textit{delivered}\ \wedge \\
+    %     & T^{r_1} = \bigcup_{j' \in \textit{winner}^{r_1}} \textit{prop}[r_1][j'] \setminus \textit{delivered} & \text{(line 16)} \\
+    %     \Rightarrow\; & \textbf{if } r_0 = r_1 \\
+    %     & \quad \Rightarrow T^{r_0} = T^{r_1} \\
+    %     & \quad \Rightarrow m_0, m_1 \in \texttt{ordered}(T^{r_0})\ \text{since \texttt{ordered} is deterministic} \\
+    %     & \quad \Rightarrow \textbf{if } m_0 < m_1 : \\
+    %     & \quad \quad \Rightarrow \texttt{AB-Deliver}_{j_0}(m_0) < \texttt{AB-Deliver}_{j_0}(m_1) & & \hspace{1em} \square\\
+    %     & \textbf{else if } r_0 < r_1 \\
+    %     & \quad \Rightarrow \forall m \in T^{r_0}, \forall m' \in T^{r_1} : \texttt{AB-Deliver}(m) < \texttt{AB-Deliver}(m') & & \hspace{1em} \square\\
+    % \end{align*}
+    
+    % Therefore, for all correct processes, messages are delivered in the same total order.
+\end{proof}

-Proof:
-\begin{align*}
-    &\exists j_0, m_0 \quad AB\_broadcast_{j_0}(m_0) \\
-    &\forall j_1, \exists r_1 \quad RB\_deliver_{j_1}^{r_1}(m_0) \\
-    &\exists receieved : m_0 \in receieved_{j_1} \\
-    &\exists r_0 : RB\_deliver(PROP, r_0, m_0) & LOOP\\ 
-    &\exists prop: \text{prop}[r_0][j_0] = m_0 \\
-    &\text{if } \not\exists (j_0, PROVE(r_0)) \in \text{proves} \\
-    &\quad r_0 += 1 \\
-    &\quad \text{jump to LOOP} \\
-    &\text{else} \\
-    &\quad \exists \text{winner}, \text{winner}^{r_0} \ni j_0 \\
-    &\quad \exists M^{r_0} \ni (\text{prop}[r_0][j_0] = m_0) \\
-    &\quad \forall j_1, \quad AB\_deliver_{j_1}(m_0)
-\end{align*}
-
-\subsubsection*{AB receive width}
-\[
-\exists j_0, m_0 \quad AB\_deliver_{j_0}(m_0) \Rightarrow \forall j_1\ AB\_deliver_{j_1}
-\]
-
-Proof:
-\begin{align*}
-    &\forall j_0, m_0\ AB\_deliver_{j_0}(m_0) \Rightarrow \exists j_1 \text{ correct }, AB\_broadcast(m_0) \\
-    &\exists j_0, m_0 \quad AB\_broadcast_{j_0}(m_0) \Rightarrow \forall j_1,\ AB\_deliver_{j_1}(m_0)
-\end{align*}
--- a/Recherche/AllowListDenyList/algo/index.tex
+++ b/Recherche/AllowListDenyList/algo/index.tex
@@ -1,60 +0,0 @@
-We consider a set of processes communicating asynchronously over reliable point-to-point channels. Each process maintains the following shared variables:
-
-\begin{itemize}
-  \item \textbf{received}: the set of messages received (but not yet delivered).
-  \item \textbf{delivered}: the set of messages that have been received, ordered, and delivered.
-  \item \textbf{prop[$r$][$j$]}: the proposal set of process $j$ at round $r$. It contains the set of messages that process $j$ claims to have received but not yet delivered at round $r$, concatenated with its newly broadcast message.
-  \item \textbf{proves}: the current content of the \texttt{DenyList} registry, accessible via the operation \texttt{READ()}. It returns a list of tuples $(j, \texttt{PROVE}(r))$, each indicating that process $j$ has issued a valid \texttt{PROVE} for round $r$.
-  \item \textbf{winner$^r$}: the set of processes that have issued a valid \texttt{PROVE} operation for round $r$.
-  \item \textbf{RB-cast}: a reliable broadcast primitive that satisfies the properties defined in Section~1.1.2.
-  \item \textbf{APPEND$(r)$}, \textbf{PROVE$(r)$}: operations that respectively insert (APPEND) and attest (PROVE) the participation of a process in round $r$ in the DenyList registry.
-  \item \textbf{READ()}: retrieves the current local view of valid operations (APPENDs and PROVEs) from the DenyList.
-  \item \textbf{ordered$(S)$}: returns a deterministic total order over a set $S$ of messages (e.g., via hash or lexicographic order).
-\end{itemize}
-
-\resetalgline
-\begin{algorithm}
-  
-  \vspace{1em}
-  \textbf{RB-received$(m, S, r_0, j_0)$}
-  \begin{algorithmic}[1]
-    \State \nextalgline $\textit{received} \gets \textit{received} \cup \{m\}$
-    \State \nextalgline $\textit{prop}[r_0][j_0] \gets S$
-  \end{algorithmic}
-
-  \vspace{1em}
-  \textbf{AB-broadcast$(m, j_0)$}
-  \begin{algorithmic}[1]
-    \State \nextalgline $\textit{proves} \gets \texttt{READ}()$
-    \State \nextalgline $r_0 \gets \max\{r : \exists j,\ (j, \texttt{PROVE}(r)) \in \textit{proves}\} + 1$
-    \State \nextalgline $\texttt{RB-cast}(m, (\textit{received} \setminus \textit{delivered}) \cup \{m\}, r_0, j_0)$
-    \State \nextalgline \texttt{PROVE}$(r_0)$
-    \State \nextalgline \texttt{APPEND}$(r_0)$
-    \Repeat
-      \State \nextalgline $\textit{proves} \gets \texttt{READ}()$
-      \State \nextalgline $r_1 \gets \max\{r : \exists j,\ (j, \texttt{PROVE}(r)) \in \textit{proves}\} - 1$
-      \State \nextalgline $\textit{winner}^{r_1} \gets \{j : (j, \texttt{PROVE}(r_1)) \in \textit{proves}\}$
-      \State \nextalgline \textbf{wait} $\forall j \in \textit{winner}^{r_1},\ \textit{prop}[r_1][j] \neq \bot$
-    \Until{\nextalgline $\exists r_2,\ \exists j_2 \in \textit{winner}^{r_2},\ m \in \textit{prop}[r_2][j_2]$} \nextalgline
-  \end{algorithmic}
-
-  \vspace{1em}
-  \textbf{AB-listen}
-  \begin{algorithmic}[1]
-    \While{true}
-      \State \nextalgline $\textit{proves} \gets \texttt{READ}()$
-      \State \nextalgline $r_1 \gets \max\{r : \exists j,\ (j, \texttt{PROVE}(r)) \in \textit{proves}\} - 1$
-      \For{$r_2 \in [r_0, \dots, r_1]$} \nextalgline
-        \State \nextalgline \texttt{APPEND}$(r_2)$
-        \State \nextalgline $\textit{proves} \gets \texttt{READ}()$
-        \State \nextalgline $\textit{winner}^{r_2} \gets \{j : (i, \texttt{PROVE}(r_2)) \in \textit{proves}\}$
-        \State \nextalgline \textbf{wait} $\forall j \in \textit{winner}^{r_2},\ \textit{prop}[r_2][j] \neq \bot$
-        \State \nextalgline $M^{r_2} \gets \bigcup_{j \in \textit{winner}^{r_2}} \textit{prop}[r_2][j]$
-        \ForAll{$m \in \texttt{ordered}(M^{r_2})$} \nextalgline
-          \State \nextalgline $\textit{delivered} \gets \textit{delivered} \cup \{m\}$
-          \State \nextalgline \texttt{AB-deliver}$(m)$
-        \EndFor
-      \EndFor
-    \EndWhile
-  \end{algorithmic}
-\end{algorithm}
--- a/Recherche/AllowListDenyList/intro/index.tex
+++ b/Recherche/AllowListDenyList/intro/index.tex
@@ -1,77 +0,0 @@
-
-\subsubsection{Model Properties}
-
-The system consists of \textit{n} asynchronous processes communicating via reliable point-to-point message passing. \\
-Each process has a unique, unforgeable identifier and knows the identifiers of all other processes. \\
-Up to $f<n$ processes may crash (fail-stop). \\
-The network is reliable: if a correct process sends a message to another correct process, it is eventually delivered. \\
-Messages are uniquely identifiable: two messages sent by distinct processes or at different rounds are distinguishable \\
-2 messages sent by the same processus in two differents rounds are differents \\
-
-\begin{property}[Message Uniqueness]
-  If two messages are sent by different processes, or by the same process in different rounds, then the messages are distinct. \\
-  Formally : \\
-  \[
-  \forall p_1, p_2,\ \forall r_1, r_2,\ \forall m_1, m_2,\ 
-  \left(
-  \begin{array}{l}
-  \text{send}(p_1, r_1, m_1) \land \text{send}(p_2, r_2, m_2) \\
-  \land\ (p_1 \ne p_2 \lor r_1 \ne r_2)
-  \end{array}
-  \right)
-  \Rightarrow m_1 \ne m_2
-  \]
-\end{property}
-
-
-\subsubsection{Reliable Broadcast Properties}
-
-\begin{property}{Integrity}
-  Every message received was previously sent. \\
-  Formally : \\
-  $\forall p_i : \text{bc-recv}_i(m) \Rightarrow \exists p_j : \text{bc-send}_j(m)$
-\end{property}
-
-\begin{property}{No Duplicates}
-  No message is received more than once at any single processor. \\
-  Formally : \\
-  $\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. \\
-  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}
-
-\subsubsection{AtomicBroadcast Properties}
-
-\begin{property}{AB Totally ordered}
-  $\forall m_1, m_2, \forall p_i, p_j : \text{ab-recv}_{p_i}(m_1) < \text{ab-recv}_{p_i}(m_2) \Rightarrow \text{ab-recv}_{p_j}(m_1) < \text{ab-recv}_{p_j}(m_2)$
-\end{property}
-
-
-\subsubsection{DenyList Properties}
-
-Let $\Pi_M$ be the set of processes authorized to issue \texttt{APPEND} operations, 
-and $\Pi_V$ the set of processes authorized to issue \texttt{PROVE} operations. \\
-Let $S$ be the set of valid values that may be appended. Let $\texttt{Seq}$ be 
-the linearization of operations recorded in the DenyList.
-
-\begin{property}{APPEND Validity}
-  An operation $\texttt{APPEND}(x)$ is valid iff :
-  the issuing process $p \in \Pi_M$, and the value $x \in S$
-\end{property}
-
-\begin{property}{PROVE Validity}
-  An operation $\texttt{PROVE}(x)$ is valid iff:
-  the issuing process $p \in \Pi_V$, and there exists no $\texttt{APPEND}(x)$ that appears earlier in $\texttt{Seq}$.
-\end{property}
-
-\begin{property}{PROGRESS}
-  If an APPEND(x) is invoked by a correct process, then all correct processes will eventually be unable to PROVE(x).
-\end{property}
-
-\begin{property}{READ Validity}
-  READ() return a list of tuples who is a random permutation of all valids PROVE() associated to the identity of the emiter process. 
-\end{property}
--- a/Recherche/AllowListDenyList/main.aux
+++ b/Recherche/AllowListDenyList/main.aux
@@ -1,20 +0,0 @@
-\relax 
-\providecommand \babel@aux [2]{\global \let \babel@toc \@gobbletwo }
-\@nameuse{bbl@beforestart}
-\catcode `:\active 
-\catcode `;\active 
-\catcode `!\active 
-\catcode `?\active 
-\abx@aux@refcontext{nty/global//global/global/global}
-\providecommand \oddpage@label [2]{}
-\babel@aux{french}{}
-\@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{1}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsection}{\numberline {1.1}Model}{1}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsubsection}{\numberline {1.1.1}Model Properties}{1}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsubsection}{\numberline {1.1.2}AtomicBroadcast Properties}{1}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsubsection}{\numberline {1.1.3}DenyList Properties}{1}{}\protected@file@percent }
-\@writefile{toc}{\contentsline {subsection}{\numberline {1.2}Algo}{1}{}\protected@file@percent }
-\@writefile{loa}{\contentsline {algocf}{\numberline {1}{\ignorespaces AB\_Broadcast}}{2}{}\protected@file@percent }
-\@writefile{loa}{\contentsline {algocf}{\numberline {2}{\ignorespaces AB\_Listen}}{2}{}\protected@file@percent }
-\abx@aux@read@bbl@mdfivesum{76D65A242EC496C9B4361AF646FF12CB}
-\gdef \@abspage@last{3}
--- a/Recherche/AllowListDenyList/main.bbl
+++ b/Recherche/AllowListDenyList/main.bbl
@@ -1,20 +0,0 @@
-% $ biblatex auxiliary file $
-% $ biblatex bbl format version 3.3 $
-% Do not modify the above lines!
-%
-% This is an auxiliary file used by the 'biblatex' package.
-% This file may safely be deleted. It will be recreated by
-% biber as required.
-%
-\begingroup
-\makeatletter
-\@ifundefined{ver@biblatex.sty}
-  {\@latex@error
-     {Missing 'biblatex' package}
-     {The bibliography requires the 'biblatex' package.}
-      \aftergroup\endinput}
-  {}
-\endgroup
-
-\endinput
-
--- a/Recherche/AllowListDenyList/main.blg
+++ b/Recherche/AllowListDenyList/main.blg
@@ -1,9 +0,0 @@
-[0] Config.pm:308> INFO - This is Biber 2.20
-[1] Config.pm:311> INFO - Logfile is 'main.blg'
-[69] biber:340> INFO - === Thu Apr 24, 2025, 18:19:12
-[87] Biber.pm:420> INFO - Reading 'main.bcf'
-[141] Biber.pm:994> INFO - Found 0 citekeys in bib section 0
-[155] bbl.pm:676> INFO - Writing 'main.bbl' with encoding 'UTF-8'
-[156] bbl.pm:779> INFO - Output to main.bbl
-[157] Biber.pm:131> WARN - The file 'main.bcf' does not contain any citations!
-[158] Biber.pm:133> INFO - WARNINGS: 1
--- a/Recherche/AllowListDenyList/main.fdb_latexmk
+++ b/Recherche/AllowListDenyList/main.fdb_latexmk
@@ -1,95 +0,0 @@
-# Fdb version 4
-["biber main"] 1745518751.69811 "main.bcf" "main.bbl" "main" 1745518755.47995 0
-  "main.bcf" 1745518755.26652 108486 d8549f9e7d9f09af6a94b466d27b9f55 "pdflatex"
-  (generated)
-  "main.bbl"
-  "main.blg"
-  (rewritten before read)
-["pdflatex"] 1745518754.18166 "/workspaces/containers/recherches/AllowListDenyList/main.tex" "main.pdf" "main" 1745518755.48238 0
-  "/usr/local/texlive/2025/texmf-dist/fonts/enc/dvips/cm-super/cm-super-t1.enc" 1136849721 2971 def0b6c1f0b107b3b936def894055589 ""
-  "/usr/local/texlive/2025/texmf-dist/fonts/map/fontname/texfonts.map" 1577235249 3524 cb3e574dea2d1052e39280babc910dc8 ""
-  "/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecbx0700.tfm" 1136768653 3584 ca0c423beaacd28d53ddce5a826cd558 ""
-  "/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecbx1000.tfm" 1136768653 3584 2d666ecf6d466d8b007246bc2f94d9da ""
-  "/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecbx1200.tfm" 1136768653 3584 402da0b29eafbad07963b1224b222f18 ""
-  "/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecbx1440.tfm" 1136768653 3584 13049b61b922a28b158a38aeff75ee9b ""
-  "/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecrm1000.tfm" 1136768653 3584 adb004a0c8e7c46ee66cad73671f37b4 ""
-  "/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecrm1200.tfm" 1136768653 3584 f80ddd985bd00e29e9a6047ebd9d4781 ""
-  "/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecrm1440.tfm" 1136768653 3584 3169d30142b88a27d4ab0e3468e963a2 ""
-  "/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecrm1728.tfm" 1136768653 3584 3c76ccb63eda935a68ba65ba9da29f1a ""
-  "/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecti1000.tfm" 1136768653 3072 3bce340d4c075dffe6d4ec732b4c32fe ""
-  "/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecti1200.tfm" 1136768653 3072 8b5a64dc91775463bc95e2d818524028 ""
-  "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb" 1248133631 36299 5f9df58c2139e7edcf37c8fca4bd384d ""
-  "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi7.pfb" 1248133631 36281 c355509802a035cadc5f15869451dcee ""
-  "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb" 1248133631 35752 024fb6c41858982481f6968b5fc26508 ""
-  "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb" 1248133631 32569 5e5ddc8df908dea60932f3c484a54c0d ""
-  "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx0700.pfb" 1215737283 144215 c89c56d5c5b828c5c1657b4326c29df7 ""
-  "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx1000.pfb" 1215737283 145408 43d44302ca7d82d487f511f83e309505 ""
-  "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx1200.pfb" 1215737283 140176 d4962f948b4cc0adf4d3dde77a128c95 ""
-  "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx1440.pfb" 1215737283 135942 859a90cad7494a1e79c94baf546d7de5 ""
-  "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfrm1000.pfb" 1215737283 138258 6525c253f16cededa14c7fd0da7f67b2 ""
-  "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfrm1200.pfb" 1215737283 136101 f533469f523533d38317ab5729d00c8a ""
-  "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfrm1728.pfb" 1215737283 131438 3aa300b3e40e5c8ba7b4e5c6cebc5dd6 ""
-  "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfti1000.pfb" 1215737283 186554 e8f0fa8ca05e038f257a06405232745f ""
-  "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfti1200.pfb" 1215737283 198221 ca5aa71411090ef358a6cc78b7458365 ""
-  "/usr/local/texlive/2025/texmf-dist/tex/generic/babel-french/french.ldf" 1722030099 66864 5ea28be04c8922f57dc437cc5c1c2c31 ""
-  "/usr/local/texlive/2025/texmf-dist/tex/generic/babel/babel.sty" 1743197512 144118 8a0145ee10f36c9987d52d114dccd1b1 ""
-  "/usr/local/texlive/2025/texmf-dist/tex/generic/babel/locale/fr/babel-fr.ini" 1733001190 6315 3c384dcbb287e14a2e736eeb5010b67f ""
-  "/usr/local/texlive/2025/texmf-dist/tex/generic/babel/locale/fr/babel-french.tex" 1711748144 2142 2e5ecc022cd62b6d520b9630cf893dfe ""
-  "/usr/local/texlive/2025/texmf-dist/tex/generic/babel/txtbabel.def" 1741723514 6833 ef397c732d8c72f527b197aa1623476d ""
-  "/usr/local/texlive/2025/texmf-dist/tex/generic/iftex/iftex.sty" 1734129479 7984 7dbb9280f03c0a315425f1b4f35d43ee ""
-  "/usr/local/texlive/2025/texmf-dist/tex/generic/infwarerr/infwarerr.sty" 1575499628 8356 7bbb2c2373aa810be568c29e333da8ed ""
-  "/usr/local/texlive/2025/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty" 1701727651 17865 1a9bd36b4f98178fa551aca822290953 ""
-  "/usr/local/texlive/2025/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty" 1593379760 20089 80423eac55aa175305d35b49e04fe23b ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/algorithm2e/algorithm2e.sty" 1500498588 167160 d91cee26d3ef5727644d2110445741dd ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/base/article.cls" 1738182759 20144 63d8bacaf52e5abf4db3bc322373e1d4 ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/base/fontenc.sty" 1738182759 5275 0d62fb62162c7ab056e941ef18c5076d ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/base/ifthen.sty" 1738182759 5525 9dced5929f36b19fa837947f5175b331 ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/base/inputenc.sty" 1738182759 5048 0270515b828149155424600fd2d58ac5 ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/base/size10.clo" 1738182759 8448 5cf247d4bd0c7d5d711bbbdf111fae2e ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/bbx/numeric.bbx" 1609451401 1818 9ed166ac0a9204a8ebe450ca09db5dde ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/bbx/standard.bbx" 1609451401 25680 409c3f3d570418bc545e8065bebd0688 ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/biblatex.cfg" 1342308459 69 249fa6df04d948e51b6d5c67bea30c42 ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/biblatex.def" 1711143581 96838 228f189cb4020ea9f6d467af8aa859c2 ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/biblatex.sty" 1711143581 533961 a8d65602d822bf3d3c823e6dc4922bbc ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/blx-case-expl3.sty" 1711143581 9961 107fdb78f652fccae7bce0d23bdc19cd ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/blx-compat.def" 1643926307 13919 5426dbe90e723f089052b4e908b56ef9 ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/blx-dm.def" 1711143581 32761 18d14e3b502c120f79b2184de4e21d14 ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/cbx/numeric.cbx" 1678141846 4629 cda468e8a0b1cfa0f61872e171037a4b ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/lbx/french.lbx" 1711143581 35297 433adeecf04fccba5dc7668ba5058972 ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/carlisle/scalefnt.sty" 1137109962 1360 df2086bf924b14b72d6121fe9502fcdb ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/csquotes/csquotes.cfg" 1429144587 7068 06f8d141725d114847527a66439066b6 ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/csquotes/csquotes.def" 1712263026 22135 0975a49eeaed232aa861e9425ffb2e7c ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/csquotes/csquotes.sty" 1712263026 62767 e79d6d7a989e7da62dcf3d0a65c1faee ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/etoolbox/etoolbox.sty" 1739306980 46850 d87daedc2abdc653769a6f1067849fe0 ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/graphics/keyval.sty" 1717359999 2671 70891d50dac933918b827d326687c6e8 ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/ifoddpage/ifoddpage.sty" 1666126449 2142 eae42205b97b7a3ad0e58db5fe99e3e6 ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/kvoptions/kvoptions.sty" 1655478651 22555 6d8e155cfef6d82c3d5c742fea7c992e ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/kvsetkeys/kvsetkeys.sty" 1665067230 13815 760b0c02f691ea230f5359c4e1de23a7 ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def" 1716410060 29785 9f93ab201fe5dd053afcc6c1bcf7d266 ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/l3kernel/expl3.sty" 1738271527 6565 f51d809db6193fae7b06c1bc26ca8f75 ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/l3packages/xparse/xparse.sty" 1724879202 9783 ab4bee47700c04aadedb8da27591b0ab ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/logreq/logreq.def" 1284153563 1620 fb1c32b818f2058eca187e5c41dfae77 ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/logreq/logreq.sty" 1284153563 6187 b27afc771af565d3a9ff1ca7d16d0d46 ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/preprint/authblk.sty" 1368488610 7016 985a983ce041cc8959cd31133cba0244 ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/preprint/fullpage.sty" 1137110595 2789 05b418f78b224ec872f5b11081138605 ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/relsize/relsize.sty" 1369619135 15542 c4cc3164fe24f2f2fbb06eb71b1da4c4 ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/tools/xspace.sty" 1717359999 4545 e3f4de576c914e2000f07f69a891c071 ""
-  "/usr/local/texlive/2025/texmf-dist/tex/latex/url/url.sty" 1388531844 12796 8edb7d69a20b857904dd0ea757c14ec9 ""
-  "/usr/local/texlive/2025/texmf-dist/web2c/texmf.cnf" 1739380943 42148 61becc7c670cd061bb319c643c27fdd4 ""
-  "/usr/local/texlive/2025/texmf-var/fonts/map/pdftex/updmap/pdftex.map" 1743313660 5501089 f2ffe622267f7d8bfaba0244ab87ba6f ""
-  "/usr/local/texlive/2025/texmf-var/web2c/pdftex/pdflatex.fmt" 1743313810 3345755 ba2ca5aadbc395a8eb3e969a7d392ec2 ""
-  "/usr/local/texlive/2025/texmf.cnf" 1743313649 455 5b996dcaa0eb4ef14a83b026bc0a008c ""
-  "/workspaces/containers/recherches/AllowListDenyList/main.tex" 1745515390.16057 722 34633c768624cc239eef0942b140dea1 ""
-  "algo/index.tex" 1745516699.00079 1166 3401d17da50a7f871b536483996a0462 ""
-  "intro/index.tex" 1745518750.07112 2222 96d5bf33e15e2d99900cb9bb0955e210 ""
-  "main.aux" 1745518755.25965 1261 7295b00608a538129f1f3d8e1e94b611 "pdflatex"
-  "main.bbl" 1745518752.8063 466 76d65a242ec496c9b4361af646ff12cb "biber main"
-  "main.run.xml" 1745518755.27359 2301 7adc9b5a22e7927ebfdd8580ad5d647d "pdflatex"
-  "main.tex" 1745515390.16057 722 34633c768624cc239eef0942b140dea1 ""
-  (generated)
-  "main.aux"
-  "main.bcf"
-  "main.log"
-  "main.pdf"
-  "main.run.xml"
-  (rewritten before read)
--- a/Recherche/AllowListDenyList/main.fls
+++ b/Recherche/AllowListDenyList/main.fls
@@ -1,152 +0,0 @@
-PWD /workspaces/containers/recherches/AllowListDenyList
-INPUT /usr/local/texlive/2025/texmf.cnf
-INPUT /usr/local/texlive/2025/texmf-dist/web2c/texmf.cnf
-INPUT /usr/local/texlive/2025/texmf-var/web2c/pdftex/pdflatex.fmt
-INPUT /workspaces/containers/recherches/AllowListDenyList/main.tex
-OUTPUT main.log
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/base/article.cls
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/base/article.cls
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/base/size10.clo
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/base/size10.clo
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/base/size10.clo
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/base/fontenc.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/base/fontenc.sty
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/map/fontname/texfonts.map
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecrm1000.tfm
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/base/inputenc.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/base/inputenc.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/csquotes/csquotes.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/csquotes/csquotes.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/etoolbox/etoolbox.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/etoolbox/etoolbox.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/keyval.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/graphics/keyval.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/csquotes/csquotes.def
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/csquotes/csquotes.def
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/csquotes/csquotes.def
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/csquotes/csquotes.cfg
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/csquotes/csquotes.cfg
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/csquotes/csquotes.cfg
-INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/babel/babel.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/babel/babel.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/babel/txtbabel.def
-INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/babel-french/french.ldf
-INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/babel-french/french.ldf
-INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/babel-french/french.ldf
-INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/babel/locale/fr/babel-french.tex
-INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/babel/locale/fr/babel-french.tex
-INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/babel/locale/fr/babel-french.tex
-INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/babel/locale/fr/babel-fr.ini
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/carlisle/scalefnt.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/carlisle/scalefnt.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/preprint/authblk.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/preprint/authblk.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/preprint/fullpage.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/preprint/fullpage.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/biblatex.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/biblatex.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/infwarerr/infwarerr.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/infwarerr/infwarerr.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/iftex/iftex.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/iftex/iftex.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/kvoptions/kvoptions.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/kvoptions/kvoptions.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/kvsetkeys/kvsetkeys.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/kvsetkeys/kvsetkeys.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/logreq/logreq.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/logreq/logreq.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/logreq/logreq.def
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/logreq/logreq.def
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/logreq/logreq.def
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/base/ifthen.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/base/ifthen.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/url/url.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/url/url.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/blx-dm.def
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/blx-dm.def
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/blx-dm.def
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/blx-compat.def
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/blx-compat.def
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/blx-compat.def
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/biblatex.def
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/biblatex.def
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/biblatex.def
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/bbx/numeric.bbx
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/bbx/numeric.bbx
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/bbx/numeric.bbx
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/bbx/standard.bbx
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/bbx/standard.bbx
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/bbx/standard.bbx
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/cbx/numeric.cbx
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/cbx/numeric.cbx
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/cbx/numeric.cbx
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/biblatex.cfg
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/biblatex.cfg
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/biblatex.cfg
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/l3kernel/expl3.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/l3kernel/expl3.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/blx-case-expl3.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/blx-case-expl3.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/l3packages/xparse/xparse.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/l3packages/xparse/xparse.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/algorithm2e/algorithm2e.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/algorithm2e/algorithm2e.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/ifoddpage/ifoddpage.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/ifoddpage/ifoddpage.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/tools/xspace.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/tools/xspace.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/relsize/relsize.sty
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/relsize/relsize.sty
-INPUT ./main.aux
-INPUT ./main.aux
-INPUT main.aux
-OUTPUT main.aux
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/lbx/french.lbx
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/lbx/french.lbx
-INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/lbx/french.lbx
-OUTPUT main.bcf
-INPUT main.bbl
-INPUT ./main.bbl
-INPUT ./main.bbl
-INPUT ./main.bbl
-INPUT main.bbl
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecrm1728.tfm
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecrm1200.tfm
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecbx1200.tfm
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecti1200.tfm
-OUTPUT main.pdf
-INPUT /usr/local/texlive/2025/texmf-var/fonts/map/pdftex/updmap/pdftex.map
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/enc/dvips/cm-super/cm-super-t1.enc
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecrm1440.tfm
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecbx1440.tfm
-INPUT ./intro/index.tex
-INPUT ./intro/index.tex
-INPUT intro/index.tex
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecbx1000.tfm
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecti1000.tfm
-INPUT ./algo/index.tex
-INPUT ./algo/index.tex
-INPUT algo/index.tex
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecbx0700.tfm
-INPUT main.aux
-INPUT main.run.xml
-OUTPUT main.run.xml
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi7.pfb
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx0700.pfb
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx1000.pfb
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx1200.pfb
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx1440.pfb
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfrm1000.pfb
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfrm1200.pfb
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfrm1728.pfb
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfti1000.pfb
-INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfti1200.pfb
--- a/Recherche/AllowListDenyList/main.log
+++ b/Recherche/AllowListDenyList/main.log
@@ -1,491 +0,0 @@
-This is pdfTeX, Version 3.141592653-2.6-1.40.27 (TeX Live 2025) (preloaded format=pdflatex 2025.3.30)  24 APR 2025 18:19
-entering extended mode
- restricted \write18 enabled.
- file:line:error style messages enabled.
- %&-line parsing enabled.
-**/workspaces/containers/recherches/AllowListDenyList/main.tex
-(/workspaces/containers/recherches/AllowListDenyList/main.tex
-LaTeX2e <2024-11-01> patch level 2
-L3 programming layer <2025-01-18>
-(/usr/local/texlive/2025/texmf-dist/tex/latex/base/article.cls
-Document Class: article 2024/06/29 v1.4n Standard LaTeX document class
-(/usr/local/texlive/2025/texmf-dist/tex/latex/base/size10.clo
-File: size10.clo 2024/06/29 v1.4n Standard LaTeX file (size option)
-)
-\c@part=\count196
-\c@section=\count197
-\c@subsection=\count198
-\c@subsubsection=\count199
-\c@paragraph=\count266
-\c@subparagraph=\count267
-\c@figure=\count268
-\c@table=\count269
-\abovecaptionskip=\skip49
-\belowcaptionskip=\skip50
-\bibindent=\dimen141
-) (/usr/local/texlive/2025/texmf-dist/tex/latex/base/fontenc.sty
-Package: fontenc 2021/04/29 v2.0v Standard LaTeX package
-) (/usr/local/texlive/2025/texmf-dist/tex/latex/base/inputenc.sty
-Package: inputenc 2024/02/08 v1.3d Input encoding file
-\inpenc@prehook=\toks17
-\inpenc@posthook=\toks18
-) (/usr/local/texlive/2025/texmf-dist/tex/latex/csquotes/csquotes.sty
-Package: csquotes 2024-04-04 v5.2o context-sensitive quotations (JAW)
- (/usr/local/texlive/2025/texmf-dist/tex/latex/etoolbox/etoolbox.sty
-Package: etoolbox 2025/02/11 v2.5l e-TeX tools for LaTeX (JAW)
-\etb@tempcnta=\count270
-) (/usr/local/texlive/2025/texmf-dist/tex/latex/graphics/keyval.sty
-Package: keyval 2022/05/29 v1.15 key=value parser (DPC)
-\KV@toks@=\toks19
-)
-\csq@reset=\count271
-\csq@gtype=\count272
-\csq@glevel=\count273
-\csq@qlevel=\count274
-\csq@maxlvl=\count275
-\csq@tshold=\count276
-\csq@ltx@everypar=\toks20
- (/usr/local/texlive/2025/texmf-dist/tex/latex/csquotes/csquotes.def
-File: csquotes.def 2024-04-04 v5.2o csquotes generic definitions (JAW)
-)
-Package csquotes Info: Trying to load configuration file 'csquotes.cfg'...
-Package csquotes Info: ... configuration file loaded successfully.
- (/usr/local/texlive/2025/texmf-dist/tex/latex/csquotes/csquotes.cfg
-File: csquotes.cfg 
-)) (/usr/local/texlive/2025/texmf-dist/tex/generic/babel/babel.sty
-Package: babel 2025/03/27 v25.6 The multilingual framework for pdfLaTeX, LuaLaTeX and XeLaTeX
-\babel@savecnt=\count277
-\U@D=\dimen142
-\l@unhyphenated=\language90
- (/usr/local/texlive/2025/texmf-dist/tex/generic/babel/txtbabel.def)
-\bbl@readstream=\read2
-\bbl@dirlevel=\count278
- (/usr/local/texlive/2025/texmf-dist/tex/generic/babel-french/french.ldf
-Language: french 2024-07-25 v3.6c French support from the babel system
-Package babel Info: Hyphen rules for 'acadian' set to \l@french
-(babel)             (\language30). Reported on input line 91.
-Package babel Info: Hyphen rules for 'canadien' set to \l@french
-(babel)             (\language30). Reported on input line 92.
-\FB@stdchar=\count279
-Package babel Info: Making : an active character on input line 421.
-Package babel Info: Making ; an active character on input line 422.
-Package babel Info: Making ! an active character on input line 423.
-Package babel Info: Making ? an active character on input line 424.
-\FBguill@level=\count280
-\FBold@everypar=\toks21
-\FB@Mht=\dimen143
-\mc@charclass=\count281
-\mc@charfam=\count282
-\mc@charslot=\count283
-\std@mcc=\count284
-\dec@mcc=\count285
-\FB@parskip=\dimen144
-\listindentFB=\dimen145
-\descindentFB=\dimen146
-\labelindentFB=\dimen147
-\labelwidthFB=\dimen148
-\leftmarginFB=\dimen149
-\parindentFFN=\dimen150
-\FBfnindent=\dimen151
-)) (/usr/local/texlive/2025/texmf-dist/tex/generic/babel/locale/fr/babel-french.tex
-Package babel Info: Importing font and identification data for french
-(babel)             from babel-fr.ini. Reported on input line 11.
-) (/usr/local/texlive/2025/texmf-dist/tex/latex/carlisle/scalefnt.sty) (/usr/local/texlive/2025/texmf-dist/tex/latex/preprint/authblk.sty
-Package: authblk 2001/02/27 1.3 (PWD)
-\affilsep=\skip51
-\@affilsep=\skip52
-\c@Maxaffil=\count286
-\c@authors=\count287
-\c@affil=\count288
-) (/usr/local/texlive/2025/texmf-dist/tex/latex/preprint/fullpage.sty
-Package: fullpage 1999/02/23 1.1 (PWD)
-\FP@margin=\skip53
-) (/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/biblatex.sty
-Package: biblatex 2024/03/21 v3.20 programmable bibliographies (PK/MW)
- (/usr/local/texlive/2025/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty
-Package: pdftexcmds 2020-06-27 v0.33 Utility functions of pdfTeX for LuaTeX (HO)
- (/usr/local/texlive/2025/texmf-dist/tex/generic/infwarerr/infwarerr.sty
-Package: infwarerr 2019/12/03 v1.5 Providing info/warning/error messages (HO)
-) (/usr/local/texlive/2025/texmf-dist/tex/generic/iftex/iftex.sty
-Package: iftex 2024/12/12 v1.0g TeX engine tests
-) (/usr/local/texlive/2025/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty
-Package: ltxcmds 2023-12-04 v1.26 LaTeX kernel commands for general use (HO)
-)
-Package pdftexcmds Info: \pdf@primitive is available.
-Package pdftexcmds Info: \pdf@ifprimitive is available.
-Package pdftexcmds Info: \pdfdraftmode found.
-) (/usr/local/texlive/2025/texmf-dist/tex/latex/kvoptions/kvoptions.sty
-Package: kvoptions 2022-06-15 v3.15 Key value format for package options (HO)
- (/usr/local/texlive/2025/texmf-dist/tex/latex/kvsetkeys/kvsetkeys.sty
-Package: kvsetkeys 2022-10-05 v1.19 Key value parser (HO)
-)) (/usr/local/texlive/2025/texmf-dist/tex/latex/logreq/logreq.sty
-Package: logreq 2010/08/04 v1.0 xml request logger
-\lrq@indent=\count289
- (/usr/local/texlive/2025/texmf-dist/tex/latex/logreq/logreq.def
-File: logreq.def 2010/08/04 v1.0 logreq spec v1.0
-)) (/usr/local/texlive/2025/texmf-dist/tex/latex/base/ifthen.sty
-Package: ifthen 2024/03/16 v1.1e Standard LaTeX ifthen package (DPC)
-) (/usr/local/texlive/2025/texmf-dist/tex/latex/url/url.sty
-\Urlmuskip=\muskip17
-Package: url 2013/09/16  ver 3.4  Verb mode for urls, etc.
-)
-\c@tabx@nest=\count290
-\c@listtotal=\count291
-\c@listcount=\count292
-\c@liststart=\count293
-\c@liststop=\count294
-\c@citecount=\count295
-\c@citetotal=\count296
-\c@multicitecount=\count297
-\c@multicitetotal=\count298
-\c@instcount=\count299
-\c@maxnames=\count300
-\c@minnames=\count301
-\c@maxitems=\count302
-\c@minitems=\count303
-\c@citecounter=\count304
-\c@maxcitecounter=\count305
-\c@savedcitecounter=\count306
-\c@uniquelist=\count307
-\c@uniquename=\count308
-\c@refsection=\count309
-\c@refsegment=\count310
-\c@maxextratitle=\count311
-\c@maxextratitleyear=\count312
-\c@maxextraname=\count313
-\c@maxextradate=\count314
-\c@maxextraalpha=\count315
-\c@abbrvpenalty=\count316
-\c@highnamepenalty=\count317
-\c@lownamepenalty=\count318
-\c@maxparens=\count319
-\c@parenlevel=\count320
-\blx@tempcnta=\count321
-\blx@tempcntb=\count322
-\blx@tempcntc=\count323
-\c@blx@maxsection=\count324
-\blx@maxsegment@0=\count325
-\blx@notetype=\count326
-\blx@parenlevel@text=\count327
-\blx@parenlevel@foot=\count328
-\blx@sectionciteorder@0=\count329
-\blx@sectionciteorderinternal@0=\count330
-\blx@entrysetcounter=\count331
-\blx@biblioinstance=\count332
-\labelnumberwidth=\skip54
-\labelalphawidth=\skip55
-\biblabelsep=\skip56
-\bibitemsep=\skip57
-\bibnamesep=\skip58
-\bibinitsep=\skip59
-\bibparsep=\skip60
-\bibhang=\skip61
-\blx@bcfin=\read3
-\blx@bcfout=\write3
-\blx@langwohyphens=\language91
-\c@mincomprange=\count333
-\c@maxcomprange=\count334
-\c@mincompwidth=\count335
-Package biblatex Info: Trying to load biblatex default data model...
-Package biblatex Info: ... file 'blx-dm.def' found.
- (/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/blx-dm.def
-File: blx-dm.def 2024/03/21 v3.20 biblatex datamodel (PK/MW)
-)
-Package biblatex Info: Trying to load biblatex custom data model...
-Package biblatex Info: ... file 'biblatex-dm.cfg' not found.
-\c@afterword=\count336
-\c@savedafterword=\count337
-\c@annotator=\count338
-\c@savedannotator=\count339
-\c@author=\count340
-\c@savedauthor=\count341
-\c@bookauthor=\count342
-\c@savedbookauthor=\count343
-\c@commentator=\count344
-\c@savedcommentator=\count345
-\c@editor=\count346
-\c@savededitor=\count347
-\c@editora=\count348
-\c@savededitora=\count349
-\c@editorb=\count350
-\c@savededitorb=\count351
-\c@editorc=\count352
-\c@savededitorc=\count353
-\c@foreword=\count354
-\c@savedforeword=\count355
-\c@holder=\count356
-\c@savedholder=\count357
-\c@introduction=\count358
-\c@savedintroduction=\count359
-\c@namea=\count360
-\c@savednamea=\count361
-\c@nameb=\count362
-\c@savednameb=\count363
-\c@namec=\count364
-\c@savednamec=\count365
-\c@translator=\count366
-\c@savedtranslator=\count367
-\c@shortauthor=\count368
-\c@savedshortauthor=\count369
-\c@shorteditor=\count370
-\c@savedshorteditor=\count371
-\c@labelname=\count372
-\c@savedlabelname=\count373
-\c@institution=\count374
-\c@savedinstitution=\count375
-\c@lista=\count376
-\c@savedlista=\count377
-\c@listb=\count378
-\c@savedlistb=\count379
-\c@listc=\count380
-\c@savedlistc=\count381
-\c@listd=\count382
-\c@savedlistd=\count383
-\c@liste=\count384
-\c@savedliste=\count385
-\c@listf=\count386
-\c@savedlistf=\count387
-\c@location=\count388
-\c@savedlocation=\count389
-\c@organization=\count390
-\c@savedorganization=\count391
-\c@origlocation=\count392
-\c@savedoriglocation=\count393
-\c@origpublisher=\count394
-\c@savedorigpublisher=\count395
-\c@publisher=\count396
-\c@savedpublisher=\count397
-\c@language=\count398
-\c@savedlanguage=\count399
-\c@origlanguage=\count400
-\c@savedoriglanguage=\count401
-\c@pageref=\count402
-\c@savedpageref=\count403
-\shorthandwidth=\skip62
-\shortjournalwidth=\skip63
-\shortserieswidth=\skip64
-\shorttitlewidth=\skip65
-\shortauthorwidth=\skip66
-\shorteditorwidth=\skip67
-\locallabelnumberwidth=\skip68
-\locallabelalphawidth=\skip69
-\localshorthandwidth=\skip70
-\localshortjournalwidth=\skip71
-\localshortserieswidth=\skip72
-\localshorttitlewidth=\skip73
-\localshortauthorwidth=\skip74
-\localshorteditorwidth=\skip75
-Package biblatex Info: Trying to load compatibility code...
-Package biblatex Info: ... file 'blx-compat.def' found.
- (/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/blx-compat.def
-File: blx-compat.def 2024/03/21 v3.20 biblatex compatibility (PK/MW)
-)
-Package biblatex Info: Trying to load generic definitions...
-Package biblatex Info: ... file 'biblatex.def' found.
- (/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/biblatex.def
-File: biblatex.def 2024/03/21 v3.20 biblatex compatibility (PK/MW)
-\c@textcitecount=\count404
-\c@textcitetotal=\count405
-\c@textcitemaxnames=\count406
-\c@biburlbigbreakpenalty=\count407
-\c@biburlbreakpenalty=\count408
-\c@biburlnumpenalty=\count409
-\c@biburlucpenalty=\count410
-\c@biburllcpenalty=\count411
-\biburlbigskip=\muskip18
-\biburlnumskip=\muskip19
-\biburlucskip=\muskip20
-\biburllcskip=\muskip21
-\c@smartand=\count412
-)
-Package biblatex Info: Trying to load bibliography style 'numeric'...
-Package biblatex Info: ... file 'numeric.bbx' found.
- (/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/bbx/numeric.bbx
-File: numeric.bbx 2024/03/21 v3.20 biblatex bibliography style (PK/MW)
-Package biblatex Info: Trying to load bibliography style 'standard'...
-Package biblatex Info: ... file 'standard.bbx' found.
- (/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/bbx/standard.bbx
-File: standard.bbx 2024/03/21 v3.20 biblatex bibliography style (PK/MW)
-\c@bbx:relatedcount=\count413
-\c@bbx:relatedtotal=\count414
-))
-Package biblatex Info: Trying to load citation style 'numeric'...
-Package biblatex Info: ... file 'numeric.cbx' found.
- (/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/cbx/numeric.cbx
-File: numeric.cbx 2024/03/21 v3.20 biblatex citation style (PK/MW)
-Package biblatex Info: Redefining '\cite'.
-Package biblatex Info: Redefining '\parencite'.
-Package biblatex Info: Redefining '\footcite'.
-Package biblatex Info: Redefining '\footcitetext'.
-Package biblatex Info: Redefining '\smartcite'.
-Package biblatex Info: Redefining '\supercite'.
-Package biblatex Info: Redefining '\textcite'.
-Package biblatex Info: Redefining '\textcites'.
-Package biblatex Info: Redefining '\cites'.
-Package biblatex Info: Redefining '\parencites'.
-Package biblatex Info: Redefining '\smartcites'.
-)
-Package biblatex Info: Trying to load configuration file...
-Package biblatex Info: ... file 'biblatex.cfg' found.
- (/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/biblatex.cfg
-File: biblatex.cfg 
-)
-Package biblatex Info: Input encoding 'utf8' detected.
-Package biblatex Info: Document encoding is UTF8 ....
- (/usr/local/texlive/2025/texmf-dist/tex/latex/l3kernel/expl3.sty
-Package: expl3 2025-01-18 L3 programming layer (loader) 
- (/usr/local/texlive/2025/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def
-File: l3backend-pdftex.def 2024-05-08 L3 backend support: PDF output (pdfTeX)
-\l__color_backend_stack_int=\count415
-\l__pdf_internal_box=\box52
-))
-Package biblatex Info: ... and expl3
-(biblatex)             2025-01-18 L3 programming layer (loader) 
-(biblatex)             is new enough (at least 2020/04/06),
-(biblatex)             setting 'casechanger=expl3'.
- (/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/blx-case-expl3.sty (/usr/local/texlive/2025/texmf-dist/tex/latex/l3packages/xparse/xparse.sty
-Package: xparse 2024-08-16 L3 Experimental document command parser
-)
-Package: blx-case-expl3 2024/03/21 v3.20 expl3 case changing code for biblatex
-)) (/usr/local/texlive/2025/texmf-dist/tex/latex/algorithm2e/algorithm2e.sty
-Package: algorithm2e 2017/07/18 v5.2 algorithms environments
-\c@AlgoLine=\count416
-\algocf@hangindent=\skip76
- (/usr/local/texlive/2025/texmf-dist/tex/latex/ifoddpage/ifoddpage.sty
-Package: ifoddpage 2022/10/18 v1.2 Conditionals for odd/even page detection
-\c@checkoddpage=\count417
-) (/usr/local/texlive/2025/texmf-dist/tex/latex/tools/xspace.sty
-Package: xspace 2014/10/28 v1.13 Space after command names (DPC,MH)
-) (/usr/local/texlive/2025/texmf-dist/tex/latex/relsize/relsize.sty
-Package: relsize 2013/03/29 ver 4.1
-)
-\skiptotal=\skip77
-\skiplinenumber=\skip78
-\skiprule=\skip79
-\skiphlne=\skip80
-\skiptext=\skip81
-\skiplength=\skip82
-\algomargin=\skip83
-\skipalgocfslide=\skip84
-\algowidth=\dimen152
-\inoutsize=\dimen153
-\inoutindent=\dimen154
-\interspacetitleruled=\dimen155
-\interspacealgoruled=\dimen156
-\interspacetitleboxruled=\dimen157
-\algocf@ruledwidth=\skip85
-\algocf@inoutbox=\box53
-\algocf@inputbox=\box54
-\AlCapSkip=\skip86
-\AlCapHSkip=\skip87
-\algoskipindent=\skip88
-\algocf@nlbox=\box55
-\algocf@hangingbox=\box56
-\algocf@untilbox=\box57
-\algocf@skipuntil=\skip89
-\algocf@capbox=\box58
-\algocf@lcaptionbox=\skip90
-\algoheightruledefault=\skip91
-\algoheightrule=\skip92
-\algotitleheightruledefault=\skip93
-\algotitleheightrule=\skip94
-\c@algocfline=\count418
-\c@algocfproc=\count419
-\c@algocf=\count420
-\algocf@algoframe=\box59
-\algocf@algobox=\box60
-)
-\c@theorem=\count421
-Package csquotes Info: Checking for multilingual support...
-Package csquotes Info: ... found 'babel' package.
-Package csquotes Info: Adjusting default style.
-Package csquotes Info: Redefining alias 'default' -> 'french'.
- (./main.aux
-Package babel Info: 'french' activates 'french' shorthands.
-(babel)             Reported  on input line 10.
-)
-\openout1 = `main.aux'.
-
-LaTeX Font Info:    Checking defaults for OML/cmm/m/it on input line 18.
-LaTeX Font Info:    ... okay on input line 18.
-LaTeX Font Info:    Checking defaults for OMS/cmsy/m/n on input line 18.
-LaTeX Font Info:    ... okay on input line 18.
-LaTeX Font Info:    Checking defaults for OT1/cmr/m/n on input line 18.
-LaTeX Font Info:    ... okay on input line 18.
-LaTeX Font Info:    Checking defaults for T1/cmr/m/n on input line 18.
-LaTeX Font Info:    ... okay on input line 18.
-LaTeX Font Info:    Checking defaults for TS1/cmr/m/n on input line 18.
-LaTeX Font Info:    ... okay on input line 18.
-LaTeX Font Info:    Checking defaults for OMX/cmex/m/n on input line 18.
-LaTeX Font Info:    ... okay on input line 18.
-LaTeX Font Info:    Checking defaults for U/cmr/m/n on input line 18.
-LaTeX Font Info:    ... okay on input line 18.
-LaTeX Info: Redefining \degres on input line 18.
-LaTeX Info: Redefining \up on input line 18.
-Package biblatex Info: Trying to load language 'french'...
-Package biblatex Info: ... file 'french.lbx' found.
- (/usr/local/texlive/2025/texmf-dist/tex/latex/biblatex/lbx/french.lbx
-File: french.lbx 2024/03/21 v3.20 biblatex localization (PK/MW)
-)
-Package biblatex Info: Input encoding 'utf8' detected.
-Package biblatex Info: Automatic encoding selection.
-(biblatex)             Assuming data encoding 'utf8'.
-\openout3 = `main.bcf'.
-
-Package biblatex Info: Trying to load bibliographic data...
-Package biblatex Info: ... file 'main.bbl' found.
- (./main.bbl)
-Package biblatex Info: Reference section=0 on input line 18.
-Package biblatex Info: Reference segment=0 on input line 18.
-
-
-[1
-
-{/usr/local/texlive/2025/texmf-var/fonts/map/pdftex/updmap/pdftex.map}{/usr/local/texlive/2025/texmf-dist/fonts/enc/dvips/cm-super/cm-super-t1.enc}] (./intro/index.tex
-LaTeX Font Info:    External font `cmex10' loaded for size
-(Font)              <7> on input line 5.
-LaTeX Font Info:    External font `cmex10' loaded for size
-(Font)              <5> on input line 5.
-
-Underfull \hbox (badness 10000) in paragraph at lines 12--14
-
- []
-
-) (./algo/index.tex
-
-[1]
-Underfull \hbox (badness 10000) in paragraph at lines 21--26
-
- []
-
-)
-
-LaTeX Warning: Empty bibliography on input line 38.
-
-
-
-[2] (./main.aux)
- ***********
-LaTeX2e <2024-11-01> patch level 2
-L3 programming layer <2025-01-18>
- ***********
-Package logreq Info: Writing requests to 'main.run.xml'.
-\openout1 = `main.run.xml'.
-
- ) 
-Here is how much of TeX's memory you used:
- 12402 strings out of 473190
- 235027 string characters out of 5715806
- 1085239 words of memory out of 5000000
- 35573 multiletter control sequences out of 15000+600000
- 566378 words of font info for 46 fonts, out of 8000000 for 9000
- 1141 hyphenation exceptions out of 8191
- 66i,18n,81p,745b,1731s stack positions out of 10000i,1000n,20000p,200000b,200000s
-</usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi7.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx0700.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx1000.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx1200.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbx1440.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfrm1000.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfrm1200.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfrm1728.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfti1000.pfb></usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfti1200.pfb>
-Output written on main.pdf (3 pages, 194797 bytes).
-PDF statistics:
- 80 PDF objects out of 1000 (max. 8388607)
- 48 compressed objects within 1 object stream
- 0 named destinations out of 1000 (max. 500000)
- 1 words of extra memory for PDF output out of 10000 (max. 10000000)
-
--- a/Recherche/AllowListDenyList/main.pdf
+++ b/Recherche/AllowListDenyList/main.pdf
--- a/Recherche/AllowListDenyList/main.synctex.gz
+++ b/Recherche/AllowListDenyList/main.synctex.gz
--- a/Recherche/AllowListDenyList/main.tex
+++ b/Recherche/AllowListDenyList/main.tex
@@ -1,63 +0,0 @@
-\documentclass{article}
-
-\usepackage[T1]{fontenc}
-\usepackage[utf8]{inputenc}
-\usepackage{csquotes}
-\usepackage[french]{babel}
-\usepackage[affil-it]{authblk}
-\usepackage{fullpage}
-
-\usepackage{amsmath}
-\usepackage{amssymb}
-
-\usepackage{biblatex}
-
-% \usepackage[linesnumbered,ruled,vlined]{algorithm2e}
-\usepackage{algorithm}
-\usepackage{algorithmicx}
-\usepackage[noend]{algpseudocode}
-\algrenewcommand\alglinenumber[1]{\tiny #1}
-
-\usepackage{etoolbox}
-
-% --- Partage du compteur de lignes entre plusieurs algorithmes
-\makeatletter
-\newcounter{algoLine}
-\renewcommand{\alglinenumber}[1]{\arabic{algoLine}}
-\newcommand{\nextalgline}{\stepcounter{algoLine}}
-\newcommand{\resetalgline}{\setcounter{algoLine}{1}}
-\makeatother
-
-\newtheorem{property}{Property}
-\newtheorem{theorem}{Theorem}
-\newtheorem{proof}{Proof}
-
-\addbibresource{sources.bib}
-
-\begin{document}
-
-\title{???}
-\author{JOLY Amaury  \\ \textbf{Encadrants :} GODARD Emmanuel, TRAVERS Corentin}
-\affil{Aix-Marseille Université, Scille}
-\date{\today}
-
-\begin{titlepage}
-  \maketitle
-\end{titlepage}
-
-
-\section{Introduction}
-
-\subsection{Model}
-\input{intro/index.tex}
-
-\subsection{Algorithms}
-\input{algo/index.tex}
-
-\subsection{proof}
-\input{proof/index.tex}
-
-\printbibliography
-
-
-\end{document}
--- a/Recherche/AllowListDenyList/proof/index.tex
+++ b/Recherche/AllowListDenyList/proof/index.tex
@@ -1,121 +0,0 @@
-\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}
-
-\begin{proof}
-    Let $j$ be a process such that $\text{AB-deliver}_j(m)$ occurs.
-
-    \begin{align*}
-        &\text{AB-deliver}_j(m) & \text{(line 24)} \\
-        \Rightarrow\; &\exists r_0 : m \in \texttt{ordered}(M^{r_0}) & \text{(line 22)} \\
-        \Rightarrow\; &\exists j_0 : j_0 \in \textit{winner}^{r_0} \land m \in \textit{prop}[r_0][j_0] & \text{(line 21)} \\
-        \Rightarrow\; &\exists m_0, S_0 : \text{RB-received}_{j_0}(m_0, S_0, r_0, j_0) \land m \in S_0 & \text{(line 2)} \\
-        \Rightarrow\; &S_0 = (\textit{received}_{j_0} \setminus \textit{delivered}_{j_0}) \cup \{m_1\} & \text{(line 5)} \\
-        \Rightarrow\; &\textbf{if } m_1 = m: \exists\, \text{AB-broadcast}_{j_0}(m) \hspace{1em} \square \\
-        &\textbf{else if } m_1 \neq m: \\
-        &\quad m \in \textit{received}_{j_0} \setminus \textit{delivered}_{j_0} \Rightarrow m \in \textit{received}_{j_0} \land m \notin \textit{delivered}_{j_0} \\
-        &\quad \exists j_1, S_1, r_1 : \text{RB-received}_{j_1}(m, S_1, r_1, j_1) & \text{(line 1)} \\
-        &\quad \Rightarrow \exists\, \text{AB-broadcast}_{j_1}(m) \hspace{1em} \square & \text{(line 5)}
-    \end{align*}
-\end{proof}
-    
-
-
-
-\begin{theorem}[No Duplication]
-    No message is delivered more than once by any process.
-\end{theorem}
-
-\begin{proof}
-    Let $j$ be a process such that both $\text{AB-deliver}_j(m_0)$ and $\text{AB-deliver}_j(m_1)$ occur, with $m_0 = m_1$.
-
-    \begin{align*}
-        &\text{AB-deliver}_j(m_0) \wedge \text{AB-deliver}_j(m_1) & \text{(line 24)} \\
-        \Rightarrow\; & m_0, m_1 \in \textit{delivered}_j & \text{(line 23)} \\
-        \Rightarrow\; &\exists r_0, r_1 : m_0 \in M^{r_0} \wedge m_1 \in M^{r_1} & \text{(line 22)} \\
-        \Rightarrow\; &\exists j_0, j_1 : m_0 \in \textit{prop}[r_0][j_0] \wedge m_1 \in \textit{prop}[r_1][j_1] \\
-        &\hspace{2.5em} \wedge\ j_0 \in \textit{winner}^{r_0},\ j_1 \in \textit{winner}^{r_1} & \text{(line 21)}
-    \end{align*}
-    
-    We now distinguish two cases:
-    
-    \vspace{0.5em}
-    \noindent\textbf{Case 1:} $r_0 = r_1$:
-    \begin{itemize}
-        \item If $j_0 \neq j_1$: this contradicts message uniqueness, since two different processes would include the same message in round $r_0$.
-        \item If $j_0 = j_1$:
-        \begin{align*}
-            \Rightarrow & |{(j_0, \texttt{PROVE}(r_0)) \in proves}| \geq 2 & \text{(line 19)}\\
-            \Rightarrow &\texttt{PROVE}_{j_0}(r_0) \text{ occurs 2 times} & \text{(line 6)}\\
-            \Rightarrow &\texttt{AB-Broadcast}_{j_0}(m_0) \text{ were invoked two times} \\
-            \Rightarrow &(max\{r: \exists j, (j, \texttt{PROVE}(r)) \in proves\} + 1) & \text{(line 4)}\\
-            &\text{ returned the same value in two differents invokations of \texttt{AB-Broadcast}} \\
-            &\textbf{But } \texttt{PROVE}(r_0) \Rightarrow \texttt{max}\{r: \exists j, (j, \texttt{PROVE}(r)) \in proves\} + 1 > r_0 \\
-            &\text{It's impossible for a single process to submit two messages in the same round} \hspace{1em} \\
-        \end{align*}
-    \end{itemize}
-    
-    % \vspace{0.5em}
-    \noindent\textbf{Case 2:} $r_0 \ne r_1$:
-    \begin{itemize}
-        \item If $j_0 \neq j_1$: again, message uniqueness prohibits two different processes from broadcasting the same message in different rounds.
-        \item If $j_0 = j_1$: message uniqueness also prohibits the same process from broadcasting the same message in two different rounds.
-    \end{itemize}
-    
-    In all cases, we reach a contradiction. Therefore, it is impossible for a process to deliver the same message more than once. $\square$
-\end{proof}
-
-% \subsubsection{No Duplication}
-
-% $M = (\bigcup_{i \rightarrow |P|} AB\_receieved_{i}(m)), \not\exists m_0 m_1 \in M \text{s.t. } m_1 = m_2$
-% \\
-% Proof \\
-% \begin{align*}
-%     &\text{Soit } i, m_0, m_1 \text{ tels que } m_0 = m_1 \\
-%     &\exists r_0,\ m_0 \in M^{r_0} \\
-%     &\exists r_1,\ m_1 \in M^{r_1} \\
-%     &\text{if } r_0 = r_1 \\
-%     &\quad \exists j_0, j_1,\ \text{prop tq } \text{prop}[r_0][j_0] = m_0,\ \text{prop}[r_0][j_1] = m_1 \quad j_0, j_1 \in \text{winnner}^{r_0} \\
-%     &\quad \text{if} j_0 \neq j_1 \\
-%     &\quad\quad \text{On admet qu'il est impossible pour un processus de soumettre le même msg qu'un autre} \\
-%     &\quad \text{if } j_0 = j_1 \\
-%     &\quad\quad j_0 \text{ a émis son } \text{PROVE}(r_0) \text{ valide 2 fois}\\
-%     &\quad\quad \text{Impossible si } j_0 \text{ correct} \\
-%     &\text{else} \\
-%     &\quad \exists j_0, j_1,\ \text{prop tq } \text{prop}[r_0][j_0] = m_0,\ \text{prop}[r_0][j_1] = m_1 \quad j_0, j_1 \in \text{winnner}^{r_0} \\
-%     &\quad \text{if } j_0 \neq j_1 \\    
-%     &\quad\quad \text{On admet qu'il est impossible pour un processus de soumettre le même msg qu'un autre} \\
-%     &\quad \text{if } j_0 = j_1 \\
-%     &j_0 \text{ à emis et validé 2 fois le même messages a des rounds différents.}\\
-%     &\text{On admet que deux message identiques soumis a des rounds différents ne peuvent être identiques}
-% \end{align*}
-
-\subsubsection{Broadcast Validity}
-$\exists j_0, m_0 \quad AB\_broadcast_{j_0}(m_0) \Rightarrow \forall j_1 \quad AB\_received_{j_1}(m_0)$ \\
-
-Proof:
-\begin{align*}
-    &\exists j_0, m_0 \quad AB\_broadcast_{j_0}(m_0) \\
-    &\forall j_1, \exists r_1 \quad RB\_deliver_{j_1}^{r_1}(m_0) \\
-    &\exists receieved : m_0 \in receieved_{j_1} \\
-    &\exists r_0 : RB\_deliver(PROP, r_0, m_0) & LOOP\\ 
-    &\exists prop: \text{prop}[r_0][j_0] = m_0 \\
-    &\text{if } \not\exists (j_0, PROVE(r_0)) \in \text{proves} \\
-    &\quad r_0 += 1 \\
-    &\quad \text{jump to LOOP} \\
-    &\text{else} \\
-    &\quad \exists \text{winner}, \text{winner}^{r_0} \ni j_0 \\
-    &\quad \exists M^{r_0} \ni (\text{prop}[r_0][j_0] = m_0) \\
-    &\quad \forall j_1, \quad AB\_deliver_{j_1}(m_0)
-\end{align*}
-
-\subsubsection*{AB receive width}
-\[
-\exists j_0, m_0 \quad AB\_deliver_{j_0}(m_0) \Rightarrow \forall j_1\ AB\_deliver_{j_1}
-\]
-
-Proof:
-\begin{align*}
-    &\forall j_0, m_0\ AB\_deliver_{j_0}(m_0) \Rightarrow \exists j_1 \text{ correct }, AB\_broadcast(m_0) \\
-    &\exists j_0, m_0 \quad AB\_broadcast_{j_0}(m_0) \Rightarrow \forall j_1,\ AB\_deliver_{j_1}(m_0)
-\end{align*}
--- a/Recherche/AllowListDenyList/sources.bib
+++ b/Recherche/AllowListDenyList/sources.bib
Author	SHA1	Message	Date
Amaury JOLY	3ea8de6388	nouvel algo	2025-09-29 16:06:43 +02:00
Amaury JOLY	35a9d91779	encore pas bon	2025-06-27 07:53:09 +00:00
Amaury JOLY	b5719a7d6b	nouvel algo + proofs	2025-05-19 16:50:06 +02:00
Amaury JOLY	d1caa2e54a	sync nextcloud	2025-05-16 14:38:08 +02:00
Amaury JOLY	0da5a47d47	sync nextcloud	2025-05-16 14:29:23 +02:00
Amaury JOLY	c3694aff50	sync nextcloud	2025-05-16 14:27:20 +02:00
Amaury JOLY	c5d71235d5	sync nextcloud	2025-05-16 14:26:37 +02:00
Amaury JOLY	82f0f8c92c	sync nextcloud	2025-05-16 14:08:06 +02:00
Amaury JOLY	999511988d	intro et algo propre. Proof en cours	2025-05-15 11:48:32 +00:00
Amaury JOLY	ee359083fd	bad message	2025-05-05 08:13:55 +00:00
Amaury JOLY	23b4126f7e	ADoverAB v2	2025-05-02 07:22:19 +00:00
Amaury JOLY	aefa847e9b	ALDoverABv1	2025-04-30 07:07:35 +00:00
amaury	87ef596364	hard push	2024-12-17 14:58:27 +01:00
amaury	ab70a09cbf	hard push	2024-12-17 14:57:43 +01:00
Amaury	e51d7de452	oups	2024-04-03 09:13:23 +02:00
Amaury	25bcd0cc27	update biblio	2023-10-31 15:59:46 +01:00
Amaury	8199d8d9e2	rapport de stage	2023-09-11 09:21:49 +02:00
Amaury	4d216f8338	update biblio	2023-07-12 14:24:04 +02:00
Amaury	9c0f14255d	configuration vscode	2023-07-11 14:25:09 +02:00
Amaury	b1ae7f3821	quelques notes de lectures (pas très beau, histoire de l'avoir sur le git)	2023-07-11 14:24:05 +02:00
Amaury	74cd55be4b	biblio au 11/07/23 + notes tri	2023-07-11 14:22:47 +02:00
Amaury	9130472a12	edit presentation dalgo + gitignore latex	2023-07-11 14:21:30 +02:00
Amaury	b00fc6acbe	reorganisation	2023-07-03 14:32:03 +02:00
Amaury	f1b1dc40ca	retrait fichier poubelle	2023-06-29 13:35:39 +02:00
Amaury	e080a1d53a	ajout présentation pour Scille séminaire été 2023	2023-06-29 13:34:57 +02:00
amaury	5b2ad4ab99	spell check + des ajouts en vrac	2023-05-12 14:56:24 +02:00
amaury	a44d8f8ebb	refactor	2023-05-07 16:08:25 +02:00
amaury	0e3463f97d	rajout de notes + debut beamer	2023-05-07 16:02:45 +02:00
amaury	5fd2cd1273	rajout de mes notes	2023-04-24 10:12:40 +02:00
Amaury JOLY	84867740de	lecture_vdLLP (#10 ) Co-authored-by: amaury <ajoly@aviatrix.com> Reviewed-on: #10	2023-04-20 13:45:09 +02:00
amaury	b0695ae27e	edit README	2023-04-13 15:18:19 +02:00
amaury	8763cc6413	edit README	2023-04-13 15:10:37 +02:00
amaury	18373a46df	done	2023-04-12 14:13:39 +02:00
amaury	6300aba265	Rey18_chapitre1	2023-04-11 14:27:28 +02:00
amaury	6c15a5bf15	first commit	2023-04-11 10:30:29 +02:00