HMAC-SHA-256 and PBKDF2-HMAC-SHA-256 on ARMv7 and x86: the generic contracts and code

[alex]

Summary

HMAC-SHA-256 and PBKDF2-HMAC-SHA-256 on ARMv7 and 32-bit x86 now use the same contracts and code as every other hash on every target:

• the contracts are Spec.Hmac.sha256I's init, finalize, iterate and pbkdf2;
• the code is the compression-level HMAC finalize and PBKDF2 iterate from HMAC finalize and PBKDF2 iterate on ARMv7 call the compression function #578 and HMAC finalize and PBKDF2 iterate on x86 call the compression function #579.

SHA-256's own 32-bit HMAC and PBKDF2 implementations and proofs are deleted. This replaces #563.

It is implementation only: no changes to Spec/ or TCB/. The old SHA-256-specific contracts in Spec (initSha256*, finalizeSha256Out*, iterateSha256*) are now unused. A separate Spec-only PR will delete them.

ARMv7

• SHA-256 becomes one more instance of Impl/Pbkdf2/Md/Arm.lean, like SHA-224 (Proof/Pbkdf2/Md/Arm/Sha256.lean, Proof/Hmac/Generic/Arm/Sha256.lean).
• The whole-PBKDF2 SHA-256 instance is rewired onto it.

x86

• The SHA-256 backend interface (Proof/Sha256/X86/Variants/Interface.lean) now carries:
  • each backend's compression function and its facts;
  • its streaming functions (Sha256Stream).
• Generic/Sha256/X86/{Hmac,Pbkdf2}.lean emit sha256I's init, finalize, iterate and pbkdf2 for each backend, built from the Md x86 code. The SHA-NI backend gets the _shani suffix.
• The proofs are written once for every backend: Proof/Hmac/Generic/X86/Sha256.lean, Proof/Pbkdf2/Md/X86/Sha256.lean, Proof/Pbkdf2/Whole/X86/Sha256.lean.

scrypt

main's scrypt (#573) calls the whole PBKDF2-HMAC-SHA256, so its proofs now follow the moved instances:

• on ARMv7, SHA-256's HashOK is Proof.Hmac.Generic.Arm.sha256OK;
• on x86, a backend's PBKDF2 is Backend.F.

Deleted

• Impl/Hmac/{X86,Arm}.lean, Impl/Hmac/Sha256/X86.lean, Impl/Pbkdf2/{X86,Arm}.lean and Impl/Pbkdf2/Sha256/X86.lean, with their proofs.
• Proof/Pbkdf2/Whole/X86/Sha256Fns.lean, Proof/Sha256/X86/Stream/{CompressAt,FinalizeVariant}.lean and Proof/Framework/TaintWeaken.lean.

Rust

src/hmac/sha256.rs uses streaming_hmac! on every architecture, with SHA-NI in its match on x86. The 32-bit HmacHash implementation and its state type are removed.

Performance (instructions)

	main (before #578/#579)	this PR
ARMv7 finalize	5190	5035
ARMv7 iterate, per iteration	4810	4810
i686 scalar finalize	7085	7125
i686 scalar iterate, per iteration	6812	6817

PBKDF2 matches main. With SHA-NI, natively, 3M iterations take 412 ms, against 426 ms on main.

A short HMAC on x86 is still a few percent slower than with the old SHA-256 code, because HMAC's init calls the streaming init and update. #586, which builds on this PR, gives init the compression-level design and makes a short HMAC-SHA-256 on x86 about 14% faster than main was.

Validation

All of the following ran on the branch after merging main, which now contains #575, #578, #579 and #582:

• Lean: a full lake build, then lake env lean --run Emit.lean --check. The axiom, compiler-override and Spec-origin audits pass.
• CI scripts: check_lean_imports, check_lean_speed, check_vectors, check_arch_gates, check_variants, check_mcdt and algorithms_table all pass.
• Rust lint: cargo fmt --check, and cargo clippy --all-targets -- -D warnings on the host, i686 and armv7.
• Tests: cargo test with Wycheproof passes on i686-musl (238 passed, 0 failed). Before the merge it also passed on the host, and on i686 with VG_CPU_FEATURES=none.

🤖 Generated with Claude Code

https://claude.ai/code/session_01RjfTK5YMk2jDsiKRYs2dbn