porting from ls-in-ls branch

.github/workflows/ci.yml

@@ -187,8 +187,25 @@ jobs:
     steps:
       - uses: actions/checkout@v6
 
+      # Staging override: on a PR from branch <b>, if the case-study repo has a
+      # branch named <pinned>-<b>, clone that instead of the pinned branch.
+      # Lets case studies be updated against an in-flight LemmaScript branch
+      # without touching the branch that main's CI pins.
       - name: Clone case study
-        run: git clone --branch ${{ matrix.branch }} https://github.com/${{ matrix.repo }}.git ../case-study
+        env:
+          DEFAULT_BRANCH: ${{ matrix.branch }}
+          LS_BRANCH: ${{ github.head_ref || github.ref_name }}
+        run: |
+          repo="https://github.com/${{ matrix.repo }}.git"
+          branch="$DEFAULT_BRANCH"
+          if [ "$LS_BRANCH" != "main" ]; then
+            staging="$DEFAULT_BRANCH-$LS_BRANCH"
+            if git ls-remote --exit-code --heads "$repo" "$staging" >/dev/null; then
+              echo "Using staging branch $staging (default: $DEFAULT_BRANCH)"
+              branch="$staging"
+            fi
+          fi
+          git clone --branch "$branch" "$repo" ../case-study
 
       - uses: actions/setup-node@v6
         with:
@@ -234,8 +251,25 @@ jobs:
     steps:
       - uses: actions/checkout@v6
 
+      # Staging override: on a PR from branch <b>, if the case-study repo has a
+      # branch named <pinned>-<b>, clone that instead of the pinned branch.
+      # Lets case studies be updated against an in-flight LemmaScript branch
+      # without touching the branch that main's CI pins.
       - name: Clone case study
-        run: git clone --branch ${{ matrix.branch }} https://github.com/${{ matrix.repo }}.git ../case-study
+        env:
+          DEFAULT_BRANCH: ${{ matrix.branch }}
+          LS_BRANCH: ${{ github.head_ref || github.ref_name }}
+        run: |
+          repo="https://github.com/${{ matrix.repo }}.git"
+          branch="$DEFAULT_BRANCH"
+          if [ "$LS_BRANCH" != "main" ]; then
+            staging="$DEFAULT_BRANCH-$LS_BRANCH"
+            if git ls-remote --exit-code --heads "$repo" "$staging" >/dev/null; then
+              echo "Using staging branch $staging (default: $DEFAULT_BRANCH)"
+              branch="$staging"
+            fi
+          fi
+          git clone --branch "$branch" "$repo" ../case-study
 
       - uses: actions/setup-node@v6
         with:

SPEC.md

@@ -469,13 +469,13 @@ The same coercion applies to non-bool conditions in `if`/`while`/`?:` positions:
 | `s.length` | `s.length` | `\|s\|` |
 | `Math.max(...s)` / `Math.min(...s)` | — | `MaxOfSeq(s)` / `MinOfSeq(s)` (requires `\|s\| > 0`) |
 | `perm(a, b)` (spec-only) | — | `Perm(a, b)` (preamble: `predicate Perm<T(==)>(a, b) { multiset(a) == multiset(b) }`) |
-| `arr.map((x) => e)` | `arr.map (fun x => e)` | `Std.Collections.Seq.Map((x) => e, arr)` |
+| `arr.map((x) => e)` | `arr.map (fun x => e)` | `seq(\|arr\|, i requires 0 <= i < \|arr\| => var x := arr[i]; e)` (§3.7) |
 | `arr.filter((x) => e)` | `arr.filter (fun x => e)` | `Std.Collections.Seq.Filter((x) => e, arr)` |
 | `arr.every((x) => e)` | `arr.all (fun x => e)` | `Std.Collections.Seq.All(arr, (x) => e)` |
 | `arr.some((x) => e)` | `arr.any (fun x => e)` | `exists x :: x in arr && e` |
 | `arr.includes(x)` | `arr.contains x` | `(x in arr)` |
 | `arr.indexOf(x)` | — | `SeqIndexOf(arr, x)` (preamble) |
-| `arr.find((x) => e)` | `arr.find? (fun x => e)` | — |
+| `arr.find((x) => e)` | `arr.find? (fun x => e)` | `SeqFind(arr, (x) => e)` (preamble) |
 | `arr.findIndex((x) => e)` | — | `SeqFindIndex(arr, (x) => e)` (preamble: `-1 ⇔ no match`, `≥0 ⇔ first match with no earlier match`) |
 | `arr.findLast((x) => e)` | — | `SeqFindLast(arr, (x) => e)` (preamble) |
 | `arr.findLastIndex((x) => e)` | — | `SeqFindLastIndex(arr, (x) => e)` (preamble: `-1 ⇔ no match`, `≥0 ⇔ last match with no later match`) |
@@ -622,6 +622,8 @@ Lambda bodies can be expressions (`(x) => x + 1`) or statement blocks (`(x) => {
 
 **filterMap.** `xs.map(x => ... | undefined).filter((x): x is T => x !== undefined)` drops the `undefined`s *and* unwraps to `seq<T>` — lowered to the proven `SeqFilterSome` preamble (a plain `Map(.value, Filter(.Some?, ...))` wouldn't verify, since `.value` is partial).
 
+**`.map` (Dafny).** Lowered to a `seq` comprehension with the element access inlined (`var x := arr[i]; e`), not `Seq.Map`. `Seq.Map` hides the element behind a closure, so a recursive rebuild walker (`Node(kids.map(walk))`) fails Dafny's termination check — the obligation gets quantified over the lambda's parameter instead of anchored at `kids[i]`. Applying a lambda inside the comprehension fails the same way, hence the inlining.
+
 **Monadic callbacks (Lean):** When the callback calls a method, the HOF call uses the monadic variant (e.g., `arr.mapM f`). Pure callbacks use the non-monadic variant (`arr.map f`). The transform checks the transformed lambda body for monadic binds and selects the variant accordingly.
 
 | Pure | Monadic | When |
@@ -647,13 +649,13 @@ The transform uses two strategies for translating `receiver.method(args)`:
 | `s.slice(start, end)` | `stringSlice` | `JSString.slice s start end` | `s[start..end]` |
 | `[...arr, e]` | `arrayPush` | `Array.push arr e` | `(arr + [e])` |
 | `arr.with(i, v)` | `arraySet` | `arr.set! i v` | `arr[i := v]` |
-| `arr.map(f)` | `map` | `arr.map f` | `Std.Collections.Seq.Map(f, arr)` |
+| `arr.map(f)` | `map` | `arr.map f` | seq comprehension (§3.7) |
 | `arr.filter(f)` | `filter` | `arr.filter f` | `Std.Collections.Seq.Filter(f, arr)` |
 | `arr.every(f)` | `every` | `arr.all f` | `Std.Collections.Seq.All(arr, f)` |
 | `arr.some(f)` | `some` | `arr.any f` | `exists x :: x in arr && ...` |
 | `arr.includes(x)` | `includes` | `arr.contains x` | `(x in arr)` |
 | `arr.indexOf(x)` | `indexOf` | — | `SeqIndexOf(arr, x)` |
-| `arr.find(f)` | `find` | `arr.find? f` | — |
+| `arr.find(f)` | `find` | `arr.find? f` | `SeqFind(arr, f)` |
 | `m.get(k)` | `mapGet` | `m.get? k` | `if k in m then Some(m[k]) else None` |
 | `m.has(k)` | `mapHas` | `m.contains k` | `(k in m)` |
 | `m.set(k, v)` | `mapSet` | `m.insert k v` | `m[k := v]` |

SPEC_DAFNY.md

@@ -92,6 +92,7 @@ The Dafny emitter auto-injects helper functions when needed. Each is emitted at
 |--------|------|---------|
 | `SeqIndexOf` | `arr.indexOf(x)` | First-index search (`-1` if absent) |
 | `SeqFindIndex` | `arr.findIndex(f)` | Predicate first-index search |
+| `SeqFind` | `arr.find(f)` | Predicate first-match search |
 | `SeqFindLast` | `arr.findLast(f)` | Predicate last-match search |
 | `SeqFilterSome` | filterMap pattern (§3.7) | Drop `None`s and unwrap to `seq<T>` |
 | `SeqFlatten` | `arr.flat()` | Flatten one level |

TOOLS.md

@@ -59,7 +59,7 @@ Type names: `Expr`, `Stmt`, `Module`, `MatchArm`, `StmtMatchArm`, and `Decl` = `
 
 All TS `receiver.method(args)` calls produce `methodCall` IR nodes carrying the receiver, its type, the TS method name, the args, and a `monadic` flag. No renaming — the IR stores the TS name (`"map"`, `"indexOf"`, `"with"`, `"get"`, etc.) and the receiver type disambiguates.
 
-Each emitter dispatches on `(receiverTy, method)` to decide syntax. For example, `(array, "map")` → Lean: `arr.map f`, Dafny: `Seq.Map(f, arr)`. Unsupported `(type, method)` pairs error at emit time.
+Each emitter dispatches on `(receiverTy, method)` to decide syntax. For example, `(array, "filter")` → Lean: `arr.filter f`, Dafny: `Seq.Filter(f, arr)`. Unsupported `(type, method)` pairs error at emit time.
 
 `app` is reserved for receiver-less calls: user-defined functions, `Pure.fnName(...)`, `JSFloorDiv(a, b)`, `SetToSeq(s)`.
 

examples/arrayFind.def.lean

@@ -0,0 +1,16 @@
+/-
+  Generated by lsc from arrayFind.ts
+  Do not edit — re-run `lsc gen` to regenerate.
+-/
+import «arrayFind.types»
+
+set_option loom.semantics.termination "total"
+set_option loom.semantics.choice "demonic"
+
+method lookup (entries : Array Entry) (key : String) return (res : Int)
+  do
+    return Pure.lookup entries key
+
+method hasEntry (entries : Array Entry) (key : String) return (res : Bool)
+  do
+    return Pure.hasEntry entries key

examples/arrayFind.dfy

@@ -0,0 +1,40 @@
+// Generated by lsc from arrayFind.ts
+
+datatype Option<T> = None | Some(value: T)
+
+function SeqFind<T>(s: seq<T>, p: T -> bool): Option<T>
+  ensures SeqFind(s, p).Some? ==> p(SeqFind(s, p).value)
+  ensures SeqFind(s, p).Some? ==> SeqFind(s, p).value in s
+  ensures SeqFind(s, p).Some? ==>
+    exists i: nat :: i < |s| && s[i] == SeqFind(s, p).value && p(s[i]) &&
+                     (forall j: nat :: j < i ==> !p(s[j]))
+  ensures SeqFind(s, p).None? ==> forall i :: 0 <= i < |s| ==> !p(s[i])
+  decreases |s|
+{
+  if |s| == 0 then None
+  else if p(s[0]) then Some(s[0])
+  else SeqFind(s[1..], p)
+}
+
+datatype Entry = Entry(key: string, val: int)
+
+function lookup(entries: seq<Entry>, key: string): int
+{
+  var e := SeqFind(entries, (x: Entry) => (x.key == key));
+  match (match e { case Some(i_oc0_val) => Option.Some(i_oc0_val.val) case None => Option.None }) {
+    case Some(i_oc1_val) =>
+      i_oc1_val
+    case None =>
+      0
+  }
+}
+
+function hasEntry(entries: seq<Entry>, key: string): bool
+{
+  match SeqFind(entries, (x: Entry) => (x.key == key)) {
+    case Some(i_) =>
+      true
+    case None =>
+      false
+  }
+}

examples/arrayFind.dfy.gen

@@ -0,0 +1,40 @@
+// Generated by lsc from arrayFind.ts
+
+datatype Option<T> = None | Some(value: T)
+
+function SeqFind<T>(s: seq<T>, p: T -> bool): Option<T>
+  ensures SeqFind(s, p).Some? ==> p(SeqFind(s, p).value)
+  ensures SeqFind(s, p).Some? ==> SeqFind(s, p).value in s
+  ensures SeqFind(s, p).Some? ==>
+    exists i: nat :: i < |s| && s[i] == SeqFind(s, p).value && p(s[i]) &&
+                     (forall j: nat :: j < i ==> !p(s[j]))
+  ensures SeqFind(s, p).None? ==> forall i :: 0 <= i < |s| ==> !p(s[i])
+  decreases |s|
+{
+  if |s| == 0 then None
+  else if p(s[0]) then Some(s[0])
+  else SeqFind(s[1..], p)
+}
+
+datatype Entry = Entry(key: string, val: int)
+
+function lookup(entries: seq<Entry>, key: string): int
+{
+  var e := SeqFind(entries, (x: Entry) => (x.key == key));
+  match (match e { case Some(i_oc0_val) => Option.Some(i_oc0_val.val) case None => Option.None }) {
+    case Some(i_oc1_val) =>
+      i_oc1_val
+    case None =>
+      0
+  }
+}
+
+function hasEntry(entries: seq<Entry>, key: string): bool
+{
+  match SeqFind(entries, (x: Entry) => (x.key == key)) {
+    case Some(i_) =>
+      true
+    case None =>
+      false
+  }
+}

examples/arrayFind.ts

@@ -0,0 +1,21 @@
+/**
+ * `array.find` — first match as an Option (E4).
+ *
+ * `find` returns `T | undefined`, so its result feeds the optional-narrowing
+ * rules: the optChain + nullish on the result exercise `ruleOptChain` /
+ * `ruleNullish` over a `SeqFind` scrutinee. Dafny lowers to the `SeqFind`
+ * preamble helper (first-match ensures); Lean lowers to `.find?`.
+ */
+
+type Entry = { key: string; val: number };
+
+function lookup(entries: Entry[], key: string): number {
+  //@ verify
+  const e = entries.find(x => x.key === key);
+  return e?.val ?? 0;
+}
+
+function hasEntry(entries: Entry[], key: string): boolean {
+  //@ verify
+  return entries.find(x => x.key === key) !== undefined;
+}

examples/arrayFind.types.lean

@@ -0,0 +1,28 @@
+/-
+  Generated by lsc — Lean types and pure function mirrors.
+-/
+import LemmaScript
+
+structure Entry where
+  key : String
+  val : Int
+deriving Repr, Inhabited, DecidableEq
+
+namespace Pure
+
+def lookup (entries : Array Entry) (key : String) : Int :=
+  let e := entries.find? (fun x => x.key = key)
+  match (match e with | .some _oc0_val => Option.some _oc0_val.val | .none => Option.none) with
+  | .some _oc1_val =>
+    _oc1_val
+  | .none =>
+    0
+
+def hasEntry (entries : Array Entry) (key : String) : Bool :=
+  match entries.find? (fun x => x.key = key) with
+  | .some _ =>
+    true
+  | .none =>
+    false
+
+end Pure

examples/ctorName.def.lean

@@ -0,0 +1,21 @@
+/-
+  Generated by lsc from ctorName.ts
+  Do not edit — re-run `lsc gen` to regenerate.
+-/
+import «ctorName.types»
+
+set_option loom.semantics.termination "total"
+set_option loom.semantics.choice "demonic"
+
+method depthOf (k : CallKind) return (res : Int)
+  ensures res ≥ 0
+  do
+    return Pure.depthOf k
+
+method specPure (depth : Int) return (res : CallKind)
+  do
+    return Pure.specPure depth
+
+method plain  return (res : CallKind)
+  do
+    return Pure.plain 

examples/ctorName.dfy

@@ -0,0 +1,31 @@
+// Generated by lsc from ctorName.ts
+
+datatype CallKind = spec_pure(depth: int) | plain
+
+function depthOf(k: CallKind): int
+{
+  match k {
+    case spec_pure(i_k_depth) =>
+      if (i_k_depth >= 0) then
+        i_k_depth
+      else
+        0
+    case plain =>
+      0
+  }
+}
+
+lemma depthOf_ensures(k: CallKind)
+  ensures (depthOf(k) >= 0)
+{
+}
+
+function specPure(depth: int): CallKind
+{
+  spec_pure(depth)
+}
+
+function plain(): CallKind
+{
+  CallKind.plain
+}

examples/ctorName.dfy.gen

@@ -0,0 +1,31 @@
+// Generated by lsc from ctorName.ts
+
+datatype CallKind = spec_pure(depth: int) | plain
+
+function depthOf(k: CallKind): int
+{
+  match k {
+    case spec_pure(i_k_depth) =>
+      if (i_k_depth >= 0) then
+        i_k_depth
+      else
+        0
+    case plain =>
+      0
+  }
+}
+
+lemma depthOf_ensures(k: CallKind)
+  ensures (depthOf(k) >= 0)
+{
+}
+
+function specPure(depth: int): CallKind
+{
+  spec_pure(depth)
+}
+
+function plain(): CallKind
+{
+  CallKind.plain
+}

examples/ctorName.ts

@@ -0,0 +1,36 @@
+/**
+ * Union tags that are not valid identifiers.
+ *
+ * A discriminated union's tag is a source string and may contain characters no
+ * identifier has (`"spec-pure"`). The declaration, the patterns, and the
+ * constructor *applications* must all spell it the same sanitized way —
+ * `spec_pure` in Dafny, `«spec-pure»` in Lean. Applications are the easy one to
+ * miss: they go through a different emit path than declarations and patterns.
+ */
+
+type CallKind =
+  | { kind: "spec-pure"; depth: number }
+  | { kind: "plain" };
+
+export function depthOf(k: CallKind): number {
+  //@ verify
+  //@ ensures \result >= 0
+  switch (k.kind) {
+    case "spec-pure":
+      return k.depth >= 0 ? k.depth : 0;
+    case "plain":
+      return 0;
+  }
+}
+
+// Populated constructor application — the case the sanitizer originally missed.
+export function specPure(depth: number): CallKind {
+  //@ verify
+  return { kind: "spec-pure", depth };
+}
+
+// Nullary constructor application, for contrast.
+export function plain(): CallKind {
+  //@ verify
+  return { kind: "plain" };
+}