Halmos Tests with Symbolic IRM

[bhargavbh]

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.

[bhargavbh]

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

[MathisGD]

Suggested change

using MathLib for uint128;

[MathisGD]

optional

Suggested change

	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";

[MathisGD]

just to make sure I get it right: before that the rate was always zero?

what was this line useful for then?

        svm.enableSymbolicStorage(address(irm));

[bhargavbh]

thats correct, the interest was always zero in IrmMock. borrowRate() and borrowRateView() return utilization/365 days. However, in all the halmos tests, the utilization ends up being 0 because totalBorrowShares is 0 for the market when _callMorpho() is called. Confirmed this with a test. Note that the Halmos tests are for the fixed market.

IrmMock contract has no storage values, so i am not sure whats the utility of it here.

[MathisGD]

you need to run forge fmt (see this)

[bhargavbh]

interestingly, all tests pass with symbolic initialised market except check_borrowLessThanSupply() which is the only property reasoning about totalSupplyAssets and totalBorrowAssets. Verifying it generates 46 constraints but yices timesout on solving the last constraint. Attempting to run with other solvers.