Draft: Adapt Dexter2 proofs for CPMM2
See #56
Left to do:
-
rebasing -
spec and proof for xtzToToken (!125 (merged)) -
<changes forthcoming?> spec and proof for tokenToXtz (https://gitlab.com/nomadic-labs/mi-cho-coq/-/tree/cpmm2-verification--tokenToXtz) -
spec and proof for tokenToToken (https://gitlab.com/nomadic-labs/mi-cho-coq/-/tree/cpmm2-verification--tokenToToken) (@arvidnl )
Edited by Yann Regis-Gianas