Simplicity for Programmable Money

Scale By The Bay: Russell O'Connor, Simplicity for Programmable Money

Recording: Scale By The Bay: Russell O'Connor, Simplicity for Programmable Money

you all right I think this is good thank you for joining me here I'm going to talk to you about a little language I've been developing at my place block stream my application here is a cryptocurrency and so I should look at a little background of the motivation for the design of my language over here so very quick background on Bitcoin and Bitcoin funds are guarded by small little programs written in the language called Bitcoin script and a typical program in Bitcoin script all it does is take as input as a digital signature and validates that digital signature against the transaction data and the public key associated with that those funds right so in Bitcoin it's not quite true that you send money to people through a cryptographic public key but you send money to programs and it just so happens that some of these programs do this cryptographic check right but other more complex programs are available to be programmed in Bitcoin script and we can do these things to create cross chain atomic transactions which allow you to execute a protocol that does a swap of currencies across different block chains we can build hash time lock contracts which gives payment if somebody provides a pre-image of a hash within a certain time period and you can extend this to do more interesting things so that the preimage is a meaningful thing we can build bi-directional payment channels where basically have a joint account with two people and an allocation of those funds between the two people and you can those people can update those their allocation of those funds offline so they can transfer money back and forth between each other without hitting the blockchain and then the lightning network is a combination of the hash long time trial contracts with the Bible directional payment channels put into a network to allow you to pay anyone that you can reach on the Lightning Network and there's lots of more things we can do right so basically the takeaway here is that Bitcoin is actually a form of programmable money so very quickly the way Bitcoin script works it's got this stack machine it has no looping constructs in it at all right so it's naughty it's not turning complete famously not turing-complete and this has some wonderful properties it allows you to have static analysis of the Bitcoin skip programmed for in particular you can bound the maximum number of each operation that is a is going to be evaluated before execution of the program because you don't have any loops all you have to do is basically count the number of operations that are going to be there right and in particular the Bitcoin protocol it rejects programs that have too many expensive signature verification operations [Applause] so and so this prevents a denial of service attacks because even before execution we know how many of these expensive signature verification operations are there going to be Bitcoin script allows the caching of results right because in Bitcoin script the evaluation only depends on the local transaction data itself in a Bitcoin transaction right it doesn't depend on the global blocks box chain structure so that means that you know if you evaluate a Bitcoin secure can you get a successful result that results no matter it holds no matter where that transaction actually occurs in the blockchain and its other parts of the transaction and data that will limit where it can occur so these are also very nice features a Bitcoin script but it's not all roses right so there's a problem many operations in Bitcoin script were disabled by Satoshi Nakamoto the creator of Bitcoin back in 2010 right so for instance integer multiplication not available in Bitcoin scripts so this really limits the expressiveness of what were able to develop or smart contracts for Bitcoin all right so this is all a prelude to to the motivation I have for developing a new programming language right so if I were designing a programming language for Bitcoin right from scratch what would it look like right so we want to create an expressive language that lets users build novel programs and these smart contracts in a flexible way we want to enable static analysis to bound the cost of resources of programs and we want provide to provide formal semantics for reasoning about simplicity for these programs using office it's a self-professed assistant so I call my new language simplicity and in this presentation here are just going to focus on the formal semantics of simplicity and and reasoning about simplicity programs or to illustrate how that works right so this is Emacs and this is the egged language that I'm going to implement simplicity in I'm not an e max user nor am I an egg that user so this will be fun for everyone so the syntax for AG des is very similar ish to haskell if you're familiar with that and let me know if anyone has any questions about the syntax so we're gonna do an implementation of simplicity in inside egg des over here as an example right so simplicity itself is a Combinator based typed functional programming language right let's do the focus on the types first there are three kinds of types in simplicity we have the unit type which we denote by this little this little one over here right it's the unit type it has exactly one member of that type right we have product types a cross B right so we have some pairing constructor that given a value of a and a value of b gives us our pair type for a cross b and that's defined by this data constructor over here and then we have disjoint union types over here right so we have a left tag constructor over here for a values and a right tag construct for B values and they both produce values of a disjoint union with B in so in particular simplicity doesn't even have function types which is bold thing for a functional programming language so is everyone clear with this notation for this okay good okay so let's start towards talking about the term language for simplicity every simplicity expression T denotes a function from some simplicity type that we define to some other simplicity type right so when we write it for an explicit expression T we write T : a turnstile B to denote that T is a term that has an input type A and type B right and so the semantics of simplicity is a function type so we just define the turnstile to be right and it's important to hear to understand that simplicity expressions always denote functions right simplicity cannot express values at all because everything in simplicity denotes a function all right so the core simplicity language consists of nine Combinator's and there on my shirt over here right and I have the the semantics on the back so all right but let's go let's go over the t-shirt in in egged over here right so we have an identity expression its input and output types are they equal the same and we can give it semantics and semantics is going to be the identity function now you might be familiar with type inference where if you give an expression you can infer the type but a neg de we also have program inference of given a type we can infer the program so let's just do that right it's the identity function there we go okay the next one is the composition Combinator right so if we have a simplicity expression s of type A to B and simplicity expression from a from B to C then we can make a Combinator that combines those two into a function from A to C right and that's just the composition operation I don't know why it says no solution found so we'll do it by hand like so so that's the semantics of the composition operation fairly straightforward we have a unit expression that is a function that ignores its argument that always produces the unique value of the unit type right so that's just this lambda expression over here for the semantics next up is the pair Combinator right so if s is a simplicity expression from A to B and T is in the simplest expression A to C what we can do is combine them together to get a function that takes an A and executes both s and T and pairs up their results over there and that's what this function over here does and we can [Music] sorry we can infer its semantics like so the take Combinator right so if we have some places simplest expression from A to C we can lift that into a simplicity function from a cross B to C just by ignoring the second argument of the pair and executing on the first argument right so AG dicta is going to need a little bit of help on here so we're going to do a pattern match on the input like so and it's going to return something and that something is T of X right so we're just running T on the first component drop is very similar it takes a simplicity expression from B to C and lifts that to a function from a cross B to C and we can run the same game over here we turn this into the input into a pair by pattern matching and infer the rest right so we run the Combinator on the second component the left injection Combinator in gel right given a function from A to B we can turn it into a function from A to B Union C just by tagging the output with the left Combinator like so so here we just run T and take the result with the left Combinator and similarly again if we have a function from A to C as a simplicity expression T we can lift that to a simplicity expression from A to B Union C by using the right injection tag like so and then finally the the the last Combinator for the core simplicity language is this a case expression so this is really only the only common a that does any work all right so if we're a pair and the first component of that pair is a distant union type what we're going to do is we're to do case analysis on that disjoint Union type and then execute a their srt depending on which tag we have over here right so we're gonna need again a little bit more help for egg duh so if we have a Sigma L a comma C and we return something and also if we have a Sigma R B comma C we're gonna return something else like so and in the first case we're running the s commenter on AC and in the second case we are running the t Combinator on BC right right ok so that's that's it and with these non Combinator's we can write any function from a simplicity type to another simplicity type this this is sort of complete for this class of types that we've defined so simplicity is to meant to be a target language of some sort of language that you would describe your smart contracts in right but we're going to write some simplicity directly even though we're not supposed to you just serve to illustrate how the language works right so we're gonna define the type of boolean's to be the unit type disjoint union with the unit type and we can't again we can't do values directly in simplicity but we can create constant functions which are a lot like values right so here we're going to create the constant function true so we need to produce a disjoint Union type we're going to use the ins right Combinator and it needs an argument that produces a unit type and here we're just going to use you know to produce that output and that's our definition of over there our true function true simplistic expression and we're going to define false the same way except we're gonna use the little in gel for false all right let's get a little bit more sophisticated a we're gonna put in a little syntactic sugar for the pair and Composition common areas using the little triangle operator and semi colon operator respectively let's build the not operation on bits right so we want to do a case analysis and in the false case we're going to return true and in the true case we're gonna turn false and this doesn't type check right because remember the case Combinator does case analysis on the first element of a pair and if we look here the first element is is not a pair it's this boolean type over here so we're gonna have to do something else before beforehand so what is that something else that we're going to do well we need to build a pair so let's build a pair of something in something so the first component of pair is the bit that we want to do analysis on which is the input value over here so we just use the identity Combinator here and the second element is just to be ignored it's just to satisfy the case expression so we're just going to plug a unit in over here and right so that's that all type check so we're good let's get more sophisticated let's do the or boolean operator so again we do a case analysis let's do the second case first if the first value is true then we can short-circuit and just return true like so and in the second case it's more sophisticated we have this unit lying around that we need to draw up first so we'll put that in and now we're gonna we have the second bit over here and so in in the case that the first bit is false we just returned the second value over here so we've put our identity over here and that's the definition before okay let's get really fancy now all right so we've had bits right let's let's form multi bit words right so we're going to recursively define two to the n bit words right so four zero four four one bit words which is two to the zero that's just gonna be a bit like here and for two to the n plus one bit words that's just a pair of two to the n bit word so for example to an 8-bit word which is two to the three is a pair of 4-bit words which is two to the two and that's what this definition that we're here is doing over here and now we can start going back to our digital logic course at undergraduate University we're gonna build a two bit adder alright so given two inputs we're going to produce a two bit output we have a carry bit and the result over here in the first case in case the bit is zero then there is no carry so we return false and we just propagate the second bit through in the second for the second half and in the other case where the first bit is true we have a carry bit if and only if the second bit is true so that's why we have the identity function over here and then we just flip the other bit over here right so that's the definition of a two bit adder and we can make a three bit adder which is called a full adder which takes three bits and adds them to produce a two bit word and so how does this work right so what we have is we're going to take the first pair of two bits and we're going to recursively run or we're going to call our outer function on those two bits and we're gonna hold the third bit for a while so we'll do that then after that so what we have here is we have the carry bit from our first addition the result from our first addition and our third bits hanging around what we're going to do is take the result and their third bit and add them together so this function here grabs those two pieces over there and calls adder again and here we just hold on to the first carry bit and then so now we have the carry bit from the first edition the carry but from the second edition and the result of the second edition and the way the full adder works is that if either we have a carry from either two editions than we have a carry for the full edition so we take those two carry bits and we put them together with or and then we just propagate our result to the second component over here and that's what's going on over here all right so that's our full adder over here but that was kind of questionable all right so is that really it's not really doing a full adder so let's find out right okay so in order to know whether it's actually being a full adder we need to understand what the meaning of these these these words are right all right so the words they mean natural numbers in some sort of big-endian or little-endian interpretation the words right so we're going to write an interpretation function and in the case that we have a single bit word that with the left constructor that's going to denote 0 and if it has the right constructor it's going to denote 1 and then if we have a multi-bit word we have high bits and low bits and the interpretation of that is the interpretation recursively of the high bits times 2 to the power of the width of the word which is 2 to the N in this case plus the interpretation of the low bits that's right there all right and this is a specification for a full adder it says that if we have bits a b and c and we plug them into the full adder and we ask for the interpretation of that that should be equal to the sum of the interpretations of the individual bits that went into the full adder all right how we're gonna do this well there's only 8 cases that we need to consider so we can just try them all to see if it works so let's do that and yeah ok they all work and that's that's how we prove that maybe that was a little bit too easy it's let's make a ripple carry adder alright so we're gonna take a 2 to the N bit word on a 2 to the end of that word and a carry in and we're going to produce the sum as a two-bit end bit word output and the carry out this is another bit hanging out over here right and now in the case of a single bit input that's just the full adder we defined already so that case is just a full adder over here in this this other case alright what we have is that the first input bit has look a high bit in a low bit and the second one is a high set of bits and a low set of bits so what we're going to do is we're gonna take the low set of bits in the carry in and we're going to recursively call full adder word on the low bits once we've done that what we have remaining is the left over high bits and the low bit of the result and this sort of intermediate carry value and what we're going to do is again recursively call full adder word on this time on the high bits and we're going to use that intermediate carry to propagate into the input over there and then finally what we have is we have the carry out the high bits and the low bits and we just sort of need to rearrange the brackets along these these pairs to put everything into order we do that there all right so that's our full word adder no did we really get this right let's try to find out so we need a little bit more of a helper function over here this is very similar to the meaning of function we had before which operated on words but here we're gonna operate on words plus a carry output bit over here and the meaning of that word is is basically the same meaning as before it's the meaning of the y-value and then the carry bit is the sort of the overflow value of 2 to the to the end if it's set over here right so that's that's the meaning over here and now what we're going to do is we're going to prove the specification of the ripple-carry adder right and the specification is very similar but this time instead of having bits we have two to the end it where it's a and B and a carry input C and when you plug those values pull with word adder and we ask for its its meaning it means the same thing as the sum of the meanings of the words a and B and plus the carry input C like that's a specification of a ripple-carry adder right so in the case of single bit and puts that's just the full adder correctness lemma that we had before so we've just rewritten that here that works fine and then I've put some preamble over here basically what we've done is that we've we have to prove this equation here o is equal to this thing over here and what we've done is this stuff here is done as filled in some intermediate helper functions right here so it says that we've defined C 1 and and our low to be the value of the sub call to full word outer word on the a low and below inputs and in the initial carry input and we've done the same thing for the adder of the high bits right so that intermediate value we just defined C to be whatever the result the carry bit of that operation is and whatever the result of that it is now of course these are low and are high it's going to be the low and high bits of the result of the addition right but this is just defining it we just know that it is a pair and it's just assigning those values over there right so we'll be using that in our reasoning and all right so what did I say let's begin we need to prove that something is equal to something else for some reason all right QED all right so this is the thing that we need to prove is equal to this thing over here in order to get this to be correct and now we need to give some reason it's so we'll just so this is a nice thing about functional programming is that we can do equational reasoning all right so this is how we formally do equational reasoning we cut and paste sorry oh oh Emacs help me out here all right all right so we're gonna make some intermediate step and we're just going to start doing like high school math so we're gonna rearrange this be high or here and we're gonna like move it over here and we're gonna add them together like so and then we're gonna take this a low over here and move it over here and fit together like so all right so that's our intermediate step over there all right how do we prove this well this is just true from high school math right so we say so if we need to solve a six variable high school equation and with variables a high a low D high B low C and said we'll stand for that two to the two to the n all right so it is true if it's obvious that a High Times said plus a low plus B High Times said plus below C that's obviously equal to a high plus B high times ed plus a low plus B low C like so all right that's obvious tada all right so let's just fill in these parameters like so alright first step is done next we have this a low plus B low plus C which looks suspiciously like this that's correctness level we're trying to prove and so we're going to recursively call our lemma to rewrite that as this is really the semantics this is the semantics of full full adder word of a low and below and see user extended its max there alright we're doing okay so how do we prove that well we need to use this conjugation to focus on some self expression that we want to prove and so what we do is we use lambda Express expressions to define which part of the equation we're going to rewrite in and it's going to be here and what we're going to do is we're going to recursively call full adder word correct and we pass an a low fee low and see see that's fine okay next we had this equation here that said full adder word a low below C is just by definition of c1 and our low is equal to that thing over here so we can perform this substitution of this EQ one equation to rewrite this term over here so let's do that so we're going to replace this with c1 our low good and so the argument is very similar we do a conjugation to focus on the part of the expression we care about which is this in this case it's going to be within the meaning function over here whatever done wrong oh sorry like so and we're just going to use EQ 1 in there perfect next up the definition of the meaning of this pair is c1 times 2 to the 2 to the n plus the meaning of our low like so and that just holds by definition right so we don't even have to give a reason why that's true it's just obviously true ok no problem with that and now a little bit more high school algebra we're gonna move this c1 over here inside the brackets over here and get rid of this and move everything over here like so good so why does that hold again we had its volts by high school algebra so I'm just going to speed things along by cheating like so put that in there and why did that not work let me come back to that in a moment and move on to the next thing the next step is we have this a high I think it'll become player if I keep on working we have that a high B high C one and again we can do a recursive call to rewrite that into full adder word of a high be high c1u semantics here alright and that again we use this conjugation operation to prove that and we have to give the context which in this case is right here and here the proof is full adder word correct do recursive : or lemma so this is on hey hey hi be hi see what and then again we do the same sort of rewrite we had before to replace this with c2 meaning OC to plot times 2 to the 2 to the n plus the meaning of our hi like so and again we use this conjugation except we're focusing this time within the meaning of this component and here we're going to using EQ 2 which is the second version of the thing that we were capturing before like so and then finally what we need to do is we need to pull this 2 to the 2 to the N you know in in over here to refactor it and multiply these together and we put into this zero alright so there's like all these complicated reasons why that's true and if you care what the reasons are they are these reasons here there you go down here alright and like so so other than my little gap that I've messed up over here oh I see this bracket should be here there we go fixes that and there we're done alright so we have proven that our full ripple-carry word matter is correct it has the correct semantics over there right so welcome to my life but this is cool right this is not something that programmers commonly do right they don't go through the effort of proving their program correct but it's something you can do with functional programming and this is what I've been doing with simplicity so we have a I put on a github my projects last night and so you can find certain interests there so like I said I don't actually use Agda all my work is done in Kok and then I have sort of this Haskell like prototype leaky of course you can't do the proofs in Haskell you have to do the improvs in caulk right so using exactly the same techniques that what I've described over here I've written the sha-256 compression function and again using equational reasoning proved in that the chat to 56 implementation in simplicity matches the semantics of the sha-256 compression function as given by the verifiable c community and this is nice because because we've formally verified this in postie program we can accelerate the evaluation and practice and simplicity because when you encounter the shot 2 through 6 compression function written in simplicity what you're actually going to do is not do the interpretation in simplicity but call into the OpenSSL implementation and this proof of correctness shows that that substitution is going to be sound right so there's like lots more to simplicity that i can't get to so that's it for now thanks for your attention [Applause] do you have time for questions if there's a question we have a little bit of time yes so the these proofs strongly rely on having dependent types and that is something that Scala and Haskell and oh camel do not have right and so you really need with hats with when you have GE T's like we have in Haskell I don't know about net Scala right you could get a little bit of the way there but to really read in the bro code like this you need the dependent types I'm not familiar with it so I guess I can't answer yeah I'm not familiar but yeah all right thank you very much again you