proofs/fhe/dual-runtime-equivalence.tex

%% ============================================================
%% fhe/dual-runtime-equivalence.tex
%% ============================================================
%%
%% Canonical Lux FHE-Go <-> Lux FHE-C++ byte-equivalence theorem.
%% Papers cite this; do not redefine.
%% ============================================================

\subsection*{Lux FHE-Go and Lux FHE-C++ byte-equal output}

\begin{theorem}[FHE dual-runtime equivalence]
\label{thm:fhe-dual-runtime-equivalence}
Let $\mathcal{R}_{\mathsf{Go}}$ denote the Lux FHE-Go reference runtime
(\texttt{github.com/luxfi/fhe}) and let $\mathcal{R}_{\mathsf{C++}}$ denote the
Lux FHE-C++ production runtime (\texttt{github.com/luxfi/luxcpp/crypto/fhe}).
For every operation $\mathsf{op} \in \{\mathsf{KeyGen}, \mathsf{Enc}, \mathsf{Dec},
\mathsf{Eval}\}$, every parameter set $\mathsf{ps} \in
\{\mathsf{PN10QP27}, \mathsf{PN11QP54}, \mathsf{PN9QP28\_STD128}\}$, and every
input tuple $(\mathsf{seed}, x_1, \ldots, x_n)$ on which both runtimes accept
the inputs:
\[
  \mathcal{R}_{\mathsf{Go}}.\mathsf{op}(\mathsf{ps}, \mathsf{seed}, x_1, \ldots, x_n)
  \;=\;
  \mathcal{R}_{\mathsf{C\!+\!\!+}}.\mathsf{op}(\mathsf{ps}, \mathsf{seed}, x_1, \ldots, x_n)
\]
where equality is byte-equal under the Lux FHE-Core wire format
(\texttt{luxcpp/crypto/fhe/cpp/include/lux\_fhe/serialization.hpp}). The wire
format is parameter-set-tagged; the equality holds across every backend
$\mathcal{R}_{\mathsf{C\!+\!\!+}}.\mathsf{Backend} \in \{\mathsf{CPU},
\mathsf{CUDA}, \mathsf{HIP}, \mathsf{SYCL}\}$ that the runtime reports as
$\mathsf{available}(\cdot) = \mathsf{true}$.
\end{theorem}

\begin{proof}[Proof sketch]
The proof decomposes by operation:

\paragraph{KeyGen.} Both runtimes derive secret-key coefficients from the
same SHA-256 counter-mode PRNG keyed by $\mathsf{seed}$; the domain tags are
fixed (\texttt{"lwe"}, \texttt{"br"}) and the digest reduction is
identical. Public-key and evaluation-key derivations chain from the same
deterministic PRNG. Byte-equality follows from byte-equality of SHA-256
under the FIPS 180-4 specification.

\paragraph{Enc.} Both runtimes encode the bit as $b \in \{0, 1\} \mapsto
\pm q/8$ and apply the same NTT and rejection-sampled noise distribution
keyed by the same seed. Byte-equality of NTT across runtimes is the
canonical NTT byte-equivalence already established for
\texttt{luxcpp/crypto/poly\_mul} and \texttt{luxcpp/crypto/ntt}.

\paragraph{Dec.} Decryption is the inverse map of encryption. Equality of
the decoded plaintext bit follows from equality of the encrypted form and
the fixed centered-decoding rule.

\paragraph{Eval.} Each FHE gate decomposes into linear LWE combination plus
a programmable bootstrap. Linear combination is bytewise modular addition
modulo $q_{\mathrm{LWE}}$; both runtimes use the same modulus reduction
rule. Programmable bootstrapping is implemented via blind rotation; the
blind-rotation accumulator initial state, the gadget decomposition, and
the bootstrap-key indexing all match the Lux FHE-Go reference. The CUDA /
HIP / SYCL backends implement the same arithmetic; the LP-167
\texttt{Required claims for GPU-native credibility} \S 4 and \S 5 require
GPU outputs to be byte-equal to the CPU oracle on every input.

\paragraph{KAT closure.} The Lux FHE-KAT corpus (regenerated by
\texttt{lux/fhe/scripts/regen-kats.sh} and replayed by
\texttt{luxcpp/crypto/fhe/test/cpp/fhe\_kat\_replay\_test.cpp}) is the
empirical witness for byte-equality on every shipped parameter set. The
manifest digest is committed alongside the regen script.
\end{proof}

\begin{remark}[CPU fallback as semantic oracle]
\label{rem:cpu-fallback-oracle}
The C++ CPU fallback (\texttt{cpp/backends/cpu/}) is the semantic oracle:
GPU backends are byte-equal to it. If a GPU backend deviates, the GPU
backend is wrong --- the CPU fallback (which itself is byte-equal to the
Go reference under this theorem) is canonical.
\end{remark}

\begin{remark}[Scaffold milestone status]
\label{rem:fhe-scaffold-status}
On the v0.1.0-rc1-fhe-scaffold milestone this theorem holds for $\mathsf{op}
\in \{\mathsf{KeyGen}, \mathsf{Enc}, \mathsf{Dec}\}$ and the structural
fields of $\mathsf{Eval}$ (linear combination, NOT). Production
$\mathsf{Eval}$ byte-equality through programmable bootstrapping lands in
v0.1.0-rc2-fhe-gpu in lockstep with Lux FHE-Go's blind-rotate path.
\end{remark}