sortby

examples/sortBy.dfy

@@ -0,0 +1,19 @@
+// Generated by lsc from sortBy.ts
+
+function {:axiom} SeqSortBy<T(==,!new)>(s: seq<T>, cmp: (T, T) -> int): seq<T>
+  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<Rec>) returns (res: seq<Rec>)
+  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;
+}

examples/sortBy.dfy.gen

@@ -0,0 +1,19 @@
+// Generated by lsc from sortBy.ts
+
+function {:axiom} SeqSortBy<T(==,!new)>(s: seq<T>, cmp: (T, T) -> int): seq<T>
+  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<Rec>) returns (res: seq<Rec>)
+  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;
+}

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;
+}

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<s
   ensures |StringSplit(s, d)| <= |s| + 1
   ensures forall k :: 0 <= k < |StringSplit(s, d)| ==> |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<T(==,!new)>(s: seq<T>, cmp: (T, T) -> int): seq<T>
+  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],

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

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 }];