Repository navigation
SHA-256's and SHA-512's own lists of implementations, not Option fields of MdHash - #4696
Merged
Merged
Conversation
alex
force-pushed
the
claude/vg-aes-gcm-tiers
branch
from
November 8, 2026 20:43
87d70dd to
2b47209
Compare
alex
force-pushed
the
claude/vg-sha-compress-lists
branch
from
November 8, 2026 20:43
7dfa4ee to
c74fcdc
Compare
alex
force-pushed
the
claude/vg-aes-gcm-tiers
branch
from
November 8, 2026 21:22
2b47209 to
c3505d9
Compare
alex
force-pushed
the
claude/vg-sha-compress-lists
branch
from
November 8, 2026 21:22
c74fcdc to
bdbaba0
Compare
…ds of MdHash Ed25519, scrypt and RSAES-PKCS1-v1_5 decryption call SHA-512's or SHA-256's compression function alone, yet were applied to every Merkle–Damgård variant on x86-64 and AArch64 (MD5, SHA-1, … each with each CPU's code) and kept those whose `sha512` or `sha256` field, an `Option` set only for those hash functions, was `some`. Give each of the two hash functions' compression functions its list of implementations on each target (`Proof/Variants/Sha256Compress/<Target>.lean`, `Proof/Variants/Sha512Compress/<Target>.lean`), map those callers over it, and delete the two fields. The generated crates are unchanged. Part of #4548. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01TKUFHFjAR7Byf513R4zuFy
alex
force-pushed
the
claude/vg-sha-compress-lists
branch
from
November 8, 2026 21:46
bdbaba0 to
f54c962
Compare
alex
enabled auto-merge
November 8, 2026 21:47
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.
Part of #4548. This is stacked on #4692. There are no trust changes.
Ed25519, scrypt and RSAES-PKCS1-v1_5 decryption each call only SHA-512's or SHA-256's compression function. Until now, though, they were applied to every Merkle–Damgård variant on x86-64 and AArch64: MD5, SHA-1 and so on, each with each CPU's code, 22 variants on x86-64. They then kept only the variants whose
sha512orsha256field wassome, anOptionthat is set only for those two hash functions.What changes
Proof/Variants/Sha256Compress/{X86_64,AArch64}.leanProof/Variants/Sha512Compress/{X86_64,AArch64}.leanmatch … | none => []filtering is gone.MdHash: thesha512andsha256fields are deleted fromMdHashon both targets.The generated crates are unchanged.
Checks
lake buildpasses.Emit.leanpasses, with no change to the crates.check_lean_public_imports.pypasses.Generated by Claude Code