Generalize or narrow

SPEC.md

@@ -686,7 +686,8 @@ enqueued.add(id);        // → Lean: enqueued := enqueued.insert id
 
 - Equality: `v !== undefined`, `v === undefined` (early return)
 - Truthiness: `if (v)`, `if (!v)`, `opt ? a : b`
-- Composition: `v && rest` or `rest && v` (optional check on either side) — in an `if`/`?:` condition or as a bare statement (`v !== undefined && v.f()`, the `if`-less guard idiom); `a === undefined || b === undefined`
+- Composition: `v && rest` or `rest && v` (optional check on either side) — in an `if`/`?:` condition or as a bare statement (`v !== undefined && v.f()`, the `if`-less guard idiom)
+- Disjunctive early return: `a === undefined || b === undefined`, `!x || x.f !== v`, `x?.t !== 'm' || x.g`
 - Spec implication: `path !== undefined && rest ==> B` (premise narrows conclusion)
 - Optional chaining: `obj?.field`, `obj?.foo()`, `obj?.[i]`, chained `obj?.a?.b?.c` and `obj?.a.b.c`
 - Nullish coalescing: `x ?? default`; array index `arr[i] ?? default` (undefined ⟺ out of bounds under `noUncheckedIndexedAccess`) → `(0 <= i && i < arr.length) ? arr[i] : default`

examples/auction.dfy

@@ -0,0 +1,55 @@
+// Generated by lsc from auction.ts
+
+datatype Option<T> = None | Some(value: T)
+
+datatype Bid = Bid(key: string, amount: int)
+
+method highestBid(bids: seq<Option<Bid>>, key: string, reserve: int) returns (res: int)
+  ensures (res >= reserve)
+{
+  var best := reserve;
+  var i := 0;
+  while (i < |bids|)
+    invariant (best >= reserve)
+  {
+    var bid := bids[i];
+    match bid {
+      case Some(i_bid_val) =>
+        if (i_bid_val.key != key) {
+          i := (i + 1);
+          continue;
+        }
+        if (i_bid_val.amount > best) {
+          best := i_bid_val.amount;
+        }
+        i := (i + 1);
+      case None =>
+        i := (i + 1);
+    }
+  }
+  return best;
+}
+
+method firstFunded(bids: seq<Option<Bid>>, key: string) returns (res: int)
+  ensures ((res == -1) || ((0 <= res) && (res < |bids|)))
+{
+  var i := 0;
+  while (i < |bids|)
+    invariant (0 <= i)
+    invariant (i <= |bids|)
+  {
+    var bid := bids[i];
+    match bid {
+      case Some(i_bid_val) =>
+        if ((i_bid_val.key != key) || (i_bid_val.amount <= 0)) {
+          i := (i + 1);
+          continue;
+        }
+        return i;
+        i := (i + 1);
+      case None =>
+        i := (i + 1);
+    }
+  }
+  return -1;
+}

examples/auction.dfy.gen

@@ -0,0 +1,55 @@
+// Generated by lsc from auction.ts
+
+datatype Option<T> = None | Some(value: T)
+
+datatype Bid = Bid(key: string, amount: int)
+
+method highestBid(bids: seq<Option<Bid>>, key: string, reserve: int) returns (res: int)
+  ensures (res >= reserve)
+{
+  var best := reserve;
+  var i := 0;
+  while (i < |bids|)
+    invariant (best >= reserve)
+  {
+    var bid := bids[i];
+    match bid {
+      case Some(i_bid_val) =>
+        if (i_bid_val.key != key) {
+          i := (i + 1);
+          continue;
+        }
+        if (i_bid_val.amount > best) {
+          best := i_bid_val.amount;
+        }
+        i := (i + 1);
+      case None =>
+        i := (i + 1);
+    }
+  }
+  return best;
+}
+
+method firstFunded(bids: seq<Option<Bid>>, key: string) returns (res: int)
+  ensures ((res == -1) || ((0 <= res) && (res < |bids|)))
+{
+  var i := 0;
+  while (i < |bids|)
+    invariant (0 <= i)
+    invariant (i <= |bids|)
+  {
+    var bid := bids[i];
+    match bid {
+      case Some(i_bid_val) =>
+        if ((i_bid_val.key != key) || (i_bid_val.amount <= 0)) {
+          i := (i + 1);
+          continue;
+        }
+        return i;
+        i := (i + 1);
+      case None =>
+        i := (i + 1);
+    }
+  }
+  return -1;
+}

examples/auction.ts

@@ -0,0 +1,36 @@
+/**
+ * Sealed-bid auction over a sparse bid book: `bids[i]` may be empty (`undefined`)
+ * where a slot was withdrawn. `highestBid` returns the winning amount for an item,
+ * never below its reserve; `firstFunded` finds the earliest usable bid.
+ */
+
+//@ backend dafny
+
+type Bid = { key: string; amount: number };
+
+// Winning bid amount for `key` — the max over matching bids, floored at the reserve.
+function highestBid(bids: (Bid | undefined)[], key: string, reserve: number): number {
+  //@ verify
+  //@ ensures \result >= reserve
+  let best = reserve;
+  for (let i = 0; i < bids.length; i++) {
+    //@ invariant best >= reserve
+    const bid = bids[i];
+    if (!bid || bid.key !== key) continue;
+    if (bid.amount > best) best = bid.amount;
+  }
+  return best;
+}
+
+// Index of the first funded bid for `key` (present, positive amount), else -1.
+function firstFunded(bids: (Bid | undefined)[], key: string): number {
+  //@ verify
+  //@ ensures \result === -1 || (0 <= \result && \result < bids.length)
+  for (let i = 0; i < bids.length; i++) {
+    //@ invariant 0 <= i && i <= bids.length
+    const bid = bids[i];
+    if (bid?.key !== key || bid.amount <= 0) continue;
+    return i;
+  }
+  return -1;
+}

tools/src/narrow.ts

@@ -261,45 +261,82 @@ function ruleEarlyReturnConsume(s: TStmt, rest: TStmt[]): TStmt | null {
   };
 }
 
-/** Collect a `||` chain of negative optional checks (`x === undefined`).
- *  Returns the list of checks if every leaf is a negative optional check; null otherwise. */
-function collectOrChainOfNegativeChecks(cond: TExpr): ReturnType<typeof parseSimpleOptionalCheck>[] | null {
-  if (cond.kind === "binop" && cond.op === "||") {
-    const left = collectOrChainOfNegativeChecks(cond.left);
-    const right = collectOrChainOfNegativeChecks(cond.right);
-    if (!left || !right) return null;
-    return [...left, ...right];
+/** Flatten a nested `||` chain into its leaf conditions. */
+function flattenOr(e: TExpr): TExpr[] {
+  if (e.kind === "binop" && e.op === "||") return [...flattenOr(e.left), ...flattenOr(e.right)];
+  return [e];
+}
+
+/** A `||` disjunct that `x === None` makes true (so if every disjunct is false,
+ *  `x` is Some). `residual` is the guard it still contributes once `x` is Some
+ *  (`!v` for a falsy-capable `!x`; `v.chain !== lit` for an optchain compare;
+ *  null otherwise). */
+type NoneDetector = { scrutinee: TExpr; innerTy: Ty; binder: string; residual: TExpr | null };
+
+function classifyDisjunct(leaf: TExpr): NoneDetector | null {
+  // `x?.chain !== lit` — `undefined !== lit` is true when x is None.
+  if (leaf.kind === "binop" && leaf.op === "!==") {
+    const oc = leaf.left.kind === "optChain" ? leaf.left : leaf.right.kind === "optChain" ? leaf.right : null;
+    if (oc && oc.kind === "optChain" && oc.obj.ty.kind === "optional") {
+      const hint = binderHintFor(oc.obj);
+      if (hint === null) return null;
+      const binder = freshName(hint);
+      const unwrapped = applyChain({ kind: "var", name: binder, ty: oc.obj.ty.inner }, oc.chain);
+      if (unwrapped.kind === "field" && unwrapped.obj.ty.kind === "user") {
+        const base = unwrapped.obj.ty.name.replace(/<.*/, "");
+        const decl = _typeDecls.find(d => d.name === base);
+        if (decl?.kind === "discriminated-union" && decl.discriminant === unwrapped.field) unwrapped.isDiscriminant = true;
+      }
+      const lit = leaf.left === oc ? leaf.right : leaf.left;
+      return { scrutinee: oc.obj, innerTy: oc.obj.ty.inner, binder, residual: { kind: "binop", op: "!==", left: unwrapped, right: lit, ty: { kind: "bool" } } };
+    }
   }
-  const check = parseSimpleOptionalCheck(cond);
-  if (!check || !check.negated) return null;
-  return [check];
+  // `!x` / `x === undefined`.
+  const chk = parseOptionalCheck(leaf);
+  if (chk && chk.negated) {
+    const residual: TExpr | null = canBeFalsy(chk)
+      ? { kind: "unop", op: "!", expr: { kind: "var", name: chk.binderHint, ty: chk.innerTy }, ty: { kind: "bool" } }
+      : null;
+    return { scrutinee: chk.scrutinee, innerTy: chk.innerTy, binder: chk.binderHint, residual };
+  }
+  return null;
 }
 
-/** Rule: `if (x === undefined || y === undefined || ...) terminate; rest`.
- *  → nested someMatches narrowing each var in turn, each None branch = terminate,
- *    deepest someBody = rest.
+/** Rule: `if (D1 || … || Dn) terminate; rest`. Each `Di` that detects some optional
+ *  `x` is None (`!x`, `x === undefined`, `x?.chain !== lit`) narrows that `x` to Some
+ *  across `rest`; the rest — value guards reading a narrowed `x` directly, plus the
+ *  detectors' Some-case residuals — become a trailing early-return. Sound: reaching
+ *  `rest` means every disjunct was false, so every detected optional is present.
+ *  Covers `if (!x || x.f !== v) continue` / `if (x?.t !== 'm' || x.g) break`.
  *  Closes the resolve.ts:602 TODO ("|| narrowing"). */
 function ruleEarlyReturnOrChain(s: TStmt, rest: TStmt[]): TStmt | null {
   if (s.kind !== "if") return null;
   if (rest.length === 0) return null;
-  if (s.then.length === 0 || s.else.length !== 0) return null;
+  if (s.then.length === 0 || s.else.length !== 0 || !isTerminating(s.then)) return null;
   if (s.cond.kind !== "binop" || s.cond.op !== "||") return null;  // single check is the simpler rule
-  const checks = collectOrChainOfNegativeChecks(s.cond);
-  if (!checks || checks.length < 2) return null;
-  // Build nested someMatch from innermost outward
-  let inner: TStmt[] = rest;
-  for (let i = checks.length - 1; i >= 0; i--) {
-    const check = checks[i]!;
-    const someBody: TStmt[] = canBeFalsy(check)
-      ? [{ kind: "if", cond: bound(check), then: inner, else: s.then }]
-      : inner;
-    inner = [{
-      kind: "someMatch",
-      scrutinee: check.scrutinee, binderTy: check.innerTy,
-      binder: check.binderHint,
-      someBody,
-      noneBody: s.then,
-    }];
+  const leaves = flattenOr(s.cond);
+  if (leaves.length < 2) return null;
+
+  const detectors: NoneDetector[] = [];
+  const residualLeaves: TExpr[] = [];
+  const seen = new Set<string>();
+  for (const leaf of leaves) {
+    const d = classifyDisjunct(leaf);
+    if (!d) { residualLeaves.push(leaf); continue; }
+    const key = binderHintFor(d.scrutinee)!;
+    if (seen.has(key)) return null;  // two detectors on one optional: rare; leave to other rules
+    seen.add(key);
+    detectors.push(d);
+    if (d.residual) residualLeaves.push(d.residual);
+  }
+  if (detectors.length === 0) return null;
+
+  let inner: TStmt[] = residualLeaves.length === 0
+    ? rest
+    : [{ kind: "if", cond: residualLeaves.reduce((a, b): TExpr => ({ kind: "binop", op: "||", left: a, right: b, ty: { kind: "bool" } })), then: s.then, else: [] }, ...rest];
+  for (let i = detectors.length - 1; i >= 0; i--) {
+    const d = detectors[i]!;
+    inner = [{ kind: "someMatch", scrutinee: d.scrutinee, binderTy: d.innerTy, binder: d.binder, someBody: inner, noneBody: s.then }];
   }
   return inner[0];
 }

tools/src/transform.ts

@@ -335,7 +335,8 @@ function coerceCondToBool(cond: Expr, ty: Ty): Expr {
     return { kind: "binop", op: "≠", left: cond, right: { kind: "num", value: 0 } };
   if (ty.kind === "string")
     return { kind: "binop", op: ">", left: { kind: "field", obj: cond, field: "length" }, right: { kind: "num", value: 0 } };
-  if (ty.kind === "array")
+  // Arrays, objects, maps, sets, tuples are always truthy in JS (even `[]`/`{}`).
+  if (["array", "user", "map", "set", "tuple"].includes(ty.kind))
     return { kind: "bool", value: true };
   return cond;
 }