Merge remote-tracking branch 'origin/certora/dev' into certora/only-e…

…nabled
morpho-org · Aug 14, 2023 · 8acc774 · 8acc774
2 parents b20b849 + 50e3bfa
commit 8acc774
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 39 deletions.
diff --git a/certora/harness/MorphoHarness.sol b/certora/harness/MorphoHarness.sol
@@ -5,6 +5,8 @@ import "../../src/libraries/SharesMathLib.sol";
 import "../../src/libraries/MarketLib.sol";
 
 contract MorphoHarness is Morpho {
+    using MarketLib for Market;
+
     constructor(address newOwner) Morpho(newOwner) {}
 
     function getVirtualTotalSupply(Id id) external view returns (uint256) {
@@ -15,19 +17,7 @@ contract MorphoHarness is Morpho {
         return totalSupplyShares[id] + SharesMathLib.VIRTUAL_SHARES;
     }
 
-    function getTotalSupply(Id id) external view returns (uint256) {
-        return totalSupply[id];
-    }
-
-    function getTotalSupplyShares(Id id) external view returns (uint256) {
-        return totalSupplyShares[id];
-    }
-
-    function getTotalBorrowShares(Id id) external view returns (uint256) {
-        return totalBorrowShares[id];
-    }
-
-    function toId(Market memory market) external pure returns (Id) {
-        return MarketLib.id(market);
+    function getMarketId(Market memory market) external pure returns (Id) {
+        return market.id();
     }
 }
diff --git a/certora/specs/Blue.spec b/certora/specs/Blue.spec
@@ -2,19 +2,21 @@ methods {
     function supply(MorphoHarness.Market, uint256, uint256, address, bytes) external;
     function getVirtualTotalSupply(MorphoHarness.Id) external returns uint256 envfree;
     function getVirtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;
-    function getTotalSupply(MorphoHarness.Id) external returns uint256 envfree;
-    function getTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;
-    function getTotalBorrowShares(MorphoHarness.Id) external returns uint256 envfree;
+    function totalSupply(MorphoHarness.Id) external returns uint256 envfree;
+    function totalBorrow(MorphoHarness.Id) external returns uint256 envfree;
+    function totalSupplyShares(MorphoHarness.Id) external returns uint256 envfree;
+    function totalBorrowShares(MorphoHarness.Id) external returns uint256 envfree;
 
     function lastUpdate(MorphoHarness.Id) external returns uint256 envfree;
     function isLltvEnabled(uint256) external returns bool envfree;
     function isIrmEnabled(address) external returns bool envfree;
 
     function _.borrowRate(MorphoHarness.Market) external => DISPATCHER(true);
 
-    function toId(MorphoHarness.Market) external returns MorphoHarness.Id envfree;
+    function getMarketId(MorphoHarness.Market) external returns MorphoHarness.Id envfree;
     // function _.safeTransfer(address, uint256) internal => DISPATCHER(true);
     // function _.safeTransferFrom(address, address, uint256) internal => DISPATCHER(true);
+
 }
 
 ghost mapping(MorphoHarness.Id => mathint) sumSupplyShares
@@ -42,28 +44,16 @@ hook Sstore collateral[KEY MorphoHarness.Id id][KEY address owner] uint256 newAm
     sumCollateral[id] = sumCollateral[id] - oldAmount + newAmount;
 }
 
+definition VIRTUAL_ASSETS() returns mathint = 1;
+definition VIRTUAL_SHARES() returns mathint = 1000000000000000000;
+
 invariant sumSupplySharesCorrect(MorphoHarness.Id id)
-    to_mathint(getTotalSupplyShares(id)) == sumSupplyShares[id];
+    to_mathint(totalSupplyShares(id)) == sumSupplyShares[id];
 invariant sumBorrowSharesCorrect(MorphoHarness.Id id)
-    to_mathint(getTotalBorrowShares(id)) == sumBorrowShares[id];
-
-rule whatDoesNotIncreaseRatio(MorphoHarness.Id id) {
-    mathint assetsBefore = getVirtualTotalSupply(id);
-    mathint sharesBefore = getVirtualTotalSupplyShares(id);
-
-    method f;
-    env e;
-    calldataarg args;
-
-    f(e,args);
-
-    mathint assetsAfter = getVirtualTotalSupply(id);
-    mathint sharesAfter = getVirtualTotalSupplyShares(id);
-
-    // check if assetsBefore/shareBefore <= assetsAfter / sharesAfter;
-    assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore;
-}
+    to_mathint(totalBorrowShares(id)) == sumBorrowShares[id];
 
+invariant borrowLessSupply(MorphoHarness.Id id)
+    totalBorrow(id) <= totalSupply(id);
 
 rule supplyRevertZero(MorphoHarness.Market market) {
     env e;
@@ -75,7 +65,7 @@ rule supplyRevertZero(MorphoHarness.Market market) {
 }
 
 invariant invOnlyEnabledLltv(MorphoHarness.Market market)
-    lastUpdate(toId(market)) != 0 => isLltvEnabled(market.lltv);
+    lastUpdate(getMarketId(market)) != 0 => isLltvEnabled(market.lltv);
 
 invariant invOnlyEnabledIrm(MorphoHarness.Market market)
-    lastUpdate(toId(market)) != 0 => isIrmEnabled(market.irm);
+    lastUpdate(getMarketId(market)) != 0 => isIrmEnabled(market.irm);