TCB: 64-bit little-endian PowerPC (ISA model, printer, ELFv2 target)

[alex]

Part of #55. Stacked on #97 (CI); the base will move to main once that lands. This PR is entirely a trust change: it adds TCB/PPC64LE/ and changes the shared printer interface. No implementation, spec or generated file changes; those follow in their own PRs (ChaCha20, SHA-256, HMAC-SHA-256), stacked on this one.

Trust changes

TCB/PPC64LE/Isa.lean (new): the ISA model

A model of the subset of the Power ISA, Version 3.1C, Book I that the implementations need, in little-endian mode. Each instruction cites the section whose RTL it transcribes:

• add, subf (as sub), addi/subi, li/lis (addi/addis with RA = 0), ori, oris, and/or/xor (§3.3.9, §3.3.13): all on the full 64 bits.
• Rotates and shifts: rlwinm (as rotrwi/srwi; reads the low word and zero-extends its 32-bit result), rldicl (rotrdi/srdi), rldicr (sldi) (§3.3.14).
• Loads and stores: lbz/lwz/ld, stb/stw/std (§3.3.2, §3.3.3), and the byte-reversed lwbrx/ldbrx/stwbrx/stdbrx (§3.3.5). In LE mode MEM(EA, n) is a little-endian read (§1.3.2), so the byte-reversed forms are big-endian accesses. Accesses must lie in the state's permitted regions, or the instruction faults.
• mflr/mtlr (§3.3.19), bl/blr (§2.4).
• Branch conditions: cmplwi/cmpldi against 0 into CR0, then beq/bne (§3.3.10, §2.4). CR0 is volatile (ELFv2 §2.2.2.1) and nothing else reads it.

Modelling choices (all in the module doc):

• Registers are r0, r2–r12, r14–r31. r13 (thread pointer, reserved by ELFv2 §2.2.2.1) is not a Reg, so no code can name it; r1 is only moved by frame push/pop.
• Forms that read (RA|0) fault with RA = r0 (except li/lis), and unencodable immediates/displacements fault, so verified code is always encodable.
• A call leaves unknown values in LR and in r0, r11, r12, which ELFv2 lets linkage code change (§2.2.2.1, "Optional Function Linkage"). The printer never emits a nop after bl, so the linker never inserts a TOC-saving stub (§2.2.1).
• Frames are ELFv2-conformant, 48 bytes: stdu r1,-48(r1) (back chain) then std RS,32(r1); popped by ld RT,32(r1) then addi r1,r1,48.
• No instruction with operand-dependent timing (e.g. divd) is modelled.
• requires is empty: every modelled instruction is in Power ISA 2.07 (POWER8), the baseline of powerpc64le-unknown-linux-gnu.

TCB/PPC64LE/Target.lean (new): the ELFv2 target

64-bit ELF V2 ABI (OpenPOWER, rev. 1.5): arguments in r3–r10 (§2.2.4), result in r3 (§2.2.6), preserved = r2 and r14–r31 (§2.2.2.1; r2 must be restored since a naked function has st_other entry-point bits 0, §3.4.1), and abiPreserved also demands sp and LR unchanged (the printer returns with blr). rustCfg is all(target_arch = "powerpc64", target_endian = "little"), rustAbi is "C".

TCB/PPC64LE/Print.lean (new): the printer

Straightforward mnemonics (%rN registers, rotrwi/rotrdi/srwi/srdi/sldi as the base rlwinm/rldicl/rldicr forms), return blr, call bl.

TCB/Print.lean (and every target's printer): Printer.branch returns lines

A PowerPC conditional branch on a register is two instructions (a compare, then the branch), so branch : M.Cond → String → List String; the existing printers wrap their one line in a list. Their output is unchanged (the existing golden tests and Emit.lean --check confirm it).

Tests (VerifiedGarbageTest/)

• PPC64LE.lean: the semantics of every instruction on concrete values, each cross-checked against the same instruction run under qemu-ppc64le.
• Print.lean: the printing of every instruction, branch, call, return and frame.
• Frames.lean, Abi.lean: frame push/pop and the ELFv2 argument/stack conventions.

Checks

lake build (all proofs and golden tests), lake env lean --run Emit.lean --check, ci/check_lean_imports.py, ci/check_lean_speed.py, ci/check_vectors.py, cargo fmt --check, and cargo clippy/cargo test on x86-64 and (cross-built, under qemu) ppc64le all pass.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Fw6RULWHCeVgMDGc3wRrwE

---

Generated by Claude Code