Niv/cert 8248 revert example #155
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
christiane-certora
left a comment
christiane-certora
left a comment
There was a problem hiding this comment.
Do we need to mention somewhere that this is still behind the -cvlFunctionRevert flag, or is it enough that the conf uses it?
christiane-certora
approved these changes
Feb 12, 2025
Contributor
christiane-certora
left a comment
christiane-certora
left a comment
There was a problem hiding this comment.
Nice, thanks for the adjustments!
yoav-el-certora
approved these changes
Feb 25, 2025
nd-certora
reviewed
Feb 25, 2025
| /** | ||
| * @notice Dummy function that can be used to demonstrate "summary" usage | ||
| */ | ||
| function summarizeMe(bool b) external {} |
Contributor
There was a problem hiding this comment.
can we have a summzrize for this function that reverts? and then a rule for callSummarizeMe . this is the most interesting case.
Have the rule with sanity true, so we see how the call trace looks like
Contributor
Author
There was a problem hiding this comment.
What do you mean by sanity true?
nd-certora
approved these changes
Feb 25, 2025
yoav-el-certora
added a commit
that referenced
this pull request
Mar 13, 2025
* 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 <122207807+yoav-el-certora@users.noreply.github.com> * Example ready * christiane cr * Code reviews --------- Co-authored-by: Niv vaknin <122722245+nivcertora@users.noreply.github.com> Co-authored-by: liav-certora <114004726+liav-certora@users.noreply.github.com> Co-authored-by: liav-certora <liav@certora.com>
yoav-el-certora
added a commit
that referenced
this pull request
May 18, 2025
* 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 <122207807+yoav-el-certora@users.noreply.github.com> * Example ready * christiane cr * Code reviews * Config inheritance Example (#168) * Config inheritance Example * Update example based on review * CERT add invalid base conf * Update base.conf * CR comment * Update CVLByExample/ConfInheritance/invalid_base.conf Co-authored-by: urikirsh <38188877+urikirsh@users.noreply.github.com> * Fix invalid example --------- Co-authored-by: urikirsh <38188877+urikirsh@users.noreply.github.com> * Niv/cert 8958 add require reasoning (#172) * Add reasoning for require example * Address Nurit comments --------- Co-authored-by: Niv vaknin <122722245+nivcertora@users.noreply.github.com> Co-authored-by: liav-certora <114004726+liav-certora@users.noreply.github.com> Co-authored-by: liav-certora <liav@certora.com> Co-authored-by: urikirsh <38188877+urikirsh@users.noreply.github.com>
johspaeth
pushed a commit
that referenced
this pull request
Jun 30, 2025
* 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 <122207807+yoav-el-certora@users.noreply.github.com> * Example ready * christiane cr * Code reviews --------- Co-authored-by: Niv vaknin <122722245+nivcertora@users.noreply.github.com> Co-authored-by: liav-certora <114004726+liav-certora@users.noreply.github.com> Co-authored-by: liav-certora <liav@certora.com>
johspaeth
added a commit
that referenced
this pull request
Jun 30, 2025
* 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 <122207807+yoav-el-certora@users.noreply.github.com> * Example ready * christiane cr * Code reviews --------- Co-authored-by: Niv vaknin <122722245+nivcertora@users.noreply.github.com> Co-authored-by: liav-certora <114004726+liav-certora@users.noreply.github.com> Co-authored-by: liav-certora <liav@certora.com> * 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 <122207807+yoav-el-certora@users.noreply.github.com> Co-authored-by: Niv vaknin <122722245+nivcertora@users.noreply.github.com> Co-authored-by: liav-certora <114004726+liav-certora@users.noreply.github.com> Co-authored-by: liav-certora <liav@certora.com> Co-authored-by: Otakar <Otakar@certora.com>
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 <122207807+yoav-el-certora@users.noreply.github.com> * Example ready * christiane cr * Code reviews --------- Co-authored-by: Niv vaknin <122722245+nivcertora@users.noreply.github.com> Co-authored-by: liav-certora <114004726+liav-certora@users.noreply.github.com> Co-authored-by: liav-certora <liav@certora.com> * 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 <122207807+yoav-el-certora@users.noreply.github.com> Co-authored-by: Niv vaknin <122722245+nivcertora@users.noreply.github.com> Co-authored-by: liav-certora <114004726+liav-certora@users.noreply.github.com> Co-authored-by: liav-certora <liav@certora.com> Co-authored-by: Otakar <Otakar@certora.com> * 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 <johspaeth@users.noreply.github.com> * 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 <57101353+nd-certora@users.noreply.github.com> Co-authored-by: Johannes Späth <johspaeth@users.noreply.github.com> Co-authored-by: Johannes Spaeth <johannes@certora.com> * Re routing example (#180) * Re routing example * Updating example --------- Co-authored-by: Johannes Spaeth <johannes@certora.com> * 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 <johannes@certora.com> Co-authored-by: yoav-el-certora <122207807+yoav-el-certora@users.noreply.github.com> * 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 <johspaeth@users.noreply.github.com> --------- Co-authored-by: Johannes Späth <johspaeth@users.noreply.github.com> * Added foundry installation to CI (#194) --------- Co-authored-by: Johannes Späth <johspaeth@users.noreply.github.com> Co-authored-by: Niv vaknin <122722245+nivcertora@users.noreply.github.com> Co-authored-by: liav-certora <114004726+liav-certora@users.noreply.github.com> Co-authored-by: liav-certora <liav@certora.com> Co-authored-by: Otakar <Otakar@certora.com> Co-authored-by: Christiane Goltz <christiane@certora.com> Co-authored-by: Nurit Dor <57101353+nd-certora@users.noreply.github.com> Co-authored-by: Johannes Spaeth <johannes@certora.com> Co-authored-by: rahav <rahav@certora.com> Co-authored-by: Rahav <103361134+rahav-certora@users.noreply.github.com> Co-authored-by: Naftali Goldstein <44599898+naftali-g@users.noreply.github.com>
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-8248