Skip to content
57 changes: 57 additions & 0 deletions .claude/skills/ci-gates/SKILL.md
Original file line number Diff line number Diff line change
Expand Up @@ -9949,3 +9949,60 @@ list that never covered the directory at all, and said so in numbers nobody
subtracted. The controls that hold it are three, each seen failing on purpose —
a 28th unclassified file, a name in both lists, and the restored filter on
`corpus-ratchet.yml`, which is also the historical control for the two findings.

## 396. A ledger that is entirely stale is stronger emptied than held

Teaching `check_json_parses.py` to notice a stale entry turned it red on a clean
tree: **six** entries naming files in neither git nor the working tree. The scan
finds **zero** unparseable and **zero** empty tracked JSON today. The whole
ledger was debt about things that had already left.

The reflex is to keep the file and fix the check. The measurement says otherwise:
an empty ledger holds the line at **zero**, so any unparseable JSON now fails
with no slack to hide in. A ledger of six ghosts held nothing and read as debt
being managed.

**When a stale-entry check turns a ledger red on arrival, count what the ledger
would hold if it were empty.** If the true debt is zero, the ledger is not a
record -- it is six lines of noise standing between the gate and its job. Write
the measurement into the file where the entries were, so the next reader knows
the emptiness was earned rather than skipped.

## 397. Two ways to be false by construction, and the second needs its own test

A planted entry has to be FALSE the moment it lands. There are two mechanisms
and they fail differently:

* **Resolved at run time** -- `{spec}` becomes a spec that passes today,
`{json}` a tracked file that parses today. Cannot rot: the lookup re-runs.
* **A name that cannot exist** -- `planted_by_ledgers_audit`. Cheap, and it rots
the day something in the tree is actually called that. Then the planted line
is TRUE, the gate is right to stay green, and the audit reports `caught` for a
ledger it has stopped testing.

The second mechanism is only sound while nobody uses the name, which is a claim
about the whole repository -- so it needs a check, not a convention:

```rust
git grep -l SYNTHETIC -- ':!cli/tri/src/ledgers.rs' // must be empty
```

**Any hardcoded sentinel carries an unstated claim that it is unique.** Assert
it, or use a runtime lookup instead.

## 398. A pathspec resolves against the current directory

The test above failed on its own source: it ran `git grep` from the crate
directory while excluding `cli/tri/src/ledgers.rs`, the path as seen from the
repository ROOT. Git was matching `src/ledgers.rs`, the exclusion hit nothing.

Same family as every `cd`-shaped ruler in this document, and the fix is the same:
resolve the root explicitly and run there.

```rust
.current_dir(&root) // root from `git rev-parse --show-toplevel`
```

**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.
182 changes: 168 additions & 14 deletions cli/tri/src/ledgers.rs
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,10 @@ enum Gate {

/// How to make one entry FALSE without making the file unreadable.
enum Plant {
/// Append a line. `{spec}` becomes a spec that passes today.
/// Append a line. `{spec}` becomes a spec that passes today; `{json}` a
/// tracked JSON file that parses today. Both are looked up at RUN TIME --
/// a hardcoded name rots into a line that is TRUE, and the audit then
/// quietly stops testing anything.
Line(&'static str),
/// Add a ceiling for a crate the workspace does not declare.
///
Expand Down Expand Up @@ -96,6 +99,30 @@ const LEDGERS: &[Ledger] = &[
gate: Gate::Tri(&["mods", "orphan", "--gate"]),
plant: Plant::GhostCeiling,
},
Ledger {
path: "tools/devhome_baseline.txt",
gate: Gate::Script("tools/check_devhome_paths.py"),
// A spec carries no developer home path, so claiming three is false.
plant: Plant::Line("{spec}\t3"),
},
Ledger {
path: "tools/elab_baseline.txt",
gate: Gate::Script("tools/check_elab_ratchet.py"),
// A module name nothing generates.
plant: Plant::Line("planted_by_ledgers_audit 0"),
},
Ledger {
path: "tools/json_parse_baseline.txt",
gate: Gate::Script("tools/check_json_parses.py"),
// A JSON file that parses, listed as one that does not.
plant: Plant::Line("{json} | planted by `tri ledgers audit`"),
},
Ledger {
path: "tools/vector_data_baseline.txt",
gate: Gate::Script("tools/check_vector_data.py"),
// A conformance file that does not exist.
plant: Plant::Line("fpga_planted_by_ledgers_audit.json | 1 | 1"),
},
];

/// Every file in this repository shaped like a ledger, found by walking rather
Expand Down Expand Up @@ -137,7 +164,7 @@ struct Unaudited {
why: &'static str,
}

const UNAUDITED: [Unaudited; 2] = [
const UNAUDITED: [Unaudited; 6] = [
Unaudited {
path: "docs/reports/suite_expectations.json",
why: "its gate is the corpus ratchet, which compiles every spec in the corpus. \
Expand All @@ -150,8 +177,55 @@ const UNAUDITED: [Unaudited; 2] = [
would need a hash that matches text elsewhere in the tree. A planted entry \
that cannot be false by construction proves nothing.",
},
Unaudited {
path: "docs/reports/type_conflicts.json",
why: "it carries `generated_by` and is regenerated by `tri types dup`: an \
observation, not a ledger of hand-written claims. A planted line survives \
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 -- \
it reports and does not gate. Which command enforces its `max_entries` cap \
is not established here, so there is no gate yet to demand a failure from.",
},
Unaudited {
path: "docs/reports/gen_verilog_smoke_baseline.json",
why: "read by bootstrap/src/suite.rs, the corpus suite -- the same cost objection \
as suite_expectations.json, and the same answer: a meta-gate that takes \
minutes is one nobody runs before committing.",
},
];

/// A tracked JSON file that PARSES today, so a line calling it unparseable is
/// false on its face. Looked up at run time for the same reason the spec is.
fn a_parsing_json(root: &Path) -> Option<String> {
let out = std::process::Command::new("git")
.args(["ls-files", "*.json"])
.current_dir(root)
.output()
.ok()?;
String::from_utf8_lossy(&out.stdout)
.lines()
.filter(|p| !p.starts_with("external/"))
.find(|p| {
std::fs::read_to_string(root.join(p))
.ok()
.and_then(|t| serde_json::from_str::<serde_json::Value>(&t).ok())
.is_some()
})
.map(|s| s.to_string())
}

/// A spec that passes today, so a ledger line naming it is false on its face.
fn a_passing_spec(root: &Path, t27c: &Path) -> Option<String> {
let out = std::process::Command::new("git")
Expand Down Expand Up @@ -206,9 +280,12 @@ fn gate_present(root: &Path, gate: &Gate) -> bool {
}

/// The planted text: false by construction, and still readable by the gate.
fn plant_text(before: &str, plant: &Plant, spec: &str) -> Option<String> {
fn plant_text(before: &str, plant: &Plant, spec: &str, json: &str) -> Option<String> {
match plant {
Plant::Line(t) => Some(format!("{before}{}\n", t.replace("{spec}", spec))),
Plant::Line(t) => Some(format!(
"{before}{}\n",
t.replace("{spec}", spec).replace("{json}", json)
)),
Plant::GhostCeiling => {
// Textual, so the file's formatting survives: insert one key into
// the `ceilings` object rather than re-serialising the document.
Expand Down Expand Up @@ -255,7 +332,11 @@ pub fn run(cmd: &LedgersCmd, root: PathBuf) -> Result<()> {
let Some(spec) = a_passing_spec(&root, &t27c) else {
anyhow::bail!("no spec passes today -- nothing to plant a false line about");
};
let Some(json) = a_parsing_json(&root) else {
anyhow::bail!("no tracked JSON parses today -- nothing to plant a false line about");
};
println!(" planting a line about {spec}");
println!(" and about {json}");
println!(" it passes, so every planted line is FALSE by construction");
println!();

Expand Down Expand Up @@ -284,7 +365,7 @@ pub fn run(cmd: &LedgersCmd, root: PathBuf) -> Result<()> {
skipped += 1;
continue;
};
let Some(planted) = plant_text(&before, &l.plant, &spec) else {
let Some(planted) = plant_text(&before, &l.plant, &spec, &json) else {
println!(" SKIP {} (nothing to plant into)", l.path);
skipped += 1;
continue;
Expand Down Expand Up @@ -426,16 +507,79 @@ mod tests {
}
}

// The planted line must name the spec, or the audit tests nothing.
/// A planted line has to be FALSE by construction, and there are two ways.
///
/// Either it names something resolved at RUN TIME -- `{spec}` a spec that
/// passes today, `{json}` a JSON file that parses today -- or it names
/// something that cannot exist. A hardcoded name that happens to name a
/// real thing would rot into a line that is TRUE, and the audit would
/// quietly stop testing that ledger.
const SYNTHETIC: &str = "planted_by_ledgers_audit";

#[test]
fn every_template_carries_the_spec_placeholder() {
fn every_template_is_false_by_construction() {
for l in LEDGERS {
if let Plant::Line(t) = &l.plant {
assert!(t.contains("{spec}"), "template names no spec: {}", l.path);
assert!(
t.contains("{spec}") || t.contains("{json}") || t.contains(SYNTHETIC),
"{}: the planted line names nothing that makes it false -- {t:?}",
l.path
);
}
}
}

/// The synthetic name must name nothing in this repository.
///
/// That is the half a hardcoded string cannot promise on its own: if a
/// module or a conformance file were ever called this, the planted line
/// would be TRUE and the gate would be right to stay green.
#[test]
fn the_synthetic_name_occurs_nowhere() {
// From the repository ROOT: `git grep` resolves a pathspec against the
// current directory, and this test runs in the crate. The first version
// excluded `cli/tri/src/ledgers.rs` while git was seeing `src/ledgers.rs`,
// so the exclusion matched nothing and the test failed on its own source.
let Some(root) = std::process::Command::new("git")
.args(["rev-parse", "--show-toplevel"])
.output()
.ok()
.filter(|o| o.status.success())
.map(|o| PathBuf::from(String::from_utf8_lossy(&o.stdout).trim().to_string()))
else {
return;
};
let Ok(out) = std::process::Command::new("git")
// Prose is excluded, and the exclusion is the claim being made
// narrow rather than weak: the sentinel must not name a MODULE or a
// DATA FILE that a gate reads, and a Markdown paragraph can become
// neither. This test first failed in CI on the skill section that
// documents it -- the guard firing on its own documentation, which
// is evidence it works and a reminder that the tests have to be
// re-run after the commit that writes the prose.
.args([
"grep",
"-l",
SYNTHETIC,
"--",
":!cli/tri/src/ledgers.rs",
":!*.md",
":!docs/now/*",
])
.current_dir(&root)
.output()
else {
return;
};
let hits = String::from_utf8_lossy(&out.stdout);
let hits: Vec<&str> = hits.lines().filter(|l| !l.is_empty()).collect();
assert!(
hits.is_empty(),
"the synthetic name is used in the tree, so a planted line about it \
could be true: {hits:?}"
);
}

#[test]
fn every_ledger_has_a_distinct_gate() {
let mut seen = std::collections::BTreeSet::new();
Expand All @@ -448,23 +592,33 @@ mod tests {
}
}

// Substitution must produce a line that mentions the spec path verbatim --
// Substitution must produce a line that carries what makes it false --
// a template that silently drops it would plant a line no gate can match.
#[test]
fn substitution_keeps_the_path() {
fn substitution_keeps_what_makes_it_false() {
for l in LEDGERS {
match &l.plant {
Plant::Line(_) => {
let planted = plant_text("", &l.plant, "specs/x/y.t27").expect("planted");
assert!(planted.contains("specs/x/y.t27"), "{}", l.path);
Plant::Line(t) => {
let planted =
plant_text("", &l.plant, "specs/x/y.t27", "a/b.json").expect("planted");
if t.contains("{spec}") {
assert!(planted.contains("specs/x/y.t27"), "{}", l.path);
}
if t.contains("{json}") {
assert!(planted.contains("a/b.json"), "{}", l.path);
}
if t.contains(SYNTHETIC) {
assert!(planted.contains(SYNTHETIC), "{}", l.path);
}
}
// A JSON ledger is falsified by an entry, not by a spec name.
// 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::GhostCeiling => {
let before = "{\n \"ceilings\": {\n \"a\": 1\n }\n}\n";
let planted = plant_text(before, &l.plant, "unused").expect("planted");
let planted =
plant_text(before, &l.plant, "unused", "unused").expect("planted");
assert!(planted.contains("planted-by-ledgers-audit"), "{}", l.path);
assert!(
serde_json::from_str::<serde_json::Value>(&planted).is_ok(),
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
# NOW -- Every ledger in the repository is now audited or excused with a measurement (2026-08-30)

## Every ledger in the repository is now audited or excused with a measurement (Refs #2864)

- Last pass the meta-gate covered 5 of 15 ledger-shaped files and named 8 as unclassified. All eight now carry a measurement, and four of them entered the audit: devhome, elab, json_parse and vector_data baselines. Nine planted into, six excused, ZERO unclassified.
- Extending it found a live defect. `check_json_parses.py` only ever SUBTRACTED its baseline from the current bad set, so an entry naming a file that now parses was never looked at -- `tri ledgers audit` planted one naming a file it had just parsed and the gate stayed green.
- Fixed with the idiom check_specs_generate.py already uses: DEPARTED (the file left the tracked set -- not progress) and FIXED (still tracked, now parsing -- remove the line), both failing.
- That immediately turned the gate red on a clean tree: SIX entries naming files in neither git nor the working tree. The scan finds ZERO unparseable and ZERO empty tracked JSON today, so the entire ledger was debt about things that had already left. Emptied; the gate now holds the line at zero.
- The four newly audited plants are false by construction in two different ways: a runtime lookup (`{spec}`, and a new `{json}` resolved to a tracked file that parses today) or a synthetic name that cannot exist. A test asserts the synthetic name occurs nowhere in the tree -- otherwise a hardcoded plant could rot into a line that is TRUE.
- The six exclusions each carry what was measured, not a shrug: type_conflicts.json carries `generated_by` and is an observation, not a claim; type_conflicts_classified.json CATCHES (exit 1, STALE) but its plant must clone a row's field shape, which Plant cannot express; lean_completeness_mismatches leaves `tri lean vacuous` at exit 0 both ways; two are gated by the corpus suite and too slow to plant into.
- Self-criticism: my first version of the synthetic-name test ran `git grep` from the crate directory while excluding a repo-root path, so the exclusion matched nothing and the test failed on its own source. A pathspec is resolved against the current directory.
31 changes: 31 additions & 0 deletions tools/check_json_parses.py
Original file line number Diff line number Diff line change
Expand Up @@ -241,6 +241,37 @@ def main():
known = baseline()
new_bad = [(r, w) for r, w in bad if r not in known]
new_empty = [r for r in empty if r not in known]

# An entry that outlives its debt. `known` was only ever SUBTRACTED from the
# current bad set, so a line naming a file that now parses was never looked
# at -- `tri ledgers audit` planted one naming a file it had just parsed and
# this gate stayed green. Two classes, as check_specs_generate.py separates
# them: a file that started parsing is progress and its line must go; a file
# that stopped being tracked did NOT start parsing, and reading its removal
# as progress is how a count improves by subtraction.
tracked = set(tracked_json())
current = {r for r, _ in bad} | set(empty)
departed = sorted(known - tracked)
fixed = sorted((known & tracked) - current)
if departed or fixed:
if departed:
print(f"DEPARTED: {len(departed)} baseline entr(ies) name a file this "
f"repository no longer tracks.")
print("They did not start parsing -- they left the measured set, which")
print("reads as progress in the count below and is not:")
for r in departed[:10]:
print(f" {r}")
print()
if fixed:
print(f"FAIL: {len(fixed)} baseline entr(ies) name a file that PARSES today.")
print(f"An entry that outlives its debt is slack the next one hides in.")
print(f"Remove them from {BASELINE.name}:")
for r in fixed[:10]:
print(f" {r}")
print()
print(" python3 tools/check_json_parses.py --update-baseline")
return 1

if not new_bad and not new_empty:
print(f"OK: {total} tracked JSON files, none newly unparseable "
f"({len(bad) + len(empty)} known, listed in {BASELINE.name})")
Expand Down
Loading
Loading