fix(compiler): keep maybeNaN on the failed edge of ordered comparisons

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", () => {

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);

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);`,