Skip to content

Conversation

@yoav-el-certora
Copy link
Contributor

No description provided.

nivcertora and others added 6 commits February 25, 2025 12:51
* CERT 8248 Add Revert Example

* Update README

* Address Christiane review

* Update example based on Nurit Review

* Clean
Co-authored-by: yoav-el-certora <122207807+yoav-el-certora@users.noreply.github.com>
…-example

Called Contract and Executing Contract Example
@yoav-el-certora yoav-el-certora changed the title 7.26 Release 7.26.0 Release Mar 11, 2025
@yoav-el-certora yoav-el-certora merged commit ca9d987 into master Mar 13, 2025
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

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants