Tadeas Kucera, Jaroslav Bendik / DCxPrague

Transcript

uh yeah thank you uh hi everyone uh I'm this is uh today we would like to just very briefly explain what is the pr how it works and then we will show you some particular examples like we will work with particular smart contract to verify right and properties and it's also because our to recently become free to use so anyone can use it in some restricted mode but you can use it so I hope that you will actually use it to verify your contracts so let me start um our approver uh takes U some smart contract usually written in solidity and some specification and it somehow decides whether the specification holds or not

if the specification holds we can give you some mathematical guarantee that it holds if it is valuated we can give you like execution of the smart contract that valat the specification now the specification it can be something like if you execute function transfer then it actually transfers the right amount of tokens to the right address okay okay this can be like piece of the specification um we have our custom specification language it's called set verification language and you write the specification in this language and we will see some examples later um we can sometime time out because we are doing formal verification the formal verification means that we really check all the possible executions of the smart contract if any of them can violate the

specification or not so it's like it's not testing it's not fuzzing we are everything which means it's more expensive from the competitional time of view point of view and in my timeout but it gives you some additional guarantees okay that's the that's the difference maybe um and the nice thing is that once you write the specification and you made changes to your code you can run the pro again against the specification so either you write specification you integrate it into your CI tests and you know whenever you make some changes you check again if the specification still holds or not so that's like the idal use of C approver now very briefly how it works um so this is the like architecture of the approver so I'll just go briefly

over in steps and then we'll see the demo so the first step is that we take the um solidity code we compile it to bite code and uh the reason is that you uploaded bite Cod on the blockchain right and there are different compilers they produce different bite codes sometimes there are bus in compilers and we actually found some bugs in compilers because using some compilers this specification was proved and using other compilers the specification was violated so we have to work with re bite code now the issue is that the bite code is um It's Not Human readable it's hard to automatically process because it contains too many instructions um you cannot easily map it back to the solidity I mean there are

some de compilation step and if you find some valuation we want to tell the user hey that is this you know this is the the violation but we don't want to show this on the bite code we want to some my be back to Sol so there are some complications but we have to work with the bite code to make sure that we verify the code that is on the blockchain now what we do next is that we take this bite code and we convert it to our custom code representation we call it three address code and um basically the motivation is to uh make it easier for the Prov because of this three add code it's uh it's simpler it is it is using only a small number of instructions these instructions are easy so it's easier to autom ially analyze these programs and also it allows us to

actually support other inputs so everything that compiles to evm can be supported by our tool and also if you compile like let's say Solana to our three address code somehow you can also verify it using our our tool so that's like the uh motivation for having our custom three address code representation good um next step we take the specification and we add it to this three add code so we basically somehow match the specification and match the program and we actually turn the specification to assertions in our program so at the end it's about U find out if you can reach and violate an assertion in our three address code

that's the verification task now we are just checking assertions basically okay um next step we uh take this three add code and we simplify it to make it easier for the for the Pro so we do things like points to analysis if you have heard about this before uh we do some slicing some value range optimization so for instance you might have a variable let's say x it's U so it can have many values right and we are doing this form verification we are checking for all possible executions all possible values of variables but perhaps X is always between 0 and 10 if it's someone find out it can simplify the verification task for us okay so we do this like analysis of the program and

some simplifications um I have an example of slicing so there's like a oh it's at the bottom I'm not sure if you can see the program at the bottom can you see it a bit okay uh maybe I can just read it so it's very small program there are two variables it's these are structures X and Y okay and there's some internal variable F and you set set X F2 one y F2 2 then you change the value of y and then you have an assertion about X and the thing is that uh why is irrelevant because you are talking just about X in your assertion and now you know if this is the specification is assession it

basically me that you don't care about y about the variable Y and about like operations related just to Y so you can just remove it from the program you get something smaller and then it's easier for the for the prover so this is like an example of transformation simplifications that we do on the T representation and then uh we are almost done so we take this program and we encode it to logical formula so intuitively the formula says that there exist initial values of variables of the program such that after the execution the assertion or an assertion is violated this is our logical formula and if you can satisfy this

formula it's like a mathematical formula or some variables functions okay if you can satisfy this formula it means that there is an execution of the program devel specification right so and we can map it back to solidity and it's like the you know C example to your specification and if you cannot satisfy this uh formula you're okay like your specification cannot be violated by any possible execution of the smart contract and the uh very next step is that we uh take this formula we convert it to something called smt it's like a input for some solvers for logical formulas then we just apply this SM SM solver which are developed by universities or by Microsoft for instance and we check if deforma is

actually satisfiable or not and if it is satisfiable we get the execution of the smart contract that validates the specification if it is not satisfiable we have this guarantee that there is no execution that violates the specification that's it it's uh sounds very easy right uh the idea is simple it's it's not so easy but that's the idea behind formal verification uh [Music] um sure we can ask questions now can you show the example some I will not show B code but um the rest of this session will be like actually practical demo where we will show some uh smart contract and some properties and and verify them so this is the content for the rest of the

session good um I said the uh Pro yes question how it to do back and for from it's it's not easy we we'll show this any demo it's yeah could be hard but it's somehow like yeah the compilation to bite code is hard but the like let's say the compilation to our specification language is easy because it's us so you can basically you know make some marking in the specification and then use this

information to understand the country example we will see some examples to write cont some specific way verif you can form verify any contract we cannot verify any contract because the B checking formal verification it's like undecidable problem and it's hard so even if it decidable it just time out no the thing is that you can write solid in different ways some of them are good for the pro some of them are not and for instance like you might optimize for some gas consumption and make your code ugly but efficient in some way right but if it is ugly it might be hard for dis solver so

um usually it's good to think about the formul verification where where you already when you are already writing the code to make it somehow compliant with the tools that you want to use like so I will know that it is for should be like decomposable for instance into some like sub modules and then you process into all sub modules and somehow compose the results and right um yes but you mentioned that actually Sol is is the B and on the other side is specification right so well we still map the result to solidity to show the user yeah we have some some kind of

mapping and we'll show some examples somehow different to already existing to like form verification I forgot the name you mean like in the space of blockchain or in general or e in etherum so there there are more companies that does some do some form verification like random verification Trail it's there are like many tools working on different principles and we have our like custom principle selling points of this one uh that's the question hard question

it works that's my answer it works um okay um uh if you if you allow me I I postpone this discussions we can talk after the session we want to show you how to use the tool because we hope that you will start using the tool um so just um if you open our website c.com um you can click on this get started free button and basically um you can use use the tool for free there's some limitation in like number of computational time you can use per month and also like a time limit on single usage of tool but you can use it to verify smart contracts okay like you cannot verify a for instance with like

this free version because it's like too complex um but is you can you can write some some nice specification about about contracts um another thing I want to show you maybe you will find this interesting so uh Setra is organizing these contests with Cod Arena or with a community for instance um so basically the idea is that uh anyone can uh participate in these contests and you can use the prover you write specification you are use our prover and you are trying to find bus in in this prod protocols so if you would be also interesting in this like trying our tool to find backx in you know existing protocols you can just participate in some of these context we

have a context of GMX in in December for instance or you can just use the pr on yourself using like you know this free license and verify your smart contract so these are like the the options and I hope you you will try some um I'll just skip back to the slides uh we have some documentation you will find it um but for today um we prepar this uh simple smart contract it's called English auction and that will now replace me and uh show you actually how to write the specification how to run the Tool uh how to read the resells of the tool so please welcome T thank you um hello so I'm tadash and I

would like to show you the contract uh and what can we do with it um so um this is the contract I I will try to move fast uh and break nothing as our Lo Moto says and uh the contract basically is meant for uh auctioning so when you want to start using it you call the Constructor uh and you uh supply to the Constructor the address of the NFD that you want to sell and uh nftd ID and you supply also the address of uh erc20 in which you want to accept the payment and also starting bit what you want to get

at least this amount and then uh other users can um like bid and offer their uh amounts uh to to get the nftd and whenever they bid um if uh the amount they offer plus the bids that they already offered increases uh what is the current highest uh highest bid uh they become the highest bidder and the protocol gets the amount from them so they don't run away and we keep keep the uh money so let's go through some of the functions uh there is function start yes you're right we should put it

here right right yeah thanks so you can zo uh so the start function starts the protocol uh it sets started to true it gets the nft from the uh message sender which is the seller and it sets and add to uh 7 days from now which um make makes sense that you want to the auction to last seven days then there is function set operator you can allow somebody else to withdraw your funds from the um from the contract uh we will get to it when we talk about the

withdraw uh there is bit for you can bid on somebody else's behalf so um that's what it used for that there is bit function it's basic basically easy bit you call it and uh it bit for you and you pay for it and uh the amount is used and then there is this underscore bit that's internal function and this uh does all the work bidding work so it requires the fun uh the auction to be started it requires to be still before end the time stamp should be before end and um it transfer from basically you if you call this or

from the payer I'm sorry for the from the payer it transfers uh the amount that they are offering to this contract so contract takes the amount also bits which is a internal map that uh keeps um track of what is is the bits of each person um so bits of the bidder is increased by amount there might be zero like at the beginning and there might be like thousand if they bid it before and they are increasing this amount so this amount gets increased highest bidder gets updated highest gets also updated and then there is the require so um if this um offer doesn't uh like overshoot

the previous bit then this all gets U reverted makes sense right any question just should um then there is withdraw function underscore withdraw it um takes in bidder recipient and amount and what does that um when you are not the winning the highest bidder right now then you can call it and succeed uh the highest bidder cannot withdraw their money because we are counting on them to pay right so uh bids get substracted by amount um and tokens are transferred back to the um either to the bidder or to a recipient uh and that's where um

the operator come into a role so if you assign somebody a role operator for your bidding uh they can withdraw on your behalf so that's uh the withdraw for function and then there is withdraw amount function and the basic withdraw which withdraw everything you have there so that's withdraw and then there is n function anybody can call it and it can be only executed once the auction ended uh which is here uh the time stamp must be greater than uh oh yeah the time stamp must be greater than uh than end at and uh you don't want to end your uh auction twice

and uh we also require it to be started of course and what happens inside is that the nft gets either transferred to the highest bidder and um the token that we got from them inside this contract get transferred to the seller or if there is no highest bidder meaning that nobody wanted the NFD nobody gave enough money then the nft gets transferred back to the seller so this is the contract and we are going to verify it uh to verify a contract in Cura we use rules and uh uh

rules are um like uh properties written somehow I will show you how and uh when verifying we check that any possible scenario any possible run through the contract calling multiple functions and and stuff uh always these properties will hold so it's not unit testing you really test for any possible setup uh if you write it correctly and let me yes what language is it uh this is CV it's our internal language you have Maring for for

ID markings for ID I uh what is marked I mean like Ru uh oh Oh you mean this comment that's my comment uh yes we we also have we also have syntax highlighting for the language yeah it's CBL with syntax highlighting we wrote that yes thank you yeah yeah yeah syntax highlighting um okay so this is the first rule I would like to show you it's a rule

that uh takes any recipient any address uh any amount okay and any state of the contract so this environmental variable n e holds time stamp message sender and uh it holds message sender so you can pass it the e to a function of the contract which is here with draw amount right here okay uh as a first parameter so with withdraw amount actually usually takes just two parameters but but in CBL here it takes one more e and it uh contains cender of the message and time stamp and much

more so uh here we remember the bit before that's uh like what the e- message sender the one that will send this message uh had in their bits before and then we execute withdraw amount with this uh modifier which uh I just used to make sure or to track if the function reverts or not and uh so so we we execute this function and then we claim bit before is less than amount then this had to revert what does it mean you cannot withdraw more than you

have in your bits makes sense but uh not in some scenario in all scenarios so that's one rule um any questions regarding this rule so let's see another one uh let's see this one this one is the uh next easy rule um this is invariant um invariant are uh properties that you want to be preserved so it's just statement that you want to claim that it is preserved in all uh runs the beginning and then everywhere uh what this invariant says

is that either the highest bidder is zero which is at the beginning or if the highest bidder is some a uh then it means that bits of this a of the highest bidder are equal to highest bit okay we also want to make sure that the bit that the programmer uses the map keeps like like is is um uh in harmony with the highest bit that they also use okay every rule uh with with every possible run of the of the contract so

we will uh run all the r all the rules and all the invariant with the contract and we will see if it passes or notun okay yes yes so um the syntax of invariant is a bit like hidden it's you don't have there the function call as I showed you in the rule but it happens essentially you what you claim here on the two lines is just some kind of property and if you run the invariant you claim this property is preserved whenever you call anything at the beginning and later um so that's what this invariance says highest bidder um bits of highest

bidder is equal to highest bit or it's zero at the beginning um I want to show you one more Rule and then we switch to to the tool so this is Rule Integrity of bit um it's quite long but the essenti what it does is it checks the bit function and uh if you succeed to bit uh this rule says that the bidder becomes the highest bidder and their balance like the bits of of them uh should be updated accordingly but uh It also says uh another example like when bit before

plus amount is less than the current highest bit it didn't succeed let's go let's go from the beginning uh we have this filtered blog here uh we have method F we have environmental variable we know what e is that collects like the message sender and um the time stamp uh it's good we will use it to call the function with any arbitrary U State because e can be arbitrary also F can be arbitrary uh arbitrary function but we will filter some out here um that's what the filter does it uh it only accepts

functions bit for and bit okay so this rule doesn't take uh into account any function only bit for and bit uh and what it does is that it takes any amount thanks it takes any amount any address for the bidder it computes the current highest bit before the call it computes bit before before the call and then it also add one more require on the bit function you require that the bidder is the message sender because um

yeah let's let's go further uh then you also uh assign success uh to the result of this call so you call the bit function um you cannot see here uh that I'm calling bit or uh bit or bit for but um the function this is just a wrapper that we have uh up there uh it's easiest easiest things so so here we call the function with uh any arbitrary state of the program amount and bidder we know what bid after is and then we claim this assertion that if the

bidding was successful then the bit after equals to amount plus bit before and the bidder is the highest bidder right now and we also claim that if bid before plus amount was less than current highest bit then we didn't succeed actually uh we could even claim U like more we could claim if the bit before plus amount is less or equal than the current highest bit we didn't succeed but this rule is also fine it's just a little bit weaker but it will do its work so uh we we've shown three three rules of many here I've shown you the contract and now we

want to see uh what it uh what it did what what we found with verification so it took 1 minute and 50 seconds here and I will zoom in a bit and um what happened is that everything got green except for these three uh for which we claim that those rules are um uh easily U by toy it's obvious that they are met so this contract uh full fills each and every of the rules it it doesn't have bugs uh well at least uh these rules don't find it and actually yeah it's

it's buckless but uh we made uh some um modifications to the contract we added some bugs for the purpose of this Workshop um and we will now go through verification of these bucked contracts um and uh see what the tool can do so um let me first show you the code the the bugget code uh of this one uh here is a critical bug we we added unchecked block to the yes scroll down thanks we added uncheck block to withdraw function so the bits of the bidder is decreased by

amount but uh unchecked means that it can also underflow so uh let's see if the suit of our rules can catch this problem this is all green but here we see some rules failing and uh we have explained what Mortal withdraw amount rule does so let's uh have a look on the violation this is the rule just to remind you uh what it was about so it took recipient amount bit before then it

executed the withdraw amount and then then it claimed that if the bid before was smaller than the amount so the user was trying to get bigger amount that they had in in the contract it reverted it seems like this uh failed so let's let's see why okay we have the violation bit before is less than amount but it didn't revert and um corresponds yes yes yes thank you so uh this is uh like a run of the uh of the contract which got violated so um as

this rule the Mortal withdraw amount was violated with this contract we obtained the call Trace and it begins with global State setup um then bit before that's like um in in the code we had um bit before that that that's it okay so assignments to properties and this is the call trace a tree that shows up what uh what happened and uh yeah here is see violation and it corresponds with what we seen in the

code that uh was bucked and that the bits of the bidder uh got increased below so uh let's let's see we see that bid before is zero so the user didn't have any bit any balance but they was they they were able to withdraw one amount amount is here and know that amount was withdraw here so uh here bit before uh was Zero we withdraw an amount which is one and then it failed

um coverage coverage no no no um uh no we don't have that metrix but uh um uh how would you uh differentiate

the cular approach to the invariant testing which we have in found framework uh we use uh set solers SMD solers yes yes please M so the question is how is the Satur approver the def from the using tools like Foundry or so first of all we are planning to integrate with these kind of

tools there there are multiple difference one is that in foundary you specify the correctness in in solidity which is nice we specify the correctness in CVL CVL is a very expressive language for example you can talk about quantifiers you can talk about ghost you could out things that you are not expressible in programming language because we're not implementing it we are telling you what's the property like these high level properties we so we have a very powerful specification language that you can I think people are planning to integrate it into Foundry the other difference is the technology the technology is very very different and what it gives you very different in in Foundry you're starting your Cod from starting from initial State we are

starting from an arbitrary State this has downside and upside it's like proving things in mathematic by induction we start from a state that that arbitary state that satisfies the environment and then we we see that arbitary pass yeah so we are not we are exhaustive that's why we usually we are 100 times or thousand times slower and we are consuming all these Amazon machines whatever it's it's much more expensive procedure but we can show you certain bugs that we have found for example in the sushi or in the other which are Beyond reach for I mean people usually find them with but after a human have found the error and then they

replicate it it's very different this you put it to the machine and then it's it it gives this thing okay good second question which will be related if you may um I think you can still stay here because that will be also ready to you sorry sorry for grabbing the attention and it is uh during the panel we discussed over here that there are more interesting bucks and mistakes uh considering the systemic risk so when we like chain the different protocols together and then there is in in the different protocol that there becomes the change and it can influence whatever we are building on the other side uh currently Frameworks like Foundry and and hardhead it it's very

hard to simulate these you know uh not by the fact that we can roll in the the the those already on chain protocols in into the testing this is solved but but uh those systemic risks it's very hard to make the tests for it right we typically do like unit tests or we could do the fuz tests or we could do the invariant tests but regarding the systemic risks of the whole like blockchain landscape that's very hard to predict design and so on so we do not have a tool in in in in in these Frameworks for that does c somehow solves that for us at least partially yeah so the it uh so the the

answer is that it's it's partial in the sense that what we usually do when you write the setup you say which function is calling which function and then we actually analyze all the interactions and we have a mechanism which we call summarization if you if I'm calling your function and I don't know what it is I can say that it has an arbitrary Behavior so you could actually prove something like with respect to we have for example verified the compound with respect to arbitrary called to UNIS so we have specific cases that we have done it but we only what I said we only analyze the code and the interaction and there's a limitation so for example if you if we if we made certain assumption

about your function how it's called and then you are changing it then in fact we only verify the piece of code and that's our verification is not valid so and usually when we do the setup we we we make certain assumptions we make certain assumption say when I'm calling your function your function is monotonic it means I don't know what it does but at least every input if you give us larger input it give you larger output so and this this assumption we can try to check it when the code of the Ki of the function which is called is available but what if it's not available or what if it's available and later it is Chang I don't know if I I got you so the

answer is partially yeah partially exactly okay maybe I can also add that U you can basically Define some interface that should be implemented by all the contracts that connect to your contract okay and we can do the verification against this interface and then whenever you connect to new contract if it satisfies or implements correctly the interface then you should get the guarantee but it's you know when we when we do the verification if you don't know the future contracts we cannot verify against those right like precisely against those contracts but if you find out that we only actually need like this particular piece of interface to guarantee some properties and we don't care about like the other behavior of

the contract du connect this this is okay so this is what we often do like we somehow just abstract the connected contracts and work with this abstraction um I can give a a little bit more like concrete example of this sort of like systemic risk and I don't know if you are guys aware of the liquidity protocol uh that's highly emittable uh stable coin on chain but not highly it's immutable it's it's like governance free so very sexy protocol I would say but there is one there are two dependencies one dependency is on chain link and the other dependency is on Teller right when it was built and actually

released um already audits everything it was perfectly fine and and and you could like create a test to to whatever would be happening to towards the LUSD protocol and it was perfectly fine uh what was ommit that was the fact that actually Tor in the in the future you know at that time in the future uh was changing something uh a little bit I guess and it actually uh happened at at the moment that that there was like a fallback from the channeling towards the teller and then they realized that it's not working you know and the consequence was that you cannot change the liquidity protocol because that that was immutable

and actually without any proxy so it was literally immutable so they had to do some changes on the toer side you know uh but this is the part of the chaining the protocols and the systemic r that something happen somewhere else and then influences your imitable protocol that's why I'm I'm giving you the example like the really real life concrete example which we have here on blockchain with all the data and with all the experiences all of that and I I'm I wonder whether CA could help help us in in this sense in some way it's just open for further discussion whatever you know um yeah you you need to keep the contracts in the loops so you know if if

contract you are using is changed you need to rify again basically but once you know once you write the rules you can just run it again it's not like that you need to audit it completely again um sorry that we are having this discussion here but I think it's it's it's very important because we are talking here about a whole like you know defi uh security basically uh what I am aming to is that typically when we work on the projects we we we prepare even the tests in some like isolated in the scope isolated manner that we like certain those test Sur the protocol with those tests right and here we have the option Mr set that actually you you have

there already several protocols not only one right yes you have like many many protocols so isn't it a chance and I forget now the centralization or decentralization right uh wouldn't be that the chance to actually trying to um address this systemic risk that once you have those protocols there and then you can see even the changes on chain that something is being posted there as being changed that you can like foree the potential risk the systemic risk you know the impact on the other protocols and that you could like uh like trigger some wording or notification look there there is being something happening here in the D5 and could influence something else somewhere else in the D5

uh so um two things uh we would like to finish the tutorial that's one thing um so just Bri answer to this and then I hope we will have discussions later we are ready for these discussions we want to have these discussions with you um so we just say that um yes to me it makes sense so for instance like if if you do some verification and you rely on some other contract and you have these like current assumptions reasonable assumptions about that contract and the verification is fine perhaps you can contact the other company right the authors of the other contract and say hey we had these assumptions they are like really reasonable for us are they also reasonable for you and if yes then maybe the other company will you know try to comply with those assumptions in the future as well but it's nothing that

we can like as a security company to enforce it's about the authors of the of the protocols if they like you know make some danger changes in the future not but you can be the facilitator of this discussion that's my point so we are proposing to U develop a new tool that would keep track on all changes of blockchain and notify people if there is some some change but that's not really um um like we we are doing formal verification and we are we are doing Audits and you are proposing okay mly said that there are

tools in the ecosystem for this I don't know that tools so uh uh from one one point I I don't want to close this discussion on the other hand I would like to finish this um maybe we can get back to this l in in the in the schedule today I'm not sure what is the sh but maybe we'll have some time for discussion later so I mean it's it's interesting um Tash please continue yes uh so I have another mutation here so we modified the code again introduce the bu and here is the output that the pro created uh this time I would like to go first through the output and then look

at the code so what did happen here is that we got some violations uh let me choose highest bit versus bits because that's the rule that we were already talking about um so it failed here it failed on preserve and it fail on preserve with the withdraw four and withdraw function withdraw amount let's have a look what's broken so um to remind you what this uh rule was was about um this this is invariant and it it what it does it it checks that the highest

bidder always means that the bits of him are the highest bid or the highest bidder is zero which is the initial state so this was broken let's see why um we see this address that it's highest bidder we see that the highest bid is one but bits of the highest bidder is zero and we know that withdraw function was called we've seen it there we see it here so withdraw function was called um interesting thing is who called it we

see that this address 2 d86 is the same one as here so we see that the highest bidder called withdraw function and then what happened is that even though highest bit is one the highest bidder has zero bits so it it does a lot of sense to us now we we know where should we look for the bug and we go to the withdraw function and we see see that if the highest bidder calls this like or if it's called with bidder being the highest bidder um we do check

that that that uh this doesn't happen because you don't want the highest bidder to withdraw their money they they would um get the NFD and not pay for it but somebody added this if here if it's not ended so what happened was that after end of the F uh auction U the highest bidder collected their uh their tokens so that's the buck and we also introduced different bugs so right here we have this bug so the highest

bidder was set to bidder it's always when you bid you want to set the highest bidder to the bidder but here somebody wrot payer which is a mistake let's see if we see the the buck uh from the verification so here it took 2 minutes precisely and we have uh rules that failed and this time uh this time I'd like to choose Integrity of bit Yeah because that's the one that we talked about so Integrity of bit failed for the function bit let's

see uh what was the rule saying and the rule was saying that um when you bid in the end if the bidding was sucess successful then the bit gets updated so bit after is bit before plus amount and the bidder gets updated like the highest bidder gets updated to bidder if it fails we have this other assert that says that when when actually bid before plus amount is less than the current highs bit it won't succeed and this was broken

here so in the call Trace you start with arbitrary State uh you compute the current highest bit which is one then uh the bit before of of the bidder bidder is arbitrary in the rule is zero and then you call the bit function and the bit after is two and you would assume that uh if it was successful then this is uh

fulfilled but it seems it it wasn't so what happened here is that uh bit after was equal to bid before plus amount but the bidder is not the highest bidder and it resonates with the bug that we seen because here we see that the highest bidder wasn't set to bidder but the payer okay so that's another critical bug and uh I have five more minutes for like s so yeah yeah I thank you for your attention if you have any questions um please

ask okay no question thank [Applause] you