HMAC init on ARMv7 and x86: compress the padded key blocks directly by alex · Pull Request #586 · pyca/verified-garbage

alex · 2026-10-02T10:46:40Z

Summary

On ARMv7 and 32-bit x86, HMAC's init now works at the compression-function level, like finalize and PBKDF2's iterate, and like init on x86-64 and AArch64 since #587. This covers every Merkle–Damgård hash: MD5, SHA-1, SHA-224 (on ARMv7), SHA-256 (on x86, both the scalar and SHA-NI variants) and the SHA-384/512 family.

This is an implementation-only change: no changes to Spec/ or TCB/. init is proven against the existing Spec.Hmac.<hash>I.initContract.

Before, init wrote K₀ ⊕ ipad and K₀ ⊕ opad with byte loops, then called the streaming init and the streaming update of one block for each state.

Now init:

calls the streaming init on both states;
fills the inner state's buffer with 0x36363636 words and XORs the key in, with a byte loop over the key alone;
derives K₀ ⊕ opad word by word into the outer state's buffer (XOR 0x6a6a6a6a);
compresses each block with one direct call of the compression function. There is no update.

The whole PBKDF2 (Fns) and x86 SHA-256's variants (Generic/Sha256/X86/Hmac.lean) use the new init.

Proofs

New target-independent module: Proof/Pbkdf2/MdInit.lean (including Md.repr_block).
New proofs: Proof/Pbkdf2/Md/{X86,Arm}/HmacInit.lean and HmacInitCT.lean prove init once for any Md hash, at the existing stacks: 48 bytes on x86, 16 on ARMv7.
Constant time: taint_decide covers the pieces between calls; the calls are related through their contracts.
Deleted: the streaming-level init code and proofs.
Moved: the helpers still in use, to Impl/Pbkdf2/Stream/{X86,Arm}.lean and Proof/Pbkdf2/Stream/{X86,Arm}/*. The scrypt proofs (scrypt: the whole derivation as verified vg_scrypt on x86-64, AArch64, ARMv7 and x86 #573) now refer to them there.
Rust: unchanged. HMAC over streaming hashes: init and finalize in place, without zeroing scratch #582 already made the HMAC scratch uninitialized.

Performance

i686, measured with callgrind (VG_CPU_FEATURES=none), in instructions per call. "MAC" means a 32-byte key and a 16-byte message.

	SHA-256 init	SHA-256 MAC	SHA-384 init	SHA-384 MAC	MD5 init	MD5 MAC
`main` before #578/#579/#583	7165	15759	33517	70846	2047	6270
this PR	7059	15213	30633	63073	1547	3788

Native, SHA-NI, 1M MACs, pinned, median of 15 runs: HMAC-SHA-256 takes 422–436 ms here, against 490–518 ms before. With VG_CPU_FEATURES=none it takes 1125 ms, against 1199 ms.
ARMv7, instructions per init in the generated code, for a 0-byte and a 32-byte key:
- MD5: 2008 → 1459 and 2073 → 1684
- SHA-256: 5400 → 4851 and 5465 → 5076
- SHA-512 family: 20832 → 18051 and 20897 → 18276

Validation

These ran on the branch with main merged in (#583 and #587 included):

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.

Earlier, on the same code:

Lint: cargo fmt --check, and cargo clippy --all-targets -- -D warnings on the host, i686 and armv7.
Tests: cargo test with Wycheproof on the host and on i686-musl, both with SHA-NI and with VG_CPU_FEATURES=none.

The last merge of main added only #537 (ML-DSA, x86-64), which this PR doesn't touch.

🤖 Generated with Claude Code

https://claude.ai/code/session_01RjfTK5YMk2jDsiKRYs2dbn

…on (MD5, SHA-1, SHA-224, SHA-384, SHA-512, SHA-512/224, SHA-512/256) Port the compression-level design of x86-64 and AArch64 to 32-bit ARM for every Merkle-Damgard hash function but SHA-256 (which keeps its own code). New `Impl/Pbkdf2/Md/Arm.lean` (`Hash`: the streaming `Hash` plus the hash value size N, the length field L, byte order, compression scratch offset, digest-writing code and compression function): * PBKDF2 `iterate` lays out the message block once in scratch (U || 0x80 || zeros || the length of B + D bytes, as word stores). Each step copies the key's inner hash value into scratch word-wise, compresses the block once, writes the digest back over U (restoring the padding it overwrites when N > D), does the same with the outer hash value, and XORs U into T word-wise. Two compressions per step, no calls of update or finalize, no byte loops. * HMAC `finalize` calls the streaming finalize for the inner hash, then copies the outer hash value word-wise, pads the digest into a fixed block with word stores, compresses it once and writes the digest to out (via scratch and a word copy when D < N). Proofs (`Proof/Pbkdf2/Md/Arm/`), once for every hash function, against the `iterG`/`finG` contracts at 16 bytes of stack, moved to the shared `Spec.Hmac.*I.iterateContract`/`finalizeContract`: correctness against `Proof.MdStream.Md` (`Iterate.lean`, `HmacFin.lean`, with the target-independent `Md.iterate_hmac` and `Md.hmac_outer` in `Proof/Pbkdf2/MdStep.lean`); constant time with RelCT, the code between calls by `taint_decide` and the calls by `compressBlock_rel` and `fin_rel` (`IterateCT.lean`, `HmacFinCT.lean`); and the instances (`Instances.lean`, `Sha224.lean`). The whole `vg_pbkdf2_hmac_<hash>` (#564) now calls the new functions (`Proof/Pbkdf2/Whole/Arm/Instances.lean` and `Sha224.lean`, `fnsOf`). Deleted the streaming-level generic `iterate` and `finalize` on ARMv7 (`Impl/Pbkdf2/Generic/Arm.lean`, `Proof/Pbkdf2/Generic/Arm/`, `Proof/Hmac/Generic/Arm/Finalize.lean`, `finalize` in `Impl/Hmac/Generic/Arm.lean`); HMAC `init` is unchanged. No changes to TCB/ or Spec/. Instructions per PBKDF2 iteration on ARMv7 (counted by emulating the generated code; compressions included): MD5 3472 -> 1378 SHA-1 5494 -> 3296 SHA-224 7256 -> 4812 SHA-384 22554 -> 18006 SHA-512 22762 -> 18010 SHA-512/224 22294 -> 17996 SHA-512/256 22346 -> 17998 HMAC finalize (20-byte message): SHA-1 4679 -> 3542, SHA-512 21023 -> 18486. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RjfTK5YMk2jDsiKRYs2dbn

…al-labmxq-md-arm # Conflicts: # lean/VerifiedGarbage/Artifacts/HmacMd5/Arm.lean # lean/VerifiedGarbage/Artifacts/HmacSha1/Arm.lean # lean/VerifiedGarbage/Artifacts/HmacSha224/Arm.lean # lean/VerifiedGarbage/Artifacts/HmacSha384/Arm.lean # lean/VerifiedGarbage/Artifacts/HmacSha512/Arm.lean # lean/VerifiedGarbage/Artifacts/HmacSha512_224/Arm.lean # lean/VerifiedGarbage/Artifacts/HmacSha512_256/Arm.lean # lean/VerifiedGarbage/Artifacts/Pbkdf2Md5/Arm.lean # lean/VerifiedGarbage/Artifacts/Pbkdf2Sha1/Arm.lean # lean/VerifiedGarbage/Artifacts/Pbkdf2Sha224/Arm.lean # lean/VerifiedGarbage/Artifacts/Pbkdf2Sha384/Arm.lean # lean/VerifiedGarbage/Artifacts/Pbkdf2Sha512/Arm.lean # lean/VerifiedGarbage/Artifacts/Pbkdf2Sha512_224/Arm.lean # lean/VerifiedGarbage/Artifacts/Pbkdf2Sha512_256/Arm.lean # lean/VerifiedGarbage/Proof/Hmac/Generic/Arm/Finalize.lean # lean/VerifiedGarbage/Proof/Hmac/Generic/Arm/Instances.lean # lean/VerifiedGarbage/Proof/Hmac/Generic/X86/Finalize.lean # lean/VerifiedGarbage/Proof/Hmac/Generic/X86/Instances.lean # lean/VerifiedGarbage/Proof/Pbkdf2/Generic/Arm/Instances.lean # lean/VerifiedGarbage/Proof/Pbkdf2/Generic/Arm/Sha224.lean # lean/VerifiedGarbage/Proof/Pbkdf2/Generic/X86/Instances.lean # lean/VerifiedGarbage/Proof/Pbkdf2/Generic/X86/Iterate.lean # lean/VerifiedGarbage/Proof/Pbkdf2/Generic/X86/IterateCT.lean

…al-labmxq-md-arm

On 32-bit x86, HMAC's `finalize` and PBKDF2's `iterate` for MD5, SHA-1, SHA-384, SHA-512, SHA-512/224 and SHA-512/256 are now written once over a description of a Merkle-Damgard hash function (`Impl/Pbkdf2/Md/X86.lean`: its streaming functions, hash value and length-field sizes, byte order, compression function and digest code), proven once against `Proof.MdStream.Md` and instantiated per hash. * `iterate` lays the block out once (U, 0x80, zeros, the length of a B + D-byte message), and each step is two compressions: the key's inner hash value with that block, then the outer one with the digest written word by word into it. The padding a truncated digest overwrites is written back, and T ^= U is computed word by word. * HMAC `finalize` calls the streaming `finalize` for the inner hash, then computes the outer hash with one compression of a fixed-layout block: the outer hash value and the digest copied word by word, the padding and length written as word stores, the MAC written to `out` (or, truncated, to scratch and copied). The whole PBKDF2 derivation calls the new functions. The streaming-level x86 `iterate` (`Impl/Pbkdf2/Generic/X86.lean`) and HMAC `finalize`, and their proofs, are removed; HMAC's `init` is unchanged. No change to TCB/ or Spec/, to the contracts, or to other targets. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RjfTK5YMk2jDsiKRYs2dbn

Conflicts were in the docs main trimmed (#571, #572): the registration files' boilerplate and the proofs' "Untrusted" sentence, dropped here too, including from the new modules. The streaming-level x86 files main edited stay deleted. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RjfTK5YMk2jDsiKRYs2dbn

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RjfTK5YMk2jDsiKRYs2dbn

…ntracts and code SHA-256 is now one more Merkle–Damgård hash function of the compression-level design (`Impl/Pbkdf2/Md/Arm.lean`, `Impl/Pbkdf2/Md/X86.lean`), with the contracts of `Spec.Hmac.sha256I` (`initApi`, `finalizeApi`, `iterateApi`, `pbkdf2Api`), as every other hash function on every target: * ARMv7: `sha256H` and its `HashOK` (`Proof/Hmac/Generic/Arm/Sha256.lean`), `sha256Md` (`Proof/Pbkdf2/Md/Arm/Sha256.lean`, where SHA-224's file now takes `sha256_comp` from), HMAC's `init` the generic one, and the whole of PBKDF2 rewired onto them (`Proof/Pbkdf2/Whole/Arm/Sha256.lean`). * x86: the backends' code (`Proof/Sha256/X86/Variants/Code.lean`: SHA-256's streaming functions, its Md `Hash` and the whole of PBKDF2's `Fns`, for a backend's compression and streaming functions), proven once for every backend (`Proof/Hmac/Generic/X86/Sha256.lean`, `Proof/Pbkdf2/Md/X86/Sha256.lean`, `Proof/Pbkdf2/Whole/X86/Sha256.lean`; taint checks evaluated once, on the sizes). `Backend` now carries the compression function, the streaming functions (`Sha256Stream`) and the `spSafe`/no-`esp`/stack facts of the code built on them; the fields only the specialized code used are gone. `Generic/Sha256/X86/{Hmac,Pbkdf2}.lean` emit `sha256I`'s init, finalize, iterate and pbkdf2 for each backend (with `_shani` for SHA-NI). Deleted: SHA-256's own 32-bit HMAC and PBKDF2 implementations and proofs (`Impl/Hmac/Arm.lean`, `Impl/Pbkdf2/Arm.lean`, `Impl/Hmac/X86.lean`, `Impl/Hmac/Sha256/X86.lean`, `Impl/Pbkdf2/X86.lean`, `Impl/Pbkdf2/Sha256/X86.lean`, `Proof/Hmac/Arm/`, `Proof/Pbkdf2/Arm/`, `Proof/Hmac/X86/`, `Proof/Hmac/Sha256/X86/`, `Proof/Pbkdf2/X86/`, `Proof/Pbkdf2/Sha256/X86.lean`, `Proof/Pbkdf2/Whole/X86/Sha256Fns.lean`) and what only they used (`Proof/Sha256/X86/Stream/{CompressAt,FinalizeVariant}.lean`, `Proof/Framework/TaintWeaken.lean`). Scrypt's ARM proof gets its own `wp_eor`; `sha256_repr` moves to `Proof/Hmac/Generic/Common.lean`. No change to `TCB/` or `Spec/`: the old SHA-256-specific 32-bit contracts there are now unused, for a later Spec-only PR to delete. Rust: `src/hmac/sha256.rs` uses `streaming_hmac!` on every architecture (the 32-bit `HmacHash` implementation is gone); `src/pbkdf2/sha256.rs` already used `whole_pbkdf2!`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RjfTK5YMk2jDsiKRYs2dbn

…lace `streaming_hmac!`'s `init` wrote the two streaming states into locals, moved them into the computation and wiped the locals; `finalize` copied the inner state out, finalized the copy and wiped it. They now work on the computation's own states (`state_mut`, replacing `state`), which its drop wipes: no copies, and 288 fewer bytes to wipe per MAC (on i686, about 450 fewer instructions per HMAC-SHA-256 MAC of a short message). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RjfTK5YMk2jDsiKRYs2dbn

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RjfTK5YMk2jDsiKRYs2dbn

HMAC's init, for every Merkle–Damgård hash on ARMv7 and 32-bit x86 (MD5, SHA-1, SHA-224 on ARMv7, SHA-256 and its SHA-NI variant on x86, and the SHA-384/512 family), now writes K₀ ⊕ ipad into the inner state's buffer with word stores of 0x36363636 and a byte loop over the key alone, derives K₀ ⊕ opad into the outer state's buffer word by word (XOR with 0x6a6a6a6a), sets each state's hash value with the streaming init, and compresses each block with one direct call of the compression function, instead of the streaming update. It is proven once for any Md hash against initContract, at the same stacks (Proof/Pbkdf2/MdInit.lean, Proof/Pbkdf2/Md/{Arm,X86}/HmacInit{,CT}.lean), and the whole PBKDF2 calls it. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RjfTK5YMk2jDsiKRYs2dbn

The scratch the streaming HMAC passes to init and finalize is only working space, whose contents the contracts do not depend on, as for AES-GCM and CMAC. Zeroing it (832 bytes for SHA-256) cost more than the new init saved: a short-message HMAC-SHA-256 MAC on i686 took 15790 instructions, against 15758 on main; it now takes 15329. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RjfTK5YMk2jDsiKRYs2dbn

The streaming-level HMAC init (Impl/Hmac/Generic/{Arm,X86}.lean: its key and pad loops, callUpd, init; and its proofs: Init's correctness, InitCT, Instances, Lit, and the init instances of Sha224/Sha256) is no longer used by any artifact, so it is deleted. What HMAC's finalize, PBKDF2's iterate and the whole PBKDF2 still use of it (the Hash record, callInit, callFin, the saved registers, copy and the xor loop, the contracts and HashOK, the hash functions' instances) moves next to the Md code, as Impl/Pbkdf2/Stream/{Arm,X86}.lean and Proof/Pbkdf2/Stream/{Arm,X86}/ (Init.lean becomes Common.lean), in the namespaces VG.Impl.Pbkdf2.Stream.* and VG.Proof.Pbkdf2.Stream.*. The module and registration-file docs describe the new init. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RjfTK5YMk2jDsiKRYs2dbn

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RjfTK5YMk2jDsiKRYs2dbn

…backends origin/main's scrypt (#573) calls the whole PBKDF2-HMAC-SHA256 through names this branch moved or replaced: the streaming-level helpers are now in VG.Impl.Pbkdf2.Stream.*, SHA-256's HashOK on ARMv7 is Proof.Pbkdf2.Stream.Arm.sha256OK, and on x86 a backend's PBKDF2 is Backend.F (with its streaming functions' stack bounds in Backend.stream). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RjfTK5YMk2jDsiKRYs2dbn

#578, #579 and #582 are now on main; this branch already carries #578 and #579 and builds on them, so its side is kept in the files both changed. src/hmac/mod.rs takes main's, which adds #582's uninitialized scratch. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RjfTK5YMk2jDsiKRYs2dbn

main's scrypt (#573) calls the whole PBKDF2-HMAC-SHA256 through names this branch replaced: SHA-256's HashOK on ARMv7 is Proof.Hmac.Generic.Arm.sha256OK, and on x86 a backend's PBKDF2 is Backend.F, with its streaming functions' stack bounds in Backend.stream. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RjfTK5YMk2jDsiKRYs2dbn

The scrypt proofs take this branch's side: it moved the streaming helpers to VG.{Impl,Proof}.Pbkdf2.Stream.*. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RjfTK5YMk2jDsiKRYs2dbn

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RjfTK5YMk2jDsiKRYs2dbn

#583 is now on main; this branch already carries it and builds on it, so its side is kept in every file both changed. The merge adds only #537. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RjfTK5YMk2jDsiKRYs2dbn

claude added 16 commits October 2, 2026 05:25

Merge remote-tracking branch 'origin/main' into claude/inspiring-pasc…

691a8ae

…al-labmxq-md-arm

Merge the ARMv7 and x86 compression-level HMAC/PBKDF2 branches

c084de2

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RjfTK5YMk2jDsiKRYs2dbn

Merge origin/main

782a7d7

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RjfTK5YMk2jDsiKRYs2dbn

Merge origin/main

6d98fe7

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RjfTK5YMk2jDsiKRYs2dbn

alex mentioned this pull request Oct 2, 2026

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

Merged

claude added 3 commits October 2, 2026 12:46

Merge origin/main

bd55984

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RjfTK5YMk2jDsiKRYs2dbn

alex marked this pull request as ready for review October 2, 2026 13:16

alex enabled auto-merge October 2, 2026 13:19

alex added this pull request to the merge queue Oct 2, 2026

Merged via the queue into main with commit ab2245f Oct 2, 2026
42 checks passed

alex deleted the claude/inspiring-pascal-labmxq-hmac-init-md32 branch October 2, 2026 13:30

This was referenced Oct 2, 2026

HMAC init proofs: one shared lemma module for all four targets #605

Merged

SHA-384/512/512-224/512-256 streaming on ARMv7 through the shared MdStream code #606

Merged

Navigation Menu

HMAC init on ARMv7 and x86: compress the padded key blocks directly - #586

HMAC init on ARMv7 and x86: compress the padded key blocks directly#586
alex merged 19 commits into
mainfrom
claude/inspiring-pascal-labmxq-hmac-init-md32

alex commented Oct 2, 2026 •

edited

Loading

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Milestone

Development

Uh oh!

2 participants

Conversation

alex commented Oct 2, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Proofs

Performance

Validation

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Milestone

Development

Uh oh!

2 participants

alex commented Oct 2, 2026 •

edited

Loading