From d8dc8845e0b046889d3cfdc3b3238e40c2ef989f Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 16 Oct 2026 14:47:52 +0000 Subject: [PATCH] fix(#154): the runtime gates read what they claim to MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit RT-04 found a Lean runtime text only in a literal that held a namespace line and a declaration, cut each source at its first test module, and read one literal at a time. It now reads every literal outside unit-test items (an item under #[cfg(test)] is blanked, the production code after it is read), finds a declaration under a runtime name with or without a namespace line, and reads literals written together (concat!, arrays, +, format!) joined with and without a line break. Its statement 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. The statement is rewritten to what the case now checks (register, SPEC §31, scenario, CONFORMANCE.md). RT-02 recomputes the compiler-semantics IDs from disk with each frozen file changed: 1.0 and 1.1 unchanged, 1.2 changed (RP-10's recomputation is shared in support). RT-03 plants the second direction of the axiom comparison. The repository walkers skip any directory that holds a CACHEDIR.TAG, so a Cargo target directory with another name no longer reads as source (RT-01, SP-12). VERIFICATION.md records each plant, the output that names it, the one defect no RT case sees (a type-correct body change, caught by the identity pins), and what RT-04 cannot see. The blank line lost in the #145 conflict is restored. Closes #154. Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_013QppGKetUURseXowZun9KY --- CHANGELOG.md | 13 + CONFORMANCE.md | 2 +- SPEC.md | 2 +- VERIFICATION.md | 82 +++ crates/conformance/src/cases/authoring.rs | 25 +- .../conformance/src/cases/authoring_core.rs | 5 +- crates/conformance/src/cases/repository.rs | 95 +-- crates/conformance/src/cases/runtime.rs | 614 ++++++++++++++++-- crates/conformance/src/cases/verification.rs | 1 + crates/conformance/src/oracle.rs | 8 +- crates/conformance/src/support.rs | 139 +++- features/suites/runtime.feature | 10 +- model/ids.toml | 2 +- 13 files changed, 831 insertions(+), 167 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index dd76ce10f..d209bd96a 100644 --- a/CHANGELOG.md +++ b/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. - Child deadlines remain active while reading inherited output pipes after the direct child exits (#132). The process group stays registered until both readers finish, so a timeout or an embedding host can end the remaining diff --git a/CONFORMANCE.md b/CONFORMANCE.md index 996f95a4b..78724b5b0 100644 --- a/CONFORMANCE.md +++ b/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 diff --git a/SPEC.md b/SPEC.md index f09353a0b..a30435da1 100644 --- a/SPEC.md +++ b/SPEC.md @@ -9274,7 +9274,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:** 386. diff --git a/VERIFICATION.md b/VERIFICATION.md index 3159798f5..dcadae648 100644 --- a/VERIFICATION.md +++ b/VERIFICATION.md @@ -7702,6 +7702,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 diff --git a/crates/conformance/src/cases/authoring.rs b/crates/conformance/src/cases/authoring.rs index 8cf273987..b1c6dd2a9 100644 --- a/crates/conformance/src/cases/authoring.rs +++ b/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() { diff --git a/crates/conformance/src/cases/authoring_core.rs b/crates/conformance/src/cases/authoring_core.rs index 17dfcbbfd..0f6cb59da 100644 --- a/crates/conformance/src/cases/authoring_core.rs +++ b/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() { diff --git a/crates/conformance/src/cases/repository.rs b/crates/conformance/src/cases/repository.rs index 6939a9174..6a0ad7e4a 100644 --- a/crates/conformance/src/cases/repository.rs +++ b/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)> = 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 { - 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]| { - 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]| { - 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"), diff --git a/crates/conformance/src/cases/runtime.rs b/crates/conformance/src/cases/runtime.rs index e60960cb2..d60bb1df9 100644 --- a/crates/conformance/src/cases/runtime.rs +++ b/crates/conformance/src/cases/runtime.rs @@ -42,7 +42,9 @@ fn files(root: &std::path::Path, extensions: &[&str]) -> Vec .into_iter() .filter_entry(|entry| { let name = entry.file_name().to_string_lossy(); - !(entry.file_type().is_dir() && matches!(name.as_ref(), "target" | ".git" | ".lexlean")) + !(entry.file_type().is_dir() + && (matches!(name.as_ref(), "target" | ".git" | ".lexlean") + || support::holds_cache_tag(entry))) }) .flatten() .filter(|entry| entry.file_type().is_file()) @@ -292,11 +294,50 @@ fn rt_02() { "a mutated decoder is refused" ); // The frozen bytes belong to no older identity (RP-10 pins those IDs to - // the committed locks). + // the committed locks), and are part of the language-1.2 one: the three + // IDs recomputed from disk are the compiler's, and with either frozen + // file changed the 1.0 and 1.1 IDs are the same and the 1.2 ID is not. assert!( support::spec_text().contains("`language/runtime-1.2/`"), "SPEC.md §21.2 excludes the runtime project and the frozen bytes from the language-1.0 and 1.1 IDs" ); + let rows = support::normative_rows(); + let borrowed: Vec<(&str, &[u8])> = rows + .iter() + .map(|(path, bytes)| (path.as_str(), bytes.as_slice())) + .collect(); + let (ten, eleven, twelve) = support::semantics_ids(&borrowed); + assert_eq!(ten, lexlean::compiler_semantics_id_for("1.0")); + assert_eq!(eleven, lexlean::compiler_semantics_id_for("1.1")); + assert_eq!(twelve, lexlean::compiler_semantics_id_for("1.2")); + for path in [ + runtime::FROZEN_PORTABLE_PATH, + runtime::FROZEN_CORE_DECODER_PATH, + ] { + let mut changed = rows.clone(); + let row = changed + .iter_mut() + .find(|(candidate, _)| candidate == path) + .unwrap_or_else(|| panic!("{path} is in the normative tree")); + row.1.push(b'\n'); + let borrowed: Vec<(&str, &[u8])> = changed + .iter() + .map(|(path, bytes)| (path.as_str(), bytes.as_slice())) + .collect(); + let (changed_ten, changed_eleven, changed_twelve) = support::semantics_ids(&borrowed); + assert_eq!( + changed_ten, ten, + "{path}: the language-1.0 ID does not read it" + ); + assert_eq!( + changed_eleven, eleven, + "{path}: the language-1.1 ID does not read it" + ); + assert_ne!( + changed_twelve, twelve, + "{path}: the language-1.2 ID reads it" + ); + } } /// RT-03: a verification audits the runtime against its pinned axioms. @@ -328,39 +369,117 @@ fn rt_03() { ); planted.relock(); planted.verify_fails_with("LLV7005"); + // And the other direction: a declaration that uses an axiom its row does + // not pin is refused as well (the verifier compares the sets both ways). + let unpinned = P::runtime_project(); + unpinned.edit( + "src/Collections.lex.tex", + "\"policy\":{\"axioms\":[\"propext\"],\"kind\":\"exact\"}", + "\"policy\":{\"axioms\":[],\"kind\":\"exact\"}", + ); + unpinned.relock(); + unpinned.verify_fails_with("LLV7005"); +} + +/// A string literal of a Rust source. +struct Literal { + /// Where its opening delimiter is, and where its closing one ends. + start: usize, + end: usize, + /// The line it opens on. + line: usize, + /// Its text, with escapes resolved (a raw literal as written). + text: String, +} + +/// A Rust source read once: its string literals, and its code with every +/// literal, character literal and comment blanked, so that a brace, an +/// attribute or a keyword found in it is code. +struct Scan { + literals: Vec, + code: Vec, +} + +/// Whether the `r` at `index` opens a raw literal: it is not the end of a +/// longer name, apart from the `b` of a raw byte string. +fn opens_raw(bytes: &[u8], index: usize) -> bool { + let name = |byte: u8| byte.is_ascii_alphanumeric() || byte == b'_'; + match index.checked_sub(1).map(|before| bytes[before]) { + None => true, + Some(b'b') => index == 1 || !name(bytes[index - 2]), + Some(byte) => !name(byte), + } } -/// The string literals of a Rust source, decoded: raw literals as written, -/// ordinary ones with their escapes resolved, with the line each opens on. -fn string_literals(source: &str) -> Vec<(usize, String)> { +fn scan(source: &str) -> Scan { let bytes = source.as_bytes(); - let mut out = Vec::new(); + let mut code = bytes.to_vec(); + let mut literals = Vec::new(); + let blank = |code: &mut Vec, from: usize, to: usize| { + for byte in &mut code[from..to.min(bytes.len())] { + if *byte != b'\n' { + *byte = b' '; + } + } + }; + let line_of = |at: usize| source[..at].matches('\n').count() + 1; let mut index = 0; while index < bytes.len() { match bytes[index] { b'/' if bytes.get(index + 1) == Some(&b'/') => { + let start = index; while index < bytes.len() && bytes[index] != b'\n' { index += 1; } + blank(&mut code, start, index); + } + b'/' if bytes.get(index + 1) == Some(&b'*') => { + // Block comments nest. + let start = index; + let mut depth = 0usize; + while index < bytes.len() { + if bytes[index..].starts_with(b"/*") { + depth += 1; + index += 2; + } else if bytes[index..].starts_with(b"*/") { + depth -= 1; + index += 2; + if depth == 0 { + break; + } + } else { + index += 1; + } + } + blank(&mut code, start, index); } b'\'' => { - // A character literal or a lifetime: skip `'x'`, `'\x'`. - if bytes.get(index + 2) == Some(&b'\'') { + // A character literal (`'x'`, `'\n'`, `'\u{1F600}'`, `'é'`) or + // a lifetime. + let start = index; + if bytes.get(index + 1) == Some(&b'\\') { index += 3; - } else if bytes.get(index + 1) == Some(&b'\\') { - index += 2; while index < bytes.len() && bytes[index] != b'\'' { index += 1; } index += 1; + blank(&mut code, start, index); + } else if let Some(next) = source[index + 1..].chars().next() { + let width = next.len_utf8(); + if bytes.get(index + 1 + width) == Some(&b'\'') { + index += width + 2; + blank(&mut code, start, index); + } else { + index += 1; + } } else { index += 1; } } b'r' if matches!(bytes.get(index + 1), Some(b'#' | b'"')) - && (index == 0 - || !(bytes[index - 1].is_ascii_alphanumeric() || bytes[index - 1] == b'_')) => + && opens_raw(bytes, index) => { + let start = index; let mut hashes = 0; let mut at = index + 1; while bytes.get(at) == Some(&b'#') { @@ -372,18 +491,21 @@ fn string_literals(source: &str) -> Vec<(usize, String)> { continue; } let closing = format!("\"{}", "#".repeat(hashes)); - let start = at + 1; - let end = source[start..] + let text_start = at + 1; + let text_end = source[text_start..] .find(&closing) - .map_or(bytes.len(), |end| start + end); - out.push(( - source[..index].matches('\n').count() + 1, - source[start..end].to_owned(), - )); - index = end + closing.len(); + .map_or(bytes.len(), |end| text_start + end); + index = (text_end + closing.len()).min(bytes.len()); + literals.push(Literal { + start, + end: index, + line: line_of(start), + text: source[text_start..text_end].to_owned(), + }); + blank(&mut code, start, index); } b'"' => { - let line = source[..index].matches('\n').count() + 1; + let start = index; let mut text = String::new(); index += 1; while index < bytes.len() && bytes[index] != b'"' { @@ -391,6 +513,42 @@ fn string_literals(source: &str) -> Vec<(usize, String)> { match bytes[index + 1] { b'n' => text.push('\n'), b't' => text.push('\t'), + b'r' => text.push('\r'), + b'0' => text.push('\0'), + // A backslash before a line break drops the + // break and the white space that opens the next + // line: one literal written over several lines. + b'\n' | b'\r' => { + index += 2; + while index < bytes.len() && bytes[index].is_ascii_whitespace() { + index += 1; + } + continue; + } + b'x' => { + let digits = source.get(index + 2..index + 4).unwrap_or_default(); + if let Ok(value) = u8::from_str_radix(digits, 16) { + text.push(char::from(value)); + } + index += 4; + continue; + } + b'u' => { + let close = + source[index..].find('}').map_or(index + 2, |at| index + at); + let digits = source + .get(index + 3..close) + .unwrap_or_default() + .replace('_', ""); + if let Some(decoded) = u32::from_str_radix(&digits, 16) + .ok() + .and_then(char::from_u32) + { + text.push(decoded); + } + index = close + 1; + continue; + } other => text.push(char::from(other)), } index += 2; @@ -400,26 +558,99 @@ fn string_literals(source: &str) -> Vec<(usize, String)> { index += width; } } - out.push((line, text)); - index += 1; + index = (index + 1).min(bytes.len()); + literals.push(Literal { + start, + end: index, + line: line_of(start), + text, + }); + blank(&mut code, start, index); } _ => index += 1, } } - out + Scan { literals, code } } -/// Whether a text is Lean runtime text: a `namespace` and, within it, a -/// declaration. -fn is_runtime_text(text: &str) -> bool { - let declaration = |line: &str| { - let mut rest = line.trim_start(); - if rest.starts_with("@[") { - rest = rest - .split_once(']') - .map_or("", |(_, after)| after) - .trim_start(); +/// A source with its test items blanked, each by the line breaks it held so +/// that every other line keeps its number: an item under `#[cfg(test)]` (a +/// `mod`, a function, a `use`), wherever it stands, and the whole file when +/// it opens with `#![cfg(test)]`. A unit test's fixture text is no part of +/// what the compiler emits. What follows a test item is production code and +/// stays, which a cut at the first test module would have dropped. +fn without_test_items(source: &str) -> String { + let scanned = scan(source); + let code = &scanned.code; + let mut blanked = source.as_bytes().to_vec(); + let erase = |blanked: &mut Vec, from: usize, to: usize| { + for byte in &mut blanked[from..to] { + if *byte != b'\n' { + *byte = b' '; + } + } + }; + let text = String::from_utf8_lossy(code).into_owned(); + if text.contains("#![cfg(test)]") { + let whole = blanked.len(); + erase(&mut blanked, 0, whole); + } + let mut search = 0; + while let Some(found) = text[search..].find("#[cfg(test)]") { + let attribute = search + found; + // The item follows its attributes: up to the first `{` or `;` outside + // parentheses and brackets, then the matching `}`. + let mut at = attribute + "#[cfg(test)]".len(); + let mut nesting = 0usize; + let mut end = code.len(); + while at < code.len() { + match code[at] { + b'(' | b'[' => nesting += 1, + b')' | b']' => nesting = nesting.saturating_sub(1), + b';' if nesting == 0 => { + end = at + 1; + break; + } + b'{' if nesting == 0 => { + let mut depth = 0usize; + while at < code.len() { + match code[at] { + b'{' => depth += 1, + b'}' => { + depth -= 1; + if depth == 0 { + break; + } + } + _ => {} + } + at += 1; + } + end = (at + 1).min(code.len()); + break; + } + _ => {} + } + at += 1; } + erase(&mut blanked, attribute, end); + search = end.max(attribute + 1); + } + String::from_utf8(blanked).expect("blanking keeps ASCII and whole characters") +} + +/// What a line of Lean declares, when it declares: the text after the +/// declaration keyword, once its attributes and modifiers are read. +fn declaration(line: &str) -> Option<&str> { + let mut rest = line.trim_start(); + while rest.starts_with("@[") { + rest = rest + .split_once(']') + .map_or("", |(_, after)| after) + .trim_start(); + } + loop { + let before = rest; for modifier in [ "public ", "private ", @@ -430,45 +661,145 @@ fn is_runtime_text(text: &str) -> bool { ] { rest = rest.strip_prefix(modifier).unwrap_or(rest); } - [ - "def ", - "theorem ", - "instance ", - "class ", - "inductive ", - "structure ", - "abbrev ", - ] - .iter() - .any(|keyword| rest.starts_with(keyword)) + if rest == before { + break; + } + } + [ + "def ", + "theorem ", + "lemma ", + "instance ", + "class ", + "inductive ", + "structure ", + "abbrev ", + "opaque ", + "axiom ", + ] + .iter() + .find_map(|keyword| rest.strip_prefix(keyword)) +} + +/// Whether a text opens or closes a runtime namespace, or declares a name +/// under one (`def LexLeanRuntime.x`), with or without a `namespace` line +/// around it. A text that only names a runtime constant, as the Lean a +/// generated module holds does, is not one. +fn declares_under_runtime(text: &str) -> bool { + let under_runtime = |name: &str| { + NAMESPACES + .iter() + .any(|namespace| name == *namespace || name.starts_with(&format!("{namespace}."))) }; - text.lines().any(|line| line.starts_with("namespace ")) && text.lines().any(declaration) + text.lines().map(str::trim_start).any(|line| { + let namespace = line + .strip_prefix("namespace ") + .or_else(|| line.strip_prefix("end ")) + .is_some_and(|name| under_runtime(name.split_whitespace().next().unwrap_or_default())); + let declared = declaration(line).is_some_and(|rest| { + under_runtime( + rest.split(|c: char| c.is_whitespace() || ":({[".contains(c)) + .next() + .unwrap_or_default(), + ) + }); + namespace || declared + }) +} + +/// Whether a text of the compiler's source is Lean runtime text: it declares +/// under a runtime namespace, or it declares something inside a namespace of +/// its own, which is how a runtime module reads whatever it is called. +fn is_runtime_text(text: &str) -> bool { + declares_under_runtime(text) + || (text.lines().any(|line| line.starts_with("namespace ")) + && text.lines().any(|line| declaration(line).is_some())) } -/// The runtime texts of a Rust source, by line. +/// The runtime texts of a Rust source, by line: a literal alone, and the +/// literals written one after another (`concat!`, an array of lines, `+`, +/// the arguments of `format!`), read joined with and without a line break +/// between them, because a text can be cut anywhere. fn runtime_texts(source: &str) -> Vec { - string_literals(source) + let scanned = scan(source); + let mut found = Vec::new(); + let mut chain: Vec<&Literal> = Vec::new(); + let flush = |chain: &mut Vec<&Literal>, found: &mut Vec| { + if let Some(first) = chain.first() { + let texts: Vec<&str> = chain.iter().map(|literal| literal.text.as_str()).collect(); + if texts.iter().any(|text| is_runtime_text(text)) + || is_runtime_text(&texts.concat()) + || is_runtime_text(&texts.join("\n")) + { + found.push(first.line); + } + } + chain.clear(); + }; + for literal in &scanned.literals { + if let Some(previous) = chain.last() { + // The same expression: little between the two, and no statement + // or block boundary. + let between = &source[previous.end..literal.start]; + if between.len() > 64 || between.contains([';', '{', '}']) { + flush(&mut chain, &mut found); + } + } + chain.push(literal); + } + flush(&mut chain, &mut found); + found +} + +/// What a generated language-1.2 module must be to meet RT-04's statement: +/// it names a runtime constant only if it imports the runtime module that +/// declares it, and it declares nothing under a runtime namespace. +fn generated_module_defects( + text: &str, + owners: &std::collections::BTreeMap, +) -> Vec { + let mut defects = Vec::new(); + let imported: BTreeSet<&str> = runtime::imported_by([text]) + .expect("the shipped runtime") .into_iter() - .filter(|(_, text)| is_runtime_text(text)) - .map(|(line, _)| line) - .collect() + .map(|module| module.name.as_str()) + .collect(); + let mut seen = BTreeSet::new(); + for token in text.split(|c: char| !(c.is_alphanumeric() || matches!(c, '_' | '.' | '\''))) { + if !NAMESPACES + .iter() + .any(|namespace| token.starts_with(&format!("{namespace}."))) + { + continue; + } + let name = token.trim_end_matches('.'); + if let Some(owner) = owners.get(name) { + if !imported.contains(owner) && seen.insert(name.to_owned()) { + defects.push(format!("uses `{name}` without importing `{owner}`")); + } + } + } + if declares_under_runtime(text) { + defects.push("declares a runtime namespace or a name under one".to_owned()); + } + defects } /// RT-04: no Lean runtime text remains in the language-1.2 compiler but the -/// decoder of core module 2, which loads native modules. +/// decoder of core module 2, which loads native modules; and what the +/// compiler generates imports the runtime modules it uses and splices none. fn rt_04() { let source_root = repo_root().join("crates/lexlean/src"); let mut found = Vec::new(); for path in files(source_root.as_std_path(), &["rs"]) { let text = std::fs::read_to_string(&path).expect("a compiler source"); - // A unit test's fixture text is no part of what the compiler emits. - let text = text.split("\n#[cfg(test)]").next().unwrap_or_default(); + let text = without_test_items(&text); let relative = path .strip_prefix(source_root.as_std_path()) .expect("below the source root") .to_string_lossy() .replace('\\', "/"); - for line in runtime_texts(text) { + for line in runtime_texts(&text) { found.push((relative.clone(), line)); } } @@ -479,24 +810,179 @@ fn rt_04() { .position(|line| line.starts_with("pub const LEAN_CORE_DECODER_V2")) .expect("the decoder constant") + 1; + found.sort(); assert_eq!( found, [("backend/core_v2.rs".to_owned(), decoder_line)], "the only Lean runtime text in the compiler is the decoder of core module 2" ); - // A planted runtime text constant, raw or escaped, is found. - for plant in [ - "const PLANTED: &str = r#\"\nnamespace LexLeanCollections\n\n@[expose] public def listFold {α σ : Type} (step : σ -> α -> σ) (initial : σ) (values : List α) : σ :=\n values.foldl step initial\nend LexLeanCollections\n\"#;\n", - "const PLANTED: &str = \"\\nnamespace LexLeanModels\\npublic def Sound1 : Prop := True\\nend LexLeanModels\\n\";\n", + // A planted runtime text is found wherever and however it is written: + // raw or escaped, with a namespace line or only a qualified name, split + // across literals or written over several lines, and in production code + // that follows a test module. + let semantic = std::fs::read_to_string(source_root.join("backend/semantic.rs").as_std_path()) + .expect("the semantic backend"); + assert_eq!( + runtime_texts(&without_test_items(&semantic)), + Vec::::new(), + "the semantic backend carries no runtime text" + ); + for (shape, plant) in [ + ( + "a raw literal", + "const PLANTED: &str = r#\"\nnamespace LexLeanCollections\n\n@[expose] public def listFold {α σ : Type} (step : σ -> α -> σ) (initial : σ) (values : List α) : σ :=\n values.foldl step initial\nend LexLeanCollections\n\"#;\n", + ), + ( + "an escaped literal", + "const PLANTED: &str = \"\\nnamespace LexLeanModels\\npublic def Sound1 : Prop := True\\nend LexLeanModels\\n\";\n", + ), + ( + "a declaration under a runtime name and no namespace line", + "const PLANTED: &str = \"public def LexLeanRuntime.listFold {α : Type} (xs : List α) : Nat := xs.length\\n\";\n", + ), + ( + "a theorem under a runtime name", + "const PLANTED: &str = \"theorem LexLeanReasoning.sound1 : True := trivial\";\n", + ), + ( + "a namespace opened and closed with nothing declared in it", + "const PLANTED: &str = \"namespace LexLeanModels\\nend LexLeanModels\\n\";\n", + ), + ( + "literals joined by concat!", + "const PLANTED: &str = concat!(\n \"namespace LexLeanCollections\\n\",\n \"public def listFold : Nat := 0\\n\",\n \"end LexLeanCollections\\n\"\n);\n", + ), + ( + "a name cut inside its namespace", + "const PLANTED: &str = concat!(\"public def LexLean\", \"Models.Sound1 : Prop := True\");\n", + ), + ( + "an array of lines", + "const PLANTED: [&str; 2] = [\"namespace LexLeanRuntime\", \"public def x : Nat := 0\"];\n", + ), + ( + "a format! template", + "fn planted(name: &str) -> String {\n format!(\"public def LexLeanReasoning.{name} : Nat := 0\")\n}\n", + ), + ( + "a literal continued over lines", + "const PLANTED: &str = \"namespace LexLeanModels\\n\\\n public def Sound1 : Prop := True\\n\";\n", + ), ] { - let semantic = std::fs::read_to_string(source_root.join("backend/semantic.rs").as_std_path()) - .expect("the semantic backend"); - assert_eq!(runtime_texts(&semantic), Vec::::new(), "the semantic backend carries no runtime text"); let planted = format!("{semantic}\n{plant}"); assert_eq!( - runtime_texts(&planted).len(), + runtime_texts(&without_test_items(&planted)).len(), 1, - "a planted runtime text constant is found: {plant}" + "a planted runtime text is found ({shape}): {plant}" ); } + // Production code after a test module is read: a text planted after the + // `HEAVY_FRACTION` constant of the verifier, which follows its first test + // module, is found, and the finding names a line below that module. + let verifier = std::fs::read_to_string(source_root.join("verify/mod.rs").as_std_path()) + .expect("the verifier"); + let first_test = verifier + .lines() + .position(|line| line.starts_with("#[cfg(test)]")) + .expect("the verifier has a unit test module") + + 1; + let after = verifier + .find("const HEAVY_FRACTION") + .and_then(|at| verifier[at..].find('\n').map(|end| at + end + 1)) + .expect("the verifier holds HEAVY_FRACTION"); + let at_line = verifier[..after].matches('\n').count() + 1; + assert!( + at_line > first_test, + "HEAVY_FRACTION follows the first unit test module of the verifier" + ); + let planted = format!( + "{}const PLANTED: &str = \"public def LexLeanRuntime.listFold : Nat := 0\";\n{}", + &verifier[..after], + &verifier[after..] + ); + assert_eq!( + runtime_texts(&without_test_items(&planted)), + [at_line], + "a runtime text after a test module is found, on its own line" + ); + // A unit test's fixture is not what the compiler emits: the same text + // inside a test item is not found, and the production code after it is. + let in_test = format!( + "{semantic}\n#[cfg(test)]\nmod planted_tests {{\n const FIXTURE: &str = \"namespace LexLeanRuntime\\npublic def x : Nat := 0\\n\";\n fn nested() {{ if true {{ let _ = 1; }} }}\n}}\nconst PRODUCTION: &str = \"namespace LexLeanRuntime\\npublic def y : Nat := 0\\n\";\n" + ); + let found_after_test = runtime_texts(&without_test_items(&in_test)); + assert_eq!( + found_after_test.len(), + 1, + "a test item's fixture is skipped and the production text after it is found" + ); + // The statement's other half, over what the compiler generates: every + // committed language-1.2 module imports the runtime modules whose + // constants it names and declares none, and a module that omits an + // import, or splices a declaration, is refused. + let modules = runtime::modules().expect("the shipped runtime"); + let mut owners: std::collections::BTreeMap = + std::collections::BTreeMap::new(); + for module in modules { + for (name, _) in &module.declarations { + owners.insert(name.clone(), module.name.as_str()); + } + } + assert!(!owners.is_empty(), "the runtime modules declare constants"); + let root = repo_root(); + let mut generated = 0usize; + let mut using = None; + for path in files(root.as_std_path(), &["lean"]) { + let shown = path.display().to_string().replace('\\', "/"); + let is_output = shown.contains("/expected/build/modules/"); + let project = path + .ancestors() + .find(|ancestor| ancestor.join("lexlean.toml").is_file()); + let language_1_2 = project.is_some_and(|project| { + std::fs::read_to_string(project.join("lexlean.toml")) + .unwrap_or_default() + .contains("language = \"1.2\"") + }); + if !is_output || !language_1_2 { + continue; + } + let text = std::fs::read_to_string(&path).expect("a generated module"); + generated += 1; + assert_eq!( + generated_module_defects(&text, &owners), + Vec::::new(), + "{shown}: a generated language-1.2 module meets the statement" + ); + if using.is_none() + && text + .split(|c: char| !(c.is_alphanumeric() || matches!(c, '_' | '.' | '\''))) + .any(|token| owners.contains_key(token)) + { + using = Some(text); + } + } + assert!( + generated > 0, + "the repository commits generated language-1.2 modules" + ); + let using = using.expect("a committed generated module uses a runtime constant"); + let without_import = using + .lines() + .filter(|line| { + !line.starts_with("public import LexLeanRuntime.") + && !line.starts_with("import LexLeanRuntime.") + }) + .collect::>() + .join("\n"); + assert!( + !generated_module_defects(&without_import, &owners).is_empty(), + "a generated module that drops its runtime imports is refused" + ); + let spliced = format!( + "{using}\nnamespace LexLeanRuntime\npublic def planted : Nat := 0\nend LexLeanRuntime\n" + ); + assert!( + !generated_module_defects(&spliced, &owners).is_empty(), + "a generated module that declares a runtime namespace is refused" + ); } diff --git a/crates/conformance/src/cases/verification.rs b/crates/conformance/src/cases/verification.rs index 7f986bbd4..62fb792a0 100644 --- a/crates/conformance/src/cases/verification.rs +++ b/crates/conformance/src/cases/verification.rs @@ -1239,6 +1239,7 @@ pub(crate) fn run(id: &str) { .filter_entry(|entry| { ![".git", ".lake", ".lexlean", "expected", "target"] .contains(&entry.file_name().to_string_lossy().as_ref()) + && !support::holds_cache_tag(entry) }) .flatten() .filter(|entry| { diff --git a/crates/conformance/src/oracle.rs b/crates/conformance/src/oracle.rs index e611bc37d..0d6ed354b 100644 --- a/crates/conformance/src/oracle.rs +++ b/crates/conformance/src/oracle.rs @@ -181,7 +181,9 @@ pub fn tree_digest(root: &Path, pin: &Pin) -> Result<(String, usize), String> { .into_iter() .filter_entry(|entry| { let name = entry.file_name().to_string_lossy(); - !(entry.file_type().is_dir() && matches!(name.as_ref(), ".git" | ".lake" | "target")) + !(entry.file_type().is_dir() + && (matches!(name.as_ref(), ".git" | ".lake" | "target") + || crate::support::holds_cache_tag(entry))) }) { let entry = entry.map_err(|error| error.to_string())?; @@ -439,7 +441,9 @@ fn copy_tree(from: &Path, to: &Path, pin: &Pin, root: &Path) -> Result<(), Strin .into_iter() .filter_entry(|entry| { let name = entry.file_name().to_string_lossy(); - !(entry.file_type().is_dir() && matches!(name.as_ref(), ".git" | ".lake" | "target")) + !(entry.file_type().is_dir() + && (matches!(name.as_ref(), ".git" | ".lake" | "target") + || crate::support::holds_cache_tag(entry))) }) { let entry = entry.map_err(|error| error.to_string())?; diff --git a/crates/conformance/src/support.rs b/crates/conformance/src/support.rs index 937dfe898..ca7d9af84 100644 --- a/crates/conformance/src/support.rs +++ b/crates/conformance/src/support.rs @@ -24,6 +24,16 @@ pub fn repo_root() -> Utf8PathBuf { .to_path_buf() } +/// Whether a walked directory is build output: one that holds a +/// `CACHEDIR.TAG`, which Cargo writes in every target directory whatever the +/// directory is called, so a build directory kept beside the checkout's +/// sources (`target-check`, say) is skipped like `target` and is not read as +/// a source tree. +#[must_use] +pub fn holds_cache_tag(entry: &walkdir::DirEntry) -> bool { + entry.file_type().is_dir() && entry.path().join("CACHEDIR.TAG").is_file() +} + /// A proof library (SPEC.md §17.17, §17.18) is LexLean source and has no /// independently authored Lean implementation anywhere in the release tree, the /// permanent condition `VR-19` states of the Atlas: no Lean file lies under a @@ -45,7 +55,9 @@ pub fn assert_library_has_no_handwritten_lean(prefix: &str, oracle: &str) { .into_iter() .filter_entry(|entry| { let name = entry.file_name().to_string_lossy(); - !(entry.file_type().is_dir() && matches!(name.as_ref(), "target" | ".git" | ".lexlean")) + !(entry.file_type().is_dir() + && (matches!(name.as_ref(), "target" | ".git" | ".lexlean") + || holds_cache_tag(entry))) }); for entry in walker.flatten() { let path = entry.path(); @@ -2257,6 +2269,131 @@ pub fn identity_tree_digest(rows: &[(&str, &[u8])]) -> lexlean::artifact::conten lexlean::artifact::content_id::tree_digest(&borrowed) } +/// The normative tree the compiler-semantics ID is the digest of, read from +/// disk: every file of `language/`, `schemas/` and the two golden fixture +/// directories, as (path, bytes) rows in bytewise path order (SPEC.md §21.2). +/// +/// # Panics +/// +/// Panics when a file cannot be read. +#[must_use] +pub fn normative_rows() -> Vec<(String, Vec)> { + let root = repo_root(); + let mut files: Vec<(String, Vec)> = 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())); + files +} + +/// The files `SPEC.md` §21.2 lists as introduced solely for language 1.2 and +/// solely for language 1.1: the older languages' compiler-semantics IDs leave +/// them out. Read from the specification, not from the compiler. +/// +/// # Panics +/// +/// Panics when §21.2 does not state a list. +#[must_use] +pub fn introduced_later() -> (Vec, Vec) { + let spec = 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 { + 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 + }; + ( + listed( + "The language-1.1 ID excludes the files introduced solely for 1.2:", + "The language-1.0 ID", + ), + listed( + "excludes the files introduced solely for 1.1:", + "Adding a file", + ), + ) +} + +/// The compiler-semantics IDs of languages 1.0, 1.1 and 1.2 recomputed from +/// rows of the normative tree (path and bytes, in bytewise path order): 1.2 +/// over every row, and the older two over the rows §21.2 does not list as +/// introduced later (`RP-10`). +#[must_use] +pub fn semantics_ids( + rows: &[(&str, &[u8])], +) -> ( + lexlean::artifact::content_id::Sha256Digest, + lexlean::artifact::content_id::Sha256Digest, + lexlean::artifact::content_id::Sha256Digest, +) { + let (only_1_2, only_1_1) = introduced_later(); + let excluded = |path: &str, lists: &[&Vec]| { + 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]| { + let kept: Vec<(&str, &[u8])> = rows + .iter() + .copied() + .filter(|(path, _)| !excluded(path, lists)) + .collect(); + identity_tree_digest(&kept) + }; + ( + filtered(&[&only_1_2, &only_1_1]), + filtered(&[&only_1_2]), + identity_tree_digest(rows), + ) +} + /// Whether `text` has a semantic or tooling module written in the authoring /// notation that is well formed. #[must_use] diff --git a/features/suites/runtime.feature b/features/suites/runtime.feature index 3068ad0aa..c10bbc199 100644 --- a/features/suites/runtime.feature +++ b/features/suites/runtime.feature @@ -25,8 +25,8 @@ Feature: runtime And the planted row fails with LLV7005 @RT-04 @build - Scenario: 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. - Given the source of the compiler - When every string literal outside its unit tests is read for Lean declarations under a namespace - Then the only one is the decoder of core module 2 - And a runtime text constant planted in the semantic backend, raw or escaped, is found + Scenario: 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. + Given the source of the compiler and every committed generated language-1.2 module + When every string literal outside its unit-test items, and every run of literals written together, is read for a runtime namespace opened or declared under, and for a declaration inside a namespace + Then the only one is the decoder of core module 2, and every generated module that names a runtime constant imports the runtime module that declares it and declares nothing under a runtime namespace + And a runtime text planted in the semantic backend, raw or escaped, with or without a namespace line, split by concat!, an array or format!, or in production code after a unit test module, is found, a runtime text inside a unit-test item is not, and a generated module without its runtime imports or with a runtime declaration is refused diff --git a/model/ids.toml b/model/ids.toml index f4efb3acd..7f91d24b7 100644 --- a/model/ids.toml +++ b/model/ids.toml @@ -2324,4 +2324,4 @@ statement = "A verification compiles every runtime module that a project's gener id = "RT-04" level = "build" suite = "runtime" -statement = "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." +statement = "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."