Implement AES-CMAC on x86

[alex]

Implements AES-CMAC on 32-bit x86, following the x86-64 (#463), AArch64 (#469) and ARMv7 (#477) implementations, all merged. Like those, this is an implementation only: it changes no Spec/ or TCB/ files.

Lean

• Impl/CmacAes/X86.lean: vg_cmac_aes_subkeys, vg_cmac_aes_update and vg_cmac_aes_finalize for 32-bit x86, with every argument on the stack (cdecl).
  • As on the other targets, each block is encrypted by calling the verified vg_aes_ctr32 on a zero block, with the block as the counter.
  • Each call is in a frame that pushes the six arguments of vg_aes_ctr32 and pops them into eax. With the return address, that is 28 bytes of stack (stack := 28).
  • The caller's ebx, esi, edi and ebp are saved in the scratch buffer ([2064, 2080)). After each call, the code reloads its arguments from the stack, which nothing writes.
  • The subkeys double L as four byte-reversed words (bswap, then add r, r for the shift), with the reduction masked (0 − msb & 0x87).
  • x86 has a single vg_aes_ctr32, so the calls are direct, with no generic file.
• Proofs (Proof/CmacAes/X86/):
  • They are written in weakest-precondition style with the x86 helpers of Proof/MdStream/X86/Common.lean. Words.lean adds a 4-word XOR (xor4_ok) and a 4-word zeroing (zero4_ok). Save.lean covers saving and restoring the registers and reading the stack arguments.
  • Call.lean proves the framed call (WP.callWith) and its constant time (RelCT.callWith, ctr_rel).
  • Correctness is proven against per-target contracts (Contract.lean), which sig_implies connects to the shared contracts of Spec/Cmac/Contract.lean with stack := 28.
  • Constant time uses the taint analysis between the calls (from esp and the stack arguments, through Framework/X86/ArgTaint.lean) and ctr_rel for each call.
  • The proofs reuse the target-independent lemmas of Proof/Cmac/ (Mem32, Block32, Dbl32, Frame, Block).
• Artifacts/CmacAes/X86.lean registers the three functions (spSafe by lit_decide).

Rust

• cmac::aes::AesCmac now also builds on x86, scalar only: the Backend::select case and its unit test cover arm and x86.
• The tests and benchmark are gated the same way.
• The README table was regenerated: x86 is now ✅.

Testing

• Before writing the proofs, the x86 code was run on the Lean model of the ISA. It reproduced RFC 4493's subkeys and MACs.
• Locally, cargo test --target i686-unknown-linux-gnu passed: the CMAC unit tests, Wycheproof aes_cmac_test.json, all CAVP CMACGen/CMACVer vectors, and the full suite. The full suite also passed on the host.
• After merging the current main (with Implement AES-CMAC on ARMv7 #477), these pass again:
  • the full lake build and lake env lean --run Emit.lean --check
  • the ci/check_*.py scripts
  • cargo fmt --check
  • cargo clippy -D warnings for i686
  • the i686 CMAC tests
• I couldn't run the bench crate's clippy for i686 locally, because this machine has no 32-bit OpenSSL. CI's Benchmarks jobs lint it.

🤖 Generated with Claude Code

https://claude.ai/code/session_01WkLN6tAYk76HACiEWLbAMD

[alex]

The Benchmarks jobs (Compare with base) were cancelled at their 15-minute timeout. 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, which takes longer than 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 (and this PR is on main after #469 and #477), I'll merge main in and the 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

[alex]

merge conflicts

[alex]

The merge conflicts are resolved in 0d3bda3, which merges main (with #477) into this branch. The conflicting files were the four shared CMAC files that #477 squash-merged:

• src/cmac/aes.rs
• the CAVP and Wycheproof tests
• the benchmark

main's copies were identical to the ARMv7 branch this one was built on, so I kept this branch's versions, which add x86. The diff against main is still the same 24 files.

After the merge, these all pass locally:

• the full lake build and Emit.lean --check
• the ci/check_*.py scripts
• cargo fmt
• clippy and the CMAC tests on i686

The branch also merges cleanly with the current main (9270f5b).

---

Generated by Claude Code