Wrap native in Vaults and Blue bundles, refund native#82
Conversation
This reverts commit fbfb661.
QGarchery
changed the title
![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: 81dee74fda
ℹ️ 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".
The wrap-native change makes BlueBundlesV1 mint WNative to the bundler via WNative.deposit on native supply/repay and burn it via WNative.withdraw when refunding the unused native remainder. NoResidue only summarized ERC20 transfers and Morpho methods, so these calls left the persistent bundlerBalance ghost stale on native paths and the no-residue rules compared against a wrong balance. Add deposit/withdraw summaries that credit/debit bundlerBalance by the wrapped/unwrapped amount, keeping the no-residue rules exact on native paths instead of restricting them to msg.value == 0.
certora: model native wrapping in NoResidue
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 528ca0393f
ℹ️ 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 _.deposit() external with(env e) => summaryWrapNative(calledContract, e.msg.value) expect void; | ||
| function _.withdraw(uint256 amount) external => summaryUnwrapNative(calledContract, amount) expect void; | ||
|
|
||
| // Summarized without state changes, as the HAVOC_ECF allows the callee to credit native tokens to the caller. |
There was a problem hiding this comment.
See this resource https://docs.certora.com/en/latest/docs/cvl/methods.html#havoc-summaries-havoc-all-and-havoc-ecf. Third paragraph:
A HAVOC_ECF summarization for a method encodes the assumption that the called method is not reentrant. This summarization approximates a method call by assuming it can have arbitrary effects on contracts other than the contract being verified, but that it can neither change the current contract’s state nor decrease its ETH balance
3 participants
Fixes: