papers/lux-warp-v2/sections/05-soundness.tex

%% ====================================================================
\section{Soundness}
\label{sec:soundness}
%% ====================================================================

The cross-chain soundness theorem is \texttt{proofs/quasar/warp-pq-soundness.tex}. We restate it and connect it to the per-lane reductions and to the consensus-side Horizon theorem.

\subsection{Warp 2.0 envelope unforgeability}

\begin{theorem}[Warp 2.0 envelope unforgeability]
\label{thm:warp-v2-soundness}
Let $\mathsf{env}_2$ be a Warp 2.0 envelope (Definition~\ref{def:warp-v2-envelope}) with successful verification under $\mathsf{VerifyWithOptions}$. Then forging an alternative $\mathsf{env}'_2$ on the same $(\mathsf{sourceChainID}, \mathsf{sourceNebulaRoot}, \mathsf{sourceKeyEraID}, \mathsf{sourceGeneration})$ tuple with a different $\mathsf{payload}$ requires breaking either:
\begin{enumerate}[leftmargin=2em,nosep]
  \item BLS12-381 co-CDH (forging the Beam component); OR
  \item Module-LWE / Module-SIS (forging the Pulsar Pulse, Theorem~\ref{thm:pulsar-suf-cma}).
\end{enumerate}
A quantum adversary breaking only co-CDH (and not MLWE/MSIS) succeeds against the Beam alone; the Pulse remains unforgeable, so the v2 envelope as a whole remains sound under $\mathsf{VerifyWithOptions}$.
\end{theorem}

The full proof is Theorem~\ref{thm:warp-v2-soundness} of \texttt{proofs/quasar/warp-pq-soundness.tex}; the per-lane reductions live in \texttt{proofs/pulsar/unforgeability.tex} (Pulsar SUF-CMA) and are companion-cited from \texttt{quasar-cert-soundness.tex} \cite{quasarcertsoundness}. We highlight three structural facts:

\paragraph{The conjunction is essential.} The shape ``$\mathsf{VerifyWithOptions}$ accepts iff Beam-OR-Pulse'' is wrong for the same reason that ``Horizon iff Beam-OR-Pulse'' is wrong (Section~\ref{sec:prism-composition} of \cite{luxquasarhorizon}; \cite{pqfinalitynobls}): under a quantum adversary that breaks only BLS, ``Beam-OR-Pulse'' degrades to ``Beam alone'' and the envelope becomes forgeable. Warp 2.0's $\mathsf{VerifyWithOptions}$ is conjunctive: every required lane must verify against the same canonical digest $D$ (each lane over its own DST$\,\|\,D$).

\paragraph{PQ finality lives in the Pulse.} The Pulse is the post-quantum root of trust for a Warp 2.0 envelope. The Beam provides classical fast-path verification (sub-millisecond on commodity hardware). The optional ML-DSA cert set provides per-validator PQ accountability and slashing-evidence material. Under a quantum break of BLS, the Beam falls; the envelope remains sound iff the Pulse verifies. Without the Pulse, the v2 envelope degrades to Warp 1.x semantics --- which is correct, because absent the Pulse, the envelope is exactly Warp 1.x.

\paragraph{The Groth16 wrapper is not part of the PQ reduction.}

\begin{remark}[Groth16 wrapper does not contribute PQ security to Warp 2.0]
\label{rem:groth16-wrapper-warp}
A Z-Chain Groth16 rollup proof of ML-DSA cert-set verification (Definition~\ref{def:proof-lane}) is a \emph{classical succinct proof of post-quantum signature verification}. The proof system is pairing-based and not post-quantum. Warp 2.0's PQ soundness (Theorem~\ref{thm:warp-v2-soundness} parts 2 and the $\mathsf{Pulsar.Verify}$ branch) 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}.
\end{remark}

The Mar-3 freeze ships Warp 2.0 with the Pulse as the PQ root of trust. A future Warp Private PQ envelope replaces Groth16 with P3Q~\cite{luxp3q} or a lattice-based wrapper; PQ finality continues to flow from ML-DSA + Pulsar.

\subsection{Per-lane reductions}

\paragraph{Beam (BLS aggregate).} Forging the signed $\mathsf{Message}$ (the Beam carrier inside the envelope) requires either $> 2/3$-weight BLS-key control, or a forgery in the BLS12-381 signature scheme. Reduces to co-CDH \cite{boneh2001short}. Quantum-broken in polynomial time.

\paragraph{Pulse (Pulsar SUF-CMA).} Forging a Pulse over $\texttt{PulseSigningBytes}(D) = \text{``LUX-WARP-ZAP-PULSE-v1''}\,\|\,D$ with at most $t-1$ corrupted parties reduces to MLWE / MSIS, by Theorem~\ref{thm:pulsar-suf-cma} of \texttt{proofs/pulsar/unforgeability.tex}. With LP-073 parameters \cite{luxpulsar}, classical security $\geq 2^{142}$ and quantum security $\geq 2^{130}$.

\paragraph{ML-DSA cert set (FIPS 204 EUF-CMA).} Each per-validator signature reduces to MLWE / MSIS by FIPS 204's standard analysis. The cert-set's $\geq 2/3$-weight requirement adds no structural shortcut beyond the per-validator forgery cost.

\subsection{Cross-lane independence}

\begin{lemma}[Lane independence under quantum advice, cross-chain]
\label{lem:lane-independence-warp}
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 in a Warp 2.0 envelope 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)$.
\end{lemma}

This is the cross-chain analog of Lemma~\ref{lem:lane-independence} of \cite{luxquasarhorizon}: BLS provides no PQ contribution to a multi-lane cert, and the Pulse / ML-DSA reductions are independent of the BLS reduction.

\subsection{Warp Private orthogonality}

\begin{remark}[Warp Private orthogonality]
\label{rem:warp-private-orthogonal}
$\mathsf{Warp\,Private}$ (FHE-encrypted payload, optionally Pulse-signed) is orthogonal to $\mathsf{Warp\,2.0}$. Warp Private provides confidentiality; Warp 2.0 provides PQ finality. They compose: a Warp Private envelope MAY carry a Pulse, in which case Theorem~\ref{thm:warp-v2-soundness} applies unchanged to the encrypted-payload binding. Until the FHE circuits are production-ready, the Mar-3 freeze ships only Warp 2.0; Warp Private is open work.
\end{remark}

\subsection{Mechanization status}

\begin{itemize}[leftmargin=2em,nosep]
  \item \textbf{Warp 2.0 envelope unforgeability.} \texttt{proofs/quasar/warp-pq-soundness.tex}.
  \item \textbf{Pulsar SUF-CMA.} Lean: \texttt{Crypto.Pulsar.corona\_pq\_unforgeability}.
  \item \textbf{Reshare preserves master secret.} Lean: \texttt{Crypto.Threshold.Reshare.reshare\_preserves\_public\_key}.
  \item \textbf{LSS lifecycle invariants.} \texttt{proofs/lss/lifecycle-safety.tex}, \texttt{proofs/lss/rollback-safety.tex}.
  \item \textbf{Tamarin.} \texttt{tamarin/QuasarConsensus.spthy} verifies the protocol-level handshake / vote / bundle flow that produces the source-side Horizon certificate that Warp 2.0 carries.
\end{itemize}

\subsection{Why we do not assume synchrony for Warp delivery}

Warp envelope delivery is asynchronous; the destination's verifier accepts an envelope when all required lanes verify against the same transcript, irrespective of inter-chain timing. There is no global clock assumption. A Warp 2.0 envelope sits in the destination's pending-envelopes queue until the destination's resolver has the source's $(\eta, g)$ resolved; once resolved, the envelope is verifiable.

This is the cross-chain analog of asynchronous PQ finality (Section~\ref{sec:async-pq-finality} of \cite{luxquasarhorizon}). The forward consequence: cross-chain finality lag is bounded by source-chain Horizon-final lag plus destination-chain resolver-update lag, both of which are governance-configurable.