[alex]

This comes from the rustls provider analysis in #991 (#1228). It is the first PR replacing the dispatch of #1350/#1354 with real speedups in the assembly: AesGcm::encrypt stays a thin call into vg_aes_gcm_seal_gather, and there is no Rust change at all.

What changes

vg_aes_gcm_encrypt_blocks_to_vaes_vpclmul (VAES + VPCLMULQDQ on 256-bit registers) now encrypts from src to dst in the interleaved AES/GHASH loop (Impl.Gcm.X86_64.StitchTo). Before, it copied the blocks to dst and then encrypted them there in place. This is what the AVX-512 variant already does (StitchZTo).

The loop is Stitch.enc with StitchZTo's setup tail (setupCTo). That sets r8 ← src - dst and points rdx at dst. Each pair of plaintext blocks is loaded from [rdx + r8 + 32 j] and the ciphertext is stored to [rdx + 32 j], where the GHASH loads read it back as before.

seal_gather's copy threshold (copyBelow) is now chosen by the variant's out-of-place loop:

• 768 bytes for AVX-512, as before.
• 16 KiB for this loop. Below that, a slice that ends within a block, which the streaming functions buffer, costs more than the copy saves. Measured with the threshold at 768, unaligned records of 767 B–4 KiB were 10–48% slower than main.

The threshold comes down once the streaming path handles a block split across slices without buffering it, which is the next PR.

No Spec or TCB change. In src/asm/x86_64/gcm.rs, only vg_aes_gcm_encrypt_blocks_to_vaes_vpclmul (the new loop) and vg_aes_gcm_seal_gather_vaes_vpclmul (its threshold, and its documentation) change.

Proofs

Proof/Gcm/X86_64/StitchTo/ reuses the in-place loop's lemmas through the in-place view of the out-of-place state (StitchZTo.dst), as StitchZTo does:

• Base.lean: the out-of-place XOR of the keystream (xorDataKTo_ok).
• Aes.lean: a batch of eight blocks (batchTo_ok).
• Loop.lean: the loop invariant, the body (the batches with the previous group's GHASH between their rounds), the first group, the loop, and the final stores.
• stitchTo_ok (in StitchZ/OkP.lean, which already imports the field algebra, to keep Poly's importers within check_lean_speed's limit): the contract StitchToOkM M for every kind of key context.
• The variant's constant-time and static facts (toPart) are checked by taint_decide and decide +kernel, as for AVX-512.

Measurements

These are AesGcm::encrypt of two pieces (n bytes, then 1 byte), with a 13-byte AAD and a warmed key, using VG_CPU_FEATURES=aes,avx,avx2,pclmulqdq,ssse3,vaes,vpclmulqdq on an Ice Lake–class Xeon. Each value is the minimum of 33 interleaved samples, in ns. "copy+ip" copies the pieces and calls encrypt_in_place.

n	copy+ip	main	this PR	this PR / main
256	189.1	199.0	200.8	1.009
767	207.2	228.6	229.5	1.004
1023	237.2	257.3	255.4	0.993
2047	352.3	375.8	367.9	0.979
4096	602.9	607.0	604.7	0.996
8192	1026.3	1048.3	1041.8	0.994
16383	1846.0	1932.9	1832.3	0.948
16384	1868.3	1940.7	1752.8	0.903
65535	8546.7	8496.6	6581.7	0.775
65536	8560.7	8550.4	6517.5	0.762
131071	16558.8	16471.4	12963.9	0.787

Below 16 KiB the code path is the same as main's (within noise). From 16 KiB, encrypting from the pieces is 5–10% faster than main at 16 KiB and 21–24% faster at 64–128 KiB, also beating copy+ip. The other backends' code is byte-identical.

Validation

• lake build (full) and lake env lean --run Emit.lean (axiom and compiler audits; the generated code is committed).
• cargo test with Wycheproof on the default backend, and the AES-GCM tests with VG_CPU_FEATURES set to the VAES-AVX2 configuration and to none. prepared_gather_tails encrypts 16 KiB plus a suffix from pieces on every backend, which reaches the new loop.
• cargo fmt --check, cargo clippy --all-targets -- -D warnings.
• ci/check_lean_imports.py, check_lean_speed.py, check_vectors.py, check_arch_gates.py, check_variants.py, check_mcdt.py, cpu_tests.py lint, algorithms_table.py --check.

🤖 Generated with Claude Code

https://claude.ai/code/session_01FoYWDDEDFq1DFev5X7n2aq

---

Generated by Claude Code