[Certora] Check that supply share ratio increases and borrow share ratio decreases

certora/scripts/verifyBlueRatioMath.sh

@@ -5,4 +5,5 @@ certoraRun \
     --verify MorphoHarness:certora/specs/BlueRatioMath.spec \
     --solc_allow_path src \
     --msg "Morpho Ratio Math" \
+    --prover_args '-smt_hashingScheme plaininjectivity' \
     "$@"

certora/specs/BlueRatioMath.spec

@@ -1,7 +1,11 @@
 methods {
+    function getMarketId(MorphoHarness.Market) external returns MorphoHarness.Id envfree;
     function totalSupply(MorphoHarness.Id) external returns uint256 envfree;
     function totalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;
+    function totalBorrow(MorphoHarness.Id) external returns uint256 envfree;
+    function totalBorrowShares(MorphoHarness.Id) external returns uint256 envfree;
     function fee(MorphoHarness.Id) external returns uint256 envfree;
+    function lastUpdate(MorphoHarness.Id) external returns uint256 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);
@@ -35,9 +39,48 @@ function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 {
     return result;
 }
 
-rule onlyLiquidateCanDecreasesRatio(method f)
+rule accrueInterestsIncreasesSupplyRatio() {
+    MorphoHarness.Market market;
+    MorphoHarness.Id id;
+    requireInvariant feeInRange(id);
+
+    mathint assetsBefore = totalSupply(id) + VIRTUAL_ASSETS();
+    mathint sharesBefore = totalSupplyShares(id) + VIRTUAL_SHARES();
+
+    // The check is done for every market, not just for id.
+    env e;
+    accrueInterests(e, market);
+
+    mathint assetsAfter = totalSupply(id) + VIRTUAL_ASSETS();
+    mathint sharesAfter = totalSupplyShares(id) + VIRTUAL_SHARES();
+
+    // Check if ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter
+    assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore;
+}
+
+rule accrueInterestsIncreasesBorrowRatio() {
+    MorphoHarness.Market market;
+    MorphoHarness.Id id;
+    requireInvariant feeInRange(id);
+
+    mathint assetsBefore = totalBorrow(id) + VIRTUAL_ASSETS();
+    mathint sharesBefore = totalBorrowShares(id) + VIRTUAL_SHARES();
+
+    // The check is done for every market, not just for id.
+    env e;
+    accrueInterests(e, market);
+
+    mathint assetsAfter = totalBorrow(id) + VIRTUAL_ASSETS();
+    mathint sharesAfter = totalBorrowShares(id) + VIRTUAL_SHARES();
+
+    // Check if ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter
+    assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore;
+}
+
+
+rule onlyLiquidateCanDecreaseSupplyRatio(env e, method f, calldataarg args)
 filtered {
-    f -> f.selector != sig:liquidate(MorphoHarness.Market, address, uint256, bytes).selector
+    f -> !f.isView && f.selector != sig:liquidate(MorphoHarness.Market, address, uint256, bytes).selector
 }
 {
     MorphoHarness.Id id;
@@ -46,13 +89,36 @@ filtered {
     mathint assetsBefore = totalSupply(id) + VIRTUAL_ASSETS();
     mathint sharesBefore = totalSupplyShares(id) + VIRTUAL_SHARES();
 
-    env e;
-    calldataarg args;
+    // Interest is checked separately by the rules above.
+    // Here we assume interest has already been accumulated for this block.
+    require lastUpdate(id) == e.block.timestamp;
+
     f(e,args);
 
     mathint assetsAfter = totalSupply(id) + VIRTUAL_ASSETS();
     mathint sharesAfter = totalSupplyShares(id) + VIRTUAL_SHARES();
 
-    // check if ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter;
+    // Check if ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter
     assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore;
 }
+
+rule onlyAccrueInterestsCanIncreaseBorrowRatio(env e, method f, calldataarg args)
+filtered { f -> !f.isView }
+{
+    MorphoHarness.Id id;
+    requireInvariant feeInRange(id);
+
+    mathint assetsBefore = totalBorrow(id) + VIRTUAL_ASSETS();
+    mathint sharesBefore = totalBorrowShares(id) + VIRTUAL_SHARES();
+
+    // Interest would increase borrow ratio, so we need to assume no time passes.
+    require lastUpdate(id) == e.block.timestamp;
+
+    f(e,args);
+
+    mathint assetsAfter = totalBorrow(id) + VIRTUAL_ASSETS();
+    mathint sharesAfter = totalBorrowShares(id) + VIRTUAL_SHARES();
+
+    // Check if ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter
+    assert assetsBefore * sharesAfter >= assetsAfter * sharesBefore;
+}