From f55575ed460b8a43a41dc5471f4982ae0916d029 Mon Sep 17 00:00:00 2001 From: gadicer Date: Sun, 19 Nov 2023 12:32:24 +0200 Subject: [PATCH 1/6] add balanceIncrease_ge_previousScaledBalance_gt --- .../ghoVariableDebtTokenHarness_internal.sol | 57 +++++++++++++ .../verifyGhoVariableDebtToken_internal.sh | 18 ++++ certora/specs/ghoVariableDebtToken.spec | 83 ++++++++++++------- .../specs/ghoVariableDebtToken_internal.spec | 20 +++++ 4 files changed, 150 insertions(+), 28 deletions(-) create mode 100644 certora/harness/ghoVariableDebtTokenHarness_internal.sol create mode 100644 certora/scripts/verifyGhoVariableDebtToken_internal.sh create mode 100644 certora/specs/ghoVariableDebtToken_internal.spec diff --git a/certora/harness/ghoVariableDebtTokenHarness_internal.sol b/certora/harness/ghoVariableDebtTokenHarness_internal.sol new file mode 100644 index 00000000..80f1f436 --- /dev/null +++ b/certora/harness/ghoVariableDebtTokenHarness_internal.sol @@ -0,0 +1,57 @@ +pragma solidity 0.8.10; + +import {GhoVariableDebtToken} from '../munged/contracts/facilitators/aave/tokens/GhoVariableDebtToken.sol'; +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 { + using WadRayMath for uint256; + + constructor(IPool pool) public GhoVariableDebtToken(pool) { + //nop + } + + function getUserCurrentIndex(address user) external view returns (uint256) { + return _userState[user].additionalData; + } + + function getUserDiscountRate(address user) external view returns (uint256) { + return _ghoUserState[user].discountPercent; + } + + function getUserAccumulatedDebtInterest(address user) external view returns (uint256) { + return _ghoUserState[user].accumulatedDebtInterest; + } + + function scaledBalanceOfToBalanceOf(uint256 bal) public view returns (uint256) { + return bal.rayMul(POOL.getReserveNormalizedVariableDebt(_underlyingAsset)); + } + + function getBalanceOfDiscountToken(address user) external returns (uint256) { + return _discountToken.balanceOf(user); + } + + function rayMul(uint256 x, uint256 y) external view returns (uint256) { + return x.rayMul(y); + } + + function rayDiv(uint256 x, uint256 y) external view returns (uint256) { + return x.rayDiv(y); + } + + + + 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/verifyGhoVariableDebtToken_internal.sh b/certora/scripts/verifyGhoVariableDebtToken_internal.sh new file mode 100644 index 00000000..879d0406 --- /dev/null +++ b/certora/scripts/verifyGhoVariableDebtToken_internal.sh @@ -0,0 +1,18 @@ +#!/bin/sh + +certoraRun certora/harness/ghoVariableDebtTokenHarness_internal.sol:GhoVariableDebtTokenHarness \ + certora/harness/DummyPool.sol \ + certora/harness/DummyERC20WithTimedBalanceOf.sol \ + certora/munged/contracts/facilitators/aave/interestStrategy/GhoDiscountRateStrategy.sol \ + certora/harness/DummyERC20A.sol certora/harness/DummyERC20B.sol \ + --verify GhoVariableDebtTokenHarness:certora/specs/ghoVariableDebtToken_internal.spec \ + --link GhoVariableDebtTokenHarness:_discountRateStrategy=GhoDiscountRateStrategy \ + --link GhoVariableDebtTokenHarness:_discountToken=DummyERC20WithTimedBalanceOf \ + --link GhoVariableDebtTokenHarness:POOL=DummyPool \ + --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 4087de00..1054a8d6 100644 --- a/certora/specs/ghoVariableDebtToken.spec +++ b/certora/specs/ghoVariableDebtToken.spec @@ -129,6 +129,32 @@ invariant discountCantExceed100Percent(address user) } } +// rule nondecreasing_user_index(method f) filtered { f-> !f.isView } +// { +// env e; calldataarg args; +// address user; +// uint256 index_before = getUserCurrentIndex(user); +// f(e, args); +// uint256 index_after = getUserCurrentIndex(user); +// assert index_after >= index_before; +// } + + +rule user_index_increase_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; +} + /** * Imported rules from VariableDebtToken.spec **/ @@ -488,37 +514,38 @@ rule integrityOfBurn_userIsolation() { /** * @title proves that the discount rate is calculated correctly when calling updateDiscountDistribution **/ -// rule integrityOfUpdateDiscountDistribution_discountRate() { -// address sender; -// address recipient; -// uint256 senderDiscountTokenBalanceBefore; -// uint256 recipientDiscountTokenBalanceBefore; -// uint256 amount; -// uint256 senderDiscountTokenBalanceAfter = senderDiscountTokenBalanceBefore - amount; -// uint256 recipientDiscountTokenBalanceAfter = recipientDiscountTokenBalanceBefore + amount; -// env e0; -// env e; -// require(e.block.timestamp > e0.block.timestamp); -// require(indexAtTimestamp(e.block.timestamp) >= indexAtTimestamp(e0.block.timestamp)); -// require(indexAtTimestamp(e0.block.timestamp) == ray()); // reduces execution time -// require(getUserCurrentIndex(sender) == indexAtTimestamp(e0.block.timestamp)); -// require(getUserCurrentIndex(recipient) == indexAtTimestamp(e0.block.timestamp)); +// TODO: reolve timeout or comment out ruleq +rule integrityOfUpdateDiscountDistribution_discountRate() { + address sender; + address recipient; + uint256 senderDiscountTokenBalanceBefore; + uint256 recipientDiscountTokenBalanceBefore; + uint256 amount; + uint256 senderDiscountTokenBalanceAfter = require_uint256(senderDiscountTokenBalanceBefore - amount); + uint256 recipientDiscountTokenBalanceAfter = require_uint256(recipientDiscountTokenBalanceBefore + amount); + env e0; + env e; + require(e.block.timestamp > e0.block.timestamp); + require(indexAtTimestamp(e.block.timestamp) >= indexAtTimestamp(e0.block.timestamp)); + require(indexAtTimestamp(e0.block.timestamp) == ray()); // reduces execution time + require(getUserCurrentIndex(sender) == indexAtTimestamp(e0.block.timestamp)); + require(getUserCurrentIndex(recipient) == indexAtTimestamp(e0.block.timestamp)); -// require(getBalanceOfDiscountToken(e0, sender) == senderDiscountTokenBalanceBefore); -// require(getBalanceOfDiscountToken(e0, recipient) == recipientDiscountTokenBalanceBefore); -// require(discStrategy.calculateDiscountRate(balanceOf(e0, sender), senderDiscountTokenBalanceBefore) == getUserDiscountRate(sender)); -// require(discStrategy.calculateDiscountRate(balanceOf(e0, recipient), recipientDiscountTokenBalanceBefore) == getUserDiscountRate(recipient)); + require(getBalanceOfDiscountToken(e0, sender) == senderDiscountTokenBalanceBefore); + require(getBalanceOfDiscountToken(e0, recipient) == recipientDiscountTokenBalanceBefore); + require(discStrategy.calculateDiscountRate(balanceOf(e0, sender), senderDiscountTokenBalanceBefore) == getUserDiscountRate(sender)); + require(discStrategy.calculateDiscountRate(balanceOf(e0, recipient), recipientDiscountTokenBalanceBefore) == getUserDiscountRate(recipient)); -// require(getBalanceOfDiscountToken(e, sender) == senderDiscountTokenBalanceAfter); -// require(getBalanceOfDiscountToken(e, recipient) == recipientDiscountTokenBalanceAfter); - -// updateDiscountDistribution(e, sender, recipient, senderDiscountTokenBalanceBefore, recipientDiscountTokenBalanceBefore, amount); -// uint256 senderBalance = balanceOf(e, sender); -// uint256 recipientBalance = balanceOf(e, recipient); -// assert(discStrategy.calculateDiscountRate(senderBalance, senderDiscountTokenBalanceAfter) == getUserDiscountRate(sender)); -// assert(discStrategy.calculateDiscountRate(recipientBalance, recipientDiscountTokenBalanceAfter) == getUserDiscountRate(recipient)); -// } + require(getBalanceOfDiscountToken(e, sender) == senderDiscountTokenBalanceAfter); + require(getBalanceOfDiscountToken(e, recipient) == recipientDiscountTokenBalanceAfter); + + updateDiscountDistribution(e, sender, recipient, senderDiscountTokenBalanceBefore, recipientDiscountTokenBalanceBefore, amount); + uint256 senderBalance = balanceOf(e, sender); + uint256 recipientBalance = balanceOf(e, recipient); + assert(discStrategy.calculateDiscountRate(senderBalance, senderDiscountTokenBalanceAfter) == getUserDiscountRate(sender)); + assert(discStrategy.calculateDiscountRate(recipientBalance, recipientDiscountTokenBalanceAfter) == getUserDiscountRate(recipient)); +} /** * @title proves the after calling updateDiscountDistribution, the user's state is updated with the recent index value diff --git a/certora/specs/ghoVariableDebtToken_internal.spec b/certora/specs/ghoVariableDebtToken_internal.spec new file mode 100644 index 00000000..301de225 --- /dev/null +++ b/certora/specs/ghoVariableDebtToken_internal.spec @@ -0,0 +1,20 @@ +import "ghoVariableDebtToken.spec"; + + + +methods{ +} + + +rule balanceIncrease_ge_previousScaledBalance_gt { + env e; + address user; + uint256 previousScaledBalance; uint256 discountPercent; uint256 index; + uint256 balanceIncrease; uint256 discountScaled; + uint256 user_index_before = getUserCurrentIndex(user); + balanceIncrease, discountScaled = accrueDebtOnAction(e, user,previousScaledBalance,discountPercent,index); + + assert user_index_before > require_uint256(index + ray()) && previousScaledBalance > 0 => balanceIncrease > 0; +} + + From ee2563c71d3b982b16bc49a475bdce0d337d4f38 Mon Sep 17 00:00:00 2001 From: gadicer Date: Tue, 21 Nov 2023 00:45:05 +0200 Subject: [PATCH 2/6] add accumulated_interest_increase_after_mint to CI --- .github/workflows/certora.yml | 2 + .../scripts/verifyGhoDiscountRateStrategy.sh | 28 ++++++------- certora/specs/ghoVariableDebtToken.spec | 39 +++++++++++++------ .../specs/ghoVariableDebtToken_internal.spec | 18 ++++++--- 4 files changed, 55 insertions(+), 32 deletions(-) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 94d56033..7b26b570 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -66,3 +66,5 @@ jobs: - verifyGhoDiscountRateStrategy.sh equivalenceOfWadMulCVLAndWadMulSol maxDiscountForHighDiscountTokenBalance zeroDiscountForSmallDiscountTokenBalance partialDiscountForIntermediateTokenBalance limitOnDiscountRate - verifyFlashMinter.sh balanceOfFlashMinterGrows integrityOfTreasurySet integrityOfFeeSet availableLiquidityDoesntChange integrityOfDistributeFeesToTreasury feeSimulationEqualsActualFee - 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 + - verifyGhoVariableDebtToken.sh user_index_after_mint accumulated_interest_increase_after_mint + - verifyGhoVariableDebtToken_intenal.sh \ No newline at end of file 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/specs/ghoVariableDebtToken.spec b/certora/specs/ghoVariableDebtToken.spec index 1054a8d6..eacb1a9e 100644 --- a/certora/specs/ghoVariableDebtToken.spec +++ b/certora/specs/ghoVariableDebtToken.spec @@ -129,18 +129,9 @@ invariant discountCantExceed100Percent(address user) } } -// rule nondecreasing_user_index(method f) filtered { f-> !f.isView } -// { -// env e; calldataarg args; -// address user; -// uint256 index_before = getUserCurrentIndex(user); -// f(e, args); -// uint256 index_after = getUserCurrentIndex(user); -// assert index_after >= index_before; -// } - -rule user_index_increase_after_mint +// check user index after mint() +rule user_index_after_mint { env e; address user; @@ -151,10 +142,34 @@ rule user_index_increase_after_mint 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 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; + + 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 ray() <= user_index_before + && to_mathint(user_index_before + ray()) < to_mathint(index) + && balance_before > 0 + && discount_before < 5000 + => accumulated_interest_after > accumulated_interest_before; +} + /** * Imported rules from VariableDebtToken.spec **/ diff --git a/certora/specs/ghoVariableDebtToken_internal.spec b/certora/specs/ghoVariableDebtToken_internal.spec index 301de225..a3f44b25 100644 --- a/certora/specs/ghoVariableDebtToken_internal.spec +++ b/certora/specs/ghoVariableDebtToken_internal.spec @@ -1,20 +1,26 @@ import "ghoVariableDebtToken.spec"; - - methods{ } - -rule balanceIncrease_ge_previousScaledBalance_gt { +// 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); - - assert user_index_before > require_uint256(index + ray()) && previousScaledBalance > 0 => balanceIncrease > 0; + uint256 accumulated_interest_after = getUserAccumulatedDebtInterest(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 < 5000 // discount rate is less than 50% + => balanceIncrease > 0; + + assert balanceIncrease > 0 => accumulated_interest_after > accumulated_interest_before; } From f1dd72544617e894dfbf114d0a7d2b32a51e8b47 Mon Sep 17 00:00:00 2001 From: gadicer Date: Tue, 21 Nov 2023 01:17:34 +0200 Subject: [PATCH 3/6] comment out timeout rule --- .../verifyGhoVariableDebtToken_internal.sh | 1 - certora/specs/ghoVariableDebtToken.spec | 58 +++++++++---------- 2 files changed, 29 insertions(+), 30 deletions(-) diff --git a/certora/scripts/verifyGhoVariableDebtToken_internal.sh b/certora/scripts/verifyGhoVariableDebtToken_internal.sh index 879d0406..3f458272 100644 --- a/certora/scripts/verifyGhoVariableDebtToken_internal.sh +++ b/certora/scripts/verifyGhoVariableDebtToken_internal.sh @@ -1,4 +1,3 @@ -#!/bin/sh certoraRun certora/harness/ghoVariableDebtTokenHarness_internal.sol:GhoVariableDebtTokenHarness \ certora/harness/DummyPool.sol \ diff --git a/certora/specs/ghoVariableDebtToken.spec b/certora/specs/ghoVariableDebtToken.spec index eacb1a9e..8f44f423 100644 --- a/certora/specs/ghoVariableDebtToken.spec +++ b/certora/specs/ghoVariableDebtToken.spec @@ -529,38 +529,38 @@ rule integrityOfBurn_userIsolation() { /** * @title proves that the discount rate is calculated correctly when calling updateDiscountDistribution **/ -// TODO: reolve timeout or comment out ruleq -rule integrityOfUpdateDiscountDistribution_discountRate() { - address sender; - address recipient; - uint256 senderDiscountTokenBalanceBefore; - uint256 recipientDiscountTokenBalanceBefore; - uint256 amount; - uint256 senderDiscountTokenBalanceAfter = require_uint256(senderDiscountTokenBalanceBefore - amount); - uint256 recipientDiscountTokenBalanceAfter = require_uint256(recipientDiscountTokenBalanceBefore + amount); - env e0; - env e; - require(e.block.timestamp > e0.block.timestamp); - require(indexAtTimestamp(e.block.timestamp) >= indexAtTimestamp(e0.block.timestamp)); - require(indexAtTimestamp(e0.block.timestamp) == ray()); // reduces execution time - require(getUserCurrentIndex(sender) == indexAtTimestamp(e0.block.timestamp)); - require(getUserCurrentIndex(recipient) == indexAtTimestamp(e0.block.timestamp)); +// TODO: enable when timeout is resolved +// rule integrityOfUpdateDiscountDistribution_discountRate() { +// address sender; +// address recipient; +// uint256 senderDiscountTokenBalanceBefore; +// uint256 recipientDiscountTokenBalanceBefore; +// uint256 amount; +// uint256 senderDiscountTokenBalanceAfter = require_uint256(senderDiscountTokenBalanceBefore - amount); +// uint256 recipientDiscountTokenBalanceAfter = require_uint256(recipientDiscountTokenBalanceBefore + amount); +// env e0; +// env e; +// require(e.block.timestamp > e0.block.timestamp); +// require(indexAtTimestamp(e.block.timestamp) >= indexAtTimestamp(e0.block.timestamp)); +// require(indexAtTimestamp(e0.block.timestamp) == ray()); // reduces execution time +// require(getUserCurrentIndex(sender) == indexAtTimestamp(e0.block.timestamp)); +// require(getUserCurrentIndex(recipient) == indexAtTimestamp(e0.block.timestamp)); - require(getBalanceOfDiscountToken(e0, sender) == senderDiscountTokenBalanceBefore); - require(getBalanceOfDiscountToken(e0, recipient) == recipientDiscountTokenBalanceBefore); - require(discStrategy.calculateDiscountRate(balanceOf(e0, sender), senderDiscountTokenBalanceBefore) == getUserDiscountRate(sender)); - require(discStrategy.calculateDiscountRate(balanceOf(e0, recipient), recipientDiscountTokenBalanceBefore) == getUserDiscountRate(recipient)); +// require(getBalanceOfDiscountToken(e0, sender) == senderDiscountTokenBalanceBefore); +// require(getBalanceOfDiscountToken(e0, recipient) == recipientDiscountTokenBalanceBefore); +// require(discStrategy.calculateDiscountRate(balanceOf(e0, sender), senderDiscountTokenBalanceBefore) == getUserDiscountRate(sender)); +// require(discStrategy.calculateDiscountRate(balanceOf(e0, recipient), recipientDiscountTokenBalanceBefore) == getUserDiscountRate(recipient)); - require(getBalanceOfDiscountToken(e, sender) == senderDiscountTokenBalanceAfter); - require(getBalanceOfDiscountToken(e, recipient) == recipientDiscountTokenBalanceAfter); - - updateDiscountDistribution(e, sender, recipient, senderDiscountTokenBalanceBefore, recipientDiscountTokenBalanceBefore, amount); - uint256 senderBalance = balanceOf(e, sender); - uint256 recipientBalance = balanceOf(e, recipient); - assert(discStrategy.calculateDiscountRate(senderBalance, senderDiscountTokenBalanceAfter) == getUserDiscountRate(sender)); - assert(discStrategy.calculateDiscountRate(recipientBalance, recipientDiscountTokenBalanceAfter) == getUserDiscountRate(recipient)); -} +// require(getBalanceOfDiscountToken(e, sender) == senderDiscountTokenBalanceAfter); +// require(getBalanceOfDiscountToken(e, recipient) == recipientDiscountTokenBalanceAfter); + +// updateDiscountDistribution(e, sender, recipient, senderDiscountTokenBalanceBefore, recipientDiscountTokenBalanceBefore, amount); +// uint256 senderBalance = balanceOf(e, sender); +// uint256 recipientBalance = balanceOf(e, recipient); +// assert(discStrategy.calculateDiscountRate(senderBalance, senderDiscountTokenBalanceAfter) == getUserDiscountRate(sender)); +// assert(discStrategy.calculateDiscountRate(recipientBalance, recipientDiscountTokenBalanceAfter) == getUserDiscountRate(recipient)); +// } /** * @title proves the after calling updateDiscountDistribution, the user's state is updated with the recent index value From 4c57bfe281c22ab0883b71659bb1437ecb6bcd7b Mon Sep 17 00:00:00 2001 From: gadicer Date: Tue, 21 Nov 2023 02:55:15 +0200 Subject: [PATCH 4/6] add user_index_ge_one_ray --- .github/workflows/certora.yml | 2 +- certora/specs/ghoVariableDebtToken.spec | 36 ++++++++++++++++++++++--- 2 files changed, 34 insertions(+), 4 deletions(-) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 7b26b570..cccec7c7 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -66,5 +66,5 @@ jobs: - verifyGhoDiscountRateStrategy.sh equivalenceOfWadMulCVLAndWadMulSol maxDiscountForHighDiscountTokenBalance zeroDiscountForSmallDiscountTokenBalance partialDiscountForIntermediateTokenBalance limitOnDiscountRate - verifyFlashMinter.sh balanceOfFlashMinterGrows integrityOfTreasurySet integrityOfFeeSet availableLiquidityDoesntChange integrityOfDistributeFeesToTreasury feeSimulationEqualsActualFee - 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 - - verifyGhoVariableDebtToken.sh user_index_after_mint accumulated_interest_increase_after_mint + - verifyGhoVariableDebtToken.sh user_index_after_mint accumulated_interest_increase_after_mint user_index_ge_one_ray - verifyGhoVariableDebtToken_intenal.sh \ No newline at end of file diff --git a/certora/specs/ghoVariableDebtToken.spec b/certora/specs/ghoVariableDebtToken.spec index 8f44f423..0a9484d2 100644 --- a/certora/specs/ghoVariableDebtToken.spec +++ b/certora/specs/ghoVariableDebtToken.spec @@ -155,6 +155,8 @@ rule accumulated_interest_increase_after_mint uint256 amount; uint256 index; + requireInvariant user_index_ge_one_ray(e, onBehalfOf); + uint256 user_index_before = getUserCurrentIndex(onBehalfOf); uint256 balance_before = balanceOf(e, onBehalfOf); uint256 discount_before = getUserDiscountRate(onBehalfOf); @@ -163,13 +165,27 @@ rule accumulated_interest_increase_after_mint uint256 accumulated_interest_after = getUserAccumulatedDebtInterest(onBehalfOf); - assert ray() <= user_index_before - && to_mathint(user_index_before + ray()) < to_mathint(index) + assert to_mathint(user_index_before + ray()) < to_mathint(index) && balance_before > 0 && discount_before < 5000 => 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 **/ @@ -529,7 +545,7 @@ rule integrityOfBurn_userIsolation() { /** * @title proves that the discount rate is calculated correctly when calling updateDiscountDistribution **/ -// TODO: enable when timeout is resolved +// TODO: enable when timeout is resolved and add to CI // rule integrityOfUpdateDiscountDistribution_discountRate() { // address sender; // address recipient; @@ -685,3 +701,17 @@ rule burnAllDebtReturnsZeroDebt(address user) { uint256 variableDebt_ = balanceOf(e, user); assert(variableDebt_ == 0); } + + +// setup self check - reachability of currentContract external functions +// todo: debug unreachable functions and add to CI: +// transfer(), transferFrom(), approve(), allowance(), increaseAllowance(), decreaseAllowance(). +rule method_reachability { + env e; + calldataarg arg; + method f; + + f(e, arg); + satisfy true; +} + From 4ced4c83a93e5e5fe9a15698f358651452d04a02 Mon Sep 17 00:00:00 2001 From: gadicer Date: Tue, 21 Nov 2023 11:52:11 +0200 Subject: [PATCH 5/6] add nonzeroNewDiscountToken --- .github/workflows/certora.yml | 2 +- certora/specs/ghoVariableDebtToken.spec | 26 +++++++++++++------------ 2 files changed, 15 insertions(+), 13 deletions(-) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index cccec7c7..83da931c 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -66,5 +66,5 @@ jobs: - verifyGhoDiscountRateStrategy.sh equivalenceOfWadMulCVLAndWadMulSol maxDiscountForHighDiscountTokenBalance zeroDiscountForSmallDiscountTokenBalance partialDiscountForIntermediateTokenBalance limitOnDiscountRate - verifyFlashMinter.sh balanceOfFlashMinterGrows integrityOfTreasurySet integrityOfFeeSet availableLiquidityDoesntChange integrityOfDistributeFeesToTreasury feeSimulationEqualsActualFee - 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 - - verifyGhoVariableDebtToken.sh user_index_after_mint accumulated_interest_increase_after_mint user_index_ge_one_ray + - verifyGhoVariableDebtToken.sh user_index_after_mint accumulated_interest_increase_after_mint user_index_ge_one_ray nonzeroNewDiscountToken - verifyGhoVariableDebtToken_intenal.sh \ No newline at end of file diff --git a/certora/specs/ghoVariableDebtToken.spec b/certora/specs/ghoVariableDebtToken.spec index 0a9484d2..f827aeca 100644 --- a/certora/specs/ghoVariableDebtToken.spec +++ b/certora/specs/ghoVariableDebtToken.spec @@ -47,6 +47,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 *; @@ -130,6 +131,19 @@ invariant discountCantExceed100Percent(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 { @@ -703,15 +717,3 @@ rule burnAllDebtReturnsZeroDebt(address user) { } -// setup self check - reachability of currentContract external functions -// todo: debug unreachable functions and add to CI: -// transfer(), transferFrom(), approve(), allowance(), increaseAllowance(), decreaseAllowance(). -rule method_reachability { - env e; - calldataarg arg; - method f; - - f(e, arg); - satisfy true; -} - From d501279ff7a48fe46fc33aa2cb1ced12a8b0e476 Mon Sep 17 00:00:00 2001 From: gadicer Date: Tue, 21 Nov 2023 18:01:14 +0200 Subject: [PATCH 6/6] inherit harness --- .../ghoVariableDebtTokenHarnessInternal.sol | 26 +++++++++ .../ghoVariableDebtTokenHarness_internal.sol | 57 ------------------- .../verifyGhoVariableDebtTokenInternal.sh | 11 ++++ .../verifyGhoVariableDebtToken_internal.sh | 17 ------ ...spec => ghoVariableDebtTokenInternal.spec} | 0 5 files changed, 37 insertions(+), 74 deletions(-) create mode 100644 certora/harness/ghoVariableDebtTokenHarnessInternal.sol delete mode 100644 certora/harness/ghoVariableDebtTokenHarness_internal.sol create mode 100644 certora/scripts/verifyGhoVariableDebtTokenInternal.sh delete mode 100644 certora/scripts/verifyGhoVariableDebtToken_internal.sh rename certora/specs/{ghoVariableDebtToken_internal.spec => ghoVariableDebtTokenInternal.spec} (100%) 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/harness/ghoVariableDebtTokenHarness_internal.sol b/certora/harness/ghoVariableDebtTokenHarness_internal.sol deleted file mode 100644 index 80f1f436..00000000 --- a/certora/harness/ghoVariableDebtTokenHarness_internal.sol +++ /dev/null @@ -1,57 +0,0 @@ -pragma solidity 0.8.10; - -import {GhoVariableDebtToken} from '../munged/contracts/facilitators/aave/tokens/GhoVariableDebtToken.sol'; -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 { - using WadRayMath for uint256; - - constructor(IPool pool) public GhoVariableDebtToken(pool) { - //nop - } - - function getUserCurrentIndex(address user) external view returns (uint256) { - return _userState[user].additionalData; - } - - function getUserDiscountRate(address user) external view returns (uint256) { - return _ghoUserState[user].discountPercent; - } - - function getUserAccumulatedDebtInterest(address user) external view returns (uint256) { - return _ghoUserState[user].accumulatedDebtInterest; - } - - function scaledBalanceOfToBalanceOf(uint256 bal) public view returns (uint256) { - return bal.rayMul(POOL.getReserveNormalizedVariableDebt(_underlyingAsset)); - } - - function getBalanceOfDiscountToken(address user) external returns (uint256) { - return _discountToken.balanceOf(user); - } - - function rayMul(uint256 x, uint256 y) external view returns (uint256) { - return x.rayMul(y); - } - - function rayDiv(uint256 x, uint256 y) external view returns (uint256) { - return x.rayDiv(y); - } - - - - 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/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/scripts/verifyGhoVariableDebtToken_internal.sh b/certora/scripts/verifyGhoVariableDebtToken_internal.sh deleted file mode 100644 index 3f458272..00000000 --- a/certora/scripts/verifyGhoVariableDebtToken_internal.sh +++ /dev/null @@ -1,17 +0,0 @@ - -certoraRun certora/harness/ghoVariableDebtTokenHarness_internal.sol:GhoVariableDebtTokenHarness \ - certora/harness/DummyPool.sol \ - certora/harness/DummyERC20WithTimedBalanceOf.sol \ - certora/munged/contracts/facilitators/aave/interestStrategy/GhoDiscountRateStrategy.sol \ - certora/harness/DummyERC20A.sol certora/harness/DummyERC20B.sol \ - --verify GhoVariableDebtTokenHarness:certora/specs/ghoVariableDebtToken_internal.spec \ - --link GhoVariableDebtTokenHarness:_discountRateStrategy=GhoDiscountRateStrategy \ - --link GhoVariableDebtTokenHarness:_discountToken=DummyERC20WithTimedBalanceOf \ - --link GhoVariableDebtTokenHarness:POOL=DummyPool \ - --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_internal.spec b/certora/specs/ghoVariableDebtTokenInternal.spec similarity index 100% rename from certora/specs/ghoVariableDebtToken_internal.spec rename to certora/specs/ghoVariableDebtTokenInternal.spec