diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index 47e091715..6203f6f31 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -29,12 +29,14 @@ jobs: - 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 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/lib/halmos-cheatcodes b/lib/halmos-cheatcodes new file mode 160000 index 000000000..c0d865508 --- /dev/null +++ b/lib/halmos-cheatcodes @@ -0,0 +1 @@ +Subproject commit c0d865508c0fee0a11b97732c5e90f9cad6b65a5 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/test/halmos/HalmosTest.sol b/test/halmos/HalmosTest.sol new file mode 100644 index 000000000..f9ddc5ec8 --- /dev/null +++ b/test/halmos/HalmosTest.sol @@ -0,0 +1,183 @@ +// 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 "../../src/Morpho.sol"; +import "../../src/libraries/ConstantsLib.sol"; +import {MorphoLib} from "../../src/libraries/periphery/MorphoLib.sol"; + +/// @custom:halmos --symbolic-storage --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; + + 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(); + } + + // 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) { + uint256 rand = svm.createUint256("rand"); + address token; + if (rand == 0) { + token = address(loanToken); + } else if (rand == 1) { + token = address(collateralToken); + } else { + ERC20Mock otherToken = new ERC20Mock(); + token = address(otherToken); + } + args = abi.encode(marketParams, token, assets, emptyData); + } 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())); + } +}