[alex]

AesGcm::new zeroed the whole 1 KiB key context, and drop wiped all of it. But the AES-NI+AVX and VAES-256 backends' prepare16 write only the first 512 bytes. This is the same fix as #3167 for AES-ECB's scratch, applied to GCM key setup.

Proofs and registration

• Proofs:
  • Proof/Gcm/X86_64/PrepareCT.lean adds Prepare16.written16. It turns a prepare16 implementation's frame (memory outside [ctx + 256, ctx + 512) unchanged) into Sig.writtenWithin … [("ctx", 512)].
  • Both implementations prove that frame: PrepareAvx/Ok.lean (its invariant's frame narrowed from 768 to 256 bytes past the key context) and Prepare16.lean.
• Registration: Artifacts/Gcm/X86_64.lean gives both prepare16 artifacts written := [("ctx", 512)] and writtenOk. The emitter exports VG_AES_GCM_PREPARE16_{PCLMUL_AVX,VPCLMUL}_CTX_WRITTEN = 512.
• No TCB/ or Spec/ changes.

Rust (src/aes_gcm.rs)

• The key context is a MaybeUninit<KeyCtx>. new clears only the 256 bytes vg_aes_gcm_init writes (key reads them), and prepare writes its proven bytes after them. Nothing reads the rest.
• Fns/Prepared carry written, which drop wipes with zeroize_raw:
  • the _CTX_WRITTEN constant for the two prepare16 backends;
  • the whole context for AVX-512, whose prepare writes all 48 powers;
  • 256 bytes for backends without prepared instances;
  • the whole KeyCtx on other architectures, as before.
• Tests:
  • with_backend wipes the old backend's powers before switching, since drop wipes only up to the new backend's written.
  • eager_powers compares only the written words.

Benchmarks

The Benchmarks gate was x86_64 aes_gcm, default and forced AES-NI+AVX (aes,avx,pclmulqdq,ssse3), with base a793a45:

Run	CPU	config	gcm-new 128 / 256	tls-connection/1 128 / 256
40015099784	Zen 3 (EPYC 7763)	default	−7.7% / —	−9.2% / —
	Zen 4 (EPYC 9V74)	AVX	−8.7% / —	−10.3% / —
40018473101	Zen 3	default	−7.7% / −7.1%	−9.2% / −8.2%
	Zen 3	AVX	−7.3% / −7.1%	−7.3% / −6.4%
40022186876	Zen 3	default	−7.7% / −8.4%	−9.1% / −8.4%
	Zen 4	AVX	−8.3% / −8.2%	−10.1% / −6.9%

None of the three runs drew a Zen 5 runner. Zen 5 takes the AVX-512 backend by default. There the change only removes new's zero-fill of the 768 bytes after the key context, which prepare overwrites, and drop still wipes the whole context. So Zen 5 does strictly less work in new and the same in drop.

Other rows more than 0.7% slower: AES-GCM-SIV, stream-bytes/64, the two-piece reused-key and tls-seal rows on one Zen 3 AVX job, and tls-open/63. The code they run is unchanged. Comparing --emit asm of the library (one codegen unit) at base and at this branch, only AesGcm::new and <AesGcm as Drop>::drop differ. AesGcm::encrypt, encrypt_in_place, open_with, the streaming types and all of AesGcmSiv are identical. These rows also flip between runs: SIV decrypt/64 was 9.2% faster on Zen 3 in the first run and 2.9% slower in the third.

AArch64 (aes_gcm, default; 40015103240): gcm-new −0.6%, tls-connection/1 −0.5%. tls-open at 111–255 is 1.1–1.3% slower. AArch64's open path is unchanged (self.ctx.as_ptr() in place of &self.ctx, same type and layout), and its KeyCtx is the 256 bytes new already cleared.

---

Generated by Claude Code