Claim: ChaCha20 (all architectures)

[reaperhulk]

Part of #1. I'm taking ChaCha20 (the stream cipher, RFC 8439 block function; the init(key, nonce) / update / reset_nonce API from #1) on every target listed in the README, one architecture at a time:

• Spec: Spec/ChaCha20.lean (transcribed from RFC 8439 §2.1–2.4) and the x86-64 contract of its block function — Spec: ChaCha20 (RFC 8439) and the x86-64 contract of its block function #13 (merged)
• x86-64: implementation + proof + artifact + Rust API + Wycheproof/RFC 8439 tests (builds on the 32-bit instructions in TCB: x86-64 32-bit instructions (mov, store, ALU, ror/shr, bswap) and Region.Disjoint #4; rol by k is ror by 32−k, so no further TCB additions) — ChaCha20 on x86-64: verified block function and the ChaCha20 API #18 (merged)
• x86: contract → implementation (on TCB: x86 (32-bit) model, printer and cdecl target #23's model, no TCB additions needed) — Spec: the x86 (32-bit) contract of the ChaCha20 block function #26, ChaCha20 on x86 (32-bit): verified block function #27 (merged)
• ARM64: contract → implementation (on TCB: AArch64 model, printer and AAPCS64 target #10's model, no TCB additions needed) — Spec: the AArch64 contract of the ChaCha20 block function #19, ChaCha20 on AArch64: verified block function #20 (merged)
• ARMv7: contract → implementation (on TCB: ARMv7 model, printer and AAPCS target #14's model, no TCB additions needed) — Spec: the 32-bit ARM contract of the ChaCha20 block function #21, ChaCha20 on 32-bit ARM: verified block function #22 (merged)
• PPC64le: contract → implementation (no PPC64le model upstream yet)

Each item is its own PR (or PRs), following the one-kind-of-change-per-PR rule. This claim is for ChaCha20 itself, not the ISA models for x86 / ARM64 / ARMv7 / PPC64le: if someone else lands one of those first I'll build on it, and I'll comment here before starting one myself. ChaCha20-Poly1305 is not part of this claim.