From a8bc733e0addf9543e2779fa9c102eeaef74d432 Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Sun, 30 Aug 2026 23:22:20 +0700 Subject: [PATCH 1/2] feat(tri): the tenth ledger -- the one refusal that work could lift Of the six ledgers the audit excused last pass, five are excused by cost or by shape: two are gated by the corpus suite and take minutes, one is keyed by the sha1 of the line it excuses, one is a generated observation that the next regeneration would erase. Exactly one was excused by MISSING WORK. `docs/reports/type_conflicts_classified.json` was measured as catching a planted row, and left out because the plant had to clone an entry's field shape and `Plant` could express only an appended line and one ghost key. It can now. `ClassifiedName` deserialises `name` and `verdict` and nothing else, so a two-field object is complete for the reader and false for the claim -- no type name in this corpus is called `PlantedByLedgersAudit`. The row is inserted into `names` textually rather than by re-serialising, so the document's formatting survives the restore. caught docs/reports/type_conflicts_classified.json by tri types classified ledger-shaped files on disk 15 planted into 10, excused 5, unclassified 0 VERIFIED FOR THE RIGHT REASON, which is the whole risk with a JSON plant. The planted file parses, and the gate fails on the claim: STALE PlantedByLedgersAudit: classified, but no longer conflicting -- drop the row Error: 1 stale row(s) and 0 unjudged conflict(s). A shape error wearing a catch would have left this ledger reported as protected while its staleness check was never exercised. Mutation-checked: make the plant emit invalid JSON and `substitution_keeps_what_makes_it_false` fails on "planted ledger must parse". The same test asserts the planted row is one MORE row rather than a replacement, because an insertion that overwrites would test a different file. And the coverage test earned itself. Adding the ledger while leaving its exclusion in place put one path in both lists, and `no_ledger_is_both_planted_into_and_excused` failed before I noticed -- the check written two passes ago catching the change that landed today. cargo test -p tri 392 passed, 0 failed cargo clippy 120 warnings, same as master tri ledgers audit 10 caught, 0 missed, exit 0; the ledger restored unchanged Refs #2864 --- cli/tri/src/ledgers.rs | 50 +++++++++++++++---- ...er-the-one-refusal-that-work-could-lift.md | 9 ++++ 2 files changed, 50 insertions(+), 9 deletions(-) create mode 100644 docs/now/2026-08-30-the-tenth-ledger-the-one-refusal-that-work-could-lift.md diff --git a/cli/tri/src/ledgers.rs b/cli/tri/src/ledgers.rs index 15fd2dbf0..e4f902f05 100644 --- a/cli/tri/src/ledgers.rs +++ b/cli/tri/src/ledgers.rs @@ -64,6 +64,14 @@ enum Plant { /// a hardcoded name rots into a line that is TRUE, and the audit then /// quietly stops testing anything. Line(&'static str), + /// Add a classification row for a type name that is not conflicted. + /// + /// `ClassifiedName` deserialises only `name` and `verdict`, so a two-field + /// object is complete for the reader and false for the claim: nothing in + /// the corpus carries this name, so the row is STALE by construction. The + /// entry is inserted into `"names"` textually rather than by + /// re-serialising, so the document's formatting survives the restore. + StaleRow, /// Add a ceiling for a crate the workspace does not declare. /// /// Appending a line to a JSON ledger would make the gate fail because the @@ -123,6 +131,11 @@ const LEDGERS: &[Ledger] = &[ // A conformance file that does not exist. plant: Plant::Line("fpga_planted_by_ledgers_audit.json | 1 | 1"), }, + Ledger { + path: "docs/reports/type_conflicts_classified.json", + gate: Gate::Tri(&["types", "classified"]), + plant: Plant::StaleRow, + }, ]; /// Every file in this repository shaped like a ledger, found by walking rather @@ -164,7 +177,7 @@ struct Unaudited { why: &'static str, } -const UNAUDITED: [Unaudited; 6] = [ +const UNAUDITED: [Unaudited; 5] = [ Unaudited { path: "docs/reports/suite_expectations.json", why: "its gate is the corpus ratchet, which compiles every spec in the corpus. \ @@ -184,14 +197,6 @@ const UNAUDITED: [Unaudited; 6] = [ until the next regeneration erases it, so demanding a gate fail on one \ measures the regeneration, not the claim.", }, - Unaudited { - path: "docs/reports/type_conflicts_classified.json", - why: "measured, and it CATCHES: a cloned row renamed PlantedByAudit gives \ - `tri types classified` exit 1, `STALE PlantedByAudit: classified, but no \ - longer conflicting`. Not planted into yet because the plant must clone an \ - existing row's field shape, which Plant cannot express -- and an ill-shaped \ - plant would fail the gate on its SHAPE, a catch for the wrong reason.", - }, Unaudited { path: "docs/reports/lean_completeness_mismatches.json", why: "measured: a planted entry leaves `tri lean vacuous` at exit 0 both ways -- \ @@ -286,6 +291,19 @@ fn plant_text(before: &str, plant: &Plant, spec: &str, json: &str) -> Option { + // One row at the head of `names`. The gate reads `name` and + // `verdict` and nothing else, so this object is complete -- and the + // file must still PARSE, or the gate would fail on the shape + // instead of on the claim, which is a catch for the wrong reason. + let at = before.find("\"names\"")?; + let bracket = before[at..].find('[')? + at + 1; + Some(format!( + "{}\n {{ \"name\": \"PlantedByLedgersAudit\", \"verdict\": \"DRIFT\" }},{}", + &before[..bracket], + &before[bracket..] + )) + } Plant::GhostCeiling => { // Textual, so the file's formatting survives: insert one key into // the `ceilings` object rather than re-serialising the document. @@ -615,6 +633,20 @@ mod tests { // The planted text must still PARSE -- appending junk makes the // gate fail because the file is unreadable, which is a catch // for the wrong reason. + Plant::StaleRow => { + let before = "{\n \"names\": [\n { \"name\": \"A\", \"verdict\": \"DRIFT\" }\n ]\n}\n"; + let planted = + plant_text(before, &l.plant, "unused", "unused").expect("planted"); + assert!(planted.contains("PlantedByLedgersAudit"), "{}", l.path); + let v: serde_json::Value = serde_json::from_str(&planted) + .unwrap_or_else(|e| panic!("{}: planted ledger must parse -- {e}", l.path)); + assert_eq!( + v["names"].as_array().map(|a| a.len()), + Some(2), + "{}: the planted row is one more row, not a replacement", + l.path + ); + } Plant::GhostCeiling => { let before = "{\n \"ceilings\": {\n \"a\": 1\n }\n}\n"; let planted = diff --git a/docs/now/2026-08-30-the-tenth-ledger-the-one-refusal-that-work-could-lift.md b/docs/now/2026-08-30-the-tenth-ledger-the-one-refusal-that-work-could-lift.md new file mode 100644 index 000000000..b36708572 --- /dev/null +++ b/docs/now/2026-08-30-the-tenth-ledger-the-one-refusal-that-work-could-lift.md @@ -0,0 +1,9 @@ +# NOW -- The tenth ledger: the one refusal that work could lift (2026-08-30) + +## The tenth ledger: the one refusal that work could lift (Refs #2864) + +- Of the six ledgers the audit excused, five are excused by cost or by shape -- a corpus-suite gate too slow to plant into, a sha1-keyed baseline, a generated observation. Exactly one was excused by MISSING WORK: type_conflicts_classified.json catches a planted row, and the plant needed a shape the Plant enum could not express. +- It can now. `ClassifiedName` deserialises only `name` and `verdict`, so a two-field object is complete for the reader and false for the claim: no such type name is conflicted. Inserted into `names` textually so the document's formatting survives the restore. +- Verified for the RIGHT reason, which is the whole risk with a JSON plant: the planted file PARSES, and `tri types classified` exits 1 with `STALE PlantedByLedgersAudit: classified, but no longer conflicting -- drop the row`. Not a shape error wearing a catch. +- Mutation: make the plant emit invalid JSON and `substitution_keeps_what_makes_it_false` fails on 'planted ledger must parse'. The test also asserts the row is one MORE row, not a replacement. +- And the coverage test earned itself: adding the ledger while leaving its exclusion in place put one name in both lists, and `no_ledger_is_both_planted_into_and_excused` failed before I noticed. 15 files: 10 planted into, 5 excused, 0 unclassified. From 5ddc7f8ba982f2efdc9cfb026721edbbedecd337 Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Sun, 30 Aug 2026 23:23:04 +0700 Subject: [PATCH 2/2] skill(ci-gates): sort an exclusion list by what would lift it (Refs #2864) --- .claude/skills/ci-gates/SKILL.md | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/.claude/skills/ci-gates/SKILL.md b/.claude/skills/ci-gates/SKILL.md index 88d60896e..8b4632505 100644 --- a/.claude/skills/ci-gates/SKILL.md +++ b/.claude/skills/ci-gates/SKILL.md @@ -10006,3 +10006,25 @@ resolve the root explicitly and run there. **A path in a command is relative to where the command runs, not to where you wrote it.** In a test that is the crate; in a hook that is the worktree; in CI it is whatever the last `working-directory` said. + + +## 399. Sort an exclusion list by what would lift it + +The ledger audit excused six files, and reading them as one list is what hid the +finding. Sorted by what would lift the exclusion: + +* **Five need a DECISION or cost you do not control** -- a gate that takes + minutes, a baseline keyed by the sha1 of the line it excuses, a generated + observation the next regeneration would erase. Nothing you write closes those. +* **One needed WORK.** `type_conflicts_classified.json` was measured as catching + a planted row and left out because the plant had to clone a field shape the + code could not express. Two hours later it could. + +**An exclusion list is a work list with the work hidden inside the reasons.** +Every entry answers "why not", and the useful question is the next one: *would +writing something lift this, or is it a decision?* Only the first kind is yours, +and it will be a minority -- which is exactly why it disappears into the list. + +The same reading applies to any "known limitations" section, any `#[ignore]` +block, any `NOT covered here` comment. Grep them, ask of each which kind it is, +and the answer usually names one item you can close today.