Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
34 changes: 19 additions & 15 deletions src/lean_spec/spec/crypto/xmss/constants.py
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
import math
from typing import Final, Self

from pydantic import model_validator
from pydantic import Field, model_validator

from lean_spec.base import StrictBaseModel
from lean_spec.config import LEAN_ENV
Expand All @@ -15,55 +15,59 @@
class XmssConfig(StrictBaseModel):
"""A model holding the configuration constants for an XMSS preset."""

LOG_LIFETIME: int
LOG_LIFETIME: int = Field(gt=0)
"""Base-2 logarithm of the scheme's maximum lifetime, the Merkle tree height."""

DIMENSION: int
DIMENSION: int = Field(gt=0)
"""Number of hash chains per signature, v.
Security-derived: it sets how many codeword chunks a signature commits to."""

BASE: int
BASE: int = Field(gt=0)
"""Alphabet size for the digits of the encoded message, the Winternitz parameter."""

Z: int
Z: int = Field(gt=0)
"""Number of base-BASE digits extracted from each field element."""

Q: int
Q: int = Field(gt=0)
"""Quotient fixing the digit decomposition, constrained by Q * BASE^Z == P - 1."""

TARGET_SUM: int
TARGET_SUM: int = Field(gt=0)
"""Required sum of all codeword chunks for a signature to be valid.
Security-derived: it tunes the forgery resistance of the encoding."""

MAX_TRIES: int
MAX_TRIES: int = Field(gt=0)
"""Maximum resampling attempts when searching for a codeword that meets the target sum.
Performance knob: a higher cap trades signing time for fewer hard failures."""

PARAMETER_LENGTH: int
PARAMETER_LENGTH: int = Field(gt=0)
"""Length of the public parameter P, in field elements."""

TWEAK_LENGTH_FIELD_ELEMENTS: int
TWEAK_LENGTH_FIELD_ELEMENTS: int = Field(gt=0)
"""Length of a domain-separating tweak, in field elements."""

MESSAGE_LENGTH_FIELD_ELEMENTS: int
MESSAGE_LENGTH_FIELD_ELEMENTS: int = Field(gt=0)
"""Length of a message after being encoded into field elements."""

RAND_LENGTH_FIELD_ELEMENTS: int
RAND_LENGTH_FIELD_ELEMENTS: int = Field(gt=0)
"""Length of the randomness rho used during message encoding, in field elements."""

HASH_LENGTH_FIELD_ELEMENTS: int
HASH_LENGTH_FIELD_ELEMENTS: int = Field(gt=0)
"""Output length of the main tweakable hash function, in field elements.
Security-derived: it sets the collision resistance of every digest."""

CAPACITY: int
CAPACITY: int = Field(gt=0)
"""Capacity of the Poseidon sponge, in field elements.
Security-derived: the capacity sets the sponge's security level."""

@model_validator(mode="after")
def _validate_decomposition(self) -> Self:
"""Verify that Q * BASE^Z == P - 1."""
"""Verify that Q * BASE^Z == P - 1 and that LOG_LIFETIME is even."""
if self.Q * self.BASE**self.Z != P - 1:
raise ValueError(f"Q * BASE^Z must equal P-1={P - 1}")
# The key splits into a top tree and bottom trees.
# Each covers LOG_LIFETIME / 2 levels, so the lifetime exponent must be even.
if self.LOG_LIFETIME % 2 != 0:
raise ValueError(f"LOG_LIFETIME must be even, got {self.LOG_LIFETIME}")
return self

@property
Expand Down
32 changes: 32 additions & 0 deletions tests/spec/crypto/xmss/test_constants.py
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,38 @@ def test_decomposition_validator_accepts_valid_product() -> None:
assert config.Q * config.BASE**config.Z == P - 1


def test_non_positive_field_is_rejected() -> None:
"""A field constrained to be positive rejects a zero value at construction."""
kwargs = _valid_config_kwargs()
kwargs["DIMENSION"] = 0
with pytest.raises(ValueError) as exception_info:
XmssConfig(**kwargs)
assert str(exception_info.value) == (
"1 validation error for XmssConfig\n"
"DIMENSION\n"
" Input should be greater than 0 "
"[type=greater_than, input_value=0, input_type=int]\n"
" For further information visit "
"https://errors.pydantic.dev/2.12/v/greater_than"
)


def test_odd_log_lifetime_is_rejected() -> None:
"""An odd lifetime exponent cannot split into equal top and bottom trees."""
kwargs = _valid_config_kwargs()
kwargs["LOG_LIFETIME"] = 31
with pytest.raises(ValueError) as exception_info:
XmssConfig(**kwargs)
assert str(exception_info.value) == (
"1 validation error for XmssConfig\n"
" Value error, LOG_LIFETIME must be even, got 31 "
"[type=value_error, input_value={'LOG_LIFETIME': 31, 'DIM...ENTS': 8, 'CAPACITY': 9}, "
"input_type=dict]\n"
" For further information visit "
"https://errors.pydantic.dev/2.12/v/value_error"
)


def test_target_config_is_test_config_under_test_env() -> None:
"""The active configuration under the test environment is the test preset."""
assert TARGET_CONFIG is TEST_CONFIG
Expand Down
Loading