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

\section{Safety and Liveness}

\label{sec:safety}

\subsection{Burst Safety}

\begin{theorem}[Nova Safety]
\label{thm:nova-safety}
Two conflicting transactions $t_1, t_2 \in \mathcal{C}$ cannot both appear in
finalized bursts. Specifically, if $t_1 \in \text{burst}(v_1)$ and
$t_2 \in \text{burst}(v_2)$ where both bursts are finalized, then $t_1 \neq t_2$
implies $t_1 \notin \mathcal{C}(t_2)$.
\end{theorem}

\begin{proof}
Nova inherits the safety of the underlying Wave confidence mechanism. For a frontier
vertex $v$ to be finalized, it must accumulate $\beta$ rounds of supermajority for
its preferred conflict resolution. By the confidence monotonicity theorem (Wave paper,
Theorem 4.2), once a resolution is preferred with confidence $\beta$, the probability
of the competing resolution reaching confidence $\beta$ is at most $(q_0/q_1)^\beta < 2^{-128}$.

The burst mechanism only adds ancestors that are consistent with the frontier vertex's
preferred resolution (Algorithm~\ref{alg:nova-conflict}). If $t_1$ and $t_2$ conflict,
the topological sort in the conflict resolution ensures that only the higher-confidence
transaction is included in the accepted set. Since confidence is monotone and the
population converges to a single preference, all honest validators' bursts include
the same conflict resolution.
\end{proof}

\subsection{Nova Liveness}

\begin{lemma}[Burst Liveness]
\label{lem:nova-liveness}
Every valid transaction is included in a finalized burst within $O(\log n + D + \beta)$
rounds, where $D$ is the maximum depth of the transaction in the DAG.
\end{lemma}

\begin{proof}
A transaction $t$ at depth $D$ becomes part of the frontier after at most $D$ rounds
(as its parents are finalized in previous bursts or are themselves frontier vertices).
Once on the frontier, the Wave dynamics converge in $O(\log n)$ rounds, and the
confidence counter reaches $\beta$ in an additional $O(\beta)$ rounds. The total
latency is $O(D + \log n + \beta)$.

For shallow DAGs ($D = O(\log n)$), this simplifies to $O(\log n + \beta)$.
\end{proof}

%% -----------------------------------------------------------------------
%%  6. EVALUATION
%% -----------------------------------------------------------------------