DIG and DUG
I'm currently working on adding the (future) DIG and DUG instructions to Mi-Cho-Coq. See tezos/tezos!1031 (closed) for reference.
I've already done both syntax (and therefore typing) and semantics. All I've got left to do is to prove the calculated precondition is correct.
Edited by Basile Pesin