From c972ae12fb2e97919de1a27b3f9989ea865fd60c Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Tue, 3 Mar 2026 17:59:22 -0500 Subject: [PATCH 1/2] feat(laurel): Add direct operational semantics for Laurel IR MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Implement Option A from design-formal-semantics-for-laurel-ir.md: a standalone big-step operational semantics for all ~35 Laurel StmtExpr constructors, independent of Core semantics. New files: - Strata/Languages/Laurel/LaurelSemantics.lean: Core semantic definitions including LaurelValue, LaurelStore, LaurelHeap, Outcome types, and mutually inductive EvalLaurelStmt/EvalLaurelBlock relations covering literals, variables, primitive operations, control flow (if/while/ block/exit/return), assignments, verification constructs (assert/ assume), static calls, OO features (new/field select/instance call/ reference equals/is type/as type), and specification constructs (forall/exists/old/fresh/assigned/prove by/contract of). - Strata/Languages/Laurel/LaurelSemanticsProps.lean: Properties including store monotonicity (UpdateStore/InitStore preserve definedness), store operation determinism, catchExit properties, evalPrimOp determinism, and block value semantics. Full evaluation determinism theorem is stated but admitted (requires mutual induction). - StrataTest/Languages/Laurel/LaurelSemanticsTest.lean: 30+ concrete evaluation tests covering literals, identifiers, primitive ops (add, and, not, lt, strconcat), blocks (empty, singleton, multi-statement), if-then-else (true/false/no-else), exit (propagation, labeled catch, non-matching), return (with/without value, short-circuit), local variables (init/uninit), assert/assume, prove-by, nested control flow, and evalPrimOp/catchExit unit tests. - docs/designs/design-formal-semantics-for-laurel-ir.md: Design document describing three options (A: direct, B: shallow, C: hybrid) with recommendation for Option C. This implementation is Option A, serving as a reference semantics for translation correctness proofs. Design decisions: - Outcome type explicitly models non-local control flow (exit/return) - EvalArgs uses the expression evaluator δ (non-mutual) for call argument evaluation, avoiding Lean 4 mutual inductive limitations - Heap model is separate from store for OO features - Specification constructs (forall, exists, old, fresh, assigned, contract_of) are delegated to the expression evaluator δ - Static/instance calls restore the caller store after body evaluation Known limitations: - Determinism theorem is admitted (sorry) - requires careful mutual induction over EvalLaurelStmt/EvalLaurelBlock - While loop semantics only captures terminating executions (inductive) - Call argument evaluation uses δ rather than full EvalLaurelStmt (avoids mutual inductive nesting issues in Lean 4) - Translation correctness proof is out of scope (separate task) --- Strata.lean | 2 + Strata/Languages/Laurel/LaurelSemantics.lean | 399 +++++++++++++ .../Laurel/LaurelSemanticsProps.lean | 131 +++++ .../Languages/Laurel/LaurelSemanticsTest.lean | 260 +++++++++ .../design-formal-semantics-for-laurel-ir.md | 526 ++++++++++++++++++ 5 files changed, 1318 insertions(+) create mode 100644 Strata/Languages/Laurel/LaurelSemantics.lean create mode 100644 Strata/Languages/Laurel/LaurelSemanticsProps.lean create mode 100644 StrataTest/Languages/Laurel/LaurelSemanticsTest.lean create mode 100644 docs/designs/design-formal-semantics-for-laurel-ir.md diff --git a/Strata.lean b/Strata.lean index 7fa76e821..0d098794b 100644 --- a/Strata.lean +++ b/Strata.lean @@ -24,6 +24,8 @@ import Strata.Languages.Core.FactoryWF import Strata.Languages.Core.StatementSemantics import Strata.Languages.Core.SarifOutput import Strata.Languages.Laurel.LaurelToCoreTranslator +import Strata.Languages.Laurel.LaurelSemantics +import Strata.Languages.Laurel.LaurelSemanticsProps /- Code Transforms -/ import Strata.Transform.CallElimCorrect diff --git a/Strata/Languages/Laurel/LaurelSemantics.lean b/Strata/Languages/Laurel/LaurelSemantics.lean new file mode 100644 index 000000000..69e29a7b8 --- /dev/null +++ b/Strata/Languages/Laurel/LaurelSemantics.lean @@ -0,0 +1,399 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Languages.Laurel.Laurel + +/-! +# Direct Operational Semantics for Laurel IR + +This file defines a standalone big-step operational semantics for Laurel's +`StmtExpr` AST, independent of Core semantics (Option A from the design +document `docs/designs/design-formal-semantics-for-laurel-ir.md`). + +## Design + +- **LaurelValue**: runtime values (int, bool, string, void, ref) +- **LaurelStore**: variable store (`Identifier → Option LaurelValue`) +- **LaurelHeap**: object heap (`Nat → Option (Identifier × (Identifier → Option LaurelValue))`) +- **Outcome**: non-local control flow (normal, exit, return) +- **EvalLaurelStmt / EvalLaurelBlock**: mutually inductive big-step relations + +The judgment form is: `δ, π, heap, σ, stmt ⊢ heap', σ', outcome` +-/ + +namespace Strata.Laurel + +/-! ## 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 -/ + +abbrev LaurelStore := Identifier → Option LaurelValue +abbrev LaurelHeap := Nat → Option (Identifier × (Identifier → Option LaurelValue)) +abbrev LaurelEval := LaurelStore → StmtExpr → Option LaurelValue +abbrev ProcEnv := Identifier → Option Procedure + +/-! ## Outcomes -/ + +inductive Outcome where + | normal : LaurelValue → Outcome + | exit : Identifier → Outcome + | ret : Option LaurelValue → Outcome + deriving Repr, BEq, Inhabited, DecidableEq + +/-! ## Store Operations -/ + +inductive UpdateStore : LaurelStore → Identifier → LaurelValue → LaurelStore → Prop where + | update : + σ x = .some v' → + σ' x = .some v → + (∀ y, x ≠ y → σ' y = σ y) → + UpdateStore σ x v σ' + +inductive InitStore : LaurelStore → Identifier → LaurelValue → LaurelStore → Prop where + | init : + σ x = none → + σ' x = .some v → + (∀ y, x ≠ y → σ' y = σ y) → + InitStore σ x v σ' + +/-! ## Heap Operations -/ + +inductive AllocHeap : LaurelHeap → Identifier → Nat → LaurelHeap → Prop where + | alloc : + h addr = none → + 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 : Identifier) : Option LaurelValue := + match h addr with + | some (_, fields) => fields field + | none => none + +inductive HeapFieldWrite : LaurelHeap → Nat → Identifier → 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 Identifier → 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, [.vBool a, .vBool b] => some (.vBool (a && b)) + | .Or, [.vBool a, .vBool b] => some (.vBool (a || b)) + | .Not, [.vBool a] => some (.vBool (!a)) + | .Implies, [.vBool a, .vBool b] => some (.vBool (!a || b)) + | .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 + | .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)) + | _, _ => none + +def getBody : Procedure → Option StmtExprMd + | { body := .Transparent b, .. } => some b + | { body := .Opaque _ (some b) _, .. } => some b + | _ => none + +def bindParams (σ : LaurelStore) (params : List Parameter) (vals : List LaurelValue) + : Option LaurelStore := + match params, vals with + | [], [] => some σ + | p :: ps, v :: vs => + if σ p.name = none then + bindParams (fun x => if x == p.name then some v else σ x) ps vs + else none + | _, _ => none + +def HighType.typeName : HighType → Identifier + | .UserDefined name => name + | _ => "" + +/-- Non-mutual argument evaluation using the expression evaluator δ. -/ +inductive EvalArgs : LaurelEval → LaurelStore → List StmtExprMd → List LaurelValue → Prop where + | nil : EvalArgs δ σ [] [] + | cons : δ σ e.val = some v → EvalArgs δ σ es vs → EvalArgs δ σ (e :: es) (v :: vs) + +/-! ## Main Semantic Relations -/ + +mutual +inductive EvalLaurelStmt : + LaurelEval → ProcEnv → LaurelHeap → LaurelStore → + StmtExprMd → LaurelHeap → LaurelStore → Outcome → Prop where + + -- Literals + + | literal_int : + EvalLaurelStmt δ π h σ ⟨.LiteralInt i, md⟩ h σ (.normal (.vInt i)) + + | literal_bool : + EvalLaurelStmt δ π h σ ⟨.LiteralBool b, md⟩ h σ (.normal (.vBool b)) + + | literal_string : + EvalLaurelStmt δ π h σ ⟨.LiteralString s, md⟩ h σ (.normal (.vString s)) + + -- Variables + + | identifier : + σ name = some v → + EvalLaurelStmt δ π h σ ⟨.Identifier name, md⟩ h σ (.normal v) + + -- Primitive Operations (uses non-mutual EvalArgs) + + | prim_op : + EvalArgs δ σ args vals → + evalPrimOp op vals = some result → + EvalLaurelStmt δ π h σ ⟨.PrimitiveOp op args, md⟩ h σ (.normal result) + + -- Control Flow + + | ite_true : + EvalLaurelStmt δ π h σ c h₁ σ₁ (.normal (.vBool true)) → + EvalLaurelStmt δ π h₁ σ₁ thenBr h₂ σ₂ outcome → + EvalLaurelStmt δ π h σ ⟨.IfThenElse c thenBr (some elseBr), md⟩ h₂ σ₂ outcome + + | ite_false : + EvalLaurelStmt δ π h σ c h₁ σ₁ (.normal (.vBool false)) → + EvalLaurelStmt δ π h₁ σ₁ elseBr h₂ σ₂ outcome → + EvalLaurelStmt δ π h σ ⟨.IfThenElse c thenBr (some elseBr), md⟩ h₂ σ₂ outcome + + | ite_true_no_else : + EvalLaurelStmt δ π h σ c h₁ σ₁ (.normal (.vBool true)) → + EvalLaurelStmt δ π h₁ σ₁ thenBr h₂ σ₂ outcome → + EvalLaurelStmt δ π h σ ⟨.IfThenElse c thenBr none, md⟩ h₂ σ₂ outcome + + | ite_false_no_else : + EvalLaurelStmt δ π h σ c h₁ σ₁ (.normal (.vBool false)) → + EvalLaurelStmt δ π h σ ⟨.IfThenElse c thenBr none, md⟩ h₁ σ₁ (.normal .vVoid) + + | block_sem : + EvalLaurelBlock δ π h σ stmts h' σ' outcome → + catchExit label outcome = outcome' → + EvalLaurelStmt δ π h σ ⟨.Block stmts label, md⟩ h' σ' outcome' + + | exit_sem : + EvalLaurelStmt δ π h σ ⟨.Exit target, md⟩ h σ (.exit target) + + | return_some : + EvalLaurelStmt δ π h σ val h' σ' (.normal v) → + EvalLaurelStmt δ π h σ ⟨.Return (some val), md⟩ h' σ' (.ret (some v)) + + | return_none : + EvalLaurelStmt δ π h σ ⟨.Return none, md⟩ h σ (.ret none) + + -- While Loop + + | while_true : + EvalLaurelStmt δ π h σ c h₁ σ₁ (.normal (.vBool true)) → + EvalLaurelStmt δ π h₁ σ₁ body h₂ σ₂ (.normal _) → + EvalLaurelStmt δ π h₂ σ₂ ⟨.While c invs dec body, md⟩ h₃ σ₃ outcome → + EvalLaurelStmt δ π h σ ⟨.While c invs dec body, md⟩ h₃ σ₃ outcome + + | while_false : + EvalLaurelStmt δ π h σ c h₁ σ₁ (.normal (.vBool false)) → + EvalLaurelStmt δ π h σ ⟨.While c invs dec body, md⟩ h₁ σ₁ (.normal .vVoid) + + | while_exit : + EvalLaurelStmt δ π h σ c h₁ σ₁ (.normal (.vBool true)) → + EvalLaurelStmt δ π h₁ σ₁ body h₂ σ₂ (.exit label) → + EvalLaurelStmt δ π h σ ⟨.While c invs dec body, md⟩ h₂ σ₂ (.exit label) + + | while_return : + EvalLaurelStmt δ π h σ c h₁ σ₁ (.normal (.vBool true)) → + EvalLaurelStmt δ π h₁ σ₁ body h₂ σ₂ (.ret rv) → + EvalLaurelStmt δ π h σ ⟨.While c invs dec body, md⟩ h₂ σ₂ (.ret rv) + + -- Assignments + + | assign_single : + EvalLaurelStmt δ π h σ value h₁ σ₁ (.normal v) → + σ₁ name = some _ → + UpdateStore σ₁ name v σ₂ → + EvalLaurelStmt δ π h σ ⟨.Assign [⟨.Identifier name, tmd⟩] value, md⟩ h₁ σ₂ (.normal .vVoid) + + | local_var_init : + EvalLaurelStmt δ π h σ init h₁ σ₁ (.normal v) → + σ₁ name = none → + InitStore σ₁ name v σ₂ → + EvalLaurelStmt δ π h σ ⟨.LocalVariable name ty (some init), md⟩ h₁ σ₂ (.normal .vVoid) + + | local_var_uninit : + σ name = none → + InitStore σ name .vVoid σ' → + EvalLaurelStmt δ π h σ ⟨.LocalVariable name ty none, md⟩ h σ' (.normal .vVoid) + + -- Verification Constructs + + | assert_true : + EvalLaurelStmt δ π h σ c h σ (.normal (.vBool true)) → + EvalLaurelStmt δ π h σ ⟨.Assert c, md⟩ h σ (.normal .vVoid) + + | assume_true : + EvalLaurelStmt δ π h σ c h σ (.normal (.vBool true)) → + EvalLaurelStmt δ π h σ ⟨.Assume c, md⟩ h σ (.normal .vVoid) + + -- Static Calls (arguments evaluated via δ for simplicity) + + | static_call : + π callee = some proc → + EvalArgs δ σ args vals → + bindParams σ proc.inputs vals = some σBound → + getBody proc = some body → + EvalLaurelStmt δ π h σBound body h' σ' (.normal v) → + EvalLaurelStmt δ π h σ ⟨.StaticCall callee args, md⟩ h' σ (.normal v) + + | static_call_return : + π callee = some proc → + EvalArgs δ σ args vals → + bindParams σ proc.inputs vals = some σBound → + getBody proc = some body → + EvalLaurelStmt δ π h σBound body h' σ' (.ret (some v)) → + EvalLaurelStmt δ π h σ ⟨.StaticCall callee args, md⟩ h' σ (.normal v) + + -- OO Features + + | new_obj : + AllocHeap h typeName addr h' → + EvalLaurelStmt δ π h σ ⟨.New typeName, md⟩ h' σ (.normal (.vRef addr)) + + | field_select : + EvalLaurelStmt δ π h σ target h₁ σ₁ (.normal (.vRef addr)) → + heapFieldRead h₁ addr fieldName = some v → + EvalLaurelStmt δ π h σ ⟨.FieldSelect target fieldName, md⟩ h₁ σ₁ (.normal v) + + | pure_field_update : + EvalLaurelStmt δ π h σ target h₁ σ₁ (.normal (.vRef addr)) → + EvalLaurelStmt δ π h₁ σ₁ newVal h₂ σ₂ (.normal v) → + HeapFieldWrite h₂ addr fieldName v h₃ → + EvalLaurelStmt δ π h σ ⟨.PureFieldUpdate target fieldName newVal, md⟩ h₃ σ₂ (.normal (.vRef addr)) + + | reference_equals : + EvalLaurelStmt δ π h σ lhs h₁ σ₁ (.normal (.vRef a)) → + EvalLaurelStmt δ π h₁ σ₁ rhs h₂ σ₂ (.normal (.vRef b)) → + EvalLaurelStmt δ π h σ ⟨.ReferenceEquals lhs rhs, md⟩ h₂ σ₂ (.normal (.vBool (a == b))) + + | instance_call : + EvalLaurelStmt δ π h σ target h₁ σ₁ (.normal (.vRef addr)) → + h₁ addr = some (typeName, _) → + π (typeName ++ "." ++ callee) = some proc → + EvalArgs δ σ₁ args vals → + bindParams σ₁ proc.inputs ((.vRef addr) :: vals) = some σBound → + getBody proc = some body → + EvalLaurelStmt δ π h₁ σBound body h₂ σ₂ (.normal v) → + EvalLaurelStmt δ π h σ ⟨.InstanceCall target callee args, md⟩ h₂ σ₁ (.normal v) + + | this_sem : + σ "this" = some v → + EvalLaurelStmt δ π h σ ⟨.This, md⟩ h σ (.normal v) + + -- Type Operations + + | is_type : + EvalLaurelStmt δ π h σ target h₁ σ₁ (.normal (.vRef addr)) → + h₁ addr = some (actualType, _) → + EvalLaurelStmt δ π h σ ⟨.IsType target ty, md⟩ h₁ σ₁ + (.normal (.vBool (actualType == ty.val.typeName))) + + | as_type : + EvalLaurelStmt δ π h σ target h₁ σ₁ (.normal v) → + EvalLaurelStmt δ π h σ ⟨.AsType target ty, md⟩ h₁ σ₁ (.normal v) + + -- Quantifiers (specification-only, delegated to δ) + + | forall_sem : + δ σ (.Forall name ty body) = some v → + EvalLaurelStmt δ π h σ ⟨.Forall name ty body, md⟩ h σ (.normal v) + + | exists_sem : + δ σ (.Exists name ty body) = some v → + EvalLaurelStmt δ π h σ ⟨.Exists name ty body, md⟩ h σ (.normal v) + + -- Specification Constructs (delegated to δ) + + | old_sem : + δ σ (.Old val) = some v → + EvalLaurelStmt δ π h σ ⟨.Old val, md⟩ h σ (.normal v) + + | fresh_sem : + δ σ (.Fresh val) = some v → + EvalLaurelStmt δ π h σ ⟨.Fresh val, md⟩ h σ (.normal v) + + | assigned_sem : + δ σ (.Assigned name) = some v → + EvalLaurelStmt δ π h σ ⟨.Assigned name, md⟩ h σ (.normal v) + + | prove_by : + EvalLaurelStmt δ π h σ value h' σ' outcome → + EvalLaurelStmt δ π h σ ⟨.ProveBy value proof, md⟩ h' σ' outcome + + | contract_of : + δ σ (.ContractOf ct func) = some v → + EvalLaurelStmt δ π h σ ⟨.ContractOf ct func, md⟩ h σ (.normal v) + + -- Field Assignment + + | assign_field : + EvalLaurelStmt δ π h σ target h₁ σ₁ (.normal (.vRef addr)) → + EvalLaurelStmt δ π h₁ σ₁ value h₂ σ₂ (.normal v) → + HeapFieldWrite h₂ addr fieldName v h₃ → + EvalLaurelStmt δ π h σ + ⟨.Assign [⟨.FieldSelect target fieldName, tmd⟩] value, md⟩ h₃ σ₂ (.normal .vVoid) + +inductive EvalLaurelBlock : + LaurelEval → ProcEnv → LaurelHeap → LaurelStore → + List StmtExprMd → LaurelHeap → LaurelStore → Outcome → Prop where + + | nil : + EvalLaurelBlock δ π h σ [] h σ (.normal .vVoid) + + | cons_normal : + EvalLaurelStmt δ π h σ s h₁ σ₁ (.normal v) → + EvalLaurelBlock δ π h₁ σ₁ rest h₂ σ₂ outcome → + EvalLaurelBlock δ π h σ (s :: rest) h₂ σ₂ outcome + + | last_normal : + EvalLaurelStmt δ π h σ s h' σ' (.normal v) → + EvalLaurelBlock δ π h σ [s] h' σ' (.normal v) + + | cons_exit : + EvalLaurelStmt δ π h σ s h' σ' (.exit label) → + EvalLaurelBlock δ π h σ (s :: _rest) h' σ' (.exit label) + + | cons_return : + EvalLaurelStmt δ π h σ s h' σ' (.ret rv) → + EvalLaurelBlock δ π h σ (s :: _rest) h' σ' (.ret rv) + +end + +end Strata.Laurel diff --git a/Strata/Languages/Laurel/LaurelSemanticsProps.lean b/Strata/Languages/Laurel/LaurelSemanticsProps.lean new file mode 100644 index 000000000..55d7579cc --- /dev/null +++ b/Strata/Languages/Laurel/LaurelSemanticsProps.lean @@ -0,0 +1,131 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Languages.Laurel.LaurelSemantics + +/-! +# Properties of Laurel Operational Semantics + +Determinism, store monotonicity, and progress properties for the +direct Laurel operational semantics. +-/ + +namespace Strata.Laurel + +/-! ## Store Monotonicity -/ + +theorem UpdateStore_def_monotone {σ σ' : LaurelStore} {x : Identifier} {v : LaurelValue} + {vs : List Identifier} : + (∀ y, y ∈ vs → (σ y).isSome) → + UpdateStore σ x v σ' → + (∀ y, y ∈ vs → (σ' y).isSome) := by + intro Hdef Hup y Hy + cases Hup with + | update Hold Hnew Hrest => + by_cases heq : x = y + · subst heq; simp [Hnew] + · rw [Hrest y heq]; exact Hdef y Hy + +theorem InitStore_def_monotone {σ σ' : LaurelStore} {x : Identifier} {v : LaurelValue} + {vs : List Identifier} : + (∀ y, y ∈ vs → (σ y).isSome) → + InitStore σ x v σ' → + (∀ y, y ∈ vs → (σ' y).isSome) := by + intro Hdef Hinit y Hy + cases Hinit with + | init Hnone Hnew Hrest => + by_cases heq : x = y + · subst heq; simp [Hnew] + · rw [Hrest y heq]; exact Hdef y Hy + +/-! ## Determinism of Store Operations -/ + +theorem UpdateStore_deterministic {σ σ₁ σ₂ : LaurelStore} {x : Identifier} {v : LaurelValue} : + UpdateStore σ x v σ₁ → + UpdateStore σ x v σ₂ → + σ₁ = σ₂ := by + intro H1 H2 + cases H1 with | update _ Hnew1 Hrest1 => + cases H2 with | update _ Hnew2 Hrest2 => + funext y + by_cases heq : x = y + · subst heq; simp_all + · rw [Hrest1 y heq, Hrest2 y heq] + +theorem InitStore_deterministic {σ σ₁ σ₂ : LaurelStore} {x : Identifier} {v : LaurelValue} : + InitStore σ x v σ₁ → + InitStore σ x v σ₂ → + σ₁ = σ₂ := by + intro H1 H2 + cases H1 with | init _ Hnew1 Hrest1 => + cases H2 with | init _ Hnew2 Hrest2 => + funext y + by_cases heq : x = y + · subst heq; simp_all + · rw [Hrest1 y heq, Hrest2 y heq] + +/-! ## catchExit Properties -/ + +theorem catchExit_normal (label : Option Identifier) (v : LaurelValue) : + catchExit label (.normal v) = .normal v := by + cases label <;> simp [catchExit] + +theorem catchExit_return (label : Option Identifier) (rv : Option LaurelValue) : + catchExit label (.ret rv) = .ret rv := by + cases label <;> simp [catchExit] + +theorem catchExit_none_passthrough (o : Outcome) : + catchExit none o = o := by + simp [catchExit] + +/-! ## evalPrimOp Determinism -/ + +theorem evalPrimOp_deterministic (op : Operation) (args : List LaurelValue) : + ∀ v₁ v₂, evalPrimOp op args = some v₁ → evalPrimOp op args = some v₂ → v₁ = v₂ := by + intros v₁ v₂ H1 H2; rw [H1] at H2; exact Option.some.inj H2 + +/-! ## Determinism of Evaluation -/ + +/- +Theorem: Laurel evaluation is deterministic. + +For the full relation, if a statement evaluates to two results under the +same evaluator, procedure environment, heap, and store, those results are equal. + +Proof sketch: By mutual induction on the evaluation derivation. +Each constructor uniquely determines the outcome given the same inputs. + +Note: Full proof requires mutual induction over EvalLaurelStmt and +EvalLaurelBlock simultaneously. The proof is admitted here; the store +operation determinism lemmas above are the key building blocks. +-/ + +mutual +theorem EvalLaurelStmt_deterministic : + EvalLaurelStmt δ π h σ s h₁ σ₁ o₁ → + EvalLaurelStmt δ π h σ s h₂ σ₂ o₂ → + h₁ = h₂ ∧ σ₁ = σ₂ ∧ o₁ = o₂ := by + sorry + +theorem EvalLaurelBlock_deterministic : + EvalLaurelBlock δ π h σ ss h₁ σ₁ o₁ → + EvalLaurelBlock δ π h σ ss h₂ σ₂ o₂ → + h₁ = h₂ ∧ σ₁ = σ₂ ∧ o₁ = o₂ := by + sorry +end + +/-! ## Block Value Semantics -/ + +theorem empty_block_void : + EvalLaurelBlock δ π h σ [] h σ (.normal .vVoid) := + EvalLaurelBlock.nil + +theorem singleton_block_value : + EvalLaurelStmt δ π h σ s h' σ' (.normal v) → + EvalLaurelBlock δ π h σ [s] h' σ' (.normal v) := + EvalLaurelBlock.last_normal + +end Strata.Laurel diff --git a/StrataTest/Languages/Laurel/LaurelSemanticsTest.lean b/StrataTest/Languages/Laurel/LaurelSemanticsTest.lean new file mode 100644 index 000000000..e52608300 --- /dev/null +++ b/StrataTest/Languages/Laurel/LaurelSemanticsTest.lean @@ -0,0 +1,260 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Languages.Laurel.LaurelSemantics +import Strata.Languages.Laurel.LaurelSemanticsProps + +/-! +# Tests for Laurel Operational Semantics + +Concrete evaluation tests using `example` proofs to demonstrate that the +semantic rules produce expected results for each major construct. +-/ + +namespace Strata.Laurel.Test + +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 + | .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 then some v else none + +/-! ## Literal Tests -/ + +example : EvalLaurelStmt trivialEval emptyProc emptyHeap emptyStore + (mk (.LiteralInt 42)) emptyHeap emptyStore (.normal (.vInt 42)) := + .literal_int + +example : EvalLaurelStmt trivialEval emptyProc emptyHeap emptyStore + (mk (.LiteralBool true)) emptyHeap emptyStore (.normal (.vBool true)) := + .literal_bool + +example : EvalLaurelStmt trivialEval emptyProc emptyHeap emptyStore + (mk (.LiteralString "hello")) emptyHeap emptyStore (.normal (.vString "hello")) := + .literal_string + +/-! ## Identifier Test -/ + +example : EvalLaurelStmt trivialEval emptyProc emptyHeap (singleStore "x" (.vInt 7)) + (mk (.Identifier "x")) emptyHeap (singleStore "x" (.vInt 7)) (.normal (.vInt 7)) := + .identifier (by simp [singleStore]) + +/-! ## PrimitiveOp Tests -/ + +-- 2 + 3 = 5 +example : EvalLaurelStmt trivialEval emptyProc emptyHeap emptyStore + (mk (.PrimitiveOp .Add [mk (.LiteralInt 2), mk (.LiteralInt 3)])) + emptyHeap emptyStore (.normal (.vInt 5)) := + .prim_op (.cons (by rfl) (.cons (by rfl) .nil)) (by rfl) + +-- true && false = false +example : EvalLaurelStmt trivialEval emptyProc emptyHeap emptyStore + (mk (.PrimitiveOp .And [mk (.LiteralBool true), mk (.LiteralBool false)])) + emptyHeap emptyStore (.normal (.vBool false)) := + .prim_op (.cons (by rfl) (.cons (by rfl) .nil)) (by rfl) + +-- !true = false +example : EvalLaurelStmt trivialEval emptyProc emptyHeap emptyStore + (mk (.PrimitiveOp .Not [mk (.LiteralBool true)])) + emptyHeap emptyStore (.normal (.vBool false)) := + .prim_op (.cons (by rfl) .nil) (by rfl) + +-- 5 < 10 = true +example : EvalLaurelStmt trivialEval emptyProc emptyHeap emptyStore + (mk (.PrimitiveOp .Lt [mk (.LiteralInt 5), mk (.LiteralInt 10)])) + emptyHeap emptyStore (.normal (.vBool true)) := + .prim_op (.cons (by rfl) (.cons (by rfl) .nil)) (by rfl) + +-- "a" ++ "b" = "ab" +example : EvalLaurelStmt trivialEval emptyProc emptyHeap emptyStore + (mk (.PrimitiveOp .StrConcat [mk (.LiteralString "a"), mk (.LiteralString "b")])) + emptyHeap emptyStore (.normal (.vString "ab")) := + .prim_op (.cons (by rfl) (.cons (by rfl) .nil)) (by rfl) + +/-! ## Block Tests -/ + +-- Empty block evaluates to void +example : EvalLaurelStmt trivialEval emptyProc emptyHeap emptyStore + (mk (.Block [] none)) emptyHeap emptyStore (.normal .vVoid) := + .block_sem .nil (by rfl) + +-- Singleton block returns its value +example : EvalLaurelStmt trivialEval emptyProc emptyHeap emptyStore + (mk (.Block [mk (.LiteralInt 99)] none)) emptyHeap emptyStore (.normal (.vInt 99)) := + .block_sem (.last_normal .literal_int) (by rfl) + +-- Block with two statements: value is the last one +example : EvalLaurelStmt trivialEval emptyProc emptyHeap emptyStore + (mk (.Block [mk (.LiteralInt 1), mk (.LiteralInt 2)] none)) + emptyHeap emptyStore (.normal (.vInt 2)) := + .block_sem (.cons_normal .literal_int (.last_normal .literal_int)) (by rfl) + +/-! ## IfThenElse Tests -/ + +-- if true then 1 else 2 => 1 +example : EvalLaurelStmt trivialEval emptyProc emptyHeap emptyStore + (mk (.IfThenElse (mk (.LiteralBool true)) (mk (.LiteralInt 1)) (some (mk (.LiteralInt 2))))) + emptyHeap emptyStore (.normal (.vInt 1)) := + .ite_true .literal_bool .literal_int + +-- if false then 1 else 2 => 2 +example : EvalLaurelStmt trivialEval emptyProc emptyHeap emptyStore + (mk (.IfThenElse (mk (.LiteralBool false)) (mk (.LiteralInt 1)) (some (mk (.LiteralInt 2))))) + emptyHeap emptyStore (.normal (.vInt 2)) := + .ite_false .literal_bool .literal_int + +-- if false then 1 => void (no else branch) +example : EvalLaurelStmt trivialEval emptyProc emptyHeap emptyStore + (mk (.IfThenElse (mk (.LiteralBool false)) (mk (.LiteralInt 1)) none)) + emptyHeap emptyStore (.normal .vVoid) := + .ite_false_no_else .literal_bool + +/-! ## Exit Tests -/ + +-- Exit propagates through block +example : EvalLaurelStmt trivialEval emptyProc emptyHeap emptyStore + (mk (.Block [mk (.Exit "L"), mk (.LiteralInt 99)] none)) + emptyHeap emptyStore (.exit "L") := + .block_sem (.cons_exit .exit_sem) (by rfl) + +-- Labeled block catches matching exit +example : EvalLaurelStmt trivialEval emptyProc emptyHeap emptyStore + (mk (.Block [mk (.Exit "L")] (some "L"))) + emptyHeap emptyStore (.normal .vVoid) := + .block_sem (.cons_exit .exit_sem) (by rfl) + +-- Labeled block does NOT catch non-matching exit +example : EvalLaurelStmt trivialEval emptyProc emptyHeap emptyStore + (mk (.Block [mk (.Exit "other")] (some "L"))) + emptyHeap emptyStore (.exit "other") := + .block_sem (.cons_exit .exit_sem) (by decide) + +/-! ## Return Tests -/ + +-- Return with value +example : EvalLaurelStmt trivialEval emptyProc emptyHeap emptyStore + (mk (.Return (some (mk (.LiteralInt 42))))) + emptyHeap emptyStore (.ret (some (.vInt 42))) := + .return_some .literal_int + +-- Return without value +example : EvalLaurelStmt trivialEval emptyProc emptyHeap emptyStore + (mk (.Return none)) + emptyHeap emptyStore (.ret none) := + .return_none + +-- Return short-circuits block +example : EvalLaurelStmt trivialEval emptyProc emptyHeap emptyStore + (mk (.Block [mk (.Return (some (mk (.LiteralInt 1)))), mk (.LiteralInt 99)] none)) + emptyHeap emptyStore (.ret (some (.vInt 1))) := + .block_sem (.cons_return (.return_some .literal_int)) (by rfl) + +/-! ## LocalVariable Tests -/ + +-- Declare and initialize a local variable +example : let σ' := singleStore "x" (.vInt 10) + EvalLaurelStmt trivialEval emptyProc emptyHeap emptyStore + (mk (.LocalVariable "x" ⟨.TInt, emd⟩ (some (mk (.LiteralInt 10))))) + emptyHeap σ' (.normal .vVoid) := + .local_var_init .literal_int (by simp [emptyStore]) + (.init (by simp [emptyStore]) + (by simp [singleStore]) + (by intro y hne; simp [singleStore, emptyStore]; intro h; exact absurd h.symm hne)) + +-- Declare without initializer +example : let σ' := singleStore "y" .vVoid + EvalLaurelStmt trivialEval emptyProc emptyHeap emptyStore + (mk (.LocalVariable "y" ⟨.TBool, emd⟩ none)) + emptyHeap σ' (.normal .vVoid) := + .local_var_uninit (by simp [emptyStore]) + (.init (by simp [emptyStore]) + (by simp [singleStore]) + (by intro y hne; simp [singleStore, emptyStore]; intro h; exact absurd h.symm hne)) + +/-! ## Assert/Assume Tests -/ + +-- Assert true succeeds +example : EvalLaurelStmt trivialEval emptyProc emptyHeap emptyStore + (mk (.Assert (mk (.LiteralBool true)))) + emptyHeap emptyStore (.normal .vVoid) := + .assert_true .literal_bool + +-- Assume true succeeds +example : EvalLaurelStmt trivialEval emptyProc emptyHeap emptyStore + (mk (.Assume (mk (.LiteralBool true)))) + emptyHeap emptyStore (.normal .vVoid) := + .assume_true .literal_bool + +/-! ## ProveBy Test -/ + +-- ProveBy evaluates to the value of its first argument +example : EvalLaurelStmt trivialEval emptyProc emptyHeap emptyStore + (mk (.ProveBy (mk (.LiteralInt 5)) (mk (.LiteralBool true)))) + emptyHeap emptyStore (.normal (.vInt 5)) := + .prove_by .literal_int + +/-! ## Nested Control Flow Tests -/ + +-- Nested blocks with exit: inner exit propagates to outer labeled block +example : EvalLaurelStmt trivialEval emptyProc emptyHeap emptyStore + (mk (.Block [ + mk (.Block [mk (.Exit "outer"), mk (.LiteralInt 99)] none), + mk (.LiteralInt 88) + ] (some "outer"))) + emptyHeap emptyStore (.normal .vVoid) := + .block_sem + (.cons_exit (.block_sem (.cons_exit .exit_sem) (by rfl))) + (by rfl) + +/-! ## Property Tests -/ + +-- catchExit preserves normal outcomes +example : catchExit (some "L") (.normal (.vInt 1)) = .normal (.vInt 1) := by rfl + +-- catchExit preserves return outcomes +example : catchExit (some "L") (.ret (some (.vInt 1))) = .ret (some (.vInt 1)) := by rfl + +-- catchExit catches matching exit +example : catchExit (some "L") (.exit "L") = .normal .vVoid := by rfl + +-- catchExit passes through non-matching exit +example : catchExit (some "L") (.exit "M") = .exit "M" := by decide + +-- evalPrimOp: integer addition +example : evalPrimOp .Add [.vInt 3, .vInt 4] = some (.vInt 7) := by rfl + +-- evalPrimOp: boolean negation +example : evalPrimOp .Not [.vBool false] = some (.vBool true) := by rfl + +-- evalPrimOp: division by zero returns none +example : evalPrimOp .Div [.vInt 5, .vInt 0] = none := by rfl + +-- evalPrimOp: type mismatch returns none +example : evalPrimOp .Add [.vBool true, .vInt 1] = none := by rfl + +-- Empty block is void +example : EvalLaurelBlock trivialEval emptyProc emptyHeap emptyStore + [] emptyHeap emptyStore (.normal .vVoid) := + .nil + +end Strata.Laurel.Test diff --git a/docs/designs/design-formal-semantics-for-laurel-ir.md b/docs/designs/design-formal-semantics-for-laurel-ir.md new file mode 100644 index 000000000..9097baeed --- /dev/null +++ b/docs/designs/design-formal-semantics-for-laurel-ir.md @@ -0,0 +1,526 @@ +# Design: Formal Semantics for Laurel IR + +**Date:** 2026-03-03 +**Status:** Proposal + +## 1. Problem Statement + +Laurel is Strata's common intermediate representation for front-end languages like Java, Python, and JavaScript. It is translated to Strata Core for verification. However, Laurel currently lacks its own formal operational semantics — its meaning is defined only implicitly through the translation in `LaurelToCoreTranslator.lean` and the partial interpreter in `LaurelEval.lean`. + +This creates several problems: + +1. **No independent specification.** If the translator has a bug, there is no reference semantics to detect it. The translator *is* the semantics, so any behavior it produces is "correct" by definition. + +2. **No formal properties.** We cannot state or prove determinism, progress, or type preservation for Laurel programs directly. + +3. **No translation correctness.** Without Laurel semantics, we cannot prove that `LaurelToCoreTranslator` preserves program meaning — the central correctness property for the entire verification pipeline. + +4. **Laurel-specific constructs have no formal account.** Constructs like labeled `Block`/`Exit` (modeling break/continue), `StmtExpr` unification (expressions that are also statements), `Return`, type operations (`IsType`, `AsType`), and object-oriented features (`InstanceCall`, `FieldSelect`, `New`) need precise semantic definitions. + +### Concrete example: labeled Exit + +``` +// Laurel source (pseudocode) +var x: int := 0; +outer: { + inner: { + x := 1; + exit outer; // break out of outer block + x := 2; // dead code + } + x := 3; // also dead code +} +assert x == 1; +``` + +The translator converts `exit outer` into Core's `goto` mechanism, but there is no formal proof that this translation preserves the intended semantics. A direct Laurel semantics would define `Exit` as non-local control flow that unwinds to the matching labeled `Block`, and we could then prove the translation correct. + +### Concrete example: expression-statement duality + +``` +// Laurel: if-then-else as expression returning a value +var y: int := if (x > 0) { x } else { 0 - x }; +``` + +Laurel's `StmtExpr` type unifies statements and expressions. The "last expression as block value" convention means blocks can produce values. This needs a formal account — Core has no such concept (it separates expressions from statements). + +## 2. Background + +### 2.1 Core Semantics (existing) + +Core's formal semantics is defined in three layers: + +**Generic framework** (`Strata/DL/Imperative/StmtSemantics.lean`): +- `SemanticStore P` — variable store: `P.Ident → Option P.Expr` +- `SemanticEval P` — expression evaluator: `Store → Expr → Option Expr` +- `EvalCmd` — inductive relation for atomic commands (init, set, havoc, assert, assume) +- `EvalStmt` / `EvalBlock` — mutually inductive relations for statements and statement lists +- Judgment form: `δ, σ, stmt ⊢ σ', δ'` (evaluator and store are threaded) + +**Core instantiation** (`Strata/Languages/Core/StatementSemantics.lean`): +- `Value` predicate for irreducible Core expressions +- `WellFormedCoreEvalDefinedness`, `WellFormedCoreEvalCong` — well-formedness conditions +- `EvalCommand` — extends `EvalCmd` with procedure calls (`call_sem`) +- `EvalStatement` / `EvalStatements` — type aliases for the instantiated generic framework +- `EvalCommandContract` — contract-based call semantics (havoc + assume postconditions) + +**Properties** (`Strata/Languages/Core/StatementSemanticsProps.lean`): +- Store monotonicity theorems (`InitStateDefMonotone`, `UpdateStateDefMonotone`, etc.) +- Injective store operations (`InitStateInjective`, `ReadValuesInjective`) +- `EvalStmtRefinesContract` / `EvalBlockRefinesContract` — body execution refines contract semantics +- Substitution and invariant store theorems + +Key design patterns: +- Stores are abstract functions, not concrete data structures +- `InitState` requires the variable was previously unmapped; `UpdateState` requires it was mapped +- The evaluator `δ` is threaded as state to support `funcDecl` extending it +- Commands don't modify `δ`; only `funcDecl` does + +### 2.2 Laurel AST (existing) + +Defined in `Strata/Languages/Laurel/Laurel.lean`: + +`StmtExpr` is a single mutual inductive covering both statements and expressions: +- **Control flow:** `IfThenElse`, `Block` (with optional label), `While` (with invariants/decreases), `Exit` (labeled break), `Return` +- **Expressions:** `LiteralInt`, `LiteralBool`, `LiteralString`, `Identifier`, `PrimitiveOp`, `StaticCall`, `FieldSelect`, `Forall`, `Exists` +- **Assignments:** `Assign`, `LocalVariable` +- **OO features:** `New`, `This`, `InstanceCall`, `AsType`, `IsType`, `ReferenceEquals`, `PureFieldUpdate` +- **Verification:** `Assert`, `Assume`, `Old`, `Fresh`, `Assigned`, `ProveBy`, `ContractOf` + +All nodes are wrapped in `WithMetadata` carrying source locations. + +`Procedure` has inputs, outputs, preconditions, determinism, optional decreases, and a `Body` (Transparent/Opaque/Abstract). + +### 2.3 Translation pipeline (existing) + +`LaurelToCoreTranslator.lean` implements: +1. `heapParameterization` — makes heap explicit as a parameter +2. `typeHierarchyTransform` — encodes type hierarchy +3. `modifiesClausesTransform` — infers modifies clauses +4. `liftImperativeExpressions` — lifts assignments out of expression positions +5. `translateExpr` — Laurel expressions → Core expressions +6. `translateStmt` — Laurel statements → Core statements +7. `translateProcedure` — Laurel procedures → Core procedures + +### 2.4 Existing Laurel evaluator + +`LaurelEval.lean` defines a `partial def eval` interpreter in `HighLevel` namespace. It uses a different AST (`HighLevel.StmtExpr`) with constructs like `StaticInvocation`, `Closure`, `DynamicFieldAccess` that differ from the main `Laurel.StmtExpr`. This evaluator: +- Is `partial` (no termination proof) +- Uses a monadic `Eval` type with `EvalResult` (Success/Return/Exitting/TypeError/VerficationError) +- Has many `panic!` stubs for unimplemented features +- Operates on a different type hierarchy than the main Laurel AST + +This evaluator cannot serve as a formal semantics because it is partial, uses a different AST, and lacks any formal properties. + +## 3. Design Options + +### Option A: Direct Operational Semantics + +Define `EvalLaurelStmt` as a standalone inductive relation on `Laurel.StmtExpr`, independent of Core semantics. + +#### a. Implementation strategy + +Create new files in `Strata/Languages/Laurel/`: + +| File | Purpose | +|------|---------| +| `LaurelSemantics.lean` | Core semantic definitions: store, evaluator, `EvalLaurelStmt`/`EvalLaurelBlock` | +| `LaurelSemanticsProps.lean` | Determinism, progress, store monotonicity theorems | +| `LaurelTranslationCorrect.lean` | Bisimulation between Laurel and Core semantics | + +The semantic judgment has the form: + +```lean +-- Laurel semantic store maps identifiers to Laurel values +abbrev LaurelStore := Laurel.Identifier → Option LaurelValue + +-- Laurel values (distinct from Core values) +inductive LaurelValue where + | vInt : Int → LaurelValue + | vBool : Bool → LaurelValue + | vString : String → LaurelValue + | vVoid : LaurelValue + | vRef : Nat → LaurelValue -- heap reference + +-- Outcome captures non-local control flow +inductive Outcome where + | normal : LaurelValue → Outcome -- normal completion with value + | exit : Identifier → Outcome -- exit to labeled block + | ret : Option LaurelValue → Outcome -- return from procedure + +-- Expression evaluator +abbrev LaurelEval := LaurelStore → StmtExpr → Option LaurelValue + +-- Main judgment: store, expression/statement ⊢ store', outcome +mutual +inductive EvalLaurelStmt : + LaurelEval → LaurelStore → StmtExprMd → LaurelStore → Outcome → Prop where + | literal_int : + EvalLaurelStmt δ σ ⟨.LiteralInt i, md⟩ σ (.normal (.vInt i)) + | literal_bool : + EvalLaurelStmt δ σ ⟨.LiteralBool b, md⟩ σ (.normal (.vBool b)) + | ite_true : + EvalLaurelStmt δ σ cond σ₁ (.normal (.vBool true)) → + EvalLaurelStmt δ σ₁ thenBr σ₂ outcome → + EvalLaurelStmt δ σ ⟨.IfThenElse cond thenBr (some elseBr), md⟩ σ₂ outcome + | block_sem : + EvalLaurelBlock δ σ stmts σ' outcome → + -- If outcome is exit targeting this label, catch it + catchExit label outcome = outcome' → + EvalLaurelStmt δ σ ⟨.Block stmts label, md⟩ σ' outcome' + | exit_sem : + EvalLaurelStmt δ σ ⟨.Exit target, md⟩ σ (.exit target) + | while_true : + EvalLaurelStmt δ σ cond σ₁ (.normal (.vBool true)) → + EvalLaurelStmt δ σ₁ body σ₂ (.normal _) → + EvalLaurelStmt δ σ₂ ⟨.While cond invs dec body, md⟩ σ₃ outcome → + EvalLaurelStmt δ σ ⟨.While cond invs dec body, md⟩ σ₃ outcome + -- ... more constructors +inductive EvalLaurelBlock : + LaurelEval → LaurelStore → List StmtExprMd → LaurelStore → Outcome → Prop where + | nil : EvalLaurelBlock δ σ [] σ (.normal .vVoid) + | cons_normal : + EvalLaurelStmt δ σ s σ' (.normal v) → + EvalLaurelBlock δ σ' rest σ'' outcome → + EvalLaurelBlock δ σ (s :: rest) σ'' outcome + | cons_exit : + EvalLaurelStmt δ σ s σ' (.exit label) → + EvalLaurelBlock δ σ (s :: rest) σ' (.exit label) + | cons_return : + EvalLaurelStmt δ σ s σ' (.ret v) → + EvalLaurelBlock δ σ (s :: rest) σ' (.ret v) +end +``` + +Key design decisions: +- `Outcome` type handles non-local control flow (Exit, Return) explicitly, rather than using Core's goto mechanism +- `EvalLaurelBlock` propagates Exit/Return outcomes, skipping remaining statements +- Labeled `Block` catches matching `Exit` outcomes via `catchExit` +- The "last expression as block value" convention: the final `Outcome.normal v` in a block becomes the block's value + +#### b. Internal representation + +**Laurel values** are a separate type from Core expressions. This is necessary because: +- Laurel has heap references (`vRef`) that Core encodes differently (via map operations) +- Laurel's type system (nominal types, interfaces) requires runtime type tags +- The value domain must support `IsType`/`AsType` operations + +**Store** is `Identifier → Option LaurelValue` (string-keyed, matching Laurel's `abbrev Identifier := String`). + +**Heap** is modeled as a separate component `Nat → Option (Identifier × (Identifier → Option LaurelValue))` mapping references to (type-tag, field-store) pairs. This supports `New`, `FieldSelect`, and `ReferenceEquals`. + +**Expression evaluation** is a parameter `δ : LaurelEval` following Core's pattern, allowing different instantiations for different analysis modes. + +#### c. End-to-end correctness + +Translation correctness is stated as a simulation relation: + +```lean +-- Value correspondence +def valueCorr : LaurelValue → Core.Expression.Expr → Prop := ... + +-- Store correspondence (after heap parameterization) +def storeCorr : LaurelStore → LaurelHeap → CoreStore → Prop := ... + +-- Main theorem: if Laurel evaluates, the translated Core program +-- evaluates to a corresponding result +theorem translate_correct : + EvalLaurelStmt δL σL stmt σL' outcome → + storeCorr σL heap σC → + let (_, coreStmts) := translateStmt env outputs ⟨stmt, md⟩ |>.run initState + ∃ σC' δC', + EvalStatements π φ δC σC coreStmts σC' δC' ∧ + storeCorr σL' heap' σC' +``` + +The proof must account for the translation pipeline stages: +1. `heapParameterization` — relate Laurel heap to explicit heap parameter +2. `liftImperativeExpressions` — show lifting preserves semantics +3. `translateStmt` — show statement translation preserves semantics + +Each stage needs its own correctness lemma, composed for the full pipeline. + +#### d. Testing strategy + +| Test type | Location | Purpose | +|-----------|----------|---------| +| Concrete evaluation | `StrataTest/Languages/Laurel/LaurelSemanticsTest.lean` | `#guard_msgs` tests showing specific evaluations | +| Determinism examples | Same file | Show unique outcomes for concrete programs | +| Exit/Return propagation | Same file | Test non-local control flow | +| Translation correspondence | `StrataTest/Languages/Laurel/TranslationCorrectTest.lean` | Concrete examples where both semantics agree | + +Limitations: +- `While` semantics is coinductive in nature; the inductive relation only captures terminating executions +- OO features (heap, dynamic dispatch) significantly increase complexity +- Full translation correctness proof requires reasoning about 5+ pipeline stages + +#### e. Complexity and risk + +**Files changed:** 3 new files, 0 modified +**Estimated LOC:** ~800 (semantics) + ~500 (properties) + ~1500+ (translation correctness) +**Risk:** +- High: Laurel's `StmtExpr` has ~35 constructors; defining semantics for all is substantial +- High: Translation correctness proof must reason about heap parameterization, expression lifting, and statement translation simultaneously +- Medium: `Outcome` type adds complexity to every induction over the semantics +- The Laurel value domain and Core expression domain are very different, making `valueCorr` non-trivial + +--- + +### Option B: Shallow Embedding via Translation + +Define Laurel's semantics as "the semantics of the translated Core program." No new inductive relation — Laurel's meaning is Core's meaning after translation. + +#### a. Implementation strategy + +Create minimal new files: + +| File | Purpose | +|------|---------| +| `LaurelSemanticsViaCore.lean` | Definitions composing translation with Core semantics | +| `LaurelTranslationProps.lean` | Properties of the translation (well-typedness preservation, etc.) | + +The "semantics" is a definition, not an inductive: + +```lean +-- Laurel program evaluates iff its Core translation evaluates +def LaurelEvaluatesTo (program : Laurel.Program) (σ σ' : CoreStore) (δ δ' : CoreEval) : Prop := + match translate program with + | .ok (coreProgram, _) => + ∃ π φ, EvalStatements π φ δ σ coreProgram.body σ' δ' + | .error _ => False + +-- Per-procedure semantics +def LaurelProcEvaluatesTo (proc : Laurel.Procedure) (σ σ' : CoreStore) : Prop := + let (coreProc, _) := runTranslateM initState (translateProcedure proc) + ∃ δ δ' π φ, EvalStatements π φ δ σ coreProc.body σ' δ' +``` + +#### b. Internal representation + +No new value types or store types. Everything uses Core's representation: +- Values are `Core.Expression.Expr` satisfying `Core.Value` +- Store is `CoreStore` = `Core.Expression.Ident → Option Core.Expression.Expr` +- Evaluation uses `EvalStatement` / `EvalStatements` from Core + +Laurel identifiers are mapped to Core identifiers via `⟨name, ()⟩`. + +#### c. End-to-end correctness + +Translation correctness is trivial by construction — Laurel's semantics *is* Core's semantics after translation. There is nothing to prove. + +However, we can still prove useful properties: + +```lean +-- The translation produces well-typed Core programs +theorem translate_well_typed : + laurelTypeChecks program → + coreTypeChecks (translate program) + +-- The translation preserves procedure structure +theorem translate_preserves_procedures : + program.staticProcedures.length = (translate program).procedures.length + +-- Specific construct correctness (e.g., Exit → goto) +theorem exit_translates_correctly : + -- Exit to label L in Laurel becomes goto L in Core + ... +``` + +Properties like determinism and progress are inherited from Core automatically — if Core's semantics is deterministic, and the translation is a function, then Laurel's derived semantics is deterministic. + +#### d. Testing strategy + +| Test type | Location | Purpose | +|-----------|----------|---------| +| Translation output | `StrataTest/Languages/Laurel/TranslationTest.lean` | `#guard_msgs` showing translated Core for each Laurel construct | +| Round-trip verification | Existing `Examples/` | Verify Laurel programs produce expected SMT results | +| Regression tests | Same | Ensure translation changes don't break verification | + +Limitations: +- Cannot reason about Laurel programs independently of Core +- Cannot state properties about Laurel constructs that are erased by translation (e.g., type assertions in an erasure model) +- If the translation has a bug, the "semantics" has the same bug — no independent check +- Cannot compare alternative translations (e.g., optimized vs. reference) + +#### e. Complexity and risk + +**Files changed:** 2 new files, 0 modified +**Estimated LOC:** ~200 (definitions) + ~300 (properties) +**Risk:** +- Low implementation risk — very little new code +- High conceptual risk — this doesn't actually define Laurel semantics, it just names the composition of translation + Core semantics +- Medium: Properties we can prove are limited to translation structure, not semantic content +- The approach provides no defense against translator bugs + +--- + +### Option C: Hybrid — Direct Semantics for Core Constructs, Desugaring for High-Level Constructs + +Define direct operational semantics for the "imperative core" of Laurel (assignments, control flow, expressions), and define high-level constructs (OO features, type operations) via desugaring to this core. + +#### a. Implementation strategy + +Create files in two phases: + +**Phase 1 — Imperative core semantics:** + +| File | Purpose | +|------|---------| +| `LaurelSemantics.lean` | `EvalLaurelStmt`/`EvalLaurelBlock` for imperative subset | +| `LaurelSemanticsProps.lean` | Determinism, progress, monotonicity for imperative subset | + +**Phase 2 — High-level construct desugaring + translation correctness:** + +| File | Purpose | +|------|---------| +| `LaurelDesugar.lean` | Laurel-to-Laurel desugaring (OO → imperative core) | +| `LaurelDesugarCorrect.lean` | Desugaring preserves semantics | +| `LaurelTranslationCorrect.lean` | Imperative core → Core translation correctness | + +The imperative core covers these `StmtExpr` constructors: +- `LiteralInt`, `LiteralBool`, `LiteralString`, `Identifier` — values/variables +- `PrimitiveOp` — arithmetic and boolean operations +- `Assign`, `LocalVariable` — variable mutation +- `IfThenElse`, `While`, `Block`, `Exit`, `Return` — control flow +- `Assert`, `Assume` — verification constructs +- `StaticCall` — procedure calls (without OO dispatch) +- `Forall`, `Exists` — quantifiers (in specification contexts) + +High-level constructs handled by desugaring: +- `New`, `FieldSelect`, `PureFieldUpdate`, `InstanceCall`, `This` → desugared using heap parameterization (already exists as `heapParameterization`) +- `IsType`, `AsType` → desugared using type hierarchy encoding (already exists as `typeHierarchyTransform`) +- `ReferenceEquals` → desugared to equality on references +- `Old`, `Fresh`, `Assigned` → desugared to two-state predicates + +This aligns with the existing translation pipeline, which already performs these transformations before `translateStmt`. + +#### b. Internal representation + +**Values** for the imperative core: + +```lean +inductive LaurelValue where + | vInt : Int → LaurelValue + | vBool : Bool → LaurelValue + | vString : String → LaurelValue + | vFloat64 : Float → LaurelValue + | vVoid : LaurelValue +``` + +No heap references in the core — those are introduced by desugaring (heap parameterization makes the heap an explicit map variable). + +**Store** is `Identifier → Option LaurelValue`. + +**Outcome** type for non-local control flow (same as Option A): + +```lean +inductive Outcome where + | normal : LaurelValue → Outcome + | exit : Identifier → Outcome + | ret : Option LaurelValue → Outcome +``` + +**Semantic judgment:** + +```lean +mutual +inductive EvalLaurelStmt : + LaurelEval → LaurelStore → StmtExprMd → LaurelStore → Outcome → Prop +inductive EvalLaurelBlock : + LaurelEval → LaurelStore → List StmtExprMd → LaurelStore → Outcome → Prop +end +``` + +The key difference from Option A: the inductive only has constructors for the imperative core (~18 constructors instead of ~35). OO and type-level constructs are excluded — they must be desugared first. + +#### c. End-to-end correctness + +The correctness argument is modular, matching the existing pipeline: + +``` +Laurel (full) + ──[heapParameterization]──→ Laurel (no heap/OO) -- LaurelDesugarCorrect.lean + ──[typeHierarchyTransform]──→ Laurel (no types) -- LaurelDesugarCorrect.lean + ──[liftImperativeExpressions]──→ Laurel (imp. core) -- LaurelDesugarCorrect.lean + ──[translateStmt]──→ Core -- LaurelTranslationCorrect.lean +``` + +Each arrow has its own correctness theorem: + +```lean +-- Desugaring preserves semantics (Laurel → Laurel) +theorem heapParam_correct : + EvalLaurelStmt_full δ σ stmt σ' outcome → + ∃ σC σC', + storeCorr σ σC ∧ + EvalLaurelStmt δC σC (heapParam stmt) σC' outcomeC ∧ + storeCorr σ' σC' + +-- Core translation preserves semantics (Laurel imperative core → Core) +theorem translateStmt_correct : + EvalLaurelStmt δL σL stmt σL' (.normal v) → + storeCorr σL σC → + let coreStmts := (translateStmt env outputs ⟨stmt, md⟩ |>.run s).1.2 + ∃ σC' δC', + EvalStatements π φ δC σC coreStmts σC' δC' ∧ + storeCorr σL' σC' +``` + +The full pipeline correctness composes these lemmas. + +#### d. Testing strategy + +| Test type | Location | Purpose | +|-----------|----------|---------| +| Core semantics | `StrataTest/Languages/Laurel/LaurelSemanticsTest.lean` | Concrete evaluations of imperative core | +| Exit/Return | Same | Non-local control flow examples | +| Desugaring | `StrataTest/Languages/Laurel/LaurelDesugarTest.lean` | Show desugaring output for OO constructs | +| Translation | `StrataTest/Languages/Laurel/TranslationCorrectTest.lean` | End-to-end correspondence examples | +| Property tests | `StrataTest/Languages/Laurel/LaurelSemanticsPropsTest.lean` | Determinism, monotonicity on concrete examples | + +Limitations: +- Desugaring correctness proofs for heap parameterization are complex (the existing `heapParameterization` function is ~600 lines) +- The boundary between "imperative core" and "desugared" constructs is a design choice that may need revision +- `While` still only captures terminating executions + +#### e. Complexity and risk + +**Files changed:** 4-5 new files, 0 modified +**Estimated LOC:** ~500 (core semantics) + ~300 (properties) + ~400 (desugaring correctness) + ~600 (translation correctness) +**Risk:** +- Medium: Imperative core is well-scoped (~18 constructors), manageable +- Medium: Desugaring correctness for heap parameterization is the hardest part, but can be deferred +- Low: Core semantics and properties can be developed and tested independently +- The modular structure means each piece can be verified in isolation + +## 4. Recommendation + +**Option C (Hybrid)** is recommended. + +### Rationale + +1. **Matches the existing architecture.** The translation pipeline already performs Laurel→Laurel desugaring (heap parameterization, type hierarchy, expression lifting) before Laurel→Core translation. Option C formalizes this existing structure rather than fighting it. + +2. **Incremental development.** We can deliver value in phases: + - Phase 1: Imperative core semantics + determinism/progress proofs (~800 LOC). This is immediately useful for reasoning about control flow, assignments, and verification constructs. + - Phase 2: Translation correctness for the imperative core → Core (~600 LOC). This validates `translateStmt` for the most common constructs. + - Phase 3: Desugaring correctness for individual passes (can be done per-pass, in any order). + +3. **Right level of abstraction.** Option A tries to formalize everything at once (including OO features that are already desugared away before Core translation). Option B provides no independent semantics at all. Option C gives us a real semantics for the constructs that matter most (control flow, assignments, verification) while deferring the complexity of OO encoding. + +4. **Manageable proof obligations.** The imperative core has ~18 constructors (vs. ~35 for full StmtExpr). Determinism and progress proofs scale with constructor count. The `Outcome` type adds some complexity but is essential for modeling `Exit`/`Return` correctly. + +5. **Reuses existing infrastructure.** The `Outcome` type mirrors `EvalResult` from `LaurelEval.lean`. The store model follows Core's `SemanticStore` pattern. The modular correctness structure follows the existing `EvalStmtRefinesContract` pattern. + +### Suggested implementation order + +1. Define `LaurelValue`, `LaurelStore`, `Outcome` types +2. Define `EvalLaurelStmt` / `EvalLaurelBlock` for imperative core +3. Write concrete evaluation tests +4. Prove determinism for the imperative core +5. Prove store monotonicity +6. Define store correspondence `LaurelStore ↔ CoreStore` +7. Prove `translateStmt` correctness for simple constructs (Assign, LocalVariable, IfThenElse) +8. Extend to While, Block/Exit, Return +9. (Later) Prove desugaring correctness for heap parameterization +10. (Later) Prove desugaring correctness for expression lifting From c1f7393424d7eb99ed6e8c35fd4c9d2c81922427 Mon Sep 17 00:00:00 2001 From: Olivier Bouissou Date: Tue, 3 Mar 2026 18:17:48 -0500 Subject: [PATCH 2/2] fix(laurel): Address review feedback for Laurel direct operational semantics MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Bug fixes: - Fix EvalLaurelBlock non-determinism: add rest ≠ [] side condition to cons_normal so it cannot overlap with last_normal on singleton lists. last_normal handles [s] → value of s; cons_normal handles (s :: rest) where rest is non-empty. - Add static_call_return_void, instance_call_return, and instance_call_return_void rules for void-returning procedures (.ret none). Previously these caused evaluation to get stuck. - Fix bindParams to start from an empty store instead of the caller store, enforcing lexical scoping. Callees can no longer accidentally read caller locals. Documentation: - Document purity requirement for assert_true/assume_true conditions. - Document intentionally omitted constructors (Abstract, All, Hole). - Document known limitations (multi-target Assign, pure argument eval). - Update design document: replace Option C recommendation with Option A decision record reflecting the actual implementation choice. --- Strata/Languages/Laurel/LaurelSemantics.lean | 88 +++++++++++++++---- .../Languages/Laurel/LaurelSemanticsTest.lean | 2 +- .../design-formal-semantics-for-laurel-ir.md | 33 +------ 3 files changed, 77 insertions(+), 46 deletions(-) diff --git a/Strata/Languages/Laurel/LaurelSemantics.lean b/Strata/Languages/Laurel/LaurelSemantics.lean index 69e29a7b8..dc739186c 100644 --- a/Strata/Languages/Laurel/LaurelSemantics.lean +++ b/Strata/Languages/Laurel/LaurelSemantics.lean @@ -22,6 +22,22 @@ document `docs/designs/design-formal-semantics-for-laurel-ir.md`). - **EvalLaurelStmt / EvalLaurelBlock**: mutually inductive big-step relations The judgment form is: `δ, π, heap, σ, stmt ⊢ heap', σ', outcome` + +## Intentionally Omitted Constructs + +The following `StmtExpr` constructors have no evaluation rules and will get stuck: +- **`Abstract`**: Specification-level marker for abstract contracts. Not executable. +- **`All`**: Specification-level reference to all heap objects (reads/modifies clauses). +- **`Hole`**: Represents incomplete programs. Not executable by design. + +## Known Limitations + +- **Multi-target `Assign`**: Only single-target assignment (identifier or field) is + handled. Multi-target assignment (for procedures with multiple outputs) is not yet + supported. -- TODO: Add multi-target assign rules. +- **Argument evaluation**: Call arguments are evaluated via the pure evaluator `δ` + rather than `EvalLaurelStmt`, so arguments with side effects will get stuck. + This is a workaround for Lean 4 mutual inductive limitations. -/ namespace Strata.Laurel @@ -126,15 +142,18 @@ def getBody : Procedure → Option StmtExprMd | { body := .Opaque _ (some b) _, .. } => some b | _ => none -def bindParams (σ : LaurelStore) (params : List Parameter) (vals : List LaurelValue) +/-- Bind parameters to values starting from an empty store (lexical scoping). -/ +def bindParams (params : List Parameter) (vals : List LaurelValue) : Option LaurelStore := - match params, vals with - | [], [] => some σ - | p :: ps, v :: vs => - if σ p.name = none then - bindParams (fun x => if x == p.name then some v else σ x) ps vs - else none - | _, _ => none + go (fun _ => none) params vals +where + go (σ : LaurelStore) : List Parameter → List LaurelValue → Option LaurelStore + | [], [] => some σ + | p :: ps, v :: vs => + if σ p.name = none then + go (fun x => if x == p.name then some v else σ x) ps vs + else none + | _, _ => none def HighType.typeName : HighType → Identifier | .UserDefined name => name @@ -254,6 +273,10 @@ inductive EvalLaurelStmt : EvalLaurelStmt δ π h σ ⟨.LocalVariable name ty none, md⟩ h σ' (.normal .vVoid) -- Verification Constructs + -- Note: assert_true and assume_true require the condition to be pure + -- (no side effects on heap or store). Conditions with side effects have + -- no derivation. This is intentional — assert/assume conditions should + -- be specification-level expressions, not effectful computations. | assert_true : EvalLaurelStmt δ π h σ c h σ (.normal (.vBool true)) → @@ -264,11 +287,15 @@ inductive EvalLaurelStmt : EvalLaurelStmt δ π h σ ⟨.Assume c, md⟩ h σ (.normal .vVoid) -- Static Calls (arguments evaluated via δ for simplicity) + -- Note: Arguments are evaluated via the pure evaluator δ rather than + -- EvalLaurelStmt due to Lean 4 mutual inductive limitations. This means + -- call arguments cannot have side effects (e.g., f(g(x)) where g modifies + -- the store will get stuck). See commit message for details. | static_call : π callee = some proc → EvalArgs δ σ args vals → - bindParams σ proc.inputs vals = some σBound → + bindParams proc.inputs vals = some σBound → getBody proc = some body → EvalLaurelStmt δ π h σBound body h' σ' (.normal v) → EvalLaurelStmt δ π h σ ⟨.StaticCall callee args, md⟩ h' σ (.normal v) @@ -276,11 +303,19 @@ inductive EvalLaurelStmt : | static_call_return : π callee = some proc → EvalArgs δ σ args vals → - bindParams σ proc.inputs vals = some σBound → + bindParams proc.inputs vals = some σBound → getBody proc = some body → EvalLaurelStmt δ π h σBound body h' σ' (.ret (some v)) → EvalLaurelStmt δ π h σ ⟨.StaticCall callee args, md⟩ h' σ (.normal v) + | static_call_return_void : + π callee = some proc → + EvalArgs δ σ args vals → + bindParams proc.inputs vals = some σBound → + getBody proc = some body → + EvalLaurelStmt δ π h σBound body h' σ' (.ret none) → + EvalLaurelStmt δ π h σ ⟨.StaticCall callee args, md⟩ h' σ (.normal .vVoid) + -- OO Features | new_obj : @@ -308,11 +343,31 @@ inductive EvalLaurelStmt : h₁ addr = some (typeName, _) → π (typeName ++ "." ++ callee) = some proc → EvalArgs δ σ₁ args vals → - bindParams σ₁ proc.inputs ((.vRef addr) :: vals) = some σBound → + bindParams proc.inputs ((.vRef addr) :: vals) = some σBound → getBody proc = some body → EvalLaurelStmt δ π h₁ σBound body h₂ σ₂ (.normal v) → EvalLaurelStmt δ π h σ ⟨.InstanceCall target callee args, md⟩ h₂ σ₁ (.normal v) + | instance_call_return : + EvalLaurelStmt δ π h σ target h₁ σ₁ (.normal (.vRef addr)) → + h₁ addr = some (typeName, _) → + π (typeName ++ "." ++ callee) = some proc → + EvalArgs δ σ₁ args vals → + bindParams proc.inputs ((.vRef addr) :: vals) = some σBound → + getBody proc = some body → + EvalLaurelStmt δ π h₁ σBound body h₂ σ₂ (.ret (some v)) → + EvalLaurelStmt δ π h σ ⟨.InstanceCall target callee args, md⟩ h₂ σ₁ (.normal v) + + | instance_call_return_void : + EvalLaurelStmt δ π h σ target h₁ σ₁ (.normal (.vRef addr)) → + h₁ addr = some (typeName, _) → + π (typeName ++ "." ++ callee) = some proc → + EvalArgs δ σ₁ args vals → + bindParams proc.inputs ((.vRef addr) :: vals) = some σBound → + getBody proc = some body → + EvalLaurelStmt δ π h₁ σBound body h₂ σ₂ (.ret none) → + EvalLaurelStmt δ π h σ ⟨.InstanceCall target callee args, md⟩ h₂ σ₁ (.normal .vVoid) + | this_sem : σ "this" = some v → EvalLaurelStmt δ π h σ ⟨.This, md⟩ h σ (.normal v) @@ -377,15 +432,16 @@ inductive EvalLaurelBlock : | nil : EvalLaurelBlock δ π h σ [] h σ (.normal .vVoid) - | cons_normal : - EvalLaurelStmt δ π h σ s h₁ σ₁ (.normal v) → - EvalLaurelBlock δ π h₁ σ₁ rest h₂ σ₂ outcome → - EvalLaurelBlock δ π h σ (s :: rest) h₂ σ₂ outcome - | last_normal : EvalLaurelStmt δ π h σ s h' σ' (.normal v) → EvalLaurelBlock δ π h σ [s] h' σ' (.normal v) + | cons_normal : + EvalLaurelStmt δ π h σ s h₁ σ₁ (.normal _v) → + rest ≠ [] → + EvalLaurelBlock δ π h₁ σ₁ rest h₂ σ₂ outcome → + EvalLaurelBlock δ π h σ (s :: rest) h₂ σ₂ outcome + | cons_exit : EvalLaurelStmt δ π h σ s h' σ' (.exit label) → EvalLaurelBlock δ π h σ (s :: _rest) h' σ' (.exit label) diff --git a/StrataTest/Languages/Laurel/LaurelSemanticsTest.lean b/StrataTest/Languages/Laurel/LaurelSemanticsTest.lean index e52608300..d805c30db 100644 --- a/StrataTest/Languages/Laurel/LaurelSemanticsTest.lean +++ b/StrataTest/Languages/Laurel/LaurelSemanticsTest.lean @@ -107,7 +107,7 @@ example : EvalLaurelStmt trivialEval emptyProc emptyHeap emptyStore example : EvalLaurelStmt trivialEval emptyProc emptyHeap emptyStore (mk (.Block [mk (.LiteralInt 1), mk (.LiteralInt 2)] none)) emptyHeap emptyStore (.normal (.vInt 2)) := - .block_sem (.cons_normal .literal_int (.last_normal .literal_int)) (by rfl) + .block_sem (.cons_normal .literal_int (by simp) (.last_normal .literal_int)) (by rfl) /-! ## IfThenElse Tests -/ diff --git a/docs/designs/design-formal-semantics-for-laurel-ir.md b/docs/designs/design-formal-semantics-for-laurel-ir.md index 9097baeed..4ee2d09e9 100644 --- a/docs/designs/design-formal-semantics-for-laurel-ir.md +++ b/docs/designs/design-formal-semantics-for-laurel-ir.md @@ -114,7 +114,7 @@ This evaluator cannot serve as a formal semantics because it is partial, uses a ## 3. Design Options -### Option A: Direct Operational Semantics +### Option A: Direct Operational Semantics (implemented) Define `EvalLaurelStmt` as a standalone inductive relation on `Laurel.StmtExpr`, independent of Core semantics. @@ -493,34 +493,9 @@ Limitations: - Low: Core semantics and properties can be developed and tested independently - The modular structure means each piece can be verified in isolation -## 4. Recommendation +## 4. Decision -**Option C (Hybrid)** is recommended. +**Chosen approach: Option A (Direct Semantics)** — implemented in `LaurelSemantics.lean`. -### Rationale +Option A was chosen as the initial implementation to serve as a reference semantics covering all ~35 `StmtExpr` constructors, including OO features. This provides a complete formal specification against which future translations (Laurel → Core) can be validated. Option C (Hybrid) remains a viable path for translation correctness proofs, where the desugaring pipeline can be verified against the Option A reference semantics. -1. **Matches the existing architecture.** The translation pipeline already performs Laurel→Laurel desugaring (heap parameterization, type hierarchy, expression lifting) before Laurel→Core translation. Option C formalizes this existing structure rather than fighting it. - -2. **Incremental development.** We can deliver value in phases: - - Phase 1: Imperative core semantics + determinism/progress proofs (~800 LOC). This is immediately useful for reasoning about control flow, assignments, and verification constructs. - - Phase 2: Translation correctness for the imperative core → Core (~600 LOC). This validates `translateStmt` for the most common constructs. - - Phase 3: Desugaring correctness for individual passes (can be done per-pass, in any order). - -3. **Right level of abstraction.** Option A tries to formalize everything at once (including OO features that are already desugared away before Core translation). Option B provides no independent semantics at all. Option C gives us a real semantics for the constructs that matter most (control flow, assignments, verification) while deferring the complexity of OO encoding. - -4. **Manageable proof obligations.** The imperative core has ~18 constructors (vs. ~35 for full StmtExpr). Determinism and progress proofs scale with constructor count. The `Outcome` type adds some complexity but is essential for modeling `Exit`/`Return` correctly. - -5. **Reuses existing infrastructure.** The `Outcome` type mirrors `EvalResult` from `LaurelEval.lean`. The store model follows Core's `SemanticStore` pattern. The modular correctness structure follows the existing `EvalStmtRefinesContract` pattern. - -### Suggested implementation order - -1. Define `LaurelValue`, `LaurelStore`, `Outcome` types -2. Define `EvalLaurelStmt` / `EvalLaurelBlock` for imperative core -3. Write concrete evaluation tests -4. Prove determinism for the imperative core -5. Prove store monotonicity -6. Define store correspondence `LaurelStore ↔ CoreStore` -7. Prove `translateStmt` correctness for simple constructs (Assign, LocalVariable, IfThenElse) -8. Extend to While, Block/Exit, Return -9. (Later) Prove desugaring correctness for heap parameterization -10. (Later) Prove desugaring correctness for expression lifting