Every dropped token now names the recovery that took it - #2776
Merged
Conversation
…k it
W699 rungs 5 and 6. Yesterday's classification was a keyword match over printed
traces -- it saw the word `forall` and called the bucket `forall`. The parser
already writes down every token it discards, so the question is now asked of the
record.
WHAT THE RECORD SAYS, and it is not what the heuristic said:
channel tokens runs
bdd-block-fallback 23852 1484 78%
brace-body 4602 459
top-level-resync 1894 99
stray-brace / stmt-recovery the rest
heuristic yesterday: forall/==> ... 20991
Five recovery sites now record a channel beside each span, and
`restore_bdd_fallback` marks its resync so a WHOLE-BLOCK fallback is
distinguishable from an ordinary top-level skip -- both call the same function.
`parse-complete --causes` groups by (channel, head of run); `tri discard classify`
reads that instead of guessing, and the old buckets are DELETED rather than kept
as a cross-check: a heuristic beside a reading is two answers to one question.
RUNG 5: the parser named the shape and threw it away.
// BDD-style fn: `fn name() given ... then ...` -- a keyword-style test
// spelled as a fn (linker.t27). Detect BEFORE return-type parsing.
if ... lexeme == "given" {
self.skip_to_next_top_level(); // <- every clause, gone
return Ok(decl);
}
The comment cites the file it silently empties. Detection is unchanged -- same
token, same lexeme -- and the action is now the shared clause parser that already
serves `test`, `invariant` and `bench`.
specs discarding 87 -> 86 (the first time the population has moved)
discarded tokens 30451 -> 30408
Zig 217, rustc 214, cc 158, iverilog 373, ALL FOUR 63 -- all held
Only 43 tokens, against the 2 453 that `given` heads corpus-wide. That gap IS the
finding: a head token says what the parser stopped on, a channel says which
recovery threw it away, and reporting one as the other overstates every fix you
plan. The arm stays narrow because the corpus holds exactly one occurrence --
broadening it would be speculative.
AN ACCOUNTING GAP, FOUND AND CLOSED. The channel vector was pushed at "all three"
recording sites; two more existed at a different indentation. `zip` truncated to
the shorter vector and printed a clean, plausible table 27 tokens short. Nothing
failed -- the only signal was a total disagreeing with `parse-complete`'s. The
accessor now REFUSES on a length mismatch rather than zipping, and the two
accounts agree exactly at 30 408.
parse-conform 21/21
cargo test --no-fail-fast 2429 passed, 0 failed
suite --ratchet RATCHET: CLEAN, ledger 178 -> 177
check_seal_coverage.py exit 0
check_specs_generate.py exit 0
Skill 162-164.
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 02:23:11 UTC
Summary
Seal Status
|
The elaboration ratchet caught the previous commit and it was right: linker
4 -> 6.
Keeping the FnDecl and filling its body made every backend treat it as a real
function. `gen-verilog` emits synthesizable RTL for functions and deliberately
does NOT lower tests, so the recovered clauses became
\assert ((is_local(sym) == 1'b1));
is_local_test = \assert ((is_global(sym) == 1'b0));
inside a task -- "Enable of unknown task ``assert''", and an assignment to the
task's own name. A task body cannot assert, and the gate said so.
`fn name() given ... then ...` IS a test, so it now parses to a TestBlock. That
teaches no backend anything new: each already knows whether it lowers tests, and
each now does the right thing with this one.
elaboration errors 176 (baseline 176) -- OK, no module gained any
discarded tokens 30408, 86 specs -- unchanged from the previous commit
Zig 217, rustc 214, cc 158, iverilog 373, ALL FOUR 63 -- all held
Two notes on how this was nearly missed. I first measured with bare `iverilog`,
which reports "Size cast requires SystemVerilog" for constructs the gate's
`-g2012 -DSIMULATION` accepts -- so my reading showed the branch with FEWER
errors than master while the gate showed more. And under the default flags the
branch really does lose one error, because master's empty task trips "Task body
with no statements". Two different rulers, two opposite verdicts, both about the
same file.
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 02:47:48 UTC
Summary
Seal Status
|
Same file, bare iverilog vs the gate's `-g2012 -DSIMULATION`, opposite verdicts. And when recovered content lands in the wrong node kind, change the node rather than the four backends that consume it. 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 02:48:17 UTC
Summary
Seal Status
|
This was referenced Aug 29, 2026
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
Yesterday's
tri discard classifywas a keyword match over printed traces: it saw the wordforalland called the bucketforall. The parser already writes down every token it throws away, so the question is now asked of the record.What the record says, and it is not what the heuristic said
against yesterday's
forall/==> … 20991.Five recovery sites now record a channel beside each span, and
restore_bdd_fallbackmarks its resync so a whole-block fallback is distinguishable from an ordinary top-level skip — both call the same function.parse-complete --causesgroups by (channel, head-of-run);tri discard classifyreads that instead of guessing.The old buckets are deleted, not kept as a cross-check. A heuristic standing beside a reading is two answers to one question — the shape of #2767, one level down.
brace-bodyat 4 602 tokens is a channel nobody has looked at: a braced body skipped wholesale, a different defect class from the braceless fallback.Rung 5 — the parser named the shape, then threw it away
The comment cites the file it silently empties. Someone understood the shape well enough to special-case it and stopped one line short of lowering it. Detection is unchanged — same token, same lexeme — and the action is now the shared clause parser that already serves
test,invariantandbench.Only 43 tokens, against the 2 453 that
givenheads corpus-wide — and that gap is the finding. A head token says what the parser stopped on; a channel says which recovery threw it away. Reporting one as the other overstates every fix you plan.The arm stays narrow: the corpus holds exactly one occurrence of the shape, so broadening it would be speculative.
An accounting gap, found and closed
The channel vector was pushed at "all three" recording sites. Two more existed at a different indentation, and
ziptruncated to the shorter vector and printed a clean, plausible table 27 tokens short. Nothing failed. The only signal was a total that disagreed withparse-complete's.Refuses instead of truncating. The two accounts now agree exactly at 30 408 — and the reason the gap was findable at all is that a second independent account of the same quantity already existed.
🤖 Generated with Claude Code