fix(#154): the runtime gates read what they claim to

CHANGELOG.md

@@ -15,6 +15,19 @@ versions, and the entries below say what each tag does and does not claim.
 
 ## Unreleased
 
+- The runtime gates read what they claimed to (#154, follow-up to #144; no new
+  diagnostic code, no new ID). `RT-04` finds a Lean runtime text in any string
+  literal of the compiler's source outside unit-test items, in production code
+  after a test module, with or without a `namespace` line (a declaration
+  under a runtime name is one), written whole or in literals joined by
+  `concat!`, an array, `+` or `format!`; its statement now also asserts
+  what it said of generated modules: every committed language-1.2 module
+  imports the runtime modules whose constants it names and declares nothing
+  under a runtime namespace. `RT-02` recomputes the compiler-semantics IDs
+  with each frozen file changed (1.0 and 1.1 unchanged, 1.2 changed). `RT-03`
+  plants the second direction of the axiom check. Every directory that holds a
+  `CACHEDIR.TAG` is skipped by the repository walkers, so a build directory
+  beside the sources no longer reads as source. No compiled behavior changes.
 - UOR Atlas is verified in CI as the parts of one run (SPEC.md §9.4, §22.11,
   `RP-14`, `VR-23`, #131; no new diagnostic code). The examples leg, 178
   minutes on `main` at 514e95ad (CI run 38716449420), was 156 minutes of

CONFORMANCE.md

@@ -438,7 +438,7 @@ the error registry does not sanction (R5, `ERRORS.md`).
 | `RT-01` | `build` | The runtime of language 1.2 is LexLean source: every module of its registry is one native core module of the runtime's own project, which holds no file of Lean source, the registry lists only the modules in dependency order, every declaration pins its exact axioms, and a source that is missing, weakened to an inexact policy, or imports anything but `Init` and an earlier runtime module is refused; the one-time migration input is absent, no native source names a runtime copy inside a module, and no Lean file declares a runtime namespace but the released output of a language-1.0 or 1.1 project. |
 | `RT-02` | `build` | The runtime text of languages 1.0 and 1.1 is the one declared exception: the portable runtime and the decoder of core module 1 are the released bytes, held as data under `language/runtime-1.2/frozen/`, read by the language-1.0 and 1.1 backends alone, excluded from the language-1.0 and 1.1 identities, and reproduced byte for byte by the released language-1.1 and 1.0 output; a one-byte change of either is not the released output. |
 | `RT-03` | `build` | A verification compiles every runtime module that a project's generated modules, or the calculus modules its certificates are checked against, import before the project's modules, replays it with `leanchecker`, and audits each of its declarations against the axioms its row pins; the committed verification of a project that uses the collections prints them, the runtime's own project verifies under the pinned Lean, and a row that pins another axiom set than its declaration observes fails with LLV7005. |
-| `RT-04` | `build` | No Lean runtime text remains in the language-1.2 compiler: a generated language-1.2 module imports the runtime modules it uses and splices none, and the only string literal of the compiler's source that holds Lean declarations under a namespace is the decoder of core module 2, which loads native modules and so cannot be one; a planted runtime text constant, raw or escaped, is found. |
+| `RT-04` | `build` | No Lean runtime text remains in the language-1.2 compiler: a generated language-1.2 module imports the runtime modules whose constants it names and declares nothing under a runtime namespace, and the only Lean runtime text in the compiler's source outside unit-test items, in one string literal or in several written together, is the decoder of core module 2, which loads native modules and so cannot be one; a runtime text planted in any of its shapes, raw or escaped, with or without a namespace line, split across literals, or after a test module, is found. |
 
 ## rust-backend
 

SPEC.md

@@ -9279,7 +9279,7 @@ Every row below is normative, has honesty level `build`, and MUST be copied byte
 | `RT-01` | `runtime` | The runtime of language 1.2 is LexLean source: every module of its registry is one native core module of the runtime's own project, which holds no file of Lean source, the registry lists only the modules in dependency order, every declaration pins its exact axioms, and a source that is missing, weakened to an inexact policy, or imports anything but `Init` and an earlier runtime module is refused; the one-time migration input is absent, no native source names a runtime copy inside a module, and no Lean file declares a runtime namespace but the released output of a language-1.0 or 1.1 project. | §17.12 |
 | `RT-02` | `runtime` | The runtime text of languages 1.0 and 1.1 is the one declared exception: the portable runtime and the decoder of core module 1 are the released bytes, held as data under `language/runtime-1.2/frozen/`, read by the language-1.0 and 1.1 backends alone, excluded from the language-1.0 and 1.1 identities, and reproduced byte for byte by the released language-1.1 and 1.0 output; a one-byte change of either is not the released output. | §17.12, §21.2 |
 | `RT-03` | `runtime` | A verification compiles every runtime module that a project's generated modules, or the calculus modules its certificates are checked against, import before the project's modules, replays it with `leanchecker`, and audits each of its declarations against the axioms its row pins; the committed verification of a project that uses the collections prints them, the runtime's own project verifies under the pinned Lean, and a row that pins another axiom set than its declaration observes fails with LLV7005. | §17.12, §22.3, §22.5, §22.6 |
-| `RT-04` | `runtime` | No Lean runtime text remains in the language-1.2 compiler: a generated language-1.2 module imports the runtime modules it uses and splices none, and the only string literal of the compiler's source that holds Lean declarations under a namespace is the decoder of core module 2, which loads native modules and so cannot be one; a planted runtime text constant, raw or escaped, is found. | §17.12, §18.1 |
+| `RT-04` | `runtime` | No Lean runtime text remains in the language-1.2 compiler: a generated language-1.2 module imports the runtime modules whose constants it names and declares nothing under a runtime namespace, and the only Lean runtime text in the compiler's source outside unit-test items, in one string literal or in several written together, is the decoder of core module 2, which loads native modules and so cannot be one; a runtime text planted in any of its shapes, raw or escaped, with or without a namespace line, split across literals, or after a test module, is found. | §17.12, §18.1 |
 
 **Total required capability IDs:** 387.
 

VERIFICATION.md

@@ -7818,6 +7818,88 @@ error[LLV7005]: `LexLeanCollections.insertEntry` of the runtime module `LexLeanR
 
 Removed: each file was restored, and `RT-01`..`RT-04` pass on the restored
 tree.
+
+### the runtime gates, read again (Issue #154)
+
+`RT-04` had cut each compiler source at its first `#[cfg(test)]`, asked a
+literal for a `namespace` line and a declaration, and read one literal at a
+time; #154 reproduced a text that passed. Each shape below is now planted on
+the committed tree and restored after its run
+(`cargo test -p repo-conformance --all-features --test conformance --
+conformance_rt_04 --exact`); the same shapes, and the ones that must not be
+found, are asserted by the case itself.
+
+1. Production code after the first test module of the verifier: a
+   `const PLANTED: &str = "public def LexLeanRuntime.listFold : Nat := 0";`
+   after `HEAVY_FRACTION` in `verify/mod.rs`, which follows the module that
+   ends at line 2694.
+2. A declaration under a runtime name and no `namespace` line, as a string
+   constant appended to `backend/semantic.rs`.
+3. The same text written with `concat!` (`namespace LexLeanCollections`,
+   `public def listFold : Nat := 0`, `end LexLeanCollections` as three
+   literals).
+4. The same under a `format!` template
+   (`public def LexLeanReasoning.{name} : Nat := 0`).
+
+```text
+thread 'conformance_rt_04' panicked at crates/conformance/src/cases/runtime.rs:765:5:
+assertion `left == right` failed: the only Lean runtime text in the compiler is the decoder of core module 2
+  left: [("backend/core_v2.rs", 34), ("verify/mod.rs", 2731)]
+ right: [("backend/core_v2.rs", 34)]
+  left: [("backend/core_v2.rs", 34), ("backend/semantic.rs", 2965)]     (2 and 3)
+  left: [("backend/core_v2.rs", 34), ("backend/semantic.rs", 2966)]     (4)
+```
+
+What the gate cannot see is said here and not left to a reader: a text built
+at run time from parts declared apart (a name in one constant, a template in
+another) is not a literal or a run of literals, and `RT-04` does not read it.
+What bounds that is the other half of its statement, which is checked over
+the output: a generated language-1.2 module that declares under a runtime
+namespace, or names a runtime constant without importing the module that
+declares it, is refused (planted in the case: the committed module of the
+collections example with its runtime imports dropped, and with a runtime
+namespace appended).
+
+`RT-03`'s axiom check compares the observed and the pinned sets in both
+directions (`LLV7005`); the fifth plant of the section above pinned an axiom a
+declaration does not use, and the case now also plants the other:
+`LexLeanCollections.compareCodes._sparseCasesOn_1` pinned to
+`exact{axioms: []}` in `Collections.lex.tex`, which uses `propext`:
+
+```text
+error[LLV7005]: `LexLeanCollections.compareCodes._sparseCasesOn_1` violates its exact axiom policy: observed [propext]
+  --> lexlean.toml:1:1
+```
+
+A runtime declaration whose body changes and still type-checks
+(`@3159 := 64` to `65` in `Portable.lex.tex`, a width constant of
+`checkedMultiplyInt64`) is not caught by `RT-01`..`RT-04`: all four pass with
+it planted, because it is a well-typed change that pins the same axioms. It is
+caught by the identity discipline, which is the gate for any normative byte:
+the language-1.2 compiler-semantics ID changes, so `lexlean lock --check` in
+each language-1.2 example refuses its lock,
+
+```text
+error[LLC0102]: lexlean.lock is stale or noncanonical; run `lexlean lock`
+  --> lexlean.lock:1:1
+```
+
+and a verification after relocking differs from the committed record of the
+example (`examples/collections/expected/verify/audit/LexLeanAudit.Aea7d3fe….*`
+against `LexLeanAudit.A65452ac….*`; the audit prefix is a function of the
+identity); `cargo xtask verify-examples` compares those records, so the change
+stays red until every record is regenerated, which is a diff a review reads. No
+runtime-specific oracle of a declaration's body exists beyond those pins, and
+none is claimed.
+
+`RT-02`'s statement that the frozen files belong to no older identity was a
+grep of `SPEC.md` for the path; it now recomputes the three IDs from disk
+(`RP-10`'s recomputation, shared) and finds, with either frozen file changed
+by one byte, the language-1.0 and 1.1 IDs unchanged and the 1.2 ID changed.
+The repository walkers skip any directory that holds a `CACHEDIR.TAG`: with
+a Cargo target directory named `target-check` in the checkout, `RT-01` and
+`SP-12` failed on its Lean files before and pass now.
+
 ## The planted verification of the compiler project (Issue #145)
 
 `conformance_rs_12` asks which diagnostic pinned Lean's refusal of the planted

crates/conformance/src/cases/authoring.rs

@@ -65,7 +65,10 @@ fn corpus() -> Vec<(String, Json)> {
         .into_iter()
         .filter_entry(|entry| {
             let name = entry.file_name().to_string_lossy();
-            name != "target" && name != ".git" && name != ".lexlean"
+            name != "target"
+                && name != ".git"
+                && name != ".lexlean"
+                && !support::holds_cache_tag(entry)
         })
         .flatten()
     {
@@ -607,7 +610,10 @@ fn one_surface() {
         .into_iter()
         .filter_entry(|entry| {
             let name = entry.file_name().to_string_lossy();
-            name != "target" && name != ".git" && name != ".lexlean"
+            name != "target"
+                && name != ".git"
+                && name != ".lexlean"
+                && !support::holds_cache_tag(entry)
         })
         .flatten()
     {
@@ -708,7 +714,10 @@ fn tooling_corpus() -> Vec<(String, Json)> {
         .into_iter()
         .filter_entry(|entry| {
             let name = entry.file_name().to_string_lossy();
-            name != "target" && name != ".git" && name != ".lexlean"
+            name != "target"
+                && name != ".git"
+                && name != ".lexlean"
+                && !support::holds_cache_tag(entry)
         })
         .flatten()
     {
@@ -1095,7 +1104,10 @@ fn no_other_authoring_path() {
         .into_iter()
         .filter_entry(|entry| {
             let name = entry.file_name().to_string_lossy();
-            name != "target" && name != ".git" && name != ".lexlean"
+            name != "target"
+                && name != ".git"
+                && name != ".lexlean"
+                && !support::holds_cache_tag(entry)
         })
         .flatten()
     {
@@ -1145,7 +1157,10 @@ fn authoring_api() {
         .into_iter()
         .filter_entry(|entry| {
             let name = entry.file_name().to_string_lossy();
-            name != "target" && name != ".git" && name != ".lexlean"
+            name != "target"
+                && name != ".git"
+                && name != ".lexlean"
+                && !support::holds_cache_tag(entry)
         })
         .flatten()
     {

crates/conformance/src/cases/authoring_core.rs

@@ -48,7 +48,10 @@ fn committed() -> Vec<(String, String)> {
         .into_iter()
         .filter_entry(|entry| {
             let name = entry.file_name().to_string_lossy();
-            name != "target" && name != ".git" && name != ".lexlean"
+            name != "target"
+                && name != ".git"
+                && name != ".lexlean"
+                && !support::holds_cache_tag(entry)
         })
         .flatten()
     {

crates/conformance/src/cases/repository.rs

@@ -452,7 +452,11 @@ pub(crate) fn run(id: &str) {
                 .into_iter()
                 .filter_entry(|e| {
                     let name = e.file_name().to_string_lossy();
-                    name != "target" && name != ".git" && name != ".lexlean" && name != "expected"
+                    name != "target"
+                        && name != ".git"
+                        && name != ".lexlean"
+                        && name != "expected"
+                        && !support::holds_cache_tag(e)
                 })
                 .flatten()
             {
@@ -528,32 +532,7 @@ pub(crate) fn run(id: &str) {
         }
         // §21.2: the embedded semantics ID equals a clean disk recomputation.
         "RP-10" => {
-            let mut files: Vec<(String, Vec<u8>)> = Vec::new();
-            for dir in [
-                "language",
-                "schemas",
-                "tests/golden/axiom-parser",
-                "tests/golden/canonical-json",
-            ] {
-                for entry in walkdir::WalkDir::new(root.join(dir).as_std_path())
-                    .into_iter()
-                    .flatten()
-                {
-                    if entry.file_type().is_file() {
-                        let relative = format!(
-                            "{dir}/{}",
-                            entry
-                                .path()
-                                .strip_prefix(root.join(dir).as_std_path())
-                                .expect("under dir")
-                                .to_string_lossy()
-                                .replace('\\', "/")
-                        );
-                        files.push((relative, std::fs::read(entry.path()).expect("read")));
-                    }
-                }
-            }
-            files.sort_by(|a, b| a.0.as_bytes().cmp(b.0.as_bytes()));
+            let files = support::normative_rows();
             let borrowed: Vec<(&str, &[u8])> = files
                 .iter()
                 .map(|(path, bytes)| (path.as_str(), bytes.as_slice()))
@@ -568,65 +547,9 @@ pub(crate) fn run(id: &str) {
             // §21.2: the older languages' IDs are the same digest over the
             // tree minus the files SPEC.md lists as introduced later. The
             // lists are read from the specification, not from the compiler.
-            let spec = support::spec_text();
-            let section = spec
-                .split("### 21.2 Compiler-semantics ID")
-                .nth(1)
-                .and_then(|rest| rest.split("### 21.3").next())
-                .expect("§21.2");
-            let listed = |start: &str, end: &str| -> Vec<String> {
-                let text = section
-                    .split(start)
-                    .nth(1)
-                    .and_then(|rest| rest.split(end).next())
-                    .unwrap_or_else(|| panic!("§21.2 states `{start}`"));
-                let mut out = Vec::new();
-                for item in text.split('`').skip(1).step_by(2) {
-                    match (item.find('{'), item.find('}')) {
-                        (Some(open), Some(close)) => {
-                            for choice in item[open + 1..close].split(',') {
-                                out.push(format!(
-                                    "{}{choice}{}",
-                                    &item[..open],
-                                    &item[close + 1..]
-                                ));
-                            }
-                        }
-                        _ => out.push(item.to_owned()),
-                    }
-                }
-                assert!(!out.is_empty(), "§21.2 lists the files after `{start}`");
-                out
-            };
-            let only_1_2 = listed(
-                "The language-1.1 ID excludes the files introduced solely for 1.2:",
-                "The language-1.0 ID",
-            );
-            let only_1_1 = listed(
-                "excludes the files introduced solely for 1.1:",
-                "Adding a file",
-            );
-            let excluded = |path: &str, lists: &[&Vec<String>]| {
-                lists.iter().any(|list| {
-                    list.iter().any(|item| {
-                        if item.ends_with('/') {
-                            path.starts_with(item.as_str())
-                        } else {
-                            path == item
-                        }
-                    })
-                })
-            };
-            let filtered = |lists: &[&Vec<String>]| {
-                let kept: Vec<(&str, &[u8])> = borrowed
-                    .iter()
-                    .copied()
-                    .filter(|(path, _)| !excluded(path, lists))
-                    .collect();
-                support::identity_tree_digest(&kept)
-            };
-            let eleven = filtered(&[&only_1_2]);
-            let ten = filtered(&[&only_1_2, &only_1_1]);
+            let (only_1_2, only_1_1) = support::introduced_later();
+            let (ten, eleven, twelve) = support::semantics_ids(&borrowed);
+            assert_eq!(twelve, recomputed, "RP-10: the 1.2 ID");
             assert_eq!(
                 eleven,
                 lexlean::compiler_semantics_id_for("1.1"),