Define all remaining cases for dep_step
Define all the remaining cases for the dep_step
function. The IView
instruction is more complex as it uses the equality check in ty
and will be solved in the task https://gitlab.com/nomadic-labs/coq-tezos-of-ocaml/-/issues/206. Thus we will do it in another task.
-
have a simulation and associated proof for https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/script_interpreter_defs#transfer
Edit: actually the definition of the simulation of transfer
is impossible for now. Indeed, this requires having a dependent definition of the type Script_typed_ir.operation
. This type contains an existential type 'a
related to a 'a ty
and I do not find a formulation with our current setting. I think we should have a mutual inductive type for the values of Michelson, as this is done in Mi-Cho-Coq. This requires further work and some risks so we will do it later.
Edited by Guillaume Claret