-
Notifications
You must be signed in to change notification settings - Fork 0
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Check variable debt token #5
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
certora/scripts/verifyGhoVariableDebtToken.sh remains the same as in branch cvl2
import {WadRayMath} from '@aave/core-v3/contracts/protocol/libraries/math/WadRayMath.sol'; | ||
import {IPool} from '@aave/core-v3/contracts/interfaces/IPool.sol'; | ||
|
||
contract GhoVariableDebtTokenHarness is GhoVariableDebtToken { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
the contract need to be called harnessInternal like the file.
It should inherit from harness.
&& discountPercent < 5000 // discount rate is less than 50% | ||
=> balanceIncrease > 0; | ||
|
||
assert balanceIncrease > 0 => accumulated_interest_after > accumulated_interest_before; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
what about an assert that additional data is equal current index?
balanceIncrease, discountScaled = accrueDebtOnAction(e, user,previousScaledBalance,discountPercent,index); | ||
uint256 accumulated_interest_after = getUserAccumulatedDebtInterest(user); | ||
|
||
assert ray() <= user_index_before |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This should be changed imo
|
||
|
||
// check user index after mint() | ||
rule user_index_after_mint |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
use filter with all function that call accrue
Add some rules and a helper invariant to cover a bug injected to _accrueDebtOnAction()