feat(m1): implement bounded shortest ULEB128 with kernel-checked proofs

CONFORMANCE.md

@@ -37,6 +37,12 @@ The three honesty levels (R2):
 | `UC-PERF-01` | `open` | measured public-corpus compression improvement, with exact target and scope; open until actually measured |
 | `UC-REC-01` | `open` | externally accepted compression record; open unless the external authority actually accepts it |
 
+## varint
+
+| ID | Level | Statement |
+| --- | --- | --- |
+| `UC-VAR-01` | `build` | Shortest U64 ULEB128 encoding and strict decoding have source-owned domain and rejection rules, complete boundary vectors, and kernel-checked round-trip and size theorems. |
+
 ## Cited authorities
 
 | Authority | Citation | Evidence here |
@@ -54,3 +60,4 @@ The three honesty levels (R2):
 | `UC-REP-02` | `build` | `build_evidence` | `not_measured` | Dependency and execution-boundary failures are explicit and planted SDK-lock, source-lock, adjacent-checkout, and host-PATH fallbacks are rejected. |
 | `UC-HON-01` | `build` | `build_evidence` | `not_measured` | Evidence classes and research dispositions remain distinct in the LexLean claim policy. |
 | `UC-HON-02` | `build` | `build_evidence` | `not_measured` | The honesty ledger and claim summaries are exact source projections with open research claims protected against promotion. |
+| `UC-VAR-01` | `build` | `kernel_theorem` | `not_measured` | Shortest U64 ULEB128 encoding and strict decoding have source-owned domain and rejection rules, complete boundary vectors, and kernel-checked round-trip and size theorems. |

Justfile

@@ -3,7 +3,7 @@
 default: vv
 
 # The whole gate.
-vv: lexlean-authority template-check fmt-check model lint test features bdd deny lexlean-artifacts claim-dispositions reproducibility
+vv: lexlean-authority template-check fmt-check model lint test features bdd deny lexlean-artifacts claim-dispositions varint-proofs reproducibility
     @echo "vv: the acceptance gate passed"
 
 # The UORC authority files are real LexLean source, not merely files with a
@@ -80,3 +80,7 @@ claim-dispositions:
 # This invokes model/build/verify in clean roots, never recursively `just vv`.
 reproducibility:
     node scripts/offline-validation.mjs reproduce
+
+# Actual core-source defects must fail at their owning kernel declarations.
+varint-proofs:
+    node scripts/varint-validation.mjs

README.md

@@ -7,7 +7,7 @@ A lossless compression system whose compressed object is an exact executable Uni
 
 ## Current status
 
-This repository establishes the charter, source-authority, and claim-disposition slices represented by its registered conformance rows. Compression behavior, losslessness, optimality certificates, benchmark superiority, and record status are not established by these slices.
+This revision implements the charter, source-authority, claim-disposition, and bounded U64 ULEB128 slices in the LexLean graph. The codec has kernel-checked round-trip, shortest-length, exact-size, and prefix-consumption properties. Full archive, machine, search, and production-product acceptance remain separate registered work; performance and record claims remain open.
 
 ## Authority
 
@@ -57,6 +57,9 @@ This table classifies evidence within its verified scope. It does not validate a
 - `UC-PERF-01`: `not_measured`; evidence `none`; honesty level `open`.
 - `UC-REC-01`: `not_measured`; evidence `none`; honesty level `open`.
 
+The source-owned bounded ULEB128 codec, errors, and proof inventory are projected in [UORC-VARINT.md](UORC-VARINT.md).
+
+
 ## Evidence and dependency boundaries
 
 | Class | Boundary |

UORC-VARINT.md

@@ -0,0 +1,59 @@
+<!-- @generated from the UORC LexLean authority graph. -->
+# UORC ULEB128 contract
+
+## authority
+
+The native core declarations, computational definitions, and proof terms in Uorc.Varint are LexLean source. Verification reconstructs them from the source graph without any handwritten Lean file or precompiled product object as an input.
+
+## axiomPolicy
+
+Computational entry points have empty axiom sets. Proof declarations carry their exact kernel-audited subset of Lean foundations propext, Quot.sound, and Classical.choice. No additional axiom or admitted proof is allowed.
+
+## decoding
+
+Prefix decoding consumes at most ten bytes and returns the numeric value, consumed length, and untouched suffix. Exact decoding additionally rejects any suffix. The prefix is accepted only if the bounded encoder reproduces its exact bytes.
+
+## domain
+
+Unsigned 64-bit integers: natural values from 0 through 18446744073709551615. The public encoder rejects larger values before encoding. Byte inputs are natural values checked against 0..255.
+
+## encoding
+
+Shortest unsigned little-endian base-128 encoding. Each non-final byte carries seven payload bits and sets bit 7; the final byte clears bit 7. Zero is the single byte 00. A successful U64 encoding occupies one through ten bytes.
+
+## errorOrder
+
+At each consumed byte: exhausted ten-byte allowance, absent byte, invalid byte domain, then termination/continuation. After termination: U64 overflow, non-shortest spelling, then (for exact decoding) trailing bytes. Prefix decoding does not inspect suffix bytes.
+
+## offsets
+
+Offsets are zero-based relative to the varint start. Truncation identifies the first missing byte; an invalid byte identifies itself; overflow or non-shortest spelling identifies the final consumed byte; trailing bytes identify the first unconsumed byte; encoder domain rejection uses offset zero.
+
+## proofScope
+
+The two public round trips quantify over all domain values or all accepted inputs. Additional theorems establish exact size, a one-to-ten-byte bound, minimum possible base-128 representation length, and preservation of prefix/suffix concatenation. Closed vectors are separate exact observations.
+
+## Typed failures
+
+| Variant | Meaning | Negative family |
+| --- | --- | --- |
+| `truncated` | Input ends before a terminating byte. | `truncated_` |
+| `overflow` | The ten-byte allowance or U64 numeric range is exceeded. | `overflow_` |
+| `nonShortest` | The consumed bytes are not the shortest spelling of their value. | `overlong_` |
+| `invalidByte` | A consumed input element is outside the byte domain. | `invalid_byte_` |
+| `trailingBytes` | Exact decoding finds a suffix after a valid prefix. | `trailing_` |
+| `valueOutOfRange` | The encoder input is outside the U64 domain. | `encode_overflow_` |
+
+## General kernel roots
+
+- `Uorc.Varint.uleb_encode_decode`
+- `Uorc.Varint.uleb_decode_encode`
+- `Uorc.Varint.uleb_size_exact`
+- `Uorc.Varint.uleb_size_bounded`
+- `Uorc.Varint.shortest`
+- `Uorc.Varint.scan_reconstruct`
+- `Uorc.Varint.chunk_encode`
+- `Uorc.Varint.fuel_eq`
+- `Uorc.Varint.bounded_eq`
+
+236 closed vector theorems are inventoried in `model/varint.toml`.

UORC-VERIFICATION.md

@@ -8,7 +8,7 @@ authority graph. It does not replace the template-owned `VERIFICATION.md`.
 
 ## Current status
 
-This repository establishes the charter, source-authority, and claim-disposition slices represented by its registered conformance rows. Compression behavior, losslessness, optimality certificates, benchmark superiority, and record status are not established by these slices.
+This revision implements the charter, source-authority, claim-disposition, and bounded U64 ULEB128 slices in the LexLean graph. The codec has kernel-checked round-trip, shortest-length, exact-size, and prefix-consumption properties. Full archive, machine, search, and production-product acceptance remain separate registered work; performance and record claims remain open.
 
 ## Claim boundaries
 
@@ -42,6 +42,9 @@ This table classifies evidence within its verified scope. It does not validate a
 - `UC-PERF-01`: `not_measured`; evidence `none`; honesty level `open`.
 - `UC-REC-01`: `not_measured`; evidence `none`; honesty level `open`.
 
+The source-owned bounded ULEB128 codec, errors, and proof inventory are projected in [UORC-VARINT.md](UORC-VARINT.md).
+
+
 ## Evidence and dependency boundaries
 
 | Class | Boundary |

crates/model/src/authority.rs

@@ -113,6 +113,8 @@ pub struct ScenarioProjection {
 /// The complete project-owned authority graph needed by the repository model.
 #[derive(Debug, Clone)]
 pub struct AuthorityGraph {
+    /// Source-owned bounded varint contract and kernel inventory.
+    pub varint: crate::varint::VarintContract,
     /// Product charter.
     pub charter: Charter,
     /// Claim-class distinctions.
@@ -138,6 +140,7 @@ pub struct AuthorityGraph {
 impl AuthorityGraph {
     /// Load and structurally validate the LexLean authority modules.
     pub fn load(root: &Path) -> Result<Self, ModelError> {
+        let varint = crate::varint::VarintContract::load(root)?;
         let specification =
             semantic_declarations(&root.join(SPECIFICATION_PATH), "Uorc.Specification")?;
         let registry = semantic_declarations(&root.join(REGISTRY_PATH), "Uorc.Registry")?;
@@ -263,6 +266,7 @@ impl AuthorityGraph {
         }
 
         let graph = Self {
+            varint,
             charter: Charter {
                 product_name: required(&charter, "productName")?,
                 purpose: required(&charter, "purpose")?,

crates/model/src/codegen.rs

@@ -30,6 +30,14 @@ pub fn render_all(graph: &AuthorityGraph) -> Vec<(String, String)> {
         (IDS_PATH.to_string(), render_ids(&model)),
         (AUTHORITIES_PATH.to_string(), render_authorities(&model)),
         (LEDGER_PATH.to_string(), render_ledger(&model)),
+        (
+            "model/varint.toml".to_string(),
+            format!(
+                "# @generated from the UORC LexLean varint graph; do not edit.\n{}",
+                toml::to_string_pretty(&graph.varint).expect("serializable varint contract")
+            ),
+        ),
+        ("UORC-VARINT.md".to_string(), render_varint(graph)),
         (
             "model/claim-policy.toml".to_string(),
             format!(
@@ -48,6 +56,36 @@ pub fn render_all(graph: &AuthorityGraph) -> Vec<(String, String)> {
     out
 }
 
+fn render_varint(graph: &AuthorityGraph) -> String {
+    let mut out = String::from(
+        "<!-- @generated from the UORC LexLean authority graph. -->\n# UORC ULEB128 contract\n\n",
+    );
+    for (name, text) in &graph.varint.contract {
+        let _ = writeln!(out, "## {name}\n\n{text}\n");
+    }
+    let _ = writeln!(
+        out,
+        "## Typed failures\n\n| Variant | Meaning | Negative family |\n| --- | --- | --- |"
+    );
+    for row in &graph.varint.failure {
+        let _ = writeln!(
+            out,
+            "| `{}` | {} | `{}` |",
+            row["variant"], row["meaning"], row["negativeFamily"]
+        );
+    }
+    let _ = writeln!(out, "\n## General kernel roots\n");
+    for name in &graph.varint.theorem {
+        let _ = writeln!(out, "- `{name}`");
+    }
+    let _ = writeln!(
+        out,
+        "\n{} closed vector theorems are inventoried in `model/varint.toml`.",
+        graph.varint.vector.len()
+    );
+    out
+}
+
 fn render_feature_suites(graph: &AuthorityGraph) -> Vec<(String, String)> {
     let mut suites = graph
         .scenarios
@@ -345,6 +383,7 @@ pub fn render_readme(graph: &AuthorityGraph) -> String {
 
     render_claim_table(&mut out, graph);
     render_dispositions(&mut out, graph);
+    let _ = writeln!(out, "\nThe source-owned bounded ULEB128 codec, errors, and proof inventory are projected in [UORC-VARINT.md](UORC-VARINT.md).\n");
     render_evidence_table(&mut out, graph);
 
     let r = &graph.research_position;
@@ -414,6 +453,7 @@ pub fn render_project_verification(graph: &AuthorityGraph) -> String {
 
     render_claim_table(&mut out, graph);
     render_dispositions(&mut out, graph);
+    let _ = writeln!(out, "\nThe source-owned bounded ULEB128 codec, errors, and proof inventory are projected in [UORC-VARINT.md](UORC-VARINT.md).\n");
     render_evidence_table(&mut out, graph);
 
     let _ = writeln!(out);

crates/model/src/lib.rs

@@ -14,6 +14,7 @@ pub mod authority;
 pub mod claims;
 pub mod codegen;
 pub mod registry;
+pub mod varint;
 
 pub use authority::AuthorityGraph;
 pub use claims::ClaimPolicy;