fix: bind indexed some callbacks in Dafny

SPEC.md

@@ -495,7 +495,7 @@ With `local`, `SeqFilter` and `SeqAll` replace the corresponding
 | `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.some((x) => e)` | `arr.any (fun x => e)` | `exists x :: x in arr && e`; indexed inline callbacks range over positions and bind the element, index, and source array |
 | `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)` | `SeqFind(arr, (x) => e)` (preamble) |

tools/fixtures/some-callback-false-postcondition.ts

@@ -0,0 +1,5 @@
+export function capturedIndex(index: number): boolean {
+  //@ requires index === 1
+  //@ ensures \result === true
+  return [7].some((value, index) => index === 1);
+}

tools/fixtures/some-callback-parameters.dfy

@@ -0,0 +1,60 @@
+// Generated by lsc from some-callback-parameters.ts
+
+type Unknown(==, 0)
+
+function capturedIndex(index: int): bool
+  requires (index == 1)
+{
+  (var s_some: seq<nat> := [7]; exists i_some {:trigger s_some[i_some]} :: 0 <= i_some < |s_some| && (var value := s_some[i_some]; var index := i_some; (index == 1)))
+}
+
+lemma capturedIndex_ensures(index: int)
+  requires (index == 1)
+  ensures (capturedIndex(index) == false)
+{
+}
+
+function arrayArgument(items: seq<int>): bool
+{
+  (var s_some: seq<nat> := [7]; exists i_some {:trigger s_some[i_some]} :: 0 <= i_some < |s_some| && (var value := s_some[i_some]; var index := i_some; var items := s_some; ((|items| == 1) && (items[index] == value))))
+}
+
+lemma arrayArgument_ensures(items: seq<int>)
+  ensures (arrayArgument(items) == true)
+{
+  assert [7][0] == 7;
+}
+
+function duplicateValues(): bool
+{
+  (var s_some: seq<nat> := [7, 7]; exists i_some {:trigger s_some[i_some]} :: 0 <= i_some < |s_some| && (var value := s_some[i_some]; var index := i_some; var items := s_some; ((index == 1) && (items[index] == value))))
+}
+
+lemma duplicateValues_ensures()
+  ensures (duplicateValues() == true)
+{
+  assert [7, 7][1] == 7;
+}
+
+function emptyArray(): bool
+{
+  (var s_some: seq<Unknown> := []; exists i_some {:trigger s_some[i_some]} :: 0 <= i_some < |s_some| && (var value := s_some[i_some]; var index := i_some; (index == 0)))
+}
+
+lemma emptyArray_ensures()
+  ensures (emptyArray() == false)
+{
+}
+
+function receiverScope(s_some: seq<int>, i_some: int): bool
+  requires (|s_some| > 1)
+{
+  (var s_some': seq<int> := s_some[1..]; exists i_some' {:trigger s_some'[i_some']} :: 0 <= i_some' < |s_some'| && (var s_some := s_some'[i_some']; var i_some := i_some'; var items := s_some'; ((i_some == 0) && (items[i_some] == s_some))))
+}
+
+lemma receiverScope_ensures(s_some: seq<int>, i_some: int)
+  requires (|s_some| > 1)
+  ensures (receiverScope(s_some, i_some) == true)
+{
+  assert s_some[1..][0] == s_some[1];
+}

tools/fixtures/some-callback-parameters.ts

@@ -0,0 +1,26 @@
+export function capturedIndex(index: number): boolean {
+  //@ requires index === 1
+  //@ ensures \result === false
+  return [7].some((value, index) => index === 1);
+}
+
+export function arrayArgument(items: number[]): boolean {
+  //@ ensures \result === true
+  return [7].some((value, index, items) => items.length === 1 && items[index] === value);
+}
+
+export function duplicateValues(): boolean {
+  //@ ensures \result === true
+  return [7, 7].some((value, index, items) => index === 1 && items[index] === value);
+}
+
+export function emptyArray(): boolean {
+  //@ ensures \result === false
+  return ([] as number[]).some((value, index) => index === 0);
+}
+
+export function receiverScope(s_some: number[], i_some: number): boolean {
+  //@ requires s_some.length > 1
+  //@ ensures \result === true
+  return s_some.slice(1).some((s_some, i_some, items) => i_some === 0 && items[i_some] === s_some);
+}

tools/src/dafny-emit.ts

@@ -420,6 +420,25 @@ function emitExpr(e: Expr): string {
         // predicate (e.g. a function reference).
         if (e.method === "some") {
           const lam = e.args[0];
+          // Indexed callbacks range over positions, not just values. Bind the
+          // receiver once outside the callback's scope so its parameter names
+          // cannot capture it, and pass all three JavaScript callback arguments.
+          if (lam.kind === "lambda" && lam.params.length > 1) {
+            if (lam.params.length > 3) {
+              throw new Error("Dafny array.some callbacks support at most the element, index, and array parameters.");
+            }
+            const taken = (n: string): boolean => usesName(e.obj, n) || usesName(lam, n) ||
+              lam.params.some(pp => pp.name === n) || usesNameInStmts(lam.body, n);
+            const seq = escapeName(freshNameWhere("s_some", taken));
+            const idx = escapeName(freshNameWhere("i_some", n => taken(n) || escapeName(n) === seq));
+            const values = [`${seq}[${idx}]`, idx, seq];
+            const bindings = lam.params.map((pp, i) => `var ${escapeName(pp.name)} := ${values[i]}; `).join("");
+            if (lam.body.length === 1 && lam.body[0].kind === "return") {
+              const predicate = `${bindings}${emitExpr(lam.body[0].value)}`;
+              return `(var ${seq}: ${tyToDafny(e.objTy)} := ${obj}; exists ${idx} {:trigger ${seq}[${idx}]} :: 0 <= ${idx} < |${seq}| && (${predicate}))`;
+            }
+            throw new Error("Unsupported: multi-statement lambda in Dafny");
+          }
           let p: string, body: string;
           if (lam.kind === "lambda" && lam.body.length === 1 && lam.body[0].kind === "return") {
             const cb = comprehensionBinder(lam, lam.body[0].value, e.obj);

tools/test-fixtures.sh

@@ -47,6 +47,9 @@ cp tools/fixtures/deterministic-extern-equality.ts "$fixture_dir/deterministic.t
 cp tools/fixtures/impure-extern-equality.ts "$fixture_dir/impure.ts"
 cp tools/fixtures/negated-array-ternary.ts "$fixture_dir/negated-array-ternary.ts"
 cp tools/fixtures/string-search-positions.ts "$fixture_dir/string-search-positions.ts"
+cp tools/fixtures/some-callback-parameters.ts "$fixture_dir/some-callback-parameters.ts"
+cp tools/fixtures/some-callback-parameters.dfy "$fixture_dir/some-callback-parameters.dfy"
+cp tools/fixtures/some-callback-false-postcondition.ts "$fixture_dir/some-callback-false-postcondition.ts"
 cp examples/safeSlice.ts "$fixture_dir/legacy-safe-slice.ts"
 cp -R tools/fixtures/utf16-project "$fixture_dir/utf16-project"
 cp tools/fixtures/optional-binder-collisions.ts "$fixture_dir/optional-binder-collisions.ts"
@@ -62,6 +65,14 @@ fi
 npx tsx tools/src/lsc.ts check --backend=dafny --time-limit=10 "$fixture_dir/deterministic.ts"
 npx tsx tools/src/lsc.ts check --backend=dafny --time-limit=10 "$fixture_dir/negated-array-ternary.ts"
 npx tsx tools/src/lsc.ts check --backend=dafny --time-limit=10 "$fixture_dir/string-search-positions.ts"
+npx tsx tools/src/lsc.ts check --backend=dafny --time-limit=10 "$fixture_dir/some-callback-parameters.ts"
+expect_failure \
+  "Dafny verified a false postcondition using an outer callback parameter" \
+  npx tsx tools/src/lsc.ts check --backend=dafny --time-limit=10 "$fixture_dir/some-callback-false-postcondition.ts"
+if [ ! -f "$fixture_dir/some-callback-false-postcondition.dfy.gen" ]; then
+  echo "ERROR: indexed callback was rejected instead of emitted for verification"
+  exit 1
+fi
 expect_failure \
   "Dafny equated two calls to an impure extern" \
   npx tsx tools/src/lsc.ts check --backend=dafny --time-limit=10 "$fixture_dir/impure.ts"

tools/tests/some-callback-arity.test.ts

@@ -0,0 +1,94 @@
+import { test } from "node:test";
+import assert from "node:assert/strict";
+import { Project, ScriptTarget } from "ts-morph";
+import { extractModule } from "../src/extract.ts";
+import { resolveModule } from "../src/resolve.ts";
+import { narrowModule } from "../src/narrow.ts";
+import { transformModuleDafny } from "../src/transform.ts";
+import { emitDafnyFile } from "../src/dafny-emit.ts";
+
+function generate(text: string): string {
+  const project = new Project({ compilerOptions: { strict: true,
+    target: ScriptTarget.ESNext, lib: ["lib.esnext.d.ts"], types: [], skipLibCheck: true } });
+  const source = project.createSourceFile("some.ts", text);
+  assert.deepEqual(project.getPreEmitDiagnostics(), [], "input must be valid TypeScript");
+  const { typesFile, defFile } = transformModuleDafny(narrowModule(resolveModule(extractModule(source))));
+  return emitDafnyFile({ ...defFile, decls: [...(typesFile?.decls ?? []), ...defFile.decls] });
+}
+
+test("JavaScript some binds the index rather than a same-named outer variable", () => {
+  const capturedIndex = (index: number) => [7].some((value, index) => index === 1);
+  assert.equal(capturedIndex(1), false);
+  assert.equal(capturedIndex(0), false);
+  assert.equal([7].some(value => value === 7), true);
+});
+
+for (const [name, text] of [
+  ["index shadows an outer parameter", `
+    export function capturedIndex(index: number): boolean {
+      return [7].some((value, index) => index === 1);
+    }`],
+  ["index in a block callback", `
+    export function capturedIndex(index: number): boolean {
+      return [7].some((value, index) => { return index === 1; });
+    }`],
+  ["index without an outer binding", `
+    export function usesIndex(): boolean {
+      return [7].some((value, index) => index === 0);
+    }`],
+  ["array parameter shadows an outer parameter", `
+    export function capturedArray(items: number[]): boolean {
+      return [7].some((value, index, items) => items.length === 0);
+    }`],
+] as const) {
+  test(`Dafny supports some callback parameters: ${name}`, () => {
+    const output = generate(text);
+    assert.match(output, /exists \S+ \{:trigger [^}]+\} :: 0 <= \S+ < \|\S+\| &&/);
+    assert.match(output, /var index :=/);
+  });
+}
+
+test("indexed some preserves outer names and binds a computed receiver once", () => {
+  const output = generate(`
+    export function collision(s_some: number[], i_some: number): boolean {
+      return s_some.slice(1).some((s_some, i_some, items) => items[i_some] === s_some && i_some === 0);
+    }`);
+  assert.match(output, /var s_some': seq<int> :=/);
+  assert.match(output, /exists i_some' \{:trigger/);
+  assert.match(output, /var s_some := s_some'\[i_some'\]/);
+  assert.match(output, /var i_some := i_some'/);
+  assert.match(output, /var items := s_some'/);
+});
+
+test("indexed some visits duplicate values at distinct indices and never visits an empty array", () => {
+  assert.equal([7, 7].some((value, index, items) => index === 1 && items[index] === value), true);
+  assert.equal([7].some((value, index, items) => index === 1 && items[index] === value), false);
+  assert.equal(([] as number[]).some((value, index, items) => index === 0), false);
+  const output = generate(`
+    export function duplicate(): boolean {
+      return [7, 7].some((value, index, items) => index === 1 && items[index] === value);
+    }
+    export function empty(): boolean {
+      return ([] as number[]).some((value, index) => index === 0);
+    }`);
+  assert.match(output, /var items :=/);
+  assert.doesNotMatch(output, /exists value :: value in/);
+});
+
+test("Dafny still accepts unary and parameterless some callbacks", () => {
+  const output = generate(`
+    export function unary(xs: number[], limit: number): boolean {
+      return xs.some(value => value > limit);
+    }
+    export function parameterless(xs: number[], x: number): boolean {
+      return xs.some(() => x > 0);
+    }
+    export function named(xs: number[], predicate: (value: number) => boolean): boolean {
+      return xs.some(predicate);
+    }`);
+  assert.match(output, /exists value :: value in xs && \(value > limit\)/);
+  const parameterless = output.match(/exists (\S+) :: \1 in xs && \(x > 0\)/);
+  assert.ok(parameterless, "parameterless callbacks must preserve the outer x");
+  assert.notEqual(parameterless[1], "x");
+  assert.match(output, /predicate/);
+});