https://gitlab.com/nomadic-labs/mi-cho-coq
Tip revision: 401e2f7c5755df696ced7a857bd88db7f223458c authored by Arvid Jakobsson on 12 February 2021, 19:32:23 UTC
[ci] split out linting
[ci] split out linting
Tip revision: 401e2f7
dexter_addlqt_string.v
Require Import String.
Definition ep_addLiquidity1_header : string := "{ DIP { DUP ; CDR ; CAR ; CAR ; IF { PUSH string ""selfIsUpdatingToken must be false."" ; FAILWITH } {} } ;
DUP ;
CDR ;
CDR ;
NOW ;
COMPARE ;
LT ;
IF {} { PUSH string ""NOW is greater than deadline."" ; FAILWITH } ;
DUP ;
CDR ;
CAR ;
PUSH nat 0 ;
COMPARE ;
LT ;
IF {} { PUSH string ""maxTokensDeposited must be greater than zero."" ; FAILWITH } ;
DUP ;
CAR ;
CDR ;
PUSH nat 0 ;
COMPARE ;
LT ;
IF {} { PUSH string ""minLqtMinted must be greater than zero."" ; FAILWITH } ;
PUSH mutez 0 ;
AMOUNT ;
COMPARE ;
GT ;
IF {} { PUSH string ""Amount must be greater than zero."" ; FAILWITH } ;
DIP { DUP } ;
SWAP ;
CDR ;
CAR ;
CDR ;
CDR ;
INT ;
EQ } ".
Definition ep_addLiquidity2_no_lqt : string := "
{ AMOUNT ;
PUSH mutez 1000000 ;
COMPARE ;
LE ;
IF
{}
{ PUSH string ""The initial liquidity amount must be greater than or equal to 1 XTZ."" ;
FAILWITH } ;
SWAP ;
AMOUNT ;
DIP { PUSH mutez 1 } ;
EDIV ;
IF_NONE { PUSH string """" ; FAILWITH } { CAR } ;
DUP ;
DIP { DIP { DUP ; CDR } ;
DIP { DUP ; DIP { CDR } ; CAR } ;
DIP { DUP ; DIP { CAR } ; CDR } ;
DIP { DUP ; DIP { CAR } ; CDR } ;
SWAP ;
DROP ;
SWAP ;
PAIR ;
SWAP ;
PAIR ;
PAIR ;
DIP { DUP ; DIP { CAR } ; CDR } ;
SWAP ;
DROP ;
SWAP ;
PAIR } ;
SWAP ;
DIP 2 { DUP } ;
DIG 2 ;
CAR ;
CAR ;
DIP { DUP ; CAR } ;
GET ;
IF_NONE { EMPTY_MAP address nat ; PUSH nat 0 ; PAIR } {} ;
DIG 2 ;
DIP { DUP ; DIP { CDR } ; CAR } ;
SWAP ;
DROP ;
PAIR ;
DIP { DUP ; CAR } ;
SOME ;
DIP 3 { DUP } ;
DIG 3 ;
CAR ;
CAR ;
UPDATE ;
DIP { DUP ; DIP { CDR } ; CAR } ;
SWAP ;
DROP ;
PAIR ;
DUP ;
CDR ;
CDR ;
CDR ;
CDR ;
AMOUNT ;
ADD ;
DIP { DUP ; CDR } ;
DIP { DUP ; DIP { CAR } ; CDR } ;
DIP { DUP ; DIP { CAR } ; CDR } ;
DIP { DUP ; DIP { CAR } ; CDR } ;
SWAP ;
DROP ;
SWAP ;
PAIR ;
SWAP ;
PAIR ;
SWAP ;
PAIR ;
DIP { DUP ; DIP { CAR } ; CDR } ;
SWAP ;
DROP ;
SWAP ;
PAIR ;
DUP ;
CDR ;
CDR ;
CDR ;
CAR ;
DIP 2 { DUP } ;
DIG 2 ;
CDR ;
CAR ;
ADD ;
DIP { DUP ; CDR } ;
DIP { DUP ; DIP { CAR } ; CDR } ;
DIP { DUP ; DIP { CAR } ; CDR } ;
DIP { DUP ; DIP { CDR } ; CAR } ;
SWAP ;
DROP ;
PAIR ;
SWAP ;
PAIR ;
SWAP ;
PAIR ;
DIP { DUP ; DIP { CAR } ; CDR } ;
SWAP ;
DROP ;
SWAP ;
PAIR ;
DIP { DUP ; CDR ; CAR ; DIP { CAR ; CAR } } ;
DUP ;
CDR ;
CDR ;
CAR ;
CDR ;
CONTRACT %transfer (pair address (pair address nat)) ;
IF_NONE { FAILWITH } {} ;
PUSH mutez 0 ;
DIG 3 ;
SELF ;
ADDRESS ;
DIG 5 ;
DIP { PAIR } ;
PAIR ;
TRANSFER_TOKENS ;
DIP { NIL operation } ;
CONS ;
PAIR }".
Definition ep_addLiquidity3_some_lqt : string := "
{ DIP { DUP } ;
SWAP ;
CDR ;
CDR ;
CDR ;
CDR ;
DIP { PUSH mutez 1 } ;
EDIV ;
IF_NONE { PUSH string """" ; FAILWITH } { CAR } ;
AMOUNT ;
DIP { PUSH mutez 1 } ;
EDIV ;
IF_NONE { PUSH string """" ; FAILWITH } { CAR } ;
DUP ;
DIP 4 { DUP } ;
DIG 4 ;
CDR ;
CDR ;
CDR ;
CAR ;
MUL ;
DIP 2 { DUP } ;
DIG 2 ;
SWAP ;
EDIV ;
IF_NONE
{ PUSH string ""divByZero."" ; FAILWITH }
{ DUP ; CAR ; DIP { CDR } ; SWAP ; INT ; EQ ; IF {} { PUSH nat 1 ; ADD } } ;
DUP ;
PUSH nat 0 ;
COMPARE ;
LT ;
IF {} { PUSH string ""tokensDeposited is zero."" ; FAILWITH } ;
SWAP ;
DIP 4 { DUP } ;
DIG 4 ;
CDR ;
CAR ;
CDR ;
CDR ;
MUL ;
DIP { SWAP } ;
EDIV ;
IF_NONE { FAILWITH } { CAR } ;
DIP 2 { DUP } ;
DIG 2 ;
CAR ;
CDR ;
DIP { DUP } ;
COMPARE ;
LE ;
IF {} { PUSH string ""lqtMinted must be greater than or equal to minLqtMinted."" ; FAILWITH } ;
DIP { DIP { DUP } ;
SWAP ;
CDR ;
CAR ;
DIP { DUP } ;
COMPARE ;
GE ;
IF {} { PUSH string ""tokensDeposited is greater than maxTokensDeposited."" ; FAILWITH } } ;
DIP 3 { DUP } ;
DIG 3 ;
DIP 3 { DUP } ;
DIG 3 ;
CAR ;
CAR ;
DIP { CAR } ;
GET ;
IF_NONE { EMPTY_MAP address nat ; PUSH nat 0 ; PAIR } {} ;
DUP ;
CAR ;
DIP 2 { DUP } ;
DIG 2 ;
ADD ;
DIP { DUP ; DIP { CDR } ; CAR } ;
SWAP ;
DROP ;
PAIR ;
SOME ;
DIP 3 { DUP } ;
DIG 3 ;
CAR ;
CAR ;
DIP { DIP { DIG 3 ; DUP ; CAR } } ;
UPDATE ;
DIP { DUP ; DIP { CDR } ; CAR } ;
SWAP ;
DROP ;
PAIR ;
DUP ;
CDR ;
CAR ;
CDR ;
CDR ;
DIG 2 ;
ADD ;
DIP { DUP ; CDR } ;
DIP { DUP ; DIP { CDR } ; CAR } ;
DIP { DUP ; DIP { CAR } ; CDR } ;
DIP { DUP ; DIP { CAR } ; CDR } ;
SWAP ;
DROP ;
SWAP ;
PAIR ;
SWAP ;
PAIR ;
PAIR ;
DIP { DUP ; DIP { CAR } ; CDR } ;
SWAP ;
DROP ;
SWAP ;
PAIR ;
DUP ;
CDR ;
CDR ;
CDR ;
CDR ;
AMOUNT ;
ADD ;
DIP { DUP ; CDR } ;
DIP { DUP ; DIP { CAR } ; CDR } ;
DIP { DUP ; DIP { CAR } ; CDR } ;
DIP { DUP ; DIP { CAR } ; CDR } ;
SWAP ;
DROP ;
SWAP ;
PAIR ;
SWAP ;
PAIR ;
SWAP ;
PAIR ;
DIP { DUP ; DIP { CAR } ; CDR } ;
SWAP ;
DROP ;
SWAP ;
PAIR ;
DUP ;
CDR ;
CDR ;
CDR ;
CAR ;
DIP 2 { DUP } ;
DIG 2 ;
ADD ;
DIP { DUP ; CDR } ;
DIP { DUP ; DIP { CAR } ; CDR } ;
DIP { DUP ; DIP { CAR } ; CDR } ;
DIP { DUP ; DIP { CDR } ; CAR } ;
SWAP ;
DROP ;
PAIR ;
SWAP ;
PAIR ;
SWAP ;
PAIR ;
DIP { DUP ; DIP { CAR } ; CDR } ;
SWAP ;
DROP ;
SWAP ;
PAIR ;
DIP { DIP { CAR ; CAR } } ;
DUP ;
CDR ;
CDR ;
CAR ;
CDR ;
CONTRACT %transfer (pair address (pair address nat)) ;
IF_NONE { FAILWITH } {} ;
PUSH mutez 0 ;
DIG 3 ;
SELF ;
ADDRESS ;
DIG 5 ;
DIP { PAIR } ;
PAIR ;
TRANSFER_TOKENS ;
DIP { NIL operation } ;
CONS ;
PAIR }".