Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

CERT-7022 Add Reset Storage + Hook Example #132

Merged
merged 3 commits into from
Aug 28, 2024

Conversation

nivcertora
Copy link
Contributor

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
@nivcertora nivcertora self-assigned this Aug 27, 2024
certoraRun BankReset.conf
```

3. **Check the Output**: The execution show that the rule `resetZeroesAllFunds` passes, and the hook `Sstore` for `dontUseMe` is never triggered as expected.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The execution shows

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done


### Execution Link

For an example of the output, you can check the execution link: [Certora Run Output](https://prover.certora.com/output/1512/985319a08a424a6e81b8e1dcd9836848?anonymousKey=0ee6ab56949403b32b14f84c4d76ac08eb9acede)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Example of the output attached below:
Example of the output can be seen in the execution link:

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done


## 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.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

need to give a small explanation of rest_storage as this is not even in the dcouemntation.

reset_storage restore to after constructor or just all zero? are ghost also restored? can we add more to this example? it can be a later task. will this pass if in the constructor the msg.sender is allocated funds?

make sure to update the index page as well

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'll add tickets for both Documentation and Example.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@nivcertora nivcertora merged commit ec18c43 into cli-beta Aug 28, 2024
@nivcertora nivcertora deleted the niv/CERT-7022-Add-Hook-On-Reset-Storage-Example branch August 28, 2024 12:38
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.

None yet

3 participants