Halmos Soundness sanity check #744
Draft
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…th fixed MarketID but fails (as expected) when marketID passed as call data
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Minimal Example sanity checking soundness of Halmos tests.
check_isTotalBorrowAssetsZeroForFixedMarketID passes where as check_isTotalBorrowAssetsZero. Only difference is that former is calling on the fixed market (in setup) while marketId is passed as symbolic calldata in latter.
Halmos Output:
Counterexample:
halmos_assets_uint256_7b6d6b8_05 = 0x8000000000017fc00000000000000000
halmos_block.timestamp_uint64_bee682a_04 = 0x01
halmos_lltv_uint256_c41efa5_02 = 0x800000000000000
halmos_onBehalf_address_f8832d3_07 = 0x00
halmos_owner_address_f22c7fb_01 = 0x8000000000000000000000000000000000000000
halmos_receiver_address_8a81ed8_08 = 0x8000000000000000000000000000000000000000
p_caller_address_723f300_00 = 0x8000000000000000000000000000000000000000
p_id_bytes32_904ef47_00 = 0x00
p_selector_bytes4_767ebd9_00 = 0x8720316d00000000000000000000000000000000000000000000000000000000
[FAIL] check_isTotalBorrowAssetsZero(bytes4,address,bytes32) (paths: 136, time: 32.09s, bounds: [])
[PASS] check_isTotalBorrowAssetsZeroForFixedMarketID(bytes4,address) (paths: 60, time: 5.91s, bounds: [])
Looks like the selector in counterexample picks the borrow() function guessing from the args generated.
In the setup() we use enableSymbolicStorage(address(morpho)), and totalBorrowAssets is part of the market mapping in storage.
TLDR;
TotalBorrowShares is set to zero and remains zero in FixedMarket, which is not the case if marketId is symbolic. Not sure if i am missing something that explains this behaviour from halmos.