WEBVTT Kind: captions Language: en 00:00:00.000 --> 00:00:04.350 align:start position:0% foreign 00:00:04.350 --> 00:00:04.360 align:start position:0% 00:00:04.360 --> 00:00:15.189 align:start position:0% [Music] 00:00:15.189 --> 00:00:15.199 align:start position:0% 00:00:15.199 --> 00:00:18.950 align:start position:0% and<00:00:16.199> I<00:00:16.320> work<00:00:16.560> as<00:00:17.279> a<00:00:17.520> former<00:00:17.820> very<00:00:18.000> very<00:00:18.240> formal 00:00:18.950 --> 00:00:18.960 align:start position:0% and I work as a former very very formal 00:00:18.960 --> 00:00:20.630 align:start position:0% and I work as a former very very formal verification<00:00:19.500> engineer<00:00:20.100> for<00:00:20.279> one-time 00:00:20.630 --> 00:00:20.640 align:start position:0% verification engineer for one-time 00:00:20.640 --> 00:00:23.029 align:start position:0% verification engineer for one-time verification<00:00:21.180> and<00:00:22.140> today<00:00:22.320> I<00:00:22.560> want<00:00:22.619> to<00:00:22.740> talk<00:00:22.920> to 00:00:23.029 --> 00:00:23.039 align:start position:0% verification and today I want to talk to 00:00:23.039 --> 00:00:25.130 align:start position:0% verification and today I want to talk to you<00:00:23.160> about<00:00:23.340> rounding<00:00:24.000> errors<00:00:24.420> and<00:00:24.779> what<00:00:25.019> we 00:00:25.130 --> 00:00:25.140 align:start position:0% you about rounding errors and what we 00:00:25.140 --> 00:00:27.009 align:start position:0% you about rounding errors and what we can<00:00:25.260> do<00:00:25.439> about<00:00:25.680> them 00:00:27.009 --> 00:00:27.019 align:start position:0% can do about them 00:00:27.019 --> 00:00:30.790 align:start position:0% can do about them so<00:00:28.019> very<00:00:28.680> roughly<00:00:29.220> speaking<00:00:29.760> and<00:00:30.060> I'm<00:00:30.300> really 00:00:30.790 --> 00:00:30.800 align:start position:0% so very roughly speaking and I'm really 00:00:30.800 --> 00:00:33.889 align:start position:0% so very roughly speaking and I'm really oversimplifying<00:00:31.800> uh<00:00:32.759> there<00:00:33.120> are<00:00:33.300> two<00:00:33.600> things 00:00:33.889 --> 00:00:33.899 align:start position:0% oversimplifying uh there are two things 00:00:33.899 --> 00:00:37.190 align:start position:0% oversimplifying uh there are two things that<00:00:34.320> can<00:00:34.500> go<00:00:34.680> wrong<00:00:34.920> when<00:00:35.460> we<00:00:35.700> do<00:00:36.200> approximate 00:00:37.190 --> 00:00:37.200 align:start position:0% that can go wrong when we do approximate 00:00:37.200 --> 00:00:40.369 align:start position:0% that can go wrong when we do approximate arithmetic<00:00:37.980> in<00:00:38.579> contrast<00:00:38.940> to<00:00:39.379> exact 00:00:40.369 --> 00:00:40.379 align:start position:0% arithmetic in contrast to exact 00:00:40.379 --> 00:00:43.850 align:start position:0% arithmetic in contrast to exact arithmetic<00:00:41.579> the<00:00:42.180> first<00:00:42.360> one<00:00:42.540> is<00:00:42.780> our<00:00:43.260> the 00:00:43.850 --> 00:00:43.860 align:start position:0% arithmetic the first one is our the 00:00:43.860 --> 00:00:46.369 align:start position:0% arithmetic the first one is our the rounding<00:00:44.219> error<00:00:44.520> that<00:00:44.640> we<00:00:44.820> do<00:00:44.940> is<00:00:45.540> just 00:00:46.369 --> 00:00:46.379 align:start position:0% rounding error that we do is just 00:00:46.379 --> 00:00:49.069 align:start position:0% rounding error that we do is just too<00:00:46.980> big<00:00:47.160> too<00:00:47.760> far<00:00:47.940> away<00:00:48.120> from<00:00:48.539> the<00:00:48.780> exact 00:00:49.069 --> 00:00:49.079 align:start position:0% too big too far away from the exact 00:00:49.079 --> 00:00:52.490 align:start position:0% too big too far away from the exact result<00:00:49.399> and<00:00:50.399> that<00:00:50.640> is<00:00:50.820> a<00:00:50.940> problem<00:00:51.059> in<00:00:51.360> itself 00:00:52.490 --> 00:00:52.500 align:start position:0% result and that is a problem in itself 00:00:52.500 --> 00:00:55.189 align:start position:0% result and that is a problem in itself but<00:00:52.860> that<00:00:53.039> is<00:00:53.219> not<00:00:53.340> the<00:00:53.520> topic<00:00:53.760> of<00:00:53.940> today<00:00:54.180> so<00:00:54.780> I 00:00:55.189 --> 00:00:55.199 align:start position:0% but that is not the topic of today so I 00:00:55.199 --> 00:00:57.889 align:start position:0% but that is not the topic of today so I want<00:00:55.320> to<00:00:55.440> talk<00:00:55.739> about<00:00:56.120> uh<00:00:57.120> the<00:00:57.420> second<00:00:57.539> thing 00:00:57.889 --> 00:00:57.899 align:start position:0% want to talk about uh the second thing 00:00:57.899 --> 00:01:00.529 align:start position:0% want to talk about uh the second thing that<00:00:58.260> can<00:00:58.379> go<00:00:58.620> wrong<00:00:58.800> and<00:00:59.219> that<00:00:59.399> is 00:01:00.529 --> 00:01:00.539 align:start position:0% that can go wrong and that is 00:01:00.539 --> 00:01:03.229 align:start position:0% that can go wrong and that is um what<00:01:00.840> can<00:01:00.960> happen<00:01:01.140> is<00:01:01.680> that<00:01:02.280> you<00:01:02.520> want<00:01:03.120> to 00:01:03.229 --> 00:01:03.239 align:start position:0% um what can happen is that you want to 00:01:03.239 --> 00:01:06.469 align:start position:0% um what can happen is that you want to approximate<00:01:04.019> a<00:01:04.500> value<00:01:04.680> From<00:01:05.400> Below<00:01:05.820> or<00:01:06.360> you 00:01:06.469 --> 00:01:06.479 align:start position:0% approximate a value From Below or you 00:01:06.479 --> 00:01:08.690 align:start position:0% approximate a value From Below or you want<00:01:06.659> to<00:01:06.780> come<00:01:06.960> from<00:01:07.200> above<00:01:07.560> but<00:01:08.100> you<00:01:08.280> do<00:01:08.400> it<00:01:08.520> in 00:01:08.690 --> 00:01:08.700 align:start position:0% want to come from above but you do it in 00:01:08.700 --> 00:01:10.910 align:start position:0% want to come from above but you do it in the<00:01:08.820> wrong<00:01:08.939> direction<00:01:09.240> like 00:01:10.910 --> 00:01:10.920 align:start position:0% the wrong direction like 00:01:10.920 --> 00:01:14.090 align:start position:0% the wrong direction like uh<00:01:11.880> in<00:01:12.420> other<00:01:12.479> words<00:01:12.659> you<00:01:13.320> want<00:01:13.439> to<00:01:13.560> round<00:01:13.740> down 00:01:14.090 --> 00:01:14.100 align:start position:0% uh in other words you want to round down 00:01:14.100 --> 00:01:16.550 align:start position:0% uh in other words you want to round down but<00:01:14.580> you<00:01:14.760> round<00:01:14.880> it<00:01:15.119> up<00:01:15.299> instead<00:01:15.720> and<00:01:16.260> that<00:01:16.439> can 00:01:16.550 --> 00:01:16.560 align:start position:0% but you round it up instead and that can 00:01:16.560 --> 00:01:18.950 align:start position:0% but you round it up instead and that can lead<00:01:16.799> to<00:01:17.159> severe<00:01:17.760> security<00:01:18.000> vulnerabilities 00:01:18.950 --> 00:01:18.960 align:start position:0% lead to severe security vulnerabilities 00:01:18.960 --> 00:01:22.310 align:start position:0% lead to severe security vulnerabilities I<00:01:19.320> will<00:01:19.439> show<00:01:19.680> you<00:01:20.000> some<00:01:21.000> examples<00:01:21.600> that<00:01:22.140> you 00:01:22.310 --> 00:01:22.320 align:start position:0% I will show you some examples that you 00:01:22.320 --> 00:01:25.249 align:start position:0% I will show you some examples that you will<00:01:22.439> recognize<00:01:22.860> maybe<00:01:23.220> and<00:01:23.939> then<00:01:24.119> but<00:01:25.020> I'm 00:01:25.249 --> 00:01:25.259 align:start position:0% will recognize maybe and then but I'm 00:01:25.259 --> 00:01:26.749 align:start position:0% will recognize maybe and then but I'm not<00:01:25.439> going<00:01:25.560> to<00:01:25.740> work<00:01:25.979> on<00:01:26.159> these<00:01:26.400> real<00:01:26.520> world 00:01:26.749 --> 00:01:26.759 align:start position:0% not going to work on these real world 00:01:26.759 --> 00:01:28.730 align:start position:0% not going to work on these real world examples<00:01:27.240> I'm<00:01:27.600> working<00:01:27.900> on<00:01:28.140> a<00:01:28.380> like 00:01:28.730 --> 00:01:28.740 align:start position:0% examples I'm working on a like 00:01:28.740 --> 00:01:30.770 align:start position:0% examples I'm working on a like simplified<00:01:29.220> example 00:01:30.770 --> 00:01:30.780 align:start position:0% simplified example 00:01:30.780 --> 00:01:33.950 align:start position:0% simplified example um<00:01:30.900> and<00:01:31.860> make<00:01:32.159> sure<00:01:32.340> to<00:01:32.640> understand<00:01:32.820> like<00:01:33.479> the 00:01:33.950 --> 00:01:33.960 align:start position:0% um and make sure to understand like the 00:01:33.960 --> 00:01:36.109 align:start position:0% um and make sure to understand like the two-way<00:01:34.320> trading<00:01:34.799> problem 00:01:36.109 --> 00:01:36.119 align:start position:0% two-way trading problem 00:01:36.119 --> 00:01:36.830 align:start position:0% two-way trading problem um 00:01:36.830 --> 00:01:36.840 align:start position:0% um 00:01:36.840 --> 00:01:39.230 align:start position:0% um because<00:01:37.320> otherwise<00:01:37.920> you<00:01:38.220> won't<00:01:38.460> be<00:01:38.880> able<00:01:39.119> to 00:01:39.230 --> 00:01:39.240 align:start position:0% because otherwise you won't be able to 00:01:39.240 --> 00:01:41.630 align:start position:0% because otherwise you won't be able to follow<00:01:39.540> my<00:01:39.840> talk<00:01:40.020> everything<00:01:40.380> like<00:01:40.920> get<00:01:41.460> to 00:01:41.630 --> 00:01:41.640 align:start position:0% follow my talk everything like get to 00:01:41.640 --> 00:01:43.429 align:start position:0% follow my talk everything like get to this<00:01:41.820> point<00:01:42.000> stay<00:01:42.299> with<00:01:42.479> me<00:01:42.659> until<00:01:42.900> this<00:01:43.259> point 00:01:43.429 --> 00:01:43.439 align:start position:0% this point stay with me until this point 00:01:43.439 --> 00:01:47.510 align:start position:0% this point stay with me until this point and<00:01:43.680> then<00:01:43.860> you<00:01:44.040> can<00:01:44.220> make<00:01:44.400> sense<00:01:44.579> of<00:01:44.759> this<00:01:44.880> talk 00:01:47.510 --> 00:01:47.520 align:start position:0% 00:01:47.520 --> 00:01:49.190 align:start position:0% um<00:01:47.700> so 00:01:49.190 --> 00:01:49.200 align:start position:0% um so 00:01:49.200 --> 00:01:52.370 align:start position:0% um so uh<00:01:50.040> grounding<00:01:50.640> errors 00:01:52.370 --> 00:01:52.380 align:start position:0% uh grounding errors 00:01:52.380 --> 00:01:55.130 align:start position:0% uh grounding errors um<00:01:52.439> they<00:01:52.860> are<00:01:53.040> well<00:01:53.520> we<00:01:54.479> need<00:01:54.600> to<00:01:54.720> accept<00:01:54.840> them 00:01:55.130 --> 00:01:55.140 align:start position:0% um they are well we need to accept them 00:01:55.140 --> 00:01:57.590 align:start position:0% um they are well we need to accept them we<00:01:55.380> cannot<00:01:55.680> do<00:01:55.920> exact<00:01:56.820> arithmetic<00:01:57.420> on<00:01:57.540> the 00:01:57.590 --> 00:01:57.600 align:start position:0% we cannot do exact arithmetic on the 00:01:57.600 --> 00:02:00.109 align:start position:0% we cannot do exact arithmetic on the blockchain<00:01:57.899> it's<00:01:58.140> not<00:01:58.500> feasible<00:01:58.860> so<00:01:59.640> and<00:01:59.880> we 00:02:00.109 --> 00:02:00.119 align:start position:0% blockchain it's not feasible so and we 00:02:00.119 --> 00:02:01.429 align:start position:0% blockchain it's not feasible so and we found 00:02:01.429 --> 00:02:01.439 align:start position:0% found 00:02:01.439 --> 00:02:04.389 align:start position:0% found rounding<00:02:02.159> errors<00:02:02.460> in<00:02:02.880> uni<00:02:03.240> Swap 00:02:04.389 --> 00:02:04.399 align:start position:0% rounding errors in uni Swap 00:02:04.399 --> 00:02:08.570 align:start position:0% rounding errors in uni Swap and<00:02:05.399> luckily<00:02:05.880> this<00:02:06.180> running<00:02:06.360> error<00:02:06.840> was<00:02:07.020> fixed 00:02:08.570 --> 00:02:08.580 align:start position:0% and luckily this running error was fixed 00:02:08.580 --> 00:02:11.390 align:start position:0% and luckily this running error was fixed um before<00:02:09.239> uni<00:02:09.720> swap<00:02:09.899> V1<00:02:10.140> was<00:02:10.380> deployed<00:02:10.860> but<00:02:11.280> I 00:02:11.390 --> 00:02:11.400 align:start position:0% um before uni swap V1 was deployed but I 00:02:11.400 --> 00:02:13.210 align:start position:0% um before uni swap V1 was deployed but I leave<00:02:11.520> it<00:02:11.700> to<00:02:11.879> your<00:02:12.060> imagination 00:02:13.210 --> 00:02:13.220 align:start position:0% leave it to your imagination 00:02:13.220 --> 00:02:16.430 align:start position:0% leave it to your imagination how<00:02:14.220> the<00:02:15.120> blockchain<00:02:15.480> landscape<00:02:15.959> would<00:02:16.200> have 00:02:16.430 --> 00:02:16.440 align:start position:0% how the blockchain landscape would have 00:02:16.440 --> 00:02:17.930 align:start position:0% how the blockchain landscape would have looked<00:02:16.739> liked 00:02:17.930 --> 00:02:17.940 align:start position:0% looked liked 00:02:17.940 --> 00:02:20.630 align:start position:0% looked liked um if<00:02:18.480> this<00:02:19.020> bug<00:02:19.319> was<00:02:19.680> not<00:02:19.860> caught<00:02:20.160> during<00:02:20.400> an 00:02:20.630 --> 00:02:20.640 align:start position:0% um if this bug was not caught during an 00:02:20.640 --> 00:02:23.690 align:start position:0% um if this bug was not caught during an audit<00:02:21.000> and<00:02:21.720> then<00:02:21.840> we<00:02:22.080> had<00:02:22.319> like<00:02:22.980> two<00:02:23.520> more 00:02:23.690 --> 00:02:23.700 align:start position:0% audit and then we had like two more 00:02:23.700 --> 00:02:25.550 align:start position:0% audit and then we had like two more examples<00:02:24.000> Solana<00:02:24.599> token<00:02:25.080> Landing<00:02:25.319> contract 00:02:25.550 --> 00:02:25.560 align:start position:0% examples Solana token Landing contract 00:02:25.560 --> 00:02:28.369 align:start position:0% examples Solana token Landing contract and<00:02:25.739> Solana<00:02:26.099> token<00:02:26.520> stable<00:02:26.760> swap 00:02:28.369 --> 00:02:28.379 align:start position:0% and Solana token stable swap 00:02:28.379 --> 00:02:29.030 align:start position:0% and Solana token stable swap um 00:02:29.030 --> 00:02:29.040 align:start position:0% um 00:02:29.040 --> 00:02:32.630 align:start position:0% um and<00:02:29.819> there<00:02:30.180> so<00:02:30.780> the<00:02:31.680> um<00:02:31.739> these<00:02:32.160> bugs<00:02:32.520> were 00:02:32.630 --> 00:02:32.640 align:start position:0% and there so the um these bugs were 00:02:32.640 --> 00:02:35.089 align:start position:0% and there so the um these bugs were actually<00:02:32.819> caught<00:02:33.239> doing<00:02:33.780> like<00:02:34.379> why<00:02:34.800> these 00:02:35.089 --> 00:02:35.099 align:start position:0% actually caught doing like why these 00:02:35.099 --> 00:02:36.949 align:start position:0% actually caught doing like why these contracts<00:02:35.459> haven't<00:02:35.640> deployed<00:02:36.180> and<00:02:36.480> at<00:02:36.840> the 00:02:36.949 --> 00:02:36.959 align:start position:0% contracts haven't deployed and at the 00:02:36.959 --> 00:02:38.809 align:start position:0% contracts haven't deployed and at the peak<00:02:37.200> time<00:02:37.319> there<00:02:37.739> were<00:02:37.860> like<00:02:38.099> three<00:02:38.400> billion 00:02:38.809 --> 00:02:38.819 align:start position:0% peak time there were like three billion 00:02:38.819 --> 00:02:40.729 align:start position:0% peak time there were like three billion assets<00:02:39.180> at<00:02:39.420> risk 00:02:40.729 --> 00:02:40.739 align:start position:0% assets at risk 00:02:40.739 --> 00:02:41.449 align:start position:0% assets at risk um 00:02:41.449 --> 00:02:41.459 align:start position:0% um 00:02:41.459 --> 00:02:45.229 align:start position:0% um so<00:02:42.060> luckily<00:02:42.720> again<00:02:43.500> uh 00:02:45.229 --> 00:02:45.239 align:start position:0% so luckily again uh 00:02:45.239 --> 00:02:47.990 align:start position:0% so luckily again uh these<00:02:46.019> were<00:02:46.200> not<00:02:46.379> exploited<00:02:46.920> by<00:02:47.160> the<00:02:47.400> but<00:02:47.700> they 00:02:47.990 --> 00:02:48.000 align:start position:0% these were not exploited by the but they 00:02:48.000 --> 00:02:50.030 align:start position:0% these were not exploited by the but they were<00:02:48.120> found<00:02:48.300> by<00:02:48.540> white<00:02:48.720> hackers<00:02:49.200> uh<00:02:49.800> before 00:02:50.030 --> 00:02:50.040 align:start position:0% were found by white hackers uh before 00:02:50.040 --> 00:02:51.949 align:start position:0% were found by white hackers uh before any<00:02:50.400> serious<00:02:50.879> damage<00:02:51.180> could<00:02:51.420> it<00:02:51.599> could<00:02:51.840> be 00:02:51.949 --> 00:02:51.959 align:start position:0% any serious damage could it could be 00:02:51.959 --> 00:02:53.570 align:start position:0% any serious damage could it could be done 00:02:53.570 --> 00:02:53.580 align:start position:0% done 00:02:53.580 --> 00:02:54.850 align:start position:0% done um<00:02:53.700> so 00:02:54.850 --> 00:02:54.860 align:start position:0% um so 00:02:54.860 --> 00:02:58.490 align:start position:0% um so uh<00:02:55.860> I<00:02:56.220> cannot<00:02:56.580> get<00:02:56.819> into<00:02:57.000> detail<00:02:57.480> into<00:02:57.840> any<00:02:58.319> of 00:02:58.490 --> 00:02:58.500 align:start position:0% uh I cannot get into detail into any of 00:02:58.500 --> 00:03:00.770 align:start position:0% uh I cannot get into detail into any of those<00:02:58.739> but<00:02:59.220> like<00:02:59.700> I<00:02:59.940> promise<00:03:00.180> you<00:03:00.360> if<00:03:00.660> you 00:03:00.770 --> 00:03:00.780 align:start position:0% those but like I promise you if you 00:03:00.780 --> 00:03:03.589 align:start position:0% those but like I promise you if you follow<00:03:01.019> my<00:03:01.260> talk<00:03:01.500> then<00:03:02.099> you<00:03:02.400> will<00:03:02.700> be<00:03:02.819> able<00:03:03.120> to 00:03:03.589 --> 00:03:03.599 align:start position:0% follow my talk then you will be able to 00:03:03.599 --> 00:03:06.290 align:start position:0% follow my talk then you will be able to visit<00:03:03.840> the<00:03:04.080> links<00:03:04.379> that<00:03:04.560> I<00:03:04.680> put<00:03:04.800> on<00:03:04.980> the<00:03:05.099> slide 00:03:06.290 --> 00:03:06.300 align:start position:0% visit the links that I put on the slide 00:03:06.300 --> 00:03:07.850 align:start position:0% visit the links that I put on the slide um<00:03:06.420> and<00:03:06.660> you<00:03:06.780> will<00:03:06.900> be<00:03:07.019> able<00:03:07.140> to<00:03:07.260> make<00:03:07.379> sense<00:03:07.680> of 00:03:07.850 --> 00:03:07.860 align:start position:0% um and you will be able to make sense of 00:03:07.860 --> 00:03:10.910 align:start position:0% um and you will be able to make sense of these<00:03:08.099> exploits<00:03:08.640> and<00:03:08.700> and<00:03:09.000> like<00:03:09.599> how<00:03:10.319> or<00:03:10.560> these 00:03:10.910 --> 00:03:10.920 align:start position:0% these exploits and and like how or these 00:03:10.920 --> 00:03:12.649 align:start position:0% these exploits and and like how or these vulnerabilities<00:03:11.580> and<00:03:11.760> how<00:03:12.000> they<00:03:12.300> could<00:03:12.480> have 00:03:12.649 --> 00:03:12.659 align:start position:0% vulnerabilities and how they could have 00:03:12.659 --> 00:03:14.570 align:start position:0% vulnerabilities and how they could have been<00:03:12.900> exploited<00:03:13.500> if<00:03:14.040> they<00:03:14.220> haven't<00:03:14.340> been 00:03:14.570 --> 00:03:14.580 align:start position:0% been exploited if they haven't been 00:03:14.580 --> 00:03:16.210 align:start position:0% been exploited if they haven't been fixed 00:03:16.210 --> 00:03:16.220 align:start position:0% fixed 00:03:16.220 --> 00:03:17.809 align:start position:0% fixed so 00:03:17.809 --> 00:03:17.819 align:start position:0% so 00:03:17.819 --> 00:03:20.089 align:start position:0% so um I<00:03:18.540> want<00:03:18.659> to<00:03:18.780> show<00:03:19.080> you<00:03:19.319> the<00:03:19.860> two-way 00:03:20.089 --> 00:03:20.099 align:start position:0% um I want to show you the two-way 00:03:20.099 --> 00:03:22.790 align:start position:0% um I want to show you the two-way trading<00:03:20.580> problem<00:03:20.760> and<00:03:21.300> I<00:03:21.900> promise<00:03:22.319> you<00:03:22.440> this 00:03:22.790 --> 00:03:22.800 align:start position:0% trading problem and I promise you this 00:03:22.800 --> 00:03:25.009 align:start position:0% trading problem and I promise you this is<00:03:22.920> like<00:03:23.159> the<00:03:23.519> most<00:03:23.700> mathematical<00:03:24.360> slide<00:03:24.840> on 00:03:25.009 --> 00:03:25.019 align:start position:0% is like the most mathematical slide on 00:03:25.019 --> 00:03:27.830 align:start position:0% is like the most mathematical slide on my<00:03:25.260> uh<00:03:26.099> on<00:03:26.400> my<00:03:26.700> entire<00:03:26.940> talk<00:03:27.180> which<00:03:27.480> is<00:03:27.599> strange 00:03:27.830 --> 00:03:27.840 align:start position:0% my uh on my entire talk which is strange 00:03:27.840 --> 00:03:29.210 align:start position:0% my uh on my entire talk which is strange well<00:03:28.080> because<00:03:28.319> I'm<00:03:28.560> talking<00:03:28.739> about<00:03:28.920> running 00:03:29.210 --> 00:03:29.220 align:start position:0% well because I'm talking about running 00:03:29.220 --> 00:03:31.610 align:start position:0% well because I'm talking about running errors<00:03:29.700> right<00:03:29.940> okay<00:03:30.720> but 00:03:31.610 --> 00:03:31.620 align:start position:0% errors right okay but 00:03:31.620 --> 00:03:33.649 align:start position:0% errors right okay but um<00:03:31.739> I<00:03:32.159> want<00:03:32.280> to<00:03:32.400> introduce<00:03:32.940> to<00:03:33.180> you<00:03:33.300> to<00:03:33.480> my 00:03:33.649 --> 00:03:33.659 align:start position:0% um I want to introduce to you to my 00:03:33.659 --> 00:03:35.750 align:start position:0% um I want to introduce to you to my image<00:03:33.959> now<00:03:34.140> with<00:03:34.379> friend<00:03:34.680> Alice<00:03:35.159> she's<00:03:35.459> right 00:03:35.750 --> 00:03:35.760 align:start position:0% image now with friend Alice she's right 00:03:35.760 --> 00:03:39.050 align:start position:0% image now with friend Alice she's right here<00:03:36.000> hi<00:03:36.420> Alice<00:03:36.780> and<00:03:37.680> I<00:03:37.920> will<00:03:38.099> demonstrate<00:03:38.580> to 00:03:39.050 --> 00:03:39.060 align:start position:0% here hi Alice and I will demonstrate to 00:03:39.060 --> 00:03:41.330 align:start position:0% here hi Alice and I will demonstrate to you<00:03:39.180> the<00:03:39.540> two-way<00:03:39.959> rounding<00:03:40.379> problem<00:03:40.620> as<00:03:41.099> the 00:03:41.330 --> 00:03:41.340 align:start position:0% you the two-way rounding problem as the 00:03:41.340 --> 00:03:43.670 align:start position:0% you the two-way rounding problem as the two-way<00:03:41.580> trading<00:03:42.000> problem<00:03:42.180> so<00:03:42.959> first<00:03:43.260> I'm 00:03:43.670 --> 00:03:43.680 align:start position:0% two-way trading problem so first I'm 00:03:43.680 --> 00:03:45.710 align:start position:0% two-way trading problem so first I'm going<00:03:43.860> to<00:03:43.980> offer<00:03:44.340> Alice<00:03:44.700> a<00:03:44.819> trade<00:03:45.060> and<00:03:45.480> we<00:03:45.599> do 00:03:45.710 --> 00:03:45.720 align:start position:0% going to offer Alice a trade and we do 00:03:45.720 --> 00:03:47.869 align:start position:0% going to offer Alice a trade and we do it<00:03:45.840> with<00:03:46.019> exact<00:03:46.379> arithmetic<00:03:47.159> and<00:03:47.580> then<00:03:47.700> we're 00:03:47.869 --> 00:03:47.879 align:start position:0% it with exact arithmetic and then we're 00:03:47.879 --> 00:03:50.449 align:start position:0% it with exact arithmetic and then we're doing<00:03:48.180> we<00:03:48.659> are<00:03:48.840> going<00:03:49.019> to<00:03:49.140> replay<00:03:49.440> the<00:03:50.099> wall 00:03:50.449 --> 00:03:50.459 align:start position:0% doing we are going to replay the wall 00:03:50.459 --> 00:03:52.970 align:start position:0% doing we are going to replay the wall the<00:03:50.819> role<00:03:51.120> play<00:03:51.239> and<00:03:52.080> then<00:03:52.319> we<00:03:52.560> are<00:03:52.680> doing<00:03:52.799> it 00:03:52.970 --> 00:03:52.980 align:start position:0% the role play and then we are doing it 00:03:52.980 --> 00:03:56.390 align:start position:0% the role play and then we are doing it with<00:03:53.159> rounding<00:03:53.640> so<00:03:54.120> hi<00:03:54.720> Alice<00:03:55.140> also<00:03:55.620> basic 00:03:56.390 --> 00:03:56.400 align:start position:0% with rounding so hi Alice also basic 00:03:56.400 --> 00:03:58.309 align:start position:0% with rounding so hi Alice also basic scenarios<00:03:56.819> we<00:03:57.120> have<00:03:57.239> two<00:03:57.420> currencies<00:03:57.959> we<00:03:58.200> have 00:03:58.309 --> 00:03:58.319 align:start position:0% scenarios we have two currencies we have 00:03:58.319 --> 00:04:00.890 align:start position:0% scenarios we have two currencies we have dollar<00:03:58.560> and<00:03:58.980> Gill<00:03:59.340> Gill<00:04:00.000> is<00:04:00.180> just<00:04:00.360> a<00:04:00.480> fantasy 00:04:00.890 --> 00:04:00.900 align:start position:0% dollar and Gill Gill is just a fantasy 00:04:00.900 --> 00:04:02.330 align:start position:0% dollar and Gill Gill is just a fantasy currency 00:04:02.330 --> 00:04:02.340 align:start position:0% currency 00:04:02.340 --> 00:04:04.270 align:start position:0% currency um<00:04:02.400> and<00:04:02.760> we<00:04:02.879> have<00:04:03.000> exchange<00:04:03.480> rate<00:04:03.659> currently 00:04:04.270 --> 00:04:04.280 align:start position:0% um and we have exchange rate currently 00:04:04.280 --> 00:04:08.330 align:start position:0% um and we have exchange rate currently uh<00:04:05.280> that<00:04:05.580> says<00:04:05.940> I<00:04:06.299> can<00:04:06.420> get<00:04:06.780> like 00:04:08.330 --> 00:04:08.340 align:start position:0% uh that says I can get like 00:04:08.340 --> 00:04:11.089 align:start position:0% uh that says I can get like um<00:04:08.400> two<00:04:09.239> Gill<00:04:09.599> for<00:04:09.959> one<00:04:10.140> dollar<00:04:10.319> so<00:04:10.680> exchange 00:04:11.089 --> 00:04:11.099 align:start position:0% um two Gill for one dollar so exchange 00:04:11.099 --> 00:04:14.449 align:start position:0% um two Gill for one dollar so exchange rate<00:04:11.280> is<00:04:11.519> two<00:04:11.700> so<00:04:12.480> I'm<00:04:12.959> Raul<00:04:13.379> I<00:04:13.799> have<00:04:13.920> one<00:04:14.220> girl 00:04:14.449 --> 00:04:14.459 align:start position:0% rate is two so I'm Raul I have one girl 00:04:14.459 --> 00:04:17.030 align:start position:0% rate is two so I'm Raul I have one girl in<00:04:14.760> my<00:04:14.879> pocket<00:04:15.180> and<00:04:15.659> this<00:04:15.780> is<00:04:15.840> Alice<00:04:16.260> and<00:04:16.859> hey 00:04:17.030 --> 00:04:17.040 align:start position:0% in my pocket and this is Alice and hey 00:04:17.040 --> 00:04:18.890 align:start position:0% in my pocket and this is Alice and hey Alice<00:04:17.400> do<00:04:17.639> you<00:04:17.699> want<00:04:17.760> to<00:04:17.880> trade<00:04:18.060> with<00:04:18.299> me<00:04:18.419> I<00:04:18.780> can 00:04:18.890 --> 00:04:18.900 align:start position:0% Alice do you want to trade with me I can 00:04:18.900 --> 00:04:21.469 align:start position:0% Alice do you want to trade with me I can offer<00:04:19.260> you<00:04:19.440> one<00:04:19.919> gear<00:04:20.280> how<00:04:20.699> many<00:04:20.820> dollars<00:04:21.180> do<00:04:21.299> I 00:04:21.469 --> 00:04:21.479 align:start position:0% offer you one gear how many dollars do I 00:04:21.479 --> 00:04:23.270 align:start position:0% offer you one gear how many dollars do I get<00:04:21.540> for<00:04:21.720> that<00:04:21.959> and<00:04:22.560> let<00:04:22.800> us<00:04:22.919> do<00:04:23.100> the 00:04:23.270 --> 00:04:23.280 align:start position:0% get for that and let us do the 00:04:23.280 --> 00:04:24.310 align:start position:0% get for that and let us do the calculation 00:04:24.310 --> 00:04:24.320 align:start position:0% calculation 00:04:24.320 --> 00:04:27.350 align:start position:0% calculation he<00:04:25.320> gives<00:04:25.440> me<00:04:25.680> one<00:04:26.100> dollar<00:04:26.280> he<00:04:26.880> gives<00:04:27.000> me<00:04:27.180> one 00:04:27.350 --> 00:04:27.360 align:start position:0% he gives me one dollar he gives me one 00:04:27.360 --> 00:04:29.990 align:start position:0% he gives me one dollar he gives me one kill<00:04:27.600> so<00:04:28.080> I<00:04:28.259> need<00:04:28.380> to<00:04:28.560> divide<00:04:28.919> by<00:04:29.280> the<00:04:29.580> exchange 00:04:29.990 --> 00:04:30.000 align:start position:0% kill so I need to divide by the exchange 00:04:30.000 --> 00:04:33.290 align:start position:0% kill so I need to divide by the exchange rate<00:04:30.240> uh<00:04:31.080> so<00:04:31.380> you<00:04:31.800> get<00:04:32.100> one<00:04:32.460> you<00:04:32.759> get<00:04:33.000> half<00:04:33.120> a 00:04:33.290 --> 00:04:33.300 align:start position:0% rate uh so you get one you get half a 00:04:33.300 --> 00:04:35.689 align:start position:0% rate uh so you get one you get half a dollar<00:04:33.419> back<00:04:33.660> from<00:04:33.900> me<00:04:34.080> so<00:04:34.560> now<00:04:34.800> I<00:04:35.160> have<00:04:35.220> half<00:04:35.460> a 00:04:35.689 --> 00:04:35.699 align:start position:0% dollar back from me so now I have half a 00:04:35.699 --> 00:04:37.969 align:start position:0% dollar back from me so now I have half a dollar<00:04:35.820> so<00:04:36.660> I<00:04:36.840> get<00:04:37.020> back<00:04:37.199> to<00:04:37.320> Alice<00:04:37.680> and<00:04:37.860> say 00:04:37.969 --> 00:04:37.979 align:start position:0% dollar so I get back to Alice and say 00:04:37.979 --> 00:04:39.890 align:start position:0% dollar so I get back to Alice and say hey<00:04:38.160> Alice<00:04:38.639> I<00:04:39.000> don't<00:04:39.120> want<00:04:39.300> my<00:04:39.479> half<00:04:39.600> dollar 00:04:39.890 --> 00:04:39.900 align:start position:0% hey Alice I don't want my half dollar 00:04:39.900 --> 00:04:41.030 align:start position:0% hey Alice I don't want my half dollar anymore 00:04:41.030 --> 00:04:41.040 align:start position:0% anymore 00:04:41.040 --> 00:04:43.610 align:start position:0% anymore um<00:04:41.160> can<00:04:41.280> I<00:04:41.460> get<00:04:41.580> my<00:04:41.820> Gill<00:04:42.180> back<00:04:42.419> and<00:04:43.020> I<00:04:43.380> offer 00:04:43.610 --> 00:04:43.620 align:start position:0% um can I get my Gill back and I offer 00:04:43.620 --> 00:04:46.430 align:start position:0% um can I get my Gill back and I offer Alice<00:04:43.979> the<00:04:44.460> uh<00:04:44.940> half<00:04:45.300> the<00:04:45.479> dollar<00:04:45.660> and<00:04:46.259> she 00:04:46.430 --> 00:04:46.440 align:start position:0% Alice the uh half the dollar and she 00:04:46.440 --> 00:04:48.409 align:start position:0% Alice the uh half the dollar and she does<00:04:46.680> the<00:04:46.860> computation<00:04:47.280> and<00:04:47.580> now<00:04:47.940> this<00:04:48.240> time 00:04:48.409 --> 00:04:48.419 align:start position:0% does the computation and now this time 00:04:48.419 --> 00:04:50.090 align:start position:0% does the computation and now this time she<00:04:48.720> needs<00:04:48.960> to 00:04:50.090 --> 00:04:50.100 align:start position:0% she needs to 00:04:50.100 --> 00:04:52.249 align:start position:0% she needs to um<00:04:50.160> to<00:04:50.639> to<00:04:50.759> multiply<00:04:51.240> by<00:04:51.479> the<00:04:51.660> exchange<00:04:52.020> rate 00:04:52.249 --> 00:04:52.259 align:start position:0% um to to multiply by the exchange rate 00:04:52.259 --> 00:04:54.830 align:start position:0% um to to multiply by the exchange rate and<00:04:52.800> so<00:04:53.100> she<00:04:53.400> ends<00:04:53.699> up<00:04:53.759> with<00:04:54.000> one<00:04:54.180> girl 00:04:54.830 --> 00:04:54.840 align:start position:0% and so she ends up with one girl 00:04:54.840 --> 00:04:56.990 align:start position:0% and so she ends up with one girl everything<00:04:55.440> went<00:04:55.800> fine<00:04:56.040> I<00:04:56.340> started<00:04:56.580> with<00:04:56.759> one 00:04:56.990 --> 00:04:57.000 align:start position:0% everything went fine I started with one 00:04:57.000 --> 00:04:58.969 align:start position:0% everything went fine I started with one Gill<00:04:57.360> and<00:04:57.600> I<00:04:57.840> ended<00:04:58.020> up<00:04:58.139> with<00:04:58.320> one<00:04:58.500> kill<00:04:58.680> right 00:04:58.969 --> 00:04:58.979 align:start position:0% Gill and I ended up with one kill right 00:04:58.979 --> 00:05:01.670 align:start position:0% Gill and I ended up with one kill right so<00:04:59.820> now<00:05:00.060> let's<00:05:00.300> do<00:05:00.540> the<00:05:00.840> same<00:05:00.960> thing<00:05:01.199> with 00:05:01.670 --> 00:05:01.680 align:start position:0% so now let's do the same thing with 00:05:01.680 --> 00:05:04.790 align:start position:0% so now let's do the same thing with rounding<00:05:02.160> so<00:05:02.880> and<00:05:03.240> for<00:05:03.540> Simplicity<00:05:04.020> I'm<00:05:04.620> just 00:05:04.790 --> 00:05:04.800 align:start position:0% rounding so and for Simplicity I'm just 00:05:04.800 --> 00:05:07.370 align:start position:0% rounding so and for Simplicity I'm just rounding<00:05:05.220> to<00:05:05.460> like<00:05:05.820> uh<00:05:06.419> there's<00:05:06.660> there's<00:05:06.960> no 00:05:07.370 --> 00:05:07.380 align:start position:0% rounding to like uh there's there's no 00:05:07.380 --> 00:05:10.430 align:start position:0% rounding to like uh there's there's no decimal<00:05:08.160> no<00:05:09.060> digit<00:05:09.360> after<00:05:09.540> the<00:05:09.720> decimal<00:05:10.199> point 00:05:10.430 --> 00:05:10.440 align:start position:0% decimal no digit after the decimal point 00:05:10.440 --> 00:05:13.189 align:start position:0% decimal no digit after the decimal point that's<00:05:10.979> just<00:05:11.220> for<00:05:11.400> Simplicity 00:05:13.189 --> 00:05:13.199 align:start position:0% that's just for Simplicity 00:05:13.199 --> 00:05:16.610 align:start position:0% that's just for Simplicity um<00:05:13.259> so<00:05:13.620> now<00:05:13.919> Alice<00:05:14.400> I'm<00:05:14.880> Raul<00:05:15.180> I<00:05:15.479> have<00:05:15.660> one<00:05:16.199> uh 00:05:16.610 --> 00:05:16.620 align:start position:0% um so now Alice I'm Raul I have one uh 00:05:16.620 --> 00:05:18.710 align:start position:0% um so now Alice I'm Raul I have one uh Guild<00:05:16.979> to<00:05:17.160> offer<00:05:17.460> how<00:05:17.820> many<00:05:17.940> dollars<00:05:18.300> do<00:05:18.479> I<00:05:18.600> get 00:05:18.710 --> 00:05:18.720 align:start position:0% Guild to offer how many dollars do I get 00:05:18.720 --> 00:05:21.590 align:start position:0% Guild to offer how many dollars do I get for<00:05:18.840> that<00:05:19.020> let's<00:05:19.800> do<00:05:20.040> the<00:05:20.220> computation<00:05:20.699> and 00:05:21.590 --> 00:05:21.600 align:start position:0% for that let's do the computation and 00:05:21.600 --> 00:05:24.409 align:start position:0% for that let's do the computation and but<00:05:21.960> she<00:05:22.139> does<00:05:22.320> a<00:05:22.440> rounding<00:05:22.860> error 00:05:24.409 --> 00:05:24.419 align:start position:0% but she does a rounding error 00:05:24.419 --> 00:05:25.070 align:start position:0% but she does a rounding error um 00:05:25.070 --> 00:05:25.080 align:start position:0% um 00:05:25.080 --> 00:05:26.870 align:start position:0% um do<00:05:25.500> I<00:05:25.680> have<00:05:25.740> a<00:05:25.860> laser<00:05:26.100> pointer<00:05:26.340> here<00:05:26.520> no<00:05:26.699> I 00:05:26.870 --> 00:05:26.880 align:start position:0% do I have a laser pointer here no I 00:05:26.880 --> 00:05:27.770 align:start position:0% do I have a laser pointer here no I don't 00:05:27.770 --> 00:05:27.780 align:start position:0% don't 00:05:27.780 --> 00:05:30.110 align:start position:0% don't um<00:05:27.900> so<00:05:28.320> she<00:05:28.620> does<00:05:28.740> a<00:05:28.919> rounding<00:05:29.340> aware<00:05:29.639> in<00:05:30.000> this 00:05:30.110 --> 00:05:30.120 align:start position:0% um so she does a rounding aware in this 00:05:30.120 --> 00:05:32.290 align:start position:0% um so she does a rounding aware in this computation<00:05:30.660> so 00:05:32.290 --> 00:05:32.300 align:start position:0% computation so 00:05:32.300 --> 00:05:35.210 align:start position:0% computation so we<00:05:33.300> divide<00:05:33.660> two<00:05:33.960> by<00:05:34.139> one<00:05:34.320> this<00:05:34.560> gives<00:05:34.860> us<00:05:34.979> two 00:05:35.210 --> 00:05:35.220 align:start position:0% we divide two by one this gives us two 00:05:35.220 --> 00:05:37.550 align:start position:0% we divide two by one this gives us two and<00:05:35.639> then<00:05:35.759> we<00:05:35.880> want<00:05:36.120> divide<00:05:36.539> one<00:05:36.780> by<00:05:36.960> two<00:05:37.259> which 00:05:37.550 --> 00:05:37.560 align:start position:0% and then we want divide one by two which 00:05:37.560 --> 00:05:41.150 align:start position:0% and then we want divide one by two which gives<00:05:37.919> us<00:05:38.100> 0.5<00:05:38.940> and<00:05:39.840> we<00:05:40.139> are<00:05:40.320> using<00:05:40.800> uh 00:05:41.150 --> 00:05:41.160 align:start position:0% gives us 0.5 and we are using uh 00:05:41.160 --> 00:05:43.430 align:start position:0% gives us 0.5 and we are using uh rounding<00:05:41.520> to<00:05:41.639> the<00:05:41.820> nearest<00:05:41.940> neighbor<00:05:42.360> here<00:05:43.199> so 00:05:43.430 --> 00:05:43.440 align:start position:0% rounding to the nearest neighbor here so 00:05:43.440 --> 00:05:46.490 align:start position:0% rounding to the nearest neighbor here so that<00:05:43.740> means<00:05:43.979> we<00:05:44.220> are<00:05:44.400> rounding<00:05:44.820> up 00:05:46.490 --> 00:05:46.500 align:start position:0% that means we are rounding up 00:05:46.500 --> 00:05:49.070 align:start position:0% that means we are rounding up um<00:05:46.620> so<00:05:46.919> that<00:05:47.520> means<00:05:47.820> I<00:05:48.180> get<00:05:48.300> one<00:05:48.600> dollar<00:05:48.780> back 00:05:49.070 --> 00:05:49.080 align:start position:0% um so that means I get one dollar back 00:05:49.080 --> 00:05:51.770 align:start position:0% um so that means I get one dollar back from<00:05:49.380> Alice<00:05:49.740> so<00:05:50.280> now<00:05:50.460> I<00:05:50.699> have<00:05:50.759> one<00:05:51.000> dollar 00:05:51.770 --> 00:05:51.780 align:start position:0% from Alice so now I have one dollar 00:05:51.780 --> 00:05:53.749 align:start position:0% from Alice so now I have one dollar uh<00:05:52.500> I<00:05:52.680> go<00:05:52.800> back<00:05:52.919> to<00:05:53.039> our<00:05:53.160> list<00:05:53.340> and<00:05:53.520> say<00:05:53.580> hey 00:05:53.749 --> 00:05:53.759 align:start position:0% uh I go back to our list and say hey 00:05:53.759 --> 00:05:55.610 align:start position:0% uh I go back to our list and say hey Alice<00:05:54.120> I<00:05:54.360> don't<00:05:54.479> want<00:05:54.660> my<00:05:54.840> dollar<00:05:55.020> anymore<00:05:55.380> can 00:05:55.610 --> 00:05:55.620 align:start position:0% Alice I don't want my dollar anymore can 00:05:55.620 --> 00:05:57.830 align:start position:0% Alice I don't want my dollar anymore can I<00:05:55.800> get<00:05:55.860> my<00:05:55.979> Gill<00:05:56.280> back<00:05:56.460> and<00:05:56.880> again<00:05:57.060> Alice<00:05:57.660> do 00:05:57.830 --> 00:05:57.840 align:start position:0% I get my Gill back and again Alice do 00:05:57.840 --> 00:06:00.230 align:start position:0% I get my Gill back and again Alice do the<00:05:58.199> calculation<00:05:58.680> this<00:05:59.400> time<00:05:59.580> she's<00:05:59.820> not<00:06:00.120> even 00:06:00.230 --> 00:06:00.240 align:start position:0% the calculation this time she's not even 00:06:00.240 --> 00:06:02.150 align:start position:0% the calculation this time she's not even doing<00:06:00.419> a<00:06:00.660> rounding<00:06:01.020> error 00:06:02.150 --> 00:06:02.160 align:start position:0% doing a rounding error 00:06:02.160 --> 00:06:04.670 align:start position:0% doing a rounding error um<00:06:02.280> but<00:06:02.699> she<00:06:02.940> ends<00:06:03.180> up<00:06:03.240> giving<00:06:03.539> me<00:06:03.840> two<00:06:04.320> kill 00:06:04.670 --> 00:06:04.680 align:start position:0% um but she ends up giving me two kill 00:06:04.680 --> 00:06:07.189 align:start position:0% um but she ends up giving me two kill and<00:06:05.400> that<00:06:05.699> is<00:06:05.820> the<00:06:06.060> basic<00:06:06.300> problem<00:06:06.539> right<00:06:06.900> I 00:06:07.189 --> 00:06:07.199 align:start position:0% and that is the basic problem right I 00:06:07.199 --> 00:06:10.129 align:start position:0% and that is the basic problem right I started<00:06:07.740> with<00:06:07.979> one<00:06:08.160> girl<00:06:08.419> I<00:06:09.419> did<00:06:09.539> two<00:06:09.780> trades 00:06:10.129 --> 00:06:10.139 align:start position:0% started with one girl I did two trades 00:06:10.139 --> 00:06:11.870 align:start position:0% started with one girl I did two trades with<00:06:10.320> Alice<00:06:10.680> and<00:06:10.919> I<00:06:11.100> ended<00:06:11.340> up<00:06:11.460> with<00:06:11.699> two 00:06:11.870 --> 00:06:11.880 align:start position:0% with Alice and I ended up with two 00:06:11.880 --> 00:06:14.629 align:start position:0% with Alice and I ended up with two guilds<00:06:12.240> in<00:06:12.360> my<00:06:12.479> pocket<00:06:12.780> so<00:06:13.500> in<00:06:13.740> other<00:06:13.860> words<00:06:14.039> I 00:06:14.629 --> 00:06:14.639 align:start position:0% guilds in my pocket so in other words I 00:06:14.639 --> 00:06:17.870 align:start position:0% guilds in my pocket so in other words I just<00:06:14.880> like<00:06:15.479> created<00:06:16.020> money<00:06:16.320> out<00:06:16.560> of<00:06:16.680> thin<00:06:16.919> air 00:06:17.870 --> 00:06:17.880 align:start position:0% just like created money out of thin air 00:06:17.880 --> 00:06:20.390 align:start position:0% just like created money out of thin air so<00:06:18.600> let's<00:06:18.900> bring<00:06:19.139> this<00:06:19.500> example<00:06:19.979> into<00:06:20.160> the 00:06:20.390 --> 00:06:20.400 align:start position:0% so let's bring this example into the 00:06:20.400 --> 00:06:22.309 align:start position:0% so let's bring this example into the blockchain<00:06:20.759> context 00:06:22.309 --> 00:06:22.319 align:start position:0% blockchain context 00:06:22.319 --> 00:06:24.529 align:start position:0% blockchain context um<00:06:22.380> so<00:06:22.740> the<00:06:23.280> important<00:06:23.639> thing<00:06:23.940> here<00:06:24.180> in<00:06:24.419> this 00:06:24.529 --> 00:06:24.539 align:start position:0% um so the important thing here in this 00:06:24.539 --> 00:06:27.469 align:start position:0% um so the important thing here in this example<00:06:24.840> was<00:06:25.020> that<00:06:25.259> I<00:06:25.500> needed<00:06:25.800> two<00:06:26.100> trades<00:06:26.580> and 00:06:27.469 --> 00:06:27.479 align:start position:0% example was that I needed two trades and 00:06:27.479 --> 00:06:30.290 align:start position:0% example was that I needed two trades and like<00:06:27.840> in<00:06:28.139> in<00:06:28.319> many<00:06:28.560> smart<00:06:28.800> contracts<00:06:29.460> you<00:06:30.120> will 00:06:30.290 --> 00:06:30.300 align:start position:0% like in in many smart contracts you will 00:06:30.300 --> 00:06:31.370 align:start position:0% like in in many smart contracts you will see 00:06:31.370 --> 00:06:31.380 align:start position:0% see 00:06:31.380 --> 00:06:34.010 align:start position:0% see a<00:06:31.860> pair<00:06:31.979> of<00:06:32.160> trading<00:06:32.639> functions<00:06:33.060> like<00:06:33.419> a 00:06:34.010 --> 00:06:34.020 align:start position:0% a pair of trading functions like a 00:06:34.020 --> 00:06:35.809 align:start position:0% a pair of trading functions like a deposit<00:06:34.440> and<00:06:34.620> a<00:06:34.740> redu-im<00:06:35.220> function<00:06:35.580> or 00:06:35.809 --> 00:06:35.819 align:start position:0% deposit and a redu-im function or 00:06:35.819 --> 00:06:38.270 align:start position:0% deposit and a redu-im function or deposit<00:06:36.300> and<00:06:36.479> withdraw<00:06:37.020> stake<00:06:37.680> and<00:06:37.800> unstake 00:06:38.270 --> 00:06:38.280 align:start position:0% deposit and withdraw stake and unstake 00:06:38.280 --> 00:06:40.189 align:start position:0% deposit and withdraw stake and unstake function<00:06:38.699> and<00:06:39.300> so<00:06:39.479> on 00:06:40.189 --> 00:06:40.199 align:start position:0% function and so on 00:06:40.199 --> 00:06:43.790 align:start position:0% function and so on and<00:06:40.819> so<00:06:41.819> what<00:06:42.479> what<00:06:42.539> happened<00:06:43.080> here<00:06:43.319> what<00:06:43.680> went 00:06:43.790 --> 00:06:43.800 align:start position:0% and so what what happened here what went 00:06:43.800 --> 00:06:45.409 align:start position:0% and so what what happened here what went wrong<00:06:44.039> like<00:06:44.340> you<00:06:44.520> know<00:06:44.639> have<00:06:44.940> a<00:06:45.060> look<00:06:45.120> at<00:06:45.300> the 00:06:45.409 --> 00:06:45.419 align:start position:0% wrong like you know have a look at the 00:06:45.419 --> 00:06:48.230 align:start position:0% wrong like you know have a look at the red<00:06:45.539> line<00:06:45.900> so<00:06:46.560> I<00:06:46.919> deposited<00:06:47.460> one<00:06:47.699> Guild<00:06:48.000> to 00:06:48.230 --> 00:06:48.240 align:start position:0% red line so I deposited one Guild to 00:06:48.240 --> 00:06:50.749 align:start position:0% red line so I deposited one Guild to Alice<00:06:48.600> and<00:06:49.199> then<00:06:49.380> I<00:06:49.620> immediately<00:06:50.039> redeemed<00:06:50.639> it 00:06:50.749 --> 00:06:50.759 align:start position:0% Alice and then I immediately redeemed it 00:06:50.759 --> 00:06:52.909 align:start position:0% Alice and then I immediately redeemed it like<00:06:50.940> in<00:06:51.180> the<00:06:51.300> same<00:06:51.419> transaction<00:06:51.960> and<00:06:52.620> I<00:06:52.740> was 00:06:52.909 --> 00:06:52.919 align:start position:0% like in the same transaction and I was 00:06:52.919 --> 00:06:56.090 align:start position:0% like in the same transaction and I was able<00:06:53.220> to<00:06:53.340> make<00:06:53.580> two<00:06:53.819> kill<00:06:54.060> out<00:06:54.419> of<00:06:54.539> that<00:06:54.740> so<00:06:55.740> I 00:06:56.090 --> 00:06:56.100 align:start position:0% able to make two kill out of that so I 00:06:56.100 --> 00:06:58.969 align:start position:0% able to make two kill out of that so I created<00:06:56.520> money<00:06:56.699> out<00:06:56.880> of<00:06:57.060> thin<00:06:57.240> air<00:06:57.419> so 00:06:58.969 --> 00:06:58.979 align:start position:0% created money out of thin air so 00:06:58.979 --> 00:07:00.290 align:start position:0% created money out of thin air so um 00:07:00.290 --> 00:07:00.300 align:start position:0% um 00:07:00.300 --> 00:07:05.510 align:start position:0% um now<00:07:01.139> okay<00:07:02.100> so<00:07:03.259> we<00:07:04.259> we<00:07:04.620> don't<00:07:04.860> want<00:07:05.039> that<00:07:05.220> right 00:07:05.510 --> 00:07:05.520 align:start position:0% now okay so we we don't want that right 00:07:05.520 --> 00:07:08.510 align:start position:0% now okay so we we don't want that right we<00:07:06.060> need<00:07:06.180> to<00:07:06.300> fix<00:07:06.539> that<00:07:06.780> so<00:07:07.380> we<00:07:07.560> need<00:07:07.740> to<00:07:07.979> like 00:07:08.510 --> 00:07:08.520 align:start position:0% we need to fix that so we need to like 00:07:08.520 --> 00:07:11.330 align:start position:0% we need to fix that so we need to like make<00:07:08.819> a<00:07:09.000> sanity<00:07:09.360> check<00:07:09.720> that<00:07:10.139> we<00:07:10.800> don't<00:07:10.979> get 00:07:11.330 --> 00:07:11.340 align:start position:0% make a sanity check that we don't get 00:07:11.340 --> 00:07:14.090 align:start position:0% make a sanity check that we don't get like<00:07:11.699> more<00:07:12.000> money<00:07:12.240> out<00:07:12.479> than<00:07:12.780> we<00:07:13.020> put<00:07:13.199> in 00:07:14.090 --> 00:07:14.100 align:start position:0% like more money out than we put in 00:07:14.100 --> 00:07:16.969 align:start position:0% like more money out than we put in um<00:07:14.220> and<00:07:14.580> this<00:07:15.180> is<00:07:15.300> the<00:07:15.419> second<00:07:15.780> line<00:07:16.139> here<00:07:16.500> this 00:07:16.969 --> 00:07:16.979 align:start position:0% um and this is the second line here this 00:07:16.979 --> 00:07:19.370 align:start position:0% um and this is the second line here this is<00:07:17.100> my<00:07:17.400> sanity<00:07:17.819> assumption<00:07:18.360> that<00:07:18.840> when<00:07:19.020> I<00:07:19.199> put 00:07:19.370 --> 00:07:19.380 align:start position:0% is my sanity assumption that when I put 00:07:19.380 --> 00:07:22.010 align:start position:0% is my sanity assumption that when I put one<00:07:19.740> Guild<00:07:20.099> into<00:07:20.340> the<00:07:20.580> contract<00:07:20.940> or 00:07:22.010 --> 00:07:22.020 align:start position:0% one Guild into the contract or 00:07:22.020 --> 00:07:23.870 align:start position:0% one Guild into the contract or um<00:07:22.080> I<00:07:22.259> should<00:07:22.560> be<00:07:22.680> able<00:07:22.800> to<00:07:22.919> get<00:07:23.099> at<00:07:23.340> most<00:07:23.520> one 00:07:23.870 --> 00:07:23.880 align:start position:0% um I should be able to get at most one 00:07:23.880 --> 00:07:27.350 align:start position:0% um I should be able to get at most one kill<00:07:24.060> out<00:07:24.360> if<00:07:24.960> I<00:07:25.139> immediately<00:07:25.680> redeem 00:07:27.350 --> 00:07:27.360 align:start position:0% kill out if I immediately redeem 00:07:27.360 --> 00:07:29.390 align:start position:0% kill out if I immediately redeem um<00:07:27.479> and<00:07:27.720> of<00:07:27.960> course<00:07:28.080> this<00:07:28.740> concept<00:07:28.979> can<00:07:29.220> be 00:07:29.390 --> 00:07:29.400 align:start position:0% um and of course this concept can be 00:07:29.400 --> 00:07:31.249 align:start position:0% um and of course this concept can be generalized<00:07:30.000> it<00:07:30.180> shouldn't<00:07:30.599> only<00:07:30.720> hold<00:07:30.960> for 00:07:31.249 --> 00:07:31.259 align:start position:0% generalized it shouldn't only hold for 00:07:31.259 --> 00:07:33.230 align:start position:0% generalized it shouldn't only hold for one<00:07:31.500> gear<00:07:31.800> but<00:07:32.039> it<00:07:32.400> should<00:07:32.580> essentially<00:07:32.940> hold 00:07:33.230 --> 00:07:33.240 align:start position:0% one gear but it should essentially hold 00:07:33.240 --> 00:07:34.550 align:start position:0% one gear but it should essentially hold for<00:07:33.539> for 00:07:34.550 --> 00:07:34.560 align:start position:0% for for 00:07:34.560 --> 00:07:36.050 align:start position:0% for for um arbitrary<00:07:35.099> amounts<00:07:35.580> that<00:07:35.699> I'm<00:07:35.819> putting 00:07:36.050 --> 00:07:36.060 align:start position:0% um arbitrary amounts that I'm putting 00:07:36.060 --> 00:07:39.650 align:start position:0% um arbitrary amounts that I'm putting into<00:07:36.240> the<00:07:36.479> contract 00:07:39.650 --> 00:07:39.660 align:start position:0% 00:07:39.660 --> 00:07:43.010 align:start position:0% um so<00:07:40.080> this<00:07:40.680> is<00:07:40.740> what<00:07:41.160> a<00:07:41.580> typical<00:07:41.880> the<00:07:42.599> typical 00:07:43.010 --> 00:07:43.020 align:start position:0% um so this is what a typical the typical 00:07:43.020 --> 00:07:44.809 align:start position:0% um so this is what a typical the typical implementation<00:07:43.740> of 00:07:44.809 --> 00:07:44.819 align:start position:0% implementation of 00:07:44.819 --> 00:07:47.210 align:start position:0% implementation of um a<00:07:45.419> deposit<00:07:46.020> and<00:07:46.199> a<00:07:46.319> redeem<00:07:46.620> function<00:07:46.979> look 00:07:47.210 --> 00:07:47.220 align:start position:0% um a deposit and a redeem function look 00:07:47.220 --> 00:07:49.670 align:start position:0% um a deposit and a redeem function look like<00:07:47.400> looks<00:07:47.759> like<00:07:47.880> and 00:07:49.670 --> 00:07:49.680 align:start position:0% like looks like and 00:07:49.680 --> 00:07:52.070 align:start position:0% like looks like and um<00:07:49.800> what<00:07:50.039> you<00:07:50.220> can<00:07:50.400> see<00:07:50.699> here<00:07:51.000> is<00:07:51.300> like<00:07:51.780> let's 00:07:52.070 --> 00:07:52.080 align:start position:0% um what you can see here is like let's 00:07:52.080 --> 00:07:53.629 align:start position:0% um what you can see here is like let's walk<00:07:52.440> over<00:07:52.620> the<00:07:52.860> deposit<00:07:53.220> function<00:07:53.460> real 00:07:53.629 --> 00:07:53.639 align:start position:0% walk over the deposit function real 00:07:53.639 --> 00:07:56.629 align:start position:0% walk over the deposit function real quick<00:07:53.880> so<00:07:54.180> the<00:07:54.360> deposit<00:07:54.840> function<00:07:55.220> accepts<00:07:56.220> an 00:07:56.629 --> 00:07:56.639 align:start position:0% quick so the deposit function accepts an 00:07:56.639 --> 00:08:00.170 align:start position:0% quick so the deposit function accepts an asset<00:07:57.000> amount<00:07:57.680> and<00:07:58.680> then<00:07:59.039> it<00:07:59.340> converts<00:07:59.819> this 00:08:00.170 --> 00:08:00.180 align:start position:0% asset amount and then it converts this 00:08:00.180 --> 00:08:02.150 align:start position:0% asset amount and then it converts this asset<00:08:00.539> amount<00:08:00.840> into<00:08:01.199> shares<00:08:01.740> just<00:08:01.979> by 00:08:02.150 --> 00:08:02.160 align:start position:0% asset amount into shares just by 00:08:02.160 --> 00:08:04.430 align:start position:0% asset amount into shares just by multiplying<00:08:02.759> the<00:08:03.000> amount<00:08:03.240> of<00:08:03.419> assets<00:08:03.780> with<00:08:04.259> a 00:08:04.430 --> 00:08:04.440 align:start position:0% multiplying the amount of assets with a 00:08:04.440 --> 00:08:05.930 align:start position:0% multiplying the amount of assets with a current<00:08:04.620> exchange<00:08:05.160> rate 00:08:05.930 --> 00:08:05.940 align:start position:0% current exchange rate 00:08:05.940 --> 00:08:07.909 align:start position:0% current exchange rate then<00:08:06.419> we<00:08:06.539> are<00:08:06.720> transferring<00:08:07.199> the<00:08:07.440> asset<00:08:07.740> we 00:08:07.909 --> 00:08:07.919 align:start position:0% then we are transferring the asset we 00:08:07.919 --> 00:08:09.710 align:start position:0% then we are transferring the asset we are<00:08:08.039> pulling<00:08:08.340> in<00:08:08.460> we<00:08:08.880> are<00:08:09.000> pulling<00:08:09.300> the<00:08:09.419> Assets 00:08:09.710 --> 00:08:09.720 align:start position:0% are pulling in we are pulling the Assets 00:08:09.720 --> 00:08:11.089 align:start position:0% are pulling in we are pulling the Assets in<00:08:10.020> from<00:08:10.319> the 00:08:11.089 --> 00:08:11.099 align:start position:0% in from the 00:08:11.099 --> 00:08:13.550 align:start position:0% in from the um<00:08:11.160> from<00:08:11.460> the<00:08:11.580> user<00:08:11.940> uh<00:08:12.720> then<00:08:12.960> we<00:08:13.139> are<00:08:13.199> minting 00:08:13.550 --> 00:08:13.560 align:start position:0% um from the user uh then we are minting 00:08:13.560 --> 00:08:15.469 align:start position:0% um from the user uh then we are minting some<00:08:13.740> shares<00:08:14.160> and<00:08:14.280> finally<00:08:14.580> we<00:08:14.940> return<00:08:15.120> the 00:08:15.469 --> 00:08:15.479 align:start position:0% some shares and finally we return the 00:08:15.479 --> 00:08:17.870 align:start position:0% some shares and finally we return the shares<00:08:15.900> that<00:08:16.500> we<00:08:16.680> have<00:08:16.800> minted<00:08:17.220> and<00:08:17.759> the 00:08:17.870 --> 00:08:17.880 align:start position:0% shares that we have minted and the 00:08:17.880 --> 00:08:20.749 align:start position:0% shares that we have minted and the redeem<00:08:18.180> function<00:08:18.539> is<00:08:18.720> similar<00:08:19.440> and<00:08:20.220> with<00:08:20.580> what 00:08:20.749 --> 00:08:20.759 align:start position:0% redeem function is similar and with what 00:08:20.759 --> 00:08:23.390 align:start position:0% redeem function is similar and with what I<00:08:21.000> just<00:08:21.360> told<00:08:21.539> you<00:08:21.840> you<00:08:22.139> can<00:08:22.379> see<00:08:22.620> or<00:08:22.979> maybe<00:08:23.160> you 00:08:23.390 --> 00:08:23.400 align:start position:0% I just told you you can see or maybe you 00:08:23.400 --> 00:08:25.550 align:start position:0% I just told you you can see or maybe you cannot<00:08:23.699> see<00:08:23.879> it<00:08:24.060> because<00:08:24.300> well<00:08:24.780> I<00:08:25.080> didn't<00:08:25.199> use 00:08:25.550 --> 00:08:25.560 align:start position:0% cannot see it because well I didn't use 00:08:25.560 --> 00:08:28.129 align:start position:0% cannot see it because well I didn't use the<00:08:26.099> uh<00:08:26.639> you<00:08:27.240> cannot<00:08:27.419> see<00:08:27.599> the<00:08:27.720> implementation 00:08:28.129 --> 00:08:28.139 align:start position:0% the uh you cannot see the implementation 00:08:28.139 --> 00:08:30.290 align:start position:0% the uh you cannot see the implementation of<00:08:28.379> the<00:08:28.500> multiplication<00:08:29.039> function 00:08:30.290 --> 00:08:30.300 align:start position:0% of the multiplication function 00:08:30.300 --> 00:08:33.050 align:start position:0% of the multiplication function um<00:08:30.360> but<00:08:30.720> like<00:08:31.199> this<00:08:31.620> contract<00:08:32.039> is<00:08:32.520> suffering 00:08:33.050 --> 00:08:33.060 align:start position:0% um but like this contract is suffering 00:08:33.060 --> 00:08:35.389 align:start position:0% um but like this contract is suffering uh<00:08:33.659> from<00:08:33.899> the<00:08:34.080> exact<00:08:34.320> vulnerability<00:08:35.099> that 00:08:35.389 --> 00:08:35.399 align:start position:0% uh from the exact vulnerability that 00:08:35.399 --> 00:08:37.670 align:start position:0% uh from the exact vulnerability that that<00:08:35.640> I<00:08:36.000> showed<00:08:36.360> you<00:08:36.419> before 00:08:37.670 --> 00:08:37.680 align:start position:0% that I showed you before 00:08:37.680 --> 00:08:39.709 align:start position:0% that I showed you before um<00:08:37.800> and<00:08:38.039> that<00:08:38.219> was<00:08:38.339> present<00:08:38.760> in<00:08:39.060> a<00:08:39.180> like<00:08:39.419> more 00:08:39.709 --> 00:08:39.719 align:start position:0% um and that was present in a like more 00:08:39.719 --> 00:08:43.909 align:start position:0% um and that was present in a like more complicated<00:08:40.520> uh<00:08:41.520> a<00:08:42.120> more<00:08:42.899> complex<00:08:43.140> setting<00:08:43.620> in 00:08:43.909 --> 00:08:43.919 align:start position:0% complicated uh a more complex setting in 00:08:43.919 --> 00:08:47.630 align:start position:0% complicated uh a more complex setting in this<00:08:44.159> uh<00:08:44.880> in<00:08:45.420> this<00:08:45.600> unit<00:08:46.020> swap<00:08:46.500> contract<00:08:47.040> that 00:08:47.630 --> 00:08:47.640 align:start position:0% this uh in this unit swap contract that 00:08:47.640 --> 00:08:49.730 align:start position:0% this uh in this unit swap contract that I<00:08:47.760> talked<00:08:48.000> about<00:08:48.120> earlier 00:08:49.730 --> 00:08:49.740 align:start position:0% I talked about earlier 00:08:49.740 --> 00:08:52.190 align:start position:0% I talked about earlier um<00:08:49.920> so<00:08:50.700> this<00:08:51.060> multiplication<00:08:51.600> function<00:08:51.959> and 00:08:52.190 --> 00:08:52.200 align:start position:0% um so this multiplication function and 00:08:52.200 --> 00:08:54.470 align:start position:0% um so this multiplication function and this<00:08:52.380> division<00:08:52.680> function<00:08:53.040> is<00:08:53.279> is<00:08:53.580> implemented 00:08:54.470 --> 00:08:54.480 align:start position:0% this division function is is implemented 00:08:54.480 --> 00:08:56.690 align:start position:0% this division function is is implemented as<00:08:55.260> like<00:08:55.500> rounding<00:08:55.980> to<00:08:56.100> the<00:08:56.220> nearest<00:08:56.339> neighbor 00:08:56.690 --> 00:08:56.700 align:start position:0% as like rounding to the nearest neighbor 00:08:56.700 --> 00:08:58.550 align:start position:0% as like rounding to the nearest neighbor and<00:08:57.000> that<00:08:57.180> is<00:08:57.300> the<00:08:57.480> mistake<00:08:57.839> that<00:08:58.080> we<00:08:58.200> did<00:08:58.380> here 00:08:58.550 --> 00:08:58.560 align:start position:0% and that is the mistake that we did here 00:08:58.560 --> 00:09:01.430 align:start position:0% and that is the mistake that we did here but<00:08:59.220> like<00:08:59.880> how<00:09:00.360> do<00:09:00.540> we<00:09:00.660> actually<00:09:00.839> know<00:09:01.140> in 00:09:01.430 --> 00:09:01.440 align:start position:0% but like how do we actually know in 00:09:01.440 --> 00:09:03.769 align:start position:0% but like how do we actually know in which<00:09:01.620> direction<00:09:01.800> we<00:09:02.220> should<00:09:02.339> round<00:09:02.519> and 00:09:03.769 --> 00:09:03.779 align:start position:0% which direction we should round and 00:09:03.779 --> 00:09:06.829 align:start position:0% which direction we should round and um<00:09:03.839> there's<00:09:04.260> like<00:09:04.500> a<00:09:04.800> very<00:09:04.920> simple<00:09:05.279> uh 00:09:06.829 --> 00:09:06.839 align:start position:0% um there's like a very simple uh 00:09:06.839 --> 00:09:09.949 align:start position:0% um there's like a very simple uh a<00:09:07.140> very<00:09:07.560> simple<00:09:07.920> rule<00:09:08.399> of<00:09:08.519> some<00:09:08.820> rule<00:09:09.720> of<00:09:09.779> thumb 00:09:09.949 --> 00:09:09.959 align:start position:0% a very simple rule of some rule of thumb 00:09:09.959 --> 00:09:12.949 align:start position:0% a very simple rule of some rule of thumb that<00:09:10.200> I<00:09:10.440> can<00:09:10.620> give<00:09:11.160> you<00:09:11.279> and<00:09:11.459> that<00:09:11.700> is<00:09:11.880> I<00:09:12.660> call 00:09:12.949 --> 00:09:12.959 align:start position:0% that I can give you and that is I call 00:09:12.959 --> 00:09:15.829 align:start position:0% that I can give you and that is I call it<00:09:13.140> keep<00:09:13.680> the<00:09:13.860> change<00:09:14.100> that<00:09:14.519> means<00:09:14.839> whenever 00:09:15.829 --> 00:09:15.839 align:start position:0% it keep the change that means whenever 00:09:15.839 --> 00:09:19.130 align:start position:0% it keep the change that means whenever we<00:09:16.140> whenever<00:09:16.680> we<00:09:17.160> are<00:09:17.279> rounding<00:09:17.700> up<00:09:17.959> uh<00:09:18.959> oh 00:09:19.130 --> 00:09:19.140 align:start position:0% we whenever we are rounding up uh oh 00:09:19.140 --> 00:09:21.889 align:start position:0% we whenever we are rounding up uh oh sorry<00:09:19.500> whenever<00:09:20.399> we<00:09:20.760> have<00:09:20.940> incoming<00:09:21.480> assets 00:09:21.889 --> 00:09:21.899 align:start position:0% sorry whenever we have incoming assets 00:09:21.899 --> 00:09:25.190 align:start position:0% sorry whenever we have incoming assets like<00:09:22.800> accept<00:09:23.160> assets<00:09:23.700> from<00:09:23.940> the<00:09:24.120> user<00:09:24.480> then<00:09:25.019> we 00:09:25.190 --> 00:09:25.200 align:start position:0% like accept assets from the user then we 00:09:25.200 --> 00:09:28.070 align:start position:0% like accept assets from the user then we are<00:09:25.320> going<00:09:25.500> to<00:09:25.620> round<00:09:25.800> up<00:09:26.100> and<00:09:26.940> whenever<00:09:27.360> like 00:09:28.070 --> 00:09:28.080 align:start position:0% are going to round up and whenever like 00:09:28.080 --> 00:09:30.769 align:start position:0% are going to round up and whenever like we<00:09:28.380> are<00:09:28.500> sending<00:09:28.860> assets<00:09:29.279> out<00:09:29.580> to<00:09:29.880> the<00:09:30.000> user<00:09:30.360> we 00:09:30.769 --> 00:09:30.779 align:start position:0% we are sending assets out to the user we 00:09:30.779 --> 00:09:33.290 align:start position:0% we are sending assets out to the user we are<00:09:30.959> rounding<00:09:31.320> down<00:09:31.560> and<00:09:32.399> if<00:09:32.519> we<00:09:32.700> follow<00:09:32.940> this 00:09:33.290 --> 00:09:33.300 align:start position:0% are rounding down and if we follow this 00:09:33.300 --> 00:09:36.170 align:start position:0% are rounding down and if we follow this this<00:09:33.600> rule<00:09:34.080> that<00:09:34.980> means<00:09:35.339> you<00:09:35.880> will 00:09:36.170 --> 00:09:36.180 align:start position:0% this rule that means you will 00:09:36.180 --> 00:09:38.210 align:start position:0% this rule that means you will approximate<00:09:36.899> your<00:09:37.200> values<00:09:37.560> from<00:09:37.860> the<00:09:38.040> right 00:09:38.210 --> 00:09:38.220 align:start position:0% approximate your values from the right 00:09:38.220 --> 00:09:40.490 align:start position:0% approximate your values from the right direction<00:09:38.519> and<00:09:39.360> users<00:09:39.720> won't<00:09:39.959> be<00:09:40.140> able<00:09:40.320> to 00:09:40.490 --> 00:09:40.500 align:start position:0% direction and users won't be able to 00:09:40.500 --> 00:09:42.290 align:start position:0% direction and users won't be able to create<00:09:40.800> money<00:09:41.160> out<00:09:41.339> of<00:09:41.519> thin<00:09:41.700> air<00:09:41.880> and<00:09:42.060> doing 00:09:42.290 --> 00:09:42.300 align:start position:0% create money out of thin air and doing 00:09:42.300 --> 00:09:45.110 align:start position:0% create money out of thin air and doing your<00:09:42.600> contracts<00:09:43.019> that<00:09:43.680> is<00:09:43.860> the<00:09:44.160> simple<00:09:44.339> rule 00:09:45.110 --> 00:09:45.120 align:start position:0% your contracts that is the simple rule 00:09:45.120 --> 00:09:47.990 align:start position:0% your contracts that is the simple rule so<00:09:45.779> that<00:09:46.140> means<00:09:46.440> like<00:09:46.860> let's<00:09:47.160> revisit<00:09:47.820> the 00:09:47.990 --> 00:09:48.000 align:start position:0% so that means like let's revisit the 00:09:48.000 --> 00:09:50.750 align:start position:0% so that means like let's revisit the example<00:09:48.420> from<00:09:48.600> before<00:09:48.839> so 00:09:50.750 --> 00:09:50.760 align:start position:0% example from before so 00:09:50.760 --> 00:09:52.970 align:start position:0% example from before so um<00:09:50.820> like<00:09:51.660> let's<00:09:52.019> walk<00:09:52.200> over<00:09:52.320> the<00:09:52.560> deposit 00:09:52.970 --> 00:09:52.980 align:start position:0% um like let's walk over the deposit 00:09:52.980 --> 00:09:54.889 align:start position:0% um like let's walk over the deposit functions<00:09:53.399> so<00:09:53.580> instead<00:09:54.120> of<00:09:54.360> like<00:09:54.660> just 00:09:54.889 --> 00:09:54.899 align:start position:0% functions so instead of like just 00:09:54.899 --> 00:09:58.370 align:start position:0% functions so instead of like just multiplying<00:09:55.560> I<00:09:56.100> just<00:09:56.279> know<00:09:56.459> now<00:09:56.760> I<00:09:57.300> use<00:09:57.480> now 00:09:58.370 --> 00:09:58.380 align:start position:0% multiplying I just know now I use now 00:09:58.380 --> 00:09:59.870 align:start position:0% multiplying I just know now I use now um<00:09:58.440> a<00:09:58.740> variation<00:09:59.040> of<00:09:59.279> the<00:09:59.399> multiplication 00:09:59.870 --> 00:09:59.880 align:start position:0% um a variation of the multiplication 00:09:59.880 --> 00:10:03.769 align:start position:0% um a variation of the multiplication function<00:10:00.360> that<00:10:01.019> always<00:10:01.320> rounds<00:10:01.980> down<00:10:02.220> and<00:10:03.180> it 00:10:03.769 --> 00:10:03.779 align:start position:0% function that always rounds down and it 00:10:03.779 --> 00:10:06.170 align:start position:0% function that always rounds down and it runs<00:10:04.080> down<00:10:04.260> because<00:10:04.800> I'm<00:10:05.160> sending<00:10:05.580> the<00:10:05.760> assets 00:10:06.170 --> 00:10:06.180 align:start position:0% runs down because I'm sending the assets 00:10:06.180 --> 00:10:08.750 align:start position:0% runs down because I'm sending the assets out<00:10:06.839> to<00:10:07.140> the<00:10:07.260> user 00:10:08.750 --> 00:10:08.760 align:start position:0% out to the user 00:10:08.760 --> 00:10:11.329 align:start position:0% out to the user and<00:10:09.300> for<00:10:09.540> the<00:10:09.720> redeem<00:10:09.959> function<00:10:10.380> here<00:10:10.860> in<00:10:11.040> this 00:10:11.329 --> 00:10:11.339 align:start position:0% and for the redeem function here in this 00:10:11.339 --> 00:10:14.329 align:start position:0% and for the redeem function here in this example<00:10:11.700> it's<00:10:12.060> it's<00:10:12.300> the<00:10:12.600> same 00:10:14.329 --> 00:10:14.339 align:start position:0% example it's it's the same 00:10:14.339 --> 00:10:17.389 align:start position:0% example it's it's the same um<00:10:14.459> so<00:10:14.940> now 00:10:17.389 --> 00:10:17.399 align:start position:0% um so now 00:10:17.399 --> 00:10:20.389 align:start position:0% um so now how<00:10:18.000> can<00:10:18.240> we<00:10:18.480> actually<00:10:19.019> be<00:10:19.500> sure<00:10:19.680> that<00:10:20.100> our 00:10:20.389 --> 00:10:20.399 align:start position:0% how can we actually be sure that our 00:10:20.399 --> 00:10:22.070 align:start position:0% how can we actually be sure that our implementation<00:10:21.000> is<00:10:21.240> correct<00:10:21.480> I<00:10:21.720> mean<00:10:21.839> this 00:10:22.070 --> 00:10:22.080 align:start position:0% implementation is correct I mean this 00:10:22.080 --> 00:10:23.750 align:start position:0% implementation is correct I mean this example<00:10:22.380> was<00:10:22.620> really<00:10:22.860> simple<00:10:23.040> and<00:10:23.339> you<00:10:23.580> were 00:10:23.750 --> 00:10:23.760 align:start position:0% example was really simple and you were 00:10:23.760 --> 00:10:27.050 align:start position:0% example was really simple and you were maybe<00:10:24.060> able<00:10:24.480> to<00:10:24.600> follow<00:10:24.839> it<00:10:25.080> like<00:10:25.380> on<00:10:25.620> the<00:10:26.160> spot 00:10:27.050 --> 00:10:27.060 align:start position:0% maybe able to follow it like on the spot 00:10:27.060 --> 00:10:30.050 align:start position:0% maybe able to follow it like on the spot um<00:10:27.120> but<00:10:27.300> but<00:10:27.540> like<00:10:28.140> uh 00:10:30.050 --> 00:10:30.060 align:start position:0% um but but like uh 00:10:30.060 --> 00:10:31.490 align:start position:0% um but but like uh um<00:10:30.180> when<00:10:30.420> you're<00:10:30.540> working<00:10:30.779> when<00:10:31.200> you're<00:10:31.320> a 00:10:31.490 --> 00:10:31.500 align:start position:0% um when you're working when you're a 00:10:31.500 --> 00:10:33.230 align:start position:0% um when you're working when you're a developer<00:10:31.920> and<00:10:32.100> working<00:10:32.279> on<00:10:32.519> a<00:10:32.700> like<00:10:32.880> real 00:10:33.230 --> 00:10:33.240 align:start position:0% developer and working on a like real 00:10:33.240 --> 00:10:35.570 align:start position:0% developer and working on a like real world<00:10:33.480> contract<00:10:34.080> your<00:10:34.680> logic<00:10:35.100> will<00:10:35.279> be<00:10:35.459> more 00:10:35.570 --> 00:10:35.580 align:start position:0% world contract your logic will be more 00:10:35.580 --> 00:10:37.910 align:start position:0% world contract your logic will be more complex<00:10:35.940> so<00:10:36.180> you<00:10:36.420> want<00:10:36.480> to<00:10:36.660> have<00:10:36.779> tests<00:10:37.320> that 00:10:37.910 --> 00:10:37.920 align:start position:0% complex so you want to have tests that 00:10:37.920 --> 00:10:40.009 align:start position:0% complex so you want to have tests that ensure<00:10:38.339> that<00:10:38.700> you<00:10:39.000> can 00:10:40.009 --> 00:10:40.019 align:start position:0% ensure that you can 00:10:40.019 --> 00:10:41.570 align:start position:0% ensure that you can um<00:10:40.080> actually 00:10:41.570 --> 00:10:41.580 align:start position:0% um actually 00:10:41.580 --> 00:10:44.750 align:start position:0% um actually um<00:10:41.940> detect<00:10:42.600> counter<00:10:43.080> examples<00:10:43.500> and<00:10:43.860> achieve<00:10:44.640> a 00:10:44.750 --> 00:10:44.760 align:start position:0% um detect counter examples and achieve a 00:10:44.760 --> 00:10:47.150 align:start position:0% um detect counter examples and achieve a higher<00:10:45.000> level<00:10:45.060> of<00:10:45.300> confidence<00:10:45.600> so<00:10:46.440> we<00:10:46.860> are<00:10:46.980> now 00:10:47.150 --> 00:10:47.160 align:start position:0% higher level of confidence so we are now 00:10:47.160 --> 00:10:49.190 align:start position:0% higher level of confidence so we are now looking<00:10:47.519> at<00:10:48.180> the 00:10:49.190 --> 00:10:49.200 align:start position:0% looking at the 00:10:49.200 --> 00:10:52.430 align:start position:0% looking at the um<00:10:49.620> at<00:10:50.220> a<00:10:50.399> property<00:10:51.060> test<00:10:51.300> so 00:10:52.430 --> 00:10:52.440 align:start position:0% um at a property test so 00:10:52.440 --> 00:10:54.350 align:start position:0% um at a property test so um that<00:10:52.800> is<00:10:52.980> basically<00:10:53.519> just<00:10:53.820> like<00:10:54.000> a<00:10:54.240> unit 00:10:54.350 --> 00:10:54.360 align:start position:0% um that is basically just like a unit 00:10:54.360 --> 00:10:55.670 align:start position:0% um that is basically just like a unit test 00:10:55.670 --> 00:10:55.680 align:start position:0% test 00:10:55.680 --> 00:10:57.889 align:start position:0% test um but<00:10:55.920> it<00:10:56.040> has<00:10:56.220> parameters<00:10:56.820> parameters<00:10:57.660> to 00:10:57.889 --> 00:10:57.899 align:start position:0% um but it has parameters parameters to 00:10:57.899 --> 00:11:00.710 align:start position:0% um but it has parameters parameters to it<00:10:58.019> so<00:10:58.740> it<00:10:58.980> has<00:10:59.100> two<00:10:59.339> parameters<00:10:59.940> shares<00:11:00.600> per 00:11:00.710 --> 00:11:00.720 align:start position:0% it so it has two parameters shares per 00:11:00.720 --> 00:11:04.250 align:start position:0% it so it has two parameters shares per asset<00:11:01.079> which<00:11:01.500> should<00:11:01.920> just<00:11:02.160> uh<00:11:03.000> it's<00:11:03.480> just<00:11:03.660> the 00:11:04.250 --> 00:11:04.260 align:start position:0% asset which should just uh it's just the 00:11:04.260 --> 00:11:06.530 align:start position:0% asset which should just uh it's just the current<00:11:04.380> exchange<00:11:04.860> rate<00:11:05.040> and<00:11:05.880> it<00:11:06.120> has<00:11:06.300> another 00:11:06.530 --> 00:11:06.540 align:start position:0% current exchange rate and it has another 00:11:06.540 --> 00:11:09.350 align:start position:0% current exchange rate and it has another very<00:11:06.899> in<00:11:07.320> another<00:11:07.620> parameter<00:11:08.160> assets<00:11:08.579> and 00:11:09.350 --> 00:11:09.360 align:start position:0% very in another parameter assets and 00:11:09.360 --> 00:11:11.509 align:start position:0% very in another parameter assets and when<00:11:09.480> this<00:11:09.720> test<00:11:09.899> is<00:11:10.140> run 00:11:11.509 --> 00:11:11.519 align:start position:0% when this test is run 00:11:11.519 --> 00:11:15.230 align:start position:0% when this test is run um<00:11:11.660> uh<00:11:12.660> Foundry<00:11:13.519> by<00:11:14.519> the<00:11:14.760> way<00:11:14.820> that's<00:11:15.060> a 00:11:15.230 --> 00:11:15.240 align:start position:0% um uh Foundry by the way that's a 00:11:15.240 --> 00:11:17.090 align:start position:0% um uh Foundry by the way that's a Foundry<00:11:15.540> test<00:11:15.720> I<00:11:15.959> don't<00:11:16.019> know<00:11:16.140> if<00:11:16.200> I<00:11:16.440> have<00:11:16.620> said 00:11:17.090 --> 00:11:17.100 align:start position:0% Foundry test I don't know if I have said 00:11:17.100 --> 00:11:18.350 align:start position:0% Foundry test I don't know if I have said that 00:11:18.350 --> 00:11:18.360 align:start position:0% that 00:11:18.360 --> 00:11:21.230 align:start position:0% that um 00:11:21.230 --> 00:11:21.240 align:start position:0% 00:11:21.240 --> 00:11:24.110 align:start position:0% so<00:11:21.660> and<00:11:21.839> when<00:11:22.019> Foundry<00:11:22.440> wants<00:11:22.860> this<00:11:23.040> test<00:11:23.220> it 00:11:24.110 --> 00:11:24.120 align:start position:0% so and when Foundry wants this test it 00:11:24.120 --> 00:11:27.769 align:start position:0% so and when Foundry wants this test it will<00:11:24.420> like<00:11:24.959> insert<00:11:25.800> call<00:11:26.100> this<00:11:26.339> test<00:11:26.579> with<00:11:26.880> a 00:11:27.769 --> 00:11:27.779 align:start position:0% will like insert call this test with a 00:11:27.779 --> 00:11:30.290 align:start position:0% will like insert call this test with a bunch<00:11:28.200> of<00:11:28.440> random<00:11:28.860> inputs 00:11:30.290 --> 00:11:30.300 align:start position:0% bunch of random inputs 00:11:30.300 --> 00:11:33.949 align:start position:0% bunch of random inputs um<00:11:30.360> like<00:11:30.959> uh<00:11:32.399> and<00:11:32.820> that's<00:11:32.940> the<00:11:33.180> benefit<00:11:33.360> of<00:11:33.839> a 00:11:33.949 --> 00:11:33.959 align:start position:0% um like uh and that's the benefit of a 00:11:33.959 --> 00:11:36.230 align:start position:0% um like uh and that's the benefit of a unit<00:11:34.200> test<00:11:34.500> when<00:11:34.740> you<00:11:34.860> have<00:11:34.980> a<00:11:35.100> unit<00:11:35.220> test<00:11:35.519> and 00:11:36.230 --> 00:11:36.240 align:start position:0% unit test when you have a unit test and 00:11:36.240 --> 00:11:38.150 align:start position:0% unit test when you have a unit test and you<00:11:36.600> want<00:11:36.779> to<00:11:36.899> detect<00:11:37.140> such<00:11:37.320> routing<00:11:37.860> error 00:11:38.150 --> 00:11:38.160 align:start position:0% you want to detect such routing error 00:11:38.160 --> 00:11:40.850 align:start position:0% you want to detect such routing error you<00:11:38.700> basically<00:11:39.000> need<00:11:39.540> to<00:11:39.660> be<00:11:39.779> lucky<00:11:40.079> and<00:11:40.560> like 00:11:40.850 --> 00:11:40.860 align:start position:0% you basically need to be lucky and like 00:11:40.860 --> 00:11:42.590 align:start position:0% you basically need to be lucky and like put<00:11:41.100> the<00:11:41.339> right<00:11:41.459> numbers<00:11:41.700> into<00:11:42.000> the<00:11:42.180> unit<00:11:42.300> test 00:11:42.590 --> 00:11:42.600 align:start position:0% put the right numbers into the unit test 00:11:42.600 --> 00:11:45.110 align:start position:0% put the right numbers into the unit test and<00:11:42.839> guess<00:11:43.019> the<00:11:43.260> counter<00:11:43.620> example<00:11:44.100> like<00:11:44.760> with 00:11:45.110 --> 00:11:45.120 align:start position:0% and guess the counter example like with 00:11:45.120 --> 00:11:47.150 align:start position:0% and guess the counter example like with this<00:11:45.480> Foundry<00:11:45.839> test<00:11:46.079> Foundry<00:11:46.740> does<00:11:46.920> a 00:11:47.150 --> 00:11:47.160 align:start position:0% this Foundry test Foundry does a 00:11:47.160 --> 00:11:49.370 align:start position:0% this Foundry test Foundry does a guessing<00:11:47.459> for<00:11:47.640> you<00:11:47.760> and<00:11:47.940> can<00:11:48.360> it<00:11:48.540> do<00:11:49.140> much 00:11:49.370 --> 00:11:49.380 align:start position:0% guessing for you and can it do much 00:11:49.380 --> 00:11:51.829 align:start position:0% guessing for you and can it do much quicker<00:11:49.800> than<00:11:49.980> you<00:11:50.160> ever<00:11:50.459> could<00:11:50.700> like<00:11:51.300> it<00:11:51.600> can 00:11:51.829 --> 00:11:51.839 align:start position:0% quicker than you ever could like it can 00:11:51.839 --> 00:11:54.530 align:start position:0% quicker than you ever could like it can one<00:11:52.380> like<00:11:52.620> 1000<00:11:53.339> samples<00:11:53.700> or<00:11:54.000> two<00:11:54.240> thousand 00:11:54.530 --> 00:11:54.540 align:start position:0% one like 1000 samples or two thousand 00:11:54.540 --> 00:11:56.509 align:start position:0% one like 1000 samples or two thousand two<00:11:54.839> thousand<00:11:55.200> samples<00:11:55.620> in<00:11:56.100> a<00:11:56.279> couple<00:11:56.399> of 00:11:56.509 --> 00:11:56.519 align:start position:0% two thousand samples in a couple of 00:11:56.519 --> 00:11:58.310 align:start position:0% two thousand samples in a couple of milliseconds 00:11:58.310 --> 00:11:58.320 align:start position:0% milliseconds 00:11:58.320 --> 00:12:01.610 align:start position:0% milliseconds um<00:11:58.920> so<00:11:59.519> and<00:11:59.700> I<00:12:00.060> want<00:12:00.300> now<00:12:00.660> to<00:12:01.019> have<00:12:01.200> you<00:12:01.320> a<00:12:01.500> look 00:12:01.610 --> 00:12:01.620 align:start position:0% um so and I want now to have you a look 00:12:01.620 --> 00:12:06.470 align:start position:0% um so and I want now to have you a look at<00:12:01.980> line<00:12:02.160> 14<00:12:02.760> and<00:12:03.600> 15<00:12:04.040> and<00:12:05.040> see<00:12:05.880> that<00:12:06.240> it 00:12:06.470 --> 00:12:06.480 align:start position:0% at line 14 and 15 and see that it 00:12:06.480 --> 00:12:09.590 align:start position:0% at line 14 and 15 and see that it resembles<00:12:07.200> the<00:12:07.560> property<00:12:08.040> that<00:12:09.000> we<00:12:09.180> specified 00:12:09.590 --> 00:12:09.600 align:start position:0% resembles the property that we specified 00:12:09.600 --> 00:12:11.690 align:start position:0% resembles the property that we specified above<00:12:10.200> so<00:12:10.500> I<00:12:10.680> hope<00:12:10.860> that<00:12:11.040> you<00:12:11.160> can<00:12:11.279> see<00:12:11.399> in<00:12:11.519> line 00:12:11.690 --> 00:12:11.700 align:start position:0% above so I hope that you can see in line 00:12:11.700 --> 00:12:14.630 align:start position:0% above so I hope that you can see in line 14<00:12:11.940> that<00:12:12.660> we<00:12:12.839> are<00:12:13.019> like<00:12:13.200> executing<00:12:13.920> a<00:12:14.160> deposit 00:12:14.630 --> 00:12:14.640 align:start position:0% 14 that we are like executing a deposit 00:12:14.640 --> 00:12:17.269 align:start position:0% 14 that we are like executing a deposit function<00:12:14.940> and<00:12:15.660> in<00:12:15.839> the<00:12:15.959> same<00:12:16.079> transaction<00:12:16.620> we 00:12:17.269 --> 00:12:17.279 align:start position:0% function and in the same transaction we 00:12:17.279 --> 00:12:19.910 align:start position:0% function and in the same transaction we are<00:12:17.459> executing<00:12:18.120> the<00:12:18.240> redeem<00:12:18.720> function<00:12:19.079> and 00:12:19.910 --> 00:12:19.920 align:start position:0% are executing the redeem function and 00:12:19.920 --> 00:12:21.530 align:start position:0% are executing the redeem function and like<00:12:20.160> that<00:12:20.339> is<00:12:20.519> exactly<00:12:20.820> what<00:12:21.000> the<00:12:21.240> property 00:12:21.530 --> 00:12:21.540 align:start position:0% like that is exactly what the property 00:12:21.540 --> 00:12:24.829 align:start position:0% like that is exactly what the property is<00:12:21.660> above<00:12:21.980> uh<00:12:22.980> what<00:12:23.100> the<00:12:23.279> property<00:12:23.519> above<00:12:23.820> says 00:12:24.829 --> 00:12:24.839 align:start position:0% is above uh what the property above says 00:12:24.839 --> 00:12:26.690 align:start position:0% is above uh what the property above says so<00:12:25.380> and<00:12:25.560> then<00:12:25.740> then<00:12:25.980> there's<00:12:26.399> some 00:12:26.690 --> 00:12:26.700 align:start position:0% so and then then there's some 00:12:26.700 --> 00:12:28.790 align:start position:0% so and then then there's some boilerplate<00:12:27.360> code<00:12:27.480> to<00:12:27.720> to<00:12:27.959> that<00:12:28.200> test<00:12:28.380> as<00:12:28.620> well 00:12:28.790 --> 00:12:28.800 align:start position:0% boilerplate code to to that test as well 00:12:28.800 --> 00:12:32.210 align:start position:0% boilerplate code to to that test as well uh<00:12:29.640> that's<00:12:29.820> like<00:12:30.240> it's<00:12:30.480> not<00:12:31.019> like<00:12:31.380> mandatory 00:12:32.210 --> 00:12:32.220 align:start position:0% uh that's like it's not like mandatory 00:12:32.220 --> 00:12:34.190 align:start position:0% uh that's like it's not like mandatory to<00:12:32.399> understand<00:12:32.579> but<00:12:33.300> like<00:12:33.600> if<00:12:33.720> you<00:12:33.839> look<00:12:33.959> at 00:12:34.190 --> 00:12:34.200 align:start position:0% to understand but like if you look at 00:12:34.200 --> 00:12:37.130 align:start position:0% to understand but like if you look at lines<00:12:34.620> two<00:12:35.160> to<00:12:35.399> line<00:12:35.579> sevens<00:12:36.240> uh<00:12:36.779> to<00:12:36.899> line 00:12:37.130 --> 00:12:37.140 align:start position:0% lines two to line sevens uh to line 00:12:37.140 --> 00:12:39.350 align:start position:0% lines two to line sevens uh to line seven<00:12:37.380> these<00:12:38.279> are<00:12:38.399> just<00:12:38.579> some<00:12:38.880> assumptions 00:12:39.350 --> 00:12:39.360 align:start position:0% seven these are just some assumptions 00:12:39.360 --> 00:12:43.370 align:start position:0% seven these are just some assumptions that<00:12:39.600> I<00:12:39.720> make<00:12:39.899> over<00:12:40.260> the<00:12:40.620> inputs<00:12:41.660> and<00:12:42.660> I<00:12:43.079> put 00:12:43.370 --> 00:12:43.380 align:start position:0% that I make over the inputs and I put 00:12:43.380 --> 00:12:45.290 align:start position:0% that I make over the inputs and I put these<00:12:43.620> assumptions<00:12:44.040> there<00:12:44.459> just<00:12:44.760> to<00:12:45.000> avoid 00:12:45.290 --> 00:12:45.300 align:start position:0% these assumptions there just to avoid 00:12:45.300 --> 00:12:47.090 align:start position:0% these assumptions there just to avoid arithmetic<00:12:46.019> overflow<00:12:46.440> and<00:12:46.560> arithmetic 00:12:47.090 --> 00:12:47.100 align:start position:0% arithmetic overflow and arithmetic 00:12:47.100 --> 00:12:49.370 align:start position:0% arithmetic overflow and arithmetic underflow<00:12:47.700> because<00:12:48.120> if<00:12:48.420> I<00:12:48.660> went<00:12:48.779> into<00:12:49.019> such<00:12:49.260> a 00:12:49.370 --> 00:12:49.380 align:start position:0% underflow because if I went into such a 00:12:49.380 --> 00:12:51.230 align:start position:0% underflow because if I went into such a situation<00:12:49.740> my<00:12:50.040> test<00:12:50.220> would<00:12:50.519> simply<00:12:50.760> revert 00:12:51.230 --> 00:12:51.240 align:start position:0% situation my test would simply revert 00:12:51.240 --> 00:12:54.290 align:start position:0% situation my test would simply revert and<00:12:51.720> I<00:12:51.839> I<00:12:52.079> only<00:12:52.380> want<00:12:52.620> to<00:12:52.740> execute<00:12:53.160> like<00:12:53.399> uh<00:12:54.060> the 00:12:54.290 --> 00:12:54.300 align:start position:0% and I I only want to execute like uh the 00:12:54.300 --> 00:12:56.930 align:start position:0% and I I only want to execute like uh the happy<00:12:54.420> path<00:12:54.779> with<00:12:55.320> this<00:12:55.500> test 00:12:56.930 --> 00:12:56.940 align:start position:0% happy path with this test 00:12:56.940 --> 00:12:59.389 align:start position:0% happy path with this test um and<00:12:57.240> then<00:12:57.360> like<00:12:57.839> line<00:12:58.139> eight<00:12:58.500> to<00:12:58.860> line<00:12:59.100> 12 00:12:59.389 --> 00:12:59.399 align:start position:0% um and then like line eight to line 12 00:12:59.399 --> 00:13:01.790 align:start position:0% um and then like line eight to line 12 is<00:12:59.760> just<00:12:59.940> a<00:13:00.120> basic<00:13:00.420> test<00:13:00.600> setup<00:13:01.019> so<00:13:01.320> that<00:13:01.560> I 00:13:01.790 --> 00:13:01.800 align:start position:0% is just a basic test setup so that I 00:13:01.800 --> 00:13:04.009 align:start position:0% is just a basic test setup so that I that<00:13:02.160> my<00:13:02.339> contract<00:13:02.579> is<00:13:02.760> in<00:13:02.940> the<00:13:03.120> state<00:13:03.240> that<00:13:03.779> it 00:13:04.009 --> 00:13:04.019 align:start position:0% that my contract is in the state that it 00:13:04.019 --> 00:13:05.690 align:start position:0% that my contract is in the state that it can<00:13:04.200> actually<00:13:04.380> fulfill<00:13:05.100> the<00:13:05.279> transfer 00:13:05.690 --> 00:13:05.700 align:start position:0% can actually fulfill the transfer 00:13:05.700 --> 00:13:09.769 align:start position:0% can actually fulfill the transfer functions<00:13:06.180> that<00:13:06.839> I'm<00:13:07.019> calling<00:13:07.380> in<00:13:07.500> line<00:13:07.620> 14. 00:13:09.769 --> 00:13:09.779 align:start position:0% functions that I'm calling in line 14. 00:13:09.779 --> 00:13:11.449 align:start position:0% functions that I'm calling in line 14. so 00:13:11.449 --> 00:13:11.459 align:start position:0% so 00:13:11.459 --> 00:13:14.210 align:start position:0% so um 00:13:14.210 --> 00:13:14.220 align:start position:0% 00:13:14.220 --> 00:13:16.610 align:start position:0% fuzzing<00:13:15.120> is<00:13:15.360> good<00:13:15.540> and<00:13:15.899> you<00:13:16.079> should<00:13:16.380> actually 00:13:16.610 --> 00:13:16.620 align:start position:0% fuzzing is good and you should actually 00:13:16.620 --> 00:13:18.769 align:start position:0% fuzzing is good and you should actually you<00:13:17.279> should<00:13:17.399> do<00:13:17.700> it<00:13:17.880> when<00:13:18.120> you<00:13:18.300> test<00:13:18.480> for 00:13:18.769 --> 00:13:18.779 align:start position:0% you should do it when you test for 00:13:18.779 --> 00:13:21.710 align:start position:0% you should do it when you test for rounding<00:13:19.260> errors<00:13:19.560> but<00:13:19.920> like<00:13:20.639> fuzzing<00:13:21.300> is<00:13:21.540> not 00:13:21.710 --> 00:13:21.720 align:start position:0% rounding errors but like fuzzing is not 00:13:21.720 --> 00:13:24.710 align:start position:0% rounding errors but like fuzzing is not enough<00:13:22.019> that's<00:13:22.620> the<00:13:23.040> uh<00:13:23.880> the<00:13:24.300> sad<00:13:24.480> message 00:13:24.710 --> 00:13:24.720 align:start position:0% enough that's the uh the sad message 00:13:24.720 --> 00:13:27.710 align:start position:0% enough that's the uh the sad message here<00:13:25.019> like<00:13:25.740> the<00:13:26.040> third<00:13:26.220> example<00:13:26.639> from<00:13:27.060> the<00:13:27.600> um 00:13:27.710 --> 00:13:27.720 align:start position:0% here like the third example from the um 00:13:27.720 --> 00:13:30.829 align:start position:0% here like the third example from the um from<00:13:28.079> the<00:13:28.380> first<00:13:28.860> slide<00:13:29.220> that<00:13:29.459> I<00:13:29.579> showed<00:13:29.880> you 00:13:30.829 --> 00:13:30.839 align:start position:0% from the first slide that I showed you 00:13:30.839 --> 00:13:32.329 align:start position:0% from the first slide that I showed you um 00:13:32.329 --> 00:13:32.339 align:start position:0% um 00:13:32.339 --> 00:13:35.269 align:start position:0% um this<00:13:33.240> example<00:13:33.899> it<00:13:34.500> was 00:13:35.269 --> 00:13:35.279 align:start position:0% this example it was 00:13:35.279 --> 00:13:41.389 align:start position:0% this example it was um<00:13:35.339> the<00:13:36.180> uh<00:13:36.980> Stables<00:13:37.980> stable<00:13:38.899> swap<00:13:39.899> contract 00:13:41.389 --> 00:13:41.399 align:start position:0% um the uh Stables stable swap contract 00:13:41.399 --> 00:13:42.230 align:start position:0% um the uh Stables stable swap contract um 00:13:42.230 --> 00:13:42.240 align:start position:0% um 00:13:42.240 --> 00:13:44.990 align:start position:0% um uh<00:13:43.019> suffered<00:13:43.560> from<00:13:44.040> this<00:13:44.339> rounding<00:13:44.760> Direction 00:13:44.990 --> 00:13:45.000 align:start position:0% uh suffered from this rounding Direction 00:13:45.000 --> 00:13:48.710 align:start position:0% uh suffered from this rounding Direction vinyl<00:13:45.720> ability<00:13:46.339> although<00:13:47.339> it<00:13:48.060> was<00:13:48.240> heavily 00:13:48.710 --> 00:13:48.720 align:start position:0% vinyl ability although it was heavily 00:13:48.720 --> 00:13:51.410 align:start position:0% vinyl ability although it was heavily fast<00:13:48.959> and<00:13:49.800> like<00:13:50.100> this<00:13:50.399> excerpt<00:13:50.820> that<00:13:51.180> you<00:13:51.300> see 00:13:51.410 --> 00:13:51.420 align:start position:0% fast and like this excerpt that you see 00:13:51.420 --> 00:13:55.069 align:start position:0% fast and like this excerpt that you see here<00:13:51.720> is<00:13:52.500> like<00:13:52.740> from<00:13:52.980> the<00:13:53.160> blog<00:13:53.459> post<00:13:53.720> uh<00:13:54.720> that 00:13:55.069 --> 00:13:55.079 align:start position:0% here is like from the blog post uh that 00:13:55.079 --> 00:13:57.889 align:start position:0% here is like from the blog post uh that explains<00:13:55.980> this<00:13:56.160> vinyl<00:13:56.519> ability<00:13:56.880> and<00:13:57.240> just<00:13:57.540> let 00:13:57.889 --> 00:13:57.899 align:start position:0% explains this vinyl ability and just let 00:13:57.899 --> 00:14:00.889 align:start position:0% explains this vinyl ability and just let it<00:13:58.079> read<00:13:58.260> me<00:13:58.500> let<00:13:59.100> it<00:13:59.279> uh<00:14:00.120> let<00:14:00.360> me<00:14:00.480> read<00:14:00.600> it<00:14:00.779> out 00:14:00.889 --> 00:14:00.899 align:start position:0% it read me let it uh let me read it out 00:14:00.899 --> 00:14:03.410 align:start position:0% it read me let it uh let me read it out to<00:14:01.079> you<00:14:01.320> so<00:14:01.680> another<00:14:02.279> interesting<00:14:02.940> takeaway 00:14:03.410 --> 00:14:03.420 align:start position:0% to you so another interesting takeaway 00:14:03.420 --> 00:14:05.269 align:start position:0% to you so another interesting takeaway is<00:14:03.779> that<00:14:03.899> fuzzing<00:14:04.380> can<00:14:04.500> give<00:14:04.680> you<00:14:04.800> a<00:14:04.980> false 00:14:05.269 --> 00:14:05.279 align:start position:0% is that fuzzing can give you a false 00:14:05.279 --> 00:14:07.610 align:start position:0% is that fuzzing can give you a false sense<00:14:05.459> of<00:14:05.639> security<00:14:06.019> prior<00:14:07.019> to<00:14:07.200> our<00:14:07.380> report 00:14:07.610 --> 00:14:07.620 align:start position:0% sense of security prior to our report 00:14:07.620 --> 00:14:09.769 align:start position:0% sense of security prior to our report saber<00:14:08.279> had<00:14:08.459> already<00:14:08.639> deployed<00:14:09.120> comprehensive 00:14:09.769 --> 00:14:09.779 align:start position:0% saber had already deployed comprehensive 00:14:09.779 --> 00:14:12.290 align:start position:0% saber had already deployed comprehensive fuzzles<00:14:10.260> for<00:14:10.800> their<00:14:11.040> state<00:14:11.279> for<00:14:11.700> their<00:14:11.940> swept 00:14:12.290 --> 00:14:12.300 align:start position:0% fuzzles for their state for their swept 00:14:12.300 --> 00:14:14.329 align:start position:0% fuzzles for their state for their swept implementation<00:14:12.720> a<00:14:13.380> researcher<00:14:13.860> looking<00:14:14.100> at 00:14:14.329 --> 00:14:14.339 align:start position:0% implementation a researcher looking at 00:14:14.339 --> 00:14:16.370 align:start position:0% implementation a researcher looking at the<00:14:14.519> code<00:14:14.639> coverage<00:14:15.060> alone<00:14:15.360> might<00:14:15.959> come<00:14:16.200> to 00:14:16.370 --> 00:14:16.380 align:start position:0% the code coverage alone might come to 00:14:16.380 --> 00:14:17.810 align:start position:0% the code coverage alone might come to the<00:14:16.500> incorrect<00:14:16.860> conclusion<00:14:17.279> that<00:14:17.579> such 00:14:17.810 --> 00:14:17.820 align:start position:0% the incorrect conclusion that such 00:14:17.820 --> 00:14:20.150 align:start position:0% the incorrect conclusion that such extensively<00:14:18.360> fast<00:14:18.660> code<00:14:18.959> couldn't<00:14:19.620> possibly 00:14:20.150 --> 00:14:20.160 align:start position:0% extensively fast code couldn't possibly 00:14:20.160 --> 00:14:22.009 align:start position:0% extensively fast code couldn't possibly have<00:14:20.399> a<00:14:20.579> vulnerability 00:14:22.009 --> 00:14:22.019 align:start position:0% have a vulnerability 00:14:22.019 --> 00:14:24.350 align:start position:0% have a vulnerability all<00:14:22.560> right<00:14:22.800> so<00:14:22.980> what<00:14:23.339> else<00:14:23.459> can<00:14:23.700> we<00:14:23.880> do<00:14:24.000> to 00:14:24.350 --> 00:14:24.360 align:start position:0% all right so what else can we do to 00:14:24.360 --> 00:14:26.150 align:start position:0% all right so what else can we do to increase<00:14:24.480> our<00:14:24.899> confidence<00:14:25.260> in<00:14:25.740> in<00:14:25.920> our 00:14:26.150 --> 00:14:26.160 align:start position:0% increase our confidence in in our 00:14:26.160 --> 00:14:29.269 align:start position:0% increase our confidence in in our implementation<00:14:26.720> and<00:14:27.720> like<00:14:28.139> one<00:14:28.860> possible 00:14:29.269 --> 00:14:29.279 align:start position:0% implementation and like one possible 00:14:29.279 --> 00:14:32.030 align:start position:0% implementation and like one possible solution<00:14:29.700> is<00:14:30.120> that<00:14:30.480> we<00:14:30.720> could<00:14:30.899> use<00:14:31.260> like<00:14:31.800> that 00:14:32.030 --> 00:14:32.040 align:start position:0% solution is that we could use like that 00:14:32.040 --> 00:14:34.670 align:start position:0% solution is that we could use like that we<00:14:32.279> could<00:14:32.339> use<00:14:32.519> symbolic<00:14:33.060> execution<00:14:33.660> on<00:14:34.500> top 00:14:34.670 --> 00:14:34.680 align:start position:0% we could use symbolic execution on top 00:14:34.680 --> 00:14:37.250 align:start position:0% we could use symbolic execution on top of<00:14:34.860> fuzzing<00:14:35.339> so<00:14:35.639> if<00:14:36.120> you<00:14:36.240> see<00:14:36.420> that<00:14:36.660> table<00:14:36.899> on 00:14:37.250 --> 00:14:37.260 align:start position:0% of fuzzing so if you see that table on 00:14:37.260 --> 00:14:39.530 align:start position:0% of fuzzing so if you see that table on the<00:14:37.380> left<00:14:37.560> hand<00:14:37.740> side<00:14:37.980> there<00:14:38.639> are<00:14:38.880> some<00:14:39.060> like 00:14:39.530 --> 00:14:39.540 align:start position:0% the left hand side there are some like 00:14:39.540 --> 00:14:43.730 align:start position:0% the left hand side there are some like some<00:14:40.500> properties<00:14:41.120> uh<00:14:42.120> uh<00:14:42.899> that<00:14:43.079> that<00:14:43.139> fuzzing 00:14:43.730 --> 00:14:43.740 align:start position:0% some properties uh uh that that fuzzing 00:14:43.740 --> 00:14:45.410 align:start position:0% some properties uh uh that that fuzzing has<00:14:43.920> and<00:14:44.100> on<00:14:44.279> the<00:14:44.399> right<00:14:44.519> hand<00:14:44.699> side<00:14:44.880> on<00:14:45.300> the 00:14:45.410 --> 00:14:45.420 align:start position:0% has and on the right hand side on the 00:14:45.420 --> 00:14:47.269 align:start position:0% has and on the right hand side on the white<00:14:45.540> column<00:14:45.899> you<00:14:46.019> see<00:14:46.199> some<00:14:46.380> properties<00:14:46.800> of 00:14:47.269 --> 00:14:47.279 align:start position:0% white column you see some properties of 00:14:47.279 --> 00:14:50.150 align:start position:0% white column you see some properties of symbolic<00:14:48.060> execution<00:14:48.600> but<00:14:49.380> I<00:14:49.740> don't<00:14:49.860> want<00:14:50.040> to 00:14:50.150 --> 00:14:50.160 align:start position:0% symbolic execution but I don't want to 00:14:50.160 --> 00:14:52.850 align:start position:0% symbolic execution but I don't want to want<00:14:50.699> you<00:14:50.820> to<00:14:51.000> think<00:14:51.240> about<00:14:51.420> like<00:14:51.959> this<00:14:52.560> slide 00:14:52.850 --> 00:14:52.860 align:start position:0% want you to think about like this slide 00:14:52.860 --> 00:14:56.210 align:start position:0% want you to think about like this slide as<00:14:53.220> fuzzing<00:14:53.940> versus<00:14:54.740> symbolic<00:14:55.740> execution 00:14:56.210 --> 00:14:56.220 align:start position:0% as fuzzing versus symbolic execution 00:14:56.220 --> 00:14:59.930 align:start position:0% as fuzzing versus symbolic execution it's<00:14:57.180> like<00:14:57.660> you<00:14:58.440> can<00:14:58.860> get<00:14:59.040> the<00:14:59.279> best<00:14:59.459> of<00:14:59.699> both 00:14:59.930 --> 00:14:59.940 align:start position:0% it's like you can get the best of both 00:14:59.940 --> 00:15:02.090 align:start position:0% it's like you can get the best of both worlds<00:15:00.420> if<00:15:00.839> you<00:15:01.019> combine<00:15:01.380> both<00:15:01.680> of<00:15:01.860> these 00:15:02.090 --> 00:15:02.100 align:start position:0% worlds if you combine both of these 00:15:02.100 --> 00:15:05.269 align:start position:0% worlds if you combine both of these efforts<00:15:02.579> and<00:15:03.420> we<00:15:03.839> recently 00:15:05.269 --> 00:15:05.279 align:start position:0% efforts and we recently 00:15:05.279 --> 00:15:07.850 align:start position:0% efforts and we recently um<00:15:05.339> so<00:15:05.699> we<00:15:05.940> at<00:15:06.300> one<00:15:06.480> time<00:15:06.660> verification<00:15:07.199> we 00:15:07.850 --> 00:15:07.860 align:start position:0% um so we at one time verification we 00:15:07.860 --> 00:15:10.250 align:start position:0% um so we at one time verification we have<00:15:08.040> a<00:15:08.279> symbolic<00:15:08.760> execution<00:15:09.180> engine<00:15:09.540> that's 00:15:10.250 --> 00:15:10.260 align:start position:0% have a symbolic execution engine that's 00:15:10.260 --> 00:15:12.769 align:start position:0% have a symbolic execution engine that's called<00:15:10.560> KVM<00:15:11.279> that's<00:15:12.000> it's<00:15:12.180> a<00:15:12.360> symbolic 00:15:12.769 --> 00:15:12.779 align:start position:0% called KVM that's it's a symbolic 00:15:12.779 --> 00:15:15.350 align:start position:0% called KVM that's it's a symbolic execution<00:15:13.139> engine<00:15:13.380> tailored<00:15:13.920> to<00:15:14.040> the<00:15:14.760> um<00:15:14.820> to 00:15:15.350 --> 00:15:15.360 align:start position:0% execution engine tailored to the um to 00:15:15.360 --> 00:15:18.110 align:start position:0% execution engine tailored to the um to to<00:15:15.480> the<00:15:15.720> ethereum<00:15:16.199> virtual<00:15:16.560> machine<00:15:16.880> and<00:15:17.880> we 00:15:18.110 --> 00:15:18.120 align:start position:0% to the ethereum virtual machine and we 00:15:18.120 --> 00:15:20.150 align:start position:0% to the ethereum virtual machine and we recently<00:15:18.600> added<00:15:18.959> a<00:15:19.079> feature<00:15:19.440> to<00:15:19.620> that<00:15:19.800> that 00:15:20.150 --> 00:15:20.160 align:start position:0% recently added a feature to that that 00:15:20.160 --> 00:15:23.930 align:start position:0% recently added a feature to that that allows<00:15:20.639> you<00:15:20.820> to<00:15:21.959> put<00:15:22.620> Foundry<00:15:23.160> tests<00:15:23.519> into<00:15:23.639> it 00:15:23.930 --> 00:15:23.940 align:start position:0% allows you to put Foundry tests into it 00:15:23.940 --> 00:15:26.389 align:start position:0% allows you to put Foundry tests into it and<00:15:24.779> instead<00:15:25.139> of<00:15:25.380> fuzzing<00:15:26.040> over<00:15:26.160> the 00:15:26.389 --> 00:15:26.399 align:start position:0% and instead of fuzzing over the 00:15:26.399 --> 00:15:28.970 align:start position:0% and instead of fuzzing over the parameters<00:15:26.940> so<00:15:27.120> instead<00:15:27.420> of<00:15:27.540> choosing<00:15:28.199> random 00:15:28.970 --> 00:15:28.980 align:start position:0% parameters so instead of choosing random 00:15:28.980 --> 00:15:31.850 align:start position:0% parameters so instead of choosing random input<00:15:29.399> variables<00:15:30.000> for<00:15:30.180> the<00:15:30.360> parameters<00:15:30.959> and 00:15:31.850 --> 00:15:31.860 align:start position:0% input variables for the parameters and 00:15:31.860 --> 00:15:34.610 align:start position:0% input variables for the parameters and we<00:15:32.220> do<00:15:32.399> symbolic<00:15:32.940> execution<00:15:33.420> over<00:15:33.779> the<00:15:34.199> uh 00:15:34.610 --> 00:15:34.620 align:start position:0% we do symbolic execution over the uh 00:15:34.620 --> 00:15:37.129 align:start position:0% we do symbolic execution over the uh over<00:15:34.980> the<00:15:35.220> parameters<00:15:35.820> and<00:15:36.360> that<00:15:36.480> has<00:15:36.720> like 00:15:37.129 --> 00:15:37.139 align:start position:0% over the parameters and that has like 00:15:37.139 --> 00:15:40.189 align:start position:0% over the parameters and that has like different<00:15:37.680> trade-offs<00:15:38.579> so 00:15:40.189 --> 00:15:40.199 align:start position:0% different trade-offs so 00:15:40.199 --> 00:15:43.670 align:start position:0% different trade-offs so um<00:15:40.260> the<00:15:41.160> nice<00:15:41.279> thing<00:15:41.579> is<00:15:41.820> that<00:15:42.360> well<00:15:42.720> for 00:15:43.670 --> 00:15:43.680 align:start position:0% um the nice thing is that well for 00:15:43.680 --> 00:15:45.949 align:start position:0% um the nice thing is that well for Foundry<00:15:44.100> and<00:15:44.399> for<00:15:44.639> symbolic<00:15:45.360> execution<00:15:45.779> with 00:15:45.949 --> 00:15:45.959 align:start position:0% Foundry and for symbolic execution with 00:15:45.959 --> 00:15:48.650 align:start position:0% Foundry and for symbolic execution with the<00:15:46.139> evm<00:15:46.860> you<00:15:47.279> get<00:15:47.459> to<00:15:47.639> specify<00:15:48.120> your<00:15:48.360> tests 00:15:48.650 --> 00:15:48.660 align:start position:0% the evm you get to specify your tests 00:15:48.660 --> 00:15:50.810 align:start position:0% the evm you get to specify your tests and<00:15:48.899> your<00:15:49.079> specifications<00:15:49.620> in<00:15:50.399> Foundry 00:15:50.810 --> 00:15:50.820 align:start position:0% and your specifications in Foundry 00:15:50.820 --> 00:15:54.230 align:start position:0% and your specifications in Foundry itself<00:15:51.440> in<00:15:52.440> solidity<00:15:52.920> itself<00:15:53.279> sorry 00:15:54.230 --> 00:15:54.240 align:start position:0% itself in solidity itself sorry 00:15:54.240 --> 00:15:57.230 align:start position:0% itself in solidity itself sorry uh<00:15:54.839> so<00:15:55.079> that's<00:15:55.320> that's<00:15:55.560> like<00:15:55.860> easier<00:15:56.339> than<00:15:57.120> um 00:15:57.230 --> 00:15:57.240 align:start position:0% uh so that's that's like easier than um 00:15:57.240 --> 00:16:00.710 align:start position:0% uh so that's that's like easier than um than<00:15:57.779> having<00:15:58.079> to<00:15:58.620> uh<00:15:59.339> to<00:15:59.820> to<00:15:59.820> write<00:16:00.240> your<00:16:00.420> tests 00:16:00.710 --> 00:16:00.720 align:start position:0% than having to uh to to write your tests 00:16:00.720 --> 00:16:02.810 align:start position:0% than having to uh to to write your tests in<00:16:00.839> JavaScript<00:16:01.199> or<00:16:01.440> typescript<00:16:01.860> developers 00:16:02.810 --> 00:16:02.820 align:start position:0% in JavaScript or typescript developers 00:16:02.820 --> 00:16:04.970 align:start position:0% in JavaScript or typescript developers like<00:16:03.120> Foundry<00:16:03.720> especially<00:16:04.139> because<00:16:04.500> of<00:16:04.800> this 00:16:04.970 --> 00:16:04.980 align:start position:0% like Foundry especially because of this 00:16:04.980 --> 00:16:06.530 align:start position:0% like Foundry especially because of this property 00:16:06.530 --> 00:16:06.540 align:start position:0% property 00:16:06.540 --> 00:16:07.129 align:start position:0% property um 00:16:07.129 --> 00:16:07.139 align:start position:0% um 00:16:07.139 --> 00:16:09.410 align:start position:0% um so<00:16:07.620> but<00:16:07.800> that<00:16:07.980> also<00:16:08.399> means 00:16:09.410 --> 00:16:09.420 align:start position:0% so but that also means 00:16:09.420 --> 00:16:11.329 align:start position:0% so but that also means like<00:16:09.779> when<00:16:09.899> it<00:16:10.079> comes<00:16:10.199> to<00:16:10.380> Foundry<00:16:10.860> that<00:16:11.100> you 00:16:11.329 --> 00:16:11.339 align:start position:0% like when it comes to Foundry that you 00:16:11.339 --> 00:16:12.710 align:start position:0% like when it comes to Foundry that you are<00:16:11.459> somewhat<00:16:11.820> limited<00:16:12.240> to<00:16:12.420> the 00:16:12.710 --> 00:16:12.720 align:start position:0% are somewhat limited to the 00:16:12.720 --> 00:16:15.230 align:start position:0% are somewhat limited to the expressiveness<00:16:13.380> of<00:16:13.680> solidity<00:16:14.160> and<00:16:14.880> there<00:16:15.060> are 00:16:15.230 --> 00:16:15.240 align:start position:0% expressiveness of solidity and there are 00:16:15.240 --> 00:16:17.090 align:start position:0% expressiveness of solidity and there are a<00:16:15.480> bunch<00:16:15.660> of<00:16:15.839> like 00:16:17.090 --> 00:16:17.100 align:start position:0% a bunch of like 00:16:17.100 --> 00:16:19.370 align:start position:0% a bunch of like um<00:16:17.160> safety<00:16:17.639> properties<00:16:18.120> that<00:16:18.899> you<00:16:19.139> simply 00:16:19.370 --> 00:16:19.380 align:start position:0% um safety properties that you simply 00:16:19.380 --> 00:16:21.829 align:start position:0% um safety properties that you simply cannot<00:16:19.740> express<00:16:20.040> in<00:16:20.399> solidity<00:16:20.940> and<00:16:21.600> that's 00:16:21.829 --> 00:16:21.839 align:start position:0% cannot express in solidity and that's 00:16:21.839 --> 00:16:23.870 align:start position:0% cannot express in solidity and that's like<00:16:22.079> one<00:16:22.500> advantage<00:16:22.980> of<00:16:23.279> this<00:16:23.399> symbolic 00:16:23.870 --> 00:16:23.880 align:start position:0% like one advantage of this symbolic 00:16:23.880 --> 00:16:25.310 align:start position:0% like one advantage of this symbolic execution 00:16:25.310 --> 00:16:25.320 align:start position:0% execution 00:16:25.320 --> 00:16:27.590 align:start position:0% execution um<00:16:25.380> approach<00:16:25.920> like<00:16:26.699> that<00:16:27.000> you<00:16:27.180> can<00:16:27.360> actually 00:16:27.590 --> 00:16:27.600 align:start position:0% um approach like that you can actually 00:16:27.600 --> 00:16:31.069 align:start position:0% um approach like that you can actually you<00:16:28.199> can<00:16:28.320> escape<00:16:28.620> from<00:16:29.279> from<00:16:29.579> the<00:16:30.000> uh<00:16:30.540> from<00:16:30.959> the 00:16:31.069 --> 00:16:31.079 align:start position:0% you can escape from from the uh from the 00:16:31.079 --> 00:16:32.990 align:start position:0% you can escape from from the uh from the specification<00:16:31.620> format<00:16:32.160> and<00:16:32.699> you<00:16:32.880> can 00:16:32.990 --> 00:16:33.000 align:start position:0% specification format and you can 00:16:33.000 --> 00:16:36.170 align:start position:0% specification format and you can actually<00:16:33.260> use<00:16:34.260> uh<00:16:34.680> the<00:16:34.920> the<00:16:35.040> K<00:16:35.339> language<00:16:35.639> to 00:16:36.170 --> 00:16:36.180 align:start position:0% actually use uh the the K language to 00:16:36.180 --> 00:16:38.449 align:start position:0% actually use uh the the K language to specify<00:16:36.660> uh<00:16:37.380> to<00:16:37.560> gain<00:16:37.980> additional 00:16:38.449 --> 00:16:38.459 align:start position:0% specify uh to gain additional 00:16:38.459 --> 00:16:40.069 align:start position:0% specify uh to gain additional expressiveness<00:16:39.240> and<00:16:39.480> express<00:16:39.660> more 00:16:40.069 --> 00:16:40.079 align:start position:0% expressiveness and express more 00:16:40.079 --> 00:16:41.629 align:start position:0% expressiveness and express more properties 00:16:41.629 --> 00:16:41.639 align:start position:0% properties 00:16:41.639 --> 00:16:43.009 align:start position:0% properties um 00:16:43.009 --> 00:16:43.019 align:start position:0% um 00:16:43.019 --> 00:16:46.850 align:start position:0% um so<00:16:43.940> Foundry<00:16:44.940> fuzzing<00:16:45.600> is<00:16:45.959> extremely<00:16:46.560> fast 00:16:46.850 --> 00:16:46.860 align:start position:0% so Foundry fuzzing is extremely fast 00:16:46.860 --> 00:16:50.150 align:start position:0% so Foundry fuzzing is extremely fast it's<00:16:47.339> like<00:16:47.519> you<00:16:48.060> can<00:16:48.180> run<00:16:48.779> 1<00:16:49.440> 000<00:16:49.500> samples<00:16:49.920> and 00:16:50.150 --> 00:16:50.160 align:start position:0% it's like you can run 1 000 samples and 00:16:50.160 --> 00:16:52.550 align:start position:0% it's like you can run 1 000 samples and a<00:16:50.279> couple<00:16:50.399> of<00:16:50.519> milliseconds<00:16:51.240> and<00:16:52.139> that<00:16:52.380> is 00:16:52.550 --> 00:16:52.560 align:start position:0% a couple of milliseconds and that is 00:16:52.560 --> 00:16:54.470 align:start position:0% a couple of milliseconds and that is like<00:16:52.800> really<00:16:53.040> important<00:16:53.459> for<00:16:53.699> for<00:16:53.940> developers 00:16:54.470 --> 00:16:54.480 align:start position:0% like really important for for developers 00:16:54.480 --> 00:16:56.749 align:start position:0% like really important for for developers who<00:16:54.660> want<00:16:54.839> to<00:16:54.959> get<00:16:55.019> instant<00:16:55.380> feedback 00:16:56.749 --> 00:16:56.759 align:start position:0% who want to get instant feedback 00:16:56.759 --> 00:16:57.350 align:start position:0% who want to get instant feedback um 00:16:57.350 --> 00:16:57.360 align:start position:0% um 00:16:57.360 --> 00:17:00.110 align:start position:0% um so<00:16:58.019> and<00:16:58.380> compared<00:16:58.860> to<00:16:58.920> that<00:16:59.220> symbolic 00:17:00.110 --> 00:17:00.120 align:start position:0% so and compared to that symbolic 00:17:00.120 --> 00:17:03.889 align:start position:0% so and compared to that symbolic execution<00:17:00.680> is<00:17:01.680> slow<00:17:02.040> so 00:17:03.889 --> 00:17:03.899 align:start position:0% execution is slow so 00:17:03.899 --> 00:17:06.169 align:start position:0% execution is slow so um 00:17:06.169 --> 00:17:06.179 align:start position:0% 00:17:06.179 --> 00:17:08.270 align:start position:0% um<00:17:06.360> and<00:17:07.020> there's<00:17:07.380> a<00:17:07.559> reason<00:17:07.679> for<00:17:07.919> that<00:17:08.100> so 00:17:08.270 --> 00:17:08.280 align:start position:0% um and there's a reason for that so 00:17:08.280 --> 00:17:10.429 align:start position:0% um and there's a reason for that so symbolic<00:17:08.819> execution<00:17:09.240> can<00:17:09.540> can<00:17:09.780> give<00:17:10.020> you<00:17:10.199> much 00:17:10.429 --> 00:17:10.439 align:start position:0% symbolic execution can can give you much 00:17:10.439 --> 00:17:13.370 align:start position:0% symbolic execution can can give you much more<00:17:10.740> safety<00:17:11.400> guarantees<00:17:11.880> than<00:17:12.240> than<00:17:12.839> fuzzing 00:17:13.370 --> 00:17:13.380 align:start position:0% more safety guarantees than than fuzzing 00:17:13.380 --> 00:17:16.549 align:start position:0% more safety guarantees than than fuzzing can<00:17:13.579> but<00:17:14.579> that<00:17:14.699> also<00:17:15.000> means<00:17:15.299> like<00:17:15.480> it's 00:17:16.549 --> 00:17:16.559 align:start position:0% can but that also means like it's 00:17:16.559 --> 00:17:18.309 align:start position:0% can but that also means like it's it's<00:17:17.699> um 00:17:18.309 --> 00:17:18.319 align:start position:0% it's um 00:17:18.319 --> 00:17:20.870 align:start position:0% it's um computationally<00:17:19.319> much<00:17:19.860> more<00:17:20.100> expensive<00:17:20.640> than 00:17:20.870 --> 00:17:20.880 align:start position:0% computationally much more expensive than 00:17:20.880 --> 00:17:22.429 align:start position:0% computationally much more expensive than fuzzing 00:17:22.429 --> 00:17:22.439 align:start position:0% fuzzing 00:17:22.439 --> 00:17:24.829 align:start position:0% fuzzing um<00:17:22.500> so<00:17:23.040> it's<00:17:23.280> slow<00:17:23.520> but<00:17:23.939> it's<00:17:24.059> not<00:17:24.299> too<00:17:24.600> slow 00:17:24.829 --> 00:17:24.839 align:start position:0% um so it's slow but it's not too slow 00:17:24.839 --> 00:17:27.350 align:start position:0% um so it's slow but it's not too slow like<00:17:25.199> uh<00:17:25.980> it<00:17:26.339> works<00:17:26.579> for<00:17:26.760> example<00:17:27.000> you<00:17:27.240> could 00:17:27.350 --> 00:17:27.360 align:start position:0% like uh it works for example you could 00:17:27.360 --> 00:17:30.049 align:start position:0% like uh it works for example you could simply<00:17:27.919> integrate<00:17:28.919> it<00:17:29.100> into<00:17:29.400> your<00:17:29.700> CI 00:17:30.049 --> 00:17:30.059 align:start position:0% simply integrate it into your CI 00:17:30.059 --> 00:17:32.750 align:start position:0% simply integrate it into your CI Pipeline<00:17:30.660> and<00:17:31.140> let<00:17:31.320> the<00:17:31.980> um<00:17:31.980> let<00:17:32.280> the<00:17:32.400> prover 00:17:32.750 --> 00:17:32.760 align:start position:0% Pipeline and let the um let the prover 00:17:32.760 --> 00:17:35.090 align:start position:0% Pipeline and let the um let the prover run<00:17:33.120> like<00:17:33.720> on<00:17:34.080> your<00:17:34.200> nightly<00:17:34.500> builds<00:17:34.919> for 00:17:35.090 --> 00:17:35.100 align:start position:0% run like on your nightly builds for 00:17:35.100 --> 00:17:38.150 align:start position:0% run like on your nightly builds for example<00:17:35.419> and<00:17:36.419> like<00:17:36.900> this<00:17:37.320> shows<00:17:37.740> like<00:17:37.919> the 00:17:38.150 --> 00:17:38.160 align:start position:0% example and like this shows like the 00:17:38.160 --> 00:17:41.870 align:start position:0% example and like this shows like the benefit<00:17:38.340> of<00:17:39.000> like<00:17:39.620> composing<00:17:40.620> both 00:17:41.870 --> 00:17:41.880 align:start position:0% benefit of like composing both 00:17:41.880 --> 00:17:44.270 align:start position:0% benefit of like composing both um<00:17:41.940> strategies<00:17:42.840> like<00:17:43.140> fuzzing<00:17:43.620> with<00:17:43.740> Foundry 00:17:44.270 --> 00:17:44.280 align:start position:0% um strategies like fuzzing with Foundry 00:17:44.280 --> 00:17:47.210 align:start position:0% um strategies like fuzzing with Foundry and<00:17:44.940> then<00:17:45.059> symbolic<00:17:45.660> execution<00:17:46.140> with<00:17:46.799> um<00:17:46.860> with 00:17:47.210 --> 00:17:47.220 align:start position:0% and then symbolic execution with um with 00:17:47.220 --> 00:17:49.549 align:start position:0% and then symbolic execution with um with KVM 00:17:49.549 --> 00:17:49.559 align:start position:0% KVM 00:17:49.559 --> 00:17:51.230 align:start position:0% KVM um 00:17:51.230 --> 00:17:51.240 align:start position:0% um 00:17:51.240 --> 00:17:53.990 align:start position:0% um so 00:17:53.990 --> 00:17:54.000 align:start position:0% so 00:17:54.000 --> 00:17:56.990 align:start position:0% so uh 00:17:56.990 --> 00:17:57.000 align:start position:0% 00:17:57.000 --> 00:17:59.270 align:start position:0% I<00:17:57.660> don't<00:17:57.780> want<00:17:57.900> to<00:17:58.020> go<00:17:58.200> over<00:17:58.380> every<00:17:58.679> line<00:17:59.039> in 00:17:59.270 --> 00:17:59.280 align:start position:0% I don't want to go over every line in 00:17:59.280 --> 00:18:01.070 align:start position:0% I don't want to go over every line in this<00:17:59.460> table<00:17:59.640> and<00:18:00.120> but<00:18:00.360> I<00:18:00.539> want<00:18:00.660> to<00:18:00.780> talk<00:18:00.960> about 00:18:01.070 --> 00:18:01.080 align:start position:0% this table and but I want to talk about 00:18:01.080 --> 00:18:03.950 align:start position:0% this table and but I want to talk about the<00:18:01.559> false<00:18:02.400> positives<00:18:02.880> and<00:18:03.480> the<00:18:03.600> false 00:18:03.950 --> 00:18:03.960 align:start position:0% the false positives and the false 00:18:03.960 --> 00:18:05.029 align:start position:0% the false positives and the false negatives 00:18:05.029 --> 00:18:05.039 align:start position:0% negatives 00:18:05.039 --> 00:18:06.350 align:start position:0% negatives so 00:18:06.350 --> 00:18:06.360 align:start position:0% so 00:18:06.360 --> 00:18:09.049 align:start position:0% so Foundry<00:18:07.020> doesn't<00:18:07.260> have<00:18:07.620> false<00:18:08.160> positives<00:18:08.640> and 00:18:09.049 --> 00:18:09.059 align:start position:0% Foundry doesn't have false positives and 00:18:09.059 --> 00:18:11.270 align:start position:0% Foundry doesn't have false positives and what<00:18:09.299> I<00:18:09.419> mean<00:18:09.539> by<00:18:09.660> that<00:18:09.900> is<00:18:10.200> when<00:18:10.740> Foundry 00:18:11.270 --> 00:18:11.280 align:start position:0% what I mean by that is when Foundry 00:18:11.280 --> 00:18:14.630 align:start position:0% what I mean by that is when Foundry comes<00:18:12.179> up<00:18:12.240> with<00:18:12.419> a<00:18:12.600> counter<00:18:12.900> example<00:18:13.640> that 00:18:14.630 --> 00:18:14.640 align:start position:0% comes up with a counter example that 00:18:14.640 --> 00:18:16.850 align:start position:0% comes up with a counter example that means<00:18:14.940> that<00:18:15.240> counterexample<00:18:16.200> really<00:18:16.440> works 00:18:16.850 --> 00:18:16.860 align:start position:0% means that counterexample really works 00:18:16.860 --> 00:18:19.250 align:start position:0% means that counterexample really works it<00:18:17.039> breaks<00:18:17.400> your<00:18:17.520> code<00:18:17.700> so<00:18:18.600> it<00:18:18.960> doesn't<00:18:19.020> come 00:18:19.250 --> 00:18:19.260 align:start position:0% it breaks your code so it doesn't come 00:18:19.260 --> 00:18:21.950 align:start position:0% it breaks your code so it doesn't come up<00:18:19.440> with<00:18:19.620> a<00:18:19.860> with<00:18:20.580> a<00:18:20.820> counter<00:18:21.299> example<00:18:21.720> that 00:18:21.950 --> 00:18:21.960 align:start position:0% up with a with a counter example that 00:18:21.960 --> 00:18:23.690 align:start position:0% up with a with a counter example that does<00:18:22.080> not<00:18:22.200> work<00:18:22.440> your<00:18:22.740> code<00:18:22.919> so<00:18:23.280> there's<00:18:23.460> no 00:18:23.690 --> 00:18:23.700 align:start position:0% does not work your code so there's no 00:18:23.700 --> 00:18:25.250 align:start position:0% does not work your code so there's no false<00:18:24.059> positive 00:18:25.250 --> 00:18:25.260 align:start position:0% false positive 00:18:25.260 --> 00:18:29.690 align:start position:0% false positive but<00:18:26.179> Foundry<00:18:27.179> has<00:18:27.480> false<00:18:28.380> negatives<00:18:28.740> and<00:18:29.460> that 00:18:29.690 --> 00:18:29.700 align:start position:0% but Foundry has false negatives and that 00:18:29.700 --> 00:18:31.850 align:start position:0% but Foundry has false negatives and that is<00:18:29.820> simply<00:18:30.179> if<00:18:30.600> Foundry<00:18:31.080> is<00:18:31.260> not<00:18:31.440> able<00:18:31.740> to 00:18:31.850 --> 00:18:31.860 align:start position:0% is simply if Foundry is not able to 00:18:31.860 --> 00:18:34.610 align:start position:0% is simply if Foundry is not able to choose<00:18:32.220> the<00:18:32.460> right<00:18:32.640> input<00:18:33.059> variables 00:18:34.610 --> 00:18:34.620 align:start position:0% choose the right input variables 00:18:34.620 --> 00:18:36.770 align:start position:0% choose the right input variables um<00:18:34.679> that<00:18:35.400> means<00:18:35.640> it<00:18:35.880> fails<00:18:36.179> to<00:18:36.299> guess<00:18:36.539> the 00:18:36.770 --> 00:18:36.780 align:start position:0% um that means it fails to guess the 00:18:36.780 --> 00:18:39.230 align:start position:0% um that means it fails to guess the right<00:18:36.960> counter<00:18:37.440> example<00:18:37.860> and<00:18:38.640> at<00:18:39.000> the<00:18:39.120> end 00:18:39.230 --> 00:18:39.240 align:start position:0% right counter example and at the end 00:18:39.240 --> 00:18:41.630 align:start position:0% right counter example and at the end founder<00:18:40.020> will<00:18:40.140> tell<00:18:40.380> you<00:18:40.500> that<00:18:40.860> test<00:18:41.160> that 00:18:41.630 --> 00:18:41.640 align:start position:0% founder will tell you that test that 00:18:41.640 --> 00:18:44.150 align:start position:0% founder will tell you that test that that<00:18:41.820> test<00:18:42.179> actually<00:18:42.539> passed<00:18:43.140> and<00:18:43.740> that<00:18:43.919> is 00:18:44.150 --> 00:18:44.160 align:start position:0% that test actually passed and that is 00:18:44.160 --> 00:18:46.789 align:start position:0% that test actually passed and that is like<00:18:44.520> the<00:18:45.000> false<00:18:45.419> sense<00:18:45.720> of<00:18:45.900> security<00:18:46.200> that 00:18:46.789 --> 00:18:46.799 align:start position:0% like the false sense of security that 00:18:46.799 --> 00:18:48.049 align:start position:0% like the false sense of security that you<00:18:46.919> get<00:18:47.100> from 00:18:48.049 --> 00:18:48.059 align:start position:0% you get from 00:18:48.059 --> 00:18:51.529 align:start position:0% you get from um<00:18:48.120> using<00:18:48.600> Foundry<00:18:49.080> alone<00:18:49.460> so<00:18:50.460> if<00:18:51.299> we<00:18:51.419> use 00:18:51.529 --> 00:18:51.539 align:start position:0% um using Foundry alone so if we use 00:18:51.539 --> 00:18:54.950 align:start position:0% um using Foundry alone so if we use symbolic<00:18:52.020> executions<00:18:52.860> like<00:18:53.580> we<00:18:53.880> cover<00:18:54.059> 100<00:18:54.419> of 00:18:54.950 --> 00:18:54.960 align:start position:0% symbolic executions like we cover 100 of 00:18:54.960 --> 00:18:56.870 align:start position:0% symbolic executions like we cover 100 of the<00:18:55.080> input<00:18:55.380> domain<00:18:55.799> and<00:18:56.100> we<00:18:56.280> will<00:18:56.460> find<00:18:56.700> that 00:18:56.870 --> 00:18:56.880 align:start position:0% the input domain and we will find that 00:18:56.880 --> 00:18:59.390 align:start position:0% the input domain and we will find that counter<00:18:57.240> example<00:18:57.600> there's<00:18:57.780> no<00:18:58.020> matter<00:18:58.140> what 00:18:59.390 --> 00:18:59.400 align:start position:0% counter example there's no matter what 00:18:59.400 --> 00:19:01.789 align:start position:0% counter example there's no matter what um<00:18:59.520> so<00:18:59.940> there<00:19:00.240> are<00:19:00.360> no<00:19:00.660> false<00:19:01.080> negatives<00:19:01.380> when 00:19:01.789 --> 00:19:01.799 align:start position:0% um so there are no false negatives when 00:19:01.799 --> 00:19:05.330 align:start position:0% um so there are no false negatives when you<00:19:01.980> use<00:19:02.220> uh<00:19:02.640> when<00:19:03.299> you<00:19:03.480> use<00:19:03.600> kevm 00:19:05.330 --> 00:19:05.340 align:start position:0% you use uh when you use kevm 00:19:05.340 --> 00:19:05.990 align:start position:0% you use uh when you use kevm um 00:19:05.990 --> 00:19:06.000 align:start position:0% um 00:19:06.000 --> 00:19:07.610 align:start position:0% um then<00:19:06.539> there's<00:19:06.780> a<00:19:06.960> diff<00:19:07.080> there's<00:19:07.440> another 00:19:07.610 --> 00:19:07.620 align:start position:0% then there's a diff there's another 00:19:07.620 --> 00:19:09.350 align:start position:0% then there's a diff there's another trade-off<00:19:08.220> and<00:19:08.460> that<00:19:08.640> is<00:19:08.760> Foundry<00:19:09.240> is 00:19:09.350 --> 00:19:09.360 align:start position:0% trade-off and that is Foundry is 00:19:09.360 --> 00:19:11.810 align:start position:0% trade-off and that is Foundry is extremely<00:19:09.840> easy<00:19:10.080> to<00:19:10.320> use<00:19:10.500> I<00:19:11.100> I'd<00:19:11.280> argue<00:19:11.700> it's 00:19:11.810 --> 00:19:11.820 align:start position:0% extremely easy to use I I'd argue it's 00:19:11.820 --> 00:19:14.270 align:start position:0% extremely easy to use I I'd argue it's even<00:19:12.059> easier<00:19:12.480> to<00:19:12.720> use<00:19:12.900> than<00:19:13.260> than<00:19:13.559> hardhead<00:19:14.039> or 00:19:14.270 --> 00:19:14.280 align:start position:0% even easier to use than than hardhead or 00:19:14.280 --> 00:19:17.270 align:start position:0% even easier to use than than hardhead or or<00:19:14.640> truffle<00:19:15.299> uh<00:19:15.900> for<00:19:16.140> testing<00:19:16.440> because<00:19:16.679> well 00:19:17.270 --> 00:19:17.280 align:start position:0% or truffle uh for testing because well 00:19:17.280 --> 00:19:19.130 align:start position:0% or truffle uh for testing because well the<00:19:17.820> developers<00:19:18.299> the<00:19:18.600> smart<00:19:18.780> contract 00:19:19.130 --> 00:19:19.140 align:start position:0% the developers the smart contract 00:19:19.140 --> 00:19:22.310 align:start position:0% the developers the smart contract developers<00:19:19.620> are<00:19:19.860> already<00:19:20.039> familiar<00:19:20.760> with<00:19:22.260> um 00:19:22.310 --> 00:19:22.320 align:start position:0% developers are already familiar with um 00:19:22.320 --> 00:19:24.650 align:start position:0% developers are already familiar with um with<00:19:22.919> solidity<00:19:23.640> like<00:19:23.940> the<00:19:24.179> language<00:19:24.299> that 00:19:24.650 --> 00:19:24.660 align:start position:0% with solidity like the language that 00:19:24.660 --> 00:19:27.470 align:start position:0% with solidity like the language that they<00:19:24.780> use<00:19:24.960> to<00:19:25.200> write<00:19:25.380> their<00:19:25.620> contracts<00:19:26.100> and 00:19:27.470 --> 00:19:27.480 align:start position:0% they use to write their contracts and 00:19:27.480 --> 00:19:30.130 align:start position:0% they use to write their contracts and um<00:19:27.539> so<00:19:27.840> that<00:19:28.080> makes<00:19:28.260> foundu<00:19:28.980> very<00:19:29.280> easy<00:19:29.460> to<00:19:29.700> use 00:19:30.130 --> 00:19:30.140 align:start position:0% um so that makes foundu very easy to use 00:19:30.140 --> 00:19:34.789 align:start position:0% um so that makes foundu very easy to use uh<00:19:31.160> symbolic<00:19:32.160> execution<00:19:32.640> with<00:19:33.000> KVM<00:19:33.600> is<00:19:33.960> is<00:19:34.559> a 00:19:34.789 --> 00:19:34.799 align:start position:0% uh symbolic execution with KVM is is a 00:19:34.799 --> 00:19:37.370 align:start position:0% uh symbolic execution with KVM is is a little<00:19:34.860> bit<00:19:35.039> different<00:19:35.460> like<00:19:35.940> it's<00:19:36.780> very<00:19:37.080> easy 00:19:37.370 --> 00:19:37.380 align:start position:0% little bit different like it's very easy 00:19:37.380 --> 00:19:39.950 align:start position:0% little bit different like it's very easy to<00:19:37.919> try<00:19:38.160> out<00:19:38.400> it's<00:19:38.760> it's<00:19:39.000> like<00:19:39.360> if<00:19:39.600> you<00:19:39.720> have<00:19:39.840> it 00:19:39.950 --> 00:19:39.960 align:start position:0% to try out it's it's like if you have it 00:19:39.960 --> 00:19:42.169 align:start position:0% to try out it's it's like if you have it installed<00:19:40.260> on<00:19:40.380> your<00:19:40.559> machine<00:19:40.799> and<00:19:41.640> you<00:19:42.000> have 00:19:42.169 --> 00:19:42.179 align:start position:0% installed on your machine and you have 00:19:42.179 --> 00:19:44.810 align:start position:0% installed on your machine and you have Foundry<00:19:42.600> tests<00:19:42.960> specified<00:19:43.380> you<00:19:44.100> can<00:19:44.160> just<00:19:44.400> try 00:19:44.810 --> 00:19:44.820 align:start position:0% Foundry tests specified you can just try 00:19:44.820 --> 00:19:45.950 align:start position:0% Foundry tests specified you can just try running 00:19:45.950 --> 00:19:45.960 align:start position:0% running 00:19:45.960 --> 00:19:47.510 align:start position:0% running um<00:19:46.020> the<00:19:46.140> KVM<00:19:46.679> on<00:19:46.860> that<00:19:46.980> and<00:19:47.160> maybe<00:19:47.340> you're 00:19:47.510 --> 00:19:47.520 align:start position:0% um the KVM on that and maybe you're 00:19:47.520 --> 00:19:50.570 align:start position:0% um the KVM on that and maybe you're lucky<00:19:47.760> and<00:19:48.539> maybe<00:19:48.840> uh<00:19:49.380> the<00:19:49.559> KVM<00:19:50.039> will<00:19:50.340> tell<00:19:50.460> you 00:19:50.570 --> 00:19:50.580 align:start position:0% lucky and maybe uh the KVM will tell you 00:19:50.580 --> 00:19:53.750 align:start position:0% lucky and maybe uh the KVM will tell you right<00:19:50.820> your<00:19:51.179> test<00:19:51.360> pass<00:19:51.600> or<00:19:52.320> your<00:19:52.500> your<00:19:52.679> your 00:19:53.750 --> 00:19:53.760 align:start position:0% right your test pass or your your your 00:19:53.760 --> 00:19:56.570 align:start position:0% right your test pass or your your your um yeah<00:19:54.600> your<00:19:54.900> test<00:19:55.080> was<00:19:55.320> proven<00:19:55.740> or<00:19:56.280> it<00:19:56.460> was 00:19:56.570 --> 00:19:56.580 align:start position:0% um yeah your test was proven or it was 00:19:56.580 --> 00:19:58.909 align:start position:0% um yeah your test was proven or it was like<00:19:56.820> or<00:19:57.059> we<00:19:57.240> found<00:19:57.360> a<00:19:57.539> counter<00:19:57.900> example<00:19:58.260> but 00:19:58.909 --> 00:19:58.919 align:start position:0% like or we found a counter example but 00:19:58.919 --> 00:20:00.590 align:start position:0% like or we found a counter example but in<00:19:59.220> some<00:19:59.340> cases 00:20:00.590 --> 00:20:00.600 align:start position:0% in some cases 00:20:00.600 --> 00:20:02.690 align:start position:0% in some cases um<00:20:00.660> you<00:20:01.140> will<00:20:01.260> get<00:20:01.440> like<00:20:01.679> a<00:20:01.919> third<00:20:02.100> state<00:20:02.400> that 00:20:02.690 --> 00:20:02.700 align:start position:0% um you will get like a third state that 00:20:02.700 --> 00:20:05.270 align:start position:0% um you will get like a third state that is<00:20:02.820> you<00:20:03.419> didn't<00:20:03.840> pass<00:20:04.080> you<00:20:04.440> didn't<00:20:04.559> fail<00:20:04.860> but 00:20:05.270 --> 00:20:05.280 align:start position:0% is you didn't pass you didn't fail but 00:20:05.280 --> 00:20:08.510 align:start position:0% is you didn't pass you didn't fail but we<00:20:05.400> are<00:20:05.580> not<00:20:05.640> sure<00:20:06.120> like<00:20:06.900> we<00:20:07.500> don't<00:20:07.620> know<00:20:07.860> and 00:20:08.510 --> 00:20:08.520 align:start position:0% we are not sure like we don't know and 00:20:08.520 --> 00:20:10.130 align:start position:0% we are not sure like we don't know and if<00:20:08.760> you<00:20:08.880> end<00:20:09.059> up<00:20:09.179> in<00:20:09.419> this<00:20:09.539> we<00:20:09.840> don't<00:20:09.960> know 00:20:10.130 --> 00:20:10.140 align:start position:0% if you end up in this we don't know 00:20:10.140 --> 00:20:11.450 align:start position:0% if you end up in this we don't know State 00:20:11.450 --> 00:20:11.460 align:start position:0% State 00:20:11.460 --> 00:20:13.990 align:start position:0% State um that<00:20:12.240> is<00:20:12.419> when<00:20:12.780> a<00:20:13.260> human 00:20:13.990 --> 00:20:14.000 align:start position:0% um that is when a human 00:20:14.000 --> 00:20:17.270 align:start position:0% um that is when a human needs<00:20:15.000> to<00:20:15.179> drive<00:20:15.480> the<00:20:15.840> proof<00:20:16.140> forward<00:20:16.559> and 00:20:17.270 --> 00:20:17.280 align:start position:0% needs to drive the proof forward and 00:20:17.280 --> 00:20:20.090 align:start position:0% needs to drive the proof forward and that<00:20:17.460> is<00:20:17.580> actually<00:20:17.820> something<00:20:18.480> uh<00:20:19.260> that<00:20:19.679> needs 00:20:20.090 --> 00:20:20.100 align:start position:0% that is actually something uh that needs 00:20:20.100 --> 00:20:22.190 align:start position:0% that is actually something uh that needs some<00:20:20.340> practice<00:20:20.580> I<00:20:21.000> think<00:20:21.360> I<00:20:21.660> don't<00:20:21.780> think<00:20:21.960> it's 00:20:22.190 --> 00:20:22.200 align:start position:0% some practice I think I don't think it's 00:20:22.200 --> 00:20:24.770 align:start position:0% some practice I think I don't think it's impossible<00:20:22.620> to<00:20:22.860> learn<00:20:23.039> uh<00:20:23.880> I<00:20:24.059> learned<00:20:24.360> it<00:20:24.480> so 00:20:24.770 --> 00:20:24.780 align:start position:0% impossible to learn uh I learned it so 00:20:24.780 --> 00:20:26.750 align:start position:0% impossible to learn uh I learned it so I'm<00:20:25.080> sure<00:20:25.320> you<00:20:25.500> guys<00:20:25.679> can 00:20:26.750 --> 00:20:26.760 align:start position:0% I'm sure you guys can 00:20:26.760 --> 00:20:29.270 align:start position:0% I'm sure you guys can um<00:20:26.880> but<00:20:27.120> it's<00:20:27.419> it's<00:20:27.720> harder<00:20:28.140> than<00:20:28.320> just<00:20:28.679> uh 00:20:29.270 --> 00:20:29.280 align:start position:0% um but it's it's harder than just uh 00:20:29.280 --> 00:20:34.070 align:start position:0% um but it's it's harder than just uh just<00:20:29.940> calling<00:20:30.840> um<00:20:30.960> a<00:20:31.380> Foundry<00:20:31.860> test<00:20:32.039> so 00:20:34.070 --> 00:20:34.080 align:start position:0% just calling um a Foundry test so 00:20:34.080 --> 00:20:36.289 align:start position:0% just calling um a Foundry test so uh 00:20:36.289 --> 00:20:36.299 align:start position:0% uh 00:20:36.299 --> 00:20:39.529 align:start position:0% uh one<00:20:37.080> final<00:20:37.260> example<00:20:37.799> of<00:20:38.400> running<00:20:38.700> running 00:20:39.529 --> 00:20:39.539 align:start position:0% one final example of running running 00:20:39.539 --> 00:20:42.350 align:start position:0% one final example of running running Foundry<00:20:40.200> and<00:20:40.440> running<00:20:40.740> the<00:20:41.100> KVM<00:20:41.700> symbolic 00:20:42.350 --> 00:20:42.360 align:start position:0% Foundry and running the KVM symbolic 00:20:42.360 --> 00:20:44.210 align:start position:0% Foundry and running the KVM symbolic execution<00:20:42.720> engine<00:20:42.960> on<00:20:43.320> the<00:20:43.500> same<00:20:43.620> test<00:20:43.799> Suite 00:20:44.210 --> 00:20:44.220 align:start position:0% execution engine on the same test Suite 00:20:44.220 --> 00:20:47.510 align:start position:0% execution engine on the same test Suite so<00:20:44.880> on<00:20:45.179> the<00:20:45.299> uh<00:20:45.780> on<00:20:46.020> the<00:20:46.140> top<00:20:46.260> image<00:20:46.740> I<00:20:47.340> just 00:20:47.510 --> 00:20:47.520 align:start position:0% so on the uh on the top image I just 00:20:47.520 --> 00:20:49.970 align:start position:0% so on the uh on the top image I just called<00:20:47.880> Forge<00:20:48.660> test 00:20:49.970 --> 00:20:49.980 align:start position:0% called Forge test 00:20:49.980 --> 00:20:53.690 align:start position:0% called Forge test um<00:20:50.100> and<00:20:50.760> I<00:20:50.940> can<00:20:51.059> see<00:20:51.240> the<00:20:51.419> output<00:20:51.840> like 00:20:53.690 --> 00:20:53.700 align:start position:0% um and I can see the output like 00:20:53.700 --> 00:20:57.110 align:start position:0% um and I can see the output like um<00:20:53.760> that<00:20:54.539> tells<00:20:54.840> me<00:20:54.900> okay<00:20:55.400> uh<00:20:56.400> I<00:20:56.880> was<00:20:56.940> running 00:20:57.110 --> 00:20:57.120 align:start position:0% um that tells me okay uh I was running 00:20:57.120 --> 00:20:59.210 align:start position:0% um that tells me okay uh I was running one<00:20:57.480> test 00:20:59.210 --> 00:20:59.220 align:start position:0% one test 00:20:59.220 --> 00:21:04.090 align:start position:0% one test um<00:20:59.280> and<00:21:00.059> it<00:21:00.539> passed<00:21:01.440> I<00:21:02.400> tried 00:21:04.090 --> 00:21:04.100 align:start position:0% um and it passed I tried 00:21:04.100 --> 00:21:07.730 align:start position:0% um and it passed I tried 256<00:21:05.240> uh<00:21:06.240> samples<00:21:06.660> on<00:21:06.840> that<00:21:07.020> tested<00:21:07.320> that<00:21:07.500> it 00:21:07.730 --> 00:21:07.740 align:start position:0% 256 uh samples on that tested that it 00:21:07.740 --> 00:21:09.590 align:start position:0% 256 uh samples on that tested that it means<00:21:07.980> Foundry 00:21:09.590 --> 00:21:09.600 align:start position:0% means Foundry 00:21:09.600 --> 00:21:12.830 align:start position:0% means Foundry um<00:21:09.720> uh<00:21:10.559> won<00:21:10.799> this<00:21:10.980> test<00:21:11.220> was<00:21:11.460> 256<00:21:12.419> different 00:21:12.830 --> 00:21:12.840 align:start position:0% um uh won this test was 256 different 00:21:12.840 --> 00:21:14.450 align:start position:0% um uh won this test was 256 different inputs 00:21:14.450 --> 00:21:14.460 align:start position:0% inputs 00:21:14.460 --> 00:21:15.230 align:start position:0% inputs um 00:21:15.230 --> 00:21:15.240 align:start position:0% um 00:21:15.240 --> 00:21:18.710 align:start position:0% um and<00:21:15.720> then<00:21:15.900> I<00:21:16.740> can<00:21:16.919> use<00:21:17.220> like<00:21:17.940> after<00:21:18.179> I've<00:21:18.480> won 00:21:18.710 --> 00:21:18.720 align:start position:0% and then I can use like after I've won 00:21:18.720 --> 00:21:21.950 align:start position:0% and then I can use like after I've won the<00:21:18.900> founder<00:21:19.500> test<00:21:19.620> I<00:21:19.919> can<00:21:20.100> run<00:21:20.419> KVM<00:21:21.419> Foundry 00:21:21.950 --> 00:21:21.960 align:start position:0% the founder test I can run KVM Foundry 00:21:21.960 --> 00:21:24.890 align:start position:0% the founder test I can run KVM Foundry compile<00:21:22.380> and<00:21:22.860> give<00:21:23.039> it<00:21:23.240> a<00:21:24.240> Foundry<00:21:24.720> out 00:21:24.890 --> 00:21:24.900 align:start position:0% compile and give it a Foundry out 00:21:24.900 --> 00:21:27.169 align:start position:0% compile and give it a Foundry out directory<00:21:25.500> as<00:21:25.740> a<00:21:25.919> parameter<00:21:26.400> and<00:21:26.880> what<00:21:27.059> this 00:21:27.169 --> 00:21:27.179 align:start position:0% directory as a parameter and what this 00:21:27.179 --> 00:21:30.230 align:start position:0% directory as a parameter and what this comment<00:21:27.480> will<00:21:27.660> do<00:21:27.900> is<00:21:28.200> it<00:21:28.740> will<00:21:28.919> turn<00:21:29.240> The 00:21:30.230 --> 00:21:30.240 align:start position:0% comment will do is it will turn The 00:21:30.240 --> 00:21:32.390 align:start position:0% comment will do is it will turn The Foundry<00:21:30.659> test<00:21:30.840> Suite<00:21:31.380> into<00:21:31.860> a<00:21:32.100> proof 00:21:32.390 --> 00:21:32.400 align:start position:0% Foundry test Suite into a proof 00:21:32.400 --> 00:21:34.970 align:start position:0% Foundry test Suite into a proof obligation<00:21:32.940> for<00:21:33.840> the<00:21:34.140> symbolic<00:21:34.559> execution 00:21:34.970 --> 00:21:34.980 align:start position:0% obligation for the symbolic execution 00:21:34.980 --> 00:21:39.110 align:start position:0% obligation for the symbolic execution engine<00:21:35.280> like<00:21:35.940> it's<00:21:36.120> a<00:21:36.299> compile<00:21:36.539> step<00:21:36.840> and<00:21:37.740> then 00:21:39.110 --> 00:21:39.120 align:start position:0% engine like it's a compile step and then 00:21:39.120 --> 00:21:40.010 align:start position:0% engine like it's a compile step and then um 00:21:40.010 --> 00:21:40.020 align:start position:0% um 00:21:40.020 --> 00:21:42.470 align:start position:0% um when<00:21:40.500> I've<00:21:40.740> done<00:21:40.919> that<00:21:41.100> I<00:21:41.580> can<00:21:41.760> actually<00:21:41.940> try 00:21:42.470 --> 00:21:42.480 align:start position:0% when I've done that I can actually try 00:21:42.480 --> 00:21:44.810 align:start position:0% when I've done that I can actually try to<00:21:42.840> discharge<00:21:43.380> this<00:21:43.559> proof<00:21:43.860> obligation<00:21:44.280> by 00:21:44.810 --> 00:21:44.820 align:start position:0% to discharge this proof obligation by 00:21:44.820 --> 00:21:47.870 align:start position:0% to discharge this proof obligation by one<00:21:45.000> in<00:21:45.240> KVM<00:21:45.780> Foundry<00:21:46.380> proof 00:21:47.870 --> 00:21:47.880 align:start position:0% one in KVM Foundry proof 00:21:47.880 --> 00:21:50.930 align:start position:0% one in KVM Foundry proof um<00:21:48.020> and<00:21:49.020> the<00:21:49.799> output<00:21:50.039> that<00:21:50.220> you<00:21:50.400> see<00:21:50.580> here<00:21:50.760> is 00:21:50.930 --> 00:21:50.940 align:start position:0% um and the output that you see here is 00:21:50.940 --> 00:21:56.390 align:start position:0% um and the output that you see here is the<00:21:51.120> lucky<00:21:51.659> case<00:21:52.520> that<00:21:54.020> our<00:21:55.020> like<00:21:55.679> symbolic 00:21:56.390 --> 00:21:56.400 align:start position:0% the lucky case that our like symbolic 00:21:56.400 --> 00:21:59.149 align:start position:0% the lucky case that our like symbolic execution<00:21:56.820> was<00:21:57.120> actually<00:21:57.480> able<00:21:58.020> to<00:21:58.679> discharge 00:21:59.149 --> 00:21:59.159 align:start position:0% execution was actually able to discharge 00:21:59.159 --> 00:22:01.549 align:start position:0% execution was actually able to discharge the<00:21:59.280> proof<00:21:59.520> obligation<00:22:00.000> and<00:22:00.720> that's<00:22:01.020> why<00:22:01.260> it 00:22:01.549 --> 00:22:01.559 align:start position:0% the proof obligation and that's why it 00:22:01.559 --> 00:22:04.250 align:start position:0% the proof obligation and that's why it says<00:22:01.799> top<00:22:02.220> top<00:22:02.580> at<00:22:03.000> the<00:22:03.120> bottom 00:22:04.250 --> 00:22:04.260 align:start position:0% says top top at the bottom 00:22:04.260 --> 00:22:05.210 align:start position:0% says top top at the bottom um 00:22:05.210 --> 00:22:05.220 align:start position:0% um 00:22:05.220 --> 00:22:06.649 align:start position:0% um so 00:22:06.649 --> 00:22:06.659 align:start position:0% so 00:22:06.659 --> 00:22:09.409 align:start position:0% so but<00:22:07.320> well<00:22:07.919> when<00:22:08.280> this<00:22:08.520> when<00:22:08.760> a<00:22:08.940> test<00:22:09.059> doesn't 00:22:09.409 --> 00:22:09.419 align:start position:0% but well when this when a test doesn't 00:22:09.419 --> 00:22:11.330 align:start position:0% but well when this when a test doesn't pass<00:22:09.720> you<00:22:10.020> will<00:22:10.140> get<00:22:10.320> a<00:22:10.440> counter<00:22:10.740> example<00:22:11.039> that 00:22:11.330 --> 00:22:11.340 align:start position:0% pass you will get a counter example that 00:22:11.340 --> 00:22:14.930 align:start position:0% pass you will get a counter example that is<00:22:11.520> not<00:22:11.760> as<00:22:12.179> easy<00:22:12.419> like<00:22:13.260> to<00:22:13.799> link<00:22:14.220> back<00:22:14.520> to<00:22:14.760> the 00:22:14.930 --> 00:22:14.940 align:start position:0% is not as easy like to link back to the 00:22:14.940 --> 00:22:17.690 align:start position:0% is not as easy like to link back to the original<00:22:15.120> code<00:22:15.539> of<00:22:15.720> the<00:22:15.900> test<00:22:16.080> than<00:22:16.500> the 00:22:17.690 --> 00:22:17.700 align:start position:0% original code of the test than the 00:22:17.700 --> 00:22:20.810 align:start position:0% original code of the test than the um<00:22:17.820> then<00:22:18.659> The<00:22:18.780> Foundry<00:22:19.080> country<00:22:19.260> example<00:22:19.860> or 00:22:20.810 --> 00:22:20.820 align:start position:0% um then The Foundry country example or 00:22:20.820 --> 00:22:22.730 align:start position:0% um then The Foundry country example or even<00:22:21.299> worse<00:22:21.539> it<00:22:21.720> will<00:22:21.900> give<00:22:22.020> you<00:22:22.140> this<00:22:22.380> unknown 00:22:22.730 --> 00:22:22.740 align:start position:0% even worse it will give you this unknown 00:22:22.740 --> 00:22:24.590 align:start position:0% even worse it will give you this unknown State<00:22:23.039> and<00:22:23.460> like<00:22:23.700> making<00:22:23.880> sense<00:22:24.179> of<00:22:24.360> this 00:22:24.590 --> 00:22:24.600 align:start position:0% State and like making sense of this 00:22:24.600 --> 00:22:26.330 align:start position:0% State and like making sense of this unknown<00:22:24.900> State<00:22:25.140> really<00:22:25.620> requires<00:22:26.159> some 00:22:26.330 --> 00:22:26.340 align:start position:0% unknown State really requires some 00:22:26.340 --> 00:22:28.370 align:start position:0% unknown State really requires some practice<00:22:26.580> you<00:22:27.000> you<00:22:27.179> need<00:22:27.419> to<00:22:27.539> to<00:22:27.840> learn<00:22:28.080> to 00:22:28.370 --> 00:22:28.380 align:start position:0% practice you you need to to learn to 00:22:28.380 --> 00:22:30.350 align:start position:0% practice you you need to to learn to read<00:22:28.500> these<00:22:28.740> configurations<00:22:29.220> to<00:22:29.580> need<00:22:29.820> to<00:22:30.240> eat 00:22:30.350 --> 00:22:30.360 align:start position:0% read these configurations to need to eat 00:22:30.360 --> 00:22:32.990 align:start position:0% read these configurations to need to eat these<00:22:30.600> stuck<00:22:30.780> States 00:22:32.990 --> 00:22:33.000 align:start position:0% these stuck States 00:22:33.000 --> 00:22:36.770 align:start position:0% these stuck States um<00:22:33.480> so<00:22:34.200> that's<00:22:34.679> basically<00:22:35.159> it<00:22:35.400> with<00:22:35.820> my<00:22:36.000> talk 00:22:36.770 --> 00:22:36.780 align:start position:0% um so that's basically it with my talk 00:22:36.780 --> 00:22:38.210 align:start position:0% um so that's basically it with my talk um<00:22:36.840> I've<00:22:37.140> just 00:22:38.210 --> 00:22:38.220 align:start position:0% um I've just 00:22:38.220 --> 00:22:41.930 align:start position:0% um I've just um<00:22:38.280> one<00:22:38.820> more<00:22:39.059> a<00:22:39.960> couple<00:22:40.200> of<00:22:40.380> more<00:22:40.500> notes<00:22:40.980> so<00:22:41.640> I 00:22:41.930 --> 00:22:41.940 align:start position:0% um one more a couple of more notes so I 00:22:41.940 --> 00:22:43.789 align:start position:0% um one more a couple of more notes so I work<00:22:42.059> at<00:22:42.240> one<00:22:42.419> time<00:22:42.600> verification<00:22:43.200> and<00:22:43.620> we 00:22:43.789 --> 00:22:43.799 align:start position:0% work at one time verification and we 00:22:43.799 --> 00:22:46.250 align:start position:0% work at one time verification and we have<00:22:43.919> a<00:22:44.100> research<00:22:44.460> department<00:22:44.720> and<00:22:45.720> we<00:22:45.960> just 00:22:46.250 --> 00:22:46.260 align:start position:0% have a research department and we just 00:22:46.260 --> 00:22:47.750 align:start position:0% have a research department and we just recently 00:22:47.750 --> 00:22:47.760 align:start position:0% recently 00:22:47.760 --> 00:22:50.270 align:start position:0% recently um<00:22:47.820> posted<00:22:48.360> some<00:22:48.720> open<00:22:49.020> research<00:22:49.799> challenges 00:22:50.270 --> 00:22:50.280 align:start position:0% um posted some open research challenges 00:22:50.280 --> 00:22:52.669 align:start position:0% um posted some open research challenges on<00:22:50.520> our<00:22:50.640> website<00:22:51.179> research<00:22:52.080> dot<00:22:52.380> runtime 00:22:52.669 --> 00:22:52.679 align:start position:0% on our website research dot runtime 00:22:52.679 --> 00:22:54.950 align:start position:0% on our website research dot runtime verification.com<00:22:53.520> and<00:22:54.000> if<00:22:54.539> you<00:22:54.720> are<00:22:54.840> a 00:22:54.950 --> 00:22:54.960 align:start position:0% verification.com and if you are a 00:22:54.960 --> 00:22:57.649 align:start position:0% verification.com and if you are a researcher<00:22:55.620> go<00:22:56.100> to<00:22:56.220> that<00:22:56.400> website<00:22:56.820> see<00:22:57.480> if 00:22:57.649 --> 00:22:57.659 align:start position:0% researcher go to that website see if 00:22:57.659 --> 00:22:59.390 align:start position:0% researcher go to that website see if something<00:22:57.840> interests<00:22:58.500> you<00:22:58.620> and<00:22:58.919> we<00:22:59.100> have<00:22:59.220> like 00:22:59.390 --> 00:22:59.400 align:start position:0% something interests you and we have like 00:22:59.400 --> 00:23:01.070 align:start position:0% something interests you and we have like multiple<00:22:59.820> ways<00:23:00.120> to<00:23:00.240> collaborate<00:23:00.720> with<00:23:00.960> you 00:23:01.070 --> 00:23:01.080 align:start position:0% multiple ways to collaborate with you 00:23:01.080 --> 00:23:03.529 align:start position:0% multiple ways to collaborate with you like<00:23:01.679> if<00:23:01.919> everything<00:23:02.159> if<00:23:02.640> anything<00:23:02.820> interests 00:23:03.529 --> 00:23:03.539 align:start position:0% like if everything if anything interests 00:23:03.539 --> 00:23:04.310 align:start position:0% like if everything if anything interests you 00:23:04.310 --> 00:23:04.320 align:start position:0% you 00:23:04.320 --> 00:23:06.830 align:start position:0% you all<00:23:04.980> right<00:23:05.220> and<00:23:05.760> then<00:23:06.120> like<00:23:06.480> one<00:23:06.720> other 00:23:06.830 --> 00:23:06.840 align:start position:0% all right and then like one other 00:23:06.840 --> 00:23:08.210 align:start position:0% all right and then like one other announcement 00:23:08.210 --> 00:23:08.220 align:start position:0% announcement 00:23:08.220 --> 00:23:09.470 align:start position:0% announcement um 00:23:09.470 --> 00:23:09.480 align:start position:0% um 00:23:09.480 --> 00:23:11.930 align:start position:0% um a<00:23:09.659> colleague<00:23:10.200> of<00:23:10.320> mine<00:23:10.580> Richardson<00:23:11.580> audience 00:23:11.930 --> 00:23:11.940 align:start position:0% a colleague of mine Richardson audience 00:23:11.940 --> 00:23:15.169 align:start position:0% a colleague of mine Richardson audience somewhere<00:23:12.360> I<00:23:12.659> see<00:23:12.840> them<00:23:13.020> uh<00:23:13.980> he's<00:23:14.220> giving<00:23:14.460> a 00:23:15.169 --> 00:23:15.179 align:start position:0% somewhere I see them uh he's giving a 00:23:15.179 --> 00:23:17.630 align:start position:0% somewhere I see them uh he's giving a workshop<00:23:15.659> on<00:23:16.080> formal<00:23:16.559> methods<00:23:17.159> for<00:23:17.460> the 00:23:17.630 --> 00:23:17.640 align:start position:0% workshop on formal methods for the 00:23:17.640 --> 00:23:23.330 align:start position:0% workshop on formal methods for the working<00:23:17.820> D5<00:23:18.360> Dev<00:23:18.720> tomorrow<00:23:19.280> at<00:23:20.280> uh<00:23:21.240> at<00:23:21.740> 11AM<00:23:22.740> in 00:23:23.330 --> 00:23:23.340 align:start position:0% working D5 Dev tomorrow at uh at 11AM in 00:23:23.340 --> 00:23:26.270 align:start position:0% working D5 Dev tomorrow at uh at 11AM in Workshop<00:23:23.700> room<00:23:23.880> number<00:23:24.179> three<00:23:24.539> so<00:23:25.500> uh<00:23:25.919> if<00:23:26.159> you 00:23:26.270 --> 00:23:26.280 align:start position:0% Workshop room number three so uh if you 00:23:26.280 --> 00:23:28.610 align:start position:0% Workshop room number three so uh if you like<00:23:26.400> this<00:23:26.700> talk<00:23:26.940> uh<00:23:27.720> go<00:23:27.960> ahead<00:23:28.200> and<00:23:28.500> visit 00:23:28.610 --> 00:23:28.620 align:start position:0% like this talk uh go ahead and visit 00:23:28.620 --> 00:23:31.130 align:start position:0% like this talk uh go ahead and visit Richard's<00:23:29.460> talk<00:23:29.580> it's<00:23:29.940> uh<00:23:30.600> I<00:23:30.960> highly 00:23:31.130 --> 00:23:31.140 align:start position:0% Richard's talk it's uh I highly 00:23:31.140 --> 00:23:33.830 align:start position:0% Richard's talk it's uh I highly recommend<00:23:31.620> it<00:23:31.799> right<00:23:32.520> and<00:23:33.000> that's<00:23:33.360> it<00:23:33.539> I<00:23:33.720> think 00:23:33.830 --> 00:23:33.840 align:start position:0% recommend it right and that's it I think 00:23:33.840 --> 00:23:36.710 align:start position:0% recommend it right and that's it I think we<00:23:34.020> have<00:23:34.080> some<00:23:34.320> time<00:23:34.500> for<00:23:34.679> questions<00:23:34.980> do<00:23:35.520> we 00:23:36.710 --> 00:23:36.720 align:start position:0% we have some time for questions do we 00:23:36.720 --> 00:23:40.250 align:start position:0% we have some time for questions do we we<00:23:37.260> have 00:23:40.250 --> 00:23:40.260 align:start position:0% 00:23:40.260 --> 00:23:44.690 align:start position:0% do<00:23:40.679> we<00:23:40.860> have<00:23:40.980> a<00:23:41.220> microphone<00:23:41.700> for<00:23:42.120> questions 00:23:44.690 --> 00:23:44.700 align:start position:0% 00:23:44.700 --> 00:23:48.049 align:start position:0% hello<00:23:45.299> uh<00:23:46.140> great<00:23:46.440> great<00:23:46.679> presentation<00:23:47.220> uh<00:23:47.880> I 00:23:48.049 --> 00:23:48.059 align:start position:0% hello uh great great presentation uh I 00:23:48.059 --> 00:23:49.430 align:start position:0% hello uh great great presentation uh I have<00:23:48.179> a<00:23:48.299> couple<00:23:48.419> of<00:23:48.539> questions<00:23:48.780> can<00:23:49.140> you<00:23:49.260> go 00:23:49.430 --> 00:23:49.440 align:start position:0% have a couple of questions can you go 00:23:49.440 --> 00:23:52.130 align:start position:0% have a couple of questions can you go back<00:23:49.620> to<00:23:49.860> the<00:23:50.039> table<00:23:50.220> that<00:23:50.700> you<00:23:50.880> show<00:23:51.120> both<00:23:51.480> uh 00:23:52.130 --> 00:23:52.140 align:start position:0% back to the table that you show both uh 00:23:52.140 --> 00:23:57.049 align:start position:0% back to the table that you show both uh like<00:23:52.919> fasting<00:23:53.640> and<00:23:53.880> symbolic<00:23:54.419> execution 00:23:57.049 --> 00:23:57.059 align:start position:0% 00:23:57.059 --> 00:23:58.789 align:start position:0% I<00:23:57.480> have<00:23:57.600> it<00:23:57.720> on<00:23:57.840> the<00:23:57.960> screen<00:23:58.140> but<00:23:58.380> I<00:23:58.559> don't<00:23:58.679> have 00:23:58.789 --> 00:23:58.799 align:start position:0% I have it on the screen but I don't have 00:23:58.799 --> 00:24:02.990 align:start position:0% I have it on the screen but I don't have it<00:23:58.919> on<00:23:59.100> the<00:23:59.280> projector 00:24:02.990 --> 00:24:03.000 align:start position:0% 00:24:03.000 --> 00:24:03.480 align:start position:0% um 00:24:03.480 --> 00:24:03.490 align:start position:0% um 00:24:03.490 --> 00:24:04.730 align:start position:0% um [Music] 00:24:04.730 --> 00:24:04.740 align:start position:0% [Music] 00:24:04.740 --> 00:24:08.870 align:start position:0% [Music] there<00:24:05.159> it<00:24:05.340> is<00:24:05.460> okay<00:24:06.120> great<00:24:06.720> so<00:24:07.440> you<00:24:08.280> you<00:24:08.580> put 00:24:08.870 --> 00:24:08.880 align:start position:0% there it is okay great so you you put 00:24:08.880 --> 00:24:11.270 align:start position:0% there it is okay great so you you put like<00:24:09.120> in<00:24:09.360> the<00:24:09.539> fasting<00:24:10.020> column<00:24:10.559> that<00:24:11.039> it 00:24:11.270 --> 00:24:11.280 align:start position:0% like in the fasting column that it 00:24:11.280 --> 00:24:14.510 align:start position:0% like in the fasting column that it requires<00:24:11.760> no<00:24:12.179> inter<00:24:12.799> in<00:24:13.799> human<00:24:13.980> intervention 00:24:14.510 --> 00:24:14.520 align:start position:0% requires no inter in human intervention 00:24:14.520 --> 00:24:16.970 align:start position:0% requires no inter in human intervention but<00:24:15.120> you<00:24:15.299> need<00:24:15.480> someone<00:24:15.780> to<00:24:16.260> write<00:24:16.500> the 00:24:16.970 --> 00:24:16.980 align:start position:0% but you need someone to write the 00:24:16.980 --> 00:24:18.649 align:start position:0% but you need someone to write the properties<00:24:17.400> it's<00:24:17.880> the<00:24:18.120> same<00:24:18.240> for<00:24:18.480> the 00:24:18.649 --> 00:24:18.659 align:start position:0% properties it's the same for the 00:24:18.659 --> 00:24:21.710 align:start position:0% properties it's the same for the symbolic<00:24:19.100> execution<00:24:20.100> right<00:24:21.000> so<00:24:21.299> if<00:24:21.480> you<00:24:21.600> have 00:24:21.710 --> 00:24:21.720 align:start position:0% symbolic execution right so if you have 00:24:21.720 --> 00:24:24.350 align:start position:0% symbolic execution right so if you have good<00:24:21.960> properties<00:24:22.380> you<00:24:22.740> will<00:24:22.860> catch<00:24:23.340> good<00:24:23.880> bags 00:24:24.350 --> 00:24:24.360 align:start position:0% good properties you will catch good bags 00:24:24.360 --> 00:24:26.330 align:start position:0% good properties you will catch good bags if<00:24:24.539> you<00:24:24.659> don't<00:24:24.780> have<00:24:24.960> good<00:24:25.260> properties<00:24:25.679> you 00:24:26.330 --> 00:24:26.340 align:start position:0% if you don't have good properties you 00:24:26.340 --> 00:24:28.909 align:start position:0% if you don't have good properties you will<00:24:26.520> have<00:24:26.640> catch<00:24:27.179> no<00:24:27.360> bugs<00:24:27.780> right<00:24:28.020> and<00:24:28.740> this 00:24:28.909 --> 00:24:28.919 align:start position:0% will have catch no bugs right and this 00:24:28.919 --> 00:24:30.890 align:start position:0% will have catch no bugs right and this is<00:24:29.039> the<00:24:29.280> same<00:24:29.460> with<00:24:29.940> the<00:24:30.059> examples<00:24:30.480> that<00:24:30.720> you 00:24:30.890 --> 00:24:30.900 align:start position:0% is the same with the examples that you 00:24:30.900 --> 00:24:34.250 align:start position:0% is the same with the examples that you show<00:24:31.140> like<00:24:31.500> see<00:24:32.280> fasting<00:24:32.760> is<00:24:32.880> not<00:24:33.059> enough<00:24:33.260> uh 00:24:34.250 --> 00:24:34.260 align:start position:0% show like see fasting is not enough uh 00:24:34.260 --> 00:24:36.590 align:start position:0% show like see fasting is not enough uh this<00:24:34.559> code<00:24:34.679> was<00:24:34.919> fast<00:24:35.159> but<00:24:35.520> perhaps<00:24:35.880> they<00:24:36.240> are 00:24:36.590 --> 00:24:36.600 align:start position:0% this code was fast but perhaps they are 00:24:36.600 --> 00:24:40.130 align:start position:0% this code was fast but perhaps they are not<00:24:36.780> using<00:24:37.260> the<00:24:37.679> correct<00:24:38.360> uh<00:24:39.360> properties<00:24:39.780> so 00:24:40.130 --> 00:24:40.140 align:start position:0% not using the correct uh properties so 00:24:40.140 --> 00:24:42.590 align:start position:0% not using the correct uh properties so what<00:24:40.320> is<00:24:40.500> what<00:24:40.799> is<00:24:40.919> your<00:24:41.159> take<00:24:41.400> on<00:24:41.640> this<00:24:41.880> yeah 00:24:42.590 --> 00:24:42.600 align:start position:0% what is what is your take on this yeah 00:24:42.600 --> 00:24:45.409 align:start position:0% what is what is your take on this yeah yeah<00:24:42.780> that's<00:24:43.140> true<00:24:43.380> so<00:24:43.860> uh<00:24:44.460> this<00:24:44.820> is<00:24:44.940> not<00:24:45.179> like 00:24:45.409 --> 00:24:45.419 align:start position:0% yeah that's true so uh this is not like 00:24:45.419 --> 00:24:47.990 align:start position:0% yeah that's true so uh this is not like fully<00:24:45.840> automatic<00:24:46.380> like<00:24:46.620> for<00:24:46.860> example<00:24:47.100> when 00:24:47.990 --> 00:24:48.000 align:start position:0% fully automatic like for example when 00:24:48.000 --> 00:24:49.789 align:start position:0% fully automatic like for example when you<00:24:48.179> run<00:24:48.480> a<00:24:48.659> static<00:24:48.960> analysis<00:24:49.320> tool<00:24:49.620> on<00:24:49.679> your 00:24:49.789 --> 00:24:49.799 align:start position:0% you run a static analysis tool on your 00:24:49.799 --> 00:24:51.649 align:start position:0% you run a static analysis tool on your code<00:24:49.980> base<00:24:50.159> then<00:24:50.760> you<00:24:50.940> essentially<00:24:51.240> have<00:24:51.539> to 00:24:51.649 --> 00:24:51.659 align:start position:0% code base then you essentially have to 00:24:51.659 --> 00:24:53.870 align:start position:0% code base then you essentially have to do<00:24:51.780> nothing<00:24:52.020> you<00:24:52.620> can<00:24:52.679> just<00:24:52.860> like<00:24:53.400> hit<00:24:53.700> a 00:24:53.870 --> 00:24:53.880 align:start position:0% do nothing you can just like hit a 00:24:53.880 --> 00:24:55.490 align:start position:0% do nothing you can just like hit a button<00:24:54.120> and<00:24:54.240> one<00:24:54.419> Slither<00:24:54.720> on<00:24:54.960> your<00:24:55.080> code<00:24:55.260> base 00:24:55.490 --> 00:24:55.500 align:start position:0% button and one Slither on your code base 00:24:55.500 --> 00:24:59.210 align:start position:0% button and one Slither on your code base so<00:24:56.159> for<00:24:56.340> fuzzing<00:24:56.940> you<00:24:57.840> need<00:24:58.200> to<00:24:58.559> write<00:24:58.919> down 00:24:59.210 --> 00:24:59.220 align:start position:0% so for fuzzing you need to write down 00:24:59.220 --> 00:25:02.270 align:start position:0% so for fuzzing you need to write down the<00:24:59.520> tests<00:24:59.820> and<00:25:00.419> like<00:25:00.780> like<00:25:01.380> getting<00:25:01.919> the 00:25:02.270 --> 00:25:02.280 align:start position:0% the tests and like like getting the 00:25:02.280 --> 00:25:05.210 align:start position:0% the tests and like like getting the tests<00:25:02.640> getting<00:25:03.179> the<00:25:03.539> white<00:25:03.960> tests<00:25:04.440> is<00:25:04.679> is<00:25:05.100> a 00:25:05.210 --> 00:25:05.220 align:start position:0% tests getting the white tests is is a 00:25:05.220 --> 00:25:06.890 align:start position:0% tests getting the white tests is is a challenge<00:25:05.400> on<00:25:05.640> its<00:25:05.820> own<00:25:05.880> it's<00:25:06.120> not<00:25:06.299> like<00:25:06.539> it 00:25:06.890 --> 00:25:06.900 align:start position:0% challenge on its own it's not like it 00:25:06.900 --> 00:25:09.830 align:start position:0% challenge on its own it's not like it doesn't<00:25:07.020> come<00:25:07.260> easy<00:25:07.500> it<00:25:07.919> has<00:25:08.220> to<00:25:08.340> be<00:25:08.460> practiced 00:25:09.830 --> 00:25:09.840 align:start position:0% doesn't come easy it has to be practiced 00:25:09.840 --> 00:25:13.490 align:start position:0% doesn't come easy it has to be practiced um<00:25:10.220> and<00:25:11.220> the<00:25:11.760> same<00:25:12.000> is<00:25:12.419> even<00:25:12.659> more<00:25:12.900> to<00:25:13.080> when<00:25:13.380> you 00:25:13.490 --> 00:25:13.500 align:start position:0% um and the same is even more to when you 00:25:13.500 --> 00:25:15.649 align:start position:0% um and the same is even more to when you do<00:25:13.620> symbolic<00:25:14.100> execution 00:25:15.649 --> 00:25:15.659 align:start position:0% do symbolic execution 00:25:15.659 --> 00:25:17.750 align:start position:0% do symbolic execution um because<00:25:16.200> where<00:25:16.620> symbolic<00:25:17.100> execution<00:25:17.520> can 00:25:17.750 --> 00:25:17.760 align:start position:0% um because where symbolic execution can 00:25:17.760 --> 00:25:20.029 align:start position:0% um because where symbolic execution can also<00:25:18.059> can<00:25:18.299> also<00:25:18.539> be<00:25:18.659> a<00:25:18.780> foot<00:25:18.900> gun<00:25:19.140> if<00:25:19.740> you<00:25:19.860> don't 00:25:20.029 --> 00:25:20.039 align:start position:0% also can also be a foot gun if you don't 00:25:20.039 --> 00:25:22.490 align:start position:0% also can also be a foot gun if you don't know<00:25:20.220> how<00:25:20.460> to<00:25:20.580> use<00:25:20.700> it<00:25:20.880> appropriately<00:25:21.500> all 00:25:22.490 --> 00:25:22.500 align:start position:0% know how to use it appropriately all 00:25:22.500 --> 00:25:24.289 align:start position:0% know how to use it appropriately all right<00:25:22.620> yeah<00:25:22.799> yeah<00:25:23.039> definitely<00:25:23.400> and<00:25:23.940> the<00:25:24.179> other 00:25:24.289 --> 00:25:24.299 align:start position:0% right yeah yeah definitely and the other 00:25:24.299 --> 00:25:26.210 align:start position:0% right yeah yeah definitely and the other thing<00:25:24.539> very<00:25:24.720> quickly<00:25:25.020> you<00:25:25.260> put<00:25:25.500> like<00:25:25.679> false 00:25:26.210 --> 00:25:26.220 align:start position:0% thing very quickly you put like false 00:25:26.220 --> 00:25:29.210 align:start position:0% thing very quickly you put like false negatives<00:25:26.580> like<00:25:27.480> on<00:25:27.960> fun<00:25:28.200> on<00:25:28.440> fasting<00:25:28.980> which 00:25:29.210 --> 00:25:29.220 align:start position:0% negatives like on fun on fasting which 00:25:29.220 --> 00:25:31.909 align:start position:0% negatives like on fun on fasting which is<00:25:29.400> which<00:25:30.120> I<00:25:30.360> agree<00:25:30.600> and<00:25:30.960> you<00:25:31.080> put<00:25:31.260> no<00:25:31.559> false 00:25:31.909 --> 00:25:31.919 align:start position:0% is which I agree and you put no false 00:25:31.919 --> 00:25:34.250 align:start position:0% is which I agree and you put no false negative<00:25:32.159> on<00:25:32.400> symbolic<00:25:32.880> execution<00:25:33.480> or 00:25:34.250 --> 00:25:34.260 align:start position:0% negative on symbolic execution or 00:25:34.260 --> 00:25:36.890 align:start position:0% negative on symbolic execution or whatever<00:25:34.440> you<00:25:34.980> said<00:25:35.220> that<00:25:35.880> you<00:25:36.299> could<00:25:36.419> have<00:25:36.600> at 00:25:36.890 --> 00:25:36.900 align:start position:0% whatever you said that you could have at 00:25:36.900 --> 00:25:38.750 align:start position:0% whatever you said that you could have at third<00:25:37.200> state<00:25:37.440> in<00:25:37.799> which<00:25:37.980> you<00:25:38.220> don't<00:25:38.340> know<00:25:38.520> if 00:25:38.750 --> 00:25:38.760 align:start position:0% third state in which you don't know if 00:25:38.760 --> 00:25:40.610 align:start position:0% third state in which you don't know if it's<00:25:38.880> true<00:25:39.120> or<00:25:39.299> is<00:25:39.419> false 00:25:40.610 --> 00:25:40.620 align:start position:0% it's true or is false 00:25:40.620 --> 00:25:42.890 align:start position:0% it's true or is false that<00:25:41.279> sounds<00:25:41.460> like<00:25:41.640> a<00:25:41.880> false<00:25:42.120> negative<00:25:42.480> to<00:25:42.779> me 00:25:42.890 --> 00:25:42.900 align:start position:0% that sounds like a false negative to me 00:25:42.900 --> 00:25:45.470 align:start position:0% that sounds like a false negative to me like<00:25:43.799> you<00:25:44.100> you<00:25:44.220> don't<00:25:44.460> know<00:25:44.640> the<00:25:44.820> answer<00:25:45.000> the 00:25:45.470 --> 00:25:45.480 align:start position:0% like you you don't know the answer the 00:25:45.480 --> 00:25:48.049 align:start position:0% like you you don't know the answer the tool<00:25:45.720> doesn't<00:25:45.840> know<00:25:46.080> the<00:25:46.260> answer<00:25:46.380> so<00:25:46.740> it<00:25:47.460> is<00:25:47.580> it 00:25:48.049 --> 00:25:48.059 align:start position:0% tool doesn't know the answer so it is it 00:25:48.059 --> 00:25:50.870 align:start position:0% tool doesn't know the answer so it is it is<00:25:48.299> like<00:25:48.539> yeah<00:25:48.779> but<00:25:49.080> it<00:25:49.799> doesn't<00:25:49.919> say<00:25:50.220> I 00:25:50.870 --> 00:25:50.880 align:start position:0% is like yeah but it doesn't say I 00:25:50.880 --> 00:25:52.490 align:start position:0% is like yeah but it doesn't say I discharged<00:25:51.480> this<00:25:51.600> proof<00:25:51.900> application<00:25:52.260> and 00:25:52.490 --> 00:25:52.500 align:start position:0% discharged this proof application and 00:25:52.500 --> 00:25:54.049 align:start position:0% discharged this proof application and everything<00:25:52.679> is<00:25:52.980> right<00:25:53.159> it<00:25:53.520> says<00:25:53.760> you<00:25:53.880> I'm 00:25:54.049 --> 00:25:54.059 align:start position:0% everything is right it says you I'm 00:25:54.059 --> 00:25:55.850 align:start position:0% everything is right it says you I'm stuck<00:25:54.299> and<00:25:54.539> that<00:25:54.779> is<00:25:55.440> um<00:25:55.500> you<00:25:55.740> should 00:25:55.850 --> 00:25:55.860 align:start position:0% stuck and that is um you should 00:25:55.860 --> 00:25:58.250 align:start position:0% stuck and that is um you should interpret<00:25:56.460> this<00:25:56.640> as 00:25:58.250 --> 00:25:58.260 align:start position:0% interpret this as 00:25:58.260 --> 00:26:00.590 align:start position:0% interpret this as um I<00:25:58.620> need<00:25:58.799> to<00:25:58.919> put<00:25:59.159> more<00:25:59.460> effort<00:25:59.880> in<00:26:00.480> the 00:26:00.590 --> 00:26:00.600 align:start position:0% um I need to put more effort in the 00:26:00.600 --> 00:26:04.730 align:start position:0% um I need to put more effort in the proof<00:26:00.960> or<00:26:01.140> in<00:26:01.320> the<00:26:01.440> code<00:26:01.620> to<00:26:02.580> get<00:26:02.940> it<00:26:03.120> to<00:26:03.659> like<00:26:04.140> a 00:26:04.730 --> 00:26:04.740 align:start position:0% proof or in the code to get it to like a 00:26:04.740 --> 00:26:06.950 align:start position:0% proof or in the code to get it to like a final<00:26:04.980> state<00:26:05.340> that<00:26:05.640> says<00:26:05.940> true<00:26:06.179> or<00:26:06.360> false<00:26:06.779> yeah 00:26:06.950 --> 00:26:06.960 align:start position:0% final state that says true or false yeah 00:26:06.960 --> 00:26:09.049 align:start position:0% final state that says true or false yeah but<00:26:07.140> it's<00:26:07.320> the<00:26:07.799> same<00:26:07.919> for<00:26:08.100> for<00:26:08.340> fasting<00:26:08.820> when 00:26:09.049 --> 00:26:09.059 align:start position:0% but it's the same for for fasting when 00:26:09.059 --> 00:26:11.570 align:start position:0% but it's the same for for fasting when you<00:26:09.240> when<00:26:09.480> you<00:26:09.659> say<00:26:09.840> like<00:26:10.200> a<00:26:10.440> past<00:26:10.860> like<00:26:11.400> a 00:26:11.570 --> 00:26:11.580 align:start position:0% you when you say like a past like a 00:26:11.580 --> 00:26:14.630 align:start position:0% you when you say like a past like a tested<00:26:12.120> pass<00:26:12.419> it's<00:26:13.380> simply<00:26:13.740> because<00:26:13.980> you 00:26:14.630 --> 00:26:14.640 align:start position:0% tested pass it's simply because you 00:26:14.640 --> 00:26:16.750 align:start position:0% tested pass it's simply because you didn't<00:26:14.820> you<00:26:15.059> didn't<00:26:15.179> put<00:26:15.480> enough<00:26:15.600> enough<00:26:16.140> time 00:26:16.750 --> 00:26:16.760 align:start position:0% didn't you didn't put enough enough time 00:26:16.760 --> 00:26:20.269 align:start position:0% didn't you didn't put enough enough time right<00:26:17.760> to<00:26:18.480> to<00:26:18.840> run<00:26:19.080> it<00:26:19.260> so<00:26:19.440> it's<00:26:19.559> it's<00:26:19.740> a<00:26:20.159> matter 00:26:20.269 --> 00:26:20.279 align:start position:0% right to to run it so it's it's a matter 00:26:20.279 --> 00:26:22.190 align:start position:0% right to to run it so it's it's a matter of<00:26:20.520> interpretation<00:26:21.120> and<00:26:21.360> it's<00:26:21.539> a<00:26:22.020> little 00:26:22.190 --> 00:26:22.200 align:start position:0% of interpretation and it's a little 00:26:22.200 --> 00:26:25.370 align:start position:0% of interpretation and it's a little misleading<00:26:23.179> you<00:26:24.179> could<00:26:24.299> try<00:26:24.659> like<00:26:24.900> passing 00:26:25.370 --> 00:26:25.380 align:start position:0% misleading you could try like passing 00:26:25.380 --> 00:26:26.149 align:start position:0% misleading you could try like passing over 00:26:26.149 --> 00:26:26.159 align:start position:0% over 00:26:26.159 --> 00:26:29.210 align:start position:0% over um<00:26:26.220> like<00:26:27.000> the<00:26:27.240> entire<00:26:27.539> input<00:26:27.900> space<00:26:28.200> and<00:26:29.039> then 00:26:29.210 --> 00:26:29.220 align:start position:0% um like the entire input space and then 00:26:29.220 --> 00:26:31.850 align:start position:0% um like the entire input space and then you<00:26:29.700> will<00:26:29.820> also<00:26:30.120> have<00:26:30.299> like<00:26:30.600> no<00:26:30.840> false<00:26:31.320> uh<00:26:31.620> no 00:26:31.850 --> 00:26:31.860 align:start position:0% you will also have like no false uh no 00:26:31.860 --> 00:26:34.250 align:start position:0% you will also have like no false uh no false<00:26:32.220> negatives<00:26:32.580> you<00:26:33.059> could<00:26:33.179> try<00:26:33.480> that<00:26:33.720> but 00:26:34.250 --> 00:26:34.260 align:start position:0% false negatives you could try that but 00:26:34.260 --> 00:26:36.830 align:start position:0% false negatives you could try that but like<00:26:34.500> you<00:26:34.860> will<00:26:34.980> never<00:26:35.159> terminate<00:26:35.700> like<00:26:36.059> uh 00:26:36.830 --> 00:26:36.840 align:start position:0% like you will never terminate like uh 00:26:36.840 --> 00:26:39.289 align:start position:0% like you will never terminate like uh but<00:26:37.500> but<00:26:37.679> that<00:26:37.980> would<00:26:38.159> work<00:26:38.400> yeah<00:26:38.580> come<00:26:39.000> to<00:26:39.179> my 00:26:39.289 --> 00:26:39.299 align:start position:0% but but that would work yeah come to my 00:26:39.299 --> 00:26:41.149 align:start position:0% but but that would work yeah come to my talk<00:26:39.539> tomorrow<00:26:39.779> because<00:26:40.200> we'll<00:26:40.440> be<00:26:40.559> be<00:26:40.980> going 00:26:41.149 --> 00:26:41.159 align:start position:0% talk tomorrow because we'll be be going 00:26:41.159 --> 00:26:42.710 align:start position:0% talk tomorrow because we'll be be going over<00:26:41.279> how<00:26:41.520> to<00:26:41.700> write<00:26:41.820> properties<00:26:42.240> that's 00:26:42.710 --> 00:26:42.720 align:start position:0% over how to write properties that's 00:26:42.720 --> 00:26:46.460 align:start position:0% over how to write properties that's basically<00:26:43.200> the<00:26:43.380> next<00:26:43.559> talk 00:26:46.460 --> 00:26:46.470 align:start position:0% 00:26:46.470 --> 00:26:49.819 align:start position:0% [Music]