diff --git a/.kiro/settings/mcp.json b/.kiro/settings/mcp.json index 29a35b076..9b5672ba3 100644 --- a/.kiro/settings/mcp.json +++ b/.kiro/settings/mcp.json @@ -29,4 +29,4 @@ ] } } -} \ No newline at end of file +} diff --git a/Strata.lean b/Strata.lean index e5c0a108b..07b90064e 100644 --- a/Strata.lean +++ b/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.LaurelInterpreter +import Strata.Languages.Laurel.LaurelInterpreterMono /- Code Transforms -/ import Strata.Transform.CallElimCorrect diff --git a/Strata/Languages/Laurel/LaurelConcreteEval.lean b/Strata/Languages/Laurel/LaurelConcreteEval.lean new file mode 100644 index 000000000..d8da7c910 --- /dev/null +++ b/Strata/Languages/Laurel/LaurelConcreteEval.lean @@ -0,0 +1,122 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Languages.Laurel.LaurelInterpreter + +/-! +# Concrete Program Evaluator for Laurel + +Bridges the gap between `interpStmt` (which operates on individual statements) +and `Laurel.Program` (which is the top-level program structure). Given a program, +builds the required environments and calls `interpStmt` on the `main` procedure's body. + +See `LaurelSemantics.lean` for the module layering rationale. +-/ + +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 acc f => fun x => if x == f.name.text then some .vVoid else acc x) + (fun _ => none) + +/-! ## Default Expression Evaluator -/ + +/-- A `LaurelEval` that handles identifiers and literals. + Specification constructs return `none`. -/ +def defaultEval : LaurelEval := fun st expr => + match expr with + | .Identifier name => st 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 procEnv := 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 initStore := buildInitialStore prog + let initHeap : LaurelHeap := fun _ => none + interpStmt defaultEval procEnv fuel initHeap initStore 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, st, hp) => .success v st hp + | some (.ret rv, st, hp) => .returned rv st hp + | some (.exit label, _, _) => .stuck s!"uncaught exit '{label}'" + | none => .fuelExhausted + +end Strata.Laurel diff --git a/Strata/Languages/Laurel/LaurelInterpreter.lean b/Strata/Languages/Laurel/LaurelInterpreter.lean new file mode 100644 index 000000000..c0bf31614 --- /dev/null +++ b/Strata/Languages/Laurel/LaurelInterpreter.lean @@ -0,0 +1,420 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Languages.Laurel.LaurelSemantics + +/-! +# Fuel-Based Interpreter for Laurel IR + +A computable interpreter mirroring the relational semantics in +`LaurelSemantics.lean` (Option A from the design document +`docs/designs/denotational-semantics-for-laurel-as-an-interprete.md`). + +## Design + +Three mutually recursive functions with a `fuel : Nat` parameter +decremented on every recursive call. Returns `none` on fuel exhaustion +or stuck states. Reuses existing `Outcome`, `LaurelValue`, `LaurelStore`, +`LaurelHeap` types unchanged. + +## Delegation via `δ : LaurelEval` + +The `δ` parameter is a callback that lets callers plug in custom handling +for constructs the interpreter cannot evaluate natively (quantifiers, +specification constructs like `Old`, `Fresh`, `Assigned`, `ContractOf`). +The default `δ` (`defaultEval` in `LaurelConcreteEval.lean`) returns `none` +for all of these, which is equivalent to "stuck / not implemented". +Test harnesses can provide richer `δ` implementations. + +## Intentionally Omitted Constructs + +`Abstract`, `All`, `Hole` return `none`, matching the relational semantics +(which gets stuck on these). +-/ + +namespace Strata.Laurel + +/-! ## Computable Store/Heap Helpers -/ + +/-- Update an existing variable in the store. Returns `none` if the variable is not present. -/ +def updateStore (store : LaurelStore) (x : Identifier) (v : LaurelValue) : Option LaurelStore := + match store x.text with + | some _ => some (fun y => if y == x.text then some v else store y) + | none => none + +/-- Initialize a new variable in the store. Returns `none` if the variable already exists. -/ +def initStore (store : LaurelStore) (x : Identifier) (v : LaurelValue) : Option LaurelStore := + match store x.text with + | none => some (fun y => if y == x.text then some v else store y) + | some _ => none + +/-- Upper bound on the address range searched by `findSmallestFree` and `allocHeap`. -/ +def heapSearchBound : Nat := 10000 + +/-- Find the smallest free address in the heap, searching up to `bound` addresses from `n`. -/ +def findSmallestFree (heap : LaurelHeap) (n : Nat) (bound : Nat := heapSearchBound) : Nat := + match bound with + | 0 => n + | bound + 1 => + match heap n with + | some _ => findSmallestFree heap (n + 1) bound + | none => n + +/-- Allocate a new object on the heap with the given type name. +Returns `none` when the heap is full (all addresses in the search range are occupied). -/ +def allocHeap (heap : LaurelHeap) (typeName : String) : Option (Nat × LaurelHeap) := + let addr := findSmallestFree heap 0 + match heap addr with + | none => some (addr, fun a => if a == addr then some (typeName, fun _ => none) else heap a) + | some _ => none + +/-- Write a value to a field of a heap object. Returns `none` if the address is not allocated. -/ +def heapFieldWrite' (heap : LaurelHeap) (addr : Nat) (field : String) (v : LaurelValue) + : Option LaurelHeap := + match heap addr with + | some (tag, fields) => + some (fun a => if a == addr then some (tag, fun f => if f == field then some v else fields f) else heap a) + | none => none + +/-! ## Interpreter -/ + +mutual +/-- Evaluate a single statement/expression. -/ +def interpStmt (δ : LaurelEval) (π : ProcEnv) (fuel : Nat) + (heap : LaurelHeap) (store : LaurelStore) (stmt : StmtExpr) + : Option (Outcome × LaurelStore × LaurelHeap) := + match fuel with + | 0 => none + | fuel + 1 => + match stmt with + -- Literals + | .LiteralInt i => some (.normal (.vInt i), store, heap) + | .LiteralBool b => some (.normal (.vBool b), store, heap) + | .LiteralString s => some (.normal (.vString s), store, heap) + | .LiteralDecimal _ => none -- no runtime representation for decimals + + -- Variables + | .Identifier name => + match store name.text with + | some v => some (.normal v, store, heap) + | none => none + + -- Short-circuit Primitive Operations + | .PrimitiveOp .AndThen [a, b] => + match interpStmt δ π fuel heap store a.val with + | some (.normal (.vBool true), σ₁, h₁) => + interpStmt δ π fuel h₁ σ₁ b.val + | some (.normal (.vBool false), σ₁, h₁) => + some (.normal (.vBool false), σ₁, h₁) + | _ => none + + | .PrimitiveOp .OrElse [a, b] => + match interpStmt δ π fuel heap store a.val with + | some (.normal (.vBool true), σ₁, h₁) => + some (.normal (.vBool true), σ₁, h₁) + | some (.normal (.vBool false), σ₁, h₁) => + interpStmt δ π fuel h₁ σ₁ b.val + | _ => none + + | .PrimitiveOp .Implies [a, b] => + match interpStmt δ π fuel heap store a.val with + | some (.normal (.vBool false), σ₁, h₁) => + some (.normal (.vBool true), σ₁, h₁) + | some (.normal (.vBool true), σ₁, h₁) => + interpStmt δ π fuel h₁ σ₁ b.val + | _ => none + + -- Eager Primitive Operations + | .PrimitiveOp op args => + match interpArgs δ π fuel heap store args with + | some (vals, store', h') => + match evalPrimOp op vals with + | some result => some (.normal result, store', h') + | none => none + | none => none + + -- Control Flow + | .IfThenElse c thenBr (some elseBr) => + match interpStmt δ π fuel heap store c.val with + | some (.normal (.vBool true), σ₁, h₁) => interpStmt δ π fuel h₁ σ₁ thenBr.val + | some (.normal (.vBool false), σ₁, h₁) => interpStmt δ π fuel h₁ σ₁ elseBr.val + | _ => none + + | .IfThenElse c thenBr none => + match interpStmt δ π fuel heap store c.val with + | some (.normal (.vBool true), σ₁, h₁) => interpStmt δ π fuel h₁ σ₁ thenBr.val + | some (.normal (.vBool false), σ₁, h₁) => some (.normal .vVoid, σ₁, h₁) + | _ => none + + | .Block stmts label => + match interpBlock δ π fuel heap store stmts with + | some (outcome, store', h') => some (catchExit label outcome, store', h') + | none => none + + | .Exit target => some (.exit target, store, heap) + + | .Return (some val) => + match interpStmt δ π fuel heap store val.val with + | some (.normal v, store', h') => some (.ret (some v), store', h') + | _ => none + + | .Return none => some (.ret none, store, heap) + + -- While Loop + | .While c invs dec body => + match interpStmt δ π fuel heap store c.val with + | some (.normal (.vBool true), σ₁, h₁) => + match interpStmt δ π fuel h₁ σ₁ body.val with + | some (.normal _, σ₂, h₂) => + interpStmt δ π fuel h₂ σ₂ (.While c invs dec body) + | some (.exit label, σ₂, h₂) => some (.exit label, σ₂, h₂) + | some (.ret rv, σ₂, h₂) => some (.ret rv, σ₂, h₂) + | none => none + | some (.normal (.vBool false), σ₁, h₁) => some (.normal .vVoid, σ₁, h₁) + | _ => none + + -- Assignments + | .Assign [⟨.Identifier name, _⟩] value => + match interpStmt δ π fuel heap store value.val with + | some (.normal v, σ₁, h₁) => + match σ₁ name.text with + | some _ => + match updateStore σ₁ name v with + | some σ₂ => some (.normal v, σ₂, h₁) + | none => none + | none => none + | _ => none + + -- Field Assignment + | .Assign [⟨.FieldSelect target fieldName, _⟩] value => + match interpStmt δ π fuel heap store target.val with + | some (.normal (.vRef addr), σ₁, h₁) => + match interpStmt δ π fuel h₁ σ₁ value.val with + | some (.normal v, σ₂, h₂) => + match heapFieldWrite' h₂ addr fieldName.text v with + | some h₃ => some (.normal v, σ₂, h₃) + | none => none + | _ => none + | _ => none + + | .Assign _ _ => none -- multi-target not supported + + | .LocalVariable name _ty (some init) => + match interpStmt δ π fuel heap store init.val with + | some (.normal v, σ₁, h₁) => + match initStore σ₁ name v with + | some σ₂ => some (.normal .vVoid, σ₂, h₁) + | none => none + | _ => none + + | .LocalVariable name _ty none => + match initStore store name .vVoid with + | some store' => some (.normal .vVoid, store', heap) + | none => none + + -- Verification Constructs + -- Assert/assume conditions must be pure (no side effects on store or heap). + -- Runtime compilation may erase these constructs, so their bodies must not + -- have observable effects. We enforce this by discarding the post-condition + -- store/heap and returning the originals. A condition with side effects will + -- appear to have no effect, which is the correct semantics for erasable + -- constructs. The relational semantics separately requires purity as a + -- well-formedness condition on programs. + -- TODO: Enriching Outcome with DiagnosticModel would allow reporting + -- which assertion failed and where, rather than just returning none. + -- TODO: To implement `Old`, thread a pre-state snapshot captured at + -- procedure entry through the interpreter. + | .Assert c => + match interpStmt δ π fuel heap store c.val with + | some (.normal (.vBool true), _, _) => some (.normal .vVoid, store, heap) + | _ => none + + | .Assume c => + match interpStmt δ π fuel heap store c.val with + | some (.normal (.vBool true), _, _) => some (.normal .vVoid, store, heap) + | _ => none + + -- Static Calls + | .StaticCall callee args => + match π callee with + | some proc => + match interpArgs δ π fuel heap store args with + | some (vals, σ₁, h₁) => + match bindParams proc.inputs vals with + | some σBound => + match getBody proc with + | some body => + match interpStmt δ π fuel h₁ σBound body.val with + | some (.normal v, _, h') => some (.normal v, σ₁, h') + | some (.ret (some v), _, h') => some (.normal v, σ₁, h') + | some (.ret none, _, h') => some (.normal .vVoid, σ₁, h') + | _ => none + | none => none + | none => none + | none => none + | none => none + + -- OO Features + | .New typeName => + match allocHeap heap typeName.text with + | some (addr, h') => some (.normal (.vRef addr), store, h') + | none => none + + | .FieldSelect target fieldName => + match interpStmt δ π fuel heap store target.val with + | some (.normal (.vRef addr), σ₁, h₁) => + match heapFieldRead h₁ addr fieldName.text with + | some v => some (.normal v, σ₁, h₁) + | none => none + | _ => none + + | .PureFieldUpdate target fieldName newVal => + match interpStmt δ π fuel heap store target.val with + | some (.normal (.vRef addr), σ₁, h₁) => + match interpStmt δ π fuel h₁ σ₁ newVal.val with + | some (.normal v, σ₂, h₂) => + match heapFieldWrite' h₂ addr fieldName.text v with + | some h₃ => some (.normal (.vRef addr), σ₂, h₃) + | none => none + | _ => none + | _ => none + + | .ReferenceEquals lhs rhs => + match interpStmt δ π fuel heap store lhs.val with + | some (.normal (.vRef a), σ₁, h₁) => + match interpStmt δ π fuel h₁ σ₁ rhs.val with + | some (.normal (.vRef b), σ₂, h₂) => + some (.normal (.vBool (a == b)), σ₂, h₂) + | _ => none + | _ => none + + | .InstanceCall target callee args => + match interpStmt δ π fuel heap store target.val with + | some (.normal (.vRef addr), σ₁, h₁) => + match h₁ addr with + | some (typeName, _) => + match π (↑(typeName ++ "." ++ callee.text)) with + | some proc => + match interpArgs δ π fuel h₁ σ₁ args with + | some (vals, σ₂, h₂) => + match bindParams proc.inputs ((.vRef addr) :: vals) with + | some σBound => + match getBody proc with + | some body => + match interpStmt δ π fuel h₂ σBound body.val with + | some (.normal v, _, h₃) => some (.normal v, σ₂, h₃) + | some (.ret (some v), _, h₃) => some (.normal v, σ₂, h₃) + | some (.ret none, _, h₃) => some (.normal .vVoid, σ₂, h₃) + | _ => none + | none => none + | none => none + | none => none + | none => none + | none => none + | _ => none + + | .This => + match store "this" with + | some v => some (.normal v, store, heap) + | none => none + + -- Type Operations + | .IsType target ty => + match interpStmt δ π fuel heap store target.val with + | some (.normal (.vRef addr), σ₁, h₁) => + match h₁ addr with + | some (actualType, _) => + some (.normal (.vBool (actualType == ty.val.typeName)), σ₁, h₁) + | none => none + | _ => none + + | .AsType target _ty => + match interpStmt δ π fuel heap store target.val with + | some (.normal v, σ₁, h₁) => some (.normal v, σ₁, h₁) + | _ => none + + -- Quantifiers (delegated to δ) + -- TODO: Consider adding a `typeValues : LaurelType → Option (List LaurelValue)` + -- field to δ that enumerates values for finite types (bool, bounded ints), + -- enabling concrete evaluation of Forall/Exists over enumerable domains. + | .Forall name ty body => + match δ store (.Forall name ty body) with + | some v => some (.normal v, store, heap) + | none => none + + | .Exists name ty body => + match δ store (.Exists name ty body) with + | some v => some (.normal v, store, heap) + | none => none + + -- Specification Constructs (delegated to δ) + -- TODO: Implementing Old requires threading a pre-state snapshot + -- (store + heap) captured at procedure entry through the interpreter. + | .Old val => + match δ store (.Old val) with + | some v => some (.normal v, store, heap) + | none => none + + | .Fresh val => + match δ store (.Fresh val) with + | some v => some (.normal v, store, heap) + | none => none + + | .Assigned name => + match δ store (.Assigned name) with + | some v => some (.normal v, store, heap) + | none => none + + | .ProveBy value _proof => + interpStmt δ π fuel heap store value.val + + | .ContractOf ct func => + match δ store (.ContractOf ct func) with + | some v => some (.normal v, store, heap) + | none => none + + -- Intentionally omitted + | .Abstract => none + | .All => none + | .Hole _ _ => none + +/-- Evaluate a block (list of statements). -/ +def interpBlock (δ : LaurelEval) (π : ProcEnv) (fuel : Nat) + (heap : LaurelHeap) (store : LaurelStore) (stmts : List StmtExprMd) + : Option (Outcome × LaurelStore × LaurelHeap) := + match fuel with + | 0 => none + | fuel + 1 => + match stmts with + | [] => some (.normal .vVoid, store, heap) + | [s] => + interpStmt δ π fuel heap store s.val + | s :: rest => + match interpStmt δ π fuel heap store s.val with + | some (.normal _, σ₁, h₁) => interpBlock δ π fuel h₁ σ₁ rest + | some (.exit label, σ₁, h₁) => some (.exit label, σ₁, h₁) + | some (.ret rv, σ₁, h₁) => some (.ret rv, σ₁, h₁) + | none => none + +/-- Evaluate a list of arguments left-to-right, threading heap and store. -/ +def interpArgs (δ : LaurelEval) (π : ProcEnv) (fuel : Nat) + (heap : LaurelHeap) (store : LaurelStore) (args : List StmtExprMd) + : Option (List LaurelValue × LaurelStore × LaurelHeap) := + match fuel with + | 0 => none + | fuel + 1 => + match args with + | [] => some ([], store, heap) + | e :: es => + match interpStmt δ π fuel heap store e.val with + | some (.normal v, σ₁, h₁) => + match interpArgs δ π fuel h₁ σ₁ es with + | some (vs, σ₂, h₂) => some (v :: vs, σ₂, h₂) + | none => none + | _ => none +end + +end Strata.Laurel diff --git a/Strata/Languages/Laurel/LaurelInterpreterMono.lean b/Strata/Languages/Laurel/LaurelInterpreterMono.lean new file mode 100644 index 000000000..a4bd620e7 --- /dev/null +++ b/Strata/Languages/Laurel/LaurelInterpreterMono.lean @@ -0,0 +1,577 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Languages.Laurel.LaurelInterpreter + +/-! +# Fuel Monotonicity for the Laurel Interpreter + +If the interpreter succeeds with fuel `fuel₁`, it succeeds with any +`fuel₂ ≥ fuel₁` giving the same result. +-/ + +namespace Strata.Laurel + +set_option maxHeartbeats 3200000 in +set_option maxRecDepth 4096 in +mutual +theorem interpStmt_fuel_mono + {δ : LaurelEval} {π : ProcEnv} {fuel₁ fuel₂ : Nat} + {heap : LaurelHeap} {store : LaurelStore} {s : StmtExpr} + {r : Outcome × LaurelStore × LaurelHeap} + (hle : fuel₁ ≤ fuel₂) + (heval : interpStmt δ π fuel₁ heap store s = some r) : + interpStmt δ π fuel₂ heap store s = some r := by + match fuel₁, fuel₂ with + | 0, _ => simp [interpStmt] at heval + | _ + 1, 0 => omega + | n + 1, m + 1 => + have hle' : n ≤ m := by omega + -- Both sides reduce to `match s with ...` using fuel n (resp. m) for sub-calls + unfold interpStmt at heval ⊢ + cases s with + | LiteralInt => exact heval + | LiteralBool => exact heval + | LiteralString => exact heval + | LiteralDecimal => exact heval + | Identifier name => exact heval + -- TODO: The AndThen/OrElse/Implies cases below share nearly identical structure + -- (~43 lines each). Consider extracting a shared tactic or private lemma that + -- handles the common pattern: case-split on first arg result, apply IH on the + -- recursive branch, discharge impossible cases. This would reduce ~130 lines to ~50. + | PrimitiveOp op args => + cases op with + | AndThen => + cases args with + | cons a tail => + cases tail with + | cons b tail₂ => + cases tail₂ with + | nil => + match ha : interpStmt δ π n heap store a.val with + | some (.normal (.vBool true), σ₁, h₁) => + have := interpStmt_fuel_mono hle' ha + simp [ha] at heval; simp [this] + exact interpStmt_fuel_mono hle' heval + | some (.normal (.vBool false), σ₁, h₁) => + have := interpStmt_fuel_mono hle' ha + simp [ha] at heval; simp [this]; exact heval + | some (.normal (.vInt _), _, _) => simp [ha] at heval + | some (.normal (.vString _), _, _) => simp [ha] at heval + | some (.normal .vVoid, _, _) => simp [ha] at heval + | some (.normal (.vRef _), _, _) => simp [ha] at heval + | some (.exit _, _, _) => simp [ha] at heval + | some (.ret _, _, _) => simp [ha] at heval + | none => simp [ha] at heval + | cons c rest => + match hargs : interpArgs δ π n heap store (a :: b :: c :: rest) with + | some (vals, store', h') => + have := interpArgs_fuel_mono hle' hargs + simp [hargs] at heval; simp [this]; exact heval + | none => simp [hargs] at heval + | nil => + match hargs : interpArgs δ π n heap store [a] with + | some (vals, store', h') => + have := interpArgs_fuel_mono hle' hargs + simp [hargs] at heval; simp [this]; exact heval + | none => simp [hargs] at heval + | nil => + match hargs : interpArgs δ π n heap store ([] : List StmtExprMd) with + | some (vals, store', h') => + have := interpArgs_fuel_mono hle' hargs + simp [hargs] at heval; simp [this]; exact heval + | none => simp [hargs] at heval + | OrElse => + cases args with + | cons a tail => + cases tail with + | cons b tail₂ => + cases tail₂ with + | nil => + match ha : interpStmt δ π n heap store a.val with + | some (.normal (.vBool true), σ₁, h₁) => + have := interpStmt_fuel_mono hle' ha + simp [ha] at heval; simp [this]; exact heval + | some (.normal (.vBool false), σ₁, h₁) => + have := interpStmt_fuel_mono hle' ha + simp [ha] at heval; simp [this] + exact interpStmt_fuel_mono hle' heval + | some (.normal (.vInt _), _, _) => simp [ha] at heval + | some (.normal (.vString _), _, _) => simp [ha] at heval + | some (.normal .vVoid, _, _) => simp [ha] at heval + | some (.normal (.vRef _), _, _) => simp [ha] at heval + | some (.exit _, _, _) => simp [ha] at heval + | some (.ret _, _, _) => simp [ha] at heval + | none => simp [ha] at heval + | cons c rest => + match hargs : interpArgs δ π n heap store (a :: b :: c :: rest) with + | some (vals, store', h') => + have := interpArgs_fuel_mono hle' hargs + simp [hargs] at heval; simp [this]; exact heval + | none => simp [hargs] at heval + | nil => + match hargs : interpArgs δ π n heap store [a] with + | some (vals, store', h') => + have := interpArgs_fuel_mono hle' hargs + simp [hargs] at heval; simp [this]; exact heval + | none => simp [hargs] at heval + | nil => + match hargs : interpArgs δ π n heap store ([] : List StmtExprMd) with + | some (vals, store', h') => + have := interpArgs_fuel_mono hle' hargs + simp [hargs] at heval; simp [this]; exact heval + | none => simp [hargs] at heval + | Implies => + cases args with + | cons a tail => + cases tail with + | cons b tail₂ => + cases tail₂ with + | nil => + match ha : interpStmt δ π n heap store a.val with + | some (.normal (.vBool false), σ₁, h₁) => + have := interpStmt_fuel_mono hle' ha + simp [ha] at heval; simp [this]; exact heval + | some (.normal (.vBool true), σ₁, h₁) => + have := interpStmt_fuel_mono hle' ha + simp [ha] at heval; simp [this] + exact interpStmt_fuel_mono hle' heval + | some (.normal (.vInt _), _, _) => simp [ha] at heval + | some (.normal (.vString _), _, _) => simp [ha] at heval + | some (.normal .vVoid, _, _) => simp [ha] at heval + | some (.normal (.vRef _), _, _) => simp [ha] at heval + | some (.exit _, _, _) => simp [ha] at heval + | some (.ret _, _, _) => simp [ha] at heval + | none => simp [ha] at heval + | cons c rest => + match hargs : interpArgs δ π n heap store (a :: b :: c :: rest) with + | some (vals, store', h') => + have := interpArgs_fuel_mono hle' hargs + simp [hargs] at heval; simp [this]; exact heval + | none => simp [hargs] at heval + | nil => + match hargs : interpArgs δ π n heap store [a] with + | some (vals, store', h') => + have := interpArgs_fuel_mono hle' hargs + simp [hargs] at heval; simp [this]; exact heval + | none => simp [hargs] at heval + | nil => + match hargs : interpArgs δ π n heap store ([] : List StmtExprMd) with + | some (vals, store', h') => + have := interpArgs_fuel_mono hle' hargs + simp [hargs] at heval; simp [this]; exact heval + | none => simp [hargs] at heval + | _ => + match hargs : interpArgs δ π n heap store args with + | some (vals, store', h') => + have := interpArgs_fuel_mono hle' hargs + simp [hargs] at heval; simp [this]; exact heval + | none => simp [hargs] at heval + | IfThenElse c thenBr elseBr => + cases elseBr with + | some elseBr => + match hc : interpStmt δ π n heap store c.val with + | some (.normal (.vBool true), σ₁, h₁) => + have := interpStmt_fuel_mono hle' hc + simp [hc] at heval; simp [this] + exact interpStmt_fuel_mono hle' heval + | some (.normal (.vBool false), σ₁, h₁) => + have := interpStmt_fuel_mono hle' hc + simp [hc] at heval; simp [this] + exact interpStmt_fuel_mono hle' heval + | some (.normal (.vInt _), _, _) => simp [hc] at heval + | some (.normal (.vString _), _, _) => simp [hc] at heval + | some (.normal .vVoid, _, _) => simp [hc] at heval + | some (.normal (.vRef _), _, _) => simp [hc] at heval + | some (.exit _, _, _) => simp [hc] at heval + | some (.ret _, _, _) => simp [hc] at heval + | none => simp [hc] at heval + | none => + match hc : interpStmt δ π n heap store c.val with + | some (.normal (.vBool true), σ₁, h₁) => + have := interpStmt_fuel_mono hle' hc + simp [hc] at heval; simp [this] + exact interpStmt_fuel_mono hle' heval + | some (.normal (.vBool false), σ₁, h₁) => + have := interpStmt_fuel_mono hle' hc + simp [hc] at heval; simp [this]; exact heval + | some (.normal (.vInt _), _, _) => simp [hc] at heval + | some (.normal (.vString _), _, _) => simp [hc] at heval + | some (.normal .vVoid, _, _) => simp [hc] at heval + | some (.normal (.vRef _), _, _) => simp [hc] at heval + | some (.exit _, _, _) => simp [hc] at heval + | some (.ret _, _, _) => simp [hc] at heval + | none => simp [hc] at heval + | Block stmts label => + match hb : interpBlock δ π n heap store stmts with + | some (outcome, store', h') => + have := interpBlock_fuel_mono hle' hb + simp [hb] at heval; simp [this]; exact heval + | none => simp [hb] at heval + | Exit => exact heval + | Return val => + cases val with + | some val => + match hv : interpStmt δ π n heap store val.val with + | some (.normal v, store', h') => + have := interpStmt_fuel_mono hle' hv + simp [hv] at heval; simp [this]; exact heval + | some (.exit _, _, _) => simp [hv] at heval + | some (.ret _, _, _) => simp [hv] at heval + | none => simp [hv] at heval + | none => exact heval + | While c invs dec body => + match hc : interpStmt δ π n heap store c.val with + | some (.normal (.vBool true), σ₁, h₁) => + have hcm := interpStmt_fuel_mono hle' hc + simp [hc] at heval; simp [hcm] + match hbody : interpStmt δ π n h₁ σ₁ body.val with + | some (.normal v, σ₂, h₂) => + have := interpStmt_fuel_mono hle' hbody + simp [hbody] at heval; simp [this] + exact interpStmt_fuel_mono hle' heval + | some (.exit label, σ₂, h₂) => + have := interpStmt_fuel_mono hle' hbody + simp [hbody] at heval; simp [this]; exact heval + | some (.ret rv, σ₂, h₂) => + have := interpStmt_fuel_mono hle' hbody + simp [hbody] at heval; simp [this]; exact heval + | none => simp [hbody] at heval + | some (.normal (.vBool false), σ₁, h₁) => + have := interpStmt_fuel_mono hle' hc + simp [hc] at heval; simp [this]; exact heval + | some (.normal (.vInt _), _, _) => simp [hc] at heval + | some (.normal (.vString _), _, _) => simp [hc] at heval + | some (.normal .vVoid, _, _) => simp [hc] at heval + | some (.normal (.vRef _), _, _) => simp [hc] at heval + | some (.exit _, _, _) => simp [hc] at heval + | some (.ret _, _, _) => simp [hc] at heval + | none => simp [hc] at heval + | Assign targets value => + match targets with + | [⟨.Identifier name, _⟩] => + match hv : interpStmt δ π n heap store value.val with + | some (.normal v, σ₁, h₁) => + have := interpStmt_fuel_mono hle' hv + simp [hv] at heval; simp [this]; exact heval + | some (.exit _, _, _) => simp [hv] at heval + | some (.ret _, _, _) => simp [hv] at heval + | none => simp [hv] at heval + | [⟨.FieldSelect target fieldName, _⟩] => + match ht : interpStmt δ π n heap store target.val with + | some (.normal (.vRef addr), σ₁, h₁) => + have htm := interpStmt_fuel_mono hle' ht + simp [ht] at heval; simp [htm] + match hv : interpStmt δ π n h₁ σ₁ value.val with + | some (.normal v, σ₂, h₂) => + have := interpStmt_fuel_mono hle' hv + simp [hv] at heval; simp [this]; exact heval + | some (.exit _, _, _) => simp [hv] at heval + | some (.ret _, _, _) => simp [hv] at heval + | none => simp [hv] at heval + | some (.normal (.vInt _), _, _) => simp [ht] at heval + | some (.normal (.vBool _), _, _) => simp [ht] at heval + | some (.normal (.vString _), _, _) => simp [ht] at heval + | some (.normal .vVoid, _, _) => simp [ht] at heval + | some (.exit _, _, _) => simp [ht] at heval + | some (.ret _, _, _) => simp [ht] at heval + | none => simp [ht] at heval + | [] => simp at heval + | [⟨.LiteralInt _, _⟩] => simp at heval + | [⟨.LiteralBool _, _⟩] => simp at heval + | [⟨.LiteralString _, _⟩] => simp at heval + | [⟨.PrimitiveOp _ _, _⟩] => simp at heval + | [⟨.IfThenElse _ _ _, _⟩] => simp at heval + | [⟨.Block _ _, _⟩] => simp at heval + | [⟨.Exit _, _⟩] => simp at heval + | [⟨.Return _, _⟩] => simp at heval + | [⟨.While _ _ _ _, _⟩] => simp at heval + | [⟨.Assign _ _, _⟩] => simp at heval + | [⟨.LocalVariable _ _ _, _⟩] => simp at heval + | [⟨.Assert _, _⟩] => simp at heval + | [⟨.Assume _, _⟩] => simp at heval + | [⟨.StaticCall _ _, _⟩] => simp at heval + | [⟨.New _, _⟩] => simp at heval + | [⟨.PureFieldUpdate _ _ _, _⟩] => simp at heval + | [⟨.ReferenceEquals _ _, _⟩] => simp at heval + | [⟨.InstanceCall _ _ _, _⟩] => simp at heval + | [⟨.This, _⟩] => simp at heval + | [⟨.IsType _ _, _⟩] => simp at heval + | [⟨.AsType _ _, _⟩] => simp at heval + | [⟨.Forall _ _ _, _⟩] => simp at heval + | [⟨.Exists _ _ _, _⟩] => simp at heval + | [⟨.Old _, _⟩] => simp at heval + | [⟨.Fresh _, _⟩] => simp at heval + | [⟨.Assigned _, _⟩] => simp at heval + | [⟨.ProveBy _ _, _⟩] => simp at heval + | [⟨.ContractOf _ _, _⟩] => simp at heval + | [⟨.Abstract, _⟩] => simp at heval + | [⟨.All, _⟩] => simp at heval + | [⟨.Hole, _⟩] => simp at heval + | _ :: _ :: _ => simp at heval + | LocalVariable name ty init => + cases init with + | some init => + match hi : interpStmt δ π n heap store init.val with + | some (.normal v, σ₁, h₁) => + have := interpStmt_fuel_mono hle' hi + simp [hi] at heval; simp [this]; exact heval + | some (.exit _, _, _) => simp [hi] at heval + | some (.ret _, _, _) => simp [hi] at heval + | none => simp [hi] at heval + | none => exact heval + | Assert c => + match hc : interpStmt δ π n heap store c.val with + | some (.normal (.vBool true), _, _) => + have := interpStmt_fuel_mono hle' hc + simp [hc] at heval; simp [this]; exact heval + | some (.normal (.vBool false), _, _) => simp [hc] at heval + | some (.normal (.vInt _), _, _) => simp [hc] at heval + | some (.normal (.vString _), _, _) => simp [hc] at heval + | some (.normal .vVoid, _, _) => simp [hc] at heval + | some (.normal (.vRef _), _, _) => simp [hc] at heval + | some (.exit _, _, _) => simp [hc] at heval + | some (.ret _, _, _) => simp [hc] at heval + | none => simp [hc] at heval + | Assume c => + match hc : interpStmt δ π n heap store c.val with + | some (.normal (.vBool true), _, _) => + have := interpStmt_fuel_mono hle' hc + simp [hc] at heval; simp [this]; exact heval + | some (.normal (.vBool false), _, _) => simp [hc] at heval + | some (.normal (.vInt _), _, _) => simp [hc] at heval + | some (.normal (.vString _), _, _) => simp [hc] at heval + | some (.normal .vVoid, _, _) => simp [hc] at heval + | some (.normal (.vRef _), _, _) => simp [hc] at heval + | some (.exit _, _, _) => simp [hc] at heval + | some (.ret _, _, _) => simp [hc] at heval + | none => simp [hc] at heval + | StaticCall callee args => + match hp : π callee with + | some proc => + simp [hp] at heval ⊢ + match hargs : interpArgs δ π n heap store args with + | some (vals, σ₁, h₁) => + have hargm := interpArgs_fuel_mono hle' hargs + simp [hargs] at heval; simp [hargm] + match hbind : bindParams proc.inputs vals with + | some σBound => + simp [hbind] at heval ⊢ + match hbody : getBody proc with + | some body => + simp [hbody] at heval ⊢ + match hcall : interpStmt δ π n h₁ σBound body.val with + | some (.normal v, _, h') => + have := interpStmt_fuel_mono hle' hcall + simp [hcall] at heval; simp [this]; exact heval + | some (.ret (some v), _, h') => + have := interpStmt_fuel_mono hle' hcall + simp [hcall] at heval; simp [this]; exact heval + | some (.ret none, _, h') => + have := interpStmt_fuel_mono hle' hcall + simp [hcall] at heval; simp [this]; exact heval + | some (.exit _, _, _) => simp [hcall] at heval + | none => simp [hcall] at heval + | none => simp [hbody] at heval + | none => simp [hbind] at heval + | none => simp [hargs] at heval + | none => simp [hp] at heval + | New => exact heval + | FieldSelect target fieldName => + match ht : interpStmt δ π n heap store target.val with + | some (.normal (.vRef addr), σ₁, h₁) => + have := interpStmt_fuel_mono hle' ht + simp [ht] at heval; simp [this]; exact heval + | some (.normal (.vInt _), _, _) => simp [ht] at heval + | some (.normal (.vBool _), _, _) => simp [ht] at heval + | some (.normal (.vString _), _, _) => simp [ht] at heval + | some (.normal .vVoid, _, _) => simp [ht] at heval + | some (.exit _, _, _) => simp [ht] at heval + | some (.ret _, _, _) => simp [ht] at heval + | none => simp [ht] at heval + | PureFieldUpdate target fieldName newVal => + match ht : interpStmt δ π n heap store target.val with + | some (.normal (.vRef addr), σ₁, h₁) => + have htm := interpStmt_fuel_mono hle' ht + simp [ht] at heval; simp [htm] + match hv : interpStmt δ π n h₁ σ₁ newVal.val with + | some (.normal v, σ₂, h₂) => + have := interpStmt_fuel_mono hle' hv + simp [hv] at heval; simp [this]; exact heval + | some (.exit _, _, _) => simp [hv] at heval + | some (.ret _, _, _) => simp [hv] at heval + | none => simp [hv] at heval + | some (.normal (.vInt _), _, _) => simp [ht] at heval + | some (.normal (.vBool _), _, _) => simp [ht] at heval + | some (.normal (.vString _), _, _) => simp [ht] at heval + | some (.normal .vVoid, _, _) => simp [ht] at heval + | some (.exit _, _, _) => simp [ht] at heval + | some (.ret _, _, _) => simp [ht] at heval + | none => simp [ht] at heval + | ReferenceEquals lhs rhs => + match hl : interpStmt δ π n heap store lhs.val with + | some (.normal (.vRef a), σ₁, h₁) => + have hlm := interpStmt_fuel_mono hle' hl + simp [hl] at heval; simp [hlm] + match hr : interpStmt δ π n h₁ σ₁ rhs.val with + | some (.normal (.vRef b), σ₂, h₂) => + have := interpStmt_fuel_mono hle' hr + simp [hr] at heval; simp [this]; exact heval + | some (.normal (.vInt _), _, _) => simp [hr] at heval + | some (.normal (.vBool _), _, _) => simp [hr] at heval + | some (.normal (.vString _), _, _) => simp [hr] at heval + | some (.normal .vVoid, _, _) => simp [hr] at heval + | some (.exit _, _, _) => simp [hr] at heval + | some (.ret _, _, _) => simp [hr] at heval + | none => simp [hr] at heval + | some (.normal (.vInt _), _, _) => simp [hl] at heval + | some (.normal (.vBool _), _, _) => simp [hl] at heval + | some (.normal (.vString _), _, _) => simp [hl] at heval + | some (.normal .vVoid, _, _) => simp [hl] at heval + | some (.exit _, _, _) => simp [hl] at heval + | some (.ret _, _, _) => simp [hl] at heval + | none => simp [hl] at heval + | InstanceCall target callee args => + match ht : interpStmt δ π n heap store target.val with + | some (.normal (.vRef addr), σ₁, h₁) => + have htm := interpStmt_fuel_mono hle' ht + simp [ht] at heval; simp [htm] + match hlook : h₁ addr with + | some (typeName, _) => + simp [hlook] at heval ⊢ + match hproc : π (↑(typeName ++ "." ++ callee.text)) with + | some proc => + simp [hproc] at heval ⊢ + match hargs : interpArgs δ π n h₁ σ₁ args with + | some (vals, σ₂, h₂) => + have hargm := interpArgs_fuel_mono hle' hargs + simp [hargs] at heval; simp [hargm] + match hbind : bindParams proc.inputs (LaurelValue.vRef addr :: vals) with + | some σBound => + simp [hbind] at heval ⊢ + match hbody : getBody proc with + | some body => + simp [hbody] at heval ⊢ + match hcall : interpStmt δ π n h₂ σBound body.val with + | some (.normal v, _, h₃) => + have := interpStmt_fuel_mono hle' hcall + simp [hcall] at heval; simp [this]; exact heval + | some (.ret (some v), _, h₃) => + have := interpStmt_fuel_mono hle' hcall + simp [hcall] at heval; simp [this]; exact heval + | some (.ret none, _, h₃) => + have := interpStmt_fuel_mono hle' hcall + simp [hcall] at heval; simp [this]; exact heval + | some (.exit _, _, _) => simp [hcall] at heval + | none => simp [hcall] at heval + | none => simp [hbody] at heval + | none => simp [hbind] at heval + | none => simp [hargs] at heval + | none => simp [hproc] at heval + | none => simp [hlook] at heval + | some (.normal (.vInt _), _, _) => simp [ht] at heval + | some (.normal (.vBool _), _, _) => simp [ht] at heval + | some (.normal (.vString _), _, _) => simp [ht] at heval + | some (.normal .vVoid, _, _) => simp [ht] at heval + | some (.exit _, _, _) => simp [ht] at heval + | some (.ret _, _, _) => simp [ht] at heval + | none => simp [ht] at heval + | This => exact heval + | IsType target ty => + match ht : interpStmt δ π n heap store target.val with + | some (.normal (.vRef addr), σ₁, h₁) => + have := interpStmt_fuel_mono hle' ht + simp [ht] at heval; simp [this]; exact heval + | some (.normal (.vInt _), _, _) => simp [ht] at heval + | some (.normal (.vBool _), _, _) => simp [ht] at heval + | some (.normal (.vString _), _, _) => simp [ht] at heval + | some (.normal .vVoid, _, _) => simp [ht] at heval + | some (.exit _, _, _) => simp [ht] at heval + | some (.ret _, _, _) => simp [ht] at heval + | none => simp [ht] at heval + | AsType target ty => + match ht : interpStmt δ π n heap store target.val with + | some (.normal v, σ₁, h₁) => + have := interpStmt_fuel_mono hle' ht + simp [ht] at heval; simp [this]; exact heval + | some (.exit _, _, _) => simp [ht] at heval + | some (.ret _, _, _) => simp [ht] at heval + | none => simp [ht] at heval + | Forall _ _ _ => exact heval + | Exists _ _ _ => exact heval + | Old _ => exact heval + | Fresh _ => exact heval + | Assigned _ => exact heval + | ProveBy value proof => + exact interpStmt_fuel_mono hle' heval + | ContractOf _ _ => exact heval + | Abstract => simp at heval + | All => simp at heval + | Hole => simp at heval + +theorem interpBlock_fuel_mono + {δ : LaurelEval} {π : ProcEnv} {fuel₁ fuel₂ : Nat} + {heap : LaurelHeap} {store : LaurelStore} {ss : List StmtExprMd} + {r : Outcome × LaurelStore × LaurelHeap} + (hle : fuel₁ ≤ fuel₂) + (heval : interpBlock δ π fuel₁ heap store ss = some r) : + interpBlock δ π fuel₂ heap store ss = some r := by + match fuel₁, fuel₂ with + | 0, _ => simp [interpBlock] at heval + | _ + 1, 0 => omega + | n + 1, m + 1 => + have hle' : n ≤ m := by omega + unfold interpBlock at heval ⊢ + cases ss with + | nil => exact heval + | cons s rest => + cases rest with + | nil => exact interpStmt_fuel_mono hle' heval + | cons s' rest' => + match hs : interpStmt δ π n heap store s.val with + | some (.normal _, σ₁, h₁) => + have := interpStmt_fuel_mono hle' hs + simp [hs] at heval; simp [this] + exact interpBlock_fuel_mono hle' heval + | some (.exit label, σ₁, h₁) => + have := interpStmt_fuel_mono hle' hs + simp [hs] at heval; simp [this]; exact heval + | some (.ret rv, σ₁, h₁) => + have := interpStmt_fuel_mono hle' hs + simp [hs] at heval; simp [this]; exact heval + | none => simp [hs] at heval + +theorem interpArgs_fuel_mono + {δ : LaurelEval} {π : ProcEnv} {fuel₁ fuel₂ : Nat} + {heap : LaurelHeap} {store : LaurelStore} {as : List StmtExprMd} + {r : List LaurelValue × LaurelStore × LaurelHeap} + (hle : fuel₁ ≤ fuel₂) + (heval : interpArgs δ π fuel₁ heap store as = some r) : + interpArgs δ π fuel₂ heap store as = some r := by + match fuel₁, fuel₂ with + | 0, _ => simp [interpArgs] at heval + | _ + 1, 0 => omega + | n + 1, m + 1 => + have hle' : n ≤ m := by omega + unfold interpArgs at heval ⊢ + cases as with + | nil => exact heval + | cons e es => + match he : interpStmt δ π n heap store e.val with + | some (.normal v, σ₁, h₁) => + have hem := interpStmt_fuel_mono hle' he + simp [he] at heval; simp [hem] + match hes : interpArgs δ π n h₁ σ₁ es with + | some (vs, σ₂, h₂) => + have := interpArgs_fuel_mono hle' hes + simp [hes] at heval; simp [this]; exact heval + | none => simp [hes] at heval + | some (.exit _, _, _) => simp [he] at heval + | some (.ret _, _, _) => simp [he] at heval + | none => simp [he] at heval +end + +end Strata.Laurel diff --git a/Strata/Languages/Laurel/LaurelSemantics.lean b/Strata/Languages/Laurel/LaurelSemantics.lean new file mode 100644 index 000000000..66c2fcfd5 --- /dev/null +++ b/Strata/Languages/Laurel/LaurelSemantics.lean @@ -0,0 +1,190 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Languages.Laurel.Laurel + +/-! +# Laurel Semantic Types and Helpers + +Shared type definitions (values, stores, heaps, outcomes) and helper +functions used by the interpreter (`LaurelInterpreter.lean`) and +concrete evaluator (`LaurelConcreteEval.lean`). + +## Module Layering + +- `LaurelSemantics` — types and pure helpers (this file) +- `LaurelInterpreter` — fuel-based recursive interpreter over `StmtExpr` +- `LaurelConcreteEval` — bridges interpreter to `Laurel.Program` (builds + `ProcEnv`, initial store, runs `main`) +-/ +namespace Strata.Laurel + +/-- Structural `DecidableEq` for `Identifier` comparing both `text` and `uniqueId`. + Note: the `BEq` instance in `Laurel.lean` only compares `.text` (temporary hack). + Proofs that rely on `BEq` agreeing with `DecidableEq` should use `Identifier.beq_eq` + or work with `BEq` directly. -/ +instance : DecidableEq Identifier := fun a b => + match decEq a.text b.text, decEq a.uniqueId b.uniqueId with + | .isTrue ht, .isTrue hu => + .isTrue (by cases a; cases b; simp at ht hu; simp [ht, hu]) + | .isFalse ht, _ => + .isFalse (by intro heq; cases heq; exact ht rfl) + | _, .isFalse hu => + .isFalse (by intro heq; cases heq; exact hu rfl) + +/-! ## Values -/ + +inductive LaurelValue where + | vInt : Int → LaurelValue + | vBool : Bool → LaurelValue + | vString : String → LaurelValue + | vVoid : LaurelValue + | vRef : Nat → LaurelValue + deriving Repr, BEq, Inhabited, DecidableEq + +/-! ## Store and Heap -/ + +/-- Variable store keyed by `String` (the `.text` of an `Identifier`). + Using `String` ensures `BEq` and `DecidableEq` agree, which is required + by the bridging proofs between relational and interpreter semantics. -/ +abbrev LaurelStore := String → Option LaurelValue +abbrev LaurelHeap := Nat → Option (String × (String → Option LaurelValue)) +abbrev LaurelEval := LaurelStore → StmtExpr → Option LaurelValue +abbrev ProcEnv := Identifier → Option Procedure + +/-! ## Outcomes -/ + +inductive Outcome where + | normal : LaurelValue → Outcome + | exit : String → Outcome + | ret : Option LaurelValue → Outcome + deriving Repr, BEq, Inhabited, DecidableEq + +/-! ## Store Operations -/ + +inductive UpdateStore : LaurelStore → String → LaurelValue → LaurelStore → Prop where + | update : + σ x = .some v' → + σ' x = .some v → + (∀ y, x ≠ y → σ' y = σ y) → + UpdateStore σ x v σ' + +inductive InitStore : LaurelStore → String → LaurelValue → LaurelStore → Prop where + | init : + σ x = none → + σ' x = .some v → + (∀ y, x ≠ y → σ' y = σ y) → + InitStore σ x v σ' + +/-! ## Heap Operations -/ + +/-- Heap allocation using a bump-allocator (smallest-free-address) model. +The `alloc` constructor requires `addr` to be the smallest free address: +all addresses below `addr` must be occupied (`(h a).isSome`). +This invariant makes allocation deterministic but precludes heap deallocation. +If Laurel ever needs a `free` operation, this must be relaxed to a free-list +model, which would invalidate `AllocHeap_deterministic` and downstream proofs. -/ +inductive AllocHeap : LaurelHeap → String → Nat → LaurelHeap → Prop where + | alloc : + h addr = none → + (∀ a, a < addr → (h a).isSome) → + h' addr = .some (typeName, fun _ => none) → + (∀ a, addr ≠ a → h' a = h a) → + AllocHeap h typeName addr h' + +def heapFieldRead (h : LaurelHeap) (addr : Nat) (field : String) : Option LaurelValue := + match h addr with + | some (_, fields) => fields field + | none => none + +inductive HeapFieldWrite : LaurelHeap → Nat → String → LaurelValue → LaurelHeap → Prop where + | write : + h addr = .some (tag, fields) → + h' addr = .some (tag, fun f => if f == field then some v else fields f) → + (∀ a, addr ≠ a → h' a = h a) → + HeapFieldWrite h addr field v h' + +/-! ## Helpers -/ + +def catchExit : Option String → Outcome → Outcome + | some l, .exit l' => if l == l' then .normal .vVoid else .exit l' + | _, o => o + +def evalPrimOp (op : Operation) (args : List LaurelValue) : Option LaurelValue := + match op, args with + -- `And`/`Or` are eager boolean operators: both operands are fully evaluated. + -- `AndThen`/`OrElse`/`Implies` are short-circuit operators handled in `interpStmt` + -- (they return `none` here because evalPrimOp only handles eager evaluation). + | .And, [.vBool a, .vBool b] => some (.vBool (a && b)) + | .Or, [.vBool a, .vBool b] => some (.vBool (a || b)) + | .Not, [.vBool a] => some (.vBool (!a)) + | .Add, [.vInt a, .vInt b] => some (.vInt (a + b)) + | .Sub, [.vInt a, .vInt b] => some (.vInt (a - b)) + | .Mul, [.vInt a, .vInt b] => some (.vInt (a * b)) + | .Neg, [.vInt a] => some (.vInt (-a)) + | .Div, [.vInt a, .vInt b] => if b != 0 then some (.vInt (a / b)) else none + | .Mod, [.vInt a, .vInt b] => if b != 0 then some (.vInt (a % b)) else none + | .DivT, [.vInt a, .vInt b] => if b != 0 then some (.vInt (a.tdiv b)) else none + | .ModT, [.vInt a, .vInt b] => if b != 0 then some (.vInt (a.tmod b)) else none + | .Eq, [.vInt a, .vInt b] => some (.vBool (a == b)) + | .Neq, [.vInt a, .vInt b] => some (.vBool (a != b)) + | .Lt, [.vInt a, .vInt b] => some (.vBool (a < b)) + | .Leq, [.vInt a, .vInt b] => some (.vBool (a ≤ b)) + | .Gt, [.vInt a, .vInt b] => some (.vBool (a > b)) + | .Geq, [.vInt a, .vInt b] => some (.vBool (a ≥ b)) + | .Eq, [.vBool a, .vBool b] => some (.vBool (a == b)) + | .Neq, [.vBool a, .vBool b] => some (.vBool (a != b)) + | .Eq, [.vString a, .vString b] => some (.vBool (a == b)) + | .Neq, [.vString a, .vString b] => some (.vBool (a != b)) + | .StrConcat, [.vString a, .vString b] => some (.vString (a ++ b)) + | .Eq, [.vRef a, .vRef b] => some (.vBool (a == b)) + | .Neq, [.vRef a, .vRef b] => some (.vBool (a != b)) + -- Arity/type mismatches for each operation (no wildcard catch-all): + | .And, _ => none + | .Or, _ => none + | .Not, _ => none + | .Implies, _ => none + | .AndThen, _ => none + | .OrElse, _ => none + | .Neg, _ => none + | .Add, _ => none + | .Sub, _ => none + | .Mul, _ => none + | .Div, _ => none + | .Mod, _ => none + | .DivT, _ => none + | .ModT, _ => none + | .Eq, _ => none + | .Neq, _ => none + | .Lt, _ => none + | .Leq, _ => none + | .Gt, _ => none + | .Geq, _ => none + | .StrConcat, _ => none + +def getBody : Procedure → Option StmtExprMd + | { body := .Transparent b, .. } => some b + | { body := .Opaque _ (some b) _, .. } => some b + | _ => none + +/-- Bind parameters to values starting from an empty store (lexical scoping). -/ +def bindParams (params : List Parameter) (vals : List LaurelValue) + : Option LaurelStore := + go (fun _ => none) params vals +where + go (σ : LaurelStore) : List Parameter → List LaurelValue → Option LaurelStore + | [], [] => some σ + | p :: ps, v :: vs => + if σ p.name.text = none then + go (fun x => if x == p.name.text then some v else σ x) ps vs + else none + | _, _ => none + +def HighType.typeName : HighType → String + | .UserDefined name => name.text + | _ => "" + +end Strata.Laurel diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean index 125fac35f..88dc101e0 100644 --- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean +++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean @@ -582,15 +582,16 @@ def translateDatatypeDefinition (model : SemanticModel) (dt : DatatypeDefinition structure LaurelTranslateOptions where emitResolutionErrors : Bool := true -abbrev TranslateResult := (Option Core.Program) × (List DiagnosticModel) /-- -Translate Laurel Program to Core Program +Apply the full Laurel→Laurel lowering pipeline (all passes before the Laurel→Core translation). +Returns the lowered program. -/ -def translate (options: LaurelTranslateOptions) (program : Program): TranslateResult := +abbrev LowerResult := (ResolutionResult) × (List DiagnosticModel) + +def lowerLaurelToLaurel (program : Program) : LowerResult := let program := { program with staticProcedures := coreDefinitionsForLaurel.staticProcedures ++ program.staticProcedures } - let result := resolve program let (program, model) := (result.program, result.model) let diamondErrors := validateDiamondFieldAccesses model program @@ -598,7 +599,6 @@ def translate (options: LaurelTranslateOptions) (program : Program): TranslateRe let program := heapParameterization model program let result := resolve program (some model) let (program, model) := (result.program, result.model) - let program := typeHierarchyTransform model program let result := resolve program (some model) let (program, model) := (result.program, result.model) @@ -608,8 +608,6 @@ def translate (options: LaurelTranslateOptions) (program : Program): TranslateRe -- dbg_trace "=== Program after heapParameterization + modifiesClausesTransform ===" -- dbg_trace (toString (Std.Format.pretty (Std.ToFormat.format program))) -- dbg_trace "=================================" - let result := resolve program (some model) - let (program, model) := (result.program, result.model) let program := inferHoleTypes model program let program := eliminateHoles program let program := desugarShortCircuit model program @@ -617,15 +615,22 @@ def translate (options: LaurelTranslateOptions) (program : Program): TranslateRe let program := eliminateReturnsInExpressionTransform program let result := resolve program (some model) let (program, model) := (result.program, result.model) - let (program, constrainedTypeDiags) := constrainedTypeElim model program - let result := resolve program (some model) + (resolve program (some model) , diamondErrors ++ modifiesDiags ++ constrainedTypeDiags) + +abbrev TranslateResult := (Option Core.Program) × (List DiagnosticModel) +/-- +Translate Laurel Program to Core Program +-/ +def translate (options: LaurelTranslateOptions) (program : Program): TranslateResult := + let (result, lowerErrors) := lowerLaurelToLaurel program + let (program, model) := (result.program, result.model) let initState : TranslateState := {model := model } let (coreProgramOption, translateState) := runTranslateM initState (translateLaurelToCore program) let resolutionErrors: List DiagnosticModel := if options.emitResolutionErrors then result.errors.toList else [] - let allDiagnostics := resolutionErrors ++ diamondErrors ++ modifiesDiags ++ constrainedTypeDiags ++ translateState.diagnostics + let allDiagnostics := resolutionErrors ++ lowerErrors ++ translateState.diagnostics let coreProgramOption := if translateState.coreProgramHasSuperfluousErrors then none else coreProgramOption (coreProgramOption, allDiagnostics) where diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean index e29618fef..12e322b0d 100644 --- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean +++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean @@ -223,24 +223,75 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do return resultExpr | .PrimitiveOp op args => - -- Process arguments right to left - let seqArgs ← args.reverse.mapM transformExpr + -- Process arguments right to left (for substitution mechanism) + let seqArgs ← args.reverse.attach.mapM fun ⟨arg, _⟩ => transformExpr arg return ⟨.PrimitiveOp op seqArgs.reverse, md⟩ | .StaticCall callee args => let model := (← get).model - let seqArgs ← args.reverse.mapM transformExpr - let seqCall := ⟨.StaticCall callee seqArgs.reverse, md⟩ + -- Why this is more complex than PrimitiveOp's right-to-left traversal: + -- + -- PrimitiveOp can simply process args R-to-L because the substitution + -- mechanism handles variable snapshots. But for imperative StaticCalls, + -- we must also lift the call itself to a prepend, and the interaction + -- between arg prepends and the call prepend creates two bugs that the + -- simple approach doesn't fix: + -- + -- Bug 1 (nested calls): `add(mul(2,3), mul(4,5))` — if we just process + -- args R-to-L and collect all prepends, the outer call's temp is declared + -- before inner calls' temps, referencing undeclared variables. + -- + -- Bug 2 (evaluation order): `add({x:=1;x}, {x:=x+10;x})` — if we mix + -- all arg prepends together, arg2's side effect `x:=x+10` executes before + -- arg1's `x:=1`, breaking left-to-right evaluation order. We must: + -- (a) isolate each arg's prepends so they don't leak across args + -- (b) capture side-effectful results in temporaries + -- (c) emit prepend groups in left-to-right order + -- + -- The simple fix (just reordering the call's prepend relative to arg + -- prepends) handles Bug 1 but NOT Bug 2. Both bugs are covered by + -- TransformPreservation tests in StrataTest/Languages/Laurel/ConcreteEval/. + -- + -- Isolate each arg's prepends, capture side-effectful args in temps, + -- then combine prepend groups in left-to-right order. + let savedPrepends := (← get).prependedStmts + let results ← args.reverse.attach.mapM fun ⟨arg, _⟩ => do + modify fun s => { s with prependedStmts := [] } + let seqArg ← transformExpr arg + let argPrepends ← takePrepends + if !argPrepends.isEmpty then + let needsCapture := match seqArg.val with + | .Identifier name => !name.text.startsWith "$" + | _ => true + if needsCapture then + let tmpVar ← freshCondVar + let tmpType ← computeType arg + let capture := [bare (.LocalVariable tmpVar tmpType none), + ⟨.Assign [bare (.Identifier tmpVar)] seqArg, md⟩] + return (argPrepends ++ capture, bare (.Identifier tmpVar)) + else + return (argPrepends, seqArg) + else + return ([], seqArg) + -- Restore saved prepends and add arg groups in left-to-right order + modify fun s => { s with prependedStmts := savedPrepends } + -- results is in right-to-left order; reverse to get left-to-right + let resultsLR := results.reverse + let seqArgs := resultsLR.map (·.2) + -- Emit groups right-to-left so that left groups end up on top of the + -- cons-based prepend stack (executed first). Each group's statements + -- are in program order, so reverse before cons-ing. + results.forM fun (group, _) => group.reverse.forM addPrepend + let seqCall := ⟨.StaticCall callee seqArgs, md⟩ if model.isFunction callee then return seqCall else - -- Imperative call in expression position: lift it like an assignment - -- Order matters: assign must be prepended first (it's newest-first), - -- so that when reversed the var declaration comes before the call. + let allArgPrepends ← takePrepends let callResultVar ← freshCondVar let callResultType ← computeType expr addPrepend (⟨.Assign [bare (.Identifier callResultVar)] seqCall, md⟩) addPrepend (bare (.LocalVariable callResultVar callResultType none)) + allArgPrepends.reverse.forM addPrepend return bare (.Identifier callResultVar) | .IfThenElse cond thenBranch elseBranch => diff --git a/Strata/Languages/Laurel/laurel-denotational-semantics.md b/Strata/Languages/Laurel/laurel-denotational-semantics.md new file mode 100644 index 000000000..e7732783d --- /dev/null +++ b/Strata/Languages/Laurel/laurel-denotational-semantics.md @@ -0,0 +1,136 @@ +# Laurel Denotational Semantics + +**Date:** 2026-03-20 +**Files:** +- `Strata/Languages/Laurel/LaurelSemantics.lean` — shared types and helpers +- `Strata/Languages/Laurel/LaurelDenote.lean` — interpreter +- `Strata/Languages/Laurel/LaurelDenoteMono.lean` — fuel monotonicity + +## Overview + +This document describes the fuel-based denotational interpreter for +Laurel IR. The interpreter is a computable Lean function that serves +as an executable reference semantics for Laurel programs. It is used +for testing, debugging, and as the foundation for the concrete +evaluator. + +## Motivation + +For testing, debugging, and downstream tooling, we need a computable +interpreter that: + +1. Can be `#eval`'d on concrete programs +2. Is deterministic by construction (it is a function, not a relation) +3. Covers all Laurel constructs comprehensively + +## Design + +### Fuel Parameter + +The interpreter uses a `fuel : Nat` parameter decremented on every +recursive call. This ensures termination (required by Lean for +non-`partial` functions) without restricting the class of programs that +can be evaluated — any terminating program can be evaluated with +sufficient fuel. + +When fuel reaches zero, the interpreter returns `none` (indistinguishable +from a stuck program). This is a limitation: the interpreter cannot +distinguish non-termination from insufficient fuel. + +### Three Mutually Recursive Functions + +| Function | Signature | Purpose | +|----------|-----------|---------| +| `denoteStmt` | `δ → π → fuel → h → σ → StmtExpr → Option (Outcome × LaurelStore × LaurelHeap)` | Evaluate a single statement/expression | +| `denoteBlock` | `δ → π → fuel → h → σ → List StmtExprMd → Option (Outcome × LaurelStore × LaurelHeap)` | Evaluate a block of statements | +| `denoteArgs` | `δ → π → fuel → h → σ → List StmtExprMd → Option (List LaurelValue × LaurelStore × LaurelHeap)` | Evaluate arguments left-to-right | + +### Return Convention + +The interpreter returns `Option (Outcome × LaurelStore × LaurelHeap)`: +- `some (outcome, σ', h')` — successful evaluation +- `none` — stuck state or fuel exhaustion + +### Computable Store/Heap Helpers + +The shared types in `LaurelSemantics.lean` include inductive relations +for store and heap operations (`UpdateStore`, `InitStore`, `AllocHeap`, +`HeapFieldWrite`). The denotational interpreter needs computable +versions: + +| Computable | Relational | Purpose | +|------------|------------|---------| +| `updateStore σ x v` | `UpdateStore σ x.text v σ'` | Update existing variable | +| `initStore σ x v` | `InitStore σ x.text v σ'` | Initialize new variable | +| `allocHeap h typeName` | `AllocHeap h typeName addr h'` | Allocate heap object | +| `heapFieldWrite' h addr field v` | `HeapFieldWrite h addr field v h'` | Write heap field | + +Each computable helper returns `Option` — `none` when the precondition +fails (e.g., `updateStore` on an undefined variable). + +### Heap Allocation Bound + +The computable `allocHeap` searches a bounded range (`heapSearchBound = +10000`) for a free address using `findSmallestFree`. The relational +`AllocHeap` has no such bound. This means the interpreter can fail on +programs that allocate more than 10000 objects. + +## Construct Coverage + +The interpreter covers the following constructs: + +- **Literals:** `LiteralInt`, `LiteralBool`, `LiteralString` — return + the value directly +- **Variables:** `Identifier` — look up in store +- **Operations:** `PrimitiveOp` — evaluate args via `denoteArgs`, apply op +- **Control flow:** `IfThenElse`, `Block`, `Exit`, `Return`, `While` +- **Assignments:** `Assign` (single target, field target), `LocalVariable` +- **Verification:** `Assert`, `Assume` — evaluate condition, discard + state effects, require `true` +- **Calls:** `StaticCall`, `InstanceCall` — evaluate args, bind params, + evaluate body, handle normal/return outcomes +- **OO:** `New`, `FieldSelect`, `PureFieldUpdate`, `ReferenceEquals`, + `This`, `IsType`, `AsType` +- **Specification:** `Forall`, `Exists`, `Old`, `Fresh`, `Assigned`, + `ProveBy`, `ContractOf` — delegated to `δ` +- **Omitted:** `Abstract`, `All`, `Hole` — return `none` + +## Fuel Monotonicity + +`LaurelDenoteMono.lean` proves that the interpreter is monotone in fuel: + +``` +denoteStmt_fuel_mono : fuel₁ ≤ fuel₂ → + denoteStmt δ π fuel₁ h σ s = some r → + denoteStmt δ π fuel₂ h σ s = some r +``` + +If the interpreter succeeds with `fuel₁`, it succeeds with any larger +fuel giving the same result. This is proved by mutual induction on fuel, +case-splitting on the statement, and applying the IH to sub-calls. + +Analogous theorems hold for `denoteBlock` and `denoteArgs`. + +## Limitations + +1. **Fuel exhaustion is indistinguishable from stuck.** When fuel + reaches zero, the interpreter returns `none` — the same result as + for a stuck program (e.g., undefined variable, type error). There + is no way to distinguish "needs more fuel" from "genuinely stuck." + +2. **Heap allocation bound.** The computable `allocHeap` searches at + most `heapSearchBound = 10000` addresses for a free slot. Programs + that allocate more than 10000 objects will fail. This bound is + hardcoded. + +3. **No partial evaluation.** The interpreter is total (not `partial`), + which means it cannot handle non-terminating programs at all — it + simply runs out of fuel. + +4. **Unsupported constructs.** `LiteralDecimal` returns `none` (no + float/decimal value type). `Abstract`, `All`, `Hole` return `none`. + Multi-target `Assign` returns `none`. `DivT` and `ModT` are not + handled by `evalPrimOp`. Float64 operands are not supported. + Procedures with `Abstract` or `External` bodies cannot be called + (`getBody` returns `none`). Non-local control flow in arguments + causes `none` (each argument must produce `.normal v`). diff --git a/StrataTest/Languages/Laurel/ConcreteEval.lean b/StrataTest/Languages/Laurel/ConcreteEval.lean new file mode 100644 index 000000000..002442053 --- /dev/null +++ b/StrataTest/Languages/Laurel/ConcreteEval.lean @@ -0,0 +1,22 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +-- TODO: Update this barrel file as new test modules are added to ConcreteEval/ +import StrataTest.Languages.Laurel.ConcreteEval.TestHelper +import StrataTest.Languages.Laurel.ConcreteEval.Procedures +import StrataTest.Languages.Laurel.ConcreteEval.Aliasing +import StrataTest.Languages.Laurel.ConcreteEval.SideEffects +import StrataTest.Languages.Laurel.ConcreteEval.BooleanOps +import StrataTest.Languages.Laurel.ConcreteEval.Primitives +import StrataTest.Languages.Laurel.ConcreteEval.Arithmetic +import StrataTest.Languages.Laurel.ConcreteEval.ControlFlow +import StrataTest.Languages.Laurel.ConcreteEval.Variables +import StrataTest.Languages.Laurel.ConcreteEval.HeapObjects +import StrataTest.Languages.Laurel.ConcreteEval.Recursion +import StrataTest.Languages.Laurel.ConcreteEval.Verification +import StrataTest.Languages.Laurel.ConcreteEval.TypeOps +import StrataTest.Languages.Laurel.ConcreteEval.EdgeCases +import StrataTest.Languages.Laurel.ConcreteEval.TransformPreservation diff --git a/StrataTest/Languages/Laurel/ConcreteEval/Aliasing.lean b/StrataTest/Languages/Laurel/ConcreteEval/Aliasing.lean new file mode 100644 index 000000000..a2b14b86b --- /dev/null +++ b/StrataTest/Languages/Laurel/ConcreteEval/Aliasing.lean @@ -0,0 +1,140 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import StrataTest.Languages.Laurel.ConcreteEval.TestHelper + +/-! +# Aliasing Semantics Tests + +Tests for reference aliasing: shared mutation, distinct objects, +aliasing through procedure calls, and programmatic ReferenceEquals. +-/ + +namespace Strata.Laurel.ConcreteEval.AliasingTest + +open Strata.Laurel.ConcreteEval.TestHelper +open Strata.Laurel + +/-! ## Test 1: Simple aliasing — two vars, same object -/ + +/-- +info: returned: 42 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +composite Point { var x: int } +procedure main() { + var p: Point := new Point; p#x := 1; + var q: Point := p; + q#x := 42; + return p#x +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 2: Aliasing through procedure call — pass same object twice -/ + +/-- +info: returned: 5 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +composite Box { var v: int } +procedure swap(a: Box, b: Box) { + var tmp: int := a#v; a#v := b#v; b#v := tmp +}; +procedure main() { + var b: Box := new Box; b#v := 5; + swap(b, b); + return b#v +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 3: Distinct objects are independent -/ + +/-- +info: returned: 2 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +composite Point { var x: int } +procedure main() { + var p: Point := new Point; p#x := 1; + var q: Point := new Point; q#x := 2; + p#x := 99; + return q#x +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 4: Alias survives procedure call -/ + +/-- +info: returned: 42 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +composite Box { var v: int } +procedure setV(b: Box, x: int) { b#v := x }; +procedure main() { + var a: Box := new Box; a#v := 0; + var b: Box := a; + setV(a, 42); + return b#v +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 5: ReferenceEquals — programmatic AST test -/ + +-- 5a: Same ref → true +#guard + let body := StmtExpr.Block [ + mk (.LocalVariable "p" ⟨.UserDefined "Point", emd⟩ (some (mk (.New "Point")))), + mk (.LocalVariable "q" ⟨.UserDefined "Point", emd⟩ (some (mk (.Identifier "p")))), + mk (.Return (some (mk (.ReferenceEquals (mk (.Identifier "p")) (mk (.Identifier "q")))))) + ] none + let pointType : TypeDefinition := .Composite { + name := "Point" + extending := [] + fields := [{ name := "x", isMutable := true, type := ⟨.TInt, emd⟩ }] + instanceProcedures := [] + } + let prog : Program := { + staticProcedures := [mkProc "main" [] body] + staticFields := [] + types := [pointType] + constants := [] + } + getOutcome (evalProgram prog) = some (.ret (some (.vBool true))) + +-- 5b: Different refs → false +#guard + let body := StmtExpr.Block [ + mk (.LocalVariable "p" ⟨.UserDefined "Point", emd⟩ (some (mk (.New "Point")))), + mk (.LocalVariable "r" ⟨.UserDefined "Point", emd⟩ (some (mk (.New "Point")))), + mk (.Return (some (mk (.ReferenceEquals (mk (.Identifier "p")) (mk (.Identifier "r")))))) + ] none + let pointType : TypeDefinition := .Composite { + name := "Point" + extending := [] + fields := [{ name := "x", isMutable := true, type := ⟨.TInt, emd⟩ }] + instanceProcedures := [] + } + let prog : Program := { + staticProcedures := [mkProc "main" [] body] + staticFields := [] + types := [pointType] + constants := [] + } + getOutcome (evalProgram prog) = some (.ret (some (.vBool false))) + +end Strata.Laurel.ConcreteEval.AliasingTest diff --git a/StrataTest/Languages/Laurel/ConcreteEval/Arithmetic.lean b/StrataTest/Languages/Laurel/ConcreteEval/Arithmetic.lean new file mode 100644 index 000000000..0045214fb --- /dev/null +++ b/StrataTest/Languages/Laurel/ConcreteEval/Arithmetic.lean @@ -0,0 +1,226 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import StrataTest.Languages.Laurel.ConcreteEval.TestHelper + +/-! +# Arithmetic Operations Tests + +Tests for basic arithmetic (add, sub, mul, div, mod), negation via +subtraction, division/modulus by zero, large integers, compound +expressions, and DivT/ModT stuck behavior. +-/ + +namespace Strata.Laurel.ConcreteEval.ArithmeticTest + +open Strata.Laurel.ConcreteEval.TestHelper +open Strata.Laurel + +/-! ## Test 1: Addition -/ + +/-- +info: returned: 7 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { return 3 + 4 }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 2: Subtraction -/ + +/-- +info: returned: 7 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { return 10 - 3 }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 3: Multiplication -/ + +/-- +info: returned: 42 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { return 6 * 7 }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 4: Euclidean division -/ + +/-- +info: returned: 3 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { return 7 / 2 }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 5: Euclidean modulus -/ + +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { return 7 % 2 }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 6: Negation via subtraction -/ + +/-- +info: returned: -5 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { return 0 - 5 }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 7: Division by zero — stuck -/ + +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { return 1 / 0 }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 8: Modulus by zero — stuck -/ + +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { return 1 % 0 }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 9: Large integers (arbitrary precision) -/ + +/-- +info: returned: 1000000000000000000 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { return 1000000000 * 1000000000 }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 10: Compound expression -/ + +/-- +info: returned: 15 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { return (2 + 3) * (4 - 1) }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 11: Negative arithmetic -/ + +/-- +info: returned: -7 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { return (-3) + (-4) }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 12: DivT — truncation division -/ + +/-- +info: returned: 3 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { return 7 /t 2 }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 13: ModT — truncation modulus -/ + +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { return 7 %t 2 }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 14: DivT with negative dividend (truncation toward zero) -/ + +/-- +info: returned: -3 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { return (-7) /t 2 }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 15: ModT with negative dividend -/ + +/-- +info: returned: -1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { return (-7) %t 2 }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 16: DivT by zero — stuck -/ + +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { return 7 /t 0 }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 17: ModT by zero — stuck -/ + +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { return 7 %t 0 }; +" + IO.println (toString (runProgram prog)) + +end Strata.Laurel.ConcreteEval.ArithmeticTest diff --git a/StrataTest/Languages/Laurel/ConcreteEval/BooleanOps.lean b/StrataTest/Languages/Laurel/ConcreteEval/BooleanOps.lean new file mode 100644 index 000000000..01ec1718b --- /dev/null +++ b/StrataTest/Languages/Laurel/ConcreteEval/BooleanOps.lean @@ -0,0 +1,268 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import StrataTest.Languages.Laurel.ConcreteEval.TestHelper + +/-! +# Boolean Operations and Short-Circuit Semantics Tests + +Tests for comparison operators, boolean operations, and short-circuit +semantics. Short-circuit tests verify that side effects do NOT occur +in the unevaluated branch. + +All tests use `parseLaurel`. The interpreter (`interpStmt`) +evaluates `AndThen`/`OrElse`/`Implies` with proper short-circuit semantics, +while `And`/`Or` are evaluated eagerly via `evalPrimOp`. +-/ + +namespace Strata.Laurel.ConcreteEval.BooleanOpsTest + +open Strata.Laurel.ConcreteEval.TestHelper +open Strata.Laurel + +/-! ## Comparison Operators -/ + +/-! ### Test 1: Lt, Leq, Gt, Geq on integers -/ + +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + var a: bool := 1 < 2; + var b: bool := 2 <= 2; + var c: bool := 3 > 2; + var d: bool := 2 >= 2; + if (a && b && c && d) { return 1 } else { return 0 } +}; +" + IO.println (toString (runProgram prog)) + +/-! ### Test 2: Eq and Neq on integers -/ + +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + if (5 == 5 && 5 != 6) { return 1 } else { return 0 } +}; +" + IO.println (toString (runProgram prog)) + +/-! ### Test 3: Eq and Neq on booleans -/ + +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + if (true == true && true != false) { return 1 } else { return 0 } +}; +" + IO.println (toString (runProgram prog)) + +/-! ### Test 4: Eq and Neq on strings -/ + +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r#" +procedure main() { + if ("abc" == "abc" && "abc" != "def") { return 1 } else { return 0 } +}; +"# + IO.println (toString (runProgram prog)) + +/-! ### Test 5: Not operator -/ + +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + if (!false && !(!true)) { return 1 } else { return 0 } +}; +" + IO.println (toString (runProgram prog)) + +/-! ### Test 6: String concatenation -/ + +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r#" +procedure main() { + if ("ab" ++ "cd" == "abcd") { return 1 } else { return 0 } +}; +"# + IO.println (toString (runProgram prog)) + +/-! ## Short-Circuit And -/ + +/-! ### Test 7: false && — RHS not evaluated -/ + +/-- +info: returned: 0 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + var x: int := 0; + var b: bool := false && {x := 1; true}; + return x +}; +" + IO.println (toString (runProgram prog)) + +/-! ### Test 8: true && — RHS IS evaluated -/ + +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + var x: int := 0; + var b: bool := true && {x := 1; true}; + return x +}; +" + IO.println (toString (runProgram prog)) + +/-! ### Test 9: Nested short-circuit And -/ + +/-- +info: returned: 0 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + var x: int := 0; + var b: bool := false && (true && {x := 1; true}); + return x +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Short-Circuit Or -/ + +/-! ### Test 10: true || — RHS not evaluated -/ + +/-- +info: returned: 0 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + var x: int := 0; + var b: bool := true || {x := 1; false}; + return x +}; +" + IO.println (toString (runProgram prog)) + +/-! ### Test 11: false || — RHS IS evaluated -/ + +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + var x: int := 0; + var b: bool := false || {x := 1; true}; + return x +}; +" + IO.println (toString (runProgram prog)) + +/-! ### Test 12: Nested short-circuit Or -/ + +/-- +info: returned: 0 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + var x: int := 0; + var b: bool := true || (false || {x := 1; true}); + return x +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Short-Circuit Implies -/ + +/-! ### Test 13: false ==> — RHS not evaluated -/ + +/-- +info: returned: 0 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + var x: int := 0; + var b: bool := false ==> {x := 1; false}; + return x +}; +" + IO.println (toString (runProgram prog)) + +/-! ### Test 14: true ==> — RHS IS evaluated -/ + +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + var x: int := 0; + var b: bool := true ==> {x := 1; true}; + return x +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Combined -/ + +/-! ### Test 15: Mixed short-circuit with side effects -/ + +/-- +info: returned: 10 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + var x: int := 0; + var b: bool := (true || {x := x + 1; true}) && (false || {x := x + 10; true}); + return x +}; +" + IO.println (toString (runProgram prog)) + +end Strata.Laurel.ConcreteEval.BooleanOpsTest diff --git a/StrataTest/Languages/Laurel/ConcreteEval/ControlFlow.lean b/StrataTest/Languages/Laurel/ConcreteEval/ControlFlow.lean new file mode 100644 index 000000000..8ade57d72 --- /dev/null +++ b/StrataTest/Languages/Laurel/ConcreteEval/ControlFlow.lean @@ -0,0 +1,277 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import StrataTest.Languages.Laurel.ConcreteEval.TestHelper + +/-! +# Control Flow Tests + +Tests for if-then-else, while loops, early return, nested control flow, +fuel exhaustion, and labeled block exit (break). +-/ + +namespace Strata.Laurel.ConcreteEval.ControlFlowTest + +open Strata.Laurel.ConcreteEval.TestHelper +open Strata.Laurel + +/-! ## Test 1: If-then-else, true branch -/ + +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + if (true) { return 1 } else { return 2 } +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 2: If-then-else, false branch -/ + +/-- +info: returned: 2 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + if (false) { return 1 } else { return 2 } +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 3: If-then without else (true) — returns result of then branch -/ + +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + if (true) { return 1 }; + return 0 +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 4: If-then without else (false) — falls through -/ + +/-- +info: returned: 0 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + var x: int := 0; + if (false) { x := 1 }; + return x +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 5: Nested if-then-else -/ + +/-- +info: returned: 2 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + var x: int := 15; + if (x > 10) { + if (x > 20) { return 3 } else { return 2 } + } else { return 1 } +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 6: While loop — zero iterations -/ + +/-- +info: returned: 0 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + var x: int := 0; + while (false) { x := 1 }; + return x +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 7: While loop — single iteration -/ + +/-- +info: returned: 42 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + var x: int := 0; + var done: bool := false; + while (!done) { x := 42; done := true }; + return x +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 8: While loop with early return -/ + +/-- +info: returned: 5 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + var i: int := 0; + while (i < 100) { + if (i == 5) { return i }; + i := i + 1 + }; + return -1 +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 9: Return from nested blocks propagates -/ + +/-- +info: returned: 42 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + var x: int := 0; + if (true) { + if (true) { + return 42 + } + }; + return 0 +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 10: Nested while loops + +Variable declarations inside loop bodies fail on re-entry because `initStore` +rejects already-bound names. We declare all variables before the loops. +We use small bounds (1 iteration each) to keep heartbeat usage low while +still exercising the nesting semantics. +-/ + +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + var sum: int := 0; + var i: int := 0; + var j: int := 0; + while (i < 1) { + j := 0; + while (j < 1) { + sum := sum + 1; + j := j + 1 + }; + i := i + 1 + }; + return sum +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 11: Fuel exhaustion on infinite loop + +An infinite loop with no exit path. The loop body only assigns to an +existing variable, so it runs until fuel is exhausted. +-/ + +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + var x: int := 0; + while (true) { x := x + 1 }; + return 0 +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 12: Variable re-declaration inside loop body + +Declaring a variable inside a loop body causes `initStore` to reject the +re-declaration on the second iteration (the variable is already bound). +`evalProgram` returns `none`, which `runProgram` maps to `.fuelExhausted`. +This is a known limitation — not true fuel exhaustion. +-/ + +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + while (true) { var x: int := 0 }; + return 0 +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 13: Labeled block exit (break) + +Laurel concrete syntax does not have `break`/`continue` keywords. +Instead, `Exit` targets a labeled `Block`. We construct the AST +programmatically: a while(true) loop whose body increments x and +exits a labeled block wrapping the loop when x reaches 5. +-/ + +/-- +info: returned: 5 +-/ +#guard_msgs in +#eval! do + -- Build: procedure main() { + -- var x: int := 0; + -- { while (true) { x := x + 1; if (x == 5) { exit loopBlock } } } loopBlock; + -- return x + -- } + let xId : WithMetadata StmtExpr := ⟨.Identifier (mkId "x"), .empty⟩ + let varX := mk (.LocalVariable (mkId "x") ⟨.TInt, .empty⟩ (some ⟨.LiteralInt 0, .empty⟩)) + let incrX := mk (.Assign [xId] + ⟨.PrimitiveOp .Add [xId, ⟨.LiteralInt 1, .empty⟩], .empty⟩) + let exitBlock := mk (.Exit "loopBlock") + let guard := mk (.IfThenElse + ⟨.PrimitiveOp .Eq [xId, ⟨.LiteralInt 5, .empty⟩], .empty⟩ + ⟨.Block [exitBlock] none, .empty⟩ + none) + let whileLoop := mk (.While ⟨.LiteralBool true, .empty⟩ [] none + ⟨.Block [incrX, guard] none, .empty⟩) + let labeledBlock := mk (.Block [whileLoop] (some "loopBlock")) + let ret := mk (.Return (some xId)) + let body := StmtExpr.Block [varX, labeledBlock, ret] none + let proc := mkProc "main" [] body + let prog := mkProgram [proc] + IO.println (toString (runProgram prog)) + +end Strata.Laurel.ConcreteEval.ControlFlowTest diff --git a/StrataTest/Languages/Laurel/ConcreteEval/EdgeCases.lean b/StrataTest/Languages/Laurel/ConcreteEval/EdgeCases.lean new file mode 100644 index 000000000..88b54e19e --- /dev/null +++ b/StrataTest/Languages/Laurel/ConcreteEval/EdgeCases.lean @@ -0,0 +1,126 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import StrataTest.Languages.Laurel.ConcreteEval.TestHelper + +/-! +# Edge Case Tests + +Tests for missing main, opaque body, division by zero, uninitialized +variables, field access on non-ref, empty body, nonexistent callee, +and deeply nested blocks. +-/ + +namespace Strata.Laurel.ConcreteEval.EdgeCasesTest + +open Strata.Laurel.ConcreteEval.TestHelper +open Strata.Laurel + +/-! ## Test 1: No main procedure → noMain -/ + +/-- +info: error: no 'main' procedure found +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure notMain() { return 1 }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 2: Main with opaque body → noBody (programmatic AST) -/ + +/-- +info: error: 'main' has no body +-/ +#guard_msgs in +#eval! do + let proc : Procedure := { + name := mkId "main", inputs := [], outputs := [], + preconditions := [], determinism := .deterministic none, + isFunctional := false, decreases := none, + body := .Opaque [] none [], md := emd + } + let prog := mkProgram [proc] + IO.println (toString (runProgram prog)) + +/-! ## Test 3: Division by zero → stuck -/ + +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { return 1 / 0 }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 4: Uninitialized variable read → stuck (programmatic AST) + +Read a variable not in the store. The Identifier case returns none. +-/ + +#guard + let body := StmtExpr.Return (some (mk (.Identifier "ghost"))) + let prog := mkProgram [mkProc "main" [] body] + (evalProgram prog).isNone + +/-! ## Test 5: Field access on non-ref → stuck (programmatic AST) + +`FieldSelect (LiteralInt 5) "x"` — target is not a vRef, so FieldSelect +pattern match fails. +-/ + +#guard + let body := StmtExpr.Return (some (mk (.FieldSelect (mk (.LiteralInt 5)) "x"))) + let prog := mkProgram [mkProc "main" [] body] + (evalProgram prog).isNone + +/-! ## Test 6: Empty main body + +An empty block evaluates to `(.normal .vVoid)`, which `runProgram` maps +to `.success void`. The procedure does not return, so the outcome is +`success` (not `returned`). +-/ + +/-- +info: success: void +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 7: Procedure calling nonexistent procedure → stuck -/ + +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { return ghost() }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 8: Deeply nested blocks -/ + +/-- +info: returned: 42 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + if (true) { if (true) { if (true) { return 42 } } } +}; +" + IO.println (toString (runProgram prog)) + +end Strata.Laurel.ConcreteEval.EdgeCasesTest diff --git a/StrataTest/Languages/Laurel/ConcreteEval/HeapObjects.lean b/StrataTest/Languages/Laurel/ConcreteEval/HeapObjects.lean new file mode 100644 index 000000000..c710e076d --- /dev/null +++ b/StrataTest/Languages/Laurel/ConcreteEval/HeapObjects.lean @@ -0,0 +1,191 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import StrataTest.Languages.Laurel.ConcreteEval.TestHelper + +/-! +# Heap Object Semantics Tests + +Tests for object allocation, field read/write, multiple fields, multiple +objects, instance method calls, static fields, and field access on +unallocated addresses. +-/ + +namespace Strata.Laurel.ConcreteEval.HeapObjectsTest + +open Strata.Laurel.ConcreteEval.TestHelper +open Strata.Laurel + +/-! ## Test 1: New object allocation -/ + +/-- +info: returned: 0 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +composite Point { var x: int } +procedure main() { var p: Point := new Point; return 0 }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 2: Field write and read -/ + +/-- +info: returned: 42 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +composite Point { var x: int } +procedure main() { var p: Point := new Point; p#x := 42; return p#x }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 3: Multiple fields -/ + +/-- +info: returned: 3 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +composite Point { var x: int var y: int } +procedure main() { + var p: Point := new Point; p#x := 1; p#y := 2; + return p#x + p#y +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 4: Multiple objects on heap — no cross-contamination -/ + +/-- +info: returned: 30 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +composite Box { var v: int } +procedure main() { + var a: Box := new Box; a#v := 10; + var b: Box := new Box; b#v := 20; + return a#v + b#v +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 5: Instance method call — programmatic AST + +Parser does not support instance call syntax, so we build the AST directly. +Composite `Counter` with field `n` and method `get(this: Counter) { return this#n }`. +-/ + +#guard + let getBody := StmtExpr.Return (some (mk (.FieldSelect (mk (.This)) "n"))) + let getProc : Procedure := { + name := "get" + inputs := [⟨"this", ⟨.UserDefined "Counter", emd⟩⟩] + outputs := [] + preconditions := [] + determinism := .deterministic none + isFunctional := false + decreases := none + body := .Transparent (mk getBody) + md := emd + } + let counterType : TypeDefinition := .Composite { + name := "Counter" + extending := [] + fields := [{ name := "n", isMutable := true, type := ⟨.TInt, emd⟩ }] + instanceProcedures := [getProc] + } + let body := StmtExpr.Block [ + mk (.LocalVariable "c" ⟨.UserDefined "Counter", emd⟩ (some (mk (.New "Counter")))), + mk (.Assign [⟨.FieldSelect (mk (.Identifier "c")) "n", emd⟩] (mk (.LiteralInt 7))), + mk (.Return (some (mk (.InstanceCall (mk (.Identifier "c")) "get" [])))) + ] none + let prog : Program := { + staticProcedures := [mkProc "main" [] body] + staticFields := [] + types := [counterType] + constants := [] + } + getOutcome (evalProgram prog) = some (.ret (some (.vInt 7))) + +/-! ## Test 6: Instance method modifying fields — programmatic AST + +`Counter` with method `inc(this: Counter) { this#n := this#n + 1 }`. +Call `inc` twice, expect `n` = 2. +-/ + +#guard + let incBody := StmtExpr.Block [ + mk (.Assign [⟨.FieldSelect (mk (.This)) "n", emd⟩] + (mk (.PrimitiveOp .Add [⟨.FieldSelect (mk (.This)) "n", emd⟩, ⟨.LiteralInt 1, emd⟩]))) + ] none + let incProc : Procedure := { + name := "inc" + inputs := [⟨"this", ⟨.UserDefined "Counter", emd⟩⟩] + outputs := [] + preconditions := [] + determinism := .deterministic none + isFunctional := false + decreases := none + body := .Transparent (mk incBody) + md := emd + } + let counterType : TypeDefinition := .Composite { + name := "Counter" + extending := [] + fields := [{ name := "n", isMutable := true, type := ⟨.TInt, emd⟩ }] + instanceProcedures := [incProc] + } + let body := StmtExpr.Block [ + mk (.LocalVariable "c" ⟨.UserDefined "Counter", emd⟩ (some (mk (.New "Counter")))), + mk (.Assign [⟨.FieldSelect (mk (.Identifier "c")) "n", emd⟩] (mk (.LiteralInt 0))), + mk (.InstanceCall (mk (.Identifier "c")) "inc" []), + mk (.InstanceCall (mk (.Identifier "c")) "inc" []), + mk (.Return (some (mk (.FieldSelect (mk (.Identifier "c")) "n")))) + ] none + let prog : Program := { + staticProcedures := [mkProc "main" [] body] + staticFields := [] + types := [counterType] + constants := [] + } + getOutcome (evalProgram prog) = some (.ret (some (.vInt 2))) + +/-! ## Test 7: Static fields (global variables) — programmatic AST -/ + +#guard + let body := StmtExpr.Block [ + mk (.Assign [⟨.Identifier "counter", emd⟩] (mk (.LiteralInt 10))), + mk (.Return (some (mk (.Identifier "counter")))) + ] none + let prog : Program := { + staticProcedures := [mkProc "main" [] body] + staticFields := [{ name := "counter", isMutable := true, type := ⟨.TInt, emd⟩ }] + types := [] + constants := [] + } + getOutcome (evalProgram prog) = some (.ret (some (.vInt 10))) + +/-! ## Test 8: Field access on unallocated address → stuck — programmatic AST + +Use `interpStmt` directly with a store where `"x"` maps to `.vRef 999` and an +empty heap. `FieldSelect (Identifier "x") "f"` evaluates the target to +`.vRef 999`, then `heapFieldRead` returns `none` because address 999 was never +allocated. +-/ + +#guard + let σ : LaurelStore := fun x => if x == "x" then some (.vRef 999) else none + let h : LaurelHeap := fun _ => none + let expr := StmtExpr.FieldSelect (mk (.Identifier "x")) "f" + (interpStmt defaultEval (fun _ => none) 100 h σ expr).isNone + +end Strata.Laurel.ConcreteEval.HeapObjectsTest diff --git a/StrataTest/Languages/Laurel/ConcreteEval/Primitives.lean b/StrataTest/Languages/Laurel/ConcreteEval/Primitives.lean new file mode 100644 index 000000000..6d0605f2d --- /dev/null +++ b/StrataTest/Languages/Laurel/ConcreteEval/Primitives.lean @@ -0,0 +1,126 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import StrataTest.Languages.Laurel.ConcreteEval.TestHelper + +/-! +# Primitive Literal Tests + +Tests for integer literals (positive, negative, zero), boolean literals, +string literals, and void procedures. +-/ + +namespace Strata.Laurel.ConcreteEval.PrimitivesTest + +open Strata.Laurel.ConcreteEval.TestHelper +open Strata.Laurel + +/-! ## Test 1: Integer literal (positive) -/ + +/-- +info: returned: 42 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { return 42 }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 2: Integer literal (negative) -/ + +/-- +info: returned: -7 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { return -7 }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 3: Integer literal (zero) -/ + +/-- +info: returned: 0 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { return 0 }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 4: Boolean true -/ + +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + if (true) { return 1 } else { return 0 } +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 5: Boolean false -/ + +/-- +info: returned: 0 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + if (false) { return 1 } else { return 0 } +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 6: String literal — equality -/ + +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r#" +procedure main() { + if ("hello" == "hello") { return 1 } else { return 0 } +}; +"# + IO.println (toString (runProgram prog)) + +/-! ## Test 7: Empty string — equality -/ + +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r#" +procedure main() { + if ("" == "") { return 1 } else { return 0 } +}; +"# + IO.println (toString (runProgram prog)) + +/-! ## Test 8: Void — procedure with no return value -/ + +/-- +info: returned: 0 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure noop() { var x: int := 1 }; +procedure main() { noop(); return 0 }; +" + IO.println (toString (runProgram prog)) + +end Strata.Laurel.ConcreteEval.PrimitivesTest diff --git a/StrataTest/Languages/Laurel/ConcreteEval/Procedures.lean b/StrataTest/Languages/Laurel/ConcreteEval/Procedures.lean new file mode 100644 index 000000000..7bcbb051d --- /dev/null +++ b/StrataTest/Languages/Laurel/ConcreteEval/Procedures.lean @@ -0,0 +1,142 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import StrataTest.Languages.Laurel.ConcreteEval.TestHelper + +/-! +# Procedure Call Semantics Tests + +Tests for call-by-value semantics, shared heap behavior, parameter +reassignment, nested calls, and void returns. +-/ + +namespace Strata.Laurel.ConcreteEval.ProceduresTest + +open Strata.Laurel.ConcreteEval.TestHelper +open Strata.Laurel + +/-! ## Test 1: Call by value — primitive not modified in caller -/ + +/-- +info: returned: 5 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure inc(x: int) { x := x + 1; return x }; +procedure main() { var a: int := 5; var b: int := inc(a); return a }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 2: Shared heap — field mutation through passed ref is visible -/ + +/-- +info: returned: 42 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +composite Point { var x: int } +procedure setX(p: Point, v: int) { p#x := v }; +procedure main() { + var p: Point := new Point; p#x := 1; setX(p, 42); return p#x +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 3: Parameter reassignment — callee rebinding does not affect caller -/ + +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +composite Point { var x: int } +procedure replace(p: Point) { p := new Point; p#x := 99 }; +procedure main() { + var p: Point := new Point; p#x := 1; replace(p); return p#x +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 4: Simple return value from callee -/ + +/-- +info: returned: 42 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure double(x: int) { return x * 2 }; +procedure main() { return double(21) }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 5: Nested procedure calls -/ + +/-- +info: returned: 26 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure add(a: int, b: int) { return a + b }; +procedure mul(a: int, b: int) { return a * b }; +procedure main() { return add(mul(2, 3), mul(4, 5)) }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 6: Procedure modifying heap, caller reads updated heap -/ + +/-- +info: returned: 3 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +composite Counter { var n: int } +procedure increment(c: Counter) { c#n := c#n + 1 }; +procedure main() { + var c: Counter := new Counter; c#n := 0; + increment(c); increment(c); increment(c); + return c#n +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 7: Callee cannot see caller's locals -/ + +-- Note: "fuel exhausted" is reported because `readX()` looks up `x` in an +-- empty store (bindParams creates a fresh store for a zero-parameter procedure), +-- causing the evaluator to get stuck (returns `none`). `runProgram` maps any +-- `none` to `.fuelExhausted`, so stuck states and true fuel exhaustion are +-- indistinguishable in the output. +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure readX() { return x }; +procedure main() { var x: int := 42; return readX() }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 8: Procedure with no return — returns void -/ + +/-- +info: returned: 0 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure noop() { var x: int := 1 }; +procedure main() { noop(); return 0 }; +" + IO.println (toString (runProgram prog)) + +end Strata.Laurel.ConcreteEval.ProceduresTest diff --git a/StrataTest/Languages/Laurel/ConcreteEval/Recursion.lean b/StrataTest/Languages/Laurel/ConcreteEval/Recursion.lean new file mode 100644 index 000000000..5117f396f --- /dev/null +++ b/StrataTest/Languages/Laurel/ConcreteEval/Recursion.lean @@ -0,0 +1,112 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import StrataTest.Languages.Laurel.ConcreteEval.TestHelper + +/-! +# Recursion Semantics Tests + +Tests for simple recursion (factorial), mutual recursion (even/odd), +deep recursion (fuel exhaustion), recursion with heap effects, and fibonacci. +-/ + +namespace Strata.Laurel.ConcreteEval.RecursionTest + +open Strata.Laurel.ConcreteEval.TestHelper +open Strata.Laurel + +/-! ## Test 1: Simple recursion — factorial -/ + +/-- +info: returned: 120 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure fact(n: int) { + if (n <= 1) { return 1 } else { return n * fact(n - 1) } +}; +procedure main() { return fact(5) }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 2: Mutual recursion — even/odd -/ + +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure isEven(n: int) { + if (n == 0) { return true } else { return isOdd(n - 1) } +}; +procedure isOdd(n: int) { + if (n == 0) { return false } else { return isEven(n - 1) } +}; +procedure main() { if (isEven(4)) { return 1 } else { return 0 } }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 3: Deep recursion — fuel exhaustion + +Default fuel is 10000; `deep(100000)` exceeds it. +-/ + +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure deep(n: int) { + if (n == 0) { return 0 } else { return deep(n - 1) } +}; +procedure main() { return deep(100000) }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 4: Recursion with heap effects + +`fill(b, 5)` adds 5+4+3+2+1 = 15 to `b#v`. +-/ + +/-- +info: returned: 15 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +composite Box { var v: int } +procedure fill(b: Box, n: int) { + if (n <= 0) { return 0 } + else { b#v := b#v + n; return fill(b, n - 1) } +}; +procedure main() { + var b: Box := new Box; b#v := 0; + fill(b, 5); + return b#v +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 5: Fibonacci -/ + +/-- +info: returned: 55 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure fib(n: int) { + if (n <= 1) { return n } + else { return fib(n - 1) + fib(n - 2) } +}; +procedure main() { return fib(10) }; +" + IO.println (toString (runProgram prog)) + +end Strata.Laurel.ConcreteEval.RecursionTest diff --git a/StrataTest/Languages/Laurel/ConcreteEval/SideEffects.lean b/StrataTest/Languages/Laurel/ConcreteEval/SideEffects.lean new file mode 100644 index 000000000..e46564101 --- /dev/null +++ b/StrataTest/Languages/Laurel/ConcreteEval/SideEffects.lean @@ -0,0 +1,150 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import StrataTest.Languages.Laurel.ConcreteEval.TestHelper + +/-! +# Side Effects and Evaluation Order Tests + +Tests for side effects in expression position and left-to-right evaluation +order of arguments. The evaluation order is directly from `interpArgs`. + +The `interpArgs` function in `LaurelInterpreter.lean` evaluates arguments +left-to-right, threading store and heap through each argument evaluation. +These tests are prescriptive — they define the intended evaluation order. +-/ + +namespace Strata.Laurel.ConcreteEval.SideEffectsTest + +open Strata.Laurel.ConcreteEval.TestHelper +open Strata.Laurel + +/-! ## Test 1: Left-to-right argument evaluation order + +First arg: x becomes 1, evaluates to 1. +Second arg: x (now 1) becomes 1+10=11, evaluates to 11. +add(1, 11) = 12. +-/ + +/-- +info: returned: 12 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure add(a: int, b: int) { return a + b }; +procedure main() { + var x: int := 0; + return add({x := 1; x}, {x := x + 10; x}) +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 2: Assignment in argument position + +Side effect sets a=42, id returns 42, so b=42. a+b = 84. +-/ + +/-- +info: returned: 84 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure id(x: int) { return x }; +procedure main() { + var a: int := 0; + var b: int := id({a := 42; a}); + return a + b +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 3: Block expression as argument + +Block declares local t=10, evaluates to t+5=15. id(15) = 15. +-/ + +/-- +info: returned: 15 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure id(x: int) { return x }; +procedure main() { + return id({var t: int := 10; t + 5}) +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 4: Side effects in if condition + +Block in condition sets x=1 and evaluates to true (1==1). +Then-branch reads x=1, returns 1+10=11. +-/ + +/-- +info: returned: 11 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + var x: int := 0; + if ({x := 1; x == 1}) { return x + 10 } else { return x } +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 5: Side effects persist across loop iterations + +Each iteration: side effect adds 10 to x, id returns that value which is +assigned back. After 3 iterations: x = 30. + +This test uses side effects in call arguments inside the loop body. +-/ + +/-- +info: returned: 30 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure id(x: int) { return x }; +procedure main() { + var x: int := 0; + var i: int := 0; + while (i < 3) { + x := id({x := x + 10; x}); + i := i + 1 + }; + return x +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 6: Multiple side effects across nested calls + +Inner add: first arg: x=1*2=2, val=2; second arg: x=2+3=5, val=5; add(2,5)=7. +Outer add: first arg=7; second arg: x is now 5, val=5; add(7,5)=12. +-/ + +/-- +info: returned: 12 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure add(a: int, b: int) { return a + b }; +procedure main() { + var x: int := 1; + return add(add({x := x * 2; x}, {x := x + 3; x}), x) +}; +" + IO.println (toString (runProgram prog)) + +end Strata.Laurel.ConcreteEval.SideEffectsTest diff --git a/StrataTest/Languages/Laurel/ConcreteEval/TestHelper.lean b/StrataTest/Languages/Laurel/ConcreteEval/TestHelper.lean new file mode 100644 index 000000000..af559d9eb --- /dev/null +++ b/StrataTest/Languages/Laurel/ConcreteEval/TestHelper.lean @@ -0,0 +1,73 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.DDM.Elab +import Strata.DDM.BuiltinDialects.Init +import Strata.Languages.Laurel.Grammar.LaurelGrammar +import Strata.Languages.Laurel.Grammar.ConcreteToAbstractTreeTranslator +import Strata.Languages.Laurel.Resolution +import Strata.Languages.Laurel.LaurelConcreteEval +import Strata.Languages.Laurel.LaurelToCoreTranslator + +/-! +# Shared Test Helpers for Laurel ConcreteEval Tests + +Reusable `parseLaurel` helper and programmatic AST construction utilities +extracted from `LaurelConcreteEvalTest.lean`. +-/ + +namespace Strata.Laurel.ConcreteEval.TestHelper + +open Strata +open Strata.Elab (parseStrataProgramFromDialect) +open Strata.Laurel + +/-! ## Parsing Helper -/ + +def parseLaurel (input : String) : IO Laurel.Program := do + let inputCtx := Strata.Parser.stringInputContext "test" input + let dialects := Strata.Elab.LoadedDialects.ofDialects! #[initDialect, Laurel] + let strataProgram ← parseStrataProgramFromDialect dialects Laurel.name inputCtx + let uri := Strata.Uri.file "test" + match Laurel.TransM.run uri (Laurel.parseProgram strataProgram) with + | .error e => throw (IO.userError s!"Translation errors: {e}") + | .ok program => + let result := resolve program + return result.program + +/-- Parse and apply the full Laurel→Laurel lowering pipeline (all passes before Laurel→Core). -/ +def parseLaurelTransformed (input : String) : IO Laurel.Program := do + let inputCtx := Strata.Parser.stringInputContext "test" input + let dialects := Strata.Elab.LoadedDialects.ofDialects! #[initDialect, Laurel] + let strataProgram ← parseStrataProgramFromDialect dialects Laurel.name inputCtx + let uri := Strata.Uri.file "test" + match Laurel.TransM.run uri (Laurel.parseProgram strataProgram) with + | .error e => throw (IO.userError s!"Translation errors: {e}") + | .ok program => + let (result, _) := lowerLaurelToLaurel program + return result.program + +/-! ## Programmatic AST Helpers -/ + +abbrev emd : Imperative.MetaData Core.Expression := .empty +def mk (s : StmtExpr) : StmtExprMd := ⟨s, emd⟩ + +def mkProc (name : String) (inputs : List Parameter := []) + (body : StmtExpr) : Procedure := + { name := mkId name, inputs := inputs, outputs := [], + preconditions := [], determinism := .deterministic none, + isFunctional := false, decreases := none, + body := .Transparent (mk body), md := emd } + +def mkProgram (procs : List Procedure) : Program := + { staticProcedures := procs, staticFields := [], types := [], constants := [] } + +/-! ## Outcome Helper -/ + +def getOutcome (r : Option (Outcome × LaurelStore × LaurelHeap)) : Option Outcome := + r.map (·.1) + +end Strata.Laurel.ConcreteEval.TestHelper diff --git a/StrataTest/Languages/Laurel/ConcreteEval/TransformPreservation.lean b/StrataTest/Languages/Laurel/ConcreteEval/TransformPreservation.lean new file mode 100644 index 000000000..b14521463 --- /dev/null +++ b/StrataTest/Languages/Laurel/ConcreteEval/TransformPreservation.lean @@ -0,0 +1,1361 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import StrataTest.Languages.Laurel.ConcreteEval.TestHelper + +/-! +# Transform Preservation Tests + +Runs every string-based ConcreteEval test after the full +Laurel→Laurel lowering pipeline from LaurelToCoreTranslator.translate. + +TODO: find a way to not duplicate the test cases and their expected results + +## Status +- Passing: 82 / 94 tests (output matches direct mode) +- Failing: 12 / 94 tests (output differs from direct mode) + +## Known failure categories +- heapParameterization (12 tests): all tests using composite types / heap + objects fail because the evaluator does not handle heap-parameterized + programs (field accesses become map select/store operations). +-/ + +namespace Strata.Laurel.ConcreteEval.TransformPreservationTest + +open Strata.Laurel.ConcreteEval.TestHelper +open Strata.Laurel + +/-! ## Primitives -/ + +/-! ### Primitives Test 1: Integer literal (positive) -/ +/-- +info: returned: 42 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { return 42 }; +" + IO.println (toString (runProgram prog)) + +/-! ### Primitives Test 2: Integer literal (negative) -/ +/-- +info: returned: -7 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { return -7 }; +" + IO.println (toString (runProgram prog)) + +/-! ### Primitives Test 3: Integer literal (zero) -/ +/-- +info: returned: 0 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { return 0 }; +" + IO.println (toString (runProgram prog)) + +/-! ### Primitives Test 4: Boolean true -/ +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { + if (true) { return 1 } else { return 0 } +}; +" + IO.println (toString (runProgram prog)) + +/-! ### Primitives Test 5: Boolean false -/ +/-- +info: returned: 0 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { + if (false) { return 1 } else { return 0 } +}; +" + IO.println (toString (runProgram prog)) + +/-! ### Primitives Test 6: String literal equality -/ +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r#" +procedure main() { + if ("hello" == "hello") { return 1 } else { return 0 } +}; +"# + IO.println (toString (runProgram prog)) + +/-! ### Primitives Test 7: Empty string equality -/ +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r#" +procedure main() { + if ("" == "") { return 1 } else { return 0 } +}; +"# + IO.println (toString (runProgram prog)) + +/-! ### Primitives Test 8: Void procedure -/ +/-- +info: returned: 0 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure noop() { var x: int := 1 }; +procedure main() { noop(); return 0 }; +" + IO.println (toString (runProgram prog)) + +/-! ## Arithmetic -/ + +/-! ### Arithmetic Test 1: Addition -/ +/-- +info: returned: 7 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { return 3 + 4 }; +" + IO.println (toString (runProgram prog)) + +/-! ### Arithmetic Test 2: Subtraction -/ +/-- +info: returned: 7 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { return 10 - 3 }; +" + IO.println (toString (runProgram prog)) + +/-! ### Arithmetic Test 3: Multiplication -/ +/-- +info: returned: 42 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { return 6 * 7 }; +" + IO.println (toString (runProgram prog)) + +/-! ### Arithmetic Test 4: Euclidean division -/ +/-- +info: returned: 3 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { return 7 / 2 }; +" + IO.println (toString (runProgram prog)) + +/-! ### Arithmetic Test 5: Euclidean modulus -/ +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { return 7 % 2 }; +" + IO.println (toString (runProgram prog)) + +/-! ### Arithmetic Test 6: Negation via subtraction -/ +/-- +info: returned: -5 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { return 0 - 5 }; +" + IO.println (toString (runProgram prog)) + +/-! ### Arithmetic Test 7: Division by zero — stuck -/ +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { return 1 / 0 }; +" + IO.println (toString (runProgram prog)) + +/-! ### Arithmetic Test 8: Modulus by zero — stuck -/ +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { return 1 % 0 }; +" + IO.println (toString (runProgram prog)) + +/-! ### Arithmetic Test 9: Large integers -/ +/-- +info: returned: 1000000000000000000 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { return 1000000000 * 1000000000 }; +" + IO.println (toString (runProgram prog)) + +/-! ### Arithmetic Test 10: Compound expression -/ +/-- +info: returned: 15 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { return (2 + 3) * (4 - 1) }; +" + IO.println (toString (runProgram prog)) + +/-! ### Arithmetic Test 11: Negative arithmetic -/ +/-- +info: returned: -7 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { return (-3) + (-4) }; +" + IO.println (toString (runProgram prog)) + +/-! ### Arithmetic Test 12: DivT -/ +/-- +info: returned: 3 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { return 7 /t 2 }; +" + IO.println (toString (runProgram prog)) + +/-! ### Arithmetic Test 13: ModT -/ +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { return 7 %t 2 }; +" + IO.println (toString (runProgram prog)) + +/-! ### Arithmetic Test 14: DivT with negative dividend -/ +/-- +info: returned: -3 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { return (-7) /t 2 }; +" + IO.println (toString (runProgram prog)) + +/-! ### Arithmetic Test 15: ModT with negative dividend -/ +/-- +info: returned: -1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { return (-7) %t 2 }; +" + IO.println (toString (runProgram prog)) + +/-! ### Arithmetic Test 16: DivT by zero — stuck -/ +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { return 7 /t 0 }; +" + IO.println (toString (runProgram prog)) + +/-! ### Arithmetic Test 17: ModT by zero — stuck -/ +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { return 7 %t 0 }; +" + IO.println (toString (runProgram prog)) + +/-! ## BooleanOps -/ + +/-! ### BooleanOps Test 1: Comparison operators -/ +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { + var a: bool := 1 < 2; + var b: bool := 2 <= 2; + var c: bool := 3 > 2; + var d: bool := 2 >= 2; + if (a && b && c && d) { return 1 } else { return 0 } +}; +" + IO.println (toString (runProgram prog)) + +/-! ### BooleanOps Test 2: Eq and Neq on integers -/ +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { + if (5 == 5 && 5 != 6) { return 1 } else { return 0 } +}; +" + IO.println (toString (runProgram prog)) + +/-! ### BooleanOps Test 3: Eq and Neq on booleans -/ +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { + if (true == true && true != false) { return 1 } else { return 0 } +}; +" + IO.println (toString (runProgram prog)) + +/-! ### BooleanOps Test 4: Eq and Neq on strings -/ +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r#" +procedure main() { + if ("abc" == "abc" && "abc" != "def") { return 1 } else { return 0 } +}; +"# + IO.println (toString (runProgram prog)) + +/-! ### BooleanOps Test 5: Not operator -/ +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { + if (!false && !(!true)) { return 1 } else { return 0 } +}; +" + IO.println (toString (runProgram prog)) + +/-! ### BooleanOps Test 6: String concatenation -/ +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r#" +procedure main() { + if ("ab" ++ "cd" == "abcd") { return 1 } else { return 0 } +}; +"# + IO.println (toString (runProgram prog)) + +/-! ### BooleanOps Test 7: Short-circuit And — false && side-effect -/ +/-- +info: returned: 0 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { + var x: int := 0; + var b: bool := false && {x := 1; true}; + return x +}; +" + IO.println (toString (runProgram prog)) + +/-! ### BooleanOps Test 8: Short-circuit And — true && side-effect -/ +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { + var x: int := 0; + var b: bool := true && {x := 1; true}; + return x +}; +" + IO.println (toString (runProgram prog)) + +/-! ### BooleanOps Test 9: Nested short-circuit And -/ +/-- +info: returned: 0 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { + var x: int := 0; + var b: bool := false && (true && {x := 1; true}); + return x +}; +" + IO.println (toString (runProgram prog)) + +/-! ### BooleanOps Test 10: Short-circuit Or — true || side-effect -/ +/-- +info: returned: 0 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { + var x: int := 0; + var b: bool := true || {x := 1; false}; + return x +}; +" + IO.println (toString (runProgram prog)) + +/-! ### BooleanOps Test 11: Short-circuit Or — false || side-effect -/ +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { + var x: int := 0; + var b: bool := false || {x := 1; true}; + return x +}; +" + IO.println (toString (runProgram prog)) + +/-! ### BooleanOps Test 12: Nested short-circuit Or -/ +/-- +info: returned: 0 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { + var x: int := 0; + var b: bool := true || (false || {x := 1; true}); + return x +}; +" + IO.println (toString (runProgram prog)) + +/-! ### BooleanOps Test 13: Short-circuit Implies — false ==> side-effect -/ +/-- +info: returned: 0 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { + var x: int := 0; + var b: bool := false ==> {x := 1; false}; + return x +}; +" + IO.println (toString (runProgram prog)) + +/-! ### BooleanOps Test 14: Short-circuit Implies — true ==> side-effect -/ +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { + var x: int := 0; + var b: bool := true ==> {x := 1; true}; + return x +}; +" + IO.println (toString (runProgram prog)) + +/-! ### BooleanOps Test 15: Mixed short-circuit — FAILS after transforms +liftExpressionAssignments changes nested short-circuit with side effects. +The lifted code introduces temporary variables that break the evaluator. +TODO: Extend evaluator to handle lifted expression assignments. +-/ +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { + var x: int := 0; + var b: bool := (true || {x := x + 1; true}) && (false || {x := x + 10; true}); + return x +}; +" + IO.println (toString (runProgram prog)) + +/-! ## ControlFlow -/ + +/-! ### ControlFlow Test 1: If-then-else, true branch -/ +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { + if (true) { return 1 } else { return 2 } +}; +" + IO.println (toString (runProgram prog)) + +/-! ### ControlFlow Test 2: If-then-else, false branch -/ +/-- +info: returned: 2 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { + if (false) { return 1 } else { return 2 } +}; +" + IO.println (toString (runProgram prog)) + +/-! ### ControlFlow Test 3: If-then without else (true) -/ +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { + if (true) { return 1 }; + return 0 +}; +" + IO.println (toString (runProgram prog)) + +/-! ### ControlFlow Test 4: If-then without else (false) -/ +/-- +info: returned: 0 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { + var x: int := 0; + if (false) { x := 1 }; + return x +}; +" + IO.println (toString (runProgram prog)) + +/-! ### ControlFlow Test 5: Nested if-then-else -/ +/-- +info: returned: 2 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { + var x: int := 15; + if (x > 10) { + if (x > 20) { return 3 } else { return 2 } + } else { return 1 } +}; +" + IO.println (toString (runProgram prog)) + +/-! ### ControlFlow Test 6: While loop — zero iterations -/ +/-- +info: returned: 0 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { + var x: int := 0; + while (false) { x := 1 }; + return x +}; +" + IO.println (toString (runProgram prog)) + +/-! ### ControlFlow Test 7: While loop — single iteration -/ +/-- +info: returned: 42 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { + var x: int := 0; + var done: bool := false; + while (!done) { x := 42; done := true }; + return x +}; +" + IO.println (toString (runProgram prog)) + +/-! ### ControlFlow Test 8: While loop with early return -/ +/-- +info: returned: 5 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { + var i: int := 0; + while (i < 100) { + if (i == 5) { return i }; + i := i + 1 + }; + return -1 +}; +" + IO.println (toString (runProgram prog)) + +/-! ### ControlFlow Test 9: Return from nested blocks -/ +/-- +info: returned: 42 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { + var x: int := 0; + if (true) { + if (true) { + return 42 + } + }; + return 0 +}; +" + IO.println (toString (runProgram prog)) + +/-! ### ControlFlow Test 10: Nested while loops -/ +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { + var sum: int := 0; + var i: int := 0; + var j: int := 0; + while (i < 1) { + j := 0; + while (j < 1) { + sum := sum + 1; + j := j + 1 + }; + i := i + 1 + }; + return sum +}; +" + IO.println (toString (runProgram prog)) + +/-! ### ControlFlow Test 11: Fuel exhaustion on infinite loop -/ +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { + var x: int := 0; + while (true) { x := x + 1 }; + return 0 +}; +" + IO.println (toString (runProgram prog)) + +/-! ### ControlFlow Test 12: Variable re-declaration inside loop body -/ +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { + while (true) { var x: int := 0 }; + return 0 +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Variables -/ + +/-! ### Variables Test 1: Local var with initializer -/ +/-- +info: returned: 5 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { var x: int := 5; return x }; +" + IO.println (toString (runProgram prog)) + +/-! ### Variables Test 2: Local var without initializer -/ +/-- +info: returned: 0 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { var x: int; return 0 }; +" + IO.println (toString (runProgram prog)) + +/-! ### Variables Test 3: Block expression returns last value -/ +/-- +info: returned: 42 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { var x: int := 0; return {x := 42; x} }; +" + IO.println (toString (runProgram prog)) + +/-! ### Variables Test 4: Multiple assignments -/ +/-- +info: returned: 3 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { var x: int := 1; x := 2; x := 3; return x }; +" + IO.println (toString (runProgram prog)) + +/-! ### Variables Test 5: Variable scoping -/ +/-- +info: returned: 3 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { + var x: int := 1; + if (true) { var y: int := 2; x := x + y }; + return x +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Procedures -/ + +/-! ### Procedures Test 1: Call by value -/ +/-- +info: returned: 5 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure inc(x: int) { x := x + 1; return x }; +procedure main() { var a: int := 5; var b: int := inc(a); return a }; +" + IO.println (toString (runProgram prog)) + +/-! ### Procedures Test 2: Shared heap — FAILS after transforms +heapParameterization changes calling convention for heap objects. +TODO: Extend evaluator to handle heap-parameterized programs. +-/ +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +composite Point { var x: int } +procedure setX(p: Point, v: int) { p#x := v }; +procedure main() { + var p: Point := new Point; p#x := 1; setX(p, 42); return p#x +}; +" + IO.println (toString (runProgram prog)) + +/-! ### Procedures Test 3: Parameter reassignment — FAILS after transforms +heapParameterization changes calling convention for heap objects. +-/ +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +composite Point { var x: int } +procedure replace(p: Point) { p := new Point; p#x := 99 }; +procedure main() { + var p: Point := new Point; p#x := 1; replace(p); return p#x +}; +" + IO.println (toString (runProgram prog)) + +/-! ### Procedures Test 4: Simple return value -/ +/-- +info: returned: 42 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure double(x: int) { return x * 2 }; +procedure main() { return double(21) }; +" + IO.println (toString (runProgram prog)) + +/-! ### Procedures Test 5: Nested procedure calls -/ +/-- +info: returned: 26 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure add(a: int, b: int) { return a + b }; +procedure mul(a: int, b: int) { return a * b }; +procedure main() { return add(mul(2, 3), mul(4, 5)) }; +" + IO.println (toString (runProgram prog)) + +/-! ### Procedures Test 6: Procedure modifying heap — FAILS after transforms +heapParameterization changes calling convention for heap objects. +-/ +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +composite Counter { var n: int } +procedure increment(c: Counter) { c#n := c#n + 1 }; +procedure main() { + var c: Counter := new Counter; c#n := 0; + increment(c); increment(c); increment(c); + return c#n +}; +" + IO.println (toString (runProgram prog)) + +/-! ### Procedures Test 7: Callee cannot see caller's locals -/ +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure readX() { return x }; +procedure main() { var x: int := 42; return readX() }; +" + IO.println (toString (runProgram prog)) + +/-! ### Procedures Test 8: Void procedure -/ +/-- +info: returned: 0 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure noop() { var x: int := 1 }; +procedure main() { noop(); return 0 }; +" + IO.println (toString (runProgram prog)) + +/-! ## SideEffects -/ + +/-! ### SideEffects Test 1: Left-to-right argument evaluation -/ +/-- +info: returned: 12 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure add(a: int, b: int) { return a + b }; +procedure main() { + var x: int := 0; + return add({x := 1; x}, {x := x + 10; x}) +}; +" + IO.println (toString (runProgram prog)) + +/-! ### SideEffects Test 2: Assignment in argument position -/ +/-- +info: returned: 84 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure id(x: int) { return x }; +procedure main() { + var a: int := 0; + var b: int := id({a := 42; a}); + return a + b +}; +" + IO.println (toString (runProgram prog)) + +/-! ### SideEffects Test 3: Block expression as argument -/ +/-- +info: returned: 15 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure id(x: int) { return x }; +procedure main() { + return id({var t: int := 10; t + 5}) +}; +" + IO.println (toString (runProgram prog)) + +/-! ### SideEffects Test 4: Side effects in if condition -/ +/-- +info: returned: 11 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { + var x: int := 0; + if ({x := 1; x == 1}) { return x + 10 } else { return x } +}; +" + IO.println (toString (runProgram prog)) + +/-! ### SideEffects Test 5: Side effects persist across loop iterations -/ +/-- +info: returned: 30 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure id(x: int) { return x }; +procedure main() { + var x: int := 0; + var i: int := 0; + while (i < 3) { + x := id({x := x + 10; x}); + i := i + 1 + }; + return x +}; +" + IO.println (toString (runProgram prog)) + +/-! ### SideEffects Test 6: Nested calls with side effects -/ +/-- +info: returned: 12 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure add(a: int, b: int) { return a + b }; +procedure main() { + var x: int := 1; + return add(add({x := x * 2; x}, {x := x + 3; x}), x) +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Recursion -/ + +/-! ### Recursion Test 1: Factorial -/ +/-- +info: returned: 120 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure fact(n: int) { + if (n <= 1) { return 1 } else { return n * fact(n - 1) } +}; +procedure main() { return fact(5) }; +" + IO.println (toString (runProgram prog)) + +/-! ### Recursion Test 2: Mutual recursion — even/odd -/ +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure isEven(n: int) { + if (n == 0) { return true } else { return isOdd(n - 1) } +}; +procedure isOdd(n: int) { + if (n == 0) { return false } else { return isEven(n - 1) } +}; +procedure main() { if (isEven(4)) { return 1 } else { return 0 } }; +" + IO.println (toString (runProgram prog)) + +/-! ### Recursion Test 3: Deep recursion — fuel exhaustion -/ +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure deep(n: int) { + if (n == 0) { return 0 } else { return deep(n - 1) } +}; +procedure main() { return deep(100000) }; +" + IO.println (toString (runProgram prog)) + +/-! ### Recursion Test 4: Recursion with heap effects — FAILS after transforms +heapParameterization changes calling convention for heap objects. +-/ +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +composite Box { var v: int } +procedure fill(b: Box, n: int) { + if (n <= 0) { return 0 } + else { b#v := b#v + n; return fill(b, n - 1) } +}; +procedure main() { + var b: Box := new Box; b#v := 0; + fill(b, 5); + return b#v +}; +" + IO.println (toString (runProgram prog)) + +/-! ### Recursion Test 5: Fibonacci -/ +/-- +info: returned: 55 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure fib(n: int) { + if (n <= 1) { return n } + else { return fib(n - 1) + fib(n - 2) } +}; +procedure main() { return fib(10) }; +" + IO.println (toString (runProgram prog)) + +/-! ## Aliasing -/ + +/-! ### Aliasing Test 1: Simple aliasing — FAILS after transforms +heapParameterization changes calling convention for heap objects. +-/ +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +composite Point { var x: int } +procedure main() { + var p: Point := new Point; p#x := 1; + var q: Point := p; + q#x := 42; + return p#x +}; +" + IO.println (toString (runProgram prog)) + +/-! ### Aliasing Test 2: Aliasing through procedure call — FAILS after transforms +heapParameterization changes calling convention for heap objects. +-/ +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +composite Box { var v: int } +procedure swap(a: Box, b: Box) { + var tmp: int := a#v; a#v := b#v; b#v := tmp +}; +procedure main() { + var b: Box := new Box; b#v := 5; + swap(b, b); + return b#v +}; +" + IO.println (toString (runProgram prog)) + +/-! ### Aliasing Test 3: Distinct objects — FAILS after transforms +heapParameterization changes calling convention for heap objects. +-/ +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +composite Point { var x: int } +procedure main() { + var p: Point := new Point; p#x := 1; + var q: Point := new Point; q#x := 2; + p#x := 99; + return q#x +}; +" + IO.println (toString (runProgram prog)) + +/-! ### Aliasing Test 4: Alias survives procedure call — FAILS after transforms +heapParameterization changes calling convention for heap objects. +-/ +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +composite Box { var v: int } +procedure setV(b: Box, x: int) { b#v := x }; +procedure main() { + var a: Box := new Box; a#v := 0; + var b: Box := a; + setV(a, 42); + return b#v +}; +" + IO.println (toString (runProgram prog)) + +/-! ## HeapObjects -/ + +/-! ### HeapObjects Test 1: New object allocation — FAILS after transforms +heapParameterization changes calling convention for heap objects. +-/ +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +composite Point { var x: int } +procedure main() { var p: Point := new Point; return 0 }; +" + IO.println (toString (runProgram prog)) + +/-! ### HeapObjects Test 2: Field write and read — FAILS after transforms +heapParameterization changes calling convention for heap objects. +-/ +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +composite Point { var x: int } +procedure main() { var p: Point := new Point; p#x := 42; return p#x }; +" + IO.println (toString (runProgram prog)) + +/-! ### HeapObjects Test 3: Multiple fields — FAILS after transforms +heapParameterization changes calling convention for heap objects. +-/ +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +composite Point { var x: int var y: int } +procedure main() { + var p: Point := new Point; p#x := 1; p#y := 2; + return p#x + p#y +}; +" + IO.println (toString (runProgram prog)) + +/-! ### HeapObjects Test 4: Multiple objects — FAILS after transforms +heapParameterization changes calling convention for heap objects. +-/ +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +composite Box { var v: int } +procedure main() { + var a: Box := new Box; a#v := 10; + var b: Box := new Box; b#v := 20; + return a#v + b#v +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Verification -/ + +/-! ### Verification Test 1: Assert true -/ +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { assert true; return 1 }; +" + IO.println (toString (runProgram prog)) + +/-! ### Verification Test 2: Assert false — stuck -/ +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { assert false; return 1 }; +" + IO.println (toString (runProgram prog)) + +/-! ### Verification Test 3: Assume true -/ +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { assume true; return 1 }; +" + IO.println (toString (runProgram prog)) + +/-! ### Verification Test 4: Assume false — stuck -/ +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { assume false; return 1 }; +" + IO.println (toString (runProgram prog)) + +/-! ### Verification Test 5: Assert purity -/ +/-- +info: returned: 0 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { + var x: int := 0; + assert {x := 1; true}; + return x +}; +" + IO.println (toString (runProgram prog)) + +/-! ## EdgeCases -/ + +/-! ### EdgeCases Test 1: No main procedure -/ +/-- +info: error: no 'main' procedure found +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure notMain() { return 1 }; +" + IO.println (toString (runProgram prog)) + +/-! ### EdgeCases Test 3: Division by zero -/ +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { return 1 / 0 }; +" + IO.println (toString (runProgram prog)) + +/-! ### EdgeCases Test 6: Empty main body -/ +/-- +info: success: void +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { }; +" + IO.println (toString (runProgram prog)) + +/-! ### EdgeCases Test 7: Nonexistent callee -/ +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { return ghost() }; +" + IO.println (toString (runProgram prog)) + +/-! ### EdgeCases Test 8: Deeply nested blocks -/ +/-- +info: returned: 42 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurelTransformed r" +procedure main() { + if (true) { if (true) { if (true) { return 42 } } } +}; +" + IO.println (toString (runProgram prog)) + +end Strata.Laurel.ConcreteEval.TransformPreservationTest diff --git a/StrataTest/Languages/Laurel/ConcreteEval/TypeOps.lean b/StrataTest/Languages/Laurel/ConcreteEval/TypeOps.lean new file mode 100644 index 000000000..8600fc900 --- /dev/null +++ b/StrataTest/Languages/Laurel/ConcreteEval/TypeOps.lean @@ -0,0 +1,113 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import StrataTest.Languages.Laurel.ConcreteEval.TestHelper + +/-! +# Type Operation Tests + +Tests for IsType, AsType, and ReferenceEquals — all programmatic AST +since these constructs have no concrete syntax. +-/ + +namespace Strata.Laurel.ConcreteEval.TypeOpsTest + +open Strata.Laurel.ConcreteEval.TestHelper +open Strata.Laurel + +/-! ## Test 1: IsType — correct type → true + +Allocate a Point object, check `IsType target "Point"`. +-/ + +#guard + let body := StmtExpr.Block [ + mk (.LocalVariable "p" ⟨.UserDefined "Point", emd⟩ (some (mk (.New "Point")))), + mk (.Return (some (mk (.IsType (mk (.Identifier "p")) ⟨.UserDefined "Point", emd⟩)))) + ] none + let pointType : TypeDefinition := .Composite { + name := "Point", extending := [], fields := [], instanceProcedures := [] + } + let prog : Program := { + staticProcedures := [mkProc "main" [] body] + staticFields := [], types := [pointType], constants := [] + } + getOutcome (evalProgram prog) = some (.ret (some (.vBool true))) + +/-! ## Test 2: IsType — wrong type → false + +Allocate a Point object, check `IsType target "Box"`. +-/ + +#guard + let body := StmtExpr.Block [ + mk (.LocalVariable "p" ⟨.UserDefined "Point", emd⟩ (some (mk (.New "Point")))), + mk (.Return (some (mk (.IsType (mk (.Identifier "p")) ⟨.UserDefined "Box", emd⟩)))) + ] none + let pointType : TypeDefinition := .Composite { + name := "Point", extending := [], fields := [], instanceProcedures := [] + } + let prog : Program := { + staticProcedures := [mkProc "main" [] body] + staticFields := [], types := [pointType], constants := [] + } + getOutcome (evalProgram prog) = some (.ret (some (.vBool false))) + +/-! ## Test 3: AsType — identity cast + +`AsType (vRef addr) someType` returns the same `vRef addr`. +-/ + +#guard + let body := StmtExpr.Block [ + mk (.LocalVariable "p" ⟨.UserDefined "Point", emd⟩ (some (mk (.New "Point")))), + mk (.Return (some (mk (.AsType (mk (.Identifier "p")) ⟨.UserDefined "Point", emd⟩)))) + ] none + let pointType : TypeDefinition := .Composite { + name := "Point", extending := [], fields := [], instanceProcedures := [] + } + let prog : Program := { + staticProcedures := [mkProc "main" [] body] + staticFields := [], types := [pointType], constants := [] + } + -- AsType returns the value unchanged; the ref address is 0 (first allocation) + getOutcome (evalProgram prog) = some (.ret (some (.vRef 0))) + +/-! ## Test 4: ReferenceEquals — same object → true, different objects → false -/ + +#guard + let body := StmtExpr.Block [ + mk (.LocalVariable "a" ⟨.UserDefined "Point", emd⟩ (some (mk (.New "Point")))), + mk (.LocalVariable "b" ⟨.UserDefined "Point", emd⟩ (some (mk (.New "Point")))), + -- same ref: a === a → true + mk (.Return (some (mk (.ReferenceEquals (mk (.Identifier "a")) (mk (.Identifier "a")))))) + ] none + let pointType : TypeDefinition := .Composite { + name := "Point", extending := [], fields := [], instanceProcedures := [] + } + let prog : Program := { + staticProcedures := [mkProc "main" [] body] + staticFields := [], types := [pointType], constants := [] + } + getOutcome (evalProgram prog) = some (.ret (some (.vBool true))) + +-- different refs: a === b → false +#guard + let body := StmtExpr.Block [ + mk (.LocalVariable "a" ⟨.UserDefined "Point", emd⟩ (some (mk (.New "Point")))), + mk (.LocalVariable "b" ⟨.UserDefined "Point", emd⟩ (some (mk (.New "Point")))), + mk (.Return (some (mk (.ReferenceEquals (mk (.Identifier "a")) (mk (.Identifier "b")))))) + ] none + let pointType : TypeDefinition := .Composite { + name := "Point", extending := [], fields := [], instanceProcedures := [] + } + let prog : Program := { + staticProcedures := [mkProc "main" [] body] + staticFields := [], types := [pointType], constants := [] + } + getOutcome (evalProgram prog) = some (.ret (some (.vBool false))) + +end Strata.Laurel.ConcreteEval.TypeOpsTest diff --git a/StrataTest/Languages/Laurel/ConcreteEval/Variables.lean b/StrataTest/Languages/Laurel/ConcreteEval/Variables.lean new file mode 100644 index 000000000..3a53b9a67 --- /dev/null +++ b/StrataTest/Languages/Laurel/ConcreteEval/Variables.lean @@ -0,0 +1,100 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import StrataTest.Languages.Laurel.ConcreteEval.TestHelper + +/-! +# Variable Semantics Tests + +Tests for local variable declaration (with/without initializer), assignment, +multiple assignments, variable scoping, and uninitialized variable reads. +-/ + +namespace Strata.Laurel.ConcreteEval.VariablesTest + +open Strata.Laurel.ConcreteEval.TestHelper +open Strata.Laurel + +/-! ## Test 1: Local var with initializer -/ + +/-- +info: returned: 5 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { var x: int := 5; return x }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 2: Local var without initializer — x is vVoid but never read -/ + +/-- +info: returned: 0 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { var x: int; return 0 }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 3: Block expression returns last value after side effects -/ + +/-- +info: returned: 42 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { var x: int := 0; return {x := 42; x} }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 4: Multiple assignments -/ + +/-- +info: returned: 3 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { var x: int := 1; x := 2; x := 3; return x }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 5: Variable scoping — inner block variable -/ + +/-- +info: returned: 3 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + var x: int := 1; + if (true) { var y: int := 2; x := x + y }; + return x +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 6: Uninitialized variable read → stuck + +Programmatic AST: read a variable that was never declared. +The evaluator returns `none` (stuck), which `runProgram` maps to `.fuelExhausted`. +-/ + +#guard + let body := StmtExpr.Block [ + mk (.Return (some (mk (.Identifier "undeclared")))) + ] none + let prog := mkProgram [mkProc "main" [] body] + match runProgram prog with + | .fuelExhausted => true + | _ => false + +end Strata.Laurel.ConcreteEval.VariablesTest diff --git a/StrataTest/Languages/Laurel/ConcreteEval/Verification.lean b/StrataTest/Languages/Laurel/ConcreteEval/Verification.lean new file mode 100644 index 000000000..0bf10d0c8 --- /dev/null +++ b/StrataTest/Languages/Laurel/ConcreteEval/Verification.lean @@ -0,0 +1,96 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import StrataTest.Languages.Laurel.ConcreteEval.TestHelper + +/-! +# Verification Construct Tests + +Tests for assert, assume, assert/assume purity, and ProveBy semantics. +-/ + +namespace Strata.Laurel.ConcreteEval.VerificationTest + +open Strata.Laurel.ConcreteEval.TestHelper +open Strata.Laurel + +/-! ## Test 1: Assert true → succeeds -/ + +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { assert true; return 1 }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 2: Assert false → stuck -/ + +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { assert false; return 1 }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 3: Assume true → succeeds -/ + +/-- +info: returned: 1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { assume true; return 1 }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 4: Assume false → stuck -/ + +/-- +info: error: fuel exhausted +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { assume false; return 1 }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 5: Assert purity — side effects in condition discarded + +The semantics evaluates the condition but returns the original σ and h. +The interpreter handles the impure expression `{x := 1; true}` +natively. After assert, x should still be 0. +-/ + +/-- +info: returned: 0 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + var x: int := 0; + assert {x := 1; true}; + return x +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 6: ProveBy — semantics of value, proof ignored (programmatic AST) -/ + +#guard + let body := StmtExpr.Return (some (mk (.ProveBy (mk (.LiteralInt 42)) (mk (.LiteralBool true))))) + let prog := mkProgram [mkProc "main" [] body] + getOutcome (evalProgram prog) = some (.ret (some (.vInt 42))) + +end Strata.Laurel.ConcreteEval.VerificationTest diff --git a/StrataTest/Languages/Laurel/LaurelConcreteEvalTest.lean b/StrataTest/Languages/Laurel/LaurelConcreteEvalTest.lean new file mode 100644 index 000000000..f8c4a30b5 --- /dev/null +++ b/StrataTest/Languages/Laurel/LaurelConcreteEvalTest.lean @@ -0,0 +1,293 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import StrataTest.Languages.Laurel.ConcreteEval.TestHelper + +/-! +# Tests for Laurel Concrete Program Evaluator + +Tests that `evalProgram` and `runProgram` correctly wire up `interpStmt` +for whole `Laurel.Program` values. + +Tests 1–8 use the Laurel parser to build programs from source strings. +Tests 9–13 use programmatic AST construction for internal API features +that cannot be expressed in Laurel concrete syntax. +-/ + +namespace Strata.Laurel.ConcreteEvalTest + +open Strata +open Strata.Laurel +open Strata.Laurel.ConcreteEval.TestHelper + +/-! ## Test 1: Minimal program — main returns literal int -/ + +/-- +info: returned: 42 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { return 42 }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 2: Local variables and arithmetic -/ + +/-- +info: returned: 7 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + var x: int := 3; + var y: int := 4; + return x + y +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 3: Static procedure call -/ + +/-- +info: returned: 30 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure add(a: int, b: int) { return a + b }; +procedure main() { return add(10, 20) }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 4: While loop — sum 1..10 -/ + +/-- +info: returned: 55 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure main() { + var sum: int := 0; + var i: int := 1; + while (i <= 10) { + sum := sum + i; + i := i + 1 + }; + return sum +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 5: If-then-else (abs function) -/ + +/-- +info: returned: 5 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure abs(x: int) { + if (x < 0) { return 0 - x } else { return x } +}; +procedure main() { return abs(-5) }; +" + IO.println (toString (runProgram prog)) + + +/-! ## Test 5b: Lazy And -/ + +/-- +info: returned: -1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure lazyAnd(x: int) { + var sum : int := 0; + if (x < 0 && {sum := 1; sum == 1}) { sum := 42} else { sum := sum - 1}; + return sum +}; +procedure main() { return lazyAnd(5) }; +" + IO.println (toString (runProgram prog)) + + +/-- +info: returned: -1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure lazyAnd(x: int) { + var sum : int := 0; + if (x < 0 && {sum := 1; sum == 1}) { sum := 42} else { sum := sum - 1}; + return sum +}; +procedure main() { return lazyAnd(5) }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 5c: Lazy Or -/ + +/-- +info: returned: -1 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure lazyOr(x: int) { + var sum : int := 0; + if (x > 0 || {sum := 1; sum == 1}) { sum := sum - 1} else { sum := 42}; + return sum +}; +procedure main() { return lazyOr(5) }; +" + IO.println (toString (runProgram prog)) + + +/-! ## Test 6: Recursive procedure (factorial) -/ + +/-- +info: returned: 120 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure fact(n: int) { + if (n <= 1) { return 1 } else { return n * fact(n - 1) } +}; +procedure main() { return fact(5) }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 7: No main procedure -/ + +/-- +info: error: no 'main' procedure found +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +procedure notMain() { return 1 }; +" + IO.println (toString (runProgram prog)) + +/-! ## Test 8: OO features — composite type with field access -/ + +/-- +info: returned: 3 +-/ +#guard_msgs in +#eval! do + let prog ← parseLaurel r" +composite Point { + var x: int + var y: int +} +procedure main() { + var p: Point := new Point; + p#x := 1; + p#y := 2; + return p#x + p#y +}; +" + IO.println (toString (runProgram prog)) + +/-! ## Programmatic AST Tests + +The following tests exercise internal API features (outcome classification, +opaque procedures, instance methods, static fields) that cannot be expressed +in Laurel concrete syntax. They use programmatic AST construction. +-/ + +/-! ## Test 9: runProgram success classification -/ + +#guard + let prog := mkProgram [mkProc "main" [] (.LiteralInt 42)] + match runProgram prog with + | .success (.vInt 42) _ _ => true + | _ => false + +/-! ## Test 10: runProgram returned classification -/ + +#guard + let prog := mkProgram [mkProc "main" [] (.Return (some (mk (.LiteralInt 99))))] + match runProgram prog with + | .returned (some (.vInt 99)) _ _ => true + | _ => false + +/-! ## Test 11: No body (opaque procedure) -/ + +#guard + let mainProc : Procedure := { + name := "main" + inputs := [] + outputs := [] + preconditions := [] + determinism := .deterministic none + isFunctional := false + decreases := none + body := .Opaque [] none [] + md := emd + } + let prog := mkProgram [mainProc] + match runProgram prog with + | .noBody => true + | _ => false + +/-! ## Test 12: Instance method call via buildProcEnv -/ + +#guard + let getXBody := StmtExpr.Return (some (mk (.FieldSelect (mk (.This)) "x"))) + let getXProc : Procedure := { + name := "getX" + inputs := [⟨"this", ⟨.UserDefined "Point", emd⟩⟩] + outputs := [] + preconditions := [] + determinism := .deterministic none + isFunctional := false + decreases := none + body := .Transparent (mk getXBody) + md := emd + } + let pointType : TypeDefinition := .Composite { + name := "Point" + extending := [] + fields := [{ name := "x", isMutable := true, type := ⟨.TInt, emd⟩ }] + instanceProcedures := [getXProc] + } + let body := StmtExpr.Block [ + mk (.LocalVariable "p" ⟨.UserDefined "Point", emd⟩ (some (mk (.New "Point")))), + mk (.Assign [⟨.FieldSelect (mk (.Identifier "p")) "x", emd⟩] (mk (.LiteralInt 7))), + mk (.Return (some (mk (.InstanceCall (mk (.Identifier "p")) "getX" [])))) + ] none + let prog : Program := { + staticProcedures := [mkProc "main" [] body] + staticFields := [] + types := [pointType] + constants := [] + } + getOutcome (evalProgram prog) = some (.ret (some (.vInt 7))) + +/-! ## Test 13: Static fields initialized to vVoid -/ + +#guard + let body := StmtExpr.Block [ + mk (.Assign [⟨.Identifier "counter", emd⟩] (mk (.LiteralInt 10))), + mk (.Return (some (mk (.Identifier "counter")))) + ] none + let prog : Program := { + staticProcedures := [mkProc "main" [] body] + staticFields := [{ name := "counter", isMutable := true, type := ⟨.TInt, emd⟩ }] + types := [] + constants := [] + } + getOutcome (evalProgram prog) = some (.ret (some (.vInt 10))) + +end Strata.Laurel.ConcreteEvalTest diff --git a/StrataTest/Languages/Laurel/LaurelInterpreterIntegrationTest.lean b/StrataTest/Languages/Laurel/LaurelInterpreterIntegrationTest.lean new file mode 100644 index 000000000..dd85de8d2 --- /dev/null +++ b/StrataTest/Languages/Laurel/LaurelInterpreterIntegrationTest.lean @@ -0,0 +1,457 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Languages.Laurel.LaurelInterpreter + +/-! +# Integration Scenario Tests for Laurel Interpreter + +Multi-feature scenario tests exercising realistic Laurel programs through +the interpreter. Tests combine multiple language features to +validate that semantics composes correctly. +-/ + +namespace Strata.Laurel.InterpreterIntegrationTest + +open Strata.Laurel + +/-! ## Test Helpers -/ + +abbrev emd : Imperative.MetaData Core.Expression := .empty +def mk (s : StmtExpr) : StmtExprMd := ⟨s, emd⟩ +def emptyStore : LaurelStore := fun _ => none +def emptyHeap : LaurelHeap := fun _ => none +def emptyProc : ProcEnv := fun _ => none + +def trivialEval : 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 + +def singleStore (name : String) (v : LaurelValue) : LaurelStore := + fun x => if x == name then some v else none + +def multiStore (bindings : List (String × LaurelValue)) : LaurelStore := + fun x => bindings.find? (·.1 == x) |>.map (·.2) + +def getOutcome (r : Option (Outcome × LaurelStore × LaurelHeap)) : Option Outcome := + r.map (·.1) + +def getOutcomeAndVar (r : Option (Outcome × LaurelStore × LaurelHeap)) + (name : String) : Option (Outcome × Option LaurelValue) := + r.map (fun (o, σ, _) => (o, σ name)) + +def getVar (r : Option (Outcome × LaurelStore × LaurelHeap)) + (name : String) : Option LaurelValue := + r.bind (fun (_, σ, _) => σ name) + +/-- Make a simple procedure with a body expression. -/ +def mkProc (name : String) (inputs : List (String × HighType)) + (body : StmtExpr) : Procedure := + { name := name + inputs := inputs.map fun (n, t) => { name := n, type := ⟨t, emd⟩ } + outputs := [] + preconditions := [] + determinism := .deterministic none + isFunctional := false + decreases := none + body := .Transparent (mk body) + md := emd } + +/-! ## 1. Recursive Procedures -/ + +-- Factorial: fact(n) = if n <= 0 then 1 else n * fact(n-1) +#guard + let factBody := StmtExpr.IfThenElse + (mk (.PrimitiveOp .Leq [mk (.Identifier "n"), mk (.LiteralInt 0)])) + (mk (.Return (some (mk (.LiteralInt 1))))) + (some (mk (.Return (some (mk (.PrimitiveOp .Mul + [mk (.Identifier "n"), + mk (.StaticCall "fact" [mk (.PrimitiveOp .Sub + [mk (.Identifier "n"), mk (.LiteralInt 1)])])])))))) + let factProc := mkProc "fact" [("n", .TInt)] factBody + let π : ProcEnv := fun name => if name == "fact" then some factProc else none + -- fact(5) = 120 + getOutcome (interpStmt trivialEval π 1000 emptyHeap emptyStore + (.StaticCall "fact" [mk (.LiteralInt 5)])) + = some (.normal (.vInt 120)) + +-- Fibonacci via two procedures: fib calls fibHelper +-- fib(n) = if n <= 1 then n else fib(n-1) + fib(n-2) +#guard + let fibBody := StmtExpr.IfThenElse + (mk (.PrimitiveOp .Leq [mk (.Identifier "n"), mk (.LiteralInt 1)])) + (mk (.Return (some (mk (.Identifier "n"))))) + (some (mk (.Return (some (mk (.PrimitiveOp .Add + [mk (.StaticCall "fib" [mk (.PrimitiveOp .Sub + [mk (.Identifier "n"), mk (.LiteralInt 1)])]), + mk (.StaticCall "fib" [mk (.PrimitiveOp .Sub + [mk (.Identifier "n"), mk (.LiteralInt 2)])])])))))) + let fibProc := mkProc "fib" [("n", .TInt)] fibBody + let π : ProcEnv := fun name => if name == "fib" then some fibProc else none + -- fib(6) = 8 + getOutcome (interpStmt trivialEval π 1000 emptyHeap emptyStore + (.StaticCall "fib" [mk (.LiteralInt 6)])) + = some (.normal (.vInt 8)) + +/-! ## 2. Nested Control Flow -/ + +-- Nested while loops: outer counts i 0..2, inner counts j 0..2, accumulate sum +-- Note: j is pre-declared since initStore fails on re-declaration +#guard + let σ₀ := multiStore [("i", .vInt 0), ("j", .vInt 0), ("sum", .vInt 0)] + let outerLoop := StmtExpr.While + (mk (.PrimitiveOp .Lt [mk (.Identifier "i"), mk (.LiteralInt 3)])) + [] none + (mk (.Block [ + mk (.Assign [⟨.Identifier "j", emd⟩] (mk (.LiteralInt 0))), + mk (.While + (mk (.PrimitiveOp .Lt [mk (.Identifier "j"), mk (.LiteralInt 3)])) + [] none + (mk (.Block [ + mk (.Assign [⟨.Identifier "sum", emd⟩] + (mk (.PrimitiveOp .Add [mk (.Identifier "sum"), mk (.LiteralInt 1)]))), + mk (.Assign [⟨.Identifier "j", emd⟩] + (mk (.PrimitiveOp .Add [mk (.Identifier "j"), mk (.LiteralInt 1)]))) + ] none))), + mk (.Assign [⟨.Identifier "i", emd⟩] + (mk (.PrimitiveOp .Add [mk (.Identifier "i"), mk (.LiteralInt 1)]))) + ] none)) + let r := interpStmt trivialEval emptyProc 1000 emptyHeap σ₀ outerLoop + -- 3 outer × 3 inner = 9 + getVar r "sum" = some (.vInt 9) + +-- Return inside if inside while — early termination +#guard + let σ₀ := singleStore "x" (.vInt 0) + let body := StmtExpr.While + (mk (.LiteralBool true)) [] none + (mk (.Block [ + mk (.Assign [⟨.Identifier "x", emd⟩] + (mk (.PrimitiveOp .Add [mk (.Identifier "x"), mk (.LiteralInt 1)]))), + mk (.IfThenElse + (mk (.PrimitiveOp .Eq [mk (.Identifier "x"), mk (.LiteralInt 5)])) + (mk (.Return (some (mk (.Identifier "x"))))) + none) + ] none)) + getOutcome (interpStmt trivialEval emptyProc 1000 emptyHeap σ₀ body) + = some (.ret (some (.vInt 5))) + +-- Exit from deeply nested blocks (3+ levels) +#guard + let prog := StmtExpr.Block [ + mk (.Block [ + mk (.Block [ + mk (.Exit "outer") + ] none) + ] none), + mk (.LiteralInt 999) -- should not be reached + ] (some "outer") + getOutcome (interpStmt trivialEval emptyProc 100 emptyHeap emptyStore prog) + = some (.normal .vVoid) + +-- While loop with if-then-else containing exit to labeled outer block +#guard + let σ₀ := singleStore "x" (.vInt 0) + let prog := StmtExpr.Block [ + mk (.While + (mk (.LiteralBool true)) [] none + (mk (.Block [ + mk (.Assign [⟨.Identifier "x", emd⟩] + (mk (.PrimitiveOp .Add [mk (.Identifier "x"), mk (.LiteralInt 1)]))), + mk (.IfThenElse + (mk (.PrimitiveOp .Geq [mk (.Identifier "x"), mk (.LiteralInt 4)])) + (mk (.Exit "done")) + (some (mk (.LiteralBool true)))) + ] none))) + ] (some "done") + getOutcomeAndVar (interpStmt trivialEval emptyProc 1000 emptyHeap σ₀ prog) "x" + = some (.normal .vVoid, some (.vInt 4)) + +-- Block with multiple labeled sub-blocks and targeted exits +#guard + let σ₀ := multiStore [("r", .vInt 0)] + let prog := StmtExpr.Block [ + mk (.Block [ + mk (.Assign [⟨.Identifier "r", emd⟩] (mk (.LiteralInt 1))), + mk (.Exit "b1") + ] (some "b1")), + mk (.Block [ + mk (.Assign [⟨.Identifier "r", emd⟩] (mk (.LiteralInt 2))), + mk (.Exit "b2") + ] (some "b2")), + mk (.Assign [⟨.Identifier "r", emd⟩] (mk (.LiteralInt 3))) + ] none + getVar (interpStmt trivialEval emptyProc 100 emptyHeap σ₀ prog) "r" + = some (.vInt 3) + +/-! ## 3. Effectful Expressions in Complex Positions -/ + +-- Assignment in if-condition: if (x := 5) > 3 then 1 else 0 +#guard + let σ₀ := singleStore "x" (.vInt 0) + let prog := StmtExpr.IfThenElse + (mk (.PrimitiveOp .Gt + [mk (.Assign [⟨.Identifier "x", emd⟩] (mk (.LiteralInt 5))), + mk (.LiteralInt 3)])) + (mk (.LiteralInt 1)) + (some (mk (.LiteralInt 0))) + let r := interpStmt trivialEval emptyProc 100 emptyHeap σ₀ prog + getOutcome r = some (.normal (.vInt 1)) + +-- Assignment in while-condition: while (x := x + 1) < 5 do skip +#guard + let σ₀ := singleStore "x" (.vInt 0) + let prog := StmtExpr.While + (mk (.PrimitiveOp .Lt + [mk (.Assign [⟨.Identifier "x", emd⟩] + (mk (.PrimitiveOp .Add [mk (.Identifier "x"), mk (.LiteralInt 1)]))), + mk (.LiteralInt 5)])) + [] none + (mk (.Block [] none)) + let r := interpStmt trivialEval emptyProc 100 emptyHeap σ₀ prog + getVar r "x" = some (.vInt 5) + +-- Nested assignments in arguments: (x := 1) + (y := 2) = 3 +#guard + let σ₀ := multiStore [("x", .vInt 0), ("y", .vInt 0)] + let prog := StmtExpr.PrimitiveOp .Add + [mk (.Assign [⟨.Identifier "x", emd⟩] (mk (.LiteralInt 1))), + mk (.Assign [⟨.Identifier "y", emd⟩] (mk (.LiteralInt 2)))] + let r := interpStmt trivialEval emptyProc 100 emptyHeap σ₀ prog + getOutcome r = some (.normal (.vInt 3)) + +-- Assignment in both branches of if-then-else +#guard + let σ₀ := singleStore "x" (.vInt 0) + let prog := StmtExpr.IfThenElse + (mk (.LiteralBool false)) + (mk (.Assign [⟨.Identifier "x", emd⟩] (mk (.LiteralInt 10)))) + (some (mk (.Assign [⟨.Identifier "x", emd⟩] (mk (.LiteralInt 20))))) + let r := interpStmt trivialEval emptyProc 100 emptyHeap σ₀ prog + getOutcomeAndVar r "x" = some (.normal (.vInt 20), some (.vInt 20)) + +/-! ## 4. Object-Oriented Programs -/ + +-- Create object, set multiple fields, read them back +#guard + let prog := StmtExpr.Block [ + mk (.LocalVariable "obj" ⟨.UserDefined "Pt", emd⟩ (some (mk (.New "Pt")))), + mk (.Assign [⟨.FieldSelect (mk (.Identifier "obj")) "x", emd⟩] (mk (.LiteralInt 10))), + mk (.Assign [⟨.FieldSelect (mk (.Identifier "obj")) "y", emd⟩] (mk (.LiteralInt 20))), + mk (.PrimitiveOp .Add [ + mk (.FieldSelect (mk (.Identifier "obj")) "x"), + mk (.FieldSelect (mk (.Identifier "obj")) "y")]) + ] none + getOutcome (interpStmt trivialEval emptyProc 100 emptyHeap emptyStore prog) + = some (.normal (.vInt 30)) + +-- Method call that modifies object fields via heap +#guard + let setXProc : Procedure := { + name := "Obj.setX" + inputs := [{ name := "this", type := ⟨.UserDefined "Obj", emd⟩ }, + { name := "v", type := ⟨.TInt, emd⟩ }] + outputs := [] + preconditions := [] + determinism := .deterministic none + isFunctional := false + decreases := none + body := .Transparent (mk (.Assign [⟨.FieldSelect (mk (.Identifier "this")) "x", emd⟩] + (mk (.Identifier "v")))) + md := emd + } + let π : ProcEnv := fun name => if name == "Obj.setX" then some setXProc else none + let prog := StmtExpr.Block [ + mk (.LocalVariable "o" ⟨.UserDefined "Obj", emd⟩ (some (mk (.New "Obj")))), + mk (.InstanceCall (mk (.Identifier "o")) "setX" [mk (.LiteralInt 42)]), + mk (.FieldSelect (mk (.Identifier "o")) "x") + ] none + getOutcome (interpStmt trivialEval π 100 emptyHeap emptyStore prog) + = some (.normal (.vInt 42)) + +-- Multiple objects with independent field stores +#guard + let prog := StmtExpr.Block [ + mk (.LocalVariable "a" ⟨.UserDefined "T", emd⟩ (some (mk (.New "T")))), + mk (.LocalVariable "b" ⟨.UserDefined "T", emd⟩ (some (mk (.New "T")))), + mk (.Assign [⟨.FieldSelect (mk (.Identifier "a")) "v", emd⟩] (mk (.LiteralInt 1))), + mk (.Assign [⟨.FieldSelect (mk (.Identifier "b")) "v", emd⟩] (mk (.LiteralInt 2))), + mk (.FieldSelect (mk (.Identifier "a")) "v") + ] none + getOutcome (interpStmt trivialEval emptyProc 100 emptyHeap emptyStore prog) + = some (.normal (.vInt 1)) + +-- Chain: new → field update → method call → field select +#guard + let getF : Procedure := { + name := "C.getF" + inputs := [{ name := "this", type := ⟨.UserDefined "C", emd⟩ }] + outputs := [] + preconditions := [] + determinism := .deterministic none + isFunctional := false + decreases := none + body := .Transparent (mk (.Return (some (mk (.FieldSelect (mk (.Identifier "this")) "f"))))) + md := emd + } + let π : ProcEnv := fun name => if name == "C.getF" then some getF else none + let prog := StmtExpr.Block [ + mk (.LocalVariable "c" ⟨.UserDefined "C", emd⟩ (some (mk (.New "C")))), + mk (.Assign [⟨.FieldSelect (mk (.Identifier "c")) "f", emd⟩] (mk (.LiteralInt 77))), + mk (.InstanceCall (mk (.Identifier "c")) "getF" []) + ] none + getOutcome (interpStmt trivialEval π 100 emptyHeap emptyStore prog) + = some (.normal (.vInt 77)) + +-- ReferenceEquals after aliasing +#guard + let prog := StmtExpr.Block [ + mk (.LocalVariable "a" ⟨.UserDefined "T", emd⟩ (some (mk (.New "T")))), + mk (.LocalVariable "b" ⟨.UserDefined "T", emd⟩ (some (mk (.Identifier "a")))), + mk (.ReferenceEquals (mk (.Identifier "a")) (mk (.Identifier "b"))) + ] none + getOutcome (interpStmt trivialEval emptyProc 100 emptyHeap emptyStore prog) + = some (.normal (.vBool true)) + +/-! ## 5. Procedure Interaction Patterns -/ + +-- Procedure A calls procedure B (non-recursive call chain) +#guard + let double := mkProc "double" [("n", .TInt)] + (.Return (some (mk (.PrimitiveOp .Mul [mk (.Identifier "n"), mk (.LiteralInt 2)])))) + let quadruple := mkProc "quadruple" [("n", .TInt)] + (.Return (some (mk (.StaticCall "double" + [mk (.StaticCall "double" [mk (.Identifier "n")])])))) + let π : ProcEnv := fun name => + if name == "double" then some double + else if name == "quadruple" then some quadruple + else none + getOutcome (interpStmt trivialEval π 100 emptyHeap emptyStore + (.StaticCall "quadruple" [mk (.LiteralInt 3)])) + = some (.normal (.vInt 12)) + +-- Procedure with precondition (assert in body) +#guard + let safeDiv := mkProc "safeDiv" [("a", .TInt), ("b", .TInt)] + (.Block [ + mk (.Assert (mk (.PrimitiveOp .Neq [mk (.Identifier "b"), mk (.LiteralInt 0)]))), + mk (.Return (some (mk (.PrimitiveOp .Div [mk (.Identifier "a"), mk (.Identifier "b")])))) + ] none) + let π : ProcEnv := fun name => if name == "safeDiv" then some safeDiv else none + -- safeDiv(10, 2) = 5 + getOutcome (interpStmt trivialEval π 100 emptyHeap emptyStore + (.StaticCall "safeDiv" [mk (.LiteralInt 10), mk (.LiteralInt 2)])) + = some (.normal (.vInt 5)) + +-- Procedure that returns early via Return in the middle of a block +#guard + let earlyRet := mkProc "earlyRet" [("n", .TInt)] + (.Block [ + mk (.IfThenElse + (mk (.PrimitiveOp .Lt [mk (.Identifier "n"), mk (.LiteralInt 0)])) + (mk (.Return (some (mk (.LiteralInt (-1)))))) + none), + mk (.Return (some (mk (.Identifier "n")))) + ] none) + let π : ProcEnv := fun name => if name == "earlyRet" then some earlyRet else none + -- earlyRet(-5) = -1 + getOutcome (interpStmt trivialEval π 100 emptyHeap emptyStore + (.StaticCall "earlyRet" [mk (.LiteralInt (-5))])) + = some (.normal (.vInt (-1))) + +-- Procedure with local variables that shadow caller's variables +#guard + let σ₀ := singleStore "x" (.vInt 100) + let setX := mkProc "setX" [] + (.Block [ + mk (.LocalVariable "x" ⟨.TInt, emd⟩ (some (mk (.LiteralInt 999)))), + mk (.Return (some (mk (.Identifier "x")))) + ] none) + let π : ProcEnv := fun name => if name == "setX" then some setX else none + let r := interpStmt trivialEval π 100 emptyHeap σ₀ + (.StaticCall "setX" []) + -- Procedure returns 999 (its local x), caller's x unchanged + getOutcome r = some (.normal (.vInt 999)) && + getVar r "x" = some (.vInt 100) + +/-! ## 6. Store Threading Correctness -/ + +-- Sequence of assignments verifying left-to-right store threading +#guard + let σ₀ := multiStore [("a", .vInt 0), ("b", .vInt 0), ("c", .vInt 0)] + let prog := StmtExpr.Block [ + mk (.Assign [⟨.Identifier "a", emd⟩] (mk (.LiteralInt 1))), + mk (.Assign [⟨.Identifier "b", emd⟩] (mk (.PrimitiveOp .Add [mk (.Identifier "a"), mk (.LiteralInt 1)]))), + mk (.Assign [⟨.Identifier "c", emd⟩] (mk (.PrimitiveOp .Add [mk (.Identifier "b"), mk (.LiteralInt 1)]))) + ] none + let r := interpStmt trivialEval emptyProc 100 emptyHeap σ₀ prog + getVar r "a" = some (.vInt 1) && + getVar r "b" = some (.vInt 2) && + getVar r "c" = some (.vInt 3) + +-- While loop accumulator pattern (sum 1..5) +#guard + let σ₀ := multiStore [("i", .vInt 1), ("sum", .vInt 0)] + let prog := StmtExpr.While + (mk (.PrimitiveOp .Leq [mk (.Identifier "i"), mk (.LiteralInt 5)])) + [] none + (mk (.Block [ + mk (.Assign [⟨.Identifier "sum", emd⟩] + (mk (.PrimitiveOp .Add [mk (.Identifier "sum"), mk (.Identifier "i")]))), + mk (.Assign [⟨.Identifier "i", emd⟩] + (mk (.PrimitiveOp .Add [mk (.Identifier "i"), mk (.LiteralInt 1)]))) + ] none)) + let r := interpStmt trivialEval emptyProc 1000 emptyHeap σ₀ prog + getVar r "sum" = some (.vInt 15) + +-- Swap pattern: t := x; x := y; y := t +#guard + let σ₀ := multiStore [("x", .vInt 10), ("y", .vInt 20)] + let prog := StmtExpr.Block [ + mk (.LocalVariable "t" ⟨.TInt, emd⟩ (some (mk (.Identifier "x")))), + mk (.Assign [⟨.Identifier "x", emd⟩] (mk (.Identifier "y"))), + mk (.Assign [⟨.Identifier "y", emd⟩] (mk (.Identifier "t"))) + ] none + let r := interpStmt trivialEval emptyProc 100 emptyHeap σ₀ prog + getVar r "x" = some (.vInt 20) && + getVar r "y" = some (.vInt 10) + +/-! ## 7. Edge Cases -/ + +-- Deeply nested blocks (10+ levels) — verify no stack issues with fuel +#guard + let rec nestBlocks : Nat → StmtExpr → StmtExpr + | 0, inner => inner + | n + 1, inner => .Block [mk (nestBlocks n inner)] none + let prog := nestBlocks 15 (.LiteralInt 42) + getOutcome (interpStmt trivialEval emptyProc 100 emptyHeap emptyStore prog) + = some (.normal (.vInt 42)) + +-- Empty program (empty block) +#guard + getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Block [] none)) + = some (.normal .vVoid) + +-- Program that exhausts fuel (infinite loop with limited fuel → none) +#guard + interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.While (mk (.LiteralBool true)) [] none (mk (.Block [] none))) + = none + +-- Large number of sequential assignments +#guard + let stmts : List StmtExprMd := List.range 20 |>.map fun i => + mk (.LocalVariable (s!"v{i}") ⟨.TInt, emd⟩ (some (mk (.LiteralInt (Int.ofNat i))))) + let prog := StmtExpr.Block (stmts ++ [mk (.Identifier "v19")]) none + getOutcome (interpStmt trivialEval emptyProc 100 emptyHeap emptyStore prog) + = some (.normal (.vInt 19)) + +end Strata.Laurel.InterpreterIntegrationTest diff --git a/StrataTest/Languages/Laurel/LaurelInterpreterPropertyTest.lean b/StrataTest/Languages/Laurel/LaurelInterpreterPropertyTest.lean new file mode 100644 index 000000000..e6726c79d --- /dev/null +++ b/StrataTest/Languages/Laurel/LaurelInterpreterPropertyTest.lean @@ -0,0 +1,452 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Languages.Laurel.LaurelInterpreter +import Plausible + +/-! +# Property-Based Tests for Laurel Interpreter + +Plausible-based property tests validating structural invariants of the +Laurel interpreter across randomly generated inputs. +-/ + +namespace Strata.Laurel.InterpreterPropertyTest + +open Strata.Laurel +open Plausible + +/-! ## Test Infrastructure -/ + +abbrev emd : Imperative.MetaData Core.Expression := .empty +def mk (s : StmtExpr) : StmtExprMd := ⟨s, emd⟩ +def mkTy (t : HighType) : HighTypeMd := ⟨t, emd⟩ + +def emptyStore : LaurelStore := fun _ => none +def emptyHeap : LaurelHeap := fun _ => none +def emptyProc : ProcEnv := fun _ => none +def trivialEval : LaurelEval := fun _ _ => none + +def idNames : List String := ["x", "y", "z", "a", "b"] + +/-- Check if two results agree on outcome and a specific variable. + TODO: This ignores the heap component — a counterexample differing only in + heap state would be missed. Consider comparing the full result triple. -/ +def resultAgrees (r1 r2 : Option (Outcome × LaurelStore × LaurelHeap)) + (vars : List String) : Bool := + match r1, r2 with + | some (o1, σ1, _), some (o2, σ2, _) => + o1 == o2 && vars.all (fun v => σ1 v == σ2 v) + | none, none => true + | _, _ => false + +/-! ## Repr / Shrinkable / Arbitrary for LaurelValue -/ + +instance : Shrinkable LaurelValue where + shrink + | .vInt i => (Shrinkable.shrink i).map .vInt + | .vBool _ => [] + | .vString s => (Shrinkable.shrink s).map .vString + | .vVoid => [] + | .vRef n => (Shrinkable.shrink n).map .vRef + +instance : Arbitrary LaurelValue where + arbitrary := do + let tag ← Gen.choose Nat 0 4 (by omega) + match tag.val with + | 0 => return .vInt (← Arbitrary.arbitrary) + | 1 => return .vBool (← Arbitrary.arbitrary) + | 2 => return .vString (← Arbitrary.arbitrary) + | 3 => return .vVoid + | _ => return .vRef (← Gen.choose Nat 0 9 (by omega)) + +/-! ## Simplified Test Expression -/ + +/-- A simplified expression type for property testing. -/ +inductive TestExpr where + | litInt (i : Int) + | litBool (b : Bool) + | litStr (s : String) + | ident (name : String) + | primOp (op : Operation) (args : List TestExpr) + | ite (c t e : TestExpr) + | block (stmts : List TestExpr) + | assign (name : String) (val : TestExpr) + | localVar (name : String) (init : TestExpr) + | exit_ (label : String) + deriving Repr + +def TestExpr.inferType : TestExpr → HighType + | .litBool _ => .TBool + | .litStr _ => .TString + | _ => .TInt + +def TestExpr.toStmtExpr : TestExpr → StmtExpr + | .litInt i => .LiteralInt i + | .litBool b => .LiteralBool b + | .litStr s => .LiteralString s + | .ident n => .Identifier (mkId n) + | .primOp op args => .PrimitiveOp op (args.map (mk ·.toStmtExpr)) + | .ite c t e => .IfThenElse (mk c.toStmtExpr) (mk t.toStmtExpr) (some (mk e.toStmtExpr)) + | .block ss => .Block (ss.map (mk ·.toStmtExpr)) none + | .assign n v => .Assign [mk (.Identifier (mkId n))] (mk v.toStmtExpr) + | .localVar n init => .LocalVariable (mkId n) (mkTy init.inferType) (some (mk init.toStmtExpr)) + | .exit_ l => .Exit l + +/-! ## Generators -/ + +instance : Inhabited Operation where + default := .Add + +instance : Arbitrary Operation where + arbitrary := do + let ops := #[Operation.Eq, .Neq, .And, .Or, .Not, .Implies, .Neg, + .Add, .Sub, .Mul, .Div, .Mod, .DivT, .ModT, + .Lt, .Leq, .Gt, .Geq, .StrConcat] + let i ← Gen.choose Nat 0 (ops.size - 1) (by omega) + return ops[i.val]! + +instance : Shrinkable Operation where + shrink _ := [] + +/-- Depth-bounded generator for TestExpr. -/ +partial def genTestExpr (depth : Nat) : Gen TestExpr := do + match depth with + | 0 => + let tag ← Gen.choose Nat 0 3 (by omega) + match tag.val with + | 0 => return .litInt (← Arbitrary.arbitrary) + | 1 => return .litBool (← Arbitrary.arbitrary) + | 2 => return .litStr (← Arbitrary.arbitrary) + | _ => + let i ← Gen.choose Nat 0 (idNames.length - 1) (by omega) + return .ident idNames[i.val]! + | d + 1 => + let tag ← Gen.choose Nat 0 7 (by omega) + match tag.val with + | 0 => return .litInt (← Arbitrary.arbitrary) + | 1 => return .litBool (← Arbitrary.arbitrary) + | 2 => + let a ← genTestExpr d; let b ← genTestExpr d + return .primOp .Add [a, b] + | 3 => + let a ← genTestExpr d; let b ← genTestExpr d + return .primOp .Lt [a, b] + | 4 => + let c ← genTestExpr d; let t ← genTestExpr d; let e ← genTestExpr d + return .ite c t e + | 5 => + let len ← Gen.choose Nat 1 3 (by omega) + let stmts ← List.range len.val |>.mapM (fun _ => genTestExpr d) + return .block stmts + | 6 => + let i ← Gen.choose Nat 0 (idNames.length - 1) (by omega) + let v ← genTestExpr d + return .assign idNames[i.val]! v + | _ => + let i ← Gen.choose Nat 0 (idNames.length - 1) (by omega) + let v ← genTestExpr d + return .localVar idNames[i.val]! v + +instance : Shrinkable TestExpr where + shrink + | .litInt i => (Shrinkable.shrink i).map .litInt + | .litBool _ => [] + | .litStr s => (Shrinkable.shrink s).map .litStr + | .ident _ => [] + | .primOp _ args => args + | .ite c t e => [c, t, e] + | .block ss => ss + | .assign _ v => [v] + | .localVar _ v => [v] + | .exit_ _ => [] + +instance : Arbitrary TestExpr where + arbitrary := genTestExpr 2 + +/-! ## Store Generator -/ + +/-- Wrapper for store generation in Plausible. -/ +structure TestStore where + store : LaurelStore + vars : List String -- track which vars are set for comparison + +instance : Repr TestStore where + reprPrec _ _ := "⟨TestStore⟩" + +instance : Shrinkable TestStore where + shrink _ := [] + +instance : Arbitrary TestStore where + arbitrary := do + let mut σ : LaurelStore := fun _ => none + let mut vs : List String := [] + for name in idNames do + let include_ ← Arbitrary.arbitrary (α := Bool) + if include_ then + let v ← Arbitrary.arbitrary (α := LaurelValue) + σ := fun x => if x == name then some v else σ x + vs := name :: vs + return ⟨σ, vs⟩ + +/-! ## 1. Fuel Monotonicity -/ + +/-- If interpStmt succeeds with fuel₁, it gives the same result with fuel₁ + k. -/ +def fuelMonoProp (e : TestExpr) (ts : TestStore) (fuel₁ : Fin 20) (k : Fin 20) : Bool := + let s := e.toStmtExpr + let f1 := fuel₁.val + 1 + let f2 := f1 + k.val + let r1 := interpStmt trivialEval emptyProc f1 emptyHeap ts.store s + let r2 := interpStmt trivialEval emptyProc f2 emptyHeap ts.store s + match r1 with + | some _ => resultAgrees r1 r2 ts.vars + | none => true + +#eval Testable.check (cfg := { numInst := 300, quiet := true }) + (∀ e : TestExpr, ∀ ts : TestStore, ∀ f1 : Fin 20, ∀ k : Fin 20, + fuelMonoProp e ts f1 k) + +/-! ## 2. Determinism: Unused Store Entries Don't Affect Literals -/ + +/-- Adding an unused variable to the store doesn't change literal evaluation. -/ +def unusedStoreIrrelevantProp (i : Int) (extraVal : LaurelValue) : Bool := + let σ1 : LaurelStore := emptyStore + let σ2 : LaurelStore := fun x => if x == "__unused__" then some extraVal else none + let r1 := interpStmt trivialEval emptyProc 5 emptyHeap σ1 (.LiteralInt i) + let r2 := interpStmt trivialEval emptyProc 5 emptyHeap σ2 (.LiteralInt i) + match r1, r2 with + | some (o1, _, _), some (o2, _, _) => o1 == o2 + | none, none => true + | _, _ => false + +#eval Testable.check (cfg := { numInst := 300, quiet := true }) + (∀ i : Int, ∀ v : LaurelValue, unusedStoreIrrelevantProp i v) + +/-! ## 3. Literal Stability -/ + +/-- Literals return the corresponding value and don't modify the store. -/ +def litIntStable (i : Int) : Bool := + let σ : LaurelStore := fun x => if x == "x" then some (.vInt 42) else none + match interpStmt trivialEval emptyProc 5 emptyHeap σ (.LiteralInt i) with + | some (.normal (.vInt j), σ', _) => i == j && σ' "x" == some (.vInt 42) + | _ => false + +def litBoolStable (b : Bool) : Bool := + let σ : LaurelStore := fun x => if x == "x" then some (.vInt 42) else none + match interpStmt trivialEval emptyProc 5 emptyHeap σ (.LiteralBool b) with + | some (.normal (.vBool b'), σ', _) => b == b' && σ' "x" == some (.vInt 42) + | _ => false + +def litStrStable (s : String) : Bool := + let σ : LaurelStore := fun x => if x == "x" then some (.vInt 42) else none + match interpStmt trivialEval emptyProc 5 emptyHeap σ (.LiteralString s) with + | some (.normal (.vString s'), σ', _) => s == s' && σ' "x" == some (.vInt 42) + | _ => false + +#eval Testable.check (cfg := { numInst := 300, quiet := true }) + (∀ i : Int, litIntStable i) + +#eval Testable.check (cfg := { numInst := 300, quiet := true }) + (∀ b : Bool, litBoolStable b) + +#eval Testable.check (cfg := { numInst := 300, quiet := true }) + (∀ s : String, litStrStable s) + +/-! ## 4. evalPrimOp Totality on Well-Typed Inputs -/ + +/-- Arithmetic ops on ints return some (except div/mod by zero). -/ +def arithTotalProp (a b : Int) : Bool := + (evalPrimOp .Add [.vInt a, .vInt b]).isSome && + (evalPrimOp .Sub [.vInt a, .vInt b]).isSome && + (evalPrimOp .Mul [.vInt a, .vInt b]).isSome && + (b == 0 || (evalPrimOp .Div [.vInt a, .vInt b]).isSome) && + (b == 0 || (evalPrimOp .Mod [.vInt a, .vInt b]).isSome) && + (b == 0 || (evalPrimOp .DivT [.vInt a, .vInt b]).isSome) && + (b == 0 || (evalPrimOp .ModT [.vInt a, .vInt b]).isSome) && + (evalPrimOp .Neg [.vInt a]).isSome + +/-- Boolean ops on bools return some (Implies is short-circuit, handled in interpStmt). -/ +def boolTotalProp (a b : Bool) : Bool := + (evalPrimOp .And [.vBool a, .vBool b]).isSome && + (evalPrimOp .Or [.vBool a, .vBool b]).isSome && + (evalPrimOp .Not [.vBool a]).isSome + +/-- Comparison ops on ints return some. -/ +def cmpTotalProp (a b : Int) : Bool := + (evalPrimOp .Lt [.vInt a, .vInt b]).isSome && + (evalPrimOp .Leq [.vInt a, .vInt b]).isSome && + (evalPrimOp .Gt [.vInt a, .vInt b]).isSome && + (evalPrimOp .Geq [.vInt a, .vInt b]).isSome + +/-- Equality ops on same-typed values return some. -/ +def eqTotalProp (a b : Int) (c d : Bool) (s t : String) : Bool := + (evalPrimOp .Eq [.vInt a, .vInt b]).isSome && + (evalPrimOp .Neq [.vInt a, .vInt b]).isSome && + (evalPrimOp .Eq [.vBool c, .vBool d]).isSome && + (evalPrimOp .Neq [.vBool c, .vBool d]).isSome && + (evalPrimOp .Eq [.vString s, .vString t]).isSome && + (evalPrimOp .Neq [.vString s, .vString t]).isSome + +/-- String concat on strings returns some. -/ +def strConcatTotalProp (a b : String) : Bool := + (evalPrimOp .StrConcat [.vString a, .vString b]).isSome + +#eval Testable.check (cfg := { numInst := 300, quiet := true }) + (∀ a b : Int, arithTotalProp a b) + +#eval Testable.check (cfg := { numInst := 300, quiet := true }) + (∀ a b : Bool, boolTotalProp a b) + +#eval Testable.check (cfg := { numInst := 300, quiet := true }) + (∀ a b : Int, cmpTotalProp a b) + +#eval Testable.check (cfg := { numInst := 300, quiet := true }) + (∀ a b : Int, ∀ c d : Bool, ∀ s t : String, eqTotalProp a b c d s t) + +#eval Testable.check (cfg := { numInst := 300, quiet := true }) + (∀ a b : String, strConcatTotalProp a b) + +/-! ## 5. evalPrimOp Type Preservation -/ + +def isVInt : LaurelValue → Bool + | .vInt _ => true + | _ => false + +def isVBool : LaurelValue → Bool + | .vBool _ => true + | _ => false + +def isVString : LaurelValue → Bool + | .vString _ => true + | _ => false + +/-- Arithmetic ops on ints return int. -/ +def arithTypePresProp (a b : Int) : Bool := + let chk := fun r => match r with | some v => isVInt v | none => true + chk (evalPrimOp .Add [.vInt a, .vInt b]) && + chk (evalPrimOp .Sub [.vInt a, .vInt b]) && + chk (evalPrimOp .Mul [.vInt a, .vInt b]) && + chk (evalPrimOp .Neg [.vInt a]) && + chk (evalPrimOp .Div [.vInt a, .vInt b]) && + chk (evalPrimOp .Mod [.vInt a, .vInt b]) && + chk (evalPrimOp .DivT [.vInt a, .vInt b]) && + chk (evalPrimOp .ModT [.vInt a, .vInt b]) + +/-- Boolean ops on bools return bool. -/ +def boolTypePresProp (a b : Bool) : Bool := + let chk := fun r => match r with | some v => isVBool v | none => true + chk (evalPrimOp .And [.vBool a, .vBool b]) && + chk (evalPrimOp .Or [.vBool a, .vBool b]) && + chk (evalPrimOp .Not [.vBool a]) && + chk (evalPrimOp .Implies [.vBool a, .vBool b]) + +/-- Comparison ops return bool. -/ +def cmpTypePresProp (a b : Int) : Bool := + let chk := fun r => match r with | some v => isVBool v | none => true + chk (evalPrimOp .Lt [.vInt a, .vInt b]) && + chk (evalPrimOp .Leq [.vInt a, .vInt b]) && + chk (evalPrimOp .Gt [.vInt a, .vInt b]) && + chk (evalPrimOp .Geq [.vInt a, .vInt b]) && + chk (evalPrimOp .Eq [.vInt a, .vInt b]) && + chk (evalPrimOp .Neq [.vInt a, .vInt b]) + +/-- String concat returns string. -/ +def strConcatTypePresProp (a b : String) : Bool := + match evalPrimOp .StrConcat [.vString a, .vString b] with + | some v => isVString v + | none => true + +#eval Testable.check (cfg := { numInst := 300, quiet := true }) + (∀ a b : Int, arithTypePresProp a b) + +#eval Testable.check (cfg := { numInst := 300, quiet := true }) + (∀ a b : Bool, boolTypePresProp a b) + +#eval Testable.check (cfg := { numInst := 300, quiet := true }) + (∀ a b : Int, cmpTypePresProp a b) + +#eval Testable.check (cfg := { numInst := 300, quiet := true }) + (∀ a b : String, strConcatTypePresProp a b) + +/-! ## 6. Block Value Is Last Statement's Value -/ + +/-- A block of int literals returns the value of the last literal. -/ +def blockLastValueProp2 (a b : Int) : Bool := + let stmts := [mk (.LiteralInt a), mk (.LiteralInt b)] + match interpBlock trivialEval emptyProc 20 emptyHeap emptyStore stmts with + | some (.normal (.vInt v), _, _) => v == b + | _ => false + +def blockLastValueProp3 (a b c : Int) : Bool := + let stmts := [mk (.LiteralInt a), mk (.LiteralInt b), mk (.LiteralInt c)] + match interpBlock trivialEval emptyProc 20 emptyHeap emptyStore stmts with + | some (.normal (.vInt v), _, _) => v == c + | _ => false + +def blockSingletonProp (a : Int) : Bool := + match interpBlock trivialEval emptyProc 20 emptyHeap emptyStore [mk (.LiteralInt a)] with + | some (.normal (.vInt v), _, _) => v == a + | _ => false + +#eval Testable.check (cfg := { numInst := 300, quiet := true }) + (∀ a b : Int, blockLastValueProp2 a b) + +#eval Testable.check (cfg := { numInst := 300, quiet := true }) + (∀ a b c : Int, blockLastValueProp3 a b c) + +#eval Testable.check (cfg := { numInst := 300, quiet := true }) + (∀ a : Int, blockSingletonProp a) + +/-! ## 7. Exit Propagation -/ + +/-- If a block contains an Exit, the block produces .exit regardless of + statements after it. -/ +def exitPropagationProp (i : Int) (label : String) (j : Int) : Bool := + let stmts := [mk (.LiteralInt i), mk (.Exit label), mk (.LiteralInt j)] + match interpBlock trivialEval emptyProc 20 emptyHeap emptyStore stmts with + | some (.exit l, _, _) => l == label + | _ => false + +#eval Testable.check (cfg := { numInst := 300, quiet := true }) + (∀ i : Int, ∀ label : String, ∀ j : Int, exitPropagationProp i label j) + +/-- Exit at the first position also propagates. -/ +def exitFirstProp (label : String) (i : Int) : Bool := + let stmts := [mk (.Exit label), mk (.LiteralInt i)] + match interpBlock trivialEval emptyProc 20 emptyHeap emptyStore stmts with + | some (.exit l, _, _) => l == label + | _ => false + +#eval Testable.check (cfg := { numInst := 300, quiet := true }) + (∀ label : String, ∀ i : Int, exitFirstProp label i) + +/-! ## 8. Store Threading in Blocks -/ + +/-- LocalVariable followed by Identifier lookup returns the initialized value. -/ +def storeThreadingIntProp (v : Int) : Bool := + let name := mkId "fresh_var" + let localDecl := mk (.LocalVariable name (mkTy .TInt) (some (mk (.LiteralInt v)))) + let lookup := mk (.Identifier name) + match interpBlock trivialEval emptyProc 20 emptyHeap emptyStore [localDecl, lookup] with + | some (.normal (.vInt v'), _, _) => v == v' + | _ => false + +#eval Testable.check (cfg := { numInst := 300, quiet := true }) + (∀ v : Int, storeThreadingIntProp v) + +/-- LocalVariable with bool value followed by lookup. -/ +def storeThreadingBoolProp (b : Bool) : Bool := + let name := mkId "fresh_var" + let localDecl := mk (.LocalVariable name (mkTy .TBool) (some (mk (.LiteralBool b)))) + let lookup := mk (.Identifier name) + match interpBlock trivialEval emptyProc 20 emptyHeap emptyStore [localDecl, lookup] with + | some (.normal (.vBool b'), _, _) => b == b' + | _ => false + +#eval Testable.check (cfg := { numInst := 300, quiet := true }) + (∀ b : Bool, storeThreadingBoolProp b) + +end Strata.Laurel.InterpreterPropertyTest diff --git a/StrataTest/Languages/Laurel/LaurelInterpreterTest.lean b/StrataTest/Languages/Laurel/LaurelInterpreterTest.lean new file mode 100644 index 000000000..cf7ad5181 --- /dev/null +++ b/StrataTest/Languages/Laurel/LaurelInterpreterTest.lean @@ -0,0 +1,529 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Languages.Laurel.LaurelInterpreter + +/-! +# Tests for Laurel Interpreter + +`#guard` tests mirroring every test in `LaurelSemanticsTest.lean`. +Uses concrete finite stores and extracts outcomes for comparison since +`LaurelStore` and `LaurelHeap` are function types without `BEq`. +-/ + +namespace Strata.Laurel.InterpreterTest + +open Strata.Laurel + +/-! ## Test Helpers -/ + +abbrev emd : Imperative.MetaData Core.Expression := .empty + +def mk (s : StmtExpr) : StmtExprMd := ⟨s, emd⟩ + +def emptyStore : LaurelStore := fun _ => none +def emptyHeap : LaurelHeap := fun _ => none +def emptyProc : ProcEnv := fun _ => none + +def trivialEval : 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 + +def singleStore (name : Identifier) (v : LaurelValue) : LaurelStore := + fun x => if x == name.text then some v else none + +/-- Extract just the outcome from a interpreter result. -/ +def getOutcome (r : Option (Outcome × LaurelStore × LaurelHeap)) : Option Outcome := + r.map (·.1) + +/-- Extract outcome and a store lookup from a interpreter result. -/ +def getOutcomeAndVar (r : Option (Outcome × LaurelStore × LaurelHeap)) + (name : Identifier) : Option (Outcome × Option LaurelValue) := + r.map (fun (o, σ, _) => (o, σ name.text)) + +/-- Check that a interpreter result has the expected outcome and the store is unchanged. -/ +def checkPure (r : Option (Outcome × LaurelStore × LaurelHeap)) + (expected : Outcome) : Bool := + match r with + | some (o, _, _) => o == expected + | none => false + +/-! ## Literal Tests -/ + +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.LiteralInt 42)) = some (.normal (.vInt 42)) + +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.LiteralBool true)) = some (.normal (.vBool true)) + +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.LiteralString "hello")) = some (.normal (.vString "hello")) + +/-! ## Identifier Test -/ + +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap (singleStore "x" (.vInt 7)) + (.Identifier "x")) = some (.normal (.vInt 7)) + +/-! ## PrimitiveOp Tests -/ + +-- 2 + 3 = 5 +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.PrimitiveOp .Add [mk (.LiteralInt 2), mk (.LiteralInt 3)])) + = some (.normal (.vInt 5)) + +-- true && false = false +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.PrimitiveOp .And [mk (.LiteralBool true), mk (.LiteralBool false)])) + = some (.normal (.vBool false)) + +-- !true = false +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.PrimitiveOp .Not [mk (.LiteralBool true)])) + = some (.normal (.vBool false)) + +-- 5 < 10 = true +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.PrimitiveOp .Lt [mk (.LiteralInt 5), mk (.LiteralInt 10)])) + = some (.normal (.vBool true)) + +-- "a" ++ "b" = "ab" +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.PrimitiveOp .StrConcat [mk (.LiteralString "a"), mk (.LiteralString "b")])) + = some (.normal (.vString "ab")) + +/-! ## Effectful Argument Evaluation Test -/ + +-- x + (x := 1) with x initially 0 evaluates to 0 + 1 = 1, final store x = 1. +#guard + let σ₀ := singleStore "x" (.vInt 0) + let r := interpStmt trivialEval emptyProc 10 emptyHeap σ₀ + (.PrimitiveOp .Add [mk (.Identifier "x"), + mk (.Assign [⟨.Identifier "x", emd⟩] (mk (.LiteralInt 1)))]) + getOutcomeAndVar r "x" = some (.normal (.vInt 1), some (.vInt 1)) + +/-! ## Assignment Return Value Tests -/ + +-- assign_single returns the assigned value (not void) +#guard + let σ₀ := singleStore "x" (.vInt 0) + let r := interpStmt trivialEval emptyProc 10 emptyHeap σ₀ + (.Assign [⟨.Identifier "x", emd⟩] (mk (.LiteralInt 5))) + getOutcomeAndVar r "x" = some (.normal (.vInt 5), some (.vInt 5)) + +/-! ## Nested Effectful Argument Tests -/ + +-- f((x := 1), (x := 2)) with x initially 0 → args are [1, 2], final x = 2. +#guard + let σ₀ := singleStore "x" (.vInt 0) + let r := interpArgs trivialEval emptyProc 10 emptyHeap σ₀ + [mk (.Assign [⟨.Identifier "x", emd⟩] (mk (.LiteralInt 1))), + mk (.Assign [⟨.Identifier "x", emd⟩] (mk (.LiteralInt 2)))] + r.map (fun (vs, σ, _) => (vs, σ "x")) = some ([.vInt 1, .vInt 2], some (.vInt 2)) + +-- EvalStmtArgs with pure arguments +#guard + let r := interpArgs trivialEval emptyProc 10 emptyHeap emptyStore + [mk (.LiteralInt 1), mk (.LiteralBool true)] + r.map (·.1) = some [.vInt 1, .vBool true] + +-- EvalStmtArgs on empty list +#guard + let r := interpArgs trivialEval emptyProc 10 emptyHeap emptyStore [] + r.map (·.1) = some [] + +/-! ## Block Tests -/ + +-- Empty block evaluates to void +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Block [] none)) = some (.normal .vVoid) + +-- Singleton block returns its value +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Block [mk (.LiteralInt 99)] none)) = some (.normal (.vInt 99)) + +-- Block with two statements: value is the last one +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Block [mk (.LiteralInt 1), mk (.LiteralInt 2)] none)) + = some (.normal (.vInt 2)) + +/-! ## IfThenElse Tests -/ + +-- if true then 1 else 2 => 1 +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.IfThenElse (mk (.LiteralBool true)) (mk (.LiteralInt 1)) (some (mk (.LiteralInt 2))))) + = some (.normal (.vInt 1)) + +-- if false then 1 else 2 => 2 +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.IfThenElse (mk (.LiteralBool false)) (mk (.LiteralInt 1)) (some (mk (.LiteralInt 2))))) + = some (.normal (.vInt 2)) + +-- if false then 1 => void (no else branch) +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.IfThenElse (mk (.LiteralBool false)) (mk (.LiteralInt 1)) none)) + = some (.normal .vVoid) + +/-! ## Exit Tests -/ + +-- Exit propagates through block +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Block [mk (.Exit "L"), mk (.LiteralInt 99)] none)) + = some (.exit "L") + +-- Labeled block catches matching exit +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Block [mk (.Exit "L")] (some "L"))) + = some (.normal .vVoid) + +-- Labeled block does NOT catch non-matching exit +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Block [mk (.Exit "other")] (some "L"))) + = some (.exit "other") + +/-! ## Return Tests -/ + +-- Return with value +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Return (some (mk (.LiteralInt 42))))) + = some (.ret (some (.vInt 42))) + +-- Return without value +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Return none)) + = some (.ret none) + +-- Return short-circuits block +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Block [mk (.Return (some (mk (.LiteralInt 1)))), mk (.LiteralInt 99)] none)) + = some (.ret (some (.vInt 1))) + +/-! ## LocalVariable Tests -/ + +-- Declare and initialize a local variable +#guard + let r := interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.LocalVariable "x" ⟨.TInt, emd⟩ (some (mk (.LiteralInt 10)))) + getOutcomeAndVar r "x" = some (.normal .vVoid, some (.vInt 10)) + +-- Declare without initializer +#guard + let r := interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.LocalVariable "y" ⟨.TBool, emd⟩ none) + getOutcomeAndVar r "y" = some (.normal .vVoid, some .vVoid) + +/-! ## Assert/Assume Tests -/ + +-- Assert true succeeds +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Assert (mk (.LiteralBool true)))) + = some (.normal .vVoid) + +-- Assume true succeeds +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Assume (mk (.LiteralBool true)))) + = some (.normal .vVoid) + +/-! ## ProveBy Test -/ + +-- ProveBy evaluates to the value of its first argument +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.ProveBy (mk (.LiteralInt 5)) (mk (.LiteralBool true)))) + = some (.normal (.vInt 5)) + +/-! ## Nested Control Flow Tests -/ + +-- Nested blocks with exit: inner exit propagates to outer labeled block +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Block [ + mk (.Block [mk (.Exit "outer"), mk (.LiteralInt 99)] none), + mk (.LiteralInt 88) + ] (some "outer"))) + = some (.normal .vVoid) + +/-! ## Property Tests -/ + +-- catchExit preserves normal outcomes +#guard catchExit (some "L") (.normal (.vInt 1)) = .normal (.vInt 1) + +-- catchExit preserves return outcomes +#guard catchExit (some "L") (.ret (some (.vInt 1))) = .ret (some (.vInt 1)) + +-- catchExit catches matching exit +#guard catchExit (some "L") (.exit "L") = .normal .vVoid + +-- catchExit passes through non-matching exit +#guard catchExit (some "L") (.exit "M") = .exit "M" + +-- evalPrimOp: integer addition +#guard evalPrimOp .Add [.vInt 3, .vInt 4] = some (.vInt 7) + +-- evalPrimOp: boolean negation +#guard evalPrimOp .Not [.vBool false] = some (.vBool true) + +-- evalPrimOp: division by zero returns none +#guard evalPrimOp .Div [.vInt 5, .vInt 0] = none + +-- evalPrimOp: type mismatch returns none +#guard evalPrimOp .Add [.vBool true, .vInt 1] = none + +-- Empty block is void +#guard getOutcome (interpBlock trivialEval emptyProc 10 emptyHeap emptyStore []) + = some (.normal .vVoid) + +/-! ## Fuel Exhaustion Test -/ + +-- Fuel 0 returns none +#guard interpStmt trivialEval emptyProc 0 emptyHeap emptyStore (.LiteralInt 1) = none + +/-! ## Stuck State Tests -/ + +-- Undefined variable returns none +#guard interpStmt trivialEval emptyProc 10 emptyHeap emptyStore (.Identifier "undef") = none + +-- Abstract returns none +#guard interpStmt trivialEval emptyProc 10 emptyHeap emptyStore .Abstract = none + +-- All returns none +#guard interpStmt trivialEval emptyProc 10 emptyHeap emptyStore .All = none + +-- Hole returns none +#guard interpStmt trivialEval emptyProc 10 emptyHeap emptyStore .Hole = none + +/-! ## While Loop Test -/ + +-- Simple while loop: x starts at 0, increments to 3 +#guard + let σ₀ := singleStore "x" (.vInt 0) + let whileStmt := StmtExpr.While + (mk (.PrimitiveOp .Lt [mk (.Identifier "x"), mk (.LiteralInt 3)])) + [] none + (mk (.Assign [⟨.Identifier "x", emd⟩] + (mk (.PrimitiveOp .Add [mk (.Identifier "x"), mk (.LiteralInt 1)])))) + let r := interpStmt trivialEval emptyProc 100 emptyHeap σ₀ whileStmt + getOutcomeAndVar r "x" = some (.normal .vVoid, some (.vInt 3)) + +/-! ## Static Call Tests -/ + +-- Simple static call: procedure that returns its argument + 1 +#guard + let proc : Procedure := { + name := "inc" + inputs := [{ name := "n", type := ⟨.TInt, emd⟩ }] + outputs := [{ name := "result", type := ⟨.TInt, emd⟩ }] + preconditions := [] + determinism := .deterministic none + isFunctional := false + decreases := none + body := .Transparent (mk (.PrimitiveOp .Add [mk (.Identifier "n"), mk (.LiteralInt 1)])) + md := emd + } + let π : ProcEnv := fun name => if name == "inc" then some proc else none + getOutcome (interpStmt trivialEval π 10 emptyHeap emptyStore + (.StaticCall "inc" [mk (.LiteralInt 5)])) + = some (.normal (.vInt 6)) + +-- Static call with return statement +#guard + let proc : Procedure := { + name := "f" + inputs := [{ name := "n", type := ⟨.TInt, emd⟩ }] + outputs := [{ name := "result", type := ⟨.TInt, emd⟩ }] + preconditions := [] + determinism := .deterministic none + isFunctional := false + decreases := none + body := .Transparent (mk (.Return (some (mk (.Identifier "n"))))) + md := emd + } + let π : ProcEnv := fun name => if name == "f" then some proc else none + getOutcome (interpStmt trivialEval π 10 emptyHeap emptyStore + (.StaticCall "f" [mk (.LiteralInt 42)])) + = some (.normal (.vInt 42)) + +-- Static call with void return +#guard + let proc : Procedure := { + name := "g" + inputs := [] + outputs := [] + preconditions := [] + determinism := .deterministic none + isFunctional := false + decreases := none + body := .Transparent (mk (.Return none)) + md := emd + } + let π : ProcEnv := fun name => if name == "g" then some proc else none + getOutcome (interpStmt trivialEval π 10 emptyHeap emptyStore + (.StaticCall "g" [])) + = some (.normal .vVoid) + +/-! ## OO Feature Tests -/ + +-- New allocates an object +#guard + let r := interpStmt trivialEval emptyProc 10 emptyHeap emptyStore (.New "MyClass") + getOutcome r = some (.normal (.vRef 0)) + +-- FieldSelect after PureFieldUpdate +#guard + let r := interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Block [ + mk (.LocalVariable "obj" ⟨.UserDefined "T", emd⟩ (some (mk (.New "T")))), + mk (.PureFieldUpdate (mk (.Identifier "obj")) "f" (mk (.LiteralInt 42))), + mk (.FieldSelect (mk (.Identifier "obj")) "f") + ] none) + getOutcome r = some (.normal (.vInt 42)) + +-- ReferenceEquals: same ref +#guard + let r := interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Block [ + mk (.LocalVariable "obj" ⟨.UserDefined "T", emd⟩ (some (mk (.New "T")))), + mk (.ReferenceEquals (mk (.Identifier "obj")) (mk (.Identifier "obj"))) + ] none) + getOutcome r = some (.normal (.vBool true)) + +-- ReferenceEquals: different refs +#guard + let r := interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Block [ + mk (.LocalVariable "a" ⟨.UserDefined "T", emd⟩ (some (mk (.New "T")))), + mk (.LocalVariable "b" ⟨.UserDefined "T", emd⟩ (some (mk (.New "T")))), + mk (.ReferenceEquals (mk (.Identifier "a")) (mk (.Identifier "b"))) + ] none) + getOutcome r = some (.normal (.vBool false)) + +/-! ## Type Operation Tests -/ + +-- IsType: matching type +#guard + let r := interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Block [ + mk (.LocalVariable "obj" ⟨.UserDefined "Dog", emd⟩ (some (mk (.New "Dog")))), + mk (.IsType (mk (.Identifier "obj")) ⟨.UserDefined "Dog", emd⟩) + ] none) + getOutcome r = some (.normal (.vBool true)) + +-- IsType: non-matching type +#guard + let r := interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Block [ + mk (.LocalVariable "obj" ⟨.UserDefined "Dog", emd⟩ (some (mk (.New "Dog")))), + mk (.IsType (mk (.Identifier "obj")) ⟨.UserDefined "Cat", emd⟩) + ] none) + getOutcome r = some (.normal (.vBool false)) + +-- AsType: pass-through +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.AsType (mk (.LiteralInt 5)) ⟨.TInt, emd⟩)) + = some (.normal (.vInt 5)) + +/-! ## Specification Construct Tests -/ + +-- Old (delegated to δ) +#guard + let δ : LaurelEval := fun σ e => + match e with + | .Old ⟨.Identifier name, _⟩ => σ name.text + | _ => trivialEval σ e + getOutcome (interpStmt δ emptyProc 10 emptyHeap (singleStore "x" (.vInt 99)) + (.Old (mk (.Identifier "x")))) + = some (.normal (.vInt 99)) + +-- Forall (delegated to δ) +#guard + let δ : LaurelEval := fun _ e => + match e with + | .Forall _ _ _ => some (.vBool true) + | _ => none + getOutcome (interpStmt δ emptyProc 10 emptyHeap emptyStore + (.Forall ⟨"x", ⟨.TInt, emd⟩⟩ none (mk (.LiteralBool true)))) + = some (.normal (.vBool true)) + +-- Exists (delegated to δ) +#guard + let δ : LaurelEval := fun _ e => + match e with + | .Exists _ _ _ => some (.vBool true) + | _ => none + getOutcome (interpStmt δ emptyProc 10 emptyHeap emptyStore + (.Exists ⟨"x", ⟨.TInt, emd⟩⟩ none (mk (.LiteralBool true)))) + = some (.normal (.vBool true)) + +/-! ## This Test -/ + +#guard + let σ := singleStore "this" (.vRef 42) + getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap σ .This) + = some (.normal (.vRef 42)) + +/-! ## While Loop with Exit -/ + +#guard + let σ₀ := singleStore "x" (.vInt 0) + let whileStmt := StmtExpr.While + (mk (.LiteralBool true)) [] none + (mk (.Block [ + mk (.Assign [⟨.Identifier "x", emd⟩] + (mk (.PrimitiveOp .Add [mk (.Identifier "x"), mk (.LiteralInt 1)]))), + mk (.IfThenElse + (mk (.PrimitiveOp .Eq [mk (.Identifier "x"), mk (.LiteralInt 3)])) + (mk (.Exit "done")) + none) + ] none)) + let r := interpStmt trivialEval emptyProc 100 emptyHeap σ₀ + (.Block [mk whileStmt] (some "done")) + getOutcomeAndVar r "x" = some (.normal .vVoid, some (.vInt 3)) + +/-! ## While Loop with Return -/ + +#guard + let σ₀ := singleStore "x" (.vInt 0) + let whileStmt := StmtExpr.While + (mk (.LiteralBool true)) [] none + (mk (.Return (some (mk (.LiteralInt 99))))) + let r := interpStmt trivialEval emptyProc 100 emptyHeap σ₀ whileStmt + getOutcome r = some (.ret (some (.vInt 99))) + +/-! ## Field Assignment Test -/ + +#guard + let r := interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Block [ + mk (.LocalVariable "obj" ⟨.UserDefined "T", emd⟩ (some (mk (.New "T")))), + mk (.Assign [⟨.FieldSelect (mk (.Identifier "obj")) "f", emd⟩] (mk (.LiteralInt 7))), + mk (.FieldSelect (mk (.Identifier "obj")) "f") + ] none) + getOutcome r = some (.normal (.vInt 7)) + +/-! ## Instance Call Test -/ + +#guard + let proc : Procedure := { + name := "MyClass.getVal" + inputs := [{ name := "this", type := ⟨.UserDefined "MyClass", emd⟩ }] + outputs := [{ name := "result", type := ⟨.TInt, emd⟩ }] + preconditions := [] + determinism := .deterministic none + isFunctional := false + decreases := none + body := .Transparent (mk (.LiteralInt 100)) + md := emd + } + let π : ProcEnv := fun name => if name == "MyClass.getVal" then some proc else none + let r := interpStmt trivialEval π 10 emptyHeap emptyStore + (.Block [ + mk (.LocalVariable "obj" ⟨.UserDefined "MyClass", emd⟩ (some (mk (.New "MyClass")))), + mk (.InstanceCall (mk (.Identifier "obj")) "getVal" []) + ] none) + getOutcome r = some (.normal (.vInt 100)) + +end Strata.Laurel.InterpreterTest diff --git a/StrataTest/Languages/Laurel/LaurelInterpreterUnitTest.lean b/StrataTest/Languages/Laurel/LaurelInterpreterUnitTest.lean new file mode 100644 index 000000000..28b8ae3f3 --- /dev/null +++ b/StrataTest/Languages/Laurel/LaurelInterpreterUnitTest.lean @@ -0,0 +1,533 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Languages.Laurel.LaurelInterpreter + +/-! +# Comprehensive Unit Tests for Laurel Interpreter + +Covers gaps in `LaurelInterpreterTest.lean`: every `evalPrimOp` case, +edge cases for `interpStmt` constructs, and stuck/error states. +-/ + +namespace Strata.Laurel.InterpreterUnitTest + +open Strata.Laurel + +/-! ## Test Helpers (reused from LaurelInterpreterTest) -/ + +abbrev emd : Imperative.MetaData Core.Expression := .empty + +def mk (s : StmtExpr) : StmtExprMd := ⟨s, emd⟩ + +def emptyStore : LaurelStore := fun _ => none +def emptyHeap : LaurelHeap := fun _ => none +def emptyProc : ProcEnv := fun _ => none + +def trivialEval : 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 + +def singleStore (name : Identifier) (v : LaurelValue) : LaurelStore := + fun x => if x == name.text then some v else none + +def twoStore (n1 : Identifier) (v1 : LaurelValue) (n2 : Identifier) (v2 : LaurelValue) + : LaurelStore := + fun x => if x == n1.text then some v1 else if x == n2.text then some v2 else none + +def getOutcome (r : Option (Outcome × LaurelStore × LaurelHeap)) : Option Outcome := + r.map (·.1) + +def getOutcomeAndVar (r : Option (Outcome × LaurelStore × LaurelHeap)) + (name : Identifier) : Option (Outcome × Option LaurelValue) := + r.map (fun (o, σ, _) => (o, σ name.text)) + +/-! ## evalPrimOp: Arithmetic -/ + +-- Sub +#guard evalPrimOp .Sub [.vInt 10, .vInt 3] = some (.vInt 7) +#guard evalPrimOp .Sub [.vInt 0, .vInt 5] = some (.vInt (-5)) + +-- Mul +#guard evalPrimOp .Mul [.vInt 4, .vInt 5] = some (.vInt 20) +#guard evalPrimOp .Mul [.vInt 0, .vInt 99] = some (.vInt 0) + +-- Div (non-zero) +#guard evalPrimOp .Div [.vInt 10, .vInt 3] = some (.vInt 3) +#guard evalPrimOp .Div [.vInt (-7), .vInt 2] = some (.vInt (-4)) + +-- Mod (non-zero) +#guard evalPrimOp .Mod [.vInt 10, .vInt 3] = some (.vInt 1) +#guard evalPrimOp .Mod [.vInt (-7), .vInt 2] = some (.vInt 1) + +-- Neg +#guard evalPrimOp .Neg [.vInt 5] = some (.vInt (-5)) +#guard evalPrimOp .Neg [.vInt (-3)] = some (.vInt 3) +#guard evalPrimOp .Neg [.vInt 0] = some (.vInt 0) + +/-! ## evalPrimOp: Division by zero -/ + +#guard evalPrimOp .Div [.vInt 5, .vInt 0] = none +#guard evalPrimOp .Mod [.vInt 5, .vInt 0] = none +#guard evalPrimOp .DivT [.vInt 5, .vInt 0] = none +#guard evalPrimOp .ModT [.vInt 5, .vInt 0] = none + +/-! ## evalPrimOp: Truncation division and modulus -/ + +-- DivT (truncation toward zero) +#guard evalPrimOp .DivT [.vInt 7, .vInt 2] = some (.vInt 3) +#guard evalPrimOp .DivT [.vInt (-7), .vInt 2] = some (.vInt (-3)) +#guard evalPrimOp .DivT [.vInt 7, .vInt (-2)] = some (.vInt (-3)) +#guard evalPrimOp .DivT [.vInt (-7), .vInt (-2)] = some (.vInt 3) + +-- ModT (truncation modulus) +#guard evalPrimOp .ModT [.vInt 7, .vInt 2] = some (.vInt 1) +#guard evalPrimOp .ModT [.vInt (-7), .vInt 2] = some (.vInt (-1)) +#guard evalPrimOp .ModT [.vInt 7, .vInt (-2)] = some (.vInt 1) +#guard evalPrimOp .ModT [.vInt (-7), .vInt (-2)] = some (.vInt (-1)) + +-- Short-circuit ops return none in evalPrimOp (handled in interpStmt) +#guard evalPrimOp .AndThen [.vBool true, .vBool false] = none +#guard evalPrimOp .OrElse [.vBool false, .vBool true] = none +#guard evalPrimOp .Implies [.vBool false, .vBool true] = none + +/-! ## evalPrimOp: Comparison -/ + +-- Neq (int) +#guard evalPrimOp .Neq [.vInt 1, .vInt 2] = some (.vBool true) +#guard evalPrimOp .Neq [.vInt 3, .vInt 3] = some (.vBool false) + +-- Leq +#guard evalPrimOp .Leq [.vInt 3, .vInt 5] = some (.vBool true) +#guard evalPrimOp .Leq [.vInt 5, .vInt 5] = some (.vBool true) +#guard evalPrimOp .Leq [.vInt 6, .vInt 5] = some (.vBool false) + +-- Gt +#guard evalPrimOp .Gt [.vInt 5, .vInt 3] = some (.vBool true) +#guard evalPrimOp .Gt [.vInt 3, .vInt 3] = some (.vBool false) + +-- Geq +#guard evalPrimOp .Geq [.vInt 5, .vInt 3] = some (.vBool true) +#guard evalPrimOp .Geq [.vInt 3, .vInt 3] = some (.vBool true) +#guard evalPrimOp .Geq [.vInt 2, .vInt 3] = some (.vBool false) + +/-! ## evalPrimOp: Boolean -/ + +-- Or +#guard evalPrimOp .Or [.vBool false, .vBool false] = some (.vBool false) +#guard evalPrimOp .Or [.vBool true, .vBool false] = some (.vBool true) +#guard evalPrimOp .Or [.vBool false, .vBool true] = some (.vBool true) + +-- Implies (handled in interpStmt as short-circuit; evalPrimOp returns none) +#guard evalPrimOp .Implies [.vBool true, .vBool false] = none +#guard evalPrimOp .Implies [.vBool false, .vBool false] = none +#guard evalPrimOp .Implies [.vBool true, .vBool true] = none + +/-! ## evalPrimOp: String -/ + +-- Eq on strings +#guard evalPrimOp .Eq [.vString "abc", .vString "abc"] = some (.vBool true) +#guard evalPrimOp .Eq [.vString "abc", .vString "def"] = some (.vBool false) + +-- Neq on strings +#guard evalPrimOp .Neq [.vString "a", .vString "b"] = some (.vBool true) +#guard evalPrimOp .Neq [.vString "a", .vString "a"] = some (.vBool false) + +/-! ## evalPrimOp: Ref -/ + +-- Eq on refs +#guard evalPrimOp .Eq [.vRef 0, .vRef 0] = some (.vBool true) +#guard evalPrimOp .Eq [.vRef 0, .vRef 1] = some (.vBool false) + +-- Neq on refs +#guard evalPrimOp .Neq [.vRef 0, .vRef 1] = some (.vBool true) +#guard evalPrimOp .Neq [.vRef 0, .vRef 0] = some (.vBool false) + +/-! ## evalPrimOp: Bool Eq/Neq -/ + +#guard evalPrimOp .Eq [.vBool true, .vBool true] = some (.vBool true) +#guard evalPrimOp .Eq [.vBool true, .vBool false] = some (.vBool false) +#guard evalPrimOp .Neq [.vBool true, .vBool false] = some (.vBool true) +#guard evalPrimOp .Neq [.vBool true, .vBool true] = some (.vBool false) + +/-! ## evalPrimOp: Type mismatch → none -/ + +#guard evalPrimOp .Add [.vBool true, .vInt 1] = none +#guard evalPrimOp .Add [.vInt 1, .vBool true] = none +#guard evalPrimOp .And [.vInt 1, .vInt 2] = none +#guard evalPrimOp .Or [.vInt 1, .vInt 2] = none +#guard evalPrimOp .Not [.vInt 1] = none +#guard evalPrimOp .Lt [.vBool true, .vBool false] = none +#guard evalPrimOp .Sub [.vString "a", .vString "b"] = none +#guard evalPrimOp .Neg [.vBool true] = none +#guard evalPrimOp .Implies [.vInt 1, .vInt 2] = none +#guard evalPrimOp .StrConcat [.vInt 1, .vInt 2] = none + +/-! ## evalPrimOp: Wrong arity → none -/ + +#guard evalPrimOp .Add [.vInt 1] = none +#guard evalPrimOp .Add [.vInt 1, .vInt 2, .vInt 3] = none +#guard evalPrimOp .Not [.vBool true, .vBool false] = none +#guard evalPrimOp .Not [] = none +#guard evalPrimOp .Neg [] = none +#guard evalPrimOp .Eq [.vInt 1] = none +#guard evalPrimOp .And [.vBool true] = none + +/-! ## interpStmt: LiteralDecimal → none -/ + +-- LiteralDecimal has no runtime representation +#guard interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.LiteralDecimal ⟨1, 5⟩) = none + +/-! ## interpStmt: Shadowed variable -/ + +-- Variable shadowing: inner declaration shadows outer +#guard + let σ₀ := singleStore "x" (.vInt 1) + let r := interpStmt trivialEval emptyProc 10 emptyHeap σ₀ (.Identifier "x") + getOutcome r = some (.normal (.vInt 1)) + +/-! ## interpStmt: IfThenElse edge cases -/ + +-- Condition evaluates to non-bool → none (stuck) +#guard interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.IfThenElse (mk (.LiteralInt 1)) (mk (.LiteralInt 2)) (some (mk (.LiteralInt 3)))) = none + +-- Condition evaluates to non-bool, no else → none +#guard interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.IfThenElse (mk (.LiteralInt 1)) (mk (.LiteralInt 2)) none) = none + +-- Exit in then-branch propagates +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.IfThenElse (mk (.LiteralBool true)) (mk (.Exit "L")) (some (mk (.LiteralInt 2))))) + = some (.exit "L") + +-- Return in condition propagates (condition stuck since return is not normal) +#guard interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.IfThenElse (mk (.Return (some (mk (.LiteralInt 1))))) (mk (.LiteralInt 2)) none) = none + +/-! ## interpStmt: While edge cases -/ + +-- False guard on first iteration → void, body never executes +#guard + let σ₀ := singleStore "x" (.vInt 0) + let r := interpStmt trivialEval emptyProc 10 emptyHeap σ₀ + (.While (mk (.LiteralBool false)) [] none + (mk (.Assign [⟨.Identifier "x", emd⟩] (mk (.LiteralInt 99))))) + getOutcomeAndVar r "x" = some (.normal .vVoid, some (.vInt 0)) + +-- Return with value in loop body +#guard + let σ₀ := singleStore "x" (.vInt 0) + let r := interpStmt trivialEval emptyProc 100 emptyHeap σ₀ + (.While (mk (.LiteralBool true)) [] none + (mk (.Return (some (mk (.Identifier "x")))))) + getOutcome r = some (.ret (some (.vInt 0))) + +-- Non-bool guard → none +#guard interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.While (mk (.LiteralInt 1)) [] none (mk (.LiteralInt 2))) = none + +/-! ## interpStmt: LocalVariable re-declaration → none -/ + +-- initStore fails when variable already exists +#guard + let σ₀ := singleStore "x" (.vInt 1) + interpStmt trivialEval emptyProc 10 emptyHeap σ₀ + (.LocalVariable "x" ⟨.TInt, emd⟩ (some (mk (.LiteralInt 2)))) = none + +-- Uninit re-declaration also fails +#guard + let σ₀ := singleStore "x" (.vInt 1) + interpStmt trivialEval emptyProc 10 emptyHeap σ₀ + (.LocalVariable "x" ⟨.TInt, emd⟩ none) = none + +/-! ## interpStmt: Assign to undefined variable → none -/ + +#guard interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Assign [⟨.Identifier "undef", emd⟩] (mk (.LiteralInt 1))) = none + +/-! ## interpStmt: Assert false → none -/ + +#guard interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Assert (mk (.LiteralBool false))) = none + +-- Assert non-bool → none +#guard interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Assert (mk (.LiteralInt 1))) = none + +/-! ## interpStmt: Assume false → none -/ + +#guard interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Assume (mk (.LiteralBool false))) = none + +-- Assume non-bool → none +#guard interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Assume (mk (.LiteralInt 1))) = none + +/-! ## interpStmt: Block exit/return propagation -/ + +-- Exit propagates past non-matching label +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Block [mk (.Exit "X")] (some "Y"))) + = some (.exit "X") + +-- Return propagates through any block (even labeled) +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Block [mk (.Return (some (mk (.LiteralInt 42))))] (some "L"))) + = some (.ret (some (.vInt 42))) + +-- Return propagates through unlabeled block +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Block [mk (.Return none), mk (.LiteralInt 99)] none)) + = some (.ret none) + +/-! ## interpStmt: StaticCall edge cases -/ + +-- Undefined procedure → none +#guard interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.StaticCall "nonexistent" []) = none + +-- Wrong number of arguments → none (bindParams fails) +#guard + let proc : Procedure := { + name := "f" + inputs := [{ name := "a", type := ⟨.TInt, emd⟩ }, { name := "b", type := ⟨.TInt, emd⟩ }] + outputs := [] + preconditions := [] + determinism := .deterministic none + isFunctional := false + decreases := none + body := .Transparent (mk (.LiteralInt 0)) + md := emd + } + let π : ProcEnv := fun name => if name == "f" then some proc else none + interpStmt trivialEval π 10 emptyHeap emptyStore + (.StaticCall "f" [mk (.LiteralInt 1)]) = none + +-- Procedure with Abstract body → none +#guard + let proc : Procedure := { + name := "g" + inputs := [] + outputs := [] + preconditions := [] + determinism := .deterministic none + isFunctional := false + decreases := none + body := .Abstract [] + md := emd + } + let π : ProcEnv := fun name => if name == "g" then some proc else none + interpStmt trivialEval π 10 emptyHeap emptyStore + (.StaticCall "g" []) = none + +-- Procedure with External body → none +#guard + let proc : Procedure := { + name := "h" + inputs := [] + outputs := [] + preconditions := [] + determinism := .deterministic none + isFunctional := false + decreases := none + body := .External + md := emd + } + let π : ProcEnv := fun name => if name == "h" then some proc else none + interpStmt trivialEval π 10 emptyHeap emptyStore + (.StaticCall "h" []) = none + +/-! ## interpStmt: FieldSelect edge cases -/ + +-- FieldSelect on non-ref → none +#guard interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.FieldSelect (mk (.LiteralInt 5)) "f") = none + +-- FieldSelect on ref with undefined field → none +#guard + let r := interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Block [ + mk (.LocalVariable "obj" ⟨.UserDefined "T", emd⟩ (some (mk (.New "T")))), + mk (.FieldSelect (mk (.Identifier "obj")) "nonexistent") + ] none) + r = none + +/-! ## interpStmt: New allocates sequential addresses -/ + +-- First allocation gets address 0 +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.New "T")) = some (.normal (.vRef 0)) + +-- Second allocation gets address 1 +#guard + let r := interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Block [ + mk (.LocalVariable "a" ⟨.UserDefined "T", emd⟩ (some (mk (.New "T")))), + mk (.New "T") + ] none) + getOutcome r = some (.normal (.vRef 1)) + +-- Third allocation gets address 2 +#guard + let r := interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Block [ + mk (.LocalVariable "a" ⟨.UserDefined "T", emd⟩ (some (mk (.New "T")))), + mk (.LocalVariable "b" ⟨.UserDefined "T", emd⟩ (some (mk (.New "T")))), + mk (.New "T") + ] none) + getOutcome r = some (.normal (.vRef 2)) + +/-! ## interpStmt: PureFieldUpdate on non-ref → none -/ + +#guard interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.PureFieldUpdate (mk (.LiteralInt 5)) "f" (mk (.LiteralInt 1))) = none + +/-! ## interpStmt: ContractOf delegated to δ -/ + +#guard + let δ : LaurelEval := fun _ e => + match e with + | .ContractOf .Precondition _ => some (.vBool true) + | _ => none + getOutcome (interpStmt δ emptyProc 10 emptyHeap emptyStore + (.ContractOf .Precondition (mk (.Identifier "f")))) + = some (.normal (.vBool true)) + +-- ContractOf with trivialEval (no handler) → none +#guard interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.ContractOf .Precondition (mk (.Identifier "f"))) = none + +/-! ## interpStmt: Fresh delegated to δ -/ + +#guard + let δ : LaurelEval := fun _ e => + match e with + | .Fresh _ => some (.vBool true) + | _ => none + getOutcome (interpStmt δ emptyProc 10 emptyHeap emptyStore + (.Fresh (mk (.Identifier "x")))) + = some (.normal (.vBool true)) + +/-! ## interpStmt: Assigned delegated to δ -/ + +#guard + let δ : LaurelEval := fun _ e => + match e with + | .Assigned _ => some (.vBool false) + | _ => none + getOutcome (interpStmt δ emptyProc 10 emptyHeap emptyStore + (.Assigned (mk (.Identifier "x")))) + = some (.normal (.vBool false)) + +/-! ## interpStmt: Multi-target Assign → none -/ + +#guard interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Assign [⟨.Identifier "x", emd⟩, ⟨.Identifier "y", emd⟩] (mk (.LiteralInt 1))) = none + +/-! ## interpStmt: Short-circuit AndThen/OrElse/Implies via interpStmt -/ + +-- AndThen short-circuits: false && (stuck) → false +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.PrimitiveOp .AndThen [mk (.LiteralBool false), mk (.Identifier "undef")])) + = some (.normal (.vBool false)) + +-- OrElse short-circuits: true || (stuck) → true +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.PrimitiveOp .OrElse [mk (.LiteralBool true), mk (.Identifier "undef")])) + = some (.normal (.vBool true)) + +-- Implies short-circuits: false => (stuck) → true +#guard getOutcome (interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.PrimitiveOp .Implies [mk (.LiteralBool false), mk (.Identifier "undef")])) + = some (.normal (.vBool true)) + +-- AndThen does NOT short-circuit on true: true && undef → none +#guard interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.PrimitiveOp .AndThen [mk (.LiteralBool true), mk (.Identifier "undef")]) = none + +-- OrElse does NOT short-circuit on false: false || undef → none +#guard interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.PrimitiveOp .OrElse [mk (.LiteralBool false), mk (.Identifier "undef")]) = none + +-- Implies does NOT short-circuit on true: true => undef → none +#guard interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.PrimitiveOp .Implies [mk (.LiteralBool true), mk (.Identifier "undef")]) = none + +/-! ## interpStmt: ReferenceEquals on non-ref → none -/ + +#guard interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.ReferenceEquals (mk (.LiteralInt 1)) (mk (.LiteralInt 1))) = none + +/-! ## interpStmt: This with no "this" in store → none -/ + +#guard interpStmt trivialEval emptyProc 10 emptyHeap emptyStore .This = none + +/-! ## interpStmt: IsType on non-ref → none -/ + +#guard interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.IsType (mk (.LiteralInt 5)) ⟨.UserDefined "T", emd⟩) = none + +/-! ## interpStmt: Opaque procedure with implementation -/ + +#guard + let proc : Procedure := { + name := "f" + inputs := [{ name := "n", type := ⟨.TInt, emd⟩ }] + outputs := [] + preconditions := [] + determinism := .deterministic none + isFunctional := false + decreases := none + body := .Opaque [] (some (mk (.PrimitiveOp .Add [mk (.Identifier "n"), mk (.LiteralInt 1)]))) [] + md := emd + } + let π : ProcEnv := fun name => if name == "f" then some proc else none + getOutcome (interpStmt trivialEval π 10 emptyHeap emptyStore + (.StaticCall "f" [mk (.LiteralInt 5)])) + = some (.normal (.vInt 6)) + +-- Opaque procedure without implementation → none +#guard + let proc : Procedure := { + name := "f" + inputs := [] + outputs := [] + preconditions := [] + determinism := .deterministic none + isFunctional := false + decreases := none + body := .Opaque [] none [] + md := emd + } + let π : ProcEnv := fun name => if name == "f" then some proc else none + interpStmt trivialEval π 10 emptyHeap emptyStore + (.StaticCall "f" []) = none + +/-! ## interpStmt: Field assignment to unallocated ref → none -/ + +#guard interpStmt trivialEval emptyProc 10 emptyHeap emptyStore + (.Assign [⟨.FieldSelect (mk (.LiteralInt 5)) "f", emd⟩] (mk (.LiteralInt 1))) = none + +/-! ## interpBlock: fuel exhaustion -/ + +#guard interpBlock trivialEval emptyProc 0 emptyHeap emptyStore [mk (.LiteralInt 1)] = none + +/-! ## interpArgs: fuel exhaustion -/ + +#guard interpArgs trivialEval emptyProc 0 emptyHeap emptyStore [mk (.LiteralInt 1)] = none + +/-! ## interpArgs: stuck argument → none -/ + +#guard interpArgs trivialEval emptyProc 10 emptyHeap emptyStore + [mk (.LiteralInt 1), mk (.Identifier "undef")] = none + +end Strata.Laurel.InterpreterUnitTest