[DevChiniwala]

Problem

A negated array-union test reverses the source branches during structural
narrowing. This changes the modeled return value, so Dafny can prove a
postcondition that is false of the original TypeScript.

Reproduction

export function choose(x: string | number[]): number {
  return !Array.isArray(x) ? 1 : 2;
}

Expected

Strings return 1; arrays return 2. Negated array-union ternaries are
already documented in TOOLS.md's narrowing table.

Actual

On ffc07fcf1e6826b57fad0dde6e8bc2bbfb960ab5, the generated match maps
NonArrayBranch to 2 and its fallthrough to 1. A real Dafny run verifies
the reversed claims (1 verified, 0 errors) and rejects the correct claims.

Root cause

Raw and Typed IR retain the correct conditional. In
ruleConditionalArrayIsArray, selecting NonArrayBranch already accounts
for negation, but the rule also swaps the then/else expressions.

Fix

Keep the source then-branch in the selected variant and the source else-branch
in the fallthrough. Positive Array.isArray and typeof ... === "string"
tests retain their existing branch mapping.

Regression

Add bare-variable and field-path fixtures with correct contracts. The unit
tests execute the TypeScript boundary cases and inspect narrowed IR and both
emissions; all three fail before the fix and pass afterward. The standard
fixture script verifies both functions with real Dafny.

Validation

• npm run build — pass.

• (cd tools && npm run typecheck) — pass.

• npm run typecheck:examples — pass.

• npx tsx --test tools/tests/*.test.ts — 292 passed on Linux/Node 24.

• bash tools/test-fixtures.sh — pass with Dafny 4.11.0.

• bash regen-lean.sh and bash regen-dafny.sh --no-verify — pass, no
  existing generated/proof drift.

• lake build — pass with Lean 4.34.0 and Velvet lemma2.

• Generated minimal reproduction: both universal return-value theorems and
  prove_correct choose pass in Lean.

• External pi-lemmascript at 1ec4040cfcd7e20b3039b0abfa05660431aa8458:
  all six listed Dafny files pass (30 verified members), no artifact drift.

• bash tools/check.sh dafny examples/*.ts — all 71 Dafny-enabled examples
  pass (469 reported verified members); one declared Lean-only example is
  skipped. No generated or proof-file drift afterward. The source checkout
  has no root manifest, so the example paths are passed explicitly.

The Windows baseline has 29 existing CLI-subprocess test failures related to
absolute ESM loader paths; the Linux baseline passes all 289 original tests.

Backend impact

Dafny: the correct claims now verify; the previously verified false claims
fail. Both regression functions verify (2 verified, 0 errors).

Lean: both emission regressions pass. The minimal bare-variable reproduction
passes kernel theorems for every string and array, and its Velvet correctness
proof. An additional kernel check of the record-field fixture encounters an
existing DecidableEq derivation failure for a record containing a synthesized
array-union; a detached checkout of the exact base reproduces the same error.
That separate backend limitation is unchanged here.

Compatibility

No new syntax, dependency, option, annotation or type representation. The
change only corrects negated array-test ternaries. Proofs depending on the old
reversed mapping must be updated using the normal regeneration workflow.

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

Thanks for your contributions!