Fully abstract VM

[d-xo]

Some parts of the VM state are still concrete only. All data types should be an Expr instance, allowing for a completely symbolic execution environment.

For the case of gas, we can cheat a little and use a partially symbolic gas model (i.e. gas is either concrete, or unknown). This will allow us to support symbolic dynamic data without having to build a (slow & complex) symbolic gas model.