From 955d6b18a9bab6a2f5530f2cf8d1014d90001052 Mon Sep 17 00:00:00 2001 From: codeAnqiang-ma <273298913+codeAnqiang-ma@users.noreply.github.com> Date: Thu, 13 Aug 2026 00:48:27 +0800 Subject: [PATCH] fix(compiler): keep maybeNaN on the failed edge of ordered comparisons MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit refine() derived clearNaN from the negated operator, treating the failed edge of a < b as a >= b having held — the two differ exactly when a side is NaN, so guard-clause spellings let NaN be "proven" whole and cross a declared i64/u64 slot as an unchecked (int64_t) / fptosi conversion. Judge NaN exclusion by the relation that actually held on the edge; the numeric interval refinement is unchanged. Co-authored-by: Cursor --- .../compiler/src/library/int-infer.test.ts | 66 +++++++++++++++++++ packages/compiler/src/library/int-infer.ts | 10 +-- tests/harness/library-int.test.ts | 13 ++++ 3 files changed, 85 insertions(+), 4 deletions(-) diff --git a/packages/compiler/src/library/int-infer.test.ts b/packages/compiler/src/library/int-infer.test.ts index 7d74c159b..c14e6834c 100644 --- a/packages/compiler/src/library/int-infer.test.ts +++ b/packages/compiler/src/library/int-infer.test.ts @@ -49,6 +49,7 @@ const send = (value: IrExpr, callee = "send"): IrStmt => ({ const decl = (localId: string, init: IrExpr): IrStmt => ({ kind: "varDecl", localId, init, loc }); const assign = (localId: string, value: IrExpr): IrStmt => ({ kind: "assign", localId, value, loc }); const iff = (cond: IrExpr, then: IrStmt[]): IrStmt => ({ kind: "if", cond, then, else_: null, loc }); +const ret = (): IrStmt => ({ kind: "return", value: null, loc }); const forLoop = (init: IrStmt, cond: IrExpr, update: IrStmt, body: IrStmt[]): IrStmt => ({ kind: "for", init, cond, update, body, loc, }); @@ -507,6 +508,71 @@ describe("the domain's edges beyond the corpus", () => { expect(v.obligation).toBe("wholeness"); expect(v.detail).toContain("NaN"); }); + + test("the failed edge of an ordered comparison keeps NaN alive (guard clauses)", () => { + // if (a < 0) return; if (a > 100) return; send(Math.trunc(a)) — NaN + // fails BOTH guards (NaN < 0 and NaN > 100 are false), reaches the + // slot, and Math.trunc(NaN) is NaN: ¬(a < b) must not clear maybeNaN. + const v = only( + caseModule(["a"], [], [ + iff(bin("<", ref("a.0"), num(0)), [ret()]), + iff(bin(">", ref("a.0"), num(100)), [ret()]), + send(math("trunc", ref("a.0"))), + ]), + ); + expect(v.outcome).toBe("refuse"); + expect(v.obligation).toBe("wholeness"); + expect(v.detail).toContain("NaN"); + }); + + test("the else spelling of the failed edge keeps NaN alive too", () => { + const inner: IrStmt = { + kind: "if", + cond: bin(">", ref("a.0"), num(100)), + then: [], + else_: [send(math("trunc", ref("a.0")))], + loc, + }; + const v = only( + caseModule(["a"], [], [ + { kind: "if", cond: bin("<", ref("a.0"), num(0)), then: [], else_: [inner], loc }, + ]), + ); + expect(v.outcome).toBe("refuse"); + expect(v.obligation).toBe("wholeness"); + expect(v.detail).toContain("NaN"); + }); + + test("a u64 slot behind failed-edge guards refuses instead of fabricating [0, 100]", () => { + const v = only( + caseModule(["a"], [], [ + iff(bin("<", ref("a.0"), num(0)), [ret()]), + iff(bin(">", ref("a.0"), num(100)), [ret()]), + send(math("trunc", ref("a.0")), "sendU64"), + ]), + ); + expect(v.outcome).toBe("refuse"); + expect(v.obligation).toBe("wholeness"); + expect(v.detail).toContain("NaN"); + }); + + test("failed edges still refine numeric members once NaN is excluded", () => { + // if (a === a) { guards } — === held excludes NaN; the guards' failed + // edges then prove [0, 100] exactly (the negated comparison keeps + // refining the numeric members, as the refine doc comment pins). + const v = only( + caseModule(["a"], [], [ + iff(bin("===", ref("a.0"), ref("a.0")), [ + iff(bin("<", ref("a.0"), num(0)), [ret()]), + iff(bin(">", ref("a.0"), num(100)), [ret()]), + send(math("trunc", ref("a.0"))), + ]), + ]), + ); + expect(v.outcome).toBe("prove"); + expect(v.provenLo).toBe(0); + expect(v.provenHi).toBe(100); + }); }); describe("straight-line ordinary-field refinement", () => { diff --git a/packages/compiler/src/library/int-infer.ts b/packages/compiler/src/library/int-infer.ts index 97ee14258..979878bb7 100644 --- a/packages/compiler/src/library/int-infer.ts +++ b/packages/compiler/src/library/int-infer.ts @@ -1209,10 +1209,12 @@ class FnAnalyzer { if (cond.left.type.kind !== "f64" || cond.right.type.kind !== "f64") return env; if (!this.isPure(cond.left) || !this.isPure(cond.right)) return env; const op = branch ? cond.op : NEGATE[cond.op]!; - // NaN makes < <= > >= === evaluate false, so the edge where one of - // those was TRUE proves both operands NaN-free (!== held excludes - // nothing — NaN !== x is true). - const clearNaN = op !== "!=="; + // NaN makes < <= > >= === evaluate false, so only the edge where one + // of those HELD proves both operands NaN-free; on the failed edge NaN + // survives (¬(a < b) does not imply a >= b — both are false when a is + // NaN), though the negated comparison still refines the numeric + // members. !== is the mirror image: its FAILED edge means === held. + const clearNaN = branch !== (cond.op === "!=="); const a = this.evalPure(cond.left, env); const b = this.evalPure(cond.right, env); const out = cloneEnv(env); diff --git a/tests/harness/library-int.test.ts b/tests/harness/library-int.test.ts index 596b8be71..bf00c5d79 100644 --- a/tests/harness/library-int.test.ts +++ b/tests/harness/library-int.test.ts @@ -198,6 +198,19 @@ const CORPUS: CorpusCase[] = [ slot: "exports.send.params[0]", evidence: ["NaN"], }, + { + name: "nan-survives-failed-guard-edge", + // NaN < 0 and NaN > 100 are both false, so a NaN dividend (a = 0) + // falls through BOTH guard clauses into the slot: the failed edge of + // an ordered comparison excludes nothing. + body: `const q = a / a;\nif (q < 0) return;\nif (q > 100) return;\nsend(Math.trunc(q));`, + param: true, + expected: "refuse", + obligation: "wholeness", + code: "SC4022", + slot: "exports.send.params[0]", + evidence: ["NaN"], + }, { name: "infinity-reaches-slot", body: `send(1 / 0);`,