[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