Make x86 SHA-256 constructions generic over compression backends - #460
Merged
Merged
Conversation
reaperhulk
force-pushed
the
codex/sha256-x86-variants
branch
from
October 1, 2026 13:38
2c17e61 to
37cbaba
Compare
This was referenced Oct 1, 2026
This was referenced Oct 1, 2026
alex
pushed a commit
that referenced
this pull request
Oct 1, 2026
src/asm/x86/sha256.rs regenerated (main's #460 reworked the x86 SHA-256 artifacts; vg_sha224_init is re-emitted). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01HDRg9k22FbCYq3TnciKvwG
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
1 participant
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.
x86 SHA-256 compression currently has fixed scalar callers. Register it as a backend and make streaming SHA-256, HMAC-SHA-256, and PBKDF2-HMAC-SHA-256 follow every compression variant automatically. Rust HMAC and PBKDF2 selection now matches the hash backend exhaustively, so adding a backend requires its constructions to handle it.
The HMAC initializer/finalizer and PBKDF2 iteration retain their existing specialized word-copy and direct-compression bodies. Their correctness and ABI proofs now accept any verified compressor, replacing the duplicate scalar proofs. The scalar constructions are definitionally identical to the existing implementations (checked by
scalar_code_unchanged); every emitted SHA-256/HMAC/PBKDF2 assembly body is unchanged. This prepares the x86 SHA-NI implementation without claiming a scalar performance improvement.The ARM benchmark container now installs Rust into a fresh rustup home, matching the merged CI repair in #458. Updating its trimmed preinstalled Cargo failed on missing man-page files before benchmarks could run.
No changes to
TCB/orSpec/.Validation:
lake buildand emitter--check, including artifact axiom and compiler-override audits. This validation is reused after the rebase that changes only workflow setup; no Lean or Rust implementation changes followed it.git diff --check.VG_CPU_FEATURES=nonewithcpu-features-env.