diff --git a/Strata/DDM/Elab.lean b/Strata/DDM/Elab.lean
index 3be3407626..455af5073f 100644
--- a/Strata/DDM/Elab.lean
+++ b/Strata/DDM/Elab.lean
@@ -390,22 +390,17 @@ def elabDialect
   | .dialect loc dialect =>
     elabDialectRest fm dialects #[] inputContext loc dialect startPos stopPos
 
-def parseStrataProgramFromDialect (dialects : LoadedDialects) (dialect : DialectName) (filePath : String) : IO (InputContext × Strata.Program) := do
-  let bytes ← Strata.Util.readBinInputSource filePath
-  let fileContent ← match String.fromUTF8? bytes with
-    | some s => pure s
-    | none => throw (IO.userError s!"File {filePath} contains non UTF-8 data")
+def parseStrataProgramFromDialect (dialects : LoadedDialects) (dialect : DialectName) (input : InputContext) : IO Strata.Program := do
 
   let leanEnv ← Lean.mkEmptyEnvironment 0
-  let inputContext := Strata.Parser.stringInputContext filePath fileContent
 
   let isTrue mem := inferInstanceAs (Decidable (dialect ∈ dialects.dialects))
     | throw <| IO.userError "Internal {dialect} missing from loaded dialects."
 
   let strataProgram ←
-    match elabProgramRest dialects leanEnv inputContext dialect mem 0 with
+    match elabProgramRest dialects leanEnv input dialect mem 0 with
     | .ok program =>
-      pure (inputContext, program)
+      pure program
     | .error errors =>
       let errMsg ← errors.foldlM (init := "Parse errors:\n") fun msg e =>
         return s!"{msg}  {e.pos.line}:{e.pos.column}: {← e.data.toString}\n"
diff --git a/Strata/DL/Imperative/MetaData.lean b/Strata/DL/Imperative/MetaData.lean
index a85dee6275..3364a5fa8e 100644
--- a/Strata/DL/Imperative/MetaData.lean
+++ b/Strata/DL/Imperative/MetaData.lean
@@ -67,7 +67,7 @@ instance [Repr P.Ident] : Repr (MetaDataElem.Field P) where
 
 inductive Uri where
   | file (path: String)
-  deriving DecidableEq
+  deriving DecidableEq, Repr
 
 instance : ToFormat Uri where
  format fr := match fr with | .file path => path
@@ -76,7 +76,7 @@ structure FileRange where
   file: Uri
   start: Lean.Position
   ending: Lean.Position
-  deriving DecidableEq
+  deriving DecidableEq, Repr
 
 instance : ToFormat FileRange where
  format fr := f!"{fr.file}:{fr.start}-{fr.ending}"
@@ -100,7 +100,7 @@ instance [Repr P.Expr] : Repr (MetaDataElem.Value P) where
       match v with
       | .expr e => f!"MetaDataElem.Value.expr {reprPrec e prec}"
       | .msg s => f!"MetaDataElem.Value.msg {s}"
-      | .fileRange fr => f!"MetaDataElem.Value.fileRange {fr}"
+      | .fileRange fr => f!"MetaDataElem.Value.fileRange {repr fr}"
     Repr.addAppParen res prec
 
 def MetaDataElem.Value.beq [BEq P.Expr] (v1 v2 : MetaDataElem.Value P) :=
diff --git a/Strata/Languages/Boogie/Verifier.lean b/Strata/Languages/Boogie/Verifier.lean
index 55e8fe49b1..aeb9f88f7a 100644
--- a/Strata/Languages/Boogie/Verifier.lean
+++ b/Strata/Languages/Boogie/Verifier.lean
@@ -113,7 +113,7 @@ instance : ToFormat Result where
 
 def VC_folder_name: String := "vcs"
 
-def runSolver (solver : String) (args : Array String) : IO String := do
+def runSolver (solver : String) (args : Array String) : IO IO.Process.Output := do
   let output ← IO.Process.output {
     cmd := solver
     args := args
@@ -121,14 +121,15 @@ def runSolver (solver : String) (args : Array String) : IO String := do
   -- dbg_trace f!"runSolver: exitcode: {repr output.exitCode}\n\
   --                         stderr: {repr output.stderr}\n\
   --                         stdout: {repr output.stdout}"
-  return output.stdout
+  return output
 
-def solverResult (vars : List (IdentT LMonoTy Visibility)) (ans : String)
+def solverResult (vars : List (IdentT LMonoTy Visibility)) (output: IO.Process.Output)
     (ctx : SMT.Context) (E : EncoderState) :
   Except Format Result := do
-  let pos := (ans.find (fun c => c == '\n')).byteIdx
-  let verdict := (ans.take pos).trim
-  let rest := ans.drop pos
+  let stdout := output.stdout
+  let pos := (stdout.find (fun c => c == '\n')).byteIdx
+  let verdict := (stdout.take pos).trim
+  let rest := stdout.drop pos
   match verdict with
   | "sat"     =>
     let rawModel ← getModel rest
@@ -141,7 +142,7 @@ def solverResult (vars : List (IdentT LMonoTy Visibility)) (ans : String)
     | .error _model_err => (.ok (.sat []))
   | "unsat"   =>  .ok .unsat
   | "unknown" =>  .ok .unknown
-  | _     =>  .error ans
+  | _     =>  .error (stdout ++ output.stderr)
 
 open Imperative
 
@@ -220,8 +221,8 @@ def dischargeObligation
   let _ ← solver.checkSat ids -- Will return unknown for Solver.fileWriter
   if options.verbose then IO.println s!"Wrote problem to {filename}."
   let flags := getSolverFlags options smtsolver
-  let solver_out ← runSolver smtsolver (#[filename] ++ flags)
-  match solverResult vars solver_out ctx estate with
+  let output ← runSolver smtsolver (#[filename] ++ flags)
+  match solverResult vars output ctx estate with
   | .error e => return .error e
   | .ok result => return .ok (result, estate)
 
@@ -382,7 +383,7 @@ def toDiagnostic (vcr : Boogie.VCResult) : Option Diagnostic := do
     | .fileRange range =>
       let message := match result with
         | .sat _ => "assertion does not hold"
-        | .unknown => "assertion verification result is unknown"
+        | .unknown => "assertion could not be proved"
         | .err msg => s!"verification error: {msg}"
         | _ => "verification failed"
       some {
diff --git a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
index 937f396846..dddb18df2a 100644
--- a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
+++ b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
@@ -12,7 +12,6 @@ import Strata.Languages.Boogie.Expressions
 
 namespace Laurel
 
-open Laurel
 open Std (ToFormat Format format)
 open Strata (QualifiedIdent Arg SourceRange)
 open Lean.Parser (InputContext)
@@ -20,17 +19,16 @@ open Imperative (MetaData Uri FileRange)
 
 structure TransState where
   inputCtx : InputContext
-  errors : Array String
 
-abbrev TransM := StateM TransState
+abbrev TransM := StateT TransState (Except String)
 
-def TransM.run (ictx : InputContext) (m : TransM α) : (α × Array String) :=
-  let (v, s) := StateT.run m { inputCtx := ictx, errors := #[] }
-  (v, s.errors)
+def TransM.run (ictx : InputContext) (m : TransM α) : Except String α :=
+  match StateT.run m { inputCtx := ictx } with
+  | .ok (v, _) => .ok v
+  | .error e => .error e
 
-def TransM.error [Inhabited α] (msg : String) : TransM α := do
-  modify fun s => { s with errors := s.errors.push msg }
-  return panic msg
+def TransM.error (msg : String) : TransM α :=
+  throw msg
 
 def SourceRange.toMetaData (ictx : InputContext) (sr : SourceRange) : Imperative.MetaData Boogie.Expression :=
   let file := ictx.fileName
@@ -64,26 +62,61 @@ def translateIdent (arg : Arg) : TransM Identifier := do
 def translateBool (arg : Arg) : TransM Bool := do
   match arg with
   | .expr (.fn _ name) =>
-    if name == q`Laurel.boolTrue then
-      return true
-    else if name == q`Laurel.boolFalse then
-      return false
-    else
-      TransM.error s!"translateBool expects boolTrue or boolFalse, got {repr name}"
+    match name with
+    | q`Laurel.boolTrue => return true
+    | q`Laurel.boolFalse => return false
+    | _ => TransM.error s!"translateBool expects boolTrue or boolFalse, got {repr name}"
   | .op op =>
-    if op.name == q`Laurel.boolTrue then
-      return true
-    else if op.name == q`Laurel.boolFalse then
-      return false
-    else
-      TransM.error s!"translateBool expects boolTrue or boolFalse, got {repr op.name}"
+    match op.name with
+    | q`Laurel.boolTrue => return true
+    | q`Laurel.boolFalse => return false
+    | _ => TransM.error s!"translateBool expects boolTrue or boolFalse, got {repr op.name}"
   | x => TransM.error s!"translateBool expects expression or operation, got {repr x}"
 
+instance : Inhabited HighType where
+  default := .TVoid
+
+instance : Inhabited Parameter where
+  default := { name := "", type := .TVoid }
+
+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}"
+  | _ => TransM.error s!"translateHighType expects operation"
+
+def translateNat (arg : Arg) : TransM Nat := do
+  let .num _ n := arg
+    | TransM.error s!"translateNat expects num literal"
+  return n
+
+def translateParameter (arg : Arg) : TransM Parameter := do
+  let .op op := arg
+    | TransM.error s!"translateParameter expects operation"
+  match op.name, op.args with
+  | q`Laurel.parameter, #[arg0, arg1] =>
+    let name ← translateIdent arg0
+    let paramType ← translateHighType arg1
+    return { name := name, type := paramType }
+  | q`Laurel.parameter, args =>
+    TransM.error s!"parameter needs two arguments, not {args.size}"
+  | _, _ =>
+    TransM.error s!"translateParameter expects parameter operation, got {repr op.name}"
+
+def translateParameters (arg : Arg) : TransM (List Parameter) := do
+  match arg with
+  | .commaSepList _ args =>
+    args.toList.mapM translateParameter
+  | _ => pure []
+
 instance : Inhabited Procedure where
   default := {
     name := ""
     inputs := []
-    output := .TVoid
+    outputs := []
     precondition := .LiteralBool true
     decreases := none
     determinism := Determinism.deterministic none
@@ -91,31 +124,88 @@ instance : Inhabited Procedure where
     body := .Transparent (.LiteralBool true)
   }
 
+def getBinaryOp? (name : QualifiedIdent) : Option Operation :=
+  match name with
+  | q`Laurel.add => some Operation.Add
+  | q`Laurel.eq => some Operation.Eq
+  | q`Laurel.neq => some Operation.Neq
+  | q`Laurel.gt => some Operation.Gt
+  | q`Laurel.lt => some Operation.Lt
+  | q`Laurel.le => some Operation.Leq
+  | q`Laurel.ge => some Operation.Geq
+  | _ => none
+
 mutual
 
 partial def translateStmtExpr (arg : Arg) : TransM StmtExpr := do
   match arg with
-  | .op op =>
-    if op.name == q`Laurel.assert then
-      let cond ← translateStmtExpr op.args[0]!
+  | .op op => match op.name, op.args with
+    | q`Laurel.assert, #[arg0] =>
+      let cond ← translateStmtExpr arg0
       let md ← getArgMetaData (.op op)
       return .Assert cond md
-    else if op.name == q`Laurel.assume then
-      let cond ← translateStmtExpr op.args[0]!
+    | q`Laurel.assume, #[arg0] =>
+      let cond ← translateStmtExpr arg0
       let md ← getArgMetaData (.op op)
       return .Assume cond md
-    else if op.name == q`Laurel.block then
-      let stmts ← translateSeqCommand op.args[0]!
+    | q`Laurel.block, #[arg0] =>
+      let stmts ← translateSeqCommand arg0
       return .Block stmts none
-    else if op.name == q`Laurel.literalBool then
-      let boolVal ← translateBool op.args[0]!
-      return .LiteralBool boolVal
-    else if op.name == q`Laurel.boolTrue then
-      return .LiteralBool true
-    else if op.name == q`Laurel.boolFalse then
-      return .LiteralBool false
-    else
-      TransM.error s!"Unknown operation: {op.name}"
+    | q`Laurel.boolTrue, _ => return .LiteralBool true
+    | q`Laurel.boolFalse, _ => return .LiteralBool false
+    | q`Laurel.int, #[arg0] =>
+      let n ← translateNat arg0
+      return .LiteralInt n
+    | q`Laurel.varDecl, #[arg0, typeArg, assignArg] =>
+      let name ← translateIdent arg0
+      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
+      let value ← match assignArg with
+        | .option _ (some (.op assignOp)) => match assignOp.args with
+          | #[assignArg0] => translateStmtExpr assignArg0 >>= (pure ∘ some)
+          | _ => TransM.error s!"assignArg {repr assignArg} didn't match expected pattern for variable {name}"
+        | .option _ none => pure none
+        | _ => TransM.error s!"assignArg {repr assignArg} didn't match expected pattern for variable {name}"
+      return .LocalVariable name varType value
+    | q`Laurel.identifier, #[arg0] =>
+      let name ← translateIdent arg0
+      return .Identifier name
+    | q`Laurel.parenthesis, #[arg0] => translateStmtExpr arg0
+    | q`Laurel.assign, #[arg0, arg1] =>
+      let target ← translateStmtExpr arg0
+      let value ← translateStmtExpr arg1
+      return .Assign target value
+    | q`Laurel.call, #[arg0, argsSeq] =>
+      let callee ← translateStmtExpr arg0
+      let calleeName := match callee with
+        | .Identifier name => name
+        | _ => ""
+      let argsList ← match argsSeq with
+        | .commaSepList _ args => args.toList.mapM translateStmtExpr
+        | _ => pure []
+      return .StaticCall calleeName argsList
+    | q`Laurel.return, #[arg0] =>
+      let value ← translateStmtExpr arg0
+      return .Return (some value)
+    | q`Laurel.ifThenElse, #[arg0, arg1, elseArg] =>
+      let cond ← translateStmtExpr arg0
+      let thenBranch ← translateStmtExpr arg1
+      let elseBranch ← match elseArg with
+        | .option _ (some (.op elseOp)) => match elseOp.name, elseOp.args with
+          | q`Laurel.optionalElse, #[elseArg0] => translateStmtExpr elseArg0 >>= (pure ∘ some)
+          | _, _ => pure none
+        | _ => pure none
+      return .IfThenElse cond thenBranch elseBranch
+    | _, #[arg0, arg1] => match getBinaryOp? op.name with
+      | some primOp =>
+        let lhs ← translateStmtExpr arg0
+        let rhs ← translateStmtExpr arg1
+        return .PrimitiveOp primOp [lhs, rhs]
+      | none => TransM.error s!"Unknown operation: {op.name}"
+    | _, _ => TransM.error s!"Unknown operation: {op.name}"
   | _ => TransM.error s!"translateStmtExpr expects operation"
 
 partial def translateSeqCommand (arg : Arg) : TransM (List StmtExpr) := do
@@ -135,20 +225,37 @@ end
 def parseProcedure (arg : Arg) : TransM Procedure := do
   let .op op := arg
     | TransM.error s!"parseProcedure expects operation"
-  let name ← translateIdent op.args[0]!
-  let body ← translateCommand op.args[1]!
-  return {
-    name := name
-    inputs := []
-    output := .TVoid
-    precondition := .LiteralBool true
-    decreases := none
-    determinism := Determinism.deterministic none
-    modifies := none
-    body := .Transparent body
-  }
 
-/- Translate concrete Laurel syntax into abstract Laurel syntax -/
+  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
+    return {
+      name := name
+      inputs := parameters
+      outputs := returnParameters
+      precondition := .LiteralBool true
+      decreases := none
+      determinism := Determinism.deterministic none
+      modifies := none
+      body := .Transparent body
+    }
+  | q`Laurel.procedure, args =>
+    TransM.error s!"parseProcedure expects 4 arguments, got {args.size}"
+  | _, _ =>
+    TransM.error s!"parseProcedure expects procedure, got {repr op.name}"
+
+/--
+Translate concrete Laurel syntax into abstract Laurel syntax
+-/
 def parseProgram (prog : Strata.Program) : TransM Laurel.Program := do
   -- Unwrap the program operation if present
   -- The parsed program may have a single `program` operation wrapping the procedures
diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
index 860a5b6757..54e60016b3 100644
--- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
+++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
@@ -10,21 +10,68 @@ import Strata
 #dialect
 dialect Laurel;
 
-
-// Boolean literals
-type bool;
-fn boolTrue : bool => "true";
-fn boolFalse : bool => "false";
+// Types
+category LaurelType;
+op intType : LaurelType => "int";
+op boolType : LaurelType => "bool";
 
 category StmtExpr;
-op literalBool (b: bool): StmtExpr => b;
 
-op assert (cond : StmtExpr) : StmtExpr => "assert " cond ";\n";
-op assume (cond : StmtExpr) : StmtExpr => "assume " cond ";\n";
-op block (stmts : Seq StmtExpr) : StmtExpr => @[prec(1000)] "{\n" stmts "}\n";
+op boolTrue() : StmtExpr => "true";
+op boolFalse() : StmtExpr => "false";
+op int(n : Num) : StmtExpr => n;
+
+// Variable declarations
+category OptionalType;
+op optionalType(varType: LaurelType): OptionalType => ":" varType;
+
+category OptionalAssignment;
+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 identifier (name: Ident): StmtExpr => name;
+op parenthesis (inner: StmtExpr): StmtExpr => "(" inner ")";
+
+// Assignment
+op assign (target: StmtExpr, value: StmtExpr): StmtExpr => target ":=" value ";";
+
+// Binary operators
+op add (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(60)] lhs "+" rhs;
+op eq (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs "==" rhs;
+op neq (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs "!=" rhs;
+op gt (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs ">" rhs;
+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;
+
+op ifThenElse (cond: StmtExpr, thenBranch: StmtExpr, elseBranch: Option OptionalElse): StmtExpr =>
+  @[prec(20)] "if (" cond ") " thenBranch:0 elseBranch:0;
+
+op assert (cond : StmtExpr) : StmtExpr => "assert " cond ";";
+op assume (cond : StmtExpr) : StmtExpr => "assume " cond ";";
+op return (value : StmtExpr) : StmtExpr => "return " value ";";
+op block (stmts : Seq StmtExpr) : StmtExpr => @[prec(1000)] "{" stmts "}";
+
+category Parameter;
+op parameter (name: Ident, paramType: LaurelType): Parameter => name ":" paramType;
+
+category ReturnParameters;
+op returnParameters(parameters: CommaSepBy Parameter): ReturnParameters => "returns" "(" parameters ")";
 
 category Procedure;
-op procedure (name : Ident, body : StmtExpr) : Procedure => "procedure " name "() " body:0;
+op procedure (name : Ident, parameters: CommaSepBy Parameter,
+  returnParameters: Option ReturnParameters,
+  body : StmtExpr) : Procedure =>
+  "procedure " name "(" parameters ")" returnParameters body:0;
 
 op program (staticProcedures: Seq Procedure): Command => staticProcedures;
 
diff --git a/Strata/Languages/Laurel/Laurel.lean b/Strata/Languages/Laurel/Laurel.lean
index 5ee4b22a4a..b113a13ba7 100644
--- a/Strata/Languages/Laurel/Laurel.lean
+++ b/Strata/Languages/Laurel/Laurel.lean
@@ -6,6 +6,7 @@
 
 import Strata.DL.Imperative.MetaData
 import Strata.Languages.Boogie.Expressions
+import Strata.Languages.Boogie.Procedure
 
 /-
 The Laurel language is supposed to serve as an intermediate verification language for at least Java, Python, JavaScript.
@@ -46,11 +47,24 @@ namespace Laurel
 
 abbrev Identifier := String /- Potentially this could be an Int to save resources. -/
 
+inductive Operation: Type where
+  /- Works on Bool -/
+    /- Equality on composite types uses reference equality for impure types, and structural equality for pure ones -/
+  | Eq | Neq
+  | And | Or | Not
+  /- Works on Int/Float64 -/
+  | Neg | Add | Sub | Mul | Div | Mod
+  | Lt | Leq | Gt | Geq
+  deriving Repr
+
+-- Explicit instance needed for deriving Repr in the mutual block
+instance : Repr (Imperative.MetaData Boogie.Expression) := inferInstance
+
 mutual
 structure Procedure: Type where
   name : Identifier
   inputs : List Parameter
-  output : HighType
+  outputs : List Parameter
   precondition : StmtExpr
   decreases : Option StmtExpr -- optionally prove termination
   determinism: Determinism
@@ -77,6 +91,7 @@ inductive HighType : Type where
   /- Java has implicit intersection types.
      Example: `<cond> ? RustanLeino : AndersHejlsberg` could be typed as `Scientist & Scandinavian`-/
   | Intersection (types : List HighType)
+  deriving Repr
 
 /- No support for something like function-by-method yet -/
 inductive Body where
@@ -87,17 +102,6 @@ inductive Body where
     A type containing any members with abstract bodies can not be instantiated. -/
   | Abstract (postcondition : StmtExpr)
 
-/- We will support these operations for dynamic types as well -/
-/- The 'truthy' concept from JavaScript should be implemented using a library function -/
-inductive Operation: Type where
-  /- Works on Bool -/
-    /- Equality on composite types uses reference equality for impure types, and structural equality for pure ones -/
-  | Eq | Neq
-  | And | Or | Not
-  /- Works on Int/Float64 -/
-  | Neg | Add | Sub | Mul | Div | Mod
-  | Lt | Leq | Gt | Geq
-
 /-
 A StmtExpr contains both constructs that we typically find in statements and those in expressions.
 By using a single datatype we prevent duplication of constructs that can be used in both contexts,
@@ -176,12 +180,14 @@ An extending type can become concrete by redefining all procedures that had abst
   | All -- All refers to all objects in the heap. Can be used in a reads or modifies clause
 /- Hole has a dynamic type and is useful when programs are only partially available -/
   | Hole
-  deriving Inhabited
 
 inductive ContractType where
   | Reads | Modifies | Precondition | PostCondition
 end
 
+instance : Inhabited StmtExpr where
+  default := .Hole
+
 partial def highEq (a: HighType) (b: HighType) : Bool := match a, b with
   | HighType.TVoid, HighType.TVoid => true
   | HighType.TBool, HighType.TBool => true
@@ -237,7 +243,7 @@ Example 2:
  -/
 inductive TypeDefinition where
   | Composite (ty : CompositeType)
-  | Constrainted {ConstrainedType} (ty : ConstrainedType)
+  | Constrained (ty : ConstrainedType)
 
 structure Program where
   staticProcedures : List Procedure
diff --git a/Strata/Languages/Laurel/LaurelFormat.lean b/Strata/Languages/Laurel/LaurelFormat.lean
new file mode 100644
index 0000000000..1c34062a32
--- /dev/null
+++ b/Strata/Languages/Laurel/LaurelFormat.lean
@@ -0,0 +1,194 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.Languages.Laurel.Laurel
+
+namespace Laurel
+
+open Std (Format)
+
+mutual
+def formatOperation : Operation → Format
+  | .Eq => "=="
+  | .Neq => "!="
+  | .And => "&&"
+  | .Or => "||"
+  | .Not => "!"
+  | .Neg => "-"
+  | .Add => "+"
+  | .Sub => "-"
+  | .Mul => "*"
+  | .Div => "/"
+  | .Mod => "%"
+  | .Lt => "<"
+  | .Leq => "<="
+  | .Gt => ">"
+  | .Geq => ">="
+
+def formatHighType : HighType → Format
+  | .TVoid => "void"
+  | .TBool => "bool"
+  | .TInt => "int"
+  | .TFloat64 => "float64"
+  | .UserDefined name => Format.text name
+  | .Applied base args =>
+      Format.text "(" ++ formatHighType base ++ " " ++
+      Format.joinSep (args.map formatHighType) " " ++ ")"
+  | .Pure base => "pure(" ++ formatHighType base ++ ")"
+  | .Intersection types =>
+      Format.joinSep (types.map formatHighType) " & "
+
+def formatStmtExpr (s:StmtExpr) : Format :=
+  match h: s with
+  | .IfThenElse cond thenBr elseBr =>
+      "if " ++ formatStmtExpr cond ++ " then " ++ formatStmtExpr thenBr ++
+      match elseBr with
+      | none => ""
+      | some e => " else " ++ formatStmtExpr e
+  | .Block stmts _ =>
+      "{ " ++ Format.joinSep (stmts.map formatStmtExpr) "; " ++ " }"
+  | .LocalVariable name ty init =>
+      "var " ++ Format.text name ++ ": " ++ formatHighType ty ++
+      match init with
+      | none => ""
+      | some e => " := " ++ formatStmtExpr e
+  | .While cond _ _ body =>
+      "while " ++ formatStmtExpr cond ++ " " ++ formatStmtExpr body
+  | .Exit target => "exit " ++ Format.text target
+  | .Return value =>
+      "return" ++
+      match value with
+      | none => ""
+      | some v => " " ++ formatStmtExpr v
+  | .LiteralInt n => Format.text (toString n)
+  | .LiteralBool b => if b then "true" else "false"
+  | .Identifier name => Format.text name
+  | .Assign target value =>
+      formatStmtExpr target ++ " := " ++ formatStmtExpr value
+  | .FieldSelect target field =>
+      formatStmtExpr target ++ "." ++ Format.text field
+  | .PureFieldUpdate target field value =>
+      formatStmtExpr target ++ " with { " ++ Format.text field ++ " := " ++ formatStmtExpr value ++ " }"
+  | .StaticCall name args =>
+      Format.text name ++ "(" ++ Format.joinSep (args.map formatStmtExpr) ", " ++ ")"
+  | .PrimitiveOp op args =>
+      match args with
+      | [a] => formatOperation op ++ formatStmtExpr a
+      | [a, b] => formatStmtExpr a ++ " " ++ formatOperation op ++ " " ++ formatStmtExpr b
+      | _ => formatOperation op ++ "(" ++ Format.joinSep (args.map formatStmtExpr) ", " ++ ")"
+  | .This => "this"
+  | .ReferenceEquals lhs rhs =>
+      formatStmtExpr lhs ++ " === " ++ formatStmtExpr rhs
+  | .AsType target ty =>
+      formatStmtExpr target ++ " as " ++ formatHighType ty
+  | .IsType target ty =>
+      formatStmtExpr target ++ " is " ++ formatHighType ty
+  | .InstanceCall target name args =>
+      formatStmtExpr target ++ "." ++ Format.text name ++ "(" ++
+      Format.joinSep (args.map formatStmtExpr) ", " ++ ")"
+  | .Forall name ty body =>
+      "forall " ++ Format.text name ++ ": " ++ formatHighType ty ++ " => " ++ formatStmtExpr body
+  | .Exists name ty body =>
+      "exists " ++ Format.text name ++ ": " ++ formatHighType ty ++ " => " ++ formatStmtExpr body
+  | .Assigned name => "assigned(" ++ formatStmtExpr name ++ ")"
+  | .Old value => "old(" ++ formatStmtExpr value ++ ")"
+  | .Fresh value => "fresh(" ++ formatStmtExpr value ++ ")"
+  | .Assert cond _ => "assert " ++ formatStmtExpr cond
+  | .Assume cond _ => "assume " ++ formatStmtExpr cond
+  | .ProveBy value proof =>
+      "proveBy(" ++ formatStmtExpr value ++ ", " ++ formatStmtExpr proof ++ ")"
+  | .ContractOf _ fn => "contractOf(" ++ formatStmtExpr fn ++ ")"
+  | .Abstract => "abstract"
+  | .All => "all"
+  | .Hole => "<?>"
+  decreasing_by
+    all_goals (simp_wf; try omega)
+    any_goals (rename_i x_in; have := List.sizeOf_lt_of_mem x_in; omega)
+    subst_vars; cases h; rename_i x_in; have := List.sizeOf_lt_of_mem x_in; omega
+
+def formatParameter (p : Parameter) : Format :=
+  Format.text p.name ++ ": " ++ formatHighType p.type
+
+def formatDeterminism : Determinism → Format
+  | .deterministic none => "deterministic"
+  | .deterministic (some reads) => "deterministic reads " ++ formatStmtExpr reads
+  | .nondeterministic => "nondeterministic"
+
+def formatBody : Body → Format
+  | .Transparent body => formatStmtExpr body
+  | .Opaque post impl =>
+      "opaque ensures " ++ formatStmtExpr post ++
+      match impl with
+      | none => ""
+      | some e => " := " ++ formatStmtExpr e
+  | .Abstract post => "abstract ensures " ++ formatStmtExpr post
+
+def formatProcedure (proc : Procedure) : Format :=
+  "procedure " ++ Format.text proc.name ++
+  "(" ++ Format.joinSep (proc.inputs.map formatParameter) ", " ++ ") returns " ++ Format.line ++
+  "(" ++ Format.joinSep (proc.outputs.map formatParameter) ", " ++ ")" ++ Format.line ++ formatBody proc.body
+
+def formatField (f : Field) : Format :=
+  (if f.isMutable then "var " else "val ") ++
+  Format.text f.name ++ ": " ++ formatHighType f.type
+
+def formatCompositeType (ct : CompositeType) : Format :=
+  "composite " ++ Format.text ct.name ++
+  (if ct.extending.isEmpty then Format.nil else " extends " ++
+   Format.joinSep (ct.extending.map Format.text) ", ") ++
+  " { " ++ Format.joinSep (ct.fields.map formatField) "; " ++ " }"
+
+def formatConstrainedType (ct : ConstrainedType) : Format :=
+  "constrained " ++ Format.text ct.name ++
+  " = " ++ Format.text ct.valueName ++ ": " ++ formatHighType ct.base ++
+  " | " ++ formatStmtExpr ct.constraint
+
+def formatTypeDefinition : TypeDefinition → Format
+  | .Composite ty => formatCompositeType ty
+  | .Constrained ty => formatConstrainedType ty
+
+def formatProgram (prog : Program) : Format :=
+  Format.joinSep (prog.staticProcedures.map formatProcedure) "\n\n"
+
+end
+
+instance : Std.ToFormat Operation where
+  format := formatOperation
+
+instance : Std.ToFormat HighType where
+  format := formatHighType
+
+instance : Std.ToFormat StmtExpr where
+  format := formatStmtExpr
+
+instance : Std.ToFormat Parameter where
+  format := formatParameter
+
+instance : Std.ToFormat Determinism where
+  format := formatDeterminism
+
+instance : Std.ToFormat Body where
+  format := formatBody
+
+instance : Std.ToFormat Procedure where
+  format := formatProcedure
+
+instance : Std.ToFormat Field where
+  format := formatField
+
+instance : Std.ToFormat CompositeType where
+  format := formatCompositeType
+
+instance : Std.ToFormat ConstrainedType where
+  format := formatConstrainedType
+
+instance : Std.ToFormat TypeDefinition where
+  format := formatTypeDefinition
+
+instance : Std.ToFormat Program where
+  format := formatProgram
+
+end Laurel
diff --git a/Strata/Languages/Laurel/LaurelToBoogieTranslator.lean b/Strata/Languages/Laurel/LaurelToBoogieTranslator.lean
index 06921f0b66..445806ffab 100644
--- a/Strata/Languages/Laurel/LaurelToBoogieTranslator.lean
+++ b/Strata/Languages/Laurel/LaurelToBoogieTranslator.lean
@@ -10,45 +10,169 @@ import Strata.Languages.Boogie.Statement
 import Strata.Languages.Boogie.Procedure
 import Strata.Languages.Boogie.Options
 import Strata.Languages.Laurel.Laurel
+import Strata.Languages.Laurel.LiftExpressionAssignments
+import Strata.DL.Imperative.Stmt
+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)
+open Lambda (LMonoTy LTy LExpr)
+
 /-
+Translate Laurel HighType to Boogie Type
+-/
+def translateType (ty : HighType) : LMonoTy :=
+  match ty with
+  | .TInt => LMonoTy.int
+  | .TBool => LMonoTy.bool
+  | .TVoid => LMonoTy.bool  -- Using bool as placeholder for void
+  | _ => panic s!"unsupported type {repr ty}"
+
+/--
 Translate Laurel StmtExpr to Boogie Expression
 -/
-partial def translateExpr (expr : StmtExpr) : Boogie.Expression.Expr :=
-  match expr with
-  | .LiteralBool true => .boolConst () true
-  | .LiteralBool false => .boolConst () false
-  | _ => .boolConst () true  -- TODO: handle other expressions
+def translateExpr (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
+  | .PrimitiveOp op [e] =>
+    match op with
+    | .Not => .app () boolNotOp (translateExpr e)
+    | .Neg => .app () intNegOp (translateExpr 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]
+    match op with
+    | .Eq => .eq () (translateExpr e1) (translateExpr e2)
+    | .Neq => .app () boolNotOp (.eq () (translateExpr e1) (translateExpr e2))
+    | .And => binOp boolAndOp
+    | .Or => binOp boolOrOp
+    | .Add => binOp intAddOp
+    | .Sub => binOp intSubOp
+    | .Mul => binOp intMulOp
+    | .Div => binOp intDivOp
+    | .Mod => binOp intModOp
+    | .Lt => binOp intLtOp
+    | .Leq => binOp intLeOp
+    | .Gt => binOp intGtOp
+    | .Geq => binOp intGeOp
+    | _ => panic! s!"translateExpr: Invalid binary op: {repr op}"
+  | .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 belse := match elseBranch with
+                  | some e => translateExpr e
+                  | none => .const () (.intConst 0)
+      .ite () bcond bthen belse
+  | .Assign _ value => translateExpr value  -- For expressions, just translate the 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
+  | _ => panic! Std.Format.pretty (Std.ToFormat.format expr)
+  decreasing_by
+  all_goals (simp_wf; try omega)
+  rename_i x_in; have := List.sizeOf_lt_of_mem x_in; omega
 
-/-
+/--
 Translate Laurel StmtExpr to Boogie Statements
+Takes the list of output parameter names to handle return statements correctly
 -/
-partial def translateStmt (stmt : StmtExpr) : List Boogie.Statement :=
+def translateStmt (outputParams : List Parameter) (stmt : StmtExpr) : List Boogie.Statement :=
   match stmt with
   | @StmtExpr.Assert cond md =>
-    let boogieExpr := translateExpr cond
-    [Boogie.Statement.assert "assert" boogieExpr md]
+      let boogieExpr := translateExpr cond
+      [Boogie.Statement.assert "assert" boogieExpr md]
   | @StmtExpr.Assume cond md =>
-    let boogieExpr := translateExpr cond
-    [Boogie.Statement.assume "assume" boogieExpr md]
+      let boogieExpr := translateExpr cond
+      [Boogie.Statement.assume "assume" boogieExpr md]
   | .Block stmts _ =>
-    stmts.flatMap translateStmt
-  | _ => []  -- TODO: handle other statements
+      stmts.flatMap (translateStmt outputParams)
+  | .LocalVariable name ty initializer =>
+      let boogieMonoType := translateType ty
+      let boogieType := LTy.forAll [] boogieMonoType
+      let ident := Boogie.BoogieIdent.locl name
+      match initializer with
+      | some initExpr =>
+          let boogieExpr := translateExpr initExpr
+          [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 =>
+      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
+  | .IfThenElse cond thenBranch elseBranch =>
+      let bcond := translateExpr cond
+      let bthen := translateStmt outputParams thenBranch
+      let belse := match elseBranch with
+                  | some e => translateStmt outputParams e
+                  | none => []
+      -- Use Boogie's if-then-else construct
+      [Imperative.Stmt.ite bcond bthen belse .empty]
+  | .StaticCall name args =>
+      let boogieArgs := args.map translateExpr
+      [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 assignStmt := Boogie.Statement.set ident boogieExpr
+          let noFallThrough := Boogie.Statement.assume "return" (.const () (.boolConst false)) .empty
+          [assignStmt, noFallThrough]
+      | none, _ =>
+          -- Return with no value - just indicate no fallthrough
+          let noFallThrough := Boogie.Statement.assume "return" (.const () (.boolConst false)) .empty
+          [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)
 
-/-
+/--
+Translate Laurel Parameter to Boogie Signature entry
+-/
+def translateParameterToBoogie (param : Parameter) : (Boogie.BoogieIdent × LMonoTy) :=
+  let ident := Boogie.BoogieIdent.locl param.name
+  let ty := translateType param.type
+  (ident, ty)
+
+/--
 Translate Laurel Procedure to Boogie Procedure
 -/
 def translateProcedure (proc : Procedure) : Boogie.Procedure :=
+  -- Translate input parameters
+  let inputPairs := proc.inputs.map translateParameterToBoogie
+  let inputs := inputPairs
+
   let header : Boogie.Procedure.Header := {
     name := proc.name
     typeArgs := []
-    inputs := []
-    outputs := []
+    inputs := inputs
+    outputs := proc.outputs.map translateParameterToBoogie
   }
   let spec : Boogie.Procedure.Spec := {
     modifies := []
@@ -57,7 +181,7 @@ def translateProcedure (proc : Procedure) : Boogie.Procedure :=
   }
   let body : List Boogie.Statement :=
     match proc.body with
-    | .Transparent bodyExpr => translateStmt bodyExpr
+    | .Transparent bodyExpr => translateStmt proc.outputs bodyExpr
     | _ => []  -- TODO: handle Opaque and Abstract bodies
   {
     header := header
@@ -65,20 +189,30 @@ def translateProcedure (proc : Procedure) : Boogie.Procedure :=
     body := body
   }
 
-/-
+/--
 Translate Laurel Program to Boogie Program
 -/
 def translate (program : Program) : Boogie.Program :=
-  let procedures := program.staticProcedures.map translateProcedure
+  -- 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 }
 
-/-
+/--
 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
+  -- 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)
 
diff --git a/Strata/Languages/Laurel/LiftExpressionAssignments.lean b/Strata/Languages/Laurel/LiftExpressionAssignments.lean
new file mode 100644
index 0000000000..0221e4d40c
--- /dev/null
+++ b/Strata/Languages/Laurel/LiftExpressionAssignments.lean
@@ -0,0 +1,183 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.Languages.Laurel.Laurel
+
+namespace Laurel
+
+/-
+Transform assignments that appear in expression contexts into preceding statements.
+
+For example:
+  if ((x := x + 1) == (y := x)) { ... }
+
+Becomes:
+  var x1 := x + 1;
+  x := x1;
+  var y1 := x;
+  y := y1;
+  if (x1 == y1) { ... }
+-/
+
+structure SequenceState where
+  prependedStmts : List StmtExpr := []
+  tempCounter : Nat := 0
+
+abbrev SequenceM := StateM SequenceState
+
+def SequenceM.addPrependedStmt (stmt : StmtExpr) : SequenceM Unit :=
+  modify fun s => { s with prependedStmts := stmt :: s.prependedStmts }
+
+def SequenceM.takePrependedStmts : SequenceM (List StmtExpr) := do
+  let stmts := (← get).prependedStmts
+  modify fun s => { s with prependedStmts := [] }
+  return stmts.reverse
+
+def SequenceM.freshTemp : SequenceM Identifier := do
+  let counter := (← get).tempCounter
+  modify fun s => { s with tempCounter := s.tempCounter + 1 }
+  return s!"__t{counter}"
+
+mutual
+/-
+Process an expression, extracting any assignments to preceding statements.
+Returns the transformed expression with assignments replaced by variable references.
+-/
+def transformExpr (expr : StmtExpr) : SequenceM StmtExpr := do
+  match expr with
+  | .Assign target value =>
+      -- 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
+      SequenceM.addPrependedStmt assignStmt
+      -- Create a temporary variable to capture the assigned value
+      -- Use TInt as the type (could be refined with type inference)
+      let tempName ← SequenceM.freshTemp
+      let tempDecl := StmtExpr.LocalVariable tempName .TInt (some target)
+      SequenceM.addPrependedStmt tempDecl
+      -- Return the temporary variable as the expression value
+      return .Identifier tempName
+
+  | .PrimitiveOp op args =>
+      let seqArgs ← args.mapM transformExpr
+      return .PrimitiveOp op seqArgs
+
+  | .IfThenElse cond thenBranch elseBranch =>
+      let seqCond ← transformExpr cond
+      let seqThen ← transformExpr thenBranch
+      let seqElse ← match elseBranch with
+        | some e => transformExpr e >>= (pure ∘ some)
+        | none => pure none
+      return .IfThenElse seqCond seqThen seqElse
+
+  | .StaticCall name args =>
+      let seqArgs ← args.mapM transformExpr
+      return .StaticCall name seqArgs
+
+  | .Block stmts metadata =>
+      -- Block in expression position: move all but last statement to prepended
+      let rec next (remStmts: List StmtExpr) := match remStmts with
+        | [last] => transformExpr last
+        | head :: tail => do
+            let seqStmt ← transformStmt head
+            for s in seqStmt do
+              SequenceM.addPrependedStmt s
+            next tail
+        | [] => return .Block [] metadata
+
+      next stmts
+
+  -- Base cases: no assignments to extract
+  | .LiteralBool _ => return expr
+  | .LiteralInt _ => return expr
+  | .Identifier _ => return expr
+  | .LocalVariable _ _ _ => return expr
+  | _ => return expr  -- Other cases
+
+/-
+Process a statement, handling any assignments in its sub-expressions.
+Returns a list of statements (the original one may be split into multiple).
+-/
+def transformStmt (stmt : StmtExpr) : SequenceM (List StmtExpr) := do
+  match stmt with
+  | @StmtExpr.Assert cond md =>
+      -- Process the condition, extracting any assignments
+      let seqCond ← transformExpr cond
+      SequenceM.addPrependedStmt <| StmtExpr.Assert seqCond md
+      SequenceM.takePrependedStmts
+
+  | @StmtExpr.Assume cond md =>
+      let seqCond ← transformExpr cond
+      SequenceM.addPrependedStmt <| StmtExpr.Assume seqCond md
+      SequenceM.takePrependedStmts
+
+  | .Block stmts metadata =>
+      let seqStmts ← stmts.mapM transformStmt
+      return [.Block (seqStmts.flatten) metadata]
+
+  | .LocalVariable name ty initializer =>
+      match initializer with
+      | some initExpr => do
+          let seqInit ← transformExpr initExpr
+          SequenceM.addPrependedStmt <| .LocalVariable name ty (some seqInit)
+          SequenceM.takePrependedStmts
+      | none =>
+          return [stmt]
+
+  | .Assign target value =>
+      -- Top-level assignment (statement context)
+      let seqTarget ← transformExpr target
+      let seqValue ← transformExpr value
+      SequenceM.addPrependedStmt <| .Assign seqTarget seqValue
+      SequenceM.takePrependedStmts
+
+  | .IfThenElse cond thenBranch elseBranch =>
+      let seqThen ← transformStmt thenBranch
+      let thenBlock := .Block seqThen none
+
+      let seqElse ← match elseBranch with
+        | some e =>
+            let se ← transformStmt e
+            pure (some (.Block se none))
+        | none => pure none
+
+      let seqCond ← transformExpr cond
+      SequenceM.addPrependedStmt <| .IfThenElse seqCond thenBlock seqElse
+      SequenceM.takePrependedStmts
+
+  | .StaticCall name args =>
+      let seqArgs ← args.mapM transformExpr
+      SequenceM.addPrependedStmt <| .StaticCall name seqArgs
+      SequenceM.takePrependedStmts
+
+  | _ =>
+      return [stmt]
+
+end
+
+def transformProcedureBody (body : StmtExpr) : StmtExpr :=
+  let (seqStmts, _) := transformStmt body |>.run {}
+  match seqStmts with
+  | [single] => single
+  | multiple => .Block multiple.reverse none
+
+def transformProcedure (proc : Procedure) : Procedure :=
+  match proc.body with
+  | .Transparent bodyExpr =>
+      let seqBody := transformProcedureBody bodyExpr
+      { proc with body := .Transparent seqBody }
+  | _ => 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 }
+
+end Laurel
diff --git a/StrataTest/DDM/TestGrammar.lean b/StrataTest/DDM/TestGrammar.lean
index bee34684dd..a6b28260ce 100644
--- a/StrataTest/DDM/TestGrammar.lean
+++ b/StrataTest/DDM/TestGrammar.lean
@@ -8,6 +8,9 @@ import Strata.DDM.Elab
 import Strata.DDM.Parser
 import Strata.DDM.Format
 
+/-
+Allows testing whether a DDM dialect can parse and print a given program without losing information.
+-/
 open Strata
 
 namespace StrataTest.DDM
@@ -59,13 +62,13 @@ structure GrammarTestResult where
 
     Returns:
     - GrammarTestResult with parse/format results -/
-def testGrammarFile (dialect: Dialect) (filePath : String) : IO GrammarTestResult := do
+def testGrammarFile (dialect: Dialect) (ctx : Lean.Parser.InputContext) : IO GrammarTestResult := do
   try
     let loaded := .ofDialects! #[initDialect, dialect]
-    let (inputContext, ddmProgram) ← Strata.Elab.parseStrataProgramFromDialect loaded dialect.name filePath
+    let ddmProgram ← Strata.Elab.parseStrataProgramFromDialect loaded dialect.name ctx
     let formatted := ddmProgram.format.render
     let normalizedInput := normalizeWhitespace <| stripComments <|
-      s!"program {dialect.name}; " ++ inputContext.inputString
+      s!"program {dialect.name}; " ++ ctx.inputString
     let normalizedOutput := normalizeWhitespace formatted
 
     let isMatch := normalizedInput == normalizedOutput
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/2. NestedImpureStatements.lr.st b/StrataTest/Languages/Laurel/Examples/Fundamentals/2. NestedImpureStatements.lr.st
deleted file mode 100644
index 6a822a8b91..0000000000
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/2. NestedImpureStatements.lr.st	
+++ /dev/null
@@ -1,39 +0,0 @@
-/*
-  Copyright Strata Contributors
-
-  SPDX-License-Identifier: Apache-2.0 OR MIT
-*/
-
-procedure nestedImpureStatements(): int {
-  var x = 0;
-  var y = 0;
-  if ((x = x + 1) == (y = x)) {
-    1
-  } else {
-    2
-  }
-}
-
-procedure assertLocallyImpureCode()
-{
-  assert nestedImpureStatements() != 0; // pass
-}
-
-/*
-Translation towards SMT:
-
-function nestedImpureStatements(): int {
-  var x = 0;
-  var y = 0;
-  x = x + 1;
-  var t1 = x;
-  y = x;
-  var t2 = x;
-  if (t1 == t2) {
-    1
-  } else {
-    2
-  }
-}
-
-*/
\ No newline at end of file
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/3. ControlFlow.lr.st b/StrataTest/Languages/Laurel/Examples/Fundamentals/3. ControlFlow.lr.st
deleted file mode 100644
index fdde81d0bb..0000000000
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/3. ControlFlow.lr.st	
+++ /dev/null
@@ -1,72 +0,0 @@
-/*
-  Copyright Strata Contributors
-
-  SPDX-License-Identifier: Apache-2.0 OR MIT
-*/
-
-procedure guards(a: int): int
-{
-  var b = a + 2;
-  if (b > 2) {
-      var c = b + 3;
-      if (c > 3) {
-          return c + 4;
-      }
-      var d = c + 5;
-      return d + 6;
-  }
-  var e = b + 1;
-  e
-}
-
-/*
-Translation towards expression form:
-
-function guards(a: int): int {
-  var b = a + 2;
-  if (b > 2) {
-      var c = b + 3;
-      if (c > 3) {
-        c + 4;
-      } else {
-        var d = c + 5;
-        d + 6;
-      }
-  } else {
-    var e = b + 1;
-    e
-  }
-}
-*/
-
-procedure dag(a: int): int
-{
-  var b: int;
-
-  if (a > 0) {
-    b = 1;
-  } else {
-    b = 2;
-  }
-  b
-}
-
-/*
-To translate towards SMT we only need to apply something like WP calculus.
- Here's an example of what that looks like:
-
-function dag(a: int): int {
-  (
-    assume a > 0;
-    assume b == 1;
-    b;
-  ) 
-  OR
-  (
-    assume a <= 0;
-    assume b == 2;
-    b;
-  )
-}
-
-*/
\ No newline at end of file
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/10. ConstrainedTypes.lr.st b/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypes.lean
similarity index 51%
rename from StrataTest/Languages/Laurel/Examples/Fundamentals/10. ConstrainedTypes.lr.st
rename to StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypes.lean
index 31c73d96ac..3ad972ee0d 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/10. ConstrainedTypes.lr.st	
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypes.lean
@@ -1,21 +1,30 @@
-/*
+/-
   Copyright Strata Contributors
 
   SPDX-License-Identifier: Apache-2.0 OR MIT
-*/
+-/
 
-// Constrained primitive type
+import StrataTest.Util.TestDiagnostics
+import StrataTest.Languages.Laurel.TestExamples
+
+open StrataTest.Util
+open Strata
+
+namespace Laurel
+
+def program := r"
 constrained nat = x: int where x >= 0 witness 0
 
-// Something analogous to an algebriac datatype
 composite Option {}
-composite Some extends Option { 
+composite Some extends Option {
   value: int
 }
 composite None extends Option
 constrained SealedOption = x: Option where x is Some || x is None witness None
 
 procedure foo() returns (r: nat) {
-  // no assign to r. 
-  // this is accepted. there is no definite-asignment checking since types may never be empty
-}
\ No newline at end of file
+}
+"
+
+-- Not working yet
+-- #eval! testInput "ConstrainedTypes" program processLaurelFile
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/1. AssertFalse.lr.st b/StrataTest/Languages/Laurel/Examples/Fundamentals/T1_AssertFalse.lean
similarity index 52%
rename from StrataTest/Languages/Laurel/Examples/Fundamentals/1. AssertFalse.lr.st
rename to StrataTest/Languages/Laurel/Examples/Fundamentals/T1_AssertFalse.lean
index ebf246aba9..8e831c9e19 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/1. AssertFalse.lr.st	
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T1_AssertFalse.lean
@@ -1,8 +1,18 @@
-/*
+/-
   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 Laurel
+
+def program := r"
 procedure foo() {
     assert true;
     assert false;
@@ -13,5 +23,8 @@ procedure foo() {
 
 procedure bar() {
     assume false;
-    assert true;
-}
\ No newline at end of file
+    assert false;
+}
+"
+
+#eval testInputWithOffset "AssertFalse" program 14 processLaurelFile
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
new file mode 100644
index 0000000000..04d6583439
--- /dev/null
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
@@ -0,0 +1,34 @@
+/-
+  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 Laurel
+
+def program: String := r"
+procedure nestedImpureStatements(x: int) {
+  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
+}
+"
+
+#guard_msgs (error, drop all) in
+#eval! testInputWithOffset "NestedImpureStatements" program 14 processLaurelFile
+
+
+end Laurel
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean
new file mode 100644
index 0000000000..f0467c36b8
--- /dev/null
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean
@@ -0,0 +1,86 @@
+/-
+  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 Laurel
+
+def program := r"
+procedure guards(a: int) returns (r: int)
+{
+  var b := a + 2;
+  if (b > 2) {
+      var c := b + 3;
+      if (c > 3) {
+          return c + 4;
+      }
+      var d := c + 5;
+      return d + 6;
+  }
+  var e := b + 1;
+  assert e <= 3;
+    assert e < 3;
+//  ^^^^^^^^^^^^^ error: assertion does not hold
+  return e;
+}
+
+procedure dag(a: int) returns (r: int)
+{
+  var b: int;
+
+  if (a > 0) {
+    b := 1;
+  }
+  assert if (a > 0) { b == 1 } else { true };
+    assert if (a > 0) { b == 2 } else { true };
+//  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
+  return b;
+}
+"
+
+#guard_msgs (error, drop all) in
+#eval! testInputWithOffset "ControlFlow" program 14 processLaurelFile
+
+/-
+Translation towards expression form:
+
+function guards(a: int): int {
+  var b = a + 2;
+  if (b > 2) {
+      var c = b + 3;
+      if (c > 3) {
+        c + 4;
+      } else {
+        var d = c + 5;
+        d + 6;
+      }
+  } else {
+    var e = b + 1;
+    e
+  }
+}
+
+To translate towards SMT we only need to apply something like WP calculus.
+ Here's an example of what that looks like:
+
+function dag(a: int): int {
+  (
+    assume a > 0;
+    assume b == 1;
+    b;
+  )
+  OR
+  (
+    assume a <= 0;
+    assume b == 2;
+    b;
+  )
+}
+-/
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/4. LoopJumps.lr.st b/StrataTest/Languages/Laurel/Examples/Fundamentals/T4_LoopJumps.lean
similarity index 79%
rename from StrataTest/Languages/Laurel/Examples/Fundamentals/4. LoopJumps.lr.st
rename to StrataTest/Languages/Laurel/Examples/Fundamentals/T4_LoopJumps.lean
index b3aeff0032..e9cb07e937 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/4. LoopJumps.lr.st	
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T4_LoopJumps.lean
@@ -1,12 +1,22 @@
-/*
+/-
   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 Laurel
+
+def program := r"
 procedure whileWithBreakAndContinue(steps: int, continueSteps: int, exitSteps: int): int {
   var counter = 0
   {
-    while(steps > 0) 
+    while(steps > 0)
       invariant counter >= 0
     {
       {
@@ -24,9 +34,12 @@ procedure whileWithBreakAndContinue(steps: int, continueSteps: int, exitSteps: i
   } breakBlock;
   counter;
 }
+"
 
+-- Not working yet
+-- #eval! testInput "LoopJumps" program processLaurelFile
 
-/*
+/-
 Translation towards SMT:
 
 proof whileWithBreakAndContinue_body() {
@@ -35,7 +48,7 @@ proof whileWithBreakAndContinue_body() {
   var exitSteps: int;
 
   var counter = 0;
-  
+
   label loopStart;
   assert counter >= 0;
   if (steps > 0) {
@@ -54,6 +67,4 @@ proof whileWithBreakAndContinue_body() {
   label breakLabel;
   counter;
 }
-
-
-*/
\ No newline at end of file
+-/
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/5. ProcedureCalls.lr.st b/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCalls.lean
similarity index 68%
rename from StrataTest/Languages/Laurel/Examples/Fundamentals/5. ProcedureCalls.lr.st
rename to StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCalls.lean
index d01f72d9c7..3ba48f00fb 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/5. ProcedureCalls.lr.st	
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T5_ProcedureCalls.lean
@@ -1,9 +1,18 @@
-/*
+/-
   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 Laurel
+
+def program := r"
 procedure fooReassign(): int {
   var x = 0;
   x = x + 1;
@@ -20,10 +29,14 @@ procedure fooSingleAssign(): int {
 }
 
 procedure fooProof() {
-  assert fooReassign() == fooSingleAssign(); // passes
+  assert fooReassign() == fooSingleAssign();
 }
+"
+
+-- Not working yet
+-- #eval! testInput "ProcedureCalls" program processLaurelFile
 
-/*
+/-
 Translation towards SMT:
 
 function fooReassign(): int {
@@ -49,4 +62,4 @@ function fooSingleAssign(): int {
 proof fooProof_body {
   assert fooReassign() == fooSingleAssign();
 }
-*/
\ No newline at end of file
+-/
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/6. Preconditions.lr.st b/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean
similarity index 63%
rename from StrataTest/Languages/Laurel/Examples/Fundamentals/6. Preconditions.lr.st
rename to StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean
index 402b2fc638..8592576f8f 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/6. Preconditions.lr.st	
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean
@@ -1,22 +1,38 @@
-/*
+/-
   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 Laurel
+
+def program := r"
 procedure hasRequires(x: int): (r: int)
   requires assert 1 == 1; x > 2
 {
-  assert x > 0; // pass
-  assert x > 3; // fail
+  assert x > 0;
+    assert x > 3;
+//  ^^^^^^^^^^^^^ error: assertion does not hold
   x + 1
 }
 
 procedure caller() {
-  var x = hasRequires(1) // fail
-  var y = hasRequires(3) // pass
+    var x = hasRequires(1);
+//          ^^^^^^^^^^^^^^ error: precondition does not hold
+  var y = hasRequires(3);
 }
+"
+
+-- Not working yet
+-- #eval! testInput "Preconditions" program processLaurelFile
 
-/*
+/-
 Translation towards SMT:
 
 function hasRequires_requires(x: int): boolean {
@@ -47,4 +63,4 @@ proof caller_body {
   assert hasRequires_ensures(hasRequires_arg1_2); // pass
   var y: int := hasRequires(hasRequires_arg1_2);
 }
-*/
\ No newline at end of file
+-/
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/7. Decreases.lr.st b/StrataTest/Languages/Laurel/Examples/Fundamentals/T7_Decreases.lean
similarity index 62%
rename from StrataTest/Languages/Laurel/Examples/Fundamentals/7. Decreases.lr.st
rename to StrataTest/Languages/Laurel/Examples/Fundamentals/T7_Decreases.lean
index cbb2ef51c8..6c72213da4 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/7. Decreases.lr.st	
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T7_Decreases.lean
@@ -1,30 +1,36 @@
-/*
+/-
   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 Laurel
+
+/-
 A decreases clause CAN be added to a procedure to prove that it terminates.
 A procedure with a decreases clause may be called in an erased context.
-*/
+-/
 
+def program := r"
 procedure noDecreases(x: int): boolean
 procedure caller(x: int)
-  requires noDecreases(x) // error: noDecreases can not be called from a contract, because ...
+  requires noDecreases(x)
+//                    ^ error: noDecreases can not be called from a pure context, because it is not proven to terminate
 
-// Non-recursive procedures can use an empty decreases list and still prove termination
-procedure noCyclicCalls() 
+procedure noCyclicCalls()
   decreases []
 {
-  leaf(); // call passes since leaf is lower in the SCC call-graph.
+  leaf();
 }
 
 procedure leaf() decreases [1] { }
 
-// Decreases clauses are needed for recursive procedure calls.
-
-// Decreases clauses take a list of arguments
 procedure mutualRecursionA(x: nat)
   decreases [x, 1]
 {
@@ -36,8 +42,12 @@ procedure mutualRecursionB(x: nat)
 {
   if x != 0 { mutualRecursionA(x-1); }
 }
+"
+
+-- Not working yet
+-- #eval! testInput "Decreases" program processLaurelFile
 
-/*
+/-
 Translation towards SMT:
 
 proof foo_body {
@@ -51,5 +61,4 @@ proof bar_body {
     assert decreases([x, 0], [x - 1, 1]);
   }
 }
-
-*/
\ No newline at end of file
+-/
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/8. Postconditions.lr.st b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean
similarity index 62%
rename from StrataTest/Languages/Laurel/Examples/Fundamentals/8. Postconditions.lr.st
rename to StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean
index 662c25401e..570845a651 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/8. Postconditions.lr.st	
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean
@@ -1,11 +1,21 @@
-/*
+/-
   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 Laurel
+
+def program := r"
 procedure opaqueBody(x: int): (r: int)
 // the presence of the ensures make the body opaque. we can consider more explicit syntax.
-  ensures assert 1 == 1; r >= 0 
+  ensures assert 1 == 1; r >= 0
 {
   Math.abs(x)
 }
@@ -16,13 +26,18 @@ procedure transparantBody(x: int): int
 }
 
 procedure caller() {
-  assert transparantBody(-1) == 1; // pass
-  assert opaqueBody(-1) >= 0 // pass
-  assert opaqueBody(-3) == opaqueBody(-3); // pass because no heap is used and this is a det procedure
-  assert opaqueBody(-1) == 1; // error
+  assert transparantBody(-1) == 1;
+  assert opaqueBody(-1) >= 0
+  assert opaqueBody(-3) == opaqueBody(-3);
+    assert opaqueBody(-1) == 1;
+//  ^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
 }
+"
+
+-- Not working yet
+-- #eval! testInput "Postconditions" program processLaurelFile
 
-/*
+/-
 Translation towards SMT:
 
 function opaqueBody(x: int): boolean
@@ -50,6 +65,6 @@ proof caller_body {
   assert r_1 >= 0; // pass, using axiom
 
   var r_2: int := opaqueBody_ensures(-1);
-  assert r_2 == 1; // error  
+  assert r_2 == 1; // error
 }
-*/
\ No newline at end of file
+-/
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/9. Nondeterministic.lr.st b/StrataTest/Languages/Laurel/Examples/Fundamentals/T9_Nondeterministic.lean
similarity index 73%
rename from StrataTest/Languages/Laurel/Examples/Fundamentals/9. Nondeterministic.lr.st
rename to StrataTest/Languages/Laurel/Examples/Fundamentals/T9_Nondeterministic.lean
index 79a6c49bac..3dbd871159 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/9. Nondeterministic.lr.st	
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T9_Nondeterministic.lean
@@ -1,14 +1,18 @@
-/*
+/-
   Copyright Strata Contributors
 
   SPDX-License-Identifier: Apache-2.0 OR MIT
-*/
+-/
 
-/*
-When a procedure is non-deterministic, 
-every invocation might return a different result, even if the inputs are the same.
-It's comparable to having an IO monad.
-*/
+import StrataTest.Util.TestDiagnostics
+import StrataTest.Languages.Laurel.TestExamples
+
+open StrataTest.Util
+open Strata
+
+namespace Laurel
+
+def program := r"
 nondet procedure nonDeterministic(x: int): (r: int)
   ensures r > 0
 {
@@ -17,12 +21,31 @@ nondet procedure nonDeterministic(x: int): (r: int)
 
 procedure caller() {
   var x = nonDeterministic(1)
-  assert x > 0; -- pass
+  assert x > 0;
   var y = nonDeterministic(1)
-  assert x == y; -- fail
+    assert x == y;
+//  ^^^^^^^^^^^^^^ error: assertion does not hold
+}
+
+nondet procedure nonDeterminsticTransparant(x: int): (r: int)
+{
+  nonDeterministic(x + 1)
+}
+
+procedure nonDeterministicCaller(x: int): int
+{
+  nonDeterministic(x)
 }
+"
+
+-- Not working yet
+-- #eval! testInput "Nondeterministic" program processLaurelFile
+
+/-
+When a procedure is non-deterministic,
+every invocation might return a different result, even if the inputs are the same.
+It's comparable to having an IO monad.
 
-/*
 Translation towards SMT:
 
 function nonDeterministic_relation(x: int, r: int): boolean
@@ -44,22 +67,8 @@ proof caller_body {
   assume nonDeterministic_relation(1, y);
   assert x == y; // fail
 }
-*/
-
-nondet procedure nonDeterminsticTransparant(x: int): (r: int)
-{
-  nonDeterministic(x + 1)
-}
-
-/*
-Translation towards SMT:
 
 function nonDeterminsticTransparant_relation(x: int, r: int): boolean {
   nonDeterministic_relation(x + 1, r)
 }
-*/
-
-procedure nonDeterministicCaller(x: int): int
-{
-  nonDeterministic(x) // error: can not call non-deterministic procedure from deterministic one
-}
\ No newline at end of file
+-/
diff --git a/StrataTest/Languages/Laurel/Grammar/TestGrammar.lean b/StrataTest/Languages/Laurel/Grammar/TestGrammar.lean
deleted file mode 100644
index 441fd7aaee..0000000000
--- a/StrataTest/Languages/Laurel/Grammar/TestGrammar.lean
+++ /dev/null
@@ -1,26 +0,0 @@
-/-
-  Copyright Strata Contributors
-
-  SPDX-License-Identifier: Apache-2.0 OR MIT
--/
-
--- Test the minimal Laurel grammar
-import Strata.Languages.Laurel.Grammar.LaurelGrammar
-import StrataTest.DDM.TestGrammar
-import Strata.DDM.BuiltinDialects.Init
-
-open Strata
-open StrataTest.DDM
-
-namespace Laurel
-
-def testAssertFalse : IO Unit := do
-  let laurelDialect: Strata.Dialect := Laurel
-  let filePath := "StrataTest/Languages/Laurel/Examples/Fundamentals/1. AssertFalse.lr.st"
-  let result ← testGrammarFile laurelDialect filePath
-
-  if !result.normalizedMatch then
-    throw (IO.userError "Test failed: formatted output does not match input")
-
-#guard_msgs in
-#eval testAssertFalse
diff --git a/StrataTest/Languages/Laurel/TestExamples.lean b/StrataTest/Languages/Laurel/TestExamples.lean
index b674c2cbba..473eacb030 100644
--- a/StrataTest/Languages/Laurel/TestExamples.lean
+++ b/StrataTest/Languages/Laurel/TestExamples.lean
@@ -15,27 +15,22 @@ import Strata.Languages.Laurel.LaurelToBoogieTranslator
 open StrataTest.Util
 open Strata
 open Strata.Elab (parseStrataProgramFromDialect)
+open Lean.Parser (InputContext)
 
 namespace Laurel
 
-def processLaurelFile (filePath : String) : IO (Array Diagnostic) := do
+def processLaurelFile (input : InputContext) : IO (Array Diagnostic) := do
   let dialects := Strata.Elab.LoadedDialects.ofDialects! #[initDialect, Laurel]
-  let (inputContext, strataProgram) ← parseStrataProgramFromDialect dialects Laurel.name filePath
+  let strataProgram ← parseStrataProgramFromDialect dialects Laurel.name input
 
   -- Convert to Laurel.Program using parseProgram (handles unwrapping the program operation)
-  let (laurelProgram, transErrors) := Laurel.TransM.run inputContext (Laurel.parseProgram strataProgram)
-  if transErrors.size > 0 then
-    throw (IO.userError s!"Translation errors: {transErrors}")
+  let laurelProgram ← match Laurel.TransM.run input (Laurel.parseProgram strataProgram) with
+    | .ok program => pure program
+    | .error errMsg => throw (IO.userError s!"Translation error: {errMsg}")
 
   -- Verify the program
   let diagnostics ← Laurel.verifyToDiagnostics "z3" laurelProgram
 
   pure diagnostics
 
-def testAssertFalse : IO Unit := do
-  testFile processLaurelFile "StrataTest/Languages/Laurel/Examples/Fundamentals/1. AssertFalse.lr.st"
-
-#guard_msgs(error, drop all) in
-#eval! testAssertFalse
-
 end Laurel
diff --git a/StrataTest/Util/TestDiagnostics.lean b/StrataTest/Util/TestDiagnostics.lean
index e54eac301a..312cfe54a5 100644
--- a/StrataTest/Util/TestDiagnostics.lean
+++ b/StrataTest/Util/TestDiagnostics.lean
@@ -5,9 +5,11 @@
 -/
 
 import Strata.Languages.Boogie.Verifier
+import Lean.Elab.Command
 
 open Strata
 open String
+open Lean Elab
 namespace StrataTest.Util
 
 /-- A diagnostic expectation parsed from source comments -/
@@ -75,17 +77,20 @@ def matchesDiagnostic (diag : Diagnostic) (exp : DiagnosticExpectation) : Bool :
   diag.ending.column == exp.colEnd &&
   stringContains diag.message exp.message
 
-/-- Generic test function for files with diagnostic expectations.
-    Takes a function that processes a file path and returns a list of diagnostics. -/
-def testFile (processFn : String -> IO (Array Diagnostic)) (filePath : String) : IO Unit := do
-  let content <- IO.FS.readFile filePath
+/-- Test input with line offset - adds imaginary newlines to the start of the input -/
+def testInputWithOffset (filename: String) (input : String) (lineOffset : Nat)
+    (process : Lean.Parser.InputContext -> IO (Array Diagnostic)) : IO Unit := do
+
+  -- Add imaginary newlines to the start of the input so the reported line numbers match the Lean source file
+  let offsetInput := String.join (List.replicate lineOffset "\n") ++ input
+  let inputContext := Parser.stringInputContext filename offsetInput
 
   -- Parse diagnostic expectations from comments
-  let expectations := parseDiagnosticExpectations content
+  let expectations := parseDiagnosticExpectations offsetInput
   let expectedErrors := expectations.filter (fun e => e.level == "error")
 
   -- Get actual diagnostics from the language-specific processor
-  let diagnostics <- processFn filePath
+  let diagnostics <- process inputContext
 
   -- Check if all expected errors are matched
   let mut allMatched := true
@@ -97,7 +102,6 @@ def testFile (processFn : String -> IO (Array Diagnostic)) (filePath : String) :
       allMatched := false
       unmatchedExpectations := unmatchedExpectations.append [exp]
 
-  -- Check if there are unexpected diagnostics
   let mut unmatchedDiagnostics := []
   for diag in diagnostics do
     let matched := expectedErrors.any (fun exp => matchesDiagnostic diag exp)
@@ -108,7 +112,6 @@ def testFile (processFn : String -> IO (Array Diagnostic)) (filePath : String) :
   -- Report results
   if allMatched && diagnostics.size == expectedErrors.length then
     IO.println s!"✓ Test passed: All {expectedErrors.length} error(s) matched"
-    -- Print details of matched expectations
     for exp in expectedErrors do
       IO.println s!"  - Line {exp.line}, Col {exp.colStart}-{exp.colEnd}: {exp.message}"
   else
@@ -124,5 +127,9 @@ def testFile (processFn : String -> IO (Array Diagnostic)) (filePath : String) :
       IO.println s!"\nUnexpected diagnostics:"
       for diag in unmatchedDiagnostics do
         IO.println s!"  - Line {diag.start.line}, Col {diag.start.column}-{diag.ending.column}: {diag.message}"
+    throw (IO.userError "Test failed")
+
+def testInput (filename: String) (input : String) (process : Lean.Parser.InputContext -> IO (Array Diagnostic)) : IO Unit :=
+  testInputWithOffset filename input 0 process
 
 end StrataTest.Util