Invariant Testing WETH with Foundry

Transcript

[Music] foreign cool uh hi everyone my name is horse facts you can find me as horsefox.eth I'm also eth call on Twitter or you can visit my professional website terminally.online I'm a smart contract programmer and evm Enthusiast and excited to talk about invariant testing wrapped ether with Foundry today thank you so this is going to be a Hands-On

Workshop if you want to get your hands on so here are some setup instructions we're going to be using Foundry today a build tool and a development framework for solidity if you haven't used Foundry or installed found Foundry you can follow the the commands here to get that installed and then there's a GitHub repo that has all the code examples from today's talk and some additional bonus content in there if you'd like to use that you can also hit that QR code up in the corner to to reach the GitHub repo uh inside that repo you'll find a readme that has kind of written content of all the contents in today's talk and you'll find some tags in there as well that you can check out to follow the code examples along the way we're not gonna

going to use those too far in depth today but you can sort of use that repo to uh to explore as we go along with the talk and I'll leave this up here for a minute if folks want to to check that out while we talk about the the goals and agenda uh yeah so the goal for today's talk is really just to get everyone up and running with Foundry and variant testing this is kind of a broad intro to how to use the tool and hopefully people by the end of this will feel comfortable writing your first invariant tests in Foundry that's not necessarily an overview of you know Advanced Techniques or detailed in variants today and we're going to use wrapped ether a real world contract with a important real world place in the ethereum ecosystem as a motivating example and this is a good example because it's kind

of a simple a simple contract uh it's uh erc20 contract with a few a few extra methods that we can use it's a good motivating example for today um and yeah we'll be able to use that throughout this uh this Workshop so agenda for today we'll talk a little bit about what invariant tests are and discuss how they differ from unit and fuzz tests we'll take a quick look at the wrapped ether contract itself how it works and what we might want to test in the contract we'll look at setting up a Foundry project for invariant testing we'll walk through to hopefully testing three invariants uh conservation of ether solvency of deposits and solvency of balances along the way we'll look at two common invariant testing patterns one called

handlers and one called actors and then if we have time we'll look at testing our own tests using mutations and I think we're going to use all the time we have so here we go uh cool so what are invariant tests and how do they work in general I think of them as a kind of super fuzzing that are built into Forge if you've written Foundry or Forge fuzz tests before the concepts here are are pretty similar if you haven't we can go over unit tests fuzz tests invariant tests in turn here so here's an example of a unit test you can see we're testing addition and in a unit tests we're typically testing local Behavior with a specific input and a specific output so in this example five plus three equals eight so we're usually

testing one component we're choosing specific concrete inputs and usually focusing on a specific function and specific behavior uh if you're a very rigorous tester and test driven developer you might pick specific concrete cases in your use tests that sort of drive your code forward right like edge cases specific values uh as you're thinking about which concrete values to test but as you write unit tests even though everyone should write a lot of them hopefully everyone's familiar with them you're never really going to cover the whole range of inputs and outputs that are possible in the domain of your functions right you're sort of picking very specific cases uh they're interesting and useful to you I Like This Acronym in unit testing called zombies which stands for zero one many boundaries interfaces errors S I use

Security in solidity but as you're you're thinking about unit tests often you're picking these specific concrete cases concrete inputs concrete expectations uh we have this metaphor I hear a lot in testing right that your unit tests are a safety net they'll catch you when you fall um but I think it's kind of a bad metaphor in some ways right unit tests are really like you're climbing a rock wall and you're hammering little pizzons into into the wall or something you're picking these very specific uh very specific points out of the entire domain of your function to test so a fuzz test another form of testing and Foundry is kind of like a parameterized unit test so in a fuzz test we're testing the properties of of one component typically local Behavior but now we're testing it with random inputs and instead of an

expected concrete output we're expecting a specific property in this test so local Behavior random inputs expected property so in this case we're still testing addition in this code example but here we're testing the addition is commutative right so a random value for a pick a random value for B and we're going to assert that a plus b is equal to B plus a uh so yeah when the fuzzer runs it's going to generate many random concrete inputs for this test it's going to verify that the property we've defined here holds for each one of those inputs and fuzz tests are kind of a broad category they can be pretty extensible if you want they can be narrowly focused like unit tests on a single component a single Behavior or you can build them into something that's maybe more broadly focused on on multiple components or the

system as a whole but in most cases I'd say a fuzz test is still focusing on function local Behavior rather than trying to test the whole system at once so finally an invariant test applies the same idea of testing properties to the system as a whole so rather than defining the properties of specific functions we're going to define invariant properties about a specific contract or system of contracts that should always hold in the system uh so yeah here are some examples of invariance you might write for smart contract system a vault contract always holds enough con tokens to cover all of its withdrawals x times y always equals K in a unit swap pool that's a really famous invariant LPS should only ever be able to withdraw the number of staking tokens they

deposited an erc20 token Supply always equals the sum of its individual balances and so during an invariant test run the fuzzer will run against all functions in all contracts versus a fuzz test where it's targeting a specific fuzz test with specific input parameters so the fuzzer now runs against all the functions it finds in all of our contracts it tries a sequence of random calls with randomly generated call data and it checks are defined in variants after every call if any one of those call sequences breaks the invariance the tests fail and it produces a counter example for us that can show show how it failed so invariant tests are a powerful tool I think they're probably the most advanced testing feature in Foundry and they can be really good tools for shaking out

invalid assumptions complex edge cases and unexpected interactions in your smart contract system but because they're so unconstrained it can also be very challenging to channel the fuzzer's sort of unconstrained chaos into a suite of meaningful reliable useful tests and also to avoid kind of making assumptions that might fool yourself along the way and keep your keep your test testing what you actually think they are uh so we're going to test wrapped ether in this Workshop if you don't know rapt ether a quick overview is that it's a contract that allows you to deposit and wrap native ether which is then represented as we an erc20 token and similarly if you are holding with the erc20 token you can withdraw native

ether by exchanging that token one for one for for Native ether so Rapture is a simple but very critical primitive in the ethereum application layer for two two big reasons number one it enables applications that are composable with the rc20 tokens to use a representation of native ether so if you've already built a system that is composable with the rc20s you don't need to add like extra edge cases and semantics for dealing with Native ether and then secondly it helps mitigate security risks that are associated with transfers of native ether when you send native ether you're transferring control flow over to the receiver which which is risky and can lead to re-entrancy bugs so using Rapture can help mitigate some of those concerns here's the mainnet with contract the canonical with contract there's a link

here too to weth 9 which is like the canonical weave contract on mainnet this one currently holds what is this 3.4 million ether like 6.6 billion dollars so finding any bugs in this would be a big deal and this is just the mainnet contract right there are other versions of this contract deployed on on other chains as the native wrapped rep token uh the contract is actually simple enough that we can cram it into four slides here uh it's it's a little over 50 lines of code so we can speed run it quickly here you can see we have uh erc20 metadata we have some standard erc20 events we've got a mapping for balances and a nested mapping for allowances

the really interesting stuff is uh are the next three functions here fallback deposit and withdraw so you can see in deposit if the sender is a payable function right in deposit we will credit the sender with the amount of ether that they're providing similarly in withdraw we'll exchange exchange back and transfer an amount of native ether equal to the wad amount here that they're they're withdrawing and then thirdly we have this fallback function which is sort of just a convenience function so that if you send ether directly to the contract it will wrap it and deposit it for you finally we've got total Supply we've got transfer stuff approve transfer transfer from um all the details of this are not super

super important the point here is that it's like a pretty simple pretty simple 50 line contract uh cool so let's get started writing invariant tests and just starting by setting up a framework for for writing in a variant test in Forge so fortunately everything you need to start writing in a variant test is built now into the Forge test contract the based contract that you import from from Forge standard to set up a unit test uh so I like to put you know dot invariants in the name of my invariant test files to distinguish them from others but that's really just a convention it's not required from the test Runner uh and a simple invariant test can just look like the the example here uh hopefully this looks familiar if you've used Foundry you can see we're declaring our contract under test as a

state variable we create an instance of that contract in setup and then we write test functions using assertion helpers like assert EQ here that will make assertions about the state of the system the one thing that's different here you might notice is that the the test function is prefixed with invariance underscore so invariant test need to be start need to start with this invariant underscore prefix so we're starting with a pretty useless invariant here but let's just see what happens this is testing that the total supply of rap ether is always going to be zero and if we run the tests here's the outputs that we'll get back you can see this looks sort of like a standard Forge unit test run but we have

a little bit more information underneath it here it runs calls and reverts so when you read an invariant run it's going to print back some sort of diagnostic information about the Run that includes runs this is the total number of random call sequences that were generated by the fuzzer during this run the number of calls so this is the total number of external calls the fuzzer made to our contract during this test run this is equal to the number of runs times the depth which is a parameter you can configure in your Forge setup and that's how many how many calls will be made uh in a in a run sequence so you can sort of tweak that to have more or fewer calls and then finally we have reverts which is the number of calls that actually reverted in this test run so in this

case you can see like well over half of our calls reverted so these are all the randomly generated calls that were made by the fuzzer to our contract over half of them reverted uh so you might wonder what's going on here is this doing anything uh this kind of reverted a bunch but the test passed so what's going on one tool we can use here to figure that out is another setting within the forge config called fail on revert you can toggle this between false and true to see what's happening in an invariant run so this will cause those previously we had this set to false right so the tests will run we're sort of allowing the test to to fail and revert in the case that anything reverts if we want to see what has failed we can toggle this to True rerun the tests and and look at what's

going on so yeah switch this to true rerun our tests and we can see see a failure case here so this is sort of a failed test run will look like and you can see we have some information about the call sequence the sender the address that was being called the call data of those calls which tells us what calls were made in in what order so here the call that is reverting is this transfer from uh probably because the caller had hadn't made an approval right so the two addressed the from address hadn't made an approval for this sender address to transfer to transfer their ether here um yeah so if we look carefully at uh at this fuzzer output we will sort of

discover that what's happening here in this initial test uh is that basically every call is reverting except for a handful of calls that are making a zero deposit or a zero withdrawal which is which is allowed if you look carefully at the the rep due through contract it doesn't catch zero deposits zero withdrawals so uh this sort of open fuzzing uh where we point the fuzzer uh just at the raw contract let it kind of wreak havoc on all methods all arguments uh everything it finds at once can be useful in some scenarios but this is a good example of how we sort of have to constrain the environment often in invariant testing to actually simulate the conditions that we care about in this case we want we want to actually test you know making deposits and withdrawals from this contract the fuzzer by default is is not

going to do that so um there's an interesting trade-off here right there's a trade-off between exploring more random call sequences in invariant testing and finding meaningful sequences that actually test our invariance if we expose more surface area to the fuzzer there's much more that we can fuzz but it means we use more of these these limited runs on things that might simply might simply revert and not test the invariance that we care about so if everything is reverting because arguments and ordering are not realistic we might not really be testing the invariance we want to in a useful way at all and I find this like the trickiest the trickiest trade-off in fuzz and invariant testing in general is to think about think about if you can only do a limited number of runs how are you going to sort of use use those runs

as effectively as possible uh okay so in order to sort of constrain our environment and test what we really care about here we're going to use a pattern called a Handler so a Handler is a wrapper contract that we can use to manage interactions with the contract under test and basically rather than expose the the week 9 functions directly to the fuzzer we're going to wrap it in this Handler contract this lets us control the environment it lets us sort of choose when to expose particular functions to to the fuzzer as we build out our test suite and it lets us use cheat codes like VM prank and deal things we usually use in in Forge to set up the environment with the conditions that we care about so a Handler is just another contract as

you can see here typically I like to pass in the contract under test as a Constructor ARG and then within this Handler contract you'll write wrapper functions for each external function on the contract that you're testing and then one by one expose those functions to the fuzzer as you build up your Suite uh yeah so in this example you can see we're sort of mirroring the interface of the with nine contract right here we've just exposed deposit sort of the first the first function we want to test but as we build this out we're going to expose deposit withdraw transfer transfer from all of those external functions um and as we fuzz this contract the fuzzer is now going to Generate random calls with random values to the functions we've defined on the Handler rather than the with nine contract itself so an

important note here is that it's up to us to pass through those first arguments to the contract under test and to think about constraining them if necessary within the Handler so here we're passing through the fuzzed amount value in deposit to with deposit as the as the value when we make that call and second here since our test contract needs to have some ether balance in order to make a deposit without reverting we're going to use deal in the Constructor here right after we after we set the weave contracts to deal ourselves some ether in the Constructor so just tanning through to start uh okay back over in the tests uh we need to set up our Handler contract alongside the wheat contract uh so yeah this is how this looks uh

we'll import our Handler set up that Handler in the setup function and then importantly here we're using the Target contract built in this is is part of the Forge test class and this is telling the fuzzer to now Target our Handler contract instead of pointing at width 9 directly and this is important don't forget to set this up if you don't do this the fuzzer will find all all functions all contracts that are created during setup and it'll implicitly fuzz all the methods that it finds on those contracts now so this is a way to kind of Target it just to the specific function that we want to expose specific contract interface that we want to expose okay we run these tests now and we have a successful failure so unlike our very

first failure which broke right after setup uh the fuzzer has failed here and we have a Successful Failure right what we expect so the fuzzer has helpfully printed the call sequence that broke our invariant here 's the sender the address you can see now this is our Handler contract right we were calling the Handler contract rather than with nine directly the call data of the function that broke the invariant here it was a deposit and the arguments to that function so in this example we called deposit we deposited 65 way and that broke our now invalid invariant that the the total

Supply is always zero okay so what should our first invariant condition actually be in this case uh I think thinking and invariance can be very different from the way that we think about the system when you're writing unit tests you need to sort of think about properties of the system as a whole rather than specific reactions to specific concrete inputs but here's one invariant we can test I'm going to call this one conservation of ether so if you think about our our two contracts we have our Handler contract and the The rapt Ether contract and those two contracts are a closed system right eth is only created in the Handler when we deal it to ourselves and it can only flow into week 9 once when we deposit or out of with nine if we if we

withdraw so we can test this sort of conservation of ether property in this closed system which is that the wheat total Supply Plus the Handler's ether balance should always equal the circulating supply of eth in this closed system so let's update our Handler a little bit here uh we'll make it like a little bit more realistic we just we dealt 10 ether before but we can use kind of a more realistic value here right there's like around 120 and a half million ether in circulation so let's uh we'll add this as a public constant on our Handler and we'll deal that amount to ourselves in the Handler uh during setup and then from here we can now Define our

invariant test uh in the invariant test file so here's the property that should always hold the Handler each Supply which we can access since it's exposed as a public constant is equal to the Handler contracts balance plus the wheat total Supply at all times so for now we'll also add one more condition to our test which is to use this bound helper to bound the deposit amounts such that it's less than or equal to the remaining ether balance in the Handler contract and this will prevent calls from reverting if we generate a random call that tries to deposit more eth than is available we don't necessarily have to do this right we could let our tests revert in that case but for now as we're building

up this Suite I sort of want to focus on testing testing the conditions that we care about right which is not not the revert case uh we might want sort of at the end of The Suite once we built out these invariants to remove some of these bounds and make our fuzzer our fuzz run a little bit more unconstrained allow more things to revert but I find that it's helpful kind of as you're building up these tests often to uh to prevent things from reverting and and use this bound helper here if you haven't seen bound before this constrains a value right so we're constraining the amount value here to be between zero and the balance of our Handler contract so it's not going to try to deposit more than the Handler has in its balance and when you're fuzzing on like a really big

un-256 number you often generate uh generate really big numbers in these runs um bound is uh is kind of like VM assumed too if you've used VM assume but it's it's uh a better tool because it doesn't throw away the run right so you can use bound it's just going to constrain the value rather than throwing away the Run altogether cool run these tests and we should see them pass and you can see here reverts is now zero right we're never attempting a deposit that exceeds the balance so none of these calls revert like they were they were before we're kind of banging on the contract and over 50 of our calls were reverting uh so switching back and forth between open open tests and constrained tests and bounded and unbounded calls can be a

very useful technique as we write in variant tests but for now we're going to kind of keep these values constrained as we build up the Handler invariance okay so our test pass but we've only exposed one function from the contract under test through the Handler so to test the real world behavior of wrapped ether we need to expose withdraw transfer transfer from all the rest of those external functions and eventually we'll get to adding transfers and approvals but let's not add them yet for now let's add withdraw and a fallback function yep here we go uh yeah so you can see here we've added withdraw we're also going to use Bound Again to bound the amount that we're fuzzing on here to the balance of the color we also need to add a receive callback to the Handler here so that when we

withdraw that the test contract can receive it send fallback is kind of interesting right in this in this Handler function we need to trigger the fallback function on on weft so here we're going to this looks similar to deposit right but rather than called deposit directly we're going to use a low level call in order to invoke the invoke the fallback function and send these directly uh cool and once we've added these run our tests again we can see they they still pass so our invariant is still holding as we've exposed more more Behavior to the fuzzer uh okay let's move on to to another invariant uh so the second variant here is

solvency and in order to test this invariant we're going to introduce a new pattern called ghost variables so with this invariant it's important that the weave contracts native balance is always high enough to cover all possible withdrawals from the contract all right otherwise it would be insolvent not everyone could withdraw their if all right since wrapped ether any thorough convertible one one to one the contracts balance should always equal all the deposits that have ever come into the contract minus all the withdrawals that have ever come out of the contract and in order to test this we need a way to track all the deposits that have ever come into the contract and all the withdrawals that have ever come out of the contract so we can use a technique that's called the ghost variable in order to track this so a ghost variable is a stateful

variable we can put in our Handler contract and it's going to track state that's not otherwise exposed by the contract under test I like to prefix these with ghost underscore I see folks who use uh Satora and other invariant testing things like to prefix these with with ghost but really these are just normal variables right it's just a solidity a solidity State variable you can name it whatever we want so here we've defined a two two unit 256 variables here ghost deposit some in ghost withdraw sum and we're going to increment both of those right when we deposit we're going to increment ghost deposit sum when we withdraw we will increment ghost withdraw sum and that's going to keep track of total deposits in total withdrawals out uh you might wonder why we don't just decrement ghost deposit sum right just

use one variable and increment sometimes decrement sometimes I think there are two good reasons so one is that it's nice to have these um sort of Intermediate Accounting variables available as separate properties so you may want to Define another invariant later that uses these as kind of intermediate intermediate parameters and the other thing is that it's just good to be as wary as you can about adding any complex or conditional behavior in the Handler if you can keep your ghost variables really simple just keep them as like simple accumulators you probably should because the more complex your Handler gets the more likely you are to introduce an invalid assumption that that breaks your tests in a way that you don't expect so keep them as simple as you can is kind of a good a good practice uh cool so here's our invariant

since we've set up these ghost variables as public State variables we can now access them in the test to Define our invariant property so here the uh the weath contracts balance should always be equal to the Handler ghost deposit sum minus the Handler ghost withdraw some uh okay let's give this a run see what happens uh and here we go with uh with those two changes we've made we actually get a failure So reading failed call sequences uh invariant testing is kind of kind of part of the art of learning and variant testing uh you'll really learn to like read and debug and decode your call data if you're reading these counter examples that it speaks back at you especially if you have like a complex nested struct in

the interface of your of your functions um but one one thing that's really helpful here is that it's always the final call that caused the invariant to fail right so we're getting the whole call sequence here we can see three calls deposit deposit send fallback it's always the third of those after which are are invariant failed uh and we we failed the test so yeah here's the call data and the arguments that broke our invariant and you can see it was calling send file back with the value 1007. does anyone see what happens here cool yeah so we forgot to account for deposits in the fallback function right there's this other way that we can we can deposit into into F that will

increase the balance and we forgot to do our internal Accounting in the Handler here so uh yeah this is a good example right of a way that you can uh if you're not careful in your Handler about the things that you're tracking and testing uh you can maybe not test test what you think you are so yeah here let's uh let's increment ghost deposit sum just like we do in deposits uh in our send fallback function here and cool once we've done that all our tests pass again yep yep three times right yeah yeah it failed just one time and

what it's showing us are the three calls in the sequence so there was a deposit that succeeded uh right we deposited [Music] um it ran like 1000 times and among those 1000 runs it was just a single failure or just one was reported here uh yes a single failure was reported here I may have copy pasted this from a code example so uh okay yeah but in this case yeah this is the single this is the first I think it's reporting the first counter example that it that it found here so okay because probably I mean if if it's fuzzing it would feel like I know one third of the time so it's like a huge number of failures right yeah it's just gonna report one counter

example that it finds I actually don't know if it holds on to the uh other failed counter examples if it finds that okay awesome thanks some fuzzing tools will do like shrinking which which is is really helpful where it'll shrink down the the field example to uh uh the smallest input I could find but as far as I know Foundry doesn't do that uh cool so that's our second invariant solvency of deposits uh let's look at another solvency invariant this is going to be the most complex one uh which I'll call solvency of balances so solvency of deposits was looking at like all the deposits that have ever come in all the deposits that have ever gone out of the contract solvency of balances is uh is a little bit different

for this one we want to uh we want to check that The Ether balance of the contract should be equal to the sum of all individual balances in the contract and that includes balances before and after transfers right so we have this mapping of each each account address and its balance of of the token we want to look at every entry in that mapping sum up all those all those balances and that should always be equal to the total supply of the token uh and this is an interesting one right because even if users transfer their tokens around this sum of balances should should stay the same and remain equal to the contracts ether balance at least modulo deposits and withdrawals uh okay so this is kind of complex to track right how do we want to track individual balances within this mapping within the contract one thing we could

do is like add a more complicated ghost variable to our Handler we could add a mapping of address to un256 track each color's balance as it comes into the contracts but if you start going down that path you'll realize pretty quickly that you're you're just replicating the behavior of the erc20 token in your Handler that's something we want to avoid right we should keep our Handler as simple as possible so in general I think it's a good practice to rely on external state from the contract you're testing whenever you can so if you find yourself adding lots of complex logic step back think about whether you can access that information in another way and to do that we we can right so rather than store balances internally what we can do is save the address of every caller iterate over each of those addresses and

get its balance and then add up the balances in our test so here's how we can do that to do this we're going to need to introduce a new pattern called called actors and we're also just going to need to introduce this concept of of multiple callers which we haven't yet right so far every call to the to the rap ether contract is originating from our Handler contract so this is not very realistic only a single address is ever calling calling the contract under test what we want to do is simulate many calls coming from many different addresses so Foundry does fuzz different message sender addresses on each call to our Handler but since we have this Handler contract sitting between the fuzzer and our contract under test we need to propagate those we need to pass them along using VM prank in order to pass

them through to to the contractor test a second thing we have to to think about here is that all those calls will revert if the the caller doesn't have enough eth to make a deposit or enough balance to make a withdrawal and since our tests are a closed system right we've created all the eth in the world in our test environment when we set it up we want to actually send real ether or like real fake ether here in this test rather than using a cheat code like vmdl which would kind of mess with our circulating Ethan variant right so it's important within the Handler that we're actually sending sending using using real eth transfers so we have a pay helper down here at the bottom which will help us make those transfers before tests that we need them okay and here's what it looks like in

deposit to to actually fuzz on multiple message senders we're going to use vmprint right before we call deposits pass through the message sender which will be fuzz by Foundry in this test uh yeah and then prior to that you can see on the line right above we're going to pay that message sender pay that caller the amount that they need in order to make this deposit I will update withdraw so you can see here we're going to change the constraint here from the balance of the Handler contract to the balance of the caller message sender we'll print message sender make the withdrawal and then one additional thing we're doing here is we need to send that eth back using Pay to that to the Handler to keep it keep it circulating the way we expect

and then similarly we can update send fallback this is basically like like deposit uh pay the color prank the caller pass that through cool so the test is still pass here we've introduced this concept of fuzzing on multiple actors basically with every call Foundry is generating a new random caller and we're passing that through to the contract under test so we're now testing multiple actors interacting with the contracts what we haven't done yet is like track their addresses right we don't know what all those addresses are so we still need to build up build up the ability to track those addresses okay so here's one simple way we can do this right we want to capture a deduplicated list of all the callers that we care about we can do so with like a simple simple append only set

struct here uh one way I like to do this is with a modifier and a little struct we can use to to hold on to these these colors so here's an address that struct this is going to store a dynamic array of addresses and then a Boolean mapping that just checks whether we've added added a value to the address or not we're just kind of going to build this ourselves you could use like opens up an innumerable set or something here if you don't want to want to roll it yourself we'll write a few Library functions here to add some Behavior to this data structure so here add will just push an address into that array if it hasn't already been seen count will just give us back the total number of addresses in that structure and then when we're at it let's add this

function so this Rand function will grab a random actor address out of that set based on an input seed so just doing a little modulo here um and grabbing a random address out of that set so we'll use this in a little bit but but not just yet but I'll show it now so we we don't have to go back okay let's use this set and the library in our Handler so we'll create this set struct as a state variable we'll use this solidity using syntax to attach the behavior from the library and then we're going to add a view function to our Handler here which exposes All the known actor addresses and I like to pull this all together into a couple modifiers this is a pretty

common pattern uh in Foundry and variant testing you'll see is this notion of using a current actor State variable that represents the sort of currently selected actor so what we're doing here is we're going to also add a a state variable to the Handler called current actor and this is sort of going to replace message sender in our in our tests we'll add this modifier create actor what this does is set the current actor to whatever the fuzz message center value is and then add it to the add it to the set that ad will be a no op if it's already in the set right so just can be added to our actorset and then this use Vector modifier which takes a seed as an argument so we can fuzz on a seed and grab a random actor out of that known known list of vector

addresses okay I know that's quite quite a lot of refactor here but we'll uh we now have what we need to write our invariant right so here we go The Weave contracts ether balance should always be at least as much as the sum of individual balances so yeah here we can now um create an integer here to tally up the sum of all balances we can grab those actor addresses from our Handler uh iterate over each of those actor addresses ask the weath contract for their balance and add it to that sum and then at the end here uh we can make our assertion right the balance should always equal that that total amount that we've tallied up by uh by asking the contract for each actor's balance

okay final step before you can run this is to update all of our functions in the Handler to use actors so we'll add that modifier here create actor to deposit and you can see we basically replace the places we were using message sender before with current actor so it's just kind of a helper that sets message sender to this current actor actor value same thing on send fallback this looks pretty similar to deposit it's just doing the low level call and then withdraw is a bit more complicated so for this one we're going to use that use actor modifier which selects a randomly known actor from the set and we're going to add an extra argument to the Handler function so this is a seed that we can use pass through to that modifier which we'll select a

random vector so here we kind of want to choose a known actor to ensure that we're testing realistic withdrawals we could easily just fuzz on a random address here just like use message sender rather than a known nectar from our set but if we do so nearly all withdrawals are going to have zero amounts because most of those randomly fuzzed addresses don't have any balance in the contract so what we actually want to test here in our sort of constrained invariant tests is is testing actors that actually have a balance in the contract um yeah we won't have time to go into detail today on this but there's a good example in in the repo about this uh this Handler function in particular uh and how it's sort of easy easy to fool yourself here uh if you're not not

careful about uh checking checking that the address that you're fuzzing on actually has a balance in the contract so one technique that's really useful for this where we don't have time to talk about it today but is a a call summary so collecting and printing some diagnostic information about which calls are actually being invoked and with what arguments uh as you're fuzzing looking at that to make sure it's like well distributed across the functions you expect it's not reverting when when you don't expect it to revert stuff like that um hopefully we have some like better tooling coming in Foundry on that soon that'll help us like collect collect metrics and data over these runs but for now you can roll it yourself okay so there we go uh we run this and all three after this large refactor

right all three of our our invariants are holding cool so a few more changes we need to make here to expose all the functionality of the contracts uh so far we've only exposed deposit withdraw and the fallback function but we need to add the rest of the rap ether functions to the Handler and we have our invariance defined now uh and at each step here as we expose these we expect those invariants to to continue to hold so as we add this functionality we'll sort of keep running the tests and make sure that they they still pass so here's approve when we're doing an approval we'll choose a random spender and just approve them for some randomly fuzzed amount for transfer we will choose a random

destination address uh yeah you can see we're using uh we're sort of hitting the the actors set there directly calling calling Rand directly on it to select that to address transfer from is a little bit more complicated um here we're going to select a random color select a random two address select a random from address for the transfer from if we were to stop there again many of these transfers would revert because it would be unlikely that the fuzzed address the fuzz caller was approved to transfer from right so um and a good way to tell that right is just run your tests build build this out run the tests look at how many reverts there are right you may see like other

thousands and thousands of reverts because most of these calls are failing so one thing we'll do here is add this Boolean flag for approve we'll fuzz on that and then 50 of the time if that is set to True we'll explicitly approve the caller before before we make that call so that prevents this from reverting all the time it will revert revert some of the time and that's okay cool and these should still pass Okay so let's see I'm just gonna try to show some Live code we'll see so we've made quite a lot of changes to to uh our contracts to our

Handler uh over the course of this so far uh right one thing we'd like to get out of this is sort of a sense of if uh if our tests are still testing what we think they are right the Quality quality of our invarian systems yes yes it's a good question um yeah I think this output example maybe a copy paste yeah um yeah it's that's it's a good number though to watch like over the course of it as you run these tests right like if you expect zero you should always toggle that toggle that setting back to true

and see what it was that reverted to check that I do find with like native eth transfers often you'll get a handful of reverts uh if you're not careful about constraining it to avoid like pre-compiles and uh some of the some other weird unusual addresses depending on the on the setup so that's probably where some of those reverts are coming from and generally yeah it's a good practice as you go like if you're in the mode where you want no reverts at all always check those out make sure you understand why it's reverting if it's reverting uh and occasionally if you're in sort of fuzzing in a mode where you don't care if you're reverting right you don't mind every every once in a while flip that on and check what what is reverting to make sure it's not something that's that's unexpected uh cool so it'd be nice for us to have a

way to to test our tests right we've built out this this Handler it's quite complex is it actually testing what we think it is is it actually catching bugs in our contract uh and this can be tricky right like unlike unit tests where it's kind of easy to think about mapping one specific input to one specific output is is usually pretty clear invariant tests can sometimes be tricky and they'll accidentally pass if you've introduced an incorrect assumption about your system so one way to ensure our tests are actually working is to test our tests by introducing artificial bugs one thing we can do here is like intentionally break some of the production code run our tests and then see if they fail so here's a little a little diff a little patch we can add rather than actually crediting the uh the caller with the value the message value amount

that they're providing in deposit we'll just credit them with one way right ignore their amount and credit them with one way uh and so a technique I like to use here sometimes is to save some bugs in the contract under test as get patch files in the repo and then you can sort of reapply them from time to time double check that the test Suite still works as expected this is kind of a quick and dirty mutation testing framework uh so yeah here are a few other bugs we might introduce we'll change withdraw to just send back one way instead of the full amount here's one we'll we'll remove the call to deposit from the fallback so it's not not actually invoking that anymore and then we can add here's a simple little make file that we can use to

apply a patch out of that directory run the tests and then check that they fail so if we sort of get apply each patch in turn verify that the tests catch that bug in this case we want to see them fail right rather than see them pass we can be confident that that our tests are catching those bugs and our tests are working so this is just a quick and dirty form of what's called mutation testing hopefully this is coming to Foundry pretty soon there's a an open thread on adding adding support for Gambit which is a new tool that Satora is working on for mutation testing maybe we can actually show one of these yeah cool

yeah so here's an example we applied that bug one patch ran the tests and we can see it broke one of our broke one of our invariants here so yeah this is a good sign that our our test Suite is actually testing what we what we think it is okay so our tests may seem to be pretty comprehensive but we have kind of one final boss before we can call them complete uh and this is an interesting one there's actually one intuitive invariance you might think should exist in the wheat contract that famously doesn't hold and it has to do with the way that it's calculating total Supply

there's a great post from Stephen zellick who used Z3 to do some formal verification on on with and and talks about finding a violation of this invariant so here's how the weave contract uses uh calculates total Supply I don't know if folks see an issue with this there's a hint in the title of the slide uh yeah so rather than storing the total token balance in a separate State variable it's using this uh this sort of shortcut by just using its total ether balance as the total token Supply and this uh saves gas over time but it actually breaks this invariance that total Supply equals the sum of all balances and that's because there's one way that we can force the contract to increase that total Supply value without actually creating new rapt ether tokens and

that's by force sending ether by calling self-destruct which will uh will force push ether into its contract balance uh so The Foundry fuzzer tests a lot of things out of the box but it's not going to like force push ether to particular addresses uh unless we configure it to do so so we're going to need to simulate the scenario in our Handler ourselves and we can do it with this simple simple little contract here so this push contract just as a Constructor takes a destination address and immediately self-destructs itself and sends whatever whatever ether was provided when it was created so we'll also expose this Force push function on the Handler which will invoke that contract and force push some amounts of some fuzzed amounts to the wrapped ether contract

okay so once we've added this to our Handler we run the tests and fortunately we can see two invariants have failed here the solvency balances invariant and the solvency deposits invariant both failed so one thing we could do here is like relax our invariance definition right maybe the invariant here is just that just that the contract balance is at least as much as all the deposits it could be more but we actually have the ability to account exactly for the amount of force pushed user right we can make it a little bit a little bit more rigorous than that so let's do that uh same pattern as before right we can account for the amount of ether that's been forced pushed into the contract we'll use a ghost variable to do that we'll increment that on on Force push

and then we can update our solvency and variance here to account for that right so now in solvency of deposits the contracts balance should always be equal to the total amount of deposits that have been made plus the total amount of force pushed ether minus the total amount of withdrawals and then similarly here in Balance solvency we'll subtract out the the force pushed amount from from the total or we could add it to the other the other term there I suppose uh and sorry this is a an outdated example that's using this like reducer thing which we didn't have time to to look at today cool so we'll give those like a final good long run here 25 000 runs uh a

pretty deep call depth here and we can see that all our invariants have passed so those three three invariant tests are all passing so I think invariant tests are a super powerful tool in in Foundry um but this case of like force pushes especially is an interesting illustration of one of their blind spots right if we were using like a symbolic test or uh maybe more fully featured fuzzler that's modeling those ether sends via self-destruct it would probably catch that bug pretty quickly but in fact we nearly missed it with the fuzzer we had to rely on our own knowledge about the weath contract to cover it on the other hand invariant tests are much faster to run uh they're they're pretty good right we fuzzing fuzzing gets you a lot of the value that you would get out of out of many more sophisticated methods and they allow us

to build up a suite of reasonably high confidence and variant properties that maybe we want to invest more in testing over time right we might want to further verify those invariants that we've defined using even more powerful tools and I find them especially useful as you develop like as you're developing your system right as you're working along the way as you're thinking about invariance going back and forth and kind of uh defining these yourselves causes you to think about the actual invariance in the the underlying code under test but yeah it's important here to remember that all types of fuzz tests invariant tests included are probabilistic right so unlike a symbolic test that's going to explore all possible execution paths fuzz tests are only as good as the random data that they're generating this is still really really good most of the time but as with all smart contract

testing we should really do it all when we can right right unit tests right fuzz tests write Fork tests write invariant tests and and use formal verification when we can okay that's it thank you everyone uh please if you want more details check out the the repo there's some additional content in there and you can follow me on Twitter at ethical [Applause] is there any question can you share any hands-on experience on um how to run fuzzy tests for continuous integration and uh so the last run I saw was slightly less than two hours yeah I

suppose this is not something you would do on every push or I don't know can you parallelize this I know yeah I know uh yeah so Foundry will let you configure profiles in your your foundry.tamil that's pretty useful to set different um uh different parameters right for the the depth of the run that you want and the the length of the Run um yeah and I think sort of depends on the stage of production that you're targeting with your CI run right you want to run them frequently as a developer and maybe uh maybe often when you're checking into Main and then do some some very intensive fuzzing before you you deploy to production uh yeah I think a good example you might want to look at is this the seaport repo has some good configuration for different uh different fuzz fuzz runs and fuzz

configurations for different uh different environments someone want to add something so the uh self-destruct thing is a little scary there because you think you have this beautiful invariant you think you've got it and there's you know something you actually have to work to test um is there anything besides having a list of gotchas that you kind of go through to work around that or catch things like that yeah that's a good question uh I think I think one technique that really helps is building this Suite up

alongside the development of your contracts right which causes you it's kind of like test driven development right it causes you to stop think about the assumptions at each point think about how things would go on go wrong um uh but yeah like it's an important underline here that there's like no there's no magic bullet for testing or there's no tool that we can just point at our contracts and and find all the all the errors uh there's some really good tools out there but they all rely on your knowledge of of the contract itself your expectations about the contract itself uh and your knowledge of yeah potential potential errors and gotchas yeah so I think you know the more we can model those gotchas in the tools that we use the better there are a lot of tools that do do that um but yeah it's a tricky a tricky

problem I don't have a good answer foreign [Music] [Music]