Michelson, docs: various fixes

This commit is contained in:
Benjamin Canou 2018-06-12 15:41:50 +02:00
parent 377f3e1e44
commit 15c8c7af86
3 changed files with 57 additions and 75 deletions

View File

@ -16,11 +16,11 @@ are immutable and garbage collected.
A Michelson program receives as input a single element stack containing A Michelson program receives as input a single element stack containing
an input value and the contents of a storage space. It must return a an input value and the contents of a storage space. It must return a
single element stack containing an output value and the new contents of single element stack containing aa output value a list of internal
the storage space. Alternatively, a Michelson program can fail, operations, and the new contents of the storage space. Alternatively,
explicitly using a specific opcode, or because something went wrong that a Michelson program can fail, explicitly using a specific opcode,
could not be caught by the type system (e.g. division by zero, gas or because something went wrong that could not be caught by the type
exhaustion). system (e.g. division by zero, gas exhaustion).
The types of the input, output and storage are fixed and monomorphic, The types of the input, output and storage are fixed and monomorphic,
and the program is typechecked before being introduced into the system. and the program is typechecked before being introduced into the system.
@ -1166,7 +1166,7 @@ VI - Domain specific data types
- ``timestamp``: Dates in the real world. - ``timestamp``: Dates in the real world.
- ``tez``: A specific type for manipulating tokens. - ``mutez``: A specific type for manipulating tokens.
- ``contract 'param``: A contract, with the type of its code. - ``contract 'param``: A contract, with the type of its code.
@ -1230,19 +1230,20 @@ retrieved from script parameters or globals.
iff t1 > t2 iff t1 > t2
Operations on Tez Operations on Mutez
~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~
Tez are internally represented by a 64 bit signed integer. There are Mutez (micro-Tez) are internally represented by a 64 bit signed
restrictions to prevent creating a negative amount of tez. Operations integers. There are restrictions to prevent creating a negative amount
are limited to prevent overflow and mixing them with other numerical of mutez. Operations are limited to prevent overflow and mixing them
types by mistake. They are also mandatory checked for under/overflows. with other numerical types by mistake. They are also mandatory checked
for under/overflows.
- ``ADD``: - ``ADD``:
:: ::
:: tez : tez : 'S -> tez : 'S :: mutez : mutez : 'S -> mutez : 'S
> ADD / x : y : S => [FAILED] on overflow > ADD / x : y : S => [FAILED] on overflow
> ADD / x : y : S => (x + y) : S > ADD / x : y : S => (x + y) : S
@ -1251,7 +1252,7 @@ types by mistake. They are also mandatory checked for under/overflows.
:: ::
:: tez : tez : 'S -> tez : 'S :: mutez : mutez : 'S -> mutez : 'S
> SUB / x : y : S => [FAILED] > SUB / x : y : S => [FAILED]
iff x < y iff x < y
@ -1261,8 +1262,8 @@ types by mistake. They are also mandatory checked for under/overflows.
:: ::
:: tez : nat : 'S -> tez : 'S :: mutez : nat : 'S -> mutez : 'S
:: nat : tez : 'S -> tez : 'S :: nat : mutez : 'S -> mutez : 'S
> MUL / x : y : S => [FAILED] on overflow > MUL / x : y : S => [FAILED] on overflow
> MUL / x : y : S => (x * y) : S > MUL / x : y : S => (x * y) : S
@ -1271,8 +1272,8 @@ types by mistake. They are also mandatory checked for under/overflows.
:: ::
:: tez : nat : 'S -> option (pair tez tez) : 'S :: mutez : nat : 'S -> option (pair mutez mutez) : 'S
:: tez : tez : 'S -> option (pair nat tez) : 'S :: mutez : mutez : 'S -> option (pair nat mutez) : 'S
> EDIV / x : 0 : S => None > EDIV / x : 0 : S => None
> EDIV / x : y : S => Some (Pair (x / y) (x % y)) : S > EDIV / x : y : S => Some (Pair (x / y) (x % y)) : S
@ -1282,7 +1283,7 @@ types by mistake. They are also mandatory checked for under/overflows.
:: ::
:: tez : tez : 'S -> int : 'S :: mutez : mutez : 'S -> int : 'S
> COMPARE / x : y : S => -1 : S > COMPARE / x : y : S => -1 : S
iff x < y iff x < y
@ -1305,7 +1306,7 @@ Operations on contracts
:: ::
:: key_hash : option key_hash : bool : bool : tez : lambda (pair 'p 'g) (pair (list operation) 'g) : 'g : 'S :: key_hash : option key_hash : bool : bool : mutez : lambda (pair 'p 'g) (pair (list operation) 'g) : 'g : 'S
-> operation : address : 'S -> operation : address : 'S
As with non code-emitted originations the contract code takes as As with non code-emitted originations the contract code takes as
@ -1325,7 +1326,7 @@ The ``CONTRACT 'p`` instruction will fail until it is actually originated.
:: ::
:: key_hash : option key_hash : bool : bool : tez : 'g : 'S :: key_hash : option key_hash : bool : bool : mutez : 'g : 'S
-> operation : address : 'S -> operation : address : '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
@ -1338,7 +1339,7 @@ currently executed contract.
:: ::
:: key_hash : option key_hash : bool : tez : 'S :: key_hash : option key_hash : bool : mutez : 'S
-> operation : contract unit : 'S -> operation : contract unit : 'S
Take as argument the manager, optional delegate, the delegatable flag Take as argument the manager, optional delegate, the delegatable flag
@ -1349,7 +1350,7 @@ contract.
:: ::
:: 'p : tez : contract 'p : 'S -> operation : S :: 'p : mutez : contract 'p : 'S -> operation : S
The parameter must be consistent with the one expected by the The parameter must be consistent with the one expected by the
contract, unit for an account. contract, unit for an account.
@ -1360,11 +1361,11 @@ contract, unit for an account.
:: option key_hash : 'S -> operation : S :: option key_hash : 'S -> operation : S
- ``BALANCE``: Push the current amount of tez of the current contract. - ``BALANCE``: Push the current amount of mutez of the current contract.
:: ::
:: 'S -> tez : 'S :: 'S -> mutez : 'S
- ``ADDRESS``: Push the untyped version of a contract. - ``ADDRESS``: Push the untyped version of a contract.
@ -1419,7 +1420,7 @@ contract, unit for an account.
:: ::
:: 'S -> tez : 'S :: 'S -> mutez : 'S
- ``IMPLICIT_ACCOUNT``: Return a default contract with the given - ``IMPLICIT_ACCOUNT``: Return a default contract with the given
public/private key pair. Any funds deposited in this contract can public/private key pair. Any funds deposited in this contract can
@ -1804,31 +1805,23 @@ specification: instructions are represented by uppercase identifiers,
type constructors by lowercase identifiers, and constant constructors type constructors by lowercase identifiers, and constant constructors
are Capitalized. are Capitalized.
All domain specific constants are Micheline strings with specific All domain specific constants are Micheline constants with specific
formats: formats. Some have two representations accepted by the data type
checker: a readable one in a string and an optimized one in a natural.
- ``tez`` amounts are written using the same notation as JSON schemas - ``mutez`` amounts are written as naturals.
and the command line client: thousands are optionally separated by - ``timestamp``\ s are written either using ``RFC 339`` notation
commas, and so goes for mutez. in a string (readable), or as the number of seconds since Epoch
in a natural (optimized).
- ``contract``\ s, ``address``\ es, ``key``\ s and ``signature``\ s
are written as strings, in their usual Base58 encoded versions
(readable), or as the little indian interpretation of their
bytes in a natural (optimized).
- in regexp form: ``([0-9]{1,3}(,[0-9]{3})+)|[0-9]+(\.[0.9]{2})?`` The optimized versions should not reach the RPCs, the protocol code
- ``"1234567"`` means 1234567 tez will convert to optimized by itself when forging operations, storing
- ``"1,234,567"`` means 1234567 tez to the database, and before hashing to get a canonical representation
- ``"1234567.89"`` means 1234567890000 mutez of a datum for a given type.
- ``"1,234,567.0"`` means 123456789 tez
- ``"10,123.456,789"`` means 10123456789 mutez
- ``"1234,567"`` is invalid
- ``"1,234,567.123456"`` is invalid
- ``timestamp``\ s are written using ``RFC 339`` notation.
- ``contract``\ s are the raw strings returned by JSON RPCs or the
command line interface and cannot be forged by hand so their format
is of no interest here.
- ``key``\ s are ``Blake2B`` hashes of ``ed25519`` public keys encoded
in ``base58`` format with the following custom alphabet:
``"eXMNE9qvHPQDdcFx5J86rT7VRm2atAypGhgLfbS3CKjnksB4"``.
- ``signature``\ s are ``ed25519`` signatures as a series of
hex-encoded bytes.
To prevent errors, control flow primitives that take instructions as To prevent errors, control flow primitives that take instructions as
parameters require sequences in the concrete syntax. parameters require sequences in the concrete syntax.
@ -1843,8 +1836,7 @@ Main program structure
The toplevel of a smart contract file must be an un-delimited sequence The toplevel of a smart contract file must be an un-delimited sequence
of four primitive applications (in no particular order) that provide its of four primitive applications (in no particular order) that provide its
``parameter``, ``return`` and ``storage`` types, as well as its ``code``, ``parameter`` and ``storage`` fields.
``code``.
See the next section for a concrete example. See the next section for a concrete example.
@ -2525,11 +2517,6 @@ At the beginning of the transaction:
A via a CDDDDDAR A via a CDDDDDAR
B via a CDDDDDDR B via a CDDDDDDR
For the contract to stay alive, we test that all least ``(Tez "1.00")``
is still available after each transaction. This value is given as an
example and must be updated according to the actual Tezos minimal value
for contract balance.
The complete source ``scrutable_reservoir.tz`` is: The complete source ``scrutable_reservoir.tz`` is:
:: ::
@ -2541,7 +2528,7 @@ The complete source ``scrutable_reservoir.tz`` is:
(pair (pair
timestamp # T timestamp # T
(pair (pair
(pair tez tez) # P N (pair mutez mutez) # P N
(pair (pair
(contract unit) # X (contract unit) # X
(pair (contract unit) (contract unit)))))) ; # A B (pair (contract unit) (contract unit)))))) ; # A B
@ -2554,8 +2541,8 @@ The complete source ``scrutable_reservoir.tz`` is:
NOW ; NOW ;
COMPARE ; LT ; COMPARE ; LT ;
IF { # Before timeout IF { # Before timeout
# We compute ((1 + P) + N) tez for keeping the contract alive # We compute (P + N) mutez
PUSH tez "1.00" ; PUSH mutez 0 ;
DIP { DUP ; CDDDAAR } ; ADD ; # P DIP { DUP ; CDDDAAR } ; ADD ; # P
DIP { DUP ; CDDDADR } ; ADD ; # N DIP { DUP ; CDDDADR } ; ADD ; # N
# We compare to the cumulated amount # We compare to the cumulated amount
@ -2581,17 +2568,17 @@ The complete source ``scrutable_reservoir.tz`` is:
# We update the global # We update the global
CDDR ; PUSH string "timeout" ; PAIR ; CDDR ; PUSH string "timeout" ; PAIR ;
# We try to transfer the fee to the broker # We try to transfer the fee to the broker
PUSH tez "1.00" ; BALANCE ; SUB ; # available BALANCE ; # available
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 { BALANCE ; # available
DIP { DUP ; CDDDAR } ; # X DIP { DUP ; CDDDAR } ; # X
UNIT ; TRANSFER_TOKENS } UNIT ; TRANSFER_TOKENS }
{ DUP ; CDDAAR ; # P { DUP ; CDDAAR ; # P
DIP { DUP ; CDDDAR } ; # X DIP { DUP ; CDDDAR } ; # X
UNIT ; TRANSFER_TOKENS } ; UNIT ; TRANSFER_TOKENS } ;
# We transfer the rest to B # We transfer the rest to B
DIP { PUSH tez "1.00" ; BALANCE ; SUB ; # available DIP { BALANCE ; # available
DIP { DUP ; CDDDDDR } ; # B DIP { DUP ; CDDDDDR } ; # B
UNIT ; TRANSFER_TOKENS } ; UNIT ; TRANSFER_TOKENS } ;
NIL operation ; SWAP ; CONS ; SWAP ; CONS ; NIL operation ; SWAP ; CONS ; SWAP ; CONS ;
@ -2698,9 +2685,6 @@ At the beginning of the transaction:
the amount versed by the seller via a CDADDR the amount versed by the seller via a CDADDR
the argument via a CAR the argument via a CAR
The contract returns a unit value, and we assume that it is created with
the minimum amount, set to ``(Tez "1.00")``.
The complete source ``forward.tz`` is: The complete source ``forward.tz`` is:
:: ::
@ -2747,13 +2731,12 @@ The complete source ``forward.tz`` is:
{ FAIL } } # (Right _) { FAIL } } # (Right _)
{ # After Z + 24 { # After Z + 24
# if balance is emptied, just fail # if balance is emptied, just fail
BALANCE ; PUSH tez "0" ; IFCMPEQ { FAIL } {} ; BALANCE ; PUSH mutez 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
PUSH nat 2 ; MUL ; PUSH nat 2 ; MUL ;
PUSH tez "1.00" ; ADD ; BALANCE ; COMPARE ; LT ; # balance < 2 * (Q * C)
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
@ -2819,7 +2802,7 @@ The complete source ``forward.tz`` is:
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 ; MANAGER ; SENDER ; 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)

View File

@ -45,8 +45,7 @@ code
DUP ; CDDAAR ; # Q DUP ; CDDAAR ; # Q
DIP { DUP ; CDDDADR } ; MUL ; # C DIP { DUP ; CDDDADR } ; MUL ; # C
PUSH nat 2 ; MUL ; PUSH nat 2 ; MUL ;
PUSH mutez 1000000 ; ADD ; BALANCE ; COMPARE ; LT ; # balance < 2 * (Q * C)
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

View File

@ -18,8 +18,8 @@ code
NOW ; NOW ;
COMPARE ; LT ; COMPARE ; LT ;
IF { # Before timeout IF { # Before timeout
# We compute ((1 + P) + N) mutez for keeping the contract alive # We compute (P + N) mutez
PUSH mutez 1000000 ; PUSH mutez 0 ;
DIP { DUP ; CDDDAAR } ; ADD ; # P DIP { DUP ; CDDDAAR } ; ADD ; # P
DIP { DUP ; CDDDADR } ; ADD ; # N DIP { DUP ; CDDDADR } ; ADD ; # N
# We compare to the cumulated amount # We compare to the cumulated amount
@ -45,17 +45,17 @@ code
# We update the global # We update the global
CDDR ; PUSH string "timeout" ; PAIR ; CDDR ; PUSH string "timeout" ; PAIR ;
# We try to transfer the fee to the broker # We try to transfer the fee to the broker
PUSH mutez 1000000 ; BALANCE ; SUB ; # available BALANCE ; # available
DIP { DUP ; CDDAAR } ; # P DIP { DUP ; CDDAAR } ; # P
COMPARE ; LT ; # available < P COMPARE ; LT ; # available < P
IF { PUSH mutez 1000000 ; BALANCE ; SUB ; # available IF { BALANCE ; # available
DIP { DUP ; CDDDAR } ; # X DIP { DUP ; CDDDAR } ; # X
UNIT ; TRANSFER_TOKENS } UNIT ; TRANSFER_TOKENS }
{ DUP ; CDDAAR ; # P { DUP ; CDDAAR ; # P
DIP { DUP ; CDDDAR } ; # X DIP { DUP ; CDDDAR } ; # X
UNIT ; TRANSFER_TOKENS } ; UNIT ; TRANSFER_TOKENS } ;
# We transfer the rest to B # We transfer the rest to B
DIP { PUSH mutez 1000000 ; BALANCE ; SUB ; # available DIP { BALANCE ; # available
DIP { DUP ; CDDDDDR } ; # B DIP { DUP ; CDDDDDR } ; # B
UNIT ; TRANSFER_TOKENS } ; UNIT ; TRANSFER_TOKENS } ;
NIL operation ; SWAP ; CONS ; SWAP ; CONS ; NIL operation ; SWAP ; CONS ; SWAP ; CONS ;