Liav/cert 8376 switch cvt image #160
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
7.25.1 Release
nivcertora
approved these changes
Feb 26, 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.
No description provided.