deal with terminators uniformly in narrowing and resolve

examples/forContinue.def.lean

@@ -65,6 +65,34 @@ method countPositivesNonNested (grid : Array (Array Int)) return (res : Int)
       i := i + 1
     return total
 
+method lastPresent (xs : Array (Option Int)) return (res : Option Int)
+  do
+    let mut cur : Option Int := none
+    for _x_idx in [:xs.size]
+      invariant _x_idx ≤ xs.size
+    do
+      let x := xs[_x_idx]!
+      if h_x : (x).isSome = true then
+        let _x_val := (x).get h_x
+        cur := some _x_val
+      else
+        pure ()
+    return cur
+
+method lastBeforeGap (xs : Array (Option Int)) return (res : Option Int)
+  do
+    let mut cur : Option Int := none
+    for _x_idx in [:xs.size]
+      invariant _x_idx ≤ xs.size
+    do
+      let x := xs[_x_idx]!
+      if h_x : (x).isSome = true then
+        let _x_val := (x).get h_x
+        cur := some _x_val
+      else
+        break
+    return cur
+
 method countKeep (items : Array Item) return (res : Int)
   ensures 0 ≤ res
   ensures res ≤ items.size

examples/forContinue.dfy

@@ -1,5 +1,7 @@
 // Generated by lsc from forContinue.ts
 
+datatype Option<T> = None | Some(value: T)
+
 function JSRem(a: int, b: int): int
   requires b != 0
 {
@@ -81,6 +83,44 @@ method countPositivesNonNested(grid: seq<seq<int>>) returns (res: int)
   return total;
 }
 
+method lastPresent(xs: seq<Option<int>>) returns (res: Option<int>)
+{
+  var cur := None;
+  var i_x_idx := 0;
+  while i_x_idx < |xs|
+    invariant (i_x_idx <= |xs|)
+  {
+    var x := xs[i_x_idx];
+    match x {
+      case Some(i_x_val) =>
+        cur := Some(i_x_val);
+      case None =>
+
+    }
+    i_x_idx := i_x_idx + 1;
+  }
+  return cur;
+}
+
+method lastBeforeGap(xs: seq<Option<int>>) returns (res: Option<int>)
+{
+  var cur := None;
+  var i_x_idx := 0;
+  while i_x_idx < |xs|
+    invariant (i_x_idx <= |xs|)
+  {
+    var x := xs[i_x_idx];
+    match x {
+      case Some(i_x_val) =>
+        cur := Some(i_x_val);
+      case None =>
+        break;
+    }
+    i_x_idx := i_x_idx + 1;
+  }
+  return cur;
+}
+
 method countKeep(items: seq<Item>) returns (res: int)
   ensures (0 <= res)
   ensures (res <= |items|)

examples/forContinue.dfy.gen

@@ -1,5 +1,7 @@
 // Generated by lsc from forContinue.ts
 
+datatype Option<T> = None | Some(value: T)
+
 function JSRem(a: int, b: int): int
   requires b != 0
 {
@@ -81,6 +83,44 @@ method countPositivesNonNested(grid: seq<seq<int>>) returns (res: int)
   return total;
 }
 
+method lastPresent(xs: seq<Option<int>>) returns (res: Option<int>)
+{
+  var cur := None;
+  var i_x_idx := 0;
+  while i_x_idx < |xs|
+    invariant (i_x_idx <= |xs|)
+  {
+    var x := xs[i_x_idx];
+    match x {
+      case Some(i_x_val) =>
+        cur := Some(i_x_val);
+      case None =>
+
+    }
+    i_x_idx := i_x_idx + 1;
+  }
+  return cur;
+}
+
+method lastBeforeGap(xs: seq<Option<int>>) returns (res: Option<int>)
+{
+  var cur := None;
+  var i_x_idx := 0;
+  while i_x_idx < |xs|
+    invariant (i_x_idx <= |xs|)
+  {
+    var x := xs[i_x_idx];
+    match x {
+      case Some(i_x_val) =>
+        cur := Some(i_x_val);
+      case None =>
+        break;
+    }
+    i_x_idx := i_x_idx + 1;
+  }
+  return cur;
+}
+
 method countKeep(items: seq<Item>) returns (res: int)
   ensures (0 <= res)
   ensures (res <= |items|)

examples/forContinue.ts

@@ -70,6 +70,33 @@ export function countPositivesNonNested(grid: number[][]): number {
   return total;
 }
 
+// Early `continue` on an optional guard must narrow `x` for the rest of the
+// body — resolve's block-tail narrowing fires on any terminator (return/throw/
+// break/continue), the same set as narrow's isTerminating. The assignment into
+// the optional `cur` then needs a Some-wrap of the narrowed `x`; regression was
+// `cur := i_x_val` (ill-typed Dafny) because only `return` triggered narrowing.
+export function lastPresent(xs: (number | undefined)[]): number | undefined {
+  //@ verify
+  let cur: number | undefined = undefined;
+  for (const x of xs) {
+    if (x === undefined) continue;
+    cur = x;
+  }
+  return cur;
+}
+
+// Same shape with `break`: stop at the first absent entry, keeping the last
+// present value seen. Pins the terminator set beyond `continue`.
+export function lastBeforeGap(xs: (number | undefined)[]): number | undefined {
+  //@ verify
+  let cur: number | undefined = undefined;
+  for (const x of xs) {
+    if (x === undefined) break;
+    cur = x;
+  }
+  return cur;
+}
+
 // A `continue` in a non-last `switch` (→ `match`) arm: the inverter can't fold
 // it (not a trailing-guard `if`, and the match isn't the loop body's last stmt),
 // so it survives to native Dafny `continue` emission — the shape flue's narrowed

tools/src/narrow.ts

@@ -36,6 +36,7 @@
  */
 
 import type { TModule, TFunction, TStmt, TExpr, Ty } from "./typedir.js";
+import { isTerminatorKind } from "./typedir.js";
 import type { TypeDeclInfo } from "./types.js";
 import { freshName } from "./names.js";
 
@@ -875,8 +876,7 @@ function parseNegativeDiscriminantCond(cond: TExpr): { scrutinee: TExpr & { kind
 
 function isTerminating(stmts: TStmt[]): boolean {
   if (stmts.length === 0) return false;
-  const last = stmts[stmts.length - 1];
-  return last.kind === "return" || last.kind === "throw" || last.kind === "break" || last.kind === "continue";
+  return isTerminatorKind(stmts[stmts.length - 1].kind);
 }
 
 /** Rule (list-level): consecutive `if (x.kind === "v") ...` chain → tagMatch.

tools/src/resolve.ts

@@ -7,7 +7,7 @@
 
 import type { RawExpr, RawStmt, RawFunction, RawModule } from "./rawir.js";
 import type { Ty, TExpr, TStmt, TFunction, TModule, TParam, CallKind } from "./typedir.js";
-import { isBigInt, tyEqual } from "./typedir.js";
+import { isBigInt, tyEqual, isTerminatorKind } from "./typedir.js";
 import { parseTsType, tyToCanonical } from "./types.js";
 import type { TypeDeclInfo } from "./types.js";
 import { parseExpr } from "./specparser.js";
@@ -1260,9 +1260,12 @@ function resolveBlock(stmts: RawStmt[], ctx: Ctx): TStmt[] {
     env = nextEnv;
     // Flow narrowing: if (x === undefined) { return } narrows x for rest of block.
     // Also handles compound: if (x === undefined || y === undefined) { return }
+    // Any terminator counts (return/throw/break/continue — same set as narrow's
+    // isTerminating): each exits the current block, so the rest of the block
+    // only runs when the guard was false.
     // Field chains are excluded — resolve can't substitute in statement lists;
     // transform's emitOptionalMatch handles field chains in statement contexts.
-    if (s.kind === "if" && s.then.length > 0 && s.then[s.then.length - 1].kind === "return" && s.else.length === 0) {
+    if (s.kind === "if" && s.then.length > 0 && isTerminatorKind(s.then[s.then.length - 1].kind) && s.else.length === 0) {
       const narrowings = collectEarlyReturnNarrowings(s.cond, withEnv(ctx, env));
       for (const n of narrowings) {
         env = extend(env, n.varName, n.innerTy);

tools/src/typedir.ts

@@ -133,6 +133,13 @@ export type TStmt =
       cases: { variant: string; body: TStmt[] }[];
       fallthrough: TStmt[] }
 
+/** Statement kinds that unconditionally leave the enclosing block. Shared by
+ *  resolve (block-tail narrowing) and narrow (isTerminating); works on raw and
+ *  typed IR alike since both use these kind strings. */
+export function isTerminatorKind(kind: string): boolean {
+  return kind === "return" || kind === "throw" || kind === "break" || kind === "continue";
+}
+
 // ── Top-level ────────────────────────────────────────────────
 
 export interface TParam {