Support return statements in Laurel functions

[keyboardDrummer]

Changes

Functional:

• Adds a new EliminateReturnsInExpression pass that tries to eliminate return statements.
• Adds not supported message for assert, assume, and local variable declarations without an initializer, that occur in expressions.

Refactoring:

• Introduces a MetaData type abbreviation and refactors the disallowed helper signature
• Renames boogie* variables to core* in translateStmt

Performance:

• Partitions liftImperativeExpressions to skip functional procedures. This does not change the outcome of the pipeline but it might reduce work a bit.

Testing

• Added cases to T3_ControlFlow
• Added T3_ControlFlowError to clarify that assert and assume are not yet supported in functions

[joehendrix]

Minor note: canBeCoreFunctionBody and isPureExpr in LaurelToCoreTranslator.lean (lines 451–506) appear to be dead code — neither is called anywhere in the codebase. The translation pipeline partitions by isFunctional (line 591) and attempts translation directly via tryTranslatePureToFunction, collecting diagnostics rather than pre-checking purity. Consider removing these or adding a comment explaining their intended future use.

[joehendrix]

The PR description understates the scope of this change. Beyond supporting return statements, this PR also:

• Adds a new EliminateReturnsInExpression pass that rewrites guard patterns (if-then without else) into if-then-else expression trees
• Partitions liftImperativeExpressions to skip functional procedures
• Adds translateExpr handlers for Assert, Assume, and LocalVariable blocks in pure context
• Introduces a MetaData type abbreviation and refactors the disallowed helper signature
• Renames boogie* variables to core* in translateStmt

Consider updating the description to better reflect the full set of changes.

[fabiomadge]

The return elimination pass has a wrong-code bug when a full if-else (with returns in both branches) appears as a non-last statement in a function body. We could also just disallow it, or fail properly. See inline comment for details and repro.

[joehendrix]

I left one performance comment, but I don't consider it blocking.