Michelson: a step function with evaluation

Fix https://gitlab.com/nomadic-labs/coq-tezos-of-ocaml/-/issues/60

The diff is very large on the interpreter but it is actually mostly indentation as the whole function is intended differently. The two main changes are:

• A {struct} parameter on gas for the step function, rather than the couple g_value (also named function_parameter) as before;
• The function Local_gas_counter.local_gas_counter_and_outdated_context is made Opaque as it was blocking the evaluation (I do not really know why, I found it by dichotomy commenting the rest of the code).

I made a beginning of proof for the equality of dep_step and step with the case IDrop and a few other ones.