[alex]

What

vg_aes_gcm_seal_gather (AesGcm::encrypt) copies each slice to the output and seals it there when the whole text is short (under 768 bytes on AVX-512). This copy also runs in the _prepared instance. The copy moved 64 bytes at a time, then 16, then up to 15 more one byte at a time. That byte loop cost about 1.5 ns per byte, so a 15-byte tail cost 20–25 ns, much of the gap between encrypt and copy-then-encrypt_in_place.

Now, when a slice of at least 16 bytes has a remainder after the 16-byte loop, a single 16-byte move copies its last 16 bytes (copyLast). The bytes before the remainder are copied a second time with the same values. Slices shorter than 16 bytes still go one byte at a time.

Part of #1228, for the small, few-slice encryptions from the rustls analysis in #991.

Measurements

AesGcm::encrypt with a reused key, 13-byte AAD and 12-byte nonce, on an AVX-512 Xeon (VAES, VPCLMULQDQ). Each cell is the better of two best-of-11 runs, in ns, base → this PR. [2] splits the text at n/2 + 3, so both slices have a tail. encrypt_in_place is shown for reference.

bytes	encrypt_in_place	encrypt [n]	encrypt [2]
64	74	86 → 86	90 → 83
100	77–79	90 → 90	117 → 88
128	79	88 → 87	111 → 88
200	90	107 → 100	111 → 100
255	105	144 → 121	149 → 129
300	109	146 → 139	148 → 140
767	209	233 → 227	233 → 228

Two slices of 100–128 bytes are about 20–25% faster, and a 255-byte text about 16%. Block-aligned single slices (64, 128) are unchanged.

Proofs

Proof/AesGcm/X86_64/Gather/Copy.lean: copyLast_ok proves that, after j ≥ n - 16 bytes, one more 16-byte write at n - 16 leaves exactly the n bytes copied. It uses a new lemma, writeBytes_over: writing ys over xs from the same address, with ys at least as long, is just writing ys. setupLast_ok covers the n < 16 test, and CInv.readW' reads the source at any offset. The constant-time proof is unchanged in shape: copy_check is re-checked by taint_decide, and the new branch depends only on the slice length. Spec, TCB and contracts are unchanged.

Checks

• Full lake build, then the emitter. Only src/asm/x86_64/gcm.rs changes.
• ci/check_lean_speed.py, check_lean_imports.py, check_vectors.py, check_arch_gates.py, check_variants.py, check_mcdt.py, cpu_tests.py lint, algorithms_table.py.
• cargo fmt --check, cargo clippy --all-targets -- -D warnings.
• cargo test with Wycheproof, and the AES-GCM tests with VG_CPU_FEATURES=none. out_of_place and backends_agree already cover slices with and without a tail, and shorter than 16 bytes.

🤖 Generated with Claude Code

https://claude.ai/code/session_01FoYWDDEDFq1DFev5X7n2aq

---

Generated by Claude Code