[alex]

What

On the AES-NI+AVX backend (_aesni_pclmul_avx), vg_aes_gcm_encrypt_blocks interleaved counter mode and GHASH only over the first 16 ⌊n / 16⌋ blocks. It encrypted the rest with vg_aes_ctr32_aesni and hashed them with vg_ghash_pclmul. At 384 B, for example, 8 of the 24 blocks took that path, at about 60 ns.

The encryption loop (Impl.Gcm.X86_64.StitchAvx8.encFor) now takes every block from 16 on, and Blocks.stitchPart gives it all of them (full, as the AVX-512 prepared loop already does):

• The pipeline still runs in groups of 8. With n = 16 + 8 k + t blocks it stops with t < 8 blocks left, rather than requiring n to be a multiple of 16.
• When t > 0, tailT encrypts the 8 counters the pipeline has already prepared (ksTail, stored at scratch + 832). It advances the counter by t and points at the powers H'ᵗ … H' (tailSetup). It then runs the AVX-512 loop's verified per-block body (StitchZH.remBody/remNext) over the t blocks: XOR with the keystream, store, and accumulate the product with the block's power. Finally it does one reduction into Y (tailEnd).
• r9 (the number of blocks) is public, so the branch and the loop are covered by the existing constant-time check, now run on stitchPart … full.

Decryption is unchanged.

This is part of #1228, following the rustls analysis in #991. It addresses the AES-NI+AVX backend's gap in the 256 B–1 KiB range. encrypt_in_place and AesGcm::encrypt's copy-and-seal path for short texts both reach this code through 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'. The machine is a Xeon, pinned to one core, with a 16-byte key and 13-byte AAD. Each cell is best-of-11 in ns, two alternating runs, main → this PR. "+1" is AesGcm::encrypt of n + 1 bytes from two slices; for aws-lc-rs it is copy plus seal_in_place_separate_tag.

bytes	in place	aws-lc-rs	out of place (+1)	aws-lc-rs (+1)
384	251, 247 → 190, 190	168–181	306, 312 → 252, 255	201–213
640	283, 273 → 239, 236	227–240	340, 337 → 297, 313	270–283
1024	308, 307 → 303, 303	295–317	391, 389 → 372, 371	328–351
1088	328, 351 → 331, 323	305–312	402, 411 → 394, 375	344–361
256, 512, 768	unchanged (multiples of 16 blocks)

The largest gain is in-place encryption at 384 B: 24% faster, now within about 10% of aws-lc-rs.

Proofs

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

• Proof/Gcm/X86_64/StitchAvx8/Tail.lean (new) proves the tail (tail_ok). It reuses StitchZH.remLoop_ok, and a TailLaw that Ok.lean proves of the setup's powers, as remZ does for the AVX-512 tables.
• The loop proofs no longer need nb mod 16 = 0. StitchAvx8.enc_ok holds for any nb ≥ 16.
• StitchImpl gains full and okFull, and StitchImpl.code passes them to StitchCode. The base-context encrypt_blocks instances pass full to Blocks.encrypt. Only StitchName.aesniAvx sets it.
• New unit test block_counts_agree: every block count from 16 to 41, whole or with 5 extra bytes, for 128-, 192- and 256-bit keys. It runs on every detected backend and compares against the scalar baseline.

🤖 Generated with Claude Code

https://claude.ai/code/session_01FoYWDDEDFq1DFev5X7n2aq

---

Generated by Claude Code

[alex]

merge conflicts