diff --git a/Strata/Languages/Laurel/ConstrainedTypeElim.lean b/Strata/Languages/Laurel/ConstrainedTypeElim.lean
index 7fdaf3f7c6..566dab3ae6 100644
--- a/Strata/Languages/Laurel/ConstrainedTypeElim.lean
+++ b/Strata/Languages/Laurel/ConstrainedTypeElim.lean
@@ -75,7 +75,7 @@ def constraintCallFor (ptMap : ConstrainedTypeMap) (ty : HighType)
     For nested types, the function calls the parent's constraint function. -/
 def mkConstraintFunc (ptMap : ConstrainedTypeMap) (ct : ConstrainedType) : Procedure :=
   let baseType := resolveType ptMap ct.base
-  let bodyExpr := match ct.base.val with
+  let bodyExpr: StmtExprMd := match ct.base.val with
     | .UserDefined parent =>
       if ptMap.contains parent.text then
         let paramId := { ct.valueName with uniqueId := none }
@@ -89,7 +89,7 @@ def mkConstraintFunc (ptMap : ConstrainedTypeMap) (ct : ConstrainedType) : Proce
   { name := mkId s!"{ct.name.text}$constraint"
     inputs := [{ name := ct.valueName, type := baseType }]
     outputs := [{ name := mkId "result", type := { val := .TBool, source := none } }]
-    body := .Transparent { val := .Block [bodyExpr] none, source := none }
+    body := .Transparent { val := .Return bodyExpr, source := none }
     isFunctional := true
     decreases := none
     preconditions := [] }
@@ -244,11 +244,11 @@ public def constrainedTypeElim (model : SemanticModel) (program : Program)
    funcDiags)
 
 /-- Pipeline pass: constrained type elimination. -/
-public def constrainedTypeElimPass : LaurelPass where
+public def constrainedTypeElimPass : LoweringPass where
   name := "ConstrainedTypeElim"
   documentation := "Eliminates constrained types by replacing them with their base types and generating constraint-checking functions and witness procedures. Type tests against constrained types are rewritten to call the generated constraint function."
   needsResolves := true
-  run := fun p m =>
+  run := fun p m _ =>
     let (p', diags) := constrainedTypeElim m p
     (p', diags, {})
 
diff --git a/Strata/Languages/Laurel/ContractPass.lean b/Strata/Languages/Laurel/ContractPass.lean
new file mode 100644
index 0000000000..cc93ba02f9
--- /dev/null
+++ b/Strata/Languages/Laurel/ContractPass.lean
@@ -0,0 +1,461 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+public import Strata.Languages.Laurel.MapStmtExpr
+public import Strata.Languages.Laurel.LaurelPass
+import Strata.Languages.Laurel.EliminateReturnStatements
+import Strata.Util.Tactics
+
+/-!
+## Contract Pass (Laurel → Laurel)
+
+Removes pre- and postconditions from all procedures and replaces them with
+explicit precondition/postcondition helper procedures, assumptions, and
+assertions.
+
+For each procedure with contracts:
+- Generate a separate precondition procedure (`foo$pre0`, `foo$pre1`, ...) for each precondition.
+- Generate a separate postcondition procedure (`foo$post0`, `foo$post1`, ...) for each postcondition.
+  Each takes all inputs and all outputs as parameters and returns the condition.
+- Insert `assume foo$pre0(inputs); assume foo$pre1(inputs); ...` at the start of the body.
+- Insert `assert foo$post0(inputs, outputs); assert foo$post1(inputs, outputs); ...` at the end of the body.
+
+For each call to a contracted procedure:
+- Assign all input arguments to temporary variables before the call.
+- Insert `assert foo$pre0(temps); assert foo$pre1(temps); ...` before the call.
+- After the call, insert `assume foo$post0(temps, outputs); assume foo$post1(temps, outputs); ...`.
+-/
+
+namespace Strata.Laurel
+
+public section
+
+private def mkMd (e : StmtExpr) : StmtExprMd := { val := e, source := none }
+private def mkVarMd (v : Variable) : VariableMd := { val := v, source := none }
+
+/-- Name for the i-th precondition helper procedure. -/
+def preCondProcName (procName : String) (i : Nat) : String := s!"{procName}$pre{i}"
+
+/-- Name for the i-th postcondition helper procedure. -/
+def postCondProcName (procName : String) (i : Nat) : String := s!"{procName}$post{i}"
+
+/-- Get postconditions from a procedure body. -/
+private def getPostconditions (body : Body) : List Condition :=
+  match body with
+  | .Opaque postconds _ _ => postconds
+  | .Abstract postconds => postconds
+  | _ => []
+
+/-- Build a call expression. -/
+private def mkCall (callee : String) (args : List StmtExprMd) : StmtExprMd :=
+  mkMd (.StaticCall (mkId callee) args)
+
+/-- Convert parameters to identifier expressions. -/
+private def paramsToArgs (params : List Parameter) : List StmtExprMd :=
+  params.map fun p => mkMd (.Var (.Local p.name))
+
+/-- Build a helper function for a single condition over the given parameters.
+    Preconditions pass `proc.inputs`; postconditions use `mkPostConditionProc`. -/
+private def mkConditionProc (name : String) (params : List Parameter)
+    (condition : Condition) : Procedure :=
+  { name := mkId name
+    inputs := params
+    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
+    into a postcondition helper *function*.
+
+    A postcondition helper takes both the procedure's inputs and outputs as plain
+    function parameters. When an output shares a name with an input (e.g. an inout
+    `$heap`, which the heap-parameterization pass lists in both `inputs` and
+    `outputs`), the two would collide in the helper's single parameter scope and
+    produce "Duplicate definition '…' is already defined in this scope". Suffixing
+    every output keeps the two distinct. The choice is heap-agnostic: it applies to
+    all outputs, not just `$heap`. -/
+public def outParamSuffix : String := "$out"
+
+/-- Rewrite a postcondition body so it refers to the renamed output parameters.
+
+    In a postcondition, a bare reference to an output parameter denotes its
+    post-state value, while `old(x)` denotes the pre-state value of an inout
+    parameter (the corresponding *input*). The helper is a pure function with two
+    distinct parameters, so:
+    - bare `Var (Local n)` where `n` is an output → suffixed name (`n ++ outParamSuffix`)
+    - `old(Var (Local n))` → `Var (Local n)`, i.e. strip `old` and keep the
+      un-suffixed name so it resolves to the input parameter (functions have no
+      two-state semantics, so an unstripped `old` would later be rejected).
+
+    `pushOldInward` guarantees every `old` immediately wraps a local variable. -/
+private def renameOutputsInPostExpr (outputNames : List String) (expr : StmtExprMd) : StmtExprMd :=
+  let suffixIfOutput (n : Identifier) : Identifier :=
+    if outputNames.contains n.text then mkId (n.text ++ outParamSuffix) else n
+  mapStmtExprPrePostM (m := Id)
+    (fun e =>
+      match e.val with
+      | .Old value =>
+        match value.val with
+        | .Var (.Local _) => some value
+        | _ => none
+      | _ => none)
+    (fun e =>
+      match e.val with
+      | .Var (.Local n) => ⟨.Var (.Local (suffixIfOutput n)), e.source⟩
+      | _ => e)
+    expr
+
+/-- Build a postcondition helper function over the procedure's inputs and outputs.
+    Output parameters are renamed (see `outParamSuffix`) to avoid colliding with
+    identically-named inputs, and the condition body is rewritten to match. -/
+private def mkPostConditionProc (name : String) (inputs outputs : List Parameter)
+    (condition : Condition) : Procedure :=
+  let outputNames := outputs.map (·.name.text)
+  let renamedOutputs := outputs.map (fun p => { p with name := mkId (p.name.text ++ outParamSuffix) })
+  { name := mkId name
+    inputs := inputs ++ renamedOutputs
+    outputs := [⟨mkId "$result", { val := .TBool, source := none }⟩]
+    preconditions := []
+    decreases := none
+    isFunctional := true
+    body := .Transparent (renameOutputsInPostExpr outputNames condition.condition) }
+
+/-- Information about a procedure's contracts. -/
+private structure ContractInfo where
+  preNames : List (String × Option String)  -- (procName, summary) for each precondition
+  postNames : List (String × Option String) -- (procName, summary) for each postcondition
+  inputParams : List Parameter
+  outputParams : List Parameter
+
+private def ContractInfo.hasPreCondition (info : ContractInfo) : Bool := !info.preNames.isEmpty
+private def ContractInfo.hasPostCondition (info : ContractInfo) : Bool := !info.postNames.isEmpty
+
+/-- Collect contract info for all procedures with contracts. -/
+private def collectContractInfo (procs : List Procedure) : Std.HashMap String ContractInfo :=
+  procs.foldl (fun m proc =>
+    let postconds := getPostconditions proc.body
+    let hasPre := !proc.preconditions.isEmpty
+    let hasPost := !postconds.isEmpty
+    if !proc.isFunctional && (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) =>
+        (postCondProcName proc.name.text i, c.summary)
+      m.insert proc.name.text {
+        preNames := preNames
+        postNames := postNames
+        inputParams := proc.inputs
+        outputParams := proc.outputs
+      }
+    else m) {}
+
+/-- Transform a procedure body to add assume/assert for its own contracts. -/
+private def transformProcBody (proc : Procedure) (info : ContractInfo) : Body :=
+  let inputArgs := paramsToArgs proc.inputs
+  let postconds := getPostconditions proc.body
+  let preAssumes : List StmtExprMd :=
+    proc.preconditions.zip info.preNames |>.map fun (pc, name, _) =>
+      ⟨.Assume (mkCall name inputArgs), 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 _ none mods =>
+    .Opaque postconds none mods
+  | .Abstract _ =>
+    .Abstract postconds
+  | b => b
+
+/-- Monad used by the contract-pass rewriter; carries a global counter for
+    generating fresh temporary variable names. -/
+private abbrev ContractM := StateM Nat
+
+/-- Allocate a fresh temporary name with the `$cp_` prefix.  The global counter
+    guarantees uniqueness across the entire pass. -/
+private def freshTemp : ContractM String := do
+  let n ← get
+  set (n + 1)
+  return s!"$cp_{n}"
+
+/-- Generate temporary variable assignments for input arguments at a call site.
+    Returns (temp declarations+assignments, temp variable references). -/
+private def mkTempAssignments (args : List StmtExprMd)
+    (inputParams : List Parameter) (src : Option FileRange)
+    : ContractM (List StmtExprMd × List StmtExprMd) := do
+  let mut decls : List StmtExprMd := []
+  let mut refs : List StmtExprMd := []
+  for arg in args, i in List.range args.length do
+    let tempName ← freshTemp
+    let paramType := match inputParams[i]? with
+      | some p => p.type
+      | none => { val := .Unknown, source := none }
+    let param : Parameter := { name := mkId tempName, type := paramType }
+    decls := decls ++ [⟨StmtExpr.Assign [mkVarMd (.Declare param)] arg, src⟩]
+    refs := refs ++ [mkMd (.Var (.Local (mkId tempName)))]
+  return (decls, refs)
+
+/-- Generate precondition checks (one per precondition) for a call site. -/
+private def mkPreChecks (info : ContractInfo) (isFunctional : Bool)
+    (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⟩
+
+/-- Generate postcondition assumes (one per postcondition) for a call site. -/
+private def mkPostAssumes (info : ContractInfo)
+    (tempRefs : List StmtExprMd) (outputArgs : List StmtExprMd) (src : Option FileRange) : List StmtExprMd :=
+  if !info.hasPostCondition then []
+  else info.postNames.map fun (name, _) =>
+    ⟨.Assume (mkCall name (tempRefs ++ outputArgs)), src⟩
+
+/-- Names of the callee's inout parameters: those appearing in both the input and
+    output lists. By the Laurel inout convention an inout is declared by giving the
+    input and output the same name, so at a call site the inout argument is the same
+    variable as the corresponding output target — and the Core lowering relies on
+    that identity. -/
+private def ContractInfo.inoutNames (info : ContractInfo) : List String :=
+  info.inputParams.filterMap fun p =>
+    if info.outputParams.any (·.name.text == p.name.text) then some p.name.text else none
+
+/-- Build the positional argument list for the rewritten call.
+
+    Ordinary inputs are passed via their snapshot temp (so pre/postconditions can
+    reference the pre-call value). Inout inputs, however, are passed as the
+    *original* argument variable rather than the temp: the call mutates that
+    variable in place, so it must coincide with the corresponding output target
+    (the Laurel inout invariant). The temp is still created and used by
+    `mkPostAssumes` to supply the inout's pre-state to `$post*`. -/
+private def mkCallArgs (info : ContractInfo) (origArgs tempRefs : List StmtExprMd) : List StmtExprMd :=
+  let inout := info.inoutNames
+  tempRefs.zipIdx.map fun (tempRef, i) =>
+    match info.inputParams[i]? with
+    | some p => if inout.contains p.name.text then origArgs[i]?.getD tempRef else tempRef
+    | none => tempRef
+
+/-- Rewrite call sites in a statement/expression tree. -/
+private def rewriteCallSites (contractInfoMap : Std.HashMap String ContractInfo)
+    (isFunctional : Bool) (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 (callStmt, postAssume, returnValue) ←
+      if info.hasPostCondition && !info.outputParams.isEmpty then do
+        let mut outputTempDecls : List VariableMd := []
+        let mut outputRefs : List StmtExprMd := []
+        for p in info.outputParams do
+          let tempName ← freshTemp
+          outputTempDecls := outputTempDecls ++ [mkVarMd (.Declare { name := mkId tempName, type := p.type })]
+          outputRefs := outputRefs ++ [mkMd (.Var (.Local (mkId tempName)))]
+        let callWithOutputs : StmtExprMd :=
+          ⟨.Assign outputTempDecls ⟨.StaticCall callee tempRefs, src⟩, src⟩
+        let assume := mkPostAssumes info tempRefs outputRefs src
+        let retVal : List StmtExprMd := match outputRefs with
+          | [single] => [single]
+          | _ => []
+        pure (callWithOutputs, assume, retVal)
+      else
+        pure (⟨.StaticCall callee tempRefs, src⟩, [], [])
+    return tempDecls ++ preCheck ++ [callStmt] ++ postAssume ++ returnValue
+  let result ←
+    mapStmtExprFlattenM (m := ContractM)
+      -- Pre: intercept Assign targets (StaticCall ...) before recursion
+      (fun _ e => do
+        match e.val with
+        | .Assign targets (.mk (.StaticCall callee args) callSrc) =>
+          match contractInfoMap.get? callee.text with
+          | some info =>
+            let src := e.source
+            -- Recurse into arguments
+            let args' ← args.mapM (mapStmtExprM (m := ContractM) (fun e' => do
+              match e'.val with
+              | .StaticCall callee' args' =>
+                match contractInfoMap.get? callee'.text with
+                | some info' =>
+                  let stmts ← rewriteStaticCall callee' args' info' e'.source
+                  return ⟨.Block stmts none, e'.source⟩
+                | none => return e'
+              | _ => return e'))
+            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 outputArgs := targets.filterMap fun t =>
+              match t.val with
+              | .Local name => some (mkMd (.Var (.Local name)))
+              | .Declare param => some (mkMd (.Var (.Local param.name)))
+              | _ => none
+            let postAssume := mkPostAssumes info tempRefs outputArgs src
+            return some (tempDecls ++ preCheck ++ [callWithTemps] ++ postAssume)
+          | none => return none
+        | _ => return none)
+      -- Post: handle bare StaticCall
+      (fun _ e => do
+        match e.val with
+        | .StaticCall callee args =>
+          match contractInfoMap.get? callee.text with
+          | some info =>
+            let stmts ← rewriteStaticCall callee args info e.source
+            return stmts
+          | none => return [e]
+        | _ => return [e]) true expr
+  return result
+
+/-- 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
+  match proc.body with
+  | .Transparent body =>
+    let body' ← rw body
+    return { proc with body := .Transparent body' }
+  | .Opaque posts impl mods =>
+    let posts' ← posts.mapM (·.mapM rw)
+    let impl' ← impl.mapM rw
+    let mods' ← mods.mapM rw
+    return { proc with body := Body.Opaque posts' impl' mods' }
+  | _ => return proc
+
+/-- Conjoin a list of conditions into a single expression with `&&`. -/
+private def conjoin (conds : List Condition) : Option StmtExprMd :=
+  match conds.map (·.condition) with
+  | [] => none
+  | e :: rest => some (rest.foldl (fun acc x => mkMd (.PrimitiveOp .And [acc, x])) e)
+
+/-- Build an axiom expression from `invokeOn` trigger and ensures clauses.
+    Produces `∀ p1, ∀ p2, ..., ∀ pn :: { trigger } (preconds => ensures)`.
+    The trigger controls when the SMT solver instantiates the axiom. -/
+private def mkInvokeOnAxiom (params : List Parameter) (trigger : StmtExprMd)
+    (preconds : List Condition) (postconds : List Condition) : StmtExprMd :=
+  let ensures := (conjoin postconds).getD (mkMd (.LiteralBool true))
+  let body := match conjoin preconds with
+    | some pre => mkMd (.PrimitiveOp .Implies [pre, ensures])
+    | none => ensures
+  -- Wrap in nested Forall from last param (innermost) to first (outermost).
+  -- The trigger is placed on the innermost quantifier.
+  params.foldr (init := (body, true)) (fun p (acc, isInnermost) =>
+    let trig := if isInnermost then some trigger else none
+    (mkMd (.Quantifier .Forall p trig acc), false)) |>.1
+
+/-- Check whether a `StmtExprMd` tree mentions a local variable by name. -/
+private def exprMentions (name : String) (expr : StmtExprMd) : Bool :=
+  match expr with
+  | AstNode.mk val _ =>
+  match val with
+  | .Var (.Local id) => id.text == name
+  | .StaticCall _ args => args.attach.any (fun x => exprMentions name x.val)
+  | .PrimitiveOp _ args _ => args.attach.any (fun x => exprMentions name x.val)
+  | .IfThenElse c t e => exprMentions name c || exprMentions name t ||
+      match e with | some el => exprMentions name el | none => false
+  | .Block stmts _ => stmts.attach.any (fun x => exprMentions name x.val)
+  | .Quantifier _ _ trigger body => exprMentions name body ||
+      match trigger with | some t => exprMentions name t | none => false
+  | .ReferenceEquals l r => exprMentions name l || exprMentions name r
+  | .Assign _ v => exprMentions name v
+  | .Old v => exprMentions name v
+  | .Fresh v => exprMentions name v
+  | .Assume c => exprMentions name c
+  | .Assert c => exprMentions name c.condition
+  | .Return (some v) => exprMentions name v
+  | .InstanceCall t _ args => exprMentions name t || args.attach.any (fun x => exprMentions name x.val)
+  | .AsType t _ => exprMentions name t
+  | .IsType t _ => exprMentions name t
+  | .PureFieldUpdate t _ v => exprMentions name t || exprMentions name v
+  | .ProveBy v p => exprMentions name v || exprMentions name p
+  | .ContractOf _ f => exprMentions name f
+  | .Assigned n => exprMentions name n
+  | _ => false
+  termination_by expr
+  decreasing_by
+    all_goals (try cases x)
+    all_goals (try simp_all)
+    all_goals (try have := Condition.sizeOf_condition_lt ‹_›)
+    all_goals (try term_by_mem)
+    all_goals omega
+
+/-- Emit a diagnostic if an `invokeOn` procedure has postconditions referencing
+    output parameters (which are not quantified in the axiom). -/
+private def invokeOnOutputRefError (proc : Procedure) : Option DiagnosticModel :=
+  if proc.invokeOn.isNone then none else
+    let postconds := getPostconditions proc.body
+    let referenced := proc.outputs.filterMap (fun out =>
+      if postconds.any (fun c => exprMentions out.name.text c.condition)
+      then some out.name.text else none)
+    match referenced with
+    | [] => none
+    | names => some (diagnosticFromSource proc.name.source
+        s!"'invokeOn' procedure '{proc.name.text}' has an ensures referencing its output(s) ({String.intercalate ", " names}); the auto-invocation axiom is quantified over inputs only."
+        DiagnosticType.UserError)
+
+/-- Run the contract pass on a Laurel program.
+    All procedures with contracts are transformed. -/
+def lowerContracts (program : Program) : Program × List DiagnosticModel :=
+  let contractInfoMap := collectContractInfo program.staticProcedures
+
+  -- Check for output-referencing ensures in invokeOn procedures
+  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 postconds := getPostconditions proc.body
+    let preProcs := proc.preconditions.zipIdx.map fun (c, i) =>
+      mkConditionProc (preCondProcName proc.name.text i) proc.inputs c
+    let postProcs := postconds.zipIdx.map fun (c, i) =>
+      mkPostConditionProc (postCondProcName proc.name.text i) proc.inputs proc.outputs c
+    preProcs ++ postProcs
+
+  -- 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
+
+  ({ program with staticProcedures := helperProcs ++ transformedProcs }, diagnostics)
+
+public def contractPass : LoweringPass where
+  name := "ContractPass"
+  documentation := "Lowers pre and postcondition to assertions and assumptions around call-sites and procedure bodies"
+  comesAfter := [⟨ eliminateReturnStatementsPass.meta, "The contract pass wraps the body of procedures to get: `assume preconditions; body; assert postconditions`. Eliminating returns first means that the postcondition assertions are guaranteed to execute."⟩ ]
+  needsResolves := true
+  run := fun p _m _ =>
+    let (p', diags) := lowerContracts p
+    (p', diags, {})
+
+end -- public section
+end Strata.Laurel
diff --git a/Strata/Languages/Laurel/CoreDefinitionsForLaurel.lean b/Strata/Languages/Laurel/CoreDefinitionsForLaurel.lean
index 362d45110d..dfe3e09782 100644
--- a/Strata/Languages/Laurel/CoreDefinitionsForLaurel.lean
+++ b/Strata/Languages/Laurel/CoreDefinitionsForLaurel.lean
@@ -27,16 +27,21 @@ program Laurel;
 
 datatype LaurelResolutionErrorPlaceholder {}
 datatype Float64IsNotSupportedYet {}
+datatype LaurelUnit { MkLaurelUnit() }
 
 // The types for these Map functions are incorrect.
 // We'll fix them when Laurel supports polymorphism
-function select(map: int, key: int) : int
+// And then we can remove the datatype Box as well
+// And remove the hacky filter in HeapParameterization
+datatype Box { MkBox() }
+
+function select(map: int, key: int) : Box
   external;
 
-function update(map: int, key: int, value: int) : int
+function update(map: int, key: int, value: int) : Box
   external;
 
-function const(value: int) : int
+function const(value: int) : Box
   external;
 
 #end
diff --git a/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean b/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean
index 34c526e26d..57007a95a5 100644
--- a/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean
+++ b/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean
@@ -5,7 +5,9 @@
 -/
 
 module
-public import Strata.Languages.Laurel.TransparencyPass
+public import Strata.Languages.Laurel.LaurelAST
+public import Strata.Languages.Laurel.UnorderedCore
+public import Strata.Languages.Laurel.LaurelPass
 import Strata.DL.Lambda.LExpr
 import StrataDDM.Util.Graph.Tarjan
 import Strata.Languages.Laurel.Grammar.AbstractToConcreteTreeTranslator
@@ -27,6 +29,7 @@ declarations before they are emitted as Strata Core declarations.
 namespace Strata.Laurel
 
 open Lambda (LMonoTy LExpr)
+open Std (Format ToFormat)
 
 /-- Collect all `UserDefined` type names referenced in a `HighType`, including nested ones. -/
 def collectTypeRefs : HighTypeMd → List String
@@ -54,7 +57,7 @@ def collectStaticCallNames (expr : StmtExprMd) : List String :=
   match val with
   | .StaticCall callee args =>
       callee.text :: args.flatMap (fun a => collectStaticCallNames a)
-  | .PrimitiveOp _ args => args.flatMap (fun a => collectStaticCallNames a)
+  | .PrimitiveOp _ args _ => args.flatMap (fun a => collectStaticCallNames a)
   | .IfThenElse cond t e =>
       collectStaticCallNames cond ++
       collectStaticCallNames t ++
@@ -113,18 +116,18 @@ Build the procedure call graph, run Tarjan's SCC algorithm, and return each SCC
 as a list of procedures paired with a flag indicating whether the SCC is recursive.
 Results are in reverse topological order: dependencies before dependents.
 
-Procedures with `invokeOn` are placed as early as possible — before
+Procedures with axioms are placed as early as possible — before
 unrelated procedures without them — by stably partitioning them first before building
 the graph. Tarjan then naturally assigns them lower indices, causing them to appear
 earlier in the output.
 -/
 public def computeSccDecls (program : UnorderedCoreWithLaurelTypes) : List (List Procedure × Bool) :=
-  -- Stable partition: procedures with invokeOn come first, preserving relative
+  -- Stable partition: procedures with axioms come first, preserving relative
   -- order within each group. Tarjan then places them earlier in the topological output.
   let allProcs := program.functions ++ program.coreProcedures
-  let (withInvokeOn, withoutInvokeOn) :=
-    allProcs.partition (fun p => p.invokeOn.isSome)
-  let orderedProcs : List Procedure := withInvokeOn ++ withoutInvokeOn
+  let (withAxioms, withoutAxioms) :=
+    allProcs.partition (fun p => !p.axioms.isEmpty)
+  let orderedProcs : List Procedure := withAxioms ++ withoutAxioms
 
   -- Build a call-graph over all procedures.
   -- An edge proc → callee means proc's body/contracts contain a StaticCall to callee.
@@ -142,7 +145,8 @@ public def computeSccDecls (program : UnorderedCoreWithLaurelTypes) : List (List
       | _ => []
     let contractExprs : List StmtExprMd :=
       proc.preconditions.map (·.condition) ++
-      proc.invokeOn.toList
+      proc.invokeOn.toList ++
+      proc.axioms
     (bodyExprs ++ contractExprs).flatMap collectStaticCallNames
 
   -- Build the OutGraph for Tarjan.
@@ -225,7 +229,7 @@ Functions are grouped into SCCs (for mutual recursion). Proofs are emitted
 as individual `procedure` decls. Both participate in the topological ordering
 so that axioms are available to functions that need them.
 -/
-public def orderFunctionsAndProcedures (program : UnorderedCoreWithLaurelTypes) : CoreWithLaurelTypes :=
+def orderFunctionsAndProcedures (program : UnorderedCoreWithLaurelTypes) : CoreWithLaurelTypes :=
   let datatypeDecls := (groupDatatypesByScc' program).map OrderedDecl.datatypes
   let constantDecls := program.constants.map OrderedDecl.constant
   let funcNames : Std.HashSet String :=
@@ -254,4 +258,16 @@ where
       let members := comp.toList.filterMap fun idx => dtsArr[idx]?
       if members.isEmpty then none else some members
 
+public def orderingPass : LaurelPass UnorderedCoreWithLaurelTypes CoreWithLaurelTypes where
+  name := "OrderingPass"
+  comesBefore := []
+  documentation := "Produce a `CoreWithLaurelTypes` from a `UnorderedCoreWithLaurelTypes` by
+computing a combined ordering of functions and proofs using the call graph,
+then collecting datatypes and constants.
+Functions are grouped into SCCs (for mutual recursion). Proofs are emitted
+as individual `procedure` decls. Both participate in the topological ordering
+so that axioms are available to functions that need them."
+  run := fun p _ _ =>
+    (orderFunctionsAndProcedures p, [], {})
+
 end Strata.Laurel
diff --git a/Strata/Languages/Laurel/DesugarShortCircuit.lean b/Strata/Languages/Laurel/DesugarShortCircuit.lean
index acd1c02eb4..b8d65c1e40 100644
--- a/Strata/Languages/Laurel/DesugarShortCircuit.lean
+++ b/Strata/Languages/Laurel/DesugarShortCircuit.lean
@@ -25,11 +25,11 @@ namespace Strata.Laurel
 
 public section
 
-private def bare (v : StmtExpr) : StmtExprMd := ⟨v, none⟩
 
 /-- Local rewrite of a single short-circuit node. Recursion is handled by `mapStmtExpr`. -/
-private def desugarShortCircuitNode (model : SemanticModel) (expr : StmtExprMd) : StmtExprMd :=
+private def desugarShortCircuitNode (imperativeCallees : List String) (expr : StmtExprMd) : StmtExprMd :=
   let source := expr.source
+  let wrap (v : StmtExpr) : StmtExprMd := ⟨v, source⟩
   match expr.val with
   | .PrimitiveOp op args _ =>
     match op, args with
@@ -37,30 +37,31 @@ private def desugarShortCircuitNode (model : SemanticModel) (expr : StmtExprMd)
     -- short-circuits converted to IfThenElse). The check still works because
     -- `containsAssignmentOrImperativeCall` recurses into IfThenElse.
     | .AndThen, [a, b] | .Implies, [a, b] =>
-      if containsAssignmentOrImperativeCall model b then
+      if containsAssignmentOrImperativeCall imperativeCallees b then
         let elseVal := match op with | .AndThen => false | _ => true
-        ⟨.IfThenElse a b (some (bare (.LiteralBool elseVal))), source⟩
+        ⟨.IfThenElse a b (some (wrap (.LiteralBool elseVal))), source⟩
       else expr
     | .OrElse, [a, b] =>
-      if containsAssignmentOrImperativeCall model b then
-        ⟨.IfThenElse a (bare (.LiteralBool true)) (some b), source⟩
+      if containsAssignmentOrImperativeCall imperativeCallees b then
+        ⟨.IfThenElse a (wrap (.LiteralBool true)) (some b), source⟩
       else expr
     | _, _ => expr
   | _ => expr
 
 /-- Desugar short-circuit operators in a program. -/
-def desugarShortCircuit (model : SemanticModel) (program : Program) : Program :=
-  mapProgram (mapStmtExpr (desugarShortCircuitNode model)) program
+def desugarShortCircuit (program : Program) : Program :=
+  let imperativeCallees := (program.staticProcedures.filter (!·.isFunctional)).map (·.name.text)
+  mapProgram (mapStmtExpr (desugarShortCircuitNode imperativeCallees)) program
 
 end -- public section
 
 /-- Pipeline pass: desugar short-circuit operators. -/
-public def desugarShortCircuitPass : LaurelPass where
+public def desugarShortCircuitPass : LoweringPass where
   name := "DesugarShortCircuit"
   documentation := "Rewrites short-circuit boolean operators (`&&` and `||`) into equivalent conditional expressions. This simplifies subsequent passes and the final translation to Core, which does not have short-circuit semantics built in."
-  run := fun p m =>
-    (desugarShortCircuit m p, [], {})
+  run := fun p _ _ =>
+    (desugarShortCircuit p, [], {})
   comesBefore := [
-      ⟨ liftExpressionAssignmentsPass, "The desugar short circuit pass introduces if-then-else expressions whose control-flow must be taken into account by the lifting pass."⟩]
+      ⟨ liftImperativeExpressionsPass.meta, "The desugar short circuit pass introduces if-then-else expressions whose control-flow must be taken into account by the lifting pass."⟩]
 
 end Strata.Laurel
diff --git a/Strata/Languages/Laurel/EliminateDeterministicHoles.lean b/Strata/Languages/Laurel/EliminateDeterministicHoles.lean
index c1784d41fc..d7286e86c7 100644
--- a/Strata/Languages/Laurel/EliminateDeterministicHoles.lean
+++ b/Strata/Languages/Laurel/EliminateDeterministicHoles.lean
@@ -90,10 +90,10 @@ def eliminateDeterministicHoles (program : Program) : Program × Statistics :=
 end -- public section
 
 /-- Pipeline pass: eliminate deterministic holes. -/
-public def eliminateDeterministicHolesPass : LaurelPass where
+public def eliminateDeterministicHolesPass : LoweringPass where
   name := "EliminateDeterministicHoles"
   documentation := "Replaces every deterministic hole with a call to a freshly generated uninterpreted function. After this pass the program contains only non-deterministic holes. Assumes `InferHoleTypes` has already annotated holes with types."
-  run := fun p _m =>
+  run := fun p _m _ =>
     let (p', stats) := eliminateDeterministicHoles p
     (p', [], stats)
 
diff --git a/Strata/Languages/Laurel/EliminateDoWhile.lean b/Strata/Languages/Laurel/EliminateDoWhile.lean
index 0c3539eff4..345b1ad694 100644
--- a/Strata/Languages/Laurel/EliminateDoWhile.lean
+++ b/Strata/Languages/Laurel/EliminateDoWhile.lean
@@ -73,10 +73,10 @@ def eliminateDoWhile (program : Program) : Program :=
   (mapProgramProceduresM rewrite program |>.run {}).fst
 
 /-- Pipeline pass: eliminate post-test (`do … while`) loops. -/
-public def eliminateDoWhilePass : LaurelPass where
+public def eliminateDoWhilePass : LoweringPass where
   name := "EliminateDoWhile"
   documentation := "Lowers post-test `While` loops (the `do … while` form) into the pre-test loop `{ while(true) invariant I { BODY; if (!COND) exit L } } L`, with a fresh `$`-prefixed exit label `L`. Runs early so no later pass observes a post-test loop; the invariant is checked at the loop head, matching `while`."
-  run := fun p _m => (eliminateDoWhile p, [], {})
+  run := fun p _m _ => (eliminateDoWhile p, [], {})
 
 end -- public section
 end Strata.Laurel
diff --git a/Strata/Languages/Laurel/EliminateIncrDecr.lean b/Strata/Languages/Laurel/EliminateIncrDecr.lean
index 85be3c24ed..7f1c06a2a5 100644
--- a/Strata/Languages/Laurel/EliminateIncrDecr.lean
+++ b/Strata/Languages/Laurel/EliminateIncrDecr.lean
@@ -100,10 +100,10 @@ def eliminateIncrDecr (program : Program) : Program :=
   mapProgramProcedures lowerProcedure program
 
 /-- Pipeline pass: eliminate increment/decrement operators. -/
-public def eliminateIncrDecrPass : LaurelPass where
+public def eliminateIncrDecrPass : LoweringPass where
   name := "EliminateIncrDecr"
   documentation := "Lowers Java-style increment/decrement operators (`++x`, `x++`, `--x`, `x--`) into existing Laurel assignment and arithmetic constructs. Prefix forms yield the new value; postfix forms yield the old value. Runs early so that no later pass observes an `.IncrDecr` node."
-  run := fun p _m => (eliminateIncrDecr p, [], {})
+  run := fun p _m _ => (eliminateIncrDecr p, [], {})
 
 end -- public section
 end Strata.Laurel
diff --git a/Strata/Languages/Laurel/EliminateReturnStatements.lean b/Strata/Languages/Laurel/EliminateReturnStatements.lean
new file mode 100644
index 0000000000..d2a7743765
--- /dev/null
+++ b/Strata/Languages/Laurel/EliminateReturnStatements.lean
@@ -0,0 +1,83 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+public import Strata.Languages.Laurel.MapStmtExpr
+public import Strata.Languages.Laurel.LaurelPass
+
+/-!
+# Eliminate Return Statements
+
+Replaces `return` statements in imperative procedure bodies with assignments
+to the output parameters followed by an `exit` to a labelled block that wraps
+the entire body. This ensures that code placed after the body block (e.g.,
+postcondition assertions inserted by the contract pass) is always reached.
+
+This pass should run after `EliminateReturnsInExpression` (which handles
+functional/expression-position returns) and before the contract pass.
+-/
+
+namespace Strata.Laurel
+
+public section
+
+private def returnLabel : String := "$return"
+
+
+
+
+/-- Transform a single procedure: wrap body in a labelled block and replace returns. -/
+private def eliminateReturnStmts (proc : Procedure) : Procedure :=
+  match proc.body with
+  | .Opaque postconds (some impl) mods =>
+    let impl' := replaceReturn proc.outputs impl
+    let wrapped := match impl'.val with
+      | .Block stmts none => ⟨.Block stmts (some returnLabel), impl'.source⟩
+      | _ => ⟨ .Block [impl'] (some returnLabel), proc.name.source ⟩
+    { proc with body := .Opaque postconds (some wrapped) mods }
+  | .Transparent body =>
+    let body' := replaceReturn proc.outputs body
+    let wrapped := match body'.val with
+      | .Block stmts none => ⟨.Block stmts (some returnLabel), body'.source⟩
+      | _ => ⟨ .Block [body'] (some returnLabel), proc.name.source ⟩
+    { proc with body := .Transparent wrapped }
+  | _ => proc
+where
+
+  /-- Replace `Return val` with `output := val; exit "$return"` (or just `exit`
+    for valueless returns). Uses `mapStmtExpr` for bottom-up traversal. -/
+  replaceReturn (outputs : List Parameter) (expr : StmtExprMd) : StmtExprMd :=
+    mapStmtExpr (fun e =>
+      match e.val with
+      | .Return (some val) =>
+        /- Handling valued return is required because the heap param pass introduces valued return in
+        Strata/Languages/Laurel/HeapParameterizationConstants.lean
+        We should change that so we can remove this case.
+        -/
+        match outputs with
+        | [out] =>
+          let assign := ⟨ .Assign [⟨ .Local out.name, expr.source ⟩] val, expr.source ⟩
+          let exit := ⟨ .Exit returnLabel, expr.source ⟩
+          ⟨.Block [assign, exit] none, e.source⟩
+        | _ => ⟨ .Exit returnLabel, expr.source ⟩
+      | .Return none => ⟨ .Exit returnLabel, expr.source ⟩
+      | _ => e) expr
+
+/-- Transform a program by eliminating return statements in all procedure bodies. -/
+def eliminateReturnStatements (program : Program) : Program :=
+  { program with staticProcedures := program.staticProcedures.map eliminateReturnStmts }
+
+public def eliminateReturnStatementsPass : LoweringPass where
+  name := "EliminateReturnStatements"
+  documentation := "Lower return statements to exit statements. Wrap each procedure body with a 'return' block"
+  run := fun p _m _ =>
+    let p' := eliminateReturnStatements p
+    (p', [], {})
+  -- comesBefore := [contractPass]
+
+end -- public section
+
+end Strata.Laurel
diff --git a/Strata/Languages/Laurel/EliminateValueInReturns.lean b/Strata/Languages/Laurel/EliminateValueInReturns.lean
index 38ea5f4b99..d209465bf6 100644
--- a/Strata/Languages/Laurel/EliminateValueInReturns.lean
+++ b/Strata/Languages/Laurel/EliminateValueInReturns.lean
@@ -8,16 +8,13 @@ module
 public import Strata.Languages.Laurel.LaurelAST
 public import Strata.Languages.Laurel.LaurelPass
 import Strata.Languages.Laurel.MapStmtExpr
-import Strata.Languages.Laurel.HeapParameterization
 import Strata.Util.Tactics
 
 /-!
-# Eliminate Value Returns
+# Eliminate Values In Returns
 
 Rewrites `return expr` into `outParam := expr; return` for imperative
-(non-functional) procedures that have an output parameter. This decouples
-the return-value assignment from the `LaurelToCoreTranslator`, which no
-longer needs to know about output parameters when translating returns.
+(non-functional) procedures that have an output parameter.
 
 The pass is a Laurel-to-Laurel rewrite that runs before Core translation.
 It only applies to static procedures, hence LiftInstanceProcedures must
@@ -26,18 +23,19 @@ be executed before it.
 
 namespace Strata.Laurel
 
-/-- Rewrite a single `Return (some value)` node into
-    `Block [Assign [Identifier outParam] value, Return none]`.
-    Recursion into children is handled by `mapStmtExpr`. -/
-private def eliminateValueReturnNode (outParam : Identifier) (stmt : StmtExprMd) : StmtExprMd :=
+/-- Rewrite a single `Return (some value)` node into the list
+    `[Assign outParam value, Return none]`.
+    When used with `mapStmtExprFlattenM`, these statements are flattened
+    into the enclosing block rather than wrapped in a nested block. -/
+private def eliminateValueReturnNode (outParam : Identifier) (stmt : StmtExprMd) : Id (List StmtExprMd) :=
   match stmt.val with
   | .Return (some value) =>
     -- Synthesized nodes use default metadata since no diagnostics should be reported on them
-    let target : VariableMd := { val := .Local outParam, source := none }
-    let assign : StmtExprMd := { val := .Assign [target] value, source := none }
+    let target : VariableMd := { val := .Local outParam, source := stmt.source }
+    let assign : StmtExprMd := { val := .Assign [target] value, source := stmt.source }
     let ret : StmtExprMd := { val := .Return none, source := stmt.source }
-    { val := .Block [assign, ret] none, source := none }
-  | _ => stmt
+    [assign, ret]
+  | _ => [stmt]
 
 /-- Check whether a statement tree contains any `Return (some _)`. -/
 def hasValuedReturn (stmt : StmtExprMd) : Bool :=
@@ -56,14 +54,23 @@ def hasValuedReturn (stmt : StmtExprMd) : Bool :=
     all_goals (try term_by_mem)
     all_goals omega
 
-/-- Apply value-return elimination to a single procedure. Only applies to
-    non-functional procedures with exactly one output parameter.
-    Emits an error if a valued return is used with multiple output parameters. -/
+/-- 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).
+    Emits an error if a valued return is used with zero or multiple output parameters. -/
 def eliminateValueReturnsInProc (proc : Procedure) : Procedure :=
-  if proc.isFunctional then proc
-  else match proc.outputs with
+  match proc.outputs with
   | [outParam] =>
-    let rewrite := mapStmtExpr (eliminateValueReturnNode outParam.name)
+    let pre (_: Bool) (stmt : StmtExprMd) : Id (Option (List StmtExprMd)) :=
+      match stmt.val with
+      | .Return (some value) =>
+        let target : VariableMd := { val := .Local outParam.name, source := stmt.source }
+        let assign : StmtExprMd := { val := .Assign [target] value, source := stmt.source }
+        let ret : StmtExprMd := { val := .Return none, source := stmt.source }
+        some [assign, ret]
+      | _ => none
+    let post (_: Bool) (stmt : StmtExprMd) : Id (List StmtExprMd) := pure [stmt]
+    let rewrite := mapStmtExprFlattenM (m := Id) pre post true
     match proc.body with
     | .Transparent body =>
       { proc with body := .Transparent (rewrite body) }
@@ -85,10 +92,9 @@ def eliminateValueInReturnsTransform (program : Program) : Program  :=
 end -- public section
 
 /-- Pipeline pass: eliminate value returns. -/
-public def eliminateValueInReturnsPass : LaurelPass where
+public def eliminateValueInReturnsPass : LoweringPass where
   name := "EliminateValueInReturns"
   documentation := "Rewrites `return expr` into `outParam := expr; return` for imperative procedures that have an output parameter. This decouples the return-value assignment from the final Core translation, which no longer needs to know about output parameters when translating returns."
-  run := fun p _m => (eliminateValueInReturnsTransform p, [], {})
-  comesBefore := [⟨ heapParameterizationPass, "eliminate value in returns need to come before any passes that change the amount of output parameters of procedures." ⟩]
+  run := fun p _m _ => (eliminateValueInReturnsTransform p, [], {})
 
 end Laurel
diff --git a/Strata/Languages/Laurel/FilterPrelude.lean b/Strata/Languages/Laurel/FilterPrelude.lean
index 2e6a45ba48..52fd25fcbc 100644
--- a/Strata/Languages/Laurel/FilterPrelude.lean
+++ b/Strata/Languages/Laurel/FilterPrelude.lean
@@ -221,8 +221,6 @@ private def buildDependencyMap (prog : Laurel.Program)
         for c in dt.constructors do
           insertNew c.name.text (deps.insert name)
             s!"constructor '{c.name.text}' of datatype '{name}'"
-          insertNew (dt.testerName c) (deps.insert name)
-            s!"tester '{dt.testerName c}' of datatype '{name}'"
           for a in c.args do
             insertNew (dt.destructorName a) (deps.insert name)
               s!"destructor '{dt.destructorName a}'"
diff --git a/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean
index 5ae406e820..145c39694f 100644
--- a/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean
+++ b/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean
@@ -256,7 +256,14 @@ private def procedureToOp (proc : Procedure) : StrataDDM.Operation :=
     laurelOp "invokeOnClause" #[stmtExprToArg e])
   let (opaqueSpecArg, bodyArg) := match proc.body with
     | .Transparent body =>
-      (optionArg none, optionArg (some (laurelOp "body" #[stmtExprToArg 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])))
     | .Opaque postconds impl modifies =>
       let ens := postconds.map ensuresClauseToArg |>.toArray
       let mods := if modifies.isEmpty then #[] else modifiesClausesToArgs modifies
diff --git a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
index 349775d760..bf5e10dd12 100644
--- a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
+++ b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
@@ -568,6 +568,11 @@ 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
diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
index 3eadd5dd90..dc54d7617a 100644
--- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
+++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
@@ -9,7 +9,6 @@ module
 -- NOTE: Changes to LaurelGrammar.st are not automatically tracked by the build system.
 -- Update this file (e.g. this comment) to trigger a recompile after modifying LaurelGrammar.st.
 -- Last grammar change: fieldAccess prec raised 90 -> 95 (paren-free `c#n++`); shares prec(95) with `call`.
-
 public import StrataDDM.AST
 import StrataDDM.BuiltinDialects.Init
 import StrataDDM.Integration.Lean.HashCommands
diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
index 40af1e116c..53f0c33f99 100644
--- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
+++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
@@ -115,10 +115,10 @@ op errorSummary(msg: Str): ErrorSummary => " summary " msg;
 
 // If-else
 category ElseBranch;
-op elseBranch(stmts : StmtExpr) : ElseBranch => @[prec(0)] " else " stmts;
+op elseBranch(stmts : StmtExpr) : ElseBranch => @[prec(0)] "\nelse " stmts;
 
 op ifThenElse (cond: StmtExpr, thenBranch: StmtExpr, elseBranch: Option ElseBranch): StmtExpr =>
-  @[prec(20)] "if " cond " then " thenBranch:0 elseBranch:0;
+  @[prec(20)] "if " cond "\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;
diff --git a/Strata/Languages/Laurel/HeapParameterization.lean b/Strata/Languages/Laurel/HeapParameterization.lean
index 06c1e6d04a..4fb4ff74a4 100644
--- a/Strata/Languages/Laurel/HeapParameterization.lean
+++ b/Strata/Languages/Laurel/HeapParameterization.lean
@@ -12,9 +12,8 @@ import Strata.Languages.Laurel.Grammar.AbstractToConcreteTreeTranslator
 import Strata.Languages.Laurel.HeapParameterizationConstants
 import Strata.Languages.Laurel.LaurelTypes
 import Strata.Util.Tactics
-import Strata.Languages.Laurel.TypeHierarchy
-import Strata.Languages.Laurel.ModifiesClauses
 import Strata.Languages.Laurel.LiftImperativeExpressions
+import Strata.Languages.Laurel.EliminateValueInReturns
 
 /-
 Heap Parameterization Pass
@@ -248,7 +247,7 @@ def readsHeap (name : Identifier) : TransformM Bool := do
 def writesHeap (name : Identifier) : TransformM Bool := do
   return (← get).heapWriters.contains name
 
-def freshVarName : TransformM Identifier := do
+private def freshVarName : TransformM Identifier := do
   let s ← get
   set { s with freshCounter := s.freshCounter + 1 }
   return s!"$tmp{s.freshCounter}"
@@ -571,21 +570,25 @@ def heapParameterization (model: SemanticModel) (program : Program) : Program :=
   -- Generate Box datatype from all constructors used during transformation
   let boxDatatype : TypeDefinition :=
     .Datatype { name := "Box", typeArgs := [], constructors := state1.usedBoxConstructors }
+
+  let types := fieldDatatype :: boxDatatype :: heapConstants.types ++
+    -- The filter is a hack to deal with another hack,
+    -- the box that was added in CoreDefinitionsForLaurel.lean
+    -- because Laurel does not support polymorphism yet
+    types'.filter (fun td => td.name.text != "Box")
   { program with
     staticProcedures := heapConstants.staticProcedures ++ procs',
-    types := fieldDatatype :: boxDatatype :: heapConstants.types ++ types' }
+    types }
 
 /-- Pipeline pass: heap parameterization. -/
-public def heapParameterizationPass : LaurelPass where
+public def heapParameterizationPass : LoweringPass where
   name := "HeapParameterization"
   documentation := "Transforms procedures that interact with the heap by adding explicit heap parameters. The heap is modeled as `Map Composite (Map Field Box)`. Procedures that write the heap receive both an input and output heap parameter; procedures that only read the heap receive an input heap parameter. Field reads and writes are rewritten to use `readField` and `updateField` functions."
   needsResolves := false -- Only resolve again after completing HeapParam, ModifiesClauses and TypeHierarchy. These are logically one pass.
-  run := fun p m =>
+  run := fun p m _ =>
     (heapParameterization m p, [], {})
-  comesBefore := [
-      ⟨ typeHierarchyTransformPass, "the type hierarchy pass modifies the 'Composite' datatype that is introduced by this pass." ⟩,
-      ⟨ modifiesClausesTransformPass, "the modifies pass refers to several types and variables introduced by heap parameterization: Composite, Field, $heap_in, $heap." ⟩,
-      ⟨ liftExpressionAssignmentsPass, "the heap parameterization pass introduces assignments (to the heap variables) that need to be lifted."⟩]
+  comesAfter := [⟨ eliminateValueInReturnsPass.meta, "eliminate value in returns need to come before any passes that change the amount of output parameters of procedures." ⟩]
+  comesBefore := [⟨ liftImperativeExpressionsPass.meta, "the heap parameterization pass introduces assignments (to the heap variables) that need to be lifted."⟩]
 
 end Strata.Laurel
 
diff --git a/Strata/Languages/Laurel/HeapParameterizationConstants.lean b/Strata/Languages/Laurel/HeapParameterizationConstants.lean
index 7258f29d6a..a9c6e80206 100644
--- a/Strata/Languages/Laurel/HeapParameterizationConstants.lean
+++ b/Strata/Languages/Laurel/HeapParameterizationConstants.lean
@@ -18,9 +18,6 @@ public section
 /-- The name of the heap variable used by the heap parameterization pass. -/
 def heapVarName : Identifier := "$heap"
 
-/-- The name of the input heap parameter used by the heap parameterization pass. -/
-def heapInVarName : Identifier := "$heap_in"
-
 /--
 The Laurel Core prelude defines the heap model types and operations
 used by the Laurel-to-Core translator. These declarations are expressed
diff --git a/Strata/Languages/Laurel/InferHoleTypes.lean b/Strata/Languages/Laurel/InferHoleTypes.lean
index 46ecf93701..994627c3e1 100644
--- a/Strata/Languages/Laurel/InferHoleTypes.lean
+++ b/Strata/Languages/Laurel/InferHoleTypes.lean
@@ -192,13 +192,13 @@ def inferHoleTypes (model : SemanticModel) (program : Program) : Program × List
 end -- public section
 
 /-- Pipeline pass: infer hole types. -/
-public def inferHoleTypesPass : LaurelPass where
+public def inferHoleTypesPass : LoweringPass where
   name := "InferHoleTypes"
   documentation := "Annotates every verification hole (`.Hole`) in the program with a type inferred from context. This type information is needed by subsequent passes that replace holes with uninterpreted functions or nondeterministic values."
-  run := fun p m =>
+  run := fun p m _ =>
     let (p', diags, stats) := inferHoleTypes m p
     (p', diags, stats)
   comesBefore := [
-      ⟨ eliminateDeterministicHolesPass, "eliminating deterministic holes relies on knowing the type of holes"⟩]
+      ⟨ eliminateDeterministicHolesPass.meta, "eliminating deterministic holes relies on knowing the type of holes"⟩]
 
 end Laurel
diff --git a/Strata/Languages/Laurel/LaurelAST.lean b/Strata/Languages/Laurel/LaurelAST.lean
index d7ba9cd8ca..fb02d7cd59 100644
--- a/Strata/Languages/Laurel/LaurelAST.lean
+++ b/Strata/Languages/Laurel/LaurelAST.lean
@@ -229,6 +229,9 @@ structure Procedure : Type where
       whose body is the ensures clause universally quantified over the procedure's inputs,
       with this expression as the SMT trigger. -/
   invokeOn : Option (AstNode StmtExpr) := none
+  /-- Axioms to emit alongside this procedure. Populated by the contract pass from
+      `invokeOn` and ensures clauses. -/
+  axioms : List (AstNode StmtExpr) := []
 
 /--
 A typed parameter for a procedure.
@@ -837,6 +840,9 @@ structure ConstrainedType where
 structure DatatypeConstructor where
   name : Identifier
   args : List Parameter
+  /-- Identifier for the auto-generated tester function (e.g. `IntList..isNil`).
+      Populated with a `uniqueId` during resolution. -/
+  testerName : Identifier := mkId ""
 
 /-- A Laurel datatype definition with optional type parameters.
     Zero constructors produces an opaque (abstract) type in Core.
diff --git a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
index d0cfe695fc..298b93f1b6 100644
--- a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
+++ b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
@@ -5,8 +5,9 @@
 -/
 module
 
-public import Strata.Languages.Laurel.LaurelToCoreTranslator
+public import Strata.Languages.Laurel.LaurelToCoreSchemaPass
 import Strata.Languages.Laurel.DesugarShortCircuit
+import Strata.Languages.Laurel.EliminateReturnStatements
 import Strata.Languages.Laurel.EliminateDoWhile
 import Strata.Languages.Laurel.EliminateIncrDecr
 import Strata.Languages.Laurel.MergeAndLiftReturns
@@ -17,8 +18,11 @@ import Strata.Languages.Laurel.TypeHierarchy
 import Strata.Languages.Laurel.InferHoleTypes
 import Strata.Languages.Laurel.EliminateDeterministicHoles
 import Strata.Languages.Laurel.CoreDefinitionsForLaurel
+import Strata.Languages.Laurel.CoreGroupingAndOrdering
+import Strata.Languages.Laurel.TransparencyPass
 import Strata.Languages.Laurel.LiftImperativeExpressions
 import Strata.Languages.Laurel.ConstrainedTypeElim
+import Strata.Languages.Laurel.ContractPass
 import Strata.Languages.Laurel.PushOldInward
 import Strata.Languages.Laurel.LiftInstanceProcedures
 import Strata.Languages.Laurel.TypeAliasElim
@@ -38,7 +42,7 @@ to Strata Core. The pipeline is:
 1. Prepend core definitions for Laurel.
 2. Run a sequence of Laurel-to-Laurel lowering passes (resolution, heap
    parameterization, type hierarchy, modifies clauses, hole inference,
-   desugaring, lifting, constrained type elimination).
+   desugaring, lifting, constrained type elimination, contract pass).
 3. Run the transparency pass to produce an `UnorderedCoreWithLaurelTypes`.
 4. Group and order declarations into a `CoreWithLaurelTypes`.
 5. Translate the `CoreWithLaurelTypes` to a `Core.Program`.
@@ -93,45 +97,26 @@ public section
 abbrev TranslateResultWithLaurel := (Option Core.Program) × (List DiagnosticModel) × Program × Statistics
 
 /-- The ordered sequence of Laurel-to-Laurel lowering passes. -/
-def laurelPipeline : Array LaurelPass := #[
+def laurelPipeline : Array LoweringPass := #[
   eliminateDoWhilePass,
   eliminateIncrDecrPass,
   typeAliasElimPass,
   constrainedTypeElimPass,
   filterNonCompositeModifiesPass,
+  mergeAndLiftReturnsPass,
   liftInstanceProceduresPass,
   eliminateValueInReturnsPass,
   heapParameterizationPass,
   typeHierarchyTransformPass,
   modifiesClausesTransformPass,
-  { name := "PushOldInward"
-    documentation := "Distributes `old(...)` over its subexpressions until each `old` immediately wraps an inout variable. Warns on `old(e)` where `e` mentions no inout parameter and on nested `old(old(...))`."
-    run := fun p _m =>
-      let (p', diags) := pushOldInward p
-      (p', diags, {}) },
+  pushOldInwardPass,
   inferHoleTypesPass,
   eliminateDeterministicHolesPass,
   desugarShortCircuitPass,
-  liftExpressionAssignmentsPass,
-  mergeAndLiftReturnsPass
+  eliminateReturnStatementsPass,
+  contractPass
 ]
 
-/-- Every `comesBefore` constraint is respected by the pipeline order.
-    Checked at elaboration time so that mis-ordered passes are caught immediately. -/
-def comesBeforeRespected : Bool :=
-  let names := laurelPipeline.toList.map (·.name)
-  (List.range laurelPipeline.size).zip laurelPipeline.toList |>.all fun (i, p) =>
-    p.comesBefore.all fun cb =>
-      match names.findIdx? (· == cb.pass.name) with
-      | some j => i < j
-      | none   => false   -- target not in laurelPipeline
-
--- Use `initialize` to check at load time instead of `#guard` which requires
--- interpreter IR that is not available for passes defined in `module` files.
-initialize do
-  unless comesBeforeRespected do
-    throw <| .userError "laurelPipeline: comesBefore ordering constraints violated"
-
 /--
 Run all Laurel-to-Laurel lowering passes on a program, returning the lowered
 program, the semantic model, accumulated diagnostics, and merged statistics.
@@ -141,6 +126,7 @@ program state after each named Laurel pass is written to
 `{prefix}.{n}.{passName}.laurel.st`.
 -/
 private def runLaurelPasses
+    (options: LaurelTranslateOptions)
     (pctx : Strata.Pipeline.PipelineContext) (program : Program)
     : PipelineM (Program × SemanticModel × List DiagnosticModel × Statistics) := do
   let program := { program with
@@ -162,7 +148,7 @@ private def runLaurelPasses
   let mut allStats : Statistics := {}
 
   for pass in laurelPipeline do
-    let (program', diags, stats) ← pctx.withPhase pass.name do pure (pass.run program model)
+    let (program', diags, stats) ← pctx.withPhase pass.name do pure (pass.run program model options)
     program := program'
     allDiags := allDiags ++ diags
     allStats := allStats.merge stats
@@ -174,7 +160,7 @@ private def runLaurelPasses
         let newDiags := newErrors.toList.map fun d =>
           { d with
               message :=
-                s!"Internal error: resolution after '{pass.name}' introduced this diagnostic: {d.message}"
+                s!"Internal error: resolution after '{pass.name}' introduced this diagnostic: {d}. Existing diagnostics were: {resolutionErrors.toList}"
               type := .StrataBug }
         emit pass.name "laurel.st" program
         return (program, model, allDiags ++ newDiags, allStats)
@@ -184,6 +170,11 @@ private def runLaurelPasses
 
   return (program, model, allDiags, allStats)
 
+/-- The ordered sequence of passes on the unordered Core representation. -/
+private def unorderedCorePipeline : Array (LaurelPass UnorderedCoreWithLaurelTypes UnorderedCoreWithLaurelTypes) := #[
+  liftImperativeExpressionsPass
+]
+
 /--
 Translate Laurel Program to Core Program, also returning the lowered Laurel program.
 
@@ -197,47 +188,55 @@ def translateWithLaurel (options : LaurelTranslateOptions) (program : Program)
     | some ctx => pure ctx
     | none => Strata.Pipeline.PipelineContext.create (outputMode := .quiet)
   runPipelineM options.keepAllFilesPrefix do
-    let (program, model, passDiags, stats) ← runLaurelPasses pctx program
-    -- Sanity check: `LiftInstanceProcedures` should have cleared every
-    -- composite's `instanceProcedures` list.
-    let mut passDiags := passDiags
-    for td in program.types do
-      if let .Composite ct := td then
-        for proc in ct.instanceProcedures do
-          passDiags := passDiags ++ [diagnosticFromSource proc.name.source
-            s!"Instance procedure '{proc.name.text}' on composite type '{ct.name.text}' was not lifted before Core translation (pipeline-ordering bug)"
-            DiagnosticType.StrataBug]
-    let unorderedCore := transparencyPass program
-    emit "transparencyPass" "core.st" unorderedCore
-
-    -- Resolve so that identifiers introduced by earlier passes get uniqueIds.
-    let compositeTypes := program.types.filter (fun t => match t with | .Composite _ => true | _ => false)
-    let (unorderedCore, model) := resolveUnorderedCore unorderedCore (existingModel := some model) (additionalTypes := compositeTypes)
-
-    let coreWithLaurelTypes := orderFunctionsAndProcedures unorderedCore
-
-    -- This early return is a simple way to protect against duplicative errors. Without this return,
-    -- resolution errors reported by Laurel would also be reported by Core.
-    -- There might be better solution that allows getting some resolution errors from Laurel and some verification errors from Core,
-    -- but that would need more consideration.
-    if passDiags.any (·.type != .Warning) then
-      return (none, passDiags, program, stats)
-
-    emit "CoreWithLaurelTypes" "core.st" coreWithLaurelTypes
-    let initState : TranslateState := { model := model, overflowChecks := options.overflowChecks }
-    let (coreProgramOption, translateState) :=
-      runTranslateM initState (translateLaurelToCore options coreWithLaurelTypes)
-    -- Because of the duplication between functions and procedures, this translation is liable to create duplicate diagnostics
-    let mut allDiagnostics: List DiagnosticModel := passDiags ++ translateState.diagnostics.eraseDups;
-
-    if !translateState.coreDiagnostics.isEmpty && allDiagnostics.isEmpty then
-      allDiagnostics := allDiagnostics ++ translateState.coreDiagnostics
-
-    if coreProgramOption.isSome then
-      emit "Core" "core.st" coreProgramOption.get!
-    let coreProgramOption :=
-      if translateState.coreDiagnostics.isEmpty then coreProgramOption else none
-    return (coreProgramOption, allDiagnostics, program, stats)
+  let (program, model, passDiags, stats) ← runLaurelPasses options pctx program
+
+  -- Sanity check: `LiftInstanceProcedures` should have cleared every
+  -- composite's `instanceProcedures` list.
+  let mut passDiags := passDiags
+  for td in program.types do
+    if let .Composite ct := td then
+      for proc in ct.instanceProcedures do
+        passDiags := passDiags ++ [diagnosticFromSource proc.name.source
+          s!"Instance procedure '{proc.name.text}' on composite type '{ct.name.text}' was not lifted before Core translation (pipeline-ordering bug)"
+          DiagnosticType.StrataBug]
+
+  -- This early return is a simple way to protect against duplicative errors. Without this return,
+  -- resolution errors reported by Laurel would also be reported by Core.
+  -- There might be better solution that allows getting some resolution errors from Laurel and some verification errors from Core,
+  -- but that would need more consideration.
+  if passDiags.any (·.type != .Warning) then
+    return (none, passDiags, program, stats)
+
+  let unorderedCore := (transparencyPass.run program model options).1
+  emit "transparencyPass" "core.st" unorderedCore
+  let mut unorderedCore := unorderedCore
+  let mut fnModel := model
+
+  for pass in unorderedCorePipeline do
+    unorderedCore := (pass.run unorderedCore fnModel options).1
+    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
+      if !errors.isEmpty then
+        let newDiags := errors.toList.map fun d =>
+          { 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)
+      unorderedCore := uc'
+      fnModel := m'
+    emit pass.name "unorderedCoreWithLaurelTypes.st" unorderedCore
+
+  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;
+
+  emit "Core" "core.st" coreProgram
+  let coreProgramOption :=
+    if coreDiagnostics.isEmpty then some coreProgram else none
+  return (coreProgramOption, allDiagnostics, program, stats)
 
 /--
 Translate Laurel Program to Core Program.
@@ -347,4 +346,33 @@ def verifyToDiagnosticModelsCapturing (program : Program)
       return (translateDiags ++ vcDiags).toArray
 
 end -- public section
+
+public def allPasses: Array PassMeta := laurelPipeline.map (fun p => p.meta) ++
+  [transparencyPass.meta] ++
+  unorderedCorePipeline.map (fun p => p.meta) ++
+  [orderingPass.meta, laurelToCoreSchemaPass.meta]
+
+/-- Every `comesBefore` and `comesAfter` constraint is respected by the
+    pipeline order. A `comesBefore` dependency requires this pass to appear
+    earlier than its target; a `comesAfter` dependency requires it to appear
+    later. -/
+def orderingRespected : Bool :=
+  let names := allPasses.map (·.name)
+  (List.range allPasses.size).zip allPasses.toList |>.all fun (i, p) =>
+    (p.comesBefore.all fun cb =>
+      match names.findIdx? (· == cb.pass.name) with
+      | some j => i < j
+      | none   => false)  -- target not in allPasses
+    &&
+    (p.comesAfter.all fun ca =>
+      match names.findIdx? (· == ca.pass.name) with
+      | some j => j < i
+      | none   => false)  -- target not in allPasses
+
+-- Use `initialize` to check at load time instead of `#guard` which requires
+-- interpreter IR that is not available for passes defined in `module` files.
+initialize do
+  unless orderingRespected do
+    throw <| .userError "laurelPipeline: comesBefore/comesAfter ordering constraints violated"
+
 end Laurel
diff --git a/Strata/Languages/Laurel/LaurelPass.lean b/Strata/Languages/Laurel/LaurelPass.lean
index 5a682db402..130ae2cf09 100644
--- a/Strata/Languages/Laurel/LaurelPass.lean
+++ b/Strata/Languages/Laurel/LaurelPass.lean
@@ -7,31 +7,60 @@ module
 
 public import Strata.Languages.Laurel.SemanticModel
 public import Strata.Util.Statistics
+public import Strata.Languages.Core.Options
 
 namespace Strata.Laurel
 
 public section
 
+structure LaurelTranslateOptions where
+  inlineFunctionsWhenPossible : Bool := false
+  overflowChecks : Core.OverflowChecks := {}
+  keepAllFilesPrefix : Option String := none
+
+instance : Inhabited LaurelTranslateOptions where
+  default := {}
+
 mutual
-structure ComesBefore where
-  pass : LaurelPass
-  reason: String
 
-/-- A single Laurel-to-Laurel pass. Each pass receives the current program and
-    semantic model and returns the (possibly modified) program, accumulated
-    diagnostics, and statistics. -/
-structure LaurelPass where
+/-- The parameter-free metadata of a pass, independent of the `Input`/`Output`
+    types it operates on. `LaurelPass` extends this so that passes with
+    different parameterizations (e.g. `LaurelPass Program Program` and
+    `LaurelPass UnorderedCoreWithLaurelTypes UnorderedCoreWithLaurelTypes`)
+    share a common, type-parameter-free view that can be collected into a
+    single homogeneous list. -/
+structure PassMeta where
   /-- Human-readable name, used for profiling and file emission. -/
   name : String
   /-- Whether `resolve` should be run after the pass. -/
   needsResolves : Bool := false
-  /-- The pass action. -/
-  run : Program → SemanticModel → Program × List DiagnosticModel × Statistics
   /-- A description of what this pass does, used for documentation generation. -/
   documentation : String
-  comesBefore : List ComesBefore := []
+  /-- Passes that must run before this one. -/
+  comesBefore : List PassDependency := []
+  /-- Passes that must run after this one. -/
+  comesAfter : List PassDependency := []
+
+structure PassDependency where
+  pass : PassMeta
+  reason: String
 end
 
+/-- A single Laurel-to-Laurel pass. Each pass receives the current program and
+    semantic model and returns the (possibly modified) program, accumulated
+    diagnostics, and statistics. Extends `PassMeta` with the `run` action; the
+    metadata fields remain directly accessible (e.g. `p.name`). -/
+structure LaurelPass (Input: Type) (Output: Type) extends PassMeta where
+  /-- The pass action. -/
+  run : Input → SemanticModel → LaurelTranslateOptions → Output × List DiagnosticModel × Statistics
+
+abbrev LoweringPass := LaurelPass Laurel.Program Laurel.Program
+
+/-- Project a `LaurelPass` to its parameter-free metadata, discarding the
+    `run` action and the `Input`/`Output` type parameters. -/
+abbrev LaurelPass.meta {Input Output : Type} (p : LaurelPass Input Output) : PassMeta :=
+  p.toPassMeta
+
 end -- public section
 
 end Strata.Laurel
diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreSchemaPass.lean
similarity index 93%
rename from Strata/Languages/Laurel/LaurelToCoreTranslator.lean
rename to Strata/Languages/Laurel/LaurelToCoreSchemaPass.lean
index cbc317c6d8..3c6cda03cd 100644
--- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean
+++ b/Strata/Languages/Laurel/LaurelToCoreSchemaPass.lean
@@ -145,10 +145,7 @@ def translateExpr (expr : StmtExprMd)
   let model := s.model
   let md := astNodeToCoreMd expr
   let disallowed (source : Option FileRange) (msg : String) : TranslateM Core.Expression.Expr := do
-    if isPureContext then
       throwExprDiagnostic $ diagnosticFromSource source msg
-    else
-      throwExprDiagnostic $ diagnosticFromSource source s!"{msg} (should have been lifted)" DiagnosticType.StrataBug
 
   match h: expr.val with
   | .LiteralBool b => return .const () (.boolConst b)
@@ -282,9 +279,6 @@ def translateExpr (expr : StmtExprMd)
   | .Block (⟨ .IfThenElse cond thenBranch (some elseBranch), innerSrc⟩ :: rest) label =>
     disallowed innerSrc "if-then-else only supported as the last statement in a block"
 
-  | .IsType _ _ =>
-      throwExprDiagnostic $ diagnosticFromSource expr.source "IsType should have been lowered" DiagnosticType.StrataBug
-  | .New _ => throwExprDiagnostic $ diagnosticFromSource expr.source s!"New should have been eliminated by typeHierarchyTransform" DiagnosticType.StrataBug
   | .Var (.Field target fieldId) =>
       -- Field selects should have been eliminated by heap parameterization
       -- If we see one here, it's an error in the pipeline
@@ -298,7 +292,9 @@ def translateExpr (expr : StmtExprMd)
   | .Block [] _ =>
       throwExprDiagnostic $ diagnosticFromSource expr.source "empty block expression should have been lowered in a separate pass" DiagnosticType.StrataBug
   | .Return _ => disallowed expr.source "return expression should be lowered in a separate pass"
-
+  | .IsType _ _ =>
+      throwExprDiagnostic $ diagnosticFromSource expr.source "IsType should have been lowered" DiagnosticType.StrataBug
+  | .New _ => throwExprDiagnostic $ diagnosticFromSource expr.source s!"New should have been eliminated by typeHierarchyTransform" DiagnosticType.StrataBug
   | .AsType target _ => throwExprDiagnostic $ diagnosticFromSource expr.source "AsType expression translation" DiagnosticType.NotYetImplemented
   | .Assigned _ => throwExprDiagnostic $ diagnosticFromSource expr.source "assigned expression translation" DiagnosticType.NotYetImplemented
   | .Old value =>
@@ -600,12 +596,13 @@ Translate a list of checks (preconditions or postconditions) to Core checks.
 Each check gets a label like `"requires"` or `"requires_0"`, `"requires_1"`, etc.
 -/
 private def translateChecks (checks : List Condition) (labelBase : String) (overrideFree: Bool)
+    (defaultSummary : Option String := none)
     : TranslateM (ListMap Core.CoreLabel Core.Procedure.Check) :=
   checks.mapIdxM (fun i check => do
     let label := if checks.length == 1 then labelBase else s!"{labelBase}_{i}"
     let checkExpr ← translateExpr check.condition [] (isPureContext := true)
     let baseMd := astNodeToCoreMd check.condition
-    let md := match check.summary with
+    let md := match check.summary.orElse (fun _ => defaultSummary) with
       | some msg => baseMd.pushElem Imperative.MetaData.propertySummary (.msg msg)
       | none => baseMd
     let attr := if check.free || overrideFree then Core.Procedure.CheckAttr.Free else .Default
@@ -659,6 +656,7 @@ def translateProcedure (proc : Procedure) : TranslateM Core.Procedure := do
     match proc.body with
     | .Opaque postconds _ _ | .Abstract postconds =>
         translateChecks postconds s!"postcondition" bodyStmts.isNone
+          (defaultSummary := "postcondition")
     | _ => pure []
   -- Wrap body in a labeled block so early returns (exit) work correctly.
   -- `bodyLabel` is the shared "$body" constant the resolver pre-registers.
@@ -666,50 +664,6 @@ def translateProcedure (proc : Procedure) : TranslateM Core.Procedure := do
   let spec : Core.Procedure.Spec := { preconditions, postconditions }
   return { header, spec, body := .structured body }
 
-def translateInvokeOnAxiom (proc : Procedure) (trigger : StmtExprMd)
-    : TranslateM (Option Core.Decl) := do
-  let postconds := match proc.body with
-    | .Opaque postconds _ _ | .Abstract postconds => postconds
-    | _ => []
-  if postconds.isEmpty then return none
-  -- All input param names become bound variables.
-  -- buildQuants nests ∀ p1, ∀ p2, ..., ∀ pn :: body, so inside body the innermost
-  -- binder (pn) is de Bruijn index 0, and the outermost (p1) is index n-1.
-  -- translateExpr uses findIdx? on boundVars, so we must list params innermost-first
-  -- (i.e. reversed) so that pn → 0, ..., p1 → n-1.
-  let boundVars := proc.inputs.reverse.map (·.name)
-  -- Translate postconditions and trigger with the full bound-var context
-  let postcondExprs ← postconds.mapM (fun pc => translateExpr pc.condition boundVars (isPureContext := true))
-  let bodyExpr : Core.Expression.Expr := match postcondExprs with
-    | [] => .const () (.boolConst true)
-    | [e] => e
-    | e :: rest => rest.foldl (fun acc x => LExpr.mkApp () boolAndOp [acc, x]) e
-  let triggerExpr ← translateExpr trigger boundVars (isPureContext := true)
-  -- Wrap in ∀ from outermost (first param) to innermost (last param).
-  -- The trigger is placed on the innermost quantifier.
-  let quantified ← buildQuants proc.inputs bodyExpr triggerExpr
-  return some (.ax { name := s!"invokeOn_{proc.name.text}", e := quantified } (identifierToCoreMd proc.name))
-where
-  /-- Build `∀ p1 ... pn :: { trigger } body`. The trigger is on the innermost quantifier. -/
-  buildQuants (params : List Parameter)
-      (body : Core.Expression.Expr) (trigger : Core.Expression.Expr)
-      : TranslateM Core.Expression.Expr := do
-    match params with
-    | [] => return body
-    | [p] =>
-      return LExpr.allTr () p.name.text (some (← translateType p.type)) trigger body
-    | p :: rest => do
-      let inner ← buildQuants rest body trigger
-      return LExpr.all () p.name.text (some (← translateType p.type)) inner
-
-structure LaurelTranslateOptions where
-  inlineFunctionsWhenPossible : Bool := false
-  overflowChecks : Core.OverflowChecks := {}
-  keepAllFilesPrefix : Option String := none
-
-instance : Inhabited LaurelTranslateOptions where
-  default := {}
-
 structure LaurelVerifyOptions where
   translateOptions : LaurelTranslateOptions := {}
   verifyOptions : Core.VerifyOptions := .default
@@ -717,6 +671,13 @@ structure LaurelVerifyOptions where
 instance : Inhabited LaurelVerifyOptions where
   default := {}
 
+/-- Unwrap the pattern produced by EliminateValuesInReturns + EliminateReturnStatements:
+    `{ result := <expr>; exit "$return" } $return` → `<expr>` -/
+private def unwrapReturnBlock (b : StmtExprMd) : StmtExprMd :=
+  match b.val with
+  | .Block [⟨.Assign [⟨.Local _, _⟩] value, _⟩, ⟨.Exit "$return", _⟩] (some "$return") => value
+  | _ => b
+
 /--
 Translate a Laurel Procedure to a Core Function (when applicable) using `TranslateM`.
 Diagnostics for disallowed constructs in the function body are emitted into the monad state.
@@ -755,10 +716,11 @@ def translateProcedureToFunction (options: LaurelTranslateOptions) (isRecursive:
     | none => if options.inlineFunctionsWhenPossible then #[.inline] else #[]
 
   let body ← match proc.body with
-    | .Transparent bodyExpr => some <$> translateExpr bodyExpr [] (isPureContext := true)
+    | .Transparent bodyExpr =>
+      some <$> translateExpr (unwrapReturnBlock bodyExpr) [] (isPureContext := true)
     | .Opaque _ (some bodyExpr) _ =>
       emitDiagnostic (diagnosticFromSource proc.name.source "functions with postconditions are not yet supported")
-      some <$> translateExpr bodyExpr [] (isPureContext := true)
+      some <$> translateExpr (unwrapReturnBlock bodyExpr) [] (isPureContext := true)
     | _ => pure none
   let f : Core.Function := {
     name := ⟨proc.name.text, ()⟩
@@ -816,13 +778,11 @@ def translateLaurelToCore (options: LaurelTranslateOptions) (ordered : CoreWithL
         return coreFuncs
     | .procedure proc => do
       let procDecl ← translateProcedure proc
-      -- Translate axioms from invokeOn
-      let invokeOnDecls ← match proc.invokeOn with
-        | some trigger => do
-          let axDecl? ← translateInvokeOnAxiom proc trigger
-          pure axDecl?.toList
-        | none => pure []
-      return [Core.Decl.proc procDecl (identifierToCoreMd proc.name)] ++ invokeOnDecls
+      -- Translate axioms (populated by the contract pass from invokeOn + ensures)
+      let axiomDecls ← proc.axioms.mapM fun ax => do
+        let coreExpr ← translateExpr ax [] (isPureContext := true)
+        return Core.Decl.ax { name := s!"invokeOn_{proc.name.text}", e := coreExpr } (identifierToCoreMd proc.name)
+      return [Core.Decl.proc procDecl (identifierToCoreMd proc.name)] ++ axiomDecls
     | .datatypes dts => do
       let ldatatypes ← dts.mapM translateDatatypeDefinition
       return [Core.Decl.type (.data ldatatypes) mdWithUnknownLoc]
@@ -839,5 +799,22 @@ def translateLaurelToCore (options: LaurelTranslateOptions) (ordered : CoreWithL
 
   pure { decls := coreDecls }
 
+public def laurelToCoreSchemaPass : LaurelPass CoreWithLaurelTypes Core.Program where
+  name := "LaurelToCoreSchemaPass"
+  comesBefore := []
+  documentation := "Produce a `Core` program from a `CoreWithLaurelTypes` program. Intended to be dumb 1-to-1 translation. However, there are several smart translations still happening:
+  - The @[cases] parameter is inferred for recursive functions.
+  - 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 (coreProgramOption, translateState) :=
+      runTranslateM initState (translateLaurelToCore options p)
+    let diagnostics : List DiagnosticModel :=
+      -- Because of the duplication between functions and procedures, this translation is liable to create duplicate diagnostics
+      let d := translateState.diagnostics.eraseDups
+      if d.isEmpty then translateState.coreDiagnostics else d
+    (coreProgramOption.getD default, diagnostics, {})
+
 end -- public section
 end Laurel
diff --git a/Strata/Languages/Laurel/LaurelTypes.lean b/Strata/Languages/Laurel/LaurelTypes.lean
index dd29c80bab..d462f5242e 100644
--- a/Strata/Languages/Laurel/LaurelTypes.lean
+++ b/Strata/Languages/Laurel/LaurelTypes.lean
@@ -129,6 +129,7 @@ triggers heap parameterization. -/
 def isHeapRelevantType (ty : HighType) : Bool :=
   (classifyModifiesHighType ty).isSome
 
+
 end Strata.Laurel
 
 end
diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean
index dcd2954729..971bafbf91 100644
--- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean
+++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean
@@ -9,6 +9,7 @@ import Strata.Util.Tactics
 public import Strata.Languages.Laurel.LaurelPass
 public import Strata.Languages.Laurel.Resolution
 import Strata.Languages.Laurel.LaurelTypes
+import Strata.Languages.Laurel.TransparencyPass
 
 namespace Strata
 namespace Laurel
@@ -80,47 +81,38 @@ structure LiftState where
   condCounter : Nat := 0
   /-- All procedures in the program, used to look up return types of imperative calls -/
   procedures : List Procedure := []
+  /-- Names of callees whose calls should be treated as imperative (lifted) -/
+  imperativeCallees : List String := []
 
 @[expose] abbrev LiftM := StateM LiftState
 
-private def emptyMd : Option String := none
-
 private def freshTempFor (varName : Identifier) : LiftM Identifier := do
   let counters := (← get).varCounters
   let counter := counters.find? (·.1 == varName) |>.map (·.2) |>.getD 0
   modify fun s => { s with varCounters := (varName, counter + 1) :: s.varCounters.filter (·.1 != varName) }
   return s!"${varName.text}_{counter}"
 
-private def freshCondVar : LiftM Identifier := do
+private def freshTempVar : LiftM Identifier := do
   let n := (← get).condCounter
   modify fun s => { s with condCounter := n + 1 }
-  return s!"$c_{n}"
+  return s!"$cndtn_{n}"
 
 private def prepend (stmt : StmtExprMd) : LiftM Unit :=
   modify fun s => { s with prependedStmts := stmt :: s.prependedStmts }
 
+private def prependList (stmts : List StmtExprMd) : LiftM Unit :=
+  modify fun s => { s with prependedStmts := stmts ++ s.prependedStmts }
+
 private def onlyKeepSideEffectStmtsAndLast (stmts : List StmtExprMd) : LiftM (List StmtExprMd) := do
   match stmts with
   | [] => return []
   | _ =>
+    -- return stmts
     let last := stmts.getLast!
     let nonLast ← stmts.dropLast.flatMapM (fun s =>
       match s.val with
       | .Var (.Declare ..) | .Assign ([⟨.Declare .., _⟩]) _ => do
-          -- This addPrepend is a hack to work around Core not having let expressions
-          -- Otherwise we could keep them in the block
-          prepend s
-          pure []
-      | .Assert _ => do
-          -- Hack to work around Core not supporting assert expressions
-          -- Otherwise we could keep them in the block
-          prepend s
-          pure []
-      | .Assume _ => do
-          -- Hack to work around Core not supporting assume expressions
-          -- Otherwise we could keep them in the block
-          prepend s
-          pure []
+          pure [s]
 
       /-
       Any other impure StmtExpr, like .Assign, .Exit or .Return,
@@ -149,97 +141,104 @@ private def computeType (expr : StmtExprMd) : LiftM HighTypeMd := do
   let s ← get
   return computeExprType s.model expr
 
-/-- Check if an expression contains any assignments (recursively). -/
-def containsAssignment (expr : StmtExprMd) : Bool :=
+/-- Check if an expression contains any assignments or imperative calls
+(recursively). When `liftsAssertsAssumes` is set, asserts and assumes also
+count — these are lifted into statement position by `transformExpr`, so an
+if-then-else whose branch contains one must itself be lifted to keep the
+statement guarded by the condition. -/
+def containsAssignmentOrImperativeCall (imperativeCallees : List String) (expr : StmtExprMd)
+    (liftsAssertsAssumes : Bool := false) : Bool :=
   match expr with
   | AstNode.mk val _ =>
   match val with
   | .Assign .. => true
   | .IncrDecr .. => true
-  | .StaticCall _ args => args.attach.any (fun x => containsAssignment x.val)
-  | .PrimitiveOp _ args _ => args.attach.any (fun x => containsAssignment x.val)
-  | .Block stmts _ => stmts.attach.any (fun x => containsAssignment x.val)
+  | .StaticCall name args1 =>
+    imperativeCallees.contains name.text ||
+      args1.attach.any (fun x => containsAssignmentOrImperativeCall imperativeCallees x.val liftsAssertsAssumes)
+  | .PrimitiveOp _ args2 _ => args2.attach.any (fun x => containsAssignmentOrImperativeCall imperativeCallees x.val liftsAssertsAssumes)
+  | .Block stmts _ => stmts.attach.any (fun x => containsAssignmentOrImperativeCall imperativeCallees x.val liftsAssertsAssumes)
   | .IfThenElse cond th el =>
-      containsAssignment cond || containsAssignment th ||
-      match el with | some e => containsAssignment e | none => false
+      containsAssignmentOrImperativeCall imperativeCallees cond liftsAssertsAssumes ||
+      containsAssignmentOrImperativeCall imperativeCallees th liftsAssertsAssumes ||
+      match el with | some e => containsAssignmentOrImperativeCall imperativeCallees e liftsAssertsAssumes | none => false
+  | .Assume cond => liftsAssertsAssumes || containsAssignmentOrImperativeCall imperativeCallees cond liftsAssertsAssumes
+  | .Assert cond => liftsAssertsAssumes || containsAssignmentOrImperativeCall imperativeCallees cond.condition liftsAssertsAssumes
+  | .InstanceCall target _ args =>
+      containsAssignmentOrImperativeCall imperativeCallees target liftsAssertsAssumes ||
+      args.attach.any (fun x => containsAssignmentOrImperativeCall imperativeCallees x.val liftsAssertsAssumes)
+  | .Quantifier _ _ trigger body =>
+      containsAssignmentOrImperativeCall imperativeCallees body liftsAssertsAssumes ||
+      match trigger with | some t => containsAssignmentOrImperativeCall imperativeCallees t liftsAssertsAssumes | none => false
+  | .Old value => containsAssignmentOrImperativeCall imperativeCallees value liftsAssertsAssumes
+  | .Fresh value => containsAssignmentOrImperativeCall imperativeCallees value liftsAssertsAssumes
+  | .ProveBy value proof =>
+      containsAssignmentOrImperativeCall imperativeCallees value liftsAssertsAssumes ||
+      containsAssignmentOrImperativeCall imperativeCallees proof liftsAssertsAssumes
+  | .ReferenceEquals lhs rhs =>
+      containsAssignmentOrImperativeCall imperativeCallees lhs liftsAssertsAssumes ||
+      containsAssignmentOrImperativeCall imperativeCallees rhs liftsAssertsAssumes
+  | .PureFieldUpdate target _ newValue =>
+      containsAssignmentOrImperativeCall imperativeCallees target liftsAssertsAssumes ||
+      containsAssignmentOrImperativeCall imperativeCallees newValue liftsAssertsAssumes
+  | .AsType target _ => containsAssignmentOrImperativeCall imperativeCallees target liftsAssertsAssumes
+  | .IsType target _ => containsAssignmentOrImperativeCall imperativeCallees target liftsAssertsAssumes
+  | .Assigned name => containsAssignmentOrImperativeCall imperativeCallees name liftsAssertsAssumes
+  | .ContractOf _ func => containsAssignmentOrImperativeCall imperativeCallees func liftsAssertsAssumes
+  | .Return (some v) => containsAssignmentOrImperativeCall imperativeCallees v liftsAssertsAssumes
   | _ => false
   termination_by expr
   decreasing_by
-    all_goals ((try cases x); simp_all; try term_by_mem)
+    all_goals (try cases x)
+    all_goals (try simp_all)
+    all_goals (try have := Condition.sizeOf_condition_lt ‹_›)
+    all_goals (try term_by_mem)
+    all_goals omega
 
-/-- Like containsAssignment but does NOT recurse into Blocks (treats them as opaque).
-    Used by assert/assume handlers to allow generated Block wrappers through. -/
-def containsBareAssignment (expr : StmtExprMd) : Bool :=
-  match expr with
-  | AstNode.mk val _ =>
-  match val with
-  | .Assign .. => true
-  | .IncrDecr .. => true
-  | .StaticCall _ args => args.attach.any (fun x => containsBareAssignment x.val)
-  | .PrimitiveOp _ args _ => args.attach.any (fun x => containsBareAssignment x.val)
-  | .Block _ _ => false
-  | .IfThenElse cond th el =>
-      containsBareAssignment cond || containsBareAssignment th ||
-      match el with | some e => containsBareAssignment e | none => false
-  | _ => false
-  termination_by expr
-  decreasing_by
-    all_goals ((try cases x); simp_all; try term_by_mem)
+mutual
 
-/-- Check if an expression contains any non-functional procedure calls (recursively). -/
-def containsImperativeCall (model : SemanticModel) (expr : StmtExprMd) : Bool :=
-  match expr with
-  | AstNode.mk val _ =>
-  match val with
-  | .StaticCall name args =>
-    (match model.get name with
-    | .staticProcedure proc => !proc.isFunctional
-    | _ => false) ||
-      args.attach.any (fun x => containsImperativeCall model x.val)
-  | .PrimitiveOp _ args _ => args.attach.any (fun x => containsImperativeCall model x.val)
-  | .Block stmts _ => stmts.attach.any (fun x => containsImperativeCall model x.val)
-  | .IfThenElse cond th el =>
-      containsImperativeCall model cond ||
-      containsImperativeCall model th ||
-      match el with | some e => containsImperativeCall model e | none => false
-  | _ => false
-  termination_by expr
-  decreasing_by
-    all_goals ((try cases x); simp_all; try term_by_mem)
+def asLifted { t: Type } (runner: LiftM t) : LiftM t := do
+  let savedState ← get
+  modify fun s => { s with prependedStmts := [], subst := []}
+  let result ← runner
+  modify fun _ => savedState
+  return result
 
-/-- Check if an expression contains any assignments or non-functional procedure calls (recursively). -/
-def containsAssignmentOrImperativeCall (model : SemanticModel) (expr : StmtExprMd) : Bool :=
-  containsAssignment expr || containsImperativeCall model expr
+/--
+Process an expression in expression context, traversing arguments right to left.
+Assignments are lifted to prependedStmts and replaced with snapshot variable references.
+-/
+def transformLiftedExpr (expr : StmtExprMd) : LiftM (List StmtExprMd × StmtExprMd) := do
+  let savedSubst := (← get).subst
+  let savedPrepends ← takePrepends
+  modify fun s => { s with prependedStmts := [], subst := []}
+  let result ← transformExpr expr
+  let newPrepends ← takePrepends
+  modify fun s => { s with prependedStmts := savedPrepends, subst := savedSubst }
+  return (newPrepends, result)
+  termination_by (sizeOf expr, 3)
 
 /--
-Shared logic for lifting an assignment in expression position:
-prepends the assignment, creates before-snapshots for all targets,
-and updates substitutions. The value should already be transformed by the caller.
+Process an expression in expression context, traversing arguments right to left.
+Assignments are lifted to prependedStmts and replaced with snapshot variable references.
 -/
-private def liftAssignExpr (targets : List VariableMd) (seqValue : StmtExprMd)
-    (source : Option FileRange) : LiftM Unit := do
-  -- Prepend the assignment itself
-  prepend (⟨.Assign targets seqValue, source⟩)
-  -- Create a before-snapshot for each target and update substitutions
-  for target in targets do
-    match target.val with
-    | .Local varName =>
-        let snapshotName ← freshTempFor varName
-        let varType ← computeType (⟨ .Var (.Local varName), source⟩)
-        -- Snapshot goes before the assignment (cons pushes to front)
-        prepend (⟨.Assign [⟨.Declare ⟨snapshotName, varType⟩, source⟩] (⟨.Var (.Local varName), source⟩), source⟩)
-        setSubst varName snapshotName
-    | _ => pure ()
+def transformLiftedStmt (expr : StmtExprMd) : LiftM Unit := do
+  let savedSubst := (← get).subst
+  let previousPrepends := (← get).prependedStmts
+  modify fun s => { s with subst := [], prependedStmts := [] }
+  let result ← transformStmt expr
+  modify fun s => { s with subst := savedSubst, prependedStmts := previousPrepends }
+  prependList result
+  termination_by (sizeOf expr, 1)
 
-mutual
 /--
 Process an expression in expression context, traversing arguments right to left.
 Assignments are lifted to prependedStmts and replaced with snapshot variable references.
 -/
 def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do
-  match expr with
+  match h_node : expr with
   | AstNode.mk val source =>
-  match val with
+  match h_val : val with
   | .Var (.Local name) =>
       return ⟨.Var (.Local (← getSubst name)), source⟩
 
@@ -247,7 +246,7 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do
 
   | .Hole false (some holeType) =>
       -- Nondeterministic typed hole: lift to a fresh variable with no initializer (havoc)
-      let holeVar ← freshCondVar
+      let holeVar ← freshTempVar
       prepend ⟨ .Var (.Declare ⟨holeVar, holeType⟩), source⟩
       return ⟨ .Var (.Local holeVar), source ⟩
 
@@ -266,14 +265,23 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do
           if hasSubst then
             pure (⟨.Var (.Local (← getSubst param.name)), source⟩)
           else
-            return expr
+            pure (⟨.Var (.Local param.name), source⟩)
         | _ =>
           dbg_trace "Strata bug: non-identifier targets should have been removed before the lift expression phase";
           return expr
 
-      -- Use the original value (not seqValue) for the prepended assignment,
-      -- because prepended statements execute in program order and don't need substitutions.
-      liftAssignExpr targets value source
+      transformLiftedStmt expr
+
+      -- Create a before-snapshot for each target and update substitutions
+      for target in targets do
+        match target.val with
+        | .Local varName =>
+            let snapshotName ← freshTempFor varName
+            let varType ← computeType ⟨ .Var (.Local varName), source ⟩
+            -- Snapshot goes before the assignment (cons pushes to front)
+            prepend (⟨.Assign [⟨.Declare ⟨snapshotName, varType⟩, source⟩] (⟨.Var (.Local varName), source⟩), source⟩)
+            setSubst varName snapshotName
+        | _ => pure ()
 
       return resultExpr
 
@@ -283,71 +291,76 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do
       return ⟨.PrimitiveOp op seqArgs.reverse, source⟩
 
   | .StaticCall callee args =>
-    let model := (← get).model
-    let seqArgs ← args.reverse.mapM transformExpr
-    let seqCall := ⟨.StaticCall callee seqArgs.reverse, source⟩
-    if model.isFunction callee then
+    let imperativeCallees := (← get).imperativeCallees
+    if !imperativeCallees.contains callee.text then
+      let seqArgs ← args.reverse.mapM transformExpr
+      let seqCall := ⟨.StaticCall callee seqArgs.reverse, source⟩
       return seqCall
     else
-      -- Imperative call in expression position: lift to an assignment.
-      -- Only valid for single-output procedures (or unresolved ones where we
-      -- fall back to a single target). Multi-output procedures in expression
-      -- position are a bug in the upstream translation — Resolution should
-      -- emit a diagnostic for that case.
-      let outputs := match model.get callee with
-        | .staticProcedure proc => proc.outputs
-        | .instanceProcedure _ proc => proc.outputs
-        | _ => []
-      let callResultVar ← freshCondVar
-      let callResultType ← match outputs with
-        | [single] => pure single.type
-        | _ => computeType expr
-      let liftedCall := [
-        ⟨.Var (.Declare ⟨callResultVar, callResultType⟩), source⟩,
-        ⟨.Assign [⟨.Local callResultVar, source⟩] seqCall, source⟩
-      ]
-      modify fun s => { s with prependedStmts := s.prependedStmts ++ liftedCall}
+      let callResultVar ← freshTempVar
+      let callResultType ← computeType expr
+
+      let prepends ← asLifted (transformStmtAssignImperativeCall
+        [⟨ .Declare ⟨callResultVar, callResultType⟩, source⟩] callee args source source)
+      prependList prepends
       return ⟨.Var (.Local callResultVar), source⟩
 
   | .IfThenElse cond thenBranch elseBranch =>
-      let model :=  (← get).model
-      let thenHasAssign := containsAssignmentOrImperativeCall model thenBranch
+      let imperativeCallees := (← get).imperativeCallees
+      -- A branch must be lifted if it contains anything `transformExpr` would
+      -- hoist: assignments, imperative calls, asserts, or assumes. (Asserts and
+      -- assumes matter because hoisting them out of the branch would drop the
+      -- condition's guard — see `liftsAssertsAssumes`.)
+      let thenHasAssign := containsAssignmentOrImperativeCall imperativeCallees thenBranch (liftsAssertsAssumes := true)
       let elseHasAssign := match elseBranch with
-        | some e => containsAssignmentOrImperativeCall model e
+        | some e => containsAssignmentOrImperativeCall imperativeCallees e (liftsAssertsAssumes := true)
         | none => false
       if thenHasAssign || elseHasAssign then
+
+        -- Infer type from the ORIGINAL then-branch (not the transformed one),
+        -- because the transformed expression may reference freshly generated
+        -- variables (e.g. $c_2) that don't exist in the SemanticModel yet.
+        let condType ← computeType thenBranch
+        let needsCondVar := condType.val != .TVoid
+
         -- Lift the entire if-then-else. Introduce a fresh variable for the result.
-        let condVar ← freshCondVar
-        let seqCond ← transformExpr cond
+        let condVar ← freshTempVar
         -- Save outer state
         let savedSubst := (← get).subst
-        let savedPrepends := (← get).prependedStmts
+        let savedPrepends ← takePrepends
+
+        let seqCond ← transformExpr cond
+        let condPrepends ← takePrepends
         -- Process then-branch from scratch
         modify fun s => { s with prependedStmts := [], subst := [] }
         let seqThen ← transformExpr thenBranch
         let thenPrepends ← takePrepends
-        let thenBlock := ⟨.Block (thenPrepends ++ [⟨.Assign [⟨ .Local condVar, source⟩] seqThen, source⟩]) none, source⟩
+        let assignStmts := if needsCondVar then [⟨.Assign [⟨ .Local condVar, source⟩] seqThen, source⟩] else [seqThen]
+        let thenBlock := ⟨.Block (thenPrepends ++ assignStmts) none, source ⟩
         -- Process else-branch from scratch
         modify fun s => { s with prependedStmts := [], subst := [] }
         let seqElse ← match elseBranch with
           | some e => do
               let se ← transformExpr e
               let elsePrepends ← takePrepends
-              pure (some ⟨.Block (elsePrepends ++ [⟨.Assign [⟨ .Local condVar, source⟩] se, source⟩]) none, source⟩)
+              let assignStmts: List StmtExprMd := if needsCondVar then [⟨.Assign [⟨ .Local condVar, source⟩] se, source⟩] else [se];
+              pure (some (⟨.Block (elsePrepends ++ assignStmts) none, source ⟩))
           | none => pure none
         -- Restore outer state
         modify fun s => { s with subst := savedSubst, prependedStmts := savedPrepends }
-        -- Infer type from the ORIGINAL then-branch (not the transformed one),
-        -- because the transformed expression may reference freshly generated
-        -- variables (e.g. $c_2) that don't exist in the SemanticModel yet.
-        let condType ← computeType thenBranch
         -- IfThenElse added first (cons puts it deeper), then declaration (cons puts it on top)
         -- Output order: declaration, then if-then-else
         prepend (⟨.IfThenElse seqCond thenBlock seqElse, source⟩)
-        prepend ⟨.Var (.Declare ⟨condVar, condType⟩), source⟩
-        return ⟨.Var (.Local condVar), source⟩
+        if needsCondVar then
+          prepend ⟨.Var (.Declare ⟨condVar, condType⟩), source ⟩
+          modify fun s => { s with prependedStmts := condPrepends ++ s.prependedStmts }
+          return ⟨.Var (.Local condVar), source⟩
+        else
+          modify fun s => { s with prependedStmts := condPrepends ++ s.prependedStmts }
+          -- Unused value
+          return ⟨ .Hole, expr.source ⟩
       else
-        -- No assignments in branches — recurse normally
+        -- No liftable statements in branches — recurse normally.
         let seqCond ← transformExpr cond
         let seqThen ← transformExpr thenBranch
         let seqElse ← match elseBranch with
@@ -393,26 +406,105 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do
       else
         return expr
 
-  | .Assert _ =>
-      -- An assert in expression position (e.g. inside a block used as a value)
-      -- is lifted as a side effect. Prepend it *here*, during the right-to-left
-      -- traversal, so it keeps its position relative to assignments lifted from
-      -- the same block. (If it were left for `onlyKeepSideEffectStmtsAndLast` to
-      -- prepend afterwards, it would be moved ahead of those assignments.)
-      -- Core has no assert-expression, so the expression yields a dummy value
-      -- that the surrounding block discards as a non-final statement.
-      prepend expr
-      return ⟨.LiteralBool true, source⟩
-
-  | .Assume _ =>
-      -- See the `.Assert` case above: same side-effect lifting for assumes.
-      prepend expr
-      return ⟨.LiteralBool true, source⟩
+  | .Assume cond =>
+      let (argPrepends, newCond) ← transformLiftedExpr cond
+      prepend ⟨ .Assume newCond, source⟩
+      prependList argPrepends
+      default
+
+  | .Assert cond =>
+      let (argPrepends, newCond) ← transformLiftedExpr cond.condition
+      prepend ⟨ .Assert {cond with condition := newCond}, source⟩
+      prependList argPrepends
+      default
+
+  | .Return (some retExpr) =>
+      let seqRet ← transformExpr retExpr
+      return ⟨.Return (some seqRet), source⟩
+
+  | .While cond invs dec body =>
+      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⟩
+
+  | .PureFieldUpdate target fieldName newValue =>
+      let seqTarget ← transformExpr target
+      let seqNewValue ← transformExpr newValue
+      return ⟨.PureFieldUpdate seqTarget fieldName seqNewValue, source⟩
+
+  | .ReferenceEquals lhs rhs =>
+      let seqRhs ← transformExpr rhs
+      let seqLhs ← transformExpr lhs
+      return ⟨.ReferenceEquals seqLhs seqRhs, source⟩
+
+  | .AsType target ty =>
+      let seqTarget ← transformExpr target
+      return ⟨.AsType seqTarget ty, source⟩
+
+  | .IsType target ty =>
+      let seqTarget ← transformExpr target
+      return ⟨.IsType seqTarget ty, source⟩
+
+  | .InstanceCall target callee args =>
+      let seqArgs ← args.reverse.mapM transformExpr
+      let seqTarget ← transformExpr target
+      return ⟨.InstanceCall seqTarget callee seqArgs.reverse, source⟩
+
+  | .Quantifier mode param trigger body =>
+      let seqBody ← transformExpr body
+      let seqTrigger ← match trigger with
+        | some t => pure (some (← transformExpr t))
+        | none => pure none
+      return ⟨.Quantifier mode param seqTrigger seqBody, source⟩
+
+  | .Old value =>
+      let seqValue ← transformExpr value
+      return ⟨.Old seqValue, source⟩
+
+  | .Fresh value =>
+      let seqValue ← transformExpr value
+      return ⟨.Fresh seqValue, source⟩
+
+  | .Assigned name =>
+      let seqName ← transformExpr name
+      return ⟨.Assigned seqName, source⟩
+
+  | .ProveBy value proof =>
+      let seqValue ← transformExpr value
+      let seqProof ← transformExpr proof
+      return ⟨.ProveBy seqValue seqProof, source⟩
+
+  | .ContractOf ty func =>
+      let seqFunc ← transformExpr func
+      return ⟨.ContractOf ty seqFunc, source⟩
 
   | _ => return expr
-  termination_by (sizeOf expr, 0)
+  termination_by (sizeOf expr, 2)
+  decreasing_by
+    all_goals first
+      | (apply Prod.Lex.left; (try have := Condition.sizeOf_condition_lt ‹_›); term_by_mem)
+      | (apply Prod.Lex.left; simp <;> omega)
+      | (try subst h_node; try subst h_val; apply Prod.Lex.right; omega)
+
+def transformStmtAssignImperativeCall
+    (targets : List (AstNode Variable))
+    (callee: Identifier)
+    (args: List StmtExprMd)
+    (source: Option FileRange)
+    (callSource: Option FileRange): LiftM (List StmtExprMd) := do
+  let seqArgs ← args.reverse.mapM transformExpr
+  let argPrepends ← takePrepends
+  modify fun s => { s with subst := [] }
+  return argPrepends ++ [⟨.Assign targets ⟨.StaticCall callee seqArgs.reverse, callSource⟩, source⟩]
+  termination_by (sizeOf args, 0)
   decreasing_by
-    all_goals (simp_all; try term_by_mem)
+    all_goals try (apply Prod.Lex.right; omega)
+    all_goals (try simp_all; try have := Condition.sizeOf_condition_lt ‹_›; try term_by_mem)
+    all_goals (try (apply Prod.Lex.left); try term_by_mem; try omega)
 
 /--
 Process a statement, handling any assignments in its sub-expressions.
@@ -423,26 +515,24 @@ def transformStmt (stmt : StmtExprMd) : LiftM (List StmtExprMd) := do
   | AstNode.mk val source =>
   match val with
   | .Assert cond =>
-      -- Do not transform assert conditions with bare assignments — they are
-      -- semantic errors that should be rejected downstream.
-      -- But Blocks with assignments (generated multi-output call wrappers)
-      -- are handled by the Block case in transformExpr above.
-      if !containsBareAssignment cond.condition then
+      -- Do not transform assert conditions with assignments — they must be rejected.
+      -- But nondeterministic holes need to be lifted.
+      -- if containsNondetHole cond.condition && !containsAssignmentOrImperativeCall (← get).model cond.condition then
         let seqCond ← transformExpr cond.condition
         let prepends ← takePrepends
         modify fun s => { s with subst := [] }
         return prepends ++ [⟨.Assert { cond with condition := seqCond }, source⟩]
-      else
-        return [stmt]
+      -- else
+      --   return [stmt]
 
   | .Assume cond =>
-      if !containsBareAssignment cond then
+      -- if containsNondetHole cond && !containsAssignmentOrImperativeCall (← get).model cond then
         let seqCond ← transformExpr cond
         let prepends ← takePrepends
         modify fun s => { s with subst := [] }
         return prepends ++ [⟨.Assume seqCond, source⟩]
-      else
-        return [stmt]
+      -- else
+      --   return [stmt]
 
   | .Block stmts metadata =>
       let seqStmts ← stmts.mapM transformStmt
@@ -458,17 +548,14 @@ def transformStmt (stmt : StmtExprMd) : LiftM (List StmtExprMd) := do
       | AstNode.mk value callSource =>
       match _: value with
       | .StaticCall callee args =>
-          let model := (← get).model
-          if model.isFunction callee then
+          let imperativeCallees := (← get).imperativeCallees
+          if imperativeCallees.contains callee.text then
+            transformStmtAssignImperativeCall targets callee args source callSource
+          else
             let seqValue ← transformExpr valueMd
             let prepends ← takePrepends
             modify fun s => { s with subst := [] }
             return prepends ++ [⟨.Assign targets seqValue, source⟩]
-          else
-            let seqArgs ← args.mapM transformExpr
-            let argPrepends ← takePrepends
-            modify fun s => { s with subst := [] }
-            return argPrepends ++ [⟨.Assign targets ⟨.StaticCall callee seqArgs, callSource⟩, source⟩]
       | _ =>
           let seqValue ← transformExpr valueMd
           let prepends ← takePrepends
@@ -480,11 +567,11 @@ def transformStmt (stmt : StmtExprMd) : LiftM (List StmtExprMd) := do
       let condPrepends ← takePrepends
       let seqThen ← do
         let stmts ← transformStmt thenBranch
-        pure ⟨.Block stmts none, source⟩
+        pure ⟨ .Block stmts none, source ⟩
       let seqElse ← match elseBranch with
         | some e => do
             let se ← transformStmt e
-            pure $ some ⟨.Block se none, source⟩
+            pure (some (⟨.Block se none, source ⟩))
         | none => pure none
       return condPrepends ++ [⟨.IfThenElse seqCond seqThen seqElse, source⟩]
 
@@ -509,16 +596,16 @@ def transformStmt (stmt : StmtExprMd) : LiftM (List StmtExprMd) := do
       let prepends ← takePrepends
       return prepends ++ [⟨.StaticCall name seqArgs, source⟩]
 
-  | .PrimitiveOp _ _ =>
+  | .PrimitiveOp _ args =>
       -- A `PrimitiveOp` in statement position. If it carries any side effects
       -- (an embedded assignment or imperative call — typically the result of
       -- the postfix increment lowering `(x := x + 1) - 1`), lift them out and
       -- discard the unused pure result. Otherwise leave the expression
       -- statement intact so the Core translator can preserve it via
       -- `exprAsUnusedInit`.
-      let model := (← get).model
-      if containsAssignmentOrImperativeCall model stmt then
-        let _ ← transformExpr stmt
+      let imperativeCallees := (← get).imperativeCallees
+      if containsAssignmentOrImperativeCall imperativeCallees stmt then
+        let _ ← args.reverse.mapM transformExpr
         let prepends ← takePrepends
         modify fun s => { s with subst := [] }
         return prepends
@@ -531,28 +618,33 @@ def transformStmt (stmt : StmtExprMd) : LiftM (List StmtExprMd) := do
       modify fun s => { s with subst := [] }
       return prepends ++ [⟨.Return (some seqRet), source⟩]
 
+  | .PrimitiveOp name args _ =>
+      let seqArgs ← args.mapM transformExpr
+      let prepends ← takePrepends
+      return prepends ++ [⟨.PrimitiveOp name seqArgs, source⟩]
   | _ =>
       return [stmt]
   termination_by (sizeOf stmt, 0)
   decreasing_by
-    all_goals (try term_by_mem)
-    all_goals (apply Prod.Lex.left; try term_by_mem)
+    all_goals try (apply Prod.Lex.right; omega)
+    all_goals (try simp_all; try have := Condition.sizeOf_condition_lt ‹_›; try term_by_mem)
+    all_goals (try (apply Prod.Lex.left); try term_by_mem; try omega)
 end
 
-def transformProcedureBody (proc : Procedure) (body : StmtExprMd) : LiftM StmtExprMd := do
+def transformProcedureBody (source: Option FileRange) (body : StmtExprMd) : LiftM StmtExprMd := do
   let stmts ← transformStmt body
   match stmts with
   | [single] => pure single
-  | multiple => pure ⟨.Block multiple none, proc.name.source⟩
+  | multiple => pure ⟨.Block multiple none, source ⟩
 
 def transformProcedure (proc : Procedure) : LiftM Procedure := do
   modify fun s => { s with subst := [], prependedStmts := [], varCounters := [] }
   match proc.body with
   | .Transparent bodyExpr =>
-      let seqBody ← transformProcedureBody proc bodyExpr
+      let seqBody ← transformProcedureBody proc.name.source bodyExpr
       pure { proc with body := .Transparent seqBody }
   | .Opaque postconds impl modif =>
-      let impl' ← impl.mapM (transformProcedureBody proc)
+      let impl' ← impl.mapM (transformProcedureBody proc.name.source)
       pure { proc with body := .Opaque postconds impl' modif }
   | .Abstract _ =>
       pure proc
@@ -561,19 +653,42 @@ def transformProcedure (proc : Procedure) : LiftM Procedure := do
 
 /--
 Transform a program to lift all assignments that occur in an expression context.
+When `procedureNames` is non-empty, only procedures whose name appears in the
+list are transformed; all others are left unchanged. When `procedureNames` is
+empty, no procedures are transformed.
 -/
-def liftExpressionAssignments (model: SemanticModel) (program : Program) : Program :=
-  let initState : LiftState := { model := model }
-  let (seqProcedures, _) := (program.staticProcedures.mapM transformProcedure).run initState
+def liftExpressionAssignments (program : Program)
+    (model : SemanticModel) (imperativeCallees : List String) : Program :=
+  let initState : LiftState := { model := model, imperativeCallees := imperativeCallees }
+  let transform := program.staticProcedures.mapM transformProcedure
+  let (seqProcedures, _) := transform.run initState
   { program with staticProcedures := seqProcedures }
 
 end -- public section
 
-/-- Pipeline pass: lift expression assignments. -/
-public def liftExpressionAssignmentsPass : LaurelPass where
-  name := "LiftExpressionAssignments"
-  documentation := "Lifts assignments that appear in expression contexts into preceding statements. This is necessary because Strata Core does not support assignments within expressions. The pass introduces fresh temporary variables where needed."
-  run := fun p m =>
-    (liftExpressionAssignments m p, [], {})
+/--
+Apply `liftExpressionAssignments` to the core (non-functional) procedures in an
+`UnorderedCoreWithLaurelTypes`. Only procedures whose names appear in the core
+procedure list are transformed; functions are left unchanged.
+-/
+def liftImperativeExpressionsInCore (uc : UnorderedCoreWithLaurelTypes)
+    (model : SemanticModel) : UnorderedCoreWithLaurelTypes :=
+  let imperativeCallees := uc.coreProcedures.map (·.name.text)
+  let liftedProgram := liftExpressionAssignments
+    { staticProcedures := uc.coreProcedures, staticFields := [], types := [], constants := [] }
+    model imperativeCallees
+  let liftedProcs := liftedProgram.staticProcedures
+  { uc with
+    functions := uc.functions
+    coreProcedures := liftedProcs
+  }
+
+public def liftImperativeExpressionsPass : LaurelPass UnorderedCoreWithLaurelTypes UnorderedCoreWithLaurelTypes where
+  name := "LiftImperativeExpressionsPass"
+  documentation := "Lifts assignments and other imperative expressions that appear in expression contexts into preceding statements. This is necessary because Strata Core does not support assignments within expressions. The pass introduces fresh temporary variables where needed."
+  comesAfter := [⟨ transparencyPass.meta, "The imperative expression lifting is only done in procedures, so it comes after the transparency pass"⟩]
+  needsResolves := true
+  run := fun p m _ =>
+    (liftImperativeExpressionsInCore p m, [], {})
 
 end Laurel
diff --git a/Strata/Languages/Laurel/LiftInstanceProcedures.lean b/Strata/Languages/Laurel/LiftInstanceProcedures.lean
index 2178269623..34ae4366c0 100644
--- a/Strata/Languages/Laurel/LiftInstanceProcedures.lean
+++ b/Strata/Languages/Laurel/LiftInstanceProcedures.lean
@@ -125,11 +125,11 @@ end -- public section
 
 /-- Pipeline pass: lift instance procedures to top-level static procedures
     and rewrite call sites to use the lifted names. -/
-public def liftInstanceProceduresPass : LaurelPass where
+public def liftInstanceProceduresPass : LoweringPass where
   name := "LiftInstanceProcedures"
   documentation := "Lifts every procedure declared inside a `composite` block to a top-level static procedure named `<CompositeName>$<methodName>` and rewrites call sites resolved to an instance procedure (including `obj#method(args)` surface syntax) to point at the lifted name. Clears `instanceProcedures` on every composite. Must run before HeapParameterization."
   needsResolves := true
-  run := fun p m => (liftInstanceProcedures m p, [], {})
-  comesBefore := [⟨ eliminateValueInReturnsPass, "eliminateValueInReturns only applies to static methods, hence all instance methods must have been lifted before." ⟩]
+  run := fun p m _ => (liftInstanceProcedures m p, [], {})
+  comesBefore := [⟨ eliminateValueInReturnsPass.meta, "eliminateValueInReturns only applies to static methods, hence all instance methods must have been lifted before." ⟩]
 
 end Strata.Laurel
diff --git a/Strata/Languages/Laurel/MapStmtExpr.lean b/Strata/Languages/Laurel/MapStmtExpr.lean
index 6d27d37aaf..2ba11ebea7 100644
--- a/Strata/Languages/Laurel/MapStmtExpr.lean
+++ b/Strata/Languages/Laurel/MapStmtExpr.lean
@@ -248,7 +248,6 @@ children, `pre` is called. If `pre` returns `some result`, that result is used
 directly (children are NOT recursed into). If `pre` returns `none`, normal
 bottom-up recursion proceeds and `post` is applied after children are rebuilt.
 -/
-@[expose]
 def mapStmtExprPrePostM [Monad m] (pre : StmtExprMd → m (Option StmtExprMd))
     (post : StmtExprMd → m StmtExprMd) (expr : StmtExprMd) : m StmtExprMd := do
   match ← pre expr with
@@ -278,16 +277,17 @@ def mapStmtExprPrePostM [Monad m] (pre : StmtExprMd → m (Option StmtExprMd))
     pure ⟨.Assign targets' (← mapStmtExprPrePostM pre post value), source⟩
   | .Var (.Field target fieldName) =>
     pure ⟨.Var (.Field (← mapStmtExprPrePostM pre post target) fieldName), source⟩
-  | .IncrDecr mode op ⟨.Field tgt fieldName, vs⟩ =>
-    pure ⟨.IncrDecr mode op ⟨.Field (← mapStmtExprPrePostM pre post tgt) fieldName, vs⟩, source⟩
-  | .IncrDecr _ _ ⟨.Local _, _⟩ | .IncrDecr _ _ ⟨.Declare _, _⟩ => pure expr
+  | .IncrDecr mode op target => match target with
+    | ⟨.Field tgt fieldName, vs⟩ => pure ⟨.IncrDecr mode op ⟨.Field (← mapStmtExprPrePostM pre post tgt) fieldName, vs⟩, source⟩
+    | ⟨.Local _, _⟩
+    | ⟨.Declare _, _⟩ => pure expr
+
   | .PureFieldUpdate target fieldName newValue =>
-    pure ⟨.PureFieldUpdate (← mapStmtExprPrePostM pre post target) fieldName
-      (← mapStmtExprPrePostM pre post newValue), source⟩
+    pure ⟨.PureFieldUpdate (← mapStmtExprPrePostM pre post target) fieldName (← mapStmtExprPrePostM pre post newValue), source⟩
   | .StaticCall callee args =>
     pure ⟨.StaticCall callee (← args.attach.mapM fun ⟨e, _⟩ => mapStmtExprPrePostM pre post e), source⟩
-  | .PrimitiveOp op args skipProof =>
-    pure ⟨.PrimitiveOp op (← args.attach.mapM fun ⟨e, _⟩ => mapStmtExprPrePostM pre post e) skipProof, source⟩
+  | .PrimitiveOp op args skipProofs =>
+    pure ⟨.PrimitiveOp op (← args.attach.mapM fun ⟨e, _⟩ => mapStmtExprPrePostM pre post e) skipProofs, source⟩
   | .ReferenceEquals lhs rhs =>
     pure ⟨.ReferenceEquals (← mapStmtExprPrePostM pre post lhs) (← mapStmtExprPrePostM pre post rhs), source⟩
   | .AsType target ty =>
@@ -314,16 +314,15 @@ def mapStmtExprPrePostM [Monad m] (pre : StmtExprMd → m (Option StmtExprMd))
     pure ⟨.ProveBy (← mapStmtExprPrePostM pre post value) (← mapStmtExprPrePostM pre post proof), source⟩
   | .ContractOf ty func =>
     pure ⟨.ContractOf ty (← mapStmtExprPrePostM pre post func), source⟩
+  -- Leaves: no StmtExprMd children.
+  -- ⚠ If a new StmtExpr constructor with StmtExprMd children is added,
+  -- it must get its own arm above; otherwise all passes will silently
+  -- skip recursion into those children.
   | .Exit _ | .LiteralInt _ | .LiteralBool _ | .LiteralString _ | .LiteralDecimal _ | .LiteralBv _ _
   | .Var (.Local _) | .Var (.Declare _) | .New _ | .This | .Abstract | .All | .Hole .. => pure expr
   post rebuilt
 termination_by sizeOf expr
-decreasing_by
-  all_goals simp_wf
-  all_goals (try have := AstNode.sizeOf_val_lt expr)
-  all_goals (try have := Condition.sizeOf_condition_lt ‹_›)
-  all_goals (try term_by_mem)
-  all_goals (cases expr; simp_all; omega)
+decreasing_by map_stmt_expr_decreasing expr
 
 /-- Apply a monadic transformation to all procedure bodies. -/
 @[expose]
@@ -336,14 +335,14 @@ def mapProcedureBodiesM [Monad m] (f : StmtExprMd → m StmtExprMd) (proc : Proc
   | .External => return proc
 
 /-- Apply a monadic transformation to all `StmtExprMd` nodes in a procedure
-    (preconditions, decreases, body, and invokeOn). -/
-@[expose]
+    (preconditions, decreases, body, invokeOn, and axioms). -/
 def mapProcedureM [Monad m] (f : StmtExprMd → m StmtExprMd) (proc : Procedure) : m Procedure := do
   let proc ← mapProcedureBodiesM f proc
   return { proc with
     preconditions := ← proc.preconditions.mapM (·.mapM f)
     decreases := ← proc.decreases.mapM f
-    invokeOn := ← proc.invokeOn.mapM f }
+    invokeOn := ← proc.invokeOn.mapM f
+    axioms := ← proc.axioms.mapM f }
 
 /-- Apply a monadic transformation to every procedure in a program — both
     top-level static procedures and the instance procedures of composite types.
diff --git a/Strata/Languages/Laurel/MergeAndLiftReturns.lean b/Strata/Languages/Laurel/MergeAndLiftReturns.lean
index 567dd276fc..06f44102d1 100644
--- a/Strata/Languages/Laurel/MergeAndLiftReturns.lean
+++ b/Strata/Languages/Laurel/MergeAndLiftReturns.lean
@@ -6,124 +6,95 @@
 module
 
 public import Strata.Languages.Laurel.LaurelAST
+import Strata.Languages.Laurel.Grammar.AbstractToConcreteTreeTranslator
 import Strata.Util.Tactics
+import Strata.Languages.Laurel.EliminateValueInReturns
 public import Strata.Languages.Laurel.LaurelPass
 
 /-!
-# Eliminate Returns in Expression Position
 
-Rewrites functional procedure bodies so that `return` statements are removed
-and early-return guard patterns become if-then-else expressions. This makes
-the body a pure expression tree suitable for translation to a Core function.
-
-The algorithm walks a block backwards (from last statement to first),
-accumulating a result expression:
-
-- The last statement is converted via `lastStmtToExpr` which strips `return`,
-  recurses into blocks, and handles if-then-else.
-- Each preceding statement wraps around the accumulated result via `stmtsToExpr`:
-  - `if (cond) { body }` (no else) becomes `if cond then lastStmtToExpr(body) else acc`
-  - Other statements are kept in a two-element block with the accumulator.
+Given a transparent body, merge the returns into a single outer return.
+Emits a diagnostic if it fails at any step.
 
 -/
 
 namespace Strata.Laurel
 
-/-- Appending a singleton strictly increases `sizeOf`. -/
-private theorem List.sizeOf_lt_append_singleton [SizeOf α] (xs : List α) (y : α) :
-    sizeOf xs < sizeOf (xs ++ [y]) := by
-  induction xs with
-  | nil => simp_all; omega
-  | cons hd tl ih => simp_all [List.cons_append]
-
-/-- `dropLast` of a non-empty list has strictly smaller `sizeOf`. -/
-private theorem List.sizeOf_dropLast_lt [SizeOf α] {l : List α} (h_ne : l ≠ []) :
-    sizeOf l.dropLast < sizeOf l := by
-  have h_concat := List.dropLast_concat_getLast h_ne
-  have : sizeOf l = sizeOf (l.dropLast ++ [l.getLast h_ne]) := by rw [h_concat]
-  rw [this]
-  exact List.sizeOf_lt_append_singleton l.dropLast (l.getLast h_ne)
-
-mutual
-
-/--
-Fold a list of preceding statements (right-to-left) around an accumulator
-expression. Each `if-then` (no else) guard wraps as
-`if cond then lastStmtToExpr(body) else acc`; other statements produce
-`Block [stmt, acc]`.
--/
-def stmtsToExpr (stmts : List StmtExprMd) (acc : StmtExprMd)
-    : StmtExprMd :=
-  match stmts with
-  | [] => acc
-  | s :: rest =>
-    let acc' := stmtsToExpr rest acc
-    match s with
-    | ⟨.IfThenElse cond thenBr none, ssrc⟩ =>
-      ⟨.IfThenElse cond (lastStmtToExpr thenBr) (some acc'), ssrc⟩
-    | _ =>
-      { val := .Block [s, acc'] none, source := none }
-  termination_by (sizeOf stmts, 1)
-
-/--
-Convert the last statement of a block into an expression.
-- `return expr` → `expr`
-- A non-empty block → process last element, fold preceding statements
-- `if cond then A else B` → recurse into both branches
-- Anything else → kept as-is
--/
-def lastStmtToExpr (stmt : StmtExprMd) : StmtExprMd :=
-  match stmt with
-  | ⟨.Return (some val), _⟩ => val
-  | ⟨.Block stmts _, _⟩ =>
-    match h_last : stmts.getLast? with
-    | some last =>
-      have := List.mem_of_getLast? h_last
-      let lastExpr := lastStmtToExpr last
-      let dropped := stmts.dropLast
-      have h : sizeOf stmts.dropLast < sizeOf stmts :=
-        List.sizeOf_dropLast_lt (by intro h; simp [h] at h_last)
-      stmtsToExpr dropped lastExpr
-    | none => stmt
-  | ⟨.IfThenElse cond thenBr (some elseBr), source⟩ =>
-    ⟨.IfThenElse cond (lastStmtToExpr thenBr) (some (lastStmtToExpr elseBr)), source⟩
-  | _ => stmt
-  termination_by (sizeOf stmt, 0)
-  decreasing_by
-    all_goals (simp_all; term_by_mem)
-
-end
-
-/--
-Apply return elimination to a functional procedure's body.
-The entire body is treated as an expression to be converted.
--/
-def eliminateReturnsInExpression (proc : Procedure) : Procedure :=
-  if !proc.isFunctional then proc
-  else
-    match proc.body with
-    | .Transparent bodyExpr =>
-      { proc with body := .Transparent (lastStmtToExpr bodyExpr) }
-    | .Opaque postconds (some impl) modif =>
-      { proc with body := .Opaque postconds (some (lastStmtToExpr impl)) modif }
-    | _ => proc
+/-- Recurse into a statement, applying the guard-return rewrite inside blocks and branches.
+    Returns `Except DiagnosticModel StmtExprMd` so that unsupported statement forms produce
+    a diagnostic instead of panicking. -/
+def removeReturns (stmt : StmtExprMd) : Except DiagnosticModel StmtExprMd :=
+  match _h : stmt.val with
+  | .Return (some expr) => .ok expr
+  | .Block [head] _ => removeReturns head
+  | .Block (head :: tail) label => do
+    let newTail ← removeReturns ⟨.Block tail none, stmt.source⟩
+    let passThrough: StmtExprMd :=
+      let tailList := match newTail.val with
+        | .Block stmts _ => stmts
+        | _ => [newTail]
+      ⟨ .Block (head :: tailList) label, stmt.source ⟩
+    match _hhead : head.val with
+    | .IfThenElse cond thenBr none =>
+      let newThen ← removeReturns thenBr
+      .ok ⟨ .IfThenElse cond newThen newTail, head.source ⟩
+    | .Assign _ _ => .ok passThrough
+    | .Assume _ => .ok passThrough
+    | .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")
+    | _ => .error (diagnosticFromSource head.source
+        s!"unsupported statement {head.val.constructorName} in block head")
+  | .IfThenElse cond thenBr (some elseBr) => do
+      let thenExpr ← removeReturns thenBr
+      let elseExpr ← removeReturns elseBr
+      .ok ⟨ .IfThenElse cond thenExpr (some elseExpr), stmt.source⟩
+  | _ => .error (diagnosticFromSource stmt.source
+      s!"ending a transparent body with a {stmt.val.constructorName} statement is not supported")
+termination_by sizeOf stmt.val
+decreasing_by
+  all_goals
+    simp only [_h, StmtExpr.Block.sizeOf_spec, StmtExpr.IfThenElse.sizeOf_spec,
+      List.cons.sizeOf_spec, List.nil.sizeOf_spec, Option.none.sizeOf_spec,
+      Option.some.sizeOf_spec]
+    try have hhd := AstNode.sizeOf_val_lt head
+    try have htb := AstNode.sizeOf_val_lt thenBr
+    try have heb := AstNode.sizeOf_val_lt elseBr
+    try simp only [_hhead, StmtExpr.IfThenElse.sizeOf_spec, Option.none.sizeOf_spec] at hhd
+    omega
+
+/-- Transform a single procedure by applying the guard-return elimination to its body.
+    Returns the procedure and any diagnostic emitted on failure. -/
+private def eliminateReturnsInExpression (proc : Procedure) : Procedure × List DiagnosticModel :=
+  match proc.body with
+  | .Transparent body =>
+    match removeReturns body with
+    | .ok result => ({ proc with body := .Transparent ⟨.Return result, body.source ⟩ }, [])
+    | .error diag => (proc, [diag])
+  | _ => (proc, [])
 
 public section
 
 /--
-Transform a program by eliminating returns in all functional procedure bodies.
+Transform a program by eliminating returns in all procedure bodies.
 -/
-def mergeAndLiftReturns (program : Program) : Program :=
-  { program with staticProcedures := program.staticProcedures.map eliminateReturnsInExpression }
+def mergeAndLiftReturns (program : Program) : Program × List DiagnosticModel :=
+  let (procs, diags) := program.staticProcedures.foldl (fun (ps, ds) proc =>
+    let (proc', procDiags) := eliminateReturnsInExpression proc
+    (proc' :: ps, ds ++ procDiags)
+  ) ([], [])
+  ({ program with staticProcedures := procs.reverse }, diags)
 
 end -- public section
 
 /-- Pipeline pass: merge and lift returns. -/
-public def mergeAndLiftReturnsPass : LaurelPass where
+public def mergeAndLiftReturnsPass : LoweringPass where
   name := "MergeAndLiftReturns"
   documentation := "Attempts to merge and lift returns so that only a single outer return remains, enabling the procedure to be more easily converted to a functional form."
   needsResolves := true
-  run := fun p _m =>
-    (mergeAndLiftReturns p, [], {})
+  comesBefore := [⟨ eliminateValueInReturnsPass.meta, "Lifts returns with a value, so the value should not yet have been lowered."⟩]
+  run := fun p _m _ =>
+    let (p', diags) := mergeAndLiftReturns p
+    (p', diags, {})
 
 end Laurel
diff --git a/Strata/Languages/Laurel/ModifiesClauses.lean b/Strata/Languages/Laurel/ModifiesClauses.lean
index b5045ff97a..dbe7eef50f 100644
--- a/Strata/Languages/Laurel/ModifiesClauses.lean
+++ b/Strata/Languages/Laurel/ModifiesClauses.lean
@@ -8,6 +8,7 @@ module
 public import Strata.Languages.Laurel.Resolution
 public import Strata.Languages.Laurel.LaurelPass
 import Strata.Languages.Laurel.HeapParameterizationConstants
+import Strata.Languages.Laurel.HeapParameterization
 import Strata.Languages.Laurel.Grammar.AbstractToConcreteTreeTranslator
 import Strata.Languages.Laurel.LaurelTypes
 
@@ -233,19 +234,20 @@ def modifiesClausesTransform (model: SemanticModel) (program : Program) : Progra
 end -- public section
 
 /-- Pipeline pass: filter non-composite modifies clauses. -/
-public def filterNonCompositeModifiesPass : LaurelPass where
+public def filterNonCompositeModifiesPass : LoweringPass where
   name := "FilterNonCompositeModifies"
   documentation := "Filters modifies clauses that refer to non-composite types (e.g. primitives), which cannot be heap-parameterized. Emits a warning for each removed clause. Should run before heap parameterization so that phase remains agnostic to modifies clauses."
-  run := fun p m =>
+  run := fun p m _ =>
     let (p', diags) := filterNonCompositeModifies m p
     (p', diags, {})
 
 /-- Pipeline pass: translate modifies clauses into ensures clauses. -/
-public def modifiesClausesTransformPass : LaurelPass where
+public def modifiesClausesTransformPass : LoweringPass where
   name := "ModifiesClausesTransform"
   documentation := "Translates modifies clauses into additional ensures clauses. The modifies clause of a procedure is translated into a quantified assertion that states objects not mentioned in the modifies clause have their field values preserved between the input and output heap."
   needsResolves := true
-  run := fun p m =>
+  comesAfter := [⟨ heapParameterizationPass.meta, "the modifies pass refers to several types and variables introduced by heap parameterization: Composite, Field, $heap_in, $heap."⟩]
+  run := fun p m _ =>
     let (p', diags) := modifiesClausesTransform m p
     (p', diags, {})
 
diff --git a/Strata/Languages/Laurel/PushOldInward.lean b/Strata/Languages/Laurel/PushOldInward.lean
index 6fd6119023..c9db47123a 100644
--- a/Strata/Languages/Laurel/PushOldInward.lean
+++ b/Strata/Languages/Laurel/PushOldInward.lean
@@ -6,6 +6,7 @@
 module
 
 public import Strata.Languages.Laurel.MapStmtExpr
+public import Strata.Languages.Laurel.LaurelPass
 
 /-!
 # Push `Old` Inward
@@ -70,12 +71,19 @@ def transformProcedurePushOld (proc : Procedure) : PushOldM Procedure := do
 
 /-- Push every `StmtExpr.Old` inward until it immediately wraps an inout
     variable. Returns the rewritten program and any warnings emitted. -/
-@[expose]
 def pushOldInward (program : Program) : Program × List DiagnosticModel :=
   let (program', finalState) :=
     (program.staticProcedures.mapM transformProcedurePushOld).run {}
   ({ program with staticProcedures := program' }, finalState.diagnostics)
 
+/-- Pipeline pass: translate modifies clauses into ensures clauses. -/
+public def pushOldInwardPass : LoweringPass where
+  name := "pushOldInward"
+  documentation := "Distributes `old(...)` over its subexpressions until each `old` immediately wraps an inout variable. Warns on `old(e)` where `e` mentions no inout parameter and on nested `old(old(...))`."
+  run := fun p _ _ =>
+    let (p', diags) := pushOldInward p
+    (p', diags, {})
+
 end -- public section
 end Laurel
 end Strata
diff --git a/Strata/Languages/Laurel/Resolution.lean b/Strata/Languages/Laurel/Resolution.lean
index 96af7cab53..a3e3e5090d 100644
--- a/Strata/Languages/Laurel/Resolution.lean
+++ b/Strata/Languages/Laurel/Resolution.lean
@@ -6,8 +6,8 @@
 module
 
 public import Strata.Languages.Laurel.LaurelAST
+public import Strata.Languages.Laurel.UnorderedCore
 public import Strata.Languages.Laurel.Grammar.AbstractToConcreteTreeTranslator
-public import Strata.Languages.Laurel.TransparencyPass
 import Strata.Util.Tactics
 public import Strata.Languages.Laurel.SemanticModel
 public import Strata.Languages.Laurel.LaurelTypes
@@ -2579,8 +2579,8 @@ def resolveOutputParameter (inputNames : List String) (param : Parameter) : Reso
   else
     resolveParameter param
 
-/-- Resolve a procedure body by synthesizing its impl block (if any).
-    Bodies without an impl block (`Abstract`, `External`) resolve
+/-- Resolve a procedure body by synthesizing its body (if any).
+    Bodies without an body (`Abstract`, `External`) resolve
     postconditions only. -/
 def resolveBody (body : Body) : ResolveM Body := do
   match body with
@@ -2632,10 +2632,12 @@ def resolveProcedure (proc : Procedure) : ResolveM Procedure := do
     -- (e.g. destructive assignments) inside a transparent body. So there is
     -- no transparent-body rejection here, unlike `resolveInstanceProcedure`.
     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',
              body := body' }
 
 /-- Resolve a field: define its name under the qualified key (OwnerType.fieldName) and resolve its type. -/
@@ -2667,16 +2669,14 @@ def resolveInstanceProcedure (typeName : Identifier) (proc : Procedure) : Resolv
     -- See `resolveProcedure` for the rationale on `bodyLabel`.
     let body' ← withLabel (some bodyLabel) <| resolveBody proc.body
     modify fun s => { s with answerType := savedAnswer }
-    if !proc.isFunctional && body'.isTransparent && !proc.name.text.any (· == '$') then
-      let diag := diagnosticFromSource proc.name.source
-        s!"transparent statement bodies are not supported. Add 'opaque' to make the procedure opaque"
-      modify fun s => { s with errors := s.errors.push diag }
     let invokeOn' ← proc.invokeOn.mapM resolveStmtExpr
     modify fun s => { s with instanceTypeName := savedInstType }
+    let axioms' ← proc.axioms.mapM resolveStmtExpr
     return { name := procName', inputs := inputs', outputs := outputs',
              isFunctional := proc.isFunctional,
              preconditions := pres', decreases := dec',
              invokeOn := invokeOn',
+             axioms := axioms',
              body := body' }
 
 /-- Resolve a type definition. -/
@@ -2730,7 +2730,12 @@ def resolveTypeDefinition (td : TypeDefinition) : ResolveM TypeDefinition := do
         -- parameter's own name should stay unqualified.
         let destructorId := { p.name with uniqueId := resolved.uniqueId }
         return ⟨ destructorId, ty' ⟩
-      return { name := ctorName', args := args' : DatatypeConstructor }
+      -- Resolve the tester name so its uniqueId is set.
+      let testerResolved ← resolveRef (dt.testerName ctor)
+      let testerName' := { ctor.testerName with
+        text := testerResolved.text
+        uniqueId := testerResolved.uniqueId }
+      return { name := ctorName', args := args', testerName := testerName' : DatatypeConstructor }
     return .Datatype { name := dtName', typeArgs := dt.typeArgs, constructors := ctors' }
   | .Alias ta =>
     let target' ← resolveHighType ta.target
@@ -2746,6 +2751,28 @@ def resolveConstant (c : Constant) : ResolveM Constant := do
 
 /-! ## Phase 2: Build refToDef map from the resolved program -/
 
+/-- Generate a virtual tester procedure for a single constructor of a datatype.
+    The tester takes a single argument of the datatype's type and returns `bool`.
+    Used during resolution to synthesize the scope entry for tester calls
+    (e.g. `IntList..isNil(x)`) without requiring a separate AST pass. -/
+private def mkTesterProcedure (dt : DatatypeDefinition) (ctor : DatatypeConstructor) : Procedure :=
+  let tName := dt.testerName ctor
+  let inputParam : Parameter := {
+    name := mkId "value"
+    type := { val := .UserDefined dt.name, source := none }
+  }
+  let outputParam : Parameter := {
+    name := mkId "$result"
+    type := { val := .TBool, source := none }
+  }
+  { name := mkId tName
+    inputs := [inputParam]
+    outputs := [outputParam]
+    preconditions := []
+    decreases := none
+    isFunctional := true
+    body := .External }
+
 /-- Insert a definition into the refToDef map using the ID already on the identifier. -/
 private def register (map : Std.HashMap Nat ResolvedNode) (iden : Identifier) (node : ResolvedNode)
     : Std.HashMap Nat ResolvedNode :=
@@ -2883,6 +2910,9 @@ private def collectTypeDefinition (map : Std.HashMap Nat ResolvedNode) (td : Typ
     let map := register map dt.name (.datatypeDefinition dt)
     dt.constructors.foldl (fun map ctor =>
       let map := register map ctor.name (.datatypeConstructor dt.name ctor)
+      -- Register the tester function in the refToDef map.
+      let testerProc := mkTesterProcedure dt ctor
+      let map := register map ctor.testerName (.staticProcedure testerProc)
       ctor.args.foldl (fun map p =>
         -- The constructor parameter's `uniqueId` (set by `resolveTypeDefinition`)
         -- is the shared uniqueId of the safe/unsafe destructor scope entries,
@@ -3063,13 +3093,11 @@ private def preRegisterTopLevel (program : Program) : ResolveM Unit := do
     | .Datatype dt =>
       let _ ← defineNameCheckDup dt.name (.datatypeDefinition dt)
       for ctor in dt.constructors do
-        -- Register the tester override first; the second call reuses the
-        -- returned Identifier (now carrying a uniqueId) so the unprefixed
-        -- constructor name and the `TypeName..isCtor` tester name resolve to
-        -- the same uniqueId, which `buildRefToDef` in turn maps to
-        -- `.datatypeConstructor`.
-        let ctorName ← defineNameCheckDup ctor.name (.datatypeConstructor dt.name ctor) (some (dt.testerName ctor))
-        let _ ← defineNameCheckDup ctorName (.datatypeConstructor dt.name ctor)
+        let _ ← defineNameCheckDup ctor.name (.datatypeConstructor dt.name ctor)
+        -- Register the tester function (e.g. `IntList..isNil`) as a static procedure.
+        let testerProc := mkTesterProcedure dt ctor
+        let _ ← defineNameCheckDup (mkId (dt.testerName ctor))
+          (.staticProcedure testerProc) (some (dt.testerName ctor))
         for p in ctor.args do
           -- Same chaining trick for the safe and unsafe destructor names: both
           -- point to the same uniqueId so `IntList..head` and `IntList..head!`
@@ -3155,10 +3183,10 @@ but they are because certain type references have incorrectly not been updated.
 public def resolveUnorderedCore (uc : UnorderedCoreWithLaurelTypes)
     (existingModel : Option SemanticModel := none)
     (additionalTypes : List TypeDefinition := [])
-    : UnorderedCoreWithLaurelTypes × SemanticModel :=
+    : UnorderedCoreWithLaurelTypes × SemanticModel × Array DiagnosticModel :=
   let fnProgram := unorderedCoreToProgram uc additionalTypes
   let fnResolveResult := resolve fnProgram existingModel
-  (fromResolvedProgram fnResolveResult.program, fnResolveResult.model)
+  (fromResolvedProgram fnResolveResult.program, fnResolveResult.model, fnResolveResult.errors)
 
 end -- public section
 end Strata.Laurel
diff --git a/Strata/Languages/Laurel/TransparencyPass.lean b/Strata/Languages/Laurel/TransparencyPass.lean
index b4b59dcec4..c44751ff96 100644
--- a/Strata/Languages/Laurel/TransparencyPass.lean
+++ b/Strata/Languages/Laurel/TransparencyPass.lean
@@ -7,6 +7,8 @@ module
 
 public import Strata.Languages.Laurel.MapStmtExpr
 public import Strata.Languages.Laurel.LaurelAST
+public import Strata.Languages.Laurel.LaurelPass
+public import Strata.Languages.Laurel.CoreGroupingAndOrdering
 import Strata.Languages.Laurel.Grammar.AbstractToConcreteTreeTranslator
 import Strata.DL.Lambda.TypeFactory
 
@@ -28,18 +30,6 @@ namespace Strata.Laurel
 
 public section
 
-/--
-An intermediate representation produced by the transparency pass.
-Functions are pure computational procedures (suffixed `$asFunction`);
-coreProcedures are the original procedures with any free postconditions
-embedded in their `Body.Opaque` postcondition lists.
--/
-public structure UnorderedCoreWithLaurelTypes where
-  functions : List Procedure
-  coreProcedures : List Procedure
-  datatypes : List DatatypeDefinition
-  constants : List Constant
-
 /-- Deep traversal that strips all Assert and Assume nodes from a StmtExpr tree.
     Assert/Assume nodes are replaced with `LiteralBool true`, and Block nodes
     are collapsed by filtering out trivial `LiteralBool true` leftovers. -/
@@ -84,6 +74,35 @@ private def rewriteCallsToFunctional (asFunctionNames : Std.HashSet String) (exp
     | .PrimitiveOp operator arguments _ => ⟨ .PrimitiveOp operator arguments true, e.source⟩
     | _ => e) expr
 
+/-- Rewrite quantifier bodies like function bodies: strip assert/assume and
+    rewrite calls to their `$asFunction` variants. This ensures that calls
+    inside quantifiers (e.g. in modifies frame conditions) reference the
+    pure functional version and are not treated as imperative by later passes. -/
+private def rewriteQuantifierBodies (nonExternalNames : Std.HashSet String) (expr : StmtExprMd) : StmtExprMd :=
+  mapStmtExpr (fun e =>
+    match e.val with
+    | .Quantifier mode param trigger body =>
+      let body' := rewriteCallsToFunctional nonExternalNames (stripAssertAssume body)
+      let trigger' := trigger.map (rewriteCallsToFunctional nonExternalNames)
+      ⟨.Quantifier mode param trigger' body', e.source⟩
+    | _ => e) expr
+
+/-- Apply quantifier body rewriting to all postconditions and the implementation
+    of a procedure. -/
+private def rewriteQuantifierBodiesInProc (nonExternalNames : Std.HashSet String) (proc : Procedure) : Procedure :=
+  let rewrite := rewriteQuantifierBodies nonExternalNames
+  match proc.body with
+  | .Opaque postconds impl modif =>
+    let postconds' := postconds.map fun c => { c with condition := rewrite c.condition }
+    let impl' := impl.map rewrite
+    { proc with body := .Opaque postconds' impl' modif }
+  | .Transparent body =>
+    { proc with body := .Transparent (rewrite body) }
+  | .Abstract postconds =>
+    let postconds' := postconds.map fun c => { c with condition := rewrite c.condition }
+    { proc with body := .Abstract postconds' }
+  | .External => proc
+
 /-- Build a free postcondition equating the procedure's output to its functional version.
     For a procedure `foo(a, b) returns (r)`, produces:
       `r == foo$asFunction(a, b)` -/
@@ -100,12 +119,15 @@ private def mkFreePostcondition (proc : Procedure) : StmtExprMd :=
     If the procedure is transparent, include a functional body.
     Otherwise the function is opaque. -/
 private def mkFunctionCopy (asFunctionNames : Std.HashSet String) (proc : Procedure) : Procedure :=
-  let funcName := { proc.name with text := proc.name.text ++ "$asFunction", uniqueId := none }
+  let hasProcedureTwin := asFunctionNames.contains proc.name.text
+  let funcName := if hasProcedureTwin then
+    { proc.name with text := proc.name.text ++ "$asFunction", uniqueId := none }
+    else proc.name
   let body := match proc.body with
-    | .Transparent b => .Transparent (rewriteCallsToFunctional asFunctionNames (stripAssertAssume b))
-    | .Opaque _ _ _ => .Opaque [] none []
+    | .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, preconditions := [] }
+  { proc with name := funcName, isFunctional := true, body := body }
 
 /-- Append a free postcondition to a procedure's body postconditions.
     For Opaque and Abstract bodies, the free condition is appended to the
@@ -126,46 +148,31 @@ 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 transparencyPass (program : Program) : UnorderedCoreWithLaurelTypes :=
-  let (skipped, notSkipped) := program.staticProcedures.partition (fun p => p.body.isExternal ||
-    -- Skip functions until we introduce a contract pass,
-    -- which enables lifting procedure calls from contracts
-    p.isFunctional)
-  let asFunctionNames : Std.HashSet String := notSkipped.foldl (fun s p => s.insert p.name.text) {}
-  let asFunctions := notSkipped.map (mkFunctionCopy asFunctionNames)
-
-  -- External procedures get a plain function copy (they have no $asFunction version)
-  let (skippedFunctions, skippedProcedures) := skipped.partition (fun p => p.isFunctional)
-  let functions := skippedFunctions ++ asFunctions
-  let coreProcedures := notSkipped.map fun p =>
-    let freePostcondition := mkFreePostcondition p
-    let p := addFreePostcondition p freePostcondition
-    { p with isFunctional := false }
+def createFunctionsForTransparentBodies (program : Program) : UnorderedCoreWithLaurelTypes :=
+  let (toUpdate, _) := program.staticProcedures.partition (fun p => !p.body.isExternal && !p.isFunctional)
+  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 := rewriteQuantifierBodiesInProc toUpdateNames proc
+    addFreePostcondition proc freePostcondition
   let datatypes := program.types.filterMap fun td => match td with
     | .Datatype dt => some dt
     | _ => none
-  let procs: List Procedure := skippedProcedures ++ coreProcedures
-  { functions, coreProcedures := procs, datatypes, constants := program.constants }
+  { functions, coreProcedures, datatypes, constants := program.constants }
 
-open Std (Format ToFormat)
-
-def formatUnorderedCoreWithLaurelTypes (p : UnorderedCoreWithLaurelTypes) : Format :=
-  let datatypeFmts := p.datatypes.map ToFormat.format
-  let constantFmts := p.constants.map ToFormat.format
-  let functionFmts := p.functions.map ToFormat.format
-  let procFmts := p.coreProcedures.map ToFormat.format
-  Format.joinSep (datatypeFmts ++ constantFmts ++ functionFmts ++ procFmts) "\n\n"
-
-instance : ToFormat UnorderedCoreWithLaurelTypes where
-  format := formatUnorderedCoreWithLaurelTypes
+public def transparencyPass : LaurelPass Laurel.Program UnorderedCoreWithLaurelTypes where
+  name := "TransparencyPass"
+  comesBefore := [⟨ orderingPass.meta, "Transparency pass creates functions that are not ordered" ⟩]
+  documentation := "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"
+  run := fun p _ _ =>
+    (createFunctionsForTransparentBodies p, [], {})
 
 end -- public section
 end Strata.Laurel
diff --git a/Strata/Languages/Laurel/TypeAliasElim.lean b/Strata/Languages/Laurel/TypeAliasElim.lean
index 36c5426613..65a3a462e2 100644
--- a/Strata/Languages/Laurel/TypeAliasElim.lean
+++ b/Strata/Languages/Laurel/TypeAliasElim.lean
@@ -61,10 +61,10 @@ public def typeAliasElim (_model : SemanticModel) (program : Program) : Program
   { program with types := program.types.filter fun | .Alias _ => false | _ => true }
 
 /-- Pipeline pass: type alias elimination. -/
-public def typeAliasElimPass : LaurelPass where
+public def typeAliasElimPass : LoweringPass where
   name := "TypeAliasElim"
   documentation := "Eliminates type aliases by replacing all UserDefined references to alias names with their resolved target types. Chained aliases are resolved transitively. Alias entries are removed from the type list."
   needsResolves := true
-  run := fun p m => (typeAliasElim m p, [], {})
+  run := fun p m _ => (typeAliasElim m p, [], {})
 
 end Strata.Laurel
diff --git a/Strata/Languages/Laurel/TypeHierarchy.lean b/Strata/Languages/Laurel/TypeHierarchy.lean
index 7ada70ac30..0414298e6a 100644
--- a/Strata/Languages/Laurel/TypeHierarchy.lean
+++ b/Strata/Languages/Laurel/TypeHierarchy.lean
@@ -10,6 +10,7 @@ import Strata.Util.Tactics
 public import Strata.Languages.Laurel.LaurelPass
 public import Strata.Languages.Laurel.Resolution
 import Std.Tactic.BVDecide.Normalize.Prop
+import Strata.Languages.Laurel.HeapParameterization
 import Strata.Languages.Laurel.LaurelTypes
 import Strata.Languages.Laurel.MapStmtExpr
 
@@ -187,11 +188,12 @@ def typeHierarchyTransform (model: SemanticModel) (program : Program) : Program
   mapProgramHighTypes (compositeRefToComposite compositeSet) transformed
 
 /-- Pipeline pass: type hierarchy transform. -/
-public def typeHierarchyTransformPass : LaurelPass where
+public def typeHierarchyTransformPass : LoweringPass where
   name := "TypeHierarchyTransform"
   documentation := "Encodes the object-oriented type hierarchy (inheritance, dynamic dispatch, type tests, and casts) into explicit operations on a flat representation. Composite types with parents are flattened, and dynamic dispatch is resolved through type-test chains."
   needsResolves := false -- Only resolve again after completing HeapParam, ModifiesClauses and TypeHierarchy. These are logically one pass.
-  run := fun p m =>
+  comesAfter := [⟨ heapParameterizationPass.meta, "the type hierarchy pass modifies the 'Composite' datatype that is introduced by this pass."⟩]
+  run := fun p m _ =>
     (typeHierarchyTransform m p, [], {})
 
 end Strata.Laurel
diff --git a/Strata/Languages/Laurel/UnorderedCore.lean b/Strata/Languages/Laurel/UnorderedCore.lean
new file mode 100644
index 0000000000..97c070902b
--- /dev/null
+++ b/Strata/Languages/Laurel/UnorderedCore.lean
@@ -0,0 +1,34 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+module
+public import Strata.Languages.Laurel.LaurelAST
+import Strata.Languages.Laurel.Grammar.AbstractToConcreteTreeTranslator
+
+namespace Strata.Laurel
+
+open Std (Format ToFormat)
+/--
+An intermediate representation produced by the transparency pass.
+Functions are pure computational procedures (suffixed `$asFunction`);
+coreProcedures are the original procedures with any free postconditions
+embedded in their `Body.Opaque` postcondition lists.
+-/
+public structure UnorderedCoreWithLaurelTypes where
+  functions : List Procedure
+  coreProcedures : List Procedure
+  datatypes : List DatatypeDefinition
+  constants : List Constant
+
+public def formatUnorderedCoreWithLaurelTypes (p : UnorderedCoreWithLaurelTypes) : Format :=
+  let datatypeFmts := p.datatypes.map ToFormat.format
+  let constantFmts := p.constants.map ToFormat.format
+  let functionFmts := p.functions.map ToFormat.format
+  let procFmts := p.coreProcedures.map ToFormat.format
+  Format.joinSep (datatypeFmts ++ constantFmts ++ functionFmts ++ procFmts) "\n\n"
+
+public instance : ToFormat UnorderedCoreWithLaurelTypes where
+  format := formatUnorderedCoreWithLaurelTypes
diff --git a/StrataPython/StrataPython/PySpecPipeline.lean b/StrataPython/StrataPython/PySpecPipeline.lean
index 13e376c2ab..02322f079b 100644
--- a/StrataPython/StrataPython/PySpecPipeline.lean
+++ b/StrataPython/StrataPython/PySpecPipeline.lean
@@ -404,9 +404,9 @@ public def translateCombinedLaurelWithLowered (combined : Laurel.Program)
 
 /-- Translate a combined Laurel program to Core and prepend the full
     runtime prelude. -/
-public def translateCombinedLaurel (combined : Laurel.Program)
+public def translateCombinedLaurel (combined : Laurel.Program) (keepAllFilesPrefix : Option String := none)
     : IO (Option Core.Program × List DiagnosticModel) := do
-  let (coreOption, errors, _, _) ← translateCombinedLaurelWithLowered combined
+  let (coreOption, errors, _, _) ← translateCombinedLaurelWithLowered combined keepAllFilesPrefix
   return (coreOption, errors)
 
 /-- Run the pyAnalyzeLaurel pipeline: read a Python Ion program,
diff --git a/StrataPython/StrataPython/PythonToLaurel.lean b/StrataPython/StrataPython/PythonToLaurel.lean
index 199963fa40..c01919b418 100644
--- a/StrataPython/StrataPython/PythonToLaurel.lean
+++ b/StrataPython/StrataPython/PythonToLaurel.lean
@@ -2063,7 +2063,7 @@ partial def translateStmt (ctx : TranslationContext) (s : stmt SourceRange)
             let assumeInRange := mkStmtExprMdWithLoc (.Assume inRangeExpr) md
             pure [assumeTypeInt, assumeInRange]
           | _ =>
-            let targetInIter := mkStmtExprMd (.StaticCall "PIn" [targetVar, iterExpr])
+            let targetInIter := mkStmtExprMdWithLoc (.StaticCall "PIn" [targetVar, iterExpr]) md
             let assumeInStmt := mkStmtExprMdWithLoc (.Assume (Any_to_bool targetInIter)) md
             pure [assumeInStmt]
       | _ => pure []
diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_class_empty.expected b/StrataPython/StrataPythonTest/expected_laurel/test_class_empty.expected
index aab04f3a0d..7f98693936 100644
--- a/StrataPython/StrataPythonTest/expected_laurel/test_class_empty.expected
+++ b/StrataPython/StrataPythonTest/expected_laurel/test_class_empty.expected
@@ -1,4 +1,4 @@
-test_class_empty.py(5, 4): ✅ pass - callElimAssert_requires_4
+test_class_empty.py(5, 4): ✅ pass - precondition
 test_class_empty.py(6, 4): ✅ pass - empty class instantiated
 DETAIL: 2 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_class_field_init.expected b/StrataPython/StrataPythonTest/expected_laurel/test_class_field_init.expected
index 7cb1e2fc89..4757a64ef8 100644
--- a/StrataPython/StrataPythonTest/expected_laurel/test_class_field_init.expected
+++ b/StrataPython/StrataPythonTest/expected_laurel/test_class_field_init.expected
@@ -1,2 +1,4 @@
-DETAIL: 0 passed, 0 failed, 0 inconclusive
+test_class_field_init.py(20, 4): ✔️ always true if reached - (CircularBuffer@__init__ requires) Type constraint of size
+test_class_field_init.py(20, 4): ✔️ always true if reached - (CircularBuffer@__init__ requires) Type constraint of name
+DETAIL: 2 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_class_field_use.expected b/StrataPython/StrataPythonTest/expected_laurel/test_class_field_use.expected
index 0caaf75c9f..29a689ea2c 100644
--- a/StrataPython/StrataPythonTest/expected_laurel/test_class_field_use.expected
+++ b/StrataPython/StrataPythonTest/expected_laurel/test_class_field_use.expected
@@ -1,5 +1,6 @@
+test_class_field_use.py(13, 4): ✔️ always true if reached - (CircularBuffer@__init__ requires) Type constraint of n
 test_class_field_use.py(14, 4): ✔️ always true if reached - Check PMul exception
 test_class_field_use.py(14, 4): ✔️ always true if reached - assert(302)
 test_class_field_use.py(15, 4): ✔️ always true if reached - Doubling of buffer did not work
-DETAIL: 3 passed, 0 failed, 0 inconclusive
+DETAIL: 4 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_class_methods.expected b/StrataPython/StrataPythonTest/expected_laurel/test_class_methods.expected
index 36c53a8361..f0601e776e 100644
--- a/StrataPython/StrataPythonTest/expected_laurel/test_class_methods.expected
+++ b/StrataPython/StrataPythonTest/expected_laurel/test_class_methods.expected
@@ -1,11 +1,17 @@
-test_class_methods.py(34, 4): ✔️ always true if reached - main_assert(471)_13
+test_class_methods.py(34, 4): ✔️ always true if reached - (Account@__init__ requires) Type constraint of owner
+test_class_methods.py(34, 4): ✔️ always true if reached - (Account@__init__ requires) Type constraint of balance
+test_class_methods.py(34, 4): ✔️ always true if reached - main_assert(471)_32
 test_class_methods.py(34, 4): ✔️ always true if reached - get_owner should return Alice
-test_class_methods.py(34, 4): ✔️ always true if reached - main_assert(564)_15
+test_class_methods.py(34, 4): ✔️ always true if reached - main_assert(564)_35
 test_class_methods.py(34, 4): ✔️ always true if reached - get_balance should return 100
-test_class_methods.py(34, 4): ✔️ always true if reached - main_assert(678)_17
+test_class_methods.py(34, 4): ✔️ always true if reached - (Account@set_balance requires) Type constraint of amount
+test_class_methods.py(34, 4): ✔️ always true if reached - main_assert(678)_40
 test_class_methods.py(34, 4): ✔️ always true if reached - set_balance should update balance
+test_class_methods.py(34, 4): ✔️ always true if reached - (Origin_test_helper_procedure_Requires)req_name_is_foo
+test_class_methods.py(34, 4): ✔️ always true if reached - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str
+test_class_methods.py(34, 4): ✔️ always true if reached - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
 test_class_methods.py(31, 4): ✔️ always true if reached - assert_name_is_foo
 test_class_methods.py(31, 4): ✔️ always true if reached - assert_opt_name_none_or_str
 test_class_methods.py(31, 4): ✔️ always true if reached - assert_opt_name_none_or_bar
-DETAIL: 9 passed, 0 failed, 0 inconclusive
+DETAIL: 15 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_class_mixed_init.expected b/StrataPython/StrataPythonTest/expected_laurel/test_class_mixed_init.expected
index e0d77a61a6..1966e6aa7b 100644
--- a/StrataPython/StrataPythonTest/expected_laurel/test_class_mixed_init.expected
+++ b/StrataPython/StrataPythonTest/expected_laurel/test_class_mixed_init.expected
@@ -1,4 +1,6 @@
+test_class_mixed_init.py(19, 0): ✔️ always true if reached - (WithInit@__init__ requires) Type constraint of x
 test_class_mixed_init.py(19, 0): ✔️ always true if reached - class with init
+test_class_mixed_init.py(19, 0): ✔️ always true if reached - precondition
 test_class_mixed_init.py(19, 0): ✔️ always true if reached - class with init
-DETAIL: 2 passed, 0 failed, 0 inconclusive
+DETAIL: 4 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_class_no_init.expected b/StrataPython/StrataPythonTest/expected_laurel/test_class_no_init.expected
index 7228247375..a55c76cfe4 100644
--- a/StrataPython/StrataPythonTest/expected_laurel/test_class_no_init.expected
+++ b/StrataPython/StrataPythonTest/expected_laurel/test_class_no_init.expected
@@ -1,4 +1,4 @@
-test_class_no_init.py(5, 4): ✅ pass - callElimAssert_requires_4
+test_class_no_init.py(5, 4): ✅ pass - precondition
 test_class_no_init.py(6, 4): ❓ unknown - class without __init__
 DETAIL: 1 passed, 0 failed, 1 inconclusive
 RESULT: Inconclusive
diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_class_no_init_multi_field.expected b/StrataPython/StrataPythonTest/expected_laurel/test_class_no_init_multi_field.expected
index 3dbe40b3b6..13ba7f459b 100644
--- a/StrataPython/StrataPythonTest/expected_laurel/test_class_no_init_multi_field.expected
+++ b/StrataPython/StrataPythonTest/expected_laurel/test_class_no_init_multi_field.expected
@@ -1,4 +1,4 @@
-test_class_no_init_multi_field.py(7, 4): ✅ pass - callElimAssert_requires_4
+test_class_no_init_multi_field.py(7, 4): ✅ pass - precondition
 test_class_no_init_multi_field.py(8, 4): ✅ pass - class with multiple annotated fields no init
 DETAIL: 2 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_class_no_init_with_method.expected b/StrataPython/StrataPythonTest/expected_laurel/test_class_no_init_with_method.expected
index 29b6682a29..93f5036c2d 100644
--- a/StrataPython/StrataPythonTest/expected_laurel/test_class_no_init_with_method.expected
+++ b/StrataPython/StrataPythonTest/expected_laurel/test_class_no_init_with_method.expected
@@ -1,5 +1,5 @@
 test_class_no_init_with_method.py(4, 23): ❓ unknown - (WithMethod@get_x ensures) Return type constraint
-test_class_no_init_with_method.py(8, 4): ✅ pass - callElimAssert_requires_4
+test_class_no_init_with_method.py(8, 4): ✅ pass - precondition
 test_class_no_init_with_method.py(9, 4): ✅ pass - class with method but no __init__
 DETAIL: 2 passed, 0 failed, 1 inconclusive
 RESULT: Inconclusive
diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_class_with_methods.expected b/StrataPython/StrataPythonTest/expected_laurel/test_class_with_methods.expected
index 1085e02e58..3f5ddaf665 100644
--- a/StrataPython/StrataPythonTest/expected_laurel/test_class_with_methods.expected
+++ b/StrataPython/StrataPythonTest/expected_laurel/test_class_with_methods.expected
@@ -1,9 +1,15 @@
-test_class_with_methods.py(32, 4): ✔️ always true if reached - main_assert(484)_12
+test_class_with_methods.py(32, 4): ✔️ always true if reached - (DataStore@__init__ requires) Type constraint of name
+test_class_with_methods.py(32, 4): ✔️ always true if reached - (DataStore@add requires) Type constraint of amount
+test_class_with_methods.py(32, 4): ✔️ always true if reached - (DataStore@add requires) Type constraint of amount
+test_class_with_methods.py(32, 4): ✔️ always true if reached - main_assert(484)_34
 test_class_with_methods.py(32, 4): ✔️ always true if reached - get_count should return 30
-test_class_with_methods.py(32, 4): ✔️ always true if reached - main_assert(569)_14
+test_class_with_methods.py(32, 4): ✔️ always true if reached - main_assert(569)_37
 test_class_with_methods.py(32, 4): ✔️ always true if reached - get_name should return mystore
+test_class_with_methods.py(32, 4): ✔️ always true if reached - (Origin_test_helper_procedure_Requires)req_name_is_foo
+test_class_with_methods.py(32, 4): ✔️ always true if reached - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str
+test_class_with_methods.py(32, 4): ✔️ always true if reached - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
 test_class_with_methods.py(29, 4): ✔️ always true if reached - assert_name_is_foo
 test_class_with_methods.py(29, 4): ✔️ always true if reached - assert_opt_name_none_or_str
 test_class_with_methods.py(29, 4): ✔️ always true if reached - assert_opt_name_none_or_bar
-DETAIL: 7 passed, 0 failed, 0 inconclusive
+DETAIL: 13 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_deep_inline.expected b/StrataPython/StrataPythonTest/expected_laurel/test_deep_inline.expected
index eac560309d..bc3395d77d 100644
--- a/StrataPython/StrataPythonTest/expected_laurel/test_deep_inline.expected
+++ b/StrataPython/StrataPythonTest/expected_laurel/test_deep_inline.expected
@@ -1,11 +1,15 @@
+test_deep_inline.py(21, 4): ✔️ always true if reached - (triple_apply requires) Type constraint of x
+test_deep_inline.py(15, 4): ✔️ always true if reached - (double_inc requires) Type constraint of x
+test_deep_inline.py(10, 4): ✔️ always true if reached - (inc requires) Type constraint of x
 test_deep_inline.py(6, 4): ✔️ always true if reached - Check PAdd exception
-test_deep_inline.py(10, 4): ✔️ always true if reached - double_inc_assert(135)_35
+test_deep_inline.py(10, 4): ✔️ always true if reached - double_inc_assert(135)_54
 test_deep_inline.py(10, 4): ✔️ always true if reached - Check PMul exception
-test_deep_inline.py(15, 4): ✔️ always true if reached - triple_apply_assert(206)_17
+test_deep_inline.py(15, 4): ✔️ always true if reached - triple_apply_assert(206)_27
+test_deep_inline.py(15, 4): ✔️ always true if reached - (inc requires) Type constraint of x
 test_deep_inline.py(11, 4): ✔️ always true if reached - Check PAdd exception
-test_deep_inline.py(15, 4): ✔️ always true if reached - triple_apply_assert(233)_18
-test_deep_inline.py(21, 4): ✔️ always true if reached - main_assert(279)_5
+test_deep_inline.py(15, 4): ✔️ always true if reached - triple_apply_assert(233)_30
+test_deep_inline.py(21, 4): ✔️ always true if reached - main_assert(279)_9
 test_deep_inline.py(21, 4): ✔️ always true if reached - triple_apply(3) should be 9
 test_deep_inline.py(21, 4): ✖️ always false if reached - triple_apply(3) should not be 10
-DETAIL: 8 passed, 1 failed, 0 inconclusive
+DETAIL: 12 passed, 1 failed, 0 inconclusive
 RESULT: Failures found
diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_havoc_callee_after_hole_call.expected b/StrataPython/StrataPythonTest/expected_laurel/test_havoc_callee_after_hole_call.expected
index 9a320c707c..85efc6288d 100644
--- a/StrataPython/StrataPythonTest/expected_laurel/test_havoc_callee_after_hole_call.expected
+++ b/StrataPython/StrataPythonTest/expected_laurel/test_havoc_callee_after_hole_call.expected
@@ -2,9 +2,10 @@ test_havoc_callee_after_hole_call.py(8, 0): ❓ unknown - expected unknown becau
 test_havoc_callee_after_hole_call.py(12, 0): ❓ unknown - expected unknown because xs should be havocked
 test_havoc_callee_after_hole_call.py(16, 0): ✔️ always true if reached - chained call: receiver not havocked (chained attribute is not a Name)
 test_havoc_callee_after_hole_call.py(20, 0): ✔️ always true if reached - unrelated variable: nothing should be havocked
+test_havoc_callee_after_hole_call.py(22, 0): ✔️ always true if reached - (MyClass@__init__ requires) Type constraint of n
 test_havoc_callee_after_hole_call.py(25, 0): ✔️ always true if reached - composite arg: heap not havocked (out of scope)
 test_havoc_callee_after_hole_call.py(30, 0): ❓ unknown - expected unknown because argument locals should be havocked
 test_havoc_callee_after_hole_call.py(36, 0): ❓ unknown - assume_assume(1193)_calls_PIn_0
 test_havoc_callee_after_hole_call.py(37, 4): ✔️ always true if reached - for-loop over unmodeled iterator should not crash
-DETAIL: 4 passed, 0 failed, 4 inconclusive
+DETAIL: 5 passed, 0 failed, 4 inconclusive
 RESULT: Inconclusive
diff --git a/StrataPython/StrataPythonTest/expected_laurel/test_with_statement.expected b/StrataPython/StrataPythonTest/expected_laurel/test_with_statement.expected
index c73e76d8cb..8948ea9e4e 100644
--- a/StrataPython/StrataPythonTest/expected_laurel/test_with_statement.expected
+++ b/StrataPython/StrataPythonTest/expected_laurel/test_with_statement.expected
@@ -1,9 +1,13 @@
+test_with_statement.py(16, 4): ✔️ always true if reached - (Resource@__init__ requires) Type constraint of n
 test_with_statement.py(17, 4): ✔️ always true if reached - assert(364)
 test_with_statement.py(20, 4): ✔️ always true if reached - assert(426)
+test_with_statement.py(23, 4): ✔️ always true if reached - (Resource@__init__ requires) Type constraint of n
 test_with_statement.py(25, 8): ✔️ always true if reached - assert(525)
 test_with_statement.py(26, 8): ✔️ always true if reached - assert(558)
+test_with_statement.py(29, 4): ✔️ always true if reached - (Resource@__init__ requires) Type constraint of n
+test_with_statement.py(30, 4): ✔️ always true if reached - (Resource@__init__ requires) Type constraint of n
 test_with_statement.py(32, 21): ✔️ always true if reached - Check PAdd exception
 test_with_statement.py(32, 8): ✔️ always true if reached - assert(697)
 test_with_statement.py(33, 8): ✔️ always true if reached - assert(724)
-DETAIL: 7 passed, 0 failed, 0 inconclusive
+DETAIL: 11 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataPython/StrataPythonTestExtra/AnalyzeLaurelTest.lean b/StrataPython/StrataPythonTestExtra/AnalyzeLaurelTest.lean
index c6bc50370d..898d069c8d 100644
--- a/StrataPython/StrataPythonTestExtra/AnalyzeLaurelTest.lean
+++ b/StrataPython/StrataPythonTestExtra/AnalyzeLaurelTest.lean
@@ -370,10 +370,9 @@ Without the attribute, the regex VC would be ❓ unknown. -/
     | .error msg => throw <| IO.userError s!"Pipeline failed: {msg}"
     | .ok vcResults =>
       for r in vcResults do
-        if r.obligation.label.startsWith "servicelib_Storage_" then
-          if !r.isSuccess then
-            throw <| IO.userError
-              s!"Expected all Storage preconditions to pass but got: {r.formatOutcome}"
+        if !r.isSuccess then
+          throw <| IO.userError
+            s!"Expected all Storage preconditions to pass but got: {r.formatOutcome}"
 
 /-! ## Resolution error test after FilterPrelude
 
diff --git a/StrataTest/Languages/Laurel/AbstractToConcreteTreeTranslatorTest.lean b/StrataTest/Languages/Laurel/AbstractToConcreteTreeTranslatorTest.lean
index 4456562e35..cfc0740d51 100644
--- a/StrataTest/Languages/Laurel/AbstractToConcreteTreeTranslatorTest.lean
+++ b/StrataTest/Languages/Laurel/AbstractToConcreteTreeTranslatorTest.lean
@@ -121,7 +121,9 @@ composite Point {
 info: procedure test(x: int): int
   opaque
 {
-  if x > 0 then x else 0 - x
+  if x > 0
+  then x
+  else 0 - x
 };
 -/
 #guard_msgs in
@@ -332,7 +334,8 @@ procedure test(): int
 info: procedure earlyExit(b: bool)
   opaque
 {
-  if b then {
+  if b
+  then {
     return
   };
   assert true
diff --git a/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean b/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean
index 855f316187..9580ece5d6 100644
--- a/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean
+++ b/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean
@@ -30,9 +30,7 @@ private def printElim (program : StrataDDM.Program) : IO Unit := do
 
 /--
 info: function nat$constraint(x: int): bool
-{
-  x >= 0
-};
+x >= 0;
 procedure test(n: int)
   returns (r: int)
   requires nat$constraint(n)
@@ -66,13 +64,12 @@ 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
-};
+v > 0;
 procedure test(b: bool)
   opaque
 {
-  if b then {
+  if b
+  then {
     var x: int := 1;
     assert pos$constraint(x)
   };
@@ -108,9 +105,7 @@ procedure test(b: bool) opaque {
 -- The variable has no known value, only the type constraint is assumed.
 /--
 info: function posint$constraint(x: int): bool
-{
-  x > 0
-};
+x > 0;
 procedure f()
   opaque
 {
diff --git a/StrataTest/Languages/Laurel/EliminateDoWhileTest.lean b/StrataTest/Languages/Laurel/EliminateDoWhileTest.lean
index 64517c93fe..548073bb0a 100644
--- a/StrataTest/Languages/Laurel/EliminateDoWhileTest.lean
+++ b/StrataTest/Languages/Laurel/EliminateDoWhileTest.lean
@@ -59,7 +59,8 @@ info: procedure basic()
       {
         x := x + 1
       };
-      if !(x < 3) then exit $dowhile_exit_0
+      if !(x < 3)
+      then exit $dowhile_exit_0
     }
   }$dowhile_exit_0;
   assert x == 3
@@ -106,12 +107,14 @@ info: procedure nested()
             {
               y := y + 1
             };
-            if !(y < 3) then exit $dowhile_exit_0
+            if !(y < 3)
+            then exit $dowhile_exit_0
           }
         }$dowhile_exit_0;
         x := x + 1
       };
-      if !(x < 3) then exit $dowhile_exit_1
+      if !(x < 3)
+      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 ca26f5f73e..0d15885bc9 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypes.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypes.lean
@@ -31,7 +31,7 @@ procedure outputValid(): nat
 
 // Output constraint — invalid return fails
 procedure outputInvalid(): nat
-//                         ^^^ error: assertion does not hold
+//                         ^^^ error: postcondition does not hold
   opaque
 {
   return -1
@@ -169,9 +169,7 @@ procedure uninitNotWitness()
 
 // Quantifier constraint injection — forall
 // n + 1 > 0 is only provable with n >= 0 injected; false for all int
-procedure forallNat()
-  opaque
-{
+procedure forallNat() opaque {
   var b: bool := forall(n: nat) => n + 1 > 0;
   assert b
 };
@@ -179,9 +177,7 @@ procedure forallNat()
 // Quantifier constraint injection — exists
 // n == -1 is satisfiable for int, but not when n >= 0 is required
 // n == 42 works because 42 >= 0
-procedure existsNat()
-  opaque
-{
+procedure existsNat() opaque {
   var b: bool := exists(n: nat) => n == 42;
   assert b
 };
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T15_ShortCircuit.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T15_ShortCircuit.lean
index 2e5e628620..eb7562fe68 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T15_ShortCircuit.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T15_ShortCircuit.lean
@@ -24,7 +24,6 @@ procedure mustNotCallProc(): int
 };
 
 // Pure path: function with requires false
-
 procedure testAndThenFunc()
   opaque
 {
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T18_RecursiveFunction.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T18_RecursiveProcedure.lean
similarity index 76%
rename from StrataTest/Languages/Laurel/Examples/Fundamentals/T18_RecursiveFunction.lean
rename to StrataTest/Languages/Laurel/Examples/Fundamentals/T18_RecursiveProcedure.lean
index 4b56c8266e..9a97632738 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T18_RecursiveFunction.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T18_RecursiveProcedure.lean
@@ -22,8 +22,9 @@ datatype IntList {
   Cons(head: int, tail: IntList)
 }
 
-function listLen(xs: IntList): int {
-  if IntList..isNil(xs) then 0
+procedure listLen(xs: IntList): int
+{
+  return if IntList..isNil(xs) then 0
   else 1 + listLen(IntList..tail!(xs))
 };
 
@@ -35,13 +36,15 @@ procedure testListLen()
 };
 
 // Mutual recursion
-function listLenEven(xs: IntList): bool {
-  if IntList..isNil(xs) then true
+procedure listLenEven(xs: IntList): bool
+{
+  return if IntList..isNil(xs) then true
   else listLenOdd(IntList..tail!(xs))
 };
 
-function listLenOdd(xs: IntList): bool {
-  if IntList..isNil(xs) then false
+procedure listLenOdd(xs: IntList): bool
+{
+  return if IntList..isNil(xs) then false
   else listLenEven(IntList..tail!(xs))
 };
 
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_InvokeOn.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_InvokeOn.lean
index 2389fa10c4..32efb65c0c 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_InvokeOn.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_InvokeOn.lean
@@ -69,7 +69,7 @@ procedure badPostcondition(x: int)
   invokeOn R(x)
   opaque
   ensures R(x)
-//        ^^^^ error: assertion could not be proved
+//        ^^^^ error: postcondition could not be proved
 {
 };
 #end
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T20_TransparentBody.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T20_TransparentBody.lean
index c9c1a2cc35..1b3ae3aa75 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T20_TransparentBody.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T20_TransparentBody.lean
@@ -15,11 +15,11 @@ program Laurel;
 procedure transparentBody(): int
 {
   assert true;
-  3
+  return 3
 };
 
 procedure tranparentCaller(): int {
-  transparentBody()
+  return transparentBody()
 };
 
 procedure transparentCallerCaller() opaque {
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T20_TransparentBodyError.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T20_TransparentBodyError.lean
index b9f59037bb..806c97af00 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T20_TransparentBodyError.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T20_TransparentBodyError.lean
@@ -16,13 +16,15 @@ procedure transparentBodyMultipleOuts() returns (q: int, r: int)
 {
   assert true;
   q := 3;
-//^^^^^^ error: destructive assignments are not supported in transparent bodies or contracts
   r := 2
+//^^^^^^ error: ending a transparent body with a Assign statement is not supported
 };
 
 procedure transparentBodyNoOuts()
 {
-  assert true
+  assert true;
+  3
+//^ error: ending a transparent body with a LiteralInt statement is not supported
 };
 
 procedure transparentProcedureCaller() opaque {
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
index bf4535c2aa..23885ec665 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
@@ -9,6 +9,7 @@ import StrataTest.Util.TestLaurel
 open StrataTest.Util
 open Strata
 
+#guard_msgs (drop info) in
 #eval testLaurel <|
 #strata
 program Laurel;
@@ -111,9 +112,9 @@ procedure imperativeCallInConditionalExpression(b: bool)
   }
 };
 
-function add(x: int, y: int): int
+procedure add(x: int, y: int): int
 {
-  x + y
+  return x + y
 };
 
 procedure repeatedBlockExpressions()
@@ -137,9 +138,58 @@ procedure addProcCaller(): int
 {
   var x: int := 0;
   var y: int := addProc({x := 1; x}, {x := x + 10; x});
-  assert y == 11 // TOOD should be 12. Fix in other PR
+  assert y == 12
 
+  // The next statement is not translated correctly.
+  // I think it's a bug in the handling of StaticCall
+  // Where a reference is substituted when it should not be
   // var z: int := addProc({x := 1; x}, {x := x + 10; x}) + (x := 3);
   // assert z == 15
 };
+
+procedure assertInsideConditionalExpression(a: int): int
+  return if a > 2
+    then 4
+    else {
+      assert a <= 2;
+      assert a < 2;
+//    ^^^^^^^^^^^^ error: assertion does not hold
+      5
+    };
+
+procedure assertInBlockExpr()
+opaque {
+  var x: int := 0;
+  var y: int := { assert x == 0; x := 1; x };
+  assert y == 1
+};
+
+procedure transparentProc(x: int) returns (r: int)
+{
+  return x + 1
+};
+
+procedure assignmentInExpressionAfterProcCall()
+opaque {
+  var x: int := 0;
+  var y: int := transparentProc(x) + (x := 2);
+  assert y == 3
+};
+
+procedure liftInsideAssignmentInExpression()
+opaque {
+  var x: int := 0;
+  var y: int := ((x := 1) + transparentProc(x));
+  assert y == 3
+};
+
+procedure hasMultipleOutputs() returns (x: int, y: int) opaque {
+  x := 1;
+  y := 2
+};
+
+procedure liftWithMultipleOutputs() opaque {
+  var x: int := { assign var y: int, var z: int := hasMultipleOutputs() ; y + z }
+};
+
 #end
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean
index d1e67ff6f6..5862e9b93f 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean
@@ -41,12 +41,10 @@ function functionWithWhile(x: int): int
 function functionCallingHasMutationAssignment(x: int): int
 {
   hasMutatingAssignment()
-//^^^^^^^^^^^^^^^^^^^^^^^ error: calls to procedures are not supported in functions or contracts
 };
 
-procedure impureContractIsNotLegal1(x: int)
+procedure impureContractIsLegal1(x: int)
   requires x == hasMutatingAssignment()
-//              ^^^^^^^^^^^^^^^^^^^^^^^ error: calls to procedures are not supported in functions or contracts
   opaque
 {
   assert hasMutatingAssignment() == 1
@@ -58,6 +56,5 @@ procedure impureContractIsNotLegal2(x: int)
   opaque
 {
   assert (x := 2) == 2
-//        ^^^^^^ error: destructive assignments are not supported in transparent bodies or contracts
 };
 #end
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean
index ed39235e88..83f3a702a2 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean
@@ -12,7 +12,7 @@ open Strata
 #eval testLaurel <|
 #strata
 program Laurel;
-function returnAtEnd(x: int) returns (r: int) {
+procedure returnAtEnd(x: int) returns (r: int) {
   if x > 0 then {
     if x == 1 then {
       return 1
@@ -24,11 +24,25 @@ function returnAtEnd(x: int) returns (r: int) {
   }
 };
 
-function elseWithCall(): int {
+function elseWithCall(): int
+{
   if true then 3 else returnAtEnd(3)
 };
 
-function guardInFunction(x: int) returns (r: int) {
+procedure testFunctions()
+  opaque
+{
+  assert returnAtEnd(1) == 1;
+  assert returnAtEnd(1) == 2;
+//^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved
+
+  assert guardInFunction(1) == 1;
+  assert guardInFunction(1) == 2
+//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved
+};
+
+procedure guardInFunction(x: int) returns (r: int)
+{
   if x > 0 then {
     if x == 1 then {
       return 1
@@ -40,20 +54,7 @@ function guardInFunction(x: int) returns (r: int) {
   return 3
 };
 
-procedure testFunctions()
-  opaque
-{
-  assert returnAtEnd(1) == 1;
-  assert returnAtEnd(1) == 2;
-//^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
-
-  assert guardInFunction(1) == 1;
-  assert guardInFunction(1) == 2
-//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
-};
-
 procedure guards(a: int) returns (r: int)
-  opaque
 {
   var b: int := a + 2;
   if b > 2 then {
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean
index 9438d322fe..a1d8f03ad7 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean
@@ -38,10 +38,4 @@ function localVariableWithoutInitializer(): int {
 //^^^^^^^^^^ error: local variables in functions must have initializers
   3
 };
-
-function deadCodeAfterIfElse(x: int) returns (r: int) {
-  if x > 0 then { return 1 } else { return 2 };
-//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: if-then-else only supported as the last statement in a block
-  return 3
-};
 #end
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError2.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError2.lean
new file mode 100644
index 0000000000..656009ffca
--- /dev/null
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError2.lean
@@ -0,0 +1,21 @@
+/-
+  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;
+
+procedure deadCodeAfterIfElse(x: int) returns (r: int) {
+  if x > 0 then { return 1 } else { return 2 };
+//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: in a transparent body, if-then-else is only supported as the last statement in a block
+  return 3
+};
+#end
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCalls.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCalls.lean
index f23b6d81c7..7f68e3caf6 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCalls.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCalls.lean
@@ -27,7 +27,7 @@ procedure fooSingleAssign(): int
   var x: int := 0;
   var x2: int := x + 1;
   var x3: int := x2 + 1;
-  x3
+  return x3
 };
 
 procedure fooProof()
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T7_Decreases.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T7_Decreases.lean
index 8be8a22a65..61175cc1e2 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T7_Decreases.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T7_Decreases.lean
@@ -21,23 +21,29 @@ procedure noDecreases(x: int): boolean;
 procedure caller(x: int)
   requires noDecreases(x)
 //                    ^ error: noDecreases can not be called from a pure context, because it is not proven to terminate
+  opaque
 ;
 
 procedure noCyclicCalls()
+  opaque
   decreases []
 {
   leaf();
 };
 
-procedure leaf() decreases [1] { };
+procedure leaf() decreases [1]
+  opaque
+{ };
 
 procedure mutualRecursionA(x: nat)
+  opaque
   decreases [x, 1]
 {
   mutualRecursionB(x);
 };
 
 procedure mutualRecursionB(x: nat)
+  opaque
   decreases [x, 0]
 {
   if x != 0 { mutualRecursionA(x-1); }
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean
index abf1d7e6c2..08e32bff17 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean
@@ -30,9 +30,24 @@ procedure callerOfOpaqueProcedure()
 };
 
 procedure invalidPostcondition(x: int)
+  returns (r: int) // TODO, removing this returns triggers a latent bug
   opaque
   ensures false
-//        ^^^^^ error: assertion does not hold
+//        ^^^^^ error: postcondition does not hold
 {
 };
+
+procedure bar(x: int) returns (r: int)
+  requires x > 0
+  opaque
+  ensures r > 0
+{
+  r := x + 1
+};
+
+procedure caller() returns (out: int)
+  opaque
+{
+  out := bar(bar(5))
+};
 #end
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8b_EarlyReturnPostconditions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8b_EarlyReturnPostconditions.lean
index 5c0ee06eb2..66a71def1c 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8b_EarlyReturnPostconditions.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8b_EarlyReturnPostconditions.lean
@@ -33,7 +33,7 @@ program Laurel;
 procedure earlyReturnBuggy(x: int) returns (r: int)
   opaque
   ensures r >= 0
-//        ^^^^^^ error: assertion does not hold
+//        ^^^^^^ error: postcondition does not hold
 {
   if x < 0 then {
     return x
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T9_Nondeterministic.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T9_Nondeterministic.lean
index d77667fb3d..1331db2c27 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T9_Nondeterministic.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T9_Nondeterministic.lean
@@ -20,6 +20,7 @@ nondet procedure nonDeterministic(x: int): (r: int)
 };
 
 procedure caller()
+  opaque
 {
   var x = nonDeterministic(1)
   assert x > 0;
@@ -29,11 +30,13 @@ procedure caller()
 };
 
 nondet procedure nonDeterminsticTransparant(x: int): (r: int)
+  opaque
 {
   nonDeterministic(x + 1)
 };
 
 procedure nonDeterministicCaller(x: int): int
+  opaque
 {
   nonDeterministic(x)
 };
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T10_CompositeBvField.lean b/StrataTest/Languages/Laurel/Examples/Objects/T10_CompositeBvField.lean
index 7c84f64a55..d60053efef 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T10_CompositeBvField.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T10_CompositeBvField.lean
@@ -44,7 +44,7 @@ procedure writeLiteral(r: Register)
 procedure writeWrongLiteral(r: Register)
   opaque
   ensures r#value == 100 bv 16
-//        ^^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved
+//        ^^^^^^^^^^^^^^^^^^^^ error: postcondition could not be proved
   modifies r
 {
   r#value := 200 bv 16
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean b/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean
index 8213eb22de..4bca875744 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean
@@ -9,7 +9,7 @@ import StrataTest.Util.TestLaurel
 open StrataTest.Util
 open Strata
 
-#eval testLaurel
+#eval testLaurelKeepIntermediates
 #strata
 program Laurel;
 composite Container {
@@ -66,9 +66,7 @@ procedure updatesAndAliasing()
   assert dAlias#intValue == d#intValue
 };
 
-procedure subsequentHeapMutations()
-  opaque
-{
+procedure subsequentHeapMutations() opaque {
   var c: Container := new Container;
 
   // The additional parenthesis on the next line are needed to let the parser succeed. Joe, any idea why this is needed?
@@ -124,9 +122,7 @@ composite Pixel {
   var color: Color
 }
 
-procedure datatypeField()
-  opaque
-{
+procedure datatypeField() opaque {
   var p: Pixel := new Pixel;
   p#color := Red();
   assert Color..isRed(p#color);
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8d_HeapMutatingValueReturn.lean b/StrataTest/Languages/Laurel/Examples/Objects/T1b_HeapMutatingValueReturn.lean
similarity index 92%
rename from StrataTest/Languages/Laurel/Examples/Fundamentals/T8d_HeapMutatingValueReturn.lean
rename to StrataTest/Languages/Laurel/Examples/Objects/T1b_HeapMutatingValueReturn.lean
index 83b315e977..1a18972604 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8d_HeapMutatingValueReturn.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T1b_HeapMutatingValueReturn.lean
@@ -40,7 +40,7 @@ composite Container {
 procedure setAndReturnBuggy(c: Container, x: int) returns (r: int)
   opaque
   ensures r == x + 1
-//        ^^^^^^^^^^ error: assertion does not hold
+//        ^^^^^^^^^^ error: postcondition does not hold
   modifies c
 {
   c#value := x;
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T3_ReadsClauses.lr.st b/StrataTest/Languages/Laurel/Examples/Objects/T3_ReadsClauses.lr.st
index 5732c7d40c..210a95c155 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T3_ReadsClauses.lr.st
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T3_ReadsClauses.lr.st
@@ -46,7 +46,8 @@ type Composite;
 type Field;
 val value: Field;
 
-function opaqueProcedure_ensures(heap: Heap, c: Container, r: int): boolean {
+function opaqueProcedure_ensures(heap: Heap, c: Container, r: int): boolean
+{
   true
 }
 
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T6_Datatypes.lean b/StrataTest/Languages/Laurel/Examples/Objects/T6_Datatypes.lean
index 99ef1565c1..896474404b 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T6_Datatypes.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T6_Datatypes.lean
@@ -18,17 +18,13 @@ datatype IntList {
 }
 
 // Construction and destructor access
-procedure testConstruction()
-  opaque
-{
+procedure testConstruction() opaque {
   var xs: IntList := Cons(42, Nil());
   assert IntList..head(xs) == 42
 };
 
 // Constructor testing
-procedure testConstructorTest()
-  opaque
-{
+procedure testConstructorTest() opaque {
   var xs: IntList := Cons(1, Nil());
   assert IntList..isCons(xs);
   assert !IntList..isNil(xs);
@@ -39,9 +35,7 @@ procedure testConstructorTest()
 };
 
 // Nested construction and deconstruction
-procedure testNested()
-  opaque
-{
+procedure testNested() opaque {
   var xs: IntList := Cons(1, Cons(2, Nil()));
   assert IntList..isCons(xs);
   assert IntList..head(xs) == 1;
@@ -50,9 +44,7 @@ procedure testNested()
   assert IntList..isNil(IntList..tail(IntList..tail(xs)))
 };
 
-procedure unsafeDestructor()
-  opaque
-{
+procedure unsafeDestructor() opaque {
   var nil: IntList := Nil();
   var noError: int := IntList..head!(nil);
   var error: int := IntList..head(nil)
@@ -66,18 +58,14 @@ function listHead(xs: IntList): int
   IntList..head(xs)
 };
 
-procedure testFunction()
-  opaque
-{
+procedure testFunction() opaque {
   var xs: IntList := Cons(10, Nil());
   var h: int := listHead(xs);
   assert h == 10
 };
 
 // Failing assertion
-procedure testFailing()
-  opaque
-{
+procedure testFailing() opaque {
   var xs: IntList := Nil();
   assert IntList..isCons(xs)
 //^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
@@ -93,9 +81,7 @@ datatype OddList {
   OCons(head: int, tail: EvenList)
 }
 
-procedure testMutualConstruction()
-  opaque
-{
+procedure testMutualConstruction() opaque {
   var even: EvenList := ENil();
   assert EvenList..isENil(even);
   var odd: OddList := OCons(1, ENil());
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T9_OldHeapTwoState.lean b/StrataTest/Languages/Laurel/Examples/Objects/T9_OldHeapTwoState.lean
index 6cc0fc85ff..89681f2234 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T9_OldHeapTwoState.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T9_OldHeapTwoState.lean
@@ -59,7 +59,7 @@ procedure bumpCell(c: Cell)
 procedure bumpCellWrong(c: Cell)
   opaque
   ensures c#value == old(c#value) + 1
-//        ^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved
+//        ^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: postcondition could not be proved
   modifies c
 {
   c#value := c#value + 2
@@ -210,7 +210,7 @@ procedure bumpUnderWildcard(c: Cell)
 procedure wrongOldRelation(c: Cell)
   opaque
   ensures c#value == old(c#value) - 1
-//        ^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved
+//        ^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: postcondition could not be proved
   modifies c
 {
   c#value := c#value + 1
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/WIP/5. Allocation.lr.st b/StrataTest/Languages/Laurel/Examples/Objects/WIP/5. Allocation.lr.st
index dd02787340..3dc57127ed 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/WIP/5. Allocation.lr.st	
+++ b/StrataTest/Languages/Laurel/Examples/Objects/WIP/5. Allocation.lr.st	
@@ -13,6 +13,7 @@ composite Immutable {
   invariant x + y >= 5
 
   procedure construct()
+    opaque
     constructor
     requires contructing == {this}
     ensures constructing == {}
@@ -50,6 +51,7 @@ composite ImmutableChainOfTwo {
 
   // only used privately
   procedure allocate()
+    opaque
     constructor
     ensures constructing = {this} {    
     // empty body
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/WIP/5. Constructors.lr.st b/StrataTest/Languages/Laurel/Examples/Objects/WIP/5. Constructors.lr.st
index 2d9a5afaa4..6d33df854c 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/WIP/5. Constructors.lr.st	
+++ b/StrataTest/Languages/Laurel/Examples/Objects/WIP/5. Constructors.lr.st	
@@ -18,6 +18,7 @@ composite Immutable {
   // fields of Immutable are considered mutable inside this procedure
   // and invariants of Immutable are not visible
   // can only call procedures that are also constructing Immutable
+    opaque
     constructs Immutable
     modifies this
   {
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/WIP/7. InstanceCallables.lr.st b/StrataTest/Languages/Laurel/Examples/Objects/WIP/7. InstanceCallables.lr.st
index fe4c5756d6..95cf829196 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/WIP/7. InstanceCallables.lr.st	
+++ b/StrataTest/Languages/Laurel/Examples/Objects/WIP/7. InstanceCallables.lr.st	
@@ -5,12 +5,14 @@
 */
 composite Base {
   procedure foo(): int
+    opaque
     ensures result > 3
     { abstract };
 }
 
 composite Extender1 extends Base {
   procedure foo(): int
+    opaque
     ensures result > 4
 //  ^^^^^^^ error: could not prove ensures clause guarantees that of extended method 'Base.foo'
     { abstract };
@@ -19,6 +21,7 @@ composite Extender1 extends Base {
 composite Extender2 extends Base {
   value: int
   procedure foo(): int
+    opaque
     ensures result > 2
   {
     this.value + 2 // 'this' is an implicit variable inside instance callables
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/WIP/9. Closures.lr.st b/StrataTest/Languages/Laurel/Examples/Objects/WIP/9. Closures.lr.st
index 212df76ab8..3449eb9246 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/WIP/9. Closures.lr.st	
+++ b/StrataTest/Languages/Laurel/Examples/Objects/WIP/9. Closures.lr.st	
@@ -87,6 +87,7 @@ so in affect there no longer are any variables captured by a closure.
 
 // Option A: first class procedures
 procedure hasClosure() returns (r: int)
+  opaque
   ensures r == 7
 {
   var x = 3;
diff --git a/StrataTest/Languages/Laurel/IncrDecrLiftTest.lean b/StrataTest/Languages/Laurel/IncrDecrLiftTest.lean
index b9d00c16cd..44731ab35d 100644
--- a/StrataTest/Languages/Laurel/IncrDecrLiftTest.lean
+++ b/StrataTest/Languages/Laurel/IncrDecrLiftTest.lean
@@ -15,7 +15,6 @@ expected output.
 meta import StrataDDM.Elab
 meta import StrataDDM.BuiltinDialects.Init
 meta import Strata.Languages.Laurel.Grammar
-meta import Strata.Languages.Laurel.LaurelToCoreTranslator
 meta import Strata.Languages.Laurel.EliminateIncrDecr
 meta import Strata.Languages.Laurel.LiftImperativeExpressions
 
@@ -42,7 +41,7 @@ def parseLowerIncrDecr (input : String) : IO Program := do
     -- Step 2: resolve so liftExpressionAssignments has a valid SemanticModel
     let result := resolve program
     let (program, model) := (result.program, result.model)
-    pure (liftExpressionAssignments model program)
+    pure (liftExpressionAssignments program model [])
 
 /-- Statement form: `x++;` and `--x` as statements. Prefix (`--x`) produces
     a clean assignment. Postfix (`x++`) emits the same assignment-based form as
diff --git a/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean b/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean
index 4754a126aa..814fabe6cf 100644
--- a/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean
+++ b/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean
@@ -11,7 +11,7 @@ by comparing the lifted Laurel against expected output.
 -/
 
 import StrataTest.Util.TestLaurel
-import Strata.Languages.Laurel.LaurelToCoreTranslator
+import Strata.Languages.Laurel.LaurelToCoreSchemaPass
 import Strata.Languages.Laurel.Resolution
 
 open Strata
@@ -22,7 +22,7 @@ namespace Strata.Laurel
 private def parseLaurelAndLift (program : StrataDDM.Program) : IO Program := do
   let laurelProgram ← translateLaurel program
   let result := resolve laurelProgram
-  pure (liftExpressionAssignments result.model result.program)
+  pure (liftExpressionAssignments result.program result.model [])
 
 private def printLifted (program : StrataDDM.Program) : IO Unit := do
   let lifted ← parseLaurelAndLift program
diff --git a/StrataTest/Languages/Laurel/LiftHolesTest.lean b/StrataTest/Languages/Laurel/LiftHolesTest.lean
index 46fc19a24f..a7d9879b9d 100644
--- a/StrataTest/Languages/Laurel/LiftHolesTest.lean
+++ b/StrataTest/Languages/Laurel/LiftHolesTest.lean
@@ -138,7 +138,8 @@ info: function $hole_0()
 procedure test()
   opaque
 {
-  if $hole_0() then {
+  if $hole_0()
+  then {
     assert true
   }
 };
@@ -160,7 +161,9 @@ info: function $hole_0()
 procedure test()
   opaque
 {
-  var x: int := if true then $hole_0() else 0
+  var x: int := if true
+  then $hole_0()
+  else 0
 };
 -/
 #guard_msgs in
@@ -336,7 +339,8 @@ info: function $hole_0()
 procedure test()
   opaque
 {
-  if 1 + $hole_0() > 0 then {
+  if 1 + $hole_0() > 0
+  then {
     assert true
   }
 };
@@ -424,7 +428,6 @@ info: function $hole_0(x: int)
   returns ($result: int)
   opaque;
 function test(x: int): int
-  opaque
 {
   $hole_0(x)
 };
@@ -434,7 +437,6 @@ function test(x: int): int
 #strata
 program Laurel;
 function test(x: int): int
-  opaque
 { <?> };
 #end
 
@@ -530,7 +532,7 @@ info: function $hole_0()
   opaque;
 procedure test()
 {
-  assert IntList..isCons($hole_0())
+  assert IntList..head($hole_0())
 };
 -/
 #guard_msgs in
@@ -538,7 +540,7 @@ procedure test()
 #strata
 program Laurel;
 datatype IntList { Nil(), Cons(head: int, tail: IntList) }
-procedure test() { assert IntList..isCons(<?>) };
+procedure test() { assert IntList..head(<?>) };
 #end
 
 end Laurel
diff --git a/StrataTest/Languages/Laurel/LiftImperativeCallsInAssertTest.lean b/StrataTest/Languages/Laurel/LiftImperativeCallsInAssertTest.lean
index 24ff37523b..dcc3135105 100644
--- a/StrataTest/Languages/Laurel/LiftImperativeCallsInAssertTest.lean
+++ b/StrataTest/Languages/Laurel/LiftImperativeCallsInAssertTest.lean
@@ -11,7 +11,7 @@ out of assert and assume conditions, while leaving assignments untouched
 -/
 
 import StrataTest.Util.TestLaurel
-import Strata.Languages.Laurel.LaurelToCoreTranslator
+import Strata.Languages.Laurel.LaurelToCoreSchemaPass
 import Strata.Languages.Laurel.Resolution
 
 open Strata
@@ -22,7 +22,7 @@ namespace Strata.Laurel
 private def parseLaurelAndLift (program : StrataDDM.Program) : IO Program := do
   let laurelProgram ← translateLaurel program
   let result := resolve laurelProgram
-  pure (liftExpressionAssignments result.model result.program)
+  pure (liftExpressionAssignments result.program result.model ["impure", "multi_out"])
 
 private def printLifted (program : StrataDDM.Program) : IO Unit := do
   let lifted ← parseLaurelAndLift program
@@ -40,9 +40,8 @@ info: procedure impure(): int
 };
 procedure test()
 {
-  var $c_0: int;
-  $c_0 := impure();
-  assert $c_0 == 1
+  var $cndtn_0: int := impure();
+  assert $cndtn_0 == 1
 };
 -/
 #guard_msgs in
@@ -65,7 +64,9 @@ procedure test() {
 info: procedure test()
 {
   var x: int := 0;
-  assert (x := 2) == 2
+  var $x_0: int := x;
+  x := 2;
+  assert x == 2
 };
 -/
 #guard_msgs in
@@ -89,9 +90,8 @@ info: procedure impure(): int
 };
 procedure test()
 {
-  var $c_0: int;
-  $c_0 := impure();
-  assume $c_0 == 1
+  var $cndtn_0: int := impure();
+  assume $cndtn_0 == 1
 };
 -/
 #guard_msgs in
@@ -121,9 +121,8 @@ info: procedure multi_out(x: int)
 };
 procedure test()
 {
-  var $c_0: BUG_MultiValuedExpr;
-  $c_0 := multi_out(5);
-  assert $c_0 == 6
+  var $cndtn_0: BUG_MultiValuedExpr := multi_out(5);
+  assert $cndtn_0 == 6
 };
 -/
 #guard_msgs in
diff --git a/docs/verso/LaurelDoc.lean b/docs/verso/LaurelDoc.lean
index eedf40093d..4de8a96ba4 100644
--- a/docs/verso/LaurelDoc.lean
+++ b/docs/verso/LaurelDoc.lean
@@ -6,7 +6,7 @@
 
 import VersoManual
 
-import Strata.Languages.Laurel
+import Strata.Languages.Laurel.LaurelAST
 import Strata.Languages.Laurel.LaurelTypes
 import Strata.Languages.Laurel.LaurelCompilationPipeline
 import Strata.Languages.Laurel.HeapParameterization
@@ -24,34 +24,39 @@ open Verso.Genre.Manual.InlineLean
 
 set_option pp.rawOnError true
 
-/-- Block command that generates documentation for all Laurel pipeline passes.
-    Usage inside a `#doc` block: `{laurelPipelineDocs}` -/
-@[block_command]
-def laurelPipelineDocs : Verso.Doc.Elab.BlockCommandOf Unit := fun () => do
-  let entries := laurelPipeline.map fun pass =>
+/-- Markdown documentation for all Laurel passes, including their
+    `comesBefore`/`comesAfter` ordering rationales. Note: pass
+    `documentation`/`reason` strings are rendered as Markdown, so avoid raw
+    `<angle-bracket>` text (it is treated as inline HTML and crashes Verso's
+    converter); use backticks for inline code instead. -/
+def laurelPipelineDocsMarkdown : String :=
+  let entries := allPasses.map fun pass =>
     let base := s!"- **{pass.name}**: {pass.documentation}"
-    if pass.comesBefore.isEmpty then base
-    else
-      let deps := pass.comesBefore.map fun cb =>
-        s!"  - Comes before **{cb.pass.name}** because: {cb.reason}"
-      base ++ "\n" ++ "\n".intercalate deps
-
-  let md := "\n".intercalate entries.toList
-  let some ast := MD4Lean.parse md
-    | Lean.throwError "Failed to parse laurelPipelineDocumentation as Markdown"
-  let blocks ← ast.blocks.mapM (Markdown.blockFromMarkdown · (handleHeaders := Markdown.strongEmphHeaders))
-  `(Verso.Doc.Block.concat #[$blocks,*])
-
-/-- Block command that generates a dependency graph for the Laurel pipeline passes
-    based on the `comesBefore` property.
-    Usage inside a `#doc` block: `{laurelPipelineDependencyGraph}` -/
-@[block_command]
-def laurelPipelineDependencyGraph : Verso.Doc.Elab.BlockCommandOf Unit := fun () => do
+    let beforeDeps := pass.comesBefore.map fun cb =>
+      s!"  - Comes before **{cb.pass.name}** because: {cb.reason}"
+    let afterDeps := pass.comesAfter.map fun ca =>
+      s!"  - Comes after **{ca.pass.name}** because: {ca.reason}"
+    let deps := beforeDeps ++ afterDeps
+    if deps.isEmpty then base
+    else base ++ "\n" ++ "\n".intercalate deps
+  "\n".intercalate entries.toList
+
+/-- Markdown dependency graph for the Laurel passes, derived from the
+    `comesBefore`/`comesAfter` properties. -/
+def laurelPipelineDependencyGraphMarkdown : String := Id.run do
   -- Collect all edges: (source, target, reason) where source comesBefore target
   let mut edges : List (String × String × String) := []
-  for pass in laurelPipeline do
+  for pass in allPasses do
+    -- `pass.comesBefore` declares: pass must run before cb.pass, i.e. pass → cb.pass
     for cb in pass.comesBefore do
       edges := edges ++ [(pass.name, cb.pass.name, cb.reason)]
+    -- `pass.comesAfter` declares: pass must run after ca.pass, i.e. ca.pass → pass
+    for ca in pass.comesAfter do
+      edges := edges ++ [(ca.pass.name, pass.name, ca.reason)]
+
+  -- Deduplicate edges with the same (source, target), keeping the first reason.
+  edges := edges.foldl (init := []) fun acc e =>
+    if acc.any (fun a => a.1 == e.1 && a.2.1 == e.2.1) then acc else acc ++ [e]
 
   -- Build the graph as a markdown list showing dependencies
   let mut md := "**Dependency edges** (A → B means A must run before B):\n\n"
@@ -62,16 +67,35 @@ def laurelPipelineDependencyGraph : Verso.Doc.Elab.BlockCommandOf Unit := fun ()
       md := md ++ s!"- **{src}** → **{tgt}**\n  - *{reason}*\n"
 
   -- Add a textual rendering of the pipeline order with dependency annotations
-  md := md ++ "\n**Pipeline execution order:**\n\n"
+  md := md ++ "\n**Pipeline execution order** (→ X: must run before X; ← X: must run after X):\n\n"
   md := md ++ "```\n"
   let mut idx := 1
-  for pass in laurelPipeline do
-    let deps := pass.comesBefore.map (s!" → {·.pass.name}")
+  for pass in allPasses do
+    let beforeDeps := pass.comesBefore.map (s!" → {·.pass.name}")
+    let afterDeps := pass.comesAfter.map (s!" ← {·.pass.name}")
+    let deps := beforeDeps ++ afterDeps
     let depStr := if deps.isEmpty then "" else String.join deps
     md := md ++ s!"{idx}. {pass.name}{depStr}\n"
     idx := idx + 1
   md := md ++ "```\n"
+  return md
+
+/-- Block command that generates documentation for all Laurel pipeline passes.
+    Usage inside a `#doc` block: `{laurelPipelineDocs}` -/
+@[block_command]
+def laurelPipelineDocs : Verso.Doc.Elab.BlockCommandOf Unit := fun () => do
+  let md := laurelPipelineDocsMarkdown
+  let some ast := MD4Lean.parse md
+    | Lean.throwError "Failed to parse laurelPipelineDocumentation as Markdown"
+  let blocks ← ast.blocks.mapM (Markdown.blockFromMarkdown · (handleHeaders := Markdown.strongEmphHeaders))
+  `(Verso.Doc.Block.concat #[$blocks,*])
 
+/-- Block command that generates a dependency graph for the Laurel pipeline passes
+    based on the `comesBefore` and `comesAfter` properties.
+    Usage inside a `#doc` block: `{laurelPipelineDependencyGraph}` -/
+@[block_command]
+def laurelPipelineDependencyGraph : Verso.Doc.Elab.BlockCommandOf Unit := fun () => do
+  let md := laurelPipelineDependencyGraphMarkdown
   let some ast := MD4Lean.parse md
     | Lean.throwError "Failed to parse laurelPipelineDependencyGraph as Markdown"
   let blocks ← ast.blocks.mapM (Markdown.blockFromMarkdown · (handleHeaders := Markdown.strongEmphHeaders))
@@ -940,17 +964,20 @@ If new references or definitions are created during compilation, `resolve` must
 
 ## Translation Pipeline
 
-Laurel programs are verified by translating them to Strata Core and then invoking the Core
-verification pipeline. The Laurel compilation pipeline consists of three parts:
-- Lowering, consisting of many phases. Maps Laurel to Laurel
-- Ordering, consisting of a single pass. Maps Laurel to OrderedLaurel
-- Translation, consisting of a single pass. Maps OrderedLaurel to Core.
+The Laurel to Core translation pipeline uses these IRs:
+- Laurel
+- UnorderedCoreWithLaurelTypes
+- CoreWithLaurelTypes
+- Core
 
-Ideally the translation pass only translates between types but does not change the structure of the program.
+Most of the passes are in the Laurel IR.
+The transparency pass goes from `Laurel` to `UnorderedCoreWithLaurelTypes`.
+The CoreGroupingAndOrdering goes from `UnorderedCoreWithLaurelTypes` to `CoreWithLaurelTypes`
+And the LaurelToCoreSchemaPass goes from `CoreWithLaurelTypes` to `Core`.
 
-## Lowering Passes
+## Passes
 
-The following passes are part of the lowering group:
+The following passes making up the compilation of Laurel to Core:
 
 {laurelPipelineDocs}