Verify the dexter contract
Ongoing work to publish the dexter smart contract and the accompying fa1.2 from camlCase in mi-cho-coq.
See MR: !69 (merged) !71
Tasks:
-
Dexter contract -
Informal specification (@arvidnl) -
Coq specification (@arvidnl) -
approve -
addLiquidity -
removeLiquidity -
xtzToToken -
tokenToXtz -
tokenToToken -
updateTokenPoolInternal -
updateTokenPool -
setBaker -
setManager -
default
-
-
Implementation (camlCase) -
approve -
addLiquidity -
removeLiquidity -
xtzToToken -
tokenToXtz -
tokenToToken -
updateTokenPoolInternal -
updateTokenPool -
setBaker -
setManager -
default
-
-
Coq proof (@onurb and @colin.g) -
approve (@onurb https://gitlab.com/nomadic-labs/mi-cho-coq/tree/dexter-verification-approve) -
addLiquidity (@colin.g: warning: subject to upcoming changes) -
removeLiquidity (@colin.g: warning: subject to upcoming changes) -
xtzToToken (@ksojakova: warning: subject to upcoming changes) -
tokenToXtz (@ksojakova: warning: subject to upcoming changes) -
tokenToToken (@ksojakova: warning: subject to upcoming changes) -
updateTokenPoolInternal (@colin.g) -
updateTokenPool (@colin.g) -
setBaker (@colin.g) -
setManager (@colin.g) -
default (@colin.g)
-
-
-
FA1.2 contract (see !82 (closed)) -
Informal specification (@arvidnl) -
Coq specification (@ksojakova) -
Coq proof (@ksojakova)
-
See ongoing work in branch https://gitlab.com/nomadic-labs/mi-cho-coq/tree/dexter-verification
Edited by Arvid Jakobsson