feat(cheatcodes): support additional cheatcodes to aid in symbolic testing

[JuanCoRo]

Component

Forge, Cast, Chisel

Describe the feature you would like

From a conversation with Runtime Verification highlighting additional cheatcodes that would be valuable for them as well as be generic enough to lay a foundation for symbolic testing: #15

• freshStorage(address): makes the storage of the given address fully symbolic. Any subsequent SLOAD reads a random value, and then the random value that was read is memorized (so if you SLOAD the same slot again, you get the same result)

• copyStorage(address, address): copies the storage of one contract to another.

• freshAddress() , freshBool(): returns a symbolic address or bool value, respectively.

• freshBytes(uint256) external returns (bytes memory b): returns a symbolic bytes array of a given size; in Kontrol, the returned bytes b have dynamic size but we add an assumption on b.length.

• freshUInt(uint8): returns a symbolic unsigned integer of a given size in bytes. We use this freshUInt cheatcode to define fixed-length variations for unsigned (freshUInt256(), freshUInt248(), etc.) and signed integers (freshSInt32(), freshSInt8(), etc.).

• mockFunction(address callee, address calledContract, bytes calldata data): whenever a call is made to callee with calldata data, this cheatcode instead calls calledContract with the same calldata. This functionality is similar to a delegate call made to calledContract from callee. We use it to substitute a call to a client's function with another implementation that captures the primary logic of the original function but is easier to reason about. It was inspired by Foundry’s mockCall, which helps substitute a call with specified return data but allows capturing more observable behaviors than just the return value.

• expect*Call cheatcodes: similar to expectEmit, these let us specify the expected call with its callee and calldata. We use these less frequently, but I think they can be useful even for fuzzing tests.

  • expectRegularCall: Expect a call using the CALL opcode and specified parameters
  • expectStaticCall: Expect a call using the STATICCALL opcode and specified parameters
  • expectDelegateCall: Expect a call using the DELEGATECALL opcode and specified parameters
  • expectNoCall: Expect no calls to be made after this cheat code
  • expectCreate: Expects the deployment of the specified bytecode by the specified address using the CREATE opcode
  • expectCreate2: Expects the deployment of the specified bytecode by the specified address using the CREATE2 opcode

For expect cheatcodes other than expectRegularCall and expectStaticCall, we don't have tests showing their behavior, but they should be similar to the call tests. For symbolicStorage we have this test.

The fresh* cheatcodes should return a random value. The symbolicStorage could be renamed to freshStorage, and basically what it should mean is described here:

• The accounts storage should be marked as fresh (maybe just a boolean flag added to account storage datastructure).
• Reads from uninitialized slots should: (i) sample a random uint256, and then (ii) write the sampled value back to the storage.
• It should be ensured that reading the same storage slot twice gives back the same value (not random each time), but that the first read from a given storage slot after calling the freshStorage cheatcode is random.

Context:

The freshStorage is important in terms of improving the expressive power of Foundry tests significantly, and also for Kontrol "official" integration, since we can't really claim full formal verification if it's only from the 0-initialized storage.

Everything where we would return a symbolic value should basically return a random value in Foundry.

Currently, when we take our clients property tests, we have to generalize them with the above cheatcodes to make them meaningful symbolically. This has 2 downsides: (i) now their test is no longer runnable with Foundry directly, only wiht Kontrol, and (ii) the foundry tests they write aren't covering as much behavior as possible, because they can't generalize the storage or inputs as much.

Adding support to these cheatcodes directly to Foundry would solve both of these problems, users could write more general tests from the start (and fuzz them), and then switching to Kontrol for formal verification wouldn't stop them from using Foundry.

Additional context

No response

[ehildenb]

Another one we're adding is infiniteGas(): runtimeverification/evm-semantics#1524

This can probably be a no-op on the Foundry side, as I doubt that it will exercise many cases where infinite gas is actually called for. But for symbolic reasoning it's needed.

[mds1]

forge does have pauseGasMetering and resumeGasMetering cheats which effectively give the same behavior, perhaps you could use those cheat names on the KEVM side to prevent needing an infiniteGas cheat also?

[ehildenb]

Well, it's different semantics really, infinite gas means you still get gas metering but it won't run out, so you can still tell how much gas something used. Maybe you also mean that? We'll take a look. But would also be nice to have the setSymbolicStorage (or setArbitraryStorage), whcih I think should not be too hard for Foundry. It's really by far the most useful one we use.

[ehildenb]

@gakonst , I had a conversation with @mds1 about this at EthDenver, and I tried to emphasize that symbolicStorage (or arbitraryStorage) is really a massive leap in expressive power both for us and for Foundry.

When you are testing against contract state, Foundry is currently verifying that "against an initial deployment of the contract, the given property holds". Being able to fuzz against storage makes it instead that "against an arbitrary intermediate state, the given property holds", it is a massive generalization. For verification, it honestly does not even make much benefit to verify without this extra expressive power.

Cheatcode vm.setArbitraryStorage(address) and vm.setArbitraryStorage() (which uses current address or prank address), can operate in the fuzzing setting as following:

• Mark that accounts storage as arbitrary (boolean flag?)
• Every sstore that comes through, you do a normal write.
• On sload, you first check: Has that storage slot already been written?
  • If so, you return the written value.
  • If not, you generate a random uint256, and write it to the storage.

That way, every storage slot is being fuzzed over, and you can still do vm.assume(...) on read storage slots to enforce certain contract invariants. But subsequent reads from the same slot should give back the same value as before.

Note this is more general than just being able to say that some particular value is arbitrary, which can already be achieved by passing in a random uint256 to the test function and writing it to the storage slot you want to be arbitrary.

[mds1]

Agreed, I do think these would be generically useful and they all seem pretty straightforward to implement, cc @mattsse.

@ehildenb I think 1 or 2 examples of how usage would look in practice would be valuable. Would this be a good example demonstrating the use of setArbitraryStorage?

contract ERC20Burn is Test {
  ERC20 token;

  function setUp() public {
    token = new ERC20("Token", "TKN");
    vm.setArbitraryStorage(address(token));
  }

  // QUESTION: Is this supposed to be structured as a fuzz test? Or maybe we need another
  // way to specify how many runs to execute since it is different than a regular fuzz test
  function test_BurnsTheUsersFullTokenBalance() {
    // Owner should be able to burn all of the user's tokens. When the burn
    // method checks the user's balance, the `setArbitraryStorage` tells forge
    // to put a random value there since it has not yet been accessed.
    vm.prank(owner);
    token.burn(user); 
    assertEq(token.balanceOf(user), 0);
  }
}

[ehildenb]

That looks like an excellent test! If you had a token which just implemented the burn as a no-op, this test would pass without setArbitraryStorage every time. But with that, it would fail correctly.

[sambacha]

wen symbolicStorage

[ehildenb]

I think we can use freshStorage() instead of symbolicStorage(), to not confuse users of the fuzzer.

[grandizzy]

@ehildenb for copyStorage cheatcode is test below OK? thank you!

contract Counter {
    uint256 public a;
    address public b;

    function setA(uint256 _a) public {
        a = _a;
    }

    function setB(address _b) public {
        b = _b;
    }
}

contract CounterTest is Test {
    Counter public counter;
    Counter public counter1;

    function setUp() public {
        counter = new Counter();
        counter.setA(1000);
        counter.setB(address(27));

        counter1 = new Counter();
        counter1.setA(11);
        counter1.setB(address(50));
    }

    function test_copy_storage() public {
        assertEq(counter.a(), 1000);
        assertEq(counter.b(), address(27));
        assertEq(counter1.a(), 11);
        assertEq(counter1.b(), address(50));

        vm.copyStorage(address(counter), address(counter1));

        assertEq(counter.a(), 1000);
        assertEq(counter.b(), address(27));
        assertEq(counter1.a(), 1000);
        assertEq(counter1.b(), address(27));
    }
}

[grandizzy]

for keeping scope and progress relevant, remaining expect*Call cheatcodes to add will be tracked with #9310