diff --git a/AGENTS.md b/AGENTS.md index 9a2c5ada7..03d0f4391 100644 --- a/AGENTS.md +++ b/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). diff --git a/doc/sphincs/main.tex b/doc/sphincs/main.tex index 4f825a410..a779789db 100644 --- a/doc/sphincs/main.tex +++ b/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