feat(laurel): Add direct operational semantics for Laurel IR#511

Open

olivier-aws wants to merge 18 commits intostrata-org:mainfrom

olivier-aws:feat/laurel-direct-semantics

Commits on Mar 3, 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

Commits on Mar 10, 2026

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(StatementEval): Merge block handler results to prevent VCG path multiplication
olivier-aws
committed
fix(StatementEval): Address review feedback for Fix VCG path multiplication with goto in if-then-else
olivier-aws
committed
fix(laurel): Address review feedback for Extend LaurelSemantics with store-threading argument evaluation
olivier-aws
committed
docs(StatementEval): Clarify safety of label-based path merging
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

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(laurel): Add direct operational semantics for Laurel IR#511

feat(laurel): Add direct operational semantics for Laurel IR#511
olivier-aws wants to merge 18 commits intostrata-org:mainfrom
olivier-aws:feat/laurel-direct-semantics

Commits on Mar 3, 2026

feat(laurel): Add direct operational semantics for Laurel IR

fix(laurel): Address review feedback for Laurel direct operational semantics

Commits on Mar 10, 2026

feat(laurel): Add auxiliary determinism lemmas for heap ops and EvalArgs

fix(laurel): Address review feedback for Add auxiliary determinism lemmas for heap operations and EvalArgs

feat(laurel): Prove EvalLaurelStmt and EvalLaurelBlock deterministic

fix(laurel): Address review feedback for determinism proof

feat(laurel): Add store-threading argument evaluation (EvalStmtArgs)

fix(StatementEval): Merge block handler results to prevent VCG path multiplication

fix(StatementEval): Address review feedback for Fix VCG path multiplication with goto in if-then-else

fix(laurel): Address review feedback for Extend LaurelSemantics with store-threading argument evaluation

docs(StatementEval): Clarify safety of label-based path merging

feat(laurel): Add tests for extended semantics determinism

feat(laurel): Add lift correctness proof for pure expressions

fix(laurel): Address review feedback for Lift correctness: pure expression preservation

feat(laurel): Prove lift correctness for single assignment in PrimitiveOp

feat(laurel): Add general PrimitiveOp multi-assignment lift correctness

feat(laurel): Add Phase 4 statement-level transformStmt correctness

fix(laurel): Address review feedback for Lift correctness: statement-level transformStmt