WEBVTT Kind: captions Language: en 00:00:11.980 --> 00:00:13.509 align:start position:0% hello<00:00:12.980> everyone 00:00:13.509 --> 00:00:13.519 align:start position:0% hello everyone 00:00:13.519 --> 00:00:16.390 align:start position:0% hello everyone test<00:00:13.789> test<00:00:14.379> yeah<00:00:15.409> I'm<00:00:15.589> Everett<00:00:15.889> Hilton<00:00:16.190> Brandt 00:00:16.390 --> 00:00:16.400 align:start position:0% test test yeah I'm Everett Hilton Brandt 00:00:16.400 --> 00:00:18.880 align:start position:0% test test yeah I'm Everett Hilton Brandt and<00:00:16.970> I<00:00:17.660> should<00:00:17.840> have<00:00:17.930> put<00:00:18.080> also<00:00:18.290> my<00:00:18.560> group<00:00:18.740> on 00:00:18.880 --> 00:00:18.890 align:start position:0% and I should have put also my group on 00:00:18.890 --> 00:00:20.080 align:start position:0% and I should have put also my group on there<00:00:19.070> but<00:00:19.250> I<00:00:19.280> was<00:00:19.460> kind<00:00:19.610> of<00:00:19.670> in<00:00:19.760> a<00:00:19.820> rush<00:00:19.940> to 00:00:20.080 --> 00:00:20.090 align:start position:0% there but I was kind of in a rush to 00:00:20.090 --> 00:00:21.070 align:start position:0% there but I was kind of in a rush to make<00:00:20.120> the<00:00:20.270> slides<00:00:20.510> because<00:00:20.720> it<00:00:20.870> was<00:00:20.960> all<00:00:21.050> a 00:00:21.070 --> 00:00:21.080 align:start position:0% make the slides because it was all a 00:00:21.080 --> 00:00:22.420 align:start position:0% make the slides because it was all a little<00:00:21.170> bit<00:00:21.320> last-minute<00:00:21.710> but<00:00:22.070> you<00:00:22.340> know 00:00:22.420 --> 00:00:22.430 align:start position:0% little bit last-minute but you know 00:00:22.430 --> 00:00:24.010 align:start position:0% little bit last-minute but you know that's<00:00:22.610> how<00:00:22.700> it<00:00:22.730> goes 00:00:24.010 --> 00:00:24.020 align:start position:0% that's how it goes 00:00:24.020 --> 00:00:25.900 align:start position:0% that's how it goes and<00:00:24.260> the<00:00:24.770> original<00:00:25.100> title<00:00:25.370> was<00:00:25.400> overview<00:00:25.850> on 00:00:25.900 --> 00:00:25.910 align:start position:0% and the original title was overview on 00:00:25.910 --> 00:00:27.280 align:start position:0% and the original title was overview on progress<00:00:26.210> report<00:00:26.570> and<00:00:26.720> then<00:00:26.870> I<00:00:26.900> decided 00:00:27.280 --> 00:00:27.290 align:start position:0% progress report and then I decided 00:00:27.290 --> 00:00:28.930 align:start position:0% progress report and then I decided yesterday<00:00:27.770> that<00:00:27.980> more<00:00:28.220> kind<00:00:28.520> of<00:00:28.580> a<00:00:28.640> Kay<00:00:28.760> by 00:00:28.930 --> 00:00:28.940 align:start position:0% yesterday that more kind of a Kay by 00:00:28.940 --> 00:00:31.210 align:start position:0% yesterday that more kind of a Kay by example<00:00:29.360> approach<00:00:29.600> would<00:00:29.810> go<00:00:29.990> better<00:00:30.800> here<00:00:31.070> so 00:00:31.210 --> 00:00:31.220 align:start position:0% example approach would go better here so 00:00:31.220 --> 00:00:33.100 align:start position:0% example approach would go better here so I<00:00:31.280> figured<00:00:31.640> I'll<00:00:32.329> put<00:00:32.539> that<00:00:32.629> as<00:00:32.780> a<00:00:32.809> subtitle 00:00:33.100 --> 00:00:33.110 align:start position:0% I figured I'll put that as a subtitle 00:00:33.110 --> 00:00:34.900 align:start position:0% I figured I'll put that as a subtitle but<00:00:33.680> still<00:00:33.890> leave<00:00:34.010> the<00:00:34.040> original<00:00:34.430> ones<00:00:34.579> so<00:00:34.850> I 00:00:34.900 --> 00:00:34.910 align:start position:0% but still leave the original ones so I 00:00:34.910 --> 00:00:36.340 align:start position:0% but still leave the original ones so I don't<00:00:35.090> offend<00:00:35.210> anyone<00:00:35.690> or<00:00:35.720> something<00:00:36.140> so 00:00:36.340 --> 00:00:36.350 align:start position:0% don't offend anyone or something so 00:00:36.350 --> 00:00:39.970 align:start position:0% don't offend anyone or something so we'll<00:00:36.680> see<00:00:37.390> okay<00:00:38.390> so<00:00:38.450> what<00:00:38.900> is<00:00:39.020> K<00:00:39.260> K<00:00:39.680> is<00:00:39.829> this 00:00:39.970 --> 00:00:39.980 align:start position:0% we'll see okay so what is K K is this 00:00:39.980 --> 00:00:41.380 align:start position:0% we'll see okay so what is K K is this language<00:00:40.370> for<00:00:40.760> building<00:00:40.880> programming 00:00:41.380 --> 00:00:41.390 align:start position:0% language for building programming 00:00:41.390 --> 00:00:42.790 align:start position:0% language for building programming languages<00:00:41.750> in<00:00:41.900> and<00:00:42.079> then<00:00:42.230> you<00:00:42.350> get<00:00:42.440> to<00:00:42.560> derive 00:00:42.790 --> 00:00:42.800 align:start position:0% languages in and then you get to derive 00:00:42.800 --> 00:00:44.710 align:start position:0% languages in and then you get to derive a<00:00:42.829> bunch<00:00:43.070> of<00:00:43.130> tools<00:00:43.310> from<00:00:43.520> it<00:00:43.670> so<00:00:44.000> essentially 00:00:44.710 --> 00:00:44.720 align:start position:0% a bunch of tools from it so essentially 00:00:44.720 --> 00:00:46.360 align:start position:0% a bunch of tools from it so essentially you<00:00:45.140> give<00:00:45.410> us<00:00:45.530> the<00:00:45.710> formal<00:00:46.070> language 00:00:46.360 --> 00:00:46.370 align:start position:0% you give us the formal language 00:00:46.370 --> 00:00:49.150 align:start position:0% you give us the formal language definition<00:00:46.940> syntax<00:00:47.420> and<00:00:47.630> semantics<00:00:48.110> and<00:00:49.010> then 00:00:49.150 --> 00:00:49.160 align:start position:0% definition syntax and semantics and then 00:00:49.160 --> 00:00:50.590 align:start position:0% definition syntax and semantics and then we<00:00:49.250> derive<00:00:49.489> a<00:00:49.520> bunch<00:00:49.760> of<00:00:49.880> tools<00:00:50.030> for<00:00:50.270> me<00:00:50.360> so 00:00:50.590 --> 00:00:50.600 align:start position:0% we derive a bunch of tools for me so 00:00:50.600 --> 00:00:53.170 align:start position:0% we derive a bunch of tools for me so ones<00:00:50.840> that<00:00:51.140> are<00:00:51.470> more<00:00:52.070> in<00:00:52.430> the<00:00:52.640> vision<00:00:52.970> phase 00:00:53.170 --> 00:00:53.180 align:start position:0% ones that are more in the vision phase 00:00:53.180 --> 00:00:55.150 align:start position:0% ones that are more in the vision phase right<00:00:53.450> now<00:00:53.510> our<00:00:53.870> test<00:00:54.140> case<00:00:54.320> generation<00:00:54.739> and 00:00:55.150 --> 00:00:55.160 align:start position:0% right now our test case generation and 00:00:55.160 --> 00:00:57.130 align:start position:0% right now our test case generation and compiler<00:00:55.670> but<00:00:56.180> all<00:00:56.329> of<00:00:56.450> the<00:00:56.540> other<00:00:56.690> tools<00:00:56.960> you 00:00:57.130 --> 00:00:57.140 align:start position:0% compiler but all of the other tools you 00:00:57.140 --> 00:00:58.690 align:start position:0% compiler but all of the other tools you see<00:00:57.320> here<00:00:57.590> we<00:00:57.770> actually<00:00:58.070> derived<00:00:58.370> from<00:00:58.520> the 00:00:58.690 --> 00:00:58.700 align:start position:0% see here we actually derived from the 00:00:58.700 --> 00:01:00.490 align:start position:0% see here we actually derived from the one<00:00:58.820> semantics<00:00:59.390> so<00:00:59.870> that<00:00:59.989> means<00:01:00.200> that<00:01:00.380> the 00:01:00.490 --> 00:01:00.500 align:start position:0% one semantics so that means that the 00:01:00.500 --> 00:01:01.540 align:start position:0% one semantics so that means that the tool<00:01:00.680> that<00:01:00.829> you're<00:01:00.920> doing<00:01:01.130> symbolic 00:01:01.540 --> 00:01:01.550 align:start position:0% tool that you're doing symbolic 00:01:01.550 --> 00:01:03.790 align:start position:0% tool that you're doing symbolic execution<00:01:01.670> with<00:01:02.239> or<00:01:02.510> model<00:01:03.079> checking<00:01:03.410> with<00:01:03.559> or 00:01:03.790 --> 00:01:03.800 align:start position:0% execution with or model checking with or 00:01:03.800 --> 00:01:05.770 align:start position:0% execution with or model checking with or deductive<00:01:04.280> program<00:01:04.579> verification<00:01:04.759> or<00:01:05.449> you're 00:01:05.770 --> 00:01:05.780 align:start position:0% deductive program verification or you're 00:01:05.780 --> 00:01:09.070 align:start position:0% deductive program verification or you're executing<00:01:06.320> the<00:01:06.590> test<00:01:06.799> set<00:01:06.950> with<00:01:07.450> use<00:01:08.450> all<00:01:08.750> the 00:01:09.070 --> 00:01:09.080 align:start position:0% executing the test set with use all the 00:01:09.080 --> 00:01:10.180 align:start position:0% executing the test set with use all the same<00:01:09.229> semantics<00:01:09.770> there's<00:01:09.920> only<00:01:10.010> one 00:01:10.180 --> 00:01:10.190 align:start position:0% same semantics there's only one 00:01:10.190 --> 00:01:12.310 align:start position:0% same semantics there's only one semantics<00:01:10.670> that<00:01:10.760> all<00:01:11.659> of<00:01:11.750> them<00:01:11.870> are<00:01:11.960> using<00:01:12.260> if 00:01:12.310 --> 00:01:12.320 align:start position:0% semantics that all of them are using if 00:01:12.320 --> 00:01:13.719 align:start position:0% semantics that all of them are using if there's<00:01:12.470> no<00:01:12.620> way<00:01:12.740> for<00:01:12.770> them<00:01:13.010> to<00:01:13.040> disagree<00:01:13.520> on 00:01:13.719 --> 00:01:13.729 align:start position:0% there's no way for them to disagree on 00:01:13.729 --> 00:01:16.300 align:start position:0% there's no way for them to disagree on how<00:01:14.120> the<00:01:14.180> execution<00:01:14.720> happens<00:01:15.280> which<00:01:16.280> is 00:01:16.300 --> 00:01:16.310 align:start position:0% how the execution happens which is 00:01:16.310 --> 00:01:17.560 align:start position:0% how the execution happens which is important<00:01:16.790> when<00:01:16.909> you're<00:01:17.030> trying<00:01:17.090> to<00:01:17.240> verify 00:01:17.560 --> 00:01:17.570 align:start position:0% important when you're trying to verify 00:01:17.570 --> 00:01:18.609 align:start position:0% important when you're trying to verify the<00:01:17.630> program's<00:01:18.020> have<00:01:18.140> the<00:01:18.200> properties<00:01:18.590> you 00:01:18.609 --> 00:01:18.619 align:start position:0% the program's have the properties you 00:01:18.619 --> 00:01:21.550 align:start position:0% the program's have the properties you think<00:01:18.890> they<00:01:18.979> have<00:01:19.570> the<00:01:20.570> Kay<00:01:20.750> backend<00:01:21.200> I'm<00:01:21.409> not 00:01:21.550 --> 00:01:21.560 align:start position:0% think they have the Kay backend I'm not 00:01:21.560 --> 00:01:22.870 align:start position:0% think they have the Kay backend I'm not really<00:01:21.680> gonna<00:01:21.830> go<00:01:22.010> into<00:01:22.159> much<00:01:22.310> depth<00:01:22.580> on<00:01:22.729> this 00:01:22.870 --> 00:01:22.880 align:start position:0% really gonna go into much depth on this 00:01:22.880 --> 00:01:24.760 align:start position:0% really gonna go into much depth on this but<00:01:23.180> the<00:01:23.330> static<00:01:23.659> logic<00:01:23.990> we<00:01:24.080> use<00:01:24.260> for<00:01:24.500> matching 00:01:24.760 --> 00:01:24.770 align:start position:0% but the static logic we use for matching 00:01:24.770 --> 00:01:25.750 align:start position:0% but the static logic we use for matching configurations 00:01:25.750 --> 00:01:25.760 align:start position:0% configurations 00:01:25.760 --> 00:01:28.810 align:start position:0% configurations it's<00:01:26.299> called<00:01:26.450> matching<00:01:26.659> logic<00:01:27.610> there's<00:01:28.610> some 00:01:28.810 --> 00:01:28.820 align:start position:0% it's called matching logic there's some 00:01:28.820 --> 00:01:30.310 align:start position:0% it's called matching logic there's some ongoing<00:01:29.000> work<00:01:29.420> on<00:01:29.600> showing<00:01:29.840> that<00:01:30.020> this<00:01:30.170> is<00:01:30.290> a 00:01:30.310 --> 00:01:30.320 align:start position:0% ongoing work on showing that this is a 00:01:30.320 --> 00:01:32.020 align:start position:0% ongoing work on showing that this is a generalization<00:01:30.740> of<00:01:31.070> separation<00:01:31.580> logic<00:01:31.909> and 00:01:32.020 --> 00:01:32.030 align:start position:0% generalization of separation logic and 00:01:32.030 --> 00:01:33.280 align:start position:0% generalization of separation logic and the<00:01:32.090> poly<00:01:32.270> otic<00:01:32.510> modal<00:01:32.780> logics<00:01:33.140> and 00:01:33.280 --> 00:01:33.290 align:start position:0% the poly otic modal logics and 00:01:33.290 --> 00:01:35.380 align:start position:0% the poly otic modal logics and first-order<00:01:34.250> logic<00:01:34.400> as<00:01:34.670> well<00:01:34.700> and<00:01:35.060> stuff<00:01:35.240> like 00:01:35.380 --> 00:01:35.390 align:start position:0% first-order logic as well and stuff like 00:01:35.390 --> 00:01:36.850 align:start position:0% first-order logic as well and stuff like that<00:01:35.570> so<00:01:35.840> well<00:01:36.409> and<00:01:36.560> when<00:01:36.680> I<00:01:36.710> say 00:01:36.850 --> 00:01:36.860 align:start position:0% that so well and when I say 00:01:36.860 --> 00:01:38.170 align:start position:0% that so well and when I say generalization<00:01:37.460> I<00:01:37.549> really<00:01:37.760> just<00:01:37.909> mean<00:01:38.030> like 00:01:38.170 --> 00:01:38.180 align:start position:0% generalization I really just mean like 00:01:38.180 --> 00:01:41.140 align:start position:0% generalization I really just mean like there's<00:01:38.390> embeddings<00:01:38.990> into<00:01:39.320> it<00:01:39.439> and<00:01:40.250> then<00:01:40.790> also 00:01:41.140 --> 00:01:41.150 align:start position:0% there's embeddings into it and then also 00:01:41.150 --> 00:01:43.000 align:start position:0% there's embeddings into it and then also the<00:01:41.450> dynamic<00:01:41.810> logic<00:01:42.110> is<00:01:42.200> reach<00:01:42.350> ability<00:01:42.530> logic 00:01:43.000 --> 00:01:43.010 align:start position:0% the dynamic logic is reach ability logic 00:01:43.010 --> 00:01:44.050 align:start position:0% the dynamic logic is reach ability logic which<00:01:43.159> is<00:01:43.280> this<00:01:43.400> language<00:01:43.820> independent 00:01:44.050 --> 00:01:44.060 align:start position:0% which is this language independent 00:01:44.060 --> 00:01:45.820 align:start position:0% which is this language independent dynamic<00:01:44.869> logic<00:01:45.229> for<00:01:45.439> reasoning<00:01:45.799> about 00:01:45.820 --> 00:01:45.830 align:start position:0% dynamic logic for reasoning about 00:01:45.830 --> 00:01:47.980 align:start position:0% dynamic logic for reasoning about transition<00:01:46.430> systems<00:01:46.790> so<00:01:47.420> go<00:01:47.600> ahead<00:01:47.689> and<00:01:47.780> ask 00:01:47.980 --> 00:01:47.990 align:start position:0% transition systems so go ahead and ask 00:01:47.990 --> 00:01:49.929 align:start position:0% transition systems so go ahead and ask me<00:01:48.140> or<00:01:48.530> the<00:01:48.650> other<00:01:48.680> team<00:01:49.070> members<00:01:49.100> you<00:01:49.790> guys 00:01:49.929 --> 00:01:49.939 align:start position:0% me or the other team members you guys 00:01:49.939 --> 00:01:52.300 align:start position:0% me or the other team members you guys raise<00:01:50.119> your<00:01:50.240> hands<00:01:50.390> if<00:01:51.009> you<00:01:52.009> have<00:01:52.159> any 00:01:52.300 --> 00:01:52.310 align:start position:0% raise your hands if you have any 00:01:52.310 --> 00:01:53.770 align:start position:0% raise your hands if you have any questions<00:01:52.700> about<00:01:52.820> these<00:01:53.030> specific<00:01:53.330> things 00:01:53.770 --> 00:01:53.780 align:start position:0% questions about these specific things 00:01:53.780 --> 00:01:55.240 align:start position:0% questions about these specific things but<00:01:54.470> I'm<00:01:54.560> not<00:01:54.650> really<00:01:54.770> going<00:01:54.920> to<00:01:55.009> talk<00:01:55.130> about 00:01:55.240 --> 00:01:55.250 align:start position:0% but I'm not really going to talk about 00:01:55.250 --> 00:01:58.179 align:start position:0% but I'm not really going to talk about that<00:01:55.520> in<00:01:55.640> this<00:01:55.850> presentation<00:01:56.890> instead<00:01:57.890> what 00:01:58.179 --> 00:01:58.189 align:start position:0% that in this presentation instead what 00:01:58.189 --> 00:01:59.560 align:start position:0% that in this presentation instead what I'm<00:01:58.250> going<00:01:58.280> to<00:01:58.430> focus<00:01:58.549> on<00:01:58.820> is<00:01:59.060> this<00:01:59.240> K<00:01:59.420> by 00:01:59.560 --> 00:01:59.570 align:start position:0% I'm going to focus on is this K by 00:01:59.570 --> 00:02:02.679 align:start position:0% I'm going to focus on is this K by example<00:01:59.990> thing<00:02:00.310> so<00:02:01.310> the<00:02:01.790> organization<00:02:02.420> we 00:02:02.679 --> 00:02:02.689 align:start position:0% example thing so the organization we 00:02:02.689 --> 00:02:03.940 align:start position:0% example thing so the organization we have<00:02:02.810> on<00:02:02.900> github<00:02:03.200> is<00:02:03.290> this<00:02:03.409> K<00:02:03.560> framework 00:02:03.940 --> 00:02:03.950 align:start position:0% have on github is this K framework 00:02:03.950 --> 00:02:05.950 align:start position:0% have on github is this K framework organization<00:02:04.549> for<00:02:04.729> the<00:02:04.790> KVM<00:02:05.210> repository<00:02:05.810> is<00:02:05.930> a 00:02:05.950 --> 00:02:05.960 align:start position:0% organization for the KVM repository is a 00:02:05.960 --> 00:02:08.710 align:start position:0% organization for the KVM repository is a TDM<00:02:06.320> semantics<00:02:06.799> and<00:02:07.009> all<00:02:07.759> of<00:02:07.909> the<00:02:08.060> semantics 00:02:08.710 --> 00:02:08.720 align:start position:0% TDM semantics and all of the semantics 00:02:08.720 --> 00:02:10.059 align:start position:0% TDM semantics and all of the semantics that<00:02:08.750> we<00:02:08.869> maintain<00:02:09.200> are<00:02:09.590> developed<00:02:09.920> there 00:02:10.059 --> 00:02:10.069 align:start position:0% that we maintain are developed there 00:02:10.069 --> 00:02:11.170 align:start position:0% that we maintain are developed there there<00:02:10.250> are<00:02:10.369> some<00:02:10.550> semantics<00:02:10.970> that<00:02:11.060> other 00:02:11.170 --> 00:02:11.180 align:start position:0% there are some semantics that other 00:02:11.180 --> 00:02:13.410 align:start position:0% there are some semantics that other people<00:02:11.480> maintain<00:02:11.870> that<00:02:12.200> aren't<00:02:12.950> within<00:02:13.099> our 00:02:13.410 --> 00:02:13.420 align:start position:0% people maintain that aren't within our 00:02:13.420 --> 00:02:16.500 align:start position:0% people maintain that aren't within our kind<00:02:13.599> of<00:02:13.720> organization<00:02:14.650> and<00:02:15.400> then<00:02:16.120> directly 00:02:16.500 --> 00:02:16.510 align:start position:0% kind of organization and then directly 00:02:16.510 --> 00:02:18.600 align:start position:0% kind of organization and then directly in<00:02:16.599> this<00:02:16.750> repository<00:02:16.990> we<00:02:17.680> have<00:02:17.860> this 00:02:18.600 --> 00:02:18.610 align:start position:0% in this repository we have this 00:02:18.610 --> 00:02:20.309 align:start position:0% in this repository we have this directory<00:02:19.510> which<00:02:19.630> has<00:02:19.660> a<00:02:19.810> bunch<00:02:20.050> of<00:02:20.110> toy 00:02:20.309 --> 00:02:20.319 align:start position:0% directory which has a bunch of toy 00:02:20.319 --> 00:02:21.839 align:start position:0% directory which has a bunch of toy languages<00:02:20.860> you<00:02:20.980> can<00:02:21.099> kind<00:02:21.310> of<00:02:21.340> play<00:02:21.459> with<00:02:21.550> and 00:02:21.839 --> 00:02:21.849 align:start position:0% languages you can kind of play with and 00:02:21.849 --> 00:02:23.550 align:start position:0% languages you can kind of play with and get<00:02:21.940> familiar<00:02:22.090> with<00:02:22.300> k<00:02:22.569> so<00:02:23.290> that's<00:02:23.349> a<00:02:23.440> good 00:02:23.550 --> 00:02:23.560 align:start position:0% get familiar with k so that's a good 00:02:23.560 --> 00:02:28.199 align:start position:0% get familiar with k so that's a good place<00:02:23.709> to<00:02:23.739> start<00:02:25.260> okay<00:02:26.260> so<00:02:27.010> I'm<00:02:27.880> gonna<00:02:28.000> dive 00:02:28.199 --> 00:02:28.209 align:start position:0% place to start okay so I'm gonna dive 00:02:28.209 --> 00:02:29.940 align:start position:0% place to start okay so I'm gonna dive right<00:02:28.239> in<00:02:28.599> and<00:02:28.750> basically<00:02:29.110> this<00:02:29.590> part<00:02:29.830> of<00:02:29.890> the 00:02:29.940 --> 00:02:29.950 align:start position:0% right in and basically this part of the 00:02:29.950 --> 00:02:31.140 align:start position:0% right in and basically this part of the presentation<00:02:30.040> is<00:02:30.489> just<00:02:30.520> gonna<00:02:30.730> be<00:02:30.880> a<00:02:30.910> bunch<00:02:31.060> of 00:02:31.140 --> 00:02:31.150 align:start position:0% presentation is just gonna be a bunch of 00:02:31.150 --> 00:02:33.000 align:start position:0% presentation is just gonna be a bunch of K<00:02:31.330> so<00:02:31.690> I'm<00:02:31.989> gonna<00:02:32.080> try<00:02:32.290> to<00:02:32.319> teach<00:02:32.530> you<00:02:32.560> guys<00:02:32.680> K 00:02:33.000 --> 00:02:33.010 align:start position:0% K so I'm gonna try to teach you guys K 00:02:33.010 --> 00:02:35.220 align:start position:0% K so I'm gonna try to teach you guys K using<00:02:33.970> an<00:02:34.360> example<00:02:34.720> that<00:02:34.810> hopefully<00:02:35.200> people 00:02:35.220 --> 00:02:35.230 align:start position:0% using an example that hopefully people 00:02:35.230 --> 00:02:37.860 align:start position:0% using an example that hopefully people are<00:02:35.709> familiar<00:02:35.830> with<00:02:36.160> which<00:02:36.520> is<00:02:36.730> EBM<00:02:37.120> so<00:02:37.780> we're 00:02:37.860 --> 00:02:37.870 align:start position:0% are familiar with which is EBM so we're 00:02:37.870 --> 00:02:40.350 align:start position:0% are familiar with which is EBM so we're gonna<00:02:37.989> start<00:02:38.260> off<00:02:38.410> with<00:02:38.440> some<00:02:38.650> basic<00:02:39.300> kind<00:02:40.300> of 00:02:40.350 --> 00:02:40.360 align:start position:0% gonna start off with some basic kind of 00:02:40.360 --> 00:02:43.920 align:start position:0% gonna start off with some basic kind of functional<00:02:40.780> style<00:02:41.110> rules<00:02:41.500> in<00:02:41.830> k<00:02:42.660> here<00:02:43.660> we're 00:02:43.920 --> 00:02:43.930 align:start position:0% functional style rules in k here we're 00:02:43.930 --> 00:02:45.809 align:start position:0% functional style rules in k here we're declaring<00:02:44.110> a<00:02:44.349> function<00:02:44.380> called<00:02:44.920> chop<00:02:45.220> it 00:02:45.809 --> 00:02:45.819 align:start position:0% declaring a function called chop it 00:02:45.819 --> 00:02:47.550 align:start position:0% declaring a function called chop it takes<00:02:46.090> in<00:02:46.239> an<00:02:46.330> integer<00:02:46.540> it<00:02:46.959> produces<00:02:47.440> an 00:02:47.550 --> 00:02:47.560 align:start position:0% takes in an integer it produces an 00:02:47.560 --> 00:02:49.470 align:start position:0% takes in an integer it produces an integer<00:02:47.800> so<00:02:48.069> the<00:02:48.190> type<00:02:48.640> signature<00:02:49.120> of<00:02:49.209> this<00:02:49.300> is 00:02:49.470 --> 00:02:49.480 align:start position:0% integer so the type signature of this is 00:02:49.480 --> 00:02:51.600 align:start position:0% integer so the type signature of this is int<00:02:49.720> int<00:02:50.019> we<00:02:50.739> declare<00:02:51.100> here<00:02:51.280> that<00:02:51.430> it's<00:02:51.549> a 00:02:51.600 --> 00:02:51.610 align:start position:0% int int we declare here that it's a 00:02:51.610 --> 00:02:53.340 align:start position:0% int int we declare here that it's a function<00:02:52.000> and<00:02:52.209> then<00:02:52.360> we<00:02:52.420> give<00:02:52.569> the<00:02:52.720> rule<00:02:52.989> we 00:02:53.340 --> 00:02:53.350 align:start position:0% function and then we give the rule we 00:02:53.350 --> 00:02:54.720 align:start position:0% function and then we give the rule we give<00:02:53.500> it<00:02:53.590> semantics<00:02:54.100> using<00:02:54.370> this<00:02:54.459> rule 00:02:54.720 --> 00:02:54.730 align:start position:0% give it semantics using this rule 00:02:54.730 --> 00:02:57.360 align:start position:0% give it semantics using this rule keyword<00:02:55.150> so<00:02:55.630> we<00:02:55.720> say<00:02:55.840> rule<00:02:56.170> chop<00:02:56.890> of<00:02:57.130> some 00:02:57.360 --> 00:02:57.370 align:start position:0% keyword so we say rule chop of some 00:02:57.370 --> 00:03:00.090 align:start position:0% keyword so we say rule chop of some integer<00:02:57.790> goes<00:02:58.330> to<00:02:58.510> the<00:02:58.600> integer<00:02:58.840> modulo<00:02:59.200> POW 00:03:00.090 --> 00:03:00.100 align:start position:0% integer goes to the integer modulo POW 00:03:00.100 --> 00:03:02.220 align:start position:0% integer goes to the integer modulo POW 256<00:03:00.790> where<00:03:00.940> this<00:03:01.030> is<00:03:01.180> the<00:03:01.269> built<00:03:01.450> in<00:03:01.630> K<00:03:01.840> modulus 00:03:02.220 --> 00:03:02.230 align:start position:0% 256 where this is the built in K modulus 00:03:02.230 --> 00:03:04.289 align:start position:0% 256 where this is the built in K modulus operator<00:03:02.410> and<00:03:02.950> that<00:03:02.980> only<00:03:03.549> happens<00:03:04.000> if<00:03:04.150> it's 00:03:04.289 --> 00:03:04.299 align:start position:0% operator and that only happens if it's 00:03:04.299 --> 00:03:06.270 align:start position:0% operator and that only happens if it's either<00:03:04.480> less<00:03:04.660> than<00:03:04.690> 0<00:03:05.140> or<00:03:05.380> greater<00:03:05.650> than<00:03:06.069> POW 00:03:06.270 --> 00:03:06.280 align:start position:0% either less than 0 or greater than POW 00:03:06.280 --> 00:03:09.570 align:start position:0% either less than 0 or greater than POW 256<00:03:06.970> which<00:03:07.120> is<00:03:07.269> 2<00:03:07.480> to<00:03:07.569> the<00:03:07.600> 256<00:03:08.340> otherwise<00:03:09.340> it 00:03:09.570 --> 00:03:09.580 align:start position:0% 256 which is 2 to the 256 otherwise it 00:03:09.580 --> 00:03:11.340 align:start position:0% 256 which is 2 to the 256 otherwise it just<00:03:09.610> goes<00:03:09.850> to<00:03:10.000> I<00:03:10.180> if<00:03:10.660> it's<00:03:10.900> within<00:03:11.049> those 00:03:11.340 --> 00:03:11.350 align:start position:0% just goes to I if it's within those 00:03:11.350 --> 00:03:12.930 align:start position:0% just goes to I if it's within those bounds<00:03:12.069> right<00:03:12.190> there<00:03:12.370> so<00:03:12.519> you<00:03:12.549> see<00:03:12.640> that<00:03:12.819> these 00:03:12.930 --> 00:03:12.940 align:start position:0% bounds right there so you see that these 00:03:12.940 --> 00:03:16.830 align:start position:0% bounds right there so you see that these cover<00:03:13.239> all<00:03:13.480> the<00:03:13.600> cases<00:03:15.269> some<00:03:16.269> other<00:03:16.420> operators 00:03:16.830 --> 00:03:16.840 align:start position:0% cover all the cases some other operators 00:03:16.840 --> 00:03:19.050 align:start position:0% cover all the cases some other operators we<00:03:16.959> define<00:03:17.260> these<00:03:17.829> are<00:03:17.950> just<00:03:18.100> a<00:03:18.370> fraction<00:03:18.760> of 00:03:19.050 --> 00:03:19.060 align:start position:0% we define these are just a fraction of 00:03:19.060 --> 00:03:21.810 align:start position:0% we define these are just a fraction of them<00:03:19.239> for<00:03:19.510> them<00:03:19.690> you<00:03:20.170> know<00:03:20.200> demonstrating<00:03:21.130> but 00:03:21.810 --> 00:03:21.820 align:start position:0% them for them you know demonstrating but 00:03:21.820 --> 00:03:23.009 align:start position:0% them for them you know demonstrating but for<00:03:21.970> example<00:03:22.269> there's<00:03:22.420> this<00:03:22.480> plus<00:03:22.780> word 00:03:23.009 --> 00:03:23.019 align:start position:0% for example there's this plus word 00:03:23.019 --> 00:03:25.229 align:start position:0% for example there's this plus word operator<00:03:23.530> and<00:03:23.739> notice<00:03:24.579> we<00:03:24.700> can<00:03:24.850> define<00:03:25.120> the 00:03:25.229 --> 00:03:25.239 align:start position:0% operator and notice we can define the 00:03:25.239 --> 00:03:26.910 align:start position:0% operator and notice we can define the syntax<00:03:25.450> right<00:03:25.870> here<00:03:26.079> to<00:03:26.230> be<00:03:26.320> in<00:03:26.500> fixed 00:03:26.910 --> 00:03:26.920 align:start position:0% syntax right here to be in fixed 00:03:26.920 --> 00:03:28.440 align:start position:0% syntax right here to be in fixed directly<00:03:27.160> so<00:03:27.609> we<00:03:27.640> can<00:03:27.760> say<00:03:28.030> actually 00:03:28.440 --> 00:03:28.450 align:start position:0% directly so we can say actually 00:03:28.450 --> 00:03:31.530 align:start position:0% directly so we can say actually something<00:03:28.720> like<00:03:28.870> 3<00:03:29.170> plus<00:03:29.380> word<00:03:29.709> 4<00:03:30.480> instead<00:03:31.480> of 00:03:31.530 --> 00:03:31.540 align:start position:0% something like 3 plus word 4 instead of 00:03:31.540 --> 00:03:33.720 align:start position:0% something like 3 plus word 4 instead of having<00:03:31.750> to<00:03:31.900> say<00:03:32.019> plus<00:03:32.260> word<00:03:32.470> of<00:03:32.739> 3<00:03:33.130> &<00:03:33.280> 4<00:03:33.430> for 00:03:33.720 --> 00:03:33.730 align:start position:0% having to say plus word of 3 & 4 for 00:03:33.730 --> 00:03:35.220 align:start position:0% having to say plus word of 3 & 4 for example<00:03:33.790> we<00:03:34.630> declare<00:03:34.870> that<00:03:34.900> that's<00:03:35.140> a 00:03:35.220 --> 00:03:35.230 align:start position:0% example we declare that that's a 00:03:35.230 --> 00:03:37.170 align:start position:0% example we declare that that's a function<00:03:35.620> and<00:03:35.799> then<00:03:36.190> we<00:03:36.280> give<00:03:36.400> semantics<00:03:36.850> to 00:03:37.170 --> 00:03:37.180 align:start position:0% function and then we give semantics to 00:03:37.180 --> 00:03:38.849 align:start position:0% function and then we give semantics to it<00:03:37.299> down<00:03:37.450> here<00:03:37.720> just<00:03:37.989> by<00:03:38.109> calling<00:03:38.320> the<00:03:38.650> built 00:03:38.849 --> 00:03:38.859 align:start position:0% it down here just by calling the built 00:03:38.859 --> 00:03:40.470 align:start position:0% it down here just by calling the built in<00:03:39.010> plus<00:03:39.280> int<00:03:39.519> operator<00:03:39.910> and<00:03:40.120> then<00:03:40.209> calling 00:03:40.470 --> 00:03:40.480 align:start position:0% in plus int operator and then calling 00:03:40.480 --> 00:03:42.630 align:start position:0% in plus int operator and then calling chopped<00:03:40.720> on<00:03:41.019> top<00:03:41.260> of<00:03:41.410> it<00:03:41.500> notice<00:03:42.220> we<00:03:42.310> also<00:03:42.430> give 00:03:42.630 --> 00:03:42.640 align:start position:0% chopped on top of it notice we also give 00:03:42.640 --> 00:03:44.250 align:start position:0% chopped on top of it notice we also give semantics<00:03:43.030> to<00:03:43.150> division<00:03:43.570> this<00:03:43.840> one<00:03:44.019> has<00:03:44.140> to<00:03:44.230> be 00:03:44.250 --> 00:03:44.260 align:start position:0% semantics to division this one has to be 00:03:44.260 --> 00:03:46.080 align:start position:0% semantics to division this one has to be broken<00:03:44.440> to<00:03:44.709> two<00:03:44.890> cases<00:03:45.070> where<00:03:45.519> you're 00:03:46.080 --> 00:03:46.090 align:start position:0% broken to two cases where you're 00:03:46.090 --> 00:03:47.729 align:start position:0% broken to two cases where you're dividing<00:03:46.269> by<00:03:46.510> 0<00:03:46.780> we're<00:03:47.140> an<00:03:47.230> EVM<00:03:47.560> that's 00:03:47.729 --> 00:03:47.739 align:start position:0% dividing by 0 we're an EVM that's 00:03:47.739 --> 00:03:49.949 align:start position:0% dividing by 0 we're an EVM that's defined<00:03:48.070> to<00:03:48.130> be<00:03:48.190> 0<00:03:48.480> and<00:03:49.480> where<00:03:49.720> you're<00:03:49.810> not 00:03:49.949 --> 00:03:49.959 align:start position:0% defined to be 0 and where you're not 00:03:49.959 --> 00:03:51.960 align:start position:0% defined to be 0 and where you're not dividing<00:03:50.320> by<00:03:50.410> 0<00:03:50.680> in<00:03:50.859> which<00:03:51.010> case<00:03:51.190> we<00:03:51.310> just<00:03:51.489> call 00:03:51.960 --> 00:03:51.970 align:start position:0% dividing by 0 in which case we just call 00:03:51.970 --> 00:03:55.380 align:start position:0% dividing by 0 in which case we just call chopped<00:03:52.180> on<00:03:52.359> the<00:03:52.450> normal<00:03:52.660> division<00:03:52.959> okay 00:03:55.380 --> 00:03:55.390 align:start position:0% chopped on the normal division okay 00:03:55.390 --> 00:03:57.059 align:start position:0% chopped on the normal division okay and<00:03:55.750> also<00:03:55.900> feel<00:03:56.170> free<00:03:56.319> to<00:03:56.350> ask<00:03:56.500> any<00:03:56.650> questions 00:03:57.059 --> 00:03:57.069 align:start position:0% and also feel free to ask any questions 00:03:57.069 --> 00:03:58.440 align:start position:0% and also feel free to ask any questions at<00:03:57.190> any<00:03:57.310> time<00:03:57.400> it's<00:03:57.640> gonna<00:03:57.730> kind<00:03:58.000> of<00:03:58.060> ramp<00:03:58.269> up 00:03:58.440 --> 00:03:58.450 align:start position:0% at any time it's gonna kind of ramp up 00:03:58.450 --> 00:03:59.940 align:start position:0% at any time it's gonna kind of ramp up in<00:03:58.600> difficulty<00:03:58.930> as<00:03:59.170> we<00:03:59.290> go<00:03:59.440> so<00:03:59.620> it's<00:03:59.709> better<00:03:59.859> to 00:03:59.940 --> 00:03:59.950 align:start position:0% in difficulty as we go so it's better to 00:03:59.950 --> 00:04:01.289 align:start position:0% in difficulty as we go so it's better to ask<00:04:00.579> earlier 00:04:01.289 --> 00:04:01.299 align:start position:0% ask earlier 00:04:01.299 --> 00:04:05.009 align:start position:0% ask earlier ok<00:04:01.989> so<00:04:02.049> defining<00:04:02.829> data<00:04:03.069> structures<00:04:03.489> in<00:04:03.609> K<00:04:04.019> this 00:04:05.009 --> 00:04:05.019 align:start position:0% ok so defining data structures in K this 00:04:05.019 --> 00:04:06.690 align:start position:0% ok so defining data structures in K this is<00:04:05.140> gonna<00:04:05.260> be<00:04:05.440> a<00:04:05.470> word<00:04:05.650> stack<00:04:05.950> for<00:04:06.130> evm<00:04:06.489> and 00:04:06.690 --> 00:04:06.700 align:start position:0% is gonna be a word stack for evm and 00:04:06.700 --> 00:04:08.130 align:start position:0% is gonna be a word stack for evm and we're<00:04:06.790> gonna<00:04:06.880> define<00:04:07.209> it<00:04:07.390> as<00:04:07.480> a<00:04:07.510> simple<00:04:07.959> cons 00:04:08.130 --> 00:04:08.140 align:start position:0% we're gonna define it as a simple cons 00:04:08.140 --> 00:04:10.379 align:start position:0% we're gonna define it as a simple cons list<00:04:08.440> so<00:04:08.650> anyone<00:04:08.890> in<00:04:09.220> the<00:04:10.030> functional 00:04:10.379 --> 00:04:10.389 align:start position:0% list so anyone in the functional 00:04:10.389 --> 00:04:11.640 align:start position:0% list so anyone in the functional programming<00:04:10.690> languages<00:04:11.079> will<00:04:11.260> recognize 00:04:11.640 --> 00:04:11.650 align:start position:0% programming languages will recognize 00:04:11.650 --> 00:04:14.759 align:start position:0% programming languages will recognize this<00:04:12.239> this<00:04:13.239> is<00:04:13.420> just<00:04:13.630> something<00:04:13.810> that<00:04:13.959> it's<00:04:14.620> a 00:04:14.759 --> 00:04:14.769 align:start position:0% this this is just something that it's a 00:04:14.769 --> 00:04:17.940 align:start position:0% this this is just something that it's a hint<00:04:14.950> or<00:04:15.100> at<00:04:15.280> SM<00:04:16.060> T<00:04:16.180> solver<00:04:16.539> but<00:04:17.320> basically<00:04:17.709> we 00:04:17.940 --> 00:04:17.950 align:start position:0% hint or at SM T solver but basically we 00:04:17.950 --> 00:04:19.560 align:start position:0% hint or at SM T solver but basically we say<00:04:18.160> that<00:04:18.400> we<00:04:18.489> have<00:04:18.519> this<00:04:18.760> dot<00:04:19.000> word<00:04:19.239> stack 00:04:19.560 --> 00:04:19.570 align:start position:0% say that we have this dot word stack 00:04:19.570 --> 00:04:21.690 align:start position:0% say that we have this dot word stack right<00:04:20.440> here<00:04:20.500> which<00:04:20.889> serves<00:04:21.160> as<00:04:21.310> the<00:04:21.400> empty 00:04:21.690 --> 00:04:21.700 align:start position:0% right here which serves as the empty 00:04:21.700 --> 00:04:23.010 align:start position:0% right here which serves as the empty element<00:04:22.090> of<00:04:22.150> the<00:04:22.240> cons<00:04:22.419> list<00:04:22.690> and<00:04:22.900> then<00:04:22.990> you 00:04:23.010 --> 00:04:23.020 align:start position:0% element of the cons list and then you 00:04:23.020 --> 00:04:25.409 align:start position:0% element of the cons list and then you can<00:04:23.110> also<00:04:23.349> cons<00:04:23.710> an<00:04:24.099> integer<00:04:24.669> onto<00:04:25.180> a<00:04:25.240> word 00:04:25.409 --> 00:04:25.419 align:start position:0% can also cons an integer onto a word 00:04:25.419 --> 00:04:27.180 align:start position:0% can also cons an integer onto a word stack<00:04:25.720> and<00:04:25.960> that<00:04:25.990> also<00:04:26.440> produces<00:04:26.860> a<00:04:26.890> word 00:04:27.180 --> 00:04:27.190 align:start position:0% stack and that also produces a word 00:04:27.190 --> 00:04:28.920 align:start position:0% stack and that also produces a word stack<00:04:27.370> so<00:04:28.180> this<00:04:28.300> can<00:04:28.450> be<00:04:28.540> thought<00:04:28.660> of<00:04:28.720> as<00:04:28.870> a 00:04:28.920 --> 00:04:28.930 align:start position:0% stack so this can be thought of as a 00:04:28.930 --> 00:04:31.470 align:start position:0% stack so this can be thought of as a singly<00:04:29.290> linked<00:04:29.560> list<00:04:29.770> and<00:04:30.060> then<00:04:31.060> here's<00:04:31.270> for 00:04:31.470 --> 00:04:31.480 align:start position:0% singly linked list and then here's for 00:04:31.480 --> 00:04:33.570 align:start position:0% singly linked list and then here's for example<00:04:31.510> word<00:04:31.960> stack<00:04:32.200> append<00:04:32.560> given<00:04:33.400> to<00:04:33.490> your 00:04:33.570 --> 00:04:33.580 align:start position:0% example word stack append given to your 00:04:33.580 --> 00:04:35.550 align:start position:0% example word stack append given to your word<00:04:33.700> stacks<00:04:34.030> you<00:04:34.300> can<00:04:34.810> put<00:04:35.050> plus<00:04:35.230> plus<00:04:35.440> in 00:04:35.550 --> 00:04:35.560 align:start position:0% word stacks you can put plus plus in 00:04:35.560 --> 00:04:36.930 align:start position:0% word stacks you can put plus plus in between<00:04:35.800> them<00:04:35.950> that<00:04:36.160> also<00:04:36.280> produces<00:04:36.550> a<00:04:36.760> word 00:04:36.930 --> 00:04:36.940 align:start position:0% between them that also produces a word 00:04:36.940 --> 00:04:38.790 align:start position:0% between them that also produces a word stack<00:04:37.240> and<00:04:37.540> then<00:04:38.020> you<00:04:38.110> know<00:04:38.200> dot<00:04:38.380> word<00:04:38.530> stack 00:04:38.790 --> 00:04:38.800 align:start position:0% stack and then you know dot word stack 00:04:38.800 --> 00:04:40.440 align:start position:0% stack and then you know dot word stack append<00:04:39.220> some<00:04:39.520> word<00:04:39.670> stack<00:04:39.940> is<00:04:40.090> just<00:04:40.240> the<00:04:40.330> word 00:04:40.440 --> 00:04:40.450 align:start position:0% append some word stack is just the word 00:04:40.450 --> 00:04:42.750 align:start position:0% append some word stack is just the word stack<00:04:40.720> and<00:04:40.960> then<00:04:41.410> some<00:04:42.010> word<00:04:42.190> appended<00:04:42.640> to<00:04:42.670> a 00:04:42.750 --> 00:04:42.760 align:start position:0% stack and then some word appended to a 00:04:42.760 --> 00:04:45.180 align:start position:0% stack and then some word appended to a cons<00:04:43.420> down<00:04:43.660> to<00:04:43.750> a<00:04:43.810> word<00:04:43.930> stack<00:04:44.230> append<00:04:45.010> a<00:04:45.070> word 00:04:45.180 --> 00:04:45.190 align:start position:0% cons down to a word stack append a word 00:04:45.190 --> 00:04:47.490 align:start position:0% cons down to a word stack append a word stack<00:04:45.460> is<00:04:45.670> the<00:04:45.760> word<00:04:45.940> cons<00:04:46.330> down<00:04:46.540> to<00:04:46.780> depending 00:04:47.490 --> 00:04:47.500 align:start position:0% stack is the word cons down to depending 00:04:47.500 --> 00:04:50.940 align:start position:0% stack is the word cons down to depending of<00:04:47.590> the<00:04:47.680> tails<00:04:47.860> okay<00:04:48.670> pretty<00:04:49.770> pretty<00:04:50.770> simple 00:04:50.940 --> 00:04:50.950 align:start position:0% of the tails okay pretty pretty simple 00:04:50.950 --> 00:04:54.780 align:start position:0% of the tails okay pretty pretty simple functional<00:04:51.460> programming<00:04:51.850> like<00:04:52.150> stuff<00:04:53.190> ok<00:04:54.190> so 00:04:54.780 --> 00:04:54.790 align:start position:0% functional programming like stuff ok so 00:04:54.790 --> 00:04:56.220 align:start position:0% functional programming like stuff ok so then<00:04:54.940> in<00:04:55.180> K<00:04:55.360> we<00:04:55.510> have<00:04:55.660> this<00:04:55.780> thing<00:04:55.930> called<00:04:56.080> a 00:04:56.220 --> 00:04:56.230 align:start position:0% then in K we have this thing called a 00:04:56.230 --> 00:04:57.810 align:start position:0% then in K we have this thing called a configuration<00:04:56.830> which<00:04:56.980> basically<00:04:57.250> specifies 00:04:57.810 --> 00:04:57.820 align:start position:0% configuration which basically specifies 00:04:57.820 --> 00:05:00.140 align:start position:0% configuration which basically specifies the<00:04:58.000> state<00:04:58.240> of<00:04:58.390> our<00:04:58.450> system<00:04:58.840> and<00:04:59.020> that<00:04:59.590> lets<00:04:59.860> us 00:05:00.140 --> 00:05:00.150 align:start position:0% the state of our system and that lets us 00:05:00.150 --> 00:05:03.390 align:start position:0% the state of our system and that lets us kind<00:05:01.150> of<00:05:01.380> tell<00:05:02.380> Kay<00:05:02.620> that<00:05:02.920> you<00:05:03.070> know<00:05:03.160> there's<00:05:03.370> a 00:05:03.390 --> 00:05:03.400 align:start position:0% kind of tell Kay that you know there's a 00:05:03.400 --> 00:05:04.620 align:start position:0% kind of tell Kay that you know there's a bunch<00:05:03.520> of<00:05:03.640> state<00:05:03.880> sitting<00:05:04.150> around<00:05:04.330> that<00:05:04.510> we 00:05:04.620 --> 00:05:04.630 align:start position:0% bunch of state sitting around that we 00:05:04.630 --> 00:05:05.850 align:start position:0% bunch of state sitting around that we don't<00:05:04.780> have<00:05:04.930> to<00:05:05.050> want<00:05:05.290> to<00:05:05.350> have<00:05:05.440> to<00:05:05.560> mention 00:05:05.850 --> 00:05:05.860 align:start position:0% don't have to want to have to mention 00:05:05.860 --> 00:05:06.960 align:start position:0% don't have to want to have to mention all<00:05:05.950> the<00:05:06.070> time<00:05:06.250> but<00:05:06.370> we<00:05:06.490> want<00:05:06.670> to<00:05:06.730> be<00:05:06.790> able<00:05:06.850> to 00:05:06.960 --> 00:05:06.970 align:start position:0% all the time but we want to be able to 00:05:06.970 --> 00:05:08.720 align:start position:0% all the time but we want to be able to grab<00:05:07.150> it<00:05:07.270> anytime<00:05:07.480> we<00:05:07.720> do<00:05:07.840> need<00:05:07.990> to<00:05:08.080> mention<00:05:08.230> it 00:05:08.720 --> 00:05:08.730 align:start position:0% grab it anytime we do need to mention it 00:05:08.730 --> 00:05:10.980 align:start position:0% grab it anytime we do need to mention it so<00:05:09.730> here's<00:05:10.180> just<00:05:10.240> a<00:05:10.480> fragment<00:05:10.690> of<00:05:10.930> the 00:05:10.980 --> 00:05:10.990 align:start position:0% so here's just a fragment of the 00:05:10.990 --> 00:05:12.240 align:start position:0% so here's just a fragment of the configuration<00:05:11.620> the<00:05:11.740> actual<00:05:12.010> configuration 00:05:12.240 --> 00:05:12.250 align:start position:0% configuration the actual configuration 00:05:12.250 --> 00:05:15.570 align:start position:0% configuration the actual configuration contains<00:05:12.940> 60<00:05:13.450> plus<00:05:13.660> cells<00:05:13.960> a<00:05:14.260> cell<00:05:14.620> is<00:05:15.250> one<00:05:15.460> of 00:05:15.570 --> 00:05:15.580 align:start position:0% contains 60 plus cells a cell is one of 00:05:15.580 --> 00:05:19.530 align:start position:0% contains 60 plus cells a cell is one of these<00:05:15.700> XML<00:05:16.330> like<00:05:16.630> brackets<00:05:17.320> like<00:05:18.310> this<00:05:18.540> and 00:05:19.530 --> 00:05:19.540 align:start position:0% these XML like brackets like this and 00:05:19.540 --> 00:05:21.150 align:start position:0% these XML like brackets like this and then<00:05:19.720> in<00:05:20.080> the<00:05:20.320> semantics<00:05:20.800> when<00:05:20.980> we<00:05:21.040> say 00:05:21.150 --> 00:05:21.160 align:start position:0% then in the semantics when we say 00:05:21.160 --> 00:05:22.950 align:start position:0% then in the semantics when we say configuration<00:05:21.820> you<00:05:21.970> also<00:05:22.120> supply<00:05:22.510> kind<00:05:22.870> of 00:05:22.950 --> 00:05:22.960 align:start position:0% configuration you also supply kind of 00:05:22.960 --> 00:05:24.780 align:start position:0% configuration you also supply kind of the<00:05:23.050> default<00:05:23.230> value<00:05:23.920> of<00:05:24.100> each<00:05:24.370> of<00:05:24.490> the<00:05:24.580> cells 00:05:24.780 --> 00:05:24.790 align:start position:0% the default value of each of the cells 00:05:24.790 --> 00:05:27.120 align:start position:0% the default value of each of the cells so<00:05:25.390> this<00:05:25.540> is<00:05:25.690> telling<00:05:25.900> us<00:05:26.140> that<00:05:26.200> in<00:05:26.500> the<00:05:26.620> case<00:05:26.830> L 00:05:27.120 --> 00:05:27.130 align:start position:0% so this is telling us that in the case L 00:05:27.130 --> 00:05:29.580 align:start position:0% so this is telling us that in the case L the<00:05:27.580> entire<00:05:27.880> evm<00:05:28.330> program<00:05:28.780> is<00:05:29.020> loaded<00:05:29.410> that's 00:05:29.580 --> 00:05:29.590 align:start position:0% the entire evm program is loaded that's 00:05:29.590 --> 00:05:31.230 align:start position:0% the entire evm program is loaded that's what<00:05:29.710> this<00:05:29.770> dollar<00:05:30.010> sign<00:05:30.100> PGM<00:05:30.640> it's<00:05:30.820> a<00:05:30.880> special 00:05:31.230 --> 00:05:31.240 align:start position:0% what this dollar sign PGM it's a special 00:05:31.240 --> 00:05:33.840 align:start position:0% what this dollar sign PGM it's a special symbol<00:05:31.560> is<00:05:32.560> loaded<00:05:32.950> into<00:05:33.100> the<00:05:33.250> K<00:05:33.370> cell<00:05:33.640> at<00:05:33.790> the 00:05:33.840 --> 00:05:33.850 align:start position:0% symbol is loaded into the K cell at the 00:05:33.850 --> 00:05:36.450 align:start position:0% symbol is loaded into the K cell at the beginning<00:05:34.120> of<00:05:34.150> execution<00:05:34.750> and<00:05:35.620> then<00:05:36.250> there's 00:05:36.450 --> 00:05:36.460 align:start position:0% beginning of execution and then there's 00:05:36.460 --> 00:05:39.270 align:start position:0% beginning of execution and then there's a<00:05:36.550> sub<00:05:36.850> configuration<00:05:37.540> called<00:05:37.750> EVM<00:05:38.260> that<00:05:39.070> for 00:05:39.270 --> 00:05:39.280 align:start position:0% a sub configuration called EVM that for 00:05:39.280 --> 00:05:41.580 align:start position:0% a sub configuration called EVM that for example<00:05:39.460> contains<00:05:40.000> the<00:05:40.360> VM<00:05:40.660> execution<00:05:41.350> state 00:05:41.580 --> 00:05:41.590 align:start position:0% example contains the VM execution state 00:05:41.590 --> 00:05:43.590 align:start position:0% example contains the VM execution state so<00:05:41.800> for<00:05:41.919> examples<00:05:42.310> the<00:05:42.820> current<00:05:43.090> executing 00:05:43.590 --> 00:05:43.600 align:start position:0% so for examples the current executing 00:05:43.600 --> 00:05:45.510 align:start position:0% so for examples the current executing program<00:05:43.990> which<00:05:44.530> in<00:05:44.650> the<00:05:44.740> yellow<00:05:44.890> paper<00:05:45.160> is<00:05:45.340> I 00:05:45.510 --> 00:05:45.520 align:start position:0% program which in the yellow paper is I 00:05:45.520 --> 00:05:48.090 align:start position:0% program which in the yellow paper is I underbar<00:05:45.910> be<00:05:46.090> the<00:05:46.840> current<00:05:47.260> words<00:05:47.440> gap<00:05:47.740> which 00:05:48.090 --> 00:05:48.100 align:start position:0% underbar be the current words gap which 00:05:48.100 --> 00:05:50.760 align:start position:0% underbar be the current words gap which is<00:05:48.130> me<00:05:48.370> us<00:05:48.640> the<00:05:49.180> local<00:05:49.480> memory<00:05:49.630> mu<00:05:49.930> m<00:05:50.110> and<00:05:50.350> the 00:05:50.760 --> 00:05:50.770 align:start position:0% is me us the local memory mu m and the 00:05:50.770 --> 00:05:53.760 align:start position:0% is me us the local memory mu m and the current<00:05:51.010> gas<00:05:51.220> available<00:05:51.610> which<00:05:52.240> is<00:05:52.360> mu<00:05:52.480> g<00:05:52.770> okay 00:05:53.760 --> 00:05:53.770 align:start position:0% current gas available which is mu g okay 00:05:53.770 --> 00:05:56.070 align:start position:0% current gas available which is mu g okay we<00:05:54.430> don't<00:05:54.520> just<00:05:54.730> have<00:05:54.910> the<00:05:55.060> VM<00:05:55.360> execution 00:05:56.070 --> 00:05:56.080 align:start position:0% we don't just have the VM execution 00:05:56.080 --> 00:05:59.010 align:start position:0% we don't just have the VM execution state<00:05:56.320> we<00:05:56.500> also<00:05:56.680> have<00:05:57.070> the<00:05:57.550> network<00:05:58.000> state<00:05:58.480> so 00:05:59.010 --> 00:05:59.020 align:start position:0% state we also have the network state so 00:05:59.020 --> 00:06:00.900 align:start position:0% state we also have the network state so we<00:05:59.140> have<00:05:59.260> another<00:05:59.470> sub<00:05:59.770> configuration<00:06:00.490> so 00:06:00.900 --> 00:06:00.910 align:start position:0% we have another sub configuration so 00:06:00.910 --> 00:06:02.580 align:start position:0% we have another sub configuration so what<00:06:01.090> you<00:06:01.150> saw<00:06:01.300> above<00:06:01.570> is<00:06:01.930> where<00:06:02.110> this<00:06:02.230> dot<00:06:02.560> dot 00:06:02.580 --> 00:06:02.590 align:start position:0% what you saw above is where this dot dot 00:06:02.590 --> 00:06:05.340 align:start position:0% what you saw above is where this dot dot is<00:06:02.919> this<00:06:03.880> is<00:06:03.970> the<00:06:04.060> network<00:06:04.360> state<00:06:04.630> we<00:06:05.169> have<00:06:05.320> a 00:06:05.340 --> 00:06:05.350 align:start position:0% is this is the network state we have a 00:06:05.350 --> 00:06:07.140 align:start position:0% is this is the network state we have a map<00:06:05.620> of<00:06:05.650> the<00:06:05.860> active<00:06:06.280> accounts<00:06:06.669> essentially 00:06:07.140 --> 00:06:07.150 align:start position:0% map of the active accounts essentially 00:06:07.150 --> 00:06:08.909 align:start position:0% map of the active accounts essentially that<00:06:07.240> map<00:06:07.480> just<00:06:07.690> states<00:06:07.960> whether<00:06:08.230> it's<00:06:08.590> an 00:06:08.909 --> 00:06:08.919 align:start position:0% that map just states whether it's an 00:06:08.919 --> 00:06:11.070 align:start position:0% that map just states whether it's an empty<00:06:09.340> account<00:06:09.700> or<00:06:09.910> an<00:06:10.090> actual<00:06:10.390> non-existent 00:06:11.070 --> 00:06:11.080 align:start position:0% empty account or an actual non-existent 00:06:11.080 --> 00:06:14.490 align:start position:0% empty account or an actual non-existent account<00:06:11.460> and<00:06:12.810> then<00:06:13.810> notice<00:06:14.110> we<00:06:14.230> have<00:06:14.350> this 00:06:14.490 --> 00:06:14.500 align:start position:0% account and then notice we have this 00:06:14.500 --> 00:06:16.170 align:start position:0% account and then notice we have this accounts<00:06:14.980> cell<00:06:15.250> which<00:06:15.580> is<00:06:15.610> wrapping<00:06:16.090> this 00:06:16.170 --> 00:06:16.180 align:start position:0% accounts cell which is wrapping this 00:06:16.180 --> 00:06:18.450 align:start position:0% accounts cell which is wrapping this account<00:06:16.540> cell<00:06:16.840> which<00:06:17.440> has<00:06:17.470> multiplicity<00:06:18.010> star 00:06:18.450 --> 00:06:18.460 align:start position:0% account cell which has multiplicity star 00:06:18.460 --> 00:06:20.640 align:start position:0% account cell which has multiplicity star which<00:06:18.820> basically<00:06:19.090> says<00:06:19.419> you<00:06:20.050> know<00:06:20.169> you<00:06:20.500> can 00:06:20.640 --> 00:06:20.650 align:start position:0% which basically says you know you can 00:06:20.650 --> 00:06:22.470 align:start position:0% which basically says you know you can have<00:06:20.770> as<00:06:20.860> many<00:06:21.010> account<00:06:21.490> cells<00:06:21.820> as<00:06:22.060> you<00:06:22.090> want 00:06:22.470 --> 00:06:22.480 align:start position:0% have as many account cells as you want 00:06:22.480 --> 00:06:24.810 align:start position:0% have as many account cells as you want so<00:06:22.900> you<00:06:23.410> know<00:06:23.530> in<00:06:23.650> a<00:06:23.710> realistic<00:06:23.980> EVM<00:06:24.490> network 00:06:24.810 --> 00:06:24.820 align:start position:0% so you know in a realistic EVM network 00:06:24.820 --> 00:06:26.880 align:start position:0% so you know in a realistic EVM network you<00:06:24.970> can<00:06:25.090> have<00:06:25.270> many<00:06:25.900> account<00:06:26.230> cells<00:06:26.500> and<00:06:26.770> then 00:06:26.880 --> 00:06:26.890 align:start position:0% you can have many account cells and then 00:06:26.890 --> 00:06:28.800 align:start position:0% you can have many account cells and then in<00:06:27.040> each<00:06:27.160> account<00:06:27.460> you<00:06:27.700> have<00:06:27.730> an<00:06:28.180> account<00:06:28.600> ID 00:06:28.800 --> 00:06:28.810 align:start position:0% in each account you have an account ID 00:06:28.810 --> 00:06:30.870 align:start position:0% in each account you have an account ID the<00:06:29.140> balance<00:06:29.560> the<00:06:29.800> code<00:06:30.040> the<00:06:30.370> storage<00:06:30.730> and<00:06:30.820> the 00:06:30.870 --> 00:06:30.880 align:start position:0% the balance the code the storage and the 00:06:30.880 --> 00:06:32.400 align:start position:0% the balance the code the storage and the nonce<00:06:31.090> and<00:06:31.330> these<00:06:31.540> are<00:06:31.690> the<00:06:31.810> initial<00:06:32.110> values 00:06:32.400 --> 00:06:32.410 align:start position:0% nonce and these are the initial values 00:06:32.410 --> 00:06:35.190 align:start position:0% nonce and these are the initial values down<00:06:33.130> here<00:06:33.190> we<00:06:33.940> also<00:06:34.150> have<00:06:34.450> things<00:06:34.750> like<00:06:34.900> the 00:06:35.190 --> 00:06:35.200 align:start position:0% down here we also have things like the 00:06:35.200 --> 00:06:36.719 align:start position:0% down here we also have things like the transact<00:06:35.620> of<00:06:35.770> the<00:06:35.830> current<00:06:36.070> transaction<00:06:36.550> set 00:06:36.719 --> 00:06:36.729 align:start position:0% transact of the current transaction set 00:06:36.729 --> 00:06:38.580 align:start position:0% transact of the current transaction set and<00:06:36.880> a<00:06:36.910> couple<00:06:37.090> other<00:06:37.300> little<00:06:37.600> network<00:06:38.320> state 00:06:38.580 --> 00:06:38.590 align:start position:0% and a couple other little network state 00:06:38.590 --> 00:06:40.559 align:start position:0% and a couple other little network state things<00:06:38.860> for<00:06:39.400> instance<00:06:39.490> so 00:06:40.559 --> 00:06:40.569 align:start position:0% things for instance so 00:06:40.569 --> 00:06:41.579 align:start position:0% things for instance so like<00:06:40.629> I<00:06:40.719> said<00:06:40.899> the<00:06:41.050> actual<00:06:41.199> configuration 00:06:41.579 --> 00:06:41.589 align:start position:0% like I said the actual configuration 00:06:41.589 --> 00:06:43.769 align:start position:0% like I said the actual configuration contains<00:06:42.309> you<00:06:42.909> know<00:06:42.999> sixty<00:06:43.330> plus<00:06:43.449> cells 00:06:43.769 --> 00:06:43.779 align:start position:0% contains you know sixty plus cells 00:06:43.779 --> 00:06:45.239 align:start position:0% contains you know sixty plus cells obviously<00:06:44.409> I<00:06:44.469> can't<00:06:44.649> put<00:06:44.830> the<00:06:44.889> whole<00:06:45.009> thing 00:06:45.239 --> 00:06:45.249 align:start position:0% obviously I can't put the whole thing 00:06:45.249 --> 00:06:47.669 align:start position:0% obviously I can't put the whole thing here<00:06:45.569> and<00:06:46.569> then<00:06:46.839> another<00:06:47.020> thing<00:06:47.259> to<00:06:47.379> note<00:06:47.529> this 00:06:47.669 --> 00:06:47.679 align:start position:0% here and then another thing to note this 00:06:47.679 --> 00:06:49.320 align:start position:0% here and then another thing to note this multiplicity<00:06:48.099> star<00:06:48.490> here<00:06:48.729> people<00:06:48.999> have<00:06:49.119> asked 00:06:49.320 --> 00:06:49.330 align:start position:0% multiplicity star here people have asked 00:06:49.330 --> 00:06:50.730 align:start position:0% multiplicity star here people have asked me<00:06:49.449> about<00:06:49.539> you<00:06:49.929> know<00:06:50.289> how<00:06:50.409> can<00:06:50.589> you<00:06:50.649> do 00:06:50.730 --> 00:06:50.740 align:start position:0% me about you know how can you do 00:06:50.740 --> 00:06:52.439 align:start position:0% me about you know how can you do concurrency<00:06:51.369> or<00:06:51.399> parallelism<00:06:51.939> or<00:06:52.179> something 00:06:52.439 --> 00:06:52.449 align:start position:0% concurrency or parallelism or something 00:06:52.449 --> 00:06:54.089 align:start position:0% concurrency or parallelism or something like<00:06:52.539> that<00:06:52.599> that's<00:06:53.229> exactly<00:06:53.379> how<00:06:53.770> you<00:06:53.800> do<00:06:54.009> it 00:06:54.089 --> 00:06:54.099 align:start position:0% like that that's exactly how you do it 00:06:54.099 --> 00:06:55.529 align:start position:0% like that that's exactly how you do it you<00:06:54.189> essentially<00:06:54.490> do<00:06:54.639> a<00:06:54.669> multiplicity<00:06:55.089> star 00:06:55.529 --> 00:06:55.539 align:start position:0% you essentially do a multiplicity star 00:06:55.539 --> 00:06:57.719 align:start position:0% you essentially do a multiplicity star in<00:06:56.439> a<00:06:56.619> cell<00:06:56.860> that's<00:06:57.069> surrounding<00:06:57.490> the<00:06:57.580> case 00:06:57.719 --> 00:06:57.729 align:start position:0% in a cell that's surrounding the case 00:06:57.729 --> 00:06:59.489 align:start position:0% in a cell that's surrounding the case else<00:06:58.029> so<00:06:58.179> for<00:06:58.300> example<00:06:58.659> in<00:06:58.749> the<00:06:58.839> C<00:06:58.990> semantics 00:06:59.489 --> 00:06:59.499 align:start position:0% else so for example in the C semantics 00:06:59.499 --> 00:07:01.290 align:start position:0% else so for example in the C semantics we<00:06:59.649> have<00:06:59.830> or<00:06:59.979> in<00:07:00.069> the<00:07:00.129> C++<00:07:00.339> semantics<00:07:01.029> we<00:07:01.149> have 00:07:01.290 --> 00:07:01.300 align:start position:0% we have or in the C++ semantics we have 00:07:01.300 --> 00:07:04.799 align:start position:0% we have or in the C++ semantics we have we<00:07:01.809> have<00:07:01.929> multi-threading<00:07:02.559> semantics<00:07:03.809> using 00:07:04.799 --> 00:07:04.809 align:start position:0% we have multi-threading semantics using 00:07:04.809 --> 00:07:06.889 align:start position:0% we have multi-threading semantics using this<00:07:04.869> multiplicity<00:07:05.229> star<00:07:05.649> or<00:07:05.889> in<00:07:06.279> the<00:07:06.369> rolling 00:07:06.889 --> 00:07:06.899 align:start position:0% this multiplicity star or in the rolling 00:07:06.899 --> 00:07:09.329 align:start position:0% this multiplicity star or in the rolling case<00:07:07.899> semantics<00:07:08.409> that<00:07:08.469> exists<00:07:08.860> that's<00:07:08.979> one<00:07:09.189> we 00:07:09.329 --> 00:07:09.339 align:start position:0% case semantics that exists that's one we 00:07:09.339 --> 00:07:12.329 align:start position:0% case semantics that exists that's one we don't<00:07:09.459> develop<00:07:10.439> they<00:07:11.439> also<00:07:11.619> use<00:07:11.830> multiplicity 00:07:12.329 --> 00:07:12.339 align:start position:0% don't develop they also use multiplicity 00:07:12.339 --> 00:07:13.949 align:start position:0% don't develop they also use multiplicity star<00:07:12.550> for<00:07:12.789> the<00:07:12.879> independent<00:07:13.360> processes<00:07:13.839> that 00:07:13.949 --> 00:07:13.959 align:start position:0% star for the independent processes that 00:07:13.959 --> 00:07:16.739 align:start position:0% star for the independent processes that are<00:07:14.080> evolving<00:07:14.439> in<00:07:14.559> parallel<00:07:15.599> okay 00:07:16.739 --> 00:07:16.749 align:start position:0% are evolving in parallel okay 00:07:16.749 --> 00:07:24.480 align:start position:0% are evolving in parallel okay any<00:07:17.169> questions<00:07:18.129> that's<00:07:18.699> far<00:07:21.659> okay<00:07:23.339> let's<00:07:24.339> get 00:07:24.480 --> 00:07:24.490 align:start position:0% any questions that's far okay let's get 00:07:24.490 --> 00:07:26.699 align:start position:0% any questions that's far okay let's get on<00:07:24.610> to<00:07:24.759> EDM<00:07:25.330> executions<00:07:25.990> so<00:07:26.080> before<00:07:26.469> what<00:07:26.619> we 00:07:26.699 --> 00:07:26.709 align:start position:0% on to EDM executions so before what we 00:07:26.709 --> 00:07:27.959 align:start position:0% on to EDM executions so before what we saw<00:07:26.889> were<00:07:27.069> rules<00:07:27.339> that<00:07:27.610> we're<00:07:27.729> just<00:07:27.819> defining 00:07:27.959 --> 00:07:27.969 align:start position:0% saw were rules that we're just defining 00:07:27.969 --> 00:07:29.670 align:start position:0% saw were rules that we're just defining functions<00:07:28.389> essentially<00:07:29.050> and<00:07:29.349> that's<00:07:29.439> just 00:07:29.670 --> 00:07:29.680 align:start position:0% functions essentially and that's just 00:07:29.680 --> 00:07:31.559 align:start position:0% functions essentially and that's just kind<00:07:29.830> of<00:07:29.889> the<00:07:29.949> functional<00:07:30.430> you<00:07:31.029> know<00:07:31.089> subset 00:07:31.559 --> 00:07:31.569 align:start position:0% kind of the functional you know subset 00:07:31.569 --> 00:07:32.879 align:start position:0% kind of the functional you know subset of<00:07:31.599> what<00:07:31.749> you<00:07:31.839> can<00:07:31.959> define<00:07:32.169> in<00:07:32.289> K<00:07:32.469> but<00:07:32.680> now<00:07:32.830> we 00:07:32.879 --> 00:07:32.889 align:start position:0% of what you can define in K but now we 00:07:32.889 --> 00:07:35.689 align:start position:0% of what you can define in K but now we want<00:07:33.069> to<00:07:33.219> define<00:07:33.519> generic<00:07:34.479> tranzact 00:07:35.689 --> 00:07:35.699 align:start position:0% want to define generic tranzact 00:07:35.699 --> 00:07:38.399 align:start position:0% want to define generic tranzact transitions<00:07:36.699> in<00:07:36.939> the<00:07:37.059> transition<00:07:37.509> system<00:07:37.869> so 00:07:38.399 --> 00:07:38.409 align:start position:0% transitions in the transition system so 00:07:38.409 --> 00:07:40.259 align:start position:0% transitions in the transition system so first<00:07:38.889> we<00:07:39.039> need<00:07:39.189> to<00:07:39.279> say<00:07:39.429> well<00:07:39.639> how<00:07:39.849> to<00:07:39.909> perform 00:07:40.259 --> 00:07:40.269 align:start position:0% first we need to say well how to perform 00:07:40.269 --> 00:07:42.299 align:start position:0% first we need to say well how to perform a<00:07:40.419> single<00:07:40.689> step<00:07:40.929> so<00:07:40.959> we<00:07:41.259> introduce<00:07:41.889> this<00:07:42.039> next 00:07:42.299 --> 00:07:42.309 align:start position:0% a single step so we introduce this next 00:07:42.309 --> 00:07:44.489 align:start position:0% a single step so we introduce this next operator<00:07:42.909> and<00:07:43.179> in<00:07:43.929> the<00:07:44.019> yellow<00:07:44.139> paper 00:07:44.489 --> 00:07:44.499 align:start position:0% operator and in the yellow paper 00:07:44.499 --> 00:07:47.759 align:start position:0% operator and in the yellow paper basically<00:07:44.769> what<00:07:45.099> you<00:07:45.189> do<00:07:45.309> is<00:07:45.580> you<00:07:46.419> say<00:07:46.659> okay<00:07:47.559> do 00:07:47.759 --> 00:07:47.769 align:start position:0% basically what you do is you say okay do 00:07:47.769 --> 00:07:49.230 align:start position:0% basically what you do is you say okay do a<00:07:47.800> few<00:07:48.039> simple<00:07:48.249> checks<00:07:48.580> to<00:07:48.759> see<00:07:48.909> if<00:07:48.939> this<00:07:49.180> is 00:07:49.230 --> 00:07:49.240 align:start position:0% a few simple checks to see if this is 00:07:49.240 --> 00:07:50.909 align:start position:0% a few simple checks to see if this is going<00:07:49.419> to<00:07:49.479> throw<00:07:49.629> an<00:07:49.719> exception<00:07:49.809> like<00:07:50.349> well 00:07:50.909 --> 00:07:50.919 align:start position:0% going to throw an exception like well 00:07:50.919 --> 00:07:53.459 align:start position:0% going to throw an exception like well the<00:07:51.039> word<00:07:51.189> stack<00:07:51.550> be<00:07:51.909> under<00:07:52.209> overflowed<00:07:52.839> will 00:07:53.459 --> 00:07:53.469 align:start position:0% the word stack be under overflowed will 00:07:53.469 --> 00:07:55.170 align:start position:0% the word stack be under overflowed will the<00:07:53.559> gas<00:07:53.740> limit<00:07:54.069> be<00:07:54.189> exceeded<00:07:54.639> some<00:07:54.999> other 00:07:55.170 --> 00:07:55.180 align:start position:0% the gas limit be exceeded some other 00:07:55.180 --> 00:07:57.239 align:start position:0% the gas limit be exceeded some other trucks<00:07:55.419> like<00:07:55.599> that<00:07:55.749> and<00:07:55.990> then<00:07:56.379> if<00:07:56.680> not<00:07:56.979> then 00:07:57.239 --> 00:07:57.249 align:start position:0% trucks like that and then if not then 00:07:57.249 --> 00:07:58.980 align:start position:0% trucks like that and then if not then you<00:07:57.369> execute<00:07:57.729> the<00:07:57.939> OP<00:07:58.089> code<00:07:58.119> and<00:07:58.599> then 00:07:58.980 --> 00:07:58.990 align:start position:0% you execute the OP code and then 00:07:58.990 --> 00:07:59.939 align:start position:0% you execute the OP code and then afterwards<00:07:59.379> you<00:07:59.409> increment<00:07:59.800> the<00:07:59.860> program 00:07:59.939 --> 00:07:59.949 align:start position:0% afterwards you increment the program 00:07:59.949 --> 00:08:01.920 align:start position:0% afterwards you increment the program counter<00:08:00.189> and<00:08:00.639> then<00:08:01.119> you<00:08:01.209> revert<00:08:01.449> the<00:08:01.599> state<00:08:01.809> if 00:08:01.920 --> 00:08:01.930 align:start position:0% counter and then you revert the state if 00:08:01.930 --> 00:08:03.149 align:start position:0% counter and then you revert the state if any<00:08:02.110> of<00:08:02.259> the<00:08:02.379> above<00:08:02.469> steps<00:08:02.860> through<00:08:03.069> an 00:08:03.149 --> 00:08:03.159 align:start position:0% any of the above steps through an 00:08:03.159 --> 00:08:05.999 align:start position:0% any of the above steps through an exception<00:08:03.779> okay<00:08:04.779> so<00:08:05.050> here's<00:08:05.259> the<00:08:05.319> actual<00:08:05.680> K 00:08:05.999 --> 00:08:06.009 align:start position:0% exception okay so here's the actual K 00:08:06.009 --> 00:08:08.309 align:start position:0% exception okay so here's the actual K rule<00:08:06.309> right<00:08:06.579> here<00:08:06.610> notice<00:08:07.389> here<00:08:07.749> now<00:08:08.050> we<00:08:08.110> have 00:08:08.309 --> 00:08:08.319 align:start position:0% rule right here notice here now we have 00:08:08.319 --> 00:08:09.869 align:start position:0% rule right here notice here now we have the<00:08:08.469> same<00:08:08.740> keyword<00:08:09.129> rule<00:08:09.430> but<00:08:09.669> we<00:08:09.699> have 00:08:09.869 --> 00:08:09.879 align:start position:0% the same keyword rule but we have 00:08:09.879 --> 00:08:12.829 align:start position:0% the same keyword rule but we have multiple<00:08:10.300> cells<00:08:10.569> mentioned<00:08:11.110> back<00:08:11.649> up<00:08:11.919> here 00:08:12.829 --> 00:08:12.839 align:start position:0% multiple cells mentioned back up here 00:08:12.839 --> 00:08:15.359 align:start position:0% multiple cells mentioned back up here right<00:08:13.839> we<00:08:14.079> have<00:08:14.259> rule<00:08:14.559> but<00:08:14.740> we<00:08:14.829> have<00:08:14.949> no<00:08:15.129> K 00:08:15.359 --> 00:08:15.369 align:start position:0% right we have rule but we have no K 00:08:15.369 --> 00:08:16.920 align:start position:0% right we have rule but we have no K cells<00:08:15.669> mentioned<00:08:16.149> and<00:08:16.329> then<00:08:16.629> we<00:08:16.689> have<00:08:16.809> this 00:08:16.920 --> 00:08:16.930 align:start position:0% cells mentioned and then we have this 00:08:16.930 --> 00:08:18.299 align:start position:0% cells mentioned and then we have this function<00:08:17.139> attribute<00:08:17.680> which<00:08:17.800> basically<00:08:18.039> means 00:08:18.299 --> 00:08:18.309 align:start position:0% function attribute which basically means 00:08:18.309 --> 00:08:19.769 align:start position:0% function attribute which basically means that<00:08:18.399> anywhere<00:08:18.909> in<00:08:18.999> the<00:08:19.089> configuration<00:08:19.509> this 00:08:19.769 --> 00:08:19.779 align:start position:0% that anywhere in the configuration this 00:08:19.779 --> 00:08:22.769 align:start position:0% that anywhere in the configuration this rule<00:08:19.959> can<00:08:20.079> apply<00:08:20.319> but<00:08:21.249> this<00:08:21.430> rule<00:08:21.699> only<00:08:21.999> can 00:08:22.769 --> 00:08:22.779 align:start position:0% rule can apply but this rule only can 00:08:22.779 --> 00:08:24.929 align:start position:0% rule can apply but this rule only can apply<00:08:23.050> exactly<00:08:23.409> at<00:08:23.860> these<00:08:24.249> parts<00:08:24.610> of<00:08:24.789> the 00:08:24.929 --> 00:08:24.939 align:start position:0% apply exactly at these parts of the 00:08:24.939 --> 00:08:28.170 align:start position:0% apply exactly at these parts of the configuration<00:08:25.569> so<00:08:26.379> what<00:08:27.099> do<00:08:27.159> we<00:08:27.219> do<00:08:27.369> when<00:08:28.089> we 00:08:28.170 --> 00:08:28.180 align:start position:0% configuration so what do we do when we 00:08:28.180 --> 00:08:30.480 align:start position:0% configuration so what do we do when we see<00:08:28.300> the<00:08:28.419> next<00:08:28.599> operator<00:08:29.079> we<00:08:29.319> replace<00:08:29.709> it<00:08:29.979> with 00:08:30.480 --> 00:08:30.490 align:start position:0% see the next operator we replace it with 00:08:30.490 --> 00:08:32.759 align:start position:0% see the next operator we replace it with this<00:08:30.729> chunk<00:08:31.029> of<00:08:31.119> code<00:08:31.180> when<00:08:32.169> the<00:08:32.349> program 00:08:32.759 --> 00:08:32.769 align:start position:0% this chunk of code when the program 00:08:32.769 --> 00:08:34.649 align:start position:0% this chunk of code when the program counter<00:08:32.949> is<00:08:33.250> P<00:08:33.459> count<00:08:33.759> and<00:08:33.969> in<00:08:34.240> the<00:08:34.479> program 00:08:34.649 --> 00:08:34.659 align:start position:0% counter is P count and in the program 00:08:34.659 --> 00:08:36.990 align:start position:0% counter is P count and in the program cell<00:08:35.079> the<00:08:35.169> current<00:08:35.409> program<00:08:35.740> so<00:08:35.949> that<00:08:36.550> program 00:08:36.990 --> 00:08:37.000 align:start position:0% cell the current program so that program 00:08:37.000 --> 00:08:38.759 align:start position:0% cell the current program so that program counter<00:08:37.389> is<00:08:37.419> pointing<00:08:37.959> to<00:08:38.079> OP<00:08:38.229> and<00:08:38.560> we<00:08:38.620> don't 00:08:38.759 --> 00:08:38.769 align:start position:0% counter is pointing to OP and we don't 00:08:38.769 --> 00:08:40.379 align:start position:0% counter is pointing to OP and we don't care<00:08:38.949> about<00:08:39.009> the<00:08:39.310> rest<00:08:39.459> of<00:08:39.759> the<00:08:39.880> program 00:08:40.379 --> 00:08:40.389 align:start position:0% care about the rest of the program 00:08:40.389 --> 00:08:42.480 align:start position:0% care about the rest of the program note<00:08:40.719> that<00:08:40.750> this<00:08:40.959> dot<00:08:41.199> dot<00:08:41.439> is<00:08:41.889> not<00:08:42.099> me 00:08:42.480 --> 00:08:42.490 align:start position:0% note that this dot dot is not me 00:08:42.490 --> 00:08:44.159 align:start position:0% note that this dot dot is not me alighting<00:08:43.029> details<00:08:43.389> that's<00:08:43.659> actually<00:08:44.050> what 00:08:44.159 --> 00:08:44.169 align:start position:0% alighting details that's actually what 00:08:44.169 --> 00:08:45.389 align:start position:0% alighting details that's actually what the<00:08:44.259> rule<00:08:44.410> looks<00:08:44.560> like<00:08:44.769> this<00:08:44.920> is<00:08:45.009> verbatim 00:08:45.389 --> 00:08:45.399 align:start position:0% the rule looks like this is verbatim 00:08:45.399 --> 00:08:46.139 align:start position:0% the rule looks like this is verbatim what<00:08:45.459> the<00:08:45.579> rule<00:08:45.699> looks<00:08:45.850> like<00:08:45.970> in<00:08:46.089> the 00:08:46.139 --> 00:08:46.149 align:start position:0% what the rule looks like in the 00:08:46.149 --> 00:08:48.660 align:start position:0% what the rule looks like in the semantics<00:08:46.600> so<00:08:47.199> essentially<00:08:47.709> we<00:08:48.130> use<00:08:48.310> this<00:08:48.459> dot 00:08:48.660 --> 00:08:48.670 align:start position:0% semantics so essentially we use this dot 00:08:48.670 --> 00:08:50.790 align:start position:0% semantics so essentially we use this dot dot<00:08:48.880> to<00:08:49.149> tell<00:08:49.300> K<00:08:49.540> don't<00:08:49.959> care<00:08:50.260> we<00:08:50.589> don't<00:08:50.620> care 00:08:50.790 --> 00:08:50.800 align:start position:0% dot to tell K don't care we don't care 00:08:50.800 --> 00:08:52.139 align:start position:0% dot to tell K don't care we don't care what's<00:08:51.069> there<00:08:51.220> we<00:08:51.370> just<00:08:51.519> care<00:08:51.670> about<00:08:51.699> that<00:08:51.970> one 00:08:52.139 --> 00:08:52.149 align:start position:0% what's there we just care about that one 00:08:52.149 --> 00:08:53.370 align:start position:0% what's there we just care about that one particular 00:08:53.370 --> 00:08:53.380 align:start position:0% particular 00:08:53.380 --> 00:08:57.660 align:start position:0% particular opcode<00:08:53.980> in<00:08:54.220> the<00:08:54.510> program<00:08:55.510> cell<00:08:56.310> so<00:08:57.310> yeah<00:08:57.460> when 00:08:57.660 --> 00:08:57.670 align:start position:0% opcode in the program cell so yeah when 00:08:57.670 --> 00:08:59.970 align:start position:0% opcode in the program cell so yeah when we<00:08:57.760> go<00:08:57.880> next<00:08:58.300> we<00:08:58.450> say<00:08:58.630> first<00:08:58.960> push<00:08:59.620> the<00:08:59.800> call 00:08:59.970 --> 00:08:59.980 align:start position:0% we go next we say first push the call 00:08:59.980 --> 00:09:01.770 align:start position:0% we go next we say first push the call stack<00:09:00.280> which<00:09:00.520> basically<00:09:00.820> saves<00:09:01.180> a<00:09:01.330> copy<00:09:01.510> of 00:09:01.770 --> 00:09:01.780 align:start position:0% stack which basically saves a copy of 00:09:01.780 --> 00:09:04.830 align:start position:0% stack which basically saves a copy of the<00:09:01.870> current<00:09:02.020> execution<00:09:02.380> state<00:09:03.720> then<00:09:04.720> we 00:09:04.830 --> 00:09:04.840 align:start position:0% the current execution state then we 00:09:04.840 --> 00:09:06.780 align:start position:0% the current execution state then we check<00:09:05.050> is<00:09:05.230> it<00:09:05.380> exceptional<00:09:05.920> this<00:09:06.100> is<00:09:06.310> is<00:09:06.550> it<00:09:06.730> a 00:09:06.780 --> 00:09:06.790 align:start position:0% check is it exceptional this is is it a 00:09:06.790 --> 00:09:08.460 align:start position:0% check is it exceptional this is is it a bad<00:09:06.940> jump<00:09:07.240> operator<00:09:07.780> so<00:09:07.990> is<00:09:08.050> it<00:09:08.110> going<00:09:08.230> to<00:09:08.290> jump 00:09:08.460 --> 00:09:08.470 align:start position:0% bad jump operator so is it going to jump 00:09:08.470 --> 00:09:10.350 align:start position:0% bad jump operator so is it going to jump to<00:09:08.500> an<00:09:08.650> invalid<00:09:08.860> jump<00:09:09.160> destination<00:09:09.700> is<00:09:09.850> it<00:09:10.240> one 00:09:10.350 --> 00:09:10.360 align:start position:0% to an invalid jump destination is it one 00:09:10.360 --> 00:09:12.890 align:start position:0% to an invalid jump destination is it one of<00:09:10.420> the<00:09:10.480> designated<00:09:10.960> invalid<00:09:11.350> operators 00:09:12.890 --> 00:09:12.900 align:start position:0% of the designated invalid operators 00:09:12.900 --> 00:09:15.030 align:start position:0% of the designated invalid operators there's<00:09:13.900> one<00:09:14.080> of<00:09:14.260> the<00:09:14.380> stack<00:09:14.590> underflow<00:09:15.010> or 00:09:15.030 --> 00:09:15.040 align:start position:0% there's one of the stack underflow or 00:09:15.040 --> 00:09:19.230 align:start position:0% there's one of the stack underflow or overflow<00:09:15.160> check<00:09:16.770> if<00:09:17.770> that<00:09:18.130> check<00:09:18.670> passes<00:09:19.090> and 00:09:19.230 --> 00:09:19.240 align:start position:0% overflow check if that check passes and 00:09:19.240 --> 00:09:20.310 align:start position:0% overflow check if that check passes and doesn't<00:09:19.450> throw<00:09:19.540> an<00:09:19.630> exception<00:09:19.690> then<00:09:20.260> we 00:09:20.310 --> 00:09:20.320 align:start position:0% doesn't throw an exception then we 00:09:20.320 --> 00:09:22.050 align:start position:0% doesn't throw an exception then we actually<00:09:20.470> execute<00:09:21.070> the<00:09:21.100> operator<00:09:21.520> which<00:09:21.760> does 00:09:22.050 --> 00:09:22.060 align:start position:0% actually execute the operator which does 00:09:22.060 --> 00:09:23.670 align:start position:0% actually execute the operator which does the<00:09:22.240> memory<00:09:22.450> computation<00:09:23.230> how<00:09:23.380> much<00:09:23.500> memory 00:09:23.670 --> 00:09:23.680 align:start position:0% the memory computation how much memory 00:09:23.680 --> 00:09:25.980 align:start position:0% the memory computation how much memory this<00:09:23.920> is<00:09:24.040> going<00:09:24.190> to<00:09:24.250> change<00:09:24.780> also<00:09:25.780> does<00:09:25.900> the 00:09:25.980 --> 00:09:25.990 align:start position:0% this is going to change also does the 00:09:25.990 --> 00:09:27.990 align:start position:0% this is going to change also does the gas<00:09:26.110> computation<00:09:26.800> and<00:09:26.950> also<00:09:27.280> has<00:09:27.460> the<00:09:27.670> effect 00:09:27.990 --> 00:09:28.000 align:start position:0% gas computation and also has the effect 00:09:28.000 --> 00:09:29.760 align:start position:0% gas computation and also has the effect on<00:09:28.180> the<00:09:28.330> state<00:09:28.600> of<00:09:28.810> whatever<00:09:29.110> this<00:09:29.290> opcode<00:09:29.740> is 00:09:29.760 --> 00:09:29.770 align:start position:0% on the state of whatever this opcode is 00:09:29.770 --> 00:09:31.080 align:start position:0% on the state of whatever this opcode is and<00:09:30.040> then<00:09:30.460> we<00:09:30.550> increment<00:09:30.670> the<00:09:31.000> program 00:09:31.080 --> 00:09:31.090 align:start position:0% and then we increment the program 00:09:31.090 --> 00:09:33.180 align:start position:0% and then we increment the program counter<00:09:31.360> if<00:09:31.990> any<00:09:32.590> of<00:09:32.740> these<00:09:32.830> throw<00:09:33.100> an 00:09:33.180 --> 00:09:33.190 align:start position:0% counter if any of these throw an 00:09:33.190 --> 00:09:34.800 align:start position:0% counter if any of these throw an exception<00:09:33.280> that<00:09:33.880> exception<00:09:34.210> ends<00:09:34.720> up 00:09:34.800 --> 00:09:34.810 align:start position:0% exception that exception ends up 00:09:34.810 --> 00:09:36.870 align:start position:0% exception that exception ends up consuming<00:09:35.310> the<00:09:36.310> remaining<00:09:36.670> of<00:09:36.760> these 00:09:36.870 --> 00:09:36.880 align:start position:0% consuming the remaining of these 00:09:36.880 --> 00:09:39.630 align:start position:0% consuming the remaining of these operators<00:09:37.270> until<00:09:37.690> it<00:09:37.840> hits<00:09:38.020> this<00:09:38.640> syntax 00:09:39.630 --> 00:09:39.640 align:start position:0% operators until it hits this syntax 00:09:39.640 --> 00:09:41.430 align:start position:0% operators until it hits this syntax right<00:09:39.940> here<00:09:40.210> which<00:09:40.510> basically<00:09:40.810> acts<00:09:41.110> like<00:09:41.320> an 00:09:41.430 --> 00:09:41.440 align:start position:0% right here which basically acts like an 00:09:41.440 --> 00:09:43.560 align:start position:0% right here which basically acts like an if-then-else<00:09:41.860> over<00:09:42.160> exceptions<00:09:42.670> so<00:09:43.240> if<00:09:43.390> there 00:09:43.560 --> 00:09:43.570 align:start position:0% if-then-else over exceptions so if there 00:09:43.570 --> 00:09:44.520 align:start position:0% if-then-else over exceptions so if there is<00:09:43.600> no<00:09:43.840> exceptions 00:09:44.520 --> 00:09:44.530 align:start position:0% is no exceptions 00:09:44.530 --> 00:09:47.100 align:start position:0% is no exceptions we<00:09:44.770> drop<00:09:45.040> the<00:09:45.190> call<00:09:45.370> stack<00:09:45.700> which<00:09:46.210> essentially 00:09:47.100 --> 00:09:47.110 align:start position:0% we drop the call stack which essentially 00:09:47.110 --> 00:09:48.720 align:start position:0% we drop the call stack which essentially forgets<00:09:47.500> the<00:09:47.710> state<00:09:47.920> that<00:09:48.070> we<00:09:48.130> saved<00:09:48.370> up<00:09:48.520> here 00:09:48.720 --> 00:09:48.730 align:start position:0% forgets the state that we saved up here 00:09:48.730 --> 00:09:50.610 align:start position:0% forgets the state that we saved up here but<00:09:49.210> there<00:09:49.330> is<00:09:49.510> an<00:09:49.720> exception<00:09:49.810> we<00:09:50.320> take<00:09:50.500> the 00:09:50.610 --> 00:09:50.620 align:start position:0% but there is an exception we take the 00:09:50.620 --> 00:09:52.470 align:start position:0% but there is an exception we take the false<00:09:50.860> branch<00:09:51.130> of<00:09:51.370> this<00:09:51.460> if-then-else<00:09:52.000> which 00:09:52.470 --> 00:09:52.480 align:start position:0% false branch of this if-then-else which 00:09:52.480 --> 00:09:53.580 align:start position:0% false branch of this if-then-else which means<00:09:52.660> that<00:09:52.750> we<00:09:52.840> pop<00:09:53.020> the<00:09:53.170> call<00:09:53.350> stack 00:09:53.580 --> 00:09:53.590 align:start position:0% means that we pop the call stack 00:09:53.590 --> 00:09:55.260 align:start position:0% means that we pop the call stack reverting<00:09:54.250> to<00:09:54.280> the<00:09:54.490> previous<00:09:54.850> state<00:09:55.060> and 00:09:55.260 --> 00:09:55.270 align:start position:0% reverting to the previous state and 00:09:55.270 --> 00:09:57.570 align:start position:0% reverting to the previous state and propagate<00:09:56.020> the<00:09:56.110> exception<00:09:56.530> on<00:09:56.710> so<00:09:57.400> this 00:09:57.570 --> 00:09:57.580 align:start position:0% propagate the exception on so this 00:09:57.580 --> 00:09:59.280 align:start position:0% propagate the exception on so this little<00:09:57.820> squiggly<00:09:58.060> arrow<00:09:58.240> can<00:09:58.840> be<00:09:58.870> read<00:09:59.140> as 00:09:59.280 --> 00:09:59.290 align:start position:0% little squiggly arrow can be read as 00:09:59.290 --> 00:10:01.830 align:start position:0% little squiggly arrow can be read as followed<00:09:59.800> by<00:09:59.950> essentially<00:10:00.730> so<00:10:01.420> if<00:10:01.600> you<00:10:01.690> only 00:10:01.830 --> 00:10:01.840 align:start position:0% followed by essentially so if you only 00:10:01.840 --> 00:10:04.110 align:start position:0% followed by essentially so if you only see<00:10:02.140> a<00:10:02.350> single<00:10:02.740> element<00:10:02.980> right<00:10:03.280> here<00:10:03.610> with 00:10:04.110 --> 00:10:04.120 align:start position:0% see a single element right here with 00:10:04.120 --> 00:10:07.110 align:start position:0% see a single element right here with this<00:10:04.240> dot<00:10:04.480> dot<00:10:04.690> so<00:10:05.440> this<00:10:05.620> the<00:10:06.430> precedence<00:10:07.000> of 00:10:07.110 --> 00:10:07.120 align:start position:0% this dot dot so this the precedence of 00:10:07.120 --> 00:10:09.210 align:start position:0% this dot dot so this the precedence of this<00:10:07.270> is<00:10:07.420> that<00:10:07.600> this<00:10:07.810> dot<00:10:08.200> dot<00:10:08.230> is<00:10:08.470> outside<00:10:08.950> of 00:10:09.210 --> 00:10:09.220 align:start position:0% this is that this dot dot is outside of 00:10:09.220 --> 00:10:13.200 align:start position:0% this is that this dot dot is outside of the<00:10:09.700> scope<00:10:09.820> of<00:10:10.090> this<00:10:10.240> rewrite<00:10:11.020> arrow<00:10:12.210> then 00:10:13.200 --> 00:10:13.210 align:start position:0% the scope of this rewrite arrow then 00:10:13.210 --> 00:10:14.640 align:start position:0% the scope of this rewrite arrow then that<00:10:13.390> means<00:10:13.570> there's<00:10:13.750> only<00:10:13.810> a<00:10:13.960> single<00:10:14.170> element 00:10:14.640 --> 00:10:14.650 align:start position:0% that means there's only a single element 00:10:14.650 --> 00:10:16.380 align:start position:0% that means there's only a single element and<00:10:14.800> then<00:10:14.890> anything<00:10:15.160> else<00:10:15.430> in<00:10:15.910> the<00:10:16.060> followed 00:10:16.380 --> 00:10:16.390 align:start position:0% and then anything else in the followed 00:10:16.390 --> 00:10:17.760 align:start position:0% and then anything else in the followed by<00:10:16.510> part<00:10:16.780> but<00:10:16.930> we're<00:10:17.080> replacing<00:10:17.290> the<00:10:17.590> single 00:10:17.760 --> 00:10:17.770 align:start position:0% by part but we're replacing the single 00:10:17.770 --> 00:10:18.720 align:start position:0% by part but we're replacing the single element<00:10:18.160> with<00:10:18.280> several<00:10:18.610> different 00:10:18.720 --> 00:10:18.730 align:start position:0% element with several different 00:10:18.730 --> 00:10:21.360 align:start position:0% element with several different computations<00:10:19.480> to<00:10:19.720> make<00:10:19.900> does<00:10:20.890> this<00:10:21.040> make 00:10:21.360 --> 00:10:21.370 align:start position:0% computations to make does this make 00:10:21.370 --> 00:10:26.090 align:start position:0% computations to make does this make sense<00:10:24.480> all<00:10:25.480> right 00:10:26.090 --> 00:10:26.100 align:start position:0% sense all right 00:10:26.100 --> 00:10:29.160 align:start position:0% sense all right okay<00:10:27.100> so<00:10:27.160> EBM<00:10:27.730> programs<00:10:28.150> let's<00:10:28.870> take<00:10:28.990> a<00:10:29.020> look 00:10:29.160 --> 00:10:29.170 align:start position:0% okay so EBM programs let's take a look 00:10:29.170 --> 00:10:32.460 align:start position:0% okay so EBM programs let's take a look what<00:10:29.290> they<00:10:29.410> look<00:10:29.590> like<00:10:29.620> in<00:10:29.860> K<00:10:31.110> EVM<00:10:32.110> opcodes 00:10:32.460 --> 00:10:32.470 align:start position:0% what they look like in K EVM opcodes 00:10:32.470 --> 00:10:34.650 align:start position:0% what they look like in K EVM opcodes here<00:10:32.830> are<00:10:32.950> some<00:10:33.190> simple<00:10:33.610> expressions<00:10:34.180> so<00:10:34.480> we 00:10:34.650 --> 00:10:34.660 align:start position:0% here are some simple expressions so we 00:10:34.660 --> 00:10:36.690 align:start position:0% here are some simple expressions so we actually<00:10:34.810> been<00:10:35.500> up<00:10:35.680> the<00:10:35.830> opcodes<00:10:36.250> based<00:10:36.520> on 00:10:36.690 --> 00:10:36.700 align:start position:0% actually been up the opcodes based on 00:10:36.700 --> 00:10:39.030 align:start position:0% actually been up the opcodes based on their<00:10:36.940> arity<00:10:37.360> essentially<00:10:37.990> so<00:10:38.200> sub<00:10:38.650> and<00:10:38.830> div 00:10:39.030 --> 00:10:39.040 align:start position:0% their arity essentially so sub and div 00:10:39.040 --> 00:10:41.400 align:start position:0% their arity essentially so sub and div are<00:10:39.250> binstock<00:10:39.670> ops<00:10:40.000> and<00:10:40.240> we<00:10:40.720> use<00:10:40.930> somewhere 00:10:41.400 --> 00:10:41.410 align:start position:0% are binstock ops and we use somewhere 00:10:41.410 --> 00:10:42.420 align:start position:0% are binstock ops and we use somewhere else<00:10:41.560> in<00:10:41.680> the<00:10:41.770> semantics<00:10:42.220> we<00:10:42.340> will 00:10:42.420 --> 00:10:42.430 align:start position:0% else in the semantics we will 00:10:42.430 --> 00:10:44.010 align:start position:0% else in the semantics we will automatically<00:10:43.000> load<00:10:43.180> the<00:10:43.210> arguments<00:10:43.870> based 00:10:44.010 --> 00:10:44.020 align:start position:0% automatically load the arguments based 00:10:44.020 --> 00:10:45.690 align:start position:0% automatically load the arguments based on<00:10:44.200> the<00:10:44.320> air<00:10:44.440> D<00:10:44.590> so<00:10:44.710> all<00:10:44.860> bins<00:10:45.100> stack<00:10:45.310> offs<00:10:45.520> will 00:10:45.690 --> 00:10:45.700 align:start position:0% on the air D so all bins stack offs will 00:10:45.700 --> 00:10:47.340 align:start position:0% on the air D so all bins stack offs will get<00:10:45.820> two<00:10:45.970> arguments<00:10:46.420> off<00:10:46.510> the<00:10:46.630> word<00:10:46.750> stack<00:10:47.050> and 00:10:47.340 --> 00:10:47.350 align:start position:0% get two arguments off the word stack and 00:10:47.350 --> 00:10:48.900 align:start position:0% get two arguments off the word stack and the<00:10:47.800> word<00:10:47.950> stack<00:10:48.190> will<00:10:48.310> have<00:10:48.430> those<00:10:48.580> arguments 00:10:48.900 --> 00:10:48.910 align:start position:0% the word stack will have those arguments 00:10:48.910 --> 00:10:51.690 align:start position:0% the word stack will have those arguments removed<00:10:49.360> so<00:10:50.020> sub<00:10:50.290> just<00:10:50.500> goes<00:10:50.680> to<00:10:50.860> -<00:10:51.130> word<00:10:51.340> Dave 00:10:51.690 --> 00:10:51.700 align:start position:0% removed so sub just goes to - word Dave 00:10:51.700 --> 00:10:54.570 align:start position:0% removed so sub just goes to - word Dave goes<00:10:51.910> to<00:10:52.090> /<00:10:52.510> push<00:10:52.900> /<00:10:53.470> word<00:10:53.770> and<00:10:53.980> then<00:10:54.400> that's 00:10:54.570 --> 00:10:54.580 align:start position:0% goes to / push / word and then that's 00:10:54.580 --> 00:10:56.160 align:start position:0% goes to / push / word and then that's followed<00:10:54.730> by<00:10:54.880> this<00:10:55.000> hash<00:10:55.300> push<00:10:55.630> which<00:10:55.900> is<00:10:56.020> just 00:10:56.160 --> 00:10:56.170 align:start position:0% followed by this hash push which is just 00:10:56.170 --> 00:10:58.110 align:start position:0% followed by this hash push which is just an<00:10:56.260> internal<00:10:56.620> operator<00:10:57.010> for<00:10:57.190> actually<00:10:57.520> moving 00:10:58.110 --> 00:10:58.120 align:start position:0% an internal operator for actually moving 00:10:58.120 --> 00:11:00.270 align:start position:0% an internal operator for actually moving the<00:10:58.300> result<00:10:58.600> over<00:10:58.870> to<00:10:59.050> the<00:10:59.170> /<00:10:59.980> -<00:11:00.070> the<00:11:00.160> word 00:11:00.270 --> 00:11:00.280 align:start position:0% the result over to the / - the word 00:11:00.280 --> 00:11:04.829 align:start position:0% the result over to the / - the word stack<00:11:01.140> and<00:11:02.700> then<00:11:03.700> in<00:11:03.970> here's<00:11:04.390> some<00:11:04.540> local 00:11:04.829 --> 00:11:04.839 align:start position:0% stack and then in here's some local 00:11:04.839 --> 00:11:06.780 align:start position:0% stack and then in here's some local memory<00:11:04.990> operators<00:11:05.589> like<00:11:05.770> M<00:11:05.950> load<00:11:06.250> which<00:11:06.550> is<00:11:06.580> a 00:11:06.780 --> 00:11:06.790 align:start position:0% memory operators like M load which is a 00:11:06.790 --> 00:11:08.880 align:start position:0% memory operators like M load which is a and<00:11:06.880> stack<00:11:07.210> up<00:11:07.420> so<00:11:07.630> it<00:11:07.690> takes<00:11:07.840> one<00:11:08.020> argument<00:11:08.050> so 00:11:08.880 --> 00:11:08.890 align:start position:0% and stack up so it takes one argument so 00:11:08.890 --> 00:11:11.340 align:start position:0% and stack up so it takes one argument so M<00:11:09.070> load<00:11:09.340> had<00:11:09.640> a<00:11:09.670> specific<00:11:09.940> index<00:11:10.480> you<00:11:11.080> go<00:11:11.200> and 00:11:11.340 --> 00:11:11.350 align:start position:0% M load had a specific index you go and 00:11:11.350 --> 00:11:12.780 align:start position:0% M load had a specific index you go and grab<00:11:11.530> the<00:11:11.680> local<00:11:11.980> memory<00:11:12.160> from<00:11:12.400> the<00:11:12.490> local 00:11:12.780 --> 00:11:12.790 align:start position:0% grab the local memory from the local 00:11:12.790 --> 00:11:16.080 align:start position:0% grab the local memory from the local memory<00:11:12.940> cell<00:11:13.240> and<00:11:13.450> then<00:11:14.440> you<00:11:14.560> say<00:11:14.770> as<00:11:15.010> word<00:11:15.400> the 00:11:16.080 --> 00:11:16.090 align:start position:0% memory cell and then you say as word the 00:11:16.090 --> 00:11:17.910 align:start position:0% memory cell and then you say as word the range<00:11:16.390> for<00:11:16.840> the<00:11:16.960> local<00:11:17.260> memory<00:11:17.410> starting<00:11:17.830> at 00:11:17.910 --> 00:11:17.920 align:start position:0% range for the local memory starting at 00:11:17.920 --> 00:11:20.310 align:start position:0% range for the local memory starting at index<00:11:18.220> and<00:11:18.430> going<00:11:18.610> 32<00:11:18.970> bytes<00:11:19.180> so<00:11:19.720> you<00:11:19.780> take<00:11:19.930> 32 00:11:20.310 --> 00:11:20.320 align:start position:0% index and going 32 bytes so you take 32 00:11:20.320 --> 00:11:21.990 align:start position:0% index and going 32 bytes so you take 32 bytes<00:11:20.530> from<00:11:20.650> a<00:11:20.740> local<00:11:20.980> memory<00:11:21.130> pack<00:11:21.850> it 00:11:21.990 --> 00:11:22.000 align:start position:0% bytes from a local memory pack it 00:11:22.000 --> 00:11:23.790 align:start position:0% bytes from a local memory pack it together<00:11:22.240> as<00:11:22.420> a<00:11:22.450> word<00:11:22.660> and<00:11:22.960> then<00:11:23.530> you<00:11:23.620> push 00:11:23.790 --> 00:11:23.800 align:start position:0% together as a word and then you push 00:11:23.800 --> 00:11:25.200 align:start position:0% together as a word and then you push that<00:11:23.980> on<00:11:24.130> to<00:11:24.220> the<00:11:24.280> word<00:11:24.430> stack<00:11:24.700> because 00:11:25.200 --> 00:11:25.210 align:start position:0% that on to the word stack because 00:11:25.210 --> 00:11:26.670 align:start position:0% that on to the word stack because remember<00:11:25.420> the<00:11:25.600> local<00:11:25.930> memory<00:11:26.080> is<00:11:26.320> actually<00:11:26.650> a 00:11:26.670 --> 00:11:26.680 align:start position:0% remember the local memory is actually a 00:11:26.680 --> 00:11:29.780 align:start position:0% remember the local memory is actually a byte<00:11:26.980> sequence<00:11:27.820> it's<00:11:28.000> not<00:11:28.150> a<00:11:28.180> word<00:11:28.390> sequence 00:11:29.780 --> 00:11:29.790 align:start position:0% byte sequence it's not a word sequence 00:11:29.790 --> 00:11:33.150 align:start position:0% byte sequence it's not a word sequence here<00:11:30.790> we<00:11:30.910> have<00:11:31.030> a<00:11:31.060> bin<00:11:31.240> stack<00:11:31.480> up<00:11:31.720> M<00:11:31.930> store<00:11:32.290> so<00:11:32.860> M 00:11:33.150 --> 00:11:33.160 align:start position:0% here we have a bin stack up M store so M 00:11:33.160 --> 00:11:36.570 align:start position:0% here we have a bin stack up M store so M store<00:11:33.520> of<00:11:33.760> this<00:11:34.390> value<00:11:34.930> at<00:11:35.140> this<00:11:35.410> index<00:11:35.860> it's 00:11:36.570 --> 00:11:36.580 align:start position:0% store of this value at this index it's 00:11:36.580 --> 00:11:37.860 align:start position:0% store of this value at this index it's going<00:11:36.730> to<00:11:36.790> take<00:11:36.940> the<00:11:37.060> local<00:11:37.360> memory<00:11:37.540> and 00:11:37.860 --> 00:11:37.870 align:start position:0% going to take the local memory and 00:11:37.870 --> 00:11:40.020 align:start position:0% going to take the local memory and replace<00:11:38.200> it<00:11:38.440> with<00:11:38.470> the<00:11:38.680> local<00:11:38.860> memory<00:11:39.340> where 00:11:40.020 --> 00:11:40.030 align:start position:0% replace it with the local memory where 00:11:40.030 --> 00:11:43.790 align:start position:0% replace it with the local memory where at<00:11:40.180> that<00:11:40.390> index<00:11:40.900> you<00:11:41.290> write<00:11:41.590> 32<00:11:42.430> words 00:11:43.790 --> 00:11:43.800 align:start position:0% at that index you write 32 words 00:11:43.800 --> 00:11:46.290 align:start position:0% at that index you write 32 words prefixed<00:11:44.800> with<00:11:44.980> essentially<00:11:45.790> the<00:11:45.820> bytes<00:11:46.060> of 00:11:46.290 --> 00:11:46.300 align:start position:0% prefixed with essentially the bytes of 00:11:46.300 --> 00:11:48.630 align:start position:0% prefixed with essentially the bytes of this<00:11:46.450> value<00:11:47.350> so<00:11:47.680> you<00:11:47.740> chop<00:11:48.010> that<00:11:48.190> value<00:11:48.550> up 00:11:48.630 --> 00:11:48.640 align:start position:0% this value so you chop that value up 00:11:48.640 --> 00:11:50.280 align:start position:0% this value so you chop that value up into<00:11:48.820> 32<00:11:49.060> different<00:11:49.240> words<00:11:49.540> if<00:11:49.900> it's<00:11:50.140> not 00:11:50.280 --> 00:11:50.290 align:start position:0% into 32 different words if it's not 00:11:50.290 --> 00:11:52.080 align:start position:0% into 32 different words if it's not enough<00:11:50.530> you<00:11:50.680> pad<00:11:50.890> it<00:11:50.920> to<00:11:51.100> the<00:11:51.190> width<00:11:51.340> of<00:11:51.460> 32<00:11:51.850> and 00:11:52.080 --> 00:11:52.090 align:start position:0% enough you pad it to the width of 32 and 00:11:52.090 --> 00:11:54.170 align:start position:0% enough you pad it to the width of 32 and then<00:11:52.570> you<00:11:52.660> write<00:11:52.810> it<00:11:52.900> to<00:11:52.990> the<00:11:53.020> local<00:11:53.200> memory 00:11:54.170 --> 00:11:54.180 align:start position:0% then you write it to the local memory 00:11:54.180 --> 00:11:58.320 align:start position:0% then you write it to the local memory does<00:11:55.180> this<00:11:55.300> make<00:11:55.690> sense<00:11:56.340> okay<00:11:57.340> so<00:11:58.060> the<00:11:58.150> rules 00:11:58.320 --> 00:11:58.330 align:start position:0% does this make sense okay so the rules 00:11:58.330 --> 00:11:59.400 align:start position:0% does this make sense okay so the rules are<00:11:58.420> gonna<00:11:58.600> start<00:11:58.810> getting<00:11:58.930> bigger<00:11:59.230> and 00:11:59.400 --> 00:11:59.410 align:start position:0% are gonna start getting bigger and 00:11:59.410 --> 00:12:00.750 align:start position:0% are gonna start getting bigger and mentioning<00:11:59.800> more<00:11:59.950> of<00:12:00.010> the<00:12:00.100> configuration 00:12:00.750 --> 00:12:00.760 align:start position:0% mentioning more of the configuration 00:12:00.760 --> 00:12:02.850 align:start position:0% mentioning more of the configuration notice<00:12:01.150> this<00:12:01.330> only<00:12:01.510> mentions<00:12:01.870> one<00:12:02.020> cell<00:12:02.320> this 00:12:02.850 --> 00:12:02.860 align:start position:0% notice this only mentions one cell this 00:12:02.860 --> 00:12:04.230 align:start position:0% notice this only mentions one cell this mentions<00:12:03.190> two<00:12:03.340> so<00:12:03.490> oh<00:12:03.700> and<00:12:03.730> there's<00:12:03.940> one<00:12:04.090> more 00:12:04.230 --> 00:12:04.240 align:start position:0% mentions two so oh and there's one more 00:12:04.240 --> 00:12:06.120 align:start position:0% mentions two so oh and there's one more thing<00:12:04.450> notice<00:12:05.050> here<00:12:05.320> we<00:12:05.440> have<00:12:05.470> to<00:12:05.860> rewrite 00:12:06.120 --> 00:12:06.130 align:start position:0% thing notice here we have to rewrite 00:12:06.130 --> 00:12:09.060 align:start position:0% thing notice here we have to rewrite arrows<00:12:06.720> this<00:12:07.720> is<00:12:07.930> as<00:12:08.080> opposed<00:12:08.350> to<00:12:08.500> a<00:12:08.650> lot<00:12:09.040> of 00:12:09.060 --> 00:12:09.070 align:start position:0% arrows this is as opposed to a lot of 00:12:09.070 --> 00:12:10.620 align:start position:0% arrows this is as opposed to a lot of languages<00:12:09.610> which<00:12:09.850> would<00:12:10.000> require<00:12:10.300> that<00:12:10.510> you 00:12:10.620 --> 00:12:10.630 align:start position:0% languages which would require that you 00:12:10.630 --> 00:12:13.290 align:start position:0% languages which would require that you pull<00:12:10.870> this<00:12:11.050> rewrite<00:12:11.440> arrow<00:12:11.710> outside<00:12:12.610> copy<00:12:13.090> the 00:12:13.290 --> 00:12:13.300 align:start position:0% pull this rewrite arrow outside copy the 00:12:13.300 --> 00:12:15.810 align:start position:0% pull this rewrite arrow outside copy the whole<00:12:13.390> configuration<00:12:13.720> above<00:12:14.350> and<00:12:14.500> below<00:12:14.820> but 00:12:15.810 --> 00:12:15.820 align:start position:0% whole configuration above and below but 00:12:15.820 --> 00:12:17.490 align:start position:0% whole configuration above and below but if<00:12:15.970> essentially<00:12:16.450> K<00:12:16.600> does<00:12:16.840> that<00:12:16.990> for<00:12:17.230> you<00:12:17.380> it 00:12:17.490 --> 00:12:17.500 align:start position:0% if essentially K does that for you it 00:12:17.500 --> 00:12:19.140 align:start position:0% if essentially K does that for you it pulls<00:12:17.710> rewrite<00:12:18.040> arrow<00:12:18.220> outside<00:12:18.610> and<00:12:18.790> copies 00:12:19.140 --> 00:12:19.150 align:start position:0% pulls rewrite arrow outside and copies 00:12:19.150 --> 00:12:20.910 align:start position:0% pulls rewrite arrow outside and copies you<00:12:19.690> know<00:12:19.810> so<00:12:19.930> you'll<00:12:20.080> have<00:12:20.170> a<00:12:20.230> K<00:12:20.440> and<00:12:20.590> a<00:12:20.680> local 00:12:20.910 --> 00:12:20.920 align:start position:0% you know so you'll have a K and a local 00:12:20.920 --> 00:12:22.440 align:start position:0% you know so you'll have a K and a local man<00:12:21.040> before<00:12:21.340> then<00:12:21.550> the<00:12:21.700> rewrite<00:12:21.970> arrow<00:12:22.180> then<00:12:22.390> a 00:12:22.440 --> 00:12:22.450 align:start position:0% man before then the rewrite arrow then a 00:12:22.450 --> 00:12:24.420 align:start position:0% man before then the rewrite arrow then a key<00:12:22.600> and<00:12:22.660> a<00:12:22.750> local<00:12:22.900> man<00:12:23.170> with<00:12:23.890> the<00:12:24.010> right<00:12:24.190> hand 00:12:24.420 --> 00:12:24.430 align:start position:0% key and a local man with the right hand 00:12:24.430 --> 00:12:26.070 align:start position:0% key and a local man with the right hand side<00:12:24.610> of<00:12:24.790> these<00:12:24.940> but<00:12:25.180> okay<00:12:25.570> just<00:12:25.780> pull<00:12:25.930> those 00:12:26.070 --> 00:12:26.080 align:start position:0% side of these but okay just pull those 00:12:26.080 --> 00:12:27.600 align:start position:0% side of these but okay just pull those out<00:12:26.170> for<00:12:26.410> you<00:12:26.440> so<00:12:26.650> the<00:12:27.040> rule<00:12:27.190> can<00:12:27.340> be<00:12:27.400> a<00:12:27.430> little 00:12:27.600 --> 00:12:27.610 align:start position:0% out for you so the rule can be a little 00:12:27.610 --> 00:12:30.960 align:start position:0% out for you so the rule can be a little more<00:12:27.730> compact<00:12:28.060> and<00:12:28.270> readable<00:12:29.730> does<00:12:30.730> that<00:12:30.820> make 00:12:30.960 --> 00:12:30.970 align:start position:0% more compact and readable does that make 00:12:30.970 --> 00:12:31.790 align:start position:0% more compact and readable does that make sense 00:12:31.790 --> 00:12:31.800 align:start position:0% sense 00:12:31.800 --> 00:12:34.770 align:start position:0% sense okay<00:12:32.800> so<00:12:33.730> then<00:12:33.880> here's<00:12:34.240> some<00:12:34.420> aetherium 00:12:34.770 --> 00:12:34.780 align:start position:0% okay so then here's some aetherium 00:12:34.780 --> 00:12:37.020 align:start position:0% okay so then here's some aetherium Network<00:12:35.050> op<00:12:35.230> codes<00:12:35.530> so<00:12:35.860> S<00:12:36.040> load<00:12:36.250> and<00:12:36.400> store 00:12:37.020 --> 00:12:37.030 align:start position:0% Network op codes so S load and store 00:12:37.030 --> 00:12:39.300 align:start position:0% Network op codes so S load and store they're<00:12:37.420> the<00:12:37.630> network<00:12:38.140> storage<00:12:38.440> analogues<00:12:39.160> of 00:12:39.300 --> 00:12:39.310 align:start position:0% they're the network storage analogues of 00:12:39.310 --> 00:12:41.640 align:start position:0% they're the network storage analogues of the<00:12:39.370> EM<00:12:39.520> load<00:12:39.700> and<00:12:39.850> M<00:12:39.940> store<00:12:40.320> so<00:12:41.320> when<00:12:41.440> you<00:12:41.530> s 00:12:41.640 --> 00:12:41.650 align:start position:0% the EM load and M store so when you s 00:12:41.650 --> 00:12:43.890 align:start position:0% the EM load and M store so when you s load<00:12:41.950> at<00:12:42.190> an<00:12:42.340> index<00:12:42.730> there's<00:12:43.090> a<00:12:43.180> moon<00:12:43.420> stack<00:12:43.660> up 00:12:43.890 --> 00:12:43.900 align:start position:0% load at an index there's a moon stack up 00:12:43.900 --> 00:12:46.740 align:start position:0% load at an index there's a moon stack up and<00:12:44.160> the<00:12:45.160> current<00:12:45.490> executing<00:12:46.060> account<00:12:46.360> is<00:12:46.570> the 00:12:46.740 --> 00:12:46.750 align:start position:0% and the current executing account is the 00:12:46.750 --> 00:12:47.700 align:start position:0% and the current executing account is the one<00:12:46.870> with<00:12:47.050> this<00:12:47.170> ID 00:12:47.700 --> 00:12:47.710 align:start position:0% one with this ID 00:12:47.710 --> 00:12:50.520 align:start position:0% one with this ID well<00:12:48.130> first<00:12:48.460> we<00:12:48.670> match<00:12:48.910> an<00:12:49.300> account<00:12:50.260> so 00:12:50.520 --> 00:12:50.530 align:start position:0% well first we match an account so 00:12:50.530 --> 00:12:51.600 align:start position:0% well first we match an account so remember<00:12:50.800> there's<00:12:50.950> many<00:12:51.130> different<00:12:51.460> accounts 00:12:51.600 --> 00:12:51.610 align:start position:0% remember there's many different accounts 00:12:51.610 --> 00:12:52.920 align:start position:0% remember there's many different accounts because<00:12:51.850> that<00:12:52.000> multiplicity<00:12:52.510> star<00:12:52.720> if<00:12:52.810> we 00:12:52.920 --> 00:12:52.930 align:start position:0% because that multiplicity star if we 00:12:52.930 --> 00:12:54.300 align:start position:0% because that multiplicity star if we match<00:12:53.110> the<00:12:53.320> particular<00:12:53.530> one<00:12:53.860> that<00:12:54.040> matches 00:12:54.300 --> 00:12:54.310 align:start position:0% match the particular one that matches 00:12:54.310 --> 00:12:56.520 align:start position:0% match the particular one that matches the<00:12:54.640> account<00:12:54.940> of<00:12:55.120> the<00:12:55.230> the<00:12:56.230> one<00:12:56.350> that's 00:12:56.520 --> 00:12:56.530 align:start position:0% the account of the the one that's 00:12:56.530 --> 00:12:58.500 align:start position:0% the account of the the one that's currently<00:12:56.650> executing<00:12:57.100> and<00:12:57.550> then<00:12:57.940> we<00:12:58.060> look<00:12:58.300> in 00:12:58.500 --> 00:12:58.510 align:start position:0% currently executing and then we look in 00:12:58.510 --> 00:13:01.710 align:start position:0% currently executing and then we look in its<00:12:58.660> storage<00:12:59.430> for<00:13:00.430> this<00:13:00.760> index<00:13:01.210> essentially 00:13:01.710 --> 00:13:01.720 align:start position:0% its storage for this index essentially 00:13:01.720 --> 00:13:04.020 align:start position:0% its storage for this index essentially and<00:13:01.960> we<00:13:02.110> then<00:13:02.260> we<00:13:02.350> push<00:13:02.590> the<00:13:03.070> value<00:13:03.280> up<00:13:03.820> right 00:13:04.020 --> 00:13:04.030 align:start position:0% and we then we push the value up right 00:13:04.030 --> 00:13:05.220 align:start position:0% and we then we push the value up right here<00:13:04.180> and<00:13:04.390> the<00:13:04.450> storage<00:13:04.690> and<00:13:04.900> the<00:13:04.960> account 00:13:05.220 --> 00:13:05.230 align:start position:0% here and the storage and the account 00:13:05.230 --> 00:13:06.660 align:start position:0% here and the storage and the account don't<00:13:05.380> change<00:13:05.710> we<00:13:05.860> just<00:13:05.890> push<00:13:06.190> the<00:13:06.310> value<00:13:06.520> up 00:13:06.660 --> 00:13:06.670 align:start position:0% don't change we just push the value up 00:13:06.670 --> 00:13:08.420 align:start position:0% don't change we just push the value up there 00:13:08.420 --> 00:13:08.430 align:start position:0% there 00:13:08.430 --> 00:13:10.650 align:start position:0% there yeah<00:13:09.430> so<00:13:09.550> it's<00:13:09.670> kind<00:13:09.820> of<00:13:09.850> a<00:13:09.910> lot<00:13:10.060> going<00:13:10.270> on<00:13:10.420> but 00:13:10.650 --> 00:13:10.660 align:start position:0% yeah so it's kind of a lot going on but 00:13:10.660 --> 00:13:12.930 align:start position:0% yeah so it's kind of a lot going on but once<00:13:10.870> again<00:13:11.170> this<00:13:11.650> dot<00:13:11.890> dot<00:13:12.100> is<00:13:12.490> not<00:13:12.730> me 00:13:12.930 --> 00:13:12.940 align:start position:0% once again this dot dot is not me 00:13:12.940 --> 00:13:14.310 align:start position:0% once again this dot dot is not me alighting<00:13:13.330> details<00:13:13.660> this<00:13:13.840> is<00:13:13.900> actually 00:13:14.310 --> 00:13:14.320 align:start position:0% alighting details this is actually 00:13:14.320 --> 00:13:16.550 align:start position:0% alighting details this is actually verbatim<00:13:14.740> the<00:13:14.830> K<00:13:15.010> rule<00:13:15.280> for<00:13:15.490> this<00:13:15.580> operator<00:13:16.060> so 00:13:16.550 --> 00:13:16.560 align:start position:0% verbatim the K rule for this operator so 00:13:16.560 --> 00:13:18.850 align:start position:0% verbatim the K rule for this operator so once<00:13:17.560> again<00:13:17.650> K<00:13:17.950> is<00:13:18.070> kind<00:13:18.280> of<00:13:18.310> being<00:13:18.490> our 00:13:18.850 --> 00:13:18.860 align:start position:0% once again K is kind of being our 00:13:18.860 --> 00:13:20.860 align:start position:0% once again K is kind of being our allowing<00:13:19.280> us<00:13:19.370> to<00:13:19.400> elide<00:13:19.760> lots<00:13:20.030> of<00:13:20.120> details<00:13:20.480> of 00:13:20.860 --> 00:13:20.870 align:start position:0% allowing us to elide lots of details of 00:13:20.870 --> 00:13:22.750 align:start position:0% allowing us to elide lots of details of the<00:13:21.260> configuration<00:13:21.830> that<00:13:21.860> we<00:13:22.040> don't<00:13:22.220> need<00:13:22.400> to 00:13:22.750 --> 00:13:22.760 align:start position:0% the configuration that we don't need to 00:13:22.760 --> 00:13:26.140 align:start position:0% the configuration that we don't need to mention<00:13:23.330> for<00:13:23.480> this<00:13:23.570> particular<00:13:23.840> rule<00:13:24.760> s<00:13:25.760> store 00:13:26.140 --> 00:13:26.150 align:start position:0% mention for this particular rule s store 00:13:26.150 --> 00:13:29.530 align:start position:0% mention for this particular rule s store right<00:13:26.570> here<00:13:27.670> it<00:13:28.670> has<00:13:28.820> once<00:13:29.120> again<00:13:29.210> to 00:13:29.530 --> 00:13:29.540 align:start position:0% right here it has once again to 00:13:29.540 --> 00:13:31.150 align:start position:0% right here it has once again to transition<00:13:30.050> arrows<00:13:30.290> one<00:13:30.530> that's<00:13:30.770> going<00:13:31.040> on 00:13:31.150 --> 00:13:31.160 align:start position:0% transition arrows one that's going on 00:13:31.160 --> 00:13:33.220 align:start position:0% transition arrows one that's going on within<00:13:31.850> the<00:13:32.000> account<00:13:32.390> and<00:13:32.600> one<00:13:32.810> that's<00:13:32.990> going 00:13:33.220 --> 00:13:33.230 align:start position:0% within the account and one that's going 00:13:33.230 --> 00:13:35.680 align:start position:0% within the account and one that's going on<00:13:33.380> in<00:13:34.130> the<00:13:34.280> case<00:13:34.490> L<00:13:34.730> and<00:13:34.970> then<00:13:35.570> we're 00:13:35.680 --> 00:13:35.690 align:start position:0% on in the case L and then we're 00:13:35.690 --> 00:13:37.470 align:start position:0% on in the case L and then we're rewriting<00:13:36.050> the<00:13:36.290> S<00:13:36.410> store<00:13:36.710> to<00:13:36.890> the<00:13:36.980> empty 00:13:37.470 --> 00:13:37.480 align:start position:0% rewriting the S store to the empty 00:13:37.480 --> 00:13:39.130 align:start position:0% rewriting the S store to the empty computation<00:13:38.480> essentially<00:13:38.840> so<00:13:38.930> we're<00:13:39.020> saying 00:13:39.130 --> 00:13:39.140 align:start position:0% computation essentially so we're saying 00:13:39.140 --> 00:13:40.900 align:start position:0% computation essentially so we're saying that<00:13:39.200> the<00:13:39.350> computation<00:13:39.830> is<00:13:39.920> done<00:13:39.950> we<00:13:40.760> once 00:13:40.900 --> 00:13:40.910 align:start position:0% that the computation is done we once 00:13:40.910 --> 00:13:42.970 align:start position:0% that the computation is done we once again<00:13:40.970> match<00:13:41.300> on<00:13:41.510> the<00:13:41.630> account<00:13:41.870> ID<00:13:42.080> grab<00:13:42.860> the 00:13:42.970 --> 00:13:42.980 align:start position:0% again match on the account ID grab the 00:13:42.980 --> 00:13:45.190 align:start position:0% again match on the account ID grab the account<00:13:43.280> take<00:13:43.820> the<00:13:43.940> storage<00:13:44.330> update<00:13:45.080> the 00:13:45.190 --> 00:13:45.200 align:start position:0% account take the storage update the 00:13:45.200 --> 00:13:46.870 align:start position:0% account take the storage update the index<00:13:45.380> and<00:13:45.710> the<00:13:45.770> storage<00:13:46.010> with<00:13:46.250> the<00:13:46.280> value<00:13:46.700> and 00:13:46.870 --> 00:13:46.880 align:start position:0% index and the storage with the value and 00:13:46.880 --> 00:13:48.580 align:start position:0% index and the storage with the value and then<00:13:47.300> there's<00:13:47.450> this<00:13:47.690> side<00:13:47.930> condition<00:13:48.380> here 00:13:48.580 --> 00:13:48.590 align:start position:0% then there's this side condition here 00:13:48.590 --> 00:13:50.220 align:start position:0% then there's this side condition here because<00:13:48.830> there's<00:13:48.980> a<00:13:49.010> bunch<00:13:49.130> of<00:13:49.250> different 00:13:50.220 --> 00:13:50.230 align:start position:0% because there's a bunch of different 00:13:50.230 --> 00:13:52.840 align:start position:0% because there's a bunch of different semantics<00:13:51.230> whether<00:13:51.890> the<00:13:52.160> key<00:13:52.400> is<00:13:52.520> already<00:13:52.790> in 00:13:52.840 --> 00:13:52.850 align:start position:0% semantics whether the key is already in 00:13:52.850 --> 00:13:54.220 align:start position:0% semantics whether the key is already in the<00:13:52.940> storage<00:13:53.270> or<00:13:53.390> not<00:13:53.510> in<00:13:53.600> the<00:13:53.690> storage<00:13:54.110> or 00:13:54.220 --> 00:13:54.230 align:start position:0% the storage or not in the storage or 00:13:54.230 --> 00:14:06.820 align:start position:0% the storage or not in the storage or wasn't<00:13:54.560> empty<00:13:54.650> or<00:13:54.830> it<00:13:54.890> wasn't<00:13:55.220> yeah<00:14:05.350> so<00:14:06.350> this 00:14:06.820 --> 00:14:06.830 align:start position:0% wasn't empty or it wasn't yeah so this 00:14:06.830 --> 00:14:09.190 align:start position:0% wasn't empty or it wasn't yeah so this this<00:14:07.430> this<00:14:08.090> arrow<00:14:08.360> right<00:14:08.600> here<00:14:08.630> is<00:14:09.020> actually 00:14:09.190 --> 00:14:09.200 align:start position:0% this this arrow right here is actually 00:14:09.200 --> 00:14:11.290 align:start position:0% this this arrow right here is actually map<00:14:09.680> update<00:14:10.130> and<00:14:10.310> it<00:14:10.370> ships<00:14:10.640> with<00:14:10.730> K<00:14:11.030> as<00:14:11.240> a 00:14:11.290 --> 00:14:11.300 align:start position:0% map update and it ships with K as a 00:14:11.300 --> 00:14:14.200 align:start position:0% map update and it ships with K as a built<00:14:11.780> in<00:14:11.960> from<00:14:12.170> the<00:14:12.260> preload<00:14:12.880> this<00:14:13.880> right 00:14:14.200 --> 00:14:14.210 align:start position:0% built in from the preload this right 00:14:14.210 --> 00:14:16.870 align:start position:0% built in from the preload this right here<00:14:14.510> is<00:14:14.660> actually<00:14:15.430> specific<00:14:16.430> to<00:14:16.490> the<00:14:16.580> evm 00:14:16.870 --> 00:14:16.880 align:start position:0% here is actually specific to the evm 00:14:16.880 --> 00:14:18.340 align:start position:0% here is actually specific to the evm semantics<00:14:17.450> because<00:14:17.750> it<00:14:17.870> has<00:14:17.990> to<00:14:18.110> write<00:14:18.320> a 00:14:18.340 --> 00:14:18.350 align:start position:0% semantics because it has to write a 00:14:18.350 --> 00:14:20.230 align:start position:0% semantics because it has to write a whole<00:14:18.620> word<00:14:18.860> stack<00:14:19.190> at<00:14:19.400> a<00:14:19.460> time<00:14:19.700> so<00:14:19.970> it<00:14:20.060> writes 00:14:20.230 --> 00:14:20.240 align:start position:0% whole word stack at a time so it writes 00:14:20.240 --> 00:14:21.370 align:start position:0% whole word stack at a time so it writes the<00:14:20.420> first<00:14:20.600> element<00:14:20.960> then<00:14:21.050> the<00:14:21.110> second 00:14:21.370 --> 00:14:21.380 align:start position:0% the first element then the second 00:14:21.380 --> 00:14:22.750 align:start position:0% the first element then the second element<00:14:21.410> so<00:14:21.650> this<00:14:21.740> D<00:14:21.920> sugars<00:14:22.250> to<00:14:22.400> a<00:14:22.430> sequence 00:14:22.750 --> 00:14:22.760 align:start position:0% element so this D sugars to a sequence 00:14:22.760 --> 00:14:26.650 align:start position:0% element so this D sugars to a sequence of<00:14:23.000> 32<00:14:23.510> of<00:14:23.840> the<00:14:24.620> map<00:14:24.860> update<00:14:25.250> operations<00:14:25.850> does 00:14:26.650 --> 00:14:26.660 align:start position:0% of 32 of the map update operations does 00:14:26.660 --> 00:14:29.890 align:start position:0% of 32 of the map update operations does that<00:14:26.750> make<00:14:26.840> sense<00:14:27.400> I<00:14:28.400> guess<00:14:29.210> I<00:14:29.360> could<00:14:29.570> give<00:14:29.870> it 00:14:29.890 --> 00:14:29.900 align:start position:0% that make sense I guess I could give it 00:14:29.900 --> 00:14:32.320 align:start position:0% that make sense I guess I could give it some<00:14:30.110> nicer<00:14:30.410> syntax<00:14:30.620> but<00:14:31.100> I<00:14:31.520> don't<00:14:32.150> know<00:14:32.210> that 00:14:32.320 --> 00:14:32.330 align:start position:0% some nicer syntax but I don't know that 00:14:32.330 --> 00:14:33.700 align:start position:0% some nicer syntax but I don't know that was<00:14:32.420> an<00:14:32.510> early<00:14:32.630> design<00:14:32.870> decision<00:14:33.410> then<00:14:33.590> it's 00:14:33.700 --> 00:14:33.710 align:start position:0% was an early design decision then it's 00:14:33.710 --> 00:14:41.710 align:start position:0% was an early design decision then it's hard<00:14:33.890> to<00:14:33.980> change<00:14:34.190> later<00:14:36.700> yeah<00:14:38.530> ok<00:14:40.150> ok<00:14:41.150> so<00:14:41.600> I 00:14:41.710 --> 00:14:41.720 align:start position:0% hard to change later yeah ok ok so I 00:14:41.720 --> 00:14:42.790 align:start position:0% hard to change later yeah ok ok so I just<00:14:41.900> wanted<00:14:42.050> to<00:14:42.140> show<00:14:42.230> an<00:14:42.320> example<00:14:42.410> of<00:14:42.740> a 00:14:42.790 --> 00:14:42.800 align:start position:0% just wanted to show an example of a 00:14:42.800 --> 00:14:44.260 align:start position:0% just wanted to show an example of a bigger<00:14:42.980> Network<00:14:43.310> hop<00:14:43.460> code<00:14:43.730> so<00:14:43.910> this<00:14:44.030> is<00:14:44.150> the 00:14:44.260 --> 00:14:44.270 align:start position:0% bigger Network hop code so this is the 00:14:44.270 --> 00:14:45.610 align:start position:0% bigger Network hop code so this is the call-off<00:14:44.480> code<00:14:44.840> it's<00:14:45.050> running<00:14:45.290> off<00:14:45.410> the<00:14:45.440> edge 00:14:45.610 --> 00:14:45.620 align:start position:0% call-off code it's running off the edge 00:14:45.620 --> 00:14:47.530 align:start position:0% call-off code it's running off the edge of<00:14:45.740> the<00:14:45.800> screen<00:14:46.070> here<00:14:46.250> but<00:14:47.000> basically<00:14:47.330> we 00:14:47.530 --> 00:14:47.540 align:start position:0% of the screen here but basically we 00:14:47.540 --> 00:14:50.440 align:start position:0% of the screen here but basically we define<00:14:47.840> a<00:14:47.870> bunch<00:14:48.110> of<00:14:48.200> internal<00:14:49.300> operators<00:14:50.300> to 00:14:50.440 --> 00:14:50.450 align:start position:0% define a bunch of internal operators to 00:14:50.450 --> 00:14:51.670 align:start position:0% define a bunch of internal operators to help<00:14:50.630> with<00:14:50.750> the<00:14:50.840> call<00:14:50.990> opcode<00:14:51.380> and<00:14:51.410> that's 00:14:51.670 --> 00:14:51.680 align:start position:0% help with the call opcode and that's 00:14:51.680 --> 00:14:52.990 align:start position:0% help with the call opcode and that's pretty<00:14:52.070> straightforward<00:14:52.310> to<00:14:52.580> do<00:14:52.700> but<00:14:52.880> then 00:14:52.990 --> 00:14:53.000 align:start position:0% pretty straightforward to do but then 00:14:53.000 --> 00:14:55.450 align:start position:0% pretty straightforward to do but then these<00:14:53.180> internals<00:14:53.810> can<00:14:54.020> be<00:14:54.110> reused<00:14:54.500> for<00:14:55.400> the 00:14:55.450 --> 00:14:55.460 align:start position:0% these internals can be reused for the 00:14:55.460 --> 00:14:57.700 align:start position:0% these internals can be reused for the delegate<00:14:55.880> call<00:14:56.090> opcode<00:14:56.540> or<00:14:56.780> probably<00:14:57.470> for<00:14:57.620> the 00:14:57.700 --> 00:14:57.710 align:start position:0% delegate call opcode or probably for the 00:14:57.710 --> 00:15:01.090 align:start position:0% delegate call opcode or probably for the static<00:14:58.010> call<00:14:58.220> as<00:14:58.790> well<00:14:59.000> I'm<00:14:59.750> not<00:14:59.900> sure<00:14:59.960> I'm<00:15:00.290> it 00:15:01.090 --> 00:15:01.100 align:start position:0% static call as well I'm not sure I'm it 00:15:01.100 --> 00:15:05.170 align:start position:0% static call as well I'm not sure I'm it was<00:15:01.400> awhile<00:15:01.490> since<00:15:01.730> I<00:15:01.850> wrote<00:15:02.000> this<00:15:02.090> code<00:15:04.060> ok 00:15:05.170 --> 00:15:05.180 align:start position:0% was awhile since I wrote this code ok 00:15:05.180 --> 00:15:06.790 align:start position:0% was awhile since I wrote this code ok so<00:15:05.300> gas<00:15:05.600> calculation<00:15:06.200> I'm<00:15:06.380> gonna<00:15:06.530> run<00:15:06.680> through 00:15:06.790 --> 00:15:06.800 align:start position:0% so gas calculation I'm gonna run through 00:15:06.800 --> 00:15:08.020 align:start position:0% so gas calculation I'm gonna run through this<00:15:06.950> super<00:15:07.160> quick<00:15:07.400> because<00:15:07.580> it<00:15:07.730> looks<00:15:07.880> like 00:15:08.020 --> 00:15:08.030 align:start position:0% this super quick because it looks like 00:15:08.030 --> 00:15:09.220 align:start position:0% this super quick because it looks like I'm<00:15:08.150> running<00:15:08.300> low<00:15:08.480> on<00:15:08.510> time<00:15:08.630> and<00:15:08.990> I<00:15:09.020> want<00:15:09.170> to 00:15:09.220 --> 00:15:09.230 align:start position:0% I'm running low on time and I want to 00:15:09.230 --> 00:15:12.490 align:start position:0% I'm running low on time and I want to get<00:15:09.320> to<00:15:09.380> the<00:15:09.470> verification<00:15:09.710> part<00:15:11.500> the 00:15:12.490 --> 00:15:12.500 align:start position:0% get to the verification part the 00:15:12.500 --> 00:15:14.260 align:start position:0% get to the verification part the intrinsic<00:15:13.070> gas<00:15:13.310> calculation<00:15:13.880> we<00:15:13.970> tried<00:15:14.150> to 00:15:14.260 --> 00:15:14.270 align:start position:0% intrinsic gas calculation we tried to 00:15:14.270 --> 00:15:15.640 align:start position:0% intrinsic gas calculation we tried to mirror<00:15:14.510> as<00:15:14.570> much<00:15:14.720> as<00:15:14.840> possible<00:15:15.020> to<00:15:15.320> style<00:15:15.530> of 00:15:15.640 --> 00:15:15.650 align:start position:0% mirror as much as possible to style of 00:15:15.650 --> 00:15:17.500 align:start position:0% mirror as much as possible to style of the<00:15:15.740> yellow<00:15:15.920> paper<00:15:16.210> so<00:15:17.210> we<00:15:17.300> have<00:15:17.420> this 00:15:17.500 --> 00:15:17.510 align:start position:0% the yellow paper so we have this 00:15:17.510 --> 00:15:19.720 align:start position:0% the yellow paper so we have this function<00:15:17.690> gas<00:15:17.990> exact<00:15:18.410> which<00:15:19.010> is<00:15:19.040> parametric 00:15:19.720 --> 00:15:19.730 align:start position:0% function gas exact which is parametric 00:15:19.730 --> 00:15:21.700 align:start position:0% function gas exact which is parametric in<00:15:19.910> the<00:15:20.030> fee<00:15:20.210> schedule<00:15:20.290> that<00:15:21.290> you<00:15:21.530> are 00:15:21.700 --> 00:15:21.710 align:start position:0% in the fee schedule that you are 00:15:21.710 --> 00:15:22.960 align:start position:0% in the fee schedule that you are executing<00:15:22.070> with<00:15:22.400> so<00:15:22.610> you<00:15:22.670> can<00:15:22.790> specify 00:15:22.960 --> 00:15:22.970 align:start position:0% executing with so you can specify 00:15:22.970 --> 00:15:24.880 align:start position:0% executing with so you can specify different<00:15:23.420> fee<00:15:23.540> schedules<00:15:23.990> for<00:15:24.530> example<00:15:24.800> I'll 00:15:24.880 --> 00:15:24.890 align:start position:0% different fee schedules for example I'll 00:15:24.890 --> 00:15:27.730 align:start position:0% different fee schedules for example I'll talk<00:15:25.010> about<00:15:25.070> that<00:15:25.370> on<00:15:25.490> the<00:15:25.550> next<00:15:25.670> slide<00:15:26.740> so 00:15:27.730 --> 00:15:27.740 align:start position:0% talk about that on the next slide so 00:15:27.740 --> 00:15:30.490 align:start position:0% talk about that on the next slide so given<00:15:28.250> the<00:15:28.340> schedule<00:15:28.730> and<00:15:28.940> the<00:15:29.060> opcode<00:15:29.540> call 00:15:30.490 --> 00:15:30.500 align:start position:0% given the schedule and the opcode call 00:15:30.500 --> 00:15:32.560 align:start position:0% given the schedule and the opcode call the<00:15:30.920> CS<00:15:31.730> store 00:15:32.560 --> 00:15:32.570 align:start position:0% the CS store 00:15:32.570 --> 00:15:34.600 align:start position:0% the CS store gasps<00:15:32.930> function<00:15:33.350> from<00:15:33.620> the<00:15:33.800> yellow<00:15:34.430> paper 00:15:34.600 --> 00:15:34.610 align:start position:0% gasps function from the yellow paper 00:15:34.610 --> 00:15:36.340 align:start position:0% gasps function from the yellow paper essentially<00:15:35.030> and<00:15:35.330> then<00:15:35.750> this<00:15:35.990> we're<00:15:36.200> going<00:15:36.290> to 00:15:36.340 --> 00:15:36.350 align:start position:0% essentially and then this we're going to 00:15:36.350 --> 00:15:37.660 align:start position:0% essentially and then this we're going to declare<00:15:36.620> as<00:15:36.710> a<00:15:36.770> function<00:15:37.160> which<00:15:37.310> means<00:15:37.460> we're 00:15:37.660 --> 00:15:37.670 align:start position:0% declare as a function which means we're 00:15:37.670 --> 00:15:39.310 align:start position:0% declare as a function which means we're not<00:15:37.760> allowed<00:15:38.000> to<00:15:38.030> depend<00:15:38.420> on<00:15:38.570> any<00:15:38.780> part<00:15:39.110> of<00:15:39.170> the 00:15:39.310 --> 00:15:39.320 align:start position:0% not allowed to depend on any part of the 00:15:39.320 --> 00:15:41.530 align:start position:0% not allowed to depend on any part of the external<00:15:39.650> configuration<00:15:40.370> so<00:15:40.850> this<00:15:40.970> gas<00:15:41.180> exec 00:15:41.530 --> 00:15:41.540 align:start position:0% external configuration so this gas exec 00:15:41.540 --> 00:15:43.000 align:start position:0% external configuration so this gas exec operator<00:15:41.960> is<00:15:42.050> gonna<00:15:42.200> grab<00:15:42.470> all<00:15:42.620> the<00:15:42.770> relevant 00:15:43.000 --> 00:15:43.010 align:start position:0% operator is gonna grab all the relevant 00:15:43.010 --> 00:15:45.250 align:start position:0% operator is gonna grab all the relevant parts<00:15:43.340> of<00:15:43.460> the<00:15:43.520> state<00:15:43.790> that<00:15:44.060> C<00:15:44.630> s<00:15:44.750> store<00:15:44.990> needs 00:15:45.250 --> 00:15:45.260 align:start position:0% parts of the state that C s store needs 00:15:45.260 --> 00:15:47.950 align:start position:0% parts of the state that C s store needs to<00:15:45.590> calculate<00:15:46.040> its<00:15:46.160> value<00:15:46.550> and<00:15:46.820> give<00:15:47.060> it<00:15:47.210> gives 00:15:47.950 --> 00:15:47.960 align:start position:0% to calculate its value and give it gives 00:15:47.960 --> 00:15:50.830 align:start position:0% to calculate its value and give it gives you<00:15:48.140> a<00:15:48.170> story<00:15:48.470> of<00:15:48.590> those<00:15:48.740> values<00:15:49.160> as<00:15:49.310> arguments 00:15:50.830 --> 00:15:50.840 align:start position:0% you a story of those values as arguments 00:15:50.840 --> 00:15:52.780 align:start position:0% you a story of those values as arguments so<00:15:51.170> the<00:15:51.530> definition<00:15:51.680> of<00:15:52.070> C<00:15:52.190> F<00:15:52.310> store<00:15:52.520> is<00:15:52.610> right 00:15:52.780 --> 00:15:52.790 align:start position:0% so the definition of C F store is right 00:15:52.790 --> 00:15:55.360 align:start position:0% so the definition of C F store is right here<00:15:53.260> once<00:15:54.260> again<00:15:54.440> it's<00:15:54.590> a<00:15:54.650> function<00:15:55.070> takes 00:15:55.360 --> 00:15:55.370 align:start position:0% here once again it's a function takes 00:15:55.370 --> 00:15:56.650 align:start position:0% here once again it's a function takes three<00:15:55.520> arguments<00:15:55.760> produces<00:15:56.240> an<00:15:56.330> int<00:15:56.480> and 00:15:56.650 --> 00:15:56.660 align:start position:0% three arguments produces an int and 00:15:56.660 --> 00:15:58.570 align:start position:0% three arguments produces an int and notice<00:15:57.500> it<00:15:57.590> doesn't<00:15:57.740> depend<00:15:58.010> on<00:15:58.130> any<00:15:58.310> part<00:15:58.550> of 00:15:58.570 --> 00:15:58.580 align:start position:0% notice it doesn't depend on any part of 00:15:58.580 --> 00:16:00.550 align:start position:0% notice it doesn't depend on any part of the<00:15:58.670> configuration<00:15:58.910> so<00:15:59.570> you<00:16:00.170> know<00:16:00.260> you<00:16:00.320> check 00:16:00.550 --> 00:16:00.560 align:start position:0% the configuration so you know you check 00:16:00.560 --> 00:16:03.310 align:start position:0% the configuration so you know you check is<00:16:00.830> the<00:16:01.100> value<00:16:01.340> not<00:16:01.490> equal<00:16:01.730> to<00:16:01.820> zero<00:16:02.060> and<00:16:02.450> the 00:16:03.310 --> 00:16:03.320 align:start position:0% is the value not equal to zero and the 00:16:03.320 --> 00:16:05.260 align:start position:0% is the value not equal to zero and the old<00:16:03.470> one<00:16:03.710> is<00:16:03.830> not<00:16:03.980> equal<00:16:04.100> to<00:16:04.310> zero<00:16:04.520> so<00:16:04.790> this<00:16:05.090> has 00:16:05.260 --> 00:16:05.270 align:start position:0% old one is not equal to zero so this has 00:16:05.270 --> 00:16:07.450 align:start position:0% old one is not equal to zero so this has to<00:16:05.390> do<00:16:05.510> with<00:16:05.600> whether<00:16:05.780> you're<00:16:06.100> setting<00:16:07.100> it<00:16:07.310> for 00:16:07.450 --> 00:16:07.460 align:start position:0% to do with whether you're setting it for 00:16:07.460 --> 00:16:09.280 align:start position:0% to do with whether you're setting it for the<00:16:07.520> setting<00:16:08.090> or<00:16:08.300> resetting<00:16:08.660> it<00:16:08.840> essentially 00:16:09.280 --> 00:16:09.290 align:start position:0% the setting or resetting it essentially 00:16:09.290 --> 00:16:10.780 align:start position:0% the setting or resetting it essentially and<00:16:09.470> then<00:16:09.800> these<00:16:09.950> are<00:16:10.010> different<00:16:10.400> schedule 00:16:10.780 --> 00:16:10.790 align:start position:0% and then these are different schedule 00:16:10.790 --> 00:16:12.400 align:start position:0% and then these are different schedule constants<00:16:11.330> so<00:16:11.540> they're<00:16:11.690> parametric<00:16:12.230> in<00:16:12.350> the 00:16:12.400 --> 00:16:12.410 align:start position:0% constants so they're parametric in the 00:16:12.410 --> 00:16:14.710 align:start position:0% constants so they're parametric in the particular<00:16:12.650> schedule<00:16:13.420> and<00:16:14.420> then<00:16:14.540> these<00:16:14.660> are 00:16:14.710 --> 00:16:14.720 align:start position:0% particular schedule and then these are 00:16:14.720 --> 00:16:16.600 align:start position:0% particular schedule and then these are all<00:16:15.260> sorts<00:16:15.530> of<00:16:15.560> other<00:16:15.740> cost<00:16:16.010> functions<00:16:16.490> that 00:16:16.600 --> 00:16:16.610 align:start position:0% all sorts of other cost functions that 00:16:16.610 --> 00:16:17.950 align:start position:0% all sorts of other cost functions that we've<00:16:16.760> implemented<00:16:17.060> these<00:16:17.570> mirror<00:16:17.840> exactly 00:16:17.950 --> 00:16:17.960 align:start position:0% we've implemented these mirror exactly 00:16:17.960 --> 00:16:20.560 align:start position:0% we've implemented these mirror exactly what<00:16:18.590> goes<00:16:18.710> on<00:16:18.860> in<00:16:18.980> the<00:16:19.040> yellow<00:16:19.220> paper<00:16:19.570> so 00:16:20.560 --> 00:16:20.570 align:start position:0% what goes on in the yellow paper so 00:16:20.570 --> 00:16:21.940 align:start position:0% what goes on in the yellow paper so really<00:16:20.810> you<00:16:20.960> can<00:16:21.080> read<00:16:21.290> this<00:16:21.500> instead<00:16:21.800> of<00:16:21.860> the 00:16:21.940 --> 00:16:21.950 align:start position:0% really you can read this instead of the 00:16:21.950 --> 00:16:22.990 align:start position:0% really you can read this instead of the yellow<00:16:22.070> paper<00:16:22.310> if<00:16:22.490> you<00:16:22.550> don't<00:16:22.730> like<00:16:22.850> reading 00:16:22.990 --> 00:16:23.000 align:start position:0% yellow paper if you don't like reading 00:16:23.000 --> 00:16:24.820 align:start position:0% yellow paper if you don't like reading yellow<00:16:23.330> paper<00:16:23.510> and<00:16:24.110> it<00:16:24.440> has<00:16:24.560> a<00:16:24.590> lot<00:16:24.800> more 00:16:24.820 --> 00:16:24.830 align:start position:0% yellow paper and it has a lot more 00:16:24.830 --> 00:16:27.270 align:start position:0% yellow paper and it has a lot more explanatory<00:16:25.580> text<00:16:25.730> around<00:16:25.970> it<00:16:26.270> in<00:16:26.930> our 00:16:27.270 --> 00:16:27.280 align:start position:0% explanatory text around it in our 00:16:27.280 --> 00:16:31.300 align:start position:0% explanatory text around it in our repository<00:16:28.280> online<00:16:30.130> here's<00:16:31.130> how<00:16:31.250> we 00:16:31.300 --> 00:16:31.310 align:start position:0% repository online here's how we 00:16:31.310 --> 00:16:33.670 align:start position:0% repository online here's how we implement<00:16:31.730> the<00:16:31.850> schedules<00:16:32.450> so<00:16:33.020> we<00:16:33.140> say<00:16:33.350> that 00:16:33.670 --> 00:16:33.680 align:start position:0% implement the schedules so we say that 00:16:33.680 --> 00:16:35.950 align:start position:0% implement the schedules so we say that you<00:16:33.920> can<00:16:34.100> produce<00:16:34.280> an<00:16:34.610> integer<00:16:35.060> if<00:16:35.420> you<00:16:35.810> have<00:16:35.930> a 00:16:35.950 --> 00:16:35.960 align:start position:0% you can produce an integer if you have a 00:16:35.960 --> 00:16:37.240 align:start position:0% you can produce an integer if you have a schedule<00:16:36.200> constant<00:16:36.740> and<00:16:36.830> in<00:16:36.920> these<00:16:37.040> brackets 00:16:37.240 --> 00:16:37.250 align:start position:0% schedule constant and in these brackets 00:16:37.250 --> 00:16:39.790 align:start position:0% schedule constant and in these brackets in<00:16:37.610> a<00:16:37.700> particular<00:16:37.910> schedule<00:16:38.270> and<00:16:38.780> then<00:16:39.380> here 00:16:39.790 --> 00:16:39.800 align:start position:0% in a particular schedule and then here 00:16:39.800 --> 00:16:41.500 align:start position:0% in a particular schedule and then here are<00:16:40.010> some<00:16:40.040> examples<00:16:40.640> of<00:16:40.700> schedule<00:16:41.060> constants 00:16:41.500 --> 00:16:41.510 align:start position:0% are some examples of schedule constants 00:16:41.510 --> 00:16:43.480 align:start position:0% are some examples of schedule constants once<00:16:41.690> again<00:16:41.900> from<00:16:42.050> the<00:16:42.140> yellow<00:16:42.350> paper<00:16:42.500> g0d 00:16:43.480 --> 00:16:43.490 align:start position:0% once again from the yellow paper g0d 00:16:43.490 --> 00:16:47.350 align:start position:0% once again from the yellow paper g0d base<00:16:43.820> g<00:16:44.480> very<00:16:44.600> low<00:16:45.820> here's<00:16:46.820> a<00:16:46.880> schedule<00:16:47.120> the 00:16:47.350 --> 00:16:47.360 align:start position:0% base g very low here's a schedule the 00:16:47.360 --> 00:16:49.210 align:start position:0% base g very low here's a schedule the default<00:16:47.690> schedule<00:16:48.110> you<00:16:48.410> know<00:16:48.500> it<00:16:48.620> sets<00:16:48.800> G<00:16:48.980> zero 00:16:49.210 --> 00:16:49.220 align:start position:0% default schedule you know it sets G zero 00:16:49.220 --> 00:16:51.730 align:start position:0% default schedule you know it sets G zero to<00:16:49.310> zero<00:16:49.550> do<00:16:49.760> you<00:16:49.850> base<00:16:50.000> the<00:16:50.150> to<00:16:50.300> e<00:16:50.540> I<00:16:51.110> p150 00:16:51.730 --> 00:16:51.740 align:start position:0% to zero do you base the to e I p150 00:16:51.740 --> 00:16:54.880 align:start position:0% to zero do you base the to e I p150 schedule<00:16:52.370> G<00:16:53.150> balance<00:16:53.570> gets<00:16:53.930> changed<00:16:54.200> to<00:16:54.320> 400 00:16:54.880 --> 00:16:54.890 align:start position:0% schedule G balance gets changed to 400 00:16:54.890 --> 00:16:57.250 align:start position:0% schedule G balance gets changed to 400 over<00:16:55.130> the<00:16:55.540> schedule<00:16:56.540> that<00:16:56.720> come<00:16:56.900> before<00:16:57.080> that 00:16:57.250 --> 00:16:57.260 align:start position:0% over the schedule that come before that 00:16:57.260 --> 00:16:58.810 align:start position:0% over the schedule that come before that was<00:16:57.530> like<00:16:57.650> homestead<00:16:58.190> or<00:16:58.340> something<00:16:58.610> I<00:16:58.670> don't 00:16:58.810 --> 00:16:58.820 align:start position:0% was like homestead or something I don't 00:16:58.820 --> 00:16:59.910 align:start position:0% was like homestead or something I don't quite<00:16:58.910> remember 00:16:59.910 --> 00:16:59.920 align:start position:0% quite remember 00:16:59.920 --> 00:17:03.160 align:start position:0% quite remember so<00:17:00.920> you<00:17:00.980> just<00:17:01.130> update<00:17:01.550> for<00:17:02.420> each<00:17:02.510> new<00:17:02.780> schedule 00:17:03.160 --> 00:17:03.170 align:start position:0% so you just update for each new schedule 00:17:03.170 --> 00:17:04.569 align:start position:0% so you just update for each new schedule change<00:17:03.410> you<00:17:03.560> just<00:17:03.590> update<00:17:04.100> the<00:17:04.130> schedule 00:17:04.569 --> 00:17:04.579 align:start position:0% change you just update the schedule 00:17:04.579 --> 00:17:05.800 align:start position:0% change you just update the schedule constants<00:17:05.060> for<00:17:05.180> that<00:17:05.329> particular<00:17:05.510> schedule 00:17:05.800 --> 00:17:05.810 align:start position:0% constants for that particular schedule 00:17:05.810 --> 00:17:07.360 align:start position:0% constants for that particular schedule so<00:17:06.320> there's<00:17:06.439> actually<00:17:06.680> a<00:17:06.709> command<00:17:06.949> line<00:17:07.100> flag 00:17:07.360 --> 00:17:07.370 align:start position:0% so there's actually a command line flag 00:17:07.370 --> 00:17:09.429 align:start position:0% so there's actually a command line flag you<00:17:07.550> can<00:17:07.610> give<00:17:07.820> the<00:17:07.910> semantics<00:17:08.390> to<00:17:09.170> tell<00:17:09.320> it 00:17:09.429 --> 00:17:09.439 align:start position:0% you can give the semantics to tell it 00:17:09.439 --> 00:17:11.980 align:start position:0% you can give the semantics to tell it which<00:17:09.530> schedule<00:17:09.860> to<00:17:09.949> execute<00:17:10.310> with<00:17:10.480> okay<00:17:11.480> so 00:17:11.980 --> 00:17:11.990 align:start position:0% which schedule to execute with okay so 00:17:11.990 --> 00:17:12.790 align:start position:0% which schedule to execute with okay so now<00:17:12.079> I'm<00:17:12.140> gonna<00:17:12.230> talk<00:17:12.410> about<00:17:12.530> a<00:17:12.620> toy 00:17:12.790 --> 00:17:12.800 align:start position:0% now I'm gonna talk about a toy 00:17:12.800 --> 00:17:14.439 align:start position:0% now I'm gonna talk about a toy verification<00:17:13.459> example<00:17:13.850> which<00:17:13.970> is<00:17:14.060> the<00:17:14.150> sum<00:17:14.329> to 00:17:14.439 --> 00:17:14.449 align:start position:0% verification example which is the sum to 00:17:14.449 --> 00:17:17.740 align:start position:0% verification example which is the sum to 1<00:17:14.600> sum<00:17:15.350> to<00:17:15.680> end<00:17:15.829> example<00:17:16.430> I<00:17:16.640> forgot<00:17:17.600> to<00:17:17.689> put 00:17:17.740 --> 00:17:17.750 align:start position:0% 1 sum to end example I forgot to put 00:17:17.750 --> 00:17:19.390 align:start position:0% 1 sum to end example I forgot to put what<00:17:17.900> the<00:17:18.020> actual<00:17:18.290> spec<00:17:18.560> is<00:17:18.740> here<00:17:19.070> but<00:17:19.250> it's 00:17:19.390 --> 00:17:19.400 align:start position:0% what the actual spec is here but it's 00:17:19.400 --> 00:17:22.300 align:start position:0% what the actual spec is here but it's basically<00:17:19.670> that<00:17:19.880> s<00:17:20.150> is<00:17:20.420> equal<00:17:21.170> to<00:17:21.350> n<00:17:21.589> times<00:17:22.070> n 00:17:22.300 --> 00:17:22.310 align:start position:0% basically that s is equal to n times n 00:17:22.310 --> 00:17:25.960 align:start position:0% basically that s is equal to n times n plus<00:17:22.339> 1<00:17:22.579> over<00:17:22.699> 2<00:17:22.910> just<00:17:23.420> a<00:17:23.570> classical<00:17:24.850> you<00:17:25.850> know 00:17:25.960 --> 00:17:25.970 align:start position:0% plus 1 over 2 just a classical you know 00:17:25.970 --> 00:17:28.360 align:start position:0% plus 1 over 2 just a classical you know Euler's<00:17:26.510> form<00:17:26.930> I<00:17:27.110> think<00:17:27.290> Oilers<00:17:27.709> formula<00:17:28.160> for 00:17:28.360 --> 00:17:28.370 align:start position:0% Euler's form I think Oilers formula for 00:17:28.370 --> 00:17:29.620 align:start position:0% Euler's form I think Oilers formula for sums<00:17:28.550> or<00:17:28.730> maybe<00:17:28.850> you<00:17:29.000> cleared<00:17:29.240> or<00:17:29.330> something 00:17:29.620 --> 00:17:29.630 align:start position:0% sums or maybe you cleared or something 00:17:29.630 --> 00:17:31.420 align:start position:0% sums or maybe you cleared or something and<00:17:30.350> you<00:17:30.440> say<00:17:30.710> enough<00:17:30.920> names<00:17:31.130> you<00:17:31.280> eventually 00:17:31.420 --> 00:17:31.430 align:start position:0% and you say enough names you eventually 00:17:31.430 --> 00:17:33.730 align:start position:0% and you say enough names you eventually get<00:17:31.610> them<00:17:31.760> all<00:17:32.410> so<00:17:33.410> in<00:17:33.500> no<00:17:33.620> particular 00:17:33.730 --> 00:17:33.740 align:start position:0% get them all so in no particular 00:17:33.740 --> 00:17:35.380 align:start position:0% get them all so in no particular language<00:17:34.340> this<00:17:34.550> is<00:17:34.580> kind<00:17:34.940> of<00:17:35.000> the<00:17:35.090> program 00:17:35.380 --> 00:17:35.390 align:start position:0% language this is kind of the program 00:17:35.390 --> 00:17:36.880 align:start position:0% language this is kind of the program that<00:17:35.570> we're<00:17:35.690> looking<00:17:35.960> at<00:17:36.110> but<00:17:36.350> in<00:17:36.500> EVM 00:17:36.880 --> 00:17:36.890 align:start position:0% that we're looking at but in EVM 00:17:36.890 --> 00:17:40.690 align:start position:0% that we're looking at but in EVM obviously<00:17:37.370> it<00:17:37.430> looks<00:17:37.520> a<00:17:37.640> little<00:17:37.730> uglier<00:17:39.700> so 00:17:40.690 --> 00:17:40.700 align:start position:0% obviously it looks a little uglier so 00:17:40.700 --> 00:17:42.160 align:start position:0% obviously it looks a little uglier so the<00:17:40.820> proof<00:17:40.970> claim<00:17:41.240> this<00:17:41.510> is<00:17:41.660> the<00:17:41.780> main<00:17:41.930> claim 00:17:42.160 --> 00:17:42.170 align:start position:0% the proof claim this is the main claim 00:17:42.170 --> 00:17:43.900 align:start position:0% the proof claim this is the main claim right<00:17:42.440> here<00:17:42.710> I'm<00:17:43.430> gonna<00:17:43.550> run<00:17:43.730> through<00:17:43.820> this 00:17:43.900 --> 00:17:43.910 align:start position:0% right here I'm gonna run through this 00:17:43.910 --> 00:17:45.610 align:start position:0% right here I'm gonna run through this really<00:17:44.120> quickly<00:17:44.390> but<00:17:44.960> basically<00:17:45.350> we're 00:17:45.610 --> 00:17:45.620 align:start position:0% really quickly but basically we're 00:17:45.620 --> 00:17:46.390 align:start position:0% really quickly but basically we're saying<00:17:45.830> the 00:17:46.390 --> 00:17:46.400 align:start position:0% saying the 00:17:46.400 --> 00:17:47.890 align:start position:0% saying the look<00:17:46.580> like<00:17:46.760> reach<00:17:46.940> ability<00:17:47.180> they<00:17:47.600> look<00:17:47.780> like 00:17:47.890 --> 00:17:47.900 align:start position:0% look like reach ability they look like 00:17:47.900 --> 00:17:49.750 align:start position:0% look like reach ability they look like the<00:17:48.110> the<00:17:48.530> rules<00:17:48.770> from<00:17:48.920> the<00:17:49.070> definition<00:17:49.580> and 00:17:49.750 --> 00:17:49.760 align:start position:0% the the rules from the definition and 00:17:49.760 --> 00:17:50.860 align:start position:0% the the rules from the definition and that's<00:17:49.940> because<00:17:50.240> they<00:17:50.330> pretty<00:17:50.450> much<00:17:50.600> are<00:17:50.810> the 00:17:50.860 --> 00:17:50.870 align:start position:0% that's because they pretty much are the 00:17:50.870 --> 00:17:52.360 align:start position:0% that's because they pretty much are the rules<00:17:51.020> from<00:17:51.170> the<00:17:51.230> definition<00:17:51.650> and<00:17:51.830> basically 00:17:52.360 --> 00:17:52.370 align:start position:0% rules from the definition and basically 00:17:52.370 --> 00:17:53.560 align:start position:0% rules from the definition and basically what<00:17:52.520> its<00:17:52.610> gonna<00:17:52.670> do<00:17:52.880> is<00:17:53.000> it's<00:17:53.030> gonna<00:17:53.150> start<00:17:53.480> on 00:17:53.560 --> 00:17:53.570 align:start position:0% what its gonna do is it's gonna start on 00:17:53.570 --> 00:17:55.630 align:start position:0% what its gonna do is it's gonna start on the<00:17:53.630> left-hand<00:17:54.020> side<00:17:54.230> of<00:17:54.260> the<00:17:54.410> rule<00:17:54.620> notice<00:17:55.550> we 00:17:55.630 --> 00:17:55.640 align:start position:0% the left-hand side of the rule notice we 00:17:55.640 --> 00:17:57.010 align:start position:0% the left-hand side of the rule notice we have<00:17:55.730> a<00:17:55.790> symbolic<00:17:56.030> value<00:17:56.480> here<00:17:56.630> for<00:17:56.660> the<00:17:56.870> gas 00:17:57.010 --> 00:17:57.020 align:start position:0% have a symbolic value here for the gas 00:17:57.020 --> 00:17:58.990 align:start position:0% have a symbolic value here for the gas and<00:17:57.320> symbolic<00:17:57.710> word<00:17:57.890> stack<00:17:58.190> here<00:17:58.460> and<00:17:58.610> it's 00:17:58.990 --> 00:17:59.000 align:start position:0% and symbolic word stack here and it's 00:17:59.000 --> 00:18:01.270 align:start position:0% and symbolic word stack here and it's going<00:17:59.090> to<00:17:59.150> symbolically<00:17:59.600> execute<00:18:00.230> using<00:18:01.190> the 00:18:01.270 --> 00:18:01.280 align:start position:0% going to symbolically execute using the 00:18:01.280 --> 00:18:02.920 align:start position:0% going to symbolically execute using the inference<00:18:01.610> system<00:18:01.760> of<00:18:02.090> reach<00:18:02.240> ability<00:18:02.390> logic 00:18:02.920 --> 00:18:02.930 align:start position:0% inference system of reach ability logic 00:18:02.930 --> 00:18:05.800 align:start position:0% inference system of reach ability logic until<00:18:03.530> it<00:18:03.650> reaches<00:18:03.920> a<00:18:03.950> state<00:18:04.250> that<00:18:04.490> this<00:18:05.090> that 00:18:05.800 --> 00:18:05.810 align:start position:0% until it reaches a state that this that 00:18:05.810 --> 00:18:07.450 align:start position:0% until it reaches a state that this that implies<00:18:06.170> this<00:18:06.500> right-hand<00:18:06.920> side<00:18:07.100> of<00:18:07.220> the<00:18:07.280> rule 00:18:07.450 --> 00:18:07.460 align:start position:0% implies this right-hand side of the rule 00:18:07.460 --> 00:18:11.170 align:start position:0% implies this right-hand side of the rule essentially<00:18:09.340> so<00:18:10.340> basically<00:18:10.820> we're<00:18:10.970> saying 00:18:11.170 --> 00:18:11.180 align:start position:0% essentially so basically we're saying 00:18:11.180 --> 00:18:13.840 align:start position:0% essentially so basically we're saying starting<00:18:11.930> at<00:18:12.050> any<00:18:12.200> word<00:18:12.470> stack<00:18:12.800> we<00:18:13.310> get<00:18:13.490> to<00:18:13.640> the 00:18:13.840 --> 00:18:13.850 align:start position:0% starting at any word stack we get to the 00:18:13.850 --> 00:18:16.480 align:start position:0% starting at any word stack we get to the same<00:18:14.090> word<00:18:14.330> stack<00:18:14.660> but<00:18:15.020> with<00:18:15.200> the<00:18:15.350> sum<00:18:15.620> from<00:18:16.250> 1 00:18:16.480 --> 00:18:16.490 align:start position:0% same word stack but with the sum from 1 00:18:16.490 --> 00:18:18.370 align:start position:0% same word stack but with the sum from 1 to<00:18:16.610> n<00:18:16.730> put<00:18:17.000> on<00:18:17.120> the<00:18:17.270> top<00:18:17.450> and<00:18:17.720> our<00:18:17.840> counter<00:18:18.200> gets 00:18:18.370 --> 00:18:18.380 align:start position:0% to n put on the top and our counter gets 00:18:18.380 --> 00:18:21.430 align:start position:0% to n put on the top and our counter gets to<00:18:18.530> 0<00:18:18.800> and<00:18:19.040> the<00:18:19.460> gas<00:18:19.720> consumed<00:18:20.720> is<00:18:20.960> exactly 00:18:21.430 --> 00:18:21.440 align:start position:0% to 0 and the gas consumed is exactly 00:18:21.440 --> 00:18:22.900 align:start position:0% to 0 and the gas consumed is exactly this<00:18:21.650> amount<00:18:21.830> and<00:18:22.160> then<00:18:22.520> we<00:18:22.610> have<00:18:22.730> some 00:18:22.900 --> 00:18:22.910 align:start position:0% this amount and then we have some 00:18:22.910 --> 00:18:24.430 align:start position:0% this amount and then we have some preconditions<00:18:23.270> basically<00:18:23.960> stating<00:18:24.410> that 00:18:24.430 --> 00:18:24.440 align:start position:0% preconditions basically stating that 00:18:24.440 --> 00:18:27.340 align:start position:0% preconditions basically stating that like<00:18:24.770> and<00:18:25.070> is<00:18:25.580> greater<00:18:25.850> than<00:18:25.940> 0<00:18:26.210> there<00:18:26.960> is<00:18:26.990> an 00:18:27.340 --> 00:18:27.350 align:start position:0% like and is greater than 0 there is an 00:18:27.350 --> 00:18:29.710 align:start position:0% like and is greater than 0 there is an integer<00:18:27.830> overflow<00:18:28.520> the<00:18:29.150> size<00:18:29.390> of<00:18:29.510> the<00:18:29.570> word 00:18:29.710 --> 00:18:29.720 align:start position:0% integer overflow the size of the word 00:18:29.720 --> 00:18:30.970 align:start position:0% integer overflow the size of the word stack<00:18:29.990> is<00:18:30.140> small<00:18:30.380> enough<00:18:30.560> that<00:18:30.620> there<00:18:30.860> will 00:18:30.970 --> 00:18:30.980 align:start position:0% stack is small enough that there will 00:18:30.980 --> 00:18:34.690 align:start position:0% stack is small enough that there will want<00:18:31.340> be<00:18:31.430> a<00:18:31.460> stack<00:18:31.700> overflow<00:18:31.910> and<00:18:32.450> the<00:18:33.400> the<00:18:34.400> gas 00:18:34.690 --> 00:18:34.700 align:start position:0% want be a stack overflow and the the gas 00:18:34.700 --> 00:18:36.640 align:start position:0% want be a stack overflow and the the gas consumed<00:18:35.210> is<00:18:35.390> the<00:18:35.660> gas<00:18:35.840> available<00:18:36.050> is<00:18:36.440> large 00:18:36.640 --> 00:18:36.650 align:start position:0% consumed is the gas available is large 00:18:36.650 --> 00:18:39.970 align:start position:0% consumed is the gas available is large enough<00:18:37.300> basically<00:18:38.300> you<00:18:39.260> know<00:18:39.350> we<00:18:39.560> first<00:18:39.800> write 00:18:39.970 --> 00:18:39.980 align:start position:0% enough basically you know we first write 00:18:39.980 --> 00:18:41.860 align:start position:0% enough basically you know we first write down<00:18:40.040> the<00:18:40.190> spec<00:18:40.520> up<00:18:40.700> here<00:18:41.000> and<00:18:41.150> then<00:18:41.540> we<00:18:41.630> try<00:18:41.810> to 00:18:41.860 --> 00:18:41.870 align:start position:0% down the spec up here and then we try to 00:18:41.870 --> 00:18:44.380 align:start position:0% down the spec up here and then we try to prove<00:18:42.080> it<00:18:42.260> and<00:18:42.350> then<00:18:42.560> the<00:18:42.620> prover<00:18:42.920> tells<00:18:43.160> us<00:18:43.400> in 00:18:44.380 --> 00:18:44.390 align:start position:0% prove it and then the prover tells us in 00:18:44.390 --> 00:18:46.000 align:start position:0% prove it and then the prover tells us in a<00:18:44.510> not<00:18:44.690> so<00:18:44.840> intuitive<00:18:45.110> way<00:18:45.380> that<00:18:45.710> it<00:18:45.800> can't 00:18:46.000 --> 00:18:46.010 align:start position:0% a not so intuitive way that it can't 00:18:46.010 --> 00:18:47.860 align:start position:0% a not so intuitive way that it can't prove<00:18:46.250> it<00:18:46.400> and<00:18:46.520> then<00:18:47.030> we<00:18:47.150> say<00:18:47.330> oh<00:18:47.510> what<00:18:47.720> are<00:18:47.810> the 00:18:47.860 --> 00:18:47.870 align:start position:0% prove it and then we say oh what are the 00:18:47.870 --> 00:18:50.140 align:start position:0% prove it and then we say oh what are the preconditions<00:18:48.380> we<00:18:48.470> have<00:18:48.620> to<00:18:48.740> add<00:18:48.940> the<00:18:49.940> reason 00:18:50.140 --> 00:18:50.150 align:start position:0% preconditions we have to add the reason 00:18:50.150 --> 00:18:52.960 align:start position:0% preconditions we have to add the reason I'm<00:18:50.240> telling<00:18:50.390> you<00:18:50.540> that<00:18:50.690> is<00:18:50.930> because<00:18:51.730> okay<00:18:52.730> so 00:18:52.960 --> 00:18:52.970 align:start position:0% I'm telling you that is because okay so 00:18:52.970 --> 00:18:55.270 align:start position:0% I'm telling you that is because okay so actually<00:18:53.510> with<00:18:53.630> some<00:18:53.960> example<00:18:54.620> there's<00:18:55.100> this 00:18:55.270 --> 00:18:55.280 align:start position:0% actually with some example there's this 00:18:55.280 --> 00:18:57.400 align:start position:0% actually with some example there's this loop<00:18:55.550> in<00:18:55.790> traditional<00:18:56.450> logic<00:18:57.200> style 00:18:57.400 --> 00:18:57.410 align:start position:0% loop in traditional logic style 00:18:57.410 --> 00:18:58.390 align:start position:0% loop in traditional logic style things<00:18:57.650> you<00:18:57.740> have<00:18:57.860> to<00:18:57.920> provide<00:18:58.100> a<00:18:58.160> loop 00:18:58.390 --> 00:18:58.400 align:start position:0% things you have to provide a loop 00:18:58.400 --> 00:19:00.100 align:start position:0% things you have to provide a loop invariant<00:18:58.520> we<00:18:59.240> generalize<00:18:59.690> that<00:18:59.840> a<00:18:59.900> little 00:19:00.100 --> 00:19:00.110 align:start position:0% invariant we generalize that a little 00:19:00.110 --> 00:19:01.360 align:start position:0% invariant we generalize that a little bit<00:19:00.230> and<00:19:00.320> reach<00:19:00.470> ability<00:19:00.680> logic<00:19:01.160> to<00:19:01.280> the 00:19:01.360 --> 00:19:01.370 align:start position:0% bit and reach ability logic to the 00:19:01.370 --> 00:19:03.520 align:start position:0% bit and reach ability logic to the notion<00:19:01.640> of<00:19:01.700> a<00:19:01.790> circularity<00:19:02.380> and<00:19:03.380> this 00:19:03.520 --> 00:19:03.530 align:start position:0% notion of a circularity and this 00:19:03.530 --> 00:19:05.500 align:start position:0% notion of a circularity and this basically<00:19:03.860> says<00:19:04.130> if<00:19:04.670> you're<00:19:04.880> starting<00:19:05.270> at<00:19:05.390> the 00:19:05.500 --> 00:19:05.510 align:start position:0% basically says if you're starting at the 00:19:05.510 --> 00:19:07.720 align:start position:0% basically says if you're starting at the loop<00:19:05.690> head<00:19:06.050> you<00:19:06.860> can<00:19:07.010> reach<00:19:07.190> the<00:19:07.340> end<00:19:07.370> of<00:19:07.640> the 00:19:07.720 --> 00:19:07.730 align:start position:0% loop head you can reach the end of the 00:19:07.730 --> 00:19:11.530 align:start position:0% loop head you can reach the end of the program<00:19:08.230> and<00:19:10.000> calculate<00:19:11.000> the<00:19:11.180> correct 00:19:11.530 --> 00:19:11.540 align:start position:0% program and calculate the correct 00:19:11.540 --> 00:19:13.450 align:start position:0% program and calculate the correct remaining<00:19:12.140> partial<00:19:12.590> sums<00:19:12.800> so<00:19:13.010> notice<00:19:13.310> in<00:19:13.400> a 00:19:13.450 --> 00:19:13.460 align:start position:0% remaining partial sums so notice in a 00:19:13.460 --> 00:19:14.650 align:start position:0% remaining partial sums so notice in a loop<00:19:13.640> invariant<00:19:13.820> if<00:19:14.180> you're<00:19:14.300> familiar<00:19:14.420> with 00:19:14.650 --> 00:19:14.660 align:start position:0% loop invariant if you're familiar with 00:19:14.660 --> 00:19:16.270 align:start position:0% loop invariant if you're familiar with those<00:19:14.840> you<00:19:15.380> specify<00:19:15.710> the<00:19:15.770> behavior<00:19:15.920> of<00:19:16.220> a 00:19:16.270 --> 00:19:16.280 align:start position:0% those you specify the behavior of a 00:19:16.280 --> 00:19:17.860 align:start position:0% those you specify the behavior of a single<00:19:16.460> iteration<00:19:16.700> of<00:19:17.090> loop<00:19:17.270> here<00:19:17.780> you 00:19:17.860 --> 00:19:17.870 align:start position:0% single iteration of loop here you 00:19:17.870 --> 00:19:19.510 align:start position:0% single iteration of loop here you specify<00:19:18.080> the<00:19:18.380> behavior<00:19:18.800> from<00:19:19.010> the<00:19:19.220> beginning 00:19:19.510 --> 00:19:19.520 align:start position:0% specify the behavior from the beginning 00:19:19.520 --> 00:19:20.950 align:start position:0% specify the behavior from the beginning of<00:19:19.580> the<00:19:19.640> loop<00:19:19.790> to<00:19:20.210> the<00:19:20.240> end<00:19:20.510> of<00:19:20.570> the<00:19:20.630> program 00:19:20.950 --> 00:19:20.960 align:start position:0% of the loop to the end of the program 00:19:20.960 --> 00:19:23.140 align:start position:0% of the loop to the end of the program which<00:19:21.110> is<00:19:21.230> often<00:19:21.590> easier<00:19:21.890> to<00:19:22.010> specify<00:19:22.520> than 00:19:23.140 --> 00:19:23.150 align:start position:0% which is often easier to specify than 00:19:23.150 --> 00:19:24.430 align:start position:0% which is often easier to specify than the<00:19:23.270> behavior<00:19:23.390> of<00:19:23.630> a<00:19:23.720> single<00:19:23.960> iteration<00:19:24.080> of 00:19:24.430 --> 00:19:24.440 align:start position:0% the behavior of a single iteration of 00:19:24.440 --> 00:19:25.770 align:start position:0% the behavior of a single iteration of the<00:19:24.530> loop 00:19:25.770 --> 00:19:25.780 align:start position:0% the loop 00:19:25.780 --> 00:19:28.030 align:start position:0% the loop okay<00:19:26.780> so<00:19:26.840> verifying<00:19:27.290> a<00:19:27.380> VI<00:19:27.530> compliant 00:19:28.030 --> 00:19:28.040 align:start position:0% okay so verifying a VI compliant 00:19:28.040 --> 00:19:30.490 align:start position:0% okay so verifying a VI compliant contracts<00:19:28.810> writing<00:19:29.810> these<00:19:29.930> specifications 00:19:30.490 --> 00:19:30.500 align:start position:0% contracts writing these specifications 00:19:30.500 --> 00:19:31.660 align:start position:0% contracts writing these specifications is<00:19:30.590> actually<00:19:30.860> really<00:19:30.980> hard<00:19:31.250> for<00:19:31.400> ABI 00:19:31.660 --> 00:19:31.670 align:start position:0% is actually really hard for ABI 00:19:31.670 --> 00:19:33.640 align:start position:0% is actually really hard for ABI contracts<00:19:32.240> because<00:19:32.540> you<00:19:33.110> know<00:19:33.230> they're<00:19:33.410> huge 00:19:33.640 --> 00:19:33.650 align:start position:0% contracts because you know they're huge 00:19:33.650 --> 00:19:35.590 align:start position:0% contracts because you know they're huge right<00:19:33.950> so<00:19:34.430> we've<00:19:34.730> provided<00:19:34.910> some<00:19:35.300> helper 00:19:35.590 --> 00:19:35.600 align:start position:0% right so we've provided some helper 00:19:35.600 --> 00:19:37.690 align:start position:0% right so we've provided some helper functions<00:19:36.020> like<00:19:36.260> ABI<00:19:36.560> call<00:19:36.830> data<00:19:37.040> and<00:19:37.460> some 00:19:37.690 --> 00:19:37.700 align:start position:0% functions like ABI call data and some 00:19:37.700 --> 00:19:39.550 align:start position:0% functions like ABI call data and some other<00:19:37.820> little<00:19:38.000> ones<00:19:38.270> which<00:19:38.870> will<00:19:39.080> let<00:19:39.350> you 00:19:39.550 --> 00:19:39.560 align:start position:0% other little ones which will let you 00:19:39.560 --> 00:19:41.770 align:start position:0% other little ones which will let you essentially<00:19:40.040> actually<00:19:40.910> pass<00:19:41.120> in<00:19:41.390> the<00:19:41.540> name<00:19:41.660> of 00:19:41.770 --> 00:19:41.780 align:start position:0% essentially actually pass in the name of 00:19:41.780 --> 00:19:43.150 align:start position:0% essentially actually pass in the name of the<00:19:41.840> function<00:19:41.990> you<00:19:42.290> want<00:19:42.320> to<00:19:42.500> call<00:19:42.560> or<00:19:43.040> the 00:19:43.150 --> 00:19:43.160 align:start position:0% the function you want to call or the 00:19:43.160 --> 00:19:44.500 align:start position:0% the function you want to call or the typed<00:19:43.370> arguments<00:19:43.940> that<00:19:44.090> you<00:19:44.150> want<00:19:44.300> to<00:19:44.390> pass 00:19:44.500 --> 00:19:44.510 align:start position:0% typed arguments that you want to pass 00:19:44.510 --> 00:19:45.850 align:start position:0% typed arguments that you want to pass that<00:19:44.570> function<00:19:45.170> for<00:19:45.290> example<00:19:45.620> instead<00:19:45.770> of 00:19:45.850 --> 00:19:45.860 align:start position:0% that function for example instead of 00:19:45.860 --> 00:19:49.110 align:start position:0% that function for example instead of having<00:19:45.950> to<00:19:46.250> pass<00:19:46.400> in<00:19:46.670> sorry<00:19:47.300> the<00:19:47.920> hex<00:19:48.920> encoded 00:19:49.110 --> 00:19:49.120 align:start position:0% having to pass in sorry the hex encoded 00:19:49.120 --> 00:19:53.080 align:start position:0% having to pass in sorry the hex encoded bike<00:19:50.120> string<00:19:50.510> for<00:19:50.750> example<00:19:51.640> and<00:19:52.640> so<00:19:52.760> here's<00:19:53.000> an 00:19:53.080 --> 00:19:53.090 align:start position:0% bike string for example and so here's an 00:19:53.090 --> 00:19:55.080 align:start position:0% bike string for example and so here's an example<00:19:53.150> usage<00:19:53.750> and<00:19:54.110> say<00:19:54.260> maybe<00:19:54.440> I<00:19:54.530> call<00:19:54.830> data 00:19:55.080 --> 00:19:55.090 align:start position:0% example usage and say maybe I call data 00:19:55.090 --> 00:19:58.270 align:start position:0% example usage and say maybe I call data transfer<00:19:56.090> to<00:19:56.720> this<00:19:56.840> address<00:19:57.080> this<00:19:57.950> transfer 00:19:58.270 --> 00:19:58.280 align:start position:0% transfer to this address this transfer 00:19:58.280 --> 00:19:59.769 align:start position:0% transfer to this address this transfer value<00:19:58.460> note<00:19:58.880> that<00:19:59.060> transfer<00:19:59.450> here 00:19:59.769 --> 00:19:59.779 align:start position:0% value note that transfer here 00:19:59.779 --> 00:20:01.479 align:start position:0% value note that transfer here as<00:19:59.869> a<00:19:59.929> symbolic<00:20:00.259> value<00:20:00.469> but<00:20:01.159> this<00:20:01.279> is<00:20:01.369> actually 00:20:01.479 --> 00:20:01.489 align:start position:0% as a symbolic value but this is actually 00:20:01.489 --> 00:20:04.629 align:start position:0% as a symbolic value but this is actually a<00:20:01.669> constant<00:20:02.830> so<00:20:03.830> that's<00:20:04.129> the<00:20:04.249> called<00:20:04.460> a<00:20:04.580> to 00:20:04.629 --> 00:20:04.639 align:start position:0% a constant so that's the called a to 00:20:04.639 --> 00:20:06.759 align:start position:0% a constant so that's the called a to sell<00:20:04.909> and<00:20:05.119> then<00:20:05.659> here<00:20:06.019> you<00:20:06.289> would<00:20:06.409> use<00:20:06.590> it 00:20:06.759 --> 00:20:06.769 align:start position:0% sell and then here you would use it 00:20:06.769 --> 00:20:08.529 align:start position:0% sell and then here you would use it right<00:20:06.919> here<00:20:07.249> this<00:20:07.700> is<00:20:07.879> this<00:20:08.179> would<00:20:08.330> be<00:20:08.419> that 00:20:08.529 --> 00:20:08.539 align:start position:0% right here this is this would be that 00:20:08.539 --> 00:20:10.690 align:start position:0% right here this is this would be that line<00:20:08.779> above<00:20:09.159> instead<00:20:10.159> of<00:20:10.279> having<00:20:10.429> to<00:20:10.549> write 00:20:10.690 --> 00:20:10.700 align:start position:0% line above instead of having to write 00:20:10.700 --> 00:20:12.609 align:start position:0% line above instead of having to write out<00:20:10.849> the<00:20:10.999> byte<00:20:11.149> encoded<00:20:11.690> hex<00:20:11.899> values<00:20:12.259> here<00:20:12.469> and 00:20:12.609 --> 00:20:12.619 align:start position:0% out the byte encoded hex values here and 00:20:12.619 --> 00:20:14.200 align:start position:0% out the byte encoded hex values here and then<00:20:12.679> notice<00:20:13.159> the<00:20:13.309> balanced<00:20:13.700> one<00:20:13.879> goes<00:20:14.179> to 00:20:14.200 --> 00:20:14.210 align:start position:0% then notice the balanced one goes to 00:20:14.210 --> 00:20:16.060 align:start position:0% then notice the balanced one goes to balance<00:20:14.899> one<00:20:14.989> -<00:20:15.259> transferred<00:20:15.590> miles<00:20:15.769> -<00:20:15.889> to 00:20:16.060 --> 00:20:16.070 align:start position:0% balance one - transferred miles - to 00:20:16.070 --> 00:20:18.339 align:start position:0% balance one - transferred miles - to balance<00:20:16.190> or<00:20:16.460> to<00:20:16.729> loss<00:20:17.210> transfer<00:20:17.599> and<00:20:17.779> then<00:20:18.169> all 00:20:18.339 --> 00:20:18.349 align:start position:0% balance or to loss transfer and then all 00:20:18.349 --> 00:20:20.049 align:start position:0% balance or to loss transfer and then all these<00:20:18.469> preconditions<00:20:19.070> right<00:20:19.249> here<00:20:19.460> some<00:20:20.029> of 00:20:20.049 --> 00:20:20.059 align:start position:0% these preconditions right here some of 00:20:20.059 --> 00:20:21.729 align:start position:0% these preconditions right here some of them<00:20:20.269> were<00:20:20.419> caught<00:20:20.659> this<00:20:20.929> is<00:20:21.109> this<00:20:21.320> examples 00:20:21.729 --> 00:20:21.739 align:start position:0% them were caught this is this examples 00:20:21.739 --> 00:20:23.830 align:start position:0% them were caught this is this examples hkg<00:20:22.309> token<00:20:22.639> they<00:20:22.729> had<00:20:22.849> a<00:20:22.879> bug<00:20:23.059> in<00:20:23.179> it<00:20:23.299> some<00:20:23.809> of 00:20:23.830 --> 00:20:23.840 align:start position:0% hkg token they had a bug in it some of 00:20:23.840 --> 00:20:26.589 align:start position:0% hkg token they had a bug in it some of these<00:20:23.960> were<00:20:24.109> caught<00:20:24.349> by<00:20:25.159> the<00:20:25.190> hkg<00:20:25.789> auditors 00:20:26.589 --> 00:20:26.599 align:start position:0% these were caught by the hkg auditors 00:20:26.599 --> 00:20:28.509 align:start position:0% these were caught by the hkg auditors some<00:20:26.899> weren't<00:20:27.049> actually<00:20:27.499> so<00:20:27.679> our<00:20:28.159> prove<00:20:28.429> er 00:20:28.509 --> 00:20:28.519 align:start position:0% some weren't actually so our prove er 00:20:28.519 --> 00:20:30.519 align:start position:0% some weren't actually so our prove er was<00:20:28.639> able<00:20:28.849> to<00:20:28.879> help<00:20:29.059> us<00:20:29.239> find<00:20:29.539> some<00:20:30.229> integer 00:20:30.519 --> 00:20:30.529 align:start position:0% was able to help us find some integer 00:20:30.529 --> 00:20:31.839 align:start position:0% was able to help us find some integer overflow<00:20:30.859> bugs<00:20:31.070> and<00:20:31.249> stuff<00:20:31.369> like<00:20:31.460> that<00:20:31.639> okay 00:20:31.839 --> 00:20:31.849 align:start position:0% overflow bugs and stuff like that okay 00:20:31.849 --> 00:20:35.259 align:start position:0% overflow bugs and stuff like that okay so<00:20:32.839> not<00:20:33.259> enough<00:20:33.440> time<00:20:33.679> here<00:20:33.889> but<00:20:34.279> basically<00:20:34.460> we 00:20:35.259 --> 00:20:35.269 align:start position:0% so not enough time here but basically we 00:20:35.269 --> 00:20:37.570 align:start position:0% so not enough time here but basically we passed<00:20:35.479> the<00:20:35.629> tests<00:20:36.129> almost<00:20:37.129> passing<00:20:37.399> large 00:20:37.570 --> 00:20:37.580 align:start position:0% passed the tests almost passing large 00:20:37.580 --> 00:20:38.919 align:start position:0% passed the tests almost passing large chain<00:20:37.759> tests<00:20:38.089> with<00:20:38.359> an<00:20:38.479> order<00:20:38.719> of<00:20:38.839> magnitude 00:20:38.919 --> 00:20:38.929 align:start position:0% chain tests with an order of magnitude 00:20:38.929 --> 00:20:41.200 align:start position:0% chain tests with an order of magnitude of<00:20:39.619> the<00:20:39.830> performance<00:20:40.279> of<00:20:40.369> CPP<00:20:40.759> etherium<00:20:41.089> which 00:20:41.200 --> 00:20:41.210 align:start position:0% of the performance of CPP etherium which 00:20:41.210 --> 00:20:43.029 align:start position:0% of the performance of CPP etherium which is<00:20:41.299> pretty<00:20:41.479> good<00:20:41.690> for<00:20:41.749> a<00:20:42.229> formal<00:20:42.859> verification 00:20:43.029 --> 00:20:43.039 align:start position:0% is pretty good for a formal verification 00:20:43.039 --> 00:20:46.329 align:start position:0% is pretty good for a formal verification framework<00:20:44.469> we're<00:20:45.469> working<00:20:45.769> on<00:20:45.859> some<00:20:46.070> ABI 00:20:46.329 --> 00:20:46.339 align:start position:0% framework we're working on some ABI 00:20:46.339 --> 00:20:48.339 align:start position:0% framework we're working on some ABI abstraction<00:20:46.909> stuff<00:20:47.149> and<00:20:47.389> not<00:20:47.929> discussed<00:20:48.289> here 00:20:48.339 --> 00:20:48.349 align:start position:0% abstraction stuff and not discussed here 00:20:48.349 --> 00:20:49.599 align:start position:0% abstraction stuff and not discussed here but<00:20:48.529> come<00:20:48.769> and<00:20:48.889> ask<00:20:49.009> me<00:20:49.129> about<00:20:49.219> it 00:20:49.599 --> 00:20:49.609 align:start position:0% but come and ask me about it 00:20:49.609 --> 00:20:52.509 align:start position:0% but come and ask me about it EVM<00:20:50.179> crime<00:20:50.509> which<00:20:51.229> was<00:20:51.440> the<00:20:51.619> ic3<00:20:52.009> bootcamp 00:20:52.509 --> 00:20:52.519 align:start position:0% EVM crime which was the ic3 bootcamp 00:20:52.519 --> 00:20:55.690 align:start position:0% EVM crime which was the ic3 bootcamp project<00:20:52.999> we're<00:20:53.779> extending<00:20:54.219> EVM<00:20:55.219> with<00:20:55.489> some 00:20:55.690 --> 00:20:55.700 align:start position:0% project we're extending EVM with some 00:20:55.700 --> 00:20:56.829 align:start position:0% project we're extending EVM with some stuff<00:20:55.879> to<00:20:56.059> make<00:20:56.089> it<00:20:56.210> easier<00:20:56.599> to<00:20:56.629> give 00:20:56.829 --> 00:20:56.839 align:start position:0% stuff to make it easier to give 00:20:56.839 --> 00:21:00.039 align:start position:0% stuff to make it easier to give semantics<00:20:57.799> to<00:20:57.919> Viper<00:20:58.129> via<00:20:58.940> compilation<00:20:59.690> -<00:20:59.779> EVM 00:21:00.039 --> 00:21:00.049 align:start position:0% semantics to Viper via compilation - EVM 00:21:00.049 --> 00:21:02.339 align:start position:0% semantics to Viper via compilation - EVM and<00:21:00.259> we're<00:21:00.799> getting<00:21:00.979> pretty<00:21:01.129> close<00:21:01.279> on<00:21:01.519> that 00:21:02.339 --> 00:21:02.349 align:start position:0% and we're getting pretty close on that 00:21:02.349 --> 00:21:06.719 align:start position:0% and we're getting pretty close on that yeah<00:21:03.349> so<00:21:03.559> this<00:21:03.679> is<00:21:03.739> the<00:21:04.039> K<00:21:04.609> framework<00:21:05.029> overview 00:21:06.719 --> 00:21:06.729 align:start position:0% yeah so this is the K framework overview 00:21:06.729 --> 00:21:08.979 align:start position:0% yeah so this is the K framework overview it's<00:21:07.729> not<00:21:07.879> just<00:21:08.089> for<00:21:08.239> blockchain<00:21:08.599> languages 00:21:08.979 --> 00:21:08.989 align:start position:0% it's not just for blockchain languages 00:21:08.989 --> 00:21:11.780 align:start position:0% it's not just for blockchain languages and<00:21:09.739> that's 00:21:11.780 --> 00:21:11.790 align:start position:0% and that's 00:21:11.790 --> 00:21:15.280 align:start position:0% and that's [Applause] 00:21:15.280 --> 00:21:15.290 align:start position:0% [Applause] 00:21:15.290 --> 00:21:26.420 align:start position:0% [Applause] thanks<00:21:16.010> Everett 00:21:26.420 --> 00:21:26.430 align:start position:0% 00:21:26.430 --> 00:21:34.009 align:start position:0% [Music]