Sphincs FV

.github/workflows/lean.yml

@@ -24,10 +24,10 @@ jobs:
       - name: Forbid proof escapes
         run: |
           ! grep -rnE '\b(sorry|sorryAx|admit|native_decide|unsafe|implemented_by)\b|#exit' \
-              --include='*.lean' formal/xmss | grep -vE ':[0-9]+: *(--|/-)'
+              --include='*.lean' --exclude-dir=.lake formal/xmss | grep -vE ':[0-9]+: *(--|/-)'
       # Installs the toolchain from `formal/xmss/lean-toolchain`, fetches the
       # mathlib cache, and runs `lake build` on the default target, which
-      # elaborates the root module and with it both `#guard_msgs` checks. The
+      # elaborates the root module and with it the `#guard_msgs` check. The
       # checked-in manifest is used as is: no `lake update`.
       - uses: leanprover/lean-action@v1
         with:
@@ -47,3 +47,27 @@ jobs:
         with:
           name: xmss-axioms
           path: ${{ runner.temp }}/axioms.txt
+
+  sphincs-formalization:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+      - name: Forbid proof escapes
+        run: |
+          ! grep -rnE '\b(sorry|sorryAx|admit|native_decide|unsafe|implemented_by)\b|#exit' \
+              --include='*.lean' --exclude-dir=.lake formal/sphincs | grep -vE ':[0-9]+: *(--|/-)'
+      - uses: leanprover/lean-action@v1
+        with:
+          lake-package-directory: formal/sphincs
+      - name: Check the axiom footprint
+        working-directory: formal/sphincs
+        run: |
+          printf 'import SphincsSecurity\n#print axioms SphincsSecurity.sphincs_has_127_bits_of_classical_security\n' \
+            > "$RUNNER_TEMP/axioms.lean"
+          lake env lean "$RUNNER_TEMP/axioms.lean" | tee "$RUNNER_TEMP/axioms.txt"
+          grep -qF "'SphincsSecurity.sphincs_has_127_bits_of_classical_security' depends on axioms: [propext, Classical.choice, Quot.sound]" \
+            "$RUNNER_TEMP/axioms.txt"
+      - uses: actions/upload-artifact@v4
+        with:
+          name: sphincs-axioms
+          path: ${{ runner.temp }}/axioms.txt

AGENTS.md

@@ -7,7 +7,7 @@ A minimal virtual machine and recursive SNARK for signature aggregation and blob
 - `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), `c` (Flock), and `d` (novel basis and additive NTT), 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 XMSS specification; `crates/xmss` implements its hash inputs and signature verification.
 - `doc/sphincs/` is the standalone specification of the concrete SPHINCS+ instance used where statelessness matters; its root is `doc/sphincs/main.tex`, built the same way as `doc/xmss`, and implemented by `crates/sphincs`. It uses the same BLAKE2s primitive and target-sum encoding shape as XMSS, with its own tweak layout, target sum, and signing search.
-- `formal/xmss/` is a Lean 4 proof (over VCVio) of the ideal XMSS scheme'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/` and `formal/sphincs/` are Lean 4 proofs (over VCVio) of the ideal schemes' classical random-oracle security, `xmss_has_127_bits_of_classical_security` and `sphincs_has_127_bits_of_classical_security`. Each project's `Statement.lean`, under `XmssSecurity/` or `SphincsSecurity/`, contains 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 repeated opcodes hash arbitrary byte strings by carrying the chaining value and setting the counter and final flag for each block.
 - `crates/lean_compiler/zkDSL.md` documents the (pythonic) zkDSL (that compiles to the ISA that our VM runs, and that our snark proves).
 

README.md

@@ -18,7 +18,7 @@
   </tr>
   <tr>
     <td><a href="#sphincs-aggregation">leanSPHINCS aggregation</a></td>
-    <td align="right"><b>250/s</b></td>
+    <td align="right"><b>280/s</b></td>
   </tr>
   <tr>
     <td><a href="#data-availability">leanDA commitment</a></td>
@@ -95,12 +95,12 @@ cargo run --release -- aggregate --sphincs 245 --log-inv-rate 1 --repeat 3
 
 ```
 aggregation, 245 SPHINCS signatures
-  cycles (VM steps)           : 2,351,886 = 2^21.165
-    details                   : XOR 2^19.239 (26.3%)  MUL 2^19.222 (26.0%)  SET 2^18.833 (19.9%)  DEREF 2^18.711 (18.2%)  BLAKE2S 2^16.992 (5.5%)  JUMP 2^16.543 (4.1%)  MEMORY 2^21.679  TOTAL_COMMITTED 2^26.553
-  proof size                  : 313.8 KiB
-  proving time                : 0.972 s ± 3.4%      peak memory 11.476 GiB
-  per signature               : 252.028 signatures/s
-  verifying                   : 3.969 ms
+  cycles (VM steps)           : 2,132,425 = 2^21.024
+    details                   : XOR 2^18.951 (23.8%)  MUL 2^18.93 (23.4%)  SET 2^18.847 (22.1%)  DEREF 2^18.711 (20.1%)  BLAKE2S 2^16.992 (6.1%)  JUMP 2^16.543 (4.5%)  MEMORY 2^21.564  TOTAL_COMMITTED 2^26.301
+  proof size                  : 300.1 KiB
+  proving time                : 0.861 s ± 1.5%      peak memory 9.348 GiB
+  per signature               : 284.603 signatures/s
+  verifying                   : 3.841 ms
 ```
 
 ### data availability

crates/rec_aggregation/guests/lean_ethereum.py

@@ -380,30 +380,21 @@
 # them, so the buffer holds three lanes and the top 16 are never read.
 SP_BIT_LANES = 3
 SP_BIT_CELLS = SP_BIT_LANES * BASE_FIELD_BITS
-# Tweak types (the tweak's first byte). Types 0 and 5 are the seed derivation's,
-# which is a signer's own business: nothing in-circuit ever verifies one.
-SP_TW_PRF = 0
-SP_TW_CHAIN = 1
-SP_TW_LEAF = 2
-SP_TW_NODE = 3
-SP_TW_ENC = 4
-SP_TW_FTS_PRF = 5
-SP_TW_FTS_LEAF = 6
-SP_TW_FTS_NODE = 7
-SP_TW_FTS_ROOTS = 8
-SP_TW_MSG = 9
-# enc(t, lay, tau, p, j) packs t at bit 0, lay at 8, tau at 16, p at 48 and j at
-# 80, fourteen bytes of fields and two of padding. Every field this instance uses
-# is small enough that none straddles the 64-bit lane boundary (tau < 2^26 at bit
-# 16, p <= 334 at bit 48, j < 2^12 at bit 80), so a tweak cell is
-# `t + lay*2^8 + tau*2^16 + p*2^48` in lane 0 plus `j*2^16` in lane 1, and every
-# term is one field addition. SP_TAU_POS and SP_J_POS are where a bit of tau or of
-# j weighs in the coordinate basis, the j position already carrying the lane, so
-# nothing has to be multiplied by Y afterwards.
-SP_LAY_MUL = 2 ** 8
-SP_P_MUL = 2 ** 48
-SP_TAU_POS = 16
-SP_J_POS = BASE_FIELD_BITS + 16
+# Native tweak prefixes, including the protocol domain separator and type.
+SP_TW_CHAIN = SP_TW_CHAIN_PLACEHOLDER
+SP_TW_LEAF = SP_TW_LEAF_PLACEHOLDER
+SP_TW_NODE = SP_TW_NODE_PLACEHOLDER
+SP_TW_ENC = SP_TW_ENC_PLACEHOLDER
+SP_TW_FTS_LEAF = SP_TW_FTS_LEAF_PLACEHOLDER
+SP_TW_FTS_NODE = SP_TW_FTS_NODE_PLACEHOLDER
+SP_TW_FTS_ROOTS = SP_TW_FTS_ROOTS_PLACEHOLDER
+SP_TW_MSG = SP_TW_MSG_PLACEHOLDER
+# Tweak layout: protocol_domain_sep | type | layer | zero | p | tree | index.
+# Each 32-bit field stays within one 64-bit lane.
+SP_LAY_MUL = 2 ** 16
+SP_P_MUL = 2 ** 32
+SP_TAU_POS = BASE_FIELD_BITS
+SP_J_POS = BASE_FIELD_BITS + 32
 SP_CHAIN_MUL = SP_CHAIN_LENGTH * SP_P_MUL   # chain i's tweaks start at p = 2^w * i
 # The encoding counter, LE_32 in the low four bytes of its cell: bounded by
 # decomposing exactly that many bits, so the guest accepts no preimage the native
@@ -2450,13 +2441,19 @@ def verify_sig_sphincs(signer):
         secret = StackBuf(WORDS_PER_BLOCK)
         hint_witness(secret[0:1], "sp_fts_secrets")
         fts_leaf = StackBuf(WORDS_PER_BLOCK)
-        blake2s([SP_TW_FTS_LEAF + kappa * SP_LAY_MUL + idx_tau + sp_bit_field(bits, leaf_off, SP_A, SP_J_POS), pp], [secret[0], 0], fts_leaf, counter=48, final=1)
+        node_index = sp_bit_field(bits, leaf_off, SP_A, SP_J_POS)
+        blake2s([SP_TW_FTS_LEAF + kappa * SP_LAY_MUL + idx_tau + node_index, pp], [secret[0], 0], fts_leaf, counter=48, final=1)
         node = fts_leaf[0]
         for level in unroll(0, SP_A):
             sibling = hint_witness("sp_fts_paths")
             children = order_children(node, sibling, bits[GEN ** (leaf_off + level)])
             parent = StackBuf(WORDS_PER_BLOCK)
-            blake2s([SP_TW_FTS_NODE + kappa * SP_LAY_MUL + const((level + 1) * SP_P_MUL) + idx_tau + sp_bit_field(bits, leaf_off + level + 1, SP_A - level - 1, SP_J_POS), pp], children, parent)
+            if const(level + 1 == SP_A):
+                node_index = 0
+            else:
+                # The index fits in one lane; clearing its low bit makes division by GEN a right shift.
+                node_index = (node_index + bits[GEN ** (leaf_off + level)] * COORD_BASIS[SP_J_POS]) / GEN
+            blake2s([SP_TW_FTS_NODE + kappa * SP_LAY_MUL + const((level + 1) * SP_P_MUL) + idx_tau + node_index, pp], children, parent)
             node = parent[0]
         roots[kappa] = node
     fts_key = StackBuf(WORDS_PER_BLOCK)
@@ -2474,13 +2471,18 @@ def verify_sig_sphincs(signer):
         lay = SP_D - 1 - step
         leaf_index_off = SP_SUFFIX[lay + 1]
         tau_field = sp_bit_field(bits, SP_SUFFIX[lay], SP_H - SP_SUFFIX[lay], SP_TAU_POS)
-        tw_pos = tau_field + sp_bit_field(bits, leaf_index_off, SP_HEIGHTS[lay], SP_J_POS) + lay * SP_LAY_MUL
+        node_index = sp_bit_field(bits, leaf_index_off, SP_HEIGHTS[lay], SP_J_POS)
+        tw_pos = tau_field + node_index + lay * SP_LAY_MUL
         node = sp_ots_leaf(tw_pos, pp, signed)
         for level in unroll(0, SP_HEIGHTS[lay]):
             sibling = hint_witness("sp_siblings")
             children = order_children(node, sibling, bits[GEN ** (leaf_index_off + level)])
             parent = StackBuf(WORDS_PER_BLOCK)
-            blake2s([SP_TW_NODE + lay * SP_LAY_MUL + const((level + 1) * SP_P_MUL) + tau_field + sp_bit_field(bits, leaf_index_off + level + 1, SP_HEIGHTS[lay] - level - 1, SP_J_POS), pp], children, parent)
+            if const(level + 1 == SP_HEIGHTS[lay]):
+                node_index = 0
+            else:
+                node_index = (node_index + bits[GEN ** (leaf_index_off + level)] * COORD_BASIS[SP_J_POS]) / GEN
+            blake2s([SP_TW_NODE + lay * SP_LAY_MUL + const((level + 1) * SP_P_MUL) + tau_field + node_index, pp], children, parent)
             node = parent[0]
         signed = node
     assert signed == signer[1]

crates/rec_aggregation/src/aggregation.rs

@@ -148,11 +148,10 @@ const _: () = assert!((2 + sphincs::NUM_FTS_TREES).is_multiple_of(4));
 // dynamically sized `HeapBuf` gets no compile-time index check, so a wider
 // digest would read leaf indices from cells nothing writes.
 const _: () = assert!(sphincs::DIGEST_BITS <= 3 * 64);
-// Every tweak field the guest packs must stay inside the byte range the native
-// `enc` gives it: `tau` at bit 16 below `p` at 48, `p` below the 64-bit lane
-// boundary, and `j` inside its four bytes at bit 80.
+// The guest packs each tweak field into its own 32-bit word: p at bit 32,
+// tau at bit 64, and j at bit 96.
 const _: () = assert!(sphincs::H <= 32);
-const _: () = assert!(sphincs::CHAIN_LEN * sphincs::V < 1 << 16);
+const _: () = assert!(sphincs::CHAIN_LEN * sphincs::V < 1 << 32);
 const _: () = assert!(sphincs::A <= 32 && sphincs::HEIGHTS[0] <= 32);
 
 /// A count as the guest carries it: in the exponent, `g^n`.
@@ -263,10 +262,9 @@ fn tweak_cell(tweak_type: u8, sub_position: u32) -> F192 {
 
 /// What bit `b` of the epoch weighs in a tweak's index field, so an index is its
 /// set bits summed. The one property of the layout this assumes is that the
-/// index field is linear in the index, which a leaf proof at the benchmark epoch
-/// exercises for every bit.
+/// index field is linear in the index. Subtract the constant protocol prefix.
 fn tweak_index_weight(b: usize) -> F192 {
-    pack_16_bytes(&xmss::make_tweak(0, 0, 1 << b))
+    pack_16_bytes(&xmss::make_tweak(0, 0, 1 << b)) + pack_16_bytes(&xmss::make_tweak(0, 0, 0))
 }
 /// The signer-set digest: plain BLAKE2s of one byte string, laid out in whole
 /// 64-byte blocks so the guest can absorb it four cells at a time
@@ -3002,7 +3000,7 @@ fn placeholder_map(kbc: usize) -> BTreeMap<String, String> {
 
     // The SPHINCS instance. Its tweaks are derived per signature from the index
     // the message digest picks, where XMSS's come from one public epoch, so the
-    // guest needs only the shape.
+    // guest receives the shape and the native tweak prefixes.
     let dsl_list = |values: &[usize]| {
         let inner: Vec<String> = values.iter().map(usize::to_string).collect();
         format!("[{}]", inner.join(", "))
@@ -3016,6 +3014,21 @@ fn placeholder_map(kbc: usize) -> BTreeMap<String, String> {
     ps("SP_H", sphincs::H.to_string());
     ps("SP_HEIGHTS", dsl_list(&sphincs::HEIGHTS));
     ps("SP_SUFFIX", dsl_list(&sphincs::SUFFIX));
+    for (name, tag) in [
+        ("SP_TW_CHAIN", sphincs::TWEAK_CHAIN),
+        ("SP_TW_LEAF", sphincs::TWEAK_LEAF),
+        ("SP_TW_NODE", sphincs::TWEAK_NODE),
+        ("SP_TW_ENC", sphincs::TWEAK_ENC),
+        ("SP_TW_FTS_LEAF", sphincs::TWEAK_FTS_LEAF),
+        ("SP_TW_FTS_NODE", sphincs::TWEAK_FTS_NODE),
+        ("SP_TW_FTS_ROOTS", sphincs::TWEAK_FTS_ROOTS),
+        ("SP_TW_MSG", sphincs::TWEAK_MSG),
+    ] {
+        ps(
+            name,
+            dsl_u128(pack_16_bytes(&sphincs::tweak(tag, 0, 0, 0, 0))).to_string(),
+        );
+    }
     rep
 }
 
@@ -3228,6 +3241,64 @@ mod tests {
         aggregate(&[], at_epoch(signers, XMSS_EPOCH_A), vec![], &[], None, LOG_INV_RATE).expect("leaf aggregates")
     }
 
+    #[test]
+    fn keygen_and_verification_hash_domains_are_disjoint() {
+        let xmss_tags = [
+            xmss::TWEAK_TYPE_PRF,
+            xmss::TWEAK_TYPE_CHAIN,
+            xmss::TWEAK_TYPE_WOTS_PK,
+            xmss::TWEAK_TYPE_MERKLE,
+            xmss::TWEAK_TYPE_ENCODING,
+            xmss::TWEAK_TYPE_PARAMETER,
+            xmss::TWEAK_TYPE_FILLER,
+        ];
+        let sphincs_tags = [
+            sphincs::TWEAK_PRF,
+            sphincs::TWEAK_CHAIN,
+            sphincs::TWEAK_LEAF,
+            sphincs::TWEAK_NODE,
+            sphincs::TWEAK_ENC,
+            sphincs::TWEAK_FTS_PRF,
+            sphincs::TWEAK_FTS_LEAF,
+            sphincs::TWEAK_FTS_NODE,
+            sphincs::TWEAK_FTS_ROOTS,
+            sphincs::TWEAK_MSG,
+            sphincs::TWEAK_PARAMETER,
+        ];
+        let domains: BTreeSet<_> = xmss_tags
+            .into_iter()
+            .map(|tag| xmss::make_tweak(tag, 0, 0))
+            .chain(sphincs_tags.into_iter().map(|tag| sphincs::tweak(tag, 0, 0, 0, 0)))
+            .collect();
+        assert_eq!(domains.len(), xmss_tags.len() + sphincs_tags.len());
+    }
+
+    #[test]
+    fn signature_tweaks_align_with_distinct_domains() {
+        for (xmss_tag, sphincs_tag) in [
+            (xmss::TWEAK_TYPE_CHAIN, sphincs::TWEAK_CHAIN),
+            (xmss::TWEAK_TYPE_WOTS_PK, sphincs::TWEAK_LEAF),
+            (xmss::TWEAK_TYPE_MERKLE, sphincs::TWEAK_NODE),
+            (xmss::TWEAK_TYPE_ENCODING, sphincs::TWEAK_ENC),
+        ] {
+            for position in [0, 1, u32::MAX] {
+                for index in [0, 1, 3, 0xa0b0_c0d0, u32::MAX] {
+                    let xmss_tweak = xmss::make_tweak(xmss_tag, position, index);
+                    let sphincs_tweak = sphincs::tweak(sphincs_tag, 0, 0, position, index);
+                    assert_eq!(&xmss_tweak[1..], &sphincs_tweak[1..]);
+                    assert_ne!(xmss_tweak[0], sphincs_tweak[0]);
+                    let mut guest_tweak = tweak_cell(xmss_tag, position);
+                    for bit in 0..32 {
+                        if index & (1 << bit) != 0 {
+                            guest_tweak += tweak_index_weight(bit);
+                        }
+                    }
+                    assert_eq!(guest_tweak, pack_16_bytes(&xmss_tweak));
+                }
+            }
+        }
+    }
+
     type RawSphincs = (SphincsPublicKey, sphincs::Message, SphincsSignature);
 
     fn prove_sphincs_leaf(signers: &[RawSphincs]) -> EthereumProof {
@@ -3318,7 +3389,7 @@ mod tests {
             .into_iter()
             .map(|tag| {
                 let signed: sphincs::Message = std::array::from_fn(|i| tag.wrapping_mul(i as u8 + 1));
-                let signature = sphincs::sign(&mut rng, &secret_key, &signed).expect("signs");
+                let signature = sphincs::sign(&secret_key, &signed).expect("signs");
                 (public_key, signed, signature)
             })
             .collect();

crates/rec_aggregation/src/signers_cache.rs

@@ -21,7 +21,7 @@ use xmss::*;
 
 type CachedSignature = (XmssPublicKey, XmssSignature);
 
-const SCHEMA_VERSION: u32 = 2;
+const SCHEMA_VERSION: u32 = 3;
 
 /// The epoch `get_signers` signs at. SPHINCS has none.
 pub const XMSS_EPOCH_A: Epoch = 3_000_000_007;
@@ -53,13 +53,7 @@ fn compute_signer(index: usize, epoch: Epoch) -> CachedSignature {
     let mut seed = [10u8; 32];
     seed[..8].copy_from_slice(&(index as u64).to_le_bytes());
     let (sk, pk) = xmss::key_gen_from_seed(seed, KEY_START, KEY_END).expect("keygen");
-    let sig = xmss::sign(
-        &mut StdRng::seed_from_u64(index as u64),
-        &sk,
-        &message_for(epoch),
-        epoch,
-    )
-    .expect("sign");
+    let sig = xmss::sign(&sk, &message_for(epoch), epoch).expect("sign");
     (pk, sig)
 }
 
@@ -207,7 +201,7 @@ fn compute_sphincs_signer(index: usize) -> CachedSphincsSignature {
     let mut rng = StdRng::seed_from_u64(0x5F1A_C500 ^ index as u64);
     let (secret_key, public_key) = sphincs::key_gen(&mut rng);
     let message = sphincs_message(index);
-    let signature = sphincs::sign(&mut rng, &secret_key, &message).expect("sign");
+    let signature = sphincs::sign(&secret_key, &message).expect("sign");
     (public_key, message, signature)
 }
 
@@ -220,6 +214,7 @@ fn sphincs_footprint() -> u64 {
     sphincs_message(0).hash(&mut hasher);
     sphincs_message(1).hash(&mut hasher);
     (
+        sphincs::MASTER_SECRET_LEN,
         sphincs::V,
         sphincs::W,
         sphincs::TARGET_SUM,

crates/sphincs/src/fts.rs

@@ -18,7 +18,7 @@ pub struct FtsOpening {
 }
 
 /// `s_{idx,kappa,j} = Th(P, tw_ftsprf(idx,kappa,j), S)`.
-fn fts_secret(pp: &PublicParam, master: &Digest, idx: u64, kappa: usize, j: usize) -> Digest {
+fn fts_secret(pp: &PublicParam, master: &MasterSecret, idx: u64, kappa: usize, j: usize) -> Digest {
     th(pp, &tweak(TWEAK_FTS_PRF, kappa, idx as u32, 0, j as u32), master)
 }
 
@@ -38,7 +38,7 @@ fn fts_key_of_roots(pp: &PublicParam, idx: u64, roots: &[Digest; NUM_FTS_TREES])
 
 /// `Fts.key` and `Fts.open` together, the forest being built once. `u[k-1]` is
 /// ignored: its tree is the dropped one.
-pub fn fts_open(pp: &PublicParam, master: &Digest, idx: u64, u: &[u32; K]) -> (Digest, FtsOpening) {
+pub fn fts_open(pp: &PublicParam, master: &MasterSecret, idx: u64, u: &[u32; K]) -> (Digest, FtsOpening) {
     let mut opening = FtsOpening {
         secrets: [[0; N]; NUM_FTS_TREES],
         paths: [[[0; N]; A]; NUM_FTS_TREES],