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`, and `formal/sphincs/` states the same kind of claim for the SPHINCS instance at 120 bits, with no proof yet. In both, `*/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`.
 - 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}}
@@ -74,7 +75,7 @@
   \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}
 
@@ -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}, which states $x=120$ at $\qs=2^{24}$: the eight bits below $n$ are what a proof may spend on union bounds and constants. Nothing proves it yet.
 
 \subsection{Quantum security}
 \label{sec:quantum}

formal/sphincs/.gitignore

@@ -0,0 +1 @@
+/.lake/

formal/sphincs/SphincsSecurity.lean

@@ -0,0 +1,18 @@
+import SphincsSecurity.Statement
+import SphincsSecurity.Proof
+
+namespace SphincsSecurity
+
+/-!
+The public security theorems for the statements in `SphincsSecurity.Statement`. The 125-bit proof combines the joint diagnostic and residual bounds with the forest, structural, encoding and message-collision bounds in the original SUF experiment.
+-/
+
+/-- `125` bits of classical strong unforgeability in the random-oracle model for the concrete SPHINCS instance, at `2^24` signing requests per key pair. -/
+theorem sphincs_has_125_bits_of_classical_security : SphincsSecurity125Statement := by
+  exact Concrete.OtsProbeSimulation.Range125.security125_of_completed_joint_boundary
+
+/-- `120` bits of classical strong unforgeability in the random-oracle model for the concrete SPHINCS instance, at `2^24` signatures per key pair. -/
+theorem sphincs_has_120_bits_of_classical_security : SphincsSecurityStatement := by
+  exact Concrete.OtsProbeSimulation.security_of_completed_canonical_boundary
+
+end SphincsSecurity