From 26beccf1b02e42aa2c014d447df5415a0453fb72 Mon Sep 17 00:00:00 2001 From: Nada Amin Date: Thu, 25 Jun 2026 21:16:29 -0400 Subject: [PATCH 1/2] lift closures --- examples/closureLift.def.lean | 39 +++++ examples/closureLift.dfy | 45 ++++++ examples/closureLift.dfy.gen | 45 ++++++ examples/closureLift.proof.lean | 7 + examples/closureLift.ts | 40 +++++ examples/closureLift.types.lean | 9 ++ examples/liftThunk.def.lean | 43 ++++++ examples/liftThunk.dfy | 49 +++++++ examples/liftThunk.dfy.gen | 49 +++++++ examples/liftThunk.ts | 30 ++++ examples/liftThunk.types.lean | 9 ++ lakefile.lean | 4 +- tools/src/liftclosures.ts | 249 ++++++++++++++++++++++++++++++++ tools/src/lsc.ts | 5 +- 14 files changed, 621 insertions(+), 2 deletions(-) create mode 100644 examples/closureLift.def.lean create mode 100644 examples/closureLift.dfy create mode 100644 examples/closureLift.dfy.gen create mode 100644 examples/closureLift.proof.lean create mode 100644 examples/closureLift.ts create mode 100644 examples/closureLift.types.lean create mode 100644 examples/liftThunk.def.lean create mode 100644 examples/liftThunk.dfy create mode 100644 examples/liftThunk.dfy.gen create mode 100644 examples/liftThunk.ts create mode 100644 examples/liftThunk.types.lean create mode 100644 tools/src/liftclosures.ts diff --git a/examples/closureLift.def.lean b/examples/closureLift.def.lean new file mode 100644 index 0000000..3cc8187 --- /dev/null +++ b/examples/closureLift.def.lean @@ -0,0 +1,39 @@ +/- + Generated by lsc from closureLift.ts + Do not edit — re-run `lsc gen` to regenerate. +-/ +import «closureLift.types» + +set_option loom.semantics.termination "total" +set_option loom.semantics.choice "demonic" + +method flush (result : Array Int) (pending : Array Int) return (res : FlushState) + ensures (res.result).size ≥ result.size + do + let mut out : Array Int := result + for _x_idx in [:pending.size] + invariant _x_idx ≤ pending.size + invariant out.size ≥ result.size + do + let x := pending[_x_idx]! + out := out ++ #[x] + return { result := out, pending := #[] } + +method transform (items : Array (Array Int)) return (res : Array Int) + do + let mut result : Array Int := #[] + let mut pending : Array Int := #[] + for _batch_idx in [:items.size] + invariant _batch_idx ≤ items.size + do + let batch := items[_batch_idx]! + for _x_idx in [:batch.size] + invariant _x_idx ≤ batch.size + do + let x := batch[_x_idx]! + pending := pending ++ #[x] + let _t0 ← flush result pending + let s := _t0 + result := s.result + pending := s.pending + return result diff --git a/examples/closureLift.dfy b/examples/closureLift.dfy new file mode 100644 index 0000000..9901ae7 --- /dev/null +++ b/examples/closureLift.dfy @@ -0,0 +1,45 @@ +// Generated by lsc from closureLift.ts + +datatype FlushState = FlushState(result: seq, pending: seq) + +method flush(result: seq, pending: seq) returns (res: FlushState) + ensures (|res.result| >= |result|) +{ + var out := result; + var i_x_idx := 0; + while i_x_idx < |pending| + invariant (i_x_idx <= |pending|) + invariant (|out| >= |result|) + { + var x := pending[i_x_idx]; + out := (out + [x]); + i_x_idx := i_x_idx + 1; + } + return FlushState(out, []); +} + +method transform(items: seq>) returns (res: seq) +{ + var result: seq := []; + var pending: seq := []; + var i_batch_idx := 0; + while i_batch_idx < |items| + invariant (i_batch_idx <= |items|) + { + var batch := items[i_batch_idx]; + var i_x_idx := 0; + while i_x_idx < |batch| + invariant (i_x_idx <= |batch|) + { + var x := batch[i_x_idx]; + pending := (pending + [x]); + i_x_idx := i_x_idx + 1; + } + var i_t0 := flush(result, pending); + var s := i_t0; + result := s.result; + pending := s.pending; + i_batch_idx := i_batch_idx + 1; + } + return result; +} diff --git a/examples/closureLift.dfy.gen b/examples/closureLift.dfy.gen new file mode 100644 index 0000000..9901ae7 --- /dev/null +++ b/examples/closureLift.dfy.gen @@ -0,0 +1,45 @@ +// Generated by lsc from closureLift.ts + +datatype FlushState = FlushState(result: seq, pending: seq) + +method flush(result: seq, pending: seq) returns (res: FlushState) + ensures (|res.result| >= |result|) +{ + var out := result; + var i_x_idx := 0; + while i_x_idx < |pending| + invariant (i_x_idx <= |pending|) + invariant (|out| >= |result|) + { + var x := pending[i_x_idx]; + out := (out + [x]); + i_x_idx := i_x_idx + 1; + } + return FlushState(out, []); +} + +method transform(items: seq>) returns (res: seq) +{ + var result: seq := []; + var pending: seq := []; + var i_batch_idx := 0; + while i_batch_idx < |items| + invariant (i_batch_idx <= |items|) + { + var batch := items[i_batch_idx]; + var i_x_idx := 0; + while i_x_idx < |batch| + invariant (i_x_idx <= |batch|) + { + var x := batch[i_x_idx]; + pending := (pending + [x]); + i_x_idx := i_x_idx + 1; + } + var i_t0 := flush(result, pending); + var s := i_t0; + result := s.result; + pending := s.pending; + i_batch_idx := i_batch_idx + 1; + } + return result; +} diff --git a/examples/closureLift.proof.lean b/examples/closureLift.proof.lean new file mode 100644 index 0000000..b50d467 --- /dev/null +++ b/examples/closureLift.proof.lean @@ -0,0 +1,7 @@ +import «closureLift.def» + +set_option loom.semantics.termination "total" +set_option loom.semantics.choice "demonic" + +prove_correct flush by + loom_solve diff --git a/examples/closureLift.ts b/examples/closureLift.ts new file mode 100644 index 0000000..b281a95 --- /dev/null +++ b/examples/closureLift.ts @@ -0,0 +1,40 @@ +/** + * Lean gate for the targeted closure lift (DESIGN_CLOSURE_TARGET.md §6). + * + * This is the *post-lift* shape, written by hand (the lift pass doesn't exist yet): + * a record-returning routine with a loop — which emits as a Velvet `method` returning + * a structure — that is called from a loop-bearing caller threading the returned state + * back into its own mutable locals. The open question was whether loom threads exactly + * this (record return + call from inside a `for … do`). If `lake build` is green, it does. + */ + +interface FlushState { result: number[]; pending: number[] } + +/** The lifted thunk: captured state in by value, mutated state out as a record. + * A record-returning method carrying a postcondition through its loop. */ +export function flush(result: number[], pending: number[]): FlushState { + //@ verify + //@ ensures \result.result.length >= result.length + let out = result; + for (const x of pending) { + //@ invariant out.length >= result.length + out = out.concat([x]); + } + return { result: out, pending: [] }; +} + +/** The loop-bearing caller: at each boundary, call flush and thread the record back. */ +export function transform(items: number[][]): number[] { + //@ verify + let result: number[] = []; + let pending: number[] = []; + for (const batch of items) { + for (const x of batch) { + pending = pending.concat([x]); + } + const s = flush(result, pending); + result = s.result; + pending = s.pending; + } + return result; +} diff --git a/examples/closureLift.types.lean b/examples/closureLift.types.lean new file mode 100644 index 0000000..2f315ac --- /dev/null +++ b/examples/closureLift.types.lean @@ -0,0 +1,9 @@ +/- + Generated by lsc — Lean types and pure function mirrors. +-/ +import LemmaScript + +structure FlushState where + result : Array Int + pending : Array Int +deriving Repr, Inhabited, DecidableEq diff --git a/examples/liftThunk.def.lean b/examples/liftThunk.def.lean new file mode 100644 index 0000000..b5f9afa --- /dev/null +++ b/examples/liftThunk.def.lean @@ -0,0 +1,43 @@ +/- + Generated by lsc from liftThunk.ts + Do not edit — re-run `lsc gen` to regenerate. +-/ +import «liftThunk.types» + +set_option loom.semantics.termination "total" +set_option loom.semantics.choice "demonic" + +method flush (pending : Array Int) (result : Array Int) return (res : FlushState) + do + let mut pending : Array Int := pending + let mut result : Array Int := result + for _x_idx in [:pending.size] + invariant _x_idx ≤ pending.size + do + let x := pending[_x_idx]! + result := Array.push result x + pending := #[] + return { pending := pending, result := result } + +method transform (items : Array (Array Int)) return (res : Array Int) + do + let mut result : Array Int := #[] + let mut pending : Array Int := #[] + for _batch_idx in [:items.size] + invariant _batch_idx ≤ items.size + do + let batch := items[_batch_idx]! + for _x_idx in [:batch.size] + invariant _x_idx ≤ batch.size + do + let x := batch[_x_idx]! + pending := pending ++ #[x] + let _t0 ← flush pending result + let _lc0 := _t0 + pending := _lc0.pending + result := _lc0.result + let _t1 ← flush pending result + let _lc1 := _t1 + pending := _lc1.pending + result := _lc1.result + return result diff --git a/examples/liftThunk.dfy b/examples/liftThunk.dfy new file mode 100644 index 0000000..18543f5 --- /dev/null +++ b/examples/liftThunk.dfy @@ -0,0 +1,49 @@ +// Generated by lsc from liftThunk.ts + +datatype FlushState = FlushState(pending: seq, result: seq) + +method flush(pending: seq, result: seq) returns (res: FlushState) +{ + var pending := pending; + var result := result; + var i_x_idx := 0; + while i_x_idx < |pending| + invariant (i_x_idx <= |pending|) + { + var x := pending[i_x_idx]; + result := (result + [x]); + i_x_idx := i_x_idx + 1; + } + pending := []; + return FlushState(pending, result); +} + +method transform(items: seq>) returns (res: seq) +{ + var result: seq := []; + var pending: seq := []; + var i_batch_idx := 0; + while i_batch_idx < |items| + invariant (i_batch_idx <= |items|) + { + var batch := items[i_batch_idx]; + var i_x_idx := 0; + while i_x_idx < |batch| + invariant (i_x_idx <= |batch|) + { + var x := batch[i_x_idx]; + pending := (pending + [x]); + i_x_idx := i_x_idx + 1; + } + var i_t0 := flush(pending, result); + var i_lc0 := i_t0; + pending := i_lc0.pending; + result := i_lc0.result; + i_batch_idx := i_batch_idx + 1; + } + var i_t1 := flush(pending, result); + var i_lc1 := i_t1; + pending := i_lc1.pending; + result := i_lc1.result; + return result; +} diff --git a/examples/liftThunk.dfy.gen b/examples/liftThunk.dfy.gen new file mode 100644 index 0000000..18543f5 --- /dev/null +++ b/examples/liftThunk.dfy.gen @@ -0,0 +1,49 @@ +// Generated by lsc from liftThunk.ts + +datatype FlushState = FlushState(pending: seq, result: seq) + +method flush(pending: seq, result: seq) returns (res: FlushState) +{ + var pending := pending; + var result := result; + var i_x_idx := 0; + while i_x_idx < |pending| + invariant (i_x_idx <= |pending|) + { + var x := pending[i_x_idx]; + result := (result + [x]); + i_x_idx := i_x_idx + 1; + } + pending := []; + return FlushState(pending, result); +} + +method transform(items: seq>) returns (res: seq) +{ + var result: seq := []; + var pending: seq := []; + var i_batch_idx := 0; + while i_batch_idx < |items| + invariant (i_batch_idx <= |items|) + { + var batch := items[i_batch_idx]; + var i_x_idx := 0; + while i_x_idx < |batch| + invariant (i_x_idx <= |batch|) + { + var x := batch[i_x_idx]; + pending := (pending + [x]); + i_x_idx := i_x_idx + 1; + } + var i_t0 := flush(pending, result); + var i_lc0 := i_t0; + pending := i_lc0.pending; + result := i_lc0.result; + i_batch_idx := i_batch_idx + 1; + } + var i_t1 := flush(pending, result); + var i_lc1 := i_t1; + pending := i_lc1.pending; + result := i_lc1.result; + return result; +} diff --git a/examples/liftThunk.ts b/examples/liftThunk.ts new file mode 100644 index 0000000..3d4f02f --- /dev/null +++ b/examples/liftThunk.ts @@ -0,0 +1,30 @@ +/** + * Closure lift, Slice 1 — a void parameterless thunk that captures and mutates + * enclosing locals, called by name from several sites. + * + * `flush` captures `result` (mutated by push) and `pending` (read + reassigned), + * and is called inside the loop and once at the end. The closure-lift pass lifts it + * to a top-level routine taking the captures by value and returning the mutated ones + * as a record, threading that record back at each call site. Without the pass this + * function is skipped (`Unsupported: multi-statement lambda`). + */ + +export function transform(items: number[][]): number[] { + //@ verify + let result: number[] = []; + let pending: number[] = []; + const flush = () => { + for (const x of pending) { + result.push(x); + } + pending = []; + }; + for (const batch of items) { + for (const x of batch) { + pending = pending.concat([x]); + } + flush(); + } + flush(); + return result; +} diff --git a/examples/liftThunk.types.lean b/examples/liftThunk.types.lean new file mode 100644 index 0000000..be5d176 --- /dev/null +++ b/examples/liftThunk.types.lean @@ -0,0 +1,9 @@ +/- + Generated by lsc — Lean types and pure function mirrors. +-/ +import LemmaScript + +structure FlushState where + pending : Array Int + result : Array Int +deriving Repr, Inhabited, DecidableEq diff --git a/lakefile.lean b/lakefile.lean index b78bd4d..509d448 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -129,6 +129,8 @@ lean_lib Examples where `«nestedPush.types», `«nestedPush.def», `«nestedPush.proof», `«discriminantTrailing.types», `«discriminantTrailing.def», `«discriminantTrailing.proof», `«spreadMerge.types», `«spreadMerge.def», - `«recordIndexByEnum.types», `«recordIndexByEnum.def» + `«recordIndexByEnum.types», `«recordIndexByEnum.def», + `«closureLift.types», `«closureLift.def», `«closureLift.proof», + `«liftThunk.types», `«liftThunk.def» ] extraDepTargets := #[``downloadDependencies] diff --git a/tools/src/liftclosures.ts b/tools/src/liftclosures.ts new file mode 100644 index 0000000..de1cf81 --- /dev/null +++ b/tools/src/liftclosures.ts @@ -0,0 +1,249 @@ +/** + * liftClosures — lift a non-escaping, parameterless void thunk that captures and + * mutates enclosing locals into a top-level routine (Raw IR → Raw IR, between + * extract and resolve). + * + * A `const f = () => { …stmts… }` whose every use in the enclosing function is a + * statement-position call `f()` is lifted to a function `f(...captures)` returning a + * record of the captures it mutates; each call site threads the record back: + * + * const f = () => { result.push(x); pending = [] }; f(); + * → function f(result, pending): FState { …; return { result, pending } } + * const s = f(result, pending); result = s.result; pending = s.pending; + * + * Sound because the mutable environment has a single owner (the enclosing function): + * the captures' pre-values are passed in, the post-values come back in the record. + * Anything that breaks single-ownership — the closure escaping, taking parameters, + * recursing, or nesting another closure — is left untouched (it then hits the + * existing multi-statement-lambda skip), never miscompiled. + */ + +import { RawModule, RawFunction, RawStmt, RawExpr, RawLet } from "./rawir.js"; +import { TypeDeclInfo } from "./types.js"; + +/** Array methods that mutate their receiver in place (vs. returning a new value). */ +const MUTATORS = new Set(["push", "unshift", "pop", "shift", "splice", "sort", "reverse", "fill", "copyWithin", "add", "delete", "set", "clear"]); + +// ── Raw IR traversal ───────────────────────────────────────── + +function walkExpr(e: RawExpr, visit: (x: RawExpr) => void): void { + visit(e); + switch (e.kind) { + case "binop": walkExpr(e.left, visit); walkExpr(e.right, visit); return; + case "unop": case "nonNull": walkExpr(e.expr, visit); return; + case "call": walkExpr(e.fn, visit); e.args.forEach(a => walkExpr(a, visit)); return; + case "index": walkExpr(e.obj, visit); walkExpr(e.idx, visit); return; + case "field": walkExpr(e.obj, visit); return; + case "record": if (e.spread) walkExpr(e.spread, visit); e.fields.forEach(f => walkExpr(f.value, visit)); return; + case "recordMerge": walkExpr(e.base, visit); walkExpr(e.override, visit); return; + case "arrayLiteral": e.elems.forEach(x => walkExpr(x, visit)); return; + case "conditional": walkExpr(e.cond, visit); walkExpr(e.then, visit); walkExpr(e.else, visit); return; + case "optChain": walkExpr(e.obj, visit); e.chain.forEach(s => { if (s.kind === "call") s.args.forEach(a => walkExpr(a, visit)); else if (s.kind === "index") walkExpr(s.idx, visit); }); return; + case "nullish": walkExpr(e.left, visit); walkExpr(e.right, visit); return; + case "lambda": if (Array.isArray(e.body)) e.body.forEach(s => walkStmt(s, () => {}, visit)); else walkExpr(e.body, visit); return; + case "forall": case "exists": walkExpr(e.body, visit); return; + default: return; // leaf: var, num, str, bool, result, havoc, emptyCollection + } +} + +function walkStmt(s: RawStmt, visitStmt: (s: RawStmt) => void, visitExpr: (x: RawExpr) => void): void { + visitStmt(s); + switch (s.kind) { + case "let": walkExpr(s.init, visitExpr); return; + case "assign": walkExpr(s.value, visitExpr); return; + case "return": case "expr": walkExpr(s.kind === "return" ? s.value : s.expr, visitExpr); return; + case "if": walkExpr(s.cond, visitExpr); s.then.forEach(t => walkStmt(t, visitStmt, visitExpr)); s.else.forEach(t => walkStmt(t, visitStmt, visitExpr)); return; + case "while": walkExpr(s.cond, visitExpr); s.body.forEach(t => walkStmt(t, visitStmt, visitExpr)); return; + case "forof": walkExpr(s.iterable, visitExpr); s.body.forEach(t => walkStmt(t, visitStmt, visitExpr)); return; + case "switch": walkExpr(s.expr, visitExpr); s.cases.forEach(c => c.body.forEach(t => walkStmt(t, visitStmt, visitExpr))); s.defaultBody.forEach(t => walkStmt(t, visitStmt, visitExpr)); return; + default: return; // break/continue/throw/ghost*/assert — no captured-local refs of interest + } +} + +/** Root variable of an access path (`b.items` → `b`, `m.get(k)` receiver → `m`), or null. */ +function rootVar(e: RawExpr): string | null { + let cur: RawExpr = e; + while (true) { + if (cur.kind === "var") return cur.name; + if (cur.kind === "field") cur = cur.obj; + else if (cur.kind === "index") cur = cur.obj; + else if (cur.kind === "nonNull") cur = cur.expr; + else return null; + } +} + +// ── Names bound inside a block (so they aren't free) ───────── + +function boundNames(stmts: RawStmt[], into: Set): void { + for (const s of stmts) { + if (s.kind === "let" || s.kind === "ghostLet") into.add(s.name); + if (s.kind === "if") { boundNames(s.then, into); boundNames(s.else, into); } + if (s.kind === "while") boundNames(s.body, into); + if (s.kind === "forof") { s.names.forEach(n => into.add(n)); boundNames(s.body, into); } + if (s.kind === "switch") { s.cases.forEach(c => boundNames(c.body, into)); boundNames(s.defaultBody, into); } + } +} + +/** Free variable names referenced anywhere in a block. */ +function freeVars(stmts: RawStmt[]): Set { + const bound = new Set(); + boundNames(stmts, bound); + const refs = new Set(); + stmts.forEach(s => walkStmt(s, () => {}, e => { if (e.kind === "var" && !bound.has(e.name)) refs.add(e.name); })); + return refs; +} + +/** Capture roots mutated in a block: reassignment targets and in-place mutator receivers. */ +function mutatedRoots(stmts: RawStmt[]): Set { + const out = new Set(); + stmts.forEach(s => walkStmt(s, + st => { if (st.kind === "assign") out.add(st.target); }, + e => { + if (e.kind === "call" && e.fn.kind === "field" && MUTATORS.has(e.fn.field)) { + const r = rootVar(e.fn.obj); if (r) out.add(r); + } + })); + return out; +} + +// ── The lift ───────────────────────────────────────────────── + +function cap(s: string): string { return s.charAt(0).toUpperCase() + s.slice(1); } + +/** Rewrite every `return …` in a void-thunk body to `return `. */ +function rewriteReturns(stmts: RawStmt[], state: RawExpr): RawStmt[] { + return stmts.map(s => { + if (s.kind === "return") return { ...s, value: state }; + if (s.kind === "if") return { ...s, then: rewriteReturns(s.then, state), else: rewriteReturns(s.else, state) }; + if (s.kind === "while") return { ...s, body: rewriteReturns(s.body, state) }; + if (s.kind === "forof") return { ...s, body: rewriteReturns(s.body, state) }; + if (s.kind === "switch") return { ...s, cases: s.cases.map(c => ({ ...c, body: rewriteReturns(c.body, state) })), defaultBody: rewriteReturns(s.defaultBody, state) }; + return s; + }); +} + +function endsInReturn(stmts: RawStmt[]): boolean { + const last = stmts[stmts.length - 1]; + return !!last && last.kind === "return"; +} + +interface LiftResult { fn: RawFunction; typeDecl: TypeDeclInfo; liftedName: string; recordName: string; captureOrder: string[]; mutated: string[]; } + +/** Try to lift the closure bound by `decl` within enclosing `host`. Null ⇒ not liftable. */ +function tryLift(decl: RawLet, host: RawFunction, taken: Set): LiftResult | null { + const lam = decl.init; + if (lam.kind !== "lambda" || !Array.isArray(lam.body)) return null; + if (lam.params.length !== 0) return null; // Slice 2: parameters + const body = lam.body; + + // Nested closure inside the body → breaks the single-owner analysis. Refuse. + let hasNestedLambda = false; + body.forEach(s => walkStmt(s, () => {}, e => { if (e.kind === "lambda") hasNestedLambda = true; })); + if (hasNestedLambda) return null; + + const fv = freeVars(body); + if (fv.has(decl.name)) return null; // recursive self-reference + + // Captures = free vars that name an enclosing param or local. + const typeOf = new Map(); + for (const p of host.params) typeOf.set(p.name, p.tsType); + host.body.forEach(s => { if (s.kind === "let" && s.name !== decl.name && s.tsType) typeOf.set(s.name, s.tsType); }); + + const captureOrder: string[] = []; + for (const name of fv) if (typeOf.has(name)) captureOrder.push(name); + if (captureOrder.length === 0) return null; + // A capture whose declared type we can't name as a string can't become a param. Refuse. + if (captureOrder.some(c => !typeOf.get(c))) return null; + + const muts = mutatedRoots(body); + const mutated = captureOrder.filter(c => muts.has(c)); + if (mutated.length === 0) return null; // nothing to thread → not this feature + + const liftedName = taken.has(decl.name) ? `${host.name}_${decl.name}` : decl.name; + const recordName = (() => { let n = `${cap(decl.name)}State`; while (taken.has(n)) n = `${host.name}_${n}`; return n; })(); + taken.add(liftedName); taken.add(recordName); + + const stateRecord: RawExpr = { kind: "record", spread: null, fields: mutated.map(c => ({ name: c, value: { kind: "var", name: c } })) }; + let liftedBody = rewriteReturns(body, stateRecord); + if (!endsInReturn(liftedBody)) liftedBody = [...liftedBody, { kind: "return", value: stateRecord, line: decl.line }]; + + const params = captureOrder.map(c => ({ name: c, tsType: typeOf.get(c)! })); + const fn: RawFunction = { + name: liftedName, exported: false, typeParams: [], + params, tsParams: params.map(p => ({ kind: "simple" as const, binds: [p.name] })), + returnType: recordName, requires: [], ensures: [], contract: [], decreases: null, + pure: false, autohavoc: host.autohavoc, typeAnnotations: [], body: liftedBody, line: decl.line, + }; + const typeDecl: TypeDeclInfo = { name: recordName, kind: "record", fields: mutated.map(c => ({ name: c, tsType: typeOf.get(c)! })) }; + return { fn, typeDecl, liftedName, recordName, captureOrder, mutated }; +} + +/** Is `s` a statement-position call `f()`? */ +function isThunkCall(s: RawStmt, name: string): boolean { + return s.kind === "expr" && s.expr.kind === "call" && s.expr.fn.kind === "var" && s.expr.fn.name === name && s.expr.args.length === 0; +} + +/** Replace each `f()` in a statement list (recursively) with the threaded call. */ +function rewriteCalls(stmts: RawStmt[], name: string, L: LiftResult, fresh: () => string): RawStmt[] { + const out: RawStmt[] = []; + for (const s of stmts) { + if (isThunkCall(s, name)) { + const sv = fresh(); + out.push({ kind: "let", name: sv, mutable: false, tsType: L.recordName, init: { kind: "call", fn: { kind: "var", name: L.liftedName }, args: L.captureOrder.map(c => ({ kind: "var" as const, name: c })) }, line: s.line }); + for (const c of L.mutated) out.push({ kind: "assign", target: c, value: { kind: "field", obj: { kind: "var", name: sv }, field: c }, line: s.line }); + continue; + } + if (s.kind === "if") out.push({ ...s, then: rewriteCalls(s.then, name, L, fresh), else: rewriteCalls(s.else, name, L, fresh) }); + else if (s.kind === "while") out.push({ ...s, body: rewriteCalls(s.body, name, L, fresh) }); + else if (s.kind === "forof") out.push({ ...s, body: rewriteCalls(s.body, name, L, fresh) }); + else if (s.kind === "switch") out.push({ ...s, cases: s.cases.map(c => ({ ...c, body: rewriteCalls(c.body, name, L, fresh) })), defaultBody: rewriteCalls(s.defaultBody, name, L, fresh) }); + else out.push(s); + } + return out; +} + +/** All uses of `name` in `host` outside its own declaration; true iff every one is a statement-call. */ +function onlyCalledInStatements(host: RawFunction, name: string): boolean { + let total = 0, calls = 0; + // count statement-calls + const countCalls = (stmts: RawStmt[]) => stmts.forEach(s => { + if (isThunkCall(s, name)) calls++; + if (s.kind === "if") { countCalls(s.then); countCalls(s.else); } + if (s.kind === "while" || s.kind === "forof") countCalls(s.body); + if (s.kind === "switch") { s.cases.forEach(c => countCalls(c.body)); countCalls(s.defaultBody); } + }); + countCalls(host.body); + // count every reference (excluding the closure's own `let` initializer) + for (const s of host.body) { + if (s.kind === "let" && s.init.kind === "lambda") continue; // the decl itself + walkStmt(s, () => {}, e => { if (e.kind === "var" && e.name === name) total++; }); + } + return total > 0 && total === calls; +} + +function liftInFunction(host: RawFunction, taken: Set, addFn: (f: RawFunction) => void, addType: (t: TypeDeclInfo) => void): RawFunction { + let body = host.body; + let counter = 0; + const fresh = () => `_lc${counter++}`; + // Top-level closure declarations in this function, in order. + for (const decl of host.body) { + if (decl.kind !== "let" || decl.init.kind !== "lambda") continue; + if (!onlyCalledInStatements(host, decl.name)) continue; // escapes → leave it + const L = tryLift(decl, host, taken); + if (!L) continue; + addFn(L.fn); addType(L.typeDecl); + // Drop the closure `let`, rewrite its calls, and make mutated captures mutable. + body = rewriteCalls(body.filter(s => s !== decl), decl.name, L, fresh) + .map(s => (s.kind === "let" && L.mutated.includes(s.name)) ? { ...s, mutable: true } : s); + } + return { ...host, body }; +} + +export function liftClosures(mod: RawModule): RawModule { + const taken = new Set([...mod.functions.map(f => f.name), ...mod.typeDecls.map(t => t.name), ...mod.constants.map(c => c.name)]); + const extraFns: RawFunction[] = []; + const extraTypes: TypeDeclInfo[] = []; + const functions = mod.functions.map(f => liftInFunction(f, taken, x => extraFns.push(x), t => extraTypes.push(t))); + if (extraFns.length === 0) return mod; + return { ...mod, typeDecls: [...mod.typeDecls, ...extraTypes], functions: [...extraFns, ...functions] }; +} diff --git a/tools/src/lsc.ts b/tools/src/lsc.ts index 9cbb804..7d158a4 100755 --- a/tools/src/lsc.ts +++ b/tools/src/lsc.ts @@ -9,6 +9,7 @@ import { Project, ScriptTarget } from "ts-morph"; import { existsSync } from "fs"; import path from "path"; import { extractModule } from "./extract.js"; +import { liftClosures } from "./liftclosures.js"; import { resolveModule } from "./resolve.js"; import { narrowModule } from "./narrow.js"; import { autoHavocModule } from "./autohavoc.js"; @@ -92,7 +93,9 @@ function main() { const safeSlice = /\/\/@ safe-slice\b/.test(fullText); // Extract: ts-morph → Raw IR - const raw = extractModule(sourceFile); + const raw0 = extractModule(sourceFile); + // Lift non-escaping mutating thunks to top-level routines (Raw IR → Raw IR). + const raw = liftClosures(raw0); if (cmd === "extract") { console.log(JSON.stringify(raw, null, 2)); From 9aec83c459b90844f3c0992a0847ed9ddcd05ddf Mon Sep 17 00:00:00 2001 From: Nada Amin Date: Thu, 25 Jun 2026 21:18:32 -0400 Subject: [PATCH 2/2] remove doc ref --- examples/closureLift.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/closureLift.ts b/examples/closureLift.ts index b281a95..749952f 100644 --- a/examples/closureLift.ts +++ b/examples/closureLift.ts @@ -1,5 +1,5 @@ /** - * Lean gate for the targeted closure lift (DESIGN_CLOSURE_TARGET.md §6). + * Lean gate for the targeted closure lift. * * This is the *post-lift* shape, written by hand (the lift pass doesn't exist yet): * a record-returning routine with a loop — which emits as a Velvet `method` returning