CERT 8687 Realistic example #167
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
Contributor
We want to keep both PRs. So this can be merged alongside version 8. I added a label. |
Contributor
|
Assigning @johspaeth (or someone from his team) to complete and merge this Example. |
johspaeth
reviewed
Jul 24, 2025
nd-certora
approved these changes
Aug 3, 2025
| @@ -0,0 +1,45 @@ | |||
| # Sorted Array Invariant Example | |||
|
|
|||
| This folder illustrates how the **new** `requireInvariant` semantics handle a **sorted array** property more accurately than the old semantics. We have: | |||
Contributor
There was a problem hiding this comment.
from version xxx instead of new
| ## Comparing Execution Outputs | ||
|
|
||
| - **Old Semantics** | ||
| [View Output](https://vaas-stg.certora.com/output/1512/784d8a16d9c748ad980619483fe391b0?anonymousKey=4754ecd79909b410927a0af9c3d77afda15d6534) |
Contributor
There was a problem hiding this comment.
links to prover.certora.com are better (they don't break...)
|
|
||
| ### Buggy Implementation | ||
|
|
||
| - **Old semantics**: |
Contributor
There was a problem hiding this comment.
version below 8.0 sematics
|
|
||
| ### Correct Implementation | ||
|
|
||
| - **Old semantics**: |
Contributor
There was a problem hiding this comment.
Below version 8.0 semantics
| [View Output](https://prover.certora.com/output/40726/1636fb234bc74a1bba7f7ee9678b9c4f/?anonymousKey=ff15dfcf8a4da66107d4d7c7f04a49416e992b4d) | ||
| *May incorrectly verify even if the array is temporarily unsorted.* | ||
|
|
||
| - **New semantics**: |
Contributor
There was a problem hiding this comment.
From version 8.0 semantics
yoav-el-certora
added a commit
that referenced
this pull request
Aug 11, 2025
* Add an example on how to reason about events in CVL (#174) * 7.26.0 Release (#163) * Niv/cert 8248 revert example (#155) * CERT 8248 Add Revert Example * Update README * Address Christiane review * Update example based on Nurit Review * Clean * Update config.yml (#160) Co-authored-by: yoav-el-certora <[email protected]> * Example ready * christiane cr * Code reviews --------- Co-authored-by: Niv vaknin <[email protected]> Co-authored-by: liav-certora <[email protected]> Co-authored-by: liav-certora <[email protected]> * Bug fixed * Add an example on how to reason about events in CVL * Addressing code reviews * Addressing Christiane's CR * Issue with merge resolution * Revert "Bug fixed" This reverts commit 33b87b9. * Reverse incorrect change after merge --------- Co-authored-by: yoav-el-certora <[email protected]> Co-authored-by: Niv vaknin <[email protected]> Co-authored-by: liav-certora <[email protected]> Co-authored-by: liav-certora <[email protected]> Co-authored-by: Otakar <[email protected]> * Removed Process from conf file * Removed send_only from conf file * add a simple example with a transient field and hooks and direct storage accesses on it * remove rule sanity Co-authored-by: Johannes Späth <[email protected]> * remove ambiguity * CERT 8687 Realistic example (#167) * CERT 8687 Realistic example * fix spec, sanity issue * fix * require invariant example * Update README * Update CVLByExample/Invariant/RequireInvariantArray/README.md * Addressing Nurit's CR --------- Co-authored-by: Nurit Dor <[email protected]> Co-authored-by: Johannes Späth <[email protected]> Co-authored-by: Johannes Spaeth <[email protected]> * Re routing example (#180) * Re routing example * Updating example --------- Co-authored-by: Johannes Spaeth <[email protected]> * Niv/fix sanity failure (#183) * Fix some of the sanity failure * Fixing specification to not have sanity failures runFullPool.conf -> https://vaas-stg.certora.com/output/53900/a7ab7f221da84eb4accea1c95e936803?anonymousKey=e063b8e60bae944b4a9d0d0431999b5bd4b578ea runBroken.con -> https://vaas-stg.certora.com/output/53900/c85b8c49fec24d32ac0de00043d7ddd6?anonymousKey=a6c585f91d010a7c13f1c6d8935143b894a0c05d * Updates to spec * Self-Review --------- Co-authored-by: Johannes Spaeth <[email protected]> Co-authored-by: yoav-el-certora <[email protected]> * Added fixes to breaking changes (#190) * foundry toml * comment * branch * branch * branch * Add an example for internal function calls (#191) * add an example for internal function calls * Update CVLByExample/InternalFunctionsFromCVL/README.md Co-authored-by: Johannes Späth <[email protected]> --------- Co-authored-by: Johannes Späth <[email protected]> * Added foundry installation to CI (#194) --------- Co-authored-by: Johannes Späth <[email protected]> Co-authored-by: Niv vaknin <[email protected]> Co-authored-by: liav-certora <[email protected]> Co-authored-by: liav-certora <[email protected]> Co-authored-by: Otakar <[email protected]> Co-authored-by: Christiane Goltz <[email protected]> Co-authored-by: Nurit Dor <[email protected]> Co-authored-by: Johannes Spaeth <[email protected]> Co-authored-by: rahav <[email protected]> Co-authored-by: Rahav <[email protected]> Co-authored-by: Naftali Goldstein <[email protected]>
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-8687
Note We need to adjust the example as the invariant is currently violated in both semantic versions.
@nd-certora let me know how to fix it.