Document opcode error preconditions

[adria0]

At this moment we describe the protections that geth offers in the opcodes (U64 overflow, out of gas, etc..), in error_state.

This acts as a preconditions that really models how we write the constrains for the opcodes.

But at this moment, we have to check manually all defined errors if applies to the opcode, it will be nice if we document, per opcode which preconditions exists. It will make out specs easier to check if something is wrong.