Nomadic Labs
Nomadic Labs
The Protocol: from High-level Command Line to Low-level Operations

Understanding the source code of Tezos may take much time for fresh contributors. This gentle note gives a global presentation of the control flow of a simple transaction example, going from the high-level command line call to the low-level account operations.

This note explains and illustrates flow of control in Tezos using the example of carrying out a simple transaction. We will go from the high-level command line call to the low-level account operations. To guide you through the codebase, we give line numbers based on release 8.1 (commit 6dbc4247).

Where do I start?

Our scenario. Imagine that Alice and Bob have one account each, and Alice wants to send ꜩ10 from her account to Bob’s. Alice can proceed by using a transfer operation. This transaction will trigger some additional transactions, which will be handled automatically by the system:

  1. Alice must pay baking fees (tokens paid to the baker who writes Alice’s main transfer onto the blockchain).
  2. Alice may also have to pay for key revelation to reveal the public key of her account.1

Here’s a picture:

The easiest way to execute our example is to run a node locally by using the sandboxed mode. In the terminal, we just type:

$ tezos-client transfer 10 from alice to bob

Inside the code

As far as the Tezos codebase is concerned, everything is a contract. This includes user-owned accounts (called implicit accounts in the codebase) and smart contracts (called originated accounts in the codebase). This is reflected in the variable and function names in the code cited below, so for consistency we may also call everything a “contract” — but note that in our example, the source and destination contracts are actually the user-owned (i.e., implicit) accounts of Alice and Bob.

Step 1: Dispatching the client command

  • The flow of control starts with the commands function, whose code is in client_proto_context_commands.ml (l.254). This determines the command-line syntax for the switches following an invocation of ‘tezos-client’.2 In our example, we have invoked the transfer sub-command (l.893).

  • Control now flows to transfer_command (l.110), which distinguishes the type of the source contract (in the pattern-matched variable sourcel.136) — in our case it is implicit and admits a public key hash. Flow of control passes to another function, transfer (l.167).

  • transfer is in client_proto_context.ml (l.73). Its job is to build the transaction operation itself, using a function build_transaction_operation. In our case, the operation is a GADT Transaction of type manager_operation (discussed below). In particular, its field amount contains the amount of tez to be transferred (excluding baking fees). transfer wraps the operation in an annotated_manager_operation by function prepare_manager_operation, adding fee and gas information; then it further wraps the operation into the GADT Injection.Single_manager of type annotated_manager_operation_list; and finally it passes this all on to function inject_manager_operation, detailed below.

Manager operations are operations that compete between themselves for inclusion in a block. This is in contrast to other types of operations such as consensus or governance related operations. The competition is realized through the proposed fees, which go to the baker selecting the operations to be included in the block. There are four types of manager operations, defined by the type manager_operation in operation_repr.ml using the following four constructors:

  1. Reveal for the revelation of a public key, a one-time prerequisite to any signed operation, in order to be able to check the sender’s signature.
  2. Transaction of some amount to some destination contract.
  3. Origination of a contract using a smart-contract script and intially credited with the amount credit.
  4. Delegation to some staking contract (designated by its public key hash).

Although we usually use tezos-client to inject a single operation, the economic protocol use a built-in notion of a list of operations (also called “packed operation”) that can be injected as a whole, for efficiency reasons. In this case the constructor Injection.Cons_manager, instead of Injection.Single_manager, would be used to build a value of type annotated_manager_operation_list.

Step 2: Injecting the operation

  • The function inject_manager_operation in injection.ml (l.911) proceeds, from the previous list of annotated manager operations (of type annotated_manager_operation_list), by creating a list of contents (of type contents_list) where each content (of type contents) is a GADT Manager_operation. This mapping is performed by the local function build_contents, and for each element by the local function contents_of_manager. These functions deconstruct and reconstruct the list of annotated manager operations, providing information for the missing values (fee, gas limit, storage limit).

    Then, function inject_manager_operation proceeds according to two cases:

    1. If Alice’s public key has not yet been revealed, then the function adds one more manager operation to reveal her public key.
    2. If Alice’s public key has been revealed, then the next function is directly called with this list of contents, which is the case in our example.
  • The function inject_operation (l.773) completes the final steps of injecting into the node. It:

    • computes estimated gas and storage (in function may_patch_limits),
    • checks compliance with cap fees (in function may_patch_limits),
    • performs a simulation (by calling preapply), and finally
    • injects the operation (by calling Shell_services.Injection.operation in l.825).

Step 3: Dispatching the operation

The calls to Alpha_block_services.Helpers.Preapply.operations in preapply for simulation and to Shell_services.Injection.operation for injection from Step 2 actually represent two RPC calls from the client to the node. Such RPCs are declared in src/lib_shell_services and implemented in src/lib_shell/ (in files with the name of the form *_directory.ml). To serve these two RPCs, the shell part of the node simply dispatches the operation execution to the relevant economic protocol, here Alpha.

Step 4: Applying the operation in the economic protocol

  • The main entrypoint to apply the operation which we injected in the previous section is the function apply_operation in src/proto_alpha/lib_protocol/main.ml (l.180). A variable operation (of type 'kind operation') containing all information for the operation itself is passed to the next function.

The record-type 'kind operation defined in file operation_repr.ml (l.62) contains a field protocol_data of type 'kind protocol_data (l.67). It wraps together a list of contents (of type contents_list) and a signature of the source contract for authentication purposes.

  • Next, the function apply_operation in src/proto_alpha/lib_protocol/apply.ml (l.1339) is called, which after some initialization, uses operation.protocol_data.contents (of type contents_list) to call the next function.
  • In the function apply_contents_list (l.1103), two function calls are worth mentioning:
    1. On one side (left in the figure), the function precheck_manager_contents_list (l.1327), which in turn calls the function precheck_manager_contents (l.928), and itself will call Contract.spend will trigger the payment of baking fees (l.833).
    2. On the other side (right in the figure), the function apply_manager_contents_list (l.1331) makes successive nested calls to apply_manager_contents_list_rec (l.987), then apply_manager_contents (l.836), and finally apply_manager_operation_content (l.518). Finally, the amount of ꜩ10 is debited from Alice when calling Contract.spend (l.552) and then credited to Bob when calling Contract.credit (l.570).

Summary

To show how operations are handled in Tezos, we started from the command-line level using tezos-client to trigger a token transfer between two accounts. This client process occurs in the shell, outside of the procotol. The command itself is parsed and a manager operation is prepared. This operation is further wrapped up as an annotated manager operation in a single-item list of the one operation.

Furthermore, to prepare for the injection into the economic protocol, this list of annotated manager operations is transformed into a list of contents. A content is a wrapper for various operations, one of them is the manager operation. Finally, the operation is injected in injection.ml.

On the economic protocol side, the operation has been fetched, consisting of a signature and a protocol data, wrapped together with a shell header. This value is then sent to apply.ml which is in charge of calling the final low-level operations for funds debit/credit.


  1. See this short tutorial (search for “first a revelation”). By default (to save space, and to provide a little additional security) only hashes of public keys are recorded on the blockchain. But in order for Alice to sign a transaction from her account to Bob’s, Alice has to pay a one-time cost — ꜩ0.001259, in the example linked to in the tutorial above — for the full public key of her account to be recorded on the blockchain as a special key revelation operation. 

  2. You can fetch a list of them at the command line with tezos-client man.
    We use here a bespoke command-line argument parser developed in Nomadic Labs called Clic. Other parts of the codebase use other parsers, including Arg, and Cmdliner (used in tezos-node). 


Smarter contracts thanks to Delphi (part 1/2)

Delphi is the successor to the Carthage protocol. Delphi’s main difference from Carthage is that gas costs are lower, so that smart contracts can compute more before hitting the Delphi/Carthage per-operation gas limit of 1,040,000 gas units (gu). In this post we quantify the difference that Delphi’s lower gas costs will make: We start with a description and justification of the Michelson gas model; and then we showcase the expected gains for some smart contracts chosen to illustrate the...

Read More
The case of mixed forks in Emmy+

Note: This analysis was done with the help of Bruno Blanchet (Inria). The interested reader can experiment with our code used in the analysis. As in the previous analysis, we do not present any security proofs. This is the fourth in a series of posts on Emmy+: After our initial analysis, recently revisited and extended to the partial synchronous network model, we now consider so-called “mixed forks”. So far, we assumed that malicious bakers wanted to undo a transaction. In this post, we consider instead...

Read More
Dexter: Decentralized exchange for Tezos, formal verification work by Nomadic Labs

The Dexter smart contract is the cornerstone of the Dexter. We outline a formal verification of its functional specification, in Coq.

On September 30th, camlCase released Dexter. Dexter is a smart contract empowering decentralized exchange, performing the same function for tez as Uniswap on Ethereum does for ether; it enables trade between tez and any other token implemented by an FA1.2 contract. To this day, the following efforts have been undertaken to ensure Dexter’s quality, including: a security audit by Trail of Bits, Read More


Emmy+ in the partial synchrony model

We’d like to expand on our previous blog post analysing Emmy+. Note: Thanks to input from Bruno Blanchet (Inria). The interested reader can experiment with our code used in the analysis. As in the previous analysis, we do not present any security proofs. To recap Emmy+ is the new Tezos consensus algorithm, adopted in October 2019. Emmy+ improved on the original Emmy (see our post on Emmy+: an improved consensus algorithm).1 In our previous analysis...

Read More
On “Defending Against Malicious Reorgs in Tezos Proof-of-Stake”

Note: We would like to acknowledge Bruno Blanchet (Inria) for his feedback. The interested reader can experiment with our code used in the analysis. We are happy to note a new paper on Emmy+: “Defending Against Malicious Reorgs in Tezos Proof-of-Stake” by Michael Neuder, Daniel J. Moroz, Rithvik Rao, and David C. Parkes in the ACM Advances in Financial Technologies 2020 conference. We are delighted that Tezos and Emmy+ are stimulating independent research activity, and we hope to see much...

Read More
Measuring test coverage

An in-depth look on how we measure test coverage of the OCaml implementation of Tezos.

As we have discussed earlier on this blog, notably in the post on regression testing, testing is an important complement to formal verification. A critical task when testing is to ensure a high degree on test coverage. In this post we discuss how we measure test coverage of the OCaml implementation of tezos using bisect_ppx, and our work towards ensuring that the Michelson interpreter of the node is fully covered by tests. Test coverage Testing is simpler to set up than formal verification but...

Read More
Catching sneaky regressions with pytest-regtest

An in-depth look on how we use regression testing to catch bugs in Tezos.

Testing is an important complement to formal methods that we use through out Tezos to ensure software quality. In this blog post we discuss how we use regression testing, through the pytest-regtest tool. Regression testing Regression testing is a coarse-grained testing method for detecting unintended changes in the behavior of the system under test. We have applied regression testing to the tezos-client, notably to smart-contract type checking and execution. Globally, regression testing consists of two components. First, a way of running and storing the...

Read More
How to write a Tezos protocol - part 2

This is the second post of a tutorial series on how to implement a Tezos protocol. In the first post, we saw how to write, compile, register, activate and use an extremely simple protocol. We also looked at the interface between the protocol and the shell. In this post, we consider a new protocol called demo_counter which extends demo_noops from the first post in several ways. Blocks can contain simple operations, whose effects update the blockchain state. It is parameterized by protocol parameters passed at activation time. It defines...

Read More
Formally Verifying a Critical Smart Contract

We present the formal verification of the Spending Limit Contract, a critical component of the Cortez wallet.

One of the main goals of Nomadic Labs is the development and applications of formal methods in the domain of distributed software, blockchains and smart contracts. In particular for the Tezos blockchain, for which we also develop the Cortez smartphone wallet (Android, iPhone). This wallet helps Tezos users manage their account and funds in a safe and secure manner. How can the user be...

Read More
  • 1
  • 2