amaury_joly/bwconsistency
1
0
Fork 0
Code Issues 5 Pull Requests Packages Projects 3 Releases Wiki Activity

update

Browse Source
This commit is contained in:
Amaury JOLY
2026-01-07 20:16:22 +01:00
parent e89e0e8d2a
commit 106bc70056
2 changed files with 45 additions and 106 deletions
Download Patch File Download Diff File Expand all files Collapse all files

151
Recherche/BFT-ARBover/6_BFT_ARB/index.tex
View File

@@ -72,143 +72,82 @@ There are three operations: $\BFTVOTE(j, r)$, $\BFTCOMMIT(r)$, and $\BFTRESULT(r
\begin{proof}
Fix $t < |M|$. Let
\[
\mathcal{T} \triangleq \{\, T \subseteq M \mid |T| = t \,\}.
\mathcal{T} = \{\, T \subseteq M \mid |T| = t \,\}.
\]
For each $T \in \mathcal{T}$, we instantiate one DenyList object $DL_T$ whose authorization sets are
\[
\Pi_M(DL_T) \triangleq S_T \triangleq M \setminus T
\Pi_M(DL_T) = S_T = M \setminus T
\qquad\text{and}\qquad
\Pi_V(DL_T) \triangleq V.
\Pi_V(DL_T) = V.
\]
Let
\[
K \triangleq \{\, DL_T \mid T \in \mathcal{T} \,\},
K = \{\, DL_T \mid T \in \mathcal{T} \,\},
\qquad\text{so that}\qquad
|K| = \binom{|M|}{t}.
\]
% The system consists of a set of $\Pi$ processes, we define a subset of processes $M \subseteq \Pi$ which are authorized to invoke the $\BFTAPPEND$ operation and a subset of processes $V \subseteq \Pi$ which are authorized to invoke the $\BFTPROVE$ operation.
% There exist $K$ a set of $\binom{|M|}{t+1}$ DenyList objects denoted by $DL_1, DL_2, \dots, DL_{|K|}$ such that each DenyList $DL_k$ is associated with a unique subset of processes $S_k \subseteq M$ of size $t+1$.
\begin{algorithmic}
\State $K \gets \{DL_1, DL_2, \dots, DL_{|K|}\}$ \Comment{Set of DenyList objects}
\vspace{1em}
\State $K \gets \{DL_T : T \subseteq M, |T|=t\}$
\Function{BFTAPPEND}{x}
\If{$p_i \not\in \Pi_M$}
\If{$p_i \notin M$}
\State \Return \textbf{false}
\EndIf
\For{\textbf{each } $DL_k \in K$ \textbf{such that} $p_i \in S_k$}
\State $DL_k.\APPEND(x)$
\For{\textbf{each } $DL_T \in K$}
\State $DL_T.\APPEND(x)$
\EndFor
\State \Return \textbf{true}
\EndFunction
\vspace{1em}
\Function{BFTPROVE}{x}
\For{\textbf{each } $DL_k \in K$}
\State $state \gets DL_k.\PROVE(x) || state$
\If{$p_i \notin V$}
\State \Return $\bot$
\EndIf
\State $state \gets false$
\For{\textbf{each } $DL_T \in K$}
\State $state \gets state \textbf{ OR } DL_T.\PROVE(x)$
\EndFor
\State \Return $state$
\EndFunction
\vspace{1em}
\Function{BFTREAD}{}
\State $results \gets \emptyset$
\For{\textbf{each } $DL_k \in K$}
\State $res \gets DL_k.\READ()$
\State $results \gets results \cup res$
\For{\textbf{each } $DL_T \in K$}
\State $results \gets results \cup DL_T.\READ()$
\EndFor
\State \Return $results$
\EndFunction
\vspace{1em}
\end{algorithmic}
\end{algorithmic}
\paragraph{BFT-APPEND Validity.} Let $A\subseteq M$ be the set of distinct issuers that invoked a valid $\BFTAPPEND(x)$ Suppose by contradiction that there exists $T\in\mathcal{T}$ with $A\cap S_T=\emptyset$. Since $S_T=M\setminus T$, this implies $A\subseteq T$, hence $|A|\le |T|=t$, contradicting $|A|\ge t+1$.
\textbf{APPEND Validity.} A process $p_i$ not in $\Pi_M$ who invokes $\BFTAPPEND(x)$ will never be able to submit a valid $\APPEND(x)$ to any DenyList $DL_k$ since each DenyList $DL_k$ is associated with a unique subset of processes $S_k \subseteq M$. Otherwise, if $p_i \in \Pi_M$, then any invocation of $\BFTAPPEND(x)$ are valid.
\textbf{PROVE Validity.}
Let set $op$ a particular invocation of $\BFTPROVE(x)$ by $p_i$.
\begin{itemize}
\item Case 1: If $p_i \not\in \Pi_V$, then $op$ is invalid since $p_i$ is not authorized to invoke $\PROVE$ operation in any DL.
\item Case 2: If at least $t+1$ valid $\BFTAPPEND(x)$ submitted by $t+1$ distincts processus appears before $op$ in $\Seq$, then for any set $S_k$ there is at least one process in $S_k$ who submitted a valid $\APPEND(x)$ before $op$. Therefore, $op$ will be invalid since all $DLs$ will be locked on the value $x$ by the PROVE Validity of DL Object.
\end{itemize}
Otherwise $op$ is always valid.
\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 a valid $\BFTAPPEND(x)$ before $op$ in $\Seq$.
\textbf{PROVE Anti-Flickering.}
Let $op=\BFTPROVE(x)$ be an invocation by a correct process $p_i \in \Pi_V$ that is \emph{invalid} in $\Seq$.
By the \textbf{PROVE Validity} of t-$\BFTDL$, this implies that there exist at least $t+1$ \emph{valid}
invocations of $\BFTAPPEND(x)$ by $t+1$ distinct processes that appear before $op$ in $\Seq$.
Let $A \subseteq \Pi_M$ be the set of these (distinct) issuers, with $|A|\ge t+1$.
Consider any DenyList object $DL_k \in K$, associated with a subset $S_k \subseteq M$ of size $|S_k|=t+1$.
Since $K$ contains \emph{all} $(t+1)$-subsets of $M$ and $|A|\ge t+1$, we have
\[
S_k \cap A \neq \emptyset.
\]
Let $p_j \in S_k \cap A$. By construction of $\BFTAPPEND$, the invocation $\BFTAPPEND^{(j)}(x)$ triggers
the operation $DL_k.\APPEND(x)$ (because $p_j \in S_k$), and since $\BFTAPPEND^{(j)}(x) \prec op$ in $\Seq$,
this $DL_k.\APPEND(x)$ appears before the operation $DL_k.\PROVE(x)$ induced by $op$ in the linearization $\Seq_k$
of $DL_k$.
Therefore, in $\Seq_k$ there exists a valid $\APPEND(x)$ before the invocation $DL_k.\PROVE(x)$ induced by $op$.
By the \textbf{PROVE Validity} property of $\DL$, this implies that the invocation $DL_k.\PROVE(x)$ induced by $op$
is \emph{invalid}. Since this holds for every $k \in K$, all component $\PROVE$ operations of $op$ are invalid.
Now consider any invocation $op'=\BFTPROVE(x)$ that appears after $op$ in $\Seq$.
For each $k$, the invocation of $DL_k.\PROVE(x)$ induced by $op'$ appears after the one induced by $op$ in $\Seq_k$.
By the \textbf{PROVE Anti-Flickering} property of $\DL$, once a $\PROVE(x)$ is invalid in $\Seq_k$,
all subsequent $\PROVE(x)$ in $\Seq_k$ are invalid. Hence, for all $k$, the $\PROVE(x)$ induced by $op'$ is invalid,
which implies that $op'$ is invalid at the t-$\BFTDL$ level.
This proves the \textbf{PROVE Anti-Flickering} property for the construction.
\medskip
\textbf{READ Validity.}
Let $op=\BFTREAD()$ be an invocation by a correct process $p$.
The algorithm executes, for each $DL_k \in K$, a read $res_k \gets DL_k.\READ()$ and returns
\[
results \;=\; \bigcup_{k\in K} res_k.
\]
By \textbf{READ Validity} of each $\DL$, $res_k$ contains exactly the valid invocations of $\PROVE$
that appear before $DL_k.\READ()$ in $\Seq_k$, together with the identities of their issuers.
We show that $results$ is exactly the set of valid invocations of $\BFTPROVE$ that appear before $op$ in $\Seq$.
\smallskip
\emph{(i) Soundness (no false positives).}
Take any entry $(j,\PROVE(x)) \in results$. Then $(j,\PROVE(x)) \in res_k$ for some $k$,
hence the invocation $DL_k.\PROVE(x)$ by $p_j$ is valid and appears before $DL_k.\READ()$ in $\Seq_k$.
In particular, there is no valid $DL_k.\APPEND(x)$ before that $DL_k.\PROVE(x)$ in $\Seq_k$
(otherwise $DL_k.\PROVE(x)$ would be invalid by \textbf{PROVE Validity} of $\DL$).
Assume by contradiction that the corresponding invocation $\BFTPROVE^{(j)}(x)$ is invalid in $\Seq$.
Then, by \textbf{PROVE Validity} of t-$\BFTDL$, there exist at least $t+1$ valid invocations of $\BFTAPPEND(x)$
by $t+1$ distinct processes before $\BFTPROVE^{(j)}(x)$ in $\Seq$.
As in the argument used for \textbf{PROVE Anti-Flickering}, this implies that for every $DL_{k'} \in K$,
there exists a valid $DL_{k'}.\APPEND(x)$ before the $DL_{k'}.\PROVE(x)$ induced by $\BFTPROVE^{(j)}(x)$.
Therefore the induced $DL_k.\PROVE(x)$ would be invalid, contradicting $(j,\PROVE(x)) \in res_k$.
Hence $\BFTPROVE^{(j)}(x)$ is valid and appears before $op$ in $\Seq$.
\noindent\textbf{Case (i): $i\notin V$.}
For every $T\in\mathcal{T}$, we configured $\Pi_V(DL_T)=V$, hence the induced operation $DL_T.\PROVE(x)$ is invalid by \textbf{PROVE Validity} of $\DL$. Therefore $op$ is invalid.
\smallskip
\emph{(ii) Completeness (no omissions).}
Consider a valid invocation $\BFTPROVE^{(j)}(x)$ that appears before $op=\BFTREAD()$ in $\Seq$.
Let $A$ be the set of distinct processes that invoked a valid $\BFTAPPEND(x)$ before $\BFTPROVE^{(j)}(x)$ in $\Seq$.
Since $\BFTPROVE^{(j)}(x)$ is valid in t-$\BFTDL$, we have $|A| \le t$.
Because $K$ contains all subsets $S_k \subseteq M$ of size $t+1$ and $t<|M|$,
there exists some $S_k$ such that
\[
S_k \cap A = \emptyset.
\]
For this $DL_k$, none of the $\BFTAPPEND(x)$ invocations issued by processes in $A$
triggers $DL_k.\APPEND(x)$ (since $\BFTAPPEND$ calls $DL_k.\APPEND(x)$ only for $k$ with issuer in $S_k$).
Thus, there is no valid $DL_k.\APPEND(x)$ before the invocation $DL_k.\PROVE(x)$ induced by $\BFTPROVE^{(j)}(x)$.
By \textbf{PROVE Validity} of $\DL$, the induced $DL_k.\PROVE(x)$ is valid.
Moreover, since $\BFTPROVE^{(j)}(x) \prec \BFTREAD()$ in $\Seq$, this induced $\PROVE(x)$ appears before
$DL_k.\READ()$ in $\Seq_k$, and therefore it is included in $res_k$.
Hence $(j,\PROVE(x)) \in results$.
Combining (i) and (ii), $results$ contains exactly the valid invocations of $\BFTPROVE$
that appear before $op$ in $\Seq$, together with the identities of their issuers.
This proves the \textbf{READ Validity} property.
\noindent\textbf{Case (ii): $|A|\ge t+1$ and $i\in V$.} Fix any $T\in\mathcal{T}$. By BFT-APPEND Validity, $A\cap S_T\neq\emptyset$. Pick $j\in A\cap S_T$. Since $j\in S_T$, the call $\BFTAPPEND^{(j)}(x)$ triggers $DL_T.\APPEND(x)$, and because $\BFTAPPEND^{(j)}(x)\prec op$ in $\Seq$, this induces a valid $DL_T.\APPEND(x)$ that appears before the induced $DL_T.\PROVE(x)$. By \textbf{PROVE Validity} of $\DL$, the induced $DL_T.\PROVE(x)$ is invalid. As this holds for every $T\in\mathcal{T}$, there is \emph{no} component $DL_T$ where $\PROVE(x)$ is valid, so $op$ is invalid.
\smallskip
\noindent\textbf{Case (iii): $|A|\le t$ and $i\in V$.}
By BFT-APPEND Validity, there exists $T^\star\in\mathcal{T}$ such that $A\cap S_{T^\star}=\emptyset$, i.e., $A\subseteq T^\star$. For any $j\in A$, we have $j\notin S_{T^\star}$, so $\BFTAPPEND^{(j)}(x)$ does \emph{not} call $DL_{T^\star}.\APPEND(x)$. Hence no valid $DL_{T^\star}.\APPEND(x)$ appears before the induced $DL_{T^\star}.\PROVE(x)$. Since also $i\in V=\Pi_V(DL_{T^\star})$, by \textbf{PROVE Validity} of $\DL$ the induced $DL_{T^\star}.\PROVE(x)$ is valid. Therefore, there exists a component with a valid $\PROVE(x)$, so by the lifting convention $op$ is valid.
\smallskip
Combining the cases yields the claimed characterization of invalidity.
\paragraph{BFT-PROVE Anti-Flickering.} Let $op=\BFTPROVE(x)$ be an invocation by a correct process $p_i\in V$ that is \emph{invalid} in $\Seq$.
By BFT-PROVE Validity, since $i\in V$, 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 $T\in\mathcal{T}$ and $DL_T$ with $\Pi_M(DL_T)=S_T=M\setminus T$. By BFT-APPEND Validity, we have $A\cap S_T\neq\emptyset$. Pick $j\in A\cap S_T$. Since $j\in S_T$, the call $\BFTAPPEND^{(j)}(x)$ triggers a call $DL_T.\APPEND(x)$. Moreover, because $\BFTAPPEND^{(j)}(x)\prec op$ in $\Seq$, the induced $DL_T.\APPEND(x)$ appears before the induced $DL_T.\PROVE(x)$ of $op$ in the projection $\Seq_T$.
Hence, in $\Seq_T$, there exists a \emph{valid} $DL_T.\APPEND(x)$ that appears before the $DL_T.\PROVE(x)$ induced by $op$. By \textbf{PROVE Validity} the base $\DL$ object, the induced $DL_T.\PROVE(x)$ is therefore \emph{invalid} in $\Seq_T$.
Now let $op'=\BFTPROVE(x)$ be any invocation such that $op\prec op'$ in $\Seq$. Fix again any $T\in\mathcal{T}$. Hence, the $DL_T.\PROVE(x)$ induced by $op'$ appears after the $DL_T.\PROVE(x)$ induced by $op$ in $\Seq_T$. Since the induced $DL_T.\PROVE(x)$ of $op$ is invalid, by \textbf{PROVE Anti-Flickering} of $\DL$, \emph{every} subsequent $DL_T.\PROVE(x)$ in $\Seq_T$ is invalid.
As this holds for every $T\in\mathcal{T}$, there is no component $DL_T$ in which the induced $\PROVE(x)$ of $op'$ is valid.
\end{proof}