fix(backend): lower explicit shared byte literals without widening limits

VERIFICATION.md

@@ -254,6 +254,55 @@ retains the original accepted identifier language and all source-audit
 prohibitions. Raw logs are retained under ignored
 `target/semantic-reserved-identifiers-{lean-red,complete-variants,mutant}.log`.
 
+### explicit byte-literal lowering can fail
+
+A modeled byte literal used to be written `ByteArray.mk #[n, ...]`. It is now
+written `_root_.ByteArray.mk #[...]` with every octet an explicit
+`_root_.UInt8.ofNat (nat_lit n)`; an octet occurring four or more times in one
+literal is bound once by a `let __byteN` local to that literal, so no generated
+local outside the literal takes part in its meaning. The canonical document
+keeps the original decimal numbers and order. SM-19, for languages 1.1 and 1.2,
+reads every generated literal back with an independent closed-grammar reader
+(it neither evaluates Lean nor calls the renderer), checks the document
+display, verifies, and evaluates the generated definitions against the
+original bytes. MD-02 applies the same reader to every embedded artifact byte.
+The reader's own controls refuse foreign, noncanonical and unused syntax, and
+a binding name that disagrees with its value.
+
+Observed before the change: with the lowerer of `main` `243f0c734` unchanged,
+`conformance_sm_19` fails at its first fixture, the empty array, with
+`closed explicit-octet lowering: "expected closed byte syntax \"_root_.ByteArray.mk #[\""`.
+That is the reader rejecting the old spelling. It is not a Lean failure: the
+largest SM-19 corpus (1024 bytes, all 256 values) elaborates under `main`'s
+rendering at the default `maxRecDepth` (1.1 s; 0.8 s explicit).
+
+Measured, not claimed as an improvement beyond these numbers: Lean 4.32.1
+(x86-64 Linux, 4 cores, one run each) on a file holding one `public def` of a
+seeded-random byte literal in which all 256 values occur.
+
+| bytes | `maxRecDepth` | `main` rendering | explicit rendering |
+| --- | --- | --- | --- |
+| 4096 | 100000 | 3.0 s, ok | 2.1 s, ok |
+| 4096 | default | 2.6 s, ok | 2.3 s, ok |
+| 16384 | 100000 | 12.7 s, ok | 11.3 s, ok |
+| 16384 | default | 10.8 s, recursion depth | 8.9 s, recursion depth |
+| 65536 | 100000 | 37.1 s, heartbeats (`isDefEq`) | 49.2 s, heartbeats (`LCNF compiler`) |
+| 65536 | default | 33.3 s, heartbeats (`isDefEq`) | 42.7 s, recursion depth |
+
+Bisection at the default `maxRecDepth` (no `set_option`), by 16-byte steps
+between 1024 and 16384 bytes, one run per size, seeded-random bytes with all 256
+values present: the largest literal that elaborates is 6394 bytes under both
+renderings, and 6409 bytes fails under both (`maximum recursion depth has been
+reached`). Elaboration time at 4096 bytes is 2.0 s under both; at 6394 bytes it
+is 4.4 s for the `main` rendering and 3.3 s for the explicit one. The lowering
+does not move the largest elaborable literal.
+
+No size succeeds under one rendering and fails under the other. Both fail at
+16384 bytes at the default depth and at 65536 bytes at either depth; the
+explicit form is faster at 4096 and 16384 bytes and slower at 65536. The
+timing script is not committed; it writes the two spellings above for the
+same seeded bytes and runs `lean` on the file.
+
 ### native diagnostic detail can fail
 
 `CL-21` was registered before its named test failed on the unwired case.

crates/conformance/src/cases/models.rs

@@ -535,6 +535,97 @@ fn check_wide_artifact(root: &camino::Utf8Path) {
     );
 }
 
+// Decode the closed generated expression independently of the renderer. An
+// exact octet comparison must survive literal-local sharing, not accept an
+// opaque expression or merely find the bytes somewhere in the module.
+fn embedded_artifact_octets(lean: &str, name: &str) -> Vec<u8> {
+    let prefix = format!("@[expose] public def {name}.bytes : ByteArray := ");
+    let expressions = lean
+        .lines()
+        .filter_map(|line| line.strip_prefix(&prefix))
+        .collect::<Vec<_>>();
+    assert_eq!(expressions.len(), 1, "one exact artifact definition");
+    let mut expression = expressions[0];
+    if expression.starts_with('(') {
+        expression = expression
+            .strip_prefix('(')
+            .and_then(|value| value.strip_suffix(')'))
+            .expect("closed literal-local expression");
+    }
+    let octet = |text: &str| {
+        let value = text.parse::<u8>().expect("bounded octet");
+        assert_eq!(text, value.to_string(), "canonical octet");
+        value
+    };
+    let mut bindings = std::collections::BTreeMap::new();
+    while expression.starts_with("let ") {
+        let (binding, rest) = expression.split_once("; ").expect("local separator");
+        let (name, value) = binding
+            .strip_prefix("let __byte")
+            .and_then(|value| value.split_once(" : _root_.UInt8 := _root_.UInt8.ofNat (nat_lit "))
+            .expect("closed octet binding");
+        let name = octet(name);
+        let value = octet(value.strip_suffix(')').expect("closed octet value"));
+        assert_eq!(name, value, "local name binds its own octet");
+        assert!(bindings.insert(name, value).is_none(), "unique local");
+        expression = rest;
+    }
+    let contents = expression
+        .strip_prefix("_root_.ByteArray.mk #[")
+        .and_then(|value| value.strip_suffix(']'))
+        .expect("closed byte array constructor");
+    if contents.is_empty() {
+        return Vec::new();
+    }
+    contents
+        .split(", ")
+        .map(|item| {
+            if let Some(name) = item.strip_prefix("__byte") {
+                *bindings.get(&octet(name)).expect("literal-local binding")
+            } else {
+                let value = item
+                    .strip_prefix("(_root_.UInt8.ofNat (nat_lit ")
+                    .and_then(|value| value.strip_suffix("))"))
+                    .expect("closed explicit octet");
+                octet(value)
+            }
+        })
+        .collect()
+}
+
+#[test]
+fn artifact_octet_oracle_rejects_opaque_unbound_and_forged_literals() {
+    let definition = |expression: &str| {
+        format!("@[expose] public def artifact.bytes : ByteArray := {expression}\n")
+    };
+    let direct = "_root_.ByteArray.mk #[(_root_.UInt8.ofNat (nat_lit 0)), (_root_.UInt8.ofNat (nat_lit 255))]";
+    assert_eq!(
+        embedded_artifact_octets(&definition(direct), "artifact"),
+        [0, 255]
+    );
+    let shared = "(let __byte0 : _root_.UInt8 := _root_.UInt8.ofNat (nat_lit 0); _root_.ByteArray.mk #[__byte0, __byte0])";
+    assert_eq!(
+        embedded_artifact_octets(&definition(shared), "artifact"),
+        [0, 0]
+    );
+    assert_eq!(
+        embedded_artifact_octets(&definition("_root_.ByteArray.mk #[]"), "artifact"),
+        Vec::<u8>::new()
+    );
+    for expression in [
+        "opaqueArtifact",
+        "_root_.ByteArray.mk #[__byte0]",
+        "_root_.ByteArray.mk #[(_root_.UInt8.ofNat (nat_lit 256))]",
+        "_root_.ByteArray.mk #[(_root_.UInt8.ofNat (nat_lit 00))]",
+        "(let __byte0 : _root_.UInt8 := _root_.UInt8.ofNat (nat_lit 1); _root_.ByteArray.mk #[__byte0])",
+        "(let __byte0 : _root_.UInt8 := _root_.UInt8.ofNat (nat_lit 0); let __byte0 : _root_.UInt8 := _root_.UInt8.ofNat (nat_lit 0); _root_.ByteArray.mk #[__byte0])",
+    ] {
+        assert!(std::panic::catch_unwind(|| embedded_artifact_octets(&definition(expression), "artifact")).is_err());
+    }
+    let duplicate = definition(direct) + &definition(direct);
+    assert!(std::panic::catch_unwind(|| embedded_artifact_octets(&duplicate, "artifact")).is_err());
+}
+
 fn md_02() {
     if let Ok(root) = std::env::var(WIDE_ARTIFACT_PROJECT) {
         check_wide_artifact(camino::Utf8Path::new(&root));
@@ -570,14 +661,7 @@ fn md_02() {
     let lean = support::lean_text(&build, "Recognizer");
     let banner = std::fs::read(project.root.join("artifacts/banner.bin").as_std_path())
         .expect("banner bytes");
-    let embedded = banner
-        .iter()
-        .map(u8::to_string)
-        .collect::<Vec<_>>()
-        .join(", ");
-    assert!(lean.contains(&format!(
-        "public def banner.bytes : ByteArray := ByteArray.mk #[{embedded}]"
-    )));
+    assert_eq!(embedded_artifact_octets(&lean, "banner"), banner);
     assert!(lean.contains("public theorem banner.decoded : banner = banner.bytes := rfl"));
     let weights = std::fs::read(
         project
@@ -591,9 +675,7 @@ fn md_02() {
         .map(u8::to_string)
         .collect::<Vec<_>>()
         .join(", ");
-    assert!(lean.contains(&format!(
-        "public def hiddenWeights.bytes : ByteArray := ByteArray.mk #[{embedded}]"
-    )));
+    assert_eq!(embedded_artifact_octets(&lean, "hiddenWeights"), weights);
     assert!(lean.contains(
         "public theorem hiddenWeights.decoded : (LexLeanModels.tensorMatches 1 true hiddenWeights.flatten hiddenWeights.bytes && (hiddenWeights.length == 12) && (hiddenWeights.map List.length == List.replicate 12 7)) = true := by decide"
     ));

crates/conformance/src/cases/semantic_ir.rs

@@ -7,6 +7,7 @@ use sha2::Digest;
 
 use crate::support::{self, P};
 
+mod bytes;
 mod names;
 mod strings;
 
@@ -140,25 +141,8 @@ fn verify_large_byte_declaration(varied: bool) {
     );
     let rendered = support::rendered(&project);
     let generated = support::lean_text(&rendered, "Main");
-    let emitted: Vec<_> = generated
-        .split("ByteArray.mk #[")
-        .skip(1)
-        .map(|tail| {
-            let literal = tail.split_once(']').expect("closed generated array").0;
-            if literal.is_empty() {
-                return String::new();
-            }
-            literal
-                .split(", ")
-                .map(|value| {
-                    format!(
-                        "{:02x}",
-                        value.parse::<u8>().expect("exact generated UInt8 literal")
-                    )
-                })
-                .collect::<String>()
-        })
-        .collect();
+    let emitted = bytes::emitted_literals(&generated)
+        .expect("every generated byte literal has the closed explicit-octet grammar");
     assert_eq!(
         emitted, expected,
         "the actual generated declaration retains every byte in order"
@@ -1097,6 +1081,7 @@ pub(crate) fn run(id: &str) {
             );
         }
         "SM-19" => {
+            bytes::verify();
             strings::verify();
             names::verify();
             verify_large_byte_declaration(false);