WEBVTT
Kind: captions
Language: en

00:00:01.110 --> 00:00:08.629 align:start position:0%
 
[Music]

00:00:08.629 --> 00:00:08.639 align:start position:0%
 
 

00:00:08.639 --> 00:00:10.310 align:start position:0%
 
yeah<00:00:08.880><c> I'm</c>

00:00:10.310 --> 00:00:10.320 align:start position:0%
yeah I'm
 

00:00:10.320 --> 00:00:13.669 align:start position:0%
yeah I'm
Y<00:00:11.320><c> and</c><00:00:11.679><c> I'm</c><00:00:11.840><c> former</c><00:00:12.240><c> verification</c><00:00:12.920><c> researcher</c>

00:00:13.669 --> 00:00:13.679 align:start position:0%
Y and I'm former verification researcher
 

00:00:13.679 --> 00:00:14.789 align:start position:0%
Y and I'm former verification researcher
as

00:00:14.789 --> 00:00:14.799 align:start position:0%
as
 

00:00:14.799 --> 00:00:17.830 align:start position:0%
as
sator<00:00:15.799><c> should</c><00:00:16.000><c> I</c><00:00:16.160><c> use</c><00:00:16.440><c> this</c>

00:00:17.830 --> 00:00:17.840 align:start position:0%
sator should I use this
 

00:00:17.840 --> 00:00:22.269 align:start position:0%
sator should I use this
one<00:00:18.840><c> this</c><00:00:19.080><c> one</c><00:00:19.520><c> okay</c><00:00:20.400><c> so</c><00:00:21.160><c> um</c><00:00:21.680><c> yeah</c><00:00:21.840><c> and</c><00:00:22.000><c> I</c><00:00:22.119><c> want</c>

00:00:22.269 --> 00:00:22.279 align:start position:0%
one this one okay so um yeah and I want
 

00:00:22.279 --> 00:00:25.189 align:start position:0%
one this one okay so um yeah and I want
to<00:00:22.400><c> show</c><00:00:22.640><c> you</c><00:00:22.840><c> how</c><00:00:22.960><c> to</c><00:00:23.480><c> prove</c><00:00:23.920><c> that</c><00:00:24.199><c> your</c>

00:00:25.189 --> 00:00:25.199 align:start position:0%
to show you how to prove that your
 

00:00:25.199 --> 00:00:27.509 align:start position:0%
to show you how to prove that your
contract<00:00:25.800><c> Can't</c><00:00:26.119><c> Get</c>

00:00:27.509 --> 00:00:27.519 align:start position:0%
contract Can't Get
 

00:00:27.519 --> 00:00:31.710 align:start position:0%
contract Can't Get
Wrecked<00:00:28.560><c> so</c><00:00:29.560><c> uh</c><00:00:30.080><c> let's</c><00:00:30.560><c> remind</c><00:00:30.960><c> ourself</c><00:00:31.560><c> what</c>

00:00:31.710 --> 00:00:31.720 align:start position:0%
Wrecked so uh let's remind ourself what
 

00:00:31.720 --> 00:00:35.270 align:start position:0%
Wrecked so uh let's remind ourself what
an<00:00:31.920><c> amm</c><00:00:32.399><c> is</c><00:00:32.640><c> we</c><00:00:32.759><c> want</c><00:00:33.360><c> prove</c><00:00:34.360><c> uh</c><00:00:34.680><c> a</c><00:00:34.840><c> property</c>

00:00:35.270 --> 00:00:35.280 align:start position:0%
an amm is we want prove uh a property
 

00:00:35.280 --> 00:00:39.350 align:start position:0%
an amm is we want prove uh a property
for<00:00:35.879><c> a</c><00:00:36.079><c> decentralized</c><00:00:37.120><c> exchange</c><00:00:38.120><c> namely</c><00:00:38.600><c> that</c>

00:00:39.350 --> 00:00:39.360 align:start position:0%
for a decentralized exchange namely that
 

00:00:39.360 --> 00:00:42.510 align:start position:0%
for a decentralized exchange namely that
uh<00:00:40.360><c> yeah</c><00:00:40.640><c> that</c><00:00:40.840><c> has</c><00:00:41.000><c> two</c><00:00:41.200><c> major</c><00:00:41.559><c> actors</c><00:00:42.360><c> the</c>

00:00:42.510 --> 00:00:42.520 align:start position:0%
uh yeah that has two major actors the
 

00:00:42.520 --> 00:00:45.350 align:start position:0%
uh yeah that has two major actors the
traders<00:00:43.360><c> who</c><00:00:43.800><c> want</c><00:00:44.000><c> to</c><00:00:44.160><c> sell</c><00:00:44.440><c> or</c><00:00:44.600><c> buy</c><00:00:44.879><c> tokens</c>

00:00:45.350 --> 00:00:45.360 align:start position:0%
traders who want to sell or buy tokens
 

00:00:45.360 --> 00:00:47.750 align:start position:0%
traders who want to sell or buy tokens
and<00:00:45.520><c> there</c><00:00:45.719><c> are</c><00:00:45.879><c> the</c><00:00:46.039><c> liquidity</c><00:00:46.760><c> providers</c>

00:00:47.750 --> 00:00:47.760 align:start position:0%
and there are the liquidity providers
 

00:00:47.760 --> 00:00:50.670 align:start position:0%
and there are the liquidity providers
who<00:00:48.000><c> provide</c><00:00:48.480><c> the</c><00:00:49.199><c> tokens</c><00:00:49.680><c> to</c><00:00:49.879><c> be</c><00:00:50.079><c> sold</c><00:00:50.480><c> on</c>

00:00:50.670 --> 00:00:50.680 align:start position:0%
who provide the tokens to be sold on
 

00:00:50.680 --> 00:00:53.590 align:start position:0%
who provide the tokens to be sold on
this<00:00:50.960><c> amm</c><00:00:51.960><c> and</c><00:00:52.120><c> the</c><00:00:52.239><c> liquidity</c><00:00:52.879><c> providers</c>

00:00:53.590 --> 00:00:53.600 align:start position:0%
this amm and the liquidity providers
 

00:00:53.600 --> 00:00:57.069 align:start position:0%
this amm and the liquidity providers
rely<00:00:54.160><c> on</c><00:00:54.320><c> the</c><00:00:54.480><c> correctness</c><00:00:54.960><c> of</c><00:00:55.120><c> the</c><00:00:55.359><c> amm</c><00:00:56.359><c> so</c>

00:00:57.069 --> 00:00:57.079 align:start position:0%
rely on the correctness of the amm so
 

00:00:57.079 --> 00:00:59.389 align:start position:0%
rely on the correctness of the amm so
the<00:00:57.280><c> amm</c><00:00:57.800><c> smart</c><00:00:58.160><c> contract</c><00:00:58.680><c> holds</c><00:00:59.039><c> all</c><00:00:59.239><c> their</c>

00:00:59.389 --> 00:00:59.399 align:start position:0%
the amm smart contract holds all their
 

00:00:59.399 --> 00:01:02.069 align:start position:0%
the amm smart contract holds all their
funds<00:00:59.640><c> and</c><00:01:00.039><c> custody</c><00:01:01.039><c> and</c><00:01:01.199><c> the</c><00:01:01.359><c> tokens</c><00:01:01.719><c> are</c>

00:01:02.069 --> 00:01:02.079 align:start position:0%
funds and custody and the tokens are
 

00:01:02.079 --> 00:01:04.109 align:start position:0%
funds and custody and the tokens are
automatically<00:01:02.879><c> traded</c><00:01:03.440><c> and</c><00:01:03.600><c> if</c><00:01:03.760><c> there</c><00:01:03.840><c> is</c><00:01:03.960><c> a</c>

00:01:04.109 --> 00:01:04.119 align:start position:0%
automatically traded and if there is a
 

00:01:04.119 --> 00:01:07.350 align:start position:0%
automatically traded and if there is a
bug<00:01:04.400><c> in</c><00:01:04.519><c> the</c><00:01:05.040><c> amm</c><00:01:06.040><c> then</c><00:01:06.520><c> the</c><00:01:06.680><c> liquidity</c>

00:01:07.350 --> 00:01:07.360 align:start position:0%
bug in the amm then the liquidity
 

00:01:07.360 --> 00:01:09.990 align:start position:0%
bug in the amm then the liquidity
providers<00:01:08.280><c> don't</c><00:01:08.560><c> get</c><00:01:08.720><c> their</c><00:01:08.880><c> funds</c><00:01:09.240><c> back</c><00:01:09.840><c> and</c>

00:01:09.990 --> 00:01:10.000 align:start position:0%
providers don't get their funds back and
 

00:01:10.000 --> 00:01:11.789 align:start position:0%
providers don't get their funds back and
we<00:01:10.159><c> want</c><00:01:10.320><c> to</c><00:01:10.520><c> avoid</c>

00:01:11.789 --> 00:01:11.799 align:start position:0%
we want to avoid
 

00:01:11.799 --> 00:01:14.990 align:start position:0%
we want to avoid
that<00:01:12.799><c> so</c><00:01:13.040><c> the</c><00:01:13.320><c> desired</c><00:01:14.119><c> property</c><00:01:14.640><c> that</c><00:01:14.840><c> we</c>

00:01:14.990 --> 00:01:15.000 align:start position:0%
that so the desired property that we
 

00:01:15.000 --> 00:01:18.590 align:start position:0%
that so the desired property that we
want<00:01:15.200><c> to</c><00:01:16.119><c> uh</c><00:01:16.240><c> show</c><00:01:16.680><c> is</c><00:01:17.360><c> that</c><00:01:17.840><c> the</c><00:01:18.000><c> money</c><00:01:18.320><c> can</c>

00:01:18.590 --> 00:01:18.600 align:start position:0%
want to uh show is that the money can
 

00:01:18.600 --> 00:01:22.109 align:start position:0%
want to uh show is that the money can
always<00:01:19.000><c> be</c><00:01:19.240><c> withdrawn</c><00:01:19.840><c> from</c><00:01:20.119><c> the</c><00:01:21.119><c> contract</c>

00:01:22.109 --> 00:01:22.119 align:start position:0%
always be withdrawn from the contract
 

00:01:22.119 --> 00:01:24.190 align:start position:0%
always be withdrawn from the contract
even<00:01:22.479><c> if</c><00:01:22.640><c> there's</c><00:01:22.880><c> a</c><00:01:23.000><c> bank</c><00:01:23.240><c> run</c><00:01:23.560><c> if</c><00:01:23.720><c> everyone</c>

00:01:24.190 --> 00:01:24.200 align:start position:0%
even if there's a bank run if everyone
 

00:01:24.200 --> 00:01:27.990 align:start position:0%
even if there's a bank run if everyone
wants<00:01:24.439><c> to</c><00:01:24.840><c> get</c><00:01:25.000><c> the</c><00:01:25.159><c> money</c><00:01:25.759><c> back</c><00:01:26.759><c> uh</c><00:01:27.439><c> it</c><00:01:27.600><c> can</c><00:01:27.759><c> be</c>

00:01:27.990 --> 00:01:28.000 align:start position:0%
wants to get the money back uh it can be
 

00:01:28.000 --> 00:01:30.109 align:start position:0%
wants to get the money back uh it can be
withdrawn<00:01:28.520><c> and</c><00:01:28.720><c> we</c><00:01:28.840><c> need</c><00:01:29.040><c> two</c><00:01:29.400><c> properties</c>

00:01:30.109 --> 00:01:30.119 align:start position:0%
withdrawn and we need two properties
 

00:01:30.119 --> 00:01:32.749 align:start position:0%
withdrawn and we need two properties
there<00:01:30.240><c> is</c><00:01:30.479><c> enough</c><00:01:30.759><c> money</c><00:01:31.000><c> in</c><00:01:31.119><c> the</c><00:01:31.759><c> contract</c>

00:01:32.749 --> 00:01:32.759 align:start position:0%
there is enough money in the contract
 

00:01:32.759 --> 00:01:36.870 align:start position:0%
there is enough money in the contract
and<00:01:33.399><c> uh</c><00:01:33.560><c> that</c><00:01:33.759><c> withdraws</c><00:01:34.320><c> never</c>

00:01:36.870 --> 00:01:36.880 align:start position:0%
 
 

00:01:36.880 --> 00:01:40.389 align:start position:0%
 
revert<00:01:37.880><c> and</c><00:01:38.079><c> we</c><00:01:38.240><c> did</c><00:01:38.479><c> this</c><00:01:38.640><c> for</c><00:01:38.920><c> the</c><00:01:39.520><c> new</c>

00:01:40.389 --> 00:01:40.399 align:start position:0%
revert and we did this for the new
 

00:01:40.399 --> 00:01:43.510 align:start position:0%
revert and we did this for the new
upcoming<00:01:41.399><c> uh</c><00:01:42.040><c> version</c><00:01:42.439><c> of</c><00:01:42.600><c> Unis</c><00:01:42.960><c> swop</c><00:01:43.159><c> Unis</c>

00:01:43.510 --> 00:01:43.520 align:start position:0%
upcoming uh version of Unis swop Unis
 

00:01:43.520 --> 00:01:47.069 align:start position:0%
upcoming uh version of Unis swop Unis
swop<00:01:43.799><c> V4</c><00:01:44.799><c> and</c><00:01:45.040><c> this</c><00:01:45.200><c> is</c><00:01:45.520><c> a</c><00:01:45.920><c> contract</c><00:01:46.399><c> that</c><00:01:46.640><c> has</c>

00:01:47.069 --> 00:01:47.079 align:start position:0%
swop V4 and this is a contract that has
 

00:01:47.079 --> 00:01:50.149 align:start position:0%
swop V4 and this is a contract that has
a<00:01:47.240><c> few</c><00:01:47.479><c> scary</c><00:01:48.320><c> features</c><00:01:49.320><c> namely</c><00:01:49.840><c> it's</c>

00:01:50.149 --> 00:01:50.159 align:start position:0%
a few scary features namely it's
 

00:01:50.159 --> 00:01:51.910 align:start position:0%
a few scary features namely it's
permissionless<00:01:50.840><c> everyone</c><00:01:51.280><c> can</c><00:01:51.439><c> use</c><00:01:51.680><c> it</c>

00:01:51.910 --> 00:01:51.920 align:start position:0%
permissionless everyone can use it
 

00:01:51.920 --> 00:01:54.670 align:start position:0%
permissionless everyone can use it
everyone<00:01:52.320><c> can</c><00:01:52.520><c> create</c><00:01:53.079><c> pools</c><00:01:54.079><c> and</c><00:01:54.360><c> all</c><00:01:54.560><c> the</c>

00:01:54.670 --> 00:01:54.680 align:start position:0%
everyone can create pools and all the
 

00:01:54.680 --> 00:01:56.510 align:start position:0%
everyone can create pools and all the
tokens<00:01:55.079><c> of</c><00:01:55.240><c> all</c><00:01:55.399><c> the</c><00:01:55.560><c> pools</c><00:01:55.880><c> are</c><00:01:56.079><c> kept</c><00:01:56.280><c> in</c><00:01:56.399><c> a</c>

00:01:56.510 --> 00:01:56.520 align:start position:0%
tokens of all the pools are kept in a
 

00:01:56.520 --> 00:01:58.670 align:start position:0%
tokens of all the pools are kept in a
single<00:01:56.840><c> contract</c><00:01:57.320><c> so</c><00:01:57.520><c> if</c><00:01:57.680><c> there's</c><00:01:57.880><c> a</c><00:01:58.320><c> single</c>

00:01:58.670 --> 00:01:58.680 align:start position:0%
single contract so if there's a single
 

00:01:58.680 --> 00:02:02.149 align:start position:0%
single contract so if there's a single
pool<00:01:59.079><c> that</c><00:01:59.200><c> is</c><00:02:00.240><c> uh</c><00:02:00.439><c> broken</c><00:02:01.320><c> then</c><00:02:01.479><c> it</c><00:02:01.680><c> affects</c>

00:02:02.149 --> 00:02:02.159 align:start position:0%
pool that is uh broken then it affects
 

00:02:02.159 --> 00:02:03.670 align:start position:0%
pool that is uh broken then it affects
all<00:02:02.439><c> other</c>

00:02:03.670 --> 00:02:03.680 align:start position:0%
all other
 

00:02:03.680 --> 00:02:06.389 align:start position:0%
all other
pools<00:02:04.680><c> and</c><00:02:05.360><c> uh</c><00:02:05.479><c> there's</c><00:02:05.759><c> also</c><00:02:06.000><c> a</c><00:02:06.119><c> hook</c>

00:02:06.389 --> 00:02:06.399 align:start position:0%
pools and uh there's also a hook
 

00:02:06.399 --> 00:02:08.790 align:start position:0%
pools and uh there's also a hook
mechanism<00:02:06.960><c> so</c><00:02:07.159><c> you</c><00:02:07.320><c> can</c><00:02:07.560><c> create</c><00:02:07.920><c> your</c><00:02:08.080><c> own</c>

00:02:08.790 --> 00:02:08.800 align:start position:0%
mechanism so you can create your own
 

00:02:08.800 --> 00:02:12.150 align:start position:0%
mechanism so you can create your own
hook<00:02:09.160><c> for</c><00:02:09.399><c> your</c><00:02:09.679><c> pool</c><00:02:10.440><c> that</c><00:02:11.440><c> could</c><00:02:11.720><c> affect</c>

00:02:12.150 --> 00:02:12.160 align:start position:0%
hook for your pool that could affect
 

00:02:12.160 --> 00:02:14.270 align:start position:0%
hook for your pool that could affect
this<00:02:12.680><c> uh</c><00:02:12.840><c> security</c><00:02:13.319><c> of</c><00:02:13.440><c> your</c><00:02:13.599><c> funds</c><00:02:14.000><c> and</c><00:02:14.160><c> we</c>

00:02:14.270 --> 00:02:14.280 align:start position:0%
this uh security of your funds and we
 

00:02:14.280 --> 00:02:16.949 align:start position:0%
this uh security of your funds and we
need<00:02:14.440><c> to</c><00:02:14.599><c> prove</c><00:02:14.959><c> that</c><00:02:15.200><c> this</c><00:02:15.360><c> is</c><00:02:15.519><c> not</c><00:02:15.720><c> the</c><00:02:15.959><c> case</c>

00:02:16.949 --> 00:02:16.959 align:start position:0%
need to prove that this is not the case
 

00:02:16.959 --> 00:02:20.229 align:start position:0%
need to prove that this is not the case
so<00:02:17.239><c> there</c><00:02:17.599><c> are</c><00:02:18.599><c> um</c><00:02:18.879><c> some</c><00:02:19.280><c> attack</c><00:02:19.599><c> vectors</c><00:02:20.040><c> like</c>

00:02:20.229 --> 00:02:20.239 align:start position:0%
so there are um some attack vectors like
 

00:02:20.239 --> 00:02:22.949 align:start position:0%
so there are um some attack vectors like
malicious<00:02:20.800><c> ac20</c><00:02:21.640><c> tokens</c><00:02:22.120><c> and</c><00:02:22.319><c> hooks</c><00:02:22.720><c> that</c><00:02:22.879><c> we</c>

00:02:22.949 --> 00:02:22.959 align:start position:0%
malicious ac20 tokens and hooks that we
 

00:02:22.959 --> 00:02:25.589 align:start position:0%
malicious ac20 tokens and hooks that we
need<00:02:23.120><c> to</c><00:02:23.840><c> con</c><00:02:24.840><c> uh</c>

00:02:25.589 --> 00:02:25.599 align:start position:0%
need to con uh
 

00:02:25.599 --> 00:02:30.710 align:start position:0%
need to con uh
s<00:02:26.599><c> what</c><00:02:26.800><c> we</c><00:02:27.280><c> did</c><00:02:27.480><c> is</c><00:02:27.640><c> now</c><00:02:27.920><c> formal</c><00:02:28.319><c> verification</c>

00:02:30.710 --> 00:02:30.720 align:start position:0%
s what we did is now formal verification
 

00:02:30.720 --> 00:02:34.470 align:start position:0%
s what we did is now formal verification
and<00:02:31.640><c> uh</c><00:02:32.640><c> yeah</c><00:02:33.120><c> what</c><00:02:33.280><c> we</c><00:02:33.400><c> do</c><00:02:33.680><c> is</c><00:02:33.879><c> we</c><00:02:34.120><c> take</c><00:02:34.319><c> the</c>

00:02:34.470 --> 00:02:34.480 align:start position:0%
and uh yeah what we do is we take the
 

00:02:34.480 --> 00:02:36.350 align:start position:0%
and uh yeah what we do is we take the
bite<00:02:34.760><c> code</c><00:02:35.000><c> of</c><00:02:35.120><c> the</c><00:02:35.319><c> contract</c><00:02:35.840><c> and</c><00:02:35.959><c> we</c><00:02:36.160><c> take</c>

00:02:36.350 --> 00:02:36.360 align:start position:0%
bite code of the contract and we take
 

00:02:36.360 --> 00:02:38.589 align:start position:0%
bite code of the contract and we take
the<00:02:36.599><c> specification</c><00:02:37.319><c> and</c><00:02:37.480><c> we</c><00:02:37.640><c> translated</c><00:02:38.440><c> with</c>

00:02:38.589 --> 00:02:38.599 align:start position:0%
the specification and we translated with
 

00:02:38.599 --> 00:02:41.470 align:start position:0%
the specification and we translated with
our<00:02:38.800><c> tool</c><00:02:39.080><c> to</c><00:02:39.400><c> formula</c><00:02:40.280><c> that</c><00:02:40.480><c> we</c><00:02:40.959><c> then</c><00:02:41.120><c> run</c>

00:02:41.470 --> 00:02:41.480 align:start position:0%
our tool to formula that we then run
 

00:02:41.480 --> 00:02:45.670 align:start position:0%
our tool to formula that we then run
through<00:02:42.080><c> various</c><00:02:42.480><c> smt</c><00:02:42.959><c> servers</c><00:02:43.879><c> CV</c><00:02:44.280><c> C5</c><00:02:44.800><c> and</c>

00:02:45.670 --> 00:02:45.680 align:start position:0%
through various smt servers CV C5 and
 

00:02:45.680 --> 00:02:49.110 align:start position:0%
through various smt servers CV C5 and
C3<00:02:46.680><c> and</c><00:02:47.040><c> this</c><00:02:47.200><c> will</c><00:02:47.519><c> give</c><00:02:47.680><c> us</c><00:02:47.959><c> either</c><00:02:48.360><c> a</c><00:02:48.599><c> proof</c>

00:02:49.110 --> 00:02:49.120 align:start position:0%
C3 and this will give us either a proof
 

00:02:49.120 --> 00:02:51.509 align:start position:0%
C3 and this will give us either a proof
that<00:02:49.319><c> the</c><00:02:49.519><c> contract</c><00:02:50.000><c> satisfies</c><00:02:50.560><c> a</c>

00:02:51.509 --> 00:02:51.519 align:start position:0%
that the contract satisfies a
 

00:02:51.519 --> 00:02:54.110 align:start position:0%
that the contract satisfies a
specification<00:02:52.519><c> or</c><00:02:53.319><c> it</c><00:02:53.440><c> will</c><00:02:53.640><c> give</c><00:02:53.879><c> us</c><00:02:53.959><c> a</c>

00:02:54.110 --> 00:02:54.120 align:start position:0%
specification or it will give us a
 

00:02:54.120 --> 00:02:57.470 align:start position:0%
specification or it will give us a
counter<00:02:54.519><c> example</c><00:02:55.159><c> or</c><00:02:55.560><c> because</c><00:02:56.560><c> this</c><00:02:56.720><c> is</c><00:02:57.319><c> the</c>

00:02:57.470 --> 00:02:57.480 align:start position:0%
counter example or because this is the
 

00:02:57.480 --> 00:03:00.070 align:start position:0%
counter example or because this is the
logic<00:02:57.800><c> is</c><00:02:57.959><c> undecidable</c><00:02:58.879><c> that</c><00:02:59.040><c> we</c><00:02:59.200><c> use</c><00:02:59.599><c> it</c><00:02:59.879><c> can</c>

00:03:00.070 --> 00:03:00.080 align:start position:0%
logic is undecidable that we use it can
 

00:03:00.080 --> 00:03:01.949 align:start position:0%
logic is undecidable that we use it can
also<00:03:00.360><c> time</c>

00:03:01.949 --> 00:03:01.959 align:start position:0%
also time
 

00:03:01.959 --> 00:03:04.509 align:start position:0%
also time
out<00:03:02.959><c> we</c><00:03:03.120><c> have</c><00:03:03.319><c> some</c><00:03:03.640><c> assumptions</c><00:03:04.120><c> for</c><00:03:04.400><c> the</c>

00:03:04.509 --> 00:03:04.519 align:start position:0%
out we have some assumptions for the
 

00:03:04.519 --> 00:03:06.910 align:start position:0%
out we have some assumptions for the
unknown<00:03:04.879><c> codes</c><00:03:05.200><c> so</c><00:03:05.400><c> we</c><00:03:05.879><c> support</c><00:03:06.319><c> arbitrary</c>

00:03:06.910 --> 00:03:06.920 align:start position:0%
unknown codes so we support arbitrary
 

00:03:06.920 --> 00:03:10.390 align:start position:0%
unknown codes so we support arbitrary
es2<00:03:08.000><c> tokens</c><00:03:09.000><c> but</c><00:03:09.159><c> to</c><00:03:09.360><c> prove</c><00:03:09.720><c> liquidity</c><00:03:10.280><c> we</c>

00:03:10.390 --> 00:03:10.400 align:start position:0%
es2 tokens but to prove liquidity we
 

00:03:10.400 --> 00:03:12.309 align:start position:0%
es2 tokens but to prove liquidity we
need<00:03:10.599><c> some</c><00:03:10.799><c> assumptions</c><00:03:11.319><c> on</c><00:03:11.519><c> them</c><00:03:11.760><c> so</c><00:03:12.120><c> the</c>

00:03:12.309 --> 00:03:12.319 align:start position:0%
need some assumptions on them so the
 

00:03:12.319 --> 00:03:15.229 align:start position:0%
need some assumptions on them so the
balance<00:03:12.680><c> can</c><00:03:12.840><c> only</c><00:03:13.120><c> change</c><00:03:13.599><c> by</c><00:03:13.760><c> transfer</c><00:03:14.319><c> and</c>

00:03:15.229 --> 00:03:15.239 align:start position:0%
balance can only change by transfer and
 

00:03:15.239 --> 00:03:19.190 align:start position:0%
balance can only change by transfer and
burn<00:03:16.239><c> um</c><00:03:16.599><c> only</c><00:03:16.920><c> the</c><00:03:17.040><c> owner</c><00:03:17.360><c> and</c><00:03:17.879><c> approved</c><00:03:18.879><c> uh</c>

00:03:19.190 --> 00:03:19.200 align:start position:0%
burn um only the owner and approved uh
 

00:03:19.200 --> 00:03:21.270 align:start position:0%
burn um only the owner and approved uh
accounts<00:03:19.560><c> can</c><00:03:19.760><c> transfer</c><00:03:20.319><c> there's</c><00:03:20.560><c> no</c><00:03:20.760><c> Central</c>

00:03:21.270 --> 00:03:21.280 align:start position:0%
accounts can transfer there's no Central
 

00:03:21.280 --> 00:03:23.910 align:start position:0%
accounts can transfer there's no Central
author<00:03:21.879><c> Authority</c><00:03:22.440><c> that</c><00:03:22.599><c> can</c><00:03:22.760><c> steal</c><00:03:23.080><c> our</c>

00:03:23.910 --> 00:03:23.920 align:start position:0%
author Authority that can steal our
 

00:03:23.920 --> 00:03:26.949 align:start position:0%
author Authority that can steal our
tokens<00:03:24.920><c> we</c><00:03:25.120><c> need</c><00:03:25.560><c> other</c><00:03:25.920><c> assumption</c><00:03:26.480><c> that</c><00:03:26.840><c> uh</c>

00:03:26.949 --> 00:03:26.959 align:start position:0%
tokens we need other assumption that uh
 

00:03:26.959 --> 00:03:27.789 align:start position:0%
tokens we need other assumption that uh
if<00:03:27.080><c> you</c>

00:03:27.789 --> 00:03:27.799 align:start position:0%
if you
 

00:03:27.799 --> 00:03:30.110 align:start position:0%
if you
transfer<00:03:28.799><c> the</c><00:03:29.280><c> only</c><00:03:29.519><c> the</c><00:03:29.799><c> amount</c><00:03:30.000><c> is</c>

00:03:30.110 --> 00:03:30.120 align:start position:0%
transfer the only the amount is
 

00:03:30.120 --> 00:03:32.670 align:start position:0%
transfer the only the amount is
transferred<00:03:30.640><c> so</c><00:03:31.040><c> if</c><00:03:31.200><c> they</c><00:03:31.360><c> are</c><00:03:31.519><c> fees</c><00:03:31.879><c> the</c>

00:03:32.670 --> 00:03:32.680 align:start position:0%
transferred so if they are fees the
 

00:03:32.680 --> 00:03:33.990 align:start position:0%
transferred so if they are fees the
receiver<00:03:33.120><c> pays</c>

00:03:33.990 --> 00:03:34.000 align:start position:0%
receiver pays
 

00:03:34.000 --> 00:03:38.710 align:start position:0%
receiver pays
them<00:03:35.000><c> and</c><00:03:35.599><c> uh</c><00:03:35.879><c> that</c><00:03:36.120><c> transfer</c><00:03:37.040><c> never</c>

00:03:38.710 --> 00:03:38.720 align:start position:0%
them and uh that transfer never
 

00:03:38.720 --> 00:03:40.589 align:start position:0%
them and uh that transfer never
reverts

00:03:40.589 --> 00:03:40.599 align:start position:0%
reverts
 

00:03:40.599 --> 00:03:45.229 align:start position:0%
reverts
thanks<00:03:41.720><c> um</c><00:03:42.720><c> the</c><00:03:42.920><c> transfer</c><00:03:43.480><c> never</c><00:03:44.480><c> uh</c><00:03:44.760><c> reverts</c>

00:03:45.229 --> 00:03:45.239 align:start position:0%
thanks um the transfer never uh reverts
 

00:03:45.239 --> 00:03:48.910 align:start position:0%
thanks um the transfer never uh reverts
if<00:03:45.519><c> there</c><00:03:45.680><c> is</c><00:03:45.920><c> enough</c><00:03:46.319><c> balance</c><00:03:47.319><c> and</c><00:03:47.560><c> for</c><00:03:48.560><c> hooks</c>

00:03:48.910 --> 00:03:48.920 align:start position:0%
if there is enough balance and for hooks
 

00:03:48.920 --> 00:03:51.550 align:start position:0%
if there is enough balance and for hooks
we<00:03:49.040><c> need</c><00:03:49.400><c> the</c><00:03:49.760><c> assumption</c><00:03:50.400><c> that</c><00:03:51.120><c> there</c><00:03:51.239><c> is</c><00:03:51.360><c> no</c>

00:03:51.550 --> 00:03:51.560 align:start position:0%
we need the assumption that there is no
 

00:03:51.560 --> 00:03:53.470 align:start position:0%
we need the assumption that there is no
withdraw<00:03:52.000><c> hooks</c><00:03:52.400><c> otherwise</c><00:03:52.799><c> we</c><00:03:52.959><c> can't</c><00:03:53.200><c> prove</c>

00:03:53.470 --> 00:03:53.480 align:start position:0%
withdraw hooks otherwise we can't prove
 

00:03:53.480 --> 00:03:54.910 align:start position:0%
withdraw hooks otherwise we can't prove
that<00:03:53.640><c> you</c><00:03:53.840><c> can</c>

00:03:54.910 --> 00:03:54.920 align:start position:0%
that you can
 

00:03:54.920 --> 00:03:57.869 align:start position:0%
that you can
withdraw<00:03:55.920><c> so</c><00:03:56.159><c> what</c><00:03:56.319><c> we</c><00:03:56.480><c> do</c><00:03:56.720><c> is</c><00:03:57.120><c> um</c><00:03:57.680><c> an</c>

00:03:57.869 --> 00:03:57.879 align:start position:0%
withdraw so what we do is um an
 

00:03:57.879 --> 00:04:01.429 align:start position:0%
withdraw so what we do is um an
inductive<00:03:58.360><c> invariant</c><00:03:59.079><c> so</c><00:03:59.360><c> we</c><00:04:00.079><c> want</c><00:04:00.239><c> to</c><00:04:01.000><c> we</c>

00:04:01.429 --> 00:04:01.439 align:start position:0%
inductive invariant so we want to we
 

00:04:01.439 --> 00:04:05.149 align:start position:0%
inductive invariant so we want to we
split<00:04:02.120><c> our</c><00:04:03.120><c> States</c><00:04:03.480><c> into</c><00:04:03.840><c> two</c><00:04:04.200><c> kinds</c><00:04:04.519><c> of</c>

00:04:05.149 --> 00:04:05.159 align:start position:0%
split our States into two kinds of
 

00:04:05.159 --> 00:04:06.869 align:start position:0%
split our States into two kinds of
states<00:04:05.720><c> where</c><00:04:05.840><c> we</c><00:04:06.000><c> have</c><00:04:06.200><c> enough</c><00:04:06.400><c> funds</c><00:04:06.720><c> and</c>

00:04:06.869 --> 00:04:06.879 align:start position:0%
states where we have enough funds and
 

00:04:06.879 --> 00:04:09.030 align:start position:0%
states where we have enough funds and
where<00:04:06.959><c> we</c><00:04:07.120><c> don't</c><00:04:07.319><c> have</c><00:04:07.519><c> enough</c><00:04:07.760><c> funds</c><00:04:08.760><c> and</c><00:04:08.920><c> if</c>

00:04:09.030 --> 00:04:09.040 align:start position:0%
where we don't have enough funds and if
 

00:04:09.040 --> 00:04:11.149 align:start position:0%
where we don't have enough funds and if
we<00:04:09.200><c> look</c><00:04:09.360><c> at</c><00:04:09.519><c> all</c><00:04:09.720><c> the</c><00:04:09.879><c> transaction</c><00:04:10.840><c> then</c><00:04:11.000><c> we</c>

00:04:11.149 --> 00:04:11.159 align:start position:0%
we look at all the transaction then we
 

00:04:11.159 --> 00:04:13.949 align:start position:0%
we look at all the transaction then we
look<00:04:11.360><c> is</c><00:04:11.519><c> there</c><00:04:11.720><c> a</c><00:04:12.480><c> transaction</c><00:04:13.200><c> that</c><00:04:13.560><c> goes</c>

00:04:13.949 --> 00:04:13.959 align:start position:0%
look is there a transaction that goes
 

00:04:13.959 --> 00:04:17.670 align:start position:0%
look is there a transaction that goes
outside<00:04:14.400><c> the</c><00:04:14.920><c> circle</c><00:04:15.920><c> and</c><00:04:16.079><c> we</c><00:04:16.320><c> found</c><00:04:17.320><c> with</c><00:04:17.479><c> our</c>

00:04:17.670 --> 00:04:17.680 align:start position:0%
outside the circle and we found with our
 

00:04:17.680 --> 00:04:20.110 align:start position:0%
outside the circle and we found with our
tool<00:04:18.000><c> that</c><00:04:18.160><c> there</c><00:04:18.280><c> is</c><00:04:18.440><c> such</c><00:04:18.639><c> a</c><00:04:19.120><c> transaction</c>

00:04:20.110 --> 00:04:20.120 align:start position:0%
tool that there is such a transaction
 

00:04:20.120 --> 00:04:21.870 align:start position:0%
tool that there is such a transaction
but<00:04:20.280><c> it's</c><00:04:20.560><c> actually</c><00:04:20.840><c> a</c><00:04:21.000><c> transaction</c><00:04:21.560><c> that</c><00:04:21.720><c> is</c>

00:04:21.870 --> 00:04:21.880 align:start position:0%
but it's actually a transaction that is
 

00:04:21.880 --> 00:04:24.950 align:start position:0%
but it's actually a transaction that is
not<00:04:22.360><c> reachable</c><00:04:23.360><c> so</c><00:04:23.560><c> we</c><00:04:23.759><c> need</c><00:04:23.880><c> to</c><00:04:24.080><c> refine</c><00:04:24.720><c> our</c>

00:04:24.950 --> 00:04:24.960 align:start position:0%
not reachable so we need to refine our
 

00:04:24.960 --> 00:04:28.230 align:start position:0%
not reachable so we need to refine our
invariant<00:04:25.639><c> we</c><00:04:25.759><c> need</c><00:04:25.919><c> to</c><00:04:26.479><c> say</c><00:04:27.479><c> um</c><00:04:27.680><c> additional</c>

00:04:28.230 --> 00:04:28.240 align:start position:0%
invariant we need to say um additional
 

00:04:28.240 --> 00:04:31.430 align:start position:0%
invariant we need to say um additional
things<00:04:28.639><c> like</c><00:04:29.039><c> that</c><00:04:29.360><c> the</c><00:04:29.919><c> contract</c><00:04:30.919><c> also</c><00:04:31.240><c> does</c>

00:04:31.430 --> 00:04:31.440 align:start position:0%
things like that the contract also does
 

00:04:31.440 --> 00:04:33.390 align:start position:0%
things like that the contract also does
a<00:04:31.720><c> consistency</c><00:04:32.440><c> accounting</c><00:04:32.840><c> of</c><00:04:33.039><c> the</c>

00:04:33.390 --> 00:04:33.400 align:start position:0%
a consistency accounting of the
 

00:04:33.400 --> 00:04:36.870 align:start position:0%
a consistency accounting of the
liquidity<00:04:34.400><c> and</c><00:04:34.520><c> if</c><00:04:34.680><c> we</c><00:04:34.840><c> do</c><00:04:35.080><c> this</c><00:04:35.400><c> then</c><00:04:35.720><c> we</c><00:04:36.280><c> get</c>

00:04:36.870 --> 00:04:36.880 align:start position:0%
liquidity and if we do this then we get
 

00:04:36.880 --> 00:04:39.390 align:start position:0%
liquidity and if we do this then we get
the<00:04:37.880><c> that</c><00:04:38.039><c> all</c><00:04:38.240><c> the</c><00:04:38.400><c> transactions</c><00:04:39.000><c> stay</c><00:04:39.240><c> in</c>

00:04:39.390 --> 00:04:39.400 align:start position:0%
the that all the transactions stay in
 

00:04:39.400 --> 00:04:41.350 align:start position:0%
the that all the transactions stay in
this<00:04:39.600><c> inductive</c>

00:04:41.350 --> 00:04:41.360 align:start position:0%
this inductive
 

00:04:41.360 --> 00:04:45.110 align:start position:0%
this inductive
invariant<00:04:42.360><c> there</c><00:04:42.520><c> were</c><00:04:43.080><c> some</c><00:04:43.759><c> problems</c><00:04:44.680><c> with</c>

00:04:45.110 --> 00:04:45.120 align:start position:0%
invariant there were some problems with
 

00:04:45.120 --> 00:04:47.670 align:start position:0%
invariant there were some problems with
verifying<00:04:46.120><c> this</c><00:04:46.320><c> Unis</c><00:04:46.720><c> SW</c><00:04:46.919><c> it</c><00:04:47.039><c> was</c><00:04:47.199><c> not</c><00:04:47.440><c> as</c>

00:04:47.670 --> 00:04:47.680 align:start position:0%
verifying this Unis SW it was not as
 

00:04:47.680 --> 00:04:51.029 align:start position:0%
verifying this Unis SW it was not as
simple<00:04:48.000><c> as</c><00:04:48.160><c> I</c><00:04:48.360><c> just</c><00:04:48.560><c> made</c><00:04:48.759><c> it</c><00:04:49.639><c> so</c><00:04:49.880><c> we</c><00:04:50.080><c> had</c><00:04:50.280><c> some</c>

00:04:51.029 --> 00:04:51.039 align:start position:0%
simple as I just made it so we had some
 

00:04:51.039 --> 00:04:53.070 align:start position:0%
simple as I just made it so we had some
problems<00:04:51.360><c> with</c><00:04:51.560><c> rounding</c><00:04:51.960><c> errors</c><00:04:52.320><c> break</c><00:04:52.560><c> the</c>

00:04:53.070 --> 00:04:53.080 align:start position:0%
problems with rounding errors break the
 

00:04:53.080 --> 00:04:55.710 align:start position:0%
problems with rounding errors break the
invariance<00:04:54.080><c> and</c><00:04:54.280><c> other</c><00:04:54.600><c> things</c><00:04:54.960><c> like</c><00:04:55.199><c> sums</c>

00:04:55.710 --> 00:04:55.720 align:start position:0%
invariance and other things like sums
 

00:04:55.720 --> 00:04:59.909 align:start position:0%
invariance and other things like sums
over<00:04:56.560><c> ticks</c><00:04:56.960><c> and</c><00:04:57.840><c> positions</c>

00:04:59.909 --> 00:04:59.919 align:start position:0%
over ticks and positions
 

00:04:59.919 --> 00:05:02.909 align:start position:0%
over ticks and positions
we<00:05:00.080><c> solved</c><00:05:00.440><c> all</c><00:05:00.680><c> these</c><00:05:01.039><c> problems</c><00:05:02.039><c> I</c><00:05:02.320><c> can't</c><00:05:02.720><c> go</c>

00:05:02.909 --> 00:05:02.919 align:start position:0%
we solved all these problems I can't go
 

00:05:02.919 --> 00:05:05.469 align:start position:0%
we solved all these problems I can't go
into<00:05:03.160><c> the</c><00:05:03.320><c> details</c><00:05:03.840><c> because</c><00:05:04.080><c> it's</c><00:05:04.400><c> lightning</c>

00:05:05.469 --> 00:05:05.479 align:start position:0%
into the details because it's lightning
 

00:05:05.479 --> 00:05:07.790 align:start position:0%
into the details because it's lightning
talk<00:05:06.479><c> so</c><00:05:06.919><c> to</c>

00:05:07.790 --> 00:05:07.800 align:start position:0%
talk so to
 

00:05:07.800 --> 00:05:10.510 align:start position:0%
talk so to
summarize<00:05:08.800><c> what</c><00:05:08.960><c> we</c><00:05:09.080><c> showed</c><00:05:09.400><c> is</c><00:05:09.639><c> enough</c><00:05:09.919><c> funds</c>

00:05:10.510 --> 00:05:10.520 align:start position:0%
summarize what we showed is enough funds
 

00:05:10.520 --> 00:05:12.830 align:start position:0%
summarize what we showed is enough funds
and<00:05:10.759><c> consistent</c><00:05:11.400><c> accounting</c><00:05:12.400><c> is</c><00:05:12.600><c> an</c>

00:05:12.830 --> 00:05:12.840 align:start position:0%
and consistent accounting is an
 

00:05:12.840 --> 00:05:14.550 align:start position:0%
and consistent accounting is an
inductive

00:05:14.550 --> 00:05:14.560 align:start position:0%
inductive
 

00:05:14.560 --> 00:05:21.790 align:start position:0%
inductive
invariant<00:05:15.560><c> yeah</c><00:05:16.120><c> thank</c>

00:05:21.790 --> 00:05:21.800 align:start position:0%
 
 

00:05:21.800 --> 00:05:25.870 align:start position:0%
 
you<00:05:22.840><c> one</c><00:05:23.840><c> thank</c><00:05:24.000><c> you</c><00:05:24.160><c> it's</c><00:05:24.360><c> a</c><00:05:24.720><c> amazing</c><00:05:25.440><c> uh</c>

00:05:25.870 --> 00:05:25.880 align:start position:0%
you one thank you it's a amazing uh
 

00:05:25.880 --> 00:05:28.550 align:start position:0%
you one thank you it's a amazing uh
research<00:05:26.880><c> and</c><00:05:27.039><c> so</c><00:05:27.240><c> we</c><00:05:27.360><c> have</c><00:05:27.560><c> one</c><00:05:27.800><c> question</c><00:05:28.280><c> and</c>

00:05:28.550 --> 00:05:28.560 align:start position:0%
research and so we have one question and
 

00:05:28.560 --> 00:05:31.710 align:start position:0%
research and so we have one question and
I'm<00:05:28.720><c> also</c><00:05:29.199><c> very</c><00:05:29.960><c> curious</c><00:05:30.639><c> how</c><00:05:30.800><c> many</c><00:05:31.080><c> human</c>

00:05:31.710 --> 00:05:31.720 align:start position:0%
I'm also very curious how many human
 

00:05:31.720 --> 00:05:33.510 align:start position:0%
I'm also very curious how many human
hours<00:05:32.160><c> did</c><00:05:32.360><c> you</c><00:05:32.520><c> guys</c><00:05:32.680><c> spend</c><00:05:33.000><c> to</c><00:05:33.199><c> prove</c>

00:05:33.510 --> 00:05:33.520 align:start position:0%
hours did you guys spend to prove
 

00:05:33.520 --> 00:05:36.749 align:start position:0%
hours did you guys spend to prove
liquidity<00:05:34.160><c> of</c><00:05:34.600><c> uniswap</c><00:05:35.199><c> 4</c><00:05:35.919><c> and</c><00:05:36.280><c> if</c><00:05:36.440><c> they're</c>

00:05:36.749 --> 00:05:36.759 align:start position:0%
liquidity of uniswap 4 and if they're
 

00:05:36.759 --> 00:05:39.790 align:start position:0%
liquidity of uniswap 4 and if they're
like<00:05:37.039><c> maybe</c><00:05:37.319><c> you</c><00:05:37.440><c> can</c><00:05:38.400><c> uh</c><00:05:38.560><c> put</c><00:05:38.759><c> some</c><00:05:39.039><c> price</c><00:05:39.360><c> tag</c>

00:05:39.790 --> 00:05:39.800 align:start position:0%
like maybe you can uh put some price tag
 

00:05:39.800 --> 00:05:41.629 align:start position:0%
like maybe you can uh put some price tag
on<00:05:39.960><c> it</c><00:05:40.520><c> because</c><00:05:40.840><c> I</c><00:05:40.919><c> think</c><00:05:41.120><c> this</c><00:05:41.199><c> is</c><00:05:41.400><c> very</c>

00:05:41.629 --> 00:05:41.639 align:start position:0%
on it because I think this is very
 

00:05:41.639 --> 00:05:44.029 align:start position:0%
on it because I think this is very
interesting<00:05:42.280><c> because</c><00:05:42.600><c> before</c><00:05:42.960><c> like</c><00:05:43.440><c> on</c><00:05:43.639><c> the</c>

00:05:44.029 --> 00:05:44.039 align:start position:0%
interesting because before like on the
 

00:05:44.039 --> 00:05:46.110 align:start position:0%
interesting because before like on the
panel<00:05:44.440><c> before</c><00:05:44.759><c> we</c><00:05:44.880><c> were</c><00:05:45.160><c> wondering</c><00:05:45.680><c> about</c><00:05:46.000><c> you</c>

00:05:46.110 --> 00:05:46.120 align:start position:0%
panel before we were wondering about you
 

00:05:46.120 --> 00:05:49.590 align:start position:0%
panel before we were wondering about you
know<00:05:46.319><c> this</c><00:05:46.520><c> kind</c><00:05:46.639><c> of</c><00:05:47.199><c> yeah</c><00:05:48.039><c> I</c><00:05:48.280><c> I</c><00:05:48.400><c> don't</c><00:05:49.160><c> have</c>

00:05:49.590 --> 00:05:49.600 align:start position:0%
know this kind of yeah I I don't have
 

00:05:49.600 --> 00:05:52.070 align:start position:0%
know this kind of yeah I I don't have
Thea<00:05:50.319><c> price</c><00:05:50.600><c> tech</c><00:05:50.840><c> I'm</c><00:05:50.960><c> not</c><00:05:51.120><c> sure</c><00:05:51.319><c> if</c><00:05:51.479><c> I</c><00:05:51.680><c> even</c>

00:05:52.070 --> 00:05:52.080 align:start position:0%
Thea price tech I'm not sure if I even
 

00:05:52.080 --> 00:05:55.029 align:start position:0%
Thea price tech I'm not sure if I even
allowed<00:05:52.360><c> to</c><00:05:52.520><c> tell</c><00:05:52.880><c> it</c><00:05:53.880><c> um</c><00:05:54.360><c> but</c><00:05:54.560><c> we</c><00:05:54.720><c> spent</c>

00:05:55.029 --> 00:05:55.039 align:start position:0%
allowed to tell it um but we spent
 

00:05:55.039 --> 00:05:58.710 align:start position:0%
allowed to tell it um but we spent
several<00:05:55.400><c> weeks</c><00:05:55.800><c> with</c><00:05:56.199><c> a</c><00:05:57.199><c> small</c><00:05:57.639><c> team</c><00:05:58.280><c> so</c>

00:05:58.710 --> 00:05:58.720 align:start position:0%
several weeks with a small team so
 

00:05:58.720 --> 00:06:00.350 align:start position:0%
several weeks with a small team so
several<00:05:59.240><c> people</c>

00:06:00.350 --> 00:06:00.360 align:start position:0%
several people
 

00:06:00.360 --> 00:06:02.469 align:start position:0%
several people
on<00:06:00.600><c> this</c><00:06:00.800><c> contract</c><00:06:01.240><c> so</c><00:06:01.639><c> I</c><00:06:01.720><c> think</c><00:06:01.919><c> it</c><00:06:02.120><c> was</c>

00:06:02.469 --> 00:06:02.479 align:start position:0%
on this contract so I think it was
 

00:06:02.479 --> 00:06:05.590 align:start position:0%
on this contract so I think it was
something<00:06:02.840><c> like</c><00:06:03.080><c> six</c><00:06:03.479><c> weeks</c><00:06:04.479><c> six</c><00:06:04.800><c> weeks</c><00:06:05.280><c> yeah</c>

00:06:05.590 --> 00:06:05.600 align:start position:0%
something like six weeks six weeks yeah
 

00:06:05.600 --> 00:06:07.990 align:start position:0%
something like six weeks six weeks yeah
wow<00:06:06.280><c> and</c><00:06:06.599><c> uh</c><00:06:06.919><c> how</c><00:06:07.120><c> big</c><00:06:07.319><c> the</c><00:06:07.479><c> team</c><00:06:07.639><c> was</c><00:06:07.800><c> like</c>

00:06:07.990 --> 00:06:08.000 align:start position:0%
wow and uh how big the team was like
 

00:06:08.000 --> 00:06:11.990 align:start position:0%
wow and uh how big the team was like
three<00:06:08.319><c> people</c><00:06:08.919><c> five</c><00:06:09.759><c> um</c><00:06:10.319><c> more</c><00:06:10.680><c> like</c><00:06:11.680><c> I</c><00:06:11.800><c> think</c>

00:06:11.990 --> 00:06:12.000 align:start position:0%
three people five um more like I think
 

00:06:12.000 --> 00:06:15.710 align:start position:0%
three people five um more like I think
over<00:06:12.400><c> five</c><00:06:12.919><c> uh</c><00:06:13.440><c> but</c><00:06:13.599><c> less</c><00:06:13.720><c> than</c><00:06:13.919><c> 10</c><00:06:14.919><c> okay</c>

00:06:15.710 --> 00:06:15.720 align:start position:0%
over five uh but less than 10 okay
 

00:06:15.720 --> 00:06:18.270 align:start position:0%
over five uh but less than 10 okay
interesting<00:06:16.720><c> and</c><00:06:17.000><c> uh</c><00:06:17.160><c> how</c><00:06:17.280><c> many</c><00:06:17.720><c> errors</c><00:06:18.120><c> did</c>

00:06:18.270 --> 00:06:18.280 align:start position:0%
interesting and uh how many errors did
 

00:06:18.280 --> 00:06:21.790 align:start position:0%
interesting and uh how many errors did
you<00:06:18.479><c> guys</c><00:06:18.680><c> found</c><00:06:19.680><c> one</c><00:06:19.919><c> one</c><00:06:20.800><c> such</c><00:06:21.360><c> case</c><00:06:21.599><c> where</c>

00:06:21.790 --> 00:06:21.800 align:start position:0%
you guys found one one such case where
 

00:06:21.800 --> 00:06:23.870 align:start position:0%
you guys found one one such case where
this<00:06:22.080><c> transaction</c><00:06:22.680><c> can</c><00:06:22.840><c> lead</c><00:06:23.120><c> to</c><00:06:23.520><c> in</c><00:06:23.720><c> not</c>

00:06:23.870 --> 00:06:23.880 align:start position:0%
this transaction can lead to in not
 

00:06:23.880 --> 00:06:26.909 align:start position:0%
this transaction can lead to in not
enough<00:06:24.160><c> liquidity</c><00:06:24.759><c> right</c><00:06:25.440><c> um</c><00:06:26.160><c> we</c><00:06:26.319><c> didn't</c><00:06:26.599><c> find</c>

00:06:26.909 --> 00:06:26.919 align:start position:0%
enough liquidity right um we didn't find
 

00:06:26.919 --> 00:06:29.270 align:start position:0%
enough liquidity right um we didn't find
the<00:06:27.080><c> liquidity</c><00:06:27.599><c> error</c><00:06:27.919><c> so</c><00:06:28.080><c> the</c><00:06:28.199><c> code</c><00:06:28.599><c> was</c>

00:06:29.270 --> 00:06:29.280 align:start position:0%
the liquidity error so the code was
 

00:06:29.280 --> 00:06:32.309 align:start position:0%
the liquidity error so the code was
quite<00:06:29.680><c> good</c><00:06:29.880><c> there</c><00:06:30.080><c> was</c><00:06:30.639><c> mhm</c><00:06:31.639><c> slightly</c>

00:06:32.309 --> 00:06:32.319 align:start position:0%
quite good there was mhm slightly
 

00:06:32.319 --> 00:06:34.110 align:start position:0%
quite good there was mhm slightly
problems<00:06:32.759><c> like</c><00:06:32.919><c> you</c><00:06:33.080><c> can't</c><00:06:33.360><c> trade</c><00:06:33.680><c> to</c><00:06:33.880><c> the</c>

00:06:34.110 --> 00:06:34.120 align:start position:0%
problems like you can't trade to the
 

00:06:34.120 --> 00:06:37.150 align:start position:0%
problems like you can't trade to the
minimum<00:06:35.039><c> price</c><00:06:36.039><c> and</c><00:06:36.280><c> you</c><00:06:36.479><c> can't</c><00:06:36.720><c> reach</c><00:06:37.039><c> the</c>

00:06:37.150 --> 00:06:37.160 align:start position:0%
minimum price and you can't reach the
 

00:06:37.160 --> 00:06:39.070 align:start position:0%
minimum price and you can't reach the
minimum<00:06:37.680><c> price</c><00:06:38.039><c> but</c><00:06:38.199><c> if</c><00:06:38.319><c> you</c><00:06:38.440><c> start</c><00:06:38.840><c> there</c>

00:06:39.070 --> 00:06:39.080 align:start position:0%
minimum price but if you start there
 

00:06:39.080 --> 00:06:41.350 align:start position:0%
minimum price but if you start there
it's<00:06:39.360><c> possible</c><00:06:39.720><c> to</c><00:06:40.319><c> start</c><00:06:40.680><c> with</c><00:06:40.800><c> this</c><00:06:41.120><c> price</c>

00:06:41.350 --> 00:06:41.360 align:start position:0%
it's possible to start with this price
 

00:06:41.360 --> 00:06:44.309 align:start position:0%
it's possible to start with this price
so<00:06:41.599><c> there</c><00:06:41.720><c> was</c><00:06:41.919><c> some</c><00:06:42.120><c> inconsistency</c><00:06:43.319><c> there</c>

00:06:44.309 --> 00:06:44.319 align:start position:0%
so there was some inconsistency there
 

00:06:44.319 --> 00:06:45.870 align:start position:0%
so there was some inconsistency there
okay<00:06:44.479><c> so</c><00:06:44.680><c> we</c><00:06:44.800><c> have</c><00:06:44.919><c> one</c><00:06:45.080><c> more</c><00:06:45.280><c> question</c><00:06:45.720><c> could</c>

00:06:45.870 --> 00:06:45.880 align:start position:0%
okay so we have one more question could
 

00:06:45.880 --> 00:06:47.950 align:start position:0%
okay so we have one more question could
you<00:06:46.039><c> briefly</c><00:06:46.440><c> touch</c><00:06:46.680><c> on</c><00:06:46.919><c> how</c><00:06:47.120><c> you</c><00:06:47.520><c> approach</c>

00:06:47.950 --> 00:06:47.960 align:start position:0%
you briefly touch on how you approach
 

00:06:47.960 --> 00:06:50.790 align:start position:0%
you briefly touch on how you approach
dealing<00:06:48.360><c> with</c><00:06:48.639><c> the</c><00:06:49.120><c> rounding</c><00:06:49.680><c> errors</c>

00:06:50.790 --> 00:06:50.800 align:start position:0%
dealing with the rounding errors
 

00:06:50.800 --> 00:06:57.070 align:start position:0%
dealing with the rounding errors
in<00:06:51.800><c> yeah</c><00:06:52.000><c> so</c><00:06:52.319><c> we</c><00:06:52.479><c> use</c><00:06:53.360><c> um</c><00:06:54.360><c> we</c><00:06:54.520><c> use</c><00:06:55.360><c> a</c><00:06:56.360><c> we</c><00:06:56.520><c> use</c><00:06:56.720><c> fix</c>

00:06:57.070 --> 00:06:57.080 align:start position:0%
in yeah so we use um we use a we use fix
 

00:06:57.080 --> 00:06:59.629 align:start position:0%
in yeah so we use um we use a we use fix
Point<00:06:57.319><c> arithmetic</c><00:06:58.319><c> and</c><00:06:58.440><c> we</c><00:06:58.560><c> use</c><00:06:58.759><c> a</c><00:06:58.960><c> very</c><00:06:59.240><c> high</c>

00:06:59.629 --> 00:06:59.639 align:start position:0%
Point arithmetic and we use a very high
 

00:06:59.639 --> 00:07:01.710 align:start position:0%
Point arithmetic and we use a very high
Precision<00:07:00.599><c> because</c><00:07:00.879><c> we</c><00:07:01.000><c> have</c><00:07:01.160><c> unmounted</c>

00:07:01.710 --> 00:07:01.720 align:start position:0%
Precision because we have unmounted
 

00:07:01.720 --> 00:07:04.189 align:start position:0%
Precision because we have unmounted
integer<00:07:02.240><c> we</c><00:07:02.360><c> can</c><00:07:02.599><c> just</c><00:07:02.879><c> use</c><00:07:03.840><c> uh</c><00:07:03.960><c> some</c>

00:07:04.189 --> 00:07:04.199 align:start position:0%
integer we can just use uh some
 

00:07:04.199 --> 00:07:06.430 align:start position:0%
integer we can just use uh some
multiplier<00:07:04.800><c> for</c><00:07:05.000><c> fix</c><00:07:05.360><c> point</c><00:07:05.680><c> that</c><00:07:06.039><c> divides</c>

00:07:06.430 --> 00:07:06.440 align:start position:0%
multiplier for fix point that divides
 

00:07:06.440 --> 00:07:07.749 align:start position:0%
multiplier for fix point that divides
every<00:07:06.639><c> number</c><00:07:06.960><c> and</c><00:07:07.039><c> then</c><00:07:07.199><c> we</c><00:07:07.319><c> don't</c><00:07:07.560><c> get</c>

00:07:07.749 --> 00:07:07.759 align:start position:0%
every number and then we don't get
 

00:07:07.759 --> 00:07:10.469 align:start position:0%
every number and then we don't get
division<00:07:08.680><c> uh</c>

00:07:10.469 --> 00:07:10.479 align:start position:0%
division uh
 

00:07:10.479 --> 00:07:12.909 align:start position:0%
division uh
roundings<00:07:11.479><c> okay</c><00:07:11.720><c> thank</c><00:07:11.879><c> you</c><00:07:12.039><c> very</c><00:07:12.199><c> much</c><00:07:12.639><c> for</c>

00:07:12.909 --> 00:07:12.919 align:start position:0%
roundings okay thank you very much for
 

00:07:12.919 --> 00:07:15.110 align:start position:0%
roundings okay thank you very much for
interesting<00:07:13.440><c> talk</c><00:07:14.160><c> please</c><00:07:14.520><c> give</c><00:07:14.800><c> another</c>

00:07:15.110 --> 00:07:15.120 align:start position:0%
interesting talk please give another
 

00:07:15.120 --> 00:07:19.319 align:start position:0%
interesting talk please give another
round<00:07:15.319><c> of</c><00:07:15.560><c> applause</c><00:07:15.919><c> to</c><00:07:16.039><c> our</c><00:07:16.319><c> speaker</c>