diff --git a/recherches/ALDLoverAB/algo/index.tex b/recherches/ALDLoverAB/algo/index.tex index dc6d332..96385b7 100644 --- a/recherches/ALDLoverAB/algo/index.tex +++ b/recherches/ALDLoverAB/algo/index.tex @@ -1,73 +1,60 @@ -We define $k$ as the id of the round \\ -the $getMax(proves)$ return $MAX({(\_, r) : \exists (\_, PROVE(r)) \in proves})$ \\ -$buffer$ a FIFO list with $buffer[front]$ returning the first element +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} -\begin{algorithm}[H] - \DontPrintSemicolon - \SetAlgoLined +\resetalgline +\begin{algorithm} - $rcved = rcved \bigcup \{m\}$ \; - \textbf{upon} RB\_deliver(PROP, r, S) \textbf{from} j \; - prop[r][j] = S + \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{\textbf{Upon} RB\_deliver(m)} -\end{algorithm} + \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} -\begin{algorithm}[H] -\DontPrintSemicolon -\SetAlgoLined -\KwIn{le message $m$} - -\KwData{rcved = $\emptyset$ \; -delivered = $\emptyset$ \; -r = 0 \;} - -\BlankLine - -RB\_cast(m) \; -$rcved = rcvd \bigcup \{m\}$ \; - -\While{true}{ - $r = r+1$ \; - $RB\_cast(PROP, r, S)$ \; - PROVE(r) \; - APPEND(r) \; - proves = READ() \; - $winner^r = \{j : (j, PROVE(r)) \in proves\}$ \; - \textbf{wait until} $(\forall j \in winner^k: prop[r][j])$ \; - \If{$\exists j \in winner^k : m \in prop[r][j]$}{ - break \; - } -} - -\caption{AB\_Broadcast} -\end{algorithm} - -\begin{algorithm}[H] - \DontPrintSemicolon - \SetAlgoLined - - r\_prev = 0 \; - \While{true}{ - proves = READ() \; - $r\_max = MAX(\{r : \exists i, (i, PROVE(r)) \in proves\})$ \; - \For{$r = r\_prev + 1 \textbf{to} r\_max$}{ - APPEND(r) \; - proves = READ() \; - $winner^k = \{j : (j, PROVE(r)) \in proves \}$ \; - $\textbf{wait until} (\forall j \in winner^k : prop[r][j] \neq \emptyset)$ \; - $M^r = (\bigcup_{j \in winner^k} prop[r][j]) \setminus delivered$ \; - - \tcc*{we assume $M^r$ as an ordered list s.a. $\forall m_1, m_2, if m_1 < m_2$, $m_1$ appears before $m_2$ in $M^r$} - - \BlankLine - - \ForEach{$m \in M^r$}{ - $delivered = delivered \bigcup \{m\}$ \; - AB\_deliver(m) \; - } - } - } -\caption{AB\_Listen} + \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} \ No newline at end of file diff --git a/recherches/ALDLoverAB/intro/index.tex b/recherches/ALDLoverAB/intro/index.tex index 81a78a7..2064575 100644 --- a/recherches/ALDLoverAB/intro/index.tex +++ b/recherches/ALDLoverAB/intro/index.tex @@ -1,61 +1,77 @@ \subsubsection{Model Properties} -The model is defined as Message-passing Aysnchronous. \\ -There is n process. Each process is associated to a unique unforgeable id $i$.\\ -Each process know the identity of all the process in the system\\ -Each process have a reliable communication channel with all the others process such as: -\begin{itemize} - \item send(m) is the send primitive - \item recv(m) is the reception primitive -\end{itemize} -A message send is eventualy received\\ -The system is Crash-Prone. There is at most f process who can crash such as f < n.\\ +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 \forall p_j : \text{correct}(p_j) \Rightarrow \text{bc-recv}_j(m)$ +\end{property} \subsubsection{AtomicBroadcast Properties} -\begin{theorem}{AB\_broadcast Validity} - if a message is sent by a correct process, the message is eventually received by all the correct process. -\end{theorem} - -\begin{theorem}{AB\_receive Validity} - if a message is received by a correct process, the message is eventually received by all the correct process. -\end{theorem} - -\begin{theorem}{AB\_receive safety No creation} - if a message is received by a correct process, the message was emitted by a correct porcess. -\end{theorem} - -\begin{theorem}{AB\_receive safety No duplication} - each message is received at most 1 time by each process. -\end{theorem} - -\begin{theorem}{AB\_receive safety Ordering} - $\forall m_1, m_2$ two messages, $\forall p_i, p_j$ two process. \\ - if AB\_recv(m1) and AB\_recv(m2) for $p_i, p_j$ \\ - and AB\_recv(m1) is before AB\_recv(m2) for $p_i$ \\ - so AB\_recv(m1) is before AB\_recv(m2) for $p_j$ \\ -\end{theorem} - +\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} -\begin{theorem}{APPEND Validity} - a APPEND(x) is valid iff the process p who sent the operation is such as $p \in \Pi_M$. - And iff $x \in S$ where S is a set of valid values. -\end{theorem} +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{theorem}{PROVE Validity} - a PROVE(x) is valid iff the process $p$ who sent the operation is such as $p \in \Pi_V$. - And iff $\exists$ APPEND(x) who appears before PROVE(x) in Seq. -\end{theorem} +\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{theorem}{PROGRESS} - if an APPEND(x) is invoked, so there is a point in the linearization of the operations such as all PROVE(x) are valids. -\end{theorem} +\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{theorem}{READ Validity} +\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{theorem} \ No newline at end of file +\end{property} \ No newline at end of file diff --git a/recherches/ALDLoverAB/main.aux b/recherches/ALDLoverAB/main.aux index 5b3db63..052915e 100644 --- a/recherches/ALDLoverAB/main.aux +++ b/recherches/ALDLoverAB/main.aux @@ -6,16 +6,15 @@ \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}Algorithms}{1}{}\protected@file@percent } -\@writefile{loa}{\contentsline {algocf}{\numberline {1}{\ignorespaces \textbf {Upon} RB\_deliver(m)}}{2}{}\protected@file@percent } -\@writefile{loa}{\contentsline {algocf}{\numberline {2}{\ignorespaces AB\_Broadcast}}{2}{}\protected@file@percent } -\@writefile{loa}{\contentsline {algocf}{\numberline {3}{\ignorespaces AB\_Listen}}{2}{}\protected@file@percent } +\@writefile{toc}{\contentsline {subsubsection}{\numberline {1.1.2}Reliable Broadcast Properties}{1}{}\protected@file@percent } +\@writefile{toc}{\contentsline {subsubsection}{\numberline {1.1.3}AtomicBroadcast Properties}{1}{}\protected@file@percent } +\@writefile{toc}{\contentsline {subsubsection}{\numberline {1.1.4}DenyList Properties}{1}{}\protected@file@percent } +\@writefile{toc}{\contentsline {subsection}{\numberline {1.2}Algorithms}{2}{}\protected@file@percent } +\@writefile{toc}{\contentsline {subsection}{\numberline {1.3}proof}{2}{}\protected@file@percent } +\@writefile{toc}{\contentsline {subsubsection}{\numberline {1.3.1}Broadcast Validity}{4}{}\protected@file@percent } \abx@aux@read@bbl@mdfivesum{76D65A242EC496C9B4361AF646FF12CB} -\gdef \@abspage@last{3} +\gdef \@abspage@last{6} diff --git a/recherches/ALDLoverAB/main.fdb_latexmk b/recherches/ALDLoverAB/main.fdb_latexmk index 38c50ca..393f941 100644 --- a/recherches/ALDLoverAB/main.fdb_latexmk +++ b/recherches/ALDLoverAB/main.fdb_latexmk @@ -1,42 +1,60 @@ # Fdb version 4 -["biber main"] 0 "main.bcf" "main.bbl" "main" 1746172816.43057 -1 - "main.bcf" 1746172816.38112 108486 d8549f9e7d9f09af6a94b466d27b9f55 "pdflatex" +["biber main"] 0 "main.bcf" "main.bbl" "main" 1747309539.09877 -1 + "main.bcf" 1747309539.00575 108486 d8549f9e7d9f09af6a94b466d27b9f55 "pdflatex" "sources.bib" 1745505510 0 d41d8cd98f00b204e9800998ecf8427e "" (generated) "main.bbl" "main.blg" (rewritten before read) -["pdflatex"] 1746172815.97294 "/workspaces/containers/recherches/ALDLoverAB/main.tex" "main.pdf" "main" 1746172816.431 0 +["pdflatex"] 1747309538.15653 "/workspaces/containers/recherches/ALDLoverAB/main.tex" "main.pdf" "main" 1747309539.09917 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/ecbi0500.tfm" 1136768653 3072 5c02773c2e93e883bb03697d9281a6c7 "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecbi0700.tfm" 1136768653 3072 d954c3b8c413504af8820bec51a4b82c "" "/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecbi1000.tfm" 1136768653 3072 e6fe53b666f9cbd66cb135c6fdea66d3 "" - "/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/ecit0800.tfm" 1136768653 1536 09682d3e827df9145fea3c41a21d8b01 "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecit1000.tfm" 1136768653 1536 34ad639b0caa1b405dc14b9703b4e5b9 "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecrm0500.tfm" 1136768653 3584 178baad7ffca7f5d3428a83bd7cc64c3 "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecrm0700.tfm" 1136768653 3584 cf973739aac7ab6247f9150296af7954 "" "/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/ecti0500.tfm" 1136768653 3072 3d6a4805e3f8c4693f997dc6a16a6b93 "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecti0700.tfm" 1136768653 3072 b90b057319ce008920857c32d19eeb4d "" "/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/tfm/jknappen/ec/ectt0800.tfm" 1136768653 1536 0b0b8ca286de6a006b681926403f35cd "" "/usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ectt1000.tfm" 1136768653 1536 06717a2b50de47d4087ac0e6cd759455 "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/cmextra/cmex7.tfm" 1246382020 1004 54797486969f23fa377b128694d548df "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm" 1246382020 916 f87d7c45f9c908e672703b83b72241a3 "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam5.tfm" 1246382020 924 9904cf1d39e9767e7a3622f2a125a565 "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam7.tfm" 1246382020 928 2dc8d444221b7a635bb58038579b861a "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm" 1246382020 908 2921f8a10601f252058503cc6570e581 "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm5.tfm" 1246382020 940 75ac932a52f80982a9f8ea75d03a34cf "" + "/usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm7.tfm" 1246382020 940 228d6584342e91276bf566bcf9716b83 "" "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmex10.pfb" 1248133631 30251 6afa5cb1d0204815a708a080681d4674 "" "/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/cmmi5.pfb" 1248133631 37912 77d683123f92148345f3fc36a38d9ab1 "" "/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/cmr5.pfb" 1248133631 31809 8670ca339bf94e56da1fc21c80635e2a "" "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb" 1248133631 32762 224316ccc9ad3ca0423a14971cfa7fc1 "" "/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/amsfonts/cm/cmsy7.pfb" 1248133631 32716 08e384dc442464e7285e891af9f45947 "" + "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/symbols/msam10.pfb" 1248133631 31764 459c573c03a4949a528c2cc7f557e217 "" "/usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbi1000.pfb" 1215737283 193571 dce9a978093738902238b3e227edef6c "" - "/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/sfit1000.pfb" 1215737283 157419 ef2add7d886ed65124e72477bd51c8f4 "" "/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/sfti0700.pfb" 1215737283 184338 71ec80cd6b45d5405da0f23c65ebdef8 "" "/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/fonts/type1/public/cm-super/sftt1000.pfb" 1215737283 169201 9ebf99020dde51a5086e186761a34e8f "" @@ -49,7 +67,18 @@ "/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/algorithmicx/algorithmicx.sty" 1160617237 26750 ce139c05a983e19ddca355b43e29c395 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/algorithmicx/algpseudocode.sty" 1160617237 3457 d9077efe6b74c5a094199256af8d7d9a "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/algorithms/algorithm.sty" 1251330371 3249 15763257e50278eef5db1952ccde229c "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/amsfonts.sty" 1359763108 5949 3f3fd50a8cc94c3d4cbf4fc66cd3df1c "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/amssymb.sty" 1359763108 13829 94730e64147574077f8ecfea9bb69af4 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/umsa.fd" 1359763108 961 6518c6525a34feb5e8250ffa91731cff "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/umsb.fd" 1359763108 961 d02606146ba5601b5645f987c92e6193 "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsbsy.sty" 1717359999 2222 2166a1f7827be30ddc30434e5efcee1b "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsgen.sty" 1717359999 4173 d22509bc0c91281d991b2de7c88720dd "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsmath.sty" 1730928152 88370 c780f23aea0ece6add91e09b44dca2cd "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsopn.sty" 1717359999 4474 23ca1d3a79a57b405388059456d0a8df "" + "/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amstext.sty" 1717359999 2444 71618ea5f2377e33b04fb97afdd0eac2 "" "/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 "" @@ -70,8 +99,8 @@ "/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/float/float.sty" 1137110151 6749 16d2656a1984957e674b149555f1ea1d "" "/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 "" @@ -81,20 +110,19 @@ "/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/ALDLoverAB/main.tex" 1745569300.58113 728 260366a29ef55ffa4b47d22972e9e4f8 "" - "algo/index.tex" 1746172815.76911 1775 b458edc79675260c269751db3322cda9 "" - "intro/index.tex" 1745569389.83114 2291 8451d9b4ced1f44c45b59e7619773077 "" - "main.aux" 1746172816.38012 1400 8864237b874322217e4ed828cbb90076 "pdflatex" - "main.bbl" 1746171033.92694 466 76d65a242ec496c9b4361af646ff12cb "biber main" - "main.run.xml" 1746172816.38212 2301 7adc9b5a22e7927ebfdd8580ad5d647d "pdflatex" - "main.tex" 1745569300.58113 728 260366a29ef55ffa4b47d22972e9e4f8 "" + "/workspaces/containers/recherches/ALDLoverAB/main.tex" 1747299196.84721 1315 a94740caa185b946ba5aaded501a4fac "" + "algo/index.tex" 1747297294.63478 3848 bbe77613f7a73141ef38e5297b411992 "" + "intro/index.tex" 1747297807.29159 3161 448e66cc700f6c11abf8aafdf01ab6a8 "" + "main.aux" 1747309539.00275 1342 dbdb34d6c1afc7be4a9ecbc27e420731 "pdflatex" + "main.bbl" 1747233716.74109 466 76d65a242ec496c9b4361af646ff12cb "biber main" + "main.run.xml" 1747309539.00575 2301 7adc9b5a22e7927ebfdd8580ad5d647d "pdflatex" + "main.tex" 1747299196.84721 1315 a94740caa185b946ba5aaded501a4fac "" + "proof/index.tex" 1747309536.90972 6390 ff2a2396c48aac05b56092c04c844d25 "" (generated) "main.aux" "main.bcf" diff --git a/recherches/ALDLoverAB/main.fls b/recherches/ALDLoverAB/main.fls index 7392bf4..f01c089 100644 --- a/recherches/ALDLoverAB/main.fls +++ b/recherches/ALDLoverAB/main.fls @@ -43,6 +43,20 @@ 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/amsmath/amsmath.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsmath.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsopn.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amstext.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amstext.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsgen.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsgen.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsbsy.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsbsy.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsopn.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/amssymb.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/amssymb.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/amsfonts.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/amsfonts.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 @@ -95,14 +109,14 @@ 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 /usr/local/texlive/2025/texmf-dist/tex/latex/algorithms/algorithm.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/algorithms/algorithm.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/float/float.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/float/float.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/algorithmicx/algorithmicx.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/algorithmicx/algorithmicx.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/algorithmicx/algpseudocode.sty +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/algorithmicx/algpseudocode.sty INPUT ./main.aux INPUT ./main.aux INPUT main.aux @@ -130,12 +144,39 @@ 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 /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/cmextra/cmex7.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/cmextra/cmex7.tfm +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/umsa.fd +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/umsa.fd +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/umsa.fd +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam7.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam5.tfm +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/umsb.fd +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/umsb.fd +INPUT /usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/umsb.fd +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm7.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm5.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecti0700.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecti0500.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ectt1000.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecrm0700.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ectt0800.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecrm0500.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ectt0800.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecit1000.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecit0800.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecit0800.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 ./proof/index.tex +INPUT ./proof/index.tex +INPUT proof/index.tex INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecbi1000.tfm -INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ectt1000.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecbi0700.tfm +INPUT /usr/local/texlive/2025/texmf-dist/fonts/tfm/jknappen/ec/ecbi0500.tfm INPUT main.aux INPUT main.run.xml OUTPUT main.run.xml @@ -144,17 +185,20 @@ INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.p INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi5.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/cmr5.pfb INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.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/amsfonts/cm/cmsy7.pfb +INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/amsfonts/symbols/msam10.pfb INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sfbi1000.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/sfit1000.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/sfti0700.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 INPUT /usr/local/texlive/2025/texmf-dist/fonts/type1/public/cm-super/sftt1000.pfb diff --git a/recherches/ALDLoverAB/main.log b/recherches/ALDLoverAB/main.log index 9f53428..ac01fcf 100644 --- a/recherches/ALDLoverAB/main.log +++ b/recherches/ALDLoverAB/main.log @@ -1,4 +1,4 @@ -This is pdfTeX, Version 3.141592653-2.6-1.40.27 (TeX Live 2025) (preloaded format=pdflatex 2025.3.30) 2 MAY 2025 08:00 +This is pdfTeX, Version 3.141592653-2.6-1.40.27 (TeX Live 2025) (preloaded format=pdflatex 2025.3.30) 15 MAY 2025 11:45 entering extended mode restricted \write18 enabled. file:line:error style messages enabled. @@ -100,7 +100,80 @@ Package: authblk 2001/02/27 1.3 (PWD) ) (/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 +) (/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsmath.sty +Package: amsmath 2024/11/05 v2.17t AMS math features +\@mathmargin=\skip54 + +For additional information on amsmath, use the `?' option. +(/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amstext.sty +Package: amstext 2021/08/26 v2.01 AMS text + (/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsgen.sty +File: amsgen.sty 1999/11/30 v2.0 generic functions +\@emptytoks=\toks22 +\ex@=\dimen152 +)) (/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsbsy.sty +Package: amsbsy 1999/11/29 v1.2d Bold Symbols +\pmbraise@=\dimen153 +) (/usr/local/texlive/2025/texmf-dist/tex/latex/amsmath/amsopn.sty +Package: amsopn 2022/04/08 v2.04 operator names +) +\inf@bad=\count289 +LaTeX Info: Redefining \frac on input line 233. +\uproot@=\count290 +\leftroot@=\count291 +LaTeX Info: Redefining \overline on input line 398. +LaTeX Info: Redefining \colon on input line 409. +\classnum@=\count292 +\DOTSCASE@=\count293 +LaTeX Info: Redefining \ldots on input line 495. +LaTeX Info: Redefining \dots on input line 498. +LaTeX Info: Redefining \cdots on input line 619. +\Mathstrutbox@=\box52 +\strutbox@=\box53 +LaTeX Info: Redefining \big on input line 721. +LaTeX Info: Redefining \Big on input line 722. +LaTeX Info: Redefining \bigg on input line 723. +LaTeX Info: Redefining \Bigg on input line 724. +\big@size=\dimen154 +LaTeX Font Info: Redeclaring font encoding OML on input line 742. +LaTeX Font Info: Redeclaring font encoding OMS on input line 743. +\macc@depth=\count294 +LaTeX Info: Redefining \bmod on input line 904. +LaTeX Info: Redefining \pmod on input line 909. +LaTeX Info: Redefining \smash on input line 939. +LaTeX Info: Redefining \relbar on input line 969. +LaTeX Info: Redefining \Relbar on input line 970. +\c@MaxMatrixCols=\count295 +\dotsspace@=\muskip17 +\c@parentequation=\count296 +\dspbrk@lvl=\count297 +\tag@help=\toks23 +\row@=\count298 +\column@=\count299 +\maxfields@=\count300 +\andhelp@=\toks24 +\eqnshift@=\dimen155 +\alignsep@=\dimen156 +\tagshift@=\dimen157 +\tagwidth@=\dimen158 +\totwidth@=\dimen159 +\lineht@=\dimen160 +\@envbody=\toks25 +\multlinegap=\skip55 +\multlinetaggap=\skip56 +\mathdisplay@stack=\toks26 +LaTeX Info: Redefining \[ on input line 2953. +LaTeX Info: Redefining \] on input line 2954. +) (/usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/amssymb.sty +Package: amssymb 2013/01/14 v3.01 AMS font symbols + (/usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/amsfonts.sty +Package: amsfonts 2013/01/14 v3.01 Basic AMSFonts support +\symAMSa=\mathgroup4 +\symAMSb=\mathgroup5 +LaTeX Font Info: Redeclaring math symbol \hbar on input line 98. +LaTeX Font Info: Overwriting math alphabet `\mathfrak' in version `bold' +(Font) U/euf/m/n --> U/euf/b/n on input line 106. +)) (/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) @@ -120,72 +193,72 @@ Package: kvoptions 2022-06-15 v3.15 Key value format for package options (HO) 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 +\lrq@indent=\count301 (/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 +\Urlmuskip=\muskip18 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 +\c@tabx@nest=\count302 +\c@listtotal=\count303 +\c@listcount=\count304 +\c@liststart=\count305 +\c@liststop=\count306 +\c@citecount=\count307 +\c@citetotal=\count308 +\c@multicitecount=\count309 +\c@multicitetotal=\count310 +\c@instcount=\count311 +\c@maxnames=\count312 +\c@minnames=\count313 +\c@maxitems=\count314 +\c@minitems=\count315 +\c@citecounter=\count316 +\c@maxcitecounter=\count317 +\c@savedcitecounter=\count318 +\c@uniquelist=\count319 +\c@uniquename=\count320 +\c@refsection=\count321 +\c@refsegment=\count322 +\c@maxextratitle=\count323 +\c@maxextratitleyear=\count324 +\c@maxextraname=\count325 +\c@maxextradate=\count326 +\c@maxextraalpha=\count327 +\c@abbrvpenalty=\count328 +\c@highnamepenalty=\count329 +\c@lownamepenalty=\count330 +\c@maxparens=\count331 +\c@parenlevel=\count332 +\blx@tempcnta=\count333 +\blx@tempcntb=\count334 +\blx@tempcntc=\count335 +\c@blx@maxsection=\count336 +\blx@maxsegment@0=\count337 +\blx@notetype=\count338 +\blx@parenlevel@text=\count339 +\blx@parenlevel@foot=\count340 +\blx@sectionciteorder@0=\count341 +\blx@sectionciteorderinternal@0=\count342 +\blx@entrysetcounter=\count343 +\blx@biblioinstance=\count344 +\labelnumberwidth=\skip57 +\labelalphawidth=\skip58 +\biblabelsep=\skip59 +\bibitemsep=\skip60 +\bibnamesep=\skip61 +\bibinitsep=\skip62 +\bibparsep=\skip63 +\bibhang=\skip64 \blx@bcfin=\read3 \blx@bcfout=\write3 \blx@langwohyphens=\language91 -\c@mincomprange=\count333 -\c@maxcomprange=\count334 -\c@mincompwidth=\count335 +\c@mincomprange=\count345 +\c@maxcomprange=\count346 +\c@mincompwidth=\count347 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 @@ -193,88 +266,88 @@ 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 +\c@afterword=\count348 +\c@savedafterword=\count349 +\c@annotator=\count350 +\c@savedannotator=\count351 +\c@author=\count352 +\c@savedauthor=\count353 +\c@bookauthor=\count354 +\c@savedbookauthor=\count355 +\c@commentator=\count356 +\c@savedcommentator=\count357 +\c@editor=\count358 +\c@savededitor=\count359 +\c@editora=\count360 +\c@savededitora=\count361 +\c@editorb=\count362 +\c@savededitorb=\count363 +\c@editorc=\count364 +\c@savededitorc=\count365 +\c@foreword=\count366 +\c@savedforeword=\count367 +\c@holder=\count368 +\c@savedholder=\count369 +\c@introduction=\count370 +\c@savedintroduction=\count371 +\c@namea=\count372 +\c@savednamea=\count373 +\c@nameb=\count374 +\c@savednameb=\count375 +\c@namec=\count376 +\c@savednamec=\count377 +\c@translator=\count378 +\c@savedtranslator=\count379 +\c@shortauthor=\count380 +\c@savedshortauthor=\count381 +\c@shorteditor=\count382 +\c@savedshorteditor=\count383 +\c@labelname=\count384 +\c@savedlabelname=\count385 +\c@institution=\count386 +\c@savedinstitution=\count387 +\c@lista=\count388 +\c@savedlista=\count389 +\c@listb=\count390 +\c@savedlistb=\count391 +\c@listc=\count392 +\c@savedlistc=\count393 +\c@listd=\count394 +\c@savedlistd=\count395 +\c@liste=\count396 +\c@savedliste=\count397 +\c@listf=\count398 +\c@savedlistf=\count399 +\c@location=\count400 +\c@savedlocation=\count401 +\c@organization=\count402 +\c@savedorganization=\count403 +\c@origlocation=\count404 +\c@savedoriglocation=\count405 +\c@origpublisher=\count406 +\c@savedorigpublisher=\count407 +\c@publisher=\count408 +\c@savedpublisher=\count409 +\c@language=\count410 +\c@savedlanguage=\count411 +\c@origlanguage=\count412 +\c@savedoriglanguage=\count413 +\c@pageref=\count414 +\c@savedpageref=\count415 +\shorthandwidth=\skip65 +\shortjournalwidth=\skip66 +\shortserieswidth=\skip67 +\shorttitlewidth=\skip68 +\shortauthorwidth=\skip69 +\shorteditorwidth=\skip70 +\locallabelnumberwidth=\skip71 +\locallabelalphawidth=\skip72 +\localshorthandwidth=\skip73 +\localshortjournalwidth=\skip74 +\localshortserieswidth=\skip75 +\localshorttitlewidth=\skip76 +\localshortauthorwidth=\skip77 +\localshorteditorwidth=\skip78 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 @@ -284,19 +357,19 @@ 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 +\c@textcitecount=\count416 +\c@textcitetotal=\count417 +\c@textcitemaxnames=\count418 +\c@biburlbigbreakpenalty=\count419 +\c@biburlbreakpenalty=\count420 +\c@biburlnumpenalty=\count421 +\c@biburlucpenalty=\count422 +\c@biburllcpenalty=\count423 +\biburlbigskip=\muskip19 +\biburlnumskip=\muskip20 +\biburlucskip=\muskip21 +\biburllcskip=\muskip22 +\c@smartand=\count424 ) Package biblatex Info: Trying to load bibliography style 'numeric'... Package biblatex Info: ... file 'numeric.bbx' found. @@ -306,8 +379,8 @@ 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 +\c@bbx:relatedcount=\count425 +\c@bbx:relatedtotal=\count426 )) Package biblatex Info: Trying to load citation style 'numeric'... Package biblatex Info: ... file 'numeric.cbx' found. @@ -336,8 +409,8 @@ Package biblatex Info: Document encoding is UTF8 .... 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 +\l__color_backend_stack_int=\count427 +\l__pdf_internal_box=\box54 )) Package biblatex Info: ... and expl3 (biblatex) 2025-01-18 L3 programming layer (loader) @@ -347,81 +420,67 @@ Package biblatex Info: ... and expl3 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 +)) (/usr/local/texlive/2025/texmf-dist/tex/latex/algorithms/algorithm.sty +Package: algorithm 2009/08/24 v0.1 Document Style `algorithm' - floating environment + (/usr/local/texlive/2025/texmf-dist/tex/latex/float/float.sty +Package: float 2001/11/08 v1.3d Float enhancements (AL) +\c@float@type=\count428 +\float@exts=\toks27 +\float@box=\box55 +\@float@everytoks=\toks28 +\@floatcapt=\box56 ) -\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 +\@float@every@algorithm=\toks29 +\c@algorithm=\count429 +) (/usr/local/texlive/2025/texmf-dist/tex/latex/algorithmicx/algorithmicx.sty +Package: algorithmicx 2005/04/27 v1.2 Algorithmicx + +Document Style algorithmicx 1.2 - a greatly improved `algorithmic' style +\c@ALG@line=\count430 +\c@ALG@rem=\count431 +\c@ALG@nested=\count432 +\ALG@tlm=\skip79 +\ALG@thistlm=\skip80 +\c@ALG@Lnr=\count433 +\c@ALG@blocknr=\count434 +\c@ALG@storecount=\count435 +\c@ALG@tmpcounter=\count436 +\ALG@tmplength=\skip81 +) (/usr/local/texlive/2025/texmf-dist/tex/latex/algorithmicx/algpseudocode.sty +Package: algpseudocode + +Document Style - pseudocode environments for use with the `algorithmicx' style ) -\c@theorem=\count421 +\c@algoLine=\count437 +\c@property=\count438 +\c@theorem=\count439 +\c@proof=\count440 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. +(babel) Reported on input line 9. ) \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. +LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 37. +LaTeX Font Info: ... okay on input line 37. +LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 37. +LaTeX Font Info: ... okay on input line 37. +LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 37. +LaTeX Font Info: ... okay on input line 37. +LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 37. +LaTeX Font Info: ... okay on input line 37. +LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 37. +LaTeX Font Info: ... okay on input line 37. +LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 37. +LaTeX Font Info: ... okay on input line 37. +LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 37. +LaTeX Font Info: ... okay on input line 37. +LaTeX Info: Redefining \degres on input line 37. +LaTeX Info: Redefining \up on input line 37. 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 @@ -435,36 +494,55 @@ Package biblatex Info: Automatic encoding selection. 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. +Package biblatex Info: Reference section=0 on input line 37. +Package biblatex Info: Reference segment=0 on input line 37. [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. +LaTeX Font Info: Trying to load font information for U+msa on input line 6. + (/usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/umsa.fd +File: umsa.fd 2013/01/14 v3.01 AMS symbols A +) +LaTeX Font Info: Trying to load font information for U+msb on input line 6. + (/usr/local/texlive/2025/texmf-dist/tex/latex/amsfonts/umsb.fd +File: umsb.fd 2013/01/14 v3.01 AMS symbols B +) +Underfull \hbox (badness 10000) in paragraph at lines 4--10 + + [] + Underfull \hbox (badness 10000) in paragraph at lines 12--14 [] -Underfull \hbox (badness 10000) in paragraph at lines 34--39 +Underfull \hbox (badness 10000) in paragraph at lines 35--39 [] -) (./algo/index.tex -[1]) -LaTeX Warning: Empty bibliography on input line 38. +[1]) (./algo/index.tex) (./proof/index.tex + +[2] + +[3] +Underfull \hbox (badness 10000) in paragraph at lines 94--95 + + [] -[2] (./main.aux) +[4]) + +LaTeX Warning: Empty bibliography on input line 60. + + + +[5] (./main.aux) *********** LaTeX2e <2024-11-01> patch level 2 L3 programming layer <2025-01-18> @@ -474,18 +552,18 @@ Package logreq Info: Writing requests to 'main.run.xml'. ) Here is how much of TeX's memory you used: - 12405 strings out of 473190 - 235037 string characters out of 5715806 - 1089239 words of memory out of 5000000 - 35574 multiletter control sequences out of 15000+600000 - 567392 words of font info for 48 fonts, out of 8000000 for 9000 + 13334 strings out of 473190 + 244064 string characters out of 5715806 + 1101105 words of memory out of 5000000 + 36455 multiletter control sequences out of 15000+600000 + 574192 words of font info for 66 fonts, out of 8000000 for 9000 1141 hyphenation exceptions out of 8191 - 66i,18n,81p,738b,1731s stack positions out of 10000i,1000n,20000p,200000b,200000s - -Output written on main.pdf (3 pages, 262569 bytes). + 66i,14n,81p,738b,1733s stack positions out of 10000i,1000n,20000p,200000b,200000s + +Output written on main.pdf (6 pages, 341015 bytes). PDF statistics: - 110 PDF objects out of 1000 (max. 8388607) - 66 compressed objects within 1 object stream + 134 PDF objects out of 1000 (max. 8388607) + 81 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) diff --git a/recherches/ALDLoverAB/main.pdf b/recherches/ALDLoverAB/main.pdf index c936c9f..c43fa0f 100644 Binary files a/recherches/ALDLoverAB/main.pdf and b/recherches/ALDLoverAB/main.pdf differ diff --git a/recherches/ALDLoverAB/main.synctex.gz b/recherches/ALDLoverAB/main.synctex.gz index 0850729..c1995ee 100644 Binary files a/recherches/ALDLoverAB/main.synctex.gz and b/recherches/ALDLoverAB/main.synctex.gz differ diff --git a/recherches/ALDLoverAB/main.tex b/recherches/ALDLoverAB/main.tex index b23ae54..d8ca704 100644 --- a/recherches/ALDLoverAB/main.tex +++ b/recherches/ALDLoverAB/main.tex @@ -7,11 +7,30 @@ \usepackage[affil-it]{authblk} \usepackage{fullpage} +\usepackage{amsmath} +\usepackage{amssymb} + \usepackage{biblatex} -\usepackage[linesnumbered,ruled,vlined]{algorithm2e} +% \usepackage[linesnumbered,ruled,vlined]{algorithm2e} +\usepackage{algorithm} +\usepackage{algorithmicx} +\usepackage[noend]{algpseudocode} +\algrenewcommand\alglinenumber[1]{\tiny #1} -\newtheorem{theorem}{Property} +\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} @@ -35,6 +54,9 @@ \subsection{Algorithms} \input{algo/index.tex} +\subsection{proof} +\input{proof/index.tex} + \printbibliography diff --git a/recherches/ALDLoverAB/proof/index.tex b/recherches/ALDLoverAB/proof/index.tex new file mode 100644 index 0000000..a41d896 --- /dev/null +++ b/recherches/ALDLoverAB/proof/index.tex @@ -0,0 +1,121 @@ +\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*} \ No newline at end of file