WEBVTT Kind: captions Language: en 00:00:00.000 --> 00:00:04.350 align:start position:0% foreign 00:00:04.350 --> 00:00:04.360 align:start position:0% 00:00:04.360 --> 00:00:13.490 align:start position:0% [Music] 00:00:13.490 --> 00:00:13.500 align:start position:0% 00:00:13.500 --> 00:00:16.310 align:start position:0% yes<00:00:14.099> so<00:00:14.519> this<00:00:15.000> came<00:00:15.420> out<00:00:15.599> of<00:00:15.719> like<00:00:15.960> a<00:00:16.139> fun 00:00:16.310 --> 00:00:16.320 align:start position:0% yes so this came out of like a fun 00:00:16.320 --> 00:00:18.170 align:start position:0% yes so this came out of like a fun project<00:00:16.740> I<00:00:17.340> wanted<00:00:17.460> to<00:00:17.640> write<00:00:17.760> like<00:00:17.940> a<00:00:18.060> full 00:00:18.170 --> 00:00:18.180 align:start position:0% project I wanted to write like a full 00:00:18.180 --> 00:00:19.910 align:start position:0% project I wanted to write like a full like<00:00:18.480> an<00:00:18.720> end-to-end 00:00:19.910 --> 00:00:19.920 align:start position:0% like an end-to-end 00:00:19.920 --> 00:00:22.609 align:start position:0% like an end-to-end um<00:00:20.520> symbolic<00:00:21.180> execution<00:00:21.600> engine<00:00:21.779> in<00:00:22.140> solidity 00:00:22.609 --> 00:00:22.619 align:start position:0% um symbolic execution engine in solidity 00:00:22.619 --> 00:00:25.609 align:start position:0% um symbolic execution engine in solidity with<00:00:23.160> including<00:00:23.880> the<00:00:24.119> the<00:00:24.300> solver<00:00:24.900> that<00:00:25.140> we 00:00:25.609 --> 00:00:25.619 align:start position:0% with including the the solver that we 00:00:25.619 --> 00:00:27.769 align:start position:0% with including the the solver that we usually<00:00:25.859> use<00:00:25.980> in<00:00:26.160> the<00:00:26.460> in<00:00:26.640> the<00:00:26.820> background 00:00:27.769 --> 00:00:27.779 align:start position:0% usually use in the in the background 00:00:27.779 --> 00:00:30.830 align:start position:0% usually use in the in the background and<00:00:28.320> this<00:00:28.500> is<00:00:28.619> actually<00:00:28.859> pretty<00:00:29.160> fun<00:00:29.420> so<00:00:30.420> I 00:00:30.830 --> 00:00:30.840 align:start position:0% and this is actually pretty fun so I 00:00:30.840 --> 00:00:33.889 align:start position:0% and this is actually pretty fun so I want<00:00:30.960> to<00:00:31.080> share<00:00:31.320> with<00:00:31.859> you<00:00:32.040> what<00:00:33.000> this<00:00:33.120> does<00:00:33.840> um 00:00:33.889 --> 00:00:33.899 align:start position:0% want to share with you what this does um 00:00:33.899 --> 00:00:35.870 align:start position:0% want to share with you what this does um so<00:00:34.559> a<00:00:34.739> few<00:00:34.860> questions<00:00:35.040> for<00:00:35.340> like<00:00:35.520> audience 00:00:35.870 --> 00:00:35.880 align:start position:0% so a few questions for like audience 00:00:35.880 --> 00:00:38.990 align:start position:0% so a few questions for like audience adjustment<00:00:36.360> who<00:00:36.719> yes<00:00:37.020> who<00:00:37.500> here<00:00:37.860> was<00:00:38.280> at 00:00:38.990 --> 00:00:39.000 align:start position:0% adjustment who yes who here was at 00:00:39.000 --> 00:00:41.090 align:start position:0% adjustment who yes who here was at Harry's<00:00:39.480> talk<00:00:39.660> yesterday<00:00:39.899> about 00:00:41.090 --> 00:00:41.100 align:start position:0% Harry's talk yesterday about 00:00:41.100 --> 00:00:43.790 align:start position:0% Harry's talk yesterday about symbolic<00:00:41.940> computation<00:00:42.360> in<00:00:42.719> your 00:00:43.790 --> 00:00:43.800 align:start position:0% symbolic computation in your 00:00:43.800 --> 00:00:46.369 align:start position:0% symbolic computation in your okay<00:00:44.340> who<00:00:45.120> knows<00:00:45.360> what<00:00:45.540> symbolic<00:00:45.960> execution 00:00:46.369 --> 00:00:46.379 align:start position:0% okay who knows what symbolic execution 00:00:46.379 --> 00:00:47.990 align:start position:0% okay who knows what symbolic execution is 00:00:47.990 --> 00:00:48.000 align:start position:0% is 00:00:48.000 --> 00:00:50.389 align:start position:0% is okay<00:00:48.480> nice<00:00:48.780> I<00:00:49.260> am<00:00:49.379> prepared<00:00:49.680> to<00:00:49.800> tell<00:00:49.980> you<00:00:50.100> what 00:00:50.389 --> 00:00:50.399 align:start position:0% okay nice I am prepared to tell you what 00:00:50.399 --> 00:00:52.670 align:start position:0% okay nice I am prepared to tell you what it<00:00:50.520> is<00:00:50.640> though<00:00:50.879> for<00:00:51.480> the<00:00:51.660> ones<00:00:51.840> who<00:00:52.200> don't<00:00:52.500> know 00:00:52.670 --> 00:00:52.680 align:start position:0% it is though for the ones who don't know 00:00:52.680 --> 00:00:54.470 align:start position:0% it is though for the ones who don't know so<00:00:52.980> I'm<00:00:53.520> quickly<00:00:53.820> going<00:00:54.000> to<00:00:54.059> go<00:00:54.180> over<00:00:54.239> some 00:00:54.470 --> 00:00:54.480 align:start position:0% so I'm quickly going to go over some 00:00:54.480 --> 00:00:56.090 align:start position:0% so I'm quickly going to go over some slides<00:00:54.840> and<00:00:55.199> then<00:00:55.320> we're<00:00:55.500> going<00:00:55.680> to<00:00:55.800> move<00:00:55.920> to 00:00:56.090 --> 00:00:56.100 align:start position:0% slides and then we're going to move to 00:00:56.100 --> 00:00:58.549 align:start position:0% slides and then we're going to move to code<00:00:56.399> this<00:00:57.180> word<00:00:57.360> or<00:00:57.719> these<00:00:58.079> expressions<00:00:58.379> are 00:00:58.549 --> 00:00:58.559 align:start position:0% code this word or these expressions are 00:00:58.559 --> 00:00:59.990 align:start position:0% code this word or these expressions are thrown<00:00:58.739> around<00:00:58.920> a<00:00:59.160> lot<00:00:59.219> like<00:00:59.399> what<00:00:59.640> symbolic 00:00:59.990 --> 00:01:00.000 align:start position:0% thrown around a lot like what symbolic 00:01:00.000 --> 00:01:02.029 align:start position:0% thrown around a lot like what symbolic execution<00:01:00.360> what's<00:01:00.780> constraints<00:01:01.320> what's<00:01:01.500> sn2 00:01:02.029 --> 00:01:02.039 align:start position:0% execution what's constraints what's sn2 00:01:02.039 --> 00:01:04.310 align:start position:0% execution what's constraints what's sn2 silver<00:01:02.219> what's<00:01:02.579> all<00:01:02.760> that<00:01:02.940> stuff<00:01:03.120> and 00:01:04.310 --> 00:01:04.320 align:start position:0% silver what's all that stuff and 00:01:04.320 --> 00:01:05.690 align:start position:0% silver what's all that stuff and a<00:01:04.619> lot<00:01:04.739> of<00:01:04.799> people<00:01:04.920> know<00:01:05.040> what<00:01:05.159> it<00:01:05.280> is<00:01:05.400> but<00:01:05.519> if 00:01:05.690 --> 00:01:05.700 align:start position:0% a lot of people know what it is but if 00:01:05.700 --> 00:01:06.710 align:start position:0% a lot of people know what it is but if you<00:01:05.760> don't<00:01:05.880> know<00:01:06.000> what<00:01:06.060> it<00:01:06.180> is<00:01:06.299> they<00:01:06.479> kind<00:01:06.659> of 00:01:06.710 --> 00:01:06.720 align:start position:0% you don't know what it is they kind of 00:01:06.720 --> 00:01:08.690 align:start position:0% you don't know what it is they kind of like<00:01:06.840> you<00:01:06.900> feel<00:01:07.080> left<00:01:07.260> out<00:01:07.500> and<00:01:08.040> these<00:01:08.580> words 00:01:08.690 --> 00:01:08.700 align:start position:0% like you feel left out and these words 00:01:08.700 --> 00:01:10.070 align:start position:0% like you feel left out and these words are<00:01:08.880> used<00:01:09.119> very 00:01:10.070 --> 00:01:10.080 align:start position:0% are used very 00:01:10.080 --> 00:01:12.289 align:start position:0% are used very um<00:01:10.140> trivially<00:01:10.740> even<00:01:11.400> though<00:01:11.640> they're<00:01:12.060> not 00:01:12.289 --> 00:01:12.299 align:start position:0% um trivially even though they're not 00:01:12.299 --> 00:01:14.630 align:start position:0% um trivially even though they're not really<00:01:12.540> they're<00:01:12.900> simple<00:01:13.140> but<00:01:13.380> not<00:01:13.500> trivial<00:01:13.979> so 00:01:14.630 --> 00:01:14.640 align:start position:0% really they're simple but not trivial so 00:01:14.640 --> 00:01:15.710 align:start position:0% really they're simple but not trivial so first<00:01:14.760> I<00:01:14.939> want<00:01:15.060> to<00:01:15.180> tell<00:01:15.240> you<00:01:15.299> what's<00:01:15.479> not 00:01:15.710 --> 00:01:15.720 align:start position:0% first I want to tell you what's not 00:01:15.720 --> 00:01:17.390 align:start position:0% first I want to tell you what's not symbolic<00:01:16.200> execution 00:01:17.390 --> 00:01:17.400 align:start position:0% symbolic execution 00:01:17.400 --> 00:01:19.730 align:start position:0% symbolic execution and<00:01:18.119> that's<00:01:18.360> concrete<00:01:18.840> execution<00:01:19.260> so<00:01:19.560> let's 00:01:19.730 --> 00:01:19.740 align:start position:0% and that's concrete execution so let's 00:01:19.740 --> 00:01:23.270 align:start position:0% and that's concrete execution so let's say<00:01:19.920> you<00:01:20.100> have<00:01:20.340> oh<00:01:21.060> yeah<00:01:21.299> last<00:01:21.720> question<00:01:22.280> who 00:01:23.270 --> 00:01:23.280 align:start position:0% say you have oh yeah last question who 00:01:23.280 --> 00:01:27.109 align:start position:0% say you have oh yeah last question who can<00:01:24.060> read<00:01:24.600> assembly<00:01:25.439> like<00:01:25.619> this 00:01:27.109 --> 00:01:27.119 align:start position:0% can read assembly like this 00:01:27.119 --> 00:01:29.149 align:start position:0% can read assembly like this nice<00:01:27.479> okay<00:01:27.720> that's<00:01:28.020> very<00:01:28.200> good 00:01:29.149 --> 00:01:29.159 align:start position:0% nice okay that's very good 00:01:29.159 --> 00:01:31.370 align:start position:0% nice okay that's very good um<00:01:29.220> so<00:01:29.520> let's<00:01:29.640> say<00:01:29.759> we<00:01:29.939> have<00:01:30.119> this<00:01:30.540> assembly 00:01:31.370 --> 00:01:31.380 align:start position:0% um so let's say we have this assembly 00:01:31.380 --> 00:01:34.249 align:start position:0% um so let's say we have this assembly here<00:01:31.619> from<00:01:32.159> evm<00:01:32.700> and<00:01:33.540> we<00:01:33.659> want<00:01:33.840> to<00:01:33.960> run<00:01:34.080> the 00:01:34.249 --> 00:01:34.259 align:start position:0% here from evm and we want to run the 00:01:34.259 --> 00:01:36.289 align:start position:0% here from evm and we want to run the concrete<00:01:34.500> execution<00:01:34.920> over<00:01:35.159> it 00:01:36.289 --> 00:01:36.299 align:start position:0% concrete execution over it 00:01:36.299 --> 00:01:39.230 align:start position:0% concrete execution over it so<00:01:36.720> let's<00:01:36.900> say<00:01:37.020> we<00:01:37.200> have<00:01:37.380> this<00:01:37.680> call<00:01:37.920> data 00:01:39.230 --> 00:01:39.240 align:start position:0% so let's say we have this call data 00:01:39.240 --> 00:01:41.450 align:start position:0% so let's say we have this call data um<00:01:39.299> it's<00:01:39.780> 12<00:01:40.079> in<00:01:40.320> hacks<00:01:40.740> I<00:01:41.159> don't<00:01:41.280> know<00:01:41.340> what 00:01:41.450 --> 00:01:41.460 align:start position:0% um it's 12 in hacks I don't know what 00:01:41.460 --> 00:01:43.370 align:start position:0% um it's 12 in hacks I don't know what that<00:01:41.640> is<00:01:41.759> and<00:01:42.060> what<00:01:42.479> is<00:01:42.659> that<00:01:42.780> in<00:01:42.900> decimal<00:01:43.200> like 00:01:43.370 --> 00:01:43.380 align:start position:0% that is and what is that in decimal like 00:01:43.380 --> 00:01:45.770 align:start position:0% that is and what is that in decimal like 20<00:01:43.860> no 00:01:45.770 --> 00:01:45.780 align:start position:0% 20 no 00:01:45.780 --> 00:01:47.929 align:start position:0% 20 no 18.<00:01:46.680> yeah<00:01:46.860> it<00:01:47.040> makes<00:01:47.159> sense 00:01:47.929 --> 00:01:47.939 align:start position:0% 18. yeah it makes sense 00:01:47.939 --> 00:01:50.149 align:start position:0% 18. yeah it makes sense so<00:01:48.479> if<00:01:48.720> you<00:01:48.840> run<00:01:49.079> this<00:01:49.439> program<00:01:49.619> without<00:01:49.860> call 00:01:50.149 --> 00:01:50.159 align:start position:0% so if you run this program without call 00:01:50.159 --> 00:01:51.649 align:start position:0% so if you run this program without call data<00:01:50.460> what<00:01:50.579> do<00:01:50.759> we<00:01:50.880> get 00:01:51.649 --> 00:01:51.659 align:start position:0% data what do we get 00:01:51.659 --> 00:01:53.330 align:start position:0% data what do we get um<00:01:51.720> what's<00:01:52.259> like<00:01:52.560> there's<00:01:52.680> no<00:01:52.799> return<00:01:52.979> here<00:01:53.280> is 00:01:53.330 --> 00:01:53.340 align:start position:0% um what's like there's no return here is 00:01:53.340 --> 00:01:54.770 align:start position:0% um what's like there's no return here is let's<00:01:53.520> just<00:01:53.640> consider<00:01:53.880> the<00:01:54.000> top<00:01:54.180> of<00:01:54.360> the<00:01:54.479> stack 00:01:54.770 --> 00:01:54.780 align:start position:0% let's just consider the top of the stack 00:01:54.780 --> 00:01:56.690 align:start position:0% let's just consider the top of the stack as<00:01:55.259> sort<00:01:55.500> of<00:01:55.619> a<00:01:55.740> return 00:01:56.690 --> 00:01:56.700 align:start position:0% as sort of a return 00:01:56.700 --> 00:01:59.510 align:start position:0% as sort of a return in<00:01:57.420> this<00:01:57.540> case<00:01:57.659> we<00:01:58.079> get<00:01:58.200> a<00:01:58.380> 12<00:01:58.560> we're<00:01:59.280> going<00:01:59.460> to 00:01:59.510 --> 00:01:59.520 align:start position:0% in this case we get a 12 we're going to 00:01:59.520 --> 00:02:01.670 align:start position:0% in this case we get a 12 we're going to push<00:01:59.759> zero 00:02:01.670 --> 00:02:01.680 align:start position:0% push zero 00:02:01.680 --> 00:02:03.649 align:start position:0% push zero um<00:02:01.799> and<00:02:02.220> the<00:02:02.399> stock<00:02:02.520> could<00:02:02.820> call<00:02:03.000> data<00:02:03.360> load 00:02:03.649 --> 00:02:03.659 align:start position:0% um and the stock could call data load 00:02:03.659 --> 00:02:07.370 align:start position:0% um and the stock could call data load that<00:02:04.520> position<00:02:05.520> we<00:02:05.820> get<00:02:06.000> to<00:02:06.180> 12<00:02:06.420> push<00:02:07.140> three 00:02:07.370 --> 00:02:07.380 align:start position:0% that position we get to 12 push three 00:02:07.380 --> 00:02:09.650 align:start position:0% that position we get to 12 push three multiply<00:02:07.979> that's<00:02:08.220> going<00:02:08.399> to<00:02:08.459> give<00:02:08.640> us<00:02:08.819> 36<00:02:09.420> in 00:02:09.650 --> 00:02:09.660 align:start position:0% multiply that's going to give us 36 in 00:02:09.660 --> 00:02:13.970 align:start position:0% multiply that's going to give us 36 in HEX<00:02:10.440> we<00:02:11.160> add<00:02:11.459> one<00:02:11.700> so<00:02:12.120> we<00:02:12.420> get<00:02:12.599> this<00:02:13.560> number<00:02:13.739> top 00:02:13.970 --> 00:02:13.980 align:start position:0% HEX we add one so we get this number top 00:02:13.980 --> 00:02:15.650 align:start position:0% HEX we add one so we get this number top of<00:02:14.099> the<00:02:14.220> stack<00:02:14.459> right<00:02:14.760> so<00:02:15.120> this<00:02:15.300> concrete 00:02:15.650 --> 00:02:15.660 align:start position:0% of the stack right so this concrete 00:02:15.660 --> 00:02:17.210 align:start position:0% of the stack right so this concrete execution<00:02:16.020> you<00:02:16.260> have<00:02:16.379> a<00:02:16.560> program<00:02:16.680> you<00:02:16.920> have<00:02:17.099> a 00:02:17.210 --> 00:02:17.220 align:start position:0% execution you have a program you have a 00:02:17.220 --> 00:02:19.070 align:start position:0% execution you have a program you have a concrete<00:02:17.640> input<00:02:18.180> and<00:02:18.360> then<00:02:18.540> you<00:02:18.660> execute<00:02:18.959> the 00:02:19.070 --> 00:02:19.080 align:start position:0% concrete input and then you execute the 00:02:19.080 --> 00:02:20.930 align:start position:0% concrete input and then you execute the program<00:02:19.200> that<00:02:19.379> input<00:02:19.680> you<00:02:19.800> get<00:02:19.920> an<00:02:20.040> output<00:02:20.280> so 00:02:20.930 --> 00:02:20.940 align:start position:0% program that input you get an output so 00:02:20.940 --> 00:02:23.150 align:start position:0% program that input you get an output so now<00:02:21.360> what<00:02:21.599> is<00:02:21.720> symbolic<00:02:22.080> execution<00:02:22.440> we<00:02:22.860> just 00:02:23.150 --> 00:02:23.160 align:start position:0% now what is symbolic execution we just 00:02:23.160 --> 00:02:26.510 align:start position:0% now what is symbolic execution we just said<00:02:23.760> what's<00:02:24.000> not<00:02:24.319> so<00:02:25.319> t11<00:02:25.860> actually<00:02:26.099> has<00:02:26.340> a 00:02:26.510 --> 00:02:26.520 align:start position:0% said what's not so t11 actually has a 00:02:26.520 --> 00:02:27.770 align:start position:0% said what's not so t11 actually has a pretty<00:02:26.640> good<00:02:26.819> explanation<00:02:27.120> of<00:02:27.239> what<00:02:27.420> it<00:02:27.480> is<00:02:27.599> so 00:02:27.770 --> 00:02:27.780 align:start position:0% pretty good explanation of what it is so 00:02:27.780 --> 00:02:29.210 align:start position:0% pretty good explanation of what it is so it<00:02:27.900> turns<00:02:28.140> the<00:02:28.260> program<00:02:28.379> into<00:02:28.620> math<00:02:28.860> and<00:02:29.099> then 00:02:29.210 --> 00:02:29.220 align:start position:0% it turns the program into math and then 00:02:29.220 --> 00:02:30.890 align:start position:0% it turns the program into math and then solves<00:02:29.580> math<00:02:29.819> formulas 00:02:30.890 --> 00:02:30.900 align:start position:0% solves math formulas 00:02:30.900 --> 00:02:32.990 align:start position:0% solves math formulas that's<00:02:31.440> actually<00:02:31.680> a<00:02:31.980> very<00:02:32.099> precise<00:02:32.580> although 00:02:32.990 --> 00:02:33.000 align:start position:0% that's actually a very precise although 00:02:33.000 --> 00:02:35.930 align:start position:0% that's actually a very precise although very<00:02:33.300> vague<00:02:33.980> description<00:02:34.980> of<00:02:35.280> what<00:02:35.459> it<00:02:35.640> does 00:02:35.930 --> 00:02:35.940 align:start position:0% very vague description of what it does 00:02:35.940 --> 00:02:38.390 align:start position:0% very vague description of what it does we<00:02:36.720> have<00:02:36.900> the<00:02:37.020> same<00:02:37.140> program<00:02:37.379> here<00:02:37.680> but<00:02:38.160> now 00:02:38.390 --> 00:02:38.400 align:start position:0% we have the same program here but now 00:02:38.400 --> 00:02:40.070 align:start position:0% we have the same program here but now instead<00:02:38.940> of<00:02:39.060> a<00:02:39.180> concrete<00:02:39.420> called<00:02:39.660> Data<00:02:39.959> we're 00:02:40.070 --> 00:02:40.080 align:start position:0% instead of a concrete called Data we're 00:02:40.080 --> 00:02:41.330 align:start position:0% instead of a concrete called Data we're going<00:02:40.200> to<00:02:40.319> have<00:02:40.379> a<00:02:40.560> symbolic<00:02:40.980> called<00:02:41.099> Data 00:02:41.330 --> 00:02:41.340 align:start position:0% going to have a symbolic called Data 00:02:41.340 --> 00:02:43.250 align:start position:0% going to have a symbolic called Data what<00:02:41.459> does<00:02:41.580> that<00:02:41.700> mean<00:02:41.879> to<00:02:42.180> be<00:02:42.239> symbolic<00:02:42.780> is 00:02:43.250 --> 00:02:43.260 align:start position:0% what does that mean to be symbolic is 00:02:43.260 --> 00:02:45.050 align:start position:0% what does that mean to be symbolic is that<00:02:43.379> you<00:02:43.620> just<00:02:43.860> use<00:02:44.160> a<00:02:44.340> variable<00:02:44.640> instead<00:02:45.000> of 00:02:45.050 --> 00:02:45.060 align:start position:0% that you just use a variable instead of 00:02:45.060 --> 00:02:47.150 align:start position:0% that you just use a variable instead of concrete<00:02:45.420> number<00:02:45.599> that's<00:02:46.379> really<00:02:46.560> all<00:02:46.800> you<00:02:46.920> do 00:02:47.150 --> 00:02:47.160 align:start position:0% concrete number that's really all you do 00:02:47.160 --> 00:02:49.150 align:start position:0% concrete number that's really all you do you<00:02:47.760> look<00:02:47.879> you<00:02:48.120> keep<00:02:48.239> looking<00:02:48.420> at<00:02:48.599> variables 00:02:49.150 --> 00:02:49.160 align:start position:0% you look you keep looking at variables 00:02:49.160 --> 00:02:51.949 align:start position:0% you look you keep looking at variables so<00:02:50.160> our<00:02:51.000> entire<00:02:51.239> call<00:02:51.360> data<00:02:51.660> is<00:02:51.720> going<00:02:51.840> to<00:02:51.900> be 00:02:51.949 --> 00:02:51.959 align:start position:0% so our entire call data is going to be 00:02:51.959 --> 00:02:54.110 align:start position:0% so our entire call data is going to be CD<00:02:52.319> now<00:02:52.560> it's<00:02:52.800> just<00:02:52.980> a<00:02:53.099> variable<00:02:53.400> the<00:02:53.819> top<00:02:54.000> of 00:02:54.110 --> 00:02:54.120 align:start position:0% CD now it's just a variable the top of 00:02:54.120 --> 00:02:55.009 align:start position:0% CD now it's just a variable the top of our<00:02:54.239> stack<00:02:54.420> is<00:02:54.540> going<00:02:54.660> to<00:02:54.720> be<00:02:54.780> a<00:02:54.840> variable 00:02:55.009 --> 00:02:55.019 align:start position:0% our stack is going to be a variable 00:02:55.019 --> 00:02:57.350 align:start position:0% our stack is going to be a variable called<00:02:55.140> top<00:02:55.379> that's<00:02:56.160> all<00:02:56.340> we're<00:02:56.580> doing<00:02:56.819> so 00:02:57.350 --> 00:02:57.360 align:start position:0% called top that's all we're doing so 00:02:57.360 --> 00:02:59.330 align:start position:0% called top that's all we're doing so here<00:02:57.599> we're<00:02:57.780> going<00:02:57.900> to<00:02:58.080> collect<00:02:58.440> constraints 00:02:59.330 --> 00:02:59.340 align:start position:0% here we're going to collect constraints 00:02:59.340 --> 00:03:01.550 align:start position:0% here we're going to collect constraints which<00:02:59.760> are<00:03:00.000> things<00:03:00.300> that<00:03:00.599> must<00:03:00.780> be<00:03:01.019> true<00:03:01.200> when 00:03:01.550 --> 00:03:01.560 align:start position:0% which are things that must be true when 00:03:01.560 --> 00:03:03.770 align:start position:0% which are things that must be true when we<00:03:01.680> run<00:03:01.800> the<00:03:02.040> program<00:03:02.220> so 00:03:03.770 --> 00:03:03.780 align:start position:0% we run the program so 00:03:03.780 --> 00:03:07.070 align:start position:0% we run the program so when<00:03:04.680> we<00:03:04.980> run<00:03:05.280> call<00:03:05.519> data<00:03:05.819> load<00:03:06.120> of<00:03:06.360> zero<00:03:06.840> we're 00:03:07.070 --> 00:03:07.080 align:start position:0% when we run call data load of zero we're 00:03:07.080 --> 00:03:10.190 align:start position:0% when we run call data load of zero we're basically<00:03:07.440> doing<00:03:07.680> CD<00:03:08.280> of<00:03:08.580> zero<00:03:09.060> right<00:03:09.360> and 00:03:10.190 --> 00:03:10.200 align:start position:0% basically doing CD of zero right and 00:03:10.200 --> 00:03:12.110 align:start position:0% basically doing CD of zero right and then<00:03:10.319> we<00:03:10.440> can<00:03:10.560> also<00:03:10.739> call<00:03:10.860> it<00:03:10.980> X<00:03:11.280> we<00:03:11.819> can<00:03:11.879> call 00:03:12.110 --> 00:03:12.120 align:start position:0% then we can also call it X we can call 00:03:12.120 --> 00:03:13.610 align:start position:0% then we can also call it X we can call it<00:03:12.239> side<00:03:12.659> we<00:03:12.840> can<00:03:12.959> call<00:03:13.019> it<00:03:13.140> whatever<00:03:13.319> it's 00:03:13.610 --> 00:03:13.620 align:start position:0% it side we can call it whatever it's 00:03:13.620 --> 00:03:15.589 align:start position:0% it side we can call it whatever it's just<00:03:13.860> a<00:03:14.040> symbol 00:03:15.589 --> 00:03:15.599 align:start position:0% just a symbol 00:03:15.599 --> 00:03:17.750 align:start position:0% just a symbol um<00:03:15.720> and<00:03:16.319> it<00:03:16.860> happens<00:03:16.980> that<00:03:17.220> that<00:03:17.400> thing<00:03:17.519> must 00:03:17.750 --> 00:03:17.760 align:start position:0% um and it happens that that thing must 00:03:17.760 --> 00:03:19.729 align:start position:0% um and it happens that that thing must be<00:03:17.879> greater<00:03:18.120> equals<00:03:18.480> zero<00:03:18.720> because<00:03:19.080> we're 00:03:19.729 --> 00:03:19.739 align:start position:0% be greater equals zero because we're 00:03:19.739 --> 00:03:21.410 align:start position:0% be greater equals zero because we're trading<00:03:20.040> we're<00:03:20.220> dealing<00:03:20.580> dealing<00:03:20.879> with<00:03:20.940> evm 00:03:21.410 --> 00:03:21.420 align:start position:0% trading we're dealing dealing with evm 00:03:21.420 --> 00:03:24.170 align:start position:0% trading we're dealing dealing with evm words<00:03:21.599> and<00:03:22.140> they're<00:03:22.440> unsigned<00:03:22.980> right<00:03:23.220> the 00:03:24.170 --> 00:03:24.180 align:start position:0% words and they're unsigned right the 00:03:24.180 --> 00:03:25.610 align:start position:0% words and they're unsigned right the second<00:03:24.300> part<00:03:24.599> is<00:03:24.900> that<00:03:25.080> we<00:03:25.200> are<00:03:25.319> assigning 00:03:25.610 --> 00:03:25.620 align:start position:0% second part is that we are assigning 00:03:25.620 --> 00:03:27.770 align:start position:0% second part is that we are assigning that<00:03:25.739> to<00:03:25.860> X<00:03:26.040> we<00:03:26.580> just<00:03:26.760> make<00:03:26.940> a<00:03:27.120> variable<00:03:27.360> out<00:03:27.599> of 00:03:27.770 --> 00:03:27.780 align:start position:0% that to X we just make a variable out of 00:03:27.780 --> 00:03:29.809 align:start position:0% that to X we just make a variable out of out<00:03:28.080> of<00:03:28.260> that<00:03:28.440> when<00:03:28.800> we<00:03:28.920> do<00:03:29.099> the<00:03:29.280> call<00:03:29.400> data 00:03:29.809 --> 00:03:29.819 align:start position:0% out of that when we do the call data 00:03:29.819 --> 00:03:32.149 align:start position:0% out of that when we do the call data load<00:03:30.019> next<00:03:31.019> thing<00:03:31.440> we<00:03:31.920> have<00:03:32.040> this 00:03:32.149 --> 00:03:32.159 align:start position:0% load next thing we have this 00:03:32.159 --> 00:03:33.530 align:start position:0% load next thing we have this multiplication<00:03:32.700> we<00:03:33.120> can<00:03:33.239> make<00:03:33.360> another 00:03:33.530 --> 00:03:33.540 align:start position:0% multiplication we can make another 00:03:33.540 --> 00:03:36.649 align:start position:0% multiplication we can make another variable<00:03:33.900> for<00:03:34.019> it<00:03:34.200> called<00:03:34.319> Y<00:03:34.620> which<00:03:35.459> is<00:03:35.760> now<00:03:36.120> x 00:03:36.649 --> 00:03:36.659 align:start position:0% variable for it called Y which is now x 00:03:36.659 --> 00:03:40.309 align:start position:0% variable for it called Y which is now x times<00:03:37.019> three<00:03:37.580> finally<00:03:38.580> for<00:03:38.940> this<00:03:39.180> ad<00:03:39.480> we<00:03:40.200> can 00:03:40.309 --> 00:03:40.319 align:start position:0% times three finally for this ad we can 00:03:40.319 --> 00:03:41.649 align:start position:0% times three finally for this ad we can make<00:03:40.440> another<00:03:40.560> variable<00:03:40.920> for<00:03:41.099> it<00:03:41.220> called<00:03:41.400> top 00:03:41.649 --> 00:03:41.659 align:start position:0% make another variable for it called top 00:03:41.659 --> 00:03:44.089 align:start position:0% make another variable for it called top and<00:03:42.659> then<00:03:42.840> which<00:03:43.200> we<00:03:43.440> just<00:03:43.680> did<00:03:43.799> the<00:03:43.980> previous 00:03:44.089 --> 00:03:44.099 align:start position:0% and then which we just did the previous 00:03:44.099 --> 00:03:47.809 align:start position:0% and then which we just did the previous top<00:03:44.519> of<00:03:44.700> the<00:03:44.819> stack<00:03:45.000> which<00:03:45.180> is<00:03:45.360> y<00:03:45.599> plus<00:03:46.200> one 00:03:47.809 --> 00:03:47.819 align:start position:0% top of the stack which is y plus one 00:03:47.819 --> 00:03:49.250 align:start position:0% top of the stack which is y plus one um so<00:03:48.000> you<00:03:48.180> see<00:03:48.239> that<00:03:48.420> for<00:03:48.599> every<00:03:48.780> operation 00:03:49.250 --> 00:03:49.260 align:start position:0% um so you see that for every operation 00:03:49.260 --> 00:03:51.410 align:start position:0% um so you see that for every operation we<00:03:49.980> add<00:03:50.159> a<00:03:50.340> new<00:03:50.459> variable<00:03:50.819> we<00:03:51.060> add<00:03:51.180> a<00:03:51.299> new 00:03:51.410 --> 00:03:51.420 align:start position:0% we add a new variable we add a new 00:03:51.420 --> 00:03:53.270 align:start position:0% we add a new variable we add a new symbol<00:03:51.720> that<00:03:51.900> represents<00:03:52.440> that<00:03:52.799> expression 00:03:53.270 --> 00:03:53.280 align:start position:0% symbol that represents that expression 00:03:53.280 --> 00:03:56.089 align:start position:0% symbol that represents that expression and<00:03:53.940> we<00:03:54.060> collect<00:03:54.420> all<00:03:54.599> these<00:03:54.900> Expressions<00:03:55.379> so 00:03:56.089 --> 00:03:56.099 align:start position:0% and we collect all these Expressions so 00:03:56.099 --> 00:03:57.470 align:start position:0% and we collect all these Expressions so we<00:03:56.220> end<00:03:56.400> up<00:03:56.519> with<00:03:56.760> what<00:03:57.000> we<00:03:57.120> call<00:03:57.239> these 00:03:57.470 --> 00:03:57.480 align:start position:0% we end up with what we call these 00:03:57.480 --> 00:03:59.990 align:start position:0% we end up with what we call these constraints<00:03:57.900> and<00:03:58.739> this<00:03:58.980> is<00:03:59.220> what<00:03:59.459> is<00:03:59.819> our 00:03:59.990 --> 00:04:00.000 align:start position:0% constraints and this is what is our 00:04:00.000 --> 00:04:02.089 align:start position:0% constraints and this is what is our symbolic<00:04:00.480> encoding<00:04:01.019> so<00:04:01.440> we<00:04:01.560> take<00:04:01.739> the<00:04:01.920> program 00:04:02.089 --> 00:04:02.099 align:start position:0% symbolic encoding so we take the program 00:04:02.099 --> 00:04:05.270 align:start position:0% symbolic encoding so we take the program in<00:04:02.580> evm<00:04:03.120> bytecode<00:04:03.720> and<00:04:03.900> assembly<00:04:04.260> here<00:04:04.440> we 00:04:05.270 --> 00:04:05.280 align:start position:0% in evm bytecode and assembly here we 00:04:05.280 --> 00:04:07.130 align:start position:0% in evm bytecode and assembly here we transform<00:04:05.640> it<00:04:05.819> into<00:04:06.000> a<00:04:06.239> set<00:04:06.360> of<00:04:06.540> constraints 00:04:07.130 --> 00:04:07.140 align:start position:0% transform it into a set of constraints 00:04:07.140 --> 00:04:09.470 align:start position:0% transform it into a set of constraints and<00:04:07.560> that's<00:04:07.739> our<00:04:08.040> symbolic<00:04:08.519> encoding<00:04:09.000> they're 00:04:09.470 --> 00:04:09.480 align:start position:0% and that's our symbolic encoding they're 00:04:09.480 --> 00:04:10.550 align:start position:0% and that's our symbolic encoding they're different<00:04:09.720> there<00:04:09.959> are<00:04:10.140> many<00:04:10.200> many<00:04:10.319> different 00:04:10.550 --> 00:04:10.560 align:start position:0% different there are many many different 00:04:10.560 --> 00:04:12.229 align:start position:0% different there are many many different ways<00:04:10.920> to<00:04:11.099> write<00:04:11.280> these<00:04:11.580> constraints<00:04:11.879> from<00:04:12.120> a 00:04:12.229 --> 00:04:12.239 align:start position:0% ways to write these constraints from a 00:04:12.239 --> 00:04:13.509 align:start position:0% ways to write these constraints from a program 00:04:13.509 --> 00:04:13.519 align:start position:0% program 00:04:13.519 --> 00:04:15.849 align:start position:0% program which<00:04:14.519> means<00:04:14.760> we<00:04:14.879> have<00:04:15.000> different<00:04:15.180> ways<00:04:15.599> to 00:04:15.849 --> 00:04:15.859 align:start position:0% which means we have different ways to 00:04:15.859 --> 00:04:18.890 align:start position:0% which means we have different ways to symbolically<00:04:16.859> encode<00:04:17.280> your<00:04:17.519> program 00:04:18.890 --> 00:04:18.900 align:start position:0% symbolically encode your program 00:04:18.900 --> 00:04:21.469 align:start position:0% symbolically encode your program why<00:04:19.560> do<00:04:19.680> we<00:04:19.799> want<00:04:19.859> to<00:04:20.040> do<00:04:20.160> this<00:04:20.340> so<00:04:21.239> we 00:04:21.469 --> 00:04:21.479 align:start position:0% why do we want to do this so we 00:04:21.479 --> 00:04:22.790 align:start position:0% why do we want to do this so we obviously<00:04:21.900> walking<00:04:22.079> code<00:04:22.320> is<00:04:22.440> going<00:04:22.620> to<00:04:22.680> turn 00:04:22.790 --> 00:04:22.800 align:start position:0% obviously walking code is going to turn 00:04:22.800 --> 00:04:25.010 align:start position:0% obviously walking code is going to turn into<00:04:22.979> a<00:04:23.160> system<00:04:23.280> of<00:04:23.520> linear<00:04:23.820> inequalities<00:04:24.360> so 00:04:25.010 --> 00:04:25.020 align:start position:0% into a system of linear inequalities so 00:04:25.020 --> 00:04:27.650 align:start position:0% into a system of linear inequalities so this<00:04:25.440> was<00:04:25.860> our<00:04:26.220> set<00:04:26.580> of<00:04:26.699> constraints 00:04:27.650 --> 00:04:27.660 align:start position:0% this was our set of constraints 00:04:27.660 --> 00:04:29.510 align:start position:0% this was our set of constraints that's<00:04:28.080> going<00:04:28.259> to<00:04:28.380> turn<00:04:28.500> into<00:04:28.800> the<00:04:29.100> system<00:04:29.280> of 00:04:29.510 --> 00:04:29.520 align:start position:0% that's going to turn into the system of 00:04:29.520 --> 00:04:31.430 align:start position:0% that's going to turn into the system of linear<00:04:29.759> inequalities<00:04:30.240> there<00:04:30.840> are<00:04:31.020> equalities 00:04:31.430 --> 00:04:31.440 align:start position:0% linear inequalities there are equalities 00:04:31.440 --> 00:04:34.189 align:start position:0% linear inequalities there are equalities here<00:04:31.800> but<00:04:32.520> they<00:04:32.759> can<00:04:32.940> be<00:04:33.360> very<00:04:33.840> quickly 00:04:34.189 --> 00:04:34.199 align:start position:0% here but they can be very quickly 00:04:34.199 --> 00:04:36.050 align:start position:0% here but they can be very quickly translated<00:04:34.620> into<00:04:34.800> inequalities 00:04:36.050 --> 00:04:36.060 align:start position:0% translated into inequalities 00:04:36.060 --> 00:04:37.670 align:start position:0% translated into inequalities um<00:04:36.120> so<00:04:36.600> we<00:04:36.720> just<00:04:36.900> keep<00:04:37.020> them<00:04:37.199> as<00:04:37.320> they<00:04:37.440> call<00:04:37.560> it 00:04:37.670 --> 00:04:37.680 align:start position:0% um so we just keep them as they call it 00:04:37.680 --> 00:04:38.870 align:start position:0% um so we just keep them as they call it for<00:04:37.860> Simplicity 00:04:38.870 --> 00:04:38.880 align:start position:0% for Simplicity 00:04:38.880 --> 00:04:42.469 align:start position:0% for Simplicity and<00:04:39.660> why<00:04:40.500> do<00:04:40.680> we<00:04:40.800> do<00:04:40.979> this<00:04:41.220> the<00:04:42.000> reason<00:04:42.120> why<00:04:42.300> we 00:04:42.469 --> 00:04:42.479 align:start position:0% and why do we do this the reason why we 00:04:42.479 --> 00:04:43.909 align:start position:0% and why do we do this the reason why we do<00:04:42.660> this<00:04:42.780> because<00:04:42.960> we<00:04:43.199> know<00:04:43.320> how<00:04:43.500> to<00:04:43.620> solve 00:04:43.909 --> 00:04:43.919 align:start position:0% do this because we know how to solve 00:04:43.919 --> 00:04:45.890 align:start position:0% do this because we know how to solve these<00:04:44.160> things<00:04:44.280> with<00:04:45.120> algorithms<00:04:45.660> that<00:04:45.780> you 00:04:45.890 --> 00:04:45.900 align:start position:0% these things with algorithms that you 00:04:45.900 --> 00:04:47.570 align:start position:0% these things with algorithms that you might<00:04:46.020> have<00:04:46.199> seen<00:04:46.440> in<00:04:47.040> high<00:04:47.220> school<00:04:47.340> or 00:04:47.570 --> 00:04:47.580 align:start position:0% might have seen in high school or 00:04:47.580 --> 00:04:50.270 align:start position:0% might have seen in high school or University<00:04:47.759> or<00:04:48.600> you<00:04:49.199> still<00:04:49.380> will<00:04:49.620> see<00:04:49.860> it<00:04:50.040> when 00:04:50.270 --> 00:04:50.280 align:start position:0% University or you still will see it when 00:04:50.280 --> 00:04:52.249 align:start position:0% University or you still will see it when you<00:04:50.400> finish<00:04:50.639> high<00:04:50.940> school<00:04:51.120> and<00:04:51.780> what<00:04:52.020> can<00:04:52.139> we 00:04:52.249 --> 00:04:52.259 align:start position:0% you finish high school and what can we 00:04:52.259 --> 00:04:54.890 align:start position:0% you finish high school and what can we do<00:04:52.440> with<00:04:52.560> it<00:04:52.740> we<00:04:53.580> can<00:04:53.820> for<00:04:54.300> example<00:04:54.479> did<00:04:54.720> the 00:04:54.890 --> 00:04:54.900 align:start position:0% do with it we can for example did the 00:04:54.900 --> 00:04:56.330 align:start position:0% do with it we can for example did the same<00:04:55.020> thing<00:04:55.080> we<00:04:55.199> did<00:04:55.320> before<00:04:55.500> we<00:04:55.800> can<00:04:55.979> give<00:04:56.100> a 00:04:56.330 --> 00:04:56.340 align:start position:0% same thing we did before we can give a 00:04:56.340 --> 00:04:58.370 align:start position:0% same thing we did before we can give a concrete<00:04:56.639> call<00:04:56.759> data<00:04:57.180> in<00:04:57.840> this<00:04:57.960> case<00:04:58.080> the<00:04:58.259> same 00:04:58.370 --> 00:04:58.380 align:start position:0% concrete call data in this case the same 00:04:58.380 --> 00:05:02.150 align:start position:0% concrete call data in this case the same called<00:04:58.560> Data<00:04:58.919> as<00:04:58.979> we<00:04:59.100> we<00:04:59.340> had<00:04:59.580> before<00:04:59.840> and<00:05:01.160> run 00:05:02.150 --> 00:05:02.160 align:start position:0% called Data as we we had before and run 00:05:02.160 --> 00:05:03.950 align:start position:0% called Data as we we had before and run it<00:05:02.460> symbolically<00:05:03.060> what<00:05:03.540> does<00:05:03.660> that<00:05:03.780> mean 00:05:03.950 --> 00:05:03.960 align:start position:0% it symbolically what does that mean 00:05:03.960 --> 00:05:05.810 align:start position:0% it symbolically what does that mean we're<00:05:04.199> gonna<00:05:04.380> in<00:05:05.160> this<00:05:05.280> case<00:05:05.400> a<00:05:05.699> simple 00:05:05.810 --> 00:05:05.820 align:start position:0% we're gonna in this case a simple 00:05:05.820 --> 00:05:07.689 align:start position:0% we're gonna in this case a simple substitution<00:05:06.300> does<00:05:06.540> it<00:05:06.720> we<00:05:06.960> can<00:05:07.080> substitute 00:05:07.689 --> 00:05:07.699 align:start position:0% substitution does it we can substitute 00:05:07.699 --> 00:05:10.010 align:start position:0% substitution does it we can substitute CD<00:05:08.699> by 00:05:10.010 --> 00:05:10.020 align:start position:0% CD by 00:05:10.020 --> 00:05:12.409 align:start position:0% CD by visitorical<00:05:10.860> data<00:05:11.340> which<00:05:11.820> then<00:05:12.060> substitute 00:05:12.409 --> 00:05:12.419 align:start position:0% visitorical data which then substitute 00:05:12.419 --> 00:05:15.890 align:start position:0% visitorical data which then substitute CD<00:05:12.720> of<00:05:12.960> 0<00:05:13.139> by<00:05:13.380> 12<00:05:13.560> and<00:05:13.860> so<00:05:14.040> on<00:05:14.220> and<00:05:14.759> we<00:05:15.120> get 00:05:15.890 --> 00:05:15.900 align:start position:0% CD of 0 by 12 and so on and we get 00:05:15.900 --> 00:05:17.450 align:start position:0% CD of 0 by 12 and so on and we get at<00:05:16.320> the<00:05:16.440> top<00:05:16.560> is<00:05:16.800> going<00:05:16.919> to<00:05:17.040> be<00:05:17.040> this<00:05:17.280> number 00:05:17.450 --> 00:05:17.460 align:start position:0% at the top is going to be this number 00:05:17.460 --> 00:05:20.090 align:start position:0% at the top is going to be this number when<00:05:18.360> we<00:05:18.540> solve<00:05:18.840> that<00:05:18.960> with<00:05:19.440> gal<00:05:19.860> Jordan 00:05:20.090 --> 00:05:20.100 align:start position:0% when we solve that with gal Jordan 00:05:20.100 --> 00:05:21.710 align:start position:0% when we solve that with gal Jordan illumination<00:05:20.699> or<00:05:20.820> Gauss<00:05:21.120> elimination<00:05:21.479> or 00:05:21.710 --> 00:05:21.720 align:start position:0% illumination or Gauss elimination or 00:05:21.720 --> 00:05:23.330 align:start position:0% illumination or Gauss elimination or there's<00:05:21.960> tons<00:05:22.259> of<00:05:22.380> ways<00:05:22.680> of<00:05:22.800> solving<00:05:23.100> it<00:05:23.220> a 00:05:23.330 --> 00:05:23.340 align:start position:0% there's tons of ways of solving it a 00:05:23.340 --> 00:05:25.550 align:start position:0% there's tons of ways of solving it a simple<00:05:23.460> substitution<00:05:23.880> here<00:05:24.060> will<00:05:24.300> do<00:05:24.960> it<00:05:25.440> not 00:05:25.550 --> 00:05:25.560 align:start position:0% simple substitution here will do it not 00:05:25.560 --> 00:05:27.230 align:start position:0% simple substitution here will do it not only<00:05:25.740> gives<00:05:25.979> us<00:05:26.160> the<00:05:26.280> value<00:05:26.400> for<00:05:26.639> top<00:05:26.820> it<00:05:27.060> gives 00:05:27.230 --> 00:05:27.240 align:start position:0% only gives us the value for top it gives 00:05:27.240 --> 00:05:30.350 align:start position:0% only gives us the value for top it gives us<00:05:27.360> values<00:05:28.080> for<00:05:28.320> every<00:05:28.680> single<00:05:29.039> variable<00:05:29.520> in 00:05:30.350 --> 00:05:30.360 align:start position:0% us values for every single variable in 00:05:30.360 --> 00:05:31.850 align:start position:0% us values for every single variable in this<00:05:30.479> system<00:05:30.720> we<00:05:31.259> could<00:05:31.440> have<00:05:31.560> read<00:05:31.680> it<00:05:31.800> that 00:05:31.850 --> 00:05:31.860 align:start position:0% this system we could have read it that 00:05:31.860 --> 00:05:33.290 align:start position:0% this system we could have read it that it<00:05:32.039> before<00:05:32.100> with<00:05:32.340> the<00:05:32.460> concrete<00:05:32.699> execution<00:05:33.120> so 00:05:33.290 --> 00:05:33.300 align:start position:0% it before with the concrete execution so 00:05:33.300 --> 00:05:34.790 align:start position:0% it before with the concrete execution so the<00:05:33.479> cool<00:05:33.660> things<00:05:33.780> we<00:05:33.960> can<00:05:34.080> do<00:05:34.199> with<00:05:34.259> this<00:05:34.440> we 00:05:34.790 --> 00:05:34.800 align:start position:0% the cool things we can do with this we 00:05:34.800 --> 00:05:37.790 align:start position:0% the cool things we can do with this we can<00:05:34.979> ask<00:05:35.639> many<00:05:36.300> many<00:05:36.479> things<00:05:36.840> so<00:05:37.440> you<00:05:37.560> can<00:05:37.680> ask 00:05:37.790 --> 00:05:37.800 align:start position:0% can ask many many things so you can ask 00:05:37.800 --> 00:05:40.310 align:start position:0% can ask many many things so you can ask for<00:05:37.979> example<00:05:38.280> can<00:05:39.000> top<00:05:39.240> be<00:05:39.479> greater<00:05:39.780> than<00:05:39.840> 10 00:05:40.310 --> 00:05:40.320 align:start position:0% for example can top be greater than 10 00:05:40.320 --> 00:05:42.650 align:start position:0% for example can top be greater than 10 000.<00:05:40.560> how<00:05:40.979> do<00:05:41.100> we<00:05:41.220> ask<00:05:41.340> that<00:05:41.520> we<00:05:41.759> simply<00:05:42.060> add<00:05:42.419> a 00:05:42.650 --> 00:05:42.660 align:start position:0% 000. how do we ask that we simply add a 00:05:42.660 --> 00:05:45.050 align:start position:0% 000. how do we ask that we simply add a constraint<00:05:43.020> that<00:05:43.860> represents<00:05:44.580> that 00:05:45.050 --> 00:05:45.060 align:start position:0% constraint that represents that 00:05:45.060 --> 00:05:49.430 align:start position:0% constraint that represents that statement<00:05:45.600> in<00:05:46.560> this<00:05:46.740> language<00:05:47.300> so<00:05:48.300> can<00:05:48.960> top<00:05:49.199> be 00:05:49.430 --> 00:05:49.440 align:start position:0% statement in this language so can top be 00:05:49.440 --> 00:05:50.990 align:start position:0% statement in this language so can top be greater<00:05:49.680> than<00:05:49.740> 10<00:05:50.100> 000<00:05:50.160> basically<00:05:50.639> gives<00:05:50.880> us 00:05:50.990 --> 00:05:51.000 align:start position:0% greater than 10 000 basically gives us 00:05:51.000 --> 00:05:54.110 align:start position:0% greater than 10 000 basically gives us this<00:05:51.300> constraint<00:05:51.720> here<00:05:52.100> and<00:05:53.100> then<00:05:53.280> but<00:05:53.820> here's 00:05:54.110 --> 00:05:54.120 align:start position:0% this constraint here and then but here's 00:05:54.120 --> 00:05:56.930 align:start position:0% this constraint here and then but here's the<00:05:54.240> answer<00:05:54.500> it<00:05:55.500> is<00:05:55.620> possible<00:05:55.979> in<00:05:56.580> which<00:05:56.699> case 00:05:56.930 --> 00:05:56.940 align:start position:0% the answer it is possible in which case 00:05:56.940 --> 00:05:59.810 align:start position:0% the answer it is possible in which case such<00:05:57.360> a<00:05:57.539> solver<00:05:57.840> such<00:05:58.080> a<00:05:58.320> math<00:05:58.500> solver<00:05:59.039> will 00:05:59.810 --> 00:05:59.820 align:start position:0% such a solver such a math solver will 00:05:59.820 --> 00:06:01.850 align:start position:0% such a solver such a math solver will tell<00:06:00.120> us<00:06:00.300> that<00:06:00.600> the<00:06:00.780> system<00:06:00.960> is<00:06:01.259> satisfiable 00:06:01.850 --> 00:06:01.860 align:start position:0% tell us that the system is satisfiable 00:06:01.860 --> 00:06:04.550 align:start position:0% tell us that the system is satisfiable meaning<00:06:02.639> that<00:06:03.000> there<00:06:03.240> is<00:06:03.419> evaluation<00:06:04.139> for 00:06:04.550 --> 00:06:04.560 align:start position:0% meaning that there is evaluation for 00:06:04.560 --> 00:06:06.710 align:start position:0% meaning that there is evaluation for every<00:06:04.860> single<00:06:05.160> variable<00:06:05.460> in<00:06:05.639> the<00:06:05.820> system<00:06:06.000> that 00:06:06.710 --> 00:06:06.720 align:start position:0% every single variable in the system that 00:06:06.720 --> 00:06:08.990 align:start position:0% every single variable in the system that makes<00:06:07.020> this<00:06:07.560> the<00:06:07.860> the<00:06:07.919> the<00:06:08.160> set<00:06:08.820> of 00:06:08.990 --> 00:06:09.000 align:start position:0% makes this the the the set of 00:06:09.000 --> 00:06:10.969 align:start position:0% makes this the the the set of constraints<00:06:09.419> satisfiable<00:06:09.960> it<00:06:10.380> is<00:06:10.560> possible 00:06:10.969 --> 00:06:10.979 align:start position:0% constraints satisfiable it is possible 00:06:10.979 --> 00:06:13.189 align:start position:0% constraints satisfiable it is possible that<00:06:11.759> all<00:06:11.940> the<00:06:12.060> constraints<00:06:12.419> are<00:06:12.660> true<00:06:12.840> at<00:06:13.080> the 00:06:13.189 --> 00:06:13.199 align:start position:0% that all the constraints are true at the 00:06:13.199 --> 00:06:15.409 align:start position:0% that all the constraints are true at the same<00:06:13.380> time<00:06:13.560> and<00:06:14.340> it<00:06:14.460> also<00:06:14.699> gives<00:06:14.880> us<00:06:15.060> what<00:06:15.240> we 00:06:15.409 --> 00:06:15.419 align:start position:0% same time and it also gives us what we 00:06:15.419 --> 00:06:18.110 align:start position:0% same time and it also gives us what we call<00:06:15.539> a<00:06:15.780> model<00:06:15.960> which<00:06:16.440> is<00:06:16.680> the<00:06:17.460> actual<00:06:17.699> values 00:06:18.110 --> 00:06:18.120 align:start position:0% call a model which is the actual values 00:06:18.120 --> 00:06:20.689 align:start position:0% call a model which is the actual values that<00:06:18.360> make<00:06:18.479> the<00:06:18.660> whole<00:06:18.780> the<00:06:19.199> whole<00:06:19.320> set<00:06:19.699> of 00:06:20.689 --> 00:06:20.699 align:start position:0% that make the whole the whole set of 00:06:20.699 --> 00:06:23.510 align:start position:0% that make the whole the whole set of constraints<00:06:21.180> valid<00:06:21.680> and<00:06:22.680> similarity<00:06:23.280> before 00:06:23.510 --> 00:06:23.520 align:start position:0% constraints valid and similarity before 00:06:23.520 --> 00:06:25.850 align:start position:0% constraints valid and similarity before we<00:06:23.699> have<00:06:23.819> a<00:06:23.940> value<00:06:24.060> for<00:06:24.300> top<00:06:24.479> and<00:06:24.840> and<00:06:25.380> we<00:06:25.620> also 00:06:25.850 --> 00:06:25.860 align:start position:0% we have a value for top and and we also 00:06:25.860 --> 00:06:27.230 align:start position:0% we have a value for top and and we also have<00:06:25.979> values<00:06:26.340> for<00:06:26.520> every<00:06:26.699> single<00:06:27.000> variable 00:06:27.230 --> 00:06:27.240 align:start position:0% have values for every single variable 00:06:27.240 --> 00:06:30.469 align:start position:0% have values for every single variable that<00:06:27.479> appears<00:06:27.900> in<00:06:28.319> the<00:06:28.440> in<00:06:28.620> the<00:06:28.800> system 00:06:30.469 --> 00:06:30.479 align:start position:0% that appears in the in the system 00:06:30.479 --> 00:06:33.650 align:start position:0% that appears in the in the system we<00:06:30.960> can<00:06:31.080> also<00:06:31.259> ask<00:06:31.380> n<00:06:31.680> top<00:06:31.860> be<00:06:32.039> zero 00:06:33.650 --> 00:06:33.660 align:start position:0% we can also ask n top be zero 00:06:33.660 --> 00:06:35.570 align:start position:0% we can also ask n top be zero what<00:06:34.139> do<00:06:34.259> you<00:06:34.319> think<00:06:34.500> so<00:06:34.860> we<00:06:34.979> can<00:06:35.160> represent<00:06:35.400> it 00:06:35.570 --> 00:06:35.580 align:start position:0% what do you think so we can represent it 00:06:35.580 --> 00:06:37.610 align:start position:0% what do you think so we can represent it for<00:06:35.699> this<00:06:36.000> constraints<00:06:36.479> pretty<00:06:36.720> simple<00:06:36.960> by 00:06:37.610 --> 00:06:37.620 align:start position:0% for this constraints pretty simple by 00:06:37.620 --> 00:06:39.469 align:start position:0% for this constraints pretty simple by the<00:06:37.740> way<00:06:37.800> where<00:06:38.220> all<00:06:38.580> these<00:06:38.759> variables<00:06:39.060> are<00:06:39.240> on 00:06:39.469 --> 00:06:39.479 align:start position:0% the way where all these variables are on 00:06:39.479 --> 00:06:41.090 align:start position:0% the way where all these variables are on the<00:06:39.600> integers<00:06:40.020> there's<00:06:40.500> no<00:06:40.680> reals<00:06:40.979> or 00:06:41.090 --> 00:06:41.100 align:start position:0% the integers there's no reals or 00:06:41.100 --> 00:06:43.490 align:start position:0% the integers there's no reals or rationals<00:06:41.460> here<00:06:41.580> everything's<00:06:42.120> integers 00:06:43.490 --> 00:06:43.500 align:start position:0% rationals here everything's integers 00:06:43.500 --> 00:06:44.990 align:start position:0% rationals here everything's integers um in<00:06:43.740> this<00:06:43.800> case<00:06:43.919> this<00:06:44.160> oversized<00:06:44.759> the 00:06:44.990 --> 00:06:45.000 align:start position:0% um in this case this oversized the 00:06:45.000 --> 00:06:46.129 align:start position:0% um in this case this oversized the system<00:06:45.120> is<00:06:45.360> unsatisfiable<00:06:46.020> it's 00:06:46.129 --> 00:06:46.139 align:start position:0% system is unsatisfiable it's 00:06:46.139 --> 00:06:48.950 align:start position:0% system is unsatisfiable it's inconsistent<00:06:46.680> there's<00:06:46.979> there's<00:06:47.639> no<00:06:48.060> way<00:06:48.300> all 00:06:48.950 --> 00:06:48.960 align:start position:0% inconsistent there's there's no way all 00:06:48.960 --> 00:06:50.450 align:start position:0% inconsistent there's there's no way all these<00:06:49.199> constraints<00:06:49.500> can<00:06:49.680> be<00:06:49.800> true<00:06:49.979> at<00:06:50.340> the 00:06:50.450 --> 00:06:50.460 align:start position:0% these constraints can be true at the 00:06:50.460 --> 00:06:52.370 align:start position:0% these constraints can be true at the same<00:06:50.639> time<00:06:50.880> they<00:06:51.419> may<00:06:51.539> be<00:06:51.660> true<00:06:51.840> in<00:06:52.020> separation 00:06:52.370 --> 00:06:52.380 align:start position:0% same time they may be true in separation 00:06:52.380 --> 00:06:54.529 align:start position:0% same time they may be true in separation but<00:06:52.680> they<00:06:52.800> will<00:06:52.979> never<00:06:53.160> be<00:06:53.400> true 00:06:54.529 --> 00:06:54.539 align:start position:0% but they will never be true 00:06:54.539 --> 00:06:56.450 align:start position:0% but they will never be true um at<00:06:55.080> the<00:06:55.199> same<00:06:55.319> time<00:06:55.500> what<00:06:55.979> we<00:06:56.160> want<00:06:56.280> to<00:06:56.400> do 00:06:56.450 --> 00:06:56.460 align:start position:0% um at the same time what we want to do 00:06:56.460 --> 00:06:58.070 align:start position:0% um at the same time what we want to do is<00:06:56.699> basically 00:06:58.070 --> 00:06:58.080 align:start position:0% is basically 00:06:58.080 --> 00:07:01.010 align:start position:0% is basically do<00:06:58.680> exactly<00:06:59.039> that<00:06:59.220> in<00:06:59.460> solidity<00:06:59.880> so<00:07:00.660> but<00:07:00.840> what 00:07:01.010 --> 00:07:01.020 align:start position:0% do exactly that in solidity so but what 00:07:01.020 --> 00:07:02.450 align:start position:0% do exactly that in solidity so but what exactly<00:07:01.319> do<00:07:01.440> we<00:07:01.560> want<00:07:01.680> to<00:07:01.800> do 00:07:02.450 --> 00:07:02.460 align:start position:0% exactly do we want to do 00:07:02.460 --> 00:07:05.029 align:start position:0% exactly do we want to do you<00:07:02.880> can<00:07:03.000> do<00:07:03.120> several<00:07:03.479> things<00:07:03.600> you<00:07:04.020> can 00:07:05.029 --> 00:07:05.039 align:start position:0% you can do several things you can 00:07:05.039 --> 00:07:07.070 align:start position:0% you can do several things you can try<00:07:05.460> to<00:07:05.580> prove<00:07:05.819> that<00:07:05.940> a<00:07:06.180> certain<00:07:06.360> assertion<00:07:06.900> is 00:07:07.070 --> 00:07:07.080 align:start position:0% try to prove that a certain assertion is 00:07:07.080 --> 00:07:09.290 align:start position:0% try to prove that a certain assertion is true<00:07:07.259> you<00:07:07.500> can<00:07:07.620> prove<00:07:07.979> that<00:07:08.100> a<00:07:08.340> certain<00:07:08.520> thing 00:07:09.290 --> 00:07:09.300 align:start position:0% true you can prove that a certain thing 00:07:09.300 --> 00:07:11.090 align:start position:0% true you can prove that a certain thing always<00:07:09.660> happens<00:07:09.840> or<00:07:10.139> never<00:07:10.319> happens<00:07:10.500> kind<00:07:10.979> of 00:07:11.090 --> 00:07:11.100 align:start position:0% always happens or never happens kind of 00:07:11.100 --> 00:07:12.110 align:start position:0% always happens or never happens kind of things 00:07:12.110 --> 00:07:12.120 align:start position:0% things 00:07:12.120 --> 00:07:13.790 align:start position:0% things for<00:07:12.539> our<00:07:12.720> use<00:07:12.960> case<00:07:13.139> we're<00:07:13.319> going<00:07:13.440> to<00:07:13.560> try<00:07:13.680> to 00:07:13.790 --> 00:07:13.800 align:start position:0% for our use case we're going to try to 00:07:13.800 --> 00:07:16.010 align:start position:0% for our use case we're going to try to find<00:07:13.979> unreachable<00:07:14.639> branches<00:07:15.120> so<00:07:15.660> here's<00:07:15.900> a 00:07:16.010 --> 00:07:16.020 align:start position:0% find unreachable branches so here's a 00:07:16.020 --> 00:07:17.330 align:start position:0% find unreachable branches so here's a piece<00:07:16.139> of<00:07:16.259> solidity<00:07:16.680> we're<00:07:16.919> going<00:07:17.039> to<00:07:17.100> analyze 00:07:17.330 --> 00:07:17.340 align:start position:0% piece of solidity we're going to analyze 00:07:17.340 --> 00:07:19.309 align:start position:0% piece of solidity we're going to analyze the<00:07:17.460> VM<00:07:17.699> byte<00:07:17.940> code<00:07:18.060> but<00:07:18.539> this<00:07:18.720> is<00:07:18.780> just<00:07:19.020> to 00:07:19.309 --> 00:07:19.319 align:start position:0% the VM byte code but this is just to 00:07:19.319 --> 00:07:20.510 align:start position:0% the VM byte code but this is just to show<00:07:19.560> an<00:07:19.740> example 00:07:20.510 --> 00:07:20.520 align:start position:0% show an example 00:07:20.520 --> 00:07:22.309 align:start position:0% show an example so<00:07:21.060> we<00:07:21.120> have<00:07:21.240> this<00:07:21.360> functional<00:07:21.660> X<00:07:21.840> and<00:07:22.020> integer 00:07:22.309 --> 00:07:22.319 align:start position:0% so we have this functional X and integer 00:07:22.319 --> 00:07:24.770 align:start position:0% so we have this functional X and integer X<00:07:22.560> and<00:07:23.280> first<00:07:23.460> we<00:07:23.699> require<00:07:23.819> that<00:07:24.180> X<00:07:24.360> has<00:07:24.599> to<00:07:24.720> be 00:07:24.770 --> 00:07:24.780 align:start position:0% X and first we require that X has to be 00:07:24.780 --> 00:07:26.890 align:start position:0% X and first we require that X has to be last<00:07:24.900> or<00:07:25.080> equal<00:07:25.259> 10. 00:07:26.890 --> 00:07:26.900 align:start position:0% last or equal 10. 00:07:26.900 --> 00:07:29.629 align:start position:0% last or equal 10. then<00:07:27.900> we<00:07:28.199> have<00:07:28.259> the<00:07:28.500> branches<00:07:28.860> as<00:07:28.979> if<00:07:29.160> x<00:07:29.340> slash 00:07:29.629 --> 00:07:29.639 align:start position:0% then we have the branches as if x slash 00:07:29.639 --> 00:07:32.749 align:start position:0% then we have the branches as if x slash or<00:07:29.699> equal<00:07:29.819> 50<00:07:30.060> does<00:07:30.419> something<00:07:30.660> and<00:07:31.620> then<00:07:31.860> the 00:07:32.749 --> 00:07:32.759 align:start position:0% or equal 50 does something and then the 00:07:32.759 --> 00:07:35.089 align:start position:0% or equal 50 does something and then the rest<00:07:32.940> does<00:07:33.479> return<00:07:33.660> is<00:07:33.960> false 00:07:35.089 --> 00:07:35.099 align:start position:0% rest does return is false 00:07:35.099 --> 00:07:38.089 align:start position:0% rest does return is false so<00:07:35.940> this<00:07:36.479> Branch<00:07:36.840> here<00:07:37.020> basically<00:07:37.560> the<00:07:37.800> false 00:07:38.089 --> 00:07:38.099 align:start position:0% so this Branch here basically the false 00:07:38.099 --> 00:07:39.710 align:start position:0% so this Branch here basically the false branch<00:07:38.400> of<00:07:38.520> the<00:07:38.639> f 00:07:39.710 --> 00:07:39.720 align:start position:0% branch of the f 00:07:39.720 --> 00:07:41.710 align:start position:0% branch of the f it's<00:07:40.080> unreachable<00:07:40.620> right<00:07:40.860> because 00:07:41.710 --> 00:07:41.720 align:start position:0% it's unreachable right because 00:07:41.720 --> 00:07:44.629 align:start position:0% it's unreachable right because ax<00:07:42.720> we<00:07:43.080> know<00:07:43.259> that<00:07:43.440> X<00:07:43.620> is<00:07:43.800> less<00:07:43.979> or<00:07:44.220> equal<00:07:44.400> 10 00:07:44.629 --> 00:07:44.639 align:start position:0% ax we know that X is less or equal 10 00:07:44.639 --> 00:07:46.309 align:start position:0% ax we know that X is less or equal 10 from<00:07:45.000> the<00:07:45.060> beginning<00:07:45.180> of<00:07:45.419> the<00:07:45.479> function 00:07:46.309 --> 00:07:46.319 align:start position:0% from the beginning of the function 00:07:46.319 --> 00:07:48.050 align:start position:0% from the beginning of the function which<00:07:46.800> means<00:07:47.039> it's<00:07:47.280> always<00:07:47.460> less<00:07:47.699> or<00:07:47.880> equal 00:07:48.050 --> 00:07:48.060 align:start position:0% which means it's always less or equal 00:07:48.060 --> 00:07:49.309 align:start position:0% which means it's always less or equal 50. 00:07:49.309 --> 00:07:49.319 align:start position:0% 50. 00:07:49.319 --> 00:07:51.290 align:start position:0% 50. meaning<00:07:49.680> that<00:07:49.979> it<00:07:50.099> will<00:07:50.220> always<00:07:50.460> enter<00:07:50.819> the<00:07:51.060> if 00:07:51.290 --> 00:07:51.300 align:start position:0% meaning that it will always enter the if 00:07:51.300 --> 00:07:54.110 align:start position:0% meaning that it will always enter the if and<00:07:52.199> it<00:07:52.319> will<00:07:52.440> never<00:07:52.680> come<00:07:53.039> to<00:07:53.280> this<00:07:53.580> part<00:07:53.940> of 00:07:54.110 --> 00:07:54.120 align:start position:0% and it will never come to this part of 00:07:54.120 --> 00:07:55.550 align:start position:0% and it will never come to this part of the<00:07:54.180> of<00:07:54.360> the<00:07:54.599> code<00:07:54.660> so<00:07:54.900> if<00:07:55.080> you<00:07:55.139> take<00:07:55.259> the<00:07:55.380> true 00:07:55.550 --> 00:07:55.560 align:start position:0% the of the code so if you take the true 00:07:55.560 --> 00:07:59.210 align:start position:0% the of the code so if you take the true Branch<00:07:55.940> this<00:07:56.940> is<00:07:57.060> reachable<00:07:57.360> because<00:07:58.220> these 00:07:59.210 --> 00:07:59.220 align:start position:0% Branch this is reachable because these 00:07:59.220 --> 00:08:01.570 align:start position:0% Branch this is reachable because these constraints<00:08:00.120> are 00:08:01.570 --> 00:08:01.580 align:start position:0% constraints are 00:08:01.580 --> 00:08:03.529 align:start position:0% constraints are together 00:08:03.529 --> 00:08:03.539 align:start position:0% together 00:08:03.539 --> 00:08:05.930 align:start position:0% together but<00:08:03.960> these<00:08:04.199> are<00:08:04.319> not<00:08:04.440> right<00:08:05.039> so<00:08:05.280> if<00:08:05.400> x<00:08:05.580> has<00:08:05.880> to 00:08:05.930 --> 00:08:05.940 align:start position:0% but these are not right so if x has to 00:08:05.940 --> 00:08:07.730 align:start position:0% but these are not right so if x has to be<00:08:06.060> less<00:08:06.180> or<00:08:06.479> equal<00:08:06.599> 10<00:08:06.840> it<00:08:07.020> cannot<00:08:07.259> be<00:08:07.380> greater 00:08:07.730 --> 00:08:07.740 align:start position:0% be less or equal 10 it cannot be greater 00:08:07.740 --> 00:08:10.249 align:start position:0% be less or equal 10 it cannot be greater than<00:08:08.099> 50.<00:08:08.819> so<00:08:09.000> this<00:08:09.479> branch<00:08:09.720> is<00:08:09.840> unreachable 00:08:10.249 --> 00:08:10.259 align:start position:0% than 50. so this branch is unreachable 00:08:10.259 --> 00:08:11.629 align:start position:0% than 50. so this branch is unreachable we<00:08:10.500> can<00:08:10.560> remove<00:08:10.680> the<00:08:10.919> whole<00:08:11.039> thing<00:08:11.160> well<00:08:11.400> not 00:08:11.629 --> 00:08:11.639 align:start position:0% we can remove the whole thing well not 00:08:11.639 --> 00:08:14.390 align:start position:0% we can remove the whole thing well not the<00:08:11.819> whole<00:08:11.940> thing<00:08:12.060> just<00:08:12.360> the<00:08:13.080> the<00:08:13.440> bottom<00:08:13.800> the 00:08:14.390 --> 00:08:14.400 align:start position:0% the whole thing just the the bottom the 00:08:14.400 --> 00:08:16.129 align:start position:0% the whole thing just the the bottom the cool<00:08:14.520> thing<00:08:14.699> about<00:08:15.060> trying<00:08:15.599> to<00:08:15.720> do<00:08:15.840> that<00:08:15.900> stuff 00:08:16.129 --> 00:08:16.139 align:start position:0% cool thing about trying to do that stuff 00:08:16.139 --> 00:08:18.529 align:start position:0% cool thing about trying to do that stuff is<00:08:16.380> that<00:08:16.500> we<00:08:16.680> need<00:08:16.800> very<00:08:17.099> little<00:08:17.280> support<00:08:17.639> from 00:08:18.529 --> 00:08:18.539 align:start position:0% is that we need very little support from 00:08:18.539 --> 00:08:19.790 align:start position:0% is that we need very little support from the<00:08:18.599> evm<00:08:18.960> of<00:08:19.139> course<00:08:19.199> if<00:08:19.319> you<00:08:19.440> want<00:08:19.560> to<00:08:19.680> write 00:08:19.790 --> 00:08:19.800 align:start position:0% the evm of course if you want to write 00:08:19.800 --> 00:08:21.290 align:start position:0% the evm of course if you want to write if<00:08:20.460> you<00:08:20.580> want<00:08:20.699> to<00:08:20.819> write<00:08:20.879> a<00:08:20.940> symbolic 00:08:21.290 --> 00:08:21.300 align:start position:0% if you want to write a symbolic 00:08:21.300 --> 00:08:22.430 align:start position:0% if you want to write a symbolic education<00:08:21.599> engineer<00:08:22.020> to<00:08:22.199> write<00:08:22.259> an 00:08:22.430 --> 00:08:22.440 align:start position:0% education engineer to write an 00:08:22.440 --> 00:08:24.050 align:start position:0% education engineer to write an interpreter<00:08:22.800> in<00:08:22.919> the<00:08:23.039> first<00:08:23.099> place<00:08:23.340> right<00:08:23.879> you 00:08:24.050 --> 00:08:24.060 align:start position:0% interpreter in the first place right you 00:08:24.060 --> 00:08:25.730 align:start position:0% interpreter in the first place right you need<00:08:24.180> an<00:08:24.360> NVM<00:08:24.660> interpreter 00:08:25.730 --> 00:08:25.740 align:start position:0% need an NVM interpreter 00:08:25.740 --> 00:08:27.409 align:start position:0% need an NVM interpreter but<00:08:26.280> we<00:08:26.580> don't<00:08:26.699> want<00:08:26.819> to<00:08:26.940> deal<00:08:27.060> with<00:08:27.240> every 00:08:27.409 --> 00:08:27.419 align:start position:0% but we don't want to deal with every 00:08:27.419 --> 00:08:29.210 align:start position:0% but we don't want to deal with every object<00:08:27.720> because<00:08:28.020> it<00:08:28.379> gets<00:08:28.620> really<00:08:28.800> big<00:08:28.979> really 00:08:29.210 --> 00:08:29.220 align:start position:0% object because it gets really big really 00:08:29.220 --> 00:08:30.890 align:start position:0% object because it gets really big really complicated<00:08:29.699> and<00:08:30.360> we<00:08:30.479> don't<00:08:30.599> want<00:08:30.720> to<00:08:30.840> do 00:08:30.890 --> 00:08:30.900 align:start position:0% complicated and we don't want to do 00:08:30.900 --> 00:08:32.690 align:start position:0% complicated and we don't want to do things<00:08:31.020> like<00:08:31.199> call<00:08:31.440> create<00:08:31.800> and<00:08:32.219> storage<00:08:32.459> and 00:08:32.690 --> 00:08:32.700 align:start position:0% things like call create and storage and 00:08:32.700 --> 00:08:34.250 align:start position:0% things like call create and storage and all<00:08:32.820> these<00:08:33.000> complicated<00:08:33.300> stuff<00:08:33.599> which<00:08:34.080> of 00:08:34.250 --> 00:08:34.260 align:start position:0% all these complicated stuff which of 00:08:34.260 --> 00:08:35.570 align:start position:0% all these complicated stuff which of course<00:08:34.380> you<00:08:34.500> could<00:08:34.680> and<00:08:34.800> a<00:08:34.979> lot<00:08:35.039> of<00:08:35.099> tools<00:08:35.399> do 00:08:35.570 --> 00:08:35.580 align:start position:0% course you could and a lot of tools do 00:08:35.580 --> 00:08:37.190 align:start position:0% course you could and a lot of tools do that<00:08:35.760> we<00:08:36.419> don't<00:08:36.599> want<00:08:36.719> to<00:08:36.839> do<00:08:36.899> that<00:08:37.020> in 00:08:37.190 --> 00:08:37.200 align:start position:0% that we don't want to do that in 00:08:37.200 --> 00:08:38.990 align:start position:0% that we don't want to do that in solidity<00:08:37.620> the<00:08:38.039> cool<00:08:38.219> thing<00:08:38.339> again<00:08:38.520> about<00:08:38.760> this 00:08:38.990 --> 00:08:39.000 align:start position:0% solidity the cool thing again about this 00:08:39.000 --> 00:08:41.089 align:start position:0% solidity the cool thing again about this encoding<00:08:39.419> we<00:08:39.719> we<00:08:40.020> only<00:08:40.260> have<00:08:40.560> to<00:08:40.740> care<00:08:40.919> about 00:08:41.089 --> 00:08:41.099 align:start position:0% encoding we we only have to care about 00:08:41.099 --> 00:08:43.850 align:start position:0% encoding we we only have to care about the<00:08:41.700> stack<00:08:41.940> operations 00:08:43.850 --> 00:08:43.860 align:start position:0% the stack operations 00:08:43.860 --> 00:08:48.250 align:start position:0% the stack operations um control<00:08:44.099> flow<00:08:44.399> so<00:08:45.360> it<00:08:45.540> jumps<00:08:45.959> and 00:08:48.250 --> 00:08:48.260 align:start position:0% um control flow so it jumps and 00:08:48.260 --> 00:08:50.990 align:start position:0% um control flow so it jumps and opcodes<00:08:49.260> that<00:08:49.500> stop<00:08:49.680> the<00:08:49.980> execution 00:08:50.990 --> 00:08:51.000 align:start position:0% opcodes that stop the execution 00:08:51.000 --> 00:08:52.970 align:start position:0% opcodes that stop the execution and<00:08:51.420> relation<00:08:51.720> upgrades 00:08:52.970 --> 00:08:52.980 align:start position:0% and relation upgrades 00:08:52.980 --> 00:08:54.710 align:start position:0% and relation upgrades and<00:08:53.640> so<00:08:53.880> basically<00:08:54.180> we're<00:08:54.360> going<00:08:54.480> to<00:08:54.600> Care 00:08:54.710 --> 00:08:54.720 align:start position:0% and so basically we're going to Care 00:08:54.720 --> 00:08:57.230 align:start position:0% and so basically we're going to Care mostly<00:08:55.140> about<00:08:55.260> as<00:08:55.440> I<00:08:55.620> saw<00:08:55.740> before<00:08:55.920> ifs<00:08:56.760> with 00:08:57.230 --> 00:08:57.240 align:start position:0% mostly about as I saw before ifs with 00:08:57.240 --> 00:08:59.570 align:start position:0% mostly about as I saw before ifs with relation<00:08:57.839> operators<00:08:58.320> inside<00:08:58.680> so<00:08:59.100> less<00:08:59.399> than 00:08:59.570 --> 00:08:59.580 align:start position:0% relation operators inside so less than 00:08:59.580 --> 00:09:01.310 align:start position:0% relation operators inside so less than greater<00:08:59.940> than<00:09:00.060> and<00:09:00.360> the<00:09:00.540> negation<00:09:00.899> of<00:09:01.080> these 00:09:01.310 --> 00:09:01.320 align:start position:0% greater than and the negation of these 00:09:01.320 --> 00:09:03.530 align:start position:0% greater than and the negation of these so<00:09:01.500> that<00:09:01.620> you<00:09:01.800> can<00:09:01.980> get<00:09:02.160> less<00:09:03.000> than<00:09:03.180> or<00:09:03.360> equal 00:09:03.530 --> 00:09:03.540 align:start position:0% so that you can get less than or equal 00:09:03.540 --> 00:09:05.870 align:start position:0% so that you can get less than or equal and<00:09:04.019> greater<00:09:04.380> than<00:09:04.500> or<00:09:04.800> equal<00:09:04.980> the<00:09:05.459> symbolic 00:09:05.870 --> 00:09:05.880 align:start position:0% and greater than or equal the symbolic 00:09:05.880 --> 00:09:07.009 align:start position:0% and greater than or equal the symbolic encoding<00:09:06.240> we're<00:09:06.360> going<00:09:06.540> to<00:09:06.600> use<00:09:06.660> is<00:09:06.779> also 00:09:07.009 --> 00:09:07.019 align:start position:0% encoding we're going to use is also 00:09:07.019 --> 00:09:08.210 align:start position:0% encoding we're going to use is also pretty<00:09:07.140> simple 00:09:08.210 --> 00:09:08.220 align:start position:0% pretty simple 00:09:08.220 --> 00:09:10.850 align:start position:0% pretty simple so<00:09:08.700> for<00:09:08.940> every<00:09:09.300> evm<00:09:09.959> expression<00:09:10.380> that<00:09:10.500> we<00:09:10.680> saw 00:09:10.850 --> 00:09:10.860 align:start position:0% so for every evm expression that we saw 00:09:10.860 --> 00:09:12.829 align:start position:0% so for every evm expression that we saw before<00:09:11.100> we're<00:09:12.000> going<00:09:12.120> to<00:09:12.300> transform<00:09:12.600> it<00:09:12.779> into 00:09:12.829 --> 00:09:12.839 align:start position:0% before we're going to transform it into 00:09:12.839 --> 00:09:15.829 align:start position:0% before we're going to transform it into math<00:09:13.260> constraint<00:09:14.220> of<00:09:14.880> the<00:09:15.000> form<00:09:15.180> a<00:09:15.420> minus<00:09:15.720> B 00:09:15.829 --> 00:09:15.839 align:start position:0% math constraint of the form a minus B 00:09:15.839 --> 00:09:18.230 align:start position:0% math constraint of the form a minus B less<00:09:16.019> or<00:09:16.200> equal<00:09:16.320> K<00:09:16.620> where<00:09:17.459> A<00:09:17.700> and<00:09:17.820> B<00:09:18.000> are<00:09:18.120> going 00:09:18.230 --> 00:09:18.240 align:start position:0% less or equal K where A and B are going 00:09:18.240 --> 00:09:19.610 align:start position:0% less or equal K where A and B are going to<00:09:18.300> be<00:09:18.360> variables<00:09:18.779> and<00:09:18.959> K<00:09:19.140> is<00:09:19.260> going<00:09:19.380> to<00:09:19.440> be<00:09:19.560> a 00:09:19.610 --> 00:09:19.620 align:start position:0% to be variables and K is going to be a 00:09:19.620 --> 00:09:22.430 align:start position:0% to be variables and K is going to be a constant<00:09:19.980> so<00:09:20.760> this<00:09:21.180> is<00:09:21.540> also<00:09:21.779> what<00:09:21.959> Harry<00:09:22.140> was 00:09:22.430 --> 00:09:22.440 align:start position:0% constant so this is also what Harry was 00:09:22.440 --> 00:09:25.730 align:start position:0% constant so this is also what Harry was talking<00:09:22.620> about<00:09:22.740> yesterday<00:09:23.279> in<00:09:23.940> in<00:09:24.480> his<00:09:24.720> talk 00:09:25.730 --> 00:09:25.740 align:start position:0% talking about yesterday in in his talk 00:09:25.740 --> 00:09:27.650 align:start position:0% talking about yesterday in in his talk and<00:09:26.160> we<00:09:26.279> got<00:09:26.459> things<00:09:26.700> like<00:09:26.880> like<00:09:27.120> this<00:09:27.360> for 00:09:27.650 --> 00:09:27.660 align:start position:0% and we got things like like this for 00:09:27.660 --> 00:09:29.509 align:start position:0% and we got things like like this for example<00:09:27.839> whoever<00:09:28.620> was<00:09:28.800> in<00:09:28.980> Harry's<00:09:29.399> talking 00:09:29.509 --> 00:09:29.519 align:start position:0% example whoever was in Harry's talking 00:09:29.519 --> 00:09:31.970 align:start position:0% example whoever was in Harry's talking together<00:09:29.820> is<00:09:30.300> this<00:09:30.600> uh<00:09:30.959> system<00:09:31.200> satisfiable 00:09:31.970 --> 00:09:31.980 align:start position:0% together is this uh system satisfiable 00:09:31.980 --> 00:09:34.009 align:start position:0% together is this uh system satisfiable yeah<00:09:32.640> so<00:09:32.760> if<00:09:32.880> you<00:09:33.000> sum<00:09:33.180> everything<00:09:33.360> on<00:09:33.779> both 00:09:34.009 --> 00:09:34.019 align:start position:0% yeah so if you sum everything on both 00:09:34.019 --> 00:09:36.470 align:start position:0% yeah so if you sum everything on both sides<00:09:34.440> then<00:09:35.040> you<00:09:35.220> get<00:09:35.399> basically<00:09:35.820> zero<00:09:36.240> last 00:09:36.470 --> 00:09:36.480 align:start position:0% sides then you get basically zero last 00:09:36.480 --> 00:09:38.630 align:start position:0% sides then you get basically zero last Oracle<00:09:36.980> minus<00:09:37.980> two<00:09:38.160> which<00:09:38.399> is<00:09:38.519> a 00:09:38.630 --> 00:09:38.640 align:start position:0% Oracle minus two which is a 00:09:38.640 --> 00:09:40.790 align:start position:0% Oracle minus two which is a contradiction<00:09:39.060> so<00:09:40.019> this<00:09:40.200> system<00:09:40.440> is 00:09:40.790 --> 00:09:40.800 align:start position:0% contradiction so this system is 00:09:40.800 --> 00:09:43.730 align:start position:0% contradiction so this system is impossible<00:09:41.339> to<00:09:41.880> be<00:09:42.000> satisfiable 00:09:43.730 --> 00:09:43.740 align:start position:0% impossible to be satisfiable 00:09:43.740 --> 00:09:45.710 align:start position:0% impossible to be satisfiable um<00:09:43.860> the<00:09:44.339> reason<00:09:44.519> why<00:09:44.760> we<00:09:44.880> like<00:09:45.000> this<00:09:45.240> encoding 00:09:45.710 --> 00:09:45.720 align:start position:0% um the reason why we like this encoding 00:09:45.720 --> 00:09:46.850 align:start position:0% um the reason why we like this encoding is<00:09:45.899> because 00:09:46.850 --> 00:09:46.860 align:start position:0% is because 00:09:46.860 --> 00:09:49.310 align:start position:0% is because we<00:09:47.160> can<00:09:47.339> use<00:09:47.459> a<00:09:47.640> difference<00:09:47.760> logic<00:09:48.240> solver<00:09:48.540> and 00:09:49.310 --> 00:09:49.320 align:start position:0% we can use a difference logic solver and 00:09:49.320 --> 00:09:51.290 align:start position:0% we can use a difference logic solver and again<00:09:49.440> as<00:09:49.680> Harry<00:09:49.860> explained<00:09:50.279> yesterday<00:09:50.399> a 00:09:51.290 --> 00:09:51.300 align:start position:0% again as Harry explained yesterday a 00:09:51.300 --> 00:09:52.670 align:start position:0% again as Harry explained yesterday a difference<00:09:51.480> logic<00:09:51.899> solver<00:09:52.140> is<00:09:52.260> very<00:09:52.500> simple 00:09:52.670 --> 00:09:52.680 align:start position:0% difference logic solver is very simple 00:09:52.680 --> 00:09:54.410 align:start position:0% difference logic solver is very simple to<00:09:52.980> write<00:09:53.100> what<00:09:53.519> does<00:09:53.640> it<00:09:53.760> do<00:09:53.940> it<00:09:54.180> basically 00:09:54.410 --> 00:09:54.420 align:start position:0% to write what does it do it basically 00:09:54.420 --> 00:09:56.329 align:start position:0% to write what does it do it basically takes<00:09:54.720> these<00:09:55.080> constraints<00:09:55.440> these<00:09:56.279> math 00:09:56.329 --> 00:09:56.339 align:start position:0% takes these constraints these math 00:09:56.339 --> 00:09:58.730 align:start position:0% takes these constraints these math constraints<00:09:56.940> and<00:09:57.480> it<00:09:57.600> tells<00:09:57.899> you 00:09:58.730 --> 00:09:58.740 align:start position:0% constraints and it tells you 00:09:58.740 --> 00:10:00.949 align:start position:0% constraints and it tells you whether<00:09:59.279> it's<00:09:59.459> possible<00:09:59.760> or<00:10:00.000> not<00:10:00.120> that<00:10:00.720> these 00:10:00.949 --> 00:10:00.959 align:start position:0% whether it's possible or not that these 00:10:00.959 --> 00:10:02.269 align:start position:0% whether it's possible or not that these things<00:10:01.019> are<00:10:01.260> satisfiable<00:10:01.740> at<00:10:01.920> the<00:10:01.980> same<00:10:02.100> time 00:10:02.269 --> 00:10:02.279 align:start position:0% things are satisfiable at the same time 00:10:02.279 --> 00:10:04.250 align:start position:0% things are satisfiable at the same time and<00:10:02.940> if<00:10:03.060> it<00:10:03.240> is<00:10:03.360> possible<00:10:03.720> it's<00:10:03.959> going<00:10:04.080> to<00:10:04.140> give 00:10:04.250 --> 00:10:04.260 align:start position:0% and if it is possible it's going to give 00:10:04.260 --> 00:10:05.630 align:start position:0% and if it is possible it's going to give you<00:10:04.380> values<00:10:04.740> for<00:10:04.920> the<00:10:05.040> variables<00:10:05.339> that<00:10:05.459> make 00:10:05.630 --> 00:10:05.640 align:start position:0% you values for the variables that make 00:10:05.640 --> 00:10:07.310 align:start position:0% you values for the variables that make it<00:10:05.820> satisfiable<00:10:06.240> otherwise<00:10:06.959> it<00:10:07.080> just<00:10:07.200> says 00:10:07.310 --> 00:10:07.320 align:start position:0% it satisfiable otherwise it just says 00:10:07.320 --> 00:10:09.470 align:start position:0% it satisfiable otherwise it just says it's<00:10:07.740> not<00:10:07.920> possible<00:10:08.220> at<00:10:08.519> all<00:10:08.700> for<00:10:09.240> these 00:10:09.470 --> 00:10:09.480 align:start position:0% it's not possible at all for these 00:10:09.480 --> 00:10:12.050 align:start position:0% it's not possible at all for these things<00:10:09.600> to<00:10:09.779> be<00:10:09.899> satisfiable<00:10:10.440> together 00:10:12.050 --> 00:10:12.060 align:start position:0% things to be satisfiable together 00:10:12.060 --> 00:10:14.870 align:start position:0% things to be satisfiable together um<00:10:12.180> the<00:10:12.420> solver<00:10:12.720> is<00:10:12.839> much<00:10:13.080> simpler<00:10:13.440> than<00:10:14.160> the 00:10:14.870 --> 00:10:14.880 align:start position:0% um the solver is much simpler than the 00:10:14.880 --> 00:10:17.210 align:start position:0% um the solver is much simpler than the things<00:10:15.000> you<00:10:15.180> need<00:10:15.360> like<00:10:15.660> ILP<00:10:16.140> or<00:10:16.260> smt<00:10:16.740> when<00:10:17.100> you 00:10:17.210 --> 00:10:17.220 align:start position:0% things you need like ILP or smt when you 00:10:17.220 --> 00:10:18.470 align:start position:0% things you need like ILP or smt when you need<00:10:17.399> to<00:10:17.519> solve<00:10:17.760> with<00:10:17.820> linear<00:10:18.120> combinations 00:10:18.470 --> 00:10:18.480 align:start position:0% need to solve with linear combinations 00:10:18.480 --> 00:10:20.810 align:start position:0% need to solve with linear combinations or<00:10:18.839> even<00:10:19.080> non-linear<00:10:19.620> expressions<00:10:19.980> and<00:10:20.279> the 00:10:20.810 --> 00:10:20.820 align:start position:0% or even non-linear expressions and the 00:10:20.820 --> 00:10:22.850 align:start position:0% or even non-linear expressions and the sorts<00:10:21.360> of<00:10:21.420> things<00:10:21.600> that<00:10:22.320> you<00:10:22.440> end<00:10:22.560> up<00:10:22.740> with 00:10:22.850 --> 00:10:22.860 align:start position:0% sorts of things that you end up with 00:10:22.860 --> 00:10:25.310 align:start position:0% sorts of things that you end up with when<00:10:23.160> you<00:10:23.279> start<00:10:23.459> encoding<00:10:24.320> arithmetic 00:10:25.310 --> 00:10:25.320 align:start position:0% when you start encoding arithmetic 00:10:25.320 --> 00:10:28.550 align:start position:0% when you start encoding arithmetic expressions<00:10:25.740> and<00:10:26.100> other<00:10:26.279> things<00:10:26.720> and<00:10:27.720> as<00:10:28.260> also 00:10:28.550 --> 00:10:28.560 align:start position:0% expressions and other things and as also 00:10:28.560 --> 00:10:30.170 align:start position:0% expressions and other things and as also higher<00:10:28.860> explained<00:10:29.160> yesterday<00:10:29.279> this<00:10:29.760> runs<00:10:30.120> in 00:10:30.170 --> 00:10:30.180 align:start position:0% higher explained yesterday this runs in 00:10:30.180 --> 00:10:32.509 align:start position:0% higher explained yesterday this runs in employ<00:10:30.540> normal<00:10:30.779> time 00:10:32.509 --> 00:10:32.519 align:start position:0% employ normal time 00:10:32.519 --> 00:10:34.130 align:start position:0% employ normal time on<00:10:33.060> the<00:10:33.240> graph<00:10:33.420> generated<00:10:33.839> from<00:10:34.019> the 00:10:34.130 --> 00:10:34.140 align:start position:0% on the graph generated from the 00:10:34.140 --> 00:10:36.290 align:start position:0% on the graph generated from the constraints<00:10:34.560> using<00:10:35.399> the<00:10:35.519> volume<00:10:35.700> four<00:10:36.000> graph 00:10:36.290 --> 00:10:36.300 align:start position:0% constraints using the volume four graph 00:10:36.300 --> 00:10:38.210 align:start position:0% constraints using the volume four graph algorithm<00:10:36.660> not<00:10:36.959> going<00:10:37.140> to<00:10:37.260> go<00:10:37.380> much<00:10:37.860> into<00:10:38.040> that 00:10:38.210 --> 00:10:38.220 align:start position:0% algorithm not going to go much into that 00:10:38.220 --> 00:10:39.290 align:start position:0% algorithm not going to go much into that if<00:10:38.399> you<00:10:38.519> want<00:10:38.640> to<00:10:38.760> learn<00:10:38.820> more<00:10:38.940> about<00:10:39.120> that 00:10:39.290 --> 00:10:39.300 align:start position:0% if you want to learn more about that 00:10:39.300 --> 00:10:40.730 align:start position:0% if you want to learn more about that please<00:10:39.540> re-watch 00:10:40.730 --> 00:10:40.740 align:start position:0% please re-watch 00:10:40.740 --> 00:10:41.870 align:start position:0% please re-watch um Harris<00:10:41.040> talk 00:10:41.870 --> 00:10:41.880 align:start position:0% um Harris talk 00:10:41.880 --> 00:10:44.750 align:start position:0% um Harris talk and<00:10:42.480> this<00:10:43.019> algorithm<00:10:43.320> is<00:10:43.560> super<00:10:43.740> simple<00:10:43.980> this 00:10:44.750 --> 00:10:44.760 align:start position:0% and this algorithm is super simple this 00:10:44.760 --> 00:10:46.370 align:start position:0% and this algorithm is super simple this is<00:10:44.880> basically<00:10:45.240> almost<00:10:45.420> the<00:10:45.720> whole<00:10:45.839> thing<00:10:46.019> and 00:10:46.370 --> 00:10:46.380 align:start position:0% is basically almost the whole thing and 00:10:46.380 --> 00:10:49.370 align:start position:0% is basically almost the whole thing and most<00:10:46.560> of<00:10:46.740> it<00:10:46.860> is<00:10:47.040> comments<00:10:48.000> um<00:10:48.060> so<00:10:48.600> now<00:10:48.959> all<00:10:49.200> we 00:10:49.370 --> 00:10:49.380 align:start position:0% most of it is comments um so now all we 00:10:49.380 --> 00:10:50.630 align:start position:0% most of it is comments um so now all we need<00:10:49.500> to<00:10:49.620> do<00:10:49.740> is 00:10:50.630 --> 00:10:50.640 align:start position:0% need to do is 00:10:50.640 --> 00:10:53.329 align:start position:0% need to do is put<00:10:51.060> it<00:10:51.180> all<00:10:51.360> together<00:10:51.800> so<00:10:52.800> this<00:10:52.980> is<00:10:53.040> the<00:10:53.160> whole 00:10:53.329 --> 00:10:53.339 align:start position:0% put it all together so this is the whole 00:10:53.339 --> 00:10:54.230 align:start position:0% put it all together so this is the whole project 00:10:54.230 --> 00:10:54.240 align:start position:0% project 00:10:54.240 --> 00:10:57.230 align:start position:0% project so<00:10:55.140> these<00:10:55.500> are<00:10:55.560> two<00:10:55.860> tests<00:10:56.279> files<00:10:56.700> one<00:10:56.940> for<00:10:57.120> the 00:10:57.230 --> 00:10:57.240 align:start position:0% so these are two tests files one for the 00:10:57.240 --> 00:10:58.490 align:start position:0% so these are two tests files one for the solver<00:10:57.480> itself<00:10:57.720> just<00:10:57.959> like<00:10:58.079> you<00:10:58.260> need<00:10:58.380> to<00:10:58.440> test 00:10:58.490 --> 00:10:58.500 align:start position:0% solver itself just like you need to test 00:10:58.500 --> 00:11:00.170 align:start position:0% solver itself just like you need to test for<00:10:58.680> the<00:10:58.800> solver<00:10:59.100> and<00:10:59.459> one<00:10:59.700> for<00:10:59.820> the<00:10:59.940> symbol 00:11:00.170 --> 00:11:00.180 align:start position:0% for the solver and one for the symbol 00:11:00.180 --> 00:11:01.910 align:start position:0% for the solver and one for the symbol execution<00:11:00.480> engine<00:11:00.720> and<00:11:01.320> then<00:11:01.380> you<00:11:01.560> have<00:11:01.680> all 00:11:01.910 --> 00:11:01.920 align:start position:0% execution engine and then you have all 00:11:01.920 --> 00:11:04.130 align:start position:0% execution engine and then you have all those<00:11:02.100> files<00:11:02.459> for<00:11:02.700> the 00:11:04.130 --> 00:11:04.140 align:start position:0% those files for the 00:11:04.140 --> 00:11:05.750 align:start position:0% those files for the um for<00:11:04.380> the<00:11:04.560> whole<00:11:04.680> engine 00:11:05.750 --> 00:11:05.760 align:start position:0% um for the whole engine 00:11:05.760 --> 00:11:07.370 align:start position:0% um for the whole engine so 00:11:07.370 --> 00:11:07.380 align:start position:0% so 00:11:07.380 --> 00:11:08.870 align:start position:0% so what<00:11:07.800> we<00:11:07.920> want<00:11:08.100> to<00:11:08.220> do<00:11:08.279> is<00:11:08.399> like<00:11:08.579> write<00:11:08.760> an 00:11:08.870 --> 00:11:08.880 align:start position:0% what we want to do is like write an 00:11:08.880 --> 00:11:10.430 align:start position:0% what we want to do is like write an interpreter<00:11:09.300> how<00:11:09.600> do<00:11:09.720> we<00:11:09.839> write<00:11:09.959> interpreter 00:11:10.430 --> 00:11:10.440 align:start position:0% interpreter how do we write interpreter 00:11:10.440 --> 00:11:13.490 align:start position:0% interpreter how do we write interpreter we<00:11:11.220> need<00:11:11.399> so<00:11:12.060> by<00:11:12.240> the<00:11:12.360> way<00:11:12.480> please<00:11:12.959> if<00:11:13.260> you<00:11:13.380> have 00:11:13.490 --> 00:11:13.500 align:start position:0% we need so by the way please if you have 00:11:13.500 --> 00:11:15.470 align:start position:0% we need so by the way please if you have questions<00:11:13.680> just<00:11:14.040> like<00:11:14.160> try<00:11:14.399> to<00:11:14.579> you<00:11:15.000> can<00:11:15.180> ask 00:11:15.470 --> 00:11:15.480 align:start position:0% questions just like try to you can ask 00:11:15.480 --> 00:11:17.090 align:start position:0% questions just like try to you can ask questions<00:11:15.720> right<00:11:16.019> now<00:11:16.140> just<00:11:16.500> to<00:11:16.620> make<00:11:16.740> sure<00:11:16.860> we 00:11:17.090 --> 00:11:17.100 align:start position:0% questions right now just to make sure we 00:11:17.100 --> 00:11:20.150 align:start position:0% questions right now just to make sure we we<00:11:17.339> go<00:11:17.519> and<00:11:17.940> um<00:11:17.940> in<00:11:18.540> a<00:11:18.660> good<00:11:18.779> flow 00:11:20.150 --> 00:11:20.160 align:start position:0% we go and um in a good flow 00:11:20.160 --> 00:11:22.250 align:start position:0% we go and um in a good flow um<00:11:20.279> actually<00:11:20.640> it's<00:11:20.880> not<00:11:21.120> here<00:11:21.300> so<00:11:21.839> usually 00:11:22.250 --> 00:11:22.260 align:start position:0% um actually it's not here so usually 00:11:22.260 --> 00:11:24.110 align:start position:0% um actually it's not here so usually when<00:11:22.560> you<00:11:22.740> write<00:11:22.920> this<00:11:23.100> interpreter<00:11:23.519> for<00:11:23.700> evm 00:11:24.110 --> 00:11:24.120 align:start position:0% when you write this interpreter for evm 00:11:24.120 --> 00:11:25.850 align:start position:0% when you write this interpreter for evm you<00:11:24.240> have<00:11:24.420> this<00:11:24.540> context<00:11:24.899> what<00:11:25.560> is<00:11:25.740> the 00:11:25.850 --> 00:11:25.860 align:start position:0% you have this context what is the 00:11:25.860 --> 00:11:27.230 align:start position:0% you have this context what is the context<00:11:26.100> you<00:11:26.399> have<00:11:26.519> the<00:11:26.700> code<00:11:26.820> that<00:11:27.060> are 00:11:27.230 --> 00:11:27.240 align:start position:0% context you have the code that are 00:11:27.240 --> 00:11:30.110 align:start position:0% context you have the code that are executing<00:11:28.200> you<00:11:28.620> have<00:11:28.680> the<00:11:28.860> program<00:11:28.980> counter 00:11:30.110 --> 00:11:30.120 align:start position:0% executing you have the program counter 00:11:30.120 --> 00:11:31.970 align:start position:0% executing you have the program counter like<00:11:30.720> what<00:11:31.019> which<00:11:31.260> upgrade<00:11:31.620> are<00:11:31.860> you 00:11:31.970 --> 00:11:31.980 align:start position:0% like what which upgrade are you 00:11:31.980 --> 00:11:34.670 align:start position:0% like what which upgrade are you executing<00:11:32.279> right<00:11:32.519> now<00:11:32.700> we<00:11:33.420> have<00:11:33.600> a<00:11:33.720> stack<00:11:34.019> in 00:11:34.670 --> 00:11:34.680 align:start position:0% executing right now we have a stack in 00:11:34.680 --> 00:11:35.810 align:start position:0% executing right now we have a stack in our<00:11:34.800> case<00:11:35.040> it's<00:11:35.160> going<00:11:35.279> to<00:11:35.279> be<00:11:35.339> a<00:11:35.399> symbolic 00:11:35.810 --> 00:11:35.820 align:start position:0% our case it's going to be a symbolic 00:11:35.820 --> 00:11:37.310 align:start position:0% our case it's going to be a symbolic stack 00:11:37.310 --> 00:11:37.320 align:start position:0% stack 00:11:37.320 --> 00:11:38.990 align:start position:0% stack um<00:11:37.380> don't<00:11:37.740> worry<00:11:37.980> about<00:11:38.100> that<00:11:38.279> now 00:11:38.990 --> 00:11:39.000 align:start position:0% um don't worry about that now 00:11:39.000 --> 00:11:43.069 align:start position:0% um don't worry about that now we<00:11:39.660> have<00:11:40.019> a<00:11:40.560> path<00:11:40.980> which<00:11:41.940> basically<00:11:42.420> it's<00:11:42.899> a 00:11:43.069 --> 00:11:43.079 align:start position:0% we have a path which basically it's a 00:11:43.079 --> 00:11:44.990 align:start position:0% we have a path which basically it's a it's<00:11:43.260> a<00:11:43.380> path<00:11:43.560> of<00:11:43.920> all<00:11:44.100> the<00:11:44.279> program<00:11:44.399> like<00:11:44.820> of 00:11:44.990 --> 00:11:45.000 align:start position:0% it's a path of all the program like of 00:11:45.000 --> 00:11:46.790 align:start position:0% it's a path of all the program like of the<00:11:45.180> program<00:11:45.300> counters<00:11:45.779> that<00:11:46.019> were<00:11:46.260> visited 00:11:46.790 --> 00:11:46.800 align:start position:0% the program counters that were visited 00:11:46.800 --> 00:11:49.069 align:start position:0% the program counters that were visited in<00:11:47.160> the<00:11:47.279> in<00:11:47.459> the<00:11:47.579> jumps<00:11:47.940> and<00:11:48.720> we're<00:11:48.839> going<00:11:48.959> to 00:11:49.069 --> 00:11:49.079 align:start position:0% in the in the jumps and we're going to 00:11:49.079 --> 00:11:51.949 align:start position:0% in the in the jumps and we're going to use<00:11:49.140> this<00:11:49.440> to<00:11:49.860> detect<00:11:50.579> loops<00:11:51.060> and<00:11:51.540> exit 00:11:51.949 --> 00:11:51.959 align:start position:0% use this to detect loops and exit 00:11:51.959 --> 00:11:54.110 align:start position:0% use this to detect loops and exit because<00:11:52.140> we<00:11:52.320> don't<00:11:52.380> want<00:11:52.560> to<00:11:52.620> encode<00:11:52.920> loops 00:11:54.110 --> 00:11:54.120 align:start position:0% because we don't want to encode loops 00:11:54.120 --> 00:11:55.670 align:start position:0% because we don't want to encode loops we<00:11:54.660> have 00:11:55.670 --> 00:11:55.680 align:start position:0% we have 00:11:55.680 --> 00:11:57.590 align:start position:0% we have um an<00:11:56.040> array<00:11:56.279> of<00:11:56.399> constraints<00:11:56.820> this<00:11:57.360> is<00:11:57.420> what 00:11:57.590 --> 00:11:57.600 align:start position:0% um an array of constraints this is what 00:11:57.600 --> 00:11:59.990 align:start position:0% um an array of constraints this is what I<00:11:57.779> showed<00:11:58.019> before<00:11:58.200> like<00:11:59.160> when<00:11:59.399> you<00:11:59.579> see<00:11:59.760> the 00:11:59.990 --> 00:12:00.000 align:start position:0% I showed before like when you see the 00:12:00.000 --> 00:12:02.509 align:start position:0% I showed before like when you see the require<00:12:00.240> it<00:12:01.200> says<00:12:01.380> require<00:12:01.620> a<00:12:01.980> class<00:12:02.220> or<00:12:02.399> equal 00:12:02.509 --> 00:12:02.519 align:start position:0% require it says require a class or equal 00:12:02.519 --> 00:12:04.910 align:start position:0% require it says require a class or equal 10<00:12:02.760> we<00:12:03.360> go<00:12:03.600> into<00:12:03.720> that<00:12:04.019> Branch<00:12:04.320> so<00:12:04.680> we<00:12:04.800> keep 00:12:04.910 --> 00:12:04.920 align:start position:0% 10 we go into that Branch so we keep 00:12:04.920 --> 00:12:06.470 align:start position:0% 10 we go into that Branch so we keep that<00:12:05.100> constraint<00:12:05.459> because<00:12:05.760> that<00:12:06.000> thing<00:12:06.180> needs 00:12:06.470 --> 00:12:06.480 align:start position:0% that constraint because that thing needs 00:12:06.480 --> 00:12:09.650 align:start position:0% that constraint because that thing needs to<00:12:06.540> be<00:12:06.720> true<00:12:07.320> for<00:12:07.560> the<00:12:07.680> rest<00:12:07.800> of<00:12:07.920> the<00:12:08.040> execution 00:12:09.650 --> 00:12:09.660 align:start position:0% to be true for the rest of the execution 00:12:09.660 --> 00:12:14.090 align:start position:0% to be true for the rest of the execution um<00:12:09.740> and<00:12:10.740> this<00:12:11.220> counter<00:12:11.579> variable<00:12:11.940> is<00:12:12.360> just<00:12:12.540> a 00:12:14.090 --> 00:12:14.100 align:start position:0% um and this counter variable is just a 00:12:14.100 --> 00:12:16.730 align:start position:0% um and this counter variable is just a um<00:12:14.220> accounted<00:12:14.940> to<00:12:15.300> help<00:12:15.779> create<00:12:16.260> new 00:12:16.730 --> 00:12:16.740 align:start position:0% um accounted to help create new 00:12:16.740 --> 00:12:18.290 align:start position:0% um accounted to help create new variables<00:12:17.100> so<00:12:17.220> when<00:12:17.399> we<00:12:17.760> were<00:12:17.880> creating<00:12:18.120> new 00:12:18.290 --> 00:12:18.300 align:start position:0% variables so when we were creating new 00:12:18.300 --> 00:12:19.850 align:start position:0% variables so when we were creating new variables<00:12:18.540> for<00:12:18.660> the<00:12:18.779> Expressions<00:12:19.079> X<00:12:19.320> Y<00:12:19.560> and<00:12:19.740> Z 00:12:19.850 --> 00:12:19.860 align:start position:0% variables for the Expressions X Y and Z 00:12:19.860 --> 00:12:20.870 align:start position:0% variables for the Expressions X Y and Z and<00:12:20.040> so<00:12:20.160> on<00:12:20.279> here<00:12:20.459> we're<00:12:20.640> going<00:12:20.760> to<00:12:20.820> be 00:12:20.870 --> 00:12:20.880 align:start position:0% and so on here we're going to be 00:12:20.880 --> 00:12:22.370 align:start position:0% and so on here we're going to be expression<00:12:21.360> one<00:12:21.600> expression<00:12:21.899> two<00:12:22.019> expression 00:12:22.370 --> 00:12:22.380 align:start position:0% expression one expression two expression 00:12:22.380 --> 00:12:24.170 align:start position:0% expression one expression two expression three<00:12:22.560> and<00:12:22.740> so<00:12:22.860> on<00:12:22.980> and<00:12:23.519> they<00:12:23.820> need<00:12:23.940> to<00:12:24.060> be 00:12:24.170 --> 00:12:24.180 align:start position:0% three and so on and they need to be 00:12:24.180 --> 00:12:25.490 align:start position:0% three and so on and they need to be different<00:12:24.420> in<00:12:24.720> the<00:12:24.839> branches<00:12:25.200> that<00:12:25.380> we 00:12:25.490 --> 00:12:25.500 align:start position:0% different in the branches that we 00:12:25.500 --> 00:12:27.170 align:start position:0% different in the branches that we execute 00:12:27.170 --> 00:12:27.180 align:start position:0% execute 00:12:27.180 --> 00:12:29.690 align:start position:0% execute so<00:12:27.540> that's<00:12:27.779> it<00:12:27.959> we<00:12:28.320> have<00:12:28.440> the<00:12:28.560> context 00:12:29.690 --> 00:12:29.700 align:start position:0% so that's it we have the context 00:12:29.700 --> 00:12:31.790 align:start position:0% so that's it we have the context um<00:12:29.820> ignore<00:12:30.120> the<00:12:30.240> rest<00:12:30.420> for<00:12:30.660> now<00:12:30.779> let's<00:12:31.440> jump 00:12:31.790 --> 00:12:31.800 align:start position:0% um ignore the rest for now let's jump 00:12:31.800 --> 00:12:34.190 align:start position:0% um ignore the rest for now let's jump right<00:12:32.100> into<00:12:32.339> the 00:12:34.190 --> 00:12:34.200 align:start position:0% right into the 00:12:34.200 --> 00:12:36.230 align:start position:0% right into the execution<00:12:34.920> engine<00:12:35.220> so<00:12:35.519> we<00:12:35.760> have<00:12:35.880> this 00:12:36.230 --> 00:12:36.240 align:start position:0% execution engine so we have this 00:12:36.240 --> 00:12:38.509 align:start position:0% execution engine so we have this recursive<00:12:36.660> function<00:12:36.959> called<00:12:37.079> run<00:12:37.320> from 00:12:38.509 --> 00:12:38.519 align:start position:0% recursive function called run from 00:12:38.519 --> 00:12:41.269 align:start position:0% recursive function called run from which<00:12:39.060> takes<00:12:39.300> our<00:12:39.540> context<00:12:39.959> so<00:12:40.800> here<00:12:40.980> you<00:12:41.100> see 00:12:41.269 --> 00:12:41.279 align:start position:0% which takes our context so here you see 00:12:41.279 --> 00:12:44.269 align:start position:0% which takes our context so here you see it's<00:12:41.399> basically<00:12:41.820> gonna<00:12:42.060> Traverse<00:12:42.980> all<00:12:43.980> the<00:12:44.160> up 00:12:44.269 --> 00:12:44.279 align:start position:0% it's basically gonna Traverse all the up 00:12:44.279 --> 00:12:47.690 align:start position:0% it's basically gonna Traverse all the up codes<00:12:44.540> select<00:12:45.540> the<00:12:45.660> opcode 00:12:47.690 --> 00:12:47.700 align:start position:0% codes select the opcode 00:12:47.700 --> 00:12:49.970 align:start position:0% codes select the opcode this<00:12:48.600> is<00:12:48.779> just<00:12:48.959> a<00:12:49.139> check 00:12:49.970 --> 00:12:49.980 align:start position:0% this is just a check 00:12:49.980 --> 00:12:52.850 align:start position:0% this is just a check um<00:12:50.040> that<00:12:50.459> we<00:12:50.820> just<00:12:51.240> exit<00:12:51.660> early<00:12:51.839> in<00:12:52.079> Loops<00:12:52.440> we 00:12:52.850 --> 00:12:52.860 align:start position:0% um that we just exit early in Loops we 00:12:52.860 --> 00:12:54.530 align:start position:0% um that we just exit early in Loops we it<00:12:53.040> becomes<00:12:53.399> an<00:12:53.519> under<00:12:53.639> proximation<00:12:54.180> but<00:12:54.420> we 00:12:54.530 --> 00:12:54.540 align:start position:0% it becomes an under proximation but we 00:12:54.540 --> 00:12:56.690 align:start position:0% it becomes an under proximation but we don't<00:12:54.660> want<00:12:54.779> to<00:12:54.899> do<00:12:54.959> loops 00:12:56.690 --> 00:12:56.700 align:start position:0% don't want to do loops 00:12:56.700 --> 00:12:58.550 align:start position:0% don't want to do loops we<00:12:57.060> extend<00:12:57.360> the<00:12:57.540> path 00:12:58.550 --> 00:12:58.560 align:start position:0% we extend the path 00:12:58.560 --> 00:13:01.069 align:start position:0% we extend the path with<00:12:59.220> the<00:12:59.339> Disney<00:12:59.459> opcode 00:13:01.069 --> 00:13:01.079 align:start position:0% with the Disney opcode 00:13:01.079 --> 00:13:04.250 align:start position:0% with the Disney opcode and<00:13:02.040> here<00:13:02.220> is<00:13:02.339> the<00:13:02.519> part<00:13:02.700> that<00:13:03.120> the<00:13:03.899> first<00:13:04.019> part 00:13:04.250 --> 00:13:04.260 align:start position:0% and here is the part that the first part 00:13:04.260 --> 00:13:05.629 align:start position:0% and here is the part that the first part of<00:13:04.440> the<00:13:04.680> what<00:13:04.920> I<00:13:05.100> mentioned<00:13:05.279> with<00:13:05.459> The 00:13:05.629 --> 00:13:05.639 align:start position:0% of the what I mentioned with The 00:13:05.639 --> 00:13:08.030 align:start position:0% of the what I mentioned with The Interpreter<00:13:06.120> we<00:13:06.899> need<00:13:07.019> to<00:13:07.079> care<00:13:07.260> about<00:13:07.440> Stack 00:13:08.030 --> 00:13:08.040 align:start position:0% Interpreter we need to care about Stack 00:13:08.040 --> 00:13:09.110 align:start position:0% Interpreter we need to care about Stack Up<00:13:08.220> codes 00:13:09.110 --> 00:13:09.120 align:start position:0% Up codes 00:13:09.120 --> 00:13:11.389 align:start position:0% Up codes because<00:13:09.600> they're<00:13:10.260> going<00:13:10.500> to<00:13:10.620> add<00:13:10.860> some 00:13:11.389 --> 00:13:11.399 align:start position:0% because they're going to add some 00:13:11.399 --> 00:13:13.490 align:start position:0% because they're going to add some numbers<00:13:11.639> and<00:13:12.480> a<00:13:12.839> bunch<00:13:13.019> of<00:13:13.139> different<00:13:13.260> things 00:13:13.490 --> 00:13:13.500 align:start position:0% numbers and a bunch of different things 00:13:13.500 --> 00:13:16.610 align:start position:0% numbers and a bunch of different things jump<00:13:13.860> locations<00:13:14.519> jump<00:13:15.060> destinations<00:13:15.540> that<00:13:16.440> we 00:13:16.610 --> 00:13:16.620 align:start position:0% jump locations jump destinations that we 00:13:16.620 --> 00:13:18.170 align:start position:0% jump locations jump destinations that we will<00:13:16.800> need<00:13:17.040> when<00:13:17.339> when<00:13:17.639> building<00:13:17.940> our 00:13:18.170 --> 00:13:18.180 align:start position:0% will need when when building our 00:13:18.180 --> 00:13:19.250 align:start position:0% will need when when building our constraints 00:13:19.250 --> 00:13:19.260 align:start position:0% constraints 00:13:19.260 --> 00:13:21.350 align:start position:0% constraints so<00:13:19.740> this<00:13:19.920> just<00:13:20.100> does<00:13:20.279> the<00:13:20.459> usual 00:13:21.350 --> 00:13:21.360 align:start position:0% so this just does the usual 00:13:21.360 --> 00:13:22.850 align:start position:0% so this just does the usual um stack<00:13:21.660> handling<00:13:22.019> so<00:13:22.200> if<00:13:22.260> it's<00:13:22.440> a<00:13:22.620> swap 00:13:22.850 --> 00:13:22.860 align:start position:0% um stack handling so if it's a swap 00:13:22.860 --> 00:13:24.710 align:start position:0% um stack handling so if it's a swap you're<00:13:23.040> gonna<00:13:23.160> go<00:13:23.639> into<00:13:23.760> the<00:13:23.940> stack<00:13:24.240> and<00:13:24.420> swap 00:13:24.710 --> 00:13:24.720 align:start position:0% you're gonna go into the stack and swap 00:13:24.720 --> 00:13:26.389 align:start position:0% you're gonna go into the stack and swap the<00:13:24.839> numbers<00:13:24.959> if<00:13:25.260> it's<00:13:25.380> a<00:13:25.920> dupe<00:13:26.160> you're<00:13:26.279> going 00:13:26.389 --> 00:13:26.399 align:start position:0% the numbers if it's a dupe you're going 00:13:26.399 --> 00:13:27.530 align:start position:0% the numbers if it's a dupe you're going to<00:13:26.459> duplicate<00:13:26.880> whatever<00:13:27.060> it<00:13:27.300> needs<00:13:27.480> to 00:13:27.530 --> 00:13:27.540 align:start position:0% to duplicate whatever it needs to 00:13:27.540 --> 00:13:29.090 align:start position:0% to duplicate whatever it needs to duplicate<00:13:27.899> it<00:13:28.019> if<00:13:28.320> it's<00:13:28.500> a<00:13:28.620> push<00:13:28.740> you<00:13:28.920> just 00:13:29.090 --> 00:13:29.100 align:start position:0% duplicate it if it's a push you just 00:13:29.100 --> 00:13:30.710 align:start position:0% duplicate it if it's a push you just push<00:13:29.220> that<00:13:29.399> number<00:13:29.519> into<00:13:29.760> the<00:13:29.940> stack 00:13:30.710 --> 00:13:30.720 align:start position:0% push that number into the stack 00:13:30.720 --> 00:13:35.150 align:start position:0% push that number into the stack here<00:13:31.200> the<00:13:31.500> only<00:13:31.560> thing<00:13:31.800> we<00:13:32.040> do<00:13:32.220> is<00:13:32.820> apply 00:13:35.150 --> 00:13:35.160 align:start position:0% here the only thing we do is apply 00:13:35.160 --> 00:13:37.730 align:start position:0% here the only thing we do is apply a<00:13:35.760> function<00:13:36.300> on 00:13:37.730 --> 00:13:37.740 align:start position:0% a function on 00:13:37.740 --> 00:13:39.889 align:start position:0% a function on the<00:13:38.459> stack<00:13:38.700> arguments<00:13:39.240> which<00:13:39.420> is<00:13:39.600> so<00:13:39.839> for 00:13:39.889 --> 00:13:39.899 align:start position:0% the stack arguments which is so for 00:13:39.899 --> 00:13:41.810 align:start position:0% the stack arguments which is so for example<00:13:40.139> if<00:13:40.260> you<00:13:40.380> have<00:13:40.500> an<00:13:40.620> ad<00:13:40.800> we're<00:13:41.579> not 00:13:41.810 --> 00:13:41.820 align:start position:0% example if you have an ad we're not 00:13:41.820 --> 00:13:43.730 align:start position:0% example if you have an ad we're not going<00:13:42.000> to<00:13:42.180> encode<00:13:42.660> the<00:13:42.839> ad<00:13:42.959> precisely<00:13:43.500> here 00:13:43.730 --> 00:13:43.740 align:start position:0% going to encode the ad precisely here 00:13:43.740 --> 00:13:45.769 align:start position:0% going to encode the ad precisely here but<00:13:44.399> we<00:13:44.579> do<00:13:44.700> need<00:13:44.940> to<00:13:45.060> consume<00:13:45.420> the<00:13:45.600> stack 00:13:45.769 --> 00:13:45.779 align:start position:0% but we do need to consume the stack 00:13:45.779 --> 00:13:49.670 align:start position:0% but we do need to consume the stack slots<00:13:46.139> and<00:13:46.740> put<00:13:46.980> a<00:13:47.100> new<00:13:47.339> return<00:13:48.380> value<00:13:49.380> there 00:13:49.670 --> 00:13:49.680 align:start position:0% slots and put a new return value there 00:13:49.680 --> 00:13:52.310 align:start position:0% slots and put a new return value there right<00:13:49.980> so<00:13:50.639> this<00:13:50.940> basically<00:13:51.360> just<00:13:51.779> uses<00:13:52.079> these 00:13:52.310 --> 00:13:52.320 align:start position:0% right so this basically just uses these 00:13:52.320 --> 00:13:53.810 align:start position:0% right so this basically just uses these handlers<00:13:52.620> we<00:13:52.860> have<00:13:52.980> internally<00:13:53.339> it's<00:13:53.519> like<00:13:53.700> a 00:13:53.810 --> 00:13:53.820 align:start position:0% handlers we have internally it's like a 00:13:53.820 --> 00:13:55.610 align:start position:0% handlers we have internally it's like a bunch<00:13:53.880> of<00:13:54.000> function<00:13:54.180> pointers 00:13:55.610 --> 00:13:55.620 align:start position:0% bunch of function pointers 00:13:55.620 --> 00:13:56.389 align:start position:0% bunch of function pointers um 00:13:56.389 --> 00:13:56.399 align:start position:0% um 00:13:56.399 --> 00:13:59.030 align:start position:0% um to<00:13:56.940> if<00:13:57.240> you<00:13:57.360> have<00:13:57.480> an<00:13:57.600> ad<00:13:57.839> so<00:13:58.380> this<00:13:58.500> is<00:13:58.680> generic 00:13:59.030 --> 00:13:59.040 align:start position:0% to if you have an ad so this is generic 00:13:59.040 --> 00:14:00.949 align:start position:0% to if you have an ad so this is generic for<00:13:59.279> like<00:13:59.459> all<00:13:59.880> the<00:14:00.060> all<00:14:00.300> the<00:14:00.480> up<00:14:00.600> girls<00:14:00.779> we 00:14:00.949 --> 00:14:00.959 align:start position:0% for like all the all the up girls we 00:14:00.959 --> 00:14:03.350 align:start position:0% for like all the all the up girls we don't<00:14:01.079> care<00:14:01.200> about<00:14:01.320> it<00:14:01.980> takes<00:14:02.100> the<00:14:02.579> number<00:14:03.180> of 00:14:03.350 --> 00:14:03.360 align:start position:0% don't care about it takes the number of 00:14:03.360 --> 00:14:06.110 align:start position:0% don't care about it takes the number of arguments<00:14:03.839> this<00:14:04.139> op<00:14:04.380> code<00:14:04.560> takes<00:14:04.920> pops<00:14:05.880> all<00:14:06.000> of 00:14:06.110 --> 00:14:06.120 align:start position:0% arguments this op code takes pops all of 00:14:06.120 --> 00:14:09.050 align:start position:0% arguments this op code takes pops all of them<00:14:06.240> from<00:14:06.420> the<00:14:06.540> stack<00:14:06.860> creates<00:14:07.860> a<00:14:08.279> new<00:14:08.519> work 00:14:09.050 --> 00:14:09.060 align:start position:0% them from the stack creates a new work 00:14:09.060 --> 00:14:11.150 align:start position:0% them from the stack creates a new work what<00:14:09.360> we<00:14:09.540> call<00:14:09.660> symbolic<00:14:10.139> variable<00:14:10.440> so<00:14:10.800> like<00:14:10.980> a 00:14:11.150 --> 00:14:11.160 align:start position:0% what we call symbolic variable so like a 00:14:11.160 --> 00:14:13.490 align:start position:0% what we call symbolic variable so like a new<00:14:11.220> expression<00:14:11.820> 13<00:14:12.180> or<00:14:12.600> whatever<00:14:12.720> here<00:14:13.019> and 00:14:13.490 --> 00:14:13.500 align:start position:0% new expression 13 or whatever here and 00:14:13.500 --> 00:14:16.310 align:start position:0% new expression 13 or whatever here and puts<00:14:13.800> that<00:14:13.920> expression<00:14:14.339> on<00:14:14.579> the<00:14:14.700> stack 00:14:16.310 --> 00:14:16.320 align:start position:0% puts that expression on the stack 00:14:16.320 --> 00:14:18.110 align:start position:0% puts that expression on the stack um<00:14:16.440> and<00:14:16.740> we<00:14:16.920> don't<00:14:17.040> really<00:14:17.220> have<00:14:17.579> we<00:14:17.940> don't 00:14:18.110 --> 00:14:18.120 align:start position:0% um and we don't really have we don't 00:14:18.120 --> 00:14:19.670 align:start position:0% um and we don't really have we don't really<00:14:18.240> care<00:14:18.480> what<00:14:18.660> it<00:14:18.839> looks 00:14:19.670 --> 00:14:19.680 align:start position:0% really care what it looks 00:14:19.680 --> 00:14:21.170 align:start position:0% really care what it looks um<00:14:19.800> what<00:14:20.339> it<00:14:20.399> looks<00:14:20.639> like<00:14:20.700> right<00:14:20.820> now<00:14:20.940> we<00:14:21.060> don't 00:14:21.170 --> 00:14:21.180 align:start position:0% um what it looks like right now we don't 00:14:21.180 --> 00:14:22.490 align:start position:0% um what it looks like right now we don't really<00:14:21.360> care<00:14:21.540> what<00:14:21.660> kind<00:14:21.839> of<00:14:21.899> constraints<00:14:22.320> we 00:14:22.490 --> 00:14:22.500 align:start position:0% really care what kind of constraints we 00:14:22.500 --> 00:14:24.230 align:start position:0% really care what kind of constraints we have<00:14:22.680> over<00:14:22.860> it 00:14:24.230 --> 00:14:24.240 align:start position:0% have over it 00:14:24.240 --> 00:14:26.930 align:start position:0% have over it and<00:14:24.959> and<00:14:25.260> here's<00:14:25.620> a<00:14:25.800> part<00:14:25.920> of<00:14:26.100> the<00:14:26.399> that<00:14:26.700> we 00:14:26.930 --> 00:14:26.940 align:start position:0% and and here's a part of the that we 00:14:26.940 --> 00:14:28.370 align:start position:0% and and here's a part of the that we actually<00:14:27.060> care<00:14:27.360> about<00:14:27.480> the<00:14:27.779> where<00:14:27.959> we<00:14:28.139> do<00:14:28.260> the 00:14:28.370 --> 00:14:28.380 align:start position:0% actually care about the where we do the 00:14:28.380 --> 00:14:32.150 align:start position:0% actually care about the where we do the check<00:14:28.700> so<00:14:29.700> if<00:14:30.420> we<00:14:30.540> have<00:14:30.660> a<00:14:30.779> jump<00:14:30.959> every<00:14:31.800> time<00:14:32.040> we 00:14:32.150 --> 00:14:32.160 align:start position:0% check so if we have a jump every time we 00:14:32.160 --> 00:14:33.650 align:start position:0% check so if we have a jump every time we see<00:14:32.339> a<00:14:32.459> conditional<00:14:32.820> jump 00:14:33.650 --> 00:14:33.660 align:start position:0% see a conditional jump 00:14:33.660 --> 00:14:36.110 align:start position:0% see a conditional jump we<00:14:34.260> take<00:14:34.500> the<00:14:34.740> the<00:14:34.860> argument<00:14:35.399> of<00:14:35.579> that<00:14:35.700> jump<00:14:35.880> we 00:14:36.110 --> 00:14:36.120 align:start position:0% we take the the argument of that jump we 00:14:36.120 --> 00:14:37.850 align:start position:0% we take the the argument of that jump we take<00:14:36.240> the<00:14:36.360> condition<00:14:36.540> that<00:14:37.260> makes<00:14:37.440> it<00:14:37.620> jump 00:14:37.850 --> 00:14:37.860 align:start position:0% take the condition that makes it jump 00:14:37.860 --> 00:14:40.150 align:start position:0% take the condition that makes it jump and<00:14:38.519> we<00:14:38.639> ask<00:14:38.820> the<00:14:39.000> solver<00:14:39.300> is<00:14:39.540> it<00:14:39.660> possible 00:14:40.150 --> 00:14:40.160 align:start position:0% and we ask the solver is it possible 00:14:40.160 --> 00:14:42.730 align:start position:0% and we ask the solver is it possible that<00:14:41.160> we<00:14:41.459> can't<00:14:41.579> jump<00:14:41.820> to<00:14:42.060> that<00:14:42.240> location 00:14:42.730 --> 00:14:42.740 align:start position:0% that we can't jump to that location 00:14:42.740 --> 00:14:45.530 align:start position:0% that we can't jump to that location because<00:14:43.740> this<00:14:44.040> is<00:14:44.160> before<00:14:44.459> we<00:14:44.760> had<00:14:44.940> this<00:14:45.240> this 00:14:45.530 --> 00:14:45.540 align:start position:0% because this is before we had this this 00:14:45.540 --> 00:14:47.930 align:start position:0% because this is before we had this this required<00:14:46.079> an<00:14:46.260> if<00:14:46.440> right<00:14:46.800> so<00:14:47.040> we<00:14:47.399> have<00:14:47.579> require 00:14:47.930 --> 00:14:47.940 align:start position:0% required an if right so we have require 00:14:47.940 --> 00:14:50.449 align:start position:0% required an if right so we have require access<00:14:48.540> or<00:14:49.380> uh 00:14:50.449 --> 00:14:50.459 align:start position:0% access or uh 00:14:50.459 --> 00:14:54.290 align:start position:0% access or uh X<00:14:51.000> Plus<00:14:51.320> then<00:14:52.320> or<00:14:52.500> equal<00:14:52.620> to<00:14:52.860> 10.<00:14:53.399> so<00:14:54.000> we<00:14:54.120> have 00:14:54.290 --> 00:14:54.300 align:start position:0% X Plus then or equal to 10. so we have 00:14:54.300 --> 00:14:56.210 align:start position:0% X Plus then or equal to 10. so we have that<00:14:54.480> saved<00:14:54.899> X<00:14:55.139> must<00:14:55.440> be<00:14:55.620> less<00:14:55.740> or<00:14:55.920> equal<00:14:56.040> to 00:14:56.210 --> 00:14:56.220 align:start position:0% that saved X must be less or equal to 00:14:56.220 --> 00:14:59.090 align:start position:0% that saved X must be less or equal to 10.<00:14:56.579> and<00:14:56.820> then<00:14:56.940> we<00:14:57.060> see<00:14:57.240> if<00:14:57.660> x<00:14:58.199> greater<00:14:58.620> than<00:14:58.740> 50 00:14:59.090 --> 00:14:59.100 align:start position:0% 10. and then we see if x greater than 50 00:14:59.100 --> 00:15:01.129 align:start position:0% 10. and then we see if x greater than 50 and<00:14:59.880> then<00:15:00.000> we<00:15:00.120> ask<00:15:00.300> is<00:15:00.420> it<00:15:00.660> possible<00:15:00.899> though 00:15:01.129 --> 00:15:01.139 align:start position:0% and then we ask is it possible though 00:15:01.139 --> 00:15:03.889 align:start position:0% and then we ask is it possible though that<00:15:01.380> is<00:15:01.560> that<00:15:01.800> X<00:15:01.980> is<00:15:02.160> greater<00:15:02.459> than<00:15:02.519> 50.<00:15:03.240> so<00:15:03.720> at 00:15:03.889 --> 00:15:03.899 align:start position:0% that is that X is greater than 50. so at 00:15:03.899 --> 00:15:06.110 align:start position:0% that is that X is greater than 50. so at this<00:15:04.079> point<00:15:04.199> that's<00:15:04.500> when<00:15:04.740> we 00:15:06.110 --> 00:15:06.120 align:start position:0% this point that's when we 00:15:06.120 --> 00:15:06.650 align:start position:0% this point that's when we um 00:15:06.650 --> 00:15:06.660 align:start position:0% um 00:15:06.660 --> 00:15:08.990 align:start position:0% um we<00:15:07.260> have<00:15:07.500> all<00:15:07.800> the<00:15:08.040> math<00:15:08.220> things<00:15:08.459> encoded 00:15:08.990 --> 00:15:09.000 align:start position:0% we have all the math things encoded 00:15:09.000 --> 00:15:10.790 align:start position:0% we have all the math things encoded already<00:15:09.180> in<00:15:09.600> here 00:15:10.790 --> 00:15:10.800 align:start position:0% already in here 00:15:10.800 --> 00:15:13.189 align:start position:0% already in here as<00:15:11.279> you'll<00:15:11.459> see<00:15:11.639> this<00:15:12.060> make<00:15:12.420> symbol<00:15:12.839> this<00:15:13.139> is 00:15:13.189 --> 00:15:13.199 align:start position:0% as you'll see this make symbol this is 00:15:13.199 --> 00:15:15.230 align:start position:0% as you'll see this make symbol this is like<00:15:13.440> internal<00:15:14.160> helpers<00:15:14.519> not<00:15:14.760> important 00:15:15.230 --> 00:15:15.240 align:start position:0% like internal helpers not important 00:15:15.240 --> 00:15:16.310 align:start position:0% like internal helpers not important right<00:15:15.360> now 00:15:16.310 --> 00:15:16.320 align:start position:0% right now 00:15:16.320 --> 00:15:19.009 align:start position:0% right now so<00:15:16.740> here's<00:15:17.040> where<00:15:17.220> we 00:15:19.009 --> 00:15:19.019 align:start position:0% so here's where we 00:15:19.019 --> 00:15:21.470 align:start position:0% so here's where we do<00:15:19.560> the<00:15:19.920> check 00:15:21.470 --> 00:15:21.480 align:start position:0% do the check 00:15:21.480 --> 00:15:23.030 align:start position:0% do the check so<00:15:21.779> we<00:15:21.839> check<00:15:22.019> if<00:15:22.199> the<00:15:22.320> op<00:15:22.440> code<00:15:22.620> is<00:15:22.740> relational 00:15:23.030 --> 00:15:23.040 align:start position:0% so we check if the op code is relational 00:15:23.040 --> 00:15:25.610 align:start position:0% so we check if the op code is relational so<00:15:23.459> if<00:15:23.639> you<00:15:23.760> have<00:15:23.880> a<00:15:24.060> less<00:15:24.240> than<00:15:24.420> or<00:15:25.199> greater 00:15:25.610 --> 00:15:25.620 align:start position:0% so if you have a less than or greater 00:15:25.620 --> 00:15:28.550 align:start position:0% so if you have a less than or greater than<00:15:25.680> or<00:15:26.160> if<00:15:26.220> it's<00:15:26.339> an<00:15:26.519> e0<00:15:26.820> because<00:15:27.240> if<00:15:28.199> if<00:15:28.380> we 00:15:28.550 --> 00:15:28.560 align:start position:0% than or if it's an e0 because if if we 00:15:28.560 --> 00:15:30.470 align:start position:0% than or if it's an e0 because if if we needed<00:15:28.800> a<00:15:28.920> greater<00:15:29.160> or<00:15:29.279> equal<00:15:29.459> we<00:15:30.180> don't<00:15:30.300> have 00:15:30.470 --> 00:15:30.480 align:start position:0% needed a greater or equal we don't have 00:15:30.480 --> 00:15:32.030 align:start position:0% needed a greater or equal we don't have greater<00:15:30.779> or<00:15:30.899> equal<00:15:31.019> in<00:15:31.199> the<00:15:31.320> VM<00:15:31.560> so<00:15:31.680> we<00:15:31.860> need<00:15:31.920> to 00:15:32.030 --> 00:15:32.040 align:start position:0% greater or equal in the VM so we need to 00:15:32.040 --> 00:15:33.829 align:start position:0% greater or equal in the VM so we need to do<00:15:32.160> is<00:15:32.399> zero 00:15:33.829 --> 00:15:33.839 align:start position:0% do is zero 00:15:33.839 --> 00:15:37.550 align:start position:0% do is zero um<00:15:33.899> less<00:15:34.620> than<00:15:34.800> right<00:15:35.339> so<00:15:35.699> and<00:15:36.300> similarly<00:15:36.720> for 00:15:37.550 --> 00:15:37.560 align:start position:0% um less than right so and similarly for 00:15:37.560 --> 00:15:39.889 align:start position:0% um less than right so and similarly for um less<00:15:38.160> than<00:15:38.339> or<00:15:38.519> equal<00:15:38.699> so<00:15:39.300> if<00:15:39.480> it's<00:15:39.600> one<00:15:39.779> of 00:15:39.889 --> 00:15:39.899 align:start position:0% um less than or equal so if it's one of 00:15:39.899 --> 00:15:41.990 align:start position:0% um less than or equal so if it's one of these<00:15:40.139> we<00:15:40.740> basically<00:15:41.100> take<00:15:41.459> the<00:15:41.820> the 00:15:41.990 --> 00:15:42.000 align:start position:0% these we basically take the the 00:15:42.000 --> 00:15:44.750 align:start position:0% these we basically take the the condition<00:15:42.300> which<00:15:43.019> is<00:15:43.139> here<00:15:43.320> we<00:15:44.160> transform<00:15:44.579> it 00:15:44.750 --> 00:15:44.760 align:start position:0% condition which is here we transform it 00:15:44.760 --> 00:15:47.509 align:start position:0% condition which is here we transform it into<00:15:44.940> an<00:15:45.440> DL<00:15:46.440> expression<00:15:46.860> difference<00:15:47.040> logic 00:15:47.509 --> 00:15:47.519 align:start position:0% into an DL expression difference logic 00:15:47.519 --> 00:15:49.670 align:start position:0% into an DL expression difference logic expression 00:15:49.670 --> 00:15:49.680 align:start position:0% expression 00:15:49.680 --> 00:15:52.069 align:start position:0% expression um<00:15:49.800> and<00:15:50.160> basically<00:15:50.519> call<00:15:50.820> this<00:15:51.060> over<00:15:51.240> so<00:15:51.839> we 00:15:52.069 --> 00:15:52.079 align:start position:0% um and basically call this over so we 00:15:52.079 --> 00:15:54.050 align:start position:0% um and basically call this over so we have<00:15:52.199> this<00:15:52.380> check<00:15:52.560> here<00:15:53.040> which<00:15:53.459> will<00:15:53.639> take<00:15:53.820> all 00:15:54.050 --> 00:15:54.060 align:start position:0% have this check here which will take all 00:15:54.060 --> 00:15:55.970 align:start position:0% have this check here which will take all the<00:15:54.240> constraints<00:15:54.660> and<00:15:55.440> we'll<00:15:55.560> call<00:15:55.800> this 00:15:55.970 --> 00:15:55.980 align:start position:0% the constraints and we'll call this 00:15:55.980 --> 00:15:58.670 align:start position:0% the constraints and we'll call this little<00:15:56.160> DL<00:15:56.459> server<00:15:56.820> that<00:15:56.940> I<00:15:57.060> mentioned 00:15:58.670 --> 00:15:58.680 align:start position:0% little DL server that I mentioned 00:15:58.680 --> 00:15:59.449 align:start position:0% little DL server that I mentioned um 00:15:59.449 --> 00:15:59.459 align:start position:0% um 00:15:59.459 --> 00:16:02.569 align:start position:0% um which<00:16:00.120> and<00:16:00.600> this<00:16:00.839> is<00:16:00.959> the<00:16:01.260> check 00:16:02.569 --> 00:16:02.579 align:start position:0% which and this is the check 00:16:02.579 --> 00:16:04.670 align:start position:0% which and this is the check we<00:16:02.940> call<00:16:03.120> this<00:16:03.240> over<00:16:03.480> and<00:16:03.959> if<00:16:04.079> the<00:16:04.199> server<00:16:04.440> says 00:16:04.670 --> 00:16:04.680 align:start position:0% we call this over and if the server says 00:16:04.680 --> 00:16:06.829 align:start position:0% we call this over and if the server says unsut<00:16:05.220> then<00:16:05.940> we<00:16:06.180> say<00:16:06.300> this<00:16:06.480> branch<00:16:06.720> is 00:16:06.829 --> 00:16:06.839 align:start position:0% unsut then we say this branch is 00:16:06.839 --> 00:16:10.670 align:start position:0% unsut then we say this branch is unreachable<00:16:07.260> why<00:16:07.860> unsat<00:16:08.480> because<00:16:09.500> if<00:16:10.500> the 00:16:10.670 --> 00:16:10.680 align:start position:0% unreachable why unsat because if the 00:16:10.680 --> 00:16:12.170 align:start position:0% unreachable why unsat because if the branches<00:16:11.100> if<00:16:11.339> the<00:16:11.459> branch<00:16:11.639> conditions<00:16:12.120> are 00:16:12.170 --> 00:16:12.180 align:start position:0% branches if the branch conditions are 00:16:12.180 --> 00:16:13.790 align:start position:0% branches if the branch conditions are unsatisfiable 00:16:13.790 --> 00:16:13.800 align:start position:0% unsatisfiable 00:16:13.800 --> 00:16:17.569 align:start position:0% unsatisfiable together<00:16:14.600> it<00:16:15.600> means<00:16:16.019> that 00:16:17.569 --> 00:16:17.579 align:start position:0% together it means that 00:16:17.579 --> 00:16:19.850 align:start position:0% together it means that um<00:16:18.120> the<00:16:18.600> silver<00:16:18.779> will<00:16:19.019> say<00:16:19.199> unsatisfiable 00:16:19.850 --> 00:16:19.860 align:start position:0% um the silver will say unsatisfiable 00:16:19.860 --> 00:16:22.009 align:start position:0% um the silver will say unsatisfiable right<00:16:20.339> and<00:16:21.000> this<00:16:21.180> means<00:16:21.420> that<00:16:21.540> that<00:16:21.660> part<00:16:21.839> is 00:16:22.009 --> 00:16:22.019 align:start position:0% right and this means that that part is 00:16:22.019 --> 00:16:23.810 align:start position:0% right and this means that that part is not<00:16:22.139> reachable<00:16:22.500> because<00:16:23.279> there's<00:16:23.579> something 00:16:23.810 --> 00:16:23.820 align:start position:0% not reachable because there's something 00:16:23.820 --> 00:16:25.610 align:start position:0% not reachable because there's something in<00:16:24.300> in<00:16:24.480> the<00:16:24.660> middle<00:16:24.779> that<00:16:25.019> is<00:16:25.079> not<00:16:25.260> allowing 00:16:25.610 --> 00:16:25.620 align:start position:0% in in the middle that is not allowing 00:16:25.620 --> 00:16:28.310 align:start position:0% in in the middle that is not allowing that<00:16:26.100> will<00:16:26.339> not<00:16:26.519> make<00:16:26.940> the<00:16:27.180> code<00:16:27.540> the<00:16:27.839> code<00:16:27.959> the 00:16:28.310 --> 00:16:28.320 align:start position:0% that will not make the code the code the 00:16:28.320 --> 00:16:29.750 align:start position:0% that will not make the code the code the code<00:16:28.440> path<00:16:28.800> is<00:16:29.100> basically<00:16:29.339> going<00:16:29.519> to<00:16:29.699> be 00:16:29.750 --> 00:16:29.760 align:start position:0% code path is basically going to be 00:16:29.760 --> 00:16:32.090 align:start position:0% code path is basically going to be inconsistent 00:16:32.090 --> 00:16:32.100 align:start position:0% inconsistent 00:16:32.100 --> 00:16:34.730 align:start position:0% inconsistent um<00:16:32.160> and<00:16:32.760> what<00:16:33.000> the<00:16:33.120> silver<00:16:33.240> looks<00:16:33.720> like<00:16:33.779> is 00:16:34.730 --> 00:16:34.740 align:start position:0% um and what the silver looks like is 00:16:34.740 --> 00:16:37.189 align:start position:0% um and what the silver looks like is yeah<00:16:35.279> this<00:16:35.699> is<00:16:35.820> the<00:16:36.060> entire<00:16:36.300> silver 00:16:37.189 --> 00:16:37.199 align:start position:0% yeah this is the entire silver 00:16:37.199 --> 00:16:39.710 align:start position:0% yeah this is the entire silver so<00:16:37.560> you<00:16:37.680> take<00:16:37.800> the<00:16:37.980> constraints<00:16:38.399> so<00:16:39.360> here<00:16:39.540> you 00:16:39.710 --> 00:16:39.720 align:start position:0% so you take the constraints so here you 00:16:39.720 --> 00:16:41.810 align:start position:0% so you take the constraints so here you just<00:16:39.839> build<00:16:40.019> the<00:16:40.199> graph<00:16:40.980> so<00:16:41.279> this<00:16:41.399> is<00:16:41.459> built<00:16:41.759> in 00:16:41.810 --> 00:16:41.820 align:start position:0% just build the graph so this is built in 00:16:41.820 --> 00:16:43.670 align:start position:0% just build the graph so this is built in the<00:16:41.940> graph<00:16:42.180> here<00:16:42.959> you<00:16:43.079> just<00:16:43.139> need<00:16:43.259> to<00:16:43.380> know<00:16:43.500> how 00:16:43.670 --> 00:16:43.680 align:start position:0% the graph here you just need to know how 00:16:43.680 --> 00:16:45.769 align:start position:0% the graph here you just need to know how many<00:16:43.740> variables<00:16:44.100> you<00:16:44.279> have 00:16:45.769 --> 00:16:45.779 align:start position:0% many variables you have 00:16:45.779 --> 00:16:48.170 align:start position:0% many variables you have um<00:16:45.899> this<00:16:46.500> is<00:16:46.620> still<00:16:46.800> building<00:16:46.980> the<00:16:47.279> graph 00:16:48.170 --> 00:16:48.180 align:start position:0% um this is still building the graph 00:16:48.180 --> 00:16:50.329 align:start position:0% um this is still building the graph and<00:16:48.540> then<00:16:48.660> Here<00:16:48.899> We<00:16:49.079> Run<00:16:49.259> The<00:16:49.500> this<00:16:49.800> single<00:16:50.160> the 00:16:50.329 --> 00:16:50.339 align:start position:0% and then Here We Run The this single the 00:16:50.339 --> 00:16:52.490 align:start position:0% and then Here We Run The this single the single<00:16:50.699> source<00:16:50.940> for<00:16:51.060> this<00:16:51.240> path<00:16:51.360> algorithm 00:16:52.490 --> 00:16:52.500 align:start position:0% single source for this path algorithm 00:16:52.500 --> 00:16:53.930 align:start position:0% single source for this path algorithm which<00:16:52.860> is<00:16:52.920> the<00:16:53.040> first<00:16:53.160> part<00:16:53.399> of<00:16:53.519> the<00:16:53.639> solver 00:16:53.930 --> 00:16:53.940 align:start position:0% which is the first part of the solver 00:16:53.940 --> 00:16:56.210 align:start position:0% which is the first part of the solver which<00:16:54.660> is<00:16:54.839> basically<00:16:55.620> yeah<00:16:55.800> it's<00:16:55.980> a<00:16:56.160> very 00:16:56.210 --> 00:16:56.220 align:start position:0% which is basically yeah it's a very 00:16:56.220 --> 00:16:58.430 align:start position:0% which is basically yeah it's a very basic<00:16:56.519> graph<00:16:56.699> algorithm<00:16:57.060> then<00:16:58.019> we<00:16:58.199> did<00:16:58.320> a 00:16:58.430 --> 00:16:58.440 align:start position:0% basic graph algorithm then we did a 00:16:58.440 --> 00:17:00.710 align:start position:0% basic graph algorithm then we did a negative<00:16:58.680> cycle<00:16:58.980> detection<00:16:59.420> and<00:17:00.420> that's 00:17:00.710 --> 00:17:00.720 align:start position:0% negative cycle detection and that's 00:17:00.720 --> 00:17:03.530 align:start position:0% negative cycle detection and that's really<00:17:00.959> all<00:17:01.320> the<00:17:01.620> silver<00:17:01.860> does<00:17:02.220> this<00:17:03.000> is<00:17:03.120> and 00:17:03.530 --> 00:17:03.540 align:start position:0% really all the silver does this is and 00:17:03.540 --> 00:17:07.069 align:start position:0% really all the silver does this is and 20<00:17:03.779> lines<00:17:04.140> of<00:17:04.319> code<00:17:04.439> it's<00:17:04.919> really<00:17:05.160> simple<00:17:05.339> and 00:17:07.069 --> 00:17:07.079 align:start position:0% 20 lines of code it's really simple and 00:17:07.079 --> 00:17:07.669 align:start position:0% 20 lines of code it's really simple and um 00:17:07.669 --> 00:17:07.679 align:start position:0% um 00:17:07.679 --> 00:17:09.409 align:start position:0% um yeah<00:17:08.160> it's<00:17:08.339> a<00:17:08.579> it's<00:17:08.760> a<00:17:08.819> logic<00:17:09.059> that<00:17:09.179> I<00:17:09.299> really 00:17:09.409 --> 00:17:09.419 align:start position:0% yeah it's a it's a logic that I really 00:17:09.419 --> 00:17:11.449 align:start position:0% yeah it's a it's a logic that I really like<00:17:09.600> because<00:17:09.900> it<00:17:10.559> can<00:17:10.679> do<00:17:10.919> a<00:17:11.040> lot<00:17:11.160> of<00:17:11.280> things 00:17:11.449 --> 00:17:11.459 align:start position:0% like because it can do a lot of things 00:17:11.459 --> 00:17:14.510 align:start position:0% like because it can do a lot of things while<00:17:12.360> being<00:17:12.660> very<00:17:12.900> very<00:17:13.140> simple 00:17:14.510 --> 00:17:14.520 align:start position:0% while being very very simple 00:17:14.520 --> 00:17:16.429 align:start position:0% while being very very simple um<00:17:14.579> the<00:17:14.819> last<00:17:14.880> thing<00:17:15.059> that<00:17:15.179> I<00:17:15.360> want<00:17:15.419> to<00:17:15.600> show<00:17:15.720> is 00:17:16.429 --> 00:17:16.439 align:start position:0% um the last thing that I want to show is 00:17:16.439 --> 00:17:19.730 align:start position:0% um the last thing that I want to show is how<00:17:17.040> do<00:17:17.160> you<00:17:17.280> use<00:17:17.400> this<00:17:18.179> so 00:17:19.730 --> 00:17:19.740 align:start position:0% how do you use this so 00:17:19.740 --> 00:17:21.590 align:start position:0% how do you use this so here<00:17:20.220> I<00:17:20.400> have<00:17:20.520> this<00:17:20.760> contract<00:17:21.059> unreachable 00:17:21.590 --> 00:17:21.600 align:start position:0% here I have this contract unreachable 00:17:21.600 --> 00:17:23.210 align:start position:0% here I have this contract unreachable that<00:17:22.079> has<00:17:22.199> a<00:17:22.319> bunch<00:17:22.439> of<00:17:22.559> functions<00:17:22.860> and<00:17:23.040> that's 00:17:23.210 --> 00:17:23.220 align:start position:0% that has a bunch of functions and that's 00:17:23.220 --> 00:17:24.829 align:start position:0% that has a bunch of functions and that's like<00:17:23.459> some<00:17:23.640> unreachable<00:17:24.059> branches<00:17:24.600> in<00:17:24.720> each 00:17:24.829 --> 00:17:24.839 align:start position:0% like some unreachable branches in each 00:17:24.839 --> 00:17:26.210 align:start position:0% like some unreachable branches in each of<00:17:24.959> these<00:17:25.140> functions 00:17:26.210 --> 00:17:26.220 align:start position:0% of these functions 00:17:26.220 --> 00:17:29.090 align:start position:0% of these functions all<00:17:26.640> we<00:17:26.760> need<00:17:26.880> to<00:17:27.000> do<00:17:27.120> to<00:17:27.419> test<00:17:27.660> that<00:17:27.959> is<00:17:28.740> really 00:17:29.090 --> 00:17:29.100 align:start position:0% all we need to do to test that is really 00:17:29.100 --> 00:17:31.490 align:start position:0% all we need to do to test that is really just<00:17:29.400> this<00:17:29.700> we<00:17:30.419> call<00:17:30.600> the<00:17:30.720> Sim<00:17:30.900> run<00:17:31.140> function 00:17:31.490 --> 00:17:31.500 align:start position:0% just this we call the Sim run function 00:17:31.500 --> 00:17:33.049 align:start position:0% just this we call the Sim run function from<00:17:31.799> the<00:17:31.980> library<00:17:32.100> from<00:17:32.460> the<00:17:32.640> symbolic 00:17:33.049 --> 00:17:33.059 align:start position:0% from the library from the symbolic 00:17:33.059 --> 00:17:35.390 align:start position:0% from the library from the symbolic symbolic<00:17:33.780> execution<00:17:34.320> Library 00:17:35.390 --> 00:17:35.400 align:start position:0% symbolic execution Library 00:17:35.400 --> 00:17:38.270 align:start position:0% symbolic execution Library with<00:17:36.179> the<00:17:36.419> runtime<00:17:36.720> code 00:17:38.270 --> 00:17:38.280 align:start position:0% with the runtime code 00:17:38.280 --> 00:17:40.850 align:start position:0% with the runtime code from<00:17:38.700> the<00:17:38.820> contract<00:17:39.120> that's<00:17:39.360> really<00:17:39.539> all<00:17:39.860> and 00:17:40.850 --> 00:17:40.860 align:start position:0% from the contract that's really all and 00:17:40.860 --> 00:17:42.770 align:start position:0% from the contract that's really all and here's<00:17:41.340> a<00:17:41.460> simpler<00:17:41.940> thing<00:17:42.059> just<00:17:42.539> like 00:17:42.770 --> 00:17:42.780 align:start position:0% here's a simpler thing just like 00:17:42.780 --> 00:17:45.169 align:start position:0% here's a simpler thing just like manually 00:17:45.169 --> 00:17:45.179 align:start position:0% manually 00:17:45.179 --> 00:17:46.610 align:start position:0% manually um just<00:17:45.419> a<00:17:45.600> simple<00:17:45.720> test 00:17:46.610 --> 00:17:46.620 align:start position:0% um just a simple test 00:17:46.620 --> 00:17:48.409 align:start position:0% um just a simple test with<00:17:47.220> somebody<00:17:47.460> care<00:17:47.760> that<00:17:47.940> I<00:17:48.059> know<00:17:48.120> what<00:17:48.240> it 00:17:48.409 --> 00:17:48.419 align:start position:0% with somebody care that I know what it 00:17:48.419 --> 00:17:52.850 align:start position:0% with somebody care that I know what it does<00:17:48.980> and<00:17:49.980> if<00:17:50.160> you<00:17:50.340> run<00:17:50.700> this 00:17:52.850 --> 00:17:52.860 align:start position:0% does and if you run this 00:17:52.860 --> 00:17:56.090 align:start position:0% does and if you run this yeah<00:17:53.340> so<00:17:53.640> here<00:17:53.820> you'll<00:17:54.000> see<00:17:54.179> that 00:17:56.090 --> 00:17:56.100 align:start position:0% yeah so here you'll see that 00:17:56.100 --> 00:17:57.590 align:start position:0% yeah so here you'll see that um this<00:17:56.400> is<00:17:56.460> the<00:17:56.580> complicated<00:17:56.940> case<00:17:57.240> with<00:17:57.419> all 00:17:57.590 --> 00:17:57.600 align:start position:0% um this is the complicated case with all 00:17:57.600 --> 00:17:59.930 align:start position:0% um this is the complicated case with all the<00:17:57.720> solidity<00:17:58.080> high<00:17:58.260> level<00:17:58.440> functions<00:17:58.980> and 00:17:59.930 --> 00:17:59.940 align:start position:0% the solidity high level functions and 00:17:59.940 --> 00:18:01.909 align:start position:0% the solidity high level functions and it's<00:18:00.600> not<00:18:00.840> the<00:18:00.960> best<00:18:01.080> way<00:18:01.380> to<00:18:01.559> report<00:18:01.679> the 00:18:01.909 --> 00:18:01.919 align:start position:0% it's not the best way to report the 00:18:01.919 --> 00:18:04.430 align:start position:0% it's not the best way to report the things<00:18:02.100> but<00:18:02.280> it<00:18:02.460> reports<00:18:02.880> it<00:18:03.419> emits<00:18:03.900> an<00:18:04.260> event 00:18:04.430 --> 00:18:04.440 align:start position:0% things but it reports it emits an event 00:18:04.440 --> 00:18:06.650 align:start position:0% things but it reports it emits an event that<00:18:05.160> says<00:18:05.400> unreachable<00:18:05.880> Branch<00:18:06.240> with<00:18:06.539> the 00:18:06.650 --> 00:18:06.660 align:start position:0% that says unreachable Branch with the 00:18:06.660 --> 00:18:10.010 align:start position:0% that says unreachable Branch with the pc255<00:18:07.559> this<00:18:08.400> tiny<00:18:08.820> example<00:18:09.120> so<00:18:09.299> it's<00:18:09.539> this<00:18:09.840> is 00:18:10.010 --> 00:18:10.020 align:start position:0% pc255 this tiny example so it's this is 00:18:10.020 --> 00:18:11.390 align:start position:0% pc255 this tiny example so it's this is the<00:18:10.200> same<00:18:10.320> as<00:18:10.440> I<00:18:10.559> showed<00:18:10.740> in<00:18:10.860> solidity<00:18:11.220> just 00:18:11.390 --> 00:18:11.400 align:start position:0% the same as I showed in solidity just 00:18:11.400 --> 00:18:14.750 align:start position:0% the same as I showed in solidity just like<00:18:11.580> in<00:18:11.760> written<00:18:12.120> quickly<00:18:12.480> in<00:18:12.539> yule<00:18:13.559> and<00:18:14.400> this 00:18:14.750 --> 00:18:14.760 align:start position:0% like in written quickly in yule and this 00:18:14.760 --> 00:18:16.610 align:start position:0% like in written quickly in yule and this is<00:18:14.880> the<00:18:15.059> bytecode 00:18:16.610 --> 00:18:16.620 align:start position:0% is the bytecode 00:18:16.620 --> 00:18:18.950 align:start position:0% is the bytecode that<00:18:17.100> it<00:18:17.280> generates 00:18:18.950 --> 00:18:18.960 align:start position:0% that it generates 00:18:18.960 --> 00:18:23.090 align:start position:0% that it generates um well<00:18:19.140> that<00:18:19.679> I<00:18:19.799> wrote<00:18:19.980> manually<00:18:20.340> and 00:18:23.090 --> 00:18:23.100 align:start position:0% um well that I wrote manually and 00:18:23.100 --> 00:18:23.990 align:start position:0% um well that I wrote manually and um 00:18:23.990 --> 00:18:24.000 align:start position:0% um 00:18:24.000 --> 00:18:26.090 align:start position:0% um so<00:18:24.539> we<00:18:24.720> can<00:18:24.900> quickly 00:18:26.090 --> 00:18:26.100 align:start position:0% so we can quickly 00:18:26.100 --> 00:18:28.909 align:start position:0% so we can quickly compute<00:18:27.000> This<00:18:27.299> Together<00:18:27.620> keeping<00:18:28.620> track<00:18:28.740> of 00:18:28.909 --> 00:18:28.919 align:start position:0% compute This Together keeping track of 00:18:28.919 --> 00:18:31.490 align:start position:0% compute This Together keeping track of the<00:18:29.039> stack 00:18:31.490 --> 00:18:31.500 align:start position:0% 00:18:31.500 --> 00:18:33.350 align:start position:0% and<00:18:31.860> then<00:18:31.919> you<00:18:32.039> see<00:18:32.220> what<00:18:32.460> it 00:18:33.350 --> 00:18:33.360 align:start position:0% and then you see what it 00:18:33.360 --> 00:18:35.630 align:start position:0% and then you see what it what<00:18:33.720> it<00:18:33.840> actually<00:18:33.960> does<00:18:34.200> in<00:18:34.380> execution<00:18:34.919> so 00:18:35.630 --> 00:18:35.640 align:start position:0% what it actually does in execution so 00:18:35.640 --> 00:18:37.250 align:start position:0% what it actually does in execution so push<00:18:36.059> zero 00:18:37.250 --> 00:18:37.260 align:start position:0% push zero 00:18:37.260 --> 00:18:38.750 align:start position:0% push zero we're<00:18:37.559> going<00:18:37.679> to<00:18:37.740> push<00:18:37.860> zero<00:18:38.340> then<00:18:38.520> we<00:18:38.640> just 00:18:38.750 --> 00:18:38.760 align:start position:0% we're going to push zero then we just 00:18:38.760 --> 00:18:40.190 align:start position:0% we're going to push zero then we just called<00:18:38.940> it<00:18:39.059> a<00:18:39.179> load<00:18:39.360> of<00:18:39.480> zero<00:18:39.780> it's<00:18:39.900> going<00:18:40.080> to 00:18:40.190 --> 00:18:40.200 align:start position:0% called it a load of zero it's going to 00:18:40.200 --> 00:18:42.230 align:start position:0% called it a load of zero it's going to give<00:18:40.320> us<00:18:40.500> some<00:18:40.740> X 00:18:42.230 --> 00:18:42.240 align:start position:0% give us some X 00:18:42.240 --> 00:18:46.730 align:start position:0% give us some X then<00:18:42.840> we<00:18:43.260> push<00:18:43.620> 10. 00:18:46.730 --> 00:18:46.740 align:start position:0% 00:18:46.740 --> 00:18:49.850 align:start position:0% we<00:18:47.160> duplicate<00:18:47.700> the<00:18:47.940> X 00:18:49.850 --> 00:18:49.860 align:start position:0% we duplicate the X 00:18:49.860 --> 00:18:53.450 align:start position:0% we duplicate the X we<00:18:50.460> do<00:18:50.700> less<00:18:50.940> than<00:18:51.179> so<00:18:51.660> this<00:18:51.960> is<00:18:52.080> going<00:18:52.260> to<00:18:52.380> turn 00:18:53.450 --> 00:18:53.460 align:start position:0% we do less than so this is going to turn 00:18:53.460 --> 00:18:55.730 align:start position:0% we do less than so this is going to turn into<00:18:54.000> this 00:18:55.730 --> 00:18:55.740 align:start position:0% into this 00:18:55.740 --> 00:18:58.070 align:start position:0% into this this<00:18:56.100> is<00:18:56.280> the<00:18:56.460> stack<00:18:56.640> by<00:18:57.000> the<00:18:57.179> way 00:18:58.070 --> 00:18:58.080 align:start position:0% this is the stack by the way 00:18:58.080 --> 00:19:00.650 align:start position:0% this is the stack by the way and<00:18:58.620> the<00:18:58.860> top<00:18:58.980> is<00:18:59.220> the<00:18:59.340> higher<00:18:59.640> position<00:18:59.820> so 00:19:00.650 --> 00:19:00.660 align:start position:0% and the top is the higher position so 00:19:00.660 --> 00:19:02.870 align:start position:0% and the top is the higher position so now<00:19:00.780> we<00:19:00.960> push<00:19:01.140> tag<00:19:01.559> 0b 00:19:02.870 --> 00:19:02.880 align:start position:0% now we push tag 0b 00:19:02.880 --> 00:19:05.210 align:start position:0% now we push tag 0b and<00:19:03.480> we<00:19:03.720> do<00:19:03.900> the<00:19:04.080> like<00:19:04.440> a<00:19:04.620> conditional<00:19:04.980> jump 00:19:05.210 --> 00:19:05.220 align:start position:0% and we do the like a conditional jump 00:19:05.220 --> 00:19:07.250 align:start position:0% and we do the like a conditional jump where<00:19:05.700> the<00:19:05.940> false<00:19:06.240> Branch<00:19:06.480> stops<00:19:06.840> so<00:19:07.020> we<00:19:07.140> don't 00:19:07.250 --> 00:19:07.260 align:start position:0% where the false Branch stops so we don't 00:19:07.260 --> 00:19:09.289 align:start position:0% where the false Branch stops so we don't care<00:19:07.320> about<00:19:07.440> the<00:19:07.620> first<00:19:07.740> Branch<00:19:08.100> all<00:19:08.700> we<00:19:08.880> do<00:19:09.059> is 00:19:09.289 --> 00:19:09.299 align:start position:0% care about the first Branch all we do is 00:19:09.299 --> 00:19:11.330 align:start position:0% care about the first Branch all we do is just<00:19:09.480> so<00:19:09.660> you're<00:19:09.840> gonna<00:19:09.960> pop 00:19:11.330 --> 00:19:11.340 align:start position:0% just so you're gonna pop 00:19:11.340 --> 00:19:12.590 align:start position:0% just so you're gonna pop um<00:19:11.400> we're<00:19:11.760> gonna<00:19:11.880> pop<00:19:12.059> this<00:19:12.240> first<00:19:12.419> two 00:19:12.590 --> 00:19:12.600 align:start position:0% um we're gonna pop this first two 00:19:12.600 --> 00:19:15.710 align:start position:0% um we're gonna pop this first two arguments<00:19:12.960> right<00:19:13.260> because<00:19:13.500> of<00:19:13.799> the<00:19:14.580> jump<00:19:15.120> but 00:19:15.710 --> 00:19:15.720 align:start position:0% arguments right because of the jump but 00:19:15.720 --> 00:19:18.529 align:start position:0% arguments right because of the jump but because<00:19:15.900> we<00:19:16.200> go<00:19:16.440> into<00:19:16.860> a<00:19:17.220> branch<00:19:17.539> this 00:19:18.529 --> 00:19:18.539 align:start position:0% because we go into a branch this 00:19:18.539 --> 00:19:20.690 align:start position:0% because we go into a branch this condition<00:19:18.720> must<00:19:19.080> be<00:19:19.260> true<00:19:19.500> for<00:19:20.280> the<00:19:20.400> rest<00:19:20.580> of 00:19:20.690 --> 00:19:20.700 align:start position:0% condition must be true for the rest of 00:19:20.700 --> 00:19:22.370 align:start position:0% condition must be true for the rest of execution<00:19:21.120> right 00:19:22.370 --> 00:19:22.380 align:start position:0% execution right 00:19:22.380 --> 00:19:24.049 align:start position:0% execution right set<00:19:22.860> of<00:19:23.039> constraints 00:19:24.049 --> 00:19:24.059 align:start position:0% set of constraints 00:19:24.059 --> 00:19:26.150 align:start position:0% set of constraints so<00:19:24.419> we<00:19:24.539> keep<00:19:24.660> going<00:19:24.840> in<00:19:25.140> tag<00:19:25.380> one<00:19:25.559> jump<00:19:25.799> Dash 00:19:26.150 --> 00:19:26.160 align:start position:0% so we keep going in tag one jump Dash 00:19:26.160 --> 00:19:28.010 align:start position:0% so we keep going in tag one jump Dash dup<00:19:26.400> we<00:19:26.580> duplicate<00:19:26.940> X<00:19:27.120> again 00:19:28.010 --> 00:19:28.020 align:start position:0% dup we duplicate X again 00:19:28.020 --> 00:19:31.450 align:start position:0% dup we duplicate X again we<00:19:28.440> push<00:19:28.620> 50. 00:19:31.450 --> 00:19:31.460 align:start position:0% 00:19:31.460 --> 00:19:35.870 align:start position:0% we<00:19:32.460> do<00:19:32.640> an<00:19:32.820> LT<00:19:33.179> now 00:19:35.870 --> 00:19:35.880 align:start position:0% 00:19:35.880 --> 00:19:38.750 align:start position:0% and<00:19:36.600> which<00:19:36.960> consumes<00:19:37.620> the<00:19:38.039> X<00:19:38.160> and<00:19:38.520> this 00:19:38.750 --> 00:19:38.760 align:start position:0% and which consumes the X and this 00:19:38.760 --> 00:19:40.370 align:start position:0% and which consumes the X and this becomes<00:19:39.059> top<00:19:39.240> of<00:19:39.419> the<00:19:39.480> stack<00:19:39.660> just<00:19:39.900> a<00:19:40.020> symbolic 00:19:40.370 --> 00:19:40.380 align:start position:0% becomes top of the stack just a symbolic 00:19:40.380 --> 00:19:43.490 align:start position:0% becomes top of the stack just a symbolic expression<00:19:40.799> like<00:19:41.400> Y<00:19:41.820> equals<00:19:42.419> X<00:19:42.840> length<00:19:43.260> less 00:19:43.490 --> 00:19:43.500 align:start position:0% expression like Y equals X length less 00:19:43.500 --> 00:19:45.850 align:start position:0% expression like Y equals X length less than<00:19:43.740> fifth<00:19:44.700> less<00:19:44.820> than<00:19:45.000> x 00:19:45.850 --> 00:19:45.860 align:start position:0% than fifth less than x 00:19:45.860 --> 00:19:50.210 align:start position:0% than fifth less than x we<00:19:46.860> push<00:19:47.039> 14<00:19:47.400> and<00:19:47.700> then<00:19:47.820> we<00:19:48.000> jump<00:19:48.440> 2<00:19:49.440> and<00:19:50.100> then 00:19:50.210 --> 00:19:50.220 align:start position:0% we push 14 and then we jump 2 and then 00:19:50.220 --> 00:19:52.730 align:start position:0% we push 14 and then we jump 2 and then at<00:19:50.460> this<00:19:50.580> point<00:19:50.820> when<00:19:51.240> we<00:19:51.419> see<00:19:51.539> the<00:19:51.720> jump<00:19:51.960> we're 00:19:52.730 --> 00:19:52.740 align:start position:0% at this point when we see the jump we're 00:19:52.740 --> 00:19:54.169 align:start position:0% at this point when we see the jump we're going<00:19:52.860> to<00:19:52.980> ask<00:19:53.039> the<00:19:53.220> solver<00:19:53.520> is<00:19:53.760> it<00:19:53.880> possible 00:19:54.169 --> 00:19:54.179 align:start position:0% going to ask the solver is it possible 00:19:54.179 --> 00:19:57.830 align:start position:0% going to ask the solver is it possible that<00:19:54.720> this<00:19:55.020> new<00:19:55.200> condition<00:19:55.380> 50<00:19:56.220> as<00:19:56.520> an<00:19:56.640> X<00:19:56.840> is 00:19:57.830 --> 00:19:57.840 align:start position:0% that this new condition 50 as an X is 00:19:57.840 --> 00:20:00.350 align:start position:0% that this new condition 50 as an X is consistent<00:19:58.740> with<00:19:59.039> what<00:19:59.220> we<00:19:59.340> already<00:19:59.460> have<00:19:59.820> X 00:20:00.350 --> 00:20:00.360 align:start position:0% consistent with what we already have X 00:20:00.360 --> 00:20:01.610 align:start position:0% consistent with what we already have X less<00:20:00.660> than<00:20:00.780> 10<00:20:00.960> and<00:20:01.080> it's<00:20:01.200> always<00:20:01.320> going<00:20:01.559> to 00:20:01.610 --> 00:20:01.620 align:start position:0% less than 10 and it's always going to 00:20:01.620 --> 00:20:03.770 align:start position:0% less than 10 and it's always going to say<00:20:01.679> that's<00:20:01.919> not<00:20:02.160> possible<00:20:02.580> and<00:20:03.360> at<00:20:03.660> this 00:20:03.770 --> 00:20:03.780 align:start position:0% say that's not possible and at this 00:20:03.780 --> 00:20:06.650 align:start position:0% say that's not possible and at this point<00:20:04.080> here<00:20:04.640> precisely<00:20:05.640> at<00:20:05.940> this<00:20:06.120> jump<00:20:06.360> I 00:20:06.650 --> 00:20:06.660 align:start position:0% point here precisely at this jump I 00:20:06.660 --> 00:20:09.710 align:start position:0% point here precisely at this jump I that's<00:20:07.559> where<00:20:08.100> we<00:20:08.460> basically<00:20:09.120> stop<00:20:09.360> and<00:20:09.539> say 00:20:09.710 --> 00:20:09.720 align:start position:0% that's where we basically stop and say 00:20:09.720 --> 00:20:12.590 align:start position:0% that's where we basically stop and say this<00:20:09.960> Branch<00:20:10.260> here<00:20:10.440> is<00:20:10.620> is<00:20:11.000> the<00:20:12.000> true<00:20:12.179> Branch 00:20:12.590 --> 00:20:12.600 align:start position:0% this Branch here is is the true Branch 00:20:12.600 --> 00:20:16.150 align:start position:0% this Branch here is is the true Branch like<00:20:13.320> where<00:20:13.620> you're<00:20:13.799> jumping<00:20:14.160> next<00:20:14.400> is<00:20:15.360> um 00:20:16.150 --> 00:20:16.160 align:start position:0% like where you're jumping next is um 00:20:16.160 --> 00:20:18.289 align:start position:0% like where you're jumping next is um unsatisfiable<00:20:17.160> so<00:20:17.460> you<00:20:17.760> can<00:20:17.820> actually<00:20:18.000> remove 00:20:18.289 --> 00:20:18.299 align:start position:0% unsatisfiable so you can actually remove 00:20:18.299 --> 00:20:20.990 align:start position:0% unsatisfiable so you can actually remove that<00:20:18.600> entire<00:20:18.900> Branch<00:20:19.260> right 00:20:20.990 --> 00:20:21.000 align:start position:0% that entire Branch right 00:20:21.000 --> 00:20:22.970 align:start position:0% that entire Branch right but<00:20:21.480> yeah<00:20:21.600> so 00:20:22.970 --> 00:20:22.980 align:start position:0% but yeah so 00:20:22.980 --> 00:20:24.470 align:start position:0% but yeah so there's<00:20:23.520> a<00:20:23.640> lot<00:20:23.700> of<00:20:23.820> code<00:20:24.059> behind<00:20:24.360> that 00:20:24.470 --> 00:20:24.480 align:start position:0% there's a lot of code behind that 00:20:24.480 --> 00:20:25.789 align:start position:0% there's a lot of code behind that there's<00:20:24.600> a<00:20:24.780> lot<00:20:24.840> of<00:20:24.960> helpers<00:20:25.260> the<00:20:25.679> main 00:20:25.789 --> 00:20:25.799 align:start position:0% there's a lot of helpers the main 00:20:25.799 --> 00:20:27.230 align:start position:0% there's a lot of helpers the main intuition<00:20:26.160> was<00:20:26.400> basically<00:20:26.700> this<00:20:26.880> algorithm 00:20:27.230 --> 00:20:27.240 align:start position:0% intuition was basically this algorithm 00:20:27.240 --> 00:20:28.789 align:start position:0% intuition was basically this algorithm of<00:20:27.480> just<00:20:27.660> like<00:20:27.780> run<00:20:27.960> an<00:20:28.140> interpreter<00:20:28.500> caring 00:20:28.789 --> 00:20:28.799 align:start position:0% of just like run an interpreter caring 00:20:28.799 --> 00:20:29.870 align:start position:0% of just like run an interpreter caring about<00:20:28.860> if<00:20:29.100> you're<00:20:29.160> killed<00:20:29.520> not<00:20:29.580> caring<00:20:29.820> about 00:20:29.870 --> 00:20:29.880 align:start position:0% about if you're killed not caring about 00:20:29.880 --> 00:20:31.130 align:start position:0% about if you're killed not caring about other<00:20:30.120> up<00:20:30.360> codes 00:20:31.130 --> 00:20:31.140 align:start position:0% other up codes 00:20:31.140 --> 00:20:37.070 align:start position:0% other up codes and<00:20:31.860> yeah<00:20:32.840> I'm<00:20:33.840> happy<00:20:34.200> to<00:20:34.440> take<00:20:35.340> questions 00:20:37.070 --> 00:20:37.080 align:start position:0% and yeah I'm happy to take questions 00:20:37.080 --> 00:20:39.049 align:start position:0% and yeah I'm happy to take questions uh<00:20:37.500> super<00:20:37.620> cool<00:20:37.799> talk<00:20:38.039> this<00:20:38.340> is<00:20:38.460> wild<00:20:38.760> you<00:20:39.000> can 00:20:39.049 --> 00:20:39.059 align:start position:0% uh super cool talk this is wild you can 00:20:39.059 --> 00:20:40.490 align:start position:0% uh super cool talk this is wild you can do<00:20:39.179> this<00:20:39.240> in<00:20:39.360> solidity<00:20:39.780> I'm<00:20:40.200> wondering<00:20:40.380> about 00:20:40.490 --> 00:20:40.500 align:start position:0% do this in solidity I'm wondering about 00:20:40.500 --> 00:20:41.930 align:start position:0% do this in solidity I'm wondering about overflow<00:20:41.039> though<00:20:41.280> uh<00:20:41.640> because<00:20:41.760> your 00:20:41.930 --> 00:20:41.940 align:start position:0% overflow though uh because your 00:20:41.940 --> 00:20:42.950 align:start position:0% overflow though uh because your researching<00:20:42.299> at<00:20:42.419> the<00:20:42.480> beginning<00:20:42.539> was<00:20:42.780> that 00:20:42.950 --> 00:20:42.960 align:start position:0% researching at the beginning was that 00:20:42.960 --> 00:20:44.390 align:start position:0% researching at the beginning was that that<00:20:43.140> one<00:20:43.440> example<00:20:43.860> you<00:20:43.980> showed<00:20:44.220> was 00:20:44.390 --> 00:20:44.400 align:start position:0% that one example you showed was 00:20:44.400 --> 00:20:46.490 align:start position:0% that one example you showed was impossible<00:20:44.820> but<00:20:45.059> it<00:20:45.179> is<00:20:45.299> very<00:20:45.480> possible<00:20:45.840> in 00:20:46.490 --> 00:20:46.500 align:start position:0% impossible but it is very possible in 00:20:46.500 --> 00:20:48.110 align:start position:0% impossible but it is very possible in the<00:20:46.620> presence<00:20:46.799> of<00:20:46.919> overflow<00:20:47.460> no<00:20:47.760> that<00:20:48.000> one 00:20:48.110 --> 00:20:48.120 align:start position:0% the presence of overflow no that one 00:20:48.120 --> 00:20:49.730 align:start position:0% the presence of overflow no that one wasn't<00:20:48.360> because<00:20:48.660> you<00:20:48.900> need<00:20:49.080> the<00:20:49.260> answer<00:20:49.380> to<00:20:49.620> be 00:20:49.730 --> 00:20:49.740 align:start position:0% wasn't because you need the answer to be 00:20:49.740 --> 00:20:51.890 align:start position:0% wasn't because you need the answer to be minus<00:20:50.039> one-third<00:20:50.460> so<00:20:51.299> it's<00:20:51.480> not<00:20:51.600> going<00:20:51.720> to<00:20:51.840> be 00:20:51.890 --> 00:20:51.900 align:start position:0% minus one-third so it's not going to be 00:20:51.900 --> 00:20:52.970 align:start position:0% minus one-third so it's not going to be possible 00:20:52.970 --> 00:20:52.980 align:start position:0% possible 00:20:52.980 --> 00:20:54.350 align:start position:0% possible um<00:20:53.100> okay<00:20:53.400> sure<00:20:53.580> yeah<00:20:53.760> but<00:20:53.940> it<00:20:54.120> doesn't<00:20:54.240> look 00:20:54.350 --> 00:20:54.360 align:start position:0% um okay sure yeah but it doesn't look 00:20:54.360 --> 00:20:56.029 align:start position:0% um okay sure yeah but it doesn't look like<00:20:54.480> you<00:20:54.660> handle<00:20:54.900> overflow<00:20:55.320> anymore<00:20:55.620> yeah<00:20:55.860> no 00:20:56.029 --> 00:20:56.039 align:start position:0% like you handle overflow anymore yeah no 00:20:56.039 --> 00:20:58.250 align:start position:0% like you handle overflow anymore yeah no right<00:20:56.280> yeah<00:20:56.460> exactly<00:20:56.820> so<00:20:57.120> that<00:20:57.840> means<00:20:58.080> that 00:20:58.250 --> 00:20:58.260 align:start position:0% right yeah exactly so that means that 00:20:58.260 --> 00:21:01.070 align:start position:0% right yeah exactly so that means that your<00:20:58.440> results<00:20:58.620> are<00:20:59.100> not<00:21:00.000> correct<00:21:00.720> yeah 00:21:01.070 --> 00:21:01.080 align:start position:0% your results are not correct yeah 00:21:01.080 --> 00:21:02.210 align:start position:0% your results are not correct yeah exactly<00:21:01.380> there's<00:21:01.559> a<00:21:01.740> bunch<00:21:01.799> of<00:21:01.919> soundness 00:21:02.210 --> 00:21:02.220 align:start position:0% exactly there's a bunch of soundness 00:21:02.220 --> 00:21:04.130 align:start position:0% exactly there's a bunch of soundness stuff<00:21:02.400> you<00:21:02.580> have<00:21:02.700> to<00:21:02.820> add<00:21:02.880> to<00:21:03.059> this<00:21:03.179> okay<00:21:03.539> all 00:21:04.130 --> 00:21:04.140 align:start position:0% stuff you have to add to this okay all 00:21:04.140 --> 00:21:07.250 align:start position:0% stuff you have to add to this okay all right<00:21:04.320> thank<00:21:04.620> you<00:21:04.880> sorry<00:21:05.880> I<00:21:06.179> didn't<00:21:06.299> see<00:21:06.780> but 00:21:07.250 --> 00:21:07.260 align:start position:0% right thank you sorry I didn't see but 00:21:07.260 --> 00:21:10.730 align:start position:0% right thank you sorry I didn't see but is<00:21:07.860> this<00:21:08.039> code<00:21:08.280> somewhere<00:21:08.880> available<00:21:09.539> to<00:21:10.020> uh 00:21:10.730 --> 00:21:10.740 align:start position:0% is this code somewhere available to uh 00:21:10.740 --> 00:21:14.330 align:start position:0% is this code somewhere available to uh yeah<00:21:10.980> this<00:21:11.340> repo<00:21:11.820> github.com 00:21:14.330 --> 00:21:14.340 align:start position:0% yeah this repo github.com 00:21:14.340 --> 00:21:16.789 align:start position:0% yeah this repo github.com um<00:21:14.400> that<00:21:14.640> thing<00:21:14.820> and<00:21:15.419> there's<00:21:16.260> probably<00:21:16.440> bugs 00:21:16.789 --> 00:21:16.799 align:start position:0% um that thing and there's probably bugs 00:21:16.799 --> 00:21:19.549 align:start position:0% um that thing and there's probably bugs in<00:21:16.919> there<00:21:17.039> though<00:21:17.220> so<00:21:17.520> feel<00:21:18.240> free<00:21:18.419> to<00:21:18.600> fix<00:21:18.960> them 00:21:19.549 --> 00:21:19.559 align:start position:0% in there though so feel free to fix them 00:21:19.559 --> 00:21:22.010 align:start position:0% in there though so feel free to fix them um<00:21:19.620> so<00:21:20.039> since<00:21:20.340> you<00:21:20.580> wrote<00:21:20.880> this<00:21:21.059> in<00:21:21.240> solidity<00:21:21.720> I 00:21:22.010 --> 00:21:22.020 align:start position:0% um so since you wrote this in solidity I 00:21:22.020 --> 00:21:23.450 align:start position:0% um so since you wrote this in solidity I do<00:21:22.200> you<00:21:22.380> have<00:21:22.440> any<00:21:22.559> thoughts<00:21:22.860> on<00:21:22.980> why<00:21:23.280> you 00:21:23.450 --> 00:21:23.460 align:start position:0% do you have any thoughts on why you 00:21:23.460 --> 00:21:26.630 align:start position:0% do you have any thoughts on why you would<00:21:23.700> want<00:21:24.000> this<00:21:24.299> to<00:21:24.480> be<00:21:24.720> executed<00:21:25.440> on<00:21:25.740> chain 00:21:26.630 --> 00:21:26.640 align:start position:0% would want this to be executed on chain 00:21:26.640 --> 00:21:29.210 align:start position:0% would want this to be executed on chain not<00:21:27.419> at<00:21:27.600> all<00:21:27.720> okay 00:21:29.210 --> 00:21:29.220 align:start position:0% not at all okay 00:21:29.220 --> 00:21:31.549 align:start position:0% not at all okay should<00:21:29.700> not<00:21:29.880> run<00:21:30.059> this<00:21:30.299> Unchained<00:21:30.840> yeah<00:21:31.320> well 00:21:31.549 --> 00:21:31.559 align:start position:0% should not run this Unchained yeah well 00:21:31.559 --> 00:21:35.870 align:start position:0% should not run this Unchained yeah well actually<00:21:31.799> so<00:21:32.159> if<00:21:32.580> I<00:21:32.760> wait<00:21:33.120> let<00:21:33.419> me<00:21:33.539> quickly 00:21:35.870 --> 00:21:35.880 align:start position:0% actually so if I wait let me quickly 00:21:35.880 --> 00:21:41.630 align:start position:0% actually so if I wait let me quickly just<00:21:36.480> look<00:21:36.659> how<00:21:36.900> much<00:21:37.020> gas<00:21:37.200> this<00:21:37.500> takes 00:21:41.630 --> 00:21:41.640 align:start position:0% 00:21:41.640 --> 00:21:43.909 align:start position:0% for<00:21:42.240> this<00:21:42.419> tiny<00:21:42.780> program 00:21:43.909 --> 00:21:43.919 align:start position:0% for this tiny program 00:21:43.919 --> 00:21:46.310 align:start position:0% for this tiny program you<00:21:44.520> said<00:21:44.700> that<00:21:45.360> for<00:21:45.780> a<00:21:45.900> given<00:21:46.140> program 00:21:46.310 --> 00:21:46.320 align:start position:0% you said that for a given program 00:21:46.320 --> 00:21:47.930 align:start position:0% you said that for a given program there's<00:21:46.620> a<00:21:46.799> lot<00:21:46.860> of<00:21:46.980> different<00:21:47.159> encodings<00:21:47.760> you 00:21:47.930 --> 00:21:47.940 align:start position:0% there's a lot of different encodings you 00:21:47.940 --> 00:21:50.450 align:start position:0% there's a lot of different encodings you could<00:21:48.059> have<00:21:48.720> can<00:21:49.200> you<00:21:49.380> give<00:21:49.679> a<00:21:50.220> few<00:21:50.280> other 00:21:50.450 --> 00:21:50.460 align:start position:0% could have can you give a few other 00:21:50.460 --> 00:21:52.490 align:start position:0% could have can you give a few other ideas<00:21:50.700> of<00:21:51.179> other<00:21:51.539> encodings<00:21:52.080> and<00:21:52.260> what<00:21:52.380> would 00:21:52.490 --> 00:21:52.500 align:start position:0% ideas of other encodings and what would 00:21:52.500 --> 00:21:54.649 align:start position:0% ideas of other encodings and what would be<00:21:52.620> the<00:21:52.740> trade-offs 00:21:54.649 --> 00:21:54.659 align:start position:0% be the trade-offs 00:21:54.659 --> 00:21:57.049 align:start position:0% be the trade-offs yeah<00:21:55.020> so<00:21:55.200> this<00:21:55.500> encoding<00:21:55.980> uses 00:21:57.049 --> 00:21:57.059 align:start position:0% yeah so this encoding uses 00:21:57.059 --> 00:21:59.750 align:start position:0% yeah so this encoding uses um<00:21:57.539> this<00:21:57.900> encoding<00:21:58.440> basically<00:21:59.100> chooses<00:21:59.520> which 00:21:59.750 --> 00:21:59.760 align:start position:0% um this encoding basically chooses which 00:21:59.760 --> 00:22:00.950 align:start position:0% um this encoding basically chooses which has<00:22:00.000> a<00:22:00.120> difference<00:22:00.240> logic<00:22:00.600> because<00:22:00.720> the 00:22:00.950 --> 00:22:00.960 align:start position:0% has a difference logic because the 00:22:00.960 --> 00:22:02.270 align:start position:0% has a difference logic because the solver<00:22:01.260> is<00:22:01.380> very<00:22:01.559> simple<00:22:01.679> so<00:22:01.860> we<00:22:02.039> could<00:22:02.100> write 00:22:02.270 --> 00:22:02.280 align:start position:0% solver is very simple so we could write 00:22:02.280 --> 00:22:04.490 align:start position:0% solver is very simple so we could write in<00:22:02.460> solidity<00:22:02.820> right<00:22:03.059> so<00:22:03.299> the<00:22:03.539> the<00:22:03.840> encoding<00:22:04.320> is 00:22:04.490 --> 00:22:04.500 align:start position:0% in solidity right so the the encoding is 00:22:04.500 --> 00:22:06.710 align:start position:0% in solidity right so the the encoding is tailored<00:22:04.919> to<00:22:05.100> become<00:22:06.000> systems<00:22:06.600> of 00:22:06.710 --> 00:22:06.720 align:start position:0% tailored to become systems of 00:22:06.720 --> 00:22:08.029 align:start position:0% tailored to become systems of inequalities<00:22:07.260> that<00:22:07.440> look<00:22:07.679> like<00:22:07.860> the 00:22:08.029 --> 00:22:08.039 align:start position:0% inequalities that look like the 00:22:08.039 --> 00:22:09.669 align:start position:0% inequalities that look like the constraints<00:22:08.340> that<00:22:08.520> a<00:22:08.580> DL<00:22:08.820> solver<00:22:09.179> would<00:22:09.360> take 00:22:09.669 --> 00:22:09.679 align:start position:0% constraints that a DL solver would take 00:22:09.679 --> 00:22:13.970 align:start position:0% constraints that a DL solver would take but<00:22:11.059> where<00:22:12.059> is<00:22:12.240> it<00:22:12.299> now 00:22:13.970 --> 00:22:13.980 align:start position:0% but where is it now 00:22:13.980 --> 00:22:15.649 align:start position:0% but where is it now um<00:22:14.039> in<00:22:14.220> Harris<00:22:14.460> talk<00:22:14.820> actually<00:22:15.059> which<00:22:15.360> I<00:22:15.539> have 00:22:15.649 --> 00:22:15.659 align:start position:0% um in Harris talk actually which I have 00:22:15.659 --> 00:22:17.450 align:start position:0% um in Harris talk actually which I have here 00:22:17.450 --> 00:22:17.460 align:start position:0% here 00:22:17.460 --> 00:22:20.149 align:start position:0% here there<00:22:18.059> are<00:22:18.299> different 00:22:20.149 --> 00:22:20.159 align:start position:0% there are different 00:22:20.159 --> 00:22:22.010 align:start position:0% there are different so<00:22:20.640> if<00:22:20.700> you<00:22:20.820> wanna<00:22:20.940> if<00:22:21.240> you<00:22:21.360> actually<00:22:21.539> want<00:22:21.900> to 00:22:22.010 --> 00:22:22.020 align:start position:0% so if you wanna if you actually want to 00:22:22.020 --> 00:22:23.930 align:start position:0% so if you wanna if you actually want to encode<00:22:22.380> add<00:22:22.620> mold<00:22:23.100> div<00:22:23.280> all<00:22:23.520> these<00:22:23.760> kind<00:22:23.820> of 00:22:23.930 --> 00:22:23.940 align:start position:0% encode add mold div all these kind of 00:22:23.940 --> 00:22:26.450 align:start position:0% encode add mold div all these kind of things<00:22:24.059> you<00:22:24.840> will<00:22:25.020> need<00:22:25.260> more<00:22:26.039> complicated 00:22:26.450 --> 00:22:26.460 align:start position:0% things you will need more complicated 00:22:26.460 --> 00:22:28.909 align:start position:0% things you will need more complicated constraints<00:22:26.880> like<00:22:27.059> linear<00:22:27.419> combinations 00:22:28.909 --> 00:22:28.919 align:start position:0% constraints like linear combinations 00:22:28.919 --> 00:22:30.830 align:start position:0% constraints like linear combinations where<00:22:29.220> is<00:22:29.340> it<00:22:29.460> Harry 00:22:30.830 --> 00:22:30.840 align:start position:0% where is it Harry 00:22:30.840 --> 00:22:32.870 align:start position:0% where is it Harry yeah<00:22:31.100> you'll<00:22:32.100> need<00:22:32.220> linear<00:22:32.520> combinations 00:22:32.870 --> 00:22:32.880 align:start position:0% yeah you'll need linear combinations 00:22:32.880 --> 00:22:34.430 align:start position:0% yeah you'll need linear combinations like<00:22:33.360> this<00:22:33.480> for<00:22:33.659> example<00:22:33.900> and<00:22:34.080> more 00:22:34.430 --> 00:22:34.440 align:start position:0% like this for example and more 00:22:34.440 --> 00:22:36.110 align:start position:0% like this for example and more complicated<00:22:34.799> constraints<00:22:35.280> and<00:22:35.700> you'll<00:22:35.940> need 00:22:36.110 --> 00:22:36.120 align:start position:0% complicated constraints and you'll need 00:22:36.120 --> 00:22:38.390 align:start position:0% complicated constraints and you'll need like<00:22:36.299> a<00:22:36.419> Simplex<00:22:36.780> or<00:22:37.320> integer<00:22:38.100> linear 00:22:38.390 --> 00:22:38.400 align:start position:0% like a Simplex or integer linear 00:22:38.400 --> 00:22:40.370 align:start position:0% like a Simplex or integer linear programming<00:22:38.820> thing<00:22:39.120> or 00:22:40.370 --> 00:22:40.380 align:start position:0% programming thing or 00:22:40.380 --> 00:22:42.890 align:start position:0% programming thing or even<00:22:40.799> in<00:22:41.039> non-linear<00:22:41.700> is<00:22:41.820> over<00:22:42.000> depending<00:22:42.539> and 00:22:42.890 --> 00:22:42.900 align:start position:0% even in non-linear is over depending and 00:22:42.900 --> 00:22:44.510 align:start position:0% even in non-linear is over depending and these<00:22:43.559> things<00:22:43.620> are<00:22:43.799> a<00:22:43.919> lot<00:22:43.980> more<00:22:44.159> complicated 00:22:44.510 --> 00:22:44.520 align:start position:0% these things are a lot more complicated 00:22:44.520 --> 00:22:47.029 align:start position:0% these things are a lot more complicated so<00:22:44.760> Simplex<00:22:45.240> is<00:22:45.840> well<00:22:46.200> it's 00:22:47.029 --> 00:22:47.039 align:start position:0% so Simplex is well it's 00:22:47.039 --> 00:22:50.330 align:start position:0% so Simplex is well it's it's<00:22:47.520> an<00:22:47.700> exponential<00:22:48.240> algorithm<00:22:48.840> that<00:22:49.799> kind 00:22:50.330 --> 00:22:50.340 align:start position:0% it's an exponential algorithm that kind 00:22:50.340 --> 00:22:51.770 align:start position:0% it's an exponential algorithm that kind of<00:22:50.460> happens<00:22:50.580> to<00:22:50.820> run<00:22:51.000> mostly<00:22:51.299> in<00:22:51.419> polynomial 00:22:51.770 --> 00:22:51.780 align:start position:0% of happens to run mostly in polynomial 00:22:51.780 --> 00:22:54.230 align:start position:0% of happens to run mostly in polynomial time<00:22:51.960> these<00:22:52.200> days<00:22:52.640> but<00:22:53.640> in<00:22:53.760> all<00:22:53.940> linear 00:22:54.230 --> 00:22:54.240 align:start position:0% time these days but in all linear 00:22:54.240 --> 00:22:55.850 align:start position:0% time these days but in all linear non-linear<00:22:54.900> Earth<00:22:55.080> if<00:22:55.380> you're<00:22:55.679> trying<00:22:55.799> to 00:22:55.850 --> 00:22:55.860 align:start position:0% non-linear Earth if you're trying to 00:22:55.860 --> 00:22:56.930 align:start position:0% non-linear Earth if you're trying to solve<00:22:55.919> nonlinear<00:22:56.340> constraints<00:22:56.640> that's<00:22:56.820> an 00:22:56.930 --> 00:22:56.940 align:start position:0% solve nonlinear constraints that's an 00:22:56.940 --> 00:22:58.549 align:start position:0% solve nonlinear constraints that's an undetable<00:22:57.360> problem<00:22:57.600> and<00:22:58.200> you're<00:22:58.320> going<00:22:58.440> to 00:22:58.549 --> 00:22:58.559 align:start position:0% undetable problem and you're going to 00:22:58.559 --> 00:23:01.700 align:start position:0% undetable problem and you're going to have<00:22:58.620> a<00:22:58.679> hard<00:22:58.799> time<00:22:58.919> solving<00:22:59.280> it<00:22:59.340> so