diff --git a/CVLByExample/HookDisabledOnResetStorageCommand/BankReset.conf b/CVLByExample/HookDisabledOnResetStorageCommand/BankReset.conf new file mode 100644 index 0000000..a04ba13 --- /dev/null +++ b/CVLByExample/HookDisabledOnResetStorageCommand/BankReset.conf @@ -0,0 +1,7 @@ +{ + "files": [ + "BankReset.sol" + ], + "verify": "BankReset:BankReset.spec", + "solc": "solc8.20", +} \ No newline at end of file diff --git a/CVLByExample/HookDisabledOnResetStorageCommand/BankReset.sol b/CVLByExample/HookDisabledOnResetStorageCommand/BankReset.sol new file mode 100644 index 0000000..cfac27f --- /dev/null +++ b/CVLByExample/HookDisabledOnResetStorageCommand/BankReset.sol @@ -0,0 +1,4 @@ +contract BankReset { + mapping (address => uint256) public funds; + uint256 public dontUseMe; +} \ No newline at end of file diff --git a/CVLByExample/HookDisabledOnResetStorageCommand/BankReset.spec b/CVLByExample/HookDisabledOnResetStorageCommand/BankReset.spec new file mode 100644 index 0000000..b16caa8 --- /dev/null +++ b/CVLByExample/HookDisabledOnResetStorageCommand/BankReset.spec @@ -0,0 +1,10 @@ +hook Sstore currentContract.dontUseMe uint256 newVal (uint256 oldVal) { + assert false, "the hook shouldn't be called"; +} + +rule resetZeroesAllFunds(address to,uint256 amount) { + env e; + require exists address a. currentContract.funds[a] > 0; + reset_storage currentContract; + assert forall address a. currentContract.funds[a] == 0, "all funds should be zero"; +} \ No newline at end of file diff --git a/CVLByExample/HookDisabledOnResetStorageCommand/README.md b/CVLByExample/HookDisabledOnResetStorageCommand/README.md new file mode 100644 index 0000000..4b714e6 --- /dev/null +++ b/CVLByExample/HookDisabledOnResetStorageCommand/README.md @@ -0,0 +1,72 @@ +# Certora Example: Demonstrating Hooks and `reset_storage` + +## Overview + +This repository contains an example that demonstrates how hooks behave in CVL when the `reset_storage` command is used. The example uses a simple Solidity contract named `BankReset` and a CVL specification to show that hooks do not get triggered when storage is reset. + +## Solidity Contract + +The Solidity contract `BankReset` is a straightforward smart contract with a `mapping` that represents funds held by different addresses and a public state variable `dontUseMe`: + +```solidity +pragma solidity ^0.8.0; + +contract BankReset { + mapping (address => uint256) public funds; + uint256 public dontUseMe; +} +``` + +### Contract Details + +- **`funds`**: A mapping that stores the amount of funds each address has in the contract. +- **`dontUseMe`**: A public state variable intended to demonstrate that hooks aren't triggered when storage is reset. + +## Spec + +The specification provides two key elements: + +1. **Hook Definition**: Specifies a hook that triggers on any storage update to the `dontUseMe` variable. +2. **Rule Definition**: Uses `reset_storage` to demonstrate that hooks are not triggered during storage reset. + +### Specification + +```cvl +hook Sstore currentContract.dontUseMe uint256 newVal (uint256 oldVal) { + assert false, "the hook shouldn't be called"; +} + +rule resetZeroesAllFunds(address to, uint256 amount) { + env e; + require exists address a. currentContract.funds[a] > 0; + reset_storage currentContract; + assert forall address a. currentContract.funds[a] == 0, "all funds should be zero"; +} +``` + +### Specification Breakdown + +- **Hook `Sstore`**: This hook is set to trigger on any storage write (`Sstore`) to the variable `dontUseMe`. However, it contains an assertion `assert false` to demonstrate that if it is invoked the rule will get a violation. + +- **Rule `resetZeroesAllFunds`**: This rule verifies that after using the `reset_storage` command on the `BankReset` contract, all funds are zeroed out. It starts by ensuring that there exists at least one address with non-zero funds, then resets the storage and asserts that all funds are zero. + +## Key Points + +- **Hooks and `reset_storage`**: The main point of this example is to show that when the `reset_storage` command is executed, it does not trigger any hooks, even if the storage slots are affected. + +## How to Run the Example + +1. **Run Certora Prover**: + - Command: + ```bash + certoraRun BankReset.conf + ``` + +3. **Check the Output**: The execution shows that the rule `resetZeroesAllFunds` passes, and the hook `Sstore` for `dontUseMe` is never triggered as expected. + +### Execution Link + +An example of the output can be seen in the execution link: [Certora Run Output](https://prover.certora.com/output/1512/985319a08a424a6e81b8e1dcd9836848?anonymousKey=0ee6ab56949403b32b14f84c4d76ac08eb9acede) + + +For further details on Certora Verification Language and best practices, please refer to the [Certora Documentation](https://docs.certora.com). diff --git a/CVLByExample/README.md b/CVLByExample/README.md index 8fe0a10..7615a98 100644 --- a/CVLByExample/README.md +++ b/CVLByExample/README.md @@ -43,6 +43,7 @@ | **UnresolvedCallSummarization** | [example](https://github.com/Certora/Examples/blob/5be4492864f7adb10d01a71628dfbe8343a2868b/CVLByExample/UnresolvedCallSummarization/TrusterLenderPool.spec#L7) | | **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) |