feat(language-1.2): context windows and greedy and seeded text generators (LM-04..LM-06; part of #30)

CHANGELOG.md

@@ -15,6 +15,30 @@ versions, and the entries below say what each tag does and does not claim.
 
 ## Unreleased
 
+- Context windows and text generators (SPEC.md §17.12, *Text components*,
+  `LM-04`..`LM-06`, slice 2 of #30; new code `LLT4016`). A `context_window`
+  of capacity at least 1 and overflow `refuse` or `keep_last` elaborates to
+  `capacity`, `fit`, and `push` over the text-laws library and generates
+  `bounded`, `push_bounded`, `exact`, and `suffix` (`keep_last`) or
+  `refuses` (`refuse`). A `text_generator` over a prior tokenizer, window,
+  stateless `list uint32 -> list int` model, and `uint32` stop token, with
+  `max_tokens` at least 1, elaborates to `score`, the closed inductives
+  `End` (`stop`, `exhausted`) and `Failure` (`unknown_token`,
+  `context_overflow`, `invalid_utf8`), `run` (the library's bounded loop),
+  `generateTokens`, and `generate`, and generates `bounded` (at most
+  `max_tokens` tokens) and `context_bounded` (the scorer is never consulted
+  on a context that does not fit). `greedy` takes the first maximum and no
+  seed; `sample` draws through the closed `xorshift32` and `proportional`
+  members with the seed an explicit input and the next seed an explicit
+  output. Both declarations gain an `axioms` policy. A capacity or
+  `max_tokens` of 0 is `LLT4016`; a member of another kind is `LLT4006`. The
+  laws are new declarations of the native `LexLeanText` module, authored once
+  outside the release tree and exported by the same round trip as slice 1
+  (`tests/text-laws/MIGRATION.md`, second record). The language-1.2
+  `semantic_ir` and `latex_backend` versions move to 14 and 13, so every
+  language-1.2 lock, golden, fixture, and verification record is
+  regenerated. Text classifiers, adapters, composition, production, and the
+  end-to-end example remain for later slices. The register holds 417 IDs.
 - UOR Atlas, #168: the census windows `CensusCert4` and `CensusCert10`
   (`gramRange 4000 1000 = true` and `gramRange 10000 1000 = true`, each one
   `of_decide_eq_true`) are proved from ten width-100 certificates each,

CONFORMANCE.md

@@ -229,6 +229,9 @@ the error registry does not sanction (R5, `ERRORS.md`).
 | `LM-01` | `build` | A `tokenizer` is a closed language-1.2 declaration whose scheme is `byte_level` or `longest_match` and whose vocabulary is a #29 artifact with role `vocabulary` and schema `utf8_lines`; tokens are `uint32`, the single bytes are the ids 0..255 present always as the byte fallback, the vocabulary pieces take the ids from 256 in artifact order, and the declaration elaborates to `encode` and `decode` over `bytes` together with `encodeText` and `decodeText` over `string` through `utf8_encode` and `utf8_decode`, so a scheme outside the closed enumeration, a vocabulary whose role or schema is not the one stated, or a token outside `uint32` is refused as a schema violation (`LLT4001`) or by the artifact rules (`LLR3007`). |
 | `LM-02` | `build` | A tokenizer's laws are generated and kernel-checked: `roundtrip` states that for every byte string `b`, `decode (encode b)` is `some b`; `text_roundtrip` states the same over `string`; and `in_range` states that every token a decode produces indexes the vocabulary, so the round trip also fixes the token boundaries, and a tokenizer whose elaboration does not close these laws fails verification. |
 | `LM-03` | `build` | 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. |
+| `LM-04` | `build` | A `context_window` is a closed language-1.2 declaration of a capacity of at least one token and an overflow disposition `refuse` or `keep_last` that elaborates to `capacity`, `fit` over `list uint32`, and `push` of one `uint32` token through the text-laws library, with its laws generated and kernel-checked: `bounded` and `push_bounded` state that every admitted or pushed context fits the capacity, `exact` that a context that fits is admitted unchanged, `suffix` under `keep_last` that what is kept is the end of the context, and `refuses` under `refuse` that a context that does not fit is not admitted; a capacity of 0 is refused (`LLT4016`), a disposition or capacity outside the closed schema is a schema violation (`LLT4001`), and a window whose laws observe an axiom its policy omits fails the audit. |
+| `LM-05` | `build` | A `text_generator` under the `greedy` policy names a prior tokenizer, a prior context window, a prior stateless model from `list uint32` to `list int` whose every runtime check its evidence discharges, a prior `uint32` stop token, and a `max_tokens` of at least one, and elaborates to the closed outcome types `End` (`stop`, `exhausted`) and `Failure` (`unknown_token`, `context_overflow`, `invalid_utf8`) and to a loop of at most `max_tokens` steps that takes the first maximum and no seed; its laws `bounded` (at most `max_tokens` tokens are generated) and `context_bounded` (the scorer is consulted only on contexts that fit the window) are generated and kernel-checked, the loop reaches each end and each failure in the kernel, a wrong claim about its output fails verification, a `max_tokens` of 0 is refused (`LLT4016`), and a member of another kind is refused (`LLT4006`). |
+| `LM-06` | `build` | Nondeterminism is an explicit contract: a `text_generator` under the `sample` policy draws through the closed `xorshift32` generator and `proportional` distribution only, takes its seed as an explicit `uint32` input and returns the next seed as an explicit output, so the same prompt and seed give the same output, which the kernel computes; it has the same generated and kernel-checked laws as a greedy generator, `xorshift32` agrees with the reference sequence, and a generator or distribution outside the closed members, a sample policy without one, or a seed stated on a policy is a schema violation (`LLT4001`). |
 | `LM-13` | `build` | 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. |
 
 ## latex-pdf

ERRORS.md

@@ -400,6 +400,12 @@ A tooling term is not well typed: a call with the wrong type arguments or argume
 
 Class: `language`. Exit code: 1.
 
+## `LLT4016` --- Unbounded or unspecified text generation
+
+A text declaration does not state the bound it must: a context window with capacity 0, or a text generator with max_tokens 0.
+
+Class: `language`. Exit code: 1.
+
 ## `LLV7001` --- Lean/Lake/leanchecker version or executable mismatch
 
 Lean/Lake/leanchecker version or executable mismatch.

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 414 registered conformance IDs are implemented and pass; `just vv` runs clean from a checkout with the pinned toolchain installed.
+All 417 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.
 
@@ -186,7 +186,8 @@ Every row is validated by `just vv`; the IDs link the claim to its register row,
 | The bootstrap project: the compiler's own components as language-1.2 source compiled by LexLean's production pipeline to certified Rust packages, the exact axiom-output parser and its closed Lean-name check and the preservation lexer and token audit, each held to the Rust it replaces (the stage-0 oracle) by the committed vectors and a seeded differential of its evaluator and rustc realizations, with planted defects detected and the production export committed | `BS-01`..`BS-02` | `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` |
-| Language-1.2 text components, first slice: tokenizers and their round-trip laws, with the laws carried as one native core module the generated modules import rather than authored Lean text (context windows, text generators, text classifiers, adapters, and composition follow in their own slices and add their rows then) | `LM-01`, `LM-02`, `LM-03`, `LM-13` | `build` |
+| Language-1.2 text components, first slice: tokenizers and their round-trip laws, with the laws carried as one native core module the generated modules import rather than authored Lean text | `LM-01`, `LM-02`, `LM-03`, `LM-13` | `build` |
+| Language-1.2 text components, second slice: context windows with their bound, exactness, and suffix laws, and greedy and seeded text generators bounded by `max_tokens` whose scorer sees only contexts that fit, over the same native laws module (text classifiers, adapters, and composition follow in their own slices and add their rows then) | `LM-04`, `LM-05`, `LM-06` | `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.