diff --git a/certora/README.md b/certora/README.md index b9dda26aa..29f44afbb 100644 --- a/certora/README.md +++ b/certora/README.md @@ -13,7 +13,7 @@ The Morpho Blue protocol allows users to take out collateralized loans on ERC20 For a given market, Morpho Blue relies on the fact that the tokens involved respect the ERC20 standard. In particular, in case of a transfer, it is assumed that the balance of Morpho Blue increases or decreases (depending if its the recipient or the sender) of the amount transferred. -The file [Transfer.spec](./specs/Transfer.spec) defines a summary of the transfer functions. +The file [Transfer.spec](specs/Transfer.spec) defines a summary of the transfer functions. This summary is taken as the reference implementation to check that the balance of the Morpho Blue contract changes as expected. ```solidity @@ -31,9 +31,9 @@ where `balance` is the ERC20 balance of the Morpho Blue contract. The verification is done for the most common implementations of the ERC20 standard, for which we distinguish three different implementations: -- [ERC20Standard](./dispatch/ERC20Standard.sol) which respects the standard and reverts in case of insufficient funds or in case of insufficient allowance. -- [ERC20NoRevert](./dispatch/ERC20NoRevert.sol) which respects the standard but does not revert (and returns false instead). -- [ERC20USDT](./dispatch/ERC20USDT.sol) which does not strictly respects the standard because it omits the return value of the `transfer` and `transferFrom` functions. +- [ERC20Standard](dispatch/ERC20Standard.sol) which respects the standard and reverts in case of insufficient funds or in case of insufficient allowance. +- [ERC20NoRevert](dispatch/ERC20NoRevert.sol) which respects the standard but does not revert (and returns false instead). +- [ERC20USDT](dispatch/ERC20USDT.sol) which does not strictly respects the standard because it omits the return value of the `transfer` and `transferFrom` functions. Additionally, Morpho Blue always goes through a custom transfer library to handle ERC20 tokens, notably in all the above cases. This library reverts when the transfer is not successful, and this is checked for the case of insufficient funds or insufficient allowance. @@ -238,36 +238,36 @@ assert withdrawnAssets <= owedAssets; # Folder and file structure -The [`certora/specs`](./specs) folder contains the following files: +The [`certora/specs`](specs) folder contains the following files: -- [`AccrueInterest.spec`](./specs/AccrueInterest.spec) checks that the main functions accrue interest at the start of the interaction. +- [`AccrueInterest.spec`](specs/AccrueInterest.spec) checks that the main functions accrue interest at the start of the interaction. This is done by ensuring that accruing interest before calling the function does not change the outcome compared to just calling the function. View functions do not necessarily respect this property (for example, `totalSupplyShares`), and are filtered out. -- [`ConsistentState.spec`](./specs/ConsistentState.spec) checks that the state (storage) of the Morpho contract is consistent. +- [`ConsistentState.spec`](specs/ConsistentState.spec) checks that the state (storage) of the Morpho contract is consistent. This includes checking that the accounting of the total amount and shares is correct, that markets are independent from each other, that only enabled IRMs and LLTVs can be used, and that users cannot have their position made worse by an unauthorized account. -- [`ExactMath.spec`](./specs/ExactMath.spec) checks precise properties when taking into account exact multiplication and division. +- [`ExactMath.spec`](specs/ExactMath.spec) checks precise properties when taking into account exact multiplication and division. Notably, this file specifies that using supply and withdraw in the same block cannot yield more funds than at the start. -- [`ExitLiquidity.spec`](./specs/ExitLiquidity.spec) checks that when exiting a position with withdraw, withdrawCollateral, or repay, the user cannot get more than what was owed. -- [`Health.spec`](./specs/Health.spec) checks properties about the health of the positions. +- [`ExitLiquidity.spec`](specs/ExitLiquidity.spec) checks that when exiting a position with withdraw, withdrawCollateral, or repay, the user cannot get more than what was owed. +- [`Health.spec`](specs/Health.spec) checks properties about the health of the positions. Notably, functions cannot render an account unhealthy, and debt positions always have some collateral (thanks to the bad debt realization mechanism). -- [`LibSummary.spec`](./specs/LibSummary.spec) checks the summarization of the library functions that are used in other specification files. -- [`Liveness.spec`](./specs/Liveness.spec) checks that main functions change the owner of funds and the amount of shares as expected, and that it's always possible to exit a position. -- [`RatioMath.spec`](./specs/RatioMath.spec) checks that the ratio between shares and assets evolves predictably over time. -- [`Reentrancy.spec`](./specs/Reentrancy.spec) checks that the contract is immune to a particular class of reentrancy issues. -- [`Reverts.spec`](./specs/Reverts.spec) checks the condition for reverts and that inputs are correctly validated. -- [`Transfer.spec`](./specs/Transfer.spec) checks the summarization of the safe transfer library functions that are used in other specification files. +- [`LibSummary.spec`](specs/LibSummary.spec) checks the summarization of the library functions that are used in other specification files. +- [`Liveness.spec`](specs/Liveness.spec) checks that main functions change the owner of funds and the amount of shares as expected, and that it's always possible to exit a position. +- [`RatioMath.spec`](specs/RatioMath.spec) checks that the ratio between shares and assets evolves predictably over time. +- [`Reentrancy.spec`](specs/Reentrancy.spec) checks that the contract is immune to a particular class of reentrancy issues. +- [`Reverts.spec`](specs/Reverts.spec) checks the condition for reverts and that inputs are correctly validated. +- [`Transfer.spec`](specs/Transfer.spec) checks the summarization of the safe transfer library functions that are used in other specification files. -The [`certora/confs`](./confs) folder contains a configuration file for each corresponding specification file. +The [`certora/confs`](confs) folder contains a configuration file for each corresponding specification file. -The [`certora/harness`](./harness) folder contains contracts that enable the verification of Morpho Blue. +The [`certora/harness`](harness) folder contains contracts that enable the verification of Morpho Blue. Notably, this allows handling the fact that library functions should be called from a contract to be verified independently, and it allows defining needed getters. -The [`certora/dispatch`](./dispatch) folder contains different contracts similar to the ones that are expected to be called from Morpho Blue. +The [`certora/dispatch`](dispatch) folder contains different contracts similar to the ones that are expected to be called from Morpho Blue. # Getting started -Install `certoraRun` with `pip install certora-cli`. -To verify specification files, pass the corresponding configuration file in the [`certora/confs`](./confs) folder. +Install `certora-cli` package with `pip install certora-cli`. +To verify specification files, pass to `certoraRun` the corresponding configuration file in the [`certora/confs`](confs) folder. It requires having set the `CERTORAKEY` environment variable to a valid Certora key. You can also pass additional arguments, notably to verify a specific rule. For example, at the root of the repository: @@ -275,3 +275,12 @@ For example, at the root of the repository: ``` certoraRun certora/confs/ConsistentState.conf --rule borrowLessThanSupply ``` + +The `certora-cli` package also includes a `certoraMutate` binary. +The file [`gambit.conf`](gambit.conf) provides a default configuration of the mutations. +You can test to mutate the code and check it against a particular specification. +For example, at the root of the repository: + +``` +certoraMutate --prover_conf certora/confs/ConsistentState.conf --mutation_conf certora/gambit.conf +``` diff --git a/certora/gambit.conf b/certora/gambit.conf new file mode 100644 index 000000000..0dcba742c --- /dev/null +++ b/certora/gambit.conf @@ -0,0 +1,6 @@ + { + "filename" : "../src/Morpho.sol", + "sourceroot": "..", + "num_mutants": 15, + "solc_remappings": [] +} diff --git a/certora/specs/AccrueInterest.spec b/certora/specs/AccrueInterest.spec index 824cce07e..7babf38de 100644 --- a/certora/specs/AccrueInterest.spec +++ b/certora/specs/AccrueInterest.spec @@ -1,10 +1,12 @@ // SPDX-License-Identifier: GPL-2.0-or-later methods { function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; + + function 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); function MathLib.wTaylorCompounded(uint256 a, uint256 b) internal returns uint256 => ghostTaylorCompounded(a, b); - // 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.MarketParams marketParams, MorphoHarness.Market market) external with (env e) => ghostBorrowRate(marketParams.irm, e.block.timestamp) expect uint256; @@ -16,8 +18,6 @@ methods { function _.onMorphoSupply(uint256, bytes) external => NONDET; function _.onMorphoSupplyCollateral(uint256, bytes) external => NONDET; function _.onMorphoFlashLoan(uint256, bytes) external => NONDET; - - function maxFee() external returns uint256 envfree; } ghost ghostMulDivUp(uint256, uint256, uint256) returns uint256; diff --git a/certora/specs/ConsistentState.spec b/certora/specs/ConsistentState.spec index 49e0c1df8..97083a02d 100644 --- a/certora/specs/ConsistentState.spec +++ b/certora/specs/ConsistentState.spec @@ -1,25 +1,25 @@ // SPDX-License-Identifier: GPL-2.0-or-later methods { function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; + + function supplyShares(MorphoHarness.Id, address) external returns uint256 envfree; + function borrowShares(MorphoHarness.Id, address) external returns uint256 envfree; + function collateral(MorphoHarness.Id, address) external returns uint256 envfree; function totalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree; function totalSupplyShares(MorphoHarness.Id) external returns uint256 envfree; function totalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree; function totalBorrowShares(MorphoHarness.Id) external returns uint256 envfree; - function supplyShares(MorphoHarness.Id, address) external returns uint256 envfree; - function borrowShares(MorphoHarness.Id, address) external returns uint256 envfree; - function collateral(MorphoHarness.Id, address) external returns uint256 envfree; function fee(MorphoHarness.Id) external returns uint256 envfree; function lastUpdate(MorphoHarness.Id) external returns uint256 envfree; - function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id 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.MarketParams, MorphoHarness.Market) external => HAVOC_ECF; + function isLltvEnabled(uint256) external returns bool envfree; + function isAuthorized(address, address) external returns bool envfree; function maxFee() external returns uint256 envfree; function wad() external returns uint256 envfree; + function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; + + function _.borrowRate(MorphoHarness.MarketParams, MorphoHarness.Market) external => HAVOC_ECF; function SafeTransferLib.safeTransfer(address token, address to, uint256 value) internal => summarySafeTransferFrom(token, currentContract, to, value); function SafeTransferLib.safeTransferFrom(address token, address from, address to, uint256 value) internal => summarySafeTransferFrom(token, from, to, value); diff --git a/certora/specs/ExactMath.spec b/certora/specs/ExactMath.spec index 6e08543c8..5f92dac3d 100644 --- a/certora/specs/ExactMath.spec +++ b/certora/specs/ExactMath.spec @@ -1,7 +1,7 @@ // SPDX-License-Identifier: GPL-2.0-or-later methods { function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; - function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; + function virtualTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree; function virtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree; function virtualTotalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree; @@ -9,13 +9,14 @@ 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 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 maxFee() external returns uint256 envfree; } function summaryMulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 { diff --git a/certora/specs/ExitLiquidity.spec b/certora/specs/ExitLiquidity.spec index bf90ec31c..d967a7974 100644 --- a/certora/specs/ExitLiquidity.spec +++ b/certora/specs/ExitLiquidity.spec @@ -1,6 +1,7 @@ // SPDX-License-Identifier: GPL-2.0-or-later methods { function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; + function supplyShares(MorphoHarness.Id, address) external returns uint256 envfree; function borrowShares(MorphoHarness.Id, address) external returns uint256 envfree; function collateral(MorphoHarness.Id, address) external returns uint256 envfree; @@ -8,7 +9,6 @@ methods { function virtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree; function virtualTotalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree; 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; diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec index bac2aeba1..cdc689135 100644 --- a/certora/specs/Health.spec +++ b/certora/specs/Health.spec @@ -1,13 +1,15 @@ // SPDX-License-Identifier: GPL-2.0-or-later methods { function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; - function lastUpdate(MorphoHarness.Id) external returns uint256 envfree; + function totalBorrowShares(MorphoHarness.Id) external returns uint256 envfree; + function lastUpdate(MorphoHarness.Id) external returns uint256 envfree; function borrowShares(MorphoHarness.Id, address) external returns uint256 envfree; function collateral(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 libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; + function isHealthy(MorphoHarness.MarketParams, address user) external returns bool envfree; function _.price() external => mockPrice() expect uint256; function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivDown(a,b,c); diff --git a/certora/specs/LibSummary.spec b/certora/specs/LibSummary.spec index 64322f7dc..030e89140 100644 --- a/certora/specs/LibSummary.spec +++ b/certora/specs/LibSummary.spec @@ -1,6 +1,7 @@ // SPDX-License-Identifier: GPL-2.0-or-later 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; diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec index e5b96af82..0c3fb3130 100644 --- a/certora/specs/Liveness.spec +++ b/certora/specs/Liveness.spec @@ -1,15 +1,18 @@ // SPDX-License-Identifier: GPL-2.0-or-later methods { function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; + function supplyShares(MorphoInternalAccess.Id, address) external returns uint256 envfree; + function borrowShares(MorphoInternalAccess.Id, address) external returns uint256 envfree; + function collateral(MorphoInternalAccess.Id, address) external returns uint256 envfree; function totalSupplyAssets(MorphoInternalAccess.Id) external returns uint256 envfree; function totalSupplyShares(MorphoInternalAccess.Id) external returns uint256 envfree; function totalBorrowAssets(MorphoInternalAccess.Id) external returns uint256 envfree; function totalBorrowShares(MorphoInternalAccess.Id) external returns uint256 envfree; - function supplyShares(MorphoInternalAccess.Id, address) external returns uint256 envfree; - function borrowShares(MorphoInternalAccess.Id, address) external returns uint256 envfree; - function collateral(MorphoInternalAccess.Id, address) external returns uint256 envfree; function fee(MorphoInternalAccess.Id) external returns uint256 envfree; function lastUpdate(MorphoInternalAccess.Id) external returns uint256 envfree; + 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; @@ -39,6 +42,10 @@ function summarySafeTransferFrom(address token, address from, address to, uint25 } } +function min(mathint a, mathint b) returns mathint { + return a < b ? a : b; +} + // Assume no fee. // Summarize the accrue interest to avoid having to deal with reverts with absurdly high borrow rates. function summaryAccrueInterest(env e, MorphoInternalAccess.MarketParams marketParams, MorphoInternalAccess.Id id) { @@ -71,6 +78,7 @@ rule supplyChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marke mathint sharesBefore = supplyShares(id, onBehalf); mathint balanceBefore = myBalances[marketParams.loanToken]; + mathint liquidityBefore = totalSupplyAssets(id) - totalBorrowAssets(id); uint256 suppliedAssets; uint256 suppliedShares; @@ -78,11 +86,22 @@ rule supplyChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marke mathint sharesAfter = supplyShares(id, onBehalf); mathint balanceAfter = myBalances[marketParams.loanToken]; + mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id); assert assets != 0 => suppliedAssets == assets; - assert assets == 0 => suppliedShares == shares; + assert shares != 0 => suppliedShares == shares; assert sharesAfter == sharesBefore + suppliedShares; assert balanceAfter == balanceBefore + suppliedAssets; + assert liquidityAfter == liquidityBefore + suppliedAssets; +} + +// Check that you can supply non-zero tokens by passing shares. +rule canSupplyByPassingShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, address onBehalf, bytes data) { + uint256 suppliedAssets; + uint256 suppliedShares; + suppliedAssets, suppliedShares = supply(e, marketParams, 0, shares, onBehalf, data); + + satisfy suppliedAssets != 0; } // Check that tokens and shares are properly accounted following a withdraw. @@ -96,6 +115,7 @@ rule withdrawChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams mar mathint sharesBefore = supplyShares(id, onBehalf); mathint balanceBefore = myBalances[marketParams.loanToken]; + mathint liquidityBefore = totalSupplyAssets(id) - totalBorrowAssets(id); uint256 withdrawnAssets; uint256 withdrawnShares; @@ -103,11 +123,22 @@ rule withdrawChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams mar mathint sharesAfter = supplyShares(id, onBehalf); mathint balanceAfter = myBalances[marketParams.loanToken]; + mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id); assert assets != 0 => withdrawnAssets == assets; - assert assets == 0 => withdrawnShares == shares; + assert shares != 0 => withdrawnShares == shares; assert sharesAfter == sharesBefore - withdrawnShares; assert balanceAfter == balanceBefore - withdrawnAssets; + assert liquidityAfter == liquidityBefore - withdrawnAssets; +} + +// Check that you can withdraw non-zero tokens by passing shares. +rule canWithdrawByPassingShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, address onBehalf, address receiver) { + uint256 withdrawnAssets; + uint256 withdrawnShares; + withdrawnAssets, withdrawnShares = withdraw(e, marketParams, 0, shares, onBehalf, receiver); + + satisfy withdrawnAssets != 0; } // Check that tokens and shares are properly accounted following a borrow. @@ -121,6 +152,7 @@ rule borrowChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marke mathint sharesBefore = borrowShares(id, onBehalf); mathint balanceBefore = myBalances[marketParams.loanToken]; + mathint liquidityBefore = totalSupplyAssets(id) - totalBorrowAssets(id); uint256 borrowedAssets; uint256 borrowedShares; @@ -128,11 +160,22 @@ rule borrowChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marke mathint sharesAfter = borrowShares(id, onBehalf); mathint balanceAfter = myBalances[marketParams.loanToken]; + mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id); assert assets != 0 => borrowedAssets == assets; - assert assets == 0 => borrowedShares == shares; + assert shares != 0 => borrowedShares == shares; assert sharesAfter == sharesBefore + borrowedShares; assert balanceAfter == balanceBefore - borrowedAssets; + assert liquidityAfter == liquidityBefore - borrowedAssets; +} + +// Check that you can borrow non-zero tokens by passing shares. +rule canBorrowByPassingShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, address onBehalf, address receiver) { + uint256 borrowedAssets; + uint256 borrowedShares; + borrowedAssets, borrowedShares = borrow(e, marketParams, 0, shares, onBehalf, receiver); + + satisfy borrowedAssets != 0; } // Check that tokens and shares are properly accounted following a repay. @@ -146,6 +189,9 @@ rule repayChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams market mathint sharesBefore = borrowShares(id, onBehalf); mathint balanceBefore = myBalances[marketParams.loanToken]; + mathint liquidityBefore = totalSupplyAssets(id) - totalBorrowAssets(id); + + mathint borrowAssetsBefore = totalBorrowAssets(id); uint256 repaidAssets; uint256 repaidShares; @@ -153,11 +199,23 @@ rule repayChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams market mathint sharesAfter = borrowShares(id, onBehalf); mathint balanceAfter = myBalances[marketParams.loanToken]; + mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id); assert assets != 0 => repaidAssets == assets; - assert assets == 0 => repaidShares == shares; + assert shares != 0 => repaidShares == shares; assert sharesAfter == sharesBefore - repaidShares; assert balanceAfter == balanceBefore + repaidAssets; + // Taking the min to handle the zeroFloorSub in the code. + assert liquidityAfter == liquidityBefore + min(repaidAssets, borrowAssetsBefore); +} + +// Check that you can repay non-zero tokens by passing shares. +rule canRepayByPassingShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, address onBehalf, bytes data) { + uint256 repaidAssets; + uint256 repaidShares; + repaidAssets, repaidShares = repay(e, marketParams, 0, shares, onBehalf, data); + + satisfy repaidAssets != 0; } // Check that tokens and balances are properly accounted following a supplyCollateral. @@ -200,6 +258,53 @@ rule withdrawCollateralChangesTokensAndBalance(env e, MorphoInternalAccess.Marke assert balanceAfter == balanceBefore - assets; } +// 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); + + // Safe require because Morpho cannot call such functions by itself. + require currentContract != e.msg.sender; + // Assumption to simplify the balance specification in the rest of this rule. + require marketParams.loanToken != marketParams.collateralToken; + // Assumption to ensure that no interest is accumulated. + require lastUpdate(id) == e.block.timestamp; + + mathint collateralBefore = collateral(id, borrower); + mathint balanceLoanBefore = myBalances[marketParams.loanToken]; + mathint balanceCollateralBefore = myBalances[marketParams.collateralToken]; + mathint liquidityBefore = totalSupplyAssets(id) - totalBorrowAssets(id); + + mathint borrowLoanAssetsBefore = totalBorrowAssets(id); + + uint256 seizedAssets; + uint256 repaidAssets; + seizedAssets, repaidAssets = liquidate(e, marketParams, borrower, seized, repaidShares, data); + + mathint collateralAfter = collateral(id, borrower); + mathint balanceLoanAfter = myBalances[marketParams.loanToken]; + mathint balanceCollateralAfter = myBalances[marketParams.collateralToken]; + mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id); + + assert seized != 0 => seizedAssets == seized; + assert collateralBefore > to_mathint(seizedAssets) => collateralAfter == collateralBefore - seizedAssets; + assert balanceLoanAfter == balanceLoanBefore + repaidAssets; + assert balanceCollateralAfter == balanceCollateralBefore - seizedAssets; + // Taking the min to handle the zeroFloorSub in the code. + assert liquidityAfter == liquidityBefore + min(repaidAssets, borrowLoanAssetsBefore); +} + +// Check that nonce and authorization are properly updated with calling setAuthorizationWithSig. +rule setAuthorizationWithSigChangesNonceAndAuthorizes(env e, MorphoInternalAccess.Authorization authorization, MorphoInternalAccess.Signature signature) { + mathint nonceBefore = nonce(authorization.authorizer); + + setAuthorizationWithSig(e, authorization, signature); + + mathint nonceAfter = nonce(authorization.authorizer); + + assert nonceAfter == nonceBefore + 1; + assert isAuthorized(authorization.authorizer, authorization.authorized) == authorization.isAuthorized; +} + // 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); diff --git a/certora/specs/RatioMath.spec b/certora/specs/RatioMath.spec index 2d138ad13..e07ee77b9 100644 --- a/certora/specs/RatioMath.spec +++ b/certora/specs/RatioMath.spec @@ -1,7 +1,6 @@ // SPDX-License-Identifier: GPL-2.0-or-later methods { function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; - function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; function virtualTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree; function virtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree; function virtualTotalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree; @@ -9,13 +8,15 @@ 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 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.MarketParams, MorphoHarness.Market) external => HAVOC_ECF; - function maxFee() external returns uint256 envfree; } invariant feeInRange(MorphoHarness.Id id) diff --git a/certora/specs/Reentrancy.spec b/certora/specs/Reentrancy.spec index 5cb2b1639..e66336305 100644 --- a/certora/specs/Reentrancy.spec +++ b/certora/specs/Reentrancy.spec @@ -1,6 +1,7 @@ // SPDX-License-Identifier: GPL-2.0-or-later methods { function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; + function _.borrowRate(MorphoHarness.MarketParams marketParams, MorphoHarness.Market) external => summaryBorrowRate() expect uint256; } diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec index 7ecb5be1c..59554fef8 100644 --- a/certora/specs/Reverts.spec +++ b/certora/specs/Reverts.spec @@ -1,19 +1,21 @@ // SPDX-License-Identifier: GPL-2.0-or-later methods { function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; + function owner() external returns address envfree; + function feeRecipient() external returns address envfree; function totalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree; function totalBorrowAssets(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 feeRecipient() external returns address envfree; - function isLltvEnabled(uint256) external returns bool envfree; function isIrmEnabled(address) external returns bool envfree; + function isLltvEnabled(uint256) external returns bool envfree; 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 maxFee() external returns uint256 envfree; function wad() external returns uint256 envfree; } @@ -156,8 +158,22 @@ rule withdrawCollateralInputValidation(env e, MorphoHarness.MarketParams marketP assert assets == 0 || onBehalf == 0 => lastReverted; } -// Check that liqudiate reverts when its inputs are not validated. +// Check that liquidate reverts when its inputs are not validated. 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; } + +// Check that setAuthorizationWithSig reverts when its inputs are not validated. +rule setAuthorizationWithSigInputValidation(env e, MorphoHarness.Authorization authorization, MorphoHarness.Signature signature) { + uint256 nonceBefore = nonce(authorization.authorizer); + setAuthorizationWithSig@withrevert(e, authorization, signature); + assert e.block.timestamp > authorization.deadline || authorization.nonce != nonceBefore => lastReverted; +} + +// Check that accrueInterest reverts when its inputs are not validated. +rule accrueInterestInputValidation(env e, MorphoHarness.MarketParams marketParams) { + uint256 lastUpdate = lastUpdate(libId(marketParams)); + accrueInterest@withrevert(e, marketParams); + assert lastUpdate == 0 => lastReverted; +}