[alex]

From the rustls provider analysis in #991. Below 1 KiB, that provider's ChaCha20-Poly1305 was 0.58–0.84× as fast as aws-lc-rs on a Cascade Lake–class Xeon. At 16 bytes it took 322 ns against aws-lc-rs's 197 ns. Above about 4 KiB it was faster than aws-lc-rs. Below 1 KiB the fixed cost of each call dominates. Much of that cost is stores, about 270 for a 16-byte seal, and Cascade Lake can do only one store per cycle. This PR cuts those stores and some calls. It changes neither the vector ChaCha20 nor Poly1305.

Change

All in vg_chacha20_poly1305_seal/_open (Impl/ChaCha20Poly1305/X86_64.lean), for every variant:

• ChaCha20 state: the two copies of the initial state in the context are written 8 bytes at a time: the constants as 64-bit immediates, the key as quadwords, and the counter and first nonce word as one shifted load (initStateQ). Before, they were written 4 bytes at a time. That is 8 stores instead of 16 per copy.
• Keystream buffer: zeroed 16 bytes at a time with pxor/movdqu instead of 8 at a time (zeroKs).
• Short-message XOR: below the vector threshold, the XOR goes 16 bytes at a time instead of 8 before the byte loop (xorBufX).
• Poly1305 calls:
  • The Poly1305 block call is skipped when there are no whole blocks (wholeBlocks).
  • The message's partial last block and the lengths block are absorbed in one call instead of two (macPadLengths).
• Scratch wipe: the stack scratch is wiped 16 bytes at a time (withStackArgScratchWipedX, new beside withStackArgScratchWiped in Impl/StackScratch/X86_64.lean).
  • Its proof, Verified.stackArgScratchWipedBy, is generic over the wiping code (Wiper). The existing Verified.stackArgScratchWiped is now a corollary with the same statement, so its other callers are unchanged.
  • Only ChaCha20-Poly1305 uses the 16-byte wipe for now.

No TCB or spec change, no new instructions (pxor, movdqu, movImm64 and shl are all in the baseline model), and no Rust change. Only src/asm/x86_64/chacha20poly1305.rs is regenerated.

Proof

• CT.lean is reworked for the new code:
  • State setup: stQ_ok, initStateQ_ok, and the qOf_* lemmas relating each quadword to the spec's words.
  • The 16-byte zero loop.
  • MAC padding: wholeBlocks_ok, macTail_ok, macRest_ok, macPad_ok, macPadLengths_ok.
  • seal/open correctness on top of these.
• New XorBufX.lean: the 16-byte XOR loop and its frame.
• StackArgScratchWipe.lean: Wiper, the generalized wipe proof, and wipeAtX_run/wipeAtX_spSafe.
• Constant time is still checked by taint_decide.
• CT.lean uses one fewer decide := true simp, so ci/lean_speed_allowed.py goes from 19 to 18.

Measurements

These were taken on a Sapphire Rapids–class Xeon, this repo's development VM, with ci/bench_compare.py --rounds 5. Each figure is the fastest of 5 interleaved runs, against #1345. The Cascade Lake machine where the gap was measured isn't available to me.

chacha20poly1305 (in-place seal) / -decrypt / -encrypt-out-of-place (two pieces):

bytes	AVX-512	AVX2	baseline
16	−3.1% / −1.7% / −2.2%	−1.4% / −1.2% / −0.4%	−2.7% / −2.6% / −2.6%
64	−1.9% / −2.1% / −3.1%	−2.6% / −1.9% / −1.7%	−3.0% / −2.6% / −2.8%
256	−3.6% / −4.4% / −1.9%	−0.3% / −1.5% / −0.9%	−1.0% / −0.8% / −1.8%
512	−6.0% / −9.1% / −5.4%	−1.2% / −1.5% / −2.5%	−0.6% / −0.5% / −1.1%
768	−7.1% / −11.1% / −6.4%	−0.8% / −0.2% / −1.4%	−0.8% / −0.5% / −1.0%
1024	−1.0% / −2.6% / −0.3%	−1.4% / +0.3% / −1.9%	+0.2% / −0.6% / −1.0%
4096	+0.3% / −2.1% / −1.6%	−1.1% / +0.6% / −0.9%	−0.5% / +0.4% / −1.1%
16384	−1.2% / −0.1% / +1.2%	0.0% / +0.6% / −0.2%	−1.0% / +0.1% / −0.2%

AVX-512 gains most between 256 and 768 bytes, where the message ends in a scalar tail and a partial block. That is exactly where one Poly1305 call is now skipped and another merged. The few small slowdowns are within run-to-run noise. Recent x86-64 CI benchmark runners have been AMD EPYC 7763 (no AVX-512), so the AVX-512 rows can't be checked there.

This is a step, not the whole gap. On this machine we already beat aws-lc-rs at these sizes (64 B: 202 vs 259 ns), so the Cascade Lake gap is specific to that CPU. One possible cause is its cost for 512-bit registers; aws-lc-rs's ChaCha20 doesn't use AVX-512. That needs a measurement there.

Checks

• Full lake build and Emit.lean, done on the revision the CI cache was built from. The Lean sources and src/asm/x86_64/chacha20poly1305.rs are byte-identical on this branch.
• check_lean_imports, check_lean_speed, check_variants, check_mcdt, check_arch_gates, check_vectors.
• ChaCha20-Poly1305 unit and Wycheproof tests with VG_CPU_FEATURES unset (AVX-512), AVX2-only and none.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Ma2fA9rUTPXEEQjYyCMCRw

---

Generated by Claude Code