Laurel API: precondition → preconditions, postcondition → postconditions#481
Merged
keyboardDrummer merged 8 commits intomainfrom Feb 26, 2026
Merged
Laurel API: precondition → preconditions, postcondition → postconditions#481keyboardDrummer merged 8 commits intomainfrom
keyboardDrummer merged 8 commits intomainfrom
Conversation
fabiomadge
force-pushed
the
fabiomadge/laurel-api-changes
branch
from
22fc213 to
f04dd39
Compare
keyboardDrummer
requested changes
Feb 25, 2026
Contributor
keyboardDrummer
left a comment
keyboardDrummer
left a comment
There was a problem hiding this comment.
Looks good, but I left one blocking comment.
fabiomadge
force-pushed
the
fabiomadge/laurel-api-changes
branch
9 times, most recently
from
e59e793 to
c56a53c
Compare
- Laurel.lean: precondition (single) → preconditions (list), postcondition → postconditions in Body.Abstract, Parameter struct reorder, add Repr instances - ConcreteToAbstractTreeTranslator: adapt to list preconditions - LaurelToCoreTranslator: iterate over preconditions list - HeapParameterization: iterate over preconditions/postconditions lists - LaurelFormat: format preconditions list, restore formatDeterminism - LaurelEval: adapt While invariant handling - LiftExpressionAssignments: simplify block ordering - LaurelTypes: reorder operator match - PythonToLaurel, Specs/ToLaurel: adapt to new field names
fabiomadge
force-pushed
the
fabiomadge/laurel-api-changes
branch
from
c56a53c to
f022b9c
Compare
keyboardDrummer
previously approved these changes
Feb 25, 2026
github-merge-queue bot
pushed a commit
that referenced
this pull request
Feb 25, 2026
…ebase (#483) ### Changes Add additional code owners to the Laurel and Python pieces of the codebase. Example PR that this change would allow either of us to review: #481 ### Testing N/A By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.
fabiomadge
force-pushed
the
fabiomadge/laurel-api-changes
branch
from
5b344ec to
12a52bc
Compare
fabiomadge
force-pushed
the
fabiomadge/laurel-api-changes
branch
from
12a52bc to
c08adb2
Compare
keyboardDrummer
previously approved these changes
Feb 25, 2026
andrewmwells-amazon
previously approved these changes
Feb 26, 2026
atomb
reviewed
Feb 26, 2026
fabiomadge
dismissed stale reviews from andrewmwells-amazon and keyboardDrummer
via
1fccd3a
atomb
previously approved these changes
Feb 26, 2026
…/Strata into fabiomadge/laurel-api-changes
atomb
approved these changes
Feb 26, 2026
keyboardDrummer
approved these changes
Feb 26, 2026
andrewmwells-amazon
approved these changes
Feb 26, 2026
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
4 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.
Part of the incremental split of #385. Can be merged independently of #426.
Changes
Converts Laurel's
Procedurefrom a single precondition to a list of preconditions, andBody.Abstractfrom a single postcondition to a list. This enables multiplerequires/ensuresclauses per procedure, which is needed by the upcoming constrained types and contract features.Laurel.lean:
precondition : WithMetadata StmtExpr→preconditions : List (WithMetadata StmtExpr)Body.Abstract postcondition→Body.Abstract (postconditions : List ...)Body.Opaque postcondition→Body.Opaque postconditions(name only, already a list)Parameterstruct, addReprinstancesAdapted callers:
ConcreteToAbstractTreeTranslator— parseOption OptionalRequiresinto listLaurelToCoreTranslator— iterate over preconditions list, generate indexed labels for multiple preconditionsHeapParameterization— fold over preconditions/postconditions listsLaurelFormat— format preconditions/postconditions lists, relocateformatDeterminismPythonToLaurel,Specs/ToLaurel— adapt to new field namesLiftExpressionAssignments.lean:
transformStmtinstead of right-to-left viatransformExprDiscardedtransformExprDiscardedTesting
All existing Laurel, Python, and Core tests pass. No new tests needed — this is a structural refactor with no new features.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.