# Building a Formally-Verified DApp with the Reach DSL, today! by Jay McCarthy (Devcon5)

- Channel: [Devcon](https://streameth.org/devcon)
- Date: 2020-10-09
- Duration: 45:07
- Topics: blockchain, smart contracts, distributed ledger, ethereum
- Watch: https://streameth.org/watch/yt-WR50p7LXQ9M
- YouTube: https://www.youtube.com/watch?v=WR50p7LXQ9M

## Description

Visit the https://archive.devcon.org/ to gain access to the entire library of Devcon talks with the ease of filtering, playlists, personalized suggestions, decentralized access on IPFS and more.
https://archive.devcon.org/archive/watch/5/building-a-formally-verified-dapp-with-the-reach-dsl-today

In this hands-on workshop, we introduce Reach, take participants on a walkthrough of an example program, and guide them through implementing a basic DApp on their own. 
Reach, a new domain-specific language for decentralized applications, provides automatic solutions to the key problems faced by blockchain developers: ensuring the smart contract is consistent with client-side software, verifying the DApp is trustworthy, and abstracting over different blockchains.
We then take a guided tutorial consisting of an example Reach program that implements a formally-verified two-party wager DApp. We explain the structure of the ~50 line Reach program and the structure of the ~50 line JavaScript frontend, and take a deep dive into properties that Reach formally guarantees.
Participants will then work through a series of exercises implementing a different DApp with a similar structure to the sample program. They will leave with concrete experience using Alacrity that will enable them to build their own DApp.
Prerequisites: Experience programming in JavaScript, have Docker installed on their machines to install the image of the Reach compiler and demo. It is recommended participants download and install this image before the workshop at:  https://bit.ly/ReachIsTotallyAwesome. Experience with formal verification or stating DApp properties is NOT required.

Speaker(s): Jay McCarthy
Skill level: Intermediate
Track: Developer Infrastructure
Keywords: technical

Follow us: https://twitter.com/efdevcon, https://twitter.com/ethereum
Learn more about devcon: https://www.devcon.org/
Learn more about ethereum: https://ethereum.org/ 

Devcon is the Ethereum conference for developers, researchers, thinkers, and makers. 
Devcon 5 was held in Osaka, Japan on Oct 8 - 11, 2019.
Devcon is organized and presented by the Ethereum Foundation, with the support of our sponsors. To find out more, please visit https://ethereum.foundation/

## Transcript

[Applause] and has a copy of the slides and is all the codes that will be raining today if you watch all along and you can start from the initial version where we've written the entire reach part of the program and it will switch and then the final code will be the I don't want this our target for the end of the day so if you wanted to run a business how to use the English right now we have dr. and dr. compose result and of course how about music music so you want to go to this site and then from the base directory villain Tuesday final write in Greenville run then that will make sure that you have all these velvet if you want to all along if you don't want to follow a just do this later and there will be value and experiencing the rest of the show our team is because we were able to attend and then maintain McCarthy so Christmas Carol entrepreneur's had a lot of experience in the space and my background is that I am a research professor at the University of Massachusetts well and I'm also one of the developers of the record program language so a racket is a list based language that's very popular as far as list based programming languages go it's commonly used at a lot of colleges universities and my research has mostly focused on doing verification of programs for calls and there so the reader product the reader project really represented the culmination of my research now our goal as an organization is to try to dramatically lower the barrier to entry to watch so we think that there's a huge amount of potential in the space but right now it's just too complicated to build real apps and our goal is by building something here oh no that's 40 miles now its pipeline is that we want to solve three problems we want to abstract over the decentralisation important right now here it is extremely productive is probably there are many people who believe that there's problems with aetherium and other and other platforms but it's too risky to invest their time if you rate your product and reach and you will be able to compile to different platforms we are trying to we're trying to live up to the rate was running many business the next thing we want to solve is that we want to make sure that the that the depth that people rank are trustworthy so a major important what we'll be talking about later is the way that is integral to the operation of compiler and the way that we've progressed finally part of being trustworthy is ensuring that there is consistency between the expectations of contracts and expectations of compliance and it needs to realize that in the recent languages that it is not a smart contract English is a bounty which we're going to break their program in this one because you get the clients that will and there's a guarantee the verities now there are some interesting techniques that we use design and I'll talk a little bit about that before we focus on trade now one of the ways that we get the abstraction of being able to provide to go to many defensive centralisation platforms is that we have a very straightforward constraint model of what working provides all right is that we're thinking of the bunting as providing common knowledge about a monotonically and those those attitudes might say they really like constrain all the ways that we look at contractor plans to provide the contract is this repository of knowledge and the clients react to that information and attempt to add things to it if necessary and so what our main feature is another principle that we use inside of reach is that the reach language performs a lot of sophisticated analysis on your code at the most basic level we have a sound tasting as you can expect in the modern language in addition to that however we have announced these that are particular to the needs of deaths as a one little example one of it we'll see later is the way that reached uses information flow security to guarantee this information that is known only to it does not share without being explicitly transplant now the way that we do verification is that we take the program written in reach and be converted into an estimating problems SMT is one of the classic problems with either science and there are many extremely reliable on an apparent purpose legacy that can plug not I think discharge and so a major part of the way that the structure it is to make is that we can produce as our goal is to provide any during the process so if that means that they have to be able to discharge all the publications automatically and the only way that we can do that is have any ideas now we have a lot of different kinds of properties that can be expressed inside of these programs at the highest level we have basic systems level property relation between all counts think of like if you're programming the C program you never want to have a nullpointerexception and you don't actually need to know anything about the program that you're running to know that it should have that property so slim early part of reaches tool automatically synthesized companies like this would make sense for all others on the other hand we also have the ability to break down particular properties of relevance or one application in the same way that when you're writing the C program you'll have a custom assertion they make sense program so we have the same letter instead of reach and again we'll talk about this later now the next thing is that as I mentioned the reach language provides specifies the entire program we use a process called any collector Junction to extract each of the individual pieces of the program out again I'll talk about this in a moment so that's kind of a roadmap of where I want to go and the switching dive down now what does they actually want one thing which is that reach is the culmination sorry is the revolution of another DSL that I've worked on previously another company making open-source products called a blacklist and that other language is called integrity and the library is also available and has diverged development different features in the electric 11 language as the reason language and I very happy to talk to anyone about what those differences are but I want to make sure that I acknowledge they so now what I'm doing is I'm going to switch and go over to the repository so in the repository we go into the initial directory and this is the code that will be working on health can you open this there's been a lot of order fix stuff that's to make it so that it can run effectively let me just comment a tiny bit about this before we open I'm going to clarify so we need installation to make it to us as easy as possible for all look it is everything is entirely talked arrest so these run the application certainly when you compile them even it compiles it into a docker container that you can that money that docker container is automatically configured to a testamental but it also so you don't need to worry about that party testing similarly you don't need to download any download or install anything like a regional pilot the regional pilot is the shelter of redundant bottom which is eight lines it configures so there's a lot here that's gonna make some of those things all together but we are going to be inside this file right here multi-state not our name that's gonna be our meter man here's what we're going to start off this so in the rich language you are writing in a subset observers so the syntax is exactly the same syntax as JavaScript almost all normal JavaScript features are available and they mean roughly the same thing that there are many so for example let's start by talking about what we're going to build and what the overall model of engagement is we're going to build today is an abstraction of a multi signature wallet the key idea of a visual wallet is that many people collaborate to pool funds and then when they extract those funds other people have a say on whether or not the extracting happens so we're going to distract that idea to two accounts a parent and a child the parent makes a deposit on behalf of the channel and the child can attempt to sedate withdraws it must be explicitly approved by the parent so this is not a product that when we're done today we're going to launch and become blocked and leaners this is an abstraction of what kinds of problems people to solve it on the blockchain and it's small enough that we can do it in minutes 30 minutes all right so the first thing that we want to do is you want to specify that this protocol involves two different part participants a child and the parent it's either each language one of these you do is you specify each one of the parties and then we'll write one program in this main function and this main function is going to include the behavior of all the participants as well as all of the smart contracts so the first thing that we'll do is we'll have the child and attach to the contract we'll do that by having the child make a publication now the end of watching is there's this monotonically increasing data structure of the history all events or attitudes in this case we think about that as being a publication to all of the other parties so when we call child publish we're saying that it's the child's responsibility we'll publish this information now it turns out that there's actually nothing originally it's just the way that they're in now every time when you expect to see a message on in the vertical we have the same what would happen if the person who's supposed to do this didn't do it what if they what if they time on prices and so we always specify what would happen in the case of the time out and typos are expressed in terms of how many blocks you're willing to wait for an accession so we're going to just have this variable and program delay which is going to say the message has kind of comment in delay seconds and if it doesn't then we'll fail and the way that will fail is that anyone as well as underscore means anyone is able to submit the message and what this message does is it will commit the transaction and then say that we have finished writing the curveball and the reason that I'm returning this array of turin zero is because at the end of the protocol when we're finally done we're gonna return how many times the parents said yes and how many times the parents said no so if the child times out and never joins and we're done and so no event actually happened now after we do this now the code has transitioned down here and we're now inside of the contract so at this point we need to verify anything that must be true above the publication now in this case I think was actually there's nothing to say so we commit the transaction and now we go back to a context where we're outside of the purple the idea of the reach language is that you switch between local blocks where a particular agent or many agents are simultaneously doing things and then synchronization or consensus works and in those consensus works all of the parties are doing the same thing and they agreed on all the information of let's do an actually interesting example so after the child has joined the protocol we now want the parent table so a parent table only so this is something that only the parent they do now what do we want them to do we're going to have them run a function and so we'll specify that as a function of narrators and what they'll do is they'll compute what the allowance that we're going to give us now notice that this is a circumstance where it makes sense that the at this point in the parole the parent is always going to decide what the allowances but in our reach program like how do we know what you do clear parent are going to give to Sally before she goes on her you know it's big trouble how do you know well there's two ways that we can do this the first thing is that notice I'm here when I wrote when I defined the parent I said and this empty object right here so in this spot you can write and at every print that that participant starts the Protomen so we could add in here knowledge what the initial step will do though is that we will interact with the front end so we interact this is a special object inside of the reach language that represents the client it will ultimately run the parent part of the world so we're going to take that object and we're going to call allowance on it now let's convert our net value and we need to assert that that value is going to be an integer now this value right here we want to eventually provide it so we'll go next and we'll say parent not publish the allowance so we're going to publish to the rest of the world that the allowance that that child has access to is this number now unfortunately if we try to compile the program right now it is going to fail and it's not an ability because I have this time here it's got a billion records that the reason it's going to fail is that this program fails to satisfy the information flows of dreams the reason why is that all the information that comes from the client comes from the front end is assumed to be standard information it must be it classified so we'll do we'll call do you classify MS and another Declassified in we're allowed to watch it okay now the next thing that I want to talk to you about is how every time we make a publication we can combine that with a unit of value that we transfer it to so so will actually pay the allowance and will write down the time code so every program every interaction on the chain must be accompanied by what would happen if there's a timeout we refer to this property as kill safety the idea is that your program has to be safe with respect to any participant refusing to engage in the protocol at every point going forward so in this case what we're saying with this time of luck if we're saying what if the parent never did this problem what should happen now do these early stage of the protocol there's really nothing interesting to say that's why they just had but in principle as we go forward there's going to be more interesting interrupts they're going to happen all right so now at this point you're now inside of the contract the contract has access to the allowance and you need to go forward the thing that we want to do going forward is what to have a little well and this little while loop is going to repeatedly allow the child to ask a buzzer so we'll write about now what is the condition that's going to tell us that we're done well the condition was going to tell us that we're done is that the balance is going to be zero when the balance is empty then the program will be over now Alice Bob something like special variable that we're not going to we're going to keep track of the balances okay so we're gonna say that well the balance isn't zero continue running this part of Seoul define a new variable call the balance it's going to be equal to the allowance no just so that we have something interesting to return to do is we're going to keep track of how many times you said yes and how many times you said no running the program so how many times the child asks for money and the parents that way we don't this isn't that important you just keep adding something and then that's the information that we're going to return at the end okay now there's one last thing that we need to do and it's actually kind of a big thing when you're doing formal verification and you have a value the while loop represents a point in your program where many many different things to cover there's an addition of this program that runs where you reach this point in the allowance with zero and since the allowance was thrown we never execute the code inside of here and we go right to the end there's another version of this program of this program executing where we run the inside of one time then after running it one time it all balances fun and then meetings there's another version we're gonna run it two times sometimes so there's some times an infinite number of different ways to run a program that has a single level I don't know how many times you go around the mouth so it's a big problem how are you gonna know what the program will actually do because the way to think it's a way to internalize what program is is you're making a prediction about what the program will do now one way that we could do this is that we can automatically take the program and verify it for when we went 0 times verify Poneman 1 verifiable 1 2 3 4 5 6 7 8 9 10 etcetera and what we would be doing is we will literally be like copying piecing this code inside of the verifier over and over again to verify each one of those different versions that's called interject evening and intimidated is what to do in situations where we can't figure out we do not either instead we have a programmer specify a loop invariant now if you remember from your analysis of algorithms course we're you to use the CLN respo excuse computers I hope you've probably learned a lot love with veneering and if you're like me you hated that class and it was very frustrating okay mostly I do have a little bit Marion is what do you know before those nerves and what you know again another thing that we know is that the balance in the contract is equal to this balance okay and anything that we do inside of this that and will not be like will not be allowed to compilers and what this is gonna do is it's gonna allow the compiler to make it to verify this mortgages we're gonna verify everything above this to make sure it establishes Levin great we're gonna verify the inside to make sure that preserves it then we're gonna verify the end and then also air but what this means is that we provide complete nerve agent behavior of your program by just proving three smaller girls it's not let's go inside and do some stuff so we were in kind of the context of the consensus so we have to commit the transaction and that will go back to the world where the two participant do something and then they want to do is want the child to do something or something where she's gonna ask for a certain amount of money and we know that this money will start be classified and it's going to be a number and will interact interact with a customer sorry-sorry the front end to request the money and the way that we're gonna do this they said we're gonna tell the front end how much money is in the account it's okay you know know how to display to the user yeah Sally do you have a hundred dollars of elders how much do you want so this internet object is not only a way to get information from the front end it's a way to share information so it's a two-way street essentially what's going on is that this breach program is specifying the API to the contract the API to the clients sorry that they've got to the backend then we'll write up some client now the next thing we need to do is write an assertion that's gonna say that how much had better be stronger than or equal to the balance because this program would make sense in that production business function right here is one of the verification assertions that we can put out I mentioned before you can go look at the slides that you might enter that there are different kinds of a search assertions are things I always want to be true if they're not refusal in compile assumes are kind of like require insulin where we obviously check this property at runtime but the other thing that we do is we make sure that all the assertions later on in the program are entailed by these assumptions so later on in the program were allowed to write down a service and if any ascertain would fail because you forgot one of these assumes then will refuse to compile the program the idea is that we're guaranteeing consistency between the clients and the contracts we're making sure that your program at runtime actually verifies all the properties that are necessary for your contract to run so now what we'll do is we'll have the child publish mmm then animal ready the time ability and the type of food will be a lot of available to the parent to run and if she fishy times out then we'll just say that it is an automatic dignity so it's not an it's not a yes or a No but we just continue the purple so what happens here is that rather than returning at the end we say that all of the variables that the loot is iterating over they stayed up in the statement and then we continue to the next generation if we wanted to we could say that if the time what happens then it like goes in favor of the of the child that she had for me they talk to us and we do this by the way is one of these one of the one of the examples that the reach language is different from my earlier project the elaborate language because they have that pretty language the timeout locks are automatically generated upon ear and a half they're not able to but also you don't have to specify what they do so they automatically enter protocol to get all the money okay so now we're inside of the contract and we will require that how much is less than the balance so this vertical only makes sense going forward and how much it is not more than that once now it looks like what we're doing is we're saying something twice we're setting about here coursing event here and of course we've literally ripped down how much less than miles two times what we did it for totally different reasons what we're doing right here is we're saying that this protocol makes no sense unless this is true what we're saying up here is that I am a bad client if I don't check this properly and you have to specify both of those things if you want to have a current program because you're writing down the client and you're writing down the content and one of the thing we'll do in the verification process is make sure that the contract only interacts with good clients so if we left of this line and this line will fail to verify and it'll say that because of course in the actual and like your actual project you don't want to submit a transaction and how that transaction will fail because you failed okay so then we'll forget the transaction and now we're back to the local context and we'll have to parent oh I know this is approved in this case we'll get back to moving because the interact on there doesn't only the turn numbers can return arbitrary information so will the interaction will say all approve and will tell the front end here's how much she asks for it here's what the remaining balances then what we'll do is we'll publish that and we'll have to deal with what happens if there is a timeout and we'll do the same thing as before where is that if there is a time of the parent never gets around to it and in this case we'll call that a note okay so now we're back inside of the context 45:34 the contract and now the contract knows the balance it knows how much money was asked for and it knows whether the parent degrees so at this point we can actually make this transaction so we'll say if the approval is true then we'll transfer how much to the China and we'll update our state areas say that the balance is less than that how much we'll say that there's been a one that is called yes and no notice and then we'll continue and otherwise what will do it will say that the balance is unchanged okay is unchanged but there's and we'll continue and then at the end we'll need to commit the final transaction when the balance is empty and then we'll return the OTAs in the mix okay so we just fruit 63 lives and I hope that it belts not to beard it doesn't feel like rating saluting it doesn't feel like writing a smart contract it feels like reading the whole done behind the scenes what we're going to do is we're going to automatically synthesize the front end code and we're about to synthesizing a contract out let's go to the terminal and see what type of a name and then so we'll take make building and what it's going to do is it's going to run the compiler oh I made no mistakes so I don't know about you guys but I'm a master and a lot of the time my students make mistakes when they write paragraphs okay this is why you shouldn't hire them to write their verified compilers you should hire me to write over first time now let's me go back for a moment and look at what we read now what if we made a mistake so obviously this it would be totally stupid but what if we accidentally subtracted how much and then added one there's no off by one error in our program now I've never made not that whatever program but I've heard of it okay let's try to compile and see what happens I'm suspicious that maybe it's not looking in smile hmm okay I'm really nervous one of the one of the annoyances with doctor is that sometimes doesn't copy ok hold up talking about that for a moment what I'm going to show you right now is what we make what the compiler produced so if there's an adult directory and we'll look at the saloon because it was generating so right now the reach language can in principle produce things other than a theory but right now the only part of the theory this is the contract that came out so this program this contract is come certainly laborious embers so there's 100 nod2 lives you can look at if you want to send them to the Builder everything right in yourself and let's just look at like one little part of it so let's look right here at message six so message six is a message that has all these parameters and let's try to see if what's going on so it says right here that it must have come from a zero that the block number is less than the delay going in there the value has to be 0 that's one of the messages that doesn't have a payment with that over these 17 has to be smaller than to be aimed of least 17 that's how much he ate was the balance then what we do is we commit that and then update the state so with this messages this event number six is the six thing in our program which is this step right here and this publication right here when the child says here's how much I want and when you go to the contract we require that how much does my eye care I realized by the way why the by that allowed us to comment on that line because actually commented out the line that that was the assertion rather than the line that made sure the assertion was right so I believe that if I comment about this one all right now I'm not really nervous though Hey sorry okay so now let's look at the image options that they generated so this the structure could have generated is the code for the child so we get a new it's called child that takes as an argument that hand over the contract will see this given a leader and the interact object and then it goes through and it has each one of the pieces of the program so just make a new window we can compare the two of them so for example look at the first one that took the child does the child calls requests on the Internet so the very first thing is that we published nothing and then we're going to wait or the parent to publish the allowance so we look at the code the very first thing that happens is that the child sends and then receive special message one with no information expecting to receive event one afterwards or event two of those entitled there was talent nobody do is mean to you or both remember we expect to receive event three and event three comes with these five this that will end up being the allowance okay so this rest of the curve right here is you know no code that a human would ever write but it's very straightforward about compilers it has wonderful things like let V 9 equals 0 because let's be 9v9 is the count for how many times we said ok alright so now what we've done is we've written the bar for every reach we've compiled it behind the scenes it's done verification for us and we now have the Johnson poop and we have this ability code but this javascript code that we have the only thing that it does is it provides these high level up these high level functions to spin up a child and twos enough the parent may skip down there's a limit parents and then we also and then you know the details of the contract know we have eight minutes left so we're not going to break by in the front encoder instead I'll show you the front so what I'm going to do is I'm to go out of the app directory and go is the minimal directory and don't look at the index MJS file so the first thing that we'll do is we'll import the standard library we'll import that noticing for them well Sid our starting balance and then to be we're going to test assignment and then we'll scrape a new account for the parents that have that starting balance and then that's going to deploy the W parent unemployed then what we're going to do is we're going to define the internet project and for this first version I'm gonna say that the allowance is always going to be fifteen there so I just write this function that money that when you get that pause with allowance I return to the beaver now if I we're making like a real application you know I might have a pop up for ever and oh you mean like actually do a real interaction with music then remember our approval function and our cool function this is a really nice parent aircrew function is true okay because this is just for testing purposes okay then what we'll do is we'll define a logo that will run the parent function so the whole month is it but can't give it this contract object that you might have to play into that interactive function and then we'll get back a promise for the answer that will eventually come out of the parent when it's done right and to do something similar to the child will start it off with the balance and just because I'm lazy in this test I mean to start in exactly the same so and you have some money to provide the gasoline then the child will attach to the multi-state contract and when you attach versus deployed he doesn't say what the address of the contract is and when it was created you need to know what it was created to the you know they're not sending people now the child it's gonna say I'm ingredient Island what I want to do my request is everything and then we'll ask for it he apparently will wait those two in there let me just pop back to the comment over to turn over here and we'll make run finding out that that meant starting get waiting for it to be around I mean this the texture here that's actually running it really nervous in my life demo now ended and it said apparent up there okay so what this coach shows us is that we have 28 lines and we're able to take our noticing program that we wrote and write the rapper front-end so this code is the minimal amount of traveling code that we would need to write have something useful in to take this structure right here and you can build your unit testing library for this between there now now let me show you one more version that does a little bit more interesting stuff so what this person is gonna do is it's gonna be 41 lines so it's like twice as long and we're just going to do is it's my two messages about what's happening and other that's gonna be different is is that the parent is going to say that you can have any time you ask for money as long as you can ask for less than half of what's left will say yes spatulas you can ask without much much as and though the child is going to do it as a child is going to ask for a random amount of money that is divisible by 8 dollars life it's a liar why am I doing this just let it over to love life the child particularly asked for random lots of money and needs until eventually it gets down to the point where there's only I think one eater left and then it will end so this new version of the permit is going to be more like exciting to watch we're gonna mean but really all they're showing you is that I'm not developing that happening work I'm making a user interface I mean the policy for what the parent doesn't mean you can policy or what the child does be here is an automated policy but you could have it be instead not automated one the one that's right by and we'll build in - and I love and make the text a little bigger so you can really experience okay so they deploy the contract okay that's great put in 50 ask your not okay but one of this come in look at all this money this right now it's like there's lots of times actually have paper and then it's ready for a while this is gonna get down to the point where there's only one left it's gonna take a while we get positive payments awesome plus the parent said yes 13 times and no 13 times the child so what we did today is we wrote an entire down from start to finish in 30 minutes now I program there's no point at which I said here's this complicated solidity idea to a Titan call or is it transfer it is supposed to be send let me go looking at Stack Overflow question again these are the kinds of things that are done that are decided before you correctly buy them from Heather one point the next thing is that we verify that the data is trustworthy or at least we would have my doctor configuration was writing copy the files correctly so you want out send you well then we'll post a link to a version of this this walkthrough where we show the verification condition was failing and then and it ensures that the clients and the contracts rating system art for T lying reach program produced 300 lines of front-end Java code and so the code and the details of those two programs have to mean the mentalist be connected with one another to make sure that it executes correctly now obviously you like everything pretty simple 300 lines that has to be right if you broke a real program not this little model there is help right now we have our data that has many different many constraints later but and we have a release plan for over the next year to expand the 72 though I'm very grateful for you to come here please check out our website realization is look it up on Twitter and all the social platforms you should really check out an Instagram account I've got a really cute cat and finally I just want to see exercise and reach was only a project that I worked on that's based on the same principles and so thank you so much for your time [Applause]