Implement AES-CMAC on ARMv7

[alex]

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

Lean

• Impl/CmacAes/Arm.lean: vg_cmac_aes_subkeys, vg_cmac_aes_update and vg_cmac_aes_finalize.
  • 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.
  • vg_aes_ctr32 takes n and its scratch buffer on the stack. Each call is therefore in a frame (push {rA, rB} … pop) that pushes them, so the functions use 8 bytes of stack (stack := 8).
  • The callee-saved registers and lr are saved in the scratch buffer ([2064, 2096)).
  • The subkeys double L as four byte-reversed words (rev), with the reduction masked (0 − (msb) & 0x87).
  • ARMv7 has a single vg_aes_ctr32, so the calls are direct, with no generic file.
• Proofs (Proof/CmacAes/Arm/):
  • They are written in weakest-precondition style with the ARM helpers of Proof/MdStream/Arm/Common.lean (wp_ldr, wp_str, saveList_ok, …), plus two reusable blocks in Words.lean: a 4-word XOR (xorBlk_ok) and a 4-word zeroing (zeroBlk_ok).
  • Call.lean proves the framed call (WP.frame, WP.call) and its constant time (RelCT.frame, RelCT.call).
  • Correctness is proven against per-target contracts (Contract.lean), which sig_implies connects to the shared contracts of Spec/Cmac/Contract.lean with stack := 8.
  • Constant time uses the taint analysis between the calls (the prologues from the public stack arguments) and ctr_rel for each call.
• New target-independent lemmas for 32-bit words: Proof/Cmac/Mem32.lean, Block32.lean and Dbl32.lean (doubling over four words, and the byte-reversed loads and stores).
• Proof/Framework/Arm/ArgTaint.lean (new, untrusted): argTaint, agree_argTaint, rel_agree and rel_wp, the ARM counterpart of Framework/X86/ArgTaint.lean. The same definitions are currently private copies in the BLAKE2 and HMAC proofs, which this PR doesn't touch.
• Artifacts/CmacAes/Arm.lean registers the three functions.

Rust

• cmac::aes::AesCmac now also builds on ARMv7, scalar only: Backend::select has an ARM case that always returns Scalar, with a unit test.
• The tests and benchmark are gated the same way.
• The README table was regenerated: ARMv7 is now ✅.

Testing

• Before writing the proofs, the ARMv7 code was run on the Lean model of the ISA. It reproduced RFC 4493's subkeys and MACs.
• Locally, cargo test passed for armv7-unknown-linux-gnueabihf and thumbv7neon-unknown-linux-gnueabihf under qemu: the CMAC unit tests, Wycheproof aes_cmac_test.json, and all CAVP CMACGen/CMACVer vectors. The full suite (198 tests) also passed for armv7, and on the host.
• 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 -D warnings (host, armv7, thumbv7neon and the bench crate)
• main has been merged in since. Its CMAC files matched the AArch64 branch this was built on, so only Benchmarks: a changed benchmark runs only the benchmarks of its modules #488's benchmark-selection change came along. With it, the Benchmarks run covers only AES-CMAC and AES-GCM.

The x86 (32-bit) implementation is #485, stacked on this PR.

🤖 Generated with Claude Code

https://claude.ai/code/session_01WkLN6tAYk76HACiEWLbAMD

[alex]

The Benchmarks jobs (Compare with base on arm, x86 and two x86_64 configurations) were cancelled at their 15-minute timeout, on the first run and again on one re-run. 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. Even the jobs that finished took 14 of their 15 minutes.

#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 retargeted to main after #469), 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