[alex]

What

vg_aes_gcm_encrypt_blocks_aesni_pclmul_avx (the AES-NI+AVX interleaved loop, Impl.Gcm.X86_64.StitchAvx8.encFor) stored its first eight counter blocks and then read them straight back. initCounter writes the templates at scratch + 640 with 16-byte stores followed by 4-byte stores of each counter word, and the first batch loaded them with 16-byte loads. A load that overlaps two stores of different sizes cannot be forwarded from the store buffer. It waits until both stores reach the cache, which happens only after every older instruction retires. Those older instructions include the serial chain that computes H'² … H'⁸ and, in seal, the multiplication by H of the additional data. So the first AES rounds could not start until all of that had finished.

The first batch now builds its counters in registers (regCounters). It byte-reverses the counter block that initCounter loaded into xmm7, adds 1 to doubleword 0 with vpaddd seven times, and byte-reverses each result into the batch's registers. This is the same scheme as vg_aes_ctr32_aesni's ctrs. The templates are still written as before, for the later batches, whose loads come long after their stores. The rest of the loop is unchanged.

This is part of #1228, following the rustls analysis in #991, and targets the AES-NI+AVX backend's remaining gap in the 256 B–1 KiB range. Every seal and encrypt_in_place of 256 bytes or more on this backend goes through this loop. So does AesGcm::encrypt, which copies the text and seals it in place.

Measurements

Intel (local Xeon @ 2.10 GHz, pinned to one core). The AES-NI+AVX backend was selected with VG_CPU_FEATURES=avx,avx2,avx512f,avx512bw,avx512vl,bmi1,bmi2,adx,aes,pclmulqdq,ssse3, and aws-lc-rs was restricted to the same features with OPENSSL_ia32cap='~0x0:~0x574220200000'. Each run used a 13-byte AAD and took the best of 11; there were two alternating runs per side, main → this PR. "+1" is AesGcm::encrypt of n + 1 bytes from two slices.

key	bytes	in place	aws-lc-rs	out of place (+1)	aws-lc-rs (+1)
128	256	194, 194 → 174, 178	171–175	221, 219 → 209, 207	197–199
128	384	206, 208 → 188, 196	180–183	235, 236 → 224, 224	211–213
128	512	230, 230 → 213, 214	220–222	261, 262 → 247, 248	260–261
128	640	252, 253 → 232, 234	241–251	286, 288 → 271, 271	277–288
128	768	275, 278 → 255, 257	251–254	310, 312 → 298, 295	281
128	1024	319, 320 → 300, 302	311–312	358, 357 → 343, 343	347–351
128	1088	337, 340 → 319, 321	328–329	374, 375 → 365, 365	367
128	4096	865, 869 → 841, 852	877–891	945, 936 → 922, 951	936–948
256	384	226, 226 → 203, 207	202–211	256, 254 → 242, 240	236–243
256	1024	360, 362 → 340, 347	358–366	398, 400 → 383, 384	396–405
256	4096	990, 995 → 970, 977	1028–1032	1062, 1063 → 1047, 1059	1097–1099

At 16 KiB the change is within noise (one fixed cost per call).

AMD (CI's ubuntu-latest, AMD EPYC 9V45). Two Benchmarks runs (workflow_dispatch, VG_CPU_FEATURES=aes,avx,pclmulqdq,ssse3, module aes_gcm) compared against main (run 1, run 2). Both runs landed on AMD runners:

benchmark	run 1	run 2
aes-128-gcm-encrypt/384	176 → 168 ns (4.3%)	188 → 166 ns (11.8%)
aes-128-gcm-encrypt/1024	276 → 269 ns (2.6%)	298 → 280 ns (6.0%)
aes-128-gcm-encrypt-out-of-place/384	190 → 184 ns (3.6%)	193 → 190 ns (1.6%)
aes-128-gcm-encrypt-out-of-place/1024	294 → 286 ns (2.7%)	314 → 301 ns (4.2%)
aes-128-gcm-encrypt-two-pieces/384	197 → 184 ns (6.9%)	204 → 197 ns (3.5%)
aes-128-gcm-encrypt-reused-key/600	180 → 171 ns (4.6%)	193 → 188 ns (2.5%)

Unchanged code (decryption, AES-GCM-SIV) moved by up to ±3% in run 1 and up to 6% in run 2, so the second run is noisier.

Proofs

Assembly comes only from the Lean code. Spec, TCB and contracts are unchanged.

• batch is now batchL (loads n). batchL ld takes any code ld that leaves the batch's counter blocks in aregs (CountersIn), changing only rax, xmm11, xmm12 and aregs (LdFrame). cipherBatch_ok and batchL_ok are stated for any such ld. batch_ok and CoreInv.bareBatch are the loads_ok instances.
• regCounters_ok (AesHash.lean) proves the new code's counters from the counter block in xmm7, using paddd_one and pshufb_rev_rev. Ready gains the two facts it needs after the setup: the mask in xmm0 and the counter block in xmm7, which setupPrefix_ok already established.
• The constant-time proof (Ct.lean) covers the new code unchanged: it touches only registers, and its one constant is public.
• block_counts_agree (from AES-GCM x86-64: AES-NI+AVX encryption loop takes every block from 16 on #1684) already compares every block count from 16 to 41 against the scalar baseline on every detected backend.

🤖 Generated with Claude Code

https://claude.ai/code/session_01FoYWDDEDFq1DFev5X7n2aq

---

Generated by Claude Code