[alex]

This builds on #1331 (now on main) and also covers its prepared-context gather. #1354 is stacked on this PR.

This comes from the rustls provider analysis in #991. The provider seals TLS records with AesGcm::encrypt (vg_aes_gcm_seal_gather) from two pieces, the payload and the content-type byte. On x86-64 that is slower than copying into the output and calling encrypt_in_place (#1228). This is the first of the PRs addressing that.

What changes

vg_aes_gcm_seal_gather now compares the text's length with a threshold of its variant:

• Below the threshold: it copies the slices to dst and encrypts them there with one call of the same variant's vg_aes_gcm_seal (_seal_prepared for Speed up AVX-512 AES-GCM TLS records with prepared keys and direct gather #1331's prepared context). That keeps seal's AVX-512 short path. The copy moves 64 bytes at a time through xmm0–xmm3, then 16 bytes, then single bytes. It uses only SSE2, so every variant can use it.
• Otherwise: the streaming path runs as before.

The threshold (copyBelow in Generic/AesGcm/X86_64/AesGcm.lean):

• 768 bytes for variants with out-of-place interleaved loops (VAES + VPCLMULQDQ + AVX-512). This is about where streaming starts to beat the copy (measured below).
• 2³¹ − 1 for the others. Their streaming path already copies every block, one at a time, before encrypting in place. Copying 64 bytes at a time and making a single call is faster at every length.

There's no Spec or TCB change. The Rust changes are tests only: backends_agree now crosses the 768-byte threshold and adds the TLS shape (payload plus one byte).

Proofs

• Gather/Copy.lean: the copy. One generic chunk-loop lemma covers the 64-, 16- and 1-byte loops.
• Gather/CopyLoop.lean: the slices gathered. It reuses ChaCha20-Poly1305's descriptor walk (next/advance and GatherPre/GInv from ChaCha20-Poly1305: out-of-place encryption from a list of slices (seal_gather) on every target #1324) with this copy.
• Gather/CopyPath.lean, SealCallee.lean, SealCall.lean, Prepared/GatherSeal.lean: the path's blocks, and the call of vg_aes_gcm_seal through its shared contract, the same way the gather already calls the streaming functions.
• Gather/CopyCT.lean: constant time. The copy branches only on public lengths and descriptors. The length test compares with an immediate, so it accesses no memory (rel_cmpImm), and the proof holds for any threshold below 2³¹.
• Gather/Fn.lean, Gather/CT.lean, Gather/Verified.lean: recomposed. The streaming path's proofs are unchanged.

The emitted change is only to the 12 vg_aes_gcm_seal_gather* functions in src/asm/x86_64/gcm.rs. The other 155 GCM functions are byte-identical.

Measurements

These are encrypt of two pieces (n bytes, then 1 byte) with a 13-byte AAD and a warmed key, on an Intel Xeon with VAES/VPCLMULQDQ/AVX-512 (Ice Lake class, 2.1 GHz, noisy cloud host). Each value is the minimum of 33 interleaved samples, in ns. "Before" is #1331's code without this PR. "copy+ip" copies the pieces into the output and calls encrypt_in_place. Smaller backends were selected with VG_CPU_FEATURES.

VAES + VPCLMULQDQ + AVX-512

n	copy+ip	before	after
16	66.0	132.1	84.7
64	71.9	147.4	86.4
128	76.4	163.1	91.4
256	99.2	168.3	126.4
384	117.9	224.3	140.3
511	131.2	276.7	155.6
640	219.9	234.2	233.3
1024	196.5	213.5	212.6
4096	415.9	407.9	415.8
16384	1330.6	1221.2	1256.1

At and above the threshold the code is the same as before, so the differences there are noise.

AES-NI + PCLMULQDQ + AVX (aes,pclmulqdq,ssse3,avx)

n	copy+ip	before	after
16	105.9	132.9	121.8
511	220.7	368.5	255.8
2048	537.9	580.5	566.3
4096	911.6	992.2	940.2
16384	3123.0	3371.9	3218.5

VAES + VPCLMULQDQ, AVX2 (…,vaes,vpclmulqdq without AVX-512)

n	copy+ip	before	after
16	105.5	130.2	122.0
511	163.9	309.8	184.8
2048	347.1	396.6	376.1
16384	1843.0	2094.2	1928.1

AES-NI + PCLMULQDQ (aes,pclmulqdq,ssse3)

n	copy+ip	before	after
16	105.8	129.3	121.7
511	231.8	301.9	245.1
16384	4732.7	4975.7	4807.6

What's left (follow-up PRs, in progress)

• A fixed ~15–20 ns remains on every gather call: the descriptors, the gather's argument frame and work slots, and the extra call layer. With zero-length text, the gather costs 77 ns against copy+ip's 59 ns. AES-GCM on x86-64: encrypt copies a short text and seals it in place #1354, stacked on this PR, gives AesGcm::encrypt a Rust fast path for that: below a threshold it copies the pieces into out and seals them in place.

• Out-of-place interleaved loops for AES-NI + AVX and VAES on 256-bit registers. These are planned as follow-up PRs. Their upper bound is the cost of the copy, measured as the gap between encrypt_in_place without a copy and copy+ip:

  backend	≤ 16 KiB	≥ 64 KiB
  AES-NI + AVX	5–10%	16–19%
  VAES + VPCLMULQDQ, AVX2	9–19%	28–30%

• AVX-512 block remainder (follow-up PR). On AVX-512, the blocks left after the 16-block interleaved loop (1–15) go through separate vg_aes_ctr32 and vg_ghash calls. Even in place, that costs about 25 ns plus 5 ns per block: 31 blocks take 221 ns against 135 ns for 32, and 47 take 235 ns against 155 ns for 48. Speed up AVX-512 AES-GCM TLS records with prepared keys and direct gather #1331's two-slice path pays the same cost whenever its payload is not a multiple of 16 blocks.

• AVX-512 pieces that end mid-block (follow-up PR, after the remainder fix). In the gather's streaming path, such a piece costs about 100 ns, because the partial block is buffered.

Validation

Rerun after restacking onto main:

• lake build (full) and lake env lean --run Emit.lean (no changes to the generated code; axiom and compiler audits).
• cargo test with Wycheproof on the default backend, and with VG_CPU_FEATURES=none for the AES-GCM tests. Before the restack, the AES-GCM tests also ran with aes,pclmulqdq,ssse3,avx and all eleven x86-64 backend configurations.
• 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.

🤖 Generated with Claude Code

https://claude.ai/code/session_01FoYWDDEDFq1DFev5X7n2aq

[alex]

Rust coverage failed on 16dc7e5 at src/aes_gcm.rs:1904. That line belongs to the base, not to this PR: it is the message of the assert_eq! in prepared_gather_tails, which #1331 added in 47257c3. The message only runs when the assertion fails, so on a line of its own it is never covered, and #1331's head fails the same check.

I ported a fix into this PR in 7d57c54: the test formats the message from one value, so the assertion fits on one line. An instrumented run of the test now covers every line of its loop. If #1331 makes the same change, this commit becomes a no-op. #1354 is restacked on top.

---

Generated by Claude Code

[gaynor-anthropic]

Why are we adding a bunch of dispatch code to the rust, instead of just making the function faster?

[alex]

Answering this even though the PR has merged, since I missed it before: you're right. This PR has no Rust dispatch (its Rust changes are tests), but its copy-then-call-seal path is still dispatch around a slow function rather than a faster one. The Rust dispatch was in #1354, which I've closed.

The follow-ups make vg_aes_gcm_seal_gather itself fast, so that the copy path can be removed:

• out-of-place interleaved loops for every backend, so the pieces are never copied (VAES AVX2 first; its proof is done);
• lower fixed per-call overhead;
• a short-input path inside the gather;
• a block split across pieces handled without buffering;
• the AVX-512 remainder handled in the loop.

I'll answer review comments on each of those PRs as they come.

---

Generated by Claude Code