represent bigint literals exactly

SPEC.md

@@ -981,12 +981,13 @@ The spec body is purely additive — `regen` three-way-merges and preserves user
 
 ### 6.1.1 BigInt
 
-TypeScript's `bigint` type maps to `Int`/`int` (same as `number`). BigInt literals like `32n`, `0xffffn` are treated as integer literals with the `n` suffix stripped. Hex literals (`0x...`) and the `n` suffix are supported in both function bodies and `//@ ` annotations:
+TypeScript's `bigint` type maps to `Int`/`int` (same as `number`). BigInt literals like `32n`, `0xffffn` are treated as integer literals with the `n` suffix stripped. Decimal, hex (`0x…`), binary (`0b…`), and octal (`0o…`) spellings, numeric separators (`1_000_000n`), and the `n` suffix are all supported in both function bodies and `//@ ` annotations. Since the backends have unbounded integers, a BigInt literal is carried exactly — never through a JS `number` — so values past `Number.MAX_SAFE_INTEGER` keep their identity:
 
 | TypeScript | Dafny | Lean |
 |-----------|-------|------|
 | `32n` | `32` (int) | `32` (Int) |
 | `0xffffn` | `65535` (int) | `65535` (Int) |
+| `0x20000000000001n` | `9007199254740993` (int) | `9007199254740993` (Int) |
 
 **Bitwise operators (Dafny only):** Since Dafny's `int` has no native bitwise ops, they are translated to arithmetic when the right operand is a literal:
 
@@ -996,6 +997,8 @@ TypeScript's `bigint` type maps to `Int`/`int` (same as `number`). BigInt litera
 | `x << 8n` | `x * 256` |
 | `x & 0xffffffffn` | `x % 4294967296` (only when mask+1 is a power of 2) |
 
+The shift factor and the mask modulus are computed exactly too, so wide operands (`x << 70n`, `x & 0xffffffffffffffffn`) fold correctly rather than through a double. See [`examples/bigintBits.ts`](examples/bigintBits.ts).
+
 Lean backend does not yet support bitwise operators.
 
 ### 6.1.2 Constants

SUBSET.md

@@ -32,7 +32,7 @@ Two things shape what you can verify:
 |-----------|-----------|-------|
 | `number` | integer | Maps to `int` by default. Add `//@ type nat` for a non-negative integer. |
 | `number` (non-integer literal) | real | `0.8`, `3.14` become reals; mixed int/real arithmetic coerces automatically. |
-| `bigint` | integer | Same as `number`; `32n`, `0xffffn` literals supported. |
+| `bigint` | integer | Same as `number`; `32n`, `0xffffn` literals supported, exact past 2^53. |
 | `boolean` | bool | |
 | `string` | string | |
 | `T[]` / `Array<T>` / `readonly T[]` | sequence | |

examples/bigintBits.dfy

@@ -0,0 +1,26 @@
+// Generated by lsc from bigintBits.ts
+
+function shiftWide(x: int): int
+  requires (x >= 0)
+{
+  (x * 1180591620717411303424)
+}
+
+lemma shiftWide_ensures(x: int)
+  requires (x >= 0)
+  ensures (shiftWide(x) >= x)
+{
+}
+
+function low64(x: int): int
+  requires (x >= 0)
+{
+  (x % 18446744073709551616)
+}
+
+lemma low64_ensures(x: int)
+  requires (x >= 0)
+  ensures (low64(x) < 18446744073709551616)
+  ensures (low64(x) >= 0)
+{
+}

examples/bigintBits.dfy.gen

@@ -0,0 +1,26 @@
+// Generated by lsc from bigintBits.ts
+
+function shiftWide(x: int): int
+  requires (x >= 0)
+{
+  (x * 1180591620717411303424)
+}
+
+lemma shiftWide_ensures(x: int)
+  requires (x >= 0)
+  ensures (shiftWide(x) >= x)
+{
+}
+
+function low64(x: int): int
+  requires (x >= 0)
+{
+  (x % 18446744073709551616)
+}
+
+lemma low64_ensures(x: int)
+  requires (x >= 0)
+  ensures (low64(x) < 18446744073709551616)
+  ensures (low64(x) >= 0)
+{
+}

examples/bigintBits.ts

@@ -0,0 +1,20 @@
+//@ backend dafny
+// Shifts and masks by a literal fold to exact arithmetic. The literal is read
+// as a compiler-side BigInt, so both the shift factor and the mask modulus stay
+// exact past 2^53 — a `Math.pow`/32-bit-`&` fold would emit `1.18e+21` for the
+// shift below and the wrong modulus (…552000) for the 64-bit mask.
+
+export function shiftWide(x: bigint): bigint {
+  //@ verify
+  //@ requires x >= 0
+  //@ ensures \result >= x
+  return x << 70n
+}
+
+export function low64(x: bigint): bigint {
+  //@ verify
+  //@ requires x >= 0
+  //@ ensures \result < 18446744073709551616n
+  //@ ensures \result >= 0
+  return x & 0xffffffffffffffffn
+}

examples/spec.def.lean

@@ -59,6 +59,18 @@ method midpoint (lo : Int) (hi : Int) return (res : Int)
   do
     return Pure.midpoint lo hi
 
+method exactBigIntLiteral  return (res : Int)
+  ensures res = 9007199254740993
+  ensures res ≠ 9007199254740992
+  do
+    return Pure.exactBigIntLiteral 
+
+method exactNegativeBigIntLiteral  return (res : Int)
+  ensures res = -9007199254740993
+  ensures res ≠ -9007199254740992
+  do
+    return Pure.exactNegativeBigIntLiteral 
+
 method wrapOne (x : Int) return (res : Array Int)
   ensures res.size = 1
   do

examples/spec.dfy

@@ -173,6 +173,28 @@ lemma midpoint_ensures(lo: int, hi: int)
 {
 }
 
+function exactBigIntLiteral(): int
+{
+  9007199254740993
+}
+
+lemma exactBigIntLiteral_ensures()
+  ensures (exactBigIntLiteral() == 9007199254740993)
+  ensures (exactBigIntLiteral() != 9007199254740992)
+{
+}
+
+function exactNegativeBigIntLiteral(): int
+{
+  (-(9007199254740993))
+}
+
+lemma exactNegativeBigIntLiteral_ensures()
+  ensures (exactNegativeBigIntLiteral() == (-(9007199254740993)))
+  ensures (exactNegativeBigIntLiteral() != (-(9007199254740992)))
+{
+}
+
 function wrapOne(x: int): seq<int>
 {
   [x]

examples/spec.dfy.gen

@@ -173,6 +173,28 @@ lemma midpoint_ensures(lo: int, hi: int)
 {
 }
 
+function exactBigIntLiteral(): int
+{
+  9007199254740993
+}
+
+lemma exactBigIntLiteral_ensures()
+  ensures (exactBigIntLiteral() == 9007199254740993)
+  ensures (exactBigIntLiteral() != 9007199254740992)
+{
+}
+
+function exactNegativeBigIntLiteral(): int
+{
+  (-(9007199254740993))
+}
+
+lemma exactNegativeBigIntLiteral_ensures()
+  ensures (exactNegativeBigIntLiteral() == (-(9007199254740993)))
+  ensures (exactNegativeBigIntLiteral() != (-(9007199254740992)))
+{
+}
+
 function wrapOne(x: int): seq<int>
 {
   [x]

examples/spec.proof.lean

@@ -31,6 +31,12 @@ prove_correct makeHighItem by
 prove_correct midpoint by
   unfold Pure.midpoint; loom_solve
 
+prove_correct exactBigIntLiteral by
+  unfold Pure.exactBigIntLiteral; loom_solve
+
+prove_correct exactNegativeBigIntLiteral by
+  unfold Pure.exactNegativeBigIntLiteral; loom_solve
+
 prove_correct wrapOne by
   unfold Pure.wrapOne; loom_solve
 

examples/spec.ts

@@ -96,6 +96,24 @@ function midpoint(lo: number, hi: number): number {
   return Math.floor((lo + hi) / 2);
 }
 
+// §6.1.1: BigInt literals stay exact past Number.MAX_SAFE_INTEGER. The two
+// postconditions straddle 2^53, where a double can't tell 9007199254740993
+// from 9007199254740992 — so this only verifies if the literal never rounds
+// through Number, in the body *or* in the annotation.
+function exactBigIntLiteral(): bigint {
+  //@ ensures \result === 9007199254740993n
+  //@ ensures \result !== 9007199254740992n
+  return 0x20000000000001n;
+}
+
+// §6.1.1: same, through unary minus — a negative literal must not be folded
+// by negating a JS number.
+function exactNegativeBigIntLiteral(): bigint {
+  //@ ensures \result === -9007199254740993n
+  //@ ensures \result !== -9007199254740992n
+  return -9007199254740993n;
+}
+
 // §4.2: array literal
 function wrapOne(x: number): number[] {
   //@ ensures \result.length === 1

examples/spec.types.lean

@@ -105,6 +105,12 @@ def makeHighItem (v : Int) : PriorityItem :=
 def midpoint (lo : Int) (hi : Int) : Int :=
   (lo + hi) / 2
 
+def exactBigIntLiteral  : Int :=
+  9007199254740993
+
+def exactNegativeBigIntLiteral  : Int :=
+  -9007199254740993
+
 def wrapOne (x : Int) : Array Int :=
   #[x]
 

tools/src/autohavoc.ts

@@ -30,7 +30,7 @@ import type { TExpr, TStmt, TModule } from "./typedir.js";
  *  havoc'd variable is fine; only the *source* expression is replaced. */
 function isBadNode(e: TExpr): boolean {
   switch (e.kind) {
-    case "var": case "num": case "str": case "bool": case "havoc":
+    case "var": case "num": case "bigint": case "str": case "bool": case "havoc":
       return false;
     // A field/index is unmodellable when its *object* is opaque (`req.body`,
     // `process.env.X`). It is NOT unmodellable just because its own type is
@@ -239,7 +239,7 @@ function rewriteExpr(e: TExpr, hoisted: TStmt[]): TExpr {
     return { kind: "havoc", ty: e.ty };
   }
   switch (e.kind) {
-    case "var": case "num": case "str": case "bool": case "havoc": return e;
+    case "var": case "num": case "bigint": case "str": case "bool": case "havoc": return e;
     case "binop": return { ...e, left: rewriteExpr(e.left, hoisted), right: rewriteExpr(e.right, hoisted) };
     case "unop": return { ...e, expr: rewriteExpr(e.expr, hoisted) };
     case "call": return { ...e, fn: rewriteExpr(e.fn, hoisted), args: e.args.map(a => rewriteExpr(a, hoisted)) };

tools/src/dafny-emit.ts

@@ -3,7 +3,7 @@
  */
 
 import type { Expr, Stmt, Decl, Module, MatchPattern } from "./ir.js";
-import { usesName, usesNameInDecl, usesNameInStmts } from "./ir.js";
+import { exactIntegerLiteral, usesName, usesNameInDecl, usesNameInStmts } from "./ir.js";
 import type { Ty } from "./typedir.js";
 import { freshName, freshNameWhere, userNames } from "./names.js";
 import { renameFreeVar } from "./transform.js";
@@ -221,6 +221,8 @@ function emitExpr(e: Expr): string {
   switch (e.kind) {
     case "var": return e.name === "undefined" ? "None" : escapeName(e.name);
     case "num": return `${e.value}`;
+    // Already canonical decimal; Dafny's `int` is mathematical, so no `n` suffix.
+    case "bigint": return e.value;
     case "bool": return e.value ? "true" : "false";
     case "str": return `"${e.value.replace(/\\/g, '\\\\').replace(/"/g, '\\"').replace(/\n/g, '\\n')}"`;
 
@@ -374,11 +376,14 @@ function emitExpr(e: Expr): string {
         }
         if (e.method === "split")   { needPreamble("StringSplit"); return `StringSplit(${obj}, ${args[0]})`; }
         if (e.method === "slice") {
-          // JS negative index: arr.slice(0, -N) → arr[0..|arr|-N]. After
-          // transform, unary minus on a numeric literal is folded to a
-          // negative `num` IR node, so check for that here.
-          const negVal = (a: typeof e.args[0]): number | null =>
-            a.kind === "num" && a.value < 0 ? -a.value : null;
+          // JS negative index: arr.slice(0, -N) → arr[0..|arr|-N]. Transform
+          // folds unary minus on a numeric literal into a negative `num` node,
+          // but leaves a negated bigint structural — `exactIntegerLiteral`
+          // recognizes both.
+          const negVal = (a: typeof e.args[0]): string | null => {
+            const v = exactIntegerLiteral(a);
+            return v !== null && v < 0n ? (-v).toString(10) : null;
+          };
           const loN = negVal(e.args[0]);
           const loEx = loN !== null ? `|${obj}|-${loN}` : args[0];
           if (args.length === 1) return `${obj}[${loEx}..]`;
@@ -451,6 +456,7 @@ function emitExpr(e: Expr): string {
       if (op === "!" && e.expr.kind !== "var" && e.expr.kind !== "bool")
         return `!(${emitExpr(e.expr)})`;
       if (e.op === "-" && e.expr.kind === "num") return `(-(${e.expr.value}))`;
+      if (e.op === "-" && e.expr.kind === "bigint") return `(-(${e.expr.value}))`;
       if (e.op === "-") return `(-(${emitExpr(e.expr)}))`;
       return `${op}(${emitExpr(e.expr)})`;
     }
@@ -466,27 +472,23 @@ function emitExpr(e: Expr): string {
       // Bitwise operators on int: translate to arithmetic
       // x >> n → x / 2^n (right shift)
       // x << n → x * 2^n (left shift)
-      if (e.op === ">>") {
-        if (e.right.kind === "num") {
-          return `(${emitExpr(e.left)} / ${Math.pow(2, e.right.value)})`;
-        }
-        needPreamble("Pow2");
-        return `(${emitExpr(e.left)} / Pow2(${emitExpr(e.right)}))`;
-      }
-      if (e.op === "<<") {
-        if (e.right.kind === "num") {
-          return `(${emitExpr(e.left)} * ${Math.pow(2, e.right.value)})`;
+      if (e.op === ">>" || e.op === "<<") {
+        const shift = exactIntegerLiteral(e.right);
+        // Cap the fold: a huge literal shift would inline an absurd numeral.
+        if (shift !== null && shift >= 0n && shift <= 1024n) {
+          const factor = (1n << shift).toString(10);
+          return `(${emitExpr(e.left)} ${e.op === ">>" ? "/" : "*"} ${factor})`;
         }
         needPreamble("Pow2");
-        return `(${emitExpr(e.left)} * Pow2(${emitExpr(e.right)}))`;
+        return `(${emitExpr(e.left)} ${e.op === ">>" ? "/" : "*"} Pow2(${emitExpr(e.right)}))`;
       }
       // x & mask → x % (mask + 1) for literal masks of form 2^n - 1, else BitAnd
       if (e.op === "&") {
-        if (e.right.kind === "num") {
-          const mask = e.right.value;
-          const modulus = mask + 1;
-          if ((modulus & (modulus - 1)) === 0) {
-            return `(${emitExpr(e.left)} % ${modulus})`;
+        const mask = exactIntegerLiteral(e.right);
+        if (mask !== null && mask >= 0n) {
+          const modulus = mask + 1n;
+          if ((modulus & (modulus - 1n)) === 0n) {
+            return `(${emitExpr(e.left)} % ${modulus.toString(10)})`;
           }
         }
         needPreamble("BitAnd");

tools/src/extract.ts

@@ -9,6 +9,7 @@ import { Project, Node, FunctionDeclaration, InterfaceDeclaration, SourceFile, T
 import type { TypeDeclInfo, VariantInfo } from "./types.js";
 import { initTypeParser } from "./types.js";
 import type { RawExpr, RawStmt, RawFunction, RawModule, RawClass, RawConst, RawGhostLet, RawGhostAssign } from "./rawir.js";
+import { normalizeBigIntLiteral } from "./rawir.js";
 import { setUserNames, freshName } from "./names.js";
 
 // ── Expression extraction ────────────────────────────────────
@@ -343,10 +344,11 @@ function extractExpr(node: Expression): RawExpr {
     return { kind: "num", value: Number(node.getLiteralValue()) };
   }
 
-  // BigInt literal (e.g. 32n, 0xffffn) — integer, with bigint division semantics
+  // BigInt literal (e.g. 32n, 0xffffn) — exact integer, with bigint division
+  // semantics. Kept as a decimal string: `getLiteralValue()`/`Number()` would
+  // round anything past 2^53 (`9007199254740993n` → `9007199254740992`).
   if (Node.isBigIntLiteral(node)) {
-    const text = node.getText().replace(/n$/, '');
-    return { kind: "num", value: Number(text), big: true };
+    return { kind: "bigint", value: normalizeBigIntLiteral(node.getText()) };
   }
 
   // Template literal: `foo${x}bar` → "foo" + x + "bar"
@@ -1097,7 +1099,7 @@ function renameRawExpr(e: RawExpr, from: string, to: string): RawExpr {
   const r = (x: RawExpr) => renameRawExpr(x, from, to);
   switch (e.kind) {
     case "var": return e.name === from ? { kind: "var", name: to } : e;
-    case "num": case "str": case "bool": case "result": case "havoc": case "emptyCollection": return e;
+    case "num": case "bigint": case "str": case "bool": case "result": case "havoc": case "emptyCollection": return e;
     case "binop": return { ...e, left: r(e.left), right: r(e.right) };
     case "unop": return { ...e, expr: r(e.expr) };
     case "call": return { ...e, fn: r(e.fn), args: e.args.map(r) };