[alex]

Follow-up to #1404 and part of #1228. This is the path AesGcm::encrypt takes for long texts with a long-lived key (see the rustls analysis in #991).

What changes

vg_aes_gcm_encrypt_blocks_to_prepared_vaes_vpclmul_avx512 used to run the 512-bit out-of-place loop over 16 ⌊n/16⌋ blocks only. It then copied the r = n mod 16 blocks left into the output and called vg_aes_gcm_encrypt_blocks on them there.

Now one loop, StitchZHTo.encR, takes every block from 16 on. After the groups of 16, it encrypts the r remaining blocks from the plaintext into the output in the same pass. It reuses #1404's remainder code, reading at rdx + r8 (StitchZH.remWith [add r8, rdx] .r8). Nothing is left for the copy or the call.

Speed

Measured with AesGcm::encrypt on a reused key (so the prepared path runs), on a VAES/AVX-512 machine. Each value is the best of 7 runs; three alternating rounds against #1404's commit all agreed.

bytes	one slice	two pieces (a TLS 1.3 record)
600	neutral (the short path copies and calls seal, which #1404 already sped up)	187 → 153 ns (−18%)
1350	265 → 235 ns (−11%)	230 → 199 ns (−13%)
4000	436 → 389 ns (−11%)	434 → 395 ns (−9%)
16384 (no blocks left)	neutral	neutral

#1406, which is in the merge queue, adds these reused-key groups (aes-128-gcm-encrypt-two-pieces-reused-key) to the Benchmarks check.

Proofs

No changes to TCB/ or Spec/.

• Cached/RemTo.lean: remTo_ok is the out-of-place remainder, followed by tailRTo_ok and encTailRGTo_ok. It reuses x86-64 AES-GCM: prepared AVX-512 encryption hashes the last blocks in its loop #1404's loop lemma (remLoop_ok, whose REnv keeps the source and destination separate) and its keystream and hashing lemmas, applied to the in-place view dst s₀. The plaintext stays apart from everything written, by SPreTo.s_o/s_p/s_c.
• StitchZ/OkP.lean: encRTo_ok and stitchToR_ok show that the new loop meets StitchToOkM for any number of blocks from 16 on. The cached 48-block out-of-place loop (loop48To_ok, bigRestTo_ok, bigPTo_ok) no longer needs a multiple of 16. loopERTo_ok lets the group loop stop with fewer than 32 blocks left.
• BlocksTo gets x86-64 AES-GCM: prepared AVX-512 encryption hashes the last blocks in its loop #1404's full mode:
  • takeAllTo makes the kept arguments those of an empty rest (src + 16n, dst + 16n, 0 blocks).
  • The proofs are in BlocksTo/Full.lean, encrypt_wp and part_rel/encrypt_ct.
  • spreTo_of and mid_of_postTo now take any block count.
  • StitchToCode and PieceTo carry the flag, which only the AVX-512 variant's prepared loop sets (StitchToName.fullR). Its taint check covers the new code.

Only vg_aes_gcm_encrypt_blocks_to_prepared_vaes_vpclmul_avx512 changes in src/asm/.

Checks

These ran locally before restacking onto main:

• lake build (full) and Emit.lean pass; the emitter's audits pass.
• All the ci/check_* scripts pass.
• cargo fmt --check and clippy -D warnings pass.
• cargo test --release passes with Wycheproof on AVX-512 hardware.

The restack brought in no conflicts.

🤖 Generated with Claude Code

https://claude.ai/code/session_01FoYWDDEDFq1DFev5X7n2aq

---

Generated by Claude Code