https://gitlab.com/nomadic-labs/mi-cho-coq
Revision d116674d67eca4b4b15d7c08efd878a8c8aa864b authored by kristinas on 11 May 2021, 09:41:59 UTC, committed by kristinas on 11 May 2021, 09:41:59 UTC
1 parent f70493e
Raw File
Tip revision: d116674d67eca4b4b15d7c08efd878a8c8aa864b authored by kristinas on 11 May 2021, 09:41:59 UTC
Added README
Tip revision: d116674
fa12_edukera_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_approve : string :=
  "{ UNPAIR ;
     SWAP ;
     DIG 1 ;
     DUP ;
     DUG 2 ;
     SENDER ;
     PAIR ;
     DIG 4 ;
     DUP ;
     DUG 5 ;
     DIG 1 ;
     DUP ;
     DUG 2 ;
     MEM ;
     IF { DIG 4 ;
          DUP ;
          DUG 5 ;
          DIG 1 ;
          DUP ;
          DUG 2 ;
          GET ;
          IF_NONE { PUSH string ""GetNoneValue"" ;
                    FAILWITH }
                  {  } ;
          PUSH nat 0 ;
          DIG 3 ;
          DUP ;
          DUG 4 ;
          COMPARE ;
          GT ;
          PUSH nat 0 ;
          DIG 2 ;
          DUP ;
          DUG 3 ;
          COMPARE ;
          GT ;
          AND ;
          IF { DUP ;
               PUSH string ""UnsafeAllowanceChange"" ;
               PAIR ;
               FAILWITH }
             {  } ;
          DROP }
        {  } ;
     DIG 4 ;
     DUP ;
     DUG 5 ;
     DIG 2 ;
     DUP ;
     DUG 3 ;
     SOME ;
     DIG 2 ;
     DUP ;
     DUG 3 ;
     UPDATE ;
     DIP { DIG 4 ; DROP } ;
     DUG 4 ;
     DROP 3 ;
     SWAP ;
     PAIR ;
     DIG 1 ;
     PAIR }".

Definition ep_transfer : string :=
  "{ UNPAIR ;
     SWAP ;
     UNPAIR ;
     SWAP ;
     DUP ;
     DIG 4 ;
     DUP ;
     DUG 5 ;
     DIG 4 ;
     DUP ;
     DUG 5 ;
     GET ;
     IF_NONE { PUSH string ""GetNoneValue"" ;
               FAILWITH }
             {  } ;
     COMPARE ;
     GE ;
     NOT ;
     IF { PUSH string ""NotEnoughBalance"" ;
          FAILWITH }
        {  } ;
     DIG 2 ;
     DUP ;
     DUG 3 ;
     SENDER ;
     COMPARE ;
     NEQ ;
     IF { DIG 4 ;
          DUP ;
          DUG 5 ;
          SENDER ;
          DIG 4 ;
          DUP ;
          DUG 5 ;
          PAIR ;
          GET ;
          IF_NONE { PUSH string ""GetNoneValue"" ;
                    FAILWITH }
                  {  } ;
          DIG 1 ;
          DUP ;
          DUG 2 ;
          DIG 1 ;
          DUP ;
          DUG 2 ;
          COMPARE ;
          LT ;
          IF { DUP ;
               DIG 2 ;
               DUP ;
               DUG 3 ;
               PAIR ;
               PUSH string ""NotEnoughAllowance"" ;
               PAIR ;
               FAILWITH }
             {  } ;
          DIG 5 ;
          DUP ;
          DUG 6 ;
          SENDER ;
          DIG 5 ;
          DUP ;
          DUG 6 ;
          PAIR ;
          GET ;
          IF_NONE { PUSH string ""GetNoneValue"" ;
                    FAILWITH }
                  {  } ;
          DIG 6 ;
          DUP ;
          DUG 7 ;
          PUSH int 0 ;
          DIG 4 ;
          DUP ;
          DUG 5 ;
          INT ;
          DIG 3 ;
          DUP ;
          DUG 4 ;
          SUB ;
          COMPARE ;
          GE ;
          IF { DIG 3 ;
               DUP ;
               DUG 4 ;
               INT ;
               DIG 2 ;
               DUP ;
               DUG 3 ;
               SUB ;
               ABS }
             { PUSH string ""AssignNat"" ;
               FAILWITH } ;
          SOME ;
          SENDER ;
          DIG 7 ;
          DUP ;
          DUG 8 ;
          PAIR ;
          UPDATE ;
          DIP { DIG 6 ; DROP } ;
          DUG 6 ;
          DROP 2 }
        {  } ;
     DIG 3 ;
     DUP ;
     DUG 4 ;
     DIG 3 ;
     DUP ;
     DUG 4 ;
     GET ;
     IF_NONE { PUSH string ""GetNoneValue"" ;
               FAILWITH }
             {  } ;
     DIG 4 ;
     DUP ;
     DUG 5 ;
     PUSH int 0 ;
     DIG 3 ;
     DUP ;
     DUG 4 ;
     INT ;
     DIG 3 ;
     DUP ;
     DUG 4 ;
     SUB ;
     COMPARE ;
     GE ;
     IF { DIG 2 ;
          DUP ;
          DUG 3 ;
          INT ;
          DIG 2 ;
          DUP ;
          DUG 3 ;
          SUB ;
          ABS }
        { PUSH string ""AssignNat"" ;
          FAILWITH } ;
     SOME ;
     DIG 5 ;
     DUP ;
     DUG 6 ;
     UPDATE ;
     DIP { DIG 4 ; DROP } ;
     DUG 4 ;
     DROP ;
     DIG 3 ;
     DUP ;
     DUG 4 ;
     DIG 2 ;
     DUP ;
     DUG 3 ;
     MEM ;
     IF { DIG 3 ;
          DUP ;
          DUG 4 ;
          DIG 2 ;
          DUP ;
          DUG 3 ;
          GET ;
          IF_NONE { PUSH string ""GetNoneValue"" ;
                    FAILWITH }
                  {  } ;
          DIG 4 ;
          DUP ;
          DUG 5 ;
          DIG 2 ;
          DUP ;
          DUG 3 ;
          DIG 2 ;
          DUP ;
          DUG 3 ;
          ADD ;
          SOME ;
          DIG 4 ;
          DUP ;
          DUG 5 ;
          UPDATE ;
          DIP { DIG 4 ; DROP } ;
          DUG 4 ;
          DROP }
        { DIG 3 ;
          DUP ;
          DUG 4 ;
          DIG 2 ;
          DUP ;
          DUG 3 ;
          MEM ;
          IF { PUSH string ""KeyAlreadyExists"" ;
               FAILWITH }
             { DIG 3 ;
               DUP ;
               DUG 4 ;
               DIG 1 ;
               DUP ;
               DUG 2 ;
               PUSH nat 0 ;
               ADD ;
               SOME ;
               DIG 3 ;
               DUP ;
               DUG 4 ;
               UPDATE ;
               DIP { DIG 3 ; DROP } ;
               DUG 3 } } ;
     DROP 3 ;
     SWAP ;
     PAIR ;
     DIG 1 ;
     PAIR }".

Definition ep_getTotalSupply : string :=
  "{ UNPAIR ;
     DROP ;
     DIG 3 ;
     DUP ;
     DUG 4 ;
     DIG 1 ;
     DUP ;
     DUG 2 ;
     AMOUNT ;
     PUSH nat 10000000 ;
     TRANSFER_TOKENS ;
     CONS ;
     DIP { DIG 3 ; DROP } ;
     DUG 3 ;
     DROP ;
     SWAP ;
     PAIR ;
     DIG 1 ;
     PAIR }".

Definition ep_getBalance : string :=
  "{ UNPAIR ;
     DIG 4 ;
     DUP ;
     DUG 5 ;
     DIG 2 ;
     DUP ;
     DUG 3 ;
     AMOUNT ;
     DIG 5 ;
     DUP ;
     DUG 6 ;
     DIG 4 ;
     DUP ;
     DUG 5 ;
     GET ;
     IF_NONE { PUSH string ""GetNoneValue"" ;
               FAILWITH }
             {  } ;
     TRANSFER_TOKENS ;
     CONS ;
     DIP { DIG 4 ; DROP } ;
     DUG 4 ;
     DROP 2 ;
     SWAP ;
     PAIR ;
     DIG 1 ;
     PAIR }".

Definition ep_getAllowance : string :=
  "{ UNPAIR ;
     UNPAIR ;
     SWAP ;
     DIG 5 ;
     DUP ;
     DUG 6 ;
     DIG 3 ;
     DUP ;
     DUG 4 ;
     AMOUNT ;
     DIG 7 ;
     DUP ;
     DUG 8 ;
     DIG 4 ;
     DUP ;
     DUG 5 ;
     DIG 6 ;
     DUP ;
     DUG 7 ;
     PAIR ;
     GET ;
     IF_NONE { PUSH string ""GetNoneValue"" ;
               FAILWITH }
             {  } ;
     TRANSFER_TOKENS ;
     CONS ;
     DIP { DIG 5 ; DROP } ;
     DUG 5 ;
     DROP 3 ;
     SWAP ;
     PAIR ;
     DIG 1 ;
     PAIR }".

Definition contract : string :=
  "storage (pair (big_map %allowance (pair address address) nat)
                 (big_map %ledger address nat)) ;
   parameter (or (pair %getAllowance (pair (address %owner) (address %spender)) (contract nat))
                 (or (pair %getBalance (address %owner) (contract nat))
                     (or (pair %getTotalSupply unit (contract nat))
                         (or (pair %transfer (address %from) (pair (address %to) (nat %value)))
                             (pair %approve (address %spender) (nat %value)))))) ;
   code { NIL operation ;
          DIG 1 ;
          UNPAIR ;
          DIP { UNPAIR ;
                SWAP } ;
          IF_LEFT " ++ ep_getAllowance
                    ++ "{ IF_LEFT " ++ ep_getBalance
                                    ++ "{ IF_LEFT " ++ ep_getTotalSupply
                                                    ++ "{ IF_LEFT " ++ ep_transfer
                                                                    ++ ep_approve ++ " } } } }".
back to top