Pin the cause, not just the count - #2777
Merged
Merged
Conversation
W699 rung 7. The ledger pinned how many tokens each spec discards. It did not
pin WHICH recovery took them, so a spec could swap 200 tokens of one defect for
200 of another and the ratchet would stay clean.
`parse-no-discard` entries now carry `discard_by_channel`:
"discard_tokens": 208,
"discard_by_channel": { "bdd-block-fallback": 208 }
Three rules, and only the first is about drift:
* the SPLIT moving is a failure even when the total does not move
* the map must SUM to the pinned total -- a ledger that disagrees with ITSELF
is reported before it is used to judge anything. Two accounts of one
quantity are kept deliberately: the 27-token gap in the channel recording
was found only because a second account existed to disagree with.
* pinned by total and not by channel counts as UNPINNED. Half a bound is not
a bound, and it lands in the same list for the same reason.
Seen failing on purpose, twice. Moving 5 tokens between two channels at a
constant total fires DISCARD CHANNEL while WORSENED and IMPROVED stay silent --
which is the whole point. Inflating one channel without touching the total fires
the self-consistency arm: "pinned map sums to 215 but pinned total is Some(208)".
Blessed: 86 entries, 30 408 tokens, and the per-channel sums agree with the
totals exactly.
bdd-block-fallback 23852
brace-body 4602
top-level-resync 1894
clause-junk 33
stray-brace 27
cargo test --no-fail-fast 2432 passed, 0 failed
suite --ratchet RATCHET: CLEAN, exit 0
Refs #2754
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-08-29 03:23:54 UTC
Summary
Seal Status
|
W699 rung 8, and a correction to my own plan.
Last iteration's report named `brace-body` -- 4 602 tokens, 459 runs -- as "a
channel nobody has looked at" and proposed it as the next rung. Reading the
ledger that rung 7 had just filled:
brace-body WITHOUT bdd-block-fallback: 3 specs, 88 tokens
brace-body WITH it: 40 specs, 4 514 tokens
Ninety-eight percent of it is collateral. A braced statement inside a braceless
block that fell back is the SAME event, reached through a second function --
`restore_bdd_fallback` resyncs, the resync meets a `{`, and `skip_brace_body`
consumes it. The split counted one event as two.
while (i < 3) { <- the block gives up here, bdd-block-fallback
var j : usize = 0; <- and everything inside is brace-body
}
The channel is now contextual, using the flag rung 6 already had:
bdd-block-fallback 23852
brace-body/in-fallback 4345 93% is ONE class
top-level-resync 1894
brace-body 257 the independent class, 10 specs
clause-junk 33
stray-brace 27
So the work I advertised at 4 602 tokens is 257. Recorded rather than quietly
re-scoped: a plan built on a number that has since been measured properly should
say so, especially when the number was mine.
Re-blessed (channel names changed): 86 entries, 30 408 tokens, sums consistent.
cargo test --no-fail-fast 2432 passed, 0 failed
suite --ratchet RATCHET: CLEAN, exit 0
check_seal_coverage.py exit 0
check_elab_ratchet.py exit 0
Refs #2754
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Contributor
PR DashboardGenerated at: 2026-08-29 03:32:36 UTC
Summary
Seal Status
|
…ount (167-169) A channel split can count one event twice: 98% of the class I recommended as the next rung turned out to be collateral of the class above it, and the work was 257 tokens rather than 4602. Adding a second dimension to an amnesty means restating every rule that governed the first, including the boring one that says a bound must exist. And the derivable field stays: a second account of one quantity is the only thing that can disagree with the first. Refs #2754 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
1 similar comment
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-08-29 03:33:13 UTC
Summary
Seal Status
|
gHashTag
added a commit
that referenced
this pull request
Aug 29, 2026
…ot one
W699 rung 12, plus the regression it caused and the ledger entry that caught it.
A body that OPENS with a call had no earlier clause to take a column from, so
`first_clause_col` was None and the bare-call arm never ran:
bench ternary_not_performance
@setEvalBranchQuota(10000); <- and everything after it
var result : i32 = 0;
The const/var arm already seeds the column from the statement itself (W904); this
is the same seed.
THE SEED EXPOSED A HOLE NOTHING HAD EVER TESTED. `given (exp, mant) = f(15)` is
an identifier followed by `(`, so the bare-call arm matched a CLAUSE KEYWORD.
Before the seed the arm could not reach a block's first token at all, which is
why the shape had never been reached. Clause keywords are now excluded.
discarded tokens 23926 -> 23644 (-282)
specs discarding 76 -> 75
Zig 214, rustc 214, cc 163, iverilog 373, ALL FOUR 66 -- all held
THE PER-ENTRY RATCHET CAUGHT ITS AUTHOR, ONE DAY OLD. With only the seed, the
corpus total FELL and no acceptance column moved -- a clean win by every
aggregate. The ledger disagreed:
> phi_split_optimality.t27 discards 214, pinned at 129 (+85)
> phi_universal_attractor.t27 discards 108, pinned at 73 (+35)
A total that falls can hide two entries that rose. That is what #2777 was for.
AND MY FIRST FIX FOR IT WAS WRONG. I assumed the seed skewed the W905 clause
anchor and stopped writing `first_clause_col`. The total went 23 738 -> 24 046
and the spec was still broken: a plausible cause, disproved in one build. The
real one was the clause keyword.
Also here: docs/DISCARD_WHAT_IS_LEFT.md -- a census of the 964 remaining fallback
events, classified by reading the source line each fired on. 93.5% is
QUANTIFICATION in four notations, which makes #2774 not "a construct in 35 specs"
but nearly everything left. It also corrects this loop's own earlier report,
which called the 38 `for` events a Zig-capture syntax problem: 35 of the 38 are
quantifier SUFFIXES (`... for all Trit`) and belong to #2774.
parse-conform 25/25, new case load-bearing
cargo test --no-fail-fast 2432 passed, 0 failed
suite --ratchet RATCHET: CLEAN, ledger 167 -> 166
check_seal_coverage.py exit 0
check_elab_ratchet.py exit 0
check_specs_generate.py exit 0
Skill 179-181, including the one about this checkout being shared: this branch
was parked under me mid-iteration by another session and the work was finished
in a private worktree.
Refs #2754, #2774
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
gHashTag
added a commit
that referenced
this pull request
Aug 29, 2026
* wip(parser): seed the column for a body that OPENS with a call
W699 rung 12, PARKED UNMERGED. Written and measured, not landed: the repository
owner has forked to continue the parser line, and this touches the same arm.
A bench body beginning with a call --
bench ternary_not_performance
@setEvalBranchQuota(10000);
var result : i32 = 0;
-- had no earlier clause to take a column from, so `first_clause_col` was still
None, the bare-call arm never ran, and the whole block fell back. The const/var
arm already seeds the column from the statement itself when it is the first thing
in the block (W904); this is the same seed. The `c > 1` guard against unindented
blocks is unchanged, and a failed parse un-seeds the column so a later shallower
statement cannot pass a guard on a column the block never established.
Measured in a dirty tree, which is how it was found:
discarded tokens 23926 -> 23738 (-188)
specs discarding 76 -> 75
NOT verified beyond that: no corpus run, no conformance case, no re-bless. Whoever
picks this up owes it those three things.
Refs #2754
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* wip(parser): the conformance case for rung 12, reunited with its fix
This case was written with the rung-12 fix and left behind in the working tree
when the fix was parked. On master it is a test for a fix that is not there:
`parse-conform` exits 1 with
case a_body_may_open_with_a_call
expected Full with 1 decl(s), 0 discarded
actual Full with 1 decl(s), 14 discarded
A case and the change it covers are one unit. Splitting them leaves a red gate
behind and a fix nobody can tell is load-bearing.
Refs #2754
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* fix(parser): a body may open with a call -- and a clause keyword is not one
W699 rung 12, plus the regression it caused and the ledger entry that caught it.
A body that OPENS with a call had no earlier clause to take a column from, so
`first_clause_col` was None and the bare-call arm never ran:
bench ternary_not_performance
@setEvalBranchQuota(10000); <- and everything after it
var result : i32 = 0;
The const/var arm already seeds the column from the statement itself (W904); this
is the same seed.
THE SEED EXPOSED A HOLE NOTHING HAD EVER TESTED. `given (exp, mant) = f(15)` is
an identifier followed by `(`, so the bare-call arm matched a CLAUSE KEYWORD.
Before the seed the arm could not reach a block's first token at all, which is
why the shape had never been reached. Clause keywords are now excluded.
discarded tokens 23926 -> 23644 (-282)
specs discarding 76 -> 75
Zig 214, rustc 214, cc 163, iverilog 373, ALL FOUR 66 -- all held
THE PER-ENTRY RATCHET CAUGHT ITS AUTHOR, ONE DAY OLD. With only the seed, the
corpus total FELL and no acceptance column moved -- a clean win by every
aggregate. The ledger disagreed:
> phi_split_optimality.t27 discards 214, pinned at 129 (+85)
> phi_universal_attractor.t27 discards 108, pinned at 73 (+35)
A total that falls can hide two entries that rose. That is what #2777 was for.
AND MY FIRST FIX FOR IT WAS WRONG. I assumed the seed skewed the W905 clause
anchor and stopped writing `first_clause_col`. The total went 23 738 -> 24 046
and the spec was still broken: a plausible cause, disproved in one build. The
real one was the clause keyword.
Also here: docs/DISCARD_WHAT_IS_LEFT.md -- a census of the 964 remaining fallback
events, classified by reading the source line each fired on. 93.5% is
QUANTIFICATION in four notations, which makes #2774 not "a construct in 35 specs"
but nearly everything left. It also corrects this loop's own earlier report,
which called the 38 `for` events a Zig-capture syntax problem: 35 of the 38 are
quantifier SUFFIXES (`... for all Trit`) and belong to #2774.
parse-conform 25/25, new case load-bearing
cargo test --no-fail-fast 2432 passed, 0 failed
suite --ratchet RATCHET: CLEAN, ledger 167 -> 166
check_seal_coverage.py exit 0
check_elab_ratchet.py exit 0
check_specs_generate.py exit 0
Skill 179-181, including the one about this checkout being shared: this branch
was parked under me mid-iteration by another session and the work was finished
in a private worktree.
Refs #2754, #2774
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
* chore(ledger): re-bless after merging master
The W700 pin (`max_gate_failures`) came in from master; the discard numbers are
this branch's. Their schema, my measurements.
Refs #2754
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
---------
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
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.
Refs #2754
The ledger pinned how many tokens each spec discards. It did not pin which recovery took them, so a spec could swap 200 tokens of one defect for 200 of another and the ratchet would stay clean.
Three rules, and only the first is about drift
Seen failing on purpose, twice
Moving 5 tokens between two channels at a constant total:
The two totals arms stay silent — which is the whole point. And inflating one channel without touching the total fires the self-consistency arm:
Three unit tests cover the swap, the self-inconsistency, and the half-bound.
Blessed
86 entries, 30 408 tokens, per-channel sums agreeing with the totals exactly:
🤖 Generated with Claude Code