From 6e7fb8ddd9047853f048cb7c6e5e5a6b4fccd096 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rapha=C3=ABl=20Cauderlier?= Date: Wed, 2 Dec 2020 11:01:21 +0100 Subject: [PATCH] Doc/Michelson: document a Michelson extension for writing unit tests --- docs/alpha/michelson.rst | 494 ++++++++++++++++++++++++++++++++++++ docs/nairobi/michelson.rst | 502 +++++++++++++++++++++++++++++++++++++ 2 files changed, 996 insertions(+) diff --git a/docs/alpha/michelson.rst b/docs/alpha/michelson.rst index 8de7c1472e56..7415b3ba2006 100644 --- a/docs/alpha/michelson.rst +++ b/docs/alpha/michelson.rst @@ -796,6 +796,8 @@ parameters require sequences in the concrete syntax. IF { instr1_true ; instr2_true ; ... } { instr1_false ; instr2_false ; ... } +.. _syntax_of_scripts_alpha: + Main program structure ~~~~~~~~~~~~~~~~~~~~~~ @@ -1980,3 +1982,495 @@ The language is implemented in OCaml as follows: function is very simple, what we have to check is that we transform a ``Prim ("If", ...)`` into an ``If``, a ``Prim ("Dup", ...)`` into a ``Dup``, etc. + +.. michelson_tzt_alpha: + +TZT, a Syntax extension for writing unit tests +---------------------------------------------- + +This section describes the TZT format, an extension of the Michelson +language allowing to run Michelson unit tests at a finer level than a +full smart contract script. This extension adds syntax to specify an +instruction (or sequence of instructions) to test, a concrete input +stack and the expected output stack. + +These unit tests can be useful for both smart contract developers who +need to independently test various parts of the smart contracts they +develop and to the developers of new implementations of the Michelson +interpreter who need to check that their new implementations behave as +the reference implementation by passing `a conformance test suite +`__. + +Similarly to Michelson scripts, the concrete syntax of TZT unit tests +is :doc:`../shell/micheline`. + +TZT unit test files usually have the extension ``.tzt``. A unit test +file describes a single unit test. It consists of a Micheline sequence +of primitive applications (see :doc:`../shell/micheline`), in no particular order. This is +:ref:`similar to Michelson scripts ` but +the set of primitives allowed at the toplevel differ; in Michelson +scripts, the allowed toplevel primitives are ``parameter`` +(mandatory), ``storage`` (mandatory), ``code`` (mandatory), and +``view`` (optional and repeated). For TZT unit tests, the toplevel +primitives which can be used are: + + - ``input``, + - ``code``, + - ``output``, + - ``now``, + - ``sender``, + - ``source``, + - ``chain_id``, + - ``self``, + - ``parameter``, + - ``amount``, + - ``balance``, + - ``other_contracts``, and + - ``big_maps``. + +Mandatory primitives +~~~~~~~~~~~~~~~~~~~~ + +Each of the mandatory primitives ``input``, ``code``, and ``output`` +must occur exactly once in a unit test file in no particular order. + +The ``input`` primitive is used to declare the input stack (see the +:ref:`syntax of concrete stacks `). + +The ``code`` primitive is used to declare the instruction or sequence +of instructions to execute. + +The ``output`` primitive is used to declare if the execution is +expected to succeed or fail and what result is expected from the +execution. For executions expected to succeed, the argument of the +``output`` primitive is simply the expected output stack (see the +:ref:`syntax of errors `). For executions +expected to fail, the argument is the expected error. In both cases, +the :ref:`wildcard pattern ` can +be used to omit part of the expected output. + +The simplest test which can be written asserts that executing no +instruction on the empty stack successfully returns the empty stack: + +:: + + input {}; + code {}; + output {} + +Here is a slightly more involved test which demonstrates the effect of the `SWAP +`__ instruction: + +:: + + input + { + Stack_elt nat 8 ; + Stack_elt bool False + }; + code SWAP; + output + { + Stack_elt bool False ; + Stack_elt nat 8 + } + +It is possible to test the effect of several instructions by wrapping them in a sequence: + +:: + + input + { + Stack_elt nat 8 ; + Stack_elt bool False + }; + code { SWAP ; SWAP }; + output + { + Stack_elt nat 8 ; + Stack_elt bool False + } + +Here is an example showing how to test the ``FAILWITH`` instruction: + +:: + + input {Stack_elt nat 2}; + code FAILWITH; + output (Failed 2) + +Optional primitives +~~~~~~~~~~~~~~~~~~~ + +Optional primitives are used to set the execution context for the +test. Each of the optional primitives can be used at most once, in no +particular order. + + - ``amount`` (optional, defaults to 0): the amount, expressed in + mutez, that should be pushed by the `AMOUNT + `__ + instruction + + - ``balance`` (optional, defaults to 0): the balance, expressed in + mutez, that should be pushed by the `BALANCE + `__ + instruction + + - ``now`` (optional, defaults to ``"1970-01-01T00:00:00Z"``): the + timestamp that should be pushed by the `NOW + `__ + instruction + + - ``sender`` (optional, defaults to + ``"tz1KqTpEZ7Yob7QbPE4Hy4Wo8fHG8LhKxZSx"``): the sender address + that should be pushed by the `SENDER + `__ + instruction + + - ``source`` (optional, defaults to + ``"tz1KqTpEZ7Yob7QbPE4Hy4Wo8fHG8LhKxZSx"``): the source address + that should be pushed by the `SOURCE + `__ + instruction + + - ``chain_id`` (optional, defaults to ``"NetXdQprcVkpaWU"``): the + chain identifier that should be pushed by the `CHAIN_ID + `__ + instruction + + - ``self`` (optional, defaults to + ``"KT1BEqzn5Wx8uJrZNvuS9DVHmLvG9td3fDLi"``): the address that + should be pushed by the `SELF + `__ and + `SELF_ADDRESS + `__ + instructions + + - ``parameter`` (optional, defaults to ``unit``): the type of the + parameter of the contract pushed by the `SELF + `__ + instruction + + - ``other_contracts`` (optional, defaults to ``{}``): mapping between + the contract addresses that are assumed to exist and their + parameter types (see the :ref:`syntax of other contracts + specifications `) + + - ``big_maps`` (optional, defaults to ``{}``): mapping between + integers representing ``big_map`` indices and descriptions of big + maps (see the :ref:`syntax of extra big maps specifications + `) + +The following test example asserts that the default value for the `NOW +`__ +instruction is the unix epoch: + +:: + + input {}; + code NOW; + output { Stack_elt timestamp "1970-01-01T00:00:00Z" } + +The following example shows how to use the ``now`` toplevel primitive +to make the `NOW +`__ +instruction return a chosen timestamp: + +:: + + input {}; + now "2020-01-08T07:13:51Z"; + code NOW; + output { Stack_elt timestamp "2020-01-08T07:13:51Z" } + +.. _syntax_of_concrete_stacks_alpha: + +Syntax of concrete stacks +~~~~~~~~~~~~~~~~~~~~~~~~~ + +A concrete stack is written as a Micheline sequence whose elements are +of the form ``Stack_elt `` where ```` is a Michelson value +and ```` is its type. For example, ``{ Stack_elt bool True ; +Stack_elt nat 42 }`` is a concrete stack of length 2 whose top element +is the boolean ``True`` and the bottom element is the natural number +``42``. + +.. _omitting_parts_of_the_output_alpha: + +Omitting parts of the output +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Any part of the ``output`` specification can be replaced with the +wildcard pattern ``_``. + +For example, let's consider the following test of the ``PAIR`` instruction: + +:: + + input {Stack_elt bool True; Stack_elt string "foo"}; + code PAIR; + output {Stack_elt (pair bool string) (Pair True "foo")} + +Omitting the ``True`` argument to the ``Pair`` primitive can be done as follows: + +:: + + input {Stack_elt bool True; Stack_elt string "foo"}; + code PAIR; + output {Stack_elt (pair bool string) (Pair _ "foo")} + +Omitting the ``Pair`` primitive: + +:: + + input {Stack_elt bool True; Stack_elt string "foo"}; + code PAIR; + output {Stack_elt (pair bool string) (_ True "foo")} + +Omitting the ``pair bool string`` type: + +:: + + input {Stack_elt bool True; Stack_elt string "foo"}; + code PAIR; + output {Stack_elt _ (Pair True "foo")} + +Omitting the resulting stack element: + +:: + + input {Stack_elt bool True; Stack_elt string "foo"}; + code PAIR; + output {_} + +Omitting all of the output: + +:: + + input {Stack_elt bool True; Stack_elt string "foo"}; + code PAIR; + output _ + +The difference between the last two examples is that ``output {_}`` +means that the instruction is expected to successfully return a stack +of length 1 while ``output _`` means that nothing in particular is +expected from the execution of the instruction, not even being +successful. + +The wildcard pattern is typically used to omit unspecified aspects of +the Michelson language when writing portable tests; in particular the +cryptographic nonces in values of type ``operation`` (see the +:ref:`syntax of concrete operations +`) or implementation-specific +parts of error outputs (see the :ref:`syntax of errors +`). + +.. _output_normalization_alpha: + +Output normalization +~~~~~~~~~~~~~~~~~~~~ + +The input and output stacks can use the readable and optimized formats +for Michelson values and even mix the formats; for a test to pass, the +expected output does not need to syntactically match the result of the +execution but only to match up to conversion between optimized and +readable formats; the TZT test runner is responsible for normalizing +the actual output and the expected one to common format. This means in +particular that conversion between readable and optimized formats can +be tested by using ``{}`` as the ``code`` instruction sequence to +test; for example these two tests pass: + +:: + + input {Stack_elt address 0x0000e7670f32038107a59a2b9cfefae36ea21f5aa63c}; + code {}; + output {Stack_elt address "tz1gjaF81ZRRvdzjobyfVNsAeSC6PScjfQwN"} + +:: + + input {Stack_elt address "tz1gjaF81ZRRvdzjobyfVNsAeSC6PScjfQwN"}; + code {}; + output {Stack_elt address 0x0000e7670f32038107a59a2b9cfefae36ea21f5aa63c} + +This normalization feature is however incompatible with using the +:ref:`wildcard pattern ` in the +output; when using wildcards the output must be formatted using the +readable format so the following test does not pass: + +:: + + input {Stack_elt address "tz1gjaF81ZRRvdzjobyfVNsAeSC6PScjfQwN"}; + code {}; + output {Stack_elt _ 0x0000e7670f32038107a59a2b9cfefae36ea21f5aa63c} + +but the following test does pass: + +:: + + input {Stack_elt address 0x0000e7670f32038107a59a2b9cfefae36ea21f5aa63c}; + code {}; + output {Stack_elt _ "tz1gjaF81ZRRvdzjobyfVNsAeSC6PScjfQwN"} + +.. _syntax_of_errors: +.. _syntax_of_errors_alpha: + +Syntax of errors +~~~~~~~~~~~~~~~~ + +To test that the execution of an instruction fails, the following +syntaxes can be used instead of the output stack as the argument of the +``output`` toplevel primitive to specify which error the instruction is expected to +raise: + + - ``(StaticError )``: an error occurred before the + instruction was executed; the error description format is + unspecified so consider using a :ref:`wildcard + ` such as ``(StaticError _)`` + to write portable tests; + + - ``(Failed )``: the execution reached a ``FAILWITH`` + instruction and the topmost element of the stack at this point was + ````; + + - ``MutezOverflow``: an addition or multiplication on type ``mutez`` + produced a result which was too large to be represented as a value + of type ``mutez``; + + - ``MutezUnderflow``: a mutez subtraction resulted in a negative + value. This should only happen in the case of the deprecated + ``mutez`` case of the ``SUB`` instruction; + + - ``GeneralOverflow``: the number of bits to shift using the ``LSL`` + or ``LSR`` instruction was too large; + + +The following example shows how to test a runtime failure; it asserts +that the `FAILWITH +`__ +instruction produces a runtime error containing the top of the stack. + +:: + + input { Stack_elt nat 4 ; Stack_elt bytes 0x }; + code FAILWITH; + output (Failed 4) + +The following example shows how to test type checking failure; it +asserts that the `DUP +`__ +instruction cannot be used on an empty stack. + +:: + + input {}; + code DUP; + output (StaticError _) + +The following example shows another kind of static failure: a string +cannot be passed as argument to the `DUP +`__ +instruction. + +:: + + input { Stack_elt nat 8 }; + code { DUP "foo" }; + output (StaticError _) + +.. _syntax_of_concrete_operations_alpha: + +Syntax of concrete operations +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The `operation type +`__ has +no concrete syntax in Michelson. In order to specify the result of the +operation forging instructions `TRANSFER_TOKENS +`__, +`CREATE_CONTRACT +`__, +and `SET_DELEGATE +`__ , +the following data constructors are added: + + - ``Transfer_tokens``, + - ``Create_contract``, and + - ``Set_delegate``. + +They take as arguments the inputs of the corresponding operation +forging instructions plus a cryptographic nonce represented as a byte +sequence. The result of ``TRANSFER_TOKENS``, ``CREATE_CONTRACT``, +and ``SET_DELEGATE`` have respectively the following shapes: + + - ``Transfer_tokens
``, + - ``Create_contract {