Laurel semantics#583

Draft

keyboardDrummer wants to merge 31 commits intomainfrom

laurel_semantics

Commits on Mar 16, 2026

feat(laurel): Add direct operational semantics for Laurel IR
olivier-aws
committed
fix(laurel): Address review feedback for Laurel direct operational semantics
olivier-aws
committed
feat(laurel): Add auxiliary determinism lemmas for heap ops and EvalArgs
olivier-aws
committed
fix(laurel): Address review feedback for Add auxiliary determinism lemmas for heap operations and EvalArgs
olivier-aws
committed
feat(laurel): Prove EvalLaurelStmt and EvalLaurelBlock deterministic
olivier-aws
committed
fix(laurel): Address review feedback for determinism proof
olivier-aws
committed
feat(laurel): Add store-threading argument evaluation (EvalStmtArgs)
olivier-aws
committed
fix(laurel): Address review feedback for Extend LaurelSemantics with store-threading argument evaluation
olivier-aws
committed
feat(laurel): Add tests for extended semantics determinism
olivier-aws
committed
feat(laurel): Add lift correctness proof for pure expressions
olivier-aws
committed
fix(laurel): Address review feedback for Lift correctness: pure expression preservation
olivier-aws
committed
feat(laurel): Prove lift correctness for single assignment in PrimitiveOp
olivier-aws
committed
feat(laurel): Add general PrimitiveOp multi-assignment lift correctness
olivier-aws
committed
feat(laurel): Add Phase 4 statement-level transformStmt correctness
olivier-aws
committed
fix(laurel): Address review feedback for Lift correctness: statement-level transformStmt
olivier-aws
committed
add design docs
olivier-aws
committed
feat(laurel): Merge StatementEval VCG path fixes from feat/laurel-direct-semantics
olivier-aws
committed
feat(laurel): Add fuel-based denotational interpreter for Laurel
olivier-aws
committed
feat(laurel): Add bridging lemmas for store/heap helpers
olivier-aws
committed
fix(laurel): Address review feedback for Soundness: denotational interpreter implies relational semantics
olivier-aws
committed
feat(laurel): Prove completeness of denotational interpreter
olivier-aws
committed
feat(laurel): Add equivalence corollaries for denotational semantics
olivier-aws
committed
fix(laurel): Address review feedback for Equivalence corollaries for denotational semantics
olivier-aws
committed
fix(laurel): Adapt semantics to upstream Identifier struct and API changes
olivier-aws
committed
fix(laurel): Remove last two sorry's from denotational soundness proof
olivier-aws
committed
Revert "feat(laurel): Merge StatementEval VCG path fixes from feat/laurel-direct-semantics"
olivier-aws
committed
Remove warnings
olivier-aws
committed
copyright fix
olivier-aws
committed
fix(laurel): Fix CI test failures in laurel_semantics branch
olivier-aws
committed
Remove comments
olivier-aws
committed
Fix CI tests
olivier-aws
committed