diff --git a/docs/alpha/michelson.rst b/docs/alpha/michelson.rst index c9d7895170310fe50b4246530ec311ed6c4cf7fd..64fc3daedbb291e740d670ee77ad26845087af85 100644 --- a/docs/alpha/michelson.rst +++ b/docs/alpha/michelson.rst @@ -1,9 +1,11 @@ Michelson: the language of Smart Contracts in Tezos =================================================== -This specification gives a detailed formal semantics of the Michelson +This specification gives an overview of the Michelson language, and a short explanation of how smart contracts are executed -and interact in the blockchain. +and interact in the blockchain. For a detailed reference to the formal +semantics of the core instructions and the data types of the language, we refer +to the `interactive Michelson reference`_. The language is stack-based, with high level data types and primitives, and strict static type checking. Its design cherry picks traits from @@ -444,1897 +446,24 @@ as well-typed. This is because the implementation uses a simple single pass typechecking algorithm, and does not handle any form of polymorphism. -Core data types and notations +Data types and notations ----------------------------- -- ``string``, ``nat``, ``int`` and ``bytes``: The core primitive - constant types. +The reference to Michelson core data types and notation is now found +in the `interactive Michelson reference`_. -- ``bool``: The type for booleans whose values are ``True`` and - ``False``. - -- ``unit``: The type whose only value is ``Unit``, to use as a - placeholder when some result or parameter is not necessary. For - instance, when the only goal of a contract is to update its storage. - -- ``never``: The empty type. Since ``never`` has no inhabitant, no value of - this type is allowed to occur in a well-typed program. - -- ``list (t)``: A single, immutable, homogeneous linked list, whose - elements are of type ``(t)``, and that we write ``{}`` for the empty - list or ``{ first ; ... }``. In the semantics, we use chevrons to - denote a subsequence of elements. For instance: ``{ head ; }``. - -- ``pair (l) (r)``: A pair of values ``a`` and ``b`` of types ``(l)`` - and ``(r)``, that we write ``(Pair a b)``. - -- ``pair (t{1}) ... (t{n})`` with ``n > 2``: A shorthand for ``pair (t{1}) (pair (t{2}) ... (pair (t{n-1}) (t{n})) ...)``. - -- ``option (t)``: Optional value of type ``(t)`` that we write ``None`` - or ``(Some v)``. - -- ``or (l) (r)``: A union of two types: a value holding either a value - ``a`` of type ``(l)`` or a value ``b`` of type ``(r)``, that we write - ``(Left a)`` or ``(Right b)``. - -- ``set (t)``: Immutable sets of values of type ``(t)`` that we write as - lists ``{ item ; ... }``, of course with their elements unique, and - sorted. - -- ``map (k) (t)``: Immutable maps from keys of type ``(k)`` of values - of type ``(t)`` that we write ``{ Elt key value ; ... }``, with keys - sorted. - -- ``big_map (k) (t)``: Lazily deserialized maps from keys of type - ``(k)`` of values of type ``(t)``. - These maps should be used if you intend to store large amounts of data in a map. - Using ``big_map`` can reduce gas costs significantly compared to standard maps, as data is lazily deserialized. - Note however that individual operations on ``big_map`` have higher gas costs than those over standard maps. - A ``big_map`` also has a lower storage cost than a standard map of the same size, when large keys are used, since only the hash of each key is stored in a ``big_map``. - - A ``big_map`` cannot appear inside another ``big_map``. - See the section on :ref:`operations on big maps ` for a description of the syntax of values of type ``big_map (k) (t)`` and available operations. - -Core instructions ------------------ - -Control structures -~~~~~~~~~~~~~~~~~~ - -- ``FAILWITH``: Explicitly abort the current program. - -:: - - :: 'a : \_ -> \_ - -This special instruction aborts the current program exposing the top -element of the stack in its error message (first rule below). It makes -the output useless since all subsequent instructions will simply -ignore their usual semantics to propagate the failure up to the main -result (second rule below). Its type is thus completely generic. - -:: - - > FAILWITH / a : _ => [FAILED] - > _ / [FAILED] => [FAILED] - -- ``{}``: Empty sequence. - -:: - - :: 'A -> 'A - - > {} / SA => SA - -- ``{ I ; C }``: Sequence. - -:: - - :: 'A -> 'C - iff I :: [ 'A -> 'B ] - C :: [ 'B -> 'C ] - - > I ; C / SA => SC - where I / SA => SB - and C / SB => SC - -- ``IF bt bf``: Conditional branching. - -:: - - :: bool : 'A -> 'B - iff bt :: [ 'A -> 'B ] - bf :: [ 'A -> 'B ] - - > IF bt bf / True : S => bt / S - > IF bt bf / False : S => bf / S - -- ``LOOP body``: A generic loop. - -:: - - :: bool : 'A -> 'A - iff body :: [ 'A -> bool : 'A ] - - > LOOP body / True : S => body ; LOOP body / S - > LOOP body / False : S => S - -- ``LOOP_LEFT body``: A loop with an accumulator. - -:: - - :: (or 'a 'b) : 'A -> 'b : 'A - iff body :: [ 'a : 'A -> (or 'a 'b) : 'A ] - - > LOOP_LEFT body / (Left a) : S => body ; LOOP_LEFT body / a : S - > LOOP_LEFT body / (Right b) : S => b : S - -- ``DIP code``: Runs code protecting the top element of the stack. - -:: - - :: 'b : 'A -> 'b : 'C - iff code :: [ 'A -> 'C ] - - > DIP code / x : S => x : S' - where code / S => S' - -- ``DIP n code``: Runs code protecting the ``n`` topmost elements of - the stack. In particular, ``DIP 0 code`` is equivalent to ``code`` - and ``DIP 1 code`` is equivalent to ``DIP code``. - -:: - - :: 'a{1} : ... : 'a{n} : 'A -> 'a{1} : ... : 'a{n} : 'B - iff code :: [ 'A -> 'B ] - - > DIP n code / x{1} : ... : x{n} : S => x{1} : ... : x{n} : S' - where code / S => S' - -- ``EXEC``: Execute a function from the stack. - -:: - - :: 'a : lambda 'a 'b : 'C -> 'b : 'C - - > EXEC / a : f : S => r : S - where f / a : [] => r : [] - -- ``APPLY``: Partially apply a tuplified function from the stack. - Values that are not both pushable and storable - (values of type ``operation``, ``contract _`` and ``big map _ _``) - cannot be captured by ``APPLY`` (cannot appear in ``'a``). - -:: - - :: 'a : lambda (pair 'a 'b) 'c : 'C -> lambda 'b 'c : 'C - - > APPLY / a : f : S => { PUSH 'a a ; PAIR ; f } : S - -Stack operations -~~~~~~~~~~~~~~~~ - -- ``DROP``: Drop the top element of the stack. - -:: - - :: _ : 'A -> 'A - - > DROP / _ : S => S - -- ``DROP n``: Drop the `n` topmost elements of the stack. In - particular, ``DROP 0`` is a noop and ``DROP 1`` is equivalent to - ``DROP``. - -:: - - :: 'a{1} : ... : 'a{n} : 'A -> 'A - - > DROP n / x{1} : ... : x{n} : S => S - -- ``DUP``: Duplicate the top element of the stack. - -:: - - :: 'a : 'A -> 'a : 'a : 'A - - > DUP / x : S => x : x : S - -- ``DUP n``: Duplicate the N-th element of the stack. `DUP 1` is equivalent to `DUP`. `DUP 0` is rejected. - -:: - - DUP 1 :: 'a : 'A -> 'a : 'a : 'A - - DUP (n+1) :: 'a : 'A -> 'b : 'a : 'A - iff DUP n :: 'A -> 'b : 'A - - > DUP 1 / x : S => x : x : S - - > DUP (n+1) / x : S => y : x : S - iff DUP n / S => y : S - - -- ``SWAP``: Exchange the top two elements of the stack. - -:: - - :: 'a : 'b : 'A -> 'b : 'a : 'A - - > SWAP / x : y : S => y : x : S - -- ``DIG n``: Take the element at depth ``n`` of the stack and move it - on top. The element on top of the stack is at depth ``0`` so that - ``DIG 0`` is a no-op and ``DIG 1`` is equivalent to ``SWAP``. - -:: - - :: 'a{1} : ... : 'a{n} : 'b : 'A -> 'b : 'a{1} : ... : 'a{n} : 'A - - > DIG n / x{1} : ... : x{n} : y : S => y : x{1} : ... : x{n} : S - -- ``DUG n``: Place the element on top of the stack at depth ``n``. The - element on top of the stack is at depth ``0`` so that ``DUG 0`` is a - no-op and ``DUG 1`` is equivalent to ``SWAP``. - -:: - - :: 'b : 'a{1} : ... : 'a{n} : 'A -> 'a{1} : ... : 'a{n} : 'b : 'A - - > DUG n / y : x{1} : ... : x{n} : S => x{1} : ... : x{n} : y : S - -- ``PUSH 'a x``: Push a constant value of a given type onto the stack. - -:: - - :: 'A -> 'a : 'A - iff x :: 'a - - > PUSH 'a x / S => x : S - -- ``LAMBDA 'a 'b code``: Push a lambda with the given parameter type `'a` and return - type `'b` onto the stack. - -:: - - :: 'A -> (lambda 'a 'b) : 'A - - > LAMBDA _ _ code / S => code : S - -Generic comparison -~~~~~~~~~~~~~~~~~~ - -Comparison only works on a class of types that we call comparable. A -``COMPARE`` operation is defined in an ad hoc way for each comparable -type, but the result of compare is always an ``int``, which can in turn -be checked in a generic manner using the following combinators. The -result of ``COMPARE`` is ``0`` if the top two elements of the stack are -equal, negative if the first element in the stack is less than the -second, and positive otherwise. - -- ``EQ``: Checks that the top element of the stack is equal to zero. - -:: - - :: int : 'S -> bool : 'S - - > EQ / 0 : S => True : S - > EQ / v : S => False : S - iff v <> 0 - -- ``NEQ``: Checks that the top element of the stack is not equal to zero. - -:: - - :: int : 'S -> bool : 'S - - > NEQ / 0 : S => False : S - > NEQ / v : S => True : S - iff v <> 0 - -- ``LT``: Checks that the top element of the stack is less than zero. - -:: - - :: int : 'S -> bool : 'S - - > LT / v : S => True : S - iff v < 0 - > LT / v : S => False : S - iff v >= 0 - -- ``GT``: Checks that the top element of the stack is greater than zero. - -:: - - :: int : 'S -> bool : 'S - - > GT / v : S => C / True : S - iff v > 0 - > GT / v : S => C / False : S - iff v <= 0 - -- ``LE``: Checks that the top element of the stack is less than or equal to - zero. - -:: - - :: int : 'S -> bool : 'S - - > LE / v : S => True : S - iff v <= 0 - > LE / v : S => False : S - iff v > 0 - -- ``GE``: Checks that the top of the stack is greater than or equal to - zero. - -:: - - :: int : 'S -> bool : 'S - - > GE / v : S => True : S - iff v >= 0 - > GE / v : S => False : S - iff v < 0 - -Operations ----------- - -Operations on unit -~~~~~~~~~~~~~~~~~~ - -- ``UNIT``: Push a unit value onto the stack. - -:: - - :: 'A -> unit : 'A - - > UNIT / S => Unit : S - -- ``COMPARE``: Unit comparison - -:: - - :: unit : unit : 'S -> int : 'S - - > COMPARE / Unit : Unit : S => 0 : S - -Operations on type never -~~~~~~~~~~~~~~~~~~~~~~~~ - -The type ``never`` is the type of forbidden values. The most prominent -scenario in which ``never`` is used is when implementing a contract -template with no additional entrypoint. A contract template defines a set -of basic entrypoints, and its ``parameter`` declaration contains a type -variable for additional entrypoints in some branch of an union type, or -wrapped inside an option type. Letting this type variable be ``never`` in -a particular implementation indicates that the contract template has not -been extended, and turns the branch in the code that processes the -additional entrypoints into a forbidden branch. - -Values of type ``never`` cannot occur in a well-typed program. However, -they can be abstracted in the ``parameter`` declaration of a contract---or -by using the ``LAMBDA`` operation---thus indicating that the corresponding -branches in the code are forbidden. The type ``never`` also plays a role -when introducing values of union or option type with ``LEFT never``, -``RIGHT never``, or ``NONE never``. In such cases, the created values can -be inspected with the operations ``IF_LEFT``, ``IF_RIGHT``, or -``IF_NONE``, and the corresponding branches in the code are forbidden -branches. - -- ``NEVER``: Close a forbidden branch. - -:: - - :: never : 'A -> 'B - -- ``COMPARE``: Trivial comparison on type ``never`` - -:: - - :: never : never : 'S -> int : 'S - - -Operations on booleans -~~~~~~~~~~~~~~~~~~~~~~ - -- ``OR`` - -:: - - :: bool : bool : 'S -> bool : 'S - - > OR / x : y : S => (x | y) : S - -- ``AND`` - -:: - - :: bool : bool : 'S -> bool : 'S - - > AND / x : y : S => (x & y) : S - -- ``XOR`` - -:: - - :: bool : bool : 'S -> bool : 'S - - > XOR / x : y : S => (x ^ y) : S - -- ``NOT`` - -:: - - :: bool : 'S -> bool : 'S - - > NOT / x : S => ~x : S - -- ``COMPARE``: Boolean comparison - -:: - - :: bool : bool : 'S -> int : 'S - - > COMPARE / False : False : S => 0 : S - > COMPARE / False : True : S => -1 : S - > COMPARE / True : False : S => 1 : S - > COMPARE / True : True : S => 0 : S - -Operations on integers and natural numbers -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -Integers and naturals are arbitrary-precision, meaning that the only size -limit is gas. - -- ``NEG`` - -:: - - :: int : 'S -> int : 'S - :: nat : 'S -> int : 'S - - > NEG / x : S => -x : S - -- ``ABS`` - -:: - - :: int : 'S -> nat : 'S - - > ABS / x : S => abs (x) : S - -- ``ISNAT`` - -:: - - :: int : 'S -> option nat : 'S - - > ISNAT / x : S => Some (x) : S - iff x >= 0 - - > ISNAT / x : S => None : S - iff x < 0 - -- ``INT`` - -:: - - :: nat : 'S -> int : 'S - - > INT / x : S => x : S - -- ``ADD`` - -:: - - :: int : int : 'S -> int : 'S - :: int : nat : 'S -> int : 'S - :: nat : int : 'S -> int : 'S - :: nat : nat : 'S -> nat : 'S - - > ADD / x : y : S => (x + y) : S - -- ``SUB`` - -:: - - :: int : int : 'S -> int : 'S - :: int : nat : 'S -> int : 'S - :: nat : int : 'S -> int : 'S - :: nat : nat : 'S -> int : 'S - - > SUB / x : y : S => (x - y) : S - -- ``MUL`` - -:: - - :: int : int : 'S -> int : 'S - :: int : nat : 'S -> int : 'S - :: nat : int : 'S -> int : 'S - :: nat : nat : 'S -> nat : 'S - - > MUL / x : y : S => (x * y) : S - -- ``EDIV``: Perform Euclidean division - -:: - - :: int : int : 'S -> option (pair int nat) : 'S - :: int : nat : 'S -> option (pair int nat) : 'S - :: nat : int : 'S -> option (pair int nat) : 'S - :: nat : nat : 'S -> option (pair nat nat) : 'S - - > EDIV / x : 0 : S => None : S - > EDIV / x : y : S => Some (Pair (x / y) (x % y)) : S - iff y <> 0 - -Bitwise logical operators are also available on unsigned integers. - -- ``OR`` - -:: - - :: nat : nat : 'S -> nat : 'S - - > OR / x : y : S => (x | y) : S - -- ``AND``: (also available when the top operand is signed) - -:: - - :: nat : nat : 'S -> nat : 'S - :: int : nat : 'S -> nat : 'S - - > AND / x : y : S => (x & y) : S - -- ``XOR`` - -:: - - :: nat : nat : 'S -> nat : 'S - - > XOR / x : y : S => (x ^ y) : S - -- ``NOT``: Two's complement - -:: - - :: nat : 'S -> int : 'S - :: int : 'S -> int : 'S - - > NOT / x : S => ~x : S - - -The return type of ``NOT`` is an ``int`` and not a ``nat``. This is -because the sign is also negated. The resulting integer is computed -using two's complement. For instance, the boolean negation of ``0`` is -``-1``. To get a natural back, a possibility is to use ``AND`` with an -unsigned mask afterwards. - - -- ``LSL`` - -:: - - :: nat : nat : 'S -> nat : 'S - - > LSL / x : s : S => (x << s) : S - iff s <= 256 - > LSL / x : s : S => [FAILED] - iff s > 256 - -- ``LSR`` - -:: - - :: nat : nat : 'S -> nat : 'S - - > LSR / x : s : S => (x >> s) : S - iff s <= 256 - > LSR / x : s : S => [FAILED] - iff s > 256 - -- ``COMPARE``: Integer/natural comparison - -:: - - :: int : int : 'S -> int : 'S - :: nat : nat : 'S -> int : 'S - - > COMPARE / x : y : S => -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 -~~~~~~~~~~~~~~~~~~~~~ - -Strings are mostly used for naming things without having to rely on -external ID databases. They are restricted to the printable subset of -7-bit ASCII, plus some escaped characters (see section on -constants). So what can be done is basically use string constants as -is, concatenate or splice them, and use them as keys. - - -- ``CONCAT``: String concatenation. - -:: - - :: string : string : 'S -> string : 'S - - > CONCAT / s : t : S => (s ^ t) : S - - :: string list : 'S -> string : 'S - - > CONCAT / {} : S => "" : S - > CONCAT / { s ; } : S => (s ^ r) : S - where CONCAT / { } : S => r : S - -- ``SIZE``: number of characters in a string. - -:: - - :: string : 'S -> nat : 'S - -- ``SLICE``: String access. - -:: - - :: nat : nat : string : 'S -> option string : 'S - - > SLICE / offset : length : s : S => Some ss : S - where ss is the substring of s at the given offset and of the given length - iff offset and (offset + length) are in bounds - > SLICE / offset : length : s : S => None : S - iff offset or (offset + length) are out of bounds - -- ``COMPARE``: Lexicographic comparison. - -:: - - :: string : string : 'S -> int : 'S - - > COMPARE / s : t : S => -1 : S - iff s < t - > COMPARE / s : t : S => 0 : S - iff s = t - > COMPARE / s : t : S => 1 : S - iff s > t - -Operations on pairs and right combs -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -The type ``pair l r`` is the type of binary pairs composed of a left -element of type ``l`` and a right element of type ``r``. A value of -type ``pair l r`` is written ``Pair x y`` where ``x`` is a value of -type ``l`` and ``y`` is a value of type ``r``. - -To build tuples of length greater than 2, right combs have specific -optimized operations. For any ``n > 2``, the compact notations ``pair -t{0} t{1} ... t{n-2} t{n-1}`` is provided for the type of right combs -``pair t{0} (pair t{1} ... (pair t{n-2} t{n-1}) ...)``. Similarly, the -compact notation ``Pair x{0} x{1} ... x{n-2} x{n-1}`` is provided for -the right-comb value ``Pair x{0} (Pair x{1} ... (Pair x{n-2} x{n-1}) -...)``. Right-comb values can also be written using sequences; ``Pair -x{0} x{1} ... x{n-2} x{n-1}`` can be written ``{x{0}; x{1}; ...; x{n-2}; x{n-1}}``. - -- ``PAIR``: Build a binary pair from the stack's top two elements. - -:: - - :: 'a : 'b : 'S -> pair 'a 'b : 'S - - > PAIR / x : y : S => Pair x y : S - -- ``PAIR n``: Fold ``n`` values on the top of the stack in a right comb. - ``PAIR 0`` and ``PAIR 1`` are rejected. ``PAIR 2`` is equivalent to ``PAIR``. - -:: - - PAIR 2 :: 'a : 'b : 'S -> pair 'a 'b : 'S - PAIR (k+1) :: 'x : 'S -> pair 'x 'y : 'T - iff PAIR k :: 'S -> 'y : 'T - - Or equivalently, for n >= 2, - PAIR n :: 'a{0} : ... : 'a{n-1} : 'A -> pair 'a{0} ... 'a{n-1} : 'A - - > PAIR 2 / x : y : S => Pair x y : S - > PAIR (k+1) / x : S => Pair x y : T - iff PAIR k / S => y : T - - Or equivalently, for n >= 2, - > PAIR n / x{0} : ... : x{n-1} : S => Pair x{0} ... x{n-1} : S - -- ``UNPAIR``: Split a pair into its components. - -:: - - :: pair 'a 'b : 'S -> 'a : 'b : 'S - - > UNPAIR / Pair a b : S => a : b : S - - -- ``UNPAIR n``: Unfold ``n`` values from a right comb on the top of the stack. ``UNPAIR 0`` and ``UNPAIR 1`` are rejected. ``UNPAIR 2`` is equivalent to ``UNPAIR``. - -:: - - UNPAIR 2 :: pair 'a 'b : 'A -> 'a : 'b : 'A - UNPAIR (k+1) :: pair 'a 'b : 'A -> 'a : 'B - iff UNPAIR k :: 'b : 'A -> 'B - - Or equivalently, for n >= 2, - UNPAIR n :: pair 'a{0} ... 'a{n-1} : S -> 'a{0} : ... : 'a{n-1} : S - - > UNPAIR 2 / Pair x y : S => x : y : S - > UNPAIR (k+1) / Pair x y : SA => x : SB - iff UNPAIR k / y : SA => SB - - Or equivalently, for n >= 2, - > UNPAIR n / Pair x{0} ... x{n-1} : S => x{0} : ... : x{n-1} : S - -- ``CAR``: Access the left part of a pair. - -:: - - :: pair 'a _ : 'S -> 'a : 'S - - > CAR / Pair x _ : S => x : S - -- ``CDR``: Access the right part of a pair. - -:: - - :: pair _ 'b : 'S -> 'b : 'S - - > CDR / Pair _ y : S => y : S - -- ``GET k``: Access an element or a sub comb in a right comb. - - The nodes of a right comb of size ``n`` are canonically numbered as follows: - -:: - - 0 - / \ - 1 2 - / \ - 3 4 - / \ - 5 ... - 2n-2 - / \ - 2n-1 2n - - -Or in plain English: - - - The root is numbered with 0, - - The left child of the node numbered by ``k`` is numbered by ``k+1``, and - - The right child of the node numbered by ``k`` is numbered by ``k+2``. - -The ``GET k`` instruction accesses the node numbered by ``k``. In -particular, for a comb of size ``n``, the ``n-1`` first elements are -accessed by ``GET 1``, ``GET 3``, ..., and ``GET (2n-1)`` and the last -element is accessed by ``GET (2n)``. - -:: - - GET 0 :: 'a : 'S -> 'a : 'S - GET 1 :: pair 'x _ : 'S -> 'x : 'S - GET (k+2) :: pair _ 'y : 'S -> 'z : 'S - iff GET k :: 'y : 'S -> 'z : 'S - - Or equivalently, - GET 0 :: 'a : 'S -> 'a : 'S - GET (2k) :: pair 'a{0} ... 'a{k-1} 'a{k} : 'S -> 'a{k} : 'S - GET (2k+1) :: pair 'a{0} ... 'a{k} 'a{k+1} : 'S -> 'a{k} : 'S - - > GET 0 / x : S => x : S - > GET 1 / Pair x _ : S => x : S - > GET (k+2) / Pair _ y : S => GET k / y : S - - Or equivalently, - > GET 0 / x : S => x : S - > GET (2k) / Pair x{0} ... x{k-1} x{k} : 'S -> x{k} : 'S - > GET (2k+1) / Pair x{0} ... x{k} x{k+1} : 'S -> x{k} : 'S - - -- ``UPDATE k``: Update an element or a sub comb in a right comb. The topmost stack element is the new value to insert in the comb, the second stack element is the right comb to update. The meaning of ``k`` is the same as for the ``GET k`` instruction. - -:: - - UPDATE 0 :: 'a : 'b : 'S -> 'a : 'S - UPDATE 1 :: 'a2 : pair 'a1 'b : 'S -> pair 'a2 'b : 'S - UPDATE (k+2) :: 'c : pair 'a 'b1 : 'S -> pair 'a 'b2 : 'S - iff UPDATE k :: 'c : 'b1 : 'S -> 'b2 : 'S - - Or equivalently, - UPDATE 0 :: 'a : 'b : 'S -> 'a : 'S - UPDATE (2k) :: 'c : pair 'a{0} ... 'a{k-1} 'a{k} : 'S -> pair 'a{0} ... 'a{k-1} 'c : 'S - UPDATE (2k+1) :: 'c : pair 'a{0} ... 'a{k} 'a{k+1} : 'S -> pair 'a{0} ... 'a{k-1} 'c 'a{k+1} : 'S - - > UPDATE 0 / x : _ : S => x : S - > UPDATE 1 / x2 : Pair x1 y : S => Pair x2 y : S - > UPDATE (k+2) / z : Pair x y1 : S => Pair x y2 : S - iff UPDATE k / z : y1 : S => y2 : S - - Or equivalently, - > UPDATE 0 / x : _ : S => x : S - > UPDATE (2k) / z : Pair x{0} ... x{k-1} x{k} : 'S => Pair x{0} ... x{k-1} z : 'S - > UPDATE (2k+1) / z : Pair x{0} ... x{k-1} x{k} x{k+1} : 'S => Pair x{0} ... x{k-1} z x{k+1} : 'S - -- ``COMPARE``: Lexicographic comparison. - -:: - - :: pair 'a 'b : pair 'a 'b : 'S -> int : 'S - - > COMPARE / (Pair sa sb) : (Pair ta tb) : S => -1 : S - iff COMPARE / sa : ta : S => -1 : S - > COMPARE / (Pair sa sb) : (Pair ta tb) : S => 1 : S - iff COMPARE / sa : ta : S => 1 : S - > COMPARE / (Pair sa sb) : (Pair ta tb) : S => r : S - iff COMPARE / sa : ta : S => 0 : S - COMPARE / sb : tb : S => r : S - -Operations on sets -~~~~~~~~~~~~~~~~~~ - -- ``EMPTY_SET 'elt``: Build a new, empty set for elements of a given - type. - - The ``'elt`` type must be comparable (the ``COMPARE`` - primitive must be defined over it). - -:: - - :: 'S -> set 'elt : 'S - - > EMPTY_SET _ / S => {} : S - -- ``MEM``: Check for the presence of an element in a set. - -:: - - :: 'elt : set 'elt : 'S -> bool : 'S - - > MEM / x : {} : S => false : S - > MEM / x : { hd ; } : S => r : S - iff COMPARE / x : hd : [] => 1 : [] - where MEM / x : { } : S => r : S - > MEM / x : { hd ; } : S => true : S - iff COMPARE / x : hd : [] => 0 : [] - > MEM / x : { hd ; } : S => false : S - iff COMPARE / x : hd : [] => -1 : [] - -- ``UPDATE``: Inserts or removes an element in a set, replacing a - previous value. - -:: - - :: 'elt : bool : set 'elt : 'S -> set 'elt : 'S - - > UPDATE / x : false : {} : S => {} : S - > UPDATE / x : true : {} : S => { x } : S - > UPDATE / x : v : { hd ; } : S => { hd ; } : S - iff COMPARE / x : hd : [] => 1 : [] - where UPDATE / x : v : { } : S => { } : S - > UPDATE / x : false : { hd ; } : S => { } : S - iff COMPARE / x : hd : [] => 0 : [] - > UPDATE / x : true : { hd ; } : S => { hd ; } : S - iff COMPARE / x : hd : [] => 0 : [] - > UPDATE / x : false : { hd ; } : S => { hd ; } : S - iff COMPARE / x : hd : [] => -1 : [] - > UPDATE / x : true : { hd ; } : S => { x ; hd ; } : S - iff COMPARE / x : hd : [] => -1 : [] - -- ``ITER body``: Apply the body expression to each element of a set. - The body sequence has access to the stack. - -:: - - :: (set 'elt) : 'A -> 'A - iff body :: [ 'elt : 'A -> 'A ] - - > ITER body / {} : S => S - > ITER body / { hd ; } : S => ITER body / { } : S' - iff body / hd : S => S' - - -- ``SIZE``: Get the cardinality of the set. - -:: - - :: set 'elt : 'S -> nat : 'S - - > SIZE / {} : S => 0 : S - > SIZE / { _ ; } : S => 1 + s : S - where SIZE / { } : S => s : S - -Operations on maps -~~~~~~~~~~~~~~~~~~ - -- ``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 - be defined over it). - -:: - - :: 'S -> map 'key 'val : 'S - - > EMPTY_MAP _ _ / S => {} : S - - -- ``GET``: Access an element in a map, returns an optional value to be - checked with ``IF_SOME``. - -:: - - :: 'key : map 'key 'val : 'S -> option 'val : 'S - - > GET / x : {} : S => None : S - > GET / x : { Elt k v ; } : S => opt_y : S - iff COMPARE / x : k : [] => 1 : [] - where GET / x : { } : S => opt_y : S - > GET / x : { Elt k v ; } : S => Some v : S - iff COMPARE / x : k : [] => 0 : [] - > GET / x : { Elt k v ; } : S => None : S - iff COMPARE / x : k : [] => -1 : [] - -- ``MEM``: Check for the presence of a binding for a key in a map. - -:: - - :: 'key : map 'key 'val : 'S -> bool : 'S - - > MEM / x : {} : S => false : S - > MEM / x : { Elt k v ; } : S => r : S - iff COMPARE / x : k : [] => 1 : [] - where MEM / x : { } : S => r : S - > MEM / x : { Elt k v ; } : S => true : S - iff COMPARE / x : k : [] => 0 : [] - > MEM / x : { Elt k v ; } : S => false : S - iff COMPARE / x : k : [] => -1 : [] - -- ``UPDATE``: Assign or remove an element in a map. - -:: - - :: 'key : option 'val : map 'key 'val : 'S -> map 'key 'val : 'S - - > UPDATE / x : None : {} : S => {} : S - > UPDATE / x : Some y : {} : S => { Elt x y } : S - > UPDATE / x : opt_y : { Elt k v ; } : S => { Elt k v ; } : S - iff COMPARE / x : k : [] => 1 : [] - where UPDATE / x : opt_y : { } : S => { } : S - > UPDATE / x : None : { Elt k v ; } : S => { } : S - iff COMPARE / x : k : [] => 0 : [] - > UPDATE / x : Some y : { Elt k v ; } : S => { Elt k y ; } : S - iff COMPARE / x : k : [] => 0 : [] - > UPDATE / x : None : { Elt k v ; } : S => { Elt k v ; } : S - iff COMPARE / x : k : [] => -1 : [] - > UPDATE / x : Some y : { Elt k v ; } : S => { Elt x y ; Elt k v ; } : S - iff COMPARE / x : k : [] => -1 : [] - -- ``GET_AND_UPDATE``: A combination of the ``GET`` and ``UPDATE`` instructions. - -:: - - :: 'key : option 'val : map 'key 'val : 'S -> option 'val : map 'key 'val : 'S - -This instruction is similar to ``UPDATE`` but it also returns the -value that was previously stored in the ``map`` at the same key as -``GET`` would. - -:: - - > GET_AND_UPDATE / x : None : {} : S => None : {} : S - > GET_AND_UPDATE / x : Some y : {} : S => None : { Elt x y } : S - > GET_AND_UPDATE / x : opt_y : { Elt k v ; } : S => opt_y' : { Elt k v ; } : S - iff COMPARE / x : k : [] => 1 : [] - where GET_AND_UPDATE / x : opt_y : { } : S => opt_y' : { } : S - > GET_AND_UPDATE / x : None : { Elt k v ; } : S => Some v : { } : S - iff COMPARE / x : k : [] => 0 : [] - > GET_AND_UPDATE / x : Some y : { Elt k v ; } : S => Some v : { Elt k y ; } : S - iff COMPARE / x : k : [] => 0 : [] - > GET_AND_UPDATE / x : None : { Elt k v ; } : S => None : { Elt k v ; } : S - iff COMPARE / x : k : [] => -1 : [] - > GET_AND_UPDATE / x : Some y : { Elt k v ; } : S => None : { Elt x y ; Elt k v ; } : S - iff COMPARE / x : k : [] => -1 : [] - -- ``MAP body``: Apply the body expression to each element of a map. The - body sequence has access to the stack. - -:: - - :: (map 'key 'val) : 'A -> (map 'key 'b) : 'A - iff body :: [ (pair 'key 'val) : 'A -> 'b : 'A ] - - > MAP body / {} : S => {} : S - > MAP body / { Elt k v ; } : S => { Elt k v' ; } : S'' - where body / Pair k v : S => v' : S' - and MAP body / { } : S' => { } : S'' - -- ``ITER body``: Apply the body expression to each element of a map. - The body sequence has access to the stack. - -:: - - :: (map 'elt 'val) : 'A -> 'A - iff body :: [ (pair 'elt 'val : 'A) -> 'A ] - - > ITER body / {} : S => S - > ITER body / { Elt k v ; } : S => ITER body / { } : S' - iff body / (Pair k v) : S => S' - -- ``SIZE``: Get the cardinality of the map. - -:: - - :: map 'key 'val : 'S -> nat : 'S - - > SIZE / {} : S => 0 : S - > SIZE / { _ ; } : S => 1 + s : S - where SIZE / { } : S => s : S - - -Operations on ``big_maps`` -~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. _OperationsOnBigMaps_alpha: - -Big maps have three possible representations. A map literal is always -a valid representation for a big map. Big maps can also be represented -by integers called big-map identifiers. Finally, big maps can be -represented as pairs of a big-map identifier (an integer) and a -big-map diff (written in the same syntax as a map whose values are -options). - -So for example, ``{ Elt "bar" True ; Elt "foo" False }``, ``42``, and -``Pair 42 { Elt "foo" (Some False) }`` are all valid representations -of type ``big_map string bool``. - -The behavior of big-map operations is the same as if they were normal -maps, except that under the hood, the elements are loaded and -deserialized on demand. - -- ``EMPTY_BIG_MAP 'key 'val``: Build a new, empty big map from keys of a - given type to values of another given type. - - The ``'key`` type must be comparable (the ``COMPARE`` primitive must - be defined over it). - -:: - - :: 'S -> map 'key 'val : 'S - -- ``GET``: Access an element in a ``big_map``, returns an optional value to be - checked with ``IF_SOME``. - -:: - - :: 'key : big_map 'key 'val : 'S -> option 'val : 'S - -- ``MEM``: Check for the presence of an element in a ``big_map``. - -:: - - :: 'key : big_map 'key 'val : 'S -> bool : 'S - -- ``UPDATE``: Assign or remove an element in a ``big_map``. - -:: - - :: 'key : option 'val : big_map 'key 'val : 'S -> big_map 'key 'val : 'S - - -- ``GET_AND_UPDATE``: A combination of the ``GET`` and ``UPDATE`` instructions. - -:: - - :: 'key : option 'val : big_map 'key 'val : 'S -> option 'val : big_map 'key 'val : 'S - -This instruction is similar to ``UPDATE`` but it also returns the -value that was previously stored in the ``big_map`` at the same key as -``GET`` would. - - -Operations on optional values -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -- ``SOME``: Pack a value as an optional value. - -:: - - :: 'a : 'S -> option 'a : 'S - - > SOME / v : S => (Some v) : S - -- ``NONE 'a``: The absent optional value. - -:: - - :: 'S -> option 'a : 'S - - > NONE / S => None : S - -- ``IF_NONE bt bf``: Inspect an optional value. - -:: - - :: option 'a : 'A -> 'B - iff bt :: [ 'A -> 'B] - bf :: [ 'a : 'A -> 'B] - - > IF_NONE bt bf / (None) : S => bt / S - > IF_NONE bt bf / (Some a) : S => bf / a : S - -- ``COMPARE``: Optional values comparison - -:: - - :: option 'a : option 'a : 'S -> int : 'S - - > COMPARE / None : None : S => 0 : S - > COMPARE / None : (Some _) : S => -1 : S - > COMPARE / (Some _) : None : S => 1 : S - > COMPARE / (Some a) : (Some b) : S => COMPARE / a : b : S - -Operations on unions -~~~~~~~~~~~~~~~~~~~~ - -- ``LEFT 'b``: Pack a value in a union (left case). - -:: - - :: 'a : 'S -> or 'a 'b : 'S - - > LEFT / v : S => (Left v) : S - -- ``RIGHT 'a``: Pack a value in a union (right case). - -:: - - :: 'b : 'S -> or 'a 'b : 'S - - > RIGHT / v : S => (Right v) : S - -- ``IF_LEFT bt bf``: Inspect a value of a union. - -:: - - :: or 'a 'b : 'A -> 'B - iff bt :: [ 'a : 'A -> 'B] - bf :: [ 'b : 'A -> 'B] - - > IF_LEFT bt bf / (Left a) : S => bt / a : S - > IF_LEFT bt bf / (Right b) : S => bf / b : S - -- ``COMPARE``: Unions comparison - -:: - - :: or 'a 'b : or 'a 'b : 'S -> int : 'S - - > COMPARE / (Left a) : (Left b) : S => COMPARE / a : b : S - > COMPARE / (Left _) : (Right _) : S => -1 : S - > COMPARE / (Right _) : (Left _) : S => 1 : S - > COMPARE / (Right a) : (Right b) : S => COMPARE / a : b : S - -Operations on lists -~~~~~~~~~~~~~~~~~~~ - -- ``CONS``: Prepend an element to a list. - -:: - - :: 'a : list 'a : 'S -> list 'a : 'S - - > CONS / a : { } : S => { a ; } : S - -- ``NIL 'a``: The empty list. - -:: - - :: 'S -> list 'a : 'S - - > NIL / S => {} : S - -- ``IF_CONS bt bf``: Inspect a list. - -:: - - :: list 'a : 'A -> 'B - iff bt :: [ 'a : list 'a : 'A -> 'B] - bf :: [ 'A -> 'B] - - > IF_CONS bt bf / { a ; } : S => bt / a : { } : S - > IF_CONS bt bf / {} : S => bf / S - -- ``MAP body``: Apply the body expression to each element of the list. - The body sequence has access to the stack. - -:: - - :: (list 'elt) : 'A -> (list 'b) : 'A - iff body :: [ 'elt : 'A -> 'b : 'A ] - - > MAP body / {} : S => {} : S - > MAP body / { a ; } : S => { b ; } : S'' - where body / a : S => b : S' - and MAP body / { } : S' => { } : S'' - -- ``SIZE``: Get the number of elements in the list. - -:: - - :: list 'elt : 'S -> nat : 'S - - > SIZE / { _ ; } : S => 1 + s : S - where SIZE / { } : S => s : S - > SIZE / {} : S => 0 : S - - -- ``ITER body``: Apply the body expression to each element of a list. - The body sequence has access to the stack. - -:: - - :: (list 'elt) : 'A -> 'A - iff body :: [ 'elt : 'A -> 'A ] - > ITER body / {} : S => S - > ITER body / { a ; } : S => ITER body / { } : S' - iff body / a : S => S' - - -Domain specific data types --------------------------- - -- ``timestamp``: Dates in the real world. - -- ``mutez``: A specific type for manipulating tokens. - -- ``address``: An untyped address (implicit account or smart contract). - -- ``contract 'param``: A contract, with the type of its code, - ``contract unit`` for implicit accounts. - -- ``operation``: An internal operation emitted by a contract. - -- ``key``: A public cryptographic key. - -- ``key_hash``: The hash of a public cryptographic key. - -- ``signature``: A cryptographic signature. - -- ``chain_id``: An identifier for a chain, used to distinguish the test and the main chains. - -- ``bls12_381_g1``, ``bls12_381_g2`` : Points on the BLS12-381 curves G\ :sub:`1`\ and G\ :sub:`2`\ , respectively. - -- ``bls12_381_fr`` : An element of the scalar field F\ :sub:`r`\ , used for scalar multiplication on the BLS12-381 curves G\ :sub:`1`\ and G\ :sub:`2`\ . - -- ``sapling_transaction ms``: A :doc:`Sapling ` transaction - -- ``sapling_state ms``: A :doc:`Sapling ` state - -- ``ticket (t)``: A ticket used to authenticate information of type ``(t)`` on-chain. - -Domain specific operations --------------------------- - -Operations on timestamps -~~~~~~~~~~~~~~~~~~~~~~~~ - -Timestamps can be obtained by the ``NOW`` operation, or retrieved from -script parameters or globals. - -- ``ADD`` Increment / decrement a timestamp of the given number of - seconds. - -:: - - :: timestamp : int : 'S -> timestamp : 'S - :: int : timestamp : 'S -> timestamp : 'S - - > ADD / seconds : nat (t) : S => (seconds + t) : S - > ADD / nat (t) : seconds : S => (t + seconds) : S - -- ``SUB`` Subtract a number of seconds from a timestamp. - -:: - - :: timestamp : int : 'S -> timestamp : 'S - - > SUB / seconds : nat (t) : S => (seconds - t) : S - -- ``SUB`` Subtract two timestamps. - -:: - - :: timestamp : timestamp : 'S -> int : 'S - - > SUB / seconds(t1) : seconds(t2) : S => (t1 - t2) : S - -- ``COMPARE``: Timestamp comparison. - -:: - - :: timestamp : timestamp : 'S -> int : 'S - - > COMPARE / seconds(t1) : seconds(t2) : S => -1 : S - iff t1 < t2 - > COMPARE / seconds(t1) : seconds(t2) : S => 0 : S - iff t1 = t2 - > COMPARE / seconds(t1) : seconds(t2) : S => 1 : S - iff t1 > t2 - - -Operations on Mutez -~~~~~~~~~~~~~~~~~~~ - -Mutez (micro-Tez) are internally represented by a 64 bit signed -integers. There are restrictions to prevent creating a negative amount -of mutez. Operations are limited to prevent overflow and mixing them -with other numerical types by mistake. They are also mandatory checked -for under/overflows. - -- ``ADD`` - -:: - - :: mutez : mutez : 'S -> mutez : 'S - - > ADD / x : y : S => [FAILED] on overflow - > ADD / x : y : S => (x + y) : S - -- ``SUB`` - -:: - - :: mutez : mutez : 'S -> mutez : 'S - - > SUB / x : y : S => [FAILED] - iff x < y - > SUB / x : y : S => (x - y) : S - -- ``MUL`` - -:: - - :: mutez : nat : 'S -> mutez : 'S - :: nat : mutez : 'S -> mutez : 'S - - > MUL / x : y : S => [FAILED] on overflow - > MUL / x : y : S => (x * y) : S - -- ``EDIV`` - -:: - - :: mutez : nat : 'S -> option (pair mutez mutez) : 'S - :: mutez : mutez : 'S -> option (pair nat mutez) : 'S - - > EDIV / x : 0 : S => None - > EDIV / x : y : S => Some (Pair (x / y) (x % y)) : S - iff y <> 0 - -- ``COMPARE``: Mutez comparison - -:: - - :: mutez : mutez : 'S -> int : 'S - - > COMPARE / x : y : S => -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 contracts -~~~~~~~~~~~~~~~~~~~~~~~ - -- ``CREATE_CONTRACT { storage 'g ; parameter 'p ; code ... }``: - Forge a new contract from a literal. - -:: - - :: option key_hash : mutez : 'g : 'S - -> operation : address : 'S - -Originate a contract based on a literal. The parameters are the -optional delegate, the initial amount taken from the current -contract, and the initial storage of the originated contract. -The contract is returned as a first class value (to be dropped, passed -as parameter or stored). The ``CONTRACT 'p`` instruction will fail -until it is actually originated. - -- ``TRANSFER_TOKENS``: Forge a transaction. - -:: - - :: 'p : mutez : contract 'p : 'S -> operation : 'S - -The parameter must be consistent with the one expected by the -contract, unit for an account. - -.. _MichelsonSetDelegate_alpha: - -- ``SET_DELEGATE``: Set or withdraw the contract's delegation. - -:: - - :: option key_hash : 'S -> operation : 'S - -Using this instruction is the only way to modify the delegation of a -smart contract. If the parameter is ``None`` then the delegation of the -current contract is withdrawn; if it is ``Some kh`` where ``kh`` is the -key hash of a registered delegate that is not the current delegate of -the contract, then this operation sets the delegate of the contract to -this registered delegate. The operation fails if ``kh`` is the current -delegate of the contract or if ``kh`` is not a registered delegate. - -- ``BALANCE``: Push the current amount of mutez held by the executing - contract, including any mutez added by the calling transaction. - -:: - - :: 'S -> mutez : 'S - -- ``ADDRESS``: Cast the contract to its address. - -:: - - :: contract _ : 'S -> address : 'S - - > ADDRESS / addr : S => addr : S - -- ``CONTRACT 'p``: Cast the address to the given contract type if possible. - -:: - - :: address : 'S -> option (contract 'p) : 'S - - > CONTRACT / addr : S => Some addr : S - iff addr exists and is a contract of parameter type 'p - > CONTRACT / addr : S => Some addr : S - iff 'p = unit and addr is an implicit contract - > CONTRACT / addr : S => None : S - otherwise - -- ``SOURCE``: Push the contract that initiated the current - transaction, i.e. the contract that paid the fees and - storage cost, and whose manager signed the operation - that was sent on the blockchain. Note that since - ``TRANSFER_TOKENS`` instructions can be chained, - ``SOURCE`` and ``SENDER`` are not necessarily the same. - -:: - - :: 'S -> address : 'S - -- ``SENDER``: Push the contract that initiated the current - internal transaction. It may be the ``SOURCE``, but may - also be different if the source sent an order to an intermediate - smart contract, which then called the current contract. - -:: - - :: 'S -> address : 'S - -- ``SELF``: Push the current contract. - -:: - - :: 'S -> contract 'p : 'S - where contract 'p is the type of the current contract - -Note that ``SELF`` is forbidden in lambdas because it cannot be -type-checked; the type of the contract executing the lambda cannot be -known at the point of type-checking the lambda's body. - -- ``SELF_ADDRESS``: Push the address of the current contract. This is - equivalent to ``SELF; ADDRESS`` except that it is allowed in - lambdas. - -:: - - :: 'S -> address : 'S - -Note that ``SELF_ADDRESS`` inside a lambda returns the address of the -contract executing the lambda, which can be different from the address -of the contract in which the ``SELF_ADDRESS`` instruction is written. - -- ``AMOUNT``: Push the amount of the current transaction. - -:: - - :: 'S -> mutez : 'S - -- ``IMPLICIT_ACCOUNT``: Return a default contract with the given - public/private key pair. Any funds deposited in this contract can - immediately be spent by the holder of the private key. This contract - cannot execute Michelson code and will always exist on the - blockchain. - -:: - - :: key_hash : 'S -> contract unit : 'S - -- ``VOTING_POWER``: Return the voting power of a given contract. This voting power - coincides with the weight of the contract in the voting listings (i.e., the rolls - count) which is calculated at the beginning of every voting period. - -:: - - :: key_hash : 'S -> nat : 'S - -Special operations -~~~~~~~~~~~~~~~~~~ - -- ``NOW``: Push the minimal injection time for the current block, - namely the block whose validation triggered this execution. The - minimal injection time is 60 seconds after the timestamp of the - predecessor block. This value does not change during the execution - of the contract. - -:: - - :: 'S -> timestamp : 'S - -- ``CHAIN_ID``: Push the chain identifier. - -:: - - :: 'S -> chain_id : 'S - -- ``COMPARE``: Chain identifier comparison - -:: - - :: chain_id : chain_id : 'S -> int : 'S - - > COMPARE / x : y : S => -1 : S - iff x < y - > COMPARE / x : y : S => 0 : S - iff x = y - > COMPARE / x : y : S => 1 : S - iff x > y - -- ``LEVEL``: Push the current block level. - -:: - - :: 'S -> nat : 'S - -- ``TOTAL_VOTING_POWER``: Return the total voting power of all contracts. The total - voting power coincides with the sum of the rolls count of every contract in the voting - listings. The voting listings is calculated at the beginning of every voting period. - -:: - - :: 'S -> nat : 'S - -Operations on bytes -~~~~~~~~~~~~~~~~~~~ - -Bytes are used for serializing data, in order to check signatures and -compute hashes on them. They can also be used to incorporate data from -the wild and untyped outside world. - -- ``PACK``: Serializes a piece of data to its optimized - binary representation. - -:: - - :: 'a : 'S -> bytes : 'S - -- ``UNPACK 'a``: Deserializes a piece of data, if valid. - -:: - - :: bytes : 'S -> option 'a : 'S - -- ``CONCAT``: Byte sequence concatenation. - -:: - - :: bytes : bytes : 'S -> bytes : 'S - - > CONCAT / s : t : S => (s ^ t) : S - - :: bytes list : 'S -> bytes : 'S - - > CONCAT / {} : S => 0x : S - > CONCAT / { s ; } : S => (s ^ r) : S - where CONCAT / { } : S => r : S - -- ``SIZE``: size of a sequence of bytes. - -:: - - :: bytes : 'S -> nat : 'S - -- ``SLICE``: Bytes access. - -:: - - :: nat : nat : bytes : 'S -> option bytes : 'S - - > SLICE / offset : length : s : S => Some ss : S - where ss is the substring of s at the given offset and of the given length - iff offset and (offset + length) are in bounds - > SLICE / offset : length : s : S => None : S - iff offset or (offset + length) are out of bounds - -- ``COMPARE``: Lexicographic comparison. - -:: - - :: bytes : bytes : 'S -> int : 'S - - > COMPARE / s : t : S => -1 : S - iff s < t - > COMPARE / s : t : S => 0 : S - iff s = t - > COMPARE / s : t : S => 1 : S - iff s > t - - -Cryptographic primitives -~~~~~~~~~~~~~~~~~~~~~~~~ - -- ``HASH_KEY``: Compute the b58check of a public key. - -:: - - :: key : 'S -> key_hash : 'S - -- ``BLAKE2B``: Compute a cryptographic hash of the value contents using the - Blake2b-256 cryptographic hash function. - -:: - - :: bytes : 'S -> bytes : 'S - -- ``KECCAK``: Compute a cryptographic hash of the value contents using the - Keccak-256 cryptographic hash function. - -:: - - :: bytes : 'S -> bytes : 'S - -- ``SHA256``: Compute a cryptographic hash of the value contents using the - Sha256 cryptographic hash function. - -:: - - :: bytes : 'S -> bytes : 'S - -- ``SHA512``: Compute a cryptographic hash of the value contents using the - Sha512 cryptographic hash function. - -:: - - :: bytes : 'S -> bytes : 'S - -- ``SHA3``: Compute a cryptographic hash of the value contents using the - SHA3-256 cryptographic hash function. - -:: - - :: bytes : 'S -> bytes : 'S - -- ``CHECK_SIGNATURE``: Check that a sequence of bytes has been signed - with a given key. - -:: - - :: key : signature : bytes : 'S -> bool : 'S - -- ``COMPARE``: Key hash, key and signature comparison - -:: - - :: key_hash : key_hash : 'S -> int : 'S - :: key : key : 'S -> int : 'S - :: signature : signature : 'S -> int : 'S - - > COMPARE / x : y : S => -1 : S - iff x < y - > COMPARE / x : y : S => 0 : S - iff x = y - > COMPARE / x : y : S => 1 : S - iff x > y - -BLS12-381 primitives -~~~~~~~~~~~~~~~~~~~~~~~~ - -- ``NEG``: Negate a curve point or field element. - -:: - - :: bls12_381_g1 : 'S -> bls12_381_g1 : 'S - :: bls12_381_g2 : 'S -> bls12_381_g2 : 'S - :: bls12_381_fr : 'S -> bls12_381_fr : 'S - -- ``ADD``: Add two curve points or field elements. - -:: - - :: bls12_381_g1 : bls12_381_g1 : 'S -> bls12_381_g1 : 'S - :: bls12_381_g2 : bls12_381_g2 : 'S -> bls12_381_g2 : 'S - :: bls12_381_fr : bls12_381_fr : 'S -> bls12_381_fr : 'S - -- ``MUL``: Multiply a curve point or field element by a scalar field element. Fr - elements can be built from naturals by multiplying by the unit of Fr using ``PUSH bls12_381_fr 1; MUL``. Note - that the multiplication will be computed using the natural modulo the order - of Fr. - -:: - - :: bls12_381_g1 : bls12_381_fr : 'S -> bls12_381_g1 : 'S - :: bls12_381_g2 : bls12_381_fr : 'S -> bls12_381_g2 : 'S - :: bls12_381_fr : bls12_381_fr : 'S -> bls12_381_fr : 'S - :: nat : bls12_381_fr : 'S -> bls12_381_fr : 'S - :: int : bls12_381_fr : 'S -> bls12_381_fr : 'S - :: bls12_381_fr : nat : 'S -> bls12_381_fr : 'S - :: bls12_381_fr : int : 'S -> bls12_381_fr : 'S - -- ``INT``: Convert a field element to type ``int``. The returned value is always between ``0`` (inclusive) and the order of Fr (exclusive). - -:: - - :: bls12_381_fr : 'S -> int : 'S - -- ``PAIRING_CHECK``: - Verify that the product of pairings of the given list of points is equal to 1 in Fq12. Returns ``true`` if the list is empty. - Can be used to verify if two pairings P1 and P2 are equal by verifying P1 * P2^(-1) = 1. - -:: - - :: list (pair bls12_381_g1 bls12_381_g2) : 'S -> bool : 'S - - -Sapling operations -~~~~~~~~~~~~~~~~~~ - -Please see the :doc:`Sapling integration` page for a more -comprehensive description of the Sapling protocol. - -- ``SAPLING_VERIFY_UPDATE``: verify and apply a transaction on a Sapling state. - -:: - - :: sapling_transaction ms : sapling_state ms : 'S -> option (pair int (sapling_state ms)): 'S - - > SAPLING_VERIFY_UPDATE / t : s : S => Some (Pair b s') : S - iff the transaction t successfully applied on state s resulting - in balance b and an updated state s' - > SAPLING_VERIFY_UPDATE / t : s : S => None : S - iff the transaction t is invalid with respect to the state - -- ``SAPLING_EMPTY_STATE ms``: Pushes an empty state on the stack. - - :: - - :: 'S -> sapling_state ms: 'S - - > SAPLING_EMPTY_STATE ms / S => sapling_state ms : S - with `sapling_state ms` being the empty state (ie. no one can spend tokens from it) - with memo_size `ms` - - -.. _MichelsonTickets_alpha: - -Operations on tickets -~~~~~~~~~~~~~~~~~~~~~ - -The following operations deal with tickets. Tickets are a way for smart-contracts -to authenticate data with respect to a Tezos address. This authentication can -then be used to build composable permission systems. - -A contract can create a ticket from a value and an amount. The ticket, when -inspected reveals the value, the amount, and the address of the ticketer (the contract that created the ticket). It is -impossible for a contract to “forge” a ticket that appears to have been created -by another ticketer. - -The amount is a meta-data that can be used to implement UTXOs. - -Tickets cannot be duplicated using the ``DUP`` instruction. - -For example, a ticket could represent a Non Fungible Token (NFT) or a Unspent -Transaction Output (UTXO) which can then be passed around and behave like a value. -This process can happen without the need to interact with a centralized NFT contract, -simplifying the code. - -- ``TICKET``: Create a ticket with the given content and amount. The ticketer is the address - of `SELF`. - -:: - - :: 'a : nat : 'S -> ticket 'a : 'S - -Type ``'a`` must be comparable (the ``COMPARE`` primitive must be defined over it). - -- ``READ_TICKET``: Retrieve the information stored in a ticket. Also return the ticket. - -:: - - :: ticket 'a : 'S -> pair address 'a nat : ticket 'a : 'S - -- ``SPLIT_TICKET``: Delete the given ticket and create two tickets with the - same content and ticketer as the original, but with the new provided amounts. - (This can be used to easily implement UTXOs.) - Return None iff the ticket's original amount is not equal to the sum of the - provided amounts. - -:: - - :: ticket 'a : (pair nat nat) : 'S -> - option (pair (ticket 'a) (ticket 'a)) : 'S - -- ``JOIN_TICKETS``: The inverse of ``SPLIT_TICKET``. Delete the given tickets and create a ticket with an amount equal to the - sum of the amounts of the input tickets. - (This can be used to consolidate UTXOs.) - Return None iff the input tickets have a different ticketer or content. - -:: - - :: (pair (ticket 'a) (ticket 'a)) : 'S -> - option (ticket 'a) : 'S - - -Removed instructions -~~~~~~~~~~~~~~~~~~~~ - -:ref:`005_babylon` deprecated the following instructions. Because no smart -contract used these on Mainnet before they got deprecated, they have been -removed. The Michelson type-checker will reject any contract using them. - -- ``CREATE_CONTRACT { storage 'g ; parameter 'p ; code ... }``: - Forge a new contract from a literal. - -:: - - :: key_hash : option key_hash : bool : bool : mutez : 'g : 'S - -> operation : address : 'S - -See the documentation of the new ``CREATE_CONTRACT`` instruction. The -first, third, and fourth parameters are ignored. - -- ``CREATE_ACCOUNT``: Forge an account creation operation. - -:: - - :: key_hash : option key_hash : bool : mutez : 'S - -> operation : address : 'S - -Takes as argument the manager, optional delegate, the delegatable flag -and finally the initial amount taken from the currently executed -contract. This instruction originates a contract with two entrypoints; -``%default`` of type ``unit`` that does nothing and ``%do`` of type -``lambda unit (list operation)`` that executes and returns the -parameter if the sender is the contract's manager. - -- ``STEPS_TO_QUOTA``: Push the remaining steps before the contract - execution must terminate. - -:: - - :: 'S -> nat : 'S +Instructions +----------------- +The reference to Michelson instructions is now found in the +`interactive Michelson reference`_. Macros ------ -In addition to the operations above, several extensions have been added +In addition to the instructions, detailed in the +`interactive Michelson reference`_, +several extensions have been added to the language's concrete syntax. If you are interacting with the node via RPC, bypassing the client, which expands away these macros, you will need to desugar them yourself. @@ -3687,3 +1816,5 @@ The language is implemented in OCaml as follows: function is very simple, what we have to check is that we transform a ``Prim ("If", ...)`` into an ``If``, a ``Prim ("Dup", ...)`` into a ``Dup``, etc. + +.. _interactive Michelson reference: https://tezos.gitlab.io/michelson-reference/ diff --git a/docs/introduction/howtorun.rst b/docs/introduction/howtorun.rst index 4c40f8c704700272e7e427527a4f2c6d66597574..ce2eb41d5745940c648dd29888dd121d0665f7fc 100644 --- a/docs/introduction/howtorun.rst +++ b/docs/introduction/howtorun.rst @@ -50,7 +50,7 @@ origination using the ``--delegate`` option: Once the contract is originated, the only way to stop or modify its delegation is by using the ``SET_DELEGATE`` Michelson instruction (see -:ref:`the Michelson documentation` for more +`the Michelson reference `_ for more details).