Required invariant minimal example #166
Merged
Conversation
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
nd-certora
reviewed
Apr 7, 2025
| 2. A **CVL specification** (`DataInvariant.spec`) that declares an invariant requiring **nonnegative** balances. | ||
| 3. A **configuration file** (`DataInvariant.conf`) used to run the Certora Prover with our spec. | ||
|
|
||
| Under the **old** semantics, the invariant won't be enforced at the time the hook triggered, leading to a **false passing** invariant execution. Under the **new** `requireInvariant` semantics, the invariant is checked at rule boundaries or after calls/havocs for strong invariants, correctly **failing** when a negative balance occurs. |
There was a problem hiding this comment.
can we say which version of certora?
the requireinvariant is checked at the rule boundaries on the arguments passed...
There was a problem hiding this comment.
The new version isn't published yet so i am not sure how to mention specific version here, @yoav-el-certora maybe you know how we should handle this.
There was a problem hiding this comment.
Once @johspaeth merge his PR, we will know the release version for this example.
Please keep us updated.
(Both this PR and the other one should not merge before Johannes merge his PR)
Co-authored-by: Nurit Dor <[email protected]>
johspaeth
reviewed
May 27, 2025
nd-certora
approved these changes
May 29, 2025
|
|
||
| - **`DataInvariant.spec`** | ||
| - **Invariant**: `alwaysPositive(address a)` states `currentContract.balance[a] >= 0`. | ||
| The invariant is violated when `breakInvariant` is called under the new semantics but not under the old semantics. |
There was a problem hiding this comment.
instead of new and old use versions
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
https://certora.atlassian.net/browse/CERT-8686