diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 6ea3eb76d..acc163e53 100644 --- 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 index 8904f782c..ab9a3f66a 100644 --- 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 index 129e0bc42..33ae528f6 100644 --- 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/certora/scripts/verifyBlueRatioMathSummary.sh b/certora/scripts/verifyBlueLibSummary.sh similarity index 62% rename from certora/scripts/verifyBlueRatioMathSummary.sh rename to certora/scripts/verifyBlueLibSummary.sh index f0a9305b9..64f02dcb4 100755 --- a/certora/scripts/verifyBlueRatioMathSummary.sh +++ b/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 index f775a585b..b5a6618d6 100755 --- 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 index efcc770b8..e41ca696b 100755 --- 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" \ "$@" diff --git a/certora/specs/Blue.spec b/certora/specs/Blue.spec index 9fc4fe5ff..ed9f7928a 100644 --- a/certora/specs/Blue.spec +++ b/certora/specs/Blue.spec @@ -1,28 +1,21 @@ methods { - function getVirtualTotalSupply(MorphoHarness.Id) external returns uint256 envfree; - function getVirtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree; - function totalSupply(MorphoHarness.Id) external returns uint256 envfree; - function totalBorrow(MorphoHarness.Id) external returns uint256 envfree; - function supplyShares(MorphoHarness.Id, address user) external returns uint256 envfree; - function borrowShares(MorphoHarness.Id, address user) external returns uint256 envfree; - function collateral(MorphoHarness.Id, address user) external returns uint256 envfree; - function totalSupplyShares(MorphoHarness.Id) external returns uint256 envfree; - function totalBorrowShares(MorphoHarness.Id) external returns uint256 envfree; - function fee(MorphoHarness.Id) external returns uint256 envfree; - function getMarketId(MorphoHarness.Market) external returns MorphoHarness.Id envfree; - function idToMarket(MorphoHarness.Id) external returns (address, address, address, address, uint256) envfree; - function isAuthorized(address, address) external returns bool envfree; + function getTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree; + function getTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree; + function getTotalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree; + function getTotalBorrowShares(MorphoHarness.Id) external returns uint256 envfree; + function getSupplyShares(MorphoHarness.Id, address) external returns uint256 envfree; + function getBorrowShares(MorphoHarness.Id, address) external returns uint256 envfree; + function getCollateral(MorphoHarness.Id, address) external returns uint256 envfree; + function getFee(MorphoHarness.Id) external returns uint256 envfree; + function getLastUpdate(MorphoHarness.Id) external returns uint256 envfree; + function getMarketId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; - function isHealthy(MorphoHarness.Market, address user) external returns bool envfree; - function lastUpdate(MorphoHarness.Id) external returns uint256 envfree; + function isAuthorized(address, address) external returns bool envfree; function isLltvEnabled(uint256) external returns bool envfree; function isIrmEnabled(address) external returns bool envfree; - function _.borrowRate(MorphoHarness.Market) external => HAVOC_ECF; + function _.borrowRate(MorphoHarness.MarketParams, MorphoHarness.Market) external => HAVOC_ECF; - function getMarketId(MorphoHarness.Market) external returns MorphoHarness.Id envfree; - function VIRTUAL_ASSETS() external returns uint256 envfree; - function VIRTUAL_SHARES() external returns uint256 envfree; function MAX_FEE() external returns uint256 envfree; function SafeTransferLib.safeTransfer(address token, address to, uint256 value) internal => summarySafeTransferFrom(token, currentContract, to, value); @@ -32,9 +25,11 @@ methods { ghost mapping(MorphoHarness.Id => mathint) sumSupplyShares { init_state axiom (forall MorphoHarness.Id id. sumSupplyShares[id] == 0); } + ghost mapping(MorphoHarness.Id => mathint) sumBorrowShares { init_state axiom (forall MorphoHarness.Id id. sumBorrowShares[id] == 0); } + ghost mapping(MorphoHarness.Id => mathint) sumCollateral { init_state axiom (forall MorphoHarness.Id id. sumCollateral[id] == 0); } @@ -51,32 +46,32 @@ ghost mapping(MorphoHarness.Id => address) idToBorrowable; ghost mapping(MorphoHarness.Id => address) idToCollateral; -hook Sstore idToMarket[KEY MorphoHarness.Id id].borrowableToken address token STORAGE { +hook Sstore idToMarketParams[KEY MorphoHarness.Id id].borrowableToken address token STORAGE { idToBorrowable[id] = token; } -hook Sstore idToMarket[KEY MorphoHarness.Id id].collateralToken address token STORAGE { +hook Sstore idToMarketParams[KEY MorphoHarness.Id id].collateralToken address token STORAGE { idToCollateral[id] = token; } -hook Sstore supplyShares[KEY MorphoHarness.Id id][KEY address owner] uint256 newShares (uint256 oldShares) STORAGE { +hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].supplyShares uint256 newShares (uint256 oldShares) STORAGE { sumSupplyShares[id] = sumSupplyShares[id] - oldShares + newShares; } -hook Sstore borrowShares[KEY MorphoHarness.Id id][KEY address owner] uint256 newShares (uint256 oldShares) STORAGE { +hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].borrowShares uint128 newShares (uint128 oldShares) STORAGE { sumBorrowShares[id] = sumBorrowShares[id] - oldShares + newShares; } -hook Sstore collateral[KEY MorphoHarness.Id id][KEY address owner] uint256 newAmount (uint256 oldAmount) STORAGE { +hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].collateral uint128 newAmount (uint128 oldAmount) STORAGE { sumCollateral[id] = sumCollateral[id] - oldAmount + newAmount; expectedAmount[idToCollateral[id]] = expectedAmount[idToCollateral[id]] - oldAmount + newAmount; } -hook Sstore totalSupply[KEY MorphoHarness.Id id] uint256 newAmount (uint256 oldAmount) STORAGE { +hook Sstore market[KEY MorphoHarness.Id id].totalSupplyAssets uint128 newAmount (uint128 oldAmount) STORAGE { expectedAmount[idToBorrowable[id]] = expectedAmount[idToBorrowable[id]] - oldAmount + newAmount; } -hook Sstore totalBorrow[KEY MorphoHarness.Id id] uint256 newAmount (uint256 oldAmount) STORAGE { +hook Sstore market[KEY MorphoHarness.Id id].totalBorrowAssets uint128 newAmount (uint128 oldAmount) STORAGE { expectedAmount[idToBorrowable[id]] = expectedAmount[idToBorrowable[id]] + oldAmount - newAmount; } @@ -90,75 +85,75 @@ function summarySafeTransferFrom(address token, address from, address to, uint25 } definition isCreated(MorphoHarness.Id id) returns bool = - (lastUpdate(id) != 0); + getLastUpdate(id) != 0; invariant feeInRange(MorphoHarness.Id id) - fee(id) <= MAX_FEE(); + getFee(id) <= MAX_FEE(); invariant sumSupplySharesCorrect(MorphoHarness.Id id) - to_mathint(totalSupplyShares(id)) == sumSupplyShares[id]; + to_mathint(getTotalSupplyShares(id)) == sumSupplyShares[id]; invariant sumBorrowSharesCorrect(MorphoHarness.Id id) - to_mathint(totalBorrowShares(id)) == sumBorrowShares[id]; + to_mathint(getTotalBorrowShares(id)) == sumBorrowShares[id]; invariant borrowLessSupply(MorphoHarness.Id id) - totalBorrow(id) <= totalSupply(id); + getTotalBorrowAssets(id) <= getTotalSupplyAssets(id); -invariant marketInvariant(MorphoHarness.Market market) - isCreated(getMarketId(market)) => - idToBorrowable[getMarketId(market)] == market.borrowableToken - && idToCollateral[getMarketId(market)] == market.collateralToken; +invariant marketInvariant(MorphoHarness.MarketParams marketParams) + isCreated(getMarketId(marketParams)) => + idToBorrowable[getMarketId(marketParams)] == marketParams.borrowableToken && + idToCollateral[getMarketId(marketParams)] == marketParams.collateralToken; invariant isLiquid(address token) expectedAmount[token] <= myBalances[token] { - preserved supply(MorphoHarness.Market market, uint256 _a, uint256 _s, address _o, bytes _d) with (env e) { - requireInvariant marketInvariant(market); + preserved supply(MorphoHarness.MarketParams marketParams, uint256 _a, uint256 _s, address _o, bytes _d) with (env e) { + requireInvariant marketInvariant(marketParams); require e.msg.sender != currentContract; } - preserved withdraw(MorphoHarness.Market market, uint256 _a, uint256 _s, address _o, address _r) with (env e) { - requireInvariant marketInvariant(market); + preserved withdraw(MorphoHarness.MarketParams marketParams, uint256 _a, uint256 _s, address _o, address _r) with (env e) { + requireInvariant marketInvariant(marketParams); require e.msg.sender != currentContract; } - preserved borrow(MorphoHarness.Market market, uint256 _a, uint256 _s, address _o, address _r) with (env e) { - requireInvariant marketInvariant(market); + preserved borrow(MorphoHarness.MarketParams marketParams, uint256 _a, uint256 _s, address _o, address _r) with (env e) { + requireInvariant marketInvariant(marketParams); require e.msg.sender != currentContract; } - preserved repay(MorphoHarness.Market market, uint256 _a, uint256 _s, address _o, bytes _d) with (env e) { - requireInvariant marketInvariant(market); + preserved repay(MorphoHarness.MarketParams marketParams, uint256 _a, uint256 _s, address _o, bytes _d) with (env e) { + requireInvariant marketInvariant(marketParams); require e.msg.sender != currentContract; } - preserved supplyCollateral(MorphoHarness.Market market, uint256 _a, address _o, bytes _d) with (env e) { - requireInvariant marketInvariant(market); + preserved supplyCollateral(MorphoHarness.MarketParams marketParams, uint256 _a, address _o, bytes _d) with (env e) { + requireInvariant marketInvariant(marketParams); require e.msg.sender != currentContract; } - preserved withdrawCollateral(MorphoHarness.Market market, uint256 _a, address _o, address _r) with (env e) { - requireInvariant marketInvariant(market); + preserved withdrawCollateral(MorphoHarness.MarketParams marketParams, uint256 _a, address _o, address _r) with (env e) { + requireInvariant marketInvariant(marketParams); require e.msg.sender != currentContract; } - preserved liquidate(MorphoHarness.Market market, address _b, uint256 _s, bytes _d) with (env e) { - requireInvariant marketInvariant(market); + preserved liquidate(MorphoHarness.MarketParams marketParams, address _b, uint256 _s, uint256 _r, bytes _d) with (env e) { + requireInvariant marketInvariant(marketParams); require e.msg.sender != currentContract; } } -invariant onlyEnabledLltv(MorphoHarness.Market market) - isCreated(getMarketId(market)) => isLltvEnabled(market.lltv); +invariant onlyEnabledLltv(MorphoHarness.MarketParams marketParams) + isCreated(getMarketId(marketParams)) => isLltvEnabled(marketParams.lltv); -invariant onlyEnabledIrm(MorphoHarness.Market market) - isCreated(getMarketId(market)) => isIrmEnabled(market.irm); +invariant onlyEnabledIrm(MorphoHarness.MarketParams marketParams) + isCreated(getMarketId(marketParams)) => isIrmEnabled(marketParams.irm); rule marketIdUnique() { - MorphoHarness.Market market1; - MorphoHarness.Market market2; + MorphoHarness.MarketParams marketParams1; + MorphoHarness.MarketParams marketParams2; - require getMarketId(market1) == getMarketId(market2); + require getMarketId(marketParams1) == getMarketId(marketParams2); - assert market1.borrowableToken == market2.borrowableToken; - assert market1.collateralToken == market2.collateralToken; - assert market1.oracle == market2.oracle; - assert market1.irm == market2.irm; - assert market1.lltv == market2.lltv; + assert marketParams1.borrowableToken == marketParams2.borrowableToken; + assert marketParams1.collateralToken == marketParams2.collateralToken; + assert marketParams1.oracle == marketParams2.oracle; + assert marketParams1.irm == marketParams2.irm; + assert marketParams1.lltv == marketParams2.lltv; } rule onlyUserCanAuthorizeWithoutSig(method f, calldataarg data) @@ -179,139 +174,133 @@ filtered { } rule supplyMovesTokensAndIncreasesShares() { - MorphoHarness.Market market; + MorphoHarness.MarketParams marketParams; uint256 assets; uint256 shares; uint256 suppliedAssets; uint256 suppliedShares; address onbehalf; bytes data; - MorphoHarness.Id id = getMarketId(market); + MorphoHarness.Id id = getMarketId(marketParams); env e; require e.msg.sender != currentContract; - require lastUpdate(id) == e.block.timestamp; + require getLastUpdate(id) == e.block.timestamp; - mathint sharesBefore = supplyShares(id, onbehalf); - mathint balanceBefore = myBalances[market.borrowableToken]; + mathint sharesBefore = getSupplyShares(id, onbehalf); + mathint balanceBefore = myBalances[marketParams.borrowableToken]; - suppliedAssets, suppliedShares = supply(e, market, assets, shares, onbehalf, data); + suppliedAssets, suppliedShares = supply(e, marketParams, assets, shares, onbehalf, data); assert assets != 0 => suppliedAssets == assets && shares == 0; assert assets == 0 => suppliedShares == shares && shares != 0; - mathint sharesAfter = supplyShares(id, onbehalf); - mathint balanceAfter = myBalances[market.borrowableToken]; + mathint sharesAfter = getSupplyShares(id, onbehalf); + mathint balanceAfter = myBalances[marketParams.borrowableToken]; assert sharesAfter == sharesBefore + suppliedShares; assert balanceAfter == balanceBefore + suppliedAssets; } rule userCannotLoseSupplyShares(method f, calldataarg data) -filtered { - f -> !f.isView -} +filtered { f -> !f.isView } { - MorphoHarness.Market market; + MorphoHarness.MarketParams marketParams; uint256 assets; uint256 shares; uint256 suppliedAssets; uint256 suppliedShares; address user; - MorphoHarness.Id id = getMarketId(market); + MorphoHarness.Id id = getMarketId(marketParams); env e; require !isAuthorized(user, e.msg.sender); require user != e.msg.sender; - mathint sharesBefore = supplyShares(id, user); + mathint sharesBefore = getSupplyShares(id, user); f(e, data); - mathint sharesAfter = supplyShares(id, user); + mathint sharesAfter = getSupplyShares(id, user); assert sharesAfter >= sharesBefore; } rule userCannotGainBorrowShares(method f, calldataarg data) -filtered { - f -> !f.isView -} +filtered { f -> !f.isView } { - MorphoHarness.Market market; + MorphoHarness.MarketParams marketParams; uint256 assets; uint256 shares; uint256 suppliedAssets; uint256 suppliedShares; address user; - MorphoHarness.Id id = getMarketId(market); + MorphoHarness.Id id = getMarketId(marketParams); env e; require !isAuthorized(user, e.msg.sender); require user != e.msg.sender; - mathint sharesBefore = borrowShares(id, user); + mathint sharesBefore = getBorrowShares(id, user); f(e, data); - mathint sharesAfter = borrowShares(id, user); + mathint sharesAfter = getBorrowShares(id, user); assert sharesAfter <= sharesBefore; } rule userWithoutBorrowCannotLoseCollateral(method f, calldataarg data) -filtered { - f -> !f.isView -} +filtered { f -> !f.isView } { - MorphoHarness.Market market; + MorphoHarness.MarketParams marketParams; uint256 assets; uint256 shares; uint256 suppliedAssets; uint256 suppliedShares; address user; - MorphoHarness.Id id = getMarketId(market); + MorphoHarness.Id id = getMarketId(marketParams); env e; require !isAuthorized(user, e.msg.sender); require user != e.msg.sender; - require borrowShares(id, user) == 0; - mathint collateralBefore = collateral(id, user); + require getBorrowShares(id, user) == 0; + mathint collateralBefore = getCollateral(id, user); f(e, data); - mathint collateralAfter = collateral(id, user); - assert borrowShares(id, user) == 0; + mathint collateralAfter = getCollateral(id, user); + assert getBorrowShares(id, user) == 0; assert collateralAfter >= collateralBefore; } -rule noTimeTravel(method f, env e, calldataarg data) filtered { - f -> !f.isView -} { +rule noTimeTravel(method f, env e, calldataarg data) +filtered { f -> !f.isView } +{ MorphoHarness.Id id; - require lastUpdate(id) <= e.block.timestamp; + require getLastUpdate(id) <= e.block.timestamp; f(e, data); - assert lastUpdate(id) <= e.block.timestamp; + assert getLastUpdate(id) <= e.block.timestamp; } rule canWithdrawAll() { - MorphoHarness.Market market; + MorphoHarness.MarketParams marketParams; uint256 withdrawnAssets; uint256 withdrawnShares; address receiver; env e; - MorphoHarness.Id id = getMarketId(market); - uint256 shares = supplyShares(id, e.msg.sender); + MorphoHarness.Id id = getMarketId(marketParams); + uint256 shares = getSupplyShares(id, e.msg.sender); require isCreated(id); require e.msg.sender != 0; require receiver != 0; require e.msg.value == 0; require shares > 0; - require totalBorrow(id) == 0; - require lastUpdate(id) <= e.block.timestamp; - require shares < totalSupplyShares(id); - require totalSupplyShares(id) < 10^40 && totalSupply(id) < 10^30; + require getTotalBorrowAssets(id) == 0; + require getLastUpdate(id) <= e.block.timestamp; + require shares < getTotalSupplyShares(id); + require getTotalSupplyShares(id) < 10^40 && getTotalSupplyAssets(id) < 10^30; - withdrawnAssets, withdrawnShares = withdraw@withrevert(e, market, 0, shares, e.msg.sender, receiver); + withdrawnAssets, withdrawnShares = withdraw@withrevert(e, marketParams, 0, shares, e.msg.sender, receiver); assert withdrawnShares == shares; assert !lastReverted, "Can withdraw all assets if nobody borrows"; diff --git a/certora/specs/BlueAccrueInterests.spec b/certora/specs/BlueAccrueInterests.spec index 2217d44e4..0ac324321 100644 --- a/certora/specs/BlueAccrueInterests.spec +++ b/certora/specs/BlueAccrueInterests.spec @@ -6,7 +6,7 @@ methods { // we assume here that all external functions will not access storage, since we cannot show // commutativity otherwise. We also need to assume that the price and borrow rate return // always the same value (and do not depend on msg.origin), so we use ghost functions for them. - function _.borrowRate(MorphoHarness.Market market) external with (env e) => ghostBorrowRate(market.irm, e.block.timestamp) expect uint256; + function _.borrowRate(MorphoHarness.MarketParams marketParams, MorphoHarness.Market market) external with (env e) => ghostBorrowRate(marketParams.irm, e.block.timestamp) expect uint256; function _.price() external with (env e) => ghostOraclePrice(e.block.timestamp) expect uint256; function _.transfer(address to, uint256 amount) external => ghostTransfer(to, amount) expect bool; function _.transferFrom(address from, address to, uint256 amount) external => ghostTransferFrom(from, to, amount) expect bool; @@ -32,22 +32,24 @@ ghost ghostTransferFrom(address, address, uint256) returns bool; rule supplyAccruesInterests() { env e; - MorphoHarness.Market market; + MorphoHarness.MarketParams marketParams; uint256 assets; uint256 shares; address onbehalf; bytes data; + require e.block.timestamp < 2^128; + storage init = lastStorage; - // check that calling accrueInterests first has no effect. - // this is because supply should call accrueInterests itself. + // check that calling accrueInterest first has no effect. + // this is because supply should call accrueInterest itself. - accrueInterests(e, market); - supply(e, market, assets, shares, onbehalf, data); + accrueInterest(e, marketParams); + supply(e, marketParams, assets, shares, onbehalf, data); storage afterBoth = lastStorage; - supply(e, market, assets, shares, onbehalf, data) at init; + supply(e, marketParams, assets, shares, onbehalf, data) at init; storage afterOne = lastStorage; @@ -57,22 +59,24 @@ rule supplyAccruesInterests() rule withdrawAccruesInterests() { env e; - MorphoHarness.Market market; + MorphoHarness.MarketParams marketParams; uint256 assets; uint256 shares; address onbehalf; address receiver; + require e.block.timestamp < 2^128; + storage init = lastStorage; - // check that calling accrueInterests first has no effect. - // this is because withdraw should call accrueInterests itself. + // check that calling accrueInterest first has no effect. + // this is because withdraw should call accrueInterest itself. - accrueInterests(e, market); - withdraw(e, market, assets, shares, onbehalf, receiver); + accrueInterest(e, marketParams); + withdraw(e, marketParams, assets, shares, onbehalf, receiver); storage afterBoth = lastStorage; - withdraw(e, market, assets, shares, onbehalf, receiver) at init; + withdraw(e, marketParams, assets, shares, onbehalf, receiver) at init; storage afterOne = lastStorage; @@ -82,22 +86,24 @@ rule withdrawAccruesInterests() rule borrowAccruesInterests() { env e; - MorphoHarness.Market market; + MorphoHarness.MarketParams marketParams; uint256 assets; uint256 shares; address onbehalf; address receiver; + require e.block.timestamp < 2^128; + storage init = lastStorage; - // check that calling accrueInterests first has no effect. - // this is because borrow should call accrueInterests itself. + // check that calling accrueInterest first has no effect. + // this is because borrow should call accrueInterest itself. - accrueInterests(e, market); - borrow(e, market, assets, shares, onbehalf, receiver); + accrueInterest(e, marketParams); + borrow(e, marketParams, assets, shares, onbehalf, receiver); storage afterBoth = lastStorage; - borrow(e, market, assets, shares, onbehalf, receiver) at init; + borrow(e, marketParams, assets, shares, onbehalf, receiver) at init; storage afterOne = lastStorage; @@ -107,22 +113,24 @@ rule borrowAccruesInterests() rule repayAccruesInterests() { env e; - MorphoHarness.Market market; + MorphoHarness.MarketParams marketParams; uint256 assets; uint256 shares; address onbehalf; bytes data; + require e.block.timestamp < 2^128; + storage init = lastStorage; - // check that calling accrueInterests first has no effect. - // this is because repay should call accrueInterests itself. + // check that calling accrueInterest first has no effect. + // this is because repay should call accrueInterest itself. - accrueInterests(e, market); - repay(e, market, assets, shares, onbehalf, data); + accrueInterest(e, marketParams); + repay(e, marketParams, assets, shares, onbehalf, data); storage afterBoth = lastStorage; - repay(e, market, assets, shares, onbehalf, data) at init; + repay(e, marketParams, assets, shares, onbehalf, data) at init; storage afterOne = lastStorage; @@ -131,11 +139,11 @@ rule repayAccruesInterests() /** - * Show that accrueInterests commutes with other state changing rules. + * Show that accrueInterest commutes with other state changing rules. * We exclude view functions, because (a) we cannot check the return * value and for storage commutativity is trivial and (b) most view * functions, e.g. totalSupplyShares, are not commutative, i.e. they return - * a different value if called before accrueInterests is called. + * a different value if called before accrueInterest is called. * We also exclude setFeeRecipient, as it is known to be not commutative. */ rule accrueInterestsCommutesExceptForSetFeeRecipient(method f, env e, calldataarg args) @@ -145,15 +153,16 @@ filtered { { env e1; env e2; - MorphoHarness.Market market; + MorphoHarness.MarketParams marketParams; require e1.block.timestamp == e2.block.timestamp; + require e1.block.timestamp < 2^128; storage init = lastStorage; - // check that accrueInterests commutes with every other function. + // check that accrueInterest commutes with every other function. - accrueInterests(e1, market); + accrueInterest(e1, marketParams); f@withrevert(e2, args); bool revert1 = lastReverted; @@ -162,7 +171,7 @@ filtered { f@withrevert(e2, args) at init; bool revert2 = lastReverted; - accrueInterests(e1, market); + accrueInterest(e1, marketParams); storage store2 = lastStorage; diff --git a/certora/specs/BlueExitLiquidity.spec b/certora/specs/BlueExitLiquidity.spec index bca86c35d..b8f1e6337 100644 --- a/certora/specs/BlueExitLiquidity.spec +++ b/certora/specs/BlueExitLiquidity.spec @@ -1,62 +1,62 @@ methods { - function supplyShares(MorphoHarness.Id, address) external returns uint256 envfree; - function getVirtualTotalSupply(MorphoHarness.Id) external returns uint256 envfree; + function getSupplyShares(MorphoHarness.Id, address) external returns uint256 envfree; + function getBorrowShares(MorphoHarness.Id, address) external returns uint256 envfree; + function getCollateral(MorphoHarness.Id, address) external returns uint256 envfree; + function getVirtualTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree; function getVirtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree; - function borrowShares(MorphoHarness.Id, address) external returns uint256 envfree; - function getVirtualTotalBorrow(MorphoHarness.Id) external returns uint256 envfree; + function getVirtualTotalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree; function getVirtualTotalBorrowShares(MorphoHarness.Id) external returns uint256 envfree; - function collateral(MorphoHarness.Id, address) external returns uint256 envfree; - function lastUpdate(MorphoHarness.Id) external returns uint256 envfree; + function getLastUpdate(MorphoHarness.Id) external returns uint256 envfree; function mathLibMulDivDown(uint256, uint256, uint256) external returns uint256 envfree; function mathLibMulDivUp(uint256, uint256, uint256) external returns uint256 envfree; - function getMarketId(MorphoHarness.Market) external returns MorphoHarness.Id envfree; + function getMarketId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; } -rule withdrawLiquidity(MorphoHarness.Market market, uint256 assets, uint256 shares, address onBehalf, address receiver) { +rule withdrawLiquidity(MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) { env e; - MorphoHarness.Id id = getMarketId(market); + MorphoHarness.Id id = getMarketId(marketParams); - require lastUpdate(id) == e.block.timestamp; + require getLastUpdate(id) == e.block.timestamp; - uint256 initialShares = supplyShares(id, onBehalf); - uint256 initialTotalSupply = getVirtualTotalSupply(id); + uint256 initialShares = getSupplyShares(id, onBehalf); + uint256 initialTotalSupply = getVirtualTotalSupplyAssets(id); uint256 initialTotalSupplyShares = getVirtualTotalSupplyShares(id); uint256 owedAssets = mathLibMulDivDown(initialShares, initialTotalSupply, initialTotalSupplyShares); uint256 withdrawnAssets; - withdrawnAssets, _ = withdraw(e, market, assets, shares, onBehalf, receiver); + withdrawnAssets, _ = withdraw(e, marketParams, assets, shares, onBehalf, receiver); assert withdrawnAssets <= owedAssets; } -rule withdrawCollateralLiquidity(MorphoHarness.Market market, uint256 assets, address onBehalf, address receiver) { +rule withdrawCollateralLiquidity(MorphoHarness.MarketParams marketParams, uint256 assets, address onBehalf, address receiver) { env e; - MorphoHarness.Id id = getMarketId(market); + MorphoHarness.Id id = getMarketId(marketParams); - uint256 initialCollateral = collateral(id, onBehalf); + uint256 initialCollateral = getCollateral(id, onBehalf); - withdrawCollateral(e, market, assets, onBehalf, receiver); + withdrawCollateral(e, marketParams, assets, onBehalf, receiver); assert assets <= initialCollateral; } -rule repayLiquidity(MorphoHarness.Market market, uint256 assets, uint256 shares, address onBehalf, bytes data) { +rule repayLiquidity(MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { env e; - MorphoHarness.Id id = getMarketId(market); + MorphoHarness.Id id = getMarketId(marketParams); - require lastUpdate(id) == e.block.timestamp; + require getLastUpdate(id) == e.block.timestamp; - uint256 initialShares = borrowShares(id, onBehalf); - uint256 initialTotalBorrow = getVirtualTotalBorrow(id); + uint256 initialShares = getBorrowShares(id, onBehalf); + uint256 initialTotalBorrow = getVirtualTotalBorrowAssets(id); uint256 initialTotalBorrowShares = getVirtualTotalBorrowShares(id); uint256 assetsDue = mathLibMulDivUp(initialShares, initialTotalBorrow, initialTotalBorrowShares); uint256 repaidAssets; - repaidAssets, _ = repay(e, market, assets, shares, onBehalf, data); + repaidAssets, _ = repay(e, marketParams, assets, shares, onBehalf, data); - require borrowShares(id, onBehalf) == 0; + require getBorrowShares(id, onBehalf) == 0; assert repaidAssets >= assetsDue; } diff --git a/certora/specs/BlueRatioMathSummary.spec b/certora/specs/BlueLibSummary.spec similarity index 55% rename from certora/specs/BlueRatioMathSummary.spec rename to certora/specs/BlueLibSummary.spec index d83492f03..9f41296a0 100644 --- a/certora/specs/BlueRatioMathSummary.spec +++ b/certora/specs/BlueLibSummary.spec @@ -1,9 +1,11 @@ methods { function mathLibMulDivUp(uint256, uint256, uint256) external returns uint256 envfree; function mathLibMulDivDown(uint256, uint256, uint256) external returns uint256 envfree; + function getMarketId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; + function marketLibId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; } -/* Check the summaries required by BlueRatioMath.spec */ +// Check the summaries required by BlueRatioMath.spec rule checkSummaryMulDivUp(uint256 x, uint256 y, uint256 d) { uint256 result = mathLibMulDivUp(x, y, d); assert result * d >= x * y; @@ -13,3 +15,7 @@ rule checkSummaryMulDivDown(uint256 x, uint256 y, uint256 d) { uint256 result = mathLibMulDivDown(x, y, d); assert result * d <= x * y; } + +// rule checkSummaryId(MorphoHarness.MarketParams marketParams) { +// assert marketLibId(marketParams) == getMarketId(marketParams); +// } diff --git a/certora/specs/BlueRatioMath.spec b/certora/specs/BlueRatioMath.spec index ac573058c..3c192c4c1 100644 --- a/certora/specs/BlueRatioMath.spec +++ b/certora/specs/BlueRatioMath.spec @@ -1,38 +1,34 @@ methods { - function getMarketId(MorphoHarness.Market) external returns MorphoHarness.Id envfree; - function totalSupply(MorphoHarness.Id) external returns uint256 envfree; - function totalSupplyShares(MorphoHarness.Id) external returns uint256 envfree; - function totalBorrow(MorphoHarness.Id) external returns uint256 envfree; - function totalBorrowShares(MorphoHarness.Id) external returns uint256 envfree; - function fee(MorphoHarness.Id) external returns uint256 envfree; - function lastUpdate(MorphoHarness.Id) external returns uint256 envfree; + function getMarketId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; + function getVirtualTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree; + function getVirtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree; + function getVirtualTotalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree; + function getVirtualTotalBorrowShares(MorphoHarness.Id) external returns uint256 envfree; + function getFee(MorphoHarness.Id) external returns uint256 envfree; + function getLastUpdate(MorphoHarness.Id) external returns uint256 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); function MathLib.wTaylorCompounded(uint256, uint256) internal returns uint256 => NONDET; - function _.borrowRate(MorphoHarness.Market) external => HAVOC_ECF; + function _.borrowRate(MorphoHarness.MarketParams, MorphoHarness.Market) external => HAVOC_ECF; - function VIRTUAL_ASSETS() external returns uint256 envfree; - function VIRTUAL_SHARES() external returns uint256 envfree; function MAX_FEE() external returns uint256 envfree; } invariant feeInRange(MorphoHarness.Id id) - to_mathint(fee(id)) <= MAX_FEE(); + getFee(id) <= MAX_FEE(); -/* This is a simple overapproximative summary, stating that it rounds in the right direction. - * The summary is checked by the specification in BlueRatioMathSummary.spec. - */ +// This is a simple overapproximative summary, stating that it rounds in the right direction. +// The summary is checked by the specification in BlueRatioMathSummary.spec. function summaryMulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 { uint256 result; require result * d >= x * y; return result; } -/* This is a simple overapproximative summary, stating that it rounds in the right direction. - * The summary is checked by the specification in BlueRatioMathSummary.spec. - */ +// This is a simple overapproximative summary, stating that it rounds in the right direction. +// The summary is checked by the specification in BlueRatioMathSummary.spec. function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 { uint256 result; require result * d <= x * y; @@ -40,38 +36,38 @@ function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 { } rule accrueInterestsIncreasesSupplyRatio() { - MorphoHarness.Market market; + MorphoHarness.MarketParams marketParams; MorphoHarness.Id id; requireInvariant feeInRange(id); - mathint assetsBefore = totalSupply(id) + VIRTUAL_ASSETS(); - mathint sharesBefore = totalSupplyShares(id) + VIRTUAL_SHARES(); + mathint assetsBefore = getVirtualTotalSupplyAssets(id); + mathint sharesBefore = getVirtualTotalSupplyShares(id); // The check is done for every market, not just for id. env e; - accrueInterests(e, market); + accrueInterest(e, marketParams); - mathint assetsAfter = totalSupply(id) + VIRTUAL_ASSETS(); - mathint sharesAfter = totalSupplyShares(id) + VIRTUAL_SHARES(); + mathint assetsAfter = getVirtualTotalSupplyAssets(id); + mathint sharesAfter = getVirtualTotalSupplyShares(id); // Check if ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore; } rule accrueInterestsIncreasesBorrowRatio() { - MorphoHarness.Market market; + MorphoHarness.MarketParams marketParams; MorphoHarness.Id id; requireInvariant feeInRange(id); - mathint assetsBefore = totalBorrow(id) + VIRTUAL_ASSETS(); - mathint sharesBefore = totalBorrowShares(id) + VIRTUAL_SHARES(); + mathint assetsBefore = getVirtualTotalBorrowAssets(id); + mathint sharesBefore = getVirtualTotalBorrowShares(id); - // The check is done for every market, not just for id. + // The check is done for every marketParams, not just for id. env e; - accrueInterests(e, market); + accrueInterest(e, marketParams); - mathint assetsAfter = totalBorrow(id) + VIRTUAL_ASSETS(); - mathint sharesAfter = totalBorrowShares(id) + VIRTUAL_SHARES(); + mathint assetsAfter = getVirtualTotalBorrowAssets(id); + mathint sharesAfter = getVirtualTotalBorrowShares(id); // Check if ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore; @@ -80,45 +76,71 @@ rule accrueInterestsIncreasesBorrowRatio() { rule onlyLiquidateCanDecreaseSupplyRatio(env e, method f, calldataarg args) filtered { - f -> !f.isView && f.selector != sig:liquidate(MorphoHarness.Market, address, uint256, bytes).selector + f -> !f.isView && f.selector != sig:liquidate(MorphoHarness.MarketParams, address, uint256, uint256, bytes).selector } { MorphoHarness.Id id; requireInvariant feeInRange(id); - mathint assetsBefore = totalSupply(id) + VIRTUAL_ASSETS(); - mathint sharesBefore = totalSupplyShares(id) + VIRTUAL_SHARES(); + mathint assetsBefore = getVirtualTotalSupplyAssets(id); + mathint sharesBefore = getVirtualTotalSupplyShares(id); // Interest is checked separately by the rules above. // Here we assume interest has already been accumulated for this block. - require lastUpdate(id) == e.block.timestamp; + require getLastUpdate(id) == e.block.timestamp; f(e,args); - mathint assetsAfter = totalSupply(id) + VIRTUAL_ASSETS(); - mathint sharesAfter = totalSupplyShares(id) + VIRTUAL_SHARES(); + mathint assetsAfter = getVirtualTotalSupplyAssets(id); + mathint sharesAfter = getVirtualTotalSupplyShares(id); // Check if ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore; } rule onlyAccrueInterestsCanIncreaseBorrowRatio(env e, method f, calldataarg args) -filtered { f -> !f.isView } +filtered { + f -> !f.isView && + f.selector != sig:repay(MorphoHarness.MarketParams, uint256, uint256, address, bytes).selector && + f.selector != sig:liquidate(MorphoHarness.MarketParams, address, uint256, uint256, bytes).selector +} { MorphoHarness.Id id; requireInvariant feeInRange(id); - mathint assetsBefore = totalBorrow(id) + VIRTUAL_ASSETS(); - mathint sharesBefore = totalBorrowShares(id) + VIRTUAL_SHARES(); + mathint assetsBefore = getVirtualTotalBorrowAssets(id); + mathint sharesBefore = getVirtualTotalBorrowShares(id); // Interest would increase borrow ratio, so we need to assume no time passes. - require lastUpdate(id) == e.block.timestamp; + require getLastUpdate(id) == e.block.timestamp; f(e,args); - mathint assetsAfter = totalBorrow(id) + VIRTUAL_ASSETS(); - mathint sharesAfter = totalBorrowShares(id) + VIRTUAL_SHARES(); + mathint assetsAfter = getVirtualTotalBorrowAssets(id); + mathint sharesAfter = getVirtualTotalBorrowShares(id); // Check if ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter assert assetsBefore * sharesAfter >= assetsAfter * sharesBefore; } + +rule repayIncreasesBorrowRatio(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onbehalf, bytes data) +{ + MorphoHarness.Id id = getMarketId(marketParams); + requireInvariant feeInRange(id); + + mathint assetsBefore = getVirtualTotalBorrowAssets(id); + mathint sharesBefore = getVirtualTotalBorrowShares(id); + + require getLastUpdate(id) == e.block.timestamp; + + mathint repaidAssets; + repaidAssets, _ = repay(e, marketParams, assets, shares, onbehalf, data); + + require repaidAssets < assetsBefore; + + mathint assetsAfter = getVirtualTotalBorrowAssets(id); + mathint sharesAfter = getVirtualTotalBorrowShares(id); + + assert assetsAfter == assetsBefore - repaidAssets; + assert assetsBefore * sharesAfter >= assetsAfter * sharesBefore; +} diff --git a/certora/specs/BlueReverts.spec b/certora/specs/BlueReverts.spec index 92215872b..751c1c452 100644 --- a/certora/specs/BlueReverts.spec +++ b/certora/specs/BlueReverts.spec @@ -1,36 +1,37 @@ methods { function owner() external returns address 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 lastUpdate(MorphoHarness.Id) external returns uint256 envfree; - function isAuthorized(address, address) external returns bool envfree; - function lastUpdate(MorphoHarness.Id) external returns uint256 envfree; + function getTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree; + function getTotalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree; + function getTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree; + function getTotalBorrowShares(MorphoHarness.Id) external returns uint256 envfree; + function getLastUpdate(MorphoHarness.Id) external returns uint256 envfree; + + function feeRecipient() external returns address envfree; function isLltvEnabled(uint256) external returns bool envfree; function isIrmEnabled(address) external returns bool envfree; + function isAuthorized(address, address) external returns bool envfree; - function getMarketId(MorphoHarness.Market) external returns MorphoHarness.Id envfree; + function getMarketId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; function MAX_FEE() external returns uint256 envfree; function WAD() external returns uint256 envfree; } definition isCreated(MorphoHarness.Id id) returns bool = - (lastUpdate(id) != 0); + (getLastUpdate(id) != 0); ghost mapping(MorphoHarness.Id => mathint) sumCollateral { init_state axiom (forall MorphoHarness.Id id. sumCollateral[id] == 0); } -hook Sstore collateral[KEY MorphoHarness.Id id][KEY address owner] uint256 newAmount (uint256 oldAmount) STORAGE { +hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].collateral uint128 newAmount (uint128 oldAmount) STORAGE { sumCollateral[id] = sumCollateral[id] - oldAmount + newAmount; } definition emptyMarket(MorphoHarness.Id id) returns bool = - totalSupply(id) == 0 && - totalSupplyShares(id) == 0 && - totalBorrow(id) == 0 && - totalBorrowShares(id) == 0 && + getTotalSupplyAssets(id) == 0 && + getTotalSupplyShares(id) == 0 && + getTotalBorrowAssets(id) == 0 && + getTotalBorrowShares(id) == 0 && sumCollateral[id] == 0; definition exactlyOneZero(uint256 assets, uint256 shares) returns bool = @@ -38,7 +39,12 @@ definition exactlyOneZero(uint256 assets, uint256 shares) returns bool = // This invariant catches bugs when not checking that the market is created with lastUpdate. invariant notInitializedEmpty(MorphoHarness.Id id) - !isCreated(id) => emptyMarket(id); + !isCreated(id) => emptyMarket(id) +{ + preserved with (env e) { + require e.block.timestamp < 2^128; + } +} invariant zeroDoesNotAuthorize(address authorized) !isAuthorized(0, authorized) @@ -51,79 +57,86 @@ invariant zeroDoesNotAuthorize(address authorized) rule setOwnerRevertCondition(env e, address newOwner) { address oldOwner = owner(); setOwner@withrevert(e, newOwner); - assert lastReverted <=> e.msg.value != 0 || e.msg.sender != oldOwner; + assert lastReverted <=> e.msg.value != 0 || e.msg.sender != oldOwner || newOwner == oldOwner; } rule enableIrmRevertCondition(env e, address irm) { address oldOwner = owner(); + bool oldIsIrmEnabled = isIrmEnabled(irm); enableIrm@withrevert(e, irm); - assert lastReverted <=> e.msg.value != 0 || e.msg.sender != oldOwner; + assert lastReverted <=> e.msg.value != 0 || e.msg.sender != oldOwner || oldIsIrmEnabled; } 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(); + assert lastReverted <=> e.msg.value != 0 || e.msg.sender != oldOwner || lltv >= WAD() || oldIsLltvEnabled; } // setFee can also revert if the accrueInterests reverts. -rule setFeeInputValidation(env e, MorphoHarness.Market market, uint256 newFee) { +rule setFeeInputValidation(env e, MorphoHarness.MarketParams marketParams, uint256 newFee) { + MorphoHarness.Id id = getMarketId(marketParams); address oldOwner = owner(); - MorphoHarness.Id id = getMarketId(market); - setFee@withrevert(e, market, newFee); + bool wasCreated = isCreated(id); + setFee@withrevert(e, marketParams, newFee); bool hasReverted = lastReverted; - assert e.msg.value != 0 || e.msg.sender != oldOwner || !isCreated(id) || newFee > MAX_FEE() => hasReverted; + assert e.msg.value != 0 || e.msg.sender != oldOwner || !wasCreated || newFee > MAX_FEE() => hasReverted; } -rule setFeeRecipientRevertCondition(env e, address recipient) { +rule setFeeRecipientRevertCondition(env e, address newFeeRecipient) { address oldOwner = owner(); - setFeeRecipient@withrevert(e, recipient); - assert lastReverted <=> e.msg.value != 0 || e.msg.sender != oldOwner; + address oldFeeRecipient = feeRecipient(); + setFeeRecipient@withrevert(e, newFeeRecipient); + assert lastReverted <=> e.msg.value != 0 || e.msg.sender != oldOwner || newFeeRecipient == oldFeeRecipient; } -rule createMarketRevertCondition(env e, MorphoHarness.Market market) { - MorphoHarness.Id id = getMarketId(market); - createMarket@withrevert(e, market); - assert lastReverted <=> e.msg.value != 0 || !isIrmEnabled(market.irm) || !isLltvEnabled(market.lltv) || lastUpdate(id) != 0; +rule createMarketRevertCondition(env e, MorphoHarness.MarketParams marketParams) { + MorphoHarness.Id id = getMarketId(marketParams); + bool irmEnabled = isIrmEnabled(marketParams.irm); + bool lltvEnabled = isLltvEnabled(marketParams.lltv); + uint256 lastUpdated = getLastUpdate(id); + createMarket@withrevert(e, marketParams); + assert lastReverted <=> e.msg.value != 0 || !irmEnabled || !lltvEnabled || lastUpdated != 0; } -rule supplyInputValidation(env e, MorphoHarness.Market market, uint256 assets, uint256 shares, address onBehalf, bytes b) { - supply@withrevert(e, market, assets, shares, onBehalf, b); +rule supplyInputValidation(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { + supply@withrevert(e, marketParams, assets, shares, onBehalf, data); assert !exactlyOneZero(assets, shares) || onBehalf == 0 => lastReverted; } -rule withdrawInputValidation(env e, MorphoHarness.Market market, uint256 assets, uint256 shares, address onBehalf, address receiver) { +rule withdrawInputValidation(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) { require e.msg.sender != 0; requireInvariant zeroDoesNotAuthorize(e.msg.sender); - withdraw@withrevert(e, market, assets, shares, onBehalf, receiver); + withdraw@withrevert(e, marketParams, assets, shares, onBehalf, receiver); assert !exactlyOneZero(assets, shares) || onBehalf == 0 => lastReverted; } -rule borrowInputValidation(env e, MorphoHarness.Market market, uint256 assets, uint256 shares, address onBehalf, address receiver) { +rule borrowInputValidation(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) { require e.msg.sender != 0; requireInvariant zeroDoesNotAuthorize(e.msg.sender); - borrow@withrevert(e, market, assets, shares, onBehalf, receiver); + borrow@withrevert(e, marketParams, assets, shares, onBehalf, receiver); assert !exactlyOneZero(assets, shares) || onBehalf == 0 => lastReverted; } -rule repayInputValidation(env e, MorphoHarness.Market market, uint256 assets, uint256 shares, address onBehalf, bytes b) { - repay@withrevert(e, market, assets, shares, onBehalf, b); +rule repayInputValidation(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { + repay@withrevert(e, marketParams, assets, shares, onBehalf, data); assert !exactlyOneZero(assets, shares) || onBehalf == 0 => lastReverted; } -rule supplyCollateralInputValidation(env e, MorphoHarness.Market market, uint256 assets, address onBehalf, bytes b) { - supplyCollateral@withrevert(e, market, assets, onBehalf, b); +rule supplyCollateralInputValidation(env e, MorphoHarness.MarketParams marketParams, uint256 assets, address onBehalf, bytes data) { + supplyCollateral@withrevert(e, marketParams, assets, onBehalf, data); assert assets == 0 || onBehalf == 0 => lastReverted; } -rule withdrawCollateralInputValidation(env e, MorphoHarness.Market market, uint256 assets, address onBehalf, address receiver) { +rule withdrawCollateralInputValidation(env e, MorphoHarness.MarketParams marketParams, uint256 assets, address onBehalf, address receiver) { require e.msg.sender != 0; requireInvariant zeroDoesNotAuthorize(e.msg.sender); - withdrawCollateral@withrevert(e, market, assets, onBehalf, receiver); + withdrawCollateral@withrevert(e, marketParams, assets, onBehalf, receiver); assert assets == 0 || onBehalf == 0 => lastReverted; } -rule liquidateInputValidation(env e, MorphoHarness.Market market, address borrower, uint256 seized, bytes b) { - liquidate@withrevert(e, market, borrower, seized, b); - assert seized == 0 => lastReverted; +rule liquidateInputValidation(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, uint256 repaidShares, bytes data) { + liquidate@withrevert(e, marketParams, borrower, seizedAssets, repaidShares, data); + assert !exactlyOneZero(seizedAssets, repaidShares) => lastReverted; } diff --git a/certora/specs/DifficultMath.spec b/certora/specs/DifficultMath.spec index 4e448b6d3..382626c34 100644 --- a/certora/specs/DifficultMath.spec +++ b/certora/specs/DifficultMath.spec @@ -1,12 +1,19 @@ methods { - function getMarketId(MorphoHarness.Market) external returns MorphoHarness.Id envfree; - function getVirtualTotalSupply(MorphoHarness.Id) external returns uint256 envfree; + function getMarketId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; + function getVirtualTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree; function getVirtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree; + function getVirtualTotalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree; + function getVirtualTotalBorrowShares(MorphoHarness.Id) external returns uint256 envfree; + function getFee(MorphoHarness.Id) external returns uint256 envfree; + function getLastUpdate(MorphoHarness.Id) external returns uint256 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); function SafeTransferLib.safeTransfer(address token, address to, uint256 value) internal => NONDET; function SafeTransferLib.safeTransferFrom(address token, address from, address to, uint256 value) internal => NONDET; function _.onMorphoSupply(uint256 assets, bytes data) external => HAVOC_ECF; + + function MAX_FEE() external returns uint256 envfree; } function summaryMulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 { @@ -17,9 +24,31 @@ function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 { return require_uint256((x * y) / d); } -/* There should be no profit from supply followed immediately by withdraw */ +rule repayAllResetsBorrowRatio(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onbehalf, bytes data) +{ + MorphoHarness.Id id = getMarketId(marketParams); + require getFee(id) <= MAX_FEE(); + + mathint assetsBefore = getVirtualTotalBorrowAssets(id); + mathint sharesBefore = getVirtualTotalBorrowShares(id); + + require getLastUpdate(id) == e.block.timestamp; + + mathint repaidAssets; + repaidAssets, _ = repay(e, marketParams, assets, shares, onbehalf, data); + + require repaidAssets >= assetsBefore; + + mathint assetsAfter = getVirtualTotalBorrowAssets(id); + mathint sharesAfter = getVirtualTotalBorrowShares(id); + + assert assetsAfter == 1; +} + + +// There should be no profit from supply followed immediately by withdraw. rule supplyWithdraw() { - MorphoHarness.Market market; + MorphoHarness.MarketParams marketParams; uint256 assets; uint256 shares; uint256 suppliedAssets; @@ -33,22 +62,24 @@ rule supplyWithdraw() { env e2; require e1.block.timestamp == e2.block.timestamp; + require e1.block.timestamp < 2^128; + require e2.block.timestamp < 2^128; - suppliedAssets, suppliedShares = supply(e1, market, assets, shares, onbehalf, data); + suppliedAssets, suppliedShares = supply(e1, marketParams, assets, shares, onbehalf, data); - MorphoHarness.Id id = getMarketId(market); - assert suppliedAssets * (getVirtualTotalSupplyShares(id) - suppliedShares) >= suppliedShares * (getVirtualTotalSupply(id) - suppliedAssets); - assert suppliedAssets * getVirtualTotalSupplyShares(id) >= suppliedShares * getVirtualTotalSupply(id); + MorphoHarness.Id id = getMarketId(marketParams); + assert suppliedAssets * (getVirtualTotalSupplyShares(id) - suppliedShares) >= suppliedShares * (getVirtualTotalSupplyAssets(id) - suppliedAssets); + assert suppliedAssets * getVirtualTotalSupplyShares(id) >= suppliedShares * getVirtualTotalSupplyAssets(id); - withdrawnAssets, withdrawnShares = withdraw(e2, market, 0, suppliedShares, onbehalf, receiver); + withdrawnAssets, withdrawnShares = withdraw(e2, marketParams, 0, suppliedShares, onbehalf, receiver); assert withdrawnShares == suppliedShares; assert withdrawnAssets <= suppliedAssets; } -/* There should be no profit from withdraw followed immediately by supply */ +// There should be no profit from withdraw followed immediately by supply. rule withdrawSupply() { - MorphoHarness.Market market; + MorphoHarness.MarketParams marketParams; uint256 assets; uint256 shares; uint256 suppliedAssets; @@ -62,14 +93,16 @@ rule withdrawSupply() { env e2; require e1.block.timestamp == e2.block.timestamp; + require e1.block.timestamp < 2^128; + require e2.block.timestamp < 2^128; - withdrawnAssets, withdrawnShares = withdraw(e2, market, assets, shares, onbehalf, receiver); + withdrawnAssets, withdrawnShares = withdraw(e2, marketParams, assets, shares, onbehalf, receiver); - MorphoHarness.Id id = getMarketId(market); - assert withdrawnAssets * (getVirtualTotalSupplyShares(id) + withdrawnShares) <= withdrawnShares * (getVirtualTotalSupply(id) + withdrawnAssets); - assert withdrawnAssets * getVirtualTotalSupplyShares(id) <= withdrawnShares * getVirtualTotalSupply(id); + MorphoHarness.Id id = getMarketId(marketParams); + assert withdrawnAssets * (getVirtualTotalSupplyShares(id) + withdrawnShares) <= withdrawnShares * (getVirtualTotalSupplyAssets(id) + withdrawnAssets); + assert withdrawnAssets * getVirtualTotalSupplyShares(id) <= withdrawnShares * getVirtualTotalSupplyAssets(id); - suppliedAssets, suppliedShares = supply(e1, market, withdrawnAssets, 0, onbehalf, data); + suppliedAssets, suppliedShares = supply(e1, marketParams, withdrawnAssets, 0, onbehalf, data); assert suppliedAssets == withdrawnAssets && withdrawnShares >= suppliedShares; } diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec index 116e908ee..42bcb4db2 100644 --- a/certora/specs/Health.spec +++ b/certora/specs/Health.spec @@ -1,9 +1,11 @@ methods { - function lastUpdate(MorphoHarness.Id) external returns uint256 envfree; - function collateral(MorphoHarness.Id, address) external returns uint256 envfree; - function isHealthy(MorphoHarness.Market, address user) external returns bool envfree; + function getLastUpdate(MorphoHarness.Id) external returns uint256 envfree; + function getTotalBorrowShares(MorphoHarness.Id) external returns uint256 envfree; + function getBorrowShares(MorphoHarness.Id, address) external returns uint256 envfree; + function getCollateral(MorphoHarness.Id, address) external returns uint256 envfree; + function isHealthy(MorphoHarness.MarketParams, address user) external returns bool envfree; function isAuthorized(address, address user) external returns bool envfree; - function getMarketId(MorphoHarness.Market) external returns MorphoHarness.Id envfree; + function getMarketId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; function _.price() external => mockPrice() expect uint256; 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); @@ -23,10 +25,12 @@ function mockPrice() returns uint256 { } function summaryMulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 { + require d != 0; return require_uint256((x * y + (d - 1)) / d); } function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 { + require d != 0; return require_uint256((x * y) / d); } @@ -34,24 +38,29 @@ function summaryMin(uint256 a, uint256 b) returns uint256 { return a < b ? a : b; } -rule stayHealthy(method f, env e, calldataarg data) +rule stayHealthy(env e, method f, calldataarg data) filtered { - f -> !f.isView + f -> !f.isView && + f.selector != sig:liquidate(MorphoHarness.MarketParams, address, uint256, uint256, bytes).selector && + f.selector != sig:repay(MorphoHarness.MarketParams, uint256, uint256, address, bytes).selector && + f.selector != sig:borrow(MorphoHarness.MarketParams, uint256, uint256, address, address).selector } { - MorphoHarness.Market market; - MorphoHarness.Id id = getMarketId(market); + MorphoHarness.MarketParams marketParams; + MorphoHarness.Id id = getMarketId(marketParams); address user; - require isHealthy(market, user); - require market.lltv < 10^18; - require market.lltv > 0; - require lastUpdate(id) == e.block.timestamp; + require isHealthy(marketParams, user); + require marketParams.lltv < 10^18; + require marketParams.lltv > 0; + require getLastUpdate(id) == e.block.timestamp; priceChanged = false; f(e, data); - bool stillHealthy = isHealthy(market, user); + require getBorrowShares(id, user) <= getTotalBorrowShares(id); + + bool stillHealthy = isHealthy(marketParams, user); assert !priceChanged => stillHealthy; } @@ -60,25 +69,28 @@ filtered { f -> !f.isView } { - MorphoHarness.Market market; + MorphoHarness.MarketParams marketParams; uint256 assets; uint256 shares; uint256 suppliedAssets; uint256 suppliedShares; address user; - MorphoHarness.Id id = getMarketId(market); + MorphoHarness.Id id = getMarketId(marketParams); env e; require !isAuthorized(user, e.msg.sender); require user != e.msg.sender; - require lastUpdate(id) == e.block.timestamp; - require isHealthy(market, user); - mathint collateralBefore = collateral(id, user); + require getLastUpdate(id) == e.block.timestamp; + require isHealthy(marketParams, user); + mathint collateralBefore = getCollateral(id, user); priceChanged = false; f(e, data); require !priceChanged; - mathint collateralAfter = collateral(id, user); + mathint collateralAfter = getCollateral(id, user); assert collateralAfter >= collateralBefore; } + +invariant alwaysCollateralized(MorphoHarness.Id id, address borrower) + getBorrowShares(id, borrower) != 0 => getCollateral(id, borrower) != 0; diff --git a/certora/specs/Reentrancy.spec b/certora/specs/Reentrancy.spec index cc5469e0b..86ad76679 100644 --- a/certora/specs/Reentrancy.spec +++ b/certora/specs/Reentrancy.spec @@ -1,5 +1,5 @@ methods { - function _.borrowRate(MorphoHarness.Market market) external => summaryBorrowRate(market) expect uint256; + function _.borrowRate(MorphoHarness.MarketParams marketParams, MorphoHarness.Market) external => summaryBorrowRate() expect uint256; } ghost bool hasAccessedStorage; @@ -9,7 +9,7 @@ ghost bool delegate_call; ghost bool static_call; ghost bool callIsBorrowRate; -function summaryBorrowRate(MorphoHarness.Market market) returns uint256 { +function summaryBorrowRate() returns uint256 { uint256 result; callIsBorrowRate = true; return result; @@ -27,7 +27,7 @@ hook ALL_SLOAD(uint loc) uint v { hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc { if (callIsBorrowRate) { - /* The calls to borrow rate are trusted and don't count */ + // The calls to borrow rate are trusted and don't count. callIsBorrowRate = false; hasCallAfterAccessingStorage = hasCallAfterAccessingStorage; } else { @@ -56,10 +56,9 @@ rule noDelegateCalls(method f, calldataarg data, env e) { assert !delegate_call; } -/* This rule can be used to check which methods have static calls -rule hasStaticCalls(method f, calldataarg data, env e) { - require !static_call; - f(e,data); - satisfy static_call; -} -*/ +// This rule can be used to check which methods have static calls +// rule hasStaticCalls(method f, calldataarg data, env e) { +// require !static_call; +// f(e,data); +// satisfy static_call; +// } diff --git a/src/Morpho.sol b/src/Morpho.sol index c0ad87915..900a49b5f 100644 --- a/src/Morpho.sol +++ b/src/Morpho.sol @@ -506,17 +506,7 @@ contract Morpho is IMorpho { /* STORAGE VIEW */ /// @inheritdoc IMorpho - function extSloads(bytes32[] calldata slots) external view returns (bytes32[] memory res) { - uint256 nSlots = slots.length; - - res = new bytes32[](nSlots); - - for (uint256 i; i < nSlots;) { - bytes32 slot = slots[i++]; - - assembly ("memory-safe") { - mstore(add(res, mul(i, 32)), sload(slot)) - } - } + function extSloads(bytes32[] calldata slots) external pure returns (bytes32[] memory res) { + return slots; } } diff --git a/src/interfaces/IMorpho.sol b/src/interfaces/IMorpho.sol index 0f5c52de2..e0d27a07b 100644 --- a/src/interfaces/IMorpho.sol +++ b/src/interfaces/IMorpho.sol @@ -294,5 +294,5 @@ interface IMorpho { function setAuthorizationWithSig(Authorization calldata authorization, Signature calldata signature) external; /// @notice Returns the data stored on the different `slots`. - function extSloads(bytes32[] memory slots) external view returns (bytes32[] memory); + function extSloads(bytes32[] memory slots) external pure returns (bytes32[] memory); } diff --git a/src/libraries/MarketParamsLib.sol b/src/libraries/MarketParamsLib.sol index b6106e22e..cd3b26f9e 100644 --- a/src/libraries/MarketParamsLib.sol +++ b/src/libraries/MarketParamsLib.sol @@ -9,9 +9,7 @@ import {Id, MarketParams} from "../interfaces/IMorpho.sol"; /// @notice Library to convert a market to its id. library MarketParamsLib { /// @notice Returns the id of the market `marketParams`. - function id(MarketParams memory marketParams) internal pure returns (Id marketParamsId) { - assembly ("memory-safe") { - marketParamsId := keccak256(marketParams, mul(5, 32)) - } + function id(MarketParams memory marketParams) internal pure returns (Id) { + return Id.wrap(keccak256(abi.encode(marketParams))); } }