From c51b7b7b3f368d2276ff329879c1993a714fe0df Mon Sep 17 00:00:00 2001 From: Dev Chiniwala Date: Wed, 28 Oct 2026 13:40:20 +0530 Subject: [PATCH 1/2] fix: reject indexed some callbacks in Dafny Reject extra Array.some callback parameters instead of allowing their uses to capture outer variables in the element-only existential. Keep unary callbacks and captured variables unchanged, document the boundary, and cover the unsupported callback forms with regressions. --- SPEC.md | 2 +- tools/src/dafny-emit.ts | 5 ++ tools/tests/some-callback-arity.test.ts | 65 +++++++++++++++++++++++++ 3 files changed, 71 insertions(+), 1 deletion(-) create mode 100644 tools/tests/some-callback-arity.test.ts diff --git a/SPEC.md b/SPEC.md index e800a8d..1b6804d 100644 --- a/SPEC.md +++ b/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` (callbacks declare at most one element parameter; index/array parameters are rejected) | | `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) | diff --git a/tools/src/dafny-emit.ts b/tools/src/dafny-emit.ts index b7bccb1..213f413 100644 --- a/tools/src/dafny-emit.ts +++ b/tools/src/dafny-emit.ts @@ -420,6 +420,11 @@ function emitExpr(e: Expr): string { // predicate (e.g. a function reference). if (e.method === "some") { const lam = e.args[0]; + // The existential binds only the element. Dropping another callback + // parameter could make its uses resolve to a same-named outer value. + if (lam.kind === "lambda" && lam.params.length > 1) { + throw new Error("Dafny array.some callbacks support at most one element parameter; index and array callback parameters are not supported."); + } 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); diff --git a/tools/tests/some-callback-arity.test.ts b/tools/tests/some-callback-arity.test.ts new file mode 100644 index 0000000..37cf892 --- /dev/null +++ b/tools/tests/some-callback-arity.test.ts @@ -0,0 +1,65 @@ +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 refuses unsupported some callback parameters: ${name}`, () => { + assert.throws(() => generate(text), /some.*(index|callback|parameter)/i); + }); +} + +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/); +}); From a4faef3bc3399e8dbe756dabc47b5d06531a0221 Mon Sep 17 00:00:00 2001 From: Dev Chiniwala Date: Thu, 29 Oct 2026 14:08:38 +0530 Subject: [PATCH 2/2] fix: bind indexed some callback arguments in Dafny Range over valid positions and bind the element, index and source array without capturing receiver names. Cover empty arrays and retain proof obligations for both valid results and the original false postcondition. --- SPEC.md | 2 +- .../some-callback-false-postcondition.ts | 5 ++ tools/fixtures/some-callback-parameters.dfy | 60 +++++++++++++++++++ tools/fixtures/some-callback-parameters.ts | 26 ++++++++ tools/src/dafny-emit.ts | 20 ++++++- tools/test-fixtures.sh | 11 ++++ tools/tests/some-callback-arity.test.ts | 33 +++++++++- 7 files changed, 151 insertions(+), 6 deletions(-) create mode 100644 tools/fixtures/some-callback-false-postcondition.ts create mode 100644 tools/fixtures/some-callback-parameters.dfy create mode 100644 tools/fixtures/some-callback-parameters.ts diff --git a/SPEC.md b/SPEC.md index 1b6804d..76182a3 100644 --- a/SPEC.md +++ b/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` (callbacks declare at most one element parameter; index/array parameters are rejected) | +| `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) | diff --git a/tools/fixtures/some-callback-false-postcondition.ts b/tools/fixtures/some-callback-false-postcondition.ts new file mode 100644 index 0000000..14fef6f --- /dev/null +++ b/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); +} diff --git a/tools/fixtures/some-callback-parameters.dfy b/tools/fixtures/some-callback-parameters.dfy new file mode 100644 index 0000000..e477781 --- /dev/null +++ b/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 := [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): bool +{ + (var s_some: seq := [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) + ensures (arrayArgument(items) == true) +{ + assert [7][0] == 7; +} + +function duplicateValues(): bool +{ + (var s_some: seq := [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 := []; 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, i_some: int): bool + requires (|s_some| > 1) +{ + (var s_some': seq := 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, i_some: int) + requires (|s_some| > 1) + ensures (receiverScope(s_some, i_some) == true) +{ + assert s_some[1..][0] == s_some[1]; +} diff --git a/tools/fixtures/some-callback-parameters.ts b/tools/fixtures/some-callback-parameters.ts new file mode 100644 index 0000000..096fc29 --- /dev/null +++ b/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); +} diff --git a/tools/src/dafny-emit.ts b/tools/src/dafny-emit.ts index 213f413..92ceaf7 100644 --- a/tools/src/dafny-emit.ts +++ b/tools/src/dafny-emit.ts @@ -420,10 +420,24 @@ function emitExpr(e: Expr): string { // predicate (e.g. a function reference). if (e.method === "some") { const lam = e.args[0]; - // The existential binds only the element. Dropping another callback - // parameter could make its uses resolve to a same-named outer value. + // 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) { - throw new Error("Dafny array.some callbacks support at most one element parameter; index and array callback parameters are not supported."); + 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") { diff --git a/tools/test-fixtures.sh b/tools/test-fixtures.sh index 4e5e957..ab3e74c 100755 --- a/tools/test-fixtures.sh +++ b/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" diff --git a/tools/tests/some-callback-arity.test.ts b/tools/tests/some-callback-arity.test.ts index 37cf892..751f23f 100644 --- a/tools/tests/some-callback-arity.test.ts +++ b/tools/tests/some-callback-arity.test.ts @@ -41,11 +41,40 @@ for (const [name, text] of [ return [7].some((value, index, items) => items.length === 0); }`], ] as const) { - test(`Dafny refuses unsupported some callback parameters: ${name}`, () => { - assert.throws(() => generate(text), /some.*(index|callback|parameter)/i); + 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 :=/); + 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 {