SHA-384/512/512-224/512-256 on PPC64LE: verified compress/init/update/finalize

[alex]

Part of #55. Stacked on #110 (SHA-256, whose stream lemmas it reuses), and so on #109, #108 and #97. It is independent of the HMAC PR (#111). There are no TCB or spec changes. This PR adds implementations proven against the existing Spec.Sha512 contracts.

What

• vg_sha512_compress(state = r3, blocks = r4, n = r5, scratch = r6) has the structure of the PPC64LE SHA-256 implementation, on whole 64-bit registers:
  • The working variables live in r7–r12, r14 and r15, renamed by the unrolled rounds.
  • The 16-word schedule window is in scratch[0..128), and the nonvolatile r14–r19 are saved in scratch[128..176).
  • The message is loaded big-endian with ldbrx.
  • Each Kₜ is built with lis, ori, sldi, oris, ori (movImm64, proven equal to the constant once, movImm64_eq).
• vg_sha384_init/vg_sha512_init/vg_sha512_224_init/vg_sha512_256_init, vg_sha512_update and vg_sha512_finalize:
  • As on AArch64, these inline the compression function instead of calling it. They change neither the link register nor the stack, and need no frame (the contracts take stack = 0).
  • Their variables live in r26–r31, with the caller's values saved in scratch[176..224).
  • The update/finalize proofs track r14–r19, which only the inlined compression function writes, through its Verified ABI guarantee (WP.inline).
  • The final hash value and the 128-bit bit length are stored big-endian with stdbrx.

The proofs are in Proof/Sha512/PPC64LE/. The code uses 176 bytes of scratch for compress and 224 for update/finalize. Shared.lean widens these to the shared contracts' current 1328/1376 bytes (sized on main for x86-64's AVX2 compression function), as AArch64 does, and moves them to the shared contracts. The seven artifacts are registered in Api form in Artifacts/Sha512/PPC64LE.lean.

Rust

• src/hashes/sha512.rs names PPC64LE in its inner #[cfg(...)]. PPC64LE uses only the scalar backend.
• tests/cavp/sha512.rs and the SHA-512 benchmark lose the four-architecture gates that SHA-256 on PPC64LE: verified compress/init/update/finalize #110 and CI: test on ppc64le, on a ppc64le runner as pyca/cryptography does #97 gave them.

README

Regenerated by ci/algorithms_table.py: the SHA-384/512 row is ✅ on PPC64LE.

Testing

On current main (with #97), these all pass:

• lake build and Emit.lean --check
• ci/check_lean_imports.py, check_lean_speed.py, check_vectors.py, check_arch_gates.py, check_variants.py, algorithms_table.py --check
• cargo fmt, and cargo clippy -D warnings on the host and for ppc64le
• cargo test on x86-64, and cross-built for powerpc64le-unknown-linux-gnu under qemu-ppc64le (CAVP short, long and Monte Carlo for all four of SHA-384, SHA-512, SHA-512/224 and SHA-512/256)

🤖 Generated with Claude Code

https://claude.ai/code/session_01Fw6RULWHCeVgMDGc3wRrwE

[reaperhulk]

This PR still uses the old layout that the conflict restructure (#144, #147, #148, #150) replaced on main. Moving it over makes it add files instead of editing shared lists, so it stops conflicting with other PRs.

What to move:

• Artifacts.lean entries (vg_sha512_* and the SHA-384/512-224/512-256 inits on PPC64LE): move them out of lean/VerifiedGarbage/Artifacts.lean into registration files, one per algorithm and target: lean/VerifiedGarbage/Artifacts/Sha512/PPC64LE.lean. Each defines VG.Artifacts.<Alg>.<Target>.artifacts : List Artifact (see Artifacts/Selftest/X86_64.lean or Artifacts/Scrypt/X86_64.lean); Emit.lean finds them automatically. The legacy SHA/HMAC/ChaCha20/MD5/SHA-1/SHA-3 entries are also moving into such files in a pending PR, so if a file you need already exists by then, append to its list.
• README table: if README: generate the algorithm table from the code #151 lands, the table is generated; add a docs/algorithms/<alg>.toml and run python3 ci/algorithms_table.py instead of editing README.md by hand.

This PR is stacked on another branch, so apply the same moves on that base first.

See the "Keeping parallel PRs from conflicting" section of CLAUDE.md and step 4 of "Adding a primitive".

---

Generated by Claude Code

[alex]

Done, on current main (0f3b0ca): the seven vg_sha512_*/vg_sha384_init/vg_sha512_224_init/vg_sha512_256_init artifacts on PPC64LE are in lean/VerifiedGarbage/Artifacts/Sha512/PPC64LE.lean (the same entries as Artifacts/Sha512/AArch64.lean up to the target, plus explicit spSafes), src/hashes/sha512.rs and tests/cavp/sha512.rs name PPC64LE in their inner #[cfg(...)], and the README row is regenerated. The bases got the same moves first. SHA-384/512 and the CAVP vectors pass under qemu-ppc64le.

---

Generated by Claude Code