papers/lux-quasar-horizon/sections/02-formal-model.tex

%% ====================================================================
\section{Formal Model}
\label{sec:formal-model}
%% ====================================================================

This section fixes notation. We follow the canonical definitions of the proof bucket; we do not redefine algorithms. The single source of truth for algorithm signatures is \texttt{proofs/definitions/algorithms.tex}; the single source of truth for transcript binding is \texttt{proofs/definitions/transcript-binding.tex}; the single source of truth for finality state and certificate composition is \texttt{proofs/definitions/finality-definitions.tex}. We summarize what is needed for the composition argument.

\subsection{Validator set and key era}

Let $V_t$ be the validator set at chain time $t$. A \textbf{key era} is a maximal interval over which the Pulsar GroupKey $(\mathbf{A}, \tilde{\mathbf{b}})$ and the Lens GroupKey $(g, h, X)$ remain byte-identical. Eras are indexed by a monotone scalar $\eta = \mathsf{KeyEraID}$, incremented only on \emph{Reanchor} (LSS lifecycle, \cite{luxlssmpc,lp077}). Within an era, a generation index $g \geq 0$ tracks LSS-managed share rotations; $g$ increments on every Refresh (HJKY97 \cite{hjky97}) or Reshare (Desmedt--Jajodia \cite{desmedtjajodia97}; verifiable per Wong--Wang--Wing \cite{wongwangwing02}). A rollback marker $r = \mathsf{RollbackFrom}$ records the prior generation reverted from when the chain rolls back; $r=0$ on forward transitions.

Every validator $i \in V_t$ holds a Pulsar \emph{shard} (one Shamir share over $R_q^{N_{\textrm{vec}}}$ of the Pulsar master secret $\mathbf{s}$), an independent BLS keypair, an independent ML-DSA-65 keypair, and optionally a Lens shard. The four key materials are intentionally independent: a quantum adversary breaking BLS does not break the ML-DSA, Pulsar, or Lens components.

\subsection{Nebula DAG substrate}

The chain produces a partial order of vertices over the cycle of epochs and rounds; this is the \textbf{Nebula} substrate (LP-020 \cite{lp020}, LP-105 \cite{lp105}). At each epoch's bundle interval (the Lux mainnet uses a $\sim 3$-second interval grouping $\sim 6$ blocks), a deterministic DAG-finalization rule selects a cut and emits a 32-byte $\mathsf{NebulaRoot}_b$:
\begin{equation}
  \mathsf{NebulaRoot}_b \;:=\; H_T\bigl(\mathsf{header}, \mathsf{vertexSet}_b, \mathsf{validatorSetHash}, \eta, g, b\bigr)
\end{equation}
where $H_T$ is the canonical TupleHash256 \cite{nistsp800185}. We write $\mathsf{NebulaRoot}_b$ to mean the canonical bundle root of bundle $b$; for a non-bundle frontier or epoch-level cut the same notation is used with the appropriate canonical content.

\subsection{Adversary and corruption model}

The adversary is computationally bounded with possibly quantum-aided lower-bound queries; it adaptively corrupts up to $f$ validators with $f < n/3$ for the standard Byzantine bound, where $n = |V_t|$. The adversary controls the network (delay, drop, reorder) but not the chain's deterministic state-machine acceptance rule. The adversary's PQ access is independent of its classical access: a quantum oracle for elliptic-curve discrete log (which breaks BLS and Groth16) does not provide a Module-LWE oracle (which would break ML-DSA, Pulsar, and Lens to the extent Lens runs on a curve --- see below).

\subsection{Generation as the canonical lifecycle scalar}

The Pulsar share lineage is $(\eta, g, r)$. A Pulsar Pulse emitted at $(\eta, g)$ verifies under the GroupKey that is byte-identical for every $g$ within $\eta$ (Lemma~\ref{lem:gk-byte-identical}, \texttt{proofs/lss/lifecycle-safety.tex}). Therefore: a verifier need only know the active $\eta$ and the active GroupKey; it does not need to track $g$ for verification \emph{within} an era, only across eras.

This is the technical reason Horizon can compose Beam, ML-DSA cert set, and Pulse: each lane references the same $(\eta, g, \mathsf{HashSuiteID})$ tuple in its transcript, and that tuple is enough to identify which BLS validator-set, which ML-DSA validator-set, and which Pulsar GroupKey to verify against. The transcript binding makes the lanes mutually self-locating without out-of-band registry lookups beyond the chain's own state.

\subsection{Generation, validator-set, and tier coupling}

\begin{definition}[Coupled state at $(\eta, g)$]
\label{def:coupled-state}
The chain's coupled state at $(\eta, g)$ is the tuple
\[
  \bigl(V_t, \mathsf{BLSRegistry}_t, \mathsf{MLDSARegistry}_t, \mathsf{PulsarGroupKey}_\eta, \mathsf{LensGroupKey}_\eta, \mathsf{HashSuiteID}\bigr)
\]
recorded on chain at the moment Bootstrap or Reshare for $(\eta, g)$ activated successfully under \texttt{QUASAR-PULSAR-ACTIVATE-v1} \cite{luxpulsar}. A Horizon certificate at $(\eta, g)$ is a Prism-bound composite over this coupled state.
\end{definition}

\subsection{What we hold fixed}

The following are protocol parameters fixed by the chain configuration:
\begin{itemize}[leftmargin=2em,nosep]
  \item Pulsar parameters: $R_q = \mathbb{Z}_q[X]/(X^{256}+1)$, $q = \texttt{0x1000000004A01}$, matrix dimensions $(M, N_{\mathrm{vec}}) = (8, 7)$ (\texttt{proofs/definitions/algorithms.tex} Definition \texttt{def:pulsar-setup}; mirror in \texttt{pulsar/sign/config.go});
  \item ML-DSA parameter set: ML-DSA-65 (FIPS 204);
  \item BLS curve: BLS12-381;
  \item Hash suite: $\mathsf{Pulsar\text{-}SHA3}$ by default (\texttt{proofs/definitions/transcript-binding.tex} Definition \texttt{def:pulsar-sha3}); $\mathsf{Pulsar\text{-}BLAKE3}$ allowed but not normative for production;
  \item Bundle interval: $\sim 3$ seconds on Lux mainnet (LP-020 \cite{lp020}).
\end{itemize}

The composition theorem (Section~\ref{sec:horizon-soundness}) is parametric in these choices: any FIPS-equivalent classical aggregate, any FIPS-204-conformant per-validator PQ signature, and any Module-LWE-secure two-round threshold lattice scheme satisfying the LP-073 systems contract works in this slot. We name the production choices for concreteness; the architecture is not tied to them.