diff --git a/.gitignore b/.gitignore
index f7d8f2cb47..3776616d98 100644
--- a/.gitignore
+++ b/.gitignore
@@ -12,4 +12,4 @@ vcs/*.smt2
 *.py.ion
 *.py.ion.core.st
 
-Strata.code-workspace
+Strata.code-workspace
\ No newline at end of file
diff --git a/Strata/Languages/Laurel/ConstrainedTypeElim.lean b/Strata/Languages/Laurel/ConstrainedTypeElim.lean
index 6b10099e4e..7e86c374a1 100644
--- a/Strata/Languages/Laurel/ConstrainedTypeElim.lean
+++ b/Strata/Languages/Laurel/ConstrainedTypeElim.lean
@@ -55,7 +55,7 @@ def constraintCallFor (ptMap : ConstrainedTypeMap) (ty : HighType)
     (varName : Identifier) (src : Option FileRange := none) : Option StmtExprMd :=
   match ty with
   | .UserDefined name => if ptMap.contains name.text then
-      some ⟨.StaticCall (mkId s!"{name.text}$constraint") [⟨.Identifier varName, src⟩], src⟩
+      some ⟨.StaticCall (mkId s!"{name.text}$constraint") [⟨.Var (.Local varName), src⟩], src⟩
     else none
   | _ => none
 
@@ -68,7 +68,7 @@ def mkConstraintFunc (ptMap : ConstrainedTypeMap) (ct : ConstrainedType) : Proce
       if ptMap.contains parent.text then
         let paramId := { ct.valueName with uniqueId := none }
         let paramRef : StmtExprMd :=
-          { val := .Identifier paramId, source := none }
+          { val := .Var (.Local paramId), source := none }
         let parentCall : StmtExprMd :=
           { val := .StaticCall (mkId s!"{parent.text}$constraint") [paramRef], source := none }
         { val := .PrimitiveOp .And [ct.constraint, parentCall], source := none }
@@ -86,14 +86,21 @@ private def wrap (stmts : List StmtExprMd) (src : Option FileRange)
     : StmtExprMd :=
   match stmts with | [s] => s | ss => ⟨.Block ss none, src⟩
 
+def resolveVariable (ptMap : ConstrainedTypeMap) (v : VariableMd) : VariableMd :=
+  match v.val with
+  | .Declare param => ⟨.Declare { param with type := resolveType ptMap param.type }, v.source⟩
+  | _ => v
+
 /-- Resolve constrained types in type positions and inject constraint calls into quantifier bodies.
     Recursion into StmtExprMd children is handled by `mapStmtExpr`. -/
 def resolveExprNode (ptMap : ConstrainedTypeMap) (expr : StmtExprMd) : StmtExprMd :=
   let source := expr.source
 
   match expr.val with
-  | .LocalVariable n ty init =>
-    ⟨.LocalVariable n (resolveType ptMap ty) init, source⟩
+  | .Assign targets value =>
+    ⟨.Assign (targets.map (resolveVariable ptMap)) value, source⟩
+  | .Var (.Declare param) =>
+    ⟨.Var (.Declare { param with type := resolveType ptMap param.type }), source⟩
   | .Quantifier mode param trigger body =>
     let param' := { param with type := resolveType ptMap param.type }
     -- With bottom-up traversal, `body` is already recursed into. The newly
@@ -122,25 +129,31 @@ def elimStmt (ptMap : ConstrainedTypeMap)
   let source := stmt.source
 
   match _h : stmt.val with
-  | .LocalVariable name ty init =>
-    let callOpt := constraintCallFor ptMap ty.val name (src := source)
-    if callOpt.isSome then modify fun pv => pv.insert name.text ty.val
-    let (init', check) : Option StmtExprMd × List StmtExprMd := match init with
-      | none => match callOpt with
-        | some c => (none, [⟨.Assume c, source⟩])
-        | none => (none, [])
-      | some _ => (init, callOpt.toList.map fun c => ⟨.Assert { condition := c }, source⟩)
-    pure ([⟨.LocalVariable name ty init', source⟩] ++ check)
-
-  | .Assign [target] _ => match target.val with
-    | .Identifier name => do
-      match (← get).get? name.text with
-      | some ty =>
-        let assert := (constraintCallFor ptMap ty name (src := source)).toList.map
-          fun c => ⟨.Assert { condition := c }, source⟩
-        pure ([stmt] ++ assert)
-      | none => pure [stmt]
-    | _ => pure [stmt]
+  | .Var (.Declare param) =>
+    let callOpt := constraintCallFor ptMap param.type.val param.name (src := source)
+    if callOpt.isSome then modify fun pv => pv.insert param.name.text param.type.val
+    let check := match callOpt with
+      | some c => [⟨.Assume c, source⟩]
+      | none => []
+    pure ([stmt] ++ check)
+
+  | .Assign targets _value =>
+    -- Handle Declare targets for constrained type elimination
+    let declareChecks ← targets.foldlM (init := ([] : List StmtExprMd)) fun acc target =>
+      match target.val with
+      | .Declare param => do
+        let callOpt := constraintCallFor ptMap param.type.val param.name (src := source)
+        if callOpt.isSome then modify fun pv => pv.insert param.name.text param.type.val
+        pure (acc ++ callOpt.toList.map fun c => ⟨.Assert { condition := c }, source⟩)
+      | .Local name => do
+        match (← get).get? name.text with
+        | some ty =>
+          let assert := (constraintCallFor ptMap ty name (src := source)).toList.map
+            fun c => ⟨.Assert { condition := c }, source⟩
+          pure (acc ++ assert)
+        | none => pure acc
+      | _ => pure acc
+    pure ([stmt] ++ declareChecks)
 
   | .Block stmts sep =>
     let stmtss ← inScope (stmts.mapM (elimStmt ptMap))
@@ -205,7 +218,7 @@ private def mkWitnessProc (ptMap : ConstrainedTypeMap) (ct : ConstrainedType) :
 
   let witnessId : Identifier := mkId "$witness"
   let witnessInit : StmtExprMd :=
-    ⟨.LocalVariable witnessId (resolveType ptMap ct.base) (some ct.witness), src⟩
+    ⟨.Assign [⟨.Declare ⟨witnessId, resolveType ptMap ct.base⟩, src⟩] ct.witness, src⟩
   let assert : StmtExprMd :=
     ⟨.Assert { condition := (constraintCallFor ptMap (.UserDefined ct.name) witnessId (src := src)).get! }, src⟩
   { name := mkId s!"$witness_{ct.name.text}"
diff --git a/Strata/Languages/Laurel/CoreDefinitionsForLaurel.lean b/Strata/Languages/Laurel/CoreDefinitionsForLaurel.lean
index e86d14dcad..2df59b8ceb 100644
--- a/Strata/Languages/Laurel/CoreDefinitionsForLaurel.lean
+++ b/Strata/Languages/Laurel/CoreDefinitionsForLaurel.lean
@@ -25,6 +25,7 @@ def coreDefinitionsForLaurelDDM :=
 #strata
 program Laurel;
 
+datatype LaurelResolutionErrorPlaceholder {}
 datatype Float64IsNotSupportedYet {}
 
 // The types for these Map functions are incorrect.
diff --git a/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean b/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean
index 2a9287e605..3f0cc570cf 100644
--- a/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean
+++ b/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean
@@ -62,13 +62,11 @@ def collectStaticCallNames (expr : StmtExprMd) : List String :=
       | some eelse => collectStaticCallNames eelse
       | none => []
   | .Block stmts _ => stmts.flatMap (fun s => collectStaticCallNames s)
-  | .Assign targets v =>
-      targets.flatMap (fun t => collectStaticCallNames t) ++
+  | .Assign _targets v =>
+      -- Targets are Variables; Field targets can contain StmtExpr children,
+      -- but field-target assigns are eliminated before this pass runs,
+      -- so we only need to collect from the value.
       collectStaticCallNames v
-  | .LocalVariable _ _ initOption =>
-      match initOption with
-      | some init => collectStaticCallNames init
-      | none => []
   | .Return v =>
       match v with
       | some x => collectStaticCallNames x
@@ -85,7 +83,7 @@ def collectStaticCallNames (expr : StmtExprMd) : List String :=
       | some t => collectStaticCallNames t
       | none => []) ++
       collectStaticCallNames body
-  | .FieldSelect t _ => collectStaticCallNames t
+  | .Var (.Field t _) => collectStaticCallNames t
   | .PureFieldUpdate t _ v => collectStaticCallNames t ++ collectStaticCallNames v
   | .InstanceCall t _ args =>
       collectStaticCallNames t ++ args.flatMap (fun a => collectStaticCallNames a)
@@ -98,7 +96,11 @@ def collectStaticCallNames (expr : StmtExprMd) : List String :=
   | .Assigned v => collectStaticCallNames v
   | _ => []
 termination_by sizeOf expr
-decreasing_by all_goals (have := AstNode.sizeOf_val_lt ‹_›; term_by_mem)
+decreasing_by
+  all_goals simp_wf
+  all_goals (try have := AstNode.sizeOf_val_lt expr)
+  all_goals (try term_by_mem)
+  all_goals omega
 
 /--
 Build the procedure call graph, run Tarjan's SCC algorithm, and return each SCC
diff --git a/Strata/Languages/Laurel/EliminateHoles.lean b/Strata/Languages/Laurel/EliminateHoles.lean
index a10cacd9d0..ecf34a2669 100644
--- a/Strata/Languages/Laurel/EliminateHoles.lean
+++ b/Strata/Languages/Laurel/EliminateHoles.lean
@@ -52,7 +52,7 @@ private def mkHoleCall (holeType : HighTypeMd) : ElimHoleM StmtExprMd := do
     body := .Opaque [] none []
   }
   modify fun s => { s with generatedFunctions := s.generatedFunctions ++ [holeProc] }
-  return bare (.StaticCall holeName (inputs.map (fun p => bare (.Identifier p.name))))
+  return bare (.StaticCall holeName (inputs.map (fun p => bare (.Var (.Local p.name)))))
 
 /-- Replace a deterministic `.Hole` with a call to a fresh uninterpreted function.
     Non-hole nodes pass through unchanged; recursion is handled by `mapStmtExprM`. -/
diff --git a/Strata/Languages/Laurel/EliminateValueReturns.lean b/Strata/Languages/Laurel/EliminateValueReturns.lean
index b057c0d8c9..f465c6055c 100644
--- a/Strata/Languages/Laurel/EliminateValueReturns.lean
+++ b/Strata/Languages/Laurel/EliminateValueReturns.lean
@@ -27,7 +27,7 @@ private def eliminateValueReturnNode (outParam : Identifier) (stmt : StmtExprMd)
   match stmt.val with
   | .Return (some value) =>
     -- Synthesized nodes use default metadata since no diagnostics should be reported on them
-    let target : StmtExprMd := { val := .Identifier outParam, source := none }
+    let target : VariableMd := { val := .Local outParam, source := none }
     let assign : StmtExprMd := { val := .Assign [target] value, source := none }
     let ret : StmtExprMd := { val := .Return none, source := stmt.source }
     { val := .Block [assign, ret] none, source := none }
diff --git a/Strata/Languages/Laurel/FilterPrelude.lean b/Strata/Languages/Laurel/FilterPrelude.lean
index 569dde80ad..c4c2181c81 100644
--- a/Strata/Languages/Laurel/FilterPrelude.lean
+++ b/Strata/Languages/Laurel/FilterPrelude.lean
@@ -78,7 +78,7 @@ private partial def collectHighTypeNames (ty : HighTypeMd) : CollectM Unit := do
   | .Pure base => collectHighTypeNames base
   | .Intersection types => types.forM collectHighTypeNames
   | .TVoid | .TBool | .TInt | .TFloat64 | .TReal | .TString | .THeap
-  | .TBv _ | .Unknown => pure ()
+  | .TBv _ | .Unknown | .MultiValuedExpr _ => pure ()
 
 /-- Collect all referenced names (procedure calls, type references) from a StmtExpr tree. -/
 private partial def collectExprNames (expr : StmtExprMd) : CollectM Unit := do
@@ -92,16 +92,19 @@ private partial def collectExprNames (expr : StmtExprMd) : CollectM Unit := do
     collectExprNames cond; collectExprNames thenB
     elseB.forM collectExprNames
   | .Block stmts _ => stmts.forM collectExprNames
-  | .LocalVariable _ ty init =>
-    collectHighTypeNames ty
-    init.forM collectExprNames
   | .While cond invs dec body =>
     collectExprNames cond; invs.forM collectExprNames
     dec.forM collectExprNames
     collectExprNames body
   | .Assign targets value =>
-    collectExprNames value; targets.forM collectExprNames
-  | .FieldSelect target _ => collectExprNames target
+    collectExprNames value
+    for ⟨t, _⟩ in targets.attach do
+      match t.val with
+      | .Field target _ => collectExprNames target
+      | .Local _ => pure ()
+      | .Declare param => collectHighTypeNames param.type
+  | .Var (.Field target _) => collectExprNames target
+  | .Var (.Declare param) => collectHighTypeNames param.type
   | .PureFieldUpdate target _ newVal =>
     collectExprNames target; collectExprNames newVal
   | .PrimitiveOp _ args => args.forM collectExprNames
@@ -120,7 +123,7 @@ private partial def collectExprNames (expr : StmtExprMd) : CollectM Unit := do
   | .ReferenceEquals lhs rhs => collectExprNames lhs; collectExprNames rhs
   | .Hole _ ty => ty.forM collectHighTypeNames
   | .Exit _ | .LiteralInt _ | .LiteralBool _ | .LiteralString _ | .LiteralDecimal _
-  | .Identifier _ | .This | .Abstract | .All => pure ()
+  | .Var (.Local _) | .This | .Abstract | .All => pure ()
 
 /-- Collect names from a procedure body. -/
 private def collectBodyNames (body : Body) : CollectM Unit := do
@@ -177,7 +180,7 @@ private partial def collectInvokeOnTargets (expr : StmtExprMd)
   | .StaticCall callee args =>
     let rest ← args.flatMapM collectInvokeOnTargets
     return callee.text :: rest
-  | .Identifier _ | .LiteralInt _ | .LiteralBool _ | .LiteralString _
+  | .Var (.Local _) | .LiteralInt _ | .LiteralBool _ | .LiteralString _
   | .LiteralDecimal _ => return []
   | _ =>
     throw s!"FilterPrelude.collectInvokeOnTargets: unexpected node in invokeOn expression"
diff --git a/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean
index 5532883ef4..e8ced7af6f 100644
--- a/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean
+++ b/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean
@@ -62,6 +62,7 @@ partial def highTypeValToArg : HighType → Arg
     | [] => laurelOp "compositeType" #[ident "Unknown"]
     | t :: _ => highTypeToArg t
   | .Unknown => laurelOp "compositeType" #[ident "Unknown"]
+  | .MultiValuedExpr _ => laurelOp "compositeType" #[ident "Unknown"]
 
 end
 
@@ -80,6 +81,10 @@ private def operationName : Operation → String
 partial def stmtExprToArg (s : StmtExprMd) : Arg :=
   stmtExprValToArg s.val
 where
+  variableToArg : Variable → Arg
+    | .Local name => laurelOp "identifier" #[ident name.text]
+    | .Field target field => laurelOp "fieldAccess" #[stmtExprToArg target, ident field.text]
+    | .Declare param => laurelOp "identifier" #[ident param.name.text]
   stmtExprValToArg : StmtExpr → Arg
     | .LiteralBool b => laurelOp "literalBool" #[boolToArg b]
     | .LiteralInt n =>
@@ -90,23 +95,37 @@ where
     | .LiteralString s => laurelOp "string" #[.strlit sr s]
     | .Hole true _ => laurelOp "hole"
     | .Hole false _ => laurelOp "nondetHole"
-    | .Identifier name => laurelOp "identifier" #[ident name.text]
+    | .Var (.Local name) => laurelOp "identifier" #[ident name.text]
     | .Block stmts label =>
       let stmtArgs := stmts.map stmtExprToArg |>.toArray
       match label with
       | none => laurelOp "block" #[semicolonSep stmtArgs]
       | some l => laurelOp "labelledBlock" #[semicolonSep stmtArgs, ident l]
-    | .LocalVariable name ty init =>
-      let typeOpt := optionArg (some (laurelOp "typeAnnotation" #[highTypeToArg ty]))
-      let initOpt := optionArg (init.map fun e => laurelOp "initializer" #[stmtExprToArg e])
-      laurelOp "varDecl" #[ident name.text, typeOpt, initOpt]
+    | .Var (.Declare param) =>
+      let typeOpt := optionArg (some (laurelOp "typeAnnotation" #[highTypeToArg param.type]))
+      let initOpt := optionArg none
+      laurelOp "varDecl" #[ident param.name.text, typeOpt, initOpt]
+    | .Assign [⟨.Declare param, _⟩] value =>
+      let typeOpt := optionArg (some (laurelOp "typeAnnotation" #[highTypeToArg param.type]))
+      let initOpt := optionArg (some (laurelOp "initializer" #[stmtExprToArg value]))
+      laurelOp "varDecl" #[ident param.name.text, typeOpt, initOpt]
     | .Assign targets value =>
-      -- Grammar only supports single-target assign; use first target or placeholder
-      let targetArg := match targets with
-        | t :: _ => stmtExprToArg t
-        | [] => laurelOp "identifier" #[ident "_"]
-      laurelOp "assign" #[targetArg, stmtExprToArg value]
-    | .FieldSelect target field =>
+      if targets.length > 1 then
+        let targetArgs := targets.map fun t =>
+          match t.val with
+          | .Declare param => laurelOp "assignTargetDecl" #[ident param.name.text, highTypeToArg param.type]
+          | .Local name => laurelOp "assignTargetVar" #[ident name.text]
+          | .Field target _ =>
+            match target.val with
+            | .Var (.Local name) => laurelOp "assignTargetField" #[ident name.text, ident (match t.val with | .Field _ f => f.text | _ => "_")]
+            | _ => laurelOp "assignTargetVar" #[ident "_"]
+        laurelOp "multiAssign" #[commaSep targetArgs.toArray, stmtExprToArg value]
+      else
+        let targetArg := match targets with
+          | t :: _ => variableToArg t.val
+          | [] => laurelOp "identifier" #[ident "_"]
+        laurelOp "assign" #[targetArg, stmtExprToArg value]
+    | .Var (.Field target field) =>
       laurelOp "fieldAccess" #[stmtExprToArg target, ident field.text]
     | .StaticCall callee args =>
       let calleeArg := laurelOp "identifier" #[ident callee.text]
@@ -358,6 +377,12 @@ def formatTypeDefinition : TypeDefinition → Format
   | .Datatype ty => formatDatatypeDefinition ty
   | .Alias ta => "type " ++ format ta.name ++ " = " ++ formatHighType ta.target
 
+def formatVariable (v : Variable) : Format :=
+  formatArg (stmtExprToArg ⟨.Var v, none⟩)
+
+def formatVariableMd (v : VariableMd) : Format :=
+  formatArg (stmtExprToArg ⟨.Var v.val, v.source⟩)
+
 def formatConstant (c : Constant) : Format :=
   "const " ++ format c.name ++ ": " ++ formatHighType c.type ++
   match c.initializer with
@@ -375,6 +400,8 @@ instance : Std.ToFormat CompositeType where format := formatCompositeType
 instance : Std.ToFormat ConstrainedType where format := formatConstrainedType
 instance : Std.ToFormat DatatypeConstructor where format := formatDatatypeConstructor
 instance : Std.ToFormat DatatypeDefinition where format := formatDatatypeDefinition
+instance : Std.ToFormat Variable where format := formatVariable
+instance : Std.ToFormat VariableMd where format := formatVariableMd
 instance : Std.ToFormat Constant where format := formatConstant
 instance : Std.ToFormat TypeDefinition where format := formatTypeDefinition
 instance : Std.ToFormat Program where format := formatProgram
diff --git a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
index e3ea1f61c9..8d3dcdc460 100644
--- a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
+++ b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
@@ -82,7 +82,7 @@ def translateBool (arg : Arg) : TransM Bool := do
   | x => TransM.error s!"translateBool expects expression or operation, got {repr x}"
 
 instance : Inhabited Parameter where
-  default := { name := "" , type := { val := .Unknown, source := none } }
+  default := { name := "" , type := default }
 
 def mkHighTypeMd (t : HighType) (source : Option FileRange) : HighTypeMd := { val := t, source := source }
 def mkStmtExprMd (e : StmtExpr) (source : Option FileRange) : StmtExprMd := { val := e, source := source }
@@ -240,15 +240,42 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExprMd := do
           | _ => TransM.error s!"assignArg {repr assignArg} didn't match expected pattern for variable {name}"
         | .option _ none => pure none
         | _ => TransM.error s!"assignArg {repr assignArg} didn't match expected pattern for variable {name}"
-      return mkStmtExprMd (.LocalVariable name varType value) src
+      match value with
+      | some init => return mkStmtExprMd (.Assign [⟨.Declare ⟨name, varType⟩, src⟩] init) src
+      | none => return mkStmtExprMd (.Var (.Declare ⟨name, varType⟩)) src
     | q`Laurel.identifier, #[arg0] =>
       let name ← translateIdent arg0
-      return mkStmtExprMd (.Identifier name) src
+      return mkStmtExprMd (.Var (.Local name)) src
     | q`Laurel.parenthesis, #[arg0] => translateStmtExpr arg0
     | q`Laurel.assign, #[arg0, arg1] =>
       let target ← translateStmtExpr arg0
+      let targetVar : VariableMd ← match target.val with
+        | .Var v => pure ⟨v, target.source⟩
+        | _ => TransM.error s!"assign target must be a variable or field access"
       let value ← translateStmtExpr arg1
-      return mkStmtExprMd (.Assign [target] value) src
+      return mkStmtExprMd (.Assign [targetVar] value) src
+    | q`Laurel.multiAssign, #[targetsSeq, valueArg] =>
+      let targets ← match targetsSeq with
+        | .seq _ .comma args => args.toList.mapM fun targ => do
+          let tSrc ← getArgFileRange targ
+          let .op top := targ
+            | TransM.error s!"multiAssign target expects operation"
+          match top.name, top.args with
+          | q`Laurel.assignTargetDecl, #[nameArg, typeArg] =>
+            let name ← translateIdent nameArg
+            let ty ← translateHighType typeArg
+            pure (⟨.Declare ⟨name, ty⟩, tSrc⟩ : VariableMd)
+          | q`Laurel.assignTargetVar, #[nameArg] =>
+            let name ← translateIdent nameArg
+            pure (⟨.Local name, tSrc⟩ : VariableMd)
+          | q`Laurel.assignTargetField, #[objArg, fieldArg] =>
+            let obj ← translateIdent objArg
+            let field ← translateIdent fieldArg
+            pure (⟨.Field ⟨.Var (.Local obj), tSrc⟩ field, tSrc⟩ : VariableMd)
+          | _, _ => TransM.error s!"multiAssign: unexpected target {repr top.name}"
+        | _ => pure []
+      let value ← translateStmtExpr valueArg
+      return mkStmtExprMd (.Assign targets value) src
     | q`Laurel.new, #[nameArg] =>
       let name ← translateIdent nameArg
       return mkStmtExprMd (.New name) src
@@ -263,7 +290,7 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExprMd := do
     | q`Laurel.call, #[arg0, argsSeq] =>
       let callee ← translateStmtExpr arg0
       let calleeName := match callee.val with
-        | .Identifier name => name
+        | .Var (.Local name) => name
         | _ => ""
       let argsList ← match argsSeq with
         | .seq _ .comma args => args.toList.mapM translateStmtExpr
@@ -285,7 +312,7 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExprMd := do
       let obj ← translateStmtExpr objArg
       let field ← translateIdent fieldArg
       let fieldSrc ← getArgFileRange fieldArg
-      return mkStmtExprMd (.FieldSelect obj field) fieldSrc
+      return mkStmtExprMd (.Var (.Field obj field)) fieldSrc
     | q`Laurel.while, #[condArg, invSeqArg, bodyArg] =>
       let cond ← translateStmtExpr condArg
       let invariants ← match invSeqArg with
diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
index b36b1b54ea..69ebee1a5e 100644
--- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
+++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
@@ -9,7 +9,7 @@ module
 -- Laurel dialect definition, loaded from LaurelGrammar.st
 -- NOTE: Changes to LaurelGrammar.st are not automatically tracked by the build system.
 -- Update this file (e.g. this comment) to trigger a recompile after modifying LaurelGrammar.st.
--- Last grammar change: added modifiesWildcard for `modifies *` and opaque keyword
+-- Last grammar change: merged modifiesWildcard, opaque keyword, and multiAssign field access targets.
 public import Strata.DDM.Integration.Lean
 public meta import Strata.DDM.Integration.Lean
 
diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
index cc2cc46083..b81b0d8b11 100644
--- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
+++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
@@ -48,6 +48,16 @@ op parenthesis (inner: StmtExpr): StmtExpr => "(" inner ")";
 // Assignment
 op assign (target: StmtExpr, value: StmtExpr): StmtExpr => @[prec(10)] target " := " value;
 
+// Multi-target assignment: assign var x: int, y, var z: int := call()
+// Uses the 'assign' keyword to avoid ambiguity with other comma-separated constructs.
+category AssignTarget;
+op assignTargetDecl (name: Ident, targetType: LaurelType): AssignTarget => "var " name ": " targetType;
+op assignTargetVar (name: Ident): AssignTarget => name;
+op assignTargetField (obj: Ident, field: Ident): AssignTarget => obj "#" field;
+
+op multiAssign (targets: CommaSepBy AssignTarget, value: StmtExpr): StmtExpr
+  => @[prec(0)] "assign " targets " := " value:0;
+
 // Binary operators
 op add (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(60), leftassoc] lhs " + " rhs;
 op sub (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(60), leftassoc] lhs " - " rhs;
diff --git a/Strata/Languages/Laurel/HeapParameterization.lean b/Strata/Languages/Laurel/HeapParameterization.lean
index 02cf41f45b..240fceb44a 100644
--- a/Strata/Languages/Laurel/HeapParameterization.lean
+++ b/Strata/Languages/Laurel/HeapParameterization.lean
@@ -57,23 +57,21 @@ def collectExprMd (expr : StmtExprMd) : StateM AnalysisResult Unit := collectExp
 
 def collectExpr (expr : StmtExpr) : StateM AnalysisResult Unit := do
   match _: expr with
-  | .FieldSelect target _ =>
+  | .Var (.Field target _) =>
       modify fun s => { s with readsHeapDirectly := true }; collectExprMd target
   | .InstanceCall target _ args => collectExprMd target; for a in args do collectExprMd a
   | .StaticCall callee args => modify fun s => { s with callees := callee :: s.callees }; for a in args do collectExprMd a
   | .IfThenElse c t e => collectExprMd c; collectExprMd t; if let some x := e then collectExprMd x
   | .Block stmts _ => for s in stmts do collectExprMd s
-  | .LocalVariable _ _ i => if let some x := i then collectExprMd x
   | .While c invs d b => collectExprMd c; collectExprMd b; for inv in invs do collectExprMd inv; if let some x := d then collectExprMd x
   | .Return v => if let some x := v then collectExprMd x
   | .Assign assignTargets v =>
       -- Check if any target is a field assignment (heap write)
       for ⟨assignTarget, _⟩ in assignTargets.attach do
         match assignTarget.val with
-        | .FieldSelect _ _ =>
+        | .Field _ _ =>
             modify fun s => { s with writesHeapDirectly := true }
-        | _ => pure ()
-        collectExprMd assignTarget
+        | .Local _ | .Declare _ => pure ()
       collectExprMd v
   | .PureFieldUpdate t _ v => collectExprMd t; collectExprMd v
   | .PrimitiveOp _ args => for a in args do collectExprMd a
@@ -98,9 +96,7 @@ def analyzeProc (proc : Procedure) : AnalysisResult :=
   let bodyResult := match proc.body with
     | .Transparent b => (collectExprMd b).run {} |>.2
     | .Opaque postconds impl modif =>
-        -- A non-empty modifies clause implies the procedure reads and writes the heap;
-        -- no need to inspect the body further in that case.
-        if !modif.isEmpty then
+        if impl.isNone && !modif.isEmpty then
           { readsHeapDirectly := true, writesHeapDirectly := true, callees := [] }
         else
           let r1 := postconds.foldl (fun (acc : AnalysisResult) (pc : Condition) =>
@@ -237,6 +233,7 @@ def freshVarName : TransformM Identifier := do
 
 /-- Helper to wrap a StmtExpr into StmtExprMd with empty metadata -/
 private def mkMd (e : StmtExpr) : StmtExprMd := { val := e, source := none }
+private def mkVarMd (v : Variable) : VariableMd := { val := v, source := none }
 
 /--
 Resolve the owning composite type name for a field access by computing the target expression's type.
@@ -245,7 +242,7 @@ Returns the qualified field name "DeclaringType.fieldName".
 def resolveQualifiedFieldName (model: SemanticModel) (fieldName : Identifier) : Option String :=
   match model.get fieldName with
     | .field owner _ => owner.text ++ "." ++ fieldName.text
-    | .unresolved => none
+    | .unresolved _ => none
     | _ => dbg_trace s!"BUG: resolveQualifiedFieldName {fieldName} did resolved to something other than a field"; none
 
 /--
@@ -260,12 +257,12 @@ where
   recurse (exprMd : StmtExprMd) (valueUsed : Bool := true) : TransformM StmtExprMd := do
     let ⟨expr, source⟩ := exprMd
     match _h : expr with
-    | .FieldSelect selectTarget fieldName => do
+    | .Var (.Field selectTarget fieldName) => do
         let some qualifiedName := resolveQualifiedFieldName model fieldName
           | return ⟨ .Hole, source ⟩
 
         let valTy := (model.get fieldName).getType
-        let readExpr := ⟨ .StaticCall "readField" [mkMd (.Identifier heapVar), selectTarget, mkMd (.StaticCall qualifiedName [])], source ⟩
+        let readExpr := ⟨ .StaticCall "readField" [mkMd (.Var (.Local heapVar)), selectTarget, mkMd (.StaticCall qualifiedName [])], source ⟩
         -- Unwrap Box: apply the appropriate destructor
         recordBoxConstructor model valTy.val
         return mkMd <| .StaticCall (boxDestructorName model valTy.val) [readExpr]
@@ -276,15 +273,22 @@ where
         if calleeWritesHeap then
           if valueUsed then
             let freshVar ← freshVarName
-            let varDecl := mkMd (.LocalVariable freshVar (computeExprType model exprMd) none)
             let callWithHeap := ⟨ .Assign
-              [mkMd (.Identifier heapVar), mkMd (.Identifier freshVar)]
-              (⟨ .StaticCall callee (mkMd (.Identifier heapVar) :: args'), source ⟩), source ⟩
-            return ⟨ .Block [varDecl, callWithHeap, mkMd (.Identifier freshVar)] none, source ⟩
+              [mkVarMd (.Local heapVar), mkVarMd (.Declare ⟨freshVar, computeExprType model exprMd⟩)]
+              (⟨ .StaticCall callee (mkMd (.Var (.Local heapVar)) :: args'), source ⟩), source ⟩
+            return ⟨ .Block [callWithHeap, mkMd (.Var (.Local freshVar))] none, source ⟩
           else
-            return ⟨ .Assign [mkMd (.Identifier heapVar)] (⟨ .StaticCall callee (mkMd (.Identifier heapVar) :: args'), source ⟩), source ⟩
+            -- Generate throwaway Declare targets for any non-heap outputs
+            let procOutputs := match model.get callee with
+              | .staticProcedure proc => proc.outputs
+              | .instanceProcedure _ proc => proc.outputs
+              | _ => []
+            let extraTargets ← procOutputs.mapM fun out => do
+              pure (mkVarMd (.Declare ⟨← freshVarName, out.type⟩))
+            let allTargets := mkVarMd (.Local heapVar) :: extraTargets
+            return ⟨ .Assign allTargets (⟨ .StaticCall callee (mkMd (.Var (.Local heapVar)) :: args'), source ⟩), source ⟩
         else if calleeReadsHeap then
-          return ⟨ .StaticCall callee (mkMd (.Identifier heapVar) :: args'), source ⟩
+          return ⟨ .StaticCall callee (mkMd (.Var (.Local heapVar)) :: args'), source ⟩
         else
           return ⟨ .StaticCall callee args', source ⟩
     | .InstanceCall callTarget callee args =>
@@ -307,9 +311,6 @@ where
           termination_by sizeOf remaining
         let stmts' ← processStmts 0 stmts
         return ⟨ .Block stmts' label, source ⟩
-    | .LocalVariable n ty i =>
-        let i' ← match i with | some x => some <$> recurse x | none => pure none
-        return ⟨ .LocalVariable n ty i', source ⟩
     | .While c invs d b =>
         let invs' ← invs.mapM (recurse ·)
         return ⟨ .While (← recurse c) invs' d (← recurse b false), source ⟩
@@ -317,31 +318,61 @@ where
         let v' ← match v with | some x => some <$> recurse x | none => pure none
         return ⟨ .Return v', source ⟩
     | .Assign targets v =>
-        match targets with
-        | [⟨.FieldSelect target fieldName, _⟩] =>
-            let some qualifiedName := resolveQualifiedFieldName model fieldName
-              | return ⟨ .Hole, source ⟩
-            let valTy := (model.get fieldName).getType
-            let target' ← recurse target
-            let v' ← recurse v
-            -- Wrap value in Box constructor
-            recordBoxConstructor model valTy.val
-            let boxedVal := mkMd <| .StaticCall (boxConstructorName model valTy.val) [v']
-            let heapAssign := ⟨ .Assign [mkMd (.Identifier heapVar)]
-              (mkMd (.StaticCall "updateField" [mkMd (.Identifier heapVar), target', mkMd (.StaticCall qualifiedName []), boxedVal])), source ⟩
-            if valueUsed then
-              return ⟨ .Block [heapAssign, v'] none, source ⟩
-            else
-              return heapAssign
-        | [fieldSelectMd] =>
-          let tgt' ← recurse fieldSelectMd
-          return ⟨ .Assign [tgt'] (← recurse v), source ⟩
-        | [] =>
-            return ⟨ .Assign [] (← recurse v), source ⟩
-        | tgt :: rest =>
-            let tgt' ← recurse tgt
-            let targets' ← rest.mapM (recurse ·)
-            return ⟨ .Assign (tgt' :: targets') (← recurse v), source ⟩
+
+      let processFieldAssignments :
+        TransformM (List (AstNode Variable) × List (AstNode StmtExpr)) :=
+        targets.attach.foldlM (init := ([], [])) fun (accTargets, accStmts) ⟨t, _⟩ =>
+          match _htv : t.val with
+          | .Field target fieldName => do
+              let some qualifiedName := resolveQualifiedFieldName model fieldName
+                | return (accTargets ++ [t], accStmts)
+              let valTy := (model.get fieldName).getType
+              recordBoxConstructor model valTy.val
+              let freshVar ← freshVarName
+              let target' ← recurse target
+              let boxedVal := mkMd <| .StaticCall (boxConstructorName model valTy.val) [mkMd (.Var (.Local freshVar))]
+              let updateStmt : StmtExprMd := ⟨ .Assign [mkVarMd (.Local heapVar)]
+                (mkMd (.StaticCall "updateField" [mkMd (.Var (.Local heapVar)), target', mkMd (.StaticCall qualifiedName []), boxedVal])), source ⟩
+              return (accTargets ++ [mkVarMd (.Declare ⟨freshVar, valTy⟩)], accStmts ++ [updateStmt])
+          | _ => return (accTargets ++ [t], accStmts)
+
+      let (v', addedHeap) <- match _hv : v.val with
+        | .StaticCall callee args => do
+          let args' <- args.mapM recurse
+          let calleeWritesHeap ← writesHeap callee
+          let calleeReadsHeap ← readsHeap callee
+          if calleeWritesHeap then
+            pure (⟨ .StaticCall callee (mkMd (.Var (.Local heapVar)) :: args'), v.source ⟩, true)
+          else if calleeReadsHeap then
+            pure (⟨ .StaticCall callee (mkMd (.Var (.Local heapVar)) :: args'), v.source ⟩, false)
+          else
+            pure (⟨ .StaticCall callee args', v.source ⟩, false)
+        | .InstanceCall callTarget _callee args => do
+          let _callTarget' ← recurse callTarget
+          let _args' <- args.mapM recurse
+          pure (v, false)
+        | _ =>
+          pure (<- recurse v, false)
+
+      let (processedTargets, updateStatements) <- processFieldAssignments
+      let allTargets := if addedHeap
+        then ⟨ Variable.Local heapVar, v.source ⟩ :: processedTargets
+        else processedTargets
+      let newAssign: AstNode StmtExpr := ⟨ StmtExpr.Assign allTargets v', source ⟩
+
+      let declareToLocal(var: Variable): Variable := match var with
+        | .Declare param => Variable.Local param.name
+        | x => x
+
+      let suffixes: List (AstNode StmtExpr) := if valueUsed && targets.length == 1
+        then updateStatements ++ [⟨ StmtExpr.Var $ declareToLocal $ if addedHeap then allTargets[1]!.val else allTargets[0]!.val, source⟩]
+        else updateStatements
+
+      if suffixes.length > 0 then
+        return ⟨ StmtExpr.Block (newAssign :: suffixes) none, source ⟩
+      else
+        return newAssign
+
     | .PureFieldUpdate t f v => return ⟨ .PureFieldUpdate (← recurse t) f (← recurse v), source ⟩
     | .PrimitiveOp op args =>
       let args' ← args.mapM (recurse ·)
@@ -385,6 +416,57 @@ where
     | .ContractOf ty f => return ⟨ .ContractOf ty (← recurse f), source ⟩
     | _ => return exprMd
     termination_by sizeOf exprMd
+    decreasing_by
+      all_goals simp_wf
+      all_goals (try have := AstNode.sizeOf_val_lt exprMd)
+      all_goals (try have := AstNode.sizeOf_val_lt v)
+      all_goals (try term_by_mem)
+      all_goals (try omega)
+      all_goals (try (cases exprMd; simp_all; omega))
+      -- For sub-expressions of StaticCall/InstanceCall inside Assign value:
+      all_goals (try (
+        have : sizeOf args < sizeOf v := by
+          have h1 := AstNode.sizeOf_val_lt v
+          rw [_hv] at h1; simp at h1; omega
+        term_by_mem))
+      -- For target inside Field in single-target case and multi-target Field recursion:
+      all_goals (try (
+        have := AstNode.sizeOf_val_lt targetHead
+        have : sizeOf target < sizeOf targetHead.val := by
+          cases targetHead with | mk val _ _ =>
+            simp only []
+            subst_vars
+            omega
+        omega))
+      -- For field inner expressions in attach-based mapM:
+      all_goals (try (
+        have := List.sizeOf_lt_of_mem ‹_›
+        have := AstNode.sizeOf_val_lt t
+        have : sizeOf t.val = sizeOf (Variable.Field target fieldName) := by exact congrArg sizeOf _htv
+        omega))
+      -- For field inner expressions in attach-based foldlM:
+      all_goals (try (
+        have := List.sizeOf_lt_of_mem ‹_›
+        have := AstNode.sizeOf_val_lt t
+        have : sizeOf t.val = sizeOf (Variable.Field target fieldName) := by exact congrArg sizeOf _htv
+        simp_all
+        omega))
+      -- For callTarget/args inside InstanceCall/StaticCall in value:
+      all_goals (try (
+        have : sizeOf callTarget < sizeOf v := by
+          have h1 := AstNode.sizeOf_val_lt v
+          rw [_hv] at h1; simp at h1; omega
+        omega))
+      all_goals (try (
+        have : sizeOf args < sizeOf v := by
+          have h1 := AstNode.sizeOf_val_lt v
+          rw [_hv] at h1; simp at h1; omega
+        term_by_mem))
+      -- Remaining goals
+      all_goals (
+        cases exprMd with | mk val src mmd =>
+        simp_all
+        omega)
 
 def heapTransformProcedure (model: SemanticModel) (proc : Procedure) : TransformM Procedure := do
   let heapName : Identifier := "$heap"
@@ -408,7 +490,7 @@ def heapTransformProcedure (model: SemanticModel) (proc : Procedure) : Transform
     let body' ← match proc.body with
       | .Transparent bodyExpr =>
           -- First assign $heap_in to $heap, then transform body using $heap
-          let assignHeap := mkMd (.Assign [mkMd (.Identifier heapName)] (mkMd (.Identifier heapInName)))
+          let assignHeap := mkMd (.Assign [mkVarMd (.Local heapName)] (mkMd (.Var (.Local heapInName))))
           let bodyExpr' ← heapTransformExpr heapName model bodyExpr bodyValueIsUsed
           pure (.Transparent (mkMd (.Block [assignHeap, bodyExpr'] none)))
       | .Opaque postconds impl modif =>
@@ -416,7 +498,7 @@ def heapTransformProcedure (model: SemanticModel) (proc : Procedure) : Transform
           let postconds' ← postconds.mapM (·.mapM (heapTransformExpr heapName model))
           let impl' ← match impl with
             | some implExpr =>
-                let assignHeap := mkMd (.Assign [mkMd (.Identifier heapName)] (mkMd (.Identifier heapInName)))
+                let assignHeap := mkMd (.Assign [mkVarMd (.Local heapName)] (mkMd (.Var (.Local heapInName))))
                 let implExpr' ← heapTransformExpr heapName model implExpr bodyValueIsUsed
                 pure (some (mkMd (.Block [assignHeap, implExpr'] none)))
             | none => pure none
diff --git a/Strata/Languages/Laurel/InferHoleTypes.lean b/Strata/Languages/Laurel/InferHoleTypes.lean
index 76244e3c7b..878c19b210 100644
--- a/Strata/Languages/Laurel/InferHoleTypes.lean
+++ b/Strata/Languages/Laurel/InferHoleTypes.lean
@@ -29,15 +29,16 @@ namespace Laurel
 
 public section
 
+
 private def bareType (v : HighType) : HighTypeMd := ⟨v, none⟩
 private def voidType : HighTypeMd := bareType .TVoid
 private def defaultHoleType : HighTypeMd := bareType .Unknown
 
 /-- Compute the expected type for an argument of a comparison operator
     by looking at the first non-hole sibling. -/
-private def inferComparisonArgType (model : SemanticModel) (args : List StmtExprMd) : HighTypeMd :=
+private def inferComparisonArgType (model : SemanticModel) (args : List StmtExprMd) (source: Option FileRange) : HighTypeMd :=
   args.findSome? (fun a => match a.val with | .Hole _ _ => none | _ => some (computeExprType model a))
-    |>.getD defaultHoleType
+    |>.getD ⟨ .TInt, source ⟩ -- use Int as a default type for comparisons where both operands are holes
 
 /-- Get the expected type for each argument of a call from the callee's parameter list. -/
 private def calleeParamTypes (model : SemanticModel) (callee : Identifier) : Option (List HighTypeMd) :=
@@ -57,6 +58,7 @@ structure InferHoleState where
   model : SemanticModel
   currentOutputType : HighTypeMd := ⟨.Unknown, none⟩
   statistics : Statistics := {}
+  diagnostics : List DiagnosticModel := []
 
 private abbrev InferHoleM := StateM InferHoleState
 
@@ -68,7 +70,7 @@ private def inferArgsTyped (args : List StmtExprMd) (types : List HighTypeMd) :
   let mut result : List StmtExprMd := []
   let mut i := 0
   for a in args do
-    result := result ++ [← inferExpr a (types.getD i defaultHoleType)]
+    result := result ++ [← inferExpr a types[i]!]
     i := i + 1
   return result
 
@@ -78,7 +80,7 @@ private def inferBlockStmts (stmts : List StmtExprMd) (expectedType : HighTypeMd
   match stmts with
   | [] => return []
   | [last] => return [← inferExpr last expectedType]
-  | head :: tail => return (← inferExpr head voidType) :: (← inferBlockStmts tail expectedType)
+  | head :: tail => return (← inferExpr head ⟨ .TVoid, head.source⟩ ) :: (← inferBlockStmts tail expectedType)
 
 /-- Annotate every `.Hole` in an expression with its contextual type.
     Statement-position nodes should be called with `expectedType = voidType`,
@@ -90,14 +92,17 @@ private def inferExpr (expr : StmtExprMd) (expectedType : HighTypeMd) : InferHol
   match val with
   | .Hole det _ =>
       if expectedType.val == .Unknown then
-        modify fun s => { s with statistics := s.statistics.increment s!"{InferHoleTypesStats.holesLeftUnknown}" }
+        modify fun s => { s with
+          statistics := s.statistics.increment s!"{InferHoleTypesStats.holesLeftUnknown}"
+          diagnostics := s.diagnostics ++ [diagnosticFromSource source "could not infer type"]
+        }
         return expr
       else
         modify fun s => { s with statistics := s.statistics.increment s!"{InferHoleTypesStats.holesAnnotated}" }
         return ⟨.Hole det (some expectedType), source⟩
   | .PrimitiveOp op args =>
       let argType := match op with
-        | .Eq | .Neq | .Lt | .Leq | .Gt | .Geq => inferComparisonArgType model args
+        | .Eq | .Neq | .Lt | .Leq | .Gt | .Geq => inferComparisonArgType model args source
         | _ =>
           -- Use computeExprType on the whole expression to get the result type,
           -- which equals the argument type for arithmetic/logic/string ops.
@@ -114,7 +119,7 @@ private def inferExpr (expr : StmtExprMd) (expectedType : HighTypeMd) : InferHol
         | none => inferArgs args defaultHoleType
       return ⟨.StaticCall callee args', source⟩
   | .InstanceCall target callee args =>
-      return ⟨.InstanceCall (← inferExpr target defaultHoleType) callee (← inferArgs args defaultHoleType), source⟩
+      return ⟨.InstanceCall (← inferExpr target ⟨ .Unknown, source ⟩) callee (← inferArgs args ⟨ .Unknown, source ⟩), source⟩
   | .ReferenceEquals lhs rhs =>
       return ⟨.ReferenceEquals (← inferExpr lhs defaultHoleType) (← inferExpr rhs defaultHoleType), source⟩
   | .IfThenElse cond th el =>
@@ -126,16 +131,15 @@ private def inferExpr (expr : StmtExprMd) (expectedType : HighTypeMd) : InferHol
       return ⟨.Block (← inferBlockStmts stmts expectedType) label, source⟩
   | .Assign targets value =>
       let targetType := match targets with
-        | target :: _ => computeExprType model target
+        | target :: _ => match target.val with
+          | .Local name => computeExprType model ⟨.Var (.Local name), target.source⟩
+          | .Field _ fieldName => computeExprType model ⟨.Var (.Field ⟨.Hole, none⟩ fieldName), target.source⟩
+          | .Declare param => param.type
         | _ => defaultHoleType
       return ⟨.Assign targets (← inferExpr value targetType), source⟩
-  | .LocalVariable name ty init =>
-      match init with
-      | some initExpr => return ⟨.LocalVariable name ty (some (← inferExpr initExpr ty)), source⟩
-      | none => return expr
   | .While cond invs dec body =>
       let dec' ← match dec with
-        | some d => pure (some (← inferExpr d (bareType .TInt)))
+        | some d => pure (some (← inferExpr d (⟨ .TInt, source ⟩)))
         | none => pure none
       return ⟨.While (← inferExpr cond (bareType .TBool)) (← invs.mapM (inferExpr · (bareType .TBool))) dec' (← inferExpr body voidType), source⟩
   | .Assert ⟨condExpr, summary⟩ =>
@@ -150,7 +154,7 @@ private def inferExpr (expr : StmtExprMd) (expectedType : HighTypeMd) : InferHol
   | .ContractOf ty f => return ⟨.ContractOf ty (← inferExpr f defaultHoleType), source⟩
   | .Quantifier mode p trigger b =>
       let trigger' ← match trigger with
-        | some t => pure (some (← inferExpr t defaultHoleType))
+        | some t => pure (some (← inferExpr t ⟨ .Unknown, source ⟩))
         | none => pure none
       return ⟨.Quantifier mode p trigger' (← inferExpr b (bareType .TBool)), source⟩
   | _ => return expr
@@ -159,7 +163,7 @@ end
 private def inferProcedure (proc : Procedure) : InferHoleM Procedure := do
   let outputType := match proc.outputs with
     | [single] => single.type
-    | _ => { val := .Unknown, source := none }
+    | _ => { val := .Unknown, source := proc.name.source }
   modify fun s => { s with currentOutputType := outputType }
   match proc.body with
   | .Transparent bodyExpr => return { proc with body := .Transparent (← inferExpr bodyExpr outputType) }
@@ -170,10 +174,10 @@ private def inferProcedure (proc : Procedure) : InferHoleM Procedure := do
 /--
 Annotate every `.Hole` in the program with a type inferred from context.
 -/
-def inferHoleTypes (model : SemanticModel) (program : Program) : Program × Statistics :=
-  let initState : InferHoleState := { model := model }
+def inferHoleTypes (model : SemanticModel) (program : Program) : Program × List DiagnosticModel × Statistics :=
+  let initState : InferHoleState := { model := model, currentOutputType := { val := .Unknown, source := none }}
   let (procs, finalState) := (program.staticProcedures.mapM inferProcedure).run initState
-  ({ program with staticProcedures := procs }, finalState.statistics)
+  ({ program with staticProcedures := procs }, finalState.diagnostics, finalState.statistics)
 
 end -- public section
 end Laurel
diff --git a/Strata/Languages/Laurel/Laurel.lean b/Strata/Languages/Laurel/Laurel.lean
index a8d6aa9860..62ece47108 100644
--- a/Strata/Languages/Laurel/Laurel.lean
+++ b/Strata/Languages/Laurel/Laurel.lean
@@ -162,6 +162,9 @@ inductive HighType : Type where
   Any type can be assigned to unknown and unknown can be assigned to any type.
   The unknown type can not be represented in Core so its occurence will abort compilation before evaluating Core -/
   | Unknown
+  /-- A multi-valued expression type, returned by procedure calls with multiple outputs.
+  Used by the resolution pass to validate that the LHS of an assignment has the correct number of targets. -/
+  | MultiValuedExpr (types : List (AstNode HighType))
   deriving Repr
 
 /-- Whether a quantifier is universal or existential. -/
@@ -235,6 +238,17 @@ inductive Body where
   /-- An external body for procedures that are not translated to Core (e.g., built-in primitives). -/
   | External
 
+/--
+A variable reference or declaration: a local variable, a field access on an expression, or a local variable declaration.
+-/
+inductive Variable : Type where
+  /-- A local variable reference by name. -/
+  | Local (name : Identifier)
+  /-- Read a field from a target expression. Combined with `Assign` for field writes. -/
+  | Field (target : AstNode StmtExpr) (fieldName : Identifier)
+  /-- A local variable declaration with a name and type. -/
+  | Declare (parameter : Parameter)
+
 /--
 The unified statement-expression type for Laurel programs.
 
@@ -248,8 +262,6 @@ inductive StmtExpr : Type where
   | IfThenElse (cond : AstNode StmtExpr) (thenBranch : AstNode StmtExpr) (elseBranch : Option (AstNode StmtExpr))
   /-- A sequence of statements with an optional label for `Exit`. -/
   | Block (statements : List (AstNode StmtExpr)) (label : Option String)
-  /-- A local variable declaration with a type and optional initializer. The initializer must be set if this `StmtExpr` is pure. -/
-  | LocalVariable (name : Identifier) (type : AstNode HighType) (initializer : Option (AstNode StmtExpr))
   /-- A while loop with a condition, invariants, optional termination measure, and body. Only allowed in impure contexts. -/
   | While (cond : AstNode StmtExpr) (invariants : List (AstNode StmtExpr))
     (decreases : Option (AstNode StmtExpr))
@@ -266,12 +278,10 @@ inductive StmtExpr : Type where
   | LiteralString (value : String)
   /-- A decimal literal. -/
   | LiteralDecimal (value : Decimal)
-  /-- A variable reference by name. -/
-  | Identifier (name : Identifier)
-  /-- Assignment to one or more targets. Multiple targets are only allowed when the value is a `StaticCall` to a procedure with multiple outputs. -/
-  | Assign (targets : List (AstNode StmtExpr)) (value : AstNode StmtExpr)
-  /-- Read a field from a target expression. Combined with `Assign` for field writes. -/
-  | FieldSelect (target : AstNode StmtExpr) (fieldName : Identifier)
+  /-- A variable reference. -/
+  | Var (var : Variable)
+  /-- Assignment to one or more targets. Multiple targets are only supported with identifier targets and a call as the RHS. -/
+  | Assign (targets : List (AstNode Variable)) (value : AstNode StmtExpr)
   /-- Update a field on a pure (value) type, producing a new value. -/
   | PureFieldUpdate (target : AstNode StmtExpr) (fieldName : Identifier) (newValue : AstNode StmtExpr)
   /-- Call a static procedure by name with the given arguments. -/
@@ -280,7 +290,7 @@ inductive StmtExpr : Type where
   | PrimitiveOp (operator : Operation) (arguments : List (AstNode StmtExpr))
   /-- Create new object (`new`). -/
   | New (ref : Identifier)
-  /-- Identifier to the current object (`this`/`self`). -/
+  /-- Reference to the current object (`this`/`self`). -/
   | This
   /-- Reference equality test between two expressions. -/
   | ReferenceEquals (lhs : AstNode StmtExpr) (rhs : AstNode StmtExpr)
@@ -324,6 +334,7 @@ end
 
 @[expose] abbrev HighTypeMd := AstNode HighType
 @[expose] abbrev StmtExprMd := AstNode StmtExpr
+@[expose] abbrev VariableMd := AstNode Variable
 
 theorem AstNode.sizeOf_val_lt {t : Type} [SizeOf t] (e : AstNode t) : sizeOf e.val < sizeOf e := by
   cases e; grind
@@ -361,12 +372,24 @@ def diagnosticFromSource (source : Option FileRange) (msg : String) (type : Diag
 instance : Inhabited StmtExpr where
   default := .Hole
 
+instance : Inhabited (AstNode Variable) where
+  default := { val := .Local default, source := none }
+
 instance : Inhabited HighTypeMd where
-  default := { val := HighType.Unknown, source := none }
+  default := { val := HighType.Unknown, source := some { file := .file "HighTypeMd default", range := default} }
 
 instance : Inhabited StmtExprMd where
   default := { val := default, source := none }
 
+instance : Std.ToFormat Variable where
+  format
+    | .Local name => Std.format name.text
+    | .Field _target fieldName => f!"<expr>.{fieldName.text}"
+    | .Declare param => f!"var {param.name.text}"
+
+instance : Std.ToFormat (AstNode Variable) where
+  format v := Std.format v.val
+
 def highEq (a : HighTypeMd) (b : HighTypeMd) : Bool := match _a: a.val, _b: b.val with
   | HighType.TVoid, HighType.TVoid => true
   | HighType.TBool, HighType.TBool => true
@@ -386,12 +409,15 @@ def highEq (a : HighTypeMd) (b : HighTypeMd) : Bool := match _a: a.val, _b: b.va
   | HighType.Intersection ts1, HighType.Intersection ts2 =>
       ts1.length == ts2.length && (ts1.attach.zip ts2 |>.all (fun (t1, t2) => highEq t1.1 t2))
   | HighType.Unknown, HighType.Unknown => true
+  | HighType.MultiValuedExpr ts1, HighType.MultiValuedExpr ts2 =>
+      ts1.length == ts2.length && (ts1.attach.zip ts2 |>.all (fun (t1, t2) => highEq t1.1 t2))
   | _, _ => false
   termination_by (SizeOf.sizeOf a)
   decreasing_by
     all_goals (cases a; cases b; try term_by_mem)
     . cases a1; term_by_mem
     . cases t1; term_by_mem
+    . cases t1; term_by_mem
 
 instance : BEq HighTypeMd where
   beq := highEq
diff --git a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
index 3c5ac9c80d..1a08f32bef 100644
--- a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
+++ b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
@@ -113,8 +113,8 @@ private def laurelPipeline : Array LaurelPass := #[
       (p', diags, {}) },
   { name := "InferHoleTypes"
     run := fun p m =>
-      let (p', stats) := inferHoleTypes m p
-      (p', [], stats) },
+      let (p', diags, stats) := inferHoleTypes m p
+      (p', diags, stats) },
   { name := "EliminateHoles"
     run := fun p _m =>
       let (p', stats) := eliminateHoles p
@@ -147,7 +147,8 @@ program state after each named Laurel pass is written to
 private def runLaurelPasses (options : LaurelTranslateOptions) (program : Program)
     : PipelineM (Program × SemanticModel × List DiagnosticModel × Statistics) := do
   let program := { program with
-    staticProcedures := coreDefinitionsForLaurel.staticProcedures ++ program.staticProcedures
+    staticProcedures := coreDefinitionsForLaurel.staticProcedures ++ program.staticProcedures,
+    types := coreDefinitionsForLaurel.types ++ program.types
   }
 
   -- Step 0: the input program before any passes
@@ -196,12 +197,15 @@ def translateWithLaurel (options : LaurelTranslateOptions) (program : Program)
   runPipelineM options.keepAllFilesPrefix do
     let (program, model, passDiags, stats) ← runLaurelPasses options program
     let ordered := orderProgram program
+    if ! passDiags.isEmpty then
+      return (none, passDiags, program, stats)
+
     let initState : TranslateState := { model := model, overflowChecks := options.overflowChecks }
     let (coreProgramOption, translateState) :=
       runTranslateM initState (translateLaurelToCore options program ordered)
     if let some coreProgram := coreProgramOption then
       emit "CoreProgram" "core.st" coreProgram
-    let allDiagnostics := passDiags ++ translateState.diagnostics
+    let mut allDiagnostics := passDiags ++ translateState.diagnostics
     let coreProgramOption :=
       if translateState.coreProgramHasSuperfluousErrors then none else coreProgramOption
     return (coreProgramOption, allDiagnostics, program, stats)
diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean
index b24c41ea23..a7b75bde3e 100644
--- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean
+++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean
@@ -76,7 +76,7 @@ def emitDiagnostic (d : DiagnosticModel) : TranslateM Unit :=
 private def throwTypeDiagnostic (ty : HighTypeMd) (msg : String) : TranslateM LMonoTy := do
   emitDiagnostic (diagnosticFromSource ty.source msg)
   modify fun s => { s with coreProgramHasSuperfluousErrors := true }
-  return .tcons "Error" []
+  return .tcons s!"LaurelResolutionErrorPlaceholder" []
 
 /-
 Translate Laurel HighType to Core Type
@@ -103,8 +103,9 @@ def translateType (ty : HighTypeMd) : TranslateM LMonoTy := do
       return .tcons "Composite" []
   | .TCore s => return .tcons s []
   | .TReal => return LMonoTy.real
-  | .Unknown => throwTypeDiagnostic ty "could not infer type"
+  | .Unknown => throwTypeDiagnostic ty "bug in Laurel: unknown type encountered while translating to Core"
   | _ => throwTypeDiagnostic ty "cannot translate type to Core: not supported yet"
+
 termination_by ty.val
 decreasing_by all_goals (first | (cases elementType; term_by_mem) | (cases keyType; term_by_mem) | (cases valueType; term_by_mem))
 
@@ -162,7 +163,7 @@ def translateExpr (expr : StmtExprMd)
   | .LiteralInt i => return .const () (.intConst i)
   | .LiteralString s => return .const () (.strConst s)
   | .LiteralDecimal d => return .const () (.realConst (Strata.Decimal.toRat d))
-  | .Identifier name =>
+  | .Var (.Local name) =>
       -- First check if this name is bound by an enclosing quantifier
       match boundVars.findIdx? (· == name) with
       | some idx =>
@@ -174,6 +175,8 @@ def translateExpr (expr : StmtExprMd)
             return .op () ⟨f.name.text, ()⟩ none
         | astNode =>
             return .fvar () ⟨name.text, ()⟩ (some (← translateType astNode.getType))
+  | .Var (.Declare _) =>
+      throwExprDiagnostic $ md.toDiagnostic "variable declaration in expression context should have been lowered" DiagnosticType.StrataBug
   | .PrimitiveOp op [e] =>
     match op with
     | .Not =>
@@ -272,27 +275,26 @@ def translateExpr (expr : StmtExprMd)
   | .Block (⟨ .Assume _, innerSrc⟩ :: rest) label =>
     _ ← disallowed innerSrc "assumes are not YET supported in functions or contracts"
     translateExpr { val := StmtExpr.Block rest label, source := innerSrc } boundVars isPureContext
-  | .Block (⟨ .LocalVariable name ty (some initializer), innerSrc⟩ :: rest) label => do
-      let valueExpr ← translateExpr  initializer boundVars isPureContext
+  | .Block (⟨ .Assign [⟨ .Declare ⟨name, ty ⟩, _source⟩] initializer, innerSrc⟩ :: rest) label => do
+      let valueExpr ← translateExpr initializer boundVars isPureContext
       let bodyExpr ← translateExpr { val := StmtExpr.Block rest label, source := innerSrc } (name :: boundVars) isPureContext
       let coreMonoType ← translateType ty
       return .app () (.abs () name.text (some coreMonoType) bodyExpr) valueExpr
-  | .Block (⟨ .LocalVariable name ty none, innerSrc⟩ :: rest) label =>
-    disallowed innerSrc "local variables in functions must have initializers"
+  | .Block (⟨ .Var (.Declare _), innerSrc⟩ :: rest) label => do
+    _ ← disallowed innerSrc "local variables in functions must have initializers"
+    translateExpr { val := StmtExpr.Block rest label, source := innerSrc } boundVars isPureContext
   | .Block (⟨ .IfThenElse cond thenBranch (some elseBranch), innerSrc⟩ :: rest) label =>
     disallowed innerSrc "if-then-else only supported as the last statement in a block"
 
   | .IsType _ _ =>
       throwExprDiagnostic $ diagnosticFromSource expr.source "IsType should have been lowered" DiagnosticType.StrataBug
   | .New _ => throwExprDiagnostic $ diagnosticFromSource expr.source s!"New should have been eliminated by typeHierarchyTransform" DiagnosticType.StrataBug
-  | .FieldSelect target fieldId =>
+  | .Var (.Field target fieldId) =>
       -- Field selects should have been eliminated by heap parameterization
       -- If we see one here, it's an error in the pipeline
       throwExprDiagnostic $ diagnosticFromSource expr.source s!"FieldSelect should have been eliminated by heap parameterization: {Std.ToFormat.format target}#{fieldId.text}" DiagnosticType.StrataBug
   | .Block _ _ =>
       throwExprDiagnostic $ diagnosticFromSource expr.source "block expression should have been lowered in a separate pass" DiagnosticType.StrataBug
-  | .LocalVariable _ _ _ =>
-      throwExprDiagnostic $ diagnosticFromSource expr.source "local variable expression should be lowered in a separate pass" DiagnosticType.StrataBug
   | .Return _ => disallowed expr.source "return expression should be lowered in a separate pass"
 
   | .AsType target _ => throwExprDiagnostic $ diagnosticFromSource expr.source "AsType expression translation" DiagnosticType.NotYetImplemented
@@ -366,98 +368,104 @@ def translateStmt (stmt : StmtExprMd)
       match label with
       | some l => return [Imperative.Stmt.block l innerStmts md]
       | none   => return innerStmts
-  | .LocalVariable id ty initializer =>
-      let coreMonoType ← translateType ty
+  | .Var (.Declare param) =>
+      let coreMonoType ← translateType param.type
       let coreType := LTy.forAll [] coreMonoType
-      let ident := ⟨id.text, ()⟩
-      match initializer with
-      | some (⟨ .StaticCall callee args, callSrc⟩) =>
-          -- Check if this is a function or a procedure call
-          if model.isFunction callee then
-            -- Translate as expression (function application)
-            let coreExpr ← translateExpr { val := .StaticCall callee args, source := callSrc }
-            return [Core.Statement.init ident coreType (.det coreExpr) md]
-          else
-            -- Translate as: var name; call name := callee(args)
-            let coreArgs ← args.mapM (fun a => translateExpr a)
-            let defaultExpr ← defaultExprForType ty
-            let initStmt := Core.Statement.init ident coreType (.det defaultExpr) md
-            let callStmt := Core.Statement.call callee.text (coreArgs.map .inArg ++ [.outArg ident]) md
-            return [initStmt, callStmt]
-      | some (⟨ .InstanceCall .., _⟩) =>
-          -- 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 .nondet md
-          return [initStmt]
-      | some (⟨ .Hole _ _, _⟩) =>
-          -- Hole initializer: treat as havoc (init without value)
-          return [Core.Statement.init ident coreType .nondet md]
-      | some initExpr =>
-          let coreExpr ← translateExpr initExpr
-          return [Core.Statement.init ident coreType (.det coreExpr) md]
-      | none =>
-          return [Core.Statement.init ident coreType .nondet md]
+      let ident := ⟨param.name.text, ()⟩
+      return [Core.Statement.init ident coreType .nondet md]
   | .Assign targets value =>
-      match targets with
-      | [⟨ .Identifier targetId, _ ⟩] =>
-          let ident := ⟨targetId.text, ()⟩
-          -- Check if RHS is a procedure call (not a function)
-          match value.val with
-          | .StaticCall callee args =>
-              if model.isFunction callee then
-                -- Functions are translated as expressions
-                let coreExpr ← translateExpr value
-                return [Core.Statement.set ident coreExpr md]
-              else
-                -- Procedure calls need to be translated as call statements
-                let coreArgs ← args.mapM (fun a => translateExpr a)
-                -- Synthesize throwaway LHS variables for any outputs beyond the
-                -- assigned target (e.g. void-returns-Any adds an extra output).
-                let outputs := match model.get callee with
-                  | .staticProcedure proc => proc.outputs
-                  | .instanceProcedure _ proc => proc.outputs
-                  | _ => []
-                let mut inits : List Core.Statement := []
-                let mut lhs : List Core.CoreIdent := [ident]
-                for out in outputs.drop 1 do
-                  let id ← freshId
-                  let unusedIdent : Core.CoreIdent := ⟨s!"$unused_{id}", ()⟩
-                  let coreType := LTy.forAll [] (← translateType out.type)
-                  inits := inits ++ [Core.Statement.init unusedIdent coreType .nondet md]
-                  lhs := lhs ++ [unusedIdent]
-                let outArgs : List (Core.CallArg Core.Expression) := lhs.map .outArg
-                return inits ++ [Core.Statement.call callee.text (coreArgs.map .inArg ++ outArgs) md]
-          | .InstanceCall .. =>
-              -- Instance method call: havoc the target variable
-              return [Core.Statement.havoc ident md]
-          | .Hole _ _ =>
-              -- Hole RHS: havoc the target (unmodeled call side-effect).
-              return [Core.Statement.havoc ident md]
-          | _ =>
-              let coreExpr ← translateExpr value
-              return [Core.Statement.set ident coreExpr md]
+      -- Check if any target is a Field — these should have been lowered already
+      let hasField := targets.any fun t => match t.val with | .Field _ _ => true | _ => false
+      if hasField then
+        emitDiagnostic $ md.toDiagnostic "Field targets in assignment should have been lowered by heap parameterization" DiagnosticType.StrataBug
+        modify fun s => { s with coreProgramHasSuperfluousErrors := true }
+        return []
+      else
+      -- Match on the value to decide how to translate
+      match _hv : value.val with
+      | .StaticCall callee args =>
+        if model.isFunction callee then
+          -- Function call: translate as a normal expression assignment
+          let coreExpr ← translateExpr value
+          let mut result : List Core.Statement := []
+          for target in targets do
+            match target.val with
+            | .Declare param =>
+              let coreType := LTy.forAll [] (← translateType param.type)
+              let ident : Core.CoreIdent := ⟨param.name.text, ()⟩
+              result := result ++ [Core.Statement.init ident coreType (.det coreExpr) md]
+            | .Local name =>
+              let ident : Core.CoreIdent := ⟨name.text, ()⟩
+              result := result ++ [Core.Statement.set ident coreExpr md]
+            | .Field _ _ => pure () -- already handled above
+          return result
+        else
+          -- Procedure call: init Declare targets with nondet, then emit call
+          let coreArgs ← args.mapM (fun a => translateExpr a)
+          let mut inits : List Core.Statement := []
+          let mut lhs : List Core.CoreIdent := []
+          for target in targets do
+            match target.val with
+            | .Declare param =>
+              let coreType := LTy.forAll [] (← translateType param.type)
+              let ident : Core.CoreIdent := ⟨param.name.text, ()⟩
+              inits := inits ++ [Core.Statement.init ident coreType .nondet md]
+              lhs := lhs ++ [ident]
+            | .Local name =>
+              let ident : Core.CoreIdent := ⟨name.text, ()⟩
+              lhs := lhs ++ [ident]
+            | .Field _ _ => pure () -- already handled above
+          let outArgs : List (Core.CallArg Core.Expression) := lhs.map .outArg
+          return inits ++ [Core.Statement.call callee.text (coreArgs.map .inArg ++ outArgs) md]
+      | .InstanceCall _target callee args =>
+          -- Instance call: init Declare targets with nondet, then emit call
+          let coreArgs ← args.mapM (fun a => translateExpr a)
+          let mut inits : List Core.Statement := []
+          let mut lhs : List Core.CoreIdent := []
+          for target in targets do
+            match target.val with
+            | .Declare param =>
+              let coreType := LTy.forAll [] (← translateType param.type)
+              let ident : Core.CoreIdent := ⟨param.name.text, ()⟩
+              inits := inits ++ [Core.Statement.init ident coreType .nondet md]
+              lhs := lhs ++ [ident]
+            | .Local name =>
+              let ident : Core.CoreIdent := ⟨name.text, ()⟩
+              lhs := lhs ++ [ident]
+            | .Field _ _ => pure () -- already handled above
+          let outArgs : List (Core.CallArg Core.Expression) := lhs.map .outArg
+          return inits ++ [Core.Statement.call callee.text (coreArgs.map .inArg ++ outArgs) md]
+      | .Hole _ _ =>
+          -- Hole RHS: havoc all targets (unmodeled call side-effect).
+          let mut result : List Core.Statement := []
+          for target in targets do
+            match target.val with
+            | .Declare param =>
+              let coreType := LTy.forAll [] (← translateType param.type)
+              let ident : Core.CoreIdent := ⟨param.name.text, ()⟩
+              result := result ++ [Core.Statement.init ident coreType .nondet md]
+            | .Local name =>
+              let ident : Core.CoreIdent := ⟨name.text, ()⟩
+              result := result ++ [Core.Statement.havoc ident md]
+            | .Field _ _ => pure () -- already handled above
+          return result
       | _ =>
-          -- Parallel assignment: (var1, var2, ...) := expr
-          -- Example use is heap-modifying procedure calls: (result, heap) := f(heap, args)
-          match value.val with
-          | .StaticCall callee args =>
-              let coreArgs ← args.mapM (fun a => translateExpr a)
-              let lhsIdents := targets.filterMap fun t =>
-                match t.val with
-                | .Identifier name => some (⟨name.text, ()⟩)
-                | _ => none
-              let outArgs : List (Core.CallArg Core.Expression) := lhsIdents.map .outArg
-              return [Core.Statement.call callee.text (coreArgs.map .inArg ++ outArgs) (astNodeToCoreMd value)]
-          | .InstanceCall .. =>
-              -- Instance method call: havoc all target variables
-              let havocStmts := targets.filterMap fun t =>
-                match t.val with
-                | .Identifier name => some (Core.Statement.havoc ⟨name.text, ()⟩ md)
-                | _ => none
-              return (havocStmts)
-          | _ =>
-              emitDiagnostic $ diagnosticFromSource stmt.source "Assignments with multiple target but without a RHS call should not be constructed"
-              returnNone
+        match targets with
+        | [target] =>
+          let coreExpr ← translateExpr value
+          match target.val with
+            | .Declare param =>
+              let coreType := LTy.forAll [] (← translateType param.type)
+              let ident : Core.CoreIdent := ⟨param.name.text, ()⟩
+              return [Core.Statement.init ident coreType (.det coreExpr) md]
+            | .Local name =>
+              let ident : Core.CoreIdent := ⟨name.text, ()⟩
+              return [Core.Statement.set ident coreExpr md]
+            | .Field _ _ => pure [] -- already handled above
+        | _ =>
+          emitDiagnostic $ md.toDiagnostic "Multi-target assignment need a call as a RHS" DiagnosticType.StrataBug
+          modify fun s => { s with coreProgramHasSuperfluousErrors := true }
+          return []
   | .IfThenElse cond thenBranch elseBranch =>
       let bcond ← translateExpr cond
       let bthen ← translateStmt thenBranch
@@ -472,8 +480,8 @@ def translateStmt (stmt : StmtExprMd)
         exprAsUnusedInit stmt md
       else
         let coreArgs ← args.mapM (fun a => translateExpr a)
-        -- Synthesize throwaway LHS variables so Core arity checking
-        -- passes (lhs.length == outputs.length).
+        -- Generate throwaway LHS variables for all outputs so Core arity
+        -- checking passes (lhs.length == outputs.length).
         let outputs := match model.get callee with
           | .staticProcedure proc => proc.outputs
           | .instanceProcedure _ proc => proc.outputs
@@ -625,12 +633,16 @@ structure LaurelTranslateOptions where
   overflowChecks : Core.OverflowChecks := {}
   keepAllFilesPrefix : Option String := none
   profile : Bool := false
-  deriving Inhabited
+
+instance : Inhabited LaurelTranslateOptions where
+  default := {}
 
 structure LaurelVerifyOptions where
   translateOptions : LaurelTranslateOptions := {}
   verifyOptions : Core.VerifyOptions := .default
-  deriving Inhabited
+
+instance : Inhabited LaurelVerifyOptions where
+  default := {}
 
 /--
 Translate a Laurel Procedure to a Core Function (when applicable) using `TranslateM`.
diff --git a/Strata/Languages/Laurel/LaurelTypes.lean b/Strata/Languages/Laurel/LaurelTypes.lean
index 6f42948de3..ff07ae5171 100644
--- a/Strata/Languages/Laurel/LaurelTypes.lean
+++ b/Strata/Languages/Laurel/LaurelTypes.lean
@@ -21,6 +21,18 @@ no inference is performed.
 
 namespace Strata.Laurel
 
+def getCallType (source : Option FileRange) (model : SemanticModel) (callee : Identifier): HighTypeMd :=
+  match model.get callee with
+    | .datatypeConstructor t _ => ⟨ .UserDefined t, source ⟩
+    | .parameter p => p.type
+    | .staticProcedure proc => match proc.outputs with
+      | [singleOutput] => singleOutput.type
+      | outputs => { val := .MultiValuedExpr (outputs.map (·.type)), source := none }
+    | .unresolved source => { val := HighType.Unknown, source := source }
+    | astNode =>
+      dbg_trace s!"BUG: static call to {callee} not to a procedure but to a {repr astNode}"
+      default
+
 /--
 Compute the HighType of a StmtExpr given a type environment, type definitions, and procedure list.
 No inference is performed — all types are determined by annotations on parameters
@@ -36,23 +48,15 @@ def computeExprType (model : SemanticModel) (expr : StmtExprMd) : HighTypeMd :=
   | .LiteralString _ => ⟨ .TString, source ⟩
   | .LiteralDecimal _ => ⟨ .TReal, source ⟩
   -- Variables
-  | .Identifier id => (model.get id).getType
+  | .Var (.Local id) => (model.get id).getType
+  | .Var (.Declare _) => ⟨ .TVoid, source ⟩
   -- Field access
-  | .FieldSelect _ fieldName => (model.get fieldName).getType
+  | .Var (.Field _ fieldName) => (model.get fieldName).getType
   -- Pure field update returns the same type as the target
   | .PureFieldUpdate target _ _ => computeExprType model target
   -- Calls — return the declared output type when available, fall back to Unknown otherwise
-  | .StaticCall callee _ => match model.get callee with
-    | .datatypeConstructor t _ => ⟨ .UserDefined t, source ⟩
-    | .parameter p => p.type
-    | .staticProcedure proc => match proc.outputs with
-      | [singleOutput] => singleOutput.type
-      | _ => { val := HighType.Unknown, source := none }
-    | .unresolved => { val := HighType.Unknown, source := none }
-    | astNode =>
-      dbg_trace s!"BUG: static call to {callee} not to a procedure but to a {repr astNode}"
-      default
-  | .InstanceCall _ _ _ => default -- TODO: implement
+  | .StaticCall callee _ => getCallType source model callee
+  | .InstanceCall _ callee _ => getCallType source model callee
   -- Operators
   | .PrimitiveOp op args =>
       match args with
@@ -75,7 +79,6 @@ def computeExprType (model : SemanticModel) (expr : StmtExprMd) : HighTypeMd :=
         computeExprType model last
     | none => ⟨ .TVoid, source ⟩
   -- Statements
-  | .LocalVariable _ _ _ => ⟨ .TVoid, source ⟩
   | .While _ _ _ _ => ⟨ .TVoid, source ⟩
   | .Exit _ => ⟨ .TVoid, source ⟩
   | .Return _ => ⟨ .TVoid, source ⟩
diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean
index 1a32241e93..0f1d5a9b69 100644
--- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean
+++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean
@@ -89,6 +89,7 @@ private def emptyMd : Option String := none
 
 /-- Wrap a StmtExpr value with empty metadata -/
 private def bare (v : StmtExpr) : StmtExprMd := ⟨v, none⟩
+private def bareVar (v : Variable) : VariableMd := ⟨v, none⟩
 
 /-- Wrap a HighType value with empty metadata -/
 private def bareType (v : HighType) : HighTypeMd := ⟨v, none⟩
@@ -114,7 +115,7 @@ private def onlyKeepSideEffectStmtsAndLast (stmts : List StmtExprMd) : LiftM (Li
     let last := stmts.getLast!
     let nonLast ← stmts.dropLast.flatMapM (fun s =>
       match s.val with
-      | .LocalVariable .. => do
+      | .Var (.Declare ..) | .Assign ([⟨.Declare .., _⟩]) _ => do
           -- This addPrepend is a hack to work around Core not having let expressions
           -- Otherwise we could keep them in the block
           prepend s
@@ -201,18 +202,18 @@ Shared logic for lifting an assignment in expression position:
 prepends the assignment, creates before-snapshots for all targets,
 and updates substitutions. The value should already be transformed by the caller.
 -/
-private def liftAssignExpr (targets : List StmtExprMd) (seqValue : StmtExprMd)
+private def liftAssignExpr (targets : List VariableMd) (seqValue : StmtExprMd)
     (source : Option FileRange) : LiftM Unit := do
   -- Prepend the assignment itself
   prepend (⟨.Assign targets seqValue, source⟩)
   -- Create a before-snapshot for each target and update substitutions
   for target in targets do
     match target.val with
-    | .Identifier varName =>
+    | .Local varName =>
         let snapshotName ← freshTempFor varName
-        let varType ← computeType target
+        let varType ← computeType (bare (.Var (.Local varName)))
         -- Snapshot goes before the assignment (cons pushes to front)
-        prepend (⟨.LocalVariable snapshotName varType (some (⟨.Identifier varName, source⟩)), source⟩)
+        prepend (⟨.Assign [⟨.Declare ⟨snapshotName, varType⟩, source⟩] (⟨.Var (.Local varName), source⟩), source⟩)
         setSubst varName snapshotName
     | _ => pure ()
 
@@ -225,16 +226,16 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do
   match expr with
   | AstNode.mk val source =>
   match val with
-  | .Identifier name =>
-      return ⟨.Identifier (← getSubst name), source⟩
+  | .Var (.Local name) =>
+      return ⟨.Var (.Local (← getSubst name)), source⟩
 
   | .LiteralInt _ | .LiteralBool _ | .LiteralString _ | .LiteralDecimal _ => return expr
 
   | .Hole false (some holeType) =>
       -- Nondeterministic typed hole: lift to a fresh variable with no initializer (havoc)
       let holeVar ← freshCondVar
-      prepend (bare (.LocalVariable holeVar holeType none))
-      return bare (.Identifier holeVar)
+      prepend (bare (.Var (.Declare ⟨holeVar, holeType⟩)))
+      return bare (.Var (.Local holeVar))
 
   | .Assign targets value =>
       -- The expression result is the current substitution for the first target
@@ -244,7 +245,14 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do
         | _ => return expr
 
       let resultExpr ← match firstTarget.val with
-        | .Identifier varName => pure (⟨.Identifier (← getSubst varName), source⟩)
+        | .Local varName => pure (⟨.Var (.Local (← getSubst varName)), source⟩)
+        | .Declare param =>
+          -- Declaration with initializer: check if substitution exists
+          let hasSubst := (← get).subst.lookup param.name |>.isSome
+          if hasSubst then
+            pure (⟨.Var (.Local (← getSubst param.name)), source⟩)
+          else
+            return expr
         | _ =>
           dbg_trace "Strata bug: non-identifier targets should have been removed before the lift expression phase";
           return expr
@@ -271,11 +279,11 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do
       let callResultVar ← freshCondVar
       let callResultType ← computeType expr
       let liftedCall := [
-        ⟨ (.LocalVariable callResultVar callResultType none), source⟩,
-        ⟨.Assign [bare (.Identifier callResultVar)] seqCall, source⟩
+        ⟨ (.Var (.Declare ⟨callResultVar, callResultType⟩)), source ⟩,
+        ⟨.Assign [bareVar (.Local callResultVar)] seqCall, source⟩
       ]
       modify fun s => { s with prependedStmts := s.prependedStmts ++ liftedCall}
-      return bare (.Identifier callResultVar)
+      return bare (.Var (.Local callResultVar))
 
   | .IfThenElse cond thenBranch elseBranch =>
       let model :=  (← get).model
@@ -294,14 +302,14 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do
         modify fun s => { s with prependedStmts := [], subst := [] }
         let seqThen ← transformExpr thenBranch
         let thenPrepends ← takePrepends
-        let thenBlock := bare (.Block (thenPrepends ++ [⟨.Assign [bare (.Identifier condVar)] seqThen, source⟩]) none)
+        let thenBlock := bare (.Block (thenPrepends ++ [⟨.Assign [bareVar (.Local condVar)] seqThen, source⟩]) none)
         -- Process else-branch from scratch
         modify fun s => { s with prependedStmts := [], subst := [] }
         let seqElse ← match elseBranch with
           | some e => do
               let se ← transformExpr e
               let elsePrepends ← takePrepends
-              pure (some (bare (.Block (elsePrepends ++ [⟨.Assign [bare (.Identifier condVar)] se, source⟩]) none)))
+              pure (some (bare (.Block (elsePrepends ++ [⟨.Assign [bareVar (.Local condVar)] se, source⟩]) none)))
           | none => pure none
         -- Restore outer state
         modify fun s => { s with subst := savedSubst, prependedStmts := savedPrepends }
@@ -312,8 +320,8 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do
         -- IfThenElse added first (cons puts it deeper), then declaration (cons puts it on top)
         -- Output order: declaration, then if-then-else
         prepend (⟨.IfThenElse seqCond thenBlock seqElse, source⟩)
-        prepend (bare (.LocalVariable condVar condType none))
-        return bare (.Identifier condVar)
+        prepend (bare (.Var (.Declare ⟨condVar, condType⟩)))
+        return bare (.Var (.Local condVar))
       else
         -- No assignments in branches — recurse normally
         let seqCond ← transformExpr cond
@@ -327,19 +335,14 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do
       let newStmts := (← stmts.reverse.mapM transformExpr).reverse
       return ⟨ .Block (← onlyKeepSideEffectStmtsAndLast newStmts) labelOption, source⟩
 
-  | .LocalVariable name ty initializer =>
+  | .Var (.Declare param) =>
       -- If the substitution map has an entry for this variable, it was
       -- assigned to the right and we need to lift this declaration so it
       -- appears before the snapshot that references it.
-      let hasSubst := (← get).subst.lookup name |>.isSome
+      let hasSubst := (← get).subst.lookup param.name |>.isSome
       if hasSubst then
-        match initializer with
-        | some initExpr =>
-            let seqInit ← transformExpr initExpr
-            prepend (⟨.LocalVariable name ty (some seqInit), expr.source⟩)
-        | none =>
-            prepend (⟨.LocalVariable name ty none, expr.source⟩)
-        return ⟨.Identifier (← getSubst name), expr.source⟩
+        prepend (⟨.Var (.Declare param), expr.source⟩)
+        return ⟨.Var (.Local (← getSubst param.name)), expr.source⟩
       else
         return expr
 
@@ -380,34 +383,8 @@ def transformStmt (stmt : StmtExprMd) : LiftM (List StmtExprMd) := do
       let seqStmts ← stmts.mapM transformStmt
       return [bare (.Block seqStmts.flatten metadata)]
 
-  | .LocalVariable name ty initializer =>
-      match _ : initializer with
-      | some initExprMd =>
-         -- If the initializer is a direct imperative StaticCall, don't lift it —
-         -- translateStmt handles LocalVariable + StaticCall directly as a call statement.
-          match _: initExprMd with
-          | AstNode.mk initExpr _ =>
-          match _: initExpr with
-          | .StaticCall callee args =>
-              let model := (← get).model
-              if model.isFunction callee then
-                let seqInit ← transformExpr initExprMd
-                let prepends ← takePrepends
-                modify fun s => { s with subst := [] }
-                return prepends ++ [⟨.LocalVariable name ty (some seqInit), source⟩]
-              else
-                -- Pass through as-is; translateStmt will emit init + call
-                let seqArgs ← args.mapM transformExpr
-                let argPrepends ← takePrepends
-                modify fun s => { s with subst := [] }
-                return argPrepends ++ [⟨.LocalVariable name ty (some ⟨.StaticCall callee seqArgs, initExprMd.source⟩), source⟩]
-          | _ =>
-              let seqInit ← transformExpr initExprMd
-              let prepends ← takePrepends
-              modify fun s => { s with subst := [] }
-              return prepends ++ [⟨.LocalVariable name ty (some seqInit), source⟩]
-      | none =>
-          return [stmt]
+  | .Var (.Declare _) =>
+      return [stmt]
 
   | .Assign targets valueMd =>
       -- If the RHS is a direct imperative StaticCall, don't lift it —
diff --git a/Strata/Languages/Laurel/MapStmtExpr.lean b/Strata/Languages/Laurel/MapStmtExpr.lean
index b236c37317..e3892bae93 100644
--- a/Strata/Languages/Laurel/MapStmtExpr.lean
+++ b/Strata/Languages/Laurel/MapStmtExpr.lean
@@ -38,8 +38,6 @@ def mapStmtExprM [Monad m] (f : StmtExprMd → m StmtExprMd) (expr : StmtExprMd)
       (← el.attach.mapM fun ⟨e, _⟩ => mapStmtExprM f e), source⟩
   | .Block stmts label =>
     pure ⟨.Block (← stmts.attach.mapM fun ⟨e, _⟩ => mapStmtExprM f e) label, source⟩
-  | .LocalVariable name ty init =>
-    pure ⟨.LocalVariable name ty (← init.attach.mapM fun ⟨e, _⟩ => mapStmtExprM f e), source⟩
   | .While cond invs dec body =>
     pure ⟨.While (← mapStmtExprM f cond)
       (← invs.attach.mapM fun ⟨e, _⟩ => mapStmtExprM f e)
@@ -48,9 +46,15 @@ def mapStmtExprM [Monad m] (f : StmtExprMd → m StmtExprMd) (expr : StmtExprMd)
   | .Return v =>
     pure ⟨.Return (← v.attach.mapM fun ⟨e, _⟩ => mapStmtExprM f e), source⟩
   | .Assign targets value =>
-    pure ⟨.Assign (← targets.attach.mapM fun ⟨e, _⟩ => mapStmtExprM f e) (← mapStmtExprM f value), source⟩
-  | .FieldSelect target fieldName =>
-    pure ⟨.FieldSelect (← mapStmtExprM f target) fieldName, source⟩
+    let targets' ← targets.attach.mapM fun ⟨v, _⟩ => do
+      let ⟨vv, vs⟩ := v
+      match vv with
+      | .Field target fieldName =>
+        pure ⟨Variable.Field (← mapStmtExprM f target) fieldName, vs⟩
+      | .Local _ | .Declare _ => pure v
+    pure ⟨.Assign targets' (← mapStmtExprM f value), source⟩
+  | .Var (.Field target fieldName) =>
+    pure ⟨.Var (.Field (← mapStmtExprM f target) fieldName), source⟩
   | .PureFieldUpdate target fieldName newValue =>
     pure ⟨.PureFieldUpdate (← mapStmtExprM f target) fieldName (← mapStmtExprM f newValue), source⟩
   | .StaticCall callee args =>
@@ -88,7 +92,7 @@ def mapStmtExprM [Monad m] (f : StmtExprMd → m StmtExprMd) (expr : StmtExprMd)
   -- it must get its own arm above; otherwise all passes will silently
   -- skip recursion into those children.
   | .Exit _ | .LiteralInt _ | .LiteralBool _ | .LiteralString _ | .LiteralDecimal _
-  | .Identifier _ | .New _ | .This | .Abstract | .All | .Hole .. => pure expr
+  | .Var (.Local _) | .Var (.Declare _) | .New _ | .This | .Abstract | .All | .Hole .. => pure expr
   f rebuilt
 termination_by sizeOf expr
 decreasing_by
@@ -96,7 +100,7 @@ decreasing_by
   all_goals (try have := AstNode.sizeOf_val_lt expr)
   all_goals (try have := Condition.sizeOf_condition_lt ‹_›)
   all_goals (try term_by_mem)
-  all_goals omega
+  all_goals (cases expr; simp_all; omega)
 
 /-- Pure bottom-up traversal of `StmtExprMd`. -/
 def mapStmtExpr (f : StmtExprMd → StmtExprMd) (expr : StmtExprMd) : StmtExprMd :=
diff --git a/Strata/Languages/Laurel/ModifiesClauses.lean b/Strata/Languages/Laurel/ModifiesClauses.lean
index ac9309a5de..20fd01445d 100644
--- a/Strata/Languages/Laurel/ModifiesClauses.lean
+++ b/Strata/Languages/Laurel/ModifiesClauses.lean
@@ -103,10 +103,10 @@ def buildModifiesEnsures (proc: Procedure) (model: SemanticModel) (modifiesExprs
   let entries := extractModifiesEntries model modifiesExprs
   let objName : Identifier := "$modifies_obj"
   let fldName : Identifier := "$modifies_fld"
-  let obj := mkMd <| .Identifier objName
-  let fld := mkMd <| .Identifier fldName
-  let heapIn := mkMd <| .Identifier heapInName
-  let heapOut := mkMd <| .Identifier heapOutName
+  let obj := mkMd <| .Var (.Local objName)
+  let fld := mkMd <| .Var (.Local fldName)
+  let heapIn := mkMd <| .Var (.Local heapInName)
+  let heapOut := mkMd <| .Var (.Local heapOutName)
       -- Build the "obj is allocated" condition: Composite..ref($obj) < $heap_in.nextReference
   let heapCounter := mkMd <| .StaticCall "Heap..nextReference!" [heapIn]
   let objRef := mkMd <| .StaticCall "Composite..ref!" [obj]
@@ -146,6 +146,9 @@ may modify anything on the heap), and the modifies list is simply cleared.
 If the procedure has a `$heap` but no modifies clause, adds a postcondition
 that all allocated objects are preserved between heaps:
   `forall $obj: Composite, $fld: Field => $obj < $heap_in.nextReference ==> readField($heap_in, $obj, $fld) == readField($heap, $obj, $fld)`
+
+If the modifies clause uses a wildcard (`*`), the frame condition is skipped
+entirely — the procedure may modify anything.
 -/
 def transformModifiesClauses (model: SemanticModel)
     (proc : Procedure) : Except (Array DiagnosticModel) Procedure :=
@@ -160,7 +163,7 @@ def transformModifiesClauses (model: SemanticModel)
         let heapName : Identifier := "$heap"
         let frameCondition := buildModifiesEnsures proc model modifiesExprs heapInName heapName
         let postconds' := match frameCondition with
-          | some frame => postconds ++ [{ condition := frame : Condition }]
+          | some frame => postconds ++ [{ condition := frame, summary := "modifies clause" }]
           | none => postconds
         .ok { proc with body := .Opaque postconds' impl [] }
       else
diff --git a/Strata/Languages/Laurel/Resolution.lean b/Strata/Languages/Laurel/Resolution.lean
index 00914cfd74..659dda2864 100644
--- a/Strata/Languages/Laurel/Resolution.lean
+++ b/Strata/Languages/Laurel/Resolution.lean
@@ -33,7 +33,7 @@ happens after Phase 1, the `ResolvedNode` values in the map contain the fully
 resolved sub-trees (e.g. a procedure's parameters already have their IDs).
 
 ### Definition nodes (introduce a name into scope)
-- `StmtExpr.LocalVariable` — local variable declaration
+- `Variable.Declare` — local variable declaration (in `Assign` targets or `Var`)
 - `StmtExpr.Quantifier` — quantifier-bound variable
 - `Parameter` — procedure parameter
 - `Procedure` — procedure definition
@@ -43,10 +43,10 @@ resolved sub-trees (e.g. a procedure's parameters already have their IDs).
 - `Constant` — named constant
 
 ### Reference nodes (use a name)
-- `StmtExpr.Identifier` — variable reference
+- `StmtExpr.Var (.Local ...)` — variable reference
 - `StmtExpr.StaticCall` — static procedure call
 - `StmtExpr.InstanceCall` — instance method call
-- `StmtExpr.FieldSelect` — field access
+- `StmtExpr.Var (.Field ...)` — field access
 - `StmtExpr.New` — object creation (references a type)
 - `StmtExpr.Exit` — exit a labelled block
 - `HighType.UserDefined` — type reference
@@ -122,11 +122,11 @@ inductive ResolvedNode where
   | constant (c : Constant)
   /-- A quantifier-bound variable. -/
   | quantifierVar (name : Identifier) (type : HighTypeMd)
-  | unresolved
+  | unresolved (referenceSource: Option FileRange)
   deriving Repr
 
 instance : Inhabited ResolvedNode where
-  default := ResolvedNode.unresolved
+  default := ResolvedNode.unresolved none
 
 /-- Return the constructor tag of a `ResolvedNode`. -/
 def ResolvedNode.kind : ResolvedNode → ResolvedNodeKind
@@ -142,7 +142,7 @@ def ResolvedNode.kind : ResolvedNode → ResolvedNodeKind
   | .typeAlias ..         => .typeAlias
   | .constant ..          => .constant
   | .quantifierVar ..     => .quantifierVar
-  | .unresolved           => .unresolved
+  | .unresolved _          => .unresolved
 
 def ResolvedNode.getType (node: ResolvedNode): HighTypeMd := match node with
  | .var _ type => type
@@ -151,10 +151,8 @@ def ResolvedNode.getType (node: ResolvedNode): HighTypeMd := match node with
  | .datatypeConstructor type _ => ⟨ .UserDefined type, none ⟩
  | .constant c => c.type
  | .quantifierVar _ type => type
- | .unresolved =>
-    -- The Python through Laurel pipeline does not resolve yet
-    ⟨ .UserDefined "dummyName", none ⟩
- | _ => dbg_trace s!"SOUND BUG: getType called on {repr node}"; ⟨ HighType.Unknown, none ⟩
+ | .unresolved source => ⟨ .Unknown, source ⟩
+ | _ => dbg_trace s!"SOUND BUG: getType called on {repr node}"; default
 
 /-! ## Resolution result -/
 
@@ -175,7 +173,7 @@ def SemanticModel.isFunction (model: SemanticModel) (id: Identifier): Bool :=
       | .parameter _ => true
       | .datatypeConstructor _ _ => true
       | .constant _ => true
-      | .unresolved => true -- functions calls are more permissive, so true avoids possibly incorrect errors
+      | .unresolved _ => true -- functions calls are more permissive, so true avoids possibly incorrect errors
       | node =>
           dbg_trace s!"Sound but incomplete BUG! id: {repr id}, is not a procedure, but a node {repr node}"
           false
@@ -225,18 +223,6 @@ private def freshId : ResolveM Nat := do
   set { s with nextId := id + 1 }
   return id
 
-/-- Register a definition: assign a fresh ID to the identifier and record it in scope with its ResolvedNode. -/
-def defineName (iden : Identifier) (node : ResolvedNode) (overrideResolutionName: Option String := none) : ResolveM Identifier := do
-  let resolutionName := overrideResolutionName.getD iden.text
-  let (name', uniqueId) ← match iden.uniqueId with
-    | some uid => pure (iden, uid)
-    | none =>
-      let id ← freshId
-      pure ({ iden with uniqueId := some (id) }, id)
-
-  modify fun s => { s with scope := s.scope.insert resolutionName (uniqueId, node),
-                           currentScopeNames := s.currentScopeNames.insert resolutionName }
-  return name'
 
 /-- Like `defineName`, but reports a diagnostic if the name already exists in the current scope.
     Inserts an `.unresolved` node so subsequent references still resolve without cascading errors. -/
@@ -245,9 +231,21 @@ def defineNameCheckDup (iden : Identifier) (node : ResolvedNode) (overrideResolu
   if (← get).currentScopeNames.contains resolutionName then
     let diag := diagnosticFromSource iden.source s!"Duplicate definition '{resolutionName}' is already defined in this scope"
     modify fun s => { s with errors := s.errors.push diag }
-    defineName iden .unresolved overrideResolutionName
+    defineName iden (.unresolved iden.source) overrideResolutionName
   else
     defineName iden node overrideResolutionName
+  where
+  defineName (iden : Identifier) (node : ResolvedNode) (overrideResolutionName: Option String := none) : ResolveM Identifier := do
+    let resolutionName := overrideResolutionName.getD iden.text
+    let (name', uniqueId) ← match iden.uniqueId with
+      | some uid => pure (iden, uid)
+      | none =>
+        let id ← freshId
+        pure ({ iden with uniqueId := some (id) }, id)
+
+    modify fun s => { s with scope := s.scope.insert resolutionName (uniqueId, node),
+                             currentScopeNames := s.currentScopeNames.insert resolutionName }
+    return name'
 
 /-- Resolve a reference: look up the name in scope and assign the definition's ID.
     Returns the identifier with its ID filled in.
@@ -274,7 +272,7 @@ def resolveRef (name : Identifier) (source : Option FileRange := none)
 private def targetTypeName (target : StmtExprMd) : ResolveM (Option String) := do
   let s ← get
   match target.val with
-  | .Identifier ref =>
+  | .Var (.Local ref) =>
     match s.scope.get? ref.text with
     | some (_, node) =>
       match node.getType.val with
@@ -349,6 +347,9 @@ def resolveHighType (ty : HighTypeMd) : ResolveM HighTypeMd := do
   | .Intersection tys =>
     let tys' ← tys.mapM resolveHighType
     pure (.Intersection tys')
+  | .MultiValuedExpr tys =>
+    let tys' ← tys.mapM resolveHighType
+    pure (.MultiValuedExpr tys')
   | other => pure other
   return { val := val', source := ty.source }
 
@@ -365,11 +366,6 @@ def resolveStmtExpr (exprMd : StmtExprMd) : ResolveM StmtExprMd := do
     withScope do
       let stmts' ← stmts.mapM resolveStmtExpr
       pure (.Block stmts' label)
-  | .LocalVariable name ty init =>
-    let ty' ← resolveHighType ty
-    let init' ← init.attach.mapM (fun a => have := a.property; resolveStmtExpr a.val)
-    let name' ← defineNameCheckDup name (.var name ty')
-    pure (.LocalVariable name' ty' init')
   | .While cond invs dec body =>
     let cond' ← resolveStmtExpr cond
     let invs' ← invs.attach.mapM (fun a => have := a.property; resolveStmtExpr a.val)
@@ -384,17 +380,60 @@ def resolveStmtExpr (exprMd : StmtExprMd) : ResolveM StmtExprMd := do
   | .LiteralBool v => pure (.LiteralBool v)
   | .LiteralString v => pure (.LiteralString v)
   | .LiteralDecimal v => pure (.LiteralDecimal v)
-  | .Identifier ref =>
+  | .Var (.Local ref) =>
     let ref' ← resolveRef ref source
-    pure (.Identifier ref')
+    pure (.Var (.Local ref'))
+  | .Var (.Declare param) =>
+    let ty' ← resolveHighType param.type
+    let name' ← defineNameCheckDup param.name (.var param.name ty')
+    pure (.Var (.Declare ⟨name', ty'⟩))
   | .Assign targets value =>
-    let targets' ← targets.mapM resolveStmtExpr
+    let targets' ← targets.attach.mapM fun ⟨v, _⟩ => do
+      let ⟨vv, vs⟩ := v
+      match vv with
+      | .Local ref =>
+        let ref' ← resolveRef ref source
+        pure (⟨.Local ref', vs⟩ : VariableMd)
+      | .Field target fieldName =>
+        let target' ← resolveStmtExpr target
+        let fieldName' ← resolveFieldRef target' fieldName source
+        pure (⟨.Field target' fieldName', vs⟩ : VariableMd)
+      | .Declare param =>
+        let ty' ← resolveHighType param.type
+        let name' ← defineNameCheckDup param.name (.var param.name ty')
+        pure (⟨.Declare ⟨name', ty'⟩, vs⟩ : VariableMd)
     let value' ← resolveStmtExpr value
+    -- Check that LHS target count matches the number of outputs from the RHS
+    let expectedOutputCount ← match value'.val with
+      | .StaticCall callee _ => do
+        let s ← get
+        match s.scope.get? callee.text with
+        | some (_, .staticProcedure proc) => pure (some proc.outputs.length)
+        | some (_, .instanceProcedure _ proc) => pure (some proc.outputs.length)
+        | _ => pure none
+      | .InstanceCall _ callee _ => do
+        let s ← get
+        match s.scope.get? callee.text with
+        | some (_, .instanceProcedure _ proc) => pure (some proc.outputs.length)
+        | some (_, .staticProcedure proc) => pure (some proc.outputs.length)
+        | _ => pure none
+      | _ => pure none
+    match expectedOutputCount with
+    | some expected =>
+      if targets'.length != expected then
+        let calleeName := match value'.val with
+          | .StaticCall callee _ => callee.text
+          | .InstanceCall _ callee _ => callee.text
+          | _ => "unknown"
+        let diag := diagnosticFromSource source
+          s!"Assignment target count mismatch: {targets'.length} targets but '{calleeName}' returns {expected} values"
+        modify fun s => { s with errors := s.errors.push diag }
+    | none => pure ()
     pure (.Assign targets' value')
-  | .FieldSelect target fieldName =>
+  | .Var (.Field target fieldName) =>
     let target' ← resolveStmtExpr target
     let fieldName' ← resolveFieldRef target' fieldName source
-    pure (.FieldSelect target' fieldName')
+    pure (.Var (.Field target' fieldName'))
   | .PureFieldUpdate target fieldName newVal =>
     let target' ← resolveStmtExpr target
     let fieldName' ← resolveFieldRef target' fieldName source
@@ -493,15 +532,19 @@ def resolveBody (body : Body) : ResolveM Body := do
     return .Abstract posts'
   | .External => return .External
 
-/-- Resolve a procedure: define its name, then resolve params, contracts, and body in a new scope. -/
+/-- Resolve a procedure: resolve its name, then resolve params, contracts, and body in a new scope. -/
 def resolveProcedure (proc : Procedure) : ResolveM Procedure := do
-  let procName' ← defineName proc.name (.staticProcedure proc)
+  let procName' ← resolveRef proc.name
   withScope do
     let inputs' ← proc.inputs.mapM resolveParameter
     let outputs' ← proc.outputs.mapM resolveParameter
     let pres' ← proc.preconditions.mapM (·.mapM resolveStmtExpr)
     let dec' ← proc.decreases.mapM resolveStmtExpr
     let body' ← resolveBody proc.body
+    if !proc.isFunctional && body'.isTransparent then
+      let diag := diagnosticFromSource proc.name.source
+        s!"transparent procedures are not yet supported. Add 'opaque' to make the procedure opaque"
+      modify fun s => { s with errors := s.errors.push diag }
     let invokeOn' ← proc.invokeOn.mapM resolveStmtExpr
     return { name := procName', inputs := inputs', outputs := outputs',
              isFunctional := proc.isFunctional,
@@ -513,12 +556,16 @@ def resolveProcedure (proc : Procedure) : ResolveM Procedure := do
 def resolveField (ownerName : Identifier) (field : Field) : ResolveM Field := do
   let ty' ← resolveHighType field.type
   let qualifiedName := ownerName.text ++ "." ++ field.name.text
-  let name' ← defineName field.name (.field ownerName { field with type := ty' }) (some qualifiedName)
+  let resolved ← resolveRef qualifiedName
+  -- Keep the original field name text; only take the uniqueId from resolution.
+  -- resolveRef returns text = "Owner.field" (the qualified lookup key), but the
+  -- field's own name should stay unqualified.
+  let name' := { field.name with uniqueId := resolved.uniqueId }
   return { name := name', isMutable := field.isMutable, type := ty' }
 
 /-- Resolve an instance procedure on a composite type. -/
 def resolveInstanceProcedure (typeName : Identifier) (proc : Procedure) : ResolveM Procedure := do
-  let procName' ← defineName proc.name (.instanceProcedure typeName proc)
+  let procName' ← resolveRef proc.name
   withScope do
     let savedInstType := (← get).instanceTypeName
     modify fun s => { s with instanceTypeName := some typeName.text }
@@ -527,6 +574,10 @@ def resolveInstanceProcedure (typeName : Identifier) (proc : Procedure) : Resolv
     let pres' ← proc.preconditions.mapM (·.mapM resolveStmtExpr)
     let dec' ← proc.decreases.mapM resolveStmtExpr
     let body' ← resolveBody proc.body
+    if !proc.isFunctional && body'.isTransparent then
+      let diag := diagnosticFromSource proc.name.source
+        s!"transparent procedures are not yet supported. Add 'opaque' to make the procedure opaque"
+      modify fun s => { s with errors := s.errors.push diag }
     let invokeOn' ← proc.invokeOn.mapM resolveStmtExpr
     modify fun s => { s with instanceTypeName := savedInstType }
     return { name := procName', inputs := inputs', outputs := outputs',
@@ -539,7 +590,7 @@ def resolveInstanceProcedure (typeName : Identifier) (proc : Procedure) : Resolv
 def resolveTypeDefinition (td : TypeDefinition) : ResolveM TypeDefinition := do
   match td with
   | .Composite ct =>
-    let ctName' ← defineName ct.name (.compositeType ct)
+    let ctName' ← resolveRef ct.name
     let extending' ← ct.extending.mapM (resolveRef · none (expected := #[.compositeType]))
     let fields' ← ct.fields.mapM (resolveField ctName')
     -- Build per-type scope BEFORE resolving instance procedures, so that
@@ -563,40 +614,41 @@ def resolveTypeDefinition (td : TypeDefinition) : ResolveM TypeDefinition := do
     return .Composite { name := ctName', extending := extending',
                         fields := fields', instanceProcedures := instProcs' }
   | .Constrained ct =>
-    let ctName' ← defineName ct.name (.constrainedType ct)
+    let ctName' ← resolveRef ct.name
     let base' ← resolveHighType ct.base
     -- The valueName (e.g. `x` in `constrained nat = x: int where x >= 0`) must be
     -- in scope when resolving the constraint and witness expressions.
     let (valueName', constraint', witness') ← withScope do
-      let valueName' ← defineName ct.valueName (.quantifierVar ct.valueName base')
+      let valueName' ← defineNameCheckDup ct.valueName (.quantifierVar ct.valueName base')
       let constraint' ← resolveStmtExpr ct.constraint
       let witness' ← resolveStmtExpr ct.witness
       return (valueName', constraint', witness')
     return .Constrained { name := ctName', base := base', valueName := valueName',
                           constraint := constraint', witness := witness' }
   | .Datatype dt =>
-    let dtName' ← defineName dt.name (.datatypeDefinition dt)
+    let dtName' ← resolveRef dt.name
     let ctors' ← dt.constructors.mapM fun ctor => do
-      let ctorName' ← defineName ctor.name (.datatypeConstructor dt.name ctor)
-      _ ← defineName ctor.name (.datatypeConstructor dt.name ctor) (some (dt.testerName ctor))
+      let ctorName' ← resolveRef ctor.name
       let args' ← ctor.args.mapM fun (p: Parameter) => do
         let ty' ← resolveHighType p.type
-        let destructorId ← defineName p.name (.parameter p) (some (dt.destructorName p))
-        -- unsafeDestructorId
-        _ ← defineName p.name (.parameter p) (some (dt.unsafeDestructorName p))
+        let resolved ← resolveRef (dt.destructorName p)
+        -- Keep the original parameter name; only take the uniqueId from resolution.
+        -- resolveRef returns text = "DtName..field" (the qualified lookup key), but the
+        -- parameter's own name should stay unqualified.
+        let destructorId := { p.name with uniqueId := resolved.uniqueId }
         return ⟨ destructorId, ty' ⟩
       return { name := ctorName', args := args' : DatatypeConstructor }
     return .Datatype { name := dtName', typeArgs := dt.typeArgs, constructors := ctors' }
   | .Alias ta =>
     let target' ← resolveHighType ta.target
-    let taName' ← defineName ta.name (.typeAlias { ta with target := target' })
+    let taName' ← resolveRef ta.name
     return .Alias { name := taName', target := target' }
 
 /-- Resolve a constant definition. -/
 def resolveConstant (c : Constant) : ResolveM Constant := do
   let ty' ← resolveHighType c.type
   let init' ← c.initializer.mapM resolveStmtExpr
-  let name' ← defineName c.name (.constant c)
+  let name' ← resolveRef c.name
   return { name := name', type := ty', initializer := init' }
 
 /-! ## Phase 2: Build refToDef map from the resolved program -/
@@ -623,6 +675,7 @@ private def collectHighType (map : Std.HashMap Nat ResolvedNode) (ty : HighTypeM
     args.foldl collectHighType map
   | .Pure base => collectHighType map base
   | .Intersection tys => tys.foldl collectHighType map
+  | .MultiValuedExpr tys => tys.foldl collectHighType map
   | _ => map
 
 private def collectStmtExpr (map : Std.HashMap Nat ResolvedNode) (expr : StmtExprMd)
@@ -637,23 +690,25 @@ private def collectStmtExpr (map : Std.HashMap Nat ResolvedNode) (expr : StmtExp
     | some e => collectStmtExpr map e
     | none => map
   | .Block stmts _ => stmts.foldl collectStmtExpr map
-  | .LocalVariable name ty init =>
-    let map := register map name (.var name ty)
-    let map := collectHighType map ty
-    match init with
-    | some i => collectStmtExpr map i
-    | none => map
   | .While cond invs dec body =>
     let map := collectStmtExpr map cond
     let map := invs.foldl collectStmtExpr map
     let map := match dec with | some d => collectStmtExpr map d | none => map
     collectStmtExpr map body
   | .Return val => match val with | some v => collectStmtExpr map v | none => map
-  | .Identifier _ => map
+  | .Var (.Local _) => map
+  | .Var (.Declare param) =>
+    let map := register map param.name (.var param.name param.type)
+    collectHighType map param.type
   | .Assign targets value =>
-    let map := targets.foldl collectStmtExpr map
+    let map := targets.foldl (fun map t =>
+      match t.val with
+      | .Declare param =>
+        let map := register map param.name (.var param.name param.type)
+        collectHighType map param.type
+      | _ => map) map
     collectStmtExpr map value
-  | .FieldSelect target _ => collectStmtExpr map target
+  | .Var (.Field target _) => collectStmtExpr map target
   | .PureFieldUpdate target _ newVal =>
     let map := collectStmtExpr map target
     collectStmtExpr map newVal
@@ -761,6 +816,7 @@ def buildRefToDef (program : Program) : Std.HashMap Nat ResolvedNode :=
 
 /-! ## Pre-registration: populate scope with all top-level names before resolving bodies -/
 
+
 /-- A default ResolvedNode used as a placeholder during pre-registration.
     It will be overwritten with the real node when the definition is fully resolved. -/
 private def placeholderNode : ResolvedNode := .var "$placeholder" { val := .TVoid, source := none }
@@ -778,17 +834,20 @@ private def preRegisterTopLevel (program : Program) : ResolveM Unit := do
       let _ ← defineNameCheckDup ct.name (.compositeType ct)
       for field in ct.fields do
         let qualifiedName := ct.name.text ++ "." ++ field.name.text
-        let _ ← defineNameCheckDup field.name placeholderNode (some qualifiedName)
+        let _ ← defineNameCheckDup field.name (.field ct.name field) (some qualifiedName)
       for proc in ct.instanceProcedures do
-        let _ ← defineNameCheckDup proc.name placeholderNode
+        let _ ← defineNameCheckDup proc.name (.instanceProcedure ct.name proc)
     | .Constrained ct =>
       let _ ← defineNameCheckDup ct.name (.constrainedType ct)
     | .Datatype dt =>
       let _ ← defineNameCheckDup dt.name (.datatypeDefinition dt)
       for ctor in dt.constructors do
-        let _ ← defineName ctor.name (.datatypeConstructor dt.name ctor)
+        _ ← defineNameCheckDup ctor.name (.datatypeConstructor dt.name ctor) (some (dt.testerName ctor))
+        let _ ← defineNameCheckDup ctor.name (.datatypeConstructor dt.name ctor)
         for p in ctor.args do
-          let _ ← defineName p.name placeholderNode (some (dt.destructorName p))
+          let _ ← defineNameCheckDup p.name (.parameter p) (some (dt.destructorName p))
+          -- unsafeDestructorId
+          let _ ← defineNameCheckDup p.name (.parameter p) (some (dt.unsafeDestructorName p))
     | .Alias ta =>
       let _ ← defineNameCheckDup ta.name (.typeAlias ta)
   -- Pre-register constants
diff --git a/Strata/Languages/Laurel/TypeAliasElim.lean b/Strata/Languages/Laurel/TypeAliasElim.lean
index ed67eee05c..f4ccc539a0 100644
--- a/Strata/Languages/Laurel/TypeAliasElim.lean
+++ b/Strata/Languages/Laurel/TypeAliasElim.lean
@@ -51,11 +51,18 @@ partial def resolveAliasType (amap : AliasMap) (ty : HighTypeMd)
     { val := .Intersection (tys.map (resolveAliasType amap · visited)), source := ty.source }
   | _ => ty
 
+def resolveAliasVariable (amap : AliasMap) (v : VariableMd) : VariableMd :=
+  match v.val with
+  | .Declare param => ⟨.Declare { param with type := resolveAliasType amap param.type }, v.source⟩
+  | _ => v
+
 /-- Resolve aliases in expression type positions. -/
 def resolveAliasExprNode (amap : AliasMap) (expr : StmtExprMd) : StmtExprMd :=
   match expr.val with
-  | .LocalVariable n ty init =>
-    { val := .LocalVariable n (resolveAliasType amap ty) init, source := expr.source }
+  | .Assign targets value =>
+    ⟨.Assign (targets.map (resolveAliasVariable amap)) value, expr.source⟩
+  | .Var (.Declare param) =>
+    ⟨.Var (.Declare { param with type := resolveAliasType amap param.type }), expr.source⟩
   | .Quantifier mode param trigger body =>
     { val := .Quantifier mode { param with type := resolveAliasType amap param.type } trigger body, source := expr.source }
   | .AsType t ty => { val := .AsType t (resolveAliasType amap ty), source := expr.source }
diff --git a/Strata/Languages/Laurel/TypeHierarchy.lean b/Strata/Languages/Laurel/TypeHierarchy.lean
index 8b15aaa76e..b03d241787 100644
--- a/Strata/Languages/Laurel/TypeHierarchy.lean
+++ b/Strata/Languages/Laurel/TypeHierarchy.lean
@@ -38,6 +38,7 @@ def computeAncestors (model: SemanticModel) (name : Identifier) : List Composite
     else (acc ++ [ct], seen ++ [ct.name])) ([], seen) |>.1
 
 private def mkMd (e : StmtExpr) : StmtExprMd := ⟨e, none⟩
+private def mkVarMd (v : Variable) : VariableMd := ⟨v, none⟩
 
 /--
 Generate Laurel constant definitions for the type hierarchy:
@@ -122,7 +123,7 @@ Walk a StmtExpr AST and collect DiagnosticModel errors for diamond-inherited fie
 def validateDiamondFieldAccessesForStmtExpr (model : SemanticModel)
     (expr : StmtExprMd) : List DiagnosticModel :=
   match _h : expr.val with
-  | .FieldSelect target fieldName =>
+  | .Var (.Field target fieldName) =>
     let targetErrors := validateDiamondFieldAccessesForStmtExpr model target
     let fieldError := match (computeExprType model target).val with
       | .UserDefined typeName =>
@@ -135,7 +136,19 @@ def validateDiamondFieldAccessesForStmtExpr (model : SemanticModel)
   | .Block stmts _ =>
     stmts.flatMap (fun s => validateDiamondFieldAccessesForStmtExpr model s)
   | .Assign targets value =>
-    let targetErrors := targets.attach.foldl (fun acc ⟨t, _⟩ => acc ++ validateDiamondFieldAccessesForStmtExpr model t) []
+    let targetErrors := targets.attach.foldl (fun acc ⟨t, _⟩ =>
+      match _hv : t.val with
+      | .Field target fieldName =>
+        let innerErrors := validateDiamondFieldAccessesForStmtExpr model target
+        let fieldError := match (computeExprType model target).val with
+          | .UserDefined typeName =>
+            if isDiamondInheritedField model typeName fieldName then
+              let fileRange := t.source.getD FileRange.unknown
+              [DiagnosticModel.withRange fileRange s!"fields that are inherited multiple times can not be accessed."]
+            else []
+          | _ => []
+        acc ++ innerErrors ++ fieldError
+      | .Local _ | .Declare _ => acc) []
     targetErrors ++ validateDiamondFieldAccessesForStmtExpr model value
   | .IfThenElse c t e =>
     let errs := validateDiamondFieldAccessesForStmtExpr model c ++
@@ -143,8 +156,6 @@ def validateDiamondFieldAccessesForStmtExpr (model : SemanticModel)
     match e with
     | some eb => errs ++ validateDiamondFieldAccessesForStmtExpr model eb
     | none => errs
-  | .LocalVariable _ _ (some init) =>
-    validateDiamondFieldAccessesForStmtExpr model init
   | .While c invs _ b =>
     let errs := validateDiamondFieldAccessesForStmtExpr model c ++
                 validateDiamondFieldAccessesForStmtExpr model b
@@ -161,9 +172,12 @@ def validateDiamondFieldAccessesForStmtExpr (model : SemanticModel)
   decreasing_by
     all_goals simp_wf
     all_goals (try have := AstNode.sizeOf_val_lt expr)
+    all_goals (try have := AstNode.sizeOf_val_lt t)
     all_goals (try have := Condition.sizeOf_condition_lt ‹_›)
     all_goals (try term_by_mem)
-    all_goals omega
+    all_goals (try omega)
+    -- For nested Variable.Field in Var (.Field ..) case
+    all_goals (cases expr; rename_i val _ _ _h; subst _h; simp_all; omega)
 
 /--
 Validate a Laurel program for diamond-inherited field accesses.
@@ -218,11 +232,11 @@ Lower `New name` to a block that:
 def lowerNew (name : Identifier) (source : Option FileRange) : THM StmtExprMd := do
   let heapVar : Identifier := "$heap"
   let freshVar ← freshVarName
-  let getCounter := mkMd (.StaticCall "Heap..nextReference!" [mkMd (.Identifier heapVar)])
-  let saveCounter := mkMd (.LocalVariable freshVar ⟨.TInt, none⟩ (some getCounter))
-  let newHeap := mkMd (.StaticCall "increment" [mkMd (.Identifier heapVar)])
-  let updateHeap := mkMd (.Assign [mkMd (.Identifier heapVar)] newHeap)
-  let compositeResult := mkMd (.StaticCall "MkComposite" [mkMd (.Identifier freshVar), mkMd (.StaticCall (name.text ++ "_TypeTag") [])])
+  let getCounter := mkMd (.StaticCall "Heap..nextReference!" [mkMd (.Var (.Local heapVar))])
+  let saveCounter := mkMd (.Assign [mkVarMd (.Declare ⟨freshVar, ⟨.TInt, none⟩⟩)] getCounter)
+  let newHeap := mkMd (.StaticCall "increment" [mkMd (.Var (.Local heapVar))])
+  let updateHeap := mkMd (.Assign [mkVarMd (.Local heapVar)] newHeap)
+  let compositeResult := mkMd (.StaticCall "MkComposite" [mkMd (.Var (.Local freshVar)), mkMd (.StaticCall (name.text ++ "_TypeTag") [])])
   return { val := .Block [saveCounter, updateHeap, compositeResult] none, source := source }
 
 /-- Local rewrite of `IsType` and `New` nodes. Recursion is handled by `mapStmtExprM`. -/
diff --git a/Strata/Languages/Python/PythonLaurelTypedExpr.lean b/Strata/Languages/Python/PythonLaurelTypedExpr.lean
index 5b5e9549ba..c2b27e09cd 100644
--- a/Strata/Languages/Python/PythonLaurelTypedExpr.lean
+++ b/Strata/Languages/Python/PythonLaurelTypedExpr.lean
@@ -48,7 +48,7 @@ def ofStmt {tp} (s : StmtExpr) (source : Option FileRange := none) : TypedStmtEx
 
 def identifier (v : String) (tp : HighType)
     (source : Option FileRange := none) : TypedStmtExpr tp :=
-  .ofStmt (.Identifier (mkId v)) source
+  .ofStmt (.Var (.Local (mkId v))) source
 
 def literalBool (v : Bool)
     (source : Option FileRange := none) : TypedStmtExpr .TBool :=
diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean
index 5336b929a1..feba2c106c 100644
--- a/Strata/Languages/Python/PythonToLaurel.lean
+++ b/Strata/Languages/Python/PythonToLaurel.lean
@@ -194,10 +194,31 @@ def mkCoreType (s: String): HighTypeMd :=
 def mkStmtExprMd (expr : StmtExpr) : StmtExprMd :=
   { val := expr, source := none }
 
+/-- Create a VariableMd with default metadata -/
+def mkVariableMd (v : Variable) : VariableMd :=
+  { val := v, source := none }
+
+/-- Extract a Variable from a StmtExpr, if it is a Var. -/
+def stmtExprToVar (e : StmtExprMd) : VariableMd :=
+  match e.val with
+  | .Var v => { val := v, source := e.source }
+  | _ => { val := .Local "BUG_invalid_var", source := e.source }
+
+/-- A wildcard modifies list, meaning the procedure may modify anything. -/
+def wildcardModifies : List StmtExprMd := [mkStmtExprMd .All]
+
 /-- Create a StmtExprMd with source location metadata. -/
 def mkStmtExprMdWithLoc (expr : StmtExpr) (source : Option FileRange) : StmtExprMd :=
   { val := expr, source := source }
 
+/-- Create a local variable declaration with initializer. -/
+def mkVarDeclInit (name : Identifier) (ty : AstNode HighType) (init : StmtExprMd) : StmtExprMd :=
+  mkStmtExprMd (.Assign [mkVariableMd (.Declare ⟨name, ty⟩)] init)
+
+/-- Create a local variable declaration with initializer and source location. -/
+def mkVarDeclInitWithLoc (name : Identifier) (ty : AstNode HighType) (init : StmtExprMd) (source : Option FileRange) : StmtExprMd :=
+  mkStmtExprMdWithLoc (.Assign [mkVariableMd (.Declare ⟨name, ty⟩)] init) source
+
 /-- Mangle a class name and method name into a flat procedure name: `ClassName@methodName`. -/
 def manglePythonMethod (className : String) (methodName : String) : String :=
   className ++ "@" ++ methodName
@@ -574,7 +595,7 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang
 
   -- Variable references
   | .Name _ name _ =>
-    return mkStmtExprMd (StmtExpr.Identifier name.val)
+    return mkStmtExprMd (StmtExpr.Var (.Local name.val))
 
   -- Binary operations
   | .BinOp _ left op right => do
@@ -661,9 +682,9 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang
           -- non-collision proof would require threading variable-scope info
           -- through the translator.
           let freshVar := s!"$cmp_tmp_{e.toAst.ann.start.byteIdx}_{i}"
-          let varDecl := mkStmtExprMd (StmtExpr.LocalVariable freshVar AnyTy (some comp))
+          let varDecl := mkVarDeclInit { text := freshVar } AnyTy comp
           tempDecls := tempDecls.push varDecl
-          operandRefs := operandRefs.push (mkStmtExprMd (StmtExpr.Identifier freshVar))
+          operandRefs := operandRefs.push (mkStmtExprMd (StmtExpr.Var (.Local { text := freshVar })))
         else
           operandRefs := operandRefs.push comp
       let ⟨hOpSize⟩ ← guardProp (p := operandRefs.size ≥ n + 1) "operandRefs size < n+1"
@@ -728,7 +749,7 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang
         let dict ← fields.foldlM (fun acc (fname, fty) =>
           return mkStmtExprMd (.StaticCall "DictStrAny_cons"
             [mkStmtExprMd (.LiteralString fname),
-             ← wrapFieldInAny fty (mkStmtExprMd (.FieldSelect inner fname)), acc]))
+             ← wrapFieldInAny fty (mkStmtExprMd (.Var (.Field inner fname))), acc]))
           (mkStmtExprMd (.StaticCall "DictStrAny_empty" []))
         pure <| mkStmtExprMd (.StaticCall "from_ClassInstance"
           [mkStmtExprMd (.LiteralString ty), dict])
@@ -804,9 +825,9 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang
     | .Name _ name _ =>
       if name.val == "self" && ctx.currentClassName.isSome then
         -- self.field in a method - field type is Any (builtins) or Composite (classes)
-        let fieldExpr := mkStmtExprMd (StmtExpr.FieldSelect
-          (mkStmtExprMd (StmtExpr.Identifier "self"))
-          attr.val)
+        let fieldExpr := mkStmtExprMd (StmtExpr.Var (.Field
+          (mkStmtExprMd (StmtExpr.Var (.Local "self")))
+          attr.val))
         let className := ctx.currentClassName.get!
         match tryLookupFieldHighType ctx className attr.val with
         | some (.UserDefined _) =>
@@ -829,7 +850,7 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang
       else
         -- Regular object.field access
         let objExpr ← translateExpr ctx obj
-        let fieldExpr := mkStmtExprMd (StmtExpr.FieldSelect objExpr attr.val)
+        let fieldExpr := mkStmtExprMd (StmtExpr.Var (.Field objExpr attr.val))
         let objType ← inferExprType ctx obj
         match tryLookupFieldHighType ctx objType attr.val with
           | some ty => wrapFieldInAny ty fieldExpr
@@ -837,7 +858,7 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang
     | _ =>
       -- Complex object expression - translate and access field
       let objExpr ← translateExpr ctx obj
-      let fieldExpr := mkStmtExprMd (StmtExpr.FieldSelect objExpr attr.val)
+      let fieldExpr := mkStmtExprMd (StmtExpr.Var (.Field objExpr attr.val))
       let objType ← inferExprType ctx obj
       match tryLookupFieldHighType ctx objType attr.val with
         | some ty => wrapFieldInAny ty fieldExpr
@@ -1121,7 +1142,7 @@ partial def translateExprAsReceiver (ctx : TranslationContext)
     match tryLookupFieldHighType ctx objType fieldAttr.val with
     | some (.UserDefined _) =>
       let objExpr ← translateExprAsReceiver ctx obj
-      pure <| mkStmtExprMd (StmtExpr.FieldSelect objExpr fieldAttr.val)
+      pure <| mkStmtExprMd (StmtExpr.Var (.Field objExpr fieldAttr.val))
     | _ => translateExpr ctx e
   | _ => translateExpr ctx e
 
@@ -1165,7 +1186,7 @@ partial def translateCall (ctx : TranslationContext)
       | .Attribute _ (.Name _ receiverName _) _ _ =>
         if receiverName.val ∈ ctx.variableTypes.unzip.1 then
           [mkStmtExprMd (StmtExpr.Assign
-            [mkStmtExprMd (StmtExpr.Identifier receiverName.val)]
+            [mkVariableMd (.Local receiverName.val)]
             (mkStmtExprMd .Hole))]
         else []
       | _ => []
@@ -1175,7 +1196,7 @@ partial def translateCall (ctx : TranslationContext)
         | some (varName, ty) =>
           if ty == PyLauType.Any then
             [mkStmtExprMd (StmtExpr.Assign
-              [mkStmtExprMd (StmtExpr.Identifier varName)]
+              [mkVariableMd (.Local varName)]
               (mkStmtExprMd (.Hole false none)))]
           else []
         | _ => []
@@ -1310,7 +1331,7 @@ def withException (ctx : TranslationContext) (funcname: String) : Bool :=
     | some sig => hasErrorOutput sig
     | none => false
 
-def freeVar (name: String) := mkStmtExprMd (.Identifier name)
+def freeVar (name: String) := mkStmtExprMd (.Var (.Local name))
 def maybeExceptVar := freeVar "maybe_except"
 def nullcall_var := freeVar "nullcall_ret"
 
@@ -1357,13 +1378,13 @@ partial def translateAssign  (ctx : TranslationContext)
   {
     let exceptHavoc :=
       if rhsIsCall then
-        [mkStmtExprMdWithLoc (StmtExpr.Assign [maybeExceptVar] (mkStmtExprMd (.Hole false none))) source]
+        [mkStmtExprMdWithLoc (StmtExpr.Assign [stmtExprToVar maybeExceptVar] (mkStmtExprMd (.Hole false none))) source]
       else []
     match lhs with
     | .Name _ n _ =>
       if n.val ∈ ctx.variableTypes.unzip.1 then
-        let targetExpr := mkStmtExprMd (StmtExpr.Identifier n.val)
-        return (ctx, [mkStmtExprMd (StmtExpr.Assign [targetExpr] rhs_trans)] ++ exceptHavoc, true)
+        let targetExpr := mkStmtExprMd (StmtExpr.Var (.Local n.val))
+        return (ctx, [mkStmtExprMd (StmtExpr.Assign [stmtExprToVar targetExpr] rhs_trans)] ++ exceptHavoc, true)
       else
         -- Use type annotation if it matches a known composite type
         let annType := annotation.map (fun a => pyExprToString a) |>.getD "Any"
@@ -1373,7 +1394,7 @@ partial def translateAssign  (ctx : TranslationContext)
           | some _ =>
             throw (.userPythonError lhs.ann s!"'{annType}' is not a type")
           | _ => pure (AnyTy, "Any")
-        let initStmt := mkStmtExprMd (StmtExpr.LocalVariable n.val varTy (mkStmtExprMd .Hole))
+        let initStmt := mkVarDeclInit n.val varTy (mkStmtExprMd .Hole)
         let newctx := {ctx with variableTypes:=(n.val, trackType)::ctx.variableTypes}
         return (newctx, [initStmt] ++ exceptHavoc, true)
     | _ => return (ctx, [mkStmtExprMd .Hole] ++ exceptHavoc, false)
@@ -1381,33 +1402,33 @@ partial def translateAssign  (ctx : TranslationContext)
   let mut newctx := ctx
   match lhs with
     | .Name _ n _ =>
-        let targetExpr := mkStmtExprMd (StmtExpr.Identifier n.val)
+        let targetExpr := mkStmtExprMd (StmtExpr.Var (.Local n.val))
         let assignStmts := match rhs_trans.val with
         | .StaticCall fnname args =>
             if let some (ImportedSymbol.compositeType laurelName) := ctx.importedSymbols[fnname.text]? then
               let resolvedId := mkId laurelName
               let newExpr := mkStmtExprMd (StmtExpr.New resolvedId)
               let varType := mkHighTypeMd (.UserDefined resolvedId)
-              let selfRef := mkStmtExprMd (StmtExpr.Identifier n.val)
+              let selfRef := mkStmtExprMd (StmtExpr.Var (.Local n.val))
               let initStmt := mkInstanceMethodCall laurelName "__init__" selfRef args source
               if n.val ∈ ctx.variableTypes.unzip.1 then
-                let assignStmt := mkStmtExprMdWithLoc (StmtExpr.Assign [targetExpr] newExpr) source
+                let assignStmt := mkStmtExprMdWithLoc (StmtExpr.Assign [stmtExprToVar targetExpr] newExpr) source
                 [assignStmt, initStmt]
               else
-                let newStmt := mkStmtExprMdWithLoc (StmtExpr.LocalVariable n.val varType (some newExpr)) source
+                let newStmt := mkVarDeclInitWithLoc n.val varType newExpr source
                 [newStmt, initStmt]
             else if withException ctx fnname.text then
-              [mkStmtExprMdWithLoc (StmtExpr.Assign [targetExpr, maybeExceptVar] rhs_trans) source]
+              [mkStmtExprMdWithLoc (StmtExpr.Assign [stmtExprToVar targetExpr, stmtExprToVar maybeExceptVar] rhs_trans) source]
             else
-                [mkStmtExprMdWithLoc (StmtExpr.Assign [targetExpr] rhs_trans) source]
+                [mkStmtExprMdWithLoc (StmtExpr.Assign [stmtExprToVar targetExpr] rhs_trans) source]
         | .New className =>
             if n.val ∈ ctx.variableTypes.unzip.1 then
-              [mkStmtExprMdWithLoc (StmtExpr.Assign [targetExpr] rhs_trans) source]
+              [mkStmtExprMdWithLoc (StmtExpr.Assign [stmtExprToVar targetExpr] rhs_trans) source]
             else
               let varType := mkHighTypeMd (.UserDefined className)
-              let newStmt := mkStmtExprMdWithLoc (StmtExpr.LocalVariable n.val varType (some rhs_trans)) source
+              let newStmt := mkVarDeclInitWithLoc n.val varType rhs_trans source
               [newStmt]
-        | _ => [mkStmtExprMdWithLoc (StmtExpr.Assign [targetExpr] rhs_trans) source]
+        | _ => [mkStmtExprMdWithLoc (StmtExpr.Assign [stmtExprToVar targetExpr] rhs_trans) source]
         newctx := match rhs_trans.val with
         | .StaticCall fnname _ =>
             if let some (ImportedSymbol.compositeType laurelName) := ctx.importedSymbols[fnname.text]? then
@@ -1427,7 +1448,7 @@ partial def translateAssign  (ctx : TranslationContext)
                -- If the annotation isn't a recognized type, prefer the
                -- inferred type from the RHS (e.g., overload dispatch).
                if isKnownType ctx annStr then annStr else inferType
-          let initStmt := mkStmtExprMd (StmtExpr.LocalVariable n.val AnyTy AnyNone)
+          let initStmt := mkVarDeclInit n.val AnyTy AnyNone
           newctx := {ctx with variableTypes:=(n.val, type)::ctx.variableTypes}
           return (newctx, initStmt :: assignStmts, true)
     | .Subscript _ _ _ _ =>
@@ -1437,7 +1458,7 @@ partial def translateAssign  (ctx : TranslationContext)
             let slices ← slices.mapM (translateExpr ctx)
             let source := sourceRangeToSource ctx.filePath lhs.toAst.ann
             let anySetsExpr := mkStmtExprMdWithLoc (StmtExpr.StaticCall "Any_sets!" [ListAny_mk slices, target, rhs_trans]) source
-            let assignStmts := [mkStmtExprMdWithLoc (StmtExpr.Assign [target] anySetsExpr) source]
+            let assignStmts := [mkStmtExprMdWithLoc (StmtExpr.Assign [stmtExprToVar target] anySetsExpr) source]
             return (ctx,assignStmts, false)
         | _ =>  throw (.internalError "Invalid Subscript Expr")
     | .Attribute _ obj attr _ =>
@@ -1445,9 +1466,9 @@ partial def translateAssign  (ctx : TranslationContext)
       | .Name _ name _ =>
         if name.val == "self" && ctx.currentClassName.isSome then
           -- self.field : type = value in a method
-          let fieldAccess := mkStmtExprMd (StmtExpr.FieldSelect
-            (mkStmtExprMd (StmtExpr.Identifier "self"))
-            attr.val)
+          let fieldAccess := mkStmtExprMd (StmtExpr.Var (.Field
+            (mkStmtExprMd (StmtExpr.Var (.Local "self")))
+            attr.val))
           -- When the annotation is a composite type, the RHS (which is Any)
           -- cannot be assigned directly; use New to initialize the field.
           let rhs' ← match annotation with
@@ -1457,11 +1478,11 @@ partial def translateAssign  (ctx : TranslationContext)
                 pure (mkStmtExprMd (StmtExpr.New (mkId laurelName)))
               else pure rhs_trans
             | none => pure rhs_trans
-          let assignStmt := mkStmtExprMdWithLoc (StmtExpr.Assign [fieldAccess] rhs') source
+          let assignStmt := mkStmtExprMdWithLoc (StmtExpr.Assign [stmtExprToVar fieldAccess] rhs') source
           return (ctx, [assignStmt], true)
         else
           let targetExpr ← translateExpr ctx lhs  -- This will handle self.field via translateExpr
-          let assignStmt := mkStmtExprMdWithLoc (StmtExpr.Assign [targetExpr] rhs_trans) source
+          let assignStmt := mkStmtExprMdWithLoc (StmtExpr.Assign [stmtExprToVar targetExpr] rhs_trans) source
           return (ctx, [assignStmt], true)
       | _ => throw (.unsupportedConstruct "Assignment targets not yet supported" (toString (repr lhs)))
     | _ => throw (.unsupportedConstruct "Assignment targets not yet supported" (toString (repr lhs)))
@@ -1531,7 +1552,7 @@ def createVarDeclStmtsAndCtx (ctx : TranslationContext) (newDecls : List (String
       then acc else acc ++ [(n, ty)]) []
   let hoistedDecls : List StmtExprMd ←  newDecls.mapM fun (name, tyStr) => do
       let ty ← translateType ctx tyStr
-      pure $ mkStmtExprMd (StmtExpr.LocalVariable (name : String) ty (some (mkStmtExprMd .Hole)))
+      pure $ mkVarDeclInit (name : String) ty (mkStmtExprMd .Hole)
   let hoistedCtx := { ctx with variableTypes := ctx.variableTypes ++
       (newDecls.map fun (n, ty) =>
         if isCompositeType ctx ty then (n, ty) else (n, PyLauType.Any)) }
@@ -1589,8 +1610,8 @@ def getExceptionCheckPreamble (ctx : TranslationContext) (e : StmtExprMd) (varNa
   if (getMaybeExceptionExprs ctx e).isEmpty then
     ([], e)
   else if containsUserCall ctx e then
-    let varDecl := mkStmtExprMd (StmtExpr.LocalVariable varName AnyTy (some e))
-    let varRef := mkStmtExprMd (StmtExpr.Identifier varName)
+    let varDecl := mkVarDeclInit varName AnyTy e
+    let varRef := mkStmtExprMd (StmtExpr.Var (.Local varName))
     ([varDecl, mkExceptionCheckAssert varRef "Check exception"], varRef)
   else
     (getExceptionAssertions ctx e, e)
@@ -1647,7 +1668,7 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
           let annStr := pyExprToString annotation
           match typeTester? annStr with
           | some testerName =>
-            let varExpr := mkStmtExprMd (StmtExpr.Identifier n.val)
+            let varExpr := mkStmtExprMd (StmtExpr.Var (.Local n.val))
             let cond := mkStmtExprMd (StmtExpr.StaticCall testerName [varExpr])
             [mkStmtExprMdWithLoc (StmtExpr.Assert { condition := cond }) md]
           | none => []
@@ -1661,7 +1682,7 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
           return (ctx, [])
       let newctx := {ctx with variableTypes:=(varName, varType)::ctx.variableTypes}
       let varType ← translateType ctx varType
-      let declStmt := mkStmtExprMd (StmtExpr.LocalVariable varName varType AnyNone)
+      let declStmt := mkVarDeclInit varName varType AnyNone
       return (newctx, [declStmt])
 
   -- If statement
@@ -1702,7 +1723,7 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
         let (preamble, eRef) := getExceptionCheckPreamble ctx e s!"$ret_exc_{expr.toAst.ann.start.byteIdx}"
         -- Coerce Composite return values to Any for LaurelResult : Any
         let eRef ← coerceToAny ctx expr eRef
-        let assign := mkStmtExprMdWithLoc (StmtExpr.Assign [mkStmtExprMd (StmtExpr.Identifier PyLauFuncReturnVar)] eRef) md
+        let assign := mkStmtExprMdWithLoc (StmtExpr.Assign [mkVariableMd (.Local PyLauFuncReturnVar)] eRef) md
         .ok $ preamble ++ [assign, mkStmtExprMdWithLoc (StmtExpr.Exit "$body") md]
       | none => .ok [mkStmtExprMdWithLoc (StmtExpr.Exit "$body") md]
     return (ctx, stmts)
@@ -1720,8 +1741,8 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
       | .Hole =>
         let freshVar := s!"assert_cond_{test.toAst.ann.start.byteIdx}"
         let varType := mkHighTypeMd .TBool
-        let varDecl := mkStmtExprMd (StmtExpr.LocalVariable freshVar varType (some condExpr))
-        let varRef := mkStmtExprMd (StmtExpr.Identifier freshVar)
+        let varDecl := mkVarDeclInit freshVar varType condExpr
+        let varRef := mkStmtExprMd (StmtExpr.Var (.Local freshVar))
         ([varDecl], varRef, { ctx with variableTypes := ctx.variableTypes ++ [(freshVar, "bool")] })
       | _ => ([], condExpr, ctx)
 
@@ -1750,7 +1771,7 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
     -- since an unmodeled call is a black box that could throw any exception.
     let holeExceptHavoc :=
       if let .Call _ _ _ _ := value then
-        [mkStmtExprMdWithLoc (StmtExpr.Assign [maybeExceptVar] (mkStmtExprMd (.Hole false none))) md]
+        [mkStmtExprMdWithLoc (StmtExpr.Assign [stmtExprToVar maybeExceptVar] (mkStmtExprMd (.Hole false none))) md]
       else []
     match expr.val with
     | .StaticCall fnname _ =>
@@ -1759,7 +1780,7 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
             let targets := if funsig.ret.isNone then [] else [nullcall_var]
             let targets := if withException ctx fnname.text then targets++[maybeExceptVar] else targets
             if targets.length > 0 then
-              return (ctx, exceptionCheck ++ [mkStmtExprMdWithLoc (StmtExpr.Assign targets expr) md])
+              return (ctx, exceptionCheck ++ [mkStmtExprMdWithLoc (StmtExpr.Assign (targets.map stmtExprToVar) expr) md])
             else
               return (ctx, exceptionCheck ++ [expr])
         | _ => return (ctx, exceptionCheck ++ [expr])
@@ -1791,7 +1812,7 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
     -- Insert exception checks after each statement in try body
     let bodyStmtsWithChecks := bodyStmts.flatMap fun stmt =>
       let isException := mkStmtExprMd (StmtExpr.StaticCall "isError"
-        [mkStmtExprMd (StmtExpr.Identifier "maybe_except")])
+        [mkStmtExprMd (StmtExpr.Var (.Local "maybe_except"))])
       let exitToHandler := mkStmtExprMd (StmtExpr.IfThenElse isException
         (mkStmtExprMd (StmtExpr.Exit catchersLabel)) none)
       [stmt, exitToHandler]
@@ -1829,8 +1850,8 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
         let mgrExpr ← translateExpr currentCtx ctxExpr
         let mgrTy ← inferExprType currentCtx ctxExpr
         let mgrLauTy ← translateType currentCtx mgrTy
-        let mgrDecl := mkStmtExprMd (StmtExpr.LocalVariable mgrName mgrLauTy (some mgrExpr))
-        let mgrRef := mkStmtExprMd (StmtExpr.Identifier mgrName)
+        let mgrDecl := mkVarDeclInit mgrName mgrLauTy mgrExpr
+        let mgrRef := mkStmtExprMd (StmtExpr.Var (.Local mgrName))
         currentCtx := {currentCtx with variableTypes := currentCtx.variableTypes ++ [(mgrName, mgrTy)]}
         let enterCall := mkInstanceMethodCall mgrTy "__enter__" mgrRef [] md
         let exitCall := mkInstanceMethodCall mgrTy "__exit__" mgrRef [] md
@@ -1839,11 +1860,11 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
           let varName := pyExprToString varExpr
           if varName ∈ currentCtx.variableTypes.unzip.fst then
             let assignStmt := mkStmtExprMd (StmtExpr.Assign
-              [mkStmtExprMd (StmtExpr.Identifier varName)] enterCall)
+              [mkVariableMd (.Local varName)] enterCall)
             setupStmts := setupStmts ++ [mgrDecl, assignStmt]
           else
             -- New variable — declare outside the block so it's visible after
-            let varDecl := mkStmtExprMd (StmtExpr.LocalVariable varName AnyTy (some enterCall))
+            let varDecl := mkVarDeclInit varName AnyTy enterCall
             currentCtx := {currentCtx with variableTypes := currentCtx.variableTypes ++ [(varName, PyLauType.Any)]}
             setupStmts := setupStmts ++ [mgrDecl, varDecl]
         | none =>
@@ -1878,8 +1899,8 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
     let (iterPreamble, iterExpr) := match iterRaw.val with
       | .Block (_ :: _ :: _) _ =>
         let varName := s!"$for_iter_{iter.toAst.ann.start.byteIdx}"
-        let varDecl := mkStmtExprMd (StmtExpr.LocalVariable varName AnyTy (some iterRaw))
-        let varRef  := mkStmtExprMd (StmtExpr.Identifier varName)
+        let varDecl := mkVarDeclInit varName AnyTy iterRaw
+        let varRef  := mkStmtExprMd (StmtExpr.Var (.Local varName))
         ([varDecl], varRef)
       | _ => ([], iterRaw)
     if let .Call _ (.Name _ {val:= "range",..} _) _ _  := iter then
@@ -1894,8 +1915,8 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
     let sr := target.ann
     let counterName := s!"@for_loop_counter_{s.toAst.ann.start.byteIdx}"
     let counterVar := freeVar counterName
-    let counterDecl := mkStmtExprMd $ .LocalVariable counterName (mkHighTypeMd $ .TInt) (mkStmtExprMd $ .LiteralInt 0)
-    let counterIncrease := mkStmtExprMd $ .Assign [counterVar] (mkStmtExprMd $ .PrimitiveOp .Add [counterVar, mkStmtExprMd $ .LiteralInt 1])
+    let counterDecl := mkVarDeclInit counterName (mkHighTypeMd $ .TInt) (mkStmtExprMd $ .LiteralInt 0)
+    let counterIncrease := mkStmtExprMd $ .Assign [stmtExprToVar counterVar] (mkStmtExprMd $ .PrimitiveOp .Add [counterVar, mkStmtExprMd $ .LiteralInt 1])
     let indexRhs := expr.Call sr (.Name sr {val:= "Any_iter_index", ann:= sr} default)
                         {val:= #[iter, .Name sr {val:= counterName, ann:= sr} default], ann:= sr} {val:= #[], ann:= sr}
     -- Any_iter_index is defined in PythonRuntimeLaurelPart, so indexRhs would be translated into .StaticCall "Any_iter_index" ..., hot .Hole
@@ -1907,7 +1928,7 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
     let (finalCtx, bodyStmts) ← translateStmtList bodyCtx body.val.toList
     let assumeStmts : List StmtExprMd ← do match target with
       | .Name _ n _ =>
-        let targetVar := mkStmtExprMd (StmtExpr.Identifier n.val)
+        let targetVar := mkStmtExprMd (StmtExpr.Var (.Local n.val))
         let isAnyNone (s: StmtExprMd) := match s.val with
           | .StaticCall constructor _ => constructor == AnyConstructor.None | _ => false
         match iterExpr.val with
@@ -1969,7 +1990,7 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
       | _ => (target, [], [])
     let slices ← slices.mapM (translateExpr ctx)
     let tempVarDecls := (tempVars.zip slices).map λ (var, slice) =>
-              mkStmtExprMd (.LocalVariable { text := var } AnyTy slice)
+              mkVarDeclInit { text := var } AnyTy slice
     let rhs : Python.expr SourceRange := .BinOp sr target op value
     let pyNormalAssign : Python.stmt SourceRange :=
           .Assign sr {val:= #[target], ann:= target.ann} rhs {val:= none, ann:= sr}
@@ -1991,7 +2012,7 @@ partial def translateStmtList (ctx : TranslationContext) (stmts : List (Python.s
 end
 
 def prependExceptHandlingHelper (l: List StmtExprMd) : List StmtExprMd :=
-  mkStmtExprMd (.LocalVariable "maybe_except" (mkCoreType "Error") (some NoError)) :: l
+  mkVarDeclInit "maybe_except" (mkCoreType "Error") NoError :: l
 
 partial def getNestedSubscripts (expr:  Python.expr SourceRange) : List ( Python.expr SourceRange) :=
   match expr with
@@ -2149,8 +2170,8 @@ def renameInputParams (inputs : List Parameter) (exclude : String → Bool := fu
   let copies := inputs.filter (fun p => !exclude p.name.text) |>.map fun p =>
     let orig : String := p.name.text
     let prefixed : String := paramInputPrefix ++ orig
-    mkStmtExprMd (StmtExpr.LocalVariable (mkId orig) p.type
-      (some (mkStmtExprMd (StmtExpr.Identifier prefixed))))
+    mkVarDeclInit (mkId orig) p.type
+      (mkStmtExprMd (StmtExpr.Var (.Local prefixed)))
   (renamed, copies)
 
 /-- Translate a Python function body: collect all variable declarations, hoist them
@@ -2164,9 +2185,9 @@ def translateFunctionBody (ctx : TranslationContext) (kwargsName : Option String
     let nonSelfParams := inputs.filter (fun p => p.name.text != "self")
     let (_, paramCopies) := renameInputParams nonSelfParams
       (match kwargsName with | some kw => (· == kw) | none => fun _ => false)
-    let noneReturn := mkStmtExprMd (.Assign [mkStmtExprMd (.Identifier PyLauFuncReturnVar)] AnyNone)
+    let noneReturn := mkStmtExprMd (.Assign [mkVariableMd (.Local PyLauFuncReturnVar)] AnyNone)
     let bodyStmts := noneReturn::paramCopies ++ bodyStmts
-    let bodyStmts := (mkStmtExprMd (.LocalVariable "nullcall_ret" AnyTy (some AnyNone))) :: bodyStmts
+    let bodyStmts := (mkStmtExprMd (.Assign [mkVariableMd $ .Declare ⟨ "nullcall_ret", AnyTy⟩] AnyNone)) :: bodyStmts
     return (mkStmtExprMd (StmtExpr.Block bodyStmts none), newctx)
 
 /-- Translate Python function to Laurel Procedure -/
@@ -2216,27 +2237,24 @@ def translateFunction (ctx : TranslationContext) (sourceRange: SourceRange) (fun
     let ctx := match ctx.currentClassName with
       | some cn => {ctx with variableTypes := ("self", cn) :: ctx.variableTypes}
       | none => ctx
-    let (bodyTrans, newCtx) ← match body with
+    let (body, newCtx) ← match body with
     | some body =>
         let (bodyBlock, newCtx) ←  translateFunctionBody ctx funcDecl.kwargsName inputs body
-        if typeConstraintPostcondition.isEmpty then
-            pure $ (Body.Transparent bodyBlock, newCtx)
-        else
-            pure $ (Body.Opaque typeConstraintPostcondition bodyBlock [], newCtx)
+        pure $ (Body.Opaque typeConstraintPostcondition bodyBlock wildcardModifies, newCtx)
     | _ =>  pure $ (Body.Opaque [] none [], ctx)
 
     let renamedInputs := inputs.map fun p =>
       if p.name.text == "self" then p
       else { p with name := mkId ("$in_" ++ p.name.text) }
 
-    -- Create procedure with transparent body (no contracts for now)
+    -- Create procedure
     let proc : Procedure := {
       name := { text := funcDecl.name, source := sourceRangeToSource ctx.filePath sourceRange }
       inputs := renamedInputs
       outputs := outputs
       preconditions := typeConstraintPreconditions
       decreases := none
-      body := bodyTrans
+      body := body
       isFunctional := false
     }
 
@@ -2417,7 +2435,7 @@ def mkDefaultInitDecl (className : String) : PythonFunctionDecl × Procedure :=
     preconditions := [{ condition := mkStmtExprMd (StmtExpr.LiteralBool true) }]
     isFunctional := false
     decreases := none
-    body := .Opaque [] .none []
+    body := .Opaque [] .none wildcardModifies
   }
   (decl, proc)
 
@@ -2561,7 +2579,7 @@ structure PreludeInfo where
   maybeExceptionFunctions : List String := []
   /-- Procedure names (non-function callables) -/
   procedureNames : List String := []
-  /-- Names of procedures with transparent bodies (can be inlined). -/
+  /-- Names of procedures that should generate calls (have transparent bodies or preconditions). -/
   inlinableProcedures : Std.HashSet String := {}
   /-- Maps Python-visible names to their structured symbol info.
       Includes both canonical Laurel names and unprefixed aliases. -/
@@ -2615,7 +2633,7 @@ def PreludeInfo.ofLaurelProgram (prog : Laurel.Program) : PreludeInfo where
         -- Use "Any" for all parameter types to match the Python→Laurel
         -- pipeline's Any-wrapping convention at call sites.
         let ins := p.inputs.map fun _ => "Any"
-        let outs := p.outputs.map fun _ => "Any"
+        let outs := p.outputs.map fun param => getHighTypeName param.type.val
         m.insert p.name.text { inputs := ins, outputs := outs }
   functionSignatures :=
     prog.staticProcedures.filterMap fun p =>
@@ -2654,7 +2672,10 @@ def PreludeInfo.ofLaurelProgram (prog : Laurel.Program) : PreludeInfo where
       if p.body.isExternal || p.isFunctional then none else some p.name.text
   inlinableProcedures :=
     prog.staticProcedures.foldl (init := {}) fun s p =>
-      if p.body.isTransparent then s.insert p.name.text else s
+      match p.body with
+      | .Transparent _ => s.insert p.name.text
+      | .Opaque _ (some _) _ => s.insert p.name.text
+      | _ => if !p.preconditions.isEmpty then s.insert p.name.text else s
 
 /-- Merge two `PreludeInfo` values by concatenating each field. -/
 def PreludeInfo.merge (a b : PreludeInfo) : PreludeInfo where
@@ -2834,7 +2855,7 @@ def pythonToLaurel (info : PreludeInfo)
     outputs := [{ name := PyLauFuncReturnVar, type := AnyTy }],
     preconditions := [],
     decreases := none,
-    body := .Transparent bodyBlock
+    body := .Opaque [] (some bodyBlock) wildcardModifies
     isFunctional := false
   }
 
@@ -2853,7 +2874,7 @@ def pythonToLaurel (info : PreludeInfo)
         outputs := [{ name := "result", type := mkHighTypeMd .TString }]
         preconditions := []
         decreases := none
-        body := .Opaque [] none []
+        body := .Opaque [] none wildcardModifies
         isFunctional := false }
     procedures := procedures.push
       { name := { text := compositeToStringAnyName ct.name.text }
@@ -2861,7 +2882,7 @@ def pythonToLaurel (info : PreludeInfo)
         outputs := [{ name := "result", type := AnyTy }]
         preconditions := []
         decreases := none
-        body := .Opaque [] none []
+        body := .Opaque [] none wildcardModifies
         isFunctional := false }
 
   let program : Laurel.Program := {
diff --git a/Strata/Languages/Python/Specs/ToLaurel.lean b/Strata/Languages/Python/Specs/ToLaurel.lean
index 217a5fd053..da75cc4076 100644
--- a/Strata/Languages/Python/Specs/ToLaurel.lean
+++ b/Strata/Languages/Python/Specs/ToLaurel.lean
@@ -419,12 +419,12 @@ def buildSpecBody (allArgs : Array Arg)
   let mut stmts : Array StmtExprMd := #[]
   -- 1. Havoc the result: result := Hole(nondet)
   let holeExpr : StmtExprMd := { val := .Hole (deterministic := false), source := source }
-  let resultId : StmtExprMd := { val := .Identifier (mkId "result"), source := source }
+  let resultId : AstNode Variable := { val := Variable.Local (mkId "result"), source := source }
   let assignStmt ← mkStmtWithLoc (.Assign [resultId] holeExpr) default
   stmts := stmts.push assignStmt
   -- 2. Assert type / required-param preconditions
   for arg in allArgs do
-    let paramId : StmtExprMd := { val := .Identifier (mkId arg.name), source := source }
+    let paramId : StmtExprMd := { val := .Var $ Variable.Local (mkId arg.name), source := source }
     match ← typeAssertion? arg.type paramId source with
     | some assertion =>
       if arg.default.isSome then
@@ -471,7 +471,7 @@ def buildSpecBody (allArgs : Array Arg)
   -- NOTE. Skip NoneType: generated stubs currently declare `-> None` even for methods
   -- that return values. Assuming isfrom_None would make callers unreachable.
   if returnType.asIdent != some .noneType then
-    let resultRef : StmtExprMd := { val := .Identifier (mkId "result"), source := source }
+    let resultRef : StmtExprMd := { val := .Var $ Variable.Local (mkId "result"), source := source }
     if let some retAssertion ← typeAssertion? returnType resultRef source then
       let assumeStmt ← mkStmtWithLoc (.Assume retAssertion) default
       stmts := stmts.push assumeStmt
@@ -479,7 +479,7 @@ def buildSpecBody (allArgs : Array Arg)
       val := .Block stmts.toList none,
       source := fileSource
   }
-  return .Transparent body
+  return .Opaque [] (some body) [{ val := .All, source := none }]
 
 /-! ## Declaration Translation -/
 
diff --git a/StrataMain.lean b/StrataMain.lean
index 8061b77a49..84fa1a8b95 100644
--- a/StrataMain.lean
+++ b/StrataMain.lean
@@ -1345,7 +1345,8 @@ def pyInterpretCommand : Command where
         IO.Process.exit ExitCode.userError
     match core.run with
     | .ok E =>
-      let outputNames := match Core.Program.Procedure.find? core ⟨"__main__", ()⟩ with
+      let mainProc := Core.Program.Procedure.find? core ⟨"__main__", ()⟩
+      let outputNames := match mainProc with
         | some p => p.header.outputs.keys.map (·.name)
         | none => []
       let (lhs, exprEnv) := Core.Env.genVars outputNames E.exprEnv
diff --git a/StrataTest/Backends/CBMC/GOTO/test_property_summary_e2e.sh b/StrataTest/Backends/CBMC/GOTO/test_property_summary_e2e.sh
index 5e3252b5c3..47b1871cdc 100755
--- a/StrataTest/Backends/CBMC/GOTO/test_property_summary_e2e.sh
+++ b/StrataTest/Backends/CBMC/GOTO/test_property_summary_e2e.sh
@@ -15,7 +15,9 @@ trap 'rm -rf "$WORK"' EXIT
 
 # Create Laurel program with property summaries
 cat > "$WORK/test.lr.st" << 'LAUREL'
-procedure main() {
+procedure main()
+  opaque
+{
     var x: int := 5;
     var y: int := 3;
     assert x + y == 8 summary "addition equals eight";
diff --git a/StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean b/StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean
index de6cf5a807..40e8a9112d 100644
--- a/StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean
+++ b/StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean
@@ -19,7 +19,9 @@ generates verification conditions for these preconditions.
 -/
 
 def e2eProgram := r"
-procedure safeDivision() {
+procedure safeDivision()
+  opaque
+{
   var x: int := 10;
   var y: int := 2;
   var z: int := x / y;
@@ -27,7 +29,9 @@ procedure safeDivision() {
 };
 
 // Error ranges are too wide because Core does not use expression locations
-procedure unsafeDivision(x: int) {
+procedure unsafeDivision(x: int)
+  opaque
+{
   var z: int := 10 / x
 //^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
 // Error ranges are too wide because Core does not use expression locations
@@ -39,12 +43,16 @@ function pureDiv(x: int, y: int): int
   x / y
 };
 
-procedure callPureDivSafe() {
+procedure callPureDivSafe()
+  opaque
+{
   var z: int := pureDiv(10, 2);
   assert z == 5
 };
 
-procedure callPureDivUnsafe(x: int) {
+procedure callPureDivUnsafe(x: int)
+  opaque
+{
   var z: int := pureDiv(10, x)
 //^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
 // Error ranges are too wide because Core does not use expression locations
diff --git a/StrataTest/Languages/Laurel/DuplicateNameTests.lean b/StrataTest/Languages/Laurel/DuplicateNameTests.lean
index b948859925..beb1a06737 100644
--- a/StrataTest/Languages/Laurel/DuplicateNameTests.lean
+++ b/StrataTest/Languages/Laurel/DuplicateNameTests.lean
@@ -37,8 +37,8 @@ private def processResolution (input : Lean.Parser.InputContext) : IO (Array Dia
 /-! ## Duplicate static procedure names -/
 
 def dupProcedures := r"
-procedure foo() { };
-procedure foo() { };
+procedure foo() opaque { };
+procedure foo() opaque { };
 //        ^^^ error: Duplicate definition 'foo' is already defined in this scope
 "
 
@@ -72,7 +72,7 @@ composite Foo {
 /-! ## Duplicate parameter names in a procedure -/
 
 def dupParams := r"
-procedure foo(x: int, x: bool) { };
+procedure foo(x: int, x: bool) opaque { };
 //                    ^ error: Duplicate definition 'x' is already defined in this scope
 "
 
@@ -83,8 +83,8 @@ procedure foo(x: int, x: bool) { };
 
 def dupInstanceProcs := r"
 composite Foo {
-  procedure bar() { };
-  procedure bar() { };
+  procedure bar() opaque { };
+  procedure bar() opaque { };
 //          ^^^ error: Duplicate definition 'bar' is already defined in this scope
 }
 "
@@ -95,7 +95,7 @@ composite Foo {
 /-! ## Duplicate local variable names in the same block -/
 
 def dupLocals := r"
-procedure foo() {
+procedure foo() opaque {
   var x: int := 1;
   var x: int := 2
 //    ^ error: Duplicate definition 'x' is already defined in this scope
@@ -109,7 +109,7 @@ procedure foo() {
 
 def dupProcType := r"
 composite Foo { }
-procedure Foo() { };
+procedure Foo() opaque { };
 //        ^^^ error: Duplicate definition 'Foo' is already defined in this scope
 "
 
@@ -119,7 +119,7 @@ procedure Foo() { };
 /-! ## Shadowing quantifier variables in nested scopes is OK (no error expected) -/
 
 def shadowQuantifierVars := r"
-procedure test() {
+procedure test() opaque {
   assert forall(x: int) => forall(x: int) => x > 0
 };
 "
@@ -130,7 +130,7 @@ procedure test() {
 /-! ## Shadowing in nested blocks is OK (no error expected) -/
 
 def shadowingOk := r"
-procedure foo() {
+procedure foo() opaque {
   var x: int := 1;
   {
     var x: int := 2
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypes.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypes.lean
index 291f669064..80d21eb4d6 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypes.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypes.lean
@@ -17,56 +17,76 @@ constrained nat = x: int where x >= 0 witness 0
 constrained posnat = x: nat where x != 0 witness 1
 
 // Input constraint becomes requires — body can rely on it
-procedure inputAssumed(n: nat) {
+procedure inputAssumed(n: nat)
+  opaque
+{
   assert n >= 0
 };
 
 // Output constraint — valid return passes
-procedure outputValid(): nat {
+procedure outputValid(): nat
+  opaque
+{
   return 3
 };
 
 // Output constraint — invalid return fails
-procedure outputInvalid(): nat {
+procedure outputInvalid(): nat
 //                         ^^^ error: assertion does not hold
+  opaque
+{
   return -1
 };
 
 // Return value of constrained type — caller gets ensures via call elimination
 procedure opaqueNat(): nat;
-procedure callerAssumes() returns (r: int) {
+procedure callerAssumes() returns (r: int)
+  opaque
+{
   var x: int := opaqueNat();
   assert x >= 0;
   return x
 };
 
 // Assignment to constrained-typed variable — valid
-procedure assignValid() {
+procedure assignValid()
+  opaque
+{
   var y: nat := 5
 };
 
 // Assignment to constrained-typed variable — invalid
-procedure assignInvalid() {
+procedure assignInvalid()
+  opaque
+{
   var y: nat := -1
 //^^^^^^^^^^^^^^^^ error: assertion does not hold
 };
 
 // Reassignment to constrained-typed variable — invalid
-procedure reassignInvalid() {
+procedure reassignInvalid()
+  opaque
+{
   var y: nat := 5;
   y := -1
 //^^^^^^^ error: assertion does not hold
 };
 
 // Argument to constrained-typed parameter — valid
-procedure takesNat(n: nat) returns (r: int) { return n };
-procedure argValid() returns (r: int) {
+procedure takesNat(n: nat) returns (r: int)
+  opaque
+{ return n };
+procedure argValid() returns (r: int)
+  opaque
+{
   var x: int := takesNat(3);
   return x
 };
 
 // Argument to constrained-typed parameter — invalid (requires violation)
-procedure argInvalid() returns (r: int) {
+procedure argInvalid() returns (r: int)
+  opaque
+{
   var x: int := takesNat(-1);
 //^^^^^^^^^^^^^^^^^^^^^^^^^^ error: precondition does not hold
   return x
@@ -75,26 +95,34 @@ procedure argInvalid() returns (r: int) {
 // Nested constrained type — independent constraints require transitive collection
 constrained even = x: int where x % 2 == 0 witness 0
 constrained evenpos = x: even where x > 0 witness 2
-procedure nestedInput(x: evenpos) {
+procedure nestedInput(x: evenpos)
+  opaque
+{
   assert x > 0;
   assert x % 2 == 0
 };
 
 // Multiple constrained-typed parameters
-procedure multiParam(a: nat, b: nat) {
+procedure multiParam(a: nat, b: nat)
+  opaque
+{
   assert a >= 0;
   assert b >= 0
 };
 
 // Two calls to same procedure — no temp var collision
-procedure twoCalls() returns (r: int) {
+procedure twoCalls() returns (r: int)
+  opaque
+{
   var a: int := takesNat(1);
   var b: int := takesNat(2);
   return a + b
 };
 
 // Constrained type in expression position must be resolved
-procedure constrainedInExpr() {
+procedure constrainedInExpr()
+  opaque
+{
   var b: bool := forall(n: nat) => n + 1 > n;
   assert b
 };
@@ -104,42 +132,36 @@ constrained bad = x: int where x > 0 witness -1
 //                                           ^^ error: assertion does not hold
 
 // Uninitialized constrained variable — havoc + assume constraint
-procedure uninitNat() {
+procedure uninitNat()
+  opaque
+{
   var y: nat;
   assert y >= 0
 };
 
 // Uninitialized nested constrained variable — havoc + assume constraint
-procedure uninitPosnat() {
+procedure uninitPosnat()
+  opaque
+{
   var y: posnat;
   assert y != 0;
   assert y >= 0
 };
 
 // Uninitialized constrained variable — witness value is not provable
-procedure uninitNotWitness() {
+procedure uninitNotWitness()
+  opaque
+{
   var y: posnat;
   assert y == 1
 //^^^^^^^^^^^^^ error: assertion does not hold
 };
 
-// Function with valid constrained return — constraint not checked (not yet supported)
-function goodFunc(): nat { 3 };
-//       ^^^^^^^^ error: constrained return types on functions are not yet supported
-
-// Function with invalid constrained return — constraint not checked (not yet supported)
-function badFunc(): nat { -1 };
-//       ^^^^^^^ error: constrained return types on functions are not yet supported
-
-// Caller of constrained function — body is inlined, caller sees actual value
-procedure callerGood() {
-  var x: int := goodFunc();
-  assert x >= 0
-};
-
 // Quantifier constraint injection — forall
 // n + 1 > 0 is only provable with n >= 0 injected; false for all int
-procedure forallNat() {
+procedure forallNat()
+  opaque
+{
   var b: bool := forall(n: nat) => n + 1 > 0;
   assert b
 };
@@ -147,14 +169,18 @@ procedure forallNat() {
 // Quantifier constraint injection — exists
 // n == -1 is satisfiable for int, but not when n >= 0 is required
 // n == 42 works because 42 >= 0
-procedure existsNat() {
+procedure existsNat()
+  opaque
+{
   var b: bool := exists(n: nat) => n == 42;
   assert b
 };
 
 // Quantifier constraint injection — nested constrained type
 // n - 1 >= 0 is only provable with n > 0 injected
-procedure forallPosnat() {
+procedure forallPosnat()
+  opaque
+{
   var b: bool := forall(n: posnat) => n - 1 >= 0;
   assert b
 };
@@ -162,7 +188,9 @@ procedure forallPosnat() {
 // Capture avoidance — bound var y in constraint must not collide with parameter y
 // Without capture avoidance, requires becomes exists(y) => y > y (false), making body vacuously true
 constrained haslarger = x: int where (exists(y: int) => y > x) witness 0
-procedure captureTest(y: haslarger) {
+procedure captureTest(y: haslarger)
+  opaque
+{
   assert false
 //^^^^^^^^^^^^ error: assertion does not hold
 };
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypesError.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypesError.lean
new file mode 100644
index 0000000000..342b6b144d
--- /dev/null
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypesError.lean
@@ -0,0 +1,39 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import StrataTest.Util.TestDiagnostics
+import StrataTest.Languages.Laurel.TestExamples
+
+open StrataTest.Util
+
+namespace Strata
+namespace Laurel
+
+def program := r"
+constrained nat = x: int where x >= 0 witness 0
+
+// Function with valid constrained return — constraint not checked (not yet supported)
+function goodFunc(): nat { 3 };
+//       ^^^^^^^^ error: constrained return types on functions are not yet supported
+
+// Function with invalid constrained return — constraint not checked (not yet supported)
+function badFunc(): nat { -1 };
+//       ^^^^^^^ error: constrained return types on functions are not yet supported
+
+// Caller of constrained function — body is inlined, caller sees actual value
+procedure callerGood()
+  opaque
+{
+  var x: int := goodFunc();
+  assert x >= 0
+};
+"
+
+#guard_msgs(drop info, error) in
+#eval testInputWithOffset "ConstrainedTypes" program 14 processLaurelFile
+
+end Laurel
+end Strata
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T12_Operators.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T12_Operators.lean
index d8a2e9374f..b33450c145 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T12_Operators.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T12_Operators.lean
@@ -13,7 +13,9 @@ namespace Strata
 namespace Laurel
 
 def operatorsProgram := r"
-procedure testArithmetic() {
+procedure testArithmetic()
+  opaque
+{
     var a: int := 10;
     var b: int := 3;
     var x: int := a - b;
@@ -26,7 +28,9 @@ procedure testArithmetic() {
     assert r == 2
 };
 
-procedure testLogical() {
+procedure testLogical()
+  opaque
+{
     var t: bool := true;
     var f: bool := false;
     var a: bool := t && f;
@@ -39,13 +43,17 @@ procedure testLogical() {
     assert f ==> t
 };
 
-procedure testUnary() {
+procedure testUnary()
+  opaque
+{
     var x: int := 5;
     var y: int := -x;
     assert y == 0 - 5
 };
 
-procedure testTruncatingDiv() {
+procedure testTruncatingDiv()
+  opaque
+{
     assert 7 /t 3 == 2;
     assert 7 %t 3 == 1;
     assert (0 - 7) /t 3 == 0 - 2;
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T13_WhileLoops.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T13_WhileLoops.lean
index 9e6b2d195e..b6b0b2e178 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T13_WhileLoops.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T13_WhileLoops.lean
@@ -13,7 +13,9 @@ namespace Strata
 namespace Laurel
 
 def whileLoopsProgram := r"
-procedure countDown() {
+procedure countDown()
+  opaque
+{
     var i: int := 3;
     while(i > 0)
       invariant i >= 0
@@ -23,7 +25,9 @@ procedure countDown() {
     assert i == 0
 };
 
-procedure countUp() {
+procedure countUp()
+  opaque
+{
     var n: int := 5;
     var i: int := 0;
     while(i < n)
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T14_Quantifiers.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T14_Quantifiers.lean
index 271e3a4371..c60edd889c 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T14_Quantifiers.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T14_Quantifiers.lean
@@ -13,11 +13,15 @@ namespace Strata
 namespace Laurel
 
 def quantifiersProgram := r"
-procedure testForall() {
+procedure testForall()
+  opaque
+{
     assert forall(x: int) => x + 0 == x
 };
 
-procedure testExists() {
+procedure testExists()
+  opaque
+{
     assert exists(x: int) => x == 42
 };
 
@@ -30,7 +34,9 @@ procedure testQuantifierInContract(n: int)
 
 function P(x: int): int;
 function Q(): int;
-procedure triggers() {
+procedure triggers()
+  opaque
+{
   assert forall(i: int) { P(i) } => P(i) == i + 1;
 //^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
   assert forall(i: int) => true;
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T15_ShortCircuit.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T15_ShortCircuit.lean
index 2559e95b2d..2e5b46a8ab 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T15_ShortCircuit.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T15_ShortCircuit.lean
@@ -19,54 +19,73 @@ function mustNotCallFunc(x: int): int
 
 procedure mustNotCallProc(): int
   requires false
+  opaque
 {
   return 0
 };
 
 // Pure path: function with requires false
 
-procedure testAndThenFunc() {
+procedure testAndThenFunc()
+  opaque
+{
   var b: bool := false && mustNotCallFunc(0) > 0;
   assert !b
 };
 
-procedure testOrElseFunc() {
+procedure testOrElseFunc()
+  opaque
+{
   var b: bool := true || mustNotCallFunc(0) > 0;
   assert b
 };
 
-procedure testImpliesFunc() {
+procedure testImpliesFunc()
+  opaque
+{
   var b: bool := false ==> mustNotCallFunc(0) > 0;
   assert b
 };
 
 // Pure path: division by zero
 
-procedure testAndThenDivByZero() {
+procedure testAndThenDivByZero()
+  opaque
+{
   assert !(false && 1 / 0 > 0)
 };
 
-procedure testOrElseDivByZero() {
+procedure testOrElseDivByZero()
+  opaque
+{
   assert true || 1 / 0 > 0
 };
 
-procedure testImpliesDivByZero() {
+procedure testImpliesDivByZero()
+  opaque
+{
   assert false ==> 1 / 0 > 0
 };
 
 // Imperative path: procedure with requires false
 
-procedure testAndThenProc() {
+procedure testAndThenProc()
+  opaque
+{
   var b: bool := false && mustNotCallProc() > 0;
   assert !b
 };
 
-procedure testOrElseProc() {
+procedure testOrElseProc()
+  opaque
+{
   var b: bool := true || mustNotCallProc() > 0;
   assert b
 };
 
-procedure testImpliesProc() {
+procedure testImpliesProc()
+  opaque
+{
   var b: bool := false ==> mustNotCallProc() > 0;
   assert b
 };
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T16_PropertySummary.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T16_PropertySummary.lean
index 67d2f109d3..b9d25ce265 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T16_PropertySummary.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T16_PropertySummary.lean
@@ -16,13 +16,16 @@ def program := r#"
 procedure divide(x: int, y: int) returns (result: int)
   requires y != 0 summary "divisor is non-zero"
 // Call elimination reports precondition errors at the call site.
+  opaque
 {
   assert y == 0 summary "divisor is zero";
 //^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: divisor is zero does not hold
   return x
 };
 
-procedure checkPositive(n: int) returns (ok: bool) {
+procedure checkPositive(n: int) returns (ok: bool)
+  opaque
+{
   var x: int := divide(3, 0)
 //^^^^^^^^^^^^^^^^^^^^^^^^^^ error: divisor is non-zero does not hold
 };
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T17_ForLoop.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T17_ForLoop.lean
index 9710af32c7..9e0276a960 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T17_ForLoop.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T17_ForLoop.lean
@@ -13,7 +13,9 @@ namespace Strata
 namespace Laurel
 
 def forLoopProgram := r"
-procedure sumToThree() {
+procedure sumToThree()
+  opaque
+{
   var sum: int := 0;
   for (var i: int := 0; i < 3; i := i + 1)
     invariant sum >= 0
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T18_RecursiveFunction.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T18_RecursiveFunction.lean
index a0325e7c1b..23da15a520 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T18_RecursiveFunction.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T18_RecursiveFunction.lean
@@ -27,7 +27,9 @@ function listLen(xs: IntList): int {
   else 1 + listLen(IntList..tail!(xs))
 };
 
-procedure testListLen() {
+procedure testListLen()
+  opaque
+{
   var xs: IntList := Cons(1, Cons(2, Nil()));
   assert listLen(xs) == 2
 };
@@ -43,7 +45,9 @@ function listLenOdd(xs: IntList): bool {
   else listLenEven(IntList..tail!(xs))
 };
 
-procedure testMutualRecursion() {
+procedure testMutualRecursion()
+  opaque
+{
   var xs: IntList := Cons(1, Cons(2, Nil()));
   assert listLenEven(xs) == true
 };
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_BitvectorTypes.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_BitvectorTypes.lean
index 1e814bd74f..dec53e08a4 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_BitvectorTypes.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_BitvectorTypes.lean
@@ -16,28 +16,38 @@ def bvProgram := r"
 // Bitvector types in procedure signatures and variable declarations.
 
 // Parameters and return types
-procedure identity32(x: bv 32) returns (r: bv 32) {
+procedure identity32(x: bv 32) returns (r: bv 32)
+  opaque
+{
   r := x
 };
 
-procedure identity8(x: bv 8) returns (r: bv 8) {
+procedure identity8(x: bv 8) returns (r: bv 8)
+  opaque
+{
   r := x
 };
 
 // Local variable with bv type
-procedure localBv() returns (r: bv 16) {
+procedure localBv() returns (r: bv 16)
+  opaque
+{
   var x: bv 16 := r;
   r := x
 };
 
 // Opaque procedure returning bv64 — caller gets typed result
 procedure opaqueBv64() returns (r: bv 64);
-procedure callOpaque() returns (r: bv 64) {
+procedure callOpaque() returns (r: bv 64)
+  opaque
+{
   r := opaqueBv64()
 };
 
 // Mixed bv and int parameters
-procedure mixedTypes(a: bv 32, b: int) returns (r: int) {
+procedure mixedTypes(a: bv 32, b: int) returns (r: int)
+  opaque
+{
   r := b
 };
 "
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_InvokeOn.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_InvokeOn.lean
index cb323622bb..522859d197 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_InvokeOn.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_InvokeOn.lean
@@ -31,11 +31,15 @@ function needsPAndQsInvoke2(): int {
 };
 
 // The axiom fires because P(x) appears in the goal.
-procedure fireAxiomUsingPattern(x: int) {
+procedure fireAxiomUsingPattern(x: int)
+  opaque
+{
   assert P(x)
 };
 
-procedure axiomDoesNotFireBecauseOfPattern(x: int) {
+procedure axiomDoesNotFireBecauseOfPattern(x: int)
+  opaque
+{
   assert Q(x)
 //^^^^^^^^^^^ error: assertion could not be proved
 };
@@ -47,11 +51,15 @@ procedure AAndB(x: int, y: real)
   opaque
   ensures A(x, y) && B(y);
 
-procedure invokeA(x: int, y :real) {
+procedure invokeA(x: int, y :real)
+  opaque
+{
   assert A(x, y)
 };
 
-procedure invokeB(x: int, y :real) {
+procedure invokeB(x: int, y :real)
+  opaque
+{
   assert B(y)
 //^^^^^^^^^^^ error: assertion could not be proved
 };
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T1_AssertFalse.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T1_AssertFalse.lean
index 7baf038299..7a913ad921 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T1_AssertFalse.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T1_AssertFalse.lean
@@ -13,7 +13,9 @@ namespace Strata
 namespace Laurel
 
 def program := r"
-procedure foo() {
+procedure foo()
+  opaque
+{
     assert true;
     assert false;
 //  ^^^^^^^^^^^^ error: assertion does not hold
@@ -21,7 +23,9 @@ procedure foo() {
 //  ^^^^^^^^^^^^ error: assertion does not hold
 };
 
-procedure bar() {
+procedure bar()
+  opaque
+{
     assume false;
     assert false
 };
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T20_InferTypeError.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T20_InferTypeError.lean
index d8f352f716..8ac8f93f48 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T20_InferTypeError.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T20_InferTypeError.lean
@@ -13,7 +13,9 @@ namespace Strata
 namespace Laurel
 
 def inferTypeErrorProgram := r"
-procedure foo() {
+procedure foo()
+  opaque
+{
   <?>
 //^^^ error: could not infer type
 };
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T20_TransparentBodyError.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T20_TransparentBodyError.lean
new file mode 100644
index 0000000000..c86b0e3c9c
--- /dev/null
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T20_TransparentBodyError.lean
@@ -0,0 +1,26 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import StrataTest.Util.TestDiagnostics
+import StrataTest.Languages.Laurel.TestExamples
+
+open StrataTest.Util
+
+namespace Strata
+namespace Laurel
+
+def transparentBodyProgram := r"
+procedure transparentBody()
+//        ^^^^^^^^^^^^^^^ error: transparent procedures are not yet supported. Add 'opaque' to make the procedure opaque
+{
+  assert true
+};
+"
+
+#guard_msgs(drop info, error) in
+#eval testInputWithOffset "TransparentBody" transparentBodyProgram 14 processLaurelFile
+
+end Laurel
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T21_ExitMultiPathAssert.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T21_ExitMultiPathAssert.lean
index d9d4b0988e..97db999027 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T21_ExitMultiPathAssert.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T21_ExitMultiPathAssert.lean
@@ -12,7 +12,9 @@ open StrataTest.Util
 namespace Strata.Laurel
 
 def exitMultiPathProgram := r"
-procedure foo(x: int) {
+procedure foo(x: int)
+  opaque
+{
   {
     if x == 0 then {
       exit myBlock
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T22_MultipleReturns.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T22_MultipleReturns.lean
new file mode 100644
index 0000000000..c3e31806d7
--- /dev/null
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T22_MultipleReturns.lean
@@ -0,0 +1,52 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import StrataTest.Util.TestDiagnostics
+import StrataTest.Languages.Laurel.TestExamples
+
+open StrataTest.Util
+open Strata
+
+namespace Strata.Laurel
+
+def program := r"
+procedure multipleReturns() returns (x: int, y: int, z: int)
+  opaque
+  ensures x == 1 && y == 2 && z == 3;
+
+procedure caller()
+  opaque
+{
+  var y: int;
+  assign var x: int, y, var z: int := multipleReturns();
+  assert x == 1;
+  assert y == 2;
+  assert z == 3;
+
+  var a: int;
+  assign a, var b: int, var c: int := multipleReturns();
+  assert a == 1;
+  assert b == 2;
+  assert c == 3;
+
+  var m: int := 3;
+  var n: int;
+  n := 4
+};
+
+procedure repeatedAssignTarget()
+  opaque
+{
+  var x: int;
+  assign x, x, x := multipleReturns();
+  assert x == 3
+};
+"
+
+#guard_msgs (drop info, error) in
+#eval testInputWithOffset "MultipleReturns" program 14 processLaurelFile
+
+end Strata.Laurel
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
index ba3ed74314..e65d283f57 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
@@ -13,7 +13,9 @@ open Strata
 namespace Strata.Laurel
 
 def program: String := r"
-procedure nestedImpureStatements() {
+procedure nestedImpureStatements()
+  opaque
+{
   var y: int := 0;
   var x: int := y;
   var z: int := y := y + 1;
@@ -22,13 +24,17 @@ procedure nestedImpureStatements() {
   assert z == y
 };
 
-procedure multipleAssignments() {
+procedure multipleAssignments()
+  opaque
+{
   var x: int := 1;
   var y: int := x + ((x := 2) + x) + (x := 3);
   assert y == 8
 };
 
-procedure conditionalAssignmentInExpression(x: int) {
+procedure conditionalAssignmentInExpression(x: int)
+  opaque
+{
   var y: int := 0;
   var z: int := (if x > 0 then { y := y + 1 } else { 0 }) + y;
   if x > 0 then {
@@ -40,14 +46,18 @@ procedure conditionalAssignmentInExpression(x: int) {
   }
 };
 
-procedure anotherConditionAssignmentInExpression(c: bool) {
+procedure anotherConditionAssignmentInExpression(c: bool)
+  opaque
+{
   var b: bool := c;
   var z: bool := (if b then { b := false } else (b := true)) || b;
   assert z
 //^^^^^^^^ error: assertion does not hold
 };
 
-procedure blockWithTwoAssignmentsInExpression() {
+procedure blockWithTwoAssignmentsInExpression()
+  opaque
+{
   var x: int := 0;
   var y: int := 0;
   var z: int := { x := 1; y := 2 };
@@ -78,7 +88,9 @@ procedure imperativeProc(x: int) returns (r: int)
   r
 };
 
-procedure imperativeCallInExpressionPosition() {
+procedure imperativeCallInExpressionPosition()
+  opaque
+{
   var x: int := 0;
   // imperativeProc(x) is lifted out; its argument is evaluated before the call,
   // so the result is 1 (imperativeProc(0)), and x is still 0 afterwards.
@@ -88,7 +100,9 @@ procedure imperativeCallInExpressionPosition() {
 };
 
 // An imperative call inside a conditional expression is also lifted.
-procedure imperativeCallInConditionalExpression(b: bool) {
+procedure imperativeCallInConditionalExpression(b: bool)
+  opaque
+{
   var counter: int := 0;
   // The imperative call in the then-branch is lifted out of the expression.
   var result: int := (if b then { imperativeProc(counter) } else { 0 }) + counter;
@@ -104,7 +118,9 @@ function add(x: int, y: int): int
   x + y
 };
 
-procedure repeatedBlockExpressions() {
+procedure repeatedBlockExpressions()
+  opaque
+{
   var x: int := 2;
   var y: int := { x := 1; x } + { x := x + 10; x };
   var z: int := add({ x := 1; x }, { x := x + 10; x });
@@ -118,7 +134,9 @@ procedure addProc(a: int, b: int) returns (r: int)
   return a + b
 };
 
-procedure addProcCaller(): int {
+procedure addProcCaller(): int
+  opaque
+{
   var x: int := 0;
   var y: int := addProc({x := 1; x}, {x := x + 10; x});
   assert y == 11
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean
index 379701d566..57e5a61ddd 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean
@@ -13,7 +13,9 @@ open Strata
 namespace Strata.Laurel
 
 def program: String := r"
-procedure impure(): int {
+procedure impure(): int
+  opaque
+{
   var x: int := 0;
   x := x + 1;
   x
@@ -39,6 +41,7 @@ function impureFunction3(x: int): int
 procedure impureContractIsNotLegal1(x: int)
   requires x == impure()
 //              ^^^^^^^^ error: calls to procedures are not supported in functions or contracts
+  opaque
 {
   assert impure() == 1
 //       ^^^^^^^^ error: calls to procedures are not supported in functions or contracts
@@ -47,6 +50,7 @@ procedure impureContractIsNotLegal1(x: int)
 procedure impureContractIsNotLegal2(x: int)
   requires (x := 2) == 2
 //          ^^^^^^ error: destructive assignments are not supported in functions or contracts
+  opaque
 {
   assert (x := 2) == 2
 //        ^^^^^^ error: destructive assignments are not supported in functions or contracts
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean
index 150ee55f50..6e79453261 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean
@@ -41,7 +41,9 @@ function guardInFunction(x: int) returns (r: int) {
   return 3
 };
 
-procedure testFunctions() {
+procedure testFunctions()
+  opaque
+{
   assert returnAtEnd(1) == 1;
   assert returnAtEnd(1) == 2;
 //^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
@@ -52,6 +54,7 @@ procedure testFunctions() {
 };
 
 procedure guards(a: int) returns (r: int)
+  opaque
 {
   var b: int := a + 2;
   if b > 2 then {
@@ -70,6 +73,7 @@ procedure guards(a: int) returns (r: int)
 };
 
 procedure dag(a: int) returns (r: int)
+  opaque
 {
   var b: int;
 
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T4b_Exit.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T4b_Exit.lean
index c321315684..ce3868af8f 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T4b_Exit.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T4b_Exit.lean
@@ -12,7 +12,9 @@ open StrataTest.Util
 namespace Strata.Laurel
 
 def exitProgram := r"
-procedure exitSkipsRest() {
+procedure exitSkipsRest()
+  opaque
+{
     var x: int := 0;
     {
         x := 1;
@@ -21,7 +23,9 @@ procedure exitSkipsRest() {
     assert x == 1
 };
 
-procedure exitFromNestedBlock() {
+procedure exitFromNestedBlock()
+  opaque
+{
     var x: int := 0;
     {
         {
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCalls.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCalls.lean
index adb08b2aaf..e1e5c0cfd8 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCalls.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCalls.lean
@@ -13,7 +13,9 @@ open Strata
 namespace Strata.Laurel
 
 def program := r"
-procedure fooReassign(): int {
+procedure fooReassign(): int
+  opaque
+{
   var x: int := 0;
   x := x + 1;
   assert x == 1;
@@ -21,14 +23,18 @@ procedure fooReassign(): int {
   x
 };
 
-procedure fooSingleAssign(): int {
+procedure fooSingleAssign(): int
+  opaque
+{
   var x: int := 0;
   var x2: int := x + 1;
   var x3: int := x2 + 1;
   x3
 };
 
-procedure fooProof() {
+procedure fooProof()
+  opaque
+{
   var x: int := fooReassign();
   var y: int := fooSingleAssign()
 // The following assertions fails while it should succeed,
@@ -41,7 +47,9 @@ function aFunction(x: int): int
   x
 };
 
-procedure aFunctionCaller() {
+procedure aFunctionCaller()
+  opaque
+{
   var x: int := aFunction(3);
   assert x == 3
 };
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean
index c22d91c671..c7f1742a88 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean
@@ -18,6 +18,7 @@ procedure hasRequires(x: int) returns (r: int)
 // Call elimination reports precondition errors at the call site,
 // not at the requires clause definition.
 //
+  opaque
 {
   assert x > 0;
   assert x > 3;
@@ -25,7 +26,9 @@ procedure hasRequires(x: int) returns (r: int)
   x + 1
 };
 
-procedure caller() {
+procedure caller()
+  opaque
+{
   var x: int := hasRequires(1);
 //^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: precondition does not hold
   var y: int := hasRequires(3)
@@ -37,7 +40,9 @@ function aFunctionWithPrecondition(x: int): int
   x
 };
 
-procedure aFunctionWithPreconditionCaller() {
+procedure aFunctionWithPreconditionCaller()
+  opaque
+{
   var x: int := aFunctionWithPrecondition(0)
 //^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
 // Error ranges are too wide because Core does not use expression locations
@@ -46,11 +51,14 @@ procedure aFunctionWithPreconditionCaller() {
 procedure multipleRequires(x: int, y: int) returns (r: int)
   requires x > 0
   requires y > 0
+  opaque
 {
   x + y
 };
 
-procedure multipleRequiresCaller() {
+procedure multipleRequiresCaller()
+  opaque
+{
   var a: int := multipleRequires(1, 2);
   var b: int := multipleRequires(-1, 2)
 //^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: precondition does not hold
@@ -63,7 +71,9 @@ function funcMultipleRequires(x: int, y: int): int
   x + y
 };
 
-procedure funcMultipleRequiresCaller() {
+procedure funcMultipleRequiresCaller()
+  opaque
+{
   var a: int := funcMultipleRequires(1, 2);
   var b: int := funcMultipleRequires(1, -1)
 //^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean
index 94a070dec1..526a03dd92 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean
@@ -21,7 +21,9 @@ procedure opaqueBody(x: int) returns (r: int)
   else { r := 1 }
 };
 
-procedure callerOfOpaqueProcedure() {
+procedure callerOfOpaqueProcedure()
+  opaque
+{
   var x: int := opaqueBody(3);
   assert x > 0;
   assert x == 3
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_PostconditionsErrors.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_PostconditionsErrors.lean
index d5721c8050..d61c5849da 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_PostconditionsErrors.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_PostconditionsErrors.lean
@@ -25,7 +25,9 @@ function opaqueFunction(x: int) returns (r: int)
   x
 };
 
-procedure callerOfOpaqueFunction() {
+procedure callerOfOpaqueFunction()
+  opaque
+{
   var x: int := opaqueFunction(3);
   assert x > 0;
 // The following assertion should fail but does not
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8c_BodilessInlining.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8c_BodilessInlining.lean
index 5d7d273280..34ef67a97e 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8c_BodilessInlining.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8c_BodilessInlining.lean
@@ -22,14 +22,16 @@ procedure bodilessProcedure() returns (r: int)
   ensures r > 0
 ;
 
-procedure caller() {
+procedure caller()
+  opaque
+{
   var x: int := bodilessProcedure();
   assert x > 0;
   assert false
 };
 "
 
-/-- info: "assert(152): ❌ fail" -/
+/-- info: "assert(161): ❌ fail" -/
 #guard_msgs in
 #eval show IO String from do
   let laurelProg ← Strata.parseLaurelText "test.laurel" laurelSource
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean b/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean
index 832b8633c9..1275b0b1c2 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean
@@ -20,13 +20,17 @@ composite Container {
   var stringValue: string
 }
 
-procedure newsAreNotEqual() {
+procedure newsAreNotEqual()
+  opaque
+{
   var c: Container := new Container;
   var d: Container := new Container;
   assert c != d
 };
 
-procedure simpleAssign() {
+procedure simpleAssign()
+  opaque
+{
   var c: Container := new Container;
   var iv: int := c#intValue;
   var rv: real := c#realValue;
@@ -45,6 +49,7 @@ procedure simpleAssign() {
 };
 
 procedure updatesAndAliasing()
+  opaque
 {
   var c: Container := new Container;
   var d: Container := new Container;
@@ -62,13 +67,20 @@ procedure updatesAndAliasing()
   assert dAlias#intValue == d#intValue
 };
 
-procedure subsequentHeapMutations(c: Container) {
+procedure subsequentHeapMutations(c: Container)
+  opaque
+  modifies c
+{
   // The additional parenthesis on the next line are needed to let the parser succeed. Joe, any idea why this is needed?
   var sum: int := ((c#intValue := 1) + c#intValue) + (c#intValue := 2);
   assert sum == 4
 };
 
-procedure implicitEquality(c: Container, d: Container) {
+procedure implicitEquality(c: Container, d: Container)
+  opaque
+  modifies c
+  modifies d
+{
   c#intValue := 1;
   d#intValue := 2;
   if c#intValue == d#intValue then {
@@ -79,7 +91,9 @@ procedure implicitEquality(c: Container, d: Container) {
   }
 };
 
-procedure useBool(c: Container) returns (r: bool) {
+procedure useBool(c: Container) returns (r: bool)
+  opaque
+{
   r := c#boolValue
 };
 
@@ -87,7 +101,11 @@ composite SameFieldName {
   var intValue: bool
 }
 
-procedure sameFieldNameDifferentType(a: Container, b: SameFieldName) {
+procedure sameFieldNameDifferentType(a: Container, b: SameFieldName)
+  opaque
+  modifies a
+  modifies b
+{
   a#intValue := 1;
   b#intValue := true;
 
@@ -106,7 +124,9 @@ composite Pixel {
   var color: Color
 }
 
-procedure datatypeField() {
+procedure datatypeField()
+  opaque
+{
   var p: Pixel := new Pixel;
   p#color := Red();
   assert Color..isRed(p#color);
@@ -137,6 +157,35 @@ procedure datatypeField() {
 //   assert d#intValue == 1;
 //   assert x == 4;
 // }
+
+procedure modifyHeapAndReturnMultiple(c: Container) returns (x: int, y: int, z: int)
+  opaque
+  ensures x == 1 && y == 2 && z == 3
+  modifies c
+;
+
+procedure heapModifyingMultipleReturnCaller()
+  opaque
+{
+  var c: Container := new Container;
+  var y: int;
+  assign var x: int, y, var z: int := modifyHeapAndReturnMultiple(c);
+  assert x == 1;
+  assert y == 2;
+  assert z == 3
+};
+
+procedure fieldAssignsFromHeapModifyingMultipleReturnCaller()
+  opaque
+{
+  var c: Container := new Container;
+  var y: int;
+  assign var w: int, y, var z: int := modifyHeapAndReturnMultiple(c);
+  c#intValue := w;
+  assert c#intValue == 1;
+  assert y == 2;
+  assert z == 3
+};
 "#
 
 #guard_msgs(drop info, error) in
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T2_ModifiesClauses.lean b/StrataTest/Languages/Laurel/Examples/Objects/T2_ModifiesClauses.lean
index 49fdd05400..52a16146c5 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T2_ModifiesClauses.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T2_ModifiesClauses.lean
@@ -35,13 +35,9 @@ procedure modifyContainerOpaque(c: Container) returns (b: bool)
   true
 };
 
-procedure modifyContainerTransparant(c: Container) returns (i: int)
+procedure caller()
+  opaque
 {
-  c#value := c#value + 1;
-  7
-};
-
-procedure caller() {
   var c: Container := new Container;
   var d: Container := new Container;
   var x: int := d#value;
@@ -49,8 +45,13 @@ procedure caller() {
   assert x == d#value // pass
 };
 
-// This test-case does not work yet.
-// Because Core procedures never have transparent bodies
+// Commented out because
+// Transparent assignments are not supported yet
+// procedure modifyContainerTransparant(c: Container) returns (i: int)
+//{
+//  c#value := c#value + 1;
+//  7
+//};
 //procedure modifyContainerWithPermission1(c: Container, d: Container)
 //   ensures true
 //   modifies c
@@ -58,17 +59,23 @@ procedure caller() {
 //    var i: int := modifyContainerTransparant(c);
 //}
 
+procedure modifyContainerWildcard(c: Container) returns (i: int)
+  opaque
+  modifies *
+{
+  c#value := c#value + 1;
+  7
+};
+
 procedure modifyContainerWithoutPermission1(c: Container, d: Container)
-//        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
-// the above error is because the body does not satisfy the empty modifies clause. error needs to be improved
-   opaque
+//        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: modifies clause does not hold
+  opaque
 {
-    var i: int := modifyContainerTransparant(c)
+    var i: int := modifyContainerWildcard(c)
 };
 
 procedure modifyContainerWithoutPermission2(c: Container, d: Container)
-//        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved
-// the above error is because the body does not satisfy the modifies clause. error needs to be improved
+//        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: modifies clause could not be proved
   opaque
   modifies d
 {
@@ -76,12 +83,11 @@ procedure modifyContainerWithoutPermission2(c: Container, d: Container)
 };
 
 procedure modifyContainerWithoutPermission3(c: Container, d: Container)
-//        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
-// the above error is because the body does not satisfy the modifies clause. error needs to be improved
+//        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: modifies clause could not be proved
   opaque
   modifies d
 {
-    var i: int := modifyContainerTransparant(c)
+    var i: bool := modifyContainerOpaque(c)
 };
 
 procedure multipleModifiesClauses(c: Container, d: Container, e: Container)
@@ -90,7 +96,9 @@ procedure multipleModifiesClauses(c: Container, d: Container, e: Container)
   modifies d
 ;
 
-procedure multipleModifiesClausesCaller() {
+procedure multipleModifiesClausesCaller()
+  opaque
+{
   var c: Container := new Container;
   var d: Container := new Container;
   var e: Container := new Container;
@@ -110,7 +118,10 @@ procedure modifiesWildcardBodiless(c: Container, d: Container)
   opaque
   modifies *;
 
-procedure modifiesWildcardBodilessCaller() {
+procedure modifiesWildcardBodilessCaller()
+  opaque
+  modifies *
+{
   var c: Container := new Container;
   var d: Container := new Container;
   var x: int := d#value;
@@ -132,7 +143,10 @@ procedure modifiesWildcardAndSpecific(c: Container, d: Container)
   modifies c
   modifies *;
 
-procedure modifiesWildcardAndSpecificCaller() {
+procedure modifiesWildcardAndSpecificCaller()
+  opaque
+  modifies *
+{
   var c: Container := new Container;
   var d: Container := new Container;
   var x: int := d#value;
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T5_inheritance.lean b/StrataTest/Languages/Laurel/Examples/Objects/T5_inheritance.lean
index d9cb4dbde4..dc6307263d 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T5_inheritance.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T5_inheritance.lean
@@ -25,7 +25,10 @@ composite Extender extends Base, Base2 {
   var zValue: int
 }
 
-procedure inheritedFields(a: Extender) {
+procedure inheritedFields(a: Extender)
+  opaque
+  modifies a
+{
   a#xValue := 1;
   a#yValue := 2;
   a#zValue := 3;
@@ -35,7 +38,9 @@ procedure inheritedFields(a: Extender) {
   assert a#zValue == 3
 };
 
-procedure typeCheckingAndCasting() {
+procedure typeCheckingAndCasting()
+  opaque
+{
   var a: Base := new Base;
   assert a is Base;
   assert !(a is Extender);
@@ -64,7 +69,9 @@ composite Bottom extends Left, Right {
   var bValue: int
 }
 
-procedure diamondInheritance() {
+procedure diamondInheritance()
+  opaque
+{
   var b: Bottom := new Bottom;
   b#lValue := 1;
   b#rValue := 2;
@@ -91,5 +98,5 @@ procedure diamondInheritance() {
 //}
 "
 
-#guard_msgs (drop info) in
+#guard_msgs (drop info, error) in
 #eval testInputWithOffset "Inheritance" program 14 processLaurelFile
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T5_inheritanceErrors.lean b/StrataTest/Languages/Laurel/Examples/Objects/T5_inheritanceErrors.lean
index 0b6d471b6c..af1b8ee5eb 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T5_inheritanceErrors.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T5_inheritanceErrors.lean
@@ -21,7 +21,10 @@ composite Left extends Top {}
 composite Right extends Top {}
 composite Bottom extends Left, Right {}
 
-procedure diamondField(b: Bottom) {
+procedure diamondField(b: Bottom)
+  opaque
+  modifies b
+{
   b#xValue := 1
 //  ^^^^^^ error: fields that are inherited multiple times can not be accessed.
 };
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T6_Datatypes.lean b/StrataTest/Languages/Laurel/Examples/Objects/T6_Datatypes.lean
index 00be7c2c8f..9bb51c2d13 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T6_Datatypes.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T6_Datatypes.lean
@@ -19,13 +19,17 @@ datatype IntList {
 }
 
 // Construction and destructor access
-procedure testConstruction() {
+procedure testConstruction()
+  opaque
+{
   var xs: IntList := Cons(42, Nil());
   assert IntList..head(xs) == 42
 };
 
 // Constructor testing
-procedure testConstructorTest() {
+procedure testConstructorTest()
+  opaque
+{
   var xs: IntList := Cons(1, Nil());
   assert IntList..isCons(xs);
   assert !IntList..isNil(xs);
@@ -36,7 +40,9 @@ procedure testConstructorTest() {
 };
 
 // Nested construction and deconstruction
-procedure testNested() {
+procedure testNested()
+  opaque
+{
   var xs: IntList := Cons(1, Cons(2, Nil()));
   assert IntList..isCons(xs);
   assert IntList..head(xs) == 1;
@@ -45,7 +51,9 @@ procedure testNested() {
   assert IntList..isNil(IntList..tail(IntList..tail(xs)))
 };
 
-procedure unsafeDestructor() {
+procedure unsafeDestructor()
+  opaque
+{
   var nil: IntList := Nil();
   var noError: int := IntList..head!(nil);
   var error: int := IntList..head(nil)
@@ -59,14 +67,18 @@ function listHead(xs: IntList): int
   IntList..head(xs)
 };
 
-procedure testFunction() {
+procedure testFunction()
+  opaque
+{
   var xs: IntList := Cons(10, Nil());
   var h: int := listHead(xs);
   assert h == 10
 };
 
 // Failing assertion
-procedure testFailing() {
+procedure testFailing()
+  opaque
+{
   var xs: IntList := Nil();
   assert IntList..isCons(xs)
 //^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
@@ -82,7 +94,9 @@ datatype OddList {
   OCons(head: int, tail: EvenList)
 }
 
-procedure testMutualConstruction() {
+procedure testMutualConstruction()
+  opaque
+{
   var even: EvenList := ENil();
   assert EvenList..isENil(even);
   var odd: OddList := OCons(1, ENil());
@@ -93,8 +107,8 @@ procedure testMutualConstruction() {
   assert EvenList..head(even2) == 2
 };
 
-datatype RootBeforeLeaf { RootBeforeLeaf(leaf: LeafAfterRoot) }
-datatype LeafAfterRoot { LeafAfterRoot }
+datatype RootBeforeLeaf { RootBeforeLeafC(leaf: LeafAfterRoot) }
+datatype LeafAfterRoot { LeafAfterRootC }
 "
 
 #guard_msgs (error, drop all) in
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T7_InstanceProcedures.lean b/StrataTest/Languages/Laurel/Examples/Objects/T7_InstanceProcedures.lean
index 069c33cd4f..ec05fcfd3d 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T7_InstanceProcedures.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T7_InstanceProcedures.lean
@@ -15,12 +15,16 @@ namespace Strata.Laurel
 def instanceProcedureProgram := r"
 composite Counter {
   var count: int
-  procedure increment(self: Counter) {
+  procedure increment(self: Counter)
 //          ^^^^^^^^^ error: Instance procedure 'increment' on composite type 'Counter' is not yet supported
+    opaque
+  {
     self#count := self#count + 1
   };
-  procedure reset(self: Counter) {
+  procedure reset(self: Counter)
 //          ^^^^^ error: Instance procedure 'reset' on composite type 'Counter' is not yet supported
+    opaque
+  {
     self#count := 0
   };
 }
diff --git a/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T1_Decimals.lean b/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T1_Decimals.lean
index 417c1ec77f..98d3908d77 100644
--- a/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T1_Decimals.lean
+++ b/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T1_Decimals.lean
@@ -13,7 +13,9 @@ namespace Strata
 namespace Laurel
 
 def decimalsProgram := r"
-procedure testDecimalLiterals() {
+procedure testDecimalLiterals()
+  opaque
+{
     var a: real := 1.5;
     var b: real := 2.5;
     assert a == 1.5;
@@ -21,7 +23,9 @@ procedure testDecimalLiterals() {
     assert a != b
 };
 
-procedure testDecimalArithmetic() {
+procedure testDecimalArithmetic()
+  opaque
+{
     var a: real := 1.5;
     var b: real := 2.5;
     var sum: real := a + b;
@@ -34,13 +38,17 @@ procedure testDecimalArithmetic() {
     assert quot == 5.0 / 3.0
 };
 
-procedure testDecimalNeg() {
+procedure testDecimalNeg()
+  opaque
+{
     var a: real := 1.5;
     var neg: real := -a;
     assert neg == 0.0 - 1.5
 };
 
-procedure testDecimalComparisons() {
+procedure testDecimalComparisons()
+  opaque
+{
     var a: real := 1.5;
     var b: real := 2.5;
     assert a < b;
@@ -51,7 +59,9 @@ procedure testDecimalComparisons() {
     assert a >= a
 };
 
-procedure testDecimalAssertFails() {
+procedure testDecimalAssertFails()
+  opaque
+{
     var a: real := 1.5;
     var b: real := 2.5;
     assert a == b
diff --git a/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T2_String.lean b/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T2_String.lean
index bfb32714e0..02b5729dc8 100644
--- a/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T2_String.lean
+++ b/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T2_String.lean
@@ -16,7 +16,7 @@ namespace Laurel
 def program := r#"
 procedure testStringKO()
 returns (result: string)
-requires true
+  opaque
 {
   var message: string := "Hello";
   assert(message == "Hell");
@@ -27,7 +27,7 @@ requires true
 
 procedure testStringOK()
 returns (result: string)
-requires true
+  opaque
 {
   var message: string := "Hello";
   assert(message == "Hello");
@@ -36,14 +36,14 @@ requires true
 };
 
 procedure testStringLiteralConcatOK()
-requires true
+  opaque
 {
   var result: string := "a" ++ "b";
   assert(result == "ab")
 };
 
 procedure testStringLiteralConcatKO()
-requires true
+  opaque
 {
   var result: string := "a" ++ "b";
   assert(result == "cd")
@@ -51,7 +51,7 @@ requires true
 };
 
 procedure testStringVarConcatOK()
-requires true
+  opaque
 {
   var x: string := "Hello";
   var result: string := x ++ " World";
@@ -59,7 +59,7 @@ requires true
 };
 
 procedure testStringVarConcatKO()
-requires true
+  opaque
 {
   var x: string := "Hello";
   var result: string := x ++ " World";
diff --git a/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T2_StringConcatLifting.lean b/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T2_StringConcatLifting.lean
index 482dd20d0c..6f0b2a01a7 100644
--- a/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T2_StringConcatLifting.lean
+++ b/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T2_StringConcatLifting.lean
@@ -14,7 +14,7 @@ namespace Strata.Laurel
 
 def stringConcatLiftingProgram := r#"
 procedure stringConcatWithAssignment()
-requires true
+  opaque
 {
   var x: string := "Hello";
   var y: string := x ++ (x := " World");
@@ -23,7 +23,7 @@ requires true
 };
 
 procedure stringConcatOK()
-requires true
+  opaque
 {
   var a: string := "Hello";
   var b: string := " World";
@@ -32,7 +32,7 @@ requires true
 };
 
 procedure stringConcatKO()
-requires true
+  opaque
 {
   var a: string := "Hello";
   var b: string := " World";
diff --git a/StrataTest/Languages/Laurel/LiftHolesTest.lean b/StrataTest/Languages/Laurel/LiftHolesTest.lean
index 9065609fba..14d25a4416 100644
--- a/StrataTest/Languages/Laurel/LiftHolesTest.lean
+++ b/StrataTest/Languages/Laurel/LiftHolesTest.lean
@@ -33,7 +33,7 @@ private def parseElimAndPrint (input : String) : IO Unit := do
   | .ok program =>
     let result := resolve program
     let (program, model) := (result.program, result.model)
-    let (program, _) := inferHoleTypes model program
+    let (program, _, _) := inferHoleTypes model program
     let (program, _) := eliminateHoles program
     for proc in program.staticProcedures do
       IO.println (toString (Std.Format.pretty (Std.ToFormat.format proc)))
@@ -53,7 +53,7 @@ procedure test()
 procedure test() { var x: int := 1 + <?> };
 "
 
--- Bare Hole as LocalVariable initializer → replaced with call (no longer preserved as havoc).
+-- Bare Hole as Assign Declare initializer → replaced with call (no longer preserved as havoc).
 /--
 info: function $hole_0()
   returns ($result: int)
diff --git a/StrataTest/Languages/Laurel/MapStmtExprTest.lean b/StrataTest/Languages/Laurel/MapStmtExprTest.lean
index b1406daf31..b9329a99f8 100644
--- a/StrataTest/Languages/Laurel/MapStmtExprTest.lean
+++ b/StrataTest/Languages/Laurel/MapStmtExprTest.lean
@@ -50,7 +50,7 @@ private def testMapStmtExprId (input : String) : IO Unit := do
   else
     IO.println s!"MISMATCH\nbefore:\n{before}\nafter:\n{after}"
 
--- Exercises: IfThenElse, Block, LocalVariable, While, Return, Assign,
+-- Exercises: IfThenElse, Block, Var Declare, While, Return, Assign,
 -- PrimitiveOp, Assert, Assume, Forall, Exists, LiteralInt, LiteralBool, Identifier.
 def testProgram : String := r"
 procedure test(x: int, b: bool) returns (r: int)
diff --git a/StrataTest/Languages/Laurel/ResolutionKindTests.lean b/StrataTest/Languages/Laurel/ResolutionKindTests.lean
index 61627924ad..acbef556b6 100644
--- a/StrataTest/Languages/Laurel/ResolutionKindTests.lean
+++ b/StrataTest/Languages/Laurel/ResolutionKindTests.lean
@@ -37,7 +37,7 @@ private def processResolution (input : Lean.Parser.InputContext) : IO (Array Dia
 /-! ## Using a variable name where a type is expected -/
 
 def varAsType := r"
-procedure foo() {
+procedure foo() opaque {
   var x: int := 1;
   var y: x := 2
 //       ^ error: 'x' resolves to variable, but expected composite type, constrained type, datatype definition, type alias
@@ -50,8 +50,8 @@ procedure foo() {
 /-! ## Using a procedure name where a type is expected -/
 
 def procAsType := r"
-procedure bar() { };
-procedure foo() {
+procedure bar() opaque { };
+procedure foo() opaque {
   var y: bar := 1
 //       ^^^ error: 'bar' resolves to static procedure, but expected composite type, constrained type, datatype definition, type alias
 };
@@ -64,7 +64,7 @@ procedure foo() {
 
 def typeAsStaticCall := r"
 composite Foo { }
-procedure bar() {
+procedure bar() opaque {
   var x: int := Foo()
 //              ^^^^^ error: 'Foo' resolves to composite type, but expected parameter, static procedure, datatype constructor, constant
 };
@@ -76,15 +76,15 @@ procedure bar() {
 /-! ## Using a procedure name with `new` -/
 
 def newWithProc := r"
-procedure bar() { };
-procedure foo() {
+procedure bar() opaque { };
+procedure foo() opaque {
   var x: int := new bar
 //              ^^^^^^^ error: 'bar' resolves to static procedure, but expected composite type, datatype definition
 };
 "
 
 #guard_msgs (error, drop all) in
-#eval testInputWithOffset "NewWithProc" newWithProc 73 processResolution
+#eval testInputWithOffset "NewWithProc" newWithProc 77 processResolution
 
 /-! ## Extending a non-composite type (e.g. a constrained type) -/
 
@@ -95,6 +95,6 @@ composite Foo extends nat { }
 "
 
 #guard_msgs (error, drop all) in
-#eval testInputWithOffset "ExtendConstrained" extendConstrained 83 processResolution
+#eval testInputWithOffset "ExtendConstrained" extendConstrained 90 processResolution
 
 end Laurel
diff --git a/StrataTest/Languages/Laurel/TypeAliasElimTest.lean b/StrataTest/Languages/Laurel/TypeAliasElimTest.lean
index 4ca58d611c..7110cdfeec 100644
--- a/StrataTest/Languages/Laurel/TypeAliasElimTest.lean
+++ b/StrataTest/Languages/Laurel/TypeAliasElimTest.lean
@@ -49,7 +49,7 @@ private def chainedProgram : Program :=
       mkProc "test"
         [{ name := mkId "x", type := mkTy (.UserDefined (mkId "B")) }]
         [{ name := mkId "r", type := mkTy (.UserDefined (mkId "A")) }]
-        (.Transparent ⟨.Return (some ⟨.Identifier (mkId "x"), none⟩), none⟩)
+        (.Transparent ⟨.Return (some ⟨.Var (.Local (mkId "x")), none⟩), none⟩)
     ]
     staticFields := []
     types := [
@@ -111,7 +111,7 @@ private def procSigProgram : Program :=
         [{ name := mkId "a", type := mkTy (.UserDefined (mkId "MyInt")) },
          { name := mkId "b", type := mkTy (.UserDefined (mkId "MyBool")) }]
         [{ name := mkId "r", type := mkTy (.UserDefined (mkId "MyInt")) }]
-        (.Transparent ⟨.Return (some ⟨.Identifier (mkId "a"), none⟩), none⟩)
+        (.Transparent ⟨.Return (some ⟨.Var (.Local (mkId "a")), none⟩), none⟩)
     ]
     staticFields := []
     types := [
diff --git a/StrataTest/Languages/Laurel/tests/cbmc_expected.txt b/StrataTest/Languages/Laurel/tests/cbmc_expected.txt
index 2eff9f1bd1..538a309a7a 100644
--- a/StrataTest/Languages/Laurel/tests/cbmc_expected.txt
+++ b/StrataTest/Languages/Laurel/tests/cbmc_expected.txt
@@ -5,33 +5,33 @@
 # with the expected status.
 
 test_arithmetic.lr.st
-  [main.1] line 6 assert: SUCCESS
-  [main.2] line 11 assert: SUCCESS
-  [main.3] line 14 assert: SUCCESS
-  [main.4] line 17 assert: SUCCESS
+  [main.1] line 8 assert: SUCCESS
+  [main.2] line 13 assert: SUCCESS
+  [main.3] line 16 assert: SUCCESS
+  [main.4] line 19 assert: SUCCESS
 
 test_comparisons.lr.st
-  [main.1] line 4 assert: SUCCESS
-  [main.2] line 8 assert: SUCCESS
-  [main.3] line 9 assert: SUCCESS
-  [main.4] line 10 assert: SUCCESS
-  [main.5] line 11 assert: SUCCESS
+  [main.1] line 6 assert: SUCCESS
+  [main.2] line 10 assert: SUCCESS
+  [main.3] line 11 assert: SUCCESS
+  [main.4] line 12 assert: SUCCESS
+  [main.5] line 13 assert: SUCCESS
 
 test_control_flow.lr.st
-  [main.1] line 10 assert: SUCCESS
-  [main.2] line 24 assert: SUCCESS
-  [main.3] line 34 assert: SUCCESS
+  [main.1] line 12 assert: SUCCESS
+  [main.2] line 26 assert: SUCCESS
+  [main.3] line 36 assert: SUCCESS
 
 test_failing_assert.lr.st
-  [main.1] line 3 assert: FAILURE
+  [main.1] line 5 assert: FAILURE
 
 test_operators.lr.st
-  [main.1] line 5 assert: SUCCESS
-  [main.2] line 7 assert: SUCCESS
-  [main.3] line 9 assert: SUCCESS
-  [main.4] line 11 assert: SUCCESS
-  [main.5] line 16 assert: SUCCESS
+  [main.1] line 7 assert: SUCCESS
+  [main.2] line 9 assert: SUCCESS
+  [main.3] line 11 assert: SUCCESS
+  [main.4] line 13 assert: SUCCESS
+  [main.5] line 18 assert: SUCCESS
 
 test_strings.lr.st
-  [main.1] line 5 assert: SUCCESS
-  [main.2] line 9 assert: SUCCESS
+  [main.1] line 7 assert: SUCCESS
+  [main.2] line 11 assert: SUCCESS
diff --git a/StrataTest/Languages/Laurel/tests/test_arithmetic.lr.st b/StrataTest/Languages/Laurel/tests/test_arithmetic.lr.st
index 679d116441..7b5da7f2d3 100644
--- a/StrataTest/Languages/Laurel/tests/test_arithmetic.lr.st
+++ b/StrataTest/Languages/Laurel/tests/test_arithmetic.lr.st
@@ -1,4 +1,6 @@
-procedure main() {
+procedure main()
+  opaque
+{
     var x: int := 5;
     var y: int := 3;
 
diff --git a/StrataTest/Languages/Laurel/tests/test_bitvector_types.lr.st b/StrataTest/Languages/Laurel/tests/test_bitvector_types.lr.st
index 9e83f61157..6c98d6fc40 100644
--- a/StrataTest/Languages/Laurel/tests/test_bitvector_types.lr.st
+++ b/StrataTest/Languages/Laurel/tests/test_bitvector_types.lr.st
@@ -1,14 +1,20 @@
 // Bitvector types through the GOTO/CBMC pipeline.
 
-procedure identity32(x: bv 32) returns (r: bv 32) {
+procedure identity32(x: bv 32) returns (r: bv 32)
+  opaque
+{
   r := x
 };
 
-procedure identity8(x: bv 8) returns (r: bv 8) {
+procedure identity8(x: bv 8) returns (r: bv 8)
+  opaque
+{
   r := x
 };
 
-procedure localBv() returns (r: bv 16) {
+procedure localBv() returns (r: bv 16)
+  opaque
+{
   var x: bv 16 := r;
   r := x
 };
diff --git a/StrataTest/Languages/Laurel/tests/test_comparisons.lr.st b/StrataTest/Languages/Laurel/tests/test_comparisons.lr.st
index 6b67b797e0..1b0dc4d6b1 100644
--- a/StrataTest/Languages/Laurel/tests/test_comparisons.lr.st
+++ b/StrataTest/Languages/Laurel/tests/test_comparisons.lr.st
@@ -1,4 +1,6 @@
-procedure main() {
+procedure main()
+  opaque
+{
     var a: int := 10;
     var b: int := 10;
     assert a == b;
diff --git a/StrataTest/Languages/Laurel/tests/test_control_flow.lr.st b/StrataTest/Languages/Laurel/tests/test_control_flow.lr.st
index b255bd7b3a..84fba11963 100644
--- a/StrataTest/Languages/Laurel/tests/test_control_flow.lr.st
+++ b/StrataTest/Languages/Laurel/tests/test_control_flow.lr.st
@@ -1,4 +1,6 @@
-procedure main() {
+procedure main()
+  opaque
+{
     var x: int := 5;
     var result: int := 0;
 
diff --git a/StrataTest/Languages/Laurel/tests/test_failing_assert.lr.st b/StrataTest/Languages/Laurel/tests/test_failing_assert.lr.st
index 9a6248151b..3cf0ace618 100644
--- a/StrataTest/Languages/Laurel/tests/test_failing_assert.lr.st
+++ b/StrataTest/Languages/Laurel/tests/test_failing_assert.lr.st
@@ -1,4 +1,6 @@
-procedure main() {
+procedure main()
+  opaque
+{
     var x: int := 5;
     assert x == 10
 };
diff --git a/StrataTest/Languages/Laurel/tests/test_operators.lr.st b/StrataTest/Languages/Laurel/tests/test_operators.lr.st
index e38dfa7d9e..392414ad11 100644
--- a/StrataTest/Languages/Laurel/tests/test_operators.lr.st
+++ b/StrataTest/Languages/Laurel/tests/test_operators.lr.st
@@ -1,4 +1,6 @@
-procedure main() {
+procedure main()
+  opaque
+{
     var a: int := 10;
     var b: int := 3;
     var x: int := a - b;
diff --git a/StrataTest/Languages/Laurel/tests/test_strings.lr.st b/StrataTest/Languages/Laurel/tests/test_strings.lr.st
index 35c643a9e2..f9a84a5b3e 100644
--- a/StrataTest/Languages/Laurel/tests/test_strings.lr.st
+++ b/StrataTest/Languages/Laurel/tests/test_strings.lr.st
@@ -1,4 +1,6 @@
-procedure main() {
+procedure main()
+  opaque
+{
     var s1: string := "hello";
     var s2: string := " world";
     var result: string := s1 ++ s2;
diff --git a/StrataTest/Languages/Python/PySpecArgTypeTest.lean b/StrataTest/Languages/Python/PySpecArgTypeTest.lean
index 4030fc45fd..d921aaab9c 100644
--- a/StrataTest/Languages/Python/PySpecArgTypeTest.lean
+++ b/StrataTest/Languages/Python/PySpecArgTypeTest.lean
@@ -95,6 +95,8 @@ preconditions redundant. -/
 
 /--
 info: procedure typed_func(x: Any, y: Any): Any
+  opaque
+  modifies *
 { result := <??>; assert Any..isfrom_int(x); assert Any..isfrom_str(y); assume Any..isfrom_float(result) };
 -/
 #guard_msgs in
diff --git a/StrataTest/Languages/Python/ToLaurelTest.lean b/StrataTest/Languages/Python/ToLaurelTest.lean
index ae922c8db5..597badb207 100644
--- a/StrataTest/Languages/Python/ToLaurelTest.lean
+++ b/StrataTest/Languages/Python/ToLaurelTest.lean
@@ -62,6 +62,7 @@ private def fmtHighType : HighType → String
   | .TBv n => s!"TBv({n})"
   | .TCore s => s!"TCore({s})"
   | .Unknown => "Unknown"
+  | .MultiValuedExpr _ => "MultiValuedExpr"
 
 private def fmtParam (p : Parameter) : String :=
   s!"{p.name}:{fmtHighType p.type.val}"
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_empty.expected b/StrataTest/Languages/Python/expected_laurel/test_class_empty.expected
index c5963c0e19..aab04f3a0d 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_empty.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_empty.expected
@@ -1,4 +1,4 @@
-test_class_empty.py(5, 4): ✅ pass - callElimAssert_requires_2
+test_class_empty.py(5, 4): ✅ pass - callElimAssert_requires_4
 test_class_empty.py(6, 4): ✅ pass - empty class instantiated
 DETAIL: 2 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected b/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected
index 7be00f5c53..36c53a8361 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected
@@ -1,8 +1,8 @@
-test_class_methods.py(34, 4): ✔️ always true if reached - main_assert(471)_17
+test_class_methods.py(34, 4): ✔️ always true if reached - main_assert(471)_13
 test_class_methods.py(34, 4): ✔️ always true if reached - get_owner should return Alice
-test_class_methods.py(34, 4): ✔️ always true if reached - main_assert(564)_19
+test_class_methods.py(34, 4): ✔️ always true if reached - main_assert(564)_15
 test_class_methods.py(34, 4): ✔️ always true if reached - get_balance should return 100
-test_class_methods.py(34, 4): ✔️ always true if reached - main_assert(678)_21
+test_class_methods.py(34, 4): ✔️ always true if reached - main_assert(678)_17
 test_class_methods.py(34, 4): ✔️ always true if reached - set_balance should update balance
 test_class_methods.py(31, 4): ✔️ always true if reached - assert_name_is_foo
 test_class_methods.py(31, 4): ✔️ always true if reached - assert_opt_name_none_or_str
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_mixed_init.expected b/StrataTest/Languages/Python/expected_laurel/test_class_mixed_init.expected
index ba94db344c..766329f9a4 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_mixed_init.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_mixed_init.expected
@@ -1,3 +1,4 @@
-test_class_mixed_init.py(15, 0): ✔️ always true if reached - class with init
-DETAIL: 1 passed, 0 failed, 0 inconclusive
-RESULT: Analysis success
+test_class_mixed_init.py(19, 0): ✔️ always true if reached - class with init
+test_class_mixed_init.py(19, 0): ❓ unknown - class with init
+DETAIL: 1 passed, 0 failed, 1 inconclusive
+RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_no_init.expected b/StrataTest/Languages/Python/expected_laurel/test_class_no_init.expected
index 6424100a9e..7228247375 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_no_init.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_no_init.expected
@@ -1,4 +1,4 @@
-test_class_no_init.py(5, 4): ✅ pass - callElimAssert_requires_2
+test_class_no_init.py(5, 4): ✅ pass - callElimAssert_requires_4
 test_class_no_init.py(6, 4): ❓ unknown - class without __init__
 DETAIL: 1 passed, 0 failed, 1 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_no_init_multi_field.expected b/StrataTest/Languages/Python/expected_laurel/test_class_no_init_multi_field.expected
index 33265abfc6..3dbe40b3b6 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_no_init_multi_field.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_no_init_multi_field.expected
@@ -1,4 +1,4 @@
-test_class_no_init_multi_field.py(7, 4): ✅ pass - callElimAssert_requires_2
+test_class_no_init_multi_field.py(7, 4): ✅ pass - callElimAssert_requires_4
 test_class_no_init_multi_field.py(8, 4): ✅ pass - class with multiple annotated fields no init
 DETAIL: 2 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_no_init_with_method.expected b/StrataTest/Languages/Python/expected_laurel/test_class_no_init_with_method.expected
index 9b24703e59..29b6682a29 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_no_init_with_method.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_no_init_with_method.expected
@@ -1,5 +1,5 @@
 test_class_no_init_with_method.py(4, 23): ❓ unknown - (WithMethod@get_x ensures) Return type constraint
-test_class_no_init_with_method.py(8, 4): ✅ pass - callElimAssert_requires_2
+test_class_no_init_with_method.py(8, 4): ✅ pass - callElimAssert_requires_4
 test_class_no_init_with_method.py(9, 4): ✅ pass - class with method but no __init__
 DETAIL: 2 passed, 0 failed, 1 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected b/StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected
index bd04bc0055..1085e02e58 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected
@@ -1,6 +1,6 @@
-test_class_with_methods.py(32, 4): ✔️ always true if reached - main_assert(484)_19
+test_class_with_methods.py(32, 4): ✔️ always true if reached - main_assert(484)_12
 test_class_with_methods.py(32, 4): ✔️ always true if reached - get_count should return 30
-test_class_with_methods.py(32, 4): ✔️ always true if reached - main_assert(569)_21
+test_class_with_methods.py(32, 4): ✔️ always true if reached - main_assert(569)_14
 test_class_with_methods.py(32, 4): ✔️ always true if reached - get_name should return mystore
 test_class_with_methods.py(29, 4): ✔️ always true if reached - assert_name_is_foo
 test_class_with_methods.py(29, 4): ✔️ always true if reached - assert_opt_name_none_or_str
diff --git a/StrataTest/Languages/Python/expected_laurel/test_method_kwargs_no_hierarchy.expected b/StrataTest/Languages/Python/expected_laurel/test_method_kwargs_no_hierarchy.expected
index edd04a23ce..56de827e26 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_method_kwargs_no_hierarchy.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_method_kwargs_no_hierarchy.expected
@@ -8,6 +8,5 @@ test_method_kwargs_no_hierarchy.py(11, 18): ✅ pass - (Calculator@add requires)
 test_method_kwargs_no_hierarchy.py(11, 4): ✅ pass - assert(254)
 test_method_kwargs_no_hierarchy.py(12, 4): ❓ unknown - assert(286)
 test_method_kwargs_no_hierarchy.py(8, 14): ✅ pass - (main ensures) Return type constraint
-test_method_kwargs_no_hierarchy.py(8, 0): ❓ unknown - postcondition_1
-DETAIL: 8 passed, 0 failed, 3 inconclusive
+DETAIL: 8 passed, 0 failed, 2 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/tests/test_class_mixed_init.py b/StrataTest/Languages/Python/tests/test_class_mixed_init.py
index 382a99ec5f..4ec8c031a5 100644
--- a/StrataTest/Languages/Python/tests/test_class_mixed_init.py
+++ b/StrataTest/Languages/Python/tests/test_class_mixed_init.py
@@ -10,6 +10,10 @@ class NoInit:
 
 def test():
     a = WithInit(10)
-    b = NoInit()
     assert a.x == 10, "class with init"
+    b = NoInit()
+    # Previously this passed because Python was incorrectly creating Laurel procedures that were not modifying the heap.
+    # For this to pass, we need transparent procedures with assignment in Laurel, so
+    # NoInit.__init__ can be transparent instead of "opaque modifies *"
+    assert a.x == 10, "class with init" 
 test()
diff --git a/StrataTestExtra/Languages/Python/AnalyzeLaurelTest.lean b/StrataTestExtra/Languages/Python/AnalyzeLaurelTest.lean
index 0b2c761a2e..98c7dc9efc 100644
--- a/StrataTestExtra/Languages/Python/AnalyzeLaurelTest.lean
+++ b/StrataTestExtra/Languages/Python/AnalyzeLaurelTest.lean
@@ -302,10 +302,9 @@ Expected output (when Python + z3 available):
     | .ok vcResults =>
       let mut foundAlwaysFalse := false
       for r in vcResults do
-        if r.obligation.label.startsWith "servicelib_Storage_" then
-          let line := r.formatOutcome
-          if (line.splitOn "✖️").length != 1 then
-            foundAlwaysFalse := true
+        let line := r.formatOutcome
+        if (line.splitOn "✖️").length != 1 then
+          foundAlwaysFalse := true
       if !foundAlwaysFalse then
         throw <| IO.userError
           "Expected ✖️ always false for regex violation"
@@ -327,10 +326,9 @@ assertion. This exercises the full pipeline with type alias resolution.
     | .ok vcResults =>
       let mut foundAlwaysFalse := false
       for r in vcResults do
-        if r.obligation.label.startsWith "servicelib_Storage_" then
-          let line := r.formatOutcome
-          if (line.splitOn "✖️").length != 1 then
-            foundAlwaysFalse := true
+        let line := r.formatOutcome
+        if (line.splitOn "✖️").length != 1 then
+          foundAlwaysFalse := true
       if !foundAlwaysFalse then
         throw <| IO.userError
           "Expected ✖️ always false for empty bucket violation"
diff --git a/StrataTestExtra/Languages/Python/VerifyPythonTest.lean b/StrataTestExtra/Languages/Python/VerifyPythonTest.lean
index f343531250..a8343c61a1 100644
--- a/StrataTestExtra/Languages/Python/VerifyPythonTest.lean
+++ b/StrataTestExtra/Languages/Python/VerifyPythonTest.lean
@@ -340,7 +340,7 @@ def main() -> None:
 "
   let (laurel, output) ← toLaurel pythonCmd program
   let calcAdd := manglePythonMethod "Calculator" "add"
-  assertHasBody laurel calcAdd
+  assertOpaque laurel calcAdd
   unless containsSubstr output s!"{calcAdd}(" do
     throw <| IO.userError s!"Expected '{calcAdd}(' in Laurel output but not found"