From fa6226ac8949a47cc4141afb7f76cc1efee938f1 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Thu, 26 Sep 2024 15:45:38 -0700 Subject: [PATCH 1/4] chore: update halmos-cheatcodes submodule --- lib/halmos-cheatcodes | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/halmos-cheatcodes b/lib/halmos-cheatcodes index c0d86550..a02072cd 160000 --- a/lib/halmos-cheatcodes +++ b/lib/halmos-cheatcodes @@ -1 +1 @@ -Subproject commit c0d865508c0fee0a11b97732c5e90f9cad6b65a5 +Subproject commit a02072cd5eb8560d00c3f4a73b27831ec6e3137e From 32b24fc797449a20285117a841e2affc696f5634 Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Thu, 26 Sep 2024 16:58:50 -0700 Subject: [PATCH 2/4] test(halmos): adjust for halmos v2 --- test/halmos/HalmosTest.sol | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/test/halmos/HalmosTest.sol b/test/halmos/HalmosTest.sol index f9ddc5ec..51bab7d6 100644 --- a/test/halmos/HalmosTest.sol +++ b/test/halmos/HalmosTest.sol @@ -13,7 +13,7 @@ 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 +/// @custom:halmos --solver-timeout-assertion 0 contract HalmosTest is SymTest, Test { using MorphoLib for IMorpho; using MarketParamsLib for MarketParams; @@ -47,6 +47,17 @@ contract HalmosTest is SymTest, Test { morpho.enableLltv(lltv); morpho.createMarket(marketParams); vm.stopPrank(); + + // Enable symbolic storage + svm.enableSymbolicStorage(address(morpho)); + svm.enableSymbolicStorage(address(loanToken)); + svm.enableSymbolicStorage(address(collateralToken)); + svm.enableSymbolicStorage(address(oracle)); + svm.enableSymbolicStorage(address(irm)); + + // 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. From 387e4b5cc78ccff2d0a377ce66b04110371e814c Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Thu, 26 Sep 2024 21:04:16 -0700 Subject: [PATCH 3/4] test(halmos): fix calldata generation for flashLoan --- test/halmos/HalmosTest.sol | 24 +++++++++++++----------- 1 file changed, 13 insertions(+), 11 deletions(-) diff --git a/test/halmos/HalmosTest.sol b/test/halmos/HalmosTest.sol index 51bab7d6..73076d2a 100644 --- a/test/halmos/HalmosTest.sol +++ b/test/halmos/HalmosTest.sol @@ -8,6 +8,7 @@ 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"; @@ -29,6 +30,9 @@ contract HalmosTest is SymTest, Test { MarketParams internal marketParams; + ERC20Mock internal otherToken; + FlashBorrowerMock internal flashBorrower; + function setUp() public virtual { owner = svm.createAddress("owner"); morpho = IMorpho(address(new Morpho(owner))); @@ -48,12 +52,18 @@ contract HalmosTest is SymTest, Test { morpho.createMarket(marketParams); vm.stopPrank(); + // for flashLoan + otherToken = new ERC20Mock(); + flashBorrower = new FlashBorrowerMock(morpho); + // Enable symbolic storage 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")); @@ -85,17 +95,9 @@ contract HalmosTest is SymTest, Test { 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); + 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) { From a80998eba45966881cb4ab645395b38f710f429f Mon Sep 17 00:00:00 2001 From: Daejun Park Date: Fri, 27 Sep 2024 13:03:11 -0700 Subject: [PATCH 4/4] test(halmos): enable symbolic storage for the test contract --- test/halmos/HalmosTest.sol | 1 + 1 file changed, 1 insertion(+) diff --git a/test/halmos/HalmosTest.sol b/test/halmos/HalmosTest.sol index 73076d2a..6a6bf8a7 100644 --- a/test/halmos/HalmosTest.sol +++ b/test/halmos/HalmosTest.sol @@ -57,6 +57,7 @@ contract HalmosTest is SymTest, Test { flashBorrower = new FlashBorrowerMock(morpho); // Enable symbolic storage + svm.enableSymbolicStorage(address(this)); svm.enableSymbolicStorage(address(morpho)); svm.enableSymbolicStorage(address(loanToken)); svm.enableSymbolicStorage(address(collateralToken));