Sphincs aggregation

.github/workflows/doc.yml

@@ -62,10 +62,16 @@ jobs:
         with:
           working_directory: doc/xmss
           root_file: main.tex
+      - name: Compile SPHINCS specification
+        uses: xu-cheng/latex-action@v3
+        with:
+          working_directory: doc/sphincs
+          root_file: main.tex
       - name: Name the artifacts
         run: |
           cp doc/leanvm/.build/main.pdf leanVM-b.pdf
           cp doc/xmss/.build/main.pdf XMSS.pdf
+          cp doc/sphincs/.build/main.pdf SPHINCS.pdf
       - name: Publish PDFs as release assets
         uses: softprops/action-gh-release@v2
         with:
@@ -76,7 +82,9 @@ jobs:
 
             `leanVM-b.pdf` contains the leanVM-b specification.
             `XMSS.pdf` contains the XMSS specification.
+            `SPHINCS.pdf` contains the SPHINCS specification.
           make_latest: false
           files: |
             leanVM-b.pdf
             XMSS.pdf
+            SPHINCS.pdf

AGENTS.md

@@ -6,6 +6,8 @@ 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.
 - 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).
 
@@ -28,7 +30,8 @@ Dependency order, leaves first:
 | `lean_vm`         | arithmetization: tables, bus, constraints, `cpu::prove`/`verify`       |
 | `lean_compiler`   | zkDSL (Python subset) → ISA                                            |
 | `xmss`            | XMSS over BLAKE2s; an independent leaf, consumed only by `rec_aggregation` |
-| `rec_aggregation` | recursive XMSS aggregation: the one guest, the public API, the benchmarks |
+| `sphincs`         | the stateless SPHINCS+ instance of `doc/sphincs`; an independent leaf, consumed only by `rec_aggregation` |
+| `rec_aggregation` | recursive XMSS and SPHINCS aggregation: the one guest, the public API, the benchmarks |
 
 `src/main.rs` is the CLI; guests are zkDSL under `crates/rec_aggregation/guests/`.
 
@@ -60,9 +63,12 @@ Heavy benches and measurement harnesses are `#[ignore]`d; run by name with `-- -
 ## Benchmarking
 
 The benchmarks we care about:
-- `cargo run --release -- xmss --n-signatures 900 --log-inv-rate 1 --repeat 3`
+- `cargo run --release -- aggregate --xmss 900 --log-inv-rate 1 --repeat 3`
+- `cargo run --release -- aggregate --sphincs 220 --log-inv-rate 1 --repeat 3`
 - `cargo run --release -- recursion --n 2 --xmss-per-leaf 900 --log-inv-rate 2 --repeat 3`
 
+`aggregate` takes a count per scheme, both defaulting to zero, so either alone or a mix of the two is one command; `recursion --sphincs-per-leaf` likewise puts both schemes in one tree. One SPHINCS signature costs 531 compressions against XMSS's 144, and about six times an XMSS signature's VM cycles, so a leaf of a given proven size holds proportionally fewer of them.
+
 ## The proving arena (`zk_alloc`)
 
 One proof is one **phase**, opened by `cpu::prove`. `ArenaVec` bumps a per-thread slab, freeing is a no-op, and the next `begin_phase()` reclaims everything. Not a `#[global_allocator]`: `raw_dealloc` picks arena-vs-system by address range, so with no phase open `ArenaVec` is an ordinary system vector (used in particular by the verifier, where correctness and simplicity matters much more than performance).
@@ -87,9 +93,9 @@ The same verification algorithm is written out three times, in three languages.
 
 1. **Rust**, `lean_vm::cpu::verify`. The performant verifier implem.
 2. **Python**, `python-verifier/verifier.py` (~2.5k lines, no dependencies). pure python, for readability and simplicity. Pinned by `lean_vm/tests/verifiers/python_verifier.rs`.
-3. **Recursive verifier**, `crates/rec_aggregation/guests/aggregate.py` (~2.7k lines of zkDSL). Written using our pythonic zkDSL (but it's not real python!), which then compiles to our custom ISA. Proving it result in recursion -> a snark of another snark.
+3. **Recursive verifier**, `crates/rec_aggregation/guests/aggregate.py` (~3.2k lines of zkDSL). Written using our pythonic zkDSL (but it's not real python!), which then compiles to our custom ISA. Proving it result in recursion -> a snark of another snark.
 
-Understand the third before changing the verifier. `guests/aggregate.py` is zkDSL, not runnable Python. `lean_compiler` lowers it to the six-opcode, write-once-memory VM, so the prover proves every verifier step. The guest is ~330k instructions (2^19 padded), with the mix reported by the recursion benchmark. Two consequences:
+Understand the third before changing the verifier. `guests/aggregate.py` is zkDSL, not runnable Python. `lean_compiler` lowers it to the six-opcode, write-once-memory VM, so the prover proves every verifier step. The guest is ~354k instructions (2^19 padded), with the mix reported by the recursion benchmark. It verifies raw signatures of both schemes: a node's coverage table is one contiguous region per scheme, so the one range check a write already needs also keeps an XMSS signature off a declared SPHINCS claim, and the statement's two signer lists say which scheme verified which key. The XMSS signers share the statement's message and epoch; a SPHINCS signer's message rides its own four-cell slot, so that list is `(key, message)` pairs and its length counts claims rather than distinct signers. XMSS's tweaks ride the statement (they depend only on the public epoch); SPHINCS's are built in-circuit from the index its message digest picks. Two consequences:
 
 - The guest is **self-referential**: it verifies proofs of itself, so `unified_guest` compiles it to a fixed point on its own log size. The digest needs no fixed point, riding the statement instead of the code, which is also what lets one bytecode serve any inner size and PCS rate.
 - It does not verify *quite* everything in-circuit. Three claims on fixed polynomials (stacked bytecode, flock's A0/B0) are deferred. Each node batches its children's carried claims with the fresh ones its verifications raise, `2n` per polynomial down to one; only the root's are discharged natively, by `AggregateSignature::verify` (explained in `doc/leanvm/`).

Cargo.toml

@@ -38,6 +38,7 @@ lean_vm = { path = "crates/lean_vm" }
 lean_compiler = { path = "crates/lean_compiler" }
 rec_aggregation = { path = "crates/rec_aggregation" }
 xmss = { path = "crates/xmss" }
+sphincs = { path = "crates/sphincs" }
 zk_alloc = { path = "crates/zk_alloc" }
 parallel = { path = "crates/parallel" }
 libc = "0.2"

README.md

@@ -9,8 +9,9 @@
 </p>
 
 <p align="center">
-  <a href="#xmss-aggregation"><img src="https://img.shields.io/badge/Aggregation-1100%20XMSS%2Fs-brightgreen?style=for-the-badge" alt="Aggregation: 1100 XMSS/s"></a>
-  <a href="#recursion"><img src="https://img.shields.io/badge/2%20to%201%20recursion-0.45s-orange?style=for-the-badge" alt="2 to 1 recursion: 0.45s"></a>
+  <a href="#xmss-aggregation"><img src="https://img.shields.io/badge/Aggregation-1100%20XMSS%2Fs-brightgreen?style=for-the-badge"></a>
+  <a href="#sphincs-aggregation"><img src="https://img.shields.io/badge/Aggregation-200%20SPHINCS%2Fs-green?style=for-the-badge"></a>
+  <a href="#recursion"><img src="https://img.shields.io/badge/2%20to%201%20recursion-0.45s-orange?style=for-the-badge"></a>
 </p>
 
 Warning: highly experimental.
@@ -24,19 +25,35 @@ Machine: Mac M4 Max
 Our XMSS is specified in [XMSS.pdf](https://github.com/leanEthereum/leanVM-b/releases/download/doc-latest/XMSS.pdf).
 
 ```bash
-cargo run --release -- xmss --n-signatures 900 --log-inv-rate 1 --repeat 3
+cargo run --release -- aggregate --xmss 900 --log-inv-rate 1 --repeat 3
 ```
 
 ```
-XMSS aggregation, 900 signatures
-  cycles (VM steps)           : 1,542,617 = 2^20.557
-    proven rows               : 1,967,104 = 2^20.908  (filled to powers of two)
-    details                   : DEREF 2^18.988 (33.7%)  SET 2^18.402 (22.4%)  MUL 2^18.198 (19.5%)  BLAKE2S 2^16.995 (8.5%)  XOR 2^16.96 (8.3%)  JUMP 2^16.831 (7.6%)  PACK64X2 2^9.938 (0.1%)  MEMORY 2^21.725  TOTAL_COMMITTED 2^26.195
-  signers                     : 900
-  proof size                  : 304.4 KiB
-  aggregating                 : 0.816 s ± 4.2%      peak memory 13.815 GiB
-  per signature               : 1,102.621 XMSS/s
-  verifying                   : 0.0137 s
+aggregation, 900 XMSS signatures
+  cycles (VM steps)           : 1,542,871 = 2^20.557
+    details                   : DEREF 2^18.988 (33.7%)  SET 2^18.402 (22.4%)  MUL 2^18.199 (19.5%)  BLAKE2S 2^16.995 (8.5%)  XOR 2^16.961 (8.3%)  JUMP 2^16.843 (7.6%)  MEMORY 2^21.724  TOTAL_COMMITTED 2^26.195
+  proof size                  : 304.5 KiB
+  proving time                : 0.821 s ± 2.6%      peak memory 13.956 GiB
+  per signature               : 1,096.508 signatures/s
+  verifying                   : 0.0135 s
+```
+
+### SPHINCS aggregation
+
+Our SPHINCS is specified in [SPHINCS.pdf](https://github.com/leanEthereum/leanVM-b/releases/download/doc-latest/SPHINCS.pdf).
+
+```bash
+cargo run --release -- aggregate --sphincs 245 --log-inv-rate 1 --repeat 3
+```
+
+```
+aggregation, 245 SPHINCS signatures
+  cycles (VM steps)           : 2,677,883 = 2^21.353
+    details                   : DEREF 2^19.45 (26.7%)  XOR 2^19.306 (24.2%)  MUL 2^19.212 (22.7%)  SET 2^18.866 (17.8%)  BLAKE2S 2^16.996 (4.9%)  JUMP 2^16.568 (3.6%)  MEMORY 2^22.089  TOTAL_COMMITTED 2^26.875
+  proof size                  : 345.8 KiB
+  proving time                : 1.219 s ± 5.2%      peak memory 20.119 GiB
+  per signature               : 201.022 signatures/s
+  verifying                   : 0.0177 s
 ```
 
 ### Recursion
@@ -47,14 +64,12 @@ cargo run --release -- recursion --n 2 --xmss-per-leaf 900 --log-inv-rate 2 --re
 ```
 
 ```
-recursion 2→1, over leaves of 900 signatures
-  cycles (VM steps)           : 807,637 = 2^19.623
-    proven rows               : 1,179,648 = 2^20.17  (filled to powers of two)
-    details                   : DEREF 2^18.108 (35.0%)  MUL 2^17.876 (29.8%)  XOR 2^17.503 (23.0%)  SET 2^15.539 (5.9%)  JUMP 2^14.826 (3.6%)  BLAKE2S 2^14.437 (2.7%)  MEMORY 2^19.911  TOTAL_COMMITTED 2^24.856
-  signers                     : 1,800
-  proof size                  : 213.4 KiB
-  aggregating                 : 0.453 s ± 5.7%      peak memory 17.292 GiB
-  verifying                   : 0.016 s
+recursion 2→1, over leaves of 900 XMSS signatures
+  cycles (VM steps)           : 807,861 = 2^19.624
+    details                   : DEREF 2^18.109 (35.0%)  MUL 2^17.876 (29.8%)  XOR 2^17.503 (23.0%)  SET 2^15.539 (5.9%)  JUMP 2^14.826 (3.6%)  BLAKE2S 2^14.437 (2.7%)  MEMORY 2^19.911  TOTAL_COMMITTED 2^24.856
+  proof size                  : 212.7 KiB
+  proving time                : 0.453 s ± 4.9%      peak memory 17.287 GiB
+  verifying                   : 0.0161 s
 ```
 
 ### Fibonacci
@@ -66,32 +81,33 @@ cargo run --release -- fibonacci --n 2000000 --log-inv-rate 1 --repeat 3
 
 ```
 Fibonacci (in the exponent, i.e. modulo 2^64 - 1), N = 2,000,000
-  cycles (VM steps)           : 2,127,881
-    details                   : MUL 2^20.937 (98.7%)  DEREF 2^13.967 (0.8%)  SET 2^12.552 (0.3%) JUMP 2^10.968 (0.1%)  XOR 2^10.966 (0.1%)  MEMORY 2^20.964  TOTAL_COMMITTED 2^25.263
-  proof size                  : 284.7 KiB
-  proving                     : 0.41 s ± 2.9%   5,191,741 cycles/s      peak memory 7.482 GiB
-  verifying                   : 0.00352 s
+  cycles (VM steps)           : 2,127,880
+    details                   : MUL 2^20.937 (98.7%)  DEREF 2^13.967 (0.8%)  SET 2^12.552 (0.3%)  JUMP 2^10.968 (0.1%)  XOR 2^10.966 (0.1%)  MEMORY 2^20.964  TOTAL_COMMITTED 2^25.263
+  proof size                  : 286.2 KiB
+  proving                     : 0.425 s ± 6.9%   5,009,971 cycles/s      peak memory 7.523 GiB
+  verifying                   : 0.00315 s
 ```
 
 ### Batch proving BLAKE2s
 
 ```bash
-BENCH_REPEAT=3 BENCH_COOLDOWN=2 FLOCK_N_LOG=18 cargo test --release -p flock --test blake2s_batch -- --ignored --nocapture
+BENCH_REPEAT=3 BENCH_COOLDOWN=2 FLOCK_N_LOG=18 cargo test --release -p flock --test hash_batch -- --ignored --nocapture
 ```
 
 ```
 Flock BLAKE2s batch proving, 262,144 compressions (2^18 slots)
   setup (preprocessing, excluded) :      0.0 ms
-  witness-gen                     :     51.2 ms ± 23.3%   8.6%
-  commit                          :    100.1 ms ± 0.3%   16.8%
-  zerocheck                       :    237.0 ms ± 4.2%   39.7%
-  lincheck                        :     19.4 ms ± 10.8%   3.3%
-  pcs opening                     :    188.9 ms ± 7.1%   31.7%
+  witness-gen                     :     62.2 ms ± 29.8%  10.1%
+  commit                          :    100.2 ms ± 1.2%   16.3%
+  zerocheck                       :    234.8 ms ± 1.4%   38.3%
+  lincheck                        :     20.5 ms ± 7.7%    3.3%
+  pcs opening                     :    195.9 ms ± 3.4%   31.9%
   other                           :      0.0 ms           0.0%
   ------------------------------------------
-  prove TOTAL (witness excluded)  :    545.5 ms ± 3.9%   91.4%
+  prove TOTAL (witness excluded)  :    551.4 ms ± 1.9%   89.9%
   verify                          :      2.0 ms
-  throughput                      :        480,600 compressions/s ± 3.9%
+  throughput                      :        475,423 compressions/s ± 1.9%
+  (~3256.3 XMSS/s equivalent at 146 compressions/signature)
 ```
 
 ## Security

crates/lean_compiler/zkDSL.md

@@ -24,6 +24,7 @@ Machine **words** (the contents of a memory cell, an immediate, a hashed value,
 - an integer literal `n` supplies up to 128 raw bits and is embedded as `F192(c0, c1, 0)`. This is a source-syntax limit, not the machine-word width: words have three 64-bit limbs. Thus `5` is `1 + x^2`, not the integer five, and `2 ** 64` is the tower element `y`. Full-width constants use `f192(c0, c1, c2)`, with each limb an unsigned 64-bit compile-time integer,
 - `GEN` is the fixed generator `g = x` of the 64-bit subfield `K^×` (multiplicative order `2^64 − 1`),
 - `GEN ** e` is the compile-time constant `g^e ∈ K` (`**` takes base `GEN` and a compile-time integer exponent: a literal, a constant, an `unroll` variable, `len(...)`, or index arithmetic of those). So `buf[GEN ** i]` names heap cell `i` directly inside an `unroll` loop, with no running-pointer cursor.
+- constant arithmetic means different things in the two positions, and this is a silent trap: `a + b` on two constants is **integer** addition in an index, a bound or a keyword (`buf[GEN ** (i + 1)]`, `unroll(0, n + 1)`, `counter=64 * (q + 1)`), and **XOR** in a value, where `1 + 1` is `0`. So a literal built in a value position must not add overlapping integers: `tweak = base + (level + 1) * SHIFT` drops the whole term on odd levels. Products are safe (an integer times a power of two is that shift, as long as the top bit stays inside the limb); to add, index a literal table with the integer arithmetic instead, `LEVELS[level + 1]`.
 - `base ** e` with a **non-`GEN`** base and a compile-time exponent `e` is square-and-multiply: integer arithmetic in an index/bound position (`2 ** c`), or field arithmetic in a value position (`x ** k`, e.g. a loop counter `g^i` raised to a stride to reach cell `i·stride`). The base may be runtime.
 
 A logical **index** `i` is carried as `g^i` in the 64-bit subfield (order `2^64 − 1`): incrementing is one multiplication by `GEN`, and memory/bytecode addresses are g-powers. This is the design idiom of the whole VM: loops, heap addressing, and range checks below all live in the exponent, in `K`.

crates/lean_vm/src/cpu/mod.rs

@@ -428,7 +428,7 @@ fn blake2s_value_slot(col: usize) -> Option<usize> {
 /// committed witness size, the sum of the column lengths, i.e. the real data
 /// before the stacked witness is zero-padded to a power of two `2^m`.
 pub struct Stats {
-    pub cycles: usize,
+    pub cycles: usize, // including the padding to make every instruction count a power of two
     /// Rows per table as proven: each an exact power of two, the fill blocks having
     /// filled them (`filler`).
     pub counts: [usize; tables::N_TABLES],

crates/rec_aggregation/Cargo.toml

@@ -14,6 +14,7 @@ flock.workspace = true
 lean_vm.workspace = true
 lean_compiler.workspace = true
 xmss.workspace = true
+sphincs.workspace = true
 rand.workspace = true
 bincode.workspace = true
 serde.workspace = true