Sphincs FV in ROM

AGENTS.md

@@ -7,7 +7,7 @@ A minimal (zero-knowledge Virtual Machine, which is actually not ZK in the real
 - `doc/leanvm/` is the LaTeX project describing the machine ISA and the snark that proves it. Its root is `doc/leanvm/main.tex`; build it with `cd doc/leanvm && latexmk -pdf main.tex`, which writes to the gitignored `doc/leanvm/.build/`. Sections live in `doc/leanvm/body/`, numbered `01`..`10` plus the lettered annexes `a` (ring switching), `b` (the PCS), and `c` (Flock), and every symbol is defined once in `doc/leanvm/preamble/macros.tex`. If latexmk fails oddly (a bibtex error, or a missing `main.log`) right after inputs are renamed or `refs.bib` is edited, remove `doc/leanvm/.build` and rerun; it has not reproduced on unchanged inputs. **Drafting one section:** each section file carries a `% !TeX root` comment pointing at its generated driver in `doc/leanvm/drafts/`, so the LaTeX build key (`F5`, or the extension's `cmd+alt+b`) compiles only that section, numbered as in the full document and with cross-references and citations resolved against `.build/main.aux`; in `main.tex` the same key builds everything. Run `doc/leanvm/make-drafts.sh` after adding, renaming or renumbering a section.
 - `doc/xmss/` is the standalone specification of the concrete XMSS instance implemented by `crates/xmss`.
 - `doc/sphincs/` is the standalone specification of the concrete SPHINCS+ instance we would use instead of XMSS where statelessness matters; its root is `doc/sphincs/main.tex`, built the same way as `doc/xmss`, and implemented by `crates/sphincs`. It shares XMSS's hash function, tweakable hash and target-sum code, so an aggregator implements one primitive.
-- `formal/xmss/` is a Lean 4 proof (over VCVio) of that instance's classical random-oracle security, `xmss_has_127_bits_of_classical_security`. `XmssSecurity/Statement.lean` is the only module a reviewer has to read: the concrete parameters, the byte layout of every hash input, the three algorithms, the game, and the claim. `lake exe cache get` once, then `lake build`. SPHINCS has no formalization; its security section is a target, not a theorem.
+- `formal/xmss/` is a Lean 4 proof (over VCVio) of that instance's classical random-oracle security, `xmss_has_127_bits_of_classical_security`. `formal/sphincs/` proves 127 bits of classical strong unforgeability in the random-oracle model for the SPHINCS instance, `sphincs_has_127_bits_of_classical_security`; `formal/sphincs/PROOF.md` explains the route, the module layout by component, and what to re-prove if the one-time signature changes. In both, `*/Statement.lean` defines the concrete parameters, the byte layout of every hash input, the three algorithms, the game, and the claim. `lake exe cache get` once, then `lake build`. Both root modules pin the axiom footprint of their theorem with `#guard_msgs`.
 - The one hash function is BLAKE2s, in `primitives::hash`: scalar, streaming, keyed, and a lane-transposed batched form for the PCS Merkle tree. The VM proves one compression per opcode, and BLAKE2s takes the byte counter and final-block flag as ordinary compression inputs, so a single opcode is a complete hash for any length, with no tree structure to reproduce in-circuit.
 - `crates/lean_compiler/zkDSL.md` documents the (pythonic) zkDSL (that compiles to the ISA that our VM runs, and that our snark proves).
 

doc/sphincs/main.tex

@@ -26,6 +26,7 @@
 \newcommand{\Sig}{\mathsf{Sig}}
 \newcommand{\Ver}{\mathsf{Ver}}
 \newcommand{\SIG}{\mathsf{SIG}}
+\newcommand{\Forge}{\mathsf{Forge}}
 \newcommand{\Chain}{\mathsf{Chain}}
 \newcommand{\hash}{\mathsf{H}}
 \newcommand{\LE}{\mathsf{LE}}
@@ -69,12 +70,12 @@
 
 \begin{itemize}
   \item \textbf{stateless}: supporting up to $2^{24}$ signatures.
-  \item \textbf{NIST security level~1}~\cite{NISTPQC} (TODO prove it)
+  \item \textbf{NIST security level~1}~\cite{NISTPQC}: 127 bits of classical strong unforgeability in the random-oracle model, proven in Lean (Section~\ref{sec:security}); the quantum analysis is still to do.
   \item \textbf{public key: 32 bytes}.
   \item \textbf{signature: 4924 bytes}.
   \item \textbf{497 hashes per verification}.
   \item signing costs 190K hashes with 1024 bytes of cached signer state, or 1.55M without.
-  \item \textbf{key generation costs 1.38M hashes}.
+  \item \textbf{key generation costs 1.38M hashes}, which is the one tree of layer $0$ and nothing else.
 \end{itemize}
 \end{abstract}
 
@@ -365,7 +366,7 @@ \section{Signing}
 returning $\bot$ if $\OtsSign$ does.
 \item Output $\sigma=\left(\rho,(s_\kappa,B_\kappa)_{\kappa<k-1},(c_\lay,\sigma_\lay,A_\lay)_{\lay<d}\right)$.
 \end{enumerate}
-$M_{-1}$ is computed and discarded: it is $\rootnode$ whenever the signer is honest. The signature is serialized as
+$M_{-1}$ would be $\rootnode$ whenever the signer is honest, so the loop need not compute it. The signature is serialized as
 \[
   \rho
   \concat s_0\concat B_{0,0}\concat\cdots\concat B_{0,a-1}
@@ -427,7 +428,7 @@ \section{Costs}
 \end{center}
 
 \begin{remark}[Test vectors]
-Nothing implements this scheme yet, so the document carries no test vectors. One key pair, one message, and the resulting $\rho$, $\idx$, the $k$ indices $u_\kappa$, the $d$ counters $c_\lay$ and the 4924 signature bytes would pin every convention above, and should be added before anyone implements against it.
+The document carries no test vectors yet. One key pair, one message, and the resulting $\rho$, $\idx$, the $k$ indices $u_\kappa$, the $d$ counters $c_\lay$ and the 4924 signature bytes would pin every convention above, and should be added before anyone implements against it.
 \end{remark}
 
 \section{Security}
@@ -436,25 +437,24 @@ \section{Security}
 \subsection{Classical security}
 
 \begin{definition}[Strong unforgeability in the ROM]
-Let $\SIG=(\Gen,\Sig,\Ver)$ be a signature scheme whose algorithms use a hash function $\hash:\bits{*}\to\bits{256}$. Consider the following game between a signer and an adversary $\mathcal A$ (an arbitrary probabilistic algorithm with unbounded running time and memory), with $\hash$ sampled as a random oracle, that both signer and adversary can query. The signer first runs $(\pk,\sk)\gets\Gen$ and gives $\pk$ to $\mathcal A$. The adversary may then adaptively take any of the following actions:
+Let $\SIG=(\Gen,\Sig,\Ver)$ be a signature scheme whose algorithms use a hash function $\hash:\bits{*}\to\bits{256}$. Consider the following game between a signer and an adversary $\mathcal A$ (an arbitrary probabilistic algorithm with unbounded running time and memory), with $\hash$ sampled as a random oracle that both may query. The signer runs $(\pk,\sk)\gets\Gen$ and gives $\pk$ to $\mathcal A$, which may then adaptively take any of the following actions:
 \begin{enumerate}[leftmargin=2em]
   \item Query the random oracle on any input and receive its 256-bit output.
-  \item Submit a message $m\in\bits{\lmsg}$ and receive $\sigma\gets\Sig(\sk,m)$ from the signer, which may be $\bot$. It may do so at most $\qs$ times, on any messages, the same one included: $\Sig$ keeps no state, so nothing here is used up.
+  \item Submit a message $m\in\bits{\lmsg}$ and receive $\sigma\gets\Sig(\sk,m)$ from the signer, which may be $\bot$. It may do so at most $\qs$ times.
   \item Terminate with a claimed forgery $(m^*,\sigma^*)$.
 \end{enumerate}
 The adversary wins if $\Ver(\pk,m^*,\sigma^*)=1$ and the signer did not return $\sigma^*$ in response to a signing query for $m^*$, meaning:
 \begin{itemize}[leftmargin=2em]
   \item if the adversary never queried a signature for $m^*$;
   \item or it did, but no answer it received was $\sigma^*$.
 \end{itemize}
-
-Call $\mathcal A$ $q$-bounded if the experiment makes at most $q$ random-oracle queries on every execution, counting those of key generation, signing, and the final verification of the claimed forgery. We say that $\SIG$ has $x$ bits of classical strong unforgeability in the ROM at $\qs$ signatures if every $q\geq1$ and every $q$-bounded $\mathcal A$ satisfy
+Let $\Forge_{\SIG}(\qs,q)$ be the maximum winning probability of any adversary for which the total number of random-oracle queries made in the experiment, including during key generation, signing, and the final verification of the claimed forgery, is at most $q$ on every execution path; it is $0$ below what key generation and one verification already cost. An adversary that spends all $\qs$ signatures needs $q$ past $2^{58}$, the attempt caps bounding the loops, so that is where the claim is read. We say that $\SIG$ has $x$ bits of classical strong unforgeability in the ROM at $\qs$ signatures if
 \[
-  \Pr[\mathcal A\text{ wins}]\leq\frac{q}{2^{x}}.
+  \max_{q\geq1}\frac{\Forge_{\SIG}(\qs,q)}{q}\leq 2^{-x}.
 \]
 \end{definition}
 
-TODO prove 127 bits of classical strong unforgeability in the ROM at $\qs=2^{24}$ signatures.
+That game, with the parameters and the algorithms above, is written out in Lean4 over the VCVio framework~\cite{VCVio} in \texttt{./formal/sphincs/SphincsSecurity/Statement.lean}, and \texttt{sphincs\_has\_127\_bits\_of\_classical\_security} proves $x=127$ at $\qs=2^{24}$: the one bit below $n$ is what the proof spends on union bounds and constants. The proof is in the classical random-oracle model with independently sampled secrets; the seed derivation of Remark~\ref{rem:seed} and the instantiation of $\hash$ by BLAKE2s are outside it.
 
 \subsection{Quantum security}
 \label{sec:quantum}

formal/sphincs/.gitignore

@@ -0,0 +1,3 @@
+/.lake/
+reach.txt
+taint.txt