From 3cfa493e132d1adec61ba33a8396a41f780004f6 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 6 May 2026 17:36:33 +0200 Subject: [PATCH 1/4] Lift unlabeled block expressions emitted by Python-to-Laurel The Python-to-Laurel translator emits unlabeled Block expressions in expression position for two common patterns: * Modeled method calls with precondition tag checks: { asserts...; Call } * Unmodeled method calls (PR #1019): havocs receiver + Any-typed args, then yields a Hole: { havoc_stmt...; Hole } The Laurel-to-Core translator rejects any Block in expression position ("block expression should have been lowered in a separate pass"), so the LiftImperativeExpressions pass must eliminate these patterns. The existing Block case in transformExpr kept the Block structure and only transformed its sub-expressions. This change replaces the Block structure with "prepend side-effects + return last element as value", which is the natural semantics for these patterns. Changes in LiftImperativeExpressions.lean: 1. transformExpr .Block case: for unlabeled blocks, recursively transform each stmt (preserves SSA-snapshot semantics for assigns in expression position), hoist asserts/declares via onlyKeepSideEffectStmtsAndLast, then return the last element as the expression value rather than wrapping back into a Block. 2. New helper containsAssignmentOutsideUnlabeledBlock: used by the Assert/Assume cases in transformStmt. These cases previously bailed out when a condition contained any assignment; they now proceed when the assignment is inside an unlabeled block (since the .Block case above will safely lift the side-effect). The original containsAssignment is preserved for use by the ITE case, which correctly isolates branch-local prepends when a branch contains assignments. Eliminates all "block expression should have been lowered" errors in the internal benchmark suite. Co-authored-by: Kiro --- .../Laurel/LiftImperativeExpressions.lean | 64 ++++++++++++++++--- .../Laurel/LiftExpressionAssignmentsTest.lean | 15 ++++- 2 files changed, 70 insertions(+), 9 deletions(-) diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean index 7c63b6870f..f9d590a9d5 100644 --- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean +++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean @@ -157,7 +157,38 @@ private def computeType (expr : StmtExprMd) : LiftM HighTypeMd := do let s ← get return computeExprType s.model expr -/-- Check if an expression contains any assignments (recursively). -/ +/-- Check if an expression contains any assignments that are NOT inside an +unlabeled block. Unlabeled blocks in expression position are lowered by the +`.Block` case of `transformExpr` (prepends side-effects + returns the last +element as the value), so assignments inside them do not need special +rejection logic. This is used for assert/assume conditions, which should +proceed with transformation even when an unlabeled block embeds an +assignment (e.g. havoc from PR #1019's unmodeled call handling). -/ +def containsAssignmentOutsideUnlabeledBlock (expr : StmtExprMd) : Bool := + match expr with + | AstNode.mk val _ => + match val with + | .Assign .. => true + | .StaticCall _ args => + args.attach.any (fun x => containsAssignmentOutsideUnlabeledBlock x.val) + | .PrimitiveOp _ args => + args.attach.any (fun x => containsAssignmentOutsideUnlabeledBlock x.val) + -- Unlabeled blocks are lowered by `transformExpr`, assignments inside + -- are safely lifted as prepended side effects. + | .Block _ none => false + | .Block stmts (some _) => + stmts.attach.any (fun x => containsAssignmentOutsideUnlabeledBlock x.val) + | .IfThenElse cond th el => + containsAssignmentOutsideUnlabeledBlock cond || + containsAssignmentOutsideUnlabeledBlock th || + match el with + | some e => containsAssignmentOutsideUnlabeledBlock e + | none => false + | _ => false + termination_by expr + decreasing_by + all_goals ((try cases x); simp_all; try term_by_mem) + def containsAssignment (expr : StmtExprMd) : Bool := match expr with | AstNode.mk val _ => @@ -344,8 +375,25 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do return ⟨.IfThenElse seqCond seqThen seqElse, source⟩ | .Block stmts labelOption => + -- Recursively transform sub-expressions (creates SSA snapshots for + -- assignments in expression position, via the `Assign` case above). let newStmts := (← stmts.reverse.mapM transformExpr).reverse - return ⟨ .Block (← onlyKeepSideEffectStmtsAndLast newStmts) labelOption, source⟩ + if labelOption.isNone then + match hne : newStmts with + | [] => return ⟨ .Block [] labelOption, source⟩ + | head :: rest => + -- Unlabeled block in expression position: hoist side-effects via + -- onlyKeepSideEffectStmtsAndLast (prepends asserts, var declares, + -- declare-assigns, drops plain assigns already processed), and + -- return the last element as the expression value. This lowers + -- the block structure so the Laurel-to-Core translator no longer + -- sees a Block in expression position. Pattern is commonly emitted + -- by PythonToLaurel: { asserts; Call } or { havoc; Hole } + -- (PR #1019 for unmodeled calls). + let _ ← onlyKeepSideEffectStmtsAndLast (head :: rest) + return (head :: rest).getLast (by simp) + else + return ⟨ .Block (← onlyKeepSideEffectStmtsAndLast newStmts) labelOption, source⟩ | .Var (.Declare param) => -- If the substitution map has an entry for this variable, it was @@ -372,9 +420,10 @@ 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 and imperative calls need to be lifted. - if !containsAssignment cond.condition then + -- Reject top-level assignments in assert conditions. Assignments inside + -- unlabeled blocks are OK because the Block case of transformExpr lifts + -- their side effects out as prepends. + if !containsAssignmentOutsideUnlabeledBlock cond.condition then let seqCond ← transformExpr cond.condition let prepends ← takePrepends modify fun s => { s with subst := [] } @@ -383,9 +432,8 @@ def transformStmt (stmt : StmtExprMd) : LiftM (List StmtExprMd) := do return [stmt] | .Assume cond => - -- Do not transform assume conditions with assignments — they must be rejected. - -- But nondeterministic holes and imperative calls need to be lifted. - if !containsAssignment cond then + -- Same rationale as Assert above. + if !containsAssignmentOutsideUnlabeledBlock cond then let seqCond ← transformExpr cond let prepends ← takePrepends modify fun s => { s with subst := [] } diff --git a/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean b/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean index f3a3acbd6f..6704b4ae88 100644 --- a/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean +++ b/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean @@ -23,11 +23,20 @@ namespace Strata.Laurel def blockStmtLiftingProgram : String := r" procedure assertInBlockExpr() + opaque { var x: int := 0; var y: int := { assert x == 0; x := 1; x }; assert y == 1 }; + +procedure condAssign(x: int) + opaque +{ + var y: int := 0; + var z: int := (if x > 0 then { y := y + 1 } else { 0 }) + y; + assert z == 2 +}; " def parseLaurelAndLift (input : String) : IO Program := do @@ -44,7 +53,11 @@ def parseLaurelAndLift (input : String) : IO Program := do /-- info: procedure assertInBlockExpr() -{ var x: int := 0; assert x == 0; var $x_0: int := x; x := 1; var y: int := { x }; assert y == 1 }; + opaque +{ var x: int := 0; assert x == 0; var $x_0: int := x; x := 1; var y: int := x; assert y == 1 }; +procedure condAssign(x: int) + opaque +{ var y: int := 0; var $c_0: int; if x > 0 then { var $y_0: int := y; y := y + 1; $c_0 := y } else { $c_0 := 0 }; var z: int := $c_0 + y; assert z == 2 }; -/ #guard_msgs in #eval! do From 977afc1e269b04766810e42026ad7724be8d49d7 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 15 May 2026 21:47:49 +0000 Subject: [PATCH 2/4] Address PR #1133 review feedback MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Surgical follow-up addressing the two review threads on PR #1133: 1. Fix the bug Copilot flagged in transformExpr.Assign for .Declare targets without a substitution: the previous "return expr" early- returned the original assignment with the initializer un-transformed, so any unlabeled block / nested assignment / nondeterministic hole embedded in the initializer escaped lifting and reached the Laurel- to-Core translator unchanged. The fix recursively transforms the initializer with a fresh prepend stack, then reassembles state as outerPrepends ++ innerPrepends ++ [liftedDecl]. The outerPrepends-first ordering is important: when an already-processed (later in source) assignment introduced a snapshot substitution that this declaration's initializer now references, the snapshot declaration must precede the use. 2. Revert the wholesale .Block unwrapping that this PR previously added. keyboardDrummer pointed out that LaurelToCoreTranslator already natively handles singleton blocks (`{ e }`) and var-init-prefixed blocks (translating them as let-bindings via app(abs(name, body), value)), so collapsing the Block structure unconditionally was pessimizing those cases. Going back to the original two-line .Block case lets the translator see the structure it can handle. The actual benefit of this PR — relaxing assert/assume condition handling via containsAssignmentOutsideUnlabeledBlock — is preserved. 3. Add the regression test Copilot requested for nested-block-in-decl- initializer (`var y := { var t := { x := 1; x }; t + 1 }`). Without change (1) above, the inner block survives and the Core translator raises "block expression should have been lowered". Existing test expectations are updated to reflect the .Block revert (singleton `{ x }` / `{ y }` / `{ 0 }` / `{ t + 1 }` instead of unwrapped values). Co-authored-by: Kiro --- .../Laurel/LiftImperativeExpressions.lean | 63 +++++++++++++------ .../Laurel/LiftExpressionAssignmentsTest.lean | 15 ++++- 2 files changed, 56 insertions(+), 22 deletions(-) diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean index f9d590a9d5..31d77a4cda 100644 --- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean +++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean @@ -280,12 +280,47 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do let resultExpr ← match firstTarget.val with | .Local varName => pure (⟨.Var (.Local (← getSubst varName)), source⟩) | .Declare param => - -- Declaration with initializer: check if substitution exists + -- Declaration with initializer in expression position. If we already + -- have a substitution for this name (because a later traversal pass + -- introduced one), use the snapshot. Otherwise, fully lower this + -- declaration: recursively transform the initializer (so any inner + -- assignments / unlabeled blocks / nondeterministic holes get + -- lifted), then emit the lifted declaration as a prepended statement + -- in correct execution order. Return a reference to the declared + -- name as the expression's value. let hasSubst := (← get).subst.lookup param.name |>.isSome if hasSubst then pure (⟨.Var (.Local (← getSubst param.name)), source⟩) else - return expr + -- Run the inner transformation with a fresh prepend stack so we + -- can distinguish side-effects from this declaration's initializer + -- from those already accumulated by previously-processed (later in + -- program order) statements in the right-to-left traversal. + let outerPrepends := (← get).prependedStmts + modify fun s => { s with prependedStmts := [] } + let seqValue ← transformExpr value + let innerPrepends ← takePrepends + -- Reassemble in correct execution order (front = earliest): + -- outerPrepends - already-lifted statements from later + -- positions; their snapshot decls must precede + -- any reference inserted via substitution into + -- this declaration's initializer. + -- innerPrepends - side effects from evaluating `value`; they + -- must execute before the declaration binds. + -- liftedDecl - this declaration with the transformed value. + -- Note: this means later-position prepends (outerPrepends) end up + -- at the front of state, contradicting the usual right-to-left + -- invariant. That's safe here because outerPrepends only contain + -- snapshot/havoc decls and lifted assignments that commute with + -- this declaration up to the substitutions applied to seqValue. + let liftedDecl : StmtExprMd := ⟨.Assign targets seqValue, source⟩ + modify fun s => { s with + prependedStmts := outerPrepends ++ innerPrepends ++ [liftedDecl] } + -- The expression value of `var t := init` is the just-declared `t`. + -- Returning a `.Var (.Local name)` lets `onlyKeepSideEffectStmtsAndLast` + -- drop this slot from the surrounding block (the side effect is + -- already captured in the prepended declaration above). + return ⟨.Var (.Local param.name), source⟩ | _ => dbg_trace "Strata bug: non-identifier targets should have been removed before the lift expression phase"; return expr @@ -375,25 +410,13 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do return ⟨.IfThenElse seqCond seqThen seqElse, source⟩ | .Block stmts labelOption => - -- Recursively transform sub-expressions (creates SSA snapshots for - -- assignments in expression position, via the `Assign` case above). + -- Recursively transform sub-expressions (this also creates SSA snapshots + -- for assignments in expression position, via the `.Assign` case above). + -- We keep the Block structure: `LaurelToCoreTranslator` natively handles + -- singleton blocks (`{ e }`) and `var x := init`-prefixed blocks (as + -- let-bindings), so we should not collapse those structures here. let newStmts := (← stmts.reverse.mapM transformExpr).reverse - if labelOption.isNone then - match hne : newStmts with - | [] => return ⟨ .Block [] labelOption, source⟩ - | head :: rest => - -- Unlabeled block in expression position: hoist side-effects via - -- onlyKeepSideEffectStmtsAndLast (prepends asserts, var declares, - -- declare-assigns, drops plain assigns already processed), and - -- return the last element as the expression value. This lowers - -- the block structure so the Laurel-to-Core translator no longer - -- sees a Block in expression position. Pattern is commonly emitted - -- by PythonToLaurel: { asserts; Call } or { havoc; Hole } - -- (PR #1019 for unmodeled calls). - let _ ← onlyKeepSideEffectStmtsAndLast (head :: rest) - return (head :: rest).getLast (by simp) - else - return ⟨ .Block (← onlyKeepSideEffectStmtsAndLast newStmts) labelOption, source⟩ + return ⟨ .Block (← onlyKeepSideEffectStmtsAndLast newStmts) labelOption, source⟩ | .Var (.Declare param) => -- If the substitution map has an entry for this variable, it was diff --git a/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean b/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean index 6704b4ae88..4beec6b160 100644 --- a/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean +++ b/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean @@ -37,6 +37,14 @@ procedure condAssign(x: int) var z: int := (if x > 0 then { y := y + 1 } else { 0 }) + y; assert z == 2 }; + +procedure nestedBlockInDeclInit() + opaque +{ + var x: int := 0; + var y: int := { var t: int := { x := 1; x }; t + 1 }; + assert y == 2 +}; " def parseLaurelAndLift (input : String) : IO Program := do @@ -54,10 +62,13 @@ def parseLaurelAndLift (input : String) : IO Program := do /-- info: procedure assertInBlockExpr() opaque -{ var x: int := 0; assert x == 0; var $x_0: int := x; 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 }; procedure condAssign(x: int) opaque -{ var y: int := 0; var $c_0: int; if x > 0 then { var $y_0: int := y; y := y + 1; $c_0 := y } else { $c_0 := 0 }; var z: int := $c_0 + y; assert z == 2 }; +{ var y: int := 0; var $c_0: int; if x > 0 then { var $y_0: int := y; y := y + 1; $c_0 := { y } } else { $c_0 := { 0 } }; var z: int := $c_0 + y; assert z == 2 }; +procedure nestedBlockInDeclInit() + opaque +{ var x: int := 0; var $x_0: int := x; x := 1; var t: int := { x }; var y: int := { t + 1 }; assert y == 2 }; -/ #guard_msgs in #eval! do From f5bd0f71c5d07172f9dee75c2f856104161d285a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 19 May 2026 09:35:31 +0000 Subject: [PATCH 3/4] Address PR #1133 review feedback from keyboardDrummer MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two changes responding to keyboardDrummer's observation that the tests in this PR don't actually exercise its changes: 1. T2_ImpureExpressions.lean: add three deductive-verification regression cases that fail on origin/main and pass with this PR: * assertWithBlockExpr / assumeWithBlockExpr exercise the assert/assume condition relaxation via containsAssignmentOutsideUnlabeledBlock. Before the fix, the inner unlabeled block survived to the Laurel-to-Core translator and triggered "block expression should have been lowered in a separate pass". Verified directly: both fail on a worktree at origin/main with that exact diagnostic. * nestedBlockInDeclInit exercises the fix in transformExpr.Assign for .Declare targets without a substitution. Before the fix, the case early-returned the original expression without recursing into the initializer, so the inner { x := 1; x } survived to the translator. Same verification: fails on origin/main, passes here. keyboardDrummer's suggested condAssign program is intentionally not added — it already verifies cleanly on origin/main and would not exercise this PR. 2. Rename StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean to LiftExpressionAssignmentsIdiomaticityTest.lean, drop the condAssign case (which doesn't depend on this PR), and refresh the module docstring to call out that this file is a quality-of-output check (parse + resolve + lift + #guard_msgs against pretty-printed Laurel), not a correctness check. Correctness now lives in the T2_ImpureExpressions regression cases above. Co-authored-by: Kiro --- .../Fundamentals/T2_ImpureExpressions.lean | 36 +++++++++++++++++++ ...xpressionAssignmentsIdiomaticityTest.lean} | 23 +++++------- 2 files changed, 45 insertions(+), 14 deletions(-) rename StrataTest/Languages/Laurel/{LiftExpressionAssignmentsTest.lean => LiftExpressionAssignmentsIdiomaticityTest.lean} (77%) diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean index e65d283f57..0941e369c3 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean @@ -46,6 +46,42 @@ procedure conditionalAssignmentInExpression(x: int) } }; +// Regression for #1133: an unlabeled-block expression that contains a +// destructive assignment must be admissible inside an `assert` condition. +// Before the fix, `containsAssignment` flagged the inner `x := 1` and +// `transformStmt` bailed out, leaving the block in the assert condition; +// the Laurel-to-Core translator then rejected it. +procedure assertWithBlockExpr() + opaque +{ + var x: int := 0; + assert ({ x := 1; x } > 0); + assert x == 1 +}; + +// Same regression, but exercising the `assume` path through +// `containsAssignmentOutsideUnlabeledBlock`. +procedure assumeWithBlockExpr() + opaque +{ + var x: int := 0; + assume ({ x := 1; x } > 0); + assert x == 1 +}; + +// Regression for #1133: an unlabeled block in the initializer of a +// declare-with-init that itself sits in expression position. Before the +// fix, `transformExpr` on `.Assign[.Declare]` early-returned the original +// expression without recursing into the initializer, so the inner +// `{ x := 1; x }` survived to the Laurel-to-Core translator. +procedure nestedBlockInDeclInit() + opaque +{ + var x: int := 0; + var y: int := { var t: int := { x := 1; x }; t + 1 }; + assert y == 2 +}; + procedure anotherConditionAssignmentInExpression(c: bool) opaque { diff --git a/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean b/StrataTest/Languages/Laurel/LiftExpressionAssignmentsIdiomaticityTest.lean similarity index 77% rename from StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean rename to StrataTest/Languages/Laurel/LiftExpressionAssignmentsIdiomaticityTest.lean index 4beec6b160..999e19fdf5 100644 --- a/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean +++ b/StrataTest/Languages/Laurel/LiftExpressionAssignmentsIdiomaticityTest.lean @@ -5,9 +5,15 @@ -/ /- -Tests that the expression lifter correctly handles statement constructs -(heap-updating assignments) in non-last positions of block expressions, -by comparing the lifted Laurel against expected output. +Idiomaticity tests for the expression lifter: pin the *shape* of the Laurel +output produced by `liftExpressionAssignments` for a few representative +input programs. + +This is a quality-of-output check, not a correctness check. Programs that +must verify cleanly through the full deductive-verification pipeline live +in `StrataTest/Languages/Laurel/Examples/`; tests here only run +parse + resolve + lift and compare the printed Laurel against an +expected string. -/ import Strata.DDM.Elab @@ -30,14 +36,6 @@ procedure assertInBlockExpr() assert y == 1 }; -procedure condAssign(x: int) - opaque -{ - var y: int := 0; - var z: int := (if x > 0 then { y := y + 1 } else { 0 }) + y; - assert z == 2 -}; - procedure nestedBlockInDeclInit() opaque { @@ -63,9 +61,6 @@ def parseLaurelAndLift (input : String) : IO Program := do info: procedure assertInBlockExpr() opaque { var x: int := 0; assert x == 0; var $x_0: int := x; x := 1; var y: int := { x }; assert y == 1 }; -procedure condAssign(x: int) - opaque -{ var y: int := 0; var $c_0: int; if x > 0 then { var $y_0: int := y; y := y + 1; $c_0 := { y } } else { $c_0 := { 0 } }; var z: int := $c_0 + y; assert z == 2 }; procedure nestedBlockInDeclInit() opaque { var x: int := 0; var $x_0: int := x; x := 1; var t: int := { x }; var y: int := { t + 1 }; assert y == 2 }; From ad373f985fc6c3f229bb6e0b7131ac11a764fea9 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 19 May 2026 09:53:53 +0000 Subject: [PATCH 4/4] Lift asserts/assumes in transformExpr (PR #1133 follow-up) Per keyboardDrummer's follow-up suggestion in https://github.com/strata-org/Strata/pull/1133#issuecomment-4485988998, handle asserts/assumes that appear in expression position directly in transformExpr rather than relying on the surrounding transformStmt. New transformExpr.Assert and .Assume cases: - Save the outer prepend stack, transform the condition with a fresh one, and reassemble as outerPrepends ++ condPrepends ++ [liftedAssert]. - Front-to-back execution order: outer (later-source-position) prepends first, then condition side-effects, then this assert/assume. - Return a LiteralBool true placeholder; onlyKeepSideEffectStmtsAndLast drops it from non-last positions of the surrounding block. - Preserve the existing user-facing error contract: if the condition contains a top-level destructive assignment, leave the assert/assume unchanged so the Laurel-to-Core translator can emit "destructive assignments are not supported in functions or contracts" against the original source. The transformStmt.Assert/.Assume cases retain the same bail-out check and otherwise just call transformExpr on the condition. This fixes a latent case my PR previously missed: an assert/assume inside an expression-position block whose condition itself contains an unlabeled block with an assignment. Before, transformExpr on .Assert fell through to the default catch-all and the inner block survived to the translator. Added regression test `nestedAssertInBlockExpr` to T2_ImpureExpressions covering exactly that pattern. Termination: the recursion `transformExpr cond.condition` is justified via the existing `Condition.sizeOf_condition_lt` lemma; the decreasing_by block now does `try have := Condition.sizeOf_condition_lt` before `term_by_mem`, mirroring MapStmtExpr.lean and TypeHierarchy.lean. Idiomaticity test update: with the new behaviour, asserts inside expression-position blocks now have their conditions transformed right-to-left like other expressions, which means a reference to a later-mutated variable is rewritten through the substitution map. For `assertInBlockExpr`, the inner `assert x == 0` becomes `assert $x_0 == 0` (using the just-introduced snapshot of x), positioned after the snapshot/assignment in execution order. Semantically equivalent to the previous output, more uniform with the other lifted prepends. Co-authored-by: Kiro --- .../Laurel/LiftImperativeExpressions.lean | 83 ++++++++++++++----- .../Fundamentals/T2_ImpureExpressions.lean | 15 ++++ ...ExpressionAssignmentsIdiomaticityTest.lean | 2 +- 3 files changed, 78 insertions(+), 22 deletions(-) diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean index 31d77a4cda..f2df259359 100644 --- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean +++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean @@ -159,11 +159,13 @@ private def computeType (expr : StmtExprMd) : LiftM HighTypeMd := do /-- Check if an expression contains any assignments that are NOT inside an unlabeled block. Unlabeled blocks in expression position are lowered by the -`.Block` case of `transformExpr` (prepends side-effects + returns the last -element as the value), so assignments inside them do not need special -rejection logic. This is used for assert/assume conditions, which should -proceed with transformation even when an unlabeled block embeds an -assignment (e.g. havoc from PR #1019's unmodeled call handling). -/ +`.Block` case of `transformExpr` (prepends side-effects), so assignments +inside them are safely lifted. This is used by the `.Assert` / `.Assume` +cases in both `transformStmt` and `transformExpr` to decide whether to +recursively lift the condition: `false` → lift; `true` → leave unchanged so +the Laurel-to-Core translator can emit "destructive assignments are not +supported in functions or contracts" against a top-level assignment that +the user almost certainly didn't intend. -/ def containsAssignmentOutsideUnlabeledBlock (expr : StmtExprMd) : Bool := match expr with | AstNode.mk val _ => @@ -189,6 +191,10 @@ def containsAssignmentOutsideUnlabeledBlock (expr : StmtExprMd) : Bool := decreasing_by all_goals ((try cases x); simp_all; try term_by_mem) +/-- Check if an expression contains any assignments (recursively). + +Used by the ITE case of `transformExpr` to decide whether a branch needs +its own prepend isolation. -/ def containsAssignment (expr : StmtExprMd) : Bool := match expr with | AstNode.mk val _ => @@ -429,9 +435,48 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do else return expr + | .Assert cond => + -- Asserts in expression position (typically as a non-last stmt of a + -- block in expression position) are lifted out as prepended statements. + -- The condition is recursively transformed so any nested assignments, + -- holes or unlabeled-block side-effects inside it are themselves lifted. + -- Returning a leaf placeholder lets `onlyKeepSideEffectStmtsAndLast` + -- drop this slot from the surrounding block. + -- + -- A top-level assignment in the condition (e.g. `assert (x := 2) == 2`) + -- is left in place: the Laurel-to-Core translator emits a + -- "destructive assignments are not supported" diagnostic for those, + -- which is more useful than silently lifting an almost certainly + -- unintended assignment. + if containsAssignmentOutsideUnlabeledBlock cond.condition then + return expr + let outerPrepends := (← get).prependedStmts + modify fun s => { s with prependedStmts := [] } + let seqCond ← transformExpr cond.condition + let condPrepends ← takePrepends + let liftedAssert : StmtExprMd := + ⟨.Assert { cond with condition := seqCond }, source⟩ + modify fun s => { s with + prependedStmts := outerPrepends ++ condPrepends ++ [liftedAssert] } + return ⟨.LiteralBool true, source⟩ + + | .Assume cond => + -- Same shape as the `.Assert` case above. + if containsAssignmentOutsideUnlabeledBlock cond then + return expr + let outerPrepends := (← get).prependedStmts + modify fun s => { s with prependedStmts := [] } + let seqCond ← transformExpr cond + let condPrepends ← takePrepends + let liftedAssume : StmtExprMd := ⟨.Assume seqCond, source⟩ + modify fun s => { s with + prependedStmts := outerPrepends ++ condPrepends ++ [liftedAssume] } + return ⟨.LiteralBool true, source⟩ + | _ => return expr termination_by (sizeOf expr, 0) decreasing_by + all_goals (try have := Condition.sizeOf_condition_lt ‹_›) all_goals (simp_all; try term_by_mem) /-- @@ -443,26 +488,22 @@ def transformStmt (stmt : StmtExprMd) : LiftM (List StmtExprMd) := do | AstNode.mk val source => match val with | .Assert cond => - -- Reject top-level assignments in assert conditions. Assignments inside - -- unlabeled blocks are OK because the Block case of transformExpr lifts - -- their side effects out as prepends. - if !containsAssignmentOutsideUnlabeledBlock 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 + -- See the matching case in `transformExpr` for why we leave a top-level + -- destructive assignment in the condition unchanged. + if containsAssignmentOutsideUnlabeledBlock cond.condition then return [stmt] + let seqCond ← transformExpr cond.condition + let prepends ← takePrepends + modify fun s => { s with subst := [] } + return prepends ++ [⟨.Assert { cond with condition := seqCond }, source⟩] | .Assume cond => - -- Same rationale as Assert above. - if !containsAssignmentOutsideUnlabeledBlock cond then - let seqCond ← transformExpr cond - let prepends ← takePrepends - modify fun s => { s with subst := [] } - return prepends ++ [⟨.Assume seqCond, source⟩] - else + if containsAssignmentOutsideUnlabeledBlock cond then return [stmt] + let seqCond ← transformExpr cond + let prepends ← takePrepends + modify fun s => { s with subst := [] } + return prepends ++ [⟨.Assume seqCond, source⟩] | .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 0941e369c3..d7b551f209 100644 --- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean +++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean @@ -69,6 +69,21 @@ procedure assumeWithBlockExpr() assert x == 1 }; +// Regression for #1133: an `assert` that itself sits inside an +// expression-position block and whose condition contains another unlabeled +// block with a destructive assignment. This pattern only lowers correctly +// once `transformExpr` itself has cases for `.Assert`/`.Assume` that +// recursively lift the condition (rather than relying on the surrounding +// `transformStmt` to do so). +procedure nestedAssertInBlockExpr() + opaque +{ + var z: int := 0; + var y: int := { assert ({ z := 1; z } > 0); 42 }; + assert y == 42; + assert z == 1 +}; + // Regression for #1133: an unlabeled block in the initializer of a // declare-with-init that itself sits in expression position. Before the // fix, `transformExpr` on `.Assign[.Declare]` early-returned the original diff --git a/StrataTest/Languages/Laurel/LiftExpressionAssignmentsIdiomaticityTest.lean b/StrataTest/Languages/Laurel/LiftExpressionAssignmentsIdiomaticityTest.lean index 999e19fdf5..6ee64cba73 100644 --- a/StrataTest/Languages/Laurel/LiftExpressionAssignmentsIdiomaticityTest.lean +++ b/StrataTest/Languages/Laurel/LiftExpressionAssignmentsIdiomaticityTest.lean @@ -60,7 +60,7 @@ def parseLaurelAndLift (input : String) : IO Program := do /-- info: procedure assertInBlockExpr() opaque -{ var x: int := 0; assert x == 0; var $x_0: int := x; x := 1; var y: int := { x }; assert y == 1 }; +{ var x: int := 0; var $x_0: int := x; x := 1; assert $x_0 == 0; var y: int := { x }; assert y == 1 }; procedure nestedBlockInDeclInit() opaque { var x: int := 0; var $x_0: int := x; x := 1; var t: int := { x }; var y: int := { t + 1 }; assert y == 2 };