Depends on the Merkle tree and verification landing first.
Key generation. Everything is derived from one 32-byte secret S, so a key pair is reproducible from it alone:
- the public parameter is
P = Th(0^16, tweak(type 10, 0, 0), S), hashed with an all-zero parameter because P does not exist yet;
- the secret of chain
i at epoch ep is Th(P, tweak(type 0, i, ep), S);
- walking every chain to position 7 and hashing the 42 tips gives that epoch's leaf;
- the Merkle root over the leaves gives the public key
(root, P).
A key declares an epoch range, since building all 2^32 leaves is infeasible. With the recursive node definition there is nothing else to store: the secret key is just (S, P, epoch_start, epoch_end), and every chain value and tree node is recomputed on demand. That is simpler than both the note, which stores every chain value and every node, and the reference implementation, which keeps a cached subtree — and it is observationally identical to both.
Signing. Deterministic, given (S, epoch, message):
- For
a = 0, 1, 2, ... derive rho_a = first 24 bytes of BLAKE2s-256(tweak(type 12, a, epoch) || P || S || message).
- Try to encode the message with
rho_a. Stop at the first a whose encoding is admissible.
- Reveal chain
i at position x_i for each of the 42 chains.
- Collect the 32 Merkle siblings on the path from leaf
epoch to the root.
- Return the 42 chain values,
rho, and the 32 siblings.
Note that S is inside the randomizer's hash input, so the randomizer is secret until the signature publishes it. About 2^15 trials are expected and the cap is 2^23; Lean needs this as bounded recursion on a fuel parameter rather than a while. Failing after the cap returns a typed error, which with a sound hash happens with probability below 2^-256 per signature.
Errors to raise: an empty epoch range at key generation, an epoch outside the key's range at signing, and exhausting the trial cap.
Two things the docstrings must state plainly. Signing is deterministic, so the same inputs always give the same signature. And an epoch must never sign two different messages under one key — the API is stateless and takes the epoch as an argument, so tracking spent epochs is the caller's job.
Goes in EthCryptographySpecs/Xmss/KeyGen.lean and Xmss/Sign.lean, or split into two pull requests if the diff runs long. Reference implementation: key_gen_from_seed and sign in crates/xmss/src/xmss.rs.
Depends on the Merkle tree and verification landing first.
Key generation. Everything is derived from one 32-byte secret
S, so a key pair is reproducible from it alone:P = Th(0^16, tweak(type 10, 0, 0), S), hashed with an all-zero parameter becausePdoes not exist yet;iat epochepisTh(P, tweak(type 0, i, ep), S);(root, P).A key declares an epoch range, since building all
2^32leaves is infeasible. With the recursive node definition there is nothing else to store: the secret key is just(S, P, epoch_start, epoch_end), and every chain value and tree node is recomputed on demand. That is simpler than both the note, which stores every chain value and every node, and the reference implementation, which keeps a cached subtree — and it is observationally identical to both.Signing. Deterministic, given
(S, epoch, message):a = 0, 1, 2, ...deriverho_a = first 24 bytes of BLAKE2s-256(tweak(type 12, a, epoch) || P || S || message).rho_a. Stop at the firstawhose encoding is admissible.iat positionx_ifor each of the 42 chains.epochto the root.rho, and the 32 siblings.Note that
Sis inside the randomizer's hash input, so the randomizer is secret until the signature publishes it. About2^15trials are expected and the cap is2^23; Lean needs this as bounded recursion on a fuel parameter rather than awhile. Failing after the cap returns a typed error, which with a sound hash happens with probability below2^-256per signature.Errors to raise: an empty epoch range at key generation, an epoch outside the key's range at signing, and exhausting the trial cap.
Two things the docstrings must state plainly. Signing is deterministic, so the same inputs always give the same signature. And an epoch must never sign two different messages under one key — the API is stateless and takes the epoch as an argument, so tracking spent epochs is the caller's job.
Goes in
EthCryptographySpecs/Xmss/KeyGen.leanandXmss/Sign.lean, or split into two pull requests if the diff runs long. Reference implementation:key_gen_from_seedandsignincrates/xmss/src/xmss.rs.