merged other mutatnts

.github/workflows/certora.yml

@@ -12,8 +12,7 @@ on:
 
 jobs:
   verify:
-    runs-on:
-      group: larger
+    runs-on: ubuntu-latest
 
     steps:
       - uses: actions/checkout@v2
@@ -65,6 +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 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 nonzeroNewDiscountToken
-          - verifyGhoVariableDebtToken_intenal.sh 
+          - 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
+          - verifyGhoVariableDebtToken_summarized.sh sendersDiscountPercentCannotIncrease
+          - verifyGhoVariableDebtTokenIntenal.sh 
+

certora/scripts/verifyGhoVariableDebtToken.sh

@@ -14,7 +14,7 @@ certoraRun certora/harness/ghoVariableDebtTokenHarness.sol:GhoVariableDebtTokenH
     --loop_iter 2 \
     --solc solc8.10 \
     --optimistic_loop \
-    --rules "${@}" \
+    --rule "${@}" \
     --smt_timeout 900 \
     --prover_args "-mediumTimeout 30 -depth 15" \
     --msg "GhoVariableDebtToken"

certora/scripts/verifyGhoVariableDebtToken_specialBranch.sh

@@ -0,0 +1,37 @@
+#!/bin/sh
+
+if (($# > 0))
+then
+certoraRun certora/harness/ghoVariableDebtTokenHarness.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.spec \
+    --link GhoVariableDebtTokenHarness:_discountRateStrategy=GhoDiscountRateStrategy \
+    --link GhoVariableDebtTokenHarness:_discountToken=DummyERC20WithTimedBalanceOf \
+    --link GhoVariableDebtTokenHarness:POOL=DummyPool \
+    --loop_iter 2 \
+    --solc solc8.10 \
+    --optimistic_loop \
+    --rule "${@}" \
+    --prover_args '-depth 0 -adaptiveSolverConfig false -smt_nonLinearArithmetic true' --server staging --prover_version shelly/z3-4-12-3-build \
+    --msg "GhoVariableDebtToken"
+
+else
+certoraRun certora/harness/ghoVariableDebtTokenHarness.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.spec \
+    --link GhoVariableDebtTokenHarness:_discountRateStrategy=GhoDiscountRateStrategy \
+    --link GhoVariableDebtTokenHarness:_discountToken=DummyERC20WithTimedBalanceOf \
+    --link GhoVariableDebtTokenHarness:POOL=DummyPool \
+    --loop_iter 2 \
+    --solc solc8.10 \
+    --optimistic_loop \
+    --prover_args '-depth 0 -adaptiveSolverConfig false -smt_nonLinearArithmetic true' --server staging --prover_version shelly/z3-4-12-3-build \
+    --msg "GhoVariableDebtToken"
+
+fi

certora/scripts/verifyGhoVariableDebtToken_summarized.sh

@@ -0,0 +1,37 @@
+#!/bin/sh
+
+if (($# > 0))
+then
+certoraRun certora/harness/ghoVariableDebtTokenHarness.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_summarized.spec \
+    --link GhoVariableDebtTokenHarness:_discountRateStrategy=GhoDiscountRateStrategy \
+    --link GhoVariableDebtTokenHarness:_discountToken=DummyERC20WithTimedBalanceOf \
+    --link GhoVariableDebtTokenHarness:POOL=DummyPool \
+    --loop_iter 2 \
+    --solc solc8.10 \
+    --optimistic_loop \
+    --rule "${@}" \
+    --msg "GhoVariableDebtToken"
+
+else
+certoraRun certora/harness/ghoVariableDebtTokenHarness.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_summarized.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"
+
+fi

certora/specs/ghoVariableDebtToken.spec

@@ -6,6 +6,7 @@ import "summarizations.spec";
 using GhoDiscountRateStrategy as discStrategy;
 
 methods{
+
 	/********************;
 	*	WadRayMath.sol	*;
 	*********************/
@@ -60,6 +61,11 @@ methods{
 	function getBalanceFromInterest(address) external returns (uint256) envfree;
 	function rebalanceUserDiscountPercent(address) external;
 	function updateDiscountDistribution(address ,address ,uint256 ,uint256 ,uint256) external;
+
+    /********************************;
+	*	GhoDiscountRateStrategy.sol	*;
+	*********************************/
+    function discStrategy.DISCOUNT_RATE() external returns (uint256) envfree;
 }
 
 /**
@@ -129,6 +135,17 @@ invariant discountCantExceed100Percent(address user)
 			require(indexAtTimestamp(e.block.timestamp) >= ray());
 		}
 	}
+
+/**
+* @title at any point in time, the user's discount rate isn't larger than DISCOUNT_RATE
+**/
+invariant discountCantExceedDiscountRate(address user)
+	getUserDiscountRate(user) <= discStrategy.DISCOUNT_RATE()
+	{
+		preserved updateDiscountDistribution(address sender,address recipient,uint256 senderDiscountTokenBalance,uint256 recipientDiscountTokenBalance,uint256 amount) with (env e) {
+			require(indexAtTimestamp(e.block.timestamp) >= ray());
+		}
+	}
 
 
 
@@ -556,10 +573,9 @@ rule integrityOfBurn_userIsolation() {
 * Integrity of updateDiscountDistribution
 ***************************************************************/
 
-/**
-* @title proves that the discount rate is calculated correctly when calling updateDiscountDistribution
-**/
-// TODO: enable when timeout is resolved and add to CI
+// /**
+// * @title proves that the discount rate is calculated correctly when calling updateDiscountDistribution
+// **/
 // rule integrityOfUpdateDiscountDistribution_discountRate() {
 // 	address sender;
 //     address recipient;
@@ -581,7 +597,6 @@ rule integrityOfBurn_userIsolation() {
 // 	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);
 
@@ -592,6 +607,33 @@ rule integrityOfBurn_userIsolation() {
 // 	assert(discStrategy.calculateDiscountRate(recipientBalance, recipientDiscountTokenBalanceAfter) == getUserDiscountRate(recipient));
 // }
 
+rule sendersDiscountPercentCannotIncrease(){
+	env e1;
+    address sender; address recipient; uint256 amount;
+
+    uint256 _senderStkBalance = getBalanceOfDiscountToken(e1, sender);
+    uint256 _recipientStkBalance = getBalanceOfDiscountToken(e1, recipient);
+    uint256 indE1 = indexAtTimestamp(e1.block.timestamp);
+    // require(indE1 >= ray()); // this is already enforced in the funciton's body
+    require getUserCurrentIndex(sender) == indE1;
+    uint256 _sender_debt = balanceOf(e1, sender);
+    uint256 discount_sender = discStrategy.calculateDiscountRate(_sender_debt, _senderStkBalance);
+    require(discount_sender == getDiscountPercent(e1, sender));
+    require discount_sender != 0; // this can be violated due to discontiuity of calculateDiscountRate
+
+    env e2;
+	require e1.block.timestamp <= e2.block.timestamp;
+    uint256 indE2 = indexAtTimestamp(e2.block.timestamp);
+	require(indE2 >= indE1);
+    require _senderStkBalance == getBalanceOfDiscountToken(e2, sender);
+    require _recipientStkBalance == getBalanceOfDiscountToken(e2, recipient);
+
+    updateDiscountDistribution(e2, sender, recipient, _senderStkBalance, _recipientStkBalance, amount);
+
+    uint256 discountPercent_ = getDiscountPercent(e2, sender);
+    assert (discountPercent_ <= discount_sender);
+}
+
 /**
 * @title proves the after calling updateDiscountDistribution, the user's state is updated with the recent index value
 **/
@@ -602,13 +644,20 @@ rule integrityOfUpdateDiscountDistribution_updateIndex() {
     uint256 recipientDiscountTokenBalance;
 	env e;
 	uint256 amount;
+    uint256 _senderInd = getUserCurrentIndex(sender);
+    uint256 _recipientInd = getUserCurrentIndex(recipient);
 	uint256 index = indexAtTimestamp(e.block.timestamp);
 	updateDiscountDistribution(e, sender, recipient, senderDiscountTokenBalance, recipientDiscountTokenBalance, amount);
-	assert(scaledBalanceOf(sender) > 0 => getUserCurrentIndex(sender) == index);
-	assert(scaledBalanceOf(recipient) > 0 => getUserCurrentIndex(recipient) == index);
+	if (sender != recipient){
+        assert(scaledBalanceOf(sender) > 0 => getUserCurrentIndex(sender) == index);
+	    assert(scaledBalanceOf(recipient) > 0 => getUserCurrentIndex(recipient) == index);
+    }
+    else{
+        assert(getUserCurrentIndex(sender) == _senderInd);
+        assert(getUserCurrentIndex(recipient) == _recipientInd); // this is redundant, this is here for future changes in the code/rule
+    }
 }
 
-
 /**
 * @title proves that updateDiscountDistribution can't effect other user's scaled balance
 **/
@@ -708,6 +757,9 @@ rule integrityOfBalanceOf_zeroScaledBalance() {
 	assert(balanceOf(e, user) == 0);
 }
 
+/**
+* @title burning amount of current debt nullifies the debt position
+**/
 rule burnAllDebtReturnsZeroDebt(address user) {
     env e;
 	uint256 _variableDebt = balanceOf(e, user);
@@ -716,4 +768,11 @@ rule burnAllDebtReturnsZeroDebt(address user) {
     assert(variableDebt_ == 0);
 }
 
-
+/**
+* @title 
+**/
+rule integrityOfUpdateDiscountRateStrategy(address newDiscountRateStrategy) {
+	env e;
+    updateDiscountRateStrategy(e, newDiscountRateStrategy );
+    assert(getDiscountRateStrategy(e) == newDiscountRateStrategy);
+}

certora/specs/ghoVariableDebtToken_summarized.spec

@@ -0,0 +1,42 @@
+import "ghoVariableDebtToken.spec";
+
+methods{
+	function GhoVariableDebtToken._accrueDebtOnAction(address user, uint256, uint256, uint256) internal returns (uint256, uint256) => flipAccrueCalled(user);
+	function GhoVariableDebtToken._refreshDiscountPercent(address user, uint256, uint256, uint256) internal => flipRefreshCalled(user);
+}
+
+ghost mapping(address => mathint) accrue_called_counter;
+ghost mapping(address => mathint) refresh_called_counter;
+
+function flipAccrueCalled(address user) returns (uint256, uint256) {
+    accrue_called_counter[user] = accrue_called_counter[user] + 1;
+    return (0, 0);
+}
+
+function flipRefreshCalled(address user) {
+    refresh_called_counter[user] = refresh_called_counter[user] + 1;
+}
+
+// accrue is always called before refresh
+rule accrueAlwaysCaleldBeforeRefresh(env e, method f) {
+    address user1;
+    require accrue_called_counter[user1] == refresh_called_counter[user1];
+
+    calldataarg args;
+    f(e, args);
+
+    assert refresh_called_counter[user1] == accrue_called_counter[user1], "Remember, with great power comes great responsibility.";
+}
+
+// accrue is always called before refresh example
+// should pass only on updateDiscountDistribution
+rule accrueAlwaysCaleldBeforeRefresh_witness(env e, method f) {
+    address user1;
+    mathint counter = accrue_called_counter[user1];
+    require accrue_called_counter[user1] == refresh_called_counter[user1];
+
+    calldataarg args;
+    f(e, args);
+
+    satisfy(refresh_called_counter[user1] == counter + 2);
+}