SHA-224 on x86-64, x86, AArch64 and ARMv7: vg_sha224_init and the Rust API

[alex]

Third of the SHA-224 PRs: the implementation. The vectors (#446) and the spec (#452) are merged, and main is merged into this branch. It changes no files under Spec/ or TCB/.

SHA-224 only needs an init of its own. vg_sha224_init stores SHA-224's initial hash value, and SHA-256's update and finalize do the rest (as of #452, their contracts hold for any initial hash value). Every existing implementation of those is reused: SHA-NI and AVX2 on x86-64, and the SHA2 extension on AArch64.

Lean

• Impl: on each target, init becomes initWith iv, with init := initWith H0 and init224 := initWith H0_224. The emitted vg_sha256_init is byte-identical; the only change to src/asm/ is the new vg_sha224_init, one per target.
• Proofs: each target's init proof now holds for any iv.
  • The x86-64 proof needed one new lemma (setWidth 32 (setWidth 64 x) = x); on the other targets the proof was already written over word x off.
  • Some checks can only be evaluated by the kernel on literal code: the taint analysis on every target, and on x86-64 that the code never loads MXCSR. These are passed in as hypotheses and discharged for each of the two instances.
  • The per-target init contracts take iv.
• Registration: new files Artifacts/Sha224/{X86_64,X86,AArch64,Arm}.lean, each made from Spec.Sha256.init224Api.
• Test: VerifiedGarbageTest/Sha224.lean checks Spec.Sha256.sha224 against two of the CAVP short-message vectors at build time, like the SHA-256 test. I checked that it fails if one word of H0_224 is wrong.

Rust

• hashes::sha224::Sha224: a new module with its own #[cfg], built with streaming_hash! and its own Sha224Backend.
  • The backend has SHA-256's variants and dispatches to SHA-256's update and finalize.
  • Its select test checks, for every feature set, that it picks the same implementation as Sha256Backend (matching exhaustively).
  • There are also unit tests for incremental updates and HashFunction.
• tests/cavp/sha224.rs: all 65 short and 64 long messages, plus the Monte Carlo test.
• bench/benches/primitives/sha224.rs: compared against OpenSSL's SHA-224; USES is sha224 and sha256.
• The README table is regenerated: SHA-224 is ✅ on all four architectures, with the same CPU-feature notes as SHA-256.

Checks run locally (after merging main)

• lake build (5648 jobs) and lake env lean --run Emit.lean --check
• ci/check_lean_imports.py, check_lean_speed.py, check_vectors.py, check_arch_gates.py, check_variants.py, check_mcdt.py, algorithms_table.py --check
• cargo fmt --check and cargo clippy --all-targets -- -D warnings, on x86-64 and for the i686, aarch64 and armv7 targets
• cargo test on x86-64. Before this merge I also ran it with VG_CPU_FEATURES=avx,avx2,bmi1,bmi2 and with VG_CPU_FEATURES=none; after it, the full suite and the SHA-224 vectors pass.
• cargo check --benches in bench/ (before this merge)

I couldn't run the Rust tests on the other architectures locally; CI covers them.

🤖 Generated with Claude Code

https://claude.ai/code/session_01HDRg9k22FbCYq3TnciKvwG

[alex]

Two CI failures on 43c4fc2 are not from this PR: rust (ubuntu-24.04-arm, …cryptography-runner-ubuntu-rolling:armv7l…) and Rust (Thumb, stable).

Both died in setup, before any build or test ran. rustup toolchain install stable inside the armv7l container fails while upgrading to the 1.99.0 stable published today:

info: latest update on 2026-10-01 for version 1.99.0 (b940084d7 2026-09-28)
info: removing previous version of component cargo
error: failure removing component 'cargo-armv7-unknown-linux-gnueabihf', directory does not exist: 'share/man/man1/cargo.1'

An armv7l container job in the unrelated #453 failed at the same time. I don't know of a fix yet; it is in the runner image's preinstalled toolchain, not in this repository. I'll re-run the failed jobs once when the run finishes.

---

Generated by Claude Code