morpho-org · QGarchery · Aug 29, 2023 · Aug 19, 2023 · Aug 19, 2023 · Aug 19, 2023
diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml
@@ -26,14 +26,14 @@ jobs:
 
       - name: Install solc
         run: |
-          wget https://github.com/ethereum/solidity/releases/download/v0.8.21/solc-static-linux
+          wget https://github.com/ethereum/solidity/releases/download/v0.8.19/solc-static-linux
           chmod +x solc-static-linux
-          sudo mv solc-static-linux /usr/local/bin/solc8.21
+          sudo mv solc-static-linux /usr/local/bin/solc8.19
 
       - name: Verify rule ${{ matrix.script }}
         run: |
           echo "key length" ${#CERTORAKEY}
-          bash certora/scripts/${{ matrix.script }} --solc solc8.21
+          bash certora/scripts/${{ matrix.script }} --solc solc8.19
         env:
           CERTORAKEY: ${{ secrets.CERTORAKEY }}
 
@@ -45,8 +45,11 @@ jobs:
         script:
           - verifyBlue.sh
           - verifyBlueAccrueInterests.sh
-          - verifyBlueRatioMathSummary.sh
           - verifyBlueExitLiquidity.sh
+          - verifyBlueLibSummary.sh
+          - verifyBlueRatioMath.sh
+          - verifyBlueReverts.sh
           - verifyBlueTransfer.sh
-          - verifyReentrancy.sh
           - verifyDifficultMath.sh
+          - verifyHealth.sh
+          - verifyReentrancy.sh
diff --git a/certora/dispatch/ERC20NoRevert.sol b/certora/dispatch/ERC20NoRevert.sol
@@ -44,8 +44,6 @@ contract ERC20NoRevert {
     }
 
     function approve(address _spender, uint256 _amount) public {
-        require(!((_amount != 0) && (allowed[msg.sender][_spender] != 0)));
-
         allowed[msg.sender][_spender] = _amount;
     }
 

diff --git a/certora/harness/MorphoHarness.sol b/certora/harness/MorphoHarness.sol
@@ -1,11 +1,11 @@
-pragma solidity 0.8.21;
+pragma solidity 0.8.19;
 
 import "../../src/Morpho.sol";
 import "../../src/libraries/SharesMathLib.sol";
-import "../../src/libraries/MarketLib.sol";
+import "../../src/libraries/MarketParamsLib.sol";
 
 contract MorphoHarness is Morpho {
-    using MarketLib for Market;
+    using MarketParamsLib for MarketParams;
 
     constructor(address newOwner) Morpho(newOwner) {}
 
@@ -25,24 +25,66 @@ contract MorphoHarness is Morpho {
         return MAX_FEE;
     }
 
-    function getVirtualTotalSupply(Id id) external view returns (uint256) {
-        return totalSupply[id] + SharesMathLib.VIRTUAL_ASSETS;
+    function getTotalSupplyAssets(Id id) external view returns (uint256) {
+        return market[id].totalSupplyAssets;
+    }
+
+    function getTotalSupplyShares(Id id) external view returns (uint256) {
+        return market[id].totalSupplyShares;
+    }
+
+    function getTotalBorrowAssets(Id id) external view returns (uint256) {
+        return market[id].totalBorrowAssets;
+    }
+
+    function getTotalBorrowShares(Id id) external view returns (uint256) {
+        return market[id].totalBorrowShares;
+    }
+
+    function getSupplyShares(Id id, address account) external view returns (uint256) {
+        return position[id][account].supplyShares;
+    }
+
+    function getBorrowShares(Id id, address account) external view returns (uint256) {
+        return position[id][account].borrowShares;
+    }
+
+    function getCollateral(Id id, address account) external view returns (uint256) {
+        return position[id][account].collateral;
+    }
+
+    function getLastUpdate(Id id) external view returns (uint256) {
+        return market[id].lastUpdate;
+    }
+
+    function getFee(Id id) external view returns (uint256) {
+        return market[id].fee;
+    }
+
+    function getVirtualTotalSupplyAssets(Id id) external view returns (uint256) {
+        return market[id].totalSupplyAssets + SharesMathLib.VIRTUAL_ASSETS;
     }
 
     function getVirtualTotalSupplyShares(Id id) external view returns (uint256) {
-        return totalSupplyShares[id] + SharesMathLib.VIRTUAL_SHARES;
+        return market[id].totalSupplyShares + SharesMathLib.VIRTUAL_SHARES;
     }
 
-    function getVirtualTotalBorrow(Id id) external view returns (uint256) {
-        return totalBorrow[id] + SharesMathLib.VIRTUAL_ASSETS;
+    function getVirtualTotalBorrowAssets(Id id) external view returns (uint256) {
+        return market[id].totalBorrowAssets + SharesMathLib.VIRTUAL_ASSETS;
     }
 
     function getVirtualTotalBorrowShares(Id id) external view returns (uint256) {
-        return totalBorrowShares[id] + SharesMathLib.VIRTUAL_SHARES;
+        return market[id].totalBorrowShares + SharesMathLib.VIRTUAL_SHARES;
     }
 
-    function getMarketId(Market memory market) external pure returns (Id) {
-        return market.id();
+    function getMarketId(MarketParams memory marketParams) external pure returns (Id) {
+        return marketParams.id();
+    }
+
+    function marketLibId(MarketParams memory marketParams) external pure returns (Id marketParamsId) {
+        assembly ("memory-safe") {
+            marketParamsId := keccak256(marketParams, mul(5, 32))
+        }
     }
 
     function mathLibMulDivUp(uint256 x, uint256 y, uint256 d) public pure returns (uint256) {
@@ -53,7 +95,14 @@ contract MorphoHarness is Morpho {
         return MathLib.mulDivDown(x, y, d);
     }
 
-    function isHealthy(Market memory market, address user) external view returns (bool) {
-        return _isHealthy(market, market.id(), user);
+    function accrueInterest(MarketParams memory marketParams) external {
+        Id id = marketParams.id();
+        require(market[id].lastUpdate != 0, ErrorsLib.MARKET_NOT_CREATED);
+
+        _accrueInterest(marketParams, id);
+    }
+
+    function isHealthy(MarketParams memory marketParams, address user) external view returns (bool) {
+        return _isHealthy(marketParams, marketParams.id(), user);
     }
 }
diff --git a/...ora/scripts/verifyBlueRatioMathSummary.sh → certora/scripts/verifyBlueLibSummary.sh b/...ora/scripts/verifyBlueRatioMathSummary.sh → certora/scripts/verifyBlueLibSummary.sh
@@ -2,6 +2,6 @@
 
 certoraRun \
     certora/harness/MorphoHarness.sol \
-    --verify MorphoHarness:certora/specs/BlueRatioMathSummary.spec \
+    --verify MorphoHarness:certora/specs/BlueLibSummary.spec \
     --msg "Morpho Ratio Math Summary" \
     "$@"
diff --git a/certora/scripts/verifyDifficultMath.sh b/certora/scripts/verifyDifficultMath.sh
@@ -8,5 +8,6 @@ certoraRun \
     --verify MorphoHarness:certora/specs/DifficultMath.spec \
     --loop_iter 3 \
     --optimistic_loop \
+    --prover_args '-smt_hashingScheme plaininjectivity' \
     --msg "Morpho Difficult Math" \
     "$@"
diff --git a/certora/scripts/verifyHealth.sh b/certora/scripts/verifyHealth.sh
@@ -8,5 +8,6 @@ certoraRun \
     --verify MorphoHarness:certora/specs/Health.spec \
     --loop_iter 3 \
     --optimistic_loop \
+    --prover_args '-smt_hashingScheme plaininjectivity' \
     --msg "Morpho Health Check" \
     "$@"
-Original file line number
+Diff line change
@@ Expand Up / @@ -44,8 +44,6 @@ contract ERC20NoRevert { @@
         }
         function approve(address _spender, uint256 _amount) public {
-            require(!((_amount != 0) && (allowed[msg.sender][_spender] != 0)));
             allowed[msg.sender][_spender] = _amount;
         }
@@ Expand Down @@