diff --git a/Strata/Languages/Laurel/ConstrainedTypeElim.lean b/Strata/Languages/Laurel/ConstrainedTypeElim.lean
index 566dab3ae6..8453b76ca2 100644
--- a/Strata/Languages/Laurel/ConstrainedTypeElim.lean
+++ b/Strata/Languages/Laurel/ConstrainedTypeElim.lean
@@ -71,9 +71,9 @@ def constraintCallFor (ptMap : ConstrainedTypeMap) (ty : HighType)
     (varName : Identifier) (src : Option FileRange := none) : Option StmtExprMd :=
   constraintCallForExpr ptMap ty ⟨.Var (.Local varName), src⟩ src
 
-/-- Generate a constraint function for a constrained type.
-    For nested types, the function calls the parent's constraint function. -/
-def mkConstraintFunc (ptMap : ConstrainedTypeMap) (ct : ConstrainedType) : Procedure :=
+/-- Generate a constraint procedure for a constrained type.
+    For nested types, the procedure calls the parent's constraint procedure. -/
+def mkConstraintProc (ptMap : ConstrainedTypeMap) (ct : ConstrainedType) : Procedure :=
   let baseType := resolveType ptMap ct.base
   let bodyExpr: StmtExprMd := match ct.base.val with
     | .UserDefined parent =>
@@ -90,7 +90,6 @@ def mkConstraintFunc (ptMap : ConstrainedTypeMap) (ct : ConstrainedType) : Proce
     inputs := [{ name := ct.valueName, type := baseType }]
     outputs := [{ name := mkId "result", type := { val := .TBool, source := none } }]
     body := .Transparent { val := .Return bodyExpr, source := none }
-    isFunctional := true
     decreases := none
     preconditions := [] }
 
@@ -166,7 +165,7 @@ def elimProc (ptMap : ConstrainedTypeMap) (model : SemanticModel) (proc : Proced
   let inputRequires : List Condition := proc.inputs.filterMap fun p =>
     (constraintCallFor ptMap p.type.val p.name (src := p.type.source)).map
       fun c => { condition := c }
-  let outputEnsures : List Condition := if proc.isFunctional then [] else proc.outputs.filterMap fun p =>
+  let outputEnsures : List Condition := proc.outputs.filterMap fun p =>
     (constraintCallFor ptMap p.type.val p.name (src := p.type.source)).map
       fun c => { condition := ⟨c.val, p.type.source⟩ }
   let body' := match proc.body with
@@ -174,8 +173,7 @@ def elimProc (ptMap : ConstrainedTypeMap) (model : SemanticModel) (proc : Proced
     let body := elimStmts ptMap model bodyExpr
     if outputEnsures.isEmpty then .Transparent body
     else
-      let retBody := if proc.isFunctional then ⟨.Return (some body), bodyExpr.source⟩ else body
-      .Opaque outputEnsures (some retBody) []
+      .Opaque outputEnsures (some body) []
   | .Opaque postconds impl modif =>
     let impl' := impl.map (elimStmts ptMap model)
     .Opaque (postconds ++ outputEnsures) impl' modif
@@ -206,7 +204,6 @@ private def mkWitnessProc (ptMap : ConstrainedTypeMap) (ct : ConstrainedType) :
     outputs := []
     body := .Opaque [] (some ⟨.Block [witnessInit, assert] none, src⟩) []
     preconditions := []
-    isFunctional := false
     decreases := none }
 
 /-- Eliminate constrained types within a composite type definition: resolve
@@ -227,13 +224,9 @@ public def constrainedTypeElim (model : SemanticModel) (program : Program)
   let ptMap := buildConstrainedTypeMap program.types
   if ptMap.isEmpty then (program, []) else
   let constraintFuncs := program.types.filterMap fun
-    | .Constrained ct => some (mkConstraintFunc ptMap ct) | _ => none
+    | .Constrained ct => some (mkConstraintProc ptMap ct) | _ => none
   let witnessProcedures := program.types.filterMap fun
     | .Constrained ct => some (mkWitnessProc ptMap ct) | _ => none
-  let funcDiags := program.staticProcedures.foldl (init := []) fun acc proc =>
-    if proc.isFunctional && proc.outputs.any (fun p => isConstrainedType ptMap p.type.val) then
-      acc.cons (diagnosticFromSource proc.name.source "constrained return types on functions are not yet supported")
-    else acc
   ({ program with
     staticProcedures := constraintFuncs ++ program.staticProcedures.map (elimProc ptMap model)
                         ++ witnessProcedures
@@ -241,7 +234,7 @@ public def constrainedTypeElim (model : SemanticModel) (program : Program)
       | .Constrained _ => none
       | .Composite ct => some (.Composite (elimCompositeType ptMap model ct))
       | other => some other },
-   funcDiags)
+   [])
 
 /-- Pipeline pass: constrained type elimination. -/
 public def constrainedTypeElimPass : LoweringPass where
diff --git a/Strata/Languages/Laurel/ContractPass.lean b/Strata/Languages/Laurel/ContractPass.lean
index cc93ba02f9..2bd40a46b0 100644
--- a/Strata/Languages/Laurel/ContractPass.lean
+++ b/Strata/Languages/Laurel/ContractPass.lean
@@ -67,7 +67,6 @@ private def mkConditionProc (name : String) (params : List Parameter)
     outputs := [⟨mkId "$result", { val := .TBool, source := none }⟩]
     preconditions := []
     decreases := none
-    isFunctional := true
     body := .Transparent condition.condition }
 
 /-- Suffix appended to a procedure's output-parameter names when they are lowered
@@ -123,7 +122,6 @@ private def mkPostConditionProc (name : String) (inputs outputs : List Parameter
     outputs := [⟨mkId "$result", { val := .TBool, source := none }⟩]
     preconditions := []
     decreases := none
-    isFunctional := true
     body := .Transparent (renameOutputsInPostExpr outputNames condition.condition) }
 
 /-- Information about a procedure's contracts. -/
@@ -142,7 +140,7 @@ private def collectContractInfo (procs : List Procedure) : Std.HashMap String Co
     let postconds := getPostconditions proc.body
     let hasPre := !proc.preconditions.isEmpty
     let hasPost := !postconds.isEmpty
-    if !proc.isFunctional && (hasPre || hasPost) then
+    if hasPre || hasPost then
       let preNames := proc.preconditions.zipIdx.map fun (c, i) =>
         (preCondProcName proc.name.text i, c.summary)
       let postNames := postconds.zipIdx.map fun (c, i) =>
@@ -162,19 +160,19 @@ private def transformProcBody (proc : Procedure) (info : ContractInfo) : Body :=
   let preAssumes : List StmtExprMd :=
     proc.preconditions.zip info.preNames |>.map fun (pc, name, _) =>
       ⟨.Assume (mkCall name inputArgs), pc.condition.source⟩
+  let postAsserts : List StmtExprMd :=
+    postconds.zip info.postNames |>.map fun (pc, _name, _summary) =>
+      let summary := pc.summary.getD "postcondition"
+      ⟨.Assert { condition := pc.condition, summary := some summary }, pc.condition.source⟩
   match proc.body with
   | .Transparent body =>
-    let postAsserts : List StmtExprMd :=
-      postconds.zip info.postNames |>.map fun (pc, _name, _summary) =>
-        let summary := pc.summary.getD "postcondition"
-        ⟨.Assert { condition := pc.condition, summary := some summary }, pc.condition.source⟩
     .Transparent ⟨.Block (preAssumes ++ [body] ++ postAsserts) none, body.source⟩
   | .Opaque _ (some impl) _ =>
-    .Opaque postconds (some ⟨.Block (preAssumes ++ [impl]) none, impl.source⟩) []
+    .Opaque [] (some ⟨.Block (preAssumes ++ [impl] ++ postAsserts) none, impl.source⟩) []
   | .Opaque _ none mods =>
-    .Opaque postconds none mods
+    .Opaque [] none mods
   | .Abstract _ =>
-    .Abstract postconds
+    .Abstract []
   | b => b
 
 /-- Monad used by the contract-pass rewriter; carries a global counter for
@@ -206,15 +204,12 @@ private def mkTempAssignments (args : List StmtExprMd)
   return (decls, refs)
 
 /-- Generate precondition checks (one per precondition) for a call site. -/
-private def mkPreChecks (info : ContractInfo) (isFunctional : Bool)
+private def mkPreChecks (info : ContractInfo)
     (tempRefs : List StmtExprMd) (src : Option FileRange) : List StmtExprMd :=
   if !info.hasPreCondition then []
   else info.preNames.map fun (name, summary) =>
     let call := mkCall name tempRefs
-    if isFunctional then
-      ⟨.Assume call, src⟩
-    else
-      ⟨.Assert { condition := call, summary := some (summary.getD "precondition") }, src⟩
+    ⟨.Assert { condition := call, summary := some (summary.getD "precondition") }, src⟩
 
 /-- Generate postcondition assumes (one per postcondition) for a call site. -/
 private def mkPostAssumes (info : ContractInfo)
@@ -249,12 +244,12 @@ private def mkCallArgs (info : ContractInfo) (origArgs tempRefs : List StmtExprM
 
 /-- Rewrite call sites in a statement/expression tree. -/
 private def rewriteCallSites (contractInfoMap : Std.HashMap String ContractInfo)
-    (isFunctional : Bool) (expr : StmtExprMd) : ContractM StmtExprMd := do
+    (expr : StmtExprMd) : ContractM StmtExprMd := do
   let rewriteStaticCall (callee : Identifier) (args : List StmtExprMd)
       (info : ContractInfo) (src : Option FileRange)
       : ContractM (List StmtExprMd) := do
     let (tempDecls, tempRefs) ← mkTempAssignments args info.inputParams src
-    let preCheck := mkPreChecks info isFunctional tempRefs src
+    let preCheck := mkPreChecks info tempRefs src
     let (callStmt, postAssume, returnValue) ←
       if info.hasPostCondition && !info.outputParams.isEmpty then do
         let mut outputTempDecls : List VariableMd := []
@@ -295,7 +290,7 @@ private def rewriteCallSites (contractInfoMap : Std.HashMap String ContractInfo)
             let (tempDecls, tempRefs) ← mkTempAssignments args' info.inputParams src
             let callArgs := mkCallArgs info args' tempRefs
             let callWithTemps : StmtExprMd := ⟨.Assign targets ⟨.StaticCall callee callArgs, callSrc⟩, src⟩
-            let preCheck := mkPreChecks info isFunctional tempRefs src
+            let preCheck := mkPreChecks info tempRefs src
             let outputArgs := targets.filterMap fun t =>
               match t.val with
               | .Local name => some (mkMd (.Var (.Local name)))
@@ -320,7 +315,7 @@ private def rewriteCallSites (contractInfoMap : Std.HashMap String ContractInfo)
 /-- Rewrite call sites in all bodies of a procedure. -/
 private def rewriteCallSitesInProc (contractInfoMap : Std.HashMap String ContractInfo)
     (proc : Procedure) : ContractM Procedure := do
-  let rw := rewriteCallSites contractInfoMap proc.isFunctional
+  let rw := rewriteCallSites contractInfoMap
   match proc.body with
   | .Transparent body =>
     let body' ← rw body
@@ -412,7 +407,7 @@ def lowerContracts (program : Program) : Program × List DiagnosticModel :=
   let diagnostics := program.staticProcedures.filterMap invokeOnOutputRefError
 
   -- Generate helper procedures for all procedures with contracts
-  let helperProcs := (program.staticProcedures.filter (fun proc => !proc.isFunctional)).flatMap fun proc =>
+  let helperProcs := program.staticProcedures.flatMap fun proc =>
     let postconds := getPostconditions proc.body
     let preProcs := proc.preconditions.zipIdx.map fun (c, i) =>
       mkConditionProc (preCondProcName proc.name.text i) proc.inputs c
@@ -423,28 +418,25 @@ def lowerContracts (program : Program) : Program × List DiagnosticModel :=
   -- Transform procedures: strip contracts, add assume/assert, rewrite call sites
   -- Run all call-site rewriting in a single ContractM to share the global counter.
   let (transformedProcs, _) := (program.staticProcedures.mapM fun (proc : Procedure) => do
-    if proc.isFunctional then
-      return proc
-    else
-      let proc : Procedure := match proc.invokeOn with
-        | some trigger =>
-          let postconds := getPostconditions proc.body
-          if postconds.isEmpty then { proc with invokeOn := none }
-          else if invokeOnOutputRefError proc |>.isSome then
-            -- Skip axiom generation; diagnostic already emitted
-            { proc with invokeOn := none }
-          else { proc with
-            axioms := [mkInvokeOnAxiom proc.inputs trigger proc.preconditions postconds]
-            invokeOn := none }
-        | none => proc
-      let proc : Procedure := match contractInfoMap.get? proc.name.text with
-        | some info =>
-          { proc with
-            preconditions := []
-            body := transformProcBody proc info }
-        | none => proc
-      -- Rewrite call sites in the procedure body
-      rewriteCallSitesInProc contractInfoMap proc).run 0
+    let proc : Procedure := match proc.invokeOn with
+      | some trigger =>
+        let postconds := getPostconditions proc.body
+        if postconds.isEmpty then { proc with invokeOn := none }
+        else if invokeOnOutputRefError proc |>.isSome then
+          -- Skip axiom generation; diagnostic already emitted
+          { proc with invokeOn := none }
+        else { proc with
+          axioms := [mkInvokeOnAxiom proc.inputs trigger proc.preconditions postconds]
+          invokeOn := none }
+      | none => proc
+    let proc : Procedure := match contractInfoMap.get? proc.name.text with
+      | some info =>
+        { proc with
+          preconditions := []
+          body := transformProcBody proc info }
+      | none => proc
+    -- Rewrite call sites in the procedure body
+    rewriteCallSitesInProc contractInfoMap proc).run 0
 
   ({ program with staticProcedures := helperProcs ++ transformedProcs }, diagnostics)
 
diff --git a/Strata/Languages/Laurel/CoreDefinitionsForLaurel.lean b/Strata/Languages/Laurel/CoreDefinitionsForLaurel.lean
index dfe3e09782..d5af1b992a 100644
--- a/Strata/Languages/Laurel/CoreDefinitionsForLaurel.lean
+++ b/Strata/Languages/Laurel/CoreDefinitionsForLaurel.lean
@@ -35,13 +35,13 @@ datatype LaurelUnit { MkLaurelUnit() }
 // And remove the hacky filter in HeapParameterization
 datatype Box { MkBox() }
 
-function select(map: int, key: int) : Box
+procedure select(map: int, key: int) : Box
   external;
 
-function update(map: int, key: int, value: int) : Box
+procedure update(map: int, key: int, value: int) : Box
   external;
 
-function const(value: int) : Box
+procedure const(value: int) : Box
   external;
 
 #end
diff --git a/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean b/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean
index 57007a95a5..eb8e7fa309 100644
--- a/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean
+++ b/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean
@@ -203,8 +203,14 @@ open Std (Format ToFormat)
 
 public section
 
+/-- Format a procedure as a function, replacing the leading "procedure" keyword with "function". -/
+private def formatAsFunction (proc : Procedure) : Format :=
+  let s := (ToFormat.format proc).pretty 100
+  let s := if s.startsWith "procedure" then "function" ++ s.drop "procedure".length else s
+  Format.text s
+
 def formatOrderedDecl : OrderedDecl → Format
-  | .funcs funcs _ => Format.joinSep (funcs.map ToFormat.format) "\n\n"
+  | .funcs funcs _ => Format.joinSep (funcs.map formatAsFunction) "\n\n"
   | .procedure proc => ToFormat.format proc
   | .datatypes dts => Format.joinSep (dts.map ToFormat.format) "\n\n"
   | .constant c => ToFormat.format c
diff --git a/Strata/Languages/Laurel/DesugarShortCircuit.lean b/Strata/Languages/Laurel/DesugarShortCircuit.lean
index b8d65c1e40..4a5c628a20 100644
--- a/Strata/Languages/Laurel/DesugarShortCircuit.lean
+++ b/Strata/Languages/Laurel/DesugarShortCircuit.lean
@@ -50,7 +50,8 @@ private def desugarShortCircuitNode (imperativeCallees : List String) (expr : St
 
 /-- Desugar short-circuit operators in a program. -/
 def desugarShortCircuit (program : Program) : Program :=
-  let imperativeCallees := (program.staticProcedures.filter (!·.isFunctional)).map (·.name.text)
+  let imperativeCallees := program.staticProcedures.map (·.name.text)
+  -- TODO shouldn't imperativeCallees always be empty here?
   mapProgram (mapStmtExpr (desugarShortCircuitNode imperativeCallees)) program
 
 end -- public section
diff --git a/Strata/Languages/Laurel/EliminateDeterministicHoles.lean b/Strata/Languages/Laurel/EliminateDeterministicHoles.lean
index d7286e86c7..6f452c229e 100644
--- a/Strata/Languages/Laurel/EliminateDeterministicHoles.lean
+++ b/Strata/Languages/Laurel/EliminateDeterministicHoles.lean
@@ -34,7 +34,7 @@ structure ElimHoleState where
 
 private abbrev ElimHoleM := StateM ElimHoleState
 
-/-- Generate a fresh uninterpreted function for a typed hole and return a call to it. -/
+/-- Generate a fresh uninterpreted procedure for a typed hole and return a call to it. -/
 private def mkHoleCall (source : Option FileRange) (holeType : HighTypeMd) : ElimHoleM StmtExprMd := do
   let s ← get
   let n := s.counter
@@ -47,7 +47,6 @@ private def mkHoleCall (source : Option FileRange) (holeType : HighTypeMd) : Eli
     outputs := [{ name := "$result", type := holeType }]
     preconditions := []
     decreases := none
-    isFunctional := true
     body := .Opaque [] none []
   }
   modify fun s => { s with generatedFunctions := s.generatedFunctions ++ [holeProc] }
diff --git a/Strata/Languages/Laurel/EliminateReturnStatements.lean b/Strata/Languages/Laurel/EliminateReturnStatements.lean
index d2a7743765..5ebec71f08 100644
--- a/Strata/Languages/Laurel/EliminateReturnStatements.lean
+++ b/Strata/Languages/Laurel/EliminateReturnStatements.lean
@@ -24,10 +24,8 @@ namespace Strata.Laurel
 
 public section
 
-private def returnLabel : String := "$return"
-
-
-
+@[expose, match_pattern]
+public def returnLabel : String := "$return"
 
 /-- Transform a single procedure: wrap body in a labelled block and replace returns. -/
 private def eliminateReturnStmts (proc : Procedure) : Procedure :=
diff --git a/Strata/Languages/Laurel/EliminateValueInReturns.lean b/Strata/Languages/Laurel/EliminateValueInReturns.lean
index d209465bf6..77663f9b6b 100644
--- a/Strata/Languages/Laurel/EliminateValueInReturns.lean
+++ b/Strata/Languages/Laurel/EliminateValueInReturns.lean
@@ -56,7 +56,7 @@ def hasValuedReturn (stmt : StmtExprMd) : Bool :=
 
 /-- Apply value-return elimination to a single procedure. Rewrites `return expr`
     into `outParam := expr; return` for any procedure with exactly one output
-    parameter (functional and non-functional alike).
+    parameter.
     Emits an error if a valued return is used with zero or multiple output parameters. -/
 def eliminateValueReturnsInProc (proc : Procedure) : Procedure :=
   match proc.outputs with
diff --git a/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean
index 145c39694f..8dc17d952e 100644
--- a/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean
+++ b/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean
@@ -233,7 +233,6 @@ private def modifiesClausesToArgs (modifies : List StmtExprMd) : Array Arg :=
   wildcardArgs ++ specificArgs
 
 private def procedureToOp (proc : Procedure) : StrataDDM.Operation :=
-  let opName := if proc.isFunctional then "function" else "procedure"
   let params := proc.inputs.map parameterToArg |>.toArray
   let returnTypeArg : Arg :=
     match proc.outputs with
@@ -256,14 +255,7 @@ private def procedureToOp (proc : Procedure) : StrataDDM.Operation :=
     laurelOp "invokeOnClause" #[stmtExprToArg e])
   let (opaqueSpecArg, bodyArg) := match proc.body with
     | .Transparent body =>
-      -- For functions, the body is implicitly wrapped in a Return by ConcreteToAbstract;
-      -- unwrap it here so the concrete output doesn't show an explicit `return`.
-      let emitBody := if proc.isFunctional then
-        match body.val with
-        | .Return (some inner) => inner
-        | _ => body
-      else body
-      (optionArg none, optionArg (some (laurelOp "body" #[stmtExprToArg emitBody])))
+      (optionArg none, optionArg (some (laurelOp "body" #[stmtExprToArg body])))
     | .Opaque postconds impl modifies =>
       let ens := postconds.map ensuresClauseToArg |>.toArray
       let mods := if modifies.isEmpty then #[] else modifiesClausesToArgs modifies
@@ -275,7 +267,7 @@ private def procedureToOp (proc : Procedure) : StrataDDM.Operation :=
     | .External =>
       (optionArg none, optionArg (some (laurelOp "externalBody")))
   { ann := sr
-    name := { dialect := "Laurel", name := opName }
+    name := { dialect := "Laurel", name := "procedure" }
     args := #[
       ident proc.name.text,
       commaSep params,
diff --git a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
index bf5e10dd12..78673dfeaa 100644
--- a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
+++ b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
@@ -150,7 +150,6 @@ instance : Inhabited Procedure where
     outputs := []
     preconditions := []
     decreases := none
-    isFunctional := false
     invokeOn := none
     body := .Transparent { val := .LiteralBool true, source := none }
   }
@@ -354,7 +353,7 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExprMd := do
       let cond ← translateStmtExpr condArg
       let invariants ← translateInvariantClauses translateStmtExpr invSeqArg
       let body ← translateStmtExpr bodyArg
-      return mkStmtExprMd (.While cond invariants none body) src
+      return mkStmtExprMd (.While cond invariants none body false) src
     | q`Laurel.forLoop, #[initArg, condArg, stepArg, invSeqArg, bodyArg] =>
       let init ← translateStmtExpr initArg
       let cond ← translateStmtExpr condArg
@@ -362,7 +361,7 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExprMd := do
       let invariants ← translateInvariantClauses translateStmtExpr invSeqArg
       let body ← translateStmtExpr bodyArg
       let whileBody := mkStmtExprMd (.Block [body, step] none) src
-      let whileStmt := mkStmtExprMd (.While cond invariants none whileBody) src
+      let whileStmt := mkStmtExprMd (.While cond invariants none whileBody false) src
       return mkStmtExprMd (.Block [init, whileStmt] none) src
     | q`Laurel.doWhile, #[bodyArg, condArg, invSeqArg] =>
       -- A `do … while` is a post-test `While`. The `EliminateDoWhile` pass
@@ -568,11 +567,6 @@ def parseProcedure (arg : Arg) : TransM Procedure := do
         | _, _ => TransM.error s!"Expected body or externalBody operation, got {repr bodyOp.name}"
       | .option _ none => pure none
       | _ => TransM.error s!"Expected body, got {repr bodyArg}"
-    -- For functions, wrap the body in a Return so the last expression
-    -- is treated as the return value by downstream passes.
-    let body := if op.name == q`Laurel.function then
-      body.map fun b => ⟨.Return (some b), b.source⟩
-    else body
     -- Determine procedure body kind
     let procBody :=
       if isExternal then Body.External
@@ -586,7 +580,6 @@ def parseProcedure (arg : Arg) : TransM Procedure := do
       outputs := returnParameters
       preconditions := preconditions
       decreases := none
-      isFunctional := op.name == q`Laurel.function
       invokeOn := invokeOn
       body := procBody
     }
diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
index 53f0c33f99..9d2ec74e72 100644
--- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
+++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
@@ -118,7 +118,7 @@ category ElseBranch;
 op elseBranch(stmts : StmtExpr) : ElseBranch => @[prec(0)] "\nelse " stmts;
 
 op ifThenElse (cond: StmtExpr, thenBranch: StmtExpr, elseBranch: Option ElseBranch): StmtExpr =>
-  @[prec(20)] "if " cond "\nthen " thenBranch:0 elseBranch:0;
+  @[prec(20)] "if " cond indent(2, "\nthen " thenBranch:0 elseBranch:0);
 
 op assert (cond : StmtExpr, errorMessage: Option ErrorSummary) : StmtExpr => @[prec(0)] "assert " cond:0 errorMessage:0;
 op assume (cond : StmtExpr) : StmtExpr => @[prec(0)] "assume " cond:0;
@@ -210,15 +210,6 @@ op procedure (name : Ident, parameters: CommaSepBy Parameter,
   body : Option Body) : Procedure =>
   "procedure " name "(" parameters ")" returnType returnParameters requires invokeOn opaqueSpec body ";";
 
-op function (name : Ident, parameters: CommaSepBy Parameter,
-  returnType: Option ReturnType,
-  returnParameters: Option ReturnParameters,
-  requires: Seq RequiresClause,
-  invokeOn: Option InvokeOnClause,
-  opaqueSpec: Option OpaqueSpec,
-  body : Option Body) : Procedure =>
-  "function " name "(" parameters ")" returnType returnParameters requires invokeOn opaqueSpec body ";";
-
 op composite (name: Ident, extending: Option Extends, fields: Seq Field, procedures: Seq Procedure): Composite => "composite " name extending " {" fields procedures " }";
 
 category ConstrainedType;
diff --git a/Strata/Languages/Laurel/HeapParameterizationConstants.lean b/Strata/Languages/Laurel/HeapParameterizationConstants.lean
index a9c6e80206..c81bd0022d 100644
--- a/Strata/Languages/Laurel/HeapParameterizationConstants.lean
+++ b/Strata/Languages/Laurel/HeapParameterizationConstants.lean
@@ -50,22 +50,19 @@ datatype Heap {
 }
 
 // Read a field from the heap: readField(heap, obj, field) = Heap..data!(heap)[obj][field]
-function readField(heap: Heap, obj: Composite, field: Field): Box {
-  select(select(Heap..data!(heap), obj), field)
-};
+procedure readField(heap: Heap, obj: Composite, field: Field): Box
+  return select(select(Heap..data!(heap), obj), field);
 
 // Update a field in the heap
-function updateField(heap: Heap, obj: Composite, field: Field, val: Box): Heap {
-  MkHeap(
+procedure updateField(heap: Heap, obj: Composite, field: Field, val: Box): Heap
+  return MkHeap(
     update(Heap..data!(heap), obj,
       update(select(Heap..data!(heap), obj), field, val)),
-    Heap..nextReference!(heap))
-};
+    Heap..nextReference!(heap));
 
 // Increment the heap allocation nextReference, returning a new heap
-function increment(heap: Heap): Heap {
-  MkHeap(Heap..data!(heap), Heap..nextReference!(heap) + 1)
-};
+procedure increment(heap: Heap): Heap
+  return MkHeap(Heap..data!(heap), Heap..nextReference!(heap) + 1);
 
 #end
 
diff --git a/Strata/Languages/Laurel/InlineLocalVariables.lean b/Strata/Languages/Laurel/InlineLocalVariables.lean
new file mode 100644
index 0000000000..6fc5a5ed5e
--- /dev/null
+++ b/Strata/Languages/Laurel/InlineLocalVariables.lean
@@ -0,0 +1,228 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+public import Strata.Languages.Laurel.LaurelPass
+public import Strata.Languages.Laurel.UnorderedCore
+import Strata.Languages.Laurel.LaurelAST
+import Strata.Languages.Laurel.TransparencyPass
+
+/-!
+## Inline Local Variables Pass
+
+Runs after the transparency pass and operates **only on functions** (the
+`$asFunction` copies produced by the transparency pass). Function bodies are
+pure expressions and cannot contain local variable declarations once they reach
+the Core schema translation. This pass eliminates them by inlining.
+
+For each local variable of the form `var <name> := <expr>`, every reference to
+`<name>` that occurs after the declaration is replaced with `<expr>`, and the
+declaration itself is dropped. The inlined expression is itself inlined first,
+so chains like
+
+```
+var a := 1;
+var b := a + 1;
+```
+
+become `b ↦ 1 + 1`.
+
+Because functions are pure, an inlined variable is never reassigned. Any
+assignment to such a `<name>` is therefore a user error and emits a diagnostic.
+-/
+
+namespace Strata.Laurel
+
+/-- Substitution from an inlined local variable name to the expression it was
+    initialized with. Newer bindings are pushed to the front so `List.lookup`
+    finds the most recent declaration first. -/
+private abbrev InlineSubst := List (Identifier × StmtExprMd)
+
+/-- Diagnostics are accumulated in the state. -/
+private abbrev InlineM := StateM (Array DiagnosticModel)
+
+private def emitDiag (d : DiagnosticModel) : InlineM Unit :=
+  modify (·.push d)
+
+public section
+
+mutual
+
+/--
+Inline local variables within an expression, given the substitution in scope.
+
+Only `Block` nodes introduce new (sequential) scope, so the substitution is not
+threaded back out of `inlineExpr`; child expressions simply inherit `subst`.
+-/
+private partial def inlineExpr (subst : InlineSubst) (expr : StmtExprMd) : InlineM StmtExprMd := do
+  let source := expr.source
+  match expr.val with
+  | .Var (.Local name) =>
+    match subst.lookup name with
+    | some replacement => return replacement
+    | none => return expr
+  | .Var (.Field target fieldName) =>
+    return ⟨.Var (.Field (← inlineExpr subst target) fieldName), source⟩
+  | .Var (.Declare _) => return expr
+
+  | .Block stmts label =>
+    let stmts' ← inlineBlockStmts subst stmts
+    return ⟨.Block stmts' label, source⟩
+
+  | .Assign targets value =>
+    -- An assignment to an inlined local is contradictory: report it.
+    for t in targets do
+      match t.val with
+      | .Local name =>
+        if (subst.lookup name).isSome then
+          emitDiag (diagnosticFromSource (t.source.orElse fun _ => source)
+            s!"cannot assign to '{name.text}': it is an inlined local variable")
+      | _ => pure ()
+    let targets' ← targets.mapM (inlineVariable subst)
+    let value' ← inlineExpr subst value
+    return ⟨.Assign targets' value', source⟩
+
+  | .IfThenElse cond th el =>
+    let cond' ← inlineExpr subst cond
+    let th' ← inlineExpr subst th
+    let el' ← el.mapM (inlineExpr subst)
+    return ⟨.IfThenElse cond' th' el', source⟩
+
+  | .While cond invs dec body postTest =>
+    let cond' ← inlineExpr subst cond
+    let invs' ← invs.mapM (inlineExpr subst)
+    let dec' ← dec.mapM (inlineExpr subst)
+    let body' ← inlineExpr subst body
+    return ⟨.While cond' invs' dec' body' postTest, source⟩
+
+  | .Return value =>
+    return ⟨.Return (← value.mapM (inlineExpr subst)), source⟩
+
+  | .PrimitiveOp op args skipProof =>
+    return ⟨.PrimitiveOp op (← args.mapM (inlineExpr subst)) skipProof, source⟩
+
+  | .StaticCall callee args =>
+    return ⟨.StaticCall callee (← args.mapM (inlineExpr subst)), source⟩
+
+  | .InstanceCall target callee args =>
+    let target' ← inlineExpr subst target
+    let args' ← args.mapM (inlineExpr subst)
+    return ⟨.InstanceCall target' callee args', source⟩
+
+  | .PureFieldUpdate target fieldName newValue =>
+    let target' ← inlineExpr subst target
+    let newValue' ← inlineExpr subst newValue
+    return ⟨.PureFieldUpdate target' fieldName newValue', source⟩
+
+  | .ReferenceEquals lhs rhs =>
+    return ⟨.ReferenceEquals (← inlineExpr subst lhs) (← inlineExpr subst rhs), source⟩
+
+  | .AsType target ty =>
+    return ⟨.AsType (← inlineExpr subst target) ty, source⟩
+
+  | .IsType target ty =>
+    return ⟨.IsType (← inlineExpr subst target) ty, source⟩
+
+  | .Quantifier mode param trigger body =>
+    -- The bound variable shadows any inlined local of the same name.
+    let innerSubst := subst.filter (·.1 != param.name)
+    let trigger' ← trigger.mapM (inlineExpr innerSubst)
+    let body' ← inlineExpr innerSubst body
+    return ⟨.Quantifier mode param trigger' body', source⟩
+
+  | .Assigned name =>
+    return ⟨.Assigned (← inlineExpr subst name), source⟩
+
+  | .Old value =>
+    return ⟨.Old (← inlineExpr subst value), source⟩
+
+  | .Fresh value =>
+    return ⟨.Fresh (← inlineExpr subst value), source⟩
+
+  | .Assert cond =>
+    return ⟨.Assert { cond with condition := ← inlineExpr subst cond.condition }, source⟩
+
+  | .Assume cond =>
+    return ⟨.Assume (← inlineExpr subst cond), source⟩
+
+  | .ProveBy value proof =>
+    return ⟨.ProveBy (← inlineExpr subst value) (← inlineExpr subst proof), source⟩
+
+  | .ContractOf ty func =>
+    return ⟨.ContractOf ty (← inlineExpr subst func), source⟩
+
+  | .IncrDecr mode op target =>
+    return ⟨.IncrDecr mode op (← inlineVariable subst target), source⟩
+
+  -- Leaves: nothing to inline.
+  | .Exit _ | .LiteralInt _ | .LiteralBool _ | .LiteralString _ | .LiteralDecimal _
+  | .LiteralBv _ _ | .New _ | .This | .Abstract | .All | .Hole .. => return expr
+
+/-- Inline within the target expression of a field variable; other variable
+    forms have no sub-expressions to rewrite. -/
+private partial def inlineVariable (subst : InlineSubst) (v : VariableMd) : InlineM VariableMd := do
+  match v.val with
+  | .Field target fieldName =>
+    return ⟨.Field (← inlineExpr subst target) fieldName, v.source⟩
+  | _ => return v
+
+/--
+Process the statements of a block sequentially, threading the substitution.
+
+A `var <name> := <expr>` declaration (`Assign` with a single `Declare` target)
+is removed, and `<name>` is bound to the inlined `<expr>` for the remaining
+statements. All other statements are inlined under the current substitution.
+-/
+private partial def inlineBlockStmts (subst : InlineSubst) (stmts : List StmtExprMd) : InlineM (List StmtExprMd) := do
+  match stmts with
+  | [] => return []
+  | stmt :: rest =>
+    match stmt.val with
+    | .Assign [⟨.Declare param, _⟩] value =>
+      let value' ← inlineExpr subst value
+      inlineBlockStmts ((param.name, value') :: subst) rest
+    | _ =>
+      let stmt' ← inlineExpr subst stmt
+      let rest' ← inlineBlockStmts subst rest
+      return stmt' :: rest'
+
+end
+
+/-- Inline local variables in a single function, returning the rewritten
+    procedure and any diagnostics. -/
+def inlineLocalVariablesInFunction (proc : Procedure) : Procedure × Array DiagnosticModel :=
+  match proc.body with
+  | .Transparent body =>
+    let (body', diags) := (inlineExpr [] body).run #[]
+    ({ proc with body := .Transparent body' }, diags)
+  | .Opaque postconds impl modif =>
+    match impl with
+    | some i =>
+      let (i', diags) := (inlineExpr [] i).run #[]
+      ({ proc with body := .Opaque postconds (some i') modif }, diags)
+    | none => (proc, #[])
+  | _ => (proc, #[])
+
+/-- Inline local variables in every function of an `UnorderedCoreWithLaurelTypes`.
+    Only `functions` are transformed; `coreProcedures` are left unchanged. -/
+def inlineLocalVariablesInFunctions (uc : UnorderedCoreWithLaurelTypes)
+    : UnorderedCoreWithLaurelTypes × List DiagnosticModel :=
+  let results := uc.functions.map inlineLocalVariablesInFunction
+  let functions' := results.map (·.1)
+  let diags := results.flatMap (·.2.toList)
+  ({ uc with functions := functions' }, diags)
+
+public def inlineLocalVariablesPass : LaurelPass UnorderedCoreWithLaurelTypes UnorderedCoreWithLaurelTypes where
+  name := "InlineLocalVariablesPass"
+  documentation := "Inlines local variable declarations of the form `var <name> := <expr>` in function bodies. References to the variable after its declaration are replaced with the initializer expression, and the declaration is removed. Assignments to an inlined variable emit a diagnostic. Operates only on functions, which are pure and cannot carry local variable declarations into Core."
+  comesAfter := [⟨ transparencyPass.meta, "Inlining of local variables in functions only makes sense after the transparency pass has created the functions"⟩]
+  run := fun p _ _ =>
+    let (uc, diags) := inlineLocalVariablesInFunctions p
+    (uc, diags, {})
+
+end -- public section
+
+end Strata.Laurel
diff --git a/Strata/Languages/Laurel/LaurelAST.lean b/Strata/Languages/Laurel/LaurelAST.lean
index fb02d7cd59..8b22a19cfe 100644
--- a/Strata/Languages/Laurel/LaurelAST.lean
+++ b/Strata/Languages/Laurel/LaurelAST.lean
@@ -221,8 +221,6 @@ structure Procedure : Type where
   preconditions : List Condition
   /-- Optional termination measure for recursive procedures. -/
   decreases : Option (AstNode StmtExpr) -- optionally prove termination
-  /-- If true, the body may only have functional constructs, so no destructive assignments or loops. -/
-  isFunctional : Bool
   /-- The procedure body: transparent, opaque, or abstract. -/
   body : Body
   /-- Optional trigger for auto-invocation. When present, the translator also emits an axiom
@@ -315,7 +313,7 @@ inductive StmtExpr : Type where
   | While (cond : AstNode StmtExpr) (invariants : List (AstNode StmtExpr))
     (decreases : Option (AstNode StmtExpr))
     (body : AstNode StmtExpr)
-    (postTest : Bool := false)
+    (postTest : Bool)
   /-- Exit a labelled block. Models `break` and `continue` statements. -/
   | Exit (target : String)
   /-- Return from the enclosing procedure with an optional value. -/
diff --git a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
index 298b93f1b6..fd72ede2ee 100644
--- a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
+++ b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
@@ -21,6 +21,7 @@ import Strata.Languages.Laurel.CoreDefinitionsForLaurel
 import Strata.Languages.Laurel.CoreGroupingAndOrdering
 import Strata.Languages.Laurel.TransparencyPass
 import Strata.Languages.Laurel.LiftImperativeExpressions
+import Strata.Languages.Laurel.InlineLocalVariables
 import Strata.Languages.Laurel.ConstrainedTypeElim
 import Strata.Languages.Laurel.ContractPass
 import Strata.Languages.Laurel.PushOldInward
@@ -172,7 +173,8 @@ private def runLaurelPasses
 
 /-- The ordered sequence of passes on the unordered Core representation. -/
 private def unorderedCorePipeline : Array (LaurelPass UnorderedCoreWithLaurelTypes UnorderedCoreWithLaurelTypes) := #[
-  liftImperativeExpressionsPass
+  liftImperativeExpressionsPass,
+  inlineLocalVariablesPass
 ]
 
 /--
@@ -211,9 +213,12 @@ def translateWithLaurel (options : LaurelTranslateOptions) (program : Program)
   emit "transparencyPass" "core.st" unorderedCore
   let mut unorderedCore := unorderedCore
   let mut fnModel := model
+  let mut ucDiags : List DiagnosticModel := []
 
   for pass in unorderedCorePipeline do
-    unorderedCore := (pass.run unorderedCore fnModel options).1
+    let (uc, passPassDiags, _) := pass.run unorderedCore fnModel options
+    unorderedCore := uc
+    ucDiags := ucDiags ++ passPassDiags
     if pass.needsResolves then
       let compositeTypes := program.types.filter (fun t => match t with | .Composite _ => true | _ => false)
       let (uc', m', errors) := resolveUnorderedCore unorderedCore (some fnModel) compositeTypes
@@ -222,16 +227,22 @@ def translateWithLaurel (options : LaurelTranslateOptions) (program : Program)
           { d with message :=
               s!"Internal error: resolution after '{pass.name}' introduced this diagnostic: {d.message}" }
         emit pass.name "unorderedCoreWithLaurelTypes.st" unorderedCore
-        return (none, passDiags ++ newDiags, program, stats)
+        return (none, passDiags ++ ucDiags ++ newDiags, program, stats)
       unorderedCore := uc'
       fnModel := m'
     emit pass.name "unorderedCoreWithLaurelTypes.st" unorderedCore
 
+  -- An error introduced by an unordered-core pass (e.g. an assignment to an
+  -- inlined local) prevents producing a Core program, just like Laurel pass
+  -- errors above.
+  if ucDiags.any (·.type != .Warning) then
+    return (none, passDiags ++ ucDiags, program, stats)
+
   let coreWithLaurelTypes := (orderingPass.run unorderedCore model options).1
 
   emit "CoreWithLaurelTypes" "core.st" coreWithLaurelTypes
   let (coreProgram, coreDiagnostics, _) := laurelToCoreSchemaPass.run coreWithLaurelTypes fnModel options
-  let mut allDiagnostics: List DiagnosticModel := passDiags ++ coreDiagnostics;
+  let mut allDiagnostics: List DiagnosticModel := passDiags ++ ucDiags ++ coreDiagnostics;
 
   emit "Core" "core.st" coreProgram
   let coreProgramOption :=
diff --git a/Strata/Languages/Laurel/LaurelToCoreSchemaPass.lean b/Strata/Languages/Laurel/LaurelToCoreSchemaPass.lean
index 3c6cda03cd..fae00baae7 100644
--- a/Strata/Languages/Laurel/LaurelToCoreSchemaPass.lean
+++ b/Strata/Languages/Laurel/LaurelToCoreSchemaPass.lean
@@ -9,6 +9,7 @@ public import Strata.Languages.Core.Program
 public import Strata.Languages.Core.Options
 public import Strata.Languages.Laurel.PushOldInward
 public import Strata.Languages.Laurel.CoreGroupingAndOrdering
+public import Strata.Languages.Laurel.EliminateReturnStatements
 import Strata.Languages.Laurel.Grammar.AbstractToConcreteTreeTranslator
 import Strata.Util.Tactics
 public import Strata.Languages.Laurel.Resolution
@@ -59,10 +60,15 @@ structure TranslateState where
       why the program was deemed invalid so that if no other diagnostics explain
       the suppression, these can be surfaced to the user. -/
   coreDiagnostics : List DiagnosticModel := []
+  procedureNames: Std.HashSet String
 
 /-- The translation monad: state over Except, allowing both accumulated diagnostics and hard failures -/
 @[expose] abbrev TranslateM := OptionT (StateM TranslateState)
 
+/-- Emit a diagnostic into the translation state (soft warning, does not abort) -/
+def containsProcedure (name : Identifier) : TranslateM Bool := do
+  return (← get).procedureNames.contains name.text
+
 /-- Emit a diagnostic into the translation state (soft warning, does not abort) -/
 def emitDiagnostic (d : DiagnosticModel) : TranslateM Unit :=
   modify fun s => { s with diagnostics := s.diagnostics ++ [d] }
@@ -225,7 +231,7 @@ def translateExpr (expr : StmtExprMd)
       return .ite () bcond bthen belse
   | .StaticCall callee args =>
       -- In a pure context, only Core functions (not procedures) are allowed
-      if isPureContext && !model.isFunction callee then
+      if isPureContext && (← containsProcedure callee) then
         disallowed expr.source s!"calls to procedures are not supported in functions or contracts"
       else
         let fnOp : Core.Expression.Expr := .op () ⟨callee.text, ()⟩ none
@@ -259,7 +265,7 @@ def translateExpr (expr : StmtExprMd)
       throwExprDiagnostic $ diagnosticFromSource expr.source
         "IncrDecr should have been eliminated by EliminateIncrDecr pass" DiagnosticType.StrataBug
   | .While _ _ _ _ _ =>
-      disallowed expr.source "loops are not supported in functions or contracts"
+      disallowed expr.source "loops are not supported in transparent bodies or contracts"
   | .Exit _ => disallowed expr.source "exit is not supported in expression position"
 
   | .Block (⟨ .Assert _, innerSrc⟩ :: rest) label => do
@@ -272,9 +278,11 @@ def translateExpr (expr : StmtExprMd)
       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
+      disallowed innerSrc "local variables in transparent bodies are not YET supported"
+      -- This doesn't work because of a limitation in Core.
+      -- return .app () (.abs () (some coreMonoType) bodyExpr) valueExpr
   | .Block (⟨ .Var (.Declare _), innerSrc⟩ :: rest) label => do
-    _ ← disallowed innerSrc "local variables in functions must have initializers"
+    _ ← disallowed innerSrc "local variables must have initializers in transparent bodies or contracts "
     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"
@@ -419,8 +427,6 @@ Diagnostics are emitted into the monad state.
 -/
 def translateStmt (stmt : StmtExprMd)
     : TranslateM (List Core.Statement) := do
-  let s ← get
-  let model := s.model
   let md := astNodeToCoreMd stmt
   match _h : stmt.val with
   | .Assert cond =>
@@ -493,7 +499,9 @@ def translateStmt (stmt : StmtExprMd)
       -- Match on the value to decide how to translate
       match _hv : value.val with
       | .StaticCall callee args =>
-        if model.isFunction callee then
+        if (← containsProcedure callee) then
+          translateCallTargets callee args
+        else
           -- Function call: translate as a normal expression assignment
           let coreExpr ← translateExpr value
           match targets with
@@ -504,8 +512,6 @@ def translateStmt (stmt : StmtExprMd)
             return result
           | _ =>
             throwStmtDiagnostic $ md.toDiagnostic "function call without a single target" DiagnosticType.StrataBug
-        else
-          translateCallTargets callee args
       | .InstanceCall _target callee args =>
           translateCallTargets callee args
       | .Hole _ _ =>
@@ -531,7 +537,7 @@ def translateStmt (stmt : StmtExprMd)
       return [Imperative.Stmt.ite (.det bcond) bthen belse md]
   | .StaticCall callee args =>
       -- Check if this is a function or procedure
-      if model.isFunction callee then
+      if !(← containsProcedure callee) then
         -- Function call in statement position: preserve as unused init
         exprAsUnusedInit stmt md
       else
@@ -672,10 +678,12 @@ instance : Inhabited LaurelVerifyOptions where
   default := {}
 
 /-- Unwrap the pattern produced by EliminateValuesInReturns + EliminateReturnStatements:
-    `{ result := <expr>; exit "$return" } $return` → `<expr>` -/
+    `{ result := <expr>; exit "$return" } $return` → `<expr>`
+    Support for transparent multi-out procedures is not yet available.
+-/
 private def unwrapReturnBlock (b : StmtExprMd) : StmtExprMd :=
   match b.val with
-  | .Block [⟨.Assign [⟨.Local _, _⟩] value, _⟩, ⟨.Exit "$return", _⟩] (some "$return") => value
+  | .Block [⟨.Assign [⟨.Local _, _⟩] value, _⟩, ⟨.Exit returnLabel, _⟩] (some returnLabel) => value
   | _ => b
 
 /--
@@ -807,7 +815,13 @@ public def laurelToCoreSchemaPass : LaurelPass CoreWithLaurelTypes Core.Program
   - Laurel parameter definitions are translated to Core ones.
   - Laurel calling conventions are translated to Core ones."
   run := fun p fnModel options =>
-    let initState : TranslateState := { model := fnModel, overflowChecks := options.overflowChecks }
+    let initState : TranslateState := {
+      model := fnModel,
+      overflowChecks := options.overflowChecks,
+      procedureNames := p.decls.foldl (fun r d => match d with
+        | .procedure p => r.insert p.name.text
+        | _ => r ) (Std.HashSet.emptyWithCapacity 0)
+    }
     let (coreProgramOption, translateState) :=
       runTranslateM initState (translateLaurelToCore options p)
     let diagnostics : List DiagnosticModel :=
diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean
index 971bafbf91..f3dcf5e050 100644
--- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean
+++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean
@@ -198,10 +198,18 @@ def containsAssignmentOrImperativeCall (imperativeCallees : List String) (expr :
 mutual
 
 def asLifted { t: Type } (runner: LiftM t) : LiftM t := do
-  let savedState ← get
+  -- Save only the bookkeeping that `runner` is meant to run in a fresh
+  -- sub-scope (`prependedStmts` and `subst`). We must NOT restore the whole
+  -- state: the monotonic counters (`condCounter`, `varCounters`) advanced by
+  -- `runner` reflect fresh names (e.g. `$cndtn_N`) that escape into the output
+  -- via the returned/prepended statements. Rolling those counters back would
+  -- let a later `freshTempVar`/`freshTempFor` reuse the same name, producing a
+  -- duplicate definition in the same scope.
+  let savedPrepends := (← get).prependedStmts
+  let savedSubst := (← get).subst
   modify fun s => { s with prependedStmts := [], subst := []}
   let result ← runner
-  modify fun _ => savedState
+  modify fun s => { s with prependedStmts := savedPrepends, subst := savedSubst }
   return result
 
 /--
@@ -422,14 +430,14 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do
       let seqRet ← transformExpr retExpr
       return ⟨.Return (some seqRet), source⟩
 
-  | .While cond invs dec body =>
+  | .While cond invs dec body postTest =>
       let seqCond ← transformExpr cond
       let seqInvs ← invs.mapM transformExpr
       let seqDec ← match dec with
         | some d => pure (some (← transformExpr d))
         | none => pure none
       let seqBody ← transformExpr body
-      return ⟨.While seqCond seqInvs seqDec seqBody, source⟩
+      return ⟨.While seqCond seqInvs seqDec seqBody postTest, source⟩
 
   | .PureFieldUpdate target fieldName newValue =>
       let seqTarget ← transformExpr target
diff --git a/Strata/Languages/Laurel/MergeAndLiftReturns.lean b/Strata/Languages/Laurel/MergeAndLiftReturns.lean
index 06f44102d1..c0f4b7c614 100644
--- a/Strata/Languages/Laurel/MergeAndLiftReturns.lean
+++ b/Strata/Languages/Laurel/MergeAndLiftReturns.lean
@@ -43,6 +43,8 @@ def removeReturns (stmt : StmtExprMd) : Except DiagnosticModel StmtExprMd :=
     | .Assert _ => .ok passThrough
     | .Block _ _ => .ok passThrough
     | .IfThenElse _ _ (some _) => .error (diagnosticFromSource head.source "in a transparent body, if-then-else is only supported as the last statement in a block")
+    | .While _ _ _ _ _ => .error $ diagnosticFromSource head.source $ "loops are not supported in transparent bodies or contracts"
+    | .Var (.Declare _) => .error $ diagnosticFromSource head.source $ "local variables must have initializers in transparent bodies or contracts"
     | _ => .error (diagnosticFromSource head.source
         s!"unsupported statement {head.val.constructorName} in block head")
   | .IfThenElse cond thenBr (some elseBr) => do
diff --git a/Strata/Languages/Laurel/Resolution.lean b/Strata/Languages/Laurel/Resolution.lean
index a3e3e5090d..19fe71115b 100644
--- a/Strata/Languages/Laurel/Resolution.lean
+++ b/Strata/Languages/Laurel/Resolution.lean
@@ -2634,7 +2634,6 @@ def resolveProcedure (proc : Procedure) : ResolveM Procedure := do
     let invokeOn' ← proc.invokeOn.mapM resolveStmtExpr
     let axioms' ← proc.axioms.mapM resolveStmtExpr
     return { name := procName', inputs := inputs', outputs := outputs',
-             isFunctional := proc.isFunctional,
              preconditions := pres', decreases := dec',
              invokeOn := invokeOn',
              axioms := axioms',
@@ -2673,7 +2672,6 @@ def resolveInstanceProcedure (typeName : Identifier) (proc : Procedure) : Resolv
     modify fun s => { s with instanceTypeName := savedInstType }
     let axioms' ← proc.axioms.mapM resolveStmtExpr
     return { name := procName', inputs := inputs', outputs := outputs',
-             isFunctional := proc.isFunctional,
              preconditions := pres', decreases := dec',
              invokeOn := invokeOn',
              axioms := axioms',
@@ -2770,7 +2768,6 @@ private def mkTesterProcedure (dt : DatatypeDefinition) (ctor : DatatypeConstruc
     outputs := [outputParam]
     preconditions := []
     decreases := none
-    isFunctional := true
     body := .External }
 
 /-- Insert a definition into the refToDef map using the ID already on the identifier. -/
@@ -3144,32 +3141,6 @@ public def resolve (program : Program) (existingModel: Option SemanticModel := n
 
 /-! ## Resolution for UnorderedCoreWithLaurelTypes -/
 
-/--
-Convert an `UnorderedCoreWithLaurelTypes` to a flat `Program` suitable for
-resolution. Additional type definitions (e.g. composite types from the original
-Laurel program) can be supplied so that `UserDefined` type references resolve
-correctly.
--/
-private def unorderedCoreToProgram (uc : UnorderedCoreWithLaurelTypes)
-    (additionalTypes : List TypeDefinition := []) : Program :=
-  { staticProcedures := uc.functions ++ uc.coreProcedures,
-    staticFields := [],
-    types := uc.datatypes.map TypeDefinition.Datatype ++ additionalTypes,
-    constants := uc.constants }
-
-/--
-Reconstruct an `UnorderedCoreWithLaurelTypes` from a resolved `Program`.
--/
-private def fromResolvedProgram (resolvedProgram : Program)
-    : UnorderedCoreWithLaurelTypes :=
-  let resolvedProcs := resolvedProgram.staticProcedures
-  let resolvedDatatypes := resolvedProgram.types.filterMap fun td =>
-    match td with | .Datatype dt => some dt | _ => none
-  { functions := resolvedProcs.filter (·.isFunctional)
-    coreProcedures := resolvedProcs.filter (!·.isFunctional)
-    datatypes := resolvedDatatypes
-    constants := resolvedProgram.constants }
-
 /--
 Resolve an `UnorderedCoreWithLaurelTypes` by converting to a flat `Program`,
 running the resolution pass, and reconstructing the result. Returns the
@@ -3184,9 +3155,107 @@ public def resolveUnorderedCore (uc : UnorderedCoreWithLaurelTypes)
     (existingModel : Option SemanticModel := none)
     (additionalTypes : List TypeDefinition := [])
     : UnorderedCoreWithLaurelTypes × SemanticModel × Array DiagnosticModel :=
-  let fnProgram := unorderedCoreToProgram uc additionalTypes
-  let fnResolveResult := resolve fnProgram existingModel
-  (fromResolvedProgram fnResolveResult.program, fnResolveResult.model, fnResolveResult.errors)
+  -- Phase 1: pre-register all top-level names, then resolve references
+  let phase1 : ResolveM UnorderedCoreWithLaurelTypes := do
+    -- Pre-register additional types (e.g. composite types from the original Laurel program)
+    for td in additionalTypes do
+      match td with
+      | .Composite ct =>
+        let _ ← defineNameCheckDup ct.name (.compositeType ct)
+        for field in ct.fields do
+          let qualifiedName := ct.name.text ++ "." ++ field.name.text
+          let _ ← defineNameCheckDup field.name (.field ct.name field) (some qualifiedName)
+        for proc in ct.instanceProcedures do
+          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 _ ← defineNameCheckDup ctor.name (.datatypeConstructor dt.name ctor)
+          let testerProc := mkTesterProcedure dt ctor
+          let _ ← defineNameCheckDup (mkId (dt.testerName ctor))
+            (.staticProcedure testerProc) (some (dt.testerName ctor))
+          for p in ctor.args do
+            let pName ← defineNameCheckDup p.name (.datatypeDestructor dt.name p) (some (dt.destructorName p))
+            let _ ← defineNameCheckDup pName (.datatypeDestructor dt.name p) (some (dt.unsafeDestructorName p))
+      | .Alias ta =>
+        let _ ← defineNameCheckDup ta.name (.typeAlias ta)
+
+    -- Pre-register datatypes from the unordered core
+    for dt in uc.datatypes do
+      let _ ← defineNameCheckDup dt.name (.datatypeDefinition dt)
+      for ctor in dt.constructors do
+        let _ ← defineNameCheckDup ctor.name (.datatypeConstructor dt.name ctor)
+        let testerProc := mkTesterProcedure dt ctor
+        let _ ← defineNameCheckDup (mkId (dt.testerName ctor))
+          (.staticProcedure testerProc) (some (dt.testerName ctor))
+        for p in ctor.args do
+          let pName ← defineNameCheckDup p.name (.datatypeDestructor dt.name p) (some (dt.destructorName p))
+          let _ ← defineNameCheckDup pName (.datatypeDestructor dt.name p) (some (dt.unsafeDestructorName p))
+
+    -- Pre-register constants
+    for c in uc.constants do
+      let _ ← defineNameCheckDup c.name (.constant c)
+
+    -- Pre-register functions and core procedures
+    for proc in uc.functions do
+      let _ ← defineNameCheckDup proc.name (.staticProcedure proc)
+    for proc in uc.coreProcedures do
+      let _ ← defineNameCheckDup proc.name (.staticProcedure proc)
+
+    -- Build type scopes for additional composite types (for field resolution)
+    for td in additionalTypes do
+      if let .Composite ct := td then
+        let s ← get
+        let mut typeScope : Scope := {}
+        for parent in ct.extending do
+          match s.typeScopes.get? parent.text with
+          | some parentScope =>
+            for (k, v) in parentScope do
+              typeScope := typeScope.insert k v
+          | none => pure ()
+        for field in ct.fields do
+          let qualifiedKey := ct.name.text ++ "." ++ field.name.text
+          match s.scope.get? qualifiedKey with
+          | some entry => typeScope := typeScope.insert field.name.text entry
+          | none => pure ()
+        modify fun s => { s with typeScopes := s.typeScopes.insert ct.name.text typeScope }
+
+    -- Resolve datatypes
+    let datatypes' ← uc.datatypes.mapM fun dt => do
+      match ← resolveTypeDefinition (.Datatype dt) with
+      | .Datatype dt' => pure dt'
+      | _ => pure dt -- unreachable
+
+    -- Resolve constants
+    let constants' ← uc.constants.mapM resolveConstant
+
+    -- Resolve functions and core procedures
+    let functions' ← uc.functions.mapM resolveProcedure
+    let coreProcedures' ← uc.coreProcedures.mapM resolveProcedure
+
+    return { functions := functions', coreProcedures := coreProcedures',
+             datatypes := datatypes', constants := constants' }
+
+  let nextId := existingModel.elim 1 (fun m => m.nextId)
+  let (uc', finalState) := phase1.run { nextId := nextId }
+
+  -- Phase 2: build refToDef from the resolved unordered core
+  let program' : Program := {
+    staticProcedures := uc'.functions ++ uc'.coreProcedures,
+    staticFields := [],
+    types := uc'.datatypes.map .Datatype ++ additionalTypes,
+    constants := uc'.constants
+  }
+  let refToDef := buildRefToDef program'
+
+  let model : SemanticModel := {
+    compositeCount := additionalTypes.length,
+    refToDef := refToDef,
+    nextId := finalState.nextId
+  }
+  (uc', model, finalState.errors)
 
 end -- public section
 end Strata.Laurel
diff --git a/Strata/Languages/Laurel/SemanticModel.lean b/Strata/Languages/Laurel/SemanticModel.lean
index c41e15c5dd..78b69a3e25 100644
--- a/Strata/Languages/Laurel/SemanticModel.lean
+++ b/Strata/Languages/Laurel/SemanticModel.lean
@@ -129,18 +129,6 @@ def SemanticModel.get? (model: SemanticModel) (iden: Identifier): Option Resolve
 def SemanticModel.get (model: SemanticModel) (iden: Identifier): ResolvedNode :=
   (model.get? iden).getD default
 
-def SemanticModel.isFunction (model: SemanticModel) (id: Identifier): Bool :=
-  match model.get id with
-      | .staticProcedure proc => proc.isFunctional
-      | .parameter _ => true
-      | .datatypeConstructor _ _ => true
-      | .datatypeDestructor _ _ => true
-      | .constant _ => true
-      | .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
-
 /--
 Compute the flattened set of ancestors for a composite type, including itself.
 Traverses the `extending` list transitively.
diff --git a/Strata/Languages/Laurel/TransparencyPass.lean b/Strata/Languages/Laurel/TransparencyPass.lean
index c44751ff96..d6e3be25de 100644
--- a/Strata/Languages/Laurel/TransparencyPass.lean
+++ b/Strata/Languages/Laurel/TransparencyPass.lean
@@ -127,7 +127,7 @@ private def mkFunctionCopy (asFunctionNames : Std.HashSet String) (proc : Proced
     | .Transparent b => .Transparent (rewriteCallsToFunctional asFunctionNames (if hasProcedureTwin then stripAssertAssume b else b))
     | .Opaque _ _ _ => if hasProcedureTwin then .Opaque [] none [] else proc.body
     | x => x
-  { proc with name := funcName, isFunctional := true, body := body }
+  { proc with name := funcName, body := body }
 
 /-- Append a free postcondition to a procedure's body postconditions.
     For Opaque and Abstract bodies, the free condition is appended to the
@@ -148,14 +148,22 @@ private def addFreePostcondition (proc : Procedure) (freePost : StmtExprMd) : Pr
       { proc with body := .Opaque [freeCond] (some body) [] }
     | _ => proc
 
+/--
+Transparency pass: translate a Laurel program to the UnorderedCoreWithLaurelTypes IR.
+
+For each procedure:
+- Generate a function with the same signature, named `foo$asFunction`
+- If transparent, the function gets a functional body (assertions erased, calls to functional versions)
+- If the function has a body, add a free postcondition equating the procedure output to the function
+-/
 def createFunctionsForTransparentBodies (program : Program) : UnorderedCoreWithLaurelTypes :=
-  let (toUpdate, _) := program.staticProcedures.partition (fun p => !p.body.isExternal && !p.isFunctional)
+  let (toUpdate, _) := program.staticProcedures.partition (fun p => !p.body.isExternal)
   let toUpdateNames : Std.HashSet String := toUpdate.foldl (fun s p => s.insert p.name.text) {}
   -- $asFunction copies for non-external procedures
   let functions := program.staticProcedures.map (mkFunctionCopy toUpdateNames)
   let coreProcedures := toUpdate.map fun proc =>
     let freePostcondition := mkFreePostcondition proc
-    let proc := { proc with isFunctional := false, axioms := proc.axioms.map (rewriteCallsToFunctional toUpdateNames) }
+    let proc := { proc with axioms := proc.axioms.map (rewriteCallsToFunctional toUpdateNames) }
     let proc := rewriteQuantifierBodiesInProc toUpdateNames proc
     addFreePostcondition proc freePostcondition
   let datatypes := program.types.filterMap fun td => match td with
diff --git a/StrataPython/StrataPython/PythonRuntimeLaurelPart.lean b/StrataPython/StrataPython/PythonRuntimeLaurelPart.lean
index c1352bfd71..1b10e6171b 100644
--- a/StrataPython/StrataPython/PythonRuntimeLaurelPart.lean
+++ b/StrataPython/StrataPython/PythonRuntimeLaurelPart.lean
@@ -157,150 +157,127 @@ composite re_Match {
 }
 
 // re.Match methods — uninterpreted (capture groups are beyond SMT-LIB)
-function re_Match_group (self : re_Match, n : int) : string;
-function re_Match_start (self : re_Match, n : int) : int;
-function re_Match_end   (self : re_Match, n : int) : int;
-function re_Match_span_start (self : re_Match, n : int) : int;
-function re_Match_span_end   (self : re_Match, n : int) : int;
-function re_Match_lastindex  (self : re_Match) : int;
-function re_Match_lastgroup  (self : re_Match) : string;
-function re_Match_groups     (self : re_Match) : ListStr;
-
-function re_pattern_error(pattern : string) : Error
+procedure re_Match_group (self : re_Match, n : int) : string;
+procedure re_Match_start (self : re_Match, n : int) : int;
+procedure re_Match_end   (self : re_Match, n : int) : int;
+procedure re_Match_span_start (self : re_Match, n : int) : int;
+procedure re_Match_span_end   (self : re_Match, n : int) : int;
+procedure re_Match_lastindex  (self : re_Match) : int;
+procedure re_Match_lastgroup  (self : re_Match) : string;
+procedure re_Match_groups     (self : re_Match) : ListStr;
+
+procedure re_pattern_error(pattern : string) : Error
   external;
 
 // The _bool variants are also factory functions (not inlined here) so that
 // unsupported patterns leave an uninterpreted Bool UF rather than an
 // uninterpreted RegLan UF.  An uninterpreted Bool UF produces `unknown`
 // gracefully; an uninterpreted RegLan UF causes cvc5 theory-combination errors.
-function re_fullmatch_bool(pattern : string, s : string) : bool
+procedure re_fullmatch_bool(pattern : string, s : string) : bool
   external;
-function re_match_bool(pattern : string, s : string) : bool
+procedure re_match_bool(pattern : string, s : string) : bool
   external;
-function re_search_bool(pattern : string, s : string) : bool
+procedure re_search_bool(pattern : string, s : string) : bool
   external;
 
-function Str.InRegEx(s: string, r: Core regex): bool external;
-function Str.Length(s: string): int external;
+procedure Str.InRegEx(s: string, r: Core regex): bool external;
+procedure Str.Length(s: string): int external;
 
 // /////////////////////////////////////////////////////////////////////////////////////
 
 
-function mk_re_Match(s : string) : Any {
-  from_ClassInstance("re_Match",
+procedure mk_re_Match(s : string) : Any
+  return from_ClassInstance("re_Match",
     DictStrAny_cons("re_match_string", from_str(s),
       DictStrAny_cons("re_match_pos", from_int(0),
         DictStrAny_cons("re_match_endpos", from_int(Str.Length(s)),
-          DictStrAny_empty()))))
-};
+          DictStrAny_empty()))));
 
 // re.compile is a no-op: returns the pattern string unchanged.
-function re_compile(pattern : Any) : Any
+procedure re_compile(pattern : Any) : Any
   requires Any..isfrom_str(pattern)
-{
-  pattern
-};
+  return pattern;
 
-function re_fullmatch(pattern : Any, s : Any) : Any
+procedure re_fullmatch(pattern : Any, s : Any) : Any
   requires Any..isfrom_str(pattern) && Any..isfrom_str(s)
-{
-  if Error..isRePatternError(re_pattern_error(Any..as_string!(pattern)))
-  then exception(re_pattern_error(Any..as_string!(pattern)))
-  else if re_fullmatch_bool(Any..as_string!(pattern), Any..as_string!(s))
-       then mk_re_Match(Any..as_string!(s))
-       else from_None()
-};
-function re_match(pattern : Any, s : Any) : Any
+  return if Error..isRePatternError(re_pattern_error(Any..as_string!(pattern)))
+    then exception(re_pattern_error(Any..as_string!(pattern)))
+    else if re_fullmatch_bool(Any..as_string!(pattern), Any..as_string!(s))
+        then mk_re_Match(Any..as_string!(s))
+        else from_None();
+
+procedure re_match(pattern : Any, s : Any) : Any
   requires Any..isfrom_str(pattern) && Any..isfrom_str(s)
-{
-  if Error..isRePatternError(re_pattern_error(Any..as_string!(pattern)))
-  then exception(re_pattern_error(Any..as_string!(pattern)))
-  else if re_match_bool(Any..as_string!(pattern), Any..as_string!(s))
-       then mk_re_Match(Any..as_string!(s))
-       else from_None()
-};
-function re_search(pattern : Any, s : Any) : Any
+  return if Error..isRePatternError(re_pattern_error(Any..as_string!(pattern)))
+    then exception(re_pattern_error(Any..as_string!(pattern)))
+    else if re_match_bool(Any..as_string!(pattern), Any..as_string!(s))
+        then mk_re_Match(Any..as_string!(s))
+        else from_None();
+
+procedure re_search(pattern : Any, s : Any) : Any
   requires Any..isfrom_str(pattern) && Any..isfrom_str(s)
-{
-  if Error..isRePatternError(re_pattern_error(Any..as_string!(pattern)))
-  then exception(re_pattern_error(Any..as_string!(pattern)))
-  else if re_search_bool(Any..as_string!(pattern), Any..as_string!(s))
-       then mk_re_Match(Any..as_string!(s))
-       else from_None()
-};
+  return if Error..isRePatternError(re_pattern_error(Any..as_string!(pattern)))
+    then exception(re_pattern_error(Any..as_string!(pattern)))
+    else if re_search_bool(Any..as_string!(pattern), Any..as_string!(s))
+        then mk_re_Match(Any..as_string!(s))
+        else from_None();
 
 // /////////////////////////////////////////////////////////////////////////////////////
 //Functions that we provide to Python user
 //to write assertions/contracts about about types of variables
 
-function isBool (v: Any) : Any {
-  from_bool (Any..isfrom_bool(v))
-};
+procedure isBool (v: Any) : Any
+  return from_bool (Any..isfrom_bool(v));
 
-function isInt (v: Any) : Any {
-  from_bool (Any..isfrom_int(v))
-};
+procedure isInt (v: Any) : Any
+  return from_bool (Any..isfrom_int(v));
 
-function isFloat (v: Any) : Any {
-  from_bool (Any..isfrom_float(v))
-};
+procedure isFloat (v: Any) : Any
+  return from_bool (Any..isfrom_float(v));
 
-function isString (v: Any) : Any {
-  from_bool (Any..isfrom_str(v))
-};
+procedure isString (v: Any) : Any
+  return from_bool (Any..isfrom_str(v));
 
-function isdatetime (v: Any) : Any {
-  from_bool (Any..isfrom_datetime(v))
-};
+procedure isdatetime (v: Any) : Any
+  return from_bool (Any..isfrom_datetime(v));
 
-function isDict (v: Any) : Any {
-  from_bool (Any..isfrom_DictStrAny(v))
-};
+procedure isDict (v: Any) : Any
+  return from_bool (Any..isfrom_DictStrAny(v));
 
-function isList (v: Any) : Any {
-  from_bool (Any..isfrom_ListAny(v))
-};
+procedure isList (v: Any) : Any
+  return from_bool (Any..isfrom_ListAny(v));
 
-function isClassInstance (v: Any) : Any {
-  from_bool (Any..isfrom_ClassInstance(v))
-};
+procedure isClassInstance (v: Any) : Any
+  return from_bool (Any..isfrom_ClassInstance(v));
 
-function isInstance_of_Int (v: Any) : Any {
-  from_bool (Any..isfrom_int(v) || Any..isfrom_bool(v))
-};
+procedure isInstance_of_Int (v: Any) : Any
+  return from_bool (Any..isfrom_int(v) || Any..isfrom_bool(v));
 
-function isInstance_of_Float (v: Any) : Any {
-  from_bool (Any..isfrom_float(v) || Any..isfrom_int(v) || Any..isfrom_bool(v))
-};
+procedure isInstance_of_Float (v: Any) : Any
+  return from_bool (Any..isfrom_float(v) || Any..isfrom_int(v) || Any..isfrom_bool(v));
 
 // /////////////////////////////////////////////////////////////////////////////////////
 //Functions that we provide to Python user
 //to write assertions/contracts about about types of errors
 // /////////////////////////////////////////////////////////////////////////////////////
 
-function isTypeError (e: Error) : Any {
-  from_bool (Error..isTypeError(e))
-};
+procedure isTypeError (e: Error) : Any
+return from_bool (Error..isTypeError(e));
 
-function isAttributeError (e: Error) : Any {
-  from_bool (Error..isAttributeError(e))
-};
+procedure isAttributeError (e: Error) : Any
+return from_bool (Error..isAttributeError(e));
 
-function isAssertionError (e: Error) : Any {
-  from_bool (Error..isAssertionError(e))
-};
+procedure isAssertionError (e: Error) : Any
+return from_bool (Error..isAssertionError(e));
 
-function isUnimplementedError (e: Error) : Any {
-  from_bool (Error..isUnimplementedError(e))
-};
+procedure isUnimplementedError (e: Error) : Any
+return from_bool (Error..isUnimplementedError(e));
 
-function isUndefinedError (e: Error) : Any {
-  from_bool (Error..isUndefinedError(e))
-};
+procedure isUndefinedError (e: Error) : Any
+return from_bool (Error..isUndefinedError(e));
 
-function isError (e: Error) : bool {
-  ! Error..isNoError(e)
-};
+procedure isError (e: Error) : bool
+return ! Error..isNoError(e);
 
 // /////////////////////////////////////////////////////////////////////////////////////
 //The following function convert Any type to bool
@@ -308,197 +285,152 @@ function isError (e: Error) : bool {
 // https://docs.python.org/3/library/stdtypes.html
 // /////////////////////////////////////////////////////////////////////////////////////
 
-function Any_to_bool (v: Any) : bool
-{
-  if (Any..isfrom_bool(v)) then Any..as_bool!(v) else
+procedure Any_to_bool (v: Any) : bool
+return if (Any..isfrom_bool(v)) then Any..as_bool!(v) else
   if (Any..isfrom_None(v)) then false else
   if (Any..isfrom_str(v)) then !(Any..as_string!(v) == "") else
   if (Any..isfrom_int(v)) then !(Any..as_int!(v) == 0) else
   if (Any..isfrom_float(v)) then !(Any..as_float!(v) == 0.0) else
   if (Any..isfrom_DictStrAny(v)) then !(Any..as_Dict!(v) == DictStrAny_empty()) else
   if (Any..isfrom_ListAny(v)) then !(Any..as_ListAny!(v) == ListAny_nil()) else
-  <?>
-};
+  <?>;
 
-function to_bool_any(v: Any) : Any
-{
-  from_bool(Any_to_bool(v))
-};
+procedure to_bool_any(v: Any) : Any
+return from_bool(Any_to_bool(v));
 
 // /////////////////////////////////////////////////////////////////////////////////////
 // ListAny functions
 // /////////////////////////////////////////////////////////////////////////////////////
 
-function List_len (l : ListAny) : int
-{
-  if ListAny..isListAny_nil(l) then 0 else 1 + List_len(ListAny..tail!(l))
-};
+procedure List_len (l : ListAny) : int
+return if ListAny..isListAny_nil(l) then 0 else 1 + List_len(ListAny..tail!(l));
 
 procedure List_len_pos(l : ListAny)
   invokeOn List_len(l)
   opaque
   ensures List_len(l) >= 0;
 
-function List_contains (l : ListAny, x: Any) : bool
-{
-  if ListAny..isListAny_nil(l) then false else (ListAny..head!(l) == x) || List_contains(ListAny..tail!(l), x)
-};
+procedure List_contains (l : ListAny, x: Any) : bool
+return if ListAny..isListAny_nil(l) then false else (ListAny..head!(l) == x) || List_contains(ListAny..tail!(l), x);
 
-function List_extend (l1 : ListAny, l2: ListAny) : ListAny
-{
-  if ListAny..isListAny_nil(l1) then l2
-  else ListAny_cons(ListAny..head!(l1), List_extend(ListAny..tail!(l1), l2))
-};
+procedure List_extend (l1 : ListAny, l2: ListAny) : ListAny
+return if ListAny..isListAny_nil(l1) then l2
+  else ListAny_cons(ListAny..head!(l1), List_extend(ListAny..tail!(l1), l2));
 
-function List_get_non_neg (l : ListAny, i : int) : Any
+procedure List_get_non_neg (l : ListAny, i : int) : Any
   requires i >= 0 && i < List_len(l)
-{
-  if ListAny..isListAny_nil(l) then from_None()
+return if ListAny..isListAny_nil(l) then from_None()
   else if  i == 0 then ListAny..head!(l)
-  else List_get_non_neg(ListAny..tail!(l), i - 1)
-};
+  else List_get_non_neg(ListAny..tail!(l), i - 1);
 
-function List_get (l : ListAny, i : int) : Any
+procedure List_get (l : ListAny, i : int) : Any
   requires i >= - List_len(l) && i < List_len(l)
-{
-  if i >= 0 then List_get_non_neg(l, i)
-  else List_get_non_neg(l, List_len(l) + i)
-};
+return if i >= 0 then List_get_non_neg(l, i)
+  else List_get_non_neg(l, List_len(l) + i);
 
-function List_take (l : ListAny, i: int) : ListAny
+procedure List_take (l : ListAny, i: int) : ListAny
   requires i >= 0 && i <= List_len(l)
-{
-  if ListAny..isListAny_nil(l) then ListAny_nil()
+return if ListAny..isListAny_nil(l) then ListAny_nil()
   else if  i == 0 then ListAny_nil()
-  else ListAny_cons(ListAny..head!(l), List_take(ListAny..tail!(l), i - 1))
-};
+  else ListAny_cons(ListAny..head!(l), List_take(ListAny..tail!(l), i - 1));
 
 procedure List_take_len(l : ListAny, i: int)
   invokeOn List_len(List_take(l,i))
   opaque
   ensures i >= 0 && i <= List_len(l) ==> List_len(List_take(l,i)) == i;
 
-function List_drop (l : ListAny, i: int) : ListAny
+procedure List_drop (l : ListAny, i: int) : ListAny
   requires i >= 0 && i <= List_len(l)
-{
-  if ListAny..isListAny_nil(l) then ListAny_nil()
+return if ListAny..isListAny_nil(l) then ListAny_nil()
   else if  i == 0 then l
-  else List_drop(ListAny..tail!(l), i - 1)
-};
+  else List_drop(ListAny..tail!(l), i - 1);
 
 procedure List_drop_len(l : ListAny, i: int)
   invokeOn List_len(List_drop(l,i))
   opaque
   ensures i >= 0 && i <= List_len(l) ==> List_len(List_drop(l,i)) == List_len(l) - i;
 
-function int_max (i1: int, i2: int) : int
-{
-  if i1 >= i2 then i1 else i2
-};
+procedure int_max (i1: int, i2: int) : int
+return if i1 >= i2 then i1 else i2;
 
-function int_min (i1: int, i2: int) : int
-{
-  if i1 <= i2 then i1 else i2
-};
+procedure int_min (i1: int, i2: int) : int
+return if i1 <= i2 then i1 else i2;
 
-function List_slice_non_neg (l : ListAny, start : int, stop: int) : ListAny
+procedure List_slice_non_neg (l : ListAny, start : int, stop: int) : ListAny
   requires start >= 0 && stop >= 0
-{
-  if (start >= List_len(l)) || (start >= stop) then ListAny_nil()
-  else List_take (List_drop (l, start), int_min(stop, List_len(l))  - start)
-};
+return if (start >= List_len(l)) || (start >= stop) then ListAny_nil()
+  else List_take (List_drop (l, start), int_min(stop, List_len(l))  - start);
 
 
-function List_slice (l : ListAny, start : int, stop: int) : ListAny
-{
-  List_slice_non_neg (l,
+procedure List_slice (l : ListAny, start : int, stop: int) : ListAny
+return List_slice_non_neg (l,
     if start >= 0 then start else int_max (List_len(l) + start, 0),
     if stop >= 0 then stop else int_max (List_len(l) + stop, 0)
-  )
-};
+  );
 
-function List_set_non_neg (l : ListAny, i : int, v: Any) : ListAny
+procedure List_set_non_neg (l : ListAny, i : int, v: Any) : ListAny
   requires i >= 0 && i < List_len(l)
-{
-  if ListAny..isListAny_nil(l) then ListAny_nil()
+return if ListAny..isListAny_nil(l) then ListAny_nil()
   else if  i == 0 then ListAny_cons(v, ListAny..tail!(l))
-  else ListAny_cons(ListAny..head!(l), List_set_non_neg(ListAny..tail!(l), i - 1, v))
-};
+  else ListAny_cons(ListAny..head!(l), List_set_non_neg(ListAny..tail!(l), i - 1, v));
 
-function List_set (l : ListAny, i : int, v: Any) : ListAny
+procedure List_set (l : ListAny, i : int, v: Any) : ListAny
   requires i >= - List_len(l) && i < List_len(l)
-{
-  if i >= 0 then List_set_non_neg(l, i, v)
-  else List_set_non_neg(l, List_len(l) + i, v)
-};
+return if i >= 0 then List_set_non_neg(l, i, v)
+  else List_set_non_neg(l, List_len(l) + i, v);
 
 //Require recursive function on int
-function List_repeat (l: ListAny, n: int): ListAny;
+procedure List_repeat (l: ListAny, n: int): ListAny;
 
-function range (start: Any, stop: Any, step: Any) : Any
+procedure range (start: Any, stop: Any, step: Any) : Any
   requires Any..isfrom_int(start) && Any..isfrom_None(stop) && Any..isfrom_None(step);
 
 // /////////////////////////////////////////////////////////////////////////////////////
 // DictStrAny functions
 // /////////////////////////////////////////////////////////////////////////////////////
 
-function DictStrAny_contains (d : DictStrAny, key: string) : bool
-{
-  if DictStrAny..isDictStrAny_empty(d) then false
-  else (DictStrAny..key!(d) == key) || DictStrAny_contains(DictStrAny..tail!(d), key)
-};
+procedure DictStrAny_contains (d : DictStrAny, key: string) : bool
+return if DictStrAny..isDictStrAny_empty(d) then false
+  else (DictStrAny..key!(d) == key) || DictStrAny_contains(DictStrAny..tail!(d), key);
 
-function DictStrAny_get (d : DictStrAny, key: string) : Any
+procedure DictStrAny_get (d : DictStrAny, key: string) : Any
   requires DictStrAny_contains(d, key)
-{
-  if  DictStrAny..isDictStrAny_empty(d) then from_None()
+return if  DictStrAny..isDictStrAny_empty(d) then from_None()
   else if DictStrAny..key!(d) == key then DictStrAny..val!(d)
-  else DictStrAny_get(DictStrAny..tail!(d), key)
-};
+  else DictStrAny_get(DictStrAny..tail!(d), key);
 
-function DictStrAny_get_or_none (d : DictStrAny, key: string) : Any
-{
-  if DictStrAny_contains(d, key) then DictStrAny_get(d, key)
-  else from_None()
-};
+procedure DictStrAny_get_or_none (d : DictStrAny, key: string) : Any
+return if DictStrAny_contains(d, key) then DictStrAny_get(d, key)
+  else from_None();
 
-function Any_get_or_none (dict: Any, key: Any) : Any
+procedure Any_get_or_none (dict: Any, key: Any) : Any
   requires Any..isfrom_DictStrAny(dict) && Any..isfrom_str(key)
-{
-  DictStrAny_get_or_none(Any..as_Dict!(dict), Any..as_string!(key))
-};
+return DictStrAny_get_or_none(Any..as_Dict!(dict), Any..as_string!(key));
 
-function DictStrAny_insert (d : DictStrAny, key: string, val: Any) : DictStrAny
-{
-  if DictStrAny..isDictStrAny_empty(d) then DictStrAny_cons(key, val, DictStrAny_empty())
+procedure DictStrAny_insert (d : DictStrAny, key: string, val: Any) : DictStrAny
+return if DictStrAny..isDictStrAny_empty(d) then DictStrAny_cons(key, val, DictStrAny_empty())
   else if DictStrAny..key!(d) == key then DictStrAny_cons(key, val, DictStrAny..tail!(d))
-  else DictStrAny_cons(DictStrAny..key!(d), DictStrAny..val!(d), DictStrAny_insert(DictStrAny..tail!(d), key, val))
-};
+  else DictStrAny_cons(DictStrAny..key!(d), DictStrAny..val!(d), DictStrAny_insert(DictStrAny..tail!(d), key, val));
 
-function Any_get (dictOrList: Any, index: Any): Any
+procedure Any_get (dictOrList: Any, index: Any): Any
   requires  (Any..isfrom_DictStrAny(dictOrList) && Any..isfrom_str(index) && DictStrAny_contains(Any..as_Dict!(dictOrList), Any..as_string!(index))) ||
             (Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index) && Any..as_int!(index) >= - List_len(Any..as_ListAny!(dictOrList)) && Any..as_int!(index) < List_len(Any..as_ListAny!(dictOrList)))
-{
-  if Any..isfrom_DictStrAny(dictOrList) then
+return if Any..isfrom_DictStrAny(dictOrList) then
     DictStrAny_get(Any..as_Dict!(dictOrList), Any..as_string!(index))
   else
-    List_get(Any..as_ListAny!(dictOrList), Any..as_int!(index))
-};
+    List_get(Any..as_ListAny!(dictOrList), Any..as_int!(index));
 
-function Any_get_slice (list: Any, index: Any): Any
+procedure Any_get_slice (list: Any, index: Any): Any
   requires (Any..isfrom_ListAny(list) && Any..isfrom_Slice(index))
-{
-  from_ListAny(List_slice(
+return from_ListAny(List_slice(
     Any..as_ListAny!(list),
     Any..start!(index),
     if OptionInt..isOptSome(Any..stop!(index))
     then OptionInt..unwrap!(Any..stop!(index))
-    else List_len(Any..as_ListAny!(list))))
-};
+    else List_len(Any..as_ListAny!(list))));
 
-function Any_get! (dictOrList: Any, index: Any): Any
-{
-  if Any..isexception(dictOrList) then dictOrList
+procedure Any_get! (dictOrList: Any, index: Any): Any
+return if Any..isexception(dictOrList) then dictOrList
   else if Any..isexception(index) then index
   else if !(Any..isfrom_DictStrAny(dictOrList) && Any..isfrom_str(index)) && !(Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index)) then
     exception (TypeError("Invalid subscription type"))
@@ -507,23 +439,19 @@ function Any_get! (dictOrList: Any, index: Any): Any
   else if Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index) && Any..as_int!(index) >= - List_len(Any..as_ListAny!(dictOrList)) && Any..as_int!(index) < List_len(Any..as_ListAny!(dictOrList)) then
       List_get(Any..as_ListAny!(dictOrList), Any..as_int!(index))
   else
-    exception (IndexError("Invalid subscription"))
-};
+    exception (IndexError("Invalid subscription"));
 
-function Any_set (dictOrList: Any, index: Any, val: Any): Any
+procedure Any_set (dictOrList: Any, index: Any, val: Any): Any
   requires  (Any..isfrom_DictStrAny(dictOrList) && Any..isfrom_str(index)) ||
             (Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index) &&
             Any..as_int!(index) >= - List_len(Any..as_ListAny!(dictOrList)) && Any..as_int!(index) < List_len(Any..as_ListAny!(dictOrList)))
-{
-  if Any..isfrom_DictStrAny(dictOrList) then
+return if Any..isfrom_DictStrAny(dictOrList) then
     from_DictStrAny(DictStrAny_insert(Any..as_Dict!(dictOrList), Any..as_string!(index), val))
   else
-    from_ListAny(List_set(Any..as_ListAny!(dictOrList), Any..as_int!(index), val))
-};
+    from_ListAny(List_set(Any..as_ListAny!(dictOrList), Any..as_int!(index), val));
 
-function Any_set! (dictOrList: Any, index: Any, val: Any): Any
-{
-  if Any..isexception(dictOrList) then dictOrList
+procedure Any_set! (dictOrList: Any, index: Any, val: Any): Any
+return if Any..isexception(dictOrList) then dictOrList
   else if Any..isexception(index) then index
   else if Any..isexception(val) then val
   else if !(Any..isfrom_DictStrAny(dictOrList) && Any..isfrom_str(index)) && !(Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index)) then
@@ -534,66 +462,57 @@ function Any_set! (dictOrList: Any, index: Any, val: Any): Any
           Any..as_int!(index) >= - List_len(Any..as_ListAny!(dictOrList)) && Any..as_int!(index) < List_len(Any..as_ListAny!(dictOrList)) then
     from_ListAny(List_set(Any..as_ListAny!(dictOrList), Any..as_int!(index), val))
   else
-    exception (IndexError("Index out of bound"))
-};
+    exception (IndexError("Index out of bound"));
 
-function Any_sets! (indices: ListAny, dictOrList: Any, val: Any): Any
-{
-  if ListAny..isListAny_nil(indices) then dictOrList
+procedure Any_sets! (indices: ListAny, dictOrList: Any, val: Any): Any
+return if ListAny..isListAny_nil(indices) then dictOrList
   else if ListAny..isListAny_nil(ListAny..tail!(indices)) then Any_set!(dictOrList, ListAny..head!(indices), val)
   else Any_set!(dictOrList, ListAny..head!(indices),
-    Any_sets!(ListAny..tail!(indices), Any_get!(dictOrList, ListAny..head!(indices)), val))
-};
+    Any_sets!(ListAny..tail!(indices), Any_get!(dictOrList, ListAny..head!(indices)), val));
 
-function Any_len (v: Any) : int;
+procedure Any_len (v: Any) : int;
 
-function Any_len_to_Any (v: Any) : Any {
-  from_int(Any_len(v))
-};
+procedure Any_len_to_Any (v: Any) : Any
+return from_int(Any_len(v));
 
 procedure Any_len_pos(v: Any)
   invokeOn Any_len(v)
   opaque
   ensures Any_len(v) >= 0;
 
-function Any_iter_index(iter: Any, index: int) : Any;
+procedure Any_iter_index(iter: Any, index: int) : Any;
 
-function PIn (v: Any, dictOrList: Any) : Any
+procedure PIn (v: Any, dictOrList: Any) : Any
   requires (Any..isfrom_DictStrAny(dictOrList) && Any..isfrom_str(v)) || Any..isfrom_ListAny(dictOrList)
-{
-  from_bool(
+return from_bool(
     if Any..isfrom_DictStrAny(dictOrList) then
       DictStrAny_contains(Any..as_Dict!(dictOrList), Any..as_string!(v))
     else
       List_contains(Any..as_ListAny!(dictOrList), v)
-  )
-};
+  );
 
-function PNotIn ( v: Any, dictOrList: Any) : Any
+procedure PNotIn ( v: Any, dictOrList: Any) : Any
   requires (Any..isfrom_DictStrAny(dictOrList) && Any..isfrom_str(v)) || Any..isfrom_ListAny(dictOrList)
-{
-  from_bool(
+return from_bool(
     if Any..isfrom_DictStrAny(dictOrList) then
       !DictStrAny_contains(Any..as_Dict!(dictOrList), Any..as_string!(v))
     else
       !List_contains(Any..as_ListAny!(dictOrList), v)
-  )
-};
+  );
 
 // /////////////////////////////////////////////////////////////////////////////////////
 // Python treats some values of different types to be equivalent
 // This function models that behavior
 // /////////////////////////////////////////////////////////////////////////////////////
 
-function is_IntReal (v: Any) : bool;
-function Any_real_to_int (v: Any) : int;
+procedure is_IntReal (v: Any) : bool;
+procedure Any_real_to_int (v: Any) : int;
 
-function normalize_any (v : Any) : Any {
-  if v == from_bool(true) then from_int(1)
+procedure normalize_any (v : Any) : Any
+return if v == from_bool(true) then from_int(1)
   else (if v == from_bool(false) then from_int(0) else
         if Any..isfrom_float(v) && is_IntReal(v) then from_int(Any_real_to_int(v)) else
-        v)
-};
+        v);
 
 
 // /////////////////////////////////////////////////////////////////////////////////////
@@ -606,21 +525,22 @@ function normalize_any (v : Any) : Any {
 // /////////////////////////////////////////////////////////////////////////////////////
 // This function convert an int to a real
 // Need to connect to an SMT function
-function int_to_real (i: int) : real;
+procedure int_to_real (i: int) : real;
 
 // /////////////////////////////////////////////////////////////////////////////////////
 // Converting bool to int or real
 // Used to in Python binary operators' modelling
-function bool_to_int (bval: bool) : int {if bval then 1 else 0};
-function bool_to_real (b: bool) : real {if b then 1.0 else 0.0};
+procedure bool_to_int (bval: bool) : int
+return if bval then 1 else 0;
+procedure bool_to_real (b: bool) : real
+return if b then 1.0 else 0.0;
 
 // /////////////////////////////////////////////////////////////////////////////////////
 // Modelling of Python unary operations
 // /////////////////////////////////////////////////////////////////////////////////////
 
-function PNeg (v: Any) : Any
-{
-  if Any..isexception(v) then v
+procedure PNeg (v: Any) : Any
+return if Any..isexception(v) then v
   else if Any..isfrom_bool(v) then
     from_int(- bool_to_int(Any..as_bool!(v)))
   else if Any..isfrom_int(v) then
@@ -628,35 +548,29 @@ function PNeg (v: Any) : Any
   else if Any..isfrom_float(v) then
     from_float(- Any..as_float!(v))
   else
-    exception(UndefinedError ("Operand Type is not defined"))
-};
+    exception(UndefinedError ("Operand Type is not defined"));
 
-function PBitNot (v: Any) : Any
-{
-  if Any..isexception(v) then v
+procedure PBitNot (v: Any) : Any
+return if Any..isexception(v) then v
   else if Any..isfrom_bool(v) then
     from_int(-(bool_to_int(Any..as_bool!(v)) + 1))
   else if Any..isfrom_int(v) then
     from_int(-(Any..as_int!(v) + 1))
   else
-    exception(UndefinedError ("Operand Type is not defined"))
-};
+    exception(UndefinedError ("Operand Type is not defined"));
 
-function PNot (v: Any) : Any
-{
-  if Any..isexception(v) then v
-  else from_bool(!(Any_to_bool(v)))
-};
+procedure PNot (v: Any) : Any
+return if Any..isexception(v) then v
+  else from_bool(!(Any_to_bool(v)));
 
 // /////////////////////////////////////////////////////////////////////////////////////
 // Modelling of Python binary operations
 // /////////////////////////////////////////////////////////////////////////////////////
 
-function Str.Concat(s: string, s2: string): string external;
+procedure Str.Concat(s: string, s2: string): string external;
 
-function PAdd (v1: Any, v2: Any) : Any
-{
-  if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
+procedure PAdd (v1: Any, v2: Any) : Any
+return if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
   else if Any..isfrom_bool(v1) && Any..isfrom_bool(v2) then
     from_int(bool_to_int(Any..as_bool!(v1)) + bool_to_int(Any..as_bool!(v2)))
   else if Any..isfrom_bool(v1) && Any..isfrom_int(v2) then
@@ -680,12 +594,10 @@ function PAdd (v1: Any, v2: Any) : Any
   else if Any..isfrom_datetime(v1) && Any..isfrom_int(v2) then
     from_datetime((Any..as_datetime!(v1) + Any..as_int!(v2)))
   else
-    exception(UndefinedError ("Operand Type is not defined"))
-};
+    exception(UndefinedError ("Operand Type is not defined"));
 
-function PSub (v1: Any, v2: Any) : Any
-{
-  if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
+procedure PSub (v1: Any, v2: Any) : Any
+return if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
   else if Any..isfrom_bool(v1) && Any..isfrom_bool(v2) then
     from_int(bool_to_int(Any..as_bool!(v1)) - bool_to_int(Any..as_bool!(v2)))
   else if Any..isfrom_bool(v1) && Any..isfrom_int(v2) then
@@ -709,14 +621,12 @@ function PSub (v1: Any, v2: Any) : Any
   else if Any..isfrom_datetime(v1) && Any..isfrom_datetime(v2) then
     from_int(Any..as_datetime!(v1) - Any..as_datetime!(v2))
   else
-    exception(UndefinedError ("Operand Type is not defined"))
-};
+    exception(UndefinedError ("Operand Type is not defined"));
 
-function string_repeat (s: string, i: int) : string;
+procedure string_repeat (s: string, i: int) : string;
 
-function PMul (v1: Any, v2: Any) : Any
-{
-  if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
+procedure PMul (v1: Any, v2: Any) : Any
+return if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
   else if Any..isfrom_bool(v1) && Any..isfrom_bool(v2) then
     from_int(bool_to_int(Any..as_bool!(v1)) * bool_to_int(Any..as_bool!(v2)))
   else if Any..isfrom_bool(v1) && Any..isfrom_int(v2) then
@@ -748,13 +658,11 @@ function PMul (v1: Any, v2: Any) : Any
   else if Any..isfrom_float(v1) && Any..isfrom_float(v2) then
     from_float(Any..as_float!(v1) * Any..as_float!(v2))
   else
-    exception(UndefinedError ("Operand Type is not defined"))
-};
+    exception(UndefinedError ("Operand Type is not defined"));
 
-function PFloorDiv (v1: Any, v2: Any) : Any
+procedure PFloorDiv (v1: Any, v2: Any) : Any
   requires (Any..isfrom_bool(v2)==>Any..as_bool!(v2)) && (Any..isfrom_int(v2)==>Any..as_int!(v2)!=0)
-{
-  if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
+return if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
   else if Any..isfrom_bool(v1) && Any..isfrom_bool(v2) then
     from_int( bool_to_int(Any..as_bool!(v1)) / bool_to_int(Any..as_bool!(v2)))
   else if Any..isfrom_bool(v1) && Any..isfrom_int(v2) then
@@ -764,25 +672,23 @@ function PFloorDiv (v1: Any, v2: Any) : Any
   else if Any..isfrom_int(v1) && Any..isfrom_int(v2) then
     from_int(Any..as_int!(v1) / Any..as_int!(v2))
   else
-    exception(UndefinedError ("Operand Type is not defined"))
-};
+    exception(UndefinedError ("Operand Type is not defined"));
 
 // /////////////////////////////////////////////////////////////////////////////////////
 // Modelling of Python comparision operations
 // /////////////////////////////////////////////////////////////////////////////////////
 
-function string_lt (s1: string, s2: string) : bool;
-function string_le (s1: string, s2: string) : bool;
-function string_gt (s1: string, s2: string) : bool;
-function string_ge (s1: string, s2: string) : bool;
-function List_lt (l1: ListAny, l2: ListAny): bool;
-function List_le (l1: ListAny, l2: ListAny): bool;
-function List_gt (l1: ListAny, l2: ListAny): bool;
-function List_ge (l1: ListAny, l2: ListAny): bool;
+procedure string_lt (s1: string, s2: string) : bool;
+procedure string_le (s1: string, s2: string) : bool;
+procedure string_gt (s1: string, s2: string) : bool;
+procedure string_ge (s1: string, s2: string) : bool;
+procedure List_lt (l1: ListAny, l2: ListAny): bool;
+procedure List_le (l1: ListAny, l2: ListAny): bool;
+procedure List_gt (l1: ListAny, l2: ListAny): bool;
+procedure List_ge (l1: ListAny, l2: ListAny): bool;
 
-function PLt (v1: Any, v2: Any) : Any
-{
-  if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
+procedure PLt (v1: Any, v2: Any) : Any
+return if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
   else if Any..isfrom_bool(v1) && Any..isfrom_bool(v2) then
     from_bool(bool_to_int(Any..as_bool!(v1)) < bool_to_int(Any..as_bool!(v2)))
   else if Any..isfrom_bool(v1) && Any..isfrom_int(v2) then
@@ -808,12 +714,10 @@ function PLt (v1: Any, v2: Any) : Any
   else if Any..isfrom_datetime(v1) && Any..isfrom_datetime(v2) then
     from_bool(Any..as_datetime!(v1) <Any..as_datetime!(v2))
   else
-    exception(UndefinedError ("Operand Type is not defined"))
-};
+    exception(UndefinedError ("Operand Type is not defined"));
 
-function PLe (v1: Any, v2: Any) : Any
-{
-  if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
+procedure PLe (v1: Any, v2: Any) : Any
+return if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
   else if Any..isfrom_bool(v1) && Any..isfrom_bool(v2) then
     from_bool(bool_to_int(Any..as_bool!(v1)) <= bool_to_int(Any..as_bool!(v2)))
   else if Any..isfrom_bool(v1) && Any..isfrom_int(v2) then
@@ -839,12 +743,10 @@ function PLe (v1: Any, v2: Any) : Any
   else if Any..isfrom_datetime(v1) && Any..isfrom_datetime(v2) then
     from_bool(Any..as_datetime!(v1) <=Any..as_datetime!(v2))
   else
-    exception(UndefinedError ("Operand Type is not defined"))
-};
+    exception(UndefinedError ("Operand Type is not defined"));
 
-function PGt (v1: Any, v2: Any) : Any
-{
-  if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
+procedure PGt (v1: Any, v2: Any) : Any
+return if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
   else if Any..isfrom_bool(v1) && Any..isfrom_bool(v2) then
     from_bool(bool_to_int(Any..as_bool!(v1)) > bool_to_int(Any..as_bool!(v2)))
   else if Any..isfrom_bool(v1) && Any..isfrom_int(v2) then
@@ -870,12 +772,10 @@ function PGt (v1: Any, v2: Any) : Any
   else if Any..isfrom_datetime(v1) && Any..isfrom_datetime(v2) then
     from_bool(Any..as_datetime!(v1) >Any..as_datetime!(v2))
   else
-    exception(UndefinedError ("Operand Type is not defined"))
-};
+    exception(UndefinedError ("Operand Type is not defined"));
 
-function PGe (v1: Any, v2: Any) : Any
-{
-  if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
+procedure PGe (v1: Any, v2: Any) : Any
+return if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
   else if Any..isfrom_bool(v1) && Any..isfrom_bool(v2) then
     from_bool(bool_to_int(Any..as_bool!(v1)) >= bool_to_int(Any..as_bool!(v2)))
   else if Any..isfrom_bool(v1) && Any..isfrom_int(v2) then
@@ -901,32 +801,25 @@ function PGe (v1: Any, v2: Any) : Any
   else if Any..isfrom_datetime(v1) && Any..isfrom_datetime(v2) then
     from_bool(Any..as_datetime!(v1) >=Any..as_datetime!(v2))
   else
-    exception(UndefinedError ("Operand Type is not defined"))
-};
+    exception(UndefinedError ("Operand Type is not defined"));
 
-function PEq (v: Any, v': Any) : Any {
-  from_bool(normalize_any(v) == normalize_any (v'))
-};
+procedure PEq (v: Any, v': Any) : Any
+return from_bool(normalize_any(v) == normalize_any (v'));
 
-function PNEq (v: Any, v': Any) : Any {
-  from_bool(normalize_any(v) != normalize_any (v'))
-};
+procedure PNEq (v: Any, v': Any) : Any
+return from_bool(normalize_any(v) != normalize_any (v'));
 
 // /////////////////////////////////////////////////////////////////////////////////////
 // Modelling of Python Boolean operations And and Or
 // /////////////////////////////////////////////////////////////////////////////////////
 
-function PAnd (v1: Any, v2: Any) : Any
-{
-  if Any..isexception(v1) then v1 else
-  if ! Any_to_bool (v1) then v1 else v2
-};
+procedure PAnd (v1: Any, v2: Any) : Any
+return if Any..isexception(v1) then v1 else
+  if ! Any_to_bool (v1) then v1 else v2;
 
-function POr (v1: Any, v2: Any) : Any
-{
-  if Any..isexception(v1) then v1 else
-  if Any_to_bool (v1) then v1 else v2
-};
+procedure POr (v1: Any, v2: Any) : Any
+return if Any..isexception(v1) then v1 else
+  if Any_to_bool (v1) then v1 else v2;
 
 // /////////////////////////////////////////////////////////////////////////////////////
 // Modelling of Python arithmetic and bitwise operations
@@ -934,16 +827,15 @@ function POr (v1: Any, v2: Any) : Any
 // int_pow, int_rshift, and float_pow are provided by the factory (PyFactory.lean) with concreteEval.
 // Declared here as external so PPow/PRShift can reference them; they are filtered
 // during Laurel-to-Core translation and the factory provides the Core versions.
-function int_pow (base: int, exp: int) : int
+procedure int_pow (base: int, exp: int) : int
   external;
-function int_rshift (x: int, n: int) : int
+procedure int_rshift (x: int, n: int) : int
   external;
-function float_pow (base: real, exp: real) : real
+procedure float_pow (base: real, exp: real) : real
   external;
 
-function PPow (v1: Any, v2: Any) : Any
-{
-  if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
+procedure PPow (v1: Any, v2: Any) : Any
+return if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
   else if (Any..isfrom_int(v1) && Any..isfrom_int(v2) && Any..as_int!(v2) >= 0) then
     from_int(int_pow(Any..as_int!(v1), Any..as_int!(v2)))
   else if (Any..isfrom_int(v1) && Any..isfrom_int(v2)) then
@@ -955,13 +847,11 @@ function PPow (v1: Any, v2: Any) : Any
   else if (Any..isfrom_int(v1) && Any..isfrom_bool(v2)) then
     from_int(int_pow(Any..as_int!(v1), bool_to_int(Any..as_bool!(v2))))
   else
-    exception(UnimplementedError("Pow is not defined on these input types"))
-};
+    exception(UnimplementedError("Pow is not defined on these input types"));
 
-function PMod (v1: Any, v2: Any) : Any
+procedure PMod (v1: Any, v2: Any) : Any
   requires (Any..isfrom_bool(v2)==>Any..as_bool!(v2)) && (Any..isfrom_int(v2)==>Any..as_int!(v2)!=0)
-{
-  if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
+return if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
   else if Any..isfrom_bool(v1) && Any..isfrom_bool(v2) then
     from_int( bool_to_int(Any..as_bool!(v1)) % bool_to_int(Any..as_bool!(v2)))
   else if Any..isfrom_bool(v1) && Any..isfrom_int(v2) then
@@ -971,16 +861,14 @@ function PMod (v1: Any, v2: Any) : Any
   else if Any..isfrom_int(v1) && Any..isfrom_int(v2) then
     from_int(Any..as_int!(v1) % Any..as_int!(v2))
   else
-    exception(UndefinedError ("Operand Type is not defined"))
-};
+    exception(UndefinedError ("Operand Type is not defined"));
 
 // /////////////////////////////////////////////////////////////////////////////////////
 // Modelling of Python bitwise shift operations
 // /////////////////////////////////////////////////////////////////////////////////////
 
-function PLShift (v1: Any, v2: Any) : Any
-{
-  if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
+procedure PLShift (v1: Any, v2: Any) : Any
+return if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
   else if Any..isfrom_int(v1) && Any..isfrom_int(v2) && Any..as_int!(v2) >= 0 then
     from_int(Any..as_int!(v1) * int_pow(2, Any..as_int!(v2)))
   else if Any..isfrom_bool(v1) && Any..isfrom_int(v2) && Any..as_int!(v2) >= 0 then
@@ -990,12 +878,10 @@ function PLShift (v1: Any, v2: Any) : Any
   else if Any..isfrom_bool(v1) && Any..isfrom_bool(v2) then
     from_int(bool_to_int(Any..as_bool!(v1)) * int_pow(2, bool_to_int(Any..as_bool!(v2))))
   else
-    exception(UndefinedError ("Operand Type is not defined"))
-};
+    exception(UndefinedError ("Operand Type is not defined"));
 
-function PRShift (v1: Any, v2: Any) : Any
-{
-  if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
+procedure PRShift (v1: Any, v2: Any) : Any
+return if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
   else if Any..isfrom_int(v1) && Any..isfrom_int(v2) && Any..as_int!(v2) >= 0 then
     from_int(int_rshift(Any..as_int!(v1), Any..as_int!(v2)))
   else if Any..isfrom_bool(v1) && Any..isfrom_int(v2) && Any..as_int!(v2) >= 0 then
@@ -1005,20 +891,18 @@ function PRShift (v1: Any, v2: Any) : Any
   else if Any..isfrom_bool(v1) && Any..isfrom_bool(v2) then
     from_int(int_rshift(bool_to_int(Any..as_bool!(v1)), bool_to_int(Any..as_bool!(v2))))
   else
-    exception(UndefinedError ("Operand Type is not defined"))
-};
+    exception(UndefinedError ("Operand Type is not defined"));
 
 // /////////////////////////////////////////////////////////////////////////////////////
 // Modelling some datetime-related Python operations, for testing purpose
 // /////////////////////////////////////////////////////////////////////////////////////
 
-function to_string(a: Any) : string;
+procedure to_string(a: Any) : string;
 
-function to_string_any(a: Any) : Any {
-  from_str(to_string(a))
-};
+procedure to_string_any(a: Any) : Any
+return from_str(to_string(a));
 
-function datetime_strptime(dtstring: Any, format: Any) : Any;
+procedure datetime_strptime(dtstring: Any, format: Any) : Any;
 
 procedure datetime_tostring_cancel(dt: Any)
   invokeOn datetime_strptime(to_string_any(dt), from_str ("%Y-%m-%d"))
diff --git a/StrataPython/StrataPython/PythonToLaurel.lean b/StrataPython/StrataPython/PythonToLaurel.lean
index c01919b418..56643346aa 100644
--- a/StrataPython/StrataPython/PythonToLaurel.lean
+++ b/StrataPython/StrataPython/PythonToLaurel.lean
@@ -2383,7 +2383,6 @@ def translateFunction (ctx : TranslationContext) (sourceRange: SourceRange) (fun
       preconditions := typeConstraintPreconditions
       decreases := none
       body := bodyTrans
-      isFunctional := false
     }
     return (proc, {newCtx with variableTypes := []})
 
@@ -2560,7 +2559,6 @@ def mkDefaultInitDecl (className : String) : PythonFunctionDecl × Procedure :=
     inputs := inputs
     outputs := [{name := "LaurelResult", type := AnyTy}]
     preconditions := [{ condition := mkStmtExprMd (StmtExpr.LiteralBool true) }]
-    isFunctional := false
     decreases := none
     body := .Opaque [] .none wildcardModifies
   }
@@ -2753,7 +2751,7 @@ def PreludeInfo.ofLaurelProgram (prog : Laurel.Program) : PreludeInfo where
       | _ => s
   procedures :=
     prog.staticProcedures.foldl (init := {}) fun m p =>
-      if p.body.isExternal || p.isFunctional then m
+      if p.body.isExternal then m
       else
         -- Use "Any" for all parameter types to match the Python→Laurel
         -- pipeline's Any-wrapping convention at call sites.
@@ -2776,8 +2774,6 @@ def PreludeInfo.ofLaurelProgram (prog : Laurel.Program) : PreludeInfo where
             typeTesters := pyLauTypeTesters tys : PyRetInfo }
         some { name := p.name.text, args := args, kwargsName := none, ret := ret }
   functions :=
-    let funcNames := prog.staticProcedures.filterMap fun p =>
-      if p.body.isExternal || !p.isFunctional then none else some p.name.text
     let dtFuncs := prog.types.flatMap fun td =>
       match td with
       | .Datatype dt =>
@@ -2789,12 +2785,12 @@ def PreludeInfo.ofLaurelProgram (prog : Laurel.Program) : PreludeInfo where
         let testers := dt.constructors.map fun c => "is" ++ c.name.text
         ctors ++ destrs ++ testers
       | _ => []
-    funcNames ++ dtFuncs
+    dtFuncs
   maybeExceptionFunctions :=  prog.staticProcedures.filterMap fun p =>
     if p.name.text ∈ AnyMaybeExceptionList then some p.name.text else none
   procedureNames :=
     prog.staticProcedures.filterMap fun p =>
-      if p.body.isExternal || p.isFunctional then none else some p.name.text
+      if p.body.isExternal then none else some p.name.text
   callableProcedures :=
     prog.staticProcedures.foldl (init := {}) fun s p =>
       match p.body with
@@ -2978,7 +2974,6 @@ def pythonToLaurel (info : PreludeInfo)
     preconditions := [],
     decreases := none,
     body := .Opaque [] (some bodyBlock) wildcardModifies
-    isFunctional := false
   }
 
   -- Generate $composite_to_string_<type> and $composite_to_string_any_<type>
@@ -2996,16 +2991,14 @@ def pythonToLaurel (info : PreludeInfo)
         outputs := [{ name := "result", type := mkHighTypeMd .TString }]
         preconditions := []
         decreases := none
-        body := .Opaque [] none wildcardModifies
-        isFunctional := false }
+        body := .Opaque [] none wildcardModifies }
     procedures := procedures.push
       { name := { text := compositeToStringAnyName ct.name.text }
         inputs := [selfParam]
         outputs := [{ name := "result", type := AnyTy }]
         preconditions := []
         decreases := none
-        body := .Opaque [] none wildcardModifies
-        isFunctional := false }
+        body := .Opaque [] none wildcardModifies }
 
   let program : Laurel.Program := {
     staticProcedures := (procedures.push mainProc).toList
diff --git a/StrataPython/StrataPython/Specs/ToLaurel.lean b/StrataPython/StrataPython/Specs/ToLaurel.lean
index d73b80f5e8..afd546ecb1 100644
--- a/StrataPython/StrataPython/Specs/ToLaurel.lean
+++ b/StrataPython/StrataPython/Specs/ToLaurel.lean
@@ -562,7 +562,6 @@ def funcDeclToLaurel (procName : String) (func : FunctionDecl)
     outputs := outputs
     preconditions := []
     decreases := none
-    isFunctional := false
     body := body
   }
 
diff --git a/StrataTest/Languages/Laurel/AbstractToConcreteTreeTranslatorTest.lean b/StrataTest/Languages/Laurel/AbstractToConcreteTreeTranslatorTest.lean
index cfc0740d51..9beb0e824c 100644
--- a/StrataTest/Languages/Laurel/AbstractToConcreteTreeTranslatorTest.lean
+++ b/StrataTest/Languages/Laurel/AbstractToConcreteTreeTranslatorTest.lean
@@ -91,7 +91,7 @@ procedure add(x: int, y: int): int
 #end)
 
 /--
-info: function aFunction(x: int): int
+info: procedure aFunction(x: int): int
 {
   x
 };
@@ -100,7 +100,7 @@ info: function aFunction(x: int): int
 #eval do IO.println (← roundtrip
 #strata
 program Laurel;
-function aFunction(x: int): int
+procedure aFunction(x: int): int
 { x };
 #end)
 
@@ -122,8 +122,8 @@ info: procedure test(x: int): int
   opaque
 {
   if x > 0
-  then x
-  else 0 - x
+    then x
+    else 0 - x
 };
 -/
 #guard_msgs in
@@ -335,9 +335,9 @@ info: procedure earlyExit(b: bool)
   opaque
 {
   if b
-  then {
-    return
-  };
+    then {
+      return
+    };
   assert true
 };
 -/
diff --git a/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean b/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean
index 9580ece5d6..396761d550 100644
--- a/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean
+++ b/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean
@@ -29,8 +29,8 @@ private def printElim (program : StrataDDM.Program) : IO Unit := do
     IO.println (toString (Std.Format.pretty (Std.ToFormat.format proc)))
 
 /--
-info: function nat$constraint(x: int): bool
-x >= 0;
+info: procedure nat$constraint(x: int): bool
+return x >= 0;
 procedure test(n: int)
   returns (r: int)
   requires nat$constraint(n)
@@ -63,16 +63,16 @@ procedure test(n: nat) returns (r: nat) opaque {
 
 -- Scope management: constrained variable in if-branch must not leak into sibling block
 /--
-info: function pos$constraint(v: int): bool
-v > 0;
+info: procedure pos$constraint(v: int): bool
+return v > 0;
 procedure test(b: bool)
   opaque
 {
   if b
-  then {
-    var x: int := 1;
-    assert pos$constraint(x)
-  };
+    then {
+      var x: int := 1;
+      assert pos$constraint(x)
+    };
   {
     var x: int := -5;
     x := -10
@@ -104,8 +104,8 @@ procedure test(b: bool) opaque {
 -- Uninitialized constrained variable: havoc + assume constraint.
 -- The variable has no known value, only the type constraint is assumed.
 /--
-info: function posint$constraint(x: int): bool
-x > 0;
+info: procedure posint$constraint(x: int): bool
+return x > 0;
 procedure f()
   opaque
 {
diff --git a/StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean b/StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean
index 8f652186e9..aa224bf569 100644
--- a/StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean
+++ b/StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean
@@ -18,6 +18,7 @@ generates verification conditions for these preconditions.
 
 /-! ### Safe paths verify cleanly -/
 
+#guard_msgs (drop info) in
 #eval testLaurel
 #strata
 program Laurel;
@@ -30,10 +31,10 @@ procedure safeDivision()
   assert z == 5
 };
 
-function pureDiv(x: int, y: int): int
+procedure pureDiv(x: int, y: int): int
   requires y != 0
 {
-  x / y
+  return x / y
 };
 
 procedure callPureDivSafe()
@@ -47,6 +48,7 @@ procedure callPureDivSafe()
 /-! ### Unsafe division: divisor not constrained, fails verification -/
 
 -- Error ranges are too wide because Core does not use expression locations.
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
@@ -60,19 +62,20 @@ procedure unsafeDivision(x: int)
 
 /-! ### Unsafe call to function with `requires y != 0` -/
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
-function pureDiv(x: int, y: int): int
+procedure pureDiv(x: int, y: int): int
   requires y != 0
 {
-  x / y
+  return x / y
 };
 
 procedure callPureDivUnsafe(x: int)
   opaque
 {
   var z: int := pureDiv(10, x)
-//^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
+//^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: precondition could not be proved
 };
 #end
diff --git a/StrataTest/Languages/Laurel/EliminateDoWhileTest.lean b/StrataTest/Languages/Laurel/EliminateDoWhileTest.lean
index 548073bb0a..136ad79209 100644
--- a/StrataTest/Languages/Laurel/EliminateDoWhileTest.lean
+++ b/StrataTest/Languages/Laurel/EliminateDoWhileTest.lean
@@ -60,7 +60,7 @@ info: procedure basic()
         x := x + 1
       };
       if !(x < 3)
-      then exit $dowhile_exit_0
+        then exit $dowhile_exit_0
     }
   }$dowhile_exit_0;
   assert x == 3
@@ -108,13 +108,13 @@ info: procedure nested()
               y := y + 1
             };
             if !(y < 3)
-            then exit $dowhile_exit_0
+              then exit $dowhile_exit_0
           }
         }$dowhile_exit_0;
         x := x + 1
       };
       if !(x < 3)
-      then exit $dowhile_exit_1
+        then exit $dowhile_exit_1
     }
   }$dowhile_exit_1;
   assert x == 3
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypes.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypes.lean
index 0d15885bc9..e6ffbd6dce 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypes.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypes.lean
@@ -9,6 +9,7 @@ import StrataTest.Util.TestLaurel
 open StrataTest.Util
 open Strata
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
@@ -31,7 +32,7 @@ procedure outputValid(): nat
 
 // Output constraint — invalid return fails
 procedure outputInvalid(): nat
-//                         ^^^ error: postcondition does not hold
+//                         ^^^ error: postcondition could not be proved
   opaque
 {
   return -1
@@ -59,7 +60,7 @@ procedure assignInvalid()
   opaque
 {
   var y: nat := -1
-//^^^^^^^^^^^^^^^^ error: assertion does not hold
+//^^^^^^^^^^^^^^^^ error: assertion could not be proved
 };
 
 // Reassignment to constrained-typed variable — invalid
@@ -68,7 +69,7 @@ procedure reassignInvalid()
 {
   var y: nat := 5;
   y := -1
-//^^^^^^^ error: assertion does not hold
+//^^^^^^^ error: assertion could not be proved
 };
 
 // Argument to constrained-typed parameter — valid
@@ -87,7 +88,7 @@ procedure argInvalid() returns (r: int)
   opaque
 {
   var x: int := takesNat(-1);
-//^^^^^^^^^^^^^^^^^^^^^^^^^^ error: precondition does not hold
+//^^^^^^^^^^^^^^^^^^^^^^^^^^ error: precondition could not be proved
   return x
 };
 
@@ -128,7 +129,7 @@ procedure constrainedInExpr()
 
 // Invalid witness — witness -1 does not satisfy x > 0
 constrained bad = x: int where x > 0 witness -1
-//                                           ^^ error: assertion does not hold
+//                                           ^^ error: assertion could not be proved
 
 // Uninitialized constrained variable — havoc + assume constraint
 procedure uninitNat()
@@ -144,7 +145,7 @@ procedure sideEffect()
   var x : nat;
   var y : int;
   y := (x := -1) + 1;
-//      ^^^^^^^ error: assertion does not hold
+//      ^^^^^^^ error: assertion could not be proved
   assert x==-1;
   assert y==0
 };
@@ -164,7 +165,7 @@ procedure uninitNotWitness()
 {
   var y: posnat;
   assert y == 1
-//^^^^^^^^^^^^^ error: assertion does not hold
+//^^^^^^^^^^^^^ error: assertion could not be proved
 };
 
 // Quantifier constraint injection — forall
@@ -198,6 +199,6 @@ procedure captureTest(y: haslarger)
   opaque
 {
   assert false
-//^^^^^^^^^^^^ error: assertion does not hold
+//^^^^^^^^^^^^ error: assertion could not be proved
 };
 #end
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypesError.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypesError.lean
deleted file mode 100644
index 7f523c987b..0000000000
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypesError.lean
+++ /dev/null
@@ -1,32 +0,0 @@
-/-
-  Copyright Strata Contributors
-
-  SPDX-License-Identifier: Apache-2.0 OR MIT
--/
-
-import StrataTest.Util.TestLaurel
-
-open StrataTest.Util
-open Strata
-
-#eval testLaurel <|
-#strata
-program Laurel;
-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
-};
-#end
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T12_Operators.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T12_Operators.lean
index bdfb797d68..de110a7973 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T12_Operators.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T12_Operators.lean
@@ -9,6 +9,7 @@ import StrataTest.Util.TestLaurel
 open StrataTest.Util
 open Strata
 
+#guard_msgs (drop info) in
 #eval testLaurel
 #strata
 program Laurel;
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T13_WhileLoops.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T13_WhileLoops.lean
index 0d7b193c9f..be8c930189 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T13_WhileLoops.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T13_WhileLoops.lean
@@ -9,6 +9,7 @@ import StrataTest.Util.TestLaurel
 open StrataTest.Util
 open Strata
 
+#guard_msgs (drop info) in
 #eval testLaurel
 #strata
 program Laurel;
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T13_WhileLoopsError.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T13_WhileLoopsError.lean
index e55297f647..d660bebe8e 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T13_WhileLoopsError.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T13_WhileLoopsError.lean
@@ -15,6 +15,7 @@ These negative tests pin each failing loop invariant's diagnostic to that
 invariant's own source range (per-invariant source ranges threaded through
 loop elimination), rather than the whole loop. -/
 
+#guard_msgs (drop info) in
 #eval testLaurel
 #strata
 program Laurel;
@@ -31,6 +32,7 @@ procedure badInitialInvariant()
 };
 #end
 
+#guard_msgs (drop info) in
 #eval testLaurel
 #strata
 program Laurel;
@@ -50,6 +52,7 @@ procedure secondInvariantFails()
 };
 #end
 
+#guard_msgs (drop info) in
 #eval testLaurel
 #strata
 program Laurel;
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T14_Quantifiers.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T14_Quantifiers.lean
index 9b5f93f15d..cfa2df1935 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T14_Quantifiers.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T14_Quantifiers.lean
@@ -9,6 +9,7 @@ import StrataTest.Util.TestLaurel
 open StrataTest.Util
 open Strata
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
@@ -31,8 +32,8 @@ procedure testQuantifierInContract(n: int)
 {
 };
 
-function P(x: int): int;
-function Q(): int;
+procedure P(x: int): int;
+procedure Q(): int;
 procedure triggers()
   opaque
 {
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T15_ShortCircuit.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T15_ShortCircuit.lean
index eb7562fe68..0b43e4f267 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T15_ShortCircuit.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T15_ShortCircuit.lean
@@ -9,12 +9,10 @@ import StrataTest.Util.TestLaurel
 open StrataTest.Util
 open Strata
 
+#guard_msgs (drop info) in
 #eval testLaurel
 #strata
 program Laurel;
-function mustNotCallFunc(x: int): int
-  requires false
-{ x };
 
 procedure mustNotCallProc(): int
   requires false
@@ -23,28 +21,6 @@ procedure mustNotCallProc(): int
   return 0
 };
 
-// Pure path: function with requires false
-procedure testAndThenFunc()
-  opaque
-{
-  var b: bool := false && mustNotCallFunc(0) > 0;
-  assert !b
-};
-
-procedure testOrElseFunc()
-  opaque
-{
-  var b: bool := true || mustNotCallFunc(0) > 0;
-  assert b
-};
-
-procedure testImpliesFunc()
-  opaque
-{
-  var b: bool := false ==> mustNotCallFunc(0) > 0;
-  assert b
-};
-
 // Pure path: division by zero
 
 procedure testAndThenDivByZero()
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T16_PropertySummary.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T16_PropertySummary.lean
index 9e063f036d..05b49587de 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T16_PropertySummary.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T16_PropertySummary.lean
@@ -9,6 +9,7 @@ import StrataTest.Util.TestLaurel
 open StrataTest.Util
 open Strata
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
@@ -18,7 +19,7 @@ procedure divide(x: int, y: int) returns (result: int)
   opaque
 {
   assert y == 0 summary "divisor is zero";
-//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: divisor is zero does not hold
+//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: divisor is zero could not be proved
   return x
 };
 
@@ -26,6 +27,6 @@ procedure checkPositive(n: int) returns (ok: bool)
   opaque
 {
   var x: int := divide(3, 0)
-//^^^^^^^^^^^^^^^^^^^^^^^^^^ error: divisor is non-zero does not hold
+//^^^^^^^^^^^^^^^^^^^^^^^^^^ error: divisor is non-zero could not be proved
 };
 #end
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T17_ForLoop.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T17_ForLoop.lean
index bb4358e997..0685370325 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T17_ForLoop.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T17_ForLoop.lean
@@ -9,6 +9,7 @@ import StrataTest.Util.TestLaurel
 open StrataTest.Util
 open Strata
 
+#guard_msgs (drop info) in
 #eval testLaurel
 #strata
 program Laurel;
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T18_RecursiveProcedure.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T18_RecursiveProcedure.lean
index 9a97632738..5c845fc31e 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T18_RecursiveProcedure.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T18_RecursiveProcedure.lean
@@ -14,6 +14,7 @@ A recursive function over a recursive datatype.
 The `isRecursive` flag should be inferred automatically from the self-call.
 -/
 
+#guard_msgs (drop info) in
 #eval testLaurel
 #strata
 program Laurel;
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_BitvectorTypes.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_BitvectorTypes.lean
index 11b55b9dcf..73c6017c87 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_BitvectorTypes.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_BitvectorTypes.lean
@@ -9,6 +9,7 @@ import StrataTest.Util.TestLaurel
 open StrataTest.Util
 open Strata
 
+#guard_msgs (drop info) in
 #eval testLaurel
 #strata
 program Laurel;
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_InvokeOn.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_InvokeOn.lean
index 32efb65c0c..e3f9ad577c 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_InvokeOn.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_InvokeOn.lean
@@ -9,16 +9,17 @@ import StrataTest.Util.TestLaurel
 open StrataTest.Util
 open Strata
 
+#guard_msgs (drop info) in
 #eval testLaurel
     (options := { verifyOptions := { Core.VerifyOptions.quiet with solver := "z3" } })
 #strata
 program Laurel;
-function P(x: int): bool;
-function Q(x: int): bool;
+procedure P(x: int): bool;
+procedure Q(x: int): bool;
 
-function assertP(x: int): int requires P(x);
-function needsPAndQsInvoke1(): int {
-  assertP(3)
+procedure assertP(x: int): int requires P(x);
+procedure needsPAndQsInvoke1(): int {
+  return assertP(3)
 };
 
 procedure PAndQ(x: int)
@@ -26,8 +27,8 @@ procedure PAndQ(x: int)
   opaque
   ensures P(x) && Q(x);
 
-function needsPAndQsInvoke2(): int {
-  assertP(3)
+procedure needsPAndQsInvoke2(): int {
+  return assertP(3)
 };
 
 // The axiom fires because P(x) appears in the goal.
@@ -44,8 +45,8 @@ procedure axiomDoesNotFireBecauseOfPattern(x: int)
 //^^^^^^^^^^^ error: assertion could not be proved
 };
 
-function A(x: int, y: real): bool;
-function B(x: real): bool;
+procedure A(x: int, y: real): bool;
+procedure B(x: real): bool;
 procedure AAndB(x: int, y: real)
   invokeOn A(x, y)
   opaque
@@ -64,7 +65,7 @@ procedure invokeB(x: int, y :real)
 //^^^^^^^^^^^ error: assertion could not be proved
 };
 
-function R(x: int): bool;
+procedure R(x: int): bool;
 procedure badPostcondition(x: int)
   invokeOn R(x)
   opaque
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T1_AssertFalse.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T1_AssertFalse.lean
index c509426b73..18fa27d0a6 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T1_AssertFalse.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T1_AssertFalse.lean
@@ -11,6 +11,7 @@ open Strata
 
 /-! ## Failing asserts -/
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
@@ -27,6 +28,7 @@ procedure foo()
 
 /-! ## Assume false makes assert false trivially provable -/
 
+#guard_msgs (drop info) in
 #eval testLaurel
 #strata
 program Laurel;
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T20_TransparentBody.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T20_TransparentBody.lean
index 1b3ae3aa75..1a8db064e8 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T20_TransparentBody.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T20_TransparentBody.lean
@@ -9,6 +9,7 @@ import StrataTest.Util.TestLaurel
 open StrataTest.Util
 open Strata
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T21_ExitMultiPathAssert.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T21_ExitMultiPathAssert.lean
index 855f23eb43..a4041dbec4 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T21_ExitMultiPathAssert.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T21_ExitMultiPathAssert.lean
@@ -9,6 +9,7 @@ import StrataTest.Util.TestLaurel
 open StrataTest.Util
 open Strata
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T22_ArityMismatch.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T22_ArityMismatch.lean
index 1b4a0ef1a7..6aa57a9703 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T22_ArityMismatch.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T22_ArityMismatch.lean
@@ -24,7 +24,7 @@ info: 32:16-23  error: call to 'f' expects 1 argument(s) but 2 were provided
 #eval testLaurel (showLocations := true) <|
 #strata
 program Laurel;
-function f(x: int): int { x };
+procedure f(x: int): int { return x };
 
 procedure caller()
   opaque
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T22_MultipleReturns.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T22_MultipleReturns.lean
index 3897cae872..5fac9f2338 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T22_MultipleReturns.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T22_MultipleReturns.lean
@@ -9,6 +9,7 @@ import StrataTest.Util.TestLaurel
 open StrataTest.Util
 open Strata
 
+#guard_msgs (drop info) in
 #eval testLaurel
 #strata
 program Laurel;
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T23_IncrDecr.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T23_IncrDecr.lean
index 12871b4353..e77ba754de 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T23_IncrDecr.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T23_IncrDecr.lean
@@ -32,6 +32,7 @@ parameterization which interacts poorly with counterexample search
 for the failing tests in this file).
 -/
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
@@ -132,7 +133,7 @@ procedure forLoopStep()
 
 // --- More complex scenarios -------------------------------------------------
 
-function double(n: int): int { 2 * n };
+procedure double(n: int): int { return 2 * n };
 
 procedure incrementAsFunctionArgument()
   opaque
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T23b_IncrDecrField.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T23b_IncrDecrField.lean
index 4e76ccd357..05854f5c3a 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T23b_IncrDecrField.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T23b_IncrDecrField.lean
@@ -37,6 +37,7 @@ postfix incr/decr ops (`prec(90)`), so `#` binds tighter than `++` and
 valid; `parenFreeFieldIncrDecr` below covers the paren-free form.
 -/
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean
index 5862e9b93f..c27da6dc63 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean
@@ -15,7 +15,7 @@ open Strata
 -- pipeline helper because the expected diagnostics are not pure resolution
 -- errors.
 
-#eval testLaurel <|
+#eval testLaurelKeepIntermediates <|
 #strata
 program Laurel;
 procedure hasMutatingAssignment(): int
@@ -26,21 +26,16 @@ procedure hasMutatingAssignment(): int
   x
 };
 
-function functionWithMutatingAssignment(x: int): int
-{
-  x := x + 1
-//^^^^^^^^^^ error: destructive assignments are not supported in transparent bodies or contracts
-};
-
-function functionWithWhile(x: int): int
+procedure functionWithWhile(x: int): int
 {
   while(false) {};
-//^^^^^^^^^^^^^^^ error: loops are not supported in functions or contracts
-  3
+//^^^^^^^^^^^^^^^ error: loops are not supported in transparent bodies or contracts
+  return 3
 };
-function functionCallingHasMutationAssignment(x: int): int
+
+procedure callsHasMutatingAssignment(x: int): int
 {
-  hasMutatingAssignment()
+  return hasMutatingAssignment()
 };
 
 procedure impureContractIsLegal1(x: int)
@@ -49,12 +44,4 @@ procedure impureContractIsLegal1(x: int)
 {
   assert hasMutatingAssignment() == 1
 };
-
-procedure impureContractIsNotLegal2(x: int)
-  requires (x := 2) == 2
-//          ^^^^^^ error: destructive assignments are not supported in transparent bodies or contracts
-  opaque
-{
-  assert (x := 2) == 2
-};
 #end
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError2.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError2.lean
new file mode 100644
index 0000000000..0af4f2e3fc
--- /dev/null
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError2.lean
@@ -0,0 +1,35 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+meta import StrataTest.Util.TestLaurel
+
+open StrataTest.Util
+
+meta section
+
+#eval testLaurel <|
+#strata
+program Laurel;
+
+procedure transparentWithMutatingAssignment(x: int): int
+{
+  x := x + 1;
+//^^^^^^^^^^ error: destructive assignments are not supported in transparent bodies or contracts
+  return 3
+};
+
+procedure impureContractIsNotLegal2(x: int)
+  requires (x := 2) == 2
+//          ^^^^^^ error: destructive assignments are not supported in transparent bodies or contracts
+  opaque
+{
+  assert (x := 2) == 2
+};
+
+#end
+
+end
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean
index 83f3a702a2..7e4390fecc 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean
@@ -9,9 +9,31 @@ import StrataTest.Util.TestLaurel
 open StrataTest.Util
 open Strata
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
+
+procedure letExpressionsInTransparent() returns (r: int) {
+  var x: int := 0;
+  var y: int := x + 1;
+  var z: int := y + 1;
+  return z
+};
+
+procedure callLetExpressionsInTransparent() opaque {
+  var x: int := letExpressionsInTransparent();
+  assert x == 2
+};
+
+procedure assertAndAssumeInTransparent(a: int) returns (r: int)
+{
+  assert 2 == 3;
+//^^^^^^^^^^^^^ error: assertion does not hold
+  assume true;
+  return a
+};
+
 procedure returnAtEnd(x: int) returns (r: int) {
   if x > 0 then {
     if x == 1 then {
@@ -24,9 +46,9 @@ procedure returnAtEnd(x: int) returns (r: int) {
   }
 };
 
-function elseWithCall(): int
+procedure elseWithCall(): int
 {
-  if true then 3 else returnAtEnd(3)
+  return if true then 3 else returnAtEnd(3)
 };
 
 procedure testFunctions()
@@ -56,22 +78,36 @@ procedure guardInFunction(x: int) returns (r: int)
 
 procedure guards(a: int) returns (r: int)
 {
-  var b: int := a + 2;
-  if b > 2 then {
-      var c: int := b + 3;
-      if c > 3 then {
-          return c + 4
+  if a > 2 then {
+      if a > 3 then {
+          return 4
       };
-      var d: int := c + 5;
-      return d + 6
+      return 6
   };
-  var e: int := b + 1;
-  assert e <= 3;
-  assert e < 3;
+  assert a <= 2;
+  assert a < 2;
 //^^^^^^^^^^^^ error: assertion does not hold
-  return e
+  return 5
 };
 
+//
+// procedure guards(a: int) returns (r: int)
+// {
+//   var b: int := a + 2;
+//   if b > 2 then {
+//       var c: int := b + 3;
+//       if c > 3 then {
+//           return c + 4
+//       };
+//       //var d: int := c + 5;
+//       return d + 6
+//   };
+//   //var e: int := b + 1;
+//   assert e <= 3;
+//   assert e < 3;
+//   return e
+// };
+
 procedure dag(a: int) returns (r: int)
   opaque
 {
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean
index a1d8f03ad7..850b05e499 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean
@@ -12,30 +12,10 @@ open Strata
 #eval testLaurel <|
 #strata
 program Laurel;
-function assertAndAssumeInFunctions(a: int) returns (r: int)
-{
-  assert 2 == 3;
-//^^^^^^^^^^^^^ error: asserts are not YET supported in functions or contracts
-  assume true;
-//^^^^^^^^^^^ error: assumes are not YET supported in functions or contracts
-  a
-};
-
-function letsInFunction() returns (r: int) {
-  var x: int := 0;
-  var y: int := x + 1;
-  var z: int := y + 1;
-  z
-};
-
-procedure callLetsInFunction() opaque {
-  var x: int := letsInFunction();
-  assert x == 2
-};
 
-function localVariableWithoutInitializer(): int {
+procedure localVariableWithoutInitializer(): int {
   var x: int;
-//^^^^^^^^^^ error: local variables in functions must have initializers
-  3
+//^^^^^^^^^^ error: local variables must have initializers in transparent bodies or contracts
+  return 3
 };
 #end
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T4b_Exit.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T4b_Exit.lean
index 50d7e25c96..ef6d5f8e29 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T4b_Exit.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T4b_Exit.lean
@@ -9,6 +9,7 @@ import StrataTest.Util.TestLaurel
 open StrataTest.Util
 open Strata
 
+#guard_msgs (drop info) in
 #eval testLaurel
 #strata
 program Laurel;
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCalls.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCalls.lean
index 7f68e3caf6..be801af5cb 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCalls.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCalls.lean
@@ -9,6 +9,7 @@ import StrataTest.Util.TestLaurel
 open StrataTest.Util
 open Strata
 
+#guard_msgs (drop info) in
 #eval testLaurel
 #strata
 program Laurel;
@@ -40,15 +41,4 @@ procedure fooProof()
 //  assert x == y;
 };
 
-function aFunction(x: int): int
-{
-  x
-};
-
-procedure aFunctionCaller()
-  opaque
-{
-  var x: int := aFunction(3);
-  assert x == 3
-};
 #end
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean
index da9a3d6713..99b8bc086e 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean
@@ -9,6 +9,7 @@ import StrataTest.Util.TestLaurel
 open StrataTest.Util
 open Strata
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
@@ -21,7 +22,7 @@ procedure hasRequires(x: int) returns (r: int)
 {
   assert x > 0;
   assert x > 3;
-//^^^^^^^^^^^^ error: assertion does not hold
+//^^^^^^^^^^^^ error: assertion could not be proved
   x + 1
 };
 
@@ -29,24 +30,10 @@ procedure caller()
   opaque
 {
   var x: int := hasRequires(1);
-//^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: precondition does not hold
+//^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: precondition could not be proved
   var y: int := hasRequires(3)
 };
 
-function aFunctionWithPrecondition(x: int): int
-  requires x == 10
-{
-  x
-};
-
-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
-};
-
 procedure multipleRequires(x: int, y: int) returns (r: int)
   requires x > 0
   requires y > 0
@@ -63,18 +50,4 @@ procedure multipleRequiresCaller()
 //^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: precondition could not be proved
 };
 
-function funcMultipleRequires(x: int, y: int): int
-  requires x > 0
-  requires y > 0
-{
-  x + y
-};
-
-procedure funcMultipleRequiresCaller()
-  opaque
-{
-  var a: int := funcMultipleRequires(1, 2);
-  var b: int := funcMultipleRequires(1, -1)
-//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
-};
 #end
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean
index 08e32bff17..877dc94c9f 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean
@@ -9,6 +9,7 @@ import StrataTest.Util.TestLaurel
 open StrataTest.Util
 open Strata
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_PostconditionsErrors.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_PostconditionsErrors.lean
deleted file mode 100644
index c344719e35..0000000000
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_PostconditionsErrors.lean
+++ /dev/null
@@ -1,36 +0,0 @@
-/-
-  Copyright Strata Contributors
-
-  SPDX-License-Identifier: Apache-2.0 OR MIT
--/
-
-import StrataTest.Util.TestLaurel
-
-open StrataTest.Util
-open Strata
-
-/-! ## Functions with postconditions are not yet supported -/
-
-#eval testLaurel <|
-#strata
-program Laurel;
-
-function opaqueFunction(x: int) returns (r: int)
-//       ^^^^^^^^^^^^^^ error: functions with postconditions are not yet supported
-// The above limitation is because Core does not yet support functions with postconditions
-  requires x > 0
-  opaque
-  ensures r > 0
-{
-  x
-};
-
-procedure callerOfOpaqueFunction()
-  opaque
-{
-  var x: int := opaqueFunction(3);
-  assert x > 0;
-// The following assertion should fail but does not
-  assert x == 3
-};
-#end
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8b_EarlyReturnPostconditions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8b_EarlyReturnPostconditions.lean
index 66a71def1c..7e2ab91e17 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8b_EarlyReturnPostconditions.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8b_EarlyReturnPostconditions.lean
@@ -11,6 +11,7 @@ open Strata
 
 /-! ## Correct early return -/
 
+#guard_msgs (drop info) in
 #eval testLaurel
 #strata
 program Laurel;
@@ -27,6 +28,7 @@ procedure earlyReturnCorrect(x: int) returns (r: int)
 
 /-! ## Buggy early return: postcondition fails -/
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T10_CompositeBvField.lean b/StrataTest/Languages/Laurel/Examples/Objects/T10_CompositeBvField.lean
index d60053efef..c0e0d40289 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T10_CompositeBvField.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T10_CompositeBvField.lean
@@ -14,6 +14,7 @@ import StrataTest.Util.TestLaurel
 open StrataTest.Util
 open Strata
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean b/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean
index 4bca875744..a2b1333a16 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean
@@ -9,7 +9,8 @@ import StrataTest.Util.TestLaurel
 open StrataTest.Util
 open Strata
 
-#eval testLaurelKeepIntermediates
+#guard_msgs (drop info) in
+#eval testLaurel
 #strata
 program Laurel;
 composite Container {
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T1b_HeapMutatingValueReturn.lean b/StrataTest/Languages/Laurel/Examples/Objects/T1b_HeapMutatingValueReturn.lean
index 1a18972604..0bfcac23cd 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T1b_HeapMutatingValueReturn.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T1b_HeapMutatingValueReturn.lean
@@ -11,6 +11,7 @@ open Strata
 
 /-! ## Correct heap mutating value return -/
 
+#guard_msgs (drop info) in
 #eval testLaurel
 #strata
 program Laurel;
@@ -30,6 +31,7 @@ procedure setAndReturn(c: Container, x: int) returns (r: int)
 
 /-! ## Buggy: postcondition r == x + 1 cannot hold when r := x -/
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
@@ -40,7 +42,7 @@ composite Container {
 procedure setAndReturnBuggy(c: Container, x: int) returns (r: int)
   opaque
   ensures r == x + 1
-//        ^^^^^^^^^^ error: postcondition does not hold
+//        ^^^^^^^^^^ error: postcondition could not be proved
   modifies c
 {
   c#value := x;
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T2_ModifiesClauses.lean b/StrataTest/Languages/Laurel/Examples/Objects/T2_ModifiesClauses.lean
index ed9bfc9301..fd7f32dd0b 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T2_ModifiesClauses.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T2_ModifiesClauses.lean
@@ -19,6 +19,7 @@ import StrataTest.Util.TestLaurel
 open StrataTest.Util
 open Strata
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T5_inheritance.lean b/StrataTest/Languages/Laurel/Examples/Objects/T5_inheritance.lean
index 3899f9e3a1..80b1d97207 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T5_inheritance.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T5_inheritance.lean
@@ -9,6 +9,7 @@ import StrataTest.Util.TestLaurel
 open StrataTest.Util
 open Strata
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T6_Datatypes.lean b/StrataTest/Languages/Laurel/Examples/Objects/T6_Datatypes.lean
index 896474404b..a0bc1e12e0 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T6_Datatypes.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T6_Datatypes.lean
@@ -9,6 +9,7 @@ import StrataTest.Util.TestLaurel
 open StrataTest.Util
 open Strata
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
@@ -51,14 +52,13 @@ procedure unsafeDestructor() opaque {
 //^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
 };
 
-// Datatype in function
-function listHead(xs: IntList): int
+procedure listHead(xs: IntList): int
   requires IntList..isCons(xs)
 {
-  IntList..head(xs)
+  return IntList..head(xs)
 };
 
-procedure testFunction() opaque {
+procedure testListHead() opaque {
   var xs: IntList := Cons(10, Nil());
   var h: int := listHead(xs);
   assert h == 10
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T7_InstanceProcedures.lean b/StrataTest/Languages/Laurel/Examples/Objects/T7_InstanceProcedures.lean
index 08638d1c7f..beec222d33 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T7_InstanceProcedures.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T7_InstanceProcedures.lean
@@ -22,6 +22,7 @@ open Strata
 
 /-! ## 1. Basic instance method call: `c#reset()` -/
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
@@ -49,6 +50,7 @@ procedure useCounter()
     Without per-composite scoping, `tick` would collide in the global scope
     during pre-registration. -/
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
@@ -93,6 +95,7 @@ procedure runClock()
 
 /-! ## 3. Method with multiple parameters: `c#setTo(v)` -/
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
@@ -119,6 +122,7 @@ procedure useCell(x: int)
 /-! ## 4. Boolean-typed field updated through an instance method, and read
     back via field access in the caller's `assert`. -/
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
@@ -147,6 +151,7 @@ procedure useWidget()
     only `a`; the unused `b` parameter is included to confirm method
     dispatch picks the right receiver. -/
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
@@ -174,6 +179,7 @@ procedure resetTwoCounters(a: Counter, b: Counter)
     confirms an extra (unused) method parameter doesn't break call
     dispatch or framing. -/
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
@@ -200,6 +206,7 @@ procedure useAccount()
 /-! ## 7. Instance method called through a field-selected receiver:
     `obj#field#method()`. -/
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
@@ -225,6 +232,7 @@ procedure useOuter()
 
 /-! ## 8. Chained field read: `obj#field#x`. -/
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T8_NonCompositeModifies.lean b/StrataTest/Languages/Laurel/Examples/Objects/T8_NonCompositeModifies.lean
index 87a6e2424d..3c491e1c73 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T8_NonCompositeModifies.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T8_NonCompositeModifies.lean
@@ -16,6 +16,7 @@ import StrataTest.Util.TestLaurel
 open StrataTest.Util
 open Strata
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T9_ValueReturningInstanceMethods.lean b/StrataTest/Languages/Laurel/Examples/Objects/T9_ValueReturningInstanceMethods.lean
index fb7249ddb7..d9ebc7d6d5 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T9_ValueReturningInstanceMethods.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T9_ValueReturningInstanceMethods.lean
@@ -32,6 +32,7 @@ open Strata
 
 /-! ## 1. Basic: instance method body returns a field via `return expr`. -/
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
@@ -56,6 +57,7 @@ procedure useGet()
 
 /-! ## 2. Return a computed expression. -/
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
@@ -80,6 +82,7 @@ procedure useIncd()
 
 /-! ## 3. Return an expression that uses a (non-self) parameter. -/
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
@@ -105,6 +108,7 @@ procedure useAddTo()
 /-! ## 4. Conditional / early returns: a valued `return` in each branch of an
     if-then-else inside the method body. -/
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
@@ -133,6 +137,7 @@ procedure useClampPos()
 
 /-! ## 5. Method that mutates a field (modifies clause) and then returns. -/
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
@@ -161,6 +166,7 @@ procedure useSetAndGet()
 
 /-! ## 6. Boolean return type. -/
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
@@ -186,6 +192,7 @@ procedure useIsPos()
 /-! ## 7. Two composites sharing a method name, both with value-returning
     bodies. Confirms lifting + value-return elimination keep them distinct. -/
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
@@ -224,6 +231,7 @@ procedure useBoth()
 /-! ## 8. Value-returning method invoked through a field-selected receiver:
     `o#inner#getX()`. -/
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
@@ -252,6 +260,7 @@ procedure useOuter()
 
 /-! ## 9. Local variable in the body before a valued return. -/
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
@@ -278,6 +287,7 @@ procedure useDoubleV()
 /-! ## 10. Negative: valued return in an instance method with NO output
     parameter is rejected by `EliminateValueInReturns`. -/
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
@@ -295,6 +305,7 @@ composite C {
 /-! ## 11. Negative: valued return in an instance method with MULTIPLE output
     parameters is rejected by `EliminateValueInReturns`. -/
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
diff --git a/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T1_Decimals.lean b/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T1_Decimals.lean
index 0a1280653c..b574c79b31 100644
--- a/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T1_Decimals.lean
+++ b/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T1_Decimals.lean
@@ -9,6 +9,7 @@ import StrataTest.Util.TestLaurel
 open StrataTest.Util
 open Strata
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
diff --git a/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T2_String.lean b/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T2_String.lean
index 0528672ee8..0a718b7b92 100644
--- a/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T2_String.lean
+++ b/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T2_String.lean
@@ -10,6 +10,7 @@ import StrataTest.Util.TestLaurel
 open StrataTest.Util
 open Strata
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
diff --git a/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T2_StringConcatLifting.lean b/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T2_StringConcatLifting.lean
index cc3756bed8..c223b3e3bd 100644
--- a/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T2_StringConcatLifting.lean
+++ b/StrataTest/Languages/Laurel/Examples/PrimitiveTypes/T2_StringConcatLifting.lean
@@ -9,6 +9,7 @@ import StrataTest.Util.TestLaurel
 open StrataTest.Util
 open Strata
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
diff --git a/StrataTest/Languages/Laurel/IncrDecrTypeRejectionTest.lean b/StrataTest/Languages/Laurel/IncrDecrTypeRejectionTest.lean
index 33c166b4c9..ad6cda63b6 100644
--- a/StrataTest/Languages/Laurel/IncrDecrTypeRejectionTest.lean
+++ b/StrataTest/Languages/Laurel/IncrDecrTypeRejectionTest.lean
@@ -21,6 +21,7 @@ open Strata
 
 /-! ## Rejected: `++`/`--` on unsupported element types -/
 
+#guard_msgs (drop info) in
 #eval testLaurelResolution <|
 #strata
 program Laurel;
@@ -43,6 +44,7 @@ procedure incrFloat(g: float64) opaque {
 
 /-! ## Accepted: `++`/`--` on an int-based constrained type (e.g. `nat`) -/
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
diff --git a/StrataTest/Languages/Laurel/LiftHolesTest.lean b/StrataTest/Languages/Laurel/LiftHolesTest.lean
index a7d9879b9d..680c1353b6 100644
--- a/StrataTest/Languages/Laurel/LiftHolesTest.lean
+++ b/StrataTest/Languages/Laurel/LiftHolesTest.lean
@@ -6,7 +6,7 @@
 
 /-
 Tests that the eliminateHoles pass correctly replaces `.Hole` nodes with calls
-to freshly generated uninterpreted functions, with types inferred from context.
+to freshly generated uninterpreted procedures, with types inferred from context.
 -/
 
 import StrataTest.Util.TestLaurel
@@ -32,7 +32,7 @@ private def parseElimAndPrint (program : StrataDDM.Program) : IO Unit := do
 
 -- Hole in Add arg inside typed local variable → int.
 /--
-info: function $hole_0()
+info: procedure $hole_0()
   returns ($result: int)
   opaque;
 procedure test()
@@ -52,7 +52,7 @@ procedure test()
 
 -- Bare Hole as Assign Declare initializer → replaced with call (no longer preserved as havoc).
 /--
-info: function $hole_0()
+info: procedure $hole_0()
   returns ($result: int)
   opaque;
 procedure test()
@@ -72,7 +72,7 @@ procedure test()
 
 -- Hole in comparison arg inside assert → int (inferred from sibling literal).
 /--
-info: function $hole_0()
+info: procedure $hole_0()
   returns ($result: int)
   opaque;
 procedure test()
@@ -92,7 +92,7 @@ procedure test()
 
 -- Hole directly as assert condition → bool.
 /--
-info: function $hole_0()
+info: procedure $hole_0()
   returns ($result: bool)
   opaque;
 procedure test()
@@ -112,7 +112,7 @@ procedure test()
 
 -- Hole directly as assume condition → bool.
 /--
-info: function $hole_0()
+info: procedure $hole_0()
   returns ($result: bool)
   opaque;
 procedure test()
@@ -132,16 +132,16 @@ procedure test()
 
 -- Hole as if-then-else condition → bool.
 /--
-info: function $hole_0()
+info: procedure $hole_0()
   returns ($result: bool)
   opaque;
 procedure test()
   opaque
 {
   if $hole_0()
-  then {
-    assert true
-  }
+    then {
+      assert true
+    }
 };
 -/
 #guard_msgs in
@@ -155,15 +155,15 @@ procedure test()
 
 -- Hole in then-branch of if-then-else inside typed local variable → int.
 /--
-info: function $hole_0()
+info: procedure $hole_0()
   returns ($result: int)
   opaque;
 procedure test()
   opaque
 {
   var x: int := if true
-  then $hole_0()
-  else 0
+    then $hole_0()
+    else 0
 };
 -/
 #guard_msgs in
@@ -177,7 +177,7 @@ procedure test()
 
 -- Hole as while-loop condition → bool.
 /--
-info: function $hole_0()
+info: procedure $hole_0()
   returns ($result: bool)
   opaque;
 procedure test()
@@ -199,7 +199,7 @@ procedure test()
 
 -- Hole as while-loop invariant → bool.
 /--
-info: function $hole_0()
+info: procedure $hole_0()
   returns ($result: bool)
   opaque;
 procedure test()
@@ -224,7 +224,7 @@ procedure test()
 
 -- Hole in And arg inside assert → bool.
 /--
-info: function $hole_0()
+info: procedure $hole_0()
   returns ($result: bool)
   opaque;
 procedure test()
@@ -244,7 +244,7 @@ procedure test()
 
 -- Hole in Neg inside typed local variable → int.
 /--
-info: function $hole_0()
+info: procedure $hole_0()
   returns ($result: int)
   opaque;
 procedure test()
@@ -264,7 +264,7 @@ procedure test()
 
 -- Hole in StrConcat inside typed local variable → string.
 /--
-info: function $hole_0()
+info: procedure $hole_0()
   returns ($result: string)
   opaque;
 procedure test()
@@ -282,12 +282,12 @@ procedure test()
 
 /-! ## Multiple holes -/
 
--- Two holes in Add → both int, separate functions.
+-- Two holes in Add → both int, separate procedures.
 /--
-info: function $hole_0()
+info: procedure $hole_0()
   returns ($result: int)
   opaque;
-function $hole_1()
+procedure $hole_1()
   returns ($result: int)
   opaque;
 procedure test()
@@ -307,10 +307,10 @@ procedure test()
 
 -- Holes across statements: Mul arg (int) then assert condition (bool).
 /--
-info: function $hole_0()
+info: procedure $hole_0()
   returns ($result: int)
   opaque;
-function $hole_1()
+procedure $hole_1()
   returns ($result: bool)
   opaque;
 procedure test()
@@ -333,16 +333,16 @@ procedure test()
 
 -- Hole in Add inside Gt inside if condition → int (inferred from sibling literal 0).
 /--
-info: function $hole_0()
+info: procedure $hole_0()
   returns ($result: int)
   opaque;
 procedure test()
   opaque
 {
   if 1 + $hole_0() > 0
-  then {
-    assert true
-  }
+    then {
+      assert true
+    }
 };
 -/
 #guard_msgs in
@@ -356,7 +356,7 @@ procedure test()
 
 -- Hole in Implies inside while invariant → bool.
 /--
-info: function $hole_0()
+info: procedure $hole_0()
   returns ($result: bool)
   opaque;
 procedure test()
@@ -380,7 +380,7 @@ procedure test()
 
 -- Hole in Mul inside typed local variable with real type → real.
 /--
-info: function $hole_0()
+info: procedure $hole_0()
   returns ($result: real)
   opaque;
 procedure test()
@@ -400,9 +400,9 @@ procedure test()
 
 /-! ## Call argument and return type inference -/
 
--- Hole in comparison with variable sibling → hole function takes the procedure's params.
+-- Hole in comparison with variable sibling → hole procedure takes the procedure's params.
 /--
-info: function $hole_0(n: int)
+info: procedure $hole_0(n: int)
   returns ($result: int)
   opaque;
 procedure test(n: int)
@@ -420,14 +420,14 @@ procedure test(n: int)
 { assert n > <?> };
 #end
 
-/-! ## Holes in functions -/
+/-! ## Holes in procedures -/
 
--- Hole in function body → same treatment as procedures.
+-- Hole in procedure body → same treatment as procedures.
 /--
-info: function $hole_0(x: int)
+info: procedure $hole_0(x: int)
   returns ($result: int)
   opaque;
-function test(x: int): int
+procedure test(x: int): int
 {
   $hole_0(x)
 };
@@ -436,7 +436,7 @@ function test(x: int): int
 #eval! parseElimAndPrint
 #strata
 program Laurel;
-function test(x: int): int
+procedure test(x: int): int
 { <?> };
 #end
 
@@ -461,7 +461,7 @@ procedure test()
 
 -- Mixed: det hole eliminated, nondet hole preserved.
 /--
-info: function $hole_0()
+info: procedure $hole_0()
   returns ($result: int)
   opaque;
 procedure test()
@@ -480,7 +480,7 @@ procedure test()
 { var x: int := <?>; assert <??> };
 #end
 
--- Nondet hole in function → should be rejected (not tested here since
+-- Nondet hole in procedure → should be rejected (not tested here since
 -- the error occurs at Core translation time, which requires the full pipeline).
 
 /-! ## Holes inside datatype destructor / tester arguments -/
@@ -491,7 +491,7 @@ procedure test()
 -- parent datatype's resolved Identifier (with `uniqueId`), so this works
 -- without textual decoding of the override name.
 /--
-info: function $hole_0()
+info: procedure $hole_0()
   returns ($result: IntList)
   opaque;
 procedure test()
@@ -509,7 +509,7 @@ procedure test() { var x: int := IntList..head(<?>) };
 
 -- Hole as argument to an unsafe `!` destructor → same datatype recovery.
 /--
-info: function $hole_0()
+info: procedure $hole_0()
   returns ($result: IntList)
   opaque;
 procedure test()
@@ -527,7 +527,7 @@ procedure test() { var x: int := IntList..head!(<?>) };
 
 -- Hole as argument to a tester → typed as the parent datatype.
 /--
-info: function $hole_0()
+info: procedure $hole_0()
   returns ($result: IntList)
   opaque;
 procedure test()
diff --git a/StrataTest/Languages/Laurel/MapStmtExprTest.lean b/StrataTest/Languages/Laurel/MapStmtExprTest.lean
index eee5f05fa0..32656be094 100644
--- a/StrataTest/Languages/Laurel/MapStmtExprTest.lean
+++ b/StrataTest/Languages/Laurel/MapStmtExprTest.lean
@@ -8,16 +8,21 @@
 Tests for the generic `mapStmtExprM` traversal. Verifies that `mapStmtExpr id`
 is the identity: applying it to a parsed program produces identical output.
 -/
+module
 
-import StrataTest.Util.TestLaurel
-import Strata.Languages.Laurel.MapStmtExpr
-import Strata.Languages.Laurel.Resolution
+meta import StrataTest.Util.TestLaurel
+meta import Strata.Languages.Laurel.MapStmtExpr
+meta import Strata.Languages.Laurel.Resolution
+meta import Strata.Languages.Laurel.Grammar
+meta import StrataDDM.Integration.Lean.HashCommands
 
 open Strata
 open StrataTest.Util
 
 namespace Strata.Laurel
 
+meta section
+
 private def parseAndResolve (program : StrataDDM.Program) : IO Program := do
   let laurelProgram ← translateLaurel program
   pure (resolve laurelProgram).program
@@ -75,4 +80,6 @@ procedure test(x: int, b: bool) returns (r: int)
 };
 #end
 
+end
+
 end Strata.Laurel
diff --git a/StrataTest/Languages/Laurel/ResolutionTypeCheckTests.lean b/StrataTest/Languages/Laurel/ResolutionTypeCheckTests.lean
index e3888db451..32b94132a1 100644
--- a/StrataTest/Languages/Laurel/ResolutionTypeCheckTests.lean
+++ b/StrataTest/Languages/Laurel/ResolutionTypeCheckTests.lean
@@ -31,7 +31,7 @@ procedure voidReturn(x: int)
 #eval testLaurelResolution <|
 #strata
 program Laurel;
-function foo(x: int): int {
+procedure foo(x: int): int {
   if x then 1 else 0
 //   ^ error: expected 'bool', got 'int'
 };
@@ -72,7 +72,7 @@ procedure wh() opaque {
 #eval testLaurelResolution <|
 #strata
 program Laurel;
-function foo(x: int, y: bool): bool {
+procedure foo(x: int, y: bool): bool {
   x && y
 //^ error: expected 'bool', got 'int'
 };
@@ -83,7 +83,7 @@ function foo(x: int, y: bool): bool {
 #eval testLaurelResolution <|
 #strata
 program Laurel;
-function cmp(x: string, y: int): bool {
+procedure cmp(x: string, y: int): bool {
   x < y
 //^ error: '<' expected a numeric type, got 'string'
 };
@@ -116,8 +116,8 @@ procedure foo(): int {
 #eval testLaurelResolution <|
 #strata
 program Laurel;
-function bar(x: int): int { x };
-function foo(): int {
+procedure bar(x: int): int { x };
+procedure foo(): int {
   bar(true)
 //    ^^^^ error: expected 'int', got 'bool'
 };
@@ -128,7 +128,7 @@ function foo(): int {
 #eval testLaurelResolution <|
 #strata
 program Laurel;
-function cmp(x: int, y: string): bool {
+procedure cmp(x: int, y: string): bool {
   x == y
 //^^^^^^ error: cannot compare 'int' with 'string' using '=='
 };
@@ -225,7 +225,7 @@ cleanly (no diagnostics). -/
 #eval testLaurelResolution <|
 #strata
 program Laurel;
-function foo(c: bool): bool {
+procedure foo(c: bool): bool {
   (if c then 1 else 2) == 3
 };
 #end
@@ -233,7 +233,7 @@ function foo(c: bool): bool {
 #eval testLaurelResolution <|
 #strata
 program Laurel;
-function foo(): bool {
+procedure foo(): bool {
   { 1 } == 1
 };
 #end
@@ -247,7 +247,7 @@ and synthesizes `Unknown` to suppress cascading errors. -/
 #eval testLaurelResolution <|
 #strata
 program Laurel;
-function foo(c: bool): bool {
+procedure foo(c: bool): bool {
   (if c then 1 else true) == 3
 // ^^^^^^^^^^^^^^^^^^^^^ error: 'if' branches have incompatible types 'int' and 'bool'
 };
@@ -269,7 +269,7 @@ errored.) -/
 #eval testLaurelResolution <|
 #strata
 program Laurel;
-function foo(c: bool): bool {
+procedure foo(c: bool): bool {
   (if c then <?> else "x") < 1
 // ^^^^^^^^^^^^^^^^^^^^^^ error: '<' expected a numeric type, got 'string'
 };
@@ -278,7 +278,7 @@ function foo(c: bool): bool {
 #eval testLaurelResolution <|
 #strata
 program Laurel;
-function foo(c: bool): bool {
+procedure foo(c: bool): bool {
   (if c then "x" else <?>) < 1
 // ^^^^^^^^^^^^^^^^^^^^^^ error: '<' expected a numeric type, got 'string'
 };
@@ -294,7 +294,7 @@ than collapsing to `Unknown`. So `if c then <?> else 5` synthesizes a usable
 #eval testLaurelResolution <|
 #strata
 program Laurel;
-function bar(c: bool): int {
+procedure bar(c: bool): int {
   if c then <?> else 5
 };
 #end
@@ -328,7 +328,7 @@ rejecting `TBv` and emitting a spurious "expected a numeric type" error.) -/
 #eval testLaurelResolution <|
 #strata
 program Laurel;
-function cmp(x: bv 32, y: bv 32): bool {
+procedure cmp(x: bv 32, y: bv 32): bool {
   x < y
 };
 #end
@@ -343,8 +343,8 @@ arguments) is deliberately not flagged. -/
 #eval testLaurelResolution <|
 #strata
 program Laurel;
-function foo(x: int): int { x };
-function bar(): int {
+procedure foo(x: int): int { x };
+procedure bar(): int {
   foo(1, 2)
 //^^^^^^^^^ error: call to 'foo' expects 1 argument(s) but 2 were provided
 };
@@ -362,7 +362,7 @@ behavior.) -/
 #eval testLaurelResolution <|
 #strata
 program Laurel;
-function bar(): int {
+procedure bar(): int {
   nope(1, 2)
 //^^^^^^^^^^ error: 'nope' is not defined
 };
diff --git a/StrataTest/Languages/Laurel/StrataExpectSmokeTest.lean b/StrataTest/Languages/Laurel/StrataExpectSmokeTest.lean
index ea6ba94d08..e12c9b603b 100644
--- a/StrataTest/Languages/Laurel/StrataExpectSmokeTest.lean
+++ b/StrataTest/Languages/Laurel/StrataExpectSmokeTest.lean
@@ -16,6 +16,7 @@ open Strata
 
 /-! ## Positive smoke test -/
 
+#guard_msgs (drop info) in
 #eval testLaurel
 #strata
 program Laurel;
@@ -37,6 +38,7 @@ procedure foo() opaque {
 
 /-! ## Negative smoke test: a verifier-level diagnostic. -/
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
diff --git a/StrataTest/Languages/Laurel/TypeAliasElimTest.lean b/StrataTest/Languages/Laurel/TypeAliasElimTest.lean
index 6295539cab..2a613012ca 100644
--- a/StrataTest/Languages/Laurel/TypeAliasElimTest.lean
+++ b/StrataTest/Languages/Laurel/TypeAliasElimTest.lean
@@ -32,8 +32,7 @@ private def mkTy (ty : HighType) : HighTypeMd := { val := ty, source := none }
 /-- Helper: construct a minimal procedure. -/
 private def mkProc (name : String) (inputs : List Parameter) (outputs : List Parameter)
     (body : Body := .Transparent ⟨.Block [] none, none⟩) : Procedure :=
-  { name := mkId name, inputs, outputs, preconditions := [], decreases := none,
-    isFunctional := false, body }
+  { name := mkId name, inputs, outputs, preconditions := [], decreases := none, body }
 
 /-- Helper: run resolve + typeAliasElim on a program. -/
 private def resolveAndElim (program : Program) : Program :=
diff --git a/StrataTest/Util/TestLaurel.lean b/StrataTest/Util/TestLaurel.lean
index 718a38bbaa..bc36b7eb8b 100644
--- a/StrataTest/Util/TestLaurel.lean
+++ b/StrataTest/Util/TestLaurel.lean
@@ -3,14 +3,16 @@
 
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
+module
 
+public import Strata.Languages.Laurel.Grammar.LaurelGrammar
+public import Strata.Languages.Laurel.LaurelCompilationPipeline
+public import StrataDDM.Integration.Lean.HashCommands
 import StrataDDM.Integration.Lean.HashCommands
 import StrataDDM.Elab
 import StrataDDM.BuiltinDialects.Init
-import Strata.Languages.Laurel.Grammar.LaurelGrammar
 import Strata.Languages.Laurel.Grammar.ConcreteToAbstractTreeTranslator
 import Strata.Languages.Laurel.Resolution
-import Strata.Languages.Laurel.LaurelCompilationPipeline
 import Strata.Languages.Laurel
 
 open Strata
@@ -22,7 +24,7 @@ namespace StrataTest.Util
 /-- Translate a `StrataDDM.Program` (typically produced by `#strata`) to a Laurel
     `Program`. Used by tests that need to plug in a custom post-translation
     pipeline stage; throws if translation fails. -/
-def translateLaurel (program : StrataDDM.Program) : IO Laurel.Program := do
+public def translateLaurel (program : StrataDDM.Program) : IO Laurel.Program := do
   match Laurel.TransM.run (Strata.Uri.file "<#strata>") (Laurel.parseProgram program) with
   | .error e => throw (IO.userError s!"Translation errors: {e}")
   | .ok laurelProgram => pure laurelProgram
@@ -48,7 +50,7 @@ private def renderSnippetLocal (basePos : Nat) (snippet : String)
 /-- Default options used by `testLaurel` when the caller doesn't override:
     quiet verifier, default solver. Override by passing
     `(options := …)` to `testLaurel`. -/
-def defaultLaurelTestOptions : LaurelVerifyOptions :=
+public def defaultLaurelTestOptions : LaurelVerifyOptions :=
   { verifyOptions := .quiet }
 
 /-- Run translate + resolve only on a parsed program. Skips SMT verification.
@@ -342,7 +344,7 @@ private def runAndCheck (block : SourcedProgram)
     file-relative `line:col` range (so a `#guard_msgs` golden can pin the
     localization), and `showSnippet := true` to also append the snippet-relative
     range. (Failure reports always use the file-relative format regardless.) -/
-def testLaurel (block : SourcedProgram)
+public def testLaurel (block : SourcedProgram)
     (options : LaurelVerifyOptions := defaultLaurelTestOptions)
     (showLocations : Bool := false) (showSnippet : Bool := false) : IO Unit :=
   runAndCheck block (runLaurelPipelineRaw · options) showLocations showSnippet
@@ -353,7 +355,7 @@ def buildDir : IO String := do
   let cwd ← IO.currentDir
   return s!"{cwd}/.lake/build/intermediatePrograms/"
 
-def testLaurelKeepIntermediates (block : SourcedProgram) : IO Unit := do
+public def testLaurelKeepIntermediates (block : SourcedProgram) : IO Unit := do
   let dir ← buildDir
   runAndCheck block (runLaurelPipelineRaw · { translateOptions := { keepAllFilesPrefix := dir}})
 
@@ -365,7 +367,7 @@ def testLaurelKeepIntermediates (block : SourcedProgram) : IO Unit := do
     As with `testLaurel`, succeeds silently by default; `showLocations := true`
     echoes each diagnostic's file-relative `line:col` range and
     `showSnippet := true` appends the snippet-relative range. -/
-def testLaurelResolution (block : SourcedProgram)
+public def testLaurelResolution (block : SourcedProgram)
     (showLocations : Bool := false) (showSnippet : Bool := false) : IO Unit :=
   runAndCheck block runLaurelResolutionRaw showLocations showSnippet