partial-proof on BFT ARB

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

@@ -21,7 +21,7 @@ We denoted by $\PROVE^{(j)}(r)$ or $\APPEND^{(j)}(r)$ the operation $\PROVE(r)$
 \subsubsection{t-BFT-DL}
 
 We consider a t-Byzantine Fault Tolerant DenyList (t-$\BFTDL$) with the following properties.
-There are 3 operations : $\BFTPROVE(x), \BFTAPPEND(x), \BFTREAD(x)$ such that : 
+There are 3 operations : $\BFTPROVE(x), \BFTAPPEND(x), \BFTREAD(x)$ such that :
 
 \paragraph{Termination.} Every operation $\BFTAPPEND(x)$, $\BFTPROVE(x)$, and $\BFTREAD()$ invoked by a correct process always returns.
 
@@ -29,7 +29,7 @@ There are 3 operations : $\BFTPROVE(x), \BFTAPPEND(x), \BFTREAD(x)$ such that :
 
 \paragraph{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.
 
-\paragraph{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$. 
+\paragraph{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$.
 
 \paragraph{READ Anti-Flickering.} 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$.
 
@@ -54,20 +54,20 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au
 \]
 
 \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$} 
+            \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$
@@ -78,7 +78,7 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au
         \EndFunction
 
         \vspace{1em}
-    
+
         % \caption{\BFTREAD}
         \Function{$\BFTREAD$}{$\bot$}
             \State $results \gets \emptyset$
@@ -90,7 +90,7 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au
     \end{algorithm}
 \end{algorithmic}
 
-\begin{lemma}[BFT-PROVE Validity]
+\begin{lemma}[BFT-PROVE Validity]\label{lem: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}
 
@@ -98,13 +98,13 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au
     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$.} 
+        \item \textbf{Case (i): $|A|\ge t+1$.}
         Fix any $U\in\mathcal{U}$. $A\cap U\neq\emptyset$. Pick $j\in A\cap U$. Since $j\in U$, the call $\BFTAPPEND^{(j)}(x)$ triggers $DL_U.\APPEND(x)$, and because $\BFTAPPEND^{(j)}(x)\prec op$ in $\Seq$, this induces a valid $DL_U.\APPEND(x)$ that appears before the induced $DL_U.\PROVE(x)$ by $p_i$. By \textbf{PROVE Validity} of $\DL$, the induced $DL_U.\PROVE(x)$ is invalid. As this holds for every $U\in\mathcal{U}$, there is \emph{no} component $DL_U$ where $\PROVE(x)$ is valid, so the field $state$ at line DL9 is never becoming true, and $op$ return false.
-        
+
         \item \textbf{Case (ii): $|A|\le t$.}
         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)$. Since also $i\in \Pi_V(DL_{U^\star})$, by \textbf{PROVE Validity} of $\DL$ the induced $DL_{U^\star}.\PROVE(x)$ is valid. Therefore, there exists a component with a valid $\PROVE(x)$, so $op$ is valid.
     \end{itemize}
-        
+
     \smallskip
     Combining the cases yields the claimed characterization of invalidity.
 \end{proof}
@@ -126,19 +126,19 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au
     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}
 
-\begin{lemma}[READ Liveness]
+\begin{lemma}[BFT-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$. 
+    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)$
 \end{proof}
 
-\begin{lemma}[READ Anti-Flickering]
+\begin{lemma}[BFT-READ Anti-Flickering]
     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$.
 \end{lemma}
 
@@ -147,14 +147,14 @@ For each $U \in \mathcal{U}$, we instantiate one DenyList object $DL_U$ whose au
     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$.
 
     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 
+    Therefore
     \[
     \bigcup_U R_2^U \subseteq \bigcup_U R_1^U \implies
     R_2 \subseteq R_1
     \]
 \end{proof}
 
-\begin{lemma}[READ Safety]
+\begin{lemma}[BFT-READ Safety]\label{lem:bft-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}
 
@@ -191,9 +191,9 @@ Each process $p_i$ maintains the following local variables:
   \State $Y[j]$ \Comment{Set of $n$ \BFTDL{}}
 \end{algorithmic}
 
-\renewcommand{\algletter}{D}
+\renewcommand{\algletter}{A}
 \begin{algorithm}[H]
-    \caption{ABroadcast$(m)$}
+    % \caption{ABroadcast$(m)$}
     \begin{algorithmic}[1]
         \Function{ABroadcast}{$m$}
             % \State $r \gets \current$
@@ -201,13 +201,13 @@ Each process $p_i$ maintains the following local variables:
             \For{\textbf{each}\ $r \in \{\current, \current +1, \dots\}$}
                 \Statex \Comment{PROPOSAL PHASE}
                 \State $\RBcast(i, \texttt{PROP}, S, r)$
-                \State \textbf{wait} until $|W_r| \geq n - f$ where $W_r \gets \{j: (j, \PROVEtrace(x)) \in \bigcup_{k \in \Pi} Y[k].\BFTREAD()\}$
+                \State \textbf{wait} until $|W_r| \geq n - f$ where $W_r \gets \{j: (j, \PROVEtrace(r)) \in \bigcup_{k \in \Pi} Y[k].\BFTREAD()\}$
                 \Statex \Comment{COMMIT PHASE}
                 \State \textbf{for each} $j \in W_r$ \textbf{do} $Y[j].\BFTAPPEND(r)$
                 \State $\RBcast(i, \texttt{COMMIT}, r)$
                 \State \textbf{wait} until $|\resolved[r]| \geq n - f$
                 \Statex \Comment{X PHASE}
-                \State $W_r \gets \{j: (j, \PROVEtrace(x)) \in \bigcup_{k \in \Pi} Y[k].\BFTREAD()\}$
+                \State $W_r \gets \{j: (j, \PROVEtrace(r)) \in \bigcup_{k \in \Pi} Y[k].\BFTREAD()\}$
                 \If{$\exists r' \in \mathcal{R}, j \in W_{r'} : m \in \prop[r'][j]$} \Comment{any process $j$ submited $m$ in any round $r'$}
                     \State \textbf{break}
                 \EndIf
@@ -216,17 +216,17 @@ Each process $p_i$ maintains the following local variables:
     \end{algorithmic}
 \end{algorithm}
 
-\renewcommand{\algletter}{C}
+\renewcommand{\algletter}{B}
 \begin{algorithm}[H]
-    \caption{ADeliver$(m)$}
+    % \caption*{ADeliver$(m)$}
     \begin{algorithmic}[1]
         \Function{ADeliver}{m}
             \State $r \gets \current$
             \If{$|\resolved[r]| < n - f$}
                 \State \Return $\bot$
             \EndIf
-            \State $W_r \gets \{j: (j, \PROVEtrace(x)) \in \bigcup_{k \in \Pi} Y[k].\BFTREAD()\}$
+            \State $W_r \gets \{j: (j, \PROVEtrace(r)) \in \bigcup_{k \in \Pi} Y[k].\BFTREAD()\}$
-            \If{$\exists j \in W_r,\ \prop[r][j] = \bot$} 
+            \If{$\exists j \in W_r,\ \prop[r][j] = \bot$}
                 \State \Return $\bot$
             \EndIf
             \State $M_r \gets \bigcup_{j \in W_r} \prop[r][j]$
@@ -240,9 +240,9 @@ Each process $p_i$ maintains the following local variables:
     \end{algorithmic}
 \end{algorithm}
 
-\renewcommand{\algletter}{E}
+\renewcommand{\algletter}{C}
 \begin{algorithm}[H]
-    \caption{RB handlers}
+    % \caption*{RB handlers}
     \begin{algorithmic}[1]
         \Upon{$Rdeliver(j, \texttt{PROP}, S, r)$}
             \State $\received \gets \received \cup \{S\}$
@@ -251,7 +251,7 @@ Each process $p_i$ maintains the following local variables:
         \EndUpon
 
         \vspace{1em}
-        
+
         \Upon{$Rdeliver(j, \texttt{COMMIT}, r)}$
             \State $\resolved[r] \gets \resolved[r] \cup \{j\}$
         \EndUpon
@@ -259,19 +259,86 @@ Each process $p_i$ maintains the following local variables:
 \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)}$.
+    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)}$. Let call $\BFTAPPEND(r)^\star$ the $(n-f)^{th}$ $\BFTAPPEND(r)$.
 \end{definition}
 
-\begin{definition}[BFT Closed round]
+\begin{definition}[BFT Closed round]\label{def: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]
+\begin{lemma}[BFT Stable round closure]\label{lem:bft-stable-round-closure}
-    % If a round $r$ is closed by a correct process, 
+    If a round $r$ is closed, no more $\BFTPROVE(r)$ can be valid and thus linearized. In other words, once $\BFTAPPEND(r)^\star$ is linearized, no more process can make a proof on round $r$, and the set of valid proofs for round $r$ is fixed. Therefore $\Winners_r$ is fixed.
 \end{lemma}
 
+\begin{proof}
+    By definition $r$ closed means that for all process $p_i$, there exist at least $n - f$ distinct processes $j \in \Pi$ such that $\BFTAPPEND^{(j)}(r)$ appears in $\Seq^{(i)}$. By BFT-PROVE Validity, any subsequent $\BFTPROVE(r)$ is invalid because at least $n - f$ processes already invoked a valid $\BFTAPPEND(r)$ before it. Thus no new valid $\BFTPROVE(r)$ can be linearized after $\BFTAPPEND(r)^\star$. Hence the set of valid proofs for round $r$ is fixed, and so is $\Winners_r$.
+\end{proof}
+
+\begin{lemma}[BFT $W_r$ as grow only set]\label{lem:bft-wr-grow-only}
+    For any correct process $p_i$. If $p_i$ computes $W_r$ at two different times $t_1$ and $t_2$ with $t_1 < t_2$, then $W_r^{t_1} \subseteq W_r^{t_2}$.
+\end{lemma}
+
+\begin{proof}
+    By the implementation, $W_r$ is computed exclusively from the results of $\{j: (j, \PROVEtrace(r)) \in \bigcup_{k \in \Pi} Y[k].\BFTREAD()\}$.
+
+    We know by BFT-READ Anti-Flickering that for any two $\BFTREAD()$ operations $op_1, op_2$ such that $op_1 \prec op_2$, the result of $op_2$ is included in the result of $op_1$. Therefore, if $p_i$ computes $W_r$ at two different times $t_1$ and $t_2$ with $t_1 < t_2$, then $W_r^{t_1} \subseteq W_r^{t_2}$.
+\end{proof}
+
+\begin{lemma}[BFT well defined winners]\label{lem:bft-well-defined-winners}
+    For any closed round $r$, if a correct process $p_i$ compute $W_r$, then $W_r = \Winners_r$ with $|W_r| \geq n - f$.
+\end{lemma}
+
+\begin{proof}
+    By \Cref{lem:bft-read-safety}, any correct process $p_i$ computing $W_r$ after round $r$ is closed includes all valid $\BFTPROVE(r)$ in its computation of $W_r$. Therefore $W_r = \Winners_r$.
+
+    By \Cref{def:bft-closed-round}, at least $n - f$ distinct processes invoked a valid $\BFTAPPEND(r)$ before $\BFTAPPEND(r)^\star$. By the implementation in algorithm D, if a process correct $j$ invoked a valid $\BFTAPPEND(r)$, thats means that he observed at least $n - f$ valid $\BFTPROVE(r)$ submitted by distinct processes. By \Cref{lem:bft-wr-grow-only}, once $p_j$ observed $n - f$ valid $\BFTPROVE(r)$, any correct process computing $W_r$ will eventually observe at least these $n - f$ valid $\BFTPROVE(r)$. By \Cref{lem:bft-stable-round-closure}, no more valid $\BFTPROVE(r)$ can be linearized after round $r$ is closed, so any correct process computing the same fixed set $W_r$ of at least $n - f$ distinct processes.
+\end{proof}
+
+\begin{lemma}[BFT Non-empty winners proposal]\label{lem:bft-non-empty-winners-proposal}
+    For every process $p_i$ such as $i \in W_r$, eventually $\prop[r][i] \neq \bot$.
+\end{lemma}
+
+\begin{proof}
+    By the implementation, if $i \in W_r$, then $(i, \PROVEtrace(r))$ is included in the result of at least one $\BFTREAD()$ operation. Hence there exist a valid $\BFTPROVE(r)$ operation.
+    By \Cref{lem:bft-prove-validity}, this implies that there exist at least $f + 1$ valid $\PROVE(r)$ operation invoked by processes. At least one of these processes is correct, say $p_j$. By the implementation, $p_j$ invoked $\BFTPROVE(r)$ after receiving a $Rdeliver(j, \texttt{PROP}, S, r)$ message from $p_i$. Therefore, by the reliable broadcast properties, the message will eventually be delivered to every correct process, hence eventually for any correct process $\prop[r][i] \neq \bot$.
+\end{proof}
+
+\begin{definition}[BFT Message invariant]\label{def:bft-message-invariant}
+    For any closed round $r$, for any correct process $p_i$, such that $\nexists j \in W_r : \prop[r][j] = \bot$, twe define the set
+    \[
+    \Messages_r = \bigcup_{j \in \Winners_r} \prop[r][j]
+    \]
+    as the unique set of messages proposed during round $r$.
+\end{definition}
+
+\begin{lemma}[BFT Proposal convergence]\label{lem:bft-proposal-convergence}
+    For any closed round $r$, for any correct process $p_i$, that define $M_r$ at line B10, we have $M_r = \Messages_r$.
+\end{lemma}
+
+\begin{proof}
+    By \Cref{lem:bft-well-defined-winners}, any correct process $p_i$ computing $W_r$ after round $r$ is closed has $W_r = \Winners_r$.
+    By \Cref{lem:bft-non-empty-winners-proposal}, for any correct process $p_i$, such as $i \in W_r$, eventually $\prop[r][i] \neq \bot$.
+
+    Therefore, eventually for any correct process $p_i$, at line B10 we have
+    \[
+    M_r = \bigcup_{j \in W_r} \prop[r][j] = \bigcup_{j \in \Winners_r} \prop[r][j] = \Messages_r
+    \]
+\end{proof}
+
+\begin{lemma}[BFT Inclusion]\label{proof:bft-inclusion}
+    If a correct process $p_i$ ABroadcasts a message $m$, then eventually any correct process $p_j$ ADelivers $m$.
+\end{lemma}
+
+\begin{proof}
+    Let $m$ be a message ABroadcast by a correct process $p_i$ and eventually exit the \texttt{ABroadcast} function at line A10.
+
+    By the implementation, if $p_i$ exits the \texttt{ABroadcast} function at line A10, then there exists a round $r'$ such that $m \in \prop[r'][j]$ for some $j \in W_{r'}$.
+
+    Since $p_i$ is correct, seeing that $m \in \prop[r'][j]$ for some $j \in W_{r'}$ implies that $p_i$ received a $Rdeliver(j, \texttt{PROP}, S, r')$ message from $p_j$ such that $m \in S$. And because $p_j$ is in $W_{r'}$, at least $n - f$ correct processes invoked a valid $Y[j].\BFTPROVE(r')$ before the round $r'$ were closed. By the reliable broadcast properties, the $Rdeliver(j, \texttt{PROP}, S, r')$ message will eventually be delivered to every correct process, hence eventually for any correct process $m \in \prop[r'][j]$ with $j \in W_{r'}$. Hence $m$ will eventually be included in the set $\Messages_{r'}$ defined in \Cref{def:bft-message-invariant} and thus eventually be ADelivered by any correct process.
+\end{proof}
+
 \begin{theorem}
     The algorithm implements a BFT Atomic Reliable Broadcast.
 \end{theorem}