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

[alex]

Draft: this regresses PBKDF2 performance on x86 (and likely ARMv7); see below. Opened so CI's Benchmarks measure it on real hardware before deciding how to proceed.

On ARMv7 and x86, HMAC-SHA-256's init/finalize and PBKDF2-HMAC-SHA-256's iterate were the last HMAC/PBKDF2 functions with implementations of their own, proven against SHA-256-specific contracts (initSha256Contract with 76 words of scratch, finalizeSha256OutContract with 86, iterateSha256Contract). They are now the one HMAC and PBKDF2 implementation for every streaming hash function (Impl/Hmac/Generic, Impl/Pbkdf2/Generic), calling SHA-256's verified streaming functions, and proven against Spec.Hmac.sha256I's generic contracts (104 words) — as SHA-1, MD5 and the SHA-512 family already are on these targets, and SHA-256 is on x86-64 and AArch64.

• ARMv7: sha256OK and the instances in Proof/{Hmac,Pbkdf2}/Generic/Arm; the registration files are like SHA-1's.
• x86: SHA-256 keeps its variant interface (Variants/Sha256/X86/): a backend now provides its streaming update/finalize (Sha256Stream); HMAC and PBKDF2 are proven once for any backend (the code between calls depends only on SHA-256's sizes, so its taint is checked once) and emitted per backend from Generic/Sha256/X86/ — so the scalar and SHA-NI (Accelerate x86 SHA-256, HMAC and PBKDF2 with SHA-NI #468) backends both get them, as would any new one.
• Deleted: the SHA-256-specific implementations and proofs (Impl/Hmac/{Arm,X86}.lean, Impl/Hmac/Sha256/X86.lean, Impl/Pbkdf2/{Arm,X86}.lean, Impl/Pbkdf2/Sha256/X86.lean, Proof/Hmac/{Arm,X86,Sha256}/…, Proof/Pbkdf2/{Arm,X86,Sha256}/…, Proof/Sha256/X86/Stream/{CompressAt,FinalizeVariant}.lean). Scrypt's ARM proof used one lemma from them (wp_eor), now its own.
• Rust: src/hmac/sha256.rs and src/pbkdf2/sha256.rs use streaming_hmac!/streaming_pbkdf2! on every target (the hand-written Sha256HmacState, sha256_key_states and iterate are gone), matching exhaustively on Sha256Backend; PBKDF2's key states are now zeroized, and ARMv7 no longer skips the backend match.
• Trust: no Spec/ or TCB/ changes. The SHA-256-specific contracts in Spec/Hmac/Contract.lean and Spec/Pbkdf2/Contract.lean become unused; a separate trust-change PR removes them after this one.

Performance regression

The SHA-256-specific iteration made two compression calls per step. The generic one, for each of the inner and outer states, copies the 96-byte state byte by byte, updates (buffering the 32-byte U byte by byte) and finalizes, then XORs T byte by byte. On i686 (musl build on an x86-64 SHA-NI machine, min of 7 runs):

	before	after
PBKDF2, per iteration, scalar	393 ns	606 ns (+54%)
PBKDF2, per iteration, SHA-NI	136 ns	307 ns (2.25×)
HMAC of 64 bytes, scalar	1174 ns	1376 ns (+17%)
HMAC of 64 bytes, SHA-NI	453 ns	661 ns (+46%)

ARMv7 wasn't measured locally; from the emitted code, the two 96-byte copies alone are ~1,350 instructions per iteration, so expect something similar. The same costs already apply to SHA-1, MD5 and the SHA-512 family on these targets. Ways to recover it (word-wise state copies and XOR in the generic code, or porting the 64-bit targets' compression-level Md design to 32-bit) are follow-ups.

Checked locally: full lake build, Emit.lean regenerated and --check, every ci/ check, cargo fmt/clippy (native, i686, armv7, aarch64), cargo test with Wycheproof natively and on i686 (musl) with VG_CPU_FEATURES=none, sha,ssse3 and unrestricted (both x86 backends). Not run locally: ARMv7 tests.

🤖 Generated with Claude Code

https://claude.ai/code/session_01RjfTK5YMk2jDsiKRYs2dbn

---

Generated by Claude Code

[alex]

On 42984e3 the Compare with base checks fail for arm, x86 and x86 with VG_CPU_FEATURES=none. The slowdown was expected and comes from this PR:

Benchmark	arm	x86 (SHA-NI)	x86 (none)
pbkdf2-hmac-sha256/64	50.1% slower	146.3% slower	25.6% slower
pbkdf2-hmac-sha256/1024	51.8% slower	150.9% slower	30.1% slower
pbkdf2-hmac-sha256/16384	51.6% slower	151.2% slower	24.3% slower
hmac-sha256/64	12.6% slower	61.9% slower	32.3% slower

The cause is described in the PR body. The generic 32-bit code copies its state byte by byte and runs a full update/finalize on every PBKDF2 iteration. The old SHA-256-specific code compressed directly. The fixed overhead is worst where compression is cheap, as with SHA-NI. I'm keeping this as a draft until we've decided how to win the speed back:

• make the generic copies and XORs word-wise, or
• port the 64-bit compress-level Md design to the 32-bit targets.

---

Generated by Claude Code

[alex]

I'm closing this in favour of #583. That PR moves SHA-256 on ARMv7 and x86 onto the same generic contracts as this one, but uses the compression-level HMAC finalize and PBKDF2 iterate from #578 and #579 rather than the streaming-level code. With that, PBKDF2-SHA-256 runs as fast as it does on main, instead of 50–150% slower.

---

Generated by Claude Code