Docs: update Michelson spec to the new semantics

This commit is contained in:
Benjamin Canou 2018-04-14 00:28:20 +02:00 committed by Grégoire Henry
parent 595685cf42
commit 46efb6f3b3
4 changed files with 351 additions and 126 deletions

View File

@ -1250,7 +1250,9 @@ VI - Domain specific data types
- ``tez``: A specific type for manipulating tokens. - ``tez``: A specific type for manipulating tokens.
- ``contract 'param 'result``: A contract, with the type of its code. - ``contract 'param``: A contract, with the type of its code.
- ``operation``: An internal operation emitted by a contract.
- ``key``: A public cryptography key. - ``key``: A public cryptography key.
@ -1376,33 +1378,33 @@ Operations on contracts
:: ::
:: contract 'p 'r : 'S -> key_hash : 'S :: contract 'p : 'S -> key_hash : 'S
- ``CREATE_CONTRACT``: Forge a new contract. - ``CREATE_CONTRACT``: Forge a new contract.
:: ::
:: key_hash : option key_hash : bool : bool : tez : lambda (pair 'p 'g) (pair 'r 'g) : 'g : 'S :: key_hash : option key_hash : bool : bool : tez : lambda (pair 'p 'g) (pair (list operation) 'g) : 'g : 'S
-> contract 'p 'r : 'S -> contract 'p : 'S
As with non code-emitted originations the contract code takes as As with non code-emitted originations the contract code takes as
argument the transferred amount plus an ad-hoc argument and returns an argument the transferred amount plus an ad-hoc argument and returns an
ad-hoc value. The code also takes the global data and returns it to be ad-hoc value. The code also takes the global data and returns it to be
stored and retrieved on the next transaction. These data are initialized stored and retrieved on the next transaction. These data are initialized
by another parameter. The calling convention for the code is as follows: by another parameter. The calling convention for the code is as follows:
``(Pair arg globals)) -> (Pair ret globals)``, as extrapolated from ``(Pair arg globals)) -> (Pair operations globals)``, as extrapolated from
the instruction type. The first parameters are the manager, optional the instruction type. The first parameters are the manager, optional
delegate, then spendable and delegatable flags and finally the initial delegate, then spendable and delegatable flags and finally the initial
amount taken from the currently executed contract. The contract is amount taken from the currently executed contract. The contract is
returned as a first class value to be called immediately or stored. returned as a first class value to be called immediately or stored.
- ``CREATE_CONTRACT { storage 'g ; parameter 'p ; return 'r ; code ... }``: - ``CREATE_CONTRACT { storage 'g ; parameter 'p ; code ... }``:
Forge a new contract from a literal. Forge a new contract from a literal.
:: ::
:: key_hash : option key_hash : bool : bool : tez : 'g : 'S :: key_hash : option key_hash : bool : bool : tez : 'g : 'S
-> contract 'p 'r : 'S -> contract 'p : 'S
Originate a contract based on a literal. This is currently the only way Originate a contract based on a literal. This is currently the only way
to include transfers inside of an originated contract. The first to include transfers inside of an originated contract. The first
@ -1415,32 +1417,20 @@ value to be called immediately or stored.
:: ::
:: key_hash : option key_hash : bool : tez : 'S -> contract unit unit : 'S :: key_hash : option key_hash : bool : tez : 'S -> contract unit : 'S
Take as argument the manager, optional delegate, the delegatable flag Take as argument the manager, optional delegate, the delegatable flag
and finally the initial amount taken from the currently executed and finally the initial amount taken from the currently executed
contract. contract.
- ``TRANSFER_TOKENS``: Forge and evaluate a transaction. - ``TRANSFER_TOKENS``: Forge a transaction.
:: ::
:: 'p : tez : contract 'p 'r : 'g : [] -> 'r : 'g : [] :: 'p : tez : contract 'p : 'S -> operation : S
The parameter and return value must be consistent with the ones expected The parameter must be consistent with the one expected by the
by the contract, unit for an account. To preserve the global consistency contract, unit for an account.
of the system, the current contracts storage must be updated before
passing the control to another script. For this, the script must put the
partially updated storage on the stack (g is the type of the contracts
storage). If a recursive call to the current contract happened, the
updated storage is put on the stack next to the return value. Nothing
else can remain on the stack during a nested call. If some local values
have to be kept for after the nested call, they have to be stored
explicitly in a transient part of the storage. A trivial example of that
is to reserve a boolean in the storage, initialized to false, reset to
false at the end of each contract execution, and set to true during a
nested call. This thus gives an easy way for a contract to prevent
recursive call (the contract just fails if the boolean is true).
- ``BALANCE``: Push the current amount of tez of the current contract. - ``BALANCE``: Push the current amount of tez of the current contract.
@ -1448,19 +1438,19 @@ recursive call (the contract just fails if the boolean is true).
:: 'S -> tez : 'S :: 'S -> tez : 'S
- ``SOURCE 'p 'r``: Push the source contract of the current - ``SOURCE 'p``: Push the source contract of the current
transaction. transaction.
:: ::
:: 'S -> contract 'p 'r : 'S :: 'S -> contract 'p : 'S
- ``SELF``: Push the current contract. - ``SELF``: Push the current contract.
:: ::
:: 'S -> contract 'p 'r : 'S :: 'S -> contract 'p : 'S
where contract 'p 'r is the type of the current contract where contract 'p is the type of the current contract
- ``AMOUNT``: Push the amount of the current transaction. - ``AMOUNT``: Push the amount of the current transaction.
@ -1476,7 +1466,7 @@ recursive call (the contract just fails if the boolean is true).
:: ::
:: key_hash : 'S -> contract unit unit : 'S :: key_hash : 'S -> contract unit : 'S
Special operations Special operations
~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~
@ -1922,25 +1912,25 @@ storage. The type of the global data of the storage is fixed for each
contract at origination time. This is ensured statically by checking on contract at origination time. This is ensured statically by checking on
origination that the code preserves the type of the global data. For origination that the code preserves the type of the global data. For
this, the code of the contract is checked to be of type this, the code of the contract is checked to be of type
``lambda (pair arg global) -> (pair ret global)`` where ``global`` is the ``lambda (pair arg global) -> (pair (list operation) global)`` where
type of the original global store given on origination. The contract ``global`` is the type of the original global store given on origination.
also takes a parameter and returns a value, hence the complete calling The contract also takes a parameter and returns a list of internal operations,
convention above. hence the complete calling convention above. The internal operations are
queued for execution when the contract returns.
Empty contract Empty contract
~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~
Any contract with the same ``parameter`` and ``return`` types may be The simplest contract is the contract for which the ``parameter`` and
written with an empty sequence in its ``code`` section. The simplest ``storage`` are all of type ``unit``. This contract is as follows:
contract is the contract for which the ``parameter``, ``storage``, and
``return`` are all of type ``unit``. This contract is as follows:
:: ::
code {}; code { CDR ; # keep the storage
NIl operation ; # return no internal operation
PAIR }; # respect the calling convention
storage unit; storage unit;
parameter unit; parameter unit;
return unit;
Reservoir contract Reservoir contract
~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~
@ -1962,7 +1952,7 @@ Hence, the global data of the contract has the following type
'g = 'g =
pair pair
(pair timestamp tez) (pair timestamp tez)
(pair (contract unit unit) (contract unit unit)) (pair (contract unit) (contract unit))
Following the contract calling convention, the code is a lambda of type Following the contract calling convention, the code is a lambda of type
@ -1970,7 +1960,7 @@ Following the contract calling convention, the code is a lambda of type
lambda lambda
(pair unit 'g) (pair unit 'g)
(pair unit 'g) (pair (list operation) 'g)
written as written as
@ -1981,48 +1971,46 @@ written as
unit unit
(pair (pair
(pair timestamp tez) (pair timestamp tez)
(pair (contract unit unit) (contract unit unit)))) (pair (contract unit) (contract unit))))
(pair (pair
unit (list operation)
(pair (pair
(pair timestamp tez) (pair timestamp tez)
(pair (contract unit unit) (contract unit unit)))) (pair (contract unit) (contract unit))))
The complete source ``reservoir.tz`` is: The complete source ``reservoir.tz`` is:
:: ::
parameter timestamp ; parameter unit ;
storage storage
(pair (pair
(pair timestamp tez) # T N (pair (timestamp @T) (tez @N)) # T N
(pair (contract unit unit) (contract unit unit))) ; # A B (pair (contract @A unit) (contract @B unit))) ; # A B
return unit ;
code code
{ DUP ; CDAAR ; # T { CDR ; DUP ; CAAR ; # T
NOW ; NOW ; COMPARE ; LE ;
COMPARE ; LE ; IF { DUP ; CADR ; # N
IF { DUP ; CDADR ; # N
BALANCE ; BALANCE ;
COMPARE ; LE ; COMPARE ; LE ;
IF { CDR ; UNIT ; PAIR } IF { NIL operation ; PAIR }
{ DUP ; CDDDR ; # B { DUP ; CDDR ; # B
BALANCE ; UNIT ; BALANCE ; UNIT ;
DIIIP { CDR } ;
TRANSFER_TOKENS ; TRANSFER_TOKENS ;
NIL operation ; SWAP ; CONS ;
PAIR } } PAIR } }
{ DUP ; CDDAR ; # A { DUP ; CDAR ; # A
BALANCE ; BALANCE ;
UNIT ; UNIT ;
DIIIP { CDR } ;
TRANSFER_TOKENS ; TRANSFER_TOKENS ;
NIL operation ; SWAP ; CONS ;
PAIR } } PAIR } }
Reservoir contract (variant with broker and status) Reservoir contract (variant with broker and status)
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We basically want the same contract as the previous one, but instead of We basically want the same contract as the previous one, but instead of
destroying it, we want to keep it alive, storing a flag ``S`` so that we leaving it empty, we want to keep it alive, storing a flag ``S`` so that we
can tell afterwards if the tokens have been transferred to ``A`` or can tell afterwards if the tokens have been transferred to ``A`` or
``B``. We also want a broker ``X`` to get some fee ``P`` in any case. ``B``. We also want a broker ``X`` to get some fee ``P`` in any case.
@ -2053,20 +2041,19 @@ The complete source ``scrutable_reservoir.tz`` is:
:: ::
parameter timestamp ; parameter unit ;
storage storage
(pair (pair
string # S string # S
(pair (pair
timestamp # T timestamp # T
(pair (pair
(pair tez tez) ; # P N (pair tez tez) # P N
(pair (pair
(contract unit unit) # X (contract unit) # X
(pair (contract unit unit) (contract unit unit)))))) ; # A B (pair (contract unit) (contract unit)))))) ; # A B
return unit ;
code code
{ DUP ; CDAR # S { DUP ; CDAR ; # S
PUSH string "open" ; PUSH string "open" ;
COMPARE ; NEQ ; COMPARE ; NEQ ;
IF { FAIL } # on "success", "timeout" or a bad init value IF { FAIL } # on "success", "timeout" or a bad init value
@ -2083,18 +2070,20 @@ The complete source ``scrutable_reservoir.tz`` is:
COMPARE; LT ; COMPARE; LT ;
IF { # Not enough cash, we just accept the transaction IF { # Not enough cash, we just accept the transaction
# and leave the global untouched # and leave the global untouched
CDR } CDR ; NIL operation ; PAIR }
{ # Enough cash, successful ending { # Enough cash, successful ending
# We update the global # We update the global
CDDR ; PUSH string "success" ; PAIR ; CDDR ; PUSH string "success" ; PAIR ;
# We transfer the fee to the broker # We transfer the fee to the broker
DUP ; CDDAAR ; # P DUP ; CDDAAR ; # P
DIP { DUP ; CDDDAR } # X DIP { DUP ; CDDDAR } ; # X
UNIT ; TRANSFER_TOKENS ; DROP ; UNIT ; TRANSFER_TOKENS ;
# We transfer the rest to A # We transfer the rest to A
DUP ; CDDADR ; # N DIP { DUP ; CDDADR ; # N
DIP { DUP ; CDDDDAR } # A DIP { DUP ; CDDDDAR } ; # A
UNIT ; TRANSFER_TOKENS ; DROP } } UNIT ; TRANSFER_TOKENS } ;
NIL operation ; SWAP ; CONS ; SWAP ; CONS ;
PAIR } }
{ # After timeout, we refund { # After timeout, we refund
# We update the global # We update the global
CDDR ; PUSH string "timeout" ; PAIR ; CDDR ; PUSH string "timeout" ; PAIR ;
@ -2103,17 +2092,17 @@ The complete source ``scrutable_reservoir.tz`` is:
DIP { DUP ; CDDAAR } ; # P DIP { DUP ; CDDAAR } ; # P
COMPARE ; LT ; # available < P COMPARE ; LT ; # available < P
IF { PUSH tez "1.00" ; BALANCE ; SUB ; # available IF { PUSH tez "1.00" ; BALANCE ; SUB ; # available
DIP { DUP ; CDDDAR } # X DIP { DUP ; CDDDAR } ; # X
UNIT ; TRANSFER_TOKENS ; DROP } UNIT ; TRANSFER_TOKENS }
{ DUP ; CDDAAR ; # P { DUP ; CDDAAR ; # P
DIP { DUP ; CDDDAR } # X DIP { DUP ; CDDDAR } ; # X
UNIT ; TRANSFER_TOKENS ; DROP } UNIT ; TRANSFER_TOKENS } ;
# We transfer the rest to B # We transfer the rest to B
PUSH tez "1.00" ; BALANCE ; SUB ; # available DIP { PUSH tez "1.00" ; BALANCE ; SUB ; # available
DIP { DUP ; CDDDDDR } # B DIP { DUP ; CDDDDDR } ; # B
UNIT ; TRANSFER_TOKENS ; DROP } } UNIT ; TRANSFER_TOKENS } ;
# return Unit NIL operation ; SWAP ; CONS ; SWAP ; CONS ;
UNIT ; PAIR } PAIR } } }
Forward contract Forward contract
~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~
@ -2162,8 +2151,8 @@ send all the tokens to the seller.
Otherwise, the seller must deliver at least ``Q`` tons of dried peas to Otherwise, the seller must deliver at least ``Q`` tons of dried peas to
the warehouse, in the next 24 hours. When the amount is equal to or the warehouse, in the next 24 hours. When the amount is equal to or
exceeds ``Q``, all the tokens are transferred to the seller and the exceeds ``Q``, all the tokens are transferred to the seller.
contract is destroyed. For storing the quantity of peas already For storing the quantity of peas already
delivered, we add a counter of type ``nat`` in the global storage. For delivered, we add a counter of type ``nat`` in the global storage. For
knowing this quantity, we accept messages from W with a partial amount knowing this quantity, we accept messages from W with a partial amount
of delivered peas as argument. of delivered peas as argument.
@ -2223,8 +2212,8 @@ The complete source ``forward.tz`` is:
:: ::
parameter (or string nat) ; parameter
return unit ; (or string nat) ;
storage storage
(pair (pair
(pair nat (pair tez tez)) # counter from_buyer from_seller (pair nat (pair tez tez)) # counter from_buyer from_seller
@ -2233,11 +2222,11 @@ The complete source ``forward.tz`` is:
(pair (pair
(pair tez tez) # K C (pair tez tez) # K C
(pair (pair
(pair (contract unit unit) (contract unit unit)) # B S (pair (contract unit) (contract unit)) # B S
(contract unit unit))))) ; # W (contract unit))))) ; # W
code code
{ DUP ; CDDADDR ; # Z { DUP ; CDDADDR ; # Z
PUSH nat 86400 ; SWAP ; ADD ; # one day in second PUSH int 86400 ; SWAP ; ADD ; # one day in second
NOW ; COMPARE ; LT ; NOW ; COMPARE ; LT ;
IF { # Before Z + 24 IF { # Before Z + 24
DUP ; CAR ; # we must receive (Left "buyer") or (Left "seller") DUP ; CAR ; # we must receive (Left "buyer") or (Left "seller")
@ -2251,7 +2240,7 @@ The complete source ``forward.tz`` is:
PUSH nat 0 ; PAIR ; # delivery counter at 0 PUSH nat 0 ; PAIR ; # delivery counter at 0
DIP { CDDR } ; PAIR ; # parameters DIP { CDDR } ; PAIR ; # parameters
# and return Unit # and return Unit
UNIT ; PAIR } NIL operation ; PAIR }
{ PUSH string "seller" ; COMPARE ; EQ ; { PUSH string "seller" ; COMPARE ; EQ ;
IF { DUP ; CDADDR ; # amount already versed by the seller IF { DUP ; CDADDR ; # amount already versed by the seller
DIP { AMOUNT } ; ADD ; # transaction DIP { AMOUNT } ; ADD ; # transaction
@ -2260,10 +2249,12 @@ The complete source ``forward.tz`` is:
PUSH nat 0 ; PAIR ; # delivery counter at 0 PUSH nat 0 ; PAIR ; # delivery counter at 0
DIP { CDDR } ; PAIR ; # parameters DIP { CDDR } ; PAIR ; # parameters
# and return Unit # and return Unit
UNIT ; PAIR } NIL operation ; PAIR }
{ FAIL } } } # (Left _) { FAIL } } } # (Left _)
{ FAIL } } # (Right _) { FAIL } } # (Right _)
{ # After Z + 24 { # After Z + 24
# if balance is emptied, just fail
BALANCE ; PUSH tez "0" ; IFCMPEQ { FAIL } {} ;
# test if the required amount is reached # test if the required amount is reached
DUP ; CDDAAR ; # Q DUP ; CDDAAR ; # Q
DIP { DUP ; CDDDADR } ; MUL ; # C DIP { DUP ; CDDDADR } ; MUL ; # C
@ -2272,25 +2263,28 @@ The complete source ``forward.tz`` is:
BALANCE ; COMPARE ; LT ; # balance < 2 * (Q * C) + 1 BALANCE ; COMPARE ; LT ; # balance < 2 * (Q * C) + 1
IF { # refund the parties IF { # refund the parties
CDR ; DUP ; CADAR ; # amount versed by the buyer CDR ; DUP ; CADAR ; # amount versed by the buyer
DIP { DUP ; CDDDAAR } # B DIP { DUP ; CDDDAAR } ; # B
UNIT ; TRANSFER_TOKENS ; DROP UNIT ; TRANSFER_TOKENS ;
NIL operation ; SWAP ; CONS ; SWAP ;
DUP ; CADDR ; # amount versed by the seller DUP ; CADDR ; # amount versed by the seller
DIP { DUP ; CDDDADR } # S DIP { DUP ; CDDDADR } ; # S
UNIT ; TRANSFER_TOKENS ; DROP UNIT ; TRANSFER_TOKENS ; SWAP ;
BALANCE ; # bonus to the warehouse to destroy the account DIP { CONS } ;
DIP { DUP ; CDDDDR } # W DUP ; CADAR ; DIP { DUP ; CADDR } ; ADD ;
UNIT ; TRANSFER_TOKENS ; DROP BALANCE ; SUB ; # bonus to the warehouse
# return unit, don't change the global DIP { DUP ; CDDDDR } ; # W
# since the contract will be destroyed UNIT ; TRANSFER_TOKENS ;
UNIT ; PAIR } DIP { SWAP } ; CONS ;
# leave the storage as-is, as the balance is now 0
PAIR }
{ # otherwise continue { # otherwise continue
DUP ; CDDADAR # T DUP ; CDDADAR ; # T
NOW ; COMPARE ; LT NOW ; COMPARE ; LT ;
IF { FAIL } # Between Z + 24 and T IF { FAIL } # Between Z + 24 and T
{ # after T { # after T
DUP ; CDDADAR # T DUP ; CDDADAR ; # T
PUSH nat 86400 ; ADD # one day in second PUSH int 86400 ; ADD ; # one day in second
NOW ; COMPARE ; LT NOW ; COMPARE ; LT ;
IF { # Between T and T + 24 IF { # Between T and T + 24
# we only accept transactions from the buyer # we only accept transactions from the buyer
DUP ; CAR ; # we must receive (Left "buyer") DUP ; CAR ; # we must receive (Left "buyer")
@ -2309,7 +2303,7 @@ The complete source ``forward.tz`` is:
PUSH nat 0 ; PAIR ; # delivery counter at 0 PUSH nat 0 ; PAIR ; # delivery counter at 0
DIP { CDDR } ; PAIR ; # parameters DIP { CDDR } ; PAIR ; # parameters
# and return Unit # and return Unit
UNIT ; PAIR } NIL operation ; PAIR }
{ FAIL } } # (Left _) { FAIL } } # (Left _)
{ FAIL } } # (Right _) { FAIL } } # (Right _)
{ # After T + 24 { # After T + 24
@ -2318,24 +2312,23 @@ The complete source ``forward.tz`` is:
DIP { DUP ; CDDDAAR } ; MUL ; # K DIP { DUP ; CDDDAAR } ; MUL ; # K
DIP { DUP ; CDADAR } ; # amount already versed by the buyer DIP { DUP ; CDADAR } ; # amount already versed by the buyer
COMPARE ; NEQ ; COMPARE ; NEQ ;
IF { # not reached, pay the seller and destroy the contract IF { # not reached, pay the seller
BALANCE ; BALANCE ;
DIP { DUP ; CDDDDADR } # S DIP { DUP ; CDDDDADR } ; # S
DIIP { CDR } ; DIIP { CDR } ;
UNIT ; TRANSFER_TOKENS ; DROP ; UNIT ; TRANSFER_TOKENS ;
# and return Unit NIL operation ; SWAP ; CONS ; PAIR }
UNIT ; PAIR }
{ # otherwise continue { # otherwise continue
DUP ; CDDADAR # T DUP ; CDDADAR ; # T
PUSH nat 86400 ; ADD ; PUSH int 86400 ; ADD ;
PUSH nat 86400 ; ADD ; # two days in second PUSH int 86400 ; ADD ; # two days in second
NOW ; COMPARE ; LT NOW ; COMPARE ; LT ;
IF { # Between T + 24 and T + 48 IF { # Between T + 24 and T + 48
# We accept only delivery notifications, from W # We accept only delivery notifications, from W
DUP ; CDDDDDR ; MANAGER ; # W DUP ; CDDDDDR ; MANAGER ; # W
SOURCE unit unit ; MANAGER ; SOURCE unit ; MANAGER ;
COMPARE ; NEQ ; COMPARE ; NEQ ;
IF { FAIL } {} # fail if not the warehouse IF { FAIL } {} ; # fail if not the warehouse
DUP ; CAR ; # we must receive (Right amount) DUP ; CAR ; # we must receive (Right amount)
IF_LEFT IF_LEFT
{ FAIL } # (Left _) { FAIL } # (Left _)
@ -2349,20 +2342,21 @@ The complete source ``forward.tz`` is:
DUP ; CDAAR ; DUP ; CDAAR ;
DIP { DUP ; CDDAAR } ; DIP { DUP ; CDDAAR } ;
COMPARE ; LT ; # counter < Q COMPARE ; LT ; # counter < Q
IF { CDR } # wait for more IF { CDR ; NIL operation } # wait for more
{ # Transfer all the money to the seller { # Transfer all the money to the seller
BALANCE ; # and destroy the contract BALANCE ;
DIP { DUP ; CDDDDADR } # S DIP { DUP ; CDDDDADR } ; # S
DIIP { CDR } ; DIIP { CDR } ;
UNIT ; TRANSFER_TOKENS ; DROP } } ; UNIT ; TRANSFER_TOKENS ;
UNIT ; PAIR } NIL operation ; SWAP ; CONS } } ;
PAIR }
{ # after T + 48, transfer everything to the buyer { # after T + 48, transfer everything to the buyer
BALANCE ; # and destroy the contract BALANCE ;
DIP { DUP ; CDDDDAAR } # B DIP { DUP ; CDDDDAAR } ; # B
DIIP { CDR } ; DIIP { CDR } ;
UNIT ; TRANSFER_TOKENS ; DROP ; UNIT ; TRANSFER_TOKENS ;
# and return unit NIL operation ; SWAP ; CONS ;
UNIT ; PAIR } } } } } } } PAIR} } } } } } }
XII - Full grammar XII - Full grammar
------------------ ------------------
@ -2469,7 +2463,8 @@ XII - Full grammar
| option <type> | option <type>
| list <type> | list <type>
| set <comparable type> | set <comparable type>
| contract <type> <type> | operation
| contract <type>
| pair <type> <type> | pair <type> <type>
| or <type> <type> | or <type> <type>
| lambda <type> <type> | lambda <type> <type>

View File

@ -0,0 +1,145 @@
parameter
(or string nat) ;
storage
(pair
(pair nat (pair tez tez)) # counter from_buyer from_seller
(pair
(pair nat (pair timestamp timestamp)) # Q T Z
(pair
(pair tez tez) # K C
(pair
(pair (contract unit) (contract unit)) # B S
(contract unit))))) ; # W
code
{ DUP ; CDDADDR ; # Z
PUSH int 86400 ; SWAP ; ADD ; # one day in second
NOW ; COMPARE ; LT ;
IF { # Before Z + 24
DUP ; CAR ; # we must receive (Left "buyer") or (Left "seller")
IF_LEFT
{ DUP ; PUSH string "buyer" ; COMPARE ; EQ ;
IF { DROP ;
DUP ; CDADAR ; # amount already versed by the buyer
DIP { AMOUNT } ; ADD ; # transaction
# then we rebuild the globals
DIP { DUP ; CDADDR } ; PAIR ; # seller amount
PUSH nat 0 ; PAIR ; # delivery counter at 0
DIP { CDDR } ; PAIR ; # parameters
# and return Unit
NIL operation ; PAIR }
{ PUSH string "seller" ; COMPARE ; EQ ;
IF { DUP ; CDADDR ; # amount already versed by the seller
DIP { AMOUNT } ; ADD ; # transaction
# then we rebuild the globals
DIP { DUP ; CDADAR } ; SWAP ; PAIR ; # buyer amount
PUSH nat 0 ; PAIR ; # delivery counter at 0
DIP { CDDR } ; PAIR ; # parameters
# and return Unit
NIL operation ; PAIR }
{ FAIL } } } # (Left _)
{ FAIL } } # (Right _)
{ # After Z + 24
# if balance is emptied, just fail
BALANCE ; PUSH tez "0" ; IFCMPEQ { FAIL } {} ;
# test if the required amount is reached
DUP ; CDDAAR ; # Q
DIP { DUP ; CDDDADR } ; MUL ; # C
PUSH nat 2 ; MUL ;
PUSH tez "1.00" ; ADD ;
BALANCE ; COMPARE ; LT ; # balance < 2 * (Q * C) + 1
IF { # refund the parties
CDR ; DUP ; CADAR ; # amount versed by the buyer
DIP { DUP ; CDDDAAR } ; # B
UNIT ; TRANSFER_TOKENS ;
NIL operation ; SWAP ; CONS ; SWAP ;
DUP ; CADDR ; # amount versed by the seller
DIP { DUP ; CDDDADR } ; # S
UNIT ; TRANSFER_TOKENS ; SWAP ;
DIP { CONS } ;
DUP ; CADAR ; DIP { DUP ; CADDR } ; ADD ;
BALANCE ; SUB ; # bonus to the warehouse
DIP { DUP ; CDDDDR } ; # W
UNIT ; TRANSFER_TOKENS ;
DIP { SWAP } ; CONS ;
# leave the storage as-is, as the balance is now 0
PAIR }
{ # otherwise continue
DUP ; CDDADAR ; # T
NOW ; COMPARE ; LT ;
IF { FAIL } # Between Z + 24 and T
{ # after T
DUP ; CDDADAR ; # T
PUSH int 86400 ; ADD ; # one day in second
NOW ; COMPARE ; LT ;
IF { # Between T and T + 24
# we only accept transactions from the buyer
DUP ; CAR ; # we must receive (Left "buyer")
IF_LEFT
{ PUSH string "buyer" ; COMPARE ; EQ ;
IF { DUP ; CDADAR ; # amount already versed by the buyer
DIP { AMOUNT } ; ADD ; # transaction
# The amount must not exceed Q * K
DUP ;
DIIP { DUP ; CDDAAR ; # Q
DIP { DUP ; CDDDAAR } ; MUL ; } ; # K
DIP { COMPARE ; GT ; # new amount > Q * K
IF { FAIL } { } } ; # abort or continue
# then we rebuild the globals
DIP { DUP ; CDADDR } ; PAIR ; # seller amount
PUSH nat 0 ; PAIR ; # delivery counter at 0
DIP { CDDR } ; PAIR ; # parameters
# and return Unit
NIL operation ; PAIR }
{ FAIL } } # (Left _)
{ FAIL } } # (Right _)
{ # After T + 24
# test if the required payment is reached
DUP ; CDDAAR ; # Q
DIP { DUP ; CDDDAAR } ; MUL ; # K
DIP { DUP ; CDADAR } ; # amount already versed by the buyer
COMPARE ; NEQ ;
IF { # not reached, pay the seller
BALANCE ;
DIP { DUP ; CDDDDADR } ; # S
DIIP { CDR } ;
UNIT ; TRANSFER_TOKENS ;
NIL operation ; SWAP ; CONS ; PAIR }
{ # otherwise continue
DUP ; CDDADAR ; # T
PUSH int 86400 ; ADD ;
PUSH int 86400 ; ADD ; # two days in second
NOW ; COMPARE ; LT ;
IF { # Between T + 24 and T + 48
# We accept only delivery notifications, from W
DUP ; CDDDDDR ; MANAGER ; # W
SOURCE unit ; MANAGER ;
COMPARE ; NEQ ;
IF { FAIL } {} ; # fail if not the warehouse
DUP ; CAR ; # we must receive (Right amount)
IF_LEFT
{ FAIL } # (Left _)
{ # We increment the counter
DIP { DUP ; CDAAR } ; ADD ;
# And rebuild the globals in advance
DIP { DUP ; CDADR } ; PAIR ;
DIP { CDDR } ; PAIR ;
UNIT ; PAIR ;
# We test if enough have been delivered
DUP ; CDAAR ;
DIP { DUP ; CDDAAR } ;
COMPARE ; LT ; # counter < Q
IF { CDR ; NIL operation } # wait for more
{ # Transfer all the money to the seller
BALANCE ;
DIP { DUP ; CDDDDADR } ; # S
DIIP { CDR } ;
UNIT ; TRANSFER_TOKENS ;
NIL operation ; SWAP ; CONS } } ;
PAIR }
{ # after T + 48, transfer everything to the buyer
BALANCE ;
DIP { DUP ; CDDDDAAR } ; # B
DIIP { CDR } ;
UNIT ; TRANSFER_TOKENS ;
NIL operation ; SWAP ; CONS ;
PAIR} } } } } } }

View File

@ -0,0 +1,23 @@
parameter unit ;
storage
(pair
(pair (timestamp @T) (tez @N))
(pair (contract @A unit) (contract @B unit))) ;
code
{ CDR ; DUP ; CAAR ; # T
NOW ; COMPARE ; LE ;
IF { DUP ; CADR ; # N
BALANCE ;
COMPARE ; LE ;
IF { NIL operation ; PAIR }
{ DUP ; CDDR ; # B
BALANCE ; UNIT ;
TRANSFER_TOKENS ;
NIL operation ; SWAP ; CONS ;
PAIR } }
{ DUP ; CDAR ; # A
BALANCE ;
UNIT ;
TRANSFER_TOKENS ;
NIL operation ; SWAP ; CONS ;
PAIR } }

View File

@ -0,0 +1,62 @@
parameter unit ;
storage
(pair
string # S
(pair
timestamp # T
(pair
(pair tez tez) # P N
(pair
(contract unit) # X
(pair (contract unit) (contract unit)))))) ; # A B
code
{ DUP ; CDAR ; # S
PUSH string "open" ;
COMPARE ; NEQ ;
IF { FAIL } # on "success", "timeout" or a bad init value
{ DUP ; CDDAR ; # T
NOW ;
COMPARE ; LT ;
IF { # Before timeout
# We compute ((1 + P) + N) tez for keeping the contract alive
PUSH tez "1.00" ;
DIP { DUP ; CDDDAAR } ; ADD ; # P
DIP { DUP ; CDDDADR } ; ADD ; # N
# We compare to the cumulated amount
BALANCE ;
COMPARE; LT ;
IF { # Not enough cash, we just accept the transaction
# and leave the global untouched
CDR ; NIL operation ; PAIR }
{ # Enough cash, successful ending
# We update the global
CDDR ; PUSH string "success" ; PAIR ;
# We transfer the fee to the broker
DUP ; CDDAAR ; # P
DIP { DUP ; CDDDAR } ; # X
UNIT ; TRANSFER_TOKENS ;
# We transfer the rest to A
DIP { DUP ; CDDADR ; # N
DIP { DUP ; CDDDDAR } ; # A
UNIT ; TRANSFER_TOKENS } ;
NIL operation ; SWAP ; CONS ; SWAP ; CONS ;
PAIR } }
{ # After timeout, we refund
# We update the global
CDDR ; PUSH string "timeout" ; PAIR ;
# We try to transfer the fee to the broker
PUSH tez "1.00" ; BALANCE ; SUB ; # available
DIP { DUP ; CDDAAR } ; # P
COMPARE ; LT ; # available < P
IF { PUSH tez "1.00" ; BALANCE ; SUB ; # available
DIP { DUP ; CDDDAR } ; # X
UNIT ; TRANSFER_TOKENS }
{ DUP ; CDDAAR ; # P
DIP { DUP ; CDDDAR } ; # X
UNIT ; TRANSFER_TOKENS } ;
# We transfer the rest to B
DIP { PUSH tez "1.00" ; BALANCE ; SUB ; # available
DIP { DUP ; CDDDDDR } ; # B
UNIT ; TRANSFER_TOKENS } ;
NIL operation ; SWAP ; CONS ; SWAP ; CONS ;
PAIR } } }