Monadic Design Patterns for the Blockchain

Transcript

[Music] So, first of all, uh you know, thanks to Vitalik and Vlad for asking me to come and it's it's great to be here. I'm glad uh glad to be able to deliver a few impressions. I think in in 25 minutes that's all I can do is is deliver a few impressions. Vlad and I have been working a lot on Casper. Um and and kind of the the technologies and and tools and ideas that I'm bringing to the formal verification of Casper are also

uh embodied in some of the ideas that I'll be presenting here. So, um, kind of the, you know, just want to touch on the an overall narrative and then, and really, if you, if you walk away with nothing else, I want to leave you with this one big picture idea. Um, but, but, you know, in the details, there's enough space for God and the devil, right? So, there's always lots and lots of space in in the details and and maybe talk about some next steps. So, that's kind of what we're going to do. And the narrative is actually a fairly simple one. It's fairly straightforward.

Consensus is a necessary component of the blockchain. So you heard Vlad talk uh rather eloquently about consensus and some of the problems there. Um it it turns out I mean I think I think many of the people here know that that blockchain currently you know as embodied uh doesn't doesn't scale very well and Casper's variation and the proof of stake is an important step along the way towards scaling. I wouldn't say that it's it's the solution to scaling, but it's it's one component of of a scaling solution.

Um, and so so we we want to look at proof of stake and in particular the the Casper variant of proof of stake uh and really bash on it from the from the point of view of of formal verification. We we we'd like to know for sure once and for all whether Casper enjoys certain properties. Um, and so we're we're we're one of the tools that we're using to go about this is something called the applied pi calculus. Um, and this gives us and and I'll show uh kind of where we are in in the state of that uh later in the talk, but this gives us access to automated support for proof of correctness.

So the tools that we're uh employing right now in include uh proverif but but um much more the spatial logic model checker which was developed by Luis Kares um and uh uh that that turns out to be good fun and if you want to look at the code uh it's up on GitHub and I'll I'll give you a link a bit a bit later but it turns out that if you have a spec in the applied pi calculus well I have a bunch of libraries that up on GitHub called spec special K and they are an implementation an an an executable distributed virtual machine of the applied pi calculus. So if you have a spec you can turn it straight into an

implementation. So if you have a spec that you can reason about the the correctness properties then you can actually run Casper. Um and so this this is has big implications for the correctness of an implementation. what you get is correct by construction. And that's that's a that's a different approach to design than I think you know happens uh in a lot of um software a lot of the software industry but but in particular in this space um I'm I'm not sure that that that uh um the blockchain as originally conceived was was done in a correct by construction style. I think it was quite quite the opposite actually. Um but but if you do take on

correct by construction one uh this helps with scaling there there are a lot of different aspects to scaling right it's not just about volume and performance right it's also about um when when you have reliability reliability is what engenders adoption right so you think think about you're you're you're um you're someone who manages a large financial firm and there's this great new technology that promises wonderful things but am I going to swap it out for the thing that works. Well, I might be more inclined to do that uh take take on some of that risk if I knew that it had certain reliability properties that were formally and automatically verified.

Um, it also helps uh with uh with maintenance and evolution because as we know this space is changing very fast and so it's kind of important to be able to to uh adapt uh the code to the needs of the space. Um so uh it turns out that uh in addition to some of these benefits um special K provide already of its own provides a broad range of transactional semantics and and we get these because of the monatic decomposition of the the elements that are that are used to to

make these kinds of transactions and and I'll I'll go through those but you There's there's basically a handful of programming uh paradigms that are used successfully today in building uh distributed systems and and it turns out that you can organize all of those under a single rubric under essentially a single API. Um additionally uh the compositional nature of the uh of the the pi calculus. Uh so I'm just giving you some sense of all the benefits of of this kind of approach makes it possible to write down in a single page a metered distributed concurrent VM. So just for fun I'll show you that spec right at the

end. That's some nice feedback. That's some really nice high frequencies. Um, okay. So, so the big picture is that compositionality is the key to scaling any system. So, if you forget every everything else in this talk, if you remember that one idea, you know, I'm I'm hoping to plant that seed in your mind and and go home and think about that. So, what the hell is compositionality? Is it even a word? Right? If spellch check is going to underline it in red, I guarantee you. Um, so let me let me kind of unpack this idea. So, so in computing, I think we're all familiar with the idea that scaling refers to lots and lots of copies of of things that are, you know, potentially

not reliable individually, right? So, lots of chips, lots of boxes, lots of uh databases, lots of servers, lots of data centers, right? So, that's the traditional, you know, uh high volume, high performance uh notion of scaling. Compositionality turns this upside down. And what it says is that scaling is about making the the large reflect the small, right? And and every child understands this idea. They hold up the leaf, they look at the leaf, and they say, "Hey, there's a tree inside this leaf, right?" Um, and that is in fact how nature scales. And we see it again and

again and again. And it's kind of funny. Why is it that we forget? We knew this at one point and then we forget it. And why is it that we forget this? Well, it turns out that it's actually a fairly new thing for culture to remember this. Um, so I'm just giving you a few examples from pop culture of of this idea. And you'll notice that all of them, I mean, even Mandlerought sets are very new on culture on the cultural landscape, right? And just to give you another sense of how how interesting and different this way of thinking is. So here's a bunch of people who had

computationally very effective ideas, right? So you know maybe you know maybe you recognize Paul D. The Rock, maybe you recognize an Schroinger, but quantum mechanics as formulated in those days was not compositional. And it's only been in the last five years that we've had a compositional formulation or presentation of quantum mechanics via Samson Abramsky and Bob Cooker. Uh a similar thing has happened uh uh in the physics of the large gravitation and cosmology. And because we don't have good compositional accounts, physics fails to scale. We don't have a nice way to marry those two ideas. So if you're feeling like, hey, I'm not quite sure what compositionality

is. I'm not sure not sure. Well, these guys didn't either. So, it's it's kind of okay. Um, but what I can say is that the notion of composition has has nice for formalizations. So, in the since about the 1950s, there's been an appropriately parametric notion of composition that was formulated uh first in category theory and it was given this weird crazy name of a monad. um if you if you pair monads with their dual mathematical widget the co monad you can think of them so composition is kind of like nesting right it's like the Russian dolls you you nest you you know it's

like the the the the tree inside the leaf and the leaf inside that tree and the tree inside the leaf right so it's about nesting and and what what monads and coonads give you monads give you a way to zoom out and comon give you a way to zoom in on this nesting phenomen phenomena or this composing phenomena and lest you think I'm talking about abstract airy fairy stuff um again I'm just all I can do in 25 minutes is give you a few impressions right so so here are effective uh uh APIs expressed in the language Scala you can find similar expressions in the language Haskell just out of curiosity how many people code in functional languages here awesome how

many people use monads in their daily practice. Yeah. Quite a few less. Yeah. Okay. Uh but but the the the point is that they are an effective notion and they're a great way to structure your code even if you're not thinking about uh scaling blockchains. They're they're a great way to structure container code. They're a great way to construct uh to structure control flow. Um but it turns out that we can do better than that. So in particular, special K uh KVDB um looks at a duality between continuation which is the rest of your program. So let's say your program walks up to the blockchain and says I'm looking for something, right? And what if that something isn't there yet? What do you

do with that program that that is is waiting for data and can't go further, right? So in special K what happens is the rest of that program is packaged up as a piece of data and stored at at the place where you where it was looking for something right so that's the continuation and then data is dual to that and in fact you can have a notion of data integrity that that goes all the way back to the law of excluded middle right a or not a right that has to do with um this duality between continuation and data so at this location that you're looking for this address on the blockchain or in the case of special K it's a it's a more sophisticated kind of key but at this location you will either have a

continuation or some data and if if a program is looking for uh for data and it's not there the continuation will will be stored there if a program is depositing data if there is a continuation there that continuation will be woken up and handed the data okay that's the basic setup right now you can ask some questions questions about that setup. You can say well after the data and the program the continuation meet each other what happens and there are there are only a handful of possibilities. One is the data disappears and the continuation disappears. So they meet each other in this abstract space this this address

and they go poof. All right. Another possibility is that the continuation remains and the data goes poof. Another goes poof and the data remains. And the last possibility of course is that they they both persist. Right? So so what does what does that have to do with um uh traditional uh approaches to distributed applications? Well, if it well, if the data persists and the continuation evaporates, that's just traditional database operations. Think about a read, right? My program wants the data. I read it, but I don't get rid of it out of the database just from the read operation, right? That's that's

traditional database operations. If I publish and and uh and the the the publishing data is ephemeral but the continuation persists that's ordinary publish and subscribe. That's ordinary publish and subscribe. And if they if both of them persist, it's publish and subscribe with a history with a backlog of what you published. And finally, this is quite interesting. If they if they both disappear then you get item level locking in a distributed transactional semantics. So one API which I uh showed you nothing up my sleeves right one API

the the monatic API covers all of those distributed uh programming paradigms. So now how does this apply to the blockchain? Um well that that that how we provide that is that the continuation monad is the is the monad underlying being able to bring those those patterns together. Right? So we talked about this duality between continuation and data. Well, it's the it's the structuring of the continuations and the way we store them that uses the continuation monad uh to provide to provide that unification of all those programming paradigms. And and so we looked at that API. It turns

out that if you just tilt that API on its side a little bit, what you end up getting is the applied pi calculus. And that's exactly how special K is organized. So if you look at special K, if you go to GitHub right now and you look at special K, what you'll find is a little DSL that provides an implementation of the applied pi calculus. So but here's a little preview of applying that API to Casper. So I I spent last night and refactored this. I had good fun. Um so let's see if I can Can you see that?

That's That's all right. So, I'm just gonna again I only have time to give you a flavor. So, here are the files in the spec and let's take a look briefly at just some of them. So, in in Casper, the consensus protocol is organized around nodes which we think of as as validators. And what a validator wants to do is essentially uh receive blocks and then make bets on whether or not a block should be published to the to the um uh to the to the blockchain. And here's here's basically just an applied pyalculus spec

of the betting and the the convergence around betting uh spec uh for the validator. We can uh there are similar and you can see how tiny it is. It's it's teenytiny. um this uh this Wow, we're are already at two minutes. Okay, come see me afterwards and I'll show you probing this spec for properties. Okay, so I'll I'll I'll cut to the cut to the chase. So, I was going to give you a demo, but I would like to just take take a just come come see me afterwards and I'll I'll give you a lot more of the the

flavor of the spec and how how we can probe it automatically with the spatial logic model checker. But I would like to conclude by just taking you through a little bit taking these same kind of specs and using the compositional structure, we can walk this structure. we can essentially build up a new semantics from the existing semantics in a nice clean careful way. So I took the I took the uh essentially a variant of the applied pi calculus and I added to it metering and this metering basically uses three elements. So there's a resource there's uh there's and a channel for the exchange of the resource

and there's a channel for the next step. That next step is again an encoding of a continuation. And what what we see here is essentially just just a a tiny little harness for for running uh a metered uh VM. We run inside that harness the translation of our of our little tiny API for for uh contracts, right? But this this API and this contract language is a little different. And the reason it's different is because contracts can be uh uh executed in parallel. Uh contracts uh have have other interesting properties in that contracts themselves can be reified and exchanged.

Um the important point here again I'm happy to go through all the details with you offline but the important point here is the size of this spec and not only the size of this spec but the correctness properties of this virtual machine can be stated and proved in about a half a page. Right? So even more interestingly you can take this kind of virtual machine and bootstrap. So you can build this virtual machine on top of this virtual machine. Now it would be interesting to look at look at doing that with the existing VM. That would be an interesting question. Could we build the Ethereum blockchain on top of the existing VM? Does it bootstrap?

And that that that brings us back to the point I was trying to make at the very beginning. Do we have this self loop? Right? because that's your first and best test that you can scale. So the big picture that I want to leave you with is that is that compositionality this this kind of finding the small and the large the large and the small is the key to scaling any system. So thank you [Applause]