https://gitlab.com/nomadic-labs/mi-cho-coq
Raw File
Tip revision: 401e2f7c5755df696ced7a857bd88db7f223458c authored by Arvid Jakobsson on 12 February 2021, 19:32:23 UTC
[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 }".

back to top