[v0.4] Add language-model semantic components and compositional text-processing pipeline

Scope

Provide the closed primitives needed to model language-processing systems as LexLean programs and reusable stdlib components.

Work

Define typed text/token/byte interfaces, vocabulary/tokenization contracts, bounded context/state, generation/classification interfaces, and deterministic composition semantics.
Treat learned parameter artifacts separately from semantic contracts.
Define sampling/randomness only through an explicit machine/randomness contract; deterministic profiles must remain deterministic.
Support model adapters whose observable behavior is fully specified at the LexLean boundary.

DoD

No free-form prompt string is treated as semantic code.
Tokenization/encoding/decoding and context bounds are explicit and tested.
Any nondeterminism is parameterized by an explicit source/seed/distribution contract and accounted for in production claims.

Acceptance criteria

End-to-end fixture implements a nontrivial text model pipeline from closed components.
Round-trip/token boundary, context overflow, invalid UTF-8/artifact, and nondeterminism-contract negatives are covered.
Generated Lean verifies all stated contracts and production-eligible portions compile through the v0.4 compiler.
Full just vv passes.

Depends on model semantics and production compiler API.

Design for #30 (proposal; work proceeds unless objected to)

Base: main 0b0ebd9. This builds on #29 (models) and #31 (reasoning machines) and adds no engine and no opaque primitive. Every new construct is a closed declaration in lexlean/semantic-module/2. Linking elaborates it into ordinary language-1.2 definitions and theorems, exactly as models and reasoners are.

New closed declarations (language 1.2 only)

tokenizer

Schemes byte_level and longest_match. The vocabulary is a [v0.4] Introduce closed Model, Realization, Contract, and Evidence semantics #29 artifact with role vocabulary and schema utf8_lines.
Tokens are uint32. Ids 0..255 are the single bytes, always present as the byte fallback. Ids from 256 are the vocabulary pieces, in artifact order.
Elaborates to encode/decode over bytes, plus encodeText/decodeText over string through utf8_encode/utf8_decode.
Generated and kernel-checked: roundtrip (∀ b, decode (encode b) = some b, which also fixes token boundaries), text_roundtrip, and in_range.

context_window

Capacity of at least 1, and overflow refuse or keep_last.
Elaborates to a [v0.4] Introduce closed Model, Realization, Contract, and Evidence semantics #29 stateful contract and realization over list uint32. The invariant is length ≤ capacity, with preservation, suffix and exactness theorems. It composes like any stateful stage, including scan.

text_generator

Takes a tokenizer, a window, and a scorer, which is a [v0.4] Introduce closed Model, Realization, Contract, and Evidence semantics #29 model from list uint32 to list int with width equal to the vocabulary size.
Mandatory max_tokens and stop. The loop is iterate_until, and running out of fuel is exhausted.
Policy greedy: takes the first maximum and has no seed parameter, so it is deterministic by type.
Policy sample: the generator is xorshift32 and the distribution proportional, both closed. The seed is an explicit input and the next seed an explicit output. The arithmetic is checked fixed-width, with no wrapping primitive added.
The eligibility report gains text_rows, which record the nondeterminism contract of each production root, as [v0.4] Add reasoning-machine semantics: state, rules, search, verification, iteration, and termination #31's reasoning_rows do.

text_classifier

Token-count features from the tokenizer, fed to a [v0.4] Introduce closed Model, Realization, Contract, and Evidence semantics #29 model that produces the label.

text_failure

A closed type: invalid_utf8, unknown_token, context_overflow, exhausted.

Adapters are #29 models whose realizations are these elaborations, with contracts over text types and satisfies_contract evidence. There is no new adapter kind.

No free-form prompt string is semantic code, by construction. string is data, the primitive set has no string-to-code member, and a prompt reaches a model only as encodeText. One conformance ID audits the registries for a string-to-code row and plants one.

Register (suite `language-models`, prefix `LM`)

IDs: LM-01..LM-12 cover tokenizers, the round-trip and boundary laws, invalid UTF-8, context bounds, greedy generation, explicit randomness, classification, composition and adapters, no prompt as code, production (rust-std; rust-core refused because text allocates; differential; certificates A, B and E), the end-to-end example examples/text-models with a planted mutation, and coverage of every fixed helper.
Codes: LLT4013 "Text interface mismatch" and LLT4014 "Unbounded or unspecified text generation". All others are reused: LLR3007, LLR3008, LLS8002, LLT4001, LLT4005, LLV7002.
Coordination: none of these collide with feat(verify): public host-driven API to end live child groups (#67) #75 (CL-22, LLV7018) or feat(api): production export contract and stable compiler API (#28) #76 (CL-23..25, PX-01..20, LLC0201..0209, LLV7101..7109).
Identity: semantics-1.2.toml bumps semantic_ir, lean_backend and latex_backend, with the usual relock and regeneration of 1.2 projects. fix(backend): lower explicit shared byte literals without widening limits #68 bumps lean_backend too; whichever of us lands later rebases.

Questions (a recommendation for each)

Where the universal laws are proved. roundtrip for every input cannot be closed by decide. The options are (a) a fixed emitted Lean runtime LexLeanText, like LexLeanModels and LexLeanReasoning, or (b) a LexLean-authored lexlean.text library proved in LexLean's proof language.
- Recommendation: (a), for consistency with [v0.4] Introduce closed Model, Realization, Contract, and Evidence semantics #29 and [v0.4] Add reasoning-machine semantics: state, rules, search, verification, iteration, and termination #31.
- Your comment on [v0.4] Author the production compiler itself in LexLean and verify the generated Lean implementation #27 refuses handwritten Lean in the admitted dependency. If that audit covers emitted runtimes too, (b) is the right home, at a higher cost and with some risk that the structured proof language needs extending for the matcher's induction. This is the one decision I need before going past the IR layer.
Vocabulary pieces stay utf8_lines, with the 256 byte ids as the fallback. Arbitrary-byte pieces (byte-level BPE) would need a new artifact schema, which the acceptance criteria do not require.
xorshift32 and proportional are the only closed sampling members. They are stated as a contract, with no claim about randomness quality.
Text components are rust-std only. rust-core is refused with LLT4005, because strings and bytes allocate.

I start with the register rows, scenarios, failing named tests, and the IR and checker layer, none of which depends on question 1.

Generated by Claude Code

feat(language-1.2): register the language-model capability contract (#30

feat(language-1.2): language-model example fixture, SPEC subsection, …

feat(language-1.2): register the language-model capability family (#30)

feat(language-1.2): register the text-component family per the design…

feat(language-1.2): text-component declarations and their family modu…

On question 1 of the design (where the universal laws are proved), for whoever picks it up; I am not working on #30.

The maintainers' answer on #27 (comment) is that handwritten Lean is out of scope as normative content, and that includes the fixed runtimes the backend splices (LexLeanModels, LexLeanReasoning today are string constants in backend/semantic.rs). Stage 4 of #27, #90, is the issue that converts those to native modules. So (a) as written, a new handwritten LexLeanText text constant, adds a runtime that #90 would immediately have to remove.

A route that is consistent with both and is already proven in this repository (#79: the preservation and certification libraries): author the text laws once as Lean in a scratch directory outside the release tree (roundtrip by the matcher's induction, text_roundtrip, in_range, the UTF-8 laws), export the elaborated environment losslessly into native lexlean/core-module/2 data, commit that as .lex.tex in an embedded project, record the migration (declarations equal in types, values, reducibility and attributes after re-export), and have generated 1.2 modules import the generated module rather than splice text. The release tree then holds no handwritten Lean for it, the permanent SP-12/GC-11-style condition extends to it, and a change to the laws goes through the same round trip. The cost is a migration record, not a proof language; (b), a proof language for LexLean-authored lexlean.text, would have to state the matcher's induction, which is the project #27's plan declined for the libraries.

One coordination point: rust_backend is now 3 on main once #88 merges (#81), and lean_backend/latex_backend bumps for #30 rebase over it; #82's register total (363 to 375) has to be recomputed against main's 366 (367 with RB-08).

Generated by Claude Code

feat(language-1.2): register the text-component family per the design…

feat(language-1.2): text-component declarations and their family modu…

feat(language-1.2): the text laws as an embedded native library (slic…

test(#30): a vocabulary reference is a member object

feat(#30): the tokenizer elaboration moves the language-1.2 semantic_…

fix(#30): restore the main changes the 9e260b2 merge dropped (#130 PX…

docs(#30): changelog entry for the tokenizer elaboration and the text…

chore(#30): regenerate CONFORMANCE.md for the 390-row register

chore(#30): regenerate locks, goldens, calculus packages, fixtures, p…

fix(#30): the text declarations have production rows, the laws librar…

fix(#30): the text-laws records join the attestation through their ow…

chore(#30): regenerate every language-1.2 record for the merged tree'…

fix(#30): the four text declarations are not-runtime rows of the orac…

chore(#30): regenerate every language-1.2 record for the tree merged …

chore(#30): regenerate the language-1.2 records for the tree merged w…

Merge pull request #82 from UOR-Foundation/issue-30-language-model

Slice 2 of #30: bounded context and generation (intent)

Slice 1 (#82: tokenizers, LM-01..LM-03, LM-13) is merged. I'm taking slice 2 next. It makes context_window and text_generator real. Linking does not elaborate either of them today.

Constructs

context_window (capacity ≥ 1, overflow refuse or keep_last) elaborates to capacity, fit : list uint32 -> option (list uint32) and push. The name admit is reserved by the name rules, so the admission is called fit.
text_generator names a prior tokenizer, a prior window, a prior stateless [v0.4] Introduce closed Model, Realization, Contract, and Evidence semantics #29 model from list uint32 to list int whose evidence discharges every runtime check, a prior uint32 stop token, and max_tokens ≥ 1. It elaborates to:
- score;
- two closed inductives, End (stop, exhausted) and Failure (unknown_token, context_overflow, invalid_utf8), which are the text_failure members;
- run, the library's loop, structural in max_tokens;
- generateTokens, and generate over string.
Policies:
- greedy takes the first maximum, and nothing it elaborates to takes a seed.
- sample uses the closed xorshift32 and proportional members. It takes seed : uint32 and returns the next seed. No primitive is added, and no claim is made about randomness quality.
Exhaustion: running out of max_tokens is an end reason that keeps the output, not a failure.

Laws, all generated and kernel-checked

Each law is proved by one LexLeanText lemma, applied after unfolding, as the tokenizer's are.

Window laws:
- bounded and push_bounded: every admitted or pushed context fits.
- exact: a context that fits is admitted unchanged.
- suffix (keep_last): what is kept is the end of the context.
- refuses (refuse): a context that does not fit is not admitted.
Generator laws:
- bounded: at most max_tokens tokens are generated.
- context_bounded: the run equals the run whose scorer is never consulted on a context that does not fit.

The lemmas are new declarations of the native LexLeanText module. They were added by the route from your 2026-10-14 comment: authored as Lean outside the tree, exported to core-module/2, committed as .lex.tex, and re-exported from the compiler-generated Lean for an equivalence check. That check found the same 198 declarations and 19,448 nodes, differing only in the decoder's Lean import and one hygienic binder name. It is recorded as a second entry in tests/text-laws/MIGRATION.md.

I put the loop in the library rather than proving it through LexLeanReasoning's iterateUntil lemmas. That keeps every text law in one place, proved once with induction in Lean, and adds no proof template.

Other changes

Policies: both declarations gain an axioms policy, as tokenizer has, and the audit holds them to it.
Register: LM-04 (windows), LM-05 (greedy generation, bounds, and every end and failure evaluated by the kernel) and LM-06 (sampling: the same prompt and seed give the same output, with reference vectors).
Codes: LLT4013 and LLT4014 from my design are now tooling's. Interface mismatches keep LLT4006. One new code, LLT4016 "Unbounded or unspecified text generation", covers capacity 0 and max_tokens 0.
Identity: semantic_ir and latex_backend move to 13.
Docs: SPEC §17.12 gains the Text components subsection that the production section already cites.

Left for later

Slice 3: classifiers, adapters, composition (a window as a scan stage), and the no-prompt-as-code audit.
Slice 4: production rows (text_rows), rust-std/rust-core, examples/text-models end to end, and the just vv that closes [v0.4] Add language-model semantic components and compositional text-processing pipeline #30.

Timing: this moves the language-1.2 identity. Per your 10:10Z status, the PR stays a draft until certificate A (#157) and certificate B (#163) have landed. I'll then merge main once, regenerate, and mark it ready. If you'd rather it land at a different point in the queue, say so here.

Navigation Menu

Repository navigation

[v0.4] Add language-model semantic components and compositional text-processing pipeline #30

Scope

Work

DoD

Acceptance criteria

Design for #30 (proposal; work proceeds unless objected to)

New closed declarations (language 1.2 only)

Register (suite `language-models`, prefix `LM`)

Questions (a recommendation for each)

5 remaining items

Slice 2 of #30: bounded context and generation (intent)

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

[v0.4] Add language-model semantic components and compositional text-processing pipeline #30

Description

Scope

Work

DoD

Acceptance criteria

Activity

humuhumu33 commented on Oct 12, 2026

Design for #30 (proposal; work proceeds unless objected to)

New closed declarations (language 1.2 only)

Register (suite language-models, prefix LM)

Questions (a recommendation for each)

afflom commented on Oct 14, 2026

5 remaining items

humuhumu33 commented on Oct 17, 2026

Slice 2 of #30: bounded context and generation (intent)

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

Register (suite `language-models`, prefix `LM`)