General Cleanup of Crypto Builtins#308
Merged
Merged
Conversation
Eduardogbg
commented
Jun 19, 2026
Eduardogbg
commented
Collaborator
- move hash tests to Tests (improving build time?)
- dedup ECDSA verification across secp256{k,r}1
- dedup a lot of 32-bit word logic amongst all the hash functions
- add missing requirements to python scripts
- remove some redundant comments
- fix an unused hypothesis lint warning
- turn blake3 spec into a public theorem
SHA-256, BLAKE2s and BLAKE3 each carried their own copies of rotr32, the little-endian byte<->u32 conversions (bytesToWord, blockBytesToWords, wordToBytes, stateTo32Bytes, padBlock) and the SHA-256 initial hash value (which BLAKE2s/BLAKE3 reuse verbatim as their IV). Move them to Lampe/Crypto/WordUtils.lean in the shared Lampe.Crypto namespace and make the three hash models use it.
Secp256k1.lean and Secp256r1.lean were clones modulo curve constants: bytesToNatBE, the Fermat-inversion orderPow/orderInv pair, and the FIPS 186-4 $6.4.2 verifyBytes body. Factor the curve-independent core into Lampe/Crypto/Ecdsa/Verify.lean, parameterized over the curve, its group order and the generator, and make the two curve files thin instantiations. The per-curve verifyBytes names (used by Builtin/Crypto/Ecdsa.lean) are preserved.
The native_decide example vectors in Secp256k1.lean / Secp256r1.lean ran on every library build and were invisible to lake test. Move them to Lampe/Tests/Ecdsa.lean (one section per curve), following the structure of the other crypto reference-vector test files.
The FIPS 180-2 Appendix B vectors lived both inside Lampe/Crypto/Sha256.lean (private theorems re-checked on every library build) and in Lampe/Tests/Sha256.lean. Drop the library-side copies and add the one vector Tests was missing (block 1 of the two-block example: IV -> intermediate H^(1)), so the Tests file now covers all three compressions.
The two XKCP KAT theorems ran full Keccak-f[1600] permutations through the kernel evaluator via plain decide (with a bumped maxRecDepth). Every other reference-vector test in the crypto series uses native_decide; align these for consistency and faster builds.
The file holds only the poseidon2Permutation builtin; every later crypto primitive has a self-named file. Update the Lampe.lean import.
Drop the redundant doc comments on the ECDSA and BLAKE3 builtins (they restate the definitions; the `isUnconstrained = false` note is a given), and fix stale wording / test-vector references in the BLAKE2s and Keccak module docs.
kustosz
approved these changes
Jun 19, 2026
Eduardogbg
force-pushed
the
edu/crypto-cleanup
branch
2 times, most recently
from
717e5fa to
b94ea18
Compare
The reference test-vector and Pratt-certificate generators are author-time tools whose outputs are committed and which CI never runs. Group them under scripts/gen/ (mirroring scripts/ci/) with their own requirements.txt, so the CI-image deps (scripts/requirements.txt) and the generator-only deps no longer share a directory. Give every generator one interface -- `python3 scripts/gen/<name>.py <path>` -- that rewrites only the region between `-- BEGIN/END generated <label> --` markers in the target file and leaves the rest hand-editable; a shared scripts/gen/_lean.py does the splice. Generators emit anonymous `example ... := by native_decide` checks; pratt.py reads the prime from the target's own `primeNat`. Regenerated vectors and certificates are byte-identical to the previously committed values.
Mark the unused `a.val < pow128` hypothesis as `_ha` (callers still pass it positionally) and switch the contradiction step from `simpa using h` to `simp at h`.
Eduardogbg
force-pushed
the
edu/crypto-cleanup
branch
from
b94ea18 to
2f61054
Compare
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
2 participants
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.