Repository navigation
fix(t27b): the ledger stores no total over its entries -- counts are derived, as steward.t27 decides (Closes #7859) - #7862
Conversation
…ed, as steward.t27 decides (Closes #7859) docs/reports/t27b_expectations.json kept `counts` (pass, pass_vacuous, not_pass) in its header. Every PR that adds a spec moved the same "pass" line: on 2026-10-08 #7579, #7586 and #7626 went dirty three times in two hours on that line alone while their entries merged cleanly, and the fpga jobs take an hour. - steward.t27: header_stored(field) -- a header field is stored only when it is not a total over the entries. counts is one; max_not_pass is not (the ratchet's promise; a pass entry does not move it). 4 tests and an invariant; 128/128 pass. gen/c/tri/t27b/steward.c regenerated by t27c gen-c. - t27b.py: binds header_stored and dump_ledger writes only the fields the spec stores; ledger_counts derives the totals bless prints. An unknown field is an error. No other hand-written foreign file moves. - The committed ledger loses its counts block, nothing else. - test_a_t27b_spec_cannot_move_silently.py: two branches that bless one and two new pass specs merge cleanly; with rules that store the counts the same merge conflicts (negative control). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01ScHVrGSr6zZUdwkdC8DR9k
The ledger takes master's entries; dump_ledger drops the counts. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01ScHVrGSr6zZUdwkdC8DR9k
|
own-language is red by design on this PR and needs the owner's
Generated by Claude Code |
|
duplicate-bodies is not this PR's. It has been red on master since a6d4e55 (#7490, run), and
This PR touches neither file. No fix exists yet. The two ways out are reusing the linker's bodies, or Generated by Claude Code |
duplicate-bodies is red on master since #7490; the same three-line bless as #7868, so this PR is green on it now and the line no-ops once #7868 lands. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01ScHVrGSr6zZUdwkdC8DR9k
The ledger takes master's entries; dump_ledger drops the counts. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01ScHVrGSr6zZUdwkdC8DR9k
PR DashboardGenerated at: 2026-10-08 17:39:16 UTC
Summary
Seal Status
|
duplicate-bodies stays red on master after #7864 because of `assign 3`; the same line as #7874, which no-ops once it lands. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01ScHVrGSr6zZUdwkdC8DR9k
The previous commit wrote an empty tools/duplicate_bodies_baseline.txt (a git show of a branch that was not fetched). This restores it: master's ledger plus the four lines of #7864 and #7874, nothing else (dupe_scan: ok). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01ScHVrGSr6zZUdwkdC8DR9k
|
t27b-native-ratchet is not this PR's. It reports the same findings as master's latest completed run (81da894, job 113450310705): UNEXPECTED PASS 2 ( There is no traceback and no UNREADABLE verdict. The native ratchet reads the ledger without No fix exists yet. The cure is a bless PR from a fresh lab run of master ( Generated by Claude Code |
|
Check L1 TRACEABILITY is red because of my own commit: Fixing that message would mean rewriting a pushed branch, and force-push is forbidden in this workspace. The check is not required, and the PR is merged by squash under the title Generated by Claude Code |
PR DashboardGenerated at: 2026-10-08 18:18:34 UTC
Summary
Seal Status
|
PR DashboardGenerated at: 2026-10-08 18:19:44 UTC
Summary
Seal Status
|
PR DashboardGenerated at: 2026-10-08 20:04:47 UTC
Summary
Seal Status
|
The ledger takes master's entries; dump_ledger drops the counts. The duplicate-bodies lines this branch carried are on master now (#7864, #7887). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01ScHVrGSr6zZUdwkdC8DR9k
The ledger takes master's entries; dump_ledger drops the counts. The duplicate-bodies lines this branch carried are on master now (#7864, #7887). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01ScHVrGSr6zZUdwkdC8DR9k
PR DashboardGenerated at: 2026-10-08 23:22:34 UTC
Summary
Seal Status
|
The ledger takes master's entries; dump_ledger drops the counts. The duplicate-bodies lines this branch carried are on master now (#7864, #7887). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01ScHVrGSr6zZUdwkdC8DR9k
PR DashboardGenerated at: 2026-10-08 23:26:15 UTC
Summary
Seal Status
|
Pull Request Checklist
Closes #7859specs/tri/t27b/steward.t27has no seal;gen/c/tri/t27b/steward.cis regenerated byt27c gen-cand byte-identical to itDescription
docs/reports/t27b_expectations.jsonstoredcounts(pass,pass_vacuous,not_pass) in its header. Those numbers are a total overentries, so every PR that adds a spec changed the same"pass"line. On 2026-10-08, #7579, #7586 and #7626 wentdirtythree times in two hours on that line alone, while their entries merged cleanly. The fpga jobs take an hour, so a spec PR could not outrun the t27b PRs landing on master.The rule is written in t27 first.
steward.t27gainsheader_stored(field): a header field is stored only when it is not a total over the entries.countsis such a total;max_not_passis not. The cap is the ratchet's promise (non-pass may only fall), and a PR that adds a pass entry does not move it.Changes
specs/tri/t27b/steward.t27:header_stored, plus 4 tests and an invariant. 128 of 128 tests pass, 0 vacuous.gen/c/tri/t27b/steward.c: regenerated byt27c gen-c.scripts/tri_loop/t27b.py, a listed foreign exception (30 lines added): bindsheader_stored.dump_ledgerwrites only the fields the spec stores, andledger_countsderives the totalsblessprints. An unknown header field is an error.docs/reports/t27b_expectations.json: thecountsblock is removed; nothing else changes.scripts/ci/test_a_t27b_spec_cannot_move_silently.py(28 lines added): it readreal["counts"]and now checks that there are none. New case: two branches that bless 1 and 2 new pass specs merge without a conflict, and with rules that store the counts the same merge conflicts (negative control).docs/now/2026-10-08-t27b-ledger-derived-counts.md.Testing
The negative control was seen red before it was made robust. In its first form both branches added one entry each, so both moved
"pass": 2 → 3identically and git merged the stored counts cleanly. The control now uses 1 and 2 new entries, as real spec PRs do (#7579 added 1, #7586 3, #7626 18).Review Notes
scripts/ci/test_a_t27b_spec_cannot_move_silently.pyis a hand-written.pywith no entry intools/policy/foreign-exceptions.txt, and its old assertion reads the removed field, so the test cannot stay as it is. The foreign-line budget passes (28 + 30 of 80, each under 40). The PR needs the owner'sowner-approved-foreignlabel. I did not add it myself.max_not_passstays stored on purpose. A spec PR that adds a non-pass entry still moves it, but that is rarer, and it is a decision a reviewer should see.🤖 Generated with Claude Code
https://claude.ai/code/session_01ScHVrGSr6zZUdwkdC8DR9k
Generated by Claude Code