diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index c915f729..323c82bc 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -64,7 +64,9 @@ jobs: - verifyGhoAToken.sh noMint noBurn noTransfer transferUnderlyingToCantExceedCapacity totalSupplyAlwaysZero userBalanceAlwaysZero handleRepayment_after_transferUnderlyingTo level_does_not_decrease_after_transferUnderlyingTo_followed_by_handleRepayment - verifyGhoDiscountRateStrategy.sh equivalenceOfWadMulCVLAndWadMulSol maxDiscountForHighDiscountTokenBalance zeroDiscountForSmallDiscountTokenBalance partialDiscountForIntermediateTokenBalance limitOnDiscountRate - verifyFlashMinter.sh balanceOfFlashMinterGrows integrityOfTreasurySet integrityOfFeeSet availableLiquidityDoesntChange integrityOfDistributeFeesToTreasury feeSimulationEqualsActualFee + - verifyGhoVariableDebtToken.sh user_index_after_mint accumulated_interest_increase_after_mint user_index_ge_one_ray nonzeroNewDiscountToken - verifyGhoVariableDebtToken.sh discountCantExceed100Percent disallowedFunctionalities nonMintFunctionCantIncreaseBalance nonMintFunctionCantIncreaseScaledBalance debtTokenIsNotTransferable onlyCertainFunctionsCanModifyScaledBalance userAccumulatedDebtInterestWontDecrease userCantNullifyItsDebt integrityOfMint_updateDiscountRate integrityOfMint_updateIndex integrityOfMint_updateScaledBalance_fixedIndex integrityOfMint_userIsolation onlyMintForUserCanIncreaseUsersBalance integrityOfMint_cantDecreaseInterestWithMint integrityMint_atoken integrityOfBurn_updateDiscountRate integrityOfBurn_updateIndex burnZeroDoesntChangeBalance integrityOfBurn_fullRepay_concrete integrityOfBurn_userIsolation integrityOfUpdateDiscountDistribution_updateIndex integrityOfUpdateDiscountDistribution_userIsolation integrityOfRebalanceUserDiscountPercent_updateDiscountRate integrityOfRebalanceUserDiscountPercent_updateIndex integrityOfRebalanceUserDiscountPercent_userIsolation integrityOfBalanceOf_fullDiscount integrityOfBalanceOf_noDiscount integrityOfBalanceOf_zeroScaledBalance burnAllDebtReturnsZeroDebt integrityOfUpdateDiscountRateStrategy discountCantExceedDiscountRate - verifyGhoVariableDebtToken_summarized.sh accrueAlwaysCaleldBeforeRefresh + - verifyGhoVariableDebtTokenIntenal.sh - verifyGhoVariableDebtToken_specialBranch.sh sendersDiscountPercentCannotIncrease - verifyGhoVariableDebtToken-rayMulDiv-summarization.sh diff --git a/certora/harness/ghoVariableDebtTokenHarnessInternal.sol b/certora/harness/ghoVariableDebtTokenHarnessInternal.sol new file mode 100644 index 00000000..c7d0d9e2 --- /dev/null +++ b/certora/harness/ghoVariableDebtTokenHarnessInternal.sol @@ -0,0 +1,26 @@ +pragma solidity 0.8.10; + +import {GhoVariableDebtTokenHarness} from './ghoVariableDebtTokenHarness.sol'; +import {GhoVariableDebtToken} from '../munged/contracts/facilitators/aave/tokens/GhoVariableDebtToken.sol'; +import {IPool} from '@aave/core-v3/contracts/interfaces/IPool.sol'; + +contract GhoVariableDebtTokenHarnessInternal is GhoVariableDebtTokenHarness { + +constructor(IPool pool) public GhoVariableDebtTokenHarness(pool) { + //nop + } + + function accrueDebtOnAction( + address user, + uint256 previousScaledBalance, + uint256 discountPercent, + uint256 index + ) external returns (uint256, uint256) { + return _accrueDebtOnAction( + user, + previousScaledBalance, + discountPercent, + index + ); + } +} diff --git a/certora/scripts/verifyGhoDiscountRateStrategy.sh b/certora/scripts/verifyGhoDiscountRateStrategy.sh index 5cb1db4a..05605099 100644 --- a/certora/scripts/verifyGhoDiscountRateStrategy.sh +++ b/certora/scripts/verifyGhoDiscountRateStrategy.sh @@ -1,5 +1,5 @@ -if (($# > 0)) -then +#if (($# > 0)) +#then certoraRun certora/harness/GhoDiscountRateStrategyHarness.sol:GhoDiscountRateStrategyHarness \ --verify GhoDiscountRateStrategyHarness:certora/specs/ghoDiscountRateStrategy.spec \ --solc solc8.10 \ @@ -7,15 +7,15 @@ certoraRun certora/harness/GhoDiscountRateStrategyHarness.sol:GhoDiscountRateStr --optimistic_loop \ --prover_args "-mediumTimeout 20 -depth 10" \ --smt_timeout 500 \ - --rules "${@}" \ - --msg "GhoDiscountRateStrategy, rules ${@}." -else -certoraRun certora/harness/GhoDiscountRateStrategyHarness.sol:GhoDiscountRateStrategyHarness \ - --verify GhoDiscountRateStrategyHarness:certora/specs/ghoDiscountRateStrategy.spec \ - --solc solc8.10 \ - --loop_iter 2 \ - --optimistic_loop \ - --prover_args "-mediumTimeout 20 -depth 10" \ - --smt_timeout 500 \ - --msg "GhoDiscountRateStrategy, all rules." -fi + --rules "$2" \ + --msg "GhoDiscountRateStrategy, rules $2." +# else +# certoraRun certora/harness/GhoDiscountRateStrategyHarness.sol:GhoDiscountRateStrategyHarness \ +# --verify GhoDiscountRateStrategyHarness:certora/specs/ghoDiscountRateStrategy.spec \ +# --solc solc8.10 \ +# --loop_iter 2 \ +# --optimistic_loop \ +# --prover_args "-mediumTimeout 20 -depth 10" \ +# --smt_timeout 500 \ +# --msg "GhoDiscountRateStrategy, all rules." +# fi diff --git a/certora/scripts/verifyGhoVariableDebtTokenInternal.sh b/certora/scripts/verifyGhoVariableDebtTokenInternal.sh new file mode 100644 index 00000000..f263f8ed --- /dev/null +++ b/certora/scripts/verifyGhoVariableDebtTokenInternal.sh @@ -0,0 +1,11 @@ + +certoraRun certora/harness/ghoVariableDebtTokenHarnessInternal.sol:GhoVariableDebtTokenHarnessInternal \ + certora/munged/contracts/facilitators/aave/interestStrategy/GhoDiscountRateStrategy.sol \ + --verify GhoVariableDebtTokenHarnessInternal:certora/specs/ghoVariableDebtTokenInternal.spec \ + --loop_iter 2 \ + --solc solc8.10 \ + --optimistic_loop \ + --smt_timeout 900 \ + --prover_args "-mediumTimeout 30 -depth 15" \ + --msg "GhoVariableDebtToken internal functions" + diff --git a/certora/specs/ghoVariableDebtToken.spec b/certora/specs/ghoVariableDebtToken.spec index fdd85805..26d35a90 100644 --- a/certora/specs/ghoVariableDebtToken.spec +++ b/certora/specs/ghoVariableDebtToken.spec @@ -48,6 +48,7 @@ methods{ function getUserDiscountRate(address) external returns (uint256) envfree; function getUserAccumulatedDebtInterest(address) external returns (uint256) envfree; function getBalanceOfDiscountToken(address) external returns (uint256); + function getDiscountToken() external returns (address) envfree; /********************************; * GhoVariableDebtToken.sol *; @@ -146,6 +147,74 @@ invariant discountCantExceedDiscountRate(address user) } } + + +//mutatnt 6 +// A new discount token is not address zero +rule nonzeroNewDiscountToken{ + + env e; + address newDiscountToken; + updateDiscountToken(e, newDiscountToken); + assert newDiscountToken != 0; +} + + +// check user index after mint() +rule user_index_after_mint +{ + env e; + address user; + address onBehalfOf; + uint256 amount; + uint256 index; + + uint256 user_index_before = getUserCurrentIndex(onBehalfOf); + mint(e, user, onBehalfOf, amount, index); + uint256 user_index_after = getUserCurrentIndex(onBehalfOf); + assert index > user_index_before => user_index_after > user_index_before; + assert user_index_after == index; +} + +// check accumulated interest after mint() +rule accumulated_interest_increase_after_mint +{ + env e; + address user; + address onBehalfOf; + uint256 amount; + uint256 index; + + requireInvariant user_index_ge_one_ray(e, onBehalfOf); + requireInvariant discountCantExceedDiscountRate(onBehalfOf); + + uint256 user_index_before = getUserCurrentIndex(onBehalfOf); + uint256 balance_before = balanceOf(e, onBehalfOf); + uint256 discount_before = getUserDiscountRate(onBehalfOf); + uint256 accumulated_interest_before = getUserAccumulatedDebtInterest(onBehalfOf); + mint(e, user, onBehalfOf, amount, index); + uint256 accumulated_interest_after = getUserAccumulatedDebtInterest(onBehalfOf); + + + assert balance_before > 0 && to_mathint(user_index_before + ray()) < to_mathint(index) + => accumulated_interest_after > accumulated_interest_before; +} + +// User index >= 1 ray for every user with positive balance +invariant user_index_ge_one_ray(env e1, address user1) + scaledBalanceOf(e1, user1) != 0 => ray() <= getUserCurrentIndex(user1) + { + preserved mint(address user2, address onBehalfOf, uint256 amount, uint256 index) with (env e2) + { + require index >= ray(); //TODO: verify - the Pool calls mint() with index >= 1 ray + } + preserved burn(address from, uint256 amount, uint256 index) with (env e3) + { + require index >= ray(); //TODO: verify - the Pool calls burn() with index >= 1 ray + } + } + + /** * Imported rules from VariableDebtToken.spec **/ diff --git a/certora/specs/ghoVariableDebtTokenInternal.spec b/certora/specs/ghoVariableDebtTokenInternal.spec new file mode 100644 index 00000000..144cf6f2 --- /dev/null +++ b/certora/specs/ghoVariableDebtTokenInternal.spec @@ -0,0 +1,31 @@ +import "ghoVariableDebtToken.spec"; + +methods{ +} + + +// check a scenario that function _accrueDebtOnAction() returns non zero balance increase +rule positive_balanceIncrease { + env e; + address user; + uint256 previousScaledBalance; uint256 discountPercent; uint256 index; + uint256 balanceIncrease; uint256 discountScaled; + uint256 user_index_before = getUserCurrentIndex(user); + uint256 accumulated_interest_before = getUserAccumulatedDebtInterest(user); + balanceIncrease, discountScaled = accrueDebtOnAction(e, user,previousScaledBalance,discountPercent,index); + uint256 accumulated_interest_after = getUserAccumulatedDebtInterest(user); + uint256 user_index_after = getUserCurrentIndex(user); + + assert ray() <= user_index_before + && to_mathint(user_index_before + ray()) < to_mathint(index) // user index increase by more than 1 ray + && 0 < previousScaledBalance + && discountPercent < discStrategy.DISCOUNT_RATE() // discount rate is less than 30% + //(if user index increases by 1 ray discount percent could be as high as 50%) + => balanceIncrease > 0; + + assert balanceIncrease > 0 => accumulated_interest_after > accumulated_interest_before; + + assert user_index_after == index; +} + +