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

[alex]

Summary

This came out of a review looking for duplication that points to missing abstractions. MD5, SHA-1 and SHA-256 already streamed through Impl/MdStream/<T> on every target, but SHA-512 did so only on x86-64. On ARMv7 the MdStream Params fixed a 64-byte block and an 8-byte length field, so the SHA-512 family had its own streaming code (Impl/Sha512/Arm/Stream.lean) and about 2,350 lines of its own streaming proofs.

This PR generalises ARMv7 MdStream over the block size and length-field size, as x86-64 already is. The SHA-512 family is then an instance of it, and the bespoke streaming code and proofs are deleted.

No changes to Spec/ or TCB/. The contracts are unchanged.

The abstraction

• Impl/MdStream/Arm.lean
  • Params gains B (block size) and L (length-field size).
  • The code uses B, B - 1, B - L, L - 1 and log₂ B where it used 64, 63, 56, 7 and 6.
  • out may write r9 and r10.
  • For B = 64, L = 8 the code is the same as before.
• Proof/MdStream/Arm/Common.lean
  • The contracts, Shape and CalleeOk are stated over Md P.B P.N P.L.
  • Dims gains B ∈ {64, 128}, 0 < L ≤ 16 and the encodability of the new immediates.
  • New lemmas: Dims.{pos, le, lg, mod, mod64, div_eq_zero}, shrB, cmp0_shrB, andB, ofNat_shlB, op2_shrB, op2_shlB.
• Proof/MdStream/Arm/{Update,Finalize}.lean
  • Both proofs now hold for any such B and L.
  • finalize names the end of the zero padding lim P k, so its single symbolic execution stays independent of k, as before.
• SHA-512 family on ARMv7
  • Impl/Sha512/Arm/Stream.lean keeps init and outW. It adds params: N = 64, B = 128, L = 16, scratch offset 224, a length field written using only r9, and the existing outW digest.
  • update and finalize are now the generic code.
  • Proof/Sha512/Arm/Stream/{Update,Finalize}.lean keep their module and theorem names (update_verified, finalize_verified, sat, wordBytes_split, writeW_rev, flat_length), so HMAC, PBKDF2 and Ed25519 still find them. They now instantiate the generic proofs:
    • dims and callee for the size parameters and the compression function;
    • shape, made of len_ok and out_ok;
    • constant time by taint_decide.
• Callers
  • MD5, SHA-1 and SHA-256 add B := 64, L := 8 to their params.
  • Their dims and shape proofs need one-line adjustments.
  • Ed25519's Whole/Hash.lean unfolds the generic definitions to prove noFrames.
  • Pbkdf2/Md/Arm/Words.lean's OutOk.ofShape takes Md P.B P.N P.L, a two-line change.

What is removed (line counts against main)

File	Before	After
Proof/Sha512/Arm/Stream/Update.lean	1162	41
Proof/Sha512/Arm/Stream/Finalize.lean	1083	222
Impl/Sha512/Arm/Stream.lean	143	59

The generic proofs grew by about 160 lines. Overall: 18 files changed, 757 insertions, 2667 deletions (net −1910).

Performance

Emitted code

lake env lean --run Emit.lean changes only src/asm/arm/sha512.rs.

• MD5, SHA-1, SHA-224 and SHA-256 on ARMv7 are byte-for-byte unchanged, as are all other targets and all other ARMv7 files: HMAC, PBKDF2 and Ed25519 call vg_sha512_* by symbol.
• The SHA-512 family's update now compresses whole blocks straight from the data. The old code copied every byte through the buffer.

Instructions executed on ARMv7

These are SHA-512 init + update + finalize on ARMv7, counted under qemu-arm -one-insn-per-tb -d exec. Each figure is the difference between 20 and 10 iterations of the hash, divided by 10.

Message, chunks	Before	After
0 bytes	10,544	10,542
111 bytes, one update	11,271	11,277
112 bytes, one update (two-block padding)	20,820	20,826
128 bytes, one update	20,834	19,940
1 KiB, one update	89,434	82,009 (−8%)
1 KiB, 64-byte updates	96,944	97,070
1 KiB, 1-byte updates	606,992	613,166 (+1%)
16 KiB, one update	1,265,434	1,146,049 (−9%)

The benchmarks (hash_group) hash each message in one call, which is the same or faster at every size. Feeding many tiny updates costs about 6 instructions more per call.

Proof checking

These are -Dprofiler=true, -j1, Elab.async=false, best of 3 runs on the same idle machine, toolchain and revision. Each cell is elaboration + kernel, then kernel alone, in ms. Hardware counters weren't available in this VM, so perf stat couldn't be used.

Module	Before	After
Proof/MdStream/Arm/Common	2658 / 483	3292 / 724
Proof/MdStream/Arm/Update	7541 / 2660	6550 / 2170
Proof/MdStream/Arm/Finalize	6798 / 1580	6609 / 1770
Proof/Sha512/Arm/Stream/Update	9081 / 2880	3018 / 2580
Proof/Sha512/Arm/Stream/Finalize	7856 / 1740	4232 / 2720
Proof/Sha512/Arm/Lit	1408 / 1080	1449 / 1130
Proof/Sha512/Arm/Shared	1656 / 218	1546 / 190
Proof/Sha256/Arm/Stream/Md	1884 / 1420	1994 / 1510
Proof/Md5/Arm/Stream/Md	1449 / 1120	1485 / 1160
Proof/Sha1/Arm/Stream/Md	2042 / 1580	1847 / 1430
Total	52,373 / 14,761	34,022 / 15,384

• Elaboration + kernel together drop by 35%.
• Kernel time alone rises 4% (+0.6 s), which is against this refactor's "no slower" requirement. Most of it is SHA-512 finalize's constant-time proof. That proof is now the standard taint_decide over the code, which includes the compression function. The deleted proof was a hand-written relational one.
• Common's kernel time also rises (+0.24 s), from the Dims lemmas.

Validation run locally

• Lean
  • A full lake build, both before and after merging the latest main (which brought in HMAC-SHA-256 and PBKDF2-HMAC-SHA-256 on ARMv7 and x86: the generic contracts and code #583 and HMAC init on ARMv7 and x86: compress the padded key blocks directly #586).
  • lake env lean --run Emit.lean --check: passes. The audits pass, and the committed src/asm/ is what the emitter generates.
• CI scripts: check_lean_imports.py, check_lean_speed.py, check_vectors.py, check_arch_gates.py, check_variants.py, check_mcdt.py and algorithms_table.py (the README tables are unchanged).
• Rust: cargo fmt --check and cargo clippy --all-targets -- -D warnings on x86-64.
• ARMv7 tests: WYCHEPROOF_ROOT=… cargo test --target armv7-unknown-linux-gnueabihf under qemu-user, after the merge. All pass, including SHA-512's incremental tests and the Wycheproof tests.
• Not run locally:
  • The x86-64 cargo test. No x86-64 code changed.
  • The coverage merge.
  • Benchmarks on real ARMv7 hardware.

Follow-up

Proof/Pbkdf2/Md/Arm/Sha512.lean proves the same digest code (outW) that the new Proof.Sha512.Arm.Stream.Finalize.out_ok proves. It can now become OutOk.ofShape Proof.Sha512.Arm.Stream.Finalize.shape. I left it alone here because the PBKDF2 code was being changed in parallel.

🤖 Generated with Claude Code

https://claude.ai/code/session_019oSrQeJdKT2MeBHirxaPKi

---

Generated by Claude Code

[alex]

merge conflict

[alex]

merge conflict