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
Tip revision: d116674d67eca4b4b15d7c08efd878a8c8aa864b authored by kristinas on 11 May 2021, 09:41:59 UTC
Added README
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 ++ " } } } }".
Computing file changes ...