Implement AES-CMAC on x86-64, with an AES-NI variant

[alex]

Implements the AES-CMAC primitives specified in #447 (VG.Spec.Cmac) on x86-64 and builds the public API on them. This PR is an implementation only: it changes no Spec/ or TCB/ files.

Lean

• Impl/CmacAes/X86_64.lean: vg_cmac_aes_subkeys, vg_cmac_aes_update and vg_cmac_aes_finalize.
  • Each encrypts a block by calling the verified vg_aes_ctr32 with that block as the counter and a zero block as the data. The callee's output is then CIPH_K(X) (ctr32_one).
  • The subkeys double L in two byte-swapped 64-bit words (Proof/CmacAes/X86_64/Dbl.lean).
  • finalize handles a full last block (XOR with K1) and a partial one (copy, pad with 0x80, XOR with K2), then makes one more call.
• Proofs (Proof/CmacAes/X86_64/) cover correctness against the shared contracts (Verified.of_correct, then sig_implies) and constant time.
  • The code around each call is checked by the taint analysis.
  • Each call is checked relationally (RelCT) from ctr32's own constant-time proof, because the callee's spills hide which saved registers stay public.
• The CMAC code is generic over the implementations of ctr32, through a new AesCtr32 interface:
  • Generic/AesCtr32/X86_64/CmacAes.lean registers the functions.
  • Variants/AesCtr32/X86_64/{Scalar,AesNi}.lean add the implementations. Proof/Aes/X86_64/Variant.lean packages each ctr32 with its proofs.
  • The emitter therefore also emits vg_cmac_aes_*_aesni (features aes, ssse3), which call vg_aes_ctr32_aesni.
• Shared, target-independent lemmas are in Proof/Cmac/ (Spec, Mem, Dbl), ready for the other architectures.

Rust

• verified_garbage::cmac::aes::AesCmac (new, update, finalize, verify, mac), gated on x86-64 for now.
  • The only unverified logic is keeping the last (possibly full) block back for finalize.
  • The backend is chosen by CPU feature with an exhaustive match (Scalar / AesNi).
• cmac::{InvalidKeyLength, InvalidMac} are shared with the later 3DES-CMAC module.

Tests and benchmark

• Wycheproof aes_cmac_test.json: 63 valid, 243 modified tags and 5 bad key sizes. Each MAC is computed three ways: all at once, in one update, and byte by byte.
• Every vector of the vendored CAVP CMACGen files (336) and CMACVer files (480: 96 pass, 384 fail), with tags truncated to Tlen.
• A unit test of streaming split at every point, run on a clone of a fresh key.
• Run with all CPU features and with VG_CPU_FEATURES=none. Line coverage of the new files is 100% across the two configurations.
• bench/benches/primitives/cmac_aes.rs measures aes-128-cmac and aes-128-cmac-verify against OpenSSL's PKey::cmac. A quick local run (AES-NI) gave about 230 MiB/s at 64 B and 560 MiB/s at 16 KiB, against OpenSSL's 13 and 335 MiB/s on the same machine.
• The README table was regenerated (ci/algorithms_table.py): AES-CMAC is now ✅ AES-NI on x86-64.

Checks run locally

• lake build (full) and lake env lean --run Emit.lean --check
• check_lean_imports, check_lean_speed, check_vectors, check_arch_gates, check_variants and check_mcdt
• cargo fmt --check and cargo clippy --all-targets -D warnings (crate and bench)
• cargo test with Wycheproof, with and without VG_CPU_FEATURES=none

The AArch64, ARMv7 and x86 implementations will follow in separate PRs.

🤖 Generated with Claude Code

https://claude.ai/code/session_01WkLN6tAYk76HACiEWLbAMD

---

Generated by Claude Code

[alex]

The failures on the previous head (rust (… armv7l …), Rust (Thumb, stable), Compare with base (arm), and through them all-green) were not from this change. Each one stopped at rustup toolchain install stable in the armv7l container: rustup's update to 1.99.0 failed with failure removing component 'cargo-armv7-unknown-linux-gnueabihf', directory does not exist: 'share/man/man1/cargo.1', before anything was built. main has since fixed this ("Use a fresh rustup home for ARM benchmark containers", in #460 and #462), and I merged main into this branch (7719a3f) to pick up that fix.

---

Generated by Claude Code