Various fixes. New rules requested from PR

euler-xyz · Aug 12, 2024 · 4f06340 · 4f06340
1 parent b04e9da
commit 4f06340
Show file tree

Hide file tree

Showing 5 changed files with 114 additions and 81 deletions.
diff --git a/certora/harness/modules/LiquidationHarness.sol b/certora/harness/modules/LiquidationHarness.sol
@@ -16,6 +16,13 @@ contract LiquidationHarness is AbstractBaseHarness, Liquidation {
         return calculateLiquidity(loadVault(), account, getCollaterals(account), true);
     }
 
+    function calculateLiquidityLiquidation(
+        address account
+    ) public view returns (uint256 collateralValue, uint256 liabilityValue) {
+        return calculateLiquidity(loadVault(), account, getCollaterals(account), false);
+    }
+
+
     function calculateLiquidationExt(
         VaultCache memory vaultCache,
         address liquidator,

diff --git a/certora/scripts/runHealthStatusAllModules.py b/certora/scripts/runHealthStatusAllModules.py
@@ -7,69 +7,68 @@
                     help='a message for all the jobs')
 args = parser.parse_args()
 
-hs_confs = [
-    "BalanceForwarder",
-    "Borrowing",
-    "Governance",
-    "Initialize",
-    "Liquidation",
-    "Token",
-    "Vault",
-    "ETokenCollateral",
-    "UnderlyingToken"
-]
-
-for conf in hs_confs:
-    script = f"certora/conf/healthStatus/{conf}HealthStatus.conf"
-    command = f"certoraRun {script} --msg \"{conf} : {args.batchMsg}\" --rule \"accountsStayHealthy_strategy\""
-    print(f"runing {command}")
-    subprocess.run(command, shell=True)
-
-# List includes all public non-view methods
-gov_separate_methods = [
-    "convertFees()",
-    "setGovernorAdmin(address)",
-    "setFeeReceiver(address)",
-    "setLTV(address,uint16,uint16,uint32)",
-    "clearLTV(address)",
-    "setMaxLiquidationDiscount(uint16)",
-    "setLiquidationCoolOffTime(uint16)",
-    "setInterestRateModel(address)",
-    "setHookConfig(address,uint32)",
-    "setConfigFlags(uint32)",
-    "setCaps(uint16,uint16)",
-    "setInterestFee(uint16)"
-]
-
-for method in gov_separate_methods:
-    script = f"certora/conf/healthStatus/GovernanceHealthStatus.conf"
-    command = f"certoraRun {script} --msg \"Governance.{method} : {args.batchMsg}\" --rule \"accountsStayHealthy_strategy\" --method \"{method}\""
-    print(f"runing {command}")
-    subprocess.run(command, shell=True)
-
-borrow_separate_methods = [
-  "borrow(uint256,address)",
-  "pullDebt(uint256,address)",
-  "repayWithShares(uint256,address)",
-  "repay(uint256,address)",
-]
-
-for method in borrow_separate_methods:
-    script = f"certora/conf/healthStatus/BorrowingHealthStatus.conf"
-    command = f"certoraRun {script} --msg \"Borrow.{method} : {args.batchMsg}\" --rule \"accountsStayHealthy_strategy\" --method \"{method}\""
-    print(f"runing {command}")
-    subprocess.run(command, shell=True)
-
-vault_separate_methods = [
-  "redeem(uint256,address,address)",
-  "withdraw(uint256,address,address)"
-]
-
-for method in vault_separate_methods:
-    script = f"certora/conf/healthStatus/VaultHealthStatus.conf"
-    command = f"certoraRun {script} --msg \"Vault.{method} : {args.batchMsg}\" --rule \"accountsStayHealthy_strategy\" --method \"{method}\""
-    print(f"runing {command}")
-    subprocess.run(command, shell=True)
+# hs_confs = [
+#     "BalanceForwarder",
+#     "Borrowing",
+#     "Governance",
+#     "Initialize",
+#     "Liquidation",
+#     "Token",
+#     "Vault",
+#     "ETokenCollateral",
+#     "UnderlyingToken"
+# ]
+# 
+# for conf in hs_confs:
+#     script = f"certora/conf/healthStatus/{conf}HealthStatus.conf"
+#     command = f"certoraRun {script} --msg \"{conf} : {args.batchMsg}\" --rule \"accountsStayHealthy_strategy\""
+#     print(f"runing {command}")
+#     subprocess.run(command, shell=True)
+# 
+# # List includes all public non-view methods aside from setLTV, clearLTV which
+# # are out of scope for the holy grail rule.
+# gov_separate_methods = [
+#     "convertFees()",
+#     "setGovernorAdmin(address)",
+#     "setFeeReceiver(address)",
+#     "setMaxLiquidationDiscount(uint16)",
+#     "setLiquidationCoolOffTime(uint16)",
+#     "setInterestRateModel(address)",
+#     "setHookConfig(address,uint32)",
+#     "setConfigFlags(uint32)",
+#     "setCaps(uint16,uint16)",
+#     "setInterestFee(uint16)"
+# ]
+# 
+# for method in gov_separate_methods:
+#     script = f"certora/conf/healthStatus/GovernanceHealthStatus.conf"
+#     command = f"certoraRun {script} --msg \"Governance.{method} : {args.batchMsg}\" --rule \"accountsStayHealthy_strategy\" --method \"{method}\""
+#     print(f"runing {command}")
+#     subprocess.run(command, shell=True)
+# 
+# borrow_separate_methods = [
+#   "borrow(uint256,address)",
+#   "pullDebt(uint256,address)",
+#   "repayWithShares(uint256,address)",
+#   "repay(uint256,address)",
+# ]
+# 
+# for method in borrow_separate_methods:
+#     script = f"certora/conf/healthStatus/BorrowingHealthStatus.conf"
+#     command = f"certoraRun {script} --msg \"Borrow.{method} : {args.batchMsg}\" --rule \"accountsStayHealthy_strategy\" --method \"{method}\""
+#     print(f"runing {command}")
+#     subprocess.run(command, shell=True)
+# 
+# vault_separate_methods = [
+#   "redeem(uint256,address,address)",
+#   "withdraw(uint256,address,address)"
+# ]
+# 
+# for method in vault_separate_methods:
+#     script = f"certora/conf/healthStatus/VaultHealthStatus.conf"
+#     command = f"certoraRun {script} --msg \"Vault.{method} : {args.batchMsg}\" --rule \"accountsStayHealthy_strategy\" --method \"{method}\""
+#     print(f"runing {command}")
+#     subprocess.run(command, shell=True)
 
 liquidate_cases = [
     "liquidateAccountsStayHealthy_liquidator_no_debt_socialization",

diff --git a/certora/specs/LiquidateHealthStatus.spec b/certora/specs/LiquidateHealthStatus.spec
@@ -129,10 +129,8 @@ function CVLSafeTransferFrom(address token, address from, address to, uint256 va
 */
 // Because calling to requireAccountStatusCheck on EVC is expensive
 // for the prover, instead assign which account gets checked to a ghost
-persistent ghost address collateralTransferCheckedAccount;
 function CVLEnforceCollateralTransfer(address collateral, uint256 amount, address from, address receiver) {
     env e;
-    collateralTransferCheckedAccount = from;
     if (collateral == ETokenA) {
         ETokenA.transferFromInternalHarnessed(e, from, receiver, amount);
     } else if (collateral == ETokenB) {
@@ -198,7 +196,6 @@ rule liquidateAccountsStayHealthy_liquidator_no_debt_socialization {
 
     // initialize checked accounts to 0
     require accountToCheckGhost == 0; // account checked in initialize
-    require collateralTransferCheckedAccount == 0;
 
     // account eq liquidator case
     require collateral == ETokenA || collateral == ETokenB;
@@ -215,9 +212,6 @@ rule liquidateAccountsStayHealthy_liquidator_no_debt_socialization {
     if(accountToCheckGhost != 0) {
         currentContract.checkAccountStatus(e, accountToCheckGhost, collaterals);
     }
-    if(collateralTransferCheckedAccount != 0) {
-        currentContract.checkAccountStatus(e, collateralTransferCheckedAccount, collaterals);
-    }
 
     bool healthyAfter = checkLiquidityReturning(e, account, collaterals);
     assert healthyBefore => healthyAfter; 
@@ -262,7 +256,6 @@ rule liquidateAccountsStayHealthy_liquidator_with_debt_socialization {
 
     // initialize checked accounts to 0
     require accountToCheckGhost == 0; // account checked in initialize
-    require collateralTransferCheckedAccount == 0;
 
     // account eq liquidator case
     require collateral == collaterals[0] || collateral == collaterals[1];
@@ -279,9 +272,6 @@ rule liquidateAccountsStayHealthy_liquidator_with_debt_socialization {
     if(accountToCheckGhost != 0) {
         currentContract.checkAccountStatus(e, accountToCheckGhost, collaterals);
     }
-    if(collateralTransferCheckedAccount != 0) {
-        currentContract.checkAccountStatus(e, collateralTransferCheckedAccount, collaterals);
-    }
 
     bool healthyAfter = checkLiquidityReturning(e, account, collaterals);
     assert healthyBefore => healthyAfter; 
@@ -325,7 +315,6 @@ rule liquidateAccountsStayHealthy_not_violator {
 
     // initialize checked accounts to 0
     require accountToCheckGhost == 0; // account checked in initialize
-    require collateralTransferCheckedAccount == 0;
 
     // account NE violator case
     require account != violator;
@@ -347,9 +336,6 @@ rule liquidateAccountsStayHealthy_not_violator {
     if(accountToCheckGhost != 0) {
         currentContract.checkAccountStatus(e, accountToCheckGhost, collaterals);
     }
-    if(collateralTransferCheckedAccount != 0) {
-        currentContract.checkAccountStatus(e, collateralTransferCheckedAccount, collaterals);
-    }
 
     bool healthyAfter = checkLiquidityReturning(e, account, collaterals);
     assert healthyBefore => healthyAfter; 
@@ -393,7 +379,6 @@ rule liquidateAccountsStayHealthy_account_cur_contract {
 
     // initialize checked accounts to 0
     require accountToCheckGhost == 0; // account checked in initialize
-    require collateralTransferCheckedAccount == 0;
 
     bool healthyBefore = checkLiquidityReturning(e, account, collaterals);
     currentContract.liquidate(e, violator, collateral, repayAssets, minYieldBalance);
@@ -410,9 +395,6 @@ rule liquidateAccountsStayHealthy_account_cur_contract {
     if(accountToCheckGhost != 0) {
         currentContract.checkAccountStatus(e, accountToCheckGhost, collaterals);
     }
-    if(collateralTransferCheckedAccount != 0) {
-        currentContract.checkAccountStatus(e, collateralTransferCheckedAccount, collaterals);
-    }
 
     bool healthyAfter = checkLiquidityReturning(e, account, collaterals);
     assert healthyBefore => healthyAfter; 

diff --git a/certora/specs/Liquidation.spec b/certora/specs/Liquidation.spec
@@ -76,6 +76,34 @@ rule checkLiquidation_healthy() {
     assert maxYield == 0;
 }
 
+rule checkLiquidation_healthy_reverts() {
+    env e;
+    address account;
+    require oracleAddress != 0;
+
+    uint256 liquidityCollateralValue;
+    uint256 liquidityLiabilityValue;
+    address[] collaterals = getCollateralsExt(account);
+    require collaterals.length == 2; // loop unrolling bound
+    (liquidityCollateralValue, liquidityLiabilityValue) = 
+        calculateLiquidityLiquidation(e, account);
+
+    // returns true if there is no liability
+    require liquidityLiabilityValue > 0;
+
+    // calculateLiquidity and checkLiquidity are only
+    // the same if the unitOfAccount is the same
+    // as the underlying asset -- otherwise the
+    // value of the unitOfAccount could change the value
+    // of the liability value returned by getLiabilityValue
+    require unitOfAccount == erc20;
+
+    // checkLiquidityReturning must return FALSE if collateral is not
+    // greater than liability.
+    assert checkLiquidityReturning(e, account, collaterals) <=>
+        (liquidityCollateralValue > liquidityLiabilityValue);
+}
+
 // passing
 // checkLiquidation must revert if:
 //  - violator is the same account as liquidator

diff --git a/certora/specs/RiskManager.spec b/certora/specs/RiskManager.spec
@@ -65,6 +65,23 @@ rule ltv_liabilities_equal{
     assert liabilityValue_liquidation == liabilityValue_borrowing;
 }
 
+rule checkLiquidityReturningSameAsOriginal {
+    env e;
+    address account;
+    address[] collaterals = getCollateralsExt(account);
+    // rule out irrelevant reverts in calculateLiquidityExternal
+    // which are also ruled out by the EVC call/batch interface
+    // and the setup for the holy grail rule
+    require e.msg.sender == evc;
+    require evc.areChecksInProgress(e);
+
+    require collaterals.length <= 2; // loop bound
+    bool ret = checkLiquidityReturning(e, account, collaterals);
+    checkAccountStatus@withrevert(e, account, collaterals);
+    bool originalReverted = lastReverted;
+    assert ret <=> !originalReverted;
+}
+
 // Passing
 
 rule accountLiquidityMustRevert {