Skip to content

DIG and DUG

Basile Pesin requested to merge Vertmo/mi-cho-coq:DigDug into master

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

Merge request reports