chore: rename ratio to exchange rate

.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,12 +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",
         "-smt_easy_LIA true",
     ],
     "server": "production",
-    "msg": "Morpho Blue Ratio Math"
+    "msg": "Morpho Blue Exchange Rate"
 }

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

@@ -46,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);
 
@@ -59,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);
 
@@ -77,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
 }
@@ -103,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);
@@ -128,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 checked separately, see below.
-rule onlyAccrueInterestCanIncreaseBorrowRatio(env e, method f, calldataarg args)
+rule onlyAccrueInterestCanIncreaseBorrowExchangeRate(env e, method f, calldataarg args)
 filtered {
     f -> !f.isView &&
     f.selector != sig:repay(MorphoHarness.MarketParams, uint256, uint256, address, bytes).selector &&
@@ -145,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);
@@ -156,22 +156,22 @@ 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 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;
@@ -184,19 +184,19 @@ rule repayDecreasesBorrowRatio(env e, MorphoHarness.MarketParams marketParams, u
     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 liquidateDecreasesBorrowRatio(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, uint256 repaidShares, bytes data)
+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 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;
 
     liquidate(e, marketParams, borrower, seizedAssets, repaidShares, data);
@@ -206,6 +206,6 @@ rule liquidateDecreasesBorrowRatio(env e, MorphoHarness.MarketParams marketParam
 
     require assetsAfter != 1;
 
-    // Check that the ratio decreases: assetsBefore/sharesBefore >= assetsAfter / sharesAfter
+    // Check that the exchange rate decreases: assetsBefore/sharesBefore >= assetsAfter/sharesAfter
     assert assetsBefore * sharesAfter >= assetsAfter * sharesBefore;
 }

certora/specs/LibSummary.spec

@@ -9,13 +9,13 @@ methods {
     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;