Meanwhile at Nomadic Labs #11

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:

Twitter @LabosNomades ~ Website ~ LinkedIn ~ Technical blog ~ GitLab repo

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

• Edo protocol upgrade and Florence protocol proposal
• Easier, safer, better installation of the Tezos codebase
• Culture and growth
• Announcing 1,000 days of Tezos mainnet
• Adoption and support
• Dexter
• Umami
• Forthcoming switch from Emmy⁺ to Emmy^★ and then Tenderbake
• NL research seminars
• Research and sponsorship
• À la prochaine

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).¹ Edo introduced several substantive new features to Tezos:

• Zcash Sapling integration (privacy-preserving transactions; see doc and an accessible explanation).
• Tickets (mechanism for smart contracts to authenticate data with respect to a Tezos address).
• An extended Voting procedure (adds a two-week “Adoption” phase).
• … and more. See also a detailed analysis of the Edo upgrade.

Associated to the Edo protocol upgrade is also a new major release of tezos-node that contains an update to the protocol environment², 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

• the detailed Florence changelog,
• an accessible discussion.

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.³ So smart contracts in Florence can be smarter, for the same gas.⁴

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

• The DFS Tezos Improvement Proposal (TZIP).
• A detailed discussion of the code design.

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.⁵

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.⁶

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.⁷

(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

Adoption and support

• Nomadic Labs has joined Infrachain, a Luxembourg-based European cross-industry effort to pool blockchain expertise and promote regulatory-compliant adoption. See the announcement (in English) and a short article in Paperjam (in French).

• We are pleased to welcome two new institutional bakers on the Tezos chain:

  • Wakam (a digital insurance and bespoke insurance creator) is now a Tezos baker (see the press release; also as a pdf).
  • The Blockchain Group (a blockchain service and technology group), through its subsidiary The Blockchain Xdev, is now a Tezos baker (see the press release).

• Nomadic Labs has helped to deploy Lugh (currency name EURL).⁸ Lugh is a Euro-backed digital asset, meaning that 1 EURL is always equal to 1€ (see press release). If you hold 1 EURL then this corresponds to 1€ in the balance of a certain bank account at Société Générale. Lugh has been reviewed by a “big four” firm (PriceWaterhouseCoopers). See also this short video introducing Lugh, and the Lugh LinkedIn page.

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:

1. The ETH-wrapped token ETHtz (ETHtz homepage)
2. The USD-pegged stablecoin USDtz (USDtz homepage)
3. The Wrapped Bitcoin tzBTC (tzBTC homepage)

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

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.¹⁰ 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.

From April 20th you will be able to download Umami beta here. See also the Umami GitLab repo.

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 resillience 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.¹¹

After the upgrade to Emmy^★ there will follow an upgrade to Tenderbake. Tenderbake belongs to the classical BFT-style family, so the switch from the Nakamoto-style to the classical 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.¹²

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)

Research and sponsorship

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:

• On Monday 18 Jan, Arvid Jakobsson presented the formalisation of the Dexter decentralised exchange contract in the Mi-Cho-Coq framework at CPP’s 2021 Lightning Talks session¹³.

• On Wednesday 20 Jan, Michel Mauny, Nomadic Labs’ CEO, made a short presentation of our company at POPL’s Sponsor Reception, which also featured a contributed video presenting a general overview of Tezos by Arthur Breitman.

• On Friday 22 Jan, Germán Delbianco presented new developments in the algebraic foundations of Concurrent Separation logics at POPL¹⁴.

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.

Table of contents generated with markdown-toc