Allow to make storage memory symbolic, even on test mode

[gustavo-grieco]

Take a look to the following example. An auditor wants to use symbolic execution in order to understand when an invariant can fail:

pragma solidity ^0.8.13;

import "forge-std/Test.sol";

contract Counter {
    uint256 public number;

    function increment() public {
        number++;
    }
}

contract CounterSymTest is Test {
    Counter public counter;

    function setUp () public {
        counter = new Counter();
    }

    function prove_isIncrementFeasible() public {
        vm.assume(counter.number() != 2);
        counter.increment();
        assertTrue(!(counter.number() == 2), "number is 2");
    }
}

However, hevm allows to run either in symbolic mode or test mode but none of them is useful here. Test mode will verify the property, since the concrete state of the Counter program is preserved and it is impossible to force some storage to be symbolic.
Purely symbolic mode will make everything symbolic, even during contract deployment, but here we only want to make the Counter storage symbolic after setUp deployed the contract.

One possible solution is add a cheatcode that allows to make the complete storage (or even specific slots) for a given address symbolic. I'm usually not pushing to add specific cheatcodes, but in this perhaps it makes sense. What do you think?

h/t @GalloDaSballo

[msooseth]

Hmmm... so I think the best would be to be able to compute invariants, such as being able to increment number to any value. Then apply this invariant and figure out that we can set number to 2. But that will take a year, if not years.

As for doing this now. You can actually make that setUp into a constructor, and pass --create. I think that should work?

[gustavo-grieco]

So you are saying that we can workaround this in symbolic mode using --create if we include the setUp into the constructor (e.g. as an internal call)?

[msooseth]

Yes, I think we can!

[msooseth]

I am working on this. And sorry -- the create trick does not work. I'm going brrrr...

[msooseth]

As @gustavo-grieco pointed out, this could be solved via:

https://github.com/a16z/halmos/blob/main/src/halmos/cheatcodes.py#L226-L238

i.e.

def symbolic_storage(ex, arg, sevm, stack):
    account = uint160(arg.get_word(4))
    account_alias = sevm.resolve_address_alias(
        ex, account, stack, allow_branching=False
    )

    if account_alias is None:
        error_msg = f"enableSymbolicStorage() or setArbitraryStorage() is not allowed for a nonexistent account: {hexify(account)}"
        raise HalmosException(error_msg)

    ex.storage[account_alias].symbolic = True

    return ByteVec()  # empty return data

Which is a cheatcode to simbolify the storage space of a contract. I think we could have this cheatcode in hevm.