https://gitlab.com/nomadic-labs/mi-cho-coq
Tip revision: 1bbce76e64651eac23567e27d30d16aa311ed9c5 authored by Arvid Jakobsson on 30 April 2021, 11:11:23 UTC
Merge branch 'arvid@cpmm2-verification' into 'dexter_fa12lqt-verification'
Merge branch 'arvid@cpmm2-verification' into 'dexter_fa12lqt-verification'
Tip revision: 1bbce76
dexter_string.v
(* Open Source License *)
(* Copyright (c) 2021 Nomadic Labs. <contact@nomadic-labs.com> *)
(* Permission is hereby granted, free of charge, to any person obtaining a *)
(* copy of this software and associated documentation files (the "Software"), *)
(* to deal in the Software without restriction, including without limitation *)
(* the rights to use, copy, modify, merge, publish, distribute, sublicense, *)
(* and/or sell copies of the Software, and to permit persons to whom the *)
(* Software is furnished to do so, subject to the following conditions: *)
(* The above copyright notice and this permission notice shall be included *)
(* in all copies or substantial portions of the Software. *)
(* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR *)
(* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, *)
(* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL *)
(* THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER *)
(* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING *)
(* FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER *)
(* DEALINGS IN THE SOFTWARE. *)
Require Import String.
Definition ep_addLiquidity : string := "{ DUP ;
CDR ;
SWAP ;
CAR ;
SWAP ;
DUP ;
CDR ;
SWAP ;
CAR ;
SWAP ;
DUP ;
CDR ;
SWAP ;
CAR ;
SWAP ;
NOW ;
COMPARE ;
GE ;
IF
{ DROP 4 ; PUSH nat 3 ; FAILWITH }
{ PUSH mutez 1 ;
DIG 4 ;
DUP ;
DUG 5 ;
CDR ;
CAR ;
EDIV ;
IF_NONE { PUSH string ""DIV by 0"" ; FAILWITH } {} ;
CAR ;
AMOUNT ;
PUSH mutez 1 ;
SWAP ;
EDIV ;
IF_NONE { PUSH string ""DIV by 0"" ; FAILWITH } {} ;
CAR ;
SWAP ;
DUP ;
DUG 2 ;
DIG 6 ;
DUP ;
DUG 7 ;
CDR ;
CDR ;
CAR ;
DIG 2 ;
DUP ;
DUG 3 ;
MUL ;
EDIV ;
IF_NONE { PUSH string ""DIV by 0"" ; FAILWITH } {} ;
CAR ;
DIG 2 ;
DIG 6 ;
DUP ;
DUG 7 ;
CAR ;
DIG 3 ;
MUL ;
EDIV ;
IF_NONE
{ PUSH string ""DIV by 0"" ; FAILWITH }
{ DUP ; CDR ; SWAP ; CAR ; PUSH nat 0 ; DIG 2 ; COMPARE ; EQ ; IF {} { PUSH nat 1 ; ADD } } ;
DIG 2 ;
SWAP ;
DUP ;
DUG 2 ;
COMPARE ;
GT ;
IF
{ DROP 5 ; PUSH nat 4 ; FAILWITH }
{ DUG 2 ;
DUP ;
DUG 3 ;
COMPARE ;
LT ;
IF
{ DROP 4 ; PUSH nat 5 ; FAILWITH }
{ DIG 3 ;
DUP ;
DUG 4 ;
CDR ;
CDR ;
CDR ;
DIG 2 ;
DUP ;
DUG 3 ;
DIG 5 ;
DUP ;
DUG 6 ;
CDR ;
CDR ;
CAR ;
ADD ;
PAIR ;
DIG 4 ;
DUP ;
DUG 5 ;
CDR ;
CAR ;
PAIR ;
DIG 4 ;
DUP ;
DUG 5 ;
CAR ;
PAIR ;
CDR ;
SWAP ;
DUP ;
DUG 2 ;
DIG 5 ;
DUP ;
DUG 6 ;
CAR ;
ADD ;
PAIR ;
DUP ;
CDR ;
CDR ;
AMOUNT ;
DIG 6 ;
CDR ;
CAR ;
ADD ;
PAIR ;
SWAP ;
CAR ;
PAIR ;
SWAP ;
SELF ;
ADDRESS ;
PAIR ;
SENDER ;
PAIR ;
SWAP ;
DUP ;
DUG 2 ;
SWAP ;
DUP ;
CDR ;
SWAP ;
CAR ;
SWAP ;
DUP ;
CDR ;
SWAP ;
CAR ;
DIG 3 ;
CDR ;
CDR ;
CDR ;
CAR ;
CONTRACT %transfer (pair address (pair address nat)) ;
IF_NONE { PUSH nat 0 ; FAILWITH } {} ;
PUSH mutez 0 ;
DIG 3 ;
DIG 3 ;
PAIR ;
DIG 3 ;
PAIR ;
TRANSFER_TOKENS ;
DIG 2 ;
INT ;
DIG 3 ;
PAIR ;
DIG 2 ;
DUP ;
DUG 3 ;
SWAP ;
DUP ;
CDR ;
SWAP ;
CAR ;
DIG 2 ;
CDR ;
CDR ;
CDR ;
CDR ;
CONTRACT %mintOrBurn (pair (int %quantity) (address %target)) ;
IF_NONE { PUSH nat 12 ; FAILWITH } {} ;
PUSH mutez 0 ;
DIG 2 ;
DIG 3 ;
PAIR ;
TRANSFER_TOKENS ;
DIG 2 ;
NIL operation ;
DIG 2 ;
CONS ;
DIG 2 ;
CONS ;
PAIR } } } }".
Definition ep_default : string := "{ DROP ; DUP ; CDR ; CDR ; AMOUNT ; DIG 2 ; DUP ; DUG 3 ; CDR ; CAR ; ADD ; PAIR ; SWAP ; CAR ; PAIR ; NIL operation ; PAIR }".
Definition ep_removeLiquidity : string := "{ DUP ;
CDR ;
SWAP ;
CAR ;
SWAP ;
DUP ;
CDR ;
SWAP ;
CAR ;
SWAP ;
DUP ;
CDR ;
SWAP ;
CAR ;
SWAP ;
DUP ;
CDR ;
SWAP ;
CAR ;
SWAP ;
NOW ;
COMPARE ;
GE ;
IF
{ DROP 5 ; PUSH nat 3 ; FAILWITH }
{ PUSH mutez 0 ;
AMOUNT ;
COMPARE ;
GT ;
IF
{ DROP 5 ; PUSH nat 10 ; FAILWITH }
{ DIG 4 ;
DUP ;
DUG 5 ;
CDR ;
CDR ;
CAR ;
PUSH mutez 1 ;
DIG 6 ;
DUP ;
DUG 7 ;
CDR ;
CAR ;
EDIV ;
IF_NONE { PUSH string ""DIV by 0"" ; FAILWITH } {} ;
CAR ;
DIG 4 ;
DUP ;
DUG 5 ;
MUL ;
EDIV ;
IF_NONE { PUSH string ""DIV by 0"" ; FAILWITH } {} ;
CAR ;
PUSH mutez 1 ;
SWAP ;
MUL ;
DIG 5 ;
DUP ;
DUG 6 ;
CDR ;
CDR ;
CAR ;
DIG 6 ;
DUP ;
DUG 7 ;
CAR ;
DIG 5 ;
DUP ;
DUG 6 ;
MUL ;
EDIV ;
IF_NONE { PUSH string ""DIV by 0"" ; FAILWITH } {} ;
CAR ;
DIG 3 ;
DIG 2 ;
DUP ;
DUG 3 ;
COMPARE ;
LT ;
IF
{ DROP 6 ; PUSH nat 11 ; FAILWITH }
{ DIG 2 ;
SWAP ;
DUP ;
DUG 2 ;
COMPARE ;
LT ;
IF
{ DROP 5 ; PUSH nat 13 ; FAILWITH }
{ DIG 2 ;
DUP ;
DUG 3 ;
DIG 5 ;
DUP ;
DUG 6 ;
CDR ;
CDR ;
CAR ;
SUB ;
ISNAT ;
IF_NONE { PUSH nat 14 ; FAILWITH } {} ;
SWAP ;
DUP ;
DUG 2 ;
DIG 6 ;
DUP ;
DUG 7 ;
CAR ;
SUB ;
ISNAT ;
IF_NONE { PUSH nat 15 ; FAILWITH } {} ;
DIG 4 ;
PUSH int 0 ;
SUB ;
SENDER ;
PAIR ;
DIG 6 ;
DUP ;
DUG 7 ;
SWAP ;
DUP ;
CDR ;
SWAP ;
CAR ;
DIG 2 ;
CDR ;
CDR ;
CDR ;
CDR ;
CONTRACT %mintOrBurn (pair (int %quantity) (address %target)) ;
IF_NONE { PUSH nat 12 ; FAILWITH } {} ;
PUSH mutez 0 ;
DIG 2 ;
DIG 3 ;
PAIR ;
TRANSFER_TOKENS ;
DIG 3 ;
DIG 5 ;
DUP ;
DUG 6 ;
PAIR ;
SELF ;
ADDRESS ;
PAIR ;
DIG 6 ;
DUP ;
DUG 7 ;
SWAP ;
DUP ;
CDR ;
SWAP ;
CAR ;
SWAP ;
DUP ;
CDR ;
SWAP ;
CAR ;
DIG 3 ;
CDR ;
CDR ;
CDR ;
CAR ;
CONTRACT %transfer (pair address (pair address nat)) ;
IF_NONE { PUSH nat 0 ; FAILWITH } {} ;
PUSH mutez 0 ;
DIG 3 ;
DIG 3 ;
PAIR ;
DIG 3 ;
PAIR ;
TRANSFER_TOKENS ;
DIG 4 ;
DUP ;
DUG 5 ;
DIG 6 ;
CONTRACT unit ;
IF_NONE { PUSH nat 9 ; FAILWITH } {} ;
SWAP ;
PUSH unit Unit ;
TRANSFER_TOKENS ;
DIG 6 ;
DUP ;
DUG 7 ;
CDR ;
CDR ;
DIG 6 ;
DIG 7 ;
DUP ;
DUG 8 ;
CDR ;
CAR ;
SUB ;
PAIR ;
DIG 6 ;
CAR ;
PAIR ;
DUP ;
CDR ;
CDR ;
CDR ;
DIG 6 ;
PAIR ;
SWAP ;
DUP ;
DUG 2 ;
CDR ;
CAR ;
PAIR ;
SWAP ;
CAR ;
PAIR ;
CDR ;
DIG 4 ;
PAIR ;
NIL operation ;
DIG 2 ;
CONS ;
DIG 2 ;
CONS ;
DIG 2 ;
CONS ;
PAIR } } } } }".
Definition ep_tokenToToken : string := "{ DUP ;
CDR ;
SWAP ;
CAR ;
SWAP ;
DUP ;
CDR ;
SWAP ;
CAR ;
SWAP ;
DUP ;
CDR ;
SWAP ;
CAR ;
SWAP ;
DUP ;
CDR ;
SWAP ;
CAR ;
DIG 4 ;
CONTRACT %xtzToToken (pair (address %to) (pair (nat %minTokensBought) (timestamp %deadline))) ;
IF_NONE { PUSH nat 31 ; FAILWITH } {} ;
PUSH mutez 0 ;
AMOUNT ;
COMPARE ;
GT ;
IF
{ DROP 6 ; PUSH nat 10 ; FAILWITH }
{ DIG 2 ;
DUP ;
DUG 3 ;
NOW ;
COMPARE ;
GE ;
IF
{ DROP 6 ; PUSH nat 3 ; FAILWITH }
{ PUSH nat 999 ;
DIG 2 ;
DUP ;
DUG 3 ;
MUL ;
PUSH nat 1000 ;
DIG 7 ;
DUP ;
DUG 8 ;
CAR ;
MUL ;
ADD ;
DIG 6 ;
DUP ;
DUG 7 ;
CDR ;
CAR ;
PUSH nat 999 ;
DIG 4 ;
DUP ;
DUG 5 ;
MUL ;
MUL ;
EDIV ;
IF_NONE { PUSH string ""DIV by 0"" ; FAILWITH } {} ;
CAR ;
PUSH nat 1000 ;
PUSH nat 999 ;
DIG 2 ;
DUP ;
DUG 3 ;
MUL ;
EDIV ;
IF_NONE { PUSH string ""DIV by 0"" ; FAILWITH } {} ;
CAR ;
DIG 7 ;
DUP ;
DUG 8 ;
CDR ;
DIG 4 ;
DUP ;
DUG 5 ;
DIG 9 ;
DUP ;
DUG 10 ;
CAR ;
ADD ;
PAIR ;
DUP ;
CDR ;
CDR ;
DIG 2 ;
DUP ;
DUG 3 ;
DIG 10 ;
CDR ;
CAR ;
SUB ;
PAIR ;
SWAP ;
CAR ;
PAIR ;
DIG 4 ;
SELF ;
ADDRESS ;
PAIR ;
SENDER ;
PAIR ;
SWAP ;
DUP ;
DUG 2 ;
SWAP ;
DUP ;
CDR ;
SWAP ;
CAR ;
SWAP ;
DUP ;
CDR ;
SWAP ;
CAR ;
DIG 3 ;
CDR ;
CDR ;
CDR ;
CAR ;
CONTRACT %transfer (pair address (pair address nat)) ;
IF_NONE { PUSH nat 0 ; FAILWITH } {} ;
PUSH mutez 0 ;
DIG 3 ;
DIG 3 ;
PAIR ;
DIG 3 ;
PAIR ;
TRANSFER_TOKENS ;
DIG 4 ;
DIG 3 ;
DUP ;
DUG 4 ;
DIG 6 ;
DIG 8 ;
PAIR ;
DIG 7 ;
PAIR ;
TRANSFER_TOKENS ;
DIG 3 ;
DIG 4 ;
SUB ;
PUSH address ""tz1Ke2h7sDdakHJQh8WX4Z372du1KChsksyU"" ;
CONTRACT unit ;
IF_NONE { PUSH nat 9 ; FAILWITH } {} ;
SWAP ;
PUSH unit Unit ;
TRANSFER_TOKENS ;
DIG 3 ;
NIL operation ;
DIG 2 ;
CONS ;
DIG 2 ;
CONS ;
DIG 2 ;
CONS ;
PAIR } } }".
Definition ep_tokenToXtz : string := "{ DUP ;
CDR ;
SWAP ;
CAR ;
SWAP ;
DUP ;
CDR ;
SWAP ;
CAR ;
SWAP ;
DUP ;
CDR ;
SWAP ;
CAR ;
SWAP ;
NOW ;
COMPARE ;
GE ;
IF
{ DROP 4 ; PUSH nat 3 ; FAILWITH }
{ PUSH mutez 0 ;
AMOUNT ;
COMPARE ;
GT ;
IF
{ DROP 4 ; PUSH nat 10 ; FAILWITH }
{ PUSH nat 999 ;
DIG 2 ;
DUP ;
DUG 3 ;
MUL ;
PUSH nat 1000 ;
DIG 5 ;
DUP ;
DUG 6 ;
CAR ;
MUL ;
ADD ;
PUSH mutez 1 ;
DIG 5 ;
DUP ;
DUG 6 ;
CDR ;
CAR ;
EDIV ;
IF_NONE { PUSH string ""DIV by 0"" ; FAILWITH } {} ;
CAR ;
PUSH nat 999 ;
DIG 4 ;
DUP ;
DUG 5 ;
MUL ;
MUL ;
EDIV ;
IF_NONE { PUSH string ""DIV by 0"" ; FAILWITH } {} ;
CAR ;
PUSH mutez 1 ;
SWAP ;
MUL ;
PUSH nat 1000 ;
PUSH nat 999 ;
DIG 2 ;
DUP ;
DUG 3 ;
MUL ;
EDIV ;
IF_NONE { PUSH string ""DIV by 0"" ; FAILWITH } {} ;
CAR ;
DIG 2 ;
SWAP ;
DUP ;
DUG 2 ;
COMPARE ;
LT ;
IF { DROP ; PUSH nat 8 ; FAILWITH } {} ;
DIG 2 ;
DUP ;
DUG 3 ;
SELF ;
ADDRESS ;
PAIR ;
SENDER ;
PAIR ;
DIG 5 ;
DUP ;
DUG 6 ;
SWAP ;
DUP ;
CDR ;
SWAP ;
CAR ;
SWAP ;
DUP ;
CDR ;
SWAP ;
CAR ;
DIG 3 ;
CDR ;
CDR ;
CDR ;
CAR ;
CONTRACT %transfer (pair address (pair address nat)) ;
IF_NONE { PUSH nat 0 ; FAILWITH } {} ;
PUSH mutez 0 ;
DIG 3 ;
DIG 3 ;
PAIR ;
DIG 3 ;
PAIR ;
TRANSFER_TOKENS ;
SWAP ;
DUP ;
DUG 2 ;
DIG 5 ;
CONTRACT unit ;
IF_NONE { PUSH nat 9 ; FAILWITH } {} ;
SWAP ;
PUSH unit Unit ;
TRANSFER_TOKENS ;
DIG 5 ;
DUP ;
DUG 6 ;
CDR ;
DIG 5 ;
DIG 6 ;
DUP ;
DUG 7 ;
CAR ;
ADD ;
PAIR ;
DUP ;
CDR ;
CDR ;
DIG 4 ;
DUP ;
DUG 5 ;
DIG 7 ;
CDR ;
CAR ;
SUB ;
PAIR ;
SWAP ;
CAR ;
PAIR ;
DIG 3 ;
DIG 4 ;
SUB ;
PUSH address ""tz1Ke2h7sDdakHJQh8WX4Z372du1KChsksyU"" ;
CONTRACT unit ;
IF_NONE { PUSH nat 9 ; FAILWITH } {} ;
SWAP ;
PUSH unit Unit ;
TRANSFER_TOKENS ;
SWAP ;
NIL operation ;
DIG 2 ;
CONS ;
DIG 2 ;
CONS ;
DIG 2 ;
CONS ;
PAIR } } }".
Definition ep_xtzToToken : string := "{ DUP ;
CDR ;
SWAP ;
CAR ;
SWAP ;
DUP ;
CDR ;
SWAP ;
CAR ;
SWAP ;
NOW ;
COMPARE ;
GE ;
IF
{ DROP 3 ; PUSH nat 3 ; FAILWITH }
{ PUSH mutez 1 ;
DIG 3 ;
DUP ;
DUG 4 ;
CDR ;
CAR ;
EDIV ;
IF_NONE { PUSH string ""DIV by 0"" ; FAILWITH } {} ;
CAR ;
AMOUNT ;
PUSH mutez 1 ;
SWAP ;
EDIV ;
IF_NONE { PUSH string ""DIV by 0"" ; FAILWITH } {} ;
CAR ;
PUSH nat 1000 ;
PUSH nat 999 ;
DIG 2 ;
DUP ;
DUG 3 ;
MUL ;
EDIV ;
IF_NONE { PUSH string ""DIV by 0"" ; FAILWITH } {} ;
CAR ;
DUP ;
DIG 2 ;
SUB ;
ABS ;
PUSH nat 999 ;
DIG 2 ;
DUP ;
DUG 3 ;
MUL ;
PUSH nat 1000 ;
DIG 4 ;
MUL ;
ADD ;
DIG 5 ;
DUP ;
DUG 6 ;
CAR ;
PUSH nat 999 ;
DIG 4 ;
DUP ;
DUG 5 ;
MUL ;
MUL ;
EDIV ;
IF_NONE { PUSH string ""DIV by 0"" ; FAILWITH } {} ;
CAR ;
DIG 3 ;
SWAP ;
DUP ;
DUG 2 ;
COMPARE ;
LT ;
IF { DROP ; PUSH nat 18 ; FAILWITH } {} ;
DUP ;
DIG 5 ;
DUP ;
DUG 6 ;
CAR ;
SUB ;
ISNAT ;
IF_NONE { PUSH nat 19 ; FAILWITH } {} ;
DIG 5 ;
DUP ;
DUG 6 ;
CDR ;
CDR ;
PUSH mutez 1 ;
DIG 5 ;
MUL ;
DIG 6 ;
DUP ;
DUG 7 ;
CDR ;
CAR ;
ADD ;
PAIR ;
DIG 5 ;
CAR ;
PAIR ;
CDR ;
SWAP ;
PAIR ;
SWAP ;
DIG 3 ;
PAIR ;
SELF ;
ADDRESS ;
PAIR ;
SWAP ;
DUP ;
DUG 2 ;
SWAP ;
DUP ;
CDR ;
SWAP ;
CAR ;
SWAP ;
DUP ;
CDR ;
SWAP ;
CAR ;
DIG 3 ;
CDR ;
CDR ;
CDR ;
CAR ;
CONTRACT %transfer (pair address (pair address nat)) ;
IF_NONE { PUSH nat 0 ; FAILWITH } {} ;
PUSH mutez 0 ;
DIG 3 ;
DIG 3 ;
PAIR ;
DIG 3 ;
PAIR ;
TRANSFER_TOKENS ;
PUSH mutez 1 ;
DIG 3 ;
MUL ;
PUSH address ""tz1Ke2h7sDdakHJQh8WX4Z372du1KChsksyU"" ;
CONTRACT unit ;
IF_NONE { PUSH nat 9 ; FAILWITH } {} ;
SWAP ;
PUSH unit Unit ;
TRANSFER_TOKENS ;
DIG 2 ;
NIL operation ;
DIG 2 ;
CONS ;
DIG 2 ;
CONS ;
PAIR } }".
Definition contract_s : string := "parameter (or
(or
(or
(pair %addLiquidity (address %owner)
(pair (nat %minLqtMinted)
(pair (nat %maxTokensDeposited) (timestamp %deadline))))
(unit %default))
(or
(pair %removeLiquidity (address %to)
(pair (nat %lqtBurned)
(pair (mutez %minXtzWithdrawn)
(pair (nat %minTokensWithdrawn)
(timestamp %deadline)))))
(pair %tokenToToken (address %outputDexterContract)
(pair (nat %minTokensBought)
(pair (address %to)
(pair (nat %tokensSold) (timestamp %deadline)))))))
(or
(pair %tokenToXtz (address %to)
(pair (nat %tokensSold)
(pair (mutez %minXtzBought) (timestamp %deadline))))
(pair %xtzToToken (address %to) (pair (nat %minTokensBought) (timestamp %deadline)))));
storage (pair (nat %tokenPool)
(pair (mutez %xtzPool)
(pair (nat %lqtTotal) (pair (address %tokenAddress) (address %lqtAddress)))));
code { DUP ;
CDR ;
SWAP ;
CAR ;
IF_LEFT
{ IF_LEFT
{ IF_LEFT " ++ ep_addLiquidity ++ " " ++ ep_default ++ " }
{ IF_LEFT " ++ ep_removeLiquidity ++ " " ++ ep_tokenToToken ++ " } }
{ IF_LEFT " ++ ep_tokenToXtz ++ " " ++ ep_xtzToToken ++ " } }".
