papers/lux-nebula-protocol/sections/05-safety-and-liveness.tex

\section{Safety and Liveness}

\label{sec:safety}

\begin{theorem}[Nebula Safety]
\label{thm:nebula-safety}
Under the Nebula protocol with $f < n/3$ Byzantine validators, the probability of
conflicting finalizations is bounded by:
\[
\Pr[\text{safety violation}] \leq \left(\frac{q_0}{q_1}\right)^{\beta} + n \cdot e^{-\Omega(\xi k)}
\]
where the second term accounts for incomplete information propagation in sparse networks.
\end{theorem}

\begin{proof}
The first term is the standard Wave safety bound: with threshold $\beta$, the probability
of the minority color overtaking the majority is $(q_0/q_1)^\beta$.

The second term arises because in sparse networks, local neighborhoods may temporarily
disagree with the global majority. If validator $v$'s neighborhood has a local majority
for color 0 while the global majority is color 1, $v$ might incorrectly finalize color 0.

The probability of this local disagreement persisting for $\beta$ rounds is bounded by
the probability that bridge information fails to correct the local bias. Each bridge
sample of size $k_b$ carries global information with accuracy $O(\sqrt{1/k_b})$. Over
$\beta$ rounds, the cumulative bridge information has accuracy $O(\sqrt{\beta / k_b}) = O(\sqrt{1/\xi k})$.

For this local bias to persist despite bridge information, the bridge samples must
all fail to reflect the global majority, with probability $\leq e^{-\Omega(\xi k)}$ per
round and $\leq e^{-\Omega(\xi k \beta)}$ over $\beta$ rounds.

A union bound over $n$ validators gives the stated result.
\end{proof}

\begin{lemma}[Nebula Liveness]
\label{lem:nebula-liveness}
After GST, every valid transaction is finalized within $O(\log n / \xi + \beta)$ rounds.
\end{lemma}

\begin{proof}
After GST, messages are delivered within $\Delta$. Bridge validators propagate
information across the network in $O(1/\xi)$ hops per round. The global convergence
takes $O(\log n / \xi)$ rounds (Theorem~\ref{thm:nebula-convergence}), and the
confidence counter reaches $\beta$ in an additional $O(\beta)$ rounds. Total:
$O(\log n / \xi + \beta)$.
\end{proof}

%% -----------------------------------------------------------------------
%%  6. PARTITION RECOVERY
%% -----------------------------------------------------------------------