Merge pull request #5 from Certora/check_variable_debt_token

Check variable debt token

.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

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
+  );
+  }
+}

certora/scripts/verifyGhoDiscountRateStrategy.sh

@@ -1,21 +1,21 @@
-if (($# > 0))
-then
+#if (($# > 0))
+#then
 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 \
-    --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

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"
+

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
 **/

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;
+}
+
+