Foundry-based Formal Verification

Transcript

all right hello um so well welcome to the uh control Workshop here in in the SS um so basically in this Workshop what I'm going to to to try to show you is um sort of like the grand like high level picture of what you're in for when you want to use control and sort of what I hope that you get from this talk is basically the foundation of what you are going to be dealing with um when you you know when you start using control um we we have killer documentation for a lot of features um so basically what I want you to get from this is just being able to go to this documentation and be

actually familiar with the whole process and know what to expect so but first things first who am I I'm I'm Juan um I'm a verification engineer at runtime verification you know what control is from um and yeah we're we're we're a a formal methods uh company uh we do formal methods for for ethereum also for other chains um and yeah you should you should check out our work because it's very very nice um the way to get control uh it's you can just run this this bash uh this bash command to install K which is our our package manager uh for you know our Frameworks and just you know you can you

can use control from there um and also there's there's a repo with uh with the examples that we're going to be uh showing in this in this Workshop um you are not required to you to get the to get the repo for for for this presentation but uh you can recreate the the examples uh from there so this is where your control Journey starts uh at this very moment and it starts with re Jesus or F right so basically uh if you know F uh that's that's basically you know what you like you already know how to write control proofs like that's that's because

basically control proofs are 100% Foundry compatible um and so basically you can take any any Foundry test uh that you would fuzz over and then you can run it as a control proof right uh and you will be executing it symbolically instead of uh concretely and we'll see what that means a bit later so the way to basically take a Foundry test and then you know turn it into a control proof is you swap instead of Forge build you just have control build and then instead of Forge test you have control proof right and and these two commands basically do what you would expect them to do um um in in Foundry to run you know to run a test you need to prefix it with

test uh with control we actually have two more prefixes which is proof that come from hbn which is another formal verification tool from for solidity and then we also have check which comes from Hal much so this means that you know running writing you know control proes also it's it's compatible with these with these other tools or you can also take these you know properties written for these tools and bring them over to control so it also has like great um compatibility features um also we as you would expect with something that uh a Fest we also have compatibility with cheat codes we also have our own cheat code so besides um supporting fundry CH codes we also

have our own um but also recently fundry have have have included some some of which were our cheat C initially into into their cheat C suit um so basically the for the compatible funded cheat codes you know you get the um mostly the most execution related cheat codes the way that you know allow you to manipulate evm State and so on um we don't have 100% of like the maximum amount of cheat codes that fundry has more the ones that we don't have usually is because we haven't like see that we need to use them so if you're missing any um feel free to reach out uh and and you know we'll we also incom them based on you know what they

what our users uh what our users need so yeah feel free to to just reach us out um also we have our own like cheat codes which are because we're doing symbolic execution rather than concrete right so we needed the own type of cheat codes that was U you know important for symbolic executions um so yeah we added them and one of the reasons why why we initially have this you know instead of having a test prefix have a proof prefix is because if you have custom cheat codes they won't run as a Foundry tests so you also you want to separate them and not to Break um you know F test suits so with some of the cheat codes

that are own fundry won't run but this is big of an asteris because you know fundry recently added some of our cheat codes in particularly these are the new cheat codes that were control inspired um this set arbitrary storage copy storage mock function and then this random u in bu address and bytes so the control equivalence is not exactly the same cheat code in the sense of the naming but what it does it's sort of equivalent BR brought to the realm of of of fuzzing so set arbitary storage for us it's symbolic storage for copy storage and mock function is the same and then for the random we just call them fresh because in in the symbolic context it does it's not random itself uh it's just a fresh variable

so basically what set arbitary stars does uh in case you don't know it in Foundry it just sets you know a concrete fixed number uh for any uninitialized rre slots um of a given address um and for us it sets the entire symbolic storage uh so sorry the entire storage are symbolic right um copy storage it does with what it says it just copies the the storage from one account to another uh we also support copying transing storage uh when when needed um and in Foundry as a you you cannot use uh both copy storage and set arbitary storage um we also have this mock function which is sort of like a you

know a mock call but on steroid a bit so mck call would the cheat code mck call would just you know swap a function call with a in a specified return value in this case mock function what it does is mocks the execution so it will swap the mock the the the call with uh what you can consider a model of the of the function that you're mocking uh and so you that that is useful if you want to if you have very complicated function and you want that you know yet you want to execute just you know sort of like a model or a summary of it um but you you still want to run it not just you know get a concrete return value and then we have this random which is just uh in F just a new fixed uh value and for us is a fresh

um symbolic variable so these uh these cheat codes are not yet implemented in Foundry uh they are sort of in the pipeline so these are chitos that we still have uh which is sort of for funer you have expect call which is like for us expect regular call but we we wanted to also have some some sort of more granularity where we're writing our tests so in particular we have these calls which with is cheat codes which is which are kind of you know self-explanatory um so basically up to this point why do we need to be so symbolic right like we have like you have Foundry which you know fuzzes

concretely and so on so why do we why is there need for symbolic reasoning and well a bit the the the reason behind it is that you know with concrete like the state space is just too much big um so with with symbolic reasoning it allows you to actually explore basically the totality of it if you if you if you do it correctly and or at least a way bigger amount of the state space and to ensure that your function you know has been uh as thoroughly explored as possible and so for instance here you what you this could be like just a Foundry test um but you know what what executing it symbolically allows us to

do is to make sure that there is no value that's being tested that if this passes you know there's no value that will that will um make this test fail whereas with concrete execution if if you're if you're fuzzing you know you you will never get to this level of assurance um so what is symbolic execution in this case right for so as we said for concrete execution basically you just take uh concrete values you start with concrete values then you execute and you always get sort of a concrete result whereas with symbolic execution you can think of it as um executing it as if it were variables from like a math equation right so you start with symbolic in this case from

for instance if you're trying to somehow verify the behavior of the transfer from function you will start with um symbolic values for for for your pre-state then you will execute with some symbolic VAR values and what you will get is an execution brand as sorry yeah an execution tree where each branch basically summarizes a lot of behaviors that can be done in like a lot of concrete tests and in this case you just get like for instance in this example like what is what if in the transfer from what is from is different from Two and what is their equal and then what you get is like a mathematical evaluation of this and sort of like a symbolic summary of what's the behavior of your function going to be and so as we said um symbolic execution you're executing but in a

symbolic way sort of like just think of it like variables in a math equation um and you start from a from a concrete from sorry from a symbolic State and you end up with a bunch of symbolic States each of them symbolizing where can function end um and so taking also one step back it's like so what is formal verification right um more broadly formal verification means like you assert properties of your code which is called specifying it which in the case of control you can do it uh with a Foundry test with have found the property test and then you prove you know that your code

actually satisfies your specifications there are a lot of techniques to do this like to take some specifications some blueprint of what your code supposed to do and then doing some mathematical reasoning on it to make sure that you know your code actually follows These Blueprints symbolic execution is just one of them uh where we execute your code you know as we said symbolic parameters then you get all this branching and basically you just get like a a a like what's your function actually doing and then we check that for every possible path execution path that your function can take um you know your specifications your blueprint uh is complied with so it's it's also the case that you know there there are many techniques for

for doing formal methods formal verification um and and they there's a spectrum right like they they vary in the in the degrees of automatization and they also vary in the degrees of which is the the problems that they are able to solve so meaning what's the kind of statements that you can prove um and usually as a rule of thumb you know the more complex so sorry the more the more automated approv is or rather the other way around the less automated approv is a sorry um a tool for for doing uh formal verification usually this this translates into the ability of of proving more complex uh problems um this is also like sort sort of like a rule of

thumb but um basically there's this this spectrum of the most Auto the least automated Ur usually the the more like General problems or the more complex problems you're able to tackle um it is also true that you know the more automate automated you are the the the the bigger the the easier to use it is right and especially for the for the kind of problems that it's automated to solve uh these tools are are really fantastic fantastic for for just ease of use and you know um yeah just to to get you going um and I wanted to give you some like examples of of how how like how does these different sort of proof systems work

right so basically you have what interactive Theory improving which is like the most automated thing that you can get which is like most mostly manual and you also rely on you know constant feedback from your tool to let you know where you are and it requires a lot of user input and usually the the learning curve is quite steep um and then you also have automated reasoning which usually doesn't require any any interaction hence automated um and it's also usually the case that you know you don't have any insights into what is the proving process so it's sort of a bit like a blackbox in the sense that you you query it for a proof saying I want to prove that my function something um and then will say yes no um but but

there isn't as much insight as with the uh you know interactive uh tools so for instance here's an example of an interactive tool um this it's not very important what it say it's just so this LM for is what is called an interactive theover and in particular this proof proves that you know if a graph is hamiltonian then is connected we don't really care a lot about this but the thing is that with interactive theor provs you can get as far as into formally verifying virtually any type of math like not just you know programs and functions but like literal theorems about very complex things um this is what a proof looks like there like the statement is like the first and second

line and basically the user needs to needs to fill every other line here which it doesn't look very intuitive and the type of feedback that you're being given by the machine while you run this looks like sort of like this so you can tell that there's a there's a somehow a steep curve into learning this sort of stuff it's also very rewarding in the sense that it allows you to go very deep and prove like you know arbitrarily complex properties about math or your code or you have it then we have um automated proofs in this case just with halmos and this is how one like how an automated proof looks like in the sense that you know you just run it and it says if it passes or not um if not it it

gives you a houn example it is also true that with automation it means that you can get unknown results uh meaning that the tool may just you know run out of time and saying you know I I try to prove this automatically you know there's some bounds of time because the tool is not going to be running forever uh and if it doesn't find a solution to it it will just say hey I didn't I didn't just find the solution for this um and then I want to give an example of control because control is sort of in the middle uh it's it's automated but it's also Interactive um so this is one example of what a control proof looks like uh when when it passes so it just sort of like it looks like automated like you just run it and it passes or not um but we also get

feedback which is one of the key principles that you need for for an automated procedure right so in particular with control the type of feedback that you get is this this this tree that's that's made all of all of the possible execution paths that your function can take in particular here we're seeing a branch uh where it tells you which is the path constraint that you're that that you're traversing right so for instance here it's telling us that you know Y is different than zero and that x. Y is less than you know Max you into 56 so there's no overflow in the multiplication and so on and so basically you know like okay I'm executing the function in this context and what we see here are nodes uh so

basically the nodes are snapshots of the execution at a given point uh and in this in this notes uh what you get is like the full state of of the or formalization of the etherum virtual machine so you get this sort of HTML looking configuration and here it's contain the all the information uh of formalization of of of evbm so basically here you have um in in we go like with cells right and so the cas cell for instance it's or formalization of the execution uh of evbm and then you have some things like this chedle uh which we default to Shanghai but we also support Cancun and changing this is just you

know one one command flag away you also have the output you also have you know color call data and so on war stack local memory so basically everything that you would hope for uh when executing like okay what's the state of uh what's the state of of my smart contract when I'm actually running this function function and then we also have the interactiveness part right um so because here so the way this goes usually it's like you execute it then you inspect a bunch of states and then you say okay this is telling me that my function is behaving like this and then you can tell control to say okay now I require you to reason about this in this in this specific way and we do it uh through

what we call lemas um we'll we'll go over this uh in know in in more later but this is basically what it what interacting with with control is looks like it's writing these files that then control will will parse and then we'll we'll rason with uh taking into account what we wrote um here's also sort of like snapshot of of you know this is a non-exhaustive list of formal verification tools available for the for the ethereum ecosystem um but yeah we we luckily in this space we are not sure of tools and and there's there are fantastic teams uh working on on formal verification for this so I I heavily encourage you to to

take a look at every tool because you know as we said there's like a spectrum of automation versus versus ease of use versus you know kind of problems that you can solve uh and so there's there's like there's one tool for each job I would say or at least you know for the kind of of verification that you want to do so yeah definitely check them out um that's nice but you know this is a workshop so let's let's get some some work done uh we're going to be verifying some stuff with control um so first of things first I want to talk about Harbor requirements because control is quite resource intensive and we've had this cases in the past where

it seems like control is crashing or failing but it may be that it's it's because of of lack of resources so we require minimum of 16 GB of memory for for things like building and so on um there's some caveats like if you're using uh this windows subsystem for Linux I think it by default only allocates like two gigabytes to it so you should like you should look that up and make sure that you have if your machine has it at least give 16 gigb of ram to it and same with Docker containers I think in Max it's also cap like a 2 gigabyte or something so just make sure that you you have these requirements like setup um and also for running proofs in parallel as a

rule of th we like 8 gigb of ram per proof this is not like you can experiment with it your computer is not going to burn or anything um but yeah this is sort of like what we look to uh usually and so this you may you may feel if you've ever tried control you may feel a bit uh represented in this picture in the sense that there's a lot of options and there's a lot of things that you can tweak with it and it can be a bit over overwhelming at the beginning so I'm hopefully trying to give you some uh some clarity into into all of this so this is basically how the interactive interaction Lo with control looks like so you would start uh right at the at

the build stage right you first build then you prove and then you inspect right so you build to well first be able to prove but also to include new lemas this is this is um one of the reasons to keep rebuilding stuff and then when you prove basically you will produce what I said what I showed before this uh this symbolic execution tree and basically there's like a su Loop there in which you inspect the symbolic execution tree and then you sort of you can manipulate you can you know like you can say okay you did something weird here and I want to zoom out on zoom in on this and so there's this there's this cycle in which you know you prove you produce your symbolic exit ution tree which is like

the summary of how your function behaves and then you can inspect this summary that control produces for you um and and just sort of gain more insights into what's happening and then out of those insights then you may be wanting to write more lemas uh to then include them again and proving and this will make some sense um in a moment but this is yeah this is like high level how the you know proving interaction works with control so yeah if you just go and do like control build help or control proof help you will be bombarded with all these options and sort of if if you try to sort of um understand which ones are the ones

that are more useful to you it's again it can be a bit overwhelming so let's start with control proof oh sorry build um and see among all of these what is really important for you as a user so basically the the the important option revolve about you know including ocular including lemas basically excluding some if you want to and also regenerating uh K definitions uh which you know this is used to include new lemas so basically to include auxillary lemas we have this flag auxiliary lemas to control build at the bottom you can see sort of the command that you would need to put to to to execute this this step um this auxilary lemas is just

things that we haven't uh and you know working with the tool and we found very useful so this is just also sort of if your proof is not if not working from the beginning this is something to try right away because this enhances controls ability to reason um then you also can include uh your own lemas uh we do this with this you know require and then a path to your K file and then the model that you want to require this is not important that you like memorize any of this it's just like so that you know how it looks like um then we also have some catch lemas that are included by default in control um you can also exclude them but you know they are basically like working

assumptions on how the cat should be basically we assume injectivity and we assume some Collision resistance from symbolic values uh these are not mathematically sound uh and this is why we include them as a separate part like these are not part of like our core semantics of ebm but you know these are like working assumptions that we need to do uh in order to be able to to reason effectively about uh about you know evm code um and then you can also just regenerate K definitions in case you include some lemas with regional recompile so this is a bit of how like the the full control build um command looks like and also we have control proof so again control proof has even more uh

options than control build and so it can be really daunting to to just go about it um again the the relevant options uh are for proof execution tricks so it's just getting you know zooming in into the execution trees uh doing some Loop exploration behavior and also to to increase the performance of control uh to get you know a more detailed uh execution trees remember we we have a node so we so an execution Tre is basically it's paths based on Branch conditions and then we can specify when do we want to create a node which is like a snapshot of the entire state of orbm while executing your function and so we have a lot of you know rules to

create uh new nodes uh you know we have max depth which basically means after doing X steps of execution just make a snapshot of whatever you have then we can also specify when do we want it to break in terms of for instance AVM up codes either every AVM upod every jump ey we also have now jump uh we can also like if if you say like you know I want to know where I'm jumping to a function or when I'm jumping into a loop or whatever you can break on jumpy will allow you to create a cave Cog where you have snapshotted every time you did something like that also on storage and and on cheat codes

um you know we we also can change the loop exploration Behavior so one thing that's in control by default we don't bound Loop execution this means that if you have like an unbounded Loop uh you know you you can get an infinite uh exec a potential infinite execution tree uh and the way we do it we we allow we allow uh bounded Loop reasoning in control via this BMC depth um command where you specify how many Loop and Rollings you want to get so basically you will enter a loop and then you will execute it the amount of time you specify and after that it will it will just uh conclude the proof and and and give it as as as

passing um and we can also specify looping variant which is sort of like the other way of tackling Loops which is instead of just you know unrolling a finite amount of times you can actually specify what's the expected behavior of your Loop and then control will take that into account and then as per control 1.0 uh which really released uh some months ago we also have this optimized performance flag uh which will just make things faster and you don't have to take uh you know you don't have to tweak some parameters uh yourself it will just get the fast execution running where and it

will also do like parallel Branch exploration uh which you know you can set the number of how many branches do you want to explore concurrently again this depends like the number of branches that you can and Export concurrently will depend on on you know the the hardware that you're running this with but yeah just keep that in mind okay so you just control proed something and it passed or failed um now we need to inspect what control uh gave us back right so we have basically two exploration commands one is control view K CFG which is a terminal UI uh interactive viewer where you can click on the different nodes and see the different uh State snapshots that they

took uh and there's also a control show with just plain CLI output um and also uh we introducing K as a service which it also gives you a web view of of your proof and it's it's a very nice web view um and and so yeah more on that also later um once you seen what your proof looks like you can also do some manipulation um which basically means you can remove nodes you can you know say I don't want to explore this Branch anymore um we'll see some some more of that later but I just want you to get with like the main part I want you to to go with it's like

you really can inspect everything you want about your function execution with control then you can you know manipulate what the snapshot looks like um and and and start reasoning from there so maybe you're like a bit like this after you know all this all this mambo jumbo so just remember what we're doing here basically just these different steps where we're either including lemas they're they're we're we're proving and then producing these these uh symbolic execution trees and then we're manipulating them we're expecting them we're doing a lot of things with them and out of all that interaction we can write new lemas uh that will make or proofs Advance

further okay so now let's let's apply the verification cycle uh that we just shown we're being we're going to be working with um with this example uh which it doesn't look very super interesting at first but it will tackle the whole thing um and and it's a very I think it's a very complete example as in how is the complete usage of control looks like right so this basically is just you know adding numbers from I from zero to to n um so we start with n then we have these two these two variables set to zero then we go into this Loop that you know we

just add one to to I and then add I to result and then we return result right so what we expect intuitively is that you know Su to n of of n it's actually the uh well adding uh numbers from zero to n which coincidentally this this has a very nice mathematical close formula which is this one uh we won't be proving we won't be showing this in the proof of this statement in the talk there's a very nice post that that um that R here recently uh did uh about formal verification on on loops and the proof is there so I encourage you to go to our blog post page and and find it um and so

after looking at this we would expect that you know our specification for for the prove some to and look something like that right so with this in mind we can just build it and then just try to prove it and as I said before control by default doesn't bound any loops and and sum to n is basically just one Loop and so what we would get if we just execute what we have here it's something like this uh so this is the the execution tree sorry the the symbolic execution tree that I was talking about earlier uh so basically you just get this this notes which are just snapshots of what you have and then basically here you can see a jump ey this so the thing also in

control is that you're you're working with evbm bite code so even though you write your testing solidity what you're actually verifying is what the what you're what your code is actually being compiled to um so here we we see that we are entering the loop uh with this with this jumpy instruction and we also see that we're checking if n is less than zero so basically what this is checking even though we we this is not exactly the condition that we put in but the compiled code what it's doing is checking should I exit the loop or should I continue and enter the loop right and so it's checking is it n less or equal than zero so should I just exit and then control just branches right this is symbolic execution so then control just says hey I don't know if n

is less equ zero n is a symbolic variable so let's just suppose on the one hand let's just suppose it is and then if it's Leal zero it just exits the loop we can see it exiting the loop here and then it just says okay then I I just finish so for this Branch you know I do get to a successful State and your test passes and then it goes on and says okay what if actually n is greater than zero then we enter the loop and then we execute a bunch more and then you know we do one iteration and we say Hey Now what if n is less than one then if if that's the case then we just exit and if it's not the case we're still in the loop and then control will do just will

just do that again with two and with three and with four and it will just not stop why because we have not we are not bounding Loop execution here so by default control just will start to create this potentially infinite uh execution Branch right um execution three sorry uh unless we at some point we stop it but if not as you can see it will just get bigger and bigger and bigger here is where I stopped it but and so how do we go about this um does that mean that we cannot verify this with control well luckily uh what we have here is that we can add BMC some BMC depth so we can tell control hey I take some given you know depth uh just accept

the proof like I just want to execute this symbolically and you know if it has worked for the first four iterations let's just assume it will work for the other how many it will it could have right um and so with that it will pass pass um so I executed this proof with BMC 4 and we want to see how the how the the execution tree looks in this case which it will look basically the same as what we just saw but at some point again it's here it's branching then we enter the loop and then it says oops and then it says yeah sure everything is fine and then we will do that several times and then right at the bottom

exactly and then we get here and then it's like well is N More greater than than four should I enter the loop and then it's saying well here I'm assuming it is but I would be entering the loop a fifth time so that's out of her you know that's out of her bounds and then it just cuts it and say okay I give this Pro I I for every iteration that I entered you know I completed I successfully completed the test uh in this case I'm just going to end the test here because you told me so and so that's all that's fine uh but for instance what happens if we have say a malicious sum to n and by malicious I mean like what if you know we're executing the loop but it says huh if I'm greater than four I'm just going to

give you an incorrect result right uh well the thing what what happens here is the same basically you will you will if we I think I have it here uh if we run this uh oops sorry about the live demo thing

uh yep well you can see here if you run it uh basically it will pass uh you will have the same amount of nodes um and it runs in basically the same amount of time and so here what is happening is that the the you know the the the behavior that would make this proof fail it only happens after a certain amount of iterations and so how can we basically go about this right uh yeah if we executed with this basically we'll just uh succeed uh so how can we solve this well we can solve this with with uh with looping variants so looping variants are basically their properties that you know are supposed to

hold before the execution of a given piece of code and after the execution of a given piece of code um you know invariants can also be trivial properties uh because something that holds before and after doesn't really need to be meaningful about your code but you want this to be something actually meaningful uh about your code code so basically a looping variant you should craft a looping variant in the sense that you should craft a property that captures what your what Your Loop is really doing um I will also say crafting looping variance it's a problem that is arbitrarily hard like this this is this is this can be very quite a challenging uh problem to face in the sense that you know for instance if you

had a very dumb Loop that it just computes you know you just give it a number and it computes the nth prime number like coming up with a looping variant for that will basically Grant you the the novel equivalent in mathematics so it's it's really like it's a it can be a very challenging um Endeavor but you know control supports it and and there are ways to to sort of automatically or Prat pragmatically come about with looping variant so let's just start forging the intuition here on on how does forging gooping variant for this look like so when we start the function we basically have that result is equal to I which is equal to zero which coincidentally it's also equal to you

know the closed formula that we hope this function to be uh equal to and after executing the the loop we would we would get that I is equal to n and then hopefully we would get that the result is equal to you know n * n + 1 ided by 2 this is what we want to actually know like this is our intuition but we don't know and so these are sort of the loop invariance uh recipe when you're looking at solidity code so you basically look at the Loop head see what you expect the state to be then you execute the loop then see how the state is updated and then you sort of want to generalize that into a property that captures you know what

what is the what are what is the state updates that your that your Loop uh ends up with this is for Sol though um for Ev um you we have to do a bit some more extra work uh because we first need to identify where the loop head is uh because that's not that's not um you know super trivial to do uh when reading U bite code and then we just again sort of inspect how the state is see how it's updated generalize it it's very important with control once you come up with what you think is a sound looping variant control allows you to actually prove that you're looping variant is correct and then basically you can

include this looping variant as extra knowledge to control to say hey my Loop takes states that you know have this sort of form and after executing this Loop it transforms it to at this different state that has this particular form and in this way what you're doing is actually you're you're effectively summarizing the actual behavior of the loop and you are sort of executing it to completion which uh you know it it gets rid of of just executing a a few iterations you're actually encapsulating the entire behavior of the loop in this uh using this invariant approach right so first we need a word about lemas

because you need to understand how to write a bit of you know K which is what control is based on in order to fit it lemas and so basically very quick um the files you know starts with some requires with which you know you in here we we import a formalization of you know how founder execution works and how evm execution works then you just have this module which where you will have your your Lamas which are like this reasoning bits that control takes to enhance its reasoning power um you import some modules and then basically there here is like the meat of the of the file which is the rules the rules sorry or lemas um so a rule basically just has the S rules

something requires something and then simplification for us a rule is something that that is a rule that has the attribute simplification but yeah basically just rule then you just write your rewrite conditions this basically means you know if you start with the left hand side of this rewrite in this case Vol toward toward X you you will rewrite it to whatever is on the right hand side so this is the rewrite symbol so this tells us that you you you start with this state and then you will end up with this other state St then you can have a requires clause which basically is just apply this you know this transition between two evm states just apply it only if the condition that goes after the requires Clauses uh is

fulfilled you don't it's not necessary to have a requires Clause but it's there in case you need it and then it's just the simplification attribute which is sort of like a particular type of of re rule that we have great so um let's prove the invariant but first let's see how this looks so we want to in this case we want to First inspect um the configuration that control has given us right um so when this loads we sort of go here uh just as a as also a note um we executed this if you remember from way before um we had this break on jumpy

instructions which basically tells when you are doing symbolic execution and you face you know a jump ey I want you to create a node which basically a note here is just I want to snapshot I want control to snapshot whatever the state is here for me to execute it and we did this because uh since we're entering a lo lo start with jump eyes so basically we just scroll down also sort of like warning sometimes you will have to aggressively scroll down or up due to the you know amount of information that controls gives you but that's just something to get used to and I think it's actually a pretty good thing so here we are um note 27 we are at a jumpi and here we are splitting so here we're

branching um tldr this is our Loop head really as we saw it's seeing if n is less or equal than zero and if it's if it's not it will just exit the loop and if it's if it is then it will just enter right so I I executed this with B C depth 4 and here our goal now is to see okay I have this jump ey here uh note four uh and this is the very first time I'm entering the loop and then if we scroll the way down we can see yeah this is where it bounded this is the last time it exited the loop uh here this is the last time it exit it exited the loop um and so

basically what we can say now it's okay uh give me so the the way we're going to come up with the invariant is we're going to see which are the state changes that happened between the first time we were uh we were entering at the entering the loop the first time we were at the Loop head and then the last time that we that we let control execute the last time it exited the loop so the way to do this um is via this uh it's via this uh control show uh node Delta so what this will basically do is it it will take to node and it will perform the difference of what what's what has changed in the evm state

between this note and this note and if you notice um we're doing it with node 54 which is the first node that's actually jumped out of the loop um so if we just do the no Delta thing it will it may take a little while to just load but it will basically give give us again the the entire configuration and then at the very bottom of it it will give us a configuration that contains the state Delta here so it contains basically what has changed between node 27 and node 54 uh and we can we can look at it by

looking at these at these arrows so B basically it said okay what what has changed is you know in the K in the K cell which basically is where the you know the evm code is executed you went from this jump ey on this condition to basically just jumping and then if we scroll a bit down everything else stays sort of the same uh and the only thing that changed as well was that in the word stack you know we started with these two variables and then we sort of we are we ar right to two and then here to three and this is for actually for for be for the second execution so once we see this our job is to say okay we we've gotten these State updates um what is the general form of

this right uh and basically that's how you you can craft an invariant with control you can just come sort of come here and say okay you know we we know we were we were here and then we jumped here that's concrete and then so first of all what we're going to do is we're going to well first craft the thing uh and then we're going to prove that what we craft is correct um so yeah basically we're just saying you know we have this sort of this state and then we're just going from here to here and then we generalized what we saw oops we generalize what we saw here into a more uh abstract formula and just saying you know from I go to n and

then from this close for form we go to this other close form the thing is this is a claim so maybe this is too detailed but what I want you to get to to remember of is this is a claim of what you're doing is you're crafting uh a state difference and then you're actually proving that the state difference holds um and this is done via this this this claim instead of a rule uh we're just saying yeah this is this is how you know the K execution cell is going to to to differ to change um there are some stuff that uh you know we want to keep um just to get to keep the rule uh actually uh well provable in the case in the sense that

you know this is how we executed this program um here is the the the main let's say source of reasoning that you want to have so the main abstraction that we're doing is coming from what is written here to what is written here and and that's that's where the challenging part of crafting looping variant comes which is you have to you have to understand your code you have to uh reason about the properties that it has and then you you sort of go from this concrete um difference to to the general form that it should uh that it should have then we have uh the same PC that that we were executing with and then you know some more stuff and then some some

well forness conditions and the thing is what we're saying now is hey this can be turned into a rewrite rule so this can be turned into basically just telling control whenever you are at this program counter whenever you are facing you know the head the loop head which is this thing that we have here just rewrite it to this and then you know the general behavior of my Loop is going to be this transition right and with this claim what you're actually doing is telling control prove me that this is correct so this is not giving the user like you just write whatever and then control will just take it you're just able to you're actually able to take control and

say just prove that this state transition is actually accurate and that it works um and then you just you know you you can translate this into a rule once you have proven it correct um which basically means just taking a bunch of other constraints and putting it in the button but basically you end up in a loop in which you know you actually like you have the state transition and this captures the actual behavior of of the loop of the of the while loop that we were facing with um once you do it uh it you can actually prove the statement without any BMC depth so it will be capturing the loop behavior in full um and yeah and that's how you

that's how you basically can verify a loop with control um we this we have used uh in in in our engagements uh because also there so we have been dealing with a very like on the face kind of loop um but also for instance there are some Loops that are inserted by the compiler um not with the recent with the mo with the latest one since we have now M Copy but it was the case for for I think it was from solity 0.824 previously if you had like a bytes memory argument you will like the compiler will insert their all Loop that you will need to reason about uh and so for instance

this this lets you reason about it uh in full generality so I hope you you you are excited to try control I try to show here uh from you know going to from the basic use to actually show you an advanced uh example of how of how to use control uh we have I think we have killer documentation on this uh you you we we also you can also have control on your CI um so please feel free to to to go to the documentation read it and we're also very responsive and active uh so if you want to get in touch with us uh feel free to come to our

telegram channel to our to our Discord uh we're we're more than happy to hear from from from our users and so thank you very much for attending this talk [Applause]