docs(xmss): document the 4-byte epoch packing precondition in the PRF (#1118)

The PRF packs the epoch into four big-endian bytes in both chain-start
and randomness derivation. This is sound only because the epoch is
bounded by the key lifetime, and every supported config keeps
LOG_LIFETIME <= 32, so the value always fits in four bytes.

Record that precondition next to each packing site so a future config
exceeding the bound is understood as the cause of the resulting
overflow at signing time, rather than appearing as an unexplained
failure. The wire layout is unchanged.

Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: tcoratger

src/lean_spec/spec/crypto/xmss/prf.py

@@ -74,6 +74,10 @@ def derive_chain_start(
         #     domain_sep || 0x00 || key || epoch (4 bytes) || chain_index (8 bytes)
         #
         # The 0x00 byte separates chain-start derivation from randomness derivation.
+        #
+        # The epoch is bounded by the key lifetime, which fits in four bytes for every
+        # supported configuration (LOG_LIFETIME <= 32).
+        # A config beyond that bound would overflow this fixed-width packing.
         input_data = (
             PRF_DOMAIN_SEP
             + PRF_DOMAIN_SEP_DOMAIN_ELEMENT
@@ -128,6 +132,10 @@ def derive_randomness(
         # Layout:
         #
         #     domain_sep || 0x01 || key || epoch || message || counter
+        #
+        # The epoch is bounded by the key lifetime, which fits in four bytes for every
+        # supported configuration (LOG_LIFETIME <= 32).
+        # A config beyond that bound would overflow this fixed-width packing.
         input_data = (
             PRF_DOMAIN_SEP
             + PRF_DOMAIN_SEP_RANDOMNESS