WEBVTT Kind: captions Language: en 00:00:01.070 --> 00:00:13.850 align:start position:0% [Applause] 00:00:13.850 --> 00:00:13.860 align:start position:0% 00:00:13.860 --> 00:00:17.850 align:start position:0% all<00:00:14.860> right<00:00:15.160> welcome<00:00:15.700> everyone<00:00:16.830> we're<00:00:17.830> about 00:00:17.850 --> 00:00:17.860 align:start position:0% all right welcome everyone we're about 00:00:17.860 --> 00:00:22.740 align:start position:0% all right welcome everyone we're about to<00:00:18.130> kick<00:00:18.580> off<00:00:21.090> we're<00:00:22.090> going<00:00:22.240> to<00:00:22.330> be<00:00:22.420> conducting 00:00:22.740 --> 00:00:22.750 align:start position:0% to kick off we're going to be conducting 00:00:22.750 --> 00:00:27.780 align:start position:0% to kick off we're going to be conducting today<00:00:23.400> for<00:00:24.400> your<00:00:24.520> very<00:00:24.760> eyes<00:00:25.000> a<00:00:26.790> competition 00:00:27.780 --> 00:00:27.790 align:start position:0% today for your very eyes a competition 00:00:27.790 --> 00:00:30.090 align:start position:0% today for your very eyes a competition in<00:00:28.029> golf<00:00:28.320> around<00:00:29.320> the<00:00:29.439> Gulf<00:00:29.619> you<00:00:29.770> might<00:00:29.920> say 00:00:30.090 --> 00:00:30.100 align:start position:0% in golf around the Gulf you might say 00:00:30.100 --> 00:00:32.810 align:start position:0% in golf around the Gulf you might say that<00:00:30.910> will<00:00:31.119> also<00:00:31.420> be<00:00:31.510> form<00:00:31.780> of<00:00:31.869> the<00:00:31.930> red<00:00:32.080> pipe 00:00:32.810 --> 00:00:32.820 align:start position:0% that will also be form of the red pipe 00:00:32.820 --> 00:00:37.049 align:start position:0% that will also be form of the red pipe so<00:00:33.820> we're<00:00:34.270> rewriting<00:00:34.510> smart<00:00:34.900> contracts<00:00:35.879> and<00:00:36.879> I 00:00:37.049 --> 00:00:37.059 align:start position:0% so we're rewriting smart contracts and I 00:00:37.059 --> 00:00:40.560 align:start position:0% so we're rewriting smart contracts and I never<00:00:37.210> like<00:00:37.449> what<00:00:37.570> you<00:00:37.720> prefer<00:00:37.920> and<00:00:39.570> you'll 00:00:40.560 --> 00:00:40.570 align:start position:0% never like what you prefer and you'll 00:00:40.570 --> 00:00:44.670 align:start position:0% never like what you prefer and you'll submit<00:00:40.930> submit<00:00:41.920> your<00:00:42.250> effects<00:00:42.790> to<00:00:43.030> our<00:00:43.680> CI 00:00:44.670 --> 00:00:44.680 align:start position:0% submit submit your effects to our CI 00:00:44.680 --> 00:00:48.000 align:start position:0% submit submit your effects to our CI server<00:00:44.860> which<00:00:45.640> will<00:00:45.850> run<00:00:46.570> a<00:00:46.600> suite<00:00:47.019> of<00:00:47.290> formal 00:00:48.000 --> 00:00:48.010 align:start position:0% server which will run a suite of formal 00:00:48.010 --> 00:00:50.670 align:start position:0% server which will run a suite of formal verification<00:00:48.330> proofs<00:00:49.330> against<00:00:49.900> that<00:00:50.500> white 00:00:50.670 --> 00:00:50.680 align:start position:0% verification proofs against that white 00:00:50.680 --> 00:00:54.540 align:start position:0% verification proofs against that white coat<00:00:50.979> and<00:00:52.500> if<00:00:53.500> you<00:00:53.680> do<00:00:53.830> manage<00:00:54.070> to<00:00:54.190> pass 00:00:54.540 --> 00:00:54.550 align:start position:0% coat and if you do manage to pass 00:00:54.550 --> 00:00:56.610 align:start position:0% coat and if you do manage to pass perspex<00:00:55.000> we<00:00:55.180> have<00:00:55.390> approval<00:00:56.019> incorrect 00:00:56.610 --> 00:00:56.620 align:start position:0% perspex we have approval incorrect 00:00:56.620 --> 00:00:59.549 align:start position:0% perspex we have approval incorrect contracts<00:00:57.420> then<00:00:58.420> there's<00:00:58.870> a<00:00:58.960> competition<00:00:59.260> for 00:00:59.549 --> 00:00:59.559 align:start position:0% contracts then there's a competition for 00:00:59.559 --> 00:01:02.219 align:start position:0% contracts then there's a competition for making<00:01:00.129> the<00:01:00.640> most<00:01:00.790> gas<00:01:01.120> efficient<00:01:01.659> that's<00:01:02.080> a 00:01:02.219 --> 00:01:02.229 align:start position:0% making the most gas efficient that's a 00:01:02.229 --> 00:01:04.920 align:start position:0% making the most gas efficient that's a contract<00:01:03.120> and<00:01:04.120> in<00:01:04.299> particular<00:01:04.659> we'll<00:01:04.839> be 00:01:04.920 --> 00:01:04.930 align:start position:0% contract and in particular we'll be 00:01:04.930 --> 00:01:08.990 align:start position:0% contract and in particular we'll be doing<00:01:05.260> it<00:01:05.740> today<00:01:06.100> with<00:01:06.700> an<00:01:06.850> ESD<00:01:07.150> twenty<00:01:07.540> cents 00:01:08.990 --> 00:01:09.000 align:start position:0% doing it today with an ESD twenty cents 00:01:09.000 --> 00:01:10.800 align:start position:0% doing it today with an ESD twenty cents this<00:01:10.000> is<00:01:10.150> the<00:01:10.240> month<00:01:10.450> where<00:01:10.570> the<00:01:10.630> most 00:01:10.800 --> 00:01:10.810 align:start position:0% this is the month where the most 00:01:10.810 --> 00:01:14.000 align:start position:0% this is the month where the most straightforward<00:01:11.340> specification<00:01:12.340> of<00:01:12.549> course 00:01:14.000 --> 00:01:14.010 align:start position:0% straightforward specification of course 00:01:14.010 --> 00:01:16.530 align:start position:0% straightforward specification of course there's<00:01:15.010> some<00:01:15.190> caveats<00:01:15.430> on<00:01:15.820> what<00:01:16.420> the 00:01:16.530 --> 00:01:16.540 align:start position:0% there's some caveats on what the 00:01:16.540 --> 00:01:18.090 align:start position:0% there's some caveats on what the specification<00:01:16.960> actually<00:01:17.380> looks<00:01:17.620> like<00:01:17.800> were 00:01:18.090 --> 00:01:18.100 align:start position:0% specification actually looks like were 00:01:18.100 --> 00:01:19.890 align:start position:0% specification actually looks like were made<00:01:18.340> a<00:01:18.580> little<00:01:19.030> bit<00:01:19.210> of<00:01:19.270> an<00:01:19.450> opinionated 00:01:19.890 --> 00:01:19.900 align:start position:0% made a little bit of an opinionated 00:01:19.900 --> 00:01:22.230 align:start position:0% made a little bit of an opinionated choice<00:01:20.260> here<00:01:20.500> we'll<00:01:21.490> go<00:01:21.640> over<00:01:21.700> that<00:01:21.910> at<00:01:22.090> their 00:01:22.230 --> 00:01:22.240 align:start position:0% choice here we'll go over that at their 00:01:22.240 --> 00:01:28.830 align:start position:0% choice here we'll go over that at their time<00:01:24.120> so<00:01:26.910> when<00:01:27.910> I<00:01:27.940> said<00:01:28.210> that<00:01:28.480> we'll<00:01:28.600> be<00:01:28.690> doing 00:01:28.830 --> 00:01:28.840 align:start position:0% time so when I said that we'll be doing 00:01:28.840 --> 00:01:30.870 align:start position:0% time so when I said that we'll be doing a<00:01:29.320> competition<00:01:29.680> actually<00:01:30.400> met<00:01:30.580> we'll<00:01:30.760> be 00:01:30.870 --> 00:01:30.880 align:start position:0% a competition actually met we'll be 00:01:30.880 --> 00:01:34.490 align:start position:0% a competition actually met we'll be doing<00:01:31.090> two<00:01:31.270> competitions<00:01:32.550> at<00:01:33.550> the<00:01:33.580> same<00:01:33.910> time 00:01:34.490 --> 00:01:34.500 align:start position:0% doing two competitions at the same time 00:01:34.500 --> 00:01:37.380 align:start position:0% doing two competitions at the same time namely<00:01:35.500> there's<00:01:35.860> this<00:01:36.070> Ian<00:01:36.850> golf<00:01:37.120> competition 00:01:37.380 --> 00:01:37.390 align:start position:0% namely there's this Ian golf competition 00:01:37.390 --> 00:01:39.490 align:start position:0% namely there's this Ian golf competition that<00:01:37.840> I<00:01:37.870> just<00:01:38.080> described 00:01:39.490 --> 00:01:39.500 align:start position:0% that I just described 00:01:39.500 --> 00:01:43.279 align:start position:0% that I just described hoo-wee<00:01:40.500> correct<00:01:40.860> coz<00:01:41.280> 20<00:01:41.610> permutation<00:01:42.289> but 00:01:43.279 --> 00:01:43.289 align:start position:0% hoo-wee correct coz 20 permutation but 00:01:43.289 --> 00:01:45.679 align:start position:0% hoo-wee correct coz 20 permutation but there<00:01:43.409> is<00:01:43.500> actually<00:01:43.649> a<00:01:43.920> second<00:01:44.340> contest<00:01:44.789> going 00:01:45.679 --> 00:01:45.689 align:start position:0% there is actually a second contest going 00:01:45.689 --> 00:01:47.270 align:start position:0% there is actually a second contest going on<00:01:45.780> behind<00:01:46.020> the<00:01:46.229> scenes<00:01:46.289> and<00:01:46.740> if<00:01:47.039> you're 00:01:47.270 --> 00:01:47.280 align:start position:0% on behind the scenes and if you're 00:01:47.280 --> 00:01:51.080 align:start position:0% on behind the scenes and if you're feeling<00:01:48.560> like<00:01:49.560> the<00:01:49.920> first<00:01:50.159> one<00:01:50.369> might<00:01:50.729> not<00:01:50.909> be 00:01:51.080 --> 00:01:51.090 align:start position:0% feeling like the first one might not be 00:01:51.090 --> 00:01:52.550 align:start position:0% feeling like the first one might not be too<00:01:51.420> much<00:01:51.600> of<00:01:51.719> a<00:01:51.780> challenge<00:01:51.960> for<00:01:52.170> you<00:01:52.439> were 00:01:52.550 --> 00:01:52.560 align:start position:0% too much of a challenge for you were 00:01:52.560 --> 00:01:55.389 align:start position:0% too much of a challenge for you were here<00:01:52.890> thinking<00:01:53.759> that<00:01:53.789> formal<00:01:54.270> education<00:01:54.329> is 00:01:55.389 --> 00:01:55.399 align:start position:0% here thinking that formal education is 00:01:55.399 --> 00:02:00.289 align:start position:0% here thinking that formal education is just<00:01:56.399> a<00:01:56.970> sham<00:01:57.710> then<00:01:58.710> you<00:01:59.579> can<00:01:59.729> participate<00:01:59.880> in 00:02:00.289 --> 00:02:00.299 align:start position:0% just a sham then you can participate in 00:02:00.299 --> 00:02:03.190 align:start position:0% just a sham then you can participate in the<00:02:00.420> second<00:02:00.750> competition<00:02:01.229> which<00:02:01.590> asks<00:02:02.189> you<00:02:02.399> to 00:02:03.190 --> 00:02:03.200 align:start position:0% the second competition which asks you to 00:02:03.200 --> 00:02:06.919 align:start position:0% the second competition which asks you to submit<00:02:04.200> bytecode<00:02:04.920> that<00:02:05.880> has<00:02:06.509> some<00:02:06.689> sort<00:02:06.899> of 00:02:06.919 --> 00:02:06.929 align:start position:0% submit bytecode that has some sort of 00:02:06.929 --> 00:02:10.369 align:start position:0% submit bytecode that has some sort of bug<00:02:07.200> in<00:02:07.380> it<00:02:08.000> but<00:02:09.000> it<00:02:09.090> still<00:02:09.360> passive<00:02:09.899> suspects 00:02:10.369 --> 00:02:10.379 align:start position:0% bug in it but it still passive suspects 00:02:10.379 --> 00:02:11.900 align:start position:0% bug in it but it still passive suspects somehow<00:02:10.739> if<00:02:10.920> you<00:02:10.950> believe<00:02:11.310> that<00:02:11.340> the<00:02:11.610> specs 00:02:11.900 --> 00:02:11.910 align:start position:0% somehow if you believe that the specs 00:02:11.910 --> 00:02:13.789 align:start position:0% somehow if you believe that the specs and<00:02:12.150> the<00:02:12.360> methods<00:02:12.750> that<00:02:12.870> we<00:02:13.110> have<00:02:13.290> created 00:02:13.789 --> 00:02:13.799 align:start position:0% and the methods that we have created 00:02:13.799 --> 00:02:17.600 align:start position:0% and the methods that we have created with<00:02:14.459> the<00:02:15.739> formal<00:02:16.739> verification<00:02:16.890> process 00:02:17.600 --> 00:02:17.610 align:start position:0% with the formal verification process 00:02:17.610 --> 00:02:21.069 align:start position:0% with the formal verification process that<00:02:17.790> has<00:02:17.910> been<00:02:17.940> set<00:02:18.390> up<00:02:18.680> then<00:02:19.680> you<00:02:20.220> can<00:02:20.400> try<00:02:20.579> to 00:02:21.069 --> 00:02:21.079 align:start position:0% that has been set up then you can try to 00:02:21.079 --> 00:02:23.750 align:start position:0% that has been set up then you can try to fool<00:02:22.079> it<00:02:22.290> and<00:02:22.530> you<00:02:22.620> can<00:02:22.739> try<00:02:22.920> to<00:02:22.950> submit<00:02:23.459> might 00:02:23.750 --> 00:02:23.760 align:start position:0% fool it and you can try to submit might 00:02:23.760 --> 00:02:25.610 align:start position:0% fool it and you can try to submit might go<00:02:23.970> that<00:02:24.209> fast<00:02:24.720> those<00:02:25.079> effects<00:02:25.380> butter 00:02:25.610 --> 00:02:25.620 align:start position:0% go that fast those effects butter 00:02:25.620 --> 00:02:29.330 align:start position:0% go that fast those effects butter otherwise<00:02:26.599> faulty<00:02:27.599> in<00:02:27.870> some<00:02:28.110> way<00:02:28.260> I<00:02:28.500> mean<00:02:28.739> this 00:02:29.330 --> 00:02:29.340 align:start position:0% otherwise faulty in some way I mean this 00:02:29.340 --> 00:02:32.059 align:start position:0% otherwise faulty in some way I mean this hard<00:02:29.579> to<00:02:29.670> define<00:02:29.910> one<00:02:30.680> there's<00:02:31.680> no<00:02:31.860> longer 00:02:32.059 --> 00:02:32.069 align:start position:0% hard to define one there's no longer 00:02:32.069 --> 00:02:34.309 align:start position:0% hard to define one there's no longer expect<00:02:32.459> to<00:02:32.579> talk<00:02:32.730> about<00:02:32.910> but<00:02:33.329> I'm<00:02:33.900> sure<00:02:33.959> we'll 00:02:34.309 --> 00:02:34.319 align:start position:0% expect to talk about but I'm sure we'll 00:02:34.319 --> 00:02:36.460 align:start position:0% expect to talk about but I'm sure we'll be<00:02:34.440> able<00:02:34.470> to<00:02:34.709> figure<00:02:34.920> something<00:02:35.190> out<00:02:35.370> so 00:02:36.460 --> 00:02:36.470 align:start position:0% be able to figure something out so 00:02:36.470 --> 00:02:38.690 align:start position:0% be able to figure something out so you'll<00:02:37.470> be<00:02:37.590> able<00:02:37.650> to<00:02:37.829> compete<00:02:38.099> in<00:02:38.280> both<00:02:38.549> of 00:02:38.690 --> 00:02:38.700 align:start position:0% you'll be able to compete in both of 00:02:38.700 --> 00:02:41.509 align:start position:0% you'll be able to compete in both of these<00:02:38.790> competitions<00:02:39.599> and<00:02:40.130> we'll<00:02:41.130> get<00:02:41.250> to<00:02:41.400> the 00:02:41.509 --> 00:02:41.519 align:start position:0% these competitions and we'll get to the 00:02:41.519 --> 00:02:45.920 align:start position:0% these competitions and we'll get to the details<00:02:43.850> first<00:02:44.850> I'm<00:02:45.420> not<00:02:45.480> going<00:02:45.810> to<00:02:45.870> be 00:02:45.920 --> 00:02:45.930 align:start position:0% details first I'm not going to be 00:02:45.930 --> 00:02:48.890 align:start position:0% details first I'm not going to be talking<00:02:46.049> too<00:02:46.350> much<00:02:46.380> about<00:02:47.420> the<00:02:48.420> theory<00:02:48.720> behind 00:02:48.890 --> 00:02:48.900 align:start position:0% talking too much about the theory behind 00:02:48.900 --> 00:02:51.650 align:start position:0% talking too much about the theory behind what<00:02:49.230> we're<00:02:49.410> doing<00:02:49.590> today<00:02:49.739> because<00:02:50.250> we<00:02:51.239> need 00:02:51.650 --> 00:02:51.660 align:start position:0% what we're doing today because we need 00:02:51.660 --> 00:02:55.569 align:start position:0% what we're doing today because we need to<00:02:51.840> have<00:02:51.989> time<00:02:52.230> to<00:02:52.470> actually<00:02:52.620> do<00:02:53.100> some<00:02:53.639> hacking 00:02:55.569 --> 00:02:55.579 align:start position:0% to have time to actually do some hacking 00:02:55.579 --> 00:03:01.009 align:start position:0% to have time to actually do some hacking but<00:02:56.579> let<00:02:56.850> me<00:02:56.940> just<00:02:56.970> mention<00:02:57.299> that<00:02:58.730> the<00:03:00.019> proving 00:03:01.009 --> 00:03:01.019 align:start position:0% but let me just mention that the proving 00:03:01.019 --> 00:03:02.599 align:start position:0% but let me just mention that the proving methods<00:03:01.350> that<00:03:01.500> were<00:03:01.650> using<00:03:01.829> here<00:03:02.280> for<00:03:02.340> this 00:03:02.599 --> 00:03:02.609 align:start position:0% methods that were using here for this 00:03:02.609 --> 00:03:04.430 align:start position:0% methods that were using here for this workshop<00:03:03.030> we're<00:03:03.720> gonna<00:03:03.840> be<00:03:03.930> using<00:03:04.109> the 00:03:04.430 --> 00:03:04.440 align:start position:0% workshop we're gonna be using the 00:03:04.440 --> 00:03:08.629 align:start position:0% workshop we're gonna be using the catering<00:03:04.859> work<00:03:05.600> and<00:03:06.680> we'll<00:03:07.680> be<00:03:07.829> writing<00:03:08.250> our 00:03:08.629 --> 00:03:08.639 align:start position:0% catering work and we'll be writing our 00:03:08.639 --> 00:03:11.319 align:start position:0% catering work and we'll be writing our specs<00:03:09.000> without<00:03:09.389> looking<00:03:09.690> at<00:03:09.810> her<00:03:09.900> specs 00:03:11.319 --> 00:03:11.329 align:start position:0% specs without looking at her specs 00:03:11.329 --> 00:03:15.620 align:start position:0% specs without looking at her specs written<00:03:12.329> in<00:03:12.569> the<00:03:13.560> act<00:03:14.120> smart<00:03:15.120> contracts 00:03:15.620 --> 00:03:15.630 align:start position:0% written in the act smart contracts 00:03:15.630 --> 00:03:19.700 align:start position:0% written in the act smart contracts specification<00:03:16.350> language<00:03:16.680> we'll<00:03:17.280> get<00:03:17.459> it 00:03:19.700 --> 00:03:19.710 align:start position:0% 00:03:19.710 --> 00:03:23.550 align:start position:0% okay<00:03:20.710> so<00:03:20.940> let's<00:03:21.940> get<00:03:22.900> deeper<00:03:23.230> into<00:03:23.350> the 00:03:23.550 --> 00:03:23.560 align:start position:0% okay so let's get deeper into the 00:03:23.560 --> 00:03:31.010 align:start position:0% okay so let's get deeper into the specification<00:03:23.920> I'll<00:03:24.490> come<00:03:24.700> over<00:03:24.790> to<00:03:25.060> God<00:03:25.270> soon 00:03:31.010 --> 00:03:31.020 align:start position:0% 00:03:31.020 --> 00:03:37.220 align:start position:0% so<00:03:32.550> sometimes<00:03:33.550> people<00:03:33.850> say<00:03:34.630> that<00:03:35.040> NERC<00:03:36.040> 20 00:03:37.220 --> 00:03:37.230 align:start position:0% so sometimes people say that NERC 20 00:03:37.230 --> 00:03:40.200 align:start position:0% so sometimes people say that NERC 20 yearsI<00:03:38.230> 20<00:03:38.530> specification<00:03:39.250> as<00:03:39.400> evidence<00:03:40.060> or 00:03:40.200 --> 00:03:40.210 align:start position:0% yearsI 20 specification as evidence or 00:03:40.210 --> 00:03:43.100 align:start position:0% yearsI 20 specification as evidence or sort<00:03:40.420> of<00:03:40.510> Express<00:03:40.900> panel<00:03:41.260> it's<00:03:42.100> really<00:03:42.460> not 00:03:43.100 --> 00:03:43.110 align:start position:0% sort of Express panel it's really not 00:03:43.110 --> 00:03:45.600 align:start position:0% sort of Express panel it's really not it's<00:03:44.110> more<00:03:44.320> of<00:03:44.380> an<00:03:44.470> interface<00:03:44.860> that<00:03:45.310> really 00:03:45.600 --> 00:03:45.610 align:start position:0% it's more of an interface that really 00:03:45.610 --> 00:03:49.380 align:start position:0% it's more of an interface that really just<00:03:45.820> tells<00:03:46.330> you<00:03:46.660> what<00:03:47.700> the<00:03:48.700> methods<00:03:49.120> should 00:03:49.380 --> 00:03:49.390 align:start position:0% just tells you what the methods should 00:03:49.390 --> 00:03:52.830 align:start position:0% just tells you what the methods should look<00:03:49.600> like<00:03:50.310> in<00:03:51.310> your<00:03:51.520> contract<00:03:52.030> and<00:03:52.210> doesn't 00:03:52.830 --> 00:03:52.840 align:start position:0% look like in your contract and doesn't 00:03:52.840 --> 00:03:54.210 align:start position:0% look like in your contract and doesn't actually<00:03:52.930> say<00:03:53.290> anything<00:03:53.320> about<00:03:53.710> the<00:03:53.890> behavior 00:03:54.210 --> 00:03:54.220 align:start position:0% actually say anything about the behavior 00:03:54.220 --> 00:03:56.430 align:start position:0% actually say anything about the behavior of<00:03:54.250> course<00:03:54.520> I<00:03:54.760> mean<00:03:54.880> we<00:03:55.000> have<00:03:55.180> some<00:03:55.450> intuition 00:03:56.430 --> 00:03:56.440 align:start position:0% of course I mean we have some intuition 00:03:56.440 --> 00:03:58.410 align:start position:0% of course I mean we have some intuition around<00:03:56.890> what<00:03:57.070> this<00:03:57.250> should<00:03:57.490> be<00:03:57.730> but<00:03:58.120> there's 00:03:58.410 --> 00:03:58.420 align:start position:0% around what this should be but there's 00:03:58.420 --> 00:04:00.720 align:start position:0% around what this should be but there's actually<00:03:58.750> a<00:03:59.080> whole<00:03:59.430> range<00:04:00.430> of<00:04:00.670> different 00:04:00.720 --> 00:04:00.730 align:start position:0% actually a whole range of different 00:04:00.730 --> 00:04:05.880 align:start position:0% actually a whole range of different types<00:04:01.390> of<00:04:01.570> behavior<00:04:03.960> of<00:04:04.960> difference<00:04:05.470> here<00:04:05.710> see 00:04:05.880 --> 00:04:05.890 align:start position:0% types of behavior of difference here see 00:04:05.890 --> 00:04:07.680 align:start position:0% types of behavior of difference here see 20<00:04:06.130> tokens<00:04:06.520> and<00:04:06.730> it<00:04:06.820> gets<00:04:06.970> kind<00:04:07.420> of<00:04:07.570> annoying 00:04:07.680 --> 00:04:07.690 align:start position:0% 20 tokens and it gets kind of annoying 00:04:07.690 --> 00:04:09.870 align:start position:0% 20 tokens and it gets kind of annoying when<00:04:08.170> you<00:04:08.260> start<00:04:08.530> dealing<00:04:09.160> with<00:04:09.370> them<00:04:09.640> and 00:04:09.870 --> 00:04:09.880 align:start position:0% when you start dealing with them and 00:04:09.880 --> 00:04:11.940 align:start position:0% when you start dealing with them and then<00:04:10.000> you<00:04:10.120> have<00:04:10.240> to<00:04:10.360> check<00:04:10.540> whether<00:04:10.950> this 00:04:11.940 --> 00:04:11.950 align:start position:0% then you have to check whether this 00:04:11.950 --> 00:04:13.920 align:start position:0% then you have to check whether this particular<00:04:12.220> is<00:04:12.670> a<00:04:12.820> 20<00:04:13.210> you<00:04:13.360> actually<00:04:13.750> did 00:04:13.920 --> 00:04:13.930 align:start position:0% particular is a 20 you actually did 00:04:13.930 --> 00:04:15.630 align:start position:0% particular is a 20 you actually did return<00:04:14.290> a<00:04:14.530> boolean<00:04:14.710> at<00:04:15.100> the<00:04:15.250> end<00:04:15.370> of<00:04:15.490> its 00:04:15.630 --> 00:04:15.640 align:start position:0% return a boolean at the end of its 00:04:15.640 --> 00:04:17.640 align:start position:0% return a boolean at the end of its transfer<00:04:16.359> function<00:04:16.450> anymore<00:04:16.930> what's 00:04:17.640 --> 00:04:17.650 align:start position:0% transfer function anymore what's 00:04:17.650 --> 00:04:19.289 align:start position:0% transfer function anymore what's happening<00:04:18.130> in<00:04:18.310> the<00:04:18.430> case<00:04:18.609> where<00:04:19.000> you're 00:04:19.289 --> 00:04:19.299 align:start position:0% happening in the case where you're 00:04:19.299 --> 00:04:23.310 align:start position:0% happening in the case where you're sending<00:04:19.660> to<00:04:19.690> the<00:04:19.930> 0<00:04:20.230> is<00:04:20.280> not<00:04:21.280> like<00:04:21.430> this<00:04:21.549> so<00:04:22.320> in 00:04:23.310 --> 00:04:23.320 align:start position:0% sending to the 0 is not like this so in 00:04:23.320 --> 00:04:24.810 align:start position:0% sending to the 0 is not like this so in order<00:04:23.440> to<00:04:23.620> actually<00:04:23.740> have<00:04:24.100> a<00:04:24.130> specification 00:04:24.810 --> 00:04:24.820 align:start position:0% order to actually have a specification 00:04:24.820 --> 00:04:27.720 align:start position:0% order to actually have a specification we<00:04:25.030> need<00:04:25.450> to<00:04:25.690> make<00:04:26.590> a<00:04:26.860> choice<00:04:27.130> on<00:04:27.430> all<00:04:27.580> these 00:04:27.720 --> 00:04:27.730 align:start position:0% we need to make a choice on all these 00:04:27.730 --> 00:04:32.490 align:start position:0% we need to make a choice on all these decisions<00:04:29.430> and<00:04:30.690> neighbors<00:04:31.690> have<00:04:31.840> our<00:04:32.169> choices 00:04:32.490 --> 00:04:32.500 align:start position:0% decisions and neighbors have our choices 00:04:32.500 --> 00:04:37.500 align:start position:0% decisions and neighbors have our choices but<00:04:33.070> before<00:04:33.370> I<00:04:33.400> do<00:04:33.490> that<00:04:36.060> I'm<00:04:37.060> going<00:04:37.300> to<00:04:37.360> show 00:04:37.500 --> 00:04:37.510 align:start position:0% but before I do that I'm going to show 00:04:37.510 --> 00:04:40.080 align:start position:0% but before I do that I'm going to show you<00:04:37.950> the<00:04:38.950> language<00:04:39.160> in<00:04:39.520> which<00:04:39.640> we're 00:04:40.080 --> 00:04:40.090 align:start position:0% you the language in which we're 00:04:40.090 --> 00:04:42.950 align:start position:0% you the language in which we're presenting<00:04:40.630> these<00:04:40.780> choices<00:04:41.530> so<00:04:41.890> this<00:04:42.460> is<00:04:42.610> our 00:04:42.950 --> 00:04:42.960 align:start position:0% presenting these choices so this is our 00:04:42.960 --> 00:04:47.700 align:start position:0% presenting these choices so this is our specification<00:04:44.040> formats<00:04:45.040> that<00:04:46.560> we<00:04:47.560> have 00:04:47.700 --> 00:04:47.710 align:start position:0% specification formats that we have 00:04:47.710 --> 00:04:52.680 align:start position:0% specification formats that we have developed<00:04:47.980> in<00:04:48.520> order<00:04:48.760> to<00:04:49.090> be<00:04:51.690> literate 00:04:52.680 --> 00:04:52.690 align:start position:0% developed in order to be literate 00:04:52.690 --> 00:04:55.080 align:start position:0% developed in order to be literate language<00:04:53.080> that<00:04:53.500> should<00:04:54.430> be<00:04:54.700> intuitively 00:04:55.080 --> 00:04:55.090 align:start position:0% language that should be intuitively 00:04:55.090 --> 00:04:57.090 align:start position:0% language that should be intuitively makes<00:04:55.390> sense<00:04:55.660> users<00:04:56.169> you<00:04:56.470> know<00:04:56.560> common 00:04:57.090 --> 00:04:57.100 align:start position:0% makes sense users you know common 00:04:57.100 --> 00:05:02.790 align:start position:0% makes sense users you know common mathematical<00:04:57.990> works<00:04:58.990> and<00:05:01.230> we<00:05:02.230> have<00:05:02.410> created 00:05:02.790 --> 00:05:02.800 align:start position:0% mathematical works and we have created 00:05:02.800 --> 00:05:05.220 align:start position:0% mathematical works and we have created it<00:05:02.890> in<00:05:03.010> such<00:05:03.220> a<00:05:03.250> way<00:05:03.340> that<00:05:03.750> from<00:05:04.750> a<00:05:04.780> small 00:05:05.220 --> 00:05:05.230 align:start position:0% it in such a way that from a small 00:05:05.230 --> 00:05:06.220 align:start position:0% it in such a way that from a small specification<00:05:05.919> like 00:05:06.220 --> 00:05:06.230 align:start position:0% specification like 00:05:06.230 --> 00:05:09.420 align:start position:0% specification like we<00:05:06.440> should<00:05:06.620> be<00:05:06.770> able<00:05:06.830> to<00:05:06.980> generate<00:05:07.220> a<00:05:07.790> suite<00:05:08.240> of 00:05:09.420 --> 00:05:09.430 align:start position:0% we should be able to generate a suite of 00:05:09.430 --> 00:05:13.080 align:start position:0% we should be able to generate a suite of reachability<00:05:10.430> claims<00:05:10.880> so<00:05:11.800> proof<00:05:12.800> obligations 00:05:13.080 --> 00:05:13.090 align:start position:0% reachability claims so proof obligations 00:05:13.090 --> 00:05:17.230 align:start position:0% reachability claims so proof obligations essentially<00:05:14.090> that<00:05:14.570> you<00:05:15.140> can<00:05:15.350> port<00:05:15.680> to<00:05:16.240> right 00:05:17.230 --> 00:05:17.240 align:start position:0% essentially that you can port to right 00:05:17.240 --> 00:05:18.960 align:start position:0% essentially that you can port to right now<00:05:17.360> okay<00:05:17.780> but<00:05:17.990> there<00:05:18.140> are<00:05:18.260> more<00:05:18.380> back<00:05:18.620> ends 00:05:18.960 --> 00:05:18.970 align:start position:0% now okay but there are more back ends 00:05:18.970 --> 00:05:24.040 align:start position:0% now okay but there are more back ends and<00:05:19.970> we're<00:05:20.120> planning<00:05:21.610> and<00:05:22.610> so<00:05:22.970> let<00:05:23.840> me<00:05:23.870> show 00:05:24.040 --> 00:05:24.050 align:start position:0% and we're planning and so let me show 00:05:24.050 --> 00:05:29.380 align:start position:0% and we're planning and so let me show you<00:05:24.080> how<00:05:24.290> this<00:05:24.410> works<00:05:26.140> we<00:05:27.140> have<00:05:28.060> on<00:05:29.060> the<00:05:29.210> left 00:05:29.380 --> 00:05:29.390 align:start position:0% you how this works we have on the left 00:05:29.390 --> 00:05:31.690 align:start position:0% you how this works we have on the left hand<00:05:29.540> side<00:05:29.750> we<00:05:29.900> have<00:05:30.050> the<00:05:30.140> specification<00:05:30.800> in 00:05:31.690 --> 00:05:31.700 align:start position:0% hand side we have the specification in 00:05:31.700 --> 00:05:33.250 align:start position:0% hand side we have the specification in the<00:05:31.850> active<00:05:32.210> language<00:05:32.390> and<00:05:32.870> on<00:05:33.020> the<00:05:33.110> right 00:05:33.250 --> 00:05:33.260 align:start position:0% the active language and on the right 00:05:33.260 --> 00:05:40.870 align:start position:0% the active language and on the right hand<00:05:33.440> side<00:05:33.530> we<00:05:33.770> have<00:05:33.950> a<00:05:34.420> simple<00:05:37.810> transfer<00:05:39.880> so 00:05:40.870 --> 00:05:40.880 align:start position:0% hand side we have a simple transfer so 00:05:40.880 --> 00:05:44.590 align:start position:0% hand side we have a simple transfer so what<00:05:41.690> we<00:05:41.810> do<00:05:42.020> is<00:05:42.430> well<00:05:43.430> actually<00:05:43.760> let<00:05:44.240> me<00:05:44.360> go 00:05:44.590 --> 00:05:44.600 align:start position:0% what we do is well actually let me go 00:05:44.600 --> 00:05:48.100 align:start position:0% what we do is well actually let me go back<00:05:45.080> and<00:05:45.590> just<00:05:45.860> say<00:05:46.220> the<00:05:46.760> main<00:05:47.060> claim<00:05:47.600> of<00:05:47.990> a 00:05:48.100 --> 00:05:48.110 align:start position:0% back and just say the main claim of a 00:05:48.110 --> 00:05:53.260 align:start position:0% back and just say the main claim of a specification<00:05:48.920> is<00:05:49.280> in<00:05:49.730> this<00:05:50.540> storage<00:05:52.270> header 00:05:53.260 --> 00:05:53.270 align:start position:0% specification is in this storage header 00:05:53.270 --> 00:05:55.390 align:start position:0% specification is in this storage header so<00:05:54.020> under<00:05:54.260> the<00:05:54.380> storage<00:05:54.710> header<00:05:54.920> we're<00:05:55.160> saying 00:05:55.390 --> 00:05:55.400 align:start position:0% so under the storage header we're saying 00:05:55.400 --> 00:05:58.510 align:start position:0% so under the storage header we're saying how<00:05:55.730> the<00:05:55.790> balances<00:05:56.570> of<00:05:56.840> the<00:05:57.500> people<00:05:58.250> involved 00:05:58.510 --> 00:05:58.520 align:start position:0% how the balances of the people involved 00:05:58.520 --> 00:06:01.510 align:start position:0% how the balances of the people involved are<00:05:58.940> being<00:05:59.510> updated<00:05:59.720> so<00:06:00.560> we're<00:06:01.220> saying<00:06:01.400> that 00:06:01.510 --> 00:06:01.520 align:start position:0% are being updated so we're saying that 00:06:01.520 --> 00:06:03.910 align:start position:0% are being updated so we're saying that whatever<00:06:02.330> their<00:06:02.600> initial<00:06:03.110> balances<00:06:03.710> word 00:06:03.910 --> 00:06:03.920 align:start position:0% whatever their initial balances word 00:06:03.920 --> 00:06:05.470 align:start position:0% whatever their initial balances word from<00:06:04.370> Bella<00:06:04.610> to<00:06:04.820> above<00:06:05.060> they're<00:06:05.210> going<00:06:05.330> to<00:06:05.420> be 00:06:05.470 --> 00:06:05.480 align:start position:0% from Bella to above they're going to be 00:06:05.480 --> 00:06:09.300 align:start position:0% from Bella to above they're going to be updated<00:06:06.550> with<00:06:07.550> a<00:06:07.580> corresponding<00:06:08.270> value<00:06:08.840> as<00:06:09.170> a 00:06:09.300 --> 00:06:09.310 align:start position:0% updated with a corresponding value as a 00:06:09.310 --> 00:06:10.530 align:start position:0% updated with a corresponding value as a [Music] 00:06:10.530 --> 00:06:10.540 align:start position:0% [Music] 00:06:10.540 --> 00:06:13.150 align:start position:0% [Music] as<00:06:11.540> a<00:06:11.600> result<00:06:12.020> of<00:06:12.200> calling<00:06:12.440> the<00:06:12.710> transfer 00:06:13.150 --> 00:06:13.160 align:start position:0% as a result of calling the transfer 00:06:13.160 --> 00:06:16.630 align:start position:0% as a result of calling the transfer function<00:06:14.770> okay<00:06:15.770> but<00:06:15.950> this<00:06:16.100> doesn't<00:06:16.370> always 00:06:16.630 --> 00:06:16.640 align:start position:0% function okay but this doesn't always 00:06:16.640 --> 00:06:19.720 align:start position:0% function okay but this doesn't always happen<00:06:17.210> because<00:06:17.950> there<00:06:18.950> are<00:06:19.070> some<00:06:19.250> scenarios 00:06:19.720 --> 00:06:19.730 align:start position:0% happen because there are some scenarios 00:06:19.730 --> 00:06:21.730 align:start position:0% happen because there are some scenarios where<00:06:19.760> you<00:06:20.570> do<00:06:20.720> call<00:06:20.930> the<00:06:21.050> transfer<00:06:21.380> function 00:06:21.730 --> 00:06:21.740 align:start position:0% where you do call the transfer function 00:06:21.740 --> 00:06:23.560 align:start position:0% where you do call the transfer function and<00:06:21.890> your<00:06:22.040> balances<00:06:22.490> aren't<00:06:22.790> updated<00:06:22.970> namely 00:06:23.560 --> 00:06:23.570 align:start position:0% and your balances aren't updated namely 00:06:23.570 --> 00:06:26.110 align:start position:0% and your balances aren't updated namely if<00:06:23.690> you<00:06:24.650> don't<00:06:24.860> have<00:06:25.070> enough<00:06:25.310> money<00:06:25.610> to<00:06:25.910> send 00:06:26.110 --> 00:06:26.120 align:start position:0% if you don't have enough money to send 00:06:26.120 --> 00:06:29.560 align:start position:0% if you don't have enough money to send or<00:06:26.620> if<00:06:27.620> there's<00:06:28.100> an<00:06:28.310> overflow<00:06:28.640> when<00:06:29.420> you're 00:06:29.560 --> 00:06:29.570 align:start position:0% or if there's an overflow when you're 00:06:29.570 --> 00:06:32.290 align:start position:0% or if there's an overflow when you're trying<00:06:29.840> to<00:06:29.960> add<00:06:30.200> the<00:06:30.980> value<00:06:31.370> to<00:06:31.910> of<00:06:32.210> the 00:06:32.290 --> 00:06:32.300 align:start position:0% trying to add the value to of the 00:06:32.300 --> 00:06:35.110 align:start position:0% trying to add the value to of the receiver<00:06:32.690> and<00:06:33.290> so<00:06:33.680> this<00:06:34.280> should<00:06:34.490> be<00:06:34.640> reflected 00:06:35.110 --> 00:06:35.120 align:start position:0% receiver and so this should be reflected 00:06:35.120 --> 00:06:37.630 align:start position:0% receiver and so this should be reflected in<00:06:35.210> the<00:06:35.300> spec<00:06:35.540> and<00:06:35.870> here<00:06:36.860> it<00:06:36.920> is<00:06:36.980> we<00:06:37.190> see<00:06:37.400> that 00:06:37.630 --> 00:06:37.640 align:start position:0% in the spec and here it is we see that 00:06:37.640 --> 00:06:40.930 align:start position:0% in the spec and here it is we see that they're<00:06:37.820> actually<00:06:39.250> four<00:06:40.250> conditions 00:06:40.930 --> 00:06:40.940 align:start position:0% they're actually four conditions 00:06:40.940 --> 00:06:42.379 align:start position:0% they're actually four conditions associated<00:06:41.240> with<00:06:41.660> this 00:06:42.379 --> 00:06:42.389 align:start position:0% associated with this 00:06:42.389 --> 00:06:48.050 align:start position:0% associated with this out<00:06:43.009> and<00:06:44.750> the<00:06:45.750> first<00:06:45.990> three<00:06:46.289> are<00:06:47.060> associated 00:06:48.050 --> 00:06:48.060 align:start position:0% out and the first three are associated 00:06:48.060 --> 00:06:50.420 align:start position:0% out and the first three are associated with<00:06:48.090> and<00:06:48.599> if<00:06:49.050> and<00:06:49.229> only<00:06:49.259> if<00:06:49.439> Petter<00:06:49.979> resists 00:06:50.420 --> 00:06:50.430 align:start position:0% with and if and only if Petter resists 00:06:50.430 --> 00:06:56.149 align:start position:0% with and if and only if Petter resists iff<00:06:51.740> and<00:06:52.740> that<00:06:52.860> means<00:06:53.270> that<00:06:54.270> in<00:06:54.689> the<00:06:54.960> two<00:06:55.800> specs 00:06:56.149 --> 00:06:56.159 align:start position:0% iff and that means that in the two specs 00:06:56.159 --> 00:06:58.219 align:start position:0% iff and that means that in the two specs that<00:06:56.280> are<00:06:56.460> going<00:06:56.699> to<00:06:56.759> be<00:06:56.819> generated<00:06:57.330> or<00:06:57.900> the<00:06:58.050> to 00:06:58.219 --> 00:06:58.229 align:start position:0% that are going to be generated or the to 00:06:58.229 --> 00:06:59.659 align:start position:0% that are going to be generated or the to reach<00:06:58.469> ability<00:06:58.680> claims<00:06:59.069> are<00:06:59.250> to<00:06:59.400> proof 00:06:59.659 --> 00:06:59.669 align:start position:0% reach ability claims are to proof 00:06:59.669 --> 00:07:00.709 align:start position:0% reach ability claims are to proof obligations<00:06:59.849> that<00:07:00.360> are<00:07:00.419> going<00:07:00.599> to<00:07:00.659> be 00:07:00.709 --> 00:07:00.719 align:start position:0% obligations that are going to be 00:07:00.719 --> 00:07:06.700 align:start position:0% obligations that are going to be generated<00:07:01.229> from<00:07:01.379> this<00:07:03.110> act<00:07:04.759> we<00:07:05.759> are<00:07:05.789> going<00:07:06.210> to 00:07:06.700 --> 00:07:06.710 align:start position:0% generated from this act we are going to 00:07:06.710 --> 00:07:11.659 align:start position:0% generated from this act we are going to assume<00:07:07.710> all<00:07:08.490> of<00:07:08.550> the<00:07:09.259> conditions<00:07:10.259> in<00:07:10.560> the<00:07:10.949> pit 00:07:11.659 --> 00:07:11.669 align:start position:0% assume all of the conditions in the pit 00:07:11.669 --> 00:07:17.869 align:start position:0% assume all of the conditions in the pit of<00:07:12.030> the<00:07:12.090> earth<00:07:12.300> header<00:07:15.169> to<00:07:16.169> be<00:07:16.289> true<00:07:16.560> in<00:07:17.250> the 00:07:17.869 --> 00:07:17.879 align:start position:0% of the earth header to be true in the 00:07:17.879 --> 00:07:21.019 align:start position:0% of the earth header to be true in the past<00:07:18.180> case<00:07:18.569> than<00:07:19.169> to<00:07:19.319> be<00:07:19.439> false<00:07:19.740> in<00:07:20.639> the<00:07:20.819> fail 00:07:21.019 --> 00:07:21.029 align:start position:0% past case than to be false in the fail 00:07:21.029 --> 00:07:24.589 align:start position:0% past case than to be false in the fail case<00:07:21.379> so<00:07:22.610> what<00:07:23.610> the<00:07:23.699> nature<00:07:23.849> of<00:07:24.000> that<00:07:24.060> claim<00:07:24.389> is 00:07:24.589 --> 00:07:24.599 align:start position:0% case so what the nature of that claim is 00:07:24.599 --> 00:07:27.519 align:start position:0% case so what the nature of that claim is is<00:07:24.810> is<00:07:25.050> that<00:07:25.620> it<00:07:25.710> amounts<00:07:26.039> to<00:07:26.069> saying<00:07:26.370> that 00:07:27.519 --> 00:07:27.529 align:start position:0% is is that it amounts to saying that 00:07:27.529 --> 00:07:34.519 align:start position:0% is is that it amounts to saying that only<00:07:28.529> if<00:07:28.710> in<00:07:29.250> the<00:07:29.370> case<00:07:29.610> where<00:07:32.719> we<00:07:33.719> are<00:07:33.990> still 00:07:34.519 --> 00:07:34.529 align:start position:0% only if in the case where we are still 00:07:34.529 --> 00:07:40.809 align:start position:0% only if in the case where we are still within<00:07:34.770> the<00:07:34.979> range<00:07:35.189> of<00:07:35.550> a<00:07:35.969> UN<00:07:37.819> 256-bit<00:07:38.819> word 00:07:40.809 --> 00:07:40.819 align:start position:0% within the range of a UN 256-bit word 00:07:40.819 --> 00:07:43.820 align:start position:0% within the range of a UN 256-bit word then<00:07:41.819> these<00:07:42.449> storage<00:07:43.020> updates<00:07:43.439> should<00:07:43.680> be 00:07:43.820 --> 00:07:43.830 align:start position:0% then these storage updates should be 00:07:43.830 --> 00:07:46.430 align:start position:0% then these storage updates should be performed<00:07:44.340> and<00:07:44.750> when<00:07:45.750> any<00:07:46.139> of<00:07:46.319> these 00:07:46.430 --> 00:07:46.440 align:start position:0% performed and when any of these 00:07:46.440 --> 00:07:49.040 align:start position:0% performed and when any of these conditions<00:07:46.710> are<00:07:47.069> not<00:07:47.219> met<00:07:47.279> then<00:07:48.029> we<00:07:48.419> should<00:07:48.960> be 00:07:49.040 --> 00:07:49.050 align:start position:0% conditions are not met then we should be 00:07:49.050 --> 00:07:50.300 align:start position:0% conditions are not met then we should be in<00:07:49.139> the<00:07:49.229> field<00:07:49.349> case<00:07:49.620> in<00:07:49.770> the<00:07:49.860> fail<00:07:50.009> case 00:07:50.300 --> 00:07:50.310 align:start position:0% in the field case in the fail case 00:07:50.310 --> 00:07:52.519 align:start position:0% in the field case in the fail case asserts<00:07:50.909> that<00:07:51.029> everything<00:07:51.479> must<00:07:51.629> reverse<00:07:51.990> no 00:07:52.519 --> 00:07:52.529 align:start position:0% asserts that everything must reverse no 00:07:52.529 --> 00:07:56.659 align:start position:0% asserts that everything must reverse no storage<00:07:53.279> updates<00:07:53.759> are<00:07:54.089> to<00:07:54.270> be<00:07:54.389> performed<00:07:55.669> but 00:07:56.659 --> 00:07:56.669 align:start position:0% storage updates are to be performed but 00:07:56.669 --> 00:07:58.459 align:start position:0% storage updates are to be performed but there's<00:07:56.849> another<00:07:57.120> type<00:07:57.419> of<00:07:57.449> condition<00:07:58.110> that 00:07:58.459 --> 00:07:58.469 align:start position:0% there's another type of condition that 00:07:58.469 --> 00:08:02.510 align:start position:0% there's another type of condition that we<00:07:58.560> can<00:07:58.740> make<00:07:59.550> in<00:08:00.060> an<00:08:00.210> act<00:08:00.500> and<00:08:01.500> that's<00:08:01.589> the<00:08:01.770> if 00:08:02.510 --> 00:08:02.520 align:start position:0% we can make in an act and that's the if 00:08:02.520 --> 00:08:04.730 align:start position:0% we can make in an act and that's the if better<00:08:02.729> then<00:08:03.419> the<00:08:03.539> indenter<00:08:04.229> that<00:08:04.529> the 00:08:04.730 --> 00:08:04.740 align:start position:0% better then the indenter that the 00:08:04.740 --> 00:08:06.439 align:start position:0% better then the indenter that the conditions<00:08:05.129> in<00:08:05.279> the<00:08:05.370> if<00:08:05.490> that<00:08:05.639> are<00:08:05.759> assumed<00:08:06.210> in 00:08:06.439 --> 00:08:06.449 align:start position:0% conditions in the if that are assumed in 00:08:06.449 --> 00:08:08.689 align:start position:0% conditions in the if that are assumed in both<00:08:06.719> the<00:08:07.319> fail<00:08:07.560> in<00:08:07.770> the<00:08:07.860> past<00:08:08.069> cases<00:08:08.520> so 00:08:08.689 --> 00:08:08.699 align:start position:0% both the fail in the past cases so 00:08:08.699 --> 00:08:11.689 align:start position:0% both the fail in the past cases so obviously<00:08:09.089> this<00:08:10.219> restricts<00:08:11.219> the<00:08:11.370> nature<00:08:11.669> of 00:08:11.689 --> 00:08:11.699 align:start position:0% obviously this restricts the nature of 00:08:11.699 --> 00:08:13.610 align:start position:0% obviously this restricts the nature of your<00:08:11.849> claim<00:08:12.120> to<00:08:12.270> make<00:08:12.389> sense<00:08:12.629> slightly<00:08:13.199> weaker 00:08:13.610 --> 00:08:13.620 align:start position:0% your claim to make sense slightly weaker 00:08:13.620 --> 00:08:16.610 align:start position:0% your claim to make sense slightly weaker by<00:08:14.550> assuming<00:08:15.330> additional<00:08:15.810> assumptions<00:08:16.289> and 00:08:16.610 --> 00:08:16.620 align:start position:0% by assuming additional assumptions and 00:08:16.620 --> 00:08:19.519 align:start position:0% by assuming additional assumptions and so<00:08:17.400> if<00:08:17.669> you<00:08:17.819> have<00:08:18.060> and<00:08:18.360> it<00:08:18.839> better<00:08:19.020> like<00:08:19.289> this 00:08:19.519 --> 00:08:19.529 align:start position:0% so if you have and it better like this 00:08:19.529 --> 00:08:21.679 align:start position:0% so if you have and it better like this you<00:08:19.770> must<00:08:19.949> have<00:08:20.039> a<00:08:20.189> corresponding<00:08:20.689> next 00:08:21.679 --> 00:08:21.689 align:start position:0% you must have a corresponding next 00:08:21.689 --> 00:08:24.779 align:start position:0% you must have a corresponding next suspect<00:08:21.900> but<00:08:22.319> assumes<00:08:22.650> the<00:08:22.830> negation<00:08:23.279> of<00:08:23.460> that 00:08:24.779 --> 00:08:24.789 align:start position:0% suspect but assumes the negation of that 00:08:24.789 --> 00:08:28.050 align:start position:0% suspect but assumes the negation of that so<00:08:25.180> in<00:08:25.690> this<00:08:25.810> particular<00:08:25.990> SPECT<00:08:26.680> were<00:08:27.060> saying 00:08:28.050 --> 00:08:28.060 align:start position:0% so in this particular SPECT were saying 00:08:28.060 --> 00:08:30.510 align:start position:0% so in this particular SPECT were saying that<00:08:28.240> the<00:08:28.330> caller<00:08:28.569> ID<00:08:29.099> should<00:08:30.099> be<00:08:30.190> different 00:08:30.510 --> 00:08:30.520 align:start position:0% that the caller ID should be different 00:08:30.520 --> 00:08:32.550 align:start position:0% that the caller ID should be different from<00:08:30.610> from<00:08:31.240> the<00:08:31.360> two<00:08:31.539> meaning<00:08:31.990> of<00:08:32.110> the<00:08:32.229> sender 00:08:32.550 --> 00:08:32.560 align:start position:0% from from the two meaning of the sender 00:08:32.560 --> 00:08:33.719 align:start position:0% from from the two meaning of the sender should<00:08:32.589> be<00:08:32.830> different<00:08:33.070> from<00:08:33.250> the<00:08:33.430> receiver 00:08:33.719 --> 00:08:33.729 align:start position:0% should be different from the receiver 00:08:33.729 --> 00:08:36.139 align:start position:0% should be different from the receiver because<00:08:33.940> we<00:08:34.240> had<00:08:34.419> to<00:08:34.510> treat<00:08:34.719> this<00:08:34.979> case 00:08:36.139 --> 00:08:36.149 align:start position:0% because we had to treat this case 00:08:36.149 --> 00:08:38.639 align:start position:0% because we had to treat this case somewhat<00:08:37.200> differently 00:08:38.639 --> 00:08:38.649 align:start position:0% somewhat differently 00:08:38.649 --> 00:08:41.969 align:start position:0% somewhat differently I<00:08:38.680> mean<00:08:39.399> we<00:08:40.029> actually<00:08:40.570> that<00:08:41.529> would<00:08:41.740> only<00:08:41.860> be 00:08:41.969 --> 00:08:41.979 align:start position:0% I mean we actually that would only be 00:08:41.979 --> 00:08:45.090 align:start position:0% I mean we actually that would only be referring<00:08:42.459> to<00:08:42.610> a<00:08:42.760> single<00:08:43.529> entry<00:08:44.529> and<00:08:44.770> the 00:08:45.090 --> 00:08:45.100 align:start position:0% referring to a single entry and the 00:08:45.100 --> 00:08:47.579 align:start position:0% referring to a single entry and the storage<00:08:45.600> rather<00:08:46.600> than<00:08:46.839> two<00:08:47.050> separate<00:08:47.410> votes 00:08:47.579 --> 00:08:47.589 align:start position:0% storage rather than two separate votes 00:08:47.589 --> 00:08:50.160 align:start position:0% storage rather than two separate votes so<00:08:48.070> we<00:08:48.910> need<00:08:49.029> to<00:08:49.149> write<00:08:49.270> that<00:08:49.450> SPECT<00:08:49.750> a<00:08:49.930> little 00:08:50.160 --> 00:08:50.170 align:start position:0% so we need to write that SPECT a little 00:08:50.170 --> 00:08:55.889 align:start position:0% so we need to write that SPECT a little bit<00:08:50.290> differently<00:08:50.589> and<00:08:54.209> so<00:08:55.209> then<00:08:55.420> during<00:08:55.810> the 00:08:55.889 --> 00:08:55.899 align:start position:0% bit differently and so then during the 00:08:55.899 --> 00:08:57.210 align:start position:0% bit differently and so then during the course<00:08:56.110> of<00:08:56.170> this<00:08:56.260> competition<00:08:56.620> will<00:08:56.860> be 00:08:57.210 --> 00:08:57.220 align:start position:0% course of this competition will be 00:08:57.220 --> 00:09:02.010 align:start position:0% course of this competition will be making<00:08:59.459> we<00:09:00.459> have<00:09:00.640> a<00:09:00.850> suite<00:09:01.180> of<00:09:01.330> these<00:09:01.510> specs 00:09:02.010 --> 00:09:02.020 align:start position:0% making we have a suite of these specs 00:09:02.020 --> 00:09:07.050 align:start position:0% making we have a suite of these specs that<00:09:02.200> will<00:09:02.290> go<00:09:02.470> over<00:09:02.500> soon<00:09:03.370> enough<00:09:03.750> and<00:09:06.060> they 00:09:07.050 --> 00:09:07.060 align:start position:0% that will go over soon enough and they 00:09:07.060 --> 00:09:09.050 align:start position:0% that will go over soon enough and they will<00:09:07.240> generate<00:09:07.660> these<00:09:07.959> proof<00:09:08.380> obligations 00:09:09.050 --> 00:09:09.060 align:start position:0% will generate these proof obligations 00:09:09.060 --> 00:09:11.760 align:start position:0% will generate these proof obligations your<00:09:10.060> byte<00:09:10.360> code<00:09:10.630> will<00:09:10.899> be<00:09:11.020> associated<00:09:11.320> with<00:09:11.680> a 00:09:11.760 --> 00:09:11.770 align:start position:0% your byte code will be associated with a 00:09:11.770 --> 00:09:14.010 align:start position:0% your byte code will be associated with a proof<00:09:12.070> obligation<00:09:12.670> and<00:09:12.940> the<00:09:13.420> proof<00:09:13.779> will<00:09:13.990> be 00:09:14.010 --> 00:09:14.020 align:start position:0% proof obligation and the proof will be 00:09:14.020 --> 00:09:19.139 align:start position:0% proof obligation and the proof will be run<00:09:14.320> on<00:09:14.560> our<00:09:14.740> CI<00:09:14.980> machine<00:09:15.839> and<00:09:17.310> after<00:09:18.310> they 00:09:19.139 --> 00:09:19.149 align:start position:0% run on our CI machine and after they 00:09:19.149 --> 00:09:22.920 align:start position:0% run on our CI machine and after they have<00:09:19.330> been<00:09:19.450> run<00:09:19.720> if<00:09:20.110> all<00:09:20.529> of<00:09:20.740> your<00:09:21.779> specs<00:09:22.779> are 00:09:22.920 --> 00:09:22.930 align:start position:0% have been run if all of your specs are 00:09:22.930 --> 00:09:24.030 align:start position:0% have been run if all of your specs are passing<00:09:23.350> you<00:09:23.440> follow<00:09:23.649> that<00:09:23.800> proof 00:09:24.030 --> 00:09:24.040 align:start position:0% passing you follow that proof 00:09:24.040 --> 00:09:26.190 align:start position:0% passing you follow that proof obligations<00:09:24.190> have<00:09:24.760> been<00:09:25.000> proven<00:09:25.360> and<00:09:25.720> then 00:09:26.190 --> 00:09:26.200 align:start position:0% obligations have been proven and then 00:09:26.200 --> 00:09:29.730 align:start position:0% obligations have been proven and then there<00:09:26.740> we<00:09:27.130> will<00:09:27.310> be<00:09:27.930> taking<00:09:28.930> the<00:09:29.140> execution 00:09:29.730 --> 00:09:29.740 align:start position:0% there we will be taking the execution 00:09:29.740 --> 00:09:31.800 align:start position:0% there we will be taking the execution traces<00:09:30.250> so<00:09:30.490> the<00:09:30.970> method<00:09:31.300> by<00:09:31.450> which<00:09:31.480> we're 00:09:31.800 --> 00:09:31.810 align:start position:0% traces so the method by which we're 00:09:31.810 --> 00:09:33.780 align:start position:0% traces so the method by which we're proving<00:09:31.990> things<00:09:32.440> is<00:09:32.800> through<00:09:33.250> a<00:09:33.339> symbolic 00:09:33.780 --> 00:09:33.790 align:start position:0% proving things is through a symbolic 00:09:33.790 --> 00:09:37.260 align:start position:0% proving things is through a symbolic execution<00:09:34.290> and<00:09:35.290> that<00:09:35.680> gives<00:09:35.920> you<00:09:36.279> a<00:09:36.610> complete 00:09:37.260 --> 00:09:37.270 align:start position:0% execution and that gives you a complete 00:09:37.270 --> 00:09:39.090 align:start position:0% execution and that gives you a complete exploration<00:09:37.990> of<00:09:38.200> the<00:09:38.290> possible<00:09:38.680> things<00:09:38.890> that 00:09:39.090 --> 00:09:39.100 align:start position:0% exploration of the possible things that 00:09:39.100 --> 00:09:41.490 align:start position:0% exploration of the possible things that could<00:09:39.370> happen<00:09:39.600> through<00:09:40.600> the<00:09:40.690> execution<00:09:41.020> of 00:09:41.490 --> 00:09:41.500 align:start position:0% could happen through the execution of 00:09:41.500 --> 00:09:44.579 align:start position:0% could happen through the execution of this<00:09:41.709> method<00:09:42.610> and<00:09:42.870> through<00:09:43.870> this<00:09:43.990> execution 00:09:44.579 --> 00:09:44.589 align:start position:0% this method and through this execution 00:09:44.589 --> 00:09:47.190 align:start position:0% this method and through this execution trace<00:09:44.740> we<00:09:45.040> were<00:09:45.100> able<00:09:45.220> to<00:09:45.520> walk<00:09:46.360> down<00:09:46.390> all<00:09:46.959> the 00:09:47.190 --> 00:09:47.200 align:start position:0% trace we were able to walk down all the 00:09:47.200 --> 00:09:48.090 align:start position:0% trace we were able to walk down all the branches<00:09:47.620> and 00:09:48.090 --> 00:09:48.100 align:start position:0% branches and 00:09:48.100 --> 00:09:52.890 align:start position:0% branches and the<00:09:48.460> final<00:09:48.940> result<00:09:49.540> and<00:09:49.780> guests<00:09:51.570> the<00:09:52.570> final 00:09:52.890 --> 00:09:52.900 align:start position:0% the final result and guests the final 00:09:52.900 --> 00:09:55.110 align:start position:0% the final result and guests the final gastrous<00:09:53.260> also<00:09:53.560> the<00:09:53.680> final<00:09:54.010> gas<00:09:54.250> consumed<00:09:54.820> by 00:09:55.110 --> 00:09:55.120 align:start position:0% gastrous also the final gas consumed by 00:09:55.120 --> 00:09:59.940 align:start position:0% gastrous also the final gas consumed by this<00:09:55.180> method<00:09:55.600> in<00:09:56.020> each<00:09:56.290> match<00:09:56.820> and<00:09:58.140> when<00:09:59.140> we<00:09:59.470> do 00:09:59.940 --> 00:09:59.950 align:start position:0% this method in each match and when we do 00:09:59.950 --> 00:10:03.320 align:start position:0% this method in each match and when we do this<00:10:00.100> gas<00:10:00.790> extraction<00:10:01.270> we<00:10:01.540> take<00:10:01.780> the<00:10:02.020> maximum 00:10:03.320 --> 00:10:03.330 align:start position:0% this gas extraction we take the maximum 00:10:03.330 --> 00:10:05.700 align:start position:0% this gas extraction we take the maximum values<00:10:04.330> of<00:10:04.360> the<00:10:04.570> worst<00:10:04.750> case<00:10:04.960> scenario<00:10:05.410> call 00:10:05.700 --> 00:10:05.710 align:start position:0% values of the worst case scenario call 00:10:05.710 --> 00:10:08.720 align:start position:0% values of the worst case scenario call this<00:10:05.890> function<00:10:06.130> and<00:10:06.840> this<00:10:07.840> is<00:10:08.080> going<00:10:08.350> to<00:10:08.500> be 00:10:08.720 --> 00:10:08.730 align:start position:0% this function and this is going to be 00:10:08.730 --> 00:10:14.100 align:start position:0% this function and this is going to be your<00:10:10.320> value<00:10:11.320> that<00:10:11.680> you're<00:10:12.120> completely<00:10:13.120> so<00:10:13.810> we 00:10:14.100 --> 00:10:14.110 align:start position:0% your value that you're completely so we 00:10:14.110 --> 00:10:15.960 align:start position:0% your value that you're completely so we get<00:10:14.500> a<00:10:14.530> small<00:10:14.830> expression<00:10:15.370> like<00:10:15.520> this<00:10:15.670> if<00:10:15.820> you 00:10:15.960 --> 00:10:15.970 align:start position:0% get a small expression like this if you 00:10:15.970 --> 00:10:18.800 align:start position:0% get a small expression like this if you know<00:10:16.090> your<00:10:16.300> idiom<00:10:16.840> then<00:10:17.740> you<00:10:17.920> know<00:10:18.100> that 00:10:18.800 --> 00:10:18.810 align:start position:0% know your idiom then you know that 00:10:18.810 --> 00:10:20.990 align:start position:0% know your idiom then you know that whenever<00:10:19.810> you<00:10:20.020> do<00:10:20.110> this<00:10:20.200> story<00:10:20.440> to<00:10:20.590> update 00:10:20.990 --> 00:10:21.000 align:start position:0% whenever you do this story to update 00:10:21.000 --> 00:10:23.310 align:start position:0% whenever you do this story to update what<00:10:22.000> actually<00:10:22.330> determines<00:10:22.810> the<00:10:22.900> cost<00:10:23.110> of 00:10:23.310 --> 00:10:23.320 align:start position:0% what actually determines the cost of 00:10:23.320 --> 00:10:27.750 align:start position:0% what actually determines the cost of that<00:10:24.390> has<00:10:25.390> to<00:10:25.570> do<00:10:25.720> with<00:10:25.900> whether<00:10:26.500> the<00:10:27.160> storage 00:10:27.750 --> 00:10:27.760 align:start position:0% that has to do with whether the storage 00:10:27.760 --> 00:10:29.490 align:start position:0% that has to do with whether the storage that<00:10:27.790> you're<00:10:28.120> obtaining<00:10:28.300> was<00:10:28.660> 0<00:10:28.960> or<00:10:29.290> where 00:10:29.490 --> 00:10:29.500 align:start position:0% that you're obtaining was 0 or where 00:10:29.500 --> 00:10:31.650 align:start position:0% that you're obtaining was 0 or where they<00:10:29.680> are<00:10:29.710> putting<00:10:30.070> it<00:10:30.190> to<00:10:30.310> 0<00:10:30.550> as<00:10:31.180> so<00:10:31.360> we'll<00:10:31.510> see 00:10:31.650 --> 00:10:31.660 align:start position:0% they are putting it to 0 as so we'll see 00:10:31.660 --> 00:10:33.800 align:start position:0% they are putting it to 0 as so we'll see conditions<00:10:31.930> on<00:10:32.290> this<00:10:32.470> board<00:10:32.770> where<00:10:32.980> they<00:10:33.460> are 00:10:33.800 --> 00:10:33.810 align:start position:0% conditions on this board where they are 00:10:33.810 --> 00:10:36.450 align:start position:0% conditions on this board where they are the<00:10:34.810> most<00:10:34.960> general<00:10:35.440> but<00:10:35.620> of<00:10:35.950> course<00:10:36.220> you<00:10:36.310> can 00:10:36.450 --> 00:10:36.460 align:start position:0% the most general but of course you can 00:10:36.460 --> 00:10:38.490 align:start position:0% the most general but of course you can take<00:10:36.610> the<00:10:36.790> worst<00:10:37.510> case<00:10:37.630> scenario<00:10:38.110> this<00:10:38.260> and 00:10:38.490 --> 00:10:38.500 align:start position:0% take the worst case scenario this and 00:10:38.500 --> 00:10:44.010 align:start position:0% take the worst case scenario this and this<00:10:38.590> is<00:10:38.710> what<00:10:38.890> we'll<00:10:39.070> be<00:10:39.250> using<00:10:42.780> ok 00:10:44.010 --> 00:10:44.020 align:start position:0% this is what we'll be using ok 00:10:44.020 --> 00:10:48.960 align:start position:0% this is what we'll be using ok so<00:10:44.520> with<00:10:45.520> that<00:10:45.670> let<00:10:46.060> me<00:10:46.090> just<00:10:47.490> say<00:10:48.490> how<00:10:48.790> this 00:10:48.960 --> 00:10:48.970 align:start position:0% so with that let me just say how this 00:10:48.970 --> 00:10:52.050 align:start position:0% so with that let me just say how this will<00:10:49.150> all<00:10:49.180> go<00:10:49.510> down<00:10:50.100> as<00:10:51.100> I<00:10:51.280> said<00:10:51.550> all<00:10:51.790> groups 00:10:52.050 --> 00:10:52.060 align:start position:0% will all go down as I said all groups 00:10:52.060 --> 00:10:54.420 align:start position:0% will all go down as I said all groups will<00:10:52.300> be<00:10:52.330> running<00:10:52.690> on<00:10:52.840> our<00:10:53.130> service<00:10:54.130> you<00:10:54.250> don't 00:10:54.420 --> 00:10:54.430 align:start position:0% will be running on our service you don't 00:10:54.430 --> 00:10:58.440 align:start position:0% will be running on our service you don't actually<00:10:54.880> needs<00:10:55.120> to<00:10:55.330> do<00:10:56.040> much<00:10:57.040> yourself<00:10:57.970> of 00:10:58.440 --> 00:10:58.450 align:start position:0% actually needs to do much yourself of 00:10:58.450 --> 00:11:00.000 align:start position:0% actually needs to do much yourself of course<00:10:58.630> if<00:10:58.750> you<00:10:58.870> just<00:10:59.080> if<00:10:59.260> you<00:10:59.380> can<00:10:59.470> come<00:10:59.710> and 00:11:00.000 --> 00:11:00.010 align:start position:0% course if you just if you can come and 00:11:00.010 --> 00:11:03.330 align:start position:0% course if you just if you can come and chance<00:11:00.340> we<00:11:00.460> can<00:11:00.940> talk<00:11:01.090> about<00:11:01.180> it<00:11:01.830> but<00:11:02.830> for<00:11:03.250> the 00:11:03.330 --> 00:11:03.340 align:start position:0% chance we can talk about it but for the 00:11:03.340 --> 00:11:05.280 align:start position:0% chance we can talk about it but for the purposes<00:11:03.790> of<00:11:03.970> this<00:11:04.060> competition<00:11:04.690> the<00:11:05.050> only 00:11:05.280 --> 00:11:05.290 align:start position:0% purposes of this competition the only 00:11:05.290 --> 00:11:07.740 align:start position:0% purposes of this competition the only thing<00:11:05.440> that<00:11:05.590> you<00:11:05.680> need<00:11:05.830> to<00:11:05.860> do<00:11:06.100> is<00:11:06.370> to<00:11:07.210> write<00:11:07.480> an 00:11:07.740 --> 00:11:07.750 align:start position:0% thing that you need to do is to write an 00:11:07.750 --> 00:11:10.080 align:start position:0% thing that you need to do is to write an implementation<00:11:08.410> get<00:11:09.010> the<00:11:09.130> bytecode<00:11:09.340> of<00:11:09.910> that 00:11:10.080 --> 00:11:10.090 align:start position:0% implementation get the bytecode of that 00:11:10.090 --> 00:11:13.040 align:start position:0% implementation get the bytecode of that implementation<00:11:10.780> the<00:11:10.930> runtime<00:11:11.320> bytecode<00:11:11.770> and 00:11:13.040 --> 00:11:13.050 align:start position:0% implementation the runtime bytecode and 00:11:13.050 --> 00:11:15.900 align:start position:0% implementation the runtime bytecode and make<00:11:14.050> a<00:11:14.080> PR<00:11:14.470> to<00:11:14.860> a<00:11:14.890> repo<00:11:15.250> that<00:11:15.520> will<00:11:15.670> be<00:11:15.730> showing 00:11:15.900 --> 00:11:15.910 align:start position:0% make a PR to a repo that will be showing 00:11:15.910 --> 00:11:19.500 align:start position:0% make a PR to a repo that will be showing you<00:11:16.090> soon<00:11:17.370> and<00:11:18.370> everything<00:11:18.940> that<00:11:19.090> is<00:11:19.210> provably 00:11:19.500 --> 00:11:19.510 align:start position:0% you soon and everything that is provably 00:11:19.510 --> 00:11:24.420 align:start position:0% you soon and everything that is provably correct<00:11:19.870> will<00:11:20.020> be<00:11:20.110> analyzed<00:11:20.440> forecast 00:11:24.420 --> 00:11:24.430 align:start position:0% 00:11:24.430 --> 00:11:28.410 align:start position:0% okay<00:11:25.120> so<00:11:25.180> I<00:11:25.920> think<00:11:26.920> it's<00:11:27.220> time<00:11:27.580> to<00:11:27.850> go<00:11:27.970> over<00:11:28.000> the 00:11:28.410 --> 00:11:28.420 align:start position:0% okay so I think it's time to go over the 00:11:28.420 --> 00:11:32.610 align:start position:0% okay so I think it's time to go over the specs<00:11:29.460> they<00:11:30.460> can<00:11:30.610> be<00:11:30.670> found<00:11:30.940> at<00:11:31.300> this<00:11:31.620> repo 00:11:32.610 --> 00:11:32.620 align:start position:0% specs they can be found at this repo 00:11:32.620 --> 00:11:34.020 align:start position:0% specs they can be found at this repo which<00:11:32.800> is<00:11:32.950> the<00:11:33.100> repo<00:11:33.370> will<00:11:33.550> be<00:11:33.670> working<00:11:34.000> with 00:11:34.020 --> 00:11:34.030 align:start position:0% which is the repo will be working with 00:11:34.030 --> 00:11:36.630 align:start position:0% which is the repo will be working with inside<00:11:34.990> Catoctin<00:11:35.470> two-column<00:11:36.010> /<00:11:36.220> backward 00:11:36.630 --> 00:11:36.640 align:start position:0% inside Catoctin two-column / backward 00:11:36.640 --> 00:11:44.910 align:start position:0% inside Catoctin two-column / backward slash<00:11:36.940> yearsI<00:11:37.690> 20<00:11:38.020> -<00:11:38.200> golf<00:11:39.360> and<00:11:42.810> there's<00:11:43.810> as<00:11:44.770> i 00:11:44.910 --> 00:11:44.920 align:start position:0% slash yearsI 20 - golf and there's as i 00:11:44.920 --> 00:11:48.240 align:start position:0% slash yearsI 20 - golf and there's as i mentioned<00:11:45.220> there<00:11:45.310> were<00:11:45.460> some<00:11:47.250> opinionated 00:11:48.240 --> 00:11:48.250 align:start position:0% mentioned there were some opinionated 00:11:48.250 --> 00:11:50.940 align:start position:0% mentioned there were some opinionated choices<00:11:48.640> we<00:11:48.760> made<00:11:49.000> while<00:11:49.630> making<00:11:49.930> a<00:11:50.020> spec<00:11:50.320> well 00:11:50.940 --> 00:11:50.950 align:start position:0% choices we made while making a spec well 00:11:50.950 --> 00:11:52.860 align:start position:0% choices we made while making a spec well the<00:11:51.010> first<00:11:51.340> one<00:11:51.580> the<00:11:52.090> most<00:11:52.240> important<00:11:52.600> monster 00:11:52.860 --> 00:11:52.870 align:start position:0% the first one the most important monster 00:11:52.870 --> 00:11:55.290 align:start position:0% the first one the most important monster listed<00:11:53.170> on<00:11:53.290> this<00:11:53.380> page<00:11:53.620> will<00:11:54.370> not<00:11:54.820> be<00:11:55.030> caring 00:11:55.290 --> 00:11:55.300 align:start position:0% listed on this page will not be caring 00:11:55.300 --> 00:11:57.000 align:start position:0% listed on this page will not be caring about<00:11:55.360> logs<00:11:55.720> so<00:11:56.080> you<00:11:56.200> can<00:11:56.320> forget<00:11:56.560> about<00:11:56.620> logs 00:11:57.000 --> 00:11:57.010 align:start position:0% about logs so you can forget about logs 00:11:57.010 --> 00:11:59.580 align:start position:0% about logs so you can forget about logs for<00:11:57.310> your<00:11:57.460> implementation<00:11:58.170> for<00:11:59.170> the<00:11:59.230> purposes 00:11:59.580 --> 00:11:59.590 align:start position:0% for your implementation for the purposes 00:11:59.590 --> 00:12:03.630 align:start position:0% for your implementation for the purposes of<00:11:59.650> this<00:11:59.920> contest<00:12:01.560> everything<00:12:02.560> must<00:12:03.220> revert 00:12:03.630 --> 00:12:03.640 align:start position:0% of this contest everything must revert 00:12:03.640 --> 00:12:07.110 align:start position:0% of this contest everything must revert if<00:12:04.060> all<00:12:04.630> value<00:12:04.990> is<00:12:05.320> greater<00:12:06.220> than<00:12:06.430> zero<00:12:06.700> so 00:12:07.110 --> 00:12:07.120 align:start position:0% if all value is greater than zero so 00:12:07.120 --> 00:12:09.330 align:start position:0% if all value is greater than zero so this<00:12:07.240> is<00:12:07.360> following<00:12:07.720> the<00:12:08.080> convention<00:12:08.980> of<00:12:09.100> both 00:12:09.330 --> 00:12:09.340 align:start position:0% this is following the convention of both 00:12:09.340 --> 00:12:14.220 align:start position:0% this is following the convention of both my<00:12:09.580> parents<00:12:09.760> limiting<00:12:11.910> and<00:12:12.930> well<00:12:13.930> this<00:12:14.050> is 00:12:14.220 --> 00:12:14.230 align:start position:0% my parents limiting and well this is 00:12:14.230 --> 00:12:16.020 align:start position:0% my parents limiting and well this is this<00:12:14.470> is<00:12:14.620> actually<00:12:15.010> true<00:12:15.160> within<00:12:15.520> for<00:12:15.970> the 00:12:16.020 --> 00:12:16.030 align:start position:0% this is actually true within for the 00:12:16.030 --> 00:12:18.090 align:start position:0% this is actually true within for the minor<00:12:16.210> caveat<00:12:16.480> the<00:12:17.110> stores<00:12:17.410> will<00:12:17.620> give<00:12:17.650> you 00:12:18.090 --> 00:12:18.100 align:start position:0% minor caveat the stores will give you 00:12:18.100 --> 00:12:23.280 align:start position:0% minor caveat the stores will give you know<00:12:19.110> the<00:12:20.110> way<00:12:20.350> that<00:12:20.590> the<00:12:20.950> EVM<00:12:21.900> deals<00:12:22.900> with<00:12:23.260> a 00:12:23.280 --> 00:12:23.290 align:start position:0% know the way that the EVM deals with a 00:12:23.290 --> 00:12:25.770 align:start position:0% know the way that the EVM deals with a storage<00:12:23.770> under<00:12:24.040> the<00:12:24.070> hood<00:12:24.340> is<00:12:24.430> a<00:12:24.460> simple<00:12:24.910> key 00:12:25.770 --> 00:12:25.780 align:start position:0% storage under the hood is a simple key 00:12:25.780 --> 00:12:28.250 align:start position:0% storage under the hood is a simple key value<00:12:26.110> mapping<00:12:26.440> of<00:12:26.920> introduced<00:12:27.580> to<00:12:27.730> integers 00:12:28.250 --> 00:12:28.260 align:start position:0% value mapping of introduced to integers 00:12:28.260 --> 00:12:32.340 align:start position:0% value mapping of introduced to integers and<00:12:29.260> so<00:12:29.920> in<00:12:30.070> order<00:12:30.250> to<00:12:30.340> translate<00:12:30.970> the<00:12:31.510> so<00:12:32.020> the 00:12:32.340 --> 00:12:32.350 align:start position:0% and so in order to translate the so the 00:12:32.350 --> 00:12:34.950 align:start position:0% and so in order to translate the so the variables<00:12:32.920> that<00:12:33.070> are<00:12:33.190> being<00:12:33.250> used<00:12:33.610> in<00:12:33.970> near 00:12:34.950 --> 00:12:34.960 align:start position:0% variables that are being used in near 00:12:34.960 --> 00:12:36.720 align:start position:0% variables that are being used in near surprising<00:12:35.410> like<00:12:35.530> balances<00:12:36.040> in<00:12:36.190> total<00:12:36.460> supply 00:12:36.720 --> 00:12:36.730 align:start position:0% surprising like balances in total supply 00:12:36.730 --> 00:12:38.760 align:start position:0% surprising like balances in total supply and<00:12:36.910> allowances<00:12:37.420> you<00:12:37.660> need<00:12:38.140> to<00:12:38.260> place<00:12:38.500> these 00:12:38.760 --> 00:12:38.770 align:start position:0% and allowances you need to place these 00:12:38.770 --> 00:12:43.290 align:start position:0% and allowances you need to place these at<00:12:39.010> a<00:12:39.040> particular<00:12:39.490> location<00:12:40.290> these<00:12:42.300> these 00:12:43.290 --> 00:12:43.300 align:start position:0% at a particular location these these 00:12:43.300 --> 00:12:46.770 align:start position:0% at a particular location these these into<00:12:43.780> transit<00:12:44.110> your<00:12:44.260> mapping<00:12:44.590> in<00:12:44.800> the<00:12:45.100> UM<00:12:45.880> and 00:12:46.770 --> 00:12:46.780 align:start position:0% into transit your mapping in the UM and 00:12:46.780 --> 00:12:48.870 align:start position:0% into transit your mapping in the UM and there's<00:12:46.960> a<00:12:47.050> convention<00:12:47.890> for<00:12:48.280> how<00:12:48.430> you<00:12:48.490> do<00:12:48.700> this 00:12:48.870 --> 00:12:48.880 align:start position:0% there's a convention for how you do this 00:12:48.880 --> 00:12:53.280 align:start position:0% there's a convention for how you do this and<00:12:49.300> the<00:12:50.260> most<00:12:51.390> crucial<00:12:52.390> thing<00:12:52.810> to<00:12:52.840> know<00:12:53.080> here 00:12:53.280 --> 00:12:53.290 align:start position:0% and the most crucial thing to know here 00:12:53.290 --> 00:12:59.130 align:start position:0% and the most crucial thing to know here is<00:12:53.350> how<00:12:53.800> do<00:12:53.860> you<00:12:55.320> make<00:12:56.320> sure<00:12:56.590> that<00:12:57.900> you<00:12:58.900> need<00:12:58.990> to 00:12:59.130 --> 00:12:59.140 align:start position:0% is how do you make sure that you need to 00:12:59.140 --> 00:13:01.010 align:start position:0% is how do you make sure that you need to encode<00:12:59.380> basically<00:12:59.920> the<00:13:00.040> balances<00:13:00.520> on<00:13:00.670> the 00:13:01.010 --> 00:13:01.020 align:start position:0% encode basically the balances on the 00:13:01.020 --> 00:13:05.930 align:start position:0% encode basically the balances on the now<00:13:01.650> aids<00:13:02.150> in<00:13:03.150> a<00:13:03.210> particular<00:13:03.600> way<00:13:04.730> and<00:13:05.730> this<00:13:05.880> is 00:13:05.930 --> 00:13:05.940 align:start position:0% now aids in a particular way and this is 00:13:05.940 --> 00:13:09.610 align:start position:0% now aids in a particular way and this is a<00:13:06.120> particular<00:13:06.600> hashing<00:13:07.110> scheme<00:13:07.790> that 00:13:09.610 --> 00:13:09.620 align:start position:0% a particular hashing scheme that 00:13:09.620 --> 00:13:12.590 align:start position:0% a particular hashing scheme that salinity<00:13:10.620> uses<00:13:11.520> in<00:13:11.670> order<00:13:11.820> to<00:13:11.970> make<00:13:12.120> sure<00:13:12.360> that 00:13:12.590 --> 00:13:12.600 align:start position:0% salinity uses in order to make sure that 00:13:12.600 --> 00:13:14.810 align:start position:0% salinity uses in order to make sure that whatever<00:13:12.840> you<00:13:13.080> look<00:13:13.320> up<00:13:13.560> the<00:13:14.070> palace<00:13:14.580> of<00:13:14.700> a 00:13:14.810 --> 00:13:14.820 align:start position:0% whatever you look up the palace of a 00:13:14.820 --> 00:13:18.110 align:start position:0% whatever you look up the palace of a particular<00:13:15.270> address<00:13:16.550> you<00:13:17.550> won't<00:13:17.760> have<00:13:17.940> any 00:13:18.110 --> 00:13:18.120 align:start position:0% particular address you won't have any 00:13:18.120 --> 00:13:20.330 align:start position:0% particular address you won't have any collisions<00:13:18.510> with<00:13:18.810> any<00:13:19.530> other<00:13:19.680> address<00:13:20.100> of<00:13:20.250> the 00:13:20.330 --> 00:13:20.340 align:start position:0% collisions with any other address of the 00:13:20.340 --> 00:13:24.230 align:start position:0% collisions with any other address of the balance<00:13:20.640> of<00:13:20.700> memory<00:13:21.650> so<00:13:22.650> we<00:13:23.490> we<00:13:23.700> go<00:13:23.970> over<00:13:24.120> those 00:13:24.230 --> 00:13:24.240 align:start position:0% balance of memory so we we go over those 00:13:24.240 --> 00:13:26.570 align:start position:0% balance of memory so we we go over those details<00:13:24.300> if<00:13:25.260> you<00:13:25.500> want<00:13:25.620> to<00:13:25.890> but<00:13:26.370> you<00:13:26.490> can 00:13:26.570 --> 00:13:26.580 align:start position:0% details if you want to but you can 00:13:26.580 --> 00:13:28.220 align:start position:0% details if you want to but you can actually<00:13:26.880> also<00:13:27.030> use<00:13:27.120> the<00:13:27.420> library<00:13:27.780> Convention 00:13:28.220 --> 00:13:28.230 align:start position:0% actually also use the library Convention 00:13:28.230 --> 00:13:31.040 align:start position:0% actually also use the library Convention which<00:13:28.380> is<00:13:28.410> extremely<00:13:28.950> similar<00:13:29.520> a<00:13:29.760> big<00:13:30.300> hashes 00:13:31.040 --> 00:13:31.050 align:start position:0% which is extremely similar a big hashes 00:13:31.050 --> 00:13:32.750 align:start position:0% which is extremely similar a big hashes the<00:13:31.320> arguments<00:13:31.770> in<00:13:31.860> the<00:13:31.950> same<00:13:32.160> way<00:13:32.400> but<00:13:32.460> only 00:13:32.750 --> 00:13:32.760 align:start position:0% the arguments in the same way but only 00:13:32.760 --> 00:13:34.870 align:start position:0% the arguments in the same way but only in<00:13:32.940> a<00:13:33.030> reverse<00:13:33.300> order 00:13:34.870 --> 00:13:34.880 align:start position:0% in a reverse order 00:13:34.880 --> 00:13:37.640 align:start position:0% in a reverse order but<00:13:35.880> if<00:13:35.970> you're<00:13:36.120> using<00:13:36.270> solidity<00:13:36.990> or<00:13:37.140> vigor<00:13:37.410> to 00:13:37.640 --> 00:13:37.650 align:start position:0% but if you're using solidity or vigor to 00:13:37.650 --> 00:13:39.080 align:start position:0% but if you're using solidity or vigor to write<00:13:37.830> your<00:13:37.980> contacts<00:13:38.430> this<00:13:38.610> will<00:13:38.820> be<00:13:39.000> of 00:13:39.080 --> 00:13:39.090 align:start position:0% write your contacts this will be of 00:13:39.090 --> 00:13:43.220 align:start position:0% write your contacts this will be of course<00:13:39.360> done<00:13:39.540> for<00:13:40.020> you<00:13:41.480> and<00:13:42.480> supplying<00:13:42.960> all 00:13:43.220 --> 00:13:43.230 align:start position:0% course done for you and supplying all 00:13:43.230 --> 00:13:53.980 align:start position:0% course done for you and supplying all opinionated<00:13:43.950> choice<00:13:45.860> if<00:13:47.720> the<00:13:48.720> allowance<00:13:49.470> of<00:13:49.770> a 00:13:53.980 --> 00:13:53.990 align:start position:0% 00:13:53.990 --> 00:13:57.460 align:start position:0% particular<00:13:54.990> person<00:13:55.370> with<00:13:56.370> respect<00:13:56.490> to<00:13:56.820> some 00:13:57.460 --> 00:13:57.470 align:start position:0% particular person with respect to some 00:13:57.470 --> 00:14:03.710 align:start position:0% particular person with respect to some executors<00:13:58.470> is<00:13:59.480> the<00:14:00.480> max<00:14:00.750> possible<00:14:01.530> event<00:14:02.720> then 00:14:03.710 --> 00:14:03.720 align:start position:0% executors is the max possible event then 00:14:03.720 --> 00:14:07.850 align:start position:0% executors is the max possible event then transfer<00:14:04.560> from<00:14:04.800> should<00:14:05.700> not<00:14:05.910> decrease<00:14:06.860> the 00:14:07.850 --> 00:14:07.860 align:start position:0% transfer from should not decrease the 00:14:07.860 --> 00:14:14.030 align:start position:0% transfer from should not decrease the allowance<00:14:08.520> of<00:14:09.020> spending<00:14:12.470> okay<00:14:13.470> and<00:14:13.770> of<00:14:13.890> all 00:14:14.030 --> 00:14:14.040 align:start position:0% allowance of spending okay and of all 00:14:14.040 --> 00:14:17.660 align:start position:0% allowance of spending okay and of all the<00:14:14.190> submissions<00:14:14.370> are<00:14:14.790> due<00:14:14.820> it's<00:14:15.210> 125<00:14:16.670> let's 00:14:17.660 --> 00:14:17.670 align:start position:0% the submissions are due it's 125 let's 00:14:17.670 --> 00:14:22.400 align:start position:0% the submissions are due it's 125 let's go<00:14:17.790> over<00:14:17.880> the<00:14:17.970> space<00:14:20.180> hey<00:14:21.180> sure<00:14:21.420> yeah<00:14:21.720> so<00:14:22.140> I'll 00:14:22.400 --> 00:14:22.410 align:start position:0% go over the space hey sure yeah so I'll 00:14:22.410 --> 00:14:24.320 align:start position:0% go over the space hey sure yeah so I'll demo<00:14:22.860> it<00:14:23.010> down<00:14:23.130> the<00:14:23.400> specs<00:14:23.670> for<00:14:23.820> you<00:14:23.970> and<00:14:24.120> also 00:14:24.320 --> 00:14:24.330 align:start position:0% demo it down the specs for you and also 00:14:24.330 --> 00:14:26.300 align:start position:0% demo it down the specs for you and also have<00:14:24.480> a<00:14:24.510> CI<00:14:24.840> server<00:14:25.170> works<00:14:25.440> and<00:14:25.680> covering 00:14:26.300 --> 00:14:26.310 align:start position:0% have a CI server works and covering 00:14:26.310 --> 00:14:54.340 align:start position:0% have a CI server works and covering detail<00:14:27.170> everything<00:14:28.170> you<00:14:28.230> need<00:14:28.350> to<00:14:28.410> know<00:14:28.470> today 00:14:54.340 --> 00:14:54.350 align:start position:0% 00:14:54.350 --> 00:15:01.140 align:start position:0% [Music] 00:15:01.140 --> 00:15:01.150 align:start position:0% 00:15:01.150 --> 00:15:05.470 align:start position:0% [Music] 00:15:05.470 --> 00:15:05.480 align:start position:0% 00:15:05.480 --> 00:15:11.030 align:start position:0% can<00:15:06.480> you<00:15:06.600> see<00:15:06.779> this<00:15:08.930> is<00:15:09.930> the<00:15:10.140> size<00:15:10.380> okay<00:15:10.770> a 00:15:11.030 --> 00:15:11.040 align:start position:0% can you see this is the size okay a 00:15:11.040 --> 00:15:26.569 align:start position:0% can you see this is the size okay a little<00:15:11.399> bit<00:15:11.640> thick 00:15:26.569 --> 00:15:26.579 align:start position:0% 00:15:26.579 --> 00:15:28.009 align:start position:0% so<00:15:27.029> first<00:15:27.269> the<00:15:27.360> first<00:15:27.389> I<00:15:27.629> want<00:15:27.720> to<00:15:27.810> show<00:15:27.959> you 00:15:28.009 --> 00:15:28.019 align:start position:0% so first the first I want to show you 00:15:28.019 --> 00:15:29.960 align:start position:0% so first the first I want to show you the<00:15:28.170> structure<00:15:28.560> of<00:15:28.709> this<00:15:28.860> this<00:15:29.519> repo<00:15:29.879> has 00:15:29.960 --> 00:15:29.970 align:start position:0% the structure of this this repo has 00:15:29.970 --> 00:15:31.850 align:start position:0% the structure of this this repo has everyone<00:15:30.300> been<00:15:30.329> able<00:15:30.629> to<00:15:30.720> find<00:15:31.019> it<00:15:31.230> first<00:15:31.680> of 00:15:31.850 --> 00:15:31.860 align:start position:0% everyone been able to find it first of 00:15:31.860 --> 00:15:35.420 align:start position:0% everyone been able to find it first of all<00:15:31.949> so<00:15:32.699> we're<00:15:33.149> looking<00:15:33.449> for<00:15:34.279> looking<00:15:35.279> for 00:15:35.420 --> 00:15:35.430 align:start position:0% all so we're looking for looking for 00:15:35.430 --> 00:15:39.379 align:start position:0% all so we're looking for looking for this<00:15:35.550> repo<00:15:35.790> and<00:15:36.800> it<00:15:37.800> hasn't<00:15:38.120> and<00:15:39.120> I'm<00:15:39.209> gonna 00:15:39.379 --> 00:15:39.389 align:start position:0% this repo and it hasn't and I'm gonna 00:15:39.389 --> 00:15:42.259 align:start position:0% this repo and it hasn't and I'm gonna show<00:15:39.600> you<00:15:39.660> first<00:15:40.730> just<00:15:41.730> the<00:15:41.850> structure<00:15:42.180> of 00:15:42.259 --> 00:15:42.269 align:start position:0% show you first just the structure of 00:15:42.269 --> 00:15:47.030 align:start position:0% show you first just the structure of this<00:15:42.980> so<00:15:43.980> we've<00:15:44.459> got<00:15:45.379> going<00:15:46.379> here 00:15:47.030 --> 00:15:47.040 align:start position:0% this so we've got going here 00:15:47.040 --> 00:15:49.309 align:start position:0% this so we've got going here a<00:15:47.089> Romanian<00:15:48.089> configuration<00:15:48.810> finally<00:15:49.259> you 00:15:49.309 --> 00:15:49.319 align:start position:0% a Romanian configuration finally you 00:15:49.319 --> 00:15:52.730 align:start position:0% a Romanian configuration finally you don't<00:15:49.439> need<00:15:49.529> to<00:15:49.620> worry<00:15:49.740> about<00:15:50.000> and<00:15:51.620> the<00:15:52.620> most 00:15:52.730 --> 00:15:52.740 align:start position:0% don't need to worry about and the most 00:15:52.740 --> 00:15:53.809 align:start position:0% don't need to worry about and the most important<00:15:53.129> stuff<00:15:53.279> is<00:15:53.399> in<00:15:53.519> this<00:15:53.610> source 00:15:53.809 --> 00:15:53.819 align:start position:0% important stuff is in this source 00:15:53.819 --> 00:15:57.590 align:start position:0% important stuff is in this source directory<00:15:54.740> and<00:15:55.740> here<00:15:55.879> firstly<00:15:56.879> we<00:15:57.060> have<00:15:57.089> our 00:15:57.590 --> 00:15:57.600 align:start position:0% directory and here firstly we have our 00:15:57.600 --> 00:16:00.319 align:start position:0% directory and here firstly we have our specs<00:15:58.079> which<00:15:58.230> is<00:15:58.350> expected<00:15:58.829> of<00:15:58.949> me<00:15:59.100> and<00:15:59.939> this 00:16:00.319 --> 00:16:00.329 align:start position:0% specs which is expected of me and this 00:16:00.329 --> 00:16:01.939 align:start position:0% specs which is expected of me and this is<00:16:00.509> the<00:16:00.540> different<00:16:01.170> aspects<00:16:01.410> of<00:16:01.500> Martin<00:16:01.800> was 00:16:01.939 --> 00:16:01.949 align:start position:0% is the different aspects of Martin was 00:16:01.949 --> 00:16:05.269 align:start position:0% is the different aspects of Martin was right<00:16:02.660> -<00:16:03.660> this<00:16:04.529> is<00:16:04.649> red<00:16:04.769> there's<00:16:04.949> a<00:16:04.980> part-time 00:16:05.269 --> 00:16:05.279 align:start position:0% right - this is red there's a part-time 00:16:05.279 --> 00:16:06.920 align:start position:0% right - this is red there's a part-time files<00:16:05.550> it's<00:16:05.879> got<00:16:05.970> these<00:16:06.149> aspects<00:16:06.720> that<00:16:06.839> will 00:16:06.920 --> 00:16:06.930 align:start position:0% files it's got these aspects that will 00:16:06.930 --> 00:16:09.079 align:start position:0% files it's got these aspects that will be<00:16:07.050> tangled<00:16:07.500> tangled<00:16:08.250> out<00:16:08.310> of<00:16:08.430> it<00:16:08.550> you<00:16:08.850> do<00:16:08.970> not 00:16:09.079 --> 00:16:09.089 align:start position:0% be tangled tangled out of it you do not 00:16:09.089 --> 00:16:10.309 align:start position:0% be tangled tangled out of it you do not need<00:16:09.240> to<00:16:09.360> edit<00:16:09.449> this<00:16:09.689> because<00:16:09.990> this<00:16:10.079> is<00:16:10.199> the 00:16:10.309 --> 00:16:10.319 align:start position:0% need to edit this because this is the 00:16:10.319 --> 00:16:12.619 align:start position:0% need to edit this because this is the part<00:16:10.500> that's<00:16:10.699> that's<00:16:11.699> this<00:16:12.029> part<00:16:12.209> this<00:16:12.329> one<00:16:12.540> is 00:16:12.619 --> 00:16:12.629 align:start position:0% part that's that's this part this one is 00:16:12.629 --> 00:16:16.309 align:start position:0% part that's that's this part this one is given<00:16:13.439> to<00:16:13.560> you<00:16:13.649> for<00:16:13.949> a<00:16:15.110> but<00:16:16.110> you<00:16:16.199> do 00:16:16.309 --> 00:16:16.319 align:start position:0% given to you for a but you do 00:16:16.319 --> 00:16:17.990 align:start position:0% given to you for a but you do need<00:16:16.439> to<00:16:16.560> read<00:16:16.740> these<00:16:16.949> if<00:16:17.160> you<00:16:17.279> want<00:16:17.459> to<00:16:17.639> write 00:16:17.990 --> 00:16:18.000 align:start position:0% need to read these if you want to write 00:16:18.000 --> 00:16:21.230 align:start position:0% need to read these if you want to write limitations<00:16:18.629> over<00:16:18.810> actually<00:16:20.149> that<00:16:21.149> will 00:16:21.230 --> 00:16:21.240 align:start position:0% limitations over actually that will 00:16:21.240 --> 00:16:22.400 align:start position:0% limitations over actually that will actually<00:16:21.360> passed<00:16:21.750> it<00:16:22.019> makes<00:16:22.139> written 00:16:22.400 --> 00:16:22.410 align:start position:0% actually passed it makes written 00:16:22.410 --> 00:16:24.350 align:start position:0% actually passed it makes written understand<00:16:22.800> all<00:16:22.920> the<00:16:23.069> nuances<00:16:23.209> hopefully<00:16:24.209> not 00:16:24.350 --> 00:16:24.360 align:start position:0% understand all the nuances hopefully not 00:16:24.360 --> 00:16:28.179 align:start position:0% understand all the nuances hopefully not too<00:16:24.509> many<00:16:24.629> nuances<00:16:24.870> as<00:16:25.319> there<00:16:25.470> are<00:16:25.589> some<00:16:26.629> so 00:16:28.179 --> 00:16:28.189 align:start position:0% too many nuances as there are some so 00:16:28.189 --> 00:16:30.170 align:start position:0% too many nuances as there are some so partners<00:16:29.189> really<00:16:29.370> covered<00:16:29.699> how<00:16:29.790> these<00:16:29.939> specs 00:16:30.170 --> 00:16:30.180 align:start position:0% partners really covered how these specs 00:16:30.180 --> 00:16:31.280 align:start position:0% partners really covered how these specs book<00:16:30.360> but<00:16:30.540> I'll<00:16:30.660> make<00:16:30.779> you<00:16:30.899> just<00:16:31.019> pick<00:16:31.139> another 00:16:31.280 --> 00:16:31.290 align:start position:0% book but I'll make you just pick another 00:16:31.290 --> 00:16:33.379 align:start position:0% book but I'll make you just pick another one<00:16:31.470> and<00:16:31.620> quickly<00:16:31.920> don't<00:16:32.670> bring<00:16:32.790> any<00:16:33.029> other 00:16:33.379 --> 00:16:33.389 align:start position:0% one and quickly don't bring any other 00:16:33.389 --> 00:16:37.160 align:start position:0% one and quickly don't bring any other features<00:16:34.050> but<00:16:35.209> you<00:16:36.209> know<00:16:36.300> the<00:16:36.540> idea<00:16:36.930> is<00:16:36.990> you 00:16:37.160 --> 00:16:37.170 align:start position:0% features but you know the idea is you 00:16:37.170 --> 00:16:38.569 align:start position:0% features but you know the idea is you want<00:16:37.199> to<00:16:37.500> you<00:16:37.800> want<00:16:37.920> to<00:16:38.009> leave<00:16:38.220> these<00:16:38.370> and 00:16:38.569 --> 00:16:38.579 align:start position:0% want to you want to leave these and 00:16:38.579 --> 00:16:40.730 align:start position:0% want to you want to leave these and these<00:16:38.970> interface<00:16:39.629> lines<00:16:39.899> correspond<00:16:40.500> to<00:16:40.529> the 00:16:40.730 --> 00:16:40.740 align:start position:0% these interface lines correspond to the 00:16:40.740 --> 00:16:45.619 align:start position:0% these interface lines correspond to the familiar<00:16:41.009> DRC<00:16:42.000> 20<00:16:42.829> interfaces<00:16:43.829> and<00:16:44.389> we<00:16:45.389> use 00:16:45.619 --> 00:16:45.629 align:start position:0% familiar DRC 20 interfaces and we use 00:16:45.629 --> 00:16:51.049 align:start position:0% familiar DRC 20 interfaces and we use the<00:16:46.670> we<00:16:47.670> use<00:16:47.819> the<00:16:48.029> solidity<00:16:49.910> where<00:16:50.910> you<00:16:51.000> know 00:16:51.049 --> 00:16:51.059 align:start position:0% the we use the solidity where you know 00:16:51.059 --> 00:16:55.030 align:start position:0% the we use the solidity where you know detering<00:16:51.689> contract<00:16:52.139> ABI<00:16:52.439> for<00:16:53.120> competing 00:16:55.030 --> 00:16:55.040 align:start position:0% detering contract ABI for competing 00:16:55.040 --> 00:16:57.850 align:start position:0% detering contract ABI for competing you<00:16:55.250> know<00:16:55.340> need<00:16:55.460> to<00:16:55.490> face<00:16:56.140> selectors<00:16:57.140> from<00:16:57.530> the 00:16:57.850 --> 00:16:57.860 align:start position:0% you know need to face selectors from the 00:16:57.860 --> 00:17:01.210 align:start position:0% you know need to face selectors from the from<00:16:58.520> the<00:16:58.610> call<00:16:58.760> data<00:16:59.230> which<00:17:00.230> is<00:17:00.410> I<00:17:00.680> guess<00:17:00.920> you 00:17:01.210 --> 00:17:01.220 align:start position:0% from the call data which is I guess you 00:17:01.220 --> 00:17:02.890 align:start position:0% from the call data which is I guess you know<00:17:01.310> assume<00:17:01.700> but<00:17:02.030> basically<00:17:02.660> what<00:17:02.870> that 00:17:02.890 --> 00:17:02.900 align:start position:0% know assume but basically what that 00:17:02.900 --> 00:17:05.020 align:start position:0% know assume but basically what that means<00:17:03.170> is<00:17:03.320> that<00:17:03.350> if<00:17:04.280> you're<00:17:04.430> writing<00:17:04.640> the 00:17:05.020 --> 00:17:05.030 align:start position:0% means is that if you're writing the 00:17:05.030 --> 00:17:08.260 align:start position:0% means is that if you're writing the theoretical<00:17:05.959> total<00:17:06.230> supply<00:17:06.500> function<00:17:07.270> that 00:17:08.260 --> 00:17:08.270 align:start position:0% theoretical total supply function that 00:17:08.270 --> 00:17:12.130 align:start position:0% theoretical total supply function that means<00:17:08.449> that<00:17:08.839> the<00:17:09.730> force<00:17:10.730> four<00:17:11.030> bytes<00:17:11.270> the<00:17:11.959> call 00:17:12.130 --> 00:17:12.140 align:start position:0% means that the force four bytes the call 00:17:12.140 --> 00:17:16.150 align:start position:0% means that the force four bytes the call data<00:17:12.350> activity<00:17:13.390> the<00:17:14.390> shot<00:17:15.050> three<00:17:15.320> of<00:17:15.350> this 00:17:16.150 --> 00:17:16.160 align:start position:0% data activity the shot three of this 00:17:16.160 --> 00:17:20.770 align:start position:0% data activity the shot three of this string<00:17:17.110> has<00:17:18.110> to<00:17:18.230> be<00:17:18.350> something<00:17:18.709> like<00:17:18.800> this<00:17:19.780> so 00:17:20.770 --> 00:17:20.780 align:start position:0% string has to be something like this so 00:17:20.780 --> 00:17:22.780 align:start position:0% string has to be something like this so just<00:17:20.930> keep<00:17:21.440> that<00:17:21.470> in<00:17:21.620> mind<00:17:21.860> in<00:17:21.980> case<00:17:22.130> you're<00:17:22.339> in 00:17:22.780 --> 00:17:22.790 align:start position:0% just keep that in mind in case you're in 00:17:22.790 --> 00:17:24.310 align:start position:0% just keep that in mind in case you're in case<00:17:22.970> you're<00:17:23.209> wondering<00:17:23.329> how<00:17:23.660> however<00:17:24.260> a 00:17:24.310 --> 00:17:24.320 align:start position:0% case you're wondering how however a 00:17:24.320 --> 00:17:25.360 align:start position:0% case you're wondering how however a powder<00:17:24.500> like<00:17:24.650> this<00:17:24.680> of<00:17:24.949> course<00:17:25.130> if<00:17:25.250> you're 00:17:25.360 --> 00:17:25.370 align:start position:0% powder like this of course if you're 00:17:25.370 --> 00:17:28.570 align:start position:0% powder like this of course if you're ready<00:17:25.550> and<00:17:25.730> solidity<00:17:26.060> of<00:17:26.240> my<00:17:26.360> for<00:17:26.570> this<00:17:27.580> visit 00:17:28.570 --> 00:17:28.580 align:start position:0% ready and solidity of my for this visit 00:17:28.580 --> 00:17:34.150 align:start position:0% ready and solidity of my for this visit done<00:17:28.700> for<00:17:28.940> you<00:17:30.910> so<00:17:31.910> I<00:17:32.410> think<00:17:33.410> hopefully<00:17:33.830> these 00:17:34.150 --> 00:17:34.160 align:start position:0% done for you so I think hopefully these 00:17:34.160 --> 00:17:35.800 align:start position:0% done for you so I think hopefully these are<00:17:34.280> these<00:17:34.430> are<00:17:34.550> pretty<00:17:35.030> readable<00:17:35.270> the<00:17:35.600> best 00:17:35.800 --> 00:17:35.810 align:start position:0% are these are pretty readable the best 00:17:35.810 --> 00:17:38.980 align:start position:0% are these are pretty readable the best way<00:17:35.990> to<00:17:36.370> address<00:17:37.370> any<00:17:37.610> any<00:17:38.570> difficulties 00:17:38.980 --> 00:17:38.990 align:start position:0% way to address any any difficulties 00:17:38.990 --> 00:17:40.090 align:start position:0% way to address any any difficulties would<00:17:39.140> be<00:17:39.230> when<00:17:39.380> we<00:17:39.410> get<00:17:39.620> to<00:17:39.740> the<00:17:39.860> practical 00:17:40.090 --> 00:17:40.100 align:start position:0% would be when we get to the practical 00:17:40.100 --> 00:17:42.970 align:start position:0% would be when we get to the practical part<00:17:40.520> if<00:17:40.760> you<00:17:40.910> raise<00:17:41.240> your<00:17:41.270> hand<00:17:41.480> or<00:17:41.840> just<00:17:42.680> say 00:17:42.970 --> 00:17:42.980 align:start position:0% part if you raise your hand or just say 00:17:42.980 --> 00:17:45.370 align:start position:0% part if you raise your hand or just say something<00:17:43.310> and<00:17:43.430> we<00:17:43.520> can<00:17:43.670> discuss<00:17:44.380> discuss 00:17:45.370 --> 00:17:45.380 align:start position:0% something and we can discuss discuss 00:17:45.380 --> 00:17:49.810 align:start position:0% something and we can discuss discuss with<00:17:45.530> me<00:17:46.240> these<00:17:47.240> specimens<00:17:47.750> unclear<00:17:48.550> but<00:17:49.550> I 00:17:49.810 --> 00:17:49.820 align:start position:0% with me these specimens unclear but I 00:17:49.820 --> 00:17:52.510 align:start position:0% with me these specimens unclear but I mean<00:17:50.690> it<00:17:50.810> you<00:17:50.960> know<00:17:51.080> I<00:17:51.380> don't<00:17:52.160> either 00:17:52.510 --> 00:17:52.520 align:start position:0% mean it you know I don't either 00:17:52.520 --> 00:17:54.190 align:start position:0% mean it you know I don't either these<00:17:52.760> are<00:17:52.850> pretty<00:17:53.000> readable<00:17:53.210> so<00:17:53.600> you<00:17:53.930> can<00:17:54.050> see 00:17:54.190 --> 00:17:54.200 align:start position:0% these are pretty readable so you can see 00:17:54.200 --> 00:17:56.470 align:start position:0% these are pretty readable so you can see for<00:17:54.350> example<00:17:54.380> the<00:17:55.120> convention<00:17:56.120> with<00:17:56.300> the 00:17:56.470 --> 00:17:56.480 align:start position:0% for example the convention with the 00:17:56.480 --> 00:17:59.470 align:start position:0% for example the convention with the return<00:17:56.990> with<00:17:57.650> the<00:17:57.740> return<00:17:58.010> values<00:17:58.400> is<00:17:58.610> here<00:17:59.360> in 00:17:59.470 --> 00:17:59.480 align:start position:0% return with the return values is here in 00:17:59.480 --> 00:18:00.850 align:start position:0% return with the return values is here in this<00:17:59.570> last<00:17:59.780> night<00:17:59.960> at<00:18:00.110> the<00:18:00.170> bottom<00:18:00.470> means<00:18:00.650> you 00:18:00.850 --> 00:18:00.860 align:start position:0% this last night at the bottom means you 00:18:00.860 --> 00:18:06.970 align:start position:0% this last night at the bottom means you return<00:18:01.190> alive<00:18:01.400> in<00:18:01.640> this<00:18:01.730> things<00:18:02.860> success<00:18:05.980> so 00:18:06.970 --> 00:18:06.980 align:start position:0% return alive in this things success so 00:18:06.980 --> 00:18:08.410 align:start position:0% return alive in this things success so now<00:18:07.370> I<00:18:07.430> want<00:18:07.670> to<00:18:07.730> show<00:18:07.880> you<00:18:07.970> actually<00:18:08.090> how<00:18:08.270> to 00:18:08.410 --> 00:18:08.420 align:start position:0% now I want to show you actually how to 00:18:08.420 --> 00:18:10.960 align:start position:0% now I want to show you actually how to run<00:18:08.990> how<00:18:09.500> to<00:18:09.560> run<00:18:09.800> this<00:18:09.920> with<00:18:10.100> your<00:18:10.250> own<00:18:10.400> 0 00:18:10.960 --> 00:18:10.970 align:start position:0% run how to run this with your own 0 00:18:10.970 --> 00:18:14.440 align:start position:0% run how to run this with your own 0 implementation<00:18:12.550> so<00:18:13.550> if<00:18:13.790> you<00:18:13.910> go<00:18:14.030> back<00:18:14.210> to<00:18:14.360> this 00:18:14.440 --> 00:18:14.450 align:start position:0% implementation so if you go back to this 00:18:14.450 --> 00:18:17.440 align:start position:0% implementation so if you go back to this you<00:18:14.900> go<00:18:14.960> message<00:18:15.230> source<00:18:15.470> directory<00:18:16.450> you'll 00:18:17.440 --> 00:18:17.450 align:start position:0% you go message source directory you'll 00:18:17.450 --> 00:18:20.860 align:start position:0% you go message source directory you'll see<00:18:17.600> some<00:18:17.750> other<00:18:17.840> files<00:18:18.430> and<00:18:19.570> the<00:18:20.570> most 00:18:20.860 --> 00:18:20.870 align:start position:0% see some other files and the most 00:18:20.870 --> 00:18:22.510 align:start position:0% see some other files and the most important<00:18:21.290> one<00:18:21.380> for<00:18:21.410> you<00:18:21.680> to<00:18:21.770> edit<00:18:22.100> is<00:18:22.310> this 00:18:22.510 --> 00:18:22.520 align:start position:0% important one for you to edit is this 00:18:22.520 --> 00:18:25.390 align:start position:0% important one for you to edit is this file<00:18:22.760> in<00:18:23.060> runtime<00:18:23.710> which<00:18:24.710> contains<00:18:25.220> the 00:18:25.390 --> 00:18:25.400 align:start position:0% file in runtime which contains the 00:18:25.400 --> 00:18:28.330 align:start position:0% file in runtime which contains the runtime<00:18:25.840> byte<00:18:26.840> code<00:18:27.080> of<00:18:27.410> your<00:18:27.560> your 00:18:28.330 --> 00:18:28.340 align:start position:0% runtime byte code of your your 00:18:28.340 --> 00:18:30.040 align:start position:0% runtime byte code of your your submission<00:18:28.820> we<00:18:29.030> see<00:18:29.180> there's<00:18:29.450> already<00:18:29.600> one<00:18:29.900> in 00:18:30.040 --> 00:18:30.050 align:start position:0% submission we see there's already one in 00:18:30.050 --> 00:18:34.480 align:start position:0% submission we see there's already one in here<00:18:30.400> which<00:18:31.400> is<00:18:32.710> which<00:18:33.710> is<00:18:33.740> the<00:18:33.890> sample<00:18:34.160> one 00:18:34.480 --> 00:18:34.490 align:start position:0% here which is which is the sample one 00:18:34.490 --> 00:18:36.700 align:start position:0% here which is which is the sample one has<00:18:34.610> provided<00:18:34.910> this<00:18:35.180> is<00:18:35.390> coming<00:18:36.050> from<00:18:36.080> a<00:18:36.320> basic 00:18:36.700 --> 00:18:36.710 align:start position:0% has provided this is coming from a basic 00:18:36.710 --> 00:18:40.720 align:start position:0% has provided this is coming from a basic solidity<00:18:38.230> implementation<00:18:39.230> the<00:18:40.160> source<00:18:40.460> of 00:18:40.720 --> 00:18:40.730 align:start position:0% solidity implementation the source of 00:18:40.730 --> 00:18:44.610 align:start position:0% solidity implementation the source of which<00:18:40.970> is 00:18:44.610 --> 00:18:44.620 align:start position:0% 00:18:44.620 --> 00:18:47.560 align:start position:0% it's<00:18:45.620> in<00:18:45.770> the<00:18:45.950> it's<00:18:46.790> in<00:18:46.910> the<00:18:47.000> rebuilding<00:18:47.420> that 00:18:47.560 --> 00:18:47.570 align:start position:0% it's in the it's in the rebuilding that 00:18:47.570 --> 00:18:51.160 align:start position:0% it's in the it's in the rebuilding that they<00:18:47.720> their<00:18:48.560> injury<00:18:48.800> so<00:18:49.610> we<00:18:49.640> go<00:18:49.850> on<00:18:49.880> below<00:18:50.180> yeah 00:18:51.160 --> 00:18:51.170 align:start position:0% they their injury so we go on below yeah 00:18:51.170 --> 00:18:55.720 align:start position:0% they their injury so we go on below yeah it's<00:18:52.040> okay<00:18:52.280> so<00:18:52.720> this<00:18:53.720> is<00:18:53.900> like<00:18:53.930> the<00:18:54.170> par<00:18:54.730> that 00:18:55.720 --> 00:18:55.730 align:start position:0% it's okay so this is like the par that 00:18:55.730 --> 00:18:58.240 align:start position:0% it's okay so this is like the par that you<00:18:56.180> can<00:18:57.020> compare<00:18:57.500> yourself<00:18:57.860> against<00:18:58.190> a 00:18:58.240 --> 00:18:58.250 align:start position:0% you can compare yourself against a 00:18:58.250 --> 00:19:02.440 align:start position:0% you can compare yourself against a beggar<00:18:58.660> and<00:18:59.830> it<00:19:00.830> also<00:19:01.000> assist<00:19:02.000> you<00:19:02.060> if<00:19:02.240> you 00:19:02.440 --> 00:19:02.450 align:start position:0% beggar and it also assist you if you 00:19:02.450 --> 00:19:04.510 align:start position:0% beggar and it also assist you if you find<00:19:02.870> some<00:19:03.140> expert<00:19:03.470> to<00:19:03.590> rethink<00:19:03.920> things<00:19:04.160> have 00:19:04.510 --> 00:19:04.520 align:start position:0% find some expert to rethink things have 00:19:04.520 --> 00:19:06.940 align:start position:0% find some expert to rethink things have to<00:19:04.670> read<00:19:04.820> this<00:19:04.940> way<00:19:05.150> to<00:19:05.210> you<00:19:05.530> get<00:19:06.530> a<00:19:06.590> handle<00:19:06.860> on 00:19:06.940 --> 00:19:06.950 align:start position:0% to read this way to you get a handle on 00:19:06.950 --> 00:19:07.690 align:start position:0% to read this way to you get a handle on what's<00:19:07.130> going<00:19:07.190> on 00:19:07.690 --> 00:19:07.700 align:start position:0% what's going on 00:19:07.700 --> 00:19:10.300 align:start position:0% what's going on yes<00:19:08.240> so<00:19:08.660> to<00:19:08.720> be<00:19:08.870> clear<00:19:08.990> this<00:19:09.290> this<00:19:09.740> solidity 00:19:10.300 --> 00:19:10.310 align:start position:0% yes so to be clear this this solidity 00:19:10.310 --> 00:19:13.390 align:start position:0% yes so to be clear this this solidity that's<00:19:10.550> in<00:19:10.700> the<00:19:10.880> in<00:19:11.390> the<00:19:11.720> root<00:19:12.470> of<00:19:12.560> this<00:19:12.680> git 00:19:13.390 --> 00:19:13.400 align:start position:0% that's in the in the root of this git 00:19:13.400 --> 00:19:15.880 align:start position:0% that's in the in the root of this git repo<00:19:13.670> passes<00:19:14.270> the<00:19:14.390> specs<00:19:14.720> so<00:19:14.990> your<00:19:15.320> your<00:19:15.680> your 00:19:15.880 --> 00:19:15.890 align:start position:0% repo passes the specs so your your your 00:19:15.890 --> 00:19:17.410 align:start position:0% repo passes the specs so your your your thing<00:19:16.100> needs<00:19:16.280> to<00:19:16.340> be<00:19:16.400> behavioral<00:19:16.760> equivalent 00:19:17.410 --> 00:19:17.420 align:start position:0% thing needs to be behavioral equivalent 00:19:17.420 --> 00:19:21.030 align:start position:0% thing needs to be behavioral equivalent to<00:19:18.110> this<00:19:18.200> stuff<00:19:18.740> this<00:19:18.890> is<00:19:18.950> one<00:19:19.250> way<00:19:19.400> to<00:19:19.930> check 00:19:21.030 --> 00:19:21.040 align:start position:0% to this stuff this is one way to check 00:19:21.040 --> 00:19:23.650 align:start position:0% to this stuff this is one way to check and<00:19:22.040> except<00:19:22.490> for<00:19:22.580> the<00:19:22.670> constructor<00:19:23.180> which<00:19:23.390> we 00:19:23.650 --> 00:19:23.660 align:start position:0% and except for the constructor which we 00:19:23.660 --> 00:19:26.440 align:start position:0% and except for the constructor which we will<00:19:23.810> not<00:19:23.960> be<00:19:24.490> verifying<00:19:25.490> you<00:19:25.910> don't<00:19:26.090> need<00:19:26.270> to 00:19:26.440 --> 00:19:26.450 align:start position:0% will not be verifying you don't need to 00:19:26.450 --> 00:19:27.970 align:start position:0% will not be verifying you don't need to you<00:19:26.690> know<00:19:26.780> you<00:19:26.990> need<00:19:27.260> to<00:19:27.380> worry<00:19:27.530> about<00:19:27.770> how<00:19:27.920> to 00:19:27.970 --> 00:19:27.980 align:start position:0% you know you need to worry about how to 00:19:27.980 --> 00:19:30.390 align:start position:0% you know you need to worry about how to have<00:19:28.430> this<00:19:28.550> contracts<00:19:29.030> deployed<00:19:29.390> to<00:19:30.050> where<00:19:30.170> a 00:19:30.390 --> 00:19:30.400 align:start position:0% have this contracts deployed to where a 00:19:30.400 --> 00:19:34.610 align:start position:0% have this contracts deployed to where a transitional<00:19:31.400> process<00:19:31.640> to<00:19:31.940> play<00:19:32.060> out 00:19:34.610 --> 00:19:34.620 align:start position:0% 00:19:34.620 --> 00:19:37.460 align:start position:0% right<00:19:35.279> so<00:19:35.429> going<00:19:35.610> back<00:19:35.820> to<00:19:35.880> this<00:19:36.350> what<00:19:37.350> you 00:19:37.460 --> 00:19:37.470 align:start position:0% right so going back to this what you 00:19:37.470 --> 00:19:39.409 align:start position:0% right so going back to this what you need<00:19:37.650> to<00:19:37.740> do<00:19:37.860> is<00:19:38.010> put<00:19:38.250> your<00:19:38.400> put<00:19:39.090> your<00:19:39.150> bank 00:19:39.409 --> 00:19:39.419 align:start position:0% need to do is put your put your bank 00:19:39.419 --> 00:19:42.260 align:start position:0% need to do is put your put your bank code<00:19:39.630> into<00:19:39.929> into<00:19:40.380> this<00:19:40.500> pot<00:19:40.740> so<00:19:41.580> you<00:19:41.610> can<00:19:41.850> even 00:19:42.260 --> 00:19:42.270 align:start position:0% code into into this pot so you can even 00:19:42.270 --> 00:19:44.930 align:start position:0% code into into this pot so you can even doing<00:19:42.539> this<00:19:42.630> fund<00:19:42.900> and<00:19:43.230> up<00:19:43.350> with<00:19:43.559> your<00:19:43.940> during 00:19:44.930 --> 00:19:44.940 align:start position:0% doing this fund and up with your during 00:19:44.940 --> 00:19:48.320 align:start position:0% doing this fund and up with your during fight<00:19:45.179> card<00:19:45.450> into<00:19:46.409> it<00:19:46.760> and<00:19:47.760> I<00:19:47.820> think<00:19:47.880> you're 00:19:48.320 --> 00:19:48.330 align:start position:0% fight card into it and I think you're 00:19:48.330 --> 00:19:50.299 align:start position:0% fight card into it and I think you're actually<00:19:48.570> Lancet<00:19:49.140> because<00:19:49.650> if<00:19:49.740> you<00:19:49.919> you<00:19:50.220> know 00:19:50.299 --> 00:19:50.309 align:start position:0% actually Lancet because if you you know 00:19:50.309 --> 00:19:51.950 align:start position:0% actually Lancet because if you you know as<00:19:50.850> you'll<00:19:51.000> see<00:19:51.120> in<00:19:51.179> the<00:19:51.270> repo<00:19:51.570> to<00:19:51.809> this 00:19:51.950 --> 00:19:51.960 align:start position:0% as you'll see in the repo to this 00:19:51.960 --> 00:19:54.890 align:start position:0% as you'll see in the repo to this pimping<00:19:52.500> me<00:19:52.650> there<00:19:52.980> remain<00:19:53.279> this<00:19:53.429> repo<00:19:53.900> here's 00:19:54.890 --> 00:19:54.900 align:start position:0% pimping me there remain this repo here's 00:19:54.900 --> 00:20:02.390 align:start position:0% pimping me there remain this repo here's how<00:19:55.110> you<00:19:55.169> do<00:19:55.409> that<00:19:55.440> with<00:19:56.750> so<00:19:57.750> steep<00:20:00.980> say<00:20:01.980> I'll 00:20:02.390 --> 00:20:02.400 align:start position:0% how you do that with so steep say I'll 00:20:02.400 --> 00:20:07.070 align:start position:0% how you do that with so steep say I'll see<00:20:02.610> with<00:20:02.880> all<00:20:03.809> studies<00:20:04.169> associate<00:20:04.830> to<00:20:06.080> Dante 00:20:07.070 --> 00:20:07.080 align:start position:0% see with all studies associate to Dante 00:20:07.080 --> 00:20:10.760 align:start position:0% see with all studies associate to Dante you'll<00:20:07.520> tend<00:20:08.520> to<00:20:08.669> do<00:20:09.240> up<00:20:09.419> in<00:20:09.690> stimul<00:20:10.289> and<00:20:10.620> have 00:20:10.760 --> 00:20:10.770 align:start position:0% you'll tend to do up in stimul and have 00:20:10.770 --> 00:20:14.450 align:start position:0% you'll tend to do up in stimul and have the<00:20:10.980> effect<00:20:11.610> good<00:20:12.320> and<00:20:13.320> these<00:20:14.190> are<00:20:14.309> the 00:20:14.450 --> 00:20:14.460 align:start position:0% the effect good and these are the 00:20:14.460 --> 00:20:16.340 align:start position:0% the effect good and these are the instructions<00:20:14.880> before<00:20:14.970> survivor<00:20:15.690> and<00:20:16.020> maybe 00:20:16.340 --> 00:20:16.350 align:start position:0% instructions before survivor and maybe 00:20:16.350 --> 00:20:19.399 align:start position:0% instructions before survivor and maybe you<00:20:16.500> have<00:20:16.649> your<00:20:16.770> own<00:20:16.880> funny<00:20:17.880> tools<00:20:18.320> that<00:20:19.320> you 00:20:19.399 --> 00:20:19.409 align:start position:0% you have your own funny tools that you 00:20:19.409 --> 00:20:23.720 align:start position:0% you have your own funny tools that you want<00:20:19.590> to<00:20:19.710> try<00:20:21.590> so<00:20:22.590> it<00:20:22.770> actually<00:20:22.890> makes<00:20:23.460> a<00:20:23.549> lot 00:20:23.720 --> 00:20:23.730 align:start position:0% want to try so it actually makes a lot 00:20:23.730 --> 00:20:26.120 align:start position:0% want to try so it actually makes a lot of<00:20:23.970> this<00:20:24.450> header<00:20:24.720> but<00:20:24.960> it's<00:20:25.110> not<00:20:25.320> necessary<00:20:25.830> so 00:20:26.120 --> 00:20:26.130 align:start position:0% of this header but it's not necessary so 00:20:26.130 --> 00:20:29.419 align:start position:0% of this header but it's not necessary so you<00:20:26.549> know<00:20:26.669> simply<00:20:27.510> having<00:20:27.870> me<00:20:28.049> the<00:20:28.860> hex<00:20:29.130> in 00:20:29.419 --> 00:20:29.429 align:start position:0% you know simply having me the hex in 00:20:29.429 --> 00:20:39.470 align:start position:0% you know simply having me the hex in here<00:20:29.700> as<00:20:29.940> a<00:20:30.240> ski<00:20:30.539> is<00:20:35.840> how<00:20:37.789> house<00:20:38.789> house<00:20:39.270> I'll 00:20:39.470 --> 00:20:39.480 align:start position:0% here as a ski is how house house I'll 00:20:39.480 --> 00:20:40.750 align:start position:0% here as a ski is how house house I'll see<00:20:39.630> you<00:20:39.690> out<00:20:39.870> there 00:20:40.750 --> 00:20:40.760 align:start position:0% see you out there 00:20:40.760 --> 00:20:44.810 align:start position:0% see you out there so<00:20:41.760> now<00:20:42.270> I<00:20:42.299> will<00:20:42.600> show<00:20:42.809> you<00:20:42.840> how<00:20:43.350> this<00:20:43.529> gets<00:20:43.830> how 00:20:44.810 --> 00:20:44.820 align:start position:0% so now I will show you how this gets how 00:20:44.820 --> 00:20:53.240 align:start position:0% so now I will show you how this gets how does<00:20:44.970> gets<00:20:45.149> processed<00:20:51.529> so<00:20:52.529> it's<00:20:52.980> kind<00:20:53.159> of 00:20:53.240 --> 00:20:53.250 align:start position:0% does gets processed so it's kind of 00:20:53.250 --> 00:20:56.659 align:start position:0% does gets processed so it's kind of happened<00:20:53.610> when<00:20:53.760> you<00:20:54.500> when<00:20:55.500> you<00:20:55.590> submit<00:20:56.039> a<00:20:56.070> poor 00:20:56.659 --> 00:20:56.669 align:start position:0% happened when you when you submit a poor 00:20:56.669 --> 00:20:58.610 align:start position:0% happened when you when you submit a poor west<00:20:57.029> where<00:20:57.270> you've<00:20:57.390> ended<00:20:57.539> this<00:20:57.899> in<00:20:58.289> runtime 00:20:58.610 --> 00:20:58.620 align:start position:0% west where you've ended this in runtime 00:20:58.620 --> 00:21:02.450 align:start position:0% west where you've ended this in runtime the<00:20:59.070> file<00:20:59.340> is<00:21:00.120> our<00:21:01.080> our<00:21:01.470> CI<00:21:01.710> server<00:21:01.830> will 00:21:02.450 --> 00:21:02.460 align:start position:0% the file is our our CI server will 00:21:02.460 --> 00:21:05.960 align:start position:0% the file is our our CI server will automatically<00:21:03.059> pick<00:21:03.299> up<00:21:03.480> the<00:21:04.370> floor<00:21:05.370> but<00:21:05.610> and 00:21:05.960 --> 00:21:05.970 align:start position:0% automatically pick up the floor but and 00:21:05.970 --> 00:21:08.690 align:start position:0% automatically pick up the floor but and it's<00:21:06.870> going<00:21:07.110> to<00:21:07.380> run<00:21:07.890> the<00:21:08.220> K<00:21:08.340> framework 00:21:08.690 --> 00:21:08.700 align:start position:0% it's going to run the K framework 00:21:08.700 --> 00:21:12.139 align:start position:0% it's going to run the K framework groomer<00:21:09.200> using<00:21:10.200> the<00:21:10.289> specs<00:21:10.590> generated<00:21:11.159> from 00:21:12.139 --> 00:21:12.149 align:start position:0% groomer using the specs generated from 00:21:12.149 --> 00:21:16.220 align:start position:0% groomer using the specs generated from the<00:21:12.570> Riviera<00:21:13.500> language<00:21:13.909> against<00:21:14.909> your<00:21:15.230> guest 00:21:16.220 --> 00:21:16.230 align:start position:0% the Riviera language against your guest 00:21:16.230 --> 00:21:20.060 align:start position:0% the Riviera language against your guest or<00:21:16.380> effective<00:21:16.799> and<00:21:18.620> then<00:21:19.620> after<00:21:19.980> that 00:21:20.060 --> 00:21:20.070 align:start position:0% or effective and then after that 00:21:20.070 --> 00:21:23.299 align:start position:0% or effective and then after that execution<00:21:20.610> is<00:21:20.669> done<00:21:21.620> you<00:21:22.620> know<00:21:22.710> here's<00:21:23.220> an 00:21:23.299 --> 00:21:23.309 align:start position:0% execution is done you know here's an 00:21:23.309 --> 00:21:25.460 align:start position:0% execution is done you know here's an example<00:21:23.520> where<00:21:23.820> this<00:21:23.909> guy<00:21:24.090> running<00:21:24.419> when<00:21:25.350> his 00:21:25.460 --> 00:21:25.470 align:start position:0% example where this guy running when his 00:21:25.470 --> 00:21:27.740 align:start position:0% example where this guy running when his execution<00:21:25.860> is<00:21:25.919> done 00:21:27.740 --> 00:21:27.750 align:start position:0% execution is done 00:21:27.750 --> 00:21:30.860 align:start position:0% execution is done a<00:21:27.799> successful<00:21:28.799> proof<00:21:29.520> all<00:21:29.789> of<00:21:29.880> the<00:21:30.030> all<00:21:30.690> the 00:21:30.860 --> 00:21:30.870 align:start position:0% a successful proof all of the all the 00:21:30.870 --> 00:21:32.240 align:start position:0% a successful proof all of the all the specs<00:21:31.200> eligibility<00:21:31.919> things<00:21:32.130> were 00:21:32.240 --> 00:21:32.250 align:start position:0% specs eligibility things were 00:21:32.250 --> 00:21:36.440 align:start position:0% specs eligibility things were successfully<00:21:32.700> perfect<00:21:33.590> you<00:21:34.590> will<00:21:35.330> it<00:21:36.330> will 00:21:36.440 --> 00:21:36.450 align:start position:0% successfully perfect you will it will 00:21:36.450 --> 00:21:39.649 align:start position:0% successfully perfect you will it will actually<00:21:36.539> do<00:21:36.870> a<00:21:37.370> as<00:21:38.370> a<00:21:38.429> symbolic<00:21:38.940> analysis<00:21:39.510> of 00:21:39.649 --> 00:21:39.659 align:start position:0% actually do a as a symbolic analysis of 00:21:39.659 --> 00:21:41.029 align:start position:0% actually do a as a symbolic analysis of the<00:21:39.780> the<00:21:40.230> gas<00:21:40.409> with<00:21:40.620> all<00:21:40.740> of<00:21:40.830> all<00:21:40.950> these 00:21:41.029 --> 00:21:41.039 align:start position:0% the the gas with all of all these 00:21:41.039 --> 00:21:43.010 align:start position:0% the the gas with all of all these execution<00:21:41.549> traces<00:21:41.850> and<00:21:42.179> a<00:21:42.390> little<00:21:42.600> calculate 00:21:43.010 --> 00:21:43.020 align:start position:0% execution traces and a little calculate 00:21:43.020 --> 00:21:44.960 align:start position:0% execution traces and a little calculate the<00:21:43.110> product<00:21:43.320> is<00:21:43.500> run<00:21:43.679> seventy<00:21:44.100> the<00:21:44.610> maximum 00:21:44.960 --> 00:21:44.970 align:start position:0% the product is run seventy the maximum 00:21:44.970 --> 00:21:46.880 align:start position:0% the product is run seventy the maximum caskets<00:21:45.390> and<00:21:45.840> then<00:21:46.380> there<00:21:46.530> would<00:21:46.590> be<00:21:46.650> a<00:21:46.740> report 00:21:46.880 --> 00:21:46.890 align:start position:0% caskets and then there would be a report 00:21:46.890 --> 00:21:50.149 align:start position:0% caskets and then there would be a report produced<00:21:47.250> so<00:21:48.090> here<00:21:48.659> once<00:21:49.080> you<00:21:49.169> wonder<00:21:49.380> we<00:21:49.980> can 00:21:50.149 --> 00:21:50.159 align:start position:0% produced so here once you wonder we can 00:21:50.159 --> 00:21:51.860 align:start position:0% produced so here once you wonder we can track<00:21:50.460> your<00:21:50.610> progress<00:21:50.789> you<00:21:51.150> can<00:21:51.270> go<00:21:51.419> to<00:21:51.480> adapt 00:21:51.860 --> 00:21:51.870 align:start position:0% track your progress you can go to adapt 00:21:51.870 --> 00:21:55.159 align:start position:0% track your progress you can go to adapt on<00:21:52.080> CI<00:21:52.320> slash<00:21:52.799> GRC<00:21:53.159> 20<00:21:53.640> -<00:21:54.090> golf 00:21:55.159 --> 00:21:55.169 align:start position:0% on CI slash GRC 20 - golf 00:21:55.169 --> 00:21:57.529 align:start position:0% on CI slash GRC 20 - golf they're<00:21:55.530> here<00:21:55.740> for<00:21:55.919> every<00:21:56.280> for<00:21:57.179> every<00:21:57.210> law 00:21:57.529 --> 00:21:57.539 align:start position:0% they're here for every for every law 00:21:57.539 --> 00:22:02.680 align:start position:0% they're here for every for every law request<00:21:57.840> this<00:21:58.020> repo<00:21:58.380> there<00:21:58.679> will<00:21:58.799> be<00:21:58.830> a<00:22:01.610> hat 00:22:02.680 --> 00:22:02.690 align:start position:0% request this repo there will be a hat 00:22:02.690 --> 00:22:05.960 align:start position:0% request this repo there will be a hat which<00:22:03.690> is<00:22:03.720> your<00:22:03.960> entry<00:22:04.460> as<00:22:05.460> you<00:22:05.549> can<00:22:05.669> see<00:22:05.789> here 00:22:05.960 --> 00:22:05.970 align:start position:0% which is your entry as you can see here 00:22:05.970 --> 00:22:08.960 align:start position:0% which is your entry as you can see here they're<00:22:06.120> the<00:22:06.690> last<00:22:06.960> one<00:22:07.260> was<00:22:07.380> in<00:22:07.409> 1042<00:22:08.070> and<00:22:08.789> if 00:22:08.960 --> 00:22:08.970 align:start position:0% they're the last one was in 1042 and if 00:22:08.970 --> 00:22:10.250 align:start position:0% they're the last one was in 1042 and if you<00:22:09.120> know<00:22:09.570> if<00:22:09.690> you<00:22:09.780> look<00:22:09.900> on<00:22:10.020> the<00:22:10.110> right-hand 00:22:10.250 --> 00:22:10.260 align:start position:0% you know if you look on the right-hand 00:22:10.260 --> 00:22:13.180 align:start position:0% you know if you look on the right-hand side<00:22:10.440> you'll<00:22:10.710> see<00:22:10.740> that<00:22:10.950> there<00:22:11.610> are<00:22:11.640> 16 00:22:13.180 --> 00:22:13.190 align:start position:0% side you'll see that there are 16 00:22:13.190 --> 00:22:15.820 align:start position:0% side you'll see that there are 16 aspects<00:22:14.190> in<00:22:14.309> total<00:22:14.640> and<00:22:14.760> 16<00:22:15.059> of<00:22:15.179> them<00:22:15.330> were 00:22:15.820 --> 00:22:15.830 align:start position:0% aspects in total and 16 of them were 00:22:15.830 --> 00:22:17.899 align:start position:0% aspects in total and 16 of them were where<00:22:16.830> accepted<00:22:17.220> being<00:22:17.400> that<00:22:17.610> this<00:22:17.700> is<00:22:17.850> a 00:22:17.899 --> 00:22:17.909 align:start position:0% where accepted being that this is a 00:22:17.909 --> 00:22:19.430 align:start position:0% where accepted being that this is a correct<00:22:18.210> implementation<00:22:18.450> has<00:22:19.080> been<00:22:19.110> formed 00:22:19.430 --> 00:22:19.440 align:start position:0% correct implementation has been formed 00:22:19.440 --> 00:22:22.220 align:start position:0% correct implementation has been formed an<00:22:19.530> air<00:22:19.650> pipe<00:22:20.030> and<00:22:21.030> now<00:22:21.480> if<00:22:21.600> you<00:22:21.720> click<00:22:21.870> on<00:22:22.110> this 00:22:22.220 --> 00:22:22.230 align:start position:0% an air pipe and now if you click on this 00:22:22.230 --> 00:22:24.230 align:start position:0% an air pipe and now if you click on this link<00:22:22.530> well<00:22:23.309> you'll<00:22:23.549> be<00:22:23.580> able<00:22:23.760> to<00:22:23.940> see<00:22:24.120> an 00:22:24.230 --> 00:22:24.240 align:start position:0% link well you'll be able to see an 00:22:24.240 --> 00:22:27.289 align:start position:0% link well you'll be able to see an overview<00:22:24.809> of<00:22:25.200> coloring<00:22:25.830> past<00:22:26.100> but<00:22:26.490> also<00:22:26.730> very 00:22:27.289 --> 00:22:27.299 align:start position:0% overview of coloring past but also very 00:22:27.299 --> 00:22:30.049 align:start position:0% overview of coloring past but also very importantly<00:22:28.100> you'll<00:22:29.100> see<00:22:29.190> next<00:22:29.549> to<00:22:29.760> every 00:22:30.049 --> 00:22:30.059 align:start position:0% importantly you'll see next to every 00:22:30.059 --> 00:22:34.630 align:start position:0% importantly you'll see next to every extra<00:22:30.960> every<00:22:31.260> passing<00:22:31.799> behavior<00:22:33.140> you'll<00:22:34.140> see 00:22:34.630 --> 00:22:34.640 align:start position:0% extra every passing behavior you'll see 00:22:34.640 --> 00:22:37.610 align:start position:0% extra every passing behavior you'll see here<00:22:35.640> on<00:22:35.850> the<00:22:36.030> on<00:22:36.450> the<00:22:36.960> right<00:22:37.140> you'll<00:22:37.289> see<00:22:37.320> gas 00:22:37.610 --> 00:22:37.620 align:start position:0% here on the on the right you'll see gas 00:22:37.620 --> 00:22:39.200 align:start position:0% here on the on the right you'll see gas and<00:22:37.890> gas<00:22:37.980> analysis<00:22:38.549> so<00:22:38.700> I<00:22:38.730> want<00:22:38.970> to<00:22:39.000> show<00:22:39.150> you 00:22:39.200 --> 00:22:39.210 align:start position:0% and gas analysis so I want to show you 00:22:39.210 --> 00:22:43.070 align:start position:0% and gas analysis so I want to show you these<00:22:39.470> so<00:22:40.470> gas<00:22:40.740> is<00:22:41.240> a<00:22:42.240> bit<00:22:42.450> technical<00:22:42.630> that 00:22:43.070 --> 00:22:43.080 align:start position:0% these so gas is a bit technical that 00:22:43.080 --> 00:22:47.210 align:start position:0% these so gas is a bit technical that this<00:22:43.260> is<00:22:44.270> the<00:22:45.270> decay<00:22:45.929> term<00:22:46.289> the<00:22:46.559> new<00:22:46.679> extracted 00:22:47.210 --> 00:22:47.220 align:start position:0% this is the decay term the new extracted 00:22:47.220 --> 00:22:48.770 align:start position:0% this is the decay term the new extracted from<00:22:47.400> the<00:22:47.669> smoking<00:22:47.970> execution<00:22:48.570> that 00:22:48.770 --> 00:22:48.780 align:start position:0% from the smoking execution that 00:22:48.780 --> 00:22:51.740 align:start position:0% from the smoking execution that represents<00:22:49.740> the<00:22:50.059> state<00:22:51.059> of<00:22:51.120> the<00:22:51.240> gas<00:22:51.480> at<00:22:51.720> the 00:22:51.740 --> 00:22:51.750 align:start position:0% represents the state of the gas at the 00:22:51.750 --> 00:22:53.630 align:start position:0% represents the state of the gas at the end<00:22:51.960> of<00:22:52.140> the<00:22:52.620> end<00:22:52.740> of<00:22:52.890> every<00:22:53.130> execution<00:22:53.340> to 00:22:53.630 --> 00:22:53.640 align:start position:0% end of the end of every execution to 00:22:53.640 --> 00:22:55.220 align:start position:0% end of the end of every execution to this<00:22:53.760> dysfunction<00:22:54.750> the<00:22:54.870> reason<00:22:55.049> this<00:22:55.110> has 00:22:55.220 --> 00:22:55.230 align:start position:0% this dysfunction the reason this has 00:22:55.230 --> 00:22:56.360 align:start position:0% this dysfunction the reason this has been<00:22:55.320> complicated<00:22:55.830> because<00:22:56.039> there's<00:22:56.280> going 00:22:56.360 --> 00:22:56.370 align:start position:0% been complicated because there's going 00:22:56.370 --> 00:22:57.529 align:start position:0% been complicated because there's going to<00:22:56.429> be<00:22:56.490> branching<00:22:56.909> it<00:22:57.059> here<00:22:57.210> it's<00:22:57.360> going<00:22:57.480> to 00:22:57.529 --> 00:22:57.539 align:start position:0% to be branching it here it's going to 00:22:57.539 --> 00:23:00.020 align:start position:0% to be branching it here it's going to depend<00:22:57.780> on<00:22:57.960> the<00:22:58.190> state<00:22:59.190> state<00:22:59.490> of<00:22:59.580> the<00:22:59.669> data 00:23:00.020 --> 00:23:00.030 align:start position:0% depend on the state state of the data 00:23:00.030 --> 00:23:01.940 align:start position:0% depend on the state state of the data but<00:23:00.929> that's<00:23:01.049> not<00:23:01.289> a<00:23:01.320> little<00:23:01.380> bit<00:23:01.559> hard<00:23:01.740> to<00:23:01.770> read 00:23:01.940 --> 00:23:01.950 align:start position:0% but that's not a little bit hard to read 00:23:01.950 --> 00:23:03.200 align:start position:0% but that's not a little bit hard to read the<00:23:02.010> thing<00:23:02.309> that<00:23:02.460> the<00:23:02.520> submission<00:23:02.789> will<00:23:03.090> look 00:23:03.200 --> 00:23:03.210 align:start position:0% the thing that the submission will look 00:23:03.210 --> 00:23:04.820 align:start position:0% the thing that the submission will look at<00:23:03.390> other<00:23:03.780> the<00:23:03.960> contest<00:23:04.289> will<00:23:04.409> look<00:23:04.530> at<00:23:04.679> this 00:23:04.820 --> 00:23:04.830 align:start position:0% at other the contest will look at this 00:23:04.830 --> 00:23:07.330 align:start position:0% at other the contest will look at this gas<00:23:05.070> analysis<00:23:05.610> if<00:23:05.760> you<00:23:05.850> click<00:23:06.030> that<00:23:06.210> link 00:23:07.330 --> 00:23:07.340 align:start position:0% gas analysis if you click that link 00:23:07.340 --> 00:23:11.690 align:start position:0% gas analysis if you click that link you'll<00:23:08.340> see<00:23:08.580> that<00:23:08.789> we<00:23:08.970> have 00:23:11.690 --> 00:23:11.700 align:start position:0% 00:23:11.700 --> 00:23:14.940 align:start position:0% can<00:23:12.700> you<00:23:12.759> guys<00:23:12.909> do<00:23:13.029> this<00:23:13.059> so<00:23:14.049> basically<00:23:14.349> what 00:23:14.940 --> 00:23:14.950 align:start position:0% can you guys do this so basically what 00:23:14.950 --> 00:23:16.169 align:start position:0% can you guys do this so basically what this<00:23:15.039> is<00:23:15.099> what<00:23:15.369> this<00:23:15.460> is<00:23:15.519> showing<00:23:15.609> is<00:23:15.999> that 00:23:16.169 --> 00:23:16.179 align:start position:0% this is what this is showing is that 00:23:16.179 --> 00:23:18.419 align:start position:0% this is what this is showing is that this<00:23:16.330> balance<00:23:16.570> of<00:23:16.929> that<00:23:17.889> this<00:23:18.039> balance<00:23:18.309> of 00:23:18.419 --> 00:23:18.429 align:start position:0% this balance of that this balance of 00:23:18.429 --> 00:23:19.859 align:start position:0% this balance of that this balance of munch<00:23:18.580> is<00:23:18.700> actually<00:23:18.940> consumed<00:23:19.330> rather<00:23:19.629> than 00:23:19.859 --> 00:23:19.869 align:start position:0% munch is actually consumed rather than 00:23:19.869 --> 00:23:22.919 align:start position:0% munch is actually consumed rather than 30<00:23:20.129> gasps<00:23:21.129> and<00:23:21.429> in<00:23:21.489> every<00:23:21.729> in<00:23:22.299> every<00:23:22.419> case<00:23:22.719> this 00:23:22.919 --> 00:23:22.929 align:start position:0% 30 gasps and in every in every case this 00:23:22.929 --> 00:23:25.049 align:start position:0% 30 gasps and in every in every case this could<00:23:23.080> actually<00:23:23.229> a<00:23:23.619> very<00:23:23.799> simple<00:23:24.099> example<00:23:24.190> but 00:23:25.049 --> 00:23:25.059 align:start position:0% could actually a very simple example but 00:23:25.059 --> 00:23:26.249 align:start position:0% could actually a very simple example but now<00:23:25.149> if<00:23:25.269> we<00:23:25.299> move<00:23:25.509> on<00:23:25.659> to<00:23:25.749> something<00:23:25.929> a<00:23:26.049> little 00:23:26.249 --> 00:23:26.259 align:start position:0% now if we move on to something a little 00:23:26.259 --> 00:23:28.859 align:start position:0% now if we move on to something a little bit<00:23:26.349> more<00:23:26.429> complicated<00:23:27.429> like<00:23:27.940> its<00:23:28.509> transfer 00:23:28.859 --> 00:23:28.869 align:start position:0% bit more complicated like its transfer 00:23:28.869 --> 00:23:30.389 align:start position:0% bit more complicated like its transfer function<00:23:28.899> we<00:23:29.469> look<00:23:29.590> at<00:23:29.710> the<00:23:29.769> cast<00:23:29.950> analysis 00:23:30.389 --> 00:23:30.399 align:start position:0% function we look at the cast analysis 00:23:30.399 --> 00:23:33.149 align:start position:0% function we look at the cast analysis for<00:23:30.549> that<00:23:30.729> it's<00:23:31.629> a<00:23:31.719> little<00:23:31.929> bit<00:23:32.019> more<00:23:32.259> so<00:23:32.979> the 00:23:33.149 --> 00:23:33.159 align:start position:0% for that it's a little bit more so the 00:23:33.159 --> 00:23:34.379 align:start position:0% for that it's a little bit more so the more<00:23:33.279> complicated<00:23:33.549> secure<00:23:33.999> you<00:23:34.090> see<00:23:34.269> the 00:23:34.379 --> 00:23:34.389 align:start position:0% more complicated secure you see the 00:23:34.389 --> 00:23:35.580 align:start position:0% more complicated secure you see the first<00:23:34.629> thing<00:23:34.809> is<00:23:34.929> the<00:23:35.019> tree<00:23:35.289> so<00:23:35.469> that's 00:23:35.580 --> 00:23:35.590 align:start position:0% first thing is the tree so that's 00:23:35.590 --> 00:23:36.950 align:start position:0% first thing is the tree so that's actually<00:23:35.739> the<00:23:35.919> gas<00:23:36.129> but<00:23:36.340> all<00:23:36.429> the<00:23:36.519> cases 00:23:36.950 --> 00:23:36.960 align:start position:0% actually the gas but all the cases 00:23:36.960 --> 00:23:40.409 align:start position:0% actually the gas but all the cases conditional<00:23:37.960> on<00:23:38.139> the<00:23:38.969> starting<00:23:39.969> balance<00:23:40.090> the 00:23:40.409 --> 00:23:40.419 align:start position:0% conditional on the starting balance the 00:23:40.419 --> 00:23:42.629 align:start position:0% conditional on the starting balance the ending<00:23:40.659> balance<00:23:40.989> and<00:23:41.830> then<00:23:41.919> we<00:23:42.099> also<00:23:42.219> compute 00:23:42.629 --> 00:23:42.639 align:start position:0% ending balance and then we also compute 00:23:42.639 --> 00:23:44.669 align:start position:0% ending balance and then we also compute the<00:23:42.729> minimum<00:23:42.849> and<00:23:43.149> the<00:23:43.239> maximum<00:23:43.269> gas<00:23:43.749> use<00:23:44.019> the 00:23:44.669 --> 00:23:44.679 align:start position:0% the minimum and the maximum gas use the 00:23:44.679 --> 00:23:47.369 align:start position:0% the minimum and the maximum gas use the year<00:23:44.859> you're<00:23:45.159> here<00:23:45.369> contest<00:23:46.239> entering<00:23:47.019> is 00:23:47.369 --> 00:23:47.379 align:start position:0% year you're here contest entering is 00:23:47.379 --> 00:23:52.169 align:start position:0% year you're here contest entering is going<00:23:47.710> to<00:23:47.859> be<00:23:48.719> the<00:23:49.719> maximum<00:23:49.960> capacity<00:23:50.969> and<00:23:51.969> we 00:23:52.169 --> 00:23:52.179 align:start position:0% going to be the maximum capacity and we 00:23:52.179 --> 00:23:53.459 align:start position:0% going to be the maximum capacity and we will<00:23:52.359> completely<00:23:52.690> ignore<00:23:52.839> what<00:23:53.109> happens<00:23:53.379> in 00:23:53.459 --> 00:23:53.469 align:start position:0% will completely ignore what happens in 00:23:53.469 --> 00:23:55.829 align:start position:0% will completely ignore what happens in cases<00:23:53.799> where<00:23:54.009> you<00:23:54.519> are<00:23:54.879> where<00:23:55.599> were<00:23:55.690> your 00:23:55.829 --> 00:23:55.839 align:start position:0% cases where you are where were your 00:23:55.839 --> 00:23:57.299 align:start position:0% cases where you are where were your executions<00:23:56.440> supposed<00:23:56.619> to<00:23:56.710> revert<00:23:56.979> so<00:23:57.190> if 00:23:57.299 --> 00:23:57.309 align:start position:0% executions supposed to revert so if 00:23:57.309 --> 00:23:58.829 align:start position:0% executions supposed to revert so if someone<00:23:57.549> is<00:23:57.609> over<00:23:57.849> over<00:23:58.029> under<00:23:58.210> flowing<00:23:58.719> or 00:23:58.829 --> 00:23:58.839 align:start position:0% someone is over over under flowing or 00:23:58.839 --> 00:23:59.820 align:start position:0% someone is over over under flowing or they're<00:23:58.960> not<00:23:59.049> approved<00:23:59.379> or<00:23:59.529> something<00:23:59.739> like 00:23:59.820 --> 00:23:59.830 align:start position:0% they're not approved or something like 00:23:59.830 --> 00:24:02.009 align:start position:0% they're not approved or something like that<00:24:00.089> the<00:24:01.089> old<00:24:01.239> character<00:24:01.479> man<00:24:01.599> Cassidy's 00:24:02.009 --> 00:24:02.019 align:start position:0% that the old character man Cassidy's 00:24:02.019 --> 00:24:03.599 align:start position:0% that the old character man Cassidy's because<00:24:02.320> given<00:24:02.679> the<00:24:02.710> internet<00:24:03.099> and<00:24:03.219> error<00:24:03.369> and 00:24:03.599 --> 00:24:03.609 align:start position:0% because given the internet and error and 00:24:03.609 --> 00:24:05.099 align:start position:0% because given the internet and error and we're<00:24:03.879> not<00:24:03.940> going<00:24:04.119> to<00:24:04.210> try<00:24:04.419> to<00:24:04.450> save<00:24:04.659> any<00:24:04.899> gas 00:24:05.099 --> 00:24:05.109 align:start position:0% we're not going to try to save any gas 00:24:05.109 --> 00:24:06.329 align:start position:0% we're not going to try to save any gas so<00:24:05.259> you<00:24:05.320> can<00:24:05.529> do<00:24:05.619> whatever<00:24:05.799> you<00:24:05.979> want<00:24:06.129> in<00:24:06.219> those 00:24:06.329 --> 00:24:06.339 align:start position:0% so you can do whatever you want in those 00:24:06.339 --> 00:24:10.499 align:start position:0% so you can do whatever you want in those cases<00:24:06.549> provided<00:24:07.059> River<00:24:08.940> so<00:24:09.940> I<00:24:09.969> think<00:24:10.239> this 00:24:10.499 --> 00:24:10.509 align:start position:0% cases provided River so I think this 00:24:10.509 --> 00:24:12.329 align:start position:0% cases provided River so I think this probably<00:24:11.049> gives<00:24:11.200> you<00:24:11.379> everything<00:24:11.649> you<00:24:12.070> need 00:24:12.329 --> 00:24:12.339 align:start position:0% probably gives you everything you need 00:24:12.339 --> 00:24:16.440 align:start position:0% probably gives you everything you need to<00:24:12.929> to<00:24:13.929> get<00:24:14.049> started<00:24:14.529> so<00:24:15.279> we're<00:24:15.849> encouraging 00:24:16.440 --> 00:24:16.450 align:start position:0% to to get started so we're encouraging 00:24:16.450 --> 00:24:18.959 align:start position:0% to to get started so we're encouraging as<00:24:16.629> far<00:24:16.809> as<00:24:16.929> soon<00:24:17.349> as<00:24:17.440> possible<00:24:17.830> because<00:24:17.969> it 00:24:18.959 --> 00:24:18.969 align:start position:0% as far as soon as possible because it 00:24:18.969 --> 00:24:21.719 align:start position:0% as far as soon as possible because it will<00:24:19.089> take<00:24:19.299> you<00:24:19.539> know<00:24:20.099> people<00:24:21.099> think<00:24:21.219> about<00:24:21.399> 15 00:24:21.719 --> 00:24:21.729 align:start position:0% will take you know people think about 15 00:24:21.729 --> 00:24:23.909 align:start position:0% will take you know people think about 15 to<00:24:22.509> 20<00:24:22.749> minutes<00:24:23.019> for<00:24:23.080> these<00:24:23.349> of<00:24:23.619> these 00:24:23.909 --> 00:24:23.919 align:start position:0% to 20 minutes for these of these 00:24:23.919 --> 00:24:25.589 align:start position:0% to 20 minutes for these of these executions<00:24:24.159> to<00:24:24.489> run<00:24:24.669> the<00:24:24.820> CI<00:24:24.969> and<00:24:25.239> we<00:24:25.299> can<00:24:25.419> run 00:24:25.589 --> 00:24:25.599 align:start position:0% executions to run the CI and we can run 00:24:25.599 --> 00:24:28.680 align:start position:0% executions to run the CI and we can run a<00:24:26.169> human<00:24:26.710> parallel<00:24:27.129> of<00:24:27.279> course<00:24:27.489> but<00:24:27.729> to 00:24:28.680 --> 00:24:28.690 align:start position:0% a human parallel of course but to 00:24:28.690 --> 00:24:30.379 align:start position:0% a human parallel of course but to increase<00:24:28.989> the<00:24:29.080> chances<00:24:29.409> of<00:24:29.469> your<00:24:29.589> submission 00:24:30.379 --> 00:24:30.389 align:start position:0% increase the chances of your submission 00:24:30.389 --> 00:24:34.469 align:start position:0% increase the chances of your submission I<00:24:31.389> know<00:24:32.320> the<00:24:32.559> workshop<00:24:32.950> please<00:24:33.249> please<00:24:34.239> submit 00:24:34.469 --> 00:24:34.479 align:start position:0% I know the workshop please please submit 00:24:34.479 --> 00:24:36.180 align:start position:0% I know the workshop please please submit it<00:24:34.570> as<00:24:34.749> soon<00:24:34.869> as<00:24:34.929> possible<00:24:35.019> and<00:24:35.499> don't<00:24:35.559> worry 00:24:36.180 --> 00:24:36.190 align:start position:0% it as soon as possible and don't worry 00:24:36.190 --> 00:24:38.509 align:start position:0% it as soon as possible and don't worry about<00:24:36.279> getting<00:24:36.929> absolutely<00:24:37.929> the<00:24:38.109> best 00:24:38.509 --> 00:24:38.519 align:start position:0% about getting absolutely the best 00:24:38.519 --> 00:24:41.279 align:start position:0% about getting absolutely the best implementation<00:24:39.519> view<00:24:40.059> you<00:24:40.599> can<00:24:40.839> because<00:24:41.200> I 00:24:41.279 --> 00:24:41.289 align:start position:0% implementation view you can because I 00:24:41.289 --> 00:24:43.079 align:start position:0% implementation view you can because I think<00:24:41.320> simply<00:24:42.279> getting<00:24:42.460> something<00:24:42.759> that's 00:24:43.079 --> 00:24:43.089 align:start position:0% think simply getting something that's 00:24:43.089 --> 00:24:44.940 align:start position:0% think simply getting something that's make<00:24:43.989> some<00:24:44.169> improvements<00:24:44.619> over<00:24:44.679> its<00:24:44.769> validity 00:24:44.940 --> 00:24:44.950 align:start position:0% make some improvements over its validity 00:24:44.950 --> 00:24:48.299 align:start position:0% make some improvements over its validity learn<00:24:45.309> any<00:24:45.460> give<00:24:45.609> you<00:24:45.639> a<00:24:45.759> good<00:24:45.940> shot<00:24:46.200> and<00:24:47.309> the 00:24:48.299 --> 00:24:48.309 align:start position:0% learn any give you a good shot and the 00:24:48.309 --> 00:24:49.900 align:start position:0% learn any give you a good shot and the goal<00:24:48.339> is<00:24:48.609> to<00:24:48.639> have<00:24:48.879> fun 00:24:49.900 --> 00:24:49.910 align:start position:0% goal is to have fun 00:24:49.910 --> 00:24:51.580 align:start position:0% goal is to have fun learn<00:24:50.480> something<00:24:50.870> and<00:24:51.020> of<00:24:51.140> course<00:24:51.350> you<00:24:51.500> know 00:24:51.580 --> 00:24:51.590 align:start position:0% learn something and of course you know 00:24:51.590 --> 00:24:53.380 align:start position:0% learn something and of course you know we<00:24:51.710> can<00:24:52.190> continue<00:24:52.550> playing<00:24:52.760> for<00:24:53.090> the<00:24:53.150> next 00:24:53.380 --> 00:24:53.390 align:start position:0% we can continue playing for the next 00:24:53.390 --> 00:24:56.140 align:start position:0% we can continue playing for the next couple<00:24:54.020> of<00:24:54.050> weeks<00:24:54.140> or<00:24:54.560> months<00:24:55.250> if<00:24:55.730> you<00:24:55.850> want<00:24:56.060> to 00:24:56.140 --> 00:24:56.150 align:start position:0% couple of weeks or months if you want to 00:24:56.150 --> 00:24:58.510 align:start position:0% couple of weeks or months if you want to continue<00:24:56.420> to<00:24:56.720> you<00:24:56.810> enough<00:24:57.080> to<00:24:57.950> get<00:24:58.070> it<00:24:58.160> down<00:24:58.280> so 00:24:58.510 --> 00:24:58.520 align:start position:0% continue to you enough to get it down so 00:24:58.520 --> 00:25:00.430 align:start position:0% continue to you enough to get it down so just<00:24:58.670> just<00:24:59.060> things<00:24:59.300> workflow<00:24:59.960> completely 00:25:00.430 --> 00:25:00.440 align:start position:0% just just things workflow completely 00:25:00.440 --> 00:25:02.170 align:start position:0% just just things workflow completely clear<00:25:00.650> what<00:25:00.680> you<00:25:00.950> need<00:25:01.100> to<00:25:01.220> do<00:25:01.430> I<00:25:01.610> mean<00:25:02.090> is 00:25:02.170 --> 00:25:02.180 align:start position:0% clear what you need to do I mean is 00:25:02.180 --> 00:25:04.050 align:start position:0% clear what you need to do I mean is quickly<00:25:02.420> make<00:25:02.750> a<00:25:02.780> submission<00:25:03.170> to<00:25:03.320> this<00:25:03.530> thing 00:25:04.050 --> 00:25:04.060 align:start position:0% quickly make a submission to this thing 00:25:04.060 --> 00:25:06.010 align:start position:0% quickly make a submission to this thing to<00:25:05.060> show<00:25:05.540> you 00:25:06.010 --> 00:25:06.020 align:start position:0% to show you 00:25:06.020 --> 00:25:11.110 align:start position:0% to show you so<00:25:06.620> Karen<00:25:07.160> in<00:25:07.340> the<00:25:08.290> twenty<00:25:09.290> golf<00:25:09.500> repo<00:25:10.430> and 00:25:11.110 --> 00:25:11.120 align:start position:0% so Karen in the twenty golf repo and 00:25:11.120 --> 00:25:13.120 align:start position:0% so Karen in the twenty golf repo and let's<00:25:11.330> say<00:25:11.450> I<00:25:11.510> want<00:25:11.720> to<00:25:11.780> make<00:25:11.900> a<00:25:12.040> make<00:25:13.040> an 00:25:13.120 --> 00:25:13.130 align:start position:0% let's say I want to make a make an 00:25:13.130 --> 00:25:16.150 align:start position:0% let's say I want to make a make an optimization<00:25:13.790> to<00:25:14.060> the<00:25:14.150> banker<00:25:14.890> and<00:25:15.890> in 00:25:16.150 --> 00:25:16.160 align:start position:0% optimization to the banker and in 00:25:16.160 --> 00:25:19.390 align:start position:0% optimization to the banker and in particular<00:25:16.580> I'm<00:25:16.670> going<00:25:16.730> to<00:25:16.880> use<00:25:17.060> a<00:25:17.090> tool<00:25:18.400> then 00:25:19.390 --> 00:25:19.400 align:start position:0% particular I'm going to use a tool then 00:25:19.400 --> 00:25:24.070 align:start position:0% particular I'm going to use a tool then use<00:25:19.580> a<00:25:19.610> tool<00:25:19.910> it's<00:25:20.900> very<00:25:20.960> nice<00:25:22.420> called<00:25:23.420> STD 00:25:24.070 --> 00:25:24.080 align:start position:0% use a tool it's very nice called STD 00:25:24.080 --> 00:25:28.950 align:start position:0% use a tool it's very nice called STD which<00:25:24.770> which<00:25:25.520> stands<00:25:25.850> for<00:25:26.950> salinity<00:25:27.950> and<00:25:28.460> has 00:25:28.950 --> 00:25:28.960 align:start position:0% which which stands for salinity and has 00:25:28.960 --> 00:25:32.350 align:start position:0% which which stands for salinity and has diplom<00:25:29.990> and<00:25:30.730> what's<00:25:31.730> really<00:25:31.940> nice<00:25:32.060> about<00:25:32.120> this 00:25:32.350 --> 00:25:32.360 align:start position:0% diplom and what's really nice about this 00:25:32.360 --> 00:25:34.690 align:start position:0% diplom and what's really nice about this and<00:25:32.600> actually<00:25:32.690> comes<00:25:33.080> with<00:25:33.200> the<00:25:33.980> unit<00:25:34.250> systems 00:25:34.690 --> 00:25:34.700 align:start position:0% and actually comes with the unit systems 00:25:34.700 --> 00:25:37.630 align:start position:0% and actually comes with the unit systems and<00:25:35.290> it's<00:25:36.290> literally<00:25:36.560> actually<00:25:36.860> uses<00:25:37.160> this<00:25:37.310> to 00:25:37.630 --> 00:25:37.640 align:start position:0% and it's literally actually uses this to 00:25:37.640 --> 00:25:39.250 align:start position:0% and it's literally actually uses this to be<00:25:37.820> implemented<00:25:37.970> compiler<00:25:38.630> optimizations 00:25:39.250 --> 00:25:39.260 align:start position:0% be implemented compiler optimizations 00:25:39.260 --> 00:25:41.710 align:start position:0% be implemented compiler optimizations detectives<00:25:40.250> would<00:25:40.370> compile<00:25:40.670> into<00:25:41.150> this<00:25:41.450> just 00:25:41.710 --> 00:25:41.720 align:start position:0% detectives would compile into this just 00:25:41.720 --> 00:25:44.520 align:start position:0% detectives would compile into this just state-of-the-art<00:25:42.500> way<00:25:42.740> to<00:25:43.180> to<00:25:44.180> work<00:25:44.330> with 00:25:44.520 --> 00:25:44.530 align:start position:0% state-of-the-art way to to work with 00:25:44.530 --> 00:25:47.980 align:start position:0% state-of-the-art way to to work with about<00:25:45.530> to<00:25:45.650> my<00:25:45.770> plankton<00:25:46.190> and<00:25:46.700> my<00:25:47.480> trip<00:25:47.780> the 00:25:47.980 --> 00:25:47.990 align:start position:0% about to my plankton and my trip the 00:25:47.990 --> 00:25:53.410 align:start position:0% about to my plankton and my trip the syntax<00:25:48.200> below<00:25:48.620> that<00:25:48.800> arcade<00:25:50.170> so<00:25:52.060> push<00:25:53.060> if<00:25:53.360> you 00:25:53.410 --> 00:25:53.420 align:start position:0% syntax below that arcade so push if you 00:25:53.420 --> 00:25:55.390 align:start position:0% syntax below that arcade so push if you have<00:25:53.660> purchased<00:25:53.870> error<00:25:54.110> in<00:25:54.320> the<00:25:54.410> EVM<00:25:54.770> what 00:25:55.390 --> 00:25:55.400 align:start position:0% have purchased error in the EVM what 00:25:55.400 --> 00:25:57.280 align:start position:0% have purchased error in the EVM what that<00:25:55.550> does<00:25:55.700> is<00:25:55.940> zero<00:25:56.420> on<00:25:56.630> the<00:25:56.720> stock<00:25:56.990> that<00:25:57.170> that 00:25:57.280 --> 00:25:57.290 align:start position:0% that does is zero on the stock that that 00:25:57.290 --> 00:25:59.860 align:start position:0% that does is zero on the stock that that cost<00:25:57.500> you<00:25:57.620> three<00:25:57.860> guys<00:25:58.450> but<00:25:59.450> in<00:25:59.780> this 00:25:59.860 --> 00:25:59.870 align:start position:0% cost you three guys but in this 00:25:59.870 --> 00:26:01.780 align:start position:0% cost you three guys but in this particular<00:26:00.050> case<00:26:00.500> mr.<00:26:01.040> Berg<00:26:01.280> we're<00:26:01.580> in<00:26:01.670> this 00:26:01.780 --> 00:26:01.790 align:start position:0% particular case mr. Berg we're in this 00:26:01.790 --> 00:26:04.960 align:start position:0% particular case mr. Berg we're in this non<00:26:02.480> payable<00:26:03.160> regime<00:26:04.160> where<00:26:04.490> he<00:26:04.670> not<00:26:04.820> supposed 00:26:04.960 --> 00:26:04.970 align:start position:0% non payable regime where he not supposed 00:26:04.970 --> 00:26:06.430 align:start position:0% non payable regime where he not supposed to<00:26:05.210> set<00:26:05.420> any<00:26:05.570> value<00:26:05.600> in<00:26:05.960> otherwise<00:26:06.200> it's<00:26:06.320> gonna 00:26:06.430 --> 00:26:06.440 align:start position:0% to set any value in otherwise it's gonna 00:26:06.440 --> 00:26:07.930 align:start position:0% to set any value in otherwise it's gonna refer<00:26:06.710> to<00:26:06.770> comparison<00:26:07.250> mention<00:26:07.520> of<00:26:07.640> the<00:26:07.730> most 00:26:07.930 --> 00:26:07.940 align:start position:0% refer to comparison mention of the most 00:26:07.940 --> 00:26:10.840 align:start position:0% refer to comparison mention of the most describe<00:26:08.300> the<00:26:09.020> the<00:26:09.740> call<00:26:10.130> value<00:26:10.490> is<00:26:10.580> gonna<00:26:10.760> be 00:26:10.840 --> 00:26:10.850 align:start position:0% describe the the call value is gonna be 00:26:10.850 --> 00:26:12.370 align:start position:0% describe the the call value is gonna be zero<00:26:11.090> but<00:26:11.300> they<00:26:11.390> call<00:26:11.570> value<00:26:11.840> off<00:26:11.960> coded<00:26:12.230> only 00:26:12.370 --> 00:26:12.380 align:start position:0% zero but they call value off coded only 00:26:12.380 --> 00:26:14.020 align:start position:0% zero but they call value off coded only cost<00:26:12.590> two<00:26:12.830> yes<00:26:13.010> we<00:26:13.310> can<00:26:13.400> actually<00:26:13.520> every<00:26:14.000> time 00:26:14.020 --> 00:26:14.030 align:start position:0% cost two yes we can actually every time 00:26:14.030 --> 00:26:15.520 align:start position:0% cost two yes we can actually every time we<00:26:14.360> need<00:26:14.480> Chris<00:26:14.720> zero<00:26:14.960> which<00:26:15.140> would<00:26:15.260> be<00:26:15.380> quite 00:26:15.520 --> 00:26:15.530 align:start position:0% we need Chris zero which would be quite 00:26:15.530 --> 00:26:17.080 align:start position:0% we need Chris zero which would be quite a<00:26:15.560> few<00:26:15.710> times<00:26:15.860> because<00:26:16.220> that's<00:26:16.820> quite<00:26:17.000> a 00:26:17.080 --> 00:26:17.090 align:start position:0% a few times because that's quite a 00:26:17.090 --> 00:26:18.740 align:start position:0% a few times because that's quite a useful<00:26:17.240> number 00:26:18.740 --> 00:26:18.750 align:start position:0% useful number 00:26:18.750 --> 00:26:21.080 align:start position:0% useful number we<00:26:19.080> can<00:26:19.230> actually<00:26:19.590> replace<00:26:20.250> every<00:26:20.730> parent 00:26:21.080 --> 00:26:21.090 align:start position:0% we can actually replace every parent 00:26:21.090 --> 00:26:23.419 align:start position:0% we can actually replace every parent smoker<00:26:21.710> serial<00:26:22.710> code<00:26:22.919> which<00:26:23.100> I'm<00:26:23.250> going<00:26:23.370> to 00:26:23.419 --> 00:26:23.429 align:start position:0% smoker serial code which I'm going to 00:26:23.429 --> 00:26:26.060 align:start position:0% smoker serial code which I'm going to look<00:26:23.640> up<00:26:23.789> here<00:26:24.090> in<00:26:24.240> life<00:26:24.419> though<00:26:25.200> she<00:26:25.590> she<00:26:25.799> is 00:26:26.060 --> 00:26:26.070 align:start position:0% look up here in life though she she is 00:26:26.070 --> 00:26:30.760 align:start position:0% look up here in life though she she is is<00:26:26.520> actually<00:26:26.760> 34<00:26:27.360> in<00:26:28.169> hex<00:26:28.410> so<00:26:28.710> if<00:26:29.610> we<00:26:29.760> do<00:26:29.940> this 00:26:30.760 --> 00:26:30.770 align:start position:0% is actually 34 in hex so if we do this 00:26:30.770 --> 00:26:35.120 align:start position:0% is actually 34 in hex so if we do this to<00:26:31.770> the<00:26:32.210> incident<00:26:33.210> inspector<00:26:33.890> that<00:26:34.890> should 00:26:35.120 --> 00:26:35.130 align:start position:0% to the incident inspector that should 00:26:35.130 --> 00:26:37.610 align:start position:0% to the incident inspector that should actually<00:26:35.280> implement<00:26:36.179> this<00:26:36.270> this<00:26:36.630> one<00:26:37.169> pretty 00:26:37.610 --> 00:26:37.620 align:start position:0% actually implement this this one pretty 00:26:37.620 --> 00:26:40.400 align:start position:0% actually implement this this one pretty sophisticated<00:26:37.740> compiler<00:26:38.400> optimization<00:26:39.410> so 00:26:40.400 --> 00:26:40.410 align:start position:0% sophisticated compiler optimization so 00:26:40.410 --> 00:26:43.820 align:start position:0% sophisticated compiler optimization so now<00:26:40.530> you'll<00:26:41.070> see<00:26:41.280> that<00:26:42.140> we've<00:26:43.140> actually<00:26:43.260> got 00:26:43.820 --> 00:26:43.830 align:start position:0% now you'll see that we've actually got 00:26:43.830 --> 00:26:46.150 align:start position:0% now you'll see that we've actually got to<00:26:43.919> change<00:26:44.130> my<00:26:44.400> credit<00:26:44.760> in<00:26:45.030> some<00:26:45.299> in<00:26:45.510> some<00:26:45.539> way 00:26:46.150 --> 00:26:46.160 align:start position:0% to change my credit in some in some way 00:26:46.160 --> 00:26:50.210 align:start position:0% to change my credit in some in some way and<00:26:47.160> I<00:26:47.549> can<00:26:47.850> actually<00:26:48.830> unlikely<00:26:49.830> to<00:26:50.039> commit 00:26:50.210 --> 00:26:50.220 align:start position:0% and I can actually unlikely to commit 00:26:50.220 --> 00:27:02.630 align:start position:0% and I can actually unlikely to commit this<00:26:50.520> and<00:26:53.419> and<00:26:54.419> make<00:26:54.780> pluralism 00:27:02.630 --> 00:27:02.640 align:start position:0% 00:27:02.640 --> 00:27:11.770 align:start position:0% [Music] 00:27:11.770 --> 00:27:11.780 align:start position:0% 00:27:11.780 --> 00:27:14.080 align:start position:0% so<00:27:12.440> now<00:27:12.740> you<00:27:12.890> just<00:27:12.950> go<00:27:13.190> up<00:27:13.340> here<00:27:13.370> and<00:27:13.850> now<00:27:13.940> of 00:27:14.080 --> 00:27:14.090 align:start position:0% so now you just go up here and now of 00:27:14.090 --> 00:27:16.480 align:start position:0% so now you just go up here and now of course<00:27:14.140> you'll<00:27:15.140> make<00:27:15.500> arrests<00:27:15.980> when<00:27:16.310> you're 00:27:16.480 --> 00:27:16.490 align:start position:0% course you'll make arrests when you're 00:27:16.490 --> 00:27:28.240 align:start position:0% course you'll make arrests when you're in<00:27:16.640> for<00:27:17.180> Kirk<00:27:17.420> or<00:27:17.630> whatever<00:27:26.260> so<00:27:27.260> one<00:27:27.680> side 00:27:28.240 --> 00:27:28.250 align:start position:0% in for Kirk or whatever so one side 00:27:28.250 --> 00:27:31.680 align:start position:0% in for Kirk or whatever so one side once<00:27:28.490> I<00:27:28.640> click<00:27:28.700> create<00:27:29.450> fuller<00:27:29.810> bunch<00:27:30.170> here 00:27:31.680 --> 00:27:31.690 align:start position:0% once I click create fuller bunch here 00:27:31.690 --> 00:27:34.780 align:start position:0% once I click create fuller bunch here it's<00:27:32.690> going<00:27:32.960> to<00:27:33.110> hopefully<00:27:34.100> be<00:27:34.280> picked<00:27:34.520> up<00:27:34.610> by 00:27:34.780 --> 00:27:34.790 align:start position:0% it's going to hopefully be picked up by 00:27:34.790 --> 00:27:36.520 align:start position:0% it's going to hopefully be picked up by the<00:27:34.850> CI<00:27:35.090> straightaway<00:27:35.810> and<00:27:36.080> then<00:27:36.260> we<00:27:36.380> can 00:27:36.520 --> 00:27:36.530 align:start position:0% the CI straightaway and then we can 00:27:36.530 --> 00:27:38.410 align:start position:0% the CI straightaway and then we can start<00:27:36.740> verifying<00:27:37.220> see<00:27:37.520> how<00:27:37.640> much<00:27:37.760> gas<00:27:37.970> we<00:27:38.180> save 00:27:38.410 --> 00:27:38.420 align:start position:0% start verifying see how much gas we save 00:27:38.420 --> 00:27:43.680 align:start position:0% start verifying see how much gas we save from<00:27:38.750> implementing<00:27:39.740> this<00:27:40.720> salinity<00:27:41.720> enhanced 00:27:43.680 --> 00:27:43.690 align:start position:0% from implementing this salinity enhanced 00:27:43.690 --> 00:27:49.900 align:start position:0% from implementing this salinity enhanced diplomat<00:27:44.690> optimization<00:27:48.460> great<00:27:49.460> it's<00:27:49.610> already 00:27:49.900 --> 00:27:49.910 align:start position:0% diplomat optimization great it's already 00:27:49.910 --> 00:27:52.810 align:start position:0% diplomat optimization great it's already running<00:27:50.440> and<00:27:51.440> if<00:27:51.770> I<00:27:51.890> go<00:27:52.100> if<00:27:52.370> I<00:27:52.490> go<00:27:52.610> to<00:27:52.700> this 00:27:52.810 --> 00:27:52.820 align:start position:0% running and if I go if I go to this 00:27:52.820 --> 00:27:55.330 align:start position:0% running and if I go if I go to this website<00:27:53.060> which<00:27:53.390> again<00:27:53.510> is<00:27:53.810> adapt<00:27:54.110> up<00:27:54.320> CI<00:27:54.530> /<00:27:54.980> GRC 00:27:55.330 --> 00:27:55.340 align:start position:0% website which again is adapt up CI / GRC 00:27:55.340 --> 00:27:59.290 align:start position:0% website which again is adapt up CI / GRC 20<00:27:55.790> -<00:27:56.600> Gulf<00:27:56.870> which<00:27:57.680> is<00:27:57.890> a<00:27:58.070> nice<00:27:58.250> dashboard<00:27:58.850> for 00:27:59.290 --> 00:27:59.300 align:start position:0% 20 - Gulf which is a nice dashboard for 00:27:59.300 --> 00:28:01.990 align:start position:0% 20 - Gulf which is a nice dashboard for viewing<00:27:59.510> these<00:27:59.860> these<00:28:00.860> builds<00:28:01.310> you'll<00:28:01.790> see 00:28:01.990 --> 00:28:02.000 align:start position:0% viewing these these builds you'll see 00:28:02.000 --> 00:28:03.010 align:start position:0% viewing these these builds you'll see that<00:28:02.090> there's<00:28:02.330> a<00:28:02.390> new<00:28:02.600> one 00:28:03.010 --> 00:28:03.020 align:start position:0% that there's a new one 00:28:03.020 --> 00:28:04.840 align:start position:0% that there's a new one there's<00:28:04.010> a<00:28:04.100> new<00:28:04.190> one<00:28:04.280> at<00:28:04.400> the<00:28:04.460> top<00:28:04.610> you<00:28:04.760> see 00:28:04.840 --> 00:28:04.850 align:start position:0% there's a new one at the top you see 00:28:04.850 --> 00:28:07.210 align:start position:0% there's a new one at the top you see step<00:28:05.360> running<00:28:05.540> sixteen<00:28:06.140> so<00:28:06.890> none<00:28:07.070> of<00:28:07.100> them 00:28:07.210 --> 00:28:07.220 align:start position:0% step running sixteen so none of them 00:28:07.220 --> 00:28:08.620 align:start position:0% step running sixteen so none of them have<00:28:07.340> been<00:28:07.370> accepted<00:28:07.820> yet<00:28:07.850> and<00:28:08.270> take<00:28:08.360> a<00:28:08.420> little 00:28:08.620 --> 00:28:08.630 align:start position:0% have been accepted yet and take a little 00:28:08.630 --> 00:28:09.130 align:start position:0% have been accepted yet and take a little while 00:28:09.130 --> 00:28:09.140 align:start position:0% while 00:28:09.140 --> 00:28:13.870 align:start position:0% while form<00:28:09.650> the<00:28:09.770> verification<00:28:10.340> is<00:28:10.510> expensive<00:28:12.880> and 00:28:13.870 --> 00:28:13.880 align:start position:0% form the verification is expensive and 00:28:13.880 --> 00:28:15.460 align:start position:0% form the verification is expensive and then<00:28:14.090> you'll<00:28:14.210> see<00:28:14.720> these<00:28:14.870> you'll<00:28:15.170> see<00:28:15.350> these 00:28:15.460 --> 00:28:15.470 align:start position:0% then you'll see these you'll see these 00:28:15.470 --> 00:28:17.710 align:start position:0% then you'll see these you'll see these gas<00:28:15.770> analyses<00:28:16.220> coming<00:28:16.580> in<00:28:16.700> as<00:28:16.970> these<00:28:17.180> isomers 00:28:17.710 --> 00:28:17.720 align:start position:0% gas analyses coming in as these isomers 00:28:17.720 --> 00:28:19.660 align:start position:0% gas analyses coming in as these isomers happen<00:28:18.260> in<00:28:18.350> the<00:28:18.410> next<00:28:18.530> you<00:28:19.220> know<00:28:19.310> two<00:28:19.520> minutes 00:28:19.660 --> 00:28:19.670 align:start position:0% happen in the next you know two minutes 00:28:19.670 --> 00:28:21.100 align:start position:0% happen in the next you know two minutes probably<00:28:20.060> the<00:28:20.180> first<00:28:20.300> one<00:28:20.540> will<00:28:20.630> come<00:28:20.780> in<00:28:20.900> and 00:28:21.100 --> 00:28:21.110 align:start position:0% probably the first one will come in and 00:28:21.110 --> 00:28:22.270 align:start position:0% probably the first one will come in and also<00:28:21.230> coming<00:28:21.620> in<00:28:21.710> so<00:28:21.830> you<00:28:21.920> can<00:28:22.010> see<00:28:22.040> how<00:28:22.220> are 00:28:22.270 --> 00:28:22.280 align:start position:0% also coming in so you can see how are 00:28:22.280 --> 00:28:23.770 align:start position:0% also coming in so you can see how are you<00:28:22.370> doing<00:28:22.580> and<00:28:22.760> you<00:28:23.270> know<00:28:23.360> hopefully<00:28:23.570> it'll 00:28:23.770 --> 00:28:23.780 align:start position:0% you doing and you know hopefully it'll 00:28:23.780 --> 00:28:26.620 align:start position:0% you doing and you know hopefully it'll take<00:28:23.960> under<00:28:24.260> an<00:28:24.530> hour<00:28:25.460> around<00:28:25.520> 15<00:28:26.120> minutes<00:28:26.420> to 00:28:26.620 --> 00:28:26.630 align:start position:0% take under an hour around 15 minutes to 00:28:26.630 --> 00:28:28.660 align:start position:0% take under an hour around 15 minutes to complete<00:28:27.110> all<00:28:27.200> of<00:28:27.230> them<00:28:27.530> and<00:28:27.710> then<00:28:27.830> this<00:28:28.520> will 00:28:28.660 --> 00:28:28.670 align:start position:0% complete all of them and then this will 00:28:28.670 --> 00:28:31.060 align:start position:0% complete all of them and then this will be<00:28:28.730> the<00:28:28.820> first<00:28:29.170> be<00:28:30.170> the<00:28:30.260> first<00:28:30.500> admission<00:28:30.890> I 00:28:31.060 --> 00:28:31.070 align:start position:0% be the first be the first admission I 00:28:31.070 --> 00:28:33.160 align:start position:0% be the first be the first admission I challenge<00:28:31.430> you<00:28:31.550> to<00:28:31.850> see<00:28:32.060> if<00:28:32.150> you<00:28:32.270> can<00:28:32.480> you<00:28:33.050> can 00:28:33.160 --> 00:28:33.170 align:start position:0% challenge you to see if you can you can 00:28:33.170 --> 00:28:37.090 align:start position:0% challenge you to see if you can you can beat<00:28:33.350> this<00:28:33.500> one<00:28:34.030> using<00:28:35.530> using<00:28:36.530> any<00:28:36.680> tools<00:28:36.920> of 00:28:37.090 --> 00:28:37.100 align:start position:0% beat this one using using any tools of 00:28:37.100 --> 00:28:38.980 align:start position:0% beat this one using using any tools of your<00:28:37.160> choice<00:28:37.370> you<00:28:37.640> know<00:28:37.820> even<00:28:38.300> if<00:28:38.420> easy<00:28:38.810> way 00:28:38.980 --> 00:28:38.990 align:start position:0% your choice you know even if easy way 00:28:38.990 --> 00:28:40.600 align:start position:0% your choice you know even if easy way places<00:28:39.290> starting<00:28:39.800> to<00:28:39.950> apply<00:28:40.130> some<00:28:40.490> of<00:28:40.520> these 00:28:40.600 --> 00:28:40.610 align:start position:0% places starting to apply some of these 00:28:40.610 --> 00:28:42.760 align:start position:0% places starting to apply some of these manual<00:28:41.090> kinds<00:28:41.780> of<00:28:41.840> bike<00:28:41.990> code<00:28:42.170> optimizations 00:28:42.760 --> 00:28:42.770 align:start position:0% manual kinds of bike code optimizations 00:28:42.770 --> 00:28:44.200 align:start position:0% manual kinds of bike code optimizations you<00:28:42.890> can<00:28:43.010> also<00:28:43.160> try<00:28:43.430> running<00:28:43.760> so<00:28:43.910> I'll<00:28:44.000> see 00:28:44.200 --> 00:28:44.210 align:start position:0% you can also try running so I'll see 00:28:44.210 --> 00:28:47.370 align:start position:0% you can also try running so I'll see with<00:28:44.360> the<00:28:44.480> optimized<00:28:45.020> flag<00:28:45.350> because<00:28:46.340> the 00:28:47.370 --> 00:28:47.380 align:start position:0% with the optimized flag because the 00:28:47.380 --> 00:28:48.480 align:start position:0% with the optimized flag because the included 00:28:48.480 --> 00:28:48.490 align:start position:0% included 00:28:48.490 --> 00:28:50.310 align:start position:0% included mission<00:28:48.790> was<00:28:49.000> not<00:28:49.179> compiled<00:28:49.600> with<00:28:49.840> that<00:28:50.020> so 00:28:50.310 --> 00:28:50.320 align:start position:0% mission was not compiled with that so 00:28:50.320 --> 00:28:53.010 align:start position:0% mission was not compiled with that so that's<00:28:50.530> already<00:28:50.800> gave<00:28:51.100> me<00:28:51.160> some<00:28:52.030> pretty<00:28:52.179> good 00:28:53.010 --> 00:28:53.020 align:start position:0% that's already gave me some pretty good 00:28:53.020 --> 00:28:54.620 align:start position:0% that's already gave me some pretty good savings<00:28:53.350> and<00:28:53.620> then<00:28:53.710> of<00:28:53.800> course<00:28:53.830> an<00:28:54.130> Iranian 00:28:54.620 --> 00:28:54.630 align:start position:0% savings and then of course an Iranian 00:28:54.630 --> 00:28:57.480 align:start position:0% savings and then of course an Iranian Roy<00:28:55.630> yeah<00:28:56.020> or<00:28:56.260> whatever<00:28:56.890> whatever<00:28:57.160> you<00:28:57.340> like 00:28:57.480 --> 00:28:57.490 align:start position:0% Roy yeah or whatever whatever you like 00:28:57.490 --> 00:29:02.960 align:start position:0% Roy yeah or whatever whatever you like probably<00:28:58.330> give<00:28:58.720> you<00:29:01.320> good<00:29:02.320> time<00:29:02.470> to<00:29:02.590> start 00:29:02.960 --> 00:29:02.970 align:start position:0% probably give you good time to start 00:29:02.970 --> 00:29:06.600 align:start position:0% probably give you good time to start start<00:29:03.970> working<00:29:04.210> and<00:29:04.450> please<00:29:05.400> this<00:29:06.400> is<00:29:06.550> a 00:29:06.600 --> 00:29:06.610 align:start position:0% start working and please this is a 00:29:06.610 --> 00:29:07.799 align:start position:0% start working and please this is a workshop<00:29:06.790> the<00:29:07.120> idea<00:29:07.330> is<00:29:07.390> you're<00:29:07.540> supposed<00:29:07.750> to 00:29:07.799 --> 00:29:07.809 align:start position:0% workshop the idea is you're supposed to 00:29:07.809 --> 00:29:09.660 align:start position:0% workshop the idea is you're supposed to ask<00:29:07.960> questions<00:29:08.380> and<00:29:08.500> we<00:29:08.559> might<00:29:08.950> help<00:29:09.520> you 00:29:09.660 --> 00:29:09.670 align:start position:0% ask questions and we might help you 00:29:09.670 --> 00:29:13.650 align:start position:0% ask questions and we might help you understand<00:29:10.650> spec<00:29:11.650> language<00:29:12.100> or<00:29:12.429> or<00:29:13.300> this<00:29:13.420> is 00:29:13.650 --> 00:29:13.660 align:start position:0% understand spec language or or this is 00:29:13.660 --> 00:29:15.299 align:start position:0% understand spec language or or this is toiling<00:29:14.020> so<00:29:14.050> please<00:29:14.530> please<00:29:15.010> don't<00:29:15.190> hesitate 00:29:15.299 --> 00:29:15.309 align:start position:0% toiling so please please don't hesitate 00:29:15.309 --> 00:29:19.890 align:start position:0% toiling so please please don't hesitate to<00:29:15.610> uh<00:29:16.590> to<00:29:17.590> to<00:29:18.040> engage<00:29:18.190> with<00:29:19.090> us<00:29:19.420> and<00:29:19.660> your 00:29:19.890 --> 00:29:19.900 align:start position:0% to uh to to engage with us and your 00:29:19.900 --> 00:29:23.520 align:start position:0% to uh to to engage with us and your neighbors<00:29:21.840> are<00:29:22.840> there<00:29:22.990> any<00:29:23.080> immediate 00:29:23.520 --> 00:29:23.530 align:start position:0% neighbors are there any immediate 00:29:23.530 --> 00:29:35.600 align:start position:0% neighbors are there any immediate questions<00:29:24.750> yes 00:29:35.600 --> 00:29:35.610 align:start position:0% 00:29:35.610 --> 00:29:38.300 align:start position:0% yeah<00:29:36.420> the<00:29:36.930> dispatching<00:29:37.710> all<00:29:37.830> that<00:29:38.100> is 00:29:38.300 --> 00:29:38.310 align:start position:0% yeah the dispatching all that is 00:29:38.310 --> 00:29:39.290 align:start position:0% yeah the dispatching all that is included 00:29:39.290 --> 00:29:39.300 align:start position:0% included 00:29:39.300 --> 00:29:41.510 align:start position:0% included none<00:29:39.780> of<00:29:39.810> the<00:29:40.020> deployments<00:29:40.590> is<00:29:40.740> included<00:29:41.190> so 00:29:41.510 --> 00:29:41.520 align:start position:0% none of the deployments is included so 00:29:41.520 --> 00:29:45.650 align:start position:0% none of the deployments is included so you<00:29:41.550> know<00:29:42.650> the<00:29:43.650> length<00:29:44.580> of<00:29:44.820> my<00:29:45.000> code<00:29:45.240> doesn't 00:29:45.650 --> 00:29:45.660 align:start position:0% you know the length of my code doesn't 00:29:45.660 --> 00:29:48.410 align:start position:0% you know the length of my code doesn't matter<00:29:46.050> but<00:29:46.820> everything<00:29:47.820> that<00:29:47.850> happens<00:29:48.270> from 00:29:48.410 --> 00:29:48.420 align:start position:0% matter but everything that happens from 00:29:48.420 --> 00:29:53.990 align:start position:0% matter but everything that happens from PC<00:29:48.720> counter1<00:29:49.290> until<00:29:50.040> they<00:29:50.340> return<00:29:50.700> is 00:29:53.990 --> 00:29:54.000 align:start position:0% 00:29:54.000 --> 00:30:03.050 align:start position:0% [Music] 00:30:03.050 --> 00:30:03.060 align:start position:0% 00:30:03.060 --> 00:30:06.140 align:start position:0% [Music] 00:30:06.140 --> 00:30:06.150 align:start position:0% [Music] 00:30:06.150 --> 00:30:13.460 align:start position:0% [Music] yeah<00:30:07.180> so<00:30:08.520> exactly<00:30:09.520> like<00:30:10.030> storage<00:30:11.640> be<00:30:12.640> anything 00:30:13.460 --> 00:30:13.470 align:start position:0% yeah so exactly like storage be anything 00:30:13.470 --> 00:30:17.430 align:start position:0% yeah so exactly like storage be anything but<00:30:14.470> I<00:30:14.830> mean<00:30:15.280> the<00:30:15.809> storage<00:30:16.809> locations<00:30:17.260> that 00:30:17.430 --> 00:30:17.440 align:start position:0% but I mean the storage locations that 00:30:17.440 --> 00:30:21.060 align:start position:0% but I mean the storage locations that you'll<00:30:17.590> likely<00:30:17.950> be<00:30:18.240> working<00:30:19.240> with<00:30:19.570> are<00:30:20.200> the 00:30:21.060 --> 00:30:21.070 align:start position:0% you'll likely be working with are the 00:30:21.070 --> 00:30:23.060 align:start position:0% you'll likely be working with are the ones<00:30:21.100> that<00:30:21.460> come<00:30:21.640> from<00:30:21.670> the<00:30:21.940> mapping<00:30:22.720> of 00:30:23.060 --> 00:30:23.070 align:start position:0% ones that come from the mapping of 00:30:23.070 --> 00:30:28.230 align:start position:0% ones that come from the mapping of balances<00:30:24.070> and<00:30:24.280> allowances<00:30:24.790> so<00:30:26.160> yeah<00:30:27.240> started 00:30:28.230 --> 00:30:28.240 align:start position:0% balances and allowances so yeah started 00:30:28.240 --> 00:30:29.130 align:start position:0% balances and allowances so yeah started that<00:30:28.330> there's<00:30:28.480> one<00:30:28.630> really<00:30:28.780> important<00:30:29.080> thing 00:30:29.130 --> 00:30:29.140 align:start position:0% that there's one really important thing 00:30:29.140 --> 00:30:30.390 align:start position:0% that there's one really important thing I<00:30:29.290> missed<00:30:29.559> which<00:30:29.710> is<00:30:29.800> to<00:30:29.890> do<00:30:29.980> with<00:30:30.010> storage 00:30:30.390 --> 00:30:30.400 align:start position:0% I missed which is to do with storage 00:30:30.400 --> 00:30:31.680 align:start position:0% I missed which is to do with storage think<00:30:30.580> thanks<00:30:30.760> for<00:30:30.850> bringing<00:30:31.030> that<00:30:31.120> up<00:30:31.150> so<00:30:31.450> I 00:30:31.680 --> 00:30:31.690 align:start position:0% think thanks for bringing that up so I 00:30:31.690 --> 00:30:32.970 align:start position:0% think thanks for bringing that up so I mean<00:30:31.930> one<00:30:32.080> of<00:30:32.140> the<00:30:32.200> ways<00:30:32.320> that<00:30:32.350> it<00:30:32.590> generally 00:30:32.970 --> 00:30:32.980 align:start position:0% mean one of the ways that it generally 00:30:32.980 --> 00:30:34.410 align:start position:0% mean one of the ways that it generally to<00:30:33.100> try<00:30:33.250> off<00:30:33.400> with<00:30:33.520> my<00:30:33.610> storage<00:30:33.910> is<00:30:34.090> by<00:30:34.240> like 00:30:34.410 --> 00:30:34.420 align:start position:0% to try off with my storage is by like 00:30:34.420 --> 00:30:36.570 align:start position:0% to try off with my storage is by like packing<00:30:34.809> packing<00:30:35.500> things<00:30:36.010> together<00:30:36.130> to<00:30:36.430> try 00:30:36.570 --> 00:30:36.580 align:start position:0% packing packing things together to try 00:30:36.580 --> 00:30:38.610 align:start position:0% packing packing things together to try to<00:30:36.640> use<00:30:36.790> that<00:30:36.910> store<00:30:37.090> justify<00:30:37.690> regardless<00:30:38.530> of 00:30:38.610 --> 00:30:38.620 align:start position:0% to use that store justify regardless of 00:30:38.620 --> 00:30:39.660 align:start position:0% to use that store justify regardless of whether<00:30:38.800> that<00:30:38.860> would<00:30:39.070> be<00:30:39.100> a<00:30:39.190> good<00:30:39.309> idea<00:30:39.429> for 00:30:39.660 --> 00:30:39.670 align:start position:0% whether that would be a good idea for 00:30:39.670 --> 00:30:41.790 align:start position:0% whether that would be a good idea for any<00:30:39.850> answer<00:30:40.059> Pony<00:30:40.240> token<00:30:40.570> then<00:30:41.050> that<00:30:41.620> isn't 00:30:41.790 --> 00:30:41.800 align:start position:0% any answer Pony token then that isn't 00:30:41.800 --> 00:30:43.440 align:start position:0% any answer Pony token then that isn't really<00:30:41.920> compatible<00:30:42.250> with<00:30:42.550> our<00:30:42.730> with<00:30:43.330> our 00:30:43.440 --> 00:30:43.450 align:start position:0% really compatible with our with our 00:30:43.450 --> 00:30:45.690 align:start position:0% really compatible with our with our approach<00:30:43.690> here<00:30:43.900> because<00:30:44.580> what<00:30:45.580> we're 00:30:45.690 --> 00:30:45.700 align:start position:0% approach here because what we're 00:30:45.700 --> 00:30:47.160 align:start position:0% approach here because what we're formally<00:30:46.000> verifying<00:30:46.390> who<00:30:46.510> actually<00:30:46.660> needs<00:30:46.960> to 00:30:47.160 --> 00:30:47.170 align:start position:0% formally verifying who actually needs to 00:30:47.170 --> 00:30:49.710 align:start position:0% formally verifying who actually needs to specify<00:30:47.500> exactly<00:30:48.190> where<00:30:48.490> the<00:30:48.730> where<00:30:49.690> the 00:30:49.710 --> 00:30:49.720 align:start position:0% specify exactly where the where the 00:30:49.720 --> 00:30:51.570 align:start position:0% specify exactly where the where the storage<00:30:49.960> lives<00:30:50.230> firstly<00:30:50.650> and<00:30:50.800> secondly<00:30:51.100> the 00:30:51.570 --> 00:30:51.580 align:start position:0% storage lives firstly and secondly the 00:30:51.580 --> 00:30:53.310 align:start position:0% storage lives firstly and secondly the semantics<00:30:52.030> of<00:30:52.150> your<00:30:52.300> your<00:30:52.840> contract<00:30:53.290> you 00:30:53.310 --> 00:30:53.320 align:start position:0% semantics of your your contract you 00:30:53.320 --> 00:30:55.260 align:start position:0% semantics of your your contract you change<00:30:53.620> and<00:30:53.830> you<00:30:53.860> start<00:30:54.130> to<00:30:54.280> reduce<00:30:54.429> the<00:30:54.910> the 00:30:55.260 --> 00:30:55.270 align:start position:0% change and you start to reduce the the 00:30:55.270 --> 00:30:57.090 align:start position:0% change and you start to reduce the the size<00:30:55.840> of<00:30:56.140> the<00:30:56.230> the<00:30:56.260> integers<00:30:56.860> that<00:30:56.920> you're 00:30:57.090 --> 00:30:57.100 align:start position:0% size of the the integers that you're 00:30:57.100 --> 00:30:58.380 align:start position:0% size of the the integers that you're using<00:30:57.250> because<00:30:57.640> you<00:30:57.790> really<00:30:58.000> don't<00:30:58.059> start<00:30:58.330> to 00:30:58.380 --> 00:30:58.390 align:start position:0% using because you really don't start to 00:30:58.390 --> 00:30:59.880 align:start position:0% using because you really don't start to overflow<00:30:58.630> in<00:30:58.960> situations<00:30:59.440> where<00:30:59.590> otherwise 00:30:59.880 --> 00:30:59.890 align:start position:0% overflow in situations where otherwise 00:30:59.890 --> 00:31:02.070 align:start position:0% overflow in situations where otherwise wouldn't<00:31:00.190> have<00:31:00.250> so<00:31:01.179> that<00:31:01.420> that's<00:31:01.809> not<00:31:01.900> really 00:31:02.070 --> 00:31:02.080 align:start position:0% wouldn't have so that that's not really 00:31:02.080 --> 00:31:03.330 align:start position:0% wouldn't have so that that's not really going<00:31:02.200> to<00:31:02.260> work<00:31:02.440> and<00:31:02.710> in<00:31:02.830> particular<00:31:02.950> you 00:31:03.330 --> 00:31:03.340 align:start position:0% going to work and in particular you 00:31:03.340 --> 00:31:05.370 align:start position:0% going to work and in particular you actually<00:31:03.610> need<00:31:03.730> to<00:31:03.760> look<00:31:04.510> at<00:31:04.630> one<00:31:04.870> more<00:31:04.900> file 00:31:05.370 --> 00:31:05.380 align:start position:0% actually need to look at one more file 00:31:05.380 --> 00:31:07.890 align:start position:0% actually need to look at one more file in<00:31:05.650> this<00:31:05.770> repo<00:31:06.390> potentially<00:31:07.390> depending<00:31:07.570> on 00:31:07.890 --> 00:31:07.900 align:start position:0% in this repo potentially depending on 00:31:07.900 --> 00:31:10.860 align:start position:0% in this repo potentially depending on how<00:31:08.170> long<00:31:08.440> how<00:31:09.130> crazy<00:31:09.429> or<00:31:09.790> your<00:31:10.360> purchase 00:31:10.860 --> 00:31:10.870 align:start position:0% how long how crazy or your purchase 00:31:10.870 --> 00:31:12.570 align:start position:0% how long how crazy or your purchase which<00:31:11.350> is<00:31:11.470> the<00:31:11.590> storage<00:31:11.950> but<00:31:12.250> if<00:31:12.400> these 00:31:12.570 --> 00:31:12.580 align:start position:0% which is the storage but if these 00:31:12.580 --> 00:31:15.240 align:start position:0% which is the storage but if these business<00:31:13.000> story<00:31:13.270> specification<00:31:14.070> and<00:31:15.070> you're 00:31:15.240 --> 00:31:15.250 align:start position:0% business story specification and you're 00:31:15.250 --> 00:31:16.919 align:start position:0% business story specification and you're just<00:31:15.370> using<00:31:15.550> solidify<00:31:16.210> furtive<00:31:16.540> only<00:31:16.690> need<00:31:16.840> to 00:31:16.919 --> 00:31:16.929 align:start position:0% just using solidify furtive only need to 00:31:16.929 --> 00:31:19.830 align:start position:0% just using solidify furtive only need to do<00:31:17.080> is<00:31:17.350> follow<00:31:18.100> the<00:31:18.280> the<00:31:18.730> border<00:31:19.330> of<00:31:19.360> the 00:31:19.830 --> 00:31:19.840 align:start position:0% do is follow the the border of the 00:31:19.840 --> 00:31:23.760 align:start position:0% do is follow the the border of the stores<00:31:20.470> layout<00:31:20.860> that<00:31:21.840> that<00:31:22.840> we<00:31:23.440> gave<00:31:23.620> is<00:31:23.710> an 00:31:23.760 --> 00:31:23.770 align:start position:0% stores layout that that we gave is an 00:31:23.770 --> 00:31:25.950 align:start position:0% stores layout that that we gave is an example<00:31:24.010> which<00:31:24.250> is<00:31:24.370> balances<00:31:25.059> total<00:31:25.690> supply 00:31:25.950 --> 00:31:25.960 align:start position:0% example which is balances total supply 00:31:25.960 --> 00:31:27.180 align:start position:0% example which is balances total supply and<00:31:26.110> loans<00:31:26.260> and<00:31:26.530> so<00:31:26.679> as<00:31:26.770> long<00:31:26.890> as<00:31:26.950> the 00:31:27.180 --> 00:31:27.190 align:start position:0% and loans and so as long as the 00:31:27.190 --> 00:31:29.040 align:start position:0% and loans and so as long as the variables<00:31:27.790> are<00:31:27.880> good<00:31:27.970> parent<00:31:28.690> they'll<00:31:28.809> be<00:31:28.900> put 00:31:29.040 --> 00:31:29.050 align:start position:0% variables are good parent they'll be put 00:31:29.050 --> 00:31:30.450 align:start position:0% variables are good parent they'll be put in<00:31:29.110> the<00:31:29.200> right 00:31:30.450 --> 00:31:30.460 align:start position:0% in the right 00:31:30.460 --> 00:31:32.580 align:start position:0% in the right but<00:31:30.820> formally<00:31:31.480> what's<00:31:31.720> actually<00:31:31.870> going<00:31:32.170> on<00:31:32.350> if 00:31:32.580 --> 00:31:32.590 align:start position:0% but formally what's actually going on if 00:31:32.590 --> 00:31:33.840 align:start position:0% but formally what's actually going on if you're<00:31:32.710> using<00:31:32.860> more<00:31:33.070> of<00:31:33.190> a<00:31:33.280> level<00:31:33.550> approach 00:31:33.840 --> 00:31:33.850 align:start position:0% you're using more of a level approach 00:31:33.850 --> 00:31:36.000 align:start position:0% you're using more of a level approach then<00:31:34.510> it's<00:31:34.990> it's<00:31:35.290> actually<00:31:35.530> mapped<00:31:35.740> out<00:31:35.890> in 00:31:36.000 --> 00:31:36.010 align:start position:0% then it's it's actually mapped out in 00:31:36.010 --> 00:31:39.480 align:start position:0% then it's it's actually mapped out in this<00:31:36.130> file<00:31:36.370> so<00:31:37.120> I<00:31:37.840> mean<00:31:38.230> I<00:31:38.260> hope<00:31:38.680> that<00:31:38.740> probably 00:31:39.480 --> 00:31:39.490 align:start position:0% this file so I mean I hope that probably 00:31:39.490 --> 00:31:40.440 align:start position:0% this file so I mean I hope that probably if<00:31:39.550> you're<00:31:39.670> going<00:31:39.790> to<00:31:39.970> do<00:31:40.090> something<00:31:40.360> like 00:31:40.440 --> 00:31:40.450 align:start position:0% if you're going to do something like 00:31:40.450 --> 00:31:41.790 align:start position:0% if you're going to do something like this<00:31:40.600> video<00:31:40.780> already<00:31:41.110> know<00:31:41.260> how<00:31:41.440> solidity 00:31:41.790 --> 00:31:41.800 align:start position:0% this video already know how solidity 00:31:41.800 --> 00:31:45.210 align:start position:0% this video already know how solidity places<00:31:42.550> instance<00:31:42.940> variables<00:31:43.570> otherwise<00:31:44.220> it's 00:31:45.210 --> 00:31:45.220 align:start position:0% places instance variables otherwise it's 00:31:45.220 --> 00:31:48.960 align:start position:0% places instance variables otherwise it's going<00:31:45.370> to<00:31:45.430> be<00:31:45.550> a<00:31:46.350> few<00:31:47.350> things<00:31:47.470> to<00:31:47.620> it<00:31:47.740> but<00:31:48.730> you 00:31:48.960 --> 00:31:48.970 align:start position:0% going to be a few things to it but you 00:31:48.970 --> 00:31:50.400 align:start position:0% going to be a few things to it but you know<00:31:49.060> for<00:31:49.540> simple<00:31:49.750> for<00:31:49.900> simple<00:31:50.080> variables 00:31:50.400 --> 00:31:50.410 align:start position:0% know for simple for simple variables 00:31:50.410 --> 00:31:52.050 align:start position:0% know for simple for simple variables that<00:31:50.500> are<00:31:50.590> not<00:31:50.650> things<00:31:50.920> like<00:31:51.070> like<00:31:51.820> the<00:31:51.910> total 00:31:52.050 --> 00:31:52.060 align:start position:0% that are not things like like the total 00:31:52.060 --> 00:31:54.510 align:start position:0% that are not things like like the total supply<00:31:52.270> they're<00:31:53.260> just<00:31:53.440> going<00:31:53.560> into<00:31:53.800> the<00:31:53.980> swap 00:31:54.510 --> 00:31:54.520 align:start position:0% supply they're just going into the swap 00:31:54.520 --> 00:31:56.040 align:start position:0% supply they're just going into the swap number<00:31:55.060> and<00:31:55.180> the<00:31:55.240> corresponds<00:31:55.690> to<00:31:55.810> the 00:31:56.040 --> 00:31:56.050 align:start position:0% number and the corresponds to the 00:31:56.050 --> 00:31:59.010 align:start position:0% number and the corresponds to the starting<00:31:56.830> from<00:31:56.920> zero<00:31:57.220> the<00:31:57.750> order<00:31:58.750> that<00:31:58.900> the 00:31:59.010 --> 00:31:59.020 align:start position:0% starting from zero the order that the 00:31:59.020 --> 00:32:00.060 align:start position:0% starting from zero the order that the variable<00:31:59.440> is<00:31:59.530> declared 00:32:00.060 --> 00:32:00.070 align:start position:0% variable is declared 00:32:00.070 --> 00:32:02.190 align:start position:0% variable is declared so<00:32:00.430> total<00:32:00.700> supply<00:32:00.970> of<00:32:01.000> example<00:32:01.540> it<00:32:01.630> visits<00:32:01.990> top 00:32:02.190 --> 00:32:02.200 align:start position:0% so total supply of example it visits top 00:32:02.200 --> 00:32:03.900 align:start position:0% so total supply of example it visits top one<00:32:02.470> so<00:32:03.040> you<00:32:03.130> know<00:32:03.340> if<00:32:03.400> you<00:32:03.490> want<00:32:03.640> to<00:32:03.700> if<00:32:03.820> you 00:32:03.900 --> 00:32:03.910 align:start position:0% one so you know if you want to if you 00:32:03.910 --> 00:32:05.070 align:start position:0% one so you know if you want to if you want<00:32:03.970> to<00:32:04.090> store<00:32:04.240> the<00:32:04.330> total<00:32:04.540> supply<00:32:04.630> you<00:32:04.810> just 00:32:05.070 --> 00:32:05.080 align:start position:0% want to store the total supply you just 00:32:05.080 --> 00:32:10.880 align:start position:0% want to store the total supply you just do<00:32:05.260> s<00:32:05.590> store<00:32:06.010> one<00:32:06.750> into<00:32:07.750> the<00:32:07.930> supply 00:32:10.880 --> 00:32:10.890 align:start position:0% 00:32:10.890 --> 00:32:13.170 align:start position:0% well-well-well<00:32:11.890> mappings<00:32:12.460> like<00:32:12.640> balances 00:32:13.170 --> 00:32:13.180 align:start position:0% well-well-well mappings like balances 00:32:13.180 --> 00:32:15.450 align:start position:0% well-well-well mappings like balances and<00:32:13.390> then<00:32:13.660> to<00:32:14.080> deep<00:32:14.290> mappings<00:32:14.800> like<00:32:15.040> like 00:32:15.450 --> 00:32:15.460 align:start position:0% and then to deep mappings like like 00:32:15.460 --> 00:32:16.920 align:start position:0% and then to deep mappings like like allowances<00:32:15.940> are<00:32:16.090> a<00:32:16.120> bit<00:32:16.210> more<00:32:16.330> complicated 00:32:16.920 --> 00:32:16.930 align:start position:0% allowances are a bit more complicated 00:32:16.930 --> 00:32:18.540 align:start position:0% allowances are a bit more complicated they're<00:32:17.260> computed<00:32:17.650> using<00:32:17.860> hashes<00:32:18.370> and 00:32:18.540 --> 00:32:18.550 align:start position:0% they're computed using hashes and 00:32:18.550 --> 00:32:20.100 align:start position:0% they're computed using hashes and invective<00:32:18.910> and<00:32:19.330> conventions<00:32:19.750> as<00:32:19.810> Martin<00:32:20.050> said 00:32:20.100 --> 00:32:20.110 align:start position:0% invective and conventions as Martin said 00:32:20.110 --> 00:32:21.780 align:start position:0% invective and conventions as Martin said there's<00:32:20.380> a<00:32:20.440> living<00:32:20.620> Piper<00:32:20.950> and<00:32:21.310> they<00:32:21.580> hash 00:32:21.780 --> 00:32:21.790 align:start position:0% there's a living Piper and they hash 00:32:21.790 --> 00:32:24.810 align:start position:0% there's a living Piper and they hash things<00:32:22.000> in<00:32:22.180> the<00:32:22.270> opposite<00:32:22.630> order<00:32:23.010> and<00:32:24.010> by 00:32:24.810 --> 00:32:24.820 align:start position:0% things in the opposite order and by 00:32:24.820 --> 00:32:26.370 align:start position:0% things in the opposite order and by default<00:32:25.150> this<00:32:25.420> files<00:32:25.720> can<00:32:25.930> be<00:32:25.990> configured<00:32:26.200> to 00:32:26.370 --> 00:32:26.380 align:start position:0% default this files can be configured to 00:32:26.380 --> 00:32:28.380 align:start position:0% default this files can be configured to use<00:32:26.470> the<00:32:26.560> solidity<00:32:26.890> order<00:32:27.490> so<00:32:28.060> there's<00:32:28.270> always 00:32:28.380 --> 00:32:28.390 align:start position:0% use the solidity order so there's always 00:32:28.390 --> 00:32:30.480 align:start position:0% use the solidity order so there's always my<00:32:28.600> sense<00:32:28.840> of<00:32:28.960> solidity<00:32:29.080> here<00:32:29.590> if<00:32:29.920> I<00:32:30.220> wanted<00:32:30.430> to 00:32:30.480 --> 00:32:30.490 align:start position:0% my sense of solidity here if I wanted to 00:32:30.490 --> 00:32:32.550 align:start position:0% my sense of solidity here if I wanted to use<00:32:30.670> my<00:32:30.820> for<00:32:31.030> instead<00:32:31.390> what<00:32:31.930> I<00:32:31.960> would<00:32:32.170> do<00:32:32.290> is<00:32:32.410> I 00:32:32.550 --> 00:32:32.560 align:start position:0% use my for instead what I would do is I 00:32:32.560 --> 00:32:34.740 align:start position:0% use my for instead what I would do is I would<00:32:32.590> um<00:32:32.940> you<00:32:33.940> need<00:32:34.090> to<00:32:34.210> actually<00:32:34.480> replace 00:32:34.740 --> 00:32:34.750 align:start position:0% would um you need to actually replace 00:32:34.750 --> 00:32:37.890 align:start position:0% would um you need to actually replace this<00:32:35.590> with<00:32:36.150> with<00:32:37.150> VIPRE<00:32:37.390> and<00:32:37.690> then<00:32:37.780> we're 00:32:37.890 --> 00:32:37.900 align:start position:0% this with with VIPRE and then we're 00:32:37.900 --> 00:32:38.880 align:start position:0% this with with VIPRE and then we're gonna<00:32:37.990> hash<00:32:38.200> things<00:32:38.350> in<00:32:38.500> the<00:32:38.560> opposite<00:32:38.830> order 00:32:38.880 --> 00:32:38.890 align:start position:0% gonna hash things in the opposite order 00:32:38.890 --> 00:32:43.050 align:start position:0% gonna hash things in the opposite order no<00:32:40.710> you<00:32:41.710> know<00:32:41.800> for<00:32:42.340> the<00:32:42.400> details<00:32:42.730> of<00:32:42.880> how<00:32:43.000> to 00:32:43.050 --> 00:32:43.060 align:start position:0% no you know for the details of how to 00:32:43.060 --> 00:32:44.550 align:start position:0% no you know for the details of how to how<00:32:43.570> it's<00:32:43.720> actually<00:32:43.840> hacked<00:32:44.170> I<00:32:44.320> think<00:32:44.500> the 00:32:44.550 --> 00:32:44.560 align:start position:0% how it's actually hacked I think the 00:32:44.560 --> 00:32:45.510 align:start position:0% how it's actually hacked I think the best<00:32:44.710> thing<00:32:44.890> would<00:32:44.980> be<00:32:45.040> that<00:32:45.130> if<00:32:45.370> you're 00:32:45.510 --> 00:32:45.520 align:start position:0% best thing would be that if you're 00:32:45.520 --> 00:32:47.310 align:start position:0% best thing would be that if you're interested<00:32:45.760> in<00:32:46.060> experimenting<00:32:46.600> with<00:32:47.050> this<00:32:47.140> is 00:32:47.310 --> 00:32:47.320 align:start position:0% interested in experimenting with this is 00:32:47.320 --> 00:32:49.410 align:start position:0% interested in experimenting with this is the<00:32:47.440> you<00:32:47.590> raise<00:32:47.710> your<00:32:47.740> hand<00:32:48.120> one<00:32:49.120> of<00:32:49.150> us<00:32:49.300> will 00:32:49.410 --> 00:32:49.420 align:start position:0% the you raise your hand one of us will 00:32:49.420 --> 00:32:51.690 align:start position:0% the you raise your hand one of us will come<00:32:49.650> come<00:32:50.650> and<00:32:50.860> show<00:32:51.070> you<00:32:51.130> to<00:32:51.250> make<00:32:51.400> sure<00:32:51.430> that 00:32:51.690 --> 00:32:51.700 align:start position:0% come come and show you to make sure that 00:32:51.700 --> 00:32:53.610 align:start position:0% come come and show you to make sure that it's<00:32:52.270> correct<00:32:52.450> just<00:32:52.780> because<00:32:53.020> maybe<00:32:53.320> even 00:32:53.610 --> 00:32:53.620 align:start position:0% it's correct just because maybe even 00:32:53.620 --> 00:32:55.200 align:start position:0% it's correct just because maybe even most<00:32:53.710> people<00:32:54.040> aren't<00:32:54.700> interested<00:32:55.090> in<00:32:55.120> that 00:32:55.200 --> 00:32:55.210 align:start position:0% most people aren't interested in that 00:32:55.210 --> 00:32:56.880 align:start position:0% most people aren't interested in that it's<00:32:55.420> not<00:32:55.540> worth<00:32:55.720> it<00:32:55.840> spending<00:32:56.140> five<00:32:56.860> minutes 00:32:56.880 --> 00:32:56.890 align:start position:0% it's not worth it spending five minutes 00:32:56.890 --> 00:33:05.060 align:start position:0% it's not worth it spending five minutes explaining<00:32:57.370> it<00:32:57.610> right<00:32:57.730> now 00:33:05.060 --> 00:33:05.070 align:start position:0% 00:33:05.070 --> 00:33:07.110 align:start position:0% allowances<00:33:06.070> like<00:33:06.250> yeah<00:33:06.400> I<00:33:06.430> think<00:33:06.700> these<00:33:06.820> were 00:33:07.110 --> 00:33:07.120 align:start position:0% allowances like yeah I think these were 00:33:07.120 --> 00:33:10.710 align:start position:0% allowances like yeah I think these were their<00:33:07.240> over<00:33:07.420> source<00:33:07.660> destination<00:33:07.870> so<00:33:09.720> donor 00:33:10.710 --> 00:33:10.720 align:start position:0% their over source destination so donor 00:33:10.720 --> 00:33:15.120 align:start position:0% their over source destination so donor and<00:33:10.840> spender<00:33:11.140> is<00:33:11.200> also<00:33:11.470> correct<00:33:13.530> okay<00:33:14.530> so<00:33:14.560> then 00:33:15.120 --> 00:33:15.130 align:start position:0% and spender is also correct okay so then 00:33:15.130 --> 00:33:16.920 align:start position:0% and spender is also correct okay so then let's<00:33:15.430> get<00:33:15.760> started<00:33:15.820> if<00:33:16.420> you<00:33:16.480> have<00:33:16.600> a<00:33:16.630> question 00:33:16.920 --> 00:33:16.930 align:start position:0% let's get started if you have a question 00:33:16.930 --> 00:33:18.150 align:start position:0% let's get started if you have a question please<00:33:17.020> please<00:33:17.350> please<00:33:17.560> raise<00:33:17.710> your<00:33:17.800> hand<00:33:18.010> or 00:33:18.150 --> 00:33:18.160 align:start position:0% please please please raise your hand or 00:33:18.160 --> 00:33:20.300 align:start position:0% please please please raise your hand or justice 00:33:20.300 --> 00:33:20.310 align:start position:0% justice 00:33:20.310 --> 00:34:02.550 align:start position:0% justice [Music] 00:34:02.550 --> 00:34:02.560 align:start position:0% 00:34:02.560 --> 00:34:16.760 align:start position:0% [Music] 00:34:16.760 --> 00:34:16.770 align:start position:0% 00:34:16.770 --> 00:34:22.899 align:start position:0% effective<00:34:17.770> of<00:34:17.920> contractors<00:34:18.700> later 00:34:22.899 --> 00:34:22.909 align:start position:0% 00:34:22.909 --> 00:34:31.850 align:start position:0% [Music] 00:34:31.850 --> 00:34:31.860 align:start position:0% 00:34:31.860 --> 00:34:34.310 align:start position:0% just<00:34:32.850> just<00:34:33.000> one<00:34:33.210> interesting<00:34:33.929> fun 00:34:34.310 --> 00:34:34.320 align:start position:0% just just one interesting fun 00:34:34.320 --> 00:34:35.840 align:start position:0% just just one interesting fun interesting<00:34:34.500> piece<00:34:34.770> of<00:34:34.800> information<00:34:35.070> so<00:34:35.580> this 00:34:35.840 --> 00:34:35.850 align:start position:0% interesting piece of information so this 00:34:35.850 --> 00:34:39.230 align:start position:0% interesting piece of information so this one<00:34:36.510> that<00:34:36.540> I<00:34:36.750> tried<00:34:37.020> with<00:34:37.320> with<00:34:38.100> with<00:34:38.730> instead 00:34:39.230 --> 00:34:39.240 align:start position:0% one that I tried with with with instead 00:34:39.240 --> 00:34:40.370 align:start position:0% one that I tried with with with instead to<00:34:39.480> replace 00:34:40.370 --> 00:34:40.380 align:start position:0% to replace 00:34:40.380 --> 00:34:45.350 align:start position:0% to replace six<00:34:40.830> zero<00:34:41.100> zero<00:34:41.370> zero<00:34:42.290> with<00:34:43.310> with<00:34:44.310> 34<00:34:45.090> and 00:34:45.350 --> 00:34:45.360 align:start position:0% six zero zero zero with with 34 and 00:34:45.360 --> 00:34:47.150 align:start position:0% six zero zero zero with with 34 and actually<00:34:45.720> uh<00:34:45.890> yeah<00:34:46.890> I<00:34:46.980> can<00:34:47.130> actually 00:34:47.150 --> 00:34:47.160 align:start position:0% actually uh yeah I can actually 00:34:47.160 --> 00:34:48.890 align:start position:0% actually uh yeah I can actually corrupted<00:34:47.790> something<00:34:48.090> and<00:34:48.360> the<00:34:48.600> formal 00:34:48.890 --> 00:34:48.900 align:start position:0% corrupted something and the formal 00:34:48.900 --> 00:34:50.990 align:start position:0% corrupted something and the formal verification<00:34:49.080> just<00:34:49.530> came<00:34:49.710> back<00:34:50.000> negative 00:34:50.990 --> 00:34:51.000 align:start position:0% verification just came back negative 00:34:51.000 --> 00:34:55.070 align:start position:0% verification just came back negative very<00:34:51.510> bad<00:34:51.810> very<00:34:52.500> bad<00:34:52.620> results<00:34:53.600> don't<00:34:54.600> try<00:34:55.020> this 00:34:55.070 --> 00:34:55.080 align:start position:0% very bad very bad results don't try this 00:34:55.080 --> 00:34:58.550 align:start position:0% very bad very bad results don't try this one<00:34:55.460> you<00:34:56.460> will<00:34:56.580> be<00:34:56.760> wasting<00:34:57.110> wasting<00:34:58.110> a<00:34:58.350> time 00:34:58.550 --> 00:34:58.560 align:start position:0% one you will be wasting wasting a time 00:34:58.560 --> 00:35:00.290 align:start position:0% one you will be wasting wasting a time so<00:34:59.010> honest<00:34:59.490> as<00:34:59.610> I<00:34:59.730> don't<00:34:59.970> think<00:35:00.150> it's<00:35:00.240> a 00:35:00.290 --> 00:35:00.300 align:start position:0% so honest as I don't think it's a 00:35:00.300 --> 00:35:04.510 align:start position:0% so honest as I don't think it's a success<00:35:00.990> for<00:35:01.290> a<00:35:01.790> performer<00:35:02.790> patient<00:35:03.300> may<00:35:03.540> be<00:35:03.570> a 00:35:04.510 --> 00:35:04.520 align:start position:0% success for a performer patient may be a 00:35:04.520 --> 00:35:12.740 align:start position:0% success for a performer patient may be a bad<00:35:05.520> day<00:35:05.790> for<00:35:10.760> no<00:35:11.760> one<00:35:11.880> actually<00:35:12.120> just<00:35:12.390> just 00:35:12.740 --> 00:35:12.750 align:start position:0% bad day for no one actually just just 00:35:12.750 --> 00:35:14.450 align:start position:0% bad day for no one actually just just one<00:35:13.050> well<00:35:13.320> the<00:35:13.680> way<00:35:13.830> we<00:35:13.920> set<00:35:14.100> it<00:35:14.130> up<00:35:14.250> is<00:35:14.370> the 00:35:14.450 --> 00:35:14.460 align:start position:0% one well the way we set it up is the 00:35:14.460 --> 00:35:16.310 align:start position:0% one well the way we set it up is the first<00:35:14.670> failure<00:35:14.880> causes<00:35:15.330> at<00:35:15.480> all<00:35:15.600> that<00:35:15.780> all<00:35:16.050> the 00:35:16.310 --> 00:35:16.320 align:start position:0% first failure causes at all that all the 00:35:16.320 --> 00:35:17.900 align:start position:0% first failure causes at all that all the stops<00:35:16.560> are<00:35:16.740> don't<00:35:16.920> waste<00:35:17.130> time<00:35:17.280> so<00:35:17.550> take<00:35:17.790> the 00:35:17.900 --> 00:35:17.910 align:start position:0% stops are don't waste time so take the 00:35:17.910 --> 00:35:21.940 align:start position:0% stops are don't waste time so take the transfer<00:35:18.240> front<00:35:18.480> function<00:35:18.870> they<00:35:19.830> have 00:35:21.940 --> 00:35:21.950 align:start position:0% transfer front function they have 00:35:21.950 --> 00:35:27.710 align:start position:0% transfer front function they have nothing<00:35:22.950> actually<00:35:23.420> very<00:35:24.420> quickly<00:35:25.880> again<00:35:26.880> if 00:35:27.710 --> 00:35:27.720 align:start position:0% nothing actually very quickly again if 00:35:27.720 --> 00:35:29.420 align:start position:0% nothing actually very quickly again if that's<00:35:27.870> your<00:35:28.110> kind<00:35:28.260> because<00:35:28.770> a<00:35:28.920> cup<00:35:29.130> of<00:35:29.250> tea 00:35:29.420 --> 00:35:29.430 align:start position:0% that's your kind because a cup of tea 00:35:29.430 --> 00:35:30.740 align:start position:0% that's your kind because a cup of tea you<00:35:29.640> know<00:35:29.730> another<00:35:29.880> thing<00:35:30.000> in<00:35:30.210> to<00:35:30.510> investigate 00:35:30.740 --> 00:35:30.750 align:start position:0% you know another thing in to investigate 00:35:30.750 --> 00:35:32.270 align:start position:0% you know another thing in to investigate would<00:35:31.260> be<00:35:31.350> to<00:35:31.410> figure<00:35:31.650> out<00:35:31.740> why<00:35:31.950> it's 00:35:32.270 --> 00:35:32.280 align:start position:0% would be to figure out why it's 00:35:32.280 --> 00:35:33.710 align:start position:0% would be to figure out why it's optimization<00:35:32.790> is<00:35:32.880> on<00:35:33.000> stage<00:35:33.210> maybe<00:35:33.450> how<00:35:33.690> to 00:35:33.710 --> 00:35:33.720 align:start position:0% optimization is on stage maybe how to 00:35:33.720 --> 00:35:36.940 align:start position:0% optimization is on stage maybe how to make<00:35:33.960> it<00:35:34.080> stay 00:35:36.940 --> 00:35:36.950 align:start position:0% 00:35:36.950 --> 00:35:42.410 align:start position:0% [Music] 00:35:42.410 --> 00:35:42.420 align:start position:0% 00:35:42.420 --> 00:35:53.770 align:start position:0% [Music] 00:35:53.770 --> 00:35:53.780 align:start position:0% 00:35:53.780 --> 00:36:19.610 align:start position:0% [Music] 00:36:19.610 --> 00:36:19.620 align:start position:0% 00:36:19.620 --> 00:36:30.610 align:start position:0% [Music] 00:36:30.610 --> 00:36:30.620 align:start position:0% 00:36:30.620 --> 00:36:53.390 align:start position:0% [Music] 00:36:53.390 --> 00:36:53.400 align:start position:0% 00:36:53.400 --> 00:37:05.960 align:start position:0% we 00:37:05.960 --> 00:37:05.970 align:start position:0% 00:37:05.970 --> 00:37:10.599 align:start position:0% I<00:37:06.000> only<00:37:06.840> took<00:37:07.050> this<00:37:07.230> small<00:37:07.500> break<00:37:07.740> to<00:37:07.890> get<00:37:08.040> this 00:37:10.599 --> 00:37:10.609 align:start position:0% 00:37:10.609 --> 00:37:19.920 align:start position:0% supposed<00:37:11.609> to<00:37:11.640> take<00:37:11.820> much 00:37:19.920 --> 00:37:19.930 align:start position:0% 00:37:19.930 --> 00:37:29.540 align:start position:0% I<00:37:20.859> can<00:37:21.279> ask<00:37:21.430> for<00:37:21.760> someone<00:37:22.059> to<00:37:22.119> cover 00:37:29.540 --> 00:37:29.550 align:start position:0% 00:37:29.550 --> 00:37:34.140 align:start position:0% I<00:37:29.580> should<00:37:30.740> jokes<00:37:31.740> la-di-da 00:37:34.140 --> 00:37:34.150 align:start position:0% I should jokes la-di-da 00:37:34.150 --> 00:38:00.250 align:start position:0% I should jokes la-di-da I<00:37:34.710> could<00:37:35.710> search<00:37:35.950> for<00:37:35.980> my<00:37:36.309> username<00:37:39.690> Archer 00:38:00.250 --> 00:38:00.260 align:start position:0% 00:38:00.260 --> 00:38:11.760 align:start position:0% [Music] 00:38:11.760 --> 00:38:11.770 align:start position:0% 00:38:11.770 --> 00:38:19.500 align:start position:0% the<00:38:12.100> party<00:38:12.450> okay 00:38:19.500 --> 00:38:19.510 align:start position:0% 00:38:19.510 --> 00:38:34.390 align:start position:0% [Music] 00:38:34.390 --> 00:38:34.400 align:start position:0% 00:38:34.400 --> 00:38:49.100 align:start position:0% [Applause] 00:38:49.100 --> 00:38:49.110 align:start position:0% 00:38:49.110 --> 00:38:59.120 align:start position:0% [Music] 00:38:59.120 --> 00:38:59.130 align:start position:0% 00:38:59.130 --> 00:39:02.490 align:start position:0% [Music] 00:39:02.490 --> 00:39:02.500 align:start position:0% 00:39:02.500 --> 00:39:10.680 align:start position:0% like<00:39:03.010> knowing<00:39:03.369> that<00:39:03.400> I<00:39:03.700> said<00:39:03.910> I<00:39:07.020> forget 00:39:10.680 --> 00:39:10.690 align:start position:0% 00:39:10.690 --> 00:39:31.160 align:start position:0% [Music] 00:39:31.160 --> 00:39:31.170 align:start position:0% 00:39:31.170 --> 00:39:39.550 align:start position:0% [Music] 00:39:39.550 --> 00:39:39.560 align:start position:0% 00:39:39.560 --> 00:39:45.420 align:start position:0% [Music] 00:39:45.420 --> 00:39:45.430 align:start position:0% 00:39:45.430 --> 00:39:51.210 align:start position:0% [Music] 00:39:51.210 --> 00:39:51.220 align:start position:0% 00:39:51.220 --> 00:40:23.500 align:start position:0% [Music] 00:40:23.500 --> 00:40:25.560 align:start position:0% 00:40:25.560 --> 00:40:25.570 align:start position:0% 00:40:25.570 --> 00:40:29.440 align:start position:0% mr.<00:40:26.570> practice<00:40:26.990> currently<00:40:27.200> death 00:40:29.440 --> 00:40:29.450 align:start position:0% mr. practice currently death 00:40:29.450 --> 00:40:45.040 align:start position:0% mr. practice currently death [Music] 00:40:45.040 --> 00:40:45.050 align:start position:0% 00:40:45.050 --> 00:40:55.470 align:start position:0% Jesus 00:40:55.470 --> 00:40:55.480 align:start position:0% 00:40:55.480 --> 00:41:12.270 align:start position:0% [Music] 00:41:12.270 --> 00:41:12.280 align:start position:0% 00:41:12.280 --> 00:41:37.270 align:start position:0% [Music] 00:41:37.270 --> 00:41:37.280 align:start position:0% 00:41:37.280 --> 00:41:46.600 align:start position:0% [Music] 00:41:46.600 --> 00:41:46.610 align:start position:0% 00:41:46.610 --> 00:42:51.009 align:start position:0% [Music] 00:42:51.009 --> 00:42:51.019 align:start position:0% 00:42:51.019 --> 00:43:17.349 align:start position:0% my<00:42:52.519> segment 00:43:17.349 --> 00:43:17.359 align:start position:0% 00:43:17.359 --> 00:44:08.470 align:start position:0% I<00:43:17.390> know 00:44:08.470 --> 00:44:08.480 align:start position:0% 00:44:08.480 --> 00:44:34.760 align:start position:0% [Music] 00:44:34.760 --> 00:44:34.770 align:start position:0% 00:44:34.770 --> 00:44:52.620 align:start position:0% any<00:44:35.770> questions<00:44:36.250> or 00:44:52.620 --> 00:44:52.630 align:start position:0% 00:44:52.630 --> 00:45:19.960 align:start position:0% yes 00:45:19.960 --> 00:45:19.970 align:start position:0% 00:45:19.970 --> 00:45:40.890 align:start position:0% [Music] 00:45:40.890 --> 00:45:40.900 align:start position:0% 00:45:40.900 --> 00:45:53.290 align:start position:0% Eliott<00:45:41.900> never<00:45:42.080> easy 00:45:53.290 --> 00:45:53.300 align:start position:0% 00:45:53.300 --> 00:46:07.620 align:start position:0% our<00:45:54.440> neighbors<00:45:55.440> now<00:45:55.620> the<00:45:55.680> most<00:45:55.890> unstable 00:46:07.620 --> 00:46:07.630 align:start position:0% 00:46:07.630 --> 00:46:15.860 align:start position:0% [Music] 00:46:15.860 --> 00:46:15.870 align:start position:0% 00:46:15.870 --> 00:46:17.290 align:start position:0% [Music] 00:46:17.290 --> 00:46:17.300 align:start position:0% [Music] 00:46:17.300 --> 00:46:22.750 align:start position:0% [Music] sir 00:46:22.750 --> 00:46:22.760 align:start position:0% 00:46:22.760 --> 00:46:23.560 align:start position:0% ooh 00:46:23.560 --> 00:46:23.570 align:start position:0% ooh 00:46:23.570 --> 00:46:42.200 align:start position:0% ooh [Music] 00:46:42.200 --> 00:46:42.210 align:start position:0% 00:46:42.210 --> 00:47:15.870 align:start position:0% [Music] 00:47:15.870 --> 00:47:15.880 align:start position:0% 00:47:15.880 --> 00:47:20.800 align:start position:0% [Music] 00:47:20.800 --> 00:47:20.810 align:start position:0% 00:47:20.810 --> 00:47:29.980 align:start position:0% you<00:47:21.810> jump 00:47:29.980 --> 00:47:29.990 align:start position:0% 00:47:29.990 --> 00:47:46.470 align:start position:0% robust<00:47:30.470> and<00:47:30.680> stay<00:47:30.859> out 00:47:46.470 --> 00:47:46.480 align:start position:0% 00:47:46.480 --> 00:48:01.990 align:start position:0% so<00:47:47.480> I<00:47:47.510> just<00:47:47.690> read<00:47:47.870> one<00:47:48.440> time<00:47:51.160> yes<00:47:52.160> it<00:47:52.610> is 00:48:01.990 --> 00:48:02.000 align:start position:0% 00:48:02.000 --> 00:48:17.380 align:start position:0% president 00:48:17.380 --> 00:48:17.390 align:start position:0% 00:48:17.390 --> 00:48:24.090 align:start position:0% [Music] 00:48:24.090 --> 00:48:24.100 align:start position:0% 00:48:24.100 --> 00:48:30.910 align:start position:0% [Music] 00:48:30.910 --> 00:48:30.920 align:start position:0% 00:48:30.920 --> 00:48:43.180 align:start position:0% [Music] 00:48:43.180 --> 00:48:43.190 align:start position:0% 00:48:43.190 --> 00:48:44.499 align:start position:0% [Music] 00:48:44.499 --> 00:48:44.509 align:start position:0% [Music] 00:48:44.509 --> 00:48:56.150 align:start position:0% [Music] yeah 00:48:56.150 --> 00:48:56.160 align:start position:0% 00:48:56.160 --> 00:48:59.180 align:start position:0% we're<00:48:57.160> gonna<00:48:57.310> do<00:48:57.520> submissions<00:48:58.480> which<00:48:58.750> is 00:48:59.180 --> 00:48:59.190 align:start position:0% we're gonna do submissions which is 00:48:59.190 --> 00:49:02.270 align:start position:0% we're gonna do submissions which is sliding<00:49:00.190> around<00:49:00.310> with<00:49:00.610> the<00:49:00.730> optimizers<00:49:01.300> flag 00:49:02.270 --> 00:49:02.280 align:start position:0% sliding around with the optimizers flag 00:49:02.280 --> 00:49:07.350 align:start position:0% sliding around with the optimizers flag which<00:49:04.500> comes<00:49:05.500> in<00:49:05.650> Clarkson<00:49:06.280> and<00:49:06.490> exactly<00:49:07.180> the 00:49:07.350 --> 00:49:07.360 align:start position:0% which comes in Clarkson and exactly the 00:49:07.360 --> 00:49:22.750 align:start position:0% which comes in Clarkson and exactly the same<00:49:07.600> amount<00:49:07.870> of<00:49:07.990> gas<00:49:08.170> is<00:49:08.500> going<00:49:08.530> without 00:49:22.750 --> 00:49:22.760 align:start position:0% 00:49:22.760 --> 00:49:43.210 align:start position:0% [Music] 00:49:43.210 --> 00:49:43.220 align:start position:0% 00:49:43.220 --> 00:50:00.610 align:start position:0% I<00:49:44.050> mean<00:49:45.050> the<00:49:47.560> very<00:49:48.560> last<00:49:48.830> night 00:50:00.610 --> 00:50:00.620 align:start position:0% 00:50:00.620 --> 00:50:07.620 align:start position:0% [Music] 00:50:07.620 --> 00:50:07.630 align:start position:0% 00:50:07.630 --> 00:50:42.820 align:start position:0% [Music] 00:50:42.820 --> 00:50:42.830 align:start position:0% 00:50:42.830 --> 00:50:46.450 align:start position:0% [Music] 00:50:46.450 --> 00:50:46.460 align:start position:0% 00:50:46.460 --> 00:50:52.920 align:start position:0% yes 00:50:52.920 --> 00:50:52.930 align:start position:0% 00:50:52.930 --> 00:51:39.950 align:start position:0% argit 00:51:39.950 --> 00:51:39.960 align:start position:0% 00:51:39.960 --> 00:51:50.970 align:start position:0% at<00:51:40.960> birth 00:51:50.970 --> 00:51:50.980 align:start position:0% 00:51:50.980 --> 00:51:55.429 align:start position:0% [Applause]