[alex]

On every call, AesEcb::encrypt and decrypt zero-initialized a 2 KB working space and then wiped it. The hardware AES block functions mostly never touch it. One block, which is QUIC header protection's shape (#3154), was about 5× slower than aws-lc-rs: 41 ns against 7 ns on Neoverse N2.

This PR proves which implementations write none of scratch and registers that with the existing written mechanism. AesEcb then wipes only the bytes the chosen function may write. There is no Spec or TCB change.

Implementation	written	Proof
AArch64 vg_aes_{en,de}crypt_blocks_aes	0	The loop invariant already framed memory to the data (blocks_frame, blocks_scratch, Proof/Aes/AArch64/Aese/Blocks.lean).
x86-64 vg_aes_encrypt_blocks_aesni and _vaes	0	The loops carry the frame in their state predicate (KPf, with Stable.frame and BlkOk.frame/BlkOk16.frame), so the shared loop invariant is unchanged.
x86-64 vg_aes_decrypt_blocks_aesni and _vaes	not registered (full wipe)	They store the AESIMC round keys in scratch.
x86 vg_aes_{en,de}crypt_blocks_aesni	not registered (full wipe)	Encryption saves esi/edi there, and decryption stores 240 bytes of round keys there.
Bitsliced implementations	not registered (full wipe)

On the Rust side, in src/aes_ecb.rs:

• The working space is a MaybeUninit. The contracts hold for any contents of scratch.
• The backend match picks each function's *_SCRATCH_WRITTEN, or 2048 bytes.
• On x86, the shared AesNi arm uses a cfg'd constant that stays at 2048.
• AesEcb is the only Rust caller that passes this working space.

Speed

Runs 39875319491 (aarch64) and 39875323075 (x86-64), against main at acdcc1f, modules aes_ecb:

Benchmark	N2	EPYC 7763 (default: VAES)	EPYC 9V45 (aes,ssse3: AES-NI)
quic-hp-aes-128/16	42 → 9 ns (−80%)	46 → 12 ns (−75%)	43 → 5 ns (−89%)
quic-hp-aes-256/16	44 → 9 ns (−79%)	50 → 12 ns (−76%)	47 → 6 ns (−88%)
aes-ecb-encrypt-128/64	−26%	−32%	−46%
aes-ecb-decrypt-128/64	−26%	−7%	+3.6%

On N2 every AES-ECB row is faster, by 23–26% at 64 B and about 11% at 1 KiB. The none configuration (bitsliced, still fully wiped) moves within ±1%.

Four x86-64 decrypt rows came out slower:

• decrypt-192/16384: 2.9% on the 7763.
• decrypt-128/64: 3.6% on the 9V45.
• decrypt-256/64: 3.0% on the 9V45.
• decrypt-256/16384: 3.2% on the 9V45.

The x86-64 decrypt functions' assembly is unchanged, and their Rust path only drops the 2 KB zero-initialization; it wipes as before. Other decrypt rows in the same two jobs are 1–7% faster, and the signs are mixed between neighbouring sizes and key lengths. I read these four as noise or code placement, not this change, and haven't rerun them.

Checks

These all pass:

• Full lake build and Emit.lean --check, and EmitOne --check for Aes.AArch64 and Aes.X86_64 after rebasing onto main.
• check_lean_public_imports on the changed modules.
• check_lean_imports, check_lean_modules, check_registrations, check_lean_speed, check_vectors, check_arch_gates, check_variants and check_mcdt.
• cargo fmt and clippy on x86-64, x86 and aarch64.
• The aes_ecb tests: on x86-64 with the default features, none and aes,ssse3, and on aarch64 under qemu (-cpu neoverse-n2) with the default features and none.

---

Generated by Claude Code