lemmascript - npm Package Compare versions

Comparing version 0.5.15 to 0.5.16

package.json

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

README.md

@@ -33,2 +33,3 @@ # LemmaScript (Tech Preview)
 - **[pi-lemmascript](https://github.com/midspiral/pi-lemmascript/blob/lemmascript/README_LemmaScript.md)** — brownfield, **in-place** verification of the context-compaction cut-point selector in **pi** (the [earendil-works](https://pi.dev) agent harness). When the context window fills, pi discards history before a chosen cut; a provider API rejects a retained prefix containing an orphaned `toolResult` (a tool result whose tool call was cut away). Both selector functions proven: the cut never lets the kept suffix *start with* — nor *split a tool-use/tool-result run* into — an orphaned tool result, even across the backward metadata snap. The no-orphan result forced the session tree's tool-pairing ordering into an explicit `requires`. 4 VCs, 0 errors. Drove five toolchain additions, headlined by an **opaque fall-through type**: a union LemmaScript can't discriminate (here an array-element union of unreachable imports) becomes a single opaque `type` — the field stays present so distinct values stay distinct, and with no constructor or tag predicate it can only be passed through, never unsoundly observed. **Dafny + Lean**: the no-orphan theorem, the changelog semver core, and both tool-output truncators also carry Lean 4 (Velvet/Loom) proofs from the same annotated source, zero `sorry`; the Lean port drove the backend's brownfield batch (cross-file externs, union destructor lowering, Bool-vs-Prop contexts, `return`-in-loop elimination).
+- **[flue-lemmascript](https://github.com/midspiral/flue-lemmascript/blob/lemmascript/README_LemmaScript.md)** — brownfield, **in-place** verification of pure logic in **Flue** ([withastro/flue](https://github.com/withastro/flue)), Astro's agent harness — crash-recovery and context-compaction functions proven byte-identical. What it drove into the toolchain: native Dafny `continue`, bounds-guarded `noUncheckedIndexedAccess` optional indexing, optional narrowing past an `opt?.disc` guard composing with discriminated-union matching, and object truthiness. Dafny only.
 - **[balanced-match-lemmascript](https://github.com/midspiral/balanced-match-lemmascript/blob/lemmascript/README_LemmaScript.md)** — brownfield, **in-place** verification of [balanced-match](https://github.com/juliangruber/balanced-match), the ~70-line balanced-bracket finder pulled in by `npm`, `webpack`, and most of the JS tooling stack (1B+ downloads/month). The stack-based `range` core is verified by **refinement**: a pure recursive spec `range_spec` mirrors the loop one branch per recursive case, so the single equivalence `range == range_spec` transfers every property automatically — including an unconditional Dyck body-balance theorem for the interior of every returned pair. 2233 VCs, 0 errors under `--isolate-assertions` (registered on the `dafny-slow` track). Dafny only.
@@ -35,0 +36,0 @@ - **[guardians-lemmascript](https://github.com/midspiral/guardians-lemmascript)** — greenfield verification of the core safety argument behind [Guardians](https://github.com/metareflection/guardians) (Erik Meijer, "Guardians of the Agents", CACM Jan 2026), a generate-verify-execute checker for AI-agent workflows. Instead of verifying an app, it proves the agent *guardrail itself sound* — that a static taint/automaton check over the real recursive workflow AST can never admit an unsafe plan. Highlights: taint over **nested conditionals** as a sound branch-union over-approximation; per-source **provenance** with a join (a multi-input tool is tainted if *any* input was); **unbounded loops** discharged by a one-step pre-fixpoint (`sat = t0 ‖ bodyTaint(t0)`) that bounds taint over any iteration count without iterating to a fixpoint; and a **unified capstone** (`verifyWfSound`) — one clean verdict rules out, on *every* path, both a tainted-data-to-sink leak and a security-automaton error. 54 Dafny obligations, 0 errors. The verified cores are reached from a Guardians-style `Workflow`/`Policy` through a thin *unverified* adapter, differentially tested against the real Python Guardians (used as the oracle, not a porting target). Dafny only.

tools/dist/dafny-commands.js

@@ -70,3 +70,3 @@ /**
 }
-export function dafnyRegen(genPath, dfyPath, basePath, text, dir, timeLimit, extraFlags) {
+export function dafnyRegen(genPath, dfyPath, basePath, text, dir, timeLimit, extraFlags, noVerify = false) {
     // 1. Read old gen before overwriting (needed for base seeding)
@@ -80,3 +80,3 @@ const oldGen = existsSync(genPath) ? readFileSync(genPath, "utf-8") : "";
         console.log(`Created: ${path.basename(dfyPath)}`);
-        if (!dafnyVerify(dfyPath, dir, timeLimit, extraFlags)) {
+        if (!noVerify && !dafnyVerify(dfyPath, dir, timeLimit, extraFlags)) {
             console.error(`FAILED: ${path.basename(dfyPath)} verification failed on first run.`);
@@ -115,4 +115,4 @@ process.exit(1);
     }
-    // 7. Verify
-    if (!dafnyVerify(dfyPath, dir, timeLimit, extraFlags)) {
+    // 7. Verify (skipped under --no-verify: caller verifies separately)
+    if (!noVerify && !dafnyVerify(dfyPath, dir, timeLimit, extraFlags)) {
         console.error(`FAILED: ${path.basename(dfyPath)} verification failed.`);
@@ -119,0 +119,0 @@ process.exit(1);

tools/dist/ir.js

@@ -40,2 +40,4 @@ /**
         case "index": return anyExpr(e.arr, pred) || anyExpr(e.idx, pred);
+        case "tupleLiteral": return e.elems.some(x => anyExpr(x, pred));
+        case "tupleProj": return anyExpr(e.obj, pred);
         case "implies": return e.premises.some(p => anyExpr(p, pred)) || anyExpr(e.conclusion, pred);
@@ -42,0 +44,0 @@ case "record": return (e.spread ? anyExpr(e.spread, pred) : false) || e.fields.some(f => anyExpr(f.value, pred));

tools/dist/lean-emit.js

@@ -37,2 +37,9 @@ /**
         }
+        case "tuple":
+            // Right-nested Prod: `A × B × C` = `A × (B × C)`. Parenthesize any element
+            // whose rendering has a space so it binds tighter than `×` (e.g. `A → B`).
+            return ty.elems.map(el => {
+                const s = tyToLean(el);
+                return s.includes(" ") ? `(${s})` : s;
+            }).join(" × ");
         case "map": {
@@ -116,2 +123,5 @@ const k = tyToLean(ty.key);
             break;
+        case "tuple":
+            ty.elems.forEach(el => collectUserRefs(el, into));
+            break;
         case "optional":
@@ -323,2 +333,11 @@ collectUserRefs(ty.inner, into);
             return `#[${e.elems.map(el => emitExpr(el)).join(", ")}]`;
+        case "tupleLiteral":
+            return `(${e.elems.map(el => emitExpr(el)).join(", ")})`;
+        case "tupleProj": {
+            // Right-nested Prod projection: element i is `.2`×i then `.1`, except the
+            // last (i = arity-1) which is `.2`×i with no trailing `.1`.
+            const obj = emitExpr(e.obj);
+            const twos = ".2".repeat(e.index);
+            return e.index === e.arity - 1 ? `${obj}${twos}` : `${obj}${twos}.1`;
+        }
         case "emptyMap": return `Std.HashMap.empty`;
@@ -325,0 +344,0 @@ case "emptySet": return `Std.HashSet.empty`;

tools/dist/lsc.js

@@ -101,2 +101,12 @@ #!/usr/bin/env node
     }
+    // --no-verify (regen only): do regen + three-way merge + additions-only check
+    // but skip `dafny verify`. CI's `tools` job passes this to regen-dafny.sh so
+    // regen only enforces the drift + additions-only invariants; the separate
+    // `lsc check` pass over the same files does the one and only verification.
+    let noVerify = false;
+    const noVerifyIdx = args.indexOf("--no-verify");
+    if (noVerifyIdx >= 0) {
+        noVerify = true;
+        args.splice(noVerifyIdx, 1);
+    }
     // Anything flag-shaped left over is a typo or a space-separated form
@@ -121,3 +131,3 @@ // (`--backend lean`): reject it rather than let it become a positional arg
     }
-    runFile(cmd, filePath, backend, timeLimit, extraFlags);
+    runFile(cmd, filePath, backend, timeLimit, extraFlags, noVerify);
 }
@@ -159,3 +169,3 @@ // LemmaScript-files.txt, parsed: `filepath [timeout_in_seconds] [extra dafny
 }
-function runFile(cmd, filePath, backend, timeLimit, extraFlags) {
+function runFile(cmd, filePath, backend, timeLimit, extraFlags, noVerify = false) {
     const absPath = path.resolve(filePath);
@@ -253,3 +263,3 @@ if (!existsSync(absPath)) {
         if (cmd === "regen") {
-            dafnyRegen(genPath, dfyPath, basePath, text, dir, timeLimit, extraFlags);
+            dafnyRegen(genPath, dfyPath, basePath, text, dir, timeLimit, extraFlags, noVerify);
             return;
@@ -256,0 +266,0 @@ }

tools/dist/narrow.js

@@ -148,3 +148,3 @@ /**
     // inner shape doesn't match the simple rule directly.
-    return ruleIfAndOptional(r) ?? ruleIfAndArrayIsArray(r) ?? ruleIfOptionalSimple(r) ?? ruleExprStmtAndOptional(r) ?? r;
+    return ruleIfAndOptional(r) ?? ruleIfAndArrayIsArray(r) ?? ruleIfOptionalSimple(r) ?? ruleExprStmtAndOptional(r) ?? ruleOptionalIndexBinding(r) ?? r;
 }
@@ -163,3 +163,3 @@ function walkStmts(stmts) {
         }
-        const consumed = ruleEarlyReturnOrChain(s, rest) ?? ruleEarlyReturnConsume(s, rest);
+        const consumed = ruleEarlyReturnOrChain(s, rest) ?? ruleEarlyReturnConsume(s, rest) ?? ruleEarlyReturnOptChainCompare(s, rest);
         if (consumed) {
@@ -313,2 +313,51 @@ result.push(walkStmt(consumed));
 }
+/** Rule: `if (opt?.chain !== lit) terminate; rest` where `opt` is optional.
+ *  `opt?.chain` is `undefined` when `opt` is None, and `undefined !== lit` is
+ *  true, so the None case takes the terminating branch — falling through to
+ *  `rest` proves `opt` is Some. Rewrite to
+ *    someMatch opt { Some(v) => [if (v.chain !== lit) terminate; rest]; None => terminate }
+ *  narrowing `opt` to `v` across `rest` (transform substitutes the scrutinee) and
+ *  handing the now-non-optional inner guard to the ordinary rules (e.g.
+ *  discriminant narrowing). Bound-optional companion to ruleEarlyReturnConsume,
+ *  which handles only a bare presence check (`opt !== undefined`). Restricted to
+ *  `!==` so the None case is guaranteed to terminate. */
+function ruleEarlyReturnOptChainCompare(s, rest) {
+    if (s.kind !== "if")
+        return null;
+    if (rest.length === 0)
+        return null;
+    if (s.else.length !== 0 || !isTerminating(s.then))
+        return null;
+    const c = s.cond;
+    if (c.kind !== "binop" || c.op !== "!==")
+        return null;
+    const oc = c.left.kind === "optChain" ? c.left : c.right.kind === "optChain" ? c.right : null;
+    if (!oc || oc.kind !== "optChain" || oc.obj.ty.kind !== "optional")
+        return null;
+    const lit = c.left === oc ? c.right : c.left;
+    const innerTy = oc.obj.ty.inner;
+    const hint = binderHintFor(oc.obj);
+    if (hint === null)
+        return null;
+    const binder = freshName(hint);
+    const binderVar = { kind: "var", name: binder, ty: innerTy };
+    const unwrapped = applyChain(binderVar, oc.chain);
+    // applyChain rebuilds the field without the `isDiscriminant` flag resolve sets
+    // on a direct `x.disc`; restore it when the unwrapped access is the binder
+    // union's discriminant, so the inner guard feeds discriminant narrowing.
+    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 innerGuard = { kind: "binop", op: "!==", left: unwrapped, right: lit, ty: { kind: "bool" } };
+    // Keep `rest` as trailing statements (not an else branch) — `s.then` terminates,
+    // so `if (g) terminate; rest` ≡ `if (g) terminate else rest`, and the trailing
+    // form lets the ordinary early-exit rules (e.g. discriminant narrowing) fire on
+    // the now-non-optional inner guard when `chain` is a union discriminant.
+    const someBody = [{ kind: "if", cond: innerGuard, then: s.then, else: [] }, ...rest];
+    return { kind: "someMatch", scrutinee: oc.obj, binder, binderTy: innerTy, someBody, noneBody: s.then };
+}
 /** Rule (expression): `e !== undefined ? a : b`. */
@@ -497,2 +546,28 @@ function ruleConditionalOptionalSimple(e) {
 }
+/** Rule (statement): reconcile a `const e = arr[i]` whose binding is optional
+ *  (`e: T | undefined`) but whose array-index initializer is total (`T`). Model
+ *  the index as its JS semantics — `e := (0 <= i && i < arr.length) ? arr[i] :
+ *  undefined` — so `e` is a real `Option<T>` and a later `e?.f` someMatch is
+ *  well-typed; an in-bounds proof makes the None branch dead, so safely-indexed
+ *  code verifies as if total. Bound-form sibling of ruleOptChainIndex /
+ *  ruleNullishIndex. Fires purely on the optional-binding/total-index shape (the
+ *  usual source is `noUncheckedIndexedAccess`, but the flag itself is never
+ *  checked). Skipped when the element type is already optional: no mismatch. */
+function ruleOptionalIndexBinding(s) {
+    if (s.kind !== "let")
+        return null;
+    if (s.ty.kind !== "optional")
+        return null;
+    const init = s.init;
+    if (init.kind !== "index")
+        return null;
+    if (init.obj.ty.kind !== "array")
+        return null;
+    if (init.ty.kind === "optional")
+        return null; // array-of-optionals: not a flag artifact
+    const cond = arrayBoundsCond(init.obj, init.idx);
+    const undef = { kind: "var", name: "undefined", ty: { kind: "void" } };
+    const guarded = { kind: "conditional", cond, then: init, else: undef, ty: s.ty };
+    return { ...s, init: guarded };
+}
 /** Rule (expression): `obj?.<chain>` — single-eval optional chain.
@@ -499,0 +574,0 @@ *  → `someMatch obj { Some(_oc{N}_val) => apply(chain, _oc{N}_val), None => undefined }`.

tools/dist/peephole.js

@@ -27,2 +27,4 @@ import { patternCtor, patternBinders } from "./ir.js";
         case "index": return { ...e, arr: r(e.arr), idx: r(e.idx) };
+        case "tupleLiteral": return { ...e, elems: e.elems.map(r) };
+        case "tupleProj": return { ...e, obj: r(e.obj) };
         case "record": return { ...e, spread: e.spread ? r(e.spread) : null,
@@ -372,2 +374,4 @@ fields: e.fields.map(fi => ({ ...fi, value: r(fi.value) })) };
         case "index": return { ...e, arr: r(e.arr), idx: r(e.idx) };
+        case "tupleLiteral": return { ...e, elems: e.elems.map(r) };
+        case "tupleProj": return { ...e, obj: r(e.obj) };
         case "record": return { ...e, spread: e.spread ? r(e.spread) : null,
@@ -374,0 +378,0 @@ fields: e.fields.map(fi => ({ ...fi, value: r(fi.value) })) };

tools/dist/typedir.js

@@ -11,1 +11,37 @@ /**
 }
+/** Structural equality on Ty. Used to decide whether a tuple type is homogeneous
+ *  (all elements equal ⇒ lower to `seq`) vs heterogeneous (⇒ keep as `tuple`). */
+export function tyEqual(a, b) {
+    if (a.kind !== b.kind)
+        return false;
+    switch (a.kind) {
+        case "array": return tyEqual(a.elem, b.elem);
+        case "set": return tyEqual(a.elem, b.elem);
+        case "tuple": {
+            const bt = b;
+            return a.elems.length === bt.elems.length && a.elems.every((e, i) => tyEqual(e, bt.elems[i]));
+        }
+        case "map": {
+            const bm = b;
+            return tyEqual(a.key, bm.key) && tyEqual(a.value, bm.value);
+        }
+        case "optional": return tyEqual(a.inner, b.inner);
+        case "user": return a.name === b.name;
+        case "fn": {
+            const bf = b;
+            return a.params.length === bf.params.length
+                && a.params.every((p, i) => tyEqual(p, bf.params[i]))
+                && tyEqual(a.result, bf.result);
+        }
+        case "string": {
+            const bs = b;
+            return JSON.stringify(a.values ?? null) === JSON.stringify(bs.values ?? null);
+        }
+        case "int":
+        case "nat": return !!a.big === !!b.big;
+        case "bool":
+        case "real":
+        case "void":
+        case "unknown": return true; // no payload
+    }
+}

tools/dist/types.js

@@ -7,2 +7,3 @@ /**
  */
+import { tyEqual } from "./typedir.js";
 import { Node, Project, SyntaxKind } from "ts-morph";
@@ -94,6 +95,10 @@ /**
     if (Node.isTupleTypeNode(tn)) {
-        const elems = tn.getElements();
+        const elems = tn.getElements().map(tyFromTypeNode);
         if (elems.length === 0)
             return { kind: "array", elem: { kind: "unknown" } };
-        return { kind: "array", elem: tyFromTypeNode(elems[0]) };
+        // Homogeneous tuple → seq; only heterogeneous tuples need the tuple
+        // representation.
+        if (elems.every(e => tyEqual(e, elems[0])))
+            return { kind: "array", elem: elems[0] };
+        return { kind: "tuple", elems };
     }
@@ -163,2 +168,3 @@ if (Node.isFunctionTypeNode(tn)) {
         case "array": return `seq<${tyToCanonical(ty.elem)}>`;
+        case "tuple": return `(${ty.elems.map(tyToCanonical).join(", ")})`;
         case "map": return `map<${tyToCanonical(ty.key)}, ${tyToCanonical(ty.value)}>`;
@@ -165,0 +171,0 @@ case "set": return `set<${tyToCanonical(ty.elem)}>`;

No alert changes

Improved metrics

Total package byte prevSize

634411

1.73%

Lines of code

12393

1.56%

Number of lines in readme file

121

0.83%

Worsened metrics

Published versions last week

0

-100%

No dependency changes