Contract pass: assert postconditions in body for opaque procs

Strata/Languages/Laurel/ContractPass.lean

@@ -116,18 +116,18 @@ private def transformProcBody (proc : Procedure) (info : ContractInfo) : Body :=
   let preAssumes : List StmtExprMd :=
     proc.preconditions.zip info.preNames |>.map fun (pc, name, _) =>
       ⟨.Assume (mkCall name inputArgs), pc.condition.source⟩
+  let postAsserts : List StmtExprMd :=
+    postconds.map fun pc =>
+      let summary := pc.summary.getD "postcondition"
+      ⟨.Assert { condition := pc.condition, summary := some summary }, pc.condition.source⟩
   match proc.body with
   | .Transparent body =>
-    let postAsserts : List StmtExprMd :=
-      postconds.zip info.postNames |>.map fun (pc, _name, _summary) =>
-        let summary := pc.summary.getD "postcondition"
-        ⟨.Assert { condition := pc.condition, summary := some summary }, pc.condition.source⟩
     .Transparent ⟨.Block (preAssumes ++ [body] ++ postAsserts) none, body.source⟩
   | .Opaque _ (some impl) _ =>
     .Opaque postconds (some ⟨.Block (preAssumes ++ [impl]) none, impl.source⟩) []
   | .Opaque _ none mods =>
     .Opaque postconds none mods
-  | .Abstract _ =>
+  | .Abstract postconds =>
     .Abstract postconds
   | b => b
 

Strata/Languages/Laurel/LaurelCompilationPipeline.lean

@@ -137,9 +137,6 @@ private def laurelPipeline : Array LaurelPass := #[
   { name := "DesugarShortCircuit"
     run := fun p _ =>
       (desugarShortCircuit p, [], {}) },
-  -- { name := "LiftExpressionAssignments"
-  --   run := fun p m =>
-  --     (liftExpressionAssignments p m [], [], {}) },
   { name := "ConstrainedTypeElim"
     needsResolves := true
     run := fun p m =>
@@ -246,11 +243,6 @@ structure CorePass where
 
 /-- The ordered sequence of passes on the unordered Core representation. -/
 private def corePipeline : Array CorePass := #[
-  -- { name := "EliminateMultipleOutputs"
-  --   run := fun uc _m => eliminateMultipleOutputs uc },
-  -- { name := "InlineLocalVariablesInExpressions"
-  --   needsResolves := true
-  --   run := fun uc _m => inlineLocalVariablesInExpressions uc },
   { name := "LiftImperativeExpressionsInCore"
     needsResolves := true
     run := fun uc m => liftImperativeExpressionsInCore uc m }

Strata/Languages/Laurel/LiftImperativeExpressions.lean

@@ -104,17 +104,11 @@ private def onlyKeepSideEffectStmtsAndLast (stmts : List StmtExprMd) : LiftM (Li
   match stmts with
   | [] => return []
   | _ =>
-    -- return stmts
     let last := stmts.getLast!
     let nonLast ← stmts.dropLast.flatMapM (fun s =>
       match s.val with
       | .Var (.Declare ..) | .Assign ([⟨.Declare .., _⟩]) _ => do
           pure [s]
-      -- | .Assert _ => do
-      --     pure [s]
-      -- | .Assume _ => do
-      --     pure [s]
-
       /-
       Any other impure StmtExpr, like .Assign, .Exit or .Return,
       should already have been processed by translateExpr,
@@ -521,24 +515,16 @@ def transformStmt (stmt : StmtExprMd) : LiftM (List StmtExprMd) := do
   | AstNode.mk val source =>
   match val with
   | .Assert cond =>
-      -- Do not transform assert conditions with assignments — they must be rejected.
-      -- But nondeterministic holes need to be lifted.
-      -- if containsNondetHole cond.condition && !containsAssignmentOrImperativeCall (← get).model cond.condition then
         let seqCond ← transformExpr cond.condition
         let prepends ← takePrepends
         modify fun s => { s with subst := [] }
         return prepends ++ [⟨.Assert { cond with condition := seqCond }, source⟩]
-      -- else
-      --   return [stmt]
 
   | .Assume cond =>
-      -- if containsNondetHole cond && !containsAssignmentOrImperativeCall (← get).model cond then
         let seqCond ← transformExpr cond
         let prepends ← takePrepends
         modify fun s => { s with subst := [] }
         return prepends ++ [⟨.Assume seqCond, source⟩]
-      -- else
-      --   return [stmt]
 
   | .Block stmts metadata =>
       let seqStmts ← stmts.mapM transformStmt

StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean

@@ -149,6 +149,42 @@ procedure addProcCaller(): int
   // var z: int := addProc({x := 1; x}, {x := x + 10; x}) + (x := 3);
   // assert z == 15
 };
+
+// Test: dangling if in expression position (needsCondVar == false when type is void)
+procedure danglingIfInExpression(b: bool)
+  opaque
+{
+  var x: int := 0;
+  if b then { x := 1 };
+  assert (if b then { x == 1 } else { x == 0 })
+};
+
+// Test: assert/assume in expression position (lifted by the pass)
+procedure assertInExpressionPosition()
+  opaque
+{
+  var x: int := 0;
+  x := 1;
+  var y: int := { assert x == 1; x + 1 };
+  assert y == 2
+};
+
+procedure assumeInExpressionPosition()
+  opaque
+{
+  var x: int := 0;
+  x := 1;
+  var y: int := { assume x == 1; x + 1 };
+  assert y == 2
+};
+
+// Test: assignment to a fresh variable in expression position (line 287 feature)
+procedure freshVarAssignInExpression()
+  opaque
+{
+  var r: int := { var z: int := 42; z };
+  assert r == 42
+};
 "
 
 #guard_msgs (error, drop all) in