[DevChiniwala]

Problem

Distinct optional access paths can receive the same narrowing binder. Both
a_b and a.b produce the hint _a_b_val; nesting their presence checks
captures the first payload with the second. Both backends then model a
different result from the source program.

Reproduction

interface Box { b?: number }
export function add(a_b: number | undefined, a: Box): number {
  //@ ensures a_b === 3 && a.b === 7 ==> \result === 10
  if (a_b !== undefined) {
    if (a.b !== undefined) return a_b + a.b;
  }
  return -1;
}

Expected

add(3, { b: 7 }) returns 10. Each supported optional presence check must bind
its own path's payload.

Actual

On main at ffc07fcf1e6826b57fad0dde6e8bc2bbfb960ab5, the generated model
adds the inner binder twice and returns 14. Dafny rejects the correct claim
above and verifies the same claim with 14. The generated Lean pure definition
also reduces to 14.

Root cause

Raw and Typed IR preserve both access paths. The first divergence is narrowing:
underscore-joined path hints are not unique, and the existing freshness check
only excludes user names. Two SomeMatch nodes therefore share a binder string
before backend emission.

Fix

Allocate presence binders using the complete raw access path as a memoization
key and a scope-local occupied-name set in CondCtx. Use the existing priming
policy, excluding user names and other narrowing binders. Optional-chain and
map-access binders share the same occupied set within each scope. Functions and
methods have independent registries, and each body's registry is separate from
its contracts. The optional-chain counter retains its existing traversal order.
Keep detection stateless for
resolve, and thread the context through the presence materializers. Early-return
detector deduplication uses the allocated identity rather than the flattened hint.

Regression

Eight focused tests cover colliding variable/field paths, field/field paths,
user-name collisions, optional-chain counter collisions, early-return detectors,
determinism, isolated contexts, contract/body separation, and independent
function/method names. On unchanged main, four original tests fail and the
determinism control passes. Three additional scope regressions fail at the
initial PR commit 1d08722; all eight pass at ebdc4d5. The six-function
fixture includes five Dafny ensures lemmas and pure/mutable-body lowering.

Validation of the scope follow-up (ebdc4d5)

• Build, tools typecheck, and examples typecheck pass.
• Complete Linux unit suite: 297 passed, zero failed or skipped.
• tools/test-fixtures.sh passes, retaining the original collision regressions.
• Dafny and Lean example regeneration produces no tracked or untracked generated-file drift.
• The failing external balanced-match-lemmascript case study at
  50747512cbe087cb60b5a28569231c9a007f8fce passes the same tools/check.sh dafny
  command as CI and preserves its generated and handwritten proof files exactly.
  Its 500-second verification timeout selects the repository's generation-only
  check; this is not a claim of a full local proof run.
• Lean regeneration followed by seven kernel equalities and six Velvet proofs
  passes with the follow-up compiler.
• CI run 40300280228
  at ebdc4d55c51df9b1addc34a2d6b4ebfa79f2e025 requires maintainer approval
  before jobs can run. This is an external gate, not a passing CI result.

The original CI failure came from sharing an occupied-name registry between
\result in the contract and result in the body. The follow-up keeps those
binding scopes separate without weakening the additions-only check or changing
proof files.

Validation before the scope follow-up (1d08722)

WSL Ubuntu 24.04, Node 24.22.1, Dafny 4.11.0, Lean 4.34.0 and Velvet lemma2
at 22ed7829f4a90e786eed9b193d29fe46e61fe949:

• npm run build
• (cd tools && npm run typecheck)
• npm run typecheck:examples
• npx tsx --test tools/tests/*.test.ts — 294 passed, none failed/skipped.
• bash tools/test-fixtures.sh — passed, including five verified regression lemmas.
• bash tools/check.sh dafny examples/*.ts — 71 enabled examples, 469 verified
  members, zero errors; one declared Lean-only example skipped.
• bash regen-dafny.sh --no-verify and bash regen-lean.sh — no existing
  generated/proof drift or new generated example artifacts.
• bash tools/check.sh lean <regression-fixture> — full Lake build passed,
  1129 jobs. Existing linter/deprecation warnings remain.
• Focused lake env lean checks of generated fixture types/definitions and a
  companion proof file — seven kernel equalities and six Velvet proofs passed.
• External pi-lemmascript at 1ec4040cfcd7e20b3039b0abfa05660431aa8458:
  six manifest files, 30 verified members, no tracked artifact drift.
• External flue-lemmascript at 808d87805cc682af0fb510daa1a18651dd4c6842:
  five manifest files, 24 verified members with baseline and fixed compilers,
  no tracked artifact drift.

The correct concrete Dafny claim verifies after the fix; the wrong 14 claim
fails. Lean kernel equalities also check arbitrary payload values.

The Windows Node 25.9.0 baseline already has CLI-loader unit failures involving
absolute Windows paths. Linux runs the complete suite successfully. The full
external CI matrix was not run locally.

Backend impact

Dafny: distinct nested payload binders; the false source claim is rejected.
Lean: the same shared-IR correction; generated definitions and Velvet methods
pass focused checks. Neither emitter changes.

Compatibility

No new syntax, purity classification, type representation or assumption is
introduced. Existing examples and both tested case studies regenerate unchanged.
Only conflicting generated names need primes. Proofs relying on the captured
value may fail after regeneration; this is the intended semantic correction.

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

Fixed the balanced-match generated-line failure in ebdc4d5. Contracts and function bodies now allocate binders independently, preserving existing proof names while retaining collision protection.

Validation: 297 unit tests, the fixture suite, build/typechecks, unchanged Dafny and Lean regeneration, and the balanced-match CI generation check all pass. Seven Lean kernel equalities and six Velvet proofs also pass. The balanced-match command uses its configured generation-only mode; I have not claimed a full local proof run.

The new CI run is awaiting workflow approval. Could a maintainer approve it so the full matrix can run on this commit?

[namin]

Thank you!