Denotational semantics for Laurel IR with concrete evaluator and transform preservation tests

[olivier-aws]

Denotational semantics for Laurel IR with concrete evaluator and transform preservation tests

Summary

This PR adds a fuel-based denotational interpreter for Laurel IR, a concrete program evaluator, a comprehensive test suite (~130 tests), and transform-preservation infrastructure that validates the Laurel→Laurel lowering pipeline preserves semantics. It also fixes a bug in liftExpressionAssignments that broke evaluation order.

Changes

Denotational interpreter (Strata/Languages/Laurel/)

• LaurelSemantics.lean: Shared semantic types (values, stores, heaps, outcomes) and helper functions (evalPrimOp, bindParams, getBody, etc.) used by the interpreter and evaluator.
• LaurelDenote.lean: Fuel-based denotational interpreter (denoteStmt, denoteBlock, denoteArgs) — three mutually recursive functions covering all StmtExpr constructors exhaustively. Short-circuit operators (AndThen, OrElse, Implies) are handled as special cases before the general PrimitiveOp path. evalPrimOp uses explicit per-operation fallthrough (no wildcard) so adding a new Operation variant forces a build error.
• LaurelDenoteMono.lean: Fuel monotonicity proof — if the interpreter succeeds with fuel n, it succeeds with any m ≥ n giving the same result.
• LaurelConcreteEval.lean: Bridges denoteStmt to Laurel.Program by building ProcEnv from static + instance procedures, constructing the initial store from static fields, and running main.

Test suite (StrataTest/Languages/Laurel/)

• ConcreteEval/: 13 test modules covering primitives, arithmetic, boolean ops (including short-circuit), control flow, variables, procedures, side effects, recursion, aliasing, heap objects, type ops, verification constructs, and edge cases. Shared TestHelper.lean with parseLaurel (parse + resolve) and programmatic AST helpers.
• LaurelDenoteTest.lean, LaurelDenoteUnitTest.lean, LaurelDenoteIntegrationTest.lean, LaurelDenotePropertyTest.lean: Direct tests of the denotational interpreter using both programmatic AST and Plausible property-based testing.
• LaurelConcreteEvalTest.lean: End-to-end tests of the concrete evaluator.

Transform preservation (ConcreteEval/TransformPreservation.lean)

Runs all 94 string-based ConcreteEval tests after the full Laurel→Laurel lowering pipeline (the exact pass sequence from LaurelToCoreTranslator.translate, stopping before Laurel→Core translation). 82/94 pass — the remaining 12 failures are all due to heapParameterization changing the calling convention for composite types.

Bug fix: liftExpressionAssignments

Fixed two bugs in the StaticCall case of transformExpr:

1. Nested call ordering: add(mul(2,3), mul(4,5)) — the outer call's temp variable was declared before inner calls' temps, causing the evaluator to reference undeclared variables.

2. Side-effect evaluation order: add({x:=1;x}, {x:=x+10;x}) — the lifted code didn't preserve left-to-right evaluation order. Fixed by isolating each arg's prepends, capturing side-effectful args in temporaries, and emitting prepend groups in the correct order.

Other improvements

• LaurelToCoreTranslator.lean: Extracted lowerLaurelToLaurel function that runs all Laurel→Laurel passes, reusable by both translate and the test infrastructure.
• Removed applyLift parameter from parseLaurel — tests validate raw Laurel semantics directly.
• Removed unused simp warnings in LaurelDenoteMono.lean.

Testing

• lake build — no warnings from new files
• lake test — all tests pass
• Transform preservation: 82/94 tests match direct-mode output

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[keyboardDrummer]

Runtime compilation might erase assertions and assumptions, and to do that safely their bodies should not have side-effects. The semantics here should check that if the heap/store changes, none is returned.

[olivier-aws]

Agreed in principle. The interpreter already discards the post-condition store/heap and returns the originals, so side effects in assert/assume conditions are invisible to subsequent code. However, we cannot detect impure conditions at runtime because LaurelStore and LaurelHeap are function types (String ? Option LaurelValue and Nat ? Option (...)) which have no BEq or DecidableEq instance in Lean. There is no way to compare two closures for equality. The purity requirement must be enforced statically (e.g., by a well-formedness check on the AST before interpretation) rather than dynamically. Added documentation clarifying this design constraint.

[keyboardDrummer]

However, we cannot detect impure conditions at runtime because LaurelStore and LaurelHeap are function types

What if you use data instead of functions to represent the store and heap? Out of scope for this PR though.

[keyboardDrummer]

It seems you're leaving the meaning of quantifiers unspecified. How about you enable δ to return a List of all possible values of a particular type? Then you can use the fuel to iterate over these values and check the property.

[olivier-aws]

Interesting idea. The current δ callback was designed as an escape hatch for constructs the interpreter can't handle natively. Enumerating all values of a type using fuel would work for finite types (bool, bounded int ranges) but not for unbounded ones (int, string). I could add a typeValues : LaurelType → Option (List LaurelValue) field to δ that returns some for enumerable types and none otherwise.

Happy to add this in a follow-up PR.

[keyboardDrummer]

but not for unbounded ones

Why not? If you run out of fuel then the quantifier holds, so the proof would be of the form: for whatever amount of fuel you start with, the quantifier's value does not change before and after phase P of the compilation.

[keyboardDrummer]

What does delegating to δ mean? Shouldn't these all return a not yet implemented error?

[keyboardDrummer]

The separation between LaurelConcreteEval, LaurelDenote and LaurelSemantics seems arbitrary to me.

[olivier-aws]

LaurelSemantics defines shared types and helpers (values, stores, heaps, evalPrimOp). LaurelInterpreter (formerly LaurelDenote) is the fuel-based interpreter that uses those types. LaurelConcreteEval bridges the interpreter to Laurel.Program by building ProcEnv from program declarations and running main. The split keeps the interpreter independent of the program-level structure. Added module-level doc comments making this layering explicit.

Happy to merge some of these if you feel strongly about it.

[keyboardDrummer]

I don't feel strongly but IMO the "program level structure" is as much a part of the language as any other part of the AST.

[olivier-aws]

I agree and I have a follow-up to this PR that adds an "interpretProgram" method to define the semantics at the program level. I'll update the PR with this part

[robin-aws]

I feel more strongly about this - I think there should be no distinction between the "interpreter" and the "evaluator" anywhere, they should be labeled as the same concept that could potentially be implemented for any elements of a dialect.

I would vote for using "interpreter" in this case, only because "evaluator" is slightly ambiguous in Lean since it has `#eval.

[keyboardDrummer]

This seems awfully complicated. Isn't the change on line 267 and 272 sufficient? If not, can you explain why?

[olivier-aws]

Investigated. The simple change (just lines 267/272) handles the basic case where an imperative call's temp variable needs to be declared after its arguments' temps. But it does NOT handle the evaluation-order bug for side-effectful arguments like add({x:=1;x}, {x:=x+10;x}). In that case we need to:

1. Isolate each argument's prepended statements (so arg2's side effects don't leak into arg1's scope)
2. Capture side-effectful results in temporaries (so the final call uses snapshot values)
3. Emit the prepend groups in left-to-right order (so side effects execute in program order)

The simple fix only addresses point (1). Points (2) and (3) require the full complexity. Added a detailed comment in the code explaining which test cases require each piece.

[keyboardDrummer]

For this example add({x:=1;x}, {x:=x+10;x}), could you write down the before this PR and after this PR translation?

I thought the before would already be:

x := 1;
var x1 := x;
x := x + 10
add(x1, x);

Is something wrong with that, or was it not producing that?

[olivier-aws]

With my change:

procedure main() returns 
 ()
 deterministic
 {
   var x: int := 0;
   x := 1;
   var $c_1: int;
   $c_1 := x;
   x := x + 10;
   var $c_0: int;
   $c_0 := x;
   var $c_2: void;
   $c_2 := add($c_1, $c_0);
   return $c_2
 }

Before my change:

procedure main() returns 
()
deterministic
{
 var x: int := 0;
 var $c_0: void;
 $c_0 := add(x, x);
 x := x + 10;
 x := 1;
 return $c_0
}

[keyboardDrummer]

I think the above code changes are not the correct solution for the bug. I made a fix that I think is correct here: #672

Critical question: did all the changes in LiftImperativeExpressions in this PR make sense to you? I think before submitting a PR the answer has to be yes. I looked at the lifting changes in this PR but I couldn't make sense of them that's why I investigated the bug separately.

[keyboardDrummer]

What's the Laurel program that's failing for you on #672?

I also tried:

function add(x: int, y: int): int {
  x + y
};
procedure repeatedBlockExpressions() {
  var x: int := 2;
  var y: int := { x := 1; x } + { x := x + 10; x };
  var z: int := add({ x := 1; x }, { x := x + 10; x });
  assert y == 1 + 11;
  assert z == 1 + 11
};

this passes verification, and returns:

procedure repeatedBlockExpressions () returns ()
{
  $body: {
    var x : int := 2;
    var $x_1 : int := x;
    x := 1;
    var $x_0 : int := x;
    x := x + 10;
    var y : int := $x_0 + x;
    var $x_3 : int := x;
    x := 1;
    var $x_2 : int := x;
    x := x + 10;
    var z : int := add($x_2, x);
    assert [|assert(2376)|]: y == 1 + 11;
    assert [|assert(2398)|]: z == 1 + 11;
    }
  };

which seems good

The proposed change does make sense to me because I reviewed several iterations

Sorry for questioning that

[olivier-aws]

I integrated the change from #672 into this PR after reverting the change on LiftImperative pass. And then the test

procedure add(a: int, b: int) { return a + b };
procedure main() {
  var x: int := 0;
  return add({x := 1; x}, {x := x + 10; x})
};

would not produce the correct IR.
Maybe it is because of the return statement.

Sorry for questioning that

Don't be, it is very sound to always look for the simplest solution, especially with LLMs that tend to find too complex solutions.

[keyboardDrummer]

#672 has some issues and I'm working on resolving them. I'll update when resolved and I'll include the above test-case as well.

[keyboardDrummer]

#672 was still missing the fixes on lines 267/272 from this PR. With those, the program:

procedure add(a: int, b: int) { return a + b };
procedure main() {
  var x: int := 0;
  return add({x := 1; x}, {x := x + 10; x})
};

passes as well.

[olivier-aws]

Thanks, one #672 is merged I will update the branch and revert these changes then.

[robin-aws]

Just top level feedback so far. I'm inclined to look closer after you merge the interpreter and the evaluator, if you agree, as I believe that will cut some of the documentation and datatype complexity in half.

[robin-aws]

I feel more strongly about this - I think there should be no distinction between the "interpreter" and the "evaluator" anywhere, they should be labeled as the same concept that could potentially be implemented for any elements of a dialect.

I would vote for using "interpreter" in this case, only because "evaluator" is slightly ambiguous in Lean since it has `#eval.

[robin-aws]

It seems simpler to just have the stuck alternative, rather than picking out noMain and noBody as more specific ways to get stuck.

[robin-aws]

I suppose you might be thinking that noMain and noBody are program errors, whereas stuck is an interpreter error? I might buy that, but in that case it would be better to encode the two categories of errors more explicitly in the result naming.

[robin-aws]

Why not make the default fuel something like 2^64 - 1 (or whatever the right value that stops short of expensive bignumber operations)? We only have the fuel so we can still make it technically guaranteed to terminate, but in practice having the interpreter terminate by running out of fuel is never useful information. This number is probably far too low to be a reasonable "timeout" value on large examples, so I think we're better off letting the Lean process run "forever" and we can kill the process if actually necessary.

[robin-aws]

Apologies for the dumb question if this is known, but is Laurel itself deterministic? I had thought not, by design, in which case how is this point true?

[robin-aws]

Here I got confused because LaurelResult has stuck, but I'm again getting confused between the interpreter and the evaluator. Another point that they should be the same thing IMO.

[robin-aws]

This file should probably go under docs instead.

[robin-aws]

Does not seem true of the interpreter, since LaurelResult DOES distinguish.