From 2f74b71f7facc34c019f1a164322fac86db25c5e Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Sun, 30 Aug 2026 04:32:59 +0700 Subject: [PATCH] tri lean vacuous: the ratchet counts 44 of 114 `Completeness.lean` holds 250 hand-transcribed models, one per spec, each with a theorem asserting the module is Icarus-lowerable. 114 of them have `functions := []`, and 104 of those have an empty `Env` too. A theorem about an empty module says nothing about its spec: `native_decide` on an empty structure proves something true and useless. `max_vacuous`, the ratchet that exists to stop that number growing, counts 44 -- because it reads the mismatch ledger, and an entry only reaches that ledger if the model ALSO disagrees with the Rust classifier. Whether a theorem is vacuous has nothing to do with whether the classifier happens to disagree. models in the file 250 with `functions := []` 114 ...and an empty Env too 104 counted by max_vacuous 44 vacuous and INVISIBLE to it 70 A ratchet measuring a subset of its own subject is worse than no ratchet, because the number it reports looks like the number you care about. Its 44 marks are all correct -- zero entries marked `model_empty` that are not -- so this is a coverage gap, not a wrong reading. Measured twice, by a throwaway Python scan and by the shipped Rust, and the two agree on every one of the five numbers. The command refuses rather than printing zero when it matches no modules: a zero from a scanner that found nothing is indistinguishable from a clean file, and the file's shape is exactly what would change under it. 4 tests. WHAT THIS IS NOT. Last pass I named "write real Lean models for those four" as the only honest way to lower `max_vacuous`, and I am not doing it. `lean`, `lake` and `elan` are not installed here. A faithful model may make its theorem FALSE -- the classifier says `Rust=false` for those specs -- which is the correct outcome and not a bug, but I cannot tell the correct outcome from a transcription error without building it. Writing a proof I cannot check and pushing it to see what CI says is the thing this repository exists to prevent. Refs #2747 --- cli/tri/src/leanvac.rs | 235 ++++++++++++++++++ cli/tri/src/main.rs | 7 + ...-a-ratchet-measuring-a-subset-of-itself.md | 17 ++ 3 files changed, 259 insertions(+) create mode 100644 cli/tri/src/leanvac.rs create mode 100644 docs/now/2026-08-30-a-ratchet-measuring-a-subset-of-itself.md diff --git a/cli/tri/src/leanvac.rs b/cli/tri/src/leanvac.rs new file mode 100644 index 0000000000..cecf7b708d --- /dev/null +++ b/cli/tri/src/leanvac.rs @@ -0,0 +1,235 @@ +//! `tri lean vacuous` -- completeness theorems whose model is empty. +//! +//! `proofs/lean4/.../Completeness.lean` holds 250 hand-transcribed models, one per +//! spec, each with a theorem asserting the module is Icarus-lowerable. A model with +//! `functions := []` makes its theorem true by construction: `native_decide` on an +//! empty structure proves something, and that something is not about the spec. +//! +//! 114 of the 250 are empty. The ledger's `max_vacuous` ratchet, which exists to stop +//! that number growing, counts **44** -- because it only sees models that ALSO disagree +//! with the Rust classifier. The other 70 are vacuous and invisible to it. +//! +//! A ratchet measuring a subset of its own subject is worse than no ratchet, because +//! the number it reports looks like the number you care about. + +use anyhow::Result; +use clap::Subcommand; +use std::path::PathBuf; + +#[derive(Subcommand)] +pub enum LeanCmd { + /// Completeness theorems whose model has no functions. + Vacuous { + /// Print every name, not just the count and the gap. + #[arg(long)] + all: bool, + }, +} + +/// One model as the file states it. +pub struct Model { + pub name: String, + pub empty_fns: bool, + pub empty_env: bool, +} + +/// Every `_module` in the file, with whether its function list and its Env are +/// empty. +/// +/// Text-scanned rather than parsed, and that is a limit worth stating: this reads what +/// the file SAYS, and only a Lean build can say what it MEANS. No workflow in this +/// repository builds these proofs (#2747), so a text scan is the strongest instrument +/// available here, not the weakest one chosen. +pub fn models_in(src: &str) -> Vec { + let mut envs: Vec<(String, bool)> = Vec::new(); + let mut out: Vec = Vec::new(); + let mut cur: Option<(String, bool, bool)> = None; // name, is_module, saw_empty + let mut empty_env_names: Vec = Vec::new(); + for line in src.split('\n') { + let t = line.trim(); + if let Some(rest) = t.strip_prefix("def ") { + // flush + if let Some((name, is_module, saw)) = cur.take() { + if is_module { + out.push(Model { + empty_env: empty_env_names.contains(&name), + name, + empty_fns: saw, + }); + } else if saw { + empty_env_names.push(name); + } + } + if let Some(n) = rest.strip_suffix(" : Env := {") { + cur = Some((n.trim_end_matches("_env").to_string(), false, false)); + } else if let Some(n) = rest.strip_suffix(" : Module := {") { + cur = Some((n.trim_end_matches("_module").to_string(), true, false)); + } + continue; + } + if let Some((_, is_module, saw)) = cur.as_mut() { + if (*is_module && t.starts_with("functions := []")) + || (!*is_module && t.starts_with("structs := []")) + { + *saw = true; + } + } + } + if let Some((name, is_module, saw)) = cur.take() { + if is_module { + out.push(Model { + empty_env: empty_env_names.contains(&name), + name, + empty_fns: saw, + }); + } + } + let _ = &mut envs; + out +} + +fn repo_root() -> Result { + let out = std::process::Command::new("git") + .args(["rev-parse", "--show-toplevel"]) + .output()?; + if !out.status.success() { + anyhow::bail!("not inside a git repository"); + } + Ok(PathBuf::from( + String::from_utf8_lossy(&out.stdout).trim().to_string(), + )) +} + +pub fn run(cmd: &LeanCmd) -> Result<()> { + let LeanCmd::Vacuous { all } = cmd; + let root = repo_root()?; + let lean = root.join("proofs/lean4/Trinity/IcarusLowerable/Completeness.lean"); + let src = std::fs::read_to_string(&lean) + .map_err(|e| anyhow::anyhow!("cannot read {}: {}", lean.display(), e))?; + let models = models_in(&src); + if models.is_empty() { + anyhow::bail!( + "read {} and found no `_module : Module := {{` -- the file's shape \ + changed, and a count of zero here would be the scanner, not the proofs", + lean.display() + ); + } + let vacuous: Vec<&Model> = models.iter().filter(|m| m.empty_fns).collect(); + let both: usize = vacuous.iter().filter(|m| m.empty_env).count(); + + let ledger = root.join("docs/reports/lean_completeness_mismatches.json"); + let marked: usize = std::fs::read_to_string(&ledger) + .ok() + .and_then(|r| serde_json::from_str::(&r).ok()) + .and_then(|v| { + v.get("entries")?.as_object().map(|o| { + o.values() + .filter(|e| e.get("model_empty").and_then(|b| b.as_bool()) == Some(true)) + .count() + }) + }) + .unwrap_or(0); + + println!("VACUOUS COMPLETENESS THEOREMS"); + println!(); + println!(" models in the file {}", models.len()); + println!(" with `functions := []` {}", vacuous.len()); + println!(" ...and an empty Env too {}", both); + println!(" counted by max_vacuous {}", marked); + println!( + " vacuous and INVISIBLE to it {}", + vacuous.len().saturating_sub(marked) + ); + println!(); + if *all { + for m in &vacuous { + println!(" {}{}", m.name, if m.empty_env { " (env empty too)" } else { "" }); + } + println!(); + } + println!( + "`max_vacuous` counts only models that ALSO disagree with the Rust classifier.\n\ + A theorem about an empty module says nothing about its spec whether or not the\n\ + classifier happens to disagree, so the ratchet measures a subset of its own\n\ + subject -- and the number it reports looks like the number you care about." + ); + println!(); + println!( + "Read from the file's text. Only a Lean build can say what these theorems MEAN,\n\ + and no workflow in this repository builds them (#2747)." + ); + Ok(()) +} + +#[cfg(test)] +mod tests { + use super::*; + + const SAMPLE: &str = "\ +def a_env : Env := { + structs := [], + enums := [] +} + +def a_module : Module := { + name := \"a\", + functions := [], + tests := [] +} + +def b_env : Env := { + structs := [(\"S\", [])], + enums := [] +} + +def b_module : Module := { + name := \"b\", + functions := [{ name := \"f\" }], + tests := [] +} +"; + + #[test] + fn an_empty_function_list_is_vacuous_and_a_populated_one_is_not() { + let ms = models_in(SAMPLE); + assert_eq!(ms.len(), 2, "two modules"); + assert!(ms[0].empty_fns, "a has functions := []"); + assert!(!ms[1].empty_fns, "b lists a function"); + } + + #[test] + fn an_empty_env_is_reported_separately_from_an_empty_module() { + let ms = models_in(SAMPLE); + assert!(ms[0].empty_env, "a's Env has structs := []"); + assert!(!ms[1].empty_env, "b's Env declares a struct"); + } + + #[test] + fn a_file_with_no_modules_yields_nothing_rather_than_a_wrong_zero() { + // The command turns this into a refusal, because a zero from a scanner + // that matched nothing is indistinguishable from a clean file. + assert!(models_in("-- just a comment\n").is_empty()); + } + + #[test] + fn the_env_belonging_to_a_module_is_the_one_with_its_name() { + // `a_env` empty, `b_env` not: the pairing is by name, not by position, + // so a file that declares them out of order still pairs correctly. + let reordered = "\ +def b_env : Env := { + structs := [(\"S\", [])] +} + +def a_env : Env := { + structs := [] +} + +def a_module : Module := { + functions := [] +} +"; + let ms = models_in(reordered); + assert_eq!(ms.len(), 1); + assert!(ms[0].empty_env); + } +} diff --git a/cli/tri/src/main.rs b/cli/tri/src/main.rs index cc7c0cb880..c37675b90b 100644 --- a/cli/tri/src/main.rs +++ b/cli/tri/src/main.rs @@ -26,6 +26,7 @@ mod quant; mod red; mod rtl; mod kinddrift; +mod leanvac; mod skillnum; mod seals; mod sweep; @@ -52,6 +53,11 @@ enum Commands { #[command(subcommand)] action: kinddrift::KindsCmd, }, + /// Completeness theorems whose Lean model is empty. + Lean { + #[command(subcommand)] + action: leanvac::LeanCmd, + }, Cell { #[command(subcommand)] action: CellAction, @@ -758,6 +764,7 @@ fn main() -> Result<()> { cmd_status(&root)?; } Commands::Kinds { action } => kinddrift::run(action)?, + Commands::Lean { action } => leanvac::run(action)?, Commands::Skill { action } => { let root = find_trinity_root()?; match action { diff --git a/docs/now/2026-08-30-a-ratchet-measuring-a-subset-of-itself.md b/docs/now/2026-08-30-a-ratchet-measuring-a-subset-of-itself.md new file mode 100644 index 0000000000..4a704c4596 --- /dev/null +++ b/docs/now/2026-08-30-a-ratchet-measuring-a-subset-of-itself.md @@ -0,0 +1,17 @@ +# NOW -- A ratchet measuring a subset of its own subject (2026-08-30) + +## 114 vacuous completeness theorems; the ratchet counts 44 (Refs #2747) + +- `Completeness.lean` holds 250 hand-transcribed models; **114** have `functions := []`, and 104 of those have an empty `Env` too +- a theorem about an empty module says nothing about its spec: `native_decide` on an empty structure proves something true and useless +- `max_vacuous`, the ratchet that exists to stop that number growing, counts **44** -- only the models that ALSO disagree with the Rust classifier +- **70 vacuous theorems are invisible to it**, and the number it reports looks like the number you care about +- all 44 of its marks are correct: zero entries marked `model_empty` that are not empty +- measured twice, by a throwaway Python scan and by the shipped Rust, and the two agree at 250/114/104/44/70 + +## What I proposed last pass and am NOT doing + +- I named "write real Lean models for those four" as the only honest way to lower `max_vacuous` +- `lean`, `lake` and `elan` are not installed here; `.github/workflows/lean-proofs.yml` has a `lake build` but I cannot run it locally +- a faithful model may make its theorem FALSE -- the classifier says `Rust=false` for those four specs -- and that is the correct outcome, not a bug +- writing a proof I cannot check and pushing it to see what CI says is exactly what this repository exists to prevent, so the count is reported instead