[alex]

Trust change: new specs only. Three new files:

• lean/VerifiedGarbage/Spec/Gcm/OutOfPlace.lean
• lean/VerifiedGarbage/Spec/ChaCha20/OutOfPlace.lean
• lean/VerifiedGarbage/Spec/ChaCha20Poly1305/OutOfPlace.lean

No TCB change, no implementation, no generated code. Existing contracts are unchanged.

This is the first step for #990. The implementations follow in stacked PRs.

Why

A TLS record layer gets the plaintext in buffers it doesn't own. It must write ciphertext ‖ tag into a separate output buffer. Today AesGcm and ChaCha20Poly1305 only encrypt in place, so the rustls provider (#991) copies each record into out and then encrypts it there. The copy is about 9% of an AES-GCM record's cost.

What rustls's RecordEncrypter::encrypt hands the provider (at the revision #991 pins):

Case	Plaintext	Output
TLS 1.3	OutboundPlain::Single(chunk) or ::Multiple { chunks, .. }, then a one-byte inner content type that is encrypted too	out = ciphertext ‖ tag
TLS 1.2 AES-GCM	the chunks	out = 8-byte explicit nonce ‖ ciphertext ‖ tag; the explicit nonce is outside the AEAD
TLS 1.2 ChaCha20-Poly1305	the chunks	out = ciphertext ‖ tag

rustls's aws-lc-rs provider uses aws-lc-rs 1.18's seal_out_of_place_scatter(nonce, aad, in, out, extra_in, extra_out_and_tag), with the content-type byte as extra_in, when the plaintext is a single chunk. For Multiple, it still gathers into out and seals in place, because seal_out_of_place_scatter needs a contiguous input.

API

The functions are iovec-style, as suggested in #990: a gather input and one contiguous output. The plaintext is a list of slices, Param.slices (*const [usize; 2] plus a count), as vg_aes_siv_encrypt's associated data already is. The ciphertext goes to one dst slice.

That covers all three rows above in one call, including Multiple, which aws-lc-rs doesn't:

• TLS 1.3: [chunk…, &[typ]].
• TLS 1.2: [chunk…], with dst starting after the explicit nonce.

No TCB change is needed. Sig.contract already makes a mut buffer disjoint from every other buffer, including the listed slices and their descriptors. So the output never overlaps the input, and in-place callers keep using the existing functions. Exact aliasing (dst == src) would need a new Param kind in TCB/Sig.lean, and nothing needs it.

AES-GCM (Spec/Gcm/OutOfPlace.lean)

• vg_aes_gcm_seal_gather(ctx, rounds, nonce, nonce_len, aad, aad_len, src: *const [usize; 2], src_count, dst: *mut u8, len, tag)
  • Pre: rounds ∈ {10, 12, 14}, and the listed slices total len bytes (gatheredLen).
  • Post: encryptWith … (gathered src) aad = (dst, tag). This is sealPost with the plaintext gathered.
• vg_aes_gcm_stream_encrypt_to(…, src, len, dst, dst_len)
  • streamEncryptPost with the plaintext read from src.
  • Pre: dst_len = len.
  • This is the streaming form Out-of-place AEAD encryption for AES-GCM and ChaCha20-Poly1305 (for TLS record layers) #990 asks for (AesGcmEncryptor::update_into). The planned seal_gather calls it once per slice.
• vg_aes_gcm_encrypt_blocks_to(…, src, n, dst, dst_n, scratch)
  • encryptBlocksContract's postcondition with the plaintext blocks read from src.
  • Pre: dst_n = n.
  • This is the whole-block primitive the interleaved loops will implement out of place.
• _precomputed forms of all three, for a key context of vg_aes_gcm_init_precomputed. They work exactly as the existing _precomputed functions do (PowersRepr added to the precondition, same postcondition).

ChaCha20 (Spec/ChaCha20/OutOfPlace.lean)

• vg_chacha20_xor_to(state, src, len, dst, dst_len, buf): xorContract with the data read from src.
• vg_chacha20_apply_to(state, src, len, dst, dst_len) -> u32: applyContract with the data read from src. It may leak leftAt, as apply does.

ChaCha20-Poly1305 (Spec/ChaCha20Poly1305/OutOfPlace.lean)

• vg_chacha20_poly1305_seal_gather(key, nonce, aad, aad_len, src: *const [usize; 2], src_count, dst, len, tag)
  • Post: encrypt key nonce aad (gathered src) = (dst, tag).
  • Pre: the slices total len bytes, and len ≤ P_MAX (2³² − 1 blocks of 64 bytes).
  • Unlike sealContract, whose counter wraps, this needs the P_MAX bound so it can be built on apply_to, which refuses to pass the end of the keystream. The Rust wrapper already rejects longer texts (check_len).

Constant time and lengths

Only the pointers, lengths, src_count and where the slices are (their descriptors) are public. Sig.contract already makes descriptor contents public for Param.slices. Each _to output has its own length argument because every Param.slice carries one; the preconditions require it to equal the input's, and the # Safety docs say so.

Planned Rust API (in the implementation PRs)

impl AesGcm {
    /// GCM-AE of the concatenation of `plaintext` into `out` (their total length), returning the tag.
    pub fn encrypt(&self, nonce: &[u8], aad: &[u8], plaintext: &[&[u8]], out: &mut [u8]) -> Result<[u8; 16], Error>;
}
impl AesGcmEncryptor<'_> {
    pub fn update_into(&mut self, input: &[u8], output: &mut [u8]) -> Result<(), Error>;
}
impl ChaCha20Poly1305 {
    pub fn encrypt(&self, nonce: &[u8; 12], aad: &[u8], plaintext: &[&[u8]], out: &mut [u8]) -> Result<[u8; 16], Error>;
}

rustls's TLS 1.3 encrypter then becomes key.encrypt(&nonce, &aad, &[plain, &[typ]], &mut out[..n]), with the tag written after it.

Decryption stays in place, which is what rustls does.

Checks

• lake build +VerifiedGarbage.Spec.Gcm.OutOfPlace +VerifiedGarbage.Spec.ChaCha20.OutOfPlace +VerifiedGarbage.Spec.ChaCha20Poly1305.OutOfPlace passes.
• ci/check_lean_imports.py, ci/check_lean_speed.py, ci/check_vectors.py and ci/check_arch_gates.py pass.

🤖 Generated with Claude Code

https://claude.ai/code/session_01MmkzVkkRyGFLYBPdnXPeVb

---

Generated by Claude Code