From 668ee08253b42bd3caf469f73ddf1ded457e1199 Mon Sep 17 00:00:00 2001 From: keyboardDrummer-bot Date: Fri, 5 Jun 2026 13:42:16 +0000 Subject: [PATCH 1/3] Add tests for lifting pass features and remove commented-out code Tests added to T2_ImpureExpressions.lean: - Dangling if in expression position (needsCondVar == false) - Assert/assume in expression position (lifted by the pass) - Assignment to fresh variable in expression position Removed commented-out code: - Assert/Assume cases in onlyKeepSideEffectStmtsAndLast - Old conditional guards in transformStmt for Assert/Assume - LiftExpressionAssignments pass from Laurel pipeline - EliminateMultipleOutputs/InlineLocalVariablesInExpressions from corePipeline --- .../Laurel/LaurelCompilationPipeline.lean | 8 ----- .../Laurel/LiftImperativeExpressions.lean | 14 -------- .../Fundamentals/T2_ImpureExpressions.lean | 36 +++++++++++++++++++ 3 files changed, 36 insertions(+), 22 deletions(-) diff --git a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean index 97266ab1d7..4fae561b65 100644 --- a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean +++ 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 } diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean index c18b667639..aa04e5b7e5 100644 --- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean +++ b/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 diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean index 28584de204..0b74bc0c81 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean +++ b/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 From 52dfdcedafed3aeb164d469789ac1c02fd51768a Mon Sep 17 00:00:00 2001 From: keyboardDrummer-bot Date: Mon, 8 Jun 2026 11:27:16 +0000 Subject: [PATCH 2/3] Contract pass: assert postconditions in body for opaque procedures Move postcondition assertions into the procedure body for opaque procedures with implementation, matching the transparent case. The postconditions are now asserted as inline statements after the implementation rather than being kept in the Opaque postconditions list for the Core translator to handle. This ensures consistent behavior: separate $pre and $post helper procedures are generated per condition, used at call sites via assert/assume, while the procedure's own body asserts the raw conditions directly. --- Strata/Languages/Laurel/ContractPass.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Strata/Languages/Laurel/ContractPass.lean b/Strata/Languages/Laurel/ContractPass.lean index 0ae17de08e..1258ced791 100644 --- a/Strata/Languages/Laurel/ContractPass.lean +++ b/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 [] (some ⟨.Block (preAssumes ++ [impl] ++ postAsserts) none, impl.source⟩) [] | .Opaque _ none mods => .Opaque postconds none mods - | .Abstract _ => + | .Abstract postconds => .Abstract postconds | b => b From 311b65e91574aa55fc83e86b1c4b239990d43e1e Mon Sep 17 00:00:00 2001 From: keyboardDrummer-bot Date: Mon, 8 Jun 2026 12:18:19 +0000 Subject: [PATCH 3/3] Fix: keep postconditions in Opaque list, do not add inline assertions The original change cleared postconditions from the Opaque list and added inline assertions. This broke pyAnalyze golden-file tests because the Core translator uses the Opaque postconditions list to generate spec postconditions (which produce the named obligation results in verification output). Keep postconditions in the Opaque list for spec generation while preserving the refactoring that hoists postAsserts computation and fixes the Abstract pattern binding. --- Strata/Languages/Laurel/ContractPass.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Strata/Languages/Laurel/ContractPass.lean b/Strata/Languages/Laurel/ContractPass.lean index 1258ced791..96ffa820f3 100644 --- a/Strata/Languages/Laurel/ContractPass.lean +++ b/Strata/Languages/Laurel/ContractPass.lean @@ -124,7 +124,7 @@ private def transformProcBody (proc : Procedure) (info : ContractInfo) : Body := | .Transparent body => .Transparent ⟨.Block (preAssumes ++ [body] ++ postAsserts) none, body.source⟩ | .Opaque _ (some impl) _ => - .Opaque [] (some ⟨.Block (preAssumes ++ [impl] ++ postAsserts) none, impl.source⟩) [] + .Opaque postconds (some ⟨.Block (preAssumes ++ [impl]) none, impl.source⟩) [] | .Opaque _ none mods => .Opaque postconds none mods | .Abstract postconds =>