balsoft/ligo
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Docs: various small fixes in Michelson spec

Browse Source
This commit is contained in:
Bruno Bernardo 2018-02-06 16:18:46 +01:00 committed by Benjamin Canou
parent 518a07d5e4
commit ec86dea35f
1 changed files with 266 additions and 244 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

238
docs/whitedoc/michelson.rst
View File

@ -73,6 +73,7 @@ The rules have the main following form.
> (syntax pattern) / (initial stack pattern) => (result stack pattern) > (syntax pattern) / (initial stack pattern) => (result stack pattern)
iff (conditions) iff (conditions)
where (recursions) where (recursions)
and (more recursions)
The left hand side of the ``=>`` sign is used for selecting the rule. The left hand side of the ``=>`` sign is used for selecting the rule.
Given a program and an initial stack, one (and only one) rule can be Given a program and an initial stack, one (and only one) rule can be
@ -323,7 +324,7 @@ consistent with the expected result, also provided by the programmer.
Annotations Annotations
~~~~~~~~~~~ ~~~~~~~~~~~
Most Instructions in the language can optionally take an annotation. Most instructions in the language can optionally take an annotation.
Annotations allow you to better track data, on the stack and within Annotations allow you to better track data, on the stack and within
pairs and unions. pairs and unions.
@ -453,8 +454,8 @@ Control structures
:: (or 'a 'b) : 'A -> 'A :: (or 'a 'b) : 'A -> 'A
iff body :: [ 'a : 'A -> (or 'a 'b) : 'A ] iff body :: [ 'a : 'A -> (or 'a 'b) : 'A ]
> LOOP body / (Left a) : S => body ; LOOP body / (or 'a 'b) : S > LOOP_LEFT body / (Left a) : S => body ; LOOP_LEFT body / (or 'a 'b) : S
> LOOP body / (Right b) : S => b : S > LOOP_LEFT body / (Right b) : S => b : S
- ``DIP code``: Runs code protecting the top of the stack. - ``DIP code``: Runs code protecting the top of the stack.
@ -545,8 +546,9 @@ second, and positive otherwise.
:: int : 'S -> bool : 'S :: int : 'S -> bool : 'S
> EQ ; C / 0 : S => C / True : S > EQ / 0 : S => True : S
> EQ ; C / _ : S => C / False : S > EQ / v : S => False : S
iff v <> 0
- ``NEQ``: Checks that the top of the stack does Not EQual zero. - ``NEQ``: Checks that the top of the stack does Not EQual zero.
@ -554,8 +556,9 @@ second, and positive otherwise.
:: int : 'S -> bool : 'S :: int : 'S -> bool : 'S
> NEQ ; C / 0 : S => C / False : S > NEQ / 0 : S => False : S
> NEQ ; C / _ : S => C / True : S > NEQ / v : S => True : S
iff v <> 0
- ``LT``: Checks that the top of the stack is Less Than zero. - ``LT``: Checks that the top of the stack is Less Than zero.
@ -563,8 +566,10 @@ second, and positive otherwise.
:: int : 'S -> bool : 'S :: int : 'S -> bool : 'S
> LT ; C / v : S => C / True : S iff v < 0 > LT / v : S => True : S
> LT ; C / _ : S => C / False : S iff v < 0
> LT / v : S => False : S
iff v >= 0
- ``GT``: Checks that the top of the stack is Greater Than zero. - ``GT``: Checks that the top of the stack is Greater Than zero.
@ -572,8 +577,10 @@ second, and positive otherwise.
:: int : 'S -> bool : 'S :: int : 'S -> bool : 'S
> GT ; C / v : S => C / True : S iff v > 0 > GT / v : S => C / True : S
> GT ; C / _ : S => C / False : S iff v > 0
> GT / v : S => C / False : S
iff v <= 0
- ``LE``: Checks that the top of the stack is Less Than of Equal to - ``LE``: Checks that the top of the stack is Less Than of Equal to
zero. zero.
@ -582,8 +589,10 @@ second, and positive otherwise.
:: int : 'S -> bool : 'S :: int : 'S -> bool : 'S
> LE ; C / v : S => C / True : S iff v <= 0 > LE / v : S => True : S
> LE ; C / _ : S => C / False : S iff v <= 0
> LE / v : S => False : S
iff v > 0
- ``GE``: Checks that the top of the stack is Greater Than of Equal to - ``GE``: Checks that the top of the stack is Greater Than of Equal to
zero. zero.
@ -592,8 +601,10 @@ second, and positive otherwise.
:: int : 'S -> bool : 'S :: int : 'S -> bool : 'S
> GE ; C / v : S => C / True : S iff v >= 0 > GE / v : S => True : S
> GE ; C / _ : S => C / False : S iff v >= 0
> GE / v : S => False : S
iff v < 0
V - Operations V - Operations
-------------- --------------
@ -607,7 +618,7 @@ Operations on booleans
:: bool : bool : 'S -> bool : 'S :: bool : bool : 'S -> bool : 'S
> OR ; C / x : y : S => C / (x | y) : S > OR / x : y : S => (x | y) : S
- ``AND`` - ``AND``
@ -615,7 +626,7 @@ Operations on booleans
:: bool : bool : 'S -> bool : 'S :: bool : bool : 'S -> bool : 'S
> AND ; C / x : y : S => C / (x & y) : S > AND / x : y : S => (x & y) : S
- ``XOR`` - ``XOR``
@ -623,7 +634,7 @@ Operations on booleans
:: bool : bool : 'S -> bool : 'S :: bool : bool : 'S -> bool : 'S
> XOR ; C / x : y : S => C / (x ^ y) : S > XOR / x : y : S => (x ^ y) : S
- ``NOT`` - ``NOT``
@ -631,7 +642,7 @@ Operations on booleans
:: bool : 'S -> bool : 'S :: bool : 'S -> bool : 'S
> NOT ; C / x : S => C / ~x : S > NOT / x : S => ~x : S
Operations on integers and natural numbers Operations on integers and natural numbers
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@ -646,7 +657,7 @@ limit is fuel.
:: int : 'S -> int : 'S :: int : 'S -> int : 'S
:: nat : 'S -> int : 'S :: nat : 'S -> int : 'S
> NEG ; C / x : S => C / -x : S > NEG / x : S => -x : S
- ``ABS`` - ``ABS``
@ -654,7 +665,7 @@ limit is fuel.
:: int : 'S -> nat : 'S :: int : 'S -> nat : 'S
> ABS ; C / x : S => C / abs (x) : S > ABS / x : S => abs (x) : S
- ``ADD`` - ``ADD``
@ -665,7 +676,7 @@ limit is fuel.
:: nat : int : 'S -> int : 'S :: nat : int : 'S -> int : 'S
:: nat : nat : 'S -> nat : 'S :: nat : nat : 'S -> nat : 'S
> ADD ; C / x : y : S => C / (x + y) : S > ADD / x : y : S => (x + y) : S
- ``SUB`` - ``SUB``
@ -676,7 +687,7 @@ limit is fuel.
:: nat : int : 'S -> int : 'S :: nat : int : 'S -> int : 'S
:: nat : nat : 'S -> int : 'S :: nat : nat : 'S -> int : 'S
> SUB ; C / x : y : S => C / (x - y) : S > SUB / x : y : S => (x - y) : S
- ``MUL`` - ``MUL``
@ -687,7 +698,7 @@ limit is fuel.
:: nat : int : 'S -> int : 'S :: nat : int : 'S -> int : 'S
:: nat : nat : 'S -> nat : 'S :: nat : nat : 'S -> nat : 'S
> MUL ; C / x : y : S => C / (x * y) : S > MUL / x : y : S => (x * y) : S
- ``EDIV`` Perform Euclidian division - ``EDIV`` Perform Euclidian division
@ -698,8 +709,9 @@ limit is fuel.
:: nat : int : 'S -> option (pair int nat) : 'S :: nat : int : 'S -> option (pair int nat) : 'S
:: nat : nat : 'S -> option (pair nat nat) : 'S :: nat : nat : 'S -> option (pair nat nat) : 'S
> EDIV ; C / x : 0 : S => C / None > EDIV / x : 0 : S => None : S
> EDIV ; C / x : y : S => C / Some (Pair (x / y) (x % y)) : S > EDIV / x : y : S => Some (Pair (x / y) (x % y)) : S
iff y <> 0
Bitwise logical operators are also available on unsigned integers. Bitwise logical operators are also available on unsigned integers.
@ -709,7 +721,7 @@ Bitwise logical operators are also available on unsigned integers.
:: nat : nat : 'S -> nat : 'S :: nat : nat : 'S -> nat : 'S
> OR ; C / x : y : S => C / (x | y) : S > OR / x : y : S => (x | y) : S
- ``AND`` - ``AND``
@ -717,7 +729,7 @@ Bitwise logical operators are also available on unsigned integers.
:: nat : nat : 'S -> nat : 'S :: nat : nat : 'S -> nat : 'S
> AND ; C / x : y : S => C / (x & y) : S > AND / x : y : S => (x & y) : S
- ``XOR`` - ``XOR``
@ -725,7 +737,7 @@ Bitwise logical operators are also available on unsigned integers.
:: nat : nat : 'S -> nat : 'S :: nat : nat : 'S -> nat : 'S
> XOR ; C / x : y : S => C / (x ^ y) : S > XOR / x : y : S => (x ^ y) : S
- ``NOT`` The return type of ``NOT`` is an ``int`` and not a ``nat``. - ``NOT`` The return type of ``NOT`` is an ``int`` and not a ``nat``.
This is because the sign is also negated. The resulting integer is This is because the sign is also negated. The resulting integer is
@ -737,7 +749,7 @@ Bitwise logical operators are also available on unsigned integers.
:: nat : 'S -> int : 'S :: nat : 'S -> int : 'S
:: int : 'S -> int : 'S :: int : 'S -> int : 'S
> NOT ; C / x : S => C / ~x : S > NOT / x : S => ~x : S
- ``LSL`` - ``LSL``
@ -745,9 +757,10 @@ Bitwise logical operators are also available on unsigned integers.
:: nat : nat : 'S -> nat : 'S :: nat : nat : 'S -> nat : 'S
> LSL ; C / x : s : S => C / (x << s) : S > LSL / x : s : S => (x << s) : S
iff s <= 256 iff s <= 256
> LSL ; C / x : s : S => [FAIL] > LSL / x : s : S => [FAIL]
iff s > 256
- ``LSR`` - ``LSR``
@ -755,7 +768,7 @@ Bitwise logical operators are also available on unsigned integers.
:: nat : nat : 'S -> nat : 'S :: nat : nat : 'S -> nat : 'S
> LSR ; C / x : s : S => C / (x >>> s) : S > LSR / x : s : S => (x >>> s) : S
- ``COMPARE``: Integer/natural comparison - ``COMPARE``: Integer/natural comparison
@ -764,9 +777,12 @@ Bitwise logical operators are also available on unsigned integers.
:: int : int : 'S -> int : 'S :: int : int : 'S -> int : 'S
:: nat : nat : 'S -> int : 'S :: nat : nat : 'S -> int : 'S
> COMPARE ; C / x : y : S => C / -1 : S iff x < y > COMPARE / x : y : S => -1 : S
> COMPARE ; C / x : y : S => C / 0 : S iff x = y iff x < y
> COMPARE ; C / x : y : S => C / 1 : S iff x > y > COMPARE / x : y : S => 0 : S
iff x = y
> COMPARE / x : y : S => 1 : S
iff x > y
Operations on strings Operations on strings
~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~
@ -805,7 +821,7 @@ Operations on pairs
:: 'a : 'b : 'S -> pair 'a 'b : 'S :: 'a : 'b : 'S -> pair 'a 'b : 'S
> PAIR ; C / a : b : S => C / (Pair a b) : S > PAIR / a : b : S => (Pair a b) : S
- ``CAR``: Access the left part of a pair. - ``CAR``: Access the left part of a pair.
@ -813,7 +829,7 @@ Operations on pairs
:: pair 'a _ : 'S -> 'a : 'S :: pair 'a _ : 'S -> 'a : 'S
> Car ; C / (Pair a _) : S => C / a : S > CAR / (Pair a _) : S => a : S
- ``CDR``: Access the right part of a pair. - ``CDR``: Access the right part of a pair.
@ -821,7 +837,7 @@ Operations on pairs
:: pair _ 'b : 'S -> 'b : 'S :: pair _ 'b : 'S -> 'b : 'S
> Car ; C / (Pair _ b) : S => C / b : S > CDR / (Pair _ b) : S => b : S
Operations on sets Operations on sets
~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~
@ -829,12 +845,14 @@ Operations on sets
- ``EMPTY_SET 'elt``: Build a new, empty set for elements of a given - ``EMPTY_SET 'elt``: Build a new, empty set for elements of a given
type. type.
The ``'elt`` type must be comparable (the ``COMPARE``
primitive must be defined over it).
:: ::
:: 'S -> set 'elt : 'S :: 'S -> set 'elt : 'S
The `'elt` type must be comparable (the `COMPARE` primitive must > EMPTY_SET _ / S => {} : S
be defined over it).
- ``MEM``: Check for the presence of an element in a set. - ``MEM``: Check for the presence of an element in a set.
@ -907,7 +925,8 @@ Operations on sets
Operations on maps Operations on maps
~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~
- ``EMPTY_MAP 'key 'val``: Build a new, empty map. - ``EMPTY_MAP 'key 'val``: Build a new, empty map from keys of a
given type to values of another given type.
The ``'key`` type must be comparable (the ``COMPARE`` primitive must The ``'key`` type must be comparable (the ``COMPARE`` primitive must
be defined over it). be defined over it).
@ -1035,28 +1054,28 @@ Operations on optional values
:: ::
:: 'a : 'S -> 'a? : 'S :: 'a : 'S -> option 'a : 'S
> SOME ; C / v :: S => C / (Some v) :: S > SOME / v : S => (Some v) : S
- ``NONE 'a``: The absent optional value. - ``NONE 'a``: The absent optional value.
:: ::
:: 'S -> 'a? : 'S :: 'S -> option 'a : 'S
> NONE ; C / v :: S => C / None :: S > NONE / v : S => None : S
- ``IF_NONE bt bf``: Inspect an optional value. - ``IF_NONE bt bf``: Inspect an optional value.
:: ::
:: 'a? : 'S -> 'b : 'S :: option 'a : 'S -> 'b : 'S
iff bt :: [ 'S -> 'b : 'S] iff bt :: [ 'S -> 'b : 'S]
bf :: [ 'a : 'S -> 'b : 'S] bf :: [ 'a : 'S -> 'b : 'S]
> IF_NONE ; C / (None) : S => bt ; C / S > IF_NONE bt bf / (None) : S => bt / S
> IF_NONE ; C / (Some a) : S => bf ; C / a : S > IF_NONE bt bf / (Some a) : S => bf / a : S
Operations on unions Operations on unions
~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~
@ -1067,7 +1086,7 @@ Operations on unions
:: 'a : 'S -> or 'a 'b : 'S :: 'a : 'S -> or 'a 'b : 'S
> LEFT ; C / v :: S => C / (Left v) :: S > LEFT / v : S => (Left v) : S
- ``RIGHT 'a``: Pack a value in a union (right case). - ``RIGHT 'a``: Pack a value in a union (right case).
@ -1075,7 +1094,7 @@ Operations on unions
:: 'b : 'S -> or 'a 'b : 'S :: 'b : 'S -> or 'a 'b : 'S
> RIGHT ; C / v :: S => C / (Right v) :: S > RIGHT / v : S => (Right v) : S
- ``IF_LEFT bt bf``: Inspect a value of a variant type. - ``IF_LEFT bt bf``: Inspect a value of a variant type.
@ -1085,8 +1104,8 @@ Operations on unions
iff bt :: [ 'a : 'S -> 'c : 'S] iff bt :: [ 'a : 'S -> 'c : 'S]
bf :: [ 'b : 'S -> 'c : 'S] bf :: [ 'b : 'S -> 'c : 'S]
> IF_LEFT ; C / (Left a) : S => bt ; C / a : S > IF_LEFT bt bf / (Left a) : S => bt / a : S
> IF_LEFT ; C / (Right b) : S => bf ; C / b : S > IF_LEFT bt bf / (Right b) : S => bf / b : S
- ``IF_RIGHT bt bf``: Inspect a value of a variant type. - ``IF_RIGHT bt bf``: Inspect a value of a variant type.
@ -1096,8 +1115,8 @@ Operations on unions
iff bt :: [ 'b : 'S -> 'c : 'S] iff bt :: [ 'b : 'S -> 'c : 'S]
bf :: [ 'a : 'S -> 'c : 'S] bf :: [ 'a : 'S -> 'c : 'S]
> IF_LEFT ; C / (Right b) : S => bt ; C / b : S > IF_RIGHT bt bf / (Right b) : S => bt / b : S
> IF_RIGHT ; C / (Left a) : S => bf ; C / a : S > IF_RIGHT bt bf / (Left a) : S => bf / a : S
Operations on lists Operations on lists
~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~
@ -1108,7 +1127,7 @@ Operations on lists
:: 'a : list 'a : 'S -> list 'a : 'S :: 'a : list 'a : 'S -> list 'a : 'S
> CONS ; C / a : { <l> } : S => C / { a ; <l> } : S > CONS / a : { <l> } : S => { a ; <l> } : S
- ``NIL 'a``: The empty list. - ``NIL 'a``: The empty list.
@ -1116,7 +1135,7 @@ Operations on lists
:: 'S -> list 'a : 'S :: 'S -> list 'a : 'S
> NIL ; C / S => C / {} : S > NIL / S => {} : S
- ``IF_CONS bt bf``: Inspect an optional value. - ``IF_CONS bt bf``: Inspect an optional value.
@ -1126,8 +1145,8 @@ Operations on lists
iff bt :: [ 'a : list 'a : 'S -> 'b : 'S] iff bt :: [ 'a : list 'a : 'S -> 'b : 'S]
bf :: [ 'S -> 'b : 'S] bf :: [ 'S -> 'b : 'S]
> IF_CONS ; C / { a ; <rest> } : S => bt ; C / a : { <rest> } : S > IF_CONS bt bf / { a ; <rest> } : S => bt / a : { <rest> } : S
> IF_CONS ; C / {} : S => bf ; C / S > IF_CONS bt bf / {} : S => bf / S
- ``MAP``: Apply a function on a list from left to right and return the - ``MAP``: Apply a function on a list from left to right and return the
list of results in the same order. list of results in the same order.
@ -1220,8 +1239,8 @@ retrieved from script parameters or globals.
:: timestamp : int : 'S -> timestamp : 'S :: timestamp : int : 'S -> timestamp : 'S
:: int : timestamp : 'S -> timestamp : 'S :: int : timestamp : 'S -> timestamp : 'S
> ADD ; C / seconds : nat (t) : S => C / (seconds + t) : S > ADD / seconds : nat (t) : S => (seconds + t) : S
> ADD ; C / nat (t) : seconds : S => C / (t + seconds) : S > ADD / nat (t) : seconds : S => (t + seconds) : S
- ``SUB`` Subtract a number of seconds from a timestamp. - ``SUB`` Subtract a number of seconds from a timestamp.
@ -1229,7 +1248,7 @@ retrieved from script parameters or globals.
:: timestamp : int : 'S -> timestamp : 'S :: timestamp : int : 'S -> timestamp : 'S
> SUB ; C / seconds : nat (t) : S => C / (seconds - t) : S > SUB / seconds : nat (t) : S => (seconds - t) : S
- ``SUB`` Subtract two timestamps. - ``SUB`` Subtract two timestamps.
@ -1237,7 +1256,7 @@ retrieved from script parameters or globals.
:: timestamp : timestamp : 'S -> int : 'S :: timestamp : timestamp : 'S -> int : 'S
> SUB ; C / seconds(t1) : seconds(t2) : S => C / (t1 - t2) : S > SUB / seconds(t1) : seconds(t2) : S => (t1 - t2) : S
- ``COMPARE``: Timestamp comparison. - ``COMPARE``: Timestamp comparison.
@ -1267,8 +1286,8 @@ types by mistake. They are also mandatory checked for under/overflows.
:: tez : tez : 'S -> tez : 'S :: tez : tez : 'S -> tez : 'S
> ADD ; C / x : y : S => [FAIL] on overflow > ADD / x : y : S => [FAIL] on overflow
> ADD ; C / x : y : S => C / (x + y) : S > ADD / x : y : S => (x + y) : S
- ``SUB``: - ``SUB``:
@ -1276,8 +1295,9 @@ types by mistake. They are also mandatory checked for under/overflows.
:: tez : tez : 'S -> tez : 'S :: tez : tez : 'S -> tez : 'S
> SUB ; C / x : y : S => [FAIL] iff x < y > SUB / x : y : S => [FAIL]
> SUB ; C / x : y : S => C / (x - y) : S iff x < y
> SUB / x : y : S => (x - y) : S
- ``MUL`` - ``MUL``
@ -1286,8 +1306,8 @@ types by mistake. They are also mandatory checked for under/overflows.
:: tez : nat : 'S -> tez : 'S :: tez : nat : 'S -> tez : 'S
:: nat : tez : 'S -> tez : 'S :: nat : tez : 'S -> tez : 'S
> MUL ; C / x : y : S => [FAIL] on overflow > MUL / x : y : S => [FAIL] on overflow
> MUL ; C / x : y : S => C / (x * y) : S > MUL / x : y : S => (x * y) : S
- ``EDIV`` - ``EDIV``
@ -1296,10 +1316,12 @@ types by mistake. They are also mandatory checked for under/overflows.
:: tez : nat : 'S -> option (pair tez tez) : 'S :: tez : nat : 'S -> option (pair tez tez) : 'S
:: tez : tez : 'S -> option (pair nat tez) : 'S :: tez : tez : 'S -> option (pair nat tez) : 'S
> EDIV ; C / x : 0 : S => C / None > EDIV / x : 0 : S => None
> EDIV ; C / x : y : S => C / Some (Pair (x / y) (x % y)) : S > EDIV / x : y : S => Some (Pair (x / y) (x % y)) : S
iff y <> 0
- ``COMPARE``
- ``COMPARE``:
:: ::
:: tez : tez : ’S -> int : ’S :: tez : tez : ’S -> int : ’S
@ -1324,7 +1346,7 @@ Operations on contracts
:: ::
:: key_hash : 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 'r 'g) : 'g : 'S
-> contract 'p 'r : 'S -> contract 'p 'r : 'S
As with non code-emitted originations the contract code takes as As with non code-emitted originations the contract code takes as
@ -1343,7 +1365,7 @@ returned as a first class value to be called immediately or stored.
:: ::
:: key_hash : key_hash? : bool : bool : tez : 'g : 'S :: key_hash : option key_hash : bool : bool : tez : 'g : 'S
-> contract 'p 'r : 'S -> contract 'p 'r : '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
@ -1357,7 +1379,7 @@ value to be called immediately or stored.
:: ::
:: key_hash : key_hash? : bool : tez : 'S -> contract unit unit : 'S :: key_hash : option key_hash : bool : tez : 'S -> contract unit 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
@ -1388,27 +1410,27 @@ 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 'r``: Push the source contract of the current
transaction. transaction.
:: ::
:: 'S -> contract 'p 'r :: 'S :: 'S -> contract 'p 'r : 'S
- ``SELF``: Push the current contract. - ``SELF``: Push the current contract.
:: ::
:: 'S -> contract 'p 'r :: 'S :: 'S -> contract 'p 'r : 'S
where contract 'p 'r is the type of the current contract where contract 'p 'r is the type of the current contract
- ``AMOUNT``: Push the amount of the current transaction. - ``AMOUNT``: Push the amount of the current transaction.
:: ::
:: 'S -> tez :: 'S :: 'S -> tez : 'S
- ``DEFAULT_ACCOUNT``: Return a default contract with the given - ``DEFAULT_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
@ -1418,7 +1440,7 @@ recursive call (the contract just fails if the boolean is true).
:: ::
:: key_hash : 'S -> contract unit unit :: 'S :: key_hash : 'S -> contract unit unit : 'S
Special operations Special operations
~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~
@ -1428,7 +1450,7 @@ Special operations
:: ::
:: 'S -> nat :: 'S :: 'S -> nat : 'S
- ``NOW``: Push the timestamp of the block whose validation triggered - ``NOW``: Push the timestamp of the block whose validation triggered
this execution (does not change during the execution of the this execution (does not change during the execution of the
@ -1436,7 +1458,7 @@ Special operations
:: ::
:: 'S -> timestamp :: 'S :: 'S -> timestamp : 'S
Cryptographic primitives Cryptographic primitives
~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~
@ -1497,19 +1519,19 @@ combinators, and also for branching.
:: ::
> CMP(\op) ; C / S => COMPARE ; (\op) ; C / S > CMP(\op) / S => COMPARE ; (\op) / S
- ``IF{EQ|NEQ|LT|GT|LE|GE} bt bf`` - ``IF{EQ|NEQ|LT|GT|LE|GE} bt bf``
:: ::
> IF(\op) ; C / S => (\op) ; IF bt bf ; C / S > IF(\op) bt bf / S => (\op) ; IF bt bf / S
- ``IFCMP{EQ|NEQ|LT|GT|LE|GE} bt bf`` - ``IFCMP{EQ|NEQ|LT|GT|LE|GE} bt bf``
:: ::
> IFCMP(\op) ; C / S => COMPARE ; (\op) ; IF bt bf ; C / S > IFCMP(\op) / S => COMPARE ; (\op) ; IF bt bf / S
Assertion Macros Assertion Macros
~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~
@ -1522,7 +1544,7 @@ to increase clarity about illegal states.
:: ::
> IF {} {FAIL} > ASSERT => IF {} {FAIL}
- ``ASSERT_{EQ|NEQ|LT|LE|GT|GE}``: - ``ASSERT_{EQ|NEQ|LT|LE|GT|GE}``:
@ -1536,17 +1558,17 @@ to increase clarity about illegal states.
> ASSERT_CMP(\op) => IFCMP(\op) {} {FAIL} > ASSERT_CMP(\op) => IFCMP(\op) {} {FAIL}
- ``ASSERT_NONE``: Equivalent to \``. - ``ASSERT_NONE``
:: ::
> ASSERT_NONE => IF_NONE {} {FAIL} > ASSERT_NONE => IF_NONE {} {FAIL}
- ``ASSERT_SOME``: Equivalent to ``IF_NONE {FAIL} {}``. - ``ASSERT_SOME``
:: ::
> ASSERT_NONE => IF_NONE {FAIL} {} > ASSERT_SOME => IF_SOME {FAIL} {}
- ``ASSERT_LEFT``: - ``ASSERT_LEFT``:
@ -1583,26 +1605,26 @@ operations.
:: ::
> P(\fst=A*)AI(\rest=(A*AI)+)R ; C / S => P(\fst)AIR ; P(\rest)R ; C / S > P(\fst=A*)AI(\rest=(A*AI)+)R / S => P(\fst)AIR ; P(\rest)R / S
> PA(\rest=A*)AIR ; C / S => DIP (P(\rest)AIR) ; C / S > PA(\rest=A*)AIR / S => DIP (P(\rest)AIR) / S
- ``C[AD]+R``: A syntactic sugar for accessing fields in nested pairs. - ``C[AD]+R``: A syntactic sugar for accessing fields in nested pairs.
:: ::
> CA(\rest=[AD]+)R ; C / S => CAR ; C(\rest)R ; C / S > CA(\rest=[AD]+)R / S => CAR ; C(\rest)R / S
> CD(\rest=[AD]+)R ; C / S => CDR ; C(\rest)R ; C / S > CD(\rest=[AD]+)R / S => CDR ; C(\rest)R / S
- ``IF_SOME bt bf``: Inspect an optional value. - ``IF_SOME bt bf``: Inspect an optional value.
:: ::
:: 'a? : 'S -> 'b : 'S :: option 'a : 'S -> 'b : 'S
iff bt :: [ 'a : 'S -> 'b : 'S] iff bt :: [ 'a : 'S -> 'b : 'S]
bf :: [ 'S -> 'b : 'S] bf :: [ 'S -> 'b : 'S]
> IF_SOME ; C / (Some a) : S => bt ; C / a : S > IF_SOME / (Some a) : S => bt / a : S
> IF_SOME ; C / (None) : S => bf ; C / S > IF_SOME / (None) : S => bf / S
- ``SET_CAR``: Set the first value of a pair. - ``SET_CAR``: Set the first value of a pair.
@ -1621,32 +1643,32 @@ operations.
:: ::
> SET_CA(\rest=[AD]+)R ; C / S => > SET_CA(\rest=[AD]+)R / S =>
{ DUP ; DIP { CAR ; SET_C(\rest)R } ; CDR ; SWAP ; PAIR } ; C / S { DUP ; DIP { CAR ; SET_C(\rest)R } ; CDR ; SWAP ; PAIR } / S
> SET_CD(\rest=[AD]+)R ; C / S => > SET_CD(\rest=[AD]+)R / S =>
{ DUP ; DIP { CDR ; SET_C(\rest)R } ; CAR ; PAIR } ; C / S { DUP ; DIP { CDR ; SET_C(\rest)R } ; CAR ; PAIR } / S
- ``MAP_CAR`` code: Transform the first value of a pair. - ``MAP_CAR`` code: Transform the first value of a pair.
:: ::
> SET_CAR => DUP ; CDR ; SWAP ; code ; CAR ; PAIR > MAP_CAR code => DUP ; CDR ; SWAP ; code ; CAR ; PAIR
- ``MAP_CDR`` code: Transform the first value of a pair. - ``MAP_CDR`` code: Transform the first value of a pair.
:: ::
> SET_CDR => DUP ; CDR ; code ; SWAP ; CAR ; PAIR > MAP_CDR code => DUP ; CDR ; code ; SWAP ; CAR ; PAIR
- ``MAP_C[AD]+R`` code: A syntactic sugar for transforming fields in - ``MAP_C[AD]+R`` code: A syntactic sugar for transforming fields in
nested pairs. nested pairs.
:: ::
> MAP_CA(\rest=[AD]+)R ; C / S => > MAP_CA(\rest=[AD]+)R / S =>
{ DUP ; DIP { CAR ; MAP_C(\rest)R code } ; CDR ; SWAP ; PAIR } ; C / S { DUP ; DIP { CAR ; MAP_C(\rest)R code } ; CDR ; SWAP ; PAIR } / S
> MAP_CD(\rest=[AD]+)R ; C / S => > MAP_CD(\rest=[AD]+)R / S =>
{ DUP ; DIP { CDR ; MAP_C(\rest)R code } ; CAR ; PAIR } ; C / S { DUP ; DIP { CDR ; MAP_C(\rest)R code } ; CAR ; PAIR } / S
IX - Concrete syntax IX - Concrete syntax
-------------------- --------------------
@ -1863,8 +1885,8 @@ Contracts in the system are stored as a piece of code and a global data
storage. The type of the global data of the storage is fixed for each 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 the following 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 ’ret ’global)`` where ``’global`` is the
type of the original global store given on origination. The contract type of the original global store given on origination. The contract
also takes a parameter and returns a value, hence the complete calling also takes a parameter and returns a value, hence the complete calling
convention above. convention above.