Investigate soundness of symbolic execution against remote state

[d-xo]

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.