diff --git a/docs/007/cli-commands.rst b/docs/007/cli-commands.rst deleted file mode 100644 index 40ab0e27ee03db22dbfa788581c40f2700c771ad..0000000000000000000000000000000000000000 --- a/docs/007/cli-commands.rst +++ /dev/null @@ -1,58 +0,0 @@ -.. _cli_commands: -.. _cli_commands_007: - -********************** -Command Line Interface -********************** - -This document is a prettier output of the documentation produced by -the command line client's ``man`` command. You can obtain similar pages -using the following shell commands. - -:: - - tezos-client -protocol ProtoALphaALph man -verbosity 3 - tezos-admin-client man -verbosity 3 - -The rest of this page documents the protocol-dependent tools. -The protocol-independent tools are documented :ref:`here `. - - -.. _client_manual: -.. _client_manual_007: - -Client manual -============= - -.. raw:: html - :file: tezos-client-007.html - - -.. _baker_manual: -.. _baker_manual_007: - -Baker manual -============ - -.. raw:: html - :file: tezos-baker-007.html - - -.. _endorser_manual: -.. _endorser_manual_007: - -Endorser manual -=============== - -.. raw:: html - :file: tezos-endorser-007.html - - -.. _accuser_manual: -.. _accuser_manual_007: - -Accuser manual -============== - -.. raw:: html - :file: tezos-accuser-007.html diff --git a/docs/007/glossary.rst b/docs/007/glossary.rst deleted file mode 100644 index 67adbb4feae28232e3870f985f24b6c4bfb53a53..0000000000000000000000000000000000000000 --- a/docs/007/glossary.rst +++ /dev/null @@ -1,159 +0,0 @@ -Glossary -======== - -This glossary is divided in two sections, the first one concerns Tezos, and -the second one concerns the Alpha protocol, which is the current -`economic protocol`_. - -Tezos ------ - -.. include:: ../shell/glossary.rst.h - -Protocol Alpha --------------- - -_`Accuser` - When a node_ attempts to inject several incompatible blocks (or when it tries - to abuse the network in another similar way), another node_ can make an - accusation: show evidence of attempted abuse. The node_ making the accusation - is the accuser. - - The accuser is awarded some funds from the baking_ deposit of the accused. - - Using the tools provided by Nomadic Labs, accusation is handled by a - separate binary. - -_`Account` - An account is a unique identifier within protocol Alpha. There are different - kinds of accounts (see `Originated account`_ and `Implicit account`_). - - In the Context_, each account is associated with a balance (an amount of - tez available). - -_`Baker` - When a node_ creates a new block_, it is the baker of this block_. - Baking_ rights are distributed to different accounts based on their - available balance. Only a node_ that handles an account_ with baking_ rights - is allowed to bake; blocks created by another node_ are invalid. - The baker selects transactions from the mempool_ to be included in the block_ it bakes. - - Using the tools provided by Nomadic Labs, baking_ is handled by a - separate binary. - -_`Baking`/_`Endorsing rights` - A delegate_ is allowed to bake/endorse a block_ if he holds the - baking/endorsing right for that block_. At the start of a Cycle_, - baking and endorsing rights are computed for all the block_ heights in the - cycle_, based on the proportion of Rolls owned by each accounts. - - For each block_ height, there are several accounts that are allowed to bake. - These different accounts are given different Priorities. - - For each block_ height, there are several accounts that are allowed to - endorse. There can be multiple endorsements per block_. - -_`Contract` - See account_. - -_`Cycle` - A cycle is a set of consecutive blocks. E.g., cycle 12 started at block_ - height 49152 and ended at block_ height 53248. - - Cycles are used as a unit of “time” in the block_ chain. For example, the - different phases in the amendment voting procedures are defined based on - cycles. - -_`Delegate` - An `Implicit account`_ to which an account_ has delegated their baking_ and - `endorsing rights`_. The baking_ rights and `endorsing rights`_ are - calculated based on the total balance of tez that an account_ has been - delegated to. - -_`Delegation` - An operation_ in which an account_ balance is lent to a - delegate_. This increases the delegate_'s rolls and consequently - its Baking_ rights. The delegate_ does not control the funds from - the account_. - -_`Double baking` - When a baker_ signs two different blocks at the same height, it is called - double baking. Double baking is detrimental to the network and might be - indicative of an attempt to double spend. As such, it is punished by the - network: an accuser_ can provide proof of the double baking to be awarded - part of the baker_'s deposit. - -_`Endorser` - When a block_ is created and propagated on the network, nodes that have - `endorsing rights`_ for the matching block_ height can emit an endorsement - operation_. The accounts that emit the block_ are the endorsers of the block_. - Endorsement operations_ are included in the next block_. - - Using the tools provided by Nomadic Labs, endorsement is handled by a - separate binary. - -_`Gas` - A measure of the number of elementary operations_ performed during - the execution of a `smart contract`_. Gas is used to measure how - much computing power is used to execute a `smart contract`_. - -_`Implicit account` - An account_ that is linked to a public key. Contrary to a `smart - contract`_, an `Implicit account`_ cannot include a script and it - cannot reject incoming transactions. - - If registered, an `Implicit account`_ can act as a delegate_. - - The address of an `Implicit account`_ always starts with the - letters `tz` followed by `1`, `2` or `3` (depending on the - signature scheme) and finally the hash of the public key. - -.. _glossary_michelson: -.. _glossary_michelson_007: - -Michelson - The built-in language used by a `smart contract`_. - -_`Operations` - In protocol Alpha, the main operations are transactions (to transfer funds - or to execute smart contracts), accusations, activations, delegations, - endorsements and originations. - -_`Originated account` - See `smart contract`_. - -_`Origination` - An operation_ to create a `smart contract`_. - -_`Priority` - A rank of different baking_ rights. Each rank corresponds to a time span. A - baker_ with baking_ rights at a given priority is only allowed to bake during - the priority's corresponding time span. Baking_ outside of one's designated - priority, results in an invalid block_. - -_`Roll` - An amount of tez (e.g., 8000ꜩ) serving as a unit to determine delegates' - baking_ rights in a cycle_. A delegate_ with twice as many rolls as another - will be given twice as many rights to bake. - -_`Smart contract` - Account_ which is associated to a :ref:`Michelson ` script. They are - created with an explicit origination_ operation and are therefore - sometimes called originated accounts. The address of a smart - contract always starts with the letters ``KT1``. - -_`Transaction` - An operation_ to transfer tez between two accounts, or to run the code of a - `smart contract`_. - -_`Voting period` - A generic term for any of the ``proposal``, ``testing_vote``, ``testing`` or - ``promotion_vote`` periods in the voting procedure when amending the - `economic protocol`_. - -_`Voting listings` - The list calculated at the beginning of each `voting period`_ that - contains the staking balance (in number of rolls) of each - delegate_ that owns at least one roll_ at that moment. The voting - listings reflects the weight of the vote emitted by each delegate_ - when amending the `economic protocol`_. diff --git a/docs/007/michelson.rst b/docs/007/michelson.rst deleted file mode 100644 index f9f7d2f3977b3944145b1228cb9f6fa91c035f35..0000000000000000000000000000000000000000 --- a/docs/007/michelson.rst +++ /dev/null @@ -1,3166 +0,0 @@ -.. _michelson: -.. _michelson_007: - -Michelson: the language of Smart Contracts in Tezos -=================================================== - -This specification gives a detailed formal semantics of the Michelson -language, and a short explanation of how smart contracts are executed -and interact in the blockchain. - -The language is stack-based, with high level data types and primitives, -and strict static type checking. Its design cherry picks traits from -several language families. Vigilant readers will notice direct -references to Forth, Scheme, ML and Cat. - -A Michelson program is a series of instructions that are run in -sequence: each instruction receives as input the stack resulting of the -previous instruction, and rewrites it for the next one. The stack -contains both immediate values and heap allocated structures. All values -are immutable and garbage collected. - -The types of the input and output stack are fixed and monomorphic, -and the program is typechecked before being introduced into the system. -No smart contract execution can fail because an instruction has been -executed on a stack of unexpected length or contents. - -This specification gives the complete instruction set, type system and -semantics of the language. It is meant as a precise reference manual, -not an easy introduction. Even though, some examples are provided at -the end of the document and can be read first or at the same time as -the specification. The document also starts with a less formal -explanation of the context: how Michelson code interacts with the -blockchain. - -Semantics of smart contracts and transactions ---------------------------------------------- - -The Tezos ledger currently has two types of accounts that can hold -tokens (and be the destinations of transactions). - - - An implicit account is a non programmable account, whose tokens - are spendable and delegatable by a public key. Its address is - directly the public key hash, and starts with ``tz1``, ``tz2`` or - ``tz3``. - - A smart contract is a programmable account. A transaction to such - an address can provide data, and can fail for reasons decided by - its Michelson code. Its address is a unique hash that depends on - the operation that led to its creation, and starts with ``KT1``. - -From Michelson, they are indistinguishable. A safe way to think about -this is to consider that implicit accounts are smart contracts that -always succeed to receive tokens, and does nothing else. - -Intra-transaction semantics -~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -Alongside their tokens, smart contracts keep a piece of storage. Both -are ruled by a specific logic specified by a Michelson program. A -transaction to smart contract will provide an input value and in -option some tokens, and in return, the smart contract can modify its -storage and transfer its tokens. - -The Michelson program receives as input a stack containing a single -pair whose first element is an input value and second element the -content of the storage space. It must return a stack containing a -single pair whose first element is the list of internal operations -that it wants to emit, and second element is the new contents of the -storage space. Alternatively, a Michelson program can fail, explicitly -using a specific opcode, or because something went wrong that could -not be caught by the type system (e.g. gas exhaustion). - -A bit of polymorphism can be used at contract level, with a -lightweight system of named entrypoints: instead of an input value, -the contract can be called with an entrypoint name and an argument, -and these two component are transformed automatically in a simple and -deterministic way to an input value. This feature is available both -for users and from Michelson code. See the dedicated section. - -Inter-transaction semantics -~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -An operation included in the blockchain is a sequence of "external -operations" signed as a whole by a source address. These operations -are of three kinds: - - - Transactions to transfer tokens to implicit accounts or tokens and - parameters to a smart contract (or, optionally, to a specified - entrypoint of a smart contract). - - Originations to create new smart contracts from its Michelson - source code, an initial amount of tokens transferred from the - source, and an initial storage contents. - - Delegations to assign the tokens of the source to the stake of - another implicit account (without transferring any tokens). - -Smart contracts can also emit "internal operations". These are run -in sequence after the external transaction completes, as in the -following schema for a sequence of two external operations. - -:: - - +------+----------------+-------+----------------+ - | op 1 | internal ops 1 | op 2 | internal ops 2 | - +------+----------------+-------+----------------+ - -Smart contracts called by internal transactions can in turn also emit -internal operation. The interpretation of the internal operations -of a given external operation use a queue, as in the following -example, also with two external operations. - -:: - - +-----------+---------------+--------------------------+ - | executing | emissions | resulting queue | - +-----------+---------------+--------------------------+ - | op 1 | 1a, 1b, 1c | 1a, 1b, 1c | - | op 1a | 1ai, 1aj | 1b, 1c, 1ai, 1aj | - | op 1b | 1bi | 1c, 1ai, 1aj, 1bi | - | op 1c | | 1ai, 1aj, 1bi | - | op 1ai | | 1aj, 1bi | - | op 1aj | | 1bi | - | op 1bi | | | - | op 2 | 2a, 2b | 2a, 2b | - | op 2a | 2ai | 2b, 2ai | - | op 2b | | 2ai | - | op 2ai | 2ai1 | 2ai1 | - | op 2a1 | 2ai2 | 2ai2 | - | op 2a2 | 2ai3 | 2ai3 | - | op 2a3 | | | - +-----------+---------------+--------------------------+ - -Failures -~~~~~~~~ - -All transactions can fail for a few reasons, mostly: - - - Not enough tokens in the source to spend the specified amount. - - The script took too many execution steps. - - The script failed programmatically using the ``FAILWITH`` instruction. - -External transactions can also fail for these additional reasons: - - - The signature of the external operations was wrong. - - The code or initial storage in an origination did not typecheck. - - The parameter in a transfer did not typecheck. - - The destination did not exist. - - The specified entrypoint did not exist. - -All these errors cannot happen in internal transactions, as the type -system catches them at operation creation time. In particular, -Michelson has two types to talk about other accounts: ``address`` and -``contract t``. The ``address`` type merely gives the guarantee that -the value has the form of a Tezos address. The ``contract t`` type, on -the other hand, guarantees that the value is indeed a valid, existing -account whose parameter type is ``t``. To make a transaction from -Michelson, a value of type ``contract t`` must be provided, and the -type system checks that the argument to the transaction is indeed of -type ``t``. Hence, all transactions made from Michelson are well -formed by construction. - -In any case, when a failure happens, either total success or total -failure is guaranteed. If a transaction (internal or external) fails, -then the whole sequence fails and all the effects up to the failure -are reverted. These transactions can still be included in blocks, and -the transaction fees given to the implicit account who baked the block. - -Language semantics ------------------- - -This specification explains in a symbolic way the computation performed by the -Michelson interpreter on a given program and initial stack to produce -the corresponding resulting stack. The Michelson interpreter is a pure -function: it only builds a result stack from the elements of an initial -one, without affecting its environment. This semantics is then naturally -given in what is called a big step form: a symbolic definition of a -recursive reference interpreter. This definition takes the form of a -list of rules that cover all the possible inputs of the interpreter -(program and stack), and describe the computation of the corresponding -resulting stacks. - -Rules form and selection -~~~~~~~~~~~~~~~~~~~~~~~~ - -The rules have the main following form. - -:: - - > (syntax pattern) / (initial stack pattern) => (result stack pattern) - iff (conditions) - where (recursions) - and (more recursions) - -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 -selected using the following process. First, the toplevel structure of -the program must match the syntax pattern. This is quite simple since -there is only a few non trivial patterns to deal with instruction -sequences, and the rest is made of trivial pattern that match one -specific instruction. Then, the initial stack must match the initial -stack pattern. Finally, some rules add extra conditions over the values -in the stack that follow the ``iff`` keyword. Sometimes, several rules -may apply in a given context. In this case, the one that appears first -in this specification is to be selected. If no rule applies, the result -is equivalent to the one for the explicit ``FAILWITH`` instruction. This -case does not happen on well-typed programs, as explained in the next -section. - -The right hand side describes the result of the interpreter if the rule -applies. It consists in a stack pattern, whose parts are either -constants, or elements of the context (program and initial stack) that -have been named on the left hand side of the ``=>`` sign. - -Recursive rules (big step form) -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -Sometimes, the result of interpreting a program is derived from the -result of interpreting another one (as in conditionals or function -calls). In these cases, the rule contains a clause of the following -form. - -:: - - where (intermediate program) / (intermediate stack) => (partial result) - -This means that this rules applies in case interpreting the intermediate -state on the left gives the pattern on the right. - -The left hand sign of the ``=>`` sign is constructed from elements of -the initial state or other partial results, and the right hand side -identify parts that can be used to build the result stack of the rule. - -If the partial result pattern does not actually match the result of the -interpretation, then the result of the whole rule is equivalent to the -one for the explicit ``FAILWITH`` instruction. Again, this case does not -happen on well-typed programs, as explained in the next section. - -Format of patterns -~~~~~~~~~~~~~~~~~~ - -Code patterns are of one of the following syntactical forms. - -- ``INSTR`` (an uppercase identifier) is a simple instruction (e.g. - ``DROP``). -- ``INSTR (arg) ...`` is a compound instruction, whose arguments can be - code, data or type patterns (e.g. ``PUSH nat 3``). -- ``{ (instr) ; ... }`` is a possibly empty sequence of instructions, - (e.g. ``IF { SWAP ; DROP } { DROP }``), nested sequences can drop the - braces. -- ``name`` is a pattern that matches any program and names a part of - the matched program that can be used to build the result. -- ``_`` is a pattern that matches any instruction. - -Stack patterns are of one of the following syntactical forms. - -- ``[FAILED]`` is the special failed state. -- ``[]`` is the empty stack. -- ``(top) : (rest)`` is a stack whose top element is matched by the - data pattern ``(top)`` on the left, and whose remaining elements are - matched by the stack pattern ``(rest)`` on the right (e.g. - ``x : y : rest``). -- ``name`` is a pattern that matches any stack and names it in order to - use it to build the result. -- ``_`` is a pattern that matches any stack. - -Data patterns are of one of the following syntactical forms. - -- integer/natural number literals, (e.g. ``3``). -- string literals, (e.g. ``"contents"``). -- raw byte sequence literals (e.g. ``0xABCDEF42``). -- ``Tag`` (capitalized) is a symbolic constant, (e.g. ``Unit``, - ``True``, ``False``). -- ``(Tag (arg) ...)`` tagged constructed data, (e.g. ``(Pair 3 4)``). -- a code pattern for first class code values. -- ``name`` to name a value in order to use it to build the result. -- ``_`` to match any value. - -The domain of instruction names, symbolic constants and data -constructors is fixed by this specification. Michelson does not let the -programmer introduce its own types. - -Be aware that the syntax used in the specification may differ from -the :ref:`concrete syntax `. In particular -some instructions are annotated with types that are not present in the -concrete language because they are synthesized by the typechecker. - -Shortcuts -~~~~~~~~~ - -Sometimes, it is easier to think (and shorter to write) in terms of -program rewriting than in terms of big step semantics. When it is the -case, and when both are equivalents, we write rules of the form: - -:: - - p / S => S'' - where p' / S' => S'' - -using the following shortcut: - -:: - - p / S => p' / S' - -The concrete language also has some syntax sugar to group some common -sequences of operations as one. This is described in this specification -using a simple regular expression style recursive instruction rewriting. - -Introduction to the type system and notations ---------------------------------------------- - -This specification describes a type system for Michelson. To make things -clear, in particular to readers that are not accustomed to reading -formal programming language specifications, it does not give a -typechecking or inference algorithm. It only gives an intentional -definition of what we consider to be well-typed programs. For each -syntactical form, it describes the stacks that are considered well-typed -inputs, and the resulting outputs. - -The type system is sound, meaning that if a program can be given a type, -then if run on a well-typed input stack, the interpreter will never -apply an interpretation rule on a stack of unexpected length or -contents. Also, it will never reach a state where it cannot select an -appropriate rule to continue the execution. Well-typed programs do not -block, and do not go wrong. - -Type notations -~~~~~~~~~~~~~~ - -The specification introduces notations for the types of values, terms -and stacks. Apart from a subset of value types that appear in the form -of type annotations in some places throughout the language, it is -important to understand that this type language only exists in the -specification. - -A stack type can be written: - -- ``[]`` for the empty stack. -- ``(top) : (rest)`` for the stack whose first value has type ``(top)`` - and queue has stack type ``(rest)``. - -Instructions, programs and primitives of the language are also typed, -their types are written: - -:: - - (type of stack before) -> (type of stack after) - -The types of values in the stack are written: - -- ``identifier`` for a primitive data-type (e.g. ``bool``). -- ``identifier (arg)`` for a parametric data-type with one parameter - type ``(arg)`` (e.g. ``list nat``). -- ``identifier (arg) ...`` for a parametric data-type with several - parameters (e.g. ``map string int``). -- ``[ (type of stack before) -> (type of stack after) ]`` for a code - quotation, (e.g. ``[ int : int : [] -> int : [] ]``). -- ``lambda (arg) (ret)`` is a shortcut for - ``[ (arg) : [] -> (ret) : [] ]``. - -Meta type variables -~~~~~~~~~~~~~~~~~~~ - -The typing rules introduce meta type variables. To be clear, this has -nothing to do with polymorphism, which Michelson does not have. These -variables only live at the specification level, and are used to express -the consistency between the parts of the program. For instance, the -typing rule for the ``IF`` construct introduces meta variables to -express that both branches must have the same type. - -Here are the notations for meta type variables: - -- ``'a`` for a type variable. -- ``'A`` for a stack type variable. -- ``_`` for an anonymous type or stack type variable. - -Typing rules -~~~~~~~~~~~~ - -The system is syntax directed, meaning that it defines a single -typing rule for each syntax construct. A typing rule restricts the type -of input stacks that are authorized for this syntax construct, links the -output type to the input type, and links both of them to the -subexpressions when needed, using meta type variables. - -Typing rules are of the form: - -:: - - (syntax pattern) - :: (type of stack before) -> (type of stack after) [rule-name] - iff (premises) - -Where premises are typing requirements over subprograms or values in the -stack, both of the form ``(x) :: (type)``, meaning that value ``(x)`` -must have type ``(type)``. - -A program is shown well-typed if one can find an instance of a rule that -applies to the toplevel program expression, with all meta type variables -replaced by non variable type expressions, and of which all type -requirements in the premises can be proven well-typed in the same -manner. For the reader unfamiliar with formal type systems, this is -called building a typing derivation. - -Here is an example typing derivation on a small program that computes -``(x+5)*10`` for a given input ``x``, obtained by instantiating the -typing rules for instructions ``PUSH``, ``ADD`` and for the sequence, as -found in the next sections. When instantiating, we replace the ``iff`` -with ``by``. - -:: - - { PUSH nat 5 ; ADD ; PUSH nat 10 ; MUL } - :: [ nat : [] -> nat : [] ] - by { PUSH nat 5 ; ADD } - :: [ nat : [] -> nat : [] ] - by PUSH nat 5 - :: [ nat : [] -> nat : nat : [] ] - by 5 :: nat - and ADD - :: [ nat : nat : [] -> nat : [] ] - and { PUSH nat 10 ; MUL } - :: [ nat : [] -> nat : [] ] - by PUSH nat 10 - :: [ nat : [] -> nat : nat : [] ] - by 10 :: nat - and MUL - :: [ nat : nat : [] -> nat : [] ] - -Producing such a typing derivation can be done in a number of manners, -such as unification or abstract interpretation. In the implementation of -Michelson, this is done by performing a recursive symbolic evaluation of -the program on an abstract stack representing the input type provided by -the programmer, and checking that the resulting symbolic stack is -consistent with the expected result, also provided by the programmer. - -Side note -~~~~~~~~~ - -As with most type systems, it is incomplete. There are programs that -cannot be given a type in this type system, yet that would not go wrong -if executed. This is a necessary compromise to make the type system -usable. Also, it is important to remember that the implementation of -Michelson does not accept as many programs as the type system describes -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 ------------------------------ - -- ``string``, ``nat``, ``int`` and ``bytes``: The core primitive - constant types. - -- ``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. - -- ``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)``. - -- ``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)`` that we write ``{ Elt key value ; ... }``, - with keys sorted. These maps should be used if one intends to store - large amounts of data in a map. They have higher gas costs than - standard maps as data is lazily deserialized. A ``big_map`` cannot - appear inside another ``big_map``. - -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 - -- ``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 - -- ``UNIT``: Push a unit value onto the stack. - -:: - - :: 'A -> unit : 'A - - > UNIT / S => Unit : 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 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 - -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 -~~~~~~~~~~~~~~~~~~~ - -- ``PAIR``: Build a pair from the stack's top two elements. - -:: - - :: 'a : 'b : 'S -> pair 'a 'b : 'S - - > PAIR / a : b : S => (Pair a b) : S - -- ``CAR``: Access the left part of a pair. - -:: - - :: pair 'a _ : 'S -> 'a : 'S - - > CAR / (Pair a _) : S => a : S - -- ``CDR``: Access the right part of a pair. - -:: - - :: pair _ 'b : 'S -> 'b : 'S - - > CDR / (Pair _ b) : S => b : 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 : [] - -- ``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`` -~~~~~~~~~~~~~~~~~~~~~~~~~~ - -The behavior of these 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 - - -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 - -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 - -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. - -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 : 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: -.. _MichelsonSetDelegate_007: - -- ``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 - -- ``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 - -Special operations -~~~~~~~~~~~~~~~~~~ - -- ``NOW``: Push the timestamp of the block whose validation triggered - this execution (does not change during the execution of the - contract). - -:: - - :: 'S -> timestamp : 'S - -- ``CHAIN_ID``: Push the chain identifier. - -:: - - :: 'S -> chain_id : '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 - -- ``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 - -- ``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_hash : '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 - -Deprecated instructions -~~~~~~~~~~~~~~~~~~~~~~~ - -The following instructions are deprecated. The Michelson type-checker -will reject any contract using them but contracts already originated -on the blockchain using them will continue to work as before. - -- ``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 - - -Macros ------- - -In addition to the operations above, 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. - -These macros are designed to be unambiguous and reversible, meaning that -errors are reported in terms of desugared syntax. Below you'll see -these macros defined in terms of other syntactic forms. That is how -these macros are seen by the node. - -Compare -~~~~~~~ - -Syntactic sugar exists for merging ``COMPARE`` and comparison -combinators, and also for branching. - -- ``CMP{EQ|NEQ|LT|GT|LE|GE}`` - -:: - - > CMP(\op) / S => COMPARE ; (\op) / S - -- ``IF{EQ|NEQ|LT|GT|LE|GE} bt bf`` - -:: - - > IF(\op) bt bf / S => (\op) ; IF bt bf / S - -- ``IFCMP{EQ|NEQ|LT|GT|LE|GE} bt bf`` - -:: - - > IFCMP(\op) / S => COMPARE ; (\op) ; IF bt bf / S - -Fail -~~~~ - -The ``FAIL`` macros is equivalent to ``UNIT; FAILWITH`` and is callable -in any context since it does not use its input stack. - -- ``FAIL`` - -:: - - > FAIL / S => UNIT; FAILWITH / S - -Assertion macros -~~~~~~~~~~~~~~~~ - -All assertion operations are syntactic sugar for conditionals with a -``FAIL`` instruction in the appropriate branch. When possible, use them -to increase clarity about illegal states. - -- ``ASSERT`` - -:: - - > ASSERT => IF {} {FAIL} - -- ``ASSERT_{EQ|NEQ|LT|LE|GT|GE}`` - -:: - - > ASSERT_(\op) => IF(\op) {} {FAIL} - -- ``ASSERT_CMP{EQ|NEQ|LT|LE|GT|GE}`` - -:: - - > ASSERT_CMP(\op) => IFCMP(\op) {} {FAIL} - -- ``ASSERT_NONE`` - -:: - - > ASSERT_NONE => IF_NONE {} {FAIL} - -- ``ASSERT_SOME`` - -:: - - > ASSERT_SOME @x => IF_NONE {FAIL} {RENAME @x} - -- ``ASSERT_LEFT`` - -:: - - > ASSERT_LEFT @x => IF_LEFT {RENAME @x} {FAIL} - -- ``ASSERT_RIGHT`` - -:: - - > ASSERT_RIGHT @x => IF_LEFT {FAIL} {RENAME @x} - -Syntactic Conveniences -~~~~~~~~~~~~~~~~~~~~~~ - -These macros are simply more convenient syntax for various common -operations. - -- ``DUP n``: A syntactic sugar for duplicating the ``n``\ th element of - the stack. - -:: - - > DUP 1 / S => DUP / S - > DUP 2 / S => DIP (DUP) ; SWAP / S - > DUP (n+1) / S => DIP n (DUP) ; DIG (n+1) / S - -- ``P(\left=A|P(\left)(\right))(\right=I|P(\left)(\right))R``: A syntactic sugar - for building nested pairs. - -:: - - > PA(\right)R / S => DIP ((\right)R) ; PAIR / S - > P(\left)IR / S => (\left)R ; PAIR / S - > P(\left)(\right)R => (\left)R ; DIP ((\right)R) ; PAIR / S - -A good way to quickly figure which macro to use is to mentally parse the -macro as ``P`` for pair constructor, ``A`` for left leaf and ``I`` for -right leaf. The macro takes as many elements on the stack as there are -leaves and constructs a nested pair with the shape given by its name. - -Take the macro ``PAPPAIIR`` for instance: - -:: - - P A P P A I I R - ( l, ( ( l, r ), r )) - -A typing rule can be inferred: - -:: - - PAPPAIIR - :: 'a : 'b : 'c : 'd : 'S -> (pair 'a (pair (pair 'b 'c) 'd)) - -- ``UNP(\left=A|P(\left)(\right))(\right=I|P(\left)(\right))R``: A syntactic sugar - for destructing nested pairs. These macros follow the same convention - as the previous one. - -:: - - > UNPAIR / S => DUP ; CAR ; DIP { CDR } / S - > UNPA(\right)R / S => UNPAIR ; DIP (UN(\right)R) / S - > UNP(\left)IR / S => UNPAIR ; UN(\left)R / S - > UNP(\left)(\right)R => UNPAIR ; DIP (UN(\right)R) ; UN(\left)R / S - -- ``C[AD]+R``: A syntactic sugar for accessing fields in nested pairs. - -:: - - > CA(\rest=[AD]+)R / S => CAR ; C(\rest)R / S - > CD(\rest=[AD]+)R / S => CDR ; C(\rest)R / S - -- ``IF_SOME bt bf``: Inspect an optional value. - -:: - - > IF_SOME bt bf / S => IF_NONE bf bt / S - -- ``IF_RIGHT bt bf``: Inspect a value of a union. - -:: - - > IF_RIGHT bt bf / S => IF_LEFT bf bt / S - -- ``SET_CAR``: Set the left field of a pair. - -:: - - > SET_CAR => CDR ; SWAP ; PAIR - -- ``SET_CDR``: Set the right field of a pair. - -:: - - > SET_CDR => CAR ; PAIR - -- ``SET_C[AD]+R``: A syntactic sugar for setting fields in nested - pairs. - -:: - - > SET_CA(\rest=[AD]+)R / S => - { DUP ; DIP { CAR ; SET_C(\rest)R } ; CDR ; SWAP ; PAIR } / S - > SET_CD(\rest=[AD]+)R / S => - { DUP ; DIP { CDR ; SET_C(\rest)R } ; CAR ; PAIR } / S - -- ``MAP_CAR`` code: Transform the left field of a pair. - -:: - - > MAP_CAR code => DUP ; CDR ; DIP { CAR ; code } ; SWAP ; PAIR - -- ``MAP_CDR`` code: Transform the right field of a pair. - -:: - - > MAP_CDR code => DUP ; CDR ; code ; SWAP ; CAR ; PAIR - -- ``MAP_C[AD]+R`` code: A syntactic sugar for transforming fields in - nested pairs. - -:: - - > MAP_CA(\rest=[AD]+)R code / S => - { DUP ; DIP { CAR ; MAP_C(\rest)R code } ; CDR ; SWAP ; PAIR } / S - > MAP_CD(\rest=[AD]+)R code / S => - { DUP ; DIP { CDR ; MAP_C(\rest)R code } ; CAR ; PAIR } / S - -.. _ConcreteSyntax: -.. _ConcreteSyntax_007: - -Concrete syntax ---------------- - -The concrete language is very close to the formal notation of the -specification. Its structure is extremely simple: an expression in the -language can only be one of the five following constructs. - -1. An integer in decimal notation. -2. A character string. -3. A byte sequence in hexadecimal notation prefixed by ``0x``. -4. The application of a primitive to a sequence of expressions. -5. A sequence of expressions. - -This simple five cases notation is called :ref:`Micheline`. - -Constants -~~~~~~~~~ - -There are three kinds of constants: - -1. Integers or naturals in decimal notation. -2. Strings, with some usual escape sequences: ``\n``, ``\\``, - ``\"``. Unescaped line-breaks (both ``\n`` and ``\r``) cannot - appear in a Michelson string. Moreover, the current version of - Michelson restricts strings to be the printable subset of 7-bit - ASCII, namely characters with codes from within `[32, 126]` range, - plus the escaped characters mentioned above. -3. Byte sequences in hexadecimal notation, prefixed with ``0x``. - -Differences with the formal notation -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -The concrete syntax follows the same lexical conventions as the -specification: instructions are represented by uppercase identifiers, -type constructors by lowercase identifiers, and constant constructors -are capitalized. - -All domain specific constants are Micheline constants with specific -formats. Some have two variants accepted by the data type checker: a -readable one in a string and an optimized. - -- ``mutez`` amounts are written as naturals. -- ``timestamp``\ s are written either using ``RFC3339`` notation - 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 their raw bytes (optimized). - -The optimized versions should not reach the RPCs, the protocol code -will convert to optimized by itself when forging operations, storing -to the database, and before hashing to get a canonical representation -of a datum for a given type. - -To prevent errors, control flow primitives that take instructions as -parameters require sequences in the concrete syntax. - -:: - - IF { instr1_true ; instr2_true ; ... } - { instr1_false ; instr2_false ; ... } - -Main program structure -~~~~~~~~~~~~~~~~~~~~~~ - -The toplevel of a smart contract file must be an un-delimited sequence -of three primitive applications (in no particular order) that provide its -``code``, ``parameter`` and ``storage`` fields. - -See the next section for a concrete example. - -Annotations ------------ - -The annotation mechanism of Michelson provides ways to better track -data on the stack and to give additional type constraints. Except for -a single exception specified just after, annotations are only here to -add constraints, *i.e.* they cannot turn an otherwise rejected program -into an accepted one. The notable exception to this rule is for -entrypoints: the semantics of the `CONTRACT` and `SELF` instructions vary depending on -their constructor annotations, and some contract origination may fail due -to invalid entrypoint constructor annotations. - -Stack visualization tools like the Michelson's Emacs mode print -annotations associated with each type in the program, as propagated by -the typechecker as well as variable annotations on the types of elements -in the stack. This is useful as a debugging aid. - -We distinguish three kinds of annotations: - -- type annotations, written ``:type_annot``, -- variable annotations, written ``@var_annot``, -- and field or constructors annotations, written ``%field_annot``. - -Type annotations -~~~~~~~~~~~~~~~~ - -Each type can be annotated with at most one type annotation. They are -used to give names to types. For types to be equal, their unnamed -version must be equal and their names must be the same or at least one -type must be unnamed. - -For instance, the following Michelson program which put its integer -parameter in the storage is not well typed: - -.. code-block:: michelson - - parameter (int :p) ; - storage (int :s) ; - code { UNPAIR ; SWAP ; DROP ; NIL operation ; PAIR } - -Whereas this one is: - -.. code-block:: michelson - - parameter (int :p) ; - storage int ; - code { UNPAIR ; SWAP ; DROP ; NIL operation ; PAIR } - -Inner components of composed typed can also be named. - -:: - - (pair :point (int :x_pos) (int :y_pos)) - -Push-like instructions, that act as constructors, can also be given a -type annotation. The stack type will then have on top a type with a corresponding name. - -:: - - UNIT :t - :: 'A -> (unit :t) : 'A - - PAIR :t - :: 'a : 'b : 'S -> (pair :t 'a 'b) : 'S - - SOME :t - :: 'a : 'S -> (option :t 'a) : 'S - - NONE :t 'a - :: 'S -> (option :t 'a) : 'S - - LEFT :t 'b - :: 'a : 'S -> (or :t 'a 'b) : 'S - - RIGHT :t 'a - :: 'b : 'S -> (or :t 'a 'b) : 'S - - NIL :t 'a - :: 'S -> (list :t 'a) : 'S - - EMPTY_SET :t 'elt - :: 'S -> (set :t 'elt) : 'S - - EMPTY_MAP :t 'key 'val - :: 'S -> (map :t 'key 'val) : 'S - - EMPTY_BIG_MAP :t 'key 'val - :: 'S -> (big_map :t 'key 'val) : 'S - - -A no-op instruction ``CAST`` ensures the top of the stack has the -specified type, and change its type if it is compatible. In particular, -this allows to change or remove type names explicitly. - -:: - - CAST 'b - :: 'a : 'S -> 'b : 'S - iff 'a = 'b - - > CAST t / a : S => a : S - - -Variable annotations -~~~~~~~~~~~~~~~~~~~~ - -Variable annotations can only be used on instructions that produce -elements on the stack. An instruction that produces ``n`` elements on -the stack can be given at most ``n`` variable annotations. - -The stack type contains both the types of each element in the stack, as -well as an optional variable annotation for each element. In this -sub-section we note: - -- ``[]`` for the empty stack, -- ``@annot (top) : (rest)`` for the stack whose first value has type ``(top)`` and is annotated with variable annotation ``@annot`` and whose queue has stack type ``(rest)``. - -The instructions which do not accept any variable annotations are: - -:: - - DROP - SWAP - DIG - DUG - IF_NONE - IF_LEFT - IF_CONS - ITER - IF - LOOP - LOOP_LEFT - DIP - FAILWITH - -The instructions which accept at most one variable annotation are: - -:: - - DUP - PUSH - UNIT - SOME - NONE - PAIR - CAR - CDR - LEFT - RIGHT - NIL - CONS - SIZE - MAP - MEM - EMPTY_SET - EMPTY_MAP - EMPTY_BIG_MAP - UPDATE - GET - LAMBDA - EXEC - ADD - SUB - CONCAT - MUL - OR - AND - XOR - NOT - ABS - ISNAT - INT - NEG - EDIV - LSL - LSR - COMPARE - EQ - NEQ - LT - GT - LE - GE - ADDRESS - CONTRACT - SET_DELEGATE - IMPLICIT_ACCOUNT - NOW - AMOUNT - BALANCE - HASH_KEY - CHECK_SIGNATURE - BLAKE2B - STEPS_TO_QUOTA - SOURCE - SENDER - SELF - CAST - RENAME - CHAIN_ID - -The instructions which accept at most two variable annotations are: - -:: - - CREATE_ACCOUNT - CREATE_CONTRACT - -Annotations on instructions that produce multiple elements on the stack -will be used in order, where the first variable annotation is given to -the top-most element on the resulting stack. Instructions that produce -``n`` elements on the stack but are given less than ``n`` variable -annotations will see only their top-most stack type elements annotated. - -:: - - CREATE_ACCOUNT @op @addr - :: key_hash : option key_hash : bool : mutez : 'S - -> @op operation : @addr address : 'S - - CREATE_ACCOUNT @op - :: key_hash : option key_hash : bool : mutez : 'S - -> @op operation : address : 'S - -A no-op instruction ``RENAME`` allows to rename variables in the stack -or to erase variable annotations in the stack. - -:: - - RENAME @new - :: @old 'a ; 'S -> @new 'a : 'S - - RENAME - :: @old 'a ; 'S -> 'a : 'S - - -Field and constructor annotations -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -Components of pair types, option types and or types can be annotated -with a field or constructor annotation. This feature is useful to encode -records fields and constructors of sum types. - -:: - - (pair :point - (int %x) - (int %y)) - -The previous Michelson type can be used as visual aid to represent the -record type (given in OCaml-like syntax): - -:: - - type point = { x : int ; y : int } - -Similarly, - -:: - - (or :t - (int %A) - (or - (bool %B) - (pair %C - (nat %n1) - (nat %n2)))) - -can be used to represent the algebraic data type (in OCaml-like syntax): - -:: - - type t = - | A of int - | B of bool - | C of { n1 : nat ; n2 : nat } - - -Field annotations are part of the type (at the same level as type name -annotations), and so types with differing field names (if present) are -not considered equal. - -Instructions that construct elements of composed types can also be -annotated with one or multiple field annotations (in addition to type -and variable annotations). - -:: - - PAIR %fst %snd - :: 'a : 'b : 'S -> (pair ('a %fst) ('b %snd)) : 'S - - LEFT %left %right 'b - :: 'a : 'S -> (or ('a %left) ('b %right)) : 'S - - RIGHT %left %right 'a - :: 'b : 'S -> (or ('a %left) ('b %right)) : 'S - -To improve readability and robustness, instructions ``CAR`` and ``CDR`` -accept one field annotation. For the contract to type check, the name of -the accessed field in the destructed pair must match the one given here. - -:: - - CAR %fst - :: (pair ('a %fst) 'b) : S -> 'a : 'S - - CDR %snd - :: (pair 'a ('b %snd)) : S -> 'b : 'S - - -Syntax -~~~~~~ - -Primitive applications can receive one or many annotations. - -An annotation is a sequence of characters that matches the regular -expression ``@%|@%%|%@|[@:%][_0-9a-zA-Z][_0-9a-zA-Z\.%@]*``. -Note however that ``@%``, ``@%%`` and ``%@`` are -:ref:`special annotations ` and are not allowed everywhere. - -Annotations come after the primitive name and before its potential arguments. - -:: - - (prim @v :t %x arg1 arg2 ...) - - -Ordering between different kinds of annotations is not significant, but -ordering among annotations of the same kind is. Annotations of the same -kind must be grouped together. - -For instance these two annotated instructions are equivalent: - -:: - - PAIR :t @my_pair %x %y - - PAIR %x %y :t @my_pair - -An annotation can be empty, in this case it will mean *no annotation* -and can be used as a wildcard. For instance, it is useful to annotate -only the right field of a pair instruction ``PAIR % %right`` or to -ignore field access constraints, *e.g.* in the macro ``UNPPAIPAIR %x1 % -%x3 %x4``. - -Annotations and macros -~~~~~~~~~~~~~~~~~~~~~~ - -Macros also support annotations, which are propagated on their expanded -forms. As with instructions, macros that produce ``n`` values on the -stack accept ``n`` variable annotations. - -:: - - DUU+P @annot - > DUU(\rest=U*)P @annot / S => DIP (DU(\rest)P @annot) ; SWAP / S - - C[AD]+R @annot %field_name - > CA(\rest=[AD]+)R @annot %field_name / S => CAR ; C(\rest)R @annot %field_name / S - > CD(\rest=[AD]+)R @annot %field_name / S => CDR ; C(\rest)R @annot %field_name / S - - ``CMP{EQ|NEQ|LT|GT|LE|GE}`` @annot - > CMP(\op) @annot / S => COMPARE ; (\op) @annot / S - -The variable annotation on ``SET_C[AD]+R`` and ``MAP_C[AD]+R`` annotates -the resulting toplevel pair while its field annotation is used to check -that the modified field is the expected one. - -:: - - SET_C[AD]+R @var %field - > SET_CAR @var %field => CDR %field ; SWAP ; PAIR @var - > SET_CDR @var %field => CAR %field ; PAIR @var - > SET_CA(\rest=[AD]+)R @var %field / S => - { DUP ; DIP { CAR ; SET_C(\rest)R %field } ; CDR ; SWAP ; PAIR @var } / S - > SET_CD(\rest=[AD]+)R @var %field/ S => - { DUP ; DIP { CDR ; SET_C(\rest)R %field } ; CAR ; PAIR @var } / S - - MAP_C[AD]+R @var %field code - > MAP_CAR code => DUP ; CDR ; DIP { CAR %field ; code } ; SWAP ; PAIR @var - > MAP_CDR code => DUP ; CDR %field ; code ; SWAP ; CAR ; PAIR @var - > MAP_CA(\rest=[AD]+)R @var %field code / S => - { DUP ; DIP { CAR ; MAP_C(\rest)R %field code } ; CDR ; SWAP ; PAIR @var} / S - > MAP_CD(\rest=[AD]+)R @var %field code / S => - { DUP ; DIP { CDR ; MAP_C(\rest)R %field code } ; CAR ; PAIR @var} / S - -Macros for nested ``PAIR`` and ``UNPAIR`` accept multiple -annotations. Field annotations for ``PAIR`` give names to leaves of the -constructed nested pair, in order. Variable annotations for ``UNPAIR`` -give names to deconstructed components on the stack. This next snippet -gives examples instead of generic rewrite rules for readability -purposes. - -:: - - PAPPAIIR @p %x1 %x2 %x3 %x4 - :: 'a : 'b : 'c : 'd : 'S - -> @p (pair ('a %x1) (pair (pair ('b %x) ('c %x3)) ('d %x4))) : 'S - - PAPAIR @p %x1 %x2 %x3 - :: 'a : 'b : 'c : 'S -> @p (pair ('a %x1) (pair ('b %x) ('c %x3))) : 'S - - UNPAIR @x @y - :: (pair 'a 'b) : 'S -> @x 'a : @y 'b : 'S - - UNPAPPAIIR @x1 @x2 @x3 @x4 - :: (pair 'a (pair (pair 'b 'c) 'd )) : 'S - -> @x1 'a : @x2 'b : @x3 'c : @x4 'd : 'S - -Automatic variable and field annotations inferring -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -When no annotation is provided by the Michelson programmer, the -typechecker infers some annotations in specific cases. This greatly -helps users track information in the stack for bare contracts. - -For unannotated accesses with ``CAR`` and ``CDR`` to fields that are -named will be appended (with an additional ``.`` character) to the pair -variable annotation. - -:: - - CDAR - :: @p (pair ('a %foo) (pair %bar ('b %x) ('c %y))) : 'S -> @p.bar.x 'b : 'S - -If fields are not named but the pair is still named in the stack then -``.car`` or ``.cdr`` will be appended. - -:: - - CDAR - :: @p (pair 'a (pair 'b 'c)) : 'S -> @p.cdr.car 'b : 'S - -If the original pair is not named in the stack, but a field annotation -is present in the pair type the accessed value will be annotated with a -variable annotation corresponding to the field annotation alone. - -:: - - CDAR - :: (pair ('a %foo) (pair %bar ('b %x) ('c %y))) : 'S -> @bar.x 'b : 'S - -A similar mechanism is used for context dependent instructions: - -:: - - ADDRESS :: @c contract _ : 'S -> @c.address address : 'S - - CONTRACT 'p :: @a address : 'S -> @a.contract contract 'p : 'S - - BALANCE :: 'S -> @balance mutez : 'S - - SOURCE :: 'S -> @source address : 'S - - SENDER :: 'S -> @sender address : 'S - - SELF :: 'S -> @self contract 'p : 'S - - AMOUNT :: 'S -> @amount mutez : 'S - - STEPS_TO_QUOTA :: 'S -> @steps nat : 'S - - NOW :: 'S -> @now timestamp : 'S - -Inside nested code blocks, bound items on the stack will be given a -default variable name annotation depending on the instruction and stack -type (which can be changed). For instance the annotated typing rule for -``ITER`` on lists is: - -:: - - ITER body - :: @l (list 'e) : 'A -> 'A - iff body :: [ @l.elt e' : 'A -> 'A ] - -.. _SpecialAnnotations: -.. _SpecialAnnotations_007: - -Special annotations -~~~~~~~~~~~~~~~~~~~ - -The special variable annotations ``@%`` and ``@%%`` can be used on instructions -``CAR`` and ``CDR``. It means to use the accessed field name (if any) as -a name for the value on the stack. The following typing rule -demonstrates their use for instruction ``CAR``. - -:: - - CAR @% - :: @p (pair ('a %fst) ('b %snd)) : 'S -> @fst 'a : 'S - - CAR @%% - :: @p (pair ('a %fst) ('b %snd)) : 'S -> @p.fst 'a : 'S - -The special field annotation ``%@`` can be used on instructions -``PAIR``, ``LEFT`` and ``RIGHT``. It means to use the variable -name annotation in the stack as a field name for the constructed -element. Two examples with ``PAIR`` follows, notice the special -treatment of annotations with ``.``. - -:: - - PAIR %@ %@ - :: @x 'a : @y 'b : 'S -> (pair ('a %x) ('b %y)) : 'S - - PAIR %@ %@ - :: @p.x 'a : @p.y 'b : 'S -> @p (pair ('a %x) ('b %y)) : 'S - :: @p.x 'a : @q.y 'b : 'S -> (pair ('a %x) ('b %y)) : 'S - -Entrypoints ------------ - -The specification up to this point has been mostly ignoring existence -of entrypoints: a mechanism of contract level polymorphism. This -mechanism is optional, non intrusive, and transparent to smart -contracts that don't use them. This section is to be read as a patch -over the rest of the specification, introducing rules that apply only -in presence of contracts that make use of entrypoints. - -Defining and calling entrypoints -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -Entrypoints piggyback on the constructor annotations. A contract with -entrypoints is basically a contract that takes a disjunctive type (a -nesting of ``or`` types) as the root of its input parameter, decorated -with constructor annotations. An extra check is performed on these -constructor annotations: a contract cannot define two entrypoints with -the same name. - -An external transaction can include an entrypoint name alongside the -parameter value. In that case, if there is a constructor annotation -with this name at any position in the nesting of ``or`` types, the -value is automatically wrapped into the according constructors. If the -transaction specifies an entrypoint, but there is no such constructor -annotation, the transaction fails. - -For instance, suppose the following input type. - -``parameter (or (or (nat %A) (bool %B)) (or %maybe_C (unit %Z) (string %C)))`` - -The input values will be wrapped as in the following examples. - -:: - - +------------+-----------+---------------------------------+ - | entrypoint | input | wrapped input | - +------------+-----------+---------------------------------+ - | %A | 3 | Left (Left 3) | - | %B | False | Left (Right False) | - | %C | "bob" | Right (Right "bob") | - | %Z | Unit | Right (Left Unit) | - | %maybe_C | Right "x" | Right (Right "x") | - | %maybe_C | Left Unit | Right (Left Unit) | - +------------+-----------+---------------------------------+ - | not given | value | value (untouched) | - | %BAD | _ | failure, contract not called | - +------------+-----------+---------------------------------+ - -The ``default`` entrypoint -~~~~~~~~~~~~~~~~~~~~~~~~~~ - -A special semantics is assigned to the ``default`` entrypoint. If the -contract does not explicitly declare a ``default`` entrypoint, then it -is automatically assigned to the root of the parameter -type. Conversely, if the contract is called without specifying an -entrypoint, then it is assumed to be called with the ``default`` -entrypoint. This behaviour makes the entrypoint system completely -transparent to contracts that do not use it. - -This is the case for the previous example, for instance. If a value is -passed to such a contract specifying entrypoint ``default``, then the -value is fed to the contract untouched, exactly as if no entrypoint -was given. - -A non enforced convention is to make the entrypoint ``default`` of -type unit, and to implement the crediting operation (just receive the -transferred tokens). - -A consequence of this semantics is that if the contract uses the -entrypoint system and defines a ``default`` entrypoint somewhere else -than at the root of the parameter type, then it must provide an -entrypoint for all the paths in the toplevel disjunction. Otherwise, -some parts of the contracts would be dead code. - -Another consequence of setting the entrypoint somewhere else than at -the root is that it makes it impossible to send the raw values of the -full parameter type to a contract. A trivial solution for that is to -name the root of the type. The conventional name for that is ``root``. - -Let us recapitulate this by tweaking the names of the previous example. - -``parameter %root (or (or (nat %A) (bool %B)) (or (unit %default) string))`` - -The input values will be wrapped as in the following examples. - -:: - - +------------+---------------------+-----------------------+ - | entrypoint | input | wrapped input | - +------------+---------------------+-----------------------+ - | %A | 3 | Left (Left 3) | - | %B | False | Left (Right False) | - | %default | Unit | Right (Left Unit) | - | %root | Right (Right "bob") | Right (Right "bob") | - +------------+---------------------+-----------------------+ - | not given | Unit | Right (Left Unit) | - | %BAD | _ | failure, contract not | - +------------+---------------------+-----------------------+ - -Calling entrypoints from Michelson -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -Michelson code can also produce transactions to a specific entrypoint. - -For this, both types ``address`` and ``contract`` have the ability to -denote not just an address, but a pair of an address and an -entrypoint. The concrete notation is ``"address%entrypoint"``. -Note that ``"address"`` is strictly equivalent to ``"address%default"``, -and for clarity, the second variant is forbidden in the concrete syntax. - -When the ``TRANSFER_TOKENS`` instruction is called, it places the -entrypoint provided in the contract handle in the transaction. - -The ``CONTRACT t`` instruction has a variant ``CONTRACT %entrypoint -t``, that works as follows. Note that ``CONTRACT t`` is strictly -equivalent to ``CONTRACT %default t``, and for clarity, the second -variant is forbidden in the concrete syntax. - -:: - - +---------------+---------------------+------------------------------------------+ - | input address | instruction | output contract | - +---------------+---------------------+------------------------------------------+ - | "addr" | CONTRACT t | (Some "addr") if contract exists, has a | - | | | default entrypoint of type t, or has no | - | | | default entrypoint and parameter type t | - +---------------+---------------------+------------------------------------------+ - | "addr%name" | CONTRACT t | (Some "addr%name") if addr exists and | - +---------------+---------------------+ has an entrypoint %name of type t | - | "addr" | CONTRACT %name t | | - +---------------+---------------------+------------------------------------------+ - | "addr%_" | CONTRACT %_ t | None | - +---------------+---------------------+------------------------------------------+ - -Similarly, the ``SELF`` instruction has a variant ``SELF %entrypoint``, -that is only well-typed if the current contract has an entrypoint named ``%entrypoint``. - -- ``SELF %entrypoint`` - -:: - - :: 'S -> contract 'p : 'S - where contract 'p is the type of the entrypoint %entrypoint of the current contract - -Implicit accounts are considered to have a single ``default`` -entrypoint of type ``Unit``. - -JSON syntax ------------ - -Micheline expressions are encoded in JSON like this: - -- An integer ``N`` is an object with a single field ``"int"`` whose - value is the decimal representation as a string. - - ``{ "int": "N" }`` - -- A string ``"contents"`` is an object with a single field ``"string"`` - whose value is the decimal representation as a string. - - ``{ "string": "contents" }`` - -- A sequence is a JSON array. - - ``[ expr, ... ]`` - -- A primitive application is an object with two fields ``"prim"`` for - the primitive name and ``"args"`` for the arguments (that must - contain an array). A third optional field ``"annots"`` contains a - list of annotations, including their leading ``@``, ``%`` or ``:`` - sign. - - ``{ "prim": "pair", "args": [ { "prim": "nat", "args": [] }, { "prim": "nat", "args": [] } ], "annots": [":t"] }`` - -As in the concrete syntax, all domain specific constants are encoded as -strings. - -Examples ---------- - -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 -contract at origination time. This is ensured statically by checking on -origination that the code preserves the type of the global data. For -this, the code of the contract is checked to be of type -``lambda (pair 'arg 'global) -> (pair (list operation) 'global)`` where -``'global`` is the type of the original global store given on origination. -The contract also takes a parameter and returns a list of internal operations, -hence the complete calling convention above. The internal operations are -queued for execution when the contract returns. - -Empty contract -~~~~~~~~~~~~~~ - -The simplest contract is the contract for which the ``parameter`` and -``storage`` are all of type ``unit``. This contract is as follows: - -.. code-block:: michelson - - code { CDR ; # keep the storage - NIL operation ; # return no internal operation - PAIR }; # respect the calling convention - storage unit; - parameter unit; - - -Example contract with entrypoints -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -The following contract maintains a number in its storage. It has two -entrypoints ``add`` and ``sub`` to modify it, and the default -entrypoint, of type ``unit`` will reset it to ``0``. - -:: - - { parameter (or (or (nat %add) (nat %sub)) (unit %default)) ; - storage int ; - code { AMOUNT ; PUSH mutez 0 ; ASSERT_CMPEQ ; UNPAIR ; - IF_LEFT - { IF_LEFT { ADD } { SWAP ; SUB } } - { DROP ; DROP ; PUSH int 0 } ; - NIL operation ; PAIR } } - -Multisig contract -~~~~~~~~~~~~~~~~~ - -The multisig is a typical access control contract. The ownership of -the multisig contract is shared between ``N`` participants represented -by their public keys in the contract's storage. Any action on the -multisig contract needs to be signed by ``K`` participants where the -threshold ``K`` is also stored in the storage. - -To avoid replay of the signatures sent to the contract, the signed -data include not only a description of the action to perform but also -the address of the multisig contract and a counter that gets -incremented at each successful call to the contract. - -The multisig commands of :ref:`Tezos command line client ` -use this -smart contract. Moreover, `functional correctness of this contract has -been verified -`__ -using the Coq proof assistant. - - -.. code-block:: michelson - - parameter (pair - (pair :payload - (nat %counter) # counter, used to prevent replay attacks - (or :action # payload to sign, represents the requested action - (pair :transfer # transfer tokens - (mutez %amount) # amount to transfer - (contract %dest unit)) # destination to transfer to - (or - (option %delegate key_hash) # change the delegate to this address - (pair %change_keys # change the keys controlling the multisig - (nat %threshold) # new threshold - (list %keys key))))) # new list of keys - (list %sigs (option signature))); # signatures - - storage (pair (nat %stored_counter) (pair (nat %threshold) (list %keys key))) ; - - code - { - UNPAIR ; SWAP ; DUP ; DIP { SWAP } ; - DIP - { - UNPAIR ; - # pair the payload with the current contract address, to ensure signatures - # can't be replayed across different contracts if a key is reused. - DUP ; SELF ; ADDRESS ; CHAIN_ID ; PAIR ; PAIR ; - PACK ; # form the binary payload that we expect to be signed - DIP { UNPAIR @counter ; DIP { SWAP } } ; SWAP - } ; - - # Check that the counters match - UNPAIR @stored_counter; DIP { SWAP }; - ASSERT_CMPEQ ; - - # Compute the number of valid signatures - DIP { SWAP } ; UNPAIR @threshold @keys; - DIP - { - # Running count of valid signatures - PUSH @valid nat 0; SWAP ; - ITER - { - DIP { SWAP } ; SWAP ; - IF_CONS - { - IF_SOME - { SWAP ; - DIP - { - SWAP ; DIIP { DIP { DUP } ; SWAP } ; - # Checks signatures, fails if invalid - CHECK_SIGNATURE ; ASSERT ; - PUSH nat 1 ; ADD @valid } } - { SWAP ; DROP } - } - { - # There were fewer signatures in the list - # than keys. Not all signatures must be present, but - # they should be marked as absent using the option type. - FAIL - } ; - SWAP - } - } ; - # Assert that the threshold is less than or equal to the - # number of valid signatures. - ASSERT_CMPLE ; - DROP ; DROP ; - - # Increment counter and place in storage - DIP { UNPAIR ; PUSH nat 1 ; ADD @new_counter ; PAIR} ; - - # We have now handled the signature verification part, - # produce the operation requested by the signers. - NIL operation ; SWAP ; - IF_LEFT - { # Transfer tokens - UNPAIR ; UNIT ; TRANSFER_TOKENS ; CONS } - { IF_LEFT { - # Change delegate - SET_DELEGATE ; CONS } - { - # Change set of signatures - DIP { SWAP ; CAR } ; SWAP ; PAIR ; SWAP }} ; - PAIR } - - - -Full grammar ------------- - -:: - - ::= - | - | - | - | Unit - | True - | False - | Pair - | Left - | Right - | Some - | None - | { ; ... } - | { Elt ; ... } - | instruction - ::= - | [0-9]+ - ::= - | - | - - ::= - | "*" - ::= - | \" - | \r - | \n - | \t - | \b - | \\ - | [^"\] - ::= - | 0x[0-9a-fA-F]+ - ::= - | { ... } - | DROP - | DROP - | DUP - | SWAP - | DIG - | DUG - | PUSH - | SOME - | NONE - | UNIT - | IF_NONE { ... } { ... } - | PAIR - | CAR - | CDR - | LEFT - | RIGHT - | IF_LEFT { ... } { ... } - | NIL - | CONS - | IF_CONS { ... } { ... } - | SIZE - | EMPTY_SET - | EMPTY_MAP - | EMPTY_BIG_MAP - | MAP { ... } - | ITER { ... } - | MEM - | GET - | UPDATE - | IF { ... } { ... } - | LOOP { ... } - | LOOP_LEFT { ... } - | LAMBDA { ... } - | EXEC - | APPLY - | DIP { ... } - | DIP { ... } - | FAILWITH - | CAST - | RENAME - | CONCAT - | SLICE - | PACK - | UNPACK - | ADD - | SUB - | MUL - | EDIV - | ABS - | ISNAT - | INT - | NEG - | LSL - | LSR - | OR - | AND - | XOR - | NOT - | COMPARE - | EQ - | NEQ - | LT - | GT - | LE - | GE - | SELF - | CONTRACT - | TRANSFER_TOKENS - | SET_DELEGATE - | CREATE_ACCOUNT - | CREATE_CONTRACT { ... } - | IMPLICIT_ACCOUNT - | NOW - | AMOUNT - | BALANCE - | CHECK_SIGNATURE - | BLAKE2B - | SHA256 - | SHA512 - | HASH_KEY - | STEPS_TO_QUOTA - | SOURCE - | SENDER - | ADDRESS - | CHAIN_ID - ::= - | - | key - | unit - | signature - | option - | list - | set - | operation - | contract - | pair - | or - | lambda - | map - | big_map - | chain_id - ::= - | - | pair - ::= - | int - | nat - | string - | bytes - | mutez - | bool - | key_hash - | timestamp - | address - - -Reference implementation ------------------------- - -The language is implemented in OCaml as follows: - -- The lower internal representation is written as a GADT whose type - parameters encode exactly the typing rules given in this - specification. In other words, if a program written in this - representation is accepted by OCaml's typechecker, it is guaranteed - type-safe. This is of course also valid for programs not - handwritten but generated by OCaml code, so we are sure that any - manipulated code is type-safe. - - In the end, what remains to be checked is the encoding of the typing - rules as OCaml types, which boils down to half a line of code for - each instruction. Everything else is left to the venerable and well - trusted OCaml. - -- The interpreter is basically the direct transcription of the - rewriting rules presented above. It takes an instruction, a stack and - transforms it. OCaml's typechecker ensures that the transformation - respects the pre and post stack types declared by the GADT case for - each instruction. - - The only things that remain to be reviewed are value dependent - choices, such as we did not swap true and false when - interpreting the IF instruction. - -- The input, untyped internal representation is an OCaml ADT with - only 5 grammar constructions: ``String``, ``Int``, ``Bytes``, ``Seq`` and - ``Prim``. It is the target language for the parser, since not all - parsable programs are well typed, and thus could simply not be - constructed using the GADT. - -- The typechecker is a simple function that recognizes the abstract - grammar described in section X by pattern matching, producing the - well-typed, corresponding GADT expressions. It is mostly a checker, - not a full inferrer, and thus takes some annotations (basically the - input and output of the program, of lambdas and of uninitialized maps - and sets). It works by performing a symbolic evaluation of the - program, transforming a symbolic stack. It only needs one pass over - the whole program. - - Here again, OCaml does most of the checking, the structure of the - 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. diff --git a/docs/007/proof_of_stake.rst b/docs/007/proof_of_stake.rst deleted file mode 100644 index 28e800266a9fc06bfa322498f3dd5540b877fed3..0000000000000000000000000000000000000000 --- a/docs/007/proof_of_stake.rst +++ /dev/null @@ -1,413 +0,0 @@ -.. _proof-of-stake: - -Proof-of-stake in Tezos -======================= - -This document provides an in-depth description of the Tezos -proof-of-stake algorithm as implemented in the current protocol -(namely `PsCARTHA` on `mainnet`). - -Brief Overview --------------- - -A blockchain is a linked list of **blocks**. In Tezos, blocks to be -added to the blockchain are agreed upon through a proof-of-stake -consensus mechanism. Proof-of-stake means that participants in the -consensus algorithm are chosen in function of their stake. In Tezos, a -participant needs to have a minimum stake of 8,000 ꜩ (which is -called a **roll**). If one does not have enough stake to participate -on its own or does not want to set up the needed infrastructure, (s)he -can use **delegation**. Therefore, in Tezos, participants in the -consensus algorithm are called **delegates**. There are two roles a -delegate can have: that of a **baker**, that is a delegate that -creates blocks, or that of an **endorser**, that is a delegate that -contributes in agreeing on a block by **endorsing** that block. - -**Baking rights** and **endorsing rights** are determined at the -beginning of a **cycle** (a chunk of blocks) by a follow-the-satoshi -strategy starting from a **random seed** computed from information -already found on the blockchain. - -To incentivize participation in the consensus algorithm, delegates are -**rewarded** for their baking and endorsing. As a counter-measure -against double-baking or double-endorsement a **security deposit** is -frozen from the delegate's account. The deposit is either released -after a number of cycles or burnt in case of proven bad behavior. - -The remainder of this document contains a detailed description of -the notions which are in bold in the text above. - -Further External Resources -~~~~~~~~~~~~~~~~~~~~~~~~~~ - -The original design of the proof-of-stake mechanism in Tezos can be -found in the `whitepaper -`_. -The following blog posts present the intuition behind the changes to the original consensus algorithm: - -- https://blog.nomadic-labs.com/analysis-of-emmy.html, -- https://blog.nomadic-labs.com/emmy-an-improved-consensus-algorithm.html, -- https://blog.nomadic-labs.com/a-new-reward-formula-for-carthage.html. - -Here are a few more resources that present Tezos' proof-of-stake -mechanism: - -- `Proof of Stake `_ -- `Liquid Proof-of-Stake `_ - -Please note that these external resources may contain outdated information. - -Blocks ------- - -The Tezos blockchain is a linked list of blocks. Blocks contain a -header and a list of operations. The header itself decomposes into a -shell header (common to all protocols) and a protocol-specific header. - -Shell header -~~~~~~~~~~~~ - -The shell header contains - -- ``level``: the height of the block, from the genesis block -- ``proto``: number of protocol changes since genesis (mod 256) -- ``predecessor``: the hash of the preceding block. -- ``timestamp``: the timestamp at which the block is claimed to have - been created. -- ``validation_pass``: number of validation passes (also number of - lists of lists of operations) -- ``fitness``: a sequence of sequences of unsigned bytes, ordered by - length and then lexicographically. It represents the claimed fitness - of the chain ending in this block. -- ``operations_hash``: the hash of a list of root hashes of Merkle - trees of operations. There is one list of operations per - validation pass. -- ``context`` Hash of the state of the context after application of - this block. - -Protocol header -~~~~~~~~~~~~~~~ - -- ``signature``: a digital signature of the shell and protocol headers - (excluding the signature itself). -- ``priority``: the position in the priority list of delegates at which - the block was baked. -- ``seed_nonce_hash``: a commitment to a random number, used to - generate entropy on the chain. Present in only one out of - ``BLOCKS_PER_COMMITMENT`` = 32 blocks. -- ``proof_of_work_nonce``: a nonce used to pass a low-difficulty - proof-of-work for the block, as a spam prevention measure. - -Block size -~~~~~~~~~~ - -Tezos does not download blocks all at once but rather considers -headers and various types of operations separately. Transactions are -limited by a total maximum size of 512kB (that is 5MB every 10 minutes -at most). - -Consensus operations (endorsements, denunciations, reveals) are -limited in terms of number of operations (though the defensive -programming style also puts limits on the size of operations it -expects). This ensures that critical operations do not compete with -transactions for block space. - -Fitness -~~~~~~~ - -To each block, we associate a measure of `fitness` which determines the -quality of the chain leading to that block. This measure is simply the -length of the chain (as in Bitcoin). More precisely, the fitness of a -block is 1 plus the fitness of the previous block. The shell changes -the head of the chain to the valid block that has the highest fitness. - -Cycles ------- - -Blocks in Tezos are grouped into *cycles* of -``BLOCKS_PER_CYCLE`` = 4,096 blocks. Since blocks are at least -``TIME_BETWEEN_BLOCKS[0]`` = one minute apart, this means a cycle lasts *at -least* 2 days, 20 hours, and 16 minutes. In the following description, -the current cycle is referred to as ``n``, it is the ``n``-th cycle from the -beginning of the chain. Cycle ``(n-1)`` is the cycle that took place -before the current one, cycle ``(n-2)`` the one before, cycle ``(n+1)`` -the one after, etc. - -At any point, the shell will not implicitly accept a branch whose -fork point is in a cycle more than ``PRESERVED_CYCLES`` = 5 cycles in the -past (that is *at least* 14 days, 5 hours, and 20 minutes). - -Delegation ----------- - -Tezos uses a delegated proof-of-stake model. The acronym DPOS has come to -designate a specific type of algorithm used, for instance in Bitshares. -This is *not* the model used in Tezos, though there is a concept -of delegation. - -Delegates -~~~~~~~~~ - -Tokens are controlled through a private key called the -*manager key*. Tezos accounts let the manager specify a public -delegate key. This key may be controlled by the managers themselves, or -by another party. The responsibility of the delegate is to take part in -the proof-of-stake consensus algorithm and the governance of Tezos. - -The manager can generally change the delegate at any time, though -contracts can be marked to specify an immutable delegate. Though -delegation can be changed dynamically, the change only becomes effective -after a few cycles. - -There are also default accounts in Tezos, which are just the hash of the -public key. These accounts do not have an attached delegate key and do -not participate in the proof-of-stake algorithm. - -Finally, delegate accounts (used for placing safety deposits) are -automatically delegated to the delegate itself. - -Active and passive delegates -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -A delegate can be marked as either active or passive. A passive delegate -cannot be selected for baking or endorsing. - -A delegate becomes passive for cycle ``n`` when they fail to create -any blocks or endorsements in the past ``PRESERVED_CYCLES`` -cycles, that is, in cycles ``n-1``, ``n-2``, ..., ``n - -PRESERVED_CYCLES``. - -Discussion: giving ``PRESERVED_CYCLES`` a small value means -the chain adapts more quickly to participants disappearing. It's not -unlike the "difficulty adjustment" of Bitcoin. However, a long value -would ensure that a minority fork progresses more slowly for a longer -period of time than the majority fork. ``PRESERVED_CYCLES`` -gives the majority chain a "headstart". - -Rolls -~~~~~ - -In theory, it would be possible to give each token a serial number -and track the specific tokens assigned to specific delegates. However, -it would be too demanding of nodes to track assignments at such a -granular level. Instead, we introduce the concept of rolls. A *roll* -represents a set of coins delegated to a given key. A roll holds -``TOKENS_PER_ROLL`` = 8,000 tokens. When tokens are moved, or a -delegate for a contract is changed, the rolls change delegate -according to the following algorithm. - -Each delegate has a stack of roll identifiers plus some "change" which is always -an amount smaller than ``TOKENS_PER_ROLL``. When tokens are moved from -one delegate to the other, first, the change is used. If it is not -enough, rolls need to be "broken" which means that they move from the -delegate stack to a global, unallocated, roll stack. This is done until -the amount is covered, and some change possibly remains. - -Then, the other delegate is credited. First, the amount is added to the -"change". If it becomes greater than ``TOKENS_PER_ROLL``, then rolls -are unstacked from the global unallocated roll stack onto the delegate -stack. If the global stack is empty, a fresh roll is created. - -This preserves the property that if the delegate is changed through -several transactions, the roll assignment is preserved, even if each -operation moves less than a full roll. - -The advantage of tracking tokens in this way is that a delegate creating -a malicious fork cannot easily change the specific rolls assigned to -them, even if they control the underlying tokens and shuffle them -around. - -Roll snapshots -~~~~~~~~~~~~~~ - -Roll snapshots represent the state of rolls for a given block. Roll -snapshots are taken at each level whose position within the cycle is -one unit less than a multiple of ``BLOCKS_PER_ROLL_SNAPSHOT`` = 256; -that is, at levels with cycle position 255, 511, ..., 4095. Roll -snapshots are therefore taken 16 times per cycle. - -There is a tradeoff between memory consumption and economic -efficiency. If roll snapshots are too frequent, they will consume a -lot of memory. If they are too rare, strategic participants could -purchase many tokens in anticipation of a snapshot and resell them -right after. - -Baking -~~~~~~ - -Baking is the action of producing and signing a block. -In Bitcoin, the right to produce a block is associated with solving a -proof-of-work puzzle. In Tezos, the right to produce a block in -cycle ``n`` is assigned to a randomly selected roll in a randomly -selected roll snapshot from cycle ``n-PRESERVED_CYCLES-2``. - -We admit, for the time being, that the protocol generates a random -seed for each cycle. From this random seed, we can seed a -cryptographically secure pseudo-random number generator which is used -to draw baking rights for a cycle. - -Each level is associated with a priority list of delegates. -This list is obtained by randomly selecting an active roll for each -position in the list, and then taking the owner of the selected roll. -As the draw is independent for each list position, it is possible that -the same public key appears multiple times in this list. -The first baker in the list is the first one who can bake a block at -that level. -If a delegate is for some reason unable to bake, the next delegate in -the list can step up and bake the block. -The elements of the list that contain a certain delegate are also -called the *baking slots* of that delegate, and the indexes of these -slots are called *priorities*. - -Baking a block gives a block reward (detailed below) plus -all fees paid by transactions inside the block. - -Endorsements -~~~~~~~~~~~~ - -To each level, we associate a list of ``ENDORSERS_PER_BLOCK`` = -32 *endorsers*. Endorsers are drawn similarly as bakers, by randomly -selecting 32 active rolls with replacement. - -Each endorser verifies the last block that was baked, say at the level -``n``, and emits an endorsement operation. The endorsement operations -are then baked in block ``n+1``. Once block ``n+1`` is baked, no other -endorsement for block ``n`` will be considered valid. - -An endorser may have more than one endorsement -slot. However, the endorser injects a single endorsement operation, -which represents all of its endorsement slots. In what follows, when -we say "the number of endorsements a block contains", we do not refer -to the number of endorsement operations, but to the number of -endorsement slots covered by the contained endorsement -operations. (In the code base, the number of filled endorsement slots -is called the block's endorsing power.) - -Minimal block delays -~~~~~~~~~~~~~~~~~~~~ - -A block is valid only if its timestamp has a minimal delay with -respect to the previous block’s timestamp. The minimal delay is given -by the following expression: ``TIME_BETWEEN_BLOCKS[0] + -TIME_BETWEEN_BLOCKS[1] * p +`` ``DELAY_PER_MISSING_ENDORSEMENT * MAX -(0, INITIAL_ENDORSERS - e)`` where ``TIME_BETWEEN_BLOCKS[0]`` = 60 -seconds, ``TIME_BETWEEN_BLOCKS[1]`` = 40 seconds, -``DELAY_PER_MISSING_ENDORSEMENT`` = 8 seconds, ``INITIAL_ENDORSERS`` = -24, ``p`` is the block's priority at which the block was baked, and -``e`` is the number of endorsements the block contains. That is, the -higher the priority and the fewer endorsements a block carries the -longer it takes before it can be considered valid. However, if the -block contains more than ``INITIAL_ENDORSERS`` then there is no time -penalty. - -Rewards -~~~~~~~ - -Baking a block gives a block reward of ``e * -BAKING_REWARD_PER_ENDORSEMENT[p']`` plus all fees paid by the -transactions contained in the block, where -``BAKING_REWARD_PER_ENDORSEMENT`` = ``[1.250ꜩ, 0.1875ꜩ]``, -``e`` is the number of endorsements the block contains, ``p`` is the -priority at which the block was baked, and ``p'`` is 0 if ``p`` is -0 and is 1 if ``p`` is bigger than 0. That is, a delegate -producing a block of priority 0 will be rewarded ``e * 1.25`` -ꜩ. If a delegate produces a block at priority 1 or higher, then -the reward is ``e * 0.1875`` ꜩ. - -Endorsers also receive a reward (at the same time as block creators -do). The reward is ``ENDORSEMENT_REWARD[p']``, where -``ENDORSEMENT_REWARD`` = ``[1.250ꜩ, 0.833333ꜩ]``, where ``p'`` -is as above. That is, a delegate endorsing a block of priority 0 -will be rewarded ``e * 1.25`` ꜩ, with ``e`` the number of endorsement -slots attributed to the delegate for this level. Moreover, endorsing -blocks of priority 1 or higher will be rewarded ``e * 0.833333`` -ꜩ. - -Security deposits -~~~~~~~~~~~~~~~~~ - -The cost of a security deposit is ``BLOCK_SECURITY_DEPOSIT`` = 512 ꜩ -per block created and ``ENDORSEMENT_SECURITY_DEPOSIT`` = 64 ꜩ per -endorsement slot. - -Each delegate key has an associated security deposit account. -When a delegate bakes or endorses a block the security deposit is -automatically moved to the deposit account where it is frozen for -``PRESERVED_CYCLES`` cycles, after which it is automatically moved -back to the baker's main account. - -Since deposits are locked for a period of ``PRESERVED_CYCLES`` one can -compute that at any given time, about ((``BLOCK_SECURITY_DEPOSIT`` + -``ENDORSEMENT_SECURITY_DEPOSIT`` \* ``ENDORSERS_PER_BLOCK``) \* -(``PRESERVED_CYCLES`` + 1) \* ``BLOCKS_PER_CYCLE``) tokens of all -staked tokens should be held as security deposits. For instance, if -the amount of staked tokens is 720,000,000 ꜩ, then roughly 8.74% of -this amount is stored in security deposits. This percentage also gives -an indication of the minimal amount of tokens a delegate should own in -order to not miss out on creating a block or an endorsement. Please -refer to `this section -`_ -of the documentation for a discussion on (over-)delegation. - -Inflation -~~~~~~~~~ - -Inflation from block rewards and endorsement reward is at most -``ENDORSERS_PER_BLOCK`` \* (``ENDORSEMENT_REWARD[0]`` + -``BAKING_REWARD_PER_ENDORSEMENT[0]``) = -80 ꜩ. This means at most 5.51% annual inflation. - -Random seed -~~~~~~~~~~~ - -Each cycle ``n`` is associated with a random seed. This seed is used to -randomly select a roll snapshot from cycle ``n-2`` and to randomly -select rolls in the selected snapshot. The selected rolls determine -the baking and endorsing rights in cycle ``n+PRESERVED_CYCLES``. - -The random seed for cycle ``n`` is a 256-bit number generated at the -very end of cycle ``n-1`` from nonces to which delegates commit during -cycle ``n-2``. A commitment is the hash of a nonce. The commitment is -generated by the baker who produces the block and is included in the -block header. Every block whose position within the cycle is one unit -less than a multiple of ``BLOCKS_PER_COMMITMENT`` = 32 must contain a -commitment; that is, blocks with cycle positions 31, 63, 95, .... -There are therefore exactly 128 commitments in a cycle. - -The committed nonce must be revealed by the original baker during -cycle ``n-1`` under penalty of forfeiting the rewards and fees of the -block that included the commitment. The associated security deposit is -not forfeited. - -A *nonce revelation* is an operation, and multiple nonce revelations -can thus be included in a block. A baker receives a -``SEED_NONCE_REVELATION_TIP`` = 1/8 ꜩ reward for including a -revelation. Revelations are free operations which do not compete with -transactions for block space. Up to ``MAX_ANON_OPS_PER_BLOCK`` = 132 -revelations, wallet activations and denunciations can be contained in any -given block. - -The seed for cycle ``n`` is obtained as follows: the seed of cycle -``n-1`` is hashed with a constant and then with each nonce revealed in -cycle ``n-1``. - -Accusations ------------ - -If two endorsements are made for the same slot or two blocks at the -same height by a delegate, the evidence can be collected by an accuser -and included in a block for a period of ``PRESERVED_CYCLES``, -including the current cycle. - -This accusation forfeits the entirety of the safety deposit and future -reward up to that point in the cycle. Half is burned, half goes to the -accuser in the form of a block reward. - -In the current protocol, accusations for the *same* incident can be -made several times after the fact. This means that the deposits and -rewards for the entire cycle are forfeited, including any deposit -made, or reward earned, after the incident. - -Pragmatically, any baker who either double bakes or endorses in a -given cycle should immediately stop both baking and endorsing for the -rest of that cycle. diff --git a/docs/007/voting.rst b/docs/007/voting.rst deleted file mode 100644 index 85e13a4e4184c59fbf0e6cb4419ed888179e7dbe..0000000000000000000000000000000000000000 --- a/docs/007/voting.rst +++ /dev/null @@ -1,189 +0,0 @@ -The Voting Process -================== - -The design of the Tezos Node allows the consensus protocol to be -amended, that is replaced by another set of OCaml files which -implement the API of a valid protocol. - -In the current protocol the amendment procedure is guided by a voting -procedure where delegates can propose, select and test a candidate -protocol before activating it. -Delegates take part in the amendment procedure with an influence -proportional to their stake, one roll one vote. - -The procedure consists of four periods, each of 32768 blocks (or -~three weeks), for a total of approximately three months. - -Other than this page, there is an excellent overview from `Jacob -Arluck on medium. -`_ - -Periods -------- - -The voting procedure works as follows: - -- `Proposal period`: delegates can submit protocol amendment proposals using - the `proposals` operation. At the end of a proposal period, the proposal with - most supporters is selected and we move to a testing_vote period. - If there are no proposals, or a tie between proposals, a new proposal - period starts. Each delegate can submit a maximum of 20 proposals, - including duplicates. -- `Testing_vote period`: delegates can cast one vote to test or not the winning - proposal using the `ballot` operation. - At the end of a testing_vote period if participation reaches the quorum - and the proposal has a super-majority in favor, we proceed to a testing - period. Otherwise we go back to a proposal period. -- `Testing period`: a test chain is forked for the entire testing period to ensure a - correct migration of the context. - At the end of a testing period we move to a promotion_vote period. -- `Promotion_vote period`: delegates can cast one vote to promote or not the - tested proposal using the `ballot` operation. - At the end of a promotion_vote period if participation reaches the quorum - and the tested proposal has a super-majority in favor, it is activated as - the new protocol. Otherwise we go back to a proposal period. - -It is important to note that the stake of each delegated is computed -at the beginning of each period. - -Super-majority and Quorum -------------------------- - -Both voting periods work in the same way, only the subject of the -vote differs. -During a vote a delegate can cast a single Yea, Nay or Pass vote. -A vote is successful if it has super-majority and the participation -reaches the current quorum. - -`Super-majority` means the Yeas are more than 8/10 of Yeas+Nays votes. -The `participation` is the ratio of all received votes, including -passes, with respect to the number of possible votes. The `quorum` -starts at 80% and at each vote it is updated using the old quorum and -the current participation with the following coefficients:: - - newQ = oldQ * 8/10 + participation * 2/10 - -More details can be found in the file -``src/proto_007_PsDELPH1/lib_protocol/amendment.ml``. - -Operations ----------- - -There are two operations used by the delegates: ``proposals`` and ``ballot``. -A proposal operation can only be submitted during a proposal period. - -:: - - Proposals : { - source: Signature.Public_key_hash.t ; - period: Voting_period_repr.t ; - proposals: Protocol_hash.t list ; } - -Source is the public key hash of the delegate, period is the unique -identifier of each voting period and proposals is a non-empty list of -maximum 20 protocol hashes. -The operation can be submitted more than once but only as long as the -cumulative length of the proposals lists is less than 20. -Duplicate proposals from the same delegate are accounted for in the -maximum number of proposals for that delegate. -However duplicates from the same delegate are not tallied at the end -of the proposal period. - -For example, a delegate submits a proposals operation for protocol A -and B early in the proposal period, later a new protocol C is revealed -and the delegate submits another proposals operation for protocol B -and C. -The list of submissions that will be tallied is [A,B,C] and the - -A ballot operation can only be submitted during one of the voting -periods, and only once per period. - -:: - - Ballot : { - source: Signature.Public_key_hash.t ; - period: Voting_period_repr.t ; - proposal: Protocol_hash.t ; - ballot: Vote_repr.ballot ; } - -Source and period are the same as above, while proposal is the -currently selected proposal and ballot is one of ``Yea``, ``Nay`` or -``Pass``. -The pass vote allows a delegate to not influence a vote but still -allowing it to reach quorum. - -More details can be found, as for all operations, in -``src/proto_007_PsDELPH1/lib_protocol/operation_repr.ml``. -The binary format is described by ``tezos-client describe unsigned -operation``. - -Client Commands ---------------- - -Tezos' client provides a command to show the status of a voting period. -It displays different informations for different kind of periods, as -in the following samples:: - - $ tezos-client show voting period - Current period: "proposal" - Blocks remaining until end of period: 59 - Current proposals: - PsNa6jTtsRfbGaNSoYXNTNM5A7c3Lji22Yf2ZhpFUjQFC17iZVp 400 - - $ tezos-client show voting period - Current period: "testing_vote" - Blocks remaining until end of period: 63 - Current proposal: PsNa6jTtsRfbGaNSoYXNTNM5A7c3Lji22Yf2ZhpFUjQFC17iZVp - Ballots: { "yay": 400, "nay": 0, "pass": 0 } - Current participation 20.00%, necessary quorum 80.00% - Current in favor 400, needed supermajority 320 - - $ tezos-client show voting period - Current period: "testing" - Blocks remaining until end of period: 64 - Current proposal: PsNa6jTtsRfbGaNSoYXNTNM5A7c3Lji22Yf2ZhpFUjQFC17iZVp - -It should be noted that the number 400 above is a number of rolls. -The proposal has a total of 400 rolls, which may come from several -delegates. The same applies for the ballots, there are 400 rolls in -favor of testing protocol PsNa6jTt. - -Submit proposals -~~~~~~~~~~~~~~~~ - -During a proposal period, the list of proposals can be submitted with:: - - tezos-client submit proposals for ... - -Remember that each delegate can submit a maximum of 20 protocol -hashes including duplicates. -Moreover each proposal is accepted only if it meets one of the -following two conditions: - -- the protocol hash was already proposed on the network. In this case - we can submit an additional proposal that "upvotes" an existing one - and our rolls are added to the ones already supporting the proposal. -- the protocol is known by the node. In particular the first proposer - of a protocol should be able to successfully inject the protocol in - its node which performs some checks, compiles and loads the - protocol. - -Submit ballots -~~~~~~~~~~~~~~ - -During a voting period, being it a testing vote or a promotion vote, -ballots can be submitted once with:: - - tezos-client submit ballot for - -Other resources -~~~~~~~~~~~~~~~ - -For more details on the client commands refer to the manual at -:ref:`client_manual_007`. - -For vote related RPCs check the :ref:`rpc_index` under the prefix -``vote/``. - -For Ledger support refer to Obsidian Systems' `documentation -`_. diff --git a/docs/008/cli-commands.rst b/docs/008/cli-commands.rst index cf91ed3bce28864c8a2629e74bcdaaf07f055166..bf498f859027eeeec4dafefbb4ec3fe5fd20c8e3 100644 --- a/docs/008/cli-commands.rst +++ b/docs/008/cli-commands.rst @@ -1,3 +1,4 @@ +.. _cli_commands: .. _cli_commands_008: ********************** @@ -17,6 +18,7 @@ The rest of this page documents the protocol-dependent tools. The protocol-independent tools are documented :ref:`here `. +.. _client_manual: .. _client_manual_008: Client manual @@ -26,6 +28,7 @@ Client manual :file: tezos-client-008.html +.. _baker_manual: .. _baker_manual_008: Baker manual @@ -35,6 +38,7 @@ Baker manual :file: tezos-baker-008.html +.. _endorser_manual: .. _endorser_manual_008: Endorser manual @@ -44,6 +48,7 @@ Endorser manual :file: tezos-endorser-008.html +.. _accuser_manual: .. _accuser_manual_008: Accuser manual diff --git a/docs/008/glossary.rst b/docs/008/glossary.rst index cedbf2c26f5373874d35f1db8d5f1c22b00481bd..11bf15aa12f7fd7626d2560dffbed890e404a120 100644 --- a/docs/008/glossary.rst +++ b/docs/008/glossary.rst @@ -108,6 +108,7 @@ _`Implicit account` letters `tz` followed by `1`, `2` or `3` (depending on the signature scheme) and finally the hash of the public key. +.. _glossary_michelson: .. _glossary_michelson_008: Michelson diff --git a/docs/008/michelson.rst b/docs/008/michelson.rst index 6bca54b760aac9c66a15707d73b9a9e9c7be6aa6..c484aa84efc82fff374044a5b63c0364d623faf2 100644 --- a/docs/008/michelson.rst +++ b/docs/008/michelson.rst @@ -1,3 +1,4 @@ +.. _michelson: .. _michelson_008: Michelson: the language of Smart Contracts in Tezos @@ -1484,6 +1485,7 @@ value that was previously stored in the ``map`` at the same key as Operations on ``big_maps`` ~~~~~~~~~~~~~~~~~~~~~~~~~~ +.. _OperationsOnBigMaps: .. _OperationsOnBigMaps_008: Big maps have three possible representations. A map literal is always @@ -1861,6 +1863,7 @@ until it is actually originated. The parameter must be consistent with the one expected by the contract, unit for an account. +.. _MichelsonSetDelegate: .. _MichelsonSetDelegate_008: - ``SET_DELEGATE``: Set or withdraw the contract's delegation. @@ -2226,6 +2229,7 @@ comprehensive description of the Sapling protocol. with memo_size `ms` +.. _MichelsonTickets: .. _MichelsonTickets_008: Operations on tickets @@ -2545,6 +2549,7 @@ A typing rule can be inferred: Concrete syntax --------------- +.. _ConcreteSyntax: .. _ConcreteSyntax_008: The concrete language is very close to the formal notation of the @@ -3090,6 +3095,7 @@ type (which can be changed). For instance the annotated typing rule for Special annotations ~~~~~~~~~~~~~~~~~~~ +.. _SpecialAnnotations: .. _SpecialAnnotations_008: The special variable annotations ``@%`` and ``@%%`` can be used on instructions diff --git a/docs/008/proof_of_stake.rst b/docs/008/proof_of_stake.rst index b84bc8c82b3bd75c398dc3a0673534c5057d3cdd..9a112967e5ca55389fb7541030f682ed73c7558d 100644 --- a/docs/008/proof_of_stake.rst +++ b/docs/008/proof_of_stake.rst @@ -1,3 +1,4 @@ +.. _proof-of-stake: .. _proof-of-stake_008: Proof-of-stake in Tezos diff --git a/docs/008/sapling.rst b/docs/008/sapling.rst index e15a0b76e8d44ddf92b4a26d9b81032ea311e973..d7bfe204f0e610efd32ab841716061d77a97e51d 100644 --- a/docs/008/sapling.rst +++ b/docs/008/sapling.rst @@ -1,3 +1,4 @@ +.. _sapling_dev: .. _sapling_dev_008: **The features described in this page are experimental and have not undergone any security review.** diff --git a/docs/008/voting.rst b/docs/008/voting.rst index c1ae8f32d97aa1c6e4a77e30d75a7075f3485c8c..1cdc640081c8ef6bf15f567c99f04fee876f2174 100644 --- a/docs/008/voting.rst +++ b/docs/008/voting.rst @@ -186,7 +186,7 @@ Other resources For more details on the client commands refer to the manual at :ref:`client_manual_008`. -For vote related RPCs check the :ref:`rpc_index_008` under the prefix +For vote related RPCs check the :ref:`rpc_index` under the prefix ``vote/``. For Ledger support refer to Obsidian Systems' `documentation diff --git a/docs/009_BA/cli-commands.rst b/docs/009_BA/cli-commands.rst index 32dffd1b716e985f448ea755c6d3efcae3677e7b..f2df883816ee91106bfd5980139e8128bf67cc95 100644 --- a/docs/009_BA/cli-commands.rst +++ b/docs/009_BA/cli-commands.rst @@ -1,4 +1,4 @@ -.. _cli_commands_009: +.. _cli_commands_009_BA: ********************** Command Line Interface @@ -17,7 +17,7 @@ The rest of this page documents the protocol-dependent tools. The protocol-independent tools are documented :ref:`here `. -.. _client_manual_009: +.. _client_manual_009_BA: Client manual ============= @@ -26,7 +26,7 @@ Client manual :file: tezos-client-009.html -.. _baker_manual_009: +.. _baker_manual_009_BA: Baker manual ============ @@ -35,7 +35,7 @@ Baker manual :file: tezos-baker-009.html -.. _endorser_manual_009: +.. _endorser_manual_009_BA: Endorser manual =============== @@ -44,7 +44,7 @@ Endorser manual :file: tezos-endorser-009.html -.. _accuser_manual_009: +.. _accuser_manual_009_BA: Accuser manual ============== diff --git a/docs/009_BA/glossary.rst b/docs/009_BA/glossary.rst index d773966c9e662c012d1171ac0045690664599333..fa59846ff9c0c3e1d61978933ead8de30e8c4b29 100644 --- a/docs/009_BA/glossary.rst +++ b/docs/009_BA/glossary.rst @@ -108,7 +108,7 @@ _`Implicit account` letters `tz` followed by `1`, `2` or `3` (depending on the signature scheme) and finally the hash of the public key. -.. _glossary_michelson_009: +.. _glossary_michelson_009_BA: Michelson The built-in language used by a `smart contract`_. @@ -136,7 +136,7 @@ _`Roll` will be given twice as many rights to bake. _`Smart contract` - Account_ which is associated to a :ref:`Michelson ` script. They are + Account_ which is associated to a :ref:`Michelson ` script. They are created with an explicit origination_ operation and are therefore sometimes called originated accounts. The address of a smart contract always starts with the letters ``KT1``. diff --git a/docs/009_BA/michelson.rst b/docs/009_BA/michelson.rst index 0ef06e05a2ac457047598582dffd015d5056c462..62b29c676f7357e7238931df6fef65f56bb27bac 100644 --- a/docs/009_BA/michelson.rst +++ b/docs/009_BA/michelson.rst @@ -1,4 +1,4 @@ -.. _michelson_009: +.. _michelson_009_BA: Michelson: the language of Smart Contracts in Tezos =================================================== @@ -278,7 +278,7 @@ constructors is fixed by this specification. Michelson does not let the programmer introduce its own types. Be aware that the syntax used in the specification may differ from -the :ref:`concrete syntax `. In particular +the :ref:`concrete syntax `. In particular some instructions are annotated with types that are not present in the concrete language because they are synthesized by the typechecker. @@ -490,7 +490,7 @@ Core data types and notations intends to store large amounts of data in a map. They have higher gas costs than standard maps as data is lazily deserialized. A ``big_map`` cannot appear inside another ``big_map``. See the - section on :ref:`operations on big maps ` + section on :ref:`operations on big maps ` for a description of the syntax of values of type ``big_map (k) (t)`` and available operations. @@ -1485,7 +1485,7 @@ value that was previously stored in the ``map`` at the same key as Operations on ``big_maps`` ~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. _OperationsOnBigMaps_009: +.. _OperationsOnBigMaps_009_BA: Big maps have three possible representations. A map literal is always a valid representation for a big map. Big maps can also be represented @@ -1717,9 +1717,9 @@ Domain specific data types - ``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 :ref:`Sapling` transaction +- ``sapling_transaction ms``: A :ref:`Sapling` transaction -- ``sapling_state ms``: A :ref:`Sapling` state +- ``sapling_state ms``: A :ref:`Sapling` state - ``ticket (t)``: A ticket used to authenticate information of type ``(t)`` on-chain. @@ -1862,7 +1862,7 @@ until it is actually originated. The parameter must be consistent with the one expected by the contract, unit for an account. -.. _MichelsonSetDelegate_009: +.. _MichelsonSetDelegate_009_BA: - ``SET_DELEGATE``: Set or withdraw the contract's delegation. @@ -2201,7 +2201,7 @@ BLS12-381 primitives Sapling operations ~~~~~~~~~~~~~~~~~~ -Please see the :ref:`Sapling integration` page for a more +Please see the :ref:`Sapling integration` page for a more comprehensive description of the Sapling protocol. - ``SAPLING_VERIFY_UPDATE``: verify and apply a transaction on a Sapling state. @@ -2227,7 +2227,7 @@ comprehensive description of the Sapling protocol. with memo_size `ms` -.. _MichelsonTickets_009: +.. _MichelsonTickets_009_BA: Operations on tickets ~~~~~~~~~~~~~~~~~~~~~ @@ -2546,7 +2546,7 @@ A typing rule can be inferred: Concrete syntax --------------- -.. _ConcreteSyntax_009: +.. _ConcreteSyntax_009_BA: The concrete language is very close to the formal notation of the specification. Its structure is extremely simple: an expression in the @@ -2937,7 +2937,7 @@ Primitive applications can receive one or many annotations. An annotation is a sequence of characters that matches the regular expression ``@%|@%%|%@|[@:%][_0-9a-zA-Z][_0-9a-zA-Z\.%@]*``. Note however that ``@%``, ``@%%`` and ``%@`` are -:ref:`special annotations ` and are not allowed everywhere. +:ref:`special annotations ` and are not allowed everywhere. Annotations come after the primitive name and before its potential arguments. @@ -3091,7 +3091,7 @@ type (which can be changed). For instance the annotated typing rule for Special annotations ~~~~~~~~~~~~~~~~~~~ -.. _SpecialAnnotations_009: +.. _SpecialAnnotations_009_BA: The special variable annotations ``@%`` and ``@%%`` can be used on instructions ``CAR``, ``CDR``, and ``UNPAIR``. It means to use the accessed field name (if any) as @@ -3359,7 +3359,7 @@ data include not only a description of the action to perform but also the address of the multisig contract and a counter that gets incremented at each successful call to the contract. -The multisig commands of :ref:`Tezos command line client ` +The multisig commands of :ref:`Tezos command line client ` use this smart contract. Moreover, `functional correctness of this contract has been verified diff --git a/docs/009_BA/proof_of_stake.rst b/docs/009_BA/proof_of_stake.rst index 41b3de68647a3fef64fb20a4886a61f277dd1893..002055e6aac7f356dae7f92f179ab86b00947cd5 100644 --- a/docs/009_BA/proof_of_stake.rst +++ b/docs/009_BA/proof_of_stake.rst @@ -1,4 +1,4 @@ -.. _proof-of-stake_009: +.. _proof-of-stake_009_BA: Proof-of-stake in Tezos ======================= diff --git a/docs/009_BA/sapling.rst b/docs/009_BA/sapling.rst index 7aaa00d47487e8018c972162fc7afae8c3a79b00..40c4145ae8ffef66449aaee287752508df660027 100644 --- a/docs/009_BA/sapling.rst +++ b/docs/009_BA/sapling.rst @@ -1,4 +1,4 @@ -.. _sapling_dev_009: +.. _sapling_dev_009_BA: **The features described in this page are experimental and have not undergone any security review.** @@ -180,7 +180,7 @@ Michelson: verify update We introduce two new Michelson types `sapling_state` and `sapling_transaction`, and two instructions called `SAPLING_VERIFY_UPDATE` and `SAPLING_EMPTY_STATE` -(see the :ref:`Michelson reference` +(see the :ref:`Michelson reference` for more details). `SAPLING_EMPTY_STATE` pushes an empty `sapling_state` on the stack. `SAPLING_VERIFY_UPDATE` takes a transaction and a state and returns an diff --git a/docs/009_BA/voting.rst b/docs/009_BA/voting.rst index 4b93333017c71a9cec1a353d54dabd2fbe1d7955..126e960d8050141ab850fcdc124cb5220ffd2925 100644 --- a/docs/009_BA/voting.rst +++ b/docs/009_BA/voting.rst @@ -184,9 +184,9 @@ Other resources ~~~~~~~~~~~~~~~ For more details on the client commands refer to the manual at -:ref:`client_manual_009`. +:ref:`client_manual_009_BA`. -For vote related RPCs check the :ref:`rpc_index_009` under the prefix +For vote related RPCs check the :ref:`rpc_index_009_BA` under the prefix ``vote/``. For Ledger support refer to Obsidian Systems' `documentation diff --git a/docs/Makefile b/docs/Makefile index 56fb46a3ff1289e2e0aa514d6ec3f999588ac808..7dcb8b4cdf7363f9257e332055526e832f472ad8 100644 --- a/docs/Makefile +++ b/docs/Makefile @@ -50,11 +50,6 @@ manuals: main @../tezos-baker-$(EDO_SHORT) man -verbosity 3 -format html | sed "s#${HOME}#\$$HOME#g" > 008/tezos-baker-008.html @../tezos-endorser-$(EDO_SHORT) man -verbosity 3 -format html | sed "s#${HOME}#\$$HOME#g" > 008/tezos-endorser-008.html @../tezos-accuser-$(EDO_SHORT) man -verbosity 3 -format html | sed "s#${HOME}#\$$HOME#g" > 008/tezos-accuser-008.html - # 007 delphi - @../tezos-client -protocol $(DELPHI_LONG) man -verbosity 3 -format html | sed "s#${HOME}#\$$HOME#g" > 007/tezos-client-007.html - @../tezos-baker-$(DELPHI_SHORT) man -verbosity 3 -format html | sed "s#${HOME}#\$$HOME#g" > 007/tezos-baker-007.html - @../tezos-endorser-$(DELPHI_SHORT) man -verbosity 3 -format html | sed "s#${HOME}#\$$HOME#g" > 007/tezos-endorser-007.html - @../tezos-accuser-$(DELPHI_SHORT) man -verbosity 3 -format html | sed "s#${HOME}#\$$HOME#g" > 007/tezos-accuser-007.html # generic @../tezos-admin-client man -verbosity 3 -format html | sed "s#${HOME}#\$$HOME#g" > api/tezos-admin-client.html @../tezos-signer man -verbosity 3 -format html | sed "s#${HOME}#\$$HOME#g" > api/tezos-signer.html @@ -82,8 +77,7 @@ redirectcheck: @cd $$(pwd)/.. ; ./src/tooling/lint.sh --check-redirects xrefscheck: - $(CHECKXREFS) 007 - $(CHECKXREFS) -l 008 + $(CHECKXREFS) 008 $(CHECKXREFS) -l 009 $(CHECKXREFS) -l 009_BA @@ -106,8 +100,7 @@ $(DOCGENDIR)/rpc_doc.exe: @cd .. && dune build docs/$(DOCGENDIR)/rpc_doc.exe rpc: $(DOCGENDIR)/rpc_doc.exe - @dune exec $(DOCGENDIR)/rpc_doc.exe "" > 007/rpc.rst - @dune exec $(DOCGENDIR)/rpc_doc.exe 008 > 008/rpc.rst + @dune exec $(DOCGENDIR)/rpc_doc.exe "" > 008/rpc.rst @dune exec $(DOCGENDIR)/rpc_doc.exe 009 > 009/rpc.rst @dune exec $(DOCGENDIR)/rpc_doc.exe 009_BA > 009_BA/rpc.rst @dune exec $(DOCGENDIR)/rpc_doc.exe alpha > alpha/rpc.rst @@ -132,5 +125,5 @@ html: Makefile api/errors.rst rpc p2p clean: @-rm -Rf "$(BUILDDIR)" - @-rm -Rf api/errors.rst 007/rpc.rst 008/rpc.rst 009/rpc.rst 009_BA/rpc.rst shell/rpc.rst shell/p2p_api.rst - @-rm -Rf api/tezos-*.html api/tezos-*.txt 007/tezos-*.html 008/tezos-*.html 009/tezos-*.html 009_BA/tezos-*.html + @-rm -Rf api/errors.rst 008/rpc.rst 009/rpc.rst 009_BA/rpc.rst shell/rpc.rst shell/p2p_api.rst + @-rm -Rf api/tezos-*.html api/tezos-*.txt 008/tezos-*.html 009/tezos-*.html 009_BA/tezos-*.html diff --git a/docs/_redirects b/docs/_redirects index 4ce4a515c4b98675a8b3494d61c401f525fc701b..56761a4a20173f305c15f8db8f1ebb7b2ba769d2 100644 --- a/docs/_redirects +++ b/docs/_redirects @@ -1,12 +1,12 @@ /api/cli-commands.html /shell/cli-commands.html 302 /007/cli-commands.html /shell/cli-commands.html 302 -/api/rpc.html /007/rpc.html 302 +/api/rpc.html /008/rpc.html 302 /developer/sapling.html /008/sapling.html 302 -/user/glossary.html /007/glossary.html 302 +/user/glossary.html /008/glossary.html 302 /whitedoc/micheline.html /shell/micheline.html 302 -/whitedoc/proof_of_stake.html /007/proof_of_stake.html 302 -/whitedoc/michelson.html /007/michelson.html 302 -/whitedoc/voting.html /007/voting.html 302 +/whitedoc/proof_of_stake.html /008/proof_of_stake.html 302 +/whitedoc/michelson.html /008/michelson.html 302 +/whitedoc/voting.html /008/voting.html 302 /whitedoc/p2p.html /shell/p2p.html 302 /whitedoc/sync.html /shell/sync.html 302 /whitedoc/the_big_picture.html /shell/the_big_picture.html 302 diff --git a/docs/doc_gen/rpc_doc.ml b/docs/doc_gen/rpc_doc.ml index 22cfd2d99e8cea5793d60e40496efc9bcaddee1b..a6fcbe974e1cb007d69411fabcb0c92401291002 100644 --- a/docs/doc_gen/rpc_doc.ml +++ b/docs/doc_gen/rpc_doc.ml @@ -39,14 +39,10 @@ let protocols = "009 Florence", Some "/include/rpc_introduction.rst.inc", "PsFLorenaUUuikDWvMDr6fGBRG8kt3e3D3fHoXK1j1BFRxeSH4i" ); - ( "008", - "008 Edo", - Some "/include/rpc_introduction.rst.inc", - "PtEdo2ZkT9oKpimTah6x2embF25oss54njMuPzkJTEi5RqfdZFA" ); ( "", - "007 Delphi", + "008 Edo", Some "/include/rpc_introduction.rst.inc", - "PsDELPH1Kxsxt8f9eWbxQeRxkjfbxoqM52jvs5Y5fBxWWh4ifpo" ) ] + "PtEdo2ZkT9oKpimTah6x2embF25oss54njMuPzkJTEi5RqfdZFA" ) ] let pp_name ppf = function | [] | [""] -> diff --git a/docs/index.rst b/docs/index.rst index 1ac7217dd701bcca373cf7c3d0ecb6c3c186dfff..e630c4a763803371efd744bd3a995fbb682df1a3 100644 --- a/docs/index.rst +++ b/docs/index.rst @@ -123,17 +123,6 @@ in the :ref:`introduction `. shell/cli-commands shell/rpc -.. toctree:: - :maxdepth: 2 - :caption: 007 Delphi doc: - - 007/michelson - 007/proof_of_stake - 007/voting - 007/glossary - 007/cli-commands - 007/rpc - .. toctree:: :maxdepth: 2 :caption: 008 Edo doc: