
\subsection{Model extension}
We extend the crash model of Section 1 (same process universe, asynchronous setting, uniquely identifiable messages, and reliable point-to-point channels) with Byzantine faults and Byzantine-resilient dissemination primitives.

\paragraph{Failure threshold.} At most $t$ processes may be Byzantine, and we assume $n > 3t$, following standard asynchronous Byzantine assumptions~\cite{Bracha87}.

\paragraph{Additional communication primitive.} In addition to reliable point-to-point channels, processes use Reliable Broadcast ($\RB$) with operations $\RBcast(m)$ and $m=\rdeliver()$. We use Bracha's Byzantine RB specification~\cite{Bracha87}: for a fixed sender and broadcast instance, all correct processes that deliver, deliver the same payload, and Byzantine equivocation on that instance is prevented.

\paragraph{Byzantine behaviour}
A Byzantine process may deviate arbitrarily from the algorithm (malformed inputs, selective omission, collusion, inconsistent timing, etc.).

Byzantine processes are still constrained by the assumed primitives: they cannot violate the safety/liveness guarantees of $\DL$ and cannot break the Integrity, No-duplicates, and Validity guarantees of $\RB$.


\paragraph{Notation.} For any indice $k$ we defined by $\DL[k]$ as the $k$-th DenyList object. For a given $\DL[k]$ and any indice $x$ we defined by $\Pi_x^k$ a subset of $\Pi$. Still for a given $k$ we consider $\Pi_M^k \subseteq \Pi$ and $\Pi_V^k \subseteq \Pi$ two authorization subsets for $\DL[k]$. Indice $i \in \Pi$ refer to processes, and $p_i$ denotes the process with identifier $i$. Let $\mathcal{M}$ denote the universe of uniquely identifiable messages, with $m \in \mathcal{M}$. Let $\mathcal{R} \subseteq \mathbb{N}$ be the set of round identifiers; we write $r \in \mathcal{R}$ for a round. We use the precedence relation $\prec_k$ for the $\DL[k]$ linearization: $x \prec_k y$ means that operation $x$ appears strictly before $y$ in the linearized history of $\DL[k]$. For any finite set $A \subseteq \mathcal{M}$, \ordered$(A)$ returns a deterministic total order over $A$ (e.g., lexicographic order on $(\textit{senderId},\textit{messageId})$ or on message hashes).
For any operation $F \in O$,$F_i(...)$ denotes that the operation $F$ is invoked by process $p_i$, and by $F_i^k(...)$ the same operation invoked on the $\DL[k]$ object.

% ------------------------------------------------------------------------------
\subsection{Primitives}

\subsection{Reliable Broadcast (RB)}

\RB provides the following properties in this model (cf.~\cite{Bracha87}).
\begin{itemize}[leftmargin=*]
  \item \textbf{Integrity}: Every message received was previously sent. $\forall p_i:\ m = \rbreceived_i() \Rightarrow \exists p_j:\ \RBcast_j(m)$.
  \item \textbf{No-duplicates}: No message is received more than once at any process.
  \item \textbf{Validity}: If a correct process broadcasts $m$, every correct process eventually receives $m$.
\end{itemize}

\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()$ such that :

\paragraph{Termination.} Every operation $\BFTAPPEND(x)$, $\BFTPROVE(x)$, and $\BFTREAD()$ invoked by a correct process always returns.

\paragraph{PROVE Validity.} The invocation of $op = \BFTPROVE(x)$ by a correct process is valid iff there exist a set of correct process $C$ such that $\forall c \in C$, $c$ invoke $op_2 = \BFTAPPEND(x)$ with $op_2 \prec op_1$ and $|C| \leq t$

\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, 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$.

\paragraph{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, x)$

\subsection{DL $\Rightarrow$ t-BFT-DL}


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{algorithm}
    \caption{t-BFT-DL implementation using multiple DL objects}

    \Fn{$\BFTAPPEND(x)$}{
        \For{\textbf{each } $U \in \mathcal{U}$ st $i \in U$}{
            $DL_U.\APPEND(x)$\;
        }
    }

    \vspace{1em}

    \Fn{$\BFTPROVE(x)$}{
        $\state \gets false$\;
        \For{\textbf{each } $U \in \mathcal{U}$}{
            $\state \gets \state \textbf{ OR } DL_U.\PROVE(x)$\;\nllabel{code:prove-or}
        }
        \Return{$\state$}\;
    }

    \vspace{1em}

    \Fn{$\BFTREAD()$}{
        $\results \gets \emptyset$\;
        \For{\textbf{each } $U \in \mathcal{U}$}{
            $\results \gets \results \cup DL_U.\READ()$\;
        }
        \Return{$\results$}\;
    }
\end{algorithm}

\paragraph{Algorithm intuition.}
In the Byzantine setting, a process identifier $j$ is selected in $\winners[r]$ only when it accumulates at least $t+1$ proofs for round $r$ in $\validated(r)$. A process emits such a proof for $j$ only after receiving $j$'s $\texttt{PROP}$ payload (handler $\rdeliver(\texttt{PROP},\cdot)$). Therefore, if $j$ is a winner, at least one correct process has received $j$'s proposal. By RB agreement/validity, once one correct process receives that proposal for the instance, all correct processes eventually receive the same payload, so winner proposals eventually become available everywhere and can be merged consistently.

\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}

\begin{proof}
    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$.}
        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~\ref{code:prove-or} 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}

\begin{lemma}[BFT-PROVE Anti-Flickering]\label{lem: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$.

    Hence, in $\Seq_U$, there exists a \emph{valid} $DL_U.\APPEND(x)$ that appears before the $DL_U.\PROVE(x)$ induced by $op$. By \textbf{PROVE Validity} the base $\DL$ object, the induced $DL_U.\PROVE(x)$ is therefore \emph{invalid} in $\Seq_U$.

    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}

\begin{lemma}[BFT-READ Liveness]
    Let $op = \BFTREAD()$ invoke by a correct process such that $R$ is the result of $op$. For all $(i, 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, x) \in R$ implie that $\exists U^\star \in \mathcal{U}$ such that $(i, x) \in R^{U^\star}$ with $R^{U^\star}$ the result of $DL_{U^\star}.\READ()$. By \textbf{READ Validity} $(i, 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, x) \in R \implies \exists \BFTPROVE_i(x)$
\end{proof}

\begin{lemma}[BFT-READ Anti-Flickering]\label{lem: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}

\begin{proof}
    Let $R_1, R_2$ respectively the output of two $\BFTREAD()$ operations $op_1, op_2$ such that $op_1 \prec op_2$.
    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
    \[
    \bigcup_U R_2^U \subseteq \bigcup_U R_1^U \implies
    R_2 \subseteq R_1
    \]
\end{proof}

\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, x)$
\end{lemma}

\begin{proof}
    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$.

    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.

    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, x)$.

    Finally, by the implementation of $\BFTREAD()$, we have $R = \bigcup_{U \in \mathcal{U}} R^U$, so $(i, x) \in R$.
\end{proof}

\begin{theorem}
    For any fixed value $t$ such that $3t < |M|$, multiple DenyList Object can be used to implement a t-Byzantine Fault Tolerant DenyList Object.
\end{theorem}

\begin{proof}
    Follows directly from the previous lemmas.
\end{proof}

\subsection{Algorithm}

\begin{algorithm}[H]
    \caption{t-BFT ARB at process $p_i$}\label{alg:bft-arb}

    \SetKwBlock{LocalVars}{Local Variables:}{}
    \LocalVars{
        $\unordered \gets \emptyset$,
        $\ordered \gets \epsilon$,
        $\delivered \gets \epsilon$\;
        $\prop[r][j] \gets \bot, \forall j, r \in \Pi \times \mathbb{N}$\;
        $\done[r] \gets \emptyset, \forall r \in \mathbb{N}$\;
    }

    \vspace{0.3em}

    \For{$r = 1, 2, \ldots$}{\nllabel{alg:main-loop}
        \textbf{wait until} $\unordered \setminus \ordered \neq \emptyset$\;
        $S \gets \unordered \setminus \ordered$;
        $\RBcast(\texttt{PROP}, S, \langle i, r \rangle)$\;

        \textbf{wait until} $|\validated(r)| \geq n - t$\;\nllabel{alg:check-validated}

        \BlankLine

        \lForEach{$j \in \Pi$}{
            $\BFTAPPEND(\langle j, r\rangle)$\nllabel{alg:append}
        }

        \lForEach{$j \in \Pi$}{
            $\send(\texttt{DONE}, r)$ \textbf{ to } $p_j$
        }

        \BlankLine

        \textbf{wait until} $|\done[r]| \geq n - t$\;\nllabel{alg:check-done}
        \textbf{wait until} $\forall j \in \winners[r],\ \prop[r][j] \neq \bot$ \textbf{ with } $\winners[r] \gets \validated(r)$\;

        \BlankLine

        $M \gets \bigcup_{j \in \winners[r]} \prop[r][j]$\;\nllabel{code:Mcompute}
        $\ordered \gets \ordered \cdot \order(M)$\;
    }

    \vspace{0.3em}

    \Fn{\validated($r$)}{
        \Return{$\{j: |\{k: (k, r) \in \BFTREAD()\}| \geq t+1\}$}\;
    }

    \vspace{0.3em}

    \Upon{$\ABbroadcast(m)$}{
        $\unordered \gets \unordered \cup \{m\}$\;
    }

    \vspace{0.3em}

    \Upon{$\rdeliver(\texttt{PROP}, S, \langle j, r \rangle)$ from process $p_j$}{
        $\unordered \gets \unordered \cup S$;
        $\prop[r][j] \gets S$\;
        $\BFTPROVE(\langle j, r\rangle)$\;
    }

    \vspace{0.3em}

    \Upon{$\receive(\texttt{DONE}, r)$ from process $p_j$}{
        $\done[r] \gets \done[r] \cup \{j\}$\;
    }

    \vspace{0.3em}

    \Upon{$\ABdeliver()$}{
        \lIf{$\ordered \setminus \delivered = \emptyset$}{
            \Return{$\bot$}
        }
        let $m$ be the first message in $(\ordered \setminus \delivered)$\;
        $\delivered \gets \delivered \cdot \{m\}$\;
        \Return{$m$}
    }
    
\end{algorithm}

\paragraph{Algorithm intuition.}
The Byzantine-tolerant construction combines threshold evidence and RB agreement to make winner selection robust. A sender $j$ appears in $\validated(r)$ only when at least $t+1$ proofs for $\langle j,r\rangle$ are observed through $\BFTREAD()$, and by \Cref{lem:bft-prove-validity} this threshold means that $j$ cannot be certified without broad enough support from the system. Once a round is closed, the winner set becomes stable by \Cref{lem:winners-stability}, so correct processes stop diverging on who contributes to the round outcome. For each stable winner, the associated proposal payload is unique at correct receivers by \Cref{lem:bft-unique-proposal}, which prevents equivocation from creating distinct local values for the same winner identity. Consequently, when correct processes wait for all winner proposals and compute the union at line~\ref{code:Mcompute}, they obtain the same message set by \Cref{lem:message-content-invariance}. Progress is then ensured by \Cref{lem:bft-eventual-closure}, which guarantees that if new messages remain unordered, a new round eventually closes with at least $n-t$ winners. Finally, once rounds are commonly closed, appending $\order(M)$ at each round yields a common delivery sequence, exactly formalized by \Cref{lem:bft-total-order}.

% \textbf{Everything below has to be updated}

% \begin{definition}[BFT Closed round for $k$]
%     Given $Seq^{k}$ the linearization of the $\BFTDL$ $Y[k]$, 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^k$. Let call $\BFTAPPEND(r)^\star$ the $(n-f)^{th}$ $\BFTAPPEND(r)$.
% \end{definition}

% \begin{definition}[BFT Closed round]\label{def:bft-closed-round}
%     A round $r \in \mathcal{R}$ is \emph{closed} iff for all $\DL[k]$, $r$ is closed in $\Seq^k$.
% \end{definition}

% \subsection{Proof of correctness}

% \begin{remark}[BFT Stable round closure]\label{rem:bft-stable-round-closure}
%     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{remark}

% \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^k$. 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 Across rounds]\label{lem:bft-across-rounds}
%     For any $r, r'$ such that $r < r'$, if $r'$ is closed, $r$ is also closed.
% \end{lemma}

% \begin{proof}
%     Let $r \in \mathcal{R}$. By \cref{def:bft-closed-round}, if $r + 1$ is closed, then for all $\DL[k]$, $r + 1$ is closed in $\Seq^k$. By the implementation, a process can only invoke $\BFTAPPEND(r + 1)$ after observing at least $n - f$ valid $\BFTPROVE(r)$, which means that for all $\DL[k]$, $r$ is closed in $\Seq^k$. Hence by \cref{def:bft-closed-round}, $r$ is closed.

%     Because $r$ is monotonically increasing, we can reccursively apply the same argument to conclude that for any $r, r'$ such that $r < r'$, if $r'$ is closed, $r$ is also closed.
% \end{proof}

% \begin{lemma}[BFT Progress]\label{lem:bft_progress}
%     For any correct process $p_i$ such that
%     \[
%     \received \setminus (\delivered \cup (\cup_{r' < r} \cup_{j \in W[r'] \prop[r'][j]})) \neq \emptyset
%     \]
%     with $r$ the highest closed round in the $\DL$ linearization. Eventually $r+1$ will be closed.
% \end{lemma}

% \begin{lemma}[BFT Winners invariant]\label{lem:bft-winners-invariant}
%     For any closed round $r$, define
%     \[
%     \Winners_r = \{j: \BFTPROVE_j(r) \prec \BFTAPPEND^\star(r)\}
%     \]
%     called the unique set of winners of round $r$.
% \end{lemma}

% \begin{lemma}[BFT n-f lower-bounded Winners]
%     Let $r$ a closed round, $|W[r]| \geq n-f$.
% \end{lemma}

% \begin{remark}\label{rem:correct-in-winners}
%     Because we assume $n \geq 2f+ 1$, if $|W[r]| \geq n-f$ at least 1 correct have to be in $W[r]$ to progress.
% \end{remark}

% \begin{lemma}[BFT Winners must purpose]\label{lem:bft-winners-purpose}
%     Let $r$ a closed round, for all process $p_j$ such that $j \in W[r]$, $p_j$ must have executed $\RBcast(j, PROP, \_, r)$ and hence any correct will eventually set $\prop[r][j]$ to a non-$\bot$ value.
% \end{lemma}

% \begin{lemma}[BFT Messages Incariant]\label{lem:bft-messages-invariant}
%     For any closed round $r$ and any correct process $p_i$ such that $\forall j \in \Winners_r$: $\prop^{(i)}[r][j] \neq \bot$ define
%     \[
%         \Messages_r = \cup_{j \in \Winners_r} prop^{(i)}[r][j]
%     \]
%     as the set of messages proposed by the winners of round $r$
% \end{lemma}

% \begin{lemma}[BFT EVentual proposal closure]\label{lem:bft-eventual-proposal-closure}
%     If a correct process $p_i$ define $M$ at line~\ref{code:Mcompute}, then for every $j \in \Winners_r$, $\prop^{(i)}[r][j] \neq \bot$.
% \end{lemma}

% \begin{lemma}[BFT Unique proposal per sender per round]\label{lem:bft-unique-proposal}
%     For any round $r$ and any process $p_i$, if $p_i$ invokes two $\RBcast$ call for the same round, such that $\RBcast(i, PROP, S, r) \prec \RBcast(i, PROP, S', r)$. Then for any correct process $p_j$, $\prop^{(j)}[r][i] \in \{\bot, S\}$
% \end{lemma}







% \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}

\subsection{Correctness Lemmas}

\begin{definition}[Closed Round]
    A round $r \in \mathcal{R}$ is said to be \emph{closed} for a correct process $p_i$ if at the moment $p_i$ computes $\winners[r]$, it satisfies $|\{k : (k, r) \in \BFTREAD()\}| \geq n - t$.
\end{definition}

\begin{lemma}[Round Monotonicity]\label{lem:round-monotonicity}
    If a round $r$ is closed, then every round $r_1 < r$ is also closed.
\end{lemma}

\begin{proof}
    \textbf{Base:} $r = 0$. Suppose round $1$ is closed, the set $\{r' \in \mathcal{R}: r' < r\}$ is empty, so the claim holds.
    
    \textbf{Inductive step:} Let $r \geq 1$. Assume that the property holds for all rounds $r' < r$: whenever round $r'$ is closed, all rounds $r_2 < r'$ are also closed. We show that if round $r$ is closed, then all rounds $r_1 < r$ are closed.
    
    Suppose round $r$ is closed. This means at least one correct process $p_i$ has reached line \ref{alg:check-validated} and satisfied the condition $|\validated(r)| \geq n - t$. Consequently, $p_i$ has invoked $\BFTAPPEND(\langle j, r \rangle)$ for each $j \in \Pi$ at line \ref{alg:append}. Since these operations are invoked by a correct process, and they depend on valid proofs in the byzantine fault tolerant deny list, at least one of these operations must have succeeded in the DL object.
    
    Moreover, by the algorithm structure, a correct process can only reach the beginning of round $r$ after completing round $r-1$. In particular, process $p_i$ reaches line \ref{alg:main-loop} for round $r$ only after having completed round $r-1$, which requires the process to have observed at least $|\done[r-1]| \geq n - t$ (line \ref{alg:check-done} for round $r-1$). This condition can only be satisfied if round $r-1$ is closed: at least $n - t$ processes must have issued DONE messages, and since $n > 3f$, at least one of these is correct.
    
    Since $n - t > 2f + 1$, among the $n - t$ processes satisfying the condition for round $r-1$, at least one is correct. A correct process that issued a DONE message for round $r-1$ must have previously completed its execution of lines \ref{alg:append} for round $r-1$, which in turn required observing $|\validated(r-1)| \geq n - t$ from line \ref{alg:check-validated}. Thus, round $r-1$ is closed.
    
    Now, considering any round $r_1 < r-1$: by the inductive hypothesis applied to round $r-1$, since round $r-1$ is closed and $r_1 < r-1$, we have that $r_1$ is also closed.
    
    By strong induction, if round $r$ is closed, all rounds $r_1 < r$ are closed.
\end{proof}

\begin{lemma}[Uniqueness of Winners' Proposals]\label{lem:bft-unique-proposal}
    For any closed round $r$ and any process $p_j \in \winners[r]$, there exists a unique set $S_j \subseteq \mathcal{M}$ such that every correct process $p_i$ that has received a reliable delivery of a $\texttt{PROP}$ message from $p_j$ for round $r$ receives exactly this set $S_j$.
\end{lemma}

\begin{proof}
    Let $r$ be a closed round and $p_j \in \winners[r]$. Since $j \in \winners[r]$, it means that $(j, r) \in \BFTREAD()$, i.e., at least $t+1$ distinct processes have invoked a valid $\BFTPROVE(\langle j, r \rangle)$ before the round $r$ closed.
    
    By the algorithm, a correct process $p_i$ invokes $\BFTPROVE(\langle j, r \rangle)$ only upon receiving a reliable delivery of a $\texttt{PROP}$ message from $p_j$ for round $r$ at line \ref{alg:append}. Let $S_j^{(i)}$ denote the set received by $p_i$.
    
    Since at least $t+1$ distinct processes have performed a valid $\BFTPROVE(\langle j, r \rangle)$, and since $t < n/3$, at least one of these processes is correct. Thus, at least one correct process must have received a reliable broadcast from $p_j$ for round $r$.
    
    Now, by Bracha's Byzantine Reliable Broadcast specification, for any message broadcast instance by process $p_j$ in round $r$, all correct processes that deliver this broadcast either receive the identical message or none at all. Formally, for all correct processes $p_i, p_i'$ that received a delivery from $p_j$ for round $r$, we have $S_j^{(i)} = S_j^{(i')}$. 
    
    Therefore, there exists a unique set $S_j$ such that every correct process $p_i$ that receives a reliable delivery from $p_j$ for round $r$ receives exactly $S_j$.
\end{proof}

\begin{lemma}[Winners Stability]\label{lem:winners-stability}
    For any closed round $r$, the set $\winners[r]$ is stable.
\end{lemma}

\begin{proof}
    Let $r$ be a closed round. By definition, a closed round $r$ means that at least one correct process $p_i$ has observed $|\{k : (k, r) \in \BFTREAD()\}| \geq n - t$ and computed $\winners[r]$ at line \ref{alg:check-done}.
    
    When round $r$ becomes closed, this implies that at least $n - t$ distinct processes have invoked $\BFTAPPEND(\langle j, r \rangle)$ for $j \in \Pi$ (by the algorithm structure, since $\done[r]$ contains DONE messages from processes that completed line \ref{alg:append}). Since $n > 3f$, we have $n - t > 2f + 1 > t + 1$.
    
    Consider a fixed $j \in \Pi$. Since at least $n - t > t + 1$ processes have invoked a valid $\BFTAPPEND(\langle j, r \rangle)$, by \cref{lem:bft-prove-validity}, any subsequent invocation of $\BFTPROVE(\langle j, r \rangle)$ will be invalid.
    
    By \cref{lem:bft-prove-anti-flickering}, once a $\BFTPROVE(\langle j, r \rangle)$ operation becomes invalid, all subsequent $\BFTPROVE(\langle j, r \rangle)$ operations are also invalid.
    
    This holds for all $j \in \Pi$. Therefore, after the round $r$ is closed, the set of valid $\BFTPROVE(\langle j, r \rangle)$ operations for each $j$ cannot grow. By \cref{lem:bft-read-anti-flickering}, any subsequent $\BFTREAD()$ invocation will not return any new $(k, r)$ pairs beyond those already returned. Thus, $\winners[r] = \{j : (j, r) \in \BFTREAD()\}$ becomes stable and cannot change.
    
    Since this reasoning applies to all correct processes that compute $\winners[r]$ after round $r$ is closed, all correct processes will compute the same stable set $\winners[r]$.
\end{proof}

\begin{lemma}[Message Content Invariance]\label{lem:message-content-invariance}
    For any closed round $r$ and any correct process $p_i$, the set $M$ computed at line \ref{code:Mcompute} by $p_i$ is identical to the set computed by any other correct process $p_j$ for the same round $r$.
\end{lemma}

\begin{proof}
    Let $r$ be a closed round and let $p_i, p_{i'}$ be two correct processes. By the algorithm, both processes compute $M$ as:
    \[
    M^{(i)} = \bigcup_{j \in \winners[r]} \prop^{(i)}[r][j]
    \]
    and
    \[
    M^{(i')} = \bigcup_{j \in \winners[r]} \prop^{(i')}[r][j]
    \]
    at line \ref{code:Mcompute}.
    
    By \cref{lem:winners-stability}, the set $\winners[r]$ is stable once round $r$ is closed. Therefore, both $p_i$ and $p_{i'}$ compute the same set of winners $\winners[r]$.
    
    Now, consider any winner $j \in \winners[r]$. By \cref{lem:bft-unique-proposal}, there exists a unique set $S_j \subseteq \mathcal{M}$ such that every correct process that receives a reliable delivery of a $\texttt{PROP}$ message from $p_j$ for round $r$ receives exactly $S_j$. 
    
    By the algorithm, each correct process stores this received set in its local variable: $\prop^{(i)}[r][j] = S_j$ and $\prop^{(i')}[r][j] = S_j$.
    
    Since both processes compute the union over the same set of winners, and each winner's proposal is identical for all correct processes:
    \[
    M^{(i)} = \bigcup_{j \in \winners[r]} \prop^{(i)}[r][j] = \bigcup_{j \in \winners[r]} S_j = \bigcup_{j \in \winners[r]} \prop^{(i')}[r][j] = M^{(i')}
    \]
    
    Therefore, all correct processes compute the same set $M$ for any closed round $r$.
\end{proof}

\begin{lemma}[Inclusion]\label{lem:bft-inclusion}
    If a correct process $p_i$ invokes $\ABbroadcast(m)$, then there exist a closed round $r$ and a winner $j \in \winners[r]$ such that $p_j$ invoked $\RBcast(j, \texttt{PROP}, S, r)$ with $m \in S$.
\end{lemma}

\begin{proof}
    Let $p_i$ be a correct process that invokes $\ABbroadcast(m)$. By the algorithm, $p_i$ adds $m$ to $\unordered$. Consequently, $\unordered \setminus \ordered \neq \emptyset$, and the process enters the main loop and eventually invokes $\RBcast(i, \texttt{PROP}, S_i^{(1)}, r_1)$ for some round $r_1$ where $m \in S_i^{(1)}$.

    We distinguish two cases:
    
    \textbf{Case 1: $p_i$ becomes a winner in round $r_1$.}
    If $p_i$ is elected as a winner for round $r_1$ (i.e., $i \in \winners[r_1]$), then the claim holds with $r = r_1$ and $j = i$.
    
    \textbf{Case 2: $p_i$ does not become a winner in round $r_1$.}
    If $p_i$ is not elected as a winner, by the properties of Reliable Broadcast (Bracha's specification), at least one correct process $p_{i_1}$ will eventually receive the reliable delivery of the $\texttt{PROP}$ message from $p_i$ for round $r_1$. Process $p_{i_1}$ adds all messages from $S_i^{(1)}$ to its $\unordered$ set at line \ref{alg:append}. In particular, $m$ is now in $p_{i_1}$'s $\unordered$ set.
    
    In round $r_2 > r_1$ (and any subsequent round), process $p_{i_1}$ computes $S_{i_1}^{(2)} = \unordered \setminus \ordered$ and invokes $\RBcast(i_1, \texttt{PROP}, S_{i_1}^{(2)}, r_2)$ with $m \in S_{i_1}^{(2)}$.
    
    This process repeats: either $p_{i_1}$ becomes a winner and the claim holds, or another correct process receives $p_{i_1}$'s proposal and includes $m$ in its own proposal.
    
    Since $n > 3f$, we have $n - t > t + 1 > f$. By the pigeonhole principle, there eventually exists a round $r$ where at least $n - t$ distinct processes have proposed sets containing $m$. Since more than $2f$ processes have proposed $m$, at least one of them must be correct and be elected as a winner. Therefore, there exist a round $r$ and a winner $j \in \winners[r]$ such that $m \in S_j$ was broadcast by $p_j$.
\end{proof}

\begin{lemma}[Eventual Closure]\label{lem:bft-eventual-closure}
    For any correct process $p_i$, if $\unordered \setminus \ordered \neq \emptyset$ and if $r$ is the highest closed round observed by $p_i$, then eventually round $r+1$ will be closed with $|\winners[r+1]| \geq n - t$.
\end{lemma}

\begin{proof}
    Let $p_i$ be a correct process such that $\unordered \setminus \ordered \neq \emptyset$ after round $r$ is the highest closed round it observed. By the main loop of Algorithm~\ref{alg:bft-arb}, $p_i$ eventually enters round $r+1$, computes $S=\unordered\setminus\ordered$, and invokes $\RBcast(\texttt{PROP},S,\langle i,r+1\rangle)$.

    By RB Validity, every correct process eventually $\rdeliver(\texttt{PROP},S,\langle i,r+1\rangle)$. Upon this delivery, each correct process executes $\BFTPROVE(\langle i,r+1\rangle)$. Hence at least $n-t$ correct processes issue a proof for candidate $i$ in round $r+1$, and in particular the threshold $t+1$ used in $\validated(r+1)$ is eventually met for that candidate.

    The same argument applies to each correct process that broadcasts in round $r+1$: once its proposal is RB-delivered, at least $n-t$ correct processes issue the corresponding proofs, so that sender is eventually included in $\validated(r+1)$. Since there are at least $n-t$ correct processes, eventually $|\validated(r+1)| \geq n-t$, and the wait at line~\ref{alg:check-validated} is eventually released for every correct process in that round.

    After this point, each correct process executes the $\BFTAPPEND$ loop (line~\ref{alg:append}) and sends $\texttt{DONE}$ to all processes. By reliability of point-to-point channels, every correct process eventually receives at least $n-t$ DONE messages, so the wait at line~\ref{alg:check-done} is also eventually released. At that moment, the process computes $\winners[r+1] \gets \validated(r+1)$, and by the previous bound we have $|\winners[r+1]| \geq n-t$.

    Therefore round $r+1$ eventually becomes closed with at least $n-t$ winners.
\end{proof}

\begin{lemma}[Total Order]\label{lem:bft-total-order}
    For any two correct processes $p_i$ and $p_j$, the sequence $\ordered$ maintained locally by $p_i$ and the sequence maintained by $p_j$ contain the same messages in the same order, provided that both have reached the same set of closed rounds.
\end{lemma}

\begin{proof}
    We prove the claim by induction on the number of closed rounds completed by both processes.

    \textbf{Base case.} Before any closed round is completed, both local sequences are initialized to $\epsilon$, hence identical.

    \textbf{Induction step.} Assume that after all closed rounds up to $r-1$, processes $p_i$ and $p_j$ have identical $\ordered$ prefixes. Consider round $r$.

    By \Cref{lem:winners-stability}, once round $r$ is closed, both processes use the same stable winner set $\winners[r]$. By \Cref{lem:message-content-invariance}, the set $M$ computed at line~\ref{code:Mcompute} is identical at all correct processes for that round. Both processes then apply the same deterministic ordering function $\order(M)$ and append that same ordered block to their current sequence.

    Since they started round $r$ from identical prefixes and append the same ordered suffix for round $r$, their resulting sequences after round $r$ are identical. The induction concludes that for any common set of closed rounds, both correct processes maintain the same messages in the same order.
\end{proof}

\begin{theorem}
    The algorithm implements a BFT Atomic Reliable Broadcast.
\end{theorem}
