Intro to Proof Techniques: Proofs. Part 3 of 3

This is Part 3 of my conversation with Robert, who gives an overview of the steps to actually prove that the desired Chain Properties hold in the given model. Starting from protocol events and their relative timing, one can draw interim conclusions that finally allow to make the proofs.

Video Transcript:

Cédric: Okay. So we’ve gone through the different properties that we want to prove; we’ve talked about the models. Now what are the actual steps to get to a proof.

Robert: I cannot show you how we did the proofs, but I can give you a short and step-by-step strategy you should apply to get your properties proved.

System Events

Robert: Maybe the first step that we should look at is what are the events, the most important events in our protocol or in our system that we can categorize and that we should look more closely at. So, the first step is to identify events such as like notarizations or like when the random beacon outputs a new value. Once we have identified like the relevant events, which are important for security and liveness, we can go a step further and see how these events are timed – so which event happens first or next and how the time-based relationships are between these events.

Traversal Time

Robert: By doing so we can also derive like bounds or upper bounds on the timing because we have seen that we have this assumption that every data packet or artifact has an upper bound on its traversal time. This is this Delta that I mentioned. So now we can compose multiple events and see how many Delta it takes for one action to trigger another action.

Another aspect which is related to the timing is how the actual nodes would react to like maybe the reception of some notary share or a random beacon output. What will their reactions be and what will be the consequences on other nodes. We look at like how well node reacts to some action and what consequences this action can have on other nodes. We infer reactions and consequences.

Replicas

Robert: If we go a step further and try hard we can draw conclusions about some interim steps. As a example, we can derive some values on which is the maximum difference between the progress of two nodes with regard to the chain, so what can be the difference of the views if you look at two replicas or two nodes. Also if you may send or broadcast a new block when can you be sure that the very last – so the slowest replica – will actually notarize that block and so on.

Lemmas

Robert: We can like draw conclusions and formulate them as lemmas like, for example, what is the maximal progress within a certain amount of time. Then once we have established a set of lemmas in the right way, of course, then we can finally reach to our proofs. So we derive our proofs from these lemmas and demonstrate what was needed to that be demonstrated.

DFINITY White Paper

Cédric: Maybe we should take a step back again. I mean in today’s episode what we do want to do is give you  bit of an idea of our thinking of how to approach the White Paper. So that reading the White Paper becomes a bit less intimidating and recognize some of that structure that Robert just walked us through.

In general, getting to the proofs for the system that we’re describing we first described a number of properties on different layers, then we talked about the models in which those properties need to exist, we talked about our own model versus the threat model – basically what we cannot control – then Robert also walked us through five steps of how we get from there down to at the individual proof and how we prove that things are lively or the liveness and the safety of our systems.

Robert: That sums it up very well.

Cédric: Good stuff. So if you’re now ready, if you feel ready and ventures to dive into our White Paper then head over to DFINITY.org and there’s a section for the White Paper. By now, it’s not only available in English, at least a few other languages. You can go in and dive in. Hopefully today’s video will give you a bit of an overview that makes it a bit easier to digest the White Paper.

With that, thank you all so much for listening. Leave your questions below. If you like this video, then please subscribe and make sure you don’t miss any upcoming episodes. With that, we’ll talk to you soon.

Comments


Cédric Waldburger

Cédric Waldburger

Founder of Sendtask.io 🚀. I'm passionate about startups 👨‍🚀. I live out of a carry-on 💼. I own 64 things. They're all black.

Get tips & advice on essentialism delivered straight to your inbox