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

[humuhumu33]

Stdlib lane of #92, member 1 of the order the issue sets: bytes and text over Bytes. Not the effects boundary (§3), which stays with afflom. SHA-256 is claimed under #126 and stays out.

What this adds

• stdlib/, a language-1.2 project beside compiler/ (module prefix LexLeanStd), written in the authoring notation and verified by the examples leg exactly as compiler/ is (expected/build, expected/verify committed). First module Text, seven production roots for rust-std:

  root	oracle (Rust std)
  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
  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

  Written as the spike did (B1–B3): components over Bytes, character classes by equal on UInt8, no String scalar iteration; scans are iterate_until under the subject's length, accumulations list_fold, so the members carry recursion where they realize a library template (fix(production): a primitive realized by a library template carries the recursion effect (step 1 of #105) #129) and each declaration admits exactly the effects its closure realizes.

• SL-01 (new suite stdlib, SPEC.md §17.22, register 382): the project checks and builds and the seven roots are eligible with exactly their declared effects; each member's lowered program under the calculus evaluator (600 runs) and its rendered rust-std package under the pinned rustc (3 000 runs) agree with the Rust oracle on a seeded corpus of edge cases and random inputs; a planted character class in trim (form feed → vertical tab) is detected; and under the pinned Lean the production export certifies every member (A, B, E) into packages byte-identical to the committed ones under tests/production-export/stdlib/, each realizing the program the differential ran.

• Harness: production_export::EXPORTED adds stdlib to what check-production-export compares (PX-01 keeps its two examples); P::stdlib(); verify-examples and check-golden discover stdlib/ beside compiler/.

What it does not do

• No theorems over the members: Bytes equality by evaluation is B4 ([v0.4] #27 stage 6: complete the closed Rust AST so the runtime is generated from the calculus #91 stage 2). Until then the module's behavior is held by the differential only, as §2.B4 of the issue says.
• No String-typed members: text is handled as UTF-8 bytes (§17.22 says so).

Evidence

SL-01 on Linux x86-64 with the pinned toolchain, just vv (see the CI run). The planted defect record is in VERIFICATION.md.

Closes nothing; #92 stays open for the remaining members (sorting, JSON, hex/decimal), one PR each.

🤖 Generated with Claude Code

[afflom]

FYI from the axiom-parser pilot (#160, which vendors Text.lex.tex byte for byte minus the production: clauses, checked on every run). No change asked of this PR.

• Text.trim is trim_ascii by design and is the right oracle for what it says. The parser needs Rust's str::trim / char::is_whitespace (Unicode White_Space: VT, U+0085, U+00A0, U+1680, U+2000-200A, U+2028/2029, U+202F, U+205F, U+3000), so the pilot defines its own trimmed. A trimUnicode member could replace it later.
• startsWith, endsWith, lines, splitOn, find, matchAt, sliceOr, byteAt are used as they are and agree with the Rust parser on the pilot's corpus (12,000 audit outputs, the committed vectors).
• Not found missing: rfind (the pilot has splitLast), parse usize and decimal formatting of a Nat (the pilot has local ones; they may be worth a member in your hex/decimal PR).

---

Generated by Claude Code

[afflom]

@humuhumu33, #159 is merged: main is ccd37ec7 (tested head 1c04cf36, 26 of 26 green; main's push run on 097b9b97 is green too). This PR's head 48e06da1 is on 097b9b97, so it lacks #159. Your run on it (38982809506) is still going (rest, atlas (cert4-replay), Intel macOS).

How I will treat the gap, so you do not spend a run on it. #159 changes only CI (ci.yml, Justfile, xtask bdd), the inventory, the join's toolchain check and the conformance harness; it changes no language data, generated Lean, record or package, so no artifact this PR's run verified can differ. For this PR only, and because of that, I accept your run on 48e06da1 if it is green, after checking the merge myself. I did that on a scratch merge of main into your head (not pushed): conflicts only in CHANGELOG.md and VERIFICATION.md (both kept); validate-model 393 ids, validate-spec-links 393 bijective, check-test-inventory reads the five parts (compiler 21, preservation 14, production 39, verification 91, rest 266; SL-01 lands in rest), check-golden equal; conformance_rp_07, rp_13, rp_14 and sl_01 are running on it now and I will post the result. Main's push run after the merge is the backstop; I will watch it.

If you push anything to this branch before then, the exception is void and the run on the new head is the one I wait for. Please do not merge main into it for this.

(R3: the first commit registers SL-01, writes the case and the module together, so the order row, scenario, failing test, implementation is not in the history. The gates check that the row, scenario and test exist, not their order; I note it as I did on #146.)

---

Generated by Claude Code

[afflom]

Approved at 8591c0c84, as a non-author.

What ran. Run 38982809506 on 48e06da1: all 22 checks green (host legs, examples, rest with SL-01, the 14 Atlas jobs, repro, honesty). 8591c0c84 is that head plus one merge commit of main ccd37ec7 (#159) that I made and pushed: CHANGELOG.md and VERIFICATION.md conflicted and both sides are kept. #159 changes only CI, the inventory, the join's toolchain check and the harness, no generated artifact, so the run on 48e06da1 stays the evidence for everything but the merge itself. I checked the merge before pushing: validate-model 393 ids, validate-spec-links 393 bijective, check-test-inventory (five parts, SL-01 in rest), check-golden (stdlib: 7 artifacts equal), and conformance_rp_07, rp_13, rp_14, sl_01 pass (sl_01 in 399 s with the Lean-backed export). Main's push run after the merge is the backstop.

Against #92's stdlib lane.

• stdlib/ is a language-1.2 project (LexLeanStd.Text) written in the notation; seven roots for rust-std, each admitting exactly the effects its closure realizes.
• SL-01: each member's lowered program under the calculus evaluator (600 runs) and its rendered package under the pinned rustc (3,000 runs) agree with the Rust oracle on a seeded corpus; a planted character class in trim is detected; under the pinned Lean the production export certifies every member (A, B, E) into packages byte-identical to the committed ones.
• Honest scope: trim is trim_ascii; there are no theorems over the members (Bytes equality by evaluation is #91 stage 2), so the module's behavior is held by the differential, which is build evidence and is described as such. check-golden and check-production-export read stdlib/ beside the examples.

Not blocking. The first commit registers SL-01, writes the case and the module together, so R3's order is not in the history; the gates check existence, not order.

Merging with a merge commit pinned to this head.

---

Generated by Claude Code