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.
This change adds contract variables that can be declared in the
requires
clause and can be referenced both inrequires
andensures
, subject to usual borrow checking rules. This allows any setup common to both therequires
andensures
clauses to only be done once.In particular, one future use case would be for Fulminate-like ownership assertions in contracts, that are essentially side-effects, and executing them twice would alter the semantics of the contract.
As of this change,
requires
can now be an arbitrary sequence of statements, with the final expression being of typebool
. They are executed in sequence as expected, before checking if the finalbool
expression holds.This PR depends on #144438, and is set as a draft PR until those changes are merged in, so that this branch can be rebased to contain just the new code changes.
Contracts tracking issue: #128044
Other changes introduced:
{}
when using multiple statements. The change is backwards compatible, in that wrapping the content in{}
still works as before. The macros also now treatrequires
andensures
uniformally, meaning therequires
closure is built inside the parser, as opposed to in the macro.Known limiatations:
Contracts with variable declarations are subject to the regular borrow checking rules, and the way contracts are currently lowered limits the usefulness of contract variable declarations. Consider the below example:
We have used the new variable declarations feature to remember the initial value pointed to by
x
, however, movingx
into theensures
does not pass the borrow checker, meaning the above function contract is illegal. Ideally, something like the above should be expressable in contracts.