WIP: Model crypto nonces generated when operations are forged
Evaluating a Michelson instruction is not totally stateless. Since operations are signed with a cryptographic nonce that changes at each operation forging, there is a semantic difference between calling an instruction forging an operation twice with the same parameter and calling it once and then
DUPing the result.
This MR axiomatizes a notion of evaluation state that is preserved by all instructions but those that forge operations.