Fix Python translation pipeline: InstanceCall, control flow, and construct support

Strata/Languages/Laurel/HeapParameterization.lean

@@ -178,7 +178,7 @@ def boxDestructorName (model : SemanticModel) (ty : HighType) : Identifier :=
   | .UserDefined name =>
       if isDatatype model name then s!"Box..{name.text}Val!"
       else "Box..compositeVal!"
-  | .TCore name => s!"Box..{name}Val!"
+  | .TCore name => s!"Box..{name}Val"
   | _ => dbg_trace f!"BUG, boxDestructorName bad type {ty}"; "boxDestructorNameError"
 
 /-- Get the Box constructor name for a given Laurel HighType.

Strata/Languages/Laurel/LaurelToCoreTranslator.lean

@@ -296,7 +296,14 @@ def translateExpr (expr : StmtExprMd)
   | .ContractOf _ _ => throwExprDiagnostic $ md.toDiagnostic "contractOf expression translation" DiagnosticType.NotYetImplemented
   | .Abstract => throwExprDiagnostic $ md.toDiagnostic "abstract expression translation" DiagnosticType.NotYetImplemented
   | .All => throwExprDiagnostic $ md.toDiagnostic "all expression translation" DiagnosticType.NotYetImplemented
-  | .InstanceCall target callee args => throwExprDiagnostic $ md.toDiagnostic "instance call expression translation" DiagnosticType.NotYetImplemented
+  | .InstanceCall _target callee args =>
+      -- Note: target (self) is not passed as an argument because PySpec procedures
+      -- have self stripped from their signatures. When user-defined class methods
+      -- are supported, this will need to prepend target to the argument list.
+      let fnOp : Core.Expression.Expr := .op () ⟨callee.text, ()⟩ none
+      args.attach.foldlM (fun acc ⟨arg, _⟩ => do
+        let re ← translateExpr arg boundVars isPureContext
+        return .app () acc re) fnOp
   | .PureFieldUpdate _ _ _ => throwExprDiagnostic $ md.toDiagnostic "pure field update expression translation" DiagnosticType.NotYetImplemented
   | .This => throwExprDiagnostic $ md.toDiagnostic "this expression translation" DiagnosticType.NotYetImplemented
   termination_by expr
@@ -332,6 +339,13 @@ private def exprAsUnusedInit (expr : StmtExprMd) (md : Imperative.MetaData Core.
   let coreType := LTy.forAll [tyVarName] (.ftvar tyVarName)
   return [Core.Statement.init ident coreType (some coreExpr) md]
 
+/-- Check if a callee resolves to a procedure with no outputs (void). -/
+private def isVoidProcedure (model : SemanticModel) (callee : Identifier) : Bool :=
+  match model.get callee with
+  | .staticProcedure proc => proc.outputs.isEmpty
+  | .instanceProcedure _ proc => proc.outputs.isEmpty
+  | _ => false
+
 /--
 Translate Laurel StmtExpr to Core Statements using the `TranslateM` monad.
 Diagnostics are emitted into the monad state.
@@ -370,13 +384,18 @@ def translateStmt (outputParams : List Parameter) (stmt : StmtExprMd)
             let coreArgs ← args.mapM (fun a => translateExpr a)
             let defaultExpr := defaultExprForType model ty
             let initStmt := Core.Statement.init ident coreType (some defaultExpr) md
-            let callStmt := Core.Statement.call [ident] callee.text coreArgs md
+            -- Void procedures have no outputs; emit call without assignment target
+            let lhs := if isVoidProcedure model callee then [] else [ident]
+            let callStmt := Core.Statement.call lhs callee.text coreArgs md
             return [initStmt, callStmt]
-      | some (⟨ .InstanceCall .., _⟩) =>
+      | some (⟨ .InstanceCall _target callee args, callMd⟩) =>
           -- Instance method call as initializer: var name := target.method(args)
-          -- Havoc the result since instance methods may be on unmodeled types
-          let initStmt := Core.Statement.init ident coreType none md
-          return [initStmt]
+          let coreArgs ← args.mapM (fun a => translateExpr a)
+          let defaultExpr := defaultExprForType model ty
+          let initStmt := Core.Statement.init ident coreType (some defaultExpr) md
+          let lhs := if isVoidProcedure model callee then [] else [ident]
+          let callStmt := Core.Statement.call lhs callee.text coreArgs callMd
+          return [initStmt, callStmt]
       | some (⟨ .Hole _ _, _⟩) =>
           -- Hole initializer: treat as havoc (init without value)
           return [Core.Statement.init ident coreType none md]
@@ -399,10 +418,13 @@ def translateStmt (outputParams : List Parameter) (stmt : StmtExprMd)
               else
                 -- Procedure calls need to be translated as call statements
                 let coreArgs ← args.mapM (fun a => translateExpr a)
-                return [Core.Statement.call [ident] callee.text coreArgs md]
-          | .InstanceCall .. =>
-              -- Instance method call: havoc the target variable
-              return [Core.Statement.havoc ident md]
+                let lhs := if isVoidProcedure model callee then [] else [ident]
+                return [Core.Statement.call lhs callee.text coreArgs md]
+          | .InstanceCall _target callee args =>
+              -- Instance method call: call callee(args) with result assigned
+              let coreArgs ← args.mapM (fun a => translateExpr a)
+              let lhs := if isVoidProcedure model callee then [] else [ident]
+              return [Core.Statement.call lhs callee.text coreArgs md]
           | _ =>
               let coreExpr ← translateExpr value
               return [Core.Statement.set ident coreExpr md]
@@ -417,13 +439,14 @@ def translateStmt (outputParams : List Parameter) (stmt : StmtExprMd)
                 | .Identifier name => some (⟨name.text, ()⟩)
                 | _ => none
               return [Core.Statement.call lhsIdents callee.text coreArgs value.md]
-          | .InstanceCall .. =>
-              -- Instance method call: havoc all target variables
-              let havocStmts := targets.filterMap fun t =>
+          | .InstanceCall _target callee args =>
+              -- Instance method call: call callee(args) with all targets assigned
+              let coreArgs ← args.mapM (fun a => translateExpr a)
+              let lhsIdents := targets.filterMap fun t =>
                 match t.val with
-                | .Identifier name => some (Core.Statement.havoc ⟨name.text, ()⟩ md)
+                | .Identifier name => some (⟨name.text, ()⟩)
                 | _ => none
-              return (havocStmts)
+              return [Core.Statement.call lhsIdents callee.text coreArgs value.md]
           | _ =>
               emitDiagnostic $ md.toDiagnostic "Assignments with multiple target but without a RHS call should not be constructed"
               returnNone
@@ -442,9 +465,10 @@ def translateStmt (outputParams : List Parameter) (stmt : StmtExprMd)
       else
         let coreArgs ← args.mapM (fun a => translateExpr a)
         return [Core.Statement.call [] callee.text coreArgs md]
-  | .InstanceCall .. =>
-      -- Instance method call as statement: no return value, treated as no-op
-      return ([])
+  | .InstanceCall _target callee args =>
+      -- Instance method call as statement: call callee(args) with no return
+      let coreArgs ← args.mapM (fun a => translateExpr a)
+      return [Core.Statement.call [] callee.text coreArgs md]
   | .Return valueOpt =>
       match valueOpt, outputParams.head? with
       | some value, some outParam =>
@@ -529,6 +553,69 @@ def translateProcedure (proc : Procedure) : TranslateM Core.Procedure := do
   let spec : Core.Procedure.Spec := { modifies, preconditions, postconditions }
   return { header, spec, body }
 
+/--
+Check if a Laurel expression is pure (contains no side effects).
+Used to determine if a procedure can be translated as a Core function.
+-/
+private def isPureExpr(expr: StmtExprMd): Bool :=
+  match _h : expr.val with
+  | .LiteralBool _ => true
+  | .LiteralInt _ => true
+  | .LiteralString _ => true
+  | .LiteralDecimal _ => true
+  | .Identifier _ => true
+  | .PrimitiveOp _ args => args.attach.all (fun ⟨a, _⟩ => isPureExpr a)
+  | .IfThenElse c t none => isPureExpr c && isPureExpr t
+  | .IfThenElse c t (some e) => isPureExpr c && isPureExpr t && isPureExpr e
+  | .StaticCall _ args => args.attach.all (fun ⟨a, _⟩ => isPureExpr a)
+  | .New _ => false
+  | .ReferenceEquals e1 e2 => isPureExpr e1 && isPureExpr e2
+  | .Block [single] _ => isPureExpr single
+  | .Block _ _ => false
+  -- Statement-like
+  | .LocalVariable .. => true
+  | .While .. => false
+  | .Exit .. => false
+  | .Return .. => false
+  -- Expression-like
+  | .Assign .. => false
+  | .FieldSelect .. => true
+  | .PureFieldUpdate .. => true
+  -- Instance related
+  | .This => panic s!"isPureExpr not implemented for This"
+  | .AsType .. => panic s!"isPureExpr not supported for AsType"
+  | .IsType .. => panic s!"isPureExpr not supported for IsType"
+  | .InstanceCall .. => false
+  -- Verification specific
+  | .Forall .. => panic s!"isPureExpr not implemented for Forall"
+  | .Exists .. => panic s!"isPureExpr not implemented for Exists"
+  | .Assigned .. => panic s!"isPureExpr not supported for AsType"
+  | .Old .. => panic s!"isPureExpr not supported for AsType"
+  | .Fresh .. => panic s!"isPureExpr not supported for AsType"
+  | .Assert .. => panic s!"isPureExpr not implemented for Assert"
+  | .Assume .. => panic s!"isPureExpr not implemented for Assume"
+  | .ProveBy .. => panic s!"isPureExpr not implemented for ProveBy"
+  | .ContractOf .. => panic s!"isPureExpr not implemented for ContractOf"
+  | .Abstract => panic s!"isPureExpr not implemented for Abstract"
+  | .All => panic s!"isPureExpr not implemented for All"
+  -- Dynamic / closures
+  | .Hole _ _ => true
+  termination_by sizeOf expr
+  decreasing_by all_goals (have := WithMetadata.sizeOf_val_lt expr; term_by_mem)
+
+/-- Check if a pure-marked procedure can actually be represented as a Core function:
+    transparent body that is a pure expression and has exactly one output. -/
+private def canBeCoreFunctionBody (proc : Procedure) : Bool :=
+  match proc.body with
+  | .Transparent bodyExpr =>
+    isPureExpr bodyExpr &&
+    proc.outputs.length == 1
+  | .Opaque _ bodyExprOption _ =>
+    (bodyExprOption.map isPureExpr).getD true &&
+    proc.outputs.length == 1
+  | .External => false
+  | _ => false
+
 /--
 Translate a Laurel Procedure to a Core Function (when applicable) using `TranslateM`.
 Diagnostics for disallowed constructs in the function body are emitted into the monad state.

Strata/Languages/Laurel/LaurelTypes.lean

@@ -52,7 +52,14 @@ def computeExprType (model : SemanticModel) (expr : StmtExprMd) : HighTypeMd :=
     | astNode =>
       dbg_trace s!"BUG: static call to {callee} not to a procedure but to a {repr astNode}"
       default
-  | .InstanceCall _ _ _ => default -- TODO: implement
+  | .InstanceCall _ callee _ => match model.get callee with
+    | .instanceProcedure _ proc => match proc.outputs with
+      | [singleOutput] => singleOutput.type
+      | _ => { val := .TVoid, md := default }
+    | .staticProcedure proc => match proc.outputs with
+      | [singleOutput] => singleOutput.type
+      | _ => { val := .TVoid, md := default }
+    | _ => { val := HighType.Unknown, md := default }
   -- Operators
   | .PrimitiveOp op args =>
       match args with

Strata/Languages/Laurel/Resolution.lean

@@ -121,6 +121,7 @@ def SemanticModel.get (model: SemanticModel) (iden: Identifier): AstNode :=
 def SemanticModel.isFunction (model: SemanticModel) (id: Identifier): Bool :=
   match model.get id with
       | .staticProcedure proc => proc.isFunctional
+      | .instanceProcedure _ proc => proc.isFunctional
       | .parameter _ => true
       | .datatypeConstructor _ _ => true
       | .constant _ => true