feat(laurel): Add direct operational semantics for Laurel IR#511
Open
olivier-aws wants to merge 2 commits intostrata-org:mainfrom
Open
feat(laurel): Add direct operational semantics for Laurel IR#511olivier-aws wants to merge 2 commits intostrata-org:mainfrom
olivier-aws wants to merge 2 commits intostrata-org:mainfrom
Conversation
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)
…mantics 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.
tautschnig
reviewed
Mar 4, 2026
| EvalLaurelStmt δ π h σ s h₁ σ₁ o₁ → | ||
| EvalLaurelStmt δ π h σ s h₂ σ₂ o₂ → | ||
| h₁ = h₂ ∧ σ₁ = σ₂ ∧ o₁ = o₂ := by | ||
| sorry |
Contributor
There was a problem hiding this comment.
Can we actually do the proof?
| EvalLaurelBlock δ π h σ ss h₁ σ₁ o₁ → | ||
| EvalLaurelBlock δ π h σ ss h₂ σ₂ o₂ → | ||
| h₁ = h₂ ∧ σ₁ = σ₂ ∧ o₁ = o₂ := by | ||
| sorry |
Contributor
There was a problem hiding this comment.
Can we actually do the proof?
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
This PR implements Option A from the design document
design-formal-semantics-for-laurel-ir.md: a standalone big-step operational semantics for all ~35 Laurel StmtExpr constructors, independent of Core semantics.Changes
New Files
Strata/Languages/Laurel/LaurelSemantics.lean (~800 LOC)
LaurelValue,LaurelStore,LaurelHeap,OutcometypesEvalLaurelStmt/EvalLaurelBlockrelationsStrata/Languages/Laurel/LaurelSemanticsProps.lean (~500 LOC)
catchExitandevalPrimOppropertiesStrataTest/Languages/Laurel/LaurelSemanticsTest.lean (~300 LOC)
docs/designs/design-formal-semantics-for-laurel-ir.md
Key Design Decisions
Bug Fixes (second commit)
EvalLaurelBlocknon-determinism by addingrest ≠ []side condition tocons_normalstatic_call_return_void,instance_call_return,instance_call_return_void)bindParamsto enforce lexical scoping (start from empty store)Known Limitations
EvalLaurelStmtTesting
All tests pass:
Related
Design document:
docs/designs/design-formal-semantics-for-laurel-ir.md