https://gitlab.com/nomadic-labs/mi-cho-coq
Tip revision: d7b21f4f74735ee5a48d9a8c09af765c38a30d44 authored by Guillaume Claret on 12 March 2021, 11:19:43 UTC
[mi-cho-coq] Replace String.string_dec by String.eqb
[mi-cho-coq] Replace String.string_dec by String.eqb
Tip revision: d7b21f4
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 ;
DIG 4 ;
DUP ;
DUG 5 ;
CDR ;
CDR ;
CDR ;
CAR ;
IF
{ DROP 5 ; PUSH nat 2 ; FAILWITH }
{ 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 ;
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 ;
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 ;
CDR ;
CAR ;
IF
{ DROP ; PUSH nat 2 ; FAILWITH }
{ 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 ;
DIG 5 ;
DUP ;
DUG 6 ;
CDR ;
CDR ;
CDR ;
CAR ;
IF
{ DROP 6 ; PUSH nat 2 ; FAILWITH }
{ 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 ;
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 ;
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_setBaker : string := "{ DUP ;
CDR ;
SWAP ;
CAR ;
DIG 2 ;
DUP ;
DUG 3 ;
CDR ;
CDR ;
CDR ;
CAR ;
IF
{ DROP 3 ; PUSH nat 2 ; FAILWITH }
{ PUSH mutez 0 ;
AMOUNT ;
COMPARE ;
GT ;
IF
{ DROP 3 ; PUSH nat 10 ; FAILWITH }
{ DIG 2 ;
DUP ;
DUG 3 ;
CDR ;
CDR ;
CDR ;
CDR ;
CDR ;
CAR ;
SENDER ;
COMPARE ;
NEQ ;
IF
{ DROP 3 ; PUSH nat 20 ; FAILWITH }
{ DIG 2 ;
DUP ;
DUG 3 ;
CDR ;
CDR ;
CDR ;
CDR ;
CAR ;
IF
{ DROP 3 ; PUSH nat 22 ; FAILWITH }
{ DIG 2 ;
DUP ;
DUG 3 ;
CDR ;
CDR ;
CDR ;
CDR ;
CDR ;
DIG 2 ;
PAIR ;
DIG 2 ;
DUP ;
DUG 3 ;
CDR ;
CDR ;
CDR ;
CAR ;
PAIR ;
DIG 2 ;
DUP ;
DUG 3 ;
CDR ;
CDR ;
CAR ;
PAIR ;
DIG 2 ;
DUP ;
DUG 3 ;
CDR ;
CAR ;
PAIR ;
DIG 2 ;
CAR ;
PAIR ;
NIL operation ;
DIG 2 ;
SET_DELEGATE ;
CONS ;
PAIR } } } } }".
Definition ep_setLqtAddress : string := "{ SWAP ;
DUP ;
DUG 2 ;
CDR ;
CDR ;
CDR ;
CAR ;
IF
{ DROP 2 ; PUSH nat 2 ; FAILWITH }
{ PUSH mutez 0 ;
AMOUNT ;
COMPARE ;
GT ;
IF
{ DROP 2 ; PUSH nat 10 ; FAILWITH }
{ SWAP ;
DUP ;
DUG 2 ;
CDR ;
CDR ;
CDR ;
CDR ;
CDR ;
CAR ;
SENDER ;
COMPARE ;
NEQ ;
IF
{ DROP 2 ; PUSH nat 23 ; FAILWITH }
{ PUSH address ""tz1Ke2h7sDdakHJQh8WX4Z372du1KChsksyU"" ;
DIG 2 ;
DUP ;
DUG 3 ;
CDR ;
CDR ;
CDR ;
CDR ;
CDR ;
CDR ;
CDR ;
COMPARE ;
NEQ ;
IF
{ DROP 2 ; PUSH nat 24 ; FAILWITH }
{ SWAP ;
DUP ;
DUG 2 ;
CDR ;
CDR ;
CDR ;
CDR ;
CDR ;
CDR ;
CAR ;
PAIR ;
SWAP ;
DUP ;
DUG 2 ;
CDR ;
CDR ;
CDR ;
CDR ;
CDR ;
CAR ;
PAIR ;
SWAP ;
DUP ;
DUG 2 ;
CDR ;
CDR ;
CDR ;
CDR ;
CAR ;
PAIR ;
SWAP ;
DUP ;
DUG 2 ;
CDR ;
CDR ;
CDR ;
CAR ;
PAIR ;
SWAP ;
DUP ;
DUG 2 ;
CDR ;
CDR ;
CAR ;
PAIR ;
SWAP ;
DUP ;
DUG 2 ;
CDR ;
CAR ;
PAIR ;
SWAP ;
CAR ;
PAIR ;
NIL operation ;
PAIR } } } } }".
Definition ep_setManager : string := "{ SWAP ;
DUP ;
DUG 2 ;
CDR ;
CDR ;
CDR ;
CAR ;
IF
{ DROP 2 ; PUSH nat 2 ; FAILWITH }
{ PUSH mutez 0 ;
AMOUNT ;
COMPARE ;
GT ;
IF
{ DROP 2 ; PUSH nat 10 ; FAILWITH }
{ SWAP ;
DUP ;
DUG 2 ;
CDR ;
CDR ;
CDR ;
CDR ;
CDR ;
CAR ;
SENDER ;
COMPARE ;
NEQ ;
IF
{ DROP 2 ; PUSH nat 21 ; FAILWITH }
{ SWAP ;
DUP ;
DUG 2 ;
CDR ;
CDR ;
CDR ;
CDR ;
CDR ;
CDR ;
SWAP ;
PAIR ;
SWAP ;
DUP ;
DUG 2 ;
CDR ;
CDR ;
CDR ;
CDR ;
CAR ;
PAIR ;
SWAP ;
DUP ;
DUG 2 ;
CDR ;
CDR ;
CDR ;
CAR ;
PAIR ;
SWAP ;
DUP ;
DUG 2 ;
CDR ;
CDR ;
CAR ;
PAIR ;
SWAP ;
DUP ;
DUG 2 ;
CDR ;
CAR ;
PAIR ;
SWAP ;
CAR ;
PAIR ;
NIL operation ;
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 } {} ;
DIG 5 ;
DUP ;
DUG 6 ;
CDR ;
CDR ;
CDR ;
CAR ;
IF
{ DROP 6 ; PUSH nat 2 ; 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 997 ;
DIG 2 ;
DUP ;
DUG 3 ;
MUL ;
PUSH nat 1000 ;
DIG 7 ;
DUP ;
DUG 8 ;
CAR ;
MUL ;
ADD ;
PUSH mutez 1 ;
DIG 7 ;
DUP ;
DUG 8 ;
CDR ;
CAR ;
EDIV ;
IF_NONE { PUSH string ""DIV by 0"" ; FAILWITH } {} ;
CAR ;
PUSH nat 997 ;
DIG 4 ;
DUP ;
DUG 5 ;
MUL ;
MUL ;
EDIV ;
IF_NONE { PUSH string ""DIV by 0"" ; FAILWITH } {} ;
CAR ;
PUSH mutez 1 ;
SWAP ;
MUL ;
DIG 6 ;
DUP ;
DUG 7 ;
CDR ;
DIG 3 ;
DUP ;
DUG 4 ;
DIG 8 ;
DUP ;
DUG 9 ;
CAR ;
ADD ;
PAIR ;
DUP ;
CDR ;
CDR ;
DIG 2 ;
DUP ;
DUG 3 ;
DIG 9 ;
CDR ;
CAR ;
SUB ;
PAIR ;
SWAP ;
CAR ;
PAIR ;
DIG 3 ;
SELF ;
ADDRESS ;
PAIR ;
SENDER ;
PAIR ;
SWAP ;
DUP ;
DUG 2 ;
SWAP ;
DUP ;
CDR ;
SWAP ;
CAR ;
SWAP ;
DUP ;
CDR ;
SWAP ;
CAR ;
DIG 3 ;
CDR ;
CDR ;
CDR ;
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 3 ;
DIG 3 ;
DIG 4 ;
DIG 6 ;
PAIR ;
DIG 5 ;
PAIR ;
TRANSFER_TOKENS ;
DIG 2 ;
NIL operation ;
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 ;
DIG 4 ;
DUP ;
DUG 5 ;
CDR ;
CDR ;
CDR ;
CAR ;
IF
{ DROP 5 ; PUSH nat 2 ; FAILWITH }
{ 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 997 ;
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 997 ;
DIG 4 ;
DUP ;
DUG 5 ;
MUL ;
MUL ;
EDIV ;
IF_NONE { PUSH string ""DIV by 0"" ; FAILWITH } {} ;
CAR ;
PUSH mutez 1 ;
SWAP ;
MUL ;
DUP ;
DUG 2 ;
COMPARE ;
LT ;
IF { DROP ; PUSH nat 8 ; FAILWITH } {} ;
SWAP ;
DUP ;
DUG 2 ;
SELF ;
ADDRESS ;
PAIR ;
SENDER ;
PAIR ;
DIG 4 ;
DUP ;
DUG 5 ;
SWAP ;
DUP ;
CDR ;
SWAP ;
CAR ;
SWAP ;
DUP ;
CDR ;
SWAP ;
CAR ;
DIG 3 ;
CDR ;
CDR ;
CDR ;
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 4 ;
CONTRACT unit ;
IF_NONE { PUSH nat 9 ; FAILWITH } {} ;
SWAP ;
PUSH unit Unit ;
TRANSFER_TOKENS ;
DIG 4 ;
DUP ;
DUG 5 ;
CDR ;
DIG 4 ;
DIG 5 ;
DUP ;
DUG 6 ;
CAR ;
ADD ;
PAIR ;
DUP ;
CDR ;
CDR ;
DIG 4 ;
DIG 5 ;
CDR ;
CAR ;
SUB ;
PAIR ;
SWAP ;
CAR ;
PAIR ;
NIL operation ;
DIG 2 ;
CONS ;
DIG 2 ;
CONS ;
PAIR } } } }".
Definition ep_updateTokenPool : string := "{ DROP ;
SOURCE ;
SENDER ;
COMPARE ;
NEQ ;
IF
{ DROP ; PUSH nat 25 ; FAILWITH }
{ PUSH mutez 0 ;
AMOUNT ;
COMPARE ;
GT ;
IF
{ DROP ; PUSH nat 10 ; FAILWITH }
{ DUP ;
CDR ;
CDR ;
CDR ;
CAR ;
IF
{ DROP ; PUSH nat 33 ; FAILWITH }
{ SELF %updateTokenPoolInternal ;
SWAP ;
DUP ;
DUG 2 ;
CDR ;
CDR ;
CDR ;
CDR ;
CDR ;
CDR ;
CAR ;
CONTRACT %getBalance (pair address (contract nat)) ;
IF_NONE { PUSH nat 28 ; FAILWITH } {} ;
PUSH mutez 0 ;
DIG 2 ;
SELF ;
ADDRESS ;
PAIR ;
TRANSFER_TOKENS ;
SWAP ;
DUP ;
DUG 2 ;
CDR ;
CDR ;
CDR ;
CDR ;
PUSH bool True ;
PAIR ;
DIG 2 ;
DUP ;
DUG 3 ;
CDR ;
CDR ;
CAR ;
PAIR ;
DIG 2 ;
DUP ;
DUG 3 ;
CDR ;
CAR ;
PAIR ;
DIG 2 ;
CAR ;
PAIR ;
NIL operation ;
DIG 2 ;
CONS ;
PAIR } } } }".
Definition ep_updateTokenPoolInternal : string := "{ SWAP ;
DUP ;
DUG 2 ;
CDR ;
CDR ;
CDR ;
CDR ;
CDR ;
CDR ;
CAR ;
SENDER ;
COMPARE ;
NEQ ;
DIG 2 ;
DUP ;
DUG 3 ;
CDR ;
CDR ;
CDR ;
CAR ;
NOT ;
OR ;
IF
{ DROP 2 ; PUSH nat 29 ; FAILWITH }
{ PUSH mutez 0 ;
AMOUNT ;
COMPARE ;
GT ;
IF
{ DROP 2 ; PUSH nat 10 ; FAILWITH }
{ SWAP ;
CDR ;
SWAP ;
PAIR ;
DUP ;
CDR ;
CDR ;
CDR ;
CDR ;
PUSH bool False ;
PAIR ;
SWAP ;
DUP ;
DUG 2 ;
CDR ;
CDR ;
CAR ;
PAIR ;
SWAP ;
DUP ;
DUG 2 ;
CDR ;
CAR ;
PAIR ;
SWAP ;
CAR ;
PAIR ;
NIL operation ;
PAIR } } }".
Definition ep_xtzToToken : string := "{ DUP ;
CDR ;
SWAP ;
CAR ;
SWAP ;
DUP ;
CDR ;
SWAP ;
CAR ;
DIG 3 ;
DUP ;
DUG 4 ;
CDR ;
CDR ;
CDR ;
CAR ;
IF
{ DROP 4 ; PUSH nat 2 ; FAILWITH }
{ 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 997 ;
SWAP ;
DUP ;
DUG 2 ;
MUL ;
PUSH nat 1000 ;
DIG 3 ;
MUL ;
ADD ;
DIG 4 ;
DUP ;
DUG 5 ;
CAR ;
PUSH nat 997 ;
DIG 3 ;
MUL ;
MUL ;
EDIV ;
IF_NONE { PUSH string ""DIV by 0"" ; FAILWITH } {} ;
CAR ;
DUP ;
DUG 2 ;
COMPARE ;
LT ;
IF { DROP ; PUSH nat 18 ; FAILWITH } {} ;
DUP ;
DIG 3 ;
DUP ;
DUG 4 ;
CAR ;
SUB ;
ISNAT ;
IF_NONE { PUSH nat 19 ; FAILWITH } {} ;
DIG 3 ;
DUP ;
DUG 4 ;
CDR ;
CDR ;
AMOUNT ;
DIG 5 ;
DUP ;
DUG 6 ;
CDR ;
CAR ;
ADD ;
PAIR ;
DIG 4 ;
CAR ;
PAIR ;
CDR ;
SWAP ;
PAIR ;
SWAP ;
DIG 2 ;
PAIR ;
SELF ;
ADDRESS ;
PAIR ;
SWAP ;
DUP ;
DUG 2 ;
SWAP ;
DUP ;
CDR ;
SWAP ;
CAR ;
SWAP ;
DUP ;
CDR ;
SWAP ;
CAR ;
DIG 3 ;
CDR ;
CDR ;
CDR ;
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 ;
NIL operation ;
DIG 2 ;
CONS ;
PAIR } } }".
Definition contract_s : string := "parameter (or
(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 %setBaker (option %baker key_hash) (bool %freezeBaker))))
(or (or (address %setLqtAddress) (address %setManager))
(or
(pair %tokenToToken (address %outputDexterContract)
(pair (nat %minTokensBought)
(pair (address %to)
(pair (nat %tokensSold) (timestamp %deadline)))))
(pair %tokenToXtz (address %to)
(pair (nat %tokensSold)
(pair (mutez %minXtzBought) (timestamp %deadline)))))))
(or (or (unit %updateTokenPool) (nat %updateTokenPoolInternal))
(pair %xtzToToken (address %to) (pair (nat %minTokensBought) (timestamp %deadline)))));
storage (pair (nat %tokenPool)
(pair (mutez %xtzPool)
(pair (nat %lqtTotal)
(pair (bool %selfIsUpdatingTokenPool)
(pair (bool %freezeBaker)
(pair (address %manager)
(pair (address %tokenAddress) (address %lqtAddress))))))));
code { DUP ;
CDR ;
SWAP ;
CAR ;
IF_LEFT
{ IF_LEFT
{ IF_LEFT
{ IF_LEFT " ++ ep_addLiquidity ++ " " ++ ep_default ++ " }
{ IF_LEFT " ++ ep_removeLiquidity ++ " " ++ ep_setBaker ++ " } }
{ IF_LEFT
{ IF_LEFT " ++ ep_setLqtAddress ++ " " ++ ep_setManager ++ " }
{ IF_LEFT " ++ ep_tokenToToken ++ " " ++ ep_tokenToXtz ++ " } } }
{ IF_LEFT
{ IF_LEFT " ++ ep_updateTokenPool ++ " " ++ ep_updateTokenPoolInternal ++ " }
" ++ ep_xtzToToken ++ " } }".
