fix: Add update on GHO integration with Aave Pool (aave#366)

* fix: Update variable debt gho with full repayment * certora: Update scripts for Certora Formal Verification
Certora · Sep 11, 2023 · b2db754 · b2db754
1 parent 0d9d26d
commit b2db754
Show file tree

Hide file tree

Showing 19 changed files with 418 additions and 394 deletions.
diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
@@ -34,7 +34,7 @@ jobs:
         with: { java-version: '11', java-package: jre }
 
       - name: Install certora cli
-        run: pip install certora-cli==3.6.8.post3
+        run: pip install certora-cli
 
       - name: Install solc
         run: |
@@ -65,4 +65,4 @@ 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 integrityOfBurn_fixedIndex burnZeroDoesntChangeBalance integrityOfBurn_fullRepay_concrete integrityOfBurn_userIsolation integrityOfUpdateDiscountDistribution_updateIndex integrityOfUpdateDiscountDistribution_userIsolation integrityOfRebalanceUserDiscountPercent_updateDiscountRate integrityOfRebalanceUserDiscountPercent_updateIndex integrityOfRebalanceUserDiscountPercent_userIsolation integrityOfBalanceOf_fullDiscount integrityOfBalanceOf_noDiscount integrityOfBalanceOf_zeroScaledBalance
+          - 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
diff --git a/certora/.gitignore b/certora/.gitignore
diff --git a/certora/scripts/verifyFlashMinter.sh b/certora/scripts/verifyFlashMinter.sh
@@ -11,8 +11,7 @@ certoraRun certora/munged/contracts/facilitators/flashMinter/GhoFlashMinter.sol:
            MockFlashBorrower:AGho=GhoAToken \
     --solc solc8.10 \
     --optimistic_loop \
-    --cloud \
-    --settings -contractRecursionLimit=1 \
+    --prover_args "-contractRecursionLimit 1" \
     --rules "${@}"
     --msg "flashMinter check, rules ${@}"
 else
@@ -27,8 +26,7 @@ certoraRun certora/munged/contracts/facilitators/flashMinter/GhoFlashMinter.sol:
            MockFlashBorrower:AGho=GhoAToken \
     --solc solc8.10 \
     --optimistic_loop \
-    --cloud \
-    --settings -contractRecursionLimit=1 \
+    --prover_args "-contractRecursionLimit 1" \
     --msg "flashMinter check, all rules"
 fi
 

diff --git a/certora/scripts/verifyGhoAToken.sh b/certora/scripts/verifyGhoAToken.sh
@@ -13,7 +13,6 @@ certoraRun certora/munged/contracts/facilitators/aave/tokens/GhoAToken.sol \
     --link GhoVariableDebtToken:_ghoAToken=GhoAToken \
     --solc solc8.10 \
     --optimistic_loop \
-    --cloud \
     --rules "${@}" \
     --msg "GhoAToken, rules ${@}"
 else
@@ -28,6 +27,6 @@ certoraRun certora/munged/contracts/facilitators/aave/tokens/GhoAToken.sol \
     --link GhoVariableDebtToken:_ghoAToken=GhoAToken \
     --solc solc8.10 \
     --optimistic_loop \
-    --cloud \
+    --send_only \
     --msg "GhoAToken, all rules"
 fi
diff --git a/certora/scripts/verifyGhoDiscountRateStrategy.sh b/certora/scripts/verifyGhoDiscountRateStrategy.sh
@@ -5,8 +5,8 @@ certoraRun certora/harness/GhoDiscountRateStrategyHarness.sol:GhoDiscountRateStr
     --solc solc8.10 \
     --loop_iter 2 \
     --optimistic_loop \
-    --settings -t=500,-mediumTimeout=20,-depth=10 \
-    --cloud \
+    --prover_args "-mediumTimeout 20 -depth 10" \
+    --smt_timeout 500 \
     --rules "${@}" \
     --msg "GhoDiscountRateStrategy, rules ${@}."
 else
@@ -15,7 +15,7 @@ certoraRun certora/harness/GhoDiscountRateStrategyHarness.sol:GhoDiscountRateStr
     --solc solc8.10 \
     --loop_iter 2 \
     --optimistic_loop \
-    --settings -t=500,-mediumTimeout=20,-depth=10 \
-    --cloud \
+    --prover_args "-mediumTimeout 20 -depth 10" \
+    --smt_timeout 500 \
     --msg "GhoDiscountRateStrategy, all rules."
 fi
diff --git a/certora/scripts/verifyGhoToken.sh b/certora/scripts/verifyGhoToken.sh
@@ -7,15 +7,13 @@ certoraRun certora/harness/GhoTokenHarness.sol:GhoTokenHarness certora/munged/co
     --solc solc8.10 \
     --loop_iter 3 \
     --optimistic_loop \
-    --cloud \
     --rules "${@}" \
-    --msg "GhoToken, rules ${@}"
+    --msg "GhoToken workaround for CERT-1060, rules ${@}"
 else
 certoraRun certora/harness/GhoTokenHarness.sol:GhoTokenHarness certora/munged/contracts/gho/GhoToken.sol \
     --verify GhoTokenHarness:certora/specs/ghoToken.spec \
     --solc solc8.10 \
     --loop_iter 3 \
     --optimistic_loop \
-    --cloud \
-    --msg "GhoToken, all rules."
+    --msg "GhoToken, all rules. workaround for CERT-1060"
 fi
diff --git a/certora/scripts/verifyGhoVariableDebtToken.sh b/certora/scripts/verifyGhoVariableDebtToken.sh
@@ -14,10 +14,11 @@ certoraRun certora/harness/ghoVariableDebtTokenHarness.sol:GhoVariableDebtTokenH
     --loop_iter 2 \
     --solc solc8.10 \
     --optimistic_loop \
-    --settings -t=900,-mediumTimeout=30,-depth=15 \
-    --cloud \
     --rules "${@}" \
-    --msg "GhoVariableDebtToken, rules ${@}."
+    --smt_timeout 900 \
+    --prover_args "-mediumTimeout 30 -depth 15" \
+    --msg "GhoVariableDebtToken"
+
 else
 certoraRun certora/harness/ghoVariableDebtTokenHarness.sol:GhoVariableDebtTokenHarness \
     certora/harness/DummyPool.sol \
@@ -31,8 +32,8 @@ certoraRun certora/harness/ghoVariableDebtTokenHarness.sol:GhoVariableDebtTokenH
     --loop_iter 2 \
     --solc solc8.10 \
     --optimistic_loop \
-    --settings -t=900,-mediumTimeout=30,-depth=15 \
-    --cloud \
-    --msg "GhoVariableDebtToken, all rules."
-fi
+    --smt_timeout 900 \
+    --prover_args "-mediumTimeout 30 -depth 15" \
+    --msg "GhoVariableDebtToken"
 
+fi
diff --git a/certora/specs/VariableDebtToken.spec b/certora/specs/VariableDebtToken.spec
@@ -2,35 +2,35 @@ methods {
 	// summarization for elimination the raymul operation in balance of and totalSupply.
 	//getReserveNormalizedVariableDebt(address asset) returns (uint256) => indexAtTimestamp(e.block.timestamp)
 	//setAdditionalData(address user, uint128 data) envfree
-    handleAction(address, uint256, uint256) => NONDET
-	scaledBalanceOfToBalanceOf(uint256) returns (uint256) envfree
+    function _.handleAction(address, uint256, uint256) external => NONDET;
+	function scaledBalanceOfToBalanceOf(uint256) external returns (uint256) envfree;
     //balanceOf(address) returns (uint256) envfree
 }
 
-definition ray() returns uint = 1000000000000000000000000000; // 10^27
-definition wad() returns uint = 1000000000000000000; // 10^18
-definition bound(uint256 index) returns uint = ((index / ray()) + 1 ) / 2;
+definition ray() returns uint256 = 1000000000000000000000000000; // 10^27
+definition wad() returns uint256 = 1000000000000000000; // 10^18
+definition bound(uint256 index) returns mathint = ((index / ray()) + 1 ) / 2;
 // summerization for scaledBlanaceOf -> regularBalanceOf + 0.5 (canceling the rayMul)
 // ghost gRNVB() returns uint256 {
 // 	axiom gRNVB() == 7 * ray();
 // }
 /*
 Due to rayDiv and RayMul Rounding (+ 0.5) - blance could increase by (gRNI() / Ray() + 1) / 2.
 */
-definition bounded_error_eq(uint x, uint y, uint scale, uint256 index) returns bool = x <= y + (bound(index) * scale) && x + (bound(index) * scale) >= y;
+definition bounded_error_eq(uint x, uint y, uint scale, uint256 index) returns bool = to_mathint(x) <= y + (bound(index) * scale) && x + (bound(index) * scale) >= to_mathint(y);
 
 
 
 definition disAllowedFunctions(method f) returns bool = 
-            f.selector == transfer(address, uint256).selector ||
-            f.selector == allowance(address, address).selector ||
-            f.selector == approve(address, uint256).selector ||
-            f.selector == transferFrom(address, address, uint256).selector ||
-            f.selector == increaseAllowance(address, uint256).selector ||
-            f.selector == decreaseAllowance(address, uint256).selector;
+            f.selector == sig:transfer(address, uint256).selector ||
+            f.selector == sig:allowance(address, address).selector ||
+            f.selector == sig:approve(address, uint256).selector ||
+            f.selector == sig:transferFrom(address, address, uint256).selector ||
+            f.selector == sig:increaseAllowance(address, uint256).selector ||
+            f.selector == sig:decreaseAllowance(address, uint256).selector;
 
 
-ghost sumAllBalance() returns uint256 {
+ghost sumAllBalance() returns mathint {
     init_state axiom sumAllBalance() == 0;
 }
 
@@ -62,8 +62,8 @@ rule whoChangeTotalSupply(method f)
     uint256 newTotalSupply = totalSupply();
     assert oldTotalSupply != newTotalSupply => 
            (e.msg.sender == POOL(e) && 
-           (f.selector == burn(address, uint256, uint256).selector || 
-            f.selector == mint(address, address, uint256, uint256).selector));
+           (f.selector == sig:burn(address, uint256, uint256).selector || 
+            f.selector == sig:mint(address, address, uint256, uint256).selector));
 }
 
 /*
@@ -121,7 +121,7 @@ rule nonceChangePermits(method f)
     calldataarg args;
     f(e, args);
     uint256 newNonce = nonces(e, user);
-    assert oldNonce != newNonce => f.selector == delegationWithSig(address, address, uint256, uint256, uint8, bytes32, bytes32).selector;
+    assert oldNonce != newNonce => f.selector == sig:delegationWithSig(address, address, uint256, uint256, uint8, bytes32, bytes32).selector;
 }
 
 // minting and then buring Variable Debt Token should have no effect on the users balance
@@ -351,7 +351,7 @@ rule integrityMint_exact_should_fail(address a, uint256 x) {
 rule burnZeroDoesntChangeBalance(address u, uint256 index) {
 	env e;
 	uint256 balanceBefore = balanceOf(e, u);
-	invoke burn(e, u, 0, index);
+	burn@withrevert(e, u, 0, index);
 	uint256 balanceAfter = balanceOf(e, u);
 	assert balanceBefore == balanceAfter;
 }

diff --git a/certora/specs/erc20.spec b/certora/specs/erc20.spec
@@ -1,12 +1,12 @@
 // erc20 methods
 methods {
-    name()                                returns (string)  => DISPATCHER(true)
-    symbol()                              returns (string)  => DISPATCHER(true)
-    decimals()                            returns (string)  => DISPATCHER(true)
-    totalSupply()                         returns (uint256) => DISPATCHER(true)
-    balanceOf(address)                    returns (uint256) => DISPATCHER(true)
-    allowance(address,address)            returns (uint)    => DISPATCHER(true)
-    approve(address,uint256)              returns (bool)    => DISPATCHER(true)
-    transfer(address,uint256)             returns (bool)    => DISPATCHER(true)
-    transferFrom(address,address,uint256) returns (bool)    => DISPATCHER(true)
+    function _.name() external                                 => DISPATCHER(true);
+    function _.symbol() external                              => DISPATCHER(true);
+    function _.decimals() external                            => DISPATCHER(true);
+    function _.totalSupply() external                         => DISPATCHER(true);
+    function _.balanceOf(address) external                    => DISPATCHER(true);
+    function _.allowance(address,address) external            => DISPATCHER(true);
+    function _.approve(address,uint256) external              => DISPATCHER(true);
+    function _.transfer(address,uint256) external             => DISPATCHER(true);
+    function _.transferFrom(address,address,uint256) external => DISPATCHER(true);
 }
diff --git a/certora/specs/flashMinter.spec b/certora/specs/flashMinter.spec
@@ -1,28 +1,28 @@
-using GhoToken as gho
-using GhoAToken as atoken
-using MockFlashBorrower as flashBorrower
+using GhoToken as gho;
+using GhoAToken as atoken;
+using MockFlashBorrower as flashBorrower;
 
 methods{
-    isPoolAdmin(address user) returns (bool) => retreivePoolAdminFromGhost(user)
-    isFlashBorrower(address user) returns (bool) => retreiveFlashBorrowerFromGhost(user)
-    onFlashLoan(address, address, uint256, uint256, bytes) returns (bytes32) => DISPATCHER(true)
-    getACLManager() returns (address) => NONDET
+    function _.isPoolAdmin(address user) external => retreivePoolAdminFromGhost(user) expect bool ALL;
+    function _.isFlashBorrower(address user) external => retreiveFlashBorrowerFromGhost(user) expect bool ALL;
+    function _.onFlashLoan(address, address, uint256, uint256, bytes) external => DISPATCHER(true);
+    function _.getACLManager() external => NONDET;
 
     // FlashBorrower
-    flashBorrower.action() returns (uint8) envfree
-    flashBorrower._transferTo() returns (address) envfree
-    gho.allowance(address, address) returns (uint256) envfree
-    burn(uint256) => DISPATCHER(true)
-    mint(address, uint256) => DISPATCHER(true)
-    transfer(address, uint256) returns (bool) => DISPATCHER(true)
-    balanceOf(address) returns (uint256) => DISPATCHER(true)
+    function flashBorrower.action() external returns (MockFlashBorrower.Action) envfree;
+    function flashBorrower._transferTo() external returns (address) envfree;
+    function gho.allowance(address, address) external returns (uint256) envfree;
+    function _.burn(uint256)  external=> DISPATCHER(true);
+    function _.mint(address, uint256)  external=> DISPATCHER(true);
+    function _.transfer(address, uint256) external => DISPATCHER(true);
+    function _.balanceOf(address) external => DISPATCHER(true);
 
-    decreaseBalanceFromInterest(address, uint256) => NONDET
-    getBalanceFromInterest(address) => NONDET
-    gho.totalSupply() returns (uint256) envfree
-    gho.balanceOf(address) returns (uint256) envfree
+    function _.decreaseBalanceFromInterest(address, uint256) external => NONDET;
+    function _.getBalanceFromInterest(address) external => NONDET;
+    function gho.totalSupply() external returns (uint256) envfree;
+    function gho.balanceOf(address) external returns (uint256) envfree;
 
-    atoken.getGhoTreasury() returns (address) envfree
+    function atoken.getGhoTreasury() external returns (address) envfree;
 }
 
 // keeps track of users with pool admin permissions in order to return a consistent value per user
@@ -48,20 +48,21 @@ function flashLoanReqs(env e){
 
 // an assumption that demands the sum of balances of 3 given users is no more than the total supply
 function ghoBalanceOfTwoUsersLETotalSupply(address user1, address user2, address user3){
-    require gho.balanceOf(user1) + gho.balanceOf(user2) + gho.balanceOf(user3) <= gho.totalSupply();
+    require gho.balanceOf(user1) + gho.balanceOf(user2) + gho.balanceOf(user3) <= to_mathint(gho.totalSupply());
 }
 
 /**
  * @title The GHO balance of the flash minter should grow when calling any function, excluding distributeFees
  */
 rule balanceOfFlashMinterGrows(method f, env e, calldataarg args) 
-    filtered { f -> f.selector != distributeFeesToTreasury().selector }{
+    filtered { f -> f.selector != sig:distributeFeesToTreasury().selector }{
 
     // No overflow of gho is possible
     ghoBalanceOfTwoUsersLETotalSupply(currentContract, e.msg.sender, atoken);
     flashLoanReqs(e);
     // excluding calls to distribute fees
-    require flashBorrower.action() != 1; 
+    mathint action = assert_uint256(flashBorrower.action());
+    require action != 1; 
 
     uint256 _facilitatorBalance = gho.balanceOf(currentContract);
 
@@ -133,23 +134,33 @@ rule integrityOfDistributeFeesToTreasury(){
  */
 rule feeSimulationEqualsActualFee(address receiver, address token, uint256 amount, bytes data){
     env e;
-    uint256 feeSimulationResult = flashFee(e, token, amount);
+    mathint feeSimulationResult = flashFee(e, token, amount);
     uint256 _facilitatorBalance = gho.balanceOf(currentContract);
 
     flashLoanReqs(e);
     require atoken.getGhoTreasury() != currentContract;
     // No overflow of gho is possible
     ghoBalanceOfTwoUsersLETotalSupply(currentContract, e.msg.sender, atoken);
     // Excluding call to distributeFeesToTreasury & calling another flashloan (which will generate another fee in recursion)
-    require flashBorrower.action() != 1 && flashBorrower.action() != 0;
+    mathint borrower_action = assert_uint256(flashBorrower.action());
+    require borrower_action != 1 && borrower_action != 0;
     // Because we calculate the actual fee by balance difference of the minter, we assume no extra money is being sent to the minter.
     require flashBorrower._transferTo() != currentContract;
 
     flashLoan(e, receiver, token, amount, data);
 
     uint256 facilitatorBalance_ = gho.balanceOf(currentContract);
 
-    uint256 actualFee = facilitatorBalance_ - _facilitatorBalance;
+    mathint actualFee = facilitatorBalance_ - _facilitatorBalance;
 
     assert feeSimulationResult == actualFee;
 }
+
+
+rule sanity {
+  env e;
+  calldataarg arg;
+  method f;
+  f(e, arg);
+  satisfy true;
+}