diff --git a/certora/harness/modules/LiquidationHarness.sol b/certora/harness/modules/LiquidationHarness.sol index 75b31a85..baa0908e 100644 --- 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 index 4c44e974..db29fa63 100644 --- 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 index 821e0116..53770e5e 100644 --- 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 index cc15006e..32a1fe96 100644 --- 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 index 0914d225..b643bc77 100644 --- 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 {