The goal of this issue is to complete the definition of the interpreter for the following instructions:
The interpreter is defined in the file https://github.com/formal-land/coq-of-rust/blob/main/CoqOfRust/move_sui/simulations/move_vm_runtime/interpreter.v