You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Implement three leanSpec cryptographic subspecifications:
- KoalaBear Fp field arithmetic (modular add/sub/mul/div/pow/inverse)
- Poseidon2 hash function (pure-Python permutation, compression, sponge)
- XMSS core components (PRF, tweak encoding, hypercube mapping, hash
chains, Merkle tree construction and path verification)
Interpreter features added:
- math.comb(n, k) for binomial coefficients
- os.urandom(n) for random byte generation
- List slice assignment (e.g. state[rate:] = values)
- __bytes__ dunder dispatch in bytes() builtin
13 new tests in LeanPythonTest/Crypto.lean covering all components,
including Poseidon2 width-16 permutation verified against reference
test vectors from leanSpec.
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
0 commit comments