[Certora] New spec for checking commutativity of accrueInterests #427
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
We show for supply/withdraw/borrow/repay that calling accrueInterests before has no effect as these function already do this. For all functions we show that calling accrueInterests before or after yields the same result, except for setFeeRecipient, for which it makes a difference (new fee recipient gets the interest if they are accrued afterwards).
This also requires that transfer/transferFrom behave the same, or otherwise safeTransfer differs in revert behaviour
QGarchery
approved these changes
Aug 23, 2023
Merged
QGarchery
changed the title
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
We show for supply/withdraw/borrow/repay that calling
accrueInterestsbefore has no effect as these function already do this.For all functions we show that calling
accrueInterestsbefore or after yields the same result, except forsetFeeRecipient, for which it makes a difference (new fee recipient gets the interest if they are accrued afterwards).Note that the view functions are not commutative, as they return the value before interest is accumulated. I also omitted withdrawCollateral and liquidate from the first function specific rules. They are included in the generic commutativity rule.
The spec is not perfect. We assume the external called functions including the user supplied callbacks won't access the storage. In reality this property is not even true, as e.g. in flashLoan the user callback could read the internal data and behave differently whether or not the interests was already accrued.