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

CHANGELOG.md

@@ -15,6 +15,22 @@ versions, and the entries below say what each tag does and does not claim.
 
 ## Unreleased
 
+- The standard library's SHA-256 (SPEC.md §17.22, `SL-02`, #126 stage 1; no
+  new diagnostic code). `stdlib/src/Sha256.lex.tex` states FIPS 180-4 SHA-256
+  over the closed language-1.2 primitives (`UInt32` bit operations, widening
+  to `UInt64` for modular addition, `iterate` for the rounds and the blocks)
+  with the production roots `sha256 : Bytes -> Digest` and
+  `sha256Hex : Bytes -> Bytes` for `rust-std`, and states the FIPS 180-4
+  example digests as theorems by reflexivity. `SL-02` runs both roots' lowered
+  programs under the calculus evaluator and their rendered packages under the
+  pinned rustc on the FIPS 180-4 examples, every NIST CAVP SHA-256 short- and
+  long-message vector (`tests/stdlib/sha256/`), and a seeded corpus against
+  the `sha2` crate, detects a planted one-bit error in the round function,
+  and, under the pinned Lean, compares the certified packages the production
+  export publishes with the committed ones. The compiler's identities are
+  still computed by `sha2`; replacing it is stage 2 of #126. The register has
+  405 IDs.
+
 - CI cost, #131 (SPEC.md §8.3, §9.4, `RP-14`): `ci.yml` begins with a `plan`
   job (`.github/ci-plan.sh`) that decides what a run is from the event alone.
   A draft pull request runs the `rest` leg and no other job (about 23 runner

CONFORMANCE.md

@@ -543,6 +543,7 @@ the error registry does not sanction (R5, `ERRORS.md`).
 | ID | Level | Statement |
 | --- | --- | --- |
 | `SL-01` | `build` | The standard library's `Text` module is language-1.2 source whose seven members over `Bytes` (`startsWith`, `endsWith`, `trim`, `lines`, `splitOn`, `joinWith`, `find`) are production roots eligible for `rust-std` with exactly their declared effects; each member's lowered program under the calculus evaluator and its rendered `rust-std` package under the pinned rustc agree with Rust's `starts_with`, `ends_with`, `trim_ascii`, `lines`, `split`, `join`, and `find` on a seeded corpus; a planted defect in a member is detected; and the certified packages the production export publishes for it are the committed ones. |
+| `SL-02` | `build` | The standard library's `Sha256` module is language-1.2 source stating FIPS 180-4 SHA-256 over `UInt32` bit operations and `iterate` (modular addition by widening to `UInt64`, rotation as two shifts, padding read by position, the message schedule as a sixteen-word window, sixty-four rounds over the round-constant list), whose roots `sha256 : Bytes -> Digest` and `sha256Hex : Bytes -> Bytes` are production 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 example digests and every NIST CAVP SHA-256 short- and long-message vector, and agree with the `sha2` crate on a seeded corpus whose lengths cover every padding boundary, a disagreement failing closed and never resolved by adopting the oracle's digest; a planted one-bit error in the round function is detected; and the certified packages the production export publishes for the two roots are the committed ones. |
 
 ## tooling
 

README.md

@@ -142,7 +142,7 @@ just vv        # the complete normative acceptance gate (SPEC.md §9.2)
 just release   # vv, then the §30 release criterion; refused until 1.0.0
 ```
 
-All 404 registered conformance IDs are implemented and pass; `just vv` runs clean from a checkout with the pinned toolchain installed.
+All 405 registered conformance IDs are implemented and pass; `just vv` runs clean from a checkout with the pinned toolchain installed.
 
 The differential against the independent generator `lean4-prod` (SPEC.md §17.19, `OR-01`..`OR-08`) acquires it at its pinned commit: from the checkout `LEXLEAN_ORACLE_DIR` names, or by fetching the commit with `git` into the Cargo target directory (`LEXLEAN_ORACLE_CACHE` overrides), and builds it with the pinned Lean and Rust toolchains. It is validation evidence only and no input to any identity. An oracle that cannot be acquired, is not the pinned files, or fails is unavailable: that fails the gate on Linux x86-64 and is printed as `NOT VALIDATED` elsewhere, and is never reported as agreement.
 
@@ -182,7 +182,7 @@ Every row is validated by `just vv`; the IDs link the claim to its register row,
 | Language-1.2 compiler-tooling modules: a closed, typed program over a registry of the external Lean interface (types with exact constructors and index requirements, calls with exact signatures), with flat index-exhaustive matching, licensed partial and mutual recursion, complete recursive traversal, command registration, invocation and evaluation as semantic data, both backends from one linked value, and no member that holds Lean text | `TL-01`..`TL-11` | `build` |
 | The language-1.2 authoring notation: a readable `.lex.tex` text for a semantic module, in bijection with its canonical JSON, whose every position and variant is read from the schema, with readable forms for types and terms and a generic form for every other value, formatted canonically by `fmt` (which also writes a module out of its data form), linking to exactly the module its data form links to, failing closed, the only form in which a language-1.2 source of the product is written, the same for the compiler-tooling modules in the generic notation, with no compiler-semantics ID that depends on which form an embedded module is written in, with no product source owned by a generator but five named records, read and written by programs only through the authoring API (`lexlean::sdk`), and, for a native core module, a readable program over the shared table of kernel terms whose numbering is the order of its text | `AU-01`..`AU-12` | `build` |
 | The runtime of generated Lean as native modules: the portable, collection, model, and reasoning runtimes of language 1.2 are LexLean source that every generated module imports, migrated losslessly and audited against their exact axioms, the released runtime text of languages 1.0 and 1.1 is frozen data equal to their released output, and no other Lean runtime text remains in the compiler but the decoder of core module 2 | `RT-01`..`RT-04` | `build` |
-| The standard library: language-1.2 source beside the compiler whose members are certified production roots, each validated against Rust's standard library by a seeded differential of its evaluator and rustc realizations; bytes and text over `Bytes` | `SL-01` | `build` |
+| The standard library: language-1.2 source beside the compiler whose members are certified production roots, each validated against its oracle by a seeded differential of its evaluator and rustc realizations; bytes and text over `Bytes`; SHA-256 against FIPS 180-4, the NIST CAVP vectors, and the `sha2` crate | `SL-01`..`SL-02` | `build` |
 | The bootstrap project: the compiler's own components as language-1.2 source compiled by LexLean's production pipeline to certified Rust packages, the first being the exact axiom-output parser and its closed Lean-name check, each held to the Rust it replaces (the stage-0 oracle) by the committed golden vectors and a seeded differential of its evaluator and rustc realizations, with planted defects detected and the production export committed | `BS-01` | `build` |
 | Source packages: a language-1.2 project imports the modules of a locked, content-addressed package of its workspace: `[[source_package]]` and `lexlean-workspace.toml`, the pins in `lexlean.lock` recomputed by every command, imports closed at link, no re-export of a package's production roots, and the package's modules replayed by the importer's `verify` with their origin in the records | `PK-01`..`PK-05` | `build` |
 | The literal `nat-add-zero` example, the Lean-verified feature examples, and the complete negative fixture suite | `EX-01`..`EX-08` | `build` |

SPEC.md

@@ -491,6 +491,7 @@ The completed repository MUST have this layout. Additional files are allowed onl
 │   ├── oracle/
 │   ├── preservation-library/
 │   ├── production-export/
+│   ├── stdlib/
 │   └── tooling/
 ├── tooling/
 │   └── schemas/
@@ -6700,6 +6701,33 @@ realizes a library template, and no member recurses itself. Theorems over the
 members wait for equality of `Bytes` by evaluation; until then the module's
 behavior is held by the differential (`SL-01`).
 
+The second module, `Sha256`, is FIPS 180-4 SHA-256 (#126, stage 1), stated
+over the closed primitive vocabulary of §17.12 and nothing else: addition
+modulo 2^32 is `checked_add` of the two operands widened to `UInt64` by
+`checked_convert`, narrowed by `bit_and` and `checked_convert`; a rotation is
+two shifts and `bit_or`; 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 it, and the two length words from `quotient` and `remainder` of the
+bit length); the schedule is a sixteen-word window advanced each round; the
+sixty-four rounds are `iterate` over a record of the working variables, the
+window, and the round number, whose constant is a balanced search by `<?`;
+and the digest is the record `Digest` of eight `UInt32` or, for `sha256Hex`,
+its lowercase hexadecimal as `Bytes`, each nibble a balanced test of its bits
+by `bit_and` and `equal`. Both lookups are balanced rather than linear because
+a rendered package's program is canonical JSON read under a fixed nesting
+bound (§17.16), and a linear chain of sixty-four is past it. Its roots and oracles:
+
+| Member | Oracles |
+| --- | --- |
+| `sha256 (message : Bytes) : Digest` | the FIPS 180-4 example digests, as theorems in the module by reflexivity and under the differential |
+| `sha256Hex (message : Bytes) : Bytes` | the FIPS 180-4 example digests, every vector of the NIST CAVP `SHA256ShortMsg` and `SHA256LongMsg` files under `tests/stdlib/sha256/`, and the `sha2` crate on a seeded corpus whose lengths cover every padding boundary |
+
+A disagreement with an oracle fails the case (`SL-02`) and is a defect; it is
+never resolved by adopting the oracle's digest. The module is the first stage
+of #126: the compiler's own identities (§8, §21) are still computed by the
+`sha2` crate, and switching them to the module is the second stage, which
+waits on the measured cost of the rendered package against `sha2`.
+
 ### 17.23 The bootstrap project
 
 The bootstrap project, `bootstrap/` beside `compiler/` and `stdlib/`, holds the
@@ -9572,6 +9600,7 @@ Every row below is normative, has honesty level `build`, and MUST be copied byte
 | `RT-03` | `runtime` | A verification compiles every runtime module that a project's generated modules, or the calculus modules its certificates are checked against, import before the project's modules, replays it with `leanchecker`, and audits each of its declarations against the axioms its row pins; the committed verification of a project that uses the collections prints them, the runtime's own project verifies under the pinned Lean, and a row that pins another axiom set than its declaration observes fails with LLV7005. | §17.12, §22.3, §22.5, §22.6 |
 | `RT-04` | `runtime` | No Lean runtime text remains in the language-1.2 compiler: a generated language-1.2 module imports the runtime modules whose constants it names and declares nothing under a runtime namespace, and the only Lean runtime text in the compiler's source outside unit-test items, in one string literal or in several written together, is the decoder of core module 2, which loads native modules and so cannot be one; a runtime text planted in any of its shapes, raw or escaped, with or without a namespace line, split across literals, or after a test module, is found. | §17.12, §18.1 |
 | `SL-01` | `stdlib` | The standard library's `Text` module is language-1.2 source whose seven members over `Bytes` (`startsWith`, `endsWith`, `trim`, `lines`, `splitOn`, `joinWith`, `find`) are production roots eligible for `rust-std` with exactly their declared effects; each member's lowered program under the calculus evaluator and its rendered `rust-std` package under the pinned rustc agree with Rust's `starts_with`, `ends_with`, `trim_ascii`, `lines`, `split`, `join`, and `find` on a seeded corpus; a planted defect in a member is detected; and the certified packages the production export publishes for it are the committed ones. | §17.22 |
+| `SL-02` | `stdlib` | The standard library's `Sha256` module is language-1.2 source stating FIPS 180-4 SHA-256 over `UInt32` bit operations and `iterate` (modular addition by widening to `UInt64`, rotation as two shifts, padding read by position, the message schedule as a sixteen-word window, sixty-four rounds over the round-constant list), whose roots `sha256 : Bytes -> Digest` and `sha256Hex : Bytes -> Bytes` are production 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 example digests and every NIST CAVP SHA-256 short- and long-message vector, and agree with the `sha2` crate on a seeded corpus whose lengths cover every padding boundary, a disagreement failing closed and never resolved by adopting the oracle's digest; a planted one-bit error in the round function is detected; and the certified packages the production export publishes for the two roots are the committed ones. | §17.22 |
 | `BS-01` | `bootstrap` | The axiom-output parser of SPEC.md §22.5 is language-1.2 source in the `bootstrap/` project: `parseAuditOutput` and the closed Lean-name check `isClosedLeanName` are production roots eligible for `rust-std` with exactly their declared effects; the parser's lowered program under the calculus evaluator agrees with the Rust parser `verify::axiom` on the result, the rejection message, and the attributed declaration for every committed golden vector (accepted, accepted-wrapped, and rejected); both roots' rendered `rust-std` packages under the pinned rustc agree with the Rust oracle on a large seeded corpus of generated, wrapped, and mutated audit outputs with no disagreement; a planted defect in the source is detected; and the certified packages the production export publishes for the project are the committed ones. | §17.23, §22.5 |
 | `PK-01` | `packages` | A language-1.2 project that declares a source package by its identifier, version, kind `path`, and the member directory a `lexlean-workspace.toml` lists locks it by the tree digest of its manifest and source files, its manifest digest, its version, its module prefix, and its own packages, and the configuration and the lock read back to the bytes written; a project without a source package keeps its bytes, and a package of another kind, a source package in another language, a changed byte or version (LLC0105), an undeclared package (LLC0106), a module prefix claimed twice (LLC0107), a project or a package outside the workspace (LLC0108), a path that escapes it, and a symlink (LLS8001) are each refused with the named code. | §10.5, §11.1, §25.1 |
 | `PK-02` | `packages` | A module of a project imports only modules of its own project and modules of the packages the project declares, and a module of a package only modules of itself and of the packages its own manifest declares: a package module is a module of the importing project under its own module prefix, a module of a package the project does not declare fails with LLR3009, and an import cycle through a package fails with LLR3003. | §10.5, §15.1 |
@@ -9583,7 +9612,7 @@ Every row below is normative, has honesty level `build`, and MUST be copied byte
 | `LM-03` | `language-models` | Text that is not valid UTF-8 is refused and never tokenized: an artifact whose bytes do not decode under the `utf8_lines` schema — invalid UTF-8, a CR, or a missing final LF — fails by its artifact rules before any byte is decoded, and a text offered to `encodeText` that is not valid UTF-8 is refused rather than transcoded. | §17.12 |
 | `LM-13` | `language-models` | The text laws a tokenizer elaborates through are LexLean source and not authored text: the module that states them is one language-1.2 native core module of the embedded `language/text-1.2` project, the project holds no file of Lean source, no independently authored Lean file anywhere in the release tree declares the `LexLeanText` namespace or lies under its module root, and the one-time migration input is absent; the registry lists only that module, the declarations and their exact axiom policies are read from its native data, which the compiler embeds and hashes into the language-1.2 semantics, and a module that declares a text component imports the generated module rather than splicing any Lean text. | §17.10, §17.12 |
 
-**Total required capability IDs:** 404.
+**Total required capability IDs:** 405.
 
 No row may be downgraded to `some-true` or `open`. Upstream Lean facts are ledger/authority rows, not substitutions for these build behaviors.
 

VERIFICATION.md

@@ -8215,6 +8215,7 @@ prereleases, unrelated occurrences of the pin, and malformed banners.
 Validated after the fix: the unit case and `conformance_vr_02` pass (the
 latter in 4.76 s), as do formatting, workspace/all-target Clippy with warnings
 denied, model/spec-link audits, and all five BDD meta-gate tests.
+
 ### a standard-library member can fail its oracle (SPEC.md §17.22)
 
 `SL-01` holds every member of `LexLeanStd.Text` to the function of Rust's
@@ -8245,6 +8246,33 @@ admit exactly what they realize.
 Removed: the source was restored; `conformance_sl_01` passes, in 156 s with
 the production export of the seven members under the pinned Lean.
 
+`SL-02` holds `LexLeanStd.Sha256` to FIPS 180-4 (#126, stage 1): both roots'
+lowered programs under the calculus evaluator and their rendered `rust-std`
+packages under the pinned rustc compute the three FIPS 180-4 example digests,
+every vector of the NIST CAVP `SHA256ShortMsg.rsp` and `SHA256LongMsg.rsp`
+files (`tests/stdlib/sha256/`), and the digest of the `sha2` crate on a seeded
+corpus (every length 0..200, then random lengths to 4 KiB, and the million-`a`
+example under rustc). The oracles are checked against each other first, and one
+disagreement with them fails the case.
+
+- **one bit of the round function.** `a := (add t1 t2)` becomes
+  `a := (prim bit_xor (add t1 t2) (1 : UInt32) : UInt32)`, so the new `a` of
+  every round is off in its low bit. `-- conformance_sl_02`, without its Lean
+  half:
+
+  ```text
+  panicked at crates/conformance/src/cases/stdlib_sha256.rs:305:9:
+  sha256: the evaluator and the oracles disagree on 372 of 372 runs: ["run 0 on [Bytes { hex: \"616263\" }]: {"constructor":0,"fields":[{"kind":"u32","value":"3804428771"}, …],"kind":"adt"} != {"constructor":0,"fields":[{"kind":"u32","value":"3128432319"}, …],"kind":"adt"}", …]
+  ```
+
+  `3128432319` is `0xba7816bf`, the first word of the FIPS 180-4 digest of
+  `abc`. The same plant is made by the case itself on a copy of the project on
+  every run, so the gate stays armed.
+
+Removed: the source was restored; `conformance_sl_02` passes, in 305 s with
+the production export of both roots under the pinned Lean (`conformance_sl_01`
+in 206 s on the same tree).
+
 ## The `bdd` recipe as the parts of one run (Issue #131)
 
 With UOR Atlas verified as the parts of one run, the `rest` leg became the