Towards safer languages for smart contracts

Transcript

[Music] hello everyone uh my name is Robert this is Jack and uh we're currently working on our Master CIS in computer science and uh we're working on a new programming language for the evm and so we're here to talk about how smart contracts can be a perfect fit for a dependently typed functional language and why we want to do this uh we will also have a small example of uh how an expressive type system can help in contract development so when you deploy a smart

contract to production uh you want to be really sure that it behaves precisely as you intended to um so the more the compilator can catch for you the better so we also want to give developers high level abstraction uh of standard behavior and common patterns stuff like high level cryptography and boiler plate for errors and cleanup and I hope that after hearing Greg this morning uh you can appreciate that a language that allows for compositionality of combinators and functions can be really powerful lll is functional but it's way too low level for a lot of purposes uh so without further ado Jack will now present two

types of errors that programmers usually make when they start developing smart contracts and how we can catch them at compile time right so we look at a simple example game of rock paper scissors that's played for money uh joining costs 10 ether and the price is 20 because there's two players uh and I hope you know the rules but it doesn't really matter if you don't uh and here is a small example of uh how the function that lets players join the game could look it's very straightforward um it's the game can only be be joined if it isn't full uh

the player has to pay the fee and if both of those are okay we just save the move and the address of the player and yeah the move is just represent this Z one or two for simp uh so this for a regular programmer this would seem quite reasonable but there are actually a few bugs here um so what happens if a third player attempts to join the game he would lose all his ether and there's no way to retrieve it so let's fix this um this is better but there is one problem left uh since the blockchain is trans

arent the first player will reveal his move to the second player we'll not solve this now but keep it in mind later so just a quick recap there's two uh classes of error that we're focusing on that's very common for developers that's getting into smart development uh what we what we're trying to do is to use an expressive type system to help identify and solve this and to to do this we are including both ether flow and cryptography directly in the type system so if we want to encode ether flow in the type system what can we do

well we can start with including the transaction value in the type signature like this and as you can see we we have also put a precondition on the value saying that this function requires at least 10 ethers to be executed uh otherwise the transaction is considered invalid for our purposes and all ether is automat automatically returned to the sender and this is certainly neat but it doesn't solve our problem our problem problems uh but as you can see we actually already know uh the functions result success and the transaction value value this is actually enough

information for us to specify spe ify how the function should should handle ether in all execution pths so we just take the return value and do a conditional check on it that's the question mark and colon there as you probably recognize from imperative language languages uh if the player was able to join the game we should say we should save 10 ether and return the return the rest and if the player wasn't able to join the game then we should send back everything and don't save anything now this type signature actually causes the problematic implementation from before to be a type error that's catched at compile time

this is quite amazing because it allows us to uh eliminate a large class of bugs without doing any testing or formal ver formal verification whatsoever this technique can actually also be used for by contract developers uh to specify the behaviors of their contracts but that requires a little more a little more work on the part of the developer so we won't go into this uh but we still have the problem that uh the move is disclosed when it shouldn't be the way to solve this is to use cryptographic commitments they basically allow you to commit to a value and then

reveal it at a later time but Developers shouldn't Implement their own crypto each and every time it's tedious and very error prone so the way we solve this is by annotating the types of secret values as you can see there with commit um this indicates to the compiler that this value should be treated as a commitment and the compiler will automatically generate a function for the sender to review it at a at a later time when it has been revealed it can be accessed in Code by using the standard

Library open function which takes any commitment and Returns the and Returns the value if it hadn't been revealed previous to calling open uh then open will fail return all e to the sender and abort execution uh so our final type correct implementation would look like this note that we are forced to explicitly save all ether that we want to keep because otherwise it was wouldn't compile and now Robert will talk about how we intend to implement this thank you so some of you might have

noticed that the syntax we have used is very similar to ascal and when we first started looking at this we had the idea of of making hll on the blockchain basically but the more we looked at U these problems and how they could be solved we realized that dependent types would be really cool to do this uh also haskill is lazily evaluated which becomes prohibit expensive in real life on the evm as it is now and then we found Idris uh Idris is very similar to hcll but it has some key difference uh first of which it is dependently typed uh and it has side effects is

model with Al algebraic effects so these two things combined is what allows us to have the neat uh uh expressiveness in the type signatures that we saw before and Idris is also strictly evaluated from the GetGo so we don't need to have make any changes there and as a nice bonus we don't have to venture down into the murky depths of the GHC API if you're familiar with that um so I hope we have shown how dependent types and algebraic effects can be used together to define the flow of ether throughout execution of a contract and we'll see how we have seen how high level type annotations can

ensure that secret information stays secret until it's supposed to be revealed and we have a language where compositionality can can be achieved in a natural way so where are we currently with this well we still have a long way to go before it's actually usable in practice to create working smart contract bite code uh we have created models for how we want stuff to look for the developer and made sure that all the properties we want to enforce can be enforced using addresses type system and we have just recently started looking at uh how we can create a code generator that will take that will go from midis to lll um in a similar way the serpent does it

today and that's it for us thank you