feat: add respect supply cap rule

.github/workflows/certora.yml

@@ -28,6 +28,7 @@ jobs:
           - Reentrancy
           - Reverts
           - Roles
+          - SupplyCap
           - Timelock
           - Tokens
 

certora/confs/SupplyCap.conf

@@ -0,0 +1,21 @@
+{
+    "files": [
+        "lib/morpho-blue/certora/harness/MorphoHarness.sol",
+        "certora/helpers/MetaMorphoHarness.sol",
+        "certora/helpers/Util.sol",
+    ],
+    "link": [
+        "MetaMorphoHarness:MORPHO=MorphoHarness",
+    ],
+    "solc_map": {
+        "MorphoHarness": "solc-0.8.19",
+        "MetaMorphoHarness": "solc-0.8.21",
+        "Util": "solc-0.8.21",
+    },
+    "verify": "MetaMorphoHarness:certora/specs/SupplyCap.spec",
+    "loop_iter": "2",
+    "optimistic_loop": true,
+    "rule_sanity": "basic",
+    "server": "production",
+    "msg": "MetaMorpho Supply Cap",
+}

certora/helpers/Util.sol

@@ -42,6 +42,17 @@ contract Util {
         }
     }
 
+    function accrueInterest(IMorphoHarness morpho, Id id) external {
+        morpho.accrueInterest(id);
+    }
+
+    function supplyAssets(IMorphoHarness morpho, Id id, address user) external view returns (uint256) {
+        uint256 supplyShares = morpho.supplyShares(id, user);
+        Market memory market = morpho.market(id);
+
+        return supplyShares.toAssetsDown(market.totalSupplyAssets, market.totalSupplyShares);
+    }
+
     function libId(MarketParams memory marketParams) external pure returns (Id) {
         return marketParams.id();
     }

certora/specs/SupplyCap.spec

@@ -0,0 +1,33 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+
+using MorphoHarness as Morpho;
+
+methods {
+    function Morpho.supplyShares(MorphoHarness.Id, address) external returns(uint256) envfree;
+    function Morpho.totalSupplyAssets(MorphoHarness.Id) external returns(uint256) envfree;
+    function Morpho.totalSupplyShares(MorphoHarness.Id) external returns(uint256) envfree;
+
+    function Util.accrueInterest(address, MorphoHarness.Id) external returns(uint256) envfree;
+    function Util.supplyAssets(address, MorphoHarness.Id, address) external envfree;
+
+    function MORPHO() external returns(address) envfree;
+}
+
+methods {
+    function config_(MetaMorphoHarness.Id) external returns(MetaMorphoHarness.MarketConfig) envfree;
+}
+
+rule respectSupplyCap(method f, env e, calldataarg args)
+{
+    MetaMorphoHarness.Id id;
+    address morpho = MORPHO();
+    uint256 cap = config_(id).cap;
+
+    Util.accrueInterest(morpho, id);
+    require Util.supplyAssets(morpho, id, currentContract) < cap;
+
+    f(e, args);
+    require config_(id).cap == cap;
+
+    assert Util.supplyAssets(morpho, id, currentContract) < cap;
+}