feat(testing): support symbolic accounts with fresh storage

[grandizzy]

(opening this draft PR to get initial thoughts and if OK to have this impl in revm, thank you!)

Motivation

Re symbolic testing (atm with Kontrol) in foundry https://github.com/foundry-rs/foundry/issues/4072#issuecomment-1456844543

There's a need for a new freshStorage(address target) cheatcode where storage of target contract should follow rules below:

• Every SSTORE that comes through is handled as a normal write.
• On SLOAD:
  • If storage slot was already written, then written value is returned.
  • If storage slot wasn't already written, a random uint256 is generated and written to storage.

For example, for a contract like:

contract Counter {
    address[] public owners;

    function getOwner(uint256 pos) public view returns (address) {
        return owners[pos];
    }

    function setOwner(uint256 pos, address owner) public {
        owners[pos] = owner;
    }
}

a test like the one bellow should result in PASS

function test_fresh_storage(uint256 a) public {
    a = bound(a, 0, 100);

    Counter counter = new Counter();
    vm.freshStorage(address(counter));

    // Next call would fail with array out of bounds without freshStorage
    address owner = counter.getOwner(a);
    // Subsequent calls should retrieve same value
    assertEq(counter.getOwner(a), owner);
    // Change slot and make sure new value retrieved
    counter.setOwner(a, address(111));
    assertEq(counter.getOwner(a), address(111));
}

Solution

• add a new symbolic bool in Account struct, default false
• expose Account.mark_symbolic fn to enable symbolic storage
• in JournaledState.sload generate random value if account newly created and symbolic

[grandizzy]

@rakita @mattsse @DaniPopes could you please have a look at let me know if the right way to go, if so will follow up on working the random related failures. thank you!

[rakita]

This does not look like a good fit for Revm. Couldn't you add a logic in step_end that would override the sload value?

[grandizzy]

This does not look like a good fit for Revm. Couldn't you add a logic in step_end that would override the sload value?

yeah, can do that, just wanted to check if somehow needed here too. thank you, going to close this then.