papers/lux-photon-protocol/sections/04-safety-analysis.tex

\section{Safety Analysis}

\label{sec:safety}

\subsection{Independence of Confidence Counters}

\begin{theorem}[Pipelined Safety]
\label{thm:pipeline-safety}
For $m$ independent transactions (no shared conflict sets) in the Photon pipeline, the
probability that any transaction experiences a safety violation is at most:
\[
\Pr[\text{any violation}] \leq m \cdot (q_0/q_1)^\beta
\]
where $q_0, q_1$ are the supermajority probabilities for minority and majority colors.
\end{theorem}

\begin{proof}
Consider two transactions $t_i, t_j$ in the pipeline with independent conflict sets.
Their confidence counters $D_{i,\cdot}$ and $D_{j,\cdot}$ evolve based on the same
sample $S$ but independent color queries.

For transaction $t_i$, the responses from $S$ about $t_i$'s conflict are drawn from
the population distribution for $t_i$'s conflict set. Similarly for $t_j$. Since the
conflict sets are disjoint, the responses are independent random variables (the same
validator may respond differently for $t_i$ and $t_j$).

Therefore, the confidence counter evolution for $t_i$ is statistically independent of
$t_j$'s. The safety violation probability for each transaction is $(q_0/q_1)^\beta$
(from the Wave analysis), and by a union bound over $m$ transactions:
\[
\Pr[\text{any violation}] \leq m \cdot (q_0/q_1)^\beta
\]

For $m = 100$ and $(q_0/q_1)^\beta < 2^{-128}$: $100 \cdot 2^{-128} < 2^{-121}$,
still negligible.
\end{proof}

\subsection{Conflicting Pipeline Entries}

\begin{lemma}[Same-Conflict Serialization]
\label{lem:serialization}
If two transactions $t_i, t_j$ in the pipeline belong to the same conflict set
$\mathcal{C}$, the Photon protocol serializes their finalization: $t_j$ cannot finalize
until $t_i$'s conflict is resolved.
\end{lemma}

\begin{proof}
When $t_i \in \mathcal{C}(t_j)$, the validator's preference for $t_j$ depends on $t_i$'s
outcome. The confidence counter for $t_j$ cannot reach $\beta$ until the population
has converged on $t_i$'s resolution, because the supermajority condition for $t_j$
requires consistency with $t_i$'s resolution. This serialization adds at most $\beta$
additional rounds for the second transaction, which is the normal single-transaction
finality time.
\end{proof}

%% -----------------------------------------------------------------------
%%  5. PIPELINE STALL ANALYSIS
%% -----------------------------------------------------------------------