diff --git a/certora/confs/AccrueInterest.conf b/certora/confs/AccrueInterest.conf index 3841d32c..8d4706d1 100644 --- a/certora/confs/AccrueInterest.conf +++ b/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", diff --git a/certora/confs/AssetsAccounting.conf b/certora/confs/AssetsAccounting.conf index 72e3e20e..765e597b 100644 --- a/certora/confs/AssetsAccounting.conf +++ b/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", diff --git a/certora/confs/ConsistentState.conf b/certora/confs/ConsistentState.conf index a3749723..8e7cdaca 100644 --- a/certora/confs/ConsistentState.conf +++ b/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", diff --git a/certora/confs/ExactMath.conf b/certora/confs/ExactMath.conf index 7a82fca5..2894ce6e 100644 --- a/certora/confs/ExactMath.conf +++ b/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", diff --git a/certora/confs/ExchangeRate.conf b/certora/confs/ExchangeRate.conf index 5a549a5e..2c6efcc2 100644 --- a/certora/confs/ExchangeRate.conf +++ b/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", diff --git a/certora/confs/Health.conf b/certora/confs/Health.conf index 0b47d05a..e052dfcf 100644 --- a/certora/confs/Health.conf +++ b/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", diff --git a/certora/confs/LibSummary.conf b/certora/confs/LibSummary.conf index 34526a1f..61414e22 100644 --- a/certora/confs/LibSummary.conf +++ b/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", diff --git a/certora/confs/Liveness.conf b/certora/confs/Liveness.conf index f9196903..5c438af5 100644 --- a/certora/confs/Liveness.conf +++ b/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", diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf index c1d6dadc..a54d3bfd 100644 --- a/certora/confs/Reverts.conf +++ b/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", diff --git a/certora/confs/StayHealthy.conf b/certora/confs/StayHealthy.conf index 1854fdbc..dc605cf1 100644 --- a/certora/confs/StayHealthy.conf +++ b/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", diff --git a/certora/harness/MorphoHarness.sol b/certora/harness/MorphoHarness.sol index ff504632..ce62eb35 100644 --- a/certora/harness/MorphoHarness.sol +++ b/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); } diff --git a/certora/harness/Util.sol b/certora/harness/Util.sol new file mode 100644 index 00000000..cef51dea --- /dev/null +++ b/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); + } +} diff --git a/certora/specs/AccrueInterest.spec b/certora/specs/AccrueInterest.spec index 7babf38d..74f986ee 100644 --- a/certora/specs/AccrueInterest.spec +++ b/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); diff --git a/certora/specs/AssetsAccounting.spec b/certora/specs/AssetsAccounting.spec index 7071f17d..4006eb4c 100644 --- a/certora/specs/AssetsAccounting.spec +++ b/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,9 +16,9 @@ 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 { @@ -23,7 +26,7 @@ function expectedSupplyAssets(MorphoHarness.Id id, address user) returns uint256 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 { @@ -31,12 +34,12 @@ function expectedBorrowAssets(MorphoHarness.Id id, address user) returns uint256 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); diff --git a/certora/specs/ConsistentState.spec b/certora/specs/ConsistentState.spec index 22a787a2..2d8dc466 100644 --- a/certora/specs/ConsistentState.spec +++ b/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,14 +149,14 @@ 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() { @@ -161,7 +164,7 @@ rule libIdUnique() { MorphoHarness.MarketParams marketParams2; // Assume that arguments are the same. - require libId(marketParams1) == libId(marketParams2); + require Util.libId(marketParams1) == Util.libId(marketParams2); assert marketParams1 == marketParams2; } diff --git a/certora/specs/ExactMath.spec b/certora/specs/ExactMath.spec index eedc9f04..25458817 100644 --- a/certora/specs/ExactMath.spec +++ b/certora/specs/ExactMath.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; @@ -12,8 +15,8 @@ methods { function lastUpdate(MorphoHarness.Id) external returns uint256 envfree; function fee(MorphoHarness.Id) external returns uint256 envfree; - function maxFee() external returns uint256 envfree; - function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; + function Util.maxFee() external returns uint256 envfree; + function Util.libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivDown(a,b,c); function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivUp(a,b,c); @@ -35,9 +38,9 @@ function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 { // Check that when not accruing interest, and when repaying all, the borrow exchange rate is at least reset to the initial exchange rate. // More details on the purpose of this rule in ExchangeRate.spec. rule repayAllResetsBorrowExchangeRate(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { - MorphoHarness.Id id = libId(marketParams); + MorphoHarness.Id id = Util.libId(marketParams); // Safe require because this invariant is checked in ConsistentState.spec - require fee(id) <= maxFee(); + require fee(id) <= Util.maxFee(); mathint assetsBefore = virtualTotalBorrowAssets(id); mathint sharesBefore = virtualTotalBorrowShares(id); @@ -61,7 +64,7 @@ rule repayAllResetsBorrowExchangeRate(env e, MorphoHarness.MarketParams marketPa // There should be no profit from supply followed immediately by withdraw. rule supplyWithdraw() { MorphoHarness.MarketParams marketParams; - MorphoHarness.Id id = libId(marketParams); + MorphoHarness.Id id = Util.libId(marketParams); env e1; env e2; address onBehalf; @@ -94,7 +97,7 @@ rule supplyWithdraw() { // There should be no profit from borrow followed immediately by repaying all. rule borrowRepay() { MorphoHarness.MarketParams marketParams; - MorphoHarness.Id id = libId(marketParams); + MorphoHarness.Id id = Util.libId(marketParams); address onBehalf; env e1; env e2; diff --git a/certora/specs/ExchangeRate.spec b/certora/specs/ExchangeRate.spec index 7598afee..e2ae790c 100644 --- a/certora/specs/ExchangeRate.spec +++ b/certora/specs/ExchangeRate.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; @@ -10,8 +13,8 @@ methods { function fee(MorphoHarness.Id) external returns uint256 envfree; function lastUpdate(MorphoHarness.Id) external returns uint256 envfree; - function maxFee() external returns uint256 envfree; - function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; + function Util.maxFee() external returns uint256 envfree; + function Util.libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; function UtilsLib.min(uint256 x, uint256 y) internal returns uint256 => summaryMin(x, y); function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivDown(a,b,c); @@ -23,7 +26,7 @@ methods { } invariant feeInRange(MorphoHarness.Id id) - fee(id) <= maxFee(); + fee(id) <= Util.maxFee(); function summaryMin(uint256 x, uint256 y) returns uint256 { return x < y ? x : y; @@ -165,7 +168,7 @@ filtered { // The other case requires exact math (ie not over-approximating mulDivUp and mulDivDown), so it is checked separately in ExactMath.spec. rule repayDecreasesBorrowExchangeRate(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { - MorphoHarness.Id id = libId(marketParams); + MorphoHarness.Id id = Util.libId(marketParams); requireInvariant feeInRange(id); mathint assetsBefore = virtualTotalBorrowAssets(id); @@ -191,7 +194,7 @@ rule repayDecreasesBorrowExchangeRate(env e, MorphoHarness.MarketParams marketPa rule liquidateDecreasesBorrowExchangeRate(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, uint256 repaidShares, bytes data) { require data.length == 0; - MorphoHarness.Id id = libId(marketParams); + MorphoHarness.Id id = Util.libId(marketParams); mathint assetsBefore = virtualTotalBorrowAssets(id); mathint sharesBefore = virtualTotalBorrowShares(id); diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec index cb764b01..28fed1d8 100644 --- a/certora/specs/Health.spec +++ b/certora/specs/Health.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; @@ -12,7 +15,7 @@ methods { function isAuthorized(address, address user) external returns bool envfree; function lastUpdate(MorphoHarness.Id) external returns uint256 envfree; - function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; + function Util.libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; function isHealthy(MorphoHarness.MarketParams, address user) external returns bool envfree; function _.price() external => mockPrice() expect uint256; @@ -54,7 +57,7 @@ rule healthyUserCannotLoseCollateral(env e, method f, calldataarg data) filtered { f -> !f.isView } { MorphoHarness.MarketParams marketParams; - MorphoHarness.Id id = libId(marketParams); + MorphoHarness.Id id = Util.libId(marketParams); address user; // Assume that the e.msg.sender is not authorized. @@ -81,7 +84,7 @@ invariant alwaysCollateralized(MorphoHarness.Id id, address borrower) // Checks that passing a seized amount input to liquidate leads to repaid shares S and repaid amount A such that liquidating instead with shares S also repays the amount A. rule liquidateEquivalentInputDebtAndInputCollateral(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) { - MorphoHarness.Id id = libId(marketParams); + MorphoHarness.Id id = Util.libId(marketParams); // Assume no interest accrual to ease the verification. require lastUpdate(id) == e.block.timestamp; diff --git a/certora/specs/LibSummary.spec b/certora/specs/LibSummary.spec index 984d68dc..1d2e8dc0 100644 --- a/certora/specs/LibSummary.spec +++ b/certora/specs/LibSummary.spec @@ -1,32 +1,35 @@ // SPDX-License-Identifier: GPL-2.0-or-later + +using Util as Util; + methods { function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; - function libMulDivUp(uint256, uint256, uint256) external returns uint256 envfree; - function libMulDivDown(uint256, uint256, uint256) external returns uint256 envfree; - function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; - function refId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; - function libMin(uint256 x, uint256 y) external returns uint256 envfree; + function Util.libMulDivUp(uint256, uint256, uint256) external returns uint256 envfree; + function Util.libMulDivDown(uint256, uint256, uint256) external returns uint256 envfree; + function Util.libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; + function Util.refId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; + function Util.libMin(uint256 x, uint256 y) external returns uint256 envfree; } // Check the summary of MathLib.mulDivUp required by ExchangeRate.spec rule checkSummaryMulDivUp(uint256 x, uint256 y, uint256 d) { - uint256 result = libMulDivUp(x, y, d); + uint256 result = Util.libMulDivUp(x, y, d); assert result * d >= x * y; } // Check the summary of MathLib.mulDivDown required by ExchangeRate.spec rule checkSummaryMulDivDown(uint256 x, uint256 y, uint256 d) { - uint256 result = libMulDivDown(x, y, d); + uint256 result = Util.libMulDivDown(x, y, d); assert result * d <= x * y; } // Check the summary of MarketParamsLib.id required by Liveness.spec rule checkSummaryId(MorphoHarness.MarketParams marketParams) { - assert libId(marketParams) == refId(marketParams); + assert Util.libId(marketParams) == Util.refId(marketParams); } rule checkSummaryMin(uint256 x, uint256 y) { uint256 refMin = x < y ? x : y; - assert libMin(x, y) == refMin; + assert Util.libMin(x, y) == refMin; } diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec index e6a78ed6..8ef6f5cb 100644 --- a/certora/specs/Liveness.spec +++ b/certora/specs/Liveness.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; function supplyShares(MorphoInternalAccess.Id, address) external returns uint256 envfree; @@ -13,8 +16,8 @@ methods { function nonce(address) external returns uint256 envfree; function isAuthorized(address, address) external returns bool envfree; - function libId(MorphoInternalAccess.MarketParams) external returns MorphoInternalAccess.Id envfree; - function refId(MorphoInternalAccess.MarketParams) external returns MorphoInternalAccess.Id envfree; + function Util.libId(MorphoInternalAccess.MarketParams) external returns MorphoInternalAccess.Id envfree; + function Util.refId(MorphoInternalAccess.MarketParams) external returns MorphoInternalAccess.Id envfree; function _._accrueInterest(MorphoInternalAccess.MarketParams memory marketParams, MorphoInternalAccess.Id id) internal with (env e) => summaryAccrueInterest(e, marketParams, id) expect void; @@ -28,7 +31,7 @@ persistent ghost mapping(address => mathint) balance { } function summaryId(MorphoInternalAccess.MarketParams marketParams) returns MorphoInternalAccess.Id { - return refId(marketParams); + return Util.refId(marketParams); } function summarySafeTransferFrom(address token, address from, address to, uint256 amount) { @@ -67,7 +70,7 @@ definition isCreated(MorphoInternalAccess.Id id) returns bool = // Check that tokens and shares are properly accounted following a supply. rule supplyChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { - MorphoInternalAccess.Id id = libId(marketParams); + MorphoInternalAccess.Id id = Util.libId(marketParams); // Safe require because Morpho cannot call such functions by itself. require currentContract != e.msg.sender; @@ -103,7 +106,7 @@ rule canSupplyByPassingShares(env e, MorphoInternalAccess.MarketParams marketPar // Check that tokens and shares are properly accounted following a withdraw. rule withdrawChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) { - MorphoInternalAccess.Id id = libId(marketParams); + MorphoInternalAccess.Id id = Util.libId(marketParams); // Assume that Morpho is not the receiver. require currentContract != receiver; @@ -139,7 +142,7 @@ rule canWithdrawByPassingShares(env e, MorphoInternalAccess.MarketParams marketP // Check that tokens and shares are properly accounted following a borrow. rule borrowChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) { - MorphoInternalAccess.Id id = libId(marketParams); + MorphoInternalAccess.Id id = Util.libId(marketParams); // Assume that Morpho is not the receiver. require currentContract != receiver; @@ -175,7 +178,7 @@ rule canBorrowByPassingShares(env e, MorphoInternalAccess.MarketParams marketPar // Check that tokens and shares are properly accounted following a repay. rule repayChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { - MorphoInternalAccess.Id id = libId(marketParams); + MorphoInternalAccess.Id id = Util.libId(marketParams); // Safe require because Morpho cannot call such functions by itself. require currentContract != e.msg.sender; @@ -214,7 +217,7 @@ rule canRepayByPassingShares(env e, MorphoInternalAccess.MarketParams marketPara // Check that tokens and balances are properly accounted following a supplyCollateral. rule supplyCollateralChangesTokensAndBalance(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, address onBehalf, bytes data) { - MorphoInternalAccess.Id id = libId(marketParams); + MorphoInternalAccess.Id id = Util.libId(marketParams); // Safe require because Morpho cannot call such functions by itself. require currentContract != e.msg.sender; @@ -233,7 +236,7 @@ rule supplyCollateralChangesTokensAndBalance(env e, MorphoInternalAccess.MarketP // Check that tokens and balances are properly accounted following a withdrawCollateral. rule withdrawCollateralChangesTokensAndBalance(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, address onBehalf, address receiver) { - MorphoInternalAccess.Id id = libId(marketParams); + MorphoInternalAccess.Id id = Util.libId(marketParams); // Assume that Morpho is not the receiver. require currentContract != receiver; @@ -254,7 +257,7 @@ rule withdrawCollateralChangesTokensAndBalance(env e, MorphoInternalAccess.Marke // Check that tokens are properly accounted following a liquidate. rule liquidateChangesTokens(env e, MorphoInternalAccess.MarketParams marketParams, address borrower, uint256 seized, uint256 repaidShares, bytes data) { - MorphoInternalAccess.Id id = libId(marketParams); + MorphoInternalAccess.Id id = Util.libId(marketParams); // Safe require because Morpho cannot call such functions by itself. require currentContract != e.msg.sender; @@ -310,7 +313,7 @@ rule setAuthorizationWithSigChangesNonceAndAuthorizes(env e, MorphoInternalAcces // Check that one can always repay the debt in full. rule canRepayAll(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, bytes data) { - MorphoInternalAccess.Id id = libId(marketParams); + MorphoInternalAccess.Id id = Util.libId(marketParams); // Assume no callback, which still allows to repay all. require data.length == 0; @@ -341,7 +344,7 @@ rule canRepayAll(env e, MorphoInternalAccess.MarketParams marketParams, uint256 // Check the one can always withdraw all, under the condition that there are no outstanding debt on the market. rule canWithdrawAll(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, address receiver) { - MorphoInternalAccess.Id id = libId(marketParams); + MorphoInternalAccess.Id id = Util.libId(marketParams); // Assume a full withdraw. require shares == supplyShares(id, e.msg.sender); @@ -366,7 +369,7 @@ rule canWithdrawAll(env e, MorphoInternalAccess.MarketParams marketParams, uint2 // Check that a user can always withdraw all, under the condition that this user does not have an outstanding debt. // Combined with the canRepayAll rule, this ensures that a borrower can always fully exit a market. rule canWithdrawCollateralAll(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, address receiver) { - MorphoInternalAccess.Id id = libId(marketParams); + MorphoInternalAccess.Id id = Util.libId(marketParams); // Ensure a full withdrawCollateral. require assets == collateral(id, e.msg.sender); diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec index f2c6c204..d6a3a468 100644 --- a/certora/specs/Reverts.spec +++ b/certora/specs/Reverts.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,10 +17,10 @@ methods { function isAuthorized(address, address) external returns bool envfree; function nonce(address) external returns uint256 envfree; - function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; + function Util.libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; - function maxFee() external returns uint256 envfree; - function wad() external returns uint256 envfree; + function Util.maxFee() external returns uint256 envfree; + function Util.wad() external returns uint256 envfree; } definition isCreated(MorphoHarness.Id id) returns bool = @@ -81,18 +84,18 @@ rule enableLltvRevertCondition(env e, uint256 lltv) { address oldOwner = owner(); bool oldIsLltvEnabled = isLltvEnabled(lltv); enableLltv@withrevert(e, lltv); - assert lastReverted <=> e.msg.value != 0 || e.msg.sender != oldOwner || lltv >= wad() || oldIsLltvEnabled; + assert lastReverted <=> e.msg.value != 0 || e.msg.sender != oldOwner || lltv >= Util.wad() || oldIsLltvEnabled; } // Check that setFee reverts when its inputs are not validated. // setFee can also revert if the accrueInterest reverts. rule setFeeInputValidation(env e, MorphoHarness.MarketParams marketParams, uint256 newFee) { - MorphoHarness.Id id = libId(marketParams); + MorphoHarness.Id id = Util.libId(marketParams); address oldOwner = owner(); bool wasCreated = isCreated(id); setFee@withrevert(e, marketParams, newFee); bool hasReverted = lastReverted; - assert e.msg.value != 0 || e.msg.sender != oldOwner || !wasCreated || newFee > maxFee() => hasReverted; + assert e.msg.value != 0 || e.msg.sender != oldOwner || !wasCreated || newFee > Util.maxFee() => hasReverted; } // Check the revert condition for the setFeeRecipient function. @@ -105,7 +108,7 @@ rule setFeeRecipientRevertCondition(env e, address newFeeRecipient) { // Check that createMarket reverts when its input are not validated. rule createMarketInputValidation(env e, MorphoHarness.MarketParams marketParams) { - MorphoHarness.Id id = libId(marketParams); + MorphoHarness.Id id = Util.libId(marketParams); bool irmEnabled = isIrmEnabled(marketParams.irm); bool lltvEnabled = isLltvEnabled(marketParams.lltv); bool wasCreated = isCreated(id); @@ -173,7 +176,7 @@ rule setAuthorizationWithSigInputValidation(env e, MorphoHarness.Authorization a // Check that accrueInterest reverts when its inputs are not validated. rule accrueInterestInputValidation(env e, MorphoHarness.MarketParams marketParams) { - bool wasCreated = isCreated(libId(marketParams)); + bool wasCreated = isCreated(Util.libId(marketParams)); accrueInterest@withrevert(e, marketParams); assert !wasCreated => lastReverted; } diff --git a/certora/specs/StayHealthy.spec b/certora/specs/StayHealthy.spec index c92ea00e..78ace84d 100644 --- a/certora/specs/StayHealthy.spec +++ b/certora/specs/StayHealthy.spec @@ -10,7 +10,7 @@ filtered { } { MorphoHarness.MarketParams marketParams; - MorphoHarness.Id id = libId(marketParams); + MorphoHarness.Id id = Util.libId(marketParams); address user; // Assume that the position is healthy before the interaction. @@ -34,7 +34,7 @@ filtered { // - the market of the liquidation is the market of the user, see the *DifferentMarkets rule, // - there is still some borrow on the market after liquidation, see the *LastBorrow rule. rule stayHealthyLiquidate(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) { - MorphoHarness.Id id = libId(marketParams); + MorphoHarness.Id id = Util.libId(marketParams); address user; // Assume the invariant initially. @@ -67,7 +67,7 @@ rule stayHealthyLiquidate(env e, MorphoHarness.MarketParams marketParams, addres } rule stayHealthyLiquidateDifferentMarkets(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) { - MorphoHarness.Id id = libId(marketParams); + MorphoHarness.Id id = Util.libId(marketParams); address user; MorphoHarness.MarketParams liquidationMarketParams; @@ -93,7 +93,7 @@ rule stayHealthyLiquidateDifferentMarkets(env e, MorphoHarness.MarketParams mark } rule stayHealthyLiquidateLastBorrow(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) { - MorphoHarness.Id id = libId(marketParams); + MorphoHarness.Id id = Util.libId(marketParams); address user; // Assume the invariant initially.