WEBVTT Kind: captions Language: en 00:00:00.760 --> 00:00:03.550 align:start position:0% uh<00:00:00.960> now<00:00:01.160> I<00:00:01.400> talk<00:00:01.719> about<00:00:02.040> this<00:00:02.280> scary<00:00:02.760> topic<00:00:03.199> of 00:00:03.550 --> 00:00:03.560 align:start position:0% uh now I talk about this scary topic of 00:00:03.560 --> 00:00:05.909 align:start position:0% uh now I talk about this scary topic of formal 00:00:05.909 --> 00:00:05.919 align:start position:0% formal 00:00:05.919 --> 00:00:08.589 align:start position:0% formal verification<00:00:06.919> when<00:00:07.480> people<00:00:07.759> say<00:00:08.080> formal 00:00:08.589 --> 00:00:08.599 align:start position:0% verification when people say formal 00:00:08.599 --> 00:00:10.950 align:start position:0% verification when people say formal people<00:00:08.920> usually<00:00:09.400> talk<00:00:09.639> about<00:00:09.960> formal<00:00:10.400> attire 00:00:10.950 --> 00:00:10.960 align:start position:0% people usually talk about formal attire 00:00:10.960 --> 00:00:14.150 align:start position:0% people usually talk about formal attire formal<00:00:11.679> speech<00:00:12.599> formal 00:00:14.150 --> 00:00:14.160 align:start position:0% formal speech formal 00:00:14.160 --> 00:00:18.269 align:start position:0% formal speech formal ceremony<00:00:15.520> p<00:00:16.520> uh 00:00:18.269 --> 00:00:18.279 align:start position:0% ceremony p uh 00:00:18.279 --> 00:00:21.910 align:start position:0% ceremony p uh but<00:00:19.279> the<00:00:19.520> formal<00:00:20.119> informal<00:00:20.920> verification 00:00:21.910 --> 00:00:21.920 align:start position:0% but the formal informal verification 00:00:21.920 --> 00:00:24.870 align:start position:0% but the formal informal verification comes<00:00:22.320> from<00:00:23.000> formalized 00:00:24.870 --> 00:00:24.880 align:start position:0% comes from formalized 00:00:24.880 --> 00:00:27.710 align:start position:0% comes from formalized mathematics<00:00:25.880> uh<00:00:26.119> in<00:00:26.599> usual 00:00:27.710 --> 00:00:27.720 align:start position:0% mathematics uh in usual 00:00:27.720 --> 00:00:29.749 align:start position:0% mathematics uh in usual mathematics<00:00:28.720> something<00:00:29.119> is<00:00:29.320> written<00:00:29.599> on 00:00:29.749 --> 00:00:29.759 align:start position:0% mathematics something is written on 00:00:29.759 --> 00:00:31.109 align:start position:0% mathematics something is written on paper 00:00:31.109 --> 00:00:31.119 align:start position:0% paper 00:00:31.119 --> 00:00:34.510 align:start position:0% paper and<00:00:31.279> the<00:00:31.439> mathematician<00:00:32.239> read<00:00:32.879> it<00:00:33.879> and<00:00:34.200> she 00:00:34.510 --> 00:00:34.520 align:start position:0% and the mathematician read it and she 00:00:34.520 --> 00:00:38.389 align:start position:0% and the mathematician read it and she gets<00:00:34.719> an<00:00:35.000> idea<00:00:35.520> some<00:00:35.879> idea<00:00:36.879> and<00:00:37.079> she<00:00:37.320> can<00:00:37.600> say 00:00:38.389 --> 00:00:38.399 align:start position:0% gets an idea some idea and she can say 00:00:38.399 --> 00:00:41.270 align:start position:0% gets an idea some idea and she can say perhaps<00:00:39.160> correct<00:00:39.800> but 00:00:41.270 --> 00:00:41.280 align:start position:0% perhaps correct but 00:00:41.280 --> 00:00:44.549 align:start position:0% perhaps correct but boring<00:00:42.280> in<00:00:42.520> formalized<00:00:43.320> mathematics<00:00:44.320> uh 00:00:44.549 --> 00:00:44.559 align:start position:0% boring in formalized mathematics uh 00:00:44.559 --> 00:00:47.910 align:start position:0% boring in formalized mathematics uh something<00:00:45.000> is<00:00:45.280> written<00:00:45.800> in<00:00:46.399> computer<00:00:46.960> file 00:00:47.910 --> 00:00:47.920 align:start position:0% something is written in computer file 00:00:47.920 --> 00:00:49.990 align:start position:0% something is written in computer file and<00:00:48.079> the<00:00:48.239> Machine<00:00:49.160> Vis 00:00:49.990 --> 00:00:50.000 align:start position:0% and the Machine Vis 00:00:50.000 --> 00:00:54.150 align:start position:0% and the Machine Vis it<00:00:51.000> the<00:00:51.120> machine<00:00:51.399> has<00:00:51.600> no<00:00:51.840> idea<00:00:52.520> I<00:00:52.960> guess<00:00:53.960> but 00:00:54.150 --> 00:00:54.160 align:start position:0% it the machine has no idea I guess but 00:00:54.160 --> 00:00:58.150 align:start position:0% it the machine has no idea I guess but it<00:00:54.399> says<00:00:55.320> correct<00:00:56.039> by<00:00:56.280> just<00:00:56.480> looking<00:00:56.800> at<00:00:56.960> the 00:00:58.150 --> 00:00:58.160 align:start position:0% it says correct by just looking at the 00:00:58.160 --> 00:01:00.869 align:start position:0% it says correct by just looking at the form<00:00:59.160> of<00:00:59.399> what's<00:00:59.640> written 00:01:00.869 --> 00:01:00.879 align:start position:0% form of what's written 00:01:00.879 --> 00:01:03.830 align:start position:0% form of what's written and<00:01:01.120> this<00:01:01.440> for<00:01:02.079> is<00:01:02.480> what<00:01:02.760> this<00:01:02.960> form 00:01:03.830 --> 00:01:03.840 align:start position:0% and this for is what this form 00:01:03.840 --> 00:01:05.550 align:start position:0% and this for is what this form mathematics<00:01:04.400> is 00:01:05.550 --> 00:01:05.560 align:start position:0% mathematics is 00:01:05.560 --> 00:01:10.190 align:start position:0% mathematics is about<00:01:06.560> this<00:01:06.680> is<00:01:07.000> great<00:01:07.360> for<00:01:08.360> smart<00:01:08.840> contract 00:01:10.190 --> 00:01:10.200 align:start position:0% about this is great for smart contract 00:01:10.200 --> 00:01:12.830 align:start position:0% about this is great for smart contract verification<00:01:11.200> because<00:01:12.000> usually<00:01:12.479> when<00:01:12.680> you 00:01:12.830 --> 00:01:12.840 align:start position:0% verification because usually when you 00:01:12.840 --> 00:01:16.030 align:start position:0% verification because usually when you try<00:01:13.080> to<00:01:13.280> prove<00:01:13.680> smart<00:01:14.080> contracts<00:01:15.040> correct 00:01:16.030 --> 00:01:16.040 align:start position:0% try to prove smart contracts correct 00:01:16.040 --> 00:01:19.350 align:start position:0% try to prove smart contracts correct it's<00:01:16.200> a<00:01:16.439> massive<00:01:16.920> case<00:01:17.400> analysis<00:01:18.400> if<00:01:18.640> any<00:01:19.000> data 00:01:19.350 --> 00:01:19.360 align:start position:0% it's a massive case analysis if any data 00:01:19.360 --> 00:01:23.069 align:start position:0% it's a massive case analysis if any data is<00:01:19.560> sent<00:01:20.439> from<00:01:20.920> the<00:01:21.079> quer<00:01:22.040> if<00:01:22.280> any<00:01:22.640> value<00:01:22.920> is 00:01:23.069 --> 00:01:23.079 align:start position:0% is sent from the quer if any value is 00:01:23.079 --> 00:01:25.510 align:start position:0% is sent from the quer if any value is sent<00:01:23.400> from<00:01:23.560> the<00:01:23.720> C<00:01:24.560> if<00:01:24.720> the<00:01:24.880> center<00:01:25.240> data 00:01:25.510 --> 00:01:25.520 align:start position:0% sent from the C if the center data 00:01:25.520 --> 00:01:29.429 align:start position:0% sent from the C if the center data matches<00:01:26.000> function<00:01:26.600> signatures<00:01:27.600> or<00:01:28.159> not<00:01:29.159> um 00:01:29.429 --> 00:01:29.439 align:start position:0% matches function signatures or not um 00:01:29.439 --> 00:01:31.069 align:start position:0% matches function signatures or not um what's<00:01:29.640> in<00:01:29.759> the<00:01:30.000> storage<00:01:30.479> but<00:01:30.680> not<00:01:30.840> in<00:01:30.960> the 00:01:31.069 --> 00:01:31.079 align:start position:0% what's in the storage but not in the 00:01:31.079 --> 00:01:33.109 align:start position:0% what's in the storage but not in the storage<00:01:31.560> so<00:01:31.720> it's<00:01:31.920> massive<00:01:32.320> case<00:01:32.600> analysis 00:01:33.109 --> 00:01:33.119 align:start position:0% storage so it's massive case analysis 00:01:33.119 --> 00:01:36.429 align:start position:0% storage so it's massive case analysis and<00:01:33.840> usual<00:01:34.280> mathema<00:01:35.280> to 00:01:36.429 --> 00:01:36.439 align:start position:0% and usual mathema to 00:01:36.439 --> 00:01:40.670 align:start position:0% and usual mathema to be<00:01:37.439> enabl<00:01:37.960> to<00:01:38.240> read<00:01:38.840> read<00:01:39.040> it<00:01:39.439> because<00:01:40.439> it's 00:01:40.670 --> 00:01:40.680 align:start position:0% be enabl to read read it because it's 00:01:40.680 --> 00:01:46.910 align:start position:0% be enabl to read read it because it's too<00:01:41.280> boring<00:01:41.960> for<00:01:42.920> her 00:01:46.910 --> 00:01:46.920 align:start position:0% 00:01:46.920 --> 00:01:52.709 align:start position:0% um<00:01:47.920> for<00:01:48.280> proof<00:01:48.560> on<00:01:49.399> um<00:01:50.040> so<00:01:50.360> this<00:01:50.960> foral<00:01:51.960> for 00:01:52.709 --> 00:01:52.719 align:start position:0% um for proof on um so this foral for 00:01:52.719 --> 00:01:56.510 align:start position:0% um for proof on um so this foral for something<00:01:53.719> you<00:01:53.960> can<00:01:54.439> access<00:01:54.799> it<00:01:55.000> on<00:01:55.520> Twitter 00:01:56.510 --> 00:01:56.520 align:start position:0% something you can access it on Twitter 00:01:56.520 --> 00:02:00.149 align:start position:0% something you can access it on Twitter you<00:01:56.759> can<00:01:57.039> so<00:01:57.320> there<00:01:57.399> is<00:01:57.680> a<00:01:58.079> b<00:01:58.759> it's<00:01:59.159> here<00:01:59.399> it's 00:02:00.149 --> 00:02:00.159 align:start position:0% you can so there is a b it's here it's 00:02:00.159 --> 00:02:05.230 align:start position:0% you can so there is a b it's here it's IPC<00:02:01.159> board<00:02:02.159> uh<00:02:02.399> you<00:02:02.640> can<00:02:03.439> send<00:02:03.719> a<00:02:04.159> message<00:02:05.159> you 00:02:05.230 --> 00:02:05.240 align:start position:0% IPC board uh you can send a message you 00:02:05.240 --> 00:02:08.070 align:start position:0% IPC board uh you can send a message you can<00:02:05.399> tweet<00:02:05.799> to<00:02:06.000> it<00:02:06.439> uh<00:02:06.759> you<00:02:06.920> can<00:02:07.200> send<00:02:07.479> a 00:02:08.070 --> 00:02:08.080 align:start position:0% can tweet to it uh you can send a 00:02:08.080 --> 00:02:11.470 align:start position:0% can tweet to it uh you can send a formula<00:02:09.080> and<00:02:09.319> it<00:02:09.640> says<00:02:10.280> provable<00:02:11.080> or<00:02:11.280> not 00:02:11.470 --> 00:02:11.480 align:start position:0% formula and it says provable or not 00:02:11.480 --> 00:02:14.030 align:start position:0% formula and it says provable or not provable<00:02:12.440> and<00:02:12.680> when<00:02:12.800> it's<00:02:13.040> provable<00:02:13.520> it<00:02:13.640> shows 00:02:14.030 --> 00:02:14.040 align:start position:0% provable and when it's provable it shows 00:02:14.040 --> 00:02:14.910 align:start position:0% provable and when it's provable it shows you 00:02:14.910 --> 00:02:14.920 align:start position:0% you 00:02:14.920 --> 00:02:19.350 align:start position:0% you some<00:02:16.319> roofs<00:02:17.319> in<00:02:17.519> a<00:02:17.720> figure<00:02:18.599> did<00:02:18.720> you<00:02:18.920> write<00:02:19.120> it 00:02:19.350 --> 00:02:19.360 align:start position:0% some roofs in a figure did you write it 00:02:19.360 --> 00:02:24.550 align:start position:0% some roofs in a figure did you write it the<00:02:19.720> IPC<00:02:20.720> uh<00:02:20.920> a<00:02:21.080> friend<00:02:21.360> of<00:02:21.560> mine 00:02:24.550 --> 00:02:24.560 align:start position:0% 00:02:24.560 --> 00:02:26.430 align:start position:0% okay<00:02:25.560> but 00:02:26.430 --> 00:02:26.440 align:start position:0% okay but 00:02:26.440 --> 00:02:31.990 align:start position:0% okay but this<00:02:27.440> the<00:02:27.680> same<00:02:28.400> figures<00:02:29.400> are<00:02:30.200> there<00:02:30.360> in<00:02:31.000> 1934 00:02:31.990 --> 00:02:32.000 align:start position:0% this the same figures are there in 1934 00:02:32.000 --> 00:02:35.550 align:start position:0% this the same figures are there in 1934 this<00:02:32.160> is<00:02:32.959> originally<00:02:33.640> a<00:02:33.879> German<00:02:34.560> technology 00:02:35.550 --> 00:02:35.560 align:start position:0% this is originally a German technology 00:02:35.560 --> 00:02:37.229 align:start position:0% this is originally a German technology by 00:02:37.229 --> 00:02:37.239 align:start position:0% by 00:02:37.239 --> 00:02:40.710 align:start position:0% by the<00:02:38.239> um<00:02:38.800> every<00:02:39.159> mathematical 00:02:40.710 --> 00:02:40.720 align:start position:0% the um every mathematical 00:02:40.720 --> 00:02:46.630 align:start position:0% the um every mathematical Lans<00:02:42.000> have<00:02:43.120> um<00:02:44.120> and<00:02:44.640> then<00:02:45.640> yeah<00:02:45.959> the<00:02:46.519> the 00:02:46.630 --> 00:02:46.640 align:start position:0% Lans have um and then yeah the the 00:02:46.640 --> 00:02:50.070 align:start position:0% Lans have um and then yeah the the figure<00:02:47.640> there<00:02:47.879> was<00:02:48.159> this<00:02:48.400> thing<00:02:49.120> that<00:02:49.360> thing 00:02:50.070 --> 00:02:50.080 align:start position:0% figure there was this thing that thing 00:02:50.080 --> 00:02:56.750 align:start position:0% figure there was this thing that thing so<00:02:51.080> there<00:02:51.239> are<00:02:51.480> rules 00:02:56.750 --> 00:02:56.760 align:start position:0% 00:02:56.760 --> 00:03:00.430 align:start position:0% like<00:02:57.760> um<00:02:58.319> so<00:02:58.640> it's<00:02:58.879> called 00:03:00.430 --> 00:03:00.440 align:start position:0% like um so it's called 00:03:00.440 --> 00:03:03.390 align:start position:0% like um so it's called and<00:03:00.760> introduction<00:03:01.640> because<00:03:02.640> on<00:03:02.800> the<00:03:02.920> upper 00:03:03.390 --> 00:03:03.400 align:start position:0% and introduction because on the upper 00:03:03.400 --> 00:03:06.910 align:start position:0% and introduction because on the upper side<00:03:04.280> there's<00:03:04.560> no<00:03:04.840> and<00:03:05.280> symbol<00:03:06.280> on<00:03:06.440> the<00:03:06.560> bottom 00:03:06.910 --> 00:03:06.920 align:start position:0% side there's no and symbol on the bottom 00:03:06.920 --> 00:03:09.949 align:start position:0% side there's no and symbol on the bottom side<00:03:07.200> we<00:03:07.400> have<00:03:07.599> an<00:03:07.799> and<00:03:08.239> symbol<00:03:09.040> and<00:03:09.280> it's<00:03:09.760> it's 00:03:09.949 --> 00:03:09.959 align:start position:0% side we have an and symbol and it's it's 00:03:09.959 --> 00:03:12.509 align:start position:0% side we have an and symbol and it's it's saying<00:03:10.440> that<00:03:10.680> if<00:03:10.799> you<00:03:10.959> have<00:03:11.080> a<00:03:11.280> proof<00:03:11.560> of<00:03:11.879> a<00:03:12.280> and 00:03:12.509 --> 00:03:12.519 align:start position:0% saying that if you have a proof of a and 00:03:12.519 --> 00:03:15.390 align:start position:0% saying that if you have a proof of a and if<00:03:12.680> you<00:03:12.840> have<00:03:12.959> a<00:03:13.120> proof<00:03:13.400> of<00:03:13.680> B<00:03:14.360> you<00:03:14.599> have<00:03:14.879> a<00:03:15.280> you 00:03:15.390 --> 00:03:15.400 align:start position:0% if you have a proof of B you have a you 00:03:15.400 --> 00:03:18.430 align:start position:0% if you have a proof of B you have a you can<00:03:15.599> construct<00:03:16.239> proof 00:03:18.430 --> 00:03:18.440 align:start position:0% can construct proof 00:03:18.440 --> 00:03:20.869 align:start position:0% can construct proof of<00:03:19.440> and<00:03:19.680> this 00:03:20.869 --> 00:03:20.879 align:start position:0% of and this 00:03:20.879 --> 00:03:24.670 align:start position:0% of and this is<00:03:21.879> and<00:03:22.159> you<00:03:22.319> can<00:03:22.720> remove 00:03:24.670 --> 00:03:24.680 align:start position:0% is and you can remove 00:03:24.680 --> 00:03:26.550 align:start position:0% is and you can remove this<00:03:25.680> this 00:03:26.550 --> 00:03:26.560 align:start position:0% this this 00:03:26.560 --> 00:03:30.390 align:start position:0% this this is<00:03:27.560> so<00:03:27.799> on<00:03:27.920> the<00:03:28.400> side<00:03:28.599> we<00:03:28.760> have<00:03:29.200> an 00:03:30.390 --> 00:03:30.400 align:start position:0% is so on the side we have an 00:03:30.400 --> 00:03:33.110 align:start position:0% is so on the side we have an uh<00:03:30.640> on<00:03:30.920> the<00:03:31.680> bottom<00:03:32.040> part<00:03:32.280> you<00:03:32.400> don't<00:03:32.640> have<00:03:32.799> it 00:03:33.110 --> 00:03:33.120 align:start position:0% uh on the bottom part you don't have it 00:03:33.120 --> 00:03:35.990 align:start position:0% uh on the bottom part you don't have it and<00:03:33.519> when<00:03:33.680> you<00:03:33.799> have<00:03:33.920> a<00:03:34.040> proof<00:03:34.319> of<00:03:34.519> a<00:03:35.120> b<00:03:35.599> you<00:03:35.720> can 00:03:35.990 --> 00:03:36.000 align:start position:0% and when you have a proof of a b you can 00:03:36.000 --> 00:03:40.070 align:start position:0% and when you have a proof of a b you can have<00:03:36.439> you<00:03:36.560> can<00:03:36.760> construct<00:03:37.120> a<00:03:37.280> proof<00:03:37.560> of 00:03:40.070 --> 00:03:40.080 align:start position:0% have you can construct a proof of 00:03:40.080 --> 00:03:44.550 align:start position:0% have you can construct a proof of uh<00:03:41.080> if<00:03:41.200> you<00:03:41.519> wish<00:03:42.519> whichever<00:03:43.000> you<00:03:43.400> wish<00:03:44.400> and 00:03:44.550 --> 00:03:44.560 align:start position:0% uh if you wish whichever you wish and 00:03:44.560 --> 00:03:47.390 align:start position:0% uh if you wish whichever you wish and similarly<00:03:45.159> there's<00:03:45.799> all<00:03:46.799> when<00:03:46.959> you<00:03:47.120> have<00:03:47.239> a 00:03:47.390 --> 00:03:47.400 align:start position:0% similarly there's all when you have a 00:03:47.400 --> 00:03:50.550 align:start position:0% similarly there's all when you have a proof<00:03:47.640> of<00:03:47.840> R<00:03:48.680> you<00:03:49.040> can<00:03:49.319> construct<00:03:49.799> a<00:03:50.000> proof<00:03:50.280> of 00:03:50.550 --> 00:03:50.560 align:start position:0% proof of R you can construct a proof of 00:03:50.560 --> 00:03:53.869 align:start position:0% proof of R you can construct a proof of R<00:03:51.200> order<00:03:52.200> B<00:03:52.879> from 00:03:53.869 --> 00:03:53.879 align:start position:0% R order B from 00:03:53.879 --> 00:04:00.110 align:start position:0% R order B from it<00:03:55.120> um<00:03:56.120> so<00:03:57.079> this<00:03:57.360> guy<00:03:57.519> is<00:03:57.760> great<00:03:58.200> because<00:03:59.200> G 00:04:00.110 --> 00:04:00.120 align:start position:0% it um so this guy is great because G 00:04:00.120 --> 00:04:03.030 align:start position:0% it um so this guy is great because G this<00:04:00.280> system<00:04:00.840> and<00:04:01.439> this<00:04:01.560> is<00:04:01.799> still<00:04:02.200> used<00:04:02.640> today 00:04:03.030 --> 00:04:03.040 align:start position:0% this system and this is still used today 00:04:03.040 --> 00:04:05.710 align:start position:0% this system and this is still used today this<00:04:03.200> is<00:04:03.480> the<00:04:04.200> most<00:04:04.599> common<00:04:04.959> proof<00:04:05.360> system 00:04:05.710 --> 00:04:05.720 align:start position:0% this is the most common proof system 00:04:05.720 --> 00:04:08.750 align:start position:0% this is the most common proof system used<00:04:06.000> today<00:04:06.319> this<00:04:06.439> is<00:04:06.519> the<00:04:06.720> Bas<00:04:07.200> basis<00:04:07.439> of 00:04:08.750 --> 00:04:08.760 align:start position:0% used today this is the Bas basis of 00:04:08.760 --> 00:04:14.350 align:start position:0% used today this is the Bas basis of H<00:04:10.159> and<00:04:11.159> almost<00:04:11.640> all<00:04:12.000> modern<00:04:12.840> LS<00:04:13.640> no<00:04:13.840> I<00:04:14.000> went 00:04:14.350 --> 00:04:14.360 align:start position:0% H and almost all modern LS no I went 00:04:14.360 --> 00:04:17.670 align:start position:0% H and almost all modern LS no I went back 00:04:17.670 --> 00:04:17.680 align:start position:0% 00:04:17.680 --> 00:04:21.749 align:start position:0% sorry<00:04:18.680> yes<00:04:19.280> so<00:04:20.280> there<00:04:20.479> are<00:04:20.799> good<00:04:21.040> rules<00:04:21.440> and 00:04:21.749 --> 00:04:21.759 align:start position:0% sorry yes so there are good rules and 00:04:21.759 --> 00:04:24.090 align:start position:0% sorry yes so there are good rules and bad<00:04:22.240> rules<00:04:23.240> uh 00:04:24.090 --> 00:04:24.100 align:start position:0% bad rules uh 00:04:24.100 --> 00:04:26.310 align:start position:0% bad rules uh [Music] 00:04:26.310 --> 00:04:26.320 align:start position:0% [Music] 00:04:26.320 --> 00:04:29.749 align:start position:0% [Music] this<00:04:27.320> they<00:04:27.440> are<00:04:27.759> good<00:04:28.000> rules<00:04:28.560> because<00:04:29.440> they 00:04:29.749 --> 00:04:29.759 align:start position:0% this they are good rules because they 00:04:29.759 --> 00:04:32.670 align:start position:0% this they are good rules because they don't<00:04:29.960> allow<00:04:30.320> you<00:04:30.479> to<00:04:30.759> smuggle<00:04:31.759> things<00:04:32.240> into 00:04:32.670 --> 00:04:32.680 align:start position:0% don't allow you to smuggle things into 00:04:32.680 --> 00:04:36.270 align:start position:0% don't allow you to smuggle things into your<00:04:32.919> proofs<00:04:33.759> when<00:04:33.919> you<00:04:34.039> have<00:04:34.199> a<00:04:34.360> proof<00:04:34.720> of<00:04:35.360> a 00:04:36.270 --> 00:04:36.280 align:start position:0% your proofs when you have a proof of a 00:04:36.280 --> 00:04:38.350 align:start position:0% your proofs when you have a proof of a then<00:04:36.400> you<00:04:36.560> have<00:04:36.639> a<00:04:36.800> proof<00:04:37.039> of<00:04:37.280> B<00:04:37.840> you<00:04:37.919> can<00:04:38.120> get<00:04:38.240> a 00:04:38.350 --> 00:04:38.360 align:start position:0% then you have a proof of B you can get a 00:04:38.360 --> 00:04:40.749 align:start position:0% then you have a proof of B you can get a proof<00:04:38.600> of<00:04:38.840> r<00:04:39.400> b<00:04:39.680> but<00:04:39.800> the<00:04:39.880> only<00:04:40.160> thing<00:04:40.400> you<00:04:40.520> can 00:04:40.749 --> 00:04:40.759 align:start position:0% proof of r b but the only thing you can 00:04:40.759 --> 00:04:45.110 align:start position:0% proof of r b but the only thing you can do<00:04:41.080> with<00:04:41.280> it<00:04:41.560> is<00:04:42.039> to<00:04:42.600> introduce<00:04:43.600> b<00:04:44.240> or<00:04:44.520> R<00:04:44.880> and 00:04:45.110 --> 00:04:45.120 align:start position:0% do with it is to introduce b or R and 00:04:45.120 --> 00:04:47.150 align:start position:0% do with it is to introduce b or R and you<00:04:45.360> already<00:04:45.680> had<00:04:45.840> it<00:04:46.000> in<00:04:46.120> the<00:04:46.280> beginning<00:04:46.720> so 00:04:47.150 --> 00:04:47.160 align:start position:0% you already had it in the beginning so 00:04:47.160 --> 00:04:50.270 align:start position:0% you already had it in the beginning so nothing<00:04:47.600> new<00:04:48.560> happened<00:04:49.120> here<00:04:49.800> but<00:04:49.960> on<00:04:50.080> the 00:04:50.270 --> 00:04:50.280 align:start position:0% nothing new happened here but on the 00:04:50.280 --> 00:04:54.029 align:start position:0% nothing new happened here but on the right<00:04:50.520> hand<00:04:50.919> side<00:04:51.919> right<00:04:52.240> side<00:04:52.600> there<00:04:52.840> are<00:04:53.199> bad 00:04:54.029 --> 00:04:54.039 align:start position:0% right hand side right side there are bad 00:04:54.039 --> 00:04:57.749 align:start position:0% right hand side right side there are bad rules<00:04:55.039> uh<00:04:55.240> it's<00:04:55.520> called<00:04:55.840> TK<00:04:56.680> TK<00:04:57.120> introduction 00:04:57.749 --> 00:04:57.759 align:start position:0% rules uh it's called TK TK introduction 00:04:57.759 --> 00:04:59.990 align:start position:0% rules uh it's called TK TK introduction is<00:04:58.000> the<00:04:58.120> same<00:04:58.440> as<00:04:58.639> or<00:04:58.960> introduction<00:04:59.800> you<00:04:59.880> have 00:04:59.990 --> 00:05:00.000 align:start position:0% is the same as or introduction you have 00:05:00.000 --> 00:05:03.070 align:start position:0% is the same as or introduction you have a<00:05:00.120> proof<00:05:00.360> of<00:05:00.680> a<00:05:01.360> you<00:05:01.560> can<00:05:01.880> have<00:05:02.080> a<00:05:02.280> proof<00:05:02.560> of<00:05:02.800> a 00:05:03.070 --> 00:05:03.080 align:start position:0% a proof of a you can have a proof of a 00:05:03.080 --> 00:05:06.790 align:start position:0% a proof of a you can have a proof of a tonk<00:05:03.520> B<00:05:04.520> and<00:05:04.880> tonk<00:05:05.280> elimination<00:05:06.000> is<00:05:06.240> the<00:05:06.400> same 00:05:06.790 --> 00:05:06.800 align:start position:0% tonk B and tonk elimination is the same 00:05:06.800 --> 00:05:10.350 align:start position:0% tonk B and tonk elimination is the same as<00:05:07.800> and<00:05:08.120> elimination<00:05:08.880> and<00:05:09.080> when<00:05:09.240> you<00:05:09.440> have<00:05:09.800> a<00:05:10.039> t 00:05:10.350 --> 00:05:10.360 align:start position:0% as and elimination and when you have a t 00:05:10.360 --> 00:05:15.909 align:start position:0% as and elimination and when you have a t b<00:05:10.639> you<00:05:10.800> can<00:05:11.240> get<00:05:11.560> a<00:05:11.759> proof<00:05:12.039> of<00:05:12.600> B<00:05:13.600> and<00:05:14.240> this<00:05:14.919> this 00:05:15.909 --> 00:05:15.919 align:start position:0% b you can get a proof of B and this this 00:05:15.919 --> 00:05:19.909 align:start position:0% b you can get a proof of B and this this rules<00:05:16.400> allow<00:05:16.680> you<00:05:16.800> to<00:05:16.960> smug<00:05:17.479> the<00:05:18.919> new 00:05:19.909 --> 00:05:19.919 align:start position:0% rules allow you to smug the new 00:05:19.919 --> 00:05:22.270 align:start position:0% rules allow you to smug the new propositions<00:05:20.639> into<00:05:20.919> your<00:05:21.160> proof<00:05:21.479> and<00:05:21.800> you<00:05:22.000> can 00:05:22.270 --> 00:05:22.280 align:start position:0% propositions into your proof and you can 00:05:22.280 --> 00:05:24.870 align:start position:0% propositions into your proof and you can prove<00:05:22.759> foral<00:05:23.440> from<00:05:23.680> truth<00:05:24.000> or<00:05:24.199> something<00:05:24.600> like 00:05:24.870 --> 00:05:24.880 align:start position:0% prove foral from truth or something like 00:05:24.880 --> 00:05:27.189 align:start position:0% prove foral from truth or something like that<00:05:25.160> and<00:05:25.759> it's<00:05:25.919> all<00:05:26.160> about<00:05:26.560> Harmony<00:05:27.000> of 00:05:27.189 --> 00:05:27.199 align:start position:0% that and it's all about Harmony of 00:05:27.199 --> 00:05:31.390 align:start position:0% that and it's all about Harmony of introduction<00:05:27.800> and<00:05:27.960> elimination<00:05:28.759> and 00:05:31.390 --> 00:05:31.400 align:start position:0% introduction and elimination and 00:05:31.400 --> 00:05:35.790 align:start position:0% introduction and elimination and then<00:05:32.560> um<00:05:33.560> what<00:05:33.680> would<00:05:33.919> be<00:05:34.199> the<00:05:35.000> pro<00:05:35.400> rules 00:05:35.790 --> 00:05:35.800 align:start position:0% then um what would be the pro rules 00:05:35.800 --> 00:05:38.350 align:start position:0% then um what would be the pro rules imper<00:05:36.319> rules<00:05:36.600> for<00:05:36.840> solidity<00:05:37.400> programs<00:05:37.960> and 00:05:38.350 --> 00:05:38.360 align:start position:0% imper rules for solidity programs and 00:05:38.360 --> 00:05:39.950 align:start position:0% imper rules for solidity programs and here<00:05:38.680> I<00:05:38.840> meet<00:05:39.160> a 00:05:39.950 --> 00:05:39.960 align:start position:0% here I meet a 00:05:39.960 --> 00:05:43.790 align:start position:0% here I meet a problem<00:05:41.160> because<00:05:42.160> usually<00:05:42.720> okay<00:05:43.199> people<00:05:43.520> read 00:05:43.790 --> 00:05:43.800 align:start position:0% problem because usually okay people read 00:05:43.800 --> 00:05:46.070 align:start position:0% problem because usually okay people read solidity<00:05:44.319> code<00:05:44.600> and<00:05:44.840> get<00:05:44.960> an<00:05:45.160> idea<00:05:45.520> and<00:05:45.759> says 00:05:46.070 --> 00:05:46.080 align:start position:0% solidity code and get an idea and says 00:05:46.080 --> 00:05:48.629 align:start position:0% solidity code and get an idea and says this<00:05:46.240> works<00:05:46.479> or<00:05:46.639> this<00:05:46.800> doesn't<00:05:47.120> work<00:05:47.440> but<00:05:47.800> um 00:05:48.629 --> 00:05:48.639 align:start position:0% this works or this doesn't work but um 00:05:48.639 --> 00:05:51.510 align:start position:0% this works or this doesn't work but um who<00:05:48.880> who<00:05:49.039> told<00:05:49.400> you<00:05:49.680> to<00:05:50.639> who<00:05:50.800> told<00:05:51.039> you<00:05:51.280> that 00:05:51.510 --> 00:05:51.520 align:start position:0% who who told you to who told you that 00:05:51.520 --> 00:05:53.550 align:start position:0% who who told you to who told you that solidity<00:05:52.120> programs<00:05:52.479> are<00:05:52.680> executed<00:05:53.160> from<00:05:53.360> top 00:05:53.550 --> 00:05:53.560 align:start position:0% solidity programs are executed from top 00:05:53.560 --> 00:05:54.309 align:start position:0% solidity programs are executed from top to 00:05:54.309 --> 00:05:54.319 align:start position:0% to 00:05:54.319 --> 00:05:57.150 align:start position:0% to bottom<00:05:55.319> that<00:05:55.520> 3D<00:05:55.960> documentation<00:05:56.520> does<00:05:56.680> not 00:05:57.150 --> 00:05:57.160 align:start position:0% bottom that 3D documentation does not 00:05:57.160 --> 00:06:00.790 align:start position:0% bottom that 3D documentation does not say<00:05:58.160> might<00:05:58.400> be<00:05:58.840> bottom<00:05:59.120> to<00:05:59.360> top 00:06:00.790 --> 00:06:00.800 align:start position:0% say might be bottom to top 00:06:00.800 --> 00:06:02.909 align:start position:0% say might be bottom to top maybe<00:06:01.080> you<00:06:01.240> say<00:06:01.479> from<00:06:01.800> experiences<00:06:02.680> you 00:06:02.909 --> 00:06:02.919 align:start position:0% maybe you say from experiences you 00:06:02.919 --> 00:06:06.150 align:start position:0% maybe you say from experiences you tested<00:06:03.319> lity<00:06:04.120> codes<00:06:04.520> and<00:06:04.759> so<00:06:04.919> on<00:06:05.280> but<00:06:05.520> then<00:06:06.000> you 00:06:06.150 --> 00:06:06.160 align:start position:0% tested lity codes and so on but then you 00:06:06.160 --> 00:06:11.270 align:start position:0% tested lity codes and so on but then you are<00:06:06.680> actually<00:06:07.080> ring<00:06:07.720> on<00:06:08.000> the<00:06:08.960> compiler 00:06:11.270 --> 00:06:11.280 align:start position:0% are actually ring on the compiler 00:06:11.280 --> 00:06:15.830 align:start position:0% are actually ring on the compiler so<00:06:12.440> well<00:06:13.440> so<00:06:14.000> the<00:06:14.199> problem<00:06:14.599> here<00:06:14.880> is<00:06:15.280> you<00:06:15.720> when 00:06:15.830 --> 00:06:15.840 align:start position:0% so well so the problem here is you when 00:06:15.840 --> 00:06:17.710 align:start position:0% so well so the problem here is you when you<00:06:15.960> read<00:06:16.240> the<00:06:16.400> solidity<00:06:16.919> code<00:06:17.199> you<00:06:17.360> might<00:06:17.599> get 00:06:17.710 --> 00:06:17.720 align:start position:0% you read the solidity code you might get 00:06:17.720 --> 00:06:19.749 align:start position:0% you read the solidity code you might get a<00:06:17.880> different<00:06:18.280> idea<00:06:18.720> from<00:06:19.039> what 00:06:19.749 --> 00:06:19.759 align:start position:0% a different idea from what 00:06:19.759 --> 00:06:22.510 align:start position:0% a different idea from what happens<00:06:20.759> actually<00:06:21.440> when<00:06:21.599> you<00:06:21.800> compile<00:06:22.280> and 00:06:22.510 --> 00:06:22.520 align:start position:0% happens actually when you compile and 00:06:22.520 --> 00:06:28.990 align:start position:0% happens actually when you compile and deploy<00:06:22.880> the<00:06:23.280> code<00:06:24.479> so<00:06:25.479> I<00:06:25.960> chose<00:06:26.960> just<00:06:27.720> to<00:06:28.599> use 00:06:28.990 --> 00:06:29.000 align:start position:0% deploy the code so I chose just to use 00:06:29.000 --> 00:06:30.870 align:start position:0% deploy the code so I chose just to use the<00:06:29.120> solidity 00:06:30.870 --> 00:06:30.880 align:start position:0% the solidity 00:06:30.880 --> 00:06:35.430 align:start position:0% the solidity compiler<00:06:31.880> as<00:06:32.759> my<00:06:33.560> guidance<00:06:34.319> so<00:06:34.759> the<00:06:34.919> solidity 00:06:35.430 --> 00:06:35.440 align:start position:0% compiler as my guidance so the solidity 00:06:35.440 --> 00:06:38.510 align:start position:0% compiler as my guidance so the solidity compiler<00:06:36.039> knows<00:06:36.880> the<00:06:37.039> meaning<00:06:37.400> of<00:06:37.639> a<00:06:37.759> solidity 00:06:38.510 --> 00:06:38.520 align:start position:0% compiler knows the meaning of a solidity 00:06:38.520 --> 00:06:42.870 align:start position:0% compiler knows the meaning of a solidity code<00:06:39.520> I<00:06:39.720> get<00:06:39.960> an<00:06:40.199> EV<00:06:40.680> B<00:06:41.000> code<00:06:42.000> then<00:06:42.199> I<00:06:42.479> meet<00:06:42.720> a 00:06:42.870 --> 00:06:42.880 align:start position:0% code I get an EV B code then I meet a 00:06:42.880 --> 00:06:46.150 align:start position:0% code I get an EV B code then I meet a similar<00:06:43.280> problem<00:06:44.240> what<00:06:44.680> are<00:06:45.120> inference<00:06:45.680> rules 00:06:46.150 --> 00:06:46.160 align:start position:0% similar problem what are inference rules 00:06:46.160 --> 00:06:50.909 align:start position:0% similar problem what are inference rules for<00:06:47.120> no<00:06:47.319> ebm<00:06:47.880> B<00:06:48.240> code<00:06:49.160> then<00:06:49.800> actually<00:06:50.240> I<00:06:50.400> can 00:06:50.909 --> 00:06:50.919 align:start position:0% for no ebm B code then actually I can 00:06:50.919 --> 00:06:56.710 align:start position:0% for no ebm B code then actually I can answer<00:06:52.280> um<00:06:53.280> rules<00:06:54.240> would<00:06:54.560> look<00:06:54.840> like<00:06:55.120> this<00:06:55.720> um 00:06:56.710 --> 00:06:56.720 align:start position:0% answer um rules would look like this um 00:06:56.720 --> 00:06:58.230 align:start position:0% answer um rules would look like this um when<00:06:57.280> if<00:06:57.440> you 00:06:58.230 --> 00:06:58.240 align:start position:0% when if you 00:06:58.240 --> 00:07:01.070 align:start position:0% when if you know<00:06:59.240> if<00:06:59.639> your 00:07:01.070 --> 00:07:01.080 align:start position:0% know if your 00:07:01.080 --> 00:07:05.869 align:start position:0% know if your EDM<00:07:02.080> machine<00:07:02.759> is<00:07:03.680> at<00:07:03.840> the<00:07:04.039> second 00:07:05.869 --> 00:07:05.879 align:start position:0% EDM machine is at the second 00:07:05.879 --> 00:07:10.420 align:start position:0% EDM machine is at the second position<00:07:06.879> and<00:07:07.360> the<00:07:07.560> set<00:07:07.840> stack<00:07:08.160> element<00:07:08.680> is<00:07:09.240> 0 00:07:10.420 --> 00:07:10.430 align:start position:0% position and the set stack element is 0 00:07:10.430 --> 00:07:11.629 align:start position:0% position and the set stack element is 0 [Music] 00:07:11.629 --> 00:07:11.639 align:start position:0% [Music] 00:07:11.639 --> 00:07:15.629 align:start position:0% [Music] x60<00:07:12.639> if<00:07:12.800> you<00:07:13.080> know<00:07:13.599> this<00:07:13.960> state<00:07:14.400> does<00:07:14.639> not<00:07:14.919> go 00:07:15.629 --> 00:07:15.639 align:start position:0% x60 if you know this state does not go 00:07:15.639 --> 00:07:19.710 align:start position:0% x60 if you know this state does not go wrong<00:07:16.639> then<00:07:17.319> from<00:07:17.639> this<00:07:17.919> you<00:07:18.080> can<00:07:18.319> imper 00:07:19.710 --> 00:07:19.720 align:start position:0% wrong then from this you can imper 00:07:19.720 --> 00:07:24.230 align:start position:0% wrong then from this you can imper that<00:07:20.720> Anan<00:07:21.560> machine<00:07:22.440> at<00:07:22.560> the<00:07:22.800> first<00:07:23.360> position 00:07:24.230 --> 00:07:24.240 align:start position:0% that Anan machine at the first position 00:07:24.240 --> 00:07:27.189 align:start position:0% that Anan machine at the first position with<00:07:24.520> stock<00:07:24.960> empty<00:07:25.960> does<00:07:26.160> not<00:07:26.400> go<00:07:26.599> wrong 00:07:27.189 --> 00:07:27.199 align:start position:0% with stock empty does not go wrong 00:07:27.199 --> 00:07:29.150 align:start position:0% with stock empty does not go wrong because<00:07:27.639> the<00:07:27.759> only<00:07:28.000> thing<00:07:28.199> it<00:07:28.360> can<00:07:28.599> do<00:07:28.879> is 00:07:29.150 --> 00:07:29.160 align:start position:0% because the only thing it can do is 00:07:29.160 --> 00:07:34.670 align:start position:0% because the only thing it can do is either<00:07:29.879> go<00:07:30.120> out<00:07:30.280> of<00:07:30.560> gas<00:07:31.720> or<00:07:32.720> go<00:07:32.919> one<00:07:33.199> step<00:07:34.199> to 00:07:34.670 --> 00:07:34.680 align:start position:0% either go out of gas or go one step to 00:07:34.680 --> 00:07:38.150 align:start position:0% either go out of gas or go one step to the<00:07:34.919> original<00:07:35.919> the<00:07:36.080> second<00:07:36.479> position<00:07:36.919> I<00:07:37.360> about 00:07:38.150 --> 00:07:38.160 align:start position:0% the original the second position I about 00:07:38.160 --> 00:07:43.070 align:start position:0% the original the second position I about so<00:07:38.759> this<00:07:38.960> kind<00:07:39.160> of<00:07:39.319> inance<00:07:39.759> rules<00:07:40.120> are<00:07:40.840> good 00:07:43.070 --> 00:07:43.080 align:start position:0% so this kind of inance rules are good 00:07:43.080 --> 00:07:45.950 align:start position:0% so this kind of inance rules are good for 00:07:45.950 --> 00:07:45.960 align:start position:0% for 00:07:45.960 --> 00:07:49.710 align:start position:0% for machine<00:07:46.960> I<00:07:47.080> cheated<00:07:47.440> a<00:07:47.639> bit<00:07:47.960> on<00:07:48.479> why<00:07:48.800> did 00:07:49.710 --> 00:07:49.720 align:start position:0% machine I cheated a bit on why did 00:07:49.720 --> 00:07:54.029 align:start position:0% machine I cheated a bit on why did I<00:07:50.720> treat<00:07:51.479> solidity<00:07:52.159> and<00:07:52.560> the<00:07:53.199> virtual<00:07:53.639> machine 00:07:54.029 --> 00:07:54.039 align:start position:0% I treat solidity and the virtual machine 00:07:54.039 --> 00:07:57.550 align:start position:0% I treat solidity and the virtual machine differently<00:07:54.680> and<00:07:55.000> it's<00:07:55.800> because<00:07:56.759> just<00:07:57.360> if 00:07:57.550 --> 00:07:57.560 align:start position:0% differently and it's because just if 00:07:57.560 --> 00:08:00.790 align:start position:0% differently and it's because just if there<00:07:57.680> is<00:07:57.800> a<00:07:57.960> spec<00:07:58.400> or<00:07:58.639> not<00:07:59.759> and<00:08:00.080> if<00:08:00.319> the<00:08:00.479> spec 00:08:00.790 --> 00:08:00.800 align:start position:0% there is a spec or not and if the spec 00:08:00.800 --> 00:08:02.909 align:start position:0% there is a spec or not and if the spec is<00:08:00.960> written<00:08:01.319> in<00:08:01.520> a<00:08:01.680> more<00:08:02.000> machine<00:08:02.360> readable 00:08:02.909 --> 00:08:02.919 align:start position:0% is written in a more machine readable 00:08:02.919 --> 00:08:05.830 align:start position:0% is written in a more machine readable way<00:08:03.120> it's<00:08:04.000> better<00:08:05.000> uh<00:08:05.240> there's<00:08:05.560> one 00:08:05.830 --> 00:08:05.840 align:start position:0% way it's better uh there's one 00:08:05.840 --> 00:08:08.550 align:start position:0% way it's better uh there's one programming<00:08:06.280> language<00:08:07.280> who<00:08:07.840> spec 00:08:08.550 --> 00:08:08.560 align:start position:0% programming language who spec 00:08:08.560 --> 00:08:12.070 align:start position:0% programming language who spec authorative<00:08:09.520> is<00:08:09.879> written<00:08:10.240> for<00:08:10.479> theor<00:08:11.080> provs 00:08:12.070 --> 00:08:12.080 align:start position:0% authorative is written for theor provs 00:08:12.080 --> 00:08:13.510 align:start position:0% authorative is written for theor provs it's<00:08:12.360> called 00:08:13.510 --> 00:08:13.520 align:start position:0% it's called 00:08:13.520 --> 00:08:17.230 align:start position:0% it's called KPM<00:08:14.520> that's<00:08:14.919> the<00:08:15.080> best<00:08:15.479> language<00:08:16.240> to<00:08:16.800> prove 00:08:17.230 --> 00:08:17.240 align:start position:0% KPM that's the best language to prove 00:08:17.240 --> 00:08:20.230 align:start position:0% KPM that's the best language to prove programs<00:08:17.680> on<00:08:18.560> and<00:08:18.759> then<00:08:19.080> there<00:08:19.199> are<00:08:19.479> some 00:08:20.230 --> 00:08:20.240 align:start position:0% programs on and then there are some 00:08:20.240 --> 00:08:22.350 align:start position:0% programs on and then there are some programming<00:08:20.720> languages<00:08:21.240> for 00:08:22.350 --> 00:08:22.360 align:start position:0% programming languages for 00:08:22.360 --> 00:08:25.589 align:start position:0% programming languages for spefications<00:08:23.360> are<00:08:23.599> translated<00:08:24.319> into<00:08:25.080> proof 00:08:25.589 --> 00:08:25.599 align:start position:0% spefications are translated into proof 00:08:25.599 --> 00:08:28.430 align:start position:0% spefications are translated into proof Checkers<00:08:26.599> C 00:08:28.430 --> 00:08:28.440 align:start position:0% Checkers C 00:08:28.440 --> 00:08:30.230 align:start position:0% Checkers C 11 00:08:30.230 --> 00:08:30.240 align:start position:0% 11 00:08:30.240 --> 00:08:33.990 align:start position:0% 11 JavaScript<00:08:31.240> there<00:08:31.400> are<00:08:32.000> some<00:08:33.000> languages<00:08:33.680> with 00:08:33.990 --> 00:08:34.000 align:start position:0% JavaScript there are some languages with 00:08:34.000 --> 00:08:36.149 align:start position:0% JavaScript there are some languages with speak<00:08:34.560> with<00:08:34.839> mathematical<00:08:35.440> definitions 00:08:36.149 --> 00:08:36.159 align:start position:0% speak with mathematical definitions 00:08:36.159 --> 00:08:39.630 align:start position:0% speak with mathematical definitions maybe<00:08:36.599> they<00:08:36.760> are<00:08:37.039> easier<00:08:37.479> to<00:08:37.760> translate<00:08:38.360> into 00:08:39.630 --> 00:08:39.640 align:start position:0% maybe they are easier to translate into 00:08:39.640 --> 00:08:42.949 align:start position:0% maybe they are easier to translate into proas<00:08:40.640> and<00:08:40.839> there<00:08:40.959> are<00:08:41.200> language<00:08:41.919> for<00:08:42.599> English 00:08:42.949 --> 00:08:42.959 align:start position:0% proas and there are language for English 00:08:42.959 --> 00:08:46.269 align:start position:0% proas and there are language for English on<00:08:43.200> the<00:08:43.399> specs<00:08:43.800> and<00:08:44.000> so<00:08:44.720> on 00:08:46.269 --> 00:08:46.279 align:start position:0% on the specs and so on 00:08:46.279 --> 00:08:50.350 align:start position:0% on the specs and so on and<00:08:47.279> I<00:08:47.440> found<00:08:47.920> the<00:08:48.080> evm<00:08:48.720> a<00:08:48.880> little<00:08:49.120> bit<00:08:49.519> or 00:08:50.350 --> 00:08:50.360 align:start position:0% and I found the evm a little bit or 00:08:50.360 --> 00:08:55.550 align:start position:0% and I found the evm a little bit or maybe<00:08:50.680> more<00:08:51.440> easier<00:08:52.160> to<00:08:52.360> deal 00:08:55.550 --> 00:08:55.560 align:start position:0% 00:08:55.560 --> 00:08:59.670 align:start position:0% with<00:08:56.560> of<00:08:56.760> course<00:08:57.480> um 00:08:59.670 --> 00:08:59.680 align:start position:0% with of course um 00:08:59.680 --> 00:09:02.509 align:start position:0% with of course um there<00:08:59.800> are<00:09:00.160> problems<00:09:00.720> in<00:09:01.120> the<00:09:01.480> evbm 00:09:02.509 --> 00:09:02.519 align:start position:0% there are problems in the evbm 00:09:02.519 --> 00:09:06.670 align:start position:0% there are problems in the evbm specification<00:09:03.519> the<00:09:04.079> paper<00:09:04.680> so<00:09:05.279> I<00:09:06.200> I've<00:09:06.440> been 00:09:06.670 --> 00:09:06.680 align:start position:0% specification the paper so I I've been 00:09:06.680 --> 00:09:10.030 align:start position:0% specification the paper so I I've been opening<00:09:07.560> some<00:09:08.320> requests<00:09:09.240> to<00:09:09.440> the<00:09:09.640> yellow 00:09:10.030 --> 00:09:10.040 align:start position:0% opening some requests to the yellow 00:09:10.040 --> 00:09:12.990 align:start position:0% opening some requests to the yellow paper<00:09:10.480> repository<00:09:11.200> but<00:09:11.560> this<00:09:11.720> is<00:09:12.000> manageable 00:09:12.990 --> 00:09:13.000 align:start position:0% paper repository but this is manageable 00:09:13.000 --> 00:09:15.750 align:start position:0% paper repository but this is manageable and<00:09:13.200> this<00:09:13.279> is<00:09:13.440> manageable<00:09:14.320> I<00:09:14.480> knew<00:09:14.800> that 00:09:15.750 --> 00:09:15.760 align:start position:0% and this is manageable I knew that 00:09:15.760 --> 00:09:19.829 align:start position:0% and this is manageable I knew that because<00:09:17.040> many<00:09:18.040> client<00:09:18.560> implementers<00:09:19.440> already 00:09:19.829 --> 00:09:19.839 align:start position:0% because many client implementers already 00:09:19.839 --> 00:09:24.110 align:start position:0% because many client implementers already looked<00:09:20.240> at<00:09:20.480> it<00:09:20.800> and<00:09:21.120> found<00:09:21.720> problems 00:09:24.110 --> 00:09:24.120 align:start position:0% looked at it and found problems 00:09:24.120 --> 00:09:26.750 align:start position:0% looked at it and found problems and<00:09:25.120> the<00:09:25.320> document<00:09:25.680> is 00:09:26.750 --> 00:09:26.760 align:start position:0% and the document is 00:09:26.760 --> 00:09:30.110 align:start position:0% and the document is arrived<00:09:27.760> uh<00:09:28.040> so<00:09:28.720> I<00:09:28.880> just<00:09:29.079> had<00:09:29.440> to<00:09:29.600> implement 00:09:30.110 --> 00:09:30.120 align:start position:0% arrived uh so I just had to implement 00:09:30.120 --> 00:09:32.790 align:start position:0% arrived uh so I just had to implement another<00:09:30.440> I<00:09:30.880> virtual<00:09:31.240> machine<00:09:31.760> in 00:09:32.790 --> 00:09:32.800 align:start position:0% another I virtual machine in 00:09:32.800 --> 00:09:37.190 align:start position:0% another I virtual machine in aover<00:09:33.800> uh<00:09:33.959> it<00:09:34.120> took<00:09:34.560> like<00:09:35.200> 50<00:09:35.600> pages<00:09:36.440> in<00:09:36.959> type 00:09:37.190 --> 00:09:37.200 align:start position:0% aover uh it took like 50 pages in type 00:09:37.200 --> 00:09:41.030 align:start position:0% aover uh it took like 50 pages in type set<00:09:37.480> in<00:09:37.680> a<00:09:38.279> papers<00:09:39.279> but<00:09:39.480> it's<00:09:39.720> kind<00:09:39.880> of<00:09:40.120> easy<00:09:40.440> so 00:09:41.030 --> 00:09:41.040 align:start position:0% set in a papers but it's kind of easy so 00:09:41.040 --> 00:09:43.150 align:start position:0% set in a papers but it's kind of easy so hope<00:09:41.399> removes<00:09:41.800> the<00:09:41.959> top<00:09:42.279> element<00:09:42.760> of<00:09:42.959> the 00:09:43.150 --> 00:09:43.160 align:start position:0% hope removes the top element of the 00:09:43.160 --> 00:09:47.990 align:start position:0% hope removes the top element of the stack<00:09:43.720> and<00:09:44.560> changes<00:09:45.120> the<00:09:46.120> the<00:09:46.279> B<00:09:46.720> the<00:09:46.880> St<00:09:47.160> is<00:09:47.720> to 00:09:47.990 --> 00:09:48.000 align:start position:0% stack and changes the the B the St is to 00:09:48.000 --> 00:09:51.550 align:start position:0% stack and changes the the B the St is to the<00:09:48.600> TA<00:09:49.240> of<00:09:49.519> the<00:09:49.720> St<00:09:50.120> and 00:09:51.550 --> 00:09:51.560 align:start position:0% the TA of the St and 00:09:51.560 --> 00:09:55.470 align:start position:0% the TA of the St and so<00:09:52.560> and<00:09:52.800> then<00:09:53.440> when<00:09:53.600> you<00:09:53.760> want<00:09:54.040> to<00:09:54.600> verify<00:09:55.200> a 00:09:55.470 --> 00:09:55.480 align:start position:0% so and then when you want to verify a 00:09:55.480 --> 00:09:57.870 align:start position:0% so and then when you want to verify a program<00:09:55.880> you<00:09:56.040> have<00:09:56.200> to<00:09:56.440> past<00:09:56.839> your<00:09:57.079> program<00:09:57.480> in 00:09:57.870 --> 00:09:57.880 align:start position:0% program you have to past your program in 00:09:57.880 --> 00:10:00.590 align:start position:0% program you have to past your program in proof<00:09:58.160> Checker<00:09:59.160> this<00:09:59.760> there's<00:10:00.040> nothing<00:10:00.360> deep 00:10:00.590 --> 00:10:00.600 align:start position:0% proof Checker this there's nothing deep 00:10:00.600 --> 00:10:03.550 align:start position:0% proof Checker this there's nothing deep in<00:10:00.760> it<00:10:00.959> it's<00:10:01.360> just<00:10:01.680> huge<00:10:02.240> and<00:10:02.920> you<00:10:03.200> you<00:10:03.360> just 00:10:03.550 --> 00:10:03.560 align:start position:0% in it it's just huge and you you just 00:10:03.560 --> 00:10:05.990 align:start position:0% in it it's just huge and you you just have<00:10:03.680> to<00:10:03.839> copy<00:10:04.040> and<00:10:04.240> paste<00:10:04.480> it<00:10:05.399> actually<00:10:05.760> this 00:10:05.990 --> 00:10:06.000 align:start position:0% have to copy and paste it actually this 00:10:06.000 --> 00:10:09.030 align:start position:0% have to copy and paste it actually this POS<00:10:06.360> some<00:10:06.600> problems<00:10:07.120> in<00:10:08.040> the<00:10:08.279> proof<00:10:08.560> check 00:10:09.030 --> 00:10:09.040 align:start position:0% POS some problems in the proof check 00:10:09.040 --> 00:10:12.310 align:start position:0% POS some problems in the proof check isabo<00:10:10.040> because 00:10:12.310 --> 00:10:12.320 align:start position:0% isabo because 00:10:12.320 --> 00:10:15.790 align:start position:0% isabo because um<00:10:13.320> yeah<00:10:14.240> looking<00:10:14.600> up<00:10:14.800> an<00:10:15.040> instruction<00:10:15.560> from 00:10:15.790 --> 00:10:15.800 align:start position:0% um yeah looking up an instruction from 00:10:15.800 --> 00:10:19.150 align:start position:0% um yeah looking up an instruction from this<00:10:16.000> this<00:10:16.360> took<00:10:16.640> so<00:10:17.160> too<00:10:17.440> much<00:10:17.800> time<00:10:18.600> so<00:10:18.839> I<00:10:18.959> had 00:10:19.150 --> 00:10:19.160 align:start position:0% this this took so too much time so I had 00:10:19.160 --> 00:10:22.590 align:start position:0% this this took so too much time so I had to<00:10:19.800> transform<00:10:20.519> it<00:10:20.760> into<00:10:21.079> a<00:10:21.240> binary<00:10:21.560> tree 00:10:22.590 --> 00:10:22.600 align:start position:0% to transform it into a binary tree 00:10:22.600 --> 00:10:25.069 align:start position:0% to transform it into a binary tree but<00:10:23.600> it's<00:10:23.880> just 00:10:25.069 --> 00:10:25.079 align:start position:0% but it's just 00:10:25.079 --> 00:10:27.430 align:start position:0% but it's just bureaucracy<00:10:26.079> and<00:10:26.240> then<00:10:26.480> this<00:10:26.600> is<00:10:26.839> the<00:10:27.079> most 00:10:27.430 --> 00:10:27.440 align:start position:0% bureaucracy and then this is the most 00:10:27.440 --> 00:10:30.150 align:start position:0% bureaucracy and then this is the most important<00:10:28.079> question<00:10:28.519> when<00:10:28.720> you<00:10:28.959> want<00:10:29.519> to<00:10:30.000> the 00:10:30.150 --> 00:10:30.160 align:start position:0% important question when you want to the 00:10:30.160 --> 00:10:32.269 align:start position:0% important question when you want to the formal<00:10:30.600> verification<00:10:31.560> in<00:10:31.640> the<00:10:31.800> end<00:10:32.079> what<00:10:32.200> do 00:10:32.269 --> 00:10:32.279 align:start position:0% formal verification in the end what do 00:10:32.279 --> 00:10:33.590 align:start position:0% formal verification in the end what do you 00:10:33.590 --> 00:10:33.600 align:start position:0% you 00:10:33.600 --> 00:10:37.430 align:start position:0% you want<00:10:34.600> and<00:10:34.839> you<00:10:35.079> have<00:10:35.279> to<00:10:35.959> say<00:10:36.279> what<00:10:36.440> you<00:10:36.639> want 00:10:37.430 --> 00:10:37.440 align:start position:0% want and you have to say what you want 00:10:37.440 --> 00:10:41.150 align:start position:0% want and you have to say what you want and<00:10:38.440> uh<00:10:39.240> the<00:10:39.399> first<00:10:39.680> option<00:10:40.040> is<00:10:40.560> the<00:10:40.800> account 00:10:41.150 --> 00:10:41.160 align:start position:0% and uh the first option is the account 00:10:41.160 --> 00:10:44.310 align:start position:0% and uh the first option is the account should<00:10:41.440> do<00:10:41.720> expected<00:10:42.560> things<00:10:43.160> and<00:10:43.600> for<00:10:43.880> that<00:10:44.160> I 00:10:44.310 --> 00:10:44.320 align:start position:0% should do expected things and for that I 00:10:44.320 --> 00:10:47.509 align:start position:0% should do expected things and for that I have<00:10:44.519> to<00:10:44.880> interview<00:10:45.880> the<00:10:46.560> people<00:10:46.880> who<00:10:47.079> wrote 00:10:47.509 --> 00:10:47.519 align:start position:0% have to interview the people who wrote 00:10:47.519 --> 00:10:50.389 align:start position:0% have to interview the people who wrote this<00:10:47.959> and<00:10:48.200> what<00:10:48.360> we<00:10:48.600> expect 00:10:50.389 --> 00:10:50.399 align:start position:0% this and what we expect 00:10:50.399 --> 00:10:53.790 align:start position:0% this and what we expect and<00:10:51.399> this<00:10:51.560> is<00:10:51.800> not<00:10:52.519> easy<00:10:53.040> because<00:10:53.560> the 00:10:53.790 --> 00:10:53.800 align:start position:0% and this is not easy because the 00:10:53.800 --> 00:10:56.230 align:start position:0% and this is not easy because the question<00:10:54.200> is<00:10:54.519> very<00:10:54.800> informal<00:10:55.320> what<00:10:55.480> do<00:10:55.560> you 00:10:56.230 --> 00:10:56.240 align:start position:0% question is very informal what do you 00:10:56.240 --> 00:10:59.670 align:start position:0% question is very informal what do you want<00:10:57.240> but<00:10:58.000> my<00:10:58.320> requirement<00:10:58.959> for<00:10:59.320> the<00:10:59.399> answer 00:10:59.670 --> 00:10:59.680 align:start position:0% want but my requirement for the answer 00:10:59.680 --> 00:11:01.629 align:start position:0% want but my requirement for the answer is<00:10:59.880> very<00:11:00.160> detailed<00:11:00.639> I<00:11:00.760> have<00:11:00.880> to<00:11:01.079> type<00:11:01.279> it<00:11:01.399> into 00:11:01.629 --> 00:11:01.639 align:start position:0% is very detailed I have to type it into 00:11:01.639 --> 00:11:05.030 align:start position:0% is very detailed I have to type it into a<00:11:01.839> proof<00:11:02.079> Checker<00:11:02.560> so<00:11:02.959> I<00:11:03.240> ask<00:11:03.519> a<00:11:03.680> very<00:11:04.040> informal 00:11:05.030 --> 00:11:05.040 align:start position:0% a proof Checker so I ask a very informal 00:11:05.040 --> 00:11:07.150 align:start position:0% a proof Checker so I ask a very informal question<00:11:05.399> and<00:11:05.560> I<00:11:05.800> expect<00:11:06.200> a<00:11:06.440> very<00:11:06.720> detailed 00:11:07.150 --> 00:11:07.160 align:start position:0% question and I expect a very detailed 00:11:07.160 --> 00:11:11.629 align:start position:0% question and I expect a very detailed answer<00:11:07.519> and<00:11:07.839> that's<00:11:08.360> uh<00:11:09.120> not<00:11:10.120> easy<00:11:10.440> to<00:11:10.639> conduct 00:11:11.629 --> 00:11:11.639 align:start position:0% answer and that's uh not easy to conduct 00:11:11.639 --> 00:11:14.670 align:start position:0% answer and that's uh not easy to conduct um<00:11:12.639> at<00:11:12.800> least<00:11:13.040> I<00:11:13.200> have<00:11:13.399> to<00:11:13.959> show<00:11:14.279> something 00:11:14.670 --> 00:11:14.680 align:start position:0% um at least I have to show something 00:11:14.680 --> 00:11:17.629 align:start position:0% um at least I have to show something working<00:11:15.079> before<00:11:15.480> I<00:11:15.639> do<00:11:15.839> something<00:11:16.560> so<00:11:17.440> the 00:11:17.629 --> 00:11:17.639 align:start position:0% working before I do something so the 00:11:17.639 --> 00:11:20.949 align:start position:0% working before I do something so the second<00:11:17.920> choice<00:11:18.160> is<00:11:18.360> the<00:11:18.519> account<00:11:19.120> shouldn't 00:11:20.949 --> 00:11:20.959 align:start position:0% second choice is the account shouldn't 00:11:20.959 --> 00:11:27.069 align:start position:0% second choice is the account shouldn't do<00:11:21.959> things<00:11:22.639> wrong<00:11:23.639> and<00:11:23.920> usually<00:11:25.240> for<00:11:26.240> smart 00:11:27.069 --> 00:11:27.079 align:start position:0% do things wrong and usually for smart 00:11:27.079 --> 00:11:29.990 align:start position:0% do things wrong and usually for smart contract<00:11:28.079> the<00:11:28.240> balance<00:11:28.720> shouldn't<00:11:29.399> decrease 00:11:29.990 --> 00:11:30.000 align:start position:0% contract the balance shouldn't decrease 00:11:30.000 --> 00:11:34.710 align:start position:0% contract the balance shouldn't decrease unless<00:11:31.000> an<00:11:31.320> authorized<00:11:32.160> account<00:11:33.160> there 00:11:34.710 --> 00:11:34.720 align:start position:0% unless an authorized account there 00:11:34.720 --> 00:11:38.670 align:start position:0% unless an authorized account there so<00:11:35.720> and<00:11:36.279> with<00:11:36.839> this<00:11:37.839> a<00:11:38.000> non-authorized 00:11:38.670 --> 00:11:38.680 align:start position:0% so and with this a non-authorized 00:11:38.680 --> 00:11:41.670 align:start position:0% so and with this a non-authorized account<00:11:39.480> cannot<00:11:39.959> make<00:11:40.200> itself<00:11:40.720> authorized<00:11:41.360> or 00:11:41.670 --> 00:11:41.680 align:start position:0% account cannot make itself authorized or 00:11:41.680 --> 00:11:44.990 align:start position:0% account cannot make itself authorized or make<00:11:41.959> any<00:11:42.399> any<00:11:43.160> anybody<00:11:43.560> else<00:11:44.000> authorized 00:11:44.990 --> 00:11:45.000 align:start position:0% make any any anybody else authorized 00:11:45.000 --> 00:11:48.269 align:start position:0% make any any anybody else authorized because<00:11:45.839> that's<00:11:46.839> kind<00:11:47.040> of<00:11:47.519> makes<00:11:47.880> the<00:11:48.040> first 00:11:48.269 --> 00:11:48.279 align:start position:0% because that's kind of makes the first 00:11:48.279 --> 00:11:50.230 align:start position:0% because that's kind of makes the first point<00:11:48.560> meaning 00:11:50.230 --> 00:11:50.240 align:start position:0% point meaning 00:11:50.240 --> 00:11:52.670 align:start position:0% point meaning this<00:11:51.240> uh<00:11:51.360> so<00:11:51.560> I<00:11:51.680> have<00:11:51.839> to<00:11:52.040> type<00:11:52.360> these 00:11:52.670 --> 00:11:52.680 align:start position:0% this uh so I have to type these 00:11:52.680 --> 00:11:55.190 align:start position:0% this uh so I have to type these conditions<00:11:53.000> in<00:11:53.120> the<00:11:53.279> proof<00:11:53.560> check<00:11:54.120> it's<00:11:54.959> it's 00:11:55.190 --> 00:11:55.200 align:start position:0% conditions in the proof check it's it's 00:11:55.200 --> 00:11:57.710 align:start position:0% conditions in the proof check it's it's straight<00:11:55.639> for 00:11:57.710 --> 00:11:57.720 align:start position:0% straight for 00:11:57.720 --> 00:12:04.030 align:start position:0% straight for um<00:11:58.720> the<00:11:59.440> us<00:11:59.880> more<00:12:00.880> but<00:12:01.839> yeah 00:12:04.030 --> 00:12:04.040 align:start position:0% um the us more but yeah 00:12:04.040 --> 00:12:09.550 align:start position:0% um the us more but yeah here<00:12:05.200> saying<00:12:06.279> um<00:12:07.279> the<00:12:07.480> storage<00:12:07.959> index<00:12:08.560> zero 00:12:09.550 --> 00:12:09.560 align:start position:0% here saying um the storage index zero 00:12:09.560 --> 00:12:13.189 align:start position:0% here saying um the storage index zero does<00:12:09.800> not<00:12:10.120> contain<00:12:10.800> the<00:12:11.040> cor's<00:12:11.959> address<00:12:12.959> this 00:12:13.189 --> 00:12:13.199 align:start position:0% does not contain the cor's address this 00:12:13.199 --> 00:12:15.790 align:start position:0% does not contain the cor's address this part<00:12:13.480> is<00:12:13.680> for<00:12:14.279> non 00:12:15.790 --> 00:12:15.800 align:start position:0% part is for non 00:12:15.800 --> 00:12:19.509 align:start position:0% part is for non authorized<00:12:17.079> and<00:12:18.079> the<00:12:18.279> the<00:12:18.600> contract<00:12:19.079> is<00:12:19.240> still 00:12:19.509 --> 00:12:19.519 align:start position:0% authorized and the the contract is still 00:12:19.519 --> 00:12:23.670 align:start position:0% authorized and the the contract is still marked<00:12:20.079> active<00:12:20.680> and<00:12:20.880> so<00:12:21.079> on<00:12:21.480> under<00:12:21.920> these 00:12:23.670 --> 00:12:23.680 align:start position:0% marked active and so on under these 00:12:23.680 --> 00:12:26.590 align:start position:0% marked active and so on under these conditions<00:12:24.680> the<00:12:24.920> expectation<00:12:25.839> is<00:12:26.199> that<00:12:26.440> the 00:12:26.590 --> 00:12:26.600 align:start position:0% conditions the expectation is that the 00:12:26.600 --> 00:12:29.430 align:start position:0% conditions the expectation is that the balance<00:12:27.000> does<00:12:27.199> not<00:12:27.639> decrease<00:12:28.639> I<00:12:28.760> tried<00:12:29.040> to<00:12:29.240> to 00:12:29.430 --> 00:12:29.440 align:start position:0% balance does not decrease I tried to to 00:12:29.440 --> 00:12:33.069 align:start position:0% balance does not decrease I tried to to prove<00:12:29.800> this<00:12:30.000> Mon<00:12:30.519> and<00:12:30.880> I<00:12:31.000> failed<00:12:31.600> because 00:12:33.069 --> 00:12:33.079 align:start position:0% prove this Mon and I failed because 00:12:33.079 --> 00:12:38.110 align:start position:0% prove this Mon and I failed because I<00:12:34.079> forgot<00:12:34.680> to<00:12:35.279> say<00:12:35.880> one<00:12:36.839> condition<00:12:37.839> in<00:12:37.959> the 00:12:38.110 --> 00:12:38.120 align:start position:0% I forgot to say one condition in the 00:12:38.120 --> 00:12:41.110 align:start position:0% I forgot to say one condition in the precondition<00:12:38.959> so<00:12:39.160> I<00:12:39.320> forgot<00:12:39.720> to<00:12:40.040> say<00:12:40.880> the 00:12:41.110 --> 00:12:41.120 align:start position:0% precondition so I forgot to say the 00:12:41.120 --> 00:12:44.069 align:start position:0% precondition so I forgot to say the account<00:12:41.519> is<00:12:41.839> still<00:12:42.480> active<00:12:43.480> and<00:12:43.680> then<00:12:43.920> the 00:12:44.069 --> 00:12:44.079 align:start position:0% account is still active and then the 00:12:44.079 --> 00:12:50.389 align:start position:0% account is still active and then the proof<00:12:44.880> fails<00:12:45.880> so<00:12:46.639> I<00:12:46.920> know<00:12:47.360> that<00:12:47.600> something<00:12:47.920> is 00:12:50.389 --> 00:12:50.399 align:start position:0% 00:12:50.399 --> 00:12:54.350 align:start position:0% wrong<00:12:51.480> um<00:12:52.480> and<00:12:52.639> then<00:12:52.959> after<00:12:53.399> typing<00:12:53.800> in<00:12:54.079> your 00:12:54.350 --> 00:12:54.360 align:start position:0% wrong um and then after typing in your 00:12:54.360 --> 00:12:55.910 align:start position:0% wrong um and then after typing in your requirement<00:12:55.000> what<00:12:55.160> you 00:12:55.910 --> 00:12:55.920 align:start position:0% requirement what you 00:12:55.920 --> 00:13:00.389 align:start position:0% requirement what you wish<00:12:56.920> um<00:12:57.079> you<00:12:57.240> have<00:12:57.399> to<00:12:57.639> prove<00:12:58.160> that<00:12:58.480> thing<00:12:58.760> you 00:13:00.389 --> 00:13:00.399 align:start position:0% wish um you have to prove that thing you 00:13:00.399 --> 00:13:06.310 align:start position:0% wish um you have to prove that thing you um<00:13:01.399> this<00:13:02.079> is<00:13:03.079> just<00:13:03.760> straight<00:13:04.240> forward 00:13:06.310 --> 00:13:06.320 align:start position:0% um this is just straight forward 00:13:06.320 --> 00:13:09.350 align:start position:0% um this is just straight forward you<00:13:07.320> you<00:13:07.800> you<00:13:08.000> you<00:13:08.120> have<00:13:08.240> to<00:13:08.440> type<00:13:08.760> things<00:13:09.120> on 00:13:09.350 --> 00:13:09.360 align:start position:0% you you you you have to type things on 00:13:09.360 --> 00:13:13.030 align:start position:0% you you you you have to type things on the<00:13:09.639> upper<00:13:10.760> pain<00:13:11.760> and<00:13:11.920> the<00:13:12.040> lower<00:13:12.399> pain<00:13:12.760> is 00:13:13.030 --> 00:13:13.040 align:start position:0% the upper pain and the lower pain is 00:13:13.040 --> 00:13:16.269 align:start position:0% the upper pain and the lower pain is just<00:13:13.360> the<00:13:13.519> machine's<00:13:14.600> respones<00:13:15.600> and<00:13:15.880> here<00:13:16.120> the 00:13:16.269 --> 00:13:16.279 align:start position:0% just the machine's respones and here the 00:13:16.279 --> 00:13:20.069 align:start position:0% just the machine's respones and here the machine<00:13:16.639> is<00:13:16.880> responding<00:13:17.800> some<00:13:18.800> very<00:13:19.560> long 00:13:20.069 --> 00:13:20.079 align:start position:0% machine is responding some very long 00:13:20.079 --> 00:13:25.110 align:start position:0% machine is responding some very long proof<00:13:20.560> gold<00:13:21.399> but<00:13:21.680> I<00:13:21.920> find<00:13:22.920> a<00:13:23.199> ni<00:13:23.959> sentence<00:13:24.959> in 00:13:25.110 --> 00:13:25.120 align:start position:0% proof gold but I find a ni sentence in 00:13:25.120 --> 00:13:28.069 align:start position:0% proof gold but I find a ni sentence in the<00:13:25.279> middle<00:13:25.560> of<00:13:25.680> the<00:13:25.959> go<00:13:26.959> saying<00:13:27.600> okay<00:13:27.880> well 00:13:28.069 --> 00:13:28.079 align:start position:0% the middle of the go saying okay well 00:13:28.079 --> 00:13:31.870 align:start position:0% the middle of the go saying okay well now<00:13:28.279> it<00:13:28.440> wants<00:13:28.760> to<00:13:28.920> do<00:13:29.279> case<00:13:29.519> analysis<00:13:30.639> on<00:13:31.639> if 00:13:31.870 --> 00:13:31.880 align:start position:0% now it wants to do case analysis on if 00:13:31.880 --> 00:13:35.550 align:start position:0% now it wants to do case analysis on if the<00:13:32.040> Cent<00:13:32.440> data<00:13:32.880> is<00:13:33.240> empty<00:13:33.639> or<00:13:33.839> not<00:13:34.560> empty 00:13:35.550 --> 00:13:35.560 align:start position:0% the Cent data is empty or not empty 00:13:35.560 --> 00:13:38.389 align:start position:0% the Cent data is empty or not empty actually<00:13:35.959> whenever<00:13:36.440> you<00:13:37.199> try<00:13:37.399> to<00:13:37.639> verify<00:13:38.160> a 00:13:38.389 --> 00:13:38.399 align:start position:0% actually whenever you try to verify a 00:13:38.399 --> 00:13:41.030 align:start position:0% actually whenever you try to verify a smart<00:13:38.760> contract<00:13:39.519> generated<00:13:40.160> by<00:13:40.360> solidity 00:13:41.030 --> 00:13:41.040 align:start position:0% smart contract generated by solidity 00:13:41.040 --> 00:13:45.189 align:start position:0% smart contract generated by solidity it's<00:13:41.760> the<00:13:42.040> first<00:13:42.880> question<00:13:43.880> the<00:13:44.120> Cod<00:13:44.680> C<00:13:45.000> data 00:13:45.189 --> 00:13:45.199 align:start position:0% it's the first question the Cod C data 00:13:45.199 --> 00:13:50.350 align:start position:0% it's the first question the Cod C data is<00:13:45.360> empty<00:13:45.720> or<00:13:46.000> not<00:13:47.000> um<00:13:47.800> so<00:13:48.199> I<00:13:48.480> tell<00:13:48.880> it<00:13:49.399> do<00:13:50.120> a 00:13:50.350 --> 00:13:50.360 align:start position:0% is empty or not um so I tell it do a 00:13:50.360 --> 00:13:53.710 align:start position:0% is empty or not um so I tell it do a case<00:13:50.639> analysis<00:13:51.079> on<00:13:51.399> this<00:13:51.880> and<00:13:52.120> it<00:13:52.600> splits<00:13:53.480> the 00:13:53.710 --> 00:13:53.720 align:start position:0% case analysis on this and it splits the 00:13:53.720 --> 00:13:57.430 align:start position:0% case analysis on this and it splits the cases<00:13:54.399> and<00:13:54.839> then<00:13:55.000> I<00:13:55.120> have<00:13:55.240> to<00:13:55.399> prove<00:13:55.720> two 00:13:57.430 --> 00:13:57.440 align:start position:0% cases and then I have to prove two 00:13:57.440 --> 00:14:00.230 align:start position:0% cases and then I have to prove two goals<00:13:58.440> if<00:13:58.600> the<00:13:58.720> Cent<00:13:59.120> dat<00:13:59.320> is<00:13:59.519> empty<00:14:00.079> the 00:14:00.230 --> 00:14:00.240 align:start position:0% goals if the Cent dat is empty the 00:14:00.240 --> 00:14:02.749 align:start position:0% goals if the Cent dat is empty the requirements<00:14:00.920> hold<00:14:01.600> if<00:14:01.759> the<00:14:01.920> sent<00:14:02.399> data<00:14:02.600> is 00:14:02.749 --> 00:14:02.759 align:start position:0% requirements hold if the sent data is 00:14:02.759 --> 00:14:05.870 align:start position:0% requirements hold if the sent data is non<00:14:03.040> empty<00:14:03.680> the<00:14:03.839> requirements<00:14:04.519> hold<00:14:05.360> and<00:14:05.600> with 00:14:05.870 --> 00:14:05.880 align:start position:0% non empty the requirements hold and with 00:14:05.880 --> 00:14:08.790 align:start position:0% non empty the requirements hold and with this<00:14:06.720> with<00:14:06.880> the<00:14:07.079> usual<00:14:07.519> inference<00:14:08.000> rules<00:14:08.600> I 00:14:08.790 --> 00:14:08.800 align:start position:0% this with the usual inference rules I 00:14:08.800 --> 00:14:14.069 align:start position:0% this with the usual inference rules I get<00:14:09.600> the<00:14:10.600> result<00:14:11.440> so<00:14:11.639> I<00:14:11.759> have<00:14:12.240> to<00:14:13.240> just<00:14:13.560> repeat 00:14:14.069 --> 00:14:14.079 align:start position:0% get the result so I have to just repeat 00:14:14.079 --> 00:14:18.350 align:start position:0% get the result so I have to just repeat this<00:14:14.279> case<00:14:14.519> analysis<00:14:15.240> until<00:14:16.079> all<00:14:16.440> cases 00:14:18.350 --> 00:14:18.360 align:start position:0% this case analysis until all cases 00:14:18.360 --> 00:14:21.350 align:start position:0% this case analysis until all cases finished<00:14:19.360> and<00:14:19.560> then<00:14:19.920> the<00:14:20.120> post<00:14:20.519> conditions 00:14:21.350 --> 00:14:21.360 align:start position:0% finished and then the post conditions 00:14:21.360 --> 00:14:25.749 align:start position:0% finished and then the post conditions hold<00:14:22.360> and<00:14:22.560> then<00:14:23.320> after<00:14:23.560> I<00:14:23.720> finish<00:14:24.199> this 00:14:25.749 --> 00:14:25.759 align:start position:0% hold and then after I finish this 00:14:25.759 --> 00:14:28.829 align:start position:0% hold and then after I finish this um<00:14:26.759> okay<00:14:27.079> now<00:14:27.360> the<00:14:27.519> machine<00:14:27.839> is<00:14:28.079> convinced 00:14:28.829 --> 00:14:28.839 align:start position:0% um okay now the machine is convinced 00:14:28.839 --> 00:14:32.629 align:start position:0% um okay now the machine is convinced that<00:14:29.399> the<00:14:29.680> the<00:14:30.519> hold<00:14:31.519> um<00:14:31.839> there's<00:14:32.120> still<00:14:32.360> a 00:14:32.629 --> 00:14:32.639 align:start position:0% that the the hold um there's still a 00:14:32.639 --> 00:14:37.030 align:start position:0% that the the hold um there's still a question<00:14:33.079> does<00:14:33.320> this<00:14:33.600> match<00:14:33.920> the<00:14:34.519> reality<00:14:35.680> um 00:14:37.030 --> 00:14:37.040 align:start position:0% question does this match the reality um 00:14:37.040 --> 00:14:40.590 align:start position:0% question does this match the reality um I<00:14:38.040> the<00:14:38.199> next<00:14:38.480> thing<00:14:38.680> I<00:14:38.800> have<00:14:38.959> to<00:14:39.160> do<00:14:39.639> is<00:14:40.320> I<00:14:40.440> have 00:14:40.590 --> 00:14:40.600 align:start position:0% I the next thing I have to do is I have 00:14:40.600 --> 00:14:43.350 align:start position:0% I the next thing I have to do is I have to<00:14:40.880> test<00:14:41.680> my<00:14:41.920> own<00:14:42.320> evm 00:14:43.350 --> 00:14:43.360 align:start position:0% to test my own evm 00:14:43.360 --> 00:14:46.030 align:start position:0% to test my own evm implementation<00:14:44.360> against<00:14:44.920> the<00:14:45.440> usual 00:14:46.030 --> 00:14:46.040 align:start position:0% implementation against the usual 00:14:46.040 --> 00:14:48.030 align:start position:0% implementation against the usual standard<00:14:46.600> virtual<00:14:47.000> machine 00:14:48.030 --> 00:14:48.040 align:start position:0% standard virtual machine 00:14:48.040 --> 00:14:53.629 align:start position:0% standard virtual machine tests<00:14:49.040> for<00:14:49.399> which<00:14:50.320> um<00:14:50.639> CPP<00:14:51.440> client<00:14:52.440> uh<00:14:52.639> go<00:14:52.880> CLI 00:14:53.629 --> 00:14:53.639 align:start position:0% tests for which um CPP client uh go CLI 00:14:53.639 --> 00:14:57.389 align:start position:0% tests for which um CPP client uh go CLI and<00:14:53.959> last<00:14:54.880> all<00:14:55.880> variated<00:14:56.519> so<00:14:56.759> they<00:14:56.880> were 00:14:57.389 --> 00:14:57.399 align:start position:0% and last all variated so they were 00:14:57.399 --> 00:14:59.870 align:start position:0% and last all variated so they were compared<00:14:58.040> with<00:14:58.399> the<00:14:58.600> standard<00:14:59.199> test<00:14:59.560> and<00:14:59.759> I 00:14:59.870 --> 00:14:59.880 align:start position:0% compared with the standard test and I 00:14:59.880 --> 00:15:04.269 align:start position:0% compared with the standard test and I have<00:15:00.040> to<00:15:00.800> use<00:15:01.279> this<00:15:01.519> virtual<00:15:01.920> machine<00:15:02.320> test 00:15:04.269 --> 00:15:04.279 align:start position:0% have to use this virtual machine test 00:15:04.279 --> 00:15:07.550 align:start position:0% have to use this virtual machine test to<00:15:05.279> try 00:15:07.550 --> 00:15:07.560 align:start position:0% to try 00:15:07.560 --> 00:15:10.990 align:start position:0% to try my<00:15:08.560> evm<00:15:09.120> implementation<00:15:10.120> in<00:15:10.279> this<00:15:10.480> theorem 00:15:10.990 --> 00:15:11.000 align:start position:0% my evm implementation in this theorem 00:15:11.000 --> 00:15:14.189 align:start position:0% my evm implementation in this theorem Pro<00:15:12.000> if<00:15:12.160> this<00:15:12.279> is<00:15:12.480> wrong<00:15:12.880> I<00:15:13.279> and<00:15:13.639> this<00:15:13.920> this 00:15:14.189 --> 00:15:14.199 align:start position:0% Pro if this is wrong I and this this 00:15:14.199 --> 00:15:17.030 align:start position:0% Pro if this is wrong I and this this theorem<00:15:14.560> is<00:15:14.720> garbage<00:15:15.240> because<00:15:15.720> it's<00:15:16.279> uh<00:15:16.720> some 00:15:17.030 --> 00:15:17.040 align:start position:0% theorem is garbage because it's uh some 00:15:17.040 --> 00:15:20.310 align:start position:0% theorem is garbage because it's uh some about<00:15:17.360> some<00:15:18.040> other<00:15:18.440> machine<00:15:19.040> so<00:15:19.880> I<00:15:20.040> have<00:15:20.160> I 00:15:20.310 --> 00:15:20.320 align:start position:0% about some other machine so I have I 00:15:20.320 --> 00:15:23.269 align:start position:0% about some other machine so I have I really<00:15:20.560> have<00:15:20.680> to<00:15:20.839> do 00:15:23.269 --> 00:15:23.279 align:start position:0% 00:15:23.279 --> 00:15:26.389 align:start position:0% this<00:15:24.279> um<00:15:24.560> if<00:15:24.680> you<00:15:24.839> think<00:15:25.120> you<00:15:25.279> can<00:15:25.480> do 00:15:26.389 --> 00:15:26.399 align:start position:0% this um if you think you can do 00:15:26.399 --> 00:15:30.150 align:start position:0% this um if you think you can do better<00:15:27.399> there<00:15:27.560> will<00:15:27.720> be<00:15:27.880> a<00:15:28.079> workshop<00:15:28.680> about 00:15:30.150 --> 00:15:30.160 align:start position:0% better there will be a workshop about 00:15:30.160 --> 00:15:31.990 align:start position:0% better there will be a workshop about actually<00:15:30.519> this<00:15:30.600> is<00:15:30.800> not<00:15:31.079> just<00:15:31.319> about<00:15:31.639> program 00:15:31.990 --> 00:15:32.000 align:start position:0% actually this is not just about program 00:15:32.000 --> 00:15:35.480 align:start position:0% actually this is not just about program verification<00:15:32.920> this<00:15:33.000> is