[alex]

Part of #4548. This is stacked on #4685. There are no trust changes.

No CPU has VAES without VPCLMULQDQ, or the reverse: the two arrived together, with Ice Lake and Zen 3. ci/rust_matrix.toml already called these combinations ones "which no chip has without the other".

Despite that, x86-64 AES-GCM had four variants that pair them anyway (vaes, vpclmul, vaesPclmul and aesNiVpclmul). Its streaming functions were also built for every pair of an AES implementation and a GHASH implementation.

What changes

• Variants: the four variants are deleted from Proof/Variants/AesGcm/X86_64.lean.
• Streaming functions: they are now built for the AES and GHASH pairs that the remaining variants call (Proof.AesGcm.X86_64.streamPairs), instead of the cross product of the AesCtr32 and Ghash lists.
• What's left: every x86-64 AES-GCM and AES-GCM-SIV function now has implementations for exactly these combinations:
  • VAES with VPCLMULQDQ, in 256 or 512 bits;
  • AES-NI with PCLMULQDQ, with or without AVX's loops;
  • AES-NI alone;
  • PCLMULQDQ alone;
  • the baseline.
• Tests and benchmarks: four configurations of Ice Lake's aes_gcm group in ci/rust_matrix.toml, and four profiles in bench/gcm_siv_features.py, existed only to reach the deleted instances. They are removed.

Every other dispatcher is unchanged. I compared each dispatcher with the base branch's: the only differences are the deleted arms.

Checks

• lake build passes.
• Emit.lean passes.
• Every step of the Static checks job passes, including cpu_tests.py lint and algorithms_table.py --check.
• check_lean_public_imports.py passes.
• cargo clippy and cargo test pass, including the aes_gcm tests under several VG_CPU_FEATURES settings.

---

Generated by Claude Code

[github-actions]

This pull request has conflicts with main, found after e4c4e66 landed on main: rebase it to resolve them. Before rebasing, see CLAUDE.md on checking how much Lean main changed, and on restacking a stacked pull request.

_{Posted by .github/workflows/conflicts.yml, once per push to a conflicting pull request.}