return even more#1005
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: f73fa22bc5
ℹ️ 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".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 2d957e99fe
ℹ️ 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".
| uint256 buyerAssets; | ||
| uint256 sellerAssets; | ||
| buyerAssets, sellerAssets = take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); | ||
| buyerAssets, sellerAssets, _, _, _, _ = take(e, offer, ratifierData, units, taker, receiver, takerCallback, takerCallbackData); |
There was a problem hiding this comment.
Here fee is captured before take, but the spec only comments that reentrancy is disallowed and does not summarize IRatifier.isRatified. Since take calls the ratifier before recomputing _settlementFee, a reentrant ratifier can change the settlement fee between the pre-read and this call, so settlementFeeSpreadBounds compares the returned spread against a stale fee. Add an explicit NONDET/no-reentrancy summary or otherwise constrain the ratifier before relying on this assertion.
Useful? React with 👍 / 👎.
| uint256 buyerAssets; | ||
| uint256 sellerAssets; | ||
| buyerAssets, sellerAssets = take(e, offer, ratifierData, units, taker, receiverIfTakerIsSeller, takerCallback, takerCallbackData); | ||
| buyerAssets, sellerAssets, _, _, _, _ = take(e, offer, ratifierData, units, taker, receiverIfTakerIsSeller, takerCallback, takerCallbackData); |
There was a problem hiding this comment.
The units are computed at line 94 using the current fee, but this subsequent take still permits an arbitrary ratifier; because take calls isRatified before reading the settlement fee, a reentrant ratifier can alter the fee between the library calculation and the take. In that case the returned buyerAssets need not equal targetBuyerAssets, so the rule relies on the comment-only no-reentrancy assumption. Add explicit summaries/constraints for ratifier and callbacks, or require a non-reentrant setup.
Useful? React with 👍 / 👎.
| uint256 seizedResult; | ||
| uint256 repaidResult; | ||
| seizedResult, repaidResult = liquidate(e, market, collateralIndex, seizedAssets, repaidUnits, borrower, postMaturityMode, receiver, callback, data); | ||
| seizedResult, repaidResult, _ = liquidate(e, market, collateralIndex, seizedAssets, repaidUnits, borrower, postMaturityMode, receiver, callback, data); |
There was a problem hiding this comment.
This rule still allows arbitrary callback/data; liquidate computes repaidResult and then invokes onLiquidate before returning. Without a no-reentrancy summary, that callback can reenter functions such as repay, withdraw, or another liquidate and change withdrawable(id) before the post-call assertion, so withdrawableAfter == withdrawableBefore + repaidResult is not a property of the full call. Constrain callback == address(0) or summarize callbacks as non-reentrant if the rule is only about liquidate's own body.
Useful? React with 👍 / 👎.
2 participants
No description provided.