From 685a611eb614c30c21ef9d7f6abf72fc563d3aee Mon Sep 17 00:00:00 2001 From: Nada Amin Date: Sun, 26 Jul 2026 13:18:24 -0400 Subject: [PATCH] represent bigint literals exactly --- SPEC.md | 5 +++- SUBSET.md | 2 +- examples/bigintBits.dfy | 26 +++++++++++++++++++++ examples/bigintBits.dfy.gen | 26 +++++++++++++++++++++ examples/bigintBits.ts | 20 ++++++++++++++++ examples/spec.def.lean | 12 ++++++++++ examples/spec.dfy | 22 ++++++++++++++++++ examples/spec.dfy.gen | 22 ++++++++++++++++++ examples/spec.proof.lean | 6 +++++ examples/spec.ts | 18 +++++++++++++++ examples/spec.types.lean | 6 +++++ tools/src/autohavoc.ts | 4 ++-- tools/src/dafny-emit.ts | 46 +++++++++++++++++++------------------ tools/src/extract.ts | 10 ++++---- tools/src/ir.ts | 23 ++++++++++++++++++- tools/src/lean-emit.ts | 9 +++++--- tools/src/narrow.ts | 4 ++-- tools/src/peephole.ts | 4 ++-- tools/src/rawir.ts | 18 ++++++++++++++- tools/src/resolve.ts | 6 ++++- tools/src/specparser.ts | 31 ++++++++++++++----------- tools/src/transform.ts | 8 +++++-- tools/src/typedir.ts | 1 + 23 files changed, 274 insertions(+), 55 deletions(-) create mode 100644 examples/bigintBits.dfy create mode 100644 examples/bigintBits.dfy.gen create mode 100644 examples/bigintBits.ts diff --git a/SPEC.md b/SPEC.md index 60eec27a..a9a7c238 100644 --- a/SPEC.md +++ b/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 diff --git a/SUBSET.md b/SUBSET.md index af16776e..4cfb17f5 100644 --- a/SUBSET.md +++ b/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` / `readonly T[]` | sequence | | diff --git a/examples/bigintBits.dfy b/examples/bigintBits.dfy new file mode 100644 index 00000000..be1f6f46 --- /dev/null +++ b/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) +{ +} diff --git a/examples/bigintBits.dfy.gen b/examples/bigintBits.dfy.gen new file mode 100644 index 00000000..be1f6f46 --- /dev/null +++ b/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) +{ +} diff --git a/examples/bigintBits.ts b/examples/bigintBits.ts new file mode 100644 index 00000000..00c05a83 --- /dev/null +++ b/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 +} diff --git a/examples/spec.def.lean b/examples/spec.def.lean index 35f2dc26..481884ea 100644 --- a/examples/spec.def.lean +++ b/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 diff --git a/examples/spec.dfy b/examples/spec.dfy index 888aa7ac..8ff6c6f5 100644 --- a/examples/spec.dfy +++ b/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 { [x] diff --git a/examples/spec.dfy.gen b/examples/spec.dfy.gen index 888aa7ac..8ff6c6f5 100644 --- a/examples/spec.dfy.gen +++ b/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 { [x] diff --git a/examples/spec.proof.lean b/examples/spec.proof.lean index 1ddae1b8..e8e54efd 100644 --- a/examples/spec.proof.lean +++ b/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 diff --git a/examples/spec.ts b/examples/spec.ts index bde3691b..c860a580 100644 --- a/examples/spec.ts +++ b/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 diff --git a/examples/spec.types.lean b/examples/spec.types.lean index 4e239072..708b6723 100644 --- a/examples/spec.types.lean +++ b/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] diff --git a/tools/src/autohavoc.ts b/tools/src/autohavoc.ts index 0802e21f..98e5792c 100644 --- a/tools/src/autohavoc.ts +++ b/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)) }; diff --git a/tools/src/dafny-emit.ts b/tools/src/dafny-emit.ts index 2a8b1689..5ec8d98d 100644 --- a/tools/src/dafny-emit.ts +++ b/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"); diff --git a/tools/src/extract.ts b/tools/src/extract.ts index 73d7e7d1..6f7a877d 100644 --- a/tools/src/extract.ts +++ b/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) }; diff --git a/tools/src/ir.ts b/tools/src/ir.ts index 15a7fbd0..5dceb4e5 100644 --- a/tools/src/ir.ts +++ b/tools/src/ir.ts @@ -12,6 +12,7 @@ import type { Ty } from "./typedir.js"; export type Expr = | { kind: "var"; name: string } | { kind: "num"; value: number } + | { kind: "bigint"; value: string } // exact integer literal, canonical decimal — emitted verbatim | { kind: "bool"; value: boolean } | { kind: "str"; value: string } | { kind: "constructor"; name: string; type?: string; args: Expr[] } // .idle / .some x — name is lowercase; emitters capitalize per backend @@ -214,6 +215,26 @@ export interface Module { decls: Decl[]; } +// ── Literal queries ────────────────────────────────────────── + +/** The exact value of an integer-literal operand (possibly negated), or null + * when `e` isn't one. Answers in compiler-side `bigint` so a backend folding a + * literal into arithmetic stays exact: JS bitwise operators truncate to 32 bits + * and `Math.pow(2, n)` is a double, both of which lie past 2^53. A `num` + * outside the safe-integer range has already lost precision, so it is not a + * usable answer — hence null. */ +export function exactIntegerLiteral(e: Expr): bigint | null { + if (e.kind === "bigint") return BigInt(e.value); + if (e.kind === "num") return Number.isSafeInteger(e.value) ? BigInt(e.value) : null; + // Transform folds `-` into a negative `num`, but leaves a negated + // `bigint` structural (folding it would coerce the payload through Number). + if (e.kind === "unop" && e.op === "-") { + const inner = exactIntegerLiteral(e.expr); + return inner === null ? null : -inner; + } + return null; +} + // ── Traversal ──────────────────────────────────────────────── // // A single generic query visitor. `mapExpr`/`mapStmt` (in transform.ts) rewrite @@ -228,7 +249,7 @@ type ExprPred = (e: Expr) => boolean; export function anyExpr(e: Expr, pred: ExprPred): boolean { if (pred(e)) return true; switch (e.kind) { - case "var": case "num": case "bool": case "str": + case "var": case "num": case "bigint": case "bool": case "str": case "emptyMap": case "emptySet": case "havoc": case "default": return false; case "constructor": return e.args.some(a => anyExpr(a, pred)); case "binop": return anyExpr(e.left, pred) || anyExpr(e.right, pred); diff --git a/tools/src/lean-emit.ts b/tools/src/lean-emit.ts index eedc13de..82fe7a05 100644 --- a/tools/src/lean-emit.ts +++ b/tools/src/lean-emit.ts @@ -303,6 +303,8 @@ function emitExpr(e: Expr, parentPrec?: number): string { // `undefined` is the IR's spelling of the absent optional (mirrors dafny-emit's None) case "var": return e.name === "undefined" ? "none" : escapeName(e.name); case "num": return `${e.value}`; + // Already canonical decimal; Lean'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')}"`; @@ -357,7 +359,8 @@ function emitExpr(e: Expr, parentPrec?: number): string { case "unop": if (e.op === "¬") return _boolCtx ? `!(${emitExpr(e.expr)})` : `¬(${emitExpr(e.expr)})`; if (e.op !== "-") throw new Error(`Unsupported Lean unary operator: ${e.op}`); - return e.expr.kind === "num" ? `-${e.expr.value}` : `(-${emitExpr(e.expr)})`; + return (e.expr.kind === "num" || e.expr.kind === "bigint") + ? `-${e.expr.value}` : `(-${emitExpr(e.expr)})`; case "binop": { // Discriminator test against a constructor that carries fields: @@ -459,13 +462,13 @@ function emitExpr(e: Expr, parentPrec?: number): string { } const obj = emitExpr(e.obj); if (e.field === "collectionSize") return `${obj}.size`; - const wrap = e.obj.kind !== "var" && e.obj.kind !== "num" && e.obj.kind !== "bool"; + const wrap = e.obj.kind !== "var" && e.obj.kind !== "num" && e.obj.kind !== "bigint" && e.obj.kind !== "bool"; return wrap ? `(${obj}).${escapeName(e.field)}` : `${obj}.${escapeName(e.field)}`; } case "toNat": { const inner = emitExpr(e.expr); - const wrap = e.expr.kind !== "var" && e.expr.kind !== "num"; + const wrap = e.expr.kind !== "var" && e.expr.kind !== "num" && e.expr.kind !== "bigint"; return wrap ? `(${inner}).toNat` : `${inner}.toNat`; } diff --git a/tools/src/narrow.ts b/tools/src/narrow.ts index ada45608..3d7d2e44 100644 --- a/tools/src/narrow.ts +++ b/tools/src/narrow.ts @@ -57,7 +57,7 @@ function walkExpr(e: TExpr, ctx: CondCtx): TExpr { function recurseExpr(e: TExpr, ctx: CondCtx): TExpr { const re = (x: TExpr) => walkExpr(x, ctx); switch (e.kind) { - case "var": case "num": case "str": case "bool": + case "var": case "num": case "bigint": case "str": case "bool": case "havoc": return e; case "binop": return { ...e, left: re(e.left), right: re(e.right) }; @@ -506,7 +506,7 @@ function containsMethodCall(e: TExpr): boolean { return true; } switch (e.kind) { - case "var": case "num": case "str": case "bool": + case "var": case "num": case "bigint": case "str": case "bool": case "havoc": return false; case "binop": return containsMethodCall(e.left) || containsMethodCall(e.right); diff --git a/tools/src/peephole.ts b/tools/src/peephole.ts index de4a0a6b..78aeb961 100644 --- a/tools/src/peephole.ts +++ b/tools/src/peephole.ts @@ -23,7 +23,7 @@ function mapExpr(e: Expr, f: (e: Expr) => Expr | null): Expr { if (hit) return hit; const r = (x: Expr) => mapExpr(x, f); switch (e.kind) { - case "var": case "num": case "bool": case "str": case "constructor": + case "var": case "num": case "bigint": case "bool": case "str": case "constructor": case "emptyMap": case "emptySet": case "havoc": case "default": case "mapLiteral": return e; case "binop": return { ...e, left: r(e.left), right: r(e.right) }; case "unop": return { ...e, expr: r(e.expr) }; @@ -276,7 +276,7 @@ function peepholeExpr(e: Expr): Expr { function rewriteChildrenExpr(e: Expr): Expr { const r = peepholeExpr; switch (e.kind) { - case "var": case "num": case "bool": case "str": case "constructor": + case "var": case "num": case "bigint": case "bool": case "str": case "constructor": case "emptyMap": case "emptySet": case "havoc": case "default": case "mapLiteral": return e; case "binop": return { ...e, left: r(e.left), right: r(e.right) }; case "unop": return { ...e, expr: r(e.expr) }; diff --git a/tools/src/rawir.ts b/tools/src/rawir.ts index 09d0ad15..3ff6cca3 100644 --- a/tools/src/rawir.ts +++ b/tools/src/rawir.ts @@ -10,6 +10,21 @@ // ── Expressions ────────────────────────────────────────────── +/** Source text of a BigInt literal → the canonical decimal string stored in a + * `bigint` node. Shared by the body extractor and the spec parser so both + * sides of a function (code and `//@ ` annotations) agree exactly. + * + * A BigInt literal must never pass through `Number`/`parseInt`: `9007199254740993n` + * and `9007199254740992n` are distinct values that collapse to the same double. + * Hence the string payload — it also keeps the raw IR `JSON.stringify`-able, + * which `lsc extract` relies on. */ +export function normalizeBigIntLiteral(text: string): string { + const withoutSuffix = text.endsWith("n") ? text.slice(0, -1) : text; + // BigInt() understands decimal, hex, binary, and octal; numeric separators + // are source syntax and must be stripped first. + return BigInt(withoutSuffix.replace(/_/g, "")).toString(10); +} + /** A step in an optional chain — what to do with the binder after `?.`. * field: `?.foo` or `.foo` after `?.`. * call: `?.foo()` or `.foo()` / `()` after `?.`. @@ -21,7 +36,8 @@ export type RawChainStep = export type RawExpr = | { kind: "var"; name: string } - | { kind: "num"; value: number; big?: boolean } // `big` = BigInt literal (123n) + | { kind: "num"; value: number } + | { kind: "bigint"; value: string } // BigInt literal (123n) — canonical decimal, no `n` | { kind: "str"; value: string } | { kind: "bool"; value: boolean } | { kind: "binop"; op: string; left: RawExpr; right: RawExpr } diff --git a/tools/src/resolve.ts b/tools/src/resolve.ts index 1cd4ca0b..3e4eda42 100644 --- a/tools/src/resolve.ts +++ b/tools/src/resolve.ts @@ -710,9 +710,13 @@ function resolveExpr(e: RawExpr, ctx: Ctx): TExpr { case "num": if (!Number.isInteger(e.value)) return { kind: "num", value: e.value, ty: { kind: "real" } }; - if (e.big) return { kind: "num", value: e.value, ty: { kind: "int", big: true } }; return { kind: "num", value: e.value, ty: e.value >= 0 ? { kind: "nat" } : { kind: "int" } }; + // Always `int` (never `nat`, even when non-negative), carrying `big` so the + // surrounding arithmetic picks bigint division semantics — see `isBigInt`. + case "bigint": + return { kind: "bigint", value: e.value, ty: { kind: "int", big: true } }; + case "str": return { kind: "str", value: e.value, ty: { kind: "string" } }; diff --git a/tools/src/specparser.ts b/tools/src/specparser.ts index dd03fb9e..97dd3dc3 100644 --- a/tools/src/specparser.ts +++ b/tools/src/specparser.ts @@ -4,6 +4,7 @@ */ import type { RawExpr } from "./rawir.js"; +import { normalizeBigIntLiteral } from "./rawir.js"; export type Expr = RawExpr; @@ -11,6 +12,7 @@ export type Expr = RawExpr; type Token = | { type: "num"; value: number } + | { type: "bigint"; value: string } | { type: "str"; value: string } | { type: "ident"; value: string } | { type: "op"; value: string } @@ -19,6 +21,13 @@ type Token = const MULTI_OPS = ["<==>", "==>", "===", "!==", "==", "!=", ">=", "<=", "&&", "||"]; +/** Hex / binary / octal / decimal integer, with optional numeric separators and + * an optional `n` (BigInt) suffix in capture group 1. Deliberately integer-only: + * a trailing `.` is left for the tokenizer to emit as punctuation, exactly as + * the previous digit-scanning loop did. */ +const INTEGER_LITERAL = + /^(?:(?:0[xX][0-9a-fA-F](?:_?[0-9a-fA-F])*)|(?:0[bB][01](?:_?[01])*)|(?:0[oO][0-7](?:_?[0-7])*)|(?:[0-9](?:_?[0-9])*))(n)?/; + function tokenize(input: string): Token[] { const tokens: Token[] = []; let i = 0; @@ -55,19 +64,14 @@ function tokenize(input: string): Token[] { } if (/[0-9]/.test(input[i])) { - let value: number; - if (input[i] === "0" && i + 1 < input.length && input[i + 1] === "x") { - i += 2; - let hex = ""; - while (i < input.length && /[0-9a-fA-F]/.test(input[i])) hex += input[i++]; - value = parseInt(hex, 16); - } else { - let dec = ""; - while (i < input.length && /[0-9]/.test(input[i])) dec += input[i++]; - value = parseInt(dec, 10); - } - if (i < input.length && input[i] === "n") i++; - tokens.push({ type: "num", value }); + const match = input.slice(i).match(INTEGER_LITERAL); + if (!match) throw new Error(`Invalid numeric literal at ${i} in: ${input}`); + const text = match[0]; + i += text.length; + // The `n` suffix is meaningful, not noise: a BigInt keeps its exact value + // as a decimal string instead of being rounded into a double. + if (match[1] === "n") tokens.push({ type: "bigint", value: normalizeBigIntLiteral(text) }); + else tokens.push({ type: "num", value: Number(text.replace(/_/g, "")) }); continue; } @@ -242,6 +246,7 @@ class Parser { if (!t) throw new Error("Unexpected end of expression"); if (t.type === "result") { this.advance(); return { kind: "result" }; } if (t.type === "num") { this.advance(); return { kind: "num", value: t.value }; } + if (t.type === "bigint") { this.advance(); return { kind: "bigint", value: t.value }; } if (t.type === "str") { this.advance(); return { kind: "str", value: t.value }; } if (t.type === "ident") { if (t.value === "true") { this.advance(); return { kind: "bool", value: true }; } diff --git a/tools/src/transform.ts b/tools/src/transform.ts index a8086447..ceb3fc6a 100644 --- a/tools/src/transform.ts +++ b/tools/src/transform.ts @@ -28,7 +28,7 @@ function mapExpr(e: Expr, f: (e: Expr) => Expr | null): Expr { if (hit) return hit; const r = (x: Expr) => mapExpr(x, f); switch (e.kind) { - case "var": case "num": case "bool": case "str": case "emptyMap": case "emptySet": case "havoc": case "default": return e; + case "var": case "num": case "bigint": case "bool": case "str": case "emptyMap": case "emptySet": case "havoc": case "default": return e; case "mapLiteral": return { ...e, entries: e.entries.map(en => ({ key: r(en.key), value: r(en.value) })) }; case "constructor": return e.args ? { ...e, args: e.args.map(r) } : e; case "binop": return { ...e, left: r(e.left), right: r(e.right) }; @@ -125,7 +125,7 @@ function mapTExpr(e: TExpr, f: (e: TExpr) => TExpr | null): TExpr { if (hit) return hit; const r = (x: TExpr) => mapTExpr(x, f); 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: 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) }; @@ -446,6 +446,7 @@ function lowerExpr(e: TExpr, binds: Stmt[] | null): Expr { switch (e.kind) { case "var": return { kind: "var", name: e.name }; case "num": return { kind: "num", value: e.value }; + case "bigint": return { kind: "bigint", value: e.value }; case "bool": return { kind: "bool", value: e.value }; case "str": @@ -453,6 +454,9 @@ function lowerExpr(e: TExpr, binds: Stmt[] | null): Expr { return { kind: "str", value: e.value }; case "unop": + // Only `num` folds. A `bigint` payload is a string, so negating it here + // would coerce through `Number` and round: `-9007199254740993n` stays a + // structural `unop("-", bigint(...))` and is negated by the emitter. if (e.op === "-" && e.expr.kind === "num") return { kind: "num", value: -e.expr.value }; // String truthiness: !str → str == "" diff --git a/tools/src/typedir.ts b/tools/src/typedir.ts index 66c851c6..b0d6be8c 100644 --- a/tools/src/typedir.ts +++ b/tools/src/typedir.ts @@ -84,6 +84,7 @@ export type TChainStep = export type TExpr = | { kind: "var"; name: string; ty: Ty } | { kind: "num"; value: number; ty: Ty } + | { kind: "bigint"; value: string; ty: Ty } // exact integer, canonical decimal | { kind: "str"; value: string; ty: Ty } | { kind: "bool"; value: boolean; ty: Ty } | { kind: "binop"; op: string; left: TExpr; right: TExpr; ty: Ty }