SHA-384/512/512-224/512-256 streaming on x86 through the shared MdStream code

[alex]

This came out of a review that looked for duplicated code pointing to missing abstractions.

Summary

On x86-64, the SHA-512 family's streaming update and finalize already run on the shared Merkle–Damgård code (Impl/MdStream/X86_64). On 32-bit x86 they did not: the shared code only handled 64-byte blocks with an 8-byte length field, so SHA-512 had its own streaming code (Impl/Sha512/X86/Stream.lean) and about 2,500 lines of its own proofs.

This PR makes the x86 code generic over the block size and length-field size, as x86-64 already is. The SHA-512 family becomes one more instance of it, and its own streaming code and proofs are deleted.

Does not touch Spec/ or TCB/.

The abstraction

• Impl/MdStream/X86.lean
  • Params gains B (block size) and L (length-field size).
  • Every hard-coded 63 / 6 / 64 / 56 / 57 becomes B - 1, log₂ B, B, B - L or B - L + 1.
  • New out64 writes 64-bit words, stored little-endian, out big-endian.
  • len64 is split into loadCount ++ len64Of. The instructions are unchanged. The split lets SHA-512's 128-bit length field read count before writing anything.
• Proof/MdStream/X86/Common.lean
  • Dims gains B ∈ {64, 128} and 0 < L ≤ 16, plus lemmas for x mod B, x / B and the shift amount (Dims.and, Dims.shr, Dims.lg, Dims.mod, Dims.mod_append).
  • The contracts, Shape and CalleeOk are over Md P.B P.N P.L.
• Proof/MdStream/X86/Finalize.lean (the update and finalize proofs) is generalised throughout.
  • The finalize proof now shows that finalize only reads its arguments (finK); it never wrote them.
  • Finalize.verified derives the old, looser contract (finKw, arguments writable) from that with Verified.narrowTo, so MD5, SHA-1 and SHA-256 keep their per-target contracts unchanged.
  • The SHA-512 family needs the read-only form, which Ed25519 and HMAC/PBKDF2 already rely on. Because of this, none of those callers changed.
• Proof/MdStream/X86/Words.lean
  • out_words is generic over the word size; out32_ok and the new out64_ok both use it.
  • New len64Of_ok and loadCount_ok.

Copies removed

• Impl/Sha512/X86/Stream.lean: 143 → 51 lines (now just init plus params).
• Proof/Sha512/X86/Stream/Common.lean: 324 lines, deleted.
• Proof/Sha512/X86/Stream/Update.lean: 1038 → 46 lines.
• Proof/Sha512/X86/Stream/Finalize.lean: 1152 → 150 lines (the length field and digest of shape, and finalize_verified).
• Proof/Pbkdf2/Md/X86/Hashes.lean: its own SHA-512 digest proof (out512_ok and its step) is gone. It now gets OutOk from the family's shape, as it already did for MD5 and SHA-1.
• Totals: Lean +835 / −3187. Whole PR, including the regenerated src/asm: +1252 / −3540.

Proof/Sha256/X86/Stream/{Finalize,Common}.lean stay. On main (with #583 merged) they are still imported by Proof/Sha256/X86/Shared.lean, Proof/Scrypt/X86/Salsa.lean, Proof/Sha512/X86/Rounds.lean, Proof/Hmac/X86/Finalize.lean and Proof/Hmac/Generic/X86/Hash.lean.

Emitted code

Only the SHA-512 family's x86 files change:

• x86/sha512.rs: update and finalize are now the shared code.
• x86/hmac_sha{384,512,512_224,512_256}.rs and x86/pbkdf2_sha{384,512,512_224,512_256}.rs: only the digest writer changes. It is now the family's out64, which uses ecx where the old code used edx, with the same instruction count.

All other src/asm files are byte-for-byte identical, including MD5, SHA-1, SHA-224, SHA-256 and the SHA-NI variants.

Instructions per call, i686, counted by valgrind/callgrind, including the compression function:

	main	this PR
update, 0 B	18	39
update, 64 B	542	424
update, 1 KiB	129,043	120,588 (−6.6%)
update, 16 KiB	2,064,403	1,928,148 (−6.6%)
finalize	15,865	15,870

update now compresses whole blocks directly from the input instead of copying every byte through the buffer.

Proof cost

Hardware counters are unavailable in the VM I used (perf stat -e instructions:u reports <not supported>), so these are single-threaded wall-clock times (-j1 -DElab.async=false, best of 2, idle machine, same toolchain):

module	main	this PR
MdStream/X86/Common	4.0 s	4.9 s
MdStream/X86/Finalize	17.5 s	17.5 s
MdStream/X86/Words	4.2 s	4.2 s
Md5/X86/Stream/Md	2.6 s	2.5 s
Sha1/X86/Stream/Md	3.6 s	3.4 s
Sha256/X86/Shared	8.5 s	8.4 s
Variants/Sha256/X86/ShaNi	5.7 s	5.5 s
Sha512/X86/Stream/* (Common + Update + Finalize)	22.0 s	20.2 s
Sha512/X86/Shared	3.2 s	3.1 s
total	71.2 s	69.8 s

No heartbeat or other resource limits are set.

Validation (run locally)

• Lean:
  • Full lake build after merging main.
  • lake env lean --run Emit.lean --check: the axiom, compiler-override and Spec-origin audits all pass.
  • src/asm diffed against main; the diff is as described above.
• CI scripts: check_lean_imports, check_lean_speed, check_vectors, check_arch_gates, check_variants, check_mcdt and algorithms_table all pass. The README tables are unchanged.
• Rust:
  • cargo fmt --check and cargo clippy --all-targets -- -D warnings on the host.
  • cargo test with Wycheproof on the host (254 passed) and on i686-unknown-linux-musl (238 passed).
• Not run locally: ARM and AArch64 Rust tests, and coverage. This PR does not touch their code.

🤖 Generated with Claude Code

https://claude.ai/code/session_01167c4d5NdJ5cbpxrYD2uEs

---

Generated by Claude Code