CBC Casper Design Philosophy by Vlad Zamfir (Devcon4)

hey everyone how's it going they already started my clock so I'm just gonna start - so we got talk today about CBC Casper design philosophy it's mostly really about design methodology and I'm gonna walk you through some of the stuff that goes on in CBC Casper land in terms of the methodology that we use to develop and define distributed systems protocols I'm gonna talk about it first is like what is carpi construction and I'm gonna talk about domain theory and then like this kind of defined in this stuff it's gonna be kind of a trip it's gonna be pretty cool and then I'll talk and I'll give some examples are like actual CBC design in CBC Casper and some of the you know stuff that happens and to give you a kind of a taste of the methodology and [Music] you know like the the kind of approach that we have that kind of sets apart a CBC Casper from you know other because there's a protocol research and finally you know the last bit of my talk I'll just to remind you all that where the resources are show you some new resources and make some announcements so let's talk about design methods in CBC Casper the number one kind of like design methodology in CBC Casper is the correct by construction design a protocol design methodology the idea with correct right construction is that like the process by which you decide what program you write should guarantee that that program has the properties that you want like the very process that you use to specify the protocol should guarantee that the protocol has the properties that you want so somehow like the way you decide what like formats to use or what like the protocol is in terms of like the data and the behavior you know that happens somehow like the definitions don't come out of nowhere and there's like a process by which stuff gets defined and it's called you know your first eyes are called correct by construction if you know the process that you use to define the thing somehow is guarantees that definition that comes out is correct this is kind of as opposed to the trial and error approach where you will like try something and then analyze it and then you might it might work am I not you'll maybe get lucky and maybe and if not they may you learn something and just keep trying until maybe you'll find something so this is very different approach right because instead of like we never really have the trial and error we just have like a lot of time defining stuff and then like once the definition pops out it's like correct by construction and so there's no like error but in some way like you know it takes us a lot longer to come out with a full definition but when it when it pops out you know we know it's correct by construction and we don't worry at all about mmm mistakes in the specification in the same way so there's two basically kinds of correct by construction software design that I'm kind of aware of one of them is you know you you define like a a proof may be a type system and some proofs over broad class of four over calls or broad classic programs and then you in your design process choose your protocol your your protocol to be part of that set so that you know when you choose it that it's gonna satisfy the theorem that you know is is is inhabited by this much broader set of protocols so if we have like a you know family of protocols they all satisfy a theorem and we like pick protocols or construct them in a way to guarantee that it part of the family then we can in a correct by construction way get a protocol that has that property that you know the theorem shows for the family and then the other kind of approaches that the protocols are specified in a way that actually generates a proof of their correctness so you know the you generate the protocol and the proof like a new proof for every proton and and they don't do any of that it sounds hard and I've ever heard of people doing it and like programming languages and compilers but it hasn't showed up for me yet so what I do here is basically we we do is we define large family of protocols and we prove things about them and then we and then we and then we choose specific protocols out of them which will there by virtue of being in those families have these properties so now we're gonna switch over to this very related topic but going off into the math deep end so domain theory is a field of mathematics that studies it's a you know a it studies the semantics of programming languages but really the reason why is super interesting to me and it just invites really useful for understanding the correct by construction process is because it provides us a language for talking about partial definitions you know incomplete definitions partial protocol specifications and and and we can understand what it means to have a process of defining something as opposed to just having something that's outright fully defined as you might have in set theory so like you know you should think of domain theory as something that arose out of people's feelings that set theory was inadequate for dealing with programs and the semantics of programs especially recursive programs and like a lazy evaluation mmm but I'm not an expert in domain theory but there are some things that I've learned from domain theory that I find super useful for thinking about a bunch of stuff including correct by construction protocol design so there's a really really you know kind of core notation in in domain theory to use this like and to define this thing called undefined so this bottom notation means undefined and it's like defined to be the most undefined thing it is the most undefined thing in this partial order of defined admits like if I if I say nothing about my protocol then like I have left it completely undefined and then somehow that's like the most undefined that I could leave it and as soon as I say stuff I it becomes more defined and we could talk about in reason formally about this order of defined earnest and this process of defining stuff and you know having a certain stages a partial definition and then getting in more and more learn more defined protocols so if a is a definition that can be reached from a definition B by replacing an undefined term and B with something that's defined or something else then a is gonna be is more defined than B so basically like if I have a definition it's got some undefined term in it and I can replace it to get some other definition then that other definition is more defined than this like initial definition so I'm gonna give some examples so here we go you know bottom times bottom is more defined than bottom because you can replace bottom with bottom times bottom and therefore you know you can define something there's clearly under find bottom to be this thing bottom times bottom which is still not totally defined but it's more defined than just bottom you know bottom times empty set is more defined than bottom times bottom because you can replace bottom with empty sets and get from bottom times bottom to bottom times everything what about empty set times bottom vs. bottom bottom well you know you can place the first bottom with an empty set and so the thing on the left is more defined than the thing on the right but the next example is a little trickier because it's not more defined than the thing on the left sorry the empty set times bottom is not more defined then empty set times bottom times empty set because you can't replace the bottom to get empty set times bottom because there's already in it empty set in that position so you know basically what we're doing is replacing the bottoms on the right to see if we can get the thing on the left and if we can't then it's not more to fine then and if it if we can then it is more to find them so at the end of the day where we kind of get is this picture this partial order of the defined Earnest of these terms so like bottom is the most undefined bottom times bottom is a little more defined these two terms left and right there no more defined than each other even though they have a term that is in common I mean a term that if both of them can define that you know a term that inhabits both of these partial definitions and so kind of you know what we do in the correct by construction process is we move from less defined protocol specifications to more defined protocol specifications we have a kind of process of we say something about the protocol that we prove things about protocol so that later when we continue to define the protocol the things that we proved continue to holds because all of the later definitions are just a they're just a refinement of the previous definition you know so you know so the the kind of theorems that we have for less defined versions of the protocol spec are going to hold for more defined versions of the spec and this kind of starts to make you feel why we have like this correct by construction protocol design because at some point we're gonna have a partial spec and some proofs and then there's no way for us to define that spec more that will kill those proofs so basically like our kind of strategies to like deliberately give and Peru or give partial specifications and prove things about partial specifications so that we can have a lot of flexibility in our iteration and design because we can continue to define from that point in many different directions without having to worry and go back about you know verifying and changing proofs that you know because of the change in the protocol so like a lot of the time when you have a protocol and you make a change you're gonna have to like change the proofs that you have about protocol but if you instead has some partial definition of the protocol that you had two proofs from which you could change and you can make your change to your protocol by just read continuing to define the protocol just like in a different way from before then you can you know not have this additional proof obligation because you just have proven it for a much broader class of things which are kind of the things that inhabit this less well specified definition of the protocol so let's so you know I think we can get a lot of flexibility in design because we because of this because of this approach i so here is some actual like partial order of defining this in like some definitions that we have in the casper cbc casper world so we have this minimal cbc casper family of protocols which is like the specification it's like the easiest to understand the smallest the few fewest parts and we defined terms in that specification to define like the binary consensus for all the block chain consensus protocol and other cuz it's protocols that you've seen if you've watched me present on cbc casper over the years and so all of these protocols these three protocols the binary consensus protocol the integer and the friendly ghost they're all more defined than the minimal CBC casper specification and they all satisfy the same proof as the minimal CBC caste respect and these these all therefore we kind of benefit from that proof and we don't need to look back much when we do when we're defining forward from this minimal CBC Casper family we don't need to look back and ask about what that proof will continue to be satisfied but you know this this this family of protocols actually has a full note condition it requires that all the messages all the nodes processes all the justifications of all their messages and so that's actually not super useful for example for sharding and so we don't actually want to have to define sharding as a further definition of this specification because it's a full it requires it's full note condition and so actually what we do instead is we have like this other spec which is like this like client spec which you know where clients don't need to have all of the just all of the resolve all the pointers and all their messages and so we and we define the started watching says protocol spec as an instance of this like CB light client CBC family protocols which all satisfy the same because that's a safety proof and actually there's like a more abstract family of protocols which is you know considerably harder to communicate than the minimal one but which is less defined than both the light client protocol and the minimal CBC Casper protocol and so like if we with with this kind of set up what we think what this does is it gives us a little roadmap of like starting from where like what is defined and what properties do you have and if you go downstream from there and continue to find stuff you know what would you get to benefit from and so it can be really you know I think this kind of notion of a disorder of define Innes and of progressively giving more and more defined protocol specifications is very very very very much what we're doing in correct by construction protocol design because we're engaged in the process of defining something and we start we don't have a full definition but we want to get to a point where we do have a definition that satisfies certain properties and we want to know that the process that which we follow will guarantee that we have those properties and so you know which we try to have it's kind of a disciplined approach for getting them one step at a time and where we don't really have to look back so but you know it's not always as straightforward sometimes we have like alternative choices of what how exactly to define stuff and even to get the same goal so it's you know I painted a pretty simple picture but the reality is more complex for example for validated rotation the easy thing to do in terms of the protocol specification and the proof obligations is to just launch lots of instances of these protocols that have new validator sets and that really can work in some cases but there are also cases where we want to define protocols that do validate a rotation in a way that is outside of the minimal CBC Casper framework and whenever we do this kind of design that's outside of the of the framework we need to do we create new proof obligations and so we sometimes have to have a choice between you know do we do we design things and way to take advantage of existing proofs or do we come up with a new system on a broader family that or that have other proofs and it's it's it's tricky because like on the one hand we want to benefit from other folks we already have and we're gonna make any new ones on the other hand when we have when we can generalize stuff sometimes we can generalize it a little bit and not as much as we'd like and so if I come up with a more general family of protocols for doing validated rotation for example like I haven't come up with one that really does everything I want and so there's there's there's there's definitely it definitely isn't as simple as like you know define as you go and everything will be fine there's real choices that we need to make and like in the design process so one of the decisions we've made for example is that validator strategies are not part of the specification I would like the core core like the you know the core partial spec is only for clients it's like not the spec for miners or for people who make messages as people for people who receive them and and the reason why we did this is because there's like kind of it separates out the parts of the protocol in a way that allows us to tackle them separately and we can like independent of when validators make messages or how validators make messages show consensus safety so we have this big part of this the protocol of like when do you know it's make messages which is not defined in the course back which both seems weird because you'd expect that to be part of the consensus protocol but it also is really nice because there's nothing that there's no way that that term could be defined in a way that disrupts the proofs in the for the like client protocol and so validated strategies are not in the core the core partial protocol spec and I and that was like one of the decisions we made and deaf I definitely don't regret it at all we have a bunch of design decisions that are motivated by economic thinking but also at the same time we leave incentives undefined until very late in the game because the incentives have to respond to the actual states of the protocol and the actual and you know the consensus protocol itself and so you can't actually define the incentives until the consensus protocol is defined and so although we do a lot of thinking economic thing in front and we come up with a lot of disturb you systems properties that we want based on the economic thinking the and the the the the definition is of the incentives is left for later so you know we have the the fault tolerance threshold is not specified in the protocol there's like a decision we made and like very like you know like it was not an arbitrary decision and was like was motivated by like the design requirements that we have and we have and this is and and this is like an area where it's not in the core reference spec but we have a proof for how noes use would use it with different fault tolerance thresholds and so we can without changing the core spec very much give proofs for a new kind of use of the protocol so you know more kind of weird proof tactics around you know using multiple instances of this like correct by construction core protocols partial spec you know we have preventing das will require like you know that we bound the amount of work required to process a message and that people have throttling for the amount of messages that they can receive and so that is that's good that requires a new constraint on consensus messages it requires new strategies for the validators none of this stuff is part of the core protocol spec none of it is part of the minimal you know core piece of the like you know those like the start of the correct by construction process and all of that is kind of very deliberate because the idea is that we can define this stuff later and it's more than fine because we didn't screw it up by defining it earlier so so the the the the other kind of you know really cool thing about the crack by construction approaches the fact that you can iterate actually quite quickly without having because you don't have to reason about much of the protocol when you make changes you because you literally could not define it it in a way that screws it up and so we show you some of the progress we've made in the last little little few months on some of the charting stuff so this is what came out of the East Berlin hackathon we came up with like a pair of shards one of which kind of follows the other one there's very it's very similar to the traditional CBC cast burkas protocol in the sense that like it's you know it's really implemented completely as just a definition and a further definition that protocol by giving the consensus values and the estimators and the validators and their weights and the fault on a threshold so so so we did this binary so we said we did this to two shard system and one thing that we kind of have been wanting to do for a while that finally kind of got to implementing is you know I mean just like a few months like there's a really short order is shard rotation so like here what we see is two shards that are changing position one of them is the route at first and then it changes and then the other one is the route and then it changes again and the other one is the route so the purple blocks there are route blocks the yellow blocks are child locks and the roles of these shards and the hierarchical census are changing and this does not require that we reason about consensus safety at all because the the correct by construction process kind of guarantees that I with no thought because it's kind of upstream from our definition process and so relatively little work compared to normally working Contessa's protocols we define this like actually relatively complex because it's protocol there like this comes to consensus on you know the state of two shards with locks that have like two different positions and have like a relatively complicated fork choice role and here's like an the kind of next kind of conclusion of that is like oh look when we have two shards that can send messages we can do routing we can move shards around in two positions we can move short rounded more and then we have this you know pretty cool sharding solution where we have messages being routed around cross yards and with like the atomicity property that if your route isn't fully completed then the block that started that route will be orphaned so we have like you know a really kind of strong ability to iterate very quickly because of the correct by construction approach because we don't need to look back at the previous guarantees we're not at risk of disrupting them and so the you know I'm never walking through this again so this so so what's gonna happen here is first the the route chart was initially 0 now is switching to one these messages are being routed from chars 6 to 3 and back charged shard 0 and one switched from 0 1 to like 1 0 and then and then back and then shard 3 became a child to start for even though it was previously a sibling and then messages start to get routed through shard for after that swap so it's really kind of quite complicated we have like routing tables and they're updating and but we really didn't need to think about consensus protocol is almost at all whilst us find this thing so you know we have thank you so we have like methodology that lets us define consensus protocols we've defined a large number of consensus protocols or partially defined a large number of consensus protocols and you know and we iterate while creating minimal proof obligations and we are able to mix and match kind of a lot and you know so I recommend that you try out you know correct by construction and we sorry I'm looking at the wrong slide here got ahead of myself that was the next slide so we basically really rely on these partial specifications and you know the fact that it's not defined yet is actually a huge asset for us the fact that we leave things undefined until you know the latest possible moment means that we have as much flexibility as possible to iterate without disrupting our previous proofs so all right you said all this yes it's it's great try it correct by construction protocol design it's awesome so now let's moving to the like kind of announcement section of the talk so that was that was like oh that was pretty much all of the all of the content so we have some a bunch of a bunch of announcements of people like you know contributing to a CBC Kasper research this is a brog ham rock from true level built a generative testing for CBC caster protocols I'm gonna let see if I can and then with this spoiler alert so with this what this kind of shows here is a the the red the red dots are members of a clique which are validators who see each other agree in a way that they are actually finalizing that block the blue one down there and this is something you know related to the way that finality works in in in Casper and and and here we see like multiple views of the protocol from the point view for different validators until one of them finds a decision on this block namely finalizing you know this this blue block and the the green dots are the messages from the validator whose view and the red dots are the click which I was like a group of validators who sees each other agree in a certain way that corresponds to a because that's a signature that you know is like a decision so so that's pretty cool stuff you know that I mentioned the charting proof of concept we've been working on this but like I look significant like rotating group of people since the Berlin hackathon and actually before that at the etherium ic3 workshop we worked on the specification especially want to give a shout out to Alex Keaton off who in the last like you know week and also during the East San Francisco hackathon put in like heroic efforts to get the grouting working and the shard swapping I mean he's the first guy he's the first person to prototype the cross shard message routing bit jealous but you know you should check out this github repo and see if you like it and it's not there's still loads of bugs but there's you know it's definitely interesting Aditya who is probably somewhere here has announced that he's implementing a shortened client with like you know they're in blocks and like you know very like aetherium starting client and he has a github repo and that Twitter handle he should follow him for his work we this is a exciting one we kind of released a draft or are going to release a draft I wrote these slides I thought we'd have it released by now but we're gonna release a draft today of oh wait it is released my bad github calm slash CBC Kasper and you can download a new specification of the minimal CBC Kasper of protocol states that is you know extremely rigorous and pedantic with extremely rigorous and pedantic proof of the consensus safety result and example protocols including the Friendly Ghost a finality gadget a sharding with fixed hierarchy and I'd like to thank the code my co-author is Nate rush Aditya and Georgio's and they're all here you you should you can probably recognize them from their faces I put a GES face was on the previous slide finally you know don't forget about the prototype in the wiki at dairy m / TVC - Casper these are like good resources if you want to like dip your toes and check it out you know we're totally looking for help of all kinds and we're getting better and better at helping you help us as they're like documentation and definitions and stuff have laid themselves out in a way where you can you know come in and contribute in a way where it's really clear how it interfaces with everyone else's work and where you know you won't be wasting your time and you will be helping so you don't reach out and thanks so much for listening I have time for one question it's okay you don't need to ask a question I can just go by everyone oh wait there's a question sorry sorry sorry do you have a microphone so what's the deal there the microphones are at the front you have to come come over to the front we got like 30 seconds you got to be quick 10 second question 20 second answer yeah can you hear me good what's a good way of really understanding CBC if you come from a math background yes read this paper and anything anything more sort of high-level just know the paper is really good it's just that it's set theory okay it's very accessible I think okay you [Applause]