Merge pull request #689 from morpho-org/certora/improve-assets-accounting

[Certora] Improve assets accounting specification

Author: MerlinEgalite

certora/specs/AssetsAccounting.spec

@@ -5,6 +5,8 @@ methods {
     function supplyShares(MorphoHarness.Id, address) external returns uint256 envfree;
     function borrowShares(MorphoHarness.Id, address) external returns uint256 envfree;
     function collateral(MorphoHarness.Id, address) external returns uint256 envfree;
+    function totalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;
+    function totalBorrowShares(MorphoHarness.Id) external returns uint256 envfree;
     function virtualTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree;
     function virtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;
     function virtualTotalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree;
@@ -32,21 +34,23 @@ function expectedBorrowAssets(MorphoHarness.Id id, address user) returns uint256
     return libMulDivUp(userShares, totalBorrowAssets, totalBorrowShares);
 }
 
-// Check that the assets supplied are greater than the assets owned in the end.
+// Check that the assets supplied are greater than the increase in owned assets.
 rule supplyAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) {
     MorphoHarness.Id id = libId(marketParams);
 
     // Assume no interest as it would increase the total supply assets.
     require lastUpdate(id) == e.block.timestamp;
-    // Assume no supply position to begin with.
-    require supplyShares(id, onBehalf) == 0;
+    // Safe require because of the sumSupplySharesCorrect invariant.
+    require supplyShares(id, onBehalf) <= totalSupplyShares(id);
+
+    uint256 ownedAssetsBefore = expectedSupplyAssets(id, onBehalf);
 
     uint256 suppliedAssets;
     suppliedAssets, _ = supply(e, marketParams, assets, shares, onBehalf, data);
 
     uint256 ownedAssets = expectedSupplyAssets(id, onBehalf);
 
-    assert suppliedAssets >= ownedAssets;
+    assert ownedAssetsBefore + suppliedAssets >= to_mathint(ownedAssets);
 }
 
 // Check that the assets withdrawn are less than the assets owned initially.
@@ -64,22 +68,24 @@ rule withdrawAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, ui
     assert withdrawnAssets <= ownedAssets;
 }
 
-// Check that the assets borrowed are less than the assets owed in the end.
+// Check that the increase of owed assets are greater than the borrowed assets.
 rule borrowAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 shares, address onBehalf, address receiver) {
     MorphoHarness.Id id = libId(marketParams);
 
     // Assume no interest as it would increase the total borrowed assets.
     require lastUpdate(id) == e.block.timestamp;
-    // Assume no outstanding debt to begin with.
-    require borrowShares(id, onBehalf) == 0;
+    // Safe require because of the sumBorrowSharesCorrect invariant.
+    require borrowShares(id, onBehalf) <= totalBorrowShares(id);
+
+    uint256 owedAssetsBefore = expectedBorrowAssets(id, onBehalf);
 
     // The borrow call is restricted to shares as input to make it easier on the prover.
     uint256 borrowedAssets;
     borrowedAssets, _ = borrow(e, marketParams, 0, shares, onBehalf, receiver);
 
     uint256 owedAssets = expectedBorrowAssets(id, onBehalf);
 
-    assert borrowedAssets <= owedAssets;
+    assert owedAssetsBefore + borrowedAssets <= to_mathint(owedAssets);
 }
 
 // Check that the assets repaid are greater than the assets owed initially.
@@ -100,18 +106,17 @@ rule repayAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint2
     assert repaidAssets >= owedAssets;
 }
 
-// Check that the collateral assets supplied are greater than the assets owned in the end.
+// Check that the collateral assets supplied are equal to the increase of owned assets.
 rule supplyCollateralAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 suppliedAssets, address onBehalf, bytes data) {
     MorphoHarness.Id id = libId(marketParams);
 
-    // Assume no collateral to begin with.
-    require collateral(id, onBehalf) == 0;
+    uint256 ownedAssetsBefore = collateral(id, onBehalf);
 
     supplyCollateral(e, marketParams, suppliedAssets, onBehalf, data);
 
     uint256 ownedAssets = collateral(id, onBehalf);
 
-    assert suppliedAssets == ownedAssets;
+    assert ownedAssetsBefore + suppliedAssets == to_mathint(ownedAssets);
 }
 
 // Check that the collateral assets withdrawn are less than the assets owned initially.

certora/specs/ExactMath.spec

@@ -55,7 +55,7 @@ rule repayAllResetsBorrowExchangeRate(env e, MorphoHarness.MarketParams marketPa
     mathint sharesAfter = virtualTotalBorrowShares(id);
 
     assert assetsAfter == 1;
-    // There are at least as many shares as virtual shares.
+    // There are at least as many shares as virtual shares, by definition of virtualTotalBorrowShares.
 }
 
 // There should be no profit from supply followed immediately by withdraw.