lemmascript - npm Package Compare versions

Comparing version 0.5.16 to 0.5.17

package.json

 {
   "name": "lemmascript",
-  "version": "0.5.16",
+  "version": "0.5.17",
   "description": "A verification toolchain for TypeScript — generates Lean 4 or Dafny from annotated TS",
@@ -5,0 +5,0 @@ "type": "module",

README.md

@@ -89,2 +89,48 @@ # LemmaScript (Tech Preview)
 
+## Continuous Integration
+
+LemmaScript ships a **reusable GitHub Actions workflow** that regenerates your artifacts, verifies them, and fails the build if any committed generated file is out of date. Call it from your own repo's workflow:
+
+```yaml
+# .github/workflows/lemmascript.yml
+name: LemmaScript
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+    branches: [main]
+
+jobs:
+  verify:
+    uses: midspiral/LemmaScript/.github/workflows/verify.yml@main
+    with:
+      backend: dafny      # dafny | lean | dafny-slow
+```
+
+The workflow installs the toolchain and (per `backend`) the Dafny or Lean stack, then runs `tools/check.sh`, which batches over a **`LemmaScript-files.txt`** at your repo root. This file is the list of sources CI verifies — you create and maintain it. One entry per line, `filepath [timeout] [extra dafny flags…]`:
+
+```
+src/domain.ts
+src/patch.ts 120
+src/heavy.ts 300 --isolate-assertions
+```
+
+The optional second column is a per-file timeout in seconds; anything after it is passed verbatim to Dafny. The same list drives `lsc check` locally when you run it with no file argument, so CI and your local runs verify exactly the same set. To verify additional Dafny files outside that list, add an executable `check-extra.sh` at the root and it runs automatically (Dafny backends only).
+
+Inputs (all optional):
+
+| Input | Default | Purpose |
+|-------|---------|---------|
+| `backend` | `dafny` | `dafny`, `lean`, or `dafny-slow` (isolate-assertions / long-running proofs) |
+| `node-version` | `24` | Node.js version |
+| `ls-ref` | `main` | LemmaScript ref to verify against |
+| `typecheck` | `true` | Run `npm ci && npm run typecheck` in the calling repo first |
+
+To verify against **both** backends, add a second job with `backend: lean`.
+
+Examples:
+- **[talktimer-lemmascript](https://github.com/midspiral/talktimer-lemmascript/blob/main/.github/workflows/lemmascript.yml)** — Dafny-only.
+- **[pi-lemmascript](https://github.com/midspiral/pi-lemmascript/blob/lemmascript/.github/workflows/lemmascript.yml)** — Dafny + Lean (two jobs).
+
 ## Annotations
@@ -91,0 +137,0 @@

tools/dist/lean-emit.js

@@ -239,2 +239,4 @@ /**
             return `${obj}.${monadic ? "anyM" : "any"} ${args[0]}`;
+        if (method === "reduce" && args.length === 2)
+            return `(${obj}.foldl ${args[0]} ${args[1]})`;
         if (method === "includes")
@@ -480,4 +482,9 @@ return args.length > 1 ? `(${obj}.extract ${args[1]} ${obj}.size).contains ${args[0]}` : `${obj}.contains ${args[0]}`;
             throw new Error("real arithmetic is not supported by the Lean backend (needs noncomputable ℝ / Mathlib).");
-        case "index":
-            return `${emitExpr(e.arr)}[${emitExpr(e.idx)}]!`;
+        case "index": {
+            const arr = emitExpr(e.arr);
+            // Parenthesize a low-precedence array expr (e.g. a function application)
+            // so the index binds to the whole thing, not its last token.
+            const wrap = e.arr.kind === "app" || e.arr.kind === "binop" || e.arr.kind === "methodCall" || e.arr.kind === "if" || e.arr.kind === "let" || e.arr.kind === "unop";
+            return `${wrap ? `(${arr})` : arr}[${emitExpr(e.idx)}]!`;
+        }
         case "record": {
@@ -657,2 +664,55 @@ const fields = e.fields.map(f => `${escapeName(f.name)} := ${emitExpr(f.value)}`);
 // ── Declaration emission ─────────────────────────────────────
+/** Collect every function/variable name an IR tree references (stripping any
+ *  `Pure.` qualifier), via a generic walk over `app`/`var` nodes. */
+function collectRefNames(node, into) {
+    if (node === null || typeof node !== "object")
+        return;
+    if (Array.isArray(node)) {
+        for (const x of node)
+            collectRefNames(x, into);
+        return;
+    }
+    const n = node;
+    if (n.kind === "app" && typeof n.fn === "string")
+        into.add(n.fn.replace(/^Pure\./, ""));
+    if (n.kind === "var" && typeof n.name === "string")
+        into.add(n.name.replace(/^Pure\./, ""));
+    for (const k of Object.keys(node))
+        collectRefNames(node[k], into);
+}
+/** Lean requires definition-before-use: order sibling decls so one that
+ *  references another is emitted after it. Cycles are left in place (they would
+ *  need a `mutual` block). Bails to the original order if any decl is unnamed. */
+function orderDeclsByDeps(decls) {
+    const named = decls.filter((d) => typeof d.name === "string");
+    if (named.length !== decls.length)
+        return decls;
+    const names = new Set(named.map(d => d.name));
+    const byName = new Map(named.map(d => [d.name, d]));
+    const deps = new Map();
+    for (const d of named) {
+        const refs = new Set();
+        collectRefNames(d, refs);
+        refs.delete(d.name);
+        deps.set(d.name, [...refs].filter(r => names.has(r)));
+    }
+    const sorted = [];
+    const done = new Set();
+    const onStack = new Set();
+    const visit = (name) => {
+        if (done.has(name) || onStack.has(name))
+            return;
+        onStack.add(name);
+        for (const dep of deps.get(name) ?? [])
+            visit(dep);
+        onStack.delete(name);
+        done.add(name);
+        const def = byName.get(name);
+        if (def)
+            sorted.push(def);
+    };
+    for (const d of named)
+        visit(d.name);
+    return sorted;
+}
 function emitDecl(d) {
@@ -736,3 +796,3 @@ switch (d.kind) {
             const lines = [`namespace ${d.name}`];
-            for (const inner of d.decls)
+            for (const inner of orderDeclsByDeps(d.decls))
                 lines.push("", emitDecl(inner));
@@ -759,4 +819,6 @@ lines.push("", `end ${d.name}`);
             // the proof automation can use it, matching the ghost-function convention.
-            const hyps = d.requires.map(emitExpr);
-            const concl = d.ensures.map(emitExpr).join(" ∧ ");
+            // Parenthesize each clause: an unwrapped `∀ k, P` would otherwise swallow
+            // the following ` ∧ …` conjuncts into its body.
+            const hyps = d.requires.map(e => `(${emitExpr(e)})`);
+            const concl = d.ensures.map(e => `(${emitExpr(e)})`).join(" ∧ ");
             const axBody = [...hyps, concl].join(" → ");
@@ -763,0 +825,0 @@ const axiom = `@[grind] axiom ${escapeName(d.name)}_spec${params ? ` ${params}` : ""} : ${axBody}`;

tools/dist/narrow.js

@@ -263,20 +263,44 @@ /**
 }
-/** Collect a `||` chain of negative optional checks (`x === undefined`).
- *  Returns the list of checks if every leaf is a negative optional check; null otherwise. */
-function collectOrChainOfNegativeChecks(cond) {
-    if (cond.kind === "binop" && cond.op === "||") {
-        const left = collectOrChainOfNegativeChecks(cond.left);
-        const right = collectOrChainOfNegativeChecks(cond.right);
-        if (!left || !right)
-            return null;
-        return [...left, ...right];
+/** Flatten a nested `||` chain into its leaf conditions. */
+function flattenOr(e) {
+    if (e.kind === "binop" && e.op === "||")
+        return [...flattenOr(e.left), ...flattenOr(e.right)];
+    return [e];
+}
+function classifyDisjunct(leaf) {
+    // `x?.chain !== lit` — `undefined !== lit` is true when x is None.
+    if (leaf.kind === "binop" && leaf.op === "!==") {
+        const oc = leaf.left.kind === "optChain" ? leaf.left : leaf.right.kind === "optChain" ? leaf.right : null;
+        if (oc && oc.kind === "optChain" && oc.obj.ty.kind === "optional") {
+            const hint = binderHintFor(oc.obj);
+            if (hint === null)
+                return null;
+            const binder = freshName(hint);
+            const unwrapped = applyChain({ kind: "var", name: binder, ty: oc.obj.ty.inner }, oc.chain);
+            if (unwrapped.kind === "field" && unwrapped.obj.ty.kind === "user") {
+                const base = unwrapped.obj.ty.name.replace(/<.*/, "");
+                const decl = _typeDecls.find(d => d.name === base);
+                if (decl?.kind === "discriminated-union" && decl.discriminant === unwrapped.field)
+                    unwrapped.isDiscriminant = true;
+            }
+            const lit = leaf.left === oc ? leaf.right : leaf.left;
+            return { scrutinee: oc.obj, innerTy: oc.obj.ty.inner, binder, residual: { kind: "binop", op: "!==", left: unwrapped, right: lit, ty: { kind: "bool" } } };
+        }
     }
-    const check = parseSimpleOptionalCheck(cond);
-    if (!check || !check.negated)
-        return null;
-    return [check];
+    // `!x` / `x === undefined`.
+    const chk = parseOptionalCheck(leaf);
+    if (chk && chk.negated) {
+        const residual = canBeFalsy(chk)
+            ? { kind: "unop", op: "!", expr: { kind: "var", name: chk.binderHint, ty: chk.innerTy }, ty: { kind: "bool" } }
+            : null;
+        return { scrutinee: chk.scrutinee, innerTy: chk.innerTy, binder: chk.binderHint, residual };
+    }
+    return null;
 }
-/** Rule: `if (x === undefined || y === undefined || ...) terminate; rest`.
- *  → nested someMatches narrowing each var in turn, each None branch = terminate,
- *    deepest someBody = rest.
+/** Rule: `if (D1 || … || Dn) terminate; rest`. Each `Di` that detects some optional
+ *  `x` is None (`!x`, `x === undefined`, `x?.chain !== lit`) narrows that `x` to Some
+ *  across `rest`; the rest — value guards reading a narrowed `x` directly, plus the
+ *  detectors' Some-case residuals — become a trailing early-return. Sound: reaching
+ *  `rest` means every disjunct was false, so every detected optional is present.
+ *  Covers `if (!x || x.f !== v) continue` / `if (x?.t !== 'm' || x.g) break`.
  *  Closes the resolve.ts:602 TODO ("|| narrowing"). */
@@ -288,24 +312,35 @@ function ruleEarlyReturnOrChain(s, rest) {
         return null;
-    if (s.then.length === 0 || s.else.length !== 0)
+    if (s.then.length === 0 || s.else.length !== 0 || !isTerminating(s.then))
         return null;
     if (s.cond.kind !== "binop" || s.cond.op !== "||")
         return null; // single check is the simpler rule
-    const checks = collectOrChainOfNegativeChecks(s.cond);
-    if (!checks || checks.length < 2)
+    const leaves = flattenOr(s.cond);
+    if (leaves.length < 2)
         return null;
-    // Build nested someMatch from innermost outward
-    let inner = rest;
-    for (let i = checks.length - 1; i >= 0; i--) {
-        const check = checks[i];
-        const someBody = canBeFalsy(check)
-            ? [{ kind: "if", cond: bound(check), then: inner, else: s.then }]
-            : inner;
-        inner = [{
-                kind: "someMatch",
-                scrutinee: check.scrutinee, binderTy: check.innerTy,
-                binder: check.binderHint,
-                someBody,
-                noneBody: s.then,
-            }];
+    const detectors = [];
+    const residualLeaves = [];
+    const seen = new Set();
+    for (const leaf of leaves) {
+        const d = classifyDisjunct(leaf);
+        if (!d) {
+            residualLeaves.push(leaf);
+            continue;
+        }
+        const key = binderHintFor(d.scrutinee);
+        if (seen.has(key))
+            return null; // two detectors on one optional: rare; leave to other rules
+        seen.add(key);
+        detectors.push(d);
+        if (d.residual)
+            residualLeaves.push(d.residual);
     }
+    if (detectors.length === 0)
+        return null;
+    let inner = residualLeaves.length === 0
+        ? rest
+        : [{ kind: "if", cond: residualLeaves.reduce((a, b) => ({ kind: "binop", op: "||", left: a, right: b, ty: { kind: "bool" } })), then: s.then, else: [] }, ...rest];
+    for (let i = detectors.length - 1; i >= 0; i--) {
+        const d = detectors[i];
+        inner = [{ kind: "someMatch", scrutinee: d.scrutinee, binderTy: d.innerTy, binder: d.binder, someBody: inner, noneBody: s.then }];
+    }
     return inner[0];
@@ -312,0 +347,0 @@ }

No alert changes

Improved metrics

Total package byte prevSize

645519

1.75%

Lines of code

12570

1.43%

Number of lines in readme file

167

38.02%

No dependency changes