Investigate soundness of symbolic execution against remote state

Our new storage representation is a lot more flexible than our old one. It should allow us to (in principle) combine symbolic reads / writes with state fetched remotely. We do however need to be careful here, it would be pretty easy to introduce unsoundness here (and I suspect that we probably do right now).

We should test around this feature any more, and either fix any soundness issues that arise, or restrict it's operation so that all user exposed combinations are sound.

Start by tracing the new storage representation and the paths for symbolic reads and writes when state is fetched remotely. Test the user-exposed combinations for unsoundness, then either document and fix each issue or restrict the combinations so every supported operation is sound.

Written by the indexing model from the issue text.