Intro to Proof Techniques: Blockchain Properties. Part 1 of 3 | Cédric Waldburger

This is Part 1 of my conversation with Robert, who explains on the whiteboard what provable properties a blockchain must have to provide a finalized total order on transactions. The 3 fundamental Chain Properties are called Chain Growth, Chain Consistency, and Chain Quality.

Video Transcript:

Welcome back to yet another episode of Inside DFINITY. I’m back in Zurich and I used the time before Robert flies out to Palo Alto to get together. Today Robert and I are going to talk about the technicalities of our white paper. So back at the beginning of this year 2018, the DFINITY put out its first white paper describing its consensus mechanism. While it might be a little intimidating for people that are not very used to reading white papers all the time, there’s a lot of very interesting information in there.

Today we want to give you a bit of background information that might make it easier for you to read the white paper and also go into some of the proofs that we go through in that white paper.

DFINITY White Paper

Cédric: So without further ado, Robert welcome to the show and over to you.

Robert: Thank You Cédric for this introduction. As you said, I will try to give you an overview about proof techniques used in our white paper and I will try to show how we break down all the important properties into more specific properties that let us prove that our system provides what it should provide.

Proof Techniques

Robert: Let’s start by looking at the proof techniques used in the white paper. So the first question that we have to ask ourselves when proving any kind of properties is, “What do we want to prove in the first place?” As I already mentioned, we want to prove some properties of our system. We want to show that some properties hold and we will start by very general properties and we will break them down step by step.

Then, there’s another important question, “Under what circumstances, should our system offer this set of properties?” As we will go into more details, we will see that we will have to come up with models, in which our properties should hold. The models can be thought of on one hand as the capabilities of our system – so the tool set available to our system – and on the other hand, we also have to model the capabilities of our adversaries.

Cédric: On one hand, our system and, on the other hand, it’s the adversary. Just before we dive into the details maybe I can quickly summarize what I just heard. It makes a total sense but it’s good to ask ourselves that question at the beginning, “What is it that we actually want to prove if we set out to prove something? There are two dimensions to look – at one is what are the properties that we want to prove and I guess we’ll start with some verbal description of those properties and we probably want to get down as close as possible to the math layer or logic layer.
Then, the second under, under which circumstances do we want to prove those properties and you mentioned two dimensions – one is our system vs. adversaries system.


Robert: As I said, we start with very broad properties that are general in the sense that they apply to any kind of system not only distributed systems, not only blockchains, but to any kind of the system that runs on a computer. What properties should a system running on a computer offer? The system should be safe. So the property is safety.

Safety means that the results produced by the system should be correct. On the other hand, it may be less obvious but we also want to have a system that’s live. So liveness is the keyword here.


Robert: Liveness means that the system actually produces some results very general. So let’s break this down a blockchain is a special case of a ledger; so you can think of other ledger’s, which could be created by using some kind of directed graphs or other data structures, blockchain is just one type of ledger – the more general term. So let’s see what properties a ledger should offer.
We can just make the safety property a bit more and specific to the ledger. We say that a ledger is a means of recording transactions and of ordering transactions. So safety in that sense also means persistence; a transaction that got recorded in the ledger at some position shouldn’t change that position after all because we want to have total order on all transactions recorded. Once the system or the ledger outputs some kind of ordering, this ordering should be the same for all nodes or for all participants in the system. So same finalized order for all nodes –this is the safety property applied to a ledger.

Let’s apply the liveness property. Here what we want is that every user should have the possibility to send a transaction and to actually get a transaction recorded in the ledger. If a transaction is sent, it should appear in the ledgers of all nodes or, at least, the honest nodes that follow the protocol. The transaction will get in to finalize the ledgers. That’s a bit more specific but it’s still quite general.

Chain Properties

Robert: As you mentioned before, we at DFINITY – we are building a blockchain, which is a special case of ledger. We have to break these properties down even more.  So this is the third step – let’s call the chain properties – and now we will have three properties so more fine-grained properties.

Chain Growth

Robert: The first property that a blockchain should offer is Chain Growth. Chain growth means nothing else than we have a chain that grows – that means that blocks are appended to the chain and the chain increases over time. So C denotes the chain; C grows. This is the first property.

Chain Consistency

Robert: The second property that we want to have is Chain Consistency. Now what does Chain Consistency mean? As I already mentioned, we want to have a chain or a ledger that’s persistent and that’s safe, which means that the transactions should be finalized in some specific order that is the same for all nodes that follow the protocol. Chain Consistency in that sense means that if two nodes have finalized in their view like a blockchain, then these two finalized blockchains shouldn’t conflict with each other.

If C is like the chain of one node and C’ is the chain of some other nodes, then C should be a prefix like a subset of the other blocks contained in C’; or because it can also be that C’ is shorter than C, so it can also be that C’ is shorter or just the prefix of C. So if any of these two properties hold, then we can say the chain is consistent.

Chain Quality

Robert: I should go on with the third property, which is called Chain Quality. What is Chain Quality?

In a distributed system, there are multiple participants and we want to have a system that is also decentralized, which means that everyone who participates as a miner should have a fair chance of creating blocks and of actually being part of the system. In that sense, we can say the Chain Quality means that every participant should have a fair chance to get part of C. Now this is quite untechnical. So it means that if you create a block as a miner, then your block should have a fair chance of getting included in the chains – the finalized chains in the network.

Cédric: Okay. So we went from step two, where we talked about ledger properties to chain properties now. At the ledger properties level, we still had two properties that we were looking at – liveness and safety. Now we have three on the chain layer. Can we say it was one property broken up into two of these new properties? How do we go from one step to the next?

Property of Persistence

Robert: We can state a relation – so if we have the chain consistency here and chain growth, then we can say or show that this gives us persistence. Why is that? If you imagine a chain that grows, you also have the property of consistency, which means that there cannot be conflicting views among honest participants. So they will all have a subset of their chains that will always be in accordance with each other and the chain also growth, i.e. this means that once you have a transaction included at any position of the ledger or in any block and that can only grow and the growth will be consistent over all the participants, then it’s obvious then that this property of persistence holds.

Cédric: Here we’ve shown that the two properties on the chain layer – consistency and growth – relate to the persistence property that we define on the ledger layer.


Robert: Exactly. Let’s see how the chain growth and the chain quality play together. If you have the Chain Quality and Chain Growth and this gives us liveness. Liveness can be thought of a property with two different aspects. So we not only want to have a chain that grows, but we also have offered a property or offer a system where transactions can actually be added to blocks.

We know that honest participants will pick up the transactions that are sent through the network and they will add them or include them in their blocks. If we have this property of Chain Quality, which means that an honest participant will have a fair chance of getting his block included to the chain and at the same time we know that the chain grows, so we also know that the transactions will be appended to the chain  and will become part of the ledger. That’s why Chain Quality and Chain Growth gives us the liveness of the ledger.

Cédric: Got it. So Chain Growth on the chain layer is the quality that we need for both liveness and safety. If we go back to the very first couple properties that we defined.

Robert: Chain Growth is a very fundamental property because without Chain Growth there is nothing to talk about.

Total Oder vs. Partial Order

Robert: Now maybe let’s look at one other important aspect I already mentioned that we should have a ledger that creates a finalized order on transactions. I also mentioned the word Total Order and let’s see what that means and why we need Total Order. Maybe let’s start with the difference or with the two aspects, which is Total Order versus Partial Order. What does it mean?

Total Order

Robert: Total Order is a property, which means that if you have a set of transactions or a set of any kind of artifacts or just data blocks, then you have some algorithm that outputs an order for the whole set, which is clear and unequivocal. On the other hand, Partial Order means that if you have a set of objects, then partial order gives you some kind of equivalence relationships for each pair of two objects. For each pair of two objects from the set you can say that A primes B or a comes before B or comes after B, so this means that you have some function, which outputs the relationships between two objects.

The problem with Partial Order is that it doesn’t automatically guarantee Total Order. Why is that? Let’s assume we have three objects in a set and some function that outputs these relationships, then it can happen that A primes B and B primes C, but C primes A; so we have a loop. It’s not possible to derive any kind of total ordering in the sense that A is higher than B and higher than C. That’s not possible.

Payment Ledgers

The interesting fact about this is that for payment ledgers like bitcoin or for systems that just want to offer or enable a payment system, it turns out that it’s sufficient to have Partial Order because the only thing that you have to guarantee if you look at payment transaction is that you cannot double spend your funds or your coins. You can achieve this kind of guarantee in that you create a system that creates a Partial Order on conflicting or double spend transactions.

Cédric: That could, for example, happen if I were to send a transaction to the network, where I spent one bitcoin and I send it to you, and at the same time I’m trying to send it to someone else. There needs to be an order, where one of the transactions is cancelled and only one of them is executed for all nodes.

Robert: You just need to make sure that the order between two conflicting transactions or double spend is preserved; so you can cancel one, but you don’t need a totally ordered transaction history.

Cédric: So for that one bitcoin that I currently own we don’t really care about who possess that bitcoin before me and in what order the only thing that’s important is that when I got it, I got it from one person I was not able to spend it in any other way than sending it to me at that point.

Original Nakamoto Consensus Blockchain

Robert: Yes. But it’s important to note that Bitcoin goes further than that. Bitcoin – the original Nakamoto consensus blockchain – gives you a Total Order. It gives you a Total Order after some time; you need to wait some number of block confirmations. But once you have this probabilistic finality, then you can derive totally ordered history on your transactions. In that sense Bitcoin is a bit like an overkill.

Cédric: Because it provides more functionality than what’s necessary in order to have payment networks.

General-Purpose Decentralized Applications

Robert: On the other hand, DFINITY, Ethereum and other networks want to offer a general-purpose smart contract or even general-purpose decentralized applications. It also means that multiple people should be able to access some applications and you also want to have some complex systems. To enable such systems you need to have Total Order because you do not just want to prevent double spends, you want to enable more complex transaction logic. For general-purpose systems, you need a Total Order.

There are interesting projects, research papers out there, which propose systems that only provide Partial Order, but which are much more efficient than Bitcoin. These are interesting systems but, unfortunately, we cannot use them because we want to offer general purpose smart contracts.