From 09ec489ec00de50ff09b242fa35918c0e477529b Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Sat, 29 Aug 2026 16:44:36 +0700 Subject: [PATCH 1/2] feat(tri): the quantifier census -- 100 walkable domains out of 1005 `tri quantifiers report`. Reading only: no parse changes, no lowering, no generated artefact, no discard count moves. WHY THIS AND NOT A LOWERING. Three independently written proposals for #2774 -- one arguing to capture and never lower, one to enumerate finite domains, one to split the four backends apart -- were judged through two adversarial lenses each and all three survived. They disagree about the lowering and they agree exactly about the FIRST STEP: report before you lower, because the ceiling cannot be chosen without the distribution of domain sizes, and nobody had measured it. quantified clauses found 1005 colon 12 invariant name: forall c : Cfg, ... prefix 858 forall input : InferenceInput suffix-all 120 assert p(a) == p(b) for all Trit suffix-any 15 ... for any a, b in {1, -1} DOMAIN, from declared types only, ceiling 65536 walkable 100 finite but over the ceiling 222 unbounded 544 no binder this can read 139 largest walkable domain 65536 (specs/igla/race/ternary_mac.t27:941) ALL 135 SUFFIX FORMS HAVE NO READABLE BINDER. `for all Trit` names a type with three values and no variable to range over it; `for any a, b in {1, -1}` names a set the language has no syntax for. The small domains are exactly the ones written without a binder, which is the opposite of convenient. WHAT `|D|` MEANS, and what it deliberately does not: * computed from DECLARED TYPES ALONE. A binder over `Trit` is 3 whatever the body says about it. * `BOTTOM` (printed `unbounded`) is absorbing, and AN UNRESOLVED NAME IS NOT ASSUMED SMALL -- `string`, `[]T` with no pinned length, and a type this cannot resolve are all unbounded. * 15 struct names have MORE THAN ONE definition in the corpus and are treated as unbounded. Picking one would change `|D|` by an unbounded factor with nothing recording which was picked. * NO GUARD IS READ. `x.len() == 4` narrows nothing here. That is the part that needs a semantics, and this report must not be the thing that quietly decides one. Six tests, four of them for what it must NOT conclude: an unknown type is unbounded rather than 1, an unpinned array length is unbounded rather than its element size, a struct defined twice is unbounded even though its fields resolve, and a prose suffix yields no binder rather than a wrong one. Refs #2774 Co-Authored-By: Claude Opus 5 --- cli/tri/src/main.rs | 7 + cli/tri/src/quant.rs | 439 ++++++++++++++++++ ...census-100-walkable-domains-out-of-1005.md | 8 + 3 files changed, 454 insertions(+) create mode 100644 cli/tri/src/quant.rs create mode 100644 docs/now/2026-08-29-the-quantifier-census-100-walkable-domains-out-of-1005.md diff --git a/cli/tri/src/main.rs b/cli/tri/src/main.rs index 768053318c..44ac96130f 100644 --- a/cli/tri/src/main.rs +++ b/cli/tri/src/main.rs @@ -19,6 +19,7 @@ mod mutate; mod nownote; mod reseal; mod prcheck; +mod quant; mod red; mod rtl; mod skillnum; @@ -135,6 +136,11 @@ enum Commands { #[command(subcommand)] action: abandoned::AbandonedCmd, }, + /// Every quantified clause, its binders, and the size of its domain. + Quantifiers { + #[command(subcommand)] + action: quant::QuantCmd, + }, /// What the parser reads and throws away, ranked against its pinned bound. Discard { #[command(subcommand)] @@ -770,6 +776,7 @@ fn main() -> Result<()> { Commands::Vectors { action } => vectors::run(action)?, Commands::Rtl { action } => rtl::run(action)?, Commands::Abandoned { action } => abandoned::run(action)?, + Commands::Quantifiers { action } => quant::run(action)?, Commands::Discard { action } => discard::run(action)?, Commands::Seals { action } => seals::run(action)?, Commands::Hooks { action } => hooks::run(action)?, diff --git a/cli/tri/src/quant.rs b/cli/tri/src/quant.rs new file mode 100644 index 0000000000..903501fe44 --- /dev/null +++ b/cli/tri/src/quant.rs @@ -0,0 +1,439 @@ +//! Every quantified clause in the corpus, with the size of the domain it ranges +//! over. +//! +//! WHY THIS EXISTS +//! --------------- +//! 90% of everything the t27 parser discards is universal quantification, in +//! four notations. What to DO about that is #2774, an owner decision that binds +//! four backends. Three independently written proposals for it disagreed about +//! the lowering and agreed exactly about the first step: **report before you +//! lower**, because the ceiling cannot be chosen without knowing the +//! distribution of domain sizes, and nobody has ever measured it. +//! +//! This is that report and nothing else. It changes no parse, no lowering, no +//! generated artefact, and no discard count. It reads the specs. +//! +//! WHAT A DOMAIN SIZE MEANS HERE +//! ----------------------------- +//! `|D|` is computed from DECLARED TYPES ALONE -- never from a guard, never from +//! a value. A binder over `Trit` ranges over 3 values whatever the body says +//! about it. Guard narrowing (`x.len() == 4` collapsing a slice axis) is +//! deliberately NOT implemented: it is the part that needs a semantics, and this +//! command must not be the thing that quietly decides one. +//! +//! `BOTTOM` -- printed as `unbounded` -- is absorbing. A product with one +//! unbounded axis is unbounded. That is the honest answer for `string`, for a +//! slice with no pinned length, and for a type this command cannot resolve: +//! **an unresolved name is not assumed small.** +use anyhow::{Context, Result}; +use clap::Subcommand; +use std::collections::BTreeMap; +use std::path::PathBuf; + +#[derive(Subcommand)] +pub enum QuantCmd { + /// Every quantified clause, its binders, and the size of its domain. + Report { + /// Print one line per clause instead of the summary. + #[arg(long)] + full: bool, + /// Domain sizes at or below this are called walkable. Choosing this + /// number is the decision this report exists to inform; the default is + /// deliberately small. + #[arg(long, default_value_t = 65536u128)] + ceiling: u128, + }, +} + +/// What the type of one binder is worth. +#[derive(Clone, Copy, PartialEq, Eq, Debug)] +enum Size { + /// A finite, statically known count. + Finite(u128), + /// Not computable from the declaration. Absorbing. + Unbounded, +} + +fn primitive(t: &str) -> Option { + Some(match t { + "bool" => 2, + "Trit" | "trit" => 3, + "u2" | "i2" => 4, + "u4" | "i4" => 16, + "u8" | "i8" | "char" => 256, + "u16" | "i16" => 65_536, + "u32" | "i32" | "f32" => 1u128 << 32, + "u64" | "i64" | "usize" | "isize" | "f64" => 1u128 << 64, + "u128" | "i128" => u128::MAX, + _ => return None, + }) +} + +/// `struct Name { field: Type, ... }` as written in the specs, by name. +/// +/// A name defined more than once is recorded as CONFLICTED and treated as +/// unbounded: 50 struct names in this corpus have several definitions, and +/// picking one of them would change `|D|` by an unbounded factor with nothing +/// saying which was picked. +struct Structs { + fields: BTreeMap>, + conflicted: std::collections::BTreeSet, +} + +fn scan_structs(specs: &[(PathBuf, String)]) -> Structs { + let mut fields: BTreeMap> = BTreeMap::new(); + let mut conflicted = std::collections::BTreeSet::new(); + for (_, src) in specs { + let lines: Vec<&str> = src.lines().collect(); + let mut i = 0usize; + while i < lines.len() { + let t = lines[i].trim(); + let Some(rest) = t.strip_prefix("struct ") else { + i += 1; + continue; + }; + let name = rest + .split(|c: char| c == '{' || c.is_whitespace()) + .next() + .unwrap_or("") + .trim() + .to_string(); + if name.is_empty() { + i += 1; + continue; + } + let mut fs = Vec::new(); + let mut j = i + 1; + while j < lines.len() { + let l = lines[j].trim(); + if l.starts_with('}') { + break; + } + if let Some((_, ty)) = l.split_once(':') { + let ty = ty.trim().trim_end_matches(',').trim(); + if !ty.is_empty() && !ty.starts_with("//") { + fs.push(ty.to_string()); + } + } + j += 1; + } + if let Some(prev) = fields.get(&name) { + if *prev != fs { + conflicted.insert(name.clone()); + } + } + fields.insert(name, fs); + i = j + 1; + } + } + Structs { fields, conflicted } +} + +fn size_of(ty: &str, s: &Structs, depth: usize) -> Size { + let ty = ty.trim().trim_end_matches(',').trim(); + if depth > 8 { + return Size::Unbounded; + } + if let Some(n) = primitive(ty) { + return Size::Finite(n); + } + // `[N]T` is |T|^N when N is a literal; `[]T` and `[T]` have no pinned length. + if let Some(rest) = ty.strip_prefix('[') { + if let Some((n, elem)) = rest.split_once(']') { + let n = n.trim(); + if n.is_empty() { + return Size::Unbounded; + } + if let Ok(k) = n.parse::() { + if let Size::Finite(e) = size_of(elem, s, depth + 1) { + return match e.checked_pow(k.min(64)) { + Some(v) => Size::Finite(v), + None => Size::Finite(u128::MAX), + }; + } + } + return Size::Unbounded; + } + } + if s.conflicted.contains(ty) { + return Size::Unbounded; + } + if let Some(fs) = s.fields.get(ty) { + let mut acc: u128 = 1; + for f in fs { + match size_of(f, s, depth + 1) { + Size::Finite(n) => acc = acc.saturating_mul(n), + Size::Unbounded => return Size::Unbounded, + } + } + return Size::Finite(acc); + } + Size::Unbounded +} + +#[derive(Clone)] +struct Clause { + file: String, + line: usize, + notation: &'static str, + binders: Vec<(String, String)>, + text: String, +} + +/// The four notations, recognised on the source line. +fn scan_clauses(specs: &[(PathBuf, String)]) -> Vec { + let mut out = Vec::new(); + for (p, src) in specs { + for (i, raw) in src.lines().enumerate() { + let t = raw.trim(); + let (notation, binder_text) = if let Some(r) = t.strip_prefix("forall ") { + ("prefix", r.to_string()) + } else if let Some(idx) = t.find(": forall ") { + ("colon", t[idx + 9..].to_string()) + } else if let Some(idx) = t.find(" for all ") { + ("suffix-all", t[idx + 9..].to_string()) + } else if let Some(idx) = t.find(" for any ") { + ("suffix-any", t[idx + 9..].to_string()) + } else { + continue; + }; + // `x : T, y : U, ` -- binders are the leading `name : Type` + // pairs. A comma-separated piece with no colon ends the binder list; + // everything after it is body, and this command does not read bodies. + let mut binders = Vec::new(); + for piece in binder_text.split(',') { + let piece = piece.trim(); + let Some((n, ty)) = piece.split_once(':') else { + break; + }; + let n = n.trim(); + let ty = ty.trim(); + if n.is_empty() || ty.is_empty() || n.contains(' ') { + break; + } + binders.push((n.to_string(), ty.to_string())); + } + out.push(Clause { + file: p.display().to_string(), + line: i + 1, + notation, + binders, + text: t.to_string(), + }); + } + } + out +} + +fn repo_root() -> Result { + let out = std::process::Command::new("git") + .args(["rev-parse", "--show-toplevel"]) + .output() + .context("running `git rev-parse --show-toplevel`")?; + if !out.status.success() { + anyhow::bail!("not inside a git repository"); + } + Ok(PathBuf::from(String::from_utf8(out.stdout)?.trim())) +} + +fn read_specs(root: &std::path::Path) -> Vec<(PathBuf, String)> { + let mut out = Vec::new(); + let mut stack = vec![root.join("specs")]; + while let Some(d) = stack.pop() { + let Ok(rd) = std::fs::read_dir(&d) else { + continue; + }; + for e in rd.flatten() { + let p = e.path(); + if p.is_dir() { + if p.file_name().map(|n| n == "scratch").unwrap_or(false) { + continue; + } + stack.push(p); + } else if p.extension().and_then(|x| x.to_str()) == Some("t27") { + if let Ok(s) = std::fs::read_to_string(&p) { + let rel = p.strip_prefix(root).unwrap_or(&p).to_path_buf(); + out.push((rel, s)); + } + } + } + } + out.sort_by(|a, b| a.0.cmp(&b.0)); + out +} + +pub fn run(cmd: &QuantCmd) -> Result<()> { + let QuantCmd::Report { full, ceiling } = cmd; + let root = repo_root()?; + let specs = read_specs(&root); + if specs.is_empty() { + anyhow::bail!( + "no specs under {}/specs -- nothing was read", + root.display() + ); + } + let structs = scan_structs(&specs); + let clauses = scan_clauses(&specs); + + let mut by_notation: BTreeMap<&str, usize> = BTreeMap::new(); + let (mut walkable, mut over, mut unbounded, mut no_binder) = (0usize, 0usize, 0usize, 0usize); + let mut walkable_sizes: Vec<(u128, String, usize)> = Vec::new(); + + for c in &clauses { + *by_notation.entry(c.notation).or_default() += 1; + if c.binders.is_empty() { + no_binder += 1; + if *full { + println!(" {}:{} no binder ({})", c.file, c.line, c.notation); + } + continue; + } + let mut total: Option = Some(1); + for (_, ty) in &c.binders { + match size_of(ty, &structs, 0) { + Size::Finite(n) => total = total.map(|t| t.saturating_mul(n)), + Size::Unbounded => { + total = None; + break; + } + } + } + let verdict = match total { + None => { + unbounded += 1; + "unbounded".to_string() + } + Some(n) if n <= *ceiling => { + walkable += 1; + walkable_sizes.push((n, c.file.clone(), c.line)); + format!("walkable |D| = {n}") + } + Some(n) => { + over += 1; + format!("finite but over ceiling |D| = {n}") + } + }; + if *full { + println!( + " {}:{} {} [{}] {}", + c.file, + c.line, + verdict, + c.binders + .iter() + .map(|(n, t)| format!("{n}: {t}")) + .collect::>() + .join(", "), + &c.text[..c.text.len().min(52)] + ); + } + } + + println!(); + println!(" quantified clauses found {}", clauses.len()); + for (n, k) in &by_notation { + println!(" {:<26} {}", n, k); + } + println!(); + println!(" DOMAIN, from declared types only, ceiling {ceiling}"); + println!(" walkable {walkable}"); + println!(" finite but over the ceiling {over}"); + println!(" unbounded {unbounded}"); + println!(" no binder this can read {no_binder}"); + if !walkable_sizes.is_empty() { + walkable_sizes.sort(); + let biggest = walkable_sizes.last().unwrap(); + println!(); + println!( + " largest walkable domain {} ({}:{})", + biggest.0, biggest.1, biggest.2 + ); + } + if !structs.conflicted.is_empty() { + println!(); + println!( + " {} struct name(s) have MORE THAN ONE definition and are treated as", + structs.conflicted.len() + ); + println!(" unbounded. Picking one would change |D| by an unbounded factor with"); + println!(" nothing recording which was picked:"); + for n in structs.conflicted.iter().take(8) { + println!(" {n}"); + } + } + println!(); + println!(" No guard is read. `x.len() == 4` does not narrow anything here --"); + println!(" that is the part that needs a semantics, and this report must not be"); + println!(" the thing that quietly decides one. See #2774."); + Ok(()) +} + +#[cfg(test)] +mod tests { + use super::*; + + fn s() -> Structs { + Structs { + fields: [( + "Pair".to_string(), + vec!["bool".to_string(), "Trit".to_string()], + )] + .into_iter() + .collect(), + conflicted: Default::default(), + } + } + + #[test] + fn a_trit_is_three_and_a_struct_is_the_product() { + assert_eq!(size_of("Trit", &s(), 0), Size::Finite(3)); + assert_eq!(size_of("Pair", &s(), 0), Size::Finite(6)); + } + + /// The rule that matters: an unresolved name is NOT assumed small. + #[test] + fn an_unknown_type_is_unbounded_not_one() { + assert_eq!(size_of("ModelConfig", &s(), 0), Size::Unbounded); + assert_eq!(size_of("string", &s(), 0), Size::Unbounded); + assert_eq!(size_of("[]u8", &s(), 0), Size::Unbounded); + } + + #[test] + fn a_pinned_array_length_is_a_power_and_an_unpinned_one_is_not() { + assert_eq!(size_of("[3]Trit", &s(), 0), Size::Finite(27)); + assert_eq!(size_of("[]Trit", &s(), 0), Size::Unbounded); + } + + /// A conflicted struct name is unbounded even though its fields resolve. + #[test] + fn a_struct_defined_twice_is_unbounded() { + let mut st = s(); + st.conflicted.insert("Pair".to_string()); + assert_eq!(size_of("Pair", &st, 0), Size::Unbounded); + } + + #[test] + fn the_four_notations_are_recognised() { + let src = "\ + invariant a: forall c : Cfg, c.x > 0 + forall input : In + assert f(a) == f(b) for all Trit + assert g(a) == g(b) for any a : Trit, b : Trit +"; + let cs = scan_clauses(&[(PathBuf::from("x.t27"), src.to_string())]); + let mut kinds: Vec<&str> = cs.iter().map(|c| c.notation).collect(); + kinds.sort(); + assert_eq!(kinds, vec!["colon", "prefix", "suffix-all", "suffix-any"]); + } + + /// A suffix with no `name : Type` yields no binder rather than a wrong one. + #[test] + fn a_prose_suffix_has_no_binder() { + let cs = scan_clauses(&[( + PathBuf::from("x.t27"), + " assert p(x) for all positive integer n\n".to_string(), + )]); + assert_eq!(cs.len(), 1); + assert!(cs[0].binders.is_empty(), "{:?}", cs[0].binders); + } +} diff --git a/docs/now/2026-08-29-the-quantifier-census-100-walkable-domains-out-of-1005.md b/docs/now/2026-08-29-the-quantifier-census-100-walkable-domains-out-of-1005.md new file mode 100644 index 0000000000..aa4b9ce7c5 --- /dev/null +++ b/docs/now/2026-08-29-the-quantifier-census-100-walkable-domains-out-of-1005.md @@ -0,0 +1,8 @@ +# NOW -- The quantifier census: 100 walkable domains out of 1005 (2026-08-29) + +## The quantifier census: 100 walkable domains out of 1005 (Refs #2774) + +- three independently written proposals for #2774 disagreed on the lowering and agreed exactly on the first step: report before you lower +- 1005 quantified clauses in four notations; at a 65536 ceiling 100 are walkable, 222 finite but over it, 544 unbounded, 139 have no binder a reader can resolve +- all 135 suffix forms (for all Trit, for any a b in {1,-1}) are prose with no binder -- the small domains are exactly the ones written without one +- no guard is read: x.len() == 4 narrows nothing here, because that is the part that needs a semantics and the report must not decide one quietly From 94bc1de813be70bb1624aa70110ebef61a553234 Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Sat, 29 Aug 2026 16:45:39 +0700 Subject: [PATCH 2/2] docs(skill): the shared prefix, the broken specimen, the unknown domain (186-188) Three incompatible designs agreed on one first step, which is the step that cannot be wrong. I validated a spec fix against a line that was itself failing. And the default for an unresolvable type must be the answer that makes the tool refuse. Refs #2754, #2774 Co-Authored-By: Claude Opus 5 --- .claude/skills/ci-gates/SKILL.md | 45 ++++++++++++++++++++++++++++++++ 1 file changed, 45 insertions(+) diff --git a/.claude/skills/ci-gates/SKILL.md b/.claude/skills/ci-gates/SKILL.md index 2fcc66a913..d4cf50b1a1 100644 --- a/.claude/skills/ci-gates/SKILL.md +++ b/.claude/skills/ci-gates/SKILL.md @@ -6110,3 +6110,48 @@ to 23 644 with both regressions gone. **Re-measure after the fix for a regression, not just after the regression.** A plausible cause that makes the number worse is a cause you have disproved, and that is worth more than the twenty minutes it saves. + +## 186. Three designs that disagree can still agree on the first step + +Three independently written proposals for one language decision — capture and +never lower, enumerate finite domains, split the four backends apart — went +through two adversarial lenses each. **All three survived with zero fatal +verdicts**, which looked like a useless result: no winner. + +It was not. They disagreed about the lowering and agreed exactly about the first +increment: *report before you lower*, because the ceiling cannot be chosen +without the distribution, and nobody had measured it. + +**When a panel fails to pick a winner, look for the prefix they share.** A step +three mutually incompatible designs all need is a step that cannot be wrong. + +## 187. I validated a fix against a line that was itself broken + +Rewriting `assert G_MEASURED = 6.67e-11 +/- 1.5e-15` needed an absolute value. +The corpus already contained `assert |x - y| < 0.1`, so I used that shape. + +It moved two tokens. `|...|` does not parse — and the line I copied it from is +itself one of the discarding lines. I had validated a repair against a specimen +of the disease. + +`abs(...)` is the real idiom, used four times in clauses that lower cleanly, and +with it the three edits moved twenty tokens and each spec lost a fallback event. + +**Before copying an idiom out of the corpus, check that the line you are copying +from works.** In a corpus with a measured failure rate, a randomly chosen example +is a coin flip. + +## 188. An unresolved name is not a small domain + +The census computes `|D|` from declared types. The tempting default for a type +it cannot resolve is 1, or to skip it — both of which make a clause look +enumerable when nothing is known about it. + +`BOTTOM` is absorbing, an unresolved name is unbounded, and a struct name defined +**twice** is unbounded even though both definitions resolve: `|D|` is +undetermined not because the type is infinite but because *which type* is +undetermined. Fifteen names in this corpus are in that state. + +**The default for "I do not know" must be the answer that makes the tool refuse, +never the one that makes it proceed.** Four of the six tests on that command +exist to pin exactly that.