[alex]

Part of #4141, the small-message gap in AES-GCM on PPC64LE.

Below sixteen blocks, vg_ghash on PPC64LE hashed one block per multiply and reduction, each depending on the last. In a 239-byte TLS record that is about 15 such steps, each roughly 36 cycles of latency.

Now it hashes two blocks per iteration, (Y ⊕ X₁)·H² + X₂·H, with one reduction (pairBody):

• below sixteen blocks, from four blocks up (pairsIf 2 paired), after computing H² (preparePowers 2) and the packed H², H (packKeyStep 3);
• after the eight-block loop, from two blocks up (pairsIf 1 pairLoop), since that loop already leaves the packed H², H.

The last block, if the count is odd, still goes through the single-block loop. The pair loop writes no accumulator register, so H stays where it is. The eight-block path is unchanged.

vg_ghash is internal and shared: AES-GCM, AES-GCM-SIV and SM4-GCM on PPC64LE call it. Their code is unchanged except for the regenerated vg_ghash.

Proofs

• Proof/Gcm/PPC64LE/Vpmsum/Fold.lean: pairKeys_ok, and pairBody_ok, whose result is hashField (x·φ H) Y _ 2. Both reuse packedRead_ok, packedProducts_ok and reduce_ok.
• Proof/Gcm/PPC64LE/Vpmsum/Ghash.lean:
  • pair_step_ok, pairLoop_ok, paired_ok and pairsIf_ok;
  • bulk_ok now also keeps the packed H², H;
  • correct, over the new structure.
  • ghash_ct is still taint_decide.

No TCB or Spec change, and no Rust change.

Testing

• lake build and the full Emit.lean pass.
• The static checks from ci.yml pass, as does check_lean_public_imports.py on the edited modules.
• On powerpc64le-unknown-linux-gnu under qemu, the tests filtered by gcm, siv and sm4 pass, including Wycheproof.

Benchmark

First commit (pairs from two blocks): https://github.com/pyca/verified-garbage/actions/runs/42525152473 (powerpc64, against the merge-base; fastest of 8 copies):

Benchmark	Base	Head	Change
tls-seal/239	456 ns	407 ns	10.7% faster
tls-open/239	436 ns	385 ns	11.7% faster
tls-seal/207	407 ns	366 ns	10.0% faster
tls-open/207	389 ns	347 ns	10.8% faster
tls-seal/127	281 ns	259 ns	7.9% faster
tls-open/127	272 ns	249 ns	8.8% faster
encrypt/192	662 ns	617 ns	6.8% faster
decrypt/192	681 ns	636 ns	6.7% faster
encrypt/64	529 ns	524 ns	0.9% faster
decrypt/64	560 ns	549 ns	2.0% faster
encrypt/384	731 ns	732 ns	0.0% slower
decrypt/384	758 ns	754 ns	0.5% faster
tls-seal/31	181 ns	186 ns	2.9% slower
tls-seal/47	205 ns	209 ns	2.0% slower
tls-open/31	184 ns	188 ns	2.2% slower
tls-open/47	207 ns	209 ns	1.2% slower

Every other row is within ±2%; nothing at 1 KiB and above changes.

• TLS records of 31 and 47 bytes were the only slowdowns. Below sixteen blocks those records hash 2–3 blocks of ciphertext, and computing H² costs about as much as one pair saves. The second commit therefore starts pairs below sixteen blocks only from four blocks up. Rerun of the TLS groups on the second commit, the head: https://github.com/pyca/verified-garbage/actions/runs/42526720746.

Benchmark	Base	Head	Change
tls-seal/15	156 ns	157 ns	0.5% slower
tls-seal/31	181 ns	182 ns	0.7% slower
tls-seal/47	206 ns	207 ns	0.6% slower
tls-seal/63	231 ns	226 ns	2.3% faster
tls-seal/127	281 ns	259 ns	8.0% faster
tls-seal/239	456 ns	407 ns	10.7% faster
tls-open/31	184 ns	184 ns	0.2% faster
tls-open/47	207 ns	207 ns	0.2% faster
tls-open/127	272 ns	248 ns	8.7% faster
tls-open/239	437 ns	385 ns	11.9% faster

Every other row is within ±3%, and nothing at 1 KiB and above moves more than 0.3%.

https://claude.ai/code/session_01TKUFHE3csexSeALfzJpHUJ

---

Generated by Claude Code