[alex]

What

On the AES-NI+AVX backend (_aesni_pclmul_avx), vg_aes_gcm_seal handles the end of the text with calls: vg_aes_ctr32_aesni for the keystream of the last partial block, vg_ghash_pclmul for the padded tail and again for the lengths block, then vg_aes_ctr32_aesni once more for the tag's E(K, J₀). A profile of a 385-byte AesGcm::encrypt showed vg_ghash_pclmul and vg_aes_ctr32_aesni taking about 25% of the time; at 1025 bytes they took 17%. This is most of the out-of-place gap to aws-lc-rs, and it affects every text that doesn't end on a block boundary.

#1485 removed these calls from the AVX-512 seal (Short.finish). This PR makes that end usable without AVX-512:

• Short.finish becomes Short.finishWith ks, parameterised by the program that computes the keystream of J₀ and of the counter block into K. The AVX-512 finish is finishWith finKs, unchanged.
• Short.finKsA computes the same two blocks with AES-NI on 128-bit registers (AesNi.aes [xmm5, xmm7]).
• SealFin.seal is the other instances' seal up to the whole blocks, then finishWith finKsA. GcmImpl.fin, set by StitchName.fin for the AES-NI+AVX loops only, selects it in sealCode. That covers seal, seal_precomputed, seal_prepared and the gather's seal.

open is unchanged.

This is part of #1228, following the rustls analysis in #991. It is independent of #1684 (the AES-NI+AVX loop's tail), which changes encrypt_blocks rather than seal.

Measurements

Measured with the AES-NI+AVX backend chosen (VG_CPU_FEATURES=avx,avx2,avx512f,avx512bw,avx512vl,bmi1,bmi2,adx,aes,pclmulqdq,ssse3), and aws-lc-rs masked to the same with OPENSSL_ia32cap='~0x0:~0x574220200000'. Xeon, pinned to one core, 16-byte key, 13-byte AAD, best-of-11 in ns, two alternating runs each, main → this PR. "+1" is AesGcm::encrypt of n + 1 bytes from two slices, so the text ends inside a block; for aws-lc-rs it is a copy plus seal_in_place_separate_tag.

bytes	out of place (+1)	aws-lc-rs (+1)
256	242, 242 → 211, 214	184–197
384	297, 290 → 277, 278	206–212
512	285, 277 → 250, 259	254–265
640	346, 337 → 313, 313	269–281
768	335, 328 → 296, 310	270–290
1024	381, 383 → 341, 362	334–343
4096	972, 1011 → 914, 914	912–920

Texts ending inside a block are 20–60 ns faster. At 512 and 4096 bytes the out-of-place path is now level with aws-lc-rs. In-place texts of whole blocks take the same path's no-tail branch and are unchanged within noise.

Proofs

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

• Short/Finish.lean: sealBodyF_ok takes the keystream program and its spec (KsOk ks, finKs_ok's effect, with xmm8 also written); finKs_ksOk instantiates it.
• Short/CT.lean: finish_rel and sealRunF_rel take KsOk ks and KsRel ks, the keystream program in two runs; finKs_rel is the AVX-512 piece that was inline.
• Short/KsA.lean (new): finKsA_ksOk (from AesNi.aes_ok) and finKsA_rel (taint_decide: the rounds in rsi are public).
• Short/SealFin.lean (new): SealFin.seal's correctness (sealM_of with sealRunF_ok), constant time (sealM_relOf with sealRunF_rel), and its mxcsr, rsp and stack facts. The selectors in Short/Verified.lean, Prepared/Short.lean and the generic file gain the third case.

The existing tests cover the new path on CPUs with these features: long_tails_agree, which checks every backend the CPU can run against the scalar one with partial tails, plus the Wycheproof and CAVP AES-GCM vectors.

🤖 Generated with Claude Code

https://claude.ai/code/session_01FoYWDDEDFq1DFev5X7n2aq

---

Generated by Claude Code