diff --git a/docs/diagnostics-slugs.md b/docs/diagnostics-slugs.md index d79b43aa4..4f62b1b75 100644 --- a/docs/diagnostics-slugs.md +++ b/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 | diff --git a/src/codegen/lean/law_auto/induction/mod.rs b/src/codegen/lean/law_auto/induction/mod.rs index ac60e59d1..f349d35ab 100644 --- a/src/codegen/lean/law_auto/induction/mod.rs +++ b/src/codegen/lean/law_auto/induction/mod.rs @@ -458,6 +458,22 @@ fn program_fn_lean_names(ctx: &CodegenContext) -> BTreeSet { .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.`; the EMIT side keys - // on `(prefix, theorem_base)`. - if let Some(base) = name.strip_prefix(&format!("{}.", module.prefix)) { + // `name` is the CITATION spelling + // (`.`); 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))); } } } diff --git a/src/codegen/lean/syntax.rs b/src/codegen/lean/syntax.rs index bd7e6d1f7..53b42c4eb 100644 --- a/src/codegen/lean/syntax.rs +++ b/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{}", diff --git a/src/codegen/rust/from_mir.rs b/src/codegen/rust/from_mir.rs index dbbeaa3ff..0d1dd03dd 100644 --- a/src/codegen/rust/from_mir.rs +++ b/src/codegen/rust/from_mir.rs @@ -1003,10 +1003,11 @@ pub(super) fn emit_mir_expr(expr: &Spanned, 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) diff --git a/src/source.rs b/src/source.rs index d2da974bc..661648ade 100644 --- a/src/source.rs +++ b/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>> = OnceLock::new(); diff --git a/tests/proof_spec/cross_file.rs b/tests/proof_spec/cross_file.rs index f3839e23e..6470c0701 100644 --- a/tests/proof_spec/cross_file.rs +++ b/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, y: List) -> List\n\ + \x20 match x\n\ + \x20 [] -> y\n\ + \x20 [z, ..xs] -> qrev(xs, List.concat([z], y))\n\n\ + fn rev(x: List) -> List\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 = [[], [1], [1, 2, 3]]\n\ + \x20 given y: List = [[], [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) -> List\n\ + \x20 Type.rev(x)\n\n\ + verify myRev law myRevQrev\n\ + \x20 given x: List = [[], [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) + ); +} diff --git a/tests/stdlib_spec.rs b/tests/stdlib_spec.rs index d85efd387..ea7ffda18 100644 --- a/tests/stdlib_spec.rs +++ b/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\n\nfn fromList(xs: List) -> Result\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) -> Result\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"); diff --git a/tests/wasip2_codegen_regression.rs b/tests/wasip2_codegen_regression.rs index da2f32881..fbc6d045f 100644 --- a/tests/wasip2_codegen_regression.rs +++ b/tests/wasip2_codegen_regression.rs @@ -429,6 +429,68 @@ fn main() -> Unit ); } +/// GRADUATED CLOSE — the effect-gating counterpart of the test above. +/// `shutdown` takes a `Tcp.Connection` the caller already owns and +/// declares only `! [Tcp.close]`; the program never names `Tcp.connect`, +/// so no connect helper and no connect-gated slot exist. The close helper +/// still needs `parse_id`, which is why `wasip2_tcp::wireup::allocate` +/// gates `parse_id` on the UNION of the pool-consuming effects +/// (`TcpClose` included) rather than on the connect helper: gating on +/// connect would leave `allocate_close`'s `parse_id?` unsatisfied and the +/// emit path would hit an `expect`. Pins that the union gate keeps +/// working — a connect-shaped gate makes this program fail to compile. +#[test] +fn wasip2_tcp_close_without_connect_keeps_the_close_helper() { + let source = r#"module Probe + intent = "Close a TCP connection the caller already owns." + exposes [shutdown] + effects [Tcp.close] + +fn shutdown(conn: Tcp.Connection) -> Result + ? "Release a connection handed in by the caller." + ! [Tcp.close] + Tcp.close(conn) +"#; + let items = parse_pipeline(source).unwrap_or_else(|e| panic!("{e}\n--- source ---\n{source}")); + let bytes = aver::codegen::wasm_gc::compile_to_wasm_gc_for_wasip2(&items, None) + .unwrap_or_else(|e| panic!("wasip2 core compile: {e}\n--- source ---\n{source}")); + + let (segments, body_refs) = segments_and_body_data_refs(&bytes); + let referenced = |seg: u32| -> bool { body_refs.iter().any(|refs| refs.contains(&seg)) }; + + // Present: the close helper's own error segment. In a close-only + // program `__rt_tcp_close` is the sole body that can reference it — + // write_line / read_line / read_bytes share the text but none of + // their effects is declared here. + let unknown = segment_idx(&segments, b"tcp: unknown connection"); + assert!( + referenced(unknown), + "Tcp.close is declared — the close helper body must be emitted even \ + though the program never calls Tcp.connect" + ); + + // Absent: nothing declares Tcp.connect, so its pool-limit segment must + // not be referenced by any body (it need not be interned at all). + let connect_limit = b"tcp: connection limit reached (256 max)"; + let connect_referenced = segments + .iter() + .position(|seg| seg == connect_limit) + .is_some_and(|idx| referenced(idx as u32)); + assert!( + !connect_referenced, + "Tcp.connect is not declared — the connect helper must not be emitted" + ); + + let (component_bytes, _) = aver::codegen::wasip2::compile_to_component( + &bytes, + aver::codegen::wasip2::Wasip2World::CliCommand, + ) + .unwrap_or_else(|e| panic!("wasip2 component wrap: {e}\n--- source ---\n{source}")); + wasmparser::Validator::new_with_features(wasmparser::WasmFeatures::default()) + .validate_all(&component_bytes) + .unwrap_or_else(|e| panic!("component validate: {e}\n--- source ---\n{source}")); +} + /// `Tcp.readBytes` count-error classification on native wasip2 must /// match the VM (`src/services/tcp.rs` `count_arg` + /// `aver_rt::tcp::read_bytes`), branch by branch: