pushing verify heavy lifting into z3
also re-encoding all the "pervasives" in terms of ocaml types
I really want a macro system right now