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

[alex]

Part of #55. Stacked on #109 (ChaCha20, which now carries the whole PPC64LE proof framework, calls and frames included), #108 (TCB) and #97 (CI). There are no TCB or spec changes. This PR adds implementations proven against the existing Spec.Sha256 contracts.

SHA-256 on PPC64LE

• vg_sha256_compress:
  • The working variables are in the low words of r7–r12, r14 and r15; the fully unrolled rounds rename them.
  • The 16-word schedule window is in scratch[0..64), and the nonvolatile r14–r19 are saved in scratch[64..112).
  • The message is loaded big-endian with lwbrx, and each Kₜ is built with lis/ori.
• vg_sha256_init/update/finalize follow the AArch64 implementation:
  • Their variables live in r26–r31, with the caller's values saved in scratch[112..160).
  • They call vg_sha256_compress.
  • The link register is moved to r0 and saved in an ELFv2 frame, so update/finalize use 48 bytes of stack (stack := 48).
  • The digest and the bit length are stored big-endian with stwbrx/stdbrx.
• The update/finalize proofs track r14–r19, which only the compression function writes, through its ABI guarantee.
• Any initial hash value: since Spec: SHA-224, and SHA-256's update and finalize for any initial hash value #452, updateContract and finalizeContract hold for a state hashed from any initial hash value (ReprFrom iv, finalHash iv), so SHA-224 can share them.
  • The PPC64LE contracts and proofs quantify over iv, as ARMv7's and AArch64's do.
  • Proof/Sha256/Stream.lean (untrusted, target-independent) gets iv-general versions of its lemmas: reprFrom_congr, reprFrom_append_buf, reprFrom_append_block, finalHash_eq, finalHash_one and finalHash_two. The existing Repr/hash lemmas are now their H0 cases, so other callers are unchanged.
  • vg_sha224_init is not implemented on PPC64LE; SHA-224 stays off it for now.
• Scratch sizes: on main, the shared contracts give 560 bytes of scratch to compress and 608 to update/finalize (sized for x86-64's AVX2 code). As on AArch64, the proofs use 112/160 bytes, and Shared.lean widens them with Verified.widen. The PPC64LE Verified.widen now uses Exec.rdwr, as AArch64's does, so it applies to code with frames.
• The byte-order lemmas of finalize (rev32_bytes, rev64_bytes) are now PPC64LE's own, so no PPC64LE module imports an x86-64 one (ci/check_lean_imports.py).
• The four artifacts are registered in Api form in Artifacts/Sha256/PPC64LE.lean.

Rust

• src/hashes/sha256.rs names PPC64LE in its inner #[cfg(...)], as do the hashes and tests/cavp umbrella cfgs.
• tests/cavp/sha1.rs, sha224.rs and sha512.rs get their own four-architecture gates, since they share the CAVP binary (ci/check_arch_gates.py).
• The SHA-256 benchmark loses CI: test on ppc64le, on a ppc64le runner as pyca/cryptography does #97's gate.
• SHA-256 uses only the scalar backend on PPC64LE.

README

Regenerated by ci/algorithms_table.py: SHA-256 is ✅ on PPC64LE.

Testing

On #97's head (merged with main at 101fe4b), 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, check_mcdt.py, algorithms_table.py
• cargo fmt, and cargo clippy -D warnings on the host and for ppc64le
• cargo test cross-built for powerpc64le-unknown-linux-gnu under qemu-ppc64le (CAVP SHA-256 short, long and Monte Carlo)

🤖 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_sha256_* on PPC64LE): move them out of lean/VerifiedGarbage/Artifacts.lean into registration files, one per algorithm and target: lean/VerifiedGarbage/Artifacts/Sha256/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 (8ea0ee5): the four vg_sha256_* artifacts on PPC64LE are in lean/VerifiedGarbage/Artifacts/Sha256/PPC64LE.lean (the same entries as Artifacts/Sha256/AArch64.lean up to the target and the 48-byte frame), src/hashes/sha256.rs names PPC64LE in its inner #[cfg(...)] (and the hashes and tests/cavp umbrella cfgs, which still list architectures, add it), and the README row comes from ci/algorithms_table.py. SHA-256's backend selection uses cpu.rs's detection, so this PR also drops #97's allowance for it going unused on PPC64LE. The base (#109) got the same moves first.

---

Generated by Claude Code