[DevChiniwala]

An inline arrow callback's rest parameter currently loses its ... marker during extraction. The backends receive an ordinary parameter instead of an array collecting the callback arguments. This can verify a false JavaScript postcondition:

//@ ensures \result[0] === 1
export function argumentCounts(): number[] {
  return [[7]].map((...args: (number | number[] | number[][])[]) => args.length);
}

JavaScript returns [3]: map passes the element, index, and source array. On unchanged main dd0847e, the generated Dafny instead binds args to the element [7], giving length 1. The real CLI verifies the false postcondition with 3 verified, 0 errors, without proof additions or assumptions.

Reject rest parameters in expression arrow lambdas during extraction with an explicit diagnostic, and document the unsupported boundary. Ordinary callback parameters and object destructuring remain supported. Named variadic function declarations and top-level arrow declarations retain their existing rest-grouping metadata.

Validation:

• The seven focused tests have 4 failures / 3 passes on unchanged main and 7 passes with the fix.
• Build, tools typecheck, example typecheck, and all 320 unit tests pass.
• The full fixture suite passes. Lean and Dafny example regeneration produces no artifact changes.
• The real CLI rejects the reproduction during extraction, before verification.

Prepared with Codex assistance. The source runtime result, false proof on main, and passing-after checks were executed locally and inspected.

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

[namin]

This seems rather reasonable, but still wondering whether we can support rather than reject?

[DevChiniwala]

Yes, it is feasible, but it needs argument collection at the callback call site. For map, (...args) receives [element, index, sourceArray]; those entries can have different types, so preserving the rest parameter's name alone would still model the wrong program.

The sound follow-up is to preserve the rest binding in the lambda IR and construct its actual argument array in both backends. Its regression should verify args.length === 3, while continuing to reject the false === 1 postcondition. Would you prefer landing this soundness guard first and adding that support in a separate change?