[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".
| bool revertedDisabled = lastReverted; | ||
|
|
||
| // now set the new continuous fee and check again. | ||
| setMarketContinuousFee(eSetter, id, newContinuousFee) at initState; |
There was a problem hiding this comment.
When offer.market is not already created (tickSpacing(id) == 0), this plain setMarketContinuousFee call reverts with MarketNotCreated, so CVL prunes the path before the enabled take; that excludes the first-take case where touchMarket installs a nonzero defaultContinuousFee, even though the header claims no new take reverts from activating continuous fees. Add a separate default-fee/market-creation comparison or explicitly scope the rule to already-created markets.
AGENTS.md reference: AGENTS.md:L18-L22
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Do I understand this correctly? take can succeed on a not created market. This rule would not revert in the first scenario, it reverts in the second scenario on setMarketContinousFee(), but that revert is not guarded by @withrevert, so the rule succeeds. So in this case we don't compare the defaultContinousFee against the newContinuousFee case. To do that we would need to create the market first, before calling setMarketContinousFee, but only if the market does not already exist?
There was a problem hiding this comment.
Adding @withrevert to setMarketContinuousFee would also need more require to ensure the caller has the permission to set the fee. This clutters the rule a lot. I think it is okay to assume the setMarketContinuousFee will succeed. We already test the scenario where the market is in the state "market is created with default fee".
| if (d == 0 || x * y >= 2 ^ 256) { | ||
| revert(); | ||
| } | ||
| return require_uint256(summaryMulDivDownGhost(x, y, d)); |
There was a problem hiding this comment.
For the rate-dependent fee mulDivDown call, line 66 only upper-bounds the ghost result, so a negative summaryMulDivDownGhost(...) still satisfies the axiom and this require_uint256 then silently prunes the enabled take path instead of proving it cannot add a revert. Add a non-negativity/fit axiom for the summary result or use assert_uint256 so an inadequate summary fails the spec rather than assuming the path away.
AGENTS.md reference: AGENTS.md:L55-L56
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Overapproximating the result is okay here. The prover will try any value of the ghostMulDiv, even the one where it has the right behavior. For these the require_uint256 will not prune the path.
| 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.