https://gitlab.com/nomadic-labs/mi-cho-coq
Raw File
Tip revision: 08edb74856d05a9ecdbc5dc5e40903aee308bd1b authored by Arvid Jakobsson on 28 September 2020, 21:46:43 UTC
[dexter] update proof for exchange entrypoints
Tip revision: 08edb74
dexter_string.v
Require Import String.

Definition ep_approve : string := "{ DIP { DUP ; CDR ; CAR ; CAR ; IF { PUSH string ""selfIsUpdatingToken must be false."" ; FAILWITH } {} } ;
  PUSH mutez 0 ;
  AMOUNT ;
  COMPARE ;
  EQ ;
  IF {} { PUSH string ""Amount must be zero."" ; FAILWITH } ;
  DIP { DUP } ;
  SWAP ;
  CAR ;
  SENDER ;
  GET ;
  IF_NONE { EMPTY_MAP address nat ; PUSH nat 0 ; PAIR } {} ;
  DUP ;
  CDR ;
  DIP 2 { DUP } ;
  DIG 2 ;
  CAR ;
  GET ;
  IF_NONE { PUSH nat 0 } {} ;
  DIP 2 { DUP } ;
  DIG 2 ;
  CDR ;
  CDR ;
  COMPARE ;
  EQ ;
  IF
    {}
    { PUSH string ""The current allowance parameter must equal the sender's current allowance for the owner."" ;
      FAILWITH } ;
  DUP ;
  CDR ;
  DIG 2 ;
  DUP ;
  CAR ;
  DIP { CDR ; CAR ; SOME } ;
  UPDATE ;
  DIP { DUP ; DIP { CAR } ; CDR } ;
  SWAP ;
  DROP ;
  SWAP ;
  PAIR ;
  DIP { DUP ; CAR } ;
  SOME ;
  SENDER ;
  UPDATE ;
  DIP { DUP ; DIP { CDR } ; CAR } ;
  SWAP ;
  DROP ;
  PAIR ;
  NIL operation ;
  PAIR }".

Definition ep_addLiquidity : 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 ;
  IF
    { 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 }
    { 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 } }".

Definition ep_removeLiquidity : string := "{ DIP { DUP ; CDR ; CAR ; CAR ; IF { PUSH string ""selfIsUpdatingToken must be false."" ; FAILWITH } {} } ;
  DUP ;
  CDR ;
  CDR ;
  CDR ;
  NOW ;
  COMPARE ;
  LT ;
  IF {} { PUSH string ""NOW is greater than deadline."" ; FAILWITH } ;
  PUSH mutez 0 ;
  AMOUNT ;
  COMPARE ;
  EQ ;
  IF {} { PUSH string ""Amount must be zero."" ; FAILWITH } ;
  DUP ;
  CDR ;
  CAR ;
  PUSH mutez 0 ;
  COMPARE ;
  LT ;
  IF {} { PUSH string ""minXtzWithdrawn must be greater than zero."" ; FAILWITH } ;
  DUP ;
  CDR ;
  CDR ;
  CAR ;
  PUSH nat 0 ;
  COMPARE ;
  LT ;
  IF {} { PUSH string ""minTokensWithdrawn must be greater than zero."" ; FAILWITH } ;
  DUP ;
  CAR ;
  CDR ;
  CDR ;
  PUSH nat 0 ;
  COMPARE ;
  LT ;
  IF {} { PUSH string ""lqtBurned must be greater than zero."" ; FAILWITH } ;
  DUP ;
  CAR ;
  CAR ;
  DIP { DIP { DUP } ; SWAP ; CAR } ;
  GET ;
  IF_NONE { PUSH string ""owner has no liquidity."" ; FAILWITH } {} ;
  SWAP ;
  DUP ;
  CAR ;
  CDR ;
  CDR ;
  DIP 2 { DUP } ;
  DIG 2 ;
  CAR ;
  COMPARE ;
  GE ;
  IF {} { PUSH string ""lqtBurned is greater than owner's balance."" ; FAILWITH } ;
  DUP ;
  CAR ;
  CAR ;
  SENDER ;
  COMPARE ;
  EQ ;
  IF
    { SWAP ; CAR }
    { SWAP ;
      DUP ;
      CDR ;
      SENDER ;
      GET ;
      IF_NONE { PUSH string ""sender has no approval balance."" ; FAILWITH } {} ;
      DIP { SWAP ; DUP ; CAR ; CDR ; CDR ; DIP { PUSH int 0 } } ;
      SUB ;
      DUP ;
      DIP { COMPARE ;
            GE ;
            IF {} { PUSH string ""sender approval balance is less than LQT burned."" ; FAILWITH } } ;
      ABS ;
      SOME ;
      DIG 2 ;
      DUP ;
      CDR ;
      DIG 2 ;
      SENDER ;
      UPDATE ;
      DIP { DUP ; DIP { CAR } ; CDR } ;
      SWAP ;
      DROP ;
      SWAP ;
      PAIR ;
      DUP ;
      CAR ;
      DIP { SOME ;
            DUG 1 ;
            DUP ;
            CAR ;
            CAR ;
            SWAP ;
            DIP { DIP { DIP { DUP ; CAR } } ; UPDATE ; DIP { DUP ; DIP { CDR } ; CAR } ; SWAP ; DROP ; PAIR } } } ;
  DIP { DUP } ;
  SWAP ;
  CAR ;
  CDR ;
  CDR ;
  DIP 3 { DUP } ;
  DIG 3 ;
  CDR ;
  CDR ;
  CDR ;
  CDR ;
  DIP { PUSH mutez 1 } ;
  EDIV ;
  IF_NONE { PUSH string """" ; FAILWITH } { CAR } ;
  MUL ;
  DIP { DIP 2 { DUP } ; DIG 2 ; CDR ; CAR ; CDR ; CDR } ;
  EDIV ;
  IF_NONE { PUSH string ""divByZero."" ; FAILWITH } { CAR } ;
  PUSH mutez 1 ;
  MUL ;
  DUP ;
  DIP 3 { DUP } ;
  DIG 3 ;
  CDR ;
  CAR ;
  COMPARE ;
  LE ;
  IF {} { PUSH string ""xtzWithdrawn is less than minXtzWithdrawn."" ; FAILWITH } ;
  DIP 2 { DUP } ;
  DIG 2 ;
  CAR ;
  CDR ;
  CDR ;
  DIP { DIP 3 { DUP } ; DIG 3 ; DUP ; CDR ; CAR ; CDR ; CDR ; SWAP ; CDR ; CDR ; CDR ; CAR } ;
  MUL ;
  EDIV ;
  IF_NONE { PUSH string ""divByZero."" ; FAILWITH } { CAR } ;
  DUP ;
  DIP 4 { DUP } ;
  DIG 4 ;
  CDR ;
  CDR ;
  CAR ;
  COMPARE ;
  LE ;
  IF {} { PUSH string ""tokensWithdrawn is less than minTokensWithdrawn."" ; FAILWITH } ;
  DIP 3 { DUP } ;
  DIG 3 ;
  CAR ;
  CDR ;
  CDR ;
  DIG 3 ;
  SUB ;
  DUP ;
  PUSH int 0 ;
  COMPARE ;
  LE ;
  IF { ABS } { PUSH string """" ; FAILWITH } ;
  DIG 4 ;
  DUP ;
  DIP 5 { DUP } ;
  DIG 5 ;
  CAR ;
  CAR ;
  DIP { 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 5 { DUP } ;
  DIG 5 ;
  CAR ;
  CAR ;
  UPDATE ;
  DIP { DUP ; DIP { CDR } ; CAR } ;
  SWAP ;
  DROP ;
  PAIR ;
  DUP ;
  CDR ;
  CAR ;
  CDR ;
  CDR ;
  DIP 4 { DUP } ;
  DIG 4 ;
  CAR ;
  CDR ;
  CDR ;
  SWAP ;
  SUB ;
  DUP ;
  PUSH int 0 ;
  COMPARE ;
  LE ;
  IF { ABS } { PUSH string """" ; FAILWITH } ;
  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 ;
  CAR ;
  DIP 2 { DUP } ;
  DIG 2 ;
  SWAP ;
  SUB ;
  DUP ;
  PUSH int 0 ;
  COMPARE ;
  LE ;
  IF { ABS } { PUSH string """" ; FAILWITH } ;
  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 ;
  DUP ;
  CDR ;
  CDR ;
  CDR ;
  CDR ;
  DIP 3 { DUP } ;
  DIG 3 ;
  SWAP ;
  SUB ;
  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 ;
  DIP 3 { DUP } ;
  DIG 3 ;
  CAR ;
  CDR ;
  CAR ;
  CONTRACT unit ;
  IF_NONE { FAILWITH } {} ;
  DIG 3 ;
  UNIT ;
  TRANSFER_TOKENS ;
  DIP { DIP { DIP { CAR ; CDR ; CAR } } ;
        DUP ;
        CDR ;
        CDR ;
        CAR ;
        CDR ;
        CONTRACT %transfer (pair address (pair address nat)) ;
        IF_NONE { FAILWITH } {} ;
        PUSH mutez 0 ;
        DIG 3 ;
        DIG 4 ;
        PAIR ;
        SELF ;
        ADDRESS ;
        PAIR ;
        TRANSFER_TOKENS } ;
  NIL operation ;
  SWAP ;
  CONS ;
  SWAP ;
  CONS ;
  PAIR }".

Definition ep_xtzToToken : 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 } ;
  PUSH mutez 0 ;
  AMOUNT ;
  COMPARE ;
  GT ;
  IF {} { PUSH string ""Amount must be greater than zero."" ; FAILWITH } ;
  DUP ;
  CDR ;
  CAR ;
  PUSH nat 0 ;
  COMPARE ;
  LT ;
  IF {} { PUSH string ""minTokensBought must be greater than zero."" ; FAILWITH } ;
  DIP { DUP ;
        CDR ;
        CDR ;
        CDR ;
        CDR ;
        PUSH mutez 0 ;
        COMPARE ;
        LT ;
        IF {} { PUSH string ""xtzPool must be greater than zero."" ; FAILWITH } } ;
  DIP { DUP ;
        CDR ;
        CDR ;
        CDR ;
        CAR ;
        PUSH nat 0 ;
        COMPARE ;
        LT ;
        IF {} { PUSH string ""tokenPool must be greater than zero"" ; FAILWITH } } ;
  DIP { DUP } ;
  SWAP ;
  CDR ;
  CDR ;
  CDR ;
  CDR ;
  DIP { PUSH mutez 1 } ;
  EDIV ;
  IF_NONE { PUSH string """" ; FAILWITH } { CAR } ;
  PUSH nat 1000 ;
  MUL ;
  AMOUNT ;
  DIP { PUSH mutez 1 } ;
  EDIV ;
  IF_NONE { PUSH string """" ; FAILWITH } { CAR } ;
  DUP ;
  DIP { PUSH nat 997 ; MUL ; ADD } ;
  PUSH nat 997 ;
  MUL ;
  DIP 3 { DUP } ;
  DIG 3 ;
  CDR ;
  CDR ;
  CDR ;
  CAR ;
  MUL ;
  EDIV ;
  IF_NONE { PUSH string ""divByZero."" ; FAILWITH } { CAR } ;
  DUP ;
  DIP { DIP { DUP ; CDR ; CAR } ;
        COMPARE ;
        GE ;
        IF {} { PUSH string ""tokensBought is less than minTokensBought."" ; FAILWITH } } ;
  DUP ;
  DIP 3 { DUP } ;
  DIG 3 ;
  CDR ;
  CDR ;
  CDR ;
  CAR ;
  SUB ;
  DUP ;
  PUSH int 0 ;
  COMPARE ;
  LE ;
  IF { ABS } { PUSH string """" ; FAILWITH } ;
  DIP { DIG 2 } ;
  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 ;
  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 ;
  DIP { DIP { CAR ; SELF ; ADDRESS } } ;
  DUP ;
  CDR ;
  CDR ;
  CAR ;
  CDR ;
  CONTRACT %transfer (pair address (pair address nat)) ;
  IF_NONE { FAILWITH } {} ;
  PUSH mutez 0 ;
  DIG 3 ;
  DIG 5 ;
  DIG 5 ;
  DIP { PAIR } ;
  PAIR ;
  TRANSFER_TOKENS ;
  DIP { NIL operation } ;
  CONS ;
  PAIR }".

Definition ep_tokenToXtz : string := "{ DIP { DUP ; CDR ; CAR ; CAR ; IF { PUSH string ""selfIsUpdatingToken must be false."" ; FAILWITH } {} } ;
  DUP ;
  CDR ;
  CDR ;
  CDR ;
  NOW ;
  COMPARE ;
  LT ;
  IF {} { PUSH string ""NOW is greater than deadline."" ; FAILWITH } ;
  PUSH mutez 0 ;
  AMOUNT ;
  COMPARE ;
  EQ ;
  IF {} { PUSH string ""Amount must be zero."" ; FAILWITH } ;
  DIP { DUP ;
        CDR ;
        CDR ;
        CDR ;
        CDR ;
        PUSH mutez 0 ;
        COMPARE ;
        LT ;
        IF {} { PUSH string ""xtzPool must be greater than zero."" ; FAILWITH } } ;
  DIP { DUP ;
        CDR ;
        CDR ;
        CDR ;
        CAR ;
        PUSH nat 0 ;
        COMPARE ;
        LT ;
        IF {} { PUSH string ""tokenPool must be greater than zero"" ; FAILWITH } } ;
  DUP ;
  CDR ;
  CAR ;
  PUSH nat 0 ;
  COMPARE ;
  LT ;
  IF {} { PUSH string ""tokensSold is zero"" ; FAILWITH } ;
  DUP ;
  CDR ;
  CDR ;
  CAR ;
  PUSH mutez 0 ;
  COMPARE ;
  LT ;
  IF {} { PUSH string ""minXtzBought must be greater than zero."" ; FAILWITH } ;
  DUP ;
  CDR ;
  CAR ;
  PUSH nat 997 ;
  MUL ;
  DIP 2 { DUP } ;
  DIG 2 ;
  CDR ;
  CDR ;
  CDR ;
  CAR ;
  PUSH nat 1000 ;
  MUL ;
  ADD ;
  DIP { DUP } ;
  SWAP ;
  CDR ;
  CAR ;
  PUSH nat 997 ;
  MUL ;
  DIP 3 { DUP } ;
  DIG 3 ;
  CDR ;
  CDR ;
  CDR ;
  CDR ;
  DIP { PUSH mutez 1 } ;
  EDIV ;
  IF_NONE { PUSH string """" ; FAILWITH } { CAR } ;
  MUL ;
  EDIV ;
  IF_NONE { PUSH string ""divByZero."" ; FAILWITH } { CAR } ;
  PUSH mutez 1 ;
  MUL ;
  DUP ;
  DIP { DIP { DUP ; CDR ; CDR ; CAR } ;
        COMPARE ;
        GE ;
        IF {} { PUSH string ""xtzBought is less than minXtzBought."" ; FAILWITH } } ;
  DIP { SWAP ;
        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 } ;
  DUP ;
  DIP { DIP { DUP ; CDR ; CDR ; CDR ; CDR } ;
        SWAP ;
        SUB ;
        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 } ;
  DIP 2 { DUP } ;
  DIG 2 ;
  CAR ;
  CDR ;
  CONTRACT unit ;
  IF_NONE { FAILWITH } {} ;
  DIG 1 ;
  UNIT ;
  TRANSFER_TOKENS ;
  DIP { 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 } ;
  NIL operation ;
  DIG 2 ;
  CONS ;
  SWAP ;
  CONS ;
  PAIR }".

Definition ep_tokenToToken : string := "{ DIP { DUP ; CDR ; CAR ; CAR ; IF { PUSH string ""selfIsUpdatingToken must be false."" ; FAILWITH } {} } ;
  PUSH mutez 0 ;
  AMOUNT ;
  COMPARE ;
  EQ ;
  IF {} { PUSH string ""Amount must be zero."" ; FAILWITH } ;
  DUP ;
  CDR ;
  CDR ;
  CDR ;
  NOW ;
  COMPARE ;
  LT ;
  IF {} { PUSH string ""NOW is greater than deadline."" ; FAILWITH } ;
  DUP ;
  CDR ;
  CDR ;
  CAR ;
  PUSH nat 0 ;
  COMPARE ;
  LT ;
  IF {} { PUSH string ""tokensSold is zero"" ; FAILWITH } ;
  DUP ;
  CAR ;
  CDR ;
  CAR ;
  PUSH nat 0 ;
  COMPARE ;
  LT ;
  IF {} { PUSH string ""minTokensBought must be greater than zero."" ; FAILWITH } ;
  DIP { DUP ;
        CDR ;
        CDR ;
        CDR ;
        CDR ;
        PUSH mutez 0 ;
        COMPARE ;
        LT ;
        IF {} { PUSH string ""xtzPool must be greater than zero."" ; FAILWITH } } ;
  DIP { DUP ;
        CDR ;
        CDR ;
        CDR ;
        CAR ;
        PUSH nat 0 ;
        COMPARE ;
        LT ;
        IF {} { PUSH string ""tokenPool must be greater than zero"" ; FAILWITH } } ;
  DUP ;
  CDR ;
  CDR ;
  CAR ;
  PUSH nat 997 ;
  MUL ;
  DIP 2 { DUP } ;
  DIG 2 ;
  CDR ;
  CDR ;
  CDR ;
  CAR ;
  PUSH nat 1000 ;
  MUL ;
  ADD ;
  DIP { DUP } ;
  SWAP ;
  CDR ;
  CDR ;
  CAR ;
  PUSH nat 997 ;
  MUL ;
  DIP 3 { DUP } ;
  DIG 3 ;
  CDR ;
  CDR ;
  CDR ;
  CDR ;
  DIP { PUSH mutez 1 } ;
  EDIV ;
  IF_NONE { PUSH string """" ; FAILWITH } { CAR } ;
  MUL ;
  EDIV ;
  IF_NONE { PUSH string ""divByZero."" ; FAILWITH } { CAR } ;
  PUSH mutez 1 ;
  MUL ;
  DIP { DUP } ;
  SWAP ;
  CDR ;
  CDR ;
  CAR ;
  DIP 3 { DUP } ;
  DIG 3 ;
  CDR ;
  CDR ;
  CDR ;
  CAR ;
  ADD ;
  DIP { DIG 2 } ;
  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 ;
  DUP ;
  CDR ;
  CDR ;
  CDR ;
  CDR ;
  DIP 2 { DUP } ;
  DIG 2 ;
  SWAP ;
  SUB ;
  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 ;
  DIP 2 { DUP } ;
  DIG 2 ;
  CAR ;
  CAR ;
  CONTRACT %xtzToToken (pair address (pair nat timestamp)) ;
  IF_NONE { FAILWITH } {} ;
  DIG 2 ;
  DIP 3 { DUP } ;
  DIG 3 ;
  DUP ;
  CDR ;
  CAR ;
  DIP { DUP ; CAR ; CDR ; CAR ; DIP { DUP ; CDR ; CDR ; CDR } ; PAIR } ;
  PAIR ;
  SWAP ;
  DROP ;
  TRANSFER_TOKENS ;
  SWAP ;
  DIP { SWAP ; DUP ; CDR ; CDR ; CAR ; DIP { CAR ; CDR ; CDR } } ;
  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 ;
  NIL operation ;
  SWAP ;
  CONS ;
  DIP { SWAP } ;
  SWAP ;
  CONS ;
  PAIR }".

Definition ep_updateTokenPool : string := "{ PUSH mutez 0 ;
  AMOUNT ;
  COMPARE ;
  EQ ;
  IF {} { PUSH string ""Amount must be zero."" ; FAILWITH } ;
  IMPLICIT_ACCOUNT ;
  ADDRESS ;
  SENDER ;
  COMPARE ;
  EQ ;
  IF {} { PUSH string ""unsafeUpdateTokenPool"" ; FAILWITH } ;
  DUP ;
  CDR ;
  CAR ;
  CAR ;
  IF { PUSH string ""selfIsUpdatingToken must be false."" ; FAILWITH } {} ;
  DUP ;
  CDR ;
  PUSH bool True ;
  DIP { DUP ; DIP { CDR } ; CAR } ;
  DIP { DUP ; DIP { CDR } ; CAR } ;
  SWAP ;
  DROP ;
  PAIR ;
  PAIR ;
  DIP { DUP ; DIP { CAR } ; CDR } ;
  SWAP ;
  DROP ;
  SWAP ;
  PAIR ;
  DUP ;
  CDR ;
  CDR ;
  CAR ;
  CDR ;
  CONTRACT %getBalance (pair address (contract nat)) ;
  IF_NONE { FAILWITH } {} ;
  PUSH mutez 0 ;
  SELF %updateTokenPoolInternal ;
  SELF ;
  ADDRESS ;
  PAIR ;
  TRANSFER_TOKENS ;
  DIP { NIL operation } ;
  CONS ;
  PAIR }".

Definition ep_updateTokenPoolInternal : string := "{ PUSH mutez 0 ;
  AMOUNT ;
  COMPARE ;
  EQ ;
  IF {} { PUSH string ""Amount must be zero."" ; FAILWITH } ;
  DIP { DUP } ;
  SWAP ;
  CDR ;
  CAR ;
  CAR ;
  IF {} { PUSH string ""Dexter did not initiate this operation."" ; FAILWITH } ;
  DIP { DUP } ;
  SWAP ;
  CDR ;
  CDR ;
  CAR ;
  CDR ;
  SENDER ;
  COMPARE ;
  EQ ;
  IF
    {}
    { PUSH string ""The sender is not the token contract associated with this contract."" ; FAILWITH } ;
  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 ;
  DUP ;
  CDR ;
  PUSH bool False ;
  DIP { DUP ; DIP { CDR } ; CAR } ;
  DIP { DUP ; DIP { CDR } ; CAR } ;
  SWAP ;
  DROP ;
  PAIR ;
  PAIR ;
  DIP { DUP ; DIP { CAR } ; CDR } ;
  SWAP ;
  DROP ;
  SWAP ;
  PAIR ;
  NIL operation ;
  PAIR }".

Definition ep_setBaker : string := "{ DIP { DUP ; CDR ; CAR ; CAR ; IF { PUSH string ""selfIsUpdatingToken must be false."" ; FAILWITH } {} } ;
  PUSH mutez 0 ;
  AMOUNT ;
  COMPARE ;
  EQ ;
  IF {} { PUSH string ""Amount must be zero."" ; FAILWITH } ;
  DIP { DUP } ;
  SWAP ;
  CDR ;
  CDR ;
  CAR ;
  CAR ;
  SENDER ;
  COMPARE ;
  EQ ;
  IF {} { PUSH string ""sender is not the contract manager."" ; FAILWITH } ;
  DIP { DUP } ;
  SWAP ;
  CDR ;
  CAR ;
  CDR ;
  CAR ;
  NOT ;
  IF {} { PUSH string ""Cannot change the baker while freezeBaker is true."" ; FAILWITH } ;
  DUP ;
  CAR ;
  DIP { CDR } ;
  SET_DELEGATE ;
  DIP { DIP { DUP ; CDR } ;
        DIP { DUP ; DIP { CDR } ; CAR } ;
        DIP { DUP ; DIP { CAR } ; CDR } ;
        DIP { DUP ; DIP { CDR } ; CAR } ;
        SWAP ;
        DROP ;
        PAIR ;
        SWAP ;
        PAIR ;
        PAIR ;
        DIP { DUP ; DIP { CAR } ; CDR } ;
        SWAP ;
        DROP ;
        SWAP ;
        PAIR ;
        NIL operation } ;
  CONS ;
  PAIR }".

Definition ep_setManager : string := "{ DIP { DUP ; CDR ; CAR ; CAR ; IF { PUSH string ""selfIsUpdatingToken must be false."" ; FAILWITH } {} } ;
  PUSH mutez 0 ;
  AMOUNT ;
  COMPARE ;
  EQ ;
  IF {} { PUSH string ""Amount must be zero."" ; FAILWITH } ;
  DIP { DUP } ;
  SWAP ;
  CDR ;
  CDR ;
  CAR ;
  CAR ;
  SENDER ;
  COMPARE ;
  EQ ;
  IF {} { PUSH string ""sender is not the contract manager."" ; FAILWITH } ;
  DIP { DUP ; CDR } ;
  DIP { DUP ; DIP { CAR } ; CDR } ;
  DIP { DUP ; DIP { CDR } ; CAR } ;
  DIP { DUP ; DIP { CDR } ; CAR } ;
  SWAP ;
  DROP ;
  PAIR ;
  PAIR ;
  SWAP ;
  PAIR ;
  DIP { DUP ; DIP { CAR } ; CDR } ;
  SWAP ;
  DROP ;
  SWAP ;
  PAIR ;
  NIL operation ;
  PAIR }".

Definition ep_default : string := "{ DROP ;
  DUP ;
  CDR ;
  CAR ;
  CAR ;
  IF { PUSH string ""selfIsUpdatingToken must be false."" ; FAILWITH } {} ;
  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 ;
  NIL operation ;
  PAIR }".

Definition contract_s : string := "parameter (or
            (or
              (or (pair %approve (address :spender) (pair (nat :allowance) (nat :currentAllowance)))
                  (pair %addLiquidity (pair (address :owner) (nat :minLqtMinted))
                                      (pair (nat :maxTokensDeposited) (timestamp :deadline))))
              (or
                (pair %removeLiquidity (pair (address :owner) (pair (address :to) (nat :lqtBurned)))
                                       (pair (mutez :minXtzWithdrawn)
                                             (pair (nat :minTokensWithdrawn) (timestamp :deadline))))
                (or
                  (pair %xtzToToken (address :to)
                                    (pair (nat :minTokensBought) (timestamp :deadline)))
                  (pair %tokenToXtz (pair (address :owner) (address :to))
                                    (pair (nat :tokensSold)
                                          (pair (mutez :minXtzBought) (timestamp :deadline)))))))
            (or
              (or
                (pair %tokenToToken
                  (pair (address :outputDexterContract)
                        (pair (nat :minTokensBought) (address :owner)))
                  (pair (address :to) (pair (nat :tokensSold) (timestamp :deadline))))
                (or (key_hash %updateTokenPool) (nat %updateTokenPoolInternal)))
              (or (pair %setBaker (option key_hash) bool) (or (address %setManager) (unit %default)))));
storage (pair
          (big_map %accounts (address :owner)
                             (pair (nat :balance) (map (address :spender) (nat :allowance))))
          (pair (pair (bool :selfIsUpdatingTokenPool) (pair (bool :freezeBaker) (nat :lqtTotal)))
                (pair (pair (address :manager) (address :tokenAddress))
                      (pair (nat :tokenPool) (mutez :xtzPool)))));
code { CAST (pair
              (or
                (or
                  (or (pair address (pair nat nat)) (pair (pair address nat) (pair nat timestamp)))
                  (or (pair (pair address (pair address nat)) (pair mutez (pair nat timestamp)))
                      (or (pair address (pair nat timestamp))
                          (pair (pair address address) (pair nat (pair mutez timestamp))))))
                (or
                  (or (pair (pair address (pair nat address)) (pair address (pair nat timestamp)))
                      (or key_hash nat))
                  (or (pair (option key_hash) bool) (or address unit))))
              (pair (big_map address (pair nat (map address nat)))
                    (pair (pair bool (pair bool nat)) (pair (pair address address) (pair nat mutez))))) ;
       DUP ;
       CAR ;
       DIP { CDR } ;
       IF_LEFT
         { IF_LEFT
             { IF_LEFT " ++ ep_approve ++ " " ++ ep_addLiquidity ++ " }
             { IF_LEFT " ++ ep_removeLiquidity ++ " { IF_LEFT " ++ ep_xtzToToken ++ " " ++ ep_tokenToXtz ++ " } } }
         { IF_LEFT
             { IF_LEFT
                 " ++ ep_tokenToToken ++ "
                 { IF_LEFT " ++ ep_updateTokenPool ++ " " ++ ep_updateTokenPoolInternal ++ " } }
             { IF_LEFT " ++ ep_setBaker ++ " { IF_LEFT " ++ ep_setManager ++ " " ++ ep_default ++ " } } } }".
back to top