[alex]

What

The AES-NI+AVX interleaved loop (Impl.Gcm.X86_64.StitchAvx8) computes H'² … H'⁸ on every call. That is a serial chain of multiplications at the start of every seal of 256 bytes or more. With AAD it lands on the GHASH chain's critical path: at 384 B with a 13-byte AAD it costs about 7–9 ns.

The AVX-512 backend avoids this with the _prepared instances. Once a key has made POWERS_AFTER long calls, Powers::get computes a 1024-byte key context with the powers (Spec.Gcm.PreparedPowersRepr), and the loops read them from it. This PR gives the AES-NI+AVX variant the same instances:

• StitchAvx8.encR: enc with setupR, whose setupGR loads H' … H'⁸ from the prepared context into the registers where setupG computes them (preg i, at prepOff (i + 1)). It is otherwise the same code: encForWith setupR. Decryption keeps dec.
• Variant: StitchName.encR/fullR for .aesniAvx, and the variant's pieceR. The generic file then emits its _prepared instances (init, seal, open, seal_gather, stream_encrypt/decrypt, the block functions), with StitchAvx8.stitchR_ok as okR.
• Key setup: vg_aes_gcm_init_prepared is the generic one, whose conversion uses AVX2. Its features now name avx explicitly, since the callees of this variant don't. The AES-NI+AVX backend needs only AVX, so Backend::prepared returns the backend's _prepared instances only where the CPU also has the key setup's features (here, AVX2). Sandy and Ivy Bridge keep computing the powers.
• Rust (src/aes_gcm.rs): the hard-coded _prepared_vaes_vpclmul_avx512 calls become a table per backend (Prepared), chosen by an exhaustive match in Backend::prepared. Powers holds the key's table, looked up once in AesGcm::new. It also now counts the calls before the powers with a relaxed load and store rather than a locked fetch_add: a count lost to a race only delays the powers. Without that, a key used for a single long message measured 7–15 ns slower than on main. The AVX-512 backend gets the same saving.
• CI: a rust-cpu-features line and a CPU_FEATURES configuration for aes,avx,avx2,pclmulqdq,ssse3. That configuration now chooses differently from aes,avx,pclmulqdq,ssse3 (the prepared instances), so it is tested and benchmarked.

This is part of #1228, following the rustls analysis in #991. A connection's key encrypts many records, which is the reused-key case.

Measurements

Intel (local Xeon @ 2.10 GHz, pinned to one core). The backend was AES-NI+AVX with AVX2 (VG_CPU_FEATURES=avx,avx2,avx512f,avx512bw,avx512vl,bmi1,bmi2,adx,aes,pclmulqdq,ssse3), and aws-lc-rs was masked to the same features (OPENSSL_ia32cap='~0x0:~0x574220200000'). Each run used one key reused across messages and a 13-byte AAD, and took the best of 11. There were two alternating runs per side, #1750 (now 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	179, 179 → 169, 170	172	210, 213 → 186, 188	199–202
128	384	191, 191 → 183, 183	182–185	224, 225 → 202, 204	211–212
128	512	214, 216 → 204, 204	220–221	252, 252 → 226, 226	263–265
128	640	237, 238 → 227, 228	241–243	273, 274 → 251, 251	279–281
128	768	258, 260 → 249, 251	251–252	299, 300 → 277, 280	282–286
128	1024	304, 309 → 294, 295	311–314	346, 346 → 325, 324	349–351
128	1088	324, 325 → 310, 311	325–326	369, 366 → 343, 341	369–372
128	4096	845, 851 → 832, 834	873–876	931, 931 → 904, 901	935–937
256	384	206, 207 → 197, 198	201–202	244, 244 → 223, 218	237–239
256	1024	338, 347 → 331, 443*	355–359	384, 388 → 360, 358	397–399
256	4096	978, 979 → 964, 975	1021–1024	1057, 1060 → 1031, 1033	1087–1088

* one outlier; the other run gave 331.

AES-NI+AVX now matches or beats aws-lc-rs at every size here. With a new key for each message (the case POWERS_AFTER exists for), the cost per message is unchanged within noise: 257–269 ns → 258–267 ns at 384 B, and 370–382 → 371–380 at 1 KiB, encrypting.

AMD (CI, AMD EPYC 7763): Benchmarks run against main:

benchmark	aes,avx,avx2,pclmulqdq,ssse3	aes,avx,pclmulqdq,ssse3
aes-128-gcm-encrypt-reused-key/600	291 → 258 ns (11.4%)	291 → 293 ns (0.5% slower)
aes-128-gcm-encrypt-reused-key/1350	474 → 440 ns (7.2%)	474 → 476 ns (0.3% slower)
aes-128-gcm-encrypt-reused-key/4000	1.11 → 1.10 µs (1.2%)	1.11 → 1.12 µs (1.0% slower)
aes-128-gcm-encrypt-two-pieces-reused-key/600	325 → 294 ns (9.7%)	326 → 329 ns (1.0% slower)
aes-128-gcm-encrypt-two-pieces-reused-key/1350	520 → 491 ns (5.6%)	519 → 524 ns (1.0% slower)

The fresh-key benchmarks (encrypt, decrypt, out-of-place, two-pieces, stream), which never reach the prepared context, moved by 0–4% either way in both configurations. The configuration without AVX2 runs the same code as before. An earlier run on an EPYC 9V45, before the call-counting change, showed reused-key 3.6–9.6% faster and streaming up to 13% faster.

Proofs

Assembly comes only from the Lean code. Spec, TCB and contracts are unchanged (Spec.Gcm.PreparedPowersRepr and the _prepared contracts already exist).

• setup_ok and encFor_ok are now instances of setupWith_ok (any code leaving what setupG does: GPost) and encForWith_ok (any setup leaving Ready and the powers' law).
• setupGR_ok: setupGR lowers to SSE (lane0_setupGR), whose loads give readW (ctx + prepOff n) = hInvF (Hⁿ) (prep_val, from StitchZR.pair_values). Since x · φ (hInvF (Hⁿ)) = φ(H)ⁿ (x_φ_hInvF), this is GPost. So encR_ok and stitchR_ok : StitchOkM CtxMode.prepared encR dec 1 follow. These live in StitchAvx8/Ok.lean, the loop's one module with the field algebra, which keeps Poly.lean's importers at 40.
• Constant time: encR_piece : Piece encR true true and decR_piece : Piece dec true (Ct.lean, encR materialized).
• Tests: prepared_boundaries and powers now run on every backend with prepared instances this CPU runs, not only VaesVpclmulAvx512.

🤖 Generated with Claude Code

https://claude.ai/code/session_01FoYWDDEDFq1DFev5X7n2aq

---

Generated by Claude Code