diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml new file mode 100644 index 000000000..e4bcbbacf --- /dev/null +++ b/.github/workflows/certora.yml @@ -0,0 +1,51 @@ +name: Certora + +on: + push: + branches: + - main + pull_request: + workflow_dispatch: + +jobs: + verify: + runs-on: ubuntu-latest + + strategy: + fail-fast: false + + matrix: + conf: + - AccrueInterest + - AssetsAccounting + - ConsistentState + - ExactMath + - Health + - LibSummary + - Liveness + - RatioMath + - Reentrancy + - Reverts + - Transfer + + steps: + - uses: actions/checkout@v3 + with: + submodules: recursive + + - name: Install python + uses: actions/setup-python@v4 + + - name: Install certora + run: pip install certora-cli + + - name: Install solc + run: | + 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/solc + + - name: Verify ${{ matrix.conf }} + run: certoraRun certora/confs/${{ matrix.conf }}.conf + env: + CERTORAKEY: ${{ secrets.CERTORAKEY }} diff --git a/.github/workflows/foundry.yml b/.github/workflows/foundry.yml index 230a7cbaf..11296558c 100644 --- a/.github/workflows/foundry.yml +++ b/.github/workflows/foundry.yml @@ -39,7 +39,7 @@ jobs: uses: foundry-rs/foundry-toolchain@v1 - name: Run Forge tests in ${{ matrix.type }} mode - run: forge test -vvv + run: yarn test:forge -vvv env: FOUNDRY_FUZZ_RUNS: ${{ matrix.fuzz-runs }} FOUNDRY_FUZZ_MAX_TEST_REJECTS: ${{ matrix.max-test-rejects }} diff --git a/.github/workflows/npm-release.yml b/.github/workflows/npm-release.yml index 51aaf7f53..8aa61c260 100644 --- a/.github/workflows/npm-release.yml +++ b/.github/workflows/npm-release.yml @@ -7,9 +7,11 @@ jobs: publish-to-npm: name: Publish to NPM runs-on: ubuntu-latest + environment: name: npm url: https://www.npmjs.com/package/@morpho-org/morpho-blue + steps: - name: Checkout uses: actions/checkout@v3 @@ -17,4 +19,4 @@ jobs: - name: Publish to npm run: | echo "//registry.npmjs.org/:_authToken=${{ secrets.NPM_TOKEN }}" > ~/.npmrc - yarn publish --access public + yarn publish --access public --ignore-scripts diff --git a/.gitignore b/.gitignore index 6f198470a..84536674b 100644 --- a/.gitignore +++ b/.gitignore @@ -16,6 +16,10 @@ docs/ # Node modules /node_modules +# Certora +.certora** +emv-*-certora* + # Hardhat /types /cache_hardhat diff --git a/README.md b/README.md index 978c43a60..3164e4533 100644 --- a/README.md +++ b/README.md @@ -40,4 +40,4 @@ All audits are stored in the [audits](./audits/)' folder. ## Licences The primary license for Morpho Blue is the Business Source License 1.1 (`BUSL-1.1`), see [`LICENSE`](./LICENSE). -However, all files in the following folders can also be licensed under `GPL-2.0-or-later` (as indicated in their SPDX headers): [`src/interfaces`](./src/interfaces), [`src/libraries`](./src/libraries), [`src/mocks`](./src/mocks), [`test`](./test). +However, all files in the following folders can also be licensed under `GPL-2.0-or-later` (as indicated in their SPDX headers): [`src/interfaces`](./src/interfaces), [`src/libraries`](./src/libraries), [`src/mocks`](./src/mocks), [`test`](./test), [`certora`](./certora). diff --git a/audits/2023-11-13-cantina-managed-review-draft.pdf b/audits/2023-11-13-morpho-blue-cantina-managed-review.pdf similarity index 100% rename from audits/2023-11-13-cantina-managed-review-draft.pdf rename to audits/2023-11-13-morpho-blue-cantina-managed-review.pdf diff --git a/audits/2024-01-05-morpho-blue-cantina-competition.pdf b/audits/2024-01-05-morpho-blue-cantina-competition.pdf new file mode 100644 index 000000000..8db682646 Binary files /dev/null and b/audits/2024-01-05-morpho-blue-cantina-competition.pdf differ diff --git a/certora/LICENSE b/certora/LICENSE new file mode 100644 index 000000000..aec4e2aca --- /dev/null +++ b/certora/LICENSE @@ -0,0 +1,389 @@ +This software is available under your choice of the GNU General Public +License, version 2 or later, or the Business Source License, as set +forth below. + + GNU GENERAL PUBLIC LICENSE + Version 2, June 1991 + + Copyright (C) 1989, 1991 Free Software Foundation, Inc., + 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA + Everyone is permitted to copy and distribute verbatim copies + of this license document, but changing it is not allowed. + + Preamble + + The licenses for most software are designed to take away your +freedom to share and change it. By contrast, the GNU General Public +License is intended to guarantee your freedom to share and change free +software--to make sure the software is free for all its users. This +General Public License applies to most of the Free Software +Foundation's software and to any other program whose authors commit to +using it. (Some other Free Software Foundation software is covered by +the GNU Lesser General Public License instead.) You can apply it to +your programs, too. + + When we speak of free software, we are referring to freedom, not +price. Our General Public Licenses are designed to make sure that you +have the freedom to distribute copies of free software (and charge for +this service if you wish), that you receive source code or can get it +if you want it, that you can change the software or use pieces of it +in new free programs; and that you know you can do these things. + + To protect your rights, we need to make restrictions that forbid +anyone to deny you these rights or to ask you to surrender the rights. +These restrictions translate to certain responsibilities for you if you +distribute copies of the software, or if you modify it. + + For example, if you distribute copies of such a program, whether +gratis or for a fee, you must give the recipients all the rights that +you have. You must make sure that they, too, receive or can get the +source code. And you must show them these terms so they know their +rights. + + We protect your rights with two steps: (1) copyright the software, and +(2) offer you this license which gives you legal permission to copy, +distribute and/or modify the software. + + Also, for each author's protection and ours, we want to make certain +that everyone understands that there is no warranty for this free +software. If the software is modified by someone else and passed on, we +want its recipients to know that what they have is not the original, so +that any problems introduced by others will not reflect on the original +authors' reputations. + + Finally, any free program is threatened constantly by software +patents. We wish to avoid the danger that redistributors of a free +program will individually obtain patent licenses, in effect making the +program proprietary. To prevent this, we have made it clear that any +patent must be licensed for everyone's free use or not licensed at all. + + The precise terms and conditions for copying, distribution and +modification follow. + + GNU GENERAL PUBLIC LICENSE + TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION + + 0. This License applies to any program or other work which contains +a notice placed by the copyright holder saying it may be distributed +under the terms of this General Public License. The "Program", below, +refers to any such program or work, and a "work based on the Program" +means either the Program or any derivative work under copyright law: +that is to say, a work containing the Program or a portion of it, +either verbatim or with modifications and/or translated into another +language. (Hereinafter, translation is included without limitation in +the term "modification".) Each licensee is addressed as "you". + +Activities other than copying, distribution and modification are not +covered by this License; they are outside its scope. The act of +running the Program is not restricted, and the output from the Program +is covered only if its contents constitute a work based on the +Program (independent of having been made by running the Program). +Whether that is true depends on what the Program does. + + 1. You may copy and distribute verbatim copies of the Program's +source code as you receive it, in any medium, provided that you +conspicuously and appropriately publish on each copy an appropriate +copyright notice and disclaimer of warranty; keep intact all the +notices that refer to this License and to the absence of any warranty; +and give any other recipients of the Program a copy of this License +along with the Program. + +You may charge a fee for the physical act of transferring a copy, and +you may at your option offer warranty protection in exchange for a fee. + + 2. You may modify your copy or copies of the Program or any portion +of it, thus forming a work based on the Program, and copy and +distribute such modifications or work under the terms of Section 1 +above, provided that you also meet all of these conditions: + + a) You must cause the modified files to carry prominent notices + stating that you changed the files and the date of any change. + + b) You must cause any work that you distribute or publish, that in + whole or in part contains or is derived from the Program or any + part thereof, to be licensed as a whole at no charge to all third + parties under the terms of this License. + + c) If the modified program normally reads commands interactively + when run, you must cause it, when started running for such + interactive use in the most ordinary way, to print or display an + announcement including an appropriate copyright notice and a + notice that there is no warranty (or else, saying that you provide + a warranty) and that users may redistribute the program under + these conditions, and telling the user how to view a copy of this + License. (Exception: if the Program itself is interactive but + does not normally print such an announcement, your work based on + the Program is not required to print an announcement.) + +These requirements apply to the modified work as a whole. If +identifiable sections of that work are not derived from the Program, +and can be reasonably considered independent and separate works in +themselves, then this License, and its terms, do not apply to those +sections when you distribute them as separate works. But when you +distribute the same sections as part of a whole which is a work based +on the Program, the distribution of the whole must be on the terms of +this License, whose permissions for other licensees extend to the +entire whole, and thus to each and every part regardless of who wrote it. + +Thus, it is not the intent of this section to claim rights or contest +your rights to work written entirely by you; rather, the intent is to +exercise the right to control the distribution of derivative or +collective works based on the Program. + +In addition, mere aggregation of another work not based on the Program +with the Program (or with a work based on the Program) on a volume of +a storage or distribution medium does not bring the other work under +the scope of this License. + + 3. You may copy and distribute the Program (or a work based on it, +under Section 2) in object code or executable form under the terms of +Sections 1 and 2 above provided that you also do one of the following: + + a) Accompany it with the complete corresponding machine-readable + source code, which must be distributed under the terms of Sections + 1 and 2 above on a medium customarily used for software interchange; or, + + b) Accompany it with a written offer, valid for at least three + years, to give any third party, for a charge no more than your + cost of physically performing source distribution, a complete + machine-readable copy of the corresponding source code, to be + distributed under the terms of Sections 1 and 2 above on a medium + customarily used for software interchange; or, + + c) Accompany it with the information you received as to the offer + to distribute corresponding source code. (This alternative is + allowed only for noncommercial distribution and only if you + received the program in object code or executable form with such + an offer, in accord with Subsection b above.) + +The source code for a work means the preferred form of the work for +making modifications to it. For an executable work, complete source +code means all the source code for all modules it contains, plus any +associated interface definition files, plus the scripts used to +control compilation and installation of the executable. However, as a +special exception, the source code distributed need not include +anything that is normally distributed (in either source or binary +form) with the major components (compiler, kernel, and so on) of the +operating system on which the executable runs, unless that component +itself accompanies the executable. + +If distribution of executable or object code is made by offering +access to copy from a designated place, then offering equivalent +access to copy the source code from the same place counts as +distribution of the source code, even though third parties are not +compelled to copy the source along with the object code. + + 4. You may not copy, modify, sublicense, or distribute the Program +except as expressly provided under this License. Any attempt +otherwise to copy, modify, sublicense or distribute the Program is +void, and will automatically terminate your rights under this License. +However, parties who have received copies, or rights, from you under +this License will not have their licenses terminated so long as such +parties remain in full compliance. + + 5. You are not required to accept this License, since you have not +signed it. However, nothing else grants you permission to modify or +distribute the Program or its derivative works. These actions are +prohibited by law if you do not accept this License. Therefore, by +modifying or distributing the Program (or any work based on the +Program), you indicate your acceptance of this License to do so, and +all its terms and conditions for copying, distributing or modifying +the Program or works based on it. + + 6. Each time you redistribute the Program (or any work based on the +Program), the recipient automatically receives a license from the +original licensor to copy, distribute or modify the Program subject to +these terms and conditions. You may not impose any further +restrictions on the recipients' exercise of the rights granted herein. +You are not responsible for enforcing compliance by third parties to +this License. + + 7. If, as a consequence of a court judgment or allegation of patent +infringement or for any other reason (not limited to patent issues), +conditions are imposed on you (whether by court order, agreement or +otherwise) that contradict the conditions of this License, they do not +excuse you from the conditions of this License. If you cannot +distribute so as to satisfy simultaneously your obligations under this +License and any other pertinent obligations, then as a consequence you +may not distribute the Program at all. For example, if a patent +license would not permit royalty-free redistribution of the Program by +all those who receive copies directly or indirectly through you, then +the only way you could satisfy both it and this License would be to +refrain entirely from distribution of the Program. + +If any portion of this section is held invalid or unenforceable under +any particular circumstance, the balance of the section is intended to +apply and the section as a whole is intended to apply in other +circumstances. + +It is not the purpose of this section to induce you to infringe any +patents or other property right claims or to contest validity of any +such claims; this section has the sole purpose of protecting the +integrity of the free software distribution system, which is +implemented by public license practices. Many people have made +generous contributions to the wide range of software distributed +through that system in reliance on consistent application of that +system; it is up to the author/donor to decide if he or she is willing +to distribute software through any other system and a licensee cannot +impose that choice. + +This section is intended to make thoroughly clear what is believed to +be a consequence of the rest of this License. + + 8. If the distribution and/or use of the Program is restricted in +certain countries either by patents or by copyrighted interfaces, the +original copyright holder who places the Program under this License +may add an explicit geographical distribution limitation excluding +those countries, so that distribution is permitted only in or among +countries not thus excluded. In such case, this License incorporates +the limitation as if written in the body of this License. + + 9. The Free Software Foundation may publish revised and/or new versions +of the General Public License from time to time. Such new versions will +be similar in spirit to the present version, but may differ in detail to +address new problems or concerns. + +Each version is given a distinguishing version number. If the Program +specifies a version number of this License which applies to it and "any +later version", you have the option of following the terms and conditions +either of that version or of any later version published by the Free +Software Foundation. If the Program does not specify a version number of +this License, you may choose any version ever published by the Free Software +Foundation. + + 10. If you wish to incorporate parts of the Program into other free +programs whose distribution conditions are different, write to the author +to ask for permission. For software which is copyrighted by the Free +Software Foundation, write to the Free Software Foundation; we sometimes +make exceptions for this. Our decision will be guided by the two goals +of preserving the free status of all derivatives of our free software and +of promoting the sharing and reuse of software generally. + + NO WARRANTY + + 11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY +FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW. EXCEPT WHEN +OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES +PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED +OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF +MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE ENTIRE RISK AS +TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU. SHOULD THE +PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING, +REPAIR OR CORRECTION. + + 12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING +WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR +REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, +INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING +OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED +TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY +YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER +PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE +POSSIBILITY OF SUCH DAMAGES. + + END OF TERMS AND CONDITIONS + + +Business Source License 1.1 + +License text copyright (c) 2017 MariaDB Corporation Ab, All Rights Reserved. +"Business Source License" is a trademark of MariaDB Corporation Ab. + +----------------------------------------------------------------------------- + +Parameters + +Licensor: Morpho Association + +Licensed Work: Morpho Blue Core + The Licensed Work is (c) 2023 Morpho Association + +Additional Use Grant: Any uses listed and defined at + morpho-blue-core-license-grants.morpho.eth + +Change Date: The earlier of (i) 2026-01-01, or (ii) a date specified + at morpho-blue-core-license-date.morpho.eth, or (iii) + upon the activation of the setFee function of the + Licensed Work’s applicable protocol smart contracts + deployed for production use. + +Change License: GNU General Public License v2.0 or later + +----------------------------------------------------------------------------- + +Terms + +The Licensor hereby grants you the right to copy, modify, create derivative +works, redistribute, and make non-production use of the Licensed Work. The +Licensor may make an Additional Use Grant, above, permitting limited +production use. + +Effective on the Change Date, or the fourth anniversary of the first publicly +available distribution of a specific version of the Licensed Work under this +License, whichever comes first, the Licensor hereby grants you rights under +the terms of the Change License, and the rights granted in the paragraph +above terminate. + +If your use of the Licensed Work does not comply with the requirements +currently in effect as described in this License, you must purchase a +commercial license from the Licensor, its affiliated entities, or authorized +resellers, or you must refrain from using the Licensed Work. + +All copies of the original and modified Licensed Work, and derivative works +of the Licensed Work, are subject to this License. This License applies +separately for each version of the Licensed Work and the Change Date may vary +for each version of the Licensed Work released by Licensor. + +You must conspicuously display this License on each original or modified copy +of the Licensed Work. If you receive the Licensed Work in original or +modified form from a third party, the terms and conditions set forth in this +License apply to your use of that work. + +Any use of the Licensed Work in violation of this License will automatically +terminate your rights under this License for the current and all other +versions of the Licensed Work. + +This License does not grant you any right in any trademark or logo of +Licensor or its affiliates (provided that you may use a trademark or logo of +Licensor as expressly required by this License). + +TO THE EXTENT PERMITTED BY APPLICABLE LAW, THE LICENSED WORK IS PROVIDED ON +AN "AS IS" BASIS. LICENSOR HEREBY DISCLAIMS ALL WARRANTIES AND CONDITIONS, +EXPRESS OR IMPLIED, INCLUDING (WITHOUT LIMITATION) WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE, NON-INFRINGEMENT, AND +TITLE. + +MariaDB hereby grants you permission to use this License’s text to license +your works, and to refer to it using the trademark "Business Source License", +as long as you comply with the Covenants of Licensor below. + +----------------------------------------------------------------------------- + +Covenants of Licensor + +In consideration of the right to use this License’s text and the "Business +Source License" name and trademark, Licensor covenants to MariaDB, and to all +other recipients of the licensed work to be provided by Licensor: + +1. To specify as the Change License the GPL Version 2.0 or any later version, + or a license that is compatible with GPL Version 2.0 or a later version, + where "compatible" means that software provided under the Change License can + be included in a program with software provided under GPL Version 2.0 or a + later version. Licensor may specify additional Change Licenses without + limitation. + +2. To either: (a) specify an additional grant of rights to use that does not + impose any additional restriction on the right granted in this License, as + the Additional Use Grant; or (b) insert the text "None". + +3. To specify a Change Date. + +4. Not to modify this License in any other way. + +----------------------------------------------------------------------------- + +Notice + +The Business Source License (this document, or the "License") is not an Open +Source license. However, the Licensed Work will eventually be made available +under an Open Source License, as stated in this License. diff --git a/certora/README.md b/certora/README.md new file mode 100644 index 000000000..8d6127320 --- /dev/null +++ b/certora/README.md @@ -0,0 +1,287 @@ +This folder contains the verification of the Morpho Blue protocol using CVL, Certora's Verification Language. + +The core concepts of the the Morpho Blue protocol are described in the [Whitepaper](../morpho-blue-whitepaper.pdf). +These concepts have been verified using CVL. +We first give a [high-level description](#high-level-description) of the verification and then describe the [folder and file structure](#folder-and-file-structure) of the specification files. + +# High-level description + +The Morpho Blue protocol allows users to take out collateralized loans on ERC20 tokens. + +## ERC20 tokens and transfers + +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. +This summary is taken as the reference implementation to check that the balance of the Morpho Blue contract changes as expected. + +```solidity +function summarySafeTransferFrom(address token, address from, address to, uint256 amount) { + if (from == currentContract) { + balance[token] = require_uint256(balance[token] - amount); + } + if (to == currentContract) { + balance[token] = require_uint256(balance[token] + amount); + } +} +``` + +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. + +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. +The use of the library can make it difficult for the provers, so the summary is sometimes used in other specification files to ease the verification of rules that rely on the transfer of tokens. + +## Markets + +The Morpho Blue contract is a singleton contract that defines different markets. +Markets on Morpho Blue depend on a pair of assets, the loan token that is supplied and borrowed, and the collateral token. +Taking out a loan requires to deposit some collateral, which stays idle in the contract. +Additionally, every loan token that is not borrowed also stays idle in the contract. +This is verified by the following property: + +```solidity +invariant idleAmountLessThanBalance(address token) + idleAmount[token] <= balance[token] +``` + +where `idleAmount` is the sum over all the markets of: the collateral amounts plus the supplied amounts minus the borrowed amounts. +In effect, this means that funds can only leave the contract through borrows and withdrawals. + +Additionally, it is checked that on a given market the borrowed amounts cannot exceed the supplied amounts. + +```solidity +invariant borrowLessThanSupply(MorphoHarness.Id id) + totalBorrowAssets(id) <= totalSupplyAssets(id); +``` + +This property, along with the previous one ensures that other markets can only impact the balance positively. +Said otherwise, markets are independent: tokens from a given market cannot be impacted by operations done in another market. + +## Shares + +When supplying on Morpho Blue, interest is earned over time, and the distribution is implemented through a shares mechanism. +Shares increase in value as interest is accrued. +The share mechanism is implemented symetrically for the borrow side: a share of borrow increasing in value over time represents additional owed interest. +The rule `accrueInterestIncreasesSupplyRatio` checks this property for the supply side with the following statement. + +```soldidity + // Check that the ratio increases: assetsBefore/sharesBefore <= assetsAfter/sharesAfter. + assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore; +``` + +where `assetsBefore` and `sharesBefore` represents respectively the supplied assets and the supplied shares before accruing the interest. Similarly, `assetsAfter` and `sharesAfter` represent the supplied assets and shares after an interest accrual. + +The accounting of the shares mechanism relies on another variable to store the total number of shares, in order to compute what is the relative part of each user. +This variable needs to be kept up to date at each corresponding interaction, and it is checked that this accounting is done properly. +For example, for the supply side, this is done by the following invariant. + +```solidity +invariant sumSupplySharesCorrect(MorphoHarness.Id id) + to_mathint(totalSupplyShares(id)) == sumSupplyShares[id]; +``` + +where `sumSupplyShares` only exists in the specification, and is defined to be automatically updated whenever any of the shares of the users are modified. + +## Positions health and liquidations + +To ensure proper collateralization, a liquidation system is put in place, where unhealthy positions can be liquidated. +A position is said to be healthy if the ratio of the borrowed value over collateral value is smaller than the liquidation loan-to-value (LLTV) of that market. +This leaves a safety buffer before the position can be insolvent, where the aforementioned ratio is above 1. +To ensure that liquidators have the time to interact with unhealthy positions, it is formally verified that this buffer is respected. +Notably, it is verified that in the absence of accrued interest, which is the case when creating a new position or when interacting multiple times in the same block, a position cannot be made unhealthy. + +Let's define bad debt of a position as the amount borrowed when it is backed by no collateral. +Morpho Blue automatically realizes the bad debt when liquidating a position, by transferring it to the lenders. +In effect, this means that there is no bad debt on Morpho Blue, which is verified by the following invariant. + +```solidity +invariant alwaysCollateralized(MorphoHarness.Id id, address borrower) + borrowShares(id, borrower) != 0 => collateral(id, borrower) != 0; +``` + +More generally, this means that the result of liquidating a position multiple times eventually lead to a healthy position (possibly empty). + +## Authorization + +Morpho Blue also defines primitive authorization system, where users can authorize an account to fully manage their position. +This allows to rebuild more granular control of the position on top by authorizing an immutable contract with limited capabilities. +The authorization is verified to be sound in the sense that no user can modify the position of another user without proper authorization (except when liquidating). + +Let's detail the rule that makes sure that the supply side stays consistent. + +```solidity +rule userCannotLoseSupplyShares(env e, method f, calldataarg data) +filtered { f -> !f.isView } +{ + MorphoHarness.Id id; + address user; + + // Assume that the e.msg.sender is not authorized. + require !isAuthorized(user, e.msg.sender); + require user != e.msg.sender; + + mathint sharesBefore = supplyShares(id, user); + + f(e, data); + + mathint sharesAfter = supplyShares(id, user); + + assert sharesAfter >= sharesBefore; +} +``` + +In the previous rule, an arbitrary function of Morpho Blue `f` is called with arbitrary `data`. +Shares of `user` on the market identified by `id` are recorded before and after this call. +In this way, it is checked that the supply shares are increasing when the caller of the function is neither the owner of those shares (`user != e.msg.sender`) nor authorized (`!isAuthorized(user, e.msg.sender)`). + +## Other safety properties + +### Enabled LLTV and IRM + +Creating a market is permissionless on Morpho Blue, but some parameters should fall into the range of admitted values. +Notably, the LLTV value should be enabled beforehand. +The following rule checks that no market can ever exist with a LLTV that had not been previously approved. + +```solidity +invariant onlyEnabledLltv(MorphoHarness.MarketParams marketParams) + isCreated(libId(marketParams)) => isLltvEnabled(marketParams.lltv); +``` + +Similarly, the interest rate model (IRM) used for the market must have been previously whitelisted. + +### Range of the fee + +The governance can choose to set a fee to a given market. +Fees are guaranteed to never exceed 25% of the interest accrued, and this is verified by the following rule. + +```solidity +invariant feeInRange(MorphoHarness.Id id) + fee(id) <= maxFee(); +``` + +### Sanity checks and input validation + +The formal verification is also taking care of other sanity checks, some of which are needed properties to verify other rules. +For example, the following rule checks that the variable storing the last update time is no more than the current time. +This is a sanity check, but it is also useful to ensure that there will be no underflow when computing the time elapsed since the last update. + +```solidity +rule noTimeTravel(method f, env e, calldataarg args) +filtered { f -> !f.isView } +{ + MorphoHarness.Id id; + // Assume the property before the interaction. + require lastUpdate(id) <= e.block.timestamp; + f(e, args); + assert lastUpdate(id) <= e.block.timestamp; +} +``` + +Additional rules are verified to ensure that the sanitization of inputs is done correctly. + +```solidity +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; +} +``` + +The previous rule checks that the `supply` function reverts whenever the `onBehalf` parameter is the address zero, or when either both `assets` and `shares` are zero or both are non-zero. + +## Liveness properties + +On top of verifying that the protocol is secured, the verification also proves that it is usable. +Such properties are called liveness properties, and it is notably checked that the accounting is done when an interaction goes through. +As an example, the `withdrawChangesTokensAndShares` rule checks that calling the `withdraw` function successfully will decrease the shares of the concerned account and increase the balance of the receiver. + +Other liveness properties are verified as well. +Notably, it's also verified that it is always possible to exit a position without concern for the oracle. +This is done through the verification of two rules: the `canRepayAll` rule and the `canWithdrawCollateralAll` rule. +The `canRepayAll` rule ensures that it is always possible to repay the full debt of a position, leaving the account without any oustanding debt. +The `canWithdrawCollateralAll` rule ensures that in the case where the account has no outstanding debt, then it is possible to withdraw the full collateral. + +## Protection against common attack vectors + +Other common and known attack vectors are verified to not be possible on the Morpho Blue protocol. + +### Reentrancy + +Reentrancy is a common attack vector that happen when a call to a contract allows, when in a temporary state, to call the same contract again. +The state of the contract usually refers to the storage variables, which can typically hold values that are meant to be used only after the full execution of the current function. +The Morpho Blue contract is verified to not be vulnerable to this kind of reentrancy attack thanks to the rule `reentrancySafe`. + +### Extraction of value + +The Morpho Blue protocol uses a conservative approach to handle arithmetic operations. +Rounding is done such that potential (small) errors are in favor of the protocol, which ensures that it is not possible to extract value from other users. + +The rule `supplyWithdraw` handles the simple scenario of a supply followed by a withdraw, and has the following check. + +```solidity +assert withdrawnAssets <= suppliedAssets; +``` + +The rule `withdrawAssetsAccounting` is more general and defines `ownedAssets` as the assets that the user owns, rounding in favor of the protocol. +This rule has the following check to ensure that no more than the owned assets can be withdrawn. + +```solidity +assert withdrawnAssets <= ownedAssets; +``` + +# Folder and file structure + +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. + 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. +- [`AssetsAccounting.spec`](specs/AssetsAccounting.spec) checks that when exiting a position the user cannot get more than what was owed. + Similarly, when entering a position, the assets owned as a result are no greater than what was given. +- [`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. + Notably, this file specifies that using supply and withdraw in the same block cannot yield more funds than at the start. +- [`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. + +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. +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. + +# Getting started + +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: + +``` +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/confs/AccrueInterest.conf b/certora/confs/AccrueInterest.conf new file mode 100644 index 000000000..3ae9ec84b --- /dev/null +++ b/certora/confs/AccrueInterest.conf @@ -0,0 +1,14 @@ +{ + "files": [ + "certora/harness/MorphoHarness.sol", + ], + "verify": "MorphoHarness:certora/specs/AccrueInterest.spec", + "prover_args": [ + "-depth 3", + "-smt_hashingScheme plaininjectivity", + "-mediumTimeout 30", + ], + "rule_sanity": "basic", + "server": "production", + "msg": "Morpho Blue Accrue Interest" +} diff --git a/certora/confs/AssetsAccounting.conf b/certora/confs/AssetsAccounting.conf new file mode 100644 index 000000000..e8a011349 --- /dev/null +++ b/certora/confs/AssetsAccounting.conf @@ -0,0 +1,9 @@ +{ + "files": [ + "certora/harness/MorphoHarness.sol", + ], + "verify": "MorphoHarness:certora/specs/AssetsAccounting.spec", + "rule_sanity": "basic", + "server": "production", + "msg": "Morpho Blue Assets Accounting" +} diff --git a/certora/confs/ConsistentState.conf b/certora/confs/ConsistentState.conf new file mode 100644 index 000000000..45c0c672f --- /dev/null +++ b/certora/confs/ConsistentState.conf @@ -0,0 +1,9 @@ +{ + "files": [ + "certora/harness/MorphoHarness.sol", + ], + "verify": "MorphoHarness:certora/specs/ConsistentState.spec", + "rule_sanity": "basic", + "server": "production", + "msg": "Morpho Blue Consistent State" +} diff --git a/certora/confs/ExactMath.conf b/certora/confs/ExactMath.conf new file mode 100644 index 000000000..35d755e27 --- /dev/null +++ b/certora/confs/ExactMath.conf @@ -0,0 +1,14 @@ +{ + "files": [ + "certora/harness/MorphoHarness.sol", + ], + "verify": "MorphoHarness:certora/specs/ExactMath.spec", + "rule_sanity": "basic", + "prover_args": [ + "-depth 3", + "-smt_hashingScheme plaininjectivity", + "-mediumTimeout 30", + ], + "server": "production", + "msg": "Morpho Blue Exact Math" +} diff --git a/certora/confs/Health.conf b/certora/confs/Health.conf new file mode 100644 index 000000000..9238fde6b --- /dev/null +++ b/certora/confs/Health.conf @@ -0,0 +1,13 @@ +{ + "files": [ + "certora/harness/MorphoHarness.sol", + "src/mocks/OracleMock.sol" + ], + "verify": "MorphoHarness:certora/specs/Health.spec", + "rule_sanity": "basic", + "prover_args": [ + "-smt_hashingScheme plaininjectivity", + ], + "server": "production", + "msg": "Morpho Blue Health" +} diff --git a/certora/confs/LibSummary.conf b/certora/confs/LibSummary.conf new file mode 100644 index 000000000..6f944ed00 --- /dev/null +++ b/certora/confs/LibSummary.conf @@ -0,0 +1,9 @@ +{ + "files": [ + "certora/harness/MorphoHarness.sol", + ], + "verify": "MorphoHarness:certora/specs/LibSummary.spec", + "rule_sanity": "basic", + "server": "production", + "msg": "Morpho Blue Lib Summary" +} diff --git a/certora/confs/Liveness.conf b/certora/confs/Liveness.conf new file mode 100644 index 000000000..b3788c685 --- /dev/null +++ b/certora/confs/Liveness.conf @@ -0,0 +1,9 @@ +{ + "files": [ + "certora/harness/MorphoInternalAccess.sol", + ], + "verify": "MorphoInternalAccess:certora/specs/Liveness.spec", + "rule_sanity": "basic", + "server": "production", + "msg": "Morpho Blue Liveness" +} diff --git a/certora/confs/RatioMath.conf b/certora/confs/RatioMath.conf new file mode 100644 index 000000000..a0ac6df8b --- /dev/null +++ b/certora/confs/RatioMath.conf @@ -0,0 +1,14 @@ +{ + "files": [ + "certora/harness/MorphoHarness.sol", + ], + "verify": "MorphoHarness:certora/specs/RatioMath.spec", + "rule_sanity": "basic", + "prover_args": [ + "-smt_hashingScheme plaininjectivity", + "-mediumTimeout 30", + "-timeout 3600", + ], + "server": "production", + "msg": "Morpho Blue Ratio Math" +} diff --git a/certora/confs/Reentrancy.conf b/certora/confs/Reentrancy.conf new file mode 100644 index 000000000..db93b6a23 --- /dev/null +++ b/certora/confs/Reentrancy.conf @@ -0,0 +1,12 @@ +{ + "files": [ + "certora/harness/MorphoHarness.sol", + ], + "verify": "MorphoHarness:certora/specs/Reentrancy.spec", + "rule_sanity": "basic", + "prover_args": [ + "-enableStorageSplitting false", + ], + "server": "production", + "msg": "Morpho Blue Reentrancy" +} diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf new file mode 100644 index 000000000..a31c697d4 --- /dev/null +++ b/certora/confs/Reverts.conf @@ -0,0 +1,9 @@ +{ + "files": [ + "certora/harness/MorphoHarness.sol", + ], + "verify": "MorphoHarness:certora/specs/Reverts.spec", + "rule_sanity": "basic", + "server": "production", + "msg": "Morpho Blue Reverts" +} diff --git a/certora/confs/Transfer.conf b/certora/confs/Transfer.conf new file mode 100644 index 000000000..bedba566c --- /dev/null +++ b/certora/confs/Transfer.conf @@ -0,0 +1,12 @@ +{ + "files": [ + "certora/harness/TransferHarness.sol", + "certora/dispatch/ERC20Standard.sol", + "certora/dispatch/ERC20USDT.sol", + "certora/dispatch/ERC20NoRevert.sol", + ], + "verify": "TransferHarness:certora/specs/Transfer.spec", + "rule_sanity": "basic", + "server": "production", + "msg": "Morpho Blue Transfer" +} diff --git a/certora/dispatch/ERC20NoRevert.sol b/certora/dispatch/ERC20NoRevert.sol new file mode 100644 index 000000000..b8dfccd1e --- /dev/null +++ b/certora/dispatch/ERC20NoRevert.sol @@ -0,0 +1,48 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +pragma solidity ^0.8.0; + +contract ERC20NoRevert { + address public owner; + uint256 public totalSupply; + mapping(address => uint256) public balanceOf; + mapping(address => mapping(address => uint256)) public allowance; + + constructor() { + owner = msg.sender; + } + + modifier onlyOwner() { + require(msg.sender == owner); + _; + } + + function _transfer(address _from, address _to, uint256 _amount) internal returns (bool) { + if (balanceOf[_from] < _amount) { + return false; + } + balanceOf[_from] -= _amount; + balanceOf[_to] += _amount; + return true; + } + + function transfer(address _to, uint256 _amount) public returns (bool) { + return _transfer(msg.sender, _to, _amount); + } + + function transferFrom(address _from, address _to, uint256 _amount) public returns (bool) { + if (allowance[_from][msg.sender] < _amount) { + return false; + } + allowance[_from][msg.sender] -= _amount; + return _transfer(_from, _to, _amount); + } + + function approve(address _spender, uint256 _amount) public { + allowance[msg.sender][_spender] = _amount; + } + + function mint(address _receiver, uint256 _amount) public onlyOwner { + balanceOf[_receiver] += _amount; + totalSupply += _amount; + } +} diff --git a/certora/dispatch/ERC20Standard.sol b/certora/dispatch/ERC20Standard.sol new file mode 100644 index 000000000..71af6d9ca --- /dev/null +++ b/certora/dispatch/ERC20Standard.sol @@ -0,0 +1,42 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +pragma solidity ^0.8.0; + +contract ERC20Standard { + address public owner; + uint256 public totalSupply; + mapping(address => uint256) public balanceOf; + mapping(address => mapping(address => uint256)) public allowance; + + constructor() { + owner = msg.sender; + } + + modifier onlyOwner() { + require(msg.sender == owner); + _; + } + + function _transfer(address _from, address _to, uint256 _amount) internal returns (bool) { + balanceOf[_from] -= _amount; + balanceOf[_to] += _amount; + return true; + } + + function transfer(address _to, uint256 _amount) public returns (bool) { + return _transfer(msg.sender, _to, _amount); + } + + function transferFrom(address _from, address _to, uint256 _amount) public returns (bool) { + allowance[_from][msg.sender] -= _amount; + return _transfer(_from, _to, _amount); + } + + function approve(address _spender, uint256 _amount) public { + allowance[msg.sender][_spender] = _amount; + } + + function mint(address _receiver, uint256 _amount) public onlyOwner { + balanceOf[_receiver] += _amount; + totalSupply += _amount; + } +} diff --git a/certora/dispatch/ERC20USDT.sol b/certora/dispatch/ERC20USDT.sol new file mode 100644 index 000000000..cce99353a --- /dev/null +++ b/certora/dispatch/ERC20USDT.sol @@ -0,0 +1,45 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +pragma solidity ^0.8.0; + +contract ERC20USDT { + address public owner; + uint256 public totalSupply; + mapping(address => uint256) public balanceOf; + mapping(address => mapping(address => uint256)) public allowance; + + constructor() { + owner = msg.sender; + } + + modifier onlyOwner() { + require(msg.sender == owner); + _; + } + + function _transfer(address _from, address _to, uint256 _amount) internal { + balanceOf[_from] -= _amount; + balanceOf[_to] += _amount; + } + + function transfer(address _to, uint256 _amount) public { + _transfer(msg.sender, _to, _amount); + } + + function transferFrom(address _from, address _to, uint256 _amount) public { + if (allowance[_from][msg.sender] < type(uint256).max) { + allowance[_from][msg.sender] -= _amount; + } + _transfer(_from, _to, _amount); + } + + function approve(address _spender, uint256 _amount) public { + require(!((_amount != 0) && (allowance[msg.sender][_spender] != 0))); + + allowance[msg.sender][_spender] = _amount; + } + + function mint(address _receiver, uint256 _amount) public onlyOwner { + balanceOf[_receiver] += _amount; + totalSupply += _amount; + } +} 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/harness/MorphoHarness.sol b/certora/harness/MorphoHarness.sol new file mode 100644 index 000000000..016cfcde1 --- /dev/null +++ b/certora/harness/MorphoHarness.sol @@ -0,0 +1,96 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +pragma solidity 0.8.19; + +import "../../src/Morpho.sol"; +import "../../src/libraries/SharesMathLib.sol"; +import "../../src/libraries/MarketParamsLib.sol"; + +contract MorphoHarness is Morpho { + using MarketParamsLib for MarketParams; + + constructor(address newOwner) Morpho(newOwner) {} + + function wad() external pure returns (uint256) { + return WAD; + } + + function maxFee() external pure returns (uint256) { + return MAX_FEE; + } + + function toMarketParams(Id id) external view returns (MarketParams memory) { + return idToMarketParams[id]; + } + + function totalSupplyAssets(Id id) external view returns (uint256) { + return market[id].totalSupplyAssets; + } + + function totalSupplyShares(Id id) external view returns (uint256) { + return market[id].totalSupplyShares; + } + + function totalBorrowAssets(Id id) external view returns (uint256) { + return market[id].totalBorrowAssets; + } + + function totalBorrowShares(Id id) external view returns (uint256) { + return market[id].totalBorrowShares; + } + + function supplyShares(Id id, address account) external view returns (uint256) { + return position[id][account].supplyShares; + } + + function borrowShares(Id id, address account) external view returns (uint256) { + return position[id][account].borrowShares; + } + + function collateral(Id id, address account) external view returns (uint256) { + return position[id][account].collateral; + } + + function lastUpdate(Id id) external view returns (uint256) { + return market[id].lastUpdate; + } + + function fee(Id id) external view returns (uint256) { + return market[id].fee; + } + + function virtualTotalSupplyAssets(Id id) external view returns (uint256) { + return market[id].totalSupplyAssets + SharesMathLib.VIRTUAL_ASSETS; + } + + function virtualTotalSupplyShares(Id id) external view returns (uint256) { + return market[id].totalSupplyShares + SharesMathLib.VIRTUAL_SHARES; + } + + function virtualTotalBorrowAssets(Id id) external view returns (uint256) { + return market[id].totalBorrowAssets + SharesMathLib.VIRTUAL_ASSETS; + } + + function virtualTotalBorrowShares(Id id) external view returns (uint256) { + return market[id].totalBorrowShares + SharesMathLib.VIRTUAL_SHARES; + } + + function libId(MarketParams memory marketParams) external pure returns (Id) { + return marketParams.id(); + } + + function refId(MarketParams memory marketParams) external pure returns (Id marketParamsId) { + marketParamsId = Id.wrap(keccak256(abi.encode(marketParams))); + } + + function libMulDivUp(uint256 x, uint256 y, uint256 d) external pure returns (uint256) { + return MathLib.mulDivUp(x, y, d); + } + + function libMulDivDown(uint256 x, uint256 y, uint256 d) external pure returns (uint256) { + return MathLib.mulDivDown(x, y, d); + } + + function isHealthy(MarketParams memory marketParams, address user) external view returns (bool) { + return _isHealthy(marketParams, marketParams.id(), user); + } +} diff --git a/certora/harness/MorphoInternalAccess.sol b/certora/harness/MorphoInternalAccess.sol new file mode 100644 index 000000000..a4f7ecfa1 --- /dev/null +++ b/certora/harness/MorphoInternalAccess.sol @@ -0,0 +1,17 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +pragma solidity 0.8.19; + +import "./MorphoHarness.sol"; + +contract MorphoInternalAccess is MorphoHarness { + constructor(address newOwner) MorphoHarness(newOwner) {} + + function update(Id id, uint256 timestamp) external { + market[id].lastUpdate = uint128(timestamp); + } + + function increaseInterest(Id id, uint128 interest) external { + market[id].totalBorrowAssets += interest; + market[id].totalSupplyAssets += interest; + } +} diff --git a/certora/harness/TransferHarness.sol b/certora/harness/TransferHarness.sol new file mode 100644 index 000000000..67a6d88c8 --- /dev/null +++ b/certora/harness/TransferHarness.sol @@ -0,0 +1,35 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +pragma solidity ^0.8.12; + +import "../../src/libraries/SafeTransferLib.sol"; +import "../../src/interfaces/IERC20.sol"; + +interface IERC20Extended is IERC20 { + function balanceOf(address) external view returns (uint256); + function allowance(address, address) external view returns (uint256); + function totalSupply() external view returns (uint256); +} + +contract TransferHarness { + using SafeTransferLib for IERC20; + + function libSafeTransferFrom(address token, address from, address to, uint256 value) external { + IERC20(token).safeTransferFrom(from, to, value); + } + + function libSafeTransfer(address token, address to, uint256 value) external { + IERC20(token).safeTransfer(to, value); + } + + function balanceOf(address token, address user) external view returns (uint256) { + return IERC20Extended(token).balanceOf(user); + } + + function allowance(address token, address owner, address spender) external view returns (uint256) { + return IERC20Extended(token).allowance(owner, spender); + } + + function totalSupply(address token) external view returns (uint256) { + return IERC20Extended(token).totalSupply(); + } +} diff --git a/certora/specs/AccrueInterest.spec b/certora/specs/AccrueInterest.spec new file mode 100644 index 000000000..7babf38de --- /dev/null +++ b/certora/specs/AccrueInterest.spec @@ -0,0 +1,138 @@ +// 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; + 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; + function _.onMorphoLiquidate(uint256, bytes) external => NONDET; + function _.onMorphoRepay(uint256, bytes) external => NONDET; + function _.onMorphoSupply(uint256, bytes) external => NONDET; + function _.onMorphoSupplyCollateral(uint256, bytes) external => NONDET; + function _.onMorphoFlashLoan(uint256, bytes) external => NONDET; +} + +ghost ghostMulDivUp(uint256, uint256, uint256) returns uint256; +ghost ghostMulDivDown(uint256, uint256, uint256) returns uint256; +ghost ghostTaylorCompounded(uint256, uint256) returns uint256; +ghost ghostBorrowRate(address, uint256) returns uint256; +ghost ghostOraclePrice(uint256) returns uint256; +ghost ghostTransfer(address, uint256) returns bool; +ghost ghostTransferFrom(address, address, uint256) returns bool; + + +// Check that calling accrueInterest first has no effect. +// This is because supply should call accrueInterest itself. +rule supplyAccruesInterest(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { + // Safe require because timestamps cannot realistically be that large. + require e.block.timestamp < 2^128; + + storage init = lastStorage; + + accrueInterest(e, marketParams); + supply(e, marketParams, assets, shares, onBehalf, data); + storage afterBoth = lastStorage; + + supply(e, marketParams, assets, shares, onBehalf, data) at init; + storage afterOne = lastStorage; + + assert afterBoth == afterOne; +} + +// Check that calling accrueInterest first has no effect. +// This is because withdraw should call accrueInterest itself. +rule withdrawAccruesInterest(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) { + // Safe require because timestamps cannot realistically be that large. + require e.block.timestamp < 2^128; + + storage init = lastStorage; + + accrueInterest(e, marketParams); + withdraw(e, marketParams, assets, shares, onBehalf, receiver); + storage afterBoth = lastStorage; + + withdraw(e, marketParams, assets, shares, onBehalf, receiver) at init; + storage afterOne = lastStorage; + + assert afterBoth == afterOne; +} + +// Check that calling accrueInterest first has no effect. +// This is because borrow should call accrueInterest itself. +rule borrowAccruesInterest(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) { + // Safe require because timestamps cannot realistically be that large. + require e.block.timestamp < 2^128; + + storage init = lastStorage; + + accrueInterest(e, marketParams); + borrow(e, marketParams, assets, shares, onBehalf, receiver); + storage afterBoth = lastStorage; + + borrow(e, marketParams, assets, shares, onBehalf, receiver) at init; + storage afterOne = lastStorage; + + assert afterBoth == afterOne; +} + +// Check that calling accrueInterest first has no effect. +// This is because repay should call accrueInterest itself. +rule repayAccruesInterest(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { + // Safe require because timestamps cannot realistically be that large. + require e.block.timestamp < 2^128; + + storage init = lastStorage; + + accrueInterest(e, marketParams); + repay(e, marketParams, assets, shares, onBehalf, data); + storage afterBoth = lastStorage; + + repay(e, marketParams, assets, shares, onBehalf, data) at init; + storage afterOne = lastStorage; + + assert afterBoth == afterOne; +} + +// 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 accrueInterest is called. +// We also exclude setFeeRecipient, as it is known to be not commutative. +rule accrueInterestCommutesExceptForSetFeeRecipient(method f, calldataarg args) +filtered { + f -> !f.isView && f.selector != sig:setFeeRecipient(address).selector +} +{ + env e1; + env e2; + MorphoHarness.MarketParams marketParams; + + // Assume interactions to happen at the same block. + require e1.block.timestamp == e2.block.timestamp; + // Safe require because timestamps cannot realistically be that large. + require e1.block.timestamp < 2^128; + + storage init = lastStorage; + + accrueInterest(e1, marketParams); + f@withrevert(e2, args); + bool revert1 = lastReverted; + storage store1 = lastStorage; + + + f@withrevert(e2, args) at init; + bool revert2 = lastReverted; + accrueInterest(e1, marketParams); + storage store2 = lastStorage; + + assert revert1 <=> revert2; + assert store1 == store2; +} diff --git a/certora/specs/AssetsAccounting.spec b/certora/specs/AssetsAccounting.spec new file mode 100644 index 000000000..007500b6d --- /dev/null +++ b/certora/specs/AssetsAccounting.spec @@ -0,0 +1,126 @@ +// 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 virtualTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree; + 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; + function libMulDivUp(uint256, uint256, uint256) external returns uint256 envfree; + function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; +} + +function expectedSupplyAssets(MorphoHarness.Id id, address user) returns uint256 { + uint256 userShares = supplyShares(id, user); + uint256 totalSupplyAssets = virtualTotalSupplyAssets(id); + uint256 totalSupplyShares = virtualTotalSupplyShares(id); + + return libMulDivDown(userShares, totalSupplyAssets, totalSupplyShares); +} + +function expectedBorrowAssets(MorphoHarness.Id id, address user) returns uint256 { + uint256 userShares = borrowShares(id, user); + uint256 totalBorrowAssets = virtualTotalBorrowAssets(id); + uint256 totalBorrowShares = virtualTotalBorrowShares(id); + + return libMulDivUp(userShares, totalBorrowAssets, totalBorrowShares); +} + +// Check that the assets supplied are greater than the assets owned in the end. +rule supplyAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { + MorphoHarness.Id id = libId(marketParams); + + // Assume no interest as it would increase the total supply assets. + require lastUpdate(id) == e.block.timestamp; + // Assume no supply position to begin with. + require supplyShares(id, onBehalf) == 0; + + uint256 suppliedAssets; + suppliedAssets, _ = supply(e, marketParams, assets, shares, onBehalf, data); + + uint256 ownedAssets = expectedSupplyAssets(id, onBehalf); + + assert suppliedAssets >= ownedAssets; +} + +// Check that the assets withdrawn are less than the assets owned initially. +rule withdrawAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) { + MorphoHarness.Id id = libId(marketParams); + + // Assume no interest as it would increase the total supply assets. + require lastUpdate(id) == e.block.timestamp; + + uint256 ownedAssets = expectedSupplyAssets(id, onBehalf); + + uint256 withdrawnAssets; + withdrawnAssets, _ = withdraw(e, marketParams, assets, shares, onBehalf, receiver); + + assert withdrawnAssets <= ownedAssets; +} + +// Check that the assets borrowed are less than the assets owed in the end. +rule borrowAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 shares, address onBehalf, address receiver) { + MorphoHarness.Id id = libId(marketParams); + + // Assume no interest as it would increase the total borrowed assets. + require lastUpdate(id) == e.block.timestamp; + // Assume no outstanding debt to begin with. + require borrowShares(id, onBehalf) == 0; + + // The borrow call is restricted to shares as input to make it easier on the prover. + uint256 borrowedAssets; + borrowedAssets, _ = borrow(e, marketParams, 0, shares, onBehalf, receiver); + + uint256 owedAssets = expectedBorrowAssets(id, onBehalf); + + assert borrowedAssets <= owedAssets; +} + +// Check that the assets repaid are greater than the assets owed initially. +rule repayAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { + MorphoHarness.Id id = libId(marketParams); + + // Assume no interest as it would increase the total borrowed assets. + require lastUpdate(id) == e.block.timestamp; + + uint256 owedAssets = expectedBorrowAssets(id, onBehalf); + + uint256 repaidAssets; + repaidAssets, _ = repay(e, marketParams, assets, shares, onBehalf, data); + + // Assume a full repay. + require borrowShares(id, onBehalf) == 0; + + assert repaidAssets >= owedAssets; +} + +// Check that the collateral assets supplied are greater than the assets owned in the end. +rule supplyCollateralAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 suppliedAssets, address onBehalf, bytes data) { + MorphoHarness.Id id = libId(marketParams); + + // Assume no collateral to begin with. + require collateral(id, onBehalf) == 0; + + supplyCollateral(e, marketParams, suppliedAssets, onBehalf, data); + + uint256 ownedAssets = collateral(id, onBehalf); + + assert suppliedAssets == ownedAssets; +} + +// Check that the collateral assets withdrawn are less than the assets owned initially. +rule withdrawCollateralAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 withdrawnAssets, address onBehalf, address receiver) { + MorphoHarness.Id id = libId(marketParams); + + uint256 ownedAssets = collateral(id, onBehalf); + + withdrawCollateral(e, marketParams, withdrawnAssets, onBehalf, receiver); + + assert withdrawnAssets <= ownedAssets; +} diff --git a/certora/specs/ConsistentState.spec b/certora/specs/ConsistentState.spec new file mode 100644 index 000000000..d84995d8d --- /dev/null +++ b/certora/specs/ConsistentState.spec @@ -0,0 +1,292 @@ +// 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 fee(MorphoHarness.Id) external returns uint256 envfree; + function lastUpdate(MorphoHarness.Id) external returns uint256 envfree; + function isIrmEnabled(address) external returns bool envfree; + function isLltvEnabled(uint256) external returns bool envfree; + function isAuthorized(address, address) external returns bool envfree; + function toMarketParams(MorphoHarness.Id) external returns MorphoHarness.MarketParams envfree; + + function 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); +} + +persistent ghost mapping(MorphoHarness.Id => mathint) sumSupplyShares { + init_state axiom (forall MorphoHarness.Id id. sumSupplyShares[id] == 0); +} + +persistent ghost mapping(MorphoHarness.Id => mathint) sumBorrowShares { + init_state axiom (forall MorphoHarness.Id id. sumBorrowShares[id] == 0); +} + +persistent ghost mapping(MorphoHarness.Id => mathint) sumCollateral { + init_state axiom (forall MorphoHarness.Id id. sumCollateral[id] == 0); +} + +persistent ghost mapping(address => mathint) balance { + init_state axiom (forall address token. balance[token] == 0); +} + +persistent ghost mapping(address => mathint) idleAmount { + init_state axiom (forall address token. idleAmount[token] == 0); +} + +hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].supplyShares uint256 newShares (uint256 oldShares) STORAGE { + sumSupplyShares[id] = sumSupplyShares[id] - oldShares + newShares; +} + +hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].borrowShares uint128 newShares (uint128 oldShares) STORAGE { + sumBorrowShares[id] = sumBorrowShares[id] - oldShares + newShares; +} + +hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].collateral uint128 newAmount (uint128 oldAmount) STORAGE { + sumCollateral[id] = sumCollateral[id] - oldAmount + newAmount; + idleAmount[toMarketParams(id).collateralToken] = idleAmount[toMarketParams(id).collateralToken] - oldAmount + newAmount; +} + +hook Sstore market[KEY MorphoHarness.Id id].totalSupplyAssets uint128 newAmount (uint128 oldAmount) STORAGE { + idleAmount[toMarketParams(id).loanToken] = idleAmount[toMarketParams(id).loanToken] - oldAmount + newAmount; +} + +hook Sstore market[KEY MorphoHarness.Id id].totalBorrowAssets uint128 newAmount (uint128 oldAmount) STORAGE { + idleAmount[toMarketParams(id).loanToken] = idleAmount[toMarketParams(id).loanToken] + oldAmount - newAmount; +} + +function summarySafeTransferFrom(address token, address from, address to, uint256 amount) { + if (from == currentContract) { + // Safe require because the reference implementation would revert. + balance[token] = require_uint256(balance[token] - amount); + } + if (to == currentContract) { + // Safe require because the reference implementation would revert. + balance[token] = require_uint256(balance[token] + amount); + } +} + +definition isCreated(MorphoHarness.Id id) returns bool = + lastUpdate(id) != 0; + +// Check that the fee is always lower than the max fee constant. +invariant feeInRange(MorphoHarness.Id id) + fee(id) <= maxFee(); + +// Check that the accounting of totalSupplyShares is correct. +invariant sumSupplySharesCorrect(MorphoHarness.Id id) + to_mathint(totalSupplyShares(id)) == sumSupplyShares[id]; + +// Check that the accounting of totalBorrowShares is correct. +invariant sumBorrowSharesCorrect(MorphoHarness.Id id) + to_mathint(totalBorrowShares(id)) == sumBorrowShares[id]; + +// Check that a market only allows borrows up to the total supply. +// This invariant shows that markets are independent, tokens from one market cannot be taken by interacting with another market. +invariant borrowLessThanSupply(MorphoHarness.Id id) + totalBorrowAssets(id) <= totalSupplyAssets(id); + +// Check correctness of applying idToMarketParams() to an identifier. +invariant hashOfMarketParamsOf(MorphoHarness.Id id) + isCreated(id) => + libId(toMarketParams(id)) == id; + +// Check correctness of applying id() to a market params. +// This invariant is useful in the following rule, to link an id back to a market. +invariant marketParamsOfHashOf(MorphoHarness.MarketParams marketParams) + isCreated(libId(marketParams)) => + toMarketParams(libId(marketParams)).loanToken == marketParams.loanToken && + toMarketParams(libId(marketParams)).collateralToken == marketParams.collateralToken && + toMarketParams(libId(marketParams)).oracle == marketParams.oracle && + toMarketParams(libId(marketParams)).lltv == marketParams.lltv && + toMarketParams(libId(marketParams)).irm == marketParams.irm; + +// Check that the idle amount on the singleton is greater to the sum amount, that is the sum over all the markets of the total supply plus the total collateral minus the total borrow. +invariant idleAmountLessThanBalance(address token) + idleAmount[token] <= balance[token] +{ + // Safe requires on the sender because the contract cannot call the function itself. + preserved supply(MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) with (env e) { + requireInvariant marketParamsOfHashOf(marketParams); + require e.msg.sender != currentContract; + } + preserved withdraw(MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) with (env e) { + requireInvariant marketParamsOfHashOf(marketParams); + require e.msg.sender != currentContract; + } + preserved borrow(MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) with (env e) { + requireInvariant marketParamsOfHashOf(marketParams); + require e.msg.sender != currentContract; + } + preserved repay(MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) with (env e) { + requireInvariant marketParamsOfHashOf(marketParams); + require e.msg.sender != currentContract; + } + preserved supplyCollateral(MorphoHarness.MarketParams marketParams, uint256 assets, address onBehalf, bytes data) with (env e) { + requireInvariant marketParamsOfHashOf(marketParams); + require e.msg.sender != currentContract; + } + preserved withdrawCollateral(MorphoHarness.MarketParams marketParams, uint256 assets, address onBehalf, address receiver) with (env e) { + requireInvariant marketParamsOfHashOf(marketParams); + require e.msg.sender != currentContract; + } + preserved liquidate(MorphoHarness.MarketParams marketParams, address _b, uint256 shares, uint256 receiver, bytes data) with (env e) { + requireInvariant marketParamsOfHashOf(marketParams); + require e.msg.sender != currentContract; + } +} + +// Check that a market can only exist if its LLTV is enabled. +invariant onlyEnabledLltv(MorphoHarness.MarketParams marketParams) + isCreated(libId(marketParams)) => isLltvEnabled(marketParams.lltv); + +invariant lltvSmallerThanWad(uint256 lltv) + isLltvEnabled(lltv) => lltv < wad(); + +// Check that a market can only exist if its IRM is enabled. +invariant onlyEnabledIrm(MorphoHarness.MarketParams marketParams) + isCreated(libId(marketParams)) => isIrmEnabled(marketParams.irm); + +// Check the pseudo-injectivity of the hashing function id(). +rule libIdUnique() { + MorphoHarness.MarketParams marketParams1; + MorphoHarness.MarketParams marketParams2; + + // Assume that arguments are the same. + require libId(marketParams1) == libId(marketParams2); + + assert marketParams1.loanToken == marketParams2.loanToken; + assert marketParams1.collateralToken == marketParams2.collateralToken; + assert marketParams1.oracle == marketParams2.oracle; + assert marketParams1.irm == marketParams2.irm; + assert marketParams1.lltv == marketParams2.lltv; +} + +// Check that only the user is able to change who is authorized to manage his position. +rule onlyUserCanAuthorizeWithoutSig(env e, method f, calldataarg data) +filtered { + f -> !f.isView && f.selector != sig:setAuthorizationWithSig(MorphoHarness.Authorization memory, MorphoHarness.Signature calldata).selector +} +{ + address user; + address someone; + + // Assume that it is another user that is interacting with Morpho. + require user != e.msg.sender; + + bool authorizedBefore = isAuthorized(user, someone); + + f(e, data); + + bool authorizedAfter = isAuthorized(user, someone); + + assert authorizedAfter == authorizedBefore; +} + +// Check that only authorized users are able to decrease supply shares of a position. +rule userCannotLoseSupplyShares(env e, method f, calldataarg data) +filtered { f -> !f.isView } +{ + MorphoHarness.Id id; + address user; + + // Assume that the e.msg.sender is not authorized. + require !isAuthorized(user, e.msg.sender); + require user != e.msg.sender; + + mathint sharesBefore = supplyShares(id, user); + + f(e, data); + + mathint sharesAfter = supplyShares(id, user); + + assert sharesAfter >= sharesBefore; +} + +// Check that only authorized users are able to increase the borrow shares of a position. +rule userCannotGainBorrowShares(env e, method f, calldataarg args) +filtered { f -> !f.isView } +{ + MorphoHarness.Id id; + address user; + + // Assume that the e.msg.sender is not authorized. + require !isAuthorized(user, e.msg.sender); + require user != e.msg.sender; + + mathint sharesBefore = borrowShares(id, user); + + f(e, args); + + mathint sharesAfter = borrowShares(id, user); + + assert sharesAfter <= sharesBefore; +} + +// Check that users cannot lose collateral by unauthorized parties except in case of a liquidation. +rule userCannotLoseCollateralExceptLiquidate(env e, method f, calldataarg args) +filtered { + f -> !f.isView && + f.selector != sig:liquidate(MorphoHarness.MarketParams, address, uint256, uint256, bytes).selector +} +{ + MorphoHarness.Id id; + address user; + + // Assume that the e.msg.sender is not authorized. + require !isAuthorized(user, e.msg.sender); + require user != e.msg.sender; + + mathint collateralBefore = collateral(id, user); + + f(e, args); + + mathint collateralAfter = collateral(id, user); + + assert collateralAfter >= collateralBefore; +} + +// Check that users cannot lose collateral by unauthorized parties if they have no outstanding debt. +rule userWithoutBorrowCannotLoseCollateral(env e, method f, calldataarg args) +filtered { f -> !f.isView } +{ + MorphoHarness.Id id; + address user; + + // Assume that the e.msg.sender is not authorized. + require !isAuthorized(user, e.msg.sender); + require user != e.msg.sender; + // Assume that the user has no outstanding debt. + require borrowShares(id, user) == 0; + + mathint collateralBefore = collateral(id, user); + + f(e, args); + + mathint collateralAfter = collateral(id, user); + + assert collateralAfter >= collateralBefore; +} + +// Invariant checking that the last updated time is never greater than the current time. +rule noTimeTravel(method f, env e, calldataarg args) +filtered { f -> !f.isView } +{ + MorphoHarness.Id id; + // Assume the property before the interaction. + require lastUpdate(id) <= e.block.timestamp; + f(e, args); + assert lastUpdate(id) <= e.block.timestamp; +} diff --git a/certora/specs/ExactMath.spec b/certora/specs/ExactMath.spec new file mode 100644 index 000000000..d25465c25 --- /dev/null +++ b/certora/specs/ExactMath.spec @@ -0,0 +1,123 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +methods { + function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; + + function feeRecipient() external returns address envfree; + function supplyShares(MorphoHarness.Id, address) external returns uint256 envfree; + function borrowShares(MorphoHarness.Id, address) external returns uint256 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; + function virtualTotalBorrowShares(MorphoHarness.Id) external returns uint256 envfree; + function lastUpdate(MorphoHarness.Id) external returns uint256 envfree; + function fee(MorphoHarness.Id) external returns uint256 envfree; + + function maxFee() external returns uint256 envfree; + function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; + + function 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 summaryMulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 { + // Safe require because the reference implementation would revert. + return require_uint256((x * y + (d - 1)) / d); +} + +function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 { + // Safe require because the reference implementation would revert. + return require_uint256((x * y) / d); +} + +// Check that when not accruing interest, and when repaying all, the borrow ratio is at least reset to the initial ratio. +// More details on the purpose of this rule in RatioMath.spec. +rule repayAllResetsBorrowRatio(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { + MorphoHarness.Id id = libId(marketParams); + // Safe require because this invariant is checked in ConsistentState.spec + require fee(id) <= maxFee(); + + mathint assetsBefore = virtualTotalBorrowAssets(id); + mathint sharesBefore = virtualTotalBorrowShares(id); + + // Assume no interest as it would increase the borrowed assets. + require lastUpdate(id) == e.block.timestamp; + + mathint repaidAssets; + repaidAssets, _ = repay(e, marketParams, assets, shares, onBehalf, data); + + // Check the case where the market is fully repaid. + require repaidAssets >= assetsBefore; + + mathint assetsAfter = virtualTotalBorrowAssets(id); + mathint sharesAfter = virtualTotalBorrowShares(id); + + assert assetsAfter == 1; + // There are at least as many shares as virtual shares. +} + +// There should be no profit from supply followed immediately by withdraw. +rule supplyWithdraw() { + MorphoHarness.MarketParams marketParams; + MorphoHarness.Id id = libId(marketParams); + env e1; + env e2; + address onBehalf; + + // Assume that interactions happen at the same block. + require e1.block.timestamp == e2.block.timestamp; + // Assume that the user starts without any supply position. + require supplyShares(id, onBehalf) == 0; + // Assume that the user is not the fee recipient, otherwise the gain can come from the fee. + require onBehalf != feeRecipient(); + // Safe require because timestamps cannot realistically be that large. + require e1.block.timestamp < 2^128; + + uint256 supplyAssets; uint256 supplyShares; bytes data; + uint256 suppliedAssets; + uint256 suppliedShares; + suppliedAssets, suppliedShares = supply(e1, marketParams, supplyAssets, supplyShares, onBehalf, data); + + // Hints for the prover. + assert suppliedAssets * (virtualTotalSupplyShares(id) - suppliedShares) >= suppliedShares * (virtualTotalSupplyAssets(id) - suppliedAssets); + assert suppliedAssets * virtualTotalSupplyShares(id) >= suppliedShares * virtualTotalSupplyAssets(id); + + uint256 withdrawAssets; uint256 withdrawShares; address receiver; + uint256 withdrawnAssets; + withdrawnAssets, _ = withdraw(e2, marketParams, withdrawAssets, withdrawShares, onBehalf, receiver); + + assert withdrawnAssets <= suppliedAssets; +} + +// There should be no profit from borrow followed immediately by repaying all. +rule borrowRepay() { + MorphoHarness.MarketParams marketParams; + MorphoHarness.Id id = libId(marketParams); + address onBehalf; + env e1; + env e2; + + // Assume interactions happen at the same block. + require e1.block.timestamp == e2.block.timestamp; + // Assume that the user starts without any borrow position. + require borrowShares(id, onBehalf) == 0; + // Safe require because timestamps cannot realistically be that large. + require e1.block.timestamp < 2^128; + + uint256 borrowAssets; uint256 borrowShares; address receiver; + uint256 borrowedAssets; + uint256 borrowedShares; + borrowedAssets, borrowedShares = borrow(e2, marketParams, borrowAssets, borrowShares, onBehalf, receiver); + + // Hints for the prover. + assert borrowedAssets * (virtualTotalBorrowShares(id) - borrowedShares) <= borrowedShares * (virtualTotalBorrowAssets(id) - borrowedAssets); + assert borrowedAssets * virtualTotalBorrowShares(id) <= borrowedShares * virtualTotalBorrowAssets(id); + + bytes data; + uint256 repaidAssets; + repaidAssets, _ = repay(e1, marketParams, 0, borrowedShares, onBehalf, data); + + assert borrowedAssets <= repaidAssets; +} diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec new file mode 100644 index 000000000..45c535187 --- /dev/null +++ b/certora/specs/Health.spec @@ -0,0 +1,134 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +methods { + function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; + + 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 isAuthorized(address, address user) external returns bool envfree; + function lastUpdate(MorphoHarness.Id) external returns uint256 envfree; + + function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; + function 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); + function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivUp(a,b,c); + function UtilsLib.min(uint256 a, uint256 b) internal returns uint256 => summaryMin(a,b); +} + +persistent ghost uint256 lastPrice; +persistent ghost bool priceChanged; + +function mockPrice() returns uint256 { + uint256 updatedPrice; + if (updatedPrice != lastPrice) { + priceChanged = true; + lastPrice = updatedPrice; + } + return updatedPrice; +} + +function summaryMulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 { + // Safe require because the reference implementation would revert. + require d != 0; + return require_uint256((x * y + (d - 1)) / d); +} + +function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 { + // Safe require because the reference implementation would revert. + require d != 0; + return require_uint256((x * y) / d); +} + +function summaryMin(uint256 a, uint256 b) returns uint256 { + return a < b ? a : b; +} + +// Check that without accruing interest, no interaction can put an healthy account into an unhealthy one. +// This rule times out for liquidate, repay and borrow. +rule stayHealthy(env e, method f, calldataarg data) +filtered { + 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.MarketParams marketParams; + MorphoHarness.Id id = libId(marketParams); + address user; + + // Assume that the position is healthy before the interaction. + require isHealthy(marketParams, user); + // Safe require because of the invariants onlyEnabledLltv and lltvSmallerThanWad in ConsistentState.spec. + require marketParams.lltv < 10^18; + // Assumption to ensure that no interest is accumulated. + require lastUpdate(id) == e.block.timestamp; + + priceChanged = false; + f(e, data); + + // Safe require because of the invariant sumBorrowSharesCorrect. + require borrowShares(id, user) <= totalBorrowShares(id); + + bool stillHealthy = isHealthy(marketParams, user); + assert !priceChanged => stillHealthy; +} + +// Check that users cannot lose collateral by unauthorized parties except in case of an unhealthy position. +rule healthyUserCannotLoseCollateral(env e, method f, calldataarg data) +filtered { f -> !f.isView } +{ + MorphoHarness.MarketParams marketParams; + MorphoHarness.Id id = libId(marketParams); + address user; + + // Assume that the e.msg.sender is not authorized. + require !isAuthorized(user, e.msg.sender); + require user != e.msg.sender; + // Assumption to ensure that no interest is accumulated. + require lastUpdate(id) == e.block.timestamp; + // Assume that the user is healthy. + require isHealthy(marketParams, user); + + mathint collateralBefore = collateral(id, user); + + priceChanged = false; + f(e, data); + + mathint collateralAfter = collateral(id, user); + + assert !priceChanged => collateralAfter >= collateralBefore; +} + +// Check that users without collateral also have no debt. +// This invariant ensures that bad debt realization cannot be bypassed. +invariant alwaysCollateralized(MorphoHarness.Id id, address borrower) + borrowShares(id, borrower) != 0 => collateral(id, borrower) != 0; + +// Checks that passing a seized amount input to liquidate leads to repaid shares S and repaid amount A such that liquidating instead with shares S also repays the amount A. +rule liquidateEquivalentInputDebtAndInputCollateral(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) { + MorphoHarness.Id id = libId(marketParams); + + // Assume no interest accrual to ease the verification. + require lastUpdate(id) == e.block.timestamp; + + storage init = lastStorage; + uint256 sharesBefore = borrowShares(id, borrower); + + uint256 repaidAssets1; + _, repaidAssets1 = liquidate(e, marketParams, borrower, seizedAssets, 0, data); + require !priceChanged; + // Omit the bad debt realization case. + require collateral(id, borrower) != 0; + uint256 sharesAfter = borrowShares(id, borrower); + uint256 repaidShares1 = assert_uint256(sharesBefore - sharesAfter); + + uint256 repaidAssets2; + _, repaidAssets2 = liquidate(e, marketParams, borrower, 0, repaidShares1, data) at init; + require !priceChanged; + + assert repaidAssets1 == repaidAssets2; +} diff --git a/certora/specs/LibSummary.spec b/certora/specs/LibSummary.spec new file mode 100644 index 000000000..030e89140 --- /dev/null +++ b/certora/specs/LibSummary.spec @@ -0,0 +1,26 @@ +// 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; + function refId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; +} + +// Check the summary of MathLib.mulDivUp required by RatioMath.spec +rule checkSummaryMulDivUp(uint256 x, uint256 y, uint256 d) { + uint256 result = libMulDivUp(x, y, d); + assert result * d >= x * y; +} + +// Check the summary of MathLib.mulDivDown required by RatioMath.spec +rule checkSummaryMulDivDown(uint256 x, uint256 y, uint256 d) { + uint256 result = libMulDivDown(x, y, d); + assert result * d <= x * y; +} + +// Check the summary of MarketParamsLib.id required by Liveness.spec +rule checkSummaryId(MorphoHarness.MarketParams marketParams) { + assert libId(marketParams) == refId(marketParams); +} diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec new file mode 100644 index 000000000..e6a78ed6a --- /dev/null +++ b/certora/specs/Liveness.spec @@ -0,0 +1,386 @@ +// 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 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; + + function _._accrueInterest(MorphoInternalAccess.MarketParams memory marketParams, MorphoInternalAccess.Id id) internal with (env e) => summaryAccrueInterest(e, marketParams, id) expect void; + + function MarketParamsLib.id(MorphoInternalAccess.MarketParams memory marketParams) internal returns MorphoInternalAccess.Id => summaryId(marketParams); + 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); +} + +persistent ghost mapping(address => mathint) balance { + init_state axiom (forall address token. balance[token] == 0); +} + +function summaryId(MorphoInternalAccess.MarketParams marketParams) returns MorphoInternalAccess.Id { + return refId(marketParams); +} + +function summarySafeTransferFrom(address token, address from, address to, uint256 amount) { + if (from == currentContract) { + // Safe require because the reference implementation would revert. + balance[token] = require_uint256(balance[token] - amount); + } + if (to == currentContract) { + // Safe require because the reference implementation would revert. + balance[token] = require_uint256(balance[token] + amount); + } +} + +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) { + // Safe require because timestamps cannot realistically be that large. + require e.block.timestamp < 2^128; + if (e.block.timestamp != lastUpdate(id) && totalBorrowAssets(id) != 0) { + uint128 interest; + uint256 supply = totalSupplyAssets(id); + // Safe require because the reference implementation would revert. + require interest + supply < 2^256; + increaseInterest(e, id, interest); + } + + update(e, id, e.block.timestamp); +} + +definition isCreated(MorphoInternalAccess.Id id) returns bool = + lastUpdate(id) != 0; + +// Check that tokens and shares are properly accounted following a supply. +rule supplyChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { + MorphoInternalAccess.Id id = libId(marketParams); + + // Safe require because Morpho cannot call such functions by itself. + require currentContract != e.msg.sender; + // Assumption to ensure that no interest is accumulated. + require lastUpdate(id) == e.block.timestamp; + + mathint sharesBefore = supplyShares(id, onBehalf); + mathint balanceBefore = balance[marketParams.loanToken]; + mathint liquidityBefore = totalSupplyAssets(id) - totalBorrowAssets(id); + + uint256 suppliedAssets; + uint256 suppliedShares; + suppliedAssets, suppliedShares = supply(e, marketParams, assets, shares, onBehalf, data); + + mathint sharesAfter = supplyShares(id, onBehalf); + mathint balanceAfter = balance[marketParams.loanToken]; + mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id); + + assert assets != 0 => suppliedAssets == assets; + 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; + suppliedAssets, _ = supply(e, marketParams, 0, shares, onBehalf, data); + + satisfy suppliedAssets != 0; +} + +// Check that tokens and shares are properly accounted following a withdraw. +rule withdrawChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) { + MorphoInternalAccess.Id id = libId(marketParams); + + // Assume that Morpho is not the receiver. + require currentContract != receiver; + // Assumption to ensure that no interest is accumulated. + require lastUpdate(id) == e.block.timestamp; + + mathint sharesBefore = supplyShares(id, onBehalf); + mathint balanceBefore = balance[marketParams.loanToken]; + mathint liquidityBefore = totalSupplyAssets(id) - totalBorrowAssets(id); + + uint256 withdrawnAssets; + uint256 withdrawnShares; + withdrawnAssets, withdrawnShares = withdraw(e, marketParams, assets, shares, onBehalf, receiver); + + mathint sharesAfter = supplyShares(id, onBehalf); + mathint balanceAfter = balance[marketParams.loanToken]; + mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id); + + assert assets != 0 => withdrawnAssets == assets; + 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; + withdrawnAssets, _ = withdraw(e, marketParams, 0, shares, onBehalf, receiver); + + satisfy withdrawnAssets != 0; +} + +// Check that tokens and shares are properly accounted following a borrow. +rule borrowChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) { + MorphoInternalAccess.Id id = libId(marketParams); + + // Assume that Morpho is not the receiver. + require currentContract != receiver; + // Assumption to ensure that no interest is accumulated. + require lastUpdate(id) == e.block.timestamp; + + mathint sharesBefore = borrowShares(id, onBehalf); + mathint balanceBefore = balance[marketParams.loanToken]; + mathint liquidityBefore = totalSupplyAssets(id) - totalBorrowAssets(id); + + uint256 borrowedAssets; + uint256 borrowedShares; + borrowedAssets, borrowedShares = borrow(e, marketParams, assets, shares, onBehalf, receiver); + + mathint sharesAfter = borrowShares(id, onBehalf); + mathint balanceAfter = balance[marketParams.loanToken]; + mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id); + + assert assets != 0 => borrowedAssets == assets; + 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; + borrowedAssets, _ = borrow(e, marketParams, 0, shares, onBehalf, receiver); + + satisfy borrowedAssets != 0; +} + +// Check that tokens and shares are properly accounted following a repay. +rule repayChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { + MorphoInternalAccess.Id id = libId(marketParams); + + // Safe require because Morpho cannot call such functions by itself. + require currentContract != e.msg.sender; + // Assumption to ensure that no interest is accumulated. + require lastUpdate(id) == e.block.timestamp; + + mathint sharesBefore = borrowShares(id, onBehalf); + mathint balanceBefore = balance[marketParams.loanToken]; + mathint liquidityBefore = totalSupplyAssets(id) - totalBorrowAssets(id); + + mathint borrowAssetsBefore = totalBorrowAssets(id); + + uint256 repaidAssets; + uint256 repaidShares; + repaidAssets, repaidShares = repay(e, marketParams, assets, shares, onBehalf, data); + + mathint sharesAfter = borrowShares(id, onBehalf); + mathint balanceAfter = balance[marketParams.loanToken]; + mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id); + + assert assets != 0 => repaidAssets == assets; + 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; + repaidAssets, _ = repay(e, marketParams, 0, shares, onBehalf, data); + + satisfy repaidAssets != 0; +} + +// Check that tokens and balances are properly accounted following a supplyCollateral. +rule supplyCollateralChangesTokensAndBalance(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, address onBehalf, bytes data) { + MorphoInternalAccess.Id id = libId(marketParams); + + // Safe require because Morpho cannot call such functions by itself. + require currentContract != e.msg.sender; + + mathint collateralBefore = collateral(id, onBehalf); + mathint balanceBefore = balance[marketParams.collateralToken]; + + supplyCollateral(e, marketParams, assets, onBehalf, data); + + mathint collateralAfter = collateral(id, onBehalf); + mathint balanceAfter = balance[marketParams.collateralToken]; + + assert collateralAfter == collateralBefore + assets; + assert balanceAfter == balanceBefore + assets; +} + +// Check that tokens and balances are properly accounted following a withdrawCollateral. +rule withdrawCollateralChangesTokensAndBalance(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, address onBehalf, address receiver) { + MorphoInternalAccess.Id id = libId(marketParams); + + // Assume that Morpho is not the receiver. + require currentContract != receiver; + // Assumption to ensure that no interest is accumulated. + require lastUpdate(id) == e.block.timestamp; + + mathint collateralBefore = collateral(id, onBehalf); + mathint balanceBefore = balance[marketParams.collateralToken]; + + withdrawCollateral(e, marketParams, assets, onBehalf, receiver); + + mathint collateralAfter = collateral(id, onBehalf); + mathint balanceAfter = balance[marketParams.collateralToken]; + + assert collateralAfter == collateralBefore - assets; + 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 = balance[marketParams.loanToken]; + mathint balanceCollateralBefore = balance[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 = balance[marketParams.loanToken]; + mathint balanceCollateralAfter = balance[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 you can liquidate non-zero tokens by passing shares. +rule canLiquidateByPassingShares(env e, MorphoInternalAccess.MarketParams marketParams, address borrower, uint256 repaidShares, bytes data) { + uint256 seizedAssets; + uint256 repaidAssets; + seizedAssets, repaidAssets = liquidate(e, marketParams, borrower, 0, repaidShares, data); + + satisfy seizedAssets != 0 && repaidAssets != 0; +} + +// 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); + + // Assume no callback, which still allows to repay all. + require data.length == 0; + + // Assume a full repay. + require shares == borrowShares(id, e.msg.sender); + // Omit sanity checks. + require isCreated(id); + require e.msg.sender != 0; + require e.msg.value == 0; + require shares > 0; + // Safe require because of the noTimeTravel rule. + require lastUpdate(id) <= e.block.timestamp; + // Safe require because of the sumBorrowSharesCorrect invariant. + require shares <= totalBorrowShares(id); + + // Accrue interest first to ensure that the accrued interest is reasonable (next require). + // Safe because of the AccrueInterest.repayAccruesInterest rule + summaryAccrueInterest(e, marketParams, id); + + // Assume that the invariant about tokens total supply is respected. + require totalBorrowAssets(id) < 10^35; + + repay@withrevert(e, marketParams, 0, shares, e.msg.sender, data); + + assert !lastReverted; +} + +// Check the one can always withdraw all, under the condition that there are no outstanding debt on the market. +rule canWithdrawAll(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, address receiver) { + MorphoInternalAccess.Id id = libId(marketParams); + + // Assume a full withdraw. + require shares == supplyShares(id, e.msg.sender); + // Omit sanity checks. + require isCreated(id); + require e.msg.sender != 0; + require receiver != 0; + require e.msg.value == 0; + require shares > 0; + // Assume no outstanding debt on the market. + require totalBorrowAssets(id) == 0; + // Safe require because of the noTimeTravel rule. + require lastUpdate(id) <= e.block.timestamp; + // Safe require because of the sumSupplySharesCorrect invariant. + require shares <= totalSupplyShares(id); + + withdraw@withrevert(e, marketParams, 0, shares, e.msg.sender, receiver); + + assert !lastReverted; +} + +// Check that a user can always withdraw all, under the condition that this user does not have an outstanding debt. +// Combined with the canRepayAll rule, this ensures that a borrower can always fully exit a market. +rule canWithdrawCollateralAll(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, address receiver) { + MorphoInternalAccess.Id id = libId(marketParams); + + // Ensure a full withdrawCollateral. + require assets == collateral(id, e.msg.sender); + // Omit sanity checks. + require isCreated(id); + require receiver != 0; + require e.msg.value == 0; + require assets > 0; + // Safe require because of the noTimeTravel rule. + require lastUpdate(id) <= e.block.timestamp; + // Assume that the user does not have an outstanding debt. + require borrowShares(id, e.msg.sender) == 0; + + withdrawCollateral@withrevert(e, marketParams, assets, e.msg.sender, receiver); + + assert !lastReverted; +} diff --git a/certora/specs/RatioMath.spec b/certora/specs/RatioMath.spec new file mode 100644 index 000000000..1fabb7742 --- /dev/null +++ b/certora/specs/RatioMath.spec @@ -0,0 +1,184 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +methods { + function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; + + function collateral(MorphoHarness.Id, address) external returns uint256 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; + function virtualTotalBorrowShares(MorphoHarness.Id) external returns uint256 envfree; + 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; + +} + +invariant feeInRange(MorphoHarness.Id id) + fee(id) <= maxFee(); + +// This is a simple overapproximative summary, stating that it rounds in the right direction. +function summaryMulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 { + uint256 result; + // Safe require that is checked by the specification in LibSummary.spec. + require result * d >= x * y; + return result; +} + +// This is a simple overapproximative summary, stating that it rounds in the right direction. +function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 { + uint256 result; + // Safe require that is checked by the specification in LibSummary.spec. + require result * d <= x * y; + return result; +} + +// Check that accrueInterest increases the value of supply shares. +rule accrueInterestIncreasesSupplyRatio(env e, MorphoHarness.MarketParams marketParams) { + MorphoHarness.Id id; + requireInvariant feeInRange(id); + + mathint assetsBefore = virtualTotalSupplyAssets(id); + mathint sharesBefore = virtualTotalSupplyShares(id); + + // The check is done for every market, not just for id. + accrueInterest(e, marketParams); + + mathint assetsAfter = virtualTotalSupplyAssets(id); + mathint sharesAfter = virtualTotalSupplyShares(id); + + // Check that the ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter. + assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore; +} + +// Check that accrueInterest increases the value of borrow shares. +rule accrueInterestIncreasesBorrowRatio(env e, MorphoHarness.MarketParams marketParams) { + MorphoHarness.Id id; + requireInvariant feeInRange(id); + + mathint assetsBefore = virtualTotalBorrowAssets(id); + mathint sharesBefore = virtualTotalBorrowShares(id); + + // The check is done for every marketParams, not just for id. + accrueInterest(e, marketParams); + + mathint assetsAfter = virtualTotalBorrowAssets(id); + mathint sharesAfter = virtualTotalBorrowShares(id); + + // Check that the ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter. + assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore; +} + + +// Check that except when not accruing interest and except for liquidate, every function increases the value of supply shares. +rule onlyLiquidateCanDecreaseSupplyRatio(env e, method f, calldataarg args) +filtered { + f -> !f.isView && f.selector != sig:liquidate(MorphoHarness.MarketParams, address, uint256, uint256, bytes).selector +} +{ + MorphoHarness.Id id; + requireInvariant feeInRange(id); + + mathint assetsBefore = virtualTotalSupplyAssets(id); + mathint sharesBefore = virtualTotalSupplyShares(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; + + f(e,args); + + mathint assetsAfter = virtualTotalSupplyAssets(id); + mathint sharesAfter = virtualTotalSupplyShares(id); + + // Check that the ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter + assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore; +} + +// Check that when not realizing bad debt in liquidate, the value of supply shares increases. +rule liquidateWithoutBadDebtRealizationIncreasesSupplyRatio(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, uint256 repaidShares, bytes data) +{ + MorphoHarness.Id id; + requireInvariant feeInRange(id); + + mathint assetsBefore = virtualTotalSupplyAssets(id); + mathint sharesBefore = virtualTotalSupplyShares(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; + + liquidate(e, marketParams, borrower, seizedAssets, repaidShares, data); + + mathint assetsAfter = virtualTotalSupplyAssets(id); + mathint sharesAfter = virtualTotalSupplyShares(id); + + // Trick to ensure that no bad debt realization happened. + require collateral(id, borrower) != 0; + + // Check that the ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter + assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore; +} + +// Check that except when not accruing interest, every function is decreasing the value of borrow shares. +// The repay function is checked separately, see below. +// The liquidate function is not checked. +rule onlyAccrueInterestCanIncreaseBorrowRatio(env e, method f, calldataarg args) +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); + + // Interest would increase borrow ratio, so we need to assume that no time passes. + require lastUpdate(id) == e.block.timestamp; + + mathint assetsBefore = virtualTotalBorrowAssets(id); + mathint sharesBefore = virtualTotalBorrowShares(id); + + f(e,args); + + mathint assetsAfter = virtualTotalBorrowAssets(id); + mathint sharesAfter = virtualTotalBorrowShares(id); + + // Check that the ratio decreases: assetsBefore/sharesBefore >= assetsAfter / sharesAfter + assert assetsBefore * sharesAfter >= assetsAfter * sharesBefore; +} + +// Check that when not accruing interest, repay is decreasing the value of borrow shares. +// Check the case where the market is not repaid fully. +// The other case requires exact math (ie not over-approximating mulDivUp and mulDivDown), so it is checked separately in ExactMath.spec. +rule repayDecreasesBorrowRatio(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) +{ + MorphoHarness.Id id = libId(marketParams); + requireInvariant feeInRange(id); + + mathint assetsBefore = virtualTotalBorrowAssets(id); + mathint sharesBefore = virtualTotalBorrowShares(id); + + // Interest would increase borrow ratio, so we need to assume that no time passes. + require lastUpdate(id) == e.block.timestamp; + + mathint repaidAssets; + repaidAssets, _ = repay(e, marketParams, assets, shares, onBehalf, data); + + // Check the case where the market is not repaid fully. + require repaidAssets < assetsBefore; + + mathint assetsAfter = virtualTotalBorrowAssets(id); + mathint sharesAfter = virtualTotalBorrowShares(id); + + assert assetsAfter == assetsBefore - repaidAssets; + // Check that the ratio decreases: assetsBefore/sharesBefore >= assetsAfter / sharesAfter + assert assetsBefore * sharesAfter >= assetsAfter * sharesBefore; +} diff --git a/certora/specs/Reentrancy.spec b/certora/specs/Reentrancy.spec new file mode 100644 index 000000000..1b95eae5f --- /dev/null +++ b/certora/specs/Reentrancy.spec @@ -0,0 +1,61 @@ +// 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; +} + +persistent ghost bool delegateCall; +persistent ghost bool callIsBorrowRate; +// True when storage has been accessed with either a SSTORE or a SLOAD. +persistent ghost bool hasAccessedStorage; +// True when a CALL has been done after storage has been accessed. +persistent ghost bool hasCallAfterAccessingStorage; +// True when storage has been accessed, after which an external call is made, followed by accessing storage again. +persistent ghost bool hasReentrancyUnsafeCall; + +function summaryBorrowRate() returns uint256 { + uint256 result; + callIsBorrowRate = true; + return result; +} + +hook ALL_SSTORE(uint loc, uint v) { + hasAccessedStorage = true; + hasReentrancyUnsafeCall = hasCallAfterAccessingStorage; +} + +hook ALL_SLOAD(uint loc) uint v { + hasAccessedStorage = true; + hasReentrancyUnsafeCall = hasCallAfterAccessingStorage; +} + +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. + callIsBorrowRate = false; + } else { + hasCallAfterAccessingStorage = hasAccessedStorage; + } +} + +hook DELEGATECALL(uint g, address addr, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc { + delegateCall = true; +} + +// Check that no function is accessing storage, then making an external CALL other than to the IRM, and accessing storage again. +rule reentrancySafe(method f, env e, calldataarg data) { + // Set up the initial state. + require !callIsBorrowRate; + require !hasAccessedStorage && !hasCallAfterAccessingStorage && !hasReentrancyUnsafeCall; + f(e,data); + assert !hasReentrancyUnsafeCall; +} + +// Check that the contract is truly immutable. +rule noDelegateCalls(method f, env e, calldataarg data) { + // Set up the initial state. + require !delegateCall; + f(e,data); + assert !delegateCall; +} diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec new file mode 100644 index 000000000..531db22f8 --- /dev/null +++ b/certora/specs/Reverts.spec @@ -0,0 +1,179 @@ +// 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 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; +} + +definition isCreated(MorphoHarness.Id id) returns bool = + (lastUpdate(id) != 0); + +persistent ghost mapping(MorphoHarness.Id => mathint) sumCollateral +{ + init_state axiom (forall MorphoHarness.Id id. sumCollateral[id] == 0); +} +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 = + totalSupplyAssets(id) == 0 && + totalSupplyShares(id) == 0 && + totalBorrowAssets(id) == 0 && + totalBorrowShares(id) == 0 && + sumCollateral[id] == 0; + +definition exactlyOneZero(uint256 assets, uint256 shares) returns bool = + (assets == 0 && shares != 0) || (assets != 0 && shares == 0); + +// This invariant catches bugs when not checking that the market is created with lastUpdate. +invariant notCreatedIsEmpty(MorphoHarness.Id id) + !isCreated(id) => emptyMarket(id) +{ + preserved with (env e) { + // Safe require because timestamps cannot realistically be that large. + require e.block.timestamp < 2^128; + } +} + +// Useful to ensure that authorized parties are not the zero address and so we can omit the sanity check in this case. +invariant zeroDoesNotAuthorize(address authorized) + !isAuthorized(0, authorized) +{ + preserved setAuthorization(address _authorized, bool _newAuthorization) with (env e) { + // Safe require because no one controls the zero address. + require e.msg.sender != 0; + } +} + +// Check the revert condition for the setOwner function. +rule setOwnerRevertCondition(env e, address newOwner) { + address oldOwner = owner(); + setOwner@withrevert(e, newOwner); + assert lastReverted <=> e.msg.value != 0 || e.msg.sender != oldOwner || newOwner == oldOwner; +} + +// Check the revert condition for the setOwner function. +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 || oldIsIrmEnabled; +} + +// Check the revert condition for the enableLltv function. +rule enableLltvRevertCondition(env e, uint256 lltv) { + address oldOwner = owner(); + bool oldIsLltvEnabled = isLltvEnabled(lltv); + enableLltv@withrevert(e, lltv); + assert lastReverted <=> e.msg.value != 0 || e.msg.sender != oldOwner || lltv >= wad() || oldIsLltvEnabled; +} + +// Check that setFee reverts when its inputs are not validated. +// setFee can also revert if the accrueInterest reverts. +rule setFeeInputValidation(env e, MorphoHarness.MarketParams marketParams, uint256 newFee) { + MorphoHarness.Id id = libId(marketParams); + address oldOwner = owner(); + bool wasCreated = isCreated(id); + setFee@withrevert(e, marketParams, newFee); + bool hasReverted = lastReverted; + assert e.msg.value != 0 || e.msg.sender != oldOwner || !wasCreated || newFee > maxFee() => hasReverted; +} + +// Check the revert condition for the setFeeRecipient function. +rule setFeeRecipientRevertCondition(env e, address newFeeRecipient) { + address oldOwner = owner(); + address oldFeeRecipient = feeRecipient(); + setFeeRecipient@withrevert(e, newFeeRecipient); + assert lastReverted <=> e.msg.value != 0 || e.msg.sender != oldOwner || newFeeRecipient == oldFeeRecipient; +} + +// Check that createMarket reverts when its input are not validated. +rule createMarketInputValidation(env e, MorphoHarness.MarketParams marketParams) { + MorphoHarness.Id id = libId(marketParams); + bool irmEnabled = isIrmEnabled(marketParams.irm); + bool lltvEnabled = isLltvEnabled(marketParams.lltv); + bool wasCreated = isCreated(id); + createMarket@withrevert(e, marketParams); + assert e.msg.value != 0 || !irmEnabled || !lltvEnabled || wasCreated => lastReverted; +} + +// Check that supply reverts when its input are not validated. +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; +} + +// Check that withdraw reverts when its inputs are not validated. +rule withdrawInputValidation(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) { + // Safe require because no one controls the zero address. + require e.msg.sender != 0; + requireInvariant zeroDoesNotAuthorize(e.msg.sender); + withdraw@withrevert(e, marketParams, assets, shares, onBehalf, receiver); + assert !exactlyOneZero(assets, shares) || onBehalf == 0 || receiver == 0 => lastReverted; +} + +// Check that borrow reverts when its inputs are not validated. +rule borrowInputValidation(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) { + // Safe require because no one controls the zero address. + require e.msg.sender != 0; + requireInvariant zeroDoesNotAuthorize(e.msg.sender); + borrow@withrevert(e, marketParams, assets, shares, onBehalf, receiver); + assert !exactlyOneZero(assets, shares) || onBehalf == 0 || receiver == 0 => lastReverted; +} + +// Check that repay reverts when its inputs are not validated. +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; +} + +// Check that supplyCollateral reverts when its inputs are not validated. +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; +} + +// Check that withdrawCollateral reverts when its inputs are not validated. +rule withdrawCollateralInputValidation(env e, MorphoHarness.MarketParams marketParams, uint256 assets, address onBehalf, address receiver) { + // Safe require because no one controls the zero address. + require e.msg.sender != 0; + requireInvariant zeroDoesNotAuthorize(e.msg.sender); + withdrawCollateral@withrevert(e, marketParams, assets, onBehalf, receiver); + assert assets == 0 || onBehalf == 0 || receiver == 0 => lastReverted; +} + +// 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) { + bool wasCreated = isCreated(libId(marketParams)); + accrueInterest@withrevert(e, marketParams); + assert !wasCreated => lastReverted; +} diff --git a/certora/specs/Transfer.spec b/certora/specs/Transfer.spec new file mode 100644 index 000000000..5de54a691 --- /dev/null +++ b/certora/specs/Transfer.spec @@ -0,0 +1,82 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +methods { + function libSafeTransfer(address, address, uint256) external envfree; + function libSafeTransferFrom(address, address, address, uint256) external envfree; + function balanceOf(address, address) external returns (uint256) envfree; + function allowance(address, address, address) external returns (uint256) envfree; + function totalSupply(address) external returns (uint256) envfree; + + function _.transfer(address, uint256) external => DISPATCHER(true); + function _.transferFrom(address, address, uint256) external => DISPATCHER(true); + function _.balanceOf(address) external => DISPATCHER(true); + function _.allowance(address, address) external => DISPATCHER(true); + function _.totalSupply() external => DISPATCHER(true); +} + +persistent ghost mapping(address => mathint) balance { + init_state axiom (forall address token. balance[token] == 0); +} + +function summarySafeTransferFrom(address token, address from, address to, uint256 amount) { + if (from == currentContract) { + // Safe require because the reference implementation would revert. + balance[token] = require_uint256(balance[token] - amount); + } + if (to == currentContract) { + // Safe require because the reference implementation would revert. + balance[token] = require_uint256(balance[token] + amount); + } +} + +// Check the functional correctness of the summary of safeTransfer. +rule checkTransferSummary(address token, address to, uint256 amount) { + mathint initialBalance = balanceOf(token, currentContract); + // Safe require because the total supply is greater than the sum of the balance of any two accounts. + require to != currentContract => initialBalance + balanceOf(token, to) <= to_mathint(totalSupply(token)); + + libSafeTransfer(token, to, amount); + mathint finalBalance = balanceOf(token, currentContract); + + require balance[token] == initialBalance; + summarySafeTransferFrom(token, currentContract, to, amount); + assert balance[token] == finalBalance; +} + +// Check the functional correctness of the summary of safeTransferFrom. +rule checkTransferFromSummary(address token, address from, uint256 amount) { + mathint initialBalance = balanceOf(token, currentContract); + // Safe require because the total supply is greater than the sum of the balance of any two accounts. + require from != currentContract => initialBalance + balanceOf(token, from) <= to_mathint(totalSupply(token)); + + libSafeTransferFrom(token, from, currentContract, amount); + mathint finalBalance = balanceOf(token, currentContract); + + require balance[token] == initialBalance; + summarySafeTransferFrom(token, from, currentContract, amount); + assert balance[token] == finalBalance; +} + +// Check the revert condition of the summary of safeTransfer. +rule transferRevertCondition(address token, address to, uint256 amount) { + uint256 initialBalance = balanceOf(token, currentContract); + uint256 toInitialBalance = balanceOf(token, to); + // Safe require because the total supply is greater than the sum of the balance of any two accounts. + require to != currentContract => initialBalance + toInitialBalance <= to_mathint(totalSupply(token)); + + libSafeTransfer@withrevert(token, to, amount); + + assert lastReverted <=> initialBalance < amount; +} + +// Check the revert condition of the summary of safeTransferFrom. +rule transferFromRevertCondition(address token, address from, address to, uint256 amount) { + uint256 initialBalance = balanceOf(token, from); + uint256 toInitialBalance = balanceOf(token, to); + uint256 allowance = allowance(token, from, currentContract); + // Safe require because the total supply is greater than the sum of the balance of any two accounts. + require to != from => initialBalance + toInitialBalance <= to_mathint(totalSupply(token)); + + libSafeTransferFrom@withrevert(token, from, to, amount); + + assert lastReverted <=> initialBalance < amount || allowance < amount; +} diff --git a/foundry.toml b/foundry.toml index b698a4eec..aecd8c162 100644 --- a/foundry.toml +++ b/foundry.toml @@ -2,7 +2,7 @@ names = true sizes = true via-ir = true -optimizer_runs = 4294967295 +optimizer_runs = 999999 # Etherscan does not support verifying contracts with more optimization runs. [profile.default.invariant] runs = 16 diff --git a/lib/forge-std b/lib/forge-std index e8a047e3f..2f1126975 160000 --- a/lib/forge-std +++ b/lib/forge-std @@ -1 +1 @@ -Subproject commit e8a047e3f40f13fa37af6fe14e6e06283d9a060e +Subproject commit 2f112697506eab12d433a65fdc31a639548fe365 diff --git a/package.json b/package.json index 9f9364482..1d942bfe8 100644 --- a/package.json +++ b/package.json @@ -2,7 +2,7 @@ "name": "@morpho-org/morpho-blue", "description": "Morpho Blue Protocol", "license": "BUSL-1.1", - "version": "0.1.0", + "version": "1.0.0", "files": [ "src", "README.md", diff --git a/src/Morpho.sol b/src/Morpho.sol index f755904b6..3b2811c44 100644 --- a/src/Morpho.sol +++ b/src/Morpho.sol @@ -158,6 +158,9 @@ contract Morpho is IMorphoStaticTyping { idToMarketParams[id] = marketParams; emit EventsLib.CreateMarket(id, marketParams); + + // Call to initialize the IRM in case it is stateful. + if (marketParams.irm != address(0)) IIrm(marketParams.irm).borrowRate(marketParams, market[id]); } /* SUPPLY MANAGEMENT */ @@ -354,12 +357,11 @@ contract Morpho is IMorphoStaticTyping { _accrueInterest(marketParams, id); - uint256 collateralPrice = IOracle(marketParams.oracle).price(); + { + uint256 collateralPrice = IOracle(marketParams.oracle).price(); - require(!_isHealthy(marketParams, id, borrower, collateralPrice), ErrorsLib.HEALTHY_POSITION); + require(!_isHealthy(marketParams, id, borrower, collateralPrice), ErrorsLib.HEALTHY_POSITION); - uint256 repaidAssets; - { // The liquidation incentive factor is min(maxLiquidationIncentiveFactor, 1/(1 - cursor*(1 - lltv))). uint256 liquidationIncentiveFactor = UtilsLib.min( MAX_LIQUIDATION_INCENTIVE_FACTOR, @@ -367,15 +369,17 @@ contract Morpho is IMorphoStaticTyping { ); if (seizedAssets > 0) { - repaidAssets = - seizedAssets.mulDivUp(collateralPrice, ORACLE_PRICE_SCALE).wDivUp(liquidationIncentiveFactor); - repaidShares = repaidAssets.toSharesDown(market[id].totalBorrowAssets, market[id].totalBorrowShares); + uint256 seizedAssetsQuoted = seizedAssets.mulDivUp(collateralPrice, ORACLE_PRICE_SCALE); + + repaidShares = seizedAssetsQuoted.wDivUp(liquidationIncentiveFactor).toSharesUp( + market[id].totalBorrowAssets, market[id].totalBorrowShares + ); } else { - repaidAssets = repaidShares.toAssetsUp(market[id].totalBorrowAssets, market[id].totalBorrowShares); - seizedAssets = - repaidAssets.wMulDown(liquidationIncentiveFactor).mulDivDown(ORACLE_PRICE_SCALE, collateralPrice); + seizedAssets = repaidShares.toAssetsDown(market[id].totalBorrowAssets, market[id].totalBorrowShares) + .wMulDown(liquidationIncentiveFactor).mulDivDown(ORACLE_PRICE_SCALE, collateralPrice); } } + uint256 repaidAssets = repaidShares.toAssetsUp(market[id].totalBorrowAssets, market[id].totalBorrowShares); position[id][borrower].borrowShares -= repaidShares.toUint128(); market[id].totalBorrowShares -= repaidShares.toUint128(); @@ -384,23 +388,26 @@ contract Morpho is IMorphoStaticTyping { position[id][borrower].collateral -= seizedAssets.toUint128(); uint256 badDebtShares; + uint256 badDebtAssets; if (position[id][borrower].collateral == 0) { badDebtShares = position[id][borrower].borrowShares; - uint256 badDebt = UtilsLib.min( + badDebtAssets = UtilsLib.min( market[id].totalBorrowAssets, badDebtShares.toAssetsUp(market[id].totalBorrowAssets, market[id].totalBorrowShares) ); - market[id].totalBorrowAssets -= badDebt.toUint128(); - market[id].totalSupplyAssets -= badDebt.toUint128(); + market[id].totalBorrowAssets -= badDebtAssets.toUint128(); + market[id].totalSupplyAssets -= badDebtAssets.toUint128(); market[id].totalBorrowShares -= badDebtShares.toUint128(); position[id][borrower].borrowShares = 0; } - IERC20(marketParams.collateralToken).safeTransfer(msg.sender, seizedAssets); - // `repaidAssets` may be greater than `totalBorrowAssets` by 1. - emit EventsLib.Liquidate(id, msg.sender, borrower, repaidAssets, repaidShares, seizedAssets, badDebtShares); + emit EventsLib.Liquidate( + id, msg.sender, borrower, repaidAssets, repaidShares, seizedAssets, badDebtAssets, badDebtShares + ); + + IERC20(marketParams.collateralToken).safeTransfer(msg.sender, seizedAssets); if (data.length > 0) IMorphoLiquidateCallback(msg.sender).onMorphoLiquidate(repaidAssets, data); @@ -413,10 +420,12 @@ contract Morpho is IMorphoStaticTyping { /// @inheritdoc IMorphoBase function flashLoan(address token, uint256 assets, bytes calldata data) external { - IERC20(token).safeTransfer(msg.sender, assets); + require(assets != 0, ErrorsLib.ZERO_ASSETS); emit EventsLib.FlashLoan(msg.sender, token, assets); + IERC20(token).safeTransfer(msg.sender, assets); + IMorphoFlashLoanCallback(msg.sender).onMorphoFlashLoan(assets, data); IERC20(token).safeTransferFrom(msg.sender, address(this), assets); @@ -426,6 +435,8 @@ contract Morpho is IMorphoStaticTyping { /// @inheritdoc IMorphoBase function setAuthorization(address authorized, bool newIsAuthorized) external { + require(newIsAuthorized != isAuthorized[msg.sender][authorized], ErrorsLib.ALREADY_SET); + isAuthorized[msg.sender][authorized] = newIsAuthorized; emit EventsLib.SetAuthorization(msg.sender, msg.sender, authorized, newIsAuthorized); @@ -433,11 +444,12 @@ contract Morpho is IMorphoStaticTyping { /// @inheritdoc IMorphoBase function setAuthorizationWithSig(Authorization memory authorization, Signature calldata signature) external { + /// Do not check whether authorization is already set because the nonce increment is a desired side effect. require(block.timestamp <= authorization.deadline, ErrorsLib.SIGNATURE_EXPIRED); require(authorization.nonce == nonce[authorization.authorizer]++, ErrorsLib.INVALID_NONCE); bytes32 hashStruct = keccak256(abi.encode(AUTHORIZATION_TYPEHASH, authorization)); - bytes32 digest = keccak256(abi.encodePacked("\x19\x01", DOMAIN_SEPARATOR, hashStruct)); + bytes32 digest = keccak256(bytes.concat("\x19\x01", DOMAIN_SEPARATOR, hashStruct)); address signatory = ecrecover(digest, signature.v, signature.r, signature.s); require(signatory != address(0) && authorization.authorizer == signatory, ErrorsLib.INVALID_SIGNATURE); @@ -470,25 +482,27 @@ contract Morpho is IMorphoStaticTyping { /// @dev Assumes that the inputs `marketParams` and `id` match. function _accrueInterest(MarketParams memory marketParams, Id id) internal { uint256 elapsed = block.timestamp - market[id].lastUpdate; - if (elapsed == 0) return; - uint256 borrowRate = IIrm(marketParams.irm).borrowRate(marketParams, market[id]); - uint256 interest = market[id].totalBorrowAssets.wMulDown(borrowRate.wTaylorCompounded(elapsed)); - market[id].totalBorrowAssets += interest.toUint128(); - market[id].totalSupplyAssets += interest.toUint128(); - - uint256 feeShares; - if (market[id].fee != 0) { - uint256 feeAmount = interest.wMulDown(market[id].fee); - // The fee amount is subtracted from the total supply in this calculation to compensate for the fact - // that total supply is already increased by the full interest (including the fee amount). - feeShares = feeAmount.toSharesDown(market[id].totalSupplyAssets - feeAmount, market[id].totalSupplyShares); - position[id][feeRecipient].supplyShares += feeShares; - market[id].totalSupplyShares += feeShares.toUint128(); - } + if (marketParams.irm != address(0)) { + uint256 borrowRate = IIrm(marketParams.irm).borrowRate(marketParams, market[id]); + uint256 interest = market[id].totalBorrowAssets.wMulDown(borrowRate.wTaylorCompounded(elapsed)); + market[id].totalBorrowAssets += interest.toUint128(); + market[id].totalSupplyAssets += interest.toUint128(); + + uint256 feeShares; + if (market[id].fee != 0) { + uint256 feeAmount = interest.wMulDown(market[id].fee); + // The fee amount is subtracted from the total supply in this calculation to compensate for the fact + // that total supply is already increased by the full interest (including the fee amount). + feeShares = + feeAmount.toSharesDown(market[id].totalSupplyAssets - feeAmount, market[id].totalSupplyShares); + position[id][feeRecipient].supplyShares += feeShares; + market[id].totalSupplyShares += feeShares.toUint128(); + } - emit EventsLib.AccrueInterest(id, borrowRate, interest, feeShares); + emit EventsLib.AccrueInterest(id, borrowRate, interest, feeShares); + } // Safe "unchecked" cast. market[id].lastUpdate = uint128(block.timestamp); diff --git a/src/interfaces/IIrm.sol b/src/interfaces/IIrm.sol index db2aaf873..3de0bc1e8 100644 --- a/src/interfaces/IIrm.sol +++ b/src/interfaces/IIrm.sol @@ -8,11 +8,12 @@ import {MarketParams, Market} from "./IMorpho.sol"; /// @custom:contact security@morpho.org /// @notice Interface that Interest Rate Models (IRMs) used by Morpho must implement. interface IIrm { - /// @notice Returns the borrow rate of the market `marketParams`. + /// @notice Returns the borrow rate per second (scaled by WAD) of the market `marketParams`. /// @dev Assumes that `market` corresponds to `marketParams`. function borrowRate(MarketParams memory marketParams, Market memory market) external returns (uint256); - /// @notice Returns the borrow rate of the market `marketParams` without modifying any storage. + /// @notice Returns the borrow rate per second (scaled by WAD) of the market `marketParams` without modifying any + /// storage. /// @dev Assumes that `market` corresponds to `marketParams`. function borrowRateView(MarketParams memory marketParams, Market memory market) external view returns (uint256); } diff --git a/src/interfaces/IMorpho.sol b/src/interfaces/IMorpho.sol index b928e50ad..9c82524cb 100644 --- a/src/interfaces/IMorpho.sol +++ b/src/interfaces/IMorpho.sol @@ -70,7 +70,7 @@ interface IMorphoBase { /// @notice Whether the `lltv` is enabled. function isLltvEnabled(uint256 lltv) external view returns (bool); - /// @notice Whether `authorized` is authorized to modify `authorizer`'s positions. + /// @notice Whether `authorized` is authorized to modify `authorizer`'s position on all markets. /// @dev Anyone is authorized to modify their own positions, regardless of this variable. function isAuthorized(address authorizer, address authorized) external view returns (bool); @@ -91,6 +91,7 @@ interface IMorphoBase { function enableLltv(uint256 lltv) external; /// @notice Sets the `newFee` for the given market `marketParams`. + /// @param newFee The new fee, scaled by WAD. /// @dev Warning: The recipient can be the zero address. function setFee(MarketParams memory marketParams, uint256 newFee) external; @@ -129,12 +130,12 @@ interface IMorphoBase { /// @notice Supplies `assets` or `shares` on behalf of `onBehalf`, optionally calling back the caller's /// `onMorphoSupply` function with the given `data`. - /// @dev Either `assets` or `shares` should be zero. Most usecases should rely on `assets` as an input so the caller - /// is guaranteed to have `assets` tokens pulled from their balance, but the possibility to mint a specific amount - /// of shares is given for full compatibility and precision. - /// @dev If the supply of a market gets depleted, the supply share price instantly resets to - /// `VIRTUAL_ASSETS`:`VIRTUAL_SHARES`. + /// @dev Either `assets` or `shares` should be zero. Most use cases should rely on `assets` as an input so the + /// caller is guaranteed to have `assets` tokens pulled from their balance, but the possibility to mint a specific + /// amount of shares is given for full compatibility and precision. /// @dev Supplying a large amount can revert for overflow. + /// @dev Supplying an amount of shares may lead to supply more or fewer assets than expected due to slippage. + /// Consider using the `assets` parameter to avoid this. /// @param marketParams The market to supply assets to. /// @param assets The amount of assets to supply. /// @param shares The amount of shares to mint. @@ -150,7 +151,7 @@ interface IMorphoBase { bytes memory data ) external returns (uint256 assetsSupplied, uint256 sharesSupplied); - /// @notice Withdraws `assets` or `shares` on behalf of `onBehalf` to `receiver`. + /// @notice Withdraws `assets` or `shares` on behalf of `onBehalf` and sends the assets to `receiver`. /// @dev Either `assets` or `shares` should be zero. To withdraw max, pass the `shares`'s balance of `onBehalf`. /// @dev `msg.sender` must be authorized to manage `onBehalf`'s positions. /// @dev Withdrawing an amount corresponding to more shares than supplied will revert for underflow. @@ -171,14 +172,14 @@ interface IMorphoBase { address receiver ) external returns (uint256 assetsWithdrawn, uint256 sharesWithdrawn); - /// @notice Borrows `assets` or `shares` on behalf of `onBehalf` to `receiver`. - /// @dev Either `assets` or `shares` should be zero. Most usecases should rely on `assets` as an input so the caller - /// is guaranteed to borrow `assets` of tokens, but the possibility to mint a specific amount of shares is given for - /// full compatibility and precision. - /// @dev If the borrow of a market gets depleted, the borrow share price instantly resets to - /// `VIRTUAL_ASSETS`:`VIRTUAL_SHARES`. + /// @notice Borrows `assets` or `shares` on behalf of `onBehalf` and sends the assets to `receiver`. + /// @dev Either `assets` or `shares` should be zero. Most use cases should rely on `assets` as an input so the + /// caller is guaranteed to borrow `assets` of tokens, but the possibility to mint a specific amount of shares is + /// given for full compatibility and precision. /// @dev `msg.sender` must be authorized to manage `onBehalf`'s positions. /// @dev Borrowing a large amount can revert for overflow. + /// @dev Borrowing an amount of shares may lead to borrow fewer assets than expected due to slippage. + /// Consider using the `assets` parameter to avoid this. /// @param marketParams The market to borrow assets from. /// @param assets The amount of assets to borrow. /// @param shares The amount of shares to mint. @@ -200,6 +201,7 @@ interface IMorphoBase { /// @dev Repaying an amount corresponding to more shares than borrowed will revert for underflow. /// @dev It is advised to use the `shares` input when repaying the full position to avoid reverts due to conversion /// roundings between shares and assets. + /// @dev An attacker can front-run a repay with a small repay making the transaction revert for underflow. /// @param marketParams The market to repay assets to. /// @param assets The amount of assets to repay. /// @param shares The amount of shares to burn. @@ -226,7 +228,7 @@ interface IMorphoBase { function supplyCollateral(MarketParams memory marketParams, uint256 assets, address onBehalf, bytes memory data) external; - /// @notice Withdraws `assets` of collateral on behalf of `onBehalf` to `receiver`. + /// @notice Withdraws `assets` of collateral on behalf of `onBehalf` and sends the assets to `receiver`. /// @dev `msg.sender` must be authorized to manage `onBehalf`'s positions. /// @dev Withdrawing an amount corresponding to more collateral than supplied will revert for underflow. /// @param marketParams The market to withdraw collateral from. @@ -242,6 +244,7 @@ interface IMorphoBase { /// @dev Either `seizedAssets` or `repaidShares` should be zero. /// @dev Seizing more than the collateral balance will underflow and revert without any error message. /// @dev Repaying more than the borrow balance will underflow and revert without any error message. + /// @dev An attacker can front-run a liquidation with a small repay making the transaction revert for underflow. /// @param marketParams The market of the position. /// @param borrower The owner of the position. /// @param seizedAssets The amount of collateral to seize. diff --git a/src/libraries/ErrorsLib.sol b/src/libraries/ErrorsLib.sol index 893a6b32d..02cc94423 100644 --- a/src/libraries/ErrorsLib.sol +++ b/src/libraries/ErrorsLib.sol @@ -27,6 +27,9 @@ library ErrorsLib { /// @notice Thrown when the market is already created. string internal constant MARKET_ALREADY_CREATED = "market already created"; + /// @notice Thrown when a token to transfer doesn't have code. + string internal constant NO_CODE = "no code"; + /// @notice Thrown when the market is not created. string internal constant MARKET_NOT_CREATED = "market not created"; diff --git a/src/libraries/EventsLib.sol b/src/libraries/EventsLib.sol index 825ea1791..2ff9b829d 100644 --- a/src/libraries/EventsLib.sol +++ b/src/libraries/EventsLib.sol @@ -35,9 +35,10 @@ library EventsLib { event CreateMarket(Id indexed id, MarketParams marketParams); /// @notice Emitted on supply of assets. + /// @dev Warning: `feeRecipient` receives some shares during interest accrual without any supply event emitted. /// @param id The market id. /// @param caller The caller. - /// @param onBehalf The address that received the supply. + /// @param onBehalf The owner of the modified position. /// @param assets The amount of assets supplied. /// @param shares The amount of shares minted. event Supply(Id indexed id, address indexed caller, address indexed onBehalf, uint256 assets, uint256 shares); @@ -45,7 +46,7 @@ library EventsLib { /// @notice Emitted on withdrawal of assets. /// @param id The market id. /// @param caller The caller. - /// @param onBehalf The address from which the assets were withdrawn. + /// @param onBehalf The owner of the modified position. /// @param receiver The address that received the withdrawn assets. /// @param assets The amount of assets withdrawn. /// @param shares The amount of shares burned. @@ -61,7 +62,7 @@ library EventsLib { /// @notice Emitted on borrow of assets. /// @param id The market id. /// @param caller The caller. - /// @param onBehalf The address from which the assets were borrowed. + /// @param onBehalf The owner of the modified position. /// @param receiver The address that received the borrowed assets. /// @param assets The amount of assets borrowed. /// @param shares The amount of shares minted. @@ -77,7 +78,7 @@ library EventsLib { /// @notice Emitted on repayment of assets. /// @param id The market id. /// @param caller The caller. - /// @param onBehalf The address for which the assets were repaid. + /// @param onBehalf The owner of the modified position. /// @param assets The amount of assets repaid. May be 1 over the corresponding market's `totalBorrowAssets`. /// @param shares The amount of shares burned. event Repay(Id indexed id, address indexed caller, address indexed onBehalf, uint256 assets, uint256 shares); @@ -85,14 +86,14 @@ library EventsLib { /// @notice Emitted on supply of collateral. /// @param id The market id. /// @param caller The caller. - /// @param onBehalf The address that received the collateral. + /// @param onBehalf The owner of the modified position. /// @param assets The amount of collateral supplied. event SupplyCollateral(Id indexed id, address indexed caller, address indexed onBehalf, uint256 assets); /// @notice Emitted on withdrawal of collateral. /// @param id The market id. /// @param caller The caller. - /// @param onBehalf The address from which the collateral was withdrawn. + /// @param onBehalf The owner of the modified position. /// @param receiver The address that received the withdrawn collateral. /// @param assets The amount of collateral withdrawn. event WithdrawCollateral( @@ -106,7 +107,8 @@ library EventsLib { /// @param repaidAssets The amount of assets repaid. May be 1 over the corresponding market's `totalBorrowAssets`. /// @param repaidShares The amount of shares burned. /// @param seizedAssets The amount of collateral seized. - /// @param badDebtShares The amount of shares minted as bad debt. + /// @param badDebtAssets The amount of assets of bad debt realized. + /// @param badDebtShares The amount of borrow shares of bad debt realized. event Liquidate( Id indexed id, address indexed caller, @@ -114,6 +116,7 @@ library EventsLib { uint256 repaidAssets, uint256 repaidShares, uint256 seizedAssets, + uint256 badDebtAssets, uint256 badDebtShares ); diff --git a/src/libraries/SafeTransferLib.sol b/src/libraries/SafeTransferLib.sol index d31a79121..02c3c0a38 100644 --- a/src/libraries/SafeTransferLib.sol +++ b/src/libraries/SafeTransferLib.sol @@ -15,18 +15,19 @@ interface IERC20Internal { /// @custom:contact security@morpho.org /// @notice Library to manage transfers of tokens, even if calls to the transfer or transferFrom functions are not /// returning a boolean. -/// @dev It is the responsibility of the market creator to make sure that the address of the token has non-zero code. library SafeTransferLib { - /// @dev Warning: It does not revert on `token` with no code. function safeTransfer(IERC20 token, address to, uint256 value) internal { + require(address(token).code.length > 0, ErrorsLib.NO_CODE); + (bool success, bytes memory returndata) = address(token).call(abi.encodeCall(IERC20Internal.transfer, (to, value))); require(success, ErrorsLib.TRANSFER_REVERTED); require(returndata.length == 0 || abi.decode(returndata, (bool)), ErrorsLib.TRANSFER_RETURNED_FALSE); } - /// @dev Warning: It does not revert on `token` with no code. function safeTransferFrom(IERC20 token, address from, address to, uint256 value) internal { + require(address(token).code.length > 0, ErrorsLib.NO_CODE); + (bool success, bytes memory returndata) = address(token).call(abi.encodeCall(IERC20Internal.transferFrom, (from, to, value))); require(success, ErrorsLib.TRANSFER_FROM_REVERTED); diff --git a/src/libraries/SharesMathLib.sol b/src/libraries/SharesMathLib.sol index 514760698..3ed7115b5 100644 --- a/src/libraries/SharesMathLib.sol +++ b/src/libraries/SharesMathLib.sol @@ -14,6 +14,9 @@ library SharesMathLib { /// @dev The number of virtual shares has been chosen low enough to prevent overflows, and high enough to ensure /// high precision computations. + /// @dev Virtual shares can never be redeemed for the assets they are entitled to, but it is assumed the share price + /// stays low enough not to inflate these assets to a significant value. + /// @dev Warning: The assets to which virtual borrow shares are entitled behave like unrealizable bad debt. uint256 internal constant VIRTUAL_SHARES = 1e6; /// @dev A number of virtual assets of 1 enforces a conversion rate between shares and assets when a market is diff --git a/src/libraries/UtilsLib.sol b/src/libraries/UtilsLib.sol index 066043d13..f343ef769 100644 --- a/src/libraries/UtilsLib.sol +++ b/src/libraries/UtilsLib.sol @@ -29,7 +29,7 @@ library UtilsLib { return uint128(x); } - /// @dev Returns max(x - y, 0). + /// @dev Returns max(0, x - y). function zeroFloorSub(uint256 x, uint256 y) internal pure returns (uint256 z) { assembly { z := mul(gt(x, y), sub(x, y)) diff --git a/src/libraries/periphery/MorphoBalancesLib.sol b/src/libraries/periphery/MorphoBalancesLib.sol index 3afabfd5f..94b3b85f9 100644 --- a/src/libraries/periphery/MorphoBalancesLib.sol +++ b/src/libraries/periphery/MorphoBalancesLib.sol @@ -36,13 +36,12 @@ library MorphoBalancesLib { returns (uint256, uint256, uint256, uint256) { Id id = marketParams.id(); - Market memory market = morpho.market(id); uint256 elapsed = block.timestamp - market.lastUpdate; - // Skipped if elapsed == 0 of if totalBorrowAssets == 0 because interest would be null. - if (elapsed != 0 && market.totalBorrowAssets != 0) { + // Skipped if elapsed == 0 or totalBorrowAssets == 0 because interest would be null, or if irm == address(0). + if (elapsed != 0 && market.totalBorrowAssets != 0 && marketParams.irm != address(0)) { uint256 borrowRate = IIrm(marketParams.irm).borrowRateView(marketParams, market); uint256 interest = market.totalBorrowAssets.wMulDown(borrowRate.wTaylorCompounded(elapsed)); market.totalBorrowAssets += interest.toUint128(); @@ -90,8 +89,8 @@ library MorphoBalancesLib { /// @notice Returns the expected supply assets balance of `user` on a market after having accrued interest. /// @dev Warning: Wrong for `feeRecipient` because their supply shares increase is not taken into account. - /// @dev Warning: Withdrawing a supply position using the expected assets balance can lead to a revert due to - /// conversion roundings between shares and assets. + /// @dev Warning: Withdrawing using the expected supply assets can lead to a revert due to conversion roundings from + /// assets to shares. function expectedSupplyAssets(IMorpho morpho, MarketParams memory marketParams, address user) internal view @@ -105,8 +104,8 @@ library MorphoBalancesLib { } /// @notice Returns the expected borrow assets balance of `user` on a market after having accrued interest. - /// @dev Warning: repaying a borrow position using the expected assets balance can lead to a revert due to - /// conversion roundings between shares and assets. + /// @dev Warning: The expected balance is rounded up, so it may be greater than the market's expected total borrow + /// assets. function expectedBorrowAssets(IMorpho morpho, MarketParams memory marketParams, address user) internal view diff --git a/test/forge/BaseTest.sol b/test/forge/BaseTest.sol index 9ea65f507..eafb6465d 100644 --- a/test/forge/BaseTest.sol +++ b/test/forge/BaseTest.sol @@ -82,7 +82,9 @@ contract BaseTest is Test { irm = new IrmMock(); vm.startPrank(OWNER); + morpho.enableIrm(address(0)); morpho.enableIrm(address(irm)); + morpho.enableLltv(0); morpho.setFeeRecipient(FEE_RECIPIENT); vm.stopPrank(); @@ -93,19 +95,19 @@ contract BaseTest is Test { loanToken.approve(address(morpho), type(uint256).max); collateralToken.approve(address(morpho), type(uint256).max); - changePrank(BORROWER); + vm.startPrank(BORROWER); loanToken.approve(address(morpho), type(uint256).max); collateralToken.approve(address(morpho), type(uint256).max); - changePrank(REPAYER); + vm.startPrank(REPAYER); loanToken.approve(address(morpho), type(uint256).max); collateralToken.approve(address(morpho), type(uint256).max); - changePrank(LIQUIDATOR); + vm.startPrank(LIQUIDATOR); loanToken.approve(address(morpho), type(uint256).max); collateralToken.approve(address(morpho), type(uint256).max); - changePrank(ONBEHALF); + vm.startPrank(ONBEHALF); loanToken.approve(address(morpho), type(uint256).max); collateralToken.approve(address(morpho), type(uint256).max); morpho.setAuthorization(BORROWER, true); @@ -133,7 +135,7 @@ contract BaseTest is Test { } /// @dev Bounds the fuzzing input to a realistic number of blocks. - function _boundBlocks(uint256 blocks) internal view returns (uint256) { + function _boundBlocks(uint256 blocks) internal pure returns (uint256) { return bound(blocks, 1, type(uint32).max); } @@ -198,7 +200,7 @@ contract BaseTest is Test { return (amountCollateral, amountBorrowed, priceCollateral); } - function _boundTestLltv(uint256 lltv) internal view returns (uint256) { + function _boundTestLltv(uint256 lltv) internal pure returns (uint256) { return bound(lltv, MIN_TEST_LLTV, MAX_TEST_LLTV); } @@ -390,7 +392,7 @@ contract BaseTest is Test { return Math.min(MAX_LIQUIDATION_INCENTIVE_FACTOR, WAD.wDivDown(WAD - LIQUIDATION_CURSOR.wMulDown(WAD - lltv))); } - function _boundValidLltv(uint256 lltv) internal view returns (uint256) { + function _boundValidLltv(uint256 lltv) internal pure returns (uint256) { return bound(lltv, 0, WAD - 1); } diff --git a/test/forge/helpers/SigUtils.sol b/test/forge/helpers/SigUtils.sol index 9a60b52f0..b8e90ea51 100644 --- a/test/forge/helpers/SigUtils.sol +++ b/test/forge/helpers/SigUtils.sol @@ -12,7 +12,7 @@ library SigUtils { pure returns (bytes32) { - return keccak256(abi.encodePacked("\x19\x01", domainSeparator, hashStruct(authorization))); + return keccak256(bytes.concat("\x19\x01", domainSeparator, hashStruct(authorization))); } function hashStruct(Authorization memory authorization) internal pure returns (bytes32) { diff --git a/test/forge/integration/AccrueInterestIntegrationTest.sol b/test/forge/integration/AccrueInterestIntegrationTest.sol index 3b91564f7..c935f8f58 100644 --- a/test/forge/integration/AccrueInterestIntegrationTest.sol +++ b/test/forge/integration/AccrueInterestIntegrationTest.sol @@ -15,6 +15,18 @@ contract AccrueInterestIntegrationTest is BaseTest { morpho.accrueInterest(marketParamsFuzz); } + function testAccrueInterestIrmZero(MarketParams memory marketParamsFuzz, uint256 blocks) public { + marketParamsFuzz.irm = address(0); + marketParamsFuzz.lltv = 0; + blocks = _boundBlocks(blocks); + + morpho.createMarket(marketParamsFuzz); + + _forward(blocks); + + morpho.accrueInterest(marketParamsFuzz); + } + function testAccrueInterestNoTimeElapsed(uint256 amountSupplied, uint256 amountBorrowed) public { uint256 collateralPrice = oracle.price(); uint256 amountCollateral; diff --git a/test/forge/integration/AuthorizationIntegrationTest.sol b/test/forge/integration/AuthorizationIntegrationTest.sol index 263eaa550..dd9e2440d 100644 --- a/test/forge/integration/AuthorizationIntegrationTest.sol +++ b/test/forge/integration/AuthorizationIntegrationTest.sol @@ -16,11 +16,22 @@ contract AuthorizationIntegrationTest is BaseTest { assertFalse(morpho.isAuthorized(address(this), addressFuzz)); } + function testAlreadySet(address addressFuzz) public { + vm.expectRevert(bytes(ErrorsLib.ALREADY_SET)); + morpho.setAuthorization(addressFuzz, false); + + morpho.setAuthorization(addressFuzz, true); + + vm.expectRevert(bytes(ErrorsLib.ALREADY_SET)); + morpho.setAuthorization(addressFuzz, true); + } + function testSetAuthorizationWithSignatureDeadlineOutdated( Authorization memory authorization, uint256 privateKey, uint256 blocks ) public { + authorization.isAuthorized = true; blocks = _boundBlocks(blocks); authorization.deadline = block.timestamp - 1; @@ -40,6 +51,7 @@ contract AuthorizationIntegrationTest is BaseTest { } function testAuthorizationWithSigWrongPK(Authorization memory authorization, uint256 privateKey) public { + authorization.isAuthorized = true; authorization.deadline = bound(authorization.deadline, block.timestamp, type(uint256).max); // Private key must be less than the secp256k1 curve order. @@ -55,6 +67,7 @@ contract AuthorizationIntegrationTest is BaseTest { } function testAuthorizationWithSigWrongNonce(Authorization memory authorization, uint256 privateKey) public { + authorization.isAuthorized = true; authorization.deadline = bound(authorization.deadline, block.timestamp, type(uint256).max); authorization.nonce = bound(authorization.nonce, 1, type(uint256).max); @@ -71,6 +84,7 @@ contract AuthorizationIntegrationTest is BaseTest { } function testAuthorizationWithSig(Authorization memory authorization, uint256 privateKey) public { + authorization.isAuthorized = true; authorization.deadline = bound(authorization.deadline, block.timestamp, type(uint256).max); // Private key must be less than the secp256k1 curve order. @@ -84,11 +98,12 @@ contract AuthorizationIntegrationTest is BaseTest { morpho.setAuthorizationWithSig(authorization, sig); - assertEq(morpho.isAuthorized(authorization.authorizer, authorization.authorized), authorization.isAuthorized); + assertEq(morpho.isAuthorized(authorization.authorizer, authorization.authorized), true); assertEq(morpho.nonce(authorization.authorizer), 1); } function testAuthorizationFailsWithReusedSig(Authorization memory authorization, uint256 privateKey) public { + authorization.isAuthorized = true; authorization.deadline = bound(authorization.deadline, block.timestamp, type(uint256).max); // Private key must be less than the secp256k1 curve order. @@ -102,6 +117,7 @@ contract AuthorizationIntegrationTest is BaseTest { morpho.setAuthorizationWithSig(authorization, sig); + authorization.isAuthorized = false; vm.expectRevert(bytes(ErrorsLib.INVALID_NONCE)); morpho.setAuthorizationWithSig(authorization, sig); } diff --git a/test/forge/integration/BorrowIntegrationTest.sol b/test/forge/integration/BorrowIntegrationTest.sol index 1733c7872..7b44ef931 100644 --- a/test/forge/integration/BorrowIntegrationTest.sol +++ b/test/forge/integration/BorrowIntegrationTest.sol @@ -55,7 +55,7 @@ contract BorrowIntegrationTest is BaseTest { collateralToken.approve(address(morpho), amountCollateral); morpho.supplyCollateral(marketParams, amountCollateral, supplier, hex""); - changePrank(attacker); + vm.startPrank(attacker); vm.expectRevert(bytes(ErrorsLib.UNAUTHORIZED)); morpho.borrow(marketParams, amountBorrowed, 0, supplier, RECEIVER); } @@ -202,7 +202,7 @@ contract BorrowIntegrationTest is BaseTest { vm.startPrank(ONBEHALF); collateralToken.approve(address(morpho), amountCollateral); morpho.supplyCollateral(marketParams, amountCollateral, ONBEHALF, hex""); - morpho.setAuthorization(BORROWER, true); + // BORROWER is already authorized. vm.stopPrank(); uint256 expectedBorrowShares = amountBorrowed.toSharesUp(0, 0); @@ -248,7 +248,7 @@ contract BorrowIntegrationTest is BaseTest { vm.startPrank(ONBEHALF); collateralToken.approve(address(morpho), amountCollateral); morpho.supplyCollateral(marketParams, amountCollateral, ONBEHALF, hex""); - morpho.setAuthorization(BORROWER, true); + // BORROWER is already authorized. vm.stopPrank(); vm.prank(BORROWER); diff --git a/test/forge/integration/CallbacksIntegrationTest.sol b/test/forge/integration/CallbacksIntegrationTest.sol index 62578aa19..512522e5e 100644 --- a/test/forge/integration/CallbacksIntegrationTest.sol +++ b/test/forge/integration/CallbacksIntegrationTest.sol @@ -83,6 +83,11 @@ contract CallbacksIntegrationTest is assertEq(loanToken.balanceOf(address(morpho)), amount, "balanceOf"); } + function testFlashLoanZero() public { + vm.expectRevert(bytes(ErrorsLib.ZERO_ASSETS)); + morpho.flashLoan(address(loanToken), 0, abi.encode(this.testFlashLoan.selector, hex"")); + } + function testFlashLoanShouldRevertIfNotReimbursed(uint256 amount) public { amount = bound(amount, 1, MAX_TEST_AMOUNT); diff --git a/test/forge/integration/CreateMarketIntegrationTest.sol b/test/forge/integration/CreateMarketIntegrationTest.sol index 1fd2eb083..db675543f 100644 --- a/test/forge/integration/CreateMarketIntegrationTest.sol +++ b/test/forge/integration/CreateMarketIntegrationTest.sol @@ -9,48 +9,46 @@ contract CreateMarketIntegrationTest is BaseTest { using MarketParamsLib for MarketParams; function testCreateMarketWithNotEnabledIrmAndNotEnabledLltv(MarketParams memory marketParamsFuzz) public { - vm.assume(marketParamsFuzz.irm != address(irm) && marketParamsFuzz.lltv != marketParams.lltv); + vm.assume(!morpho.isIrmEnabled(marketParamsFuzz.irm) && !morpho.isLltvEnabled(marketParamsFuzz.lltv)); - vm.prank(OWNER); vm.expectRevert(bytes(ErrorsLib.IRM_NOT_ENABLED)); + vm.prank(OWNER); morpho.createMarket(marketParamsFuzz); } function testCreateMarketWithNotEnabledIrmAndEnabledLltv(MarketParams memory marketParamsFuzz) public { - vm.assume(marketParamsFuzz.irm != address(irm)); - marketParamsFuzz.lltv = _boundValidLltv(marketParamsFuzz.lltv); - - vm.startPrank(OWNER); - if (marketParamsFuzz.lltv != marketParams.lltv) morpho.enableLltv(marketParamsFuzz.lltv); + vm.assume(!morpho.isIrmEnabled(marketParamsFuzz.irm)); vm.expectRevert(bytes(ErrorsLib.IRM_NOT_ENABLED)); + vm.prank(OWNER); morpho.createMarket(marketParamsFuzz); - vm.stopPrank(); } function testCreateMarketWithEnabledIrmAndNotEnabledLltv(MarketParams memory marketParamsFuzz) public { - vm.assume(marketParamsFuzz.lltv != marketParams.lltv); + vm.assume(!morpho.isLltvEnabled(marketParamsFuzz.lltv)); vm.startPrank(OWNER); - if (marketParamsFuzz.irm != marketParams.irm) morpho.enableIrm(marketParamsFuzz.irm); + if (!morpho.isIrmEnabled(marketParamsFuzz.irm)) morpho.enableIrm(marketParamsFuzz.irm); + vm.stopPrank(); vm.expectRevert(bytes(ErrorsLib.LLTV_NOT_ENABLED)); + vm.prank(OWNER); morpho.createMarket(marketParamsFuzz); - vm.stopPrank(); } function testCreateMarketWithEnabledIrmAndLltv(MarketParams memory marketParamsFuzz) public { + marketParamsFuzz.irm = address(irm); marketParamsFuzz.lltv = _boundValidLltv(marketParamsFuzz.lltv); Id marketParamsFuzzId = marketParamsFuzz.id(); vm.startPrank(OWNER); - if (marketParamsFuzz.irm != marketParams.irm) morpho.enableIrm(marketParamsFuzz.irm); - if (marketParamsFuzz.lltv != marketParams.lltv) morpho.enableLltv(marketParamsFuzz.lltv); + if (!morpho.isLltvEnabled(marketParamsFuzz.lltv)) morpho.enableLltv(marketParamsFuzz.lltv); + vm.stopPrank(); vm.expectEmit(true, true, true, true, address(morpho)); emit EventsLib.CreateMarket(marketParamsFuzz.id(), marketParamsFuzz); + vm.prank(OWNER); morpho.createMarket(marketParamsFuzz); - vm.stopPrank(); assertEq(morpho.lastUpdate(marketParamsFuzzId), block.timestamp, "lastUpdate != block.timestamp"); assertEq(morpho.totalSupplyAssets(marketParamsFuzzId), 0, "totalSupplyAssets != 0"); @@ -61,28 +59,32 @@ contract CreateMarketIntegrationTest is BaseTest { } function testCreateMarketAlreadyCreated(MarketParams memory marketParamsFuzz) public { + marketParamsFuzz.irm = address(irm); marketParamsFuzz.lltv = _boundValidLltv(marketParamsFuzz.lltv); vm.startPrank(OWNER); - if (marketParamsFuzz.irm != marketParams.irm) morpho.enableIrm(marketParamsFuzz.irm); - if (marketParamsFuzz.lltv != marketParams.lltv) morpho.enableLltv(marketParamsFuzz.lltv); + if (!morpho.isLltvEnabled(marketParamsFuzz.lltv)) morpho.enableLltv(marketParamsFuzz.lltv); + vm.stopPrank(); + + vm.prank(OWNER); morpho.createMarket(marketParamsFuzz); vm.expectRevert(bytes(ErrorsLib.MARKET_ALREADY_CREATED)); + vm.prank(OWNER); morpho.createMarket(marketParamsFuzz); - vm.stopPrank(); } function testIdToMarketParams(MarketParams memory marketParamsFuzz) public { + marketParamsFuzz.irm = address(irm); marketParamsFuzz.lltv = _boundValidLltv(marketParamsFuzz.lltv); Id marketParamsFuzzId = marketParamsFuzz.id(); vm.startPrank(OWNER); - if (marketParamsFuzz.irm != marketParams.irm) morpho.enableIrm(marketParamsFuzz.irm); - if (marketParamsFuzz.lltv != marketParams.lltv) morpho.enableLltv(marketParamsFuzz.lltv); + if (!morpho.isLltvEnabled(marketParamsFuzz.lltv)) morpho.enableLltv(marketParamsFuzz.lltv); + vm.stopPrank(); + vm.prank(OWNER); morpho.createMarket(marketParamsFuzz); - vm.stopPrank(); MarketParams memory params = morpho.idToMarketParams(marketParamsFuzzId); diff --git a/test/forge/integration/LiquidateIntegrationTest.sol b/test/forge/integration/LiquidateIntegrationTest.sol index f9227b635..874591d6a 100644 --- a/test/forge/integration/LiquidateIntegrationTest.sol +++ b/test/forge/integration/LiquidateIntegrationTest.sol @@ -74,6 +74,43 @@ contract LiquidateIntegrationTest is BaseTest { uint256 lltv; } + function testLiquidateMargin(LiquidateTestParams memory params, uint256 amountSeized, uint256 elapsed) public { + _setLltv(_boundTestLltv(params.lltv)); + (params.amountCollateral, params.amountBorrowed, params.priceCollateral) = + _boundHealthyPosition(params.amountCollateral, params.amountBorrowed, 1e36); + + elapsed = bound(elapsed, 0, 365 days); + + params.amountSupplied = + bound(params.amountSupplied, params.amountBorrowed, params.amountBorrowed + MAX_TEST_AMOUNT); + _supply(params.amountSupplied); + + amountSeized = bound(amountSeized, 1, params.amountCollateral); + + oracle.setPrice(params.priceCollateral); + + loanToken.setBalance(LIQUIDATOR, params.amountBorrowed); + collateralToken.setBalance(BORROWER, params.amountCollateral); + + vm.startPrank(BORROWER); + morpho.supplyCollateral(marketParams, params.amountCollateral, BORROWER, hex""); + morpho.borrow(marketParams, params.amountBorrowed, 0, BORROWER, BORROWER); + vm.stopPrank(); + + // We have to estimate the ratio after borrowing because the borrow rate depends on the utilization. + uint256 maxRatio = WAD + irm.borrowRate(marketParams, morpho.market(id)).wTaylorCompounded(elapsed); + // Sanity check: multiply maxBorrow by 2. + uint256 maxBorrow = _maxBorrow(marketParams, BORROWER).wDivDown(maxRatio); + // Should not omit too many tests because elapsed is reasonably bounded. + vm.assume(params.amountBorrowed < maxBorrow); + + vm.warp(block.timestamp + elapsed); + + vm.prank(LIQUIDATOR); + vm.expectRevert(bytes(ErrorsLib.HEALTHY_POSITION)); + morpho.liquidate(marketParams, BORROWER, amountSeized, 0, hex""); + } + function testLiquidateSeizedInputNoBadDebtRealized(LiquidateTestParams memory params, uint256 amountSeized) public { @@ -117,7 +154,7 @@ contract LiquidateIntegrationTest is BaseTest { vm.prank(LIQUIDATOR); vm.expectEmit(true, true, true, true, address(morpho)); - emit EventsLib.Liquidate(id, LIQUIDATOR, BORROWER, expectedRepaid, expectedRepaidShares, amountSeized, 0); + emit EventsLib.Liquidate(id, LIQUIDATOR, BORROWER, expectedRepaid, expectedRepaidShares, amountSeized, 0, 0); (uint256 returnSeized, uint256 returnRepaid) = morpho.liquidate(marketParams, BORROWER, amountSeized, 0, hex""); uint256 expectedCollateral = params.amountCollateral - amountSeized; @@ -169,15 +206,15 @@ contract LiquidateIntegrationTest is BaseTest { sharesRepaid = bound(sharesRepaid, 1, Math.min(borrowShares, maxSharesRepaid)); uint256 expectedRepaid = sharesRepaid.toAssetsUp(morpho.totalBorrowAssets(id), morpho.totalBorrowShares(id)); - uint256 expectedSeized = - expectedRepaid.wMulDown(liquidationIncentiveFactor).mulDivDown(ORACLE_PRICE_SCALE, params.priceCollateral); + uint256 expectedSeized = sharesRepaid.toAssetsDown(morpho.totalBorrowAssets(id), morpho.totalBorrowShares(id)) + .wMulDown(liquidationIncentiveFactor).mulDivDown(ORACLE_PRICE_SCALE, params.priceCollateral); loanToken.setBalance(LIQUIDATOR, params.amountBorrowed); vm.prank(LIQUIDATOR); vm.expectEmit(true, true, true, true, address(morpho)); - emit EventsLib.Liquidate(id, LIQUIDATOR, BORROWER, expectedRepaid, sharesRepaid, expectedSeized, 0); + emit EventsLib.Liquidate(id, LIQUIDATOR, BORROWER, expectedRepaid, sharesRepaid, expectedSeized, 0, 0); (uint256 returnSeized, uint256 returnRepaid) = morpho.liquidate(marketParams, BORROWER, 0, sharesRepaid, hex""); uint256 expectedCollateral = params.amountCollateral - expectedSeized; @@ -266,6 +303,7 @@ contract LiquidateIntegrationTest is BaseTest { params.expectedRepaid, params.expectedRepaidShares, amountCollateral, + params.expectedBadDebt, params.expectedBadDebt * SharesMathLib.VIRTUAL_SHARES ); (uint256 returnSeized, uint256 returnRepaid) = @@ -316,4 +354,28 @@ contract LiquidateIntegrationTest is BaseTest { vm.prank(LIQUIDATOR); morpho.liquidate(marketParams, BORROWER, collateralAmount, 0, hex""); } + + function testSeizedAssetsRoundUp() public { + _setLltv(0.75e18); + _supply(100e18); + + uint256 amountCollateral = 400; + uint256 amountBorrowed = 300; + collateralToken.setBalance(BORROWER, amountCollateral); + + vm.startPrank(BORROWER); + morpho.supplyCollateral(marketParams, amountCollateral, BORROWER, hex""); + morpho.borrow(marketParams, amountBorrowed, 0, BORROWER, BORROWER); + vm.stopPrank(); + + oracle.setPrice(ORACLE_PRICE_SCALE - 0.01e18); + + loanToken.setBalance(LIQUIDATOR, amountBorrowed); + + vm.prank(LIQUIDATOR); + (uint256 seizedAssets, uint256 repaidAssets) = morpho.liquidate(marketParams, BORROWER, 0, 1, hex""); + + assertEq(seizedAssets, 0, "seizedAssets"); + assertEq(repaidAssets, 1, "repaidAssets"); + } } diff --git a/test/forge/integration/OnlyOwnerIntegrationTest.sol b/test/forge/integration/OnlyOwnerIntegrationTest.sol index fb7f8c016..0b5ba9817 100644 --- a/test/forge/integration/OnlyOwnerIntegrationTest.sol +++ b/test/forge/integration/OnlyOwnerIntegrationTest.sol @@ -59,7 +59,7 @@ contract OnlyOwnerIntegrationTest is BaseTest { } function testEnableIrm(address irmFuzz) public { - vm.assume(irmFuzz != address(irm)); + vm.assume(!morpho.isIrmEnabled(irmFuzz)); vm.prank(OWNER); vm.expectEmit(true, true, true, true, address(morpho)); @@ -94,7 +94,8 @@ contract OnlyOwnerIntegrationTest is BaseTest { function testEnableLltv(uint256 lltvFuzz) public { lltvFuzz = _boundValidLltv(lltvFuzz); - vm.assume(lltvFuzz != marketParams.lltv); + + vm.assume(!morpho.isLltvEnabled(lltvFuzz)); vm.prank(OWNER); vm.expectEmit(true, true, true, true, address(morpho)); diff --git a/test/forge/integration/SupplyCollateralIntegrationTest.sol b/test/forge/integration/SupplyCollateralIntegrationTest.sol index 2994f97ab..2f54ae8b2 100644 --- a/test/forge/integration/SupplyCollateralIntegrationTest.sol +++ b/test/forge/integration/SupplyCollateralIntegrationTest.sol @@ -28,6 +28,18 @@ contract SupplyCollateralIntegrationTest is BaseTest { morpho.supplyCollateral(marketParams, amount, address(0), hex""); } + function testSupplyCollateralTokenNotCreated(uint256 amount, address token) public { + amount = bound(amount, 1, MAX_TEST_AMOUNT); + + vm.assume(token.code.length == 0); + + marketParams.collateralToken = token; + morpho.createMarket(marketParams); + + vm.expectRevert(bytes(ErrorsLib.NO_CODE)); + morpho.supplyCollateral(marketParams, amount, ONBEHALF, hex""); + } + function testSupplyCollateral(uint256 amount) public { amount = bound(amount, 1, MAX_COLLATERAL_ASSETS); diff --git a/test/forge/integration/SupplyIntegrationTest.sol b/test/forge/integration/SupplyIntegrationTest.sol index ceeca7eeb..21b6a6021 100644 --- a/test/forge/integration/SupplyIntegrationTest.sol +++ b/test/forge/integration/SupplyIntegrationTest.sol @@ -41,6 +41,18 @@ contract SupplyIntegrationTest is BaseTest { morpho.supply(marketParams, amount, shares, address(0), hex""); } + function testSupplyTokenNotCreated(uint256 amount, address token) public { + amount = bound(amount, 1, MAX_TEST_AMOUNT); + + vm.assume(token.code.length == 0); + + marketParams.loanToken = token; + morpho.createMarket(marketParams); + + vm.expectRevert(bytes(ErrorsLib.NO_CODE)); + morpho.supply(marketParams, amount, 0, ONBEHALF, hex""); + } + function testSupplyAssets(uint256 amount) public { amount = bound(amount, 1, MAX_TEST_AMOUNT); diff --git a/test/forge/integration/WithdrawCollateralIntegrationTest.sol b/test/forge/integration/WithdrawCollateralIntegrationTest.sol index 8a5b0ce58..c9798d0ad 100644 --- a/test/forge/integration/WithdrawCollateralIntegrationTest.sol +++ b/test/forge/integration/WithdrawCollateralIntegrationTest.sol @@ -145,7 +145,7 @@ contract WithdrawCollateralIntegrationTest is BaseTest { vm.startPrank(ONBEHALF); morpho.supplyCollateral(marketParams, amountCollateral + amountCollateralExcess, ONBEHALF, hex""); - morpho.setAuthorization(BORROWER, true); + // BORROWER is already authorized. morpho.borrow(marketParams, amountBorrowed, 0, ONBEHALF, ONBEHALF); vm.stopPrank(); diff --git a/test/forge/invariant/BaseMorphoInvariantTest.sol b/test/forge/invariant/BaseMorphoInvariantTest.sol index c48ce0855..8ba45d91b 100644 --- a/test/forge/invariant/BaseMorphoInvariantTest.sol +++ b/test/forge/invariant/BaseMorphoInvariantTest.sol @@ -46,15 +46,17 @@ contract BaseMorphoInvariantTest is InvariantTest { } modifier authorized(address onBehalf) { - if (onBehalf != msg.sender) { + if (onBehalf != msg.sender && !morpho.isAuthorized(onBehalf, msg.sender)) { vm.prank(onBehalf); morpho.setAuthorization(msg.sender, true); } _; - vm.prank(onBehalf); - morpho.setAuthorization(msg.sender, false); + if (morpho.isAuthorized(onBehalf, msg.sender)) { + vm.prank(onBehalf); + morpho.setAuthorization(msg.sender, false); + } } function _randomMarket(uint256 marketSeed) internal view returns (MarketParams memory _marketParams) { diff --git a/test/forge/libraries/SafeTransferLibTest.sol b/test/forge/libraries/SafeTransferLibTest.sol index de019de1b..38eb46e1e 100644 --- a/test/forge/libraries/SafeTransferLibTest.sol +++ b/test/forge/libraries/SafeTransferLibTest.sol @@ -85,6 +85,20 @@ contract SafeTransferLibTest is Test { this.safeTransferFrom(address(tokenWithBooleanAlwaysFalse), from, to, amount); } + function testSafeTransferTokenNotCreated(address token, address to, uint256 amount) public { + vm.assume(token.code.length == 0); + + vm.expectRevert(bytes(ErrorsLib.NO_CODE)); + this.safeTransfer(token, to, amount); + } + + function testSafeTransferFromTokenNotCreated(address token, address from, address to, uint256 amount) public { + vm.assume(token.code.length == 0); + + vm.expectRevert(bytes(ErrorsLib.NO_CODE)); + this.safeTransferFrom(token, from, to, amount); + } + function safeTransfer(address token, address to, uint256 amount) external { IERC20(token).safeTransfer(to, amount); } diff --git a/test/hardhat/Morpho.spec.ts b/test/hardhat/Morpho.spec.ts index f43d02010..c095924ba 100644 --- a/test/hardhat/Morpho.spec.ts +++ b/test/hardhat/Morpho.spec.ts @@ -1,7 +1,7 @@ import { SignerWithAddress } from "@nomicfoundation/hardhat-ethers/signers"; import { setNextBlockTimestamp } from "@nomicfoundation/hardhat-network-helpers/dist/src/helpers/time"; import { expect } from "chai"; -import { AbiCoder, MaxUint256, keccak256, toBigInt } from "ethers"; +import { AbiCoder, MaxUint256, ZeroAddress, keccak256, toBigInt } from "ethers"; import hre from "hardhat"; import { Morpho, OracleMock, ERC20Mock, IrmMock } from "types"; import { MarketParamsStruct } from "types/src/Morpho"; @@ -161,6 +161,36 @@ describe("Morpho", () => { } }); + it("should simulate gas cost [idle]", async () => { + updateMarket({ + loanToken: await loanToken.getAddress(), + collateralToken: ZeroAddress, + oracle: ZeroAddress, + irm: ZeroAddress, + lltv: 0, + }); + + await morpho.enableLltv(0); + await morpho.enableIrm(ZeroAddress); + await morpho.createMarket(marketParams); + + for (let i = 0; i < suppliers.length; ++i) { + logProgress("idle", i, suppliers.length); + + const supplier = suppliers[i]; + + let assets = BigInt.WAD * toBigInt(1 + Math.floor(random() * 100)); + + await randomForwardTimestamp(); + + await morpho.connect(supplier).supply(marketParams, assets, 0, supplier.address, "0x"); + + await randomForwardTimestamp(); + + await morpho.connect(supplier).withdraw(marketParams, assets / 2n, 0, supplier.address, supplier.address); + } + }); + it("should simulate gas cost [liquidations]", async () => { for (let i = 0; i < suppliers.length; ++i) { logProgress("liquidations", i, suppliers.length); diff --git a/test/morpho_tests.tree b/test/morpho_tests.tree deleted file mode 100644 index a2faa9950..000000000 --- a/test/morpho_tests.tree +++ /dev/null @@ -1,288 +0,0 @@ -. -└── setOwner(address newOwner) external - ├── when msg.sender not owner - │ └── revert with NOT_OWNER - └── when msg.sender is owner - ├── it should set owner to newOwner - └── it should emit SetOwner(newOwner) -. -└── enableIrm(address irm) external - ├── when msg.sender not owner - │ └── revert with NOT_OWNER - └── when msg.sender is owner - ├── it should set isIrmEnabled[irm] to true - └── it should emit EnableIrm(irm) -. -└── enableLltv(uint256 lltv) external - ├── when msg.sender not owner - │ └── revert with NOT_OWNER - └── when msg.sender is owner - ├── when lltv >= WAD - │ └── revert with MAX_LLTV_EXCEEDED - └── when lltv < WAD - ├── it should set isLltvEnabled[lltv] to true - └── it should emit EnableLltv(lltv) -. -└── setFee(MarketParams memory marketParams, uint256 newFee) external - ├── when msg.sender not owner - │ └── revert with NOT_OWNER - └── when msg.sender is owner - ├── when market is not created - │ └── revert with MARKET_NOT_CREATED - └── when market is created - ├── when newFee > MAX_FEE - │ └── revert with MAX_FEE_EXCEEDED - └── when newFee <= MAX_FEE - ├── it should accrue the interest - ├── it should set fee[marketParams.id] to newFee - └── it should emit SetFee(marketParams.id, newFee) -. -└── setFeeRecipient(address recipient) external - ├── when msg.sender not owner - │ └── revert with NOT_OWNER - └── when msg.sender is owner - ├── it should set feeRecipient to recipient - └── it should emit SetFeeRecipient(recipient) -. -└── createMarket(MarketParams memory marketParams) external - ├── when irm is not enabled - │ └── revert with IRM_NOT_ENABLED - └── when irm is enabled - ├── when marketParams.lltv is not enabled - │ └── revert with LLTV_NOT_ENABLED - └── when marketParams.lltv is enabled - ├── when market is already created - │ └── revert with MARKET_ALREADY_CREATED - └── when market is not already created - ├── it should set lastUpdate[marketParams.id] to block.timestamp - ├── it should set idToMarket[id] to marketParams - └── it should emit CreateMarket(marketParams.id, marketParams) -. -└── supply(MarketParams memory marketParams, uint256 assets, uint256 shares, address onBehalf, bytes calldata data) external - ├── when market is not created - │ └── revert with MARKET_NOT_CREATED - └── when market is created - ├── when both assets and shares are null or both assets and shares are not null - │ └─ revert with INCONSISTENT_INPUT - └── when one of assets or shares is null and one of assets or shares is not null - ├── when onBehalf is the zero address - │ └── revert with ZERO_ADDRESS - └── when onBehalf is not the zero address - ├── it should accrue the interest - ├── when assets is not zero - │ └── it should set shares to assets.toSharesUp(totalSupplyAssets[marketParams.id], totalSupplyShares[marketParams.id]) - ├── when assets is zero - │ └── it should set assets to shares.toAssetsDown(totalSupplyAssets[id], totalSupplyShares[id]) - ├── it should add shares to supplyShares[marketParams.id][onBehalf] - ├── it should add shares to totalSupplyShares[marketParams.id] - ├── it should add assets to totalSupplyAssets[marketParams.id] - ├── it should emit Supply(marketParams.id, msg.sender, onBehalf, assets, shares) - ├── if data.length > 0 - │ └── it should call sender's onMorphoSupply callback - ├── it should transfer assets of the loan asset from the sender to Morpho - └── it should return the assets and the shares supplied -. -└── withdraw(MarketParams memory marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) external - ├── when market is not created - │ └── revert with MARKET_NOT_CREATED - └── when market is created - ├── when both assets and shares are null or both assets and shares are not null - │ └─ revert with INCONSISTENT_INPUT - └── when one of assets or shares is null and one of assets or shares is not null - ├── when receiver is the zero address - │ └── revert with ZERO_ADDRESS - └── when receiver is not the zero address - ├── when not sender and not approved - │ └── revert with UNAUTHORIZED - └── when sender or approved - ├── it should accrue the interest - ├── when assets is not zero - │ └── it should set shares to assets.toSharesUp(totalSupplyAssets[marketParams.id], totalSupplyShares[marketParams.id]) - ├── when assets is zero - │ └── it should set assets to shares.toAssetsDown(totalSupplyAssets[id], totalSupplyShares[id]) - ├── it should remove shares from supplyShares[marketParams.id][onBehalf] - ├── it should remove shares from totalSupplyShares[marketParams.id] - ├── it should remove assets from totalSupplyAssets[marketParams.id] - ├── it should emit Withdraw(marketParams.id, msg.sender, onBehalf, receiver, assets, shares) - ├── it should transfer assets of the loan asset to the receiver - ├── when totalBorrowAssets[marketParams.id] > totalSupplyAssets[marketParams.id] - │ └── revert with INSUFFICIENT_LIQUIDITY - └── when totalBorrowAssets[marketParams.id] <= totalSupplyAssets[marketParams.id] - └── it should return the assets and the shares withdrawn -. -└── borrow(MarketParams memory marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) external - ├── when market is not created - │ └── revert with MARKET_NOT_CREATED - └── when market is created - ├── when both assets and shares are null or both assets and shares are not null - │ └─ revert with INCONSISTENT_INPUT - └── when one of assets or shares is null and one of assets or shares is not null - ├── when receiver is the zero address - │ └── revert with ZERO_ADDRESS - └── when receiver is not the zero address - ├── when not sender and not approved - │ └── revert with UNAUTHORIZED - └── when sender or approved - ├── it should accrue the interest - ├── when assets is not zero - │ └── it should set shares to assets.toSharesUp(totalSupplyAssets[marketParams.id], totalSupplyShares[marketParams.id]) - ├── when assets is zero - │ └── it should set assets to shares.toAssetsDown(totalSupplyAssets[id], totalSupplyShares[id]) - ├── it should add shares to borrowShares[marketParams.id][onBehalf] - ├── it should add shares to totalBorrowShares[marketParams.id] - ├── it should add assets to totalBorrowAssets[marketParams.id] - ├── it should emit Borrow(marketParams.id, msg.sender, onBehalf, receiver, assets, shares) - ├── it should transfer assets of the loan asset to the receiver - ├── when position is not healthy - │ └── revert with INSUFFICIENT_COLLATERAL - └── when position is healthy - ├── when totalBorrowAssets[marketParams.id] > totalSupplyAssets[marketParams.id] - │ └── revert with INSUFFICIENT_LIQUIDITY - └── when totalBorrowAssets[marketParams.id] <= totalSupplyAssets[marketParams.id] - └── it should return the assets and the shares borrowed - -. -└── repay(MarketParams memory marketParams, uint256 assets, uint256 shares, address onBehalf, bytes calldata data) external - ├── when market is not created - │ └── revert with MARKET_NOT_CREATED - └── when market is created - ├── when both assets and shares are null or both assets and shares are not null - │ └─ revert with INCONSISTENT_INPUT - └── when one of assets or shares is null and one of assets or shares is not null - ├── when onBehalf is the zero address - │ └── revert with ZERO_ADDRESS - └── when onBehalf is not the zero address - ├── it should accrue the interest - ├── when assets is not zero - │ └── it should set shares to assets.toSharesUp(totalSupplyAssets[marketParams.id], totalSupplyShares[marketParams.id]) - ├── when assets is zero - │ └── it should set assets to shares.toAssetsDown(totalSupplyAssets[id], totalSupplyShares[id]) - ├── it should remove shares from borrowShares[marketParams.id][onBehalf] - ├── it should remove shares from totalBorrowShares[marketParams.id] - ├── it should remove assets from totalBorrowAssets[marketParams.id] - ├── it should emit Repay(marketParams.id, msg.sender, onBehalf, assets, shares) - ├── if data.length > 0 - │ └── it should call sender's onMorphoRepay callback - ├── it should transfer assets of the loan asset from the sender to Morpho - └── it should return the assets and the shares repaid -. -└── supplyCollateral(MarketParams memory marketParams, uint256 assets, address onBehalf, bytes calldata data) external - ├── when market is not created - │ └── revert with MARKET_NOT_CREATED - └── when market is created - ├── when the assets to supply is zero - │ └── revert with ZERO_ASSETS - └── when the assets to supply is not zero - ├── when onBehalf is the zero address - │ └── revert with ZERO_ADDRESS - └── when onBehalf is not the zero address - ├── it should add assets to collateral[marketParams.id][onBehalf] - ├── it should emit SupplyCollateral(marketParams.id, msg.sender, onBehalf, assets) - ├── if data.length > 0 - │ └── it should call sender's onMorphoSupplyCollateral callback - └── it should transfer assets of the collateral asset from the sender to Morpho -. -└── withdrawCollateral(MarketParams memory marketParams, uint256 assets, address onBehalf, address receiver) external - ├── when market is not created - │ └── revert with MARKET_NOT_CREATED - └── when market is created - ├── when the assets to withdraw is zero - │ └── revert with ZERO_ASSETS - └── when the assets to withdraw is not zero - ├── when receiver is the zero address - │ └── revert with ZERO_ADDRESS - └── when receiver is not the zero address - ├── when not sender and not approved - │ └── revert with MANAGER_NOT_APPROVED - └── when sender or approved - ├── it should accrue the interest - ├── it should remove assets from collateral[marketParams.id][onBehalf] - ├── it should emit WithdrawCollateral(marketParams.id, msg.sender, onBehalf, receiver, assets) - ├── it should transfer assets of the collateral asset to the receiver - └── when position is not healthy - └── revert with INSUFFICIENT_COLLATERAL -. -└── liquidate(MarketParams memory marketParams, address borrower, uint256 seizedAssets, uint256 repaidShares, bytes calldata data) external - ├── when market is not created - │ └── revert with MARKET_NOT_CREATED - └── when market is created - ├── when both seizedAssets and repaidShares are null or both seizedAssets and repaidShares are not null - │ └─ revert with INCONSISTENT_INPUT - └── when one of seizedAssets or repaidShares is null and one of seizedAssets or repaidShares is not null - ├── it should accrue the interest - ├── when position is healthy - │ └── revert with HEALTHY_POSITION - └── when the position is not healthy - ├── when seizedAssets is not zero - │ ├── it should compute assetsRepaid = seizedAssets.mulDivUp(collateralPrice, ORACLE_PRICE_SCALE).wDivUp(liquidationIncentiveFactor(marketParams.lltv)) - │ └── it should compute repaidShares = assetsRepaid.toSharesDown(totalBorrow[marketParams.id], totalBorrowShares[market.id]) - ├── when repaidShares is not zero - │ ├── it should compute assetsRepaid = repaidShares.toAssetsUp(totalBorrow[marketParams.id], totalBorrowShares[marketParams.id]) - │ └── it should compute seizedAssets = assetsRepaid.wMulDown(liquidationIncentiveFactor).mulDivDown(ORACLE_PRICE_SCALE, collateralPrice) - ├── it should remove repaidShares from totalBorrowShares[marketParams.id] - ├── it should remove assetsRepaid from totalBorrow[marketParams.id] - ├── it should remove repaidShares from collateral[marketParams.id][borrower] - ├── if after the liquidation the borrower's collateral is 0 - │ └── it should realize bad debt - │ ├── it should compute badDebt = borrowShares[marketParams.id][borrower].toAssetsUp(totalBorrow[marketParams.id], totalBorrowShares[marketParams.id]) - │ ├── it should remove badDebt from totalSupplyAssets[marketParams.id] - │ ├── it should remove badDebt from totalBorrowAssets[marketParams.id] - │ ├── it should remove borrowShares[marketParams.id][borrower] from totalBorrowShares[marketParams.id] - │ └── it should set borrowShares[marketParams.id][borrower] to 0 - ├── it should transfer repaidShares of collateral asset to the sender - ├── it should emit Liquidate(marketParams.id, msg.sender, borrower, assetsRepaid, repaidShares, seizedAssets, badDebtShares) - ├── if data.length > 0 - │ └── it should call sender's onMorphoLiquidate callback - └── it should transfer assetsRepaid of loan asset from the sender to Morpho -. -└── flashLoan(address token, uint256 assets, bytes calldata data) external - ├── it should transfer assets of token from Morpho to the sender - ├── it should call sender's onMorphoFlashLoan callback - ├── it should emit FlashLoan(msg.sender, token, assets) - └── it should transfer assets of token from the sender to Morpho -. -└── setAuthorizationWithSig(Authorization memory authorization, Signature calldata signature) external - ├── when block.timestamp > authorization.deadline - │ └── revert with SIGNATURE_EXPIRED - └── when block.timestamp <= deadline - ├── when authorization.nonce != nonce[authorization.authorizer] - │ └── revert with INVALID_NONCE - └── when authorization.nonce == nonce[authorization.authorizer] - ├── when the signature is invalid or not signed by authorization.authorizer - │ └── revert with INVALID_SIGNATURE - └── when the signature is valid and signed by authorization.authorizer - ├── it should increment authorization.authorizer's nonce - ├── it should emit IncrementNonce(msg.sender, authorization.authorizer, authorization.nonce) - ├── it should set isAuthorized[authorization.authorizer][authorization.authorized] to authorization.isAuthorized - └── it should emit SetAuthorization(msg.sender, authorization.authorizer, authorization.authorized, authorization.isAuthorized) -. -└── setAuthorization(address authorized, bool newIsAuthorized) external - ├── should set isApproved[msg.sender][authorized] to newIsAuthorized - └── it should emit SetAuthorization(msg.sender, msg.sender, authorized, newIsAuthorized) -. -└── accrueInterest(MarketParams memory marketParams) external - ├── when market is not created - │ └── revert with MARKET_NOT_CREATED - └── when market is created - └── it should accrue the interest -. -└── _accrueInterest(MarketParams memory marketParams, Id id) internal - └── when interest not already accrued in the block - ├── it should set lastUpdate to block.timestamp - └── when marketTotalBorrow is not 0 - ├── it should compute accruedInterest = marketTotalBorrow.wMulDown(borrowRate.wTaylorCompounded(elapsed)) - ├── it should add accruedInterest to totalBorrowAssets - ├── it should add accruedInterest to totalSupplyAssets - └── when fee[id] != 0 - │ ├── it should add accruedInterest.wMulDown(fee[id]) to feeAmount - │ ├── it should add feeAmount.mulDivDown(totalSupplyShares[id], totalSupplyAssets[id] - feeAmount) to supplyShares[id][feeRecipient] - │ └── it should add feeAmount.mulDivDown(totalSupplyShares[id], totalSupplyAssets[id] - feeAmount) to totalSupplyShares[id] - └── it should emit AccrueInterest(id, borrowRate, accruedInterest, feeShares) -. -└── _isHealthy(MarketParams memory marketParams, Id id, address user, uint256 collateralPrice) internal - ├── it should compute borrowed = borrowShares[id][user].toAssetsUp(totalBorrowAssets[id], totalBorrowShares[id]) - ├── it should compute maxBorrow = collateral[id][user].mulDivDown(collateralPrice, ORACLE_PRICE_SCALE).wMulDown(marketParams.lltv) - └── it should return maxBorrow >= borrowed -. -└── liquidationIncentiveFactor(uint256 lltv) internal - └── it should return min(MAX_LIQUIDATION_INCENTIVE_FACTOR, WAD.wDivDown(WAD - LIQUIDATION_CURSOR.wMulDown(WAD - lltv))) diff --git a/tsconfig.json b/tsconfig.json index 7d4c1978e..e538e2c1d 100644 --- a/tsconfig.json +++ b/tsconfig.json @@ -1,6 +1,6 @@ { "compilerOptions": { - "target": "es6", + "target": "es2020", "module": "nodenext", "moduleResolution": "nodenext", "outDir": "dist",