Spec: SHA-224, and SHA-256's update and finalize for any initial hash value

[alex]

Second of the SHA-224 PRs: the spec. (Vectors: #446. The implementation of vg_sha224_init and the Rust API follow in their own PR once this one is merged.)

FIPS 180-4's SHA-224 is SHA-256 started from a different initial hash value (§5.3.2) and truncated to 28 bytes (§6.3). This follows the SHA-512 family's design: SHA-224 shares SHA-256's streaming state and vg_sha256_update/vg_sha256_finalize, and only gets its own init.

Trust changes (Spec/), for review

Spec/Sha256.lean

• H0_224: transcribed from §5.3.2. As a cross-check, these words are the low halves of SHA-384's H0_384, as the standard derives them.
• finalHash iv m: the 32-byte H⁽ᴺ⁾ of m starting from iv. This is the old body of hash, with H0 turned into a parameter.
• hash m := finalHash H0 m (unchanged in meaning) and sha224 m := (finalHash H0_224 m).take 28.
• ReprFrom iv: the old body of Repr, with H0 turned into a parameter. Repr := ReprFrom H0, so Repr means what it did before, and the HMAC-SHA-256 and PBKDF2 contracts that use Repr and hash don't change.

Spec/Sha256/Contract.lean

• updateContract: now ∀ iv msg, ReprFrom iv m state msg → … → ReprFrom iv m' state (msg ++ …). This is a strictly stronger postcondition: iv := H0 gives back the old one.
• finalizeContract: now ∀ iv msg, ReprFrom iv … → … → bytesAt m' out 32 = finalHash iv msg. This is also strictly stronger, since finalHash H0 = hash. Unlike SHA-512's contract, it needs no extra length hypothesis: the 64-bit length field is determined by count modulo 2⁶⁴, as before.
• New init224Contract/init224Api (vg_sha224_init, module sha256, with vg_sha256_init's signature initSig): the state represents [] from H0_224.
• The update and finalize summaries now mention SHA-224 and say what finalize writes. The regenerated src/asm/*/sha256.rs differ only in those doc comments.

Proofs (untrusted)

No implementation changes. On every target, update and finalize are the generic Merkle–Damgård code, and its proofs (Proof/MdStream/) already hold for any IV; they were only being specialized to H0. So:

• the per-target contracts (Proof/Sha256/*/Contract.lean) now quantify over iv as well, and the glue that moves the generic proofs to them passes iv through instead of H0. That glue is in the Md/Variant/Shared files, including x86's Stream/Variant.lean, which Make x86 SHA-256 constructions generic over compression backends #460 added and which reached this PR when I merged main.
• the two places that consumed the H0-only per-target contracts now instantiate iv := H0: Proof/Hmac/Arm/Finalize.lean and Proof/Pbkdf2/Md/AArch64/Hashes/Sha256.lean (the latter mirrors what the SHA-512 instance already does);
• Proof/Sha256/Stream.lean unfolds the new definitions in two places.

docs/algorithms/sha224.toml adds the README row (spec landed, no architecture yet), and the table is regenerated.

Checks run locally (after merging main)

• lake build (all 5623 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, cargo clippy --all-targets -- -D warnings, cargo test (x86-64)

🤖 Generated with Claude Code

https://claude.ai/code/session_01HDRg9k22FbCYq3TnciKvwG

[alex]

This PR was dequeued because the merge-group run failed two jobs: Rust (Thumb, stable) and rust (ubuntu-24.04-arm, …cryptography-runner-ubuntu-rolling:armv7l…). Neither failure is from this PR, whose own CI is green.

Both died in Install Rust, before anything was built. Inside the armv7l container, rustup toolchain install stable fails while upgrading to today's 1.99.0:

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'

The image's preinstalled stable is missing a file that rustup expects to remove, so every PR's armv7l jobs fail the same way (the unrelated #453 too). No fix exists yet. A newer image may fix it; otherwise, a possible workaround in ci.yml is to drop the image's toolchain before installing (untested; I can't run the armv7l image here):

      - name: Install Rust
        run: |
          rustup toolchain uninstall ${{ matrix.rust }} || true
          rustup toolchain install ${{ matrix.rust }} --profile minimal --component clippy,rustfmt,llvm-tools

The same change would go in the Thumb job and in bench.yml's arm job. Once the armv7l jobs pass, this PR needs to be re-queued.

---

Generated by Claude Code