[DevChiniwala]

The Dafny emitter drops the position argument of includes, startsWith, and endsWith. For example, TypeScript's "a".includes("a", 1) is false, while its current model searches from zero. Explicit indexOf positions above the string length also return -1 for an empty needle instead of the string length. The Lean emitter silently drops a positional indexOf argument even though this form is documented as unsupported.

Preserve the Dafny positions, clamp integer bounds to the string length, and reject positional indexOf in Lean. Default-position emission stays unchanged. Add executable TypeScript controls, emitter regressions, a real Dafny fixture, and document the backend behavior.

Validation on main b9c8f65: the new regression suite fails three tests, and the unchanged model verifies three reversed postconditions that disagree with TypeScript execution. With the fix, all 297 unit tests and the fixture suite pass, the correct Dafny postconditions verify, both regeneration checks produce no generated-file drift, and the Lean build passes all 1,129 jobs. An additional compiled-Dafny differential run agrees with JavaScript for 700 results across search methods, bounds, empty strings, and needles.

The follow-up emits only the search helpers a program uses. The compatible balanced-match artifacts are in midspiral/balanced-match-lemmascript#1: 2,255 Dafny obligations verify with zero errors, all 19 package tests and the typecheck pass, and the original method contract is unchanged. Integration CI needs the upstream case-study staging ref described there.

[Copilot]

Copilot was unable to review this pull request because the user who requested the review has insufficient remaining quota.

An organization owner can choose the repository organization as the billing source for reviews requested by members with a paid Copilot license. Learn about Copilot code review billing.

[DevChiniwala]

The compatible case-study update is ready in midspiral/balanced-match-lemmascript#1. Against this PR's current compiler commit 29650a9, the complete Dafny proof verifies 2,255 obligations with zero errors; all 19 package tests, typechecking, and the generation/additions-only check pass. The proof derives its loop fact from the existing precondition and adds no input requirements.

To exercise the existing staging override, please create branch lemmascript-fix/string-search-positions in midspiral/balanced-match-lemmascript at 51ce9eebd631598374b8ebf68bf5da85d0636aa2, then rerun the failed balanced-match case-study job. The fork account has no upstream push permission, so creating that ref requires a maintainer. The companion remains draft for coordinated staging and landing.

[namin]

Thanks for all your contributions. I appreciate that they were well-organized and clear-cut. Happy to see more contributions from you!

[DevChiniwala]

Thank you for reviewing and merging these contributions. I’ve opened two focused follow-ups: #233 rejects unsupported some callback parameters, and #234 prevents rest-parameter argument collection from being lost during extraction. Each includes regressions that fail on unchanged main and a real Dafny reproduction of a false JavaScript postcondition. The local test and fixture suites pass; upstream CI is still running, and I’ll follow up on its results and any review feedback.