feat: support postconditions on Laurel functions

[fabiomadge]

Adds support for function postconditions (both ensures clauses and constrained return types) via postcondition axioms and a new OrderedProgram intermediate representation.

Approach

Function postconditions are made available to callers via axioms rather than assume statements. This means postconditions work everywhere — including inside function bodies and quantifiers — without any call-site lifting.

A $check procedure is generated per function with postconditions to verify the body satisfies the postcondition.

Pipeline

Introduces OrderedProgram as an intermediate IR between Laurel.Program and Core.Program:

Program → toLaurelOrdered → generateAxioms → orderedToCore → Core.Program

• toLaurelOrdered — structural analysis: SCC ordering, grouping, diagnostics
• generateAxioms — populates postcondition and invokeOn axioms (can be skipped for a future testing mode)
• orderedToCore — thin translation pass, no structural logic

Grammar

• function f(): int ensures result > 0 { ... } — transparent, body visible to callers
• opaque function f(): int ensures result > 0 { ... } — body hidden, callers only see postcondition via axiom
• function f(): nat { ... } — constrained return type becomes a postcondition

AST change

• Body.Transparent now carries a postconditions list

Key changes

• OrderedProgram.lean / ToOrderedProgram.lean — new IR and structural analysis pass
• FunctionPostcondCheck.lean — generates $check procedures (replaces old FunctionPostcondElim)
• DeclGrouping.lean — renamed from CoreGroupingAndOrdering, no longer depends on Core types
• LaurelToCoreTranslator.lean — orderedToCore replaces monolithic translateLaurelToCore; op nodes annotated with function types at creation
• All Laurel passes: preserve new Transparent postconditions field
• Tests: new cases for opaque-calls-opaque, quantifier postconds, result shadowing

Known trade-off

Opaque function callers get "could not be proved" instead of counterexamples, since the symbolic evaluator cannot instantiate axioms as ground facts. The right fix is in the Core evaluator, which would benefit all frontends.

[keyboardDrummer]

Looking at the implementation:

5. Inserting assume f$post(args, result) at call sites

I don't think that translation is executable. In general I think Laurel should not generate axioms or assume statements.

I think it's better if function postconditions are supported at the Core level, that way the Laurel->Core translation can remain back-end independent, and also then Core can handle everything related to postconditions, both for procedures and functions. There's an AWS internal ticket for adding them to Core.

[fabiomadge]

How else do you propose to add postconditions than to assume them at the call site?

I need them to complete constrained types and think it's better to add them now and remove them later if we end up adding them to Core. Doing it at the Laurel level turned out to be reasonably simple.

[keyboardDrummer]

How else do you propose to add postconditions than to assume them at the call site?

When the back-end has been decided, which is after translating to Core, I think that is the right thing to do.

think it's better to add them now and remove them later if we end up adding them to Core. Doing it at the Laurel level turned out to be reasonably simple.

Why not do the right thing right away? Why would it be easier to add them to Laurel than to Core? I think adding it to Laurel like you did it now breaks our executability promise.

I need them to complete constrained types

Do you have a particular end-target in mind?

[fabiomadge]

When the back-end has been decided, which is after translating to Core, I think that is the right thing to do.

As of now, Core doesn't support postconditions on functions and there is no concrete plan on how to add them.

Why not do the right thing right away? Why would it be easier to add them to Laurel than to Core? I think adding it to Laurel like you did it now breaks our executability promise.

The kind of statement lifting this PR does could also work as an early Core pass, but I think it would be more consistent with the rest of the Core implementation to hold onto them, which makes it harder. I'm not sure how assuming something we've proven elsewhere is breaking any executability promises. I'd expect someone trying to execute the final Core program to ignore these assumptions, just like they would the postconditions.

Do you have a particular end-target in mind?

You mean what I would like to enable? Constrained types as return values in functions. You can see examples in the tests I added.

[keyboardDrummer]

I'm not sure how assuming something we've proven elsewhere is breaking any executability promises. I'd expect someone trying to execute the final Core program to ignore these assumptions, just like they would the postconditions.

You're right. I think I might have incorrectly assumed you were also deleting the body of the function, to make it opaque, but that's not the case. Keeping the body and adding the assume at the call-site seems good from an executability perspective.

---

Another comment though: given that you're inserting an assume statement for calls to functions with postconditions, I imagine this does not work for calls to functions that occur inside a function. Is that right? Could we make that work as well? I'm thinking that axioms are like assume statements that can be used from inside functions as well. What if we replace the postcondition function with a postcondition axiom? That way, you also wouldn't need to lift calls to functions any more since you're not inserting assume statements.

Secondly, generating an axiom (or assume statement) and generating the check procedure per function, is something that I think makes sense when doing symbolic verification, but not when testing, so I think the Laurel pipeline should have an option to enable or disable doing these transformations, even though we don't have a testing mode.

To implement the above requires another change though, since Laurel doesn't have axioms.

An existing issue that we run into is that the top level declarations in Core are ordered, and mutually recursive functions and datatypes must be grouped together, but Laurel has no way of representing top level declarations in that way, so the reordering and grouping is done in the LaurelToCore translation phase, making it thicker than it should be.

I suggest we resolve both those issues by introducing a CoreWithStmtExpr IR, that is similar to Core, so it has axioms and allow ordering and grouping top level decls, but only has procedures, not functions. The procedure body is a Laurel StmtExpr. It might seem a bit heavy handed but I think it'll be worth it.

If you want I can also make the change of introducing CoreWithStmtExpr as a separate PR.

[fabiomadge]

Good catch on the assume-based approach — it worked at call sites but not inside function bodies or quantifier bodies, since assumes are statements and those contexts only allow expressions. The lifting pass was a workaround for that limitation, and it was complex and fragile.

Reworked based on your suggestions:

Axioms instead of assumes. Replaced the lifting + $post + assume machinery with postcondition axioms on functions. Postconditions now work everywhere, including inside functions and quantifiers. Added tests for opaque-calls-opaque, quantifiers, and result shadowing.

Intermediate IR. Introduced OrderedProgram (your CoreWithStmtExpr idea). Pipeline is now:

Program → toLaurelOrdered → generateAxioms → orderedToCore → Core.Program

Ordering/grouping, axiom generation, and Core translation are each a separate pass. generateAxioms can be skipped for a future testing mode.

Other cleanups: groupDatatypes no longer depends on Core types; op nodes annotated at creation (eliminating annotateOps workaround); renamed FunctionPostcondElim → FunctionPostcondCheck.

Known trade-off: The axiom approach means the symbolic evaluator can't produce counterexamples for failing assertions that depend on opaque function postconditions — it reports "could not be proved" instead of "does not hold" with a concrete model. This is because axioms are universally quantified and the evaluator doesn't instantiate them as ground facts. The right fix is in the Core evaluator, which would benefit all frontends.

[github-actions]

👋 Hi, @fabiomadge,
I detected conflicts against the base branch 🙊
You'll want to sync 🔄 your branch with upstream!

---

This message is automatically generated by prince-chrismc/label-merge-conflicts-action so don't hesitate to report issues/improvements there.