New cheatcode: `symbolicStorage` variant that preserves existing storage assignments

[lisandrasilva]

Summary

The existing symbolicStorage(address) cheatcode makes the entire storage of a given address symbolic by replacing the storage map with a fresh unconstrained symbolic variable:

rule <k> #setSymbolicStorage ACCTID => .K ... </k>
     <account>
       <acctID> ACCTID </acctID>
       <storage> _ => ?STORAGE </storage>
       <origStorage> _ => ?STORAGE </origStorage>
       ...
     </account>

This is fine when you want the contract to start from a completely unconstrained state, but it discards any storage assignments already made — for example, those performed during contract initialization or a setUp phase. This makes it harder to use symbolicStorage on a contract that was partially initialized and where those initial values should be treated as invariants of the proof.

Motivation

A common proof pattern is:

function setUp() public {
    token = new MyToken();
    token.initialize(owner, initialSupply); // sets concrete storage slots
}

function test_transfer(address to, uint256 amount) public {
    vm.symbolicStorage(address(token)); // ← wipes out the initialization!
    // ...
}

The user wants to make uninitialized storage slots symbolic while keeping the concrete values set during initialize. Currently, they must manually re-apply every initialization assignment after calling symbolicStorage.

Proposed Solution

Add a new overload (or a new cheatcode name) that preserves existing storage entries and only makes unset slots symbolic:

Option A — New overload:

function symbolicStorage(address target, bool keepAssigned) external;

When keepAssigned is true, the existing storage map is kept as-is and only slots not yet assigned return a fresh symbolic value on read.

Option B — Dedicated cheatcode name:

function freshStorage(address target) external;

The name freshStorage echoes the existing freshUInt / freshBytes family and signals that unread slots are fresh symbolic values, while assigned slots retain their concrete values.

Semantics

The K rule would change from unconditionally replacing <storage> with ?STORAGE to extending the existing map with a symbolic default for unmapped keys. Concretely, the desired behavior is:

• Slots already present in <storage> retain their concrete values.
• Any slot not currently in the map, when read, returns a fresh unconstrained symbolic value (rather than the default 0).