feat(semantic-ir): byte and fixed-width widening conversions in language 1.2 (SM-32, #114)

CONFORMANCE.md

@@ -497,6 +497,7 @@ the error registry does not sanction (R5, `ERRORS.md`).
 | `SM-29` | `build` | Reordered equivalent map, set, and graph literals link to byte-identical semantic data and generated Lean, LaTeX, and lexicon-closure artifacts, while duplicate keys, non-literal literal keys, and key types without a canonical order are rejected. |
 | `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. |
+| `SM-32` | `build` | Language 1.2 widening conversions, to_int from every fixed-width integer type to Int and to_nat from every unsigned fixed-width type to Nat, are total, are rejected under language 1.1, and elaborate in linking to ordinary terms over bit_and, equal, conditionals, and exact integer and natural sums, so that a production root decodes a byte string to integers with no decimal text in its lowered program and is certified like any other root. |
 
 ## tooling
 

README.md

@@ -137,7 +137,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 382 registered conformance IDs are implemented and pass; `just vv` runs clean from a checkout with the pinned toolchain installed.
+All 383 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.
 
@@ -154,7 +154,7 @@ Every row is validated by `just vv`; the IDs link the claim to its register row,
 | Total lexical closure: every accepted atom is covered by exactly one declared origin | `LX-01`..`LX-14` | `build` |
 | Versioned lexicon packages with closed schemas, denotations, and renderer tokens | `GL-01`..`GL-18` | `build` |
 | Fixed structural, mathematical, and proposition grammar with closed ambiguity handling | `GR-01`..`GR-16` | `build` |
-| Typed closed IR with canonical serialization, native core modules (and the second schema of them that lossless migration of the proof library needs), portable language-1.1 application data and operations, versioned language-1.2 semantic modules, products, and first-class functions, ordered collections and graphs, semantic snapshots, alpha identities, recursion evidence, and content identities | `SM-01`..`SM-31` | `build` |
+| Typed closed IR with canonical serialization, native core modules (and the second schema of them that lossless migration of the proof library needs), portable language-1.1 application data and operations, versioned language-1.2 semantic modules, products, first-class functions, and widening conversions, ordered collections and graphs, semantic snapshots, alpha identities, recursion evidence, and content identities | `SM-01`..`SM-32` | `build` |
 | Document and generic semantic declarations with exact self-application, type checking, structural recursion, recursive and mutual language-1.2 data, generic and executable higher-order definitions, mutual and well-founded recursion with semantic evidence, explicit state threading, and acyclicity rules | `DF-01`..`DF-18` | `build` |
 | The structured proof language with pinned Lean lowerings, including closed linear arithmetic | `PF-01`..`PF-19` | `build` |
 | Prose-free deterministic generated Lean with complete token traceability | `LN-01`..`LN-12` | `build` |

SPEC.md

@@ -2616,6 +2616,7 @@ backend runs.
 | `map_literal`, `set_literal`, `graph_literal` terms | `lexlean/semantic-module/2` | Literal collections of literal keys, canonicalized in linking under the collection rules below. |
 | collection primitives | `lexlean/semantic-module/2` | The `primitive` operations `map_insert`, `map_remove`, `map_lookup`, `map_contains`, `map_size`, `map_keys`, `map_values`, `map_entries`, `map_fold`, `set_insert`, `set_remove`, `set_contains`, `set_size`, `set_elements`, `set_union`, `set_intersection`, `set_difference`, `set_fold`, `list_fold`, `iterate`, `iterate_until`, `graph_successors`, `graph_reachable`, and `graph_topological`, under the collection rules below. |
 | `less_than` primitive | `lexlean/semantic-module/2` | `{"kind":"primitive","operation":"less_than","arguments":[a,b],"result":{"kind":"bool"}}` over two values of one ordered key type (rule 1 under *Collections and state threading*): `true` exactly when `a` precedes `b` in that type's fixed order. It lowers to `LexLeanCollections.lessThan`. |
+| `to_int`, `to_nat` primitives | `lexlean/semantic-module/2` | `{"kind":"primitive","operation":"to_int","arguments":[v],"result":{"kind":"int"}}` over any fixed-width integer `v` (`int8`..`int64`, `uint8`..`uint64`), and `{"kind":"primitive","operation":"to_nat","arguments":[v],"result":{"kind":"nat"}}` over any unsigned fixed-width integer `v` (`uint8`..`uint64`), under the widening-conversion rules below. |
 | `artifact` declaration | `lexlean/semantic-module/2` | A typed constant decoded from content-addressed project bytes, under the model rules below. |
 | `contract` declaration | `lexlean/semantic-module/2` | Typed input, output, and optional state interfaces, proposition-valued predicates, and their runtime validators, under the model rules below. |
 | `realization` declaration | `lexlean/semantic-module/2` | A deterministic, rule, statistical, neural, or composite denotation of an interface, under the model rules below. |
@@ -3598,6 +3599,32 @@ proved correct on every state its run reaches, with its check erased, all
 verified by pinned Lean, with the six-counter ledger of each run decided
 counter by counter by Lean's kernel.
 
+#### Widening conversions (language 1.2)
+
+1. **Typing.** `to_int` takes one operand of a fixed-width integer type
+   (`Int8`, `Int16`, `Int32`, `Int64`, `UInt8`, `UInt16`, `UInt32`, or
+   `UInt64`) and has result `Int`. `to_nat` takes one operand of an unsigned
+   fixed-width integer type (`UInt8`, `UInt16`, `UInt32`, or `UInt64`) and has
+   result `Nat`. Any other operand type, result type, or argument count is
+   rejected in linking (`LLT4001`) before either backend runs.
+2. **Elaboration.** A widening conversion is a total, exact conversion of its
+   operand's value. Linking elaborates each application into an ordinary
+   language-1.2 term before Lean rendering, production eligibility, or
+   production lowering runs: the operand is bound once to a generated local
+   `__widen<n>` (`n` counted in evaluation order within each declaration),
+   each bit $k$ of the width is tested with `bit_and` and `equal` against the
+   fixed-width mask $2^k$, and the bit weights are summed in a balanced tree
+   over `Int` (`subtract` and `negate`, with the sign bit of a signed width
+   weighted by $-2^{w-1}$ and bit 63 of `UInt64` expressed as $2^{62} + 2^{62}$
+   so every literal lies within 64-bit signed range) or over `Nat` (`add`).
+   Generated Lean, production eligibility, production lowering, and the
+   preservation certificates read the elaborated declaration, so a root that
+   indexes a `Bytes` value and widens the resulting `UInt8` lowers to bit
+   tests and exact sums with no decimal text (`parse_decimal` or
+   `format_decimal`). The canonical LaTeX document renders the source
+   conversion (`toInt`, `toNat`), and the snapshot records the declaration's
+   `elaboration` alongside the source declaration (`SM-32`).
+
 Routing is fixed by the project language and is never inferred from module
 content, so no byte sequence has two meanings:
 
@@ -5320,8 +5347,8 @@ root's crate. Every root whose closure declares an overflow is run on an input
 on which it overflows, so the overflow arm of each statement is exercised on
 the interpreter, Lean, the machine, and rustc, except the roots below, whose
 declared overflow no input reaches (the registry's effect rows
-over-approximate). Of the 57 certified roots of the four examples, 42
-declare an overflow, 19 of them reach it, and the other 23 rest on the
+over-approximate). Of the 59 certified roots of the four examples, 44
+declare an overflow, 19 of them reach it, and the other 25 rest on the
 kernel proof alone for the overflow arm of E, B, and the machine, because
 either the operands that can overflow do not depend on the root's parameters,
 or the overflow is a sequence, text, or collection of 2^64 elements, which no
@@ -5341,6 +5368,8 @@ Coverage.Main.natOps
 Coverage.Prims.sequences
 Coverage.Prims.decimals
 Coverage.Prims.text
+Coverage.Prims.widenings
+Coverage.Prims.pixels
 Coverage.RecRoots.roseTotal
 Coverage.RecRoots.syntaxTotal
 Coverage.RecRoots.wellFounded
@@ -5753,12 +5782,12 @@ LexLean refuses as production roots (`production-polymorphic-root`,
 `production-named-type-boundary`, and `production-universe-boundary`), with the
 production marking removed so that LexLean still compiles them to Lean. LexLean's
 verdict on a rejection project is the diagnostic its fixture records.
-The corpus has 102 roots; the oracle generates Rust for 30 of them and
-refuses 72; 23 of the crates it generates for eligible roots compile and are
+The corpus has 104 roots; the oracle generates Rust for 30 of them and
+refuses 74; 23 of the crates it generates for eligible roots compile and are
 run on 1411 inputs, and each of the other seven is a recorded difference (six
 crates that rustc rejects, and the crate of the rejected root with the
-literal beyond 64 bits). Of the 72 refusals, 66 are of roots LexLean takes
-(42 `escaping-local-function`, 13 `opaque-lowering`, 4
+literal beyond 64 bits). Of the 74 refusals, 68 are of roots LexLean takes
+(42 `escaping-local-function`, 13 `opaque-lowering`, 6
 `unresolved-external-call`, 3 `codegen-PolymorphicType`, 2
 `codegen-UnboundedInt`, 2 `codegen-UnresolvedCall`) and 6 of roots LexLean
 rejects (4 `opaque-lowering`, 1 `export-refused`, 1 `codegen-OpaqueType`; the
@@ -8955,6 +8984,7 @@ Every row below is normative, has honesty level `build`, and MUST be copied byte
 | `SM-29` | `semantic-ir` | Reordered equivalent map, set, and graph literals link to byte-identical semantic data and generated Lean, LaTeX, and lexicon-closure artifacts, while duplicate keys, non-literal literal keys, and key types without a canonical order are rejected. | §17.12, §21 |
 | `SM-30` | `semantic-ir` | 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. | §17.12 |
 | `SM-31` | `semantic-ir` | 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. | §17.10 |
+| `SM-32` | `semantic-ir` | Language 1.2 widening conversions, to_int from every fixed-width integer type to Int and to_nat from every unsigned fixed-width type to Nat, are total, are rejected under language 1.1, and elaborate in linking to ordinary terms over bit_and, equal, conditionals, and exact integer and natural sums, so that a production root decodes a byte string to integers with no decimal text in its lowered program and is certified like any other root. | §17.12 |
 | `DF-01` | `declarations` | A valid type-definition sentence emits one nonrecursive sort-valued Lean def linked to its document entry. | §15.7, §18.6 |
 | `DF-02` | `declarations` | A valid term-definition sentence emits one nonrecursive explicitly typed Lean def. | §15.7, §18.6 |
 | `DF-03` | `declarations` | A valid predicate-definition sentence emits one nonrecursive Prop-valued Lean def. | §15.7, §18.6 |
@@ -9228,7 +9258,7 @@ Every row below is normative, has honesty level `build`, and MUST be copied byte
 | `AU-11` | `authoring` | Malformed core notation fails closed and never panics: an unclosed delimiter, a keyword used as a name, a label that is not the number of its node, a reference to a node not yet written, a numeral with a redundant leading zero, a statement that defines no node, a nesting beyond the bound, and every single-token deletion and duplication of a committed module fail with a registered code at a position in the notation or link to a module that decodes. | §17.21.8 |
 | `AU-12` | `authoring` | A core module written with names for its statements and its variables reads to exactly the module its canonical notation reads to, and the canonical notation keeps the names of the binders and writes the numbers of the statements: a variable is written by the name of its binder exactly when no nearer binder has the name, a constant a binder in scope is named like is written as a string, a theorem added to the certification library by name reads to the committed module and is written as the committed bytes, and an unknown or repeated statement name and a variable given universe levels are refused with a position. | §17.21.8 |
 
-**Total required capability IDs:** 382.
+**Total required capability IDs:** 383.
 
 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

@@ -7778,3 +7778,34 @@ 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.
+
+### byte-to-fixed-width widening conversions in language 1.2 (`SM-32`, #114)
+
+Language 1.2 adds the total widening primitives `to_int` (any fixed-width
+integer to `Int`) and `to_nat` (any unsigned fixed-width integer to `Nat`),
+elaborated in linking to bit tests (`bit_and`, `equal`) and balanced sums over
+`Int` or `Nat` under a generated `__widen<n>` binding so that Lean
+verification, production eligibility, production lowering, and certificates A,
+B, and E operate on the ordinary elaborated terms without decimal formatting or
+parsing (`Coverage.Prims.widenings` and `Coverage.Prims.pixels`).
+
+- **sign bit of a signed width added instead of subtracted.** `bit_contribution`
+  in `ir::semantic::widen` weights the top bit of a signed integer by $+2^{w-1}$
+  instead of $-2^{w-1}$. `-- conformance_sm_32`:
+
+  ```text
+  panicked at crates/conformance/src/support.rs:2151:10:
+  the module verifies with real Lean: LexLeanError { class: Language, diagnostics: [Diagnostic { code: DiagnosticCode("LLV7002"), message: "lean failed in phase `LanguageTwelve.Main` (exitSome(1)): ..." }] }
+  ```
+
+- **signed operand accepted by `to_nat`.** `infer_primitive` admits `ToNat` on
+  any `is_fixed_integer()` operand instead of `is_unsigned_fixed_integer()`.
+  `-- conformance_sm_32`:
+
+  ```text
+  panicked at crates/conformance/src/support.rs:607:14:
+  check fails with LLT4001: ()
+  ```
+
+Removed: both edits were restored; `conformance_sm_32` and the unit tests of
+`ir::semantic::widen` pass.