CERT-7022 Add Reset Storage + Hook Example (#132)

* CERT-7022 Add Reset Storage + Hook Example

* Update README.md

* Add index

CVLByExample/HookDisabledOnResetStorageCommand/BankReset.conf

@@ -0,0 +1,7 @@
+{
+    "files": [
+        "BankReset.sol"
+    ],
+    "verify": "BankReset:BankReset.spec",
+    "solc": "solc8.20",
+}

CVLByExample/HookDisabledOnResetStorageCommand/BankReset.sol

@@ -0,0 +1,4 @@
+contract BankReset {
+    mapping (address => uint256) public funds;
+    uint256 public dontUseMe;
+}

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";
+}

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).

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) |