[alex]

Spec change (trusted). This PR adds one contract and Api to Spec/Hmac/Generic.lean. It changes no existing contract, adds no TCB, and adds no implementation.

What it specifies

vg_hmac_<hash>_keyed(inner: *const [u8; S], outer: *const [u8; S], msg: *const u8, len: usize, out: *mut [u8; D]):

• inner and outer are the two streaming states that vg_hmac_<hash>_init leaves, representing K₀ ⊕ ipad and K₀ ⊕ opad.
• The function writes HMAC(K₀, msg) to out, for every block-size key K₀ that the states represent.
• Both states are read only, so a caller keeps them for the key's next message.

Contract (keyedPost), stated with finalizePost's quantifier: for all k0, if k0.length = blockSize, k0.length + len < 2⁶⁴, Repr m inner (xorPad k0 ipad) and Repr m outer (xorPad k0 opad), then bytesAt m' out D = hmacBlockKey H k0 (bytesAt m msg len).

• Only pointers and len are public. The states and the message are secret.

Api: Instance.keyedApi, generic like init and finalize, so it covers every HMAC instance: SHA-256, SHA-384, and the rest.

Why

TLS 1.3's key schedule (HKDF-Expand-Label) runs many short HMACs under a few keys, about 60 per resumed handshake pair. Today each one is several Rust-driven calls:

1. clone the keyed state;
2. update;
3. finalize;
4. wipe the cloned state on drop.

Locally (Emerald Rapids, SHA-NI, rdtsc minimums), a 32–50 B HMAC-SHA256 that way costs about 340 TSC cycles, of which the two compressions are about 190. That is about 150 cycles of overhead per HMAC. With one verified call per HMAC, I project 50–65 cycles saved per short HMAC.

HKDF-Expand with one output block is HMAC(PRK, info ‖ 0x01), so it is one _keyed call with no further Spec.

Next

The implementation PR comes after this merges. It will be generic over SHA backends on each target (Generic/MdHash/<Target>/), so it gets every variant: x86-64 scalar, SHA-NI and AVX2; the AArch64 SHA extensions; x86; and ARM. It will add the Rust Hmac::mac_keyed.

---

Generated by Claude Code

[alex]

I don't really understand what this is for, it sounds like maybe you want an update_and_finalize operation?

[alex]

It's close to that. keyed computes the whole MAC of one message from the two states init leaves: keyed(inner, outer, msg, len, out, scratch). It copies the inner state into scratch, runs update on the copy, then runs HMAC's finalize with the outer state. It only reads inner and outer. That lets a key's precomputed states be reused for every message, which is what Hmac::mac and a rustls provider (#991) need. Today that takes three verified calls plus a Rust copy of the state; this is one verified call. The 16-byte copy inside the asm also avoids a store-forwarding stall that the Rust copy caused.

Measured on the Impl branch (claude/hmac-keyed-impl, x86-64 SHA-NI, not yet opened as a PR):

Row	Before	After
hmac-sha256/64	328 ns	285 ns (−12.8%)
hmac-sha384/64	997 ns	966 ns (−3.0%)
keyed alone, SHA-256/64		161 ns

The long rows are unchanged, within noise.

An update_and_finalize(inner: *mut state, count, outer, msg, len, out) would work too. It updates the inner state in place and finalizes, leaving the copy to the caller. That would also cover Hmac::update + finalize, but the Rust copy would come back for the reusable-key case: the copy is where the stall happened. A copy done in Rust would also go against keeping copies in verified code.

My preference is to keep keyed as written. If you'd rather have update_and_finalize, or both, I'll rework this spec before opening the Impl PR. Which do you want?

---

Generated by Claude Code

[alex]

I guess I don't understand what the semantics of _keyed are, or how it maps to a Rust API.

[alex]

Here are the exact semantics and the Rust mapping.

Semantics (keyedPost). Inputs:

• vg_hmac_<h>_keyed(inner, outer, msg, len, out)
• inner and outer are the two streaming hash states that vg_hmac_<h>_init produces for a key. They represent K₀ ⊕ ipad and K₀ ⊕ opad, each one block absorbed.

What it does: it writes HMAC(K₀, msg[..len]) to out.

Both states are *const. The function never writes them, so they are still valid for the next message.

Equivalently, it does the same as this sequence, in one verified call:

1. copy inner
2. update(copy, msg)
3. finalize(copy, outer)

Rust mapping (on claude/hmac-keyed-impl):

• Hmac::<H>::mac(key, data) becomes init (into a local state) followed by _keyed, instead of init + update + finalize. This is where the −12.8% at hmac-sha256/64 comes from.
• New: Hmac::<H>::mac_keyed(&self, data) -> H::Output returns the MAC of everything absorbed so far followed by data, leaving self unchanged (like self.clone().update(data).finalize()). Use with a fresh Hmac::new(key), kept per key. It MACs each message without recomputing the key's states or touching the original. When self has absorbed nothing, it is one call to _keyed; otherwise it falls back to clone + update + finalize.

mac_keyed is what a rustls hmac::Key::sign maps onto: the key is set up once, then signed with many times through &self. That's the use in #991.

If &self with clone semantics isn't the API you want, update_and_finalize(inner: *mut, outer, msg, len, out) would support Hmac::update + finalize and any number of absorbed bytes. The cost is that mac_keyed would copy the state in Rust first. Would you rather have that, or a separate HmacKey type with only new(key) and mac(&self, data) instead of a method on Hmac?

---

Generated by Claude Code

[alex]

What you're describining sounds identical to update and finalize, so I don't even know what the difference is.

[alex]

You're right. It is update + finalize on a copy of the inner state, fused into one call, and the fusion buys almost nothing. I measured both at 64 bytes on a SHA-NI machine:

• _keyed: 159 ns.
• The existing calls (copy + update + finalize): 161 ns.

Almost all of the gain on hmac-sha256/64 comes from the Rust side, not from a new primitive:

• Hmac::mac calls the verified init, update and finalize directly, with the states on the stack, instead of going through new/update/finalize.
• mac_keyed (sign many messages with one key's states) copies only the inner state.

That change alone is −9.5% to −12.4% at 32–64 B, with no new spec.

I suggest closing this PR and opening that Rust-only change instead. It's ready on claude/hmac-fast-mac and adds no Lean. OK to do that?

---

Generated by Claude Code

[alex]

yes