diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index b8de4ebed9a2afdac46481dadda94c7f5b1324b3..acdb6ff143469b4e1cb736221c110b3b1de43b84 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -16,7 +16,7 @@ include: variables: ## Please update `scripts/version.sh` accordingly - build_deps_image_version: 5554281d9e3a226cf98b0c9e8721afad2973c150 + build_deps_image_version: ecb12b00769179e6022ad1547b69950781a45061 build_deps_image_name: registry.gitlab.com/tezos/opam-repository public_docker_image_name: docker.io/${CI_PROJECT_PATH} GIT_STRATEGY: fetch diff --git a/.gitlab/ci/build.yml b/.gitlab/ci/build.yml index 96685afcde52c9726cd0e385929b3fd2eb0282ff..a96ea381feff8002b977171c4debdff2e3370761 100644 --- a/.gitlab/ci/build.yml +++ b/.gitlab/ci/build.yml @@ -16,7 +16,6 @@ check_opam_deps: extends: .build_template script: - ./scripts/opam-check.sh - allow_failure: true # This check currently timesout, a fix is in the work timeout: 10m # if it takes more than 10 minutes, then it'll just timeout after 1h check_opam_lint: diff --git a/CHANGES.md b/CHANGES.md index 0dee0de88f40f59e6215143558261250e5669d2d..29fe46cca34c2e8e7430a8baddd1c81aa9c73208 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -19,22 +19,32 @@ be documented here either. ## Node -- Cap the number of expected connections to `100` on the command line +- Added Florence, the current protocol proposal on Mainnet. + This is the version of Florence without baking accounts (`PsFLoren`). + +- Added a new version of the protocol environment (v2). + It is used by Florence. + +- Added built-in network configurations for Edo2net (which runs Edo2, + the current Mainnet protocol) and Florencenet (which runs Florence). + Their corresponding aliases for `--network` are `edo2net` and `florencenet`. + +- Capped the number of expected connections to `100` on the command-line interface. -- Fixes a bug that launched the prevalidator when the node was not +- Fixed a bug that caused the execution of the prevalidator when the node was not bootstrapped. -- Enforce loading of non-embedded protocols before starting the node - allowing the prevalidator to start correctly. +- Enforced loading of non-embedded protocols before starting the node + to allow the prevalidator to start correctly. -- Optimize I/O and CPU usage by removing an unnecessary access to the +- Optimized I/O and CPU usage by removing an unnecessary access to the context during block validation. -- Fixes a bug where any event would allocate more memory than needed - when it were not to be printed. +- Fixed a bug where any event would allocate more memory than needed + when it was not to be printed. -- Add a new RPC for Alpha: `helpers/scripts/normalize_type`. +- Added a new RPC for Alpha: `helpers/scripts/normalize_type`. - Replace Edonet by Edo2net in built-in network configuration. The alias to give to `--network` is now `edo2net`. @@ -45,55 +55,69 @@ be documented here either. - The `--network` option now also accepts the name of a file containing the configuration for a custom network, or a URL from which such a file can be downloaded. + +- Fixed JSON encoding of timestamps before epoch (1970). + Pretty-printing and encoding of dates before epoch in human-readable form (as part + of a JSON value) that failed in the past will now succeed. Binary + form (used when nodes exchange data) was unaffected by the bug. This + may impact some RPC representations of timestamps. + + +- Some RPCs now send their response in chunked transfer encoding. + Additionally, the implementation allows for more concurrency internally: it + allows RPC requests to be treated even if a request is currently being + treated. This leads to some improved response times on some RPC requests. ## Client - Fixed the return code of errors in the client calls to be non-zero. -- Added a new multisig command to change keys and threshold +- Added a new multisig command to change keys and threshold: `set threshold of multisig contract ...`. -- Added a command to perform protocol migrations in persistent mockup mode - `migrate mockup to ` +- Added a command to perform protocol migrations in persistent mockup mode: + `migrate mockup to `. -- Add `--version` flag +- Added the `--version` flag. -- Fixed commands `--mode mockup config show` and `--mode mockup config init` which returned the default values rather than the actual ones. +- Fixed commands `--mode mockup config show` and `--mode mockup config init` + which returned the default values rather than the actual ones. - Replaced command `check that was signed by ` by `check that bytes were signed by ` to differentiate from new command `check that - message was signed by ` + message was signed by `. - Added wallet support for PVSS keys. -- Added support for all protocol constants in Mockup mode +- Added support for all protocol constants in Mockup mode. ## Baker / Endorser / Accuser -- Add `--version` flag +- Added the `--version` flag. -- Fixes the operation ordering in the baker so that the most +- Fixed the operation ordering in the baker so that the most profitable operations are applied first. ## Protocol Compiler And Environment -- Add `--version` flag +- Added the `--version` flag. ## Codec -- Add `--version` flag -- Register some ground encodings including arbitrary precision integers, n-bit - sized integers, and floating point numbers. +- Added the `--version` flag. +- Added support for some base encodings including arbitrary precision integers, n-bit + sized integers, and floating point numbers. ## Docker Images ## Miscellaneous -- Make sure file descriptors are opened with the `O_CLOEXEC` flag. -- Sapling: fix dummy address generator (set correctly the last 5 bits to 0 +- Sapling: fixed dummy address generator (the last 5 bits are now correctly set to 0 instead of the first 5 bits). +- Fixed a bug that caused some file descriptors to be leaked to external processes. + # Version 8.2 ## Node @@ -253,9 +277,9 @@ be documented here either. + PATCH: `/network/peers/` payload `{ acl: [ban,trust,open] }` + PATCH: `/network/point/` payload `{ acl: [ban,trust,open], peer_id: }` where - - `{acl : ban}`: blacklist the given address/peer and remove it from + - `{acl : ban}`: blacklist the given address/peer and remove it from the whitelist if present - - `{acl: trust}`: trust a given address/peer permanently and remove it + - `{acl: trust}`: trust a given address/peer permanently and remove it from the blacklist if present. - `{acl: open}`: removes an address/peer from the blacklist and whitelist. diff --git a/docs/009_BA/cli-commands.rst b/docs/009_BA/cli-commands.rst deleted file mode 100644 index f2df883816ee91106bfd5980139e8128bf67cc95..0000000000000000000000000000000000000000 --- a/docs/009_BA/cli-commands.rst +++ /dev/null @@ -1,53 +0,0 @@ -.. _cli_commands_009_BA: - -********************** -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_009_BA: - -Client manual -============= - -.. raw:: html - :file: tezos-client-009.html - - -.. _baker_manual_009_BA: - -Baker manual -============ - -.. raw:: html - :file: tezos-baker-009.html - - -.. _endorser_manual_009_BA: - -Endorser manual -=============== - -.. raw:: html - :file: tezos-endorser-009.html - - -.. _accuser_manual_009_BA: - -Accuser manual -============== - -.. raw:: html - :file: tezos-accuser-009.html diff --git a/docs/009_BA/glossary.rst b/docs/009_BA/glossary.rst deleted file mode 100644 index dca6ffa8c5c622bf090eba954db56eff4697459a..0000000000000000000000000000000000000000 --- a/docs/009_BA/glossary.rst +++ /dev/null @@ -1,157 +0,0 @@ -Glossary -======== - -This glossary is divided in two sections, the first one concerns Tezos, and -the second one concerns the `economic protocol`_. The definitions in the latter -section may be different for other protocol versions. - -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_009_BA: - -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` Any of the ``proposal``, ``exploration``, - ``cooldown``, ``promotion`` or ``adoption`` stages in the voting - procedure when ammending 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 more - than one roll_ at that moment. For each delegate_, The voting listings - reflects the weight of the vote emitted by the delegate_ when ammending the - `economic protocol`_. diff --git a/docs/009_BA/michelson.rst b/docs/009_BA/michelson.rst deleted file mode 100644 index 62b29c676f7357e7238931df6fef65f56bb27bac..0000000000000000000000000000000000000000 --- a/docs/009_BA/michelson.rst +++ /dev/null @@ -1,3685 +0,0 @@ -.. _michelson_009_BA: - -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 uses a stack, as in the following -example, also with two external operations. - -:: - - +-----------+---------------+--------------------------+ - | executing | emissions | resulting stack | - +-----------+---------------+--------------------------+ - | op 1 | 1a, 1b, 1c | 1a, 1b, 1c | - | op 1a | 1ai, 1aj | 1ai, 1aj, 1b, 1c | - | op 1ai | | 1aj, 1b, 1c | - | op 1aj | | 1b, 1c | - | op 1b | 1bi | 1bi, 1c | - | op 1bi | | 1c | - | op 1c | | | - | op 2 | 2a, 2b | 2a, 2b | - | op 2a | 2ai | 2ai, 2b | - | op 2ai | 2ai1 | 2ai1, 2b | - | op 2ai1 | | 2b | - | op 2b | 2bi | 2bi | - | op 2bi | 2bi1 | 2bi1 | - | op 2bi1 | 2bi2 | 2bi2 | - | op 2bi2 | | | - +-----------+---------------+--------------------------+ - -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. - -- ``never``: The empty type. Since ``never`` has no inhabitant, no value of - this type is allowed to occur in a well-typed program. - -- ``list (t)``: A single, immutable, homogeneous linked list, whose - elements are of type ``(t)``, and that we write ``{}`` for the empty - list or ``{ first ; ... }``. In the semantics, we use chevrons to - denote a subsequence of elements. For instance: ``{ head ; }``. - -- ``pair (l) (r)``: A pair of values ``a`` and ``b`` of types ``(l)`` - and ``(r)``, that we write ``(Pair a b)``. - -- ``pair (t{1}) ... (t{n})`` with ``n > 2``: A shorthand for ``pair (t{1}) (pair (t{2}) ... (pair (t{n-1}) (t{n})) ...)``. - -- ``option (t)``: Optional value of type ``(t)`` that we write ``None`` - or ``(Some v)``. - -- ``or (l) (r)``: A union of two types: a value holding either a value - ``a`` of type ``(l)`` or a value ``b`` of type ``(r)``, that we write - ``(Left a)`` or ``(Right b)``. - -- ``set (t)``: Immutable sets of values of type ``(t)`` that we write as - lists ``{ item ; ... }``, of course with their elements unique, and - sorted. - -- ``map (k) (t)``: Immutable maps from keys of type ``(k)`` of values - of type ``(t)`` that we write ``{ Elt key value ; ... }``, with keys - sorted. - -- ``big_map (k) (t)``: Lazily deserialized maps from keys of type - ``(k)`` of values of type ``(t)``. These maps should be used if 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``. See the - section on :ref:`operations on big maps ` - for a description of the syntax of values of type ``big_map (k) - (t)`` and available operations. - -Core instructions ------------------ - -Control structures -~~~~~~~~~~~~~~~~~~ - -- ``FAILWITH``: Explicitly abort the current program. - -:: - - :: 'a : \_ -> \_ - -This special instruction aborts the current program exposing the top -element of the stack in its error message (first rule below). It makes -the output useless since all subsequent instructions will simply -ignore their usual semantics to propagate the failure up to the main -result (second rule below). Its type is thus completely generic. - -:: - - > FAILWITH / a : _ => [FAILED] - > _ / [FAILED] => [FAILED] - -- ``{}``: Empty sequence. - -:: - - :: 'A -> 'A - - > {} / SA => SA - -- ``{ I ; C }``: Sequence. - -:: - - :: 'A -> 'C - iff I :: [ 'A -> 'B ] - C :: [ 'B -> 'C ] - - > I ; C / SA => SC - where I / SA => SB - and C / SB => SC - -- ``IF bt bf``: Conditional branching. - -:: - - :: bool : 'A -> 'B - iff bt :: [ 'A -> 'B ] - bf :: [ 'A -> 'B ] - - > IF bt bf / True : S => bt / S - > IF bt bf / False : S => bf / S - -- ``LOOP body``: A generic loop. - -:: - - :: bool : 'A -> 'A - iff body :: [ 'A -> bool : 'A ] - - > LOOP body / True : S => body ; LOOP body / S - > LOOP body / False : S => S - -- ``LOOP_LEFT body``: A loop with an accumulator. - -:: - - :: (or 'a 'b) : 'A -> 'b : 'A - iff body :: [ 'a : 'A -> (or 'a 'b) : 'A ] - - > LOOP_LEFT body / (Left a) : S => body ; LOOP_LEFT body / a : S - > LOOP_LEFT body / (Right b) : S => b : S - -- ``DIP code``: Runs code protecting the top element of the stack. - -:: - - :: 'b : 'A -> 'b : 'C - iff code :: [ 'A -> 'C ] - - > DIP code / x : S => x : S' - where code / S => S' - -- ``DIP n code``: Runs code protecting the ``n`` topmost elements of - the stack. In particular, ``DIP 0 code`` is equivalent to ``code`` - and ``DIP 1 code`` is equivalent to ``DIP code``. - -:: - - :: 'a{1} : ... : 'a{n} : 'A -> 'a{1} : ... : 'a{n} : 'B - iff code :: [ 'A -> 'B ] - - > DIP n code / x{1} : ... : x{n} : S => x{1} : ... : x{n} : S' - where code / S => S' - -- ``EXEC``: Execute a function from the stack. - -:: - - :: 'a : lambda 'a 'b : 'C -> 'b : 'C - - > EXEC / a : f : S => r : S - where f / a : [] => r : [] - -- ``APPLY``: Partially apply a tuplified function from the stack. - Values that are not both pushable and storable - (values of type ``operation``, ``contract _`` and ``big map _ _``) - cannot be captured by ``APPLY`` (cannot appear in ``'a``). - -:: - - :: 'a : lambda (pair 'a 'b) 'c : 'C -> lambda 'b 'c : 'C - - > APPLY / a : f : S => { PUSH 'a a ; PAIR ; f } : S - -Stack operations -~~~~~~~~~~~~~~~~ - -- ``DROP``: Drop the top element of the stack. - -:: - - :: _ : 'A -> 'A - - > DROP / _ : S => S - -- ``DROP n``: Drop the `n` topmost elements of the stack. In - particular, ``DROP 0`` is a noop and ``DROP 1`` is equivalent to - ``DROP``. - -:: - - :: 'a{1} : ... : 'a{n} : 'A -> 'A - - > DROP n / x{1} : ... : x{n} : S => S - -- ``DUP``: Duplicate the top element of the stack. - -:: - - :: 'a : 'A -> 'a : 'a : 'A - - > DUP / x : S => x : x : S - -- ``DUP n``: Duplicate the N-th element of the stack. `DUP 1` is equivalent to `DUP`. `DUP 0` is rejected. - -:: - - DUP 1 :: 'a : 'A -> 'a : 'a : 'A - - DUP (n+1) :: 'a : 'A -> 'b : 'a : 'A - iff DUP n :: 'A -> 'b : 'A - - > DUP 1 / x : S => x : x : S - - > DUP (n+1) / x : S => y : x : S - iff DUP n / S => y : S - - -- ``SWAP``: Exchange the top two elements of the stack. - -:: - - :: 'a : 'b : 'A -> 'b : 'a : 'A - - > SWAP / x : y : S => y : x : S - -- ``DIG n``: Take the element at depth ``n`` of the stack and move it - on top. The element on top of the stack is at depth ``0`` so that - ``DIG 0`` is a no-op and ``DIG 1`` is equivalent to ``SWAP``. - -:: - - :: 'a{1} : ... : 'a{n} : 'b : 'A -> 'b : 'a{1} : ... : 'a{n} : 'A - - > DIG n / x{1} : ... : x{n} : y : S => y : x{1} : ... : x{n} : S - -- ``DUG n``: Place the element on top of the stack at depth ``n``. The - element on top of the stack is at depth ``0`` so that ``DUG 0`` is a - no-op and ``DUG 1`` is equivalent to ``SWAP``. - -:: - - :: 'b : 'a{1} : ... : 'a{n} : 'A -> 'a{1} : ... : 'a{n} : 'b : 'A - - > DUG n / y : x{1} : ... : x{n} : S => x{1} : ... : x{n} : y : S - -- ``PUSH 'a x``: Push a constant value of a given type onto the stack. - -:: - - :: 'A -> 'a : 'A - iff x :: 'a - - > PUSH 'a x / S => x : S - -- ``LAMBDA 'a 'b code``: Push a lambda with the given parameter type `'a` and return - type `'b` onto the stack. - -:: - - :: 'A -> (lambda 'a 'b) : 'A - - > LAMBDA _ _ code / S => code : S - -Generic comparison -~~~~~~~~~~~~~~~~~~ - -Comparison only works on a class of types that we call comparable. A -``COMPARE`` operation is defined in an ad hoc way for each comparable -type, but the result of compare is always an ``int``, which can in turn -be checked in a generic manner using the following combinators. The -result of ``COMPARE`` is ``0`` if the top two elements of the stack are -equal, negative if the first element in the stack is less than the -second, and positive otherwise. - -- ``EQ``: Checks that the top element of the stack is equal to zero. - -:: - - :: int : 'S -> bool : 'S - - > EQ / 0 : S => True : S - > EQ / v : S => False : S - iff v <> 0 - -- ``NEQ``: Checks that the top element of the stack is not equal to zero. - -:: - - :: int : 'S -> bool : 'S - - > NEQ / 0 : S => False : S - > NEQ / v : S => True : S - iff v <> 0 - -- ``LT``: Checks that the top element of the stack is less than zero. - -:: - - :: int : 'S -> bool : 'S - - > LT / v : S => True : S - iff v < 0 - > LT / v : S => False : S - iff v >= 0 - -- ``GT``: Checks that the top element of the stack is greater than zero. - -:: - - :: int : 'S -> bool : 'S - - > GT / v : S => C / True : S - iff v > 0 - > GT / v : S => C / False : S - iff v <= 0 - -- ``LE``: Checks that the top element of the stack is less than or equal to - zero. - -:: - - :: int : 'S -> bool : 'S - - > LE / v : S => True : S - iff v <= 0 - > LE / v : S => False : S - iff v > 0 - -- ``GE``: Checks that the top of the stack is greater than or equal to - zero. - -:: - - :: int : 'S -> bool : 'S - - > GE / v : S => True : S - iff v >= 0 - > GE / v : S => False : S - iff v < 0 - -Operations ----------- - -Operations on unit -~~~~~~~~~~~~~~~~~~ - -- ``UNIT``: Push a unit value onto the stack. - -:: - - :: 'A -> unit : 'A - - > UNIT / S => Unit : S - -- ``COMPARE``: Unit comparison - -:: - - :: unit : unit : 'S -> int : 'S - - > COMPARE / Unit : Unit : S => 0 : S - -Operations on type never -~~~~~~~~~~~~~~~~~~~~~~~~ - -The type ``never`` is the type of forbidden values. The most prominent -scenario in which ``never`` is used is when implementing a contract -template with no additional entrypoint. A contract template defines a set -of basic entrypoints, and its ``parameter`` declaration contains a type -variable for additional entrypoints in some branch of an union type, or -wrapped inside an option type. Letting this type variable be ``never`` in -a particular implementation indicates that the contract template has not -been extended, and turns the branch in the code that processes the -additional entrypoints into a forbidden branch. - -Values of type ``never`` cannot occur in a well-typed program. However, -they can be abstracted in the ``parameter`` declaration of a contract---or -by using the ``LAMBDA`` operation---thus indicating that the corresponding -branches in the code are forbidden. The type ``never`` also plays a role -when introducing values of union or option type with ``LEFT never``, -``RIGHT never``, or ``NONE never``. In such cases, the created values can -be inspected with the operations ``IF_LEFT``, ``IF_RIGHT``, or -``IF_NONE``, and the corresponding branches in the code are forbidden -branches. - -- ``NEVER``: Close a forbidden branch. - -:: - :: never : 'A -> 'B - -- ``COMPARE``: Trivial comparison on type ``never`` - -:: - - :: never : never : 'S -> int : 'S - - -Operations on booleans -~~~~~~~~~~~~~~~~~~~~~~ - -- ``OR`` - -:: - - :: bool : bool : 'S -> bool : 'S - - > OR / x : y : S => (x | y) : S - -- ``AND`` - -:: - - :: bool : bool : 'S -> bool : 'S - - > AND / x : y : S => (x & y) : S - -- ``XOR`` - -:: - - :: bool : bool : 'S -> bool : 'S - - > XOR / x : y : S => (x ^ y) : S - -- ``NOT`` - -:: - - :: bool : 'S -> bool : 'S - - > NOT / x : S => ~x : S - -- ``COMPARE``: Boolean comparison - -:: - - :: bool : bool : 'S -> int : 'S - - > COMPARE / False : False : S => 0 : S - > COMPARE / False : True : S => -1 : S - > COMPARE / True : False : S => 1 : S - > COMPARE / True : True : S => 0 : S - -Operations on integers and natural numbers -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -Integers and naturals are arbitrary-precision, meaning that the only size -limit is gas. - -- ``NEG`` - -:: - - :: int : 'S -> int : 'S - :: nat : 'S -> int : 'S - - > NEG / x : S => -x : S - -- ``ABS`` - -:: - - :: int : 'S -> nat : 'S - - > ABS / x : S => abs (x) : S - -- ``ISNAT`` - -:: - - :: int : 'S -> option nat : 'S - - > ISNAT / x : S => Some (x) : S - iff x >= 0 - - > ISNAT / x : S => None : S - iff x < 0 - -- ``INT`` - -:: - - :: nat : 'S -> int : 'S - - > INT / x : S => x : S - -- ``ADD`` - -:: - - :: int : int : 'S -> int : 'S - :: int : nat : 'S -> int : 'S - :: nat : int : 'S -> int : 'S - :: nat : nat : 'S -> nat : 'S - - > ADD / x : y : S => (x + y) : S - -- ``SUB`` - -:: - - :: int : int : 'S -> int : 'S - :: int : nat : 'S -> int : 'S - :: nat : int : 'S -> int : 'S - :: nat : nat : 'S -> int : 'S - - > SUB / x : y : S => (x - y) : S - -- ``MUL`` - -:: - - :: int : int : 'S -> int : 'S - :: int : nat : 'S -> int : 'S - :: nat : int : 'S -> int : 'S - :: nat : nat : 'S -> nat : 'S - - > MUL / x : y : S => (x * y) : S - -- ``EDIV``: Perform Euclidean division - -:: - - :: int : int : 'S -> option (pair int nat) : 'S - :: int : nat : 'S -> option (pair int nat) : 'S - :: nat : int : 'S -> option (pair int nat) : 'S - :: nat : nat : 'S -> option (pair nat nat) : 'S - - > EDIV / x : 0 : S => None : S - > EDIV / x : y : S => Some (Pair (x / y) (x % y)) : S - iff y <> 0 - -Bitwise logical operators are also available on unsigned integers. - -- ``OR`` - -:: - - :: nat : nat : 'S -> nat : 'S - - > OR / x : y : S => (x | y) : S - -- ``AND``: (also available when the top operand is signed) - -:: - - :: nat : nat : 'S -> nat : 'S - :: int : nat : 'S -> nat : 'S - - > AND / x : y : S => (x & y) : S - -- ``XOR`` - -:: - - :: nat : nat : 'S -> nat : 'S - - > XOR / x : y : S => (x ^ y) : S - -- ``NOT``: Two's complement - -:: - - :: nat : 'S -> int : 'S - :: int : 'S -> int : 'S - - > NOT / x : S => ~x : S - - -The return type of ``NOT`` is an ``int`` and not a ``nat``. This is -because the sign is also negated. The resulting integer is computed -using two's complement. For instance, the boolean negation of ``0`` is -``-1``. To get a natural back, a possibility is to use ``AND`` with an -unsigned mask afterwards. - - -- ``LSL`` - -:: - - :: nat : nat : 'S -> nat : 'S - - > LSL / x : s : S => (x << s) : S - iff s <= 256 - > LSL / x : s : S => [FAILED] - iff s > 256 - -- ``LSR`` - -:: - - :: nat : nat : 'S -> nat : 'S - - > LSR / x : s : S => (x >> s) : S - iff s <= 256 - > LSR / x : s : S => [FAILED] - iff s > 256 - -- ``COMPARE``: Integer/natural comparison - -:: - - :: int : int : 'S -> int : 'S - :: nat : nat : 'S -> int : 'S - - > COMPARE / x : y : S => -1 : S - iff x < y - > COMPARE / x : y : S => 0 : S - iff x = y - > COMPARE / x : y : S => 1 : S - iff x > y - -Operations on strings -~~~~~~~~~~~~~~~~~~~~~ - -Strings are mostly used for naming things without having to rely on -external ID databases. They are restricted to the printable subset of -7-bit ASCII, plus some escaped characters (see section on -constants). So what can be done is basically use string constants as -is, concatenate or splice them, and use them as keys. - - -- ``CONCAT``: String concatenation. - -:: - - :: string : string : 'S -> string : 'S - - > CONCAT / s : t : S => (s ^ t) : S - - :: string list : 'S -> string : 'S - - > CONCAT / {} : S => "" : S - > CONCAT / { s ; } : S => (s ^ r) : S - where CONCAT / { } : S => r : S - -- ``SIZE``: number of characters in a string. - -:: - - :: string : 'S -> nat : 'S - -- ``SLICE``: String access. - -:: - - :: nat : nat : string : 'S -> option string : 'S - - > SLICE / offset : length : s : S => Some ss : S - where ss is the substring of s at the given offset and of the given length - iff offset and (offset + length) are in bounds - > SLICE / offset : length : s : S => None : S - iff offset or (offset + length) are out of bounds - -- ``COMPARE``: Lexicographic comparison. - -:: - - :: string : string : 'S -> int : 'S - - > COMPARE / s : t : S => -1 : S - iff s < t - > COMPARE / s : t : S => 0 : S - iff s = t - > COMPARE / s : t : S => 1 : S - iff s > t - -Operations on pairs and right combs -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -The type ``pair l r`` is the type of binary pairs composed of a left -element of type ``l`` and a right element of type ``r``. A value of -type ``pair l r`` is written ``Pair x y`` where ``x`` is a value of -type ``l`` and ``y`` is a value of type ``r``. - -To build tuples of length greater than 2, right combs have specific -optimized operations. For any ``n > 2``, the compact notations ``pair -t{0} t{1} ... t{n-2} t{n-1}`` is provided for the type of right combs -``pair t{0} (pair t{1} ... (pair t{n-2} t{n-1}) ...)``. Similarly, the -compact notation ``Pair x{0} x{1} ... x{n-2} x{n-1}`` is provided for -the right-comb value ``Pair x{0} (Pair x{1} ... (Pair x{n-2} x{n-1}) -...)``. Right-comb values can also be written using sequences; ``Pair -x{0} x{1} ... x{n-2} x{n-1}`` can be written ``{x{0}; x{1}; ...; x{n-2}; x{n-1}}``. - -- ``PAIR``: Build a binary pair from the stack's top two elements. - -:: - - :: 'a : 'b : 'S -> pair 'a 'b : 'S - - > PAIR / x : y : S => Pair x y : S - -- ``PAIR n``: Fold ``n`` values on the top of the stack in a right comb. - ``PAIR 0`` and ``PAIR 1`` are rejected. ``PAIR 2`` is equivalent to ``PAIR``. - -:: - - PAIR 2 :: 'a : 'b : 'S -> pair 'a 'b : 'S - PAIR (k+1) :: 'x : 'S -> pair 'x 'y : 'T - iff PAIR k :: 'S -> 'y : 'T - - Or equivalently, for n >= 2, - PAIR n :: 'a{0} : ... : 'a{n-1} : 'A -> pair 'a{0} ... 'a{n-1} : 'A - - > PAIR 2 / x : y : S => Pair x y : S - > PAIR (k+1) / x : S => Pair x y : T - iff PAIR k / S => y : T - - Or equivalently, for n >= 2, - > PAIR n / x{0} : ... : x{n-1} : S => Pair x{0} ... x{n-1} : S - -- ``UNPAIR``: Split a pair into its components. - -:: - - :: pair 'a 'b : 'S -> 'a : 'b : 'S - - > UNPAIR / Pair a b : S => a : b : S - - -- ``UNPAIR n``: Unfold ``n`` values from a right comb on the top of the stack. ``UNPAIR 0`` and ``UNPAIR 1`` are rejected. ``UNPAIR 2`` is equivalent to ``UNPAIR``. - -:: - - UNPAIR 2 :: pair 'a 'b : 'A -> 'a : 'b : 'A - UNPAIR (k+1) :: pair 'a 'b : 'A -> 'a : 'B - iff UNPAIR k :: 'b : 'A -> 'B - - Or equivalently, for n >= 2, - UNPAIR n :: pair 'a{0} ... 'a{n-1} : S -> 'a{0} : ... : 'a{n-1} : S - - > UNPAIR 2 / Pair x y : S => x : y : S - > UNPAIR (k+1) / Pair x y : SA => x : SB - iff UNPAIR k / y : SA => SB - - Or equivalently, for n >= 2, - > UNPAIR n / Pair x{0} ... x{n-1} : S => x{0} : ... : x{n-1} : S - -- ``CAR``: Access the left part of a pair. - -:: - - :: pair 'a _ : 'S -> 'a : 'S - - > CAR / Pair x _ : S => x : S - -- ``CDR``: Access the right part of a pair. - -:: - - :: pair _ 'b : 'S -> 'b : 'S - - > CDR / Pair _ y : S => y : S - -- ``GET k``: Access an element or a sub comb in a right comb. - - The nodes of a right comb of size ``n`` are canonically numbered as follows: - -:: - - 0 - / \ - 1 2 - / \ - 3 4 - / \ - 5 ... - 2n-2 - / \ - 2n-1 2n - - -Or in plain English: - - - The root is numbered with 0, - - The left child of the node numbered by ``k`` is numbered by ``k+1``, and - - The right child of the node numbered by ``k`` is numbered by ``k+2``. - -The ``GET k`` instruction accesses the node numbered by ``k``. In -particular, for a comb of size ``n``, the ``n-1`` first elements are -accessed by ``GET 1``, ``GET 3``, ..., and ``GET (2n-1)`` and the last -element is accessed by ``GET (2n)``. - -:: - - GET 0 :: 'a : 'S -> 'a : 'S - GET 1 :: pair 'x _ : 'S -> 'x : 'S - GET (k+2) :: pair _ 'y : 'S -> 'z : 'S - iff GET k :: 'y : 'S -> 'z : 'S - - Or equivalently, - GET 0 :: 'a : 'S -> 'a : 'S - GET (2k) :: pair 'a{0} ... 'a{k-1} 'a{k} : 'S -> 'a{k} : 'S - GET (2k+1) :: pair 'a{0} ... 'a{k} 'a{k+1} : 'S -> 'a{k} : 'S - - > GET 0 / x : S => x : S - > GET 1 / Pair x _ : S => x : S - > GET (k+2) / Pair _ y : S => GET k / y : S - - Or equivalently, - > GET 0 / x : S => x : S - > GET (2k) / Pair x{0} ... x{k-1} x{k} : 'S -> x{k} : 'S - > GET (2k+1) / Pair x{0} ... x{k} x{k+1} : 'S -> x{k} : 'S - - -- ``UPDATE k``: Update an element or a sub comb in a right comb. The topmost stack element is the new value to insert in the comb, the second stack element is the right comb to update. The meaning of ``k`` is the same as for the ``GET k`` instruction. - -:: - - UPDATE 0 :: 'a : 'b : 'S -> 'a : 'S - UPDATE 1 :: 'a2 : pair 'a1 'b : 'S -> pair 'a2 'b : 'S - UPDATE (k+2) :: 'c : pair 'a 'b1 : 'S -> pair 'a 'b2 : 'S - iff UPDATE k :: 'c : 'b1 : 'S -> 'b2 : 'S - - Or equivalently, - UPDATE 0 :: 'a : 'b : 'S -> 'a : 'S - UPDATE (2k) :: 'c : pair 'a{0} ... 'a{k-1} 'a{k} : 'S -> pair 'a{0} ... 'a{k-1} 'c : 'S - UPDATE (2k+1) :: 'c : pair 'a{0} ... 'a{k} 'a{k+1} : 'S -> pair 'a{0} ... 'a{k-1} 'c 'a{k+1} : 'S - - > UPDATE 0 / x : _ : S => x : S - > UPDATE 1 / x2 : Pair x1 y : S => Pair x2 y : S - > UPDATE (k+2) / z : Pair x y1 : S => Pair x y2 : S - iff UPDATE k / z : y1 : S => y2 : S - - Or equivalently, - > UPDATE 0 / x : _ : S => x : S - > UPDATE (2k) / z : Pair x{0} ... x{k-1} x{k} : 'S => Pair x{0} ... x{k-1} z : 'S - > UPDATE (2k+1) / z : Pair x{0} ... x{k-1} x{k} x{k+1} : 'S => Pair x{0} ... x{k-1} z x{k+1} : 'S - -- ``COMPARE``: Lexicographic comparison. - -:: - - :: pair 'a 'b : pair 'a 'b : 'S -> int : 'S - - > COMPARE / (Pair sa sb) : (Pair ta tb) : S => -1 : S - iff COMPARE / sa : ta : S => -1 : S - > COMPARE / (Pair sa sb) : (Pair ta tb) : S => 1 : S - iff COMPARE / sa : ta : S => 1 : S - > COMPARE / (Pair sa sb) : (Pair ta tb) : S => r : S - iff COMPARE / sa : ta : S => 0 : S - COMPARE / sb : tb : S => r : S - -Operations on sets -~~~~~~~~~~~~~~~~~~ - -- ``EMPTY_SET 'elt``: Build a new, empty set for elements of a given - type. - - The ``'elt`` type must be comparable (the ``COMPARE`` - primitive must be defined over it). - -:: - - :: 'S -> set 'elt : 'S - - > EMPTY_SET _ / S => {} : S - -- ``MEM``: Check for the presence of an element in a set. - -:: - - :: 'elt : set 'elt : 'S -> bool : 'S - - > MEM / x : {} : S => false : S - > MEM / x : { hd ; } : S => r : S - iff COMPARE / x : hd : [] => 1 : [] - where MEM / x : { } : S => r : S - > MEM / x : { hd ; } : S => true : S - iff COMPARE / x : hd : [] => 0 : [] - > MEM / x : { hd ; } : S => false : S - iff COMPARE / x : hd : [] => -1 : [] - -- ``UPDATE``: Inserts or removes an element in a set, replacing a - previous value. - -:: - - :: 'elt : bool : set 'elt : 'S -> set 'elt : 'S - - > UPDATE / x : false : {} : S => {} : S - > UPDATE / x : true : {} : S => { x } : S - > UPDATE / x : v : { hd ; } : S => { hd ; } : S - iff COMPARE / x : hd : [] => 1 : [] - where UPDATE / x : v : { } : S => { } : S - > UPDATE / x : false : { hd ; } : S => { } : S - iff COMPARE / x : hd : [] => 0 : [] - > UPDATE / x : true : { hd ; } : S => { hd ; } : S - iff COMPARE / x : hd : [] => 0 : [] - > UPDATE / x : false : { hd ; } : S => { hd ; } : S - iff COMPARE / x : hd : [] => -1 : [] - > UPDATE / x : true : { hd ; } : S => { x ; hd ; } : S - iff COMPARE / x : hd : [] => -1 : [] - -- ``ITER body``: Apply the body expression to each element of a set. - The body sequence has access to the stack. - -:: - - :: (set 'elt) : 'A -> 'A - iff body :: [ 'elt : 'A -> 'A ] - - > ITER body / {} : S => S - > ITER body / { hd ; } : S => ITER body / { } : S' - iff body / hd : S => S' - - -- ``SIZE``: Get the cardinality of the set. - -:: - - :: set 'elt : 'S -> nat : 'S - - > SIZE / {} : S => 0 : S - > SIZE / { _ ; } : S => 1 + s : S - where SIZE / { } : S => s : S - -Operations on maps -~~~~~~~~~~~~~~~~~~ - -- ``EMPTY_MAP 'key 'val``: Build a new, empty map from keys of a - given type to values of another given type. - - The ``'key`` type must be comparable (the ``COMPARE`` primitive must - be defined over it). - -:: - - :: 'S -> map 'key 'val : 'S - - > EMPTY_MAP _ _ / S => {} : S - - -- ``GET``: Access an element in a map, returns an optional value to be - checked with ``IF_SOME``. - -:: - - :: 'key : map 'key 'val : 'S -> option 'val : 'S - - > GET / x : {} : S => None : S - > GET / x : { Elt k v ; } : S => opt_y : S - iff COMPARE / x : k : [] => 1 : [] - where GET / x : { } : S => opt_y : S - > GET / x : { Elt k v ; } : S => Some v : S - iff COMPARE / x : k : [] => 0 : [] - > GET / x : { Elt k v ; } : S => None : S - iff COMPARE / x : k : [] => -1 : [] - -- ``MEM``: Check for the presence of a binding for a key in a map. - -:: - - :: 'key : map 'key 'val : 'S -> bool : 'S - - > MEM / x : {} : S => false : S - > MEM / x : { Elt k v ; } : S => r : S - iff COMPARE / x : k : [] => 1 : [] - where MEM / x : { } : S => r : S - > MEM / x : { Elt k v ; } : S => true : S - iff COMPARE / x : k : [] => 0 : [] - > MEM / x : { Elt k v ; } : S => false : S - iff COMPARE / x : k : [] => -1 : [] - -- ``UPDATE``: Assign or remove an element in a map. - -:: - - :: 'key : option 'val : map 'key 'val : 'S -> map 'key 'val : 'S - - > UPDATE / x : None : {} : S => {} : S - > UPDATE / x : Some y : {} : S => { Elt x y } : S - > UPDATE / x : opt_y : { Elt k v ; } : S => { Elt k v ; } : S - iff COMPARE / x : k : [] => 1 : [] - where UPDATE / x : opt_y : { } : S => { } : S - > UPDATE / x : None : { Elt k v ; } : S => { } : S - iff COMPARE / x : k : [] => 0 : [] - > UPDATE / x : Some y : { Elt k v ; } : S => { Elt k y ; } : S - iff COMPARE / x : k : [] => 0 : [] - > UPDATE / x : None : { Elt k v ; } : S => { Elt k v ; } : S - iff COMPARE / x : k : [] => -1 : [] - > UPDATE / x : Some y : { Elt k v ; } : S => { Elt x y ; Elt k v ; } : S - iff COMPARE / x : k : [] => -1 : [] - -- ``GET_AND_UPDATE``: A combination of the ``GET`` and ``UPDATE`` instructions. - -:: - - :: 'key : option 'val : map 'key 'val : 'S -> option 'val : map 'key 'val : 'S - -This instruction is similar to ``UPDATE`` but it also returns the -value that was previously stored in the ``map`` at the same key as -``GET`` would. - -:: - - > GET_AND_UPDATE / x : None : {} : S => None : {} : S - > GET_AND_UPDATE / x : Some y : {} : S => None : { Elt x y } : S - > GET_AND_UPDATE / x : opt_y : { Elt k v ; } : S => opt_y' : { Elt k v ; } : S - iff COMPARE / x : k : [] => 1 : [] - where GET_AND_UPDATE / x : opt_y : { } : S => opt_y' : { } : S - > GET_AND_UPDATE / x : None : { Elt k v ; } : S => Some v : { } : S - iff COMPARE / x : k : [] => 0 : [] - > GET_AND_UPDATE / x : Some y : { Elt k v ; } : S => Some v : { Elt k y ; } : S - iff COMPARE / x : k : [] => 0 : [] - > GET_AND_UPDATE / x : None : { Elt k v ; } : S => None : { Elt k v ; } : S - iff COMPARE / x : k : [] => -1 : [] - > GET_AND_UPDATE / x : Some y : { Elt k v ; } : S => None : { Elt x y ; Elt k v ; } : S - iff COMPARE / x : k : [] => -1 : [] - -- ``MAP body``: Apply the body expression to each element of a map. The - body sequence has access to the stack. - -:: - - :: (map 'key 'val) : 'A -> (map 'key 'b) : 'A - iff body :: [ (pair 'key 'val) : 'A -> 'b : 'A ] - - > MAP body / {} : S => {} : S - > MAP body / { Elt k v ; } : S => { Elt k v' ; } : S'' - where body / Pair k v : S => v' : S' - and MAP body / { } : S' => { } : S'' - -- ``ITER body``: Apply the body expression to each element of a map. - The body sequence has access to the stack. - -:: - - :: (map 'elt 'val) : 'A -> 'A - iff body :: [ (pair 'elt 'val : 'A) -> 'A ] - - > ITER body / {} : S => S - > ITER body / { Elt k v ; } : S => ITER body / { } : S' - iff body / (Pair k v) : S => S' - -- ``SIZE``: Get the cardinality of the map. - -:: - - :: map 'key 'val : 'S -> nat : 'S - - > SIZE / {} : S => 0 : S - > SIZE / { _ ; } : S => 1 + s : S - where SIZE / { } : S => s : S - - -Operations on ``big_maps`` -~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. _OperationsOnBigMaps_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 -by integers called big-map identifiers. Finally, big maps can be -represented as pairs of a big-map identifier (an integer) and a -big-map diff (written in the same syntax as a map whose values are -options). - -So for example, ``{ Elt "bar" True ; Elt "foo" False }``, ``42``, and -``Pair 42 { Elt "foo" (Some False) }`` are all valid representations -of type ``big_map string bool``. - -The behavior of big-map operations is the same as if they were normal -maps, except that under the hood, the elements are loaded and -deserialized on demand. - -- ``EMPTY_BIG_MAP 'key 'val``: Build a new, empty big map from keys of a - given type to values of another given type. - - The ``'key`` type must be comparable (the ``COMPARE`` primitive must - be defined over it). - -:: - - :: 'S -> map 'key 'val : 'S - -- ``GET``: Access an element in a ``big_map``, returns an optional value to be - checked with ``IF_SOME``. - -:: - - :: 'key : big_map 'key 'val : 'S -> option 'val : 'S - -- ``MEM``: Check for the presence of an element in a ``big_map``. - -:: - - :: 'key : big_map 'key 'val : 'S -> bool : 'S - -- ``UPDATE``: Assign or remove an element in a ``big_map``. - -:: - - :: 'key : option 'val : big_map 'key 'val : 'S -> big_map 'key 'val : 'S - - -- ``GET_AND_UPDATE``: A combination of the ``GET`` and ``UPDATE`` instructions. - -:: - - :: 'key : option 'val : big_map 'key 'val : 'S -> option 'val : big_map 'key 'val : 'S - -This instruction is similar to ``UPDATE`` but it also returns the -value that was previously stored in the ``big_map`` at the same key as -``GET`` would. - - -Operations on optional values -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -- ``SOME``: Pack a value as an optional value. - -:: - - :: 'a : 'S -> option 'a : 'S - - > SOME / v : S => (Some v) : S - -- ``NONE 'a``: The absent optional value. - -:: - - :: 'S -> option 'a : 'S - - > NONE / S => None : S - -- ``IF_NONE bt bf``: Inspect an optional value. - -:: - - :: option 'a : 'A -> 'B - iff bt :: [ 'A -> 'B] - bf :: [ 'a : 'A -> 'B] - - > IF_NONE bt bf / (None) : S => bt / S - > IF_NONE bt bf / (Some a) : S => bf / a : S - -- ``COMPARE``: Optional values comparison - -:: - - :: option 'a : option 'a : 'S -> int : 'S - - > COMPARE / None : None : S => 0 : S - > COMPARE / None : (Some _) : S => -1 : S - > COMPARE / (Some _) : None : S => 1 : S - > COMPARE / (Some a) : (Some b) : S => COMPARE / a : b : S - -Operations on unions -~~~~~~~~~~~~~~~~~~~~ - -- ``LEFT 'b``: Pack a value in a union (left case). - -:: - - :: 'a : 'S -> or 'a 'b : 'S - - > LEFT / v : S => (Left v) : S - -- ``RIGHT 'a``: Pack a value in a union (right case). - -:: - - :: 'b : 'S -> or 'a 'b : 'S - - > RIGHT / v : S => (Right v) : S - -- ``IF_LEFT bt bf``: Inspect a value of a union. - -:: - - :: or 'a 'b : 'A -> 'B - iff bt :: [ 'a : 'A -> 'B] - bf :: [ 'b : 'A -> 'B] - - > IF_LEFT bt bf / (Left a) : S => bt / a : S - > IF_LEFT bt bf / (Right b) : S => bf / b : S - -- ``COMPARE``: Unions comparison - -:: - - :: or 'a 'b : or 'a 'b : 'S -> int : 'S - - > COMPARE / (Left a) : (Left b) : S => COMPARE / a : b : S - > COMPARE / (Left _) : (Right _) : S => -1 : S - > COMPARE / (Right _) : (Left _) : S => 1 : S - > COMPARE / (Right a) : (Right b) : S => COMPARE / a : b : S - -Operations on lists -~~~~~~~~~~~~~~~~~~~ - -- ``CONS``: Prepend an element to a list. - -:: - - :: 'a : list 'a : 'S -> list 'a : 'S - - > CONS / a : { } : S => { a ; } : S - -- ``NIL 'a``: The empty list. - -:: - - :: 'S -> list 'a : 'S - - > NIL / S => {} : S - -- ``IF_CONS bt bf``: Inspect a list. - -:: - - :: list 'a : 'A -> 'B - iff bt :: [ 'a : list 'a : 'A -> 'B] - bf :: [ 'A -> 'B] - - > IF_CONS bt bf / { a ; } : S => bt / a : { } : S - > IF_CONS bt bf / {} : S => bf / S - -- ``MAP body``: Apply the body expression to each element of the list. - The body sequence has access to the stack. - -:: - - :: (list 'elt) : 'A -> (list 'b) : 'A - iff body :: [ 'elt : 'A -> 'b : 'A ] - - > MAP body / {} : S => {} : S - > MAP body / { a ; } : S => { b ; } : S'' - where body / a : S => b : S' - and MAP body / { } : S' => { } : S'' - -- ``SIZE``: Get the number of elements in the list. - -:: - - :: list 'elt : 'S -> nat : 'S - - > SIZE / { _ ; } : S => 1 + s : S - where SIZE / { } : S => s : S - > SIZE / {} : S => 0 : S - - -- ``ITER body``: Apply the body expression to each element of a list. - The body sequence has access to the stack. - -:: - - :: (list 'elt) : 'A -> 'A - iff body :: [ 'elt : 'A -> 'A ] - > ITER body / {} : S => S - > ITER body / { a ; } : S => ITER body / { } : S' - iff body / a : S => S' - - -Domain specific data types --------------------------- - -- ``timestamp``: Dates in the real world. - -- ``mutez``: A specific type for manipulating tokens. - -- ``address``: An untyped address (implicit account or smart contract). - -- ``contract 'param``: A contract, with the type of its code, - ``contract unit`` for implicit accounts. - -- ``operation``: An internal operation emitted by a contract. - -- ``key``: A public cryptographic key. - -- ``key_hash``: The hash of a public cryptographic key. - -- ``signature``: A cryptographic signature. - -- ``chain_id``: An identifier for a chain, used to distinguish the test and the main chains. - -- ``bls12_381_g1``, ``bls12_381_g2`` : Points on the BLS12-381 curves G\ :sub:`1`\ and G\ :sub:`2`\ , respectively. - -- ``bls12_381_fr`` : An element of the scalar field F\ :sub:`r`\ , used for scalar multiplication on the BLS12-381 curves G\ :sub:`1`\ and G\ :sub:`2`\ . - -- ``sapling_transaction ms``: A :ref:`Sapling` transaction - -- ``sapling_state ms``: A :ref:`Sapling` state - -- ``ticket (t)``: A ticket used to authenticate information of type ``(t)`` on-chain. - -Domain specific operations --------------------------- - -Operations on timestamps -~~~~~~~~~~~~~~~~~~~~~~~~ - -Timestamps can be obtained by the ``NOW`` operation, or retrieved from -script parameters or globals. - -- ``ADD`` Increment / decrement a timestamp of the given number of - seconds. - -:: - - :: timestamp : int : 'S -> timestamp : 'S - :: int : timestamp : 'S -> timestamp : 'S - - > ADD / seconds : nat (t) : S => (seconds + t) : S - > ADD / nat (t) : seconds : S => (t + seconds) : S - -- ``SUB`` Subtract a number of seconds from a timestamp. - -:: - - :: timestamp : int : 'S -> timestamp : 'S - - > SUB / seconds : nat (t) : S => (seconds - t) : S - -- ``SUB`` Subtract two timestamps. - -:: - - :: timestamp : timestamp : 'S -> int : 'S - - > SUB / seconds(t1) : seconds(t2) : S => (t1 - t2) : S - -- ``COMPARE``: Timestamp comparison. - -:: - - :: timestamp : timestamp : 'S -> int : 'S - - > COMPARE / seconds(t1) : seconds(t2) : S => -1 : S - iff t1 < t2 - > COMPARE / seconds(t1) : seconds(t2) : S => 0 : S - iff t1 = t2 - > COMPARE / seconds(t1) : seconds(t2) : S => 1 : S - iff t1 > t2 - - -Operations on Mutez -~~~~~~~~~~~~~~~~~~~ - -Mutez (micro-Tez) are internally represented by a 64 bit signed -integers. There are restrictions to prevent creating a negative amount -of mutez. Operations are limited to prevent overflow and mixing them -with other numerical types by mistake. They are also mandatory checked -for under/overflows. - -- ``ADD`` - -:: - - :: mutez : mutez : 'S -> mutez : 'S - - > ADD / x : y : S => [FAILED] on overflow - > ADD / x : y : S => (x + y) : S - -- ``SUB`` - -:: - - :: mutez : mutez : 'S -> mutez : 'S - - > SUB / x : y : S => [FAILED] - iff x < y - > SUB / x : y : S => (x - y) : S - -- ``MUL`` - -:: - - :: mutez : nat : 'S -> mutez : 'S - :: nat : mutez : 'S -> mutez : 'S - - > MUL / x : y : S => [FAILED] on overflow - > MUL / x : y : S => (x * y) : S - -- ``EDIV`` - -:: - - :: mutez : nat : 'S -> option (pair mutez mutez) : 'S - :: mutez : mutez : 'S -> option (pair nat mutez) : 'S - - > EDIV / x : 0 : S => None - > EDIV / x : y : S => Some (Pair (x / y) (x % y)) : S - iff y <> 0 - -- ``COMPARE``: Mutez comparison - -:: - - :: mutez : mutez : 'S -> int : 'S - - > COMPARE / x : y : S => -1 : S - iff x < y - > COMPARE / x : y : S => 0 : S - iff x = y - > COMPARE / x : y : S => 1 : S - iff x > y - -Operations on contracts -~~~~~~~~~~~~~~~~~~~~~~~ - -- ``CREATE_CONTRACT { storage 'g ; parameter 'p ; code ... }``: - Forge a new contract from a literal. - -:: - - :: option key_hash : mutez : 'g : 'S - -> operation : address : 'S - -Originate a contract based on a literal. The parameters are the -optional delegate, the initial amount taken from the current -contract, and the initial storage of the originated contract. -The contract is returned as a first class value (to be dropped, passed -as parameter or stored). The ``CONTRACT 'p`` instruction will fail -until it is actually originated. - -- ``TRANSFER_TOKENS``: Forge a transaction. - -:: - - :: 'p : mutez : contract 'p : 'S -> operation : 'S - -The parameter must be consistent with the one expected by the -contract, unit for an account. - -.. _MichelsonSetDelegate_009_BA: - -- ``SET_DELEGATE``: Set or withdraw the contract's delegation. - -:: - - :: option key_hash : 'S -> operation : 'S - -Using this instruction is the only way to modify the delegation of a -smart contract. If the parameter is `None` then the delegation of the -current contract is withdrawn; if it is `Some kh` where `kh` is the -key hash of a registered delegate that is not the current delegate of -the contract, then this operation sets the delegate of the contract to -this registered delegate. The operation fails if `kh` is the current -delegate of the contract or if `kh` is not a registered delegate. - -- ``BALANCE``: Push the current amount of mutez held by the executing - contract, including any mutez added by the calling transaction. - -:: - - :: 'S -> mutez : 'S - -- ``ADDRESS``: Cast the contract to its address. - -:: - - :: contract _ : 'S -> address : 'S - - > ADDRESS / addr : S => addr : S - -- ``CONTRACT 'p``: Cast the address to the given contract type if possible. - -:: - - :: address : 'S -> option (contract 'p) : 'S - - > CONTRACT / addr : S => Some addr : S - iff addr exists and is a contract of parameter type 'p - > CONTRACT / addr : S => Some addr : S - iff 'p = unit and addr is an implicit contract - > CONTRACT / addr : S => None : S - otherwise - -- ``SOURCE``: Push the contract that initiated the current - transaction, i.e. the contract that paid the fees and - storage cost, and whose manager signed the operation - that was sent on the blockchain. Note that since - ``TRANSFER_TOKENS`` instructions can be chained, - ``SOURCE`` and ``SENDER`` are not necessarily the same. - -:: - - :: 'S -> address : 'S - -- ``SENDER``: Push the contract that initiated the current - internal transaction. It may be the ``SOURCE``, but may - also be different if the source sent an order to an intermediate - smart contract, which then called the current contract. - -:: - - :: 'S -> address : 'S - -- ``SELF``: Push the current contract. - -:: - - :: 'S -> contract 'p : 'S - where contract 'p is the type of the current contract - -Note that ``SELF`` is forbidden in lambdas because it cannot be -type-checked; the type of the contract executing the lambda cannot be -known at the point of type-checking the lambda's body. - -- ``SELF_ADDRESS``: Push the address of the current contract. This is - equivalent to ``SELF; ADDRESS`` except that it is allowed in - lambdas. - -:: - - :: 'S -> address : 'S - -Note that ``SELF_ADDRESS`` inside a lambda returns the address of the -contract executing the lambda, which can be different from the address -of the contract in which the ``SELF_ADDRESS`` instruction is written. - -- ``AMOUNT``: Push the amount of the current transaction. - -:: - - :: 'S -> mutez : 'S - -- ``IMPLICIT_ACCOUNT``: Return a default contract with the given - public/private key pair. Any funds deposited in this contract can - immediately be spent by the holder of the private key. This contract - cannot execute Michelson code and will always exist on the - blockchain. - -:: - - :: key_hash : 'S -> contract unit : 'S - -- ``VOTING_POWER``: Return the voting power of a given contract. This voting power - coincides with the weight of the contract in the voting listings (i.e., the rolls - count) which is calculated at the beginning of every voting period. - -:: - - :: key_hash : 'S -> nat : 'S - -Special operations -~~~~~~~~~~~~~~~~~~ - -- ``NOW``: Push the 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 - -- ``COMPARE``: Chain identifier comparison - -:: - - :: chain_id : chain_id : 'S -> int : 'S - - > COMPARE / x : y : S => -1 : S - iff x < y - > COMPARE / x : y : S => 0 : S - iff x = y - > COMPARE / x : y : S => 1 : S - iff x > y - -- ``LEVEL``: Push the current block level. - -:: - - :: 'S -> nat : 'S - -- ``TOTAL_VOTING_POWER``: Return the total voting power of all contracts. The total - voting power coincides with the sum of the rolls count of every contract in the voting - listings. The voting listings is calculated at the beginning of every voting period. - -:: - - :: 'S -> nat : 'S - -Operations on bytes -~~~~~~~~~~~~~~~~~~~ - -Bytes are used for serializing data, in order to check signatures and -compute hashes on them. They can also be used to incorporate data from -the wild and untyped outside world. - -- ``PACK``: Serializes a piece of data to its optimized - binary representation. - -:: - - :: 'a : 'S -> bytes : 'S - -- ``UNPACK 'a``: Deserializes a piece of data, if valid. - -:: - - :: bytes : 'S -> option 'a : 'S - -- ``CONCAT``: Byte sequence concatenation. - -:: - - :: bytes : bytes : 'S -> bytes : 'S - - > CONCAT / s : t : S => (s ^ t) : S - - :: bytes list : 'S -> bytes : 'S - - > CONCAT / {} : S => 0x : S - > CONCAT / { s ; } : S => (s ^ r) : S - where CONCAT / { } : S => r : S - -- ``SIZE``: size of a sequence of bytes. - -:: - - :: bytes : 'S -> nat : 'S - -- ``SLICE``: Bytes access. - -:: - - :: nat : nat : bytes : 'S -> option bytes : 'S - - > SLICE / offset : length : s : S => Some ss : S - where ss is the substring of s at the given offset and of the given length - iff offset and (offset + length) are in bounds - > SLICE / offset : length : s : S => None : S - iff offset or (offset + length) are out of bounds - -- ``COMPARE``: Lexicographic comparison. - -:: - - :: bytes : bytes : 'S -> int : 'S - - > COMPARE / s : t : S => -1 : S - iff s < t - > COMPARE / s : t : S => 0 : S - iff s = t - > COMPARE / s : t : S => 1 : S - iff s > t - - -Cryptographic primitives -~~~~~~~~~~~~~~~~~~~~~~~~ - -- ``HASH_KEY``: Compute the b58check of a public key. - -:: - - :: key : 'S -> key_hash : 'S - -- ``BLAKE2B``: Compute a cryptographic hash of the value contents using the - Blake2b-256 cryptographic hash function. - -:: - - :: bytes : 'S -> bytes : 'S - -- ``KECCAK``: Compute a cryptographic hash of the value contents using the - Keccak-256 cryptographic hash function. - -:: - - :: bytes : 'S -> bytes : 'S - -- ``SHA256``: Compute a cryptographic hash of the value contents using the - Sha256 cryptographic hash function. - -:: - - :: bytes : 'S -> bytes : 'S - -- ``SHA512``: Compute a cryptographic hash of the value contents using the - Sha512 cryptographic hash function. - -:: - - :: bytes : 'S -> bytes : 'S - -- ``SHA3``: Compute a cryptographic hash of the value contents using the - SHA3-256 cryptographic hash function. - -:: - - :: bytes : 'S -> bytes : 'S - -- ``CHECK_SIGNATURE``: Check that a sequence of bytes has been signed - with a given key. - -:: - - :: key : signature : bytes : 'S -> bool : 'S - -- ``COMPARE``: Key hash, key and signature comparison - -:: - - :: key_hash : key_hash : 'S -> int : 'S - :: key : key : 'S -> int : 'S - :: signature : signature : 'S -> int : 'S - - > COMPARE / x : y : S => -1 : S - iff x < y - > COMPARE / x : y : S => 0 : S - iff x = y - > COMPARE / x : y : S => 1 : S - iff x > y - -BLS12-381 primitives -~~~~~~~~~~~~~~~~~~~~~~~~ - -- ``NEG``: Negate a curve point or field element. - -:: - - :: bls12_381_g1 : 'S -> bls12_381_g1 : 'S - :: bls12_381_g2 : 'S -> bls12_381_g2 : 'S - :: bls12_381_fr : 'S -> bls12_381_fr : 'S - -- ``ADD``: Add two curve points or field elements. - -:: - - :: bls12_381_g1 : bls12_381_g1 : 'S -> bls12_381_g1 : 'S - :: bls12_381_g2 : bls12_381_g2 : 'S -> bls12_381_g2 : 'S - :: bls12_381_fr : bls12_381_fr : 'S -> bls12_381_fr : 'S - -- ``MUL``: Multiply a curve point or field element by a scalar field element. Fr - elements can be built from naturals by multiplying by the unit of Fr using ``PUSH bls12_381_fr 1; MUL``. Note - that the multiplication will be computed using the natural modulo the order - of Fr. - -:: - - :: bls12_381_g1 : bls12_381_fr : 'S -> bls12_381_g1 : 'S - :: bls12_381_g2 : bls12_381_fr : 'S -> bls12_381_g2 : 'S - :: bls12_381_fr : bls12_381_fr : 'S -> bls12_381_fr : 'S - :: nat : bls12_381_fr : 'S -> bls12_381_fr : 'S - :: int : bls12_381_fr : 'S -> bls12_381_fr : 'S - :: bls12_381_fr : nat : 'S -> bls12_381_fr : 'S - :: bls12_381_fr : int : 'S -> bls12_381_fr : 'S - -- ``INT``: Convert a field element to type ``int``. The returned value is always between ``0`` (inclusive) and the order of Fr (exclusive). - -:: - - :: bls12_381_fr : 'S -> int : 'S - -- ``PAIRING_CHECK``: - Verify that the product of pairings of the given list of points is equal to 1 in Fq12. Returns ``true`` if the list is empty. - Can be used to verify if two pairings P1 and P2 are equal by verifying P1 * P2^(-1) = 1. - -:: - - :: list (pair bls12_381_g1 bls12_381_g2) : 'S -> bool : 'S - - -Sapling operations -~~~~~~~~~~~~~~~~~~ - -Please see the :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. - -:: - - :: sapling_transaction ms : sapling_state ms : 'S -> option (pair int (sapling_state ms)): 'S - - > SAPLING_VERIFY_UPDATE / t : s : S => Some (Pair b s') : S - iff the transaction t successfully applied on state s resulting - in balance b and an updated state s' - > SAPLING_VERIFY_UPDATE / t : s : S => None : S - iff the transaction t is invalid with respect to the state - -- ``SAPLING_EMPTY_STATE ms``: Pushes an empty state on the stack. - - :: - - :: 'S -> sapling_state ms: 'S - - > SAPLING_EMPTY_STATE ms / S => sapling_state ms : S - with `sapling_state ms` being the empty state (ie. no one can spend tokens from it) - with memo_size `ms` - - -.. _MichelsonTickets_009_BA: - -Operations on tickets -~~~~~~~~~~~~~~~~~~~~~ - -The following operations deal with tickets. Tickets are a way for smart-contracts -to authenticate data with respect to a Tezos address. This authentication can -then be used to build composable permission systems. - -A contract can create a ticket from a value and an amount. The ticket, when -inspected reveals the value, the amount, and the address of the ticketer (the contract that created the ticket). It is -impossible for a contract to “forge” a ticket that appears to have been created -by another ticketer. - -The amount is a meta-data that can be used to implement UTXOs. - -Tickets cannot be duplicated using the ``DUP`` instruction. - -For example, a ticket could represent a Non Fungible Token (NFT) or a Unspent -Transaction Output (UTXO) which can then be passed around and behave like a value. -This process can happen without the need to interact with a centralized NFT contract, -simplifying the code. - -- ``TICKET``: Create a ticket with the given content and amount. The ticketer is the address - of `SELF`. - -:: - - :: 'a : nat : 'S -> ticket 'a : 'S - -Type ``'a`` must be comparable (the ``COMPARE`` primitive must be defined over it). - -- ``READ_TICKET``: Retrieve the information stored in a ticket. Also return the ticket. - -:: - - :: ticket 'a : 'S -> pair address 'a nat : ticket 'a : 'S - -- ``SPLIT_TICKET``: Delete the given ticket and create two tickets with the - same content and ticketer as the original, but with the new provided amounts. - (This can be used to easily implement UTXOs.) - Return None iff the ticket's original amount is not equal to the sum of the - provided amounts. - -:: - - :: ticket 'a : (pair nat nat) : 'S -> - option (pair (ticket 'a) (ticket 'a)) : 'S - -- ``JOIN_TICKETS``: The inverse of ``SPLIT_TICKET``. Delete the given tickets and create a ticket with an amount equal to the - sum of the amounts of the input tickets. - (This can be used to consolidate UTXOs.) - Return None iff the input tickets have a different ticketer or content. - -:: - - :: (pair (ticket 'a) (ticket 'a)) : 'S -> - option (ticket 'a) : 'S - - -Removed instructions -~~~~~~~~~~~~~~~~~~~~ - -:ref:`005_babylon` deprecated the following instructions. Because no smart -contract used these on Mainnet before they got deprecated, they have been -removed. The Michelson type-checker will reject any contract using them. - -- ``CREATE_CONTRACT { storage 'g ; parameter 'p ; code ... }``: - Forge a new contract from a literal. - -:: - - :: key_hash : option key_hash : bool : bool : mutez : 'g : 'S - -> operation : address : 'S - -See the documentation of the new ``CREATE_CONTRACT`` instruction. The -first, third, and fourth parameters are ignored. - -- ``CREATE_ACCOUNT``: Forge an account creation operation. - -:: - - :: key_hash : option key_hash : bool : mutez : 'S - -> operation : address : 'S - -Takes as argument the manager, optional delegate, the delegatable flag -and finally the initial amount taken from the currently executed -contract. This instruction originates a contract with two entrypoints; -``%default`` of type ``unit`` that does nothing and ``%do`` of type -``lambda unit (list operation)`` that executes and returns the -parameter if the sender is the contract's manager. - -- ``STEPS_TO_QUOTA``: Push the remaining steps before the contract - execution must terminate. - -:: - - :: 'S -> nat : 'S - - -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. - -- ``P(\left=A|P(\left)(\right))(\right=I|P(\left)(\right))R``: A syntactic sugar - for building nested pairs. In the case of right combs, `PAIR n` is more efficient. - -:: - - > 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. - -:: - - > 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. In the case of right combs, ``CAR k`` and ``CDR k`` are more efficient. - -:: - - > CA(\rest=[AD]+)R / S => CAR ; C(\rest)R / S - > CD(\rest=[AD]+)R / S => CDR ; C(\rest)R / S - -- ``CAR k``: Access the ``k`` -th part of a right comb of size ``n > k + 1``. ``CAR 0`` is equivalent to ``CAR`` and in general ``CAR k`` is equivalent to ``k`` times the ``CDR`` instruction followed by once the ``CAR`` instruction. Note that this instruction cannot access the last element of a right comb; ``CDR k`` should be used for that. - -:: - - > CAR n / S => GET (2n+1) / S - -- ``CDR k``: Access the rightmost element of a right comb of size ``k``. ``CDR 0`` is a no-op, ``CDR 1`` is equivalent to ``CDR`` and in general ``CDR k`` is equivalent to ``k`` times the ``CDR`` instruction. Note that on a right comb of size ``n > k >= 2``, ``CDR k`` will return the right comb composed of the same elements but the ``k`` leftmost ones. - -:: - - > CDR n / S => GET (2n) / 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. This is equivalent to ``SWAP; UPDATE 1``. - -:: - - > SET_CAR => CDR ; SWAP ; PAIR - -- ``SET_CDR``: Set the right field of a pair. This is equivalent to ``SWAP; UPDATE 2``. - -:: - - > SET_CDR => CAR ; PAIR - -- ``SET_C[AD]+R``: A syntactic sugar for setting fields in nested - pairs. In the case of right combs, `UPDATE n` is more efficient. - -:: - - > 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 - -Concrete syntax ---------------- -.. _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 -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). -- ``bls12_381_g1``\ s and ``bls12_381_g2``\ s are written as their raw bytes, using a big-endian point encoding, `as specified here `__. -- ``bls12_381_fr``\ s are written as their raw bytes, using a little-endian encoding. - -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 - LEVEL - AMOUNT - BALANCE - HASH_KEY - CHECK_SIGNATURE - BLAKE2B - SOURCE - SENDER - SELF - SELF_ADDRESS - CAST - RENAME - CHAIN_ID - -The instructions which accept at most two variable annotations are: - -:: - - UNPAIR - 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. - -:: - - UNPAIR @fist @second - :: pair 'a 'b : 'S - -> @first 'a : @second 'b : 'S - - UNPAIR @first - :: pair 'a 'b : 'S - -> @first 'a : 'b : '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`` accept multiple annotations. Field -annotations for ``PAIR`` give names to leaves of the constructed -nested pair, in order. 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 - -Annotations for nested ``UNPAIR`` are deprecated. - -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 - - SELF_ADDRESS :: 'S -> @self address : 'S - - AMOUNT :: 'S -> @amount mutez : 'S - - NOW :: 'S -> @now timestamp : 'S - - LEVEL :: 'S -> @level nat : '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 ] - -Special annotations -~~~~~~~~~~~~~~~~~~~ -.. _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 -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 - | DUP - | SWAP - | DIG - | DUG - | PUSH - | SOME - | NONE - | UNIT - | NEVER - | IF_NONE { ... } { ... } - | PAIR - | PAIR - | CAR - | CDR - | UNPAIR - | UNPAIR - | LEFT - | RIGHT - | IF_LEFT { ... } { ... } - | NIL - | CONS - | IF_CONS { ... } { ... } - | SIZE - | EMPTY_SET - | EMPTY_MAP - | EMPTY_BIG_MAP - | MAP { ... } - | ITER { ... } - | MEM - | GET - | GET - | UPDATE - | 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 - | SELF_ADDRESS - | CONTRACT - | TRANSFER_TOKENS - | SET_DELEGATE - | CREATE_CONTRACT { ... } - | IMPLICIT_ACCOUNT - | VOTING_POWER - | NOW - | LEVEL - | AMOUNT - | BALANCE - | CHECK_SIGNATURE - | BLAKE2B - | KECCAK - | SHA3 - | SHA256 - | SHA512 - | HASH_KEY - | SOURCE - | SENDER - | ADDRESS - | CHAIN_ID - | TOTAL_VOTING_POWER - | PAIRING_CHECK - | SAPLING_EMPTY_STATE - | SAPLING_VERIFY_UPDATE - | TICKET - | READ_TICKET - | SPLIT_TICKET - | JOIN_TICKETS - ::= - | - | option - | list - | set - | operation - | contract - | ticket - | pair ... - | or - | lambda - | map - | big_map - | bls12_381_g1 - | bls12_381_g2 - | bls12_381_fr - | sapling_transaction - | sapling_state - ::= - | unit - | never - | bool - | int - | nat - | string - | chain_id - | bytes - | mutez - | key_hash - | key - | signature - | timestamp - | address - | option - | or - | pair ... - - -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/009_BA/proof_of_stake.rst b/docs/009_BA/proof_of_stake.rst deleted file mode 100644 index 002055e6aac7f356dae7f92f179ab86b00947cd5..0000000000000000000000000000000000000000 --- a/docs/009_BA/proof_of_stake.rst +++ /dev/null @@ -1,408 +0,0 @@ -.. _proof-of-stake_009_BA: - -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 every ``BLOCKS_PER_ROLL_SNAPSHOT`` = 256 blocks, -which is 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.8333333`` -ꜩ. - -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``. One out of every ``BLOCKS_PER_COMMITMENT`` = 32 blocks -can contain a commitment. There are therefore at most -``BLOCKS_PER_CYCLE / BLOCKS_PER_COMMITMENT`` = 128 commitments. 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. - -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/009_BA/sapling.rst b/docs/009_BA/sapling.rst deleted file mode 100644 index 40c4145ae8ffef66449aaee287752508df660027..0000000000000000000000000000000000000000 --- a/docs/009_BA/sapling.rst +++ /dev/null @@ -1,498 +0,0 @@ -.. _sapling_dev_009_BA: - -**The features described in this page are experimental and have not undergone any security review.** - -Sapling integration -=================== - -Sapling is a protocol enabling privacy-preserving transactions of fungible -tokens in a decentralised -environment. It was designed and implemented by the Electric Coin -Company as the last iteration over a series of previous protocols and -academic works starting with the `Zerocoin seminal -paper `_. - -The reference implementation of Sapling, -`librustzcash `_, was -integrated in the Tezos codebase during 2019. It will be proposed as -part of a protocol amendment during 2020. - -Librustzcash and the Tezos integration implement the protocol -described in this `specification -`_, version 2020.1.0. - - -Sapling -------- - -Keys -~~~~ - -Sapling offers a rich set of keys, each allowing different operations. -A `spending key` allows to spend tokens so if it is lost or -compromised the tokens could remain locked or be stolen. -From a spending key it is possible to derive a corresponding `viewing -key` which allows to view all incoming and outgoing transactions. -The viewing key allows the owner of the tokens to check their balance -and transaction history so if compromised there is a complete loss of -privacy. -On the other hand a viewing key can willingly be shared with a third -party, for example with an auditor for regulatory compliance purposes. - -A viewing key can also derive several diversified `addresses`. -An address can be used to receive funds, much like the address of an -implicit account. - -Additionally `proving keys` can be used to allow the creation of proofs, -thus revealing private information, without being able to spend funds. -They are useful for example in case the spending key is stored in a -hardware wallet but we'd like to use our laptop to craft the -transaction and produce the zero-knowledge proofs, which are -computationally too intensive for an embedded device. - -More details can be found in the `specification document -`_. - -Shielded transactions -~~~~~~~~~~~~~~~~~~~~~ - -Transactions use Bitcoin's UTXO model with the important difference that each -input and output, instead of containing an amount and an address, -are just cryptographic `commitments`. -In order to avoid double spends, it's important to be able to check -that a commitment has not already been spent. In Bitcoin we just need to -check if an output is also later used as an input to verify if it's -already spent. In Sapling however we can't know because inputs are not -linked to outputs. -For this reason for each input of a transaction, the owner must also -publish a `nullifier`, which invalidates it. The nullifier can only be -produced by the owner of a commitment and it's deterministic so that -everybody can check that it hasn't been already published. -Note however that it is not possible to infer which commitment has -been nullified. -Transactions of this form are privacy preserving and are referred to -as `shielded`, because they reveal neither the amount, the sender nor -the receiver. - -The existing set of transactions is referred to as the `shielded pool`. -Unlike Bitcoin, where everybody can compute the set of unspent -outputs of every user, in Sapling only the owner of a viewing key can -find their outputs and verify that they are not already spent. -For this reason, to an external -observer, the shielded pool is always increasing in size and the more -transactions are added the harder it is to pinpoint the commitments -belonging to a user. - -When we spend a commitment there is some additional information that -we need to transmit to the recipient in order for them to spend the -corresponding output. -This data is encrypted under a symmetric key resulting from a -Diffie-Hellman key exchange using the recipient address and an -ephemeral key. -In principle this `ciphertext` can be transmitted off-chain as it's -not needed to verify the integrity of the pool. For convenience, in -Tezos, it is stored together with the commitment and the nullifier on -chain. - -For reasons of efficiency the commitments are stored in an incremental -`Merkle tree `_ which -allows for compact proofs of membership. The root of the tree is all -that is needed to refer to a certain state of the shielded pool. - -In order to ensure the correctness of a transaction, given that there -is information that we wish to remain secret, the spender must also -generate proofs that various good properties are true. -Thanks to the use of `SNARKs `_ -these proofs are very succinct in size, fast to verify and they don't -reveal any private information. - -This model of transaction adapts elegantly to the case when we need to -mint or burn tokens, which is needed to shield or unshield from a -transparent token. -It suffices to add more values in the outputs than in the inputs -to mint and to have more in inputs than outputs to burn. - -Privacy guarantees -~~~~~~~~~~~~~~~~~~ - -We explained that the shielded pool contains one commitment for each -input (spent or not), and one nullifier for each spent input. -These cryptographic commitments hide the amount and the owner of the -tokens they represent. -Additionally commitments are unlinkable meaning that we can not deduce -which input is spent to create an output. - -It should be noted that the number of inputs and outputs of a -transaction is public, which could help link a class of -transactions. This problem can be mitigated by adding any number of -dummy inputs or outputs at the cost of wasting some space. - -The shielded pool communicates with the public ledger by minting and -burning shielded tokens in exchange for public coins. -Therefore going in and out of the shielded pool is public: we know -which address shielded or unshielded and how much. -We can among other things infer the total number of shielded coins. - -Timing and network information can also help to deduce some private -information. -For example by observing the gossip network we might learn the IP -address of somebody that is submitting a shielded transaction. -This can be mitigated by using `TOR -`_. - -Good practices -~~~~~~~~~~~~~~ - -When blending in a group of people, one should always pay attention to -the size and the variety of the group. - -We recommend two good practices. First, do not originate a second -contract if another one has the same functionalities, it will split -the anonymity set. - -Second, remember that shielding and unshielding are public operations. -A typical anti-pattern is to shield from tz1-alice 15.3 tez, and then -unshield 15.3 tez to tz1-bob. It's fairly clear from timing and -amounts that Alice transferred 15.3 tez to Bob. -To decorrelate the two transfers it is important to change the -amounts, let some time pass between the two and perform the -transactions when there is traffic in the pool. -Similar problems exist in ZCash and they are illustrated in this -introductory `blog post -`_. - -There are a number of more sophisticated techniques to deanonymise -users using timing of operations, network monitoring, side-channels on -clients and analysis of number of inputs/outputs just to mention a few -(`A fistful of Bitcoins -`_ is a good -first read). -We advice users to be familiar with the use of the TOR network and to -use clients developed specifically to protect their privacy. - - -Tezos integration ------------------ - -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` -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 -option type which is Some (updated -state and a balance) if the transaction is correct, None otherwise. -A transaction has a list of inputs, outputs, a signature, a balance, -and the root of the Merkle tree containing its inputs. -The verification part checks the zero-knowledge proofs of all inputs -and outputs of the transaction, which guarantee several properties of -correctness. -It also checks a (randomised) signature associated with each input -(which guarantees that the owner forged the transaction), and the -signature that binds the whole transaction together and guarantees the -correctness of the balance. -All the signatures are over the hash of the data that we wish to sign -and the hash function used is Blake2-b, prefixed with the anti-replay string. -The anti-replay string is the the concatenation of the chain id and -the smart contract address. The same string has to be used by the client for -signing. - -Verify_update also checks that the root of the Merkle tree appears in -one of the past states and that the nullifiers are not already -present (i.e. no double spending is happening). -If one of the checks fails the instruction returns None. - -Otherwise the function adds to the new state the nullifiers given with each inputs -and adds the outputs to the Merkle tree, which will produce a new root. -It should be noted that it is possible to generate transactions -referring to an old root, as long as the inputs used were present in -the Merkle tree with that root and were not spent after. -In particular the protocol keeps 120 previous roots and guarantees -that roots are updated only once per block. -Considering 1 block per minute and that each block contains at least -one call to the same contract, a client has 2 hours to have its -transaction accepted before it is considered invalid. - -The nullifiers are stored in a set. The ciphertexts and other relevant -information linked to the commitment of the Merkle tree are -stored in a map indexed by the position of the commitment in the -Merkle tree. - -Lastly the instruction pushes the updated state and the balance as an option -on the stack. - -Example contracts -~~~~~~~~~~~~~~~~~ - -Shielded tez -^^^^^^^^^^^^ - -An example contract to have a shielded tez with a 1 to 1 conversion to -tez is available in the tests of `lib_sapling`. - -Simple Vote Contract -^^^^^^^^^^^^^^^^^^^^ - -One might think to use Sapling to do private voting. -It is possible to adapt shielded transactions to express preferences. -**Note that this is not what Sapling is designed for and it doesn't provide the same properties as an actual private voting protocol.** -A natural naive idea is the following. -Suppose we want a set of users to express a preference for option A or -B, we can generate two Sapling keys with two addresses that are -published and represent the two options. -The contract lets each user create a token which represents one vote -that can then be transferred to address A or B. -Using the published viewing keys everyone can check the outcome of the -vote. -**However note that a transaction can be replayed and we can see the balance of A or B going up. -This system does not offer ballot privacy. -Therefore one should ensure that the vote he is casting cannot be linked to him. -It is possible that the practical situation makes this usable but we recommend in general not to use -it for any important vote.** -Note that using a random elliptic curve element as incoming viewing key allows to generate a -dummy address that cannot be spent. This eases the counting of the votes. -To ensure that the ivk does not correspond to a normal address with spending key, one -can use the Fiat-Shamir heuristic. - - -Fees issue -~~~~~~~~~~ - -We have an additional privacy issue that Z-cash doesn't have. When -interacting with a shielded pool we interact with a smart contract -with a normal transaction and therefore have to pay fees from an -implicit account. -One could guess that private transactions whose fees are paid by the -same implicit account are from the same user. -This can be mitigated by making a service that act as a proxy by -forwarding the user transactions and paying it fees. The user would -then include in the transaction a shielded output for the service that -covers the fees plus a small bonus to pay the service. -This output can be open by the service before sending the transaction -to check that there is enough money to cover its fees. As for Z-cash, -users interacting with the proxy should use TOR or mitigate network -analysis as they wish. - -Gas, storage and costs -~~~~~~~~~~~~~~~~~~~~~~ - -Gas evaluation is not yet done. - -RPCs -~~~~ - -There are two Sapling RPCs under the prefix `context/sapling`. -`get_size` returns a pair with the size of the set of commitments -and the size of the set of nullifiers. -`get_diff` takes two optional starting offsets `cm_from` and `nf_from` -and returns the sapling state that was added from the offsets to the -current size. In particular it returns three lists, commitments, -ciphertexts from position `cm_from` up to the last one added and -nullifiers, from `nf_from` to the last one added. -Additionally it returns the last computed root of the merkle tree so -that a client updating its tree using the diff can verify the -correctness of the result. - -Client -~~~~~~ - -Wallet -^^^^^^ - -tezos-client supports Sapling keys and can send -shielded transactions to smart contracts. - -The client supports two ways to generate a new Sapling spending key. -It can be generated from a mnemonic using `BIP39 -`_, so -that it can be recovered in case of loss using the mnemonic. -Alternatively it is possible to derive new keys from existing ones -using `ZIP32 -`_, a Sapling -variant of `BIP32 -`_ for -hierarchical deterministic wallets. As usual, in this case it is -important to note the derivation path of the key to be able to recover -it in case of loss. -At the moment there is no hardware wallet support, keys are stored in -`~/.tezos-client/sapling_keys` by default encrypted with a password. -**Users should take care to backup this file.** - -The client can also derive addresses from viewing keys. -By default addresses are generated using an increasing counter called -the address index. Not all indexes corresponds to valid addresses for -each key so it is normal to see an increasing counter that -occasionally skips a few position. - -Because for now the only support for Sapling keys is to interact with -smart contracts, the client binds each newly generated key to a -specific smart contract address. - -Operations -^^^^^^^^^^ - -The client also facilitates the creation of shielded transactions and -their transfer as arguments of smart contracts. -For now there is seamless integration to send transactions to the -reference shielded-tez contract and we are planning to support a -larger class of contracts. - -For the shielded-tez smart contract, the client supports shielding, -unshielding and shielded transactions. -In the case of shielded transactions there are two commands, one to -forge a transaction and save it to file and one to submit it to the -smart contract. -The idea is that a user should not use their own transparent tz{1,2,3} -address to submit a shielded address but rather have a third party -inject it. - -Message argument -^^^^^^^^^^^^^^^^ -Sapling also allows to send an arbitrary encrypted message attached -to an output. -The message size has to be fixed by pool for privacy reasons. -For now it is fixed overall at eight bytes. An incorrect message length -will raise a failure in our client and the protocol will reject the -transaction. Our client adds a default zero's filled message of the -right length. If a message is provided with the --message option, -the client will pad it or truncate it if necessary. A warning message -is printed only if the user's message is truncated. - - -Code base -~~~~~~~~~ - -The current code-base is organized in three main components. -There is a core library called `lib_sapling` which binds `librustzcash`, -adds all the data structures necessary to run the sapling -protocol and includes a simple client and baker. -Under the protocol directory there is a `lib_client_sapling` library -which implements a full client capable of handling Sapling keys and -forging transactions. -Lastly in the protocol there is a efficient implementation of the -Sapling storage, in the spirit of `big_map`s, and the integration of -`SAPLING_VERIFY_UPDATE` in the Michelson interpreter. - -Protocol -^^^^^^^^ - -In order to export the Sapling library to the protocol we first need -to expose it through the environment that sandboxes the protocol. -The changes under `src/lib_protocol_environment` are simple but very -relevant as any change of the environment requires a manual update of the -Tezos node. This changes are part of version V1 of the environment -while protocols 000 to 006 depends on version V0. - -There are two main changes to Tezos' economic protocol, the storage -for Sapling and the addition of `SAPLING_VERIFY_UPDATE` to the Michelson -interpreter. - -Given that the storage of a Sapling contract can be substantially -large, it is important to provide an efficient implementation. -Similarly to what it's done for big_maps, the storage of Sapling can't -be entirely deserialized and modified in memory but only a diff of the -changes is kept by the interpreter and applied at the end of each -smart contract call. - -In the Michelson interpreter two new types are added, `sapling_state` and -`sapling_transaction`, and the instruction `SAPLING_VERIFY_UPDATE`. - -Client -^^^^^^ - -Under `lib_client_sapling` there is the client integration -with the support for Sapling keys and forging of transactions. -The main difference from the existing Tezos client is the need for the -Sapling client to keep an additional state, for each contract. -Because Sapling uses a UTXO model it is necessary for a client to -compute the set of unspent outputs in order to forge new transactions. -Computing this set requires scanning all the state of a contract which -can be expensive. -For this reason the client keeps a local state of the unspent outputs -after the last synchronization and updates it before performing any -Sapling command. -The update is done using the RPCs to recover the new updates since the -last known position. - -The state of all sapling contracts is stored in -`~/.tezos-client/sapling_states`. This file can be regenerated from -the chain in case of loss. However disclosure of this file will reveal -the balance and the unspent outputs of all viewing keys. - -Memo -^^^^^^ - -Sapling offers the possibility to add an arbitrary memo to any -created output. The memo is encrypted and available to anyone -owning the outgoing viewing key or the spending key. -For privacy reasons the size of the memo is fixed per contract -and it is chosen at origination time. -A transaction containing an output with a different memo-size -will be rejected. - -Sandbox tutorial -~~~~~~~~~~~~~~~~ - -As usual it's possible to test the system end-to-end using the -:ref:`sandboxed-mode`. -After having set up the sandbox and originated the contract, a good -way to get familiar with the system is to generate keys and then -perform the full cycle of shielding, shielded transfer and -unshielding. - -:: - - # set up the sandbox - ./src/bin_node/tezos-sandboxed-node.sh 1 --connections 0 & - eval `./src/bin_client/tezos-init-sandboxed-client.sh 1` - tezos-activate-alpha - - # originate the contract with its initial empty sapling storage, - # bake a block to include it. - # { } represents an empty Sapling state. - tezos-client originate contract shielded-tez transferring 0 from bootstrap1 \ - running src/proto_009_PsFLorBA/lib_protocol/test/contracts/sapling_contract.tz \ - --init '{ }' --burn-cap 3 & - tezos-client bake for bootstrap1 - - # as usual you can check the tezos-client manual - tezos-client sapling man - - # generate two shielded keys for Alice and Bob and use them for the shielded-tez contract - # the memo size has to be indicated - tezos-client sapling gen key alice - tezos-client sapling use key alice for contract shielded-tez --memo-size 8 - tezos-client sapling gen key bob - tezos-client sapling use key bob for contract shielded-tez --memo-size 8 - - # generate an address for Alice to receive shielded tokens. - tezos-client sapling gen address alice - zet1AliceXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX # Alice's address - - - # shield 10 tez from bootstrap1 to alice - tezos-client sapling shield 10 from bootstrap1 to zet1AliceXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX using shielded-tez --burn-cap 2 & - tezos-client bake for bootstrap1 - tezos-client sapling get balance for alice in contract shielded-tez - - # generate an address for Bob to receive shielded tokens. - tezos-client sapling gen address bob - zet1BobXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX # Bob's address - - # forge a shielded transaction from alice to bob that is saved to a file - tezos-client sapling forge transaction 10 from alice to zet1BobXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX using shielded-tez - - # submit the shielded transaction from any transparent account - tezos-client sapling submit sapling_transaction from bootstrap2 using shielded-tez --burn-cap 1 & - tezos-client bake for bootstrap1 - tezos-client sapling get balance for bob in contract shielded-tez - - # unshield from bob to any transparent account - tezos-client sapling unshield 10 from bob to bootstrap1 using shielded-tez --burn-cap 1 - ctrl+z # to put the process in background - tezos-client bake for bootstrap1 - fg # to put resume the transfer diff --git a/docs/009_BA/voting.rst b/docs/009_BA/voting.rst deleted file mode 100644 index 126e960d8050141ab850fcdc124cb5220ffd2925..0000000000000000000000000000000000000000 --- a/docs/009_BA/voting.rst +++ /dev/null @@ -1,193 +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 five periods, each of 20480 blocks (or -~two weeks), for a total of approximately 2 months and a half. - -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 exploration 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. -- `Exploration period`: delegates can cast one vote to pursue the - voting process or not with the winning proposal using the `ballot` - operation. At the end of a exploration period if participation - reaches the quorum and the proposal has a super-majority in favor, - we proceed to a cooldown period. Otherwise we go back to a proposal - period. -- `Cooldown period`: The only purpose of this period is to let some - time elapse before the promotion period. -- `Promotion period`: delegates can cast one vote to promote or not - the proposal using the `ballot` operation. At the end of a - promotion period if participation reaches the quorum and the - proposal has a super-majority in favor, we proceed to adoption - period. Otherwise we go back to a proposal period. -- `Adoption period`: at the end of the period the proposal is activated - as the new protocol and we go back to a proposal period. - -Each of the periods above are called a `voting period`. It is important to note -that the stake of each delegate is computed at the beginning of each voting -period, and if the delegate owns one roll or more, its stake in number of rolls is -stored in a list called the `voting listings`. - -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_009_PsFLorBA/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_009_PsFLorBA/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: "exploration" - 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: "cooldown" - 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 an exploration or a promotion period, -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_009_BA`. - -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 57a0f6906550e764e72310011f73f3951787a8ea..b57a2da6d97c5cc9e7e759beab3b3e97cce65367 100644 --- a/docs/Makefile +++ b/docs/Makefile @@ -15,7 +15,6 @@ FLORENCE_LONG = PsFLorenaUUuikDWvMDr6fGBRG8kt3e3D3fHoXK1j1BFRxeSH4i EDO_LONG = PtEdo2ZkT9oKpimTah6x2embF25oss54njMuPzkJTEi5RqfdZFA ALPHA_SHORT = alpha -FLOR_BA_SHORT = 009-PsFLorBA FLORENCE_SHORT = 009-PsFLoren EDO_SHORT = 008-PtEdo2Zk @@ -33,11 +32,6 @@ manuals: main @../tezos-baker-$(ALPHA_SHORT) man -verbosity 3 -format html | sed "s#${HOME}#\$$HOME#g" > alpha/tezos-baker-alpha.html @../tezos-endorser-$(ALPHA_SHORT) man -verbosity 3 -format html | sed "s#${HOME}#\$$HOME#g" > alpha/tezos-endorser-alpha.html @../tezos-accuser-$(ALPHA_SHORT) man -verbosity 3 -format html | sed "s#${HOME}#\$$HOME#g" > alpha/tezos-accuser-alpha.html - # 009 (Florence with baking accounts) protocol - @../tezos-client -protocol $(FLOR_BA_LONG) man -verbosity 3 -format html | sed "s#${HOME}#\$$HOME#g" > 009_BA/tezos-client-009.html - @../tezos-baker-$(FLOR_BA_SHORT) man -verbosity 3 -format html | sed "s#${HOME}#\$$HOME#g" > 009_BA/tezos-baker-009.html - @../tezos-endorser-$(FLOR_BA_SHORT) man -verbosity 3 -format html | sed "s#${HOME}#\$$HOME#g" > 009_BA/tezos-endorser-009.html - @../tezos-accuser-$(FLOR_BA_SHORT) man -verbosity 3 -format html | sed "s#${HOME}#\$$HOME#g" > 009_BA/tezos-accuser-009.html # 009 (Florence) protocol @../tezos-client -protocol $(FLORENCE_LONG) man -verbosity 3 -format html | sed "s#${HOME}#\$$HOME#g" > 009/tezos-client-009.html @../tezos-baker-$(FLORENCE_SHORT) man -verbosity 3 -format html | sed "s#${HOME}#\$$HOME#g" > 009/tezos-baker-009.html @@ -77,7 +71,6 @@ redirectcheck: xrefscheck: $(CHECKXREFS) 008 $(CHECKXREFS) -l 009 - $(CHECKXREFS) -l 009_BA scriptsindoccheck: introduction/test_howtoget.sh install-bin-bionic @@ -105,9 +98,8 @@ $(DOCGENDIR)/rpc_doc.exe: @cd .. && dune build docs/$(DOCGENDIR)/rpc_doc.exe rpc: $(DOCGENDIR)/rpc_doc.exe - @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 @dune exec $(DOCGENDIR)/rpc_doc.exe shell > shell/rpc.rst @@ -130,5 +122,5 @@ html: Makefile api/errors.rst rpc p2p clean: @-rm -Rf "$(BUILDDIR)" - @-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 + @-rm -Rf api/errors.rst 008/rpc.rst 009/rpc.rst alpha/rpc.rst shell/rpc.rst shell/p2p_api.rst + @-rm -Rf api/tezos-*.html api/tezos-*.txt 008/tezos-*.html 009/tezos-*.html diff --git a/docs/doc_gen/rpc_doc.ml b/docs/doc_gen/rpc_doc.ml index 81a4351e933b06dc1de8770ef732aee7aa0f76ad..1c5a5f3d36ce0ff2949f818a48c7f9e6761cf9cd 100644 --- a/docs/doc_gen/rpc_doc.ml +++ b/docs/doc_gen/rpc_doc.ml @@ -31,15 +31,11 @@ let protocols = "Alpha", Some "/include/rpc_introduction.rst.inc", "ProtoALphaALphaALphaALphaALphaALphaALphaALphaDdp3zK" ); - ( "009_BA", - "009 Florence with baking accounts", - Some "/include/rpc_introduction.rst.inc", - "PsFLorBArSaXjuy9oP76Qv1v2FRYnUs7TFtteK5GkRBC24JvbdE" ); ( "009", "009 Florence", Some "/include/rpc_introduction.rst.inc", "PsFLorenaUUuikDWvMDr6fGBRG8kt3e3D3fHoXK1j1BFRxeSH4i" ); - ( "008", + ( "", "008 Edo", Some "/include/rpc_introduction.rst.inc", "PtEdo2ZkT9oKpimTah6x2embF25oss54njMuPzkJTEi5RqfdZFA" ) ] diff --git a/docs/index.rst b/docs/index.rst index e630c4a763803371efd744bd3a995fbb682df1a3..794a324602e3c979992841655b530343bb79617a 100644 --- a/docs/index.rst +++ b/docs/index.rst @@ -137,7 +137,7 @@ in the :ref:`introduction `. .. toctree:: :maxdepth: 2 - :caption: 009 Florence (No Baking Accounts) doc: + :caption: 009 Florence doc: 009/michelson 009/proof_of_stake @@ -147,18 +147,6 @@ in the :ref:`introduction `. 009/cli-commands 009/rpc -.. toctree:: - :maxdepth: 2 - :caption: 009 Florence with Baking Accounts doc: - - 009_BA/michelson - 009_BA/proof_of_stake - 009_BA/sapling - 009_BA/voting - 009_BA/glossary - 009_BA/cli-commands - 009_BA/rpc - .. toctree:: :maxdepth: 2 :caption: Alpha Development Protocol doc: @@ -205,7 +193,6 @@ in the :ref:`introduction `. protocols/007_delphi protocols/008_edo protocols/009_florence - protocols/009_florence_BA protocols/alpha .. toctree:: diff --git a/docs/introduction/test_networks.rst b/docs/introduction/test_networks.rst index d07518d6431ecf2942230ec229c3261c96a71d1f..f6261dc1c80296c428cf82403e6c78cbde5c56e8 100644 --- a/docs/introduction/test_networks.rst +++ b/docs/introduction/test_networks.rst @@ -28,8 +28,35 @@ You can obtain the key to these accounts from a faucet to claim the funds. All networks share the same faucet: https://faucet.tzalpha.net/. The keys obtained from this faucet can be used in all test networks. +Florencenet +----------- + +- Built-in network alias: ``florencenet`` (see :ref:`builtin_networks`) + + * Available on ``master``, will be available in version 9.0 + +- Run Docker image: ``wget -O florencenet.sh https://gitlab.com/tezos/tezos/raw/latest-release/scripts/tezos-docker-manager.sh`` + +Florencenet is a test network running the PsFLoren protocol. +Florencenet will run until Florence is rejected or replaced by another protocol on Mainnet. + +On Florencenet, the following constants differ from Mainnet: + +- ``preserved_cycles`` is 3 instead of 5; +- ``blocks_per_cycle`` is 2048 instead of 4096; +- ``blocks_per_voting_period`` is 1024 instead of 32768; +- ``time_between_blocks`` is ``[ 30, 20 ]`` instead of ``[ 60, 40 ]``; +- ``test_chain_duration`` is 0 instead of 1966080; +- ``delay_per_missing_endorsement`` is 4 instead of 8. + +This results in a faster chain than Mainnet: + +- 2 blocks per minute; +- a cycle should last about 17 hours; +- a voting period lasts half a cycle and should thus last about 8 hours. + Edo2net ------- +------- - Built-in network alias: ``edo2net`` (see :ref:`builtin_networks`) diff --git a/scripts/install_build_deps.raw.sh b/scripts/install_build_deps.raw.sh index 23388bdb45699bce2404eea949c2b5548e1c05a0..e89e8811911b263e498f6e92f28dc184153b3e4e 100755 --- a/scripts/install_build_deps.raw.sh +++ b/scripts/install_build_deps.raw.sh @@ -17,7 +17,7 @@ export OPAMYES=${OPAMYES:=true} # Note that install_build_deps.sh calls install_build_deps.rust.sh # which checks whether Rust is installed with the right version and explains how # to install it if needed, so using opam depext is redundant anyway. -opam depext conf-gmp conf-libev conf-m4 conf-perl conf-pkg-config conf-hidapi ctypes-foreign conf-autoconf conf-libffi #conf-rust +opam depext conf-gmp conf-libev conf-perl conf-pkg-config conf-hidapi ctypes-foreign conf-autoconf conf-libffi #conf-rust ## In an ideal world, `--with-test` should be present only when using ## `--dev`. But this would probably break the CI, so we postponed this diff --git a/scripts/install_build_deps.sh b/scripts/install_build_deps.sh index 8fa25a84b580ea32ec83258eaaa23f933a0f0f27..dbff5a1bf68e458fa139405ee13d391301cb8445 100755 --- a/scripts/install_build_deps.sh +++ b/scripts/install_build_deps.sh @@ -13,21 +13,6 @@ else dev= fi -# Check if the default opam repo was set in this switch -default_switch= -if opam remote -s | grep -q default ; then - default_switch=yes -fi - -# install dev dependencies if needed -if [ -n "$dev" ]; then - opam remote add default --rank=-1 > /dev/null 2>&1 || true - opam install merlin odoc utop ocp-indent ocaml-lsp-server --criteria="-changed,-removed" -fi - -# remove the default repo so install tezos dependencies -opam repository remove default > /dev/null 2>&1 - opam repository set-url tezos --dont-select $opam_repository || \ opam repository add tezos --dont-select $opam_repository > /dev/null 2>&1 @@ -44,8 +29,22 @@ fi eval $(opam env --shell=sh) +# Check if the default opam repo was set in this switch +default_switch= +if opam remote -s | grep -q default ; then + default_switch=yes +fi + +# remove the default repo so install tezos dependencies +opam repository remove default > /dev/null 2>&1 + if [ "$(ocaml -vnum)" != "$ocaml_version" ]; then - opam install --unlock-base ocaml-base-compiler.$ocaml_version + # If not removed, automatically installed dependencies would be + # (tried to be) rebuilt in their old version with the new compiler + # while they will probably be updated (and at least reinstalled) + # by the next steps of the script + opam remove -a --yes + opam install --yes --unlock-base ocaml-base-compiler.$ocaml_version fi # Must be done before install_build_deps.raw.sh because install_build_deps.raw.sh installs @@ -56,9 +55,14 @@ opam install --yes opam-depext "$script_dir"/install_build_deps.raw.sh -# add back the default repo if it was present in the first place. -# we add the rank here even if it wasn't there just to be on the -# safe side -if [ -n "$default_switch" ]; then +# add back the default repo if asked to or it was present in the first +# place. we add the rank here even if it wasn't there just to be on +# the safe side +if [ -n "$default_switch" ] || [ -n "$dev" ]; then opam remote add default --rank=-1 > /dev/null 2>&1 || true fi + +# install dev dependencies if asked +if [ -n "$dev" ]; then + opam install --yes merlin odoc utop ocp-indent ocaml-lsp-server --criteria="-changed,-removed" +fi diff --git a/scripts/version.sh b/scripts/version.sh index c0ed1c860256eb648d37b079eb1e7f6602b43e30..3c8622b25539c12c634c10437f7bf3173374928c 100755 --- a/scripts/version.sh +++ b/scripts/version.sh @@ -13,7 +13,7 @@ recommended_rust_version=1.44.0 full_opam_repository_tag=eb6f20daffff6dc5c67b4b55b87bf6b0e600c4d7 ## opam_repository is an additional, tezos-specific opam repository. -opam_repository_tag=5554281d9e3a226cf98b0c9e8721afad2973c150 +opam_repository_tag=ecb12b00769179e6022ad1547b69950781a45061 opam_repository_url=https://gitlab.com/tezos/opam-repository.git opam_repository=$opam_repository_url\#$opam_repository_tag diff --git a/src/lib_base/test/test_time.ml b/src/lib_base/test/test_time.ml index 76cdf30944bb8a3a63aa0fac02efa0f45c1c3505..78c381b6e18f648e1f29ddff8e0c8156155a8ce8 100644 --- a/src/lib_base/test/test_time.ml +++ b/src/lib_base/test/test_time.ml @@ -81,6 +81,19 @@ module Protocol = struct let j = Data_encoding.Json.construct encoding t in let tt = Data_encoding.Json.destruct encoding j in Crowbar.check_eq ~pp ~eq:equal t tt) + + let () = + Crowbar.add_test + ~name:"Base.Time.Protocol.to_notation roundtrip" + [Crowbar.range 1000] + (fun i -> + let close_to_epoch = add epoch (Int64.neg @@ Int64.of_int i) in + let s = to_notation close_to_epoch in + match of_notation s with + | None -> + Crowbar.fail "Failed to roundtrip notation" + | Some after_roundtrip -> + Crowbar.check_eq ~pp ~eq:equal close_to_epoch after_roundtrip) end module System = struct diff --git a/src/lib_base/time.ml b/src/lib_base/time.ml index 6189c34e324bac795b606f37583057f19222ddf9..8084098e808b80d385ae4c33e5daa751a4855b1e 100644 --- a/src/lib_base/time.ml +++ b/src/lib_base/time.ml @@ -43,6 +43,12 @@ module Protocol = struct let to_ptime t = let days = Int64.to_int (Int64.div t 86_400L) in let ps = Int64.mul (Int64.rem t 86_400L) 1_000_000_000_000L in + let (days, ps) = + if ps < 0L then + (* [Ptime.Span.of_d_ps] only accepts picoseconds in the range 0L-86_399_999_999_999_999L. Subtract a day and add a day's worth of picoseconds if need be. *) + (Int.pred days, Int64.(add ps (mul 86_400L 1_000_000_000_000L))) + else (days, ps) + in match Option.bind (Ptime.Span.of_d_ps (days, ps)) Ptime.of_span with | None -> invalid_arg "Time.Protocol.to_ptime" @@ -85,15 +91,15 @@ module Protocol = struct Data_encoding.Json.cannot_destruct "Time.Protocol.of_notation") string - let max_rfc3999 = of_ptime Ptime.max + let max_rfc3339 = of_ptime Ptime.max - let min_rfc3999 = of_ptime Ptime.min + let min_rfc3339 = of_ptime Ptime.min let as_string_encoding = let open Data_encoding in conv (fun i -> - if min_rfc3999 <= i && i <= max_rfc3999 then to_notation i + if min_rfc3339 <= i && i <= max_rfc3339 then to_notation i else Int64.to_string i) ( Json.wrap_error (* NOTE: this encoding is only used as a building block for a json diff --git a/src/lib_base/time.mli b/src/lib_base/time.mli index 287225d298c78cbd7a08cc6dbf494b663f8a5427..cd3c08da362ed5c6503c16a3096da265ad56ded2 100644 --- a/src/lib_base/time.mli +++ b/src/lib_base/time.mli @@ -41,13 +41,20 @@ protocol update changes the notion of time. - Protocol time and system time have different levels of precision. - Protocol time and system time have different end-of-times. Respectively - that's int64 end-of-time (some time in the year 292277026596) and rfc3339 + that's int64 end-of-time (some time in the year 292277026596) and RFC3339 end-of-time (end of the year 9999). + Note that while Protocol time has the int64 range, many of its functions + do not work outside of the RFC3339 range, namely: + - all [xx_notation_xx] functions (will be renamed and moved to an RFC + submodule later) + - [rfc_encoding] + - [pp_hum] + *) module Protocol : sig - (** {1:Protocol time} *) + (** {1 Protocol time} *) (** The out-of-protocol view of in-protocol timestamps. The precision of in-protocol timestamps are only precise to the second. @@ -70,27 +77,50 @@ module Protocol : sig [b] is later than [a]. *) val diff : t -> t -> int64 - (** Conversions to and from string representations. *) + (** {2 Conversions to and from string representations} *) + + (** Convert a string in the RFC3339 format (e.g., ["1970-01-01T00:00:00Z"]) into a protocol time. + Invalid RFC3339 notations will return [None]. + Note that years outside the 0000-9999 range are invalid RFC3339-wise. *) val of_notation : string -> t option + (** Convert a string in the RFC3339 format (e.g., ["1970-01-01T00:00:00Z"]) into a protocol time. + Invalid RFC3339 notations will raise [Invalid_argument]. + + Note that years outside the 0000-9999 range are invalid RFC3339-wise. *) val of_notation_exn : string -> t + (** Convert a protocol time into an RFC3339 notation (e.g., ["1970-01-01T00:00:00Z"]). + + Note that years outside the 0000-9999 range will raise [Invalid_argument] as they are invalid RFC3339-wise. *) val to_notation : t -> string (** Conversion to and from "number of seconds since epoch" representation. *) + (** Make a Protocol time from a number of seconds since the {!epoch}. *) val of_seconds : int64 -> t + (** Convert a Protocol time into a number of seconds since the {!epoch}. *) val to_seconds : t -> int64 - (** Serialization functions *) + (** {2 Serialization functions} *) + + (** Binary and JSON encoding. + + Binary is always encoding/decoding as [int64]. + JSON is more complex (for backward compatibility and user-friendliness): + - encoding uses the RFC3339 format (e.g., ["1970-01-01T00:00:00Z"]) if the year + is between 0000 and 9999 (RFC3339-compatible); otherwise it uses the [int64] format + - decoding tries to decode as an RFC3339 notation, and if it fails, it decodes as + [int64]. + *) val encoding : t Data_encoding.t - (* Note: the RFC has a different range than the internal representation. - Specifically, the RFC can only represent times from 0000-00-00 and - 9999-12-31 (inclusive). The rfc-encoding fails for dates outside of this + (** Note: the RFC has a different range than the internal representation. + Specifically, the RFC can only represent times between 0000-00-00 and + 9999-12-31 (inclusive). The RFC-encoding fails for dates outside of this range. For this reason, it is preferable to use {!encoding} and only resort to @@ -99,12 +129,12 @@ module Protocol : sig val rpc_arg : t RPC_arg.t - (** Pretty-printing functions *) + (** {2 Pretty-printing functions} *) - (* Pretty print as a number of seconds after epoch. *) + (** Pretty print as a number of seconds after epoch. *) val pp : Format.formatter -> t -> unit - (* Note: pretty-printing uses the rfc3999 for human-readability. As mentioned + (** Note: pretty-printing uses the RFC3339 for human-readability. As mentioned in the comment on {!rfc_encoding}, this representation fails when given dates too far in the future (after 9999-12-31) or the past (before 0000-00-00). @@ -114,7 +144,7 @@ module Protocol : sig end module System : sig - (** {1:System time} *) + (** {1 System time} *) (** A representation of timestamps. @@ -127,6 +157,7 @@ module System : sig type t = Ptime.t + (** Unix epoch is 1970-01-01 00:00:00.000000000000 UTC *) val epoch : t module Span : sig @@ -141,7 +172,7 @@ module System : sig span cannot be represented. *) val of_seconds_exn : float -> t - (** Serialization functions *) + (** {2 Serialization functions} *) val rpc_arg : t RPC_arg.t @@ -150,24 +181,43 @@ module System : sig val encoding : t Data_encoding.t end - (** Conversions to and from Protocol time. Note that converting system time to - protocol time truncates any subsecond precision. *) + (** {2 Conversions to and from Protocol time} *) + (** Note that converting system time to protocol time truncates any subsecond precision. *) + + (** Convert a Protocol time into a System time. + + Return [None] if the Protocol time is outside the RFC3339 range. *) val of_protocol_opt : Protocol.t -> t option + (** Convert a Protocol time into a System time. + + Raises [Invalid_argument] if the Protocol time is outside the RFC3339 range. *) val of_protocol_exn : Protocol.t -> t + (** Convert a System time into a Protocol time. + + Note that subseconds are truncated. *) val to_protocol : t -> Protocol.t - (** Conversions to and from string. It uses rfc3339. *) + (** {2 Conversions to and from string (using RFC3339)} *) + + (** Convert a string in the RFC3339 format (e.g., ["1970-01-01T00:00:00.000-00:00"]) into a system time. + Invalid RFC3339 notations will return [None]. + Note that years outside the 0000-9999 range are invalid RFC3339-wise. *) val of_notation_opt : string -> t option + (** Convert a string in the RFC3339 format (e.g., ["1970-01-01T00:00:00.000-00:00"]) into a system time. + Invalid RFC3339 notations will raise [Invalid_argument]. + + Note that years outside the 0000-9999 range are invalid RFC3339-wise. *) val of_notation_exn : string -> t + (** Convert a system time into an RFC3339 notation (e.g., ["1970-01-01T00:00:00.000-00:00"]). *) val to_notation : t -> string - (** Serialization. *) + (** {2 Serialization} *) val encoding : t Data_encoding.t @@ -175,11 +225,11 @@ module System : sig val rpc_arg : t RPC_arg.t - (** Pretty-printing *) + (** {2 Pretty-printing} *) val pp_hum : Format.formatter -> t -> unit - (** Timestamping data. *) + (** {2 Timestamping data} *) (** Data with an associated time stamp. *) type 'a stamped = {data : 'a; stamp : t} @@ -196,7 +246,7 @@ module System : sig timestamp), or [None] if both [a] and [b] are [None]. *) val recent : ('a * t) option -> ('a * t) option -> ('a * t) option - (** Helper modules *) + (** {2 Helper modules} *) val hash : t -> int diff --git a/src/lib_protocol_environment/environment_V0.ml b/src/lib_protocol_environment/environment_V0.ml index 225402a248e25d93b694ea64cbfbb956e2be78bc..0422700c62c2d29999788306f0fa7a0a2c00b9e8 100644 --- a/src/lib_protocol_environment/environment_V0.ml +++ b/src/lib_protocol_environment/environment_V0.ml @@ -433,6 +433,8 @@ struct let return x = Lwt.return (`Ok x) + let return_chunked x = Lwt.return (`OkChunk x) + let return_stream x = Lwt.return (`OkStream x) let not_found = Lwt.return (`Not_found None) @@ -448,7 +450,7 @@ struct handler p q i >>= function | `Ok o -> - RPC_answer.return o + RPC_answer.return_chunked o | `OkStream s -> RPC_answer.return_stream s | `Created s -> diff --git a/src/lib_protocol_environment/environment_V1.ml b/src/lib_protocol_environment/environment_V1.ml index 3db4d284e096b99d079bb07a65dea40d37dd7260..fd8d723c73438bb66e51dfa6f60ab6d4b33888cf 100644 --- a/src/lib_protocol_environment/environment_V1.ml +++ b/src/lib_protocol_environment/environment_V1.ml @@ -620,6 +620,8 @@ struct let return x = Lwt.return (`Ok x) + let return_chunked x = Lwt.return (`OkChunk x) + let return_stream x = Lwt.return (`OkStream x) let not_found = Lwt.return (`Not_found None) @@ -635,7 +637,7 @@ struct handler p q i >>= function | `Ok o -> - RPC_answer.return o + RPC_answer.return_chunked o | `OkStream s -> RPC_answer.return_stream s | `Created s -> diff --git a/src/lib_protocol_environment/environment_V2.ml b/src/lib_protocol_environment/environment_V2.ml index 927c87a95510ed1c1e6e151da2e1602f51753aac..128916cc132842d6bb28df95b60e91156cb9fb5d 100644 --- a/src/lib_protocol_environment/environment_V2.ml +++ b/src/lib_protocol_environment/environment_V2.ml @@ -633,6 +633,8 @@ struct let return x = Lwt.return (`Ok x) + let return_chunked x = Lwt.return (`OkChunk x) + let return_stream x = Lwt.return (`OkStream x) let not_found = Lwt.return (`Not_found None) @@ -648,7 +650,7 @@ struct handler p q i >>= function | `Ok o -> - RPC_answer.return o + RPC_answer.return_chunked o | `OkStream s -> RPC_answer.return_stream s | `Created s -> diff --git a/src/lib_rpc/RPC_answer.ml b/src/lib_rpc/RPC_answer.ml index 06b5044d93539cfab2fd502a3ef92188e0007472..9d1dc54078773045f0cdd7c117b48dcdb6072f34 100644 --- a/src/lib_rpc/RPC_answer.ml +++ b/src/lib_rpc/RPC_answer.ml @@ -26,6 +26,7 @@ (** Return type for service handler *) type 'o t = [ `Ok of 'o (* 200 *) + | `OkChunk of 'o (* 200 *) | `OkStream of 'o stream (* 200 *) | `Created of string option (* 201 *) | `No_content (* 204 *) @@ -43,6 +44,8 @@ and 'a stream = 'a Resto_directory.Answer.stream = { let return x = Lwt.return (`Ok x) +let return_chunked x = Lwt.return (`OkChunk x) + let return_unit = Lwt.return (`Ok ()) let return_stream x = Lwt.return (`OkStream x) diff --git a/src/lib_rpc/RPC_answer.mli b/src/lib_rpc/RPC_answer.mli index b82e4289d8b8b804aafb413f0972fc667ffaeff8..c4c451adad69291ab0942e1cb91aa1ad87def4af 100644 --- a/src/lib_rpc/RPC_answer.mli +++ b/src/lib_rpc/RPC_answer.mli @@ -26,6 +26,7 @@ (** Return type for service handler *) type 'o t = [ `Ok of 'o (* 200 *) + | `OkChunk of 'o (* 200 *) | `OkStream of 'o stream (* 200 *) | `Created of string option (* 201 *) | `No_content (* 204 *) @@ -43,6 +44,8 @@ and 'a stream = 'a Resto_directory.Answer.stream = { val return : 'o -> 'o t Lwt.t +val return_chunked : 'o -> 'o t Lwt.t + val return_unit : unit t Lwt.t val return_stream : 'o stream -> 'o t Lwt.t diff --git a/src/lib_rpc/RPC_directory.ml b/src/lib_rpc/RPC_directory.ml index bba7b8611228653544d1cb184d463fbea629d3b5..38e060275cfa89fcb57ca415587eac8dba1a4d03 100644 --- a/src/lib_rpc/RPC_directory.ml +++ b/src/lib_rpc/RPC_directory.ml @@ -43,6 +43,12 @@ let register dir service handler = handler p q i >>= function Ok o -> RPC_answer.return o | Error e -> RPC_answer.fail e) +let register_chunked dir service handler = + gen_register dir service (fun p q i -> + handler p q i + >>= function + | Ok o -> RPC_answer.return_chunked o | Error e -> RPC_answer.fail e) + let opt_register dir service handler = gen_register dir service (fun p q i -> handler p q i @@ -62,6 +68,8 @@ open Curry let register0 root s f = register root s (curry Z f) +let register0_chunked root s f = register_chunked root s (curry Z f) + let register1 root s f = register root s (curry (S Z) f) let register2 root s f = register root s (curry (S (S Z)) f) diff --git a/src/lib_rpc/RPC_directory.mli b/src/lib_rpc/RPC_directory.mli index 8ae3d1e6f187e6cf119eae81f37469639d66a1da..4be09bf5b4898f0e96a8de7568fe9a2a6fd39002 100644 --- a/src/lib_rpc/RPC_directory.mli +++ b/src/lib_rpc/RPC_directory.mli @@ -36,6 +36,12 @@ val register : ('p -> 'q -> 'i -> 'o tzresult Lwt.t) -> 'prefix directory +val register_chunked : + 'prefix directory -> + ([< Resto.meth], 'prefix, 'p, 'q, 'i, 'o) RPC_service.t -> + ('p -> 'q -> 'i -> 'o tzresult Lwt.t) -> + 'prefix directory + val opt_register : 'prefix directory -> ([< Resto.meth], 'prefix, 'p, 'q, 'i, 'o) RPC_service.t -> @@ -62,6 +68,12 @@ val register0 : ('q -> 'i -> 'o tzresult Lwt.t) -> unit directory +val register0_chunked : + unit directory -> + ('m, unit, unit, 'q, 'i, 'o) RPC_service.t -> + ('q -> 'i -> 'o tzresult Lwt.t) -> + unit directory + val register1 : 'prefix directory -> ('m, 'prefix, unit * 'a, 'q, 'i, 'o) RPC_service.t -> diff --git a/src/lib_rpc_http/media_type.ml b/src/lib_rpc_http/media_type.ml index 4a00501cd1a42d8df5d1485296f3b9dff2254f36..325d8cddc66184278f21b89f15b002805d618967 100644 --- a/src/lib_rpc_http/media_type.ml +++ b/src/lib_rpc_http/media_type.ml @@ -25,6 +25,9 @@ include Resto_cohttp.Media_type.Make (RPC_encoding) +(* emits chunks of size approx chunk_size_hint but occasionally a bit bigger *) +let chunk_size_hint = 4096 + let json = { name = Cohttp.Accept.MediaType ("application", "json"); @@ -47,7 +50,7 @@ let json = @@ Data_encoding.Json.construct enc v); construct_seq = (fun enc v -> - let buffer = Bytes.create 4096 in + let buffer = Bytes.create chunk_size_hint in Data_encoding.Json.blit_instructions_seq_of_jsonm_lexeme_seq ~newline:true ~buffer @@ -68,6 +71,10 @@ let json = } let bson = + let construct enc v = + Bytes.unsafe_to_string @@ Json_repr_bson.bson_to_bytes + @@ Data_encoding.Bson.construct enc v + in { name = Cohttp.Accept.MediaType ("application", "bson"); q = Some 100; @@ -89,16 +96,11 @@ let bson = bson in Data_encoding.Json.pp ppf json); - construct = - (fun enc v -> - Bytes.unsafe_to_string @@ Json_repr_bson.bson_to_bytes - @@ Data_encoding.Bson.construct enc v); + construct; construct_seq = (fun enc v -> - let bytes = - Json_repr_bson.bson_to_bytes @@ Data_encoding.Bson.construct enc v - in - Seq.return (bytes, 0, Bytes.length bytes)); + let s = construct enc v in + Seq.return (Bytes.unsafe_of_string s, 0, String.length s)); destruct = (fun enc body -> match @@ -120,6 +122,9 @@ let bson = } let octet_stream = + let construct enc v = + Bytes.to_string @@ Data_encoding.Binary.to_bytes_exn enc v + in { name = Cohttp.Accept.MediaType ("application", "octet-stream"); q = Some 200; @@ -138,11 +143,11 @@ let octet_stream = ";; binary equivalent of the following json@.%a" Data_encoding.Json.pp (Data_encoding.Json.construct enc v)); - construct = (fun enc v -> Data_encoding.Binary.to_string_exn enc v); + construct; construct_seq = (fun enc v -> - let bytes = Data_encoding.Binary.to_bytes_exn enc v in - Seq.return (bytes, 0, Bytes.length bytes)); + let s = construct enc v in + Seq.return (Bytes.unsafe_of_string s, 0, String.length s)); destruct = (fun enc s -> match Data_encoding.Binary.of_bytes enc (Bytes.of_string s) with