From 1cf776bca372dedd84bb03a17553333544239e0a Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Thu, 26 Mar 2026 11:48:28 +0100
Subject: [PATCH 01/10] Fix bug in handling of blocks that occur in
 expresssions

---
 .../Laurel/LiftImperativeExpressions.lean     | 20 +++++--------------
 .../Fundamentals/T2_ImpureExpressions.lean    |  6 ++++++
 2 files changed, 11 insertions(+), 15 deletions(-)

diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean
index e29618fef..2b83cba53 100644
--- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean
+++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean
@@ -289,21 +289,11 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do
           | none => pure none
         return ⟨.IfThenElse seqCond seqThen seqElse, md⟩
 
-  | .Block stmts metadata =>
-      -- Block in expression position: lift all but last to prepends
-      match h_last : stmts.getLast? with
-      | none => return bare (.Block [] metadata)
-      | some last => do
-          have := List.mem_of_getLast? h_last
-
-          -- Process all-but-last as statements and prepend them in order
-          let mut blockStmts : List StmtExprMd := []
-          for nonLastStatement in stmts.dropLast.attach do
-            have := List.dropLast_subset stmts nonLastStatement.property
-            blockStmts := blockStmts ++ (← transformStmt nonLastStatement)
-          for s in blockStmts.reverse do addPrepend s
-          -- Last element is the expression value
-          transformExpr last
+  | .Block stmts labelOption =>
+      let newStmts := (← stmts.reverse.mapM transformExpr).reverse
+      match newStmts.getLast? with
+      | none => return bare (.Block [] labelOption)
+      | some last => return last
 
   | .LocalVariable name ty initializer =>
       -- If the substitution map has an entry for this variable, it was
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
index ce53e09f0..16342cfda 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
@@ -97,6 +97,12 @@ procedure imperativeCallInConditionalExpression(b: bool) {
     assert result == 0
   }
 };
+
+procedure nesting() {
+  var x: int := 2;
+  var y: int := { x := 1; x } + { x := x + 10; x };
+  assert y == 1 + 11
+};
 "
 
 #guard_msgs (error, drop all) in

From fc66f1265d401482004c48fb046832d4e15cbd1c Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Thu, 26 Mar 2026 11:54:17 +0100
Subject: [PATCH 02/10] Change test-case name

---
 .../Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean      | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
index 16342cfda..ba9749b1b 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
@@ -98,7 +98,7 @@ procedure imperativeCallInConditionalExpression(b: bool) {
   }
 };
 
-procedure nesting() {
+procedure repeatedBlockExpressions() {
   var x: int := 2;
   var y: int := { x := 1; x } + { x := x + 10; x };
   assert y == 1 + 11

From 922174bb48d908dc914a2a9bba4480ef883be216 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Thu, 26 Mar 2026 14:52:27 +0100
Subject: [PATCH 03/10] Fixes

---
 .../Laurel/LiftImperativeExpressions.lean     | 30 +++++++++++++++++--
 .../Fundamentals/T2_ImpureExpressions.lean    | 13 +++++++-
 2 files changed, 39 insertions(+), 4 deletions(-)

diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean
index 2b83cba53..1c3b351fb 100644
--- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean
+++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean
@@ -107,6 +107,29 @@ private def freshCondVar : LiftM Identifier := do
 private def addPrepend (stmt : StmtExprMd) : LiftM Unit :=
   modify fun s => { s with prependedStmts := stmt :: s.prependedStmts }
 
+/--
+From a list of statements (in expression position), prepend all `LocalVariable` declarations
+to the surrounding context and drop all other non-last statements. Returns a list containing
+only the last statement (the block's expression value), or empty if the input is empty.
+-/
+private def onlyKeepLocalDeclarationsAndLast (stmts : List StmtExprMd) : LiftM (List StmtExprMd) := do
+  match stmts with
+  | [] => return []
+  | _ =>
+    let last := stmts.getLast!
+    for s in stmts.dropLast do
+      match s.val with
+      | .LocalVariable .. =>
+          -- This addPrepend is a hack to work around Core not having let expressions
+          -- Otherwise we could keep them in the block
+          addPrepend s
+      | .Assert _ =>
+          -- Hack to work around Core not supporting assert expressions
+          -- Otherwise we could keep them in the block
+          addPrepend s
+      | _ => pure ()
+    return [last]
+
 private def takePrepends : LiftM (List StmtExprMd) := do
   let stmts := (← get).prependedStmts
   modify fun s => { s with prependedStmts := [] }
@@ -237,10 +260,12 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do
       -- Imperative call in expression position: lift it like an assignment
       -- Order matters: assign must be prepended first (it's newest-first),
       -- so that when reversed the var declaration comes before the call.
+      let allArgPrepends ← takePrepends
       let callResultVar ← freshCondVar
       let callResultType ← computeType expr
       addPrepend (⟨.Assign [bare (.Identifier callResultVar)] seqCall, md⟩)
       addPrepend (bare (.LocalVariable callResultVar callResultType none))
+      allArgPrepends.reverse.forM addPrepend
       return bare (.Identifier callResultVar)
 
   | .IfThenElse cond thenBranch elseBranch =>
@@ -291,9 +316,8 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do
 
   | .Block stmts labelOption =>
       let newStmts := (← stmts.reverse.mapM transformExpr).reverse
-      match newStmts.getLast? with
-      | none => return bare (.Block [] labelOption)
-      | some last => return last
+
+      return ⟨ .Block (← onlyKeepLocalDeclarationsAndLast newStmts) labelOption, md ⟩
 
   | .LocalVariable name ty initializer =>
       -- If the substitution map has an entry for this variable, it was
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
index ba9749b1b..68ec88a8b 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
@@ -98,10 +98,21 @@ procedure imperativeCallInConditionalExpression(b: bool) {
   }
 };
 
+function add(x: int, y: int): int {
+  x + y
+};
 procedure repeatedBlockExpressions() {
   var x: int := 2;
   var y: int := { x := 1; x } + { x := x + 10; x };
-  assert y == 1 + 11
+  var z: int := add({ x := 1; x }, { x := x + 10; x });
+  assert y == 1 + 11;
+  assert z == 1 + 11
+};
+
+procedure addProc(a: int, b: int): int { return a + b };
+procedure addProcCaller(): int {
+  var x: int := 0;
+  return addProc({x := 1; x}, {x := x + 10; x})
 };
 "
 

From 80d8e4a9acc64753ea113fb923efa054e0531c99 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Thu, 26 Mar 2026 14:53:51 +0100
Subject: [PATCH 04/10] Rename

---
 Strata/Languages/Laurel/LiftImperativeExpressions.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean
index 1c3b351fb..8159735da 100644
--- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean
+++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean
@@ -112,7 +112,7 @@ From a list of statements (in expression position), prepend all `LocalVariable`
 to the surrounding context and drop all other non-last statements. Returns a list containing
 only the last statement (the block's expression value), or empty if the input is empty.
 -/
-private def onlyKeepLocalDeclarationsAndLast (stmts : List StmtExprMd) : LiftM (List StmtExprMd) := do
+private def onlyKeepUsefulExpressionsAndLast (stmts : List StmtExprMd) : LiftM (List StmtExprMd) := do
   match stmts with
   | [] => return []
   | _ =>
@@ -316,8 +316,7 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do
 
   | .Block stmts labelOption =>
       let newStmts := (← stmts.reverse.mapM transformExpr).reverse
-
-      return ⟨ .Block (← onlyKeepLocalDeclarationsAndLast newStmts) labelOption, md ⟩
+      return ⟨ .Block (← onlyKeepUsefulExpressionsAndLast newStmts) labelOption, md ⟩
 
   | .LocalVariable name ty initializer =>
       -- If the substitution map has an entry for this variable, it was

From f1d196d029869f8d731ca9dca8afbeaecc0e7278 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Thu, 26 Mar 2026 15:03:28 +0100
Subject: [PATCH 05/10] Fix broken test

---
 .../Laurel/LiftExpressionAssignmentsTest.lean  | 18 ++----------------
 1 file changed, 2 insertions(+), 16 deletions(-)

diff --git a/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean b/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean
index 28bc064cc..f326010bf 100644
--- a/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean
+++ b/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean
@@ -22,16 +22,6 @@ open Strata.Elab (parseStrataProgramFromDialect)
 namespace Strata.Laurel
 
 def blockStmtLiftingProgram : String := r"
-composite Box {
-  var value: int
-}
-
-procedure heapUpdateInBlockExpr(b: Box)
-{
-  var x: int := { b#value := b#value + 1; b#value };
-  assert x == b#value
-};
-
 procedure assertInBlockExpr()
 {
   var x: int := 0;
@@ -53,14 +43,10 @@ def parseLaurelAndLift (input : String) : IO Program := do
     pure (liftExpressionAssignments model program)
 
 /--
-info: procedure heapUpdateInBlockExpr(b: Box) returns ⏎
-()
-deterministic
-{ b#value := b#value + 1; var x: int := b#value; assert x == b#value }
-procedure assertInBlockExpr() returns ⏎
+info: procedure assertInBlockExpr() returns ⏎
 ()
 deterministic
-{ var x: int := 0; assert x == 0; x := 1; var y: int := x; assert y == 1 }
+{ var x: int := 0; assert x == 0; var $x_0: int := x; x := 1; var y: int := { x }; assert y == 1 }
 -/
 #guard_msgs in
 #eval! do

From 9a0fc1c03fa0fe13ec23ac92b7813fb25f2def19 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Thu, 26 Mar 2026 15:21:54 +0100
Subject: [PATCH 06/10] Rename and clarify

---
 .../Laurel/LiftImperativeExpressions.lean     | 33 ++++++++++++-------
 1 file changed, 21 insertions(+), 12 deletions(-)

diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean
index 8159735da..0a59242d3 100644
--- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean
+++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean
@@ -107,28 +107,37 @@ private def freshCondVar : LiftM Identifier := do
 private def addPrepend (stmt : StmtExprMd) : LiftM Unit :=
   modify fun s => { s with prependedStmts := stmt :: s.prependedStmts }
 
-/--
-From a list of statements (in expression position), prepend all `LocalVariable` declarations
-to the surrounding context and drop all other non-last statements. Returns a list containing
-only the last statement (the block's expression value), or empty if the input is empty.
--/
-private def onlyKeepUsefulExpressionsAndLast (stmts : List StmtExprMd) : LiftM (List StmtExprMd) := do
+private def onlyKeepSideEffectStmtsAndLast (stmts : List StmtExprMd) : LiftM (List StmtExprMd) := do
   match stmts with
   | [] => return []
   | _ =>
     let last := stmts.getLast!
-    for s in stmts.dropLast do
+    let nonLast ← stmts.dropLast.flatMapM (fun s =>
       match s.val with
-      | .LocalVariable .. =>
+      | .LocalVariable .. => do
           -- This addPrepend is a hack to work around Core not having let expressions
           -- Otherwise we could keep them in the block
           addPrepend s
-      | .Assert _ =>
+          pure []
+      | .Assert _ => do
           -- Hack to work around Core not supporting assert expressions
           -- Otherwise we could keep them in the block
           addPrepend s
-      | _ => pure ()
-    return [last]
+          pure []
+      | .Assume _ => do
+          -- Hack to work around Core not supporting assume expressions
+          -- Otherwise we could keep them in the block
+          addPrepend s
+          pure []
+
+      /-
+      Any other impure StmtExpr, like .Assign, .Exit or .Return,
+      should already have been processed by translateExpr.
+      TODO: currently .Exit or .Return is not processed, this is a bug
+      -/
+      | _ => pure []
+    )
+    return nonLast ++ [last]
 
 private def takePrepends : LiftM (List StmtExprMd) := do
   let stmts := (← get).prependedStmts
@@ -316,7 +325,7 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do
 
   | .Block stmts labelOption =>
       let newStmts := (← stmts.reverse.mapM transformExpr).reverse
-      return ⟨ .Block (← onlyKeepUsefulExpressionsAndLast newStmts) labelOption, md ⟩
+      return ⟨ .Block (← onlyKeepSideEffectStmtsAndLast newStmts) labelOption, md ⟩
 
   | .LocalVariable name ty initializer =>
       -- If the substitution map has an entry for this variable, it was

From 55054f7b60eb3d2eab38217cdba8d733207a2e04 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Thu, 26 Mar 2026 15:23:12 +0100
Subject: [PATCH 07/10] Improve comment

---
 Strata/Languages/Laurel/LiftImperativeExpressions.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean
index 0a59242d3..0335f835a 100644
--- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean
+++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean
@@ -132,8 +132,9 @@ private def onlyKeepSideEffectStmtsAndLast (stmts : List StmtExprMd) : LiftM (Li
 
       /-
       Any other impure StmtExpr, like .Assign, .Exit or .Return,
-      should already have been processed by translateExpr.
-      TODO: currently .Exit or .Return is not processed, this is a bug
+      should already have been processed by translateExpr,
+      so we can assume this StmtExpr is pure and can be dropped.
+      TODO: currently .Exit and .Return are not processed by translateExpr, this is a bug
       -/
       | _ => pure []
     )

From 49e6ca0fd882a1ed40ec74ce6b1c9708b57e4869 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Thu, 26 Mar 2026 16:04:34 +0100
Subject: [PATCH 08/10] Add comment that reports a bug

---
 .../Laurel/LiftImperativeExpressions.lean     | 32 +++++++++----------
 .../Fundamentals/T2_ImpureExpressions.lean    | 19 +++++++++--
 2 files changed, 32 insertions(+), 19 deletions(-)

diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean
index 0335f835a..37463be4f 100644
--- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean
+++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean
@@ -104,7 +104,7 @@ private def freshCondVar : LiftM Identifier := do
   modify fun s => { s with condCounter := n + 1 }
   return s!"$c_{n}"
 
-private def addPrepend (stmt : StmtExprMd) : LiftM Unit :=
+private def prepend (stmt : StmtExprMd) : LiftM Unit :=
   modify fun s => { s with prependedStmts := stmt :: s.prependedStmts }
 
 private def onlyKeepSideEffectStmtsAndLast (stmts : List StmtExprMd) : LiftM (List StmtExprMd) := do
@@ -117,17 +117,17 @@ private def onlyKeepSideEffectStmtsAndLast (stmts : List StmtExprMd) : LiftM (Li
       | .LocalVariable .. => do
           -- This addPrepend is a hack to work around Core not having let expressions
           -- Otherwise we could keep them in the block
-          addPrepend s
+          prepend s
           pure []
       | .Assert _ => do
           -- Hack to work around Core not supporting assert expressions
           -- Otherwise we could keep them in the block
-          addPrepend s
+          prepend s
           pure []
       | .Assume _ => do
           -- Hack to work around Core not supporting assume expressions
           -- Otherwise we could keep them in the block
-          addPrepend s
+          prepend s
           pure []
 
       /-
@@ -204,7 +204,7 @@ and updates substitutions. The value should already be transformed by the caller
 private def liftAssignExpr (targets : List StmtExprMd) (seqValue : StmtExprMd)
     (md : Imperative.MetaData Core.Expression) : LiftM Unit := do
   -- Prepend the assignment itself
-  addPrepend (⟨.Assign targets seqValue, md⟩)
+  prepend (⟨.Assign targets seqValue, md⟩)
   -- Create a before-snapshot for each target and update substitutions
   for target in targets do
     match target.val with
@@ -212,7 +212,7 @@ private def liftAssignExpr (targets : List StmtExprMd) (seqValue : StmtExprMd)
         let snapshotName ← freshTempFor varName
         let varType ← computeType target
         -- Snapshot goes before the assignment (cons pushes to front)
-        addPrepend (⟨.LocalVariable snapshotName varType (some (⟨.Identifier varName, md⟩)), md⟩)
+        prepend (⟨.LocalVariable snapshotName varType (some (⟨.Identifier varName, md⟩)), md⟩)
         setSubst varName snapshotName
     | _ => pure ()
 
@@ -233,7 +233,7 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do
   | .Hole false (some holeType) =>
       -- Nondeterministic typed hole: lift to a fresh variable with no initializer (havoc)
       let holeVar ← freshCondVar
-      addPrepend (bare (.LocalVariable holeVar holeType none))
+      prepend (bare (.LocalVariable holeVar holeType none))
       return bare (.Identifier holeVar)
 
   | .Assign targets value =>
@@ -262,20 +262,20 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do
 
   | .StaticCall callee args =>
     let model := (← get).model
+    let afterPrepends ← takePrepends
     let seqArgs ← args.reverse.mapM transformExpr
     let seqCall := ⟨.StaticCall callee seqArgs.reverse, md⟩
     if model.isFunction callee then
       return seqCall
     else
       -- Imperative call in expression position: lift it like an assignment
-      -- Order matters: assign must be prepended first (it's newest-first),
-      -- so that when reversed the var declaration comes before the call.
       let allArgPrepends ← takePrepends
       let callResultVar ← freshCondVar
       let callResultType ← computeType expr
-      addPrepend (⟨.Assign [bare (.Identifier callResultVar)] seqCall, md⟩)
-      addPrepend (bare (.LocalVariable callResultVar callResultType none))
-      allArgPrepends.reverse.forM addPrepend
+      let liftedCall := [
+        bare (.LocalVariable callResultVar callResultType none),
+        ⟨.Assign [bare (.Identifier callResultVar)] seqCall, md⟩]
+      modify fun s => { s with prependedStmts := allArgPrepends ++ liftedCall ++ afterPrepends}
       return bare (.Identifier callResultVar)
 
   | .IfThenElse cond thenBranch elseBranch =>
@@ -312,8 +312,8 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do
         let condType ← computeType thenBranch
         -- IfThenElse added first (cons puts it deeper), then declaration (cons puts it on top)
         -- Output order: declaration, then if-then-else
-        addPrepend (⟨.IfThenElse seqCond thenBlock seqElse, md⟩)
-        addPrepend (bare (.LocalVariable condVar condType none))
+        prepend (⟨.IfThenElse seqCond thenBlock seqElse, md⟩)
+        prepend (bare (.LocalVariable condVar condType none))
         return bare (.Identifier condVar)
       else
         -- No assignments in branches — recurse normally
@@ -337,9 +337,9 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do
         match initializer with
         | some initExpr =>
             let seqInit ← transformExpr initExpr
-            addPrepend (⟨.LocalVariable name ty (some seqInit), expr.md⟩)
+            prepend (⟨.LocalVariable name ty (some seqInit), expr.md⟩)
         | none =>
-            addPrepend (⟨.LocalVariable name ty none, expr.md⟩)
+            prepend (⟨.LocalVariable name ty none, expr.md⟩)
         return ⟨.Identifier (← getSubst name), expr.md⟩
       else
         return expr
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
index 68ec88a8b..0ec9bf87f 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
@@ -98,9 +98,11 @@ procedure imperativeCallInConditionalExpression(b: bool) {
   }
 };
 
-function add(x: int, y: int): int {
+function add(x: int, y: int): int
+{
   x + y
 };
+
 procedure repeatedBlockExpressions() {
   var x: int := 2;
   var y: int := { x := 1; x } + { x := x + 10; x };
@@ -109,10 +111,21 @@ procedure repeatedBlockExpressions() {
   assert z == 1 + 11
 };
 
-procedure addProc(a: int, b: int): int { return a + b };
+procedure addProc(a: int, b: int) returns (r: int)
+  ensures r == a + b {
+  return a + b
+};
+
 procedure addProcCaller(): int {
   var x: int := 0;
-  return addProc({x := 1; x}, {x := x + 10; x})
+  var y: int := addProc({x := 1; x}, {x := x + 10; x});
+  assert y == 11
+
+  // The next statement is not translated correctly.
+  // I think it's a bug in the handling of StaticCall
+  // Where a reference is substituted when it should not be
+  // var z: int := addProc({x := 1; x}, {x := x + 10; x}) + (x := 3);
+  // assert z == 14
 };
 "
 

From edb0471530ee2663fbc6b128bd396a7a3a395905 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Thu, 26 Mar 2026 16:37:37 +0100
Subject: [PATCH 09/10] undo change

---
 Strata/Languages/Laurel/LiftImperativeExpressions.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean
index 37463be4f..e21f64bdf 100644
--- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean
+++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean
@@ -262,7 +262,6 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do
 
   | .StaticCall callee args =>
     let model := (← get).model
-    let afterPrepends ← takePrepends
     let seqArgs ← args.reverse.mapM transformExpr
     let seqCall := ⟨.StaticCall callee seqArgs.reverse, md⟩
     if model.isFunction callee then
@@ -273,9 +272,10 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do
       let callResultVar ← freshCondVar
       let callResultType ← computeType expr
       let liftedCall := [
-        bare (.LocalVariable callResultVar callResultType none),
-        ⟨.Assign [bare (.Identifier callResultVar)] seqCall, md⟩]
-      modify fun s => { s with prependedStmts := allArgPrepends ++ liftedCall ++ afterPrepends}
+        ⟨ (.LocalVariable callResultVar callResultType none), md ⟩,
+        ⟨.Assign [bare (.Identifier callResultVar)] seqCall, md⟩
+      ]
+      modify fun s => { s with prependedStmts := s.prependedStmts ++ liftedCall}
       return bare (.Identifier callResultVar)
 
   | .IfThenElse cond thenBranch elseBranch =>

From a4dedf23fd3b5459c708d32738b12a53d6190395 Mon Sep 17 00:00:00 2001
From: Remy Willems <rwillems@amazon.com>
Date: Thu, 26 Mar 2026 16:40:42 +0100
Subject: [PATCH 10/10] Remove nonesense

---
 Strata/Languages/Laurel/LiftImperativeExpressions.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean
index e21f64bdf..f1e560340 100644
--- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean
+++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean
@@ -268,7 +268,6 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do
       return seqCall
     else
       -- Imperative call in expression position: lift it like an assignment
-      let allArgPrepends ← takePrepends
       let callResultVar ← freshCondVar
       let callResultType ← computeType expr
       let liftedCall := [