Implement AES-CMAC on AArch64, with an AES-extension variant

[alex]

Implements AES-CMAC on AArch64, following the x86-64 implementation (#463, merged). Like #463, this is an implementation only: it changes no Spec/ or TCB/ files.

Lean

• Impl/CmacAes/AArch64.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 on a zero block, with the block as the counter, as on x86-64.
  • The calls (bl) keep the return address in x30. Each function saves x30 and the callee-saved registers it uses in the scratch buffer ([2064, 2120)), so no stack is used (stack := 0).
  • The model has no flags or register-offset addressing. The branches are therefore cbz/cbnz (on n, on last_len − 16 and on last_len), and the last bytes are copied through advancing pointers.
• The code is generic over the AArch64 implementations of ctr32, through the AesCtr32 interface:
  • Impl/Aes/AArch64/Callee.lean and Proof/Aes/AArch64/Variant.lean define the interface.
  • Variants/AesCtr32/AArch64/{Scalar,Aese}.lean add the implementations.
  • Generic/AesCtr32/AArch64/CmacAes.lean registers the functions, so the emitter also emits vg_cmac_aes_*_aes (feature aes), which call vg_aes_ctr32_aes.
• Proofs (Proof/CmacAes/AArch64/):
  • Correctness is proven against per-target contracts, which sig_implies connects to the shared contracts of Spec/Cmac/Contract.lean.
  • Constant time uses the taint analysis between the calls, and RelCT.call with ctr32's own constant-time proof for each call.
  • v8–v15 are preserved because no instruction writes them, the callees' included (keepsV, a field of each variant).
• The block lemmas that do not depend on the target move to Proof/Cmac/Frame.lean and Proof/Cmac/Block.lean. The x86-64 proofs keep their own copies, so this PR doesn't touch them.

Rust

• cmac::aes::AesCmac now also builds on AArch64, with an exhaustive backend match (Scalar / ArmCrypto). Its tests and benchmark are gated the same way.
• The README table was regenerated: AArch64 is now ✅ (AES).

Testing

• Before writing the proofs, the AArch64 code was run on the Lean model of the ISA. With both ctr32 callees it reproduced RFC 4493's subkeys and its MACs for 0, 16, 40 and 64 bytes.
• Locally, cargo test passed for aarch64-unknown-linux-gnu under qemu (Wycheproof aes_cmac_test.json, all CAVP CMACGen and CMACVer vectors, and the unit tests), both with the AES extension and with VG_CPU_FEATURES=none.
• Also passing locally:
  • the full lake build and lake env lean --run Emit.lean --check
  • the ci/check_*.py scripts
  • cargo fmt --check and cargo clippy (both host and aarch64)

🤖 Generated with Claude Code

https://claude.ai/code/session_01WkLN6tAYk76HACiEWLbAMD

[alex]

The Benchmarks jobs (Compare with base) on this PR were cancelled at their 15-minute timeout, so they show no result. The cause is not this PR's code.

This PR's only benchmark change is the arch cfg of bench/benches/primitives/cmac_aes.rs, which check_arch_gates.py requires. ci/bench_arches.py treats any change under bench/ as shared, so it ran every benchmark in all nine configurations. That takes about 14–15 minutes per job, so the slower runners hit the timeout.

#488 fixes this: a changed benchmark now narrows the run to the modules its USES lists. Porting it into this PR wouldn't help, because a change to bench_arches.py itself runs everything. Once #488 is on main, I'll merge main in here and the Benchmarks run will cover only AES-CMAC and AES-GCM. The Benchmarks check isn't part of all-green; the other checks are green.

---

Generated by Claude Code