Evaluating a Michelson instruction is not totally stateless. In particular there are a few cases where I; I; ASSERT_CMPEQ actually fails:
- I = STEPS_TO_QUOTA because the second one has less gas available
- instructions producing operations because operations are signed with a cryptographic nonce that changes at each operation
This MR axiomatizes a notion of evaluation state that is preserved by all instructions but those.