feat(stdlib): SHA-256 as a standard-library member (SL-02, stage 1 of #126)

[humuhumu33]

Stage 1 of #126 (plan item L5.1 of #106, under #27's rule that no handwritten code carries normative semantics), in #92's lane of more standard-library members: SHA-256 as a certified member of the standard library, with its evidence. Stage 2, switching every identity of SPEC §8 and §21 from the sha2 crate to this module, is a later PR; the measurement it needs is below.

Refs #126. Refs #92.

The branch contains main at 8765feea (through #155 and #166), merged with a merge commit. The register is 405 (main's 404 and SL-02), set by hand in README, SPEC §31, repository.rs, and xtask/src/spec_links.rs.

What this adds

• stdlib/src/Sha256.lex.tex: FIPS 180-4 SHA-256 in the authoring notation, over the closed language-1.2 primitives and nothing else. Two production roots for rust-std, each admitting exactly the effects its closure realizes (allocation, overflow, recursion):

  root	shape
  sha256 (message : Bytes) : Digest	the record of the eight UInt32 words
  sha256Hex (message : Bytes) : Bytes	the lowercase hexadecimal digest

  The FIPS 180-4 example digests (abc, the two-block message, the empty message) are stated in the module as theorems by reflexivity on the Digest record, which the kernel replays under verify.

  How it is said, since [v0.4] #27 stage 8: the production compiler authored in .lex.tex and compiled by LexLean to production software #92's spike predicted "expressible today over UInt32 bit ops and iterate" and three things were missing on the way:

  • addition modulo 2^32: no primitive wraps, so add is checked_add of the operands widened to UInt64 by checked_convert, narrowed by bit_and and checked_convert (the none arms are unreachable and would fail every vector);
  • rotation: two shifts (each an Option) and bit_or;
  • padding and the length: checked_convert refuses a Nat input and nothing turns a fixed-width value into Bytes, so the message is never padded as bytes. Every word of every block is read by position (index below the length, 0x80 at it, zero beyond), the two length words come from quotient and remainder of the bit length through a 32-step iterate over its bits (wordOfNat), and each hexadecimal digit is chosen from its nibble by bit_and and equal tests. feat(semantic-ir): byte and fixed-width widening conversions in language 1.2 (SM-32, #114) #151 (to_nat, [0.5.0] Byte-to-fixed-width conversion in the language-1.2 surface #114) would shorten wordOfNat and byteAt; this PR does not depend on it.

  The schedule is a sixteen-word window advanced each round and the sixty-four rounds are iterate over a record of the working variables, the window, and the round number; the round constant is a balanced search on that number (depth 6) and each hex nibble a balanced test of its four bits.

• SL-02 (one scenario, one conformance_sl_02, in crates/conformance/src/cases/stdlib_sha256.rs):

  • both roots eligible for rust-std with exactly their declared effects;
  • the lowered program under the calculus evaluator and the rendered rust-std package under the pinned rustc compute the FIPS 180-4 examples, every vector of the NIST CAVP SHA256ShortMsg.rsp (65) and SHA256LongMsg.rsp (64) files, committed verbatim under tests/stdlib/sha256/ with their provenance, and agree with the sha2 crate on a seeded corpus: every length 0..200 (so 55, 56, 63, 64, 119, 120 and their neighbours), then random lengths to 4 KiB, and the million-a example under rustc. The two oracles are checked against each other before either judges the module, and a disagreement fails closed: it is a defect, never resolved by adopting an oracle's digest;
  • the gate is armed on every run: one bit of the round function is flipped in a copy of the module (a := (add t1 t2) exclusive-or 1) and the first FIPS vector disagrees;
  • under the pinned Lean, the production export (lexlean production build, §24.7) certifies both roots (certificates A, B, E) into rust-std packages byte-identical to the committed ones under tests/production-export/stdlib/packages/, each realizing the program the differential ran.

• SPEC §17.22 gains the module and its oracles; §7 lists tests/stdlib/; CHANGELOG, README, CONFORMANCE.md regenerated; the VERIFICATION.md record of the planted bit.

• Regenerated for the new module only: stdlib/lexlean.lock, stdlib/expected/{build,verify}, tests/production-export/stdlib/packages/. bootstrap/lexlean.lock and bootstrap/expected/build follow, since bootstrap/ pins the standard library's tree as a source package (feat(packages): source packages, a project imports the modules of a locked package (PK-01..PK-04) #162); its verify records and packages are unchanged.

Three findings on the way

1. The package reader's nesting bound. The round constant and the hex nibble were first written linearly (a 64-element constant list, a 16-way if chain) and the rendered package was refused (package manifest is not canonical JSON: recursion limit exceeded): the reader parses the program's canonical JSON under serde_json's 128-level limit, and a 64-deep cons is past it. The module stays inside it with balanced lookups; the bound is worth a line in §17.16 or a register row of its own, and this PR does not change calculus/rust/.
2. Certificate A and a fallible callee in a nested else. Certificate A refused sha256 while wordAt (whose argument positions are Nat additions) was called from the innermost else of scheduleWord; moving the additions to the caller (wordAt takes the four bytes) is accepted. A two-function reduction did not reproduce it, so it is not filed yet; it belongs to the [v0.4] #27 stage 5: certificates A, B, E and the audit modules as typed data, with no Lean text template in the production compiler #89 lane.
3. roundConstant has no axioms. A balanced <? search over Nat literals closes with no axioms at all, so its exact policy is [], not the Quot.sound, propext its siblings carry (LLV7005 until it was aligned).

Measurement for stage 2

Measured on this branch's committed sha256_hex package (the production export for rust-std, built --release with the pinned rustc 1.97.1) against sha2 0.10, one thread on an AMD Ryzen AI Max 390 under WSL, nothing else running; seeded messages, both sides producing the lowercase hex digest. Every one of the 2,572 digests of each run equals sha2's. Third of three runs (every time of the other two within 20% of it, most within 5%):

input bytes	messages	sha2 ms	LexLean ms	LexLean / sha2	LexLean MB/s
64	2,000	1.79	7.49	4.2x	17.1
1,024	500	0.64	7.24	11.3x	70.7
16,384	60	0.46	11.05	23.9x	89.0
262,144	8	0.89	24.67	27.6x	85.0
1,048,576	3	1.31	36.79	28.0x	85.5
16,777,216	1	6.96	241.81	34.7x	69.4

The module runs at 70 to 90 MB/s, 24 to 35 times slower than sha2 from 16 KiB up; sha2 uses the CPU's SHA extensions here (about 2.4 GB/s at 16 MiB). The small-input ratios flatter the module, since the sha2 side formats its hex with format! per byte. For stage 2 that is about 0.7 s for a 48 MB module's identity in place of about 20 ms. The 16 MiB message runs on a thread with a 4 GiB stack reservation, because iterate recurses once per block; how much of it is needed was not measured. The harness (seeded corpus, sha2 as reference) is not committed; it can go under tests/stdlib/sha256/ if wanted.

What it does not do

• It does not replace sha2 anywhere in the compiler (stage 2).
• No theorem states the CAVP vectors: a 6400-byte vector by rfl is kernel work out of proportion to its evidence; those are held by the differential.
• iterate is realized as a recursive function until production: the collection and iteration primitives are realized by self-recursive functions but registered recursion = false; a root overflows the stack at about 40k iterations #105 step 2, so a root over a 48 MB module is 750 000 blocks of stack depth; the harness runs on the 64 MiB thread the generated harness already uses. Stage 2 depends on production: the collection and iteration primitives are realized by self-recursive functions but registered recursion = false; a root overflows the stack at about 40k iterations #105 for the host stack as much as on the ratio.

Evidence

Local, WSL x86-64, Lean 4.32.1: cargo fmt --check, validate-model, validate-spec-links (405 rows), check-test-inventory, RP-07, RP-11, RP-13, RP-14, clippy with -D warnings on the suite, conformance_sl_01 (206 s) and conformance_sl_02 (305 s) with the production export under the pinned Lean, check-golden, and check-production-export (every exported project). Full just vv on CI.

Closes nothing; #126 stays open for stage 2.

🤖 Generated with Claude Code