HMAC finalize and PBKDF2 iterate on ARMv7 call the compression function

[alex]

Summary

On ARMv7, HMAC finalize and PBKDF2 iterate now call the compression function directly, for MD5, SHA-1, SHA-224, SHA-384, SHA-512, SHA-512/224 and SHA-512/256. This is the design x86-64 and AArch64 already use (Impl/Pbkdf2/{X86_64,AArch64}.lean, Impl/Pbkdf2/Md/). It is written once over a description of a Merkle–Damgård hash and proven once against Proof.MdStream.Md.

Until now these functions were generic over the hash's streaming functions:

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

This PR is implementation only. There are no changes to Spec/ or TCB/: the functions are proven against the existing Spec.Hmac.Instance.finalizeContract/iterateContract at stack := 16, as before.

What is unchanged:

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

Design

Impl/Pbkdf2/Md/Arm.lean is new. Its Hash holds the hash's streaming functions plus what the compression-level code needs:

• the stored hash value size N;
• the length field size L and the byte order;
• the compression function (name, code, scratch offset);
• the digest writer.

It covers both the 64-byte-block hashes (Impl/MdStream/Arm.lean) and the SHA-512 family, which has its own streaming code.

iterate.

• The prologue writes the block U ‖ 0x80 ‖ zeros ‖ length of a (B + D)-byte message once, with word stores.
• Each step:
  • copies the inner hash value word-wise and compresses;
  • writes the digest back over U, restoring the padding when D < N;
  • does the same with the outer hash value;
  • computes T ⊕= U word-wise.
• No update/finalize calls, no byte loops, no stack.

HMAC finalize.

• One call of the streaming finalize for the inner hash, which has a variable-length message.
• Then the outer hash in one compression, as in iterate: the outer hash value is copied word-wise, and the padding and length words are written at fixed offsets.
• The digest goes to out directly when D = N, otherwise through scratch and a word copy.
• The shared helpers are copyW, padFrom, constW, lenWords and xorW.

Proofs

• New files: Proof/Pbkdf2/Md/Arm/ holds Words, Compress, Hash, Iterate, IterateCT, HmacFin, HmacFinCT, Sha512, Instances and Sha224.
• Target-independent lemmas: Md.iterate_hmac and Md.hmac_outer, in Proof/Pbkdf2/MdStep.lean.
• Constant time: taint_decide covers the blocks between calls; compressBlock_rel and fin_rel cover the calls.
• Whole PBKDF2 from Whole PBKDF2-HMAC (vg_pbkdf2_hmac_<hash>) on ARMv7 and 32-bit x86 #564 (Proof/Pbkdf2/Whole/Arm/{Instances,Sha224}.lean) now calls the new iterate and finalize, through their new theorems.
• Deleted:
  • the streaming-level Impl/Pbkdf2/Generic/Arm.lean and its proofs;
  • Proof/Hmac/Generic/Arm/Finalize.lean;
  • the finalize part of Impl/Hmac/Generic/Arm.lean;
  • the finalize parts of Proof/Hmac/Generic/Arm/{Instances,Sha224}.lean.
• There are no resource-limit options.

Instructions executed (generated code, compression calls included)

The counts come from a small ARMv7 interpreter run over the generated src/asm/arm/*.rs, which also checked every result against Python's hmac.

Hash	PBKDF2 iteration	HMAC finalize (20-byte message)
MD5	3472 → 1378	2701 → 1629
SHA-1	5494 → 3296	4679 → 3542
SHA-224	7256 → 4812	6325 → 5049
SHA-384	22554 → 18006	20879 → 18513
SHA-512	22762 → 18010	21023 → 18486
SHA-512/224	22294 → 17996	20699 → 18508
SHA-512/256	22346 → 17998	20735 → 18509

Excluding the compressions, the overhead per iteration dropped from 2276 to 78 instructions for SHA-1, and from 4984 to 232 for SHA-512. CI's "Compare with base (arm)" check will measure the real-world speedup.

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, check_mcdt and algorithms_table all pass.
• Rust:
  • cargo fmt --check;
  • cargo clippy --all-targets -- -D warnings, on the host and with --target armv7-unknown-linux-gnueabihf;
  • cargo check --target armv7-unknown-linux-gnueabihf --all-targets;
  • cargo test with Wycheproof on the host.
• Not run locally: the ARMv7 tests and benchmarks, since there is no ARM runner here. CI runs both.

🤖 Generated with Claude Code

https://claude.ai/code/session_01RjfTK5YMk2jDsiKRYs2dbn

---

Generated by Claude Code