fin (?) de la spec de BFT-DL + debut de preuve de l'algo pour BFT ARB

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

@@ -48,62 +48,65 @@ There are 3 operations : $\BFTPROVE(x), \BFTAPPEND(x), \BFTREAD(x)$ such that :
 
 \subsection{DL $\Rightarrow$ t-BFT-DL}
 
-\begin{lemma}
+
-    For any fixed value $t$ such that $3t < |M|$, multiple DenyList Object can be used to implement a t-Byzantine Fault Tolerant DenyList Object.
+Fix $3t < |M|$. Let
+\[
+\mathcal{U} = \{\, U \subseteq M \mid |U| = |M| - t \,\}.
+\]
+For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose authorization sets are
+\[
+\Pi_M(DL_T) = S_T = U
+\qquad\text{and}\qquad
+\Pi_V(DL_T) = V.
+\]
+
+\[
+|\mathcal{U}| = \binom{|M|}{|M| - t}.
+\]
+
+\begin{algorithmic}[1]
+    
+    % \renewcommand{\algletter}{}
+    \begin{algorithm}[H]
+        \caption{t-BFT-DL implementation using multiple DL objects}
+
+        % \caption{\BFTAPPEND}
+        \Function{$\BFTAPPEND$}{x}
+            \For{\textbf{each } $U \in \mathcal{U}$ st $i \in U$} 
+            \State $DL_U.\APPEND(x)$
+            \EndFor
+        \EndFunction
+
+        \vspace{1em}
+    
+        % \caption{\BFTPROVE}
+        \Function{$\BFTPROVE$}{x}
+            \State $state \gets false$
+            \For{\textbf{each } $U \in \mathcal{U}$}
+                \State $state \gets state \textbf{ OR } DL_U.\PROVE(x)$
+            \EndFor
+            \State \Return $state$
+        \EndFunction
+
+        \vspace{1em}
+    
+        % \caption{\BFTREAD}
+        \Function{$\BFTREAD$}{$\bot$}
+            \State $results \gets \emptyset$
+            \For{\textbf{each } $U \in \mathcal{U}$}
+                \State $results \gets results \cup DL_U.\READ()$
+            \EndFor
+            \State \Return $results$
+        \EndFunction
+    \end{algorithm}
+\end{algorithmic}
+
+\begin{lemma}[BFT-PROVE Validity]
+    The invocation of $op = \BFTPROVE(x)$ by a correct process is invalid iff there exist at least $t+1$ distinct processes in $M$ that invoked a valid $\BFTAPPEND(x)$ before $op$ in $\Seq$.
 \end{lemma}
 
 \begin{proof}
-    Fix $3t < |M|$. Let
+    Let $op=\BFTPROVE(x)$ be an invocation by a correct process $p_i$. Let $A\subseteq M$ be the set of distinct issuers that invoked $\BFTAPPEND(x)$ before $op$ in $\Seq$.
-    \[
-    \mathcal{U} = \{\, U \subseteq M \mid |U| = |M| - t \,\}.
-    \]
-    For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose authorization sets are
-    \[
-    \Pi_M(DL_T) = S_T = U
-    \qquad\text{and}\qquad
-    \Pi_V(DL_T) = V.
-    \]
-    
-    \[
-    |\mathcal{U}| = \binom{|M|}{|M| - t}.
-    \]
-
-    \begin{algorithmic}[1]
-
-        \renewcommand{\algletter}{DL}
-        \begin{algorithm}[H]
-            \caption{\BFTAPPEND}
-            \Function{$\BFTAPPEND$}{x}
-                \For{\textbf{each } $U \in \mathcal{U}$ st $i \in U$} 
-                \State $DL_U.\APPEND(x)$
-                \EndFor
-            \EndFunction
-        \end{algorithm}
-        
-        \begin{algorithm}[H]
-            \caption{\BFTPROVE}
-            \Function{$\BFTPROVE$}{x}
-                \State $state \gets false$
-                \For{\textbf{each } $U \in \mathcal{U}$}
-                    \State $state \gets state \textbf{ OR } DL_U.\PROVE(x)$
-                \EndFor
-                \State \Return $state$
-            \EndFunction
-        \end{algorithm}
-        
-        \begin{algorithm}[H]
-            \caption{\BFTREAD}
-            \Function{$\BFTREAD$}{$\bot$}
-                \State $results \gets \emptyset$
-                \For{\textbf{each } $U \in \mathcal{U}$}
-                    \State $results \gets results \cup DL_U.\READ()$
-                \EndFor
-                \State \Return $results$
-            \EndFunction
-        \end{algorithm}
-    \end{algorithmic}
-        
-    \paragraph{BFT-PROVE Validity.} Let $op=\BFTPROVE(x)$ be an invocation by a correct process $p_i$. Let $A\subseteq M$ be the set of distinct issuers that invoked $\BFTAPPEND(x)$ before $op$ in $\Seq$.
 
     \begin{itemize}
         \item \textbf{Case (i): $|A|\ge t+1$.} 
@@ -115,8 +118,14 @@ There are 3 operations : $\BFTPROVE(x), \BFTAPPEND(x), \BFTREAD(x)$ such that :
         
     \smallskip
     Combining the cases yields the claimed characterization of invalidity.
+\end{proof}
 
-    \paragraph{BFT-PROVE Anti-Flickering.} Let $op=\BFTPROVE(x)$ be an invocation by a correct process $p_i$ that is \emph{invalid} in $\Seq$.
+\begin{lemma}[BFT-PROVE Anti-Flickering]
+    If the invocation of a operation $op = \BFTPROVE(x)$ by a correct process $p \in \Pi_V$ is invalid, then any $\BFTPROVE(x)$ operation that appears after $op$ in $\Seq$ is invalid.
+\end{lemma}
+
+\begin{proof}
+    Let $op=\BFTPROVE(x)$ be an invocation by a correct process $p_i$ that is \emph{invalid} in $\Seq$.
     By BFT-PROVE Validity, this implies that there exist at least $t+1$ \emph{distinct} processes in $M$ that invoked a \emph{valid} $\BFTAPPEND(x)$ before $op$ in $\Seq$. Let $A\subseteq M$ denote that set, with $|A|\ge t+1$.
 
     Fix any $U\in\mathcal{U}$. We have $A\cap U\neq\emptyset$. Pick $j\in A\cap U$. Since $j\in U$, the call $\BFTAPPEND^{(j)}(x)$ triggers a call $DL_U.\APPEND(x)$. Moreover, because $\BFTAPPEND^{(j)}(x)\prec op$ in $\Seq$, the induced $DL_U.\APPEND(x)$ appears before the induced $DL_U.\PROVE(x)$ of $op$ in the projection $\Seq_U$.
@@ -126,51 +135,57 @@ There are 3 operations : $\BFTPROVE(x), \BFTAPPEND(x), \BFTREAD(x)$ such that :
     Let $op'=\BFTPROVE(x)$ be any invocation such that $op\prec op'$ in $\Seq$. Fix again any $U\in\mathcal{U}$. Hence, the $DL_U.\PROVE(x)$ induced by $op'$ appears after the $DL_U.\PROVE(x)$ induced by $op$ in $\Seq_U$. Since the induced $DL_U.\PROVE(x)$ of $op$ is invalid, by \textbf{PROVE Anti-Flickering} of $\DL$, \emph{every} subsequent $DL_U.\PROVE(x)$ in $\Seq_U$ is invalid.
 
     As this holds for every $U\in\mathcal{U}$, there is no component $DL_U$ in which the induced $\PROVE(x)$ of $op'$ is valid.
+\end{proof}
 
-    \paragraph{READ Liveness.} Let $R$ the result of a $READ()$ operation submit by any correct process. $(i, \PROVEtrace(x)) \in R$ implie that $\exists U^\star \in \mathcal{U}$ such that $(i, \PROVEtrace(x)) \in R^{U^\star}$ with $R^{U^\star}$ the result of $DL_{U^\star}.\READ()$. By \textbf{READ Validity} $(i, \PROVEtrace(x)) \in R^{U^\star}$ implie that there exist a valid  $DL_{U^\star}.\PROVE^{(i)}(x)$. The for loop in the $\BFTPROVE(x)$ implementation return true iff there at least one valid $DL_{U}.\PROVE^{(i)}(x)$ for any $U \in \mathcal{U}$.
+\begin{lemma}[READ Liveness]
+    Let $op = \BFTREAD()$ invoke by a correct process such that $R$ is the result of $op$. For all $(i, \PROVEtrace(x)) \in R$ there exist a valid invocation of $\BFTPROVE(x)$ by $p_i$. 
+\end{lemma}
+
+\begin{proof}
+    Let $R$ the result of a $READ()$ operation submit by any correct process. $(i, \PROVEtrace(x)) \in R$ implie that $\exists U^\star \in \mathcal{U}$ such that $(i, \PROVEtrace(x)) \in R^{U^\star}$ with $R^{U^\star}$ the result of $DL_{U^\star}.\READ()$. By \textbf{READ Validity} $(i, \PROVEtrace(x)) \in R^{U^\star}$ implie that there exist a valid  $DL_{U^\star}.\PROVE^{(i)}(x)$. The for loop in the $\BFTPROVE(x)$ implementation return true iff there at least one valid $DL_{U}.\PROVE^{(i)}(x)$ for any $U \in \mathcal{U}$.
     
     Hence because there exist a $U^\star$ such that $DL_{U^\star}.\PROVE^{(i)}(x)$, there exist a valid $\BFTPROVE^{(i)}(x)$.
     
      $(i, \PROVEtrace(x)) \in R \implies \exists \BFTPROVE^{(i)}(x)$
-
-    \paragraph{READ Anti-Flickering.}
-    
-    \paragraph{READ Safety.}
-
 \end{proof}
 
-
+\begin{lemma}[READ Anti-Flickering]
-\subsection{t-BFT-DL $\Rightarrow$ t-BFT-GE}
+    Let $op_1, op_2$ two $\BFTREAD()$ operations that returns respectively $R_1, R_2$. Iff $op_1 \prec op_2$ then $R_2 \subseteq R_1$. Otherwise $R_1 \subseteq R_2$.
-
-\begin{lemma}
-    For any fixed value $r \in S$, multiple BFT-DenyList Object can be used to implement a BFT-Group Election Object.
 \end{lemma}
 
 \begin{proof}
-    \begin{algorithmic}
+    Let $R_1, R_2$ respectively the output of two $\BFTREAD()$ operations $op_1, op_2$ such that $op_1 \prec op_2$.
-        \State $Y[i]$ \Comment{Is a set of $n$ $\BFTDL$ with $\Pi_M = \Pi_V = \Pi$}
+    By the implementation of $\BFTREAD$, $R_k = \bigcup_{U \in \mathcal{U}} R_k^U$ where $R_k^U$ is the result of $DL_U.\READ()$ during $op_k$.
 
-        \vspace{1em}
+    Because $op_1 \prec op_2$ for any $U \in \mathcal{U}$, the $DL_U.\READ()$ induced by $op_1$ happen before the $DL_U.\READ()$ induced by $op_2$. Hence we have for all $U, R_2^U \subseteq R_1^U$.
+    Therefore 
+    \[
+    \bigcup_U R_2^U \subseteq \bigcup_U R_1^U \implies
+    R_2 \subseteq R_1
+    \]
+\end{proof}
 
-        \Function{BFTVOTE}{j, r}
+\begin{lemma}[READ Safety]
+    Let $op_1, op_2$ respectively a valid $\BFTPROVE(x)$ operation submited by the process $p_i$ and a $\BFTREAD()$ operation submited by any correct process such that $op_1 \prec op_2$. Let $R$ the result of $op_2$ then $R \ni (i, \PROVEtrace(x))$
+\end{lemma}
 
-        \EndFunction
+\begin{proof}
-        \vspace{1em}
+    Let $op_1 = \BFTPROVE^{(i)}(x)$ be a valid operation by a correct process $p_i$ and $op_2 = \BFTREAD()$ be any $\BFTREAD()$ operation such that $op_1 \prec op_2$ in $\Seq$.
+    By BFT-PROVE Validity, there exist at most $t$ distinct processes in $M$ that invoked a valid $\BFTAPPEND(x)$ before $op_1$ in $\Seq$. Let $A\subseteq M$ denote that set, with $|A|\le t$.
 
-        \Function{BFTCOMMIT}{r}
+    There exists $U^\star\in\mathcal{U}$ such that $A\cap U^\star=\emptyset$. For any $j\in A$, we have $j\notin U^\star$, so $\BFTAPPEND^{(j)}(x)$ does \emph{not} call $DL_{U^\star}.\APPEND(x)$. Hence no valid $DL_{U^\star}.\APPEND(x)$ appears before the induced $DL_{U^\star}.\PROVE(x)$ of $op_1$. Since also $i\in \Pi_V(DL_{U^\star})$, by \textbf{PROVE Validity} of $\DL$ the induced $DL_{U^\star}.\PROVE^{(i)}(x)$ is valid.
-        \EndFunction
+
-        \vspace{1em}
+    Now, because $op_1 \prec op_2$ in $\Seq$, the induced $DL_{U^\star}.\PROVE^{(i)}(x)$ appears before the induced $DL_{U^\star}.\READ()$ of $op_2$ in $\Seq_{U^\star}$. By \textbf{READ Safety} of $\DL$, the result $R^{U^\star}$ of the induced $DL_{U^\star}.\READ()$ contains $(i, \PROVEtrace(x))$.
-        \Function{BFTRESULT}{r}
+
-            \State $Z \gets \emptyset$
+    Finally, by the implementation of $\BFTREAD()$, we have $R = \bigcup_{U \in \mathcal{U}} R^U$, so $(i, \PROVEtrace(x)) \in R$.
-            \For{\textbf{each } $j \in \Pi$}
+\end{proof}
-                \If{$|\{(\_, \PROVEtrace(\_, r)) \in Y[j].\BFTREAD(r)\}| \geq n-f$}
+
-                    \State $P \gets \BFTREAD()$
+\begin{theorem}
-                    \State \Return $\{j : (j, \PROVEtrace), \}$
+    For any fixed value $t$ such that $3t < |M|$, multiple DenyList Object can be used to implement a t-Byzantine Fault Tolerant DenyList Object.
-                \EndIf
+\end{theorem}
-            \EndFor
+
-        \EndFunction
+\begin{proof}
-        \vspace{1em}
+    Follows directly from the previous lemmas.
-    \end{algorithmic}
 \end{proof}
 
 \subsection{Algorithm}
@@ -182,9 +197,9 @@ Each process $p_i$ maintains the following local variables:
   \State $\received \gets \emptyset$
   \State $\delivered \gets \emptyset$
   \State $\prop[r][j] \gets \bot, \forall r, j$
-%   \State $X_r \gets \bot, \forall r$
   \State $W_r \gets \bot, \forall r$
   \State $\resolved[r] \gets \bot, \forall r$
+  \State $Y[j]$ \Comment{Set of $n$ \BFTDL{}}
 \end{algorithmic}
 
 \renewcommand{\algletter}{A}
@@ -192,15 +207,16 @@ Each process $p_i$ maintains the following local variables:
     \caption{ABroadcast$(m)$}
     \begin{algorithmic}[1]
         \Function{ABroadcast}{$m$}
-            \State $r \gets \current$
+            % \State $r \gets \current$
-            \State $S \gets (\received \cup \{m\}$)
+            \State $S \gets (\received \cup \{m\})$
             \For{\textbf{each}\ $r \in \{\current, \current +1, \dots\}$}
                 \State $\RBcast(i, PROP, S, r)$
-                \State \textbf{wait} until $|W_r| \geq n - f$ where $W_r = \BFTRESULT[r]$
+                \State \textbf{wait} until $|W_r| \geq n - f$ where $W_r = \bigcup_{j \in \Pi} Y[j].\BFTREAD()$
-                \State $\BFTCOMMIT(r)$
+                \State $\forall j \in W_r, Y[j].\BFTAPPEND(r)$
+                \State $\RBcast(i, COMMIT, r)$
                 \State \textbf{wait} until $|\resolved[r]| \geq n - f$
-                \State $W_r \gets \BFTRESULT[r]$
+                \State $W_r \gets \bigcup_{j \in \Pi} Y[j].\BFTREAD()$
-                \If{$i \in W_r \vee (\exists j, r': j \in W_r \wedge \prop[r'][j] \ni m)$}
+                \If{$i \in W_r \vee (\exists j, r': j \in W_{r'} \wedge \prop[r'][j] \ni m)$}
                     \State \textbf{break}
                 \EndIf
             \EndFor
@@ -217,7 +233,7 @@ Each process $p_i$ maintains the following local variables:
             \If{$|\resolved[r]| < n - f$}
                 \State \Return $\bot$
             \EndIf
-            \State $W_r \gets \BFTRESULT[r]$
+            \State $W_r \gets \bigcup_{j \in \Pi} Y[j].\BFTREAD()$
             \If{$\exists j \in W_r,\ \prop[r][j] = \bot$} 
                 \State \Return $\bot$
             \EndIf
@@ -239,13 +255,31 @@ Each process $p_i$ maintains the following local variables:
         \Function{Rreceived}{j, PROP, S, r}
             \State $\received \gets \received \cup \{S\}$
             \State $\prop[r][j] \gets S$
-            \State $\BFTVOTE(j, r)$
+            \State $Y[j].\BFTPROVE(r)$
         \EndFunction
 
         \vspace{1em}
         
         \Function{Rreceived}{j, COMMIT, r}
-            \State $\received[r] \cup \{j\}$
+            \State $\resolved[r] \cup \{j\}$
         \EndFunction
     \end{algorithmic}
 \end{algorithm}
+
+\begin{definition}[BFT Closed round for $i$]
+    Given $Seq^{(i)}$ the linearization of the $\BFTDL$ $Y[i]$, a round $r \in \mathcal{R}$ is \emph{closed} in $\Seq$ iff there exist at least $n - f$ distinct processes $j \in \Pi$ such that $\BFTAPPEND^{(j)}(r)$ appears in $\Seq^{(i)}$.
+\end{definition}
+
+\begin{definition}[BFT Closed round]
+    A round $r \in \mathcal{R}$ is \emph{closed} iff for all process $p_i$, $r$ is closed in $\Seq^{(i)}$.
+\end{definition}
+
+\subsection{Proof of correctness}
+
+\begin{lemma}[BFT Stable round closure]
+    % If a round $r$ is closed by a correct process, 
+\end{lemma}
+
+\begin{theorem}
+    The algorithm implements a BFT Atomic Reliable Broadcast.
+\end{theorem}