[alex]

Stacked on #1850, which adds the spec and contract of vg_aes_gcm_seal_split. Merge that first.

What

AesGcm::encrypt (out of place) runs vg_aes_gcm_seal_gather. On main the gather takes one of two paths:

• Short path: for a text shorter than its variant's copyBelow, it copies every slice to dst and calls seal there.
• Otherwise: it streams.

For a TLS record (the payload, then a 1-byte content type), copying first means the payload is read and written twice before any of it is encrypted (#1228).

This PR adds vg_aes_gcm_seal_split for every implementation. It seals a text whose first tl bytes are read from src and whose rest is already in place at dst + tl. The prefix is encrypted straight from src to dst with the instance's encrypt_blocks_to (ctr32_to), and the rest is sealed in place.

The gather's short path now also takes a text whose first slice holds all its whole blocks, at any length, and chooses between seal and seal_split, inside the verified code (copyShort, Impl/AesGcm/X86_64/SealGather.lean):

• seal_split: used when the first slice holds all the text's whole blocks and at least the variant's splitFrom bytes. The gather then copies only the slices after the first and calls seal_split with the first slice as src.
• seal: used otherwise. The gather copies everything and calls seal, as on main.

Where whole blocks follow the first slice (e.g. two halves), sealing in two places would take a second pass of the blocks loop, which costs more than the copy. So those texts keep the copy.

splitFrom (Generic/AesGcm/X86_64/AesGcm.lean), chosen from the Benchmarks results below:

variant	copyBelow	splitFrom
VAES + VPCLMULQDQ + AVX-512	768	752 (the TLS texts the gather would otherwise stream)
VAES + VPCLMULQDQ (AVX2)	16384	1024
AES-NI + PCLMULQDQ + AVX	3072	384
others (no out-of-place loop)	2³¹−1	never

Variants: every seal_gather_<s> calls both seal_<s> and seal_split_<s>, and each seal_split_<s> calls its own ctr32_<s>, encrypt_blocks_<s> and ghash_<s>. ci/check_variants.py passes with no exceptions. The Rust side is unchanged apart from the generated code.

Each instance's seal_split ends the way its seal does:

• AVX-512: Short.finish, with the short-message path (runShort) in front, as seal has.
• AES-NI+AVX: finishWith finKsA.
• Others: oneCrypt; oneTag 0.

Proofs

• All assembly comes from Lean. Spec/ and TCB/ are unchanged by this PR (the spec is Spec: AES-GCM seal of a plaintext whose prefix is read from elsewhere (vg_aes_gcm_seal_split) #1850's).
• seal_split is proven once, generic over its ending (FinOk/FinRel, Split/Fin.lean, Split/FinCT.lean) and its middle (MidOk/MidRel):
  • run: Split/Run.lean, Split/CT.lean.
  • runShort: Split/ShortRun.lean, Split/ShortCT.lean. It reuses sealShort's proof from a virtual entry state whose dst already holds src's bytes.
• The gather's entry (sealGather quick fast test short, sealGatherG_wp/sealGatherG_ct): a text below splitFrom goes to fast (copySeal, main's path) after quickTest; only longer texts reach test/short.
• The gather's short path (ShortFn.ofBoth, Gather/Verified.lean):
  • Its test: splitTest, selTest (Gather/SplitPath.lean, Gather/SplitCT.lean).
  • Both callees: Gather/SealCall, Gather/SealCallee, Gather/Split*.
  • splitFrom_le (splitFrom + 16 ≤ copyBelow) is what lets a copied TLS text stay within seal's short path.

Measurements

Below splitFrom the gather runs main's instructions. A text shorter than its variant's splitFrom takes the copy-and-seal path after one compare and one branch. That is the same instruction sequence as main's short path; only the threshold immediate differs. This covers every size up to 384 B, and 600 B with VAES or AVX-512. Only longer texts reach the slice tests (splitTest, then selTest).

These results are from the Benchmarks workflow (bench.yml, modules=aes_gcm) on this head (c625dda), against base 135a4d9:

• 14 runs, 168 x86-64 jobs.
• Runners: AMD EPYC 7763 / 9V45 / 9V74 and Intel Xeon 8573C / 8370C / 6973P-C.
• Three jobs are left out because an in-place control (encrypt/384, encrypt/1024, decrypt/1024, encrypt-reused-key/4000), which this PR does not change, moved by more than 10% in them.

The table gives mean % faster, then n. "two-pieces" is the TLS shape (payload, then a 1-byte content type) with a new key each time; "TLS" rows reuse the key.

bench	AVX-512 (default job)	VAES-AVX2	AES-NI+AVX	others (never split)
two-pieces/64	+2.6 /5	−0.6 /22	+0.2 /28	+0.4 /110
two-pieces/128	+2.4 /5	+0.0 /22	+0.0 /28	+0.3 /110
two-pieces/192	+1.3 /5	−0.4 /22	+0.0 /28	+0.1 /110
two-pieces/384	+1.7 /5	+0.4 /22	+0.6 /28	+0.2 /110
two-pieces/1024	+11.7 /5	+3.3 /22	+3.1 /28	+0.1 /110
two-pieces/16384	+3.3 /5	+0.8 /22	+1.6 /28	−0.0 /110
out-of-place/64	+2.8 /5	+0.1 /22	+0.8 /28	+0.1 /110
out-of-place/128	+1.8 /5	+0.3 /22	+0.3 /28	+0.1 /110
out-of-place/192	+2.3 /5	−0.6 /22	+0.3 /28	+0.1 /110
out-of-place/384	+0.9 /5	+1.2 /22	+1.4 /28	+0.0 /110
out-of-place/1024	+2.0 /5	+4.6 /22	+3.0 /28	+0.0 /110
out-of-place/16384	+1.6 /5	+0.3 /22	+0.2 /28	−0.0 /110
halves-reused-key/600	+0.7 /5	+0.6 /22	+0.9 /28	−0.1 /110
halves-reused-key/1350	−0.3 /5	+0.0 /22	+0.4 /28	−0.0 /110
halves-reused-key/4000	−1.3 /5	+0.2 /22	−0.6 /28	−0.0 /110
TLS (two-pieces-reused-key)/600	−1.0 /5	+0.4 /22	+2.7 /28	−0.0 /110
TLS/1350	−0.1 /5	+2.5 /22	+3.7 /28	+0.2 /110
TLS/4000	+0.2 /5	+7.6 /22	+3.2 /28	−0.1 /110
encrypt/384 (in place, unchanged)	−0.7 /5	−1.0 /22	+1.0 /28	+0.3 /110
encrypt/1024 (in place, unchanged)	+0.0 /5	−0.9 /22	+0.8 /28	−0.1 /110
encrypt/16384 (in place, unchanged)	+0.2 /5	+0.0 /22	+0.4 /28	+0.0 /110
decrypt/1024 (unchanged)	+0.3 /5	+0.1 /22	+0.3 /28	−0.1 /110

AVX-512, per sample. The default job lands on an AVX-512 runner only when it is not given an EPYC 7763, so these were sampled until there were five clean AMD runs, Zen 4 and Zen 5 both. Two of them are from the previous head (761d821), whose gather runs the same instructions below splitFrom:

run	head	CPU	out-of-place / two-pieces 64–384 B, mean (range)
38198774257	761d821	9V74 (Zen 4)	−7.2 (−8.4 … −6.0)
38203870753	761d821	9V45 (Zen 5)	+0.2 (−1.5 … +3.2)
38205550742	c625dda	9V74 (Zen 4)	+0.3 (−1.2 … +2.9)
38210318300	c625dda	9V74 (Zen 4)	−0.2 (−1.3 … +0.7)
38215722023	c625dda	9V45 (Zen 5)	+2.9 (−0.1 … +5.2)
38208122270	c625dda	Xeon 8573C	+4.9 (+1.0 … +7.2)
38209586754	c625dda	Xeon 8370C	+2.0 (+0.4 … +3.5)

The five AMD samples average −0.8%, or +1.0% on this head alone. The one −7% run is not repeated in the four other AMD runs. Two more AMD runs (38201427078, 38203153182, both 761d821) and one on this head (38208862806, +2.3) moved an in-place control by more than 10% and are left out.

AVX-512 and the TLS shape with a reused key. With a reused key, AVX-512 is unchanged at 1350 and 4000 B (−0.1, +0.2): its out-of-place path already reads unaligned slices without buffering, so there is little left to save there. The earlier +7/+9% at those sizes came from one run (38201427078) whose base was slow; it is left out above. With a new key per text (two-pieces), AVX-512 is +11.7% at 1024 B and +3.3% at 16 KiB.

AES-NI+AVX at 600 B. The text is above that variant's splitFrom (384), so it reads the first slice's length before it is copied and sealed as on main. Trimming a redundant length test from copyShort (selTest is now one lenTest) closed the earlier −3.2%: halves-reused-key/600 is +0.9 (n=28) and TLS/600 is +2.7 (n=28), so splitFrom stays 384.

🤖 Generated with Claude Code

https://claude.ai/code/session_01FoYWDDEDFq1DFev5X7n2aq

[alex]

Compare with base (x86_64, VG_CPU_FEATURES=aes,avx,avx2,ssse3,vaes) failed on 1de6e72: aes-xts-192/16384 was 102% slower and aes-xts-256/16384 96% slower (aes-ofb-*/16384 was also 19–31% slower, below the limit).

This PR doesn't cause it. Only src/asm/x86_64/gcm.rs differs from base, so the XTS and OFB code is identical on both sides. Those benchmarks ran only because the PR's head changes the benchmark crate (the halves group from #1877). #1877 changes nothing but that crate and showed the same XTS slowdowns at 16 KiB on the same configuration. There's no fix to port, since the library code is unchanged. I'm re-running the failed job once. The AES-GCM rows in the same table are what this PR is measured on.

---

Generated by Claude Code

[alex]

Compare with base (x86_64, VG_CPU_FEATURES=pclmulqdq,ssse3) failed in the Benchmarks run 38199349244 (on 761d821). The runner was disturbed while it ran; the failure is not from this PR.

• Unchanged code moved wildly. In-place encrypt/128 and encrypt/1024 were 104% and 89% slower, decrypt/192 76% slower and stream/64 57% slower. This PR does not change those functions.
• Some rows moved the other way. encrypt-reused-key/1350 was 28% faster and halves-reused-key/600 42% faster. A real regression would not do that.
• The flagged gather rows run main's code. out-of-place/128 and two-pieces/128 are among them, but with pclmulqdq,ssse3 (the unstitched variant, which never splits) the gather executes main's instructions apart from the threshold in the first compare.
• The PR's own run on this head passed. That is run 38198774257, with this configuration within ±2.5%.

I'll re-run the failed job once when the run completes.

---

Generated by Claude Code

[alex]

merge conflicts

[alex]

merge conflicts

[alex]

The restack onto main is ready locally: one squashed commit, with the two import conflicts resolved and the 20 new Lean files converted to modules. It hasn't been built, regenerated or pushed yet, because this session's permission layer refused the git command that brings the commit into the build checkout. I've asked for that to be allowed. Once it is, I'll build, regenerate, test and force-push.

(For about a minute, this branch briefly pointed at #1975's head by mistake. It's back on c625dda.)

---

Generated by Claude Code

[alex]

merge conflict

[alex]

still waiting on a merge conflict fix here

[alex]

Rebased onto main as one squashed commit (26eba23). Two proof files needed updating for main's #1859, which replaced absorbAl. Locally: the full lake build passes, the regenerated src/asm is committed, and the ci/ checks, fmt and clippy are clean. cargo test with Wycheproof passes with native features, none, AES-NI+AVX and a Cascade-Lake-like set.

---

Generated by Claude Code