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
- Easier, safer, better installation of the Tezos codebase
- Culture and growth
- Announcing 1,000 days of Tezos mainnet
- Adoption and support
- Forthcoming switch from Emmy+ to Emmy★ and then Tenderbake
- NL research seminars
- Research and sponsorship
- À la prochaine
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.
- 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 environment2, numbered “Version 1”.
This is significant because until now, all protocols have used “Version 0”.
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
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.
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.
As of Friday 26 March 2021, the Tezos mainnet is 1,000 days old. See this subtle poster on Reddit:
(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
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:
Nomadic Labs has helped to deploy Lugh (currency name EURL).8 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.
Examples of smart contract implementations satisfying the FA1.2 interface include:
- The ETH-wrapped token ETHtz (ETHtz homepage)
- The USD-pegged stablecoin USDtz (USDtz homepage)
- The Wrapped Bitcoin tzBTC (tzBTC homepage)
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.
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.
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):
- 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.
- 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.11
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:
- 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).
- Tenderbake has no forks. If the network degrades, the Tenderbake consensus algorithm waits until connectivity is restored.12
Our series of Nomadic Labs research seminars has continued at a regular pace:
- Practical proofs using Juvix (27 October 2020)
- Verifying smart contracts using Mi-Cho-Coq (10 November 2020)
- Efficient data storage on the blockchain using Plebeia (24 November 2020)
- Adding multicore programming to OCaml (08 December 2020)
- zkChannels in Tezos (05 January 2021)
- Towards mechanised verification of the LIGO compiler (20 January 2021)
- SmartPy: the inner workings (02 February 2021)
- Bringing K Powered Blockchain Security to Tezos (16 February 2021)
- Implementing Checker, a Robocoin Mechanism for Tezos (02 March 2021)
- 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:
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 session13.
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 POPL14.
You can read our full POPL 2021 retrospective here.
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.
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 … ↩
… 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! ↩
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”. ↩
Contrast this with paper-only scripts, which exist in the documentation but must be manually tested and copy/pasted. ↩
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. ↩
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
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. ↩
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. ↩
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. ↩
Classical BFT-style algorithms are safe, but not live, whereas Nakamoto-style algorithms are live but not safe. This means that a classical 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. ↩
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. ↩
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 ↩