Enable calling procedures in contracts#1352
Merged
keyboardDrummer merged 146 commits intoJun 23, 2026
Merged
Conversation
…trata into transparency-pass-only
… into issue-924-contract-and-proof-pass
Contributor
|
Re-checked at Note: PR is |
fabiomadge
previously approved these changes
Jun 22, 2026
keyboardDrummer
commented
Jun 23, 2026
… into issue-924-contract-and-proof-pass
joscoh
approved these changes
Jun 23, 2026
robin-aws
approved these changes
Jun 23, 2026
Merged
via the queue into
strata-org:reviewed-kbd-will-merge-to-main
with commit Jun 23, 2026
49c3e1a
15 checks passed
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
5 participants
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.
Functional changes
EliminateReturnsInExpressionnow runs for procedures as well, which enables more types of transparent bodies for procedures. To make it work for both functions and procedures, it was also necessary for the body of functions to be immediately wrapped in a return statement during parsing.LaurelPassconcept so it works for all transformation between Laurel source and Core, not just the Laurel->Laurel transformation. This helps make the documentation more complete.Why let the transparency pass rewrite the bodies of assume statements so they don't assert anything?
After the contract pass, a call will look like
assert <preconditions>; call(..); assume <postconditions>, where the body of the callee looks likeassume <preconditions>; <body>; assert <postconditions>. If we now do either concrete execution, or we do inlining, then any assertions that occur inside the pre or postconditions will be asserted twice, because they occur once in an assert and once in an assume. By ignoring the assertions inside the assume, we prevent the duplication.Whether you also want this behavior for assumptions that were created by users is something I'm not sure about. However, if we want we can let those behave differently. Right now I think we don't have enough data to decide what we want for user created assumptions, and they are AFAIK not yet used, so I think it's OK to change their behavior.
Implementation
Add these passes:
returntoexitstatements, needed for the next pass.Follow-up work