[DevChiniwala]

Problem

A three-part optional guard can be lowered with a dependent field read outside
the binder that makes it valid. Supported TypeScript then produces a model
that neither backend can use.

Reproduction

type Leaf = { value?: number };
type Box = { inner?: Leaf };
export function pick(box?: Box): number {
  if (box !== undefined && box.inner !== undefined && box.inner.value !== undefined) {
    return box.inner.value;
  }
  return -1;
}

Expected

The presence checks unwrap box, then inner, then value. This matches
TypeScript flow narrowing and the documented &&/path-narrowing contract.

Actual

On ffc07fcf1e6826b57fad0dde6e8bc2bbfb960ab5, the first generated match reads
box.inner.value while box is still optional. Real Dafny reports four
resolution/type errors when the same guard appears in the body and a spec
implication. Ternaries have the same ordering defect.

Root cause

Raw and Typed IR preserve the source guard and its flow facts. Structural
narrowing uses extractConjunct, which checks the immediate right operand
before searching the nested left subtree. For (A && B) && C, it can select
the dependent C before the checks on which it relies.

Fix

Search the left subtree before the right operand. The first matching source
conjunct becomes the outer match; remaining conjuncts retain their relative
order. Move two executable lines and correct the nearby traversal comments.
Guard recognition and purity rules are unchanged.

Regression

Six traversal cases cover both associations, unrelated guards, fallback and
no-match behavior. Integration tests execute source boundary cases, inspect
program/spec binder scope, and check both emissions. Four tests fail before
the fix and four controls already pass; all eight pass afterward.

The standard fixture runner verifies an if-return and a ternary, each with
postconditions for absent root, missing inner/value, and present values.

Validation

• Build, tool typecheck and example typecheck pass.

• All 297 Linux unit tests pass (289 on the unchanged baseline).

• The real-Dafny fixture suite passes; the new fixture reports 2 verified,
  0 errors. The original minimal reproduction also verifies after regen.

• Both regeneration scripts pass with no existing generated/proof-file drift.

• Full Lean build passes with Lean 4.34.0 / Velvet lemma2 (1129 jobs).

• Generated Lean definitions pass kernel checks for all missing-value shapes
  and arbitrary present integers, plus both Velvet correctness proofs.

• pi-lemmascript at 1ec4040cfcd7e20b3039b0abfa05660431aa8458: all six
  manifest Dafny files pass, 30 reported verified members, no artifact drift.

• bash tools/check.sh dafny examples/*.ts: all 71 Dafny-enabled examples
  pass, 469 reported verified members, no artifact drift. One declared
  Lean-only example is skipped; paths are explicit because this source
  checkout has no root manifest.

Backend impact

Dafny and Lean share the corrected match nesting. No emitter changes or new
assumptions are needed. This repairs rejection of valid supported source;
no false-proof path is claimed for this candidate.

Compatibility

No new syntax, options, dependencies or guard classification. Existing
artifacts regenerate without drift. The full external CI matrix was not
run locally. The previously recorded Windows CLI-loader test failures remain
outside scope; the focused eight tests pass natively on Windows too.

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

Thank you!