feat(stdlib): the first member, bytes and text over Bytes (#92)

.gitignore

@@ -26,3 +26,4 @@ compiler/.lexlean/
 
 # Claude Code worktrees and session state (never part of the release set).
 .claude/
+stdlib/.lexlean/

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 first member: bytes and text over `Bytes`
+  (SPEC.md §17.22, `SL-01`, #92; no new diagnostic code). `stdlib/` is a
+  language-1.2 project beside `compiler/` under the module prefix
+  `LexLeanStd`, written in the authoring notation; its `Text` module declares
+  `startsWith`, `endsWith`, `trim`, `lines`, `splitOn`, `joinWith`, and
+  `find` as production roots for `rust-std`, each admitting exactly the
+  effects its closure realizes. `SL-01` runs every member's lowered program
+  under the calculus evaluator and its rendered package under the pinned
+  rustc on a seeded corpus against Rust's `starts_with`, `ends_with`,
+  `trim_ascii`, `lines`, `split`, `join`, and `find`, detects a planted
+  character class in `trim`, and, under the pinned Lean, compares the
+  certified packages the production export publishes with the committed
+  ones under `tests/production-export/stdlib/`. The project passes the
+  example gates (`verify-examples`, `check-golden`) and
+  `check-production-export` compares its packages. `SL-01` brings the
+  register to 393 IDs.
 - The `bdd` recipe runs in CI as the parts of one run (SPEC.md §9.2, §9.4,
   `RP-13`, `RP-14`, #131; no new diagnostic code, no new ID). The `rest` leg
   took 111.5 minutes on the run that merged #152 (CI run 38905653756), 95.7 of

CONFORMANCE.md

@@ -512,6 +512,12 @@ the error registry does not sanction (R5, `ERRORS.md`).
 | `SM-30` | `build` | Language 1.2 graph literals reference only declared nodes, a graph's nodes are its keys and every successor, and successor, reachability, and topological-order queries are deterministic, bounded by the node count, and report a cycle as none. |
 | `SM-31` | `build` | Language 1.2 accepts a second native core-module schema, and only language 1.2 does, whose annotation nodes, extended names, definition safety and groups, compiled and reducibility state, and matcher, projection, no-confusion, simplification, equation-record, inlining, sparse-casesOn, and grind extension state are closed data that the linker validates against the kind of the declaration carrying it and bounds in depth by max_scope_depth, and that both backends render, and that the Lean backend's one fixed decoder submits through Lean's checked declaration API, so that the generated module elaborates under the pinned Lean with exactly its pinned axioms. |
 
+## stdlib
+
+| 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. |
+
 ## tooling
 
 | ID | Level | Statement |

README.md

@@ -138,7 +138,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 392 registered conformance IDs are implemented and pass; `just vv` runs clean from a checkout with the pinned toolchain installed.
+All 393 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.
 
@@ -178,6 +178,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 literal `nat-add-zero` example, the Lean-verified feature examples, and the complete negative fixture suite | `EX-01`..`EX-08` | `build` |
 
 Range rows abbreviate consecutive registered IDs; every individual ID in each range is registered in [`model/ids.toml`](model/ids.toml) at the stated level with its own scenario and test.

SPEC.md

@@ -6581,6 +6581,44 @@ relates the module's pieces to its text, and `fmt` writes a language-1.2 core
 module of schema 2 in the notation, so a module written as `\coredata` leaves
 the data form by being formatted.
 
+### 17.22 The standard library
+
+The standard library is the project `stdlib/` beside `compiler/`: language-1.2
+source of the product, written in the authoring notation (§17.21) under the
+module prefix `LexLeanStd`, whose members are production roots (§17.13). It is
+not an example: it passes the gates of §28.6 as the compiler project does, its
+production export (§24.7) is committed under `tests/production-export/stdlib/`
+and compared by `cargo xtask check-production-export`, and a member is
+validated by a differential before it is a member. The differential runs the
+member's lowered program under the calculus evaluator (§17.14) and its
+rendered `rust-std` package under the pinned rustc (§17.16) on a seeded corpus
+against the function of Rust's standard library the member corresponds to, and
+a member whose outcome differs from its oracle on any input is not committed.
+A member's declaration admits exactly the effects its runtime closure realizes
+on its target, so the eligibility report of every member is its own text.
+
+The first module, `Text`, is bytes and text over `Bytes`. A `String` has no
+scalar iteration in language 1.2, so text is handled as its UTF-8 bytes, a
+character class is a comparison of `UInt8` by `equal`, and a member that is
+defined on text is defined on the bytes of valid UTF-8. Its members and their
+oracles:
+
+| Member | Oracle |
+| --- | --- |
+| `startsWith (subject prefix : Bytes) : Bool` | `<[u8]>::starts_with` |
+| `endsWith (subject suffix : Bytes) : Bool` | `<[u8]>::ends_with` |
+| `trim (subject : Bytes) : Bytes` | `<[u8]>::trim_ascii` |
+| `lines (subject : Bytes) : List Bytes` | `str::lines` on UTF-8 input: a line ends at `\n` or `\r\n`, and the last line needs no ending |
+| `splitOn (subject : Bytes) (delimiter : UInt8) : List Bytes` | `<[u8]>::split` |
+| `joinWith (pieces : List Bytes) (separator : Bytes) : Bytes` | `<[Vec<u8>]>::join` |
+| `find (subject needle : Bytes) : Option Nat` | `str::find` on UTF-8 input, as a byte offset |
+
+Every scan is `iterate_until` under the subject's length as its fuel and every
+accumulation is `list_fold`, so a member carries `recursion` exactly where it
+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`).
+
 ## 18. Lean backend
 
 ### 18.1 Output contract
@@ -8727,7 +8765,7 @@ Tests MUST establish that LexLean rejects, at minimum:
 
 ### 28.6 Example verification
 
-Every directory under `examples/` is discovered rather than listed. Each example MUST include its lock and expected platform-independent build outputs. `cargo xtask verify-examples` runs `fmt --check`, `lock --check`, `check`, `build`, and `verify`. The `compiler/` project (§17.14, §17.15) passes the same gates as an example.
+Every directory under `examples/` is discovered rather than listed. Each example MUST include its lock and expected platform-independent build outputs. `cargo xtask verify-examples` runs `fmt --check`, `lock --check`, `check`, `build`, and `verify`. The `compiler/` project (§17.14, §17.15) and the `stdlib/` project (§17.22) pass the same gates as an example.
 
 ---
 
@@ -9377,8 +9415,9 @@ Every row below is normative, has honesty level `build`, and MUST be copied byte
 | `RT-02` | `runtime` | The runtime text of languages 1.0 and 1.1 is the one declared exception: the portable runtime and the decoder of core module 1 are the released bytes, held as data under `language/runtime-1.2/frozen/`, read by the language-1.0 and 1.1 backends alone, excluded from the language-1.0 and 1.1 identities, and reproduced byte for byte by the released language-1.1 and 1.0 output; a one-byte change of either is not the released output. | §17.12, §21.2 |
 | `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 |
 
-**Total required capability IDs:** 392.
+**Total required capability IDs:** 393.
 
 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

@@ -8159,6 +8159,35 @@ 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
+standard library it corresponds to: the member's lowered program under the
+calculus evaluator and its rendered `rust-std` package under the pinned rustc
+are run on a seeded corpus (edge cases first, then random inputs over the
+bytes the members distinguish), and one disagreement fails the case. The first
+run of the case found a defect in the source and not in the differential: three
+declarations admitted `overflow` their closures never realize, and the case
+refused them before any run (`startsWith: the declared effects`, declared
+`["allocation", "overflow"]`, realized `["allocation"]`); the declarations now
+admit exactly what they realize.
+
+- **a character class off by one.** `isSpace` takes the vertical tab (`11`)
+  for white space in place of the form feed (`12`), so `trim` keeps a form
+  feed and strips a vertical tab, which `<[u8]>::trim_ascii` never does.
+  `-- conformance_sl_01`:
+
+  ```text
+  panicked at crates/conformance/src/cases/stdlib.rs:483:17:
+  trim: the evaluator and Rust's standard library disagree on 431 of 600 runs: ["run 4 on [Bytes { hex: \"0b2061200b\" }]: {\"hex\":\"61\",\"kind\":\"bytes\"} != {\"hex\":\"0b2061200b\",\"kind\":\"bytes\"}", …]
+  ```
+
+  The same plant is made by the case itself on a copy of the project on every
+  run, so the gate stays armed: a corpus that no longer reaches the vertical
+  tab or the form feed fails the case.
+
+Removed: the source was restored; `conformance_sl_01` passes, in 156 s with
+the production export of the seven members under the pinned Lean.
 
 ## The `bdd` recipe as the parts of one run (Issue #131)
 

crates/conformance/src/cases/mod.rs

@@ -35,6 +35,7 @@ mod runtime;
 mod rust_backend;
 mod security;
 mod semantic_ir;
+mod stdlib;
 mod tooling;
 mod typed_diagnostics;
 mod verification;
@@ -114,6 +115,7 @@ pub fn run(id: &str) {
         "RT" => runtime::run(id),
         "TL" => tooling::run(id),
         "AU" => authoring::run(id),
+        "SL" => stdlib::run(id),
         _ => panic!("no conformance case is wired for {id}"),
     }
 }

crates/conformance/src/cases/repository.rs

@@ -411,7 +411,7 @@ pub(crate) fn run(id: &str) {
             let model = repo_model::Model::load(&root.join("model").into_std_path_buf())
                 .expect("the model loads");
             let table = spec_table();
-            assert_eq!(table.len(), 392, "§31 has 392 rows");
+            assert_eq!(table.len(), 393, "§31 has 393 rows");
             assert_eq!(model.ids.id.len(), table.len(), "register row count");
             for ((spec_id, spec_suite, spec_statement), row) in
                 table.iter().zip(model.ids.id.iter())