lift closures

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

examples/closureLift.dfy

@@ -0,0 +1,45 @@
+// Generated by lsc from closureLift.ts
+
+datatype FlushState = FlushState(result: seq<int>, pending: seq<int>)
+
+method flush(result: seq<int>, pending: seq<int>) 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<seq<int>>) returns (res: seq<int>)
+{
+  var result: seq<int> := [];
+  var pending: seq<int> := [];
+  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;
+}

examples/closureLift.dfy.gen

@@ -0,0 +1,45 @@
+// Generated by lsc from closureLift.ts
+
+datatype FlushState = FlushState(result: seq<int>, pending: seq<int>)
+
+method flush(result: seq<int>, pending: seq<int>) 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<seq<int>>) returns (res: seq<int>)
+{
+  var result: seq<int> := [];
+  var pending: seq<int> := [];
+  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;
+}

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

examples/closureLift.ts

@@ -0,0 +1,40 @@
+/**
+ * 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
+ * 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;
+}

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

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

examples/liftThunk.dfy

@@ -0,0 +1,49 @@
+// Generated by lsc from liftThunk.ts
+
+datatype FlushState = FlushState(pending: seq<int>, result: seq<int>)
+
+method flush(pending: seq<int>, result: seq<int>) 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<seq<int>>) returns (res: seq<int>)
+{
+  var result: seq<int> := [];
+  var pending: seq<int> := [];
+  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;
+}

examples/liftThunk.dfy.gen

@@ -0,0 +1,49 @@
+// Generated by lsc from liftThunk.ts
+
+datatype FlushState = FlushState(pending: seq<int>, result: seq<int>)
+
+method flush(pending: seq<int>, result: seq<int>) 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<seq<int>>) returns (res: seq<int>)
+{
+  var result: seq<int> := [];
+  var pending: seq<int> := [];
+  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;
+}

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

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

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]