fix: preserve explicit string search positions

SPEC.md

@@ -474,7 +474,7 @@ With `local`, `SeqFilter` and `SeqAll` replace the corresponding
 | `c ? a : b` | `if c then a else b` | `if c then a else b` |
 | `opt ? f(opt) : undefined` | match on Some/None | `match opt { case Some(v) => Some(f(v)) case None => None }` |
 | `s.indexOf(sub)` | `JSString.indexOf s sub` | `StringIndexOf(s, sub)` |
-| `s.indexOf(sub, from)` | — | `StringIndexOfFrom(s, sub, from)` (negative `from` clamps to 0) |
+| `s.indexOf(sub, from)` | — (rejected) | `StringIndexOfFrom(s, sub, StringSearchPosition(s, from))`; position clamps to `[0, \|s\|]` |
 | `s.slice(start, end)` | `JSString.slice s start end` | `s[start..end]` |
 | `s.substring(start)` / `s.substring(start, end)` | — | `s[start..]` / `s[start..end]` |
 | `s.charCodeAt(i)` | — | `(s[i] as int)` |
@@ -486,6 +486,9 @@ With `local`, `SeqFilter` and `SeqAll` replace the corresponding
 | `s.includes(sub)` | — | `StringIndexOf(s, sub) >= 0` |
 | `s.startsWith(p)` | — | `\|s\| >= \|p\| && s[..\|p\|] == p` |
 | `s.endsWith(p)` | — | `\|s\| >= \|p\| && s[\|s\|-\|p\|..] == p` |
+| `s.includes(sub, from)` | — | Search from the clamped position, including an empty needle at the end |
+| `s.startsWith(p, from)` | — | `StringStartsWithAt(s, p, from)`; position clamps to `[0, \|s\|]` |
+| `s.endsWith(p, end)` | — | `StringEndsWithAt(s, p, end)`; exclusive end clamps to `[0, \|s\|]` |
 | `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) }`) |

SPEC_DAFNY.md

@@ -113,6 +113,8 @@ The Dafny emitter auto-injects helper functions when needed. Each is emitted at
 | Helper | When | Purpose |
 |--------|------|---------|
 | `StringIndexOf` | `s.indexOf(sub)`, `s.indexOf(sub, from)`, `s.includes(sub)` | Recursive string search (also provides `StringIndexOfFrom`) |
+| `StringSearchPosition` | Explicit positions in `indexOf`, `includes`, `startsWith`, `endsWith` | Clamp integer positions to the string length |
+| `StringStartsWithAt` / `StringEndsWithAt` | Explicit positions in `startsWith` / `endsWith`, respectively | Test a prefix or suffix at the clamped position |
 | `StringSplit` | `s.split(d)` | Axiomatic split (`1 <= \|res\| <= \|s\| + 1`) |
 | `StringTrim` | `s.trim()` / `s.trimEnd()` / `s.trimStart()` | Trim (also provides `StringTrimRight` / `StringTrimLeft`); strips the full ECMAScript whitespace set via `IsJSWhitespace`, not just `' '` |
 | `StringToLower` / `StringToUpper` | `s.toLowerCase()` / `s.toUpperCase()` | Case folding |

tools/fixtures/string-search-positions.ts

@@ -0,0 +1,45 @@
+//@ backend dafny
+
+export function includesAt(text: string, needle: string, position: number): boolean {
+  return text.includes(needle, position);
+}
+
+export function startsAt(text: string, needle: string, position: number): boolean {
+  return text.startsWith(needle, position);
+}
+
+export function endsAt(text: string, needle: string, position: number): boolean {
+  return text.endsWith(needle, position);
+}
+
+export function indexAt(text: string, needle: string, position: number): number {
+  return text.indexOf(needle, position);
+}
+
+export function positionedPredicates(): boolean {
+  //@ ensures \result === true
+  return !"a".includes("a", 1)
+    && "ab".includes("b", 1)
+    && "ab".startsWith("b", 1)
+    && !"ab".startsWith("a", 1)
+    && "ab".endsWith("a", 1)
+    && !"ab".endsWith("b", 1);
+}
+
+export function clampedPredicates(): boolean {
+  //@ ensures \result === true
+  return "abc".includes("a", -10)
+    && !"abc".includes("a", 10)
+    && "abc".includes("", 10)
+    && "abc".startsWith("a", -10)
+    && !"abc".startsWith("a", 10)
+    && "abc".startsWith("", 10)
+    && "abc".endsWith("", -10)
+    && !"abc".endsWith("a", -10)
+    && "abc".endsWith("c", 10);
+}
+
+export function emptyNeedlePastEnd(): number {
+  //@ ensures \result === 3
+  return "abc".indexOf("", 10);
+}

tools/src/dafny-emit.ts

@@ -442,7 +442,10 @@ function emitExpr(e: Expr): string {
       if (ty === "string") {
         if (e.method === "indexOf") {
           needPreamble("StringIndexOf");
-          if (args.length === 2) return `StringIndexOfFrom(${obj}, ${args[0]}, ${args[1]})`;
+          if (args.length === 2) {
+            needPreamble("StringSearchPosition");
+            return `StringIndexOfFrom(${obj}, ${args[0]}, StringSearchPosition(${obj}, ${args[1]}))`;
+          }
           return `StringIndexOf(${obj}, ${args[0]})`;
         }
         if (e.method === "split")   { needPreamble("StringSplit"); return `StringSplit(${obj}, ${args[0]})`; }
@@ -466,14 +469,35 @@ function emitExpr(e: Expr): string {
           if (args.length === 1) return `${obj}[${args[0]}..]`;
           return `${obj}[${args[0]}..${args[1]}]`;
         }
-        if (e.method === "endsWith") return `(|${obj}| >= |${args[0]}| && ${obj}[|${obj}|-|${args[0]}|..] == ${args[0]})`;
+        if (e.method === "endsWith") {
+          if (args.length === 2) {
+            needPreamble("StringSearchPosition");
+            needPreamble("StringEndsWithAt");
+            return `StringEndsWithAt(${obj}, ${args[0]}, ${args[1]})`;
+          }
+          return `(|${obj}| >= |${args[0]}| && ${obj}[|${obj}|-|${args[0]}|..] == ${args[0]})`;
+        }
         if (e.method === "trim")    { needPreamble("StringTrim"); return `StringTrim(${obj})`; }
         if (e.method === "trimEnd") { needPreamble("StringTrim"); return `StringTrimRight(${obj})`; }
         if (e.method === "trimStart") { needPreamble("StringTrim"); return `StringTrimLeft(${obj})`; }
         if (e.method === "toLowerCase") { needPreamble("StringToLower"); return `StringToLower(${obj})`; }
         if (e.method === "toUpperCase") { needPreamble("StringToUpper"); return `StringToUpper(${obj})`; }
-        if (e.method === "includes") { needPreamble("StringIndexOf"); return `(StringIndexOf(${obj}, ${args[0]}) >= 0)`; }
-        if (e.method === "startsWith") return `(|${obj}| >= |${args[0]}| && ${obj}[..|${args[0]}|] == ${args[0]})`;
+        if (e.method === "includes") {
+          needPreamble("StringIndexOf");
+          if (args.length === 2) {
+            needPreamble("StringSearchPosition");
+            return `(StringIndexOfFrom(${obj}, ${args[0]}, StringSearchPosition(${obj}, ${args[1]})) >= 0)`;
+          }
+          return `(StringIndexOf(${obj}, ${args[0]}) >= 0)`;
+        }
+        if (e.method === "startsWith") {
+          if (args.length === 2) {
+            needPreamble("StringSearchPosition");
+            needPreamble("StringStartsWithAt");
+            return `StringStartsWithAt(${obj}, ${args[0]}, ${args[1]})`;
+          }
+          return `(|${obj}| >= |${args[0]}| && ${obj}[..|${args[0]}|] == ${args[0]})`;
+        }
         if (e.method === "charCodeAt") return `(${obj}[${args[0]}] as int)`;
         if (e.method === "repeat") { needPreamble("StringRepeat"); return `StringRepeat(${obj}, ${args[0]})`; }
       }
@@ -1220,6 +1244,24 @@ function SafeSlice<T>(s: seq<T>, lo: int, hi: int): seq<T>
   if hi' < lo' then [] else s[lo'..hi']
 }`;
 
+const STRING_SEARCH_POSITION = `function StringSearchPosition(s: string, position: int): nat
+  ensures StringSearchPosition(s, position) <= |s|
+{
+  if position < 0 then 0 else if position > |s| then |s| else position
+}`;
+
+const STRING_STARTS_WITH_AT = `function StringStartsWithAt(s: string, sub: string, position: int): bool
+{
+  var start := StringSearchPosition(s, position);
+  |sub| <= |s| - start && s[start..start + |sub|] == sub
+}`;
+
+const STRING_ENDS_WITH_AT = `function StringEndsWithAt(s: string, sub: string, position: int): bool
+{
+  var end := StringSearchPosition(s, position);
+  |sub| <= end && s[end - |sub|..end] == sub
+}`;
+
 const STRING_INDEX_OF = `function StringIndexOf(s: string, sub: string): int
   ensures StringIndexOf(s, sub) == -1
        || (0 <= StringIndexOf(s, sub) <= |s| - |sub| && s[StringIndexOf(s, sub)..StringIndexOf(s, sub) + |sub|] == sub)
@@ -1496,6 +1538,9 @@ const PREAMBLE_CODE: [string, string | (() => string)][] = [
   ["SeqJoin", SEQ_JOIN],
   ["SafeSlice", SAFE_SLICE],
   ["StringIndexOf", STRING_INDEX_OF],
+  ["StringSearchPosition", STRING_SEARCH_POSITION],
+  ["StringStartsWithAt", STRING_STARTS_WITH_AT],
+  ["StringEndsWithAt", STRING_ENDS_WITH_AT],
   ["StringSplit", STRING_SPLIT],
   ["SeqSort", SEQ_SORT],
   ["SeqSortBy", SEQ_SORT_BY],

tools/src/lean-emit.ts

@@ -267,7 +267,10 @@ function emitMethodCall(tyKind: string, method: string, monadic: boolean, obj: s
   // String methods
   if (tyKind === "string") {
     _needsJSString = true;
-    if (method === "indexOf") return `JSString.indexOf ${obj} ${args[0]}`;
+    if (method === "indexOf") {
+      if (args.length !== 1) throw new Error("Lean string.indexOf does not support a position argument");
+      return `JSString.indexOf ${obj} ${args[0]}`;
+    }
     if (method === "slice")   return `JSString.slice ${obj} ${args[0]} ${args[1]}`;
   }
   // Map methods

tools/test-fixtures.sh

@@ -46,6 +46,7 @@ trap 'rm -rf "$fixture_dir"' EXIT
 cp tools/fixtures/deterministic-extern-equality.ts "$fixture_dir/deterministic.ts"
 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 examples/safeSlice.ts "$fixture_dir/legacy-safe-slice.ts"
 cp -R tools/fixtures/utf16-project "$fixture_dir/utf16-project"
 cp tools/fixtures/unpaired-surrogate.ts "$fixture_dir/unpaired.ts"
@@ -58,6 +59,7 @@ 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"
 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/string-search-positions.test.ts

@@ -0,0 +1,68 @@
+import { test } from "node:test";
+import assert from "node:assert/strict";
+import { fileURLToPath } from "node:url";
+import { Project, ScriptTarget } from "ts-morph";
+import { includesAt, startsAt, endsAt, positionedPredicates,
+  clampedPredicates, emptyNeedlePastEnd } from "../fixtures/string-search-positions.ts";
+import { extractModule } from "../src/extract.ts";
+import { resolveModule } from "../src/resolve.ts";
+import { narrowModule } from "../src/narrow.ts";
+import { transformModuleDafny, transformModuleLean } from "../src/transform.ts";
+import { emitDafnyFile } from "../src/dafny-emit.ts";
+import { emitLeanFile, resetLeanModule } from "../src/lean-emit.ts";
+import { resolveOptions } from "../src/config.ts";
+
+function sourceModule(text?: string) {
+  const project = new Project({ compilerOptions: { strict: true,
+    target: ScriptTarget.ESNext, lib: ["lib.esnext.d.ts"], types: [], skipLibCheck: true } });
+  const source = text === undefined
+    ? project.addSourceFileAtPath(fileURLToPath(new URL("../fixtures/string-search-positions.ts", import.meta.url)))
+    : project.createSourceFile("search.ts", text);
+  assert.deepEqual(project.getPreEmitDiagnostics(), [], "regressions must be valid TypeScript");
+  return narrowModule(resolveModule(extractModule(source)));
+}
+
+test("source search predicates distinguish positions and clamp integer bounds", () => {
+  assert.equal(positionedPredicates(), true);
+  assert.equal(clampedPredicates(), true);
+  assert.equal(emptyNeedlePastEnd(), 3);
+  for (const text of ["", "abc", "aba"]) {
+    for (const needle of ["", "a", "b", "abc", "abcd"]) {
+      for (const position of [-10, -1, 0, 1, 2, 3, 10]) {
+        assert.equal(includesAt(text, needle, position), text.indexOf(needle, position) >= 0);
+        const bound = Math.max(0, Math.min(position, text.length));
+        assert.equal(startsAt(text, needle, position), text.slice(bound).startsWith(needle));
+        assert.equal(endsAt(text, needle, position), text.slice(0, bound).endsWith(needle));
+      }
+    }
+  }
+});
+
+for (const profile of ["legacy-scalar", "javascript-utf16"] as const) {
+  test(`Dafny preserves each string search position in ${profile} mode`, () => {
+    const { typesFile, defFile } = transformModuleDafny(sourceModule());
+    const output = emitDafnyFile({ ...defFile, decls: [...(typesFile?.decls ?? []), ...defFile.decls] },
+      "search.ts", resolveOptions({ "string-semantics": profile, "dafny-library": "local" }, "test"));
+    assert.match(output, /StringIndexOfFrom\(text, needle, StringSearchPosition\(text, position\)\)/);
+    assert.match(output, /StringStartsWithAt\(text, needle, position\)/);
+    assert.match(output, /StringEndsWithAt\(text, needle, position\)/);
+    assert.match(output, /StringIndexOfFrom\("abc", "", StringSearchPosition\("abc", 10\)\)/);
+  });
+}
+
+test("Lean refuses the unsupported indexOf position instead of discarding it", () => {
+  const { typesFile, defFile } = transformModuleLean(sourceModule(
+    'export function search(s: string, p: number): number { return s.indexOf("a", p); }'));
+  resetLeanModule();
+  assert.throws(() => emitLeanFile({ ...defFile,
+    decls: [...(typesFile?.decls ?? []), ...defFile.decls] }), /indexOf.*position|indexOf.*argument/i);
+});
+
+test("default-position searches do not add positional helpers", () => {
+  const { typesFile, defFile } = transformModuleDafny(sourceModule(`
+    export function ordinary(s: string): boolean {
+      return s.startsWith("a") && s.endsWith("b") && s.includes("a");
+    }`));
+  const output = emitDafnyFile({ ...defFile, decls: [...(typesFile?.decls ?? []), ...defFile.decls] });
+  assert.doesNotMatch(output, /StringSearchPosition|StringStartsWithAt|StringEndsWithAt/);
+});