more ops, and update docs

SPEC.md

@@ -167,7 +167,7 @@ When imported types can't be resolved by ts-morph (e.g., in monorepos with bundl
 //@ declare-type Rect { x: number, y: number, width: number, height: number }
 ```
 
-Each `declare-type` generates a Dafny `datatype` (or Lean `structure`) with the given fields. Field types use TS syntax (`number`, `string`, `boolean`, `T[]`, etc.) and are mapped through the standard type rules (§6.1).
+Each `declare-type` generates a Dafny `datatype` (or Lean `structure`) with the given fields. Fields separate on `,` or `;` (TS object types accept either). Field types use TS syntax (`number`, `string`, `boolean`, `T[]`, etc.) and are mapped through the standard type rules (§6.1).
 
 Place `declare-type` annotations before the first function that uses the type. They can appear as leading comments on any statement. `declare-type` takes precedence over any type/interface of the same name in the source file, and is never filtered out by brownfield mode.
 
@@ -478,18 +478,21 @@ The same coercion applies to non-bool conditions in `if`/`while`/`?:` positions:
 | `arr.find((x) => e)` | `arr.find? (fun x => e)` | — |
 | `arr.findIndex((x) => e)` | — | `SeqFindIndex(arr, (x) => e)` (preamble: `-1 ⇔ no match`, `≥0 ⇔ first match with no earlier match`) |
 | `arr.findLast((x) => e)` | — | `SeqFindLast(arr, (x) => e)` (preamble) |
+| `arr.findLastIndex((x) => e)` | — | `SeqFindLastIndex(arr, (x) => e)` (preamble: `-1 ⇔ no match`, `≥0 ⇔ last match with no later match`) |
 | `arr.flat()` | — | `SeqFlatten(arr)` (preamble) |
 | `arr.join(sep)` | `(String.intercalate sep arr.toList)` | `SeqJoin(arr, sep)` (preamble) |
 | `arr.shift()` | — | `arr[0]` + `arr := arr[1..]` |
 | `arr.pop()` | — | `(if \|arr\|>0 then Some(arr[\|arr\|-1]) else None)` + `arr := (if \|arr\|>0 then arr[..\|arr\|-1] else arr)` |
 | `arr.unshift(e)` | `(#[e] ++ arr)` (mutating → reassignment) | `([e] + arr)` (mutating → reassignment) |
 | `arr.sort(cmp)` | — | `SeqSortBy(arr, cmp)` (preamble axiom: permutation + length-preserving + sorted; mutating; `requires` cmp a total preorder) |
+| `arr.sort()` (no comparator) | — | `SeqSort(arr)` (preamble axiom: permutation + length-preserving only — JS default order is type-dependent) |
 | `arr.slice(start)` | `arr.extract start arr.size` | `arr[start..]` |
 | `arr.slice(start, end)` | `arr.extract start end` | `arr[start..end]` |
 | `expr!` (non-null) | unwrap Option | unwrap Option / direct map access |
 | `expr \|\| default` (on optional) | match Some/None | `match { Some(v) => v, None => default }` |
 | `expr \|\| undefined` (on optional) | identity | identity (no-op) |
 | `expr \|\| default` (on string) | if non-empty | `if \|expr\| > 0 then expr else default` |
+| `expr \|\| default` (on number) | if nonzero | `if expr != 0 then expr else default` |
 | `expr \|\| default` (on array) | `expr` (arrays are always truthy) | `expr` (arrays are always truthy) |
 | `expr?.method(args)` | — | `if key in map { ... }` |
 | `expr as T` | stripped | stripped |

tools/src/dafny-emit.ts

@@ -262,7 +262,10 @@ 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]})`; }
+        if (e.method === "sort")     {
+          if (args.length === 0) { needPreamble("SeqSort"); return `SeqSort(${obj})`; }
+          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;
@@ -291,6 +294,10 @@ function emitExpr(e: Expr): string {
           needPreamble("SeqFindIndex");
           return `SeqFindIndex(${obj}, ${args[0]})`;
         }
+        if (e.method === "findLastIndex") {
+          needPreamble("SeqFindLastIndex");
+          return `SeqFindLastIndex(${obj}, ${args[0]})`;
+        }
         if (e.method === "flat" && args.length === 0) {
           needPreamble("SeqFlatten");
           return `SeqFlatten(${obj})`;
@@ -954,6 +961,19 @@ function SeqIndexOfFrom<T(==)>(s: seq<T>, x: T, from: nat): int
   else SeqIndexOfFrom(s, x, from + 1)
 }`;
 
+const SEQ_FIND_LAST_INDEX = `function SeqFindLastIndex<T>(s: seq<T>, p: T -> bool): int
+  ensures -1 <= SeqFindLastIndex(s, p) < |s|
+  ensures SeqFindLastIndex(s, p) >= 0 ==> p(s[SeqFindLastIndex(s, p)])
+  ensures SeqFindLastIndex(s, p) >= 0 ==>
+    (forall j: int :: SeqFindLastIndex(s, p) < j < |s| ==> !p(s[j]))
+  ensures SeqFindLastIndex(s, p) == -1 ==> (forall i: nat :: i < |s| ==> !p(s[i]))
+  decreases |s|
+{
+  if |s| == 0 then -1
+  else if p(s[|s|-1]) then |s| - 1
+  else SeqFindLastIndex(s[..|s|-1], p)
+}`;
+
 const SEQ_FIND_LAST = `function SeqFindLast<T>(s: seq<T>, p: T -> bool): Option<T>
   ensures SeqFindLast(s, p).Some? ==> p(SeqFindLast(s, p).value)
   ensures SeqFindLast(s, p).Some? ==> SeqFindLast(s, p).value in s
@@ -1034,6 +1054,11 @@ const STRING_SPLIT = `function {:axiom} StringSplit(s: string, d: string): seq<s
 // 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).
+// Bare `.sort()`: permutation only, no sortedness (JS default order is type-dependent).
+const SEQ_SORT = `function {:axiom} SeqSort<T(==,!new)>(s: seq<T>): seq<T>
+  ensures multiset(SeqSort(s)) == multiset(s)
+  ensures |SeqSort(s)| == |s|`;
+
 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
@@ -1216,13 +1241,15 @@ const PREAMBLE_CODE: [string, string][] = [
   ["FloorReal", FLOOR_REAL],
   ["SeqIndexOf", SEQ_INDEX_OF],
   ["SeqFindIndex", SEQ_FIND_INDEX],
+  ["SeqFindLastIndex", SEQ_FIND_LAST_INDEX],
   ["SeqFilterSome", SEQ_FILTER_SOME],
   ["SeqFindLast", SEQ_FIND_LAST],
   ["SeqFlatten", SEQ_FLATTEN],
   ["SeqJoin", SEQ_JOIN],
   ["SafeSlice", SAFE_SLICE],
   ["StringIndexOf", STRING_INDEX_OF],
   ["StringSplit", STRING_SPLIT],
+  ["SeqSort", SEQ_SORT],
   ["SeqSortBy", SEQ_SORT_BY],
   ["StringTrim", STRING_TRIM],
   ["StringToLower", STRING_TO_LOWER],

tools/src/resolve.ts

@@ -496,7 +496,7 @@ function inferLambdaParamTypes(fn: TExpr, rawArgs: RawExpr[], ctx?: Ctx): RawExp
     }
   }
   if (fn.kind === "field" && fn.obj.ty.kind === "array" &&
-      ["map", "filter", "every", "some", "find", "findLast", "findIndex"].includes(fn.field) &&
+      ["map", "filter", "every", "some", "find", "findLast", "findIndex", "findLastIndex"].includes(fn.field) &&
       rawArgs.length >= 1 && rawArgs[0].kind === "lambda" &&
       rawArgs[0].params.length >= 1 && !rawArgs[0].params[0].tsType) {
     const elemTy = fn.obj.ty.elem;
@@ -598,7 +598,7 @@ function inferMethodReturnTy(fn: TExpr, args: TExpr[], ctx: Ctx): Ty {
     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 };
-    if (fn.field === "findIndex") return { kind: "int" };
+    if (fn.field === "findIndex" || fn.field === "findLastIndex") return { kind: "int" };
     if (fn.field === "flat" && objTy.elem.kind === "array") return { kind: "array", elem: objTy.elem.elem };
     if (fn.field === "slice") return objTy;
     if (fn.field === "join" && objTy.elem.kind === "string") return { kind: "string" };