Using Yolc to Build Safe Ethereum Contracts in Haskell - Miao ZC

Transcript

[Music] All right. So, I don't have slides. I'm going just do some uh live coding. So, first of all, who am I? Uh my name is Meow. I'm a co-founder of uh Superfluid Protocol and uh I have been building uh Yoke. I would uh in order to build the next version of Superfluid Protocol. So, today I'm going to give you an introduction what is yoke and why I'm building it. So um what is yoke? Well first of all yoke embeds itself in HASLL. So if you're programming yoke it is programming in HASLL. So who here actually happens to

know about Hascoll or Pep? Great I have audience. Um so so probably this one is familiar with uh whomever already know Hascoll. So uh Hasll what is Hasll? Hasll is uh they have actually changed the headline if you visit hasco.org. or they changed the tagline is that now has for you is to enjoy long-term maintainability of software you can rely on. So it's for building things in longterm. I think a lot of things in uh on smart contracts should be oriented uh toward d towards that direction because immutable it should be built for long term right and other property of including uh statically typed and purely functional and very strong typer

inferences. So uh to learn more about more about HASLL uh if you haven't uh you can visit uh learnyouu ahascoll.com or visit h hasllow-links.org or the joyful.com/hascoll uh plus map. So just a quick example just one small example of what what is data type. Um so let's see a uh inspiring example is that that's something that you probably cannot do in solidity easily yet. So let's say let's redefine the U 256 that would be like in uh solidity like U in 256 right? So let's say call it the unit. So number of the quantity you are buying for for

example let's redefine the price as U5 256 also we also need time day time let's say U32 right? So a uh something called a algebraic data type. It's probably a bit m mouthful to say for for if you haven't programming hasll but let's see example right. So let's define something called a order. What is a market order right? So there are four types right. So this is soal algebraic. So means that you can have a choice between different type of uh uh uh market order. You can have like a market buy order. So I want to buy uh amount of uh uh uh amount of let's say token at a certain time a buy certain time like

expiration right you can have a market sell order um you can have a buy limit order right or you can have a sell limit order what is buy limit order by limit order is that you want to you want the order to be executed only at a certain uh limited price uh or uh or lower and conversely A sell limit order would be something that uh you buy um uh uh you you want to sell at a limited price or uh higher right so that's uh four different type of order in hasll you can define as like let's say you have a uh choice right you can it can be either of the four choices here so uh if I type in

my interpreter here so let's say I can do uh I can create data type like Mark now. Oops. So I can say okay I can mark buy order at uh 100 units. Let's type in random time. Okay. So you can have a buy order and you can have a different uh uh sell limit order limit order uh price at 42, right? Okay. So what's the big deal, right? So now you can do pattern matching. So in some of the languages might you might have that uh already built in, right? So you can say,

oh, is my order a limited order? So let's see. Okay, so if it's a market order, uh is it limited order? False. Okay. Uh what about the sell limit order is limited order? And now it's true, right? So now you can do pattern matching. So you can pattern match and say uh which type of order is it? Okay. What about what is a market price? Okay, you can think of market price as you take a list of orders and you start to coincidence want right? So you can cancel out all the market buy or sell order. you can uh check if the buy and the sell limit order they match each other. So you can actually write a function now in a functional way. Right? So I'm not going

to show the whole function here. You can think you know maybe uh solve this problem on paper and see if you can write this function in hasll. Right? Okay. That's a very brief introduction of one type one hasll feature. But why I'm talking about here we're talk we're in a Ethereum conference. It's not a programming language conference. Right? So why uh I want actually using Haskell uh for building on Ethereum? Well, it's about type. Type is good. Type is good for you, right? So it's really about type, type and type. So uh what a expressive type system can do is that it can make hard program simpler to solve, right? And it also has uh type safety, right? So type safety is built for production. So you don't have to write a

lot of tests because a type guides you to test uh um to express your ideas without having to write the uh a lot of tests. Um so we'll see some examples uh uh later. So um let me go to the actually the meat of the talk. So what is yoke? Um first of all yoke doesn't rebuild wheel because currently only I'm working on here uh on on yoke but I would like more people actually join the journey. Uh however in order to actually make the project practical I cannot rebuild the whole language and there's no point of doing that. So yoke works with solidity u what is solidity u uh solidity as a compiler actually has two components. One is that uh it's a surface language is uh uh everyone know of but actually uh it has it can build

to you an intermediate representation. So what yokek is doing? Well what is yoke? Yoke is actually a name play of sok right so is the compiler CI name s oc I I just called it yoke because you know they are similar name uh so what yokek does is that it compiles uh hasll uh uh two uh u language so let's see some example so first of all I a very simple example I define a pure function so in yoke I actually separate the pure uh function and the effectful function effectful function mean that it will be able to write storage call external functions uh or read storage right so um so this is a pure function so it

basically takes one two values and do a multiplication well it's too trivial almost right so but I can actually print out the u uh code generated by it in in my prompt here so I say print me the u code of this uh simple multiplication function right so I hope you can see it let me make it larger per perhaps Even larger larger. Okay. Pause error. What's going on? Okay.

So, well, it's almost too trivial to talk about, but that's that's a start, right? So, this function on the left side is a Haskell function. It has a type signature. Say it is a pure function. Take a U int 256. take another U in 256 and give you a new U in 56. What it does is do a multiplication. Okay, so the U code generated on the right side which is a U function uh and do a built-in function called checked multiplication for the U56 U in 256 values and leave the function. So this is a purely u uh code. It can actually feed to the compiler of solidity uu and uh generate the EVM bite

code. I'll show you the end to end implementation in a moment but let's go to a few more examples. The second example is uh a bit more over uh more than the previous simple one which is a function that works with optional value. uh maybe you know some of the programing language has a optional value in yoke we support natively has called maybe type uh maybe I 96 means that uh it's maybe a value maybe nothing right so it's just a value or nothing so now I can do a pattern matching right so the first value is a maybe value say okay I match a but I have two cases first case is okay it's a just of a the second case will be nothing so it's actually

optional Right. So let's see what the U code generated out of this function. So let's do that. Print fn again add maybe int 96 my favorite type. Okay here you go. So it prints a switch case in U. So the switch case one which is true meaning that there's a value and second case will be case zero which is a uh false. There's a default case. Why? Default case will be if you uh feed an invalid value because you know it's EVM exposed to internet maybe right so people can send a bad value so the default case will be a constant revert zero so there's no error message just boom revert just like in solidity

you do a revert uh empty square bracket uh empty brackets and that'll be the same so now I can actually translate the code from the left to the U code on the right yeah uh Which one? That on the right side. On the right side. Okay. Yeah. Sorry, I just uh is it okay still readable? Maybe I should just do this. Okay. So, uh if you are not familiar with U code generated yet, let me just give you a quick overview. Right. So, there's a function while there's a function name actually allows this strange symbol. It's just solidity lexical allows you that. So, it takes three parameters and I give a output. Why there are three parameter?

because VA and V_B actually is representing this maybe type. So there's a A is like uh is there a value or is there not a value, right? So there is a sort of a choice there. So it's all automatically generated. All right. So there's a different way of writing the the previous one. So I just do a quick example of that. So this one will be like for people familiar with Haskell bit more. So there's a funtor version, right? So instead of doing a pattern matching you actually uh do a fun mapping of the a and uh uh there's a function say this function don't care about if it's a m just a value or maybe a value nothing it will just do a uh fun mapping over there. So if you don't know

has other functional programming language maybe that's a bit uh esoteric but it's actually just a mapping a pure uh mapping a function to a funer value functoral value. So they actually generate the same code. They they don't. All right. So it's exactly same code. All right. Now let's move on to another example which is actually doing something useful which is uh uh do a storage map. So in solidity uh you would have a map of a key to a to a story to a value right. So here I have a similar thing. I say okay storage map from a address to a u 256. So it's a mapping from a address to a value. So

it's like similar insulated uh the mapping. So I'm going to get okay I'm creating a map with this as a key. So it's actually do a SHA 256. So this becomes a root of the key and with that root of a key you can uh sh with the address and then you can get a new key. Right? So let's see how the code actually generated. Um just remember that this is uh very similar to in solidity map address to u int. So let's see how the code is generated in U. All right. So it does a K chalk of the root key. Uh so what's going

on? Yeah. So the the root key of of this string is this big number there. And then you do a K chalk of that value. under the address VA and do a S load eventually. Sload is basically the storage load, right? So you you generate a key based on the address you feed and uh you get a new key and do S load. So from the left side of the Haskell code, you generate a U code. All right. So this is kind of a very basic uh uh overview of what you can do separating the pure function and the the so-called static function like in solid you have the static view function, right? So it's a similar thing.

Um now yolks actually work with the foundry. Remember I'm talking about that the yoke is not rebuilding the wheel. So I'm only build a Haskell uh surface language. So it actually work with the foundry. So let's see one example which is a canonical counter example. Right? So I'm counting uh values. Uh so I have a global counter to start with. Uh so the global counter is indexed by this uh string right. So this string basically gives a unique uh storage uh uh address somewhere in the storage uh sort of space and uh and I can increase the counter and I export this uh uh function so that I can call it in the solidity

testing. I'll show you how I how I do that. So this function basically say give me a u 256. I'll increase a global counter and by by a value which is a input here incremental value and I say okay I want to uh set this new value and set a global count I still I'm still fixing the syntax so there's some thing here maybe scary to look at but uh uh uh in in a um in a month or two I think it will be much simpler even to look at uh but let's see the solidity code how we test this right so solidity t. So okay so what you're actually testing for the global counter is that

uh uh I create a counter program. So this is actually hasll code I I created the the solidity wrapper over the generated EVM code. That's the counter contract. I say uh I want to randomly increase uh it's a fuzzing right I say uh give me a give me a b I want to increase the value global counter by by a and I want to increase global counter by b in the end I want to test assert that the global counter is increased by a plus b so this basically show you that the um the code is actually end to end testable now uh from hasll code all the way to the uh solidity the for foundry

testing right so it's end to end connected so perhaps let me show you the uh very briefly how the code is generate how the generated code uh look like so just to show you quickly uh actually I don't have it sorry just give me a moment um maybe I come back to that so if I go back to the counter example. So I'm uh so there's a counter object. There's four exported function.

So there's a get global counter, increase global counter, get counter, and increase counter. Right? So this is H hasll code. I say I want to export a contract that has four ex uh functions and uh uh I can basically increase counter um by uh by a value, right? So, uh, give me a moment. All right.

So this is actually generated code by the by the by the yoke right. So it generated this uh uh solidity code with you know with a lot of with a binary which is generated by the yoke that's embedded and then eventually become a solidity contract. That's how I actually can interrupt with the with the uh hasll generated code uh in uh foundry. All right. So, let me move on. Uh, because I'm kind of running out of time soon. Um, I'm gonna show you one most important thing about uh yo I'm building is I'm I needed a safety feature. Uh, one of them is called a data versioning.

I'm going to show you a magic here which is uh that it can detect uh um something called well detect re-entrance error. So, how is that possible? Right. So let's see a E ex EC20 uh example here. So I have a ERC20 uh function written in yoke or hasll uh that uh um let's let's say it's a mint function. I say I want to mint to a address amount of token. So what it does is that uh uh I want to calculate a new amount right.

So from the current balance to a new balance by increase by this amount I uh update the balance right so new balance would be something plus the mint amount and I have a something called a callback right on m own own token minted right I want to tell the own token minted function that uh uh there's a the amount of the token uh that's got minted so that's all right but uh but if I swap the order of uh of these two line there's going to be a re-entrance error.

Think about it. Right? So because the amount the new amount you are calculated you're calculating based on the value you read before the uh before the call back right so that value might be outdated. So right so you're reading the balance of the current account. So if I swap this line to here and if this callback happens to mint again then the value you read the balance before might be outdated if you follow right so let's see if I save the uh code now and see my compiler what what it says oops it says there's a type error what's going on right so it says

outdated data version so there's actually type uh catch that uh the value you are using. So let's say line 83 it says uh this this storage cannot be compiled because this new uh new amount uh using the data that is uh might be updated because in this callback it might call call your function or do whatever that value might be updated right so there's a there's a re-entrance possibility and the compiler is very conservative to say well I refuse to compile this code because the data you are using is from different versions So there's a data version in here. So this is one of the safety feature that I

use has to build which is in type level make sure that you are using the data that it has to be uh up to date right so it becomes a type error if you use a data that is uh outdated so if I can't change order again uh everything should compile again similarly uh I have a I caught a similar error in in transfer right in transfer if I transfer to myself if the from address and two address is same. It's actually also type error. Unless you do a check that you are not uh the the sender address and uh message sender is is different. If you don't do that check, you might uh end up situation that the value is uh uh

outdated. So if I use a incorrect code and it's also a type error, right? So, [Music]