mirror of
https://github.com/luxfi/proofs.git
synced 2026-10-30 15:21:05 +00:00
zeekay
1430256d11
Squashed batch covering:
- lux-adopts-liquidity-protocol.tex: protocol adoption proof artifact
- chronology updates aligning Quasar consensus references to LP-020
- pq-finality-no-bls.tex: Pulsar (Corona-derived lattice threshold)
naming clarification; per-block / per-epoch / per-era cert language
- quasar-cert-soundness.tex: Pulsar (systems-layer composition with
key-era lifecycle, resharing, activation cert, rollback) vs Corona
(signing primitive); math notation and theorems unchanged
- INFRASTRUCTURE-STATUS-2026-04-20.md → INFRASTRUCTURE-STATUS.md
(drop date stamp from filename)
- LP back-refs and chronology integration
quasar-cert-soundness.tex production-publishable depth (March 3 final):
- NEW Section 6 (Pulsar Key-Era Lifecycle Lemmas): formal
definitions for Pulsar share state, GroupKey hash, and Refresh /
Reshare / Reanchor transitions. Four lifecycle lemmas with full
proofs:
Lemma 10 (Generation monotonicity)
Lemma 11 (KeyEraID stability across Reshare)
Lemma 12 (GroupKey byte-identity across Refresh and Reshare)
Lemma 13 (Rollback-lineage forward reconstruction)
Plus Theorem 14 (Activation-certificate soundness): VerifyActivation
accepts iff the new committee shares Lagrange-recombine to the
master secret under the unchanged GroupKey, except with negligible
probability under MLWE/MSIS.
- Lagrange-recombination identity written as a labelled display
equation, citing
Crypto.Threshold.Reshare.reshare_preserves_public_key in
lean/Crypto/Threshold/Reshare.lean for the mechanised companion.
- Bibliography additions: hjky97 (Herzberg--Jarecki--Krawczyk--Yung
proactive secret sharing), desmedtjajodia97 (redistribution),
wongwangwing02 (verifiable redistribution), lp073 (Pulsar paper).
- LP-073 section pointers updated to text-form references that
survive without LP-073 .aux file.
Naming evolution: throughout this work, "Corona" refers to the
lattice signing primitive (Sign1/Sign2/Combine math); "Pulsar" refers
to the Lux production fork at github.com/luxfi/pulsar that wraps it
with key-era lifecycle for permissionless validator-set rotation.
- proofs/fhe/ (NEW): canonical proof bucket for the Lux FHE
dual-runtime stack (LP-167 companion):
correctness.tex — encrypt → evaluate → decrypt correctness.
dual-runtime-equivalence.tex — Lux FHE-Go and Lux FHE-C++ produce
byte-equal output on identical inputs
and parameters; KAT closure witness.
nebula-binding.tex — FHE result roots bind into Nebula /
Quasar transcripts; reduces a forged
binding to hash collision + Pulsar
SUF-CMA forgery.
parameter-security.tex — concrete LWE parameter security under
the Albrecht estimator; ≥128-bit
classical and ≥128-bit quantum for
PN10QP27 / PN11QP54 / PN9QP28_STD128.
Theorem statements + remarks; no proof bodies duplicated in the
companion paper (papers/lux-fhe-runtime/) — the paper cites these.
54 lines
2.5 KiB
TeX
54 lines
2.5 KiB
TeX
%% ============================================================
|
|
%% fhe/correctness.tex
|
|
%% ============================================================
|
|
%%
|
|
%% Canonical Lux FHE encrypt -> evaluate -> decrypt correctness
|
|
%% theorem. Papers cite this; do not redefine.
|
|
%% ============================================================
|
|
|
|
\subsection*{Lux FHE encrypt-evaluate-decrypt correctness}
|
|
|
|
\begin{theorem}[FHE encrypt-evaluate-decrypt correctness]
|
|
\label{thm:fhe-correctness}
|
|
Let $\mathsf{Lux\text{-}FHE} = (\mathsf{KeyGen}, \mathsf{Enc}, \mathsf{Dec}, \mathsf{Eval})$
|
|
denote the Lux FHE-Go reference scheme over the LWE-modulus pair $(q_{\mathrm{LWE}}, q_{\mathrm{BR}})$
|
|
with security parameter $\lambda$ (resolved through $\mathsf{ParameterSetID} \in
|
|
\{\mathsf{PN10QP27}, \mathsf{PN11QP54}, \mathsf{PN9QP28\_STD128}\}$). For any honestly-generated
|
|
key $\mathsf{sk}$, any plaintext bit $b \in \{0, 1\}$, and any boolean circuit
|
|
$C : \{0, 1\}^k \to \{0, 1\}$ of multiplicative depth bounded by the parameter set's
|
|
bootstrapping schedule:
|
|
\[
|
|
\Pr\!\left[
|
|
\mathsf{Dec}\bigl(\mathsf{sk},
|
|
\mathsf{Eval}\bigl(\mathsf{ek}, C, \mathsf{Enc}(\mathsf{sk}, b_1), \ldots,
|
|
\mathsf{Enc}(\mathsf{sk}, b_k)\bigr)\bigr)
|
|
= C(b_1, \ldots, b_k)
|
|
\right]
|
|
\;\geq\; 1 - \mathsf{negl}(\lambda).
|
|
\]
|
|
The negligible failure probability bounds the chance that the LWE noise envelope
|
|
exceeds the decoding threshold $q_{\mathrm{LWE}} / 4$ at any gate; the bound is
|
|
tight under the Albrecht parameter selection
|
|
(\texttt{proofs/fhe/parameter-security.tex}, Theorem~\ref{thm:lwe-parameter-security}).
|
|
\end{theorem}
|
|
|
|
\begin{remark}[Per-gate bootstrap]
|
|
\label{rem:per-gate-bootstrap}
|
|
Lux FHE evaluates one programmable bootstrap per non-XOR gate (XOR is
|
|
linear in the LWE secret and noise-additive without bootstrap). The
|
|
correctness budget therefore decomposes per-gate; the full circuit
|
|
correctness reduces to the per-gate bound by union over $|C|$ gates.
|
|
\end{remark}
|
|
|
|
\begin{remark}[Reference implementations]
|
|
\label{rem:fhe-reference-impls}
|
|
The canonical Go body is \texttt{github.com/luxfi/fhe.Evaluator.bootstrap}
|
|
(file \texttt{lux/fhe/evaluator.go}). The C++ realisation in
|
|
\texttt{luxcpp/crypto/fhe/cpp/backends/cpu/bootstrap\_cpu.cpp} is byte-equal
|
|
on the production parameter sets; the GPU realisations
|
|
(\texttt{cuda/cuda\_ntt\_kernel.cpp}, \texttt{cuda/cuda\_keyswitch\_kernel.cpp})
|
|
remain byte-equal under the LP-167 dual-runtime equivalence theorem
|
|
(\texttt{proofs/fhe/dual-runtime-equivalence.tex},
|
|
Theorem~\ref{thm:fhe-dual-runtime-equivalence}).
|
|
\end{remark}
|