Granada comparisons bug
As a major development center within the Tezos ecosystem, Nomadic Labs routinely performs ongoing reviews and analysis of the Tezos protocol code. In conducting a recent review of the Granada proposal, we identified a low-severity bug that occurs in an uncommon pattern in the handling of comparisons, which we would like to raise awareness of so that developers and bakers can be best informed.
The bug was introduced when refactoring the Michelson interpreter. The refactoring dramatically improves gas consumption (typically by 5x or more), but a case was missed out in the Michelson
COMPARE function (for Michelson values): when comparing two pairs where the first element of each pair is an option type set to
COMPARE concludes that the two values are equal when correct behaviour would be to recursively compare the right parts of the pairs. For example:
Pair None 3 and
Pair None 5 would be deemed equal by the Granada
COMPARE operator, when they should not be because
5 are not equal. The ability to compare option types in Michelson is fairly new and was introduced in Edo. This was further confirmed after we reviewed the contracts deployed on Mainnet, Florencenet, and Granadanet and found that no contracts currently use the pattern that would trigger this bug. Thus, no current contracts would be affected by this error in the Granada proposal.
Please note that future contracts could be affected in the following two scenarios:
- comparing values that include option types, or
- using values that include option types as keys in sets or maps (big maps are unaffected).
Neither use case is common, and even if they do appear, they only affect the contract using it, not the protocol as a whole.
While the Michelson interpreter is well covered by tests and pair and option types are tested, the uncommon combination that triggers this bug was not, so this bug was missed by the test suite.
To better detect such errors in future, we updated our test suite to use property-based testing. Property-based testing is an approach that automatically generates random test cases that try to break a function’s desired properties, and is better able to help surface these types of bugs caused by uncommon pattern use. We used property-based testing recently to test properties of the smart contracts used in Liquidity Baking.
If Granada is adopted in the next voting period then:
- A fix for the comparison bug will be included in the subsequent “H”-named protocol. If adopted we would expect this to activate in October 2021.
- Although developers are unlikely to use the patterns that produce incorrect behavior as described above, for safety and convenience purposes we will provide a linting tool to help detect them in code.
Introducing Mi-Cho-Coq v1.0
The first public release of the Mi-Cho-Coq framework
It’s our great pleasure to announce Mi-Cho-Coq version 1.0: the first public release of the free and open-source Mi-Cho-Coq framework, a library for verifying the correctness of Michelson smart contract in Coq using weakest-precondition calculus. The Mi-Cho-Coq framework is a Coq library which models all aspects of the Michelson language: its syntax, its type system, and its semantics. Although this is the first public release, Mi-Cho-Coq has been in internal use...
A veteran implementation of Tezos gets a name: Octez
Rome the city, Rome the ideal There’s a powerful scene in the film the Gladiator where the Emperor Marcus Aurelius explains that Rome is both a physical installation of bricks and mortar, and also it is the idea of Rome — an ecosystem of standards and laws by which the people lived and a city was built. In other words: Rome is a city, and an ideal. When you download Tezos, you are actually downloading code that runs on...
This is a joint post from Nomadic Labs, Marigold, TQ, Tarides, and DaiLambda. We were proud to see Florence go live on the chain on 11th May 2021. In keeping with our policy of proposing upgrades on a regularly scheduled basis, we’re happy to announce our latest Tezos protocol proposal, Granada. (As is usual, Granada’s “true name” is its hash, which is PtGRANADsDU8R9daYKAgWnQYAJ64omN1o3KMGVCykShA97vQbvV). Granada contains several major improvements to the protocol, as well as...
Announcing a simulator for Tenderbake
If you’re impatient, you are welcome to read the guide and jump right to the simulator now. See also the implemented algorithms below. If you find that reading about it helps you get excited before using your simulator, then read on … Background The consensus algorithm is a crucial part of any blockchain project. Because of the distributed nature of blockchains, different nodes can have different ideas of what the current state of the blockchain is supposed to be....
Faster finality with Emmy*
Announcing forthcoming upgrade of consensus protocol, giving quicker time to finality (i.e. shorter transaction settlement times)
We are happy to announce that Emmy* is set to be included in the next Tezos protocol proposal Granada,1 replacing the current consensus algorithm Emmy+. If Granada is adopted, Emmy* will generally halve the time between blocks, from 60 seconds to 30 seconds, and allow transactions to achieve significantly faster finality than under the current consensus algorithm, Emmy+. Specifically, Emmy* updates Emmy+ by: a tweak in the definition of the minimal delay function, and an increase in...
Announcing the report “Possible evolutions of the voting system in Tezos”
Announcing a report on possible evolutions of the voting system in Tezos
Nomadic labs has an ongoing research relationship with INRIA (a French national technology research agency). In the context of this relationship, Nomadic Labs commissioned a short report to explore what a privacy-preserving amendment procedure might look like on Tezos, authored by three experts in voting protocols and cryptography: Véronique Cortier, Pierrick Gaudry and Stéphane Glondu. There is no plan to implement the contents of the report for now, but we welcome and...
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,...