[DevChiniwala]

Dafny's element-only some lowering can silently resolve an index or source-array callback parameter to a same-named outer variable. That can verify a false JavaScript postcondition. Support two- and three-parameter inline callbacks by ranging over valid positions, evaluating the receiver once, and binding the element, index and source array in the callback's scope.

Fresh internal names preserve receiver and captured-variable scope. A typed receiver binding handles empty arrays, and an explicit receiver-access trigger supports strict Dafny verification. The operation table documents indexed callbacks.

Validation:

• The eight focused tests have six failures and two passes against the previously published rejection-only commit; all eight pass with this change.
• All 321 unit tests, build, tools and example typechecks, and the full fixture suite pass.
• Five positive examples cover outer-name shadowing, duplicate values, empty arrays, and a computed receiver. Their proof companion adds only three ordinary witness assertions: Dafny verifies 12 obligations with no errors or warnings. The original false postcondition now emits successfully and fails verification.
• Lean and Dafny example regeneration changes no artifacts.

Prepared with Codex assistance; the JavaScript behavior, generated output, positive proofs and negative verification check were executed locally.

[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]

CI update for c51b7b7: 39 of 40 jobs pass. The remaining colorwheel Lean job has remained in setup-lean since 08:10 UTC, before regeneration starts; its downloadable log is not available yet. The same job completed successfully in the all-green run for #234.

Could a maintainer restart that setup job? My fork-contributor permissions do not allow cancelling or rerunning upstream Actions. I also applied #233 and #234 together locally: build, both typechecks, and all 326 unit tests pass.

[namin]

Is there a way we could support rather than reject?

[DevChiniwala]

Implemented support in a4faef3bc3: indexed inline callbacks now bind the element, index and source array, with the receiver evaluated once outside their scope. All 321 unit tests, the fixture suite, build and typechecks pass; regeneration changes no examples. The positive proof fixture verifies 12 obligations without warnings, and the original false postcondition now fails verification after successful emission.