[Certora] Reentrancy and View Reentrancy Specification#972
Conversation
![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: fa6d36fee8
ℹ️ About Codex in GitHub
Your team has set up Codex to 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 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| // Copyright (c) 2025 Morpho Association | ||
|
|
||
| methods { | ||
| function multicall(bytes[]) external => HAVOC_ALL DELETE; |
There was a problem hiding this comment.
For the multicall sub-rule, this summary replaces the whole delegatecall loop with HAVOC_ALL, so none of the nested calls execute and the CALL hook never has a chance to set hasCall. A concrete missed case is multicall([setConsumed(...), flashLoan(...)]): the first delegatecall writes consumed, then the second performs token/callback calls, but this rule still passes because multicall was summarized. For this reentrancy property, either model/expand multicall or explicitly document/filter it out rather than reporting the spec as covering all entry points.
Useful? React with 👍 / 👎.
| assert !staticCallAfterSStore; | ||
| //assert !staticCallUnsafe; |
There was a problem hiding this comment.
| assert !staticCallAfterSStore; | |
| //assert !staticCallUnsafe; | |
| assert !staticCallUnsafe; |
agree that it makes more sense to have this spec rather than the one of vault-v2
|
|
||
| methods { | ||
| function multicall(bytes[]) external => HAVOC_ALL DELETE; | ||
| } |
There was a problem hiding this comment.
Let's summarize touchMarket and _updatePosition as NONDET. This is safe because those are done at the beginning, and they keep the state valid (since they could be called independently). Also they don't do calls
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: e5ad4ccb8a
ℹ️ About Codex in GitHub
Your team has set up Codex to 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 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| rule reentrancySafe(method f, env e, calldataarg data) { | ||
| require (!storageChanged && !ignoredCall && !hasCallAfterStore && !unsafeCall, "set up the initial ghost state"); | ||
| f(e,data); | ||
| assert !unsafeCall; |
There was a problem hiding this comment.
For entry points that end immediately after the external call, such as withdraw writing accounting and then calling SafeTransferLib.safeTransfer, the CALL hook only sets hasCallAfterStore; no later SSTORE/TSTORE runs to flip unsafeCall, so this assertion lets that external-call-after-state-change pattern pass. Assert the flag set by the CALL hook, or set unsafeCall directly in the hook, if this rule is meant to prove line 67's no-untrusted-calls claim.
| assert !unsafeCall; | |
| assert !hasCallAfterStore && !unsafeCall; |
Useful? React with 👍 / 👎.
2 participants
First take on the Reentrancy and View Reentrancy. This flags all occurrences where external functions are called after modifiying storage.
This is a DRAFT. Before merging we need to resolve all the flagged calls.