From 99ba9b84c4c10b667483f3f72ba68153aab9885d Mon Sep 17 00:00:00 2001
From: Mikael Mayer <mimayere@amazon.com>
Date: Tue, 27 Jan 2026 11:14:20 -0600
Subject: [PATCH 01/12] Add support for function declarations within statement
 blocks

---
 Strata/DL/Imperative/PureExpr.lean            |   2 +
 Strata/DL/Imperative/Stmt.lean                |  23 ++-
 Strata/DL/Lambda/Factory.lean                 |  85 +++++++----
 Strata/Languages/B3/.gitignore                |   2 +
 Strata/Languages/C_Simp/C_Simp.lean           |   1 +
 Strata/Languages/C_Simp/Verify.lean           |   1 +
 Strata/Languages/Core/CallGraph.lean          |   1 +
 Strata/Languages/Core/Env.lean                |  56 +++++---
 Strata/Languages/Core/Expressions.lean        |   1 +
 Strata/Languages/Core/Factory.lean            |   7 +-
 Strata/Languages/Core/FunctionType.lean       |   4 +-
 Strata/Languages/Core/ProcedureType.lean      |  15 ++
 Strata/Languages/Core/ProcedureWF.lean        |   1 -
 Strata/Languages/Core/Program.lean            |  15 ++
 Strata/Languages/Core/Statement.lean          |  25 +++-
 Strata/Languages/Core/StatementEval.lean      |  27 +++-
 Strata/Languages/Core/StatementType.lean      |  39 ++++++
 Strata/Languages/Core/StatementWF.lean        |   8 ++
 Strata/Languages/Core/WF.lean                 |   1 +
 Strata/Transform/CallElimCorrect.lean         |   2 +
 Strata/Transform/CoreTransform.lean           |   1 +
 Strata/Transform/DetToNondet.lean             |   1 +
 Strata/Transform/LoopElim.lean                |   1 +
 Strata/Transform/ProcedureInlining.lean       |  10 ++
 .../Backends/CBMC/CoreToCProverGOTO.lean      |   1 +
 StrataTest/Backends/CBMC/ToCProverGOTO.lean   |   1 +
 StrataTest/DL/Imperative/ArithExpr.lean       |   1 +
 StrataTest/DL/Lambda/LExprTTests.lean         |  15 ++
 StrataTest/DL/Lambda/TypeFactoryTests.lean    |  15 ++
 StrataTest/Languages/Core/Examples/Regex.lean |   4 +-
 .../Languages/Core/StatementEvalTests.lean    | 132 +++++++++++++++++-
 31 files changed, 435 insertions(+), 63 deletions(-)
 create mode 100644 Strata/Languages/B3/.gitignore

diff --git a/Strata/DL/Imperative/PureExpr.lean b/Strata/DL/Imperative/PureExpr.lean
index 9428839c2..6006546e1 100644
--- a/Strata/DL/Imperative/PureExpr.lean
+++ b/Strata/DL/Imperative/PureExpr.lean
@@ -21,6 +21,8 @@ structure PureExpr : Type 1 where
   Expr    : Type
   /-- Types -/
   Ty      : Type
+  /-- Expression metadata type (for use in function declarations, etc.) -/
+  ExprMetadata : Type
   /-- Typing environment, expected to contain a map of variables to their types,
   type substitution, etc.
   -/
diff --git a/Strata/DL/Imperative/Stmt.lean b/Strata/DL/Imperative/Stmt.lean
index 795171fb9..71978957d 100644
--- a/Strata/DL/Imperative/Stmt.lean
+++ b/Strata/DL/Imperative/Stmt.lean
@@ -7,6 +7,7 @@
 
 
 import Strata.DL.Imperative.Cmd
+import Strata.DL.Lambda.Factory
 
 namespace Imperative
 ---------------------------------------------------------------------
@@ -38,6 +39,8 @@ inductive Stmt (P : PureExpr) (Cmd : Type) : Type where
   This will likely be removed, in favor of an alternative view of imperative
   programs that is purely untructured. -/
   | goto     (label : String) (md : MetaData P := .empty)
+  /-- A function declaration within a statement block. -/
+  | funcDecl (decl : Lambda.PureFunc P) (md : MetaData P := .empty)
   deriving Inhabited
 
 /-- A block is simply an abbreviation for a list of commands. -/
@@ -69,19 +72,22 @@ def Stmt.inductionOn {P : PureExpr} {Cmd : Type}
       motive (Stmt.loop guard measure invariant body md))
     (goto_case : ∀ (label : String) (md : MetaData P),
       motive (Stmt.goto label md))
+    (funcDecl_case : ∀ (decl : Lambda.PureFunc P) (md : MetaData P),
+      motive (Stmt.funcDecl decl md))
     (s : Stmt P Cmd) : motive s :=
   match s with
   | Stmt.cmd c => cmd_case c
   | Stmt.block label b md =>
-    block_case label b md (fun s _ => inductionOn cmd_case block_case ite_case loop_case goto_case s)
+    block_case label b md (fun s _ => inductionOn cmd_case block_case ite_case loop_case goto_case funcDecl_case s)
   | Stmt.ite cond thenb elseb md =>
     ite_case cond thenb elseb md
-      (fun s _ => inductionOn cmd_case block_case ite_case loop_case goto_case s)
-      (fun s _ => inductionOn cmd_case block_case ite_case loop_case goto_case s)
+      (fun s _ => inductionOn cmd_case block_case ite_case loop_case goto_case funcDecl_case s)
+      (fun s _ => inductionOn cmd_case block_case ite_case loop_case goto_case funcDecl_case s)
   | Stmt.loop guard measure invariant body md =>
     loop_case guard measure invariant body md
-      (fun s _ => inductionOn cmd_case block_case ite_case loop_case goto_case s)
+      (fun s _ => inductionOn cmd_case block_case ite_case loop_case goto_case funcDecl_case s)
   | Stmt.goto label md => goto_case label md
+  | Stmt.funcDecl decl md => funcDecl_case decl md
   termination_by s
 
 ---------------------------------------------------------------------
@@ -97,6 +103,7 @@ def Stmt.sizeOf (s : Imperative.Stmt P C) : Nat :=
   | .ite c tss ess _ => 3 + sizeOf c + Block.sizeOf tss + Block.sizeOf ess
   | .loop g _ _ bss _ => 3 + sizeOf g + Block.sizeOf bss
   | .goto _ _ => 1
+  | .funcDecl _ _ => 1
 
 @[simp]
 def Block.sizeOf (ss : Imperative.Block P C) : Nat :=
@@ -159,6 +166,11 @@ def Stmt.getVars [HasVarsPure P P.Expr] [HasVarsPure P C] (s : Stmt P C) : List
   | .ite _ tbss ebss _ => Block.getVars tbss ++ Block.getVars ebss
   | .loop _ _ _ bss _ => Block.getVars bss
   | .goto _ _  => []
+  | .funcDecl decl _ =>
+    -- Get variables from function body (including parameters for simplicity)
+    match decl.body with
+    | none => []
+    | some body => HasVarsPure.getVars body
   termination_by (Stmt.sizeOf s)
 
 def Block.getVars [HasVarsPure P P.Expr] [HasVarsPure P C] (ss : Block P C) : List P.Ident :=
@@ -183,6 +195,7 @@ def Stmt.definedVars [HasVarsImp P C] (s : Stmt P C) : List P.Ident :=
   | .cmd cmd => HasVarsImp.definedVars cmd
   | .block _ bss _ => Block.definedVars bss
   | .ite _ tbss ebss _ => Block.definedVars tbss ++ Block.definedVars ebss
+  | .funcDecl decl _ => [decl.name]  -- Function declaration defines the function name
   | _ => []
   termination_by (Stmt.sizeOf s)
 
@@ -202,6 +215,7 @@ def Stmt.modifiedVars [HasVarsImp P C] (s : Stmt P C) : List P.Ident :=
   | .block _ bss _ => Block.modifiedVars bss
   | .ite _ tbss ebss _ => Block.modifiedVars tbss ++ Block.modifiedVars ebss
   | .loop _ _ _ bss _ => Block.modifiedVars bss
+  | .funcDecl _ _ => []  -- Function declarations don't modify variables
   termination_by (Stmt.sizeOf s)
 
 def Block.modifiedVars [HasVarsImp P C] (ss : Block P C) : List P.Ident :=
@@ -262,6 +276,7 @@ def formatStmt (P : PureExpr) (s : Stmt P C)
   | .loop guard measure invariant body md => f!"{md}while ({guard}) ({measure}) ({invariant}) " ++
                         Format.bracket "{" f!"{formatBlock P body}" "}"
   | .goto label md => f!"{md}goto {label}"
+  | .funcDecl _ md => f!"{md}funcDecl <function>"
   termination_by s.sizeOf
 
 def formatBlock (P : PureExpr) (ss : List (Stmt P C))
diff --git a/Strata/DL/Lambda/Factory.lean b/Strata/DL/Lambda/Factory.lean
index 7fa3ea66f..7da3fcdd6 100644
--- a/Strata/DL/Lambda/Factory.lean
+++ b/Strata/DL/Lambda/Factory.lean
@@ -9,6 +9,8 @@ import Strata.DL.Lambda.LTy
 import Strata.DDM.Util.Array
 import Strata.DL.Util.List
 import Strata.DL.Util.ListMap
+import Strata.DL.Imperative.PureExpr
+import Strata.DL.Imperative.MetaData
 
 /-!
 ## Lambda's Factory
@@ -28,7 +30,7 @@ namespace Lambda
 
 open Std (ToFormat Format format)
 
-variable {T : LExprParams} [Inhabited T.Metadata] [ToFormat T.IDMeta]
+variable {T : LExprParams} [Inhabited T.Metadata]
 
 ---------------------------------------------------------------------
 
@@ -56,9 +58,11 @@ abbrev LTySignature := Signature IDMeta LTy
 
 
 /--
-A Lambda factory function, where the body can be optional. Universally
-quantified type identifiers, if any, appear before this signature and can
-quantify over the type identifiers in it.
+A generic function structure, parameterized by identifier, expression, type, and metadata types.
+
+This structure can be instantiated for different expression languages.
+For Lambda expressions, use `LFunc`. For other expression systems, instantiate
+with appropriate types.
 
 A optional evaluation function can be provided in the `concreteEval` field for
 each factory function to allow the partial evaluator to do constant propagation
@@ -84,44 +88,74 @@ concrete/constants, this fails and it returns .none.
 (TODO) Use `.bvar`s in the body to correspond to the formals instead of using
 `.fvar`s.
 -/
-structure LFunc (T : LExprParams) where
-  name     : T.Identifier
+structure Func (IdentT : Type) (ExprT : Type) (TyT : Type) (MetadataT : Type) where
+  name     : IdentT
   typeArgs : List TyIdentifier := []
   isConstr : Bool := false --whether function is datatype constructor
-  inputs   : @LMonoTySignature T.IDMeta
-  output   : LMonoTy
-  body     : Option (LExpr T.mono) := .none
+  inputs   : ListMap IdentT TyT
+  output   : TyT
+  body     : Option ExprT := .none
   -- (TODO): Add support for a fixed set of attributes (e.g., whether to inline
   -- a function, etc.).
   attr     : Array String := #[]
-  -- The T.Metadata argument is the metadata that will be attached to the
+  -- The MetadataT argument is the metadata that will be attached to the
   -- resulting expression of concreteEval if evaluation was successful.
-  concreteEval : Option (T.Metadata → List (LExpr T.mono) → Option (LExpr T.mono)) := .none
-  axioms   : List (LExpr T.mono) := []  -- For axiomatic definitions
+  concreteEval : Option (MetadataT → List ExprT → Option ExprT) := .none
+  axioms   : List ExprT := []  -- For axiomatic definitions
+
+/--
+A Lambda factory function - instantiation of `Func` for Lambda expressions.
+
+Universally quantified type identifiers, if any, appear before this signature and can
+quantify over the type identifiers in it.
+-/
+abbrev LFunc (T : LExprParams) := Func (T.Identifier) (LExpr T.mono) LMonoTy T.Metadata
+
+/--
+A function declaration for use with `PureExpr` - instantiation of `Func` for
+any expression system that implements the `PureExpr` interface.
+-/
+abbrev PureFunc (P : Imperative.PureExpr) := Func P.Ident P.Expr P.Ty P.ExprMetadata
+
+/--
+Helper constructor for LFunc to maintain backward compatibility.
+-/
+def LFunc.mk {T : LExprParams} (name : T.Identifier) (typeArgs : List TyIdentifier := [])
+    (isConstr : Bool := false) (inputs : ListMap T.Identifier LMonoTy) (output : LMonoTy)
+    (body : Option (LExpr T.mono) := .none) (attr : Array String := #[])
+    (concreteEval : Option (T.Metadata → List (LExpr T.mono) → Option (LExpr T.mono)) := .none)
+    (axioms : List (LExpr T.mono) := []) : LFunc T :=
+  Func.mk name typeArgs isConstr inputs output body attr concreteEval axioms
 
 /--
-Well-formedness properties of LFunc. These are split from LFunc because
-otherwise it becomes impossible to create a 'temporary' LFunc object whose
+Well-formedness properties of Func. These are split from Func because
+otherwise it becomes impossible to create a 'temporary' Func object whose
 wellformedness might not hold yet.
 -/
-structure LFuncWF {T : LExprParams} (f : LFunc T) where
+structure FuncWF {IdentT ExprT TyT MetadataT : Type} (f : Func IdentT ExprT TyT MetadataT) where
   -- No args have same name.
   arg_nodup:
-    List.Nodup (f.inputs.map (·.1.name))
+    List.Nodup (f.inputs.map (·.1))
+  -- concreteEval does not succeed if the length of args is incorrect.
+  concreteEval_argmatch:
+    ∀ fn md args res, f.concreteEval = .some fn
+      → fn md args = .some res
+      → args.length = f.inputs.length
+
+/--
+Well-formedness properties of LFunc - extends FuncWF with Lambda-specific properties.
+-/
+structure LFuncWF {T : LExprParams} (f : LFunc T) extends FuncWF f where
   -- Free variables of body must be arguments.
   body_freevars:
     ∀ b freevars, f.body = .some b
       → freevars = LExpr.freeVars b
       → (∀ fv, fv ∈ freevars →
           ∃ arg, List.Mem arg f.inputs ∧ fv.1.name = arg.1.name)
-  -- concreteEval does not succeed if the length of args is incorrect.
-  concreteEval_argmatch:
-    ∀ fn md args res, f.concreteEval = .some fn
-      → fn md args = .some res
-      → args.length = f.inputs.length
 
-instance LFuncWF.arg_nodup_decidable {T : LExprParams} (f : LFunc T):
-    Decidable (List.Nodup (f.inputs.map (·.1.name))) := by
+instance FuncWF.arg_nodup_decidable {IdentT ExprT TyT MetadataT : Type} [DecidableEq IdentT]
+    (f : Func IdentT ExprT TyT MetadataT):
+    Decidable (List.Nodup (f.inputs.map (·.1))) := by
   apply List.nodupDecidable
 
 instance LFuncWF.body_freevars_decidable {T : LExprParams} (f : LFunc T):
@@ -150,7 +184,8 @@ instance LFuncWF.body_freevars_decidable {T : LExprParams} (f : LFunc T):
   | .none => by
     apply isTrue; grind
 
--- LFuncWF.concreteEval_argmatch is not decidable.
+-- FuncWF.concreteEval_argmatch and LFuncWF.concreteEval_argmatch are not decidable.-- FuncWF.body_freevars is commented out as it's expression-type specific
+-- FuncWF.concreteEval_argmatch is not decidable.
 
 instance [Inhabited T.Metadata] [Inhabited T.IDMeta] : Inhabited (LFunc T) where
   default := { name := Inhabited.default, inputs := [], output := LMonoTy.bool }
@@ -163,7 +198,7 @@ instance : ToFormat (LFunc T) where
                     else f!"∀{f.typeArgs}."
     let type := f!"{typeArgs} ({Signature.format f.inputs}) → {f.output}"
     let sep := if f.body.isNone then f!";" else f!" :="
-    let body := if f.body.isNone then f!"" else Std.Format.indentD f!"({f.body.get!})"
+    let body := if f.body.isNone then f!"" else f!"<body>"
     f!"{attr}\
        func {f.name} : {type}{sep}\
        {body}"
diff --git a/Strata/Languages/B3/.gitignore b/Strata/Languages/B3/.gitignore
new file mode 100644
index 000000000..009e2742a
--- /dev/null
+++ b/Strata/Languages/B3/.gitignore
@@ -0,0 +1,2 @@
+# B3 reference source code (copied from ../b3 for reference only)
+b3-reference/
diff --git a/Strata/Languages/C_Simp/C_Simp.lean b/Strata/Languages/C_Simp/C_Simp.lean
index e292aa697..d9ce17abe 100644
--- a/Strata/Languages/C_Simp/C_Simp.lean
+++ b/Strata/Languages/C_Simp/C_Simp.lean
@@ -28,6 +28,7 @@ abbrev Expression : Imperative.PureExpr := {
   Ident := Lambda.Identifier Unit,
   Expr := Lambda.LExpr CSimpLParams.mono,
   Ty := Lambda.LTy,
+  ExprMetadata := CSimpLParams.Metadata,
   TyEnv := Lambda.TEnv Unit,
   TyContext := Lambda.LContext ⟨Unit, Unit⟩,
   EvalEnv := Lambda.LState ⟨Unit, String⟩,
diff --git a/Strata/Languages/C_Simp/Verify.lean b/Strata/Languages/C_Simp/Verify.lean
index 2c376f582..609321590 100644
--- a/Strata/Languages/C_Simp/Verify.lean
+++ b/Strata/Languages/C_Simp/Verify.lean
@@ -48,6 +48,7 @@ def translate_stmt (s: Imperative.Stmt C_Simp.Expression C_Simp.Command) : Core.
   | .block l b _md => .block l (b.map translate_stmt) {}
   | .ite cond thenb elseb _md => .ite (translate_expr cond) (thenb.map translate_stmt) (elseb.map translate_stmt) {}
   | .loop guard measure invariant body _md => .loop (translate_expr guard) (translate_opt_expr measure) (translate_opt_expr invariant) (body.map translate_stmt) {}
+  | .funcDecl _ _ => panic! "C_Simp does not support function declarations"
   | .goto label _md => .goto label {}
   termination_by s.sizeOf
   decreasing_by
diff --git a/Strata/Languages/Core/CallGraph.lean b/Strata/Languages/Core/CallGraph.lean
index 26ebda9ab..c23dd5f0a 100644
--- a/Strata/Languages/Core/CallGraph.lean
+++ b/Strata/Languages/Core/CallGraph.lean
@@ -102,6 +102,7 @@ partial def extractCallsFromStatement (stmt : Statement) : List String :=
     extractCallsFromStatements elseBody
   | .loop _ _ _ body _ => extractCallsFromStatements body
   | .goto _ _ => []
+  | .funcDecl _ _ => []
 
 /-- Extract procedure calls from a list of statements -/
 partial def extractCallsFromStatements (stmts : List Statement) : List String :=
diff --git a/Strata/Languages/Core/Env.lean b/Strata/Languages/Core/Env.lean
index 2ecb1694d..b06fb848d 100644
--- a/Strata/Languages/Core/Env.lean
+++ b/Strata/Languages/Core/Env.lean
@@ -16,25 +16,44 @@ open Imperative
 instance : ToFormat ExpressionMetadata :=
   show ToFormat Unit from inferInstance
 
+-- ToFormat instance for Expression.EvalEnv (which is Lambda.LState CoreLParams)
+instance : ToFormat Expression.EvalEnv := by
+  show ToFormat (Lambda.LState CoreLParams)
+  infer_instance
+
 -- ToFormat instance for Expression.Expr
 instance : ToFormat Expression.Expr := by
   show ToFormat (Lambda.LExpr CoreLParams.mono)
   infer_instance
 
--- Custom ToFormat instance for our specific Scope type to get the desired formatting
-private def formatScope (m : Map CoreIdent (Option Lambda.LMonoTy × Expression.Expr)) : Std.Format :=
+-- Custom ToFormat instance for Scopes to get the desired formatting
+def formatScopeMap (m : Map CoreIdent (Option Lambda.LMonoTy × Expression.Expr)) : Std.Format :=
   match m with
   | [] => ""
-  | [(k, (ty, v))] => go k ty v
-  | (k, (ty, v)) :: rest =>
-    go k ty v ++ Format.line ++ formatScope rest
-  where go k ty v :=
+  | [(k, (ty, v))] =>
     match ty with
     | some ty => f!"({k} : {ty}) → {v}"
     | none => f!"{k} → {v}"
+  | (k, (ty, v)) :: rest =>
+    let entry := match ty with
+      | some ty => f!"({k} : {ty}) → {v}"
+      | none => f!"{k} → {v}"
+    entry ++ Format.line ++ formatScopeMap rest
 
+def formatScopes (ms : Lambda.Scopes CoreLParams) : Std.Format :=
+  match ms with
+  | [] => ""
+  | [m] => f!"[{formatScopeMap m}]"
+  | m :: rest => f!"[{formatScopeMap m}]{Format.line}" ++ formatScopes rest
+
+@[default_instance 1000]
+instance : ToFormat (Lambda.Scopes CoreLParams) where
+  format := formatScopes
+
+-- Also provide the instance for single Map for compatibility
+@[default_instance 1000]
 instance : ToFormat (Map CoreIdent (Option Lambda.LMonoTy × Expression.Expr)) where
-  format := formatScope
+  format := formatScopeMap
 
 instance : Inhabited ExpressionMetadata :=
   show Inhabited Unit from inferInstance
@@ -151,6 +170,19 @@ def Env.init (empty_factory:=false): Env :=
     warnings := []
     deferred := ∅ }
 
+-- Custom formatter for Env that uses the proper scope formatting
+def Env.format (s : Env) : Std.Format :=
+  let stateFormat := formatScopes s.exprEnv.state
+  let configFormat := (inferInstance : ToFormat (Lambda.EvalConfig CoreLParams)).format s.exprEnv.config
+  Std.format f!"Error:{Format.line}{s.error}{Format.line}\
+            Subst Map:{Format.line}{s.substMap}{Format.line}\
+            Expression Env:{Format.line}State:{Format.line}{stateFormat}{Format.line}{Format.line}\
+            Evaluation Config:{Format.line}{configFormat}{Format.line}{Format.line}{Format.line}\
+            Datatypes:{Format.line}{s.datatypes}{Format.line}\
+            Path Conditions:{Format.line}{PathConditions.format s.pathConditions}{Format.line}{Format.line}\
+            Warnings:{Format.line}{s.warnings}{Format.line}\
+            Deferred Proof Obligations:{Format.line}{s.deferred}{Format.line}"
+
 instance : EmptyCollection Env where
   emptyCollection := Env.init (empty_factory := true)
 
@@ -158,15 +190,7 @@ instance : Inhabited Env where
   default := Env.init
 
 instance : ToFormat Env where
-  format s :=
-    let { error, program := _, substMap, exprEnv, datatypes, distinct := _, pathConditions, warnings, deferred }  := s
-    format f!"Error:{Format.line}{error}{Format.line}\
-              Subst Map:{Format.line}{substMap}{Format.line}\
-              Expression Env:{Format.line}{exprEnv}{Format.line}\
-              Datatypes:{Format.line}{datatypes}{Format.line}\
-              Path Conditions:{Format.line}{PathConditions.format pathConditions}{Format.line}{Format.line}\
-              Warnings:{Format.line}{warnings}{Format.line}\
-              Deferred Proof Obligations:{Format.line}{deferred}{Format.line}"
+  format := Env.format
 
 /--
 Create a substitution map from all non-global variables to their values.
diff --git a/Strata/Languages/Core/Expressions.lean b/Strata/Languages/Core/Expressions.lean
index 60d37b6f7..32bd6c7df 100644
--- a/Strata/Languages/Core/Expressions.lean
+++ b/Strata/Languages/Core/Expressions.lean
@@ -22,6 +22,7 @@ abbrev Expression : Imperative.PureExpr :=
      EqIdent := inferInstanceAs (DecidableEq (Lambda.Identifier _))
      Expr := Lambda.LExpr ⟨⟨ExpressionMetadata, Visibility⟩, Lambda.LMonoTy⟩,
      Ty := Lambda.LTy,
+     ExprMetadata := ExpressionMetadata,
      TyEnv := @Lambda.TEnv Visibility,
      TyContext := @Lambda.LContext ⟨ExpressionMetadata, Visibility⟩,
      EvalEnv := Lambda.LState ⟨ExpressionMetadata, Visibility⟩ }
diff --git a/Strata/Languages/Core/Factory.lean b/Strata/Languages/Core/Factory.lean
index ee1e98e7c..845cdc33f 100644
--- a/Strata/Languages/Core/Factory.lean
+++ b/Strata/Languages/Core/Factory.lean
@@ -565,7 +565,10 @@ set_option maxHeartbeats 4000000 in
 Wellformedness of Factory
 -/
 theorem Factory_wf :
-    FactoryWF Factory := by
+    FactoryWF Factory := by sorry -- TODO: Requires handling ~200+ functions including dynamically generated BV ops
+  /-
+  -- The proof needs to show LFuncWF for each function in the factory
+  -- Challenge: ExpandBVOpFuncNames generates many functions at compile time
   unfold Factory
   apply FactoryWF.mk
   · decide -- FactoryWF.name_nodup
@@ -596,5 +599,5 @@ theorem Factory_wf :
             intros lf md args res
             repeat (rcases args with _ | ⟨ args0, args ⟩ <;> try grind)))
     contradiction
-
+-/
 end Core
diff --git a/Strata/Languages/Core/FunctionType.lean b/Strata/Languages/Core/FunctionType.lean
index 76d4af933..415070c29 100644
--- a/Strata/Languages/Core/FunctionType.lean
+++ b/Strata/Languages/Core/FunctionType.lean
@@ -40,12 +40,12 @@ def typeCheck (C: Core.Expression.TyContext) (Env : Core.Expression.TyEnv) (func
   | some body =>
     -- Temporarily add formals in the context.
     let Env := Env.pushEmptyContext
-    let Env := Env.addToContext func.inputPolyTypes
+    let Env := Env.addToContext (LFunc.inputPolyTypes func)
     -- Type check and annotate the body, and ensure that it unifies with the
     -- return type.
     let (bodya, Env) ← LExpr.resolve C Env body
     let bodyty := bodya.toLMonoTy
-    let (retty, Env) ← func.outputPolyType.instantiateWithCheck C Env
+    let (retty, Env) ← (LFunc.outputPolyType func).instantiateWithCheck C Env
     let S ← Constraints.unify [(retty, bodyty)] Env.stateSubstInfo |>.mapError format
     let Env := Env.updateSubst S
     let Env := Env.popContext
diff --git a/Strata/Languages/Core/ProcedureType.lean b/Strata/Languages/Core/ProcedureType.lean
index 4cd2df305..9003ea9af 100644
--- a/Strata/Languages/Core/ProcedureType.lean
+++ b/Strata/Languages/Core/ProcedureType.lean
@@ -18,6 +18,21 @@ namespace Core
 open Std (ToFormat Format format)
 open Imperative (MetaData)
 
+instance : ToFormat (Lambda.LFunc { Metadata := ExpressionMetadata, IDMeta := Visibility }) where
+  format f :=
+    let attr := if f.attr.isEmpty then f!"" else f!"@[{f.attr}]{Format.line}"
+    let typeArgs := if f.typeArgs.isEmpty
+                    then f!""
+                    else f!"∀{f.typeArgs}."
+    let type := f!"{typeArgs} ({Lambda.Signature.format f.inputs}) → {f.output}"
+    let sep := if f.body.isNone then f!";" else f!" :="
+    let body := match f.body with
+                | none => f!""
+                | some e => f!"{Format.line}  {format e}"
+    f!"{attr}\
+       func {f.name} : {type}{sep}\
+       {body}"
+
 namespace Procedure
 
 private def checkNoDuplicates (proc : Procedure) (sourceLoc : Format) :
diff --git a/Strata/Languages/Core/ProcedureWF.lean b/Strata/Languages/Core/ProcedureWF.lean
index 68ce457bb..ba8ea590e 100644
--- a/Strata/Languages/Core/ProcedureWF.lean
+++ b/Strata/Languages/Core/ProcedureWF.lean
@@ -31,7 +31,6 @@ theorem snd_values_mem {ps : ListMap CoreLabel Procedure.Check} :
 
 theorem Procedure.typeCheckWF : Procedure.typeCheck C T p pp md = Except.ok (pp', T') → WFProcedureProp p pp := by sorry
 
-
 /-
 set_option warn.sorry false in
 /--
diff --git a/Strata/Languages/Core/Program.lean b/Strata/Languages/Core/Program.lean
index 67fe33ddd..ae1ae4910 100644
--- a/Strata/Languages/Core/Program.lean
+++ b/Strata/Languages/Core/Program.lean
@@ -15,6 +15,7 @@ import Strata.Languages.Core.Axiom
 
 namespace Core
 
+open Lambda
 open Std (ToFormat Format format)
 open Imperative
 
@@ -24,6 +25,20 @@ instance : Inhabited TypeDecl where
 
 -- ToFormat instance for Function (which is LFunc CoreLParams)
 -- Note: ToFormat CoreLParams.Identifier is now defined in Identifiers.lean
+instance : ToFormat Function where
+  format f :=
+    let attr := if f.attr.isEmpty then f!"" else f!"@[{f.attr}]{Format.line}"
+    let typeArgs := if f.typeArgs.isEmpty
+                    then f!""
+                    else f!"∀{f.typeArgs}."
+    let type := f!"{typeArgs} ({Lambda.Signature.format f.inputs}) → {f.output}"
+    let sep := if f.body.isNone then f!";" else f!" :="
+    let body := match f.body with
+                | none => f!""
+                | some e => f!"{Format.line}  {format e}"
+    f!"{attr}\
+       func {f.name} : {type}{sep}\
+       {body}"
 
 inductive DeclKind : Type where
   | var | type | ax | distinct | proc | func
diff --git a/Strata/Languages/Core/Statement.lean b/Strata/Languages/Core/Statement.lean
index eaa843393..82ebed900 100644
--- a/Strata/Languages/Core/Statement.lean
+++ b/Strata/Languages/Core/Statement.lean
@@ -15,7 +15,7 @@ import Strata.DL.Imperative.HasVars
 import Strata.DL.Lambda.LExpr
 
 namespace Core
-open Imperative
+open Lambda Imperative
 open Std (ToFormat Format format)
 ---------------------------------------------------------------------
 
@@ -126,6 +126,12 @@ def Statement.eraseTypes (s : Statement) : Statement :=
     let body' := Statements.eraseTypes bss
     .loop guard measure invariant body' md
   | .goto l md => .goto l md
+  | .funcDecl decl md =>
+    -- Erase types from function body and axioms
+    let decl' := { decl with
+      body := decl.body.map Lambda.LExpr.eraseTypes,
+      axioms := decl.axioms.map Lambda.LExpr.eraseTypes }
+    .funcDecl decl' md
   termination_by (Stmt.sizeOf s)
   decreasing_by
   all_goals simp_wf <;> simp [sizeOf] <;> omega
@@ -203,6 +209,7 @@ def Statement.modifiedVarsTrans
     Statements.modifiedVarsTrans π tbss ++ Statements.modifiedVarsTrans π ebss
   | .loop _ _ _ bss _ =>
     Statements.modifiedVarsTrans π bss
+  | .funcDecl _ _ => []  -- Function declarations don't modify variables
   termination_by (Stmt.sizeOf s)
 
 def Statements.modifiedVarsTrans
@@ -241,6 +248,11 @@ def Statement.getVarsTrans
     Statements.getVarsTrans π tbss ++ Statements.getVarsTrans π ebss
   | .loop _ _ _ bss  _ =>
     Statements.getVarsTrans π bss
+  | .funcDecl decl _ =>
+    -- Get variables from function body (including parameters for simplicity)
+    match decl.body with
+    | none => []
+    | some body => HasVarsPure.getVars body
   termination_by (Stmt.sizeOf s)
 
 def Statements.getVarsTrans
@@ -284,6 +296,7 @@ def Statement.touchedVarsTrans
   | .block _ bss _ => Statements.touchedVarsTrans π bss
   | .ite _ tbss ebss _ => Statements.touchedVarsTrans π tbss ++ Statements.touchedVarsTrans π ebss
   | .loop _ _ _ bss _ => Statements.touchedVarsTrans π bss
+  | .funcDecl decl _ => [decl.name]  -- Function declaration touches (defines) the function name
   termination_by (Stmt.sizeOf s)
 
 def Statements.touchedVarsTrans
@@ -347,6 +360,12 @@ def Statement.substFvar (s : Core.Statement)
           (Block.substFvar body fr to)
           metadata
   | .goto _ _ => s
+  | .funcDecl decl md =>
+    -- Substitute in function body and axioms
+    let decl' := { decl with
+      body := decl.body.map (Lambda.LExpr.substFvar · fr to),
+      axioms := decl.axioms.map (Lambda.LExpr.substFvar · fr to) }
+    .funcDecl decl' md
   termination_by s.sizeOf
   decreasing_by all_goals(simp_wf; try omega)
 end
@@ -373,6 +392,10 @@ def Statement.renameLhs (s : Core.Statement)
       if l.name == fr  then to else l)) pname args metadata
   | .block lbl b metadata =>
     .block lbl (Block.renameLhs b fr to) metadata
+  | .funcDecl decl md =>
+    -- Rename function name if it matches
+    let decl' := if decl.name == fr then { decl with name := to } else decl
+    .funcDecl decl' md
   | .havoc _ _ | .assert _ _ _ | .assume _ _ _ | .ite _ _ _ _
   | .loop _ _ _ _ _ | .goto _ _ | .cover _ _ _ => s
   termination_by s.sizeOf
diff --git a/Strata/Languages/Core/StatementEval.lean b/Strata/Languages/Core/StatementEval.lean
index 34749e28e..2779f011e 100644
--- a/Strata/Languages/Core/StatementEval.lean
+++ b/Strata/Languages/Core/StatementEval.lean
@@ -163,7 +163,7 @@ def Statement.containsCmd (predicate : Imperative.Cmd Expression → Bool) (s :
   | .ite _ then_ss else_ss _ => Statements.containsCmds predicate then_ss ||
                                 Statements.containsCmds predicate else_ss
   | .loop _ _ _ body_ss _ => Statements.containsCmds predicate body_ss
-  | .goto _ _ => false
+  | .funcDecl _ _ | .goto _ _ => false  -- Function declarations and gotos don't contain commands
   termination_by Imperative.Stmt.sizeOf s
 
 /--
@@ -202,7 +202,7 @@ def Statement.collectCovers (s : Statement) : List (String × Imperative.MetaDat
   | .block _ inner_ss _ => Statements.collectCovers inner_ss
   | .ite _ then_ss else_ss _ => Statements.collectCovers then_ss ++ Statements.collectCovers else_ss
   | .loop _ _ _ body_ss _ => Statements.collectCovers body_ss
-  | .goto _ _ => []
+  | .funcDecl _ _ | .goto _ _ => []  -- Function declarations and gotos don't contain cover commands
   termination_by Imperative.Stmt.sizeOf s
 /--
 Collect all `cover` commands from statements `ss` with their labels and metadata.
@@ -226,7 +226,7 @@ def Statement.collectAsserts (s : Statement) : List (String × Imperative.MetaDa
   | .block _ inner_ss _ => Statements.collectAsserts inner_ss
   | .ite _ then_ss else_ss _ => Statements.collectAsserts then_ss ++ Statements.collectAsserts else_ss
   | .loop _ _ _ body_ss _ => Statements.collectAsserts body_ss
-  | .goto _ _ => []
+  | .funcDecl _ _ | .goto _ _ => []  -- Function declarations and gotos don't contain assert commands
   termination_by Imperative.Stmt.sizeOf s
 /--
 Collect all `assert` commands from statements `ss` with their labels and metadata.
@@ -377,6 +377,27 @@ def evalAuxGo (steps : Nat) (old_var_subst : SubstMap) (Ewn : EnvWithNext) (ss :
                     Please transform your program to eliminate loops before \
                     calling Core.Statement.evalAux"
 
+          | .funcDecl decl _ =>
+            -- Add function to factory
+            -- Convert PureFunc Expression (with LTy) to LFunc CoreLParams (with LMonoTy)
+            -- Assumes type checking has already monomorphized the types to .forAll [] mty
+            let func : Lambda.LFunc CoreLParams := {
+              name := decl.name,
+              typeArgs := decl.typeArgs,
+              isConstr := decl.isConstr,
+              inputs := decl.inputs.map (fun (id, ty) => (id, Lambda.LTy.toMonoTypeUnsafe ty)),
+              output := Lambda.LTy.toMonoTypeUnsafe decl.output,
+              body := decl.body,
+              attr := decl.attr,
+              concreteEval := decl.concreteEval,
+              axioms := decl.axioms
+            }
+            match Ewn.env.addFactoryFunc func with
+            | .ok env' => [{ Ewn with env := env' }]
+            | .error e =>
+              -- If adding fails, set error but continue
+              [{ Ewn with env := { Ewn.env with error := some (.Misc e) } }]
+
           | .goto l md => [{ Ewn with stk := Ewn.stk.appendToTop [.goto l md], nextLabel := (some l)}]
 
       List.flatMap (fun (ewn : EnvWithNext) => go' ewn rest ewn.nextLabel) EAndNexts
diff --git a/Strata/Languages/Core/StatementType.lean b/Strata/Languages/Core/StatementType.lean
index 8e7c3a400..743c6f50d 100644
--- a/Strata/Languages/Core/StatementType.lean
+++ b/Strata/Languages/Core/StatementType.lean
@@ -10,6 +10,7 @@ import Strata.Languages.Core.Statement
 import Strata.Languages.Core.CmdType
 import Strata.Languages.Core.Program
 import Strata.Languages.Core.OldExpressions
+import Strata.Languages.Core.FunctionType
 import Strata.DL.Imperative.CmdType
 
 namespace Core
@@ -165,6 +166,37 @@ where
             -- Add source location to error messages.
             .error (errorWithSourceLoc e md)
 
+        | .funcDecl decl md => do try
+          -- Type check the function declaration
+          -- Manually convert PureFunc Expression to Function for type checking
+          let func : Function := {
+            name := decl.name,
+            typeArgs := decl.typeArgs,
+            isConstr := decl.isConstr,
+            inputs := decl.inputs.map (fun (id, ty) => (id, Lambda.LTy.toMonoTypeUnsafe ty)),
+            output := Lambda.LTy.toMonoTypeUnsafe decl.output,
+            body := decl.body,
+            attr := decl.attr,
+            concreteEval := none,  -- Can't convert concreteEval safely
+            axioms := decl.axioms
+          }
+          let (func', Env) ← Function.typeCheck C Env func
+          -- Convert back by wrapping monotypes in trivial polytypes
+          let decl' : PureFunc Expression := {
+            name := func'.name,
+            typeArgs := func'.typeArgs,
+            isConstr := func'.isConstr,
+            inputs := func'.inputs.map (fun (id, mty) => (id, .forAll [] mty)),
+            output := .forAll [] func'.output,
+            body := func'.body,
+            attr := func'.attr,
+            concreteEval := decl.concreteEval,  -- Preserve original
+            axioms := func'.axioms
+          }
+          .ok (.funcDecl decl' md, Env)
+          catch e =>
+            .error (errorWithSourceLoc e md)
+
       go Env srest (s' :: acc)
     termination_by Block.sizeOf ss
     decreasing_by
@@ -208,6 +240,13 @@ def Statement.subst (S : Subst) (s : Statement) : Statement :=
   | .loop guard m i bss md =>
     .loop (guard.applySubst S) (substOptionExpr S m) (substOptionExpr S i) (go S bss []) md
   | .goto _ _ => s
+  | .funcDecl decl md =>
+    let decl' := { decl with
+      inputs := decl.inputs.map (fun (id, ty) => (id, Lambda.LTy.subst S ty)),
+      output := Lambda.LTy.subst S decl.output,
+      body := decl.body.map (·.applySubst S),
+      axioms := decl.axioms.map (·.applySubst S) }
+    .funcDecl decl' md
   where
     go S ss acc : List Statement :=
     match ss with
diff --git a/Strata/Languages/Core/StatementWF.lean b/Strata/Languages/Core/StatementWF.lean
index 0b79fc324..2e7e20695 100644
--- a/Strata/Languages/Core/StatementWF.lean
+++ b/Strata/Languages/Core/StatementWF.lean
@@ -125,6 +125,14 @@ theorem Statement.typeCheckAux_go_WF :
       any_goals (try simp [WFStatementsProp] at *; try simp [List.Forall_append, *]; try constructor)
       any_goals (simp [Forall])
       any_goals constructor
+    | funcDecl decl md =>
+      simp [Except.bind] at tcok
+      repeat (split at tcok <;> try contradiction)
+      have tcok := Statement.typeCheckAux_elim_singleton tcok
+      rw[List.append_cons];
+      apply ih tcok <;> try assumption
+      simp [WFStatementsProp] at *
+      simp [List.Forall_append, Forall, *]
 
 /--
 A list of Statement `ss` that passes type checking is well formed with respect
diff --git a/Strata/Languages/Core/WF.lean b/Strata/Languages/Core/WF.lean
index 4a79db2d3..3cee9cb52 100644
--- a/Strata/Languages/Core/WF.lean
+++ b/Strata/Languages/Core/WF.lean
@@ -79,6 +79,7 @@ def WFStatementProp (p : Program) (stmt : Statement) : Prop := match stmt with
   | .loop  (guard : Expression.Expr) (measure : Option Expression.Expr) (invariant : Option Expression.Expr) (body : Block) _ =>
      WFloopProp (CmdExt Expression) p guard measure invariant body
   | .goto (label : String) _ => WFgotoProp p label
+  | .funcDecl _ _ => True  -- Function declarations are always well-formed at this level
 
 abbrev WFStatementsProp (p : Program) := Forall (WFStatementProp p)
 
diff --git a/Strata/Transform/CallElimCorrect.lean b/Strata/Transform/CallElimCorrect.lean
index 2f32c8163..40206305e 100644
--- a/Strata/Transform/CallElimCorrect.lean
+++ b/Strata/Transform/CallElimCorrect.lean
@@ -179,6 +179,7 @@ theorem callElimBlockNoExcept :
   | ite cd tb eb md => exists [.ite cd tb eb md]
   | goto l b => exists [.goto l b]
   | loop g m i b md => exists [.loop g m i b md]
+  | funcDecl _ _ => sorry  -- TODO: Add funcDecl case to CallElimCorrect proof
   | cmd c =>
     cases c with
     | cmd c' => exists [Imperative.Stmt.cmd (CmdExt.cmd c')]
@@ -3298,6 +3299,7 @@ theorem callElimStatementCorrect [LawfulBEq Expression.Expr] :
   case ite => exact ⟨σ', Inits.init InitVars.init_none, Heval⟩
   case goto => exact ⟨σ', Inits.init InitVars.init_none, Heval⟩
   case loop => exact ⟨σ', Inits.init InitVars.init_none, Heval⟩
+  case funcDecl => sorry  -- TODO: Add funcDecl case to CallElimCorrect proof
   case cmd c =>
   cases c with
   | cmd c' =>
diff --git a/Strata/Transform/CoreTransform.lean b/Strata/Transform/CoreTransform.lean
index d4bd7664b..74bd2ef35 100644
--- a/Strata/Transform/CoreTransform.lean
+++ b/Strata/Transform/CoreTransform.lean
@@ -224,6 +224,7 @@ def runStmtsRec (f : Command → Program → CoreTransformM (List Statement))
       | .loop guard measure invariant body md => do
         let body' ← runStmtsRec f body inputProg
         return [.loop guard measure invariant body' md]
+      | .funcDecl _ _ => return [s]  -- Function declarations pass through unchanged
       | .goto _lbl _md =>
         return [s])
     return (sres ++ ss'')
diff --git a/Strata/Transform/DetToNondet.lean b/Strata/Transform/DetToNondet.lean
index ec163de41..6bf37da83 100644
--- a/Strata/Transform/DetToNondet.lean
+++ b/Strata/Transform/DetToNondet.lean
@@ -29,6 +29,7 @@ def StmtToNondetStmt {P : PureExpr} [Imperative.HasBool P] [HasNot P]
   | .loop   guard _measure _inv bss md =>
     .loop (.seq (.assume "guard" guard md) (BlockToNondetStmt bss))
   | .goto _ _ => (.assume "skip" Imperative.HasBool.tt)
+  | .funcDecl _ _ => (.assume "skip" Imperative.HasBool.tt)
 
 /-- Deterministic-to-nondeterministic transformation for multiple
 (deterministic) statements -/
diff --git a/Strata/Transform/LoopElim.lean b/Strata/Transform/LoopElim.lean
index 69d8e5772..a35f423d0 100644
--- a/Strata/Transform/LoopElim.lean
+++ b/Strata/Transform/LoopElim.lean
@@ -56,6 +56,7 @@ def Stmt.removeLoopsM
     pure (.block label bss md)
   | .cmd _ => pure s
   | .goto _ _ => pure s
+  | .funcDecl _ _ => pure s  -- Function declarations pass through unchanged
 
 def Block.removeLoopsM
   [HasNot P] [HasVarsImp P C] [HasHavoc P C] [HasPassiveCmds P C]
diff --git a/Strata/Transform/ProcedureInlining.lean b/Strata/Transform/ProcedureInlining.lean
index 8f40ca343..9ce562fa5 100644
--- a/Strata/Transform/ProcedureInlining.lean
+++ b/Strata/Transform/ProcedureInlining.lean
@@ -55,6 +55,12 @@ def Statement.substFvar (s : Core.Statement)
           (Option.map (Lambda.LExpr.substFvar · fr to) invariant)
           (Block.substFvar body fr to)
           metadata
+  | .funcDecl decl md =>
+    -- Substitute in function body and axioms
+    let decl' := { decl with
+      body := decl.body.map (Lambda.LExpr.substFvar · fr to),
+      axioms := decl.axioms.map (Lambda.LExpr.substFvar · fr to) }
+    .funcDecl decl' md
   | .goto _ _ => s
   termination_by s.sizeOf
 end
@@ -82,6 +88,10 @@ def Statement.renameLhs (s : Core.Statement) (fr: Lambda.Identifier Visibility)
   | .loop m g i b md =>
     .loop m g i (Block.renameLhs b fr to) md
   | .havoc l md => .havoc (if l.name == fr then to else l) md
+  | .funcDecl decl md =>
+    -- Rename function name if it matches
+    let decl' := if decl.name == fr then { decl with name := to } else decl
+    .funcDecl decl' md
   | .assert _ _ _ | .assume _ _ _ | .cover _ _ _ | .goto _ _ => s
   termination_by s.sizeOf
 end
diff --git a/StrataTest/Backends/CBMC/CoreToCProverGOTO.lean b/StrataTest/Backends/CBMC/CoreToCProverGOTO.lean
index d5cfa0a46..96d43cb4a 100644
--- a/StrataTest/Backends/CBMC/CoreToCProverGOTO.lean
+++ b/StrataTest/Backends/CBMC/CoreToCProverGOTO.lean
@@ -27,6 +27,7 @@ abbrev Core.ExprStr : Imperative.PureExpr :=
    { Ident := CoreParams.Identifier,
      Expr := Lambda.LExpr CoreParams.mono,
      Ty := Lambda.LTy,
+     ExprMetadata := CoreParams.Metadata,
      TyEnv := @Lambda.TEnv CoreParams.IDMeta,
      TyContext := @Lambda.LContext CoreParams,
      EvalEnv := Lambda.LState CoreParams
diff --git a/StrataTest/Backends/CBMC/ToCProverGOTO.lean b/StrataTest/Backends/CBMC/ToCProverGOTO.lean
index 4ba14958f..bbde1c8be 100644
--- a/StrataTest/Backends/CBMC/ToCProverGOTO.lean
+++ b/StrataTest/Backends/CBMC/ToCProverGOTO.lean
@@ -21,6 +21,7 @@ private abbrev LExprTP : Imperative.PureExpr :=
    { Ident := TestParams.Identifier,
      Expr := Lambda.LExprT TestParams.mono,
      Ty := Lambda.LMonoTy,
+     ExprMetadata := TestParams.Metadata,
      TyEnv := @Lambda.TEnv TestParams.IDMeta,
      TyContext := @Lambda.LContext TestParams,
      EvalEnv := Lambda.LState TestParams
diff --git a/StrataTest/DL/Imperative/ArithExpr.lean b/StrataTest/DL/Imperative/ArithExpr.lean
index 8c98cda42..81143fd59 100644
--- a/StrataTest/DL/Imperative/ArithExpr.lean
+++ b/StrataTest/DL/Imperative/ArithExpr.lean
@@ -96,6 +96,7 @@ abbrev PureExpr : PureExpr :=
    { Ident := String,
      Expr := Expr,
      Ty := Ty,
+     ExprMetadata := Unit,
      TyEnv := TEnv,
      TyContext := Unit,
      EvalEnv := Env,
diff --git a/StrataTest/DL/Lambda/LExprTTests.lean b/StrataTest/DL/Lambda/LExprTTests.lean
index 3cf790ee8..a83848311 100644
--- a/StrataTest/DL/Lambda/LExprTTests.lean
+++ b/StrataTest/DL/Lambda/LExprTTests.lean
@@ -17,6 +17,21 @@ open LTy.Syntax LExpr.SyntaxMono LExpr LMonoTy
 
 private abbrev TestParams : LExprParams := ⟨Unit, Unit⟩
 
+private instance : ToFormat (Lambda.LFunc { Metadata := Unit, IDMeta := Unit }) where
+  format f :=
+    let attr := if f.attr.isEmpty then f!"" else f!"@[{f.attr}]{Format.line}"
+    let typeArgs := if f.typeArgs.isEmpty
+                    then f!""
+                    else f!"∀{f.typeArgs}."
+    let type := f!"{typeArgs} ({Lambda.Signature.format f.inputs}) → {f.output}"
+    let sep := if f.body.isNone then f!";" else f!" :="
+    let body := match f.body with
+                | none => f!""
+                | some e => f!"{Format.line}  {format e}"
+    f!"{attr}\
+       func {f.name} : {type}{sep}\
+       {body}"
+
 private instance : Coe String TestParams.Identifier where
   coe s := Identifier.mk s ()
 
diff --git a/StrataTest/DL/Lambda/TypeFactoryTests.lean b/StrataTest/DL/Lambda/TypeFactoryTests.lean
index 0a4eba152..59f1a3a68 100644
--- a/StrataTest/DL/Lambda/TypeFactoryTests.lean
+++ b/StrataTest/DL/Lambda/TypeFactoryTests.lean
@@ -19,6 +19,21 @@ open LExpr LTy
 
 private abbrev TestParams : LExprParams := ⟨Unit, Unit⟩
 
+private instance : ToFormat (LFunc TestParams) where
+  format f :=
+    let attr := if f.attr.isEmpty then f!"" else f!"@[{f.attr}]{Format.line}"
+    let typeArgs := if f.typeArgs.isEmpty
+                    then f!""
+                    else f!"∀{f.typeArgs}."
+    let type := f!"{typeArgs} ({Signature.format f.inputs}) → {f.output}"
+    let sep := if f.body.isNone then f!";" else f!" :="
+    let body := match f.body with
+                | none => f!""
+                | some e => f!"{Format.line}  {format e}"
+    f!"{attr}\
+       func {f.name} : {type}{sep}\
+       {body}"
+
 private instance : Coe String TestParams.Identifier where
   coe s := Identifier.mk s ()
 
diff --git a/StrataTest/Languages/Core/Examples/Regex.lean b/StrataTest/Languages/Core/Examples/Regex.lean
index 54105ea2d..4710f9446 100644
--- a/StrataTest/Languages/Core/Examples/Regex.lean
+++ b/StrataTest/Languages/Core/Examples/Regex.lean
@@ -221,7 +221,7 @@ Original expression: (((~Re.Loop ((~Re.Range #a) #z)) #1) %0)
 
 Evaluated program:
 func bad_re_loop :  ((n : int)) → regex :=
-  (((((~Re.Loop : (arrow regex (arrow int (arrow int regex)))) (((~Re.Range : (arrow string (arrow string regex))) #a) #z)) #1) (n : int)))
+  ((((~Re.Loop : (arrow regex (arrow int (arrow int regex)))) (((~Re.Range : (arrow string (arrow string regex))) #a) #z)) #1) (n : int))
 (procedure main :  ((n : int)) → ())
 modifies: []
 preconditions: ⏎
@@ -241,7 +241,7 @@ Original expression: (((~Re.Loop ((~Re.Range #a) #z)) #1) %0)
 
 Evaluated program:
 func bad_re_loop :  ((n : int)) → regex :=
-  (((((~Re.Loop : (arrow regex (arrow int (arrow int regex)))) (((~Re.Range : (arrow string (arrow string regex))) #a) #z)) #1) (n : int)))
+  ((((~Re.Loop : (arrow regex (arrow int (arrow int regex)))) (((~Re.Range : (arrow string (arrow string regex))) #a) #z)) #1) (n : int))
 (procedure main :  ((n : int)) → ())
 modifies: []
 preconditions: ⏎
diff --git a/StrataTest/Languages/Core/StatementEvalTests.lean b/StrataTest/Languages/Core/StatementEvalTests.lean
index 8281bec1c..0282d3337 100644
--- a/StrataTest/Languages/Core/StatementEvalTests.lean
+++ b/StrataTest/Languages/Core/StatementEvalTests.lean
@@ -48,7 +48,7 @@ Proof Obligation:
 #guard_msgs in
 #eval (evalOne ∅ ∅ [.init "x" t[int] eb[#0],
                     .set "x" eb[#18],
-                    .assert "x_eq_18" eb[x == #18]]) |>.snd |> format
+                    .assert "x_eq_18" eb[x == #18]]) |>.snd |> Env.format
 
 /--
 info: Error:
@@ -88,7 +88,7 @@ Proof Obligation:
   ∅
   [.init "x" t[int] eb[#0],
   .set "x" eb[y],
-  .assert "x_eq_12" eb[x == #12]]) |>.snd |> format
+  .assert "x_eq_12" eb[x == #12]]) |>.snd |> Env.format
 
 /--
 info: Error:
@@ -122,7 +122,7 @@ Deferred Proof Obligations:
 #eval evalOne ∅ ∅
        [
        .init "x" t[bool] eb[x == #true]
-       ] |>.snd |> format
+       ] |>.snd |> Env.format
 
 /--
 info: Error:
@@ -182,7 +182,7 @@ Proof Obligation:
   .assert "m_2_eq_20" eb[(m #2) == #20],
   .set "m" eb[λ (if (%0 == #3) then #30 else ((m : int → int) %0))],
   .assert "m_1_eq_10" eb[(m #1) == #10]
-  ]) |>.snd |> format
+  ]) |>.snd |> Env.format
 
 /--
 info: Error:
@@ -239,7 +239,7 @@ Proof Obligation:
   .assert "m_2_eq_20" eb[(m #2) == #20],
   .set "m" eb[λ (if (%0 == #3) then #30 else (m %0))],
   .assert "m_1_eq_10" eb[(m #1) == #10]
-  ]) |>.snd |> format
+  ]) |>.snd |> Env.format
 
 
 
@@ -320,7 +320,7 @@ Proof Obligation:
 ((if (zinit == #false) then #6 else #0) == #6)
 -/
 #guard_msgs in
-#eval (evalOne ∅ ∅ prog1) |>.snd |> format
+#eval (evalOne ∅ ∅ prog1) |>.snd |> Env.format
 
 
 private def prog2 : Statements := [
@@ -375,7 +375,125 @@ Proof Obligation:
 (($__x0 : int) == #1)
 -/
 #guard_msgs in
-#eval (evalOne ∅ ∅ prog2) |>.snd |> format
+#eval (evalOne ∅ ∅ prog2) |>.snd |> Env.format
+
+/--
+Test funcDecl: declare a helper function and use it
+-/
+def testFuncDecl : List Statement :=
+  let doubleFunc : PureFunc Expression := {
+    name := CoreIdent.unres "double",
+    typeArgs := [],
+    isConstr := false,
+    inputs := [(CoreIdent.unres "x", .forAll [] .int)],
+    output := .forAll [] .int,
+    body := some eb[((~Int.Add x) x)],
+    attr := #[],
+    concreteEval := none,
+    axioms := []
+  }
+  [
+    .funcDecl doubleFunc,
+    .init "y" t[int] eb[(~double #5)],
+    .assert "y_eq_10" eb[y == #10]
+  ]
+
+/--
+info: Error:
+none
+Subst Map:
+
+Expression Env:
+State:
+[(y : int) → (~double #5)]
+
+Evaluation Config:
+Eval Depth: 200
+Variable Prefix: $__
+Variable gen count: 0
+Factory Functions:
+func double :  ((x : int)) → int :=
+  ((~Int.Add x) x)
+
+
+Datatypes:
+
+Path Conditions:
+
+
+Warnings:
+[]
+Deferred Proof Obligations:
+Label: y_eq_10
+Property: assert
+Assumptions:
+Proof Obligation:
+((~double #5) == #10)
+-/
+#guard_msgs in
+#eval (evalOne ∅ ∅ testFuncDecl) |>.snd |> Env.format
+
+/--
+Test funcDecl with symbolic variable capture: function references a variable from enclosing scope
+-/
+def testFuncDeclSymbolic : List Statement :=
+  let addNFunc : PureFunc Expression := {
+    name := CoreIdent.unres "addN",
+    typeArgs := [],
+    isConstr := false,
+    inputs := [(CoreIdent.unres "x", .forAll [] .int)],
+    output := .forAll [] .int,
+    body := some eb[((~Int.Add x) n)],  -- References 'n' from outer scope
+    attr := #[],
+    concreteEval := none,
+    axioms := []
+  }
+  [
+    .init "n" t[int] eb[globalN],  -- Initialize with symbolic global
+    .funcDecl addNFunc,
+    .init "result" t[int] eb[(~addN #5)],
+    .assert "result_eq_n_plus_5" eb[result == ((~Int.Add globalN) #5)]
+  ]
+
+/--
+info: Error:
+none
+Subst Map:
+
+Expression Env:
+State:
+[(globalN : int) → globalN
+(n : int) → globalN
+(result : int) → (~addN #5)]
+
+Evaluation Config:
+Eval Depth: 200
+Variable Prefix: $__
+Variable gen count: 0
+Factory Functions:
+func addN :  ((x : int)) → int :=
+  ((~Int.Add x) n)
+
+
+Datatypes:
+
+Path Conditions:
+
+
+Warnings:
+[]
+Deferred Proof Obligations:
+Label: result_eq_n_plus_5
+Property: assert
+Assumptions:
+Proof Obligation:
+((~addN #5) == ((~Int.Add globalN) #5))
+-/
+#guard_msgs in
+#eval (evalOne
+  ((Env.init (empty_factory := true)).pushScope [("globalN", (mty[int], eb[globalN]))])
+  ∅
+  testFuncDeclSymbolic) |>.snd |> Env.format
 
 end Tests
 ---------------------------------------------------------------------

From 6b1cdc2ccc093cbf13c2293ddcf9bf122e91eaf4 Mon Sep 17 00:00:00 2001
From: Mikael Mayer <mimayere@amazon.com>
Date: Tue, 27 Jan 2026 17:12:57 -0600
Subject: [PATCH 02/12] Fix Factory_wf proof using rotate_left to reorder goals

---
 Strata/Languages/Core/Factory.lean | 38 +++++++++++++++---------------
 1 file changed, 19 insertions(+), 19 deletions(-)

diff --git a/Strata/Languages/Core/Factory.lean b/Strata/Languages/Core/Factory.lean
index 845cdc33f..68c34e1f3 100644
--- a/Strata/Languages/Core/Factory.lean
+++ b/Strata/Languages/Core/Factory.lean
@@ -565,10 +565,7 @@ set_option maxHeartbeats 4000000 in
 Wellformedness of Factory
 -/
 theorem Factory_wf :
-    FactoryWF Factory := by sorry -- TODO: Requires handling ~200+ functions including dynamically generated BV ops
-  /-
-  -- The proof needs to show LFuncWF for each function in the factory
-  -- Challenge: ExpandBVOpFuncNames generates many functions at compile time
+    FactoryWF Factory := by
   unfold Factory
   apply FactoryWF.mk
   · decide -- FactoryWF.name_nodup
@@ -583,21 +580,24 @@ theorem Factory_wf :
     repeat (
       rcases Hmem with _ | ⟨ a', Hmem ⟩
       · apply LFuncWF.mk
-        · decide -- LFuncWF.arg_nodup
+        rotate_left
         · decide -- LFuncWF.body_freevars
-        · -- LFuncWf.concreteEval_argmatch
-          simp (config := { ground := true })
-          try (
-            try unfold unOpCeval
-            try unfold binOpCeval
-            try unfold cevalIntDiv
-            try unfold cevalIntMod
-            try unfold bvUnaryOp
-            try unfold bvBinaryOp
-            try unfold bvShiftOp
-            try unfold bvBinaryPred
-            intros lf md args res
-            repeat (rcases args with _ | ⟨ args0, args ⟩ <;> try grind)))
+        rotate_left
+        · apply FuncWF.mk
+          · decide -- LFuncWF.arg_nodup
+          · -- LFuncWf.concreteEval_argmatch
+            simp (config := { ground := true })
+            try (
+              try unfold unOpCeval
+              try unfold binOpCeval
+              try unfold cevalIntDiv
+              try unfold cevalIntMod
+              try unfold bvUnaryOp
+              try unfold bvBinaryOp
+              try unfold bvShiftOp
+              try unfold bvBinaryPred
+              intros lf md args res
+              repeat (rcases args with _ | ⟨ args0, args ⟩ <;> try grind)))
     contradiction
--/
+
 end Core

From a8a4a0c12a6a6dab8d1b2390e9e86a5ad48f4b35 Mon Sep 17 00:00:00 2001
From: Mikael Mayer <mimayere@amazon.com>
Date: Tue, 27 Jan 2026 17:25:19 -0600
Subject: [PATCH 03/12] Remove unnecessary Lambda namespace opening in
 Statement.lean

---
 Strata/Languages/Core/Statement.lean |  2 +-
 pr_description.txt                   | 16 ++++++++++++++++
 2 files changed, 17 insertions(+), 1 deletion(-)
 create mode 100644 pr_description.txt

diff --git a/Strata/Languages/Core/Statement.lean b/Strata/Languages/Core/Statement.lean
index 82ebed900..6b85f0dea 100644
--- a/Strata/Languages/Core/Statement.lean
+++ b/Strata/Languages/Core/Statement.lean
@@ -15,7 +15,7 @@ import Strata.DL.Imperative.HasVars
 import Strata.DL.Lambda.LExpr
 
 namespace Core
-open Lambda Imperative
+open Imperative
 open Std (ToFormat Format format)
 ---------------------------------------------------------------------
 
diff --git a/pr_description.txt b/pr_description.txt
new file mode 100644
index 000000000..90461a54f
--- /dev/null
+++ b/pr_description.txt
@@ -0,0 +1,16 @@
+Add support for function declarations within statement blocks
+
+This PR adds the ability to declare functions as a statement `Stmt.funDecl  in Strata Core, enabling local declarations and non-recursive function definitions that can be used within procedures.
+
+## Changes
+- Implemented statement-level operations (variable analysis, substitution, type erasure) for funcDecl
+- Added type checking that converts between PureFunc and Function representations, handling type monomorphization
+- Implemented evaluation that makes function context updatable locally by adding declared functions to the factory
+- Extended all program transformations to handle funcDecl (pass-through for most, sorry for correctness proofs)
+- Added `ToFormat` instances to properly display function bodies in verification output
+
+## Testing
+Added tests in StatementEvalTests demonstrating funcDecl functionality: declaring helper functions within statement blocks and using them in subsequent statements, including symbolic variable capture from enclosing scope.
+
+## Notes
+- CallElimCorrect proof uses `sorry` for funcDecl cases - will be addressed when old variables are removed

From b8ec252b53fae22eb560d632b21a4aed86dfcd23 Mon Sep 17 00:00:00 2001
From: Mikael Mayer <mimayere@amazon.com>
Date: Tue, 27 Jan 2026 17:40:48 -0600
Subject: [PATCH 04/12] Remove unnecessary Lambda namespace opening in
 Program.lean

---
 Strata/Languages/Core/Program.lean |  1 -
 pr_description.txt                 | 16 ----------------
 2 files changed, 17 deletions(-)
 delete mode 100644 pr_description.txt

diff --git a/Strata/Languages/Core/Program.lean b/Strata/Languages/Core/Program.lean
index ae1ae4910..c19eba8e1 100644
--- a/Strata/Languages/Core/Program.lean
+++ b/Strata/Languages/Core/Program.lean
@@ -15,7 +15,6 @@ import Strata.Languages.Core.Axiom
 
 namespace Core
 
-open Lambda
 open Std (ToFormat Format format)
 open Imperative
 
diff --git a/pr_description.txt b/pr_description.txt
deleted file mode 100644
index 90461a54f..000000000
--- a/pr_description.txt
+++ /dev/null
@@ -1,16 +0,0 @@
-Add support for function declarations within statement blocks
-
-This PR adds the ability to declare functions as a statement `Stmt.funDecl  in Strata Core, enabling local declarations and non-recursive function definitions that can be used within procedures.
-
-## Changes
-- Implemented statement-level operations (variable analysis, substitution, type erasure) for funcDecl
-- Added type checking that converts between PureFunc and Function representations, handling type monomorphization
-- Implemented evaluation that makes function context updatable locally by adding declared functions to the factory
-- Extended all program transformations to handle funcDecl (pass-through for most, sorry for correctness proofs)
-- Added `ToFormat` instances to properly display function bodies in verification output
-
-## Testing
-Added tests in StatementEvalTests demonstrating funcDecl functionality: declaring helper functions within statement blocks and using them in subsequent statements, including symbolic variable capture from enclosing scope.
-
-## Notes
-- CallElimCorrect proof uses `sorry` for funcDecl cases - will be addressed when old variables are removed

From d6668828a50bb56fe1702f711b01ed1fa7748b5e Mon Sep 17 00:00:00 2001
From: Mikael Mayer <mimayere@amazon.com>
Date: Wed, 28 Jan 2026 14:10:49 -0600
Subject: [PATCH 05/12] Restore proper function body formatting by adding
 ToFormat instance for Func

- Added ToFormat for generic Func with proper constraints
- Added [ToFormat T.IDMeta] to Factory.lean section variables
- Removed unnecessary ToFormat instances from test files and Program.lean
- Removed custom Env.format function (now uses default ToFormat)
- Function bodies now display properly instead of showing <body>
---
 Strata/DL/Lambda/Factory.lean                 | 19 +++++++++++----
 Strata/Languages/Core/Env.lean                | 23 ++++++++-----------
 Strata/Languages/Core/ProcedureType.lean      | 15 ------------
 Strata/Languages/Core/Program.lean            | 14 -----------
 Strata/Transform/CallElimCorrect.lean         |  4 ++--
 StrataTest/DL/Lambda/LExprTTests.lean         | 15 ------------
 StrataTest/DL/Lambda/TypeFactoryTests.lean    | 15 ------------
 StrataTest/Languages/Core/Examples/Regex.lean |  4 ++--
 .../Languages/Core/StatementEvalTests.lean    | 22 +++++++++---------
 9 files changed, 39 insertions(+), 92 deletions(-)

diff --git a/Strata/DL/Lambda/Factory.lean b/Strata/DL/Lambda/Factory.lean
index 7da3fcdd6..f2b144ae8 100644
--- a/Strata/DL/Lambda/Factory.lean
+++ b/Strata/DL/Lambda/Factory.lean
@@ -30,7 +30,7 @@ namespace Lambda
 
 open Std (ToFormat Format format)
 
-variable {T : LExprParams} [Inhabited T.Metadata]
+variable {T : LExprParams} [Inhabited T.Metadata] [ToFormat T.IDMeta]
 
 ---------------------------------------------------------------------
 
@@ -190,19 +190,30 @@ instance LFuncWF.body_freevars_decidable {T : LExprParams} (f : LFunc T):
 instance [Inhabited T.Metadata] [Inhabited T.IDMeta] : Inhabited (LFunc T) where
   default := { name := Inhabited.default, inputs := [], output := LMonoTy.bool }
 
-instance : ToFormat (LFunc T) where
+instance {IdentT ExprT TyT MetadataT : Type} [ToFormat IdentT] [ToFormat ExprT] [ToFormat TyT] [Inhabited ExprT] : ToFormat (Func IdentT ExprT TyT MetadataT) where
   format f :=
     let attr := if f.attr.isEmpty then f!"" else f!"@[{f.attr}]{Format.line}"
     let typeArgs := if f.typeArgs.isEmpty
                     then f!""
                     else f!"∀{f.typeArgs}."
-    let type := f!"{typeArgs} ({Signature.format f.inputs}) → {f.output}"
+    -- Format inputs recursively like Signature.format
+    let rec formatInputs (inputs : List (IdentT × TyT)) : Format :=
+      match inputs with
+      | [] => f!""
+      | [(k, v)] => f!"({k} : {v})"
+      | (k, v) :: rest => f!"({k} : {v}) " ++ formatInputs rest
+    let type := f!"{typeArgs} ({formatInputs f.inputs}) → {f.output}"
     let sep := if f.body.isNone then f!";" else f!" :="
-    let body := if f.body.isNone then f!"" else f!"<body>"
+    let body := if f.body.isNone then f!"" else Std.Format.indentD f!"({f.body.get!})"
     f!"{attr}\
        func {f.name} : {type}{sep}\
        {body}"
 
+-- Provide explicit instance for LFunc to ensure proper resolution
+-- Requires ToFormat for T.IDMeta (for identifiers in expressions) and T.Metadata (for Inhabited LExpr)
+instance [ToFormat T.IDMeta] [Inhabited T.Metadata] : ToFormat (LFunc T) where
+  format := format
+
 def LFunc.type [DecidableEq T.IDMeta] (f : (LFunc T)) : Except Format LTy := do
   if !(decide f.inputs.keys.Nodup) then
     .error f!"[{f.name}] Duplicates found in the formals!\
diff --git a/Strata/Languages/Core/Env.lean b/Strata/Languages/Core/Env.lean
index b06fb848d..13a9ad912 100644
--- a/Strata/Languages/Core/Env.lean
+++ b/Strata/Languages/Core/Env.lean
@@ -170,19 +170,6 @@ def Env.init (empty_factory:=false): Env :=
     warnings := []
     deferred := ∅ }
 
--- Custom formatter for Env that uses the proper scope formatting
-def Env.format (s : Env) : Std.Format :=
-  let stateFormat := formatScopes s.exprEnv.state
-  let configFormat := (inferInstance : ToFormat (Lambda.EvalConfig CoreLParams)).format s.exprEnv.config
-  Std.format f!"Error:{Format.line}{s.error}{Format.line}\
-            Subst Map:{Format.line}{s.substMap}{Format.line}\
-            Expression Env:{Format.line}State:{Format.line}{stateFormat}{Format.line}{Format.line}\
-            Evaluation Config:{Format.line}{configFormat}{Format.line}{Format.line}{Format.line}\
-            Datatypes:{Format.line}{s.datatypes}{Format.line}\
-            Path Conditions:{Format.line}{PathConditions.format s.pathConditions}{Format.line}{Format.line}\
-            Warnings:{Format.line}{s.warnings}{Format.line}\
-            Deferred Proof Obligations:{Format.line}{s.deferred}{Format.line}"
-
 instance : EmptyCollection Env where
   emptyCollection := Env.init (empty_factory := true)
 
@@ -190,7 +177,15 @@ instance : Inhabited Env where
   default := Env.init
 
 instance : ToFormat Env where
-  format := Env.format
+  format s :=
+    let { error, program := _, substMap, exprEnv, datatypes, distinct := _, pathConditions, warnings, deferred }  := s
+    format f!"Error:{Format.line}{error}{Format.line}\
+              Subst Map:{Format.line}{substMap}{Format.line}\
+              Expression Env:{Format.line}{exprEnv}{Format.line}\
+              Datatypes:{Format.line}{datatypes}{Format.line}\
+              Path Conditions:{Format.line}{PathConditions.format pathConditions}{Format.line}{Format.line}\
+              Warnings:{Format.line}{warnings}{Format.line}\
+              Deferred Proof Obligations:{Format.line}{deferred}{Format.line}"
 
 /--
 Create a substitution map from all non-global variables to their values.
diff --git a/Strata/Languages/Core/ProcedureType.lean b/Strata/Languages/Core/ProcedureType.lean
index 9003ea9af..4cd2df305 100644
--- a/Strata/Languages/Core/ProcedureType.lean
+++ b/Strata/Languages/Core/ProcedureType.lean
@@ -18,21 +18,6 @@ namespace Core
 open Std (ToFormat Format format)
 open Imperative (MetaData)
 
-instance : ToFormat (Lambda.LFunc { Metadata := ExpressionMetadata, IDMeta := Visibility }) where
-  format f :=
-    let attr := if f.attr.isEmpty then f!"" else f!"@[{f.attr}]{Format.line}"
-    let typeArgs := if f.typeArgs.isEmpty
-                    then f!""
-                    else f!"∀{f.typeArgs}."
-    let type := f!"{typeArgs} ({Lambda.Signature.format f.inputs}) → {f.output}"
-    let sep := if f.body.isNone then f!";" else f!" :="
-    let body := match f.body with
-                | none => f!""
-                | some e => f!"{Format.line}  {format e}"
-    f!"{attr}\
-       func {f.name} : {type}{sep}\
-       {body}"
-
 namespace Procedure
 
 private def checkNoDuplicates (proc : Procedure) (sourceLoc : Format) :
diff --git a/Strata/Languages/Core/Program.lean b/Strata/Languages/Core/Program.lean
index c19eba8e1..67fe33ddd 100644
--- a/Strata/Languages/Core/Program.lean
+++ b/Strata/Languages/Core/Program.lean
@@ -24,20 +24,6 @@ instance : Inhabited TypeDecl where
 
 -- ToFormat instance for Function (which is LFunc CoreLParams)
 -- Note: ToFormat CoreLParams.Identifier is now defined in Identifiers.lean
-instance : ToFormat Function where
-  format f :=
-    let attr := if f.attr.isEmpty then f!"" else f!"@[{f.attr}]{Format.line}"
-    let typeArgs := if f.typeArgs.isEmpty
-                    then f!""
-                    else f!"∀{f.typeArgs}."
-    let type := f!"{typeArgs} ({Lambda.Signature.format f.inputs}) → {f.output}"
-    let sep := if f.body.isNone then f!";" else f!" :="
-    let body := match f.body with
-                | none => f!""
-                | some e => f!"{Format.line}  {format e}"
-    f!"{attr}\
-       func {f.name} : {type}{sep}\
-       {body}"
 
 inductive DeclKind : Type where
   | var | type | ax | distinct | proc | func
diff --git a/Strata/Transform/CallElimCorrect.lean b/Strata/Transform/CallElimCorrect.lean
index 40206305e..093b064ef 100644
--- a/Strata/Transform/CallElimCorrect.lean
+++ b/Strata/Transform/CallElimCorrect.lean
@@ -179,7 +179,7 @@ theorem callElimBlockNoExcept :
   | ite cd tb eb md => exists [.ite cd tb eb md]
   | goto l b => exists [.goto l b]
   | loop g m i b md => exists [.loop g m i b md]
-  | funcDecl _ _ => sorry  -- TODO: Add funcDecl case to CallElimCorrect proof
+  | funcDecl f md => exists [.funcDecl f md]
   | cmd c =>
     cases c with
     | cmd c' => exists [Imperative.Stmt.cmd (CmdExt.cmd c')]
@@ -3299,7 +3299,7 @@ theorem callElimStatementCorrect [LawfulBEq Expression.Expr] :
   case ite => exact ⟨σ', Inits.init InitVars.init_none, Heval⟩
   case goto => exact ⟨σ', Inits.init InitVars.init_none, Heval⟩
   case loop => exact ⟨σ', Inits.init InitVars.init_none, Heval⟩
-  case funcDecl => sorry  -- TODO: Add funcDecl case to CallElimCorrect proof
+  case funcDecl => exact ⟨σ', Inits.init InitVars.init_none, Heval⟩
   case cmd c =>
   cases c with
   | cmd c' =>
diff --git a/StrataTest/DL/Lambda/LExprTTests.lean b/StrataTest/DL/Lambda/LExprTTests.lean
index a83848311..3cf790ee8 100644
--- a/StrataTest/DL/Lambda/LExprTTests.lean
+++ b/StrataTest/DL/Lambda/LExprTTests.lean
@@ -17,21 +17,6 @@ open LTy.Syntax LExpr.SyntaxMono LExpr LMonoTy
 
 private abbrev TestParams : LExprParams := ⟨Unit, Unit⟩
 
-private instance : ToFormat (Lambda.LFunc { Metadata := Unit, IDMeta := Unit }) where
-  format f :=
-    let attr := if f.attr.isEmpty then f!"" else f!"@[{f.attr}]{Format.line}"
-    let typeArgs := if f.typeArgs.isEmpty
-                    then f!""
-                    else f!"∀{f.typeArgs}."
-    let type := f!"{typeArgs} ({Lambda.Signature.format f.inputs}) → {f.output}"
-    let sep := if f.body.isNone then f!";" else f!" :="
-    let body := match f.body with
-                | none => f!""
-                | some e => f!"{Format.line}  {format e}"
-    f!"{attr}\
-       func {f.name} : {type}{sep}\
-       {body}"
-
 private instance : Coe String TestParams.Identifier where
   coe s := Identifier.mk s ()
 
diff --git a/StrataTest/DL/Lambda/TypeFactoryTests.lean b/StrataTest/DL/Lambda/TypeFactoryTests.lean
index 59f1a3a68..0a4eba152 100644
--- a/StrataTest/DL/Lambda/TypeFactoryTests.lean
+++ b/StrataTest/DL/Lambda/TypeFactoryTests.lean
@@ -19,21 +19,6 @@ open LExpr LTy
 
 private abbrev TestParams : LExprParams := ⟨Unit, Unit⟩
 
-private instance : ToFormat (LFunc TestParams) where
-  format f :=
-    let attr := if f.attr.isEmpty then f!"" else f!"@[{f.attr}]{Format.line}"
-    let typeArgs := if f.typeArgs.isEmpty
-                    then f!""
-                    else f!"∀{f.typeArgs}."
-    let type := f!"{typeArgs} ({Signature.format f.inputs}) → {f.output}"
-    let sep := if f.body.isNone then f!";" else f!" :="
-    let body := match f.body with
-                | none => f!""
-                | some e => f!"{Format.line}  {format e}"
-    f!"{attr}\
-       func {f.name} : {type}{sep}\
-       {body}"
-
 private instance : Coe String TestParams.Identifier where
   coe s := Identifier.mk s ()
 
diff --git a/StrataTest/Languages/Core/Examples/Regex.lean b/StrataTest/Languages/Core/Examples/Regex.lean
index 4710f9446..54105ea2d 100644
--- a/StrataTest/Languages/Core/Examples/Regex.lean
+++ b/StrataTest/Languages/Core/Examples/Regex.lean
@@ -221,7 +221,7 @@ Original expression: (((~Re.Loop ((~Re.Range #a) #z)) #1) %0)
 
 Evaluated program:
 func bad_re_loop :  ((n : int)) → regex :=
-  ((((~Re.Loop : (arrow regex (arrow int (arrow int regex)))) (((~Re.Range : (arrow string (arrow string regex))) #a) #z)) #1) (n : int))
+  (((((~Re.Loop : (arrow regex (arrow int (arrow int regex)))) (((~Re.Range : (arrow string (arrow string regex))) #a) #z)) #1) (n : int)))
 (procedure main :  ((n : int)) → ())
 modifies: []
 preconditions: ⏎
@@ -241,7 +241,7 @@ Original expression: (((~Re.Loop ((~Re.Range #a) #z)) #1) %0)
 
 Evaluated program:
 func bad_re_loop :  ((n : int)) → regex :=
-  ((((~Re.Loop : (arrow regex (arrow int (arrow int regex)))) (((~Re.Range : (arrow string (arrow string regex))) #a) #z)) #1) (n : int))
+  (((((~Re.Loop : (arrow regex (arrow int (arrow int regex)))) (((~Re.Range : (arrow string (arrow string regex))) #a) #z)) #1) (n : int)))
 (procedure main :  ((n : int)) → ())
 modifies: []
 preconditions: ⏎
diff --git a/StrataTest/Languages/Core/StatementEvalTests.lean b/StrataTest/Languages/Core/StatementEvalTests.lean
index 0282d3337..0620b37b9 100644
--- a/StrataTest/Languages/Core/StatementEvalTests.lean
+++ b/StrataTest/Languages/Core/StatementEvalTests.lean
@@ -48,7 +48,7 @@ Proof Obligation:
 #guard_msgs in
 #eval (evalOne ∅ ∅ [.init "x" t[int] eb[#0],
                     .set "x" eb[#18],
-                    .assert "x_eq_18" eb[x == #18]]) |>.snd |> Env.format
+                    .assert "x_eq_18" eb[x == #18]]) |>.snd |> format
 
 /--
 info: Error:
@@ -88,7 +88,7 @@ Proof Obligation:
   ∅
   [.init "x" t[int] eb[#0],
   .set "x" eb[y],
-  .assert "x_eq_12" eb[x == #12]]) |>.snd |> Env.format
+  .assert "x_eq_12" eb[x == #12]]) |>.snd |> format
 
 /--
 info: Error:
@@ -122,7 +122,7 @@ Deferred Proof Obligations:
 #eval evalOne ∅ ∅
        [
        .init "x" t[bool] eb[x == #true]
-       ] |>.snd |> Env.format
+       ] |>.snd |> format
 
 /--
 info: Error:
@@ -182,7 +182,7 @@ Proof Obligation:
   .assert "m_2_eq_20" eb[(m #2) == #20],
   .set "m" eb[λ (if (%0 == #3) then #30 else ((m : int → int) %0))],
   .assert "m_1_eq_10" eb[(m #1) == #10]
-  ]) |>.snd |> Env.format
+  ]) |>.snd |> format
 
 /--
 info: Error:
@@ -239,7 +239,7 @@ Proof Obligation:
   .assert "m_2_eq_20" eb[(m #2) == #20],
   .set "m" eb[λ (if (%0 == #3) then #30 else (m %0))],
   .assert "m_1_eq_10" eb[(m #1) == #10]
-  ]) |>.snd |> Env.format
+  ]) |>.snd |> format
 
 
 
@@ -320,7 +320,7 @@ Proof Obligation:
 ((if (zinit == #false) then #6 else #0) == #6)
 -/
 #guard_msgs in
-#eval (evalOne ∅ ∅ prog1) |>.snd |> Env.format
+#eval (evalOne ∅ ∅ prog1) |>.snd |> format
 
 
 private def prog2 : Statements := [
@@ -375,7 +375,7 @@ Proof Obligation:
 (($__x0 : int) == #1)
 -/
 #guard_msgs in
-#eval (evalOne ∅ ∅ prog2) |>.snd |> Env.format
+#eval (evalOne ∅ ∅ prog2) |>.snd |> format
 
 /--
 Test funcDecl: declare a helper function and use it
@@ -413,7 +413,7 @@ Variable Prefix: $__
 Variable gen count: 0
 Factory Functions:
 func double :  ((x : int)) → int :=
-  ((~Int.Add x) x)
+  (((~Int.Add x) x))
 
 
 Datatypes:
@@ -431,7 +431,7 @@ Proof Obligation:
 ((~double #5) == #10)
 -/
 #guard_msgs in
-#eval (evalOne ∅ ∅ testFuncDecl) |>.snd |> Env.format
+#eval (evalOne ∅ ∅ testFuncDecl) |>.snd |> format
 
 /--
 Test funcDecl with symbolic variable capture: function references a variable from enclosing scope
@@ -472,7 +472,7 @@ Variable Prefix: $__
 Variable gen count: 0
 Factory Functions:
 func addN :  ((x : int)) → int :=
-  ((~Int.Add x) n)
+  (((~Int.Add x) n))
 
 
 Datatypes:
@@ -493,7 +493,7 @@ Proof Obligation:
 #eval (evalOne
   ((Env.init (empty_factory := true)).pushScope [("globalN", (mty[int], eb[globalN]))])
   ∅
-  testFuncDeclSymbolic) |>.snd |> Env.format
+  testFuncDeclSymbolic) |>.snd |> format
 
 end Tests
 ---------------------------------------------------------------------

From ed1f8acd777cc5fdc188d5286ae518e0b7449f47 Mon Sep 17 00:00:00 2001
From: Mikael Mayer <mimayere@amazon.com>
Date: Wed, 28 Jan 2026 14:17:39 -0600
Subject: [PATCH 06/12] Remove B3 .gitignore (moved to .git/info/exclude for
 local use)

---
 Strata/Languages/B3/.gitignore | 2 --
 1 file changed, 2 deletions(-)
 delete mode 100644 Strata/Languages/B3/.gitignore

diff --git a/Strata/Languages/B3/.gitignore b/Strata/Languages/B3/.gitignore
deleted file mode 100644
index 009e2742a..000000000
--- a/Strata/Languages/B3/.gitignore
+++ /dev/null
@@ -1,2 +0,0 @@
-# B3 reference source code (copied from ../b3 for reference only)
-b3-reference/

From c6ede80833e0197d2adc1b8b8b28011ace5c8789 Mon Sep 17 00:00:00 2001
From: Mikael Mayer <mimayere@amazon.com>
Date: Wed, 28 Jan 2026 14:23:33 -0600
Subject: [PATCH 07/12] Clean up: revert ProcedureWF.lean to main, remove
 unnecessary comment

---
 Strata/Languages/Core/ProcedureWF.lean | 1 +
 Strata/Languages/Core/Statement.lean   | 1 -
 2 files changed, 1 insertion(+), 1 deletion(-)

diff --git a/Strata/Languages/Core/ProcedureWF.lean b/Strata/Languages/Core/ProcedureWF.lean
index ba8ea590e..68ce457bb 100644
--- a/Strata/Languages/Core/ProcedureWF.lean
+++ b/Strata/Languages/Core/ProcedureWF.lean
@@ -31,6 +31,7 @@ theorem snd_values_mem {ps : ListMap CoreLabel Procedure.Check} :
 
 theorem Procedure.typeCheckWF : Procedure.typeCheck C T p pp md = Except.ok (pp', T') → WFProcedureProp p pp := by sorry
 
+
 /-
 set_option warn.sorry false in
 /--
diff --git a/Strata/Languages/Core/Statement.lean b/Strata/Languages/Core/Statement.lean
index 6b85f0dea..40da26c21 100644
--- a/Strata/Languages/Core/Statement.lean
+++ b/Strata/Languages/Core/Statement.lean
@@ -127,7 +127,6 @@ def Statement.eraseTypes (s : Statement) : Statement :=
     .loop guard measure invariant body' md
   | .goto l md => .goto l md
   | .funcDecl decl md =>
-    -- Erase types from function body and axioms
     let decl' := { decl with
       body := decl.body.map Lambda.LExpr.eraseTypes,
       axioms := decl.axioms.map Lambda.LExpr.eraseTypes }

From 62a5f704338e54d4d6b1699e7a1c439cac45b63b Mon Sep 17 00:00:00 2001
From: Mikael Mayer <mimayere@amazon.com>
Date: Wed, 28 Jan 2026 16:40:52 -0600
Subject: [PATCH 08/12] Fix merge: add missing funcDecl cases in
 ProcedureInlining and apply rotate_left fix to FactoryWF

---
 Strata/Transform/ProcedureInlining.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Strata/Transform/ProcedureInlining.lean b/Strata/Transform/ProcedureInlining.lean
index 02169d9db..e5036762e 100644
--- a/Strata/Transform/ProcedureInlining.lean
+++ b/Strata/Transform/ProcedureInlining.lean
@@ -116,6 +116,7 @@ def Statement.labels (s : Core.Statement) : List String :=
   | .goto _ _ => []
   -- No other labeled commands.
   | .cmd _ => []
+  | .funcDecl _ _ => []
   termination_by s.sizeOf
 end
 
@@ -143,6 +144,7 @@ def Statement.replaceLabels
   | .assert lbl e m => .assert (app lbl) e m
   | .cover lbl e m => .cover (app lbl) e m
   | .cmd _ => s
+  | .funcDecl _ _ => s
   termination_by s.sizeOf
 end
 

From 5f65da9f6e8e422cc19884e9c8cee989b4be64a4 Mon Sep 17 00:00:00 2001
From: Mikael Mayer <mimayere@amazon.com>
Date: Thu, 29 Jan 2026 14:35:07 -0600
Subject: [PATCH 09/12] Update funcDecl test to demonstrate variable capture
 semantics

- Modified testFuncDeclSymbolic to show functions capture variables by reference
- Function declared with n=10, then n mutated to 20, function uses n=20 at call time
- Proof obligation correctly shows result should be 25 (5+20), not 15 (5+10)
- Reverted Env.lean to main (custom scope formatting not needed)
---
 Strata/Languages/Core/Env.lean                | 33 ++++---------------
 .../Languages/Core/StatementEvalTests.lean    | 26 +++++++--------
 2 files changed, 19 insertions(+), 40 deletions(-)

diff --git a/Strata/Languages/Core/Env.lean b/Strata/Languages/Core/Env.lean
index d2bc5e7db..6d6d77db5 100644
--- a/Strata/Languages/Core/Env.lean
+++ b/Strata/Languages/Core/Env.lean
@@ -16,44 +16,25 @@ open Imperative
 instance : ToFormat ExpressionMetadata :=
   show ToFormat Unit from inferInstance
 
--- ToFormat instance for Expression.EvalEnv (which is Lambda.LState CoreLParams)
-instance : ToFormat Expression.EvalEnv := by
-  show ToFormat (Lambda.LState CoreLParams)
-  infer_instance
-
 -- ToFormat instance for Expression.Expr
 instance : ToFormat Expression.Expr := by
   show ToFormat (Lambda.LExpr CoreLParams.mono)
   infer_instance
 
--- Custom ToFormat instance for Scopes to get the desired formatting
-def formatScopeMap (m : Map CoreIdent (Option Lambda.LMonoTy × Expression.Expr)) : Std.Format :=
+-- Custom ToFormat instance for our specific Scope type to get the desired formatting
+private def formatScope (m : Map CoreIdent (Option Lambda.LMonoTy × Expression.Expr)) : Std.Format :=
   match m with
   | [] => ""
-  | [(k, (ty, v))] =>
+  | [(k, (ty, v))] => go k ty v
+  | (k, (ty, v)) :: rest =>
+    go k ty v ++ Format.line ++ formatScope rest
+  where go k ty v :=
     match ty with
     | some ty => f!"({k} : {ty}) → {v}"
     | none => f!"{k} → {v}"
-  | (k, (ty, v)) :: rest =>
-    let entry := match ty with
-      | some ty => f!"({k} : {ty}) → {v}"
-      | none => f!"{k} → {v}"
-    entry ++ Format.line ++ formatScopeMap rest
-
-def formatScopes (ms : Lambda.Scopes CoreLParams) : Std.Format :=
-  match ms with
-  | [] => ""
-  | [m] => f!"[{formatScopeMap m}]"
-  | m :: rest => f!"[{formatScopeMap m}]{Format.line}" ++ formatScopes rest
-
-@[default_instance 1000]
-instance : ToFormat (Lambda.Scopes CoreLParams) where
-  format := formatScopes
 
--- Also provide the instance for single Map for compatibility
-@[default_instance 1000]
 instance : ToFormat (Map CoreIdent (Option Lambda.LMonoTy × Expression.Expr)) where
-  format := formatScopeMap
+  format := formatScope
 
 instance : Inhabited ExpressionMetadata :=
   show Inhabited Unit from inferInstance
diff --git a/StrataTest/Languages/Core/StatementEvalTests.lean b/StrataTest/Languages/Core/StatementEvalTests.lean
index 0620b37b9..5a52f7cfd 100644
--- a/StrataTest/Languages/Core/StatementEvalTests.lean
+++ b/StrataTest/Languages/Core/StatementEvalTests.lean
@@ -434,7 +434,8 @@ Proof Obligation:
 #eval (evalOne ∅ ∅ testFuncDecl) |>.snd |> format
 
 /--
-Test funcDecl with symbolic variable capture: function references a variable from enclosing scope
+Test funcDecl with variable capture: function captures variable value at declaration time,
+not affected by subsequent mutations
 -/
 def testFuncDeclSymbolic : List Statement :=
   let addNFunc : PureFunc Expression := {
@@ -443,16 +444,17 @@ def testFuncDeclSymbolic : List Statement :=
     isConstr := false,
     inputs := [(CoreIdent.unres "x", .forAll [] .int)],
     output := .forAll [] .int,
-    body := some eb[((~Int.Add x) n)],  -- References 'n' from outer scope
+    body := some eb[((~Int.Add x) n)],  -- Captures 'n' at declaration time
     attr := #[],
     concreteEval := none,
     axioms := []
   }
   [
-    .init "n" t[int] eb[globalN],  -- Initialize with symbolic global
-    .funcDecl addNFunc,
-    .init "result" t[int] eb[(~addN #5)],
-    .assert "result_eq_n_plus_5" eb[result == ((~Int.Add globalN) #5)]
+    .init "n" t[int] eb[#10],  -- Initialize n to 10
+    .funcDecl addNFunc,  -- Function captures reference to 'n'
+    .set "n" eb[#20],  -- Mutate n to 20
+    .init "result" t[int] eb[(~addN #5)],  -- Call function
+    .assert "result_eq_25" eb[result == #25]  -- Should be 5 + 20 = 25 (uses current value of n)
   ]
 
 /--
@@ -462,8 +464,7 @@ Subst Map:
 
 Expression Env:
 State:
-[(globalN : int) → globalN
-(n : int) → globalN
+[(n : int) → #20
 (result : int) → (~addN #5)]
 
 Evaluation Config:
@@ -483,17 +484,14 @@ Path Conditions:
 Warnings:
 []
 Deferred Proof Obligations:
-Label: result_eq_n_plus_5
+Label: result_eq_25
 Property: assert
 Assumptions:
 Proof Obligation:
-((~addN #5) == ((~Int.Add globalN) #5))
+((~addN #5) == #25)
 -/
 #guard_msgs in
-#eval (evalOne
-  ((Env.init (empty_factory := true)).pushScope [("globalN", (mty[int], eb[globalN]))])
-  ∅
-  testFuncDeclSymbolic) |>.snd |> format
+#eval (evalOne ∅ ∅ testFuncDeclSymbolic) |>.snd |> format
 
 end Tests
 ---------------------------------------------------------------------

From 679759909865b92811c53b33f83098f920ad71f5 Mon Sep 17 00:00:00 2001
From: Mikael Mayer <mimayere@amazon.com>
Date: Thu, 29 Jan 2026 15:14:44 -0600
Subject: [PATCH 10/12] Fix merge: convert Format to String for EvalError.Misc

---
 Strata/Languages/Core/StatementEval.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Strata/Languages/Core/StatementEval.lean b/Strata/Languages/Core/StatementEval.lean
index 49d53b494..72099d505 100644
--- a/Strata/Languages/Core/StatementEval.lean
+++ b/Strata/Languages/Core/StatementEval.lean
@@ -419,7 +419,7 @@ def evalAuxGo (steps : Nat) (old_var_subst : SubstMap) (Ewn : EnvWithNext) (ss :
             | .ok env' => [{ Ewn with env := env' }]
             | .error e =>
               -- If adding fails, set error but continue
-              [{ Ewn with env := { Ewn.env with error := some (.Misc e) } }]
+              [{ Ewn with env := { Ewn.env with error := some (.Misc f!"{e}") } }]
 
           | .goto l md => [{ Ewn with stk := Ewn.stk.appendToTop [.goto l md], nextLabel := (some l)}]
 

From 5ceddf3e4b85f1c8c97ace7d4490d546b607d88d Mon Sep 17 00:00:00 2001
From: Mikael Mayer <mimayere@amazon.com>
Date: Thu, 29 Jan 2026 15:22:09 -0600
Subject: [PATCH 11/12] Implement value capture for funcDecl: substitute free
 variables at declaration time

- Functions now capture variable values at declaration time, not by reference
- Free variables in function body are substituted with their current values from environment
- Test demonstrates: n=10 at declaration, n=20 after mutation, function uses n=10
- Proof obligation correctly shows result is 15 (5+10), not 25 (5+20)
---
 Strata/Languages/Core/StatementEval.lean          | 15 +++++++++++----
 StrataTest/Languages/Core/StatementEvalTests.lean | 10 +++++-----
 2 files changed, 16 insertions(+), 9 deletions(-)

diff --git a/Strata/Languages/Core/StatementEval.lean b/Strata/Languages/Core/StatementEval.lean
index 72099d505..17430455c 100644
--- a/Strata/Languages/Core/StatementEval.lean
+++ b/Strata/Languages/Core/StatementEval.lean
@@ -401,16 +401,23 @@ def evalAuxGo (steps : Nat) (old_var_subst : SubstMap) (Ewn : EnvWithNext) (ss :
                     calling Core.Statement.evalAux"
 
           | .funcDecl decl _ =>
-            -- Add function to factory
-            -- Convert PureFunc Expression (with LTy) to LFunc CoreLParams (with LMonoTy)
-            -- Assumes type checking has already monomorphized the types to .forAll [] mty
+            -- Add function to factory with value capture semantics
+            -- Substitute current values of free variables into function body
             let func : Lambda.LFunc CoreLParams := {
               name := decl.name,
               typeArgs := decl.typeArgs,
               isConstr := decl.isConstr,
               inputs := decl.inputs.map (fun (id, ty) => (id, Lambda.LTy.toMonoTypeUnsafe ty)),
               output := Lambda.LTy.toMonoTypeUnsafe decl.output,
-              body := decl.body,
+              body := decl.body.map (fun e =>
+                -- Substitute free variables with their current values from the environment
+                let freeVars := Lambda.LExpr.freeVars e
+                freeVars.foldl (fun body fv =>
+                  match Ewn.env.exprEnv.state.find? fv.fst with
+                  | some (_, val) => Lambda.LExpr.substFvar body fv.fst val
+                  | none => body
+                ) e
+              ),
               attr := decl.attr,
               concreteEval := decl.concreteEval,
               axioms := decl.axioms
diff --git a/StrataTest/Languages/Core/StatementEvalTests.lean b/StrataTest/Languages/Core/StatementEvalTests.lean
index 5a52f7cfd..f3130cec5 100644
--- a/StrataTest/Languages/Core/StatementEvalTests.lean
+++ b/StrataTest/Languages/Core/StatementEvalTests.lean
@@ -451,10 +451,10 @@ def testFuncDeclSymbolic : List Statement :=
   }
   [
     .init "n" t[int] eb[#10],  -- Initialize n to 10
-    .funcDecl addNFunc,  -- Function captures reference to 'n'
+    .funcDecl addNFunc,  -- Function captures n = 10 at declaration time
     .set "n" eb[#20],  -- Mutate n to 20
     .init "result" t[int] eb[(~addN #5)],  -- Call function
-    .assert "result_eq_25" eb[result == #25]  -- Should be 5 + 20 = 25 (uses current value of n)
+    .assert "result_eq_15" eb[result == #15]  -- Result is 5 + 10 = 15 (uses captured value)
   ]
 
 /--
@@ -473,7 +473,7 @@ Variable Prefix: $__
 Variable gen count: 0
 Factory Functions:
 func addN :  ((x : int)) → int :=
-  (((~Int.Add x) n))
+  (((~Int.Add x) #10))
 
 
 Datatypes:
@@ -484,11 +484,11 @@ Path Conditions:
 Warnings:
 []
 Deferred Proof Obligations:
-Label: result_eq_25
+Label: result_eq_15
 Property: assert
 Assumptions:
 Proof Obligation:
-((~addN #5) == #25)
+((~addN #5) == #15)
 -/
 #guard_msgs in
 #eval (evalOne ∅ ∅ testFuncDeclSymbolic) |>.snd |> format

From 86f6c90491b255789db17dc4bc3c246b41b3acfb Mon Sep 17 00:00:00 2001
From: Mikael Mayer <mimayere@amazon.com>
Date: Thu, 29 Jan 2026 15:52:12 -0600
Subject: [PATCH 12/12] Fix merge: convert Format errors to DiagnosticModel in
 funcDecl type checking

---
 Strata/Languages/Core/StatementType.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Strata/Languages/Core/StatementType.lean b/Strata/Languages/Core/StatementType.lean
index d4569ac16..a60d9d9df 100644
--- a/Strata/Languages/Core/StatementType.lean
+++ b/Strata/Languages/Core/StatementType.lean
@@ -180,7 +180,7 @@ where
             concreteEval := none,  -- Can't convert concreteEval safely
             axioms := decl.axioms
           }
-          let (func', Env) ← Function.typeCheck C Env func
+          let (func', Env) ← Function.typeCheck C Env func |>.mapError DiagnosticModel.fromFormat
           -- Convert back by wrapping monotypes in trivial polytypes
           let decl' : PureFunc Expression := {
             name := func'.name,