From 7fc9961f815ac89639b7f209cc2f332058a0f120 Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Sat, 29 Aug 2026 17:53:24 +0700 Subject: [PATCH] feat(tri): pin the conflicted type names by identity, not by count `tri types dup` found 79 type names with more than one definition and reported them. Nothing held the line. tri types ratchet --bless # writes docs/reports/type_conflicts.json tri types ratchet # a NEW conflict fails; a RESOLVED one fails too IDENTITY, NOT A COUNT, and the difference is the whole point. A count cannot see a SWAP: one name resolved while another appears leaves the total at 79 and the ledger wrong. Seen failing on purpose, three ways: - Lexer removed from the ledger -> "+ Lexer NEW conflict", exit 1 - a name added to the ledger -> "- ZZZGone resolved", exit 1 - one swapped for another at 79 -> BOTH lines, exit 1 The third is the one a count misses. A RESOLVED name fails too, on purpose -- the same rule this repository already applies to an unexpected PASS in the corpus ratchet. An entry that has stopped being true and stays in the ledger is slack the next conflict hides in. And absence is not amnesty (T31): with no ledger the command exits 1 and says to bless once and commit the file, rather than passing quietly over an empty oracle. Eleven tests. The three new ones cover the swap at a constant count, a resolved name, and agreement being silence; `drift` is a pure function so they test the production comparison rather than a re-implementation of it. WHY THESE NAMES MATTER. A quantifier's domain size is computed from declared types. For a conflicted name the answer is "unbounded" -- not because the type is infinite but because WHICH type is undetermined. Any enumerating lowering of `forall` hits the same wall, so this set has to stop growing before that decision is worth making. See #2774. Refs #2774 Co-Authored-By: Claude Opus 5 --- cli/tri/src/types_dup.rs | 150 +++++++++++++++++- ...ames-are-pinned-by-identity-not-by-coun.md | 8 + docs/reports/type_conflicts.json | 85 ++++++++++ 3 files changed, 241 insertions(+), 2 deletions(-) create mode 100644 docs/now/2026-08-29-the-conflicted-type-names-are-pinned-by-identity-not-by-coun.md create mode 100644 docs/reports/type_conflicts.json diff --git a/cli/tri/src/types_dup.rs b/cli/tri/src/types_dup.rs index f840530886..a8847d267b 100644 --- a/cli/tri/src/types_dup.rs +++ b/cli/tri/src/types_dup.rs @@ -34,6 +34,103 @@ pub enum TypesCmd { #[arg(long)] all: bool, }, + /// Hold the conflicted set: a new conflict fails, and a resolved one fails + /// until it is blessed away. + /// + /// Identity-keyed, not a count. A count cannot see a SWAP -- one name + /// resolved while another appears leaves the total unchanged and the ledger + /// wrong, which is the failure mode the corpus ratchet in this repository + /// was rebuilt to avoid. + Ratchet { + /// Rewrite the ledger from what this run measured. + #[arg(long)] + bless: bool, + }, +} + +/// Where the conflicted set is pinned. +const LEDGER: &str = "docs/reports/type_conflicts.json"; + +#[derive(serde::Serialize, serde::Deserialize, Default)] +struct Ledger { + /// What wrote it, so a reader knows which command to re-run. + generated_by: String, + /// Why these are tolerated at all. + reason: String, + /// Sorted, so a diff stays line-local. + conflicted: Vec, +} + +/// `(new, resolved)` between a pinned set and an observed one. +/// +/// Set difference in both directions, deliberately. A COUNT cannot see a swap: +/// one name resolved while another appears leaves the total unchanged and the +/// ledger wrong. +pub fn drift(pinned: &[String], observed: &[String]) -> (Vec, Vec) { + let p: std::collections::BTreeSet<&String> = pinned.iter().collect(); + let o: std::collections::BTreeSet<&String> = observed.iter().collect(); + ( + o.difference(&p).map(|s| (*s).clone()).collect(), + p.difference(&o).map(|s| (*s).clone()).collect(), + ) +} + +fn ratchet(root: &std::path::Path, observed: &[String], bless: bool) -> Result<()> { + let path = root.join(LEDGER); + if bless { + let l = Ledger { + generated_by: "tri types ratchet --bless".to_string(), + reason: "Type names with more than one definition. Each is a name whose \ + domain size cannot be computed -- not because the type is infinite \ + but because WHICH type is undetermined. See #2774." + .to_string(), + conflicted: observed.to_vec(), + }; + let mut text = serde_json::to_string_pretty(&l)?; + text.push('\n'); + std::fs::create_dir_all(path.parent().unwrap()).ok(); + std::fs::write(&path, text).with_context(|| format!("writing {}", path.display()))?; + println!( + " blessed {} conflicted name(s) -> {}", + observed.len(), + LEDGER + ); + return Ok(()); + } + + // T31 in this repository: absence is NOT amnesty. A verification mode with + // no oracle is a hard failure, never a silent self-blessing. + let Ok(text) = std::fs::read_to_string(&path) else { + println!(" RATCHET: FAIL -- no ledger at {LEDGER}."); + println!(" Run `tri types ratchet --bless` once, review the file, and commit it."); + println!(" Absence is not amnesty."); + std::process::exit(1); + }; + let l: Ledger = + serde_json::from_str(&text).with_context(|| format!("parsing {}", path.display()))?; + + let (new, gone) = drift(&l.conflicted, observed); + + println!( + " ledger {} name(s), observed {}", + l.conflicted.len(), + observed.len() + ); + for n in &new { + println!(" + {n} NEW conflict"); + } + for n in &gone { + println!(" - {n} resolved -- remove it from the ledger"); + } + if new.is_empty() && gone.is_empty() { + println!(" RATCHET: CLEAN"); + return Ok(()); + } + println!(); + println!(" A RESOLVED name fails too, on purpose. An entry that stops being"); + println!(" true and stays in the ledger is slack the next conflict hides in --"); + println!(" the same rule the corpus ratchet applies to an unexpected PASS."); + std::process::exit(1); } /// `const Name = struct {` -- the Zig spelling, and the one the corpus uses @@ -246,8 +343,31 @@ pub fn verdict(defs: &[Def]) -> &'static str { } pub fn run(cmd: &TypesCmd) -> Result<()> { - let TypesCmd::Dup { all } = cmd; let root = repo_root()?; + let all = match cmd { + TypesCmd::Dup { all } => *all, + TypesCmd::Ratchet { bless } => { + let specs = read_specs(&root); + if specs.is_empty() { + anyhow::bail!( + "no specs under {}/specs -- nothing was read", + root.display() + ); + } + let mut by_name: BTreeMap> = BTreeMap::new(); + for (f, src) in &specs { + for (n, d) in defs_in(f, src) { + by_name.entry(n).or_default().push(d); + } + } + let observed: Vec = by_name + .iter() + .filter(|(_, v)| v.len() > 1 && verdict(v) == "CONFLICTED") + .map(|(k, _)| k.clone()) + .collect(); + return ratchet(&root, &observed, *bless); + } + }; let specs = read_specs(&root); if specs.is_empty() { anyhow::bail!( @@ -272,7 +392,7 @@ pub fn run(cmd: &TypesCmd) -> Result<()> { for (name, defs) in &multi { let v = verdict(defs); - if v == "DUPLICATED" && !*all { + if v == "DUPLICATED" && !all { continue; } println!(" {name} {v} ({} definitions)", defs.len()); @@ -394,6 +514,32 @@ mod tests { assert_eq!(names, vec!["A", "B", "C"], "{names:?}"); } + /// The case a count cannot see: one resolved, one appeared, total unchanged. + #[test] + fn a_swap_at_a_constant_count_is_two_findings() { + let pinned = vec!["A".to_string(), "B".to_string()]; + let observed = vec!["A".to_string(), "C".to_string()]; + let (new, gone) = drift(&pinned, &observed); + assert_eq!(new, vec!["C".to_string()]); + assert_eq!(gone, vec!["B".to_string()]); + assert_eq!(pinned.len(), observed.len(), "the count is identical"); + } + + /// A resolved conflict is a failure, not a quiet win: slack in the ledger + /// is where the next one hides. + #[test] + fn a_resolved_name_is_reported() { + let (new, gone) = drift(&["A".to_string(), "B".to_string()], &["A".to_string()]); + assert!(new.is_empty()); + assert_eq!(gone, vec!["B".to_string()]); + } + + #[test] + fn agreement_is_silence() { + let (new, gone) = drift(&["A".to_string()], &["A".to_string()]); + assert!(new.is_empty() && gone.is_empty()); + } + #[test] fn a_struct_with_no_parseable_fields_is_still_a_definition() { let d = parse("struct Empty {\n}\n"); diff --git a/docs/now/2026-08-29-the-conflicted-type-names-are-pinned-by-identity-not-by-coun.md b/docs/now/2026-08-29-the-conflicted-type-names-are-pinned-by-identity-not-by-coun.md new file mode 100644 index 0000000000..5cdc69c345 --- /dev/null +++ b/docs/now/2026-08-29-the-conflicted-type-names-are-pinned-by-identity-not-by-coun.md @@ -0,0 +1,8 @@ +# NOW -- The conflicted type names are pinned by identity, not by count (2026-08-29) + +## The conflicted type names are pinned by identity, not by count (Refs #2774) + +- tri types ratchet: 79 names with more than one definition, pinned as a SET -- a new conflict fails and a resolved one fails until it is blessed away +- identity and not a count because a count cannot see a swap: one resolved while another appears leaves the total unchanged and the ledger wrong +- seen failing three ways on purpose, including the swap at a constant 79 +- absence is not amnesty: with no ledger the command exits 1 rather than passing quietly diff --git a/docs/reports/type_conflicts.json b/docs/reports/type_conflicts.json new file mode 100644 index 0000000000..ea9256d4e3 --- /dev/null +++ b/docs/reports/type_conflicts.json @@ -0,0 +1,85 @@ +{ + "generated_by": "tri types ratchet --bless", + "reason": "Type names with more than one definition. Each is a name whose domain size cannot be computed -- not because the type is infinite but because WHICH type is undetermined. See #2774.", + "conflicted": [ + "ActivationType", + "AdamWConfig", + "Agent", + "AgentState", + "AgentStatus", + "AttentionConfig", + "AttentionOutput", + "BenchmarkReport", + "BenchmarkResult", + "BusPort", + "Color", + "CompileResult", + "Config", + "DataSample", + "Diagnostic", + "EnvVar", + "EvalResult", + "FFNConfig", + "FileInfo", + "Graph", + "HttpRequest", + "HttpResponse", + "HttpStatus", + "HybridBigInt", + "Hypervector", + "Info", + "Instance", + "JitCache", + "JitCompiler", + "KnowledgeGraph", + "LSTMWeights", + "Lexer", + "LinkResult", + "LogEntry", + "MHAConfig", + "Match", + "MemPort", + "Message", + "MigrationStep", + "Node", + "OptimizerStepResult", + "ParseError", + "ParseResult", + "Parser", + "PinAssignment", + "PinMapping", + "PipelineConfig", + "PipelineResult", + "PolicyOutput", + "Port", + "ProcessInfo", + "Promise", + "ProofStep", + "ProviderConfig", + "QueryResult", + "Rect", + "Response", + "Result", + "Route", + "Rule", + "SacredConstants", + "SacredRule", + "SearchResult", + "Session", + "Signal", + "SimResult", + "SystemConfig", + "Task", + "TaskResult", + "TernaryWeight", + "TernaryWord", + "ToolCall", + "ToolResult", + "TrainingConfig", + "UnpackResult", + "Url", + "Usage", + "ValidationResult", + "VerificationReport" + ] +}