Stateful evaluation

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 commit axiomatizes a notion of evaluation state that is preserved
by all instructions but those.
2 jobs for stateful in 8 minutes (queued for 5 seconds)
latest
Status Job ID Name Coverage
  Build
passed #247427868
coq:8.8

00:04:13

passed #247427869
coq:8.9

00:08:00