[0.5.0] SHA-256 in LexLean for every content identity #126

Activity

1. humuhumu33 commented on Oct 15, 2026

   

   humuhumu33

   on Oct 15, 2026

   Contributor

   More actions

   Taking this issue (humuhumu33, agent session). Scope of the first PR is stage 1: the module and its evidence, not yet the replacement of sha2.

   Stage 1 delivers

   • sha256 as a certified language-1.2 stdlib module in the .lex.tex notation (no JSON, no Rust): padding, message schedule, compression over UInt32 bit operations, driven by iterate, as the [v0.4] #27 stage 8: the production compiler authored in .lex.tex and compiled by LexLean to production software #92 spike says is expressible today.
   • R3 in order: register rows in model/ids.toml + SPEC §31, one scenario per ID, one conformance_<id> test per ID, positive and negative fixtures, and the planted one-bit error in the round function recorded in VERIFICATION.md.
   • Oracles: FIPS 180-4 example vectors, NIST CAVP SHA-256 short and long message vectors, and the sha2 crate as a differential on a seeded corpus. A disagreement fails closed and is filed as a defect, never resolved by adopting the oracle's answer.
   • A production root built through lexlean production build, with the generated Rust measured against sha2 on the corpus; the ratio goes in the PR, because stage 2 depends on it.

   Stage 2 (a later PR, after stage 1 lands and the ratio is known): switch every identity in SPEC §8 (source, semantic, artifact, attestation) to the LexLean digest, with the corpus and the examples byte-identical.

   Files I will not touch: calculus/rust/runtime.rs, the Rust AST and RustSemantics (#91), backend/semantic.rs and the core decoder (#90, #144), preservation certificates (#89, #146), production result schemas (#105, #130), the language-model family (#30, #82), CI partitioning (#131). If SHA-256 needs a primitive the calculus lacks, I stop and post the gap here with the smallest proposed addition.
2. humuhumu33

   added this to the LexLean v0.5 milestone on Oct 16, 2026
3. humuhumu33

   added 2 commits that reference this issue on Oct 17, 2026

   chore(stdlib): regenerate the stdlib records on main 8765fee (#126)

   ...

   3401fda

   docs(verification): the planted bit of SL-02 (#126)

   ...

   1de4151
4. humuhumu33 commented on Oct 17, 2026

   

   humuhumu33

   on Oct 17, 2026

   Contributor

   More actions

   Stage 1 is up as a draft PR: #172. Its head 1de4151e contains main 8765feea; the register is 405 with SL-02. I will mark it ready once its draft run is green and the head still contains main.

   Locally (WSL, Lean 4.32.1), conformance_sl_01 and conformance_sl_02 pass with the production export, as do check-golden, check-production-export, validate-model, validate-spec-links, the test inventory, RP-07/11/13/14, and clippy. A planted bit in the round function fails SL-02 on 372 of 372 runs (VERIFICATION.md).

   For stage 2: the certified sha256_hex package hashes at 70 to 90 MB/s on one core, 24 to 35 times slower than sha2 (with SHA extensions) from 16 KiB up; 16 MiB takes 242 ms against 7 ms. The PR body also records three findings for their own lanes: the package reader's 128-level nesting bound (§17.16), a certificate A refusal of a fallible callee in a nested else (#89 lane; no reduction yet), and an axiom-free roundConstant. Stage 2 waits on that ratio and on #105 for the stack.

   🤖 Generated with Claude Code
5. afflom

   added a commit that references this issue on Oct 19, 2026

   Wave 4: SL-02 (SHA-256), BS-03 (primitive scanner), PD-08 (stack boun…

   ...

   39edf5a