ChaCha20 on PPC64LE: verified block function and keystream XOR

[alex]

Part of #55. Stacked on #108 (the PPC64LE TCB), which is stacked on #97 (CI). There are no TCB or spec changes. This PR adds implementations proven against the existing Spec.ChaCha20.blockContract, Spec.ChaCha20.xorContract and Spec.Zeroize.zeroizeContract, plus the proof framework they need.

Commits

1. Proof: PPC64LE framework (symbolic execution, taint tracking, calls): Proof/Framework/PPC64LE/{Exec,Taint,Inline,Call}.lean, ported from the AArch64 framework:

   • The runBlock_cons/runStep_some/runBlock_nil stepping lemmas.
   • Proofs that sp is unchanged, and LR too in code without calls.
   • The taint analysis for VG.Taint.constantTime … (by taint_decide).
   • Running verified code with wider permissions (Exec.widen), registers that code never writes (Exec.gpr), calls of verified functions (WP.call) and the ELFv2 frames that save LR (WP.frameReg).

   32-bit values are tracked as the low word of a register, since add/subf/logical instructions act on all 64 bits; lo32_add and friends push the low word through them. The byte-reversed loads use the target-independent Proof/Framework/Bswap.lean lemmas, so no PPC64LE module imports another target's (ci/check_lean_imports.py).

2. ChaCha20 on PPC64LE:

   • vg_chacha20_block keeps the 16 state words in the low words of r5–r12 and r14–r21. It saves the nonvolatile r14–r21 in the working half of buf (bytes 64–127) and restores them at the end; r0 is the temporary for adding the input state. Rotations are rotrwi (rlwinm), which read the low word and ignore the carries the 64-bit adds leave in the high word.
   • vg_chacha20_xor follows the AArch64 implementation. It calls vg_chacha20_block once per 64 bytes of data and XORs min(64, remaining) bytes of the output into the data, a byte at a time. It then increments the counter word. state and buf stay in r3/r4, which the block function never writes. The data pointer and remaining length are kept in the nonvolatile r22/r23. Our caller's r22/r23, and the return address (mflr r0), are saved in buf[256..280), so no stack is used (stack := 0, as on the other targets). The proof tracks r14–r21 across the calls through the block function's ABI guarantee.
   • Proofs are in Proof/ChaCha20/PPC64LE/. Both artifacts are registered (in Api form) in Artifacts/ChaCha20/PPC64LE.lean, and src/asm/powerpc64le/ is regenerated.

3. Zeroization on PPC64LE: since main added vg_zeroize (crate::zeroize, used by ChaCha20's Drop), every architecture that builds ChaCha20 needs it. It is the AArch64 algorithm, in Impl/Zeroize/PPC64LE.lean: std of zero over len / 8 words, then stb over len % 8 bytes. The proof in Proof/Zeroize/PPC64LE.lean follows Proof/Zeroize/AArch64.lean and its shared Proof/Zeroize/Common.lean. The artifact is registered in Artifacts/Zeroize/PPC64LE.lean. A small crun tactic (Proof/Framework/PPC64LE/Run.lean) steps short blocks, as the AArch64 proofs' does.

Rust

• src/lib.rs aliases crate::arch to asm::powerpc64le on little-endian powerpc64.
• src/chacha20.rs, src/zeroize.rs and tests/wycheproof/chacha20.rs name PPC64LE (all(target_arch = "powerpc64", target_endian = "little")) in their inner #[cfg(...)].
• The ChaCha20 benchmark loses the gate that CI: test on ppc64le, on a ppc64le runner as pyca/cryptography does #97 added. bench_arches.py does not benchmark PPC64LE.
• ChaCha20 now picks its backend with cpu::detected() on every architecture, so the allow(dead_code) that CI: test on ppc64le, on a ppc64le runner as pyca/cryptography does #97 added to src/cpu.rs for PPC64LE is dropped.

README

The table is generated. ci/algorithms_table.py now knows PPC64LE (ARCHES gets "powerpc64", and ASM_DIRS maps it to src/asm/powerpc64le/), and the ✅ definition includes it. ChaCha20 is ✅ on PPC64LE; every other algorithm is ❌ there for now.

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 on x86-64, and cross-built for powerpc64le-unknown-linux-gnu under qemu-ppc64le (the unit tests, including zeroize's, and the Wycheproof ChaCha20 vectors)

🤖 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_chacha20_block on PPC64LE): move them out of lean/VerifiedGarbage/Artifacts.lean into registration files, one per algorithm and target: lean/VerifiedGarbage/Artifacts/ChaCha20/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: the whole stack (#97 → #108 → #109 → #110 → #111 / #117) is rebuilt on current main (d0c1a92) in the new layout, and force-pushed.

In this PR (93ee3bf):

• vg_chacha20_block on PPC64LE is registered in lean/VerifiedGarbage/Artifacts/ChaCha20/PPC64LE.lean; Artifacts.lean is untouched.
• src/chacha20.rs and tests/wycheproof/chacha20.rs name PPC64LE in their own inner #[cfg(...)]; lib.rs and tests/wycheproof/main.rs are untouched.
• The README table is regenerated by ci/algorithms_table.py, which now knows PPC64LE (ARCHES gets "powerpc64", and src/asm/powerpc64le/ for its assembly). Since ✅ now includes PPC64LE, the SHA-256 and HMAC rows read "x86-64, ARM64, ARMv7, x86" until SHA-256 on PPC64LE: verified compress/init/update/finalize #110 and HMAC-SHA-256 on PPC64LE: verified init/finalize #111.

lake build, Emit.lean --check, the Lean/vector/table checks, fmt/clippy (host and ppc64le) and cargo test (host, and ppc64le under qemu) pass on every branch of the stack.

---

Generated by Claude Code