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: https://github.com/foundry-rs/foundry/issues/15

• [ ] symbolicStorage(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