Invariants Testing for Smart Contracts in the World of Medusa - Joshua Adesanya

hello okay let's get straight into it we don't have much time so smart contract uh testing uh very interesting do have as as Foundry I know a lot of us here we use Foundry right great so we also be looking at something called invariant uh we're going to have a very short code um work through and then we're going to jump to the rest of it so testing smart contract testing I know we have a lot of web two devs here you know what testing is during testing what what does it do unit testing so it's a kind of test whereby you are you are testing a trunk of a code base so let's say you have a very large code base and you want to know what is happening in a specific function that's a unit test integration it has to do with o I want to I want to know how this like two three four functions in a particular context how work together but the emphasis on this my presentation today is actually on invariant testing and if you're in the smart contract world I know you you have heard this once or more than once so what are invariant invariant are basically properties so when you uh develop a smart contract there are conditions in which must stay true and these conditions are what we refer to as invariant there are things that no matter what happens in your contract they must not not change it must remain the same do we get that because we're going to we're going to need it later on it must not change so those are what uh that that is what I am referring to as invariant and like I said a lot of us we are familiar with Foundry Foundry is a framework that uh we are actually used to actually build our our um smart contract you can do a lot of things there you can code you can Falls and a whole lot of thing but today we'll looking at Medusa Medusa is uh basically a uh Frozen framework it does just one thing and what it does is fren but you can also F on Foundry but in addition to that you can code you can run your test and do all sort of things uh in Foundry and Medusa also does one thing Medusa Works across across board Medusa Works across board so you can use Medusa with Foundry you can use Medusa with ad and all one can you guys hear me very well okay great I'm trying to rush through so we can made up with the time so when it comes to invariant in smart contract we have two types of invariant we have the function level and we have the system level like I said we're going to check this in the code base so the function level invariant are just like unit tests they have to do with a particular function but the difference between a function level invariant and a unit test is that you have the opportunity to actually uh play around with a large uh value so for example if I want to do a unit test for a function I have to impute my parameters so X is a x is 10 B is 20 but when I'm foring I don't have to specify what x is I don't have to specify what Y is the force the forer is actually going to uh pass uh passing a whole range of values so it keeps trying zero try with one try with two try with three depending on the type that you're using with it so which means that I can easily know that oh if I'm using an unit 256 as uh my parameter is actually going going to start from zero to the max does that make sense okay system level on the other hand has to do with the old system so when you are building uh a protocol when you bu a smart contract there are stuffs on a level in which must remain the same and in the codor we're going to do we're going to see some of them uh for example if you actually um if you have a mass deposit which are going to see in in the code workor if you have a Max deposit of let's say 1 million in in the protocol you're developing and then you say this is a Max deposit that I have to that this protocol can take and then when we start depositing start depositing funds you can actually have a system level inv Varian that says that that uh the deposit must not actually exceed that Marx dep that's that's a system level it means that a lot of things need to happen people need to deposit you're not taking at the at the function level but you actually going a step further to check it at the at the um system level we're going to understand that better so let's jump into the code straight up trying to increase the font or you guys can see it very well is it clear now okay so this is a very simple smart contract called savings what what can you do in this smart contract you can you can deposit you can withdraw and you can get interest perom I think that's clear enough hello is that clear enough you can deposit you can withdraw and then you can get interest perom and then we have a couple of interesting varable we have a Max like I I mentioned before we have a mass deposit amount we have a minimum deposit and we have a couple of mappings we have total deposited and blah blah blah so what are the invariant in this uh small contract so this is this is going to give lighting to what we have been talking about so the first invariant is user deposits must increase by amount added after deposit does that make sense user deposits must increase by amount added after so when a user actually deposits uh a particular amount into the into the protocol when we check the balance of the user inside the savings contract it must actually increase by that amount does that make sense number two user balance must decrease by amount withdrawed so when a user decid to let's say I want to withdraw a particular amount from my savings when we check it it must it must actually see that the par amount we withdra is actually equal to when we actually check the balance right does that make sense the third one is that deposit must not exceed contract Max deposit example I made before so if we check the go back to the contract we'll see that we have um a constant Max deposit and then we have accorded it right there so we are saying that in this um one of our invariance is that no matter how much once we get to that amount we don't want use that to Depo it again so that that's this is a system invariant we also have another one that says users must get interest uh after after every year so at the end of the year every time was able to get interest perom and then the last one uh says that user must be able to withdraw at any time so this is where we go into Medusa like I said you can force with uh Foundry it's quite straightforward you can do that but I guess I also mentioned Medusa it's a Fen framework it does not that's the only thing it does so it gives it that uh very interesting uh uh feel and then you know that all what I'm doing here is Fring you can you can go to um on uh on Google and search for Medusa uh you can add Medusa Sol it so you can find it easy and you can download it and start using on your laptop so what what are the things that we need to do to start using Medusa so the first thing that we need uh is to identify the invariant it's very very important so Medusa does not have any strength without your invariant and like I mentioned before if if you actually want to force you need to have a LD understanding of the code base you're trying to force it is not magic so okay okay so foring so the short and is f so F I'm I'm actually going to show us so what we mean by fing is that we actually uh we have let's say we have a function right and then that function has the parameter X and Y that were passing into it on a normal day if we writing a unit test we're actually going to pass in 10 and maybe 20 and then we run it through but when you are froing I I don't need to pass anything to it I just leave it at X and Y so what the Fring engine or the Fring framework does is that it actually generates that X and Y value on its own so it doesn't just do that it actually does that for a wide range so for example he can do that for let's say x if we using inity if you're using something like maybe unit 256 you can do that from zero to the max ofit 256 so your your need your unit test is actually specific for a particular scenario but when you are fing you actually fing through the spectrum of all possible values does that make sense so what invariant testing takes it to another level because when you are fing like I said there's a function level fing which is one I just explained now but system level is that okay a lot of things happen in this system we are actually depositing we are withdrawing we are getting interest what are the uh properties of the system that must always remain true so we can also go as far as actually checking those level and making sure that it's always true and like I mentioned uh we have two invariants here that are actually very very important the which is the system level um invariant we have the ones that say that deposits must not exceed contract mark deposit you can say you can't really test this with just a function because a function means one person is actually just just doing one action it's something that you may need about maybe a th000 transaction plus before you can actually get to a point of testing this so it's not really physically possible for you to do like to test this so that is where uh Medusa comes in so as I was uh explaining we have a couple of things to do I'm assuming that we have we're going to get Medusa and we're going to install it I don't want to go through all those so identify the invariance it that's the most important thing that's the most important thing you have to identify the invariant it's very very important is when you have your invariant that you can now start using um the uh fing framework that you have so the next thing you need to do is the the one of the first function that you run when you actually want to start is Medusa in it we're all familiar with in it so what it what Medusa in it does is that it creates this J so this is basically a uh where you actually put in your properties that things that you like settings for the old fren suit and there are a couple of interesting things here I'll just touch in some of them uh one of the one of the very important thing here is the Target contract so this is me just saying this is the contract that I want you to actually use uh for the frosen I'm still going to show us this so just note that TI contract very important another thing that's very also very important is the c post directory this is where you going to check your coverage so Meda also give you gives you uh a kind of um way to check that because it is possible that you fing but you fing wrongly just the same way that you can test you can do right youit test and you are testing rubbish so you can actually F and you have a feeling that oh I'm fing something I'm doing something I'm a fer we are not doing the right thing so that is where the coverage comes in so you can be able to see ex you can see what is actually going on there so another interesting uh thing that uh Medusa does is that it gives you the uh the ability to actually include more than one users so when you are doing when you are fing in let's say Foundry or some other uh Frameworks you can you you can only by default you can only f with one user at the time so you need to actually write some a lot of ball ball plates to actually Force but Medusa actually come I can even add more currently by default it comes with three you can say sender address you can add like as much as you want so by default when I run this my fors on on Medusa is actually three users are actually doing all those deposits withdrawal and all three users by default but I can add more and so on and so forth we can check the rest let's go straight into our FS test so this is the folder in variant and I'll just go straight to savings there are lot of things I not mention but I want to just go through the core of it so the first like like we're saying here it's just like a smart contract like it's just like normal contract that I'm writing but this is actually my uh fren uh contract so the four the first thing I did was I imported the savings that we saw the tokens I'm using inside the savings uh um Medusa has a cheat um a cheat sheet that you can use for things like pranking that we are familiar with in Foundry and they added something called total balances for my test so the first one user deposit mod in increase by amount added after deposit which I mentioned right that's my first in variant and this is a test for it what did I do uh the first thing I did was me some tokens to the user ms. sender prank the user approve the amount for savings I'm tracking the total balances and the first thing I did was get my pre- balance so the reason I'm getting my pre- balance is so I can have a point of comparison so I get my pre- balance save the money get my balance after deposit and then I do my assertion which is after balance minus pre balance equals to amount does that make any sense I'm just trying to check that I have deposited this money now and I get my my uh my balance so when I subtract my balance after I balance before I should be able to get the amount actually deposited right so and then I'm testing with the assion and if it goes through that means if it remains true that means the test passes so that is the first invariant the second inv variant is the withdrawal so we going to notice something here that I'm not doing anything I'm not trying to like do the deposits or anything I just go straight into withdraw you're going to feel like what's going on so which money are are you actually trying to withdraw when you have not deposited so Med does something interesting that it calls all those functions like all these functions that we have in this fire it ca them randomly cause deposit cause withdrawal cause so what b what is happening here is that when when I call this test deposit here and I'm passing Ms sender remember I mentioned that we have multiple users so it it call all those users randomly cause deposit so the user already has some amount cause another one has has some amount then cause another random user and cause withdraw does that make any sense so it's do in such a way that it's not really it's not straightforward it's a magic it's not straight for so in that way actually mimicking real life uh uh scenario is that fine is that clear okay so let's go to the next one so withdra is basically just withdraw some amount and then like we did for the first one we get our pre- balance we get our after balance and then we check the assertion to make sure that we actually uh withdrawing that that particular amount okay so this third level uh which is the system level depos must always must exceed contract Mass deposit this is one is very very straightforward all I need to do is know the to the total deposited in the contract and make sure that always it's always less than or equal to the max deposit does that make any sense so in the if we go back to our savings we discover that there is a there's a um variable total deposited which actually tracking the total amount of tokens that all the users in the contract are depositing right and in my in my test here by test I'm trying to say that okay in this contract I want to make sure that the total deposited is always less than or equal to the max deposit in which I I've said that this is the max number that I want people to deposit does that make any sense so this is a system um level invariance system level invariant okay the okay so in the test with draw we do the pre we're doing the pre- balance so I know you guys I I'll talk about this total balances later on so then I'm doing the withdraw cranking the theage of sender then doing the withdrawal then getting the after balance that's all the deposit is coming from so like I said Medusa does this uh stuff that it cause all those functions randomly it cause deposit cause withdraw cause everything that is in this um contract so that means that user probably already has a deposit when it calls that me Center you are seeing actually is like three users randomly being called so already has if it doesn't have it's going to fail on the on the back end it's not going to tell me it's going to fail until until the user actually has a an amount before he can call the the WRA so it's actually working very fine so you don't need to actually you would have done that if you doing a unit test you what you're saying would have made sense but now we're actually Frozen we are not restricted so what does it just calls them randomly at the point each of those users will actually have some deposits and then they can withdraw does that make sense okay so I think the mass deposit is very straightforward and then we also have the get interest which will actually whopping the time so those that are familiar with Foundry they know what w so we basically just increasing the time and you can you discover that in all these things that we are doing we are not specifying amount manually you can see like I mentioned before the amount is just there hello the amount is just there we're not doing any uh 10 eer one eer so every time that you CA deposit it actually just putting any amount randomly so let me run I think my time is running so we have get interest it does the same with time and like I mentioned you need one year to be able to like get an get a particular interest but in Medusa because we can actually W the time and we can get time randomly we just run random time and we can run through it and then the last one we have the test I have enough to pay deposit which means that at every point in time in this protocol we the the contract must be able to pay deposit and I we checking that or checking that by making sure that the total balance inside the savings is always greater than or equal to Total balances which was this you guys notice I've been tracking this to balances and I did that in okay no I'll R up okay okay so I did that in the test deposit and I did that in the withdrawal so to track when the user is actually depositing and when when the user is actually withdrawing and that give me the opportunity be able to actually test this let me just run it let me run the test so we can just see one or two so the the command is Medusa fors and when I run the command I mean the dire the pressure yes real okay something is not right okay okay I think I know why I deleted something that is erroring out okay that's fine without this we have not done a demo yet so wow what's really happening don't worry okay so it's running so we got see it cut the first one and we can actually trace the the uh the part you can see in test Max deposit it means that at a point in time uh the invariant for test MK depos actually fails why is that and we can also look through the uh the sequence that is been called you can see it called test deposit and it calls test Mass deposit are you guys still with me so if we actually go through the function we are going to notice that the uh get interest is actually going to be a problem because uh we don't have we're not actually uh putting any uh extra funds into the protocol so by the time the uh by the time the the the part it start calling it calls the get interest we're actually going to take part of the phones that uh that supposed to be for the normal user and but the actual uh issue that I actually caught here is the issue of um max deposit which means at the point us deposited more than they should because when we look at our savings dots so we discover that in the deposit we're actually not checking to make sure that uh the users have actually gotten to the max deposit so this is one the other one is one I just explained now so I guess I have to stop here I hope you guys enjoy my talk thank you so much thank you very much