Merge pull request #700 from morpho-org/colin@verif/add-morpho-harnes…

…s-getters

[Certora] Improve utility functions access

certora/confs/AccrueInterest.conf

@@ -1,6 +1,7 @@
 {
   "files": [
-    "certora/harness/MorphoHarness.sol"
+    "certora/harness/MorphoHarness.sol",
+    "certora/harness/Util.sol"
   ],
   "solc": "solc-0.8.19",
   "verify": "MorphoHarness:certora/specs/AccrueInterest.spec",

certora/confs/AssetsAccounting.conf

@@ -1,6 +1,7 @@
 {
   "files": [
-    "certora/harness/MorphoHarness.sol"
+    "certora/harness/MorphoHarness.sol",
+    "certora/harness/Util.sol"
   ],
   "solc": "solc-0.8.19",
   "verify": "MorphoHarness:certora/specs/AssetsAccounting.spec",

certora/confs/ConsistentState.conf

@@ -1,6 +1,7 @@
 {
   "files": [
-    "certora/harness/MorphoHarness.sol"
+    "certora/harness/MorphoHarness.sol",
+    "certora/harness/Util.sol"
   ],
   "solc": "solc-0.8.19",
   "verify": "MorphoHarness:certora/specs/ConsistentState.spec",

certora/confs/ExactMath.conf

@@ -1,6 +1,7 @@
 {
   "files": [
-    "certora/harness/MorphoHarness.sol"
+    "certora/harness/MorphoHarness.sol",
+    "certora/harness/Util.sol"
   ],
   "solc": "solc-0.8.19",
   "verify": "MorphoHarness:certora/specs/ExactMath.spec",

certora/confs/ExchangeRate.conf

@@ -1,6 +1,7 @@
 {
   "files": [
-    "certora/harness/MorphoHarness.sol"
+    "certora/harness/MorphoHarness.sol",
+    "certora/harness/Util.sol"
   ],
   "solc": "solc-0.8.19",
   "verify": "MorphoHarness:certora/specs/ExchangeRate.spec",

certora/confs/Health.conf

@@ -1,6 +1,7 @@
 {
   "files": [
     "certora/harness/MorphoHarness.sol",
+    "certora/harness/Util.sol",
     "src/mocks/OracleMock.sol"
   ],
   "solc": "solc-0.8.19",

certora/confs/LibSummary.conf

@@ -1,6 +1,7 @@
 {
   "files": [
-    "certora/harness/MorphoHarness.sol"
+    "certora/harness/MorphoHarness.sol",
+    "certora/harness/Util.sol"
   ],
   "solc": "solc-0.8.19",
   "verify": "MorphoHarness:certora/specs/LibSummary.spec",

certora/confs/Liveness.conf

@@ -1,6 +1,7 @@
 {
   "files": [
-    "certora/harness/MorphoInternalAccess.sol"
+    "certora/harness/MorphoInternalAccess.sol",
+    "certora/harness/Util.sol"
   ],
   "solc": "solc-0.8.19",
   "verify": "MorphoInternalAccess:certora/specs/Liveness.spec",

certora/confs/Reverts.conf

@@ -1,6 +1,7 @@
 {
   "files": [
-    "certora/harness/MorphoHarness.sol"
+    "certora/harness/MorphoHarness.sol",
+    "certora/harness/Util.sol"
   ],
   "solc": "solc-0.8.19",
   "verify": "MorphoHarness:certora/specs/Reverts.spec",

certora/confs/StayHealthy.conf

@@ -1,6 +1,7 @@
 {
   "files": [
     "certora/harness/MorphoHarness.sol",
+    "certora/harness/Util.sol",
     "src/mocks/OracleMock.sol"
   ],
   "solc": "solc-0.8.19",

certora/harness/MorphoHarness.sol

@@ -10,16 +10,16 @@ contract MorphoHarness is Morpho {
 
     constructor(address newOwner) Morpho(newOwner) {}
 
-    function wad() external pure returns (uint256) {
-        return WAD;
+    function idToMarketParams_(Id id) external view returns (MarketParams memory) {
+        return idToMarketParams[id];
     }
 
-    function maxFee() external pure returns (uint256) {
-        return MAX_FEE;
+    function market_(Id id) external view returns (Market memory) {
+        return market[id];
     }
 
-    function toMarketParams(Id id) external view returns (MarketParams memory) {
-        return idToMarketParams[id];
+    function position_(Id id, address user) external view returns (Position memory) {
+        return position[id][user];
     }
 
     function totalSupplyAssets(Id id) external view returns (uint256) {
@@ -74,26 +74,6 @@ contract MorphoHarness is Morpho {
         return market[id].totalBorrowShares + SharesMathLib.VIRTUAL_SHARES;
     }
 
-    function libId(MarketParams memory marketParams) external pure returns (Id) {
-        return marketParams.id();
-    }
-
-    function refId(MarketParams memory marketParams) external pure returns (Id marketParamsId) {
-        marketParamsId = Id.wrap(keccak256(abi.encode(marketParams)));
-    }
-
-    function libMulDivUp(uint256 x, uint256 y, uint256 d) external pure returns (uint256) {
-        return MathLib.mulDivUp(x, y, d);
-    }
-
-    function libMulDivDown(uint256 x, uint256 y, uint256 d) external pure returns (uint256) {
-        return MathLib.mulDivDown(x, y, d);
-    }
-
-    function libMin(uint256 x, uint256 y) external pure returns (uint256) {
-        return UtilsLib.min(x, y);
-    }
-
     function isHealthy(MarketParams memory marketParams, address user) external view returns (bool) {
         return _isHealthy(marketParams, marketParams.id(), user);
     }

certora/harness/Util.sol

@@ -0,0 +1,39 @@
+// SPDX-License-Identifier: GPL-2.0-or-later
+pragma solidity 0.8.19;
+
+import {Id, MarketParams, MarketParamsLib} from "../../src/libraries/MarketParamsLib.sol";
+import "../../src/libraries/MathLib.sol";
+import "../../src/libraries/ConstantsLib.sol";
+import "../../src/libraries/UtilsLib.sol";
+
+contract Util {
+    using MarketParamsLib for MarketParams;
+
+    function wad() external pure returns (uint256) {
+        return WAD;
+    }
+
+    function maxFee() external pure returns (uint256) {
+        return MAX_FEE;
+    }
+
+    function libId(MarketParams memory marketParams) external pure returns (Id) {
+        return marketParams.id();
+    }
+
+    function refId(MarketParams memory marketParams) external pure returns (Id marketParamsId) {
+        marketParamsId = Id.wrap(keccak256(abi.encode(marketParams)));
+    }
+
+    function libMulDivUp(uint256 x, uint256 y, uint256 d) external pure returns (uint256) {
+        return MathLib.mulDivUp(x, y, d);
+    }
+
+    function libMulDivDown(uint256 x, uint256 y, uint256 d) external pure returns (uint256) {
+        return MathLib.mulDivDown(x, y, d);
+    }
+
+    function libMin(uint256 x, uint256 y) external pure returns (uint256) {
+        return UtilsLib.min(x, y);
+    }
+}

certora/specs/AccrueInterest.spec

@@ -2,7 +2,7 @@
 methods {
     function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE;
 
-    function maxFee() external returns uint256 envfree;
+    function Util.maxFee() external returns uint256 envfree;
 
     function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => ghostMulDivDown(a,b,c);
     function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal returns uint256 => ghostMulDivUp(a,b,c);

certora/specs/AssetsAccounting.spec

@@ -1,4 +1,7 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
+
+using Util as Util;
+
 methods {
     function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE;
 
@@ -13,30 +16,30 @@ methods {
     function virtualTotalBorrowShares(MorphoHarness.Id) external returns uint256 envfree;
     function lastUpdate(MorphoHarness.Id) external returns uint256 envfree;
 
-    function libMulDivDown(uint256, uint256, uint256) external returns uint256 envfree;
-    function libMulDivUp(uint256, uint256, uint256) external returns uint256 envfree;
-    function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
+    function Util.libMulDivDown(uint256, uint256, uint256) external returns uint256 envfree;
+    function Util.libMulDivUp(uint256, uint256, uint256) external returns uint256 envfree;
+    function Util.libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
 }
 
 function expectedSupplyAssets(MorphoHarness.Id id, address user) returns uint256 {
     uint256 userShares = supplyShares(id, user);
     uint256 totalSupplyAssets = virtualTotalSupplyAssets(id);
     uint256 totalSupplyShares = virtualTotalSupplyShares(id);
 
-    return libMulDivDown(userShares, totalSupplyAssets, totalSupplyShares);
+    return Util.libMulDivDown(userShares, totalSupplyAssets, totalSupplyShares);
 }
 
 function expectedBorrowAssets(MorphoHarness.Id id, address user) returns uint256 {
     uint256 userShares = borrowShares(id, user);
     uint256 totalBorrowAssets = virtualTotalBorrowAssets(id);
     uint256 totalBorrowShares = virtualTotalBorrowShares(id);
 
-    return libMulDivUp(userShares, totalBorrowAssets, totalBorrowShares);
+    return Util.libMulDivUp(userShares, totalBorrowAssets, totalBorrowShares);
 }
 
 // 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);
+    MorphoHarness.Id id = Util.libId(marketParams);
 
     // Assume no interest as it would increase the total supply assets.
     require lastUpdate(id) == e.block.timestamp;
@@ -55,7 +58,7 @@ rule supplyAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint
 
 // Check that the assets withdrawn are less than the assets owned initially.
 rule withdrawAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) {
-    MorphoHarness.Id id = libId(marketParams);
+    MorphoHarness.Id id = Util.libId(marketParams);
 
     // Assume no interest as it would increase the total supply assets.
     require lastUpdate(id) == e.block.timestamp;
@@ -70,7 +73,7 @@ rule withdrawAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, ui
 
 // 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);
+    MorphoHarness.Id id = Util.libId(marketParams);
 
     // Assume no interest as it would increase the total borrowed assets.
     require lastUpdate(id) == e.block.timestamp;
@@ -90,7 +93,7 @@ rule borrowAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint
 
 // Check that the assets repaid are greater than the assets owed initially.
 rule repayAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) {
-    MorphoHarness.Id id = libId(marketParams);
+    MorphoHarness.Id id = Util.libId(marketParams);
 
     // Assume no interest as it would increase the total borrowed assets.
     require lastUpdate(id) == e.block.timestamp;
@@ -108,7 +111,7 @@ rule repayAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint2
 
 // 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);
+    MorphoHarness.Id id = Util.libId(marketParams);
 
     uint256 ownedAssetsBefore = collateral(id, onBehalf);
 
@@ -121,7 +124,7 @@ rule supplyCollateralAssetsAccounting(env e, MorphoHarness.MarketParams marketPa
 
 // Check that the collateral assets withdrawn are less than the assets owned initially.
 rule withdrawCollateralAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 withdrawnAssets, address onBehalf, address receiver) {
-    MorphoHarness.Id id = libId(marketParams);
+    MorphoHarness.Id id = Util.libId(marketParams);
 
     uint256 ownedAssets = collateral(id, onBehalf);
 

certora/specs/ConsistentState.spec

@@ -1,4 +1,7 @@
 // SPDX-License-Identifier: GPL-2.0-or-later
+
+using Util as Util;
+
 methods {
     function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE;
 
@@ -14,11 +17,11 @@ methods {
     function isIrmEnabled(address) external returns bool envfree;
     function isLltvEnabled(uint256) external returns bool envfree;
     function isAuthorized(address, address) external returns bool envfree;
-    function toMarketParams(MorphoHarness.Id) external returns MorphoHarness.MarketParams envfree;
+    function idToMarketParams_(MorphoHarness.Id) external returns MorphoHarness.MarketParams envfree;
 
-    function maxFee() external returns uint256 envfree;
-    function wad() external returns uint256 envfree;
-    function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
+    function Util.maxFee() external returns uint256 envfree;
+    function Util.wad() external returns uint256 envfree;
+    function Util.libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree;
 
     function _.borrowRate(MorphoHarness.MarketParams, MorphoHarness.Market) external => HAVOC_ECF;
 
@@ -56,15 +59,15 @@ hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].borrowShares ui
 
 hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].collateral uint128 newAmount (uint128 oldAmount) {
     sumCollateral[id] = sumCollateral[id] - oldAmount + newAmount;
-    idleAmount[toMarketParams(id).collateralToken] = idleAmount[toMarketParams(id).collateralToken] - oldAmount + newAmount;
+    idleAmount[idToMarketParams_(id).collateralToken] = idleAmount[idToMarketParams_(id).collateralToken] - oldAmount + newAmount;
 }
 
 hook Sstore market[KEY MorphoHarness.Id id].totalSupplyAssets uint128 newAmount (uint128 oldAmount) {
-    idleAmount[toMarketParams(id).loanToken] = idleAmount[toMarketParams(id).loanToken] - oldAmount + newAmount;
+    idleAmount[idToMarketParams_(id).loanToken] = idleAmount[idToMarketParams_(id).loanToken] - oldAmount + newAmount;
 }
 
 hook Sstore market[KEY MorphoHarness.Id id].totalBorrowAssets uint128 newAmount (uint128 oldAmount) {
-    idleAmount[toMarketParams(id).loanToken] = idleAmount[toMarketParams(id).loanToken] + oldAmount - newAmount;
+    idleAmount[idToMarketParams_(id).loanToken] = idleAmount[idToMarketParams_(id).loanToken] + oldAmount - newAmount;
 }
 
 function summarySafeTransferFrom(address token, address from, address to, uint256 amount) {
@@ -83,7 +86,7 @@ definition isCreated(MorphoHarness.Id id) returns bool =
 
 // Check that the fee is always lower than the max fee constant.
 invariant feeInRange(MorphoHarness.Id id)
-    fee(id) <= maxFee();
+    fee(id) <= Util.maxFee();
 
 // Check that the accounting of totalSupplyShares is correct.
 invariant sumSupplySharesCorrect(MorphoHarness.Id id)
@@ -101,13 +104,13 @@ invariant borrowLessThanSupply(MorphoHarness.Id id)
 // Check correctness of applying idToMarketParams() to an identifier.
 invariant hashOfMarketParamsOf(MorphoHarness.Id id)
     isCreated(id) =>
-    libId(toMarketParams(id)) == id;
+    Util.libId(idToMarketParams_(id)) == id;
 
 // Check correctness of applying id() to a market params.
 // This invariant is useful in the following rule, to link an id back to a market.
 invariant marketParamsOfHashOf(MorphoHarness.MarketParams marketParams)
-    isCreated(libId(marketParams)) =>
-    toMarketParams(libId(marketParams)) == marketParams;
+    isCreated(Util.libId(marketParams)) =>
+    idToMarketParams_(Util.libId(marketParams)) == marketParams;
 
 // Check that the idle amount on the singleton is greater to the sum amount, that is the sum over all the markets of the total supply plus the total collateral minus the total borrow.
 invariant idleAmountLessThanBalance(address token)
@@ -146,22 +149,22 @@ invariant idleAmountLessThanBalance(address token)
 
 // Check that a market can only exist if its LLTV is enabled.
 invariant onlyEnabledLltv(MorphoHarness.MarketParams marketParams)
-    isCreated(libId(marketParams)) => isLltvEnabled(marketParams.lltv);
+    isCreated(Util.libId(marketParams)) => isLltvEnabled(marketParams.lltv);
 
 invariant lltvSmallerThanWad(uint256 lltv)
-    isLltvEnabled(lltv) => lltv < wad();
+    isLltvEnabled(lltv) => lltv < Util.wad();
 
 // Check that a market can only exist if its IRM is enabled.
 invariant onlyEnabledIrm(MorphoHarness.MarketParams marketParams)
-    isCreated(libId(marketParams)) => isIrmEnabled(marketParams.irm);
+    isCreated(Util.libId(marketParams)) => isIrmEnabled(marketParams.irm);
 
 // Check the pseudo-injectivity of the hashing function id().
 rule libIdUnique() {
     MorphoHarness.MarketParams marketParams1;
     MorphoHarness.MarketParams marketParams2;
 
     // Assume that arguments are the same.
-    require libId(marketParams1) == libId(marketParams2);
+    require Util.libId(marketParams1) == Util.libId(marketParams2);
 
     assert marketParams1 == marketParams2;
 }