Repository navigation
Spec: delete HMAC-SHA-256's and PBKDF2-HMAC-SHA-256's 32-bit contracts - #594
Merged
Merged
Conversation
Since #583, HMAC-SHA-256 and PBKDF2-HMAC-SHA-256 are proven against Spec.Hmac.sha256I's generic contracts on every target, so nothing uses initSha256*, finalizeSha256Out* (Spec/Hmac/Contract.lean) and iterateSha256* (Spec/Pbkdf2/Contract.lean) any more. Delete both files, the documentation that mentions them, and the tests that compared them with sha256I's; the test now checks sha256I's names and modules against the ones the Rust code uses. Spec/Scrypt/Contract.lean imports what it used of Spec/Pbkdf2/Contract.lean directly. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RjfTK5YMk2jDsiKRYs2dbn
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.
Summary
This is a trust change: it touches only
Spec/, plus its tests inVerifiedGarbageTest/. It removes trusted definitions and adds none.Since #583, HMAC-SHA-256 and PBKDF2-HMAC-SHA-256 on ARMv7 and x86 are proven against
Spec.Hmac.sha256I's generic contracts, like every other hash on every target. The SHA-256-specific 32-bit contracts are therefore unused. This PR deletes them:Spec/Hmac/Contract.lean:initSha256Sig,initSha256Contract,initSha256Api,finalizeSha256OutSig,finalizeSha256OutContractandfinalizeSha256OutApi.Spec/Pbkdf2/Contract.lean:iterateSha256Sig,iterateSha256ContractanditerateSha256Api.It also makes these supporting changes:
Spec/Hmac.lean,Spec/Hmac/Generic.lean,Spec/Pbkdf2.leanandSpec/Pbkdf2/Generic.lean.Spec/Hmac/Generic.leandrops the note "removed oncesha256Iis implemented on every target", since that has now happened.Spec/Scrypt/Contract.leanused to importSpec/Pbkdf2/Contract.lean. It now imports what it actually uses,Spec/Pbkdf2.leanandTCB/Artifact.lean.VerifiedGarbageTest/Hmac.leandropped therflchecks that comparedsha256I's contracts with the deleted ones. It now checkssha256I's function names and modules directly against the ones the Rust code calls (hmac_sha256::vg_hmac_sha256_init, etc.).No implementation, proof or generated code changes.
Validation
lake build, includingVerifiedGarbageTest, thenlake env lean --run Emit.lean --check. The axiom, compiler-override and Spec-origin audits pass, andsrc/asmis unchanged.check_lean_imports,check_lean_speed,check_vectors,check_arch_gates,check_variants,check_mcdtandalgorithms_tableall pass.🤖 Generated with Claude Code
https://claude.ai/code/session_01RjfTK5YMk2jDsiKRYs2dbn
Generated by Claude Code