Close six small review leftovers across TCP tests, law citation, and diagnostics

docs/diagnostics-slugs.md

@@ -65,6 +65,8 @@ Source of truth: `src/diagnostics/classify.rs` (classifier) and `src/checker/*.r
 | `unused-expose` | warning | Module `exposes` a name nobody imports. | Drop from `exposes` or start using it. |
 | `stdlib-shadow` | warning | A `depends` entry names an embedded standard module while a same-named project file exists; the project file is silently ignored because the standard library wins resolution. | Rename the project module and its `depends [...]` entries to use the project file. |
 
+`stdlib-shadow` reaches you on two channels and only one of them is suppressible: the structured finding honours `[[check.suppress]]` like every other warning, while the module loader's stderr `warning:` line is emitted at resolution time on every command (`run`, `verify`, `compile`, …) and deliberately ignores suppression — silently loading different code than the project file on disk is a change of program meaning, not a style opinion. The stderr line is printed once per process per shadowed module name.
+
 ## Naming conventions
 
 | Slug | Severity | Fires when | Repair |

src/codegen/lean/law_auto/induction/mod.rs

@@ -458,6 +458,22 @@ fn program_fn_lean_names(ctx: &CodegenContext) -> BTreeSet<String> {
         .collect()
 }
 
+/// The spelling a dep-module name carries in EMITTED Lean: every
+/// `.`-segment escaped against the reserved-token table, exactly as
+/// `expr::emit_expr` renders a qualified call site. Identity for an
+/// ordinary module name (`Lib` → `Lib`); a module named after a reserved
+/// token gains the guard (`Type` → `Type'`).
+///
+/// Any set or index that is compared against tokens of emitted Lean text
+/// — the dep membership index, the orientation analysis' program-fn set,
+/// a citation name spliced into a `simp` list — must be keyed on THIS
+/// spelling, never on the raw `ModuleInfo::prefix`. Raw prefixes stay the
+/// identity currency of the cone gate (`qualified_cone_name`) and of the
+/// `(module_prefix, theorem_base)` emit keys.
+fn dep_module_lean_prefix(prefix: &str) -> String {
+    crate::codegen::lean::syntax::aver_path_to_lean(prefix)
+}
+
 /// Map a cone fn to the lean name a DEP law's statement would render it
 /// as: dep-module fns are NAMESPACE-QUALIFIED (`Lib.qrev`), entry fns
 /// stay bare. The module is resolved by pointer-eq against
@@ -520,7 +536,13 @@ fn dep_law_admissible(
         crate::codegen::lean::toplevel::law_as_lemma_statement(dep_prev, dep_prev_law, ctx)
     })?;
     // Namespace-qualified citation; the entry imports + opens the dep.
-    let name = format!("{}.{}", dep_module.prefix, bare_name);
+    // The module segment carries the reserved-token guard because this
+    // name is spliced verbatim into the consumer's `simp` lists.
+    let name = format!(
+        "{}.{}",
+        dep_module_lean_prefix(&dep_module.prefix),
+        bare_name
+    );
     let text = format!("theorem {name} : {stmt} := by");
     let mentions = crate::codegen::lemma_discovery::mentioned_fns(&text, dep_index);
     if mentions.is_empty() {
@@ -777,9 +799,12 @@ pub(crate) fn admitted_dep_law_theorems(
                         &dep_index,
                         ctx,
                     ) {
-                        // `name` is `Module.<theorem_base>`; the EMIT side keys
-                        // on `(prefix, theorem_base)`.
-                        if let Some(base) = name.strip_prefix(&format!("{}.", module.prefix)) {
+                        // `name` is the CITATION spelling
+                        // (`<lean_prefix>.<theorem_base>`); the EMIT side keys
+                        // on the RAW `(prefix, theorem_base)`, so strip the
+                        // lean prefix and re-key on the raw one.
+                        let lean_prefix = dep_module_lean_prefix(&module.prefix);
+                        if let Some(base) = name.strip_prefix(&format!("{lean_prefix}.")) {
                             admitted.insert((module.prefix.clone(), base.to_string()));
                         }
                     }
@@ -820,10 +845,22 @@ pub(crate) fn admitted_dep_law_theorems(
 }
 
 /// Build the cross-file membership index for a dep module's laws: each
-/// pure fn of `module` mapped QUALIFIED → QUALIFIED (`Lib.qrev` →
-/// `Lib.qrev`), unioned with the entry/dep bare program index. Keyed on
-/// the qualified form because a dep law's statement renders dep fns
-/// namespace-qualified, so the gate compares qualified identity.
+/// pure fn of `module` mapped LEAN SPELLING → QUALIFIED IDENTITY
+/// (`Lib.qrev` → `Lib.qrev`), unioned with the entry/dep bare program
+/// index. Keyed on the qualified form because a dep law's statement
+/// renders dep fns namespace-qualified, so the gate compares qualified
+/// identity.
+///
+/// The two sides of the pair differ exactly when the module name is a
+/// reserved Lean token. `mentioned_fns` tokenizes the EMITTED statement,
+/// where the module segment carries the reserved-token guard
+/// (`Type'.double` — `aver_path_to_lean` escapes per segment), while the
+/// cone gate (`qualified_cone_name`) holds the RAW module prefix. Keying
+/// on the Lean spelling and mapping to the raw-prefix identity
+/// canonicalizes the two at this boundary: without it a dep module named
+/// after a reserved token never matches a token, `mentions` comes back
+/// empty, and every citation of its laws silently degrades to
+/// law-not-admitted.
 fn dep_membership_index(
     module: &crate::codegen::ModuleInfo,
     ctx: &CodegenContext,
@@ -832,10 +869,12 @@ fn dep_membership_index(
         .into_iter()
         .map(|l| (l.clone(), l))
         .collect();
+    let lean_prefix = dep_module_lean_prefix(&module.prefix);
     for fd in &module.fn_defs {
         if crate::codegen::common::is_pure_fn(fd) {
-            let qualified = format!("{}.{}", module.prefix, aver_name_to_lean(&fd.name));
-            idx.insert(qualified.clone(), qualified);
+            let bare = aver_name_to_lean(&fd.name);
+            let qualified = format!("{}.{}", module.prefix, bare);
+            idx.insert(format!("{lean_prefix}.{bare}"), qualified);
         }
     }
     idx
@@ -1455,15 +1494,17 @@ fn fastpath_simp_entries(
     // The orientation / loop-exclusion analysis keys on whether a
     // lemma's head is a program fn. A cross-file sibling's statement
     // renders dep fns NAMESPACE-QUALIFIED (`Lib.qrev`), so the program-
-    // fn set must carry those qualified forms too or the dep lemma is
-    // silently classified `None` and dropped from the simp set. No dep
-    // modules → no qualified names added → byte-identical to the
-    // single-file path.
+    // fn set must carry those qualified forms too — in the EMITTED
+    // spelling (`dep_module_lean_prefix`), since the head token is read
+    // off the statement text — or the dep lemma is silently classified
+    // `None` and dropped from the simp set. No dep modules → no
+    // qualified names added → byte-identical to the single-file path.
     let mut program_fns = program_fn_lean_names(ctx);
     for module in &ctx.modules {
+        let lean_prefix = dep_module_lean_prefix(&module.prefix);
         for fd in &module.fn_defs {
             if crate::codegen::common::is_pure_fn(fd) {
-                program_fns.insert(format!("{}.{}", module.prefix, aver_name_to_lean(&fd.name)));
+                program_fns.insert(format!("{lean_prefix}.{}", aver_name_to_lean(&fd.name)));
             }
         }
     }

src/codegen/lean/syntax.rs

@@ -270,6 +270,39 @@ mod tests {
 
     use super::aver_name_to_lean;
 
+    /// Whether a failed `lean` invocation died fetching the pinned
+    /// toolchain rather than running the probe. The `lean` on PATH is
+    /// elan's shim: with a `lean-toolchain` file in the working directory
+    /// it resolves and downloads that toolchain before handing off, so a
+    /// download error surfaces as a nonzero exit with elan's message on
+    /// stderr. Deliberately narrow — anything else (a probe that elaborated
+    /// and reported an error, a broken elab command after a toolchain
+    /// upgrade) is a real verdict and must not be retried.
+    fn toolchain_fetch_failed(stderr: &str) -> bool {
+        const FETCH_MARKERS: &[&str] = &[
+            "could not download",
+            "failed to download",
+            "error sending request",
+            "connection reset",
+            "connection refused",
+            "temporary failure in name resolution",
+            "could not resolve host",
+        ];
+        let lowered = stderr.to_ascii_lowercase();
+        FETCH_MARKERS.iter().any(|m| lowered.contains(m))
+    }
+
+    #[test]
+    fn rejects_non_fetch_probe_failures_for_retry() {
+        assert!(toolchain_fetch_failed(
+            "error: could not download file from 'https://releases.lean-lang.org/...'"
+        ));
+        assert!(!toolchain_fetch_failed(
+            "probe.lean:5:0: error: unknown identifier 'getTokenTable'"
+        ));
+        assert!(!toolchain_fetch_failed(""));
+    }
+
     #[test]
     fn escapes_reported_keyword_regressions_and_global_collisions() {
         for name in [
@@ -328,15 +361,30 @@ elab "#aver_reserved_tokens" : command => do
             .expect("write Lean token probe");
         drop(probe);
 
-        let output = match Command::new("lean")
-            .arg(&probe_path)
-            .current_dir(probe_dir.path())
-            .output()
-        {
+        let run_probe = || {
+            Command::new("lean")
+                .arg(&probe_path)
+                .current_dir(probe_dir.path())
+                .output()
+        };
+        let mut output = match run_probe() {
             Ok(output) => output,
             Err(error) if error.kind() == std::io::ErrorKind::NotFound => return,
             Err(error) => panic!("run Lean token probe: {error}"),
         };
+        // On a runner that has never used the pinned toolchain, this first
+        // `lean` call makes elan FETCH it — a network step that is not part
+        // of what this test decides, and whose transient failure would fail
+        // the proof workflow for a reason unrelated to the snapshot. Retry
+        // exactly once, and ONLY when the probe died on that fetch. A probe
+        // that failed for any other reason — and every token-table mismatch,
+        // which is decided below on a probe that SUCCEEDED — still fails
+        // loudly on the first attempt.
+        if !output.status.success()
+            && toolchain_fetch_failed(&String::from_utf8_lossy(&output.stderr))
+        {
+            output = run_probe().expect("re-run Lean token probe after toolchain fetch failure");
+        }
         assert!(
             output.status.success(),
             "Lean token probe failed:\nstdout:\n{}\nstderr:\n{}",

src/codegen/rust/from_mir.rs

@@ -1003,10 +1003,11 @@ pub(super) fn emit_mir_expr(expr: &Spanned<MirExpr>, emit_ctx: &MirEmitCtx<'_>)
                 };
                 // The method receiver is borrowed for the duration of the
                 // call. If a nested RHS expression consumes that local (for
-                // example `value - highNibble(value) * 16`), Rust rejects the
-                // receiver borrow followed by the move inside the argument.
-                // Clone only for that overlap; a direct `x + x` RHS is itself
-                // borrowed by this method call and remains `x.add(&x)`.
+                // example `n * factorial(n - 1)` in
+                // `examples/core/big_integers.av`), Rust rejects the receiver
+                // borrow followed by the move inside the argument. Clone only
+                // for that overlap; a direct `x + x` RHS is itself borrowed by
+                // this method call and remains `x.add(&x)`.
                 let lhs_rhs_move_overlap = local_of(&bop.lhs.node).is_some_and(|lhs| {
                     !matches!(&bop.rhs.node, MirExpr::Local(_))
                         && mir_expr_contains_last_use_of_slot(&bop.rhs.node, lhs.slot)

src/source.rs

@@ -123,6 +123,13 @@ pub fn stdlib_shadow_message(name: &str, shadowed_path: &str) -> String {
 /// Resolution runs several times per command (typecheck tree walk, dep
 /// compile walk, check units), and repeating the identical warning would
 /// drown the signal.
+///
+/// NOT suppressible, unlike the `stdlib-shadow` finding `aver check`
+/// reports — that one goes through the usual `[[check.suppress]]` filter,
+/// this one does not. Deliberate asymmetry: the loader runs on every
+/// command, has no `aver.toml` in hand at this depth, and what it reports
+/// is that the program being built is not the program on disk. See the
+/// `stdlib-shadow` entry in `docs/diagnostics-slugs.md`.
 fn warn_stdlib_shadow_once(name: &str, shadowed_path: &Path) {
     use std::sync::{Mutex, OnceLock};
     static WARNED: OnceLock<Mutex<HashSet<String>>> = OnceLock::new();

tests/proof_spec/cross_file.rs

@@ -935,3 +935,87 @@ fn entry_reserved_module_name_escapes_and_builds() {
     let _ = std::fs::remove_dir_all(&src);
     let _ = std::fs::remove_dir_all(&out);
 }
+
+/// `Lib` renamed to `Type` — a dep module whose name is a reserved Lean
+/// token, exporting the SAME proven law the split probe
+/// (`cross_file_consumer_proves_via_dep_law`) cites. The admissibility
+/// gate reads its mentions off the EMITTED statement, where the module
+/// segment carries the reserved-token guard (`Type'.qrev`), while the
+/// membership index / orientation set / citation name used to be built
+/// from the RAW `ModuleInfo::prefix` (`Type.qrev`). Nothing matched, so
+/// `mentions` came back empty and the dep law silently degraded to
+/// not-admitted: no theorem in `Type'.lean`, no citation in
+/// `Consumer.lean`. Same fixture under the name `Lib` is admitted and
+/// cited, so the module NAME alone decided proof strength.
+const TYPE_PROVEN: &str = "module Type\n\
+    \x20   intent =\n\
+    \x20       \"Reversal helpers with a proven accumulator-equivalence law.\"\n\
+    \x20   effects []\n\n\
+    fn qrev(x: List<Int>, y: List<Int>) -> List<Int>\n\
+    \x20   match x\n\
+    \x20       [] -> y\n\
+    \x20       [z, ..xs] -> qrev(xs, List.concat([z], y))\n\n\
+    fn rev(x: List<Int>) -> List<Int>\n\
+    \x20   match x\n\
+    \x20       [] -> []\n\
+    \x20       [y, ..xs] -> List.concat(rev(xs), [y])\n\n\
+    verify qrev law qrevSpec\n\
+    \x20   given x: List<Int> = [[], [1], [1, 2, 3]]\n\
+    \x20   given y: List<Int> = [[], [9], [8, 7]]\n\
+    \x20   qrev(x, y) => List.concat(rev(x), y)\n";
+
+const CONSUMER_USES_TYPE_DEP: &str = "module Consumer\n\
+    \x20   depends [Type]\n\
+    \x20   intent =\n\
+    \x20       \"Wraps Type.rev and proves it equals Type.qrev with empty accumulator.\"\n\
+    \x20   effects []\n\n\
+    fn myRev(x: List<Int>) -> List<Int>\n\
+    \x20   Type.rev(x)\n\n\
+    verify myRev law myRevQrev\n\
+    \x20   given x: List<Int> = [[], [1], [1, 2, 3]]\n\
+    \x20   myRev(x) => Type.qrev(x, [])\n";
+
+#[test]
+fn cross_file_reserved_module_name_dep_law_is_admitted_and_cited() {
+    if Command::new("lake").arg("--version").output().is_err() {
+        eprintln!("skipping reserved-module dep-law citation test: `lake` not available");
+        return;
+    }
+    let (summary, run, leans) = run_multi(
+        &[
+            ("Type.av", TYPE_PROVEN),
+            ("Consumer.av", CONSUMER_USES_TYPE_DEP),
+        ],
+        "Consumer.av",
+        &["Type'.lean", "Consumer.lean"],
+    );
+    let dep_lean = &leans["Type'.lean"];
+    assert!(
+        dep_lean.contains("theorem qrev_law_qrevSpec :"),
+        "the reserved-name dep module's cited law must be ADMITTED and therefore \
+         emitted as a theorem; empty mentions drop it silently\nType'.lean:\n{dep_lean}"
+    );
+    let consumer_lean = &leans["Consumer.lean"];
+    assert!(
+        consumer_lean.contains("Type'.qrev_law_qrevSpec"),
+        "the consumer proof must cite the dep law under its ESCAPED module \
+         segment\nConsumer.lean:\n{consumer_lean}"
+    );
+    assert!(
+        !consumer_lean.contains("Type."),
+        "no raw (unescaped) module segment may reach the emitted Lean — Lean \
+         cannot parse `Type.qrev_law_qrevSpec`\nConsumer.lean:\n{consumer_lean}"
+    );
+    assert_eq!(
+        (
+            summary["passed"].as_bool(),
+            summary["universal"].as_bool(),
+            summary["universal_laws"].as_u64(),
+            summary["sorries"].as_u64(),
+        ),
+        (Some(true), Some(true), Some(1), Some(0)),
+        "the reserved-name dep must give the consumer the SAME universal credit \
+         the `Lib`-named split probe gets\n{}",
+        format_output(&run)
+    );
+}

tests/stdlib_spec.rs

@@ -61,6 +61,45 @@ fn check_warns_when_project_module_is_shadowed_by_the_stdlib() {
     assert!(stderr.contains("bytes.av"), "{stderr}");
 }
 
+/// The loader's stderr warning is deduplicated once per process per module
+/// name (`source::warn_stdlib_shadow_once`), because module resolution runs
+/// several times inside one command — the typecheck tree walk, the dep
+/// compile walk, the per-unit check pass. Without the dedup a single
+/// `aver check --deps` prints the identical paragraph four times and
+/// drowns the signal it exists to carry. Counts the LOADER line only: the
+/// structured `warning[stdlib-shadow]:` finding is a separate channel with
+/// its own (suppressible) reporting.
+#[test]
+fn stdlib_shadow_loader_warning_is_printed_once_per_command() {
+    let dir = tempfile::tempdir().expect("tempdir");
+    std::fs::write(
+        dir.path().join("bytes.av"),
+        "module Bytes\n    intent = \"project-local Bytes\"\n    exposes [fromList]\n    effects []\n\nrecord Bytes\n    values: List<Int>\n\nfn fromList(xs: List<Int>) -> Result<Bytes, String>\n    ? \"Accept anything.\"\n    Result.Ok(Bytes(values = xs))\n",
+    )
+    .expect("write bytes.av");
+    let entry = dir.path().join("main.av");
+    std::fs::write(
+        &entry,
+        "module Main\n    intent = \"use Bytes\"\n    depends [Bytes]\n    effects []\n\nfn byteCount(values: List<Int>) -> Result<Int, String>\n    ? \"Validate bytes and count them.\"\n    bytes = Bytes.fromList(values)?\n    Result.Ok(List.len(Bytes.toList(bytes)))\n\nverify byteCount\n    byteCount([1, 2]) => Result.Ok(2)\n    byteCount([300]) => Result.Err(\"byte value outside 0..=255\")\n",
+    )
+    .expect("write main.av");
+    let root = dir.path().to_string_lossy().into_owned();
+    let entry_path = entry.to_string_lossy().into_owned();
+
+    let check = run_aver(&["check", &entry_path, "--module-root", &root, "--deps"]);
+    assert_success("aver check --deps (shadowed)", &check);
+    let stderr = String::from_utf8_lossy(&check.stderr);
+    let loader_lines = stderr
+        .lines()
+        .filter(|line| line.starts_with("warning: module 'Bytes' is reserved"))
+        .count();
+    assert_eq!(
+        loader_lines, 1,
+        "the loader's shadow warning must be emitted exactly once per process \
+         per module name, across every resolution phase of one command\nstderr:\n{stderr}"
+    );
+}
+
 #[test]
 fn check_stays_silent_when_no_project_file_shadows_the_stdlib() {
     let dir = tempfile::tempdir().expect("tempdir");