HMAC-SHA-256 on PPC64LE: verified init/finalize

[alex]

Part of #55. Stacked on #110 (SHA-256), #109 (ChaCha20), #108 (TCB) and #97 (CI). There are no TCB or spec changes. This PR adds implementations proven against the existing Spec.Hmac.initSha256Contract, finalizeSha256Contract and Spec.Ct.eqContract.

HMAC-SHA-256 on PPC64LE

The algorithm is the same as on ARMv7:

• vg_hmac_sha256_init stores H⁽⁰⁾ in both states, XORs the key into the ipad and opad blocks, and calls vg_sha256_compress on each.
• vg_hmac_sha256_finalize calls vg_sha256_finalize on the inner state and rebuilds it as (K₀ ⊕ opad) ‖ digest from the outer hash value. It then finalizes it again, leaving the MAC in scratch[176..208) (finalizeSha256Contract).
• Both move the link register to r0 and save it in an ELFv2 frame (48 and 96 bytes of stack, since finalize's callee pushes its own frame).
• init keeps its variables in r26–r31 (saved in scratch), and finalize keeps them in r24–r25, which the callees preserve.

On main, x86-64 and AArch64 now get HMAC from the one generic implementation over every Merkle–Damgård hash, and ARMv7 and x86 keep their own init/finalize against the per-hash contracts. PPC64LE follows ARMv7 and x86, since it has a single SHA-256 implementation:

• The functions are registered per hash: Artifacts/HmacSha256/PPC64LE.lean (Api form), module hmac_sha256.
• The shared contracts give 608/688 bytes of scratch. The proofs use 160/240 bytes, and Shared.lean widens them (Verified.widen).
• The target-independent lemmas come from Proof/Hmac/Common.lean, so no PPC64LE module imports another target's.

Constant-time comparison on PPC64LE

Hmac::verify compares MACs with vg_ct_eq (crate::ct), which main added since this PR was opened, so HMAC on PPC64LE needs it as well. The second commit adds it with the AArch64 algorithm, in Impl/Ct/PPC64LE.lean:

• If the lengths differ, return 0.
• Otherwise OR the XORs of the bytes at each offset into r7 and return (r7 - 1) >> 63.

The branches are on the lengths only. The proof in Proof/Ct/PPC64LE.lean follows Proof/Ct/AArch64.lean and its shared Proof/Ct/Common.lean. The artifact is registered in Artifacts/Ct/PPC64LE.lean.

Rust

• src/hmac/mod.rs's module gate, src/hmac/sha256.rs and src/ct.rs name PPC64LE.
• PPC64LE uses the ARMv7/x86 HmacHash implementation for SHA-256 (Sha256HmacState), with its own hmac_finalize, which reads the MAC from scratch (as the 64-bit targets did before they moved to the generic HMAC).
• sha256_key_states, which only PBKDF2 uses, stays on ARMv7 and x86. The streaming_hmac! machinery and the other hashes' HMACs stay off PPC64LE.
• tests/wycheproof/hmac.rs and hmac_sha256.rs name PPC64LE, and the HMAC-SHA-256 benchmark loses CI: test on ppc64le, on a ppc64le runner as pyca/cryptography does #97's gate.

README

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

Testing

On #97's head (main at 48dfb92), 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 cross-built for powerpc64le-unknown-linux-gnu under qemu-ppc64le (the unit tests, including ct's; Wycheproof HMAC-SHA-256 and ChaCha20; CAVP SHA-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_hmac_sha256_init/finalize on PPC64LE): move them out of lean/VerifiedGarbage/Artifacts.lean into registration files, one per algorithm and target: lean/VerifiedGarbage/Artifacts/Hmac/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 (2ed5ea3): vg_hmac_sha256_init/finalize on PPC64LE are in lean/VerifiedGarbage/Artifacts/Hmac/PPC64LE.lean, src/hmac.rs and tests/wycheproof/hmac.rs name PPC64LE in their inner #[cfg(...)] (the PPC64LE import follows main's new form: only hmac:: symbols, vg_sha256_update now comes through Sha256Backend), and the README row is regenerated. The bases got the same moves first.

---

Generated by Claude Code

[alex]

The ppc64le rust job on 0640461 failed in its "Install Rust" step, before anything was built. This is not caused by this PR's changes. Rust 1.99.0 came out today, and rustup toolchain install stable can't upgrade the toolchain preinstalled in pyca's runner images:

error: failure removing component 'cargo-powerpc64le-unknown-linux-gnu', directory does not exist: 'share/man/man1/cargo.1'

The armv7l job on main has been failing the same way since about 12:42 UTC, and #458 fixes it by installing into a fresh RUSTUP_HOME. I ported that change, applied to the ppc64le platform, into #97 (5b9345f), and rebased this stack onto it. This PR's new head, dc7bf04, is otherwise identical to 0640461.

---

Generated by Claude Code