[alex]

Part of #990. This implements the out-of-place contracts of #1209 on x86-64, vg_aes_gcm_seal_gather included, and adds a non-in-place AEAD encrypt on top that is one asm call.

No TCB/ or Spec/ changes. This is an implementation PR: Impl/ + Proof/ + registration (in the generic AES-GCM file) + generated code + Rust.

Rust API

One new method, one constant and two new error variants:

impl AesGcm {
    pub const MAX_PIECES: usize = 64;
    /// Encrypts the plaintext made of `plaintext`'s pieces, in order, into `out`
    /// (exactly as long as they are in all) and returns the tag.
    pub fn encrypt(&self, nonce: &[u8], aad: &[u8], plaintext: &[&[u8]], out: &mut [u8]) -> Result<[u8; 16], Error>;
}
// Error::InvalidOutputLength: `out` is not as long as the pieces in all.
// Error::TooManyPieces: more than MAX_PIECES pieces.

• A plaintext in one buffer is one piece: &[buf].
• On x86-64 it is one call of the verified vg_aes_gcm_seal_gather (or _precomputed), with the pieces' descriptors in a stack array. The array is why the number of pieces is capped.
• On other targets it copies the pieces into out and encrypts it there.

Verified functions (x86-64, every AES-GCM variant)

• vg_aes_gcm_encrypt_blocks_to (and _precomputed): Spec.Gcm.encryptBlocksToContract.
  • The _vaes_vpclmul_avx512 variants get new out-of-place interleaved loops (StitchZTo).
  • The other variants copy the blocks to dst and call vg_aes_gcm_encrypt_blocks.
• vg_aes_gcm_stream_encrypt_to (and _precomputed): Spec.Gcm.streamEncryptToContract.
  • It takes the whole blocks with one call of encrypt_blocks_to when the text so far ends a block, and is not empty or follows additional data of whole blocks.
  • It copies the rest to dst and encrypts it there with vg_aes_gcm_stream_encrypt.
  • It runs in a 2232-byte frame, 4856 bytes of stack in all.
• vg_aes_gcm_seal_gather (and _precomputed): Spec.Gcm.sealGatherContract.
  • Impl/AesGcm/X86_64/SealGather.lean runs the streaming functions on a state of its own: stream_init, then stream_aad.
  • If there is any text, it then pads the additional data with zeros to a whole block with a second stream_aad. GHASH pads it the same way, so the message is the same (Proof.Gcm.streamRepr_padded). The padding lets stream_encrypt_to take the whole blocks in one pass even after a 5- or 13-byte TLS header.
  • Then one stream_encrypt_to per slice, from where the slice is to the output, then stream_finish.
  • The proofs (Proof/AesGcm/X86_64/Gather/) work from the callees' shared contracts (Gather/Callee.lean): correctness through a loop invariant over the slices, and constant time with the relational framework. The descriptors are public, as the contract says.
  • It runs in a 240-byte frame for its working space (Verified.stackArgScratchL), 5128 bytes of stack in all. Proof/AesGcm/ScratchGather.lean shows the conditions read only the buffers, the descriptors and the slices.

Benchmarks

Group aes-128-gcm-encrypt-out-of-place (one piece), against OpenSSL's Crypter and aws-lc-rs's seal_out_of_place_scatter. Local AVX-512 run, key setup included in each iteration:

bytes	ours	aws-lc-rs	OpenSSL
64	177 ns	221 ns	1.05 µs
384	282 ns	249 ns	1.07 µs
1024	273 ns	304 ns	1.13 µs
16384	1.37 µs	1.37 µs	2.30 µs

The single call is 4–13% faster than this PR's previous stream-based encrypt.

Checks

• The full Lean build and Emit.lean --check pass, with the emitter's audits.
• The ci/ scripts pass, including check_variants and check_mcdt.
• cargo fmt and clippy -D warnings pass on x86-64 (with and without alloc), AArch64, x86 and ARMv7.
• The AES-GCM unit tests pass on every backend configuration this CPU can run.
  • Covered: pieces split on and off block boundaries, empty pieces, exactly MAX_PIECES pieces, too many pieces, the precomputed path.
• The Wycheproof vectors pass out of place, with the plaintext whole and in two pieces.

🤖 Generated with Claude Code

https://claude.ai/code/session_01MmkzVkkRyGFLYBPdnXPeVb