fix(tri): every ledger is now audited or excused with a measurement - #2956
Merged
Conversation
Last pass the meta-gate covered 5 of 15 ledger-shaped files and printed eight as
"NOT YET CLASSIFIED". All eight now carry a measurement, and four entered the
audit.
ledger-shaped files on disk 15 planted into 9, excused 6, unclassified 0
EXTENDING IT FOUND A LIVE DEFECT. `check_json_parses.py` only ever SUBTRACTED
its baseline from the current bad set:
new_bad = [(r, w) for r, w in bad if r not in known]
so an entry naming a file that now PARSES was never looked at. `tri ledgers
audit` planted a line naming a file it had just parsed, and the gate stayed
green. Fixed with the idiom `check_specs_generate.py` already uses, and for the
same stated reason -- two classes, both failing:
* DEPARTED -- the file left the tracked set. It did not start parsing, and
reading its removal as progress is how a count improves by subtraction.
* FIXED -- still tracked, no longer bad. The line must go.
That turned the gate red on a clean tree: SIX entries naming files in neither
git nor the working tree, five under `.trinity/icarus-baselines/specs/scratch/`
and `research/toda_derivation.json`. The scan finds ZERO unparseable and ZERO
empty tracked JSON files today, so the whole ledger was debt about things that
had already left. Emptied, with the measurement written into the file: the gate
now holds the line at zero and any unparseable JSON fails, with no slack.
FOUR NEW LEDGERS, each proven to catch before being added:
caught tools/devhome_baseline.txt by tools/check_devhome_paths.py
caught tools/elab_baseline.txt by tools/check_elab_ratchet.py
caught tools/json_parse_baseline.txt by tools/check_json_parses.py
caught tools/vector_data_baseline.txt by tools/check_vector_data.py
Their 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 else in the tree -- without that, a hardcoded plant rots into a line
that is TRUE and the audit quietly stops testing that ledger.
SIX EXCLUSIONS, each carrying what was measured rather than a shrug:
* type_conflicts.json carries `generated_by` and is regenerated by `tri types
dup` -- an observation, not a ledger of claims. A planted line survives
until the next regeneration erases it.
* type_conflicts_classified.json CATCHES: a cloned row renamed PlantedByAudit
gives `tri types classified` exit 1, `STALE PlantedByAudit: classified, but
no longer conflicting`. Not planted into because the plant must clone a
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.
* lean_completeness_mismatches.json: a planted entry leaves `tri lean vacuous`
at exit 0 both ways. It reports and does not gate.
* gen_verilog_smoke_baseline.json and suite_expectations.json are read by the
corpus suite -- minutes per run, and a meta-gate nobody runs before
committing is not a meta-gate.
* withdrawn_live_baseline.txt is keyed by sha1 of the line it excuses.
Also mine: the first version of the synthetic-name test ran `git grep` from the
crate directory while excluding a repository-root path, so the exclusion matched
nothing and the test failed on its own source. A pathspec resolves against the
current directory.
cargo test -p tri 392 passed, 0 failed (was 391; two new, two rewritten)
cargo clippy 120 warnings, same as master
tri ledgers audit 9 caught, 0 missed, exit 0
Refs #2864
… ways to be false by construction; a pathspec resolves against cwd (Refs #2864)
Contributor
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-08-30 15:04:28 UTC
Summary
Seal Status
|
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
…section documenting it (Refs #2864)
Contributor
PR DashboardGenerated at: 2026-08-30 15:09:33 UTC
Summary
Seal Status
|
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-08-30 15:36:11 UTC
Summary
Seal Status
|
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-08-30 15:36:31 UTC
Summary
Seal Status
|
Contributor
PR DashboardGenerated at: 2026-08-30 15:47:14 UTC
Summary
Seal Status
|
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Every ledger-shaped file is now audited or excused with a measurement
Last pass the meta-gate covered 5 of 15 and printed eight as
NOT YET CLASSIFIED. All eight now carry a measurement, and four entered theaudit:
Extending it found a live defect
check_json_parses.pyonly ever subtracted its baseline from the currentbad set:
so an entry naming a file that now parses was never looked at.
tri ledgers auditplanted a line naming a file it had just parsed, and thegate stayed green.
Fixed with the idiom
check_specs_generate.pyalready uses, and for the samestated reason — two classes, both failing:
And that turned the gate red on a clean tree
Six entries named files in neither git nor the working tree — five under
.trinity/icarus-baselines/specs/scratch/, plusresearch/toda_derivation.json.The scan finds zero unparseable and zero empty tracked JSON files today,
so the whole ledger was debt about things that had already left.
Emptied, with the measurement written into the file. The gate now holds the line
at zero: any unparseable JSON fails, with no slack to hide in.
Four new ledgers, each proven to catch before being added
Their plants are false by construction in two different ways — a runtime
lookup (
{spec}, and a new{json}resolved to a tracked file that parsestoday), or a synthetic name that cannot exist. A test asserts the synthetic
name occurs nowhere else in the tree; without it a hardcoded plant rots into a
line that is true and the audit quietly stops testing that ledger.
Six exclusions, each carrying what was measured
type_conflicts.jsoncarriesgenerated_byand is regenerated bytri types dup— an observation, not a ledger of claims. A planted linesurvives only until the next regeneration erases it.
type_conflicts_classified.jsoncatches: a cloned row renamedPlantedByAuditgivestri types classifiedexit 1,STALE PlantedByAudit: classified, but no longer conflicting. Not plantedinto because the plant must clone a row's field shape, which
Plantcannotexpress — and an ill-shaped plant would fail the gate on its shape, a
catch for the wrong reason.
lean_completeness_mismatches.json: a planted entry leavestri lean vacuousat exit 0 both ways. It reports and does not gate.gen_verilog_smoke_baseline.jsonandsuite_expectations.jsonareread by the corpus suite — minutes per run, and a meta-gate nobody runs before
committing is not a meta-gate.
withdrawn_live_baseline.txtis keyed by the sha1 of the line it excuses.Also mine
The first version of the synthetic-name test ran
git grepfrom the cratedirectory while excluding a repository-root path, so the exclusion matched
nothing and the test failed on its own source. A pathspec resolves against the
current directory.
Checks
cargo test -p tri— 392 passed, 0 failed (was 391; two new, two rewritten)cargo clippy --all-targets— 120 warnings, identical to mastertri ledgers audit— 9 caught, 0 missed, exit 0python3 tools/check_json_parses.py— exit 0; planting a parsing file → FAIL; planting an absent name → DEPARTEDRefs #2864