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

[alex]

Summary

SHA-384, SHA-512, SHA-512/224 and SHA-512/256 streaming (update and finalize, scalar and _sha3) on AArch64 now go through the shared Merkle–Damgård streaming code (Impl/MdStream/AArch64.lean and Proof/MdStream/AArch64/). That code already served MD5, SHA-1, SHA-224 and SHA-256. This PR deletes SHA-512's own streaming code and proofs.

It does the same as #600 did for x86-64. The proofs come out of a review for duplicated code, where each duplicate points to a missing abstraction. Here the missing abstraction was a block size and length-field size in the shared streaming code, which only knew 64-byte blocks with a 64-bit length.

The eight-bytes-at-a-time copy and zero-padding loops that #595 (merged) wrote for SHA-512 alone now live in the shared code. MD5, SHA-1 and SHA-256 get them too.

The abstraction

Impl.MdStream.AArch64.Params gains:

• B: the block size, 64 or 128 bytes.
• L: the length-field size, 8 or 16 bytes.

The code is generic over both:

• the buffer is at N + B and the length field at N + B - L;
• the block count is len >> lg B and the partial-block length is len & (B - 1);
• the padding ends at B - L;
• len128 writes SHA-512's 128-bit big-endian bit length;
• out64 writes the 64-bit big-endian state words.

The generic proofs (Proof/MdStream/AArch64/{Common,Update,Finalize,Words}) are proved once for any Md B N L with Dims (B ∈ {64, 128}, 0 < L ≤ 16).

The copy and zero loops are #595's. A word loop runs x13 = x11 >> 3 times, storing with storeWord, and a byte loop handles the rest. Their proofs (copy_word_step / copy_words_ok / copy_ok, zero_word_step / zero_words_ok / zero_ok) follow #595's, generalised over P.

SHA-512 is one instance: Impl/Sha512/AArch64/Stream.lean (params, updateWith, finalizeWith) and Proof/Sha512/AArch64/Stream/Md.lean (its Md, Dims and Shape, about 80 lines). Proof/Sha512/AArch64/Variant.lean derives update and finalize and their Verified, register and depth facts for any compression variant. The _sha3 variant therefore needs nothing of its own (Sha3/Stream.lean and Sha3/StreamLit.lean are deleted), and ci/check_variants.py passes.

The SHA-512 functions now call vg_sha512_compress* the way MD5, SHA-1 and SHA-256 call theirs, instead of inlining the whole compression function. The shared code saves x30 in a 16-byte frame, so the callers changed:

• Ed25519 (AArch64): the whole-function framework (Proof/Ed25519/AArch64/Whole/) admits callees with one frame below the locals:
  • CK E, call_okF, CallReady.wpF, and wrap_ok for depth ≤ 1;
  • vg_ed25519_{public_key,sign_cached,verify_message} document 352 bytes of stack instead of 336.
• PBKDF2 (AArch64): Impl/Pbkdf2/AArch64.lean takes out64 and len128 from the shared code, and Proof/Pbkdf2/AArch64/Sha512.lean (moved into Proof/MdStream/AArch64/Words.lean) is deleted.
• HMAC: unchanged; it builds on the same update and finalize.

Interaction with #611

#611 (merged) gave the AArch64 compression function 640 bytes of scratch. Everything update and finalize reserve for the compression function now comes from one definition, Impl.Sha512.AArch64.scratchBytes (640):

• the streaming code's scratch offset params.so;
• the compressAArch64, updateAArch64 and finalizeAArch64 contracts (scratchBytes, scratchBytes + 48);
• the widening lemmas in Shared.lean;
• PBKDF2's Wb.

A later change to the compression function's scratch changes that one number on the streaming side. #611's edits to the deleted Proof/Sha512/AArch64/Stream/* have no counterpart here.

Copies removed

file	lines
Proof/Sha512/AArch64/Stream/Update.lean	871
Proof/Sha512/AArch64/Stream/Finalize.lean	847
Proof/Sha512/AArch64/Stream/Common.lean	433
Proof/Pbkdf2/AArch64/Sha512.lean	128
Impl/Sha512/AArch64/Stream.lean (bespoke code)	−142 / +32
Impl/Sha512/AArch64/Sha3/Stream.lean, Proof/Sha512/AArch64/Sha3/StreamLit.lean	16
Impl/Pbkdf2/AArch64.lean (out64, len128, sha512)	−18 / +3

Against main:

• Lean: +1,453 / −3,131.
• With src/asm/: +2,288 / −13,756. src/asm/aarch64/sha512.rs loses 10.4k lines because update and finalize are about 150 lines each instead of 1.2k–3.6k with the compression function inlined.

Performance

Code

Instructions executed under qemu-aarch64 -cpu max (-one-insn-per-tb -d exec) for one update of n bytes after init, then finalize. The baseline is main as of #611, which includes #595 and #610. Every digest is identical.

function	n	update main → PR	finalize main → PR
md5	3	72 → 76	12460 → 12259
md5	55	436 → 153	12199 → 12201
md5	100	1032 → 845	12257 → 12192
md5	1000	10986 → 10750	12313 → 12282
md5	16384	181557 → 181557	12437 → 12236
sha1	3	72 → 76	15643 → 15448
sha1	55	436 → 159	15420 → 15422
sha1	100	1830 → 1647	15478 → 15415
sha1	1000	22956 → 22725	15496 → 15466
sha1	16384	385845 → 385845	15620 → 15425
sha1_sha2	3	72 → 76	14330 → 14135
sha1_sha2	55	436 → 159	14107 → 14109
sha1_sha2	100	517 → 334	14165 → 14102
sha1_sha2	1000	3261 → 3030	14183 → 14153
sha1_sha2	16384	49717 → 49717	14307 → 14112
sha256	3	72 → 76	23991 → 23790
sha256	55	436 → 153	23622 → 23624
sha256	100	2934 → 2747	23794 → 23729
sha256	1000	39516 → 39280	23812 → 23781
sha256	16384	668469 → 668469	23974 → 23773
sha256_sha2	3	72 → 76	21679 → 21478
sha256_sha2	55	436 → 153	21310 → 21312
sha256_sha2	100	622 → 435	21482 → 21417
sha256_sha2	1000	4836 → 4600	21500 → 21469
sha256_sha2	16384	76597 → 76597	21662 → 21461
sha512	3	74 → 76	43632 → 43636
sha512	55	151 → 153	43765 → 43769
sha512	100	178 → 180	43593 → 43597
sha512	1000	24601 → 24504	43644 → 43648
sha512	16384	447007 → 444853	43723 → 43727
sha512_sha3	3	74 → 76	41089 → 41093
sha512_sha3	55	151 → 153	41222 → 41226
sha512_sha3	100	178 → 180	41050 → 41054
sha512_sha3	1000	6800 → 6673	41101 → 41105
sha512_sha3	16384	121503 → 118714	41180 → 41184

What changed:

• MD5, SHA-1 and SHA-256: buffering a partial block copies eight bytes at a time; up to 283 instructions fewer.
• MD5, SHA-1 and SHA-256 padding: zeroed eight bytes at a time; about 200 instructions fewer per finalize.
• SHA-512 small inputs: cost 2–4 instructions more, for the x30 frame.
• SHA-512 16 KiB: 0.5% fewer instructions with the scalar compression and 2.3% fewer with _sha3.
• Whole messages: 16 KiB through MD5, SHA-1 and SHA-256 is unchanged.

Proofs

Heartbeats from Lean's profiler (-Dtrace.profiler.useHeartbeats=true, the CLAUDE.md recipe; perf is unavailable on this VM) for every module this PR touches or that depends on it. Each module was measured on its own, on the same machine, and the elaboration and kernel totals are reported separately. The baseline is main with #595, and the PR column is this branch before it merged #610–#612; those PRs change the compression function, not these streaming proofs.

module	elab main+#595	elab this PR	kernel main+#595	kernel this PR
MdStream.AArch64.Common	28.4M	38.0M	2.8M	3.7M
MdStream.AArch64.Update	58.0M	68.2M	11.1M	13.0M
MdStream.AArch64.Finalize	41.5M	53.1M	5.4M	9.9M
MdStream.AArch64.Words	11.9M	17.7M	1.4M	2.0M
Md5.AArch64.Stream.Md	7.3M	7.8M	5.5M	5.6M
Sha1.AArch64.Stream.Md	5.0M	5.5M	2.9M	3.0M
Sha256.AArch64.Stream.Md	7.1M	7.5M	4.6M	4.7M
Sha1.AArch64.ScalarBackend	34.8M	35.0M	33.7M	33.8M
Sha1.AArch64.Sha2Backend	3.7M	3.9M	2.6M	2.7M
Sha256.AArch64.ScalarBackend	48.6M	48.7M	47.4M	47.5M
Sha256.AArch64.Sha2Backend	5.1M	5.2M	3.9M	4.0M
Sha256.AArch64.Variant	1.0M	1.4M	0.1M	0.1M
Sha512.AArch64.Variant	0.5M	1.9M	0.0M	0.1M
Sha512.AArch64.ScalarBackend	8.3M	7.0M	7.0M	5.8M
Sha512.AArch64.Sha3Backend	5.1M	4.2M	3.8M	3.0M
Sha512.AArch64.Shared	10.5M	11.3M	0.5M	0.5M
Sha512.AArch64.Lit	9.1M	3.0M	7.8M	2.6M
Pbkdf2.Md.AArch64.Hashes.Sha512	69.7M	68.3M	9.7M	9.7M
Pbkdf2.Md.AArch64.Hashes.Sha256	18.5M	18.4M	2.0M	2.0M
Pbkdf2.AArch64.Iterate	99.3M	98.6M	23.7M	23.6M
Ed25519.AArch64.Whole.Hash	2.0M	1.7M	0.1M	0.0M
Ed25519.AArch64.Whole.Layout	1.4M	2.8M	0.0M	0.2M
Ed25519.AArch64.Whole.Wrap	9.3M	10.4M	0.3M	0.5M
Ed25519.AArch64.PublicKey.CT	20.1M	20.1M	0.5M	0.5M
Ed25519.AArch64.SignCached.Entry	3.6M	4.0M	0.3M	0.3M
Sha512.AArch64.Stream.Common	18.4M	—	1.2M	—
Sha512.AArch64.Stream.Update	73.4M	—	16.3M	—
Sha512.AArch64.Stream.Finalize	62.4M	—	10.5M	—
Sha512.AArch64.Sha3.StreamLit	3.6M	—	3.0M	—
Pbkdf2.AArch64.Sha512	7.1M	—	1.0M	—
Sha512.AArch64.Stream.Md	—	2.4M	—	0.2M
total	675M	546M	209M	179M

Overall, elaboration drops by 19% and the kernel by 14%. The shared modules grow, since they now cover two block sizes and the word loops. The four SHA-512 stream modules they replace cost more than that growth. Sha512.AArch64.Lit no longer materializes the stream code. The SHA-512 backends check their register facts through instrs_keeps (by lit_decide) on the compression literal, which avoids re-evaluating the whole stream function in the kernel. Every declaration stays within the default maxHeartbeats, and ci/check_lean_speed.py passes.

Validation

At the latest merge of main (including #598, #605, #606, #610, #611, #612, #615 and #616):

• cd lean && lake build (every job), lake env lean --run Emit.lean, then --check (axiom and compiler audits, and every VG.Spec definition in Spec/).
• The diff in src/asm/ is in aarch64/{md5,sha1,sha256,sha512,ed25519}.rs only (the Ed25519 change is only its stack documentation).
• python3 ci/check_lean_imports.py, check_lean_speed.py, check_vectors.py, check_arch_gates.py, check_variants.py and check_mcdt.py all pass. ci/algorithms_table.py leaves README.md unchanged.
• cargo fmt --check; cargo clippy --all-targets -- -D warnings on x86-64 and --target aarch64-unknown-linux-gnu.
• cargo test with Wycheproof:
  • 258 pass on x86-64.
  • On AArch64 under qemu-aarch64, 246 pass with -cpu max and 247 with VG_CPU_FEATURES=none --features cpu-features-env.
  • These cover HMAC and PBKDF2 over SHA-384/512 and Ed25519.

Trusted code

There are no changes to Spec/ or TCB/. The per-target contracts in Proof/Sha512/AArch64/Compress.lean (updateAArch64, finalizeAArch64, which are Proof/) gain the stack conditions of the shared contracts. They are widened to Spec.Sha512.updateContract AArch64.abi 16 (and the same for finalize) in Shared.lean.

🤖 Generated with Claude Code

https://claude.ai/code/session_01RWYqd9UNiJ8dEEq3JQhyCf