feat: support postconditions on Laurel functions#668
Draft
fabiomadge wants to merge 1 commit intomainfrom
Draft
Conversation
fabiomadge
force-pushed
the
feat/function-postconditions
branch
30 times, most recently
from
258b65f to
65bc9af
Compare
fabiomadge
force-pushed
the
feat/function-postconditions
branch
3 times, most recently
from
7e03bc1 to
65afa61
Compare
Add a new Laurel-to-Laurel pass (FunctionPostcondElim) that eliminates function postconditions from both explicit ensures clauses and constrained return types. For each function with postconditions, the pass generates: - A postcondition function (f$post) - A check procedure ($check_f) that verifies the body - assume statements at call sites Functions remain functions in Core with transparent bodies. Opaque functions (opaque keyword) hide the body from callers. Changes: - Laurel.lean: add postconditions field to Body.Transparent - LaurelGrammar.st: add opaque modifier on function - ConcreteToAbstractTreeTranslator.lean: route function bodies to Transparent with postconditions - ConstrainedTypeElim.lean: attach constrained return ensures directly to Transparent postconditions for functions - FunctionPostcondElim.lean: new pass - LaurelToCoreTranslator.lean: wire in new pass, drop body for opaque functions - All Laurel passes: preserve new Transparent postconditions field - Tests: new test cases for all scenarios
fabiomadge
force-pushed
the
feat/function-postconditions
branch
from
65afa61 to
0fdf007
Compare
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
1 participant
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.
Adds support for function postconditions (both
ensuresclauses and constrained return types) via a new Laurel-to-Laurel pass.What it does:
f$postfunction per function with postconditions$check_fprocedure that verifies the body satisfies the postconditionassume f$post(args, result)at call sitesGrammar:
function f(): int ensures result > 0 { ... }— transparent, body visible to callersopaque function f(): int ensures result > 0 { ... }— body hidden, callers only see postconditionfunction f(): nat { ... }— constrained return type becomes a postconditionAST change:
Body.Transparentnow carries a postconditions list, allowing functions to have postconditions without becomingOpaqueWhat changes:
Laurel.lean: add postconditions field toBody.TransparentLaurelGrammar.st: addopaquemodifier onfunctionConcreteToAbstractTreeTranslator.lean: route function bodies toTransparentwith postconditionsConstrainedTypeElim.lean: attach constrained return ensures directly toTransparentpostconditions for functionsFunctionPostcondElim.lean: new pass (~310 lines)LaurelToCoreTranslator.lean: wire in new pass, drop body for opaque functionsTransparentpostconditions field