papers/lux-quasar-horizon/sections/04-horizon-soundness.tex

%% ====================================================================
\section{Horizon Soundness}
\label{sec:horizon-soundness}
%% ====================================================================

The composition theorem is \texttt{proofs/quasar/horizon-soundness.tex}. We restate it here for reference and connect it to the per-lane reductions.

\subsection{The composition theorem}

\begin{theorem}[Horizon-final implies all lanes verify the same transcript]
\label{thm:horizon-soundness}
Let $\mathsf{cert}$ be a Horizon certificate (Definition~\ref{def:horizon-cert} in the canonical bucket) with $\mathsf{Prism}(\mathsf{cert}) = 1$. Then the underlying validator set of size $n$ with $f < n/3$ corruptions cannot produce two Horizon-final certificates on distinct $\mathsf{NebulaRoot}$ values at the same $(\mathsf{epoch}, \mathsf{round})$, except with negligible probability under:
\begin{enumerate}[leftmargin=2em,nosep]
  \item BLS12-381 co-CDH (for the Beam lane);
  \item Module-LWE / Module-SIS (for the Pulsar lane, Theorem~\ref{thm:pulsar-suf-cma});
  \item EUF-CMA security of ML-DSA-65 / FIPS 204 (for the ML-DSA cert-set lane).
\end{enumerate}
The proof is by independent reduction: any pair of Prism-accepted certs on conflicting $\mathsf{NebulaRoot}$s at the same $(\mathsf{epoch}, \mathsf{round})$ forces a forgery in at least one lane. The lanes are independent (different hardness assumptions); a quantum adversary breaking BLS does not break the Pulsar or ML-DSA components, and vice versa.
\end{theorem}

The full proof, including the formal definitions of the three reductions, appears as Theorem~\ref{thm:horizon-soundness} of \texttt{proofs/quasar/horizon-soundness.tex} and is companion-cited from \texttt{proofs/quasar-cert-soundness.tex} (\cite{quasarcertsoundness}) Theorem 7.5 (classical soundness), Theorem 7.6 (parallel-lane liveness), and Theorem 7.7 (PQ safety).

\subsection{Per-lane reductions}

\paragraph{Beam (BLS aggregate).} Forging a BLS aggregate requires an adversary who controls more than $2n/3$ keys (since the aggregate weighs the signer set), or a forgery in the underlying BLS12-381 signature scheme. The latter reduces to co-CDH (\cite{boneh2001short}) over BLS12-381. Under quantum advice, BLS is broken in polynomial time by Shor; under classical attack, the standard $> 2^{120}$ security applies. This is why Beam alone is \emph{not} the PQ root of trust.

\paragraph{Pulse (Pulsar SUF-CMA).} Forging a Pulse with at most $t-1$ corrupted parties reduces to MLWE / MSIS, by Theorem~\ref{thm:pulsar-suf-cma} of \texttt{proofs/pulsar/unforgeability.tex} (cf. \cite{luxpulsar} Theorem 5.2). Concretely, with the LP-073 parameters \cite{luxpulsar}, classical security $\geq 2^{142}$ and quantum security $\geq 2^{130}$ via BDGL sieving plus Grover speedup (\texttt{quasar-cert-soundness.tex} App.~E). The Lean mechanization is \texttt{Crypto.Pulsar.corona\_pq\_unforgeability} \cite{leancrypto}.

\paragraph{ML-DSA cert set (FIPS 204 EUF-CMA).} Each per-validator signature reduces to MLWE/MSIS by FIPS 204's standard analysis. For the cert-set construction (a bitmap plus per-validator signatures, each over $\tau$ with the canonical context string \texttt{lux-quasar-horizon-v1}), forging a $\geq 2/3$-weight cert set requires forging $\geq 2/3$-weight worth of validator-specific ML-DSA signatures. Each forgery individually is hard under MLWE/MSIS; the bitmap construction adds no structural shortcut.

\subsection{Cross-lane independence}

\begin{lemma}[Lane independence under quantum advice]
\label{lem:lane-independence}
Let $\mathcal{A}$ be a polynomial-time adversary with quantum oracle access to BLS12-381's discrete log. Then $\mathcal{A}$'s success probability against the Pulsar lane is bounded by $\mathrm{Adv}^{\mathsf{MLWE}}_{q,\sigma_E}(\mathcal{A}) + \mathrm{Adv}^{\mathsf{MSIS}}_{q, [\mathbf{A}|-c\tilde{\mathbf{b}}], 2B}(\mathcal{A}) + \mathrm{negl}(\lambda)$. The DL oracle gives $\mathcal{A}$ no MLWE / MSIS-relevant computational power, since neither problem reduces to elliptic-curve DL. Symmetrically, an MLWE-oracle-equipped $\mathcal{A}$ enjoys no advantage against BLS.
\end{lemma}

This is the formal statement of ``BLS contributes no PQ security to a multi-lane cert,'' which is the central observation of \texttt{proofs/pq-finality-no-bls.tex} (\cite{pqfinalitynobls}). The implication for Quasar Horizon is: the Pulse lane is the post-quantum root of trust; the Beam lane provides classical fast-path performance; the ML-DSA cert set provides per-validator PQ accountability; the optional Groth16 wrapper around the ML-DSA cert set is a classical compression artifact, not a PQ contribution.

\subsection{The Groth16 wrapper}

\begin{remark}[Groth16 wrapper does not contribute PQ security]
\label{rem:groth16-wrapper-horizon}
A Z-Chain Groth16 rollup proof of ML-DSA cert-set verification (LP-307 \cite{lp307}, Definition~\ref{def:proof-lane} of \texttt{proofs/definitions/finality-definitions.tex}) is a \emph{classical succinct proof of post-quantum signature verification}. Pairing-based SNARKs over BLS12-381 break under Shor's algorithm. Horizon's PQ soundness (Theorem~\ref{thm:horizon-soundness} parts 2 and 3) flows from the ML-DSA signatures and Pulsar threshold signature alone. The Groth16 proof is verified for compatibility / compression only and is not part of the PQ reduction. See Remark~\ref{rem:groth16-wrapper} of \texttt{proofs/quasar/horizon-soundness.tex} and Remark~\ref{rem:groth16-not-pq} of \texttt{proofs/definitions/finality-definitions.tex}.
\end{remark}

The Lux specification corpus refuses to call the Groth16 wrapper ``the PQ proof lane.'' It is a wrapper, not a root of trust. Future PQ-friendly proof systems (P3Q~\cite{luxp3q} or lattice-based) replace Groth16 in the wrapper role; PQ finality continues to flow from ML-DSA + Pulsar.

\subsection{Liveness}

\begin{theorem}[Parallel-lane liveness]
\label{thm:parallel-liveness}
If $V_t$ has $\geq 2n/3$ honest validators, then in any interval of length at least $T$ (a chain-configured upper bound on per-lane signing latency, currently $T = 3\,\mathrm{s}$ on Lux mainnet), all three lanes produce signatures, and Prism accepts. The lanes are independent, so liveness in each is independent: any single-lane stall (e.g., a Pulse coordinator timeout) does not prevent a future round's Beam from being formed and re-anchored to the new $\tau$.
\end{theorem}
This is Theorem 7.6 of \cite{quasarcertsoundness}. The implementation uses an asynchronous-finality discipline (Section~\ref{sec:async-pq-finality}) so that Pulses follow Beams without forcing the Beam path to wait. The chain's safety does not require synchrony; parallel-lane liveness is a partial-synchrony property.

\subsection{Why we do not assume synchrony}

We do not require any synchronous round. The Prism predicate is asynchronous-safe: a verifier accepts a Horizon-final certificate when all three lanes' signatures arrive over $\tau$, irrespective of intra-round timing. Asynchronous PQ finality (Section~\ref{sec:async-pq-finality}) is the operational discipline that uses this fact. A non-asynchronous design that required all three lanes to land in the same wall-clock window would fail liveness on a WAN-distributed validator set under reasonable network failure models.

\subsection{Mechanization status}

\begin{itemize}[leftmargin=2em,nosep]
  \item \textbf{Pulsar SUF-CMA.} Lean: \texttt{Crypto.Pulsar.corona\_pq\_unforgeability} \cite{leancrypto}.
  \item \textbf{Reshare preserves master secret.} Lean: \texttt{Crypto.Threshold.Reshare.reshare\_preserves\_public\_key}, \texttt{Crypto.Threshold.Reshare.reshare\_same\_secret}.
  \item \textbf{Triple consensus.} Lean: \texttt{Consensus/Quasar.lean} carries \texttt{triple\_requires\_all}, \texttt{quantum\_safe\_triple}, \texttt{independent\_pq\_from\_classical}, \texttt{cert\_intersection}, \texttt{unique\_per\_round}.
  \item \textbf{BFT safety / liveness / finality.} Lean: \texttt{Consensus/\{Safety,Liveness,Finality,BFT\}.lean}.
  \item \textbf{TLA+.} \texttt{tla/Quasar.tla} model-checked (\texttt{tla/MC\_Quasar.cfg}).
  \item \textbf{Tamarin.} \texttt{tamarin/QuasarConsensus.spthy} verified against the canonical handshake / vote / bundle protocol.
\end{itemize}

The paper-level theorems (Theorem~\ref{thm:horizon-soundness}, Theorem~\ref{thm:pulsar-suf-cma}, Lemma~\ref{lem:lane-independence}) are companion-cited from these mechanizations; the canonical theorem names cited above are verbatim from the proof tree.