WEBVTT Kind: captions Language: en 00:00:00.030 --> 00:00:02.629 align:start position:0% yeah<00:00:00.719> he's<00:00:00.870> heading<00:00:01.140> Leo<00:00:01.319> work<00:00:01.680> with<00:00:01.949> on 00:00:02.629 --> 00:00:02.639 align:start position:0% yeah he's heading Leo work with on 00:00:02.639 --> 00:00:04.910 align:start position:0% yeah he's heading Leo work with on foundation<00:00:03.389> aetherium<00:00:03.750> foundation<00:00:04.230> on<00:00:04.560> the 00:00:04.910 --> 00:00:04.920 align:start position:0% foundation aetherium foundation on the 00:00:04.920 --> 00:00:09.350 align:start position:0% foundation aetherium foundation on the solidity<00:00:05.480> team<00:00:06.740> doing<00:00:07.740> language<00:00:08.580> design<00:00:09.120> work 00:00:09.350 --> 00:00:09.360 align:start position:0% solidity team doing language design work 00:00:09.360 --> 00:00:11.629 align:start position:0% solidity team doing language design work and<00:00:09.599> compiler<00:00:09.929> work<00:00:10.139> and<00:00:10.410> also<00:00:10.559> doing<00:00:11.370> formal 00:00:11.629 --> 00:00:11.639 align:start position:0% and compiler work and also doing formal 00:00:11.639 --> 00:00:14.150 align:start position:0% and compiler work and also doing formal verification<00:00:12.080> which<00:00:13.080> is<00:00:13.440> what<00:00:13.740> this<00:00:13.950> talk<00:00:14.130> is 00:00:14.150 --> 00:00:14.160 align:start position:0% verification which is what this talk is 00:00:14.160 --> 00:00:15.829 align:start position:0% verification which is what this talk is about<00:00:14.309> I'm<00:00:14.730> going<00:00:14.880> to<00:00:14.969> talk<00:00:15.150> about<00:00:15.269> so<00:00:15.540> ladies 00:00:15.829 --> 00:00:15.839 align:start position:0% about I'm going to talk about so ladies 00:00:15.839 --> 00:00:17.960 align:start position:0% about I'm going to talk about so ladies SMT<00:00:16.170> checker<00:00:16.379> which<00:00:16.650> is<00:00:16.859> a<00:00:17.100> formal 00:00:17.960 --> 00:00:17.970 align:start position:0% SMT checker which is a formal 00:00:17.970 --> 00:00:20.210 align:start position:0% SMT checker which is a formal verification<00:00:18.119> component<00:00:18.869> that<00:00:19.770> gives 00:00:20.210 --> 00:00:20.220 align:start position:0% verification component that gives 00:00:20.220 --> 00:00:24.800 align:start position:0% verification component that gives compile<00:00:21.060> time<00:00:21.390> results<00:00:22.080> about<00:00:22.920> safety<00:00:23.810> safety 00:00:24.800 --> 00:00:24.810 align:start position:0% compile time results about safety safety 00:00:24.810 --> 00:00:28.880 align:start position:0% compile time results about safety safety checks<00:00:25.050> so<00:00:26.000> have<00:00:27.000> two<00:00:27.590> questions<00:00:28.590> so<00:00:28.740> how<00:00:28.830> many 00:00:28.880 --> 00:00:28.890 align:start position:0% checks so have two questions so how many 00:00:28.890 --> 00:00:31.120 align:start position:0% checks so have two questions so how many people<00:00:29.160> here<00:00:29.490> are<00:00:29.519> a<00:00:29.699> solidity<00:00:30.090> developers 00:00:31.120 --> 00:00:31.130 align:start position:0% people here are a solidity developers 00:00:31.130 --> 00:00:35.270 align:start position:0% people here are a solidity developers okay<00:00:32.130> cool<00:00:32.340> and<00:00:32.550> how<00:00:33.540> do<00:00:33.600> you<00:00:34.260> feel<00:00:35.219> about 00:00:35.270 --> 00:00:35.280 align:start position:0% okay cool and how do you feel about 00:00:35.280 --> 00:00:41.330 align:start position:0% okay cool and how do you feel about audience<00:00:36.059> participation<00:00:38.719> okay<00:00:39.719> cool<00:00:40.340> you 00:00:41.330 --> 00:00:41.340 align:start position:0% audience participation okay cool you 00:00:41.340 --> 00:00:44.470 align:start position:0% audience participation okay cool you asked<00:00:41.579> how<00:00:41.760> so<00:00:42.210> request<00:00:42.660> the<00:00:43.469> answer<00:00:43.829> is 00:00:44.470 --> 00:00:44.480 align:start position:0% asked how so request the answer is 00:00:44.480 --> 00:00:49.580 align:start position:0% asked how so request the answer is you're<00:00:45.480> gonna<00:00:45.539> help<00:00:46.200> me<00:00:46.320> solve<00:00:46.469> this<00:00:48.559> so<00:00:49.559> I 00:00:49.580 --> 00:00:49.590 align:start position:0% you're gonna help me solve this so I 00:00:49.590 --> 00:00:52.670 align:start position:0% you're gonna help me solve this so I want<00:00:49.950> to<00:00:49.980> first<00:00:50.190> introduce<00:00:50.370> what<00:00:50.910> is<00:00:51.680> SMT 00:00:52.670 --> 00:00:52.680 align:start position:0% want to first introduce what is SMT 00:00:52.680 --> 00:00:55.040 align:start position:0% want to first introduce what is SMT what's<00:00:52.980> why<00:00:53.250> SMT<00:00:53.699> checker<00:00:53.940> so<00:00:54.239> the<00:00:54.449> SMT<00:00:54.780> comes 00:00:55.040 --> 00:00:55.050 align:start position:0% what's why SMT checker so the SMT comes 00:00:55.050 --> 00:00:57.770 align:start position:0% what's why SMT checker so the SMT comes from<00:00:55.410> satisfiability<00:00:55.980> modular<00:00:56.520> theories<00:00:56.879> and 00:00:57.770 --> 00:00:57.780 align:start position:0% from satisfiability modular theories and 00:00:57.780 --> 00:01:01.099 align:start position:0% from satisfiability modular theories and Assam<00:00:58.410> to<00:00:58.559> solver<00:00:58.980> is<00:00:59.160> a<00:01:00.149> tool<00:01:00.480> that<00:01:00.690> will<00:01:00.840> take 00:01:01.099 --> 00:01:01.109 align:start position:0% Assam to solver is a tool that will take 00:01:01.109 --> 00:01:03.229 align:start position:0% Assam to solver is a tool that will take a<00:01:01.140> formula<00:01:01.649> like<00:01:01.800> this<00:01:01.829> a<00:01:02.160> first-order<00:01:02.609> logic 00:01:03.229 --> 00:01:03.239 align:start position:0% a formula like this a first-order logic 00:01:03.239 --> 00:01:06.980 align:start position:0% a formula like this a first-order logic formula<00:01:03.840> and<00:01:04.019> try<00:01:04.680> to<00:01:04.739> answer<00:01:05.510> this<00:01:06.510> questions 00:01:06.980 --> 00:01:06.990 align:start position:0% formula and try to answer this questions 00:01:06.990 --> 00:01:10.280 align:start position:0% formula and try to answer this questions can<00:01:07.979> we<00:01:08.100> find<00:01:08.400> integer<00:01:09.000> values<00:01:09.420> for<00:01:09.689> a<00:01:09.960> b<00:01:10.260> c 00:01:10.280 --> 00:01:10.290 align:start position:0% can we find integer values for a b c 00:01:10.290 --> 00:01:13.160 align:start position:0% can we find integer values for a b c such<00:01:10.799> that<00:01:11.360> this<00:01:12.360> formula<00:01:12.659> when<00:01:13.080> we 00:01:13.160 --> 00:01:13.170 align:start position:0% such that this formula when we 00:01:13.170 --> 00:01:15.440 align:start position:0% such that this formula when we substitute<00:01:13.409> the<00:01:14.189> values<00:01:14.610> for<00:01:15.360> these 00:01:15.440 --> 00:01:15.450 align:start position:0% substitute the values for these 00:01:15.450 --> 00:01:18.859 align:start position:0% substitute the values for these variables<00:01:15.979> evaluates<00:01:16.979> to<00:01:17.100> true<00:01:17.150> so<00:01:18.150> just<00:01:18.180> two 00:01:18.859 --> 00:01:18.869 align:start position:0% variables evaluates to true so just two 00:01:18.869 --> 00:01:22.550 align:start position:0% variables evaluates to true so just two I<00:01:19.140> can<00:01:19.950> go<00:01:20.100> together<00:01:20.340> over<00:01:21.119> the<00:01:21.299> formula<00:01:21.570> just 00:01:22.550 --> 00:01:22.560 align:start position:0% I can go together over the formula just 00:01:22.560 --> 00:01:24.620 align:start position:0% I can go together over the formula just to<00:01:22.979> give<00:01:23.460> a<00:01:23.490> little<00:01:23.640> bit<00:01:23.759> of<00:01:23.850> context<00:01:24.270> to 00:01:24.620 --> 00:01:24.630 align:start position:0% to give a little bit of context to 00:01:24.630 --> 00:01:27.140 align:start position:0% to give a little bit of context to whoever<00:01:24.930> is<00:01:25.020> not<00:01:25.110> familiar<00:01:25.439> with<00:01:26.310> electrical 00:01:27.140 --> 00:01:27.150 align:start position:0% whoever is not familiar with electrical 00:01:27.150 --> 00:01:30.830 align:start position:0% whoever is not familiar with electrical activity<00:01:27.509> this<00:01:27.600> kind<00:01:27.810> of<00:01:27.840> things<00:01:29.780> okay<00:01:30.780> so 00:01:30.830 --> 00:01:30.840 align:start position:0% activity this kind of things okay so 00:01:30.840 --> 00:01:32.600 align:start position:0% activity this kind of things okay so it's<00:01:31.439> a<00:01:31.560> boolean<00:01:31.829> formula<00:01:32.009> right<00:01:32.430> it's<00:01:32.549> a 00:01:32.600 --> 00:01:32.610 align:start position:0% it's a boolean formula right it's a 00:01:32.610 --> 00:01:34.730 align:start position:0% it's a boolean formula right it's a conjunction<00:01:33.090> of<00:01:33.329> constraints<00:01:33.840> so<00:01:34.560> this 00:01:34.730 --> 00:01:34.740 align:start position:0% conjunction of constraints so this 00:01:34.740 --> 00:01:37.700 align:start position:0% conjunction of constraints so this formula<00:01:35.210> kind<00:01:36.210> of<00:01:36.299> returns<00:01:36.630> true<00:01:37.170> or<00:01:37.439> false 00:01:37.700 --> 00:01:37.710 align:start position:0% formula kind of returns true or false 00:01:37.710 --> 00:01:39.740 align:start position:0% formula kind of returns true or false right<00:01:38.040> a<00:01:38.100> boolean<00:01:38.490> value<00:01:38.670> this<00:01:39.210> constraints 00:01:39.740 --> 00:01:39.750 align:start position:0% right a boolean value this constraints 00:01:39.750 --> 00:01:42.499 align:start position:0% right a boolean value this constraints are<00:01:39.840> satisfiable<00:01:40.350> together<00:01:40.770> or<00:01:41.009> not<00:01:41.250> so<00:01:42.240> first 00:01:42.499 --> 00:01:42.509 align:start position:0% are satisfiable together or not so first 00:01:42.509 --> 00:01:43.850 align:start position:0% are satisfiable together or not so first we<00:01:42.630> have<00:01:42.780> this<00:01:42.960> part<00:01:43.200> of<00:01:43.259> the<00:01:43.350> formula<00:01:43.590> which 00:01:43.850 --> 00:01:43.860 align:start position:0% we have this part of the formula which 00:01:43.860 --> 00:01:45.740 align:start position:0% we have this part of the formula which basically<00:01:44.310> says<00:01:44.670> it's<00:01:45.270> kind<00:01:45.570> of<00:01:45.600> like<00:01:45.720> a 00:01:45.740 --> 00:01:45.750 align:start position:0% basically says it's kind of like a 00:01:45.750 --> 00:01:47.690 align:start position:0% basically says it's kind of like a function<00:01:46.140> definition<00:01:46.259> right<00:01:46.799> so<00:01:47.070> there's<00:01:47.640> a 00:01:47.690 --> 00:01:47.700 align:start position:0% function definition right so there's a 00:01:47.700 --> 00:01:50.179 align:start position:0% function definition right so there's a lot<00:01:47.880> of<00:01:48.000> same<00:01:48.450> sex<00:01:48.630> abuse<00:01:48.990> here<00:01:49.170> but<00:01:49.470> we're 00:01:50.179 --> 00:01:50.189 align:start position:0% lot of same sex abuse here but we're 00:01:50.189 --> 00:01:52.819 align:start position:0% lot of same sex abuse here but we're gonna<00:01:50.280> ignore<00:01:50.549> that<00:01:51.030> for<00:01:51.270> now<00:01:51.470> so<00:01:52.470> this<00:01:52.649> says 00:01:52.819 --> 00:01:52.829 align:start position:0% gonna ignore that for now so this says 00:01:52.829 --> 00:01:55.789 align:start position:0% gonna ignore that for now so this says that<00:01:52.860> for<00:01:53.399> whatever<00:01:53.579> acts<00:01:53.939> f<00:01:54.390> of<00:01:54.659> X<00:01:54.899> equals<00:01:55.380> x 00:01:55.789 --> 00:01:55.799 align:start position:0% that for whatever acts f of X equals x 00:01:55.799 --> 00:02:00.340 align:start position:0% that for whatever acts f of X equals x times<00:01:56.189> 42<00:01:56.579> okay<00:01:58.009> the<00:01:59.009> next<00:01:59.399> we<00:01:59.520> have<00:01:59.700> two 00:02:00.340 --> 00:02:00.350 align:start position:0% times 42 okay the next we have two 00:02:00.350 --> 00:02:03.620 align:start position:0% times 42 okay the next we have two constraints<00:02:01.350> over<00:02:01.790> the<00:02:02.790> input<00:02:03.119> variables<00:02:03.509> we 00:02:03.620 --> 00:02:03.630 align:start position:0% constraints over the input variables we 00:02:03.630 --> 00:02:05.840 align:start position:0% constraints over the input variables we chose<00:02:03.899> so<00:02:04.229> we're<00:02:04.500> saying<00:02:04.740> that<00:02:04.890> a<00:02:05.189> has<00:02:05.670> to<00:02:05.820> be 00:02:05.840 --> 00:02:05.850 align:start position:0% chose so we're saying that a has to be 00:02:05.850 --> 00:02:08.359 align:start position:0% chose so we're saying that a has to be greater<00:02:06.210> or<00:02:06.479> equal<00:02:06.570> B<00:02:07.049> and<00:02:07.320> B<00:02:07.920> has<00:02:08.220> to<00:02:08.340> be 00:02:08.359 --> 00:02:08.369 align:start position:0% greater or equal B and B has to be 00:02:08.369 --> 00:02:13.520 align:start position:0% greater or equal B and B has to be greater<00:02:08.700> or<00:02:08.789> equal<00:02:08.940> C<00:02:09.619> and<00:02:11.300> then<00:02:12.300> last 00:02:13.520 --> 00:02:13.530 align:start position:0% greater or equal C and then last 00:02:13.530 --> 00:02:15.980 align:start position:0% greater or equal C and then last we<00:02:13.650> applied<00:02:14.370> function<00:02:15.030> f<00:02:15.240> we<00:02:15.510> defined<00:02:15.840> before 00:02:15.980 --> 00:02:15.990 align:start position:0% we applied function f we defined before 00:02:15.990 --> 00:02:19.130 align:start position:0% we applied function f we defined before over<00:02:16.440> a<00:02:16.470> and<00:02:16.860> C<00:02:17.400> saying<00:02:17.790> FFA<00:02:18.480> has<00:02:18.510> a<00:02:18.720> be<00:02:18.900> greater 00:02:19.130 --> 00:02:19.140 align:start position:0% over a and C saying FFA has a be greater 00:02:19.140 --> 00:02:22.430 align:start position:0% over a and C saying FFA has a be greater or<00:02:19.380> equal<00:02:19.410> F<00:02:19.920> of<00:02:19.950> C<00:02:20.850> so<00:02:21.660> now<00:02:22.080> the<00:02:22.140> question 00:02:22.430 --> 00:02:22.440 align:start position:0% or equal F of C so now the question 00:02:22.440 --> 00:02:25.730 align:start position:0% or equal F of C so now the question again<00:02:23.400> can<00:02:23.610> we<00:02:23.640> find<00:02:24.000> integer<00:02:24.390> values<00:02:24.750> that 00:02:25.730 --> 00:02:25.740 align:start position:0% again can we find integer values that 00:02:25.740 --> 00:02:29.740 align:start position:0% again can we find integer values that evaluate<00:02:26.220> the<00:02:26.310> formula<00:02:26.640> to<00:02:26.730> two<00:02:27.030> true<00:02:28.430> yes 00:02:29.740 --> 00:02:29.750 align:start position:0% evaluate the formula to two true yes 00:02:29.750 --> 00:02:45.140 align:start position:0% evaluate the formula to two true yes okay<00:02:30.750> can<00:02:31.260> you<00:02:31.290> give<00:02:32.069> me<00:02:32.250> values<00:02:32.610> for<00:02:32.760> ABC<00:02:44.120> yeah 00:02:45.140 --> 00:02:45.150 align:start position:0% okay can you give me values for ABC yeah 00:02:45.150 --> 00:02:47.030 align:start position:0% okay can you give me values for ABC yeah so<00:02:45.600> now<00:02:45.780> you<00:02:46.170> told<00:02:46.350> me<00:02:46.440> that<00:02:46.500> it's<00:02:46.650> possible 00:02:47.030 --> 00:02:47.040 align:start position:0% so now you told me that it's possible 00:02:47.040 --> 00:02:49.460 align:start position:0% so now you told me that it's possible right<00:02:47.250> it's<00:02:47.519> possible<00:02:47.970> to<00:02:48.209> give<00:02:48.360> values<00:02:48.780> for<00:02:49.440> a 00:02:49.460 --> 00:02:49.470 align:start position:0% right it's possible to give values for a 00:02:49.470 --> 00:02:53.530 align:start position:0% right it's possible to give values for a B<00:02:49.709> C<00:02:49.950> such<00:02:50.280> that<00:02:50.310> the<00:02:50.489> formulas<00:02:50.820> true<00:02:51.980> 0<00:02:52.980> 0<00:02:53.190> 0 00:02:53.530 --> 00:02:53.540 align:start position:0% B C such that the formulas true 0 0 0 00:02:53.540 --> 00:02:58.309 align:start position:0% B C such that the formulas true 0 0 0 does<00:02:54.540> that<00:02:54.690> work<00:02:55.370> it<00:02:56.370> works<00:02:56.580> right<00:02:57.319> zero 00:02:58.309 --> 00:02:58.319 align:start position:0% does that work it works right zero 00:02:58.319 --> 00:03:00.680 align:start position:0% does that work it works right zero greater<00:02:58.590> equals<00:02:58.950> 0<00:02:59.220> true<00:02:59.580> same<00:02:59.910> thing<00:03:00.120> for<00:03:00.150> BC 00:03:00.680 --> 00:03:00.690 align:start position:0% greater equals 0 true same thing for BC 00:03:00.690 --> 00:03:04.910 align:start position:0% greater equals 0 true same thing for BC f<00:03:00.959> of<00:03:01.590> a<00:03:01.739> 0<00:03:02.069> F<00:03:02.250> F<00:03:02.370> is<00:03:02.519> f<00:03:02.850> of<00:03:03.090> C<00:03:03.300> 0<00:03:03.440> it's<00:03:04.440> true<00:03:04.680> right 00:03:04.910 --> 00:03:04.920 align:start position:0% f of a 0 F F is f of C 0 it's true right 00:03:04.920 --> 00:03:08.300 align:start position:0% f of a 0 F F is f of C 0 it's true right but<00:03:05.790> unfortunately<00:03:06.390> that's<00:03:07.230> not<00:03:07.410> the<00:03:07.920> one 00:03:08.300 --> 00:03:08.310 align:start position:0% but unfortunately that's not the one 00:03:08.310 --> 00:03:11.210 align:start position:0% but unfortunately that's not the one that<00:03:08.430> I<00:03:08.489> had<00:03:08.640> here<00:03:08.850> so<00:03:09.680> anyway<00:03:10.680> so<00:03:10.739> this<00:03:11.040> one 00:03:11.210 --> 00:03:11.220 align:start position:0% that I had here so anyway so this one 00:03:11.220 --> 00:03:15.259 align:start position:0% that I had here so anyway so this one works<00:03:11.459> right<00:03:12.440> also<00:03:13.440> this<00:03:13.830> one<00:03:14.040> works<00:03:14.250> and<00:03:14.580> this 00:03:15.259 --> 00:03:15.269 align:start position:0% works right also this one works and this 00:03:15.269 --> 00:03:19.069 align:start position:0% works right also this one works and this one<00:03:15.480> works<00:03:16.130> how<00:03:17.130> many<00:03:17.160> do<00:03:17.910> you<00:03:17.940> think<00:03:18.269> how<00:03:18.900> many 00:03:19.069 --> 00:03:19.079 align:start position:0% one works how many do you think how many 00:03:19.079 --> 00:03:21.319 align:start position:0% one works how many do you think how many solutions<00:03:19.410> how<00:03:20.190> many<00:03:20.340> different<00:03:20.549> sets<00:03:21.060> of 00:03:21.319 --> 00:03:21.329 align:start position:0% solutions how many different sets of 00:03:21.329 --> 00:03:24.500 align:start position:0% solutions how many different sets of values<00:03:22.320> for<00:03:22.650> ABC<00:03:23.220> do<00:03:23.790> you<00:03:23.910> think<00:03:24.120> we<00:03:24.180> can<00:03:24.329> get 00:03:24.500 --> 00:03:24.510 align:start position:0% values for ABC do you think we can get 00:03:24.510 --> 00:03:28.910 align:start position:0% values for ABC do you think we can get for<00:03:24.540> this<00:03:24.840> formula<00:03:25.880> infinite<00:03:26.880> right<00:03:27.560> now<00:03:28.560> a 00:03:28.910 --> 00:03:28.920 align:start position:0% for this formula infinite right now a 00:03:28.920 --> 00:03:31.039 align:start position:0% for this formula infinite right now a slightly<00:03:29.220> different<00:03:29.430> question<00:03:30.000> what<00:03:30.630> happens 00:03:31.039 --> 00:03:31.049 align:start position:0% slightly different question what happens 00:03:31.049 --> 00:03:33.410 align:start position:0% slightly different question what happens if<00:03:31.350> we<00:03:31.530> change<00:03:31.560> this<00:03:32.250> we<00:03:32.790> could<00:03:33.000> change<00:03:33.180> the 00:03:33.410 --> 00:03:33.420 align:start position:0% if we change this we could change the 00:03:33.420 --> 00:03:37.569 align:start position:0% if we change this we could change the comparison<00:03:33.989> of<00:03:34.130> FA<00:03:35.130> and<00:03:35.310> F<00:03:35.400> of<00:03:35.519> C<00:03:35.790> to<00:03:36.570> this<00:03:36.780> and 00:03:37.569 --> 00:03:37.579 align:start position:0% comparison of FA and F of C to this and 00:03:37.579 --> 00:03:41.840 align:start position:0% comparison of FA and F of C to this and repeat<00:03:38.579> the<00:03:38.730> question<00:03:39.620> is<00:03:40.620> there<00:03:41.070> a<00:03:41.280> set<00:03:41.549> of 00:03:41.840 --> 00:03:41.850 align:start position:0% repeat the question is there a set of 00:03:41.850 --> 00:03:44.420 align:start position:0% repeat the question is there a set of values<00:03:42.120> for<00:03:42.329> ABC<00:03:43.079> that<00:03:43.739> make<00:03:44.010> the<00:03:44.130> formula 00:03:44.420 --> 00:03:44.430 align:start position:0% values for ABC that make the formula 00:03:44.430 --> 00:03:51.110 align:start position:0% values for ABC that make the formula true<00:03:48.829> so<00:03:49.829> there's<00:03:50.040> a<00:03:50.100> consensus<00:03:50.640> saying<00:03:50.880> no 00:03:51.110 --> 00:03:51.120 align:start position:0% true so there's a consensus saying no 00:03:51.120 --> 00:03:54.530 align:start position:0% true so there's a consensus saying no and<00:03:51.390> that's<00:03:52.260> correct<00:03:52.530> and<00:03:53.269> when<00:03:54.269> that's<00:03:54.450> the 00:03:54.530 --> 00:03:54.540 align:start position:0% and that's correct and when that's the 00:03:54.540 --> 00:03:55.880 align:start position:0% and that's correct and when that's the case<00:03:54.660> we<00:03:55.049> say<00:03:55.200> that<00:03:55.230> the<00:03:55.350> formula<00:03:55.769> is 00:03:55.880 --> 00:03:55.890 align:start position:0% case we say that the formula is 00:03:55.890 --> 00:03:56.930 align:start position:0% case we say that the formula is unsatisfiable 00:03:56.930 --> 00:03:56.940 align:start position:0% unsatisfiable 00:03:56.940 --> 00:03:59.569 align:start position:0% unsatisfiable because<00:03:57.480> there<00:03:57.660> is<00:03:57.720> no<00:03:57.900> set<00:03:58.320> of<00:03:58.620> values<00:03:59.549> that 00:03:59.569 --> 00:03:59.579 align:start position:0% because there is no set of values that 00:03:59.579 --> 00:04:02.420 align:start position:0% because there is no set of values that satisfy<00:04:00.140> the<00:04:01.140> formula<00:04:01.590> so<00:04:02.160> in<00:04:02.220> the<00:04:02.280> previous 00:04:02.420 --> 00:04:02.430 align:start position:0% satisfy the formula so in the previous 00:04:02.430 --> 00:04:04.270 align:start position:0% satisfy the formula so in the previous case<00:04:02.700> were<00:04:02.880> satisfiable<00:04:03.510> now<00:04:03.690> we<00:04:03.750> have 00:04:04.270 --> 00:04:04.280 align:start position:0% case were satisfiable now we have 00:04:04.280 --> 00:04:08.270 align:start position:0% case were satisfiable now we have unsatisfiable<00:04:05.280> and<00:04:06.530> why<00:04:07.530> did<00:04:07.769> I<00:04:07.859> choose<00:04:08.070> this 00:04:08.270 --> 00:04:08.280 align:start position:0% unsatisfiable and why did I choose this 00:04:08.280 --> 00:04:10.160 align:start position:0% unsatisfiable and why did I choose this formula<00:04:08.700> could<00:04:08.910> have<00:04:09.060> chosen<00:04:09.329> many<00:04:09.720> other 00:04:10.160 --> 00:04:10.170 align:start position:0% formula could have chosen many other 00:04:10.170 --> 00:04:13.160 align:start position:0% formula could have chosen many other formulas<00:04:10.620> so<00:04:10.739> the<00:04:10.859> reason<00:04:11.510> is<00:04:12.510> we<00:04:12.720> can<00:04:12.900> read 00:04:13.160 --> 00:04:13.170 align:start position:0% formulas so the reason is we can read 00:04:13.170 --> 00:04:15.470 align:start position:0% formulas so the reason is we can read this<00:04:13.380> formula<00:04:13.859> in<00:04:14.010> many<00:04:14.640> ways<00:04:14.820> right<00:04:15.150> it<00:04:15.329> can 00:04:15.470 --> 00:04:15.480 align:start position:0% this formula in many ways right it can 00:04:15.480 --> 00:04:18.319 align:start position:0% this formula in many ways right it can be<00:04:15.660> just<00:04:15.959> a<00:04:16.140> logical<00:04:16.890> formula<00:04:17.130> but<00:04:17.430> this 00:04:18.319 --> 00:04:18.329 align:start position:0% be just a logical formula but this 00:04:18.329 --> 00:04:20.960 align:start position:0% be just a logical formula but this formula<00:04:18.750> happens<00:04:19.109> to<00:04:19.769> we<00:04:20.459> can't<00:04:20.640> we<00:04:20.729> can<00:04:20.850> also 00:04:20.960 --> 00:04:20.970 align:start position:0% formula happens to we can't we can also 00:04:20.970 --> 00:04:23.060 align:start position:0% formula happens to we can't we can also read<00:04:21.180> this<00:04:21.299> formula<00:04:21.659> as<00:04:21.810> this<00:04:22.530> part<00:04:22.860> here 00:04:23.060 --> 00:04:23.070 align:start position:0% read this formula as this part here 00:04:23.070 --> 00:04:25.640 align:start position:0% read this formula as this part here highlighted<00:04:23.520> right<00:04:23.669> now<00:04:23.880> being<00:04:24.630> a<00:04:25.020> property 00:04:25.640 --> 00:04:25.650 align:start position:0% highlighted right now being a property 00:04:25.650 --> 00:04:26.650 align:start position:0% highlighted right now being a property we<00:04:25.740> want<00:04:25.830> to<00:04:25.979> prove 00:04:26.650 --> 00:04:26.660 align:start position:0% we want to prove 00:04:26.660 --> 00:04:28.120 align:start position:0% we want to prove to<00:04:26.810> function<00:04:27.170> right<00:04:27.470> application<00:04:27.950> of<00:04:28.040> the 00:04:28.120 --> 00:04:28.130 align:start position:0% to function right application of the 00:04:28.130 --> 00:04:30.940 align:start position:0% to function right application of the function<00:04:28.810> that<00:04:29.810> part<00:04:30.110> being<00:04:30.440> local 00:04:30.940 --> 00:04:30.950 align:start position:0% function that part being local 00:04:30.950 --> 00:04:33.730 align:start position:0% function that part being local constraints<00:04:31.310> say<00:04:32.240> on<00:04:32.480> input<00:04:33.140> variables<00:04:33.530> and 00:04:33.730 --> 00:04:33.740 align:start position:0% constraints say on input variables and 00:04:33.740 --> 00:04:36.520 align:start position:0% constraints say on input variables and here<00:04:34.460> basically<00:04:34.700> a<00:04:34.940> function<00:04:35.300> definition<00:04:35.530> so 00:04:36.520 --> 00:04:36.530 align:start position:0% here basically a function definition so 00:04:36.530 --> 00:04:38.760 align:start position:0% here basically a function definition so this<00:04:36.800> is<00:04:36.950> basically<00:04:37.370> how<00:04:37.520> we<00:04:37.790> just<00:04:38.240> prove 00:04:38.760 --> 00:04:38.770 align:start position:0% this is basically how we just prove 00:04:38.770 --> 00:04:43.240 align:start position:0% this is basically how we just prove correctness<00:04:39.770> of<00:04:39.920> this<00:04:40.250> smart<00:04:40.520> contract<00:04:42.250> here 00:04:43.240 --> 00:04:43.250 align:start position:0% correctness of this smart contract here 00:04:43.250 --> 00:04:46.740 align:start position:0% correctness of this smart contract here we<00:04:43.370> have<00:04:43.580> a<00:04:43.910> function<00:04:44.270> definition<00:04:44.800> which 00:04:46.740 --> 00:04:46.750 align:start position:0% we have a function definition which 00:04:46.750 --> 00:04:49.920 align:start position:0% we have a function definition which would<00:04:47.750> be<00:04:47.900> encoded<00:04:48.380> in<00:04:48.650> the<00:04:48.770> SMT<00:04:49.130> language<00:04:49.520> as 00:04:49.920 --> 00:04:49.930 align:start position:0% would be encoded in the SMT language as 00:04:49.930 --> 00:04:54.520 align:start position:0% would be encoded in the SMT language as the<00:04:50.930> first<00:04:51.250> term<00:04:52.250> of<00:04:52.400> the<00:04:52.970> conjunction<00:04:53.660> here 00:04:54.520 --> 00:04:54.530 align:start position:0% the first term of the conjunction here 00:04:54.530 --> 00:04:57.220 align:start position:0% the first term of the conjunction here we<00:04:54.650> have<00:04:54.860> two<00:04:55.280> local<00:04:55.730> constraints<00:04:56.570> right<00:04:57.050> that 00:04:57.220 --> 00:04:57.230 align:start position:0% we have two local constraints right that 00:04:57.230 --> 00:05:01.180 align:start position:0% we have two local constraints right that evaluate<00:04:57.710> that<00:04:58.340> or<00:04:58.640> encoder<00:04:58.970> Tory<00:04:59.350> as<00:05:00.350> those 00:05:01.180 --> 00:05:01.190 align:start position:0% evaluate that or encoder Tory as those 00:05:01.190 --> 00:05:03.880 align:start position:0% evaluate that or encoder Tory as those those<00:05:01.550> circumstance<00:05:02.120> and<00:05:02.360> here<00:05:02.660> we<00:05:02.780> have<00:05:02.960> the 00:05:03.880 --> 00:05:03.890 align:start position:0% those circumstance and here we have the 00:05:03.890 --> 00:05:07.480 align:start position:0% those circumstance and here we have the application<00:05:04.430> of<00:05:04.670> the<00:05:05.150> function<00:05:05.620> but<00:05:06.620> you<00:05:07.310> will 00:05:07.480 --> 00:05:07.490 align:start position:0% application of the function but you will 00:05:07.490 --> 00:05:09.550 align:start position:0% application of the function but you will probably<00:05:07.730> notice<00:05:08.060> notice<00:05:08.600> right<00:05:08.750> now<00:05:08.810> that<00:05:09.290> in 00:05:09.550 --> 00:05:09.560 align:start position:0% probably notice notice right now that in 00:05:09.560 --> 00:05:12.520 align:start position:0% probably notice notice right now that in the<00:05:09.890> code<00:05:10.070> I<00:05:10.130> have<00:05:10.340> assert<00:05:11.000> F<00:05:11.240> FA<00:05:11.540> greater<00:05:12.290> or 00:05:12.520 --> 00:05:12.530 align:start position:0% the code I have assert F FA greater or 00:05:12.530 --> 00:05:14.110 align:start position:0% the code I have assert F FA greater or equal<00:05:12.560> F<00:05:12.860> of<00:05:13.010> C<00:05:13.190> because<00:05:13.340> it's<00:05:13.640> a<00:05:13.700> property<00:05:14.090> I 00:05:14.110 --> 00:05:14.120 align:start position:0% equal F of C because it's a property I 00:05:14.120 --> 00:05:17.200 align:start position:0% equal F of C because it's a property I want<00:05:14.300> to<00:05:14.390> prove<00:05:14.540> right<00:05:15.340> and<00:05:16.340> here<00:05:16.880> in<00:05:17.090> the 00:05:17.200 --> 00:05:17.210 align:start position:0% want to prove right and here in the 00:05:17.210 --> 00:05:19.210 align:start position:0% want to prove right and here in the logical<00:05:17.600> formula<00:05:18.080> that<00:05:18.230> we<00:05:18.380> give<00:05:18.590> to<00:05:18.620> the<00:05:18.800> SMT 00:05:19.210 --> 00:05:19.220 align:start position:0% logical formula that we give to the SMT 00:05:19.220 --> 00:05:21.280 align:start position:0% logical formula that we give to the SMT solver<00:05:19.580> it's<00:05:20.060> actually<00:05:20.510> last<00:05:20.720> then<00:05:20.990> so<00:05:21.170> it's 00:05:21.280 --> 00:05:21.290 align:start position:0% solver it's actually last then so it's 00:05:21.290 --> 00:05:24.700 align:start position:0% solver it's actually last then so it's the<00:05:21.410> opposite<00:05:21.890> operation<00:05:22.460> right<00:05:23.360> the<00:05:24.290> reason 00:05:24.700 --> 00:05:24.710 align:start position:0% the opposite operation right the reason 00:05:24.710 --> 00:05:27.550 align:start position:0% the opposite operation right the reason why<00:05:25.060> we<00:05:26.060> actually<00:05:26.240> ask<00:05:26.570> for<00:05:26.840> the<00:05:26.960> opposite<00:05:27.380> is 00:05:27.550 --> 00:05:27.560 align:start position:0% why we actually ask for the opposite is 00:05:27.560 --> 00:05:31.330 align:start position:0% why we actually ask for the opposite is if<00:05:28.150> this<00:05:29.150> is<00:05:29.420> unsatisfiable<00:05:30.260> if<00:05:30.710> we<00:05:31.040> try<00:05:31.280> to 00:05:31.330 --> 00:05:31.340 align:start position:0% if this is unsatisfiable if we try to 00:05:31.340 --> 00:05:33.820 align:start position:0% if this is unsatisfiable if we try to prove<00:05:31.730> the<00:05:32.360> negation<00:05:32.930> of<00:05:33.080> the<00:05:33.200> property<00:05:33.650> and 00:05:33.820 --> 00:05:33.830 align:start position:0% prove the negation of the property and 00:05:33.830 --> 00:05:36.880 align:start position:0% prove the negation of the property and the<00:05:34.790> solver<00:05:35.090> says<00:05:35.300> is<00:05:35.450> unsatisfiable<00:05:36.140> this 00:05:36.880 --> 00:05:36.890 align:start position:0% the solver says is unsatisfiable this 00:05:36.890 --> 00:05:39.730 align:start position:0% the solver says is unsatisfiable this means<00:05:37.250> that<00:05:37.580> there's<00:05:38.120> no<00:05:38.360> behavior<00:05:39.050> there's 00:05:39.730 --> 00:05:39.740 align:start position:0% means that there's no behavior there's 00:05:39.740 --> 00:05:42.250 align:start position:0% means that there's no behavior there's no<00:05:39.950> values<00:05:40.430> for<00:05:40.640> local<00:05:40.910> rivals<00:05:41.300> with<00:05:41.960> that 00:05:42.250 --> 00:05:42.260 align:start position:0% no values for local rivals with that 00:05:42.260 --> 00:05:44.110 align:start position:0% no values for local rivals with that encoding<00:05:42.770> that<00:05:43.250> actually<00:05:43.669> break<00:05:43.910> the 00:05:44.110 --> 00:05:44.120 align:start position:0% encoding that actually break the 00:05:44.120 --> 00:05:48.010 align:start position:0% encoding that actually break the assertion<00:05:44.860> right<00:05:46.180> so<00:05:47.180> in<00:05:47.330> this<00:05:47.480> case<00:05:47.540> the 00:05:48.010 --> 00:05:48.020 align:start position:0% assertion right so in this case the 00:05:48.020 --> 00:05:50.170 align:start position:0% assertion right so in this case the solver<00:05:48.320> will<00:05:48.440> tell<00:05:48.620> me<00:05:48.770> it's<00:05:49.340> unsatisfiable 00:05:50.170 --> 00:05:50.180 align:start position:0% solver will tell me it's unsatisfiable 00:05:50.180 --> 00:05:52.420 align:start position:0% solver will tell me it's unsatisfiable which<00:05:50.660> means<00:05:50.960> that<00:05:51.110> certian<00:05:51.380> is<00:05:51.470> safe<00:05:51.680> again 00:05:52.420 --> 00:05:52.430 align:start position:0% which means that certian is safe again 00:05:52.430 --> 00:05:53.650 align:start position:0% which means that certian is safe again because<00:05:52.700> there's<00:05:52.850> no<00:05:53.030> way<00:05:53.210> you<00:05:53.270> can<00:05:53.510> go 00:05:53.650 --> 00:05:53.660 align:start position:0% because there's no way you can go 00:05:53.660 --> 00:05:55.360 align:start position:0% because there's no way you can go through<00:05:53.960> the<00:05:54.080> program<00:05:54.500> and<00:05:54.710> break<00:05:55.190> the 00:05:55.360 --> 00:05:55.370 align:start position:0% through the program and break the 00:05:55.370 --> 00:05:57.790 align:start position:0% through the program and break the assertion<00:05:55.760> so<00:05:55.910> for<00:05:56.120> all<00:05:56.300> cases<00:05:56.690> you<00:05:57.080> can<00:05:57.590> ever 00:05:57.790 --> 00:05:57.800 align:start position:0% assertion so for all cases you can ever 00:05:57.800 --> 00:06:01.300 align:start position:0% assertion so for all cases you can ever come<00:05:58.100> up<00:05:58.250> with<00:05:58.280> the<00:05:59.000> assertion<00:05:59.210> is<00:05:59.570> true<00:06:00.310> but 00:06:01.300 --> 00:06:01.310 align:start position:0% come up with the assertion is true but 00:06:01.310 --> 00:06:03.460 align:start position:0% come up with the assertion is true but let's<00:06:01.880> change<00:06:02.090> a<00:06:02.240> little<00:06:02.330> bit<00:06:02.630> so<00:06:02.960> is<00:06:03.290> that 00:06:03.460 --> 00:06:03.470 align:start position:0% let's change a little bit so is that 00:06:03.470 --> 00:06:08.140 align:start position:0% let's change a little bit so is that assertion<00:06:03.770> true<00:06:06.400> is<00:06:07.400> that<00:06:07.460> assert<00:06:07.850> correct 00:06:08.140 --> 00:06:08.150 align:start position:0% assertion true is that assert correct 00:06:08.150 --> 00:06:12.159 align:start position:0% assertion true is that assert correct for<00:06:08.360> every<00:06:08.600> input<00:06:09.370> it's<00:06:10.370> not<00:06:10.580> right<00:06:10.970> so<00:06:11.630> for 00:06:12.159 --> 00:06:12.169 align:start position:0% for every input it's not right so for 00:06:12.169 --> 00:06:15.370 align:start position:0% for every input it's not right so for our<00:06:12.410> query<00:06:12.740> to<00:06:12.980> the<00:06:13.010> SMT<00:06:13.430> solver<00:06:13.900> we<00:06:14.900> negate 00:06:15.370 --> 00:06:15.380 align:start position:0% our query to the SMT solver we negate 00:06:15.380 --> 00:06:17.170 align:start position:0% our query to the SMT solver we negate the<00:06:15.560> property<00:06:15.950> right<00:06:16.250> so<00:06:16.520> I<00:06:16.550> want<00:06:16.820> to<00:06:16.880> find 00:06:17.170 --> 00:06:17.180 align:start position:0% the property right so I want to find 00:06:17.180 --> 00:06:19.120 align:start position:0% the property right so I want to find values<00:06:17.600> I<00:06:17.720> want<00:06:17.900> the<00:06:17.990> SMT<00:06:18.350> solver<00:06:18.650> to<00:06:18.800> give<00:06:18.950> me 00:06:19.120 --> 00:06:19.130 align:start position:0% values I want the SMT solver to give me 00:06:19.130 --> 00:06:23.290 align:start position:0% values I want the SMT solver to give me values<00:06:19.490> for<00:06:20.440> my<00:06:21.440> variables<00:06:21.950> that<00:06:22.580> actually 00:06:23.290 --> 00:06:23.300 align:start position:0% values for my variables that actually 00:06:23.300 --> 00:06:25.540 align:start position:0% values for my variables that actually break<00:06:23.540> the<00:06:23.720> certian<00:06:24.110> so<00:06:24.590> one<00:06:24.830> FFA<00:06:25.310> to<00:06:25.340> be 00:06:25.540 --> 00:06:25.550 align:start position:0% break the certian so one FFA to be 00:06:25.550 --> 00:06:27.520 align:start position:0% break the certian so one FFA to be different<00:06:25.880> from<00:06:26.030> F<00:06:26.270> of<00:06:26.419> C<00:06:26.600> and<00:06:26.810> in<00:06:27.140> this<00:06:27.260> case 00:06:27.520 --> 00:06:27.530 align:start position:0% different from F of C and in this case 00:06:27.530 --> 00:06:30.130 align:start position:0% different from F of C and in this case the<00:06:28.160> solver<00:06:28.460> will<00:06:28.610> tell<00:06:28.760> me<00:06:28.940> it's<00:06:29.390> satisfiable 00:06:30.130 --> 00:06:30.140 align:start position:0% the solver will tell me it's satisfiable 00:06:30.140 --> 00:06:32.860 align:start position:0% the solver will tell me it's satisfiable and<00:06:30.350> here<00:06:30.890> are<00:06:31.070> some<00:06:31.370> values<00:06:31.640> and<00:06:31.940> this<00:06:32.720> is 00:06:32.860 --> 00:06:32.870 align:start position:0% and here are some values and this is 00:06:32.870 --> 00:06:35.020 align:start position:0% and here are some values and this is exactly<00:06:33.020> the<00:06:33.500> output<00:06:33.890> that<00:06:34.190> solidity 00:06:35.020 --> 00:06:35.030 align:start position:0% exactly the output that solidity 00:06:35.030 --> 00:06:36.550 align:start position:0% exactly the output that solidity compiler<00:06:35.479> will<00:06:35.630> give<00:06:35.870> you<00:06:36.050> at<00:06:36.200> compile<00:06:36.530> time 00:06:36.550 --> 00:06:36.560 align:start position:0% compiler will give you at compile time 00:06:36.560 --> 00:06:39.730 align:start position:0% compiler will give you at compile time when<00:06:37.490> it's<00:06:37.640> Y<00:06:37.820> when<00:06:38.120> you<00:06:38.240> run<00:06:38.840> exactly<00:06:39.380> that 00:06:39.730 --> 00:06:39.740 align:start position:0% when it's Y when you run exactly that 00:06:39.740 --> 00:06:40.390 align:start position:0% when it's Y when you run exactly that code 00:06:40.390 --> 00:06:40.400 align:start position:0% code 00:06:40.400 --> 00:06:42.820 align:start position:0% code so<00:06:40.760> here<00:06:40.940> we<00:06:41.060> see<00:06:41.270> that<00:06:41.680> compilers<00:06:42.680> say 00:06:42.820 --> 00:06:42.830 align:start position:0% so here we see that compilers say 00:06:42.830 --> 00:06:44.770 align:start position:0% so here we see that compilers say assertion<00:06:43.190> violation<00:06:43.220> happens<00:06:43.850> here<00:06:44.090> for<00:06:44.690> its 00:06:44.770 --> 00:06:44.780 align:start position:0% assertion violation happens here for its 00:06:44.780 --> 00:06:54.070 align:start position:0% assertion violation happens here for its assertion<00:06:45.020> for<00:06:45.410> a1<00:06:46.280> b1<00:06:46.580> c1<00:06:47.199> c0<00:06:48.199> sorry<00:06:52.810> so<00:06:53.810> the 00:06:54.070 --> 00:06:54.080 align:start position:0% assertion for a1 b1 c1 c0 sorry so the 00:06:54.080 --> 00:06:56.650 align:start position:0% assertion for a1 b1 c1 c0 sorry so the SMT<00:06:54.410> checker<00:06:54.680> as<00:06:55.070> a<00:06:55.610> summary<00:06:56.000> after<00:06:56.240> Jack 00:06:56.650 --> 00:06:56.660 align:start position:0% SMT checker as a summary after Jack 00:06:56.660 --> 00:07:00.850 align:start position:0% SMT checker as a summary after Jack symbolizes<00:06:57.229> saw<00:06:57.410> it's<00:06:57.979> a<00:06:58.630> SMT<00:06:59.630> based<00:06:59.900> so<00:07:00.680> we 00:07:00.850 --> 00:07:00.860 align:start position:0% symbolizes saw it's a SMT based so we 00:07:00.860 --> 00:07:03.340 align:start position:0% symbolizes saw it's a SMT based so we use<00:07:00.949> SMT<00:07:01.280> solvers<00:07:01.610> so<00:07:02.000> it's<00:07:02.120> an<00:07:02.180> SMT<00:07:02.570> based<00:07:02.810> it 00:07:03.340 --> 00:07:03.350 align:start position:0% use SMT solvers so it's an SMT based it 00:07:03.350 --> 00:07:04.830 align:start position:0% use SMT solvers so it's an SMT based it smart<00:07:03.590> contract<00:07:03.979> form<00:07:04.190> of<00:07:04.280> verification 00:07:04.830 --> 00:07:04.840 align:start position:0% smart contract form of verification 00:07:04.840 --> 00:07:09.070 align:start position:0% smart contract form of verification framework<00:07:06.370> it's<00:07:07.370> built<00:07:07.699> in<00:07:07.850> a<00:07:07.940> compiler<00:07:08.270> which 00:07:09.070 --> 00:07:09.080 align:start position:0% framework it's built in a compiler which 00:07:09.080 --> 00:07:12.219 align:start position:0% framework it's built in a compiler which is<00:07:09.530> for<00:07:10.520> us<00:07:10.699> one<00:07:11.210> of<00:07:11.240> the<00:07:11.540> one<00:07:11.900> of<00:07:11.990> the<00:07:12.080> big 00:07:12.219 --> 00:07:12.229 align:start position:0% is for us one of the one of the big 00:07:12.229 --> 00:07:16.240 align:start position:0% is for us one of the one of the big advantages<00:07:12.880> compared<00:07:13.880> to<00:07:14.270> other<00:07:15.010> ways<00:07:16.010> to 00:07:16.240 --> 00:07:16.250 align:start position:0% advantages compared to other ways to 00:07:16.250 --> 00:07:18.820 align:start position:0% advantages compared to other ways to formally<00:07:16.580> verify<00:07:16.970> your<00:07:17.150> code<00:07:17.590> the<00:07:18.590> way<00:07:18.770> it 00:07:18.820 --> 00:07:18.830 align:start position:0% formally verify your code the way it 00:07:18.830 --> 00:07:21.070 align:start position:0% formally verify your code the way it works<00:07:19.100> the<00:07:19.340> way<00:07:19.460> the<00:07:19.520> approach<00:07:19.820> our<00:07:20.690> approach 00:07:21.070 --> 00:07:21.080 align:start position:0% works the way the approach our approach 00:07:21.080 --> 00:07:23.290 align:start position:0% works the way the approach our approach is<00:07:21.380> that<00:07:21.410> we<00:07:21.680> encode<00:07:21.979> program<00:07:22.789> logic<00:07:23.150> from 00:07:23.290 --> 00:07:23.300 align:start position:0% is that we encode program logic from 00:07:23.300 --> 00:07:26.650 align:start position:0% is that we encode program logic from solidity<00:07:23.750> into<00:07:24.380> SMT<00:07:24.830> statements<00:07:25.520> and<00:07:25.699> use<00:07:26.270> SMT 00:07:26.650 --> 00:07:26.660 align:start position:0% solidity into SMT statements and use SMT 00:07:26.660 --> 00:07:28.240 align:start position:0% solidity into SMT statements and use SMT solver<00:07:26.960> to<00:07:27.139> run<00:07:27.350> those<00:07:27.530> queries<00:07:27.740> that<00:07:27.979> I<00:07:28.010> just 00:07:28.240 --> 00:07:28.250 align:start position:0% solver to run those queries that I just 00:07:28.250 --> 00:07:30.520 align:start position:0% solver to run those queries that I just mentioned<00:07:28.430> and<00:07:28.880> we<00:07:29.300> use<00:07:29.479> those<00:07:29.720> to<00:07:29.960> check<00:07:30.199> for 00:07:30.520 --> 00:07:30.530 align:start position:0% mentioned and we use those to check for 00:07:30.530 --> 00:07:33.060 align:start position:0% mentioned and we use those to check for assertion<00:07:31.220> failures<00:07:31.639> overflow<00:07:32.180> underflow 00:07:33.060 --> 00:07:33.070 align:start position:0% assertion failures overflow underflow 00:07:33.070 --> 00:07:35.110 align:start position:0% assertion failures overflow underflow trivial<00:07:34.070> conditions<00:07:34.460> and<00:07:34.639> reachable<00:07:34.820> code 00:07:35.110 --> 00:07:35.120 align:start position:0% trivial conditions and reachable code 00:07:35.120 --> 00:07:37.180 align:start position:0% trivial conditions and reachable code and<00:07:35.330> all<00:07:35.510> of<00:07:35.690> that<00:07:35.720> happens<00:07:36.289> automatically 00:07:37.180 --> 00:07:37.190 align:start position:0% and all of that happens automatically 00:07:37.190 --> 00:07:41.140 align:start position:0% and all of that happens automatically when<00:07:37.520> you<00:07:37.910> run<00:07:38.060> the<00:07:38.180> compiler<00:07:40.150> one 00:07:41.140 --> 00:07:41.150 align:start position:0% when you run the compiler one 00:07:41.150 --> 00:07:43.540 align:start position:0% when you run the compiler one characteristic<00:07:41.930> of<00:07:42.080> this<00:07:42.229> approach<00:07:42.620> which<00:07:43.370> is 00:07:43.540 --> 00:07:43.550 align:start position:0% characteristic of this approach which is 00:07:43.550 --> 00:07:45.700 align:start position:0% characteristic of this approach which is close<00:07:43.820> to<00:07:43.930> from<00:07:44.930> the<00:07:45.050> fortification 00:07:45.700 --> 00:07:45.710 align:start position:0% close to from the fortification 00:07:45.710 --> 00:07:47.710 align:start position:0% close to from the fortification community<00:07:46.190> called<00:07:46.820> bounded<00:07:47.210> model<00:07:47.479> checking 00:07:47.710 --> 00:07:47.720 align:start position:0% community called bounded model checking 00:07:47.720 --> 00:07:50.320 align:start position:0% community called bounded model checking is<00:07:48.020> that<00:07:48.320> this<00:07:49.250> approach<00:07:49.400> is<00:07:49.580> sound<00:07:49.940> but<00:07:50.210> not 00:07:50.320 --> 00:07:50.330 align:start position:0% is that this approach is sound but not 00:07:50.330 --> 00:07:54.129 align:start position:0% is that this approach is sound but not complete<00:07:50.870> and<00:07:51.200> what<00:07:51.800> that<00:07:51.950> means<00:07:52.160> is<00:07:52.660> if<00:07:53.660> it's 00:07:54.129 --> 00:07:54.139 align:start position:0% complete and what that means is if it's 00:07:54.139 --> 00:07:56.680 align:start position:0% complete and what that means is if it's sound<00:07:54.470> which<00:07:55.190> this<00:07:55.430> approach<00:07:55.700> is<00:07:55.970> whenever<00:07:56.450> it 00:07:56.680 --> 00:07:56.690 align:start position:0% sound which this approach is whenever it 00:07:56.690 --> 00:07:58.960 align:start position:0% sound which this approach is whenever it says<00:07:56.960> the<00:07:57.650> assertion<00:07:58.039> is<00:07:58.099> safe<00:07:58.430> it<00:07:58.760> is 00:07:58.960 --> 00:07:58.970 align:start position:0% says the assertion is safe it is 00:07:58.970 --> 00:08:02.140 align:start position:0% says the assertion is safe it is actually<00:07:59.539> safe<00:07:59.979> but<00:08:00.979> whenever<00:08:01.220> it<00:08:01.460> says<00:08:01.729> the 00:08:02.140 --> 00:08:02.150 align:start position:0% actually safe but whenever it says the 00:08:02.150 --> 00:08:04.029 align:start position:0% actually safe but whenever it says the assertion<00:08:02.510> is<00:08:02.539> not<00:08:02.780> safe<00:08:03.110> here's<00:08:03.770> a<00:08:03.860> counter 00:08:04.029 --> 00:08:04.039 align:start position:0% assertion is not safe here's a counter 00:08:04.039 --> 00:08:06.879 align:start position:0% assertion is not safe here's a counter example<00:08:04.280> it<00:08:05.120> might<00:08:05.450> be<00:08:05.780> that<00:08:06.260> might<00:08:06.500> be<00:08:06.710> not 00:08:06.879 --> 00:08:06.889 align:start position:0% example it might be that might be not 00:08:06.889 --> 00:08:08.860 align:start position:0% example it might be that might be not true<00:08:07.160> so<00:08:07.400> you<00:08:07.460> might<00:08:07.729> have<00:08:07.970> to<00:08:08.120> verify<00:08:08.300> it<00:08:08.570> and 00:08:08.860 --> 00:08:08.870 align:start position:0% true so you might have to verify it and 00:08:08.870 --> 00:08:12.040 align:start position:0% true so you might have to verify it and see<00:08:09.860> that<00:08:10.130> this<00:08:11.000> this<00:08:11.449> might<00:08:11.660> have<00:08:11.870> been 00:08:12.040 --> 00:08:12.050 align:start position:0% see that this this might have been 00:08:12.050 --> 00:08:14.290 align:start position:0% see that this this might have been caused<00:08:12.349> by<00:08:12.560> an<00:08:13.010> abstraction<00:08:13.460> of<00:08:13.760> some 00:08:14.290 --> 00:08:14.300 align:start position:0% caused by an abstraction of some 00:08:14.300 --> 00:08:16.689 align:start position:0% caused by an abstraction of some unsupported<00:08:15.110> features<00:08:15.470> or<00:08:15.710> functions<00:08:16.280> which 00:08:16.689 --> 00:08:16.699 align:start position:0% unsupported features or functions which 00:08:16.699 --> 00:08:19.930 align:start position:0% unsupported features or functions which is<00:08:16.880> the<00:08:17.030> case<00:08:17.240> for<00:08:17.539> our<00:08:18.260> approach<00:08:18.760> but<00:08:19.760> then 00:08:19.930 --> 00:08:19.940 align:start position:0% is the case for our approach but then 00:08:19.940 --> 00:08:21.610 align:start position:0% is the case for our approach but then being<00:08:20.240> sound<00:08:20.479> but<00:08:20.630> not<00:08:20.690> complete<00:08:21.080> also<00:08:21.440> gives 00:08:21.610 --> 00:08:21.620 align:start position:0% being sound but not complete also gives 00:08:21.620 --> 00:08:23.529 align:start position:0% being sound but not complete also gives advantage<00:08:21.860> that<00:08:22.190> it's<00:08:22.340> pretty<00:08:22.970> fast<00:08:23.270> and 00:08:23.529 --> 00:08:23.539 align:start position:0% advantage that it's pretty fast and 00:08:23.539 --> 00:08:25.150 align:start position:0% advantage that it's pretty fast and light<00:08:23.720> compared<00:08:24.139> to<00:08:24.260> other<00:08:24.349> approaches<00:08:24.800> and 00:08:25.150 --> 00:08:25.160 align:start position:0% light compared to other approaches and 00:08:25.160 --> 00:08:27.070 align:start position:0% light compared to other approaches and it<00:08:25.490> gives<00:08:25.699> useful<00:08:25.880> counter<00:08:26.539> examples<00:08:26.930> because 00:08:27.070 --> 00:08:27.080 align:start position:0% it gives useful counter examples because 00:08:27.080 --> 00:08:29.370 align:start position:0% it gives useful counter examples because it's<00:08:27.440> applied<00:08:27.710> directly<00:08:27.979> on<00:08:28.520> solidity<00:08:29.060> code 00:08:29.370 --> 00:08:29.380 align:start position:0% it's applied directly on solidity code 00:08:29.380 --> 00:08:32.050 align:start position:0% it's applied directly on solidity code instead<00:08:30.380> of<00:08:30.440> EVM<00:08:30.860> bytecode<00:08:31.310> which<00:08:31.340> then<00:08:31.820> you 00:08:32.050 --> 00:08:32.060 align:start position:0% instead of EVM bytecode which then you 00:08:32.060 --> 00:08:33.399 align:start position:0% instead of EVM bytecode which then you would<00:08:32.180> have<00:08:32.270> to<00:08:32.479> map<00:08:32.659> back<00:08:32.930> to<00:08:32.959> solidity 00:08:33.399 --> 00:08:33.409 align:start position:0% would have to map back to solidity 00:08:33.409 --> 00:08:36.880 align:start position:0% would have to map back to solidity program<00:08:34.279> variables<00:08:34.700> which<00:08:35.890> doesn't 00:08:36.880 --> 00:08:36.890 align:start position:0% program variables which doesn't 00:08:36.890 --> 00:08:40.560 align:start position:0% program variables which doesn't necessarily<00:08:37.430> work<00:08:38.709> so<00:08:39.709> here's<00:08:40.010> some<00:08:40.219> other 00:08:40.560 --> 00:08:40.570 align:start position:0% necessarily work so here's some other 00:08:40.570 --> 00:08:45.370 align:start position:0% necessarily work so here's some other frameworks<00:08:41.570> that<00:08:41.990> have<00:08:42.169> been<00:08:43.089> already<00:08:44.380> in 00:08:45.370 --> 00:08:45.380 align:start position:0% frameworks that have been already in 00:08:45.380 --> 00:08:49.150 align:start position:0% frameworks that have been already in indigo<00:08:46.070> system<00:08:46.520> for<00:08:46.790> for<00:08:47.120> some<00:08:47.270> time<00:08:47.770> in<00:08:48.770> EVM 00:08:49.150 --> 00:08:49.160 align:start position:0% indigo system for for some time in EVM 00:08:49.160 --> 00:08:52.090 align:start position:0% indigo system for for some time in EVM formal<00:08:49.490> semantics<00:08:49.970> I'd<00:08:50.420> have<00:08:50.810> Isabel<00:08:51.440> and<00:08:51.620> KVM 00:08:52.090 --> 00:08:52.100 align:start position:0% formal semantics I'd have Isabel and KVM 00:08:52.100 --> 00:08:53.920 align:start position:0% formal semantics I'd have Isabel and KVM which<00:08:52.910> are 00:08:53.920 --> 00:08:53.930 align:start position:0% which are 00:08:53.930 --> 00:08:55.950 align:start position:0% which are or<00:08:54.140> KVM<00:08:54.590> specially<00:08:55.100> is<00:08:55.160> pretty<00:08:55.370> established 00:08:55.950 --> 00:08:55.960 align:start position:0% or KVM specially is pretty established 00:08:55.960 --> 00:08:59.010 align:start position:0% or KVM specially is pretty established as<00:08:56.960> a<00:08:57.020> really<00:08:57.350> good<00:08:57.470> framework<00:08:57.650> for 00:08:59.010 --> 00:08:59.020 align:start position:0% as a really good framework for 00:08:59.020 --> 00:09:01.800 align:start position:0% as a really good framework for fortification<00:09:00.020> of<00:09:00.140> smart<00:09:00.650> contracts<00:09:01.130> it's 00:09:01.800 --> 00:09:01.810 align:start position:0% fortification of smart contracts it's 00:09:01.810 --> 00:09:04.720 align:start position:0% fortification of smart contracts it's more<00:09:02.810> expressive<00:09:03.230> but<00:09:04.010> it<00:09:04.100> also<00:09:04.280> means<00:09:04.610> that 00:09:04.720 --> 00:09:04.730 align:start position:0% more expressive but it also means that 00:09:04.730 --> 00:09:07.330 align:start position:0% more expressive but it also means that it<00:09:05.000> it's<00:09:05.570> harder<00:09:06.260> and<00:09:06.410> takes<00:09:06.560> longer<00:09:07.010> to<00:09:07.190> give 00:09:07.330 --> 00:09:07.340 align:start position:0% it it's harder and takes longer to give 00:09:07.340 --> 00:09:09.310 align:start position:0% it it's harder and takes longer to give you<00:09:07.460> proof<00:09:07.670> so<00:09:08.000> these<00:09:08.630> two<00:09:08.780> approaches<00:09:09.170> have 00:09:09.310 --> 00:09:09.320 align:start position:0% you proof so these two approaches have 00:09:09.320 --> 00:09:12.310 align:start position:0% you proof so these two approaches have pros<00:09:09.560> and<00:09:09.590> cons<00:09:10.690> caleb<00:09:11.690> is<00:09:11.810> a<00:09:11.840> really<00:09:12.140> nice 00:09:12.310 --> 00:09:12.320 align:start position:0% pros and cons caleb is a really nice 00:09:12.320 --> 00:09:15.370 align:start position:0% pros and cons caleb is a really nice debugger<00:09:12.680> for<00:09:12.830> a<00:09:12.920> cape<00:09:13.070> for<00:09:13.280> K<00:09:13.460> proofs<00:09:14.020> wit<00:09:15.020> and 00:09:15.370 --> 00:09:15.380 align:start position:0% debugger for a cape for K proofs wit and 00:09:15.380 --> 00:09:16.750 align:start position:0% debugger for a cape for K proofs wit and they<00:09:15.500> will<00:09:15.650> have<00:09:15.800> a<00:09:15.830> workshop<00:09:16.250> tomorrow<00:09:16.460> so 00:09:16.750 --> 00:09:16.760 align:start position:0% they will have a workshop tomorrow so 00:09:16.760 --> 00:09:21.100 align:start position:0% they will have a workshop tomorrow so make<00:09:17.000> sure<00:09:17.030> to<00:09:17.270> check<00:09:17.420> that<00:09:17.450> out<00:09:17.630> for<00:09:19.840> a<00:09:20.840> vm 00:09:21.100 --> 00:09:21.110 align:start position:0% make sure to check that out for a vm 00:09:21.110 --> 00:09:22.630 align:start position:0% make sure to check that out for a vm byte<00:09:21.320> code<00:09:21.530> verification<00:09:21.770> there<00:09:22.370> are<00:09:22.430> tools 00:09:22.630 --> 00:09:22.640 align:start position:0% byte code verification there are tools 00:09:22.640 --> 00:09:24.280 align:start position:0% byte code verification there are tools like<00:09:22.730> int<00:09:23.180> me<00:09:23.300> through<00:09:23.450> in<00:09:23.540> mayan<00:09:23.840> which<00:09:24.020> do 00:09:24.280 --> 00:09:24.290 align:start position:0% like int me through in mayan which do 00:09:24.290 --> 00:09:25.990 align:start position:0% like int me through in mayan which do symbolic<00:09:24.830> execution<00:09:24.920> on<00:09:25.370> the<00:09:25.400> byte<00:09:25.580> code<00:09:25.610> and 00:09:25.990 --> 00:09:26.000 align:start position:0% symbolic execution on the byte code and 00:09:26.000 --> 00:09:29.050 align:start position:0% symbolic execution on the byte code and try<00:09:26.600> to<00:09:26.660> find<00:09:26.960> bugs<00:09:27.200> basically<00:09:28.070> and<00:09:28.280> there 00:09:29.050 --> 00:09:29.060 align:start position:0% try to find bugs basically and there 00:09:29.060 --> 00:09:30.700 align:start position:0% try to find bugs basically and there were<00:09:29.270> other<00:09:29.540> projects<00:09:30.050> that<00:09:30.140> were 00:09:30.700 --> 00:09:30.710 align:start position:0% were other projects that were 00:09:30.710 --> 00:09:32.860 align:start position:0% were other projects that were translating<00:09:31.310> solidity<00:09:31.670> to<00:09:31.810> language<00:09:32.810> that 00:09:32.860 --> 00:09:32.870 align:start position:0% translating solidity to language that 00:09:32.870 --> 00:09:35.650 align:start position:0% translating solidity to language that were<00:09:33.140> whatever<00:09:33.520> verifiable<00:09:34.520> like<00:09:34.700> y3f<00:09:35.390> star 00:09:35.650 --> 00:09:35.660 align:start position:0% were whatever verifiable like y3f star 00:09:35.660 --> 00:09:38.920 align:start position:0% were whatever verifiable like y3f star and<00:09:35.900> zoos<00:09:36.860> that<00:09:36.890> with<00:09:37.880> LLVM<00:09:38.390> if<00:09:38.690> I'm<00:09:38.840> not 00:09:38.920 --> 00:09:38.930 align:start position:0% and zoos that with LLVM if I'm not 00:09:38.930 --> 00:09:43.390 align:start position:0% and zoos that with LLVM if I'm not mistake<00:09:40.990> so<00:09:41.990> how<00:09:42.170> do<00:09:42.230> you<00:09:42.350> use<00:09:42.530> it<00:09:42.710> you<00:09:43.190> just 00:09:43.390 --> 00:09:43.400 align:start position:0% mistake so how do you use it you just 00:09:43.400 --> 00:09:46.120 align:start position:0% mistake so how do you use it you just need<00:09:43.550> one<00:09:43.580> line<00:09:43.910> of<00:09:44.030> code<00:09:44.240> right<00:09:44.590> now<00:09:45.590> it's<00:09:45.980> an 00:09:46.120 --> 00:09:46.130 align:start position:0% need one line of code right now it's an 00:09:46.130 --> 00:09:47.710 align:start position:0% need one line of code right now it's an experimental<00:09:46.370> feature<00:09:46.790> it's<00:09:47.150> a<00:09:47.390> very 00:09:47.710 --> 00:09:47.720 align:start position:0% experimental feature it's a very 00:09:47.720 --> 00:09:49.780 align:start position:0% experimental feature it's a very experimental<00:09:48.080> feature<00:09:48.470> right<00:09:48.680> now<00:09:48.830> so<00:09:49.580> if<00:09:49.700> you 00:09:49.780 --> 00:09:49.790 align:start position:0% experimental feature right now so if you 00:09:49.790 --> 00:09:51.670 align:start position:0% experimental feature right now so if you use<00:09:49.940> it<00:09:50.120> you<00:09:50.150> will<00:09:50.390> find<00:09:50.810> internal<00:09:51.410> compile 00:09:51.670 --> 00:09:51.680 align:start position:0% use it you will find internal compile 00:09:51.680 --> 00:09:53.170 align:start position:0% use it you will find internal compile errors<00:09:52.100> they<00:09:52.280> will<00:09:52.400> find<00:09:52.670> and<00:09:52.820> supported 00:09:53.170 --> 00:09:53.180 align:start position:0% errors they will find and supported 00:09:53.180 --> 00:09:55.180 align:start position:0% errors they will find and supported features<00:09:53.480> and<00:09:53.690> all<00:09:53.750> kind<00:09:53.960> of<00:09:53.990> things<00:09:54.080> but<00:09:54.440> we 00:09:55.180 --> 00:09:55.190 align:start position:0% features and all kind of things but we 00:09:55.190 --> 00:09:59.290 align:start position:0% features and all kind of things but we are<00:09:55.370> working<00:09:55.910> on<00:09:56.150> it<00:09:56.650> to<00:09:57.650> make<00:09:57.800> it<00:09:58.030> of<00:09:59.030> course 00:09:59.290 --> 00:09:59.300 align:start position:0% are working on it to make it of course 00:09:59.300 --> 00:10:00.610 align:start position:0% are working on it to make it of course much<00:09:59.480> more<00:09:59.630> usable<00:10:00.050> and<00:10:00.200> hopefully 00:10:00.610 --> 00:10:00.620 align:start position:0% much more usable and hopefully 00:10:00.620 --> 00:10:05.200 align:start position:0% much more usable and hopefully non-experimental<00:10:01.630> one<00:10:02.630> day<00:10:03.520> but<00:10:04.520> then<00:10:04.730> the 00:10:05.200 --> 00:10:05.210 align:start position:0% non-experimental one day but then the 00:10:05.210 --> 00:10:07.510 align:start position:0% non-experimental one day but then the next<00:10:05.390> question<00:10:05.480> is<00:10:05.840> how<00:10:06.230> do<00:10:06.290> I<00:10:06.770> actually<00:10:07.190> use 00:10:07.510 --> 00:10:07.520 align:start position:0% next question is how do I actually use 00:10:07.520 --> 00:10:11.050 align:start position:0% next question is how do I actually use it<00:10:07.910> so<00:10:08.510> if<00:10:08.660> they<00:10:08.810> just<00:10:09.250> insert<00:10:10.250> this<00:10:10.430> line<00:10:10.730> of 00:10:11.050 --> 00:10:11.060 align:start position:0% it so if they just insert this line of 00:10:11.060 --> 00:10:14.170 align:start position:0% it so if they just insert this line of code<00:10:11.810> there<00:10:12.140> then<00:10:12.470> sure<00:10:13.010> it's<00:10:13.220> gonna<00:10:13.460> enable 00:10:14.170 --> 00:10:14.180 align:start position:0% code there then sure it's gonna enable 00:10:14.180 --> 00:10:16.210 align:start position:0% code there then sure it's gonna enable the<00:10:14.510> run<00:10:14.690> of<00:10:14.810> destiny<00:10:15.200> checker<00:10:15.410> but<00:10:15.650> what<00:10:16.100> is 00:10:16.210 --> 00:10:16.220 align:start position:0% the run of destiny checker but what is 00:10:16.220 --> 00:10:20.650 align:start position:0% the run of destiny checker but what is it<00:10:16.340> what<00:10:16.610> is<00:10:16.640> actually<00:10:17.120> doing<00:10:18.670> so<00:10:19.670> you<00:10:20.420> need<00:10:20.600> to 00:10:20.650 --> 00:10:20.660 align:start position:0% it what is actually doing so you need to 00:10:20.660 --> 00:10:22.210 align:start position:0% it what is actually doing so you need to write<00:10:20.780> formal<00:10:21.110> specifications<00:10:21.710> right<00:10:22.010> so 00:10:22.210 --> 00:10:22.220 align:start position:0% write formal specifications right so 00:10:22.220 --> 00:10:24.130 align:start position:0% write formal specifications right so whenever<00:10:22.400> you<00:10:22.640> prove<00:10:22.910> your<00:10:23.120> program<00:10:23.390> safe<00:10:23.660> you 00:10:24.130 --> 00:10:24.140 align:start position:0% whenever you prove your program safe you 00:10:24.140 --> 00:10:25.870 align:start position:0% whenever you prove your program safe you only<00:10:24.380> prove<00:10:24.590> it<00:10:24.800> with<00:10:25.100> respect<00:10:25.370> to 00:10:25.870 --> 00:10:25.880 align:start position:0% only prove it with respect to 00:10:25.880 --> 00:10:27.340 align:start position:0% only prove it with respect to specification<00:10:26.570> at<00:10:26.690> the<00:10:26.750> regional<00:10:27.080> proving 00:10:27.340 --> 00:10:27.350 align:start position:0% specification at the regional proving 00:10:27.350 --> 00:10:29.980 align:start position:0% specification at the regional proving anything<00:10:27.560> so<00:10:28.460> you<00:10:28.520> need<00:10:28.670> to<00:10:28.760> specify<00:10:28.990> what 00:10:29.980 --> 00:10:29.990 align:start position:0% anything so you need to specify what 00:10:29.990 --> 00:10:31.660 align:start position:0% anything so you need to specify what properties<00:10:30.590> you're<00:10:30.710> actually<00:10:31.040> proving<00:10:31.370> in 00:10:31.660 --> 00:10:31.670 align:start position:0% properties you're actually proving in 00:10:31.670 --> 00:10:34.510 align:start position:0% properties you're actually proving in solidity<00:10:32.510> or<00:10:32.840> with<00:10:33.230> the<00:10:33.320> SMT<00:10:33.650> checker<00:10:33.860> you 00:10:34.510 --> 00:10:34.520 align:start position:0% solidity or with the SMT checker you 00:10:34.520 --> 00:10:36.340 align:start position:0% solidity or with the SMT checker you don't<00:10:34.760> need<00:10:34.880> anything<00:10:35.120> extra<00:10:35.420> you<00:10:35.960> use<00:10:36.200> the 00:10:36.340 --> 00:10:36.350 align:start position:0% don't need anything extra you use the 00:10:36.350 --> 00:10:38.440 align:start position:0% don't need anything extra you use the normal<00:10:36.620> require<00:10:36.980> and<00:10:37.280> asserts<00:10:37.610> from<00:10:37.940> the 00:10:38.440 --> 00:10:38.450 align:start position:0% normal require and asserts from the 00:10:38.450 --> 00:10:40.690 align:start position:0% normal require and asserts from the language<00:10:38.720> itself<00:10:38.990> so<00:10:39.680> requires<00:10:40.220> and<00:10:40.400> asserts 00:10:40.690 --> 00:10:40.700 align:start position:0% language itself so requires and asserts 00:10:40.700 --> 00:10:43.930 align:start position:0% language itself so requires and asserts in<00:10:41.660> a<00:10:41.810> compiler<00:10:42.170> or<00:10:42.740> translated<00:10:43.310> into<00:10:43.490> runtime 00:10:43.930 --> 00:10:43.940 align:start position:0% in a compiler or translated into runtime 00:10:43.940 --> 00:10:45.850 align:start position:0% in a compiler or translated into runtime checks<00:10:44.240> right<00:10:44.750> when<00:10:45.260> it's<00:10:45.380> compiled<00:10:45.800> to 00:10:45.850 --> 00:10:45.860 align:start position:0% checks right when it's compiled to 00:10:45.860 --> 00:10:50.590 align:start position:0% checks right when it's compiled to bytecode<00:10:46.360> but<00:10:47.360> here<00:10:47.630> in<00:10:47.780> the<00:10:48.440> SMT<00:10:49.250> checker<00:10:49.600> we 00:10:50.590 --> 00:10:50.600 align:start position:0% bytecode but here in the SMT checker we 00:10:50.600 --> 00:10:53.020 align:start position:0% bytecode but here in the SMT checker we use<00:10:51.050> them<00:10:51.320> as<00:10:51.650> as<00:10:52.370> the<00:10:52.700> formal<00:10:52.940> specification 00:10:53.020 --> 00:10:53.030 align:start position:0% use them as as the formal specification 00:10:53.030 --> 00:10:55.800 align:start position:0% use them as as the formal specification so<00:10:53.660> ease<00:10:53.810> requires<00:10:54.230> as<00:10:54.770> assumptions<00:10:55.280> and 00:10:55.800 --> 00:10:55.810 align:start position:0% so ease requires as assumptions and 00:10:55.810 --> 00:10:58.540 align:start position:0% so ease requires as assumptions and asserts<00:10:56.810> as<00:10:57.080> verification<00:10:57.410> targets<00:10:57.980> so 00:10:58.540 --> 00:10:58.550 align:start position:0% asserts as verification targets so 00:10:58.550 --> 00:11:00.340 align:start position:0% asserts as verification targets so whatever<00:10:58.910> conditions<00:10:59.720> you<00:10:59.870> write<00:11:00.080> in<00:11:00.290> a 00:11:00.340 --> 00:11:00.350 align:start position:0% whatever conditions you write in a 00:11:00.350 --> 00:11:02.470 align:start position:0% whatever conditions you write in a require<00:11:00.680> the<00:11:01.400> SMT<00:11:01.700> checker<00:11:01.880> has<00:11:02.000> been<00:11:02.150> assume 00:11:02.470 --> 00:11:02.480 align:start position:0% require the SMT checker has been assume 00:11:02.480 --> 00:11:05.680 align:start position:0% require the SMT checker has been assume it's<00:11:02.690> true<00:11:02.930> and<00:11:04.030> whatever<00:11:05.030> you<00:11:05.210> write<00:11:05.390> has<00:11:05.540> had 00:11:05.680 --> 00:11:05.690 align:start position:0% it's true and whatever you write has had 00:11:05.690 --> 00:11:09.570 align:start position:0% it's true and whatever you write has had an<00:11:05.810> assert<00:11:06.110> it's<00:11:06.650> going<00:11:06.890> to<00:11:06.950> try<00:11:07.130> to<00:11:07.190> prove 00:11:09.570 --> 00:11:09.580 align:start position:0% 00:11:09.580 --> 00:11:13.660 align:start position:0% okay<00:11:10.580> so<00:11:11.290> how<00:11:12.290> to<00:11:12.350> use<00:11:12.560> a<00:11:12.620> require<00:11:12.920> actually<00:11:13.370> so 00:11:13.660 --> 00:11:13.670 align:start position:0% okay so how to use a require actually so 00:11:13.670 --> 00:11:16.600 align:start position:0% okay so how to use a require actually so there's<00:11:14.030> a<00:11:14.090> lot<00:11:14.300> of<00:11:14.330> debate<00:11:15.430> for<00:11:16.430> quite<00:11:16.580> a 00:11:16.600 --> 00:11:16.610 align:start position:0% there's a lot of debate for quite a 00:11:16.610 --> 00:11:18.490 align:start position:0% there's a lot of debate for quite a while<00:11:16.820> already<00:11:16.850> on<00:11:17.330> requires<00:11:18.050> and<00:11:18.230> asserts 00:11:18.490 --> 00:11:18.500 align:start position:0% while already on requires and asserts 00:11:18.500 --> 00:11:21.790 align:start position:0% while already on requires and asserts and<00:11:18.830> when<00:11:19.280> to<00:11:19.430> use<00:11:19.460> each<00:11:19.760> or<00:11:20.090> what<00:11:21.050> it<00:11:21.410> what 00:11:21.790 --> 00:11:21.800 align:start position:0% and when to use each or what it what 00:11:21.800 --> 00:11:24.010 align:start position:0% and when to use each or what it what which<00:11:21.980> one<00:11:22.160> means<00:11:22.280> so<00:11:23.150> I<00:11:23.180> just<00:11:23.480> copied<00:11:23.810> it<00:11:23.900> I'm 00:11:24.010 --> 00:11:24.020 align:start position:0% which one means so I just copied it I'm 00:11:24.020 --> 00:11:25.840 align:start position:0% which one means so I just copied it I'm gonna<00:11:24.140> read<00:11:24.350> it<00:11:24.380> from<00:11:24.620> solute<00:11:24.950> docks<00:11:25.160> the 00:11:25.840 --> 00:11:25.850 align:start position:0% gonna read it from solute docks the 00:11:25.850 --> 00:11:27.550 align:start position:0% gonna read it from solute docks the require<00:11:26.150> function<00:11:26.450> should<00:11:26.810> be<00:11:26.870> used<00:11:27.410> to 00:11:27.550 --> 00:11:27.560 align:start position:0% require function should be used to 00:11:27.560 --> 00:11:30.460 align:start position:0% require function should be used to ensure<00:11:27.860> valid<00:11:28.250> conditions<00:11:28.760> on<00:11:29.150> inputs<00:11:30.140> and 00:11:30.460 --> 00:11:30.470 align:start position:0% ensure valid conditions on inputs and 00:11:30.470 --> 00:11:32.830 align:start position:0% ensure valid conditions on inputs and contracts<00:11:31.070> a<00:11:31.190> tribals<00:11:31.640> or<00:11:31.940> to<00:11:32.480> validate 00:11:32.830 --> 00:11:32.840 align:start position:0% contracts a tribals or to validate 00:11:32.840 --> 00:11:35.200 align:start position:0% contracts a tribals or to validate return<00:11:33.260> values<00:11:33.710> from<00:11:33.860> calls<00:11:34.190> to<00:11:34.790> external 00:11:35.200 --> 00:11:35.210 align:start position:0% return values from calls to external 00:11:35.210 --> 00:11:37.510 align:start position:0% return values from calls to external contracts<00:11:35.690> so<00:11:36.350> here<00:11:36.650> in<00:11:36.800> this<00:11:36.890> example<00:11:37.220> we 00:11:37.510 --> 00:11:37.520 align:start position:0% contracts so here in this example we 00:11:37.520 --> 00:11:40.630 align:start position:0% contracts so here in this example we have<00:11:37.550> a<00:11:37.730> contract<00:11:38.360> that<00:11:38.600> has<00:11:39.460> stayed<00:11:40.460> forever 00:11:40.630 --> 00:11:40.640 align:start position:0% have a contract that has stayed forever 00:11:40.640 --> 00:11:43.410 align:start position:0% have a contract that has stayed forever a<00:11:40.940> a<00:11:41.180> bunch<00:11:41.420> of<00:11:41.510> functions<00:11:41.930> G<00:11:42.290> and<00:11:42.410> H<00:11:42.560> which 00:11:43.410 --> 00:11:43.420 align:start position:0% a a bunch of functions G and H which 00:11:43.420 --> 00:11:45.730 align:start position:0% a a bunch of functions G and H which suppose<00:11:44.420> like<00:11:44.720> that<00:11:45.050> we<00:11:45.260> don't<00:11:45.500> know<00:11:45.560> right 00:11:45.730 --> 00:11:45.740 align:start position:0% suppose like that we don't know right 00:11:45.740 --> 00:11:47.140 align:start position:0% suppose like that we don't know right now<00:11:45.890> what<00:11:46.070> they<00:11:46.160> do<00:11:46.310> and<00:11:46.640> we<00:11:46.940> have<00:11:47.060> this 00:11:47.140 --> 00:11:47.150 align:start position:0% now what they do and we have this 00:11:47.150 --> 00:11:51.460 align:start position:0% now what they do and we have this function<00:11:47.330> f<00:11:47.600> that<00:11:47.930> takes<00:11:47.990> an<00:11:48.740> integer<00:11:49.300> X<00:11:50.470> so 00:11:51.460 --> 00:11:51.470 align:start position:0% function f that takes an integer X so 00:11:51.470 --> 00:11:54.070 align:start position:0% function f that takes an integer X so here<00:11:51.770> we're<00:11:52.070> using<00:11:52.100> requires<00:11:52.900> requires<00:11:53.900> two 00:11:54.070 --> 00:11:54.080 align:start position:0% here we're using requires requires two 00:11:54.080 --> 00:11:56.860 align:start position:0% here we're using requires requires two filter<00:11:54.470> values<00:11:55.220> for<00:11:55.490> a<00:11:55.520> and<00:11:55.730> ax<00:11:56.030> right<00:11:56.540> so<00:11:56.750> we 00:11:56.860 --> 00:11:56.870 align:start position:0% filter values for a and ax right so we 00:11:56.870 --> 00:11:59.020 align:start position:0% filter values for a and ax right so we want<00:11:57.050> for<00:11:57.380> some<00:11:57.530> reason<00:11:57.800> a<00:11:57.950> to<00:11:58.280> be<00:11:58.520> 0<00:11:58.730> and<00:11:58.880> ax 00:11:59.020 --> 00:11:59.030 align:start position:0% want for some reason a to be 0 and ax 00:11:59.030 --> 00:12:01.450 align:start position:0% want for some reason a to be 0 and ax would<00:11:59.210> be<00:11:59.270> less<00:11:59.600> than<00:11:59.780> 100<00:12:00.170> then<00:12:00.350> we<00:12:00.740> sum<00:12:01.100> both 00:12:01.450 --> 00:12:01.460 align:start position:0% would be less than 100 then we sum both 00:12:01.460 --> 00:12:06.100 align:start position:0% would be less than 100 then we sum both we<00:12:01.730> put<00:12:01.910> it<00:12:02.030> in<00:12:02.090> a<00:12:02.270> and<00:12:02.540> then<00:12:03.140> after<00:12:04.070> that<00:12:04.660> we<00:12:05.660> we 00:12:06.100 --> 00:12:06.110 align:start position:0% we put it in a and then after that we we 00:12:06.110 --> 00:12:10.150 align:start position:0% we put it in a and then after that we we know<00:12:06.460> that<00:12:07.460> al<00:12:08.420> as<00:12:08.570> then<00:12:09.050> and<00:12:09.410> 100<00:12:09.860> is<00:12:09.950> true 00:12:10.150 --> 00:12:10.160 align:start position:0% know that al as then and 100 is true 00:12:10.160 --> 00:12:12.910 align:start position:0% know that al as then and 100 is true right<00:12:10.490> because<00:12:10.970> of<00:12:11.330> the<00:12:11.660> requires<00:12:11.960> before<00:12:12.380> so 00:12:12.910 --> 00:12:12.920 align:start position:0% right because of the requires before so 00:12:12.920 --> 00:12:14.440 align:start position:0% right because of the requires before so if<00:12:13.010> you<00:12:13.070> want<00:12:13.220> to<00:12:13.280> prove<00:12:13.460> that<00:12:13.520> the<00:12:14.210> last 00:12:14.440 --> 00:12:14.450 align:start position:0% if you want to prove that the last 00:12:14.450 --> 00:12:15.490 align:start position:0% if you want to prove that the last statement<00:12:14.840> should<00:12:14.900> actually<00:12:15.080> have<00:12:15.350> been<00:12:15.470> a 00:12:15.490 --> 00:12:15.500 align:start position:0% statement should actually have been a 00:12:15.500 --> 00:12:17.530 align:start position:0% statement should actually have been a require<00:12:15.830> sorry<00:12:16.490> in<00:12:16.610> a<00:12:16.670> certain<00:12:17.060> order<00:12:17.150> require 00:12:17.530 --> 00:12:17.540 align:start position:0% require sorry in a certain order require 00:12:17.540 --> 00:12:19.330 align:start position:0% require sorry in a certain order require because<00:12:18.290> it<00:12:18.380> requires<00:12:18.680> just<00:12:18.830> going<00:12:19.100> to<00:12:19.160> assume 00:12:19.330 --> 00:12:19.340 align:start position:0% because it requires just going to assume 00:12:19.340 --> 00:12:21.130 align:start position:0% because it requires just going to assume it<00:12:19.550> and<00:12:19.910> with<00:12:20.120> this<00:12:20.240> with<00:12:20.480> the<00:12:20.630> assert<00:12:20.900> we're 00:12:21.130 --> 00:12:21.140 align:start position:0% it and with this with the assert we're 00:12:21.140 --> 00:12:23.260 align:start position:0% it and with this with the assert we're actually<00:12:21.320> using<00:12:21.650> passed<00:12:22.400> knowledge<00:12:22.820> to<00:12:23.000> prove 00:12:23.260 --> 00:12:23.270 align:start position:0% actually using passed knowledge to prove 00:12:23.270 --> 00:12:25.750 align:start position:0% actually using passed knowledge to prove a<00:12:23.540> new<00:12:23.960> property<00:12:24.350> about<00:12:25.100> your<00:12:25.280> code<00:12:25.490> in<00:12:25.640> the 00:12:25.750 --> 00:12:25.760 align:start position:0% a new property about your code in the 00:12:25.760 --> 00:12:28.630 align:start position:0% a new property about your code in the end<00:12:25.850> of<00:12:25.940> the<00:12:26.060> function<00:12:27.370> so<00:12:28.370> what<00:12:28.550> about 00:12:28.630 --> 00:12:28.640 align:start position:0% end of the function so what about 00:12:28.640 --> 00:12:31.390 align:start position:0% end of the function so what about asserts<00:12:29.320> the<00:12:30.320> third<00:12:30.530> function<00:12:30.800> should<00:12:31.160> only 00:12:31.390 --> 00:12:31.400 align:start position:0% asserts the third function should only 00:12:31.400 --> 00:12:34.240 align:start position:0% asserts the third function should only be<00:12:31.700> used<00:12:31.940> to<00:12:32.210> test<00:12:32.480> for<00:12:32.660> internal<00:12:33.650> errors<00:12:34.010> and 00:12:34.240 --> 00:12:34.250 align:start position:0% be used to test for internal errors and 00:12:34.250 --> 00:12:35.560 align:start position:0% be used to test for internal errors and to<00:12:34.340> check<00:12:34.580> invariants<00:12:35.180> a<00:12:35.240> properly 00:12:35.560 --> 00:12:35.570 align:start position:0% to check invariants a properly 00:12:35.570 --> 00:12:37.690 align:start position:0% to check invariants a properly functioning<00:12:35.810> code<00:12:36.320> should<00:12:36.650> never<00:12:36.980> reach<00:12:37.520> a 00:12:37.690 --> 00:12:37.700 align:start position:0% functioning code should never reach a 00:12:37.700 --> 00:12:39.280 align:start position:0% functioning code should never reach a fail<00:12:37.910> in<00:12:38.060> a<00:12:38.120> search<00:12:38.330> statement<00:12:38.870> and<00:12:38.990> this<00:12:39.140> is 00:12:39.280 --> 00:12:39.290 align:start position:0% fail in a search statement and this is 00:12:39.290 --> 00:12:41.230 align:start position:0% fail in a search statement and this is really<00:12:39.530> important<00:12:39.920> if<00:12:40.250> this<00:12:40.670> happens<00:12:41.060> there's 00:12:41.230 --> 00:12:41.240 align:start position:0% really important if this happens there's 00:12:41.240 --> 00:12:43.030 align:start position:0% really important if this happens there's a<00:12:41.300> bug<00:12:41.600> in<00:12:41.630> our<00:12:41.840> contract<00:12:42.350> which<00:12:42.740> you<00:12:42.860> should 00:12:43.030 --> 00:12:43.040 align:start position:0% a bug in our contract which you should 00:12:43.040 --> 00:12:46.660 align:start position:0% a bug in our contract which you should fix<00:12:43.780> same<00:12:44.780> example<00:12:45.290> now<00:12:45.830> just<00:12:46.160> using<00:12:46.310> asserts 00:12:46.660 --> 00:12:46.670 align:start position:0% fix same example now just using asserts 00:12:46.670 --> 00:12:48.400 align:start position:0% fix same example now just using asserts everywhere 00:12:48.400 --> 00:12:48.410 align:start position:0% everywhere 00:12:48.410 --> 00:12:50.770 align:start position:0% everywhere can<00:12:49.280> we<00:12:49.400> assert<00:12:49.700> a<00:12:49.940> equals<00:12:50.240> zero<00:12:50.390> over<00:12:50.630> there 00:12:50.770 --> 00:12:50.780 align:start position:0% can we assert a equals zero over there 00:12:50.780 --> 00:12:54.040 align:start position:0% can we assert a equals zero over there very<00:12:51.760> likely<00:12:52.760> not<00:12:52.910> right<00:12:53.330> of<00:12:53.630> course<00:12:53.960> it 00:12:54.040 --> 00:12:54.050 align:start position:0% very likely not right of course it 00:12:54.050 --> 00:12:56.260 align:start position:0% very likely not right of course it depends<00:12:54.320> on<00:12:54.470> what<00:12:54.800> what<00:12:55.220> G<00:12:55.460> and<00:12:55.580> H<00:12:55.760> are<00:12:56.000> doing 00:12:56.260 --> 00:12:56.270 align:start position:0% depends on what what G and H are doing 00:12:56.270 --> 00:12:58.720 align:start position:0% depends on what what G and H are doing but<00:12:56.900> if<00:12:57.470> we<00:12:57.800> don't<00:12:58.010> really<00:12:58.220> know<00:12:58.430> what<00:12:58.610> it's 00:12:58.720 --> 00:12:58.730 align:start position:0% but if we don't really know what it's 00:12:58.730 --> 00:12:59.400 align:start position:0% but if we don't really know what it's doing 00:12:59.400 --> 00:12:59.410 align:start position:0% doing 00:12:59.410 --> 00:13:02.560 align:start position:0% doing we<00:13:00.410> cannot<00:13:00.650> say<00:13:00.890> assert<00:13:01.220> a<00:13:01.490> equals<00:13:02.150> a<00:13:02.270> because 00:13:02.560 --> 00:13:02.570 align:start position:0% we cannot say assert a equals a because 00:13:02.570 --> 00:13:04.140 align:start position:0% we cannot say assert a equals a because they<00:13:02.720> can<00:13:02.900> be<00:13:03.020> whatever<00:13:03.290> right<00:13:03.680> and 00:13:04.140 --> 00:13:04.150 align:start position:0% they can be whatever right and 00:13:04.150 --> 00:13:07.060 align:start position:0% they can be whatever right and especially<00:13:05.150> for<00:13:05.750> ax<00:13:05.990> here<00:13:06.380> if<00:13:06.470> you<00:13:06.560> say<00:13:06.710> assert 00:13:07.060 --> 00:13:07.070 align:start position:0% especially for ax here if you say assert 00:13:07.070 --> 00:13:09.430 align:start position:0% especially for ax here if you say assert ax<00:13:07.340> less<00:13:07.580> than<00:13:07.730> 100<00:13:08.150> it's<00:13:08.840> a<00:13:08.990> public<00:13:09.290> function 00:13:09.430 --> 00:13:09.440 align:start position:0% ax less than 100 it's a public function 00:13:09.440 --> 00:13:12.220 align:start position:0% ax less than 100 it's a public function so<00:13:09.890> anyone<00:13:10.490> can<00:13:11.090> call<00:13:11.270> this<00:13:11.420> function<00:13:11.660> with<00:13:11.990> x 00:13:12.220 --> 00:13:12.230 align:start position:0% so anyone can call this function with x 00:13:12.230 --> 00:13:14.770 align:start position:0% so anyone can call this function with x equals<00:13:12.800> to<00:13:12.950> a<00:13:12.980> hundred<00:13:13.430> and<00:13:13.640> your<00:13:14.360> assertions 00:13:14.770 --> 00:13:14.780 align:start position:0% equals to a hundred and your assertions 00:13:14.780 --> 00:13:17.080 align:start position:0% equals to a hundred and your assertions already<00:13:15.050> wrong<00:13:15.230> right<00:13:16.190> so<00:13:16.640> this<00:13:16.760> is<00:13:16.880> really 00:13:17.080 --> 00:13:17.090 align:start position:0% already wrong right so this is really 00:13:17.090 --> 00:13:18.370 align:start position:0% already wrong right so this is really important<00:13:17.420> to<00:13:17.480> notice<00:13:17.750> like<00:13:17.960> you<00:13:18.050> should<00:13:18.200> only 00:13:18.370 --> 00:13:18.380 align:start position:0% important to notice like you should only 00:13:18.380 --> 00:13:21.120 align:start position:0% important to notice like you should only assert<00:13:18.800> things<00:13:19.190> that<00:13:20.120> you're<00:13:20.540> really 00:13:21.120 --> 00:13:21.130 align:start position:0% assert things that you're really 00:13:21.130 --> 00:13:24.540 align:start position:0% assert things that you're really are<00:13:21.430> true<00:13:21.880> at<00:13:22.150> that<00:13:22.300> moment<00:13:22.750> for<00:13:23.200> every<00:13:24.100> single 00:13:24.540 --> 00:13:24.550 align:start position:0% are true at that moment for every single 00:13:24.550 --> 00:13:29.180 align:start position:0% are true at that moment for every single execution<00:13:24.970> path<00:13:25.360> that<00:13:25.900> rich<00:13:26.200> is<00:13:26.470> that<00:13:26.500> point 00:13:29.180 --> 00:13:29.190 align:start position:0% 00:13:29.190 --> 00:13:32.670 align:start position:0% and<00:13:30.190> here<00:13:30.840> the<00:13:31.840> assertion<00:13:32.110> is<00:13:32.170> correctly 00:13:32.670 --> 00:13:32.680 align:start position:0% and here the assertion is correctly 00:13:32.680 --> 00:13:33.990 align:start position:0% and here the assertion is correctly placed<00:13:33.010> at<00:13:33.190> the<00:13:33.280> end<00:13:33.400> because<00:13:33.790> the<00:13:33.910> new 00:13:33.990 --> 00:13:34.000 align:start position:0% placed at the end because the new 00:13:34.000 --> 00:13:48.360 align:start position:0% placed at the end because the new property<00:13:34.360> are<00:13:34.450> proven<00:13:34.920> yeah<00:13:46.740> yeah<00:13:47.740> this 00:13:48.360 --> 00:13:48.370 align:start position:0% property are proven yeah yeah this 00:13:48.370 --> 00:13:50.490 align:start position:0% property are proven yeah yeah this moment<00:13:48.760> yeah<00:13:48.940> so<00:13:49.240> for<00:13:49.510> example<00:13:49.780> we<00:13:49.870> have<00:13:50.140> I'm 00:13:50.490 --> 00:13:50.500 align:start position:0% moment yeah so for example we have I'm 00:13:50.500 --> 00:13:53.520 align:start position:0% moment yeah so for example we have I'm gonna<00:13:50.770> talk<00:13:50.950> about<00:13:51.160> this<00:13:51.280> later<00:13:51.940> but<00:13:52.200> if<00:13:53.200> you 00:13:53.520 --> 00:13:53.530 align:start position:0% gonna talk about this later but if you 00:13:53.530 --> 00:13:55.200 align:start position:0% gonna talk about this later but if you call<00:13:54.190> an<00:13:54.340> external<00:13:54.520> function<00:13:54.880> for<00:13:55.180> example 00:13:55.200 --> 00:13:55.210 align:start position:0% call an external function for example 00:13:55.210 --> 00:13:57.150 align:start position:0% call an external function for example which<00:13:55.600> don't<00:13:55.810> have<00:13:55.960> control<00:13:56.470> over<00:13:56.560> or<00:13:56.950> they 00:13:57.150 --> 00:13:57.160 align:start position:0% which don't have control over or they 00:13:57.160 --> 00:13:59.190 align:start position:0% which don't have control over or they know<00:13:57.280> the<00:13:57.400> code<00:13:57.580> then<00:13:58.240> when<00:13:58.660> a<00:13:58.690> function<00:13:59.020> comes 00:13:59.190 --> 00:13:59.200 align:start position:0% know the code then when a function comes 00:13:59.200 --> 00:14:01.560 align:start position:0% know the code then when a function comes back<00:13:59.440> we<00:13:59.650> have<00:13:59.800> to<00:14:00.040> reset<00:14:00.430> all<00:14:00.880> knowledge 00:14:01.560 --> 00:14:01.570 align:start position:0% back we have to reset all knowledge 00:14:01.570 --> 00:14:03.510 align:start position:0% back we have to reset all knowledge about<00:14:01.750> state<00:14:01.960> variables<00:14:02.350> right<00:14:02.680> because<00:14:03.040> you 00:14:03.510 --> 00:14:03.520 align:start position:0% about state variables right because you 00:14:03.520 --> 00:14:06.180 align:start position:0% about state variables right because you might<00:14:03.700> have<00:14:04.080> this<00:14:05.080> contractor<00:14:05.680> called<00:14:05.890> might 00:14:06.180 --> 00:14:06.190 align:start position:0% might have this contractor called might 00:14:06.190 --> 00:14:07.770 align:start position:0% might have this contractor called might have<00:14:06.400> called<00:14:06.610> your<00:14:06.730> contract<00:14:07.120> back<00:14:07.300> which 00:14:07.770 --> 00:14:07.780 align:start position:0% have called your contract back which 00:14:07.780 --> 00:14:09.660 align:start position:0% have called your contract back which changed<00:14:08.140> a<00:14:08.350> so<00:14:08.920> you<00:14:08.980> can't<00:14:09.160> really<00:14:09.400> keep<00:14:09.520> the 00:14:09.660 --> 00:14:09.670 align:start position:0% changed a so you can't really keep the 00:14:09.670 --> 00:14:10.820 align:start position:0% changed a so you can't really keep the knowledge<00:14:09.940> about<00:14:10.150> it 00:14:10.820 --> 00:14:10.830 align:start position:0% knowledge about it 00:14:10.830 --> 00:14:14.850 align:start position:0% knowledge about it but<00:14:11.830> yeah<00:14:12.700> but<00:14:12.850> modular<00:14:13.240> verification<00:14:13.750> one<00:14:14.740> of 00:14:14.850 --> 00:14:14.860 align:start position:0% but yeah but modular verification one of 00:14:14.860 --> 00:14:16.260 align:start position:0% but yeah but modular verification one of the<00:14:14.950> research<00:14:15.220> goals<00:14:15.460> that<00:14:15.580> we<00:14:15.730> have<00:14:15.910> is<00:14:16.210> to 00:14:16.260 --> 00:14:16.270 align:start position:0% the research goals that we have is to 00:14:16.270 --> 00:14:18.540 align:start position:0% the research goals that we have is to actually<00:14:16.660> infer<00:14:17.200> properties<00:14:17.230> from<00:14:17.920> different 00:14:18.540 --> 00:14:18.550 align:start position:0% actually infer properties from different 00:14:18.550 --> 00:14:21.480 align:start position:0% actually infer properties from different functions<00:14:18.970> and<00:14:19.180> see<00:14:19.660> what<00:14:19.980> state<00:14:20.980> invariants 00:14:21.480 --> 00:14:21.490 align:start position:0% functions and see what state invariants 00:14:21.490 --> 00:14:22.830 align:start position:0% functions and see what state invariants we<00:14:21.550> can<00:14:21.700> come<00:14:21.850> up<00:14:21.880> with<00:14:22.000> automatically<00:14:22.690> this 00:14:22.830 --> 00:14:22.840 align:start position:0% we can come up with automatically this 00:14:22.840 --> 00:14:25.050 align:start position:0% we can come up with automatically this is<00:14:22.900> not<00:14:23.080> done<00:14:23.350> yet<00:14:23.530> but<00:14:23.800> it's<00:14:24.190> under<00:14:24.550> to<00:14:24.940> do 00:14:25.050 --> 00:14:25.060 align:start position:0% is not done yet but it's under to do 00:14:25.060 --> 00:14:29.010 align:start position:0% is not done yet but it's under to do list<00:14:26.940> what<00:14:27.940> about<00:14:28.030> false<00:14:28.420> positives<00:14:28.600> so<00:14:28.930> I 00:14:29.010 --> 00:14:29.020 align:start position:0% list what about false positives so I 00:14:29.020 --> 00:14:31.620 align:start position:0% list what about false positives so I mentioned<00:14:29.350> earlier<00:14:29.620> that<00:14:30.150> the<00:14:31.150> approach<00:14:31.420> is 00:14:31.620 --> 00:14:31.630 align:start position:0% mentioned earlier that the approach is 00:14:31.630 --> 00:14:34.740 align:start position:0% mentioned earlier that the approach is sound<00:14:31.870> so<00:14:32.650> if<00:14:32.950> it's<00:14:33.100> a<00:14:33.190> safe<00:14:33.520> it's<00:14:33.730> safe<00:14:33.940> but<00:14:34.600> it 00:14:34.740 --> 00:14:34.750 align:start position:0% sound so if it's a safe it's safe but it 00:14:34.750 --> 00:14:36.390 align:start position:0% sound so if it's a safe it's safe but it gives<00:14:34.900> count<00:14:35.170> it<00:14:35.350> gives<00:14:35.530> false<00:14:35.860> positives 00:14:36.390 --> 00:14:36.400 align:start position:0% gives count it gives false positives 00:14:36.400 --> 00:14:39.030 align:start position:0% gives count it gives false positives which<00:14:37.240> is<00:14:37.480> basically<00:14:38.440> false<00:14:38.770> counter 00:14:39.030 --> 00:14:39.040 align:start position:0% which is basically false counter 00:14:39.040 --> 00:14:40.860 align:start position:0% which is basically false counter examples<00:14:39.460> so<00:14:39.670> your<00:14:40.060> assertion<00:14:40.480> might<00:14:40.660> be 00:14:40.860 --> 00:14:40.870 align:start position:0% examples so your assertion might be 00:14:40.870 --> 00:14:43.530 align:start position:0% examples so your assertion might be correct<00:14:41.590> and<00:14:41.830> safe<00:14:42.010> by<00:14:42.760> the<00:14:42.820> tool<00:14:43.090> says<00:14:43.330> it's 00:14:43.530 --> 00:14:43.540 align:start position:0% correct and safe by the tool says it's 00:14:43.540 --> 00:14:46.410 align:start position:0% correct and safe by the tool says it's not<00:14:43.660> safe<00:14:43.720> why<00:14:44.650> does<00:14:44.830> that<00:14:44.860> happen<00:14:45.190> it<00:14:45.970> happens 00:14:46.410 --> 00:14:46.420 align:start position:0% not safe why does that happen it happens 00:14:46.420 --> 00:14:49.170 align:start position:0% not safe why does that happen it happens because<00:14:46.570> we<00:14:47.140> have<00:14:47.290> to<00:14:47.410> abstract<00:14:47.890> the<00:14:48.790> encoding 00:14:49.170 --> 00:14:49.180 align:start position:0% because we have to abstract the encoding 00:14:49.180 --> 00:14:50.940 align:start position:0% because we have to abstract the encoding sometimes<00:14:49.600> so<00:14:49.990> for<00:14:50.140> example<00:14:50.470> for<00:14:50.620> complex 00:14:50.940 --> 00:14:50.950 align:start position:0% sometimes so for example for complex 00:14:50.950 --> 00:14:53.520 align:start position:0% sometimes so for example for complex types<00:14:51.280> and<00:14:51.610> functions<00:14:52.480> say<00:14:53.380> like 00:14:53.520 --> 00:14:53.530 align:start position:0% types and functions say like 00:14:53.530 --> 00:14:57.090 align:start position:0% types and functions say like cryptographic<00:14:53.800> Elections<00:14:54.550> we<00:14:55.390> it's<00:14:56.380> not<00:14:56.530> our 00:14:57.090 --> 00:14:57.100 align:start position:0% cryptographic Elections we it's not our 00:14:57.100 --> 00:14:58.440 align:start position:0% cryptographic Elections we it's not our approach<00:14:57.430> not<00:14:57.640> expressive<00:14:58.060> enough<00:14:58.150> to 00:14:58.440 --> 00:14:58.450 align:start position:0% approach not expressive enough to 00:14:58.450 --> 00:15:00.330 align:start position:0% approach not expressive enough to actually<00:14:58.600> implement<00:14:59.050> it<00:14:59.260> so<00:14:59.470> we<00:14:59.860> have<00:15:00.040> to<00:15:00.220> use 00:15:00.330 --> 00:15:00.340 align:start position:0% actually implement it so we have to use 00:15:00.340 --> 00:15:04.740 align:start position:0% actually implement it so we have to use symbolic<00:15:01.060> variables<00:15:01.660> on<00:15:03.240> on<00:15:04.240> the<00:15:04.360> application 00:15:04.740 --> 00:15:04.750 align:start position:0% symbolic variables on on the application 00:15:04.750 --> 00:15:06.690 align:start position:0% symbolic variables on on the application of<00:15:04.840> the<00:15:04.930> function<00:15:05.290> and<00:15:05.410> that's<00:15:05.860> as<00:15:06.070> far<00:15:06.310> as<00:15:06.550> it 00:15:06.690 --> 00:15:06.700 align:start position:0% of the function and that's as far as it 00:15:06.700 --> 00:15:09.510 align:start position:0% of the function and that's as far as it gets<00:15:07.230> so<00:15:08.230> we<00:15:08.410> don't<00:15:08.590> really<00:15:08.710> know<00:15:08.980> what<00:15:09.250> the 00:15:09.510 --> 00:15:09.520 align:start position:0% gets so we don't really know what the 00:15:09.520 --> 00:15:11.820 align:start position:0% gets so we don't really know what the actual<00:15:09.940> value<00:15:10.210> of<00:15:10.510> the<00:15:11.080> function<00:15:11.260> call<00:15:11.680> is 00:15:11.820 --> 00:15:11.830 align:start position:0% actual value of the function call is 00:15:11.830 --> 00:15:13.800 align:start position:0% actual value of the function call is going<00:15:11.980> to<00:15:12.040> be<00:15:12.190> so<00:15:13.060> in<00:15:13.180> these<00:15:13.360> abstractions 00:15:13.800 --> 00:15:13.810 align:start position:0% going to be so in these abstractions 00:15:13.810 --> 00:15:15.930 align:start position:0% going to be so in these abstractions might<00:15:14.140> lead<00:15:14.320> to<00:15:14.350> false<00:15:14.620> positives<00:15:14.790> also<00:15:15.790> if 00:15:15.930 --> 00:15:15.940 align:start position:0% might lead to false positives also if 00:15:15.940 --> 00:15:17.940 align:start position:0% might lead to false positives also if you<00:15:16.060> call<00:15:16.270> external<00:15:16.900> function<00:15:17.170> if<00:15:17.290> you<00:15:17.320> do<00:15:17.500> if 00:15:17.940 --> 00:15:17.950 align:start position:0% you call external function if you do if 00:15:17.950 --> 00:15:22.260 align:start position:0% you call external function if you do if you<00:15:18.280> yeah<00:15:18.850> I<00:15:18.880> call<00:15:19.480> external<00:15:20.470> functions<00:15:21.270> we 00:15:22.260 --> 00:15:22.270 align:start position:0% you yeah I call external functions we 00:15:22.270 --> 00:15:25.080 align:start position:0% you yeah I call external functions we might<00:15:22.510> have<00:15:22.720> you<00:15:23.020> we<00:15:23.980> do<00:15:24.250> clear<00:15:24.580> the<00:15:24.760> knowledge 00:15:25.080 --> 00:15:25.090 align:start position:0% might have you we do clear the knowledge 00:15:25.090 --> 00:15:28.880 align:start position:0% might have you we do clear the knowledge after<00:15:25.570> the<00:15:26.080> call<00:15:26.290> after<00:15:26.740> a<00:15:27.370> function<00:15:27.670> call<00:15:27.850> so 00:15:28.880 --> 00:15:28.890 align:start position:0% after the call after a function call so 00:15:28.890 --> 00:15:31.829 align:start position:0% after the call after a function call so it<00:15:29.890> might<00:15:30.190> not<00:15:30.550> have<00:15:30.910> been<00:15:30.940> the<00:15:31.270> case<00:15:31.450> that<00:15:31.780> the 00:15:31.829 --> 00:15:31.839 align:start position:0% it might not have been the case that the 00:15:31.839 --> 00:15:34.720 align:start position:0% it might not have been the case that the that<00:15:32.440> state<00:15:33.100> variable<00:15:33.460> a<00:15:33.610> got<00:15:33.970> rewritten 00:15:34.720 --> 00:15:34.730 align:start position:0% that state variable a got rewritten 00:15:34.730 --> 00:15:37.600 align:start position:0% that state variable a got rewritten but<00:15:35.449> you<00:15:35.839> never<00:15:35.959> know<00:15:36.230> so<00:15:36.260> to<00:15:36.589> be<00:15:36.920> safe<00:15:37.160> again 00:15:37.600 --> 00:15:37.610 align:start position:0% but you never know so to be safe again 00:15:37.610 --> 00:15:40.240 align:start position:0% but you never know so to be safe again we<00:15:37.970> have<00:15:38.149> to<00:15:38.420> clear<00:15:38.750> the<00:15:38.839> knowledge<00:15:39.110> also<00:15:39.920> the 00:15:40.240 --> 00:15:40.250 align:start position:0% we have to clear the knowledge also the 00:15:40.250 --> 00:15:42.040 align:start position:0% we have to clear the knowledge also the contract<00:15:40.610> state<00:15:40.760> invariants<00:15:41.269> you<00:15:41.779> as<00:15:41.959> the 00:15:42.040 --> 00:15:42.050 align:start position:0% contract state invariants you as the 00:15:42.050 --> 00:15:43.990 align:start position:0% contract state invariants you as the developer<00:15:42.470> of<00:15:42.500> the<00:15:42.680> contract<00:15:43.100> might<00:15:43.639> know 00:15:43.990 --> 00:15:44.000 align:start position:0% developer of the contract might know 00:15:44.000 --> 00:15:45.790 align:start position:0% developer of the contract might know that<00:15:44.420> certain<00:15:44.779> properties<00:15:45.170> are<00:15:45.350> valid 00:15:45.790 --> 00:15:45.800 align:start position:0% that certain properties are valid 00:15:45.800 --> 00:15:47.889 align:start position:0% that certain properties are valid throughout<00:15:46.010> your<00:15:46.190> contract<00:15:46.639> but<00:15:47.329> the<00:15:47.570> SMT 00:15:47.889 --> 00:15:47.899 align:start position:0% throughout your contract but the SMT 00:15:47.899 --> 00:15:50.939 align:start position:0% throughout your contract but the SMT checker<00:15:48.110> is<00:15:48.230> not<00:15:48.410> yet<00:15:49.279> smart<00:15:49.940> enough<00:15:50.180> to 00:15:50.939 --> 00:15:50.949 align:start position:0% checker is not yet smart enough to 00:15:50.949 --> 00:15:55.800 align:start position:0% checker is not yet smart enough to deduce<00:15:51.949> those<00:15:52.220> properties<00:15:52.610> automatically<00:15:53.120> so 00:15:55.800 --> 00:15:55.810 align:start position:0% 00:15:55.810 --> 00:15:58.750 align:start position:0% and<00:15:56.810> one<00:15:57.500> point<00:15:57.740> that<00:15:57.829> I<00:15:57.889> wanted<00:15:58.220> to<00:15:58.279> mention 00:15:58.750 --> 00:15:58.760 align:start position:0% and one point that I wanted to mention 00:15:58.760 --> 00:16:00.670 align:start position:0% and one point that I wanted to mention in<00:15:59.120> this<00:15:59.240> talk<00:15:59.449> is<00:15:59.720> you<00:15:59.779> can<00:16:00.170> actually<00:16:00.380> help 00:16:00.670 --> 00:16:00.680 align:start position:0% in this talk is you can actually help 00:16:00.680 --> 00:16:03.639 align:start position:0% in this talk is you can actually help the<00:16:00.920> SMT<00:16:01.310> checker<00:16:01.519> you<00:16:01.670> can<00:16:01.820> help<00:16:02.029> the<00:16:02.720> tool<00:16:02.930> to 00:16:03.639 --> 00:16:03.649 align:start position:0% the SMT checker you can help the tool to 00:16:03.649 --> 00:16:06.519 align:start position:0% the SMT checker you can help the tool to actually<00:16:04.220> find<00:16:04.459> it<00:16:04.610> proofs<00:16:04.820> and<00:16:05.199> it's<00:16:06.199> a<00:16:06.320> very 00:16:06.519 --> 00:16:06.529 align:start position:0% actually find it proofs and it's a very 00:16:06.529 --> 00:16:10.150 align:start position:0% actually find it proofs and it's a very simple<00:16:06.800> way<00:16:07.040> to<00:16:07.070> do<00:16:07.370> it<00:16:07.550> you<00:16:08.240> can<00:16:09.040> flood<00:16:10.040> your 00:16:10.150 --> 00:16:10.160 align:start position:0% simple way to do it you can flood your 00:16:10.160 --> 00:16:12.720 align:start position:0% simple way to do it you can flood your code<00:16:10.399> with<00:16:10.550> requires<00:16:10.899> so<00:16:11.899> every<00:16:12.170> assumption 00:16:12.720 --> 00:16:12.730 align:start position:0% code with requires so every assumption 00:16:12.730 --> 00:16:16.120 align:start position:0% code with requires so every assumption even<00:16:13.730> very<00:16:14.720> simple<00:16:14.899> things<00:16:15.320> that<00:16:15.589> you<00:16:15.860> know 00:16:16.120 --> 00:16:16.130 align:start position:0% even very simple things that you know 00:16:16.130 --> 00:16:20.470 align:start position:0% even very simple things that you know are<00:16:16.339> true<00:16:16.370> at<00:16:16.880> that<00:16:17.329> point<00:16:18.519> even<00:16:19.519> if<00:16:19.940> it's<00:16:20.180> if 00:16:20.470 --> 00:16:20.480 align:start position:0% are true at that point even if it's if 00:16:20.480 --> 00:16:22.329 align:start position:0% are true at that point even if it's if even<00:16:20.870> if<00:16:20.959> it<00:16:21.079> might<00:16:21.290> sound<00:16:21.560> redundant<00:16:22.070> to<00:16:22.220> you 00:16:22.329 --> 00:16:22.339 align:start position:0% even if it might sound redundant to you 00:16:22.339 --> 00:16:24.910 align:start position:0% even if it might sound redundant to you it<00:16:22.790> might<00:16:23.120> help<00:16:23.329> the<00:16:23.510> solver<00:16:23.839> because<00:16:24.199> the 00:16:24.910 --> 00:16:24.920 align:start position:0% it might help the solver because the 00:16:24.920 --> 00:16:27.069 align:start position:0% it might help the solver because the more<00:16:25.130> constrained<00:16:25.730> to<00:16:25.910> give<00:16:26.120> the<00:16:26.510> last<00:16:26.690> false 00:16:27.069 --> 00:16:27.079 align:start position:0% more constrained to give the last false 00:16:27.079 --> 00:16:29.379 align:start position:0% more constrained to give the last false positives<00:16:27.620> the<00:16:28.459> tool<00:16:28.639> is<00:16:28.730> gonna<00:16:28.910> it's<00:16:29.300> gonna 00:16:29.379 --> 00:16:29.389 align:start position:0% positives the tool is gonna it's gonna 00:16:29.389 --> 00:16:32.800 align:start position:0% positives the tool is gonna it's gonna issue<00:16:29.709> so<00:16:30.790> I'm<00:16:31.790> gonna<00:16:31.940> run<00:16:32.240> a<00:16:32.449> couple<00:16:32.600> examples 00:16:32.800 --> 00:16:32.810 align:start position:0% issue so I'm gonna run a couple examples 00:16:32.810 --> 00:16:36.910 align:start position:0% issue so I'm gonna run a couple examples right<00:16:33.199> now<00:16:34.480> think<00:16:35.480> of<00:16:35.540> how<00:16:35.660> like<00:16:35.920> eight 00:16:36.910 --> 00:16:36.920 align:start position:0% right now think of how like eight 00:16:36.920 --> 00:16:49.310 align:start position:0% right now think of how like eight minutes 00:16:49.310 --> 00:16:49.320 align:start position:0% 00:16:49.320 --> 00:16:53.130 align:start position:0% can<00:16:50.320> everyone<00:16:50.560> read<00:16:51.210> not<00:16:52.210> in<00:16:52.330> general<00:16:52.660> but 00:16:53.130 --> 00:16:53.140 align:start position:0% can everyone read not in general but 00:16:53.140 --> 00:17:04.860 align:start position:0% can everyone read not in general but screen<00:16:57.600> what<00:16:58.600> I<00:16:59.190> did<00:17:00.190> push<00:17:03.510> yeah<00:17:04.510> and<00:17:04.660> it<00:17:04.720> sorry 00:17:04.860 --> 00:17:04.870 align:start position:0% screen what I did push yeah and it sorry 00:17:04.870 --> 00:17:08.250 align:start position:0% screen what I did push yeah and it sorry this<00:17:05.140> one<00:17:05.470> like<00:17:06.360> okay<00:17:07.360> so<00:17:07.420> this<00:17:07.720> is<00:17:07.870> like<00:17:08.230> a 00:17:08.250 --> 00:17:08.260 align:start position:0% this one like okay so this is like a 00:17:08.260 --> 00:17:10.829 align:start position:0% this one like okay so this is like a very<00:17:08.439> tiny<00:17:08.709> token<00:17:09.130> and<00:17:09.280> not<00:17:10.150> very<00:17:10.360> interesting 00:17:10.829 --> 00:17:10.839 align:start position:0% very tiny token and not very interesting 00:17:10.839 --> 00:17:13.970 align:start position:0% very tiny token and not very interesting so<00:17:11.730> we<00:17:12.730> have<00:17:12.850> a<00:17:12.880> map<00:17:13.089> in<00:17:13.120> with<00:17:13.420> balance 00:17:13.970 --> 00:17:13.980 align:start position:0% so we have a map in with balance 00:17:13.980 --> 00:17:17.460 align:start position:0% so we have a map in with balance constructor<00:17:14.980> initializes<00:17:15.459> the<00:17:16.360> balance<00:17:17.290> of 00:17:17.460 --> 00:17:17.470 align:start position:0% constructor initializes the balance of 00:17:17.470 --> 00:17:18.630 align:start position:0% constructor initializes the balance of the<00:17:17.589> message<00:17:17.829> center<00:17:18.100> with<00:17:18.250> a<00:17:18.280> bunch<00:17:18.520> of 00:17:18.630 --> 00:17:18.640 align:start position:0% the message center with a bunch of 00:17:18.640 --> 00:17:23.549 align:start position:0% the message center with a bunch of tokens<00:17:18.819> and<00:17:21.660> accounts<00:17:22.660> can<00:17:22.780> transfer<00:17:23.170> tokens 00:17:23.549 --> 00:17:23.559 align:start position:0% tokens and accounts can transfer tokens 00:17:23.559 --> 00:17:25.439 align:start position:0% tokens and accounts can transfer tokens which<00:17:23.740> other<00:17:23.890> right<00:17:24.370> so<00:17:24.910> there<00:17:25.059> are<00:17:25.089> few<00:17:25.240> line 00:17:25.439 --> 00:17:25.449 align:start position:0% which other right so there are few line 00:17:25.449 --> 00:17:27.090 align:start position:0% which other right so there are few line a<00:17:25.480> few<00:17:25.750> extra<00:17:26.079> lines<00:17:26.260> in<00:17:26.559> this<00:17:26.650> piece<00:17:26.800> of<00:17:26.920> code 00:17:27.090 --> 00:17:27.100 align:start position:0% a few extra lines in this piece of code 00:17:27.100 --> 00:17:29.490 align:start position:0% a few extra lines in this piece of code right<00:17:27.250> compared<00:17:27.730> to<00:17:27.809> normal<00:17:28.840> token 00:17:29.490 --> 00:17:29.500 align:start position:0% right compared to normal token 00:17:29.500 --> 00:17:33.240 align:start position:0% right compared to normal token implementations<00:17:30.929> so<00:17:31.929> first<00:17:32.230> of<00:17:32.350> all<00:17:32.440> this<00:17:33.100> is 00:17:33.240 --> 00:17:33.250 align:start position:0% implementations so first of all this is 00:17:33.250 --> 00:17:35.400 align:start position:0% implementations so first of all this is a<00:17:33.280> normal<00:17:33.610> one<00:17:33.640> right<00:17:34.030> we<00:17:34.210> required<00:17:34.570> that<00:17:34.780> the 00:17:35.400 --> 00:17:35.410 align:start position:0% a normal one right we required that the 00:17:35.410 --> 00:17:38.250 align:start position:0% a normal one right we required that the message<00:17:35.710> sender<00:17:35.950> actually<00:17:36.520> has<00:17:36.960> the<00:17:37.960> amount 00:17:38.250 --> 00:17:38.260 align:start position:0% message sender actually has the amount 00:17:38.260 --> 00:17:40.740 align:start position:0% message sender actually has the amount in<00:17:38.620> their<00:17:39.250> balance<00:17:39.550> but<00:17:40.270> here<00:17:40.450> I'm<00:17:40.630> actually 00:17:40.740 --> 00:17:40.750 align:start position:0% in their balance but here I'm actually 00:17:40.750 --> 00:17:44.610 align:start position:0% in their balance but here I'm actually storing<00:17:41.350> the<00:17:41.500> old<00:17:41.730> values<00:17:43.110> for<00:17:44.110> the<00:17:44.170> balances 00:17:44.610 --> 00:17:44.620 align:start position:0% storing the old values for the balances 00:17:44.620 --> 00:17:46.980 align:start position:0% storing the old values for the balances for<00:17:44.860> the<00:17:44.920> person<00:17:45.640> sending<00:17:45.880> the<00:17:46.480> transaction 00:17:46.980 --> 00:17:46.990 align:start position:0% for the person sending the transaction 00:17:46.990 --> 00:17:49.260 align:start position:0% for the person sending the transaction and<00:17:47.110> the<00:17:47.170> person<00:17:47.500> receiving<00:17:47.800> and<00:17:48.130> yeah<00:17:49.090> the 00:17:49.260 --> 00:17:49.270 align:start position:0% and the person receiving and yeah the 00:17:49.270 --> 00:17:50.669 align:start position:0% and the person receiving and yeah the person<00:17:49.540> received<00:17:49.870> the<00:17:49.990> account<00:17:50.140> receiving 00:17:50.669 --> 00:17:50.679 align:start position:0% person received the account receiving 00:17:50.679 --> 00:17:53.970 align:start position:0% person received the account receiving the<00:17:50.920> amount<00:17:51.510> here<00:17:52.510> the<00:17:52.840> balances<00:17:53.500> are<00:17:53.559> updated 00:17:53.970 --> 00:17:53.980 align:start position:0% the amount here the balances are updated 00:17:53.980 --> 00:17:55.680 align:start position:0% the amount here the balances are updated right<00:17:54.190> and<00:17:54.490> here<00:17:55.030> we<00:17:55.090> have<00:17:55.210> an<00:17:55.300> assertion<00:17:55.540> that 00:17:55.680 --> 00:17:55.690 align:start position:0% right and here we have an assertion that 00:17:55.690 --> 00:17:58.950 align:start position:0% right and here we have an assertion that says<00:17:56.020> that<00:17:56.980> the<00:17:57.730> sum<00:17:58.000> of<00:17:58.030> the<00:17:58.210> balances<00:17:58.750> before 00:17:58.950 --> 00:17:58.960 align:start position:0% says that the sum of the balances before 00:17:58.960 --> 00:18:00.750 align:start position:0% says that the sum of the balances before the<00:17:59.320> transaction<00:17:59.830> before<00:17:59.980> the<00:18:00.340> operations 00:18:00.750 --> 00:18:00.760 align:start position:0% the transaction before the operations 00:18:00.760 --> 00:18:03.210 align:start position:0% the transaction before the operations have<00:18:01.300> to<00:18:01.450> be<00:18:01.540> equal<00:18:01.840> the<00:18:02.230> sum<00:18:02.410> of<00:18:02.470> the<00:18:02.770> balances 00:18:03.210 --> 00:18:03.220 align:start position:0% have to be equal the sum of the balances 00:18:03.220 --> 00:18:05.280 align:start position:0% have to be equal the sum of the balances after<00:18:03.580> the<00:18:03.670> operation<00:18:04.030> oh<00:18:04.179> sorry 00:18:05.280 --> 00:18:05.290 align:start position:0% after the operation oh sorry 00:18:05.290 --> 00:18:08.280 align:start position:0% after the operation oh sorry yeah<00:18:05.920> this<00:18:06.070> should<00:18:06.250> be<00:18:06.400> the<00:18:06.520> right<00:18:07.290> assertion 00:18:08.280 --> 00:18:08.290 align:start position:0% yeah this should be the right assertion 00:18:08.290 --> 00:18:13.919 align:start position:0% yeah this should be the right assertion but<00:18:08.410> I<00:18:08.470> want<00:18:08.650> it<00:18:08.740> to<00:18:08.800> break<00:18:08.950> so<00:18:12.450> okay<00:18:13.450> so<00:18:13.480> here 00:18:13.919 --> 00:18:13.929 align:start position:0% but I want it to break so okay so here 00:18:13.929 --> 00:18:16.470 align:start position:0% but I want it to break so okay so here the<00:18:14.110> tool<00:18:14.290> tell<00:18:14.770> the<00:18:15.010> compiler<00:18:15.220> tells<00:18:15.550> us<00:18:15.760> the 00:18:16.470 --> 00:18:16.480 align:start position:0% the tool tell the compiler tells us the 00:18:16.480 --> 00:18:19.140 align:start position:0% the tool tell the compiler tells us the assertion<00:18:16.870> is<00:18:16.900> broken<00:18:17.200> and<00:18:17.830> gives<00:18:18.700> a<00:18:18.850> bunch<00:18:19.030> of 00:18:19.140 --> 00:18:19.150 align:start position:0% assertion is broken and gives a bunch of 00:18:19.150 --> 00:18:22.799 align:start position:0% assertion is broken and gives a bunch of values<00:18:19.660> for<00:18:20.110> for<00:18:20.800> our<00:18:21.010> variables<00:18:21.880> right<00:18:22.179> so 00:18:22.799 --> 00:18:22.809 align:start position:0% values for for our variables right so 00:18:22.809 --> 00:18:24.120 align:start position:0% values for for our variables right so but<00:18:23.080> there's<00:18:23.260> something<00:18:23.559> weird<00:18:23.830> right<00:18:23.980> so 00:18:24.120 --> 00:18:24.130 align:start position:0% but there's something weird right so 00:18:24.130 --> 00:18:25.950 align:start position:0% but there's something weird right so it's<00:18:24.250> saying<00:18:24.490> that<00:18:24.640> it<00:18:24.970> gave<00:18:25.150> zero<00:18:25.450> to<00:18:25.630> both 00:18:25.950 --> 00:18:25.960 align:start position:0% it's saying that it gave zero to both 00:18:25.960 --> 00:18:28.740 align:start position:0% it's saying that it gave zero to both two<00:18:26.230> and<00:18:26.260> message<00:18:26.679> sender<00:18:27.040> which<00:18:27.790> commonly 00:18:28.740 --> 00:18:28.750 align:start position:0% two and message sender which commonly 00:18:28.750 --> 00:18:32.010 align:start position:0% two and message sender which commonly people<00:18:29.110> prevent<00:18:29.620> right<00:18:30.160> so<00:18:30.730> we<00:18:30.850> can<00:18:31.090> just<00:18:31.720> add 00:18:32.010 --> 00:18:32.020 align:start position:0% people prevent right so we can just add 00:18:32.020 --> 00:18:36.720 align:start position:0% people prevent right so we can just add that<00:18:32.320> here<00:18:33.090> I<00:18:34.090> want<00:18:34.630> message<00:18:35.050> sender<00:18:35.470> to<00:18:36.130> be<00:18:36.429> oh 00:18:36.720 --> 00:18:36.730 align:start position:0% that here I want message sender to be oh 00:18:36.730 --> 00:18:38.580 align:start position:0% that here I want message sender to be oh this<00:18:37.150> is<00:18:37.210> actually<00:18:37.450> gonna<00:18:37.600> work<00:18:37.809> so<00:18:38.110> I'm<00:18:38.410> just 00:18:38.580 --> 00:18:38.590 align:start position:0% this is actually gonna work so I'm just 00:18:38.590 --> 00:18:41.400 align:start position:0% this is actually gonna work so I'm just gonna<00:18:38.679> say<00:18:38.950> they<00:18:39.100> have<00:18:39.220> to<00:18:39.340> be<00:18:39.429> different<00:18:40.410> it's 00:18:41.400 --> 00:18:41.410 align:start position:0% gonna say they have to be different it's 00:18:41.410 --> 00:18:46.180 align:start position:0% gonna say they have to be different it's fine<00:18:41.620> if<00:18:41.740> there<00:18:41.860> is<00:18:41.920> zero 00:18:46.180 --> 00:18:46.190 align:start position:0% 00:18:46.190 --> 00:18:48.850 align:start position:0% so<00:18:46.820> okay<00:18:47.120> now<00:18:47.150> it<00:18:47.420> changed<00:18:47.780> right<00:18:47.960> so<00:18:48.260> two<00:18:48.320> and 00:18:48.850 --> 00:18:48.860 align:start position:0% so okay now it changed right so two and 00:18:48.860 --> 00:18:50.980 align:start position:0% so okay now it changed right so two and two<00:18:48.980> one<00:18:49.160> before<00:18:50.060> was<00:18:50.210> zero<00:18:50.390> mass<00:18:50.660> percentage 00:18:50.980 --> 00:18:50.990 align:start position:0% two one before was zero mass percentage 00:18:50.990 --> 00:18:52.120 align:start position:0% two one before was zero mass percentage to<00:18:51.110> zero<00:18:51.320> but<00:18:51.440> that's<00:18:51.590> fine<00:18:51.740> because<00:18:51.920> they're 00:18:52.120 --> 00:18:52.130 align:start position:0% to zero but that's fine because they're 00:18:52.130 --> 00:18:54.730 align:start position:0% to zero but that's fine because they're different<00:18:52.280> and<00:18:53.050> the<00:18:54.050> assertion<00:18:54.410> is<00:18:54.440> actually 00:18:54.730 --> 00:18:54.740 align:start position:0% different and the assertion is actually 00:18:54.740 --> 00:18:57.040 align:start position:0% different and the assertion is actually saying<00:18:55.010> that<00:18:55.130> the<00:18:55.220> balance<00:18:55.520> before<00:18:56.050> was 00:18:57.040 --> 00:18:57.050 align:start position:0% saying that the balance before was 00:18:57.050 --> 00:18:59.470 align:start position:0% saying that the balance before was greater<00:18:57.410> than<00:18:57.710> the<00:18:58.340> balance<00:18:58.850> right<00:18:59.060> now<00:18:59.270> which 00:18:59.470 --> 00:18:59.480 align:start position:0% greater than the balance right now which 00:18:59.480 --> 00:19:02.590 align:start position:0% greater than the balance right now which means<00:18:59.510> that<00:18:59.930> some<00:19:00.080> tokens<00:19:00.440> vanished<00:19:00.770> right<00:19:01.600> so 00:19:02.590 --> 00:19:02.600 align:start position:0% means that some tokens vanished right so 00:19:02.600 --> 00:19:04.330 align:start position:0% means that some tokens vanished right so the<00:19:02.900> assertion<00:19:03.080> is<00:19:03.260> basically<00:19:03.530> saying<00:19:03.830> every 00:19:04.330 --> 00:19:04.340 align:start position:0% the assertion is basically saying every 00:19:04.340 --> 00:19:05.970 align:start position:0% the assertion is basically saying every time<00:19:04.520> there's<00:19:04.700> a<00:19:04.760> transfer<00:19:05.120> tokens<00:19:05.510> vanish 00:19:05.970 --> 00:19:05.980 align:start position:0% time there's a transfer tokens vanish 00:19:05.980 --> 00:19:08.530 align:start position:0% time there's a transfer tokens vanish which<00:19:06.980> hopefully<00:19:07.340> is<00:19:07.550> wrong<00:19:07.820> and<00:19:08.120> the<00:19:08.390> tool 00:19:08.530 --> 00:19:08.540 align:start position:0% which hopefully is wrong and the tool 00:19:08.540 --> 00:19:10.600 align:start position:0% which hopefully is wrong and the tool set<00:19:08.720> is<00:19:08.750> wrong<00:19:09.020> can<00:19:09.620> say<00:19:09.740> balance<00:19:09.950> from<00:19:10.220> plus 00:19:10.600 --> 00:19:10.610 align:start position:0% set is wrong can say balance from plus 00:19:10.610 --> 00:19:14.220 align:start position:0% set is wrong can say balance from plus balance<00:19:10.940> to<00:19:11.530> is<00:19:12.530> actually<00:19:12.950> the<00:19:13.040> same<00:19:13.310> as 00:19:14.220 --> 00:19:14.230 align:start position:0% balance to is actually the same as 00:19:14.230 --> 00:19:17.230 align:start position:0% balance to is actually the same as balance<00:19:15.230> of<00:19:15.380> serum<00:19:15.680> plus<00:19:16.280> balance<00:19:16.640> of<00:19:16.940> one 00:19:17.230 --> 00:19:17.240 align:start position:0% balance of serum plus balance of one 00:19:17.240 --> 00:19:20.440 align:start position:0% balance of serum plus balance of one which<00:19:17.540> are<00:19:17.750> the<00:19:17.990> accounts<00:19:19.030> so<00:19:20.030> if<00:19:20.210> we<00:19:20.360> actually 00:19:20.440 --> 00:19:20.450 align:start position:0% which are the accounts so if we actually 00:19:20.450 --> 00:19:28.030 align:start position:0% which are the accounts so if we actually fix<00:19:21.020> the<00:19:21.110> assertion<00:19:26.680> there<00:19:27.680> you<00:19:27.770> go<00:19:27.860> if 00:19:28.030 --> 00:19:28.040 align:start position:0% fix the assertion there you go if 00:19:28.040 --> 00:19:30.400 align:start position:0% fix the assertion there you go if there's<00:19:28.340> no<00:19:28.570> if<00:19:29.570> it<00:19:29.780> doesn't<00:19:29.990> complain<00:19:30.230> it 00:19:30.400 --> 00:19:30.410 align:start position:0% there's no if it doesn't complain it 00:19:30.410 --> 00:19:34.660 align:start position:0% there's no if it doesn't complain it means<00:19:30.560> it's<00:19:30.680> safe<00:19:33.160> I'm<00:19:34.160> gonna<00:19:34.310> move<00:19:34.490> on<00:19:34.610> to 00:19:34.660 --> 00:19:34.670 align:start position:0% means it's safe I'm gonna move on to 00:19:34.670 --> 00:19:36.670 align:start position:0% means it's safe I'm gonna move on to it's<00:19:35.210> likely<00:19:35.450> a<00:19:35.480> better<00:19:35.600> example<00:19:35.840> with<00:19:36.350> a 00:19:36.670 --> 00:19:36.680 align:start position:0% it's likely a better example with a 00:19:36.680 --> 00:19:44.130 align:start position:0% it's likely a better example with a bunch<00:19:37.100> of<00:19:37.220> false<00:19:37.430> positives<00:19:37.940> oh<00:19:40.450> not<00:19:41.450> this 00:19:44.130 --> 00:19:44.140 align:start position:0% 00:19:44.140 --> 00:19:52.540 align:start position:0% this<00:19:45.140> okay<00:19:45.980> so<00:19:46.040> here<00:19:46.340> we<00:19:46.370> have<00:19:51.370> yeah<00:19:52.370> this 00:19:52.540 --> 00:19:52.550 align:start position:0% this okay so here we have yeah this 00:19:52.550 --> 00:19:54.490 align:start position:0% this okay so here we have yeah this contract<00:19:52.910> see<00:19:53.120> this<00:19:53.450> there's<00:19:54.260> external 00:19:54.490 --> 00:19:54.500 align:start position:0% contract see this there's external 00:19:54.500 --> 00:20:00.880 align:start position:0% contract see this there's external contract<00:19:55.010> this<00:19:55.700> matter<00:19:56.120> for<00:19:56.480> now<00:19:56.710> oh<00:19:59.890> sorry 00:20:00.880 --> 00:20:00.890 align:start position:0% contract this matter for now oh sorry 00:20:00.890 --> 00:20:01.870 align:start position:0% contract this matter for now oh sorry about<00:20:01.010> that<00:20:01.130> it's<00:20:01.370> not<00:20:01.400> the<00:20:01.520> one<00:20:01.640> I<00:20:01.700> want<00:20:01.850> to 00:20:01.870 --> 00:20:01.880 align:start position:0% about that it's not the one I want to 00:20:01.880 --> 00:20:07.990 align:start position:0% about that it's not the one I want to show<00:20:03.850> this<00:20:04.850> one<00:20:04.930> so<00:20:05.930> we<00:20:06.140> have<00:20:06.580> just<00:20:07.580> like<00:20:07.790> kind 00:20:07.990 --> 00:20:08.000 align:start position:0% show this one so we have just like kind 00:20:08.000 --> 00:20:12.520 align:start position:0% show this one so we have just like kind of<00:20:08.060> an<00:20:08.240> account<00:20:08.540> but<00:20:09.100> some<00:20:10.100> it<00:20:10.760> stores<00:20:11.600> the 00:20:12.520 --> 00:20:12.530 align:start position:0% of an account but some it stores the 00:20:12.530 --> 00:20:17.470 align:start position:0% of an account but some it stores the some<00:20:13.000> the<00:20:14.000> balance<00:20:14.390> of<00:20:15.460> like<00:20:16.460> it's<00:20:16.880> its<00:20:17.270> own 00:20:17.470 --> 00:20:17.480 align:start position:0% some the balance of like it's its own 00:20:17.480 --> 00:20:20.110 align:start position:0% some the balance of like it's its own balance<00:20:18.290> and<00:20:18.650> here<00:20:19.460> it<00:20:19.520> counts<00:20:19.940> how<00:20:19.970> many 00:20:20.110 --> 00:20:20.120 align:start position:0% balance and here it counts how many 00:20:20.120 --> 00:20:22.750 align:start position:0% balance and here it counts how many transactions<00:20:20.810> how<00:20:21.680> many<00:20:21.860> times<00:20:22.370> the<00:20:22.580> fall 00:20:22.750 --> 00:20:22.760 align:start position:0% transactions how many times the fall 00:20:22.760 --> 00:20:24.460 align:start position:0% transactions how many times the fall back<00:20:22.940> function<00:20:23.330> was<00:20:23.480> called<00:20:23.660> increasing<00:20:24.380> the 00:20:24.460 --> 00:20:24.470 align:start position:0% back function was called increasing the 00:20:24.470 --> 00:20:25.960 align:start position:0% back function was called increasing the value<00:20:24.770> increasing<00:20:25.310> the<00:20:25.400> balance<00:20:25.700> of<00:20:25.850> this 00:20:25.960 --> 00:20:25.970 align:start position:0% value increasing the balance of this 00:20:25.970 --> 00:20:27.910 align:start position:0% value increasing the balance of this account<00:20:26.140> so<00:20:27.140> here<00:20:27.350> we<00:20:27.410> have<00:20:27.530> the<00:20:27.620> fall<00:20:27.770> back 00:20:27.910 --> 00:20:27.920 align:start position:0% account so here we have the fall back 00:20:27.920 --> 00:20:32.650 align:start position:0% account so here we have the fall back function<00:20:28.280> that<00:20:28.370> says<00:20:30.490> that<00:20:31.490> the<00:20:31.760> value<00:20:32.300> sent 00:20:32.650 --> 00:20:32.660 align:start position:0% function that says that the value sent 00:20:32.660 --> 00:20:35.950 align:start position:0% function that says that the value sent to<00:20:33.080> be<00:20:33.230> greater<00:20:33.470> than<00:20:33.500> zero<00:20:33.800> and<00:20:34.570> this<00:20:35.570> is<00:20:35.630> just 00:20:35.950 --> 00:20:35.960 align:start position:0% to be greater than zero and this is just 00:20:35.960 --> 00:20:38.890 align:start position:0% to be greater than zero and this is just to<00:20:36.490> give<00:20:37.490> a<00:20:37.520> constraint<00:20:37.880> for<00:20:38.030> an<00:20:38.330> avoider<00:20:38.690> if 00:20:38.890 --> 00:20:38.900 align:start position:0% to give a constraint for an avoider if 00:20:38.900 --> 00:20:42.820 align:start position:0% to give a constraint for an avoider if cause<00:20:39.080> later<00:20:39.610> requiring<00:20:40.610> that<00:20:41.320> this<00:20:42.320> account 00:20:42.820 --> 00:20:42.830 align:start position:0% cause later requiring that this account 00:20:42.830 --> 00:20:44.320 align:start position:0% cause later requiring that this account cannot<00:20:43.070> have<00:20:43.280> more<00:20:43.520> than<00:20:43.670> 1<00:20:43.820> million<00:20:44.030> the 00:20:44.320 --> 00:20:44.330 align:start position:0% cannot have more than 1 million the 00:20:44.330 --> 00:20:46.170 align:start position:0% cannot have more than 1 million the balance<00:20:44.600> cannot<00:20:44.810> be<00:20:44.960> greater<00:20:45.200> than<00:20:45.410> 1<00:20:45.650> million 00:20:46.170 --> 00:20:46.180 align:start position:0% balance cannot be greater than 1 million 00:20:46.180 --> 00:20:49.180 align:start position:0% balance cannot be greater than 1 million so<00:20:47.180> here<00:20:47.480> we<00:20:47.600> just<00:20:47.840> increase<00:20:48.290> the<00:20:48.770> sum<00:20:49.040> and 00:20:49.180 --> 00:20:49.190 align:start position:0% so here we just increase the sum and 00:20:49.190 --> 00:20:50.920 align:start position:0% so here we just increase the sum and increase<00:20:49.430> account<00:20:49.730> right<00:20:50.030> and<00:20:50.270> here<00:20:50.720> we<00:20:50.780> have 00:20:50.920 --> 00:20:50.930 align:start position:0% increase account right and here we have 00:20:50.930 --> 00:20:53.110 align:start position:0% increase account right and here we have a<00:20:51.110> function<00:20:51.320> called<00:20:51.500> average<00:20:51.980> that<00:20:52.610> computes 00:20:53.110 --> 00:20:53.120 align:start position:0% a function called average that computes 00:20:53.120 --> 00:20:56.140 align:start position:0% a function called average that computes the<00:20:53.270> average<00:20:54.160> the<00:20:55.160> average<00:20:55.280> value<00:20:55.790> that<00:20:55.820> was 00:20:56.140 --> 00:20:56.150 align:start position:0% the average the average value that was 00:20:56.150 --> 00:20:57.700 align:start position:0% the average the average value that was sent<00:20:56.390> per<00:20:56.690> transaction 00:20:57.700 --> 00:20:57.710 align:start position:0% sent per transaction 00:20:57.710 --> 00:21:01.180 align:start position:0% sent per transaction all<00:20:58.520> right<00:20:58.960> so<00:20:59.960> here<00:21:00.500> I<00:21:00.529> put<00:21:00.740> is<00:21:00.860> required 00:21:01.180 --> 00:21:01.190 align:start position:0% all right so here I put is required 00:21:01.190 --> 00:21:04.180 align:start position:0% all right so here I put is required because<00:21:01.610> if<00:21:02.169> if<00:21:03.169> there<00:21:03.440> was<00:21:03.590> no<00:21:03.740> transaction 00:21:04.180 --> 00:21:04.190 align:start position:0% because if if there was no transaction 00:21:04.190 --> 00:21:06.269 align:start position:0% because if if there was no transaction doesn't<00:21:04.340> make<00:21:04.490> sense<00:21:04.669> compute<00:21:05.000> the<00:21:05.059> average 00:21:06.269 --> 00:21:06.279 align:start position:0% doesn't make sense compute the average 00:21:06.279 --> 00:21:08.529 align:start position:0% doesn't make sense compute the average but<00:21:07.279> here<00:21:07.460> we<00:21:07.610> have<00:21:07.789> an<00:21:07.909> ax<00:21:07.970> so<00:21:08.000> here<00:21:08.450> we 00:21:08.529 --> 00:21:08.539 align:start position:0% but here we have an ax so here we 00:21:08.539 --> 00:21:09.820 align:start position:0% but here we have an ax so here we compute<00:21:08.870> the<00:21:08.929> average<00:21:09.020> and<00:21:09.409> we<00:21:09.470> assert<00:21:09.799> that 00:21:09.820 --> 00:21:09.830 align:start position:0% compute the average and we assert that 00:21:09.830 --> 00:21:11.590 align:start position:0% compute the average and we assert that the<00:21:10.100> average<00:21:10.429> has<00:21:10.909> to<00:21:11.029> be<00:21:11.090> greater<00:21:11.299> than<00:21:11.330> zero 00:21:11.590 --> 00:21:11.600 align:start position:0% the average has to be greater than zero 00:21:11.600 --> 00:21:12.789 align:start position:0% the average has to be greater than zero right<00:21:11.809> because<00:21:12.230> if<00:21:12.350> you<00:21:12.440> did<00:21:12.620> have<00:21:12.770> a 00:21:12.789 --> 00:21:12.799 align:start position:0% right because if you did have a 00:21:12.799 --> 00:21:16.240 align:start position:0% right because if you did have a transaction<00:21:13.370> because<00:21:14.210> of<00:21:14.539> this<00:21:14.750> line<00:21:15.250> we 00:21:16.240 --> 00:21:16.250 align:start position:0% transaction because of this line we 00:21:16.250 --> 00:21:18.820 align:start position:0% transaction because of this line we cannot<00:21:16.539> compute<00:21:17.539> we<00:21:17.659> cannot<00:21:17.870> we<00:21:18.080> don't<00:21:18.289> count 00:21:18.820 --> 00:21:18.830 align:start position:0% cannot compute we cannot we don't count 00:21:18.830 --> 00:21:22.600 align:start position:0% cannot compute we cannot we don't count zeros<00:21:19.480> in<00:21:20.480> a<00:21:20.539> transaction<00:21:20.990> so<00:21:21.399> the<00:21:22.399> assertion 00:21:22.600 --> 00:21:22.610 align:start position:0% zeros in a transaction so the assertion 00:21:22.610 --> 00:21:33.740 align:start position:0% zeros in a transaction so the assertion is<00:21:23.120> true<00:21:23.779> agreed 00:21:33.740 --> 00:21:33.750 align:start position:0% 00:21:33.750 --> 00:21:36.240 align:start position:0% okay<00:21:34.750> so<00:21:34.810> it's<00:21:35.560> telling<00:21:35.740> us<00:21:35.920> that<00:21:36.040> the 00:21:36.240 --> 00:21:36.250 align:start position:0% okay so it's telling us that the 00:21:36.250 --> 00:21:39.810 align:start position:0% okay so it's telling us that the assertion<00:21:36.700> is<00:21:36.910> actually<00:21:37.780> not<00:21:37.900> true<00:21:38.640> and<00:21:39.640> give 00:21:39.810 --> 00:21:39.820 align:start position:0% assertion is actually not true and give 00:21:39.820 --> 00:21:42.630 align:start position:0% assertion is actually not true and give some<00:21:40.150> value<00:21:40.510> so<00:21:40.810> it<00:21:41.410> says<00:21:41.770> that<00:21:42.040> if<00:21:42.160> count<00:21:42.430> is 00:21:42.630 --> 00:21:42.640 align:start position:0% some value so it says that if count is 00:21:42.640 --> 00:21:45.570 align:start position:0% some value so it says that if count is one<00:21:42.880> and<00:21:43.120> sum<00:21:43.360> is<00:21:43.570> zero<00:21:43.890> then<00:21:44.890> the<00:21:45.130> average<00:21:45.400> is 00:21:45.570 --> 00:21:45.580 align:start position:0% one and sum is zero then the average is 00:21:45.580 --> 00:21:48.750 align:start position:0% one and sum is zero then the average is zero<00:21:45.790> which<00:21:46.360> is<00:21:46.600> correct<00:21:47.050> right<00:21:47.580> but<00:21:48.580> then<00:21:48.730> the 00:21:48.750 --> 00:21:48.760 align:start position:0% zero which is correct right but then the 00:21:48.760 --> 00:21:52.110 align:start position:0% zero which is correct right but then the question<00:21:49.090> is<00:21:49.620> can<00:21:50.620> this<00:21:50.740> ever<00:21:50.920> happen<00:21:51.340> can 00:21:52.110 --> 00:21:52.120 align:start position:0% question is can this ever happen can 00:21:52.120 --> 00:21:54.600 align:start position:0% question is can this ever happen can count<00:21:52.450> can<00:21:53.290> it<00:21:53.620> have<00:21:53.830> ever<00:21:54.100> happened<00:21:54.520> that 00:21:54.600 --> 00:21:54.610 align:start position:0% count can it have ever happened that 00:21:54.610 --> 00:22:00.320 align:start position:0% count can it have ever happened that count<00:21:54.850> is<00:21:55.000> 1<00:21:55.210> and<00:21:55.480> sum<00:21:55.690> is<00:21:55.870> zero<00:21:56.640> why 00:22:00.320 --> 00:22:00.330 align:start position:0% 00:22:00.330 --> 00:22:03.240 align:start position:0% exactly<00:22:01.330> so<00:22:01.630> message<00:22:02.530> Valley<00:22:02.740> is<00:22:02.890> an<00:22:03.010> integer 00:22:03.240 --> 00:22:03.250 align:start position:0% exactly so message Valley is an integer 00:22:03.250 --> 00:22:05.850 align:start position:0% exactly so message Valley is an integer right<00:22:03.610> with<00:22:04.450> this<00:22:04.660> require<00:22:05.020> is<00:22:05.260> a<00:22:05.440> message 00:22:05.850 --> 00:22:05.860 align:start position:0% right with this require is a message 00:22:05.860 --> 00:22:08.760 align:start position:0% right with this require is a message value<00:22:06.190> is<00:22:06.400> actually<00:22:07.240> at<00:22:07.540> least<00:22:07.570> one<00:22:08.050> here<00:22:08.590> and 00:22:08.760 --> 00:22:08.770 align:start position:0% value is actually at least one here and 00:22:08.770 --> 00:22:12.240 align:start position:0% value is actually at least one here and count<00:22:09.340> only<00:22:09.850> increases<00:22:10.210> by<00:22:10.360> one<00:22:10.600> so<00:22:11.590> this 00:22:12.240 --> 00:22:12.250 align:start position:0% count only increases by one so this 00:22:12.250 --> 00:22:18.320 align:start position:0% count only increases by one so this property<00:22:12.580> here<00:22:15.510> is<00:22:16.510> true<00:22:16.810> right 00:22:18.320 --> 00:22:18.330 align:start position:0% property here is true right 00:22:18.330 --> 00:22:21.120 align:start position:0% property here is true right it's<00:22:19.330> an<00:22:19.480> invariant<00:22:19.900> it's<00:22:20.110> true<00:22:20.350> like<00:22:20.680> at<00:22:20.890> any 00:22:21.120 --> 00:22:21.130 align:start position:0% it's an invariant it's true like at any 00:22:21.130 --> 00:22:24.600 align:start position:0% it's an invariant it's true like at any point<00:22:21.520> of<00:22:21.730> the<00:22:21.850> contract<00:22:22.360> right<00:22:23.370> but<00:22:24.370> it's 00:22:24.600 --> 00:22:24.610 align:start position:0% point of the contract right but it's 00:22:24.610 --> 00:22:27.000 align:start position:0% point of the contract right but it's hard<00:22:24.850> for<00:22:24.970> the<00:22:25.060> SMT<00:22:25.330> checker<00:22:25.540> to<00:22:25.900> figure<00:22:26.860> that 00:22:27.000 --> 00:22:27.010 align:start position:0% hard for the SMT checker to figure that 00:22:27.010 --> 00:22:29.490 align:start position:0% hard for the SMT checker to figure that out<00:22:27.070> on<00:22:27.220> its<00:22:27.460> own<00:22:27.610> and<00:22:27.990> that's<00:22:28.990> what<00:22:29.200> I<00:22:29.230> meant 00:22:29.490 --> 00:22:29.500 align:start position:0% out on its own and that's what I meant 00:22:29.500 --> 00:22:31.650 align:start position:0% out on its own and that's what I meant with<00:22:30.010> you<00:22:30.400> as<00:22:30.580> a<00:22:30.610> developer<00:22:30.790> of<00:22:31.120> the<00:22:31.240> contract 00:22:31.650 --> 00:22:31.660 align:start position:0% with you as a developer of the contract 00:22:31.660 --> 00:22:33.120 align:start position:0% with you as a developer of the contract know<00:22:32.170> this<00:22:32.410> kind<00:22:32.590> of<00:22:32.680> thing<00:22:32.860> then<00:22:33.040> you<00:22:33.100> can 00:22:33.120 --> 00:22:33.130 align:start position:0% know this kind of thing then you can 00:22:33.130 --> 00:22:35.250 align:start position:0% know this kind of thing then you can help<00:22:33.490> you<00:22:33.700> can<00:22:33.910> help<00:22:33.940> destiny<00:22:34.510> checker<00:22:34.750> by 00:22:35.250 --> 00:22:35.260 align:start position:0% help you can help destiny checker by 00:22:35.260 --> 00:22:37.080 align:start position:0% help you can help destiny checker by adding<00:22:35.680> those<00:22:35.800> invariants<00:22:36.370> whenever<00:22:36.940> you 00:22:37.080 --> 00:22:37.090 align:start position:0% adding those invariants whenever you 00:22:37.090 --> 00:22:40.320 align:start position:0% adding those invariants whenever you have<00:22:37.270> these<00:22:37.510> harder<00:22:37.810> checks<00:22:38.610> let's<00:22:39.610> see<00:22:39.820> okay 00:22:40.320 --> 00:22:40.330 align:start position:0% have these harder checks let's see okay 00:22:40.330 --> 00:22:45.320 align:start position:0% have these harder checks let's see okay now<00:22:40.510> it's<00:22:40.660> fine<00:22:43.050> so<00:22:44.050> I<00:22:44.080> have<00:22:44.260> one<00:22:44.530> last<00:22:44.740> example 00:22:45.320 --> 00:22:45.330 align:start position:0% now it's fine so I have one last example 00:22:45.330 --> 00:22:47.790 align:start position:0% now it's fine so I have one last example which<00:22:46.330> was<00:22:46.480> the<00:22:46.600> one<00:22:46.660> that<00:22:46.810> actually<00:22:46.900> closed 00:22:47.790 --> 00:22:47.800 align:start position:0% which was the one that actually closed 00:22:47.800 --> 00:22:51.870 align:start position:0% which was the one that actually closed here<00:22:49.890> yeah<00:22:50.890> it's<00:22:51.010> the<00:22:51.070> same<00:22:51.340> it's<00:22:51.760> the<00:22:51.820> same 00:22:51.870 --> 00:22:51.880 align:start position:0% here yeah it's the same it's the same 00:22:51.880 --> 00:22:53.580 align:start position:0% here yeah it's the same it's the same contract<00:22:52.360> just<00:22:52.570> with<00:22:52.780> the<00:22:52.960> extension<00:22:53.290> that<00:22:53.440> we 00:22:53.580 --> 00:22:53.590 align:start position:0% contract just with the extension that we 00:22:53.590 --> 00:22:57.830 align:start position:0% contract just with the extension that we have<00:22:53.710> this<00:22:53.830> exterior<00:22:54.040> contract<00:22:54.580> and<00:22:55.320> we<00:22:56.320> call 00:22:57.830 --> 00:22:57.840 align:start position:0% have this exterior contract and we call 00:22:57.840 --> 00:23:00.270 align:start position:0% have this exterior contract and we call some<00:22:58.840> function<00:22:59.230> f<00:22:59.380> next<00:22:59.740> we<00:22:59.800> know<00:22:59.890> contract 00:23:00.270 --> 00:23:00.280 align:start position:0% some function f next we know contract 00:23:00.280 --> 00:23:02.580 align:start position:0% some function f next we know contract and<00:23:00.790> what<00:23:01.030> what<00:23:01.420> happens<00:23:01.720> here<00:23:02.050> is<00:23:02.200> that<00:23:02.230> when 00:23:02.580 --> 00:23:02.590 align:start position:0% and what what happens here is that when 00:23:02.590 --> 00:23:04.290 align:start position:0% and what what happens here is that when we<00:23:02.740> call<00:23:02.920> the<00:23:03.040> external<00:23:03.340> function<00:23:03.700> the 00:23:04.290 --> 00:23:04.300 align:start position:0% we call the external function the 00:23:04.300 --> 00:23:10.560 align:start position:0% we call the external function the knowledge<00:23:06.030> gets<00:23:07.770> basically<00:23:08.770> erased<00:23:09.310> and<00:23:09.670> you 00:23:10.560 --> 00:23:10.570 align:start position:0% knowledge gets basically erased and you 00:23:10.570 --> 00:23:13.530 align:start position:0% knowledge gets basically erased and you would<00:23:10.720> need<00:23:10.900> to<00:23:11.350> add<00:23:11.710> new<00:23:12.550> constraints<00:23:13.120> after 00:23:13.530 --> 00:23:13.540 align:start position:0% would need to add new constraints after 00:23:13.540 --> 00:23:17.010 align:start position:0% would need to add new constraints after the<00:23:13.750> after<00:23:14.230> the<00:23:14.850> after<00:23:15.850> the<00:23:16.510> function<00:23:16.840> call 00:23:17.010 --> 00:23:17.020 align:start position:0% the after the after the function call 00:23:17.020 --> 00:23:18.650 align:start position:0% the after the after the function call you<00:23:17.170> maybe<00:23:17.500> even<00:23:17.830> need<00:23:17.950> to<00:23:18.040> repeat 00:23:18.650 --> 00:23:18.660 align:start position:0% you maybe even need to repeat 00:23:18.660 --> 00:23:23.340 align:start position:0% you maybe even need to repeat unconstrained<00:23:19.660> sue<00:23:21.480> in<00:23:22.480> order<00:23:22.870> to<00:23:22.990> help<00:23:23.140> us 00:23:23.340 --> 00:23:23.350 align:start position:0% unconstrained sue in order to help us 00:23:23.350 --> 00:23:25.170 align:start position:0% unconstrained sue in order to help us over<00:23:23.650> to<00:23:23.770> actually<00:23:24.070> prove<00:23:24.280> it<00:23:24.430> and<00:23:24.550> not<00:23:24.970> get 00:23:25.170 --> 00:23:25.180 align:start position:0% over to actually prove it and not get 00:23:25.180 --> 00:23:32.300 align:start position:0% over to actually prove it and not get false<00:23:25.480> positives 00:23:32.300 --> 00:23:32.310 align:start position:0% 00:23:32.310 --> 00:23:34.940 align:start position:0% and<00:23:32.930> one<00:23:33.930> last<00:23:34.050> thing<00:23:34.170> that<00:23:34.290> I<00:23:34.410> wanted<00:23:34.620> to<00:23:34.710> say 00:23:34.940 --> 00:23:34.950 align:start position:0% and one last thing that I wanted to say 00:23:34.950 --> 00:23:38.600 align:start position:0% and one last thing that I wanted to say is<00:23:36.020> future<00:23:37.020> plans<00:23:37.290> that<00:23:37.590> we<00:23:37.740> have<00:23:37.890> for<00:23:37.920> for<00:23:38.490> the 00:23:38.600 --> 00:23:38.610 align:start position:0% is future plans that we have for for the 00:23:38.610 --> 00:23:41.930 align:start position:0% is future plans that we have for for the tool<00:23:39.710> yeah<00:23:40.710> we<00:23:40.890> have<00:23:41.040> more<00:23:41.190> examples<00:23:41.280> and<00:23:41.790> I'd 00:23:41.930 --> 00:23:41.940 align:start position:0% tool yeah we have more examples and I'd 00:23:41.940 --> 00:23:45.020 align:start position:0% tool yeah we have more examples and I'd be<00:23:42.240> glad<00:23:42.390> to<00:23:42.510> talk<00:23:42.810> about<00:23:42.960> the<00:23:43.890> tool<00:23:44.070> more 00:23:45.020 --> 00:23:45.030 align:start position:0% be glad to talk about the tool more 00:23:45.030 --> 00:23:47.240 align:start position:0% be glad to talk about the tool more offline<00:23:45.990> if<00:23:46.260> you<00:23:46.320> guys<00:23:46.440> want<00:23:46.710> I<00:23:46.920> want<00:23:47.070> to<00:23:47.100> talk 00:23:47.240 --> 00:23:47.250 align:start position:0% offline if you guys want I want to talk 00:23:47.250 --> 00:23:51.590 align:start position:0% offline if you guys want I want to talk about<00:23:47.340> it<00:23:48.530> as<00:23:49.530> future<00:23:49.980> plans<00:23:50.280> we<00:23:50.610> have<00:23:50.820> what<00:23:51.570> I 00:23:51.590 --> 00:23:51.600 align:start position:0% about it as future plans we have what I 00:23:51.600 --> 00:23:54.800 align:start position:0% about it as future plans we have what I mentioned<00:23:51.870> which<00:23:52.770> is<00:23:53.090> this<00:23:54.090> sort<00:23:54.420> of<00:23:54.510> function 00:23:54.800 --> 00:23:54.810 align:start position:0% mentioned which is this sort of function 00:23:54.810 --> 00:23:59.120 align:start position:0% mentioned which is this sort of function modular<00:23:55.850> verification<00:23:56.850> part<00:23:57.120> which<00:23:57.540> is<00:23:58.170> kind 00:23:59.120 --> 00:23:59.130 align:start position:0% modular verification part which is kind 00:23:59.130 --> 00:24:02.090 align:start position:0% modular verification part which is kind of<00:23:59.280> involved<00:23:59.790> with<00:23:59.820> the<00:24:00.330> state<00:24:01.100> invariant 00:24:02.090 --> 00:24:02.100 align:start position:0% of involved with the state invariant 00:24:02.100 --> 00:24:04.550 align:start position:0% of involved with the state invariant automatic<00:24:02.790> deduction<00:24:03.240> which<00:24:04.110> is<00:24:04.230> a<00:24:04.290> very<00:24:04.470> hard 00:24:04.550 --> 00:24:04.560 align:start position:0% automatic deduction which is a very hard 00:24:04.560 --> 00:24:07.400 align:start position:0% automatic deduction which is a very hard thing<00:24:04.800> to<00:24:04.830> do<00:24:05.070> but<00:24:05.340> we<00:24:05.580> want<00:24:05.700> to<00:24:05.880> try<00:24:06.120> it<00:24:06.180> anyway 00:24:07.400 --> 00:24:07.410 align:start position:0% thing to do but we want to try it anyway 00:24:07.410 --> 00:24:09.170 align:start position:0% thing to do but we want to try it anyway and<00:24:07.590> also<00:24:07.920> one<00:24:08.520> other<00:24:08.550> thing<00:24:08.700> we<00:24:09.030> want 00:24:09.170 --> 00:24:09.180 align:start position:0% and also one other thing we want 00:24:09.180 --> 00:24:13.100 align:start position:0% and also one other thing we want introduced<00:24:09.540> rudder<00:24:10.430> soon<00:24:11.430> is<00:24:11.870> actually<00:24:12.870> the 00:24:13.100 --> 00:24:13.110 align:start position:0% introduced rudder soon is actually the 00:24:13.110 --> 00:24:17.690 align:start position:0% introduced rudder soon is actually the ability<00:24:13.410> to<00:24:13.650> let<00:24:15.650> that<00:24:16.650> developers<00:24:17.220> give<00:24:17.490> this 00:24:17.690 --> 00:24:17.700 align:start position:0% ability to let that developers give this 00:24:17.700 --> 00:24:22.690 align:start position:0% ability to let that developers give this variance<00:24:18.150> so<00:24:18.500> something<00:24:19.500> like<00:24:20.450> you<00:24:21.450> could 00:24:22.690 --> 00:24:22.700 align:start position:0% variance so something like you could 00:24:22.700 --> 00:24:25.760 align:start position:0% variance so something like you could write<00:24:23.700> something<00:24:23.940> like<00:24:24.470> declare<00:24:25.470> your 00:24:25.760 --> 00:24:25.770 align:start position:0% write something like declare your 00:24:25.770 --> 00:24:33.740 align:start position:0% write something like declare your invariants<00:24:26.340> and<00:24:31.850> this<00:24:32.850> would<00:24:33.060> be<00:24:33.210> one<00:24:33.450> of<00:24:33.480> them 00:24:33.740 --> 00:24:33.750 align:start position:0% invariants and this would be one of them 00:24:33.750 --> 00:24:37.010 align:start position:0% invariants and this would be one of them and<00:24:34.970> with<00:24:35.970> this<00:24:36.090> invariant<00:24:36.540> is<00:24:36.630> invariant 00:24:37.010 --> 00:24:37.020 align:start position:0% and with this invariant is invariant 00:24:37.020 --> 00:24:38.480 align:start position:0% and with this invariant is invariant would<00:24:37.230> be<00:24:37.350> applied<00:24:37.650> as<00:24:37.890> a<00:24:37.920> require<00:24:38.280> in<00:24:38.400> the 00:24:38.480 --> 00:24:38.490 align:start position:0% would be applied as a require in the 00:24:38.490 --> 00:24:40.550 align:start position:0% would be applied as a require in the beginning<00:24:38.760> of<00:24:38.820> every<00:24:38.940> function<00:24:39.450> and<00:24:39.570> asserted 00:24:40.550 --> 00:24:40.560 align:start position:0% beginning of every function and asserted 00:24:40.560 --> 00:24:44.780 align:start position:0% beginning of every function and asserted in<00:24:40.710> the<00:24:40.830> end<00:24:40.950> of<00:24:41.250> every<00:24:41.520> function<00:24:42.350> in<00:24:43.350> Diani<00:24:44.100> we 00:24:44.780 --> 00:24:44.790 align:start position:0% in the end of every function in Diani we 00:24:44.790 --> 00:24:46.610 align:start position:0% in the end of every function in Diani we could<00:24:45.090> even<00:24:45.420> use<00:24:45.570> that<00:24:45.900> to<00:24:46.080> get<00:24:46.170> inductive 00:24:46.610 --> 00:24:46.620 align:start position:0% could even use that to get inductive 00:24:46.620 --> 00:24:51.980 align:start position:0% could even use that to get inductive proofs<00:24:47.210> and<00:24:49.160> yeah<00:24:50.160> just<00:24:50.700> get<00:24:51.240> give<00:24:51.540> more<00:24:51.750> power 00:24:51.980 --> 00:24:51.990 align:start position:0% proofs and yeah just get give more power 00:24:51.990 --> 00:24:54.350 align:start position:0% proofs and yeah just get give more power mm<00:24:52.500> jacquard<00:24:52.800> and<00:24:52.920> actually<00:24:53.190> get<00:24:53.360> harder 00:24:54.350 --> 00:24:54.360 align:start position:0% mm jacquard and actually get harder 00:24:54.360 --> 00:24:56.480 align:start position:0% mm jacquard and actually get harder properties<00:24:54.990> proven<00:24:55.530> anyway<00:24:55.950> even<00:24:56.250> though 00:24:56.480 --> 00:24:56.490 align:start position:0% properties proven anyway even though 00:24:56.490 --> 00:25:00.260 align:start position:0% properties proven anyway even though they're<00:24:56.760> pretty<00:24:57.060> hard<00:24:58.370> so<00:24:59.370> yeah<00:24:59.520> open<00:25:00.060> for 00:25:00.260 --> 00:25:00.270 align:start position:0% they're pretty hard so yeah open for 00:25:00.270 --> 00:25:02.810 align:start position:0% they're pretty hard so yeah open for questions<00:25:00.360> not<00:25:00.750> sure<00:25:00.960> how<00:25:01.770> much<00:25:01.950> time<00:25:02.490> there's 00:25:02.810 --> 00:25:02.820 align:start position:0% questions not sure how much time there's 00:25:02.820 --> 00:25:06.020 align:start position:0% questions not sure how much time there's left<00:25:03.030> yeah<00:25:03.720> no<00:25:03.900> time<00:25:04.050> left<00:25:04.290> so<00:25:04.550> we<00:25:05.550> can<00:25:05.730> discuss 00:25:06.020 --> 00:25:06.030 align:start position:0% left yeah no time left so we can discuss 00:25:06.030 --> 00:25:17.550 align:start position:0% left yeah no time left so we can discuss offline<00:25:06.470> time<00:25:07.470> is<00:25:07.560> gone<00:25:07.710> thank<00:25:08.580> you 00:25:17.550 --> 00:25:17.560 align:start position:0% 00:25:17.560 --> 00:25:19.620 align:start position:0% you