Daejun Park
Daejun Park
https://github.com/a16z/halmos/wiki/FAQ#does-halmos-provide-support-for-mainnet-forking Could you please provide more context on the use cases that you have in mind?
closing, as we don't plan to support fork testing in halmos: https://github.com/a16z/halmos/wiki/FAQ#does-halmos-provide-support-for-mainnet-forking
Note: certain options (e.g., --ffi) are desired to be inapplicable within the tags.
> Update: analyzing vyper bytecode fails on storage access for mappings > > vyper: `keccak256(uint256(slot) . uint256(key))` solidity: `keccak256(uint256(key) . uint256(slot))` > > this is a blocker, we need to...
We can update the toy examples as suggested by Karma, once #184 is fixed.
@PraneshASP could you please try again with `--solver-timeout-assertion 0`, and let us know if you still see the discrepancy between the different solc versions?
Confirmed that the old solc generated bytecode significantly slows down the prover. Will take a look how different the generated smt queries are. Thanks for reporting!
just to make sure, do you mean having `--print-full-model` enabled automatically when --symbolic-storage is given?
Fork testing (as well as other cheat codes) are currently not supported. However, depending on your use case, you may be able to achieve similar results without them in Halmos....
moved remaining items to #409, closing