diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index e4bcbbacf..87a17a69b 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -20,21 +20,24 @@ jobs: - AssetsAccounting - ConsistentState - ExactMath + - ExchangeRate - Health - LibSummary - Liveness - - RatioMath - Reentrancy - Reverts + - StayHealthy - Transfer steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 with: submodules: recursive - name: Install python - uses: actions/setup-python@v4 + uses: actions/setup-python@v5 + with: + python-version: ">=3.9" - name: Install certora run: pip install certora-cli @@ -43,7 +46,7 @@ jobs: 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 + sudo mv solc-static-linux /usr/local/bin/solc-0.8.19 - name: Verify ${{ matrix.conf }} run: certoraRun certora/confs/${{ matrix.conf }}.conf diff --git a/.github/workflows/halmos.yml b/.github/workflows/halmos.yml new file mode 100644 index 000000000..fe56f888a --- /dev/null +++ b/.github/workflows/halmos.yml @@ -0,0 +1,31 @@ +name: Halmos + +on: + push: + branches: + - main + pull_request: + workflow_dispatch: + +jobs: + verify: + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v4 + with: + submodules: recursive + + - name: Install python + uses: actions/setup-python@v5 + with: + python-version: ">=3.9" + + - name: Install Foundry + uses: foundry-rs/foundry-toolchain@v1 + + - name: Install halmos + run: pip install halmos + + - name: Run Halmos + run: FOUNDRY_PROFILE=test halmos diff --git a/.gitmodules b/.gitmodules index 888d42dcd..ba7c98e70 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,3 +1,6 @@ [submodule "lib/forge-std"] path = lib/forge-std url = https://github.com/foundry-rs/forge-std +[submodule "lib/halmos-cheatcodes"] + path = lib/halmos-cheatcodes + url = https://github.com/a16z/halmos-cheatcodes.git diff --git a/audits/2023-11-13-morpho-blue-cantina-managed-review.pdf b/audits/2023-11-13-morpho-blue-cantina-managed-review.pdf index 090d1bef0..eb82adcdb 100644 Binary files a/audits/2023-11-13-morpho-blue-cantina-managed-review.pdf and b/audits/2023-11-13-morpho-blue-cantina-managed-review.pdf differ diff --git a/audits/2024-01-05-morpho-blue-cantina-competition.pdf b/audits/2024-01-05-morpho-blue-cantina-competition.pdf index 8db682646..b6d5e0bf7 100644 Binary files a/audits/2024-01-05-morpho-blue-cantina-competition.pdf and b/audits/2024-01-05-morpho-blue-cantina-competition.pdf differ diff --git a/certora/README.md b/certora/README.md index 8d6127320..cbd2b424c 100644 --- a/certora/README.md +++ b/certora/README.md @@ -1,6 +1,6 @@ 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). +The core concepts of 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. @@ -11,7 +11,7 @@ The Morpho Blue protocol allows users to take out collateralized loans on ERC20 ## 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. +In particular, in case of a transfer, it is assumed that the balance of Morpho Blue increases or decreases (depending if it's 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. @@ -33,7 +33,7 @@ The verification is done for the most common implementations of the ERC20 standa - [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. +- [ERC20USDT](dispatch/ERC20USDT.sol) which does not strictly respect 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. @@ -69,11 +69,11 @@ Said otherwise, markets are independent: tokens from a given market cannot be im 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. +The share mechanism is implemented symmetrically for the borrow side: a share of borrow increasing in value over time represents additional owed interest. +The rule `accrueInterestIncreasesSupplyExchangeRate` checks this property for the supply side with the following statement. ```soldidity - // Check that the ratio increases: assetsBefore/sharesBefore <= assetsAfter/sharesAfter. + // Check that the exchange rate increases: assetsBefore/sharesBefore <= assetsAfter/sharesAfter assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore; ``` @@ -107,7 +107,7 @@ 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). +More generally, this means that the result of liquidating a position multiple times eventually leads to a healthy position (possibly empty). ## Authorization @@ -205,7 +205,7 @@ As an example, the `withdrawChangesTokensAndShares` rule checks that calling the 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 `canRepayAll` rule ensures that it is always possible to repay the full debt of a position, leaving the account without any outstanding 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 @@ -214,7 +214,7 @@ Other common and known attack vectors are verified to not be possible on the Mor ### 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. +Reentrancy is a common attack vector that happens 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`. @@ -250,12 +250,13 @@ The [`certora/specs`](specs) folder contains the following files: - [`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). + Notably, 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. +- [`ExchangeRate.spec`](specs/ExchangeRate.spec) checks that the exchange rate 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. +- [`StayHealthy.spec`](specs/Health.spec) checks that functions cannot render an account unhealthy. - [`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. diff --git a/certora/confs/AccrueInterest.conf b/certora/confs/AccrueInterest.conf index 3ae9ec84b..8d4706d19 100644 --- a/certora/confs/AccrueInterest.conf +++ b/certora/confs/AccrueInterest.conf @@ -1,14 +1,16 @@ { - "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" + "files": [ + "certora/harness/MorphoHarness.sol", + "certora/harness/Util.sol" + ], + "solc": "solc-0.8.19", + "verify": "MorphoHarness:certora/specs/AccrueInterest.spec", + "prover_args": [ + "-depth 3", + "-mediumTimeout 30", + "-smt_hashingScheme plaininjectivity" + ], + "rule_sanity": "basic", + "server": "production", + "msg": "Morpho Blue Accrue Interest" } diff --git a/certora/confs/AssetsAccounting.conf b/certora/confs/AssetsAccounting.conf index e8a011349..765e597bc 100644 --- a/certora/confs/AssetsAccounting.conf +++ b/certora/confs/AssetsAccounting.conf @@ -1,9 +1,11 @@ { - "files": [ - "certora/harness/MorphoHarness.sol", - ], - "verify": "MorphoHarness:certora/specs/AssetsAccounting.spec", - "rule_sanity": "basic", - "server": "production", - "msg": "Morpho Blue Assets Accounting" + "files": [ + "certora/harness/MorphoHarness.sol", + "certora/harness/Util.sol" + ], + "solc": "solc-0.8.19", + "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 index 45c0c672f..8e7cdaca7 100644 --- a/certora/confs/ConsistentState.conf +++ b/certora/confs/ConsistentState.conf @@ -1,9 +1,11 @@ { - "files": [ - "certora/harness/MorphoHarness.sol", - ], - "verify": "MorphoHarness:certora/specs/ConsistentState.spec", - "rule_sanity": "basic", - "server": "production", - "msg": "Morpho Blue Consistent State" + "files": [ + "certora/harness/MorphoHarness.sol", + "certora/harness/Util.sol" + ], + "solc": "solc-0.8.19", + "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 index 35d755e27..2894ce6ee 100644 --- a/certora/confs/ExactMath.conf +++ b/certora/confs/ExactMath.conf @@ -1,14 +1,19 @@ { - "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" + "files": [ + "certora/harness/MorphoHarness.sol", + "certora/harness/Util.sol" + ], + "solc": "solc-0.8.19", + "verify": "MorphoHarness:certora/specs/ExactMath.spec", + "prover_args": [ + "-depth 5", + "-mediumTimeout 5", + "-timeout 3600", + "-adaptiveSolverConfig false", + "-smt_nonLinearArithmetic true", + "-solvers [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:lia2]" + ], + "rule_sanity": "basic", + "server": "production", + "msg": "Morpho Blue Exact Math" } diff --git a/certora/confs/ExchangeRate.conf b/certora/confs/ExchangeRate.conf new file mode 100644 index 000000000..2c6efcc21 --- /dev/null +++ b/certora/confs/ExchangeRate.conf @@ -0,0 +1,15 @@ +{ + "files": [ + "certora/harness/MorphoHarness.sol", + "certora/harness/Util.sol" + ], + "solc": "solc-0.8.19", + "verify": "MorphoHarness:certora/specs/ExchangeRate.spec", + "prover_args": [ + "-smt_hashingScheme plaininjectivity", + "-smt_easy_LIA true" + ], + "rule_sanity": "basic", + "server": "production", + "msg": "Morpho Blue Exchange Rate" +} diff --git a/certora/confs/Health.conf b/certora/confs/Health.conf index 9238fde6b..e052dfcf5 100644 --- a/certora/confs/Health.conf +++ b/certora/confs/Health.conf @@ -1,13 +1,15 @@ { - "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" + "files": [ + "certora/harness/MorphoHarness.sol", + "certora/harness/Util.sol", + "src/mocks/OracleMock.sol" + ], + "solc": "solc-0.8.19", + "verify": "MorphoHarness:certora/specs/Health.spec", + "prover_args": [ + "-smt_hashingScheme plaininjectivity" + ], + "rule_sanity": "basic", + "server": "production", + "msg": "Morpho Blue Health" } diff --git a/certora/confs/LibSummary.conf b/certora/confs/LibSummary.conf index 6f944ed00..61414e220 100644 --- a/certora/confs/LibSummary.conf +++ b/certora/confs/LibSummary.conf @@ -1,9 +1,14 @@ { - "files": [ - "certora/harness/MorphoHarness.sol", - ], - "verify": "MorphoHarness:certora/specs/LibSummary.spec", - "rule_sanity": "basic", - "server": "production", - "msg": "Morpho Blue Lib Summary" + "files": [ + "certora/harness/MorphoHarness.sol", + "certora/harness/Util.sol" + ], + "solc": "solc-0.8.19", + "verify": "MorphoHarness:certora/specs/LibSummary.spec", + "prover_args": [ + "-smt_bitVectorTheory true" + ], + "rule_sanity": "basic", + "server": "production", + "msg": "Morpho Blue Lib Summary" } diff --git a/certora/confs/Liveness.conf b/certora/confs/Liveness.conf index b3788c685..5c438af50 100644 --- a/certora/confs/Liveness.conf +++ b/certora/confs/Liveness.conf @@ -1,9 +1,11 @@ { - "files": [ - "certora/harness/MorphoInternalAccess.sol", - ], - "verify": "MorphoInternalAccess:certora/specs/Liveness.spec", - "rule_sanity": "basic", - "server": "production", - "msg": "Morpho Blue Liveness" + "files": [ + "certora/harness/MorphoInternalAccess.sol", + "certora/harness/Util.sol" + ], + "solc": "solc-0.8.19", + "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 deleted file mode 100644 index a0ac6df8b..000000000 --- a/certora/confs/RatioMath.conf +++ /dev/null @@ -1,14 +0,0 @@ -{ - "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 index db93b6a23..6dbec607a 100644 --- a/certora/confs/Reentrancy.conf +++ b/certora/confs/Reentrancy.conf @@ -1,12 +1,13 @@ { - "files": [ - "certora/harness/MorphoHarness.sol", - ], - "verify": "MorphoHarness:certora/specs/Reentrancy.spec", - "rule_sanity": "basic", - "prover_args": [ - "-enableStorageSplitting false", - ], - "server": "production", - "msg": "Morpho Blue Reentrancy" + "files": [ + "certora/harness/MorphoHarness.sol" + ], + "solc": "solc-0.8.19", + "verify": "MorphoHarness:certora/specs/Reentrancy.spec", + "prover_args": [ + "-enableStorageSplitting false" + ], + "rule_sanity": "basic", + "server": "production", + "msg": "Morpho Blue Reentrancy" } diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf index a31c697d4..a54d3bfd4 100644 --- a/certora/confs/Reverts.conf +++ b/certora/confs/Reverts.conf @@ -1,9 +1,11 @@ { - "files": [ - "certora/harness/MorphoHarness.sol", - ], - "verify": "MorphoHarness:certora/specs/Reverts.spec", - "rule_sanity": "basic", - "server": "production", - "msg": "Morpho Blue Reverts" + "files": [ + "certora/harness/MorphoHarness.sol", + "certora/harness/Util.sol" + ], + "solc": "solc-0.8.19", + "verify": "MorphoHarness:certora/specs/Reverts.spec", + "rule_sanity": "basic", + "server": "production", + "msg": "Morpho Blue Reverts" } diff --git a/certora/confs/StayHealthy.conf b/certora/confs/StayHealthy.conf new file mode 100644 index 000000000..dc605cf12 --- /dev/null +++ b/certora/confs/StayHealthy.conf @@ -0,0 +1,15 @@ +{ + "files": [ + "certora/harness/MorphoHarness.sol", + "certora/harness/Util.sol", + "src/mocks/OracleMock.sol" + ], + "solc": "solc-0.8.19", + "verify": "MorphoHarness:certora/specs/StayHealthy.spec", + "prover_args": [ + "-solvers [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]" + ], + "rule_sanity": "basic", + "server": "production", + "msg": "Morpho Blue Stay Healthy" +} diff --git a/certora/confs/Transfer.conf b/certora/confs/Transfer.conf index bedba566c..632ee90cf 100644 --- a/certora/confs/Transfer.conf +++ b/certora/confs/Transfer.conf @@ -1,12 +1,13 @@ { - "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" + "files": [ + "certora/harness/TransferHarness.sol", + "certora/dispatch/ERC20Standard.sol", + "certora/dispatch/ERC20USDT.sol", + "certora/dispatch/ERC20NoRevert.sol" + ], + "solc": "solc-0.8.19", + "verify": "TransferHarness:certora/specs/Transfer.spec", + "rule_sanity": "basic", + "server": "production", + "msg": "Morpho Blue Transfer" } diff --git a/certora/harness/MorphoHarness.sol b/certora/harness/MorphoHarness.sol index 016cfcde1..ce62eb35b 100644 --- a/certora/harness/MorphoHarness.sol +++ b/certora/harness/MorphoHarness.sol @@ -10,16 +10,16 @@ contract MorphoHarness is Morpho { constructor(address newOwner) Morpho(newOwner) {} - function wad() external pure returns (uint256) { - return WAD; + function idToMarketParams_(Id id) external view returns (MarketParams memory) { + return idToMarketParams[id]; } - function maxFee() external pure returns (uint256) { - return MAX_FEE; + function market_(Id id) external view returns (Market memory) { + return market[id]; } - function toMarketParams(Id id) external view returns (MarketParams memory) { - return idToMarketParams[id]; + function position_(Id id, address user) external view returns (Position memory) { + return position[id][user]; } function totalSupplyAssets(Id id) external view returns (uint256) { @@ -74,22 +74,6 @@ contract MorphoHarness is Morpho { return market[id].totalBorrowShares + SharesMathLib.VIRTUAL_SHARES; } - function libId(MarketParams memory marketParams) external pure returns (Id) { - return marketParams.id(); - } - - function refId(MarketParams memory marketParams) external pure returns (Id marketParamsId) { - marketParamsId = Id.wrap(keccak256(abi.encode(marketParams))); - } - - function libMulDivUp(uint256 x, uint256 y, uint256 d) external pure returns (uint256) { - return MathLib.mulDivUp(x, y, d); - } - - function libMulDivDown(uint256 x, uint256 y, uint256 d) external pure returns (uint256) { - return MathLib.mulDivDown(x, y, d); - } - function isHealthy(MarketParams memory marketParams, address user) external view returns (bool) { return _isHealthy(marketParams, marketParams.id(), user); } diff --git a/certora/harness/Util.sol b/certora/harness/Util.sol new file mode 100644 index 000000000..cef51dea9 --- /dev/null +++ b/certora/harness/Util.sol @@ -0,0 +1,39 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +pragma solidity 0.8.19; + +import {Id, MarketParams, MarketParamsLib} from "../../src/libraries/MarketParamsLib.sol"; +import "../../src/libraries/MathLib.sol"; +import "../../src/libraries/ConstantsLib.sol"; +import "../../src/libraries/UtilsLib.sol"; + +contract Util { + using MarketParamsLib for MarketParams; + + function wad() external pure returns (uint256) { + return WAD; + } + + function maxFee() external pure returns (uint256) { + return MAX_FEE; + } + + function libId(MarketParams memory marketParams) external pure returns (Id) { + return marketParams.id(); + } + + function refId(MarketParams memory marketParams) external pure returns (Id marketParamsId) { + marketParamsId = Id.wrap(keccak256(abi.encode(marketParams))); + } + + function libMulDivUp(uint256 x, uint256 y, uint256 d) external pure returns (uint256) { + return MathLib.mulDivUp(x, y, d); + } + + function libMulDivDown(uint256 x, uint256 y, uint256 d) external pure returns (uint256) { + return MathLib.mulDivDown(x, y, d); + } + + function libMin(uint256 x, uint256 y) external pure returns (uint256) { + return UtilsLib.min(x, y); + } +} diff --git a/certora/specs/AccrueInterest.spec b/certora/specs/AccrueInterest.spec index 7babf38de..74f986ee4 100644 --- a/certora/specs/AccrueInterest.spec +++ b/certora/specs/AccrueInterest.spec @@ -2,7 +2,7 @@ methods { function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; - function maxFee() external returns uint256 envfree; + function Util.maxFee() external returns uint256 envfree; function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => ghostMulDivDown(a,b,c); function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal returns uint256 => ghostMulDivUp(a,b,c); diff --git a/certora/specs/AssetsAccounting.spec b/certora/specs/AssetsAccounting.spec index 007500b6d..4006eb4c0 100644 --- a/certora/specs/AssetsAccounting.spec +++ b/certora/specs/AssetsAccounting.spec @@ -1,19 +1,24 @@ // SPDX-License-Identifier: GPL-2.0-or-later + +using Util as Util; + 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 totalSupplyShares(MorphoHarness.Id) external returns uint256 envfree; + function totalBorrowShares(MorphoHarness.Id) 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 Util.libMulDivDown(uint256, uint256, uint256) external returns uint256 envfree; + function Util.libMulDivUp(uint256, uint256, uint256) external returns uint256 envfree; + function Util.libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; } function expectedSupplyAssets(MorphoHarness.Id id, address user) returns uint256 { @@ -21,7 +26,7 @@ function expectedSupplyAssets(MorphoHarness.Id id, address user) returns uint256 uint256 totalSupplyAssets = virtualTotalSupplyAssets(id); uint256 totalSupplyShares = virtualTotalSupplyShares(id); - return libMulDivDown(userShares, totalSupplyAssets, totalSupplyShares); + return Util.libMulDivDown(userShares, totalSupplyAssets, totalSupplyShares); } function expectedBorrowAssets(MorphoHarness.Id id, address user) returns uint256 { @@ -29,29 +34,31 @@ function expectedBorrowAssets(MorphoHarness.Id id, address user) returns uint256 uint256 totalBorrowAssets = virtualTotalBorrowAssets(id); uint256 totalBorrowShares = virtualTotalBorrowShares(id); - return libMulDivUp(userShares, totalBorrowAssets, totalBorrowShares); + return Util.libMulDivUp(userShares, totalBorrowAssets, totalBorrowShares); } -// Check that the assets supplied are greater than the assets owned in the end. +// Check that the assets supplied are greater than the increase in owned assets. rule supplyAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { - MorphoHarness.Id id = libId(marketParams); + MorphoHarness.Id id = Util.libId(marketParams); // Assume no interest as it would increase the total supply assets. require lastUpdate(id) == e.block.timestamp; - // Assume no supply position to begin with. - require supplyShares(id, onBehalf) == 0; + // Safe require because of the sumSupplySharesCorrect invariant. + require supplyShares(id, onBehalf) <= totalSupplyShares(id); + + uint256 ownedAssetsBefore = expectedSupplyAssets(id, onBehalf); uint256 suppliedAssets; suppliedAssets, _ = supply(e, marketParams, assets, shares, onBehalf, data); uint256 ownedAssets = expectedSupplyAssets(id, onBehalf); - assert suppliedAssets >= ownedAssets; + assert ownedAssetsBefore + suppliedAssets >= to_mathint(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); + MorphoHarness.Id id = Util.libId(marketParams); // Assume no interest as it would increase the total supply assets. require lastUpdate(id) == e.block.timestamp; @@ -64,14 +71,16 @@ rule withdrawAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, ui assert withdrawnAssets <= ownedAssets; } -// Check that the assets borrowed are less than the assets owed in the end. +// Check that the increase of owed assets are greater than the borrowed assets. rule borrowAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 shares, address onBehalf, address receiver) { - MorphoHarness.Id id = libId(marketParams); + MorphoHarness.Id id = Util.libId(marketParams); // Assume no interest as it would increase the total borrowed assets. require lastUpdate(id) == e.block.timestamp; - // Assume no outstanding debt to begin with. - require borrowShares(id, onBehalf) == 0; + // Safe require because of the sumBorrowSharesCorrect invariant. + require borrowShares(id, onBehalf) <= totalBorrowShares(id); + + uint256 owedAssetsBefore = expectedBorrowAssets(id, onBehalf); // The borrow call is restricted to shares as input to make it easier on the prover. uint256 borrowedAssets; @@ -79,12 +88,12 @@ rule borrowAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint uint256 owedAssets = expectedBorrowAssets(id, onBehalf); - assert borrowedAssets <= owedAssets; + assert owedAssetsBefore + borrowedAssets <= to_mathint(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); + MorphoHarness.Id id = Util.libId(marketParams); // Assume no interest as it would increase the total borrowed assets. require lastUpdate(id) == e.block.timestamp; @@ -100,23 +109,22 @@ rule repayAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint2 assert repaidAssets >= owedAssets; } -// Check that the collateral assets supplied are greater than the assets owned in the end. +// Check that the collateral assets supplied are equal to the increase of owned assets. rule supplyCollateralAssetsAccounting(env e, MorphoHarness.MarketParams marketParams, uint256 suppliedAssets, address onBehalf, bytes data) { - MorphoHarness.Id id = libId(marketParams); + MorphoHarness.Id id = Util.libId(marketParams); - // Assume no collateral to begin with. - require collateral(id, onBehalf) == 0; + uint256 ownedAssetsBefore = collateral(id, onBehalf); supplyCollateral(e, marketParams, suppliedAssets, onBehalf, data); uint256 ownedAssets = collateral(id, onBehalf); - assert suppliedAssets == ownedAssets; + assert ownedAssetsBefore + suppliedAssets == to_mathint(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); + MorphoHarness.Id id = Util.libId(marketParams); uint256 ownedAssets = collateral(id, onBehalf); diff --git a/certora/specs/ConsistentState.spec b/certora/specs/ConsistentState.spec index d84995d8d..2d8dc466a 100644 --- a/certora/specs/ConsistentState.spec +++ b/certora/specs/ConsistentState.spec @@ -1,4 +1,7 @@ // SPDX-License-Identifier: GPL-2.0-or-later + +using Util as Util; + methods { function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; @@ -14,11 +17,11 @@ methods { function isIrmEnabled(address) external returns bool envfree; function isLltvEnabled(uint256) external returns bool envfree; function isAuthorized(address, address) external returns bool envfree; - function toMarketParams(MorphoHarness.Id) external returns MorphoHarness.MarketParams envfree; + function idToMarketParams_(MorphoHarness.Id) external returns MorphoHarness.MarketParams envfree; - function maxFee() external returns uint256 envfree; - function wad() external returns uint256 envfree; - function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; + function Util.maxFee() external returns uint256 envfree; + function Util.wad() external returns uint256 envfree; + function Util.libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; function _.borrowRate(MorphoHarness.MarketParams, MorphoHarness.Market) external => HAVOC_ECF; @@ -46,25 +49,25 @@ 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 { +hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].supplyShares uint256 newShares (uint256 oldShares) { sumSupplyShares[id] = sumSupplyShares[id] - oldShares + newShares; } -hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].borrowShares uint128 newShares (uint128 oldShares) STORAGE { +hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].borrowShares uint128 newShares (uint128 oldShares) { sumBorrowShares[id] = sumBorrowShares[id] - oldShares + newShares; } -hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].collateral uint128 newAmount (uint128 oldAmount) STORAGE { +hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].collateral uint128 newAmount (uint128 oldAmount) { sumCollateral[id] = sumCollateral[id] - oldAmount + newAmount; - idleAmount[toMarketParams(id).collateralToken] = idleAmount[toMarketParams(id).collateralToken] - oldAmount + newAmount; + idleAmount[idToMarketParams_(id).collateralToken] = idleAmount[idToMarketParams_(id).collateralToken] - oldAmount + newAmount; } -hook Sstore market[KEY MorphoHarness.Id id].totalSupplyAssets uint128 newAmount (uint128 oldAmount) STORAGE { - idleAmount[toMarketParams(id).loanToken] = idleAmount[toMarketParams(id).loanToken] - oldAmount + newAmount; +hook Sstore market[KEY MorphoHarness.Id id].totalSupplyAssets uint128 newAmount (uint128 oldAmount) { + idleAmount[idToMarketParams_(id).loanToken] = idleAmount[idToMarketParams_(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; +hook Sstore market[KEY MorphoHarness.Id id].totalBorrowAssets uint128 newAmount (uint128 oldAmount) { + idleAmount[idToMarketParams_(id).loanToken] = idleAmount[idToMarketParams_(id).loanToken] + oldAmount - newAmount; } function summarySafeTransferFrom(address token, address from, address to, uint256 amount) { @@ -83,7 +86,7 @@ definition isCreated(MorphoHarness.Id id) returns bool = // Check that the fee is always lower than the max fee constant. invariant feeInRange(MorphoHarness.Id id) - fee(id) <= maxFee(); + fee(id) <= Util.maxFee(); // Check that the accounting of totalSupplyShares is correct. invariant sumSupplySharesCorrect(MorphoHarness.Id id) @@ -101,17 +104,13 @@ invariant borrowLessThanSupply(MorphoHarness.Id id) // Check correctness of applying idToMarketParams() to an identifier. invariant hashOfMarketParamsOf(MorphoHarness.Id id) isCreated(id) => - libId(toMarketParams(id)) == id; + Util.libId(idToMarketParams_(id)) == id; // Check correctness of applying id() to a market params. // This invariant is useful in the following rule, to link an id back to a market. invariant marketParamsOfHashOf(MorphoHarness.MarketParams marketParams) - isCreated(libId(marketParams)) => - toMarketParams(libId(marketParams)).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; + isCreated(Util.libId(marketParams)) => + idToMarketParams_(Util.libId(marketParams)) == marketParams; // Check that the idle amount on the singleton is greater to the sum amount, that is the sum over all the markets of the total supply plus the total collateral minus the total borrow. invariant idleAmountLessThanBalance(address token) @@ -150,14 +149,14 @@ invariant idleAmountLessThanBalance(address token) // Check that a market can only exist if its LLTV is enabled. invariant onlyEnabledLltv(MorphoHarness.MarketParams marketParams) - isCreated(libId(marketParams)) => isLltvEnabled(marketParams.lltv); + isCreated(Util.libId(marketParams)) => isLltvEnabled(marketParams.lltv); invariant lltvSmallerThanWad(uint256 lltv) - isLltvEnabled(lltv) => lltv < wad(); + isLltvEnabled(lltv) => lltv < Util.wad(); // Check that a market can only exist if its IRM is enabled. invariant onlyEnabledIrm(MorphoHarness.MarketParams marketParams) - isCreated(libId(marketParams)) => isIrmEnabled(marketParams.irm); + isCreated(Util.libId(marketParams)) => isIrmEnabled(marketParams.irm); // Check the pseudo-injectivity of the hashing function id(). rule libIdUnique() { @@ -165,13 +164,9 @@ rule libIdUnique() { MorphoHarness.MarketParams marketParams2; // Assume that arguments are the same. - require libId(marketParams1) == libId(marketParams2); + require Util.libId(marketParams1) == Util.libId(marketParams2); - assert marketParams1.loanToken == marketParams2.loanToken; - assert marketParams1.collateralToken == marketParams2.collateralToken; - assert marketParams1.oracle == marketParams2.oracle; - assert marketParams1.irm == marketParams2.irm; - assert marketParams1.lltv == marketParams2.lltv; + assert marketParams1 == marketParams2; } // Check that only the user is able to change who is authorized to manage his position. diff --git a/certora/specs/ExactMath.spec b/certora/specs/ExactMath.spec index d25465c25..254588176 100644 --- a/certora/specs/ExactMath.spec +++ b/certora/specs/ExactMath.spec @@ -1,4 +1,7 @@ // SPDX-License-Identifier: GPL-2.0-or-later + +using Util as Util; + methods { function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; @@ -12,8 +15,8 @@ methods { function lastUpdate(MorphoHarness.Id) external returns uint256 envfree; function fee(MorphoHarness.Id) external returns uint256 envfree; - function maxFee() external returns uint256 envfree; - function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; + function Util.maxFee() external returns uint256 envfree; + function Util.libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivDown(a,b,c); function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivUp(a,b,c); @@ -32,12 +35,12 @@ function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 { 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); +// Check that when not accruing interest, and when repaying all, the borrow exchange rate is at least reset to the initial exchange rate. +// More details on the purpose of this rule in ExchangeRate.spec. +rule repayAllResetsBorrowExchangeRate(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { + MorphoHarness.Id id = Util.libId(marketParams); // Safe require because this invariant is checked in ConsistentState.spec - require fee(id) <= maxFee(); + require fee(id) <= Util.maxFee(); mathint assetsBefore = virtualTotalBorrowAssets(id); mathint sharesBefore = virtualTotalBorrowShares(id); @@ -55,13 +58,13 @@ rule repayAllResetsBorrowRatio(env e, MorphoHarness.MarketParams marketParams, u mathint sharesAfter = virtualTotalBorrowShares(id); assert assetsAfter == 1; - // There are at least as many shares as virtual shares. + // There are at least as many shares as virtual shares, by definition of virtualTotalBorrowShares. } // There should be no profit from supply followed immediately by withdraw. rule supplyWithdraw() { MorphoHarness.MarketParams marketParams; - MorphoHarness.Id id = libId(marketParams); + MorphoHarness.Id id = Util.libId(marketParams); env e1; env e2; address onBehalf; @@ -94,7 +97,7 @@ rule supplyWithdraw() { // There should be no profit from borrow followed immediately by repaying all. rule borrowRepay() { MorphoHarness.MarketParams marketParams; - MorphoHarness.Id id = libId(marketParams); + MorphoHarness.Id id = Util.libId(marketParams); address onBehalf; env e1; env e2; diff --git a/certora/specs/RatioMath.spec b/certora/specs/ExchangeRate.spec similarity index 67% rename from certora/specs/RatioMath.spec rename to certora/specs/ExchangeRate.spec index 1fabb7742..e2ae790ca 100644 --- a/certora/specs/RatioMath.spec +++ b/certora/specs/ExchangeRate.spec @@ -1,4 +1,7 @@ // SPDX-License-Identifier: GPL-2.0-or-later + +using Util as Util; + methods { function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; @@ -10,9 +13,10 @@ methods { function fee(MorphoHarness.Id) external returns uint256 envfree; function lastUpdate(MorphoHarness.Id) external returns uint256 envfree; - function maxFee() external returns uint256 envfree; - function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; + function Util.maxFee() external returns uint256 envfree; + function Util.libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; + function UtilsLib.min(uint256 x, uint256 y) internal returns uint256 => summaryMin(x, y); function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivDown(a,b,c); 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; @@ -22,7 +26,11 @@ methods { } invariant feeInRange(MorphoHarness.Id id) - fee(id) <= maxFee(); + fee(id) <= Util.maxFee(); + +function summaryMin(uint256 x, uint256 y) returns uint256 { + return x < y ? x : y; +} // This is a simple overapproximative summary, stating that it rounds in the right direction. function summaryMulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 { @@ -41,7 +49,7 @@ function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 { } // Check that accrueInterest increases the value of supply shares. -rule accrueInterestIncreasesSupplyRatio(env e, MorphoHarness.MarketParams marketParams) { +rule accrueInterestIncreasesSupplyExchangeRate(env e, MorphoHarness.MarketParams marketParams) { MorphoHarness.Id id; requireInvariant feeInRange(id); @@ -54,12 +62,12 @@ rule accrueInterestIncreasesSupplyRatio(env e, MorphoHarness.MarketParams market mathint assetsAfter = virtualTotalSupplyAssets(id); mathint sharesAfter = virtualTotalSupplyShares(id); - // Check that the ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter. + // Check that the exchange rate 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) { +rule accrueInterestIncreasesBorrowExchangeRate(env e, MorphoHarness.MarketParams marketParams) { MorphoHarness.Id id; requireInvariant feeInRange(id); @@ -72,13 +80,13 @@ rule accrueInterestIncreasesBorrowRatio(env e, MorphoHarness.MarketParams market mathint assetsAfter = virtualTotalBorrowAssets(id); mathint sharesAfter = virtualTotalBorrowShares(id); - // Check that the ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter. + // Check that the exchange rate 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) +rule onlyLiquidateCanDecreaseSupplyExchangeRate(env e, method f, calldataarg args) filtered { f -> !f.isView && f.selector != sig:liquidate(MorphoHarness.MarketParams, address, uint256, uint256, bytes).selector } @@ -98,12 +106,12 @@ filtered { mathint assetsAfter = virtualTotalSupplyAssets(id); mathint sharesAfter = virtualTotalSupplyShares(id); - // Check that the ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter + // Check that the exchange rate 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) +rule liquidateWithoutBadDebtRealizationIncreasesSupplyExchangeRate(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, uint256 repaidShares, bytes data) { MorphoHarness.Id id; requireInvariant feeInRange(id); @@ -123,14 +131,14 @@ rule liquidateWithoutBadDebtRealizationIncreasesSupplyRatio(env e, MorphoHarness // Trick to ensure that no bad debt realization happened. require collateral(id, borrower) != 0; - // Check that the ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter + // Check that the exchange rate 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) +// The liquidate function is checked separately, see below. +rule onlyAccrueInterestCanIncreaseBorrowExchangeRate(env e, method f, calldataarg args) filtered { f -> !f.isView && f.selector != sig:repay(MorphoHarness.MarketParams, uint256, uint256, address, bytes).selector && @@ -140,7 +148,7 @@ filtered { MorphoHarness.Id id; requireInvariant feeInRange(id); - // Interest would increase borrow ratio, so we need to assume that no time passes. + // Interest would increase borrow exchange rate, so we need to assume that no time passes. require lastUpdate(id) == e.block.timestamp; mathint assetsBefore = virtualTotalBorrowAssets(id); @@ -151,34 +159,56 @@ filtered { mathint assetsAfter = virtualTotalBorrowAssets(id); mathint sharesAfter = virtualTotalBorrowShares(id); - // Check that the ratio decreases: assetsBefore/sharesBefore >= assetsAfter / sharesAfter + // Check that the exchange rate 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. +// Check the case where it would not repay more than the total assets. // 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) +rule repayDecreasesBorrowExchangeRate(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { - MorphoHarness.Id id = libId(marketParams); + MorphoHarness.Id id = Util.libId(marketParams); requireInvariant feeInRange(id); mathint assetsBefore = virtualTotalBorrowAssets(id); mathint sharesBefore = virtualTotalBorrowShares(id); - // Interest would increase borrow ratio, so we need to assume that no time passes. + // Interest would increase borrow exchange rate, 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. + // Check the case where it would not repay more than the total assets. require repaidAssets < assetsBefore; mathint assetsAfter = virtualTotalBorrowAssets(id); mathint sharesAfter = virtualTotalBorrowShares(id); assert assetsAfter == assetsBefore - repaidAssets; - // Check that the ratio decreases: assetsBefore/sharesBefore >= assetsAfter / sharesAfter + // Check that the exchange rate decreases: assetsBefore/sharesBefore >= assetsAfter/sharesAfter + assert assetsBefore * sharesAfter >= assetsAfter * sharesBefore; +} + +rule liquidateDecreasesBorrowExchangeRate(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, uint256 repaidShares, bytes data) +{ + require data.length == 0; + MorphoHarness.Id id = Util.libId(marketParams); + + mathint assetsBefore = virtualTotalBorrowAssets(id); + mathint sharesBefore = virtualTotalBorrowShares(id); + + // Interest would increase borrow exchange rate, so we need to assume that no time passes. + require lastUpdate(id) == e.block.timestamp; + + liquidate(e, marketParams, borrower, seizedAssets, repaidShares, data); + + mathint assetsAfter = virtualTotalBorrowAssets(id); + mathint sharesAfter = virtualTotalBorrowShares(id); + + require assetsAfter != 1; + + // Check that the exchange rate decreases: assetsBefore/sharesBefore >= assetsAfter/sharesAfter assert assetsBefore * sharesAfter >= assetsAfter * sharesBefore; } diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec index 45c535187..28fed1d80 100644 --- a/certora/specs/Health.spec +++ b/certora/specs/Health.spec @@ -1,15 +1,21 @@ // SPDX-License-Identifier: GPL-2.0-or-later + +using Util as Util; + methods { function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; + function totalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree; function totalBorrowShares(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 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 Util.libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; function isHealthy(MorphoHarness.MarketParams, address user) external returns bool envfree; function _.price() external => mockPrice() expect uint256; @@ -46,43 +52,12 @@ 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); + MorphoHarness.Id id = Util.libId(marketParams); address user; // Assume that the e.msg.sender is not authorized. @@ -95,7 +70,6 @@ filtered { f -> !f.isView } mathint collateralBefore = collateral(id, user); - priceChanged = false; f(e, data); mathint collateralAfter = collateral(id, user); @@ -110,7 +84,7 @@ invariant alwaysCollateralized(MorphoHarness.Id id, address borrower) // Checks that passing a seized amount input to liquidate leads to repaid shares S and repaid amount A such that liquidating instead with shares S also repays the amount A. rule liquidateEquivalentInputDebtAndInputCollateral(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) { - MorphoHarness.Id id = libId(marketParams); + MorphoHarness.Id id = Util.libId(marketParams); // Assume no interest accrual to ease the verification. require lastUpdate(id) == e.block.timestamp; diff --git a/certora/specs/LibSummary.spec b/certora/specs/LibSummary.spec index 030e89140..1d2e8dc08 100644 --- a/certora/specs/LibSummary.spec +++ b/certora/specs/LibSummary.spec @@ -1,26 +1,35 @@ // SPDX-License-Identifier: GPL-2.0-or-later + +using Util as Util; + methods { function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; - function libMulDivUp(uint256, uint256, uint256) external returns uint256 envfree; - function libMulDivDown(uint256, uint256, uint256) external returns uint256 envfree; - function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; - function refId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; + function Util.libMulDivUp(uint256, uint256, uint256) external returns uint256 envfree; + function Util.libMulDivDown(uint256, uint256, uint256) external returns uint256 envfree; + function Util.libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; + function Util.refId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; + function Util.libMin(uint256 x, uint256 y) external returns uint256 envfree; } -// Check the summary of MathLib.mulDivUp required by RatioMath.spec +// Check the summary of MathLib.mulDivUp required by ExchangeRate.spec rule checkSummaryMulDivUp(uint256 x, uint256 y, uint256 d) { - uint256 result = libMulDivUp(x, y, d); + uint256 result = Util.libMulDivUp(x, y, d); assert result * d >= x * y; } -// Check the summary of MathLib.mulDivDown required by RatioMath.spec +// Check the summary of MathLib.mulDivDown required by ExchangeRate.spec rule checkSummaryMulDivDown(uint256 x, uint256 y, uint256 d) { - uint256 result = libMulDivDown(x, y, d); + uint256 result = Util.libMulDivDown(x, y, d); assert result * d <= x * y; } // Check the summary of MarketParamsLib.id required by Liveness.spec rule checkSummaryId(MorphoHarness.MarketParams marketParams) { - assert libId(marketParams) == refId(marketParams); + assert Util.libId(marketParams) == Util.refId(marketParams); +} + +rule checkSummaryMin(uint256 x, uint256 y) { + uint256 refMin = x < y ? x : y; + assert Util.libMin(x, y) == refMin; } diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec index e6a78ed6a..8ef6f5cb1 100644 --- a/certora/specs/Liveness.spec +++ b/certora/specs/Liveness.spec @@ -1,4 +1,7 @@ // SPDX-License-Identifier: GPL-2.0-or-later + +using Util as Util; + methods { function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; function supplyShares(MorphoInternalAccess.Id, address) external returns uint256 envfree; @@ -13,8 +16,8 @@ methods { function nonce(address) external returns uint256 envfree; function isAuthorized(address, address) external returns bool envfree; - function libId(MorphoInternalAccess.MarketParams) external returns MorphoInternalAccess.Id envfree; - function refId(MorphoInternalAccess.MarketParams) external returns MorphoInternalAccess.Id envfree; + function Util.libId(MorphoInternalAccess.MarketParams) external returns MorphoInternalAccess.Id envfree; + function Util.refId(MorphoInternalAccess.MarketParams) external returns MorphoInternalAccess.Id envfree; function _._accrueInterest(MorphoInternalAccess.MarketParams memory marketParams, MorphoInternalAccess.Id id) internal with (env e) => summaryAccrueInterest(e, marketParams, id) expect void; @@ -28,7 +31,7 @@ persistent ghost mapping(address => mathint) balance { } function summaryId(MorphoInternalAccess.MarketParams marketParams) returns MorphoInternalAccess.Id { - return refId(marketParams); + return Util.refId(marketParams); } function summarySafeTransferFrom(address token, address from, address to, uint256 amount) { @@ -67,7 +70,7 @@ definition isCreated(MorphoInternalAccess.Id id) returns bool = // Check that tokens and shares are properly accounted following a supply. rule supplyChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { - MorphoInternalAccess.Id id = libId(marketParams); + MorphoInternalAccess.Id id = Util.libId(marketParams); // Safe require because Morpho cannot call such functions by itself. require currentContract != e.msg.sender; @@ -103,7 +106,7 @@ rule canSupplyByPassingShares(env e, MorphoInternalAccess.MarketParams marketPar // Check that tokens and shares are properly accounted following a withdraw. rule withdrawChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) { - MorphoInternalAccess.Id id = libId(marketParams); + MorphoInternalAccess.Id id = Util.libId(marketParams); // Assume that Morpho is not the receiver. require currentContract != receiver; @@ -139,7 +142,7 @@ rule canWithdrawByPassingShares(env e, MorphoInternalAccess.MarketParams marketP // Check that tokens and shares are properly accounted following a borrow. rule borrowChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) { - MorphoInternalAccess.Id id = libId(marketParams); + MorphoInternalAccess.Id id = Util.libId(marketParams); // Assume that Morpho is not the receiver. require currentContract != receiver; @@ -175,7 +178,7 @@ rule canBorrowByPassingShares(env e, MorphoInternalAccess.MarketParams marketPar // Check that tokens and shares are properly accounted following a repay. rule repayChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { - MorphoInternalAccess.Id id = libId(marketParams); + MorphoInternalAccess.Id id = Util.libId(marketParams); // Safe require because Morpho cannot call such functions by itself. require currentContract != e.msg.sender; @@ -214,7 +217,7 @@ rule canRepayByPassingShares(env e, MorphoInternalAccess.MarketParams marketPara // Check that tokens and balances are properly accounted following a supplyCollateral. rule supplyCollateralChangesTokensAndBalance(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, address onBehalf, bytes data) { - MorphoInternalAccess.Id id = libId(marketParams); + MorphoInternalAccess.Id id = Util.libId(marketParams); // Safe require because Morpho cannot call such functions by itself. require currentContract != e.msg.sender; @@ -233,7 +236,7 @@ rule supplyCollateralChangesTokensAndBalance(env e, MorphoInternalAccess.MarketP // Check that tokens and balances are properly accounted following a withdrawCollateral. rule withdrawCollateralChangesTokensAndBalance(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, address onBehalf, address receiver) { - MorphoInternalAccess.Id id = libId(marketParams); + MorphoInternalAccess.Id id = Util.libId(marketParams); // Assume that Morpho is not the receiver. require currentContract != receiver; @@ -254,7 +257,7 @@ rule withdrawCollateralChangesTokensAndBalance(env e, MorphoInternalAccess.Marke // Check that tokens are properly accounted following a liquidate. rule liquidateChangesTokens(env e, MorphoInternalAccess.MarketParams marketParams, address borrower, uint256 seized, uint256 repaidShares, bytes data) { - MorphoInternalAccess.Id id = libId(marketParams); + MorphoInternalAccess.Id id = Util.libId(marketParams); // Safe require because Morpho cannot call such functions by itself. require currentContract != e.msg.sender; @@ -310,7 +313,7 @@ rule setAuthorizationWithSigChangesNonceAndAuthorizes(env e, MorphoInternalAcces // Check that one can always repay the debt in full. rule canRepayAll(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, bytes data) { - MorphoInternalAccess.Id id = libId(marketParams); + MorphoInternalAccess.Id id = Util.libId(marketParams); // Assume no callback, which still allows to repay all. require data.length == 0; @@ -341,7 +344,7 @@ rule canRepayAll(env e, MorphoInternalAccess.MarketParams marketParams, uint256 // Check the one can always withdraw all, under the condition that there are no outstanding debt on the market. rule canWithdrawAll(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, address receiver) { - MorphoInternalAccess.Id id = libId(marketParams); + MorphoInternalAccess.Id id = Util.libId(marketParams); // Assume a full withdraw. require shares == supplyShares(id, e.msg.sender); @@ -366,7 +369,7 @@ rule canWithdrawAll(env e, MorphoInternalAccess.MarketParams marketParams, uint2 // Check that a user can always withdraw all, under the condition that this user does not have an outstanding debt. // Combined with the canRepayAll rule, this ensures that a borrower can always fully exit a market. rule canWithdrawCollateralAll(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, address receiver) { - MorphoInternalAccess.Id id = libId(marketParams); + MorphoInternalAccess.Id id = Util.libId(marketParams); // Ensure a full withdrawCollateral. require assets == collateral(id, e.msg.sender); diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec index 531db22f8..d6a3a468f 100644 --- a/certora/specs/Reverts.spec +++ b/certora/specs/Reverts.spec @@ -1,4 +1,7 @@ // SPDX-License-Identifier: GPL-2.0-or-later + +using Util as Util; + methods { function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; @@ -14,10 +17,10 @@ methods { function isAuthorized(address, address) external returns bool envfree; function nonce(address) external returns uint256 envfree; - function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; + function Util.libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; - function maxFee() external returns uint256 envfree; - function wad() external returns uint256 envfree; + function Util.maxFee() external returns uint256 envfree; + function Util.wad() external returns uint256 envfree; } definition isCreated(MorphoHarness.Id id) returns bool = @@ -27,7 +30,7 @@ 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 { +hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].collateral uint128 newAmount (uint128 oldAmount) { sumCollateral[id] = sumCollateral[id] - oldAmount + newAmount; } @@ -81,18 +84,18 @@ rule enableLltvRevertCondition(env e, uint256 lltv) { address oldOwner = owner(); bool oldIsLltvEnabled = isLltvEnabled(lltv); enableLltv@withrevert(e, lltv); - assert lastReverted <=> e.msg.value != 0 || e.msg.sender != oldOwner || lltv >= wad() || oldIsLltvEnabled; + assert lastReverted <=> e.msg.value != 0 || e.msg.sender != oldOwner || lltv >= Util.wad() || oldIsLltvEnabled; } // Check that setFee reverts when its inputs are not validated. // setFee can also revert if the accrueInterest reverts. rule setFeeInputValidation(env e, MorphoHarness.MarketParams marketParams, uint256 newFee) { - MorphoHarness.Id id = libId(marketParams); + MorphoHarness.Id id = Util.libId(marketParams); address oldOwner = owner(); bool wasCreated = isCreated(id); setFee@withrevert(e, marketParams, newFee); bool hasReverted = lastReverted; - assert e.msg.value != 0 || e.msg.sender != oldOwner || !wasCreated || newFee > maxFee() => hasReverted; + assert e.msg.value != 0 || e.msg.sender != oldOwner || !wasCreated || newFee > Util.maxFee() => hasReverted; } // Check the revert condition for the setFeeRecipient function. @@ -105,7 +108,7 @@ rule setFeeRecipientRevertCondition(env e, address newFeeRecipient) { // Check that createMarket reverts when its input are not validated. rule createMarketInputValidation(env e, MorphoHarness.MarketParams marketParams) { - MorphoHarness.Id id = libId(marketParams); + MorphoHarness.Id id = Util.libId(marketParams); bool irmEnabled = isIrmEnabled(marketParams.irm); bool lltvEnabled = isLltvEnabled(marketParams.lltv); bool wasCreated = isCreated(id); @@ -173,7 +176,7 @@ rule setAuthorizationWithSigInputValidation(env e, MorphoHarness.Authorization a // Check that accrueInterest reverts when its inputs are not validated. rule accrueInterestInputValidation(env e, MorphoHarness.MarketParams marketParams) { - bool wasCreated = isCreated(libId(marketParams)); + bool wasCreated = isCreated(Util.libId(marketParams)); accrueInterest@withrevert(e, marketParams); assert !wasCreated => lastReverted; } diff --git a/certora/specs/StayHealthy.spec b/certora/specs/StayHealthy.spec new file mode 100644 index 000000000..78ace84d3 --- /dev/null +++ b/certora/specs/StayHealthy.spec @@ -0,0 +1,118 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +import "Health.spec"; + +// Check that without accruing interest, no interaction can put an healthy account into an unhealthy one. +// The liquidate function times out in this rule, but has been checked separately. +rule stayHealthy(env e, method f, calldataarg data) +filtered { + f -> !f.isView && + f.selector != sig:liquidate(MorphoHarness.MarketParams, address, uint256, uint256, bytes).selector +} +{ + MorphoHarness.MarketParams marketParams; + MorphoHarness.Id id = Util.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; + + f(e, data); + + // Safe require because of the invariant sumBorrowSharesCorrect. + require borrowShares(id, user) <= totalBorrowShares(id); + + bool stillHealthy = isHealthy(marketParams, user); + assert !priceChanged => stillHealthy; +} + +// The liquidate case for the stayHealthy rule, assuming no bad debt realization, otherwise it times out. +// This particular rule makes the following assumptions: +// - the market of the liquidation is the market of the user, see the *DifferentMarkets rule, +// - there is still some borrow on the market after liquidation, see the *LastBorrow rule. +rule stayHealthyLiquidate(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) { + MorphoHarness.Id id = Util.libId(marketParams); + address user; + + // Assume the invariant initially. + require isHealthy(marketParams, user); + + uint256 debtSharesBefore = borrowShares(id, user); + uint256 debtAssetsBefore = summaryMulDivUp(debtSharesBefore, virtualTotalBorrowAssets(id), virtualTotalBorrowShares(id)); + // 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; + + liquidate(e, marketParams, borrower, seizedAssets, 0, data); + require !priceChanged; + + // Safe require because of the invariant sumBorrowSharesCorrect. + require borrowShares(id, user) <= totalBorrowShares(id); + // Assume that there is still some borrow on the market after liquidation. + require totalBorrowAssets(id) > 0; + // Assume no bad debt realization. + require collateral(id, borrower) > 0; + + assert user != borrower; + assert debtSharesBefore == borrowShares(id, user); + assert debtAssetsBefore >= summaryMulDivUp(debtSharesBefore, virtualTotalBorrowAssets(id), virtualTotalBorrowShares(id)); + + bool stillHealthy = isHealthy(marketParams, user); + require !priceChanged; + assert stillHealthy; +} + +rule stayHealthyLiquidateDifferentMarkets(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) { + MorphoHarness.Id id = Util.libId(marketParams); + address user; + MorphoHarness.MarketParams liquidationMarketParams; + + // Assume the invariant initially. + 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; + // Assume that the liquidation is on a different market. + require liquidationMarketParams != marketParams; + + liquidate(e, liquidationMarketParams, borrower, seizedAssets, 0, data); + require !priceChanged; + + // Safe require because of the invariant sumBorrowSharesCorrect. + require borrowShares(id, user) <= totalBorrowShares(id); + + bool stillHealthy = isHealthy(marketParams, user); + require !priceChanged; + assert stillHealthy; +} + +rule stayHealthyLiquidateLastBorrow(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, bytes data) { + MorphoHarness.Id id = Util.libId(marketParams); + address user; + + // Assume the invariant initially. + 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; + + liquidate(e, marketParams, borrower, seizedAssets, 0, data); + require !priceChanged; + + // Safe require because of the invariant sumBorrowSharesCorrect. + require borrowShares(id, user) <= totalBorrowShares(id); + // Assume that there is no remaining borrow on the market after liquidation. + require totalBorrowAssets(id) == 0; + + bool stillHealthy = isHealthy(marketParams, user); + require !priceChanged; + assert stillHealthy; +} diff --git a/foundry.toml b/foundry.toml index aecd8c162..4206698fd 100644 --- a/foundry.toml +++ b/foundry.toml @@ -1,4 +1,5 @@ [profile.default] +libs = ["lib"] names = true sizes = true via-ir = true diff --git a/lib/halmos-cheatcodes b/lib/halmos-cheatcodes new file mode 160000 index 000000000..a02072cd5 --- /dev/null +++ b/lib/halmos-cheatcodes @@ -0,0 +1 @@ +Subproject commit a02072cd5eb8560d00c3f4a73b27831ec6e3137e diff --git a/morpho-blue-whitepaper.pdf b/morpho-blue-whitepaper.pdf index b9a5a73c9..01945f918 100644 Binary files a/morpho-blue-whitepaper.pdf and b/morpho-blue-whitepaper.pdf differ diff --git a/package.json b/package.json index 1d942bfe8..bcc0e8d00 100644 --- a/package.json +++ b/package.json @@ -16,6 +16,7 @@ "test:forge:invariant": "FOUNDRY_MATCH_CONTRACT=InvariantTest yarn test:forge", "test:forge:integration": "FOUNDRY_MATCH_CONTRACT=IntegrationTest yarn test:forge", "test:hardhat": "npx hardhat test", + "test:halmos": "FOUNDRY_PROFILE=test halmos", "lint": "yarn lint:forge && yarn lint:hardhat", "lint:forge": "forge fmt --check", "lint:hardhat": "prettier --check test/hardhat", diff --git a/src/interfaces/IMorpho.sol b/src/interfaces/IMorpho.sol index 9c82524cb..4684e778c 100644 --- a/src/interfaces/IMorpho.sol +++ b/src/interfaces/IMorpho.sol @@ -50,8 +50,8 @@ struct Signature { /// @dev Consider using the IMorpho interface instead of this one. interface IMorphoBase { /// @notice The EIP-712 domain separator. - /// @dev Warning: Every EIP-712 signed message based on this domain separator can be reused on another chain sharing - /// the same chain id because the domain separator would be the same. + /// @dev Warning: Every EIP-712 signed message based on this domain separator can be reused on chains sharing the + /// same chain id and on forks because the domain separator would be the same. function DOMAIN_SEPARATOR() external view returns (bytes32); /// @notice The owner of the contract. @@ -196,7 +196,7 @@ interface IMorphoBase { ) external returns (uint256 assetsBorrowed, uint256 sharesBorrowed); /// @notice Repays `assets` or `shares` on behalf of `onBehalf`, optionally calling back the caller's - /// `onMorphoReplay` function with the given `data`. + /// `onMorphoRepay` function with the given `data`. /// @dev Either `assets` or `shares` should be zero. To repay max, pass the `shares`'s balance of `onBehalf`. /// @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 diff --git a/test/forge/BaseTest.sol b/test/forge/BaseTest.sol index eafb6465d..3ab71b0e7 100644 --- a/test/forge/BaseTest.sol +++ b/test/forge/BaseTest.sol @@ -139,13 +139,6 @@ contract BaseTest is Test { return bound(blocks, 1, type(uint32).max); } - /// @dev Bounds the fuzzing input to a non-zero address. - /// @dev This function should be used in place of `vm.assume` in invariant test handler functions: - /// https://github.com/foundry-rs/foundry/issues/4190. - function _boundAddressNotZero(address input) internal view virtual returns (address) { - return address(uint160(bound(uint256(uint160(input)), 1, type(uint160).max))); - } - function _supply(uint256 amount) internal { loanToken.setBalance(address(this), amount); morpho.supply(marketParams, amount, 0, address(this), hex""); @@ -194,9 +187,9 @@ contract BaseTest is Test { uint256 maxCollateral = amountBorrowed.wDivDown(marketParams.lltv).mulDivDown(ORACLE_PRICE_SCALE, priceCollateral); - amountCollateral = bound(amountBorrowed, 0, Math.min(maxCollateral, MAX_COLLATERAL_ASSETS)); + amountCollateral = bound(amountCollateral, 0, Math.min(maxCollateral, MAX_COLLATERAL_ASSETS)); - vm.assume(amountCollateral > 0); + vm.assume(amountCollateral > 0 && amountCollateral < maxCollateral); return (amountCollateral, amountBorrowed, priceCollateral); } @@ -312,12 +305,8 @@ contract BaseTest is Test { { Id _id = _marketParams.id(); - uint256 borrowShares = morpho.borrowShares(_id, onBehalf); - (,, uint256 totalBorrowAssets, uint256 totalBorrowShares) = morpho.expectedMarketBalances(_marketParams); - // Rounding assets up can yield a value larger than `totalBorrowAssets` in case `totalBorrowAssets` is zero. - uint256 maxRepayAssets = - UtilsLib.min(borrowShares.toAssetsUp(totalBorrowAssets, totalBorrowShares), totalBorrowAssets); + uint256 maxRepayAssets = morpho.borrowShares(_id, onBehalf).toAssetsDown(totalBorrowAssets, totalBorrowShares); return bound(assets, 0, maxRepayAssets); } @@ -341,19 +330,16 @@ contract BaseTest is Test { { Id _id = _marketParams.id(); - (,, uint256 totalBorrowAssets, uint256 totalBorrowShares) = morpho.expectedMarketBalances(_marketParams); - - // Rounding assets up can yield a value larger than `totalBorrowAssets` in case `totalBorrowAssets` is zero. - uint256 maxRepaidAssets = UtilsLib.min( - morpho.borrowShares(_id, borrower).toAssetsUp(totalBorrowAssets, totalBorrowShares), totalBorrowAssets - ); - uint256 collateralPrice = IOracle(_marketParams.oracle).price(); + uint256 borrowShares = morpho.borrowShares(_id, borrower); + (,, uint256 totalBorrowAssets, uint256 totalBorrowShares) = morpho.expectedMarketBalances(_marketParams); + uint256 maxRepaidAssets = borrowShares.toAssetsDown(totalBorrowAssets, totalBorrowShares); uint256 maxSeizedAssets = maxRepaidAssets.wMulDown(_liquidationIncentiveFactor(_marketParams.lltv)).mulDivDown( ORACLE_PRICE_SCALE, collateralPrice ); - return bound(seizedAssets, 0, Math.min(morpho.collateral(_id, borrower), maxSeizedAssets)); + uint256 collateral = morpho.collateral(_id, borrower); + return bound(seizedAssets, 0, Math.min(collateral, maxSeizedAssets)); } function _boundLiquidateRepaidShares(MarketParams memory _marketParams, address borrower, uint256 repaidShares) @@ -370,7 +356,8 @@ contract BaseTest is Test { (,, uint256 totalBorrowAssets, uint256 totalBorrowShares) = morpho.expectedMarketBalances(marketParams); uint256 maxRepaidShares = maxRepaidAssets.toSharesDown(totalBorrowAssets, totalBorrowShares); - return bound(repaidShares, 0, Math.min(morpho.borrowShares(_id, borrower), maxRepaidShares)); + uint256 borrowShares = morpho.borrowShares(_id, borrower); + return bound(repaidShares, 0, Math.min(borrowShares, maxRepaidShares)); } function _maxBorrow(MarketParams memory _marketParams, address user) internal view returns (uint256) { diff --git a/test/forge/invariant/BaseMorphoInvariantTest.sol b/test/forge/invariant/BaseMorphoInvariantTest.sol index 8ba45d91b..ca7a2fe7a 100644 --- a/test/forge/invariant/BaseMorphoInvariantTest.sol +++ b/test/forge/invariant/BaseMorphoInvariantTest.sol @@ -153,9 +153,12 @@ contract BaseMorphoInvariantTest is InvariantTest { logCall("liquidateSeizedAssets") { uint256 collateralPrice = oracle.price(); - uint256 repaidAssets = seizedAssets.mulDivUp(collateralPrice, ORACLE_PRICE_SCALE).wDivUp( - _liquidationIncentiveFactor(_marketParams.lltv) - ); + uint256 liquidationIncentiveFactor = _liquidationIncentiveFactor(_marketParams.lltv); + (,, uint256 totalBorrowAssets, uint256 totalBorrowShares) = morpho.expectedMarketBalances(_marketParams); + uint256 seizedAssetsQuoted = seizedAssets.mulDivUp(collateralPrice, ORACLE_PRICE_SCALE); + uint256 repaidShares = + seizedAssetsQuoted.wDivUp(liquidationIncentiveFactor).toSharesUp(totalBorrowAssets, totalBorrowShares); + uint256 repaidAssets = repaidShares.toAssetsUp(totalBorrowAssets, totalBorrowShares); loanToken.setBalance(msg.sender, repaidAssets); @@ -213,7 +216,7 @@ contract BaseMorphoInvariantTest is InvariantTest { function withdrawAssetsOnBehalfNoRevert(uint256 marketSeed, uint256 assets, uint256 onBehalfSeed, address receiver) external { - receiver = _boundAddressNotZero(receiver); + vm.assume(receiver != address(0)); MarketParams memory _marketParams = _randomMarket(marketSeed); @@ -229,7 +232,7 @@ contract BaseMorphoInvariantTest is InvariantTest { function borrowAssetsOnBehalfNoRevert(uint256 marketSeed, uint256 assets, uint256 onBehalfSeed, address receiver) external { - receiver = _boundAddressNotZero(receiver); + vm.assume(receiver != address(0)); MarketParams memory _marketParams = _randomMarket(marketSeed); @@ -283,7 +286,7 @@ contract BaseMorphoInvariantTest is InvariantTest { uint256 onBehalfSeed, address receiver ) external { - receiver = _boundAddressNotZero(receiver); + vm.assume(receiver != address(0)); MarketParams memory _marketParams = _randomMarket(marketSeed); diff --git a/test/halmos/HalmosTest.sol b/test/halmos/HalmosTest.sol new file mode 100644 index 000000000..6a6bf8a7a --- /dev/null +++ b/test/halmos/HalmosTest.sol @@ -0,0 +1,197 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +pragma solidity ^0.8.0; + +import "../../lib/forge-std/src/Test.sol"; +import {SymTest} from "../../lib/halmos-cheatcodes/src/SymTest.sol"; + +import {IMorpho} from "../../src/interfaces/IMorpho.sol"; +import {IrmMock} from "../../src/mocks/IrmMock.sol"; +import {ERC20Mock} from "../../src/mocks/ERC20Mock.sol"; +import {OracleMock} from "../../src/mocks/OracleMock.sol"; +import {FlashBorrowerMock} from "../../src/mocks/FlashBorrowerMock.sol"; + +import "../../src/Morpho.sol"; +import "../../src/libraries/ConstantsLib.sol"; +import {MorphoLib} from "../../src/libraries/periphery/MorphoLib.sol"; + +/// @custom:halmos --solver-timeout-assertion 0 +contract HalmosTest is SymTest, Test { + using MorphoLib for IMorpho; + using MarketParamsLib for MarketParams; + + address internal owner; + + IMorpho internal morpho; + ERC20Mock internal loanToken; + ERC20Mock internal collateralToken; + OracleMock internal oracle; + IrmMock internal irm; + uint256 internal lltv; + + MarketParams internal marketParams; + + ERC20Mock internal otherToken; + FlashBorrowerMock internal flashBorrower; + + function setUp() public virtual { + owner = svm.createAddress("owner"); + morpho = IMorpho(address(new Morpho(owner))); + + loanToken = new ERC20Mock(); + collateralToken = new ERC20Mock(); + oracle = new OracleMock(); + oracle.setPrice(ORACLE_PRICE_SCALE); + irm = new IrmMock(); + lltv = svm.createUint256("lltv"); + + marketParams = MarketParams(address(loanToken), address(collateralToken), address(oracle), address(irm), lltv); + + vm.startPrank(owner); + morpho.enableIrm(address(irm)); + morpho.enableLltv(lltv); + morpho.createMarket(marketParams); + vm.stopPrank(); + + // for flashLoan + otherToken = new ERC20Mock(); + flashBorrower = new FlashBorrowerMock(morpho); + + // Enable symbolic storage + svm.enableSymbolicStorage(address(this)); + svm.enableSymbolicStorage(address(morpho)); + svm.enableSymbolicStorage(address(loanToken)); + svm.enableSymbolicStorage(address(collateralToken)); + svm.enableSymbolicStorage(address(oracle)); + svm.enableSymbolicStorage(address(irm)); + svm.enableSymbolicStorage(address(otherToken)); + svm.enableSymbolicStorage(address(flashBorrower)); + + // Set symbolic block number and timestamp + vm.roll(svm.createUint(64, "block.number")); + vm.warp(svm.createUint(64, "block.timestamp")); + } + + // Call Morpho, assuming interacting with only the defined market for performance reasons. + function _callMorpho(bytes4 selector, address caller) internal { + vm.assume(selector != morpho.extSloads.selector); + vm.assume(selector != morpho.createMarket.selector); + + bytes memory emptyData = hex""; + uint256 assets = svm.createUint256("assets"); + uint256 shares = svm.createUint256("shares"); + address onBehalf = svm.createAddress("onBehalf"); + address receiver = svm.createAddress("receiver"); + + bytes memory args; + + if (selector == morpho.supply.selector || selector == morpho.repay.selector) { + args = abi.encode(marketParams, assets, shares, onBehalf, emptyData); + } else if (selector == morpho.withdraw.selector || selector == morpho.borrow.selector) { + args = abi.encode(marketParams, assets, shares, onBehalf, receiver); + } else if (selector == morpho.supplyCollateral.selector) { + args = abi.encode(marketParams, assets, onBehalf, emptyData); + } else if (selector == morpho.withdrawCollateral.selector) { + args = abi.encode(marketParams, assets, onBehalf, receiver); + } else if (selector == morpho.liquidate.selector) { + address borrower = svm.createAddress("borrower"); + args = abi.encode(marketParams, borrower, assets, shares, emptyData); + } else if (selector == morpho.flashLoan.selector) { + address token = svm.createAddress("token"); + bytes memory _data = svm.createBytes(1024, "_data"); + args = abi.encode(token, assets, _data); + } else if (selector == morpho.accrueInterest.selector) { + args = abi.encode(marketParams); + } else if (selector == morpho.setFee.selector) { + uint256 newFee = svm.createUint256("newFee"); + args = abi.encode(marketParams, newFee); + } else { + args = svm.createBytes(1024, "data"); + } + + vm.prank(caller); + (bool success,) = address(morpho).call(abi.encodePacked(selector, args)); + vm.assume(success); + } + + // Check that the fee is always smaller than the max fee. + function check_feeInRange(bytes4 selector, address caller, Id id) public { + vm.assume(morpho.fee(id) <= MAX_FEE); + + _callMorpho(selector, caller); + + assert(morpho.fee(id) <= MAX_FEE); + } + + // Check that there is always less borrow than supply on the market. + function check_borrowLessThanSupply(bytes4 selector, address caller, Id id) public { + vm.assume(morpho.totalBorrowAssets(id) <= morpho.totalSupplyAssets(id)); + + _callMorpho(selector, caller); + + assert(morpho.totalBorrowAssets(id) <= morpho.totalSupplyAssets(id)); + } + + // Check that the market cannot be "destroyed". + function check_lastUpdateNonZero(bytes4 selector, address caller, Id id) public { + vm.assume(morpho.lastUpdate(id) != 0); + + _callMorpho(selector, caller); + + assert(morpho.lastUpdate(id) != 0); + } + + // Check that the lastUpdate can only increase. + function check_lastUpdateCannotDecrease(bytes4 selector, address caller, Id id) public { + uint256 lastUpdateBefore = morpho.lastUpdate(id); + + _callMorpho(selector, caller); + + uint256 lastUpdateAfter = morpho.lastUpdate(id); + assert(lastUpdateAfter >= lastUpdateBefore); + } + + // Check that enabled LLTVs are necessarily less than 1. + function check_lltvSmallerThanWad(bytes4 selector, address caller, uint256 _lltv) public { + vm.assume(!morpho.isLltvEnabled(_lltv) || _lltv < 1e18); + + _callMorpho(selector, caller); + + assert(!morpho.isLltvEnabled(_lltv) || _lltv < 1e18); + } + + // Check that LLTVs can't be disabled. + function check_lltvCannotBeDisabled(bytes4 selector, address caller) public { + _callMorpho(selector, caller); + + assert(morpho.isLltvEnabled(lltv)); + } + + // Check that IRMs can't be disabled. + // Note: IRM is not symbolic, that is not ideal. + function check_irmCannotBeDisabled(bytes4 selector, address caller) public { + _callMorpho(selector, caller); + + assert(morpho.isIrmEnabled(address(irm))); + } + + // Check that the nonce of users cannot decrease. + function check_nonceCannotDecrease(bytes4 selector, address caller, address user) public { + uint256 nonceBefore = morpho.nonce(user); + + _callMorpho(selector, caller); + + uint256 nonceAfter = morpho.nonce(user); + assert(nonceAfter == nonceBefore || nonceAfter == nonceBefore + 1); + } + + // Check that idToMarketParams cannot change. + // Note: ok because createMarket is never called by _callMorpho. + function check_idToMarketParamsForCreatedMarketCannotChange(bytes4 selector, address caller, Id id) public { + MarketParams memory itmpBefore = morpho.idToMarketParams(id); + + _callMorpho(selector, caller); + + MarketParams memory itmpAfter = morpho.idToMarketParams(id); + assert(Id.unwrap(itmpBefore.id()) == Id.unwrap(itmpAfter.id())); + } +} diff --git a/yarn.lock b/yarn.lock index cf01a8890..f97c8ad90 100644 --- a/yarn.lock +++ b/yarn.lock @@ -1713,11 +1713,11 @@ brace-expansion@^2.0.1: balanced-match "^1.0.0" braces@^3.0.2, braces@~3.0.2: - version "3.0.2" - resolved "https://registry.yarnpkg.com/braces/-/braces-3.0.2.tgz#3454e1a462ee8d599e236df336cd9ea4f8afe107" - integrity sha512-b8um+L1RzM3WDSzvhm6gIz1yfTbBt6YTlcEKAvsmqCZZFw46z626lVj9j1yEPW33H5H+lBQpZMP1k8l+78Ha0A== + version "3.0.3" + resolved "https://registry.yarnpkg.com/braces/-/braces-3.0.3.tgz#490332f40919452272d55a8480adc0c441358789" + integrity sha512-yQbXgO/OSZVD2IsiLlro+7Hf6Q18EJrKSEsdoMzKePKXct3gvD8oLcOQdIzGupr5Fj+EDe8gO/lxc1BzfMpxvA== dependencies: - fill-range "^7.0.1" + fill-range "^7.1.1" brorand@^1.1.0: version "1.1.0" @@ -2353,7 +2353,7 @@ ecc-jsbn@~0.1.1: jsbn "~0.1.0" safer-buffer "^2.1.0" -elliptic@6.5.4, elliptic@^6.5.2, elliptic@^6.5.4: +elliptic@6.5.4, elliptic@^6.5.2: version "6.5.4" resolved "https://registry.yarnpkg.com/elliptic/-/elliptic-6.5.4.tgz#da37cebd31e79a1367e941b592ed1fbebd58abbb" integrity sha512-iLhC6ULemrljPZb+QutR5TQGB+pdW6KGD5RSegS+8sorOZT+rdQFbsQFJgvN3eRqNALqJer4oQ16YvJHlU8hzQ== @@ -2366,6 +2366,19 @@ elliptic@6.5.4, elliptic@^6.5.2, elliptic@^6.5.4: minimalistic-assert "^1.0.1" minimalistic-crypto-utils "^1.0.1" +elliptic@^6.5.7: + version "6.5.7" + resolved "https://registry.yarnpkg.com/elliptic/-/elliptic-6.5.7.tgz#8ec4da2cb2939926a1b9a73619d768207e647c8b" + integrity sha512-ESVCtTwiA+XhY3wyh24QqRGBoP3rEdDUl3EDUUo9tft074fi19IrdpH7hLCMMP3CIj7jb3W96rn8lt/BqIlt5Q== + dependencies: + bn.js "^4.11.9" + brorand "^1.1.0" + hash.js "^1.0.0" + hmac-drbg "^1.0.1" + inherits "^2.0.4" + minimalistic-assert "^1.0.1" + minimalistic-crypto-utils "^1.0.1" + emoji-regex@^7.0.1: version "7.0.3" resolved "https://registry.yarnpkg.com/emoji-regex/-/emoji-regex-7.0.3.tgz#933a04052860c85e83c122479c4748a8e4c72156" @@ -2795,10 +2808,10 @@ fastq@^1.6.0: dependencies: reusify "^1.0.4" -fill-range@^7.0.1: - version "7.0.1" - resolved "https://registry.yarnpkg.com/fill-range/-/fill-range-7.0.1.tgz#1919a6a7c75fe38b2c7c77e5198535da9acdda40" - integrity sha512-qOo9F+dMUmC2Lcb4BbVvnKJxTPjCm+RRpe4gDuGrzkL7mEVl/djYSu2OdQ2Pa302N4oqkSg9ir6jaLWJ2USVpQ== +fill-range@^7.1.1: + version "7.1.1" + resolved "https://registry.yarnpkg.com/fill-range/-/fill-range-7.1.1.tgz#44265d3cac07e3ea7dc247516380643754a05292" + integrity sha512-YsGpe3WHLK8ZYi4tWDg2Jy3ebRz2rXowDxnld4bkQB00cc/1Zw9AWnC0i9ztDJitivtQvaI9KaLyKrc+hBW0yg== dependencies: to-regex-range "^5.0.1" @@ -4411,6 +4424,11 @@ node-addon-api@^2.0.0: resolved "https://registry.yarnpkg.com/node-addon-api/-/node-addon-api-2.0.2.tgz#432cfa82962ce494b132e9d72a15b29f71ff5d32" integrity sha512-Ntyt4AIXyaLIuMHF6IOoTakB3K+RWxwtsHNRxllEoA6vPwP9o4866g6YWDLUdnucilZhmkxiHwHr11gAENw+QA== +node-addon-api@^5.0.0: + version "5.1.0" + resolved "https://registry.yarnpkg.com/node-addon-api/-/node-addon-api-5.1.0.tgz#49da1ca055e109a23d537e9de43c09cca21eb762" + integrity sha512-eh0GgfEkpnoWDq+VY8OyvYhFEzBk6jIYbRKdIlyTiAXIVJ8PyBaKb0rp7oDtoddbdoHWhq8wwr+XZ81F1rpNdA== + node-emoji@^1.10.0: version "1.11.0" resolved "https://registry.yarnpkg.com/node-emoji/-/node-emoji-1.11.0.tgz#69a0150e6946e2f115e9d7ea4df7971e2628301c" @@ -5148,12 +5166,12 @@ scrypt-js@3.0.1, scrypt-js@^3.0.0: integrity sha512-cdwTTnqPu0Hyvf5in5asVdZocVDTNRmR7XEcJuIzMjJeSHybHl7vpB66AzwTaIg6CLSbtjcxc8fqcySfnTkccA== secp256k1@^4.0.1: - version "4.0.3" - resolved "https://registry.yarnpkg.com/secp256k1/-/secp256k1-4.0.3.tgz#c4559ecd1b8d3c1827ed2d1b94190d69ce267303" - integrity sha512-NLZVf+ROMxwtEj3Xa562qgv2BK5e2WNmXPiOdVIPLgs6lyTzMvBq0aWTYMI5XCP9jZMVKOcqZLw/Wc4vDkuxhA== + version "4.0.4" + resolved "https://registry.yarnpkg.com/secp256k1/-/secp256k1-4.0.4.tgz#58f0bfe1830fe777d9ca1ffc7574962a8189f8ab" + integrity sha512-6JfvwvjUOn8F/jUoBY2Q1v5WY5XS+rj8qSe0v8Y4ezH4InLgTEeOOPQsRll9OV429Pvo6BCHGavIyJfr3TAhsw== dependencies: - elliptic "^6.5.4" - node-addon-api "^2.0.0" + elliptic "^6.5.7" + node-addon-api "^5.0.0" node-gyp-build "^4.2.0" "semver@2 || 3 || 4 || 5", semver@^5.5.0, semver@^5.7.0: