[alex]

Part of the PPC64LE performance work from #4141, following #4733.

ppc64le's AES key expansion (vg_aes_expand_key, vg_aes_expand_key_scratch) computed every key length one word at a time in GPRs, with a GPR→VSR→vsbox→GPR round trip for each SubWord. 16- and 32-byte keys now compute a whole round key, four words, per step in vector registers. 24-byte keys keep #4733's word loop.

How it works

Four consecutive words w[j..j+3] are held as the 128-bit value w[j+3] ‖ w[j+2] ‖ w[j+1] ‖ w[j], which is the schedule's 16 bytes read as one little-endian number. The next four words are temp XORed into the prefix XORs of the previous four (w[j], w[j] ⊕ w[j+1], …). Each step:

• vperm copies the last word into every word, rotated by a byte for RotWord, or not;
• vsbox substitutes it;
• for 16-byte keys and the even steps of 32-byte keys, vxor adds the round constant, which is in the low byte of every word. It comes from r6, computed as the word loop computes it, through mtvsrd and vperm.
• two vsldoi shifts and two vxors form the prefixes.

A 16-byte key runs 10 such steps. A 32-byte key runs 6 pairs of steps (SubWord(RotWord) with the constant, then SubWord alone), then a final step. Each step's four words are stored with one stxvd2x. Every branch depends only on the key length or a count.

Files

• Impl/Aes/PPC64LE/Crypto/ExpandKey.lean: the dispatch on the key length and the vector loops. The word loop is unchanged, moved into wordTail.
• Proof/Aes/PPC64LE/Crypto/KeyVecBytes.lean (new): the byte-level facts.
  • Rk: a vector register holds four schedule words.
  • vbyte_sldoi and pfx_byte: the prefix XORs.
  • step_rk and next_pre: FIPS 197's recurrence, four words at a time.
  • rot_temp and sub_temp: RotWord, SubWord and the round constant in every word.
  • load_rk and store_good: the schedule's 16-byte loads and stores.
• Proof/Aes/PPC64LE/Crypto/KeyVec.lean (new): each instruction group run symbolically, the loops' invariants (VInv4, VInv8) and the setup (VStart).
• Proof/Aes/PPC64LE/Crypto/ExpandKey.lean: expandKey_ok dispatches like the code. Its statement is unchanged, so the contracts above it are unchanged.
• Proof/Aes/PPC64LE/Crypto/KeyCopy.lean: the copy loop's invariant allows r0 to change, because the length test writes it.

There is no spec or TCB change. The constant-time proof is the existing taint_decide over the new code.

Checks run locally

• full lake build and Emit.lean --check, after rebasing on main
• the static checks
• check_lean_public_imports.py on the edited modules
• ppc64le clippy

There are no new tests: the existing AES vectors cover every key length. A benchmark run (aes-*-gcm-new and AES-GCM-SIV on powerpc64, against main) follows in a comment.

---

Generated by Claude Code

[alex]

Benchmarks on POWER9 (run 42527569434) against main at 6177d9bc, limited to key setup (aes-*-gcm-new) and AES-GCM-SIV, which expands a new key for every message. Times are medians.

Benchmark	Base	Head	Change
aes-128-gcm-new/16	222 ns	148 ns	33.4% faster
aes-256-gcm-new/32	279 ns	151 ns	45.9% faster
aes-128-gcm-siv-encrypt/64	608 ns	452 ns	25.6% faster
aes-128-gcm-siv-decrypt/64	648 ns	469 ns	27.6% faster
aes-256-gcm-siv-encrypt/64	880 ns	585 ns	33.5% faster
aes-256-gcm-siv-decrypt/64	841 ns	594 ns	29.3% faster
aes-128-gcm-siv-encrypt/1024	1.78 µs	1.55 µs	12.6% faster
aes-128-gcm-siv-decrypt/1024	1.80 µs	1.68 µs	6.8% faster
aes-256-gcm-siv-encrypt/1024	2.07 µs	1.73 µs	16.4% faster
aes-256-gcm-siv-decrypt/1024	2.12 µs	1.82 µs	14.2% faster

At 16 KiB and 1 MiB, the changes are between 4.2% faster and 2.0% slower, which is noise: key expansion runs once per message. The gcm-new medians vary a lot between the base and head copies (10–35%), but the gap between them is larger than that.

AES-256 gains the most because its schedule has 52 words to compute against 40 for AES-128. In both, each step of four words replaces four iterations of the word loop and its GPR↔VSR round trip.

The first dispatch's failure on this PR was a wrong base_commit input I gave it. It measured nothing.

---

Generated by Claude Code