parser: a forall no longer takes its checkable neighbours with it (Refs #2161)

bootstrap/src/compiler.rs

@@ -5886,6 +5886,24 @@ impl Parser {
                 // An identifier that is not a clause means this body has a shape
                 // we do not model. Falling through with the parser positioned
                 // mid-block is what broke 19 specs on the first attempt.
+                // But when clauses BEFORE it lowered, throwing them away is a second
+                // loss on top of the one that is defensible. An invariant reading
+                //
+                //     assert g(1) == 111
+                //     forall x: i32 . g(x) == x
+                //     assert g(2) == 222
+                //
+                // lost BOTH asserts to the `forall` between them. Skipping an unbounded
+                // `forall` is a language decision; taking its neighbours with it is not.
+                // Keep them, and MARK the block -- the emitter's NOT CHECKED notice keys
+                // on `children.is_empty()`, so without the mark a partial block would
+                // report as fully verified.
+                if block.children.len() > start_children {
+                    block.extra_field = "partial".to_string();
+                    self.restore_state(entry);
+                    self.skip_to_next_top_level();
+                    return;
+                }
                 self.restore_bdd_fallback(block, start_children, entry);
                 return;
             }
@@ -6437,7 +6455,22 @@ impl Parser {
                     | TokenKind::KwUsing
             );
         if !clean_end {
-            self.restore_bdd_fallback(block, start_children, entry);
+            // A block that lowered SOMETHING and then met a clause it cannot
+            // model used to lose the lot: two checkable `assert`s on either
+            // side of a `forall` both vanished, and only the `forall` was
+            // defensible to skip.
+            //
+            // Keep what lowered, and MARK the block, because the emitter's
+            // "NOT CHECKED" notice keys on `children.is_empty()` -- without
+            // the mark a partial block would report as fully verified, which
+            // is the exact claim W635 was written to stop.
+            if block.children.len() > start_children {
+                block.extra_field = "partial".to_string();
+                self.restore_state(entry);
+                self.skip_to_next_top_level();
+            } else {
+                self.restore_bdd_fallback(block, start_children, entry);
+            }
         }
     }
 
@@ -8213,7 +8246,7 @@ impl Codegen {
             self.gen_stmt(stmt);
         }
 
-        if node.children.is_empty() {
+        if node.children.is_empty() || node.extra_field == "partial" {
             self.write_indent();
             // A comment, not @compileLog: @compileLog is a hard compile error
             // under `zig test` ("found compile log statement"), so the marker

bootstrap/stage0/FROZEN_HASH

@@ -1 +1 @@
-024051760b49a8fae2a3b56cbd362d2bba1dbc6bdc61594f7adfba67c1e3f9fa
+f9074870f5f306184091e22fb0090963607e3b392c2d5805b125b79e9f60c6ac

docs/now/2026-08-28-a-forall-took-its-checkable-neighbours-with-it.md

@@ -0,0 +1,8 @@
+# NOW -- A forall took its checkable neighbours with it (2026-08-28)
+
+## A forall took its checkable neighbours with it (Refs #2161)
+
+- Refs #2161. An invariant with `assert g(1) == 111`, then a forall, then `assert g(2) == 222` lost BOTH asserts. Skipping an unbounded forall is a defensible language decision -- the compiler says so in its own comment -- but taking the clauses around it is a second loss on top of the defensible one, and nothing recorded that it happened
+- Clauses lowered BEFORE the unmodellable one are now kept, and the block is MARKED. The mark matters as much as the keeping: the NOT CHECKED notice keys on children.is_empty(), so a partial block without it would report as fully verified -- the exact claim W635 exists to stop
+- Measured: assertions in generated Zig 11704 -> 11712 (+8), NOT CHECKED markers unchanged at 1068, specs that LOST an assertion ZERO, parse 620 -> 620, RATCHET CLEAN. Eight is the honest number -- the census that motivated this estimated ~9400 recoverable tokens, but that counterfactual REWROTE THE SOURCE while this keeps what the existing parser already lowered
+- Found with the compiler own instrument: T27_BDD_DEBUG named the fallback site on the first try, after I had guessed the wrong one, edited it, and watched the probe not move. The tool that answers exactly was already in the tree