Interpreter simulation: verify the Tez instructions

Fixes #252 (closed)

What makes this MR big is that we change a lot of primitive definitions like:

• changing the division operators from Z.div to Z.quot to better capture the behavior of OCaml;
• fixing the definitions of Z.to_int, Z.to_int32, Z.to_int64;
• making Option.catch an axiom rather than the identity.