Partial Concrete Storage for symbolic execution

> A fully symbolic contract storage is not always a desirable option when performing symbolic execution. In fact, when analyzing the state of a contract at a specific block, you might want to use the concrete values in its storage to prune some unfeasible paths and simplify the symbolic execution.

> When this mode is activated and greed encounters an SLOAD (let's say at slot id 0x5), greed will automatically fetch the concrete value of slot 0x5 in the contract's on-chain storage at block NUMBER (18808898) instead of using an unconstrained symbol. Similarly, any subsequent (and possibly symbolic) SSTORE at slot 0x5 will overwrite its value.

** In other words, you can imagine this mode of operation as a "lazy" initialization of the contract's storage in the symbolic executor that uses its on-chain storage at the specified block. **

related source:
https://ucsb-seclab.github.io/greed/advanced/

Start with the related advanced documentation and trace how symbolic execution handles SLOAD and SSTORE in hevm. Determine where a block number and on-chain storage value would enter the execution flow, then define tests covering concrete reads and later symbolic or concrete writes to the same slot.

Written by the indexing model from the issue text.