Repository navigation
signatures: cross-check leanXMSS against EthLib's test vectors - #648
Merged
Merged
Conversation
EthLib specifies leanXMSS in Lean and proves its keyGen, sign and verify correct. Its test vectors pin key generation, signing and verification byte for byte, rejections included. `tests/signatures/ethlib/xmss/` vendors those vectors at EthLib dd0b80a (ethereum/EthLib#50), and `ethlib_vectors.rs` runs every case against lean_xmss: 4 key generations, 6 signings and 16 verifications, all equal. `ethlib/sync.sh <commit>` refreshes the copy: it fetches EthLib at that commit, checks every case against EthLib's SHA256SUMS, and records the commit in `ethlib/COMMIT`. The cases are read by a strict reader of their fixed shape, so a change of format fails instead of skipping cases. The three tests take about 2 s in release: two full keys and four bottom trees. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
EthLib specifies leanXMSS in Lean, with machine-checked proofs that its key generation, signing and verification fit together.
Its test vectors (ethereum/EthLib#50) pin all three byte for byte, rejections included.
This runs every one of them against
lean_xmss:All 26 agree with this crate.
The signatures cover the first leaf, the first leaf of the second bottom tree, the last leaf, and
0xA5C37E19.Each rejected verification changes one input: the message, the leaf index, one bit of a randomizer, a chain value or a sibling on either layer, the key's root or public parameter, another key, or a length.
How the vectors get here
crates/signatures/tests/signatures/ethlib/xmss/is a verbatim copy of EthLib'stests/cryptography/xmss/, at the commit inethlib/COMMIT(dd0b80a).It fetches EthLib at that commit, checks every case against EthLib's
SHA256SUMS, then replaces the copy and records the commit.The test reads the copy offline, so CI never touches the network.
A strict reader parses the fixed shape of a case, so a change of format fails the test instead of skipping cases.
An EthLib output of
nullmarks an input of the wrong length, which here cannot fill the API's fixed-size arrays.Cost
Two full keys and four bottom trees: about 2 s in release.
Corrupting one byte of one vendored signature fails
sign_matches_ethliband names the case.I am an AI agent (Claude); a human reviews before merge.
🤖 Generated with Claude Code