diff --git a/Strata/DDM/Elab.lean b/Strata/DDM/Elab.lean
index 4f4601ce5..a14f09015 100644
--- a/Strata/DDM/Elab.lean
+++ b/Strata/DDM/Elab.lean
@@ -394,7 +394,6 @@ def elabDialect
     elabDialectRest fm dialects #[] inputContext loc dialect startPos stopPos
 
 def parseStrataProgramFromDialect (dialects : LoadedDialects) (dialect : DialectName) (input : InputContext) : IO Strata.Program := do
-
   let leanEnv ← Lean.mkEmptyEnvironment 0
 
   let isTrue mem := inferInstanceAs (Decidable (dialect ∈ dialects.dialects))
diff --git a/Strata/Languages/Boogie/Verifier.lean b/Strata/Languages/Boogie/Verifier.lean
index 9d5a098a7..985680ac0 100644
--- a/Strata/Languages/Boogie/Verifier.lean
+++ b/Strata/Languages/Boogie/Verifier.lean
@@ -485,18 +485,19 @@ structure Diagnostic where
   message : String
   deriving Repr, BEq
 
-def toDiagnostic (files: Map Strata.Uri Lean.FileMap) (vcr : Boogie.VCResult) : Option Diagnostic := do
+def DiagnosticModel.toDiagnostic (files: Map Strata.Uri Lean.FileMap) (dm: DiagnosticModel): Diagnostic :=
+  let fileMap := (files.find? dm.fileRange.file).get!
+  let startPos := fileMap.toPosition dm.fileRange.range.start
+  let endPos := fileMap.toPosition dm.fileRange.range.stop
+  {
+    start := { line := startPos.line, column := startPos.column }
+    ending := { line := endPos.line, column := endPos.column }
+    message := dm.message
+  }
+
+def Boogie.VCResult.toDiagnostic (files: Map Strata.Uri Lean.FileMap) (vcr : Boogie.VCResult) : Option Diagnostic := do
   let modelOption := toDiagnosticModel vcr
-  modelOption.map (fun dm =>
-      let fileMap := (files.find? dm.fileRange.file).get!
-      let startPos := fileMap.toPosition dm.fileRange.range.start
-      let endPos := fileMap.toPosition dm.fileRange.range.stop
-      {
-        start := { line := startPos.line, column := startPos.column }
-        ending := { line := endPos.line, column := endPos.column }
-        message := dm.message
-      }
-    )
+  modelOption.map (fun dm => dm.toDiagnostic files)
 
 end Strata
 
diff --git a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
index 1880ff7a9..08b930a6d 100644
--- a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
+++ b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
@@ -10,6 +10,7 @@ import Strata.Languages.Laurel.Laurel
 import Strata.DL.Imperative.MetaData
 import Strata.Languages.Boogie.Expressions
 
+namespace Strata
 namespace Laurel
 
 open Std (ToFormat Format format)
@@ -79,10 +80,13 @@ instance : Inhabited Parameter where
 def translateHighType (arg : Arg) : TransM HighType := do
   match arg with
   | .op op =>
-    match op.name with
-    | q`Laurel.intType => return .TInt
-    | q`Laurel.boolType => return .TBool
-    | _ => TransM.error s!"translateHighType expects intType or boolType, got {repr op.name}"
+    match op.name, op.args with
+    | q`Laurel.intType, _ => return .TInt
+    | q`Laurel.boolType, _ => return .TBool
+    | q`Laurel.compositeType, #[nameArg] =>
+      let name ← translateIdent nameArg
+      return .UserDefined name
+    | _, _ => TransM.error s!"translateHighType expects intType, boolType or compositeType, got {repr op.name}"
   | _ => TransM.error s!"translateHighType expects operation"
 
 def translateNat (arg : Arg) : TransM Nat := do
@@ -116,8 +120,6 @@ instance : Inhabited Procedure where
     outputs := []
     precondition := .LiteralBool true
     decreases := none
-    determinism := Determinism.deterministic none
-    modifies := none
     body := .Transparent (.LiteralBool true)
   }
 
@@ -157,8 +159,8 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExpr := do
       let varType ← match typeArg with
         | .option _ (some (.op typeOp)) => match typeOp.name, typeOp.args with
           | q`Laurel.optionalType, #[typeArg0] => translateHighType typeArg0
-          | _, _ => pure .TInt
-        | _ => pure .TInt
+          | _, _ => TransM.error s!"Variable {name} requires explicit type"
+        | _ => TransM.error s!"Variable {name} requires explicit type"
       let value ← match assignArg with
         | .option _ (some (.op assignOp)) => match assignOp.args with
           | #[assignArg0] => translateStmtExpr assignArg0 >>= (pure ∘ some)
@@ -173,7 +175,8 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExpr := do
     | q`Laurel.assign, #[arg0, arg1] =>
       let target ← translateStmtExpr arg0
       let value ← translateStmtExpr arg1
-      return .Assign target value
+      let md ← getArgMetaData (.op op)
+      return .Assign target value md
     | q`Laurel.call, #[arg0, argsSeq] =>
       let callee ← translateStmtExpr arg0
       let calleeName := match callee with
@@ -195,6 +198,10 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExpr := do
           | _, _ => pure none
         | _ => pure none
       return .IfThenElse cond thenBranch elseBranch
+    | q`Laurel.fieldAccess, #[objArg, fieldArg] =>
+      let obj ← translateStmtExpr objArg
+      let field ← translateIdent fieldArg
+      return .FieldSelect obj field
     | _, #[arg0, arg1] => match getBinaryOp? op.name with
       | some primOp =>
         let lhs ← translateStmtExpr arg0
@@ -223,32 +230,73 @@ def parseProcedure (arg : Arg) : TransM Procedure := do
     | TransM.error s!"parseProcedure expects operation"
 
   match op.name, op.args with
-  | q`Laurel.procedure, #[arg0, arg1, returnParamsArg, arg3] =>
-    let name ← translateIdent arg0
-    let parameters ← translateParameters arg1
-    -- returnParamsArg is ReturnParameters category, need to unwrap returnParameters operation
-    let returnParameters ← match returnParamsArg with
-      | .option _ (some (.op returnOp)) => match returnOp.name, returnOp.args with
-        | q`Laurel.returnParameters, #[returnArg0] => translateParameters returnArg0
-        | _, _ => TransM.error s!"Expected returnParameters operation, got {repr returnOp.name}"
-      | .option _ none => pure []
-      | _ => TransM.error s!"Expected returnParameters operation, got {repr returnParamsArg}"
-    let body ← translateCommand arg3
+  | q`Laurel.procedure, #[nameArg, paramArg, returnTypeArg, returnParamsArg,
+      requiresArg, ensuresArg, bodyArg] =>
+    let name ← translateIdent nameArg
+    let parameters ← translateParameters paramArg
+    -- Either returnTypeArg or returnParamsArg may have a value, not both
+    -- If returnTypeArg is set, create a single "result" parameter
+    let returnParameters ← match returnTypeArg with
+      | .option _ (some (.op returnTypeOp)) => match returnTypeOp.name, returnTypeOp.args with
+        | q`Laurel.optionalReturnType, #[typeArg] =>
+          let retType ← translateHighType typeArg
+          pure [{ name := "result", type := retType : Parameter }]
+        | _, _ => TransM.error s!"Expected optionalReturnType operation, got {repr returnTypeOp.name}"
+      | .option _ none =>
+        -- No return type, check returnParamsArg instead
+        match returnParamsArg with
+        | .option _ (some (.op returnOp)) => match returnOp.name, returnOp.args with
+          | q`Laurel.returnParameters, #[returnArg0] => translateParameters returnArg0
+          | _, _ => TransM.error s!"Expected returnParameters operation, got {repr returnOp.name}"
+        | .option _ none => pure []
+        | _ => TransM.error s!"Expected returnParameters operation, got {repr returnParamsArg}"
+      | _ => TransM.error s!"Expected optionalReturnType operation, got {repr returnTypeArg}"
+    -- Parse precondition (requires clause)
+    let precondition ← match requiresArg with
+      | .option _ (some (.op requiresOp)) => match requiresOp.name, requiresOp.args with
+        | q`Laurel.optionalRequires, #[exprArg] => translateStmtExpr exprArg
+        | _, _ => TransM.error s!"Expected optionalRequires operation, got {repr requiresOp.name}"
+      | .option _ none => pure (.LiteralBool true)
+      | _ => TransM.error s!"Expected optionalRequires operation, got {repr requiresArg}"
+    -- Parse postcondition (ensures clause)
+    let postcondition ← match ensuresArg with
+      | .option _ (some (.op ensuresOp)) => match ensuresOp.name, ensuresOp.args with
+        | q`Laurel.optionalEnsures, #[exprArg] => translateStmtExpr exprArg >>= (pure ∘ some)
+        | _, _ => TransM.error s!"Expected optionalEnsures operation, got {repr ensuresOp.name}"
+      | .option _ none => pure none
+      | _ => TransM.error s!"Expected optionalEnsures operation, got {repr ensuresArg}"
+    let body ← translateCommand bodyArg
+    -- If there's a postcondition, use Opaque body; otherwise use Transparent
+    let procBody := match postcondition with
+      | some post => Body.Opaque post (some body) .nondeterministic none
+      | none => Body.Transparent body
     return {
       name := name
       inputs := parameters
       outputs := returnParameters
-      precondition := .LiteralBool true
+      precondition := precondition
       decreases := none
-      determinism := Determinism.deterministic none
-      modifies := none
-      body := .Transparent body
+      body := procBody
     }
   | q`Laurel.procedure, args =>
-    TransM.error s!"parseProcedure expects 4 arguments, got {args.size}"
+    TransM.error s!"parseProcedure expects 7 arguments, got {args.size}"
   | _, _ =>
     TransM.error s!"parseProcedure expects procedure, got {repr op.name}"
 
+def parseTopLevel (arg : Arg) : TransM (Option Procedure) := do
+  let .op op := arg
+    | TransM.error s!"parseTopLevel expects operation"
+
+  match op.name, op.args with
+  | q`Laurel.topLevelProcedure, #[procArg] =>
+    let proc ← parseProcedure procArg
+    return some proc
+  | q`Laurel.topLevelComposite, #[_compositeArg] =>
+    -- TODO: handle composite types
+    return none
+  | _, _ =>
+    TransM.error s!"parseTopLevel expects topLevelProcedure or topLevelComposite, got {repr op.name}"
+
 /--
 Translate concrete Laurel syntax into abstract Laurel syntax
 -/
@@ -270,11 +318,10 @@ def parseProgram (prog : Strata.Program) : TransM Laurel.Program := do
 
   let mut procedures : List Procedure := []
   for op in commands do
-    if op.name == q`Laurel.procedure then
-      let proc ← parseProcedure (.op op)
-      procedures := procedures ++ [proc]
-    else
-      TransM.error s!"Unknown top-level declaration: {op.name}"
+    let result ← parseTopLevel (.op op)
+    match result with
+    | some proc => procedures := procedures ++ [proc]
+    | none => pure () -- composite types are skipped for now
   return {
     staticProcedures := procedures
     staticFields := []
diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
index 6efdcaeb1..54723e20b 100644
--- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
+++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
@@ -4,6 +4,7 @@ dialect Laurel;
 category LaurelType;
 op intType : LaurelType => "int";
 op boolType : LaurelType => "bool";
+op compositeType (name: Ident): LaurelType => name;
 
 category StmtExpr;
 op literalBool (b: Bool): StmtExpr => b;
@@ -19,12 +20,17 @@ op optionalAssignment(value: StmtExpr): OptionalAssignment => ":=" value:0;
 op varDecl (name: Ident, varType: Option OptionalType, assignment: Option OptionalAssignment): StmtExpr
   => @[prec(0)] "var " name varType assignment ";";
 
-// Identifiers/Variables
+op call(callee: StmtExpr, args: CommaSepBy StmtExpr): StmtExpr => callee "(" args ")";
+
+// Field access
+op fieldAccess (obj: StmtExpr, field: Ident): StmtExpr => @[prec(90)] obj "#" field;
+
+// Identifiers/Variables - must come after fieldAccess so c.value parses as fieldAccess not identifier
 op identifier (name: Ident): StmtExpr => name;
 op parenthesis (inner: StmtExpr): StmtExpr => "(" inner ")";
 
 // Assignment
-op assign (target: StmtExpr, value: StmtExpr): StmtExpr => target ":=" value ";";
+op assign (target: StmtExpr, value: StmtExpr): StmtExpr => @[prec(10)] target ":=" value ";";
 
 // Binary operators
 op add (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(60)] lhs "+" rhs;
@@ -35,8 +41,6 @@ op lt (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs "<" rhs;
 op le (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs "<=" rhs;
 op ge (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs ">=" rhs;
 
-op call(callee: StmtExpr, args: CommaSepBy StmtExpr): StmtExpr => callee "(" args ")";
-
 // If-else
 category OptionalElse;
 op optionalElse(stmts : StmtExpr) : OptionalElse => "else" stmts;
@@ -52,13 +56,38 @@ op block (stmts : Seq StmtExpr) : StmtExpr => @[prec(1000)] "{" stmts "}";
 category Parameter;
 op parameter (name: Ident, paramType: LaurelType): Parameter => name ":" paramType;
 
+// Composite types
+category Field;
+op mutableField (name: Ident, fieldType: LaurelType): Field => "var " name ":" fieldType;
+op immutableField (name: Ident, fieldType: LaurelType): Field => name ":" fieldType;
+
+category Composite;
+op composite (name: Ident, fields: Seq Field): Composite => "composite " name "{" fields "}";
+
+// Procedures
+category OptionalReturnType;
+op optionalReturnType(returnType: LaurelType): OptionalReturnType => ":" returnType;
+
+category OptionalRequires;
+op optionalRequires(cond: StmtExpr): OptionalRequires => "requires" cond:0;
+
+category OptionalEnsures;
+op optionalEnsures(cond: StmtExpr): OptionalEnsures => "ensures" cond:0;
+
 category ReturnParameters;
 op returnParameters(parameters: CommaSepBy Parameter): ReturnParameters => "returns" "(" parameters ")";
 
 category Procedure;
 op procedure (name : Ident, parameters: CommaSepBy Parameter,
+  returnType: Option OptionalReturnType,
   returnParameters: Option ReturnParameters,
+  requires: Option OptionalRequires,
+  ensures: Option OptionalEnsures,
   body : StmtExpr) : Procedure =>
-  "procedure " name "(" parameters ")" returnParameters body:0;
+  "procedure " name "(" parameters ")" returnType returnParameters requires ensures body:0;
+
+category TopLevel;
+op topLevelComposite(composite: Composite): TopLevel => composite;
+op topLevelProcedure(procedure: Procedure): TopLevel => procedure;
 
-op program (staticProcedures: Seq Procedure): Command => staticProcedures;
\ No newline at end of file
+op program (items: Seq TopLevel): Command => items;
\ No newline at end of file
diff --git a/Strata/Languages/Laurel/HeapParameterization.lean b/Strata/Languages/Laurel/HeapParameterization.lean
new file mode 100644
index 000000000..4bf9803c5
--- /dev/null
+++ b/Strata/Languages/Laurel/HeapParameterization.lean
@@ -0,0 +1,145 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.Languages.Laurel.Laurel
+import Strata.Languages.Laurel.LaurelFormat
+
+/-
+Heap Parameterization Pass
+
+Transforms transparent procedures that read fields (or call procedures that read the heap)
+by adding an explicit `heap: Heap` parameter. Field reads are translated to calls to
+`read(heap, <fieldConstant>)`.
+-/
+
+namespace Strata.Laurel
+
+structure AnalysisResult where
+  readsHeapDirectly : Bool := false
+  callees : List Identifier := []
+
+partial def collectExpr (expr : StmtExpr) : StateM AnalysisResult Unit := do
+  match expr with
+  | .FieldSelect target _ =>
+      modify fun s => { s with readsHeapDirectly := true }; collectExpr target
+  | .InstanceCall target _ args => modify fun s => { s with readsHeapDirectly := true }; collectExpr target; for a in args do collectExpr a
+  | .StaticCall callee args => modify fun s => { s with callees := callee :: s.callees }; for a in args do collectExpr a
+  | .IfThenElse c t e => collectExpr c; collectExpr t; if let some x := e then collectExpr x
+  | .Block stmts _ => for s in stmts do collectExpr s
+  | .LocalVariable _ _ i => if let some x := i then collectExpr x
+  | .While c i d b => collectExpr c; collectExpr b; if let some x := i then collectExpr x; if let some x := d then collectExpr x
+  | .Return v => if let some x := v then collectExpr x
+  | .Assign t v _ => collectExpr t; collectExpr v
+  | .PureFieldUpdate t _ v => collectExpr t; collectExpr v
+  | .PrimitiveOp _ args => for a in args do collectExpr a
+  | .ReferenceEquals l r => collectExpr l; collectExpr r
+  | .AsType t _ => collectExpr t
+  | .IsType t _ => collectExpr t
+  | .Forall _ _ b => collectExpr b
+  | .Exists _ _ b => collectExpr b
+  | .Assigned n => collectExpr n
+  | .Old v => collectExpr v
+  | .Fresh v => collectExpr v
+  | .Assert c _ => collectExpr c
+  | .Assume c _ => collectExpr c
+  | .ProveBy v p => collectExpr v; collectExpr p
+  | .ContractOf _ f => collectExpr f
+  | _ => pure ()
+
+def analyzeProc (proc : Procedure) : AnalysisResult :=
+  match proc.body with
+  | .Transparent b =>
+      dbg_trace s!"Analyzing proc {proc.name} body: {Std.Format.pretty (Std.ToFormat.format b)}"
+      (collectExpr b).run {} |>.2
+  | _ => {}
+
+def computeReadsHeap (procs : List Procedure) : List Identifier :=
+  let info := procs.map fun p => (p.name, analyzeProc p)
+  let direct := info.filterMap fun (n, r) => if r.readsHeapDirectly then some n else none
+  let rec fixpoint (fuel : Nat) (current : List Identifier) : List Identifier :=
+    match fuel with
+    | 0 => current
+    | fuel' + 1 =>
+      let next := info.filterMap fun (n, r) =>
+        if current.contains n then some n
+        else if r.callees.any current.contains then some n
+        else none
+      if next.length == current.length then current else fixpoint fuel' next
+  fixpoint procs.length direct
+
+structure TransformState where
+  fieldConstants : List Constant := []
+  heapReaders : List Identifier
+
+abbrev TransformM := StateM TransformState
+
+def addFieldConstant (name : Identifier) : TransformM Unit :=
+  modify fun s => if s.fieldConstants.any (·.name == name) then s
+    else { s with fieldConstants := { name := name, type := .TField } :: s.fieldConstants }
+
+def readsHeap (name : Identifier) : TransformM Bool := do
+  return (← get).heapReaders.contains name
+
+partial def heapTransformExpr (heap : Identifier) (expr : StmtExpr) : TransformM StmtExpr := do
+  match expr with
+  | .FieldSelect target fieldName =>
+      addFieldConstant fieldName
+      let t ← heapTransformExpr heap target
+      return .StaticCall "heapRead" [.Identifier heap, t, .Identifier fieldName]
+  | .StaticCall callee args =>
+      let args' ← args.mapM (heapTransformExpr heap)
+      return if ← readsHeap callee then .StaticCall callee (.Identifier heap :: args') else .StaticCall callee args'
+  | .InstanceCall target callee args =>
+      let t ← heapTransformExpr heap target
+      let args' ← args.mapM (heapTransformExpr heap)
+      return .InstanceCall t callee (.Identifier heap :: args')
+  | .IfThenElse c t e => return .IfThenElse (← heapTransformExpr heap c) (← heapTransformExpr heap t) (← e.mapM (heapTransformExpr heap))
+  | .Block stmts label => return .Block (← stmts.mapM (heapTransformExpr heap)) label
+  | .LocalVariable n ty i => return .LocalVariable n ty (← i.mapM (heapTransformExpr heap))
+  | .While c i d b => return .While (← heapTransformExpr heap c) (← i.mapM (heapTransformExpr heap)) (← d.mapM (heapTransformExpr heap)) (← heapTransformExpr heap b)
+  | .Return v => return .Return (← v.mapM (heapTransformExpr heap))
+  | .Assign t v md =>
+      match t with
+      | .FieldSelect target fieldName =>
+          addFieldConstant fieldName
+          let target' ← heapTransformExpr heap target
+          let v' ← heapTransformExpr heap v
+          -- heap := heapStore(heap, target, field, value)
+          return .Assign (.Identifier heap) (.StaticCall "heapStore" [.Identifier heap, target', .Identifier fieldName, v']) md
+      | _ => return .Assign (← heapTransformExpr heap t) (← heapTransformExpr heap v) md
+  | .PureFieldUpdate t f v => return .PureFieldUpdate (← heapTransformExpr heap t) f (← heapTransformExpr heap v)
+  | .PrimitiveOp op args => return .PrimitiveOp op (← args.mapM (heapTransformExpr heap))
+  | .ReferenceEquals l r => return .ReferenceEquals (← heapTransformExpr heap l) (← heapTransformExpr heap r)
+  | .AsType t ty => return .AsType (← heapTransformExpr heap t) ty
+  | .IsType t ty => return .IsType (← heapTransformExpr heap t) ty
+  | .Forall n ty b => return .Forall n ty (← heapTransformExpr heap b)
+  | .Exists n ty b => return .Exists n ty (← heapTransformExpr heap b)
+  | .Assigned n => return .Assigned (← heapTransformExpr heap n)
+  | .Old v => return .Old (← heapTransformExpr heap v)
+  | .Fresh v => return .Fresh (← heapTransformExpr heap v)
+  | .Assert c md => return .Assert (← heapTransformExpr heap c) md
+  | .Assume c md => return .Assume (← heapTransformExpr heap c) md
+  | .ProveBy v p => return .ProveBy (← heapTransformExpr heap v) (← heapTransformExpr heap p)
+  | .ContractOf ty f => return .ContractOf ty (← heapTransformExpr heap f)
+  | other => return other
+
+def heapTransformProcedure (proc : Procedure) : TransformM Procedure := do
+  if (← get).heapReaders.contains proc.name then
+    match proc.body with
+    | .Transparent bodyExpr =>
+        let body' ← heapTransformExpr "heap" bodyExpr
+        return { proc with inputs := { name := "heap", type := .THeap } :: proc.inputs, body := .Transparent body' }
+    | _ => return proc
+  else return proc
+
+def heapParameterization (program : Program) : Program :=
+  let heapReaders := computeReadsHeap program.staticProcedures
+  dbg_trace s!"Heap readers: {heapReaders}"
+  let (procs', finalState) := (program.staticProcedures.mapM heapTransformProcedure).run { heapReaders }
+  dbg_trace s!"Field constants: {finalState.fieldConstants.map (·.name)}"
+  { program with staticProcedures := procs', constants := program.constants ++ finalState.fieldConstants }
+
+end Strata.Laurel
diff --git a/Strata/Languages/Laurel/Laurel.lean b/Strata/Languages/Laurel/Laurel.lean
index ffa4d5d39..6105029a1 100644
--- a/Strata/Languages/Laurel/Laurel.lean
+++ b/Strata/Languages/Laurel/Laurel.lean
@@ -43,6 +43,7 @@ Design choices:
 - Construction of composite types is WIP. It needs a design first.
 
 -/
+namespace Strata
 namespace Laurel
 
 abbrev Identifier := String /- Potentially this could be an Int to save resources. -/
@@ -67,8 +68,6 @@ structure Procedure: Type where
   outputs : List Parameter
   precondition : StmtExpr
   decreases : Option StmtExpr -- optionally prove termination
-  determinism: Determinism
-  modifies : Option StmtExpr
   body : Body
 
 inductive Determinism where
@@ -84,6 +83,8 @@ inductive HighType : Type where
   | TBool
   | TInt
   | TFloat64 /- Required for JavaScript (number). Used by Python (float) and Java (double) as well -/
+  | THeap /- Internal type for heap parameterization pass. Not accessible via grammar. -/
+  | TField /- Internal type for field constants in heap parameterization pass. Not accessible via grammar. -/
   | UserDefined (name: Identifier)
   | Applied (base : HighType) (typeArguments : List HighType)
   /- Pure represents a composite type that does not support reference equality -/
@@ -97,7 +98,7 @@ inductive HighType : Type where
 inductive Body where
   | Transparent (body : StmtExpr)
 /- Without an implementation, the postcondition is assumed -/
-  | Opaque (postcondition : StmtExpr) (implementation : Option StmtExpr)
+  | Opaque (postcondition : StmtExpr) (implementation : Option StmtExpr) (determinism: Determinism) (modifies : Option StmtExpr)
 /- An abstract body is useful for types that are extending.
     A type containing any members with abstract bodies can not be instantiated. -/
   | Abstract (postcondition : StmtExpr)
@@ -130,7 +131,7 @@ inductive StmtExpr : Type where
   | LiteralBool (value: Bool)
   | Identifier (name : Identifier)
   /- Assign is only allowed in an impure context -/
-  | Assign (target : StmtExpr) (value : StmtExpr)
+  | Assign (target : StmtExpr) (value : StmtExpr) (md : Imperative.MetaData Boogie.Expression)
   /- Used by itself for fields reads and in combination with Assign for field writes -/
   | FieldSelect (target : StmtExpr) (fieldName : Identifier)
   /- PureFieldUpdate is the only way to assign values to fields of pure types -/
@@ -193,6 +194,8 @@ def highEq (a: HighType) (b: HighType) : Bool := match a, b with
   | HighType.TBool, HighType.TBool => true
   | HighType.TInt, HighType.TInt => true
   | HighType.TFloat64, HighType.TFloat64 => true
+  | HighType.THeap, HighType.THeap => true
+  | HighType.TField, HighType.TField => true
   | HighType.UserDefined n1, HighType.UserDefined n2 => n1 == n2
   | HighType.Applied b1 args1, HighType.Applied b2 args2 =>
       highEq b1 b2 && args1.length == args2.length && (args1.attach.zip args2 |>.all (fun (a1, a2) => highEq a1.1 a2))
@@ -250,7 +253,12 @@ inductive TypeDefinition where
   | Composite (ty : CompositeType)
   | Constrained (ty : ConstrainedType)
 
+structure Constant where
+  name : Identifier
+  type : HighType
+
 structure Program where
   staticProcedures : List Procedure
   staticFields : List Field
   types : List TypeDefinition
+  constants : List Constant := []
diff --git a/Strata/Languages/Laurel/LaurelFormat.lean b/Strata/Languages/Laurel/LaurelFormat.lean
index 1c34062a3..7b3628d5d 100644
--- a/Strata/Languages/Laurel/LaurelFormat.lean
+++ b/Strata/Languages/Laurel/LaurelFormat.lean
@@ -6,6 +6,7 @@
 
 import Strata.Languages.Laurel.Laurel
 
+namespace Strata
 namespace Laurel
 
 open Std (Format)
@@ -33,6 +34,8 @@ def formatHighType : HighType → Format
   | .TBool => "bool"
   | .TInt => "int"
   | .TFloat64 => "float64"
+  | .THeap => "Heap"
+  | .TField => "Field"
   | .UserDefined name => Format.text name
   | .Applied base args =>
       Format.text "(" ++ formatHighType base ++ " " ++
@@ -66,7 +69,7 @@ def formatStmtExpr (s:StmtExpr) : Format :=
   | .LiteralInt n => Format.text (toString n)
   | .LiteralBool b => if b then "true" else "false"
   | .Identifier name => Format.text name
-  | .Assign target value =>
+  | .Assign target value _ =>
       formatStmtExpr target ++ " := " ++ formatStmtExpr value
   | .FieldSelect target field =>
       formatStmtExpr target ++ "." ++ Format.text field
@@ -119,8 +122,12 @@ def formatDeterminism : Determinism → Format
 
 def formatBody : Body → Format
   | .Transparent body => formatStmtExpr body
-  | .Opaque post impl =>
-      "opaque ensures " ++ formatStmtExpr post ++
+  | .Opaque post impl determ modif =>
+      "opaque " ++ formatDeterminism determ ++
+      (match modif with
+       | none => ""
+       | some m => " modifies " ++ formatStmtExpr m) ++
+      " ensures " ++ formatStmtExpr post ++
       match impl with
       | none => ""
       | some e => " := " ++ formatStmtExpr e
diff --git a/Strata/Languages/Laurel/LaurelToBoogieTranslator.lean b/Strata/Languages/Laurel/LaurelToBoogieTranslator.lean
index 2ae0bcaa0..604cd6d3d 100644
--- a/Strata/Languages/Laurel/LaurelToBoogieTranslator.lean
+++ b/Strata/Languages/Laurel/LaurelToBoogieTranslator.lean
@@ -11,17 +11,18 @@ import Strata.Languages.Boogie.Procedure
 import Strata.Languages.Boogie.Options
 import Strata.Languages.Laurel.Laurel
 import Strata.Languages.Laurel.LiftExpressionAssignments
+import Strata.Languages.Laurel.HeapParameterization
 import Strata.DL.Imperative.Stmt
 import Strata.DL.Imperative.MetaData
 import Strata.DL.Lambda.LExpr
 import Strata.Languages.Laurel.LaurelFormat
 
-namespace Laurel
-
 open Boogie (VCResult VCResults)
-open Strata
-
 open Boogie (intAddOp intSubOp intMulOp intDivOp intModOp intNegOp intLtOp intLeOp intGtOp intGeOp boolAndOp boolOrOp boolNotOp)
+
+namespace Strata.Laurel
+
+open Strata
 open Lambda (LMonoTy LTy LExpr)
 
 /-
@@ -31,30 +32,40 @@ def translateType (ty : HighType) : LMonoTy :=
   match ty with
   | .TInt => LMonoTy.int
   | .TBool => LMonoTy.bool
-  | .TVoid => LMonoTy.bool  -- Using bool as placeholder for void
+  | .TVoid => LMonoTy.bool
+  | .THeap => .tcons "Heap" []
+  | .TField => .tcons "Field" [LMonoTy.int]  -- For now, all fields hold int
+  | .UserDefined _ => .tcons "Composite" []
   | _ => panic s!"unsupported type {repr ty}"
 
+abbrev TypeEnv := List (Identifier × HighType)
+
+def lookupType (env : TypeEnv) (name : Identifier) : LMonoTy :=
+  match env.find? (fun (n, _) => n == name) with
+  | some (_, ty) => translateType ty
+  | none => LMonoTy.int  -- fallback
+
 /--
 Translate Laurel StmtExpr to Boogie Expression
 -/
-def translateExpr (expr : StmtExpr) : Boogie.Expression.Expr :=
+def translateExpr (env : TypeEnv) (expr : StmtExpr) : Boogie.Expression.Expr :=
   match h: expr with
   | .LiteralBool b => .const () (.boolConst b)
   | .LiteralInt i => .const () (.intConst i)
   | .Identifier name =>
       let ident := Boogie.BoogieIdent.locl name
-      .fvar () ident (some LMonoTy.int)  -- Default to int type
+      .fvar () ident (some (lookupType env name))
   | .PrimitiveOp op [e] =>
     match op with
-    | .Not => .app () boolNotOp (translateExpr e)
-    | .Neg => .app () intNegOp (translateExpr e)
+    | .Not => .app () boolNotOp (translateExpr env e)
+    | .Neg => .app () intNegOp (translateExpr env e)
     | _ => panic! s!"translateExpr: Invalid unary op: {repr op}"
   | .PrimitiveOp op [e1, e2] =>
     let binOp (bop : Boogie.Expression.Expr): Boogie.Expression.Expr :=
-      LExpr.mkApp () bop [translateExpr e1, translateExpr e2]
+      LExpr.mkApp () bop [translateExpr env e1, translateExpr env e2]
     match op with
-    | .Eq => .eq () (translateExpr e1) (translateExpr e2)
-    | .Neq => .app () boolNotOp (.eq () (translateExpr e1) (translateExpr e2))
+    | .Eq => .eq () (translateExpr env e1) (translateExpr env e2)
+    | .Neq => .app () boolNotOp (.eq () (translateExpr env e1) (translateExpr env e2))
     | .And => binOp boolAndOp
     | .Or => binOp boolOrOp
     | .Add => binOp intAddOp
@@ -70,18 +81,20 @@ def translateExpr (expr : StmtExpr) : Boogie.Expression.Expr :=
   | .PrimitiveOp op args =>
     panic! s!"translateExpr: PrimitiveOp {repr op} with {args.length} args"
   | .IfThenElse cond thenBranch elseBranch =>
-      let bcond := translateExpr cond
-      let bthen := translateExpr thenBranch
+      let bcond := translateExpr env cond
+      let bthen := translateExpr env thenBranch
       let belse := match elseBranch with
-                  | some e => translateExpr e
+                  | some e => translateExpr env e
                   | none => .const () (.intConst 0)
       .ite () bcond bthen belse
-  | .Assign _ value => translateExpr value  -- For expressions, just translate the value
+  | .Assign _ value _ => translateExpr env value
   | .StaticCall name args =>
-      -- Create function call as an op application
       let ident := Boogie.BoogieIdent.glob name
-      let fnOp := .op () ident (some LMonoTy.int)  -- Assume int return type
-      args.foldl (fun acc arg => .app () acc (translateExpr arg)) fnOp
+      let fnOp := .op () ident none
+      args.foldl (fun acc arg => .app () acc (translateExpr env arg)) fnOp
+  | .ReferenceEquals e1 e2 =>
+      .eq () (translateExpr env e1) (translateExpr env e2)
+  | .Block [single] _ => translateExpr env single
   | _ => panic! Std.Format.pretty (Std.ToFormat.format expr)
   decreasing_by
   all_goals (simp_wf; try omega)
@@ -93,69 +106,77 @@ def getNameFromMd (md : Imperative.MetaData Boogie.Expression): String :=
 
 /--
 Translate Laurel StmtExpr to Boogie Statements
-Takes the list of output parameter names to handle return statements correctly
+Takes the type environment and output parameter names
 -/
-def translateStmt (outputParams : List Parameter) (stmt : StmtExpr) : List Boogie.Statement :=
+def translateStmt (env : TypeEnv) (outputParams : List Parameter) (stmt : StmtExpr) : TypeEnv × List Boogie.Statement :=
   match stmt with
   | @StmtExpr.Assert cond md =>
-      let boogieExpr := translateExpr cond
-      [Boogie.Statement.assert ("assert" ++ getNameFromMd md) boogieExpr md]
+      let boogieExpr := translateExpr env cond
+      (env, [Boogie.Statement.assert ("assert" ++ getNameFromMd md) boogieExpr md])
   | @StmtExpr.Assume cond md =>
-      let boogieExpr := translateExpr cond
-      [Boogie.Statement.assume ("assume" ++ getNameFromMd md) boogieExpr md]
+      let boogieExpr := translateExpr env cond
+      (env, [Boogie.Statement.assume ("assume" ++ getNameFromMd md) boogieExpr md])
   | .Block stmts _ =>
-      stmts.flatMap (translateStmt outputParams)
+      let (env', stmtsList) := stmts.foldl (fun (e, acc) s =>
+        let (e', ss) := translateStmt e outputParams s
+        (e', acc ++ ss)) (env, [])
+      (env', stmtsList)
   | .LocalVariable name ty initializer =>
+      let env' := (name, ty) :: env
       let boogieMonoType := translateType ty
       let boogieType := LTy.forAll [] boogieMonoType
       let ident := Boogie.BoogieIdent.locl name
       match initializer with
+      | some (.StaticCall callee args) =>
+          -- Translate as: var name; call name := callee(args)
+          let boogieArgs := args.map (translateExpr env)
+          let defaultExpr := match ty with
+                            | .TInt => .const () (.intConst 0)
+                            | .TBool => .const () (.boolConst false)
+                            | _ => .const () (.intConst 0)
+          let initStmt := Boogie.Statement.init ident boogieType defaultExpr
+          let callStmt := Boogie.Statement.call [ident] callee boogieArgs
+          (env', [initStmt, callStmt])
       | some initExpr =>
-          let boogieExpr := translateExpr initExpr
-          [Boogie.Statement.init ident boogieType boogieExpr]
+          let boogieExpr := translateExpr env initExpr
+          (env', [Boogie.Statement.init ident boogieType boogieExpr])
       | none =>
-          -- Initialize with default value
           let defaultExpr := match ty with
                             | .TInt => .const () (.intConst 0)
                             | .TBool => .const () (.boolConst false)
                             | _ => .const () (.intConst 0)
-          [Boogie.Statement.init ident boogieType defaultExpr]
-  | .Assign target value =>
+          (env', [Boogie.Statement.init ident boogieType defaultExpr])
+  | .Assign target value _ =>
       match target with
       | .Identifier name =>
           let ident := Boogie.BoogieIdent.locl name
-          let boogieExpr := translateExpr value
-          [Boogie.Statement.set ident boogieExpr]
-      | _ => []  -- Can only assign to simple identifiers
+          let boogieExpr := translateExpr env value
+          (env, [Boogie.Statement.set ident boogieExpr])
+      | _ => (env, [])
   | .IfThenElse cond thenBranch elseBranch =>
-      let bcond := translateExpr cond
-      let bthen := translateStmt outputParams thenBranch
+      let bcond := translateExpr env cond
+      let (_, bthen) := translateStmt env outputParams thenBranch
       let belse := match elseBranch with
-                  | some e => translateStmt outputParams e
+                  | some e => (translateStmt env outputParams e).2
                   | none => []
-      -- Use Boogie's if-then-else construct
-      [Imperative.Stmt.ite bcond bthen belse .empty]
+      (env, [Imperative.Stmt.ite bcond bthen belse .empty])
   | .StaticCall name args =>
-      let boogieArgs := args.map translateExpr
-      [Boogie.Statement.call [] name boogieArgs]
+      let boogieArgs := args.map (translateExpr env)
+      (env, [Boogie.Statement.call [] name boogieArgs])
   | .Return valueOpt =>
-      -- In Boogie, returns are done by assigning to output parameters
       match valueOpt, outputParams.head? with
       | some value, some outParam =>
-          -- Assign to the first output parameter, then assume false for no fallthrough
           let ident := Boogie.BoogieIdent.locl outParam.name
-          let boogieExpr := translateExpr value
+          let boogieExpr := translateExpr env value
           let assignStmt := Boogie.Statement.set ident boogieExpr
           let noFallThrough := Boogie.Statement.assume "return" (.const () (.boolConst false)) .empty
-          [assignStmt, noFallThrough]
+          (env, [assignStmt, noFallThrough])
       | none, _ =>
-          -- Return with no value - just indicate no fallthrough
           let noFallThrough := Boogie.Statement.assume "return" (.const () (.boolConst false)) .empty
-          [noFallThrough]
+          (env, [noFallThrough])
       | some _, none =>
-          -- Error: trying to return a value but no output parameters
           panic! "Return statement with value but procedure has no output parameters"
-  | _ => panic! Std.Format.pretty (Std.ToFormat.format stmt)
+  | _ => (env, [])
 
 /--
 Translate Laurel Parameter to Boogie Signature entry
@@ -168,65 +189,257 @@ def translateParameterToBoogie (param : Parameter) : (Boogie.BoogieIdent × LMon
 /--
 Translate Laurel Procedure to Boogie Procedure
 -/
-def translateProcedure (proc : Procedure) : Boogie.Procedure :=
-  -- Translate input parameters
-  let inputPairs := proc.inputs.map translateParameterToBoogie
+def translateProcedure (constants : List Constant) (proc : Procedure) : Boogie.Procedure :=
+  -- Check if this procedure has a heap parameter (first input named "heap")
+  let hasHeapParam := proc.inputs.any (fun p => p.name == "heap" && p.type == .THeap)
+  -- Rename heap input to heap_in if present
+  let renamedInputs := proc.inputs.map (fun p =>
+    if p.name == "heap" && p.type == .THeap then { p with name := "heap_in" } else p)
+  let inputPairs := renamedInputs.map translateParameterToBoogie
   let inputs := inputPairs
-
   let header : Boogie.Procedure.Header := {
     name := proc.name
     typeArgs := []
     inputs := inputs
     outputs := proc.outputs.map translateParameterToBoogie
   }
+  let initEnv : TypeEnv := proc.inputs.map (fun p => (p.name, p.type)) ++
+                           proc.outputs.map (fun p => (p.name, p.type)) ++
+                           constants.map (fun c => (c.name, c.type))
+  -- Translate precondition if it's not just LiteralBool true
+  let preconditions : ListMap Boogie.BoogieLabel Boogie.Procedure.Check :=
+    match proc.precondition with
+    | .LiteralBool true => []
+    | precond =>
+        let check : Boogie.Procedure.Check := { expr := translateExpr initEnv precond }
+        [("requires", check)]
+  -- Translate postcondition for Opaque bodies
+  let postconditions : ListMap Boogie.BoogieLabel Boogie.Procedure.Check :=
+    match proc.body with
+    | .Opaque postcond _ _ _ =>
+        let check : Boogie.Procedure.Check := { expr := translateExpr initEnv postcond }
+        [("ensures", check)]
+    | _ => []
   let spec : Boogie.Procedure.Spec := {
     modifies := []
-    preconditions := []
-    postconditions := []
+    preconditions := preconditions
+    postconditions := postconditions
   }
+  -- If we have a heap parameter, add initialization: var heap := heap_in
+  let heapInit : List Boogie.Statement :=
+    if hasHeapParam then
+      let heapTy := LMonoTy.tcons "Heap" []
+      let heapType := LTy.forAll [] heapTy
+      let heapIdent := Boogie.BoogieIdent.locl "heap"
+      let heapInExpr := LExpr.fvar () (Boogie.BoogieIdent.locl "heap_in") (some heapTy)
+      [Boogie.Statement.init heapIdent heapType heapInExpr]
+    else []
   let body : List Boogie.Statement :=
     match proc.body with
-    | .Transparent bodyExpr => translateStmt proc.outputs bodyExpr
-    | _ => []  -- TODO: handle Opaque and Abstract bodies
+    | .Transparent bodyExpr => heapInit ++ (translateStmt initEnv proc.outputs bodyExpr).2
+    | .Opaque _postcond (some impl) _ _ => heapInit ++ (translateStmt initEnv proc.outputs impl).2
+    | _ => []
   {
     header := header
     spec := spec
     body := body
   }
 
+def heapTypeDecl : Boogie.Decl := .type (.con { name := "Heap", numargs := 0 })
+def fieldTypeDecl : Boogie.Decl := .type (.con { name := "Field", numargs := 1 })
+def compositeTypeDecl : Boogie.Decl := .type (.con { name := "Composite", numargs := 0 })
+
+def readFunction : Boogie.Decl :=
+  let heapTy := LMonoTy.tcons "Heap" []
+  let compTy := LMonoTy.tcons "Composite" []
+  let tVar := LMonoTy.ftvar "T"
+  let fieldTy := LMonoTy.tcons "Field" [tVar]
+  .func {
+    name := Boogie.BoogieIdent.glob "heapRead"
+    typeArgs := ["T"]
+    inputs := [(Boogie.BoogieIdent.locl "heap", heapTy),
+               (Boogie.BoogieIdent.locl "obj", compTy),
+               (Boogie.BoogieIdent.locl "field", fieldTy)]
+    output := tVar
+    body := none
+  }
+
+def updateFunction : Boogie.Decl :=
+  let heapTy := LMonoTy.tcons "Heap" []
+  let compTy := LMonoTy.tcons "Composite" []
+  let tVar := LMonoTy.ftvar "T"
+  let fieldTy := LMonoTy.tcons "Field" [tVar]
+  .func {
+    name := Boogie.BoogieIdent.glob "heapStore"
+    typeArgs := ["T"]
+    inputs := [(Boogie.BoogieIdent.locl "heap", heapTy),
+               (Boogie.BoogieIdent.locl "obj", compTy),
+               (Boogie.BoogieIdent.locl "field", fieldTy),
+               (Boogie.BoogieIdent.locl "val", tVar)]
+    output := heapTy
+    body := none
+  }
+
+-- Axiom: forall h, o, f, v :: heapRead(heapStore(h, o, f, v), o, f) == v
+-- Using int for field values since Boogie doesn't support polymorphism in axioms
+def readUpdateSameAxiom : Boogie.Decl :=
+  let heapTy := LMonoTy.tcons "Heap" []
+  let compTy := LMonoTy.tcons "Composite" []
+  let fieldTy := LMonoTy.tcons "Field" [LMonoTy.int]
+  -- Build: heapRead(heapStore(h, o, f, v), o, f) == v using de Bruijn indices
+  -- Quantifier order (outer to inner): int (v), Field int (f), Composite (o), Heap (h)
+  -- So: h is bvar 0, o is bvar 1, f is bvar 2, v is bvar 3
+  let h := LExpr.bvar () 0
+  let o := LExpr.bvar () 1
+  let f := LExpr.bvar () 2
+  let v := LExpr.bvar () 3
+  let updateOp := LExpr.op () (Boogie.BoogieIdent.glob "heapStore") none
+  let readOp := LExpr.op () (Boogie.BoogieIdent.glob "heapRead") none
+  let updateExpr := LExpr.mkApp () updateOp [h, o, f, v]
+  let readExpr := LExpr.mkApp () readOp [updateExpr, o, f]
+  let eqBody := LExpr.eq () readExpr v
+  -- Wrap in foralls: forall v:int, f:Field int, o:Composite, h:Heap
+  let body := LExpr.all () (some LMonoTy.int) <|
+              LExpr.all () (some fieldTy) <|
+              LExpr.all () (some compTy) <|
+              LExpr.all () (some heapTy) eqBody
+  .ax { name := "heapRead_heapStore_same", e := body }
+
+-- Axiom: forall h, o1, o2, f, v :: o1 != o2 ==> heapRead(heapStore(h, o1, f, v), o2, f) == heapRead(h, o2, f)
+-- Using int for field values since Boogie doesn't support polymorphism in axioms
+def readUpdateDiffObjAxiom : Boogie.Decl :=
+  let heapTy := LMonoTy.tcons "Heap" []
+  let compTy := LMonoTy.tcons "Composite" []
+  let fieldTy := LMonoTy.tcons "Field" [LMonoTy.int]
+  -- Quantifier order (outer to inner): int (v), Field int (f), Composite (o2), Composite (o1), Heap (h)
+  -- So: h is bvar 0, o1 is bvar 1, o2 is bvar 2, f is bvar 3, v is bvar 4
+  let h := LExpr.bvar () 0
+  let o1 := LExpr.bvar () 1
+  let o2 := LExpr.bvar () 2
+  let f := LExpr.bvar () 3
+  let v := LExpr.bvar () 4
+  let updateOp := LExpr.op () (Boogie.BoogieIdent.glob "heapStore") none
+  let readOp := LExpr.op () (Boogie.BoogieIdent.glob "heapRead") none
+  let updateExpr := LExpr.mkApp () updateOp [h, o1, f, v]
+  let lhs := LExpr.mkApp () readOp [updateExpr, o2, f]
+  let rhs := LExpr.mkApp () readOp [h, o2, f]
+  let neq := LExpr.app () boolNotOp (LExpr.eq () o1 o2)
+  let implBody := LExpr.app () (LExpr.app () Boogie.boolImpliesOp neq) (LExpr.eq () lhs rhs)
+  let body := LExpr.all () (some LMonoTy.int) <|
+              LExpr.all () (some fieldTy) <|
+              LExpr.all () (some compTy) <|
+              LExpr.all () (some compTy) <|
+              LExpr.all () (some heapTy) implBody
+  .ax { name := "heapRead_heapStore_diff_obj", e := body }
+
+def translateConstant (c : Constant) : Boogie.Decl :=
+  let ty := translateType c.type
+  .func {
+    name := Boogie.BoogieIdent.glob c.name
+    typeArgs := []
+    inputs := []
+    output := ty
+    body := none
+  }
+
+/--
+Check if a StmtExpr is a pure expression (can be used as a Boogie function body).
+Pure expressions don't contain statements like assignments, loops, or local variables.
+A Block with a single pure expression is also considered pure.
+-/
+def isPureExpr : StmtExpr → Bool
+  | .LiteralBool _ => true
+  | .LiteralInt _ => true
+  | .Identifier _ => true
+  | .PrimitiveOp _ args => args.attach.all (fun ⟨a, _⟩ => isPureExpr a)
+  | .IfThenElse c t none => isPureExpr c && isPureExpr t
+  | .IfThenElse c t (some e) => isPureExpr c && isPureExpr t && isPureExpr e
+  | .StaticCall _ args => args.attach.all (fun ⟨a, _⟩ => isPureExpr a)
+  | .ReferenceEquals e1 e2 => isPureExpr e1 && isPureExpr e2
+  | .Block [single] _ => isPureExpr single
+  | _ => false
+termination_by e => sizeOf e
+
+/--
+Check if a procedure can be translated as a Boogie function.
+A procedure can be a function if:
+- It has a transparent body that is a pure expression
+- It has no precondition (or just `true`)
+- It has exactly one output parameter (the return type)
+-/
+def canBeBoogieFunction (proc : Procedure) : Bool :=
+  match proc.body with
+  | .Transparent bodyExpr =>
+    isPureExpr bodyExpr &&
+    (match proc.precondition with | .LiteralBool true => true | _ => false) &&
+    proc.outputs.length == 1
+  | _ => false
+
+/--
+Translate a Laurel Procedure to a Boogie Function (when applicable)
+-/
+def translateProcedureToFunction (proc : Procedure) : Boogie.Decl :=
+  let inputs := proc.inputs.map translateParameterToBoogie
+  let outputTy := match proc.outputs.head? with
+    | some p => translateType p.type
+    | none => LMonoTy.int
+  let initEnv : TypeEnv := proc.inputs.map (fun p => (p.name, p.type))
+  let body := match proc.body with
+    | .Transparent bodyExpr => some (translateExpr initEnv bodyExpr)
+    | _ => none
+  .func {
+    name := Boogie.BoogieIdent.glob proc.name
+    typeArgs := []
+    inputs := inputs
+    output := outputTy
+    body := body
+  }
+
 /--
 Translate Laurel Program to Boogie Program
 -/
-def translate (program : Program) : Boogie.Program :=
-  -- First, sequence all assignments (move them out of expression positions)
-  let sequencedProgram := liftExpressionAssignments program
-  dbg_trace "=== Sequenced program Program ==="
-  dbg_trace (toString (Std.Format.pretty (Std.ToFormat.format sequencedProgram)))
-  dbg_trace "================================="
-  -- Then translate to Boogie
-  let procedures := sequencedProgram.staticProcedures.map translateProcedure
-  let decls := procedures.map (fun p => Boogie.Decl.proc p .empty)
-  { decls := decls }
+def translate (program : Program) : Except (Array DiagnosticModel) Boogie.Program := do
+  let sequencedProgram ← liftExpressionAssignments program
+  let heapProgram := heapParameterization sequencedProgram
+  -- Separate procedures that can be functions from those that must be procedures
+  let (funcProcs, procProcs) := heapProgram.staticProcedures.partition canBeBoogieFunction
+  let procedures := procProcs.map (translateProcedure heapProgram.constants)
+  let procDecls := procedures.map (fun p => Boogie.Decl.proc p .empty)
+  let laurelFuncDecls := funcProcs.map translateProcedureToFunction
+  let constDecls := heapProgram.constants.map translateConstant
+  let typeDecls := [heapTypeDecl, fieldTypeDecl, compositeTypeDecl]
+  let funcDecls := [readFunction, updateFunction]
+  let axiomDecls := [readUpdateSameAxiom, readUpdateDiffObjAxiom]
+  return { decls := typeDecls ++ funcDecls ++ axiomDecls ++ constDecls ++ laurelFuncDecls ++ procDecls }
 
 /--
 Verify a Laurel program using an SMT solver
 -/
 def verifyToVcResults (smtsolver : String) (program : Program)
-    (options : Options := Options.default) : IO VCResults := do
-  let boogieProgram := translate program
+    (options : Options := Options.default) : IO (Except (Array DiagnosticModel) VCResults) := do
+  let boogieProgramExcept := translate program
   -- Debug: Print the generated Boogie program
-  dbg_trace "=== Generated Boogie Program ==="
-  dbg_trace (toString (Std.Format.pretty (Std.ToFormat.format boogieProgram)))
-  dbg_trace "================================="
-  EIO.toIO (fun f => IO.Error.userError (toString f))
-      (Boogie.verify smtsolver boogieProgram options)
+  match boogieProgramExcept with
+    | .error e => return .error e
+    | .ok boogieProgram =>
+      dbg_trace "=== Generated Boogie Program ==="
+      dbg_trace (toString (Std.Format.pretty (Std.ToFormat.format boogieProgram)))
+      dbg_trace "================================="
+      let ioResult <- EIO.toIO (fun f => IO.Error.userError (toString f))
+          (Boogie.verify smtsolver boogieProgram options)
+      return .ok ioResult
 
 def verifyToDiagnostics (smtsolver : String) (files: Map Strata.Uri Lean.FileMap) (program : Program): IO (Array Diagnostic) := do
   let results <- verifyToVcResults smtsolver program
-  return results.filterMap (toDiagnostic files)
+  match results with
+  | .error errors => return errors.map (fun dm => dm.toDiagnostic files)
+  | .ok results => return results.filterMap (fun dm => dm.toDiagnostic files)
+
 
 def verifyToDiagnosticModels (smtsolver : String) (program : Program): IO (Array DiagnosticModel) := do
   let results <- verifyToVcResults smtsolver program
-  return results.filterMap toDiagnosticModel
+  match results with
+  | .error errors => return errors
+  | .ok results => return results.filterMap toDiagnosticModel
 
 end Laurel
diff --git a/Strata/Languages/Laurel/LiftExpressionAssignments.lean b/Strata/Languages/Laurel/LiftExpressionAssignments.lean
index 0221e4d40..8307bd68f 100644
--- a/Strata/Languages/Laurel/LiftExpressionAssignments.lean
+++ b/Strata/Languages/Laurel/LiftExpressionAssignments.lean
@@ -5,7 +5,11 @@
 -/
 
 import Strata.Languages.Laurel.Laurel
+import Strata.Languages.Laurel.LaurelFormat
+import Strata.Languages.Boogie.Verifier
 
+
+namespace Strata
 namespace Laurel
 
 /-
@@ -23,7 +27,9 @@ Becomes:
 -/
 
 structure SequenceState where
+  insideCondition : Bool
   prependedStmts : List StmtExpr := []
+  diagnostics : List DiagnosticModel
   tempCounter : Nat := 0
 
 abbrev SequenceM := StateM SequenceState
@@ -31,6 +37,21 @@ abbrev SequenceM := StateM SequenceState
 def SequenceM.addPrependedStmt (stmt : StmtExpr) : SequenceM Unit :=
   modify fun s => { s with prependedStmts := stmt :: s.prependedStmts }
 
+def SequenceM.addDiagnostic (d : DiagnosticModel) : SequenceM Unit :=
+  modify fun s => { s with diagnostics := d :: s.diagnostics }
+
+def checkOutsideCondition(md: Imperative.MetaData Boogie.Expression): SequenceM Unit := do
+  let state <- get
+  if state.insideCondition then
+    let fileRange := (Imperative.getFileRange md).get!
+    SequenceM.addDiagnostic {
+        fileRange := fileRange,
+        message := "Could not lift assigment in expression that is evaluated conditionally"
+    }
+
+def SequenceM.setInsideCondition : SequenceM Unit := do
+  modify fun s => { s with insideCondition := true }
+
 def SequenceM.takePrependedStmts : SequenceM (List StmtExpr) := do
   let stmts := (← get).prependedStmts
   modify fun s => { s with prependedStmts := [] }
@@ -48,12 +69,13 @@ Returns the transformed expression with assignments replaced by variable referen
 -/
 def transformExpr (expr : StmtExpr) : SequenceM StmtExpr := do
   match expr with
-  | .Assign target value =>
+  | .Assign target value md =>
+      checkOutsideCondition md
       -- This is an assignment in expression context
       -- We need to: 1) execute the assignment, 2) capture the value in a temporary
       -- This prevents subsequent assignments to the same variable from changing the value
       let seqValue ← transformExpr value
-      let assignStmt := StmtExpr.Assign target seqValue
+      let assignStmt := StmtExpr.Assign target seqValue md
       SequenceM.addPrependedStmt assignStmt
       -- Create a temporary variable to capture the assigned value
       -- Use TInt as the type (could be refined with type inference)
@@ -69,6 +91,7 @@ def transformExpr (expr : StmtExpr) : SequenceM StmtExpr := do
 
   | .IfThenElse cond thenBranch elseBranch =>
       let seqCond ← transformExpr cond
+      SequenceM.setInsideCondition
       let seqThen ← transformExpr thenBranch
       let seqElse ← match elseBranch with
         | some e => transformExpr e >>= (pure ∘ some)
@@ -129,14 +152,16 @@ def transformStmt (stmt : StmtExpr) : SequenceM (List StmtExpr) := do
       | none =>
           return [stmt]
 
-  | .Assign target value =>
-      -- Top-level assignment (statement context)
+  | .Assign target value md =>
       let seqTarget ← transformExpr target
       let seqValue ← transformExpr value
-      SequenceM.addPrependedStmt <| .Assign seqTarget seqValue
+      SequenceM.addPrependedStmt <| .Assign seqTarget seqValue md
       SequenceM.takePrependedStmts
 
   | .IfThenElse cond thenBranch elseBranch =>
+      let seqCond ← transformExpr cond
+      SequenceM.setInsideCondition
+
       let seqThen ← transformStmt thenBranch
       let thenBlock := .Block seqThen none
 
@@ -146,7 +171,6 @@ def transformStmt (stmt : StmtExpr) : SequenceM (List StmtExpr) := do
             pure (some (.Block se none))
         | none => pure none
 
-      let seqCond ← transformExpr cond
       SequenceM.addPrependedStmt <| .IfThenElse seqCond thenBlock seqElse
       SequenceM.takePrependedStmts
 
@@ -160,24 +184,28 @@ def transformStmt (stmt : StmtExpr) : SequenceM (List StmtExpr) := do
 
 end
 
-def transformProcedureBody (body : StmtExpr) : StmtExpr :=
-  let (seqStmts, _) := transformStmt body |>.run {}
+def transformProcedureBody (body : StmtExpr) : SequenceM StmtExpr := do
+  let seqStmts <- transformStmt body
   match seqStmts with
-  | [single] => single
-  | multiple => .Block multiple.reverse none
+  | [single] => pure single
+  | multiple => pure <| .Block multiple.reverse none
 
-def transformProcedure (proc : Procedure) : Procedure :=
+def transformProcedure (proc : Procedure) : SequenceM Procedure := do
   match proc.body with
   | .Transparent bodyExpr =>
-      let seqBody := transformProcedureBody bodyExpr
-      { proc with body := .Transparent seqBody }
-  | _ => proc  -- Opaque and Abstract bodies unchanged
+      let seqBody <- transformProcedureBody bodyExpr
+      pure { proc with body := .Transparent seqBody }
+  | _ => pure proc  -- Opaque and Abstract bodies unchanged
 
 /--
 Transform a program to lift all assignments that occur in an expression context.
 -/
-def liftExpressionAssignments (program : Program) : Program :=
-  let seqProcedures := program.staticProcedures.map transformProcedure
-  { program with staticProcedures := seqProcedures }
+def liftExpressionAssignments (program : Program) : Except (Array DiagnosticModel) Program :=
+  let (seqProcedures, afterState) := (program.staticProcedures.mapM transformProcedure).run
+    { insideCondition := false, diagnostics := [] }
+  if !afterState.diagnostics.isEmpty then
+    .error afterState.diagnostics.toArray
+  else
+    .ok { program with staticProcedures := seqProcedures }
 
 end Laurel
diff --git a/StrataMain.lean b/StrataMain.lean
index 760a94c1f..0fc90fab1 100644
--- a/StrataMain.lean
+++ b/StrataMain.lean
@@ -257,7 +257,7 @@ def laurelAnalyzeCommand : Command where
 
     let strataFiles ← deserializeIonToLaurelFiles stdinBytes
 
-    let mut combinedProgram : Laurel.Program := {
+    let mut combinedProgram : Strata.Laurel.Program := {
       staticProcedures := []
       staticFields := []
       types := []
@@ -265,7 +265,7 @@ def laurelAnalyzeCommand : Command where
 
     for strataFile in strataFiles do
 
-      let transResult := Laurel.TransM.run (Strata.Uri.file strataFile.filePath) (Laurel.parseProgram strataFile.program)
+      let transResult := Strata.Laurel.TransM.run (Strata.Uri.file strataFile.filePath) (Strata.Laurel.parseProgram strataFile.program)
       match transResult with
       | .error transErrors => exitFailure s!"Translation errors in {strataFile.filePath}: {transErrors}"
       | .ok laurelProgram =>
@@ -276,7 +276,7 @@ def laurelAnalyzeCommand : Command where
           types := combinedProgram.types ++ laurelProgram.types
         }
 
-    let diagnostics ← Laurel.verifyToDiagnosticModels "z3" combinedProgram
+    let diagnostics ← Strata.Laurel.verifyToDiagnosticModels "z3" combinedProgram
 
     IO.println s!"==== DIAGNOSTICS ===="
     for diag in diagnostics do
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T1_AssertFalse.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T1_AssertFalse.lean
index 05e80d79c..79f93745f 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T1_AssertFalse.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T1_AssertFalse.lean
@@ -8,7 +8,6 @@ import StrataTest.Util.TestDiagnostics
 import StrataTest.Languages.Laurel.TestExamples
 
 open StrataTest.Util
-open Strata
 
 namespace Strata
 namespace Laurel
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
index a35a49baf..59be97e3b 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
@@ -10,21 +10,16 @@ import StrataTest.Languages.Laurel.TestExamples
 open StrataTest.Util
 open Strata
 
-namespace Strata
-namespace Laurel
+namespace Strata.Laurel
 
 def program: String := r"
-procedure nestedImpureStatements(x: int) {
+procedure NestedImpureStatements() {
   var y := 0;
-  if (y := y + 1; == { y := y + 1; x }) {
-    assert x == 1;
-    assert y == x + 1;
-  } else {
-    assert x != 1;
-  }
-  assert y == 2;
-    assert false;
-//  ^^^^^^^^^^^^^ error: assertion does not hold
+  var x := y;
+  var z := y := y + 1;;
+    assert x == y;
+//  ^^^^^^^^^^^^^^ error: assertion does not hold
+  assert z == y;
 }
 "
 
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsNotSupported.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsNotSupported.lean
new file mode 100644
index 000000000..cb3ad8d2c
--- /dev/null
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsNotSupported.lean
@@ -0,0 +1,32 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import StrataTest.Util.TestDiagnostics
+import StrataTest.Languages.Laurel.TestExamples
+
+open StrataTest.Util
+open Strata
+
+namespace Strata.Laurel
+
+def program: String := r"
+procedure conditionalAssignmentInExpression(x: int) {
+  var y := 0;
+  var z := if (x > 0) { y := y + 1; } else { 0 };
+//                      ^^^^^^^^^^^ error: Could not lift assigment in expression that is evaluated conditionally
+  if (x > 0) {
+    assert y == 1;
+  } else {
+    assert z == 0;
+    assert y == 0;
+  }
+}
+"
+
+#eval! testInputWithOffset "T2_ImpureExpressionsNotSupported" program 14 processLaurelFile
+
+
+end Laurel
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCallsBoogie.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCallsBoogie.lean
new file mode 100644
index 000000000..4b7e75ab8
--- /dev/null
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCallsBoogie.lean
@@ -0,0 +1,48 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+/-
+The purpose of this test is to ensure we're using functions and procedures as well as
+Strata Boogie supports them. When Strata Core makes procedures more powerful, so we
+won't need functions any more, then this test can be merged into other tests.
+-/
+
+import StrataTest.Util.TestDiagnostics
+import StrataTest.Languages.Laurel.TestExamples
+
+open StrataTest.Util
+open Strata
+
+namespace Strata.Laurel
+
+def program := r"
+procedure syntacticallyABoogieFunction(x: int): int {
+  x + 1
+}
+
+procedure noFunctionBecauseContract() returns (r: int)
+  ensures r > 0
+{
+  10
+}
+
+procedure noFunctionBecauseStatements(): int {
+  var x: int := 3;
+  x + 1
+}
+
+procedure caller() {
+  assert syntacticallyABoogieFunction(1) == 2;
+  var x: int := noFunctionBecauseContract();
+  assert x > 0;
+  var y: int := noFunctionBecauseStatements();
+    assert y == 4;
+//. ^^^^^^^^^^^^^^ error: assertion could not be proved
+}
+"
+
+#guard_msgs(drop info, error) in
+#eval! testInputWithOffset "T5_ProcedureCallsBoogie" program 20 processLaurelFile
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/1. ImmutableFields.lr.st b/StrataTest/Languages/Laurel/Examples/Objects/2. ImmutableFields.lr.st
similarity index 100%
rename from StrataTest/Languages/Laurel/Examples/Objects/1. ImmutableFields.lr.st
rename to StrataTest/Languages/Laurel/Examples/Objects/2. ImmutableFields.lr.st
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/2. MutableFields.lr.st b/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean
similarity index 53%
rename from StrataTest/Languages/Laurel/Examples/Objects/2. MutableFields.lr.st
rename to StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean
index d1b328172..a4a8054ee 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/2. MutableFields.lr.st	
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean
@@ -1,30 +1,50 @@
-/*
+/-
   Copyright Strata Contributors
 
   SPDX-License-Identifier: Apache-2.0 OR MIT
-*/
+-/
 
+import StrataTest.Util.TestDiagnostics
+import StrataTest.Languages.Laurel.TestExamples
+
+open StrataTest.Util
+
+namespace Strata
+namespace Laurel
+
+def program := r"
 composite Container {
   var value: int // var indicates mutable field
 }
 
-procedure foo(c: Container, d: Container): int
+procedure foo(c: Container, d: Container) returns (r: int)
   requires c != d
-{ 
-  var x = c.value;
-  d.value = d.value + 1;
-  assert x == c.value; // pass
-}
+{
+  var x: int := c#value;
+  var initialDValue: int := d#value;
+  d#value := d#value + 1;
+  c#value := c#value + 1;
+  assert x + 1 == c#value; // pass
+  assert initialDValue + 1 == d#value;
 
-procedure caller(c: Container, d: Container) {
-  var x = foo(c, d);
+  var e: Container := d;
+  e#value := e#value + 1;
+  assert e#value == d#value;
 }
 
-procedure impureContract(c: Container)
-  ensures foo(c, c) 
-//           ^ error: a procedure that modifies the heap may not be called in pure context.
+// The following two need support for calling procedures in an expression context.
+//procedure caller(c: Container, d: Container) {
+//  var x: int := foo(c, d);
+//}
+
+//procedure impureContract(c: Container) {
+//  assert foo(c,c) == 3;
+//}
+"
+
+#eval testInputWithOffset "MutableFields" program 14 processLaurelFile
 
-/*
+/-
 Translation towards SMT:
 
 type Composite;
@@ -64,4 +84,4 @@ proof caller {
   (x, heap) = foo(heap, c, d);
   heap_out = heap;
 }
-*/
\ No newline at end of file
+-/
diff --git a/StrataTest/Languages/Laurel/TestExamples.lean b/StrataTest/Languages/Laurel/TestExamples.lean
index f1f070751..1b5c61586 100644
--- a/StrataTest/Languages/Laurel/TestExamples.lean
+++ b/StrataTest/Languages/Laurel/TestExamples.lean
@@ -17,8 +17,7 @@ open Strata
 open Strata.Elab (parseStrataProgramFromDialect)
 open Lean.Parser (InputContext)
 
-namespace Strata
-namespace Laurel
+namespace Strata.Laurel
 
 def processLaurelFile (input : InputContext) : IO (Array Diagnostic) := do
   let dialects := Strata.Elab.LoadedDialects.ofDialects! #[initDialect, Laurel]