papers/lux-consensus/sections/05-formal-analysis.tex

\section{Formal Analysis}

\label{sec:analysis}

\subsection{Safety Analysis}

\begin{theorem}[Safety]
\label{thm:safety}
If two honest validators $v$ and $u$ both finalize transaction sets $T_v$ and $T_u$
respectively, then $T_v$ and $T_u$ are consistent: no two accepted transactions in
$T_v \cup T_u$ conflict.
\end{theorem}

\begin{proof}
Suppose for contradiction that honest validator $v$ finalizes $t$ and honest validator $u$
finalizes $t' \in \mathcal{C}(t)$ (a conflicting transaction). For $v$ to finalize $t$,
it must observe $\beta$ consecutive rounds where at least $\alpha k$ out of $k$ sampled
validators prefer $t$. Let $\rho_t(r)$ be the fraction of all validators preferring $t$
at round $r$.

For $v$ to complete $\beta$ rounds with supermajority for $t$, we need $\rho_t(r) \geq \alpha$
for all $r$ in those $\beta$ rounds (in expectation over samples). By a Chernoff bound,
the probability that fewer than $\alpha k$ out of a sample of $k$ honest validators
prefer $t$ when $\rho_t > \alpha$ is:
\begin{equation}
\Pr[\text{Bin}(k, \rho_t) < \alpha k] \leq e^{-k D(\alpha \| \rho_t)}
\label{eq:chernoff}
\end{equation}
where $D(\alpha \| \rho) = \alpha \ln(\alpha/\rho) + (1-\alpha)\ln((1-\alpha)/(1-\rho))$
is the KL-divergence.

For $u$ to finalize $t'$, by symmetric argument, $\rho_{t'}(r') \geq \alpha$ for $\beta$
rounds around time $r'$. But $t$ and $t'$ conflict: $\rho_t(r) + \rho_{t'}(r) \leq 1$
for all $r$ (a validator cannot prefer both). So $\rho_t(r) \geq \alpha$ implies
$\rho_{t'}(r) \leq 1 - \alpha < \alpha$ (since $\alpha > 1/2$).

The probability that $u$ observes $\alpha k$ supporters of $t'$ when at most $(1-\alpha)$
fraction of validators support $t'$ is bounded by Equation~\ref{eq:chernoff} with
$\rho = 1 - \alpha < \alpha$. For $u$ to complete $\beta$ such rounds, the probability
is at most $(e^{-k D(\alpha \| 1-\alpha)})^\beta$.

Setting $k = 20$, $\alpha = 0.8$, $\beta = 20$:
\begin{equation}
(e^{-20 \cdot D(0.8 \| 0.2)})^{20} = e^{-400 \cdot 0.832} \approx e^{-333} \approx 10^{-144}
\end{equation}
This is negligible in any practical security parameter. The union bound over all possible
pairs $(v, u)$ and all rounds gives a total safety failure probability of at most
$n^2 T \cdot 10^{-144}$ where $T$ is the protocol duration in rounds.
\end{proof}

\subsection{Byzantine Fault Tolerance}

\begin{theorem}[Byzantine Fault Tolerance]
\label{thm:bft}
Lux Consensus achieves safety under the presence of at most $f < n/3$ Byzantine validators.
\end{theorem}

\begin{proof}
A Byzantine validator can respond to queries with arbitrary colors. Suppose $f < n/3$
Byzantine validators all respond with color $0$, attempting to prevent honest consensus
on color $1$.

Consider a query sample $S$ of size $k$ from $n$ validators, $f$ of whom are Byzantine.
The expected number of Byzantine validators in the sample is $fk/n < k/3$.

For the adversary to create a false supermajority for color $0$, they need:
\begin{equation}
\text{Byzantine responses for } 0 + \text{honest responses for } 0 \geq \alpha k
\end{equation}

The adversary contributes at most $k/3$ votes. For $\alpha = 0.8 > 2/3$, the adversary
cannot alone create a supermajority. They need at least $0.8k - k/3 = 0.467k$ honest
votes for color $0$.

If the honest majority (fraction $> 2/3$) prefer color $1$, then the expected honest
votes for $0$ in a sample is at most $k/3$. The total expected votes for $0$ is at most
$k/3 + k/3 = 2k/3 < 0.8k = \alpha k$.

By the Hoeffding bound, the probability that the total exceeds $\alpha k$ decreases
as $e^{-2k(\alpha - 2/3)^2} = e^{-2 \cdot 20 \cdot (0.133)^2} = e^{-0.71}$. Over $\beta$
consecutive rounds, the failure probability is $(e^{-0.71})^{20} = e^{-14.2} \approx 10^{-6}$.
With the Wave confidence mechanism reinforcing the honest majority across rounds, the
actual safety margin is substantially larger.
\end{proof}

\begin{lemma}[Threshold Necessity]
\label{lem:threshold}
The condition $\alpha > 2/3$ is necessary for Byzantine safety when $f = n/3 - 1$.
\end{lemma}

\begin{proof}
If $\alpha \leq 2/3$, consider a network split into three equal groups $G_1, G_2, G_3$
of size $n/3$, where $G_3$ is Byzantine. The adversary can present color $0$ to queries
from $G_1$ and color $1$ to queries from $G_2$. With $\alpha \leq 2/3$, each group may
see a supermajority for its own color (receiving $2n/3 \geq \alpha n$ support), and two
honest nodes may finalize conflicting values.
\end{proof}

\subsection{Liveness Analysis}

\begin{theorem}[Liveness]
\label{thm:liveness}
Under partial synchrony (after GST), Lux Consensus terminates in $O(\beta \log n)$ rounds
with high probability, assuming fewer than $n/3$ Byzantine validators.
\end{theorem}

\begin{proof}
After GST, all messages are delivered within $\Delta$ time. We show convergence in two phases.

\textbf{Phase 1: Convergence to a majority.}
Let $p_r$ be the fraction of honest validators preferring color $1$ at round $r$. Starting
from any $p_0 > 1/2 + \epsilon$ for some $\epsilon > 0$, we show $p_r$ converges to 1.

The update rule for $p$ under the Wave dynamics is:
\begin{equation}
p_{r+1} = \Phi_\alpha(p_r) = \sum_{j=\lceil \alpha k \rceil}^{k} \binom{k}{j} p_r^j (1-p_r)^{k-j}
\end{equation}

This function satisfies $\Phi_\alpha(p) > p$ for all $p \in (1/2, 1)$ and the fixed points
are $\{0, 1\}$ (stable) and $1/2$ (unstable). The derivative at the unstable fixed point is:
\begin{equation}
\Phi'_\alpha(1/2) = \frac{k!}{(\lceil \alpha k \rceil - 1)!(k - \lceil \alpha k \rceil)!} \cdot 2^{-k} > 1
\end{equation}
which confirms instability and exponential amplification of deviations from $1/2$.

Starting from $p_0 > 1/2$, the dynamics reach $p > 1 - 1/n$ in at most
$O(\log n / \log(1/\lambda))$ rounds where $\lambda = \Phi'_\alpha(1/2)$.

\textbf{Phase 2: Maintaining supermajority for $\beta$ rounds.}
Once $p_r > \alpha$, the probability that any honest node fails to see supermajority
in a single round is at most $e^{-kD(\alpha \| p_r)}$. Over $\beta$ rounds, the
probability of maintaining supermajority is $(1 - e^{-\Omega(k)})^\beta$,
which is overwhelming for practical parameters.

Total convergence time: $O(\log n) + \beta = O(\beta \log n)$ rounds.
\end{proof}

\subsection{Convergence Bounds}

\begin{theorem}[Convergence Rate]
\label{thm:convergence}
Starting from any initial configuration with a strict honest majority for one value,
Lux Consensus reaches agreement in $O(\log n)$ rounds with probability
$1 - n^{-\Omega(1)}$.
\end{theorem}

\begin{proof}
Let $X_r$ be the fraction of honest validators preferring the majority value at round $r$,
and let $p_0 = X_0 > 1/2$. Define $Y_r = 1 - X_r$. We show $Y_r$ decreases geometrically.

The expected update satisfies $\mathbb{E}[Y_{r+1} \mid Y_r = y] \leq \lambda y$ for some
$\lambda < 1$ when $y < 1/2$. By the optional stopping theorem applied to the
supermartingale $\{Y_r / \lambda^r\}$, the expected time to reach $Y_r < 1/n$ is
$O(\log n)$ rounds. By Azuma's inequality, the probability that convergence takes more
than $C \log n$ rounds is at most $e^{-\Omega(C)}$.
\end{proof}

\subsection{Communication Complexity}

\begin{proposition}[Communication Complexity]
\label{prop:comm}
Lux Consensus requires $O(kn)$ messages per round and $O(k)$ amortized messages per
transaction decision in the DAG setting.
\end{proposition}

\begin{proof}
Each of the $n$ validators sends $k$ query messages per round ($kn$ total). In the DAG
setting, a single query round resolves preferences for the entire current conflict frontier
(all unresolved transactions), so the per-transaction cost is $O(k)$ amortized over the
DAG width $w$: total per-transaction complexity is $O(kn/w)$.
\end{proof}

\begin{table}[h]
\centering
\caption{Complexity comparison across consensus protocols}
\label{tab:complexity}
\begin{tabular}{@{}lllll@{}}
\toprule
Protocol & Messages/Decision & Latency & Finality & Fault Tolerance \\
\midrule
PBFT & $O(n^2)$ & $O(1)$ rounds & Immediate & $f < n/3$ \\
HotStuff & $O(n)$ & $O(1)$ rounds & Immediate & $f < n/3$ \\
Tendermint & $O(n^2)$ & $O(1)$ rounds & Immediate & $f < n/3$ \\
Nakamoto & $O(n)$ & $O(\kappa)$ blocks & Probabilistic & $f < n/2$ (hash) \\
Lux & $O(kn)$ & $O(\log n)$ rounds & Probabilistic & $f < n/3$ \\
\bottomrule
\end{tabular}
\end{table}

%% -----------------------------------------------------------------------
%%  6. PARAMETERIZATION
%% -----------------------------------------------------------------------