Lift unlabeled block expressions emitted by Python-to-Laurel

[tautschnig]

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 Python -> Laurel translation: unmodeled method calls to havoc non-receiver arguments too #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.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[Copilot]

Pull request overview

This PR updates the Laurel liftExpressionAssignments pass so that unlabeled Block expressions occurring in expression position are lowered into “prepended side-effects + final value expression”, eliminating Block nodes that the Laurel-to-Core translator rejects. This targets Python-to-Laurel output patterns like { asserts; Call } and { havoc...; Hole }, and relaxes assert/assume-condition handling to allow assignments when they occur inside such unlabeled blocks.

Changes:

• Change transformExpr’s .Block handling so unlabeled blocks are lowered by hoisting side effects and returning the last element as the value (instead of rebuilding a Block).
• Add containsAssignmentOutsideUnlabeledBlock and use it in transformStmt for .Assert / .Assume so conditions can be transformed when assignments are confined to unlabeled blocks.
• Extend lifting tests with an additional procedure to cover conditional assignment lifting behavior.

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated 2 comments.

File	Description
Strata/Languages/Laurel/LiftImperativeExpressions.lean	Lowers unlabeled block expressions to prepends + value; adjusts assert/assume filtering for assignments inside unlabeled blocks.
StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean	Adds regression coverage for unlabeled blocks in expression contexts and ITE branches.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[keyboardDrummer]

Hey, thanks for this PR. You're right that Laurel should support the code that PythonToLaurel is generating here.

One thing though, the existing error "block expression should have been lowered" is phrased too strongly. Sorry about that. LaurelToCoreTranslator is intended to support some blocks in expressions, namely the ones that can be translated to Core expressions. The intention is for a block like { var x: int := <expr1>; <expr2> } to be modeled as a Core let binding.

Could we investigate making sure that only valid expression blocks make it to LaurelToCoreTranslator, instead of preventing all expression blocks from reaching there? Lifting all blocks and not having any let expressions seems like an overly aggressive transformation that won't benefit the performance/debugability of our pipeline. Let's look at the two problematic Python cases mentioned by this PR.

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 }

Can we lift the asserts? The Laurel->Core translator will handle a singleton block { Call }

Unmodeled method calls (PR #1019): havocs receiver + Any-typed args, then yields a Hole: { havoc_stmt...; Hole }

Can you say more about what havoc_stmt looks like? If it's a destructive assignment, like x := ?, then it should have been lifted. If it's a variable declaration with (non-det) initializer, like var x: int := ?, then that's something that LaurelToCoreTranslator is intended to support. Note the case | .Block (⟨ .Assign [⟨ .Declare ⟨name, ty ⟩, _source⟩] initializer, innerSrc⟩ :: rest) label => do ...

Maybe there should be a separate case for a hole assignment in a block: | .Block (⟨ .Assign [⟨ .Declare ⟨name, ty ⟩, _source⟩] .Hole, innerSrc⟩ :: rest) label => do ...