Denotational semantics for Laurel IR with concrete evaluator and transform preservation tests

.kiro/settings/mcp.json

@@ -29,4 +29,4 @@
       ]
     }
   }
-}
+}

Strata.lean

@@ -25,6 +25,10 @@ import Strata.Languages.Core.SeqModel
 import Strata.Languages.Core.StatementSemantics
 import Strata.Languages.Core.SarifOutput
 import Strata.Languages.Laurel.LaurelToCoreTranslator
+import Strata.Languages.Laurel.LaurelSemantics
+import Strata.Languages.Laurel.LaurelConcreteEval
+import Strata.Languages.Laurel.LaurelDenote
+import Strata.Languages.Laurel.LaurelDenoteMono
 
 /- Code Transforms -/
 import Strata.Transform.CallElimCorrect

Strata/Languages/Laurel/LaurelConcreteEval.lean

@@ -0,0 +1,120 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.Languages.Laurel.LaurelDenote
+
+/-!
+# Concrete Program Evaluator for Laurel
+
+Bridges the gap between `denoteStmt` (which operates on individual statements)
+and `Laurel.Program` (which is the top-level program structure). Given a program,
+builds the required environments and calls `denoteStmt` on the `main` procedure's body.
+-/
+
+namespace Strata.Laurel
+
+/-! ## ToString for LaurelValue -/
+
+instance : ToString LaurelValue where
+  toString
+    | .vInt i => toString i
+    | .vBool b => toString b
+    | .vString s => s!"\"{s}\""
+    | .vVoid => "void"
+    | .vRef n => s!"ref({n})"
+
+/-! ## Building ProcEnv -/
+
+/-- Build a `ProcEnv` from a list of procedures. Earlier entries shadow later ones. -/
+def listToProcEnv (procs : List Procedure) : ProcEnv :=
+  fun name => procs.find? (fun p => p.name == name)
+
+/-- Build a `ProcEnv` from a `Program`, including static procedures and
+    instance procedures keyed as `"TypeName.methodName"`. -/
+def buildProcEnv (prog : Program) : ProcEnv :=
+  let statics := prog.staticProcedures
+  let instanceProcs := prog.types.foldl (fun acc td =>
+    match td with
+    | .Composite ct =>
+      ct.instanceProcedures.map (fun p =>
+        { p with name := mkId (ct.name.text ++ "." ++ p.name.text) }) ++ acc
+    | _ => acc) []
+  listToProcEnv (instanceProcs ++ statics)
+
+/-! ## Building Initial Store -/
+
+/-- Build an initial store from static fields, all initialized to `vVoid`. -/
+def buildInitialStore (prog : Program) : LaurelStore :=
+  let fields := prog.staticFields
+  fields.foldl (fun σ f => fun x => if x == f.name.text then some .vVoid else σ x)
+    (fun _ => none)
+
+/-! ## Default Expression Evaluator -/
+
+/-- A `LaurelEval` that handles identifiers and literals.
+    Specification constructs return `none`. -/
+def defaultEval : LaurelEval := fun σ e =>
+  match e with
+  | .Identifier name => σ name.text
+  | .LiteralInt i => some (.vInt i)
+  | .LiteralBool b => some (.vBool b)
+  | .LiteralString s => some (.vString s)
+  | _ => none
+
+/-! ## Core Evaluation -/
+
+/-- Evaluate a `Program` by finding and running its `main` procedure.
+    Returns `none` if there is no `main` or it has no body. -/
+def evalProgram (prog : Program) (fuel : Nat := 10000)
+    : Option (Outcome × LaurelStore × LaurelHeap) :=
+  let π := buildProcEnv prog
+  match prog.staticProcedures.find? (fun p => p.name.text == "main") with
+  | none => none
+  | some mainProc =>
+    match getBody mainProc with
+    | none => none
+    | some body =>
+      let σ₀ := buildInitialStore prog
+      let h₀ : LaurelHeap := fun _ => none
+      denoteStmt defaultEval π fuel h₀ σ₀ body.val
+
+/-! ## User-Friendly Result Type -/
+
+inductive EvalResult where
+  | success (value : LaurelValue) (store : LaurelStore) (heap : LaurelHeap)
+  | returned (value : Option LaurelValue) (store : LaurelStore) (heap : LaurelHeap)
+  | noMain
+  | noBody
+  | stuck (msg : String)
+  | fuelExhausted
+  deriving Inhabited
+
+instance : ToString EvalResult where
+  toString
+    | .success v _ _ => s!"success: {v}"
+    | .returned (some v) _ _ => s!"returned: {v}"
+    | .returned none _ _ => "returned: void"
+    | .noMain => "error: no 'main' procedure found"
+    | .noBody => "error: 'main' has no body"
+    | .stuck msg => s!"stuck: {msg}"
+    | .fuelExhausted => "error: fuel exhausted"
+
+/-- Run a program and classify the result. Delegates to `evalProgram` for
+    the core evaluation, preserving the `noMain` / `noBody` distinction. -/
+def runProgram (prog : Program) (fuel : Nat := 10000) : EvalResult :=
+  match prog.staticProcedures.find? (fun p => p.name.text == "main") with
+  | none => .noMain
+  | some mainProc =>
+    match getBody mainProc with
+    | none => .noBody
+    | some _ =>
+      match evalProgram prog fuel with
+      | some (.normal v, σ, h) => .success v σ h
+      | some (.ret rv, σ, h) => .returned rv σ h
+      | some (.exit label, _, _) => .stuck s!"uncaught exit '{label}'"
+      | none => .fuelExhausted
+
+end Strata.Laurel