Lift unlabeled block expressions emitted by Python-to-Laurel

[tautschnig]

he Python-to-Laurel translator emits unlabeled Block expressions in expression position for several patterns, including modeled method calls with precondition tag checks ({ asserts...; Call }) and unmodeled method calls (PR #1019: { havocs...; Hole }). These patterns trigger block expression should have been lowered in a separate pass errors in LaurelToCoreTranslator for nested cases, because LiftImperativeExpressions was not fully lowering blocks/assignments embedded inside declare-with-init initializers.

LaurelToCoreTranslator does already handle several block-in-expression patterns natively:

• .Block [single] — singleton blocks
• .Block (.Assign [.Declare ⟨name, ty⟩] init :: rest) — translated as a let-binding (app(abs(name, body), value))

so this PR is now scoped narrowly to make sure only valid expression blocks reach the translator, rather than collapsing block structure unconditionally.

Changes in LiftImperativeExpressions.lean:

1. transformExpr.Assign for .Declare targets without substitution now recursively transforms the initializer with a fresh prepend stack and reassembles state as outerPrepends ++ innerPrepends ++ [liftedDecl], returning a Var(.Local name) reference as the expression's value. Previously the case did return expr early, leaving inner blocks / assignments / nondeterministic holes in the initializer unlowered. The outerPrepends-first ordering preserves correct execution order when a substitution-introducing snapshot decl (from a later-in-source assignment, processed earlier in the right-to-left traversal) is referenced from the transformed initializer.

2. New helper containsAssignmentOutsideUnlabeledBlock is used by the .Assert / .Assume cases of transformStmt. These cases previously bailed out whenever the condition contained any assignment; they now proceed when the assignment is confined to an unlabeled block — since the .Block case of transformExpr together with onlyKeepSideEffectStmtsAndLast will safely lift those side effects as prepends.

   The original containsAssignment is preserved for the ITE case, which correctly isolates branch-local prepends when a branch contains assignments.

3. transformExpr.Block is unchanged in its structural behavior: sub-expressions are recursively transformed, side effects are extracted via onlyKeepSideEffectStmtsAndLast, and the result is wrapped back as a Block. We deliberately do not collapse Block structure here so that singleton blocks and var x := init-prefixed blocks remain in shape for the translator's let-binding case.

A regression test (nestedBlockInDeclInit) covering the { var t := { x := 1; x }; t + 1 } pattern is added to LiftExpressionAssignmentsTest.lean. Existing test expected outputs are kept consistent with this approach (singleton blocks { x } / { y } / { 0 } / { t + 1 } rather than unwrapped values).

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 ...

[tautschnig]

@keyboardDrummer:

Good point. In 977afc1 I reverted the wholesale .Block unwrapping so let-binding-shaped blocks ({ var x := init; ...; e }) and singletons reach LaurelToCoreTranslator intact.

Re: havoc_stmt — for the unmodeled-call pattern (PythonToLaurel.translateCall) it's a destructive Assign [.Local recv] .Hole over an existing local; after EliminateHoles runs the trailing hole becomes hole(Unknown), so by lift time the pattern is { x := hole(Unknown); …; hole(Unknown) }, which the existing .Assign[.Local] lift path reduces to a singleton { hole(Unknown) } — the translator already handles it. The { asserts; Call } case is similarly handled (asserts hoisted, residual { Call } is a singleton). No new translator case needed.

[keyboardDrummer]

for the unmodeled-call pattern (PythonToLaurel.translateCall) it's a destructive Assign [.Local recv] .Hole over an existing local; after EliminateHoles runs the trailing hole becomes hole(Unknown), so by lift time the pattern is { x := hole(Unknown); …; hole(Unknown) }, which the existing .Assign[.Local] lift path reduces to a singleton { hole(Unknown) } — the translator already handles it. The { asserts; Call } case is similarly handled (asserts hoisted, residual { Call } is a singleton). No new translator case needed.

If the holes are already covered, what cases do you still need block lifting for? Is it just assertions/assumptions that occur in expressions? Can we not lift those then? My feeling is that block lifting, while probably effective for correctness, is not the most idiomatic solution.

You can add

  | .Assume cond =>
      let prepends ← takePrepends
      let seqCond ← transformExpr cond
      let argPrepends ← takePrepends
      modify fun s => { s with prependedStmts := argPrepends ++ [⟨.Assume seqCond, source⟩] ++ prepends }
      default

  | .Assert cond =>
      let prepends ← takePrepends
      let seqCond ← transformExpr cond.condition
      let argPrepends ← takePrepends
      modify fun s => { s with prependedStmts := argPrepends ++ [⟨.Assert { cond with condition := seqCond }, source⟩] ++ prepends }
      default

to transformExpr to lift those.

[tautschnig]

If the holes are already covered, what cases do you still need block lifting for? Is it just assertions/assumptions that occur in expressions? Can we not lift those then? My feeling is that block lifting, while probably effective for correctness, is not the most idiomatic solution.
[...]

Good call — done in ad373f9. transformExpr now has .Assert/.Assume cases that recursively transform the condition and lift the assert/assume to the prepend stack with a leaf placeholder, replacing the special-casing in onlyKeepSideEffectStmtsAndLast. As a side benefit this also fixes a latent case my earlier draft missed — an assert/assume inside an expression-position block whose condition contains another unlabeled block with an assignment — covered by a new nestedAssertInBlockExpr regression test.

The containsAssignmentOutsideUnlabeledBlock guard is kept so a top-level destructive assignment in a condition (e.g. assert (x := 2) == 2) still surfaces the existing destructive assignments are not supported in functions or contracts diagnostic from LaurelToCoreTranslator rather than getting silently lifted.

[keyboardDrummer]

// Regression for #1133: an unlabeled-block expression that contains a
// destructive assignment must be admissible inside an assert condition.

Why must that be admissible? What is the use-case? I was planning to update Resolution.lean so it explicitly rejects assignments to variables that occur inside assert/assume but were the variable was defined outside of it.

[ssomayyajula]

Is the catch-all to false actually correct here? I'm having trouble understanding what happens if it returns a "false negative" to transformExpr. Is it "accidentally correct" since transformExpr has a catch-all that doesn't recurse into the same variants?