[Certora] Last timeouts

.github/workflows/certora.yml

@@ -20,10 +20,10 @@ jobs:
           - AssetsAccounting
           - ConsistentState
           - ExactMath
+          - ExchangeRate
           - Health
           - LibSummary
           - Liveness
-          - RatioMath
           - Reentrancy
           - Reverts
           - Transfer

certora/README.md

@@ -70,10 +70,10 @@ Said otherwise, markets are independent: tokens from a given market cannot be im
 When supplying on Morpho Blue, interest is earned over time, and the distribution is implemented through a shares mechanism.
 Shares increase in value as interest is accrued.
 The share mechanism is implemented symetrically for the borrow side: a share of borrow increasing in value over time represents additional owed interest.
-The rule `accrueInterestIncreasesSupplyRatio` checks this property for the supply side with the following statement.
+The rule `accrueInterestIncreasesSupplyExchangeRate` checks this property for the supply side with the following statement.
 
 ```soldidity
-    // Check that the ratio increases: assetsBefore/sharesBefore <= assetsAfter/sharesAfter.
+    // Check that the exchange rate increases: assetsBefore/sharesBefore <= assetsAfter/sharesAfter
     assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore;
 ```
 
@@ -253,7 +253,7 @@ The [`certora/specs`](specs) folder contains the following files:
   Notably, functions cannot render an account unhealthy, and debt positions always have some collateral (thanks to the bad debt realization mechanism).
 - [`LibSummary.spec`](specs/LibSummary.spec) checks the summarization of the library functions that are used in other specification files.
 - [`Liveness.spec`](specs/Liveness.spec) checks that main functions change the owner of funds and the amount of shares as expected, and that it's always possible to exit a position.
-- [`RatioMath.spec`](specs/RatioMath.spec) checks that the ratio between shares and assets evolves predictably over time.
+- [`ExchangeRate.spec`](specs/ExchangeRate.spec) checks that the exchange rate between shares and assets evolves predictably over time.
 - [`Reentrancy.spec`](specs/Reentrancy.spec) checks that the contract is immune to a particular class of reentrancy issues.
 - [`Reverts.spec`](specs/Reverts.spec) checks the condition for reverts and that inputs are correctly validated.
 - [`Transfer.spec`](specs/Transfer.spec) checks the summarization of the safe transfer library functions that are used in other specification files.

certora/confs/RatioMath.conf → certora/confs/ExchangeRate.conf

@@ -3,13 +3,12 @@
         "certora/harness/MorphoHarness.sol",
     ],
     "solc": "solc-0.8.19",
-    "verify": "MorphoHarness:certora/specs/RatioMath.spec",
+    "verify": "MorphoHarness:certora/specs/ExchangeRate.spec",
     "rule_sanity": "basic",
     "prover_args": [
         "-smt_hashingScheme plaininjectivity",
-        "-mediumTimeout 30",
-        "-timeout 3600",
+        "-smt_easy_LIA true",
     ],
     "server": "production",
-    "msg": "Morpho Blue Ratio Math"
+    "msg": "Morpho Blue Exchange Rate"
 }

certora/confs/LibSummary.conf

@@ -5,6 +5,9 @@
     "solc": "solc-0.8.19",
     "verify": "MorphoHarness:certora/specs/LibSummary.spec",
     "rule_sanity": "basic",
+    "prover_args": [
+        "-useBitVectorTheory",
+    ],
     "server": "production",
     "msg": "Morpho Blue Lib Summary"
 }

certora/harness/MorphoHarness.sol

@@ -90,6 +90,10 @@ contract MorphoHarness is Morpho {
         return MathLib.mulDivDown(x, y, d);
     }
 
+    function libMin(uint256 x, uint256 y) external pure returns (uint256) {
+        return UtilsLib.min(x, y);
+    }
+
     function isHealthy(MarketParams memory marketParams, address user) external view returns (bool) {
         return _isHealthy(marketParams, marketParams.id(), user);
     }

certora/specs/ExactMath.spec

@@ -32,9 +32,9 @@ function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 {
     return require_uint256((x * y) / d);
 }
 
-// Check that when not accruing interest, and when repaying all, the borrow ratio is at least reset to the initial ratio.
-// More details on the purpose of this rule in RatioMath.spec.
-rule repayAllResetsBorrowRatio(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) {
+// 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) {
     MorphoHarness.Id id = libId(marketParams);
     // Safe require because this invariant is checked in ConsistentState.spec
     require fee(id) <= maxFee();

certora/specs/RatioMath.spec → certora/specs/ExchangeRate.spec

@@ -13,6 +13,7 @@ methods {
     function maxFee() external returns uint256 envfree;
     function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
 
+    function UtilsLib.min(uint256 x, uint256 y) internal returns uint256 => summaryMin(x, y);
     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 MathLib.wTaylorCompounded(uint256, uint256) internal returns uint256 => NONDET;
@@ -24,6 +25,10 @@ methods {
 invariant feeInRange(MorphoHarness.Id id)
     fee(id) <= maxFee();
 
+function summaryMin(uint256 x, uint256 y) returns uint256 {
+    return x < y ? x : y;
+}
+
 // This is a simple overapproximative summary, stating that it rounds in the right direction.
 function summaryMulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 {
     uint256 result;
@@ -41,7 +46,7 @@ function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 {
 }
 
 // Check that accrueInterest increases the value of supply shares.
-rule accrueInterestIncreasesSupplyRatio(env e, MorphoHarness.MarketParams marketParams) {
+rule accrueInterestIncreasesSupplyExchangeRate(env e, MorphoHarness.MarketParams marketParams) {
     MorphoHarness.Id id;
     requireInvariant feeInRange(id);
 
@@ -54,12 +59,12 @@ rule accrueInterestIncreasesSupplyRatio(env e, MorphoHarness.MarketParams market
     mathint assetsAfter = virtualTotalSupplyAssets(id);
     mathint sharesAfter = virtualTotalSupplyShares(id);
 
-    // Check that the ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter.
+    // Check that the exchange rate increases: assetsBefore/sharesBefore <= assetsAfter/sharesAfter.
     assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore;
 }
 
 // Check that accrueInterest increases the value of borrow shares.
-rule accrueInterestIncreasesBorrowRatio(env e, MorphoHarness.MarketParams marketParams) {
+rule accrueInterestIncreasesBorrowExchangeRate(env e, MorphoHarness.MarketParams marketParams) {
     MorphoHarness.Id id;
     requireInvariant feeInRange(id);
 
@@ -72,13 +77,13 @@ rule accrueInterestIncreasesBorrowRatio(env e, MorphoHarness.MarketParams market
     mathint assetsAfter = virtualTotalBorrowAssets(id);
     mathint sharesAfter = virtualTotalBorrowShares(id);
 
-    // Check that the ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter.
+    // Check that the exchange rate increases: assetsBefore/sharesBefore <= assetsAfter/sharesAfter.
     assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore;
 }
 
 
 // Check that except when not accruing interest and except for liquidate, every function increases the value of supply shares.
-rule onlyLiquidateCanDecreaseSupplyRatio(env e, method f, calldataarg args)
+rule onlyLiquidateCanDecreaseSupplyExchangeRate(env e, method f, calldataarg args)
 filtered {
     f -> !f.isView && f.selector != sig:liquidate(MorphoHarness.MarketParams, address, uint256, uint256, bytes).selector
 }
@@ -98,12 +103,12 @@ filtered {
     mathint assetsAfter = virtualTotalSupplyAssets(id);
     mathint sharesAfter = virtualTotalSupplyShares(id);
 
-    // Check that the ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter
+    // Check that the exchange rate increases: assetsBefore/sharesBefore <= assetsAfter/sharesAfter
     assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore;
 }
 
 // Check that when not realizing bad debt in liquidate, the value of supply shares increases.
-rule liquidateWithoutBadDebtRealizationIncreasesSupplyRatio(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, uint256 repaidShares, bytes data)
+rule liquidateWithoutBadDebtRealizationIncreasesSupplyExchangeRate(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, uint256 repaidShares, bytes data)
 {
     MorphoHarness.Id id;
     requireInvariant feeInRange(id);
@@ -123,14 +128,14 @@ rule liquidateWithoutBadDebtRealizationIncreasesSupplyRatio(env e, MorphoHarness
     // Trick to ensure that no bad debt realization happened.
     require collateral(id, borrower) != 0;
 
-    // Check that the ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter
+    // Check that the exchange rate increases: assetsBefore/sharesBefore <= assetsAfter/sharesAfter
     assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore;
 }
 
 // Check that except when not accruing interest, every function is decreasing the value of borrow shares.
 // The repay function is checked separately, see below.
-// The liquidate function is not checked.
-rule onlyAccrueInterestCanIncreaseBorrowRatio(env e, method f, calldataarg args)
+// The liquidate function is checked separately, see below.
+rule onlyAccrueInterestCanIncreaseBorrowExchangeRate(env e, method f, calldataarg args)
 filtered {
     f -> !f.isView &&
     f.selector != sig:repay(MorphoHarness.MarketParams, uint256, uint256, address, bytes).selector &&
@@ -140,7 +145,7 @@ filtered {
     MorphoHarness.Id id;
     requireInvariant feeInRange(id);
 
-    // Interest would increase borrow ratio, so we need to assume that no time passes.
+    // Interest would increase borrow exchange rate, so we need to assume that no time passes.
     require lastUpdate(id) == e.block.timestamp;
 
     mathint assetsBefore = virtualTotalBorrowAssets(id);
@@ -151,34 +156,56 @@ filtered {
     mathint assetsAfter = virtualTotalBorrowAssets(id);
     mathint sharesAfter = virtualTotalBorrowShares(id);
 
-    // Check that the ratio decreases: assetsBefore/sharesBefore >= assetsAfter / sharesAfter
+    // Check that the exchange rate decreases: assetsBefore/sharesBefore >= assetsAfter/sharesAfter
     assert assetsBefore * sharesAfter >= assetsAfter * sharesBefore;
 }
 
 // Check that when not accruing interest, repay is decreasing the value of borrow shares.
-// Check the case where the market is not repaid fully.
+// Check the case where it would not repay more than the total assets.
 // The other case requires exact math (ie not over-approximating mulDivUp and mulDivDown), so it is checked separately in ExactMath.spec.
-rule repayDecreasesBorrowRatio(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data)
+rule repayDecreasesBorrowExchangeRate(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data)
 {
     MorphoHarness.Id id = libId(marketParams);
     requireInvariant feeInRange(id);
 
     mathint assetsBefore = virtualTotalBorrowAssets(id);
     mathint sharesBefore = virtualTotalBorrowShares(id);
 
-    // Interest would increase borrow ratio, so we need to assume that no time passes.
+    // Interest would increase borrow exchange rate, so we need to assume that no time passes.
     require lastUpdate(id) == e.block.timestamp;
 
     mathint repaidAssets;
     repaidAssets, _ = repay(e, marketParams, assets, shares, onBehalf, data);
 
-    // Check the case where the market is not repaid fully.
+    // Check the case where it would not repay more than the total assets.
     require repaidAssets < assetsBefore;
 
     mathint assetsAfter = virtualTotalBorrowAssets(id);
     mathint sharesAfter = virtualTotalBorrowShares(id);
 
     assert assetsAfter == assetsBefore - repaidAssets;
-    // Check that the ratio decreases: assetsBefore/sharesBefore >= assetsAfter / sharesAfter
+    // Check that the exchange rate decreases: assetsBefore/sharesBefore >= assetsAfter/sharesAfter
+    assert assetsBefore * sharesAfter >= assetsAfter * sharesBefore;
+}
+
+rule liquidateDecreasesBorrowExchangeRate(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, uint256 repaidShares, bytes data)
+{
+    require data.length == 0;
+    MorphoHarness.Id id = libId(marketParams);
+
+    mathint assetsBefore = virtualTotalBorrowAssets(id);
+    mathint sharesBefore = virtualTotalBorrowShares(id);
+
+    // Interest would increase borrow exchange rate, so we need to assume that no time passes.
+    require lastUpdate(id) == e.block.timestamp;
+
+    liquidate(e, marketParams, borrower, seizedAssets, repaidShares, data);
+
+    mathint assetsAfter = virtualTotalBorrowAssets(id);
+    mathint sharesAfter = virtualTotalBorrowShares(id);
+
+    require assetsAfter != 1;
+
+    // Check that the exchange rate decreases: assetsBefore/sharesBefore >= assetsAfter/sharesAfter
     assert assetsBefore * sharesAfter >= assetsAfter * sharesBefore;
 }

certora/specs/Health.spec

@@ -47,13 +47,11 @@ function summaryMin(uint256 a, uint256 b) returns uint256 {
 }
 
 // Check that without accruing interest, no interaction can put an healthy account into an unhealthy one.
-// This rule times out for liquidate, repay and borrow.
+// The liquidate function times out in this rule, but has been checked separately.
 rule stayHealthy(env e, method f, calldataarg data)
 filtered {
     f -> !f.isView &&
-    f.selector != sig:liquidate(MorphoHarness.MarketParams, address, uint256, uint256, bytes).selector &&
-    f.selector != sig:repay(MorphoHarness.MarketParams, uint256, uint256, address, bytes).selector &&
-    f.selector != sig:borrow(MorphoHarness.MarketParams, uint256, uint256, address, address).selector
+    f.selector != sig:liquidate(MorphoHarness.MarketParams, address, uint256, uint256, bytes).selector
 }
 {
     MorphoHarness.MarketParams marketParams;

certora/specs/LibSummary.spec

@@ -6,15 +6,16 @@ methods {
     function libMulDivDown(uint256, uint256, uint256) external returns uint256 envfree;
     function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
     function refId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
+    function libMin(uint256 x, uint256 y) external returns uint256 envfree;
 }
 
-// Check the summary of MathLib.mulDivUp required by RatioMath.spec
+// Check the summary of MathLib.mulDivUp required by ExchangeRate.spec
 rule checkSummaryMulDivUp(uint256 x, uint256 y, uint256 d) {
     uint256 result = libMulDivUp(x, y, d);
     assert result * d >= x * y;
 }
 
-// Check the summary of MathLib.mulDivDown required by RatioMath.spec
+// Check the summary of MathLib.mulDivDown required by ExchangeRate.spec
 rule checkSummaryMulDivDown(uint256 x, uint256 y, uint256 d) {
     uint256 result = libMulDivDown(x, y, d);
     assert result * d <= x * y;
@@ -24,3 +25,8 @@ rule checkSummaryMulDivDown(uint256 x, uint256 y, uint256 d) {
 rule checkSummaryId(MorphoHarness.MarketParams marketParams) {
     assert libId(marketParams) == refId(marketParams);
 }
+
+rule checkSummaryMin(uint256 x, uint256 y) {
+    uint256 refMin = x < y ? x : y;
+    assert libMin(x, y) == refMin;
+}