FAQ

Does Halmos provide support for mainnet forking?

The mental model of symbolic testing is to ensure that a given contract behaves as expected against all possible inputs and external contracts' states. To achieve this, external contracts need be mocked to represent their arbitrary storage states. This is why we haven't yet prioritized the mainnet forking feature. That said, we've noticed that some external storage slots need to be specified to match the current value from the mainnet. We plan to support additional cheatcodes to allow for that.

Please feel free to share examples that illustrate the use cases you have in mind, as it will greatly help us in developing the cheatcodes for mainnet forking.

How to simulate mainnet forking?

To simulate mainnet forking, you can create mock contracts that are initialized based on the current state of deployed contracts.

For example, consider the following contract:

contract Counter {
    uint public total; // slot 0

    mapping (address => uint) public map; // slot 1

    function increment(address user) public {
        map[user]++;
        total++;
    }
}

Suppose that the current state of the Counter contract on mainnet is:

• total: 12
• map[0x1001]: 7
• map[0x1002]: 5

Then, a mock counter contract can be created using the vm.etch() and vm.store() cheatcodes as follows.

1. First, create a new (empty) contract:

   Counter counter = Counter(address(new EmptyContract()));

   where EmptyContract serves as a dummy placeholder contract:

   contract EmptyContract { }

2. Then, set the bytecode of counter to the deployed bytecode: (Replace <bytecode> with the actual bytecode of the Counter contract from the mainnet.)

   vm.etch(address(counter), <bytecode>);

3. Next, initialize the storage slots to reflect the current state values:

   // counter.total = 12
   vm.store(address(counter), bytes32(counter_total_slot), bytes32(uint(12)));
   
   // counter.map[0x1001] = 7
   vm.store(address(counter), keccak256(abi.encode(address(0x1001), counter_map_slot)), bytes32(uint(7)));
   
   // counter.map[0x1002] = 5
   vm.store(address(counter), keccak256(abi.encode(address(0x1002), counter_map_slot)), bytes32(uint(5)));

   where the slot numbers can be identified in the storageLayout section in Counter.json:

   uint counter_total_slot = 0;
   uint counter_map_slot = 1;

   • Note that when setting storage for mappings or arrays, their slots should be constructed using keccak256 directly, rather than relying on precomputed hash values. This is because the hash function used internally during symbolic execution differs from the standard keccak256.

     For example, the following will NOT work as expected in Halmos:

     /* ❌ DO NOT THIS:
     // counter.map[0x1001] = 7
     vm.store(address(counter), bytes32(0xf04c2c5f6f9b62a2b5225d778c263b65e9f9e981a3c2cee9583d90b6a62a361c), bytes32(uint(7)));
     
     // counter.map[0x1002] = 5
     vm.store(address(counter), bytes32(0x292339123265925891d3d1c06602cc560d8bb722fcb2db8d37c0fc7a3456fc09), bytes32(uint(5)));
     */

Now, you can test whether the mock contract has been correctly initialized:

    function check_setup() public {
        assertEq(counter.total(), 12);
        assertEq(counter.map(address(0x1001)), 7);
        assertEq(counter.map(address(0x1002)), 5);
        assertEq(counter.map(address(0x1003)), 0); // uninitialized storage slots default to a zero value
    }   

You can also test contract invariants using the mock contract:

    function check_invariant(address user) public {
        // for any user, map[user] <= total
        assertLe(counter.map(user), counter.total());
    }

The full example can be found at: https://github.com/a16z/halmos/blob/main/examples/simple/test/Fork.t.sol

Is Halmos deterministic?

In theory: yes. In practice: no. Halmos itself has no random elements and re-running on the same inputs should provide the same outputs. However, Halmos does invoke external solvers with unpredictable timings, so these are a source of unpredictability. For instance, the number of paths explored may be different between 2 invocations, because the branching solver may have successfully excluded a path (unsat) in one run, but not in the next run (timeout).

To eliminate the branching solver as a source of nondeterminism, you can try running with halmos --solver-timeout-branching 0 (so you let the branching solver run until it returns either sat or unsat and don't accept unknown as an answer).