From 7f43945950f9163b4feac272c9d497bfee124248 Mon Sep 17 00:00:00 2001 From: Nada Amin Date: Wed, 24 Jun 2026 23:46:41 -0400 Subject: [PATCH 1/2] sortby --- tools/src/dafny-emit.ts | 14 ++++++++++++++ tools/src/resolve.ts | 11 +++++++++++ tools/src/transform.ts | 2 +- 3 files changed, 26 insertions(+), 1 deletion(-) diff --git a/tools/src/dafny-emit.ts b/tools/src/dafny-emit.ts index 2418f76..d71adb6 100644 --- a/tools/src/dafny-emit.ts +++ b/tools/src/dafny-emit.ts @@ -168,6 +168,7 @@ function emitExpr(e: Expr): string { if (e.method === "push") return `(${obj} + [${args.join(", ")}])`; if (e.method === "unshift") return `([${args.join(", ")}] + ${obj})`; if (e.method === "concat") return `(${obj} + [${args.join(", ")}])`; + if (e.method === "sort") { needPreamble("SeqSortBy"); return `SeqSortBy(${obj}, ${args[0]})`; } // No-arg slice is a full copy; Dafny seq is an immutable value type, so // the copy is just the seq itself (the idiom for "copy then mutate"). if (e.method === "slice" && args.length === 0) return obj; @@ -923,6 +924,18 @@ const STRING_SPLIT = `function {:axiom} StringSplit(s: string, d: string): seq |StringSplit(s, d)[k]| <= |s|`; +// `xs.sort(cmp)` in TS sorts in place by a comparator (negative ⟺ a before b). +// Modeled here as an axiom returning a permutation sorted by cmp. The `requires` +// is the soundness condition — cmp must be a total preorder, otherwise no sorted +// permutation exists and the axiom would be vacuous. Callers discharge it (e.g. +// `(a,b) => a.k - b.k` is total + transitive by linear arithmetic). +const SEQ_SORT_BY = `function {:axiom} SeqSortBy(s: seq, cmp: (T, T) -> int): seq + requires forall a: T, b: T :: cmp(a, b) <= 0 || cmp(b, a) <= 0 + requires forall a: T, b: T, c: T :: cmp(a, b) <= 0 && cmp(b, c) <= 0 ==> cmp(a, c) <= 0 + ensures multiset(SeqSortBy(s, cmp)) == multiset(s) + ensures |SeqSortBy(s, cmp)| == |s| + ensures forall i: int, j: int :: 0 <= i <= j < |SeqSortBy(s, cmp)| ==> cmp(SeqSortBy(s, cmp)[i], SeqSortBy(s, cmp)[j]) <= 0`; + const STRING_TRIM = `function StringTrimLeft(s: string): string ensures |StringTrimLeft(s)| <= |s| ensures StringTrimLeft(s) == "" || (|StringTrimLeft(s)| > 0 && StringTrimLeft(s)[0] != ' ') @@ -1085,6 +1098,7 @@ const PREAMBLE_CODE: [string, string][] = [ ["SafeSlice", SAFE_SLICE], ["StringIndexOf", STRING_INDEX_OF], ["StringSplit", STRING_SPLIT], + ["SeqSortBy", SEQ_SORT_BY], ["StringTrim", STRING_TRIM], ["StringToLower", STRING_TO_LOWER], ["StringToUpper", STRING_TO_UPPER], diff --git a/tools/src/resolve.ts b/tools/src/resolve.ts index f7cfbf2..6cc4686 100644 --- a/tools/src/resolve.ts +++ b/tools/src/resolve.ts @@ -482,6 +482,16 @@ function tyToTsStr(ty: Ty): string | undefined { return undefined; } function inferLambdaParamTypes(fn: TExpr, rawArgs: RawExpr[], ctx?: Ctx): RawExpr[] { + // sort's comparator takes two params, both the element type. + if (fn.kind === "field" && fn.obj.ty.kind === "array" && fn.field === "sort" && + rawArgs.length >= 1 && rawArgs[0].kind === "lambda" && rawArgs[0].params.length >= 1) { + const tsType = tyToTsStr(fn.obj.ty.elem); + if (tsType) { + const lam = rawArgs[0]; + const updatedParams = lam.params.map(p => (p.tsType ? p : { ...p, tsType })); + return [{ ...lam, params: updatedParams }, ...rawArgs.slice(1)]; + } + } if (fn.kind === "field" && fn.obj.ty.kind === "array" && ["map", "filter", "every", "some", "find", "findLast", "findIndex"].includes(fn.field) && rawArgs.length >= 1 && rawArgs[0].kind === "lambda" && @@ -581,6 +591,7 @@ function inferMethodReturnTy(fn: TExpr, args: TExpr[], ctx: Ctx): Ty { if (fn.field === "shift") return objTy.elem; if (fn.field === "pop") return { kind: "optional", inner: objTy.elem }; if (fn.field === "push" || fn.field === "unshift" || fn.field === "concat") return objTy; + if (fn.field === "sort") return objTy; if (fn.field === "filter") return objTy; if (fn.field === "every" || fn.field === "some") return { kind: "bool" }; if (fn.field === "find" || fn.field === "findLast") return { kind: "optional", inner: objTy.elem }; diff --git a/tools/src/transform.ts b/tools/src/transform.ts index eaa1bc6..7f81360 100644 --- a/tools/src/transform.ts +++ b/tools/src/transform.ts @@ -1366,7 +1366,7 @@ function transformStmt(s: TStmt, typeDecls: TypeDeclInfo[]): Stmt[] { const f = s.expr.fn.field; const isMutating = ((recv.ty.kind === "map" || recv.ty.kind === "set") && (f === "set" || f === "add" || f === "delete")) || - (recv.ty.kind === "array" && (f === "push" || f === "unshift")); + (recv.ty.kind === "array" && (f === "push" || f === "unshift" || f === "sort")); if (isMutating && recv.kind === "var") { const { binds, expr } = liftMethodCalls(s.expr); return [...binds, { kind: "assign", target: recv.name, value: expr }]; From 1103970eb3fbb5c9e912a968c0413e931132c5e0 Mon Sep 17 00:00:00 2001 From: Nada Amin Date: Wed, 24 Jun 2026 23:58:18 -0400 Subject: [PATCH 2/2] example --- examples/sortBy.dfy | 19 +++++++++++++++++++ examples/sortBy.dfy.gen | 19 +++++++++++++++++++ examples/sortBy.ts | 22 ++++++++++++++++++++++ 3 files changed, 60 insertions(+) create mode 100644 examples/sortBy.dfy create mode 100644 examples/sortBy.dfy.gen create mode 100644 examples/sortBy.ts diff --git a/examples/sortBy.dfy b/examples/sortBy.dfy new file mode 100644 index 0000000..6271bd8 --- /dev/null +++ b/examples/sortBy.dfy @@ -0,0 +1,19 @@ +// Generated by lsc from sortBy.ts + +function {:axiom} SeqSortBy(s: seq, cmp: (T, T) -> int): seq + requires forall a: T, b: T :: cmp(a, b) <= 0 || cmp(b, a) <= 0 + requires forall a: T, b: T, c: T :: cmp(a, b) <= 0 && cmp(b, c) <= 0 ==> cmp(a, c) <= 0 + ensures multiset(SeqSortBy(s, cmp)) == multiset(s) + ensures |SeqSortBy(s, cmp)| == |s| + ensures forall i: int, j: int :: 0 <= i <= j < |SeqSortBy(s, cmp)| ==> cmp(SeqSortBy(s, cmp)[i], SeqSortBy(s, cmp)[j]) <= 0 + +datatype Rec = Rec(k: int) + +method sortByKey(input: seq) returns (res: seq) + ensures (|res| == |input|) + ensures forall i: nat :: (((i + 1) < |res|) ==> (res[i].k <= res[(i + 1)].k)) +{ + var xs := input; + xs := SeqSortBy(xs, (a: Rec, b: Rec) => (a.k - b.k)); + return xs; +} diff --git a/examples/sortBy.dfy.gen b/examples/sortBy.dfy.gen new file mode 100644 index 0000000..6271bd8 --- /dev/null +++ b/examples/sortBy.dfy.gen @@ -0,0 +1,19 @@ +// Generated by lsc from sortBy.ts + +function {:axiom} SeqSortBy(s: seq, cmp: (T, T) -> int): seq + requires forall a: T, b: T :: cmp(a, b) <= 0 || cmp(b, a) <= 0 + requires forall a: T, b: T, c: T :: cmp(a, b) <= 0 && cmp(b, c) <= 0 ==> cmp(a, c) <= 0 + ensures multiset(SeqSortBy(s, cmp)) == multiset(s) + ensures |SeqSortBy(s, cmp)| == |s| + ensures forall i: int, j: int :: 0 <= i <= j < |SeqSortBy(s, cmp)| ==> cmp(SeqSortBy(s, cmp)[i], SeqSortBy(s, cmp)[j]) <= 0 + +datatype Rec = Rec(k: int) + +method sortByKey(input: seq) returns (res: seq) + ensures (|res| == |input|) + ensures forall i: nat :: (((i + 1) < |res|) ==> (res[i].k <= res[(i + 1)].k)) +{ + var xs := input; + xs := SeqSortBy(xs, (a: Rec, b: Rec) => (a.k - b.k)); + return xs; +} diff --git a/examples/sortBy.ts b/examples/sortBy.ts new file mode 100644 index 0000000..d1f8f50 --- /dev/null +++ b/examples/sortBy.ts @@ -0,0 +1,22 @@ +/** + * In-place `Array.prototype.sort(cmp)` is modeled as reassignment to a + * permutation of the input sorted by the comparator (Dafny only). The model + * `requires` the comparator to be a total preorder — the soundness condition for + * a sorted permutation to exist — which the standard key-difference idiom + * `(a, b) => a.k - b.k` discharges automatically by linear arithmetic. The + * result is a same-length, same-multiset permutation, sorted ascending by key. + */ + +//@ backend dafny + +interface Rec { + k: number; +} + +export function sortByKey(input: Rec[]): Rec[] { + //@ ensures \result.length === input.length + //@ ensures forall(i: nat, i + 1 < \result.length ==> \result[i].k <= \result[i + 1].k) + const xs = input.slice(); + xs.sort((a, b) => a.k - b.k); + return xs; +}