From bcb3c7dd876a184272f6d515a0304c7e4202db77 Mon Sep 17 00:00:00 2001 From: yoav-el-certora <122207807+yoav-el-certora@users.noreply.github.com> Date: Thu, 13 Mar 2025 14:46:24 +0200 Subject: [PATCH 1/8] 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 --- CVLByExample/README.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/CVLByExample/README.md b/CVLByExample/README.md index 5970eb23..7bf6a501 100644 --- a/CVLByExample/README.md +++ b/CVLByExample/README.md @@ -42,8 +42,13 @@ | **directStorageAccess** | [example](https://github.com/Certora/Examples/blob/ad5e75bf63d915bbff634bf8e02c404304eef595/CVLByExample/Immutable/DirectStoragePrivateImmutable.spec#L6) | | **UnresolvedCallSummarization** | [example](https://github.com/Certora/Examples/blob/master/CVLByExample/UnresolvedCallSummarization/TrusterLenderPool.spec) | | **ContractAlias** | [example](https://github.com/Certora/Examples/blob/42395eb745d20c40c14f297fd28b3a658f87f889/CVLByExample/ContractAlias/ContractAlias.spec#L1-L3) | +<<<<<<< HEAD | **StoreToArray** | [example](https://github.com/Certora/Examples/blob/master/CVLByExample/Types/StoreToArray/README.md) | | **HookOnResetStorageCommand** | [example](https://github.com/Certora/Examples/blob/master/CVLByExample/HookDisabledOnResetStorageCommand/README.md) | +======= +| **StoreToArray** | [example](https://github.com/Certora/Examples/blob/niv/CERT-6524/CVLByExample/Types/StoreToArray/StoreToArray.spec#L4) | +| **HookOnResetStorageCommand** | [example](https://github.com/Certora/Examples/blob/niv/CERT-7022-Add-Hook-On-Reset-Storage-Example/CVLByExample/HookDisabledOnResetStorageCommand/BankReset.spec#L1-L10) | +>>>>>>> ca9d987 (7.26.0 Release (#163)) | **RevertKeyWord** | [example](https://github.com/Certora/Examples/blob/niv/CERT-8248-Revert-Example/CVLByExample/RevertKeyWord/example.spec#L13) | From 33b87b91aadda634367634cf6d7ac73602940ae1 Mon Sep 17 00:00:00 2001 From: Otakar Date: Thu, 24 Apr 2025 21:49:18 +0200 Subject: [PATCH 2/8] Bug fixed --- DEFI/ERC4626/certora/specs/ERC4626.spec | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/DEFI/ERC4626/certora/specs/ERC4626.spec b/DEFI/ERC4626/certora/specs/ERC4626.spec index 842419de..682efd97 100644 --- a/DEFI/ERC4626/certora/specs/ERC4626.spec +++ b/DEFI/ERC4626/certora/specs/ERC4626.spec @@ -477,16 +477,16 @@ function callFunctionsWithReceiverAndOwner(env e, method f, uint256 assets, uint if (f.selector == sig:withdraw(uint256,address,address).selector) { withdraw(e, assets, receiver, owner); } - if (f.selector == sig:redeem(uint256,address,address).selector) { + else if (f.selector == sig:redeem(uint256,address,address).selector) { redeem(e, shares, receiver, owner); } - if (f.selector == sig:deposit(uint256,address).selector) { + else if (f.selector == sig:deposit(uint256,address).selector) { deposit(e, assets, receiver); } - if (f.selector == sig:mint(uint256,address).selector) { + else if (f.selector == sig:mint(uint256,address).selector) { mint(e, shares, receiver); } - if (f.selector == sig:transferFrom(address,address,uint256).selector) { + else if (f.selector == sig:transferFrom(address,address,uint256).selector) { transferFrom(e, owner, receiver, shares); } else { From d61ec6e98efe1d24f6198d3729e464b6a6025a55 Mon Sep 17 00:00:00 2001 From: Johannes Spaeth Date: Wed, 4 Jun 2025 13:30:00 +0200 Subject: [PATCH 3/8] Add an example on how to reason about events in CVL --- CVLByExample/Events/README.md | 15 ++++++++ .../Events/certora/specs/Auction.spec | 37 +++++++++++++++++++ CVLByExample/Events/contracts/Auction.sol | 8 ++++ .../Events/contracts/AuctionFixed.sol | 13 +++++++ CVLByExample/Events/runAuctionFixed.conf | 8 ++++ 5 files changed, 81 insertions(+) create mode 100644 CVLByExample/Events/README.md create mode 100644 CVLByExample/Events/certora/specs/Auction.spec create mode 100644 CVLByExample/Events/contracts/Auction.sol create mode 100644 CVLByExample/Events/contracts/AuctionFixed.sol create mode 100644 CVLByExample/Events/runAuctionFixed.conf diff --git a/CVLByExample/Events/README.md b/CVLByExample/Events/README.md new file mode 100644 index 00000000..35dd20ff --- /dev/null +++ b/CVLByExample/Events/README.md @@ -0,0 +1,15 @@ +# Reasoning about Events + +This directory demonstrates how to reason about events with the Prover. +The Prover cannot natively reason about the Events, therefore a workaround is needed. + +The workaround is to wrap the `emits` of Solidity `events` into an internal function and then apply internal summarization to reason about the emitted event. + +- +Run this configuration via: + +```certoraRun runAuctionFixed.conf``` + +[A report of this run](https://prover.certora.com/output/53900/4ffdad0c20094a729d830bfb1b460f3e?anonymousKey=b345ea4d1fe4b3631442c0f110e926a58f47ee9b) + + diff --git a/CVLByExample/Events/certora/specs/Auction.spec b/CVLByExample/Events/certora/specs/Auction.spec new file mode 100644 index 00000000..55b0020c --- /dev/null +++ b/CVLByExample/Events/certora/specs/Auction.spec @@ -0,0 +1,37 @@ +/** + * @title Reasoning about Events example + * + * This is an example specification for reason about events in CVL. + */ + +methods { + function emitBidEvent(address from) internal => cvlEmitBidEvent(from); +} + +persistent ghost bool isEventEmitted; +persistent ghost address emittedEventAddress; + +function cvlEmitBidEvent(address from){ + isEventEmitted = true; + emittedEventAddress = from; +} + +/** + * This rule checks that an event is emitted + */ +rule eventIsEmitted() { + env e; + isEventEmitted = false; + bid(e); + assert isEventEmitted; +} + +/** + * This rule checks that the emitted event address is the one + * that initiated the bid operation. + */ +rule eventEmitsMsgSender() { + env e; + bid(e); + assert emittedEventAddress == e.msg.sender; +} \ No newline at end of file diff --git a/CVLByExample/Events/contracts/Auction.sol b/CVLByExample/Events/contracts/Auction.sol new file mode 100644 index 00000000..0ad8f0b0 --- /dev/null +++ b/CVLByExample/Events/contracts/Auction.sol @@ -0,0 +1,8 @@ +contract Auction +{ + event BidEvent(address from); + function bid() public + { + emit BidEvent(msg.sender); + } +} \ No newline at end of file diff --git a/CVLByExample/Events/contracts/AuctionFixed.sol b/CVLByExample/Events/contracts/AuctionFixed.sol new file mode 100644 index 00000000..461179bf --- /dev/null +++ b/CVLByExample/Events/contracts/AuctionFixed.sol @@ -0,0 +1,13 @@ +contract AuctionFixed +{ + event BidEvent(address from); + function bid() public + { + emitBidEvent(msg.sender); + } + + function emitBidEvent(address from) internal + { + emit BidEvent(from); + } +} \ No newline at end of file diff --git a/CVLByExample/Events/runAuctionFixed.conf b/CVLByExample/Events/runAuctionFixed.conf new file mode 100644 index 00000000..6923ae6b --- /dev/null +++ b/CVLByExample/Events/runAuctionFixed.conf @@ -0,0 +1,8 @@ +{ + "files": [ + "contracts/AuctionFixed.sol", + ], + "verify": "AuctionFixed:certora/specs/Auction.spec", + "msg": "Reasoning about events", + "rule_sanity" : "basic" // check there is a trace satisfying the rule. +} From 601b1748940bf67d1afc4752245b40d8e35a7f88 Mon Sep 17 00:00:00 2001 From: Johannes Spaeth Date: Wed, 4 Jun 2025 22:19:34 +0200 Subject: [PATCH 4/8] Addressing code reviews --- CVLByExample/Events/README.md | 8 +++++--- CVLByExample/Events/certora/specs/Auction.spec | 4 ++-- CVLByExample/Events/runAuctionFixed.conf | 2 +- 3 files changed, 8 insertions(+), 6 deletions(-) diff --git a/CVLByExample/Events/README.md b/CVLByExample/Events/README.md index 35dd20ff..f3cdfcd3 100644 --- a/CVLByExample/Events/README.md +++ b/CVLByExample/Events/README.md @@ -1,10 +1,12 @@ -# Reasoning about Events +# Reasoning about Solidity events -This directory demonstrates how to reason about events with the Prover. -The Prover cannot natively reason about the Events, therefore a workaround is needed. +This directory demonstrates how to reason about Solidity events with the Prover. +The Prover cannot natively reason about events, therefore a workaround is needed. The workaround is to wrap the `emits` of Solidity `events` into an internal function and then apply internal summarization to reason about the emitted event. +See `contracts/Auction.sol` for the original code that uses and an event and take a look at `contract/AuctionFixed.sol` for code that uses the workaround. + - Run this configuration via: diff --git a/CVLByExample/Events/certora/specs/Auction.spec b/CVLByExample/Events/certora/specs/Auction.spec index 55b0020c..12e92482 100644 --- a/CVLByExample/Events/certora/specs/Auction.spec +++ b/CVLByExample/Events/certora/specs/Auction.spec @@ -1,7 +1,7 @@ /** - * @title Reasoning about Events example + * @title Reasoning about Solidity events example * - * This is an example specification for reason about events in CVL. + * This is an example specification for reasoning about events in CVL. */ methods { diff --git a/CVLByExample/Events/runAuctionFixed.conf b/CVLByExample/Events/runAuctionFixed.conf index 6923ae6b..44918fb2 100644 --- a/CVLByExample/Events/runAuctionFixed.conf +++ b/CVLByExample/Events/runAuctionFixed.conf @@ -3,6 +3,6 @@ "contracts/AuctionFixed.sol", ], "verify": "AuctionFixed:certora/specs/Auction.spec", - "msg": "Reasoning about events", + "msg": "Reasoning about Solidity events", "rule_sanity" : "basic" // check there is a trace satisfying the rule. } From a62177a247ce8bcad49a0f2a3d07d005ca296981 Mon Sep 17 00:00:00 2001 From: Johannes Spaeth Date: Thu, 5 Jun 2025 09:45:11 +0200 Subject: [PATCH 5/8] Addressing Christiane's CR --- CVLByExample/Events/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CVLByExample/Events/README.md b/CVLByExample/Events/README.md index f3cdfcd3..464c2870 100644 --- a/CVLByExample/Events/README.md +++ b/CVLByExample/Events/README.md @@ -5,7 +5,7 @@ The Prover cannot natively reason about events, therefore a workaround is needed The workaround is to wrap the `emits` of Solidity `events` into an internal function and then apply internal summarization to reason about the emitted event. -See `contracts/Auction.sol` for the original code that uses and an event and take a look at `contract/AuctionFixed.sol` for code that uses the workaround. +See `contracts/Auction.sol` for the original code that uses an event and take a look at `contract/AuctionFixed.sol` for code that uses the workaround. - Run this configuration via: From 0816b234c135cc34443281cb39bcc533fd757bea Mon Sep 17 00:00:00 2001 From: Johannes Spaeth Date: Mon, 30 Jun 2025 09:10:08 +0200 Subject: [PATCH 6/8] Issue with merge resolution --- CVLByExample/README.md | 5 ----- 1 file changed, 5 deletions(-) diff --git a/CVLByExample/README.md b/CVLByExample/README.md index 7bf6a501..98650191 100644 --- a/CVLByExample/README.md +++ b/CVLByExample/README.md @@ -42,13 +42,8 @@ | **directStorageAccess** | [example](https://github.com/Certora/Examples/blob/ad5e75bf63d915bbff634bf8e02c404304eef595/CVLByExample/Immutable/DirectStoragePrivateImmutable.spec#L6) | | **UnresolvedCallSummarization** | [example](https://github.com/Certora/Examples/blob/master/CVLByExample/UnresolvedCallSummarization/TrusterLenderPool.spec) | | **ContractAlias** | [example](https://github.com/Certora/Examples/blob/42395eb745d20c40c14f297fd28b3a658f87f889/CVLByExample/ContractAlias/ContractAlias.spec#L1-L3) | -<<<<<<< HEAD -| **StoreToArray** | [example](https://github.com/Certora/Examples/blob/master/CVLByExample/Types/StoreToArray/README.md) | -| **HookOnResetStorageCommand** | [example](https://github.com/Certora/Examples/blob/master/CVLByExample/HookDisabledOnResetStorageCommand/README.md) | -======= | **StoreToArray** | [example](https://github.com/Certora/Examples/blob/niv/CERT-6524/CVLByExample/Types/StoreToArray/StoreToArray.spec#L4) | | **HookOnResetStorageCommand** | [example](https://github.com/Certora/Examples/blob/niv/CERT-7022-Add-Hook-On-Reset-Storage-Example/CVLByExample/HookDisabledOnResetStorageCommand/BankReset.spec#L1-L10) | ->>>>>>> ca9d987 (7.26.0 Release (#163)) | **RevertKeyWord** | [example](https://github.com/Certora/Examples/blob/niv/CERT-8248-Revert-Example/CVLByExample/RevertKeyWord/example.spec#L13) | From 214c068a377b245bf6887825e4036ba351cafbd4 Mon Sep 17 00:00:00 2001 From: Johannes Spaeth Date: Mon, 30 Jun 2025 09:10:47 +0200 Subject: [PATCH 7/8] Revert "Bug fixed" This reverts commit 33b87b91aadda634367634cf6d7ac73602940ae1. --- DEFI/ERC4626/certora/specs/ERC4626.spec | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/DEFI/ERC4626/certora/specs/ERC4626.spec b/DEFI/ERC4626/certora/specs/ERC4626.spec index 682efd97..842419de 100644 --- a/DEFI/ERC4626/certora/specs/ERC4626.spec +++ b/DEFI/ERC4626/certora/specs/ERC4626.spec @@ -477,16 +477,16 @@ function callFunctionsWithReceiverAndOwner(env e, method f, uint256 assets, uint if (f.selector == sig:withdraw(uint256,address,address).selector) { withdraw(e, assets, receiver, owner); } - else if (f.selector == sig:redeem(uint256,address,address).selector) { + if (f.selector == sig:redeem(uint256,address,address).selector) { redeem(e, shares, receiver, owner); } - else if (f.selector == sig:deposit(uint256,address).selector) { + if (f.selector == sig:deposit(uint256,address).selector) { deposit(e, assets, receiver); } - else if (f.selector == sig:mint(uint256,address).selector) { + if (f.selector == sig:mint(uint256,address).selector) { mint(e, shares, receiver); } - else if (f.selector == sig:transferFrom(address,address,uint256).selector) { + if (f.selector == sig:transferFrom(address,address,uint256).selector) { transferFrom(e, owner, receiver, shares); } else { From b981ec8ad9697d79eaf85c3274da437bcf487816 Mon Sep 17 00:00:00 2001 From: Johannes Spaeth Date: Mon, 30 Jun 2025 09:14:50 +0200 Subject: [PATCH 8/8] Reverse incorrect change after merge --- CVLByExample/README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/CVLByExample/README.md b/CVLByExample/README.md index 98650191..5970eb23 100644 --- a/CVLByExample/README.md +++ b/CVLByExample/README.md @@ -42,8 +42,8 @@ | **directStorageAccess** | [example](https://github.com/Certora/Examples/blob/ad5e75bf63d915bbff634bf8e02c404304eef595/CVLByExample/Immutable/DirectStoragePrivateImmutable.spec#L6) | | **UnresolvedCallSummarization** | [example](https://github.com/Certora/Examples/blob/master/CVLByExample/UnresolvedCallSummarization/TrusterLenderPool.spec) | | **ContractAlias** | [example](https://github.com/Certora/Examples/blob/42395eb745d20c40c14f297fd28b3a658f87f889/CVLByExample/ContractAlias/ContractAlias.spec#L1-L3) | -| **StoreToArray** | [example](https://github.com/Certora/Examples/blob/niv/CERT-6524/CVLByExample/Types/StoreToArray/StoreToArray.spec#L4) | -| **HookOnResetStorageCommand** | [example](https://github.com/Certora/Examples/blob/niv/CERT-7022-Add-Hook-On-Reset-Storage-Example/CVLByExample/HookDisabledOnResetStorageCommand/BankReset.spec#L1-L10) | +| **StoreToArray** | [example](https://github.com/Certora/Examples/blob/master/CVLByExample/Types/StoreToArray/README.md) | +| **HookOnResetStorageCommand** | [example](https://github.com/Certora/Examples/blob/master/CVLByExample/HookDisabledOnResetStorageCommand/README.md) | | **RevertKeyWord** | [example](https://github.com/Certora/Examples/blob/niv/CERT-8248-Revert-Example/CVLByExample/RevertKeyWord/example.spec#L13) |