Halmos Tests with Symbolic IRM #741
Conversation
|
the linter fails because i cast a Uint256 into Uint128. Halmos only has the symbolic version for Uint256 but not Uint128. Hence i cast it to Uint128. For a halmos test, this is perfectly reasonable and sound since i am casting down and all the symbolic values of Uint128 are covered. Is there a better way around? @QGarchery |
test/halmos/HalmosTest.sol
Outdated
|
|
||
| // A symbolic IRM for Halmos Tests. | ||
| contract IrmSymbolic is IIrm, SymTest, Test { | ||
| using MathLib for uint128; |
There was a problem hiding this comment.
| using MathLib for uint128; |
| 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"; | ||
|
|
||
| import {IIrm} from "../../src/interfaces/IIrm.sol"; | ||
|
|
||
| import {MathLib} from "../../src/libraries/MathLib.sol"; |
There was a problem hiding this comment.
optional
| import {MathLib} from "../../src/libraries/MathLib.sol"; | |
| 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 {IIrm} from "../../src/interfaces/IIrm.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"; | |
| import {MathLib} from "../../src/libraries/MathLib.sol"; |
…e all the fields of market are non-zero
|
interestingly, all tests pass with symbolic initialised market except |
… is called with --contract
… 20mins and 8 paths
|
|
||
| assert( | ||
| morpho.totalSupplyAssets(id) != 0 && morpho.totalSupplyShares(id) != 0 && morpho.totalBorrowAssets(id) != 0 | ||
| && morpho.totalBorrowShares(id) != 0 && morpho.fee(id) != 0 |
There was a problem hiding this comment.
interesting this test passes as we assert fee!=0. However, fee is set symbolic uint256, and hence can very well be zero.
test/halmos/HalmosTest.sol
Outdated
| vm.assume(morpho.totalBorrowAssets(id) <= morpho.totalSupplyAssets(id)); | ||
|
|
||
| // all solvers timeout on liquidate | ||
| vm.assume(selector != morpho.liquidate.selector); |
There was a problem hiding this comment.
we either remove the whole test or keep it excluding liquidate.
|
removed the check_borrowLessThanSupply test since the solver timesout. The other tests are meaningful now with the symbolicIRM and the initial state is symbolic (non-zero). |
Added a symbolic IRM contract which returns a non-deterministic rate for the borrowRate() and borrowRateView() functions. The Morpho contract now calls a symbolic IRM instead of Mock IRM. Halmos tests pass with slightly higher path exploration.