[alex]

From the rustls provider analysis in #991. That provider wants to seal TLS records with ChaCha20Poly1305::encrypt (gather, two pieces: payload and content type). It still copies and calls encrypt_in_place, because encrypt measured 3–7% slower than that.

Why it was slower

vg_chacha20_poly1305_seal_gather copied its slices 16 bytes at a time with SSE2's movdqu. Rust's memcpy, which copy + encrypt_in_place uses, copies a cache line at a time.

Change

Each instance now copies as wide as the CPUs of the seal it calls allow (SealGather.Width, taken from the variant's vg_poly1305_blocks):

• _avx512: 64 bytes at a time (vmovdqu32 zmm0).
• _avx2: 32 bytes at a time (vmovdqu ymm0).
• In both: then 16 bytes at a time with AVX's vmovdqu xmm0 (not SSE2's, which would pay for the dirty upper half), vzeroupper, and the last bytes one at a time.
• Baseline instance: generated code unchanged.

No new instructions, no TCB or spec change, no Rust change.

Proof

• Gather/Copy.lean now has one loop lemma for any width (chunks_ok), starting where the previous loop stopped, plus a step lemma per body (wideStep_ok, vexStep_ok).
• Loop, LoopCT, Fn, CT and Verified take the width as a parameter.
• Constant time is still checked by taint_decide, once per width.

Measurements

Sapphire Rapids–class Xeon (this repo's development VM), two pieces (n − 1 and 1 bytes), minimum of 41 interleaved samples. Ratio is encrypt time over copy + encrypt_in_place time.

bytes	AVX-512 before	AVX-512 after	AVX2 before	AVX2 after
16	1.08	1.06	1.04	1.06
256	1.05	1.03	1.04	1.02
1024	1.05	1.02	1.04	1.02
4096	1.06	1.02	1.05	1.01
16384	1.09	1.02	1.05	1.02

The 16-byte AVX2 row is noise; the copy isn't the cost there. The remaining ~2% (more at 16 bytes) is the wrapper itself: its frame, the second call, and a separate copy pass. A follow-up will remove that by XORing the keystream from the pieces straight into the output for short messages, so encrypt beats copy + encrypt_in_place rather than trailing it.

Recent CI benchmark runners for x86-64 have been AMD EPYC 7763 (no AVX-512), so the _avx512 instance can't be compared there.

Checks

• Full lake build and Emit.lean, done on the revision the CI cache was built from: x86-64 TCB: model movq r64, xmm #1333 only adds a TCB instruction that no code uses, and generates nothing.
• check_lean_imports, check_lean_speed, check_variants, check_mcdt, check_arch_gates.
• ChaCha20-Poly1305 unit and Wycheproof tests with VG_CPU_FEATURES unset, AVX2-only and none.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Ma2fA9rUTPXEEQjYyCMCRw

---

Generated by Claude Code