Proving liquidity of an AMM by Jochen Hoenicke | Devcon SEA

[Music] yeah I'm Y and I'm former verification researcher as sator should I use this one this one okay so um yeah and I want to show you how to prove that your contract Can't Get Wrecked so uh let's remind ourself what an amm is we want prove uh a property for a decentralized exchange namely that uh yeah that has two major actors the traders who want to sell or buy tokens and there are the liquidity providers who provide the tokens to be sold on this amm and the liquidity providers rely on the correctness of the amm so the amm smart contract holds all their funds and custody and the tokens are automatically traded and if there is a bug in the amm then the liquidity providers don't get their funds back and we want to avoid that so the desired property that we want to uh show is that the money can always be withdrawn from the contract even if there's a bank run if everyone wants to get the money back uh it can be withdrawn and we need two properties there is enough money in the contract and uh that withdraws never revert and we did this for the new upcoming uh version of Unis swop Unis swop V4 and this is a contract that has a few scary features namely it's permissionless everyone can use it everyone can create pools and all the tokens of all the pools are kept in a single contract so if there's a single pool that is uh broken then it affects all other pools and uh there's also a hook mechanism so you can create your own hook for your pool that could affect this uh security of your funds and we need to prove that this is not the case so there are um some attack vectors like malicious ac20 tokens and hooks that we need to con uh s what we did is now formal verification and uh yeah what we do is we take the bite code of the contract and we take the specification and we translated with our tool to formula that we then run through various smt servers CV C5 and C3 and this will give us either a proof that the contract satisfies a specification or it will give us a counter example or because this is the logic is undecidable that we use it can also time out we have some assumptions for the unknown codes so we support arbitrary es2 tokens but to prove liquidity we need some assumptions on them so the balance can only change by transfer and burn um only the owner and approved uh accounts can transfer there's no Central author Authority that can steal our tokens we need other assumption that uh if you transfer the only the amount is transferred so if they are fees the receiver pays them and uh that transfer never reverts thanks um the transfer never uh reverts if there is enough balance and for hooks we need the assumption that there is no withdraw hooks otherwise we can't prove that you can withdraw so what we do is um an inductive invariant so we want to we split our States into two kinds of states where we have enough funds and where we don't have enough funds and if we look at all the transaction then we look is there a transaction that goes outside the circle and we found with our tool that there is such a transaction but it's actually a transaction that is not reachable so we need to refine our invariant we need to say um additional things like that the contract also does a consistency accounting of the liquidity and if we do this then we get the that all the transactions stay in this inductive invariant there were some problems with verifying this Unis SW it was not as simple as I just made it so we had some problems with rounding errors break the invariance and other things like sums over ticks and positions we solved all these problems I can't go into the details because it's lightning talk so to summarize what we showed is enough funds and consistent accounting is an inductive invariant yeah thank you one thank you it's a amazing uh research and so we have one question and I'm also very curious how many human hours did you guys spend to prove liquidity of uniswap 4 and if they're like maybe you can uh put some price tag on it because I think this is very interesting because before like on the panel before we were wondering about you know this kind of yeah I I don't have Thea price tech I'm not sure if I even allowed to tell it um but we spent several weeks with a small team so several people on this contract so I think it was something like six weeks six weeks yeah wow and uh how big the team was like three people five um more like I think over five uh but less than 10 okay interesting and uh how many errors did you guys found one one such case where this transaction can lead to in not enough liquidity right um we didn't find the liquidity error so the code was quite good there was mhm slightly problems like you can't trade to the minimum price and you can't reach the minimum price but if you start there it's possible to start with this price so there was some inconsistency there okay so we have one more question could you briefly touch on how you approach dealing with the rounding errors in yeah so we use um we use a we use fix Point arithmetic and we use a very high Precision because we have unmounted integer we can just use uh some multiplier for fix point that divides every number and then we don't get division uh roundings okay thank you very much for interesting talk please give another round of applause to our speaker