feat(laurel): Add direct operational semantics for Laurel IR#511
Open
olivier-aws wants to merge 18 commits intostrata-org:mainfrom
Open
feat(laurel): Add direct operational semantics for Laurel IR#511olivier-aws wants to merge 18 commits intostrata-org:mainfrom
olivier-aws wants to merge 18 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?
Contributor
Author
There was a problem hiding this comment.
Yes, updated the PR (thanks Kiro for 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?
Contributor
Author
There was a problem hiding this comment.
Yes, updated the PR (thanks Kiro for the proof)
Contributor
|
I think we may need to define the two functions |
Add HeapFieldWrite_deterministic and EvalArgs_deterministic lemmas to LaurelSemanticsProps.lean as building blocks for the full EvalLaurelStmt determinism proof. HeapFieldWrite_deterministic: given the same heap, address, field, and value, the resulting heap is unique. Proof by funext and by_cases on address equality. EvalArgs_deterministic: given the same evaluator, store, and expression list, the resulting value list is unique. Proof by induction on the first derivation, using functionality of the pure evaluator δ. AllocHeap_deterministic is NOT included because AllocHeap is non-deterministic in the allocated address — the constructor existentially picks any addr where h addr = none, so two derivations can choose different addresses. The full EvalLaurelStmt determinism proof will need either a weaker formulation (heap bisimilarity up to address renaming) or AllocHeap must be made deterministic (e.g., pick the smallest free address). Design ref: docs/designs/design-formal-semantics-for-laurel-ir.md Chosen design: Option A (Direct Semantics) — auxiliary lemmas for sub-relations to support the main determinism theorem.
…mmas for heap operations and EvalArgs Remove false EvalLaurelStmt_deterministic / EvalLaurelBlock_deterministic theorems that claimed full determinism including heap equality. The new_obj rule uses AllocHeap which existentially picks any free address, making the heap component non-deterministic. A sorry-admitted false theorem is worse than no theorem because downstream proofs could silently inherit unsoundness. Replace with a design-options comment documenting three approaches for recovering a determinism result: deterministic allocator, bisimilarity up to address renaming, or restricted heap-free determinism. Add example-based tests exercising HeapFieldWrite_deterministic and EvalArgs_deterministic on concrete derivations.
Prove full determinism for the Laurel big-step operational semantics: given the same inputs, EvalLaurelStmt and EvalLaurelBlock produce identical heaps, stores, and outcomes. Design: docs/designs/design-formal-semantics-for-laurel-ir.md (Option A) Approach: Mutual structural recursion on the first derivation (term-mode match on H1, tactic-mode cases on H2 inside each branch). Changes: - LaurelSemantics.lean: Add smallest-free-address condition to AllocHeap (∀ a, a < addr → (h a).isSome) making allocation deterministic. This is design option 1 from the prior AllocHeap analysis. - LaurelSemanticsProps.lean: Add AllocHeap_deterministic lemma and complete sorry-free proofs of EvalLaurelStmt_deterministic and EvalLaurelBlock_deterministic covering all constructor pairs. Case structure: - Trivial (13 leaf constructors): direct equality - Single IH (8 cases): chain IH, subst, conclude - Condition+branch (4 ite/while groups): IH on condition, cross-case contradiction via true≠false - Outcome discrimination (while/call variants): IH gives outcome equality, discriminate normal vs exit vs return - Multi-IH (field ops, assigns, calls): chain multiple IH applications Known limitation: maxRecDepth 4096 and maxHeartbeats 800000 needed due to the large number of mutual inductive constructors (~35 stmt, 5 block).
- Remove duplicate set_option directives before mutual block (bug #1) - Add doc comment on AllocHeap.alloc noting bump-allocator invariant and implications for heap deallocation (design concern #1) - Add TODO for heartbeat reduction via call-case helper lemma (design concern strata-org#2, recommendation strata-org#4) - Remove unused catchExit_deterministic and evalPrimOp_deterministic (recommendation strata-org#3)
Add EvalStmtArgs to the mutual inductive block in LaurelSemantics.lean, enabling effectful argument evaluation for PrimitiveOp and all call constructors. This follows Option A from the design document docs/designs/design-extended-semantics-for-effectful-argument-e.md. Changes: - Add EvalStmtArgs (nil/cons) to the EvalLaurelStmt/EvalLaurelBlock mutual block, threading heap and store left-to-right through arguments - Replace EvalArgs with EvalStmtArgs in prim_op and all 6 call constructors (static_call, static_call_return, static_call_return_void, instance_call, instance_call_return, instance_call_return_void) - Change assign_single to return .normal v (assigned value) instead of .normal .vVoid, modeling assignments as expressions (like C "=") - Change assign_field similarly to return .normal v - Use σ_args (store after argument evaluation) as the caller store after calls, consistent with the lifting pass model - Retain old EvalArgs inductive for reasoning about pure sub-expressions - Update file header documentation Known downstream breakage (fixed in subsequent tasks): - LaurelSemanticsProps.lean: determinism proof uses EvalArgs_deterministic on what are now EvalStmtArgs premises; needs EvalStmtArgs_deterministic added to the mutual proof - LaurelSemanticsTest.lean: prim_op tests construct EvalArgs derivations; need updating to EvalStmtArgs with EvalLaurelStmt sub-derivations
…ultiplication When a procedure contains an exit (goto) inside an if-then-else branch, processIteBranches produces multiple EnvWithNext results (one per branch path). These propagate through evalAuxGo and the block handler, which consumes matching exits but does not merge the resulting environments. This causes subsequent procedures in ProgramEval to be verified once per path from the previous procedure, duplicating proof obligations. The fix adds mergeByExitLabel in the block handler: after consuming exits, results that converge to the same exit label are merged using Env.merge. This ensures at most one result per distinct exit label, preventing path multiplication through ProgramEval. Fix VCG path multiplication with goto in if-then-else Ref: strata-org#419
…cation with goto in if-then-else Fix three bugs in the path merging logic: 1. Fix Env.merge argument order in mergeByExitLabel: the true-branch environment must be E1 and false-branch E2. The condition is now extracted and used to identify which environment is which, by detecting the negation pattern (ite cond false true). 2. Fix condition extraction: determine the ite condition by inspecting the path condition structure rather than blindly using the newest entry. The negated form identifies the false branch. 3. Fix repeated merge corruption: replace the foldl-based merge (which corrupted path-condition scopes on 3+ paths) with a match that only merges exactly 2-path groups and leaves larger groups unmerged. Additionally, move merge logic into processIteBranches for same-label exits where cond' is directly available, mirroring the existing single-path merge. Unmatched paths (different exit labels) fall through to the block-level mergeByExitLabel. Add tests for: - Merged variable value correctness (assert r == 1 || r == 0) - Three paths converging to the same exit label via nested ite
…store-threading argument evaluation Fix downstream breakage from EvalArgs → EvalStmtArgs migration: - Add EvalStmtArgs_deterministic to the mutual determinism proof block, returning h₁ = h₂ ∧ σ₁ = σ₂ ∧ vals₁ = vals₂ (heap, store, and values) - Fix all 19 type mismatches in EvalLaurelStmt_deterministic: replace EvalArgs_deterministic with EvalStmtArgs_deterministic in prim_op and all 6 static/instance call cases, propagating heap/store equalities - Fix 5 prim_op tests to use EvalStmtArgs constructors with EvalLaurelStmt sub-derivations instead of EvalArgs constructors with (by rfl) - Add effectful argument evaluation test: x + (x := 1) with x=0 evaluates to 1 with final store x=1, exercising left-to-right store-threading - Reorder EvalStmtArgs before EvalLaurelBlock in the mutual block to match dependency flow (EvalStmtArgs is used by EvalLaurelStmt, not EvalLaurelBlock) - Update TODO comment to reflect EvalStmtArgs structure in call-case prefix - Add documentation comment to EvalArgs_deterministic noting it is retained for reasoning about pure sub-expressions
Address review feedback on PR strata-org#519 regarding label uniqueness concerns. The mergeByExitLabel function is safe even without enforced label uniqueness because it only merges sibling paths (paths that result from evaluating the same block's statements). Label uniqueness across different blocks is irrelevant since we never merge paths from different block evaluations. Added comprehensive documentation explaining: - Why block-level merging is safe - How the two-level merging strategy works - Why this merging is essential to prevent path multiplication Changes: - Enhanced mergeByExitLabel documentation with safety rationale - Added clarifying comment in block handler - Created LABEL_MERGING_SAFETY.md with detailed explanation Ref: strata-org#519 (comment)
Add tests to LaurelSemanticsTest.lean covering the extended semantics from task 005 (EvalStmtArgs, assign_single returning assigned value): - assign_single return value: verify x := 5 evaluates to (.normal (.vInt 5)) rather than (.normal .vVoid), confirming the semantic change - Nested effectful arguments: f((x := 1), (x := 2)) with x=0 produces args [1, 2] with final store x=2, exercising left-to-right threading - Pure EvalStmtArgs: verify EvalStmtArgs on pure args (literals) matches EvalArgs behavior with identity heap/store threading - Empty EvalStmtArgs: verify nil case preserves heap and store - EvalStmtArgs_deterministic: verify the mutual determinism lemma works for effectful argument lists (heap, store, and values all determined) The LaurelSemanticsProps.lean file already contains the complete EvalStmtArgs_deterministic proof in the mutual block, and all prim_op, static_call, and instance_call cases already use it. No changes needed. Design: docs/designs/design-extended-semantics-for-effectful-argument-e.md Chosen option: Option A (mutual EvalStmtArgs + assign_single returns value)
Create LiftImperativeExpressionsCorrectness.lean with Phase 1 of the
bottom-up correctness proof for the lifting pass.
Proved helper lemmas:
- getSubst_run_empty: getSubst with empty subst returns the name
- transformExpr_literal_{int,bool,string}: literals are identity
- transformExpr_identifier: identifiers with empty subst are identity
Stated and structured main theorems:
- transformExpr_pure_preserves: semantic preservation for pure exprs
- containsAssignmentOrImperativeCall_false_no_prepends: no-prepends
- transformExpr_pure_identity: identity on pure expressions
Made getSubst, addToEnv, and containsAssignmentOrImperativeCall public
in LiftImperativeExpressions.lean to enable correctness proofs.
Design reference: Option C (Phased bottom-up proof), Phase 1.
See docs/designs/design-correctness-theorem-for-liftimperativeexpre.md
Known limitations:
- Three sorry's remain in the main theorems for the recursive cases
(PrimitiveOp, IfThenElse, StaticCall, Block). These require proving
that mapM transformExpr is identity on lists of pure expressions,
which needs well-founded induction threading the subst=[] invariant
through StateM computations. The mapM infrastructure lemmas
(List.mapM_fst_pure, List.mapM_state_pure) were developed but the
Lean4 simp/unfold interaction with do-notation StateM functions
proved more complex than anticipated — each monadic helper needs
explicit show/delta to unfold properly within the namespace.
- The proof strategy is sound: show e' = e via the identity property,
then semantic preservation follows by rewriting.
…ssion preservation - Unify purity predicate convention to `= false` across all theorems, replacing `¬ (· = true)` in the main theorem to match supporting lemmas - Remove redundant `hno_prepends` hypothesis from `transformExpr_pure_preserves`; no-prepends is a consequence of purity, not an independent assumption - Reorder file so supporting lemmas (`transformExpr_pure_identity`, `containsAssignmentOrImperativeCall_false_no_prepends`) appear before the main theorem, matching the logical dependency order - Remove unused private `Map.find?_nil` lemma - Add TODO documenting the Block gap: supporting lemmas exclude blocks via `hnotblock` but the main theorem covers all pure expressions - Add note on fragile δ/π universal quantification (sound only because proof strategy is syntactic identity)
…veOp Extend LiftImperativeExpressionsCorrectness.lean with the Phase 2 proof: correctness of lifting a single assignment from PrimitiveOp arguments. Concrete case: op(x, x := e) where e is pure, lifted to: var snap := x; x := e; op(snap, x) Two theorem variants: - lift_single_assign_correct: constructive form taking semantic components as hypotheses, directly constructing the block derivation. - lift_single_assign_from_eval: derivation-based form that inverts an original prim_op derivation and delegates to the constructive form. Key proof technique: define intermediate stores as explicit functions (sigma_snap, sigma_final) and prove store facts (InitStore, UpdateStore, variable lookups) by simp on BEq/Ne. The purity side condition (he_ext) states that e evaluates identically in any store agreeing with the original on all variables except the snapshot name. Also adds helper lemmas to LaurelSemanticsProps.lean: - InitStore_get_other, InitStore_get_self - UpdateStore_get_other, UpdateStore_get_self - EvalLaurelBlock_cons_normal_append Design reference: docs/designs/design-correctness-theorem-for- liftimperativeexpre.md, Option C Phase 2. No sorry. All proofs fully checked by Lean. Known limitation: the purity side condition (he_ext) must be provided by the caller. Phase 3 will generalize this to derive purity from a syntactic IsPure predicate.
Extend LiftImperativeExpressionsCorrectness.lean with Phase 3 of the bottom-up correctness proof: general PrimitiveOp arguments containing multiple assignments. Key additions: LiftImperativeExpressionsCorrectness.lean: - ArgSpec inductive: describes each PrimitiveOp argument as pure or assignment, with its value, snapshot name, and expression - applyArgEffect/threadEffectsRL: model store effects right-to-left, matching the actual execution order of allPrepends - threadEffectsRL_preserves_none: snapshot freshness is preserved through store threading - assign_prepends_eval: the prepended [var snap := x; x := e] block evaluates correctly, producing applyArgEffect on the store - SpecsOK inductive witness: encodes well-formedness and evaluation conditions for a spec list without indexing or BEq instances - allPrepends_eval: the full prepend block evaluates correctly by structural recursion on SpecsOK, composing via EvalLaurelBlock_append - lift_multi_assign_correct: main theorem composing allPrepends_eval with the cleaned PrimitiveOp evaluation LaurelSemanticsProps.lean: - EvalLaurelBlock_append: evaluating ss1 ++ ss2 where ss1 produces .normal decomposes into evaluating ss1 then ss2 - EvalLaurelBlock_append_singleton: variant for singleton ss2 - EvalStmtArgs_cons_inv: decompose EvalStmtArgs on (e :: es) Design reference: Option C (Phased bottom-up proof), Phase 3. See docs/designs/design-correctness-theorem-for-liftimperativeexpre.md Deviation from design: used SpecsOK inductive witness instead of indexed hypotheses (List.get? was removed in Lean 4.27). Used threadEffectsRL (right-to-left) instead of threadEffects (left-to-right) to match the actual execution order of allPrepends. No sorry. All theorems fully proved.
Extend LiftImperativeExpressionsCorrectness.lean with proofs that transformStmt preserves semantics for statement-level constructs. Phase 4 theorems (Option C bottom-up proof, Phase 4): - stmt_to_block: singleton block evaluates same as the statement - transformStmt_assign_correct: prepends ++ [assign] composition - transformStmt_local_var_correct: prepends ++ [local_var] composition - transformStmt_ite_correct: condPrepends ++ [ite] composition - transformStmt_while_correct: condPrepends ++ [while] composition - transformStmt_static_call_correct: prepends ++ [call] composition - transformStmt_block_correct: Block wrapper with catchExit - transformed_block_cons_normal/exit/return: block append lemmas - TransformOK inductive + TransformOK_eval: general block composition The approach follows the design doc's Phase 4 plan: each statement case of transformStmt produces prepends ++ [transformed_stmt], and the proof composes the Phase 3 expression-level results with statement-level semantics via EvalLaurelBlock_append_singleton. The TransformOK inductive provides a general framework for proving that mapping transformStmt over a block preserves semantics: it witnesses that each source statement's transformation evaluates correctly, and TransformOK_eval assembles these into a proof that the flattened target block evaluates correctly. Design reference: docs/designs/design-correctness-theorem-for-liftimperativeexpre.md Chosen design: Option C (Phased bottom-up proof), Phase 4 Known limitations: - Theorems are stated about the output shape (prepends ++ [stmt]), not directly about the monadic transformStmt function. The connection between the monadic output and these shapes is deferred to a future refinement phase. - The TransformOK.cons_normal constructor requires stmts_rest != [] as a side condition, which must be discharged by showing each statement transforms to at least one statement.
…level transformStmt Bug fixes: - Remove no-op transformStmt_block_flatten (was P → P, misleading docstring). The theorem provided no content; block_correct already covers the Block case. - Add last_exit and last_return constructors to TransformOK so singleton non-normal cases are first-class, avoiding the ++ [] workaround via cons_exit/cons_return with empty _stmts_rest. Design improvements: - Add transformStmt_prepend_correct as the single generic lemma for prepend composition. The five per-statement theorems (assign, local_var, ite, while, static_call) are now abbrevs of it, making the shared proof structure explicit. - Add transformStmt_identity_correct for the catch-all identity cases (Return, Exit, Assert, Assume, etc.) to document coverage. - Add comment in While case noting that condition prepends are evaluated once before the loop while seqCond is re-evaluated per iteration; callers must ensure prepends capture loop-invariant values. - Add TODO on TransformOK documenting that cons_normal does not constrain intermediate normal values to agree between source and target.
aqjune-aws
reviewed
Mar 17, 2026
Contributor
aqjune-aws
left a comment
aqjune-aws
left a comment
There was a problem hiding this comment.
Do you also have a plan to add small-step semantics for Laurel? This is helpful for describing the top-level soundness statement of assert (written as a comment below), where assert can be embedded in the middle of an inner block, e.g.,
int x = 1;
...
if (...) {
assert(x == 1);
}
To describe the validity of assert in the if block, we will need steps from the beginning of a program to the middle of if, but big-step style would not represent the program state at this position. In the small-step style, this is possible because what small-step does is really mimicking the interpreter (and hitting the 'stop' on a debugger :) )
| /-! ## Store and Heap -/ | ||
|
|
||
| abbrev LaurelStore := Identifier → Option LaurelValue | ||
| abbrev LaurelHeap := Nat → Option (Identifier × (Identifier → Option LaurelValue)) |
Contributor
There was a problem hiding this comment.
What is the first Identifier in the range of this type?
|
|
||
| | assert_true : | ||
| EvalLaurelStmt δ π h σ c h σ (.normal (.vBool true)) → | ||
| EvalLaurelStmt δ π h σ ⟨.Assert c, md⟩ h σ (.normal .vVoid) |
Contributor
There was a problem hiding this comment.
We are thinking of adding a top-level soundness specification of assert to Strata which looks like this:
forall (s0 s:ProgramState),
init_state(s0) /\ s0 ->* s /\ s.programCounter.instruction = "assert(P)"
==> P(s) holds
which decouples the operational semantics of assert(P) with what actually assert(P) being valid means.
For this reason, #509 is amending assert as a skip instruction. Unless a program state explicitly has "isError?" flag and assert(P) mark as true when P doesn't hold, I think operational semantics of assert shouldn't matter, and simpler semantics of assert is always better.
Could Laurel also use the same style with Core, for easier proof of transformation in the future?
| inductive TransformOK : | ||
| LaurelEval → ProcEnv → LaurelHeap → LaurelStore → | ||
| List StmtExprMd → List StmtExprMd → | ||
| LaurelHeap → LaurelStore → Outcome → Prop where |
Contributor
There was a problem hiding this comment.
It seems TransformOK doesn't directly use the executable transformExpr function in LiftImperativeExpressions - or am I missing it?
| @@ -0,0 +1,672 @@ | |||
| /- | |||
Contributor
There was a problem hiding this comment.
It's not entirely clear to me what the meaning of this correctness proof is. The left translation pass is partial: it panics for certain Laurel programs. How is that reflected in this proof?
|
|
||
| /-! ## Outcomes -/ | ||
|
|
||
| inductive Outcome where |
Contributor
There was a problem hiding this comment.
What about a program with resolution errors? Shouldn't reporting a resolution error be a possible outcome?
| /-! ## Store and Heap -/ | ||
|
|
||
| abbrev LaurelStore := Identifier → Option LaurelValue | ||
| abbrev LaurelHeap := Nat → Option (Identifier × (Identifier → Option LaurelValue)) |
Contributor
There was a problem hiding this comment.
Please use structure instead of × when it's not entirely obvious
| -- Literals | ||
|
|
||
| | literal_int : | ||
| EvalLaurelStmt δ π h σ ⟨.LiteralInt i, md⟩ h σ (.normal (.vInt i)) |
Contributor
There was a problem hiding this comment.
Please don't use single letter identifiers unless their meaning is obvious from the line that they're in (which is rarely the case)
| /-! ## Main Semantic Relations -/ | ||
|
|
||
| mutual | ||
| inductive EvalLaurelStmt : |
Contributor
There was a problem hiding this comment.
Could we compare proofs written using these semantics versus those written using the more interpreter style semantics? I'm really excited about extracting the resolution semantics from the latter.
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
5 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