Empty stack pre- and post-condition notation does not allow for abstract big_map, contract, and operation literals

[sskeirik]

Currently, we execute pre- and post-conditions in an environment starting with an empty stack and PUSHing on all needed values on the stack. The problem comes when we want pre- and post-conditions to constrain abstract values of type big_map, contract, and operation.

Because these values are not PUSHable by Michelson, we should not use the PUSH instruction to put them on the stack. However, since our pre- and post-conditions execute in an environment with no initial stack, it is impossible to refer to these abstract values.

NOTE: it may be that K-Michelson can push them, but that syntax will not be interoperable with the reference client or other clients.