From 937e72ed6ee216cebe858b43a2d834a6a3d5b143 Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Sat, 29 Aug 2026 09:22:13 +0700 Subject: [PATCH 1/3] feat(parser,tri): every dropped token now names the recovery that took 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 --- .claude/skills/ci-gates/SKILL.md | 54 +++++++ .trinity/seals/Linker.json | 8 +- .trinity/seals/fpga_Linker.json | 14 +- bootstrap/src/compiler.rs | 78 +++++++++- bootstrap/src/main.rs | 127 ++++++++++++++++- bootstrap/src/parse_conform.rs | 8 ++ bootstrap/stage0/FROZEN_HASH | 2 +- cli/tri/src/discard.rs | 133 +++++------------- ...-the-parser-do-not-grep-what-it-printed.md | 8 ++ docs/reports/suite_expectations.json | 10 +- 10 files changed, 320 insertions(+), 122 deletions(-) create mode 100644 docs/now/2026-08-29-ask-the-parser-do-not-grep-what-it-printed.md diff --git a/.claude/skills/ci-gates/SKILL.md b/.claude/skills/ci-gates/SKILL.md index cae167c369..423b6b60ee 100644 --- a/.claude/skills/ci-gates/SKILL.md +++ b/.claude/skills/ci-gates/SKILL.md @@ -5735,3 +5735,57 @@ measured, which is exactly what makes one unmeasured number dangerous. Corrected by a follow-up commit, not an amend (see 155). **Write the number after running the command, in the same minute, or do not write it.** + +## 162. Ask the parser what it dropped instead of grepping what it printed + +Yesterday's `tri discard classify` 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 throws away, so the question could be asked of the record instead. + +Two answers changed: + + heuristic: forall/==> ......... 20 991 + record: bdd-block-fallback ... 23 852 (78%, one channel) + brace-body ........... 4 602 + top-level-resync ..... 1 894 + +And the head token is not the channel. `given` was the fourth-largest head at +2 453 tokens, which read like a fn-shaped defect worth thousands. Fixing that arm +recovered **43**. The other 2 410 came from braceless blocks falling back — a +different defect wearing the same first word. + +**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.** + +## 163. `zip` on two parallel vectors is a silent truncation + +I added a channel vector beside the existing span vector, pushed at "all three" +recording sites, and zipped them. The total came out 27 tokens short of +`parse-complete`'s — two more push sites existed at a different indentation and +my search pattern had missed them. + +`zip` truncated to the shorter side and reported a clean, plausible, wrong table. +Nothing failed. The only signal was a total that did not match another account of +the same thing. + + if spans.len() != channels.len() { return Err(...) } + +**Two vectors that must stay in lockstep need an assertion, not a `zip`.** And the +reason the gap was findable at all is that a second, independent account of the +same quantity already existed — which is the argument for keeping both. + +## 164. The parser named the shape, then 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 self.current.kind == TokenKind::Ident && self.current.lexeme == "given" { + self.skip_to_next_top_level(); // <- every clause, gone + return Ok(decl); + } + +The comment cites the exact file it silently empties. Someone understood the shape +well enough to special-case it and stopped one line short of lowering it. + +**A comment that names a construct beside a `skip` is a fix that was scoped and +not finished.** Grep for that pair: recognition followed by discard is a different +and better-signposted target than an unhandled shape nobody has looked at. diff --git a/.trinity/seals/Linker.json b/.trinity/seals/Linker.json index b0a1137813..5051aea013 100644 --- a/.trinity/seals/Linker.json +++ b/.trinity/seals/Linker.json @@ -1,8 +1,8 @@ { - "gen_hash_c": "sha256:108d46508c8fe24bd3bca14b4b54d51c3d8827c6928c2f9be71995e446e0c857", - "gen_hash_rust": "sha256:f6ea2b804287146898f363f3c2f0f29e4185bc7a60ee3fc6c1a35e0a93143760", - "gen_hash_verilog": "sha256:78cfa653fb656438b2dff0eea3df9198dc1ade38253897016a7031868c63018d", - "gen_hash_zig": "sha256:e21e5e37dd9d05dea274649d7e956c7899d72bfe26285d9a78541993510c4d56", + "gen_hash_c": "sha256:3375a8f992fd63e359abe881dd254965a5095911df624ab9453b2c21092e5fd4", + "gen_hash_rust": "sha256:838f26e311ccdeb0812827225cf3380f3b26accf47e31f01439425a59032c969", + "gen_hash_verilog": "sha256:4a4cb3732aef18ce3656fa6c56e78950bf849460549cd5db16b5d542d5aaad53", + "gen_hash_zig": "sha256:e3e90b0920d1da9a26f32c58eaafe3c2c1cc77f97afe89278db24838ef3bd684", "module": "Linker", "ring": 12, "sealed_at": "2026-08-28T18:19:55Z", diff --git a/.trinity/seals/fpga_Linker.json b/.trinity/seals/fpga_Linker.json index 1633846256..6c6f43d1ac 100644 --- a/.trinity/seals/fpga_Linker.json +++ b/.trinity/seals/fpga_Linker.json @@ -1,12 +1,12 @@ { - "gen_hash_c": "sha256:108d46508c8fe24bd3bca14b4b54d51c3d8827c6928c2f9be71995e446e0c857", - "gen_hash_rust": "sha256:f6ea2b804287146898f363f3c2f0f29e4185bc7a60ee3fc6c1a35e0a93143760", - "gen_hash_verilog": "sha256:78cfa653fb656438b2dff0eea3df9198dc1ade38253897016a7031868c63018d", - "gen_hash_zig": "sha256:e21e5e37dd9d05dea274649d7e956c7899d72bfe26285d9a78541993510c4d56", + "gen_hash_c": "sha256:3375a8f992fd63e359abe881dd254965a5095911df624ab9453b2c21092e5fd4", + "gen_hash_rust": "sha256:838f26e311ccdeb0812827225cf3380f3b26accf47e31f01439425a59032c969", + "gen_hash_verilog": "sha256:4a4cb3732aef18ce3656fa6c56e78950bf849460549cd5db16b5d542d5aaad53", + "gen_hash_zig": "sha256:e3e90b0920d1da9a26f32c58eaafe3c2c1cc77f97afe89278db24838ef3bd684", "module": "Linker", "ring": 12, - "sealed_at": "2026-08-28T18:19:55Z", - "sealed_by": "t27c-bootstrap@0.1.0", + "sealed_at": "2026-08-29T02:18:08Z", + "sealed_by": "t27c-bootstrap@0.2.0", "spec_hash": "sha256:64a8091d1c5d8163af7ce400dee2b8ffbe713584045340e1126a0b7560b04c6e", "spec_path": "specs/fpga/linker.t27" -} +} \ No newline at end of file diff --git a/bootstrap/src/compiler.rs b/bootstrap/src/compiler.rs index b1c5871efa..540e01451d 100644 --- a/bootstrap/src/compiler.rs +++ b/bootstrap/src/compiler.rs @@ -1093,6 +1093,17 @@ pub struct Parser { /// told us 55,563 tokens vanish; only reading them can say whether any of /// it is content a theorem depends on. See T43. dropped_spans: Vec<(u32, String)>, + /// W699: WHICH recovery threw each token away, parallel to `dropped_spans`. + /// + /// The head token of a dropped run says what the parser stopped ON. It does + /// not say which of the four recovery channels did the dropping, and the two + /// are different questions: `given` is the fourth-largest head in the corpus + /// and only 43 of its 2 453 tokens came from the fn arm that names it. + dropped_channels: Vec<&'static str>, + /// Set by `restore_bdd_fallback` for the duration of its resync, so the + /// tokens a WHOLE-BLOCK fallback discards are distinguishable from an + /// ordinary top-level resync. Both call the same function. + in_bdd_fallback: bool, } #[derive(Clone)] @@ -1155,6 +1166,8 @@ impl Parser { bdd_role_preset: false, bdd_first_col_preset: None, dropped_spans: Vec::new(), + dropped_channels: Vec::new(), + in_bdd_fallback: false, } } @@ -1263,6 +1276,7 @@ impl Parser { if self.dropped_spans.len() < 20000 { self.dropped_spans .push((self.current.line as u32, self.current.lexeme.clone())); + self.dropped_channels.push("brace-body"); } self.advance(); } @@ -1330,6 +1344,7 @@ impl Parser { if self.dropped_spans.len() < 20000 { self.dropped_spans .push((self.current.line as u32, self.current.lexeme.clone())); + self.dropped_channels.push("clause-junk"); } if self.current.kind == TokenKind::LBrace { self.advance(); @@ -1425,6 +1440,14 @@ impl Parser { if self.dropped_spans.len() < 20000 { self.dropped_spans .push((self.current.line as u32, self.current.lexeme.clone())); + // W699: `restore_bdd_fallback` resyncs through this same + // function, and "a whole braceless block fell back" is a + // different finding from "a top-level item was skipped". + self.dropped_channels.push(if self.in_bdd_fallback { + "bdd-block-fallback" + } else { + "top-level-resync" + }); } self.advance(); } @@ -1551,6 +1574,7 @@ impl Parser { if self.dropped_spans.len() < 20000 { self.dropped_spans .push((self.current.line as u32, self.current.lexeme.clone())); + self.dropped_channels.push("stray-brace"); } self.advance(); self.parse_module_body(&mut module)?; @@ -2993,7 +3017,20 @@ impl Parser { // spelled as a fn (linker.t27). Detect BEFORE return-type parsing, // which would otherwise consume `given` as an identifier return type. if self.current.kind == TokenKind::Ident && self.current.lexeme == "given" { - self.skip_to_next_top_level(); + // W699 rung 5: this arm RECOGNISED the shape by name and then threw + // it away. `skip_to_next_top_level()` discarded every clause under + // such a fn -- 2 453 tokens across 19 specs, and `given` is the + // fourth-largest head token in the whole corpus discard. + // + // The shared clause parser already serves `test`, `invariant` and + // `bench`; a fn spelled as a test is the same body. Detection is + // unchanged -- same token, same lexeme -- only the action is. + // + // The column anchor is what the bench path (W905) had to set for the + // same reason: continuation statements need an anchor that the head + // never established, and without it the statement arms stay dark. + self.bdd_first_col_preset = Some(self.current.col); + self.parse_bdd_clauses(&mut decl); return Ok(decl); } @@ -3296,6 +3333,7 @@ impl Parser { if self.dropped_spans.len() < 20000 { self.dropped_spans .push((self.current.line as u32, self.current.lexeme.clone())); + self.dropped_channels.push("stmt-recovery"); } } match self.current.kind { @@ -6545,7 +6583,13 @@ impl Parser { } block.children.truncate(start_children); self.restore_state(entry); + // W699: nested fallbacks are possible, so save and restore rather than + // clearing -- an inner block finishing must not tell the outer one's + // remaining tokens they came from a plain resync. + let outer = self.in_bdd_fallback; + self.in_bdd_fallback = true; self.skip_to_next_top_level(); + self.in_bdd_fallback = outer; } fn parse_invariant_block(&mut self) -> Result { @@ -19342,6 +19386,38 @@ impl Compiler { Ok((ast, parser.dropped_top_level_tokens())) } + /// W699: the discarded tokens with the recovery that threw each away, as + /// `(line, lexeme, channel)`. + /// + /// The channel vector is pushed in lockstep with the spans. If the two + /// lengths ever disagree this REFUSES rather than zipping to the shorter -- + /// see the note at the check. + pub fn parse_ast_dropped_records(source: &str) -> Result, String> { + let lexer = Lexer::new(source); + let mut parser = Parser::new(lexer); + let _ = parser.parse()?; + // W699: `zip` truncates to the shorter side, and that is exactly how a + // missed push site hides. Two sites WERE missed on the first pass -- 27 + // tokens across 27 specs -- and the only reason it surfaced was a total + // that did not match `parse-complete`'s. Refuse instead of truncating. + if parser.dropped_spans.len() != parser.dropped_channels.len() { + return Err(format!( + "drop accounting is inconsistent: {} span(s) but {} channel(s). \ + A recovery site records a span without naming its channel; find \ + it rather than reading the shorter list.", + parser.dropped_spans.len(), + parser.dropped_channels.len() + )); + } + Ok(parser + .dropped_spans + .iter() + .cloned() + .zip(parser.dropped_channels.iter().copied()) + .map(|((l, x), c)| (l, x, c)) + .collect()) + } + /// W634: the discarded tokens themselves, as `(line, lexeme)`. pub fn parse_ast_dropped_spans(source: &str) -> Result, String> { let lexer = Lexer::new(source); diff --git a/bootstrap/src/main.rs b/bootstrap/src/main.rs index 4caae52428..7447138f26 100644 --- a/bootstrap/src/main.rs +++ b/bootstrap/src/main.rs @@ -487,6 +487,15 @@ enum Commands { #[arg(long)] show: Option, + /// W699: group the whole corpus's discard by the token the parser + /// STOPPED ON -- the head of each contiguous dropped run. + /// + /// A ranked list says where the tokens are and a keyword match over the + /// traces guesses why. This asks the record itself: the parser wrote + /// down every token it threw away, and the first one of each run is the + /// construct it could not read. Nothing is inferred. + #[arg(long, default_value_t = false)] + causes: bool, /// Name the top-level items whose removal changes the discard count. /// /// `--show` prints WHAT was dropped; this says WHICH construct the @@ -3937,11 +3946,40 @@ fn run_bisect(path: &str) -> anyhow::Result<()> { Ok(()) } +/// Contiguous runs of dropped tokens, as `(head lexeme, token count)`. +/// +/// A run breaks at a line gap: the spans carry a line but no column, so two +/// dropped regions on the same line are indistinguishable from one, and a blank +/// or surviving line between them is the only separator available. That is a +/// deliberate under-count of runs, never an over-count -- it can merge two +/// causes into one, and cannot invent a cause that is not there. +fn dropped_runs(records: &[(u32, String, &'static str)]) -> Vec<(String, &'static str, usize)> { + let mut runs: Vec<(String, &'static str, usize)> = Vec::new(); + let mut prev: Option<(u32, &'static str)> = None; + for (line, lex, chan) in records { + // A run continues only while BOTH hold: the lines are adjacent and the + // recovery is the same one. Two channels meeting on consecutive lines + // are two findings, and merging them would attribute one's tokens to the + // other's head. + match prev { + Some((p, c)) if *line <= p + 1 && c == *chan => { + if let Some(last) = runs.last_mut() { + last.2 += 1; + } + } + _ => runs.push((lex.clone(), *chan, 1)), + } + prev = Some((*line, *chan)); + } + runs +} + fn run_parse_complete( specs_dir: &str, include_scratch: bool, show: Option<&str>, bisect: Option<&str>, + causes: bool, ) -> anyhow::Result<()> { if let Some(path) = bisect { return run_bisect(path); @@ -3992,6 +4030,75 @@ fn run_parse_complete( } } files.sort(); + + // W699: what the parser STOPPED ON, corpus-wide. + // + // The classification this replaces was a keyword match over the printed + // traces, run from outside the compiler -- it guessed `forall` from the + // presence of the word. This asks the record: the head of each contiguous + // dropped run IS the token recovery began at. `forall` is not the answer it + // gives, and the answer it gives is better. + if causes { + let mut runs_by_head: std::collections::BTreeMap = + std::collections::BTreeMap::new(); + let mut specs_by_head: std::collections::BTreeMap> = + std::collections::BTreeMap::new(); + let mut unread = 0usize; + for f in &files { + let Ok(src) = std::fs::read_to_string(f) else { + unread += 1; + continue; + }; + // A file that does not parse at all has no drop record to read -- + // and it is the `parse` phase's business, not this one. + let Ok(records) = compiler::Compiler::parse_ast_dropped_records(&src) else { + continue; + }; + if records.is_empty() { + continue; + } + for (head, chan, n) in dropped_runs(&records) { + let key = format!("{chan:<19} {head}"); + let e = runs_by_head.entry(key.clone()).or_insert((0, 0)); + e.0 += 1; + e.1 += n; + specs_by_head + .entry(key) + .or_default() + .insert(f.display().to_string()); + } + } + let mut rows: Vec<_> = runs_by_head.iter().collect(); + rows.sort_by(|a, b| b.1 .1.cmp(&a.1 .1).then(a.0.cmp(b.0))); + println!("--- what the parser stopped on ---"); + println!(); + println!(" {:>8} {:>6} {:>6} channel head token", "tokens", "runs", "specs"); + for (head, (runs, toks)) in &rows { + println!( + " {:>8} {:>6} {:>6} {}", + toks, + runs, + specs_by_head[*head].len(), + head + ); + } + println!(); + println!( + " {} distinct head token(s), {} run(s), {} token(s)", + rows.len(), + rows.iter().map(|(_, (r, _))| r).sum::(), + rows.iter().map(|(_, (_, t))| t).sum::() + ); + if unread > 0 { + println!(" {unread} file(s) could not be read -- NOT counted as anything"); + } + println!(); + println!(" A run breaks at a LINE GAP. The spans carry a line and no column, so"); + println!(" two dropped regions on one line read as one: this under-counts runs and"); + println!(" cannot invent a cause that is not there."); + return Ok(()); + } + let (mut ok, mut truncated, mut rejected) = (0usize, 0usize, 0usize); let (mut discarded, mut discarded_tokens) = (0usize, 0usize); for f in &files { @@ -10665,8 +10772,14 @@ async fn main() -> anyhow::Result<()> { } Commands::LexDropped { specs_dir } => run_lex_dropped(&specs_dir)?, Commands::ParseConform => run_parse_conform()?, - Commands::ParseComplete { specs_dir, include_scratch, show, bisect } => { - run_parse_complete(&specs_dir, include_scratch, show.as_deref(), bisect.as_deref())? + Commands::ParseComplete { specs_dir, include_scratch, show, bisect, causes } => { + run_parse_complete( + &specs_dir, + include_scratch, + show.as_deref(), + bisect.as_deref(), + causes, + )? } Commands::CheckCalls { specs_dir, include_scratch } => { run_check_calls(&specs_dir, include_scratch)? @@ -11071,8 +11184,14 @@ fn main() -> anyhow::Result<()> { } Commands::LexDropped { specs_dir } => run_lex_dropped(&specs_dir)?, Commands::ParseConform => run_parse_conform()?, - Commands::ParseComplete { specs_dir, include_scratch, show, bisect } => { - run_parse_complete(&specs_dir, include_scratch, show.as_deref(), bisect.as_deref())? + Commands::ParseComplete { specs_dir, include_scratch, show, bisect, causes } => { + run_parse_complete( + &specs_dir, + include_scratch, + show.as_deref(), + bisect.as_deref(), + causes, + )? } Commands::CheckCalls { specs_dir, include_scratch } => { run_check_calls(&specs_dir, include_scratch)? diff --git a/bootstrap/src/parse_conform.rs b/bootstrap/src/parse_conform.rs index 75ae8c7df5..c4b6bb0b56 100644 --- a/bootstrap/src/parse_conform.rs +++ b/bootstrap/src/parse_conform.rs @@ -231,6 +231,14 @@ version of this is the parse-no-discard suite phase.", discards: Some(0), note: "`setup` is an Ident, so it was read as a CLAUSE HEAD and its argument list as the clause's value; the lowering failed and the whole block fell to the discard, taking the assertion after it. specs/isa/ternary_deque.t27 lost 1873 tokens this way -- and the calls are what SET UP the state the assertions check", }, + Case { + name: "a_fn_spelled_as_a_test_keeps_its_clauses", + input: "module m\n\nfn g(x: u32) -> bool { return x == 0; }\n\n fn plain_test()\n given a = 1\n then g(a) == false\n", + verdict: Verdict::Full, + decls: Some(2), + discards: Some(0), + note: "the arm RECOGNISED this shape by name -- `fn name() given ...` -- and then called skip_to_next_top_level on it, throwing away every clause. The shared clause parser already serves test, invariant and bench; detection is unchanged, only the action is", + }, Case { name: "unterminated_fn_body", input: "module m\n\nfn a() -> u32 { return 1;\n", diff --git a/bootstrap/stage0/FROZEN_HASH b/bootstrap/stage0/FROZEN_HASH index 736b8d5baf..db62cac6c0 100644 --- a/bootstrap/stage0/FROZEN_HASH +++ b/bootstrap/stage0/FROZEN_HASH @@ -1 +1 @@ -3e563db2d411526ac9be21f36434924158ae0d68b271c5b8deac08873fb80886 +976a3c3414a9ffb92f137ee29f20ae1de9e33bbbf05c9d2ef9538bdf90bfd944 diff --git a/cli/tri/src/discard.rs b/cli/tri/src/discard.rs index 5605920a95..f188a1e8ef 100644 --- a/cli/tri/src/discard.rs +++ b/cli/tri/src/discard.rs @@ -29,28 +29,29 @@ pub enum DiscardCmd { #[arg(long, default_value_t = 15)] n: usize, }, - /// Group the discard by what the parser stopped on. + /// Group the discard by which recovery threw it away, and what it stopped on. /// - /// A ranked list says where the tokens are; it does not say whether the top - /// six are six problems or one. They were one: 38 specs and 20 991 of the - /// 30 451 tokens are quantified invariants (`forall x : T ... ==>`), a - /// construct the grammar does not contain (#2774). That is a language - /// decision, not a parser rung, and the ranking alone could not tell. + /// Reads `t27c parse-complete --causes`, which reports the PARSER's own + /// record. The keyword heuristic this replaced guessed `forall` from the + /// presence of the word; the record says 78% of the discard is one channel, + /// a whole braceless block falling back, and that `given` -- the head that + /// named the fn arm fixed in rung 5 -- owed only 43 of its 2 453 tokens to + /// it. Head token and recovery channel are different questions. Classify, } -/// The buckets, in the order they are TESTED -- first match wins, so the more -/// specific pattern must come first. `forall` before `var`, because a quantified -/// invariant's body often declares one too. -/// -/// This is a coarse keyword match over `parse-complete --show` traces, and it -/// says so: `other` is where anything mis-binned lands, and a large `other` is -/// the signal that these buckets have stopped describing the corpus. -const CLASSES: [(&str, &[&str]); 3] = [ - ("forall/==> (quantified)", &["forall", "==>", "== >"]), - ("var/const statement", &["dropped: var ", "dropped: const "]), - ("assert", &["assert"]), -]; +// W699 rung 6: this used to be a keyword match over printed traces, run from +// outside the compiler. It guessed `forall` from the presence of the word. +// +// It no longer guesses. `t27c parse-complete --causes` reports what the PARSER +// recorded: which of five recovery channels threw each token away, and the head +// of each contiguous dropped run. The heuristic said "forall 20 991"; the record +// says 78% of the discard is one channel -- a whole braceless block falling back +// -- and the colon after an invariant name is the largest single head. +// +// The old buckets are gone rather than kept as a cross-check. Two answers to one +// question is what #2767 is about, and a heuristic beside a reading is the same +// shape one level down. fn repo_root() -> Result { let out = std::process::Command::new("git") @@ -131,72 +132,38 @@ fn pinned(root: &std::path::Path) -> Result>> { Ok(map) } -/// The drop trace for one spec, as `t27c parse-complete --show` prints it. -fn drop_trace(root: &std::path::Path, spec: &str) -> Option { +fn classify(root: &std::path::Path) -> Result<()> { let t27c = ["target/release/t27c", "target/debug/t27c"] .iter() .map(|p| root.join(p)) - .find(|p| p.is_file())?; + .find(|p| p.is_file()) + .ok_or_else(|| { + anyhow::anyhow!( + "t27c is not built. `cargo build --release -p t27c` first --\n \ + reporting nothing rather than a classification this run did not earn" + ) + })?; let out = std::process::Command::new(t27c) - .args(["parse-complete", "--show", spec]) + .args(["parse-complete", "--causes"]) .current_dir(root) .output() - .ok()?; - Some(String::from_utf8_lossy(&out.stdout).to_string()) -} - -fn classify(root: &std::path::Path, obs: &BTreeMap) -> Result<()> { - let mut specs: BTreeMap<&str, usize> = BTreeMap::new(); - let mut toks: BTreeMap<&str, usize> = BTreeMap::new(); - let mut unread = 0usize; - for (spec, n) in obs { - let Some(trace) = drop_trace(root, spec) else { - // Not "other". No trace was read, so no cause is claimed. - unread += 1; - continue; - }; - let dropped: String = trace - .lines() - .filter(|l| l.trim_start().starts_with("dropped:")) - .collect::>() - .join("\n"); - let name = CLASSES - .iter() - .find(|(_, pats)| pats.iter().any(|p| dropped.contains(p))) - .map(|(n, _)| *n) - .unwrap_or("other"); - *specs.entry(name).or_default() += 1; - *toks.entry(name).or_default() += n; - } - let mut rows: Vec<_> = toks.iter().collect(); - rows.sort_by(|a, b| b.1.cmp(a.1)); - println!(" {:<26} {:>6} {:>9}", "class", "specs", "tokens"); - for (name, t) in rows { - println!(" {:<26} {:>6} {:>9}", name, specs[*name], t); - } - println!( - " {:<26} {:>6} {:>9}", - "TOTAL", - specs.values().sum::(), - toks.values().sum::() - ); - if unread > 0 { - println!(); - println!(" {unread} spec(s) yielded no trace -- NOT counted as `other`."); + .context("running `t27c parse-complete --causes`")?; + if !out.status.success() { + anyhow::bail!( + "`t27c parse-complete --causes` exited {}. Nothing is claimed.", + out.status + ); } - println!(); - println!(" Coarse keyword match over `parse-complete --show`. A large `other`"); - println!(" means these buckets have stopped describing the corpus, not that"); - println!(" the corpus has stopped having causes."); + print!("{}", String::from_utf8_lossy(&out.stdout)); Ok(()) } pub fn run(cmd: &DiscardCmd) -> Result<()> { let root = repo_root()?; - let obs = observed(&root)?; if matches!(cmd, DiscardCmd::Classify) { - return classify(&root, &obs); + return classify(&root); } + let obs = observed(&root)?; let pin = pinned(&root)?; let DiscardCmd::Top { n } = cmd else { @@ -250,32 +217,6 @@ mod tests { assert_eq!(n, 208); } - /// First match wins, so a quantified invariant whose body also declares a - /// `var` must land in the quantified bucket. Reordering CLASSES silently - /// re-attributes thousands of tokens, which is why the order is tested. - #[test] - fn the_more_specific_class_is_tested_first() { - let trace = "dropped: forall x : T\ndropped: var y = 1 ;"; - let name = super::CLASSES - .iter() - .find(|(_, pats)| pats.iter().any(|p| trace.contains(p))) - .map(|(n, _)| *n) - .unwrap_or("other"); - assert_eq!(name, "forall/==> (quantified)"); - } - - /// `==>` reaches the trace as `== >` because the lexer splits it. A matcher - /// that only looked for `==>` would report zero of the 38 specs. - #[test] - fn the_split_implication_arrow_is_matched() { - let trace = "dropped: input . activations . len == 4 == >"; - let hit = super::CLASSES[0].1.iter().any(|p| trace.contains(p)); - assert!( - hit, - "the lexer splits `==>`; match what the trace actually says" - ); - } - /// A summary line must not be mistaken for a spec row. #[test] fn the_summary_lines_are_not_rows() { diff --git a/docs/now/2026-08-29-ask-the-parser-do-not-grep-what-it-printed.md b/docs/now/2026-08-29-ask-the-parser-do-not-grep-what-it-printed.md new file mode 100644 index 0000000000..55bf265d09 --- /dev/null +++ b/docs/now/2026-08-29-ask-the-parser-do-not-grep-what-it-printed.md @@ -0,0 +1,8 @@ +# NOW -- Ask the parser, do not grep what it printed (2026-08-29) + +## Ask the parser, do not grep what it printed (Refs #2754) + +- every dropped token now carries the recovery that threw it away: bdd-block-fallback 23852 (78%), brace-body 4602, top-level-resync 1894, stray-brace and stmt-recovery the rest +- head token is not channel: given was the 4th-largest head at 2453 tokens and the fn arm that names it owed only 43 of them +- the fn arm recognised by name and called skip_to_next_top_level on it; the shared clause parser already served test/invariant/bench +- zip over two parallel vectors truncated silently and hid two missed push sites -- 27 tokens; the accessor now refuses on a length mismatch diff --git a/docs/reports/suite_expectations.json b/docs/reports/suite_expectations.json index 432d2fc328..ac88cc407c 100644 --- a/docs/reports/suite_expectations.json +++ b/docs/reports/suite_expectations.json @@ -1,7 +1,7 @@ { "schema_version": 1, "generated_by": "t27c suite --bless-expectations", - "max_entries": 178, + "max_entries": 177, "entries": [ { "path": "specs/account/repo.t27", @@ -226,14 +226,6 @@ "issue": 1959, "expires": "2026-11-30" }, - { - "path": "specs/fpga/linker.t27", - "phase": "parse-no-discard", - "reason": "unclassified: blessed by --bless-expectations", - "issue": 1959, - "expires": "2026-11-30", - "discard_tokens": 43 - }, { "path": "specs/fpga/mac.t27", "phase": "parse-no-discard", From 257977160926573d901881c0d68445c40f08b53a Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Sat, 29 Aug 2026 09:47:33 +0700 Subject: [PATCH 2/3] fix(parser): lower a fn-spelled test as a TEST, not as a function 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 --- .trinity/seals/Linker.json | 8 ++++---- .trinity/seals/fpga_Linker.json | 10 +++++----- bootstrap/src/compiler.rs | 19 +++++++++++++++++-- bootstrap/stage0/FROZEN_HASH | 2 +- 4 files changed, 27 insertions(+), 12 deletions(-) diff --git a/.trinity/seals/Linker.json b/.trinity/seals/Linker.json index 5051aea013..2769352ba3 100644 --- a/.trinity/seals/Linker.json +++ b/.trinity/seals/Linker.json @@ -1,8 +1,8 @@ { - "gen_hash_c": "sha256:3375a8f992fd63e359abe881dd254965a5095911df624ab9453b2c21092e5fd4", - "gen_hash_rust": "sha256:838f26e311ccdeb0812827225cf3380f3b26accf47e31f01439425a59032c969", - "gen_hash_verilog": "sha256:4a4cb3732aef18ce3656fa6c56e78950bf849460549cd5db16b5d542d5aaad53", - "gen_hash_zig": "sha256:e3e90b0920d1da9a26f32c58eaafe3c2c1cc77f97afe89278db24838ef3bd684", + "gen_hash_c": "sha256:af9eaaa325e9a0aa0f5fc783a9564b967a852322f1a63f947e02c13d65901948", + "gen_hash_rust": "sha256:e9e1f909a3f8773af1ccf6437cc65ae079945b7a57bde528760f7b5bca288037", + "gen_hash_verilog": "sha256:49b4eed7bfa531a9fa124bee2469bbab58cea99f818f0ee1609444d5a757006c", + "gen_hash_zig": "sha256:f928ec5f281b5df49d58d087284b04604e13c7dafa4c718d1bda8d7ed63a7f41", "module": "Linker", "ring": 12, "sealed_at": "2026-08-28T18:19:55Z", diff --git a/.trinity/seals/fpga_Linker.json b/.trinity/seals/fpga_Linker.json index 6c6f43d1ac..edce6a5f99 100644 --- a/.trinity/seals/fpga_Linker.json +++ b/.trinity/seals/fpga_Linker.json @@ -1,11 +1,11 @@ { - "gen_hash_c": "sha256:3375a8f992fd63e359abe881dd254965a5095911df624ab9453b2c21092e5fd4", - "gen_hash_rust": "sha256:838f26e311ccdeb0812827225cf3380f3b26accf47e31f01439425a59032c969", - "gen_hash_verilog": "sha256:4a4cb3732aef18ce3656fa6c56e78950bf849460549cd5db16b5d542d5aaad53", - "gen_hash_zig": "sha256:e3e90b0920d1da9a26f32c58eaafe3c2c1cc77f97afe89278db24838ef3bd684", + "gen_hash_c": "sha256:af9eaaa325e9a0aa0f5fc783a9564b967a852322f1a63f947e02c13d65901948", + "gen_hash_rust": "sha256:e9e1f909a3f8773af1ccf6437cc65ae079945b7a57bde528760f7b5bca288037", + "gen_hash_verilog": "sha256:49b4eed7bfa531a9fa124bee2469bbab58cea99f818f0ee1609444d5a757006c", + "gen_hash_zig": "sha256:f928ec5f281b5df49d58d087284b04604e13c7dafa4c718d1bda8d7ed63a7f41", "module": "Linker", "ring": 12, - "sealed_at": "2026-08-29T02:18:08Z", + "sealed_at": "2026-08-29T02:47:18Z", "sealed_by": "t27c-bootstrap@0.2.0", "spec_hash": "sha256:64a8091d1c5d8163af7ce400dee2b8ffbe713584045340e1126a0b7560b04c6e", "spec_path": "specs/fpga/linker.t27" diff --git a/bootstrap/src/compiler.rs b/bootstrap/src/compiler.rs index 540e01451d..92b0a6ee3f 100644 --- a/bootstrap/src/compiler.rs +++ b/bootstrap/src/compiler.rs @@ -3029,9 +3029,24 @@ impl Parser { // The column anchor is what the bench path (W905) had to set for the // same reason: continuation statements need an anchor that the head // never established, and without it the statement arms stay dark. + // ... and it is lowered as a TEST, not as a function. + // + // The first attempt kept the FnDecl and filled its body. Every + // backend then treated it as a real function: `gen-verilog` emits + // synthesizable RTL for functions and deliberately does NOT lower + // tests, so the recovered clauses became `\assert (...)` inside a + // task -- "Enable of unknown task ``assert''" -- and the elaboration + // ratchet caught it, linker 4 -> 6. Correctly: a task body cannot + // assert, and a test body must not become one. + // + // `fn name() given ... then ...` IS a test. Emitting a TestBlock + // teaches no backend anything new: each already knows whether it + // lowers tests, and each now does the right thing with this one. + let mut block = Node::new(NodeKind::TestBlock); + block.name = decl.name.clone(); self.bdd_first_col_preset = Some(self.current.col); - self.parse_bdd_clauses(&mut decl); - return Ok(decl); + self.parse_bdd_clauses(&mut block); + return Ok(block); } // Optional arrow for return type: -> Type diff --git a/bootstrap/stage0/FROZEN_HASH b/bootstrap/stage0/FROZEN_HASH index db62cac6c0..54e51dafb0 100644 --- a/bootstrap/stage0/FROZEN_HASH +++ b/bootstrap/stage0/FROZEN_HASH @@ -1 +1 @@ -976a3c3414a9ffb92f137ee29f20ae1de9e33bbbf05c9d2ef9538bdf90bfd944 +fcfb279c055ccb603ec8eea758053347198a27ce01baa7d6c5240a961d7af697 From 434cfe6bbc141577e428d8e92daa3cd1248892b2 Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Sat, 29 Aug 2026 09:47:58 +0700 Subject: [PATCH 3/3] docs(skill): the gate's flags are part of the gate (165-166) 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 --- .claude/skills/ci-gates/SKILL.md | 30 +++++++++++++++++++ ...atchet-was-right-and-my-ruler-was-wrong.md | 7 +++++ 2 files changed, 37 insertions(+) create mode 100644 docs/now/2026-08-29-the-elaboration-ratchet-was-right-and-my-ruler-was-wrong.md diff --git a/.claude/skills/ci-gates/SKILL.md b/.claude/skills/ci-gates/SKILL.md index 423b6b60ee..c83c228770 100644 --- a/.claude/skills/ci-gates/SKILL.md +++ b/.claude/skills/ci-gates/SKILL.md @@ -5789,3 +5789,33 @@ well enough to special-case it and stopped one line short of lowering it. **A comment that names a construct beside a `skip` is a fix that was scoped and not finished.** Grep for that pair: recognition followed by discard is a different and better-signposted target than an unhandled shape nobody has looked at. + +## 165. Same file, two flag sets, opposite verdicts + +The elaboration ratchet said my change took `linker` from 4 errors to 6. I ran +iverilog on the same generated file and counted **fewer** errors than master. + +The gate runs `iverilog -g2012 -DSIMULATION`; I had run bare `iverilog`. Under +the default the file is Verilog-2005, where every size cast is an error and +master's *empty task* trips "Task body with no statements" — so master looked +worse. Under `-g2012` both of those are legal, the size casts vanish, and what +remains is the two errors my change actually added. + +**Copy the gate's invocation, flags included, out of its source.** A tool with +the right name and the wrong flags is a different tool, and it will happily +disagree with the gate about the same file. + +## 166. If a backend refuses to lower a construct, produce that construct + +A `fn` whose body is BDD clauses is a test spelled as a function. My first fix +kept it a `FnDecl` and filled the body, so `gen-verilog` — which emits RTL for +functions and deliberately does **not** lower tests — produced `\assert (…)` +inside a task and an assignment to the task's own name. + +The fix was not to teach the Verilog backend about a new fn flavour. It was to +emit a `TestBlock`, because that is what the source means. Every backend already +knows whether it lowers tests. + +**When recovered content lands in the wrong node kind, change the node, not the +four consumers.** The give-away is a fix that would need a matching change in +every backend: that is usually the parser choosing the wrong shape. diff --git a/docs/now/2026-08-29-the-elaboration-ratchet-was-right-and-my-ruler-was-wrong.md b/docs/now/2026-08-29-the-elaboration-ratchet-was-right-and-my-ruler-was-wrong.md new file mode 100644 index 0000000000..c441a241fe --- /dev/null +++ b/docs/now/2026-08-29-the-elaboration-ratchet-was-right-and-my-ruler-was-wrong.md @@ -0,0 +1,7 @@ +# NOW -- The elaboration ratchet was right and my ruler was wrong (2026-08-29) + +## The elaboration ratchet was right and my ruler was wrong (Refs #2754) + +- keeping the FnDecl made gen-verilog emit assert inside a task; a fn spelled as a test now parses to a TestBlock and every backend already knows what that is +- I measured with bare iverilog while the gate runs -g2012 -DSIMULATION: two rulers, opposite verdicts about the same file +- elaboration errors back to 176 = baseline, discard unchanged at 30408