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.
48 lines
2.2 KiB
TeX
48 lines
2.2 KiB
TeX
%% ============================================================
|
|
%% pulsar/activation-safety.tex
|
|
%% ============================================================
|
|
%%
|
|
%% Canonical Activation circuit-breaker safety theorem.
|
|
%% ============================================================
|
|
|
|
\subsection*{Activation circuit-breaker safety}
|
|
|
|
\begin{theorem}[Activation cert is necessary and sufficient for safe transition]
|
|
\label{thm:pulsar-activation-safety}
|
|
Let $\mathsf{state}_g$ be the Pulsar share state at generation $g$, and
|
|
let $\mathsf{state}_{g+1}$ be a candidate next-generation state produced
|
|
by $\mathsf{DynamicResharePulsar}$
|
|
(Definition~\ref{def:lss-pulsar-adapter}). Suppose
|
|
$\mathsf{Pulsar.Verify}(\mathsf{GroupKey}, \mathsf{ActivationMsg}_{g+1},
|
|
\sigma_{\text{act}}) = 1$ where $\sigma_{\text{act}} = \mathsf{Pulsar.}
|
|
\mathsf{Activate}(\{\mathsf{Share}'_j\}, \mathsf{ActivationMsg}_{g+1})$.
|
|
Then with overwhelming probability:
|
|
\begin{enumerate}[nosep]
|
|
\item The new shares $\{\mathsf{Share}'_j\}$ recombine via Lagrange
|
|
to the same master secret $\mathbf{s}$ underlying
|
|
$\mathsf{state}_g$ (cf.\ Theorem~\ref{thm:pulsar-reshare-preserves-s}).
|
|
\item The new committee can produce verifying signatures under the
|
|
unchanged $\mathsf{GroupKey}$ for any future message.
|
|
\item The KeyEraID $\eta$ is unchanged from $\mathsf{state}_g$.
|
|
\end{enumerate}
|
|
Conversely, if any of (1), (2), (3) fail, the activation verification
|
|
fails with overwhelming probability.
|
|
|
|
\textbf{Soundness reduction:} a forgery of $\sigma_{\text{act}}$
|
|
without a quorum of valid new shares reduces to Pulsar SUF-CMA
|
|
(Theorem~\ref{thm:pulsar-suf-cma}) under the unchanged GroupKey.
|
|
|
|
\textbf{Companion proof:} \texttt{quasar-cert-soundness.tex}
|
|
Theorem 14 (\texttt{thm:activation-soundness}).
|
|
\end{theorem}
|
|
|
|
\begin{lemma}[Failure-mode containment]
|
|
\label{lem:activation-fail-safe}
|
|
If $\mathsf{Pulsar.Verify}$ on the activation cert returns $0$, the
|
|
chain remains at state $\mathsf{state}_g$. The candidate
|
|
$\mathsf{state}_{g+1}$ is discarded; the LSS RollbackManager retains
|
|
$\mathsf{state}_g$ as the active snapshot. This containment is
|
|
unconditional (does not depend on the cryptographic assumption); it is
|
|
a structural property of the chain's state-machine acceptance rule.
|
|
\end{lemma}
|