[alex]

This replaces #4737, which conflicted with main once #4721 deleted vg_aes_ctr32_to's generated files. It adds the 4/2/1 remainder the AES-GCM session asked for, and deletes vg_aes_ctr32_to. Part of the ppc64le performance work from #4141; the audit found AES-CTR at 1.6× aws-lc-rs at 16 KiB.

This is an implementation change only. It changes no TCB or Spec/ file, and it uses vadduwm, which is already in the model.

Why

From the audit run's numbers, the AES rounds cost about 1 cycle per round per block. That is vcipher's throughput, the same floor aws-lc-rs reaches. The gaps are elsewhere:

• Bulk: about 7 cycles per block spent outside the rounds.
• Short messages: the last 0–7 blocks went one at a time, each a serial chain of rounds. A 239-byte GCM message, for example, has 6 serial blocks.

What changes (Impl/Aes/PPC64LE/Crypto.lean)

• Counter:
  • Before, each block's counter took mtvsrd, vperm and addi on a counter word kept in r8.
  • Now the counter block stays in counterBase (v10). Each block takes a copy of it (vor), then vadduwm counterBase, counterBase, counterStep.
  • counterStep (v11) holds counterOne, which is one in the last word. So the add increments the last 32 bits modulo 2³², exactly inc32.
• XOR: CTR's writeBlock loads the data with lxvd2x and puts the keystream into lxvd2x's order with the store's vperm. It XORs in that order and stores with stxvd2x. That is one vperm per block instead of two.
• Counter writeback: at the end, the whole counter block is stored back to the counter (16 bytes; the contract makes all 16 writable). This replaces the byte-reversed store of r8.
• Tail: batches takes the blocks left after the batches of eight (fewer than eight) by four, two and one, by the bits of their number (tailStep). That is at most three serial chains instead of up to seven. ECB shares batches, so its tail changes too.
• vg_aes_ctr32_to: deleted, with ctrWith's out-of-place parameter, its contract (Proof/Aes/PPC64LE/Base.lean) and its proofs. Nothing has called it since PPC64LE AES-GCM: open_to decrypts and hashes in one pass (vg_aes_gcm_decrypt_blocks_to) #4721.

Per block, the loop goes from 10 instructions outside the rounds to 7, and from 3 vperms to 1.

Proofs (Proof/Aes/PPC64LE/Crypto/)

• Counter value: ctrAdd v i, the counter block with i added to its last 32 bits, replaces the r8 counter word. It appears in readValue, in ReadInv, BatchRead, BatchCipher and BatchDone, and in LoopInv, whose counter is now counterBase = ctrAdd icb k.
• Counter step: counter_step shows that vadduwm by counterOne is ctrAdd · 1, via pack4 and the words of counterOne. ctrAdd_repeat shows ctrAdd icb j = inc32^j icb.
• Stores: writeBlock_ok's CTR case shows the stored block is rev128 (v ⊕ rev128 data), using swapDwords_xor, flip_store and rev128_xor.
• Tail: tail_step_ok proves one step. Before the step for c, fewer than 2c blocks are left, so bit c is set exactly when at least c are (bit_test, by decide over eight cases). batches_ok runs the three steps after the batch loop.
• ctr32_wp: in place only. The counter block is stored back with store_ok, and read_write_self16 gives back the advanced block.
• Constant time: still taint_decide over ctr32. The tail branches only on bits of n.

There's no sorry, no new axiom and no change of resource limits.

Checks

• CI is green, including Rust (Linux, PPC64LE, stable), which runs the AES-CTR, ECB, GCM and CCM vector tests on POWER.
• Every step of the static-checks job passes.
• All 16 AES-related PPC64LE registration files build.
• Emit.lean regenerated the crate, changing only vg_aes_ctr32 and the ECB functions in aes.rs and aes_ecb.rs.
• check_lean_public_imports.py reports nothing.

Benchmark

Run 42527285490: arches=powerpc64, base main at 846fbbae, on POWER9. Modules aes_ctr aes_ecb aes_gcm, narrowed to aes-ctr-.*|aes-ecb-encrypt-.*|aes-128-gcm-(encrypt|decrypt), since the full modules exceed the job's budget. Each figure is the fastest of each side's copies.

Benchmark	Base	This PR	Change
aes-ctr-128/64	528 ns	485 ns	8.2% faster
aes-ctr-128/1024	904 ns	864 ns	4.4% faster
aes-ctr-128/16384	7.27 µs	6.66 µs	8.4% faster
aes-ctr-192/16384	8.11 µs	7.50 µs	7.5% faster
aes-ctr-256/16384	9.01 µs	9.27 µs	3.0% slower
aes-128-gcm-decrypt/16384	10.06 µs	9.45 µs	6.1% faster
aes-128-gcm-decrypt/1048576	619 µs	569 µs	8.1% faster
aes-128-gcm-encrypt/64	530 ns	502 ns	5.4% faster
aes-128-gcm-encrypt/192	659 ns	627 ns	4.8% faster
aes-ecb-encrypt-128/16384	6.69 µs	7.10 µs	6.1% slower

• CTR and GCM decryption, which run vg_aes_ctr32's whole loop, are 6–8% faster at 16 KiB and up (AES-128 and AES-192). That is less than the 1.2× I estimated, so the work outside the rounds was not all that held CTR back.
• Short GCM messages (64 and 192 bytes) are about 5% faster, from the 4/2/1 tail. GCM encryption has its own stitched loop and is otherwise unchanged (0.5–2%).
• The runner was noisy: each benchmark's copies spread by 15% to 137% (Base copies / Head copies in the run's summary). aes-ctr-192/64 reads 22% slower in this run, while 64 bytes of AES-128 and AES-256 read faster.

AES-CTR-128 at 16 KiB is now about 1.5× aws-lc-rs's 4.48 µs from the audit run, down from 1.6×.

The two slower rows

I compared the generated code with main instead of rerunning.

• ECB encryption (3–7% slower at 1 KiB and 16 KiB): the code these sizes run is byte for byte the same as on main, and it is at the same offset within the function. assembly/aes_ecb.s and the encoded words in src/aes_ecb.rs first differ after the batch-of-eight loop (labels 24/25), in the tail. Neither size reaches the tail, since both are whole multiples of eight blocks. The function grew by the tail's code, so its placement relative to other functions in the binary may have moved. Its instructions did not.
• AES-256 CTR (3% slower at 16 KiB): it runs the same vg_aes_ctr32 code as AES-128 and AES-192, with 14 rounds instead of 10 or 12. Those read 8.4% and 7.5% faster in the same run.

So neither row reflects a change to the code it runs. Each is runner noise, or for ECB possibly a layout effect of the longer function.

🤖 Generated with Claude Code

https://claude.ai/code/session_01TKUFHGBeNadVff4mCVhkSH

[alex]

The merge queue dropped this PR in run 42528625150, but the failure isn't this PR's. All of the run's test, build and Lean jobs passed; it was tested on top of #4751.

The only failure is all-green's metrics step (job 128879080698). It failed when gh api repos/pyca/verified-garbage/actions/runs/42528625150 exited with status 1: a GitHub API error, not a check of the code. There is no fix to port. Re-queueing should be enough.

---

Generated by Claude Code