Claim: SHA-384 / SHA-512 / SHA-512/224 / SHA-512/256 (x86-64 first)

[reaperhulk]

Claiming the SHA-512 family from #1, in separate PRs per CLAUDE.md:

1. TCB: x86-64 64-bit ror/shr by an immediate, bswap r64, and mov r64, imm64 (movabs), on top of TCB: x86-64 32-bit instructions (mov, store, ALU, ror/shr, bswap) and Region.Disjoint #4
2. Spec: Spec/Sha512.lean (FIPS 180-4) + the x86-64 contract of the compression function, on top of TCB: x86-64 32-bit instructions (mov, store, ALU, ror/shr, bswap) and Region.Disjoint #4
3. x86-64 impl + proof + artifact + Rust API (Sha384, Sha512, Sha512_224, Sha512_256), reusing SHA-256 on x86-64: verified compression function and the Sha256 API #6's proof framework

Other architectures later, one PR each. Not claiming HMAC/PBKDF2 (#7/#8 are generic over the hash). If someone lands a piece first I'll build on it.

[reaperhulk]

Status update, and a question before I rebase the rest of the stack onto main.

Opened:

• Test vectors: vendor the NIST CAVP SHA-384 and SHA-512 family vectors, with their provenance #49 vendors the CAVP SHA-384/512/512-224/512-256 vectors (following Test vectors: vendor the NIST CAVP SHA-256 vectors, with their provenance #28).
• The x86-64 TCB PR (64-bit ror/shr and movabs r64, imm64) is next, targeting main directly. bswap r64 has been dropped from it because TCB: x86-64 byte load/store (movzx, mov BYTE PTR) and 64-bit bswap #30 already added it.

Question: compression function first, or straight to streaming? The SHA-512 x86-64 implementation I have verifies vg_sha512_compress. Padding, buffering and the 128-bit length are in Rust, which is where SHA-256 stood after #6. Since then SHA-256 has moved to verified init/update/finalize (#31/#33). There are two ways to go:

1. Compression first (ready now, once rebased): the spec, the x86-64 contract, then impl + proof + a Rust API tested against every CAVP vector. The streaming spec and implementation follow as their own PRs, as with Spec: streaming SHA-256 and its x86-64 contracts (init, update, finalize) #31/SHA-256 on x86-64, AArch64 and ARMv7: verified streaming init/update/finalize #33.
2. Streaming only: skip the compression-only Rust API and go straight to Repr + init/update/finalize contracts and proofs, with vg_sha512_compress only inlined. This is a lot more proof work before anything lands. It also means deciding the length question: FIPS 180-4 pads with a 128-bit bit length, while SHA-256's streaming state keeps a public u64 byte count. Keeping that count works if the contract states that the high bits of the 128-bit length are zero (messages under 2⁶⁴ bytes).

Either way the spec stays split: Spec/Sha512.lean (target-independent) plus Spec/Sha512/X86_64.lean. The plan is (1) unless you'd rather have (2).

---

Generated by Claude Code

[alex]

Straight to streaming please

[alex]

We're still missing these for 32-bit x86