xmss: scaffolding for the signature spec

Author: tcoratger

src/lean_spec/subspecs/xmss/constants.py

@@ -9,7 +9,7 @@
 MESSAGE_LENGTH: int = 32
 """The length in bytes for all messages to be signed."""
 
-LOG_LIFETIME: int = 32
+LOG_LIFETIME: int = 18
 """The base-2 logarithm of the scheme's maximum lifetime."""
 
 LIFETIME: int = 1 << LOG_LIFETIME
@@ -19,6 +19,7 @@
 An individual key pair can be active for a smaller sub-range.
 """
 
+
 # =================================================================
 # Target Sum WOTS Parameters
 # =================================================================
@@ -29,12 +30,12 @@
 BASE: int = 8
 """The alphabet size for the digits of the encoded message."""
 
+FINAL_LAYER: int = 77
+"""The number of top layers of the hypercube to map the hash output into."""
+
 TARGET_SUM: int = 375
 """The required sum of all codeword chunks for a signature to be valid."""
 
-CHUNK_SIZE: int = 3
-"""The number of bits per chunk, calculated as ceil(log2(BASE))."""
-
 
 # =================================================================
 # Hash and Encoding Length Parameters (in field elements)
@@ -44,27 +45,33 @@
 """
 The length of the public parameter `P`.
 
-It isused to specialize the hash function.
+It is used to specialize the hash function.
 """
 
-HASH_LEN: int = 8
-"""The output length of the main tweakable hash function."""
-
-RAND_LEN: int = 7
-"""The length of the randomness `rho` used during message encoding."""
-
-TWEAK_LEN: int = 2
+TWEAK_LEN_FE: int = 2
 """The length of a domain-separating tweak."""
 
-MSG_LEN: int = 9
+MSG_LEN_FE: int = 9
 """The length of a message after being encoded into field elements."""
 
-MSG_HASH_LEN: int = 15
-"""The output length of the hash function used to digest the message."""
+RAND_LEN_FE: int = 6
+"""The length of the randomness `rho` used during message encoding."""
+
+HASH_LEN_FE: int = 7
+"""The output length of the main tweakable hash function."""
 
 CAPACITY: int = 9
 """The capacity of the Poseidon2 sponge, defining its security level."""
 
+POS_OUTPUT_LEN_PER_INV_FE: int = 15
+"""Output length per invocation for the message hash."""
+
+POS_INVOCATIONS: int = 1
+"""Number of invocations for the message hash."""
+
+POS_OUTPUT_LEN_FE: int = POS_OUTPUT_LEN_PER_INV_FE * POS_INVOCATIONS
+"""Total output length for the message hash."""
+
 
 # =================================================================
 # Domain Separator Prefixes for Tweaks

src/lean_spec/subspecs/xmss/interface.py

@@ -1,17 +1,16 @@
 """
 Defines the core interface for the Generalized XMSS signature scheme.
 
-This file specifies the high-level functions (`key_gen`, `sign`, `verify`)
+Specification for the high-level functions (`key_gen`, `sign`, `verify`)
 that constitute the public API of the signature scheme. For the purpose of this
 specification, these are defined as placeholders with detailed documentation.
 """
 
-from typing import List, Tuple
+from __future__ import annotations
+
+from typing import Tuple
 
-from ..koalabear import Fp
-from .constants import BASE, CHUNK_SIZE, DIMENSION, LIFETIME, MESSAGE_LENGTH
 from .structures import PublicKey, SecretKey, Signature
-from .utils import chain, encode, hash_tree_verify, tweakable_hash
 
 
 def key_gen() -> Tuple[PublicKey, SecretKey]:
@@ -55,34 +54,46 @@ def sign(sk: SecretKey, epoch: int, message: bytes) -> Signature:
 
 
 def verify(pk: PublicKey, epoch: int, message: bytes, sig: Signature) -> bool:
+    r"""
+    Verifies a digital signature against a public key, message, and epoch.
+
+    This function is a placeholder. The complete verification logic is detailed
+    below and will be implemented in a future update.
+
+    ### Verification Algorithm
+
+    1.  **Re-encode Message**: The verifier uses the randomness `rho` from the
+        signature to re-compute the codeword $x = (x_1, \dots, x_v)$ from the
+        message `m`. This includes calculating the checksum or checking the target sum.
+
+    2.  **Reconstruct One-Time Public Key**: For each intermediate hash `y_i`
+        in the signature, the verifier completes the corresponding hash chain.
+        Since `y_i` was computed with $x_i$ steps, the verifier applies the
+        hash function an additional $w - 1 - x_i$ times to arrive at the
+        one-time public key component `otpk_{ep,i}`.
+
+    3.  **Compute Merkle Leaf**: The verifier hashes the reconstructed one-time
+        public key components to compute the expected Merkle leaf for `epoch`.
+
+    4.  **Verify Merkle Path**: The verifier uses the `path` from the signature
+        to compute a candidate Merkle root starting from the computed leaf.
+        Verification succeeds if and only if this candidate root matches the
+        `root` in the `PublicKey`.
+
+    Args:
+        pk: The public key to verify against.
+        epoch: The epoch the signature corresponds to.
+        message: The message that was supposedly signed.
+        sig: The signature object to be verified.
+
+    Returns:
+        `True` if the signature is valid, `False` otherwise.
+
+    For the formal specification of this process, please refer to:
+    - "Hash-Based Multi-Signatures for Post-Quantum Ethereum" [DKKW25a]
+    - "Technical Note: LeanSig for Post-Quantum Ethereum" [DKKW25b]
+    - The canonical Rust implementation: https://github.com/b-wagn/hash-sig
     """
-    Verifies a digital signature against:
-        - a public key,
-        - a message,
-        - epoch.
-    """
-    assert len(message) == MESSAGE_LENGTH, "Invalid message length"
-    assert 0 <= epoch < LIFETIME, "Epoch out of valid range"
-
-    # Re-encode the message to get the expected codeword.
-    codeword = encode(pk.parameter, message, sig.rho, epoch)
-    if codeword is None:
-        return False
-
-    # Reconstruct the one-time public key from the signature's hashes.
-    chain_ends: List[List[Fp]] = []
-    for i in range(DIMENSION):
-        steps_to_end = (BASE**CHUNK_SIZE - 1) - codeword[i]
-        end_of_chain = chain(
-            pk.parameter, epoch, i, codeword[i], steps_to_end, sig.hashes[i]
-        )
-        chain_ends.append(end_of_chain)
-
-    # Compute the Merkle leaf by hashing the reconstructed one-time public key.
-    # Note: A proper tweak would be used here. For simplicity, we omit it.
-    computed_leaf = tweakable_hash(pk.parameter, [], chain_ends)
-
-    # Verify the Merkle path against the public key's root.
-    return hash_tree_verify(
-        pk.parameter, pk.root, epoch, computed_leaf, sig.path
+    raise NotImplementedError(
+        "verify will be implemented in a future update to the specification."
     )

src/lean_spec/subspecs/xmss/structures.py

@@ -5,7 +5,7 @@
 from pydantic import BaseModel, ConfigDict, Field
 
 from ..koalabear import Fp
-from .constants import HASH_LEN, PARAMETER_LEN, RAND_LEN
+from .constants import HASH_LEN_FE, PARAMETER_LEN, RAND_LEN_FE
 
 
 class HashTreeOpening(BaseModel):
@@ -26,7 +26,7 @@ class PublicKey(BaseModel):
     """The public key for the Generalized XMSS scheme."""
 
     model_config = ConfigDict(frozen=True, arbitrary_types_allowed=True)
-    root: List[Fp] = Field(..., max_length=HASH_LEN, min_length=HASH_LEN)
+    root: List[Fp] = Field(..., max_length=HASH_LEN_FE, min_length=HASH_LEN_FE)
     parameter: List[Fp] = Field(
         ..., max_length=PARAMETER_LEN, min_length=PARAMETER_LEN
     )
@@ -37,7 +37,7 @@ class Signature(BaseModel):
 
     model_config = ConfigDict(frozen=True, arbitrary_types_allowed=True)
     path: HashTreeOpening
-    rho: List[Fp] = Field(..., max_length=RAND_LEN, min_length=RAND_LEN)
+    rho: List[Fp] = Field(..., max_length=RAND_LEN_FE, min_length=RAND_LEN_FE)
     hashes: List[List[Fp]]