From 81945bd9e8153e12a045cb5f820fe162149cb839 Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Sun, 30 Aug 2026 20:39:33 +0700 Subject: [PATCH 1/2] feat(tri): `census audit` says what it does not check, and why One row added and two refused, which is the more useful half. ADDED -- `lean vacuous` prints 250 models, counted as `def NAME : Module := {`. The counter counts `theorem` lines in Completeness.lean instead: a different marker for the same population, and a real invariant -- one theorem per model -- that a hand-transcribed file of 250 entries can break in either direction. Mutation: comment out one theorem and the row reads 250 against 249, exit 1. REFUSED -- `types dup` prints 1180 struct definitions. A counter loose enough to be independent reads 1182, and the two extra are specs/lsp/schema.t27:155 struct = 21, specs/lsp/schema.t27:204 struct = 22, enum members named `struct`, which the census correctly rejects by requiring the name to start with an ascii letter. The census is right. Any counter accurate enough to agree with it is a copy of its matcher, which is the same reason `seals hollow` was removed last pass. REFUSED -- `discard classify` counts parser events produced at run time, not artefacts on disk. Counting them a second way means running the same parser. The pattern behind both refusals is worth naming: a census whose population is defined by a MATCHER cannot have an independent counter, because any counter precise enough to agree IS that matcher. Only a population defined by something external -- files on disk, workspace members, a marker in a different file -- can honestly be counted twice. So the audit now prints what it does not check and why. Its own coverage was the same class it exists to catch: a page of green rows looks like the whole story until somebody asks what is missing from it. Each exclusion carries the measurement that produced it, because otherwise a reader cannot tell "looked and could not" from "never looked". lean vacuous 250 250 `theorem` lines in Completeness.lean Not checked here, and why: seals hollow built and removed; planting a seal moved BOTH numbers types dup 1182 vs 1180, and the census is right discard classify run-time events, not artefacts A test refuses a census that appears in both lists, and refuses an exclusion shorter than 60 characters -- an exclusion is a measurement, not a shrug. Both mutation-checked. cargo test -p tri 389 passed, 0 failed (was 387; two new) cargo clippy 120 warnings, same as master Refs #2864 --- cli/tri/src/census.rs | 124 +++++++++++++++++- ...dit-says-what-it-does-not-check-and-why.md | 10 ++ 2 files changed, 133 insertions(+), 1 deletion(-) create mode 100644 docs/now/2026-08-30-the-audit-says-what-it-does-not-check-and-why.md diff --git a/cli/tri/src/census.rs b/cli/tri/src/census.rs index a46dd2d37..1751fca03 100644 --- a/cli/tri/src/census.rs +++ b/cli/tri/src/census.rs @@ -61,7 +61,7 @@ struct Row { reading: &'static str, } -const ROWS: [Row; 3] = [ +const ROWS: [Row; 4] = [ Row { census: "unparsed report", args: &["unparsed", "report"], @@ -89,6 +89,48 @@ const ROWS: [Row; 3] = [ soft: false, reading: "the census walked a list; this walks the cargo workspace", }, + Row { + census: "lean vacuous", + args: &["lean", "vacuous"], + marker: "models in the file", + nth: 0, + what: "`theorem` lines in Completeness.lean", + soft: false, + reading: "the census counts `def NAME : Module := {`; this counts the theorems, \ + one per model, and a hand-transcribed file can gain either without the other", + }, +]; + +/// A census this audit does NOT check, and the reason. +/// +/// Without this list the audit is narrow in exactly the way it exists to +/// catch: a page of green rows looks like coverage until somebody asks what is +/// not on it. Each entry is a measurement, not a shrug. +struct Uncovered { + census: &'static str, + why: &'static str, +} + +const UNCOVERED: [Uncovered; 3] = [ + Uncovered { + census: "seals hollow", + why: "built and removed. Its counter tested json text for `\"spec_path\"` while the \ + census parses that same field, so planting one more seal moved BOTH numbers \ + to 1314 and the row stayed green. No input makes them disagree.", + }, + Uncovered { + census: "types dup", + why: "measured: a counter loose enough to be independent reads 1182 where the census \ + reads 1180, and the two extra are `struct = 21,` -- enum members named `struct`, \ + which the census correctly rejects. Any counter accurate enough to agree is a \ + copy of its matcher.", + }, + Uncovered { + census: "discard classify", + why: "its population is parser events produced at run time, not artefacts on disk. \ + Counting them a second way means running the same parser, which is not a \ + second opinion.", + }, ]; /// Every number on a line, in order. @@ -282,10 +324,45 @@ fn independent(census: &str, repo: &Path) -> Result { } Ok(n) } + "lean vacuous" => { + // A different marker for the same population: the census counts + // `def NAME : Module := {`, this counts the theorem each model is + // supposed to carry. The file is found by name rather than by the + // path the census uses. + let mut v = Vec::new(); + walk(&repo.join("proofs"), "Completeness.lean", &mut v); + let p = v.first().ok_or_else(|| { + anyhow::anyhow!("no Completeness.lean under proofs/ -- nothing to count") + })?; + let src = std::fs::read_to_string(p)?; + Ok(src + .lines() + .filter(|l| l.trim_start().starts_with("theorem ")) + .count()) + } other => anyhow::bail!("no independent counter for {other}"), } } +/// Break a sentence into lines of at most `w` characters, on word boundaries. +fn wrap(s: &str, w: usize) -> Vec { + let mut out = Vec::new(); + let mut cur = String::new(); + for word in s.split_whitespace() { + if !cur.is_empty() && cur.len() + 1 + word.len() > w { + out.push(std::mem::take(&mut cur)); + } + if !cur.is_empty() { + cur.push(' '); + } + cur.push_str(word); + } + if !cur.is_empty() { + out.push(cur); + } + out +} + fn repo_root() -> Result { let out = std::process::Command::new("git") .args(["rev-parse", "--show-toplevel"]) @@ -369,6 +446,16 @@ pub fn run(cmd: &CensusCmd) -> Result<()> { ); } println!(" AGREED. Every census speaks about the population it prints."); + println!(); + println!(" Not checked here, and why -- because a page of green rows looks"); + println!(" like coverage until somebody asks what is missing from it:"); + for u in &UNCOVERED { + println!(); + println!(" {}", u.census); + for chunk in wrap(u.why, 68) { + println!(" {chunk}"); + } + } Ok(()) } @@ -422,6 +509,41 @@ mod tests { } } + /// A census is either checked or explicitly not, never neither. + /// + /// The audit's own coverage is the same class it exists to catch: a page + /// of green rows looks like the whole story. A name in both lists, or an + /// exclusion with no measurement behind it, puts it back there. + #[test] + fn nothing_is_both_checked_and_excused() { + for u in &UNCOVERED { + assert!( + !ROWS.iter().any(|r| r.census == u.census), + "{} is listed as unchecked and also has a row", + u.census + ); + assert!( + u.why.len() > 60, + "{}: an exclusion is a measurement, not a shrug -- {:?}", + u.census, + u.why + ); + } + } + + /// The reasons are printed, so they have to fit the page. + #[test] + fn a_reason_wraps_on_word_boundaries() { + let w = wrap("one two three four five", 9); + assert_eq!(w, vec!["one two", "three", "four five"]); + assert!(wrap("", 10).is_empty()); + // A word longer than the width is not cut in half. + assert_eq!( + wrap("supercalifragilistic ok", 8), + vec!["supercalifragilistic", "ok"] + ); + } + /// A soft row states why its difference is not a defect. /// /// Without that sentence a reader cannot tell "measured and forgiven" from diff --git a/docs/now/2026-08-30-the-audit-says-what-it-does-not-check-and-why.md b/docs/now/2026-08-30-the-audit-says-what-it-does-not-check-and-why.md new file mode 100644 index 000000000..0ec2c30af --- /dev/null +++ b/docs/now/2026-08-30-the-audit-says-what-it-does-not-check-and-why.md @@ -0,0 +1,10 @@ +# NOW -- The audit says what it does not check, and why (2026-08-30) + +## The audit says what it does not check, and why (Refs #2864) + +- New row: `lean vacuous` prints 250 models; the counter counts `theorem` lines in Completeness.lean. Different marker, same population, and a real invariant -- one theorem per model -- that a hand-transcribed file can break in either direction. Mutation: comment out one theorem and the row reads 250 against 249, exit 1. +- Two candidates were measured and REFUSED. `types dup` prints 1180 struct definitions; a counter loose enough to be independent reads 1182, and the two extra are `struct = 21,` -- enum members named struct, which the census correctly rejects. Any counter accurate enough to agree is a copy of its matcher. +- `discard classify` counts parser events produced at run time, not artefacts on disk; counting them a second way means running the same parser, which is not a second opinion. +- So the audit now prints what it does NOT check and why. Its own coverage was the same class it exists to catch: a page of green rows looks like the whole story until somebody asks what is missing from it. +- A test refuses a census that is in both lists, and refuses an exclusion under 60 characters -- an exclusion is a measurement, not a shrug. Both directions mutation-checked. +- Pattern that fell out of two refusals: a census whose population is defined by a MATCHER cannot have an independent counter, because any counter precise enough to agree is that matcher. Only populations defined by something external -- files on disk, workspace members, a marker in another file -- can be counted twice. From 71710afb11a2416b90351d35e2d0762a0634b918 Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Sun, 30 Aug 2026 20:40:16 +0700 Subject: [PATCH 2/2] skill(ci-gates) 382-383: a matcher-defined population cannot be counted twice; an exclusion is a measurement (Refs #2864) --- .claude/skills/ci-gates/SKILL.md | 43 ++++++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) diff --git a/.claude/skills/ci-gates/SKILL.md b/.claude/skills/ci-gates/SKILL.md index fbfea7e1c..c08e04fa0 100644 --- a/.claude/skills/ci-gates/SKILL.md +++ b/.claude/skills/ci-gates/SKILL.md @@ -9581,3 +9581,46 @@ file, not the crate") does not hold when the single file is a root. --stat` before every commit: five unrelated files is not a thing you notice in the test output, and on a shared repository it is somebody else's conflict tomorrow. + +## 382. A matcher-defined population cannot be counted twice + +Two candidates for a second opinion were measured and refused, and the refusals +name a rule the three working rows had been obeying by luck. + +`types dup` prints **1180** struct definitions. A counter loose enough to be +independent reads **1182**, and the two extra are + +``` +specs/lsp/schema.t27:155 struct = 21, +specs/lsp/schema.t27:204 struct = 22, +``` + +enum members *named* `struct`, which the census correctly rejects by requiring +the name to start with an ascii letter. **The census is right.** Any counter +accurate enough to agree with it is a copy of its matcher -- exactly why the +`seals hollow` row was removed one pass earlier, where both sides tested the +same json field and a planted seal moved both numbers. + +> **A census whose population is defined by a MATCHER cannot have an independent +> counter, because any counter precise enough to agree IS that matcher. Only a +> population defined by something EXTERNAL -- files on disk, workspace members, +> a marker in a different file -- can honestly be counted twice.** + +The rows that work obey it: `.t27` on disk, `.rs` under the cargo workspace, the +bare letters of a keyword, `theorem` lines in a file the census reads for +something else. Before building a differential row, ask what defines its +population. If the answer is "the code under test", stop. + +## 383. An exclusion is a measurement, not a shrug + +Having refused two rows, the audit had three green rows and no statement of what +it was not checking -- its own coverage in exactly the shape it exists to catch. +It now prints the uncovered censuses with the measurement behind each: what was +tried, what it read, and why the two routes cannot disagree. + +Enforced rather than intended: a test refuses a census that appears in both +lists, and refuses a reason shorter than sixty characters. `"too hard"` fails. + +The distinction being preserved is the one this whole document keeps circling: +a reader must be able to tell **"looked and could not"** from **"never looked"**, +and a blank space says the second while meaning the first.