HMAC finalize and PBKDF2 iterate on x86 call the compression function

[alex]

Summary

On 32-bit x86, HMAC finalize and PBKDF2 iterate now call the compression function directly for MD5, SHA-1, SHA-384, SHA-512, SHA-512/224 and SHA-512/256. This is the design already used on x86-64 and AArch64, and on ARMv7 in #578. It is written once over a description of a Merkle–Damgård hash and proven once against Proof.MdStream.Md.

Before this change, these functions were generic over the hash's streaming functions:

• each PBKDF2 iteration copied a state byte by byte, then called update and finalize, twice;
• HMAC's outer hash went through update and finalize too.

This PR is implementation only, with no changes to Spec/ or TCB/. The functions are proven against the existing Spec.Hmac.Instance.finalizeContract and iterateContract, at the same stack as before (48).

Some things stay as they are:

• SHA-256 on x86, both the scalar and SHA-NI variants, keeps its own code and its SHA-256-specific contracts. A follow-up moves it onto this code; it will replace HMAC-SHA-256 and PBKDF2-HMAC-SHA-256 on ARMv7 and x86: the generic code #563.
• HMAC init stays the generic one, which runs once per key.
• Other targets: no ARMv7, x86-64 or AArch64 code changes.

Design

Impl/Pbkdf2/Md/X86.lean is new. Its Hash holds:

• the hash's streaming functions, which HMAC init and the inner finalize call;
• the stored hash value size N;
• the length field size L and its byte order;
• the compression function, with its scratch size;
• the digest writer.

It covers both the 64-byte-block hashes (Impl/MdStream/X86.lean) and the SHA-512 family. The block always sits right after the hash value.

iterate. The prologue copies U into the block and writes the padding of a B + D-byte message, once. Each step then:

1. loads the inner hash value from key and compresses;
2. writes the digest into the block, loads the outer hash value and compresses;
3. writes the digest again, and computes T ⊕= U word-wise in t.

So each step is exactly two compressions, with no update/finalize and no byte loops.

HMAC finalize. It makes one call of the streaming finalize for the inner hash. It then reuses the inner state as the outer block, with word copies and constant word stores for the padding and length, and does one compression. The digest goes to out, through scratch and a word copy for the truncated hashes. The helpers (copyW, storeW, pad, digest, cmp) are shared with iterate.

Proofs

• Target-independent lemmas go in a new module, Proof/Pbkdf2/MdHmac.lean: Link.hmac_outer, blockAt_tailPad and Link.hash_outer.
• x86 proofs are in Proof/Pbkdf2/Md/X86/:
  • Block (shared pieces, and MdOk, which bundles what is needed of a hash);
  • Iterate and IterateCT;
  • HmacFin and HmacFinCT;
  • Hashes, Lit and Instances.
• Constant time: taint_decide covers the code between calls; cmp_rel and fin_rel relate the calls through their contracts.
• Whole PBKDF2 (Whole PBKDF2-HMAC (vg_pbkdf2_hmac_<hash>) on ARMv7 and 32-bit x86 #564, Proof/Pbkdf2/Whole/X86/{Lit,Instances}.lean) now calls the new iterate and finalize.
• Deleted:
  • Impl/Pbkdf2/Generic/X86.lean, and Proof/Pbkdf2/Generic/X86/{Iterate,IterateCT,Instances}.lean;
  • the finalize part of Impl/Hmac/Generic/X86.lean, with the proofs trimmed to what init needs (FinalizeCT.lean becomes InitCT.lean).
• Speed: there are no resource-limit options, and the largest new declarations take about 2 s.

Instructions executed (i686, callgrind)

	before	after	change
PBKDF2-MD5, per iteration	3776	1261	−67%
PBKDF2-SHA-1, per iteration	5464	2836	−48%
PBKDF2-SHA-384, per iteration	36048	30403	−16%
PBKDF2-SHA-512, per iteration	36288	30399	−16%
HMAC finalize MD5	2871	1587	−45%
HMAC finalize SHA-1	4515	3159	−30%
HMAC finalize SHA-384	33985	31061	−9%
HMAC finalize SHA-512	34161	31036	−9%

There is no 32-bit OpenSSL here, so the bench crate doesn't build for i686. CI's "Compare with base (x86)" check will measure the change.

Validation

• Lean: a full lake build, then lake env lean --run Emit.lean --check. The axiom and compiler-override audits pass, and the generated code matches.
• CI scripts: check_lean_imports, check_lean_speed, check_vectors, check_arch_gates, check_variants and check_mcdt pass, and algorithms_table needs no README change.
• Lint: cargo fmt --check passes, and so does cargo clippy --all-targets -- -D warnings on the host and for i686.
• Tests:
  • cargo test with Wycheproof passes on the host.
  • On i686, it passes with default features (SHA-NI host) and with VG_CPU_FEATURES=none. These ran on i686-unknown-linux-musl, because the -gnu target can't link in this environment; CI runs -gnu.

Merging with #578

The two PRs conflict only in comments. #578 edited doc references in x86 files that this PR deletes or trims. Whichever merges second keeps this PR's side of those files.

🤖 Generated with Claude Code

https://claude.ai/code/session_01RjfTK5YMk2jDsiKRYs2dbn

---

Generated by Claude Code