From 12294f07050cb749240f2bfd93859cbcce3eacf2 Mon Sep 17 00:00:00 2001
From: Jochen Hoenicke <hoenicke@gmail.com>
Date: Mon, 14 Aug 2023 11:46:50 +0200
Subject: [PATCH] Added borrow less supply invariant

---
 certora/harness/MorphoHarness.sol | 14 ++++---------
 certora/specs/Blue.spec           | 34 +++++++++++--------------------
 2 files changed, 16 insertions(+), 32 deletions(-)

diff --git a/certora/harness/MorphoHarness.sol b/certora/harness/MorphoHarness.sol
index e85bd58e7..679185ef4 100644
--- a/certora/harness/MorphoHarness.sol
+++ b/certora/harness/MorphoHarness.sol
@@ -4,6 +4,8 @@ import "../../src/Morpho.sol";
 import "../../src/libraries/SharesMathLib.sol";
 
 contract MorphoHarness is Morpho {
+    using MarketLib for Market;
+    
     constructor(address newOwner) Morpho(newOwner) {}
 
     function getVirtualTotalSupply(Id id) external view returns (uint256) {
@@ -14,15 +16,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 getMarketId(Market memory market) external pure returns (Id) {
+        return market.id();
     }
 }
diff --git a/certora/specs/Blue.spec b/certora/specs/Blue.spec
index 96818620a..c6bcd7e5b 100644
--- a/certora/specs/Blue.spec
+++ b/certora/specs/Blue.spec
@@ -2,14 +2,16 @@ 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 _.borrowRate(MorphoHarness.Market) external => DISPATCHER(true);
 
     // function _.safeTransfer(address, uint256) internal => DISPATCHER(true);
     // function _.safeTransferFrom(address, address, uint256) internal => DISPATCHER(true);
+
 }
 
 ghost mapping(MorphoHarness.Id => mathint) sumSupplyShares
@@ -37,28 +39,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;