[Certora] Prove that take has no new reverts due to continuous fees - #998
[Certora] Prove that take has no new reverts due to continuous fees#998jhoenicke wants to merge 7 commits into
Conversation
Compare a run of take with zero fees with a run of take with arbitrary fee. Show that if the first does not revert, the second doesn't as well. Requires a deterministic setting (all external gates are modeled by a deterministic ghost).
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 158ad4329f
ℹ️ About Codex in GitHub
Codex has been enabled to automatically review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".
Also set the continuousfee in the second scenario to a new non-zero value. We don't have to require it was zero before and prove an even stronger property that changing the value will not cause new reverts.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 43262ab25d
ℹ️ About Codex in GitHub
Codex has been enabled to automatically review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
When you sign up for Codex through ChatGPT, Codex can also answer questions or update the PR, like "@codex address that feedback".
| function SafeTransferLib.safeTransferFrom(address, address, address, uint256) internal => NONDET; | ||
| function SafeTransferLib.safeTransfer(address, address, uint256) internal => NONDET; |
There was a problem hiding this comment.
not important, but to be 100% correct they should do deterministicSuccess as well no?
3 participants
Compare a run of take with zero fees with a run of take with arbitrary fee. Show that if the first does not revert, the second doesn't as well.
Requires a deterministic setting (all external gates and internal abstracted functions are modelled by a deterministic ghost). This is why it is using its own separate spec file.