A summary of Nomadic Labs activities in the first quarter of 2021

Welcome to our meanwhile series, the ongoing story of Nomadic Labs’ amazing adventures in the Tezos blockchain space. This post is a recap of our activities in the first quarter of 2021, following on from our 2020 recap. As always, you can find out more about us here:

So here’s what we’ve been up to these past three months:

Edo protocol upgrade and Florence protocol proposal

The Tezos blockchain contains a self-amendment mechanism to upgrade the protocol by community vote, meaning: no need for hard forks, and in-built agility and ability to adopt new ideas in the fast-evolving blockchain space. We intend to follow a regular protocol upgrade schedule.

The recent Edo protocol upgrade on 13 February 2020 went smoothly (block height 1,398,551; cycle 341; changelog).1 Edo introduced several substantive new features to Tezos:

Associated to the Edo protocol upgrade is also a new major release of tezos-node that contains an update to the protocol environment2, numbered “Version 1”. This is significant because until now, all protocols have used “Version 0”.

Together with Marigold, Tarides, DaiLambda, and Keefer Taylor, we proposed a successor protocol upgrade, Florence. See

One standout feature of Florence is a new arithmetic system (based on saturation arithmetic) for computing gas costs in Michelson smart contracts. Our benchmarks indicate a tenfold speedup of gas computation, and a 35% speedup of the execution cycle of the smart contract Michelson interpreter in Florence overall.3 So smart contracts in Florence can be smarter, for the same gas.4

Another notable feature is a migration from BFS to DFS. See also:

The main developer of this feature is ChiaChi Tsai from Marigold. Nomadic Labs’ participation in the BFS to DFS migration was in the design (especially security considerations), to review several versions of the code, and to perform a major replay test.5

Easier, safer, better installation of the Tezos codebase

The “How to get Tezos” installation instructions are now automatically checked as part of the build process itself, meaning they are automatically tested and included in documentation and should stay correct and up-to-date even as they depend on an extensive environment in constant evolution, due to

• development of Tezos itself (e.g. switching to new protocols, releasing new versions of the platform, adding dependencies), and
• evolution of third-party software packages (e.g. the OPAM package manager for OCaml, individual OCaml packages, Linux releases, and so forth).

Technically, this was accomplished by writing a library of executable scripts for each installation scenario (binaries, docker images, compiling from source, …) which are executed in the CI (continuous integration) process itself, and automatically copied over each time documentation is generated and published.6

This new system means

• early and automatic detection and quick correction of installation problems, and
• no more copy/paste errors or stale install scripts in documentation

— thus making installation more reliable and convenient for all Tezos users, from neophytes to experienced developers.

In summary: the Tezos installation scripts and relevant documentation are now part of the testable codebase of Tezos itself.

Culture and growth

Since January 2021 we are delighted to have been joined by three new hires and three interns, bringing our count of full-time employees to 62.

Announcing 1,000 days of Tezos mainnet

As of Friday 26 March 2021, the Tezos mainnet is 1,000 days old. See this subtle poster on Reddit:

1000 Days of Tezos Mainnet from r/tezos

Specifically, the chain was launched on June 30 2018, as per the timestamp of the genesis Tezos block.7

(The main Tezos network wasn’t called “Tezos Mainnet” at the time but “Tezos Betanet”. It was renamed on September 17, once devs were confident in its stability. Following the precedent of a famous singer, we might say that “The blockchain formerly known as Tezos Betanet” is now 1,000 days old.)

You can check the arithmetic in a Unix system by running

\$ date -d "June 30 2018 + 1000 days"
Fri 26 Mar 00:00:00 GMT 2021


Dexter

Dexter is a smart contract to enable trade between tez and any FA1.2-compliant token (dapp; doc; tutorials). Think: “Uniswap for Tezos”.

Examples of smart contract implementations satisfying the FA1.2 interface include:

Thus using Dexter, a user can exchange tez for ETHtz, USDtz, and tzBTC — all on the Tezos blockchain.9

Nomadic Labs verified that the Dexter implementation conforms to the Dexter specification — this is called verifying the functional specification — using the Coq proof assistant with the Mi-Cho-Coq framework. This was in addition to a security audit by Trail of Bits and property-based testing by camlCase.

However, we discovered in late February while working on the Florence upgrade proposal that the Dexter specification itself contained an error.

Just because something is a specification does not make it right: specifications can have mistakes just like anything else (indeed we commented on this in the initial blog post). This is why responsible ecosystems like Tezos subject complex systems like Dexter to multiple overlapping verification efforts.10 So this is just another day in The Real World.

We reported the error and a “White Knight” operation was used to remove funds from the contract — using the error itself, by the way — and to return funds to their owners.

A rewrite of Dexter is under development in a collaboration between Nomadic Labs and LIGO (see this GitLab repo). We at Nomadic Labs are carrying out a formal verification of it. So far, we’ve finished the verification of a functional specification, which brings confidence up to the level of the previous version of Dexter. Obviously we should go further, and the way to do this is to verify high-level properties of the new specification, to check that no further errors exist like the one discovered in the previous version.

In the meantime, and to avoid delays for the existing users of Dexter, the Dexter contract has been patched (patch source code) to fix the flaw, and brought back online.

Umami

Our Wallet team has been diligently at work on the new Umami wallet. Umami is a cryptocurrency wallet for Tezos giving both beginner users and power users convenient access to all features available within the Tezos protocol including: multiple accounts, tokens, batch transactions, and delegation — and eventually, though not in the initial beta: contracts and use of hardware wallets.

Forthcoming switch from Emmy+ to Emmy★ and then Tenderbake

We plan to upgrade our consensus algorithm from the current Emmy+ to Emmy, and shortly thereafter to Tenderbake.

Emmy+ is a Nakamoto-style consensus algorithm. This means that it is similar to the Bitcoin consensus algorithm, just adapted to Tezos’ proof-of-stake system rather than the proof-of-work system used by Bitcoin. Emmy refines the Emmy+ system in two ways (listed in decreasing order of significance):

1. Emmy provides a special fast consensus path for when the network is operating normally, which is most of the time. This makes Emmy faster than Emmy+ when things are going well — and no slower when they’re not.
2. Emmy increases the number of endorsement slots from 32 to 256. This is a technical tweak designed to increase stability and participation.

How does Emmy fare at scale in a test that approximates a real-live system? This is what resilience testing is about. TQTezos, with support from Nomadic Labs, has constructed a resilience test network framework based on Kubernetes which allows us to quickly deploy a large testnet on AWS. It takes about 30 minutes to deploy a 400 node private network and start baking on it.11

After the upgrade to Emmy there will follow an upgrade to Tenderbake. Tenderbake belongs to the BFT-style family, so the switch from the Nakamoto-style to the BFT-style is a big deal. We discuss this in detail in a blog post looking ahead to Tenderbake. In summary:

1. Tenderbake offers deterministic finality, with finality time of one minute assuming good network behaviour. This means that (assuming the network is stable and not under attack) a block becomes final in one minute (i.e. the transaction settlement time is one minute).
2. Tenderbake has no forks. If the network degrades, the Tenderbake consensus algorithm waits until connectivity is restored.12

NL research seminars

Our series of Nomadic Labs research seminars has continued at a regular pace:

1. Practical proofs using Juvix (27 October 2020)
2. Verifying smart contracts using Mi-Cho-Coq (10 November 2020)
3. Efficient data storage on the blockchain using Plebeia (24 November 2020)
4. Adding multicore programming to OCaml (08 December 2020)
5. zkChannels in Tezos (05 January 2021)
6. Towards mechanised verification of the LIGO compiler (20 January 2021)
7. SmartPy: the inner workings (02 February 2021)
8. Bringing K Powered Blockchain Security to Tezos (16 February 2021)
9. Implementing Checker, a Robocoin Mechanism for Tezos (02 March 2021)
10. High-level smart contract design & verification with Archetype (16 March 2021)

The Tezos Foundation was a platinum sponsor of POPL 2021 in January 2021 (and of POPL 2020 and POPL 2019), and Nomadic Labs sponsored the colocated CPP 2021 (Conference on Certified Programs and Proofs) (and CPP 2020). Our engineers had a strong presence at these events, including:

You can read our full POPL 2021 retrospective here.

À la prochaine

So that’s it! The first three months of 2021 have been eventful and productive, and the next three months surely will be too. Thanks for reading, and do check in again next quarter for the next Meanwhile.

1. The previous protocol upgrade was Delphi on 12 November 2020 (block height 1,212,417; cycle 296; changelog; significance of the upgrade).

2. The protocol environment is a library of cryptographic primitives and other useful functions (packaged as an OCaml module).

3. The term execution cycle in the context of gas costing is the gas cost of decoding instructions, dispatching them, and of gas monitoring itself. So ‘execution cycle’ does not include the cost of actually executing instructions; it is the cost of arranging for instructions to execute …

4. … thus, a theoretical smart contract in Florence, consisting of instructions that do zero work and cost zero gas, can do this nothing up to 35% faster (and for $$1/1.35$$ of the gas) than it would in Edo!

5. A replay test is when chain history is replayed using the newer protocol, to check for breaking changes and to check that the functionality of any existing live smart contracts is not affected. See also the blog post; search for “Replays of on-chain history”.

6. Contrast this with paper-only scripts, which exist in the documentation but must be manually tested and copy/pasted.

7. The genesis block of a blockchain is its first block. It is numbered 0 (not 1) because programmers and computer scientists start counting at zero: thus zero is the first number, one is the second, and so on.

8. Lugh is an Irish deity associated with craftsmanship and skill, roughly corresponding to Mercury in Roman mythology and Apollo in Greek mythology.

9. Here’s how it works: tez is the primitive token of the Tezos blockchain. Tezos has no other primitive tokens. However, Tezos does have smart contracts, which gives huge flexibility, and in particular ETHtz, USDtz, and tzBTC are smart contracts on the Tezos blockchain which implement ledgers giving the effect of what we will call non-primitive tokens in this footnote — e.g. they include ledger-like entrypoints such as %transfer, %getBalance, and %getTotalSupply.

The FA1.2 standard is a precise specification which smart contracts intending to implement non-primitive tokens, can satisfy. Then Dexter is a smart contract which implements functionality to convert between tez and any non-primitive token, provided that the smart contract implementing the non-primitive token satisfies the FA1.2 specification.

10. This means that yes, sometimes more work is required so that features ship later than we hoped. That’s not a bug, that’s a feature. And it’s not unique to blockchain. This is what it’s like to work with any complex system, be it a bank, an aircraft design, or getting your child into bed.

11. Think: “easy test flights, for software”. You can fire up a large test system and watch it run as you tweak parameters, play with network properties, and so check the real-world conditions in which the system performs well as an engineering structure. The infrastructure toolchain is built on Helm, Kubernetes and Docker. You can also use Pulumi to automate your deployment into AWS EKS. For local deployments the toolchain utilises minikube, which enables comfortable set-up of a local network of up to 20 nodes (depending on available RAM).

The code is open-source and accessible via the tezos-k8s github repo. It is in active development, and the developers welcome external contributions in bug fixes, feature code, and requirements definition.

12. BFT-style algorithms are safe, but not live, whereas Nakamoto-style algorithms are live but not safe. This means that a BFT-style algorithm (like Tenderbake) will safely wait out periods of network degradation and continue once connectivity is restored; whereas a Nakamoto-style algorithm will remain live and fork during a period of network degradation, and the fork collapses once connectivity is restored.

13. Arvid Jakobsson, Colin González, Bruno Bernardo, and Raphaël Cauderlier. Formally Verified Decentralized Exchange with Mi-Cho-Coq. Contributed Lightning Talk to CPP 2021. Thanks also to Kristina Sojakova (INRIA) and James Haver (camlCase) for their contributions to the formalisation effort.

14. František Farka, Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, and Ignacio Fábregas. On Algebraic Abstractions for Concurrent Separation Logics. Proc. ACM Program. Lang. 5, POPL, Article 5 (January 2021), 32 pages. https://doi.org/10.1145/3434286

Sound and fast gas monitoring with saturation arithmetic

Fast calculation of gas costs using saturation arithmetic. With speed comes some theoretical loss of safety, but in practice it works well.

Sound and fast gas monitoring? Let’s use saturation arithmetic! Introduction: we got gas In Tezos, as with most smart contract platforms, on-chain operations cost gas — a theoretical resource intended to reflect (and so limit) the on-chain computational cost of running a smart contract. The gas model allocates gas costs to atomic computation steps. When a computation starts it receives some finite allocation of gas, from which the gas cost of each of its atomic computations is deducted...

Tezos calling convention migrating from Breadth-First to Depth-First Order (BFS to DFS)

Summary: If the Florence proposal is adopted, we recommend you do not deploy new Michelson contracts that are dependent on the BFS calling convention. We do not expect this to be a problem in practice. However, those planning on deploying contracts in the near term should check that their contract’s correctness is unaffected by the change in calling convention. The current calling convention for intercontract calls in Tezos is that they are added to a “first-in,...

Baking Accounts proposal contains unexpected breaking changes

Summary Ongoing testing and review of baking accounts has uncovered some important and previously undocumented breaking changes (see the section on breaking changes in the TZIP for Baking Accounts) in the baking account proposal. These issues are significant, and affect the functionality of both existing and future smart contracts; they are detailed below. Bakers should please these carefully when casting their vote. We believe Baking Accounts should be postponed until a thorough audit of functionality is...

Florence: Our Next Protocol Upgrade Proposal

Announcing Florence Proposal

UPDATE: We believe that the baking accounts implementation is significantly flawed. See: Baking Accounts proposal contains unexpected breaking changes This is a joint announcement from Nomadic Labs, Marigold, DaiLambda, and Tarides. As we described in this post, several development organizations in the Tezos ecosystem are now collaborating to submit protocol upgrade proposals every few months, which is the interval permitted by the Tezos on-chain governance process. When the Edo upgrade went live on February 13,...

A technical description of the Dexter flaw

In this technical blog post, we detail the flaw found in the Dexter contract and the exploit used to “white-knight” the funds in those contracts. Background The Dexter contract contains several entrypoints allowing users to perform various operations, such as adding and removing liquidity, or converting tokens to tez back and forth. The exact interface is given by the type of the contract’s parameter: parameter (or...

Dexter Flaw Discovered; Funds are Safe

TL;DR: A flaw was found in the camlCase’s Dexter contract. The funds have been removed from the contract and returned to their original holders. A high level explanation follows; technical details of the Dexter flaw will be described in a separate post to come. As many of you know, we have been working on a new Tezos upgrade proposal. This proposal, if accepted, will change the calling convention from breadth first ordering to depth first ordering. In...

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.2 (commit 6102c808). Where do I start? Our scenario. Imagine that Alice and Bob have one account each, and Alice wants to send ꜩ10 from her account...

Edo, the latest Tezos upgrade, is LIVE

This is a joint announcement from Nomadic Labs, Marigold, and DaiLambda. On 13 February 2021, the Tezos blockchain successfully upgraded by adopting Edo at block 1,343,489. Jointly developed by Nomadic Labs, Marigold, DaiLambda, and Metastate, Edo is the fifth Tezos upgrade in the span of two years, and follows the Delphi upgrade of three months ago. The Tezos blockchain currently allows protocol upgrades every several months, and we intend for the foreseeable future to take advantage of...