Pure Functional Solidity for Fun and Profit / Miao Zhicheng

Transcript

foreign [Music] thank you put here instead okay uh yeah thanks thank thanks for

people coming here for the uh rather technical talk about pure functional solidity for fine profit um I just want to like how many people actually familiar with the idea of functional program just so that I know all right great so uh let's just get going um so the goal of this talk is uh to demonstrate the possibility of limited functional programming solidity and uh the second is I use a new paradigm to build a simple super token step by step so it's going to be involved and I'll try to go uh write speed but a bit short time the third one is examples of using certora to formally verify the code right I don't say it's a complete down by the the just exploring the

possibilities and last if uh is uh if you are not familiar with a functional program yet is to make you interested in functional program in general right so okay so let's start with today's uh task or or idea is how let's reimagine what is a token right so let's have a new mental model of what is a token let's call it super token for now right so token is like a bank uh containing a collection of accounts right that's how we know about even erc20 tokens right each account has an owner representing the owner's wallet with a collection of let's let's give a abstract name monetary units not to be confused with

currency units we're talking about just abstract units right so and each these monetary units provides a balance right and a set of payment Primitives all right so let's have this mental mode and move on and see what what what's what's about right so what is what are payment Primitives right let's give four of them and they have two Dimensions one is one two one transfer one is Instant versus a constant flow right so we're all familiar with one to one instant that's erc20 transfer right that's one just one thing in that in that two two by two Diamond uh boxes there's one to n instant to all the accounts there are a lot of ad hoc projects that are doing doing that but

let's say can we generalize as sort of a payment primitive so we want to one-to-end instant transfer that is one-to-one constant flow of money right often known as money streaming by by by people right and uh the last is the one to end constant flow how about I distribute uh to any number of people as flow of money right so that's so-called a generalized payment flow a generalized payment Primitives right okay furthermore what what can what Karma come with this uh generalized payment uh from uh Primitives and the new mental motorizer it's also frictionless what does it mean so it's real time so it's a

model that continues in time right so it's in fact because blockchain moved per block so actually it is moved per block but it's modeled continuous in time so it's real time true real time right the other is composable right so it can be changed with other payment Primitives so the moment you receive the money is a moment you can use the money right so it's frictionless in that sense there's not you don't need to wait for the money accumulate and you transfer as a batch later right so it's uh using at the same time you receive right so programmability also right so there's two uh programmability one is own chair mechanism right so let's say include a callback so when you receive us the

money you act on it one of the examples DRC triple seven but uh you can generalize it if you receive a flow of money then you trigger a callback that's something that's kind of own chair mechanism there are certain things you cannot do own chains such as uh reacting on time right you can't do that on evm yet right so uh when the certain time hits you do something for example right so it's not doable so you have to provide off-chain incentive when the uh in that kind of cases right so a little bit more thoughts about super token before move on actually about the main topic which is functional programming is uh uh monetary units you can think of as uh coins cards or notes in your wallets

right so optionally uh you can you can think of like new txo based system or home chain representation of account could be kind of complete bypass it's no longer wallet but just a bunch of notes you can do that in your in your UI instead all right okay let's now have this mental model in mind now let's build it uh using solidity right so uh but we'll not do all the future we'll talk about so far we'll talk about online uh the creating those payment Primitives also for Farm disclaimer this is not for production right so just for fun right so first of all let's define some types right so there's something called custom types

already in insulated I don't know if you start to use it or not right so this is what you can use for wrapping numerical types and from 8.19 there is something called operator overloading also so yeah you can actually make it more convenient to use uh by using that so let's see an example right so first of all let's define something called time in this case the time is uh Inked 32 unsigned and you define two functions pure functions uh for ADD and subtraction and the last line is the 8.19 new feature right you can do operator overloading where you you say okay you say the plus operator is using this function and the minus the subtraction operator is using

this function so this is uh the new syntax available from 8.19 so with this you can then actually use the custom types in a more ergonomic way right just syntax sugar but it's it's very convenient right let's define more types right so you need to have value unlike the es20 value this is assigned also right so there's a positive and a negative so it's Inked 256 uh similarly uh you define the ADD and sub and you apply the operator overloading also right so now that is flow rate in this case let's say it's a 128 bits instead because otherwise you know it's gonna overflow you know it's there's only two five six otherwise right so very similar

code then previous one let's move on quickly uh unit uh we'll talk about what is Unity later it's really about about distribution think of the dividends payments you need to have a sheer number uh in traditional like how many shares you have Microsoft share twilio share whichever and those are measured by something called Unit so this is gonna the type gonna be handy later all right so or however solidity doesn't have a operator overloading when you have two types that are different so you kind of have to go back to the old way using a library say if you want to multiply the flow rate by time and you put it as a library function and then you uh you use

use kind of keyword using this library for the the flow rate globally right this way you can then have a Operator by name of a DOT Mao right so multiplication so this is uh uh you can't do mix type so unfortunately you have to do this all right so next step let's define what is actually the uh the uh the thing we're talking about here right so we need some some sort of a data type for for doing this very specific magical token right so with uh there's three things there's a time for that data structure and it's very abstract and it's called a basic particle or we will see later Y and there is value and there's a flow rate

with three Fields uh you can call okay before before I go uh further right so there's something in the solidity about functional programming is that uh it's not really pure function why because it's similar to JavaScript or some of the language that uh when you have an input of of the memory uh data type storage indicator you can actually modify the input right so this is uh not really a pure function in that sense if you're if you know what is actually the pure function you can modify the input which is kind of bad right so uh for the functional programming perspective so what you really need to do is do a clone so you whatever input you receive you

clone it so you make sure that you don't modify the input so we keep that pattern throughout the uh the coding right so make it a purer all right I didn't check the time so I'm gonna move on fairly quickly so now we have a small data type now we need to calculate the uh the balance from the data type right so it's it's very straightforward uh it's a one line I say okay flow rate multiplied by the Delta of the time right then you plus a something called a settled value then effectively you have a calculation of what's the balance of the of that data structure right so it's got an rtb right a real-time balance uh another very abstract function you

want to settle is because uh it's a very important uh kind of construct throughout the code in order to make sure that uh when you do operation between two data structure they are synchronized uh with the same data structure at the same time right you settle to at the same time otherwise they don't they're not compatible let's say or another way to put it if they don't if they're not settled at the same time you cannot do operational topics so let's call it settle right as you can see there is first operator is always dot clone so you don't modify the input data or talking about a functional programming you always clone it in solidity unfortunately you have to do that so that makes a little bit boilerplate but not too much right you

clone the data you calculate the real-time balance is the second line of the function calculate the balance settle it and put the time in the Third Field right so okay now go to the third um step right one other thing about a functional program is that you will you define bunch of function but how do you know if those functions are correct right so you do now need to Define uh some laws for it right so laws what are the laws right so laws are mathematical laws right so let's let's define something called a monoid it's a if you are in a functional program you probably know what uh what I'm talking about here but uh it's it's actually a

very simple concept so it's uh the data structure we talked about there has additional operator let's call it a X or has a some name called a append and satisfy certain laws what are laws very simple right so you there is a empty elements multiplied by any number adding any data is equal to that data it's like a like zero plus x equal to X or one plus one multiplied by x equal to X you can do different order left or right so if you come have a left and right so now we have a Foundry based test property based testing right so you have any random input and you test if the law satisfies with any order you have right so multiply by

append from the left or pen from the right you get the same equality right so that's kind of Foundry basically testing right so the first thing uh to test this law that's always a test but this is one convenient way all right another is associativity right so you a a multiplied by B multiply c equal to a multiplied by B multiplied by C with the different brackets uh locations and in the function is also very clear one liner right so you check if uh if if it gives the same data uh you do a kind of with different uh uh brackets applied to the data structure right so it's very easy to test right that's a common mathematical

property for the data for a lot of data especially for data wants to append to each other uh but uh the data we've just defined also has its own laws right because we're talking about some domain specific stuff uh something is kind of it's called there's a set of function right so if you settle twice they should give the same result right so it's kind of ident potent so let's call it right so actually the fun fact I ask chargpt can judge gbt generate to the function if I just give the function name actually generally pretty okay uh it doesn't work uh fully but uh it doesn't understand the word and it understands what uh what it what it what it means right so uh because in principle it's

it's a second formulas I just settle twice with the same time is equal to settled only one time right so that's basically what about this is not very interesting yet the the next interesting one is what actually about the the the the the constant flow of money right so you actually then test uh the real-time balance is always uh the same no matter how you settle it right you have three times them here now in The Foundry based testing you have a T1 T2 T3 and you settle with a different order then you calculate the balance at the same time they always equal right this way you can make sure that the function you define actually makes sense according to this law right so Foundry again provides a very nice facility for testing this very

concise test you just test the uh the property and if you put random inputs and uh it will give you 1000 the data points and it all works then you're happy right so right uh I'm gonna speed around now the number four step uh we'll talk about one to n also right how do we model the one two and now we need a new data type right let's call it the pool of money right let's look at the pie chart imagine that okay I need a data structure can represent an ownership of the pool of money by different owners so so let's say that each pool has members and each member owes some amount of units and anyone can distribute distribute money through this pool of

money to its members and these distributions can be kind of instant or as flows and members share of the distribution are proportional to kind of a number of units relative to others right so uh this is a mental mode of a data structure uh let's just Define it okay we have this kind of basic data structure we defined a few slides ago now we just wrap it into three two on the left side two different uh new data structure right so you say the pool has total units and you contain a wrapped information that wrapped particle is actually measured per unit and then you have each member each member say how many units I own and the where is the

settled number I have there and uh what's my synchronized position of that now you have two data structure and essentially done you have you have now a one to end how right so again you need to Define function that we defined for the basic data structure now we Define what's a real-time balance for this function right it's also very very concise this is a kind of Hallmark of functional programming right so you just Define pure functions different data structure different really really small functions and you gradually build things up and you'll get what you want right so as you can see here the art real-time balance function for that pool is essentially a few lines right you say oh the I need to see the difference between the Raptor uh one and the Sinker one you

multiply by the number of units this member has and you know you plus this so-called separate value done how do you come up with this formula it takes a little time but once you get it it's short and it works but how do you know it works right there's something called said to us about let's move on how do you know it works remember we talked about laws right so in order to know if it works you basically test with the same law we're talking about there to see if these new function you created satisfy those laws and the good news is they satisfy right so now you know you created something new and they satisfy the same law and they work right that's the good news about about that's kind of why you should do functional programming because then you just create data create

function test with loss and step by step and build things up and yeah I'm having a hand waving here I just trust me it worked uh right so now uh not finished yet now we have data structure now we need to go to the something finally right so we're building the token right we're not there yet step five uh five minutes all right so we need a shift and flow right so we need to shift the value from uh from two parties from left to right and we need flow uh money from left to right right so that's called two Primitives and uh in solidity I have to do twice this for different uh data structure on the left side is uh

two basic particle on the right side is on the left side is us on the right side you have a basic particle is a and you have a pool which is B and as you can see they are very very similar functions uh uh looking right the body of the function is very very similar almost identical right it's not a coincidence let's see another example right then you have a shift flow right they're almost the same they're just different input types A and B they are just slightly different type signature but the structure of the function is almost identical right so this is a something that insulated they are going to be introducing as far as I heard from last year they're going to introduce something called generic programming so

that means when solidity have generic programming I don't have to create the same function twice because they are essentially the same what we need is General programming so that I can write one function and they can work for both different types because they you can just duct tape it right duct type it packing JavaScript you can you don't care about the type of it you just say oh if your function just works right so we need a similar thing kind of in solidity right then we don't need to create the function twice right okay so now we have laws for for the uh for the new function right so insulated I want to show you one trick in Foundry rather it's a little different Foundry so I have a generator uh function so it takes two functions as a point as an

input and I can generate uh tests based on the operation one operation two they are abstract function sorry they are function pointers and uh this is kind of my template to generate more tests uh what do I do right I use I then I use that generator function to create four different test case a set of test cases I say uh it's a shifting shifting flow flow flow shift shift flow I've now all combinations with the generator function right so this is something that you could also do in solidity with function pointers and then you generate the bunch of uh the tests using that right so uh all right now where are we now we can do shift we

can do flow and if you shift from Two basic data structure you get the transfer you have to turn transfer and you get a one-to-one flow and if you do the shift for the basic data structure and the pool then you get one to n both instant one and both stream one right so as you can see it's using functional programming to build stuff from bottom to up you build you have basic data structure you have a complex data structure but same function and you get the uh uh you get you get all all the functions you need all right so I'm going to get a functional you need it right so okay now what right so we have a

we have a library pure function Library that's not it does a lot of things but also at the same time nothing because it can't really change storage can't do anything uh so like what do we do now right so let's call it uh the the the infamous m word if you know the function programming that's kind of the most ready to work because no one can explain it right so uh what but let's focus what do we need we need a reusable code that use this the library we just created to build these tokens right so um I'm gonna fast charge sorry for if I if I can have to jump jump a little bit right so uh so let's go straight here right so what

we can do is we create abstract function has a has a function that say I want to flow I call these pure functions and then I want uh actually modify the storage right that means I have to define a virtual function and then do all the tricks right so this how you create a kind of reusable code for for using those uh those functional uh pure functions and uh well the implementation in the token so this is not a final code in the token.flow you will see okay I use the only important part is almost in the end like underscore don't do flow and uh then you then you have it

all right so there's another trick unfortunately I can't show you here but just see this this is actually solidity code didn't see the last line right you have the dot Set uh sorry this one uh the last part is you can this almost exotic code is like you can do shift and Dot flow it's like a chain of function calls right so it's a re-implemented the uh the same token flow with uh with uh with a slightly different uh uh ergonomics how you do it right so what we have achieved so we now have a solid have a solidity pure function library for implementing a token now we have a two variants of the interface that uh for using that code and uh right why it matters I'm gonna jump real quick

because people are waiting and uh so what is function program it's really about Implement as much code as possible using data definitions equation and logic formulas and to make code actually useful I need to have the kind of computation strategies stuff right so what why it matters I suggest you look at this paper called a y-functional program matters that's really really old paper but it's 10 pager and it tells you why it really matters right so the keyword is that it's for better debugging reusability and less maintenance costs right uh the main point I want to actually bring out is that with this data data with with this kind of a way of building

stuff you can actually make a form of verification really easy right then you can have the uh in in the search Torah you can have this Define the rule we say this property we're using Foundry to prove it always work not only with 1000 data samples but also mathematically always works there's another magic from certora is that uh it can inductively prove that uh something always works throughout the the state of the program all right okay so I'm rushing a lot here but uh thank you for listening yeah