HMAC init proofs: one shared lemma module for all four targets - #605
Merged
Merged
Conversation
#586 (ARMv7, x86) and #587 (x86-64, AArch64) each added a target-independent module of lemmas for HMAC's `init` over a Merkle-Damgard hash: Proof/Pbkdf2/MdInit.lean and Proof/Pbkdf2/MdKeys.lean. Several of their facts were the same. Keep one module, MdKeys, with each fact proven once in its most general form, and delete MdInit: * `Md.repr_block` (the general form) replaces `Md.repr_of_block`, which also took the initial hash value as `stateAt m p`: x86-64 and AArch64 now pass `e.trans (congrArg (compress · _) iv)`. * `xorOpad_ipad` replaces the identical `xorPad_6a`. * `writeW_xorRep` (any repeated byte) replaces `writeW_xorOpad` (0x6a only); `xorOpad_mem` rewrites with `c6a` first. * `xor_byte` is stated for any width of at least a byte (an auto-param), replacing MdInit's 32-bit one and AArch64 HmacInit's 64-bit copy. The rest of MdInit's lemmas (`writeW_rep`, `c6a`, `bytes_over`, `blockKey_short`, `xorPad_short`) move to MdKeys unchanged. Proof-only: the emitter's output is unchanged. 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
Two PRs gave HMAC's
initthe compression-level design: #586 (ARMv7 and x86) and #587 (x86-64 and AArch64). Each added its own target-independent lemma module,Proof/Pbkdf2/MdInit.leanandProof/Pbkdf2/MdKeys.lean, and several facts ended up proven in both. This PR merges the two intoMdKeys.lean, proves each fact once in its more general form, and points all four targets'HmacInitproofs at it.MdInit.leanis deleted.This is a proof-only refactor. There are no changes to
TCB/,Spec/,Impl/, Rust or the generated code.Md.repr_blockMd.repr_of_blockstateAt m p = iv.xorOpad_ipadxorPad_6awriteW_xorRepwriteW_xorOpad0x6a.xor_byteHmacInit.leanw ≥ 8.The rest of
MdInit's lemmas moved over unchanged, andMdKeysalready imports everything they need. Some target-specific lemmas stay where they are, because they are stated over each target's own registers, state or parameters:keep_st/keep_repr;blockKey_eq;xor_word;setWidthxor_byte.Proof cost
The table shows instructions, counted with valgrind's cachegrind (
perfhas no hardware counters in this VM). The run-to-run noise is about ±5M.MdKeys)Validation
lake build, thenlake env lean --run Emit.lean --check. The axiom, compiler-override and Spec-origin audits pass, andsrc/is unchanged.check_lean_imports,check_lean_speed,check_vectors,check_arch_gates,check_variantsandcheck_mcdtall pass.cargo fmt --checkpasses.🤖 Generated with Claude Code
https://claude.ai/code/session_01RjfTK5YMk2jDsiKRYs2dbn
Generated by Claude Code