[alex]

This removes a check that duplicates what the proofs already establish. It cleans up my merged PRs (#4666 and #4693), under the new rule that a #guard stays only if it pins down something nothing else does.

What changes

The #guard in Impl/TripleDes/PPC64LE/Bitsliced.lean, added in #4666, checked one thing: that the written-out S-box code is what the register allocator (compile) produces. The proofs check that same code directly against the S-boxes, so the #guard was redundant:

• sbox_check and sboxLiteral_eq in Proof/TripleDes/PPC64LE/Bitsliced/Sbox.lean;
• taint_decide for constant time.

It isn't a TCB check either.

Removed:

• the #guard;
• Impl/TripleDes/PPC64LE/BitsliceAlloc.lean, the allocator, which only that #guard used;
• freeRegs, which likewise had no other use.

Two doc comments no longer mention them.

The generated code is unchanged: EmitOne.lean --check TripleDes.PPC64LE emits identical assembly.

The rest of the audit

None of my PRs added Rust tests:

• 3DES PPC64LE: bitsliced ECB, 64 blocks at a time #4666: bitsliced ECB.
• 3DES PPC64LE: the round function as a 64-lane table lookup #4693: single block.
• 3DES PPC64LE: CBC and CFB64 decryption 64 blocks at a time #4694: batched CBC/CFB64 decryption.
• PPC64LE brainpoolP256r1, P384r1: public keys and signatures by the comb #4711: brainpool combs.

All four are covered by the existing Wycheproof and published vectors. #4693 and #4711 added no #guard. #4694 carries #4666's commits, so it drops the #guard when it is restacked onto main.

Testing

• The 3DES PPC64LE registration builds.
• EmitOne --check shows the same code.
• The static checks pass.

No Rust or TCB change.

---

Generated by Claude Code

[alex]

The merge queue's run (42522838991) failed only in Rust (macOS, AArch64, stable), at actions/checkout: git exited with 128 before any build or test ran, so all-green failed. No job reached this PR's code, and its own CI passed. It looks like infrastructure, maybe the queue's temporary branch going away while the queue reshuffled. The PR can go back in the queue as is.

---

Generated by Claude Code