[Certora] Simplify summarization of mulDiv and price

certora/specs/ExactMath.spec

@@ -18,23 +18,11 @@ methods {
     function Util.maxFee() external returns uint256 envfree;
     function Util.libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
 
-    function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivDown(a,b,c);
-    function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivUp(a,b,c);
     function SafeTransferLib.safeTransfer(address token, address to, uint256 value) internal => NONDET;
     function SafeTransferLib.safeTransferFrom(address token, address from, address to, uint256 value) internal => NONDET;
     function _.onMorphoSupply(uint256 assets, bytes data) external => HAVOC_ECF;
 }
 
-function summaryMulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 {
-    // Safe require because the reference implementation would revert.
-    return require_uint256((x * y + (d - 1)) / d);
-}
-
-function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 {
-    // Safe require because the reference implementation would revert.
-    return require_uint256((x * y) / d);
-}
-
 // Check that when not accruing interest, and when repaying all, the borrow exchange rate is at least reset to the initial exchange rate.
 // More details on the purpose of this rule in ExchangeRate.spec.
 rule repayAllResetsBorrowExchangeRate(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) {

certora/specs/Health.spec

@@ -18,36 +18,10 @@ methods {
     function Util.libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
     function isHealthy(MorphoHarness.MarketParams, address user) external returns bool envfree;
 
-    function _.price() external => mockPrice() expect uint256;
-    function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivDown(a,b,c);
-    function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivUp(a,b,c);
+    function _.price() external => CONSTANT;
     function UtilsLib.min(uint256 a, uint256 b) internal returns uint256 => summaryMin(a,b);
 }
 
-persistent ghost uint256 lastPrice;
-persistent ghost bool priceChanged;
-
-function mockPrice() returns uint256 {
-    uint256 updatedPrice;
-    if (updatedPrice != lastPrice) {
-        priceChanged = true;
-        lastPrice = updatedPrice;
-    }
-    return updatedPrice;
-}
-
-function summaryMulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 {
-    // Safe require because the reference implementation would revert.
-    require d != 0;
-    return require_uint256((x * y + (d - 1)) / d);
-}
-
-function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 {
-    // Safe require because the reference implementation would revert.
-    require d != 0;
-    return require_uint256((x * y) / d);
-}
-
 function summaryMin(uint256 a, uint256 b) returns uint256 {
     return a < b ? a : b;
 }
@@ -68,13 +42,11 @@ filtered { f -> !f.isView }
     // Assume that the user is healthy.
     require isHealthy(marketParams, user);
 
-    mathint collateralBefore = collateral(id, user);
+    uint256 collateralBefore = collateral(id, user);
 
     f(e, data);
 
-    mathint collateralAfter = collateral(id, user);
-
-    assert !priceChanged => collateralAfter >= collateralBefore;
+    assert collateral(id, user) >= collateralBefore;
 }
 
 // Check that users without collateral also have no debt.
@@ -94,15 +66,13 @@ rule liquidateEquivalentInputDebtAndInputCollateral(env e, MorphoHarness.MarketP
 
     uint256 repaidAssets1;
     _, repaidAssets1 = liquidate(e, marketParams, borrower, seizedAssets, 0, data);
-    require !priceChanged;
     // Omit the bad debt realization case.
     require collateral(id, borrower) != 0;
     uint256 sharesAfter = borrowShares(id, borrower);
     uint256 repaidShares1 = assert_uint256(sharesBefore - sharesAfter);
 
     uint256 repaidAssets2;
     _, repaidAssets2 = liquidate(e, marketParams, borrower, 0, repaidShares1, data) at init;
-    require !priceChanged;
 
     assert repaidAssets1 == repaidAssets2;
 }

certora/specs/StayHealthy.spec

@@ -1,6 +1,11 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
 import "Health.spec";
 
+function mulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 {
+    assert d != 0;
+    return assert_uint256((x * y + (d - 1)) / d);
+}
+
 // Check that without accruing interest, no interaction can put an healthy account into an unhealthy one.
 // The liquidate function times out in this rule, but has been checked separately.
 rule stayHealthy(env e, method f, calldataarg data)
@@ -25,8 +30,7 @@ filtered {
     // Safe require because of the invariant sumBorrowSharesCorrect.
     require borrowShares(id, user) <= totalBorrowShares(id);
 
-    bool stillHealthy = isHealthy(marketParams, user);
-    assert !priceChanged => stillHealthy;
+    assert isHealthy(marketParams, user);
 }
 
 // The liquidate case for the stayHealthy rule, assuming no bad debt realization, otherwise it times out.
@@ -41,14 +45,13 @@ rule stayHealthyLiquidate(env e, MorphoHarness.MarketParams marketParams, addres
     require isHealthy(marketParams, user);
 
     uint256 debtSharesBefore = borrowShares(id, user);
-    uint256 debtAssetsBefore = summaryMulDivUp(debtSharesBefore, virtualTotalBorrowAssets(id), virtualTotalBorrowShares(id));
+    uint256 debtAssetsBefore = mulDivUp(debtSharesBefore, virtualTotalBorrowAssets(id), virtualTotalBorrowShares(id));
     // Safe require because of the invariants onlyEnabledLltv and lltvSmallerThanWad in ConsistentState.spec.
     require marketParams.lltv < 10^18;
     // Assumption to ensure that no interest is accumulated.
     require lastUpdate(id) == e.block.timestamp;
 
     liquidate(e, marketParams, borrower, seizedAssets, 0, data);
-    require !priceChanged;
 
     // Safe require because of the invariant sumBorrowSharesCorrect.
     require borrowShares(id, user) <= totalBorrowShares(id);
@@ -57,12 +60,12 @@ rule stayHealthyLiquidate(env e, MorphoHarness.MarketParams marketParams, addres
     // Assume no bad debt realization.
     require collateral(id, borrower) > 0;
 
+    bool stillHealthy = isHealthy(marketParams, user);
+
     assert user != borrower;
     assert debtSharesBefore == borrowShares(id, user);
-    assert debtAssetsBefore >= summaryMulDivUp(debtSharesBefore, virtualTotalBorrowAssets(id), virtualTotalBorrowShares(id));
+    assert debtAssetsBefore >= mulDivUp(debtSharesBefore, virtualTotalBorrowAssets(id), virtualTotalBorrowShares(id));
 
-    bool stillHealthy = isHealthy(marketParams, user);
-    require !priceChanged;
     assert stillHealthy;
 }
 
@@ -82,14 +85,11 @@ rule stayHealthyLiquidateDifferentMarkets(env e, MorphoHarness.MarketParams mark
     require liquidationMarketParams != marketParams;
 
     liquidate(e, liquidationMarketParams, borrower, seizedAssets, 0, data);
-    require !priceChanged;
 
     // Safe require because of the invariant sumBorrowSharesCorrect.
     require borrowShares(id, user) <= totalBorrowShares(id);
 
-    bool stillHealthy = isHealthy(marketParams, user);
-    require !priceChanged;
-    assert stillHealthy;
+    assert isHealthy(marketParams, user);
 }
 
 rule stayHealthyLiquidateLastBorrow(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) {
@@ -105,14 +105,11 @@ rule stayHealthyLiquidateLastBorrow(env e, MorphoHarness.MarketParams marketPara
     require lastUpdate(id) == e.block.timestamp;
 
     liquidate(e, marketParams, borrower, seizedAssets, 0, data);
-    require !priceChanged;
 
     // Safe require because of the invariant sumBorrowSharesCorrect.
     require borrowShares(id, user) <= totalBorrowShares(id);
     // Assume that there is no remaining borrow on the market after liquidation.
     require totalBorrowAssets(id) == 0;
 
-    bool stillHealthy = isHealthy(marketParams, user);
-    require !priceChanged;
-    assert stillHealthy;
+    assert isHealthy(marketParams, user);
 }