Five parser and instrument defects, and the 73 Lean disagreements that were reporting as 1

.trinity/seals/ar_asp_solver.json

@@ -1,11 +1,11 @@
 {
-  "gen_hash_c": "sha256:bc789553d5845fb5da7807fabe1214b11021e40db3f72b4aee6faa0363bc6e05",
-  "gen_hash_rust": "sha256:9af8ab0e0f9536780c8cde8387397307e51e26d097967b7cd7e2ffe26cb457fa",
-  "gen_hash_verilog": "sha256:a0f029e4f435a3996a91b60b3f0e7632c510e1d368462aacbc3c652b9eba0d56",
-  "gen_hash_zig": "sha256:99ee47f25bbf868e6b16ee35611140805c5dbc1b06117722c37fc1a02fe685a3",
+  "gen_hash_c": "sha256:55419456ce808ff3f0baed2af64640584c30707bc1eaa6bc2eddc6be380a7ddc",
+  "gen_hash_rust": "sha256:1c6115d02a60911a8ae8ee86cd4e1047ea4cad9711c3466c8edb4ef9fb849d4f",
+  "gen_hash_verilog": "sha256:4a3aac88230f26e414bd206d0168d8063b891db31ae52d7ed63c02186a0d6944",
+  "gen_hash_zig": "sha256:78ef736ad5e3b4d39fc1ff3bcfe0accebcbc0fd090b10fb4941e32e6f6c3cb25",
   "module": "asp_solver",
   "ring": 12,
-  "sealed_at": "2026-08-06T15:25:18Z",
-  "spec_hash": "sha256:cb61281176bafb99fd47a406941d7f224280dbfc0c0e255c3f0afb9dd6ce3976",
+  "sealed_at": "2026-08-27T22:18:39Z",
+  "spec_hash": "sha256:eca06ff812c61e2693f706b7389c71dcd769c30dfbb2cfb958e0416a5118b404",
   "spec_path": "specs/ar/asp_solver.t27"
-}
+}

.trinity/seals/asp_solver.json

@@ -1,11 +1,11 @@
 {
-  "gen_hash_c": "sha256:bc789553d5845fb5da7807fabe1214b11021e40db3f72b4aee6faa0363bc6e05",
-  "gen_hash_rust": "sha256:9af8ab0e0f9536780c8cde8387397307e51e26d097967b7cd7e2ffe26cb457fa",
-  "gen_hash_verilog": "sha256:57879a0b67f4f4bb6f5aff75a64ad10470da429b9eefbbafcce5d7982d47d7a4",
-  "gen_hash_zig": "sha256:99ee47f25bbf868e6b16ee35611140805c5dbc1b06117722c37fc1a02fe685a3",
+  "gen_hash_c": "sha256:55419456ce808ff3f0baed2af64640584c30707bc1eaa6bc2eddc6be380a7ddc",
+  "gen_hash_rust": "sha256:1c6115d02a60911a8ae8ee86cd4e1047ea4cad9711c3466c8edb4ef9fb849d4f",
+  "gen_hash_verilog": "sha256:4a3aac88230f26e414bd206d0168d8063b891db31ae52d7ed63c02186a0d6944",
+  "gen_hash_zig": "sha256:78ef736ad5e3b4d39fc1ff3bcfe0accebcbc0fd090b10fb4941e32e6f6c3cb25",
   "module": "asp_solver",
   "ring": 12,
-  "sealed_at": "2026-05-18T04:24:38Z",
-  "spec_hash": "sha256:cb61281176bafb99fd47a406941d7f224280dbfc0c0e255c3f0afb9dd6ce3976",
+  "sealed_at": "2026-08-27T22:18:39Z",
+  "spec_hash": "sha256:eca06ff812c61e2693f706b7389c71dcd769c30dfbb2cfb958e0416a5118b404",
   "spec_path": "specs/ar/asp_solver.t27"
-}
+}

CHANGELOG.md

@@ -7,6 +7,42 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+### Parser and instruments, W699 (2026-08-28)
+
+#### Fixed
+- **A leading `(` was taken as proof of a parenthesised condition.**
+  `if (i >> j) & 1 == 1 {` read `(i >> j)` as the whole condition and died at the
+  brace. Three byte-identical copies of that code stood in `parse_if_stmt`,
+  `parse_while_stmt` and `parse_if_expr`; they are now one `parse_condition`.
+  Corpus specs parsing: **558 -> 559**.
+- **`specs/ar/asp_solver.t27:369`** opened a list and never closed it, so the
+  parser ran to EOF looking for `]` — a typo in the spec that cost 186 lines.
+- **Zig builtins leaked into generated Rust.** `gen-rust` passed `@as`,
+  `@intCast`, `@min`, `@sqrt`, `@rem`, `@intFromEnum` through verbatim. They are
+  translated now. The earlier claim that these were *the* reason 43 specs do not
+  compile is withdrawn: rustc reports 499 distinct error classes and the builtins
+  account for 40 errors; the largest class is 688 occurrences of a missing
+  `serde`.
+- **A test body may open with `var`**, and `const (a, b) = f()` is a statement.
+
+#### Changed
+- **The Rust/Lean completeness test reported 1 disagreement out of 73.** It
+  asserted agreement one spec at a time and aborted on the first. It now collects
+  all of them into `docs/reports/lean_completeness_mismatches.json`, an
+  identity-keyed ledger that moves down only. **40 of the 73 are theorems about
+  an EMPTY module** — `native_decide` proving that nothing is lowerable. The
+  ledger makes the number visible and monotonic; it does not repair it.
+- **A conformance case can now demand "accepted, and nothing dropped".**
+  `Case` gains `discards`, so `stray_closing_brace` asserts Full with 2 decls and
+  exactly 1 discarded instead of demanding a rejection that would have thrown
+  `fn b` away. Suite: **1629 passed / 6 failed -> 1630 passed / 5 failed**.
+
+#### Removed
+- Two guards that had been unreachable behind the early abort: `specs/scratch`
+  envs (untracked since #2283) counted as Lean-only witnesses, and a `>= 245`
+  floor that a deliberate skip could walk under. The floor now holds on
+  `checked + skipped`.
+
 ### FPGA — measured, W746-W761 (2026-08-14/15)
 
 #### Added

bootstrap/src/compiler.rs

@@ -1857,6 +1857,15 @@ impl Parser {
         }
 
         match self.current.kind {
+            // `const (a, b) = f();` is the tuple-destructure STATEMENT, and the
+            // corpus writes it inside test bodies. When a braceless block stops
+            // on one, the parser hands it here, where `parse_const_decl`
+            // demands a name and dies with "Expected identifier after 'const',
+            // got LParen" -- a hard error on a form the statement parser has
+            // handled all along. Route it to the parser that knows it.
+            TokenKind::KwConst if self.peek.kind == TokenKind::LParen => {
+                self.parse_let_destructuring()
+            }
             TokenKind::KwConst => self.parse_const_decl(is_pub),
             TokenKind::KwVar => self.parse_var_decl(is_pub),
             TokenKind::KwFn => self.parse_fn_decl(is_pub),
@@ -3736,6 +3745,51 @@ impl Parser {
     }
 
     /// Parse if / else if / else statement
+    /// The condition of an `if`, a `while`, or an `if` expression.
+    ///
+    /// `body_follows` says whether a `{` block must come next. It is false for
+    /// the `if` EXPRESSION, whose then-branch is an expression: `if (c) a else
+    /// b` is legitimate and the paren really does close the condition there.
+    /// Rewinding in that context re-read `(c) a` as one expression and killed
+    /// six specs -- ops, ternary_add, types, gf16, gfternary, tf3 -- which a
+    /// before/after parse of the whole corpus caught and the green test did
+    /// not.
+    ///
+    /// Three byte-identical copies of this stood in the parser and all three
+    /// carried the same defect, so the fix lives in one place.
+    ///
+    /// A leading `(` is NOT proof of the parenthesised form: it may be the
+    /// first factor of a bare condition, as in `if (i >> j) & 1 == 1 {`
+    /// (specs/ar/asp_solver.t27:154). Reading `(i >> j)` as the whole
+    /// condition leaves `& 1 == 1` sitting where the body belongs, and the
+    /// enclosing function dies at the brace -- which is how one real spec
+    /// stopped parsing while a Lean theorem went on asserting it lowerable.
+    ///
+    /// The two forms are told apart by what FOLLOWS the closing paren: the
+    /// body `{`, or a payload capture `|x|`. Anything else means the
+    /// condition continued, so the checkpoint rewinds and the bare path
+    /// re-reads it whole. Without parentheses, `Name {` would open the BODY,
+    /// so struct-literal parsing is suppressed there.
+    fn parse_condition(&mut self, body_follows: bool) -> Result<Node, String> {
+        if self.current.kind == TokenKind::LParen {
+            let checkpoint = self.save_state();
+            self.advance();
+            let c = self.parse_expr()?;
+            self.expect(TokenKind::RParen)?;
+            if !body_follows
+                || self.current.kind == TokenKind::LBrace
+                || self.current.kind == TokenKind::Pipe
+            {
+                return Ok(c);
+            }
+            self.restore_state(checkpoint);
+        }
+        self.no_struct_literal += 1;
+        let c = self.parse_expr();
+        self.no_struct_literal -= 1;
+        c
+    }
+
     fn parse_if_stmt(&mut self) -> Result<Node, String> {
         let mut if_node = Node::new(NodeKind::StmtIf);
         self.advance(); // consume 'if'
@@ -3744,17 +3798,7 @@ impl Parser {
         // `if cond { ... }` and it was "Expected LParen, got Ident" -- 1,002
         // assertion clauses (W578). Without parentheses, `Name {` opens the
         // BODY, so struct-literal parsing is suppressed for the condition.
-        let cond = if self.current.kind == TokenKind::LParen {
-            self.advance();
-            let c = self.parse_expr()?;
-            self.expect(TokenKind::RParen)?;
-            c
-        } else {
-            self.no_struct_literal += 1;
-            let c = self.parse_expr();
-            self.no_struct_literal -= 1;
-            c?
-        };
+        let cond = self.parse_condition(true)?;
         if_node.children.push(cond);
 
         // PAYLOAD CAPTURE: `if (opt) |value| { ... }` -- Zig's optional
@@ -3851,17 +3895,7 @@ impl Parser {
         // (W578). `while e > 0 {` is the Rust form and 22 specs use it. Without
         // parentheses a `Name {` opens the BODY, so struct-literal parsing is
         // suppressed while reading the condition.
-        let cond = if self.current.kind == TokenKind::LParen {
-            self.advance();
-            let c = self.parse_expr()?;
-            self.expect(TokenKind::RParen)?;
-            c
-        } else {
-            self.no_struct_literal += 1;
-            let c = self.parse_expr();
-            self.no_struct_literal -= 1;
-            c?
-        };
+        let cond = self.parse_condition(true)?;
         while_node.children.push(cond);
 
         // Zig's CONTINUE EXPRESSION: `while (i < n) : (i += 1) { ... }`, the
@@ -5485,17 +5519,7 @@ impl Parser {
         // Without parentheses, `Name {` opens the THEN branch, so
         // struct-literal parsing is suppressed for the condition exactly as
         // it is for the statement form.
-        let cond = if self.current.kind == TokenKind::LParen {
-            self.advance();
-            let c = self.parse_expr()?;
-            self.expect(TokenKind::RParen)?;
-            c
-        } else {
-            self.no_struct_literal += 1;
-            let c = self.parse_expr();
-            self.no_struct_literal -= 1;
-            c?
-        };
+        let cond = self.parse_condition(false)?;
 
         // Then expression
         let then_expr = self.parse_branch_value()?;
@@ -5718,6 +5742,11 @@ impl Parser {
             // Statement clauses must sit on the line immediately after the
             // previous clause; a gap returns the old boundary reading.
             let adjacent = self.current.line <= self.last_line + 1;
+            let eff_col = if lowered == 0 && self.peek.kind == TokenKind::Ident {
+                first_clause_col.or(Some(self.current.col))
+            } else {
+                first_clause_col
+            };
             // A body that OPENS with `var`/`const` has no earlier clause to
             // take a column from, so `first_clause_col` was still None, this
             // arm was skipped, and the whole braceless body fell back to the
@@ -5726,8 +5755,17 @@ impl Parser {
             // the block, it IS the first clause.
             if matches!(self.current.kind, TokenKind::KwConst | TokenKind::KwVar)
                 && adjacent
-                && first_clause_col.map_or(false, |c| c > 1 && self.current.col >= c)
+                // The arm models `const NAME ...` only. `const (a, b) = f()` is the
+                // tuple-destructure statement, and letting the arm swallow the
+                // keyword leaves the parser on `(` at module level, where
+                // parse_const_decl demands a name and dies -- a hard error where the
+                // old path fell back safely.
+                && self.peek.kind == TokenKind::Ident
+                && eff_col.map_or(false, |c| c > 1 && self.current.col >= c)
             {
+                if first_clause_col.is_none() {
+                    first_clause_col = eff_col;
+                }
                 let st_entry = self.save_state();
                 let _st_line = self.current.line;
                 let mutable = self.current.kind == TokenKind::KwVar;
@@ -6446,14 +6484,23 @@ impl Parser {
         // invariant followed by any of those dropped its OWN assert. They end
         // the block here as cleanly as const/fn do; the GLOBAL boundary set is
         // left alone (adding KwVar there would hoist keyword-test-body vars).
-        let clean_end = Self::is_block_boundary(self.current.kind)
-            || matches!(
-                self.current.kind,
-                TokenKind::KwVar
-                    | TokenKind::KwEnum
-                    | TokenKind::KwStruct
-                    | TokenKind::KwUsing
-            );
+        // `const` opens a module-level DECLARATION and is a boundary -- unless
+        // it is followed by `(`, which is the tuple-destructure STATEMENT form
+        // `const (a, b) = f();`. Treating that as a clean end hands it to the
+        // module parser, which requires a name after `const` and dies with
+        // "Expected identifier after 'const', got LParen". The block has not
+        // ended; the clause parser simply stopped inside it.
+        let const_destructure =
+            self.current.kind == TokenKind::KwConst && self.peek.kind == TokenKind::LParen;
+        let clean_end = !const_destructure
+            && (Self::is_block_boundary(self.current.kind)
+                || matches!(
+                    self.current.kind,
+                    TokenKind::KwVar
+                        | TokenKind::KwEnum
+                        | TokenKind::KwStruct
+                        | TokenKind::KwUsing
+                ));
         if !clean_end {
             // A block that lowered SOMETHING and then met a clause it cannot
             // model used to lose the lot: two checkable `assert`s on either
@@ -21805,6 +21852,64 @@ impl RustCodegen {
         }
     }
 
+    /// Zig builtins, in Rust.
+    ///
+    /// t27's surface is Zig-shaped, so `@as`, `@intCast`, `@min` and friends
+    /// appear in specs. The Rust emitter passed them through verbatim -- 27
+    /// distinct builtins, ~250 occurrences across 43 specs -- and `@as(u32, x)`
+    /// is not Rust, so every one of those files failed to compile. Nothing
+    /// reported it, because `corpus` did not measure the Rust backend at all.
+    ///
+    /// Two groups, and the difference matters. Where Zig names the target type
+    /// the translation is exact. Where Zig INFERS it from context (`@intCast`,
+    /// `@floatFromInt`) the honest Rust is `as _`, which asks rustc to infer
+    /// from the same context -- a `let` with a declared type, or a `return` in
+    /// a typed fn. Guessing a concrete width instead would be a silent wrong
+    /// answer, which is the defect class this backend has just been cleared of.
+    fn zig_builtin_to_rust(name: &str, args: &[String]) -> Option<String> {
+        if !name.starts_with('@') {
+            return None;
+        }
+        let a = |i: usize| args.get(i).cloned().unwrap_or_default();
+        let two = args.len() == 2;
+        let one = args.len() == 1;
+        Some(match name {
+            // Target named by the source: exact.
+            "@as" if two => format!("({} as {})", a(1), Self::t27_type_to_rust(&a(0))),
+            "@intCast" | "@floatCast" | "@truncate" if two => {
+                format!("({} as {})", a(1), Self::t27_type_to_rust(&a(0)))
+            }
+            "@intFromFloat" | "@floatFromInt" if two => {
+                format!("({} as {})", a(1), Self::t27_type_to_rust(&a(0)))
+            }
+            // Target inferred from context, exactly as in Zig.
+            "@intCast" | "@floatCast" | "@truncate" | "@intFromFloat" | "@floatFromInt"
+                if one =>
+            {
+                format!("({} as _)", a(0))
+            }
+            // A fieldless enum casts to its discriminant in both languages.
+            "@intFromEnum" if one => format!("({} as i32)", a(0)),
+            // Method calls in Rust.
+            "@min" if two => format!("({}).min({})", a(0), a(1)),
+            "@max" if two => format!("({}).max({})", a(0), a(1)),
+            "@sqrt" | "@abs" | "@round" | "@floor" | "@ceil" | "@trunc" | "@exp" | "@log"
+            | "@sin" | "@cos" | "@tan"
+                if one =>
+            {
+                format!("({}).{}()", a(0), &name[1..])
+            }
+            // Operators in Rust.
+            "@rem" if two => format!("({} % {})", a(0), a(1)),
+            "@mod" if two => format!("({}).rem_euclid({})", a(0), a(1)),
+            "@divTrunc" if two => format!("({} / {})", a(0), a(1)),
+            "@divFloor" if two => format!("({}).div_euclid({})", a(0), a(1)),
+            // Anything else keeps its spelling: a wrong translation is worse
+            // than an untranslated one, because the first compiles.
+            _ => return None,
+        })
+    }
+
     fn t27_type_to_rust(t27_type: &str) -> String {
         let t = t27_type.trim();
         // Handle optional types. t27 writes the Zig spelling -- a LEADING `?`
@@ -22092,6 +22197,9 @@ impl RustCodegen {
                     .iter()
                     .map(|c| self.expr_to_rust(c))
                     .collect();
+                if let Some(built) = Self::zig_builtin_to_rust(&node.name, &args) {
+                    return built;
+                }
                 format!("{}({})", node.name, args.join(", "))
             }
             NodeKind::ExprArrayLiteral => {