diff --git a/.claude/skills/ci-gates/SKILL.md b/.claude/skills/ci-gates/SKILL.md index b95dff70fc..4f50d2edab 100644 --- a/.claude/skills/ci-gates/SKILL.md +++ b/.claude/skills/ci-gates/SKILL.md @@ -5913,3 +5913,48 @@ assertions now actually run. **Do not read that column falling as damage without opening each spec.** One was a real false property, two were shape complaints, and five other specs went the other way once the backend defects they exposed were fixed (cc 158 → 163). + +## 173. The code often names the shape it fails on — grep your own comments + +Two rungs this pass were shapes the parser had already described in prose and +never handled: + + // it can also mean we stopped mid-clause -- e.g. on the comma of + // `given clk = true, rst_n = false` + +That comment sits at the top of the loop that then discards exactly that. 19 +fallback events in one spec. The other, `given crossings: [i32] = []`, is the +same story one arm down. + +Together with the `fn name() given …` arm from an earlier pass and the `forall` +arm, that is **four** defects in one file where somebody understood the shape +well enough to write it down and stopped short of lowering it. + +**A comment naming a construct next to a `skip`, a `return`, or a fallback is a +scoped-and-abandoned fix.** It is a better-signposted target than any census, +and `grep` finds it in seconds. + +## 174. "Someone who knows the domain" was me, one script later + +I filed a failing assertion saying it needed *"someone who knows the intended +encoding"*. Both functions were in the same file. Transcribing them to twelve +lines of Python answered it completely: the encoder is balanced ternary, the +decoder is unipolar, they are not inverses, and 8 of 16 values fail. + +It also found a second bug the first one hid — with the correct inverse, three +balanced trits span −13..13, so the test's `i < 16` bound walks past the +encodable range regardless. + +**Before deferring a question to a human, check whether the artefact answers +it.** Deferring is right when the question is a *decision* (which encoding is +intended — still open). It was wrong for the part that was arithmetic. + +## 175. A census that names a target you cannot open stops one step short + +`--fallbacks` reported *19 events in 1 spec* and could not say which spec. I +brute-forced it by looping the whole corpus through a per-file command. + +The fix was ten lines: let the census take `--show ` and scope to one file. +**Any aggregate you build should have a per-item mode from the start** — you will +need it the first time the aggregate says something interesting, which is +immediately. diff --git a/.trinity/seals/ISAMemoryOps.json b/.trinity/seals/ISAMemoryOps.json index 85ee24c985..f54247da33 100644 --- a/.trinity/seals/ISAMemoryOps.json +++ b/.trinity/seals/ISAMemoryOps.json @@ -1,8 +1,8 @@ { - "gen_hash_c": "sha256:67a78d90bb7cb889f3e6c037fdcba78b75f7f419c191a3afa519a844a02c24b5", + "gen_hash_c": "sha256:f774cae150e65db765a73b61432e809285899aec07634c5b582ef73400b2721b", "gen_hash_rust": "sha256:08c0a5537152d0d7f2eae51a2a8b78932821460d3d6cf6d61d376570235db239", "gen_hash_verilog": "sha256:0dccef9c3c538ea2399276395a58aaa116f002a42e4180c75d46756cb9f56e0b", - "gen_hash_zig": "sha256:1d2982e1cbc4e526ff2ff1d64481c96a956ac9abffabd6b292b4a6d4a623d76b", + "gen_hash_zig": "sha256:4c2cc4e686186bdd7bd495cd473f11fbba6c71820488fd68cf9f49955183dc3b", "module": "ISAMemoryOps", "ring": 12, "sealed_at": "2026-08-28T00:21:37Z", diff --git a/.trinity/seals/JonesPolynomial.json b/.trinity/seals/JonesPolynomial.json index 3ac3825c0d..12bd756132 100644 --- a/.trinity/seals/JonesPolynomial.json +++ b/.trinity/seals/JonesPolynomial.json @@ -1,8 +1,8 @@ { - "gen_hash_c": "sha256:f35215644bc1fb1fac23407da26ff08b4e562f0a0cb5218fe773451a401f6df1", + "gen_hash_c": "sha256:c286be618ed78366c1df1dd44cb15c1e6fd57fa37bf557b03be11b0bb8f854af", "gen_hash_rust": "sha256:2dd52a6bc47b88e5ea49fff38bbe9937fa3b3e87e8d104e6314091c94d3e1d3f", "gen_hash_verilog": "sha256:644d8c5309231400b435250fd966219bd5b5b28c9ae8732a5a48884088072fa0", - "gen_hash_zig": "sha256:d8f4fb82c1461dc3a500e0e895bb8a4b196fb33b1d3e0136834b8fdaf535b76a", + "gen_hash_zig": "sha256:1c78dfad02821454197755756ccc61755626a4f901350aa8be5c14395c06fef3", "module": "JonesPolynomial", "ring": 12, "sealed_at": "2026-08-28T00:21:37Z", diff --git a/.trinity/seals/TernaryControlFlow.json b/.trinity/seals/TernaryControlFlow.json index a8e00c6f6e..80e1a91bbe 100644 --- a/.trinity/seals/TernaryControlFlow.json +++ b/.trinity/seals/TernaryControlFlow.json @@ -1,8 +1,8 @@ { - "gen_hash_c": "sha256:04fe0bc679daacc52a3601b2a337fc098780585ec0944e8802706bf277f3df05", + "gen_hash_c": "sha256:d042f8bfaaef6bd86b05d080a61c1fd89f196b8bb1d7ef58aa1069dfea7bbe8f", "gen_hash_rust": "sha256:0b6a37615eadf1a45b07eaeb4f7dcad3e209605e93a695287bf0ca414c25bbbe", "gen_hash_verilog": "sha256:c4e7373882bf56f5fc546a7d03ee7de41e6fa7b4a91b87cbe8fc03be6ba5604e", - "gen_hash_zig": "sha256:51ff256df040056f4e700416f2b25a9ceb3bb150b0e06c0df7e4219eed408c28", + "gen_hash_zig": "sha256:b8c7be6f8bd788eb6fa8642a2dcc7d76ce34a7e1003d6dce4626a0f1e65b897b", "module": "TernaryControlFlow", "ring": 12, "sealed_at": "2026-08-28T00:21:37Z", diff --git a/.trinity/seals/isa_ISAMemoryOps.json b/.trinity/seals/isa_ISAMemoryOps.json index 6209f987a0..2ac3481bca 100644 --- a/.trinity/seals/isa_ISAMemoryOps.json +++ b/.trinity/seals/isa_ISAMemoryOps.json @@ -1,11 +1,11 @@ { - "gen_hash_c": "sha256:67a78d90bb7cb889f3e6c037fdcba78b75f7f419c191a3afa519a844a02c24b5", + "gen_hash_c": "sha256:f774cae150e65db765a73b61432e809285899aec07634c5b582ef73400b2721b", "gen_hash_rust": "sha256:08c0a5537152d0d7f2eae51a2a8b78932821460d3d6cf6d61d376570235db239", "gen_hash_verilog": "sha256:0dccef9c3c538ea2399276395a58aaa116f002a42e4180c75d46756cb9f56e0b", - "gen_hash_zig": "sha256:1d2982e1cbc4e526ff2ff1d64481c96a956ac9abffabd6b292b4a6d4a623d76b", + "gen_hash_zig": "sha256:4c2cc4e686186bdd7bd495cd473f11fbba6c71820488fd68cf9f49955183dc3b", "module": "ISAMemoryOps", "ring": 12, - "sealed_at": "2026-08-29T04:11:28Z", + "sealed_at": "2026-08-29T04:46:46Z", "sealed_by": "t27c-bootstrap@0.2.0", "spec_hash": "sha256:29ad72599016b8ced9266c0cce3604e11222c3e7d569768312df89903088cff3", "spec_path": "specs/isa/ternary_memory.t27" diff --git a/.trinity/seals/isa_TernaryControlFlow.json b/.trinity/seals/isa_TernaryControlFlow.json index a2e96db9f9..9643553aa3 100644 --- a/.trinity/seals/isa_TernaryControlFlow.json +++ b/.trinity/seals/isa_TernaryControlFlow.json @@ -1,11 +1,11 @@ { - "gen_hash_c": "sha256:04fe0bc679daacc52a3601b2a337fc098780585ec0944e8802706bf277f3df05", + "gen_hash_c": "sha256:d042f8bfaaef6bd86b05d080a61c1fd89f196b8bb1d7ef58aa1069dfea7bbe8f", "gen_hash_rust": "sha256:0b6a37615eadf1a45b07eaeb4f7dcad3e209605e93a695287bf0ca414c25bbbe", "gen_hash_verilog": "sha256:c4e7373882bf56f5fc546a7d03ee7de41e6fa7b4a91b87cbe8fc03be6ba5604e", - "gen_hash_zig": "sha256:51ff256df040056f4e700416f2b25a9ceb3bb150b0e06c0df7e4219eed408c28", + "gen_hash_zig": "sha256:b8c7be6f8bd788eb6fa8642a2dcc7d76ce34a7e1003d6dce4626a0f1e65b897b", "module": "TernaryControlFlow", "ring": 12, - "sealed_at": "2026-08-29T04:11:28Z", + "sealed_at": "2026-08-29T04:46:46Z", "sealed_by": "t27c-bootstrap@0.2.0", "spec_hash": "sha256:dcb5de4bdcaaac334bf386d0ee8c2badc68a3debababb033eb4a6df16ff6d6ad", "spec_path": "specs/isa/ternary_control_flow.t27" diff --git a/.trinity/seals/race_igla-race-cordic-top.json b/.trinity/seals/race_igla-race-cordic-top.json index 2ac3f207d1..f84ff8a83a 100644 --- a/.trinity/seals/race_igla-race-cordic-top.json +++ b/.trinity/seals/race_igla-race-cordic-top.json @@ -1,11 +1,11 @@ { - "gen_hash_c": "sha256:e61cc48184e5754d9544ae52a3c8ed5dec066333639c883bc5463b29759cb46a", + "gen_hash_c": "sha256:ef4f41400ff2f064d61513da02965b70373c2a9df16238155299ca1e726fd161", "gen_hash_rust": "sha256:c643445e277d654e432068eea6e9958ccc45b6e394603376c38e3791e8d7c097", "gen_hash_verilog": "sha256:4cbfacb005043739944c0fa4ca55fe2f648875c771cb94a9c35e338b9e5eb610", - "gen_hash_zig": "sha256:031aa59dda7f6804f13883a661052427ffd3eee7b8d64c7dd89728d8201823d7", + "gen_hash_zig": "sha256:5afe1ae2b906f855f5cbddf6337351d42c81132d32851f36ffa2c74791a8dd23", "module": "igla-race-cordic-top", "ring": 12, - "sealed_at": "2026-08-29T01:19:56Z", + "sealed_at": "2026-08-29T04:46:46Z", "sealed_by": "t27c-bootstrap@0.2.0", "spec_hash": "sha256:ef4e2d3e90d9a3b29abb9254cd70e3dd011a566eb73155b4efb7fa340a7db6b8", "spec_path": "specs/igla/race/cordic_top.t27" diff --git a/.trinity/seals/vsa_JonesPolynomial.json b/.trinity/seals/vsa_JonesPolynomial.json index dbb43dd000..a5c9b73878 100644 --- a/.trinity/seals/vsa_JonesPolynomial.json +++ b/.trinity/seals/vsa_JonesPolynomial.json @@ -1,11 +1,11 @@ { - "gen_hash_c": "sha256:f35215644bc1fb1fac23407da26ff08b4e562f0a0cb5218fe773451a401f6df1", + "gen_hash_c": "sha256:c286be618ed78366c1df1dd44cb15c1e6fd57fa37bf557b03be11b0bb8f854af", "gen_hash_rust": "sha256:2dd52a6bc47b88e5ea49fff38bbe9937fa3b3e87e8d104e6314091c94d3e1d3f", "gen_hash_verilog": "sha256:644d8c5309231400b435250fd966219bd5b5b28c9ae8732a5a48884088072fa0", - "gen_hash_zig": "sha256:d8f4fb82c1461dc3a500e0e895bb8a4b196fb33b1d3e0136834b8fdaf535b76a", + "gen_hash_zig": "sha256:1c78dfad02821454197755756ccc61755626a4f901350aa8be5c14395c06fef3", "module": "JonesPolynomial", "ring": 12, - "sealed_at": "2026-08-28T23:38:44Z", + "sealed_at": "2026-08-29T04:46:46Z", "sealed_by": "t27c-bootstrap@0.2.0", "spec_hash": "sha256:b1ff39e967bed28b4fd7033a0368f00b9a8b395d16dc4d7b62759e27feab3834", "spec_path": "specs/vsa/jones_polynomial.t27" diff --git a/bootstrap/src/compiler.rs b/bootstrap/src/compiler.rs index 0f8f4f81e8..d462cdfc26 100644 --- a/bootstrap/src/compiler.rs +++ b/bootstrap/src/compiler.rs @@ -6396,6 +6396,29 @@ impl Parser { let bind_look = self.save_state(); let name = self.current.lexeme.clone(); self.advance(); + // W699 rung 11: a TYPED binding. + // + // given crossings: [i32] = [] + // + // The arm below peeks for `=` immediately after the name, so + // an annotation between them read as "not a binding" and the + // clause -- and its whole block -- went to the discard. 17 + // fallback events across 4 specs, all of them `given`. + // + // The type is parsed and kept on the declaration, the way + // `var x : T = v` already does in the statement arm. If no `=` + // follows the annotation this restores and changes nothing. + let mut typed = String::new(); + if self.current.kind == TokenKind::Colon { + let ty_look = self.save_state(); + self.advance(); // : + let ty = self.parse_type_annotation(); + if self.current.kind == TokenKind::Equals && !ty.is_empty() { + typed = ty; + } else { + self.restore_state(ty_look); + } + } if self.current.kind != TokenKind::Equals { self.restore_state(bind_look); // W906 (0013): a DOTTED/INDEXED LVALUE step -- @@ -6496,7 +6519,55 @@ impl Parser { } decl.extra_field = tail; } + decl.extra_type = typed.clone(); block.children.push(decl); + // W699 rung 10: COMMA-SEPARATED bindings in one + // clause. + // + // given clk = true, rst_n = false, angle = 4096 + // + // The loop's own comment at the top of this + // function names the shape -- "it can also mean we + // stopped mid-clause -- e.g. on the comma of + // `given clk = true, rst_n = false`" -- and nothing + // ever acted on it. 19 fallback events in + // specs/igla/race/cordic_top.t27 alone, each one + // taking a whole block of clauses with it. + // + // Same line only: a comma opening the next line is + // somebody else's punctuation. Anything this cannot + // read restores to the comma and leaves the clause + // as it stands, so a partial list still lowers what + // it understood. + while self.current.kind == TokenKind::Comma + && self.current.line == self.last_line + && self.peek.kind == TokenKind::Ident + { + let cm = self.save_state(); + self.advance(); // , + let n2 = self.current.lexeme.clone(); + self.advance(); // name + if self.current.kind != TokenKind::Equals { + self.restore_state(cm); + break; + } + self.advance(); // = + self.in_bdd_clause_value = true; + let r2 = self.parse_expr(); + self.in_bdd_clause_value = false; + match r2 { + Ok(e2) => { + let mut d2 = Node::new(NodeKind::StmtLocal); + d2.name = n2; + d2.children.push(e2); + block.children.push(d2); + } + Err(_) => { + self.restore_state(cm); + break; + } + } + } true } Err(_) => false, diff --git a/bootstrap/src/main.rs b/bootstrap/src/main.rs index f1c93017e4..483dc9537b 100644 --- a/bootstrap/src/main.rs +++ b/bootstrap/src/main.rs @@ -3992,6 +3992,29 @@ fn run_parse_complete( if let Some(path) = bisect { return run_bisect(path); } + // W699: `--fallbacks --show ` scopes the census to one file. + // + // The corpus view says a shape exists 19 times in 1 spec and cannot say + // WHICH -- and a census that names a target you then cannot open is an + // instrument that stops one step short. + if let Some(path) = show { + let src = std::fs::read_to_string(path)?; + let events = compiler::Compiler::parse_ast_bdd_fallbacks(&src) + .map_err(|e| anyhow::anyhow!("{} does not parse: {}", path, e))?; + if events.is_empty() { + println!("{}: no whole-block fallback", path); + return Ok(()); + } + let lines: Vec<&str> = src.lines().collect(); + println!("{}: {} whole-block fallback(s)", path, events.len()); + println!(); + for (line, why, clause) in &events { + let text = lines.get((*line as usize).saturating_sub(1)).unwrap_or(&""); + println!(" {:5}| {}", line, text.trim_end()); + println!(" {why} (on `{clause}`)"); + } + return Ok(()); + } // W634: single-file mode -- print what was discarded, grouped by line, so a // human can decide whether any of it is content a theorem depends on. if let Some(path) = show { diff --git a/bootstrap/src/parse_conform.rs b/bootstrap/src/parse_conform.rs index 9f2dc83639..41d353cceb 100644 --- a/bootstrap/src/parse_conform.rs +++ b/bootstrap/src/parse_conform.rs @@ -247,6 +247,22 @@ version of this is the parse-no-discard suite phase.", discards: Some(0), note: "`for` and `while` are keywords, so they are neither a clause head nor a block boundary and the loop fell through to the whole-block fallback -- taking the assertion after it. 110 fallback events across ~25 specs, the largest non-`forall` shape in the distribution", }, + Case { + name: "one_clause_may_bind_several_names", + input: "module m\n\n test t\n given clk = true, rst_n = false, angle = 4096\n then clk == true\n", + verdict: Verdict::Full, + decls: Some(1), + discards: Some(0), + note: "the loop's own comment named this shape -- `given clk = true, rst_n = false` -- as the reason a block can stop mid-clause, and nothing acted on it. 19 fallback events in one spec, each taking a whole block of clauses with it", + }, + Case { + name: "a_clause_binding_may_carry_a_type", + input: "module m\n\n test t\n given crossings : [i32] = [1]\n then crossings[0] == 1\n", + verdict: Verdict::Full, + decls: Some(1), + discards: Some(0), + note: "the binding arm peeked for `=` immediately after the name, so an annotation between them read as `not a binding` and the whole block went to the discard", + }, 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 a9c010b0e9..5baa2ea2e0 100644 --- a/bootstrap/stage0/FROZEN_HASH +++ b/bootstrap/stage0/FROZEN_HASH @@ -1 +1 @@ -03cdabb2b2439bb0d3308c94eeecccfad17e45d954659a9612b368900109dff2 +347e84842d907365acafa9edcd4384f1d2d202e381d0babaafb272a690f46d51 diff --git a/docs/now/2026-08-29-the-long-tail-and-two-shapes-the-code-had-already-named.md b/docs/now/2026-08-29-the-long-tail-and-two-shapes-the-code-had-already-named.md new file mode 100644 index 0000000000..246cb1fca1 --- /dev/null +++ b/docs/now/2026-08-29-the-long-tail-and-two-shapes-the-code-had-already-named.md @@ -0,0 +1,8 @@ +# NOW -- The long tail, and two shapes the code had already named (2026-08-29) + +## The long tail, and two shapes the code had already named (Refs #2754) + +- given clk = true, rst_n = false: the loop's own comment names comma-separated bindings as a reason to stop mid-clause, and nothing acted on it -- 19 events in one spec +- given crossings : [i32] = []: the arm peeked for = immediately after the name, so an annotation between them read as not-a-binding +- 25093 -> 23926 tokens, 77 -> 76 specs, and not one acceptance column moved: zero rows differ across 650 specs +- --fallbacks --show scopes the census to one file; a census that names a target you cannot then open stops one step short diff --git a/docs/reports/suite_expectations.json b/docs/reports/suite_expectations.json index 44894dc1ee..98200434a8 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": 168, + "max_entries": 167, "entries": [ { "path": "specs/account/repo.t27", @@ -612,9 +612,9 @@ "reason": "top-level drop-recovery discards tokens; parser reaches EOF so `parse` reports success (T42)", "issue": 1959, "expires": "2026-11-30", - "discard_tokens": 1238, + "discard_tokens": 499, "discard_by_channel": { - "bdd-block-fallback": 1237, + "bdd-block-fallback": 498, "stray-brace": 1 } }, @@ -835,17 +835,6 @@ "brace-body/in-fallback": 21 } }, - { - "path": "specs/isa/ternary_control_flow.t27", - "phase": "parse-no-discard", - "reason": "top-level drop-recovery discards tokens; parser reaches EOF so `parse` reports success (T42)", - "issue": 1959, - "expires": "2026-11-30", - "discard_tokens": 30, - "discard_by_channel": { - "bdd-block-fallback": 30 - } - }, { "path": "specs/isa/ternary_encoding.t27", "phase": "parse", @@ -871,10 +860,10 @@ "reason": "top-level drop-recovery discards tokens; parser reaches EOF so `parse` reports success (T42)", "issue": 1959, "expires": "2026-11-30", - "discard_tokens": 211, + "discard_tokens": 46, "discard_by_channel": { - "bdd-block-fallback": 128, - "brace-body/in-fallback": 83 + "bdd-block-fallback": 12, + "brace-body/in-fallback": 34 } }, { @@ -1525,9 +1514,9 @@ "reason": "parser reaches EOF but DISCARDS top-level tokens (forall-quantified properties)", "issue": 2474, "expires": "2026-11-30", - "discard_tokens": 302, + "discard_tokens": 69, "discard_by_channel": { - "bdd-block-fallback": 289, + "bdd-block-fallback": 56, "brace-body/in-fallback": 4, "top-level-resync": 9 }